Add initial treeless -> lambdabox translation

src/Agda/Lib.hs

@@ -46,6 +46,7 @@ import Agda.Syntax.Common
   ( Arg, unArg, defaultArg, defaultArgInfo
   , ArgInfo
   , ArgName, bareNameWithDefault
+  , Erased(..)
   , LensQuantity(..), hasQuantity0
   , LensHiding(..), visible
   , MetaId(..), NameId(NameId)

src/Agda2Lambox/Convert/Terms.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE LambdaCase, FlexibleInstances #-}
 module Agda2Lambox.Convert.Terms () where
 
 import Utils
@@ -15,8 +16,45 @@ import Agda2Lambox.Convert.Class
 -- import Agda2Lambox.Convert.Builtins
 -- import Agda2Lambox.Convert.Types
 
+fixme :: L.Name
+fixme = L.Named "FIXME"
+
 -- | Compiling (treeless) Agda terms into Lambox expressions.
 instance A.TTerm ~> L.Term where
-  go t = do
-   report $ "* compiling tterm: " <> pp t
-   return L.Box
+  go = \case
+    A.TVar n -> return $ L.BVar n -- Can variables be erased?
+    A.TPrim tp -> return $ L.Const (show tp) -- FIXME
+    A.TDef qn -> return $ L.FVar (A.prettyShow qn)
+    A.TApp t args -> do
+      ct <- go t
+      cargs <- mapM go args
+      return $ foldl L.App ct cargs
+    A.TLam tt -> L.Lam L.Anon <$> go tt -- FIXME
+    A.TLit l -> return $ L.Const (show l) -- FIXME: How are literals (eg. the numeral 10) represented in λ□?
+    A.TCon qn -> return $ L.Ctor (L.Inductive $ A.prettyShow qn) 99 -- FIXME
+    A.TLet tt tu -> L.Let L.Anon <$> go tt <*> (go tu) -- FIXME: name
+    A.TCase n A.CaseInfo{..} tt talts ->
+      case caseErased of
+        A.Erased _ -> fail ""
+        A.NotErased _ -> do
+          calts <- traverse go talts
+          cind <- go caseType
+          return $ L.Case cind 0 (L.BVar n) calts
+
+    A.TUnit -> return L.Box
+    A.TSort -> return L.Box
+    A.TErased -> return L.Box
+    A.TCoerce tt -> fail "TCoerce"
+    A.TError terr -> fail "TError"
+
+instance A.TAlt ~> (Int, L.Term) where
+  go = \case
+    A.TACon{..} -> (aArity,) <$> go aBody
+    A.TALit{..} -> (0,) <$> go aBody
+    A.TAGuard{..} -> fail "TAGuard"
+
+instance A.CaseType ~> L.Inductive where
+  go = \case
+    A.CTData qn -> return $ L.Inductive (A.prettyShow qn)
+    A.CTNat -> return $ L.Inductive "Nat"
+    _ -> fail ""

src/Agda2Lambox/Monad.hs

@@ -6,22 +6,7 @@ import Control.Monad.State ( StateT, runStateT )
 import Agda ( TCM )
 
 -- | TCM monad extended with a custom environment and state.
-type C = StateT State (ReaderT Env TCM)
+type C = TCM
 
-runC :: State -> C a -> TCM (a, State)
-runC s0 k = runReaderT (runStateT k s0) initEnv
-
-runC0 :: C a -> TCM (a, State)
-runC0 = runC initState
-
--- | Environment tracking which part of a definition we are currently compiling.
-data Env = Env {}
-
-initEnv :: Env
-initEnv = Env {}
-
--- | Compilation state.
-data State = State {}
-
-initState :: State
-initState = State {}
+runC0 :: C a -> TCM a
+runC0 = id

src/Main.hs

@@ -34,11 +34,14 @@ type ModuleEnv   = ()
 type ModuleRes   = ()
 data CompiledDef' = CompiledDef
   { name :: QName
-  , term :: L.Term
+  , tterm :: TTerm
+  , lterm :: L.Term
   }
 
 instance Show CompiledDef' where
-  show CompiledDef{..} = prettyShow (qnameName name) <> " = " <> show term
+  show CompiledDef{..} =
+    unlines [ prettyShow (qnameName name) <> " = " <> prettyShow tterm
+            , prettyShow (qnameName name) <> " = " <> show lterm ]
 
 type CompiledDef = Maybe CompiledDef'
 
@@ -75,7 +78,7 @@ compile opts tlm _ Defn{..}
       Nothing -> return Nothing
       Just (CompilerPragma _ _) -> do
         Just tterm <- toTreeless EagerEvaluation defName
-        Just . (CompiledDef defName) . fst <$> runC0 (convert tterm)
+        Just . (CompiledDef defName tterm) <$> runC0 (convert tterm)
 
 writeModule :: Options -> ModuleEnv -> IsMain -> TopLevelModuleName
             -> [CompiledDef]