Direct translation from MicroJuvix to MiniC (#1386)

app/Main.hs

@@ -25,8 +25,8 @@ import Juvix.Syntax.MiniHaskell.Pretty qualified as MiniHaskell
 import Juvix.Syntax.MonoJuvix.Pretty qualified as Mono
 import Juvix.Termination qualified as Termination
 import Juvix.Translation.AbstractToMicroJuvix qualified as Micro
+import Juvix.Translation.MicroJuvixToMiniC qualified as MiniC
 import Juvix.Translation.MicroJuvixToMonoJuvix qualified as Mono
-import Juvix.Translation.MonoJuvixToMiniC qualified as MiniC
 import Juvix.Translation.MonoJuvixToMiniHaskell qualified as MiniHaskell
 import Juvix.Translation.ScopedToAbstract qualified as Abstract
 import Juvix.Utils.Version (runDisplayVersion)

src/Juvix/Pipeline.hs

@@ -17,8 +17,8 @@ import Juvix.Syntax.MicroJuvix.MicroJuvixResult qualified as MicroJuvix
 import Juvix.Syntax.MicroJuvix.MicroJuvixTypedResult qualified as MicroJuvix
 import Juvix.Syntax.MicroJuvix.TypeChecker qualified as MicroJuvix
 import Juvix.Translation.AbstractToMicroJuvix qualified as MicroJuvix
+import Juvix.Translation.MicroJuvixToMiniC qualified as MiniC
 import Juvix.Translation.MicroJuvixToMonoJuvix qualified as MonoJuvix
-import Juvix.Translation.MonoJuvixToMiniC qualified as MiniC
 import Juvix.Translation.MonoJuvixToMiniHaskell qualified as MiniHaskell
 import Juvix.Translation.ScopedToAbstract qualified as Abstract
 
@@ -95,7 +95,7 @@ upToMiniC ::
   Members '[Files, NameIdGen, Builtins, Error JuvixError] r =>
   EntryPoint ->
   Sem r MiniC.MiniCResult
-upToMiniC = upToMonoJuvix >=> pipelineMiniC
+upToMiniC = upToMicroJuvixTyped >=> pipelineMiniC
 
 --------------------------------------------------------------------------------
 
@@ -149,6 +149,6 @@ pipelineMiniHaskell = MiniHaskell.entryMiniHaskell
 
 pipelineMiniC ::
   Member Builtins r =>
-  MonoJuvix.MonoJuvixResult ->
+  MicroJuvix.MicroJuvixTypedResult ->
   Sem r MiniC.MiniCResult
 pipelineMiniC = MiniC.entryMiniC

src/Juvix/Syntax/MicroJuvix/InfoTable.hs

@@ -7,15 +7,17 @@ import Juvix.Syntax.MicroJuvix.Language.Extra
 data ConstructorInfo = ConstructorInfo
   { _constructorInfoInductiveParameters :: [InductiveParameter],
     _constructorInfoArgs :: [Expression],
-    _constructorInfoInductive :: InductiveName
+    _constructorInfoInductive :: InductiveName,
+    _constructorInfoBuiltin :: Maybe BuiltinConstructor
   }
 
 newtype FunctionInfo = FunctionInfo
   { _functionInfoDef :: FunctionDef
   }
 
-newtype AxiomInfo = AxiomInfo
-  { _axiomInfoType :: Expression
+data AxiomInfo = AxiomInfo
+  { _axiomInfoType :: Expression,
+    _axiomInfoBuiltin :: Maybe BuiltinAxiom
   }
 
 newtype InductiveInfo = InductiveInfo
@@ -71,11 +73,13 @@ buildTable1 m = InfoTable {..} <> buildTable (map (^. includeModule) includes)
     _infoConstructors :: HashMap Name ConstructorInfo
     _infoConstructors =
       HashMap.fromList
-        [ (c ^. constructorName, ConstructorInfo params args ind)
+        [ (c ^. constructorName, ConstructorInfo params args ind builtin)
           | StatementInductive d <- ss,
             let ind = d ^. inductiveName,
+            let n = length (d ^. inductiveConstructors),
             let params = d ^. inductiveParameters,
-            c <- d ^. inductiveConstructors,
+            let builtins = maybe (replicate n Nothing) (map Just . builtinConstructors) (d ^. inductiveBuiltin),
+            (builtin, c) <- zipExact builtins (d ^. inductiveConstructors),
             let args = c ^. constructorParameters
         ]
     _infoFunctions :: HashMap Name FunctionInfo
@@ -87,7 +91,7 @@ buildTable1 m = InfoTable {..} <> buildTable (map (^. includeModule) includes)
     _infoAxioms :: HashMap Name AxiomInfo
     _infoAxioms =
       HashMap.fromList
-        [ (d ^. axiomName, AxiomInfo (d ^. axiomType))
+        [ (d ^. axiomName, AxiomInfo (d ^. axiomType) (d ^. axiomBuiltin))
           | StatementAxiom d <- ss
         ]
     ss = m ^. (moduleBody . moduleStatements)

src/Juvix/Syntax/MicroJuvix/Language.hs

@@ -69,6 +69,14 @@ data Iden
   | IdenInductive Name
   deriving stock (Eq, Generic)
 
+getName :: Iden -> Name
+getName = \case
+  IdenFunction n -> n
+  IdenConstructor n -> n
+  IdenVar n -> n
+  IdenAxiom n -> n
+  IdenInductive n -> n
+
 instance Hashable Iden
 
 data TypedExpression = TypedExpression

src/Juvix/Syntax/MicroJuvix/Language/Extra.hs

@@ -113,6 +113,44 @@ mkConcreteType = fmap ConcreteType . go
       e' <- go e
       return (FunctionParameter m i e')
 
+newtype PolyType = PolyType {_unpolyType :: Expression}
+  deriving stock (Eq, Generic)
+
+instance Hashable PolyType
+
+makeLenses ''PolyType
+
+mkPolyType' :: Expression -> PolyType
+mkPolyType' =
+  fromMaybe (error "the given type contains holes")
+    . mkPolyType
+
+-- mkPolyType removes all named function parameters; currently the assumption in
+-- MicroJuvixToMiniC.hs is that these coincide with type parameters
+mkPolyType :: Expression -> Maybe PolyType
+mkPolyType = fmap PolyType . go
+  where
+    go :: Expression -> Maybe Expression
+    go t = case t of
+      ExpressionApplication (Application l r i) -> do
+        l' <- go l
+        r' <- go r
+        return (ExpressionApplication (Application l' r' i))
+      ExpressionUniverse {} -> return t
+      ExpressionFunction (Function (FunctionParameter m i e) r)
+        | isNothing m -> do
+            e' <- go e
+            r' <- go r
+            return (ExpressionFunction (Function (FunctionParameter m i e') r'))
+        | otherwise -> go r
+      ExpressionHole {} -> Nothing
+      ExpressionLiteral {} -> return t
+      ExpressionIden IdenFunction {} -> return t
+      ExpressionIden IdenInductive {} -> return t
+      ExpressionIden IdenConstructor {} -> return t
+      ExpressionIden IdenAxiom {} -> return t
+      ExpressionIden IdenVar {} -> return t
+
 class HasExpressions a where
   leafExpressions :: Traversal' a Expression
 

src/Juvix/Syntax/MicroJuvix/MicroJuvixTypedResult.hs

@@ -9,9 +9,12 @@ import Juvix.Syntax.MicroJuvix.InfoTable
 import Juvix.Syntax.MicroJuvix.Language
 import Juvix.Syntax.MicroJuvix.MicroJuvixArityResult (MicroJuvixArityResult)
 
+type TypesTable = HashMap Name Expression
+
 data MicroJuvixTypedResult = MicroJuvixTypedResult
   { _resultMicroJuvixArityResult :: MicroJuvixArityResult,
-    _resultModules :: NonEmpty Module
+    _resultModules :: NonEmpty Module,
+    _resultIdenTypes :: TypesTable
   }
 
 makeLenses ''MicroJuvixTypedResult

src/Juvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -16,23 +16,32 @@ import Juvix.Syntax.MicroJuvix.MicroJuvixArityResult
 import Juvix.Syntax.MicroJuvix.MicroJuvixTypedResult
 import Juvix.Syntax.MicroJuvix.TypeChecker.Inference
 
+addIdens :: Member (State TypesTable) r => TypesTable -> Sem r ()
+addIdens idens = modify (HashMap.union idens)
+
+registerConstructor :: Members '[State TypesTable, Reader InfoTable] r => InductiveConstructorDef -> Sem r ()
+registerConstructor ctr = do
+  ty <- constructorType (ctr ^. constructorName)
+  modify (HashMap.insert (ctr ^. constructorName) ty)
+
 entryMicroJuvixTyped ::
   Members '[Error TypeCheckerError, NameIdGen] r =>
   MicroJuvixArityResult ->
   Sem r MicroJuvixTypedResult
 entryMicroJuvixTyped res@MicroJuvixArityResult {..} = do
-  r <- runReader table (mapM checkModule _resultModules)
+  (idens, r) <- runState (mempty :: TypesTable) (runReader table (mapM checkModule _resultModules))
   return
     MicroJuvixTypedResult
       { _resultMicroJuvixArityResult = res,
-        _resultModules = r
+        _resultModules = r,
+        _resultIdenTypes = idens
       }
   where
     table :: InfoTable
     table = buildTable _resultModules
 
 checkModule ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   Module ->
   Sem r Module
 checkModule Module {..} = do
@@ -44,7 +53,7 @@ checkModule Module {..} = do
       }
 
 checkModuleBody ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   ModuleBody ->
   Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -55,35 +64,45 @@ checkModuleBody ModuleBody {..} = do
       }
 
 checkInclude ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   Include ->
   Sem r Include
 checkInclude = traverseOf includeModule checkModule
 
 checkStatement ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   Statement ->
   Sem r Statement
 checkStatement s = case s of
   StatementFunction fun -> StatementFunction <$> checkFunctionDef fun
   StatementForeign {} -> return s
-  StatementInductive {} -> return s
+  StatementInductive ind -> do
+    mapM_ registerConstructor (ind ^. inductiveConstructors)
+    ty <- inductiveType (ind ^. inductiveName)
+    modify (HashMap.insert (ind ^. inductiveName) ty)
+    return s
   StatementInclude i -> StatementInclude <$> checkInclude i
-  StatementAxiom {} -> return s
+  StatementAxiom ax -> do
+    modify (HashMap.insert (ax ^. axiomName) (ax ^. axiomType))
+    return s
 
 checkFunctionDef ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   FunctionDef ->
   Sem r FunctionDef
-checkFunctionDef FunctionDef {..} = runInferenceDef $ do
-  info <- lookupFunction _funDefName
-  checkFunctionDefType _funDefType
-  _funDefClauses' <- mapM (checkFunctionClause info) _funDefClauses
-  return
-    FunctionDef
-      { _funDefClauses = _funDefClauses',
-        ..
-      }
+checkFunctionDef FunctionDef {..} = do
+  (funDef, idens) <- runInferenceDef $ do
+    info <- lookupFunction _funDefName
+    checkFunctionDefType _funDefType
+    registerIden _funDefName _funDefType
+    _funDefClauses' <- mapM (checkFunctionClause info) _funDefClauses
+    return
+      FunctionDef
+        { _funDefClauses = _funDefClauses',
+          ..
+        }
+  addIdens idens
+  return funDef
 
 checkFunctionDefType :: forall r. Members '[Inference] r => Expression -> Sem r ()
 checkFunctionDefType = traverseOf_ (leafExpressions . _ExpressionHole) go
@@ -203,6 +222,7 @@ checkPattern funName = go
         PatternBraces {} -> impossible
         PatternVariable v -> do
           modify (addType v ty)
+          registerIden v ty
           case argTy ^. paramName of
             Just v' -> do
               modify (over localTyMap (HashMap.insert v' v))

src/Juvix/Syntax/MicroJuvix/TypeChecker/Inference.hs

@@ -4,6 +4,7 @@ import Data.HashMap.Strict qualified as HashMap
 import Juvix.Prelude hiding (fromEither)
 import Juvix.Syntax.MicroJuvix.Error
 import Juvix.Syntax.MicroJuvix.Language.Extra
+import Juvix.Syntax.MicroJuvix.MicroJuvixTypedResult
 
 data MetavarState
   = Fresh
@@ -21,21 +22,32 @@ data Inference m a where
   MatchTypes :: Expression -> Expression -> Inference m (Maybe MatchError)
   QueryMetavar :: Hole -> Inference m (Maybe Expression)
   NormalizeType :: Expression -> Inference m Expression
+  RegisterIden :: Name -> Expression -> Inference m ()
 
 makeSem ''Inference
 
-newtype InferenceState = InferenceState
-  { _inferenceMap :: HashMap Hole MetavarState
+data InferenceState = InferenceState
+  { _inferenceMap :: HashMap Hole MetavarState,
+    _inferenceIdens :: TypesTable
   }
 
 makeLenses ''InferenceState
 
 iniState :: InferenceState
-iniState = InferenceState mempty
-
-closeState :: Member (Error TypeCheckerError) r => InferenceState -> Sem r (HashMap Hole Expression)
+iniState = InferenceState mempty mempty
+
+closeState ::
+  Member (Error TypeCheckerError) r =>
+  InferenceState ->
+  Sem
+    r
+    ( HashMap Hole Expression,
+      TypesTable
+    )
 closeState = \case
-  InferenceState m -> execState mempty (f m)
+  InferenceState m idens -> do
+    holeMap <- execState mempty (f m)
+    return (holeMap, idens)
   where
     f ::
       forall r'.
@@ -110,7 +122,11 @@ re = reinterpret $ \case
   MatchTypes a b -> matchTypes' a b
   QueryMetavar h -> queryMetavar' h
   NormalizeType t -> normalizeType' t
+  RegisterIden i ty -> registerIden' i ty
   where
+    registerIden' :: Members '[State InferenceState] r => Name -> Expression -> Sem r ()
+    registerIden' i ty = modify (over inferenceIdens (HashMap.insert i ty))
+
     refineFreshMetavar ::
       Members '[Error TypeCheckerError, State InferenceState] r =>
       Hole ->
@@ -199,12 +215,10 @@ re = reinterpret $ \case
                     bicheck (go l1 l2) (local' (go r1 r2))
                 | otherwise = ok
 
-runInference :: Member (Error TypeCheckerError) r => Sem (Inference ': r) Expression -> Sem r Expression
-runInference a = do
-  (subs, expr) <- runState iniState (re a) >>= firstM closeState
-  return (fillHoles subs expr)
-
-runInferenceDef :: Member (Error TypeCheckerError) r => Sem (Inference ': r) FunctionDef -> Sem r FunctionDef
+runInferenceDef ::
+  Member (Error TypeCheckerError) r =>
+  Sem (Inference ': r) FunctionDef ->
+  Sem r (FunctionDef, TypesTable)
 runInferenceDef a = do
-  (subs, expr) <- runState iniState (re a) >>= firstM closeState
-  return (fillHolesFunctionDef subs expr)
+  ((subs, idens), expr) <- runState iniState (re a) >>= firstM closeState
+  return (fillHolesFunctionDef subs expr, fillHoles subs <$> idens)