WIP: Add typechecker

Makefile

@@ -1,10 +1,12 @@
+AGDA2LAMBOX_BIN ?= agda2lambox
+
 .PHONY: default
 
 default:
 	cabal install --overwrite-policy=always
 
 %.ast:
-	agda2lambox -o build test/$*.agda
+	$(AGDA2LAMBOX_BIN) -o build test/$*.agda
 
 %.wasm: %.ast
 	lbox wasm -o demo/$@ build/$*.ast
@@ -16,7 +18,7 @@ default:
 	lbox rust -o demo/$@ build/$*.ast
 
 %.v:
-	agda2lambox -o build --rocq test/$*.agda
+	$(AGDA2LAMBOX_BIN) -o build --rocq test/$*.agda
 
 %.typed:
-	agda2lambox -o build --typed --no-blocks test/$*.agda
+	$(AGDA2LAMBOX_BIN) -o build --typed --no-blocks test/$*.agda

agda2lambox.cabal

@@ -36,6 +36,7 @@ executable agda2lambox
                        LambdaBox.Type,
                        LambdaBox.Env,
                        LambdaBox,
+                       LambdaBox.Typecheck,
                        CoqGen,
                        SExpr,
                        Paths_agda2lambox

src/Agda2Lambox/Compile.hs

@@ -7,6 +7,7 @@ import Control.Monad.IO.Class ( liftIO )
 import Data.IORef
 
 import Control.Monad.State
+import Data.Bifunctor (bimap)
 
 import Agda.Compiler.Backend
 import Agda.Syntax.Internal ( QName )
@@ -28,56 +29,55 @@ import Agda2Lambox.Compile.Inductive  ( compileInductive )
 import Agda2Lambox.Compile.TypeScheme ( compileTypeScheme )
 import Agda2Lambox.Compile.Type       ( compileTopLevelType )
 
-import LambdaBox ( emptyName, emptyDecl )
+import LambdaBox ( emptyGlobalDecl )
 import LambdaBox.Names
-import LambdaBox.Env (GlobalEnv(..), GlobalDecl(..), ConstantBody(..))
+import LambdaBox.Env (GlobalEnv(..), GlobalDecl(..), GlobalTermDecl(..), GlobalTypeDecl(..), ConstantBody(..))
 import LambdaBox.Term (Term(LBox))
 
 
 
 -- | Compile the given names into to a λ□ environment.
-compile :: Target t -> [QName] -> CompileM (GlobalEnv t)
-compile t qs = do
-  items <- compileLoop (compileDefinition t) qs
-  pure $ GlobalEnv $ map itemToEntry items ++ [(emptyName, emptyDecl t)]
+compile :: [QName] -> CompileM (GlobalEnv Typed)
+compile qs = do
+  items <- compileLoop compileDefinition qs
+  pure $ GlobalEnv $ map itemToEntry items ++ [emptyGlobalDecl]
   where
-    itemToEntry :: CompiledItem (GlobalDecl t) -> (KerName, GlobalDecl t)
-    itemToEntry CompiledItem{..} = (qnameToKName itemName, itemValue)
-
-
-compileDefinition :: Target t -> Definition -> CompileM (Maybe (GlobalDecl t))
-compileDefinition target defn@Defn{..} = setCurrentRange defName do
+    itemToEntry :: CompiledItem (Either (GlobalTermDecl Typed) (GlobalTypeDecl Typed))
+                    -> GlobalDecl Typed
+    itemToEntry CompiledItem{..} = case itemValue of
+      Left d -> GlobalTermDecl (qnameToKName itemName, d)
+      Right d -> GlobalTypeDecl (Some (qnameToKName itemName, d))
+
+compileDefinition :: Definition -> CompileM (Maybe (Either (GlobalTermDecl Typed) (GlobalTypeDecl Typed)))
+compileDefinition defn@Defn{..} = setCurrentRange defName do
   reportSDoc "agda2lambox.compile" 1 $ "Compiling definition: " <+> prettyTCM defName
 
   -- we skip definitions introduced by module application
 
   if defCopy then pure Nothing else do
 
-  typ <- whenTyped target $ compileTopLevelType defType
+  typ <- Some <$> compileTopLevelType defType
 
   -- logical definitions are immediately compiled to □
   ifM (liftTCM $ isLogical $ Arg defArgInfo defType)
-     (pure $ Just $ ConstantDecl $ ConstantBody typ $ Just LBox) do
+     (pure $ Just . Left $ ConstantDecl $ ConstantBody typ $ Just LBox) do
 
   case theDef of
     PrimitiveSort{}    -> pure Nothing
     GeneralizableVar{} -> pure Nothing
 
     Axiom{} -> do
-      typ <- whenTyped target $ compileTopLevelType defType
-      pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
+      typ <- Some <$> compileTopLevelType defType
+      pure $ Just . Left $ ConstantDecl $ ConstantBody typ Nothing
 
     Constructor{conData} -> Nothing <$ requireDef conData
 
     Function{} -> do
-      ifNotM (liftTCM $ isArity defType) (compileFunction target defn) do
-        -- it's a type scheme
-        case target of
-          ToUntyped -> pure Nothing
-          -- we only compile it with --typed
-          ToTyped   -> Just <$> compileTypeScheme defn
+      ifNotM (liftTCM $ isArity defType)
+        ((Left <$>) <$> compileFunction defn)
+        ((Right <$>) <$> Just <$> compileTypeScheme defn)
 
-    d | isDataOrRecDef d -> compileInductive target defn
+    d | isDataOrRecDef d -> (Left <$>) <$> compileInductive defn
 
     Primitive{..} -> do
       reportSDoc "agda2lambox.compile" 5 $
@@ -113,12 +113,12 @@ compileDefinition target defn@Defn{..} = setCurrentRange defName do
           liftTCM $ modifyGlobalDefinition defName $ const defn'
 
           -- and then we compile it as a regular function
-          compileFunction target defn'
+          (Left <$>) <$> compileFunction defn'
 
         -- otherwise, compiling it as an axiom
         _ -> do
           reportSDoc "agda2lambox.compile" 5 $ "Compiling it to an axiom."
-          typ <- whenTyped target $ compileTopLevelType defType
-          pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
+          typ <- Some <$> compileTopLevelType defType
+          pure $ Just . Left $ ConstantDecl $ ConstantBody typ Nothing
 
     _ -> genericError $ "Cannot compile: " <> prettyShow defName

src/Agda2Lambox/Compile/Function.hs

@@ -40,7 +40,7 @@ isFunction _ = False
 
 
 -- | Convert a function body to a Lambdabox term.
-compileFunctionBody :: [QName] -> Definition -> CompileM LBox.Term
+compileFunctionBody :: [QName] -> Definition -> CompileM (LBox.Term Typed)
 compileFunctionBody ms Defn{defName, theDef} = do
   Just t <- liftTCM $ treeless defName
 
@@ -59,9 +59,9 @@ shouldCompileFunction def@Defn{theDef} | Function{..} <- theDef
     && hasQuantityω def       -- non-erased
 
 -- | Convert a function definition to a λ□ declaration.
-compileFunction :: Target t -> Definition -> CompileM (Maybe (LBox.GlobalDecl t))
-compileFunction t defn | not (shouldCompileFunction defn) = pure Nothing
-compileFunction (t :: Target t) defn@Defn{defType} = do
+compileFunction :: Definition -> CompileM (Maybe (LBox.GlobalTermDecl Typed))
+compileFunction defn | not (shouldCompileFunction defn) = pure Nothing
+compileFunction defn@Defn{defType} = do
   let fundef@Function{funMutual = Just mutuals} = theDef defn
 
   reportSDoc "agda2lambox.compile.function" 5 $
@@ -78,7 +78,7 @@ compileFunction (t :: Target t) defn@Defn{defType} = do
   let mnames = map defName mdefs
 
   -- (conditionally) compile type of function
-  typ <- whenTyped t $ case isRecordProjection fundef of
+  typ <- case isRecordProjection fundef of
     Nothing -> compileTopLevelType defType
 
     -- if it is a (real) projection, drop the parameters from the type
@@ -94,8 +94,8 @@ compileFunction (t :: Target t) defn@Defn{defType} = do
     --                they should be eta-expanded somehow,
     --                OR treated like projections
 
-  let builder :: LBox.Term -> Maybe (LBox.GlobalDecl t)
-      builder = Just . ConstantDecl . ConstantBody typ . Just
+  let builder :: LBox.Term Typed -> Maybe (LBox.GlobalTermDecl Typed)
+      builder = Just . ConstantDecl . ConstantBody (Some typ) . Just
 
   -- if the function is not recursive, just compile the body
   if null mdefs then builder <$> compileFunctionBody [] defn
@@ -108,7 +108,7 @@ compileFunction (t :: Target t) defn@Defn{defType} = do
       forM mdefs \def@Defn{defName} -> do
         body <- compileFunctionBody mnames def >>= \case
           l@LBox.LLambda{} -> pure l
-          LBox.LBox        -> pure $ LBox.LLambda LBox.Anon LBox.LBox
+          LBox.LBox        -> pure $ LBox.LLambda LBox.Anon (Some LBox.TBox) LBox.LBox
           _                -> genericError "Fixpoint body must be Lambda."
         return LBox.Def
           { dName = qnameToName defName

src/Agda2Lambox/Compile/Inductive.hs

@@ -35,8 +35,8 @@ import Agda2Lambox.Compile.Type
 import LambdaBox qualified as LBox
 
 -- | Toplevel conversion from a datatype/record definition to a Lambdabox declaration.
-compileInductive :: Target t -> Definition -> CompileM (Maybe (LBox.GlobalDecl t))
-compileInductive t defn@Defn{defName} = do
+compileInductive :: Definition -> CompileM (Maybe (LBox.GlobalTermDecl Typed))
+compileInductive defn@Defn{defName} = do
   mutuals <- liftTCM $ dataOrRecDefMutuals defn
 
   reportSDoc "agda2lambox.compile.inductive" 5 $
@@ -70,7 +70,7 @@ compileInductive t defn@Defn{defName} = do
     unless (all (isDataOrRecDef . theDef) defs) $
       genericError "Mutually-defined datatypes/records *and* functions not supported."
 
-    bodies <- forM defs $ actuallyConvertInductive t
+    bodies <- forM defs $ actuallyConvertInductive
 
     return $ Just $ LBox.InductiveDecl $ LBox.MutualInductive
       { indFinite = LBox.Finite -- TODO(flupe)
@@ -106,8 +106,8 @@ getBundle defn@Defn{defName, defType, theDef} =
         }
 
 
-actuallyConvertInductive :: ∀ t. Target t -> Definition -> CompileM (LBox.OneInductiveBody t)
-actuallyConvertInductive t defn = do
+actuallyConvertInductive :: Definition -> CompileM (LBox.OneInductiveBody Typed)
+actuallyConvertInductive defn = do
   let Bundle{..} = getBundle defn
 
   params <- theTel <$> telViewUpTo indPars indType
@@ -119,7 +119,7 @@ actuallyConvertInductive t defn = do
 
   addContext params do
 
-    tyvars <- whenTyped t $ forM (flattenTel params) \pdom -> do
+    tyvars <- forM (flattenTel params) \pdom -> do
       let domType = unDom pdom
       isParamLogical <- liftTCM $ isLogical pdom
       isParamArity   <- liftTCM $ isArity domType
@@ -137,15 +137,15 @@ actuallyConvertInductive t defn = do
           DataCon arity         -> arity
           RecordCon _ _ arity _ -> arity
 
-        conTypeInfo <- whenTyped t do
-          conType <- liftTCM $ (`piApplyM` pvars) . defType =<< getConstInfo cname
+        conTypeInfo <- do
+          conType <- liftTCM $ (`piApplyM` pvars) =<< defType <$> (getConstInfo cname)
           conTel  <- toList . theTel <$> telView conType
           compileArgs indPars conTel
 
         pure LBox.Constructor
           { cstrName  = qnameToIdent cname
           , cstrArgs  = arity
-          , cstrTypes = conTypeInfo
+          , cstrTypes = Some conTypeInfo
           }
 
     pure LBox.OneInductive
@@ -154,5 +154,5 @@ actuallyConvertInductive t defn = do
       , indKElim         = LBox.IntoAny -- TODO(flupe)
       , indCtors         = ctors
       , indProjs         = []
-      , indTypeVars      = tyvars
+      , indTypeVars      = Some tyvars
       }

src/Agda2Lambox/Compile/Target.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE DataKinds, GADTs, FlexibleInstances #-}
 -- | Compile targets for the backend
-module Agda2Lambox.Compile.Target 
+module Agda2Lambox.Compile.Target
   ( Typing(..)
   , Target(..)
   , WhenTyped(..)
@@ -9,6 +9,7 @@ module Agda2Lambox.Compile.Target
   , getUntyped
   , whenTyped
   , whenUntyped
+  , TypeErasure(..)
   ) where
 
 import Data.Foldable (Foldable(foldMap))
@@ -43,7 +44,6 @@ instance Foldable (WhenTyped t) where
   foldMap f None     = mempty
   foldMap f (Some x) = f x
 
--- | Type wrapper that contains a value iff we're in the untyped setting.
 data WhenUntyped (t :: Typing) (a :: Type) :: Type where
   NoneU ::      WhenUntyped Typed a
   SomeU :: a -> WhenUntyped Untyped   a
@@ -85,3 +85,6 @@ whenUntyped ToUntyped x = SomeU <$> x
 instance NFData (Target t) where
   rnf ToTyped   = ()
   rnf ToUntyped = ()
+
+class TypeErasure t where
+  erase :: t Typed -> t Untyped