hide term compilation monad

Author: flupe

src/Agda2Lambox/Compile/Function.hs

@@ -20,7 +20,7 @@ import Agda.Utils.Monad (guardWithError)
 
 import Agda.Utils ( etaExpandCtor )
 import Agda2Lambox.Compile.Utils
-import Agda2Lambox.Compile.Term ( runC, compileTerm, withMutuals )
+import Agda2Lambox.Compile.Term ( compileTerm )
 import LambdaBox qualified as LBox
 
 
@@ -32,9 +32,9 @@ isFunction _ = False
 
 -- | Convert a function body to a Lambdabox term.
 compileFunctionBody :: [QName] -> Definition -> TCM LBox.Term
-compileFunctionBody fixpoints Defn{defName} = do
+compileFunctionBody ms Defn{defName} = do
     Just t <-toTreeless EagerEvaluation defName
-    runC . withMutuals fixpoints . compileTerm =<< etaExpandCtor t
+    compileTerm ms =<< etaExpandCtor t
 
 
 -- | Whether to compile a function definition to λ□.

src/Agda2Lambox/Compile/Term.hs

@@ -1,9 +1,6 @@
 {-# LANGUAGE NamedFieldPuns, DerivingVia, GeneralizedNewtypeDeriving #-}
 module Agda2Lambox.Compile.Term
-  ( C
-  , runC
-  , withMutuals
-  , compileTerm
+  ( compileTerm
   ) where
 
 import Control.Monad ( mapM )
@@ -74,8 +71,16 @@ withMutuals ms = local \e -> e { mutuals = reverse ms }
 -- * Term conversion
 
 -- | Convert a treeless term to its λ□ equivalent.
-compileTerm :: TTerm -> C LBox.Term
-compileTerm = \case
+compileTerm
+  :: [QName]
+     -- ^ Local fixpoints.
+  -> TTerm
+  -> TCM LBox.Term
+compileTerm ms = runC . withMutuals ms . compileTermC
+
+-- | Convert a treeless term to its λ□ equivalent.
+compileTermC :: TTerm -> C LBox.Term
+compileTermC = \case
   TVar  n -> pure $ LRel n
   TPrim p -> fail "primitives not supported"
 
@@ -86,20 +91,20 @@ compileTerm = \case
       Just i  -> LRel   $ i + boundVars
 
   TCon q             -> liftTCM $ toConApp q []
-  TApp (TCon q) args -> liftTCM . toConApp q =<< mapM compileTerm args
+  TApp (TCon q) args -> liftTCM . toConApp q =<< mapM compileTermC args
   -- ^ For dealing with fully-applied constructors
 
   TApp u es -> do
-    cu  <- compileTerm u
-    ces <- mapM compileTerm es
+    cu  <- compileTermC u
+    ces <- mapM compileTermC es
     pure $ foldl' LApp cu ces
 
-  TLam t -> underBinder $ LLam <$> compileTerm t
+  TLam t -> underBinder $ LLam <$> compileTermC t
 
   TLit l -> fail "literals not supported"
 
-  TLet u v -> LLet <$> compileTerm u
-                   <*> underBinder (compileTerm v)
+  TLet u v -> LLet <$> compileTermC u
+                   <*> underBinder (compileTermC v)
 
   TCase n CaseInfo{..} dt talts ->
     case caseErased of
@@ -125,6 +130,6 @@ compileCaseType = \case
 compileAlt :: TAlt -> C ([LBox.Name], LBox.Term)
 compileAlt = \case
   TACon{..}   -> let names = take aArity $ repeat LBox.Anon
-                 in (names,) <$> underBinders aArity (compileTerm aBody)
+                 in (names,) <$> underBinders aArity (compileTermC aBody)
   TALit{..}   -> fail "literal patterns not supported"
   TAGuard{..} -> fail "case guards not supported"

theories/Eval.v

@@ -6,11 +6,42 @@ From MetaCoq.Erasure       Require Import EAst.
 From CertiCoq.Common       Require Import Common.
 From CertiCoq.LambdaBoxMut Require Import compile term program wcbvEval.
 
+
 (* TODO: eta-expand here *)
 
 (* convert a lambda box program to certicoq lambda box mut, and run it *)
 Definition eval_program (p : EAst.program) : exception Term :=
   let prog := {| env  := LambdaBoxMut.compile.compile_ctx (fst p);
       main := compile (snd p)
   |}
-  in wcbvEval (env prog) (2 ^ 14) (main prog).
+  in wcbvEval (env prog) (2 ^ 14) (main prog).
+
+
+(* Courtesy of Eske *)
+
+From CertiCoq Require Import LambdaBoxLocal.toplevel.
+From CertiCoq Require Import LambdaANF.toplevel.
+From CertiCoq Require Import Compiler.pipeline.
+Require Import ExtLib.Structures.Monad.
+Import MonadNotation.
+From CertiCoq Require Import Common.Common Common.compM Common.Pipeline_utils.
+
+Definition box_to_wasm (p : EAst.program) :=
+  (* For simplicity we assume that the program contains no primitives *)
+  let prims := [] in
+  let next_id := 100%positive in
+  let opts := default_opts in
+  (* Translate lambda_box -> lambda_boxmut *)
+  let p_mut := {| CertiCoq.Common.AstCommon.main := LambdaBoxMut.compile.compile (snd p) ; CertiCoq.Common.AstCommon.env := LambdaBoxMut.compile.compile_ctx (fst p) |} in
+  check_axioms prims p_mut;;
+  (* Translate lambda_boxmut -> lambda_boxlocal *)
+  p_local <- compile_LambdaBoxLocal prims p_mut;;
+  (* Translate lambda_boxlocal -> lambda_anf *)
+  p_anf <- compile_LambdaANF_ANF next_id prims p_local;;
+  (* Translate lambda_anf -> lambda_anf *)
+  p_anf <- compile_LambdaANF next_id p_anf;;
+  (* Compile lambda_anf -> WASM *)
+  compile_LambdaANF_to_Wasm prims p_anf.
+
+Definition test (p : EAst.program) :=
+  run_pipeline _ _ default_opts p box_to_wasm.