[minihaskell] add compilation to MiniHaskell

app/Main.hs

@@ -25,6 +25,8 @@ import qualified MiniJuvix.Termination as T
 import qualified MiniJuvix.Termination.CallGraph as A
 import qualified MiniJuvix.Translation.AbstractToMicroJuvix as Micro
 import qualified MiniJuvix.Translation.ScopedToAbstract as A
+import qualified MiniJuvix.Translation.MicroJuvixToMiniHaskell as Hask
+import qualified MiniJuvix.Syntax.MiniHaskell.Pretty.Ansi as Hask
 import MiniJuvix.Utils.Version (runDisplayVersion)
 import Options.Applicative
 import Options.Applicative.Help.Pretty
@@ -264,13 +266,12 @@ go c = do
         Right {} -> putStrLn "Well done! It type checks"
     MiniHaskell MiniHaskellOptions {..} -> do
       m <- parseModuleIO _mhaskellInputFile
-      (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
-      -- a <- fromRightIO' putStrLn (return $ A.translateModule s)
-      _ <- fromRightIO' putStrLn (return $ A.translateModule s)
-      -- let mini = Micro.translateModule a
-      -- Micro.printPrettyCodeDefault mini
-      -- TODO
-      error "todo"
+      (_, s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
+      (_, a) <- fromRightIO' putStrLn (return $ A.translateModule s)
+      let micro = Micro.translateModule a
+      checkedMicro <- fromRightIO' putStrLn (return $ Micro.checkModule micro)
+      minihaskell <- fromRightIO' putStrLn (return $ Hask.translateModule checkedMicro)
+      Hask.printPrettyCodeDefault minihaskell
     Termination (Calls opts@CallsOptions {..}) -> do
       m <- parseModuleIO _callsInputFile
       (_ , s) <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m

src/MiniJuvix/Internal/Strings.hs

@@ -65,6 +65,9 @@ let_ = "let"
 public :: IsString s => s
 public = "public"
 
+any :: IsString s => s
+any = "Any"
+
 type_ :: IsString s => s
 type_ = "Type"
 

src/MiniJuvix/Syntax/Abstract/Language.hs

@@ -41,14 +41,19 @@ data Module s = Module
   deriving stock (Show, Eq)
 
 data ModuleBody = ModuleBody
-  { _moduleInductives :: HashMap InductiveName (Indexed InductiveDef),
-    _moduleFunctions :: HashMap FunctionName (Indexed FunctionDef),
-    _moduleImports :: [Indexed TopModule],
-    _moduleForeigns :: [Indexed ForeignBlock],
-    _moduleLocalModules :: HashMap LocalModuleName (Indexed LocalModule)
+  { _moduleStatements :: [Statement]
   }
   deriving stock (Show, Eq)
 
+data Statement =
+  StatementInductive InductiveDef
+  | StatementFunction FunctionDef
+  | StatementImport TopModule
+  | StatementForeign ForeignBlock
+  | StatementLocalModule LocalModule
+  | StatementAxiom AxiomDef
+  deriving stock (Show, Eq)
+
 data FunctionDef = FunctionDef
   { _funDefName :: FunctionName,
     _funDefTypeSig :: Expression,

src/MiniJuvix/Syntax/Backends.hs

@@ -0,0 +1,14 @@
+module MiniJuvix.Syntax.Backends where
+
+import MiniJuvix.Prelude
+
+data Backend = BackendGhc | BackendAgda
+  deriving stock (Show, Eq, Ord)
+
+data BackendItem = BackendItem
+  { _backendItemBackend :: Backend,
+    _backendItemCode :: Text
+  }
+  deriving stock (Show, Eq, Ord)
+
+makeLenses ''BackendItem

src/MiniJuvix/Syntax/Concrete/Language.hs

@@ -3,6 +3,9 @@ module MiniJuvix.Syntax.Concrete.Language
   ( module MiniJuvix.Syntax.Concrete.Language,
     module MiniJuvix.Syntax.Concrete.Name,
     module MiniJuvix.Syntax.Concrete.Loc,
+    module MiniJuvix.Syntax.Concrete.Literal,
+    module MiniJuvix.Syntax.Backends,
+    module MiniJuvix.Syntax.ForeignBlock,
     module MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn,
     module MiniJuvix.Syntax.Concrete.PublicAnn,
     module MiniJuvix.Syntax.Concrete.ModuleIsTop,
@@ -18,7 +21,10 @@ where
 import qualified Data.Kind as GHC
 import MiniJuvix.Prelude hiding (show)
 import MiniJuvix.Syntax.Concrete.Language.Stage
+import MiniJuvix.Syntax.Backends
+import MiniJuvix.Syntax.ForeignBlock
 import MiniJuvix.Syntax.Concrete.Loc
+import MiniJuvix.Syntax.Concrete.Literal
 import MiniJuvix.Syntax.Concrete.ModuleIsTop
 import MiniJuvix.Syntax.Concrete.Name
 import MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn
@@ -132,12 +138,6 @@ deriving stock instance
   ) =>
   Ord (Statement s)
 
-data ForeignBlock = ForeignBlock
-  { _foreignBackend :: Backend,
-    _foreignCode :: Text
-  }
-  deriving stock (Eq, Ord, Show)
-
 --------------------------------------------------------------------------------
 -- Import statement
 --------------------------------------------------------------------------------
@@ -662,11 +662,6 @@ data Expression
   | ExpressionFunction (Function 'Scoped)
   deriving stock (Show, Eq, Ord)
 
-instance HasAtomicity Literal where
-  atomicity = \case
-    LitInteger {} -> Atom
-    LitString {} -> Atom
-
 instance HasAtomicity Expression where
   atomicity e = case e of
     ExpressionIdentifier {} -> Atom
@@ -685,11 +680,6 @@ instance HasAtomicity Expression where
 -- Expression atom
 --------------------------------------------------------------------------------
 
-data Literal
-  = LitString Text
-  | LitInteger Integer
-  deriving stock (Show, Eq, Ord)
-
 -- | Expressions without application
 data ExpressionAtom (s :: Stage)
   = AtomIdentifier (IdentifierType s)
@@ -1058,19 +1048,6 @@ deriving stock instance
   ) =>
   Ord (LetClause s)
 
---------------------------------------------------------------------------------
--- Backends
---------------------------------------------------------------------------------
-
-data Backend = BackendGhc | BackendAgda
-  deriving stock (Show, Eq, Ord)
-
-data BackendItem = BackendItem
-  { _backendItemBackend :: Backend,
-    _backendItemCode :: Text
-  }
-  deriving stock (Show, Eq, Ord)
-
 --------------------------------------------------------------------------------
 -- Debugging statements
 --------------------------------------------------------------------------------
@@ -1117,14 +1094,12 @@ makeLenses ''TypeSignature
 makeLenses ''AxiomDef
 makeLenses ''FunctionClause
 makeLenses ''InductiveParameter
-makeLenses ''ForeignBlock
 makeLenses ''AxiomRef'
 makeLenses ''InductiveRef'
 makeLenses ''ModuleRef'
 makeLenses ''ModuleRef''
 makeLenses ''FunctionRef'
 makeLenses ''ConstructorRef'
-makeLenses ''BackendItem
 makeLenses ''OpenModule
 makeLenses ''PatternApp
 makeLenses ''PatternInfixApp

src/MiniJuvix/Syntax/Concrete/Literal.hs

@@ -0,0 +1,23 @@
+module MiniJuvix.Syntax.Concrete.Literal where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Fixity
+import Prettyprinter
+
+data Literal
+  = LitString Text
+  | LitInteger Integer
+  deriving stock (Show, Eq, Ord)
+
+instance HasAtomicity Literal where
+  atomicity = \case
+    LitInteger {} -> Atom
+    LitString {} -> Atom
+
+instance Pretty Literal where
+  pretty = \case
+    LitInteger n -> pretty n
+    LitString s -> ppStringLit s
+     where
+     ppStringLit :: Text -> Doc a
+     ppStringLit = dquotes . pretty

src/MiniJuvix/Syntax/Concrete/Scoped/Name.hs

@@ -1,8 +1,7 @@
-{-# LANGUAGE StandaloneKindSignatures #-}
-
 module MiniJuvix.Syntax.Concrete.Scoped.Name
   ( module MiniJuvix.Syntax.Concrete.Scoped.Name,
     module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
+    module MiniJuvix.Syntax.NameId
   )
 where
 
@@ -12,9 +11,9 @@ import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Concrete.Loc
 import qualified MiniJuvix.Syntax.Concrete.Name as C
 import MiniJuvix.Syntax.Concrete.Scoped.VisibilityAnn
+import MiniJuvix.Syntax.NameId
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
 import qualified MiniJuvix.Syntax.Fixity as C
-import Prettyprinter
 
 --------------------------------------------------------------------------------
 -- Names
@@ -24,12 +23,6 @@ data IsConcrete = NotConcrete | Concrete
 
 $(genSingletons [''IsConcrete])
 
-newtype NameId = NameId Word64
-  deriving stock (Show, Eq, Ord, Generic)
-
-instance Pretty NameId where
-  pretty (NameId w) = pretty w
-
 data AbsModulePath = AbsModulePath
   { absTopModulePath :: C.TopModulePath,
     absLocalPath :: [C.Symbol]
@@ -62,8 +55,6 @@ allNameIds = NameId <$> ids
     ids = aux minBound
     aux i = Cons i (aux (succ i))
 
-instance Hashable NameId
-
 -- | Why a symbol is in scope.
 data WhyInScope
   = -- | Inherited from the parent module.

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -422,7 +422,7 @@ ppName = case sing :: SStage s of
   SScoped -> ppCode
 
 instance PrettyCode S.NameId where
-  ppCode (S.NameId k) = return $ pretty k
+  ppCode (S.NameId k) = return (pretty k)
 
 annDef :: forall s. SingI s => SymbolType s -> Doc Ann -> Doc Ann
 annDef nm = case sing :: SStage s of
@@ -673,7 +673,7 @@ instance PrettyCode Application where
     return $ l' <+> r'
 
 instance PrettyCode Literal where
-  ppCode l = case l of
+  ppCode = \case
     LitInteger n -> return $ annotate AnnLiteralInteger (pretty n)
     LitString s -> return $ ppStringLit s
 

src/MiniJuvix/Syntax/ForeignBlock.hs

@@ -0,0 +1,13 @@
+module MiniJuvix.Syntax.ForeignBlock where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Backends
+
+data ForeignBlock = ForeignBlock
+  { _foreignBackend :: Backend,
+    _foreignCode :: Text
+  }
+  deriving stock (Eq, Ord, Show)
+
+
+makeLenses ''ForeignBlock

src/MiniJuvix/Syntax/MicroJuvix/InfoTable.hs

@@ -0,0 +1,52 @@
+module MiniJuvix.Syntax.MicroJuvix.InfoTable where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Syntax.Backends
+import qualified Data.HashMap.Strict as HashMap
+
+data ConstructorInfo = ConstructorInfo {
+  _constructorInfoArgs :: [Type],
+  _constructorInfoInductive :: InductiveName
+  }
+
+data FunctionInfo = FunctionInfo {
+  _functionInfoType :: Type
+  }
+
+data AxiomInfo = AxiomInfo {
+  _axiomInfoType :: Type,
+  _axiomInfoBackends :: [BackendItem]
+  }
+
+data InfoTable = InfoTable {
+  _infoConstructors :: HashMap Name ConstructorInfo,
+  _infoAxioms :: HashMap Name AxiomInfo,
+  _infoFunctions :: HashMap Name FunctionInfo
+  }
+
+buildTable :: Module -> InfoTable
+buildTable m = InfoTable {..}
+  where
+   _infoConstructors :: HashMap Name ConstructorInfo
+   _infoConstructors = HashMap.fromList
+     [ (c ^. constructorName, ConstructorInfo args ind) |
+       StatementInductive d <- ss,
+       let ind = d ^. inductiveName,
+       c <- d ^. inductiveConstructors,
+       let args = c ^. constructorParameters
+     ]
+   _infoFunctions :: HashMap Name FunctionInfo
+   _infoFunctions = HashMap.fromList
+     [ (f ^. funDefName, FunctionInfo (f ^. funDefType)) |
+       StatementFunction f <- ss]
+   _infoAxioms :: HashMap Name AxiomInfo
+   _infoAxioms = HashMap.fromList
+     [ (d ^. axiomName , AxiomInfo (d ^. axiomType) (d ^. axiomBackendItems))
+       | StatementAxiom d <- ss ]
+   ss = m ^. moduleBody ^. moduleStatements
+
+makeLenses ''InfoTable
+makeLenses ''FunctionInfo
+makeLenses ''ConstructorInfo
+makeLenses ''AxiomInfo

src/MiniJuvix/Syntax/MicroJuvix/Language.hs

@@ -2,17 +2,23 @@ module MiniJuvix.Syntax.MicroJuvix.Language
   ( module MiniJuvix.Syntax.MicroJuvix.Language,
     module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
     module MiniJuvix.Syntax.Concrete.Scoped.Name,
+    module MiniJuvix.Syntax.Concrete.Literal,
   )
 where
 
 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Concrete.Language (ForeignBlock (..))
+import MiniJuvix.Syntax.ForeignBlock
+import MiniJuvix.Syntax.Backends
 import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..))
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
+import MiniJuvix.Syntax.Concrete.Literal
 import MiniJuvix.Syntax.Fixity
+import Prettyprinter
 
 type FunctionName = Name
 
+type AxiomName = Name
+
 type VarName = Name
 
 type ConstrName = Name
@@ -24,6 +30,7 @@ data Name = Name
     _nameId :: NameId,
     _nameKind :: NameKind
   }
+  deriving stock (Show)
 
 makeLenses ''Name
 
@@ -39,6 +46,9 @@ instance Hashable Name where
 instance HasNameKind Name where
   getNameKind = _nameKind
 
+instance Pretty Name where
+  pretty = pretty . _nameText
+
 data Module = Module
   { _moduleName :: Name,
     _moduleBody :: ModuleBody
@@ -52,10 +62,17 @@ data Statement =
   StatementInductive InductiveDef
   | StatementFunction FunctionDef
   | StatementForeign ForeignBlock
+  | StatementAxiom AxiomDef
+
+data AxiomDef = AxiomDef
+  { _axiomName :: AxiomName,
+    _axiomType :: Type,
+    _axiomBackendItems :: [BackendItem]
+  }
 
 data FunctionDef = FunctionDef
   { _funDefName :: FunctionName,
-    _funDefTypeSig :: Type,
+    _funDefType :: Type,
     _funDefClauses :: NonEmpty FunctionClause
   }
 
@@ -68,6 +85,7 @@ data Iden
   = IdenFunction Name
   | IdenConstructor Name
   | IdenVar VarName
+  | IdenAxiom Name
 
 data TypedExpression = TypedExpression {
   _typedType :: Type,
@@ -77,6 +95,7 @@ data TypedExpression = TypedExpression {
 data Expression
   = ExpressionIden Iden
   | ExpressionApplication Application
+  | ExpressionLiteral Literal
   | ExpressionTyped TypedExpression
 
 data Application = Application
@@ -88,7 +107,7 @@ data Function = Function
   { _funLeft :: Type,
     _funRight :: Type
   }
-  deriving stock (Eq)
+  deriving stock (Show, Eq)
 
 -- | Fully applied constructor in a pattern.
 data ConstructorApp = ConstructorApp
@@ -111,36 +130,24 @@ data InductiveConstructorDef = InductiveConstructorDef
     _constructorParameters :: [Type]
   }
 
-newtype TypeIden
+data TypeIden
   = TypeIdenInductive InductiveName
-  deriving stock (Eq)
+  | TypeIdenAxiom AxiomName
+  deriving stock (Show, Eq)
 
 data Type
   = TypeIden TypeIden
   | TypeFunction Function
-  deriving stock (Eq)
-
-data ConstructorInfo = ConstructorInfo {
-  _constructorInfoArgs :: [Type],
-  _constructorInfoInductive :: InductiveName
-  }
-
-data FunctionInfo = FunctionInfo {
-  _functionInfoType :: Type
-  }
-
-data InfoTable = InfoTable {
-  _infoConstructors :: HashMap Name ConstructorInfo,
-  _infoFunctions :: HashMap Name FunctionInfo
-  }
+  | TypeUniverse
+  | TypeAny
+  deriving stock (Show, Eq)
 
 makeLenses ''Module
 makeLenses ''Function
 makeLenses ''FunctionDef
-makeLenses ''FunctionInfo
-makeLenses ''ConstructorInfo
 makeLenses ''FunctionClause
 makeLenses ''InductiveDef
+makeLenses ''AxiomDef
 makeLenses ''ModuleBody
 makeLenses ''Application
 makeLenses ''TypedExpression
@@ -155,6 +162,7 @@ instance HasAtomicity Expression where
     ExpressionIden {} -> Atom
     ExpressionApplication a -> atomicity a
     ExpressionTyped t -> atomicity (t ^. typedExpression)
+    ExpressionLiteral l -> atomicity l
 
 instance HasAtomicity Function where
   atomicity = const (Aggregate funFixity)
@@ -163,6 +171,8 @@ instance HasAtomicity Type where
   atomicity t = case t of
     TypeIden {} -> Atom
     TypeFunction f -> atomicity f
+    TypeUniverse -> Atom
+    TypeAny -> Atom
 
 instance HasAtomicity ConstructorApp where
   atomicity (ConstructorApp _ args)

src/MiniJuvix/Syntax/MicroJuvix/Pretty/Base.hs

@@ -1,10 +1,10 @@
--- TODO handle capital letters and characters not supported by Haskell.
 module MiniJuvix.Syntax.MicroJuvix.Pretty.Base where
 
 import qualified MiniJuvix.Internal.Strings as Str
 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Concrete.Language (Backend (..), ForeignBlock (..))
 import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.Backends
+import MiniJuvix.Syntax.ForeignBlock
 import MiniJuvix.Syntax.MicroJuvix.Language
 import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
 import Prettyprinter
@@ -34,6 +34,7 @@ instance PrettyCode Iden where
     IdenFunction na -> ppCode na
     IdenConstructor na -> ppCode na
     IdenVar na -> ppCode na
+    IdenAxiom a -> ppCode a
 
 instance PrettyCode Application where
   ppCode a = do
@@ -45,10 +46,11 @@ instance PrettyCode TypedExpression where
   ppCode e = ppCode (e ^. typedExpression)
 
 instance PrettyCode Expression where
-  ppCode e = case e of
+  ppCode = \case
     ExpressionIden i -> ppCode i
     ExpressionApplication a -> ppCode a
     ExpressionTyped a -> ppCode a
+    ExpressionLiteral l -> return (pretty l)
 
 keyword :: Text -> Doc Ann
 keyword = annotate AnnKeyword . pretty
@@ -56,6 +58,9 @@ keyword = annotate AnnKeyword . pretty
 kwArrow :: Doc Ann
 kwArrow = keyword Str.toAscii
 
+kwMapsto :: Doc Ann
+kwMapsto = keyword Str.mapstoUnicode
+
 kwForeign :: Doc Ann
 kwForeign = keyword Str.foreign_
 
@@ -65,6 +70,8 @@ kwAgda = keyword Str.agda
 kwGhc :: Doc Ann
 kwGhc = keyword Str.ghc
 
+kwColon :: Doc Ann
+kwColon = keyword Str.colon
 
 kwData :: Doc Ann
 kwData = keyword Str.data_
@@ -78,25 +85,47 @@ kwColonColon = keyword (Str.colon <> Str.colon)
 kwPipe :: Doc Ann
 kwPipe = keyword Str.pipe
 
+kwAxiom :: Doc Ann
+kwAxiom = keyword Str.axiom
+
 kwWhere :: Doc Ann
 kwWhere = keyword Str.where_
 
 kwModule :: Doc Ann
 kwModule = keyword Str.module_
 
+kwAny :: Doc Ann
+kwAny = keyword Str.any
+
+kwType :: Doc Ann
+kwType = keyword Str.type_
+
 kwWildcard :: Doc Ann
 kwWildcard = keyword Str.underscore
 
+instance PrettyCode BackendItem where
+  ppCode BackendItem {..} = do
+    backend <- ppCode _backendItemBackend
+    return $
+      backend <+> kwMapsto <+> pretty _backendItemCode
+
 instance PrettyCode Function where
   ppCode (Function l r) = do
     l' <- ppLeftExpression funFixity l
     r' <- ppRightExpression funFixity r
     return $ l' <+> kwArrow <+> r'
 
+instance PrettyCode TypeIden where
+  ppCode = \case
+    TypeIdenInductive i -> ppCode i
+    TypeIdenAxiom i -> ppCode i
+
 instance PrettyCode Type where
-  ppCode t = case t of
-    TypeIden (TypeIdenInductive n) -> ppCode n
+  ppCode = \case
+    TypeIden i -> ppCode i
     TypeFunction f -> ppCode f
+    TypeUniverse -> return kwType
+    TypeAny -> return kwAny
 
 instance PrettyCode InductiveConstructorDef where
   ppCode c = do
@@ -109,6 +138,14 @@ indent' d = do
   i <- asks _optIndent
   return $ indent i d
 
+ppBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
+ppBlock items = mapM ppCode items >>= bracesIndent . vsep . toList
+
+bracesIndent :: Members '[Reader Options] r => Doc Ann -> Sem r (Doc Ann)
+bracesIndent d = do
+  d' <- indent' d
+  return $ braces (line <> d' <> line)
+
 instance PrettyCode InductiveDef where
   ppCode d = do
     inductiveName' <- ppCode (d ^. inductiveName)
@@ -131,10 +168,10 @@ instance PrettyCode Pattern where
 instance PrettyCode FunctionDef where
   ppCode f = do
     funDefName' <- ppCode (f ^. funDefName)
-    funDefTypeSig' <- ppCode (f ^. funDefTypeSig)
+    funDefType' <- ppCode (f ^. funDefType)
     clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses)
     return $
-      funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
+      funDefName' <+> kwColonColon <+> funDefType' <> line
         <> vsep (toList clauses')
     where
       ppClause fun c = do
@@ -156,11 +193,22 @@ instance PrettyCode ForeignBlock where
         <> line
         <> rbrace
 
+instance PrettyCode AxiomDef where
+  ppCode AxiomDef {..} = do
+    axiomName' <- ppCode _axiomName
+    axiomType' <- ppCode _axiomType
+    axiomBackendItems' <- case _axiomBackendItems of
+      [] -> return Nothing
+      bs -> Just <$> ppBlock bs
+    return $ kwAxiom <+> axiomName' <+> kwColon <+> axiomType' <+?> axiomBackendItems'
+
+
 instance PrettyCode Statement where
   ppCode = \case
     StatementForeign f -> ppCode f
     StatementFunction f -> ppCode f
     StatementInductive f -> ppCode f
+    StatementAxiom f -> ppCode f
 
 instance PrettyCode ModuleBody where
   ppCode m = do

src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs

@@ -1,6 +1,7 @@
 module MiniJuvix.Syntax.MicroJuvix.TypeChecker where
 import MiniJuvix.Prelude
 import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Syntax.MicroJuvix.InfoTable
 import qualified Data.HashMap.Strict as HashMap
 
 type Err = Text
@@ -14,23 +15,6 @@ makeLenses ''LocalVars
 checkModule :: Module -> Either Err Module
 checkModule m = run $ runError $ runReader (buildTable m) (checkModule' m)
 
-buildTable :: Module -> InfoTable
-buildTable m = InfoTable {..}
-  where
-   _infoConstructors :: HashMap Name ConstructorInfo
-   _infoConstructors = HashMap.fromList
-     [ (c ^. constructorName, ConstructorInfo args ind) |
-       StatementInductive d <- ss,
-       let ind = d ^. inductiveName,
-       c <- d ^. inductiveConstructors,
-       let args = c ^. constructorParameters
-     ]
-   _infoFunctions :: HashMap Name FunctionInfo
-   _infoFunctions = HashMap.fromList
-     [ (f ^. funDefName, FunctionInfo (f ^. funDefTypeSig)) |
-       StatementFunction f <- ss]
-   ss = m ^. moduleBody ^. moduleStatements
-
 checkModule' :: Members '[Reader InfoTable, Error Err] r =>
   Module -> Sem r Module
 checkModule' Module {..} = do
@@ -53,7 +37,8 @@ checkStatement :: Members '[Reader InfoTable, Error Err] r =>
 checkStatement s = case s of
   StatementFunction fun -> StatementFunction <$> checkFunctionDef fun
   StatementForeign {} -> return s
-  StatementInductive {} -> return s -- TODO is checking inductives needed?
+  StatementInductive {} -> return s
+  StatementAxiom {} -> return s
 
 checkFunctionDef :: Members '[Reader InfoTable, Error Err] r =>
   FunctionDef -> Sem r FunctionDef
@@ -69,9 +54,17 @@ checkExpression :: Members '[Reader InfoTable, Error Err, Reader LocalVars] r =>
   Type -> Expression -> Sem r Expression
 checkExpression t e = do
   t' <- inferExpression' e
-  when (t /= t' ^. typedType) (throwErr "wrong type")
+  unlessM (matchTypes t (t' ^. typedType)) (throwErr "wrong type")
   return (ExpressionTyped t')
 
+matchTypes :: Members '[Reader InfoTable] r =>
+  Type -> Type -> Sem r Bool
+matchTypes a b = do
+  a' <- normalizeType a
+  b' <- normalizeType b
+  return $
+    a' == TypeAny || b' == TypeAny || a' == b'
+
 inferExpression :: Members '[Reader InfoTable, Error Err, Reader LocalVars] r =>
    Expression -> Sem r Expression
 inferExpression = fmap ExpressionTyped . inferExpression'
@@ -82,6 +75,9 @@ lookupConstructor f = HashMap.lookupDefault impossible f <$> asks _infoConstruct
 lookupFunction :: Member (Reader InfoTable) r => Name -> Sem r FunctionInfo
 lookupFunction f = HashMap.lookupDefault impossible f <$> asks _infoFunctions
 
+lookupAxiom :: Member (Reader InfoTable) r => Name -> Sem r AxiomInfo
+lookupAxiom f = HashMap.lookupDefault impossible f <$> asks _infoAxioms
+
 lookupVar :: Member (Reader LocalVars) r => Name -> Sem r Type
 lookupVar v = HashMap.lookupDefault impossible v <$> asks _localTypes
 
@@ -100,8 +96,8 @@ foldFunType l r = case l of
 -- | a -> (b -> c)  ==> ([a, b], c)
 unfoldFunType :: Type -> ([Type], Type)
 unfoldFunType t = case t of
-  TypeIden {} -> ([], t)
   TypeFunction (Function l r) -> first (l:) (unfoldFunType r)
+  _ -> ([], t)
 
 checkFunctionClause :: forall r. Members '[Reader InfoTable, Error Err] r =>
   FunctionInfo -> FunctionClause -> Sem r FunctionClause
@@ -139,13 +135,33 @@ checkPattern type_ pat = LocalVars . HashMap.fromList <$> go type_ pat
 throwErr :: Members '[Error Err] r => Err -> Sem r a
 throwErr = throw
 
+normalizeType :: forall r. Members '[Reader InfoTable] r => Type -> Sem r Type
+normalizeType t = case t of
+  TypeAny -> return TypeAny
+  TypeUniverse -> return TypeUniverse
+  TypeFunction f -> TypeFunction <$> normalizeFunction f
+  TypeIden i -> normalizeIden i
+  where
+  normalizeIden :: TypeIden -> Sem r Type
+  normalizeIden i = case i of
+   TypeIdenInductive {} -> return (TypeIden i)
+   TypeIdenAxiom {} -> return (TypeIden i)
+  normalizeFunction :: Function -> Sem r Function
+  normalizeFunction (Function l r) = do
+    l' <- normalizeType l
+    r' <- normalizeType r
+    return (Function l' r')
+
 inferExpression' :: forall r. Members '[Reader InfoTable, Error Err, Reader LocalVars] r =>
    Expression -> Sem r TypedExpression
 inferExpression' e = case e of
   ExpressionIden i -> inferIden i
   ExpressionApplication a -> inferApplication a
   ExpressionTyped {} -> impossible
+  ExpressionLiteral l -> goLiteral l
   where
+  goLiteral :: Literal -> Sem r TypedExpression
+  goLiteral l = return (TypedExpression TypeAny (ExpressionLiteral l))
   inferIden :: Iden -> Sem r TypedExpression
   inferIden i = case i of
     IdenFunction fun -> do
@@ -157,6 +173,9 @@ inferExpression' e = case e of
     IdenVar v -> do
       ty <- lookupVar v
       return (TypedExpression ty (ExpressionIden i))
+    IdenAxiom v -> do
+      info <- lookupAxiom v
+      return (TypedExpression (info ^. axiomInfoType) (ExpressionIden i))
   inferApplication :: Application -> Sem r TypedExpression
   inferApplication a = do
     l <- inferExpression' (a ^. appLeft)
@@ -172,4 +191,4 @@ inferExpression' e = case e of
   getFunctionType :: Type -> Sem r Function
   getFunctionType t = case t of
     TypeFunction f -> return f
-    _ -> throwErr "expected function type"
+    _ -> throwErr ("expected function type " <> show t)

src/MiniJuvix/Syntax/MiniHaskell/Language.hs

@@ -1,13 +1,15 @@
 module MiniJuvix.Syntax.MiniHaskell.Language
   ( module MiniJuvix.Syntax.MiniHaskell.Language,
     module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
-    module MiniJuvix.Syntax.Concrete.Scoped.Name,
+    module MiniJuvix.Syntax.NameId,
+    module MiniJuvix.Syntax.Concrete.Literal,
   )
 where
 
 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId (..))
+import MiniJuvix.Syntax.NameId
 import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
+import MiniJuvix.Syntax.Concrete.Literal
 import MiniJuvix.Syntax.Fixity
 
 type FunctionName = Name
@@ -22,6 +24,7 @@ data Name = Name
   { _nameText :: Text,
     _nameKind :: NameKind
   }
+  deriving stock (Show)
 
 makeLenses ''Name
 
@@ -32,71 +35,88 @@ data Module = Module
   { _moduleName :: Name,
     _moduleBody :: ModuleBody
   }
+  deriving stock (Show)
 
 newtype ModuleBody = ModuleBody
   { _moduleStatements :: [Statement]
   }
+  deriving stock (Show)
   deriving newtype (Monoid, Semigroup)
 
 data Statement
-  = StatementInductiveDef InductiveDef
-  | StatementFunctionDef FunctionDef
+  = StatementInductive InductiveDef
+  | StatementFunction FunctionDef
+  | StatementVerbatim Text
+  deriving stock (Show)
 
 data FunctionDef = FunctionDef
   { _funDefName :: FunctionName,
-    _funDefTypeSig :: Type,
+    _funDefType :: Type,
     _funDefClauses :: NonEmpty FunctionClause
   }
+  deriving stock (Show)
 
 data FunctionClause = FunctionClause
   { _clausePatterns :: [Pattern],
     _clauseBody :: Expression
   }
+  deriving stock (Show)
 
 type Iden = Name
 
 data Expression
   = ExpressionIden Iden
   | ExpressionApplication Application
-
--- TODO Add a constructor for literals
+  | ExpressionLiteral Literal
+  | ExpressionVerbatim Text
+  deriving stock (Show)
 
 data Application = Application
   { _appLeft :: Expression,
     _appRight :: Expression
   }
+  deriving stock (Show)
 
 data Function = Function
   { _funLeft :: Type,
     _funRight :: Type
   }
+  deriving stock (Show)
 
 -- | Fully applied constructor in a pattern.
 data ConstructorApp = ConstructorApp
   { _constrAppConstructor :: Name,
     _constrAppParameters :: [Pattern]
   }
+  deriving stock (Show)
 
 data Pattern
   = PatternVariable VarName
   | PatternConstructorApp ConstructorApp
   | PatternWildcard
+  deriving stock (Show)
 
 data InductiveDef = InductiveDef
   { _inductiveName :: InductiveName,
     _inductiveConstructors :: [InductiveConstructorDef]
   }
+  deriving stock (Show)
 
 data InductiveConstructorDef = InductiveConstructorDef
   { _constructorName :: ConstrName,
     _constructorParameters :: [Type]
   }
+  deriving stock (Show)
 
-type TypeIden = InductiveName
+data TypeIden
+  = TypeIdenInductive InductiveName
+  deriving stock (Show)
 
 data Type
   = TypeIden TypeIden
   | TypeFunction Function
+  | TypeVerbatim Text
+  deriving stock (Show)
 
 makeLenses ''Module
 makeLenses ''Function
@@ -115,6 +135,8 @@ instance HasAtomicity Expression where
   atomicity e = case e of
     ExpressionIden {} -> Atom
     ExpressionApplication a -> atomicity a
+    ExpressionVerbatim {} -> Atom
+    ExpressionLiteral l -> atomicity l
 
 instance HasAtomicity Function where
   atomicity = const (Aggregate funFixity)
@@ -123,6 +145,7 @@ instance HasAtomicity Type where
   atomicity t = case t of
     TypeIden {} -> Atom
     TypeFunction f -> atomicity f
+    TypeVerbatim {} -> Atom
 
 instance HasAtomicity ConstructorApp where
   atomicity (ConstructorApp _ args)

src/MiniJuvix/Syntax/MiniHaskell/Pretty/Base.hs

@@ -37,6 +37,8 @@ instance PrettyCode Expression where
   ppCode e = case e of
     ExpressionIden i -> ppCode i
     ExpressionApplication a -> ppCode a
+    ExpressionVerbatim c -> return (pretty c)
+    ExpressionLiteral l -> ppCode l
 
 keyword :: Text -> Doc Ann
 keyword = annotate AnnKeyword . pretty
@@ -71,10 +73,15 @@ instance PrettyCode Function where
     r' <- ppRightExpression funFixity r
     return $ l' <+> kwArrow <+> r'
 
+instance PrettyCode TypeIden where
+  ppCode = \case
+    TypeIdenInductive t -> ppCode t
+
 instance PrettyCode Type where
   ppCode t = case t of
     TypeIden n -> ppCode n
     TypeFunction f -> ppCode f
+    TypeVerbatim c -> return (pretty c)
 
 instance PrettyCode InductiveConstructorDef where
   ppCode c = do
@@ -109,7 +116,7 @@ instance PrettyCode Pattern where
 instance PrettyCode FunctionDef where
   ppCode f = do
     funDefName' <- ppCode (f ^. funDefName)
-    funDefTypeSig' <- ppCode (f ^. funDefTypeSig)
+    funDefTypeSig' <- ppCode (f ^. funDefType)
     clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses)
     return $
       funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
@@ -122,8 +129,9 @@ instance PrettyCode FunctionDef where
 
 instance PrettyCode Statement where
   ppCode = \case
-    StatementFunctionDef f -> ppCode f
-    StatementInductiveDef d -> ppCode d
+    StatementFunction f -> ppCode f
+    StatementInductive d -> ppCode d
+    StatementVerbatim t -> return (pretty t)
 
 instance PrettyCode ModuleBody where
   ppCode m = do
@@ -132,6 +140,21 @@ instance PrettyCode ModuleBody where
     where
       vsep2 = concatWith (\a b -> a <> line <> line <> b)
 
+instance PrettyCode Literal where
+  ppCode = \case
+    LitInteger n -> return $ annotate AnnLiteralInteger (pretty n)
+    LitString s -> return $ ppStringLit s
+
+doubleQuotes :: Doc Ann -> Doc Ann
+doubleQuotes = enclose kwDQuote kwDQuote
+
+kwDQuote :: Doc Ann
+kwDQuote = pretty ("\"" :: Text)
+
+ppStringLit :: Text -> Doc Ann
+ppStringLit = annotate AnnLiteralString . doubleQuotes . pretty
+
+
 instance PrettyCode Module where
   ppCode m = do
     name' <- ppCode (m ^. moduleName)

src/MiniJuvix/Syntax/NameId.hs

@@ -0,0 +1,15 @@
+module MiniJuvix.Syntax.NameId where
+
+import Prettyprinter
+import MiniJuvix.Prelude
+
+newtype NameId = NameId {
+  _unNameId :: Word64
+  }
+  deriving stock (Show, Eq, Ord, Generic)
+makeLenses ''NameId
+
+instance Pretty NameId where
+  pretty (NameId w) = pretty w
+
+instance Hashable NameId

src/MiniJuvix/Syntax/Universe.hs

@@ -4,9 +4,11 @@ import MiniJuvix.Prelude
 import MiniJuvix.Syntax.Fixity
 
 newtype Universe = Universe
-  { universeLevel :: Maybe Natural
+  { _universeLevel :: Maybe Natural
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasAtomicity Universe where
   atomicity = const Atom
+
+makeLenses ''Universe

src/MiniJuvix/Termination/CallMap.hs

@@ -86,8 +86,11 @@ checkModule m = checkModuleBody (m ^. moduleBody)
 
 checkModuleBody :: Members '[State CallMap] r => ModuleBody -> Sem r ()
 checkModuleBody body = do
-  mapM_ (checkFunctionDef . (^. indexedThing)) (toList $ body ^. moduleFunctions)
-  mapM_ (checkLocalModule . (^. indexedThing)) (toList $ body ^. moduleLocalModules)
+  mapM_ checkFunctionDef moduleFunctions
+  mapM_ checkLocalModule moduleLocalModules
+  where
+  moduleFunctions = [ f | StatementFunction f <- body ^. moduleStatements ]
+  moduleLocalModules = [ f | StatementLocalModule f <- body ^. moduleStatements ]
 
 checkLocalModule :: Members '[State CallMap] r => LocalModule -> Sem r ()
 checkLocalModule m = checkModuleBody (m ^. moduleBody)

src/MiniJuvix/Translation/AbstractToMicroJuvix.hs

@@ -1,11 +1,10 @@
 module MiniJuvix.Translation.AbstractToMicroJuvix where
 
-import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Concrete.Language (ForeignBlock)
 import qualified MiniJuvix.Syntax.Abstract.Language.Extra as A
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Syntax.Universe
 import qualified MiniJuvix.Syntax.Usage as A
 
 translateModule :: A.TopModule -> Module
@@ -26,38 +25,25 @@ goSymbol s =
   Name
     { _nameText = S.symbolText s,
       _nameId = S._nameId s,
-      _nameKind = getNameKind s
-    }
+      _nameKind = getNameKind s }
 
 unsupported :: Text -> a
-unsupported thing = error ("Not yet supported: " <> thing)
+unsupported thing = error ("Abstract to MicroJuvix: Not yet supported: " <> thing)
 
 goImport :: A.TopModule -> ModuleBody
 goImport m = goModuleBody (m ^. A.moduleBody)
 
 goModuleBody :: A.ModuleBody -> ModuleBody
-goModuleBody b
-  | not (HashMap.null (b ^. A.moduleLocalModules)) = unsupported "local modules"
-  | otherwise =
-    ModuleBody sortedStatements
-  where
-   sortedStatements :: [Statement]
-   sortedStatements = map _indexedThing (sortOn _indexedIx statements)
-   statements :: [Indexed Statement]
-   statements = map (fmap StatementForeign) foreigns
-     <> map (fmap StatementFunction) functions
-     <> map (fmap StatementInductive) inductives
-   inductives :: [Indexed InductiveDef]
-   inductives =
-       [ d | d <- map (fmap goInductiveDef) (toList (b ^. A.moduleInductives))]
-   functions :: [Indexed FunctionDef]
-   functions  =
-      [ f | f <- map (fmap goFunctionDef) (toList (b ^. A.moduleFunctions))]
-   foreigns :: [Indexed ForeignBlock]
-   foreigns = b ^. A.moduleForeigns
+goModuleBody b = ModuleBody (map goStatement (b ^. A.moduleStatements))
 
-
--- <> mconcatMap goImport (b ^. A.moduleImports)
+goStatement :: A.Statement -> Statement
+goStatement = \case
+  A.StatementAxiom d -> StatementAxiom (goAxiomDef d)
+  A.StatementForeign f -> StatementForeign f
+  A.StatementFunction f -> StatementFunction (goFunctionDef f)
+  A.StatementImport {} -> unsupported "imports"
+  A.StatementLocalModule {} -> unsupported "local modules"
+  A.StatementInductive i -> StatementInductive (goInductiveDef i)
 
 goTypeIden :: A.Iden -> TypeIden
 goTypeIden i = case i of
@@ -65,7 +51,14 @@ goTypeIden i = case i of
   A.IdenConstructor {} -> unsupported "constructors in types"
   A.IdenVar {} -> unsupported "type variables"
   A.IdenInductive d -> TypeIdenInductive (goName (d ^. A.inductiveRefName))
-  A.IdenAxiom {} -> unsupported "axioms in types"
+  A.IdenAxiom a -> TypeIdenAxiom (goName (a ^. A.axiomRefName))
+
+goAxiomDef :: A.AxiomDef -> AxiomDef
+goAxiomDef a =
+  AxiomDef {
+  _axiomName = goSymbol (a ^. A.axiomName),
+  _axiomType = goType (a ^. A.axiomType),
+  _axiomBackendItems = a ^. A.axiomBackendItems }
 
 goFunctionParameter :: A.FunctionParameter -> Type
 goFunctionParameter f = case f ^. A.paramName of
@@ -81,7 +74,7 @@ goFunctionDef :: A.FunctionDef -> FunctionDef
 goFunctionDef f =
   FunctionDef
     { _funDefName = goSymbol (f ^. A.funDefName),
-      _funDefTypeSig = goType (f ^. A.funDefTypeSig),
+      _funDefType = goType (f ^. A.funDefTypeSig),
       _funDefClauses = fmap goFunctionClause (f ^. A.funDefClauses)
     }
 
@@ -105,10 +98,15 @@ goConstructorApp c =
     (goName (c ^. A.constrAppConstructor . A.constructorRefName))
     (map goPattern (c ^. A.constrAppParameters))
 
+goTypeUniverse :: Universe -> Type
+goTypeUniverse u
+ | 0 == fromMaybe 0 (u ^. universeLevel) = TypeUniverse
+ | otherwise = unsupported "big universes"
+
 goType :: A.Expression -> Type
 goType e = case e of
   A.ExpressionIden i -> TypeIden (goTypeIden i)
-  A.ExpressionUniverse {} -> unsupported "universes in types"
+  A.ExpressionUniverse u -> goTypeUniverse u
   A.ExpressionApplication {} -> unsupported "application in types"
   A.ExpressionFunction f -> TypeFunction (goFunction f)
   A.ExpressionLiteral {} -> unsupported "literals in types"
@@ -121,7 +119,7 @@ goIden i = case i of
   A.IdenFunction n -> IdenFunction (goName (n ^. A.functionRefName))
   A.IdenConstructor c -> IdenConstructor (goName (c ^. A.constructorRefName))
   A.IdenVar v -> IdenVar (goSymbol v)
-  A.IdenAxiom {} -> unsupported "axiom identifier"
+  A.IdenAxiom a -> IdenAxiom (goName (a ^. A.axiomRefName))
   A.IdenInductive {} -> unsupported "inductive identifier"
 
 goExpression :: A.Expression -> Expression
@@ -130,7 +128,7 @@ goExpression e = case e of
   A.ExpressionUniverse {} -> unsupported "universes in expression"
   A.ExpressionFunction {} -> unsupported "function type in expressions"
   A.ExpressionApplication a -> ExpressionApplication (goApplication a)
-  A.ExpressionLiteral {} -> unsupported "literals in expression"
+  A.ExpressionLiteral l -> ExpressionLiteral l
 
 goInductiveDef :: A.InductiveDef -> InductiveDef
 goInductiveDef i = case i ^. A.inductiveType of
@@ -157,7 +155,7 @@ viewExpressionFunctionType e = case e of
   A.ExpressionFunction f -> first toList (viewFunctionType f)
   A.ExpressionIden i -> ([], TypeIden (goTypeIden i))
   A.ExpressionApplication {} -> unsupported "application in a type"
-  A.ExpressionUniverse {} -> unsupported "universe in a type"
+  A.ExpressionUniverse {} -> ([], TypeUniverse)
   A.ExpressionLiteral {} -> unsupported "literal in a type"
 
 viewFunctionType :: A.Function -> (NonEmpty Type, Type)

src/MiniJuvix/Translation/MicroJuvixToMiniHaskell.hs

@@ -0,0 +1,196 @@
+module MiniJuvix.Translation.MicroJuvixToMiniHaskell where
+import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Prelude
+import qualified MiniJuvix.Syntax.MiniHaskell.Language as H
+import MiniJuvix.Syntax.MicroJuvix.InfoTable
+import MiniJuvix.Syntax.ForeignBlock
+import MiniJuvix.Syntax.Backends
+import MiniJuvix.Syntax.NameId
+import Prettyprinter
+import qualified Data.Text as Text
+
+translateModule :: Module -> Either Err H.Module
+translateModule m = run (runError (runReader table (goModule m)))
+  where
+  table = buildTable m
+
+type Err = Text
+
+goModule :: Members '[Error Err, Reader InfoTable] r => Module -> Sem r H.Module
+goModule Module {..} = do
+  _moduleBody' <- goModuleBody _moduleBody
+  return H.Module {
+    _moduleName = goName (_moduleName),
+    _moduleBody = _moduleBody'
+    }
+
+unsupported :: Text -> a
+unsupported msg = error $ msg <> " not yet supported"
+
+goModuleBody :: Members '[Error Err, Reader InfoTable] r =>
+  ModuleBody -> Sem r H.ModuleBody
+goModuleBody ModuleBody {..} =
+  H.ModuleBody <$> mapMaybeM goStatement _moduleStatements
+
+goStatement :: Members '[Error Err, Reader InfoTable] r => Statement -> Sem r (Maybe H.Statement)
+goStatement = \case
+  StatementInductive d -> Just . H.StatementInductive <$> goInductive d
+  StatementFunction d -> Just . H.StatementFunction <$> goFunctionDef d
+  StatementForeign d -> return (goForeign d)
+  StatementAxiom {} -> return Nothing
+
+goForeign :: ForeignBlock -> Maybe H.Statement
+goForeign b = case b ^. foreignBackend of
+  BackendGhc -> Just (H.StatementVerbatim (b ^. foreignCode))
+  _ -> Nothing
+
+lookupAxiom :: Members '[Error Err, Reader InfoTable] r => Name -> Sem r AxiomInfo
+lookupAxiom n =
+  fromMaybe impossible . (^. infoAxioms . at n) <$> ask
+
+goIden :: Members '[Error Err, Reader InfoTable] r => Iden -> Sem r H.Expression
+goIden = \case
+  IdenFunction fun -> return (goName' fun)
+  IdenConstructor c -> return (goName' c)
+  IdenVar v -> return (goName' v)
+  IdenAxiom a -> H.ExpressionVerbatim <$> goAxiomIden a
+
+throwErr :: Member (Error Err) r => Text -> Sem r a
+throwErr = throw
+
+goAxiomIden :: Members '[Error Err, Reader InfoTable] r => Name -> Sem r Text
+goAxiomIden n = do
+  backends <- (^. axiomInfoBackends) <$> lookupAxiom n
+  case firstJust getCode backends of
+    Nothing -> throwErr ("ghc does not support this primitive:" <> show (pretty n))
+    Just t -> return t
+  where
+  getCode :: BackendItem -> Maybe Text
+  getCode b =
+    guard (BackendGhc == b ^. backendItemBackend)
+    $> b ^. backendItemCode
+
+goName' :: Name -> H.Expression
+goName' = H.ExpressionIden . goName
+
+goName :: Name -> H.Name
+goName n = H.Name {
+  _nameText = goNameText n,
+  _nameKind = n ^. nameKind
+  }
+
+goNameText :: Name -> Text
+goNameText n =
+  adaptFirstLetter lexeme <> "_" <> show (n ^. nameId . unNameId)
+  where
+  lexeme
+    | Text.null lexeme' = "v"
+    | otherwise = lexeme'
+    where
+    lexeme' = Text.filter isValidChar (n ^. nameText)
+  isValidChar :: Char -> Bool
+  isValidChar c = isLetter c && isAscii c
+  adaptFirstLetter :: Text -> Text
+  adaptFirstLetter t = case Text.uncons t of
+    Nothing -> impossible
+    Just (h, r) -> Text.cons (capitalize h) r
+    where
+    capitalize :: Char -> Char
+    capitalize
+      | capital = toUpper
+      | otherwise = toLower
+    capital = case n ^. nameKind of
+      KNameConstructor -> True
+      KNameInductive -> True
+      KNameTopModule -> True
+      KNameLocalModule -> True
+      _ -> False
+
+goFunctionDef :: Members '[Error Err, Reader InfoTable] r => FunctionDef -> Sem r H.FunctionDef
+goFunctionDef FunctionDef {..} = do
+  _funDefType' <- goType _funDefType
+  _funDefClauses' <- mapM goFunctionClause _funDefClauses
+  return H.FunctionDef {
+    _funDefName = goName _funDefName,
+    _funDefType = _funDefType',
+    _funDefClauses = _funDefClauses'
+    }
+
+goPattern :: Pattern -> H.Pattern
+goPattern = \case
+  PatternVariable v -> H.PatternVariable (goName v)
+  PatternConstructorApp a -> H.PatternConstructorApp (goConstructorApp a)
+  PatternWildcard -> H.PatternWildcard
+
+goConstructorApp :: ConstructorApp -> H.ConstructorApp
+goConstructorApp c = H.ConstructorApp {
+  _constrAppConstructor = goName (c ^. constrAppConstructor),
+  _constrAppParameters = map goPattern (c ^. constrAppParameters)
+  }
+
+goExpression :: Members '[Error Err, Reader InfoTable] r =>
+  Expression -> Sem r H.Expression
+goExpression = \case
+  ExpressionIden i -> goIden i
+  ExpressionTyped t -> goExpression (t ^. typedExpression)
+  ExpressionApplication a -> H.ExpressionApplication <$> goApplication a
+  ExpressionLiteral l -> return (H.ExpressionLiteral l)
+
+goApplication :: Members '[Error Err, Reader InfoTable] r =>
+  Application -> Sem r H.Application
+goApplication Application {..} = do
+  _appLeft' <- goExpression _appLeft
+  _appRight' <- goExpression _appRight
+  return H.Application {
+    _appLeft = _appLeft',
+    _appRight = _appRight'
+    }
+
+goFunctionClause :: Members '[Error Err, Reader InfoTable] r =>
+ FunctionClause -> Sem r H.FunctionClause
+goFunctionClause FunctionClause {..} = do
+  _clauseBody' <- goExpression _clauseBody
+  let _clausePatterns' = map goPattern _clausePatterns
+  return H.FunctionClause {
+    _clauseBody = _clauseBody',
+    _clausePatterns = _clausePatterns'
+    }
+
+goInductive :: Members '[Error Err, Reader InfoTable] r =>
+  InductiveDef -> Sem r H.InductiveDef
+goInductive InductiveDef {..} = do
+  _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors
+  return H.InductiveDef {
+    _inductiveName = goName _inductiveName,
+    _inductiveConstructors = _inductiveConstructors'
+    }
+
+goConstructorDef :: Members '[Error Err, Reader InfoTable] r =>
+  InductiveConstructorDef -> Sem r H.InductiveConstructorDef
+goConstructorDef InductiveConstructorDef {..} = do
+  _constructorParameters' <- mapM goType _constructorParameters
+  return H.InductiveConstructorDef {
+    _constructorName = goName _constructorName,
+    _constructorParameters = _constructorParameters'
+    }
+
+goFunction :: Members '[Error Err, Reader InfoTable] r => Function -> Sem r H.Function
+goFunction Function {..} = do
+  _funLeft' <- goType _funLeft
+  _funRight' <- goType _funRight
+  return H.Function {
+    _funLeft = _funLeft',
+    _funRight = _funRight'
+    }
+
+goTypeIden :: Members '[Error Err, Reader InfoTable] r => TypeIden -> Sem r H.Type
+goTypeIden = \case
+  TypeIdenInductive n -> return (H.TypeIden (H.TypeIdenInductive (goName n)))
+  TypeIdenAxiom n -> H.TypeVerbatim <$> goAxiomIden n
+
+goType :: Members '[Error Err, Reader InfoTable] r => Type -> Sem r H.Type
+goType = \case
+  TypeIden t -> goTypeIden t
+  TypeFunction f -> H.TypeFunction <$> goFunction f
+  TypeUniverse -> throwErr "MiniHaskell: universes in types not supported"
+  TypeAny -> impossible

src/MiniJuvix/Translation/ScopedToAbstract.hs

@@ -1,6 +1,5 @@
 module MiniJuvix.Translation.ScopedToAbstract where
 
-import qualified Data.HashMap.Strict as HashMap
 import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Abstract.Language as A
 import MiniJuvix.Syntax.Concrete.Language
@@ -12,7 +11,7 @@ import MiniJuvix.Syntax.Abstract.Language (FunctionDef(_funDefTypeSig))
 type Err = Text
 
 unsupported :: Members '[Error Err] r => Err -> Sem r a
-unsupported msg = throw $ msg <> " not yet supported"
+unsupported msg = throw $ msg <> "Scoped to Abstract: not yet supported"
 
 translateModule :: Module 'Scoped 'ModuleTop -> Either Err (InfoTable, A.TopModule)
 translateModule = run . runError . runInfoTableBuilder . goTopModule
@@ -28,62 +27,49 @@ goModule (Module n par b) = case par of
   [] -> A.Module n <$> goModuleBody b
   _ -> unsupported "Module parameters"
 
-goModuleBody :: forall r. Members '[Error Err, InfoTableBuilder] r => [Statement 'Scoped] -> Sem r A.ModuleBody
+goModuleBody :: forall r. Members '[Error Err, InfoTableBuilder] r
+  => [Statement 'Scoped] -> Sem r A.ModuleBody
 goModuleBody ss' = do
-  _moduleInductives <- inductives
-  _moduleLocalModules <- locals
-  _moduleFunctions <- functions
-  _moduleImports <- imports
-  _moduleForeigns <- foreigns
+  otherThanFunctions <- mapMaybeM goStatement ss
+  functions <- map (fmap A.StatementFunction) <$> compiledFunctions
+  let _moduleStatements = map (^. indexedThing) (sortOn (^. indexedIx)
+                          (otherThanFunctions <> functions))
   return A.ModuleBody {..}
   where
     ss :: [Indexed (Statement 'Scoped)]
     ss = zipWith Indexed [0 ..] ss'
-    inductives :: Sem r (HashMap A.InductiveName (Indexed A.InductiveDef))
-    inductives =
+    compiledFunctions :: Sem r [Indexed A.FunctionDef]
+    compiledFunctions =
       sequence $
-        HashMap.fromList
-          [ (def ^. inductiveName, Indexed i <$> goInductive def)
-            | Indexed i (StatementInductive def) <- ss
-          ]
-    locals :: Sem r (HashMap A.InductiveName (Indexed A.LocalModule))
-    locals =
-      sequence $
-        HashMap.fromList
-          [ (m ^. modulePath, Indexed i <$> goLocalModule m)
-            | Indexed i (StatementModule m) <- ss
-          ]
-    foreigns :: Sem r [Indexed ForeignBlock]
-    foreigns =
-      return
-        [ Indexed i f
-          | Indexed i (StatementForeign f) <- ss
-        ]
-    imports :: Sem r [Indexed A.TopModule]
-    imports =
-      sequence $
-        [ Indexed i <$> goModule m
-          | Indexed i (StatementImport (Import m)) <- ss
-        ]
-    functions :: Sem r (HashMap A.FunctionName (Indexed A.FunctionDef))
-    functions = do
-      sequence $
-        HashMap.fromList
-          [ (name, Indexed i <$> funDef)
+          [ Indexed i <$> funDef
             | Indexed i sig <- sigs,
               let name = sig ^. sigName,
-              let funDef = goFunctionDef sig (getClauses name)
-          ]
+              let funDef = goFunctionDef sig (getClauses name) ]
       where
         getClauses :: S.Symbol -> NonEmpty (FunctionClause 'Scoped)
         getClauses name =
           fromMaybe impossible $
             nonEmpty
-              [ c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction
-              ]
+              [ c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction ]
         sigs :: [Indexed (TypeSignature 'Scoped)]
         sigs = [Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss]
 
+goStatement :: forall r. Members '[Error Err, InfoTableBuilder] r
+   => Indexed (Statement 'Scoped) -> Sem r (Maybe (Indexed A.Statement))
+goStatement (Indexed idx s) = fmap (Indexed idx) <$> case s of
+  StatementAxiom d -> Just . A.StatementAxiom <$> goAxiom d
+  StatementImport (Import t) -> Just . A.StatementImport <$> goModule t
+  StatementOperator {} -> return Nothing
+  StatementOpenModule {} -> return Nothing
+  StatementEval {} -> unsupported "eval statements"
+  StatementPrint {} -> unsupported "print statements"
+  StatementInductive i -> Just . A.StatementInductive <$> goInductive i
+  StatementForeign f -> return (Just (A.StatementForeign f))
+  StatementModule f -> Just . A.StatementLocalModule <$> goLocalModule f
+  StatementTypeSignature {} -> return Nothing
+  StatementFunctionClause {} -> return Nothing
+
+
 goFunctionDef :: forall r. Members '[Error Err, InfoTableBuilder] r => TypeSignature 'Scoped -> NonEmpty (FunctionClause 'Scoped) -> Sem r A.FunctionDef
 goFunctionDef sig clauses = do
   let _funDefName = sig ^. sigName

tests/positive/MiniHaskell/HelloWorld.mjuvix

@@ -0,0 +1,49 @@
+module HelloWorld;
+
+inductive ℕ {
+  zero : ℕ;
+  suc : ℕ → ℕ;
+};
+
+inductive V {
+  zeroV : V;
+  sucV : V;
+};
+
+
+infixl 6 +;
++ : ℕ → ℕ → ℕ;
++ zero b ≔ b;
++ (suc a) b ≔ suc (a + b);
+
+infixl 7 *;
+* : ℕ → ℕ → ℕ;
+* zero b ≔ zero;
+* (suc a) b ≔ b + (a * b);
+
+axiom Action : Type {
+ ghc ↦ "IO ()";
+};
+
+infixl 1 >>;
+axiom >> : Action → Action → Action {
+  ghc ↦ "(>>)";
+};
+
+axiom String : Type;
+
+axiom putStr : String → Action {
+  ghc ↦ "putStrLn";
+};
+
+doTimes : ℕ → Action → Action;
+doTimes zero _ ≔ putStr "done";
+doTimes (suc n) a ≔ a >> doTimes n a;
+
+three : ℕ;
+three ≔ suc (suc (suc zero));
+
+main : Action;
+main := doTimes three (putStr "hello world");
+
+end;