I don't fully understand this: - The Piece type uses CondP, ListConsP, whereas your quoted fragments use Cont, (:). I think you are saying that you want to use Haskell syntax to write rewrite rules, which are then munged into real Haskell by your make_rule function. I don't really understand what values are used in the quoted stuff. I'm rather dubious about switching off the type checker for quotations, although I can see that (as you say) it's a pretty non-invasive change. I suggest you discuss this with Oege, work on your examples, see if there are any alternatives, and come back to the TH list if you're still convinced. Simon | -----Original Message----- | From: Ian Lynagh [mailto:igloo@earth.li] | Sent: 08 April 2003 14:26 | To: Simon Peyton-Jones | Cc: template-haskell@haskell.org | | On Tue, Apr 08, 2003 at 01:48:24PM +0100, Simon Peyton-Jones wrote: | > I didn't understand this. Care to elaborate, with some examples? | | OK, the key point is that it is easier, should you want to build an | expression that doesn't type check, to have GHC do it for you than to | write App (Con "Tup") (...) by hand. | | In this particular case (which is a reimplementation of pan) I have | (I've cut this down a lot): | | data Piece = | -- Exp | AppP Addr Addr | | CondP Addr Addr Addr | | TupP Addr | -- DotDot | | FromP Addr | -- [a] | | ListConsP Addr Addr | | ListNilP | | which I can use to represent the syntax trees as DAGs with a FiniteMap | in each direction (Piece -> Addr, Addr -> Piece). | | Something I want to be able to do is to float ifs up as then I can | simplify more, e.g., | 1 + (if g then 2 else 3) | to | if g then 3 else 4 | | So I have a function make_opt_rule :: Exp -> Exp so, for example: | | ======================= | do rule <- runQ [| \g x y z -> App x (Cond g y z) | --> | Cond g (App x y) (App x z) |] | putStrLn $ render $ pprExp $ make_opt_rule rule | ======================= | | produces: | | ======================= | \p -> case p of | AppP x'1 aopt@1 ->i | do popt@1 <- look_at aopt@1 | case popt@1 of | CondP g'0 y'2 z'3 -> | do addr@0 <- local_opt (AppP x'1 y'2) | addr@1 <- local_opt (AppP x'1 z'3) | addr@2 <- local_opt (CondP g'0 addr@0 addr@1) | return (Just addr@2) | _ -> return Nothing | _ -> return Nothing | ======================= | | Now, this one is fine because both sides of the rule correspond to valid | Haskell expressions. But I also want to rewrite | (0, if g then 1 else 2, 3) | to | if g then (0, 1, 3) else (0, 2, 3) | | Now, as it turns out it is fine to do locally bad rewrites like | | [| \g x y z -> (:) (Cond g x y) z --> Cond g ((:) x z) ((:) y z) |n], | [| \g x y z -> (:) x (Cond g y z) --> Cond g ((:) x y) ((:) x z) |n], | | (which moves the Cond up through the list of expressions wrapped by Tup) | as when it gets to the top it will be rewritten again with | | [| \g x y -> Tup (Cond g x y) --> Cond g (Tup x) (Tup y) |n], | | and we are back with a valid datastructure represented by the DAG. | Turning off type checking allows me to tell GHC that I know that what I | am doing looks bad, but if it looks the other way for a minute it'll all | turn out OK in the end (both in terms of the code spliced in (which | operates on Pieces) and the DAG that will ultimately be flattened). | | | Did that make sense? | | | Thanks | Ian |