Embedded Language Example

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> 

 


metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.