[Haskell-cafe] Compile-time evaluation
Robin Green
greenrd at greenrd.org
Fri Nov 2 07:09:55 EDT 2007
On Fri, 2 Nov 2007 05:11:53 -0500
"Nicholas Messenger" <nmessenger at gmail.com> wrote:
> -- Many people ask if GHC will evaluate toplevel constants at compile
> -- time, you know, since Haskell is pure it'd be great if those
> -- computations could be done once and not use up cycles during
> -- runtime. Not an entirely bad idea, I think.
I implemented the same idea. First a note about nomenclature: since
there is a Template Haskell class for the concept of "translating actual
values into TH representations of those values" called Lift, I call that
"lifting"; I also call evaluating and storing top-level constants at
compile time "baking them into the executable".
>From glancing at your code, my approach has two main differences
(apart from the fact that I didn't implement support for all of the
types that you did):
1. A generic lifter using Data.Generics does not work for certain
types, like IntSet. So I implemented the Template Haskell class Lift
for each of my own data types that I wanted to use in lifting, and
where it would work, called my generic lifter function, otherwise
lifted it more manually (as shown below).
2. I used synthesise instead of gmapQ, and did not use an intermediate
Tree data structure.
Here is the module which does most of the work. (You will not be able to
compile this as-is, obviously, because I have not published the rest of
my code yet.)
{-# OPTIONS_GHC -fglasgow-exts -fallow-overlapping-instances
-fallow-undecidable-instances -XTemplateHaskell #-}
module Language.Coq.Syntax.AbstractionBaking where
import Data.Generics.Basics (ConstrRep(..), constrRep, Data, toConstr,
Typeable)
import Data.Generics.Schemes (synthesize)
import Data.List (foldl')
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet (fromList, toList)
import Data.Set (Set)
import qualified Data.Set as Set (fromList, toList)
import Language.Haskell.TH.Lib (appE, charL, conE, ExpQ, infixE,
integerL, litE)
import Language.Haskell.TH.Syntax (Lift(..), mkName)
import System.FilePath ((</>))
import Data.DList (DList)
import Data.ListLike (fromList, ListLike, toList)
import Language.Coq.Parser (CoqParserState(..))
import Language.Coq.Syntax.Abstract (CoqState(..), Sentence, Term)
import Language.Coq.Syntax.Concrete (NotationRec(..))
import Language.Coq.Syntax.ParseSpec
lifter :: Data d => d -> ExpQ
lifter = head . synthesize [] (++) combiner
where
combiner x args = [case rep of
IntConstr i -> litE $ integerL i
AlgConstr _ -> algebraic (show constr) args
StringConstr (h:_) -> litE $ charL h
_ -> fail $ "Unimplemented constrRep: " ++
show rep]
where constr = toConstr x
rep = constrRep constr
algebraic "(:)" = cons
algebraic name = foldl' appE $ conE $ mkName name
cons [] = [e| (:) |]
cons [left] = infixE (Just left) (cons []) Nothing
cons [left, right] = infixE (Just left) (cons []) $
Just right
instance Lift NotationRec where
lift (NotationRec w x y z)
= appE (appE (appE (appE [| NotationRec |] $ lift w) $ lift x)
$ lift y) $ lift z
instance Lift ParseSpecTok where
lift = lifter
instance Lift Associativity where
lift = lifter
instance Lift Sentence where
lift = lifter
instance Lift Term where
lift = lifter
instance Lift CoqState where
lift (CoqState x y) = appE (appE [| CoqState |] $ lift x) $ lift y
instance Lift CoqParserState where
lift (CoqParserState x y z) = appE (appE (appE [| CoqParserState |]
$ lift x) $ lift y) $ lift z
instance (Lift a, ListLike full a) => Lift full where
lift = appE [| fromList |] . lift . toList
instance Lift IntSet where
lift = appE [| IntSet.fromList |] . lift . IntSet.toList
instance Lift a => Lift (Set a) where
lift = appE [| Set.fromList |] . lift . Set.toList
--
Robin
More information about the Haskell-Cafe
mailing list