The only example I can find is from David Christiansen’s PhD thesis
(see also Epic)
Here the recursive datatype 'Lang' defines a simple language to define an expression.
'exampleFun' is a function, written in that language, to add two integers.
'elabLang' takes the language definition and a function written in the language to produce the elaborator code.
|
import Data.Fin
import Data.Vect
%language ElabReflection
||| A simple language to define an expression
data Lang : Nat -> Type where
||| A fixed length list of variables
||| Gives a name for each de Bruijn index.
V : Fin n -> Lang n
||| Function application,
Ap : Lang n -> Lang n -> Lang n
||| A lambda function
Lam : Lang (S n) -> Lang n
||| Integer constant
CstI : Integer -> Lang n
||| Calls primitave operators by name
FFI : TTName -> Lang n
exampleFun : Lang 0
exampleFun = Lam $ Lam $
Ap (Ap (FFI `{prim__addBigInt})
(V 0))
(V 1)
mkHole : Raw -> Elab TTName
mkHole r = do x <- gensym "t"
claim x r
pure x
elabLang : Vect k TTName -> Lang k -> Elab ()
elabLang ctxt (V i) = do fill (Var (index i ctxt))
solve
elabLang ctxt (CstI x) = do fill (quote x)
solve
elabLang ctxt (Lam x) =
do n <- gensym "argument"
attack
intro n
elabLang (n :: ctxt) x
solve
elabLang ctxt (Ap x y) =
do t1 <- mkHole `(Type)
t2 <- mkHole `(Type)
fun <- mkHole `(~(Var t1) -> ~(Var t2))
arg <- mkHole (Var t1)
fill (RApp (Var fun) (Var arg))
solve
focus fun; elabLang ctxt x
focus arg; elabLang ctxt y
elabLang ctxt (FFI n) =
do fill (Var n)
solve
compiled : Integer -> Integer -> Integer
compiled = %runElab (elabLang [] exampleFun) |
|
Evaluating compiled gives:
\argument1 => \argument2 => prim__addBigInt argument2 argument1
*embed> compiled 1 2
3 : Integer
*embed>*embed> :doc exampleFun
Main.exampleFun : Lang (fromInteger 0)
The function is: Total & public export
*embed>
:doc compiled
Main.compiled : Integer -> Integer -> Integer
The function is: Total & public export
*embed>
|
