Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

added dsl blocks

  • Loading branch information...
commit dc3f0f9afdf0880a53897f65b0ac881b2cdee809 1 parent c08dff7
Edwin Brady authored
View
2  idris.cabal
@@ -61,7 +61,7 @@ Executable idris
Idris.Delaborate, Idris.Primitives, Idris.Imports,
Idris.Compiler, Idris.Prover, Idris.ElabTerm,
Idris.Coverage, Idris.IBC, Idris.Unlit,
- Idris.DataOpts, Idris.Transforms,
+ Idris.DataOpts, Idris.Transforms, Idris.DSL,
Paths_idris
View
22 samples/interp.idr
@@ -30,6 +30,12 @@ using (G : Vect Ty n)
Expr G c
If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
+
+ dsl expr
+ lambda = Lam
+ variable = Var
+ index_first = stop
+ index_next = pop
interp : Env G -> {static} Expr G t -> interpTy t
interp env (Var i) = lookup i env
@@ -39,28 +45,29 @@ using (G : Vect Ty n)
interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e)
interp env (Bind v f) = interp env (f (interp env v))
-
+
eId : Expr G (TyFun TyInt TyInt)
- eId = Lam (Var stop)
+ eId = expr (\x => x)
eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
- eTEST = Lam (Lam (Var (pop stop)))
+ eTEST = expr (\x, y => y)
eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
- eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))))
+ eAdd = expr (\x, y => Op (+) x y)
-- eDouble : Expr G (TyFun TyInt TyInt)
-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))
eDouble : Expr G (TyFun TyInt TyInt)
- eDouble = Lam (App (App eAdd (Var stop)) (Var stop))
+ eDouble = expr (\x => App (App eAdd x) (Var stop))
app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
app = \f, a => App f a
eFac : Expr G (TyFun TyInt TyInt)
- eFac = Lam (If (Op (==) (Var stop) (Val 0))
- (Val 1) (Op (*) (app eFac (Op (-) (Var stop) (Val 1))) (Var stop)))
+ eFac = expr (\x => If (Op (==) x (Val 0))
+ (Val 1)
+ (Op (*) (app eFac (Op (-) x (Val 1))) x))
-- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
@@ -70,6 +77,7 @@ using (G : Vect Ty n)
(\y => Bind (App eDouble (Val x))
(\z => App (App eAdd (Val y)) (Val z))))))
+
test : Int
test = interp [] eProg 2 2
View
32 src/Idris/AbsSyntax.hs
@@ -40,6 +40,7 @@ data IState = IState { tt_ctxt :: Context,
idris_implicits :: Ctxt [PArg],
idris_statics :: Ctxt [Bool],
idris_classes :: Ctxt ClassInfo,
+ idris_dsls :: Ctxt DSL,
idris_optimisation :: Ctxt OptInfo,
idris_datatypes :: Ctxt TypeInfo,
idris_patdefs :: Ctxt [(Term, Term)], -- not exported
@@ -70,6 +71,7 @@ data IBCWrite = IBCFix FixDecl
| IBCImp Name
| IBCStatic Name
| IBCClass Name
+ | IBCDSL Name
| IBCData Name
| IBCOpt Name
| IBCSyntax Syntax
@@ -83,7 +85,7 @@ data IBCWrite = IBCFix FixDecl
deriving Show
idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
- emptyContext emptyContext emptyContext
+ emptyContext emptyContext emptyContext emptyContext
"" defaultOpts 6 [] [] [] [] [] [] [] []
Nothing Nothing Nothing [] [] [] Hidden [] Nothing
@@ -372,6 +374,7 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration
[t] -- parameters
t -- full instance type
[PDecl' t]
+ | PDSL Name (DSL' t)
| PSyntax FC Syntax
| PDirective (Idris ())
deriving Functor
@@ -558,16 +561,22 @@ deriving instance Binary TypeInfo
-- Syntactic sugar info
-data DSL = DSL { dsl_bind :: PTerm,
- dsl_return :: PTerm,
- dsl_apply :: PTerm,
- dsl_pure :: PTerm,
- index_first :: Maybe PTerm,
- index_next :: Maybe PTerm,
- dsl_lambda :: Maybe PTerm,
- dsl_let :: Maybe PTerm
- }
- deriving Show
+data DSL' t = DSL { dsl_bind :: t,
+ dsl_return :: t,
+ dsl_apply :: t,
+ dsl_pure :: t,
+ dsl_var :: Maybe t,
+ index_first :: Maybe t,
+ index_next :: Maybe t,
+ dsl_lambda :: Maybe t,
+ dsl_let :: Maybe t
+ }
+ deriving (Show, Functor)
+{-!
+deriving instance Binary DSL'
+!-}
+
+type DSL = DSL' PTerm
data SynContext = PatternSyntax | TermSyntax | AnySyntax
deriving Show
@@ -598,6 +607,7 @@ initDSL = DSL (PRef f (UN ">>="))
Nothing
Nothing
Nothing
+ Nothing
where f = FC "(builtin)" 0
data SyntaxInfo = Syn { using :: [(Name, PTerm)],
View
105 src/Idris/DSL.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE PatternGuards #-}
+
+module Idris.DSL where
+
+import Idris.AbsSyntax
+import Paths_idris
+
+import Core.CoreParser
+import Core.TT
+import Core.Evaluate
+
+desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
+desugar syn i t = let t' = expandDo (dsl_info syn) t in
+ t' -- addImpl i t'
+
+expandDo :: DSL -> PTerm -> PTerm
+expandDo dsl (PLam n ty tm)
+ | Just lam <- dsl_lambda dsl
+ = let sc = PApp (FC "(dsl)" 0) lam [pexp (var dsl n tm 0)] in
+ expandDo dsl sc
+expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)
+expandDo dsl (PLet n ty v tm)
+ | Just letb <- dsl_let dsl
+ = let sc = PApp (FC "(dsl)" 0) letb [pexp v, pexp (var dsl n tm 0)] in
+ expandDo dsl sc
+expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
+expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
+expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
+ (map (fmap (expandDo dsl)) args)
+expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)
+ (map (pmap (expandDo dsl)) opts)
+expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)
+expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)
+ (expandDo dsl r)
+expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as)
+expandDo dsl (PHidden t) = PHidden (expandDo dsl t)
+expandDo dsl (PReturn fc) = dsl_return dsl
+expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds
+ where
+ block b [DoExp fc tm] = tm
+ block b [a] = PElabError "Last statement in do block must be an expression"
+ block b (DoBind fc n tm : rest)
+ = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]
+ block b (DoBindP fc p tm : rest)
+ = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder
+ (PCase fc (PRef fc (MN 0 "bpat"))
+ [(p, block b rest)]))]
+ block b (DoLet fc n ty tm : rest)
+ = PLet n ty tm (block b rest)
+ block b (DoLetP fc p tm : rest)
+ = PCase fc tm [(p, block b rest)]
+ block b (DoExp fc tm : rest)
+ = PApp fc b
+ [pexp tm,
+ pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]
+ block b _ = PElabError "Invalid statement in do block"
+
+expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
+expandDo dsl t = t
+
+var :: DSL -> Name -> PTerm -> Int -> PTerm
+var dsl n t i = v' i t where
+ v' i (PRef fc x) | x == n =
+ case dsl_var dsl of
+ Nothing -> PElabError "No 'variable' defined in dsl"
+ Just v -> PApp fc v [pexp (mkVar fc i)]
+ v' i (PLam n ty sc)
+ | Nothing <- dsl_lambda dsl
+ = PLam n ty (v' i sc)
+ | otherwise = PLam n (v' i ty) (v' (i + 1) sc)
+ v' i (PLet n ty val sc)
+ | Nothing <- dsl_let dsl
+ = PLet n (v' i ty) (v' i val) (v' i sc)
+ | otherwise = PLet n (v' i ty) (v' i val) (v' (i + 1) sc)
+ v' i (PPi p n ty sc) = PPi p n (v' i ty) (v' i sc)
+ v' i (PTyped l r) = PTyped (v' i l) (v' i r)
+ v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)
+ v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)
+ v' i (PEq f l r) = PEq f (v' i l) (v' i r)
+ v' i (PPair f l r) = PPair f (v' i l) (v' i r)
+ v' i (PDPair f l t r) = PDPair f (v' i l) (v' i t) (v' i r)
+ v' i (PAlternative as) = PAlternative $ map (v' i) as
+ v' i (PHidden t) = PHidden (v' i t)
+ v' i (PIdiom f t) = PIdiom f (v' i t)
+ v' i t = t
+
+ mkVar fc 0 = case index_first dsl of
+ Nothing -> PElabError "No index_first defined"
+ Just f -> f
+ mkVar fc n = case index_next dsl of
+ Nothing -> PElabError "No index_next defined"
+ Just f -> PApp fc f [pexp (mkVar fc (n-1))]
+
+unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
+unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in
+ mkap (getFn e)
+ where
+ getFn (PApp fc f args) = (PApp fc pure [pexp f], args)
+ getFn f = (f, [])
+
+ mkap (f, []) = f
+ mkap (f, a:as) = mkap (PApp fc ap [pexp f, a], as)
+
+unIdiom ap pure fc e = PApp fc pure [pexp e]
+
View
6 src/Idris/ElabDecls.hs
@@ -3,6 +3,7 @@
module Idris.ElabDecls where
import Idris.AbsSyntax
+import Idris.DSL
import Idris.Error
import Idris.Delaborate
import Idris.Imports
@@ -623,6 +624,11 @@ elabDecl' info (PInstance s f cs n ps t ds)
elabDecl' info (PRecord s f tyn ty cn cty)
= do iLOG $ "Elaborating record " ++ show tyn
elabRecord info s f tyn ty cn cty
+elabDecl' info (PDSL n dsl)
+ = do i <- get
+ put (i { idris_dsls = addDef n dsl (idris_dsls i) })
+ addIBC (IBCDSL n)
+
elabDecl' info (PDirective i) = i
elabCaseBlock info d@(PClauses f o n ps)
View
7 src/Idris/ElabTerm.hs
@@ -1,6 +1,9 @@
+{-# LANGUAGE PatternGuards #-}
+
module Idris.ElabTerm where
import Idris.AbsSyntax
+import Idris.DSL
import Core.Elaborate hiding (Tactic(..))
import Core.TT
@@ -191,6 +194,10 @@ elab ist info pattern tcgen fn tm
-- elabE True ty
-- focus valn
-- elabE True val
+-- elab' ina (PApp fc (PRef _ dsl) [arg])
+-- | [d] <- lookupCtxt Nothing dsl (idris_dsls ist)
+-- = let dsl' = expandDo d (getTm arg) in
+-- trace (show dsl') $ elab' ina dsl'
elab' ina (PApp fc (PRef _ f) args')
= do let args = {- case lookupCtxt f (inblock info) of
Just ps -> (map (pexp . (PRef fc)) ps ++ args')
View
45 src/Idris/IBC.hs
@@ -22,7 +22,7 @@ import System.Directory
import Paths_idris
ibcVersion :: Word8
-ibcVersion = 9
+ibcVersion = 10
data IBCFile = IBCFile { ver :: Word8,
sourcefile :: FilePath,
@@ -31,6 +31,7 @@ data IBCFile = IBCFile { ver :: Word8,
ibc_fixes :: [FixDecl],
ibc_statics :: [(Name, [Bool])],
ibc_classes :: [(Name, ClassInfo)],
+ ibc_dsls :: [(Name, DSL)],
ibc_datatypes :: [(Name, TypeInfo)],
ibc_optimise :: [(Name, OptInfo)],
ibc_syntax :: [Syntax],
@@ -45,7 +46,7 @@ deriving instance Binary IBCFile
!-}
initIBC :: IBCFile
-initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] []
+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] []
loadIBC :: FilePath -> Idris ()
loadIBC fp = do iLOG $ "Loading ibc " ++ fp
@@ -84,6 +85,10 @@ ibc i (IBCClass n) f
= case lookupCtxt Nothing n (idris_classes i) of
[v] -> return f { ibc_classes = (n,v): ibc_classes f }
_ -> fail "IBC write failed"
+ibc i (IBCDSL n) f
+ = case lookupCtxt Nothing n (idris_dsls i) of
+ [v] -> return f { ibc_dsls = (n,v): ibc_dsls f }
+ _ -> fail "IBC write failed"
ibc i (IBCData n) f
= case lookupCtxt Nothing n (idris_datatypes i) of
[v] -> return f { ibc_datatypes = (n,v): ibc_datatypes f }
@@ -116,6 +121,7 @@ process i fn
pFixes (ibc_fixes i)
pStatics (ibc_statics i)
pClasses (ibc_classes i)
+ pDSLs (ibc_dsls i)
pDatatypes (ibc_datatypes i)
pOptimise (ibc_optimise i)
pSyntax (ibc_syntax i)
@@ -174,6 +180,13 @@ pClasses cs = mapM_ (\ (n, c) ->
= addDef n c (idris_classes i) }))
cs
+pDSLs :: [(Name, DSL)] -> Idris ()
+pDSLs cs = mapM_ (\ (n, c) ->
+ do i <- getIState
+ putIState (i { idris_dsls
+ = addDef n c (idris_dsls i) }))
+ cs
+
pDatatypes :: [(Name, TypeInfo)] -> Idris ()
pDatatypes cs = mapM_ (\ (n, c) ->
do i <- getIState
@@ -568,7 +581,7 @@ instance Binary Accessibility where
_ -> error "Corrupted binary data for Accessibility"
instance Binary IBCFile where
- put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)
+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17)
= do put x1
put x2
put x3
@@ -585,6 +598,7 @@ instance Binary IBCFile where
put x14
put x15
put x16
+ put x17
get
= do x1 <- get
if x1 == ibcVersion then
@@ -603,7 +617,8 @@ instance Binary IBCFile where
x14 <- get
x15 <- get
x16 <- get
- return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)
+ x17 <- get
+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17)
else return (initIBC { ver = x1 })
instance Binary Fixity where
@@ -1024,6 +1039,28 @@ instance Binary Syntax where
x3 <- get
return (Rule x1 x2 x3)
+instance (Binary t) => Binary (DSL' t) where
+ put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)
+ = do put x1
+ put x2
+ put x3
+ put x4
+ put x5
+ put x6
+ put x7
+ put x8
+ put x9
+ get
+ = do x1 <- get
+ x2 <- get
+ x3 <- get
+ x4 <- get
+ x5 <- get
+ x6 <- get
+ x7 <- get
+ x8 <- get
+ x9 <- get
+ return (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9)
instance Binary SSymbol where
put x
View
103 src/Idris/Parser.hs
@@ -1,6 +1,9 @@
+{-# LANGUAGE PatternGuards #-}
+
module Idris.Parser where
import Idris.AbsSyntax
+import Idris.DSL
import Idris.Imports
import Idris.Error
import Idris.ElabDecls
@@ -310,6 +313,7 @@ pDecl syn = do notEndBlock
<|> pNamespace syn
<|> pClass syn
<|> pInstance syn
+ <|> do d <- pDSL syn; return [d]
<|> pDirective
<|> try (do reserved "import"
fp <- identifier
@@ -728,7 +732,13 @@ pApp syn = do f <- pSimpleExpr syn
fc <- pfc
args <- many1 (do notEndApp
pArg syn)
- return (PApp fc f args)
+ i <- getState
+ return (dslify i $ PApp fc f args)
+ where
+ dslify i (PApp fc (PRef _ f) [a])
+ | [d] <- lookupCtxt Nothing f (idris_dsls i)
+ = desugar (syn { dsl_info = d }) i (getTm a)
+ dslify i t = t
pArg :: SyntaxInfo -> IParser PArg
pArg syn = try (pImplicitArg syn)
@@ -979,6 +989,45 @@ pSimpleCon syn
pSimpleExpr syn)
return (cn, args, fc)
+--------- DSL syntax overloading ---------
+
+pDSL :: SyntaxInfo -> IParser PDecl
+pDSL syn = do reserved "dsl"; n <- pfName
+ open_block; push_indent
+ bs <- many1 (do notEndBlock
+ b <- pOverload syn
+ pKeepTerminator
+ return b)
+ pop_indent; close_block
+ let dsl = mkDSL bs (dsl_info syn)
+ checkDSL dsl
+ i <- getState
+ setState (i { idris_dsls = addDef n dsl (idris_dsls i) })
+ return (PDSL n dsl)
+ where mkDSL bs dsl = let var = lookup "variable" bs
+ first = lookup "index_first" bs
+ next = lookup "index_next" bs
+ leto = lookup "let" bs
+ lambda = lookup "lambda" bs in
+ initDSL { dsl_var = var,
+ index_first = first,
+ index_next = next,
+ dsl_lambda = lambda,
+ dsl_let = leto }
+
+checkDSL :: DSL -> IParser ()
+checkDSL dsl = return ()
+
+pOverload :: SyntaxInfo -> IParser (String, PTerm)
+pOverload syn = do o <- identifier <|> do reserved "let"; return "let"
+ if (not (o `elem` overloadable))
+ then fail $ show o ++ " is not an overloading"
+ else do
+ lchar '='
+ t <- pExpr syn
+ return (o, t)
+ where overloadable = ["let","lambda","index_first","index_next","variable"]
+
--------- Pattern match clauses ---------
pPattern :: SyntaxInfo -> IParser PDecl
@@ -1193,55 +1242,3 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
imp = do lchar '?'; return False
<|> do lchar '_'; return True
-desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
-desugar syn i t = let t' = expandDo (dsl_info syn) t in
- t' -- addImpl i t'
-
-expandDo :: DSL -> PTerm -> PTerm
-expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)
-expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)
-expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
-expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
- (map (fmap (expandDo dsl)) args)
-expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)
- (map (pmap (expandDo dsl)) opts)
-expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)
-expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)
- (expandDo dsl r)
-expandDo dsl (PAlternative as) = PAlternative (map (expandDo dsl) as)
-expandDo dsl (PHidden t) = PHidden (expandDo dsl t)
-expandDo dsl (PReturn fc) = dsl_return dsl
-expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds
- where
- block b [DoExp fc tm] = tm
- block b [a] = PElabError "Last statement in do block must be an expression"
- block b (DoBind fc n tm : rest)
- = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]
- block b (DoBindP fc p tm : rest)
- = PApp fc b [pexp tm, pexp (PLam (MN 0 "bpat") Placeholder
- (PCase fc (PRef fc (MN 0 "bpat"))
- [(p, block b rest)]))]
- block b (DoLet fc n ty tm : rest)
- = PLet n ty tm (block b rest)
- block b (DoLetP fc p tm : rest)
- = PCase fc tm [(p, block b rest)]
- block b (DoExp fc tm : rest)
- = PApp fc b
- [pexp tm,
- pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]
- block b _ = PElabError "Invalid statement in do block"
-expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
-expandDo dsl t = t
-
-unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
-unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in
- mkap (getFn e)
- where
- getFn (PApp fc f args) = (PApp fc pure [pexp f], args)
- getFn f = (f, [])
-
- mkap (f, []) = f
- mkap (f, a:as) = mkap (PApp fc ap [pexp f, a], as)
-
-unIdiom ap pure fc e = PApp fc pure [pexp e]
-
View
21 test/test001/test001.idr
@@ -30,7 +30,13 @@ using (G : Vect Ty n) {
Expr G c
If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b
-
+
+ dsl expr
+ lambda = Lam
+ variable = Var
+ index_first = stop
+ index_next = pop
+
interp : Env G -> {static} Expr G t -> interpTy t
interp env (Var i) = lookup i env
interp env (Val x) = x
@@ -41,26 +47,27 @@ using (G : Vect Ty n) {
interp env (Bind v f) = interp env (f (interp env v))
eId : Expr G (TyFun TyInt TyInt)
- eId = Lam (Var stop)
+ eId = expr (\x => x)
eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
- eTEST = Lam (Lam (Var (pop stop)))
+ eTEST = expr (\x, y => y)
eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
- eAdd = Lam (Lam (Op prim__addInt (Var stop) (Var (pop stop))))
+ eAdd = expr (\x, y => Op (+) x y)
-- eDouble : Expr G (TyFun TyInt TyInt)
-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO))
eDouble : Expr G (TyFun TyInt TyInt)
- eDouble = Lam (App (App eAdd (Var stop)) (Var stop))
+ eDouble = expr (\x => App (App eAdd x) (Var stop))
app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t
app = \f, a => App f a
eFac : Expr G (TyFun TyInt TyInt)
- eFac = Lam (If (Op (==) (Var stop) (Val 0))
- (Val 1) (Op (*) (app eFac (Op (-) (Var stop) (Val 1))) (Var stop)))
+ eFac = expr (\x => If (Op (==) x (Val 0))
+ (Val 1)
+ (Op (*) (app eFac (Op (-) x (Val 1))) x))
-- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
Please sign in to comment.
Something went wrong with that request. Please try again.