Add (bare) typechecker

Author: carlostome

agda2lambox.cabal

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

src/LambdaBox/Names.hs

@@ -19,12 +19,14 @@ data ModPath
     -- ^ parameters of functors
   | MPDot ModPath Ident
     -- ^ submodules
+  deriving (Eq)
 
 -- | Absolute name of objects in the Rocq kernel.
 data KerName = KerName
   { kerModPath :: ModPath
   , kerName    :: Ident
   }
+  deriving (Eq)
 
 -- | Reference to an inductive datatype.
 data Inductive = Inductive
@@ -33,6 +35,7 @@ data Inductive = Inductive
   , indInd  :: Int
     -- ^ Which of those is the inductive we care about.
   }
+  deriving (Eq)
 
 -- | Names used in binders
 data Name = Anon | Named Ident

src/LambdaBox/Type.hs

@@ -15,6 +15,7 @@ data Type
       --   Uses De Bruijn *levels* and NOT indices.
   | TInd Inductive
   | TConst KerName
+  deriving (Eq)
 
 instance Pretty Type where
   prettyPrec p = \case

src/LambdaBox/Typecheck.hs

@@ -0,0 +1,56 @@
+{-# LANGUAGE DataKinds #-}
+module LambdaBox.Typecheck where
+
+import Agda2Lambox.Compile.Target
+import LambdaBox
+import Agda.Utils.Monad
+
+type Env = Int -> Type
+
+extend :: Env -> Type -> Env
+extend env ty 0 = ty
+extend env ty i = env (i - 1)
+
+-- | Infer the type of a term
+infer :: MonadFail m => Term Typed -> Env -> m Type
+infer term env =
+  case term of
+    LBox -> return TBox
+    LRel n -> return $ env n
+    LLambda n (Some ty) b ->
+      infer b (extend env ty)
+    LLetIn n t b -> do
+      ty <- infer t env
+      ty' <- infer b (extend env ty)
+      return (TArr ty ty')
+    LApp t t' -> do
+      TArr t1 t2 <- infer t env
+      ifM (check t' t1 env)
+        (return t2)
+        (fail "Failure")
+    LConst kn -> fail "Not implemented" -- FIXME
+    LConstruct ind i ts -> fail "Not implemented" -- FIXME
+    LCase ind n t bs -> fail "Not implemented" -- FIXME
+    LFix mfix i -> fail "Not implemented" -- FIXME
+
+-- | Check a term against a type
+check :: MonadFail m => Term Typed -> Type -> Env -> m Bool
+check term ty env = case term of
+  LBox -> return $ TBox == ty
+  LRel n -> return $ env n == ty
+  LLambda n (Some ty) b -> case ty of
+    TArr t1 t2 -> check b t2 (extend env t1)
+    _ -> return False
+  LLetIn n t b -> do
+    ty' <- infer t env
+    check b ty (extend env ty')
+  LApp t t' -> do
+    TArr t1 t2 <- infer t env
+    check t' t1 env
+  LConst c -> return False
+  LConstruct ind n ts -> return False
+  LCase ind i t bs -> return False
+  LFix mfix i -> return False
+
+typecheck :: GlobalEnv Typed -> Bool
+typecheck _ = False

src/Main.hs

@@ -35,6 +35,7 @@ import CoqGen    ( prettyCoq  )
 import SExpr     ( prettySexp )
 import LambdaBox.Env
 import LambdaBox.Names (KerName)
+import LambdaBox.Typecheck (typecheck)
 import Agda2Lambox.Compile.Monad (runCompile, CompileEnv(..))
 
 
@@ -48,12 +49,13 @@ data Output = RocqOutput | AstOutput
 data Options = forall t. Options
   { optOutDir   :: Maybe FilePath
   , optTarget   :: Target t
+  , optWithTC   :: Bool
   , optOutput   :: Output
   , optNoBlocks :: Bool
   }
 
 instance NFData Options where
-  rnf (Options m t o nb) = rnf m `seq` rnf t `seq` rnf o `seq` rnf nb
+  rnf (Options m t tc o nb) = rnf m `seq` rnf t `seq` rnf tc `seq` rnf o `seq` rnf nb
 
 -- | Setter for output directory option.
 outdirOpt :: Monad m => FilePath -> Options -> m Options
@@ -68,11 +70,15 @@ rocqOpt opts = return opts { optOutput = RocqOutput }
 noBlocksOpt :: Monad m => Options -> m Options
 noBlocksOpt opts = return opts { optNoBlocks = True }
 
+withTC :: Monad m => Options -> m Options
+withTC opts = return opts { optWithTC = True }
+
 -- | Default backend options.
 defaultOptions :: Options
 defaultOptions  = Options
   { optOutDir   = Nothing
   , optTarget   = ToUntyped
+  , optWithTC   = False
   , optOutput   = AstOutput
   , optNoBlocks = False
   }
@@ -97,6 +103,8 @@ agda2lambox = Backend backend
             "Write output files to DIR. (default: project root)"
           , Option ['t'] ["typed"] (NoArg typedOpt)
             "Compile to typed λ□ environments."
+          , Option "tc" ["typecheck"] (NoArg typedOpt)
+            "Typecheck output λ□."
           , Option ['c'] ["rocq"] (NoArg rocqOpt)
             "Output a Rocq file."
           , Option [] ["no-blocks"] (NoArg noBlocksOpt)
@@ -134,6 +142,11 @@ writeModule Options{..} menv IsMain m defs = do
   mains    <- getMain optTarget programs
   env      <- runCompile (CompileEnv optNoBlocks) $ compile defs
 
+  liftIO $ putStrLn $ "Typechecking generated λ□."
+  if (typecheck env)
+    then genericError "Failure"
+    else liftIO $ putStrLn "Success"
+
   liftIO $ createDirectoryIfMissing True outDir
 
   let fileName = outDir </> prettyShow m