Direct translation from MicroJuvix to MiniC.

* Closes issue #1341.
* Depends on PR [#8](anoma/juvix-stdlib#8) in juvix-stdlib.
* Translation/MonoJuvixToMiniC removed.
* MonoJuvix itself not removed because the MiniHaskell backend depends on it.
* Since MiniHaskell is deprecated, I see no point in wasting time on writing a translation from MicroJuvix to MiniHaskell.

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

@@ -112,6 +112,46 @@ 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 is not concrete")
+    . 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) ->
+        if isNothing m
+          then do
+            e' <- go e
+            r' <- go r
+            return (ExpressionFunction (Function (FunctionParameter m i e') r'))
+          else go r
+      ExpressionHole {} -> Nothing
+      ExpressionLiteral {} -> return t
+      ExpressionIden i -> case i of
+        IdenFunction {} -> return t
+        IdenInductive {} -> return t
+        IdenConstructor {} -> return t
+        IdenAxiom {} -> return t
+        IdenVar {} -> return t
+
 class HasExpressions a where
   leafExpressions :: Traversal' a Expression
 

src/Juvix/Syntax/MicroJuvix/MicroJuvixTypedResult.hs

@@ -9,10 +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,
-    _resultIdenTypes :: HashMap Iden Expression
+    _resultIdenTypes :: TypesTable
   }
 
 makeLenses ''MicroJuvixTypedResult

src/Juvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -16,12 +16,20 @@ 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
-  (idens, r) <- runState (mempty :: HashMap Iden Expression) (runReader table (mapM checkModule _resultModules))
+  (idens, r) <- runState (mempty :: TypesTable) (runReader table (mapM checkModule _resultModules))
   return
     MicroJuvixTypedResult
       { _resultMicroJuvixArityResult = res,
@@ -33,7 +41,7 @@ entryMicroJuvixTyped res@MicroJuvixArityResult {..} = do
     table = buildTable _resultModules
 
 checkModule ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State (HashMap Iden Expression)] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   Module ->
   Sem r Module
 checkModule Module {..} = do
@@ -45,7 +53,7 @@ checkModule Module {..} = do
       }
 
 checkModuleBody ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State (HashMap Iden Expression)] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   ModuleBody ->
   Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -56,30 +64,37 @@ checkModuleBody ModuleBody {..} = do
       }
 
 checkInclude ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State (HashMap Iden Expression)] 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, State (HashMap Iden Expression)] 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, State (HashMap Iden Expression)] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r =>
   FunctionDef ->
   Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
   (funDef, idens) <- runInferenceDef $ do
     info <- lookupFunction _funDefName
     checkFunctionDefType _funDefType
+    registerIden _funDefName _funDefType
     _funDefClauses' <- mapM (checkFunctionClause info) _funDefClauses
     return
       FunctionDef
@@ -89,9 +104,6 @@ checkFunctionDef FunctionDef {..} = do
   addIdens idens
   return funDef
 
-addIdens :: Member (State (HashMap Iden Expression)) r => HashMap Iden Expression -> Sem r ()
-addIdens idens = modify (HashMap.union idens)
-
 checkFunctionDefType :: forall r. Members '[Inference] r => Expression -> Sem r ()
 checkFunctionDefType = traverseOf_ (leafExpressions . _ExpressionHole) go
   where
@@ -172,7 +184,7 @@ checkFunctionClause info FunctionClause {..} = do
               }
 
 checkPatterns ::
-  Members '[Reader InfoTable, Error TypeCheckerError] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, Inference] r =>
   FunctionName ->
   [(FunctionParameter, Pattern)] ->
   Sem r LocalVars
@@ -183,7 +195,7 @@ typeOfArg = (^. paramType)
 
 checkPattern ::
   forall r.
-  Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference] r =>
   FunctionName ->
   FunctionParameter ->
   Pattern ->
@@ -202,6 +214,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
@@ -14,22 +15,28 @@ data Inference m a where
   FreshMetavar :: Hole -> Inference m TypedExpression
   MatchTypes :: Expression -> Expression -> Inference m Bool
   QueryMetavar :: Hole -> Inference m (Maybe Expression)
-  RegisterIden :: Iden -> Expression -> Inference m ()
+  RegisterIden :: Name -> Expression -> Inference m ()
 
 makeSem ''Inference
 
 data InferenceState = InferenceState
   { _inferenceMap :: HashMap Hole MetavarState,
-    _inferenceIdens :: HashMap Iden Expression
+    _inferenceIdens :: TypesTable
   }
 
 makeLenses ''InferenceState
 
 iniState :: InferenceState
 iniState = InferenceState mempty mempty
 
-closeState :: Member (Error TypeCheckerError) r => InferenceState -> Sem r (HashMap Hole Expression,
-                                                                             HashMap Iden Expression)
+closeState ::
+  Member (Error TypeCheckerError) r =>
+  InferenceState ->
+  Sem
+    r
+    ( HashMap Hole Expression,
+      TypesTable
+    )
 closeState = \case
   InferenceState m idens -> do
     holeMap <- execState mempty (f m)
@@ -73,7 +80,7 @@ re = reinterpret $ \case
   QueryMetavar h -> queryMetavar' h
   RegisterIden i ty -> registerIden' i ty
   where
-    registerIden' :: Members '[State InferenceState] r => Iden -> Expression -> Sem r ()
+    registerIden' :: Members '[State InferenceState] r => Name -> Expression -> Sem r ()
     registerIden' i ty = modify (over inferenceIdens (HashMap.insert i ty))
 
     queryMetavar' :: Members '[State InferenceState] r => Hole -> Sem r (Maybe Expression)
@@ -163,8 +170,10 @@ re = reinterpret $ \case
                     andM [go l1 l2, local' (go r1 r2)]
                 | otherwise = return False
 
-runInferenceDef :: Member (Error TypeCheckerError) r => Sem (Inference ': r) FunctionDef
-   -> Sem r (FunctionDef, HashMap Iden Expression)
+runInferenceDef ::
+  Member (Error TypeCheckerError) r =>
+  Sem (Inference ': r) FunctionDef ->
+  Sem r (FunctionDef, TypesTable)
 runInferenceDef a = do
   ((subs, idens), expr) <- runState iniState (re a) >>= firstM closeState
   return (fillHolesFunctionDef subs expr, fillHoles subs <$> idens)