refactor type compilation

Author: flupe

src/Agda/Utils.hs

@@ -59,20 +59,8 @@ getInductiveParams Record{recPars}    = recPars
 -- TODO: consider erased things to be logical
 --       so maybe take a Dom Type instead
 
-isLogical, isArity :: Type -> TCM Bool
-
--- | Whether a type is logical.
-isLogical typ = do
-  tel <- telView typ
-  let sort = isSort $ unEl $ theCore $ tel
-  case sort of
-    Just (Univ UProp _) -> pure True
-    Just (Inf  UProp _) -> pure True
-    Just LevelUniv      -> pure True
-    Just SizeUniv       -> pure True
-    _                   -> pure False
-
 -- | Whether a type is an arity.
+isArity :: Type -> TCM Bool
 isArity typ = do
   tel <- telView typ
   pure $ isJust $ isSort $ unEl $ theCore $ tel

src/Agda2Lambox/Compile.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE NamedFieldPuns, DataKinds, OverloadedStrings #-}
+{-# LANGUAGE NamedFieldPuns, DataKinds, OverloadedStrings, NondecreasingIndentation #-}
 module Agda2Lambox.Compile 
   ( compile
   ) where
@@ -8,10 +8,11 @@ import Data.IORef
 
 import Agda.Compiler.Backend
 import Agda.Syntax.Internal ( QName )
+import Agda.Syntax.Common (Arg(..))
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.TypeChecking.Monad ( liftTCM, getConstInfo )
 import Agda.TypeChecking.Pretty
-import Agda.Utils.Monad ( whenM )
+import Agda.Utils.Monad ( whenM, ifM )
 
 import Agda.Utils ( hasPragma, isDataOrRecDef, treeless )
 
@@ -35,25 +36,29 @@ compile t qs = GlobalEnv <$> compileLoop (compileDefinition t) qs
 compileDefinition :: Target t -> Definition -> CompileM (Maybe (KerName, GlobalDecl t))
 compileDefinition target defn@Defn{..} = setCurrentRange defName do
   reportSDoc "agda2lambox.compile" 1 $ "Compiling definition: " <+> prettyTCM defName
-  fmap (qnameToKerName defName,) <$> -- prepend kername
-    case theDef of
-      GeneralizableVar{} -> pure Nothing
 
-      Axiom{} -> do
-        typ <- whenTyped target $ compileTopLevelType defType
-        pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
+  -- we skip logical definitions altogether
+  ifM (liftTCM $ isLogical $ Arg defArgInfo defType) (pure Nothing) do
 
-      Constructor{conData} -> Nothing <$ requireDef conData
+  -- prepend kername
+  fmap (qnameToKerName defName,) <$> case theDef of
+    GeneralizableVar{} -> pure Nothing
 
-      Function{} -> compileFunction target defn
+    Axiom{} -> do
+      typ <- whenTyped target $ compileTopLevelType defType
+      pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
 
-      d | isDataOrRecDef d -> compileInductive target defn
+    Constructor{conData} -> Nothing <$ requireDef conData
 
-      Primitive{..} -> do
-        reportSDoc "agda2lambox.compile" 5 $
-          "Found primitive: " <> prettyTCM defName <> ". Compiling it as axiom."
+    Function{} -> compileFunction target defn
 
-        typ <- whenTyped target $ compileTopLevelType defType
-        pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
+    d | isDataOrRecDef d -> compileInductive target defn
 
-      _ -> genericError $ "Cannot compile: " <> prettyShow defName
+    Primitive{..} -> do
+      reportSDoc "agda2lambox.compile" 5 $
+        "Found primitive: " <> prettyTCM defName <> ". Compiling it as axiom."
+
+      typ <- whenTyped target $ compileTopLevelType defType
+      pure $ Just $ ConstantDecl $ ConstantBody typ Nothing
+
+    _ -> genericError $ "Cannot compile: " <> prettyShow defName

src/Agda2Lambox/Compile/Inductive.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE NamedFieldPuns, ImportQualifiedPost, DataKinds, OverloadedStrings #-}
+{-# LANGUAGE NamedFieldPuns, ImportQualifiedPost, DataKinds, OverloadedStrings, UnicodeSyntax #-}
 -- | Convert Agda datatypes to λ□ inductive declarations
 module Agda2Lambox.Compile.Inductive
   ( compileInductive
@@ -19,15 +19,15 @@ import Agda.TypeChecking.Monad.Base hiding (None)
 import Agda.TypeChecking.Monad.Env ( withCurrentModule )
 import Agda.TypeChecking.Datatypes ( ConstructorInfo(..), getConstructorInfo, isDatatype )
 import Agda.TypeChecking.Pretty
-import Agda.TypeChecking.Telescope (telViewUpTo, piApplyM, teleArgs, telView)
+import Agda.TypeChecking.Telescope (telViewUpTo, piApplyM, teleArgs, telView, flattenTel)
 import Agda.TypeChecking.Substitute (TelView, TelV(theTel), apply)
 import Agda.Compiler.Backend ( getConstInfo, lookupMutualBlock, reportSDoc, AddContext (addContext), constructorForm)
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Syntax.Common (Arg)
 import Agda.Syntax.Internal
 import Agda.Utils.Monad ( unlessM )
 
-import Agda.Utils ( isDataOrRecDef, isLogical, isArity )
+import Agda.Utils ( isDataOrRecDef, isArity )
 import Agda2Lambox.Compile.Target
 import Agda2Lambox.Compile.Utils
 import Agda2Lambox.Compile.Monad
@@ -86,6 +86,7 @@ data InductiveBundle = Bundle
   , indPars :: Int
   }
 
+-- | Gather the shared information for compiling inductives.
 getBundle :: Definition -> InductiveBundle
 getBundle defn@Defn{defName, defType, theDef} =
   case theDef of
@@ -104,53 +105,54 @@ getBundle defn@Defn{defName, defType, theDef} =
         , indPars = recPars
         }
 
--- TODO(flupe):
---  actually really unify the compilation of both, they do exactly the same thing
-actuallyConvertInductive :: forall t. Target t -> Definition -> CompileM (LBox.OneInductiveBody t)
+
+actuallyConvertInductive :: ∀ t. Target t -> Definition -> CompileM (LBox.OneInductiveBody t)
 actuallyConvertInductive t defn = do
   let Bundle{..} = getBundle defn
 
   params <- theTel <$> telViewUpTo indPars indType
+
   reportSDoc "agda2lambox.compile.inductive" 10 $
     "Inductive parameters:" <+> prettyTCM params
 
   let pvars :: [Arg Term] = teleArgs params
 
-  -- TODO(flupe): bind params iteratively to correctly figure out the type info
-  tyvars <- whenTyped t $ forM (toList params) \pdom -> do
-    let domType = unDom pdom
-    isParamLogical <- liftTCM $ isLogical domType
-    isParamArity   <- liftTCM $ isArity domType
-    let isParamSort = isJust $ isSort $ unEl $ domType
-    pure LBox.TypeVarInfo
-      { tvarName      = maybe LBox.Anon (LBox.Named . prettyShow) $ domName pdom
-            , tvarIsLogical = isParamLogical
-            , tvarIsArity   = isParamArity
-            , tvarIsSort    = isParamSort
-            }
-
-  ctors :: [LBox.ConstructorBody t] <-
-    forM indCons \cname -> do
-      arity <- liftTCM $ getConstructorInfo cname <&> \case
-        DataCon arity         -> arity
-        RecordCon _ _ arity _ -> arity
-
-      conTypeInfo <- whenTyped t do
-        conType <- liftTCM $ (`piApplyM` pvars) =<< defType <$> getConstInfo cname
-        conTel  <- toList . theTel <$> telView conType
-        compileArgs indPars conTel
-
-      pure LBox.Constructor
-        { cstrName  = prettyShow $ qnameName cname
-        , cstrArgs  = arity
-        , cstrTypes = conTypeInfo
+  addContext params do
+
+    tyvars <- whenTyped t $ forM (flattenTel params) \pdom -> do
+      let domType = unDom pdom
+      isParamLogical <- liftTCM $ isLogical pdom
+      isParamArity   <- liftTCM $ isArity domType
+      let isParamSort = isJust  $ isSort $ unEl $ domType
+      pure LBox.TypeVarInfo
+        { tvarName      = maybe LBox.Anon (LBox.Named . prettyShow) $ domName pdom
+        , tvarIsLogical = isParamLogical
+        , tvarIsArity   = isParamArity
+        , tvarIsSort    = isParamSort
         }
 
-  pure LBox.OneInductive
-    { indName          = prettyShow $ qnameName indName
-    , indPropositional = False        -- TODO(flupe)
-    , indKElim         = LBox.IntoAny -- TODO(flupe)
-    , indCtors         = ctors
-    , indProjs         = []
-    , indTypeVars      = tyvars
-    }
+    ctors :: [LBox.ConstructorBody t] <-
+      forM indCons \cname -> do
+        arity <- liftTCM $ getConstructorInfo cname <&> \case
+          DataCon arity         -> arity
+          RecordCon _ _ arity _ -> arity
+
+        conTypeInfo <- whenTyped t do
+          conType <- liftTCM $ (`piApplyM` pvars) =<< defType <$> getConstInfo cname
+          conTel  <- toList . theTel <$> telView conType
+          compileArgs indPars conTel
+
+        pure LBox.Constructor
+          { cstrName  = prettyShow $ qnameName cname
+          , cstrArgs  = arity
+          , cstrTypes = conTypeInfo
+          }
+
+    pure LBox.OneInductive
+      { indName          = prettyShow $ qnameName indName
+      , indPropositional = False        -- TODO(flupe)
+      , indKElim         = LBox.IntoAny -- TODO(flupe)
+      , indCtors         = ctors
+      , indProjs         = []
+      , indTypeVars      = tyvars
+      }