# Embedded Language Example

The only example I can find is from David Christiansen’s PhD thesis

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> ```