[Haskell-cafe] Compile-time evaluation

[Robin Green]

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