separate MiniHaskell into MicroJuvix and 'new' MiniHaskell

app/Commands/MicroJuvix.hs

@@ -0,0 +1,15 @@
+{-# LANGUAGE ApplicativeDo #-}
+module Commands.MicroJuvix where
+
+import Commands.Extra
+import Options.Applicative
+import MiniJuvix.Prelude hiding (Doc)
+
+newtype MicroJuvixOptions = MicroJuvixOptions
+  { _mjuvixInputFile :: FilePath
+  }
+
+parseMicroJuvix :: Parser MicroJuvixOptions
+parseMicroJuvix = do
+  _mjuvixInputFile <- parseInputFile
+  pure MicroJuvixOptions {..}

app/Commands/MiniHaskell.hs

@@ -5,7 +5,7 @@ import Commands.Extra
 import Options.Applicative
 import MiniJuvix.Prelude hiding (Doc)
 
-data MiniHaskellOptions = MiniHaskellOptions
+newtype MiniHaskellOptions = MiniHaskellOptions
   { _mhaskellInputFile :: FilePath
   }
 

app/Main.hs

@@ -6,9 +6,10 @@ import qualified MiniJuvix.Syntax.Concrete.Language as M
 import qualified MiniJuvix.Syntax.Concrete.Parser as M
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Ansi as M
 import qualified MiniJuvix.Syntax.MiniHaskell.Pretty.Ansi as H
+import qualified MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi as Micro
 import qualified MiniJuvix.Termination as T
 import qualified MiniJuvix.Translation.ScopedToAbstract as A
-import qualified MiniJuvix.Translation.AbstractToMiniHaskell as H
+import qualified MiniJuvix.Translation.AbstractToMicroJuvix as Micro
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Pretty.Base as M
 import qualified MiniJuvix.Termination.CallGraph as A
 import qualified MiniJuvix.Syntax.Abstract.Pretty.Base as A
@@ -23,6 +24,7 @@ import qualified MiniJuvix.Syntax.Abstract.Pretty.Ansi as A
 import Commands.Extra
 import Commands.Termination as T
 import Commands.MiniHaskell
+import Commands.MicroJuvix
 
 data Command
   = Scope ScopeOptions
@@ -30,6 +32,7 @@ data Command
   | Html HtmlOptions
   | Termination TerminationCommand
   | MiniHaskell MiniHaskellOptions
+  | MicroJuvix MicroJuvixOptions
 
 data ScopeOptions = ScopeOptions
   { _scopeRootDir :: FilePath,
@@ -135,9 +138,19 @@ parseCommand =
         commandScope,
         commandHtml,
         commandTermination,
+        commandMicroJuvix,
         commandMiniHaskell
       ]
   where
+    commandMicroJuvix :: Mod CommandFields Command
+    commandMicroJuvix = command "microjuvix" minfo
+      where
+        minfo :: ParserInfo Command
+        minfo =
+          info
+            (MicroJuvix <$> parseMicroJuvix)
+            (progDesc "Translate a .mjuvix file to MicroJuvix")
+
     commandMiniHaskell :: Mod CommandFields Command
     commandMiniHaskell = command "minihaskell" minfo
       where
@@ -217,12 +230,20 @@ go c = do
       m <- parseModuleIO _htmlInputFile
       s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       genHtml defaultOptions _htmlRecursive _htmlTheme s
+    MicroJuvix MicroJuvixOptions {..} -> do
+      m <- parseModuleIO _mjuvixInputFile
+      s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
+      a <- fromRightIO' putStrLn (return $ A.translateModule s)
+      let mini = Micro.translateModule a
+      Micro.printPrettyCodeDefault mini
     MiniHaskell MiniHaskellOptions {..} -> do
       m <- parseModuleIO _mhaskellInputFile
       s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m
       a <- fromRightIO' putStrLn (return $ A.translateModule s)
-      let mini = H.translateModule a
-      H.printPrettyCodeDefault mini
+      -- let mini = Micro.translateModule a
+      -- Micro.printPrettyCodeDefault mini
+      -- TODO
+      error "todo"
     Termination (Calls opts@CallsOptions {..}) -> do
       m <- parseModuleIO _callsInputFile
       s <- fromRightIO' printErrorAnsi $ M.scopeCheck1IO root m

package.yaml

@@ -62,8 +62,10 @@ ghc-options:
 
 default-extensions:
 - DataKinds
+- DeriveFoldable
 - DeriveGeneric
 - DeriveLift
+- DeriveTraversable
 - DerivingStrategies
 - FlexibleContexts
 - FlexibleInstances

src/MiniJuvix/Prelude/Base.hs

@@ -215,3 +215,14 @@ infixl 7 <+?>
 infixl 7 <?>
 (<?>) :: Semigroup m => m -> Maybe m -> m
 (<?>) a = maybe a (a <>)
+
+data Indexed a = Indexed {
+  _indexedIx :: Int,
+  _indexedThing :: a
+  }
+  deriving stock (Show, Eq, Ord, Foldable, Traversable)
+
+instance Functor Indexed where
+  fmap f (Indexed i a) = Indexed i (f a)
+
+makeLenses ''Indexed

src/MiniJuvix/Syntax/Abstract/Language.hs

@@ -5,7 +5,7 @@ module MiniJuvix.Syntax.Abstract.Language
 where
 
 import MiniJuvix.Prelude
-import MiniJuvix.Syntax.Concrete.Language (Usage, Literal(..))
+import MiniJuvix.Syntax.Concrete.Language (Usage, Literal(..), ForeignBlock(..))
 import qualified MiniJuvix.Syntax.Concrete.Name as C
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import MiniJuvix.Syntax.Fixity
@@ -38,10 +38,11 @@ data Module s = Module
   deriving stock (Show, Eq)
 
 data ModuleBody = ModuleBody
-  { _moduleInductives :: HashMap InductiveName InductiveDef,
-    _moduleFunctions :: HashMap FunctionName FunctionDef,
-    _moduleImports :: [TopModule],
-    _moduleLocalModules :: HashMap LocalModuleName LocalModule
+  { _moduleInductives :: HashMap InductiveName (Indexed InductiveDef),
+    _moduleFunctions :: HashMap FunctionName (Indexed FunctionDef),
+    _moduleImports :: [Indexed TopModule],
+    _moduleForeign :: [Indexed ForeignBlock],
+    _moduleLocalModules :: HashMap LocalModuleName (Indexed LocalModule)
   }
   deriving stock (Show, Eq)
 

src/MiniJuvix/Syntax/MicroJuvix/Language.hs

@@ -0,0 +1,155 @@
+module MiniJuvix.Syntax.MicroJuvix.Language (
+  module MiniJuvix.Syntax.MicroJuvix.Language,
+  module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
+  module MiniJuvix.Syntax.Concrete.Scoped.Name
+   ) where
+
+import MiniJuvix.Prelude
+import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
+import MiniJuvix.Syntax.Concrete.Language (ForeignBlock(..))
+import MiniJuvix.Syntax.Concrete.Scoped.Name (NameId(..))
+import MiniJuvix.Syntax.Fixity
+
+type FunctionName = Name
+type VarName = Name
+type ConstrName = Name
+type InductiveName = Name
+
+data Name = Name {
+    _nameText :: Text,
+    _nameId :: NameId,
+    _nameKind :: NameKind
+    }
+makeLenses ''Name
+
+instance Eq Name where
+  (==) = (==) `on` _nameId
+
+instance Ord Name where
+  compare = compare `on` _nameId
+
+instance Hashable Name where
+  hashWithSalt salt = hashWithSalt salt . _nameId
+
+instance HasNameKind Name where
+  getNameKind = _nameKind
+
+data Module = Module
+  { _moduleName :: Name,
+    _moduleBody :: ModuleBody
+  }
+
+data ModuleBody = ModuleBody {
+  _moduleInductives :: HashMap InductiveName (Indexed InductiveDef),
+  _moduleFunctions :: HashMap FunctionName (Indexed FunctionDef),
+  _moduleForeign :: [Indexed ForeignBlock]
+  }
+
+data FunctionDef = FunctionDef {
+   _funDefName :: FunctionName,
+   _funDefTypeSig :: Type,
+   _funDefClauses :: NonEmpty FunctionClause
+  }
+
+data FunctionClause = FunctionClause {
+    _clausePatterns :: [Pattern],
+    _clauseBody :: Expression
+  }
+
+data Iden =
+  IdenDefined Name
+  | IdenConstructor Name
+  | IdenVar VarName
+
+data Expression
+  = ExpressionIden Iden
+  | ExpressionApplication Application
+
+data Application = Application {
+  _appLeft :: Expression,
+  _appRight :: Expression
+  }
+
+data Function = Function {
+  _funLeft :: Type,
+  _funRight :: Type
+  }
+
+-- | Fully applied constructor in a pattern.
+data ConstructorApp = ConstructorApp {
+  _constrAppConstructor :: Name,
+  _constrAppParameters :: [Pattern]
+  }
+
+data Pattern
+  = PatternVariable VarName
+  | PatternConstructorApp ConstructorApp
+  | PatternWildcard
+
+data InductiveDef = InductiveDef
+  { _inductiveName :: InductiveName,
+    _inductiveConstructors :: [InductiveConstructorDef]
+  }
+
+data InductiveConstructorDef = InductiveConstructorDef
+  { _constructorName :: ConstrName,
+    _constructorParameters :: [Type]
+  }
+
+newtype TypeIden =
+  TypeIdenInductive InductiveName
+
+data Type =
+  TypeIden TypeIden
+ | TypeFunction Function
+
+makeLenses ''Module
+makeLenses ''Function
+makeLenses ''FunctionDef
+makeLenses ''FunctionClause
+makeLenses ''InductiveDef
+makeLenses ''ModuleBody
+makeLenses ''Application
+makeLenses ''InductiveConstructorDef
+makeLenses ''ConstructorApp
+
+instance Semigroup ModuleBody where
+  a <> b = ModuleBody {
+    _moduleInductives = a ^. moduleInductives <> b ^. moduleInductives,
+    _moduleFunctions = a ^. moduleFunctions <> b ^. moduleFunctions,
+    _moduleForeign = a ^. moduleForeign <> b ^. moduleForeign
+    }
+
+instance Monoid ModuleBody where
+  mempty = ModuleBody {
+    _moduleInductives = mempty,
+    _moduleForeign = mempty,
+    _moduleFunctions = mempty
+    }
+
+instance HasAtomicity Application where
+  atomicity = const (Aggregate appFixity)
+
+instance HasAtomicity Expression where
+  atomicity e = case e of
+    ExpressionIden {} -> Atom
+    ExpressionApplication a -> atomicity a
+
+instance HasAtomicity Function where
+  atomicity = const (Aggregate funFixity)
+
+instance HasAtomicity Type where
+  atomicity t = case t of
+    TypeIden {} -> Atom
+    TypeFunction f -> atomicity f
+
+instance HasAtomicity ConstructorApp where
+  atomicity (ConstructorApp _ args)
+   | null args = Atom
+   | otherwise = Aggregate appFixity
+
+instance HasAtomicity Pattern where
+  atomicity p = case p of
+    PatternConstructorApp a -> atomicity a
+    PatternVariable {} -> Atom
+    PatternWildcard {} -> Atom

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

@@ -0,0 +1,9 @@
+module MiniJuvix.Syntax.MicroJuvix.Pretty.Ann where
+
+import MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind
+
+data Ann =
+  AnnKind NameKind
+  | AnnKeyword
+  | AnnLiteralString
+  | AnnLiteralInteger

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

@@ -0,0 +1,31 @@
+module MiniJuvix.Syntax.MicroJuvix.Pretty.Ansi where
+
+import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Base
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
+import MiniJuvix.Prelude
+import Prettyprinter
+import Prettyprinter.Render.Terminal
+
+printPrettyCodeDefault :: PrettyCode c => c -> IO ()
+printPrettyCodeDefault = printPrettyCode defaultOptions
+
+printPrettyCode :: PrettyCode c => Options -> c -> IO ()
+printPrettyCode = hPrintPrettyCode stdout
+
+hPrintPrettyCode :: PrettyCode c => Handle -> Options -> c -> IO ()
+hPrintPrettyCode h opts = renderIO h . docStream opts
+
+renderPrettyCode :: PrettyCode c => Options -> c -> Text
+renderPrettyCode opts = renderStrict . docStream opts
+
+docStream :: PrettyCode c => Options -> c -> SimpleDocStream AnsiStyle
+docStream opts = reAnnotateS stylize . layoutPretty defaultLayoutOptions
+    . run . runReader opts . ppCode
+
+stylize :: Ann -> AnsiStyle
+stylize a = case a of
+  AnnKind k -> nameKindAnsi k
+  AnnKeyword -> colorDull Blue
+  AnnLiteralString -> colorDull Red
+  AnnLiteralInteger -> colorDull Cyan

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

@@ -0,0 +1,180 @@
+-- TODO handle capital letters and characters not supported by Haskell.
+module MiniJuvix.Syntax.MicroJuvix.Pretty.Base where
+
+
+import MiniJuvix.Prelude
+import Prettyprinter
+import MiniJuvix.Syntax.Fixity
+import MiniJuvix.Syntax.MicroJuvix.Pretty.Ann
+import MiniJuvix.Syntax.MicroJuvix.Language
+import MiniJuvix.Syntax.Concrete.Language (ForeignBlock(..))
+import qualified MiniJuvix.Internal.Strings as Str
+
+newtype Options = Options
+  {
+    _optIndent :: Int
+  }
+
+defaultOptions :: Options
+defaultOptions = Options {
+  _optIndent = 2
+  }
+
+class PrettyCode c where
+  ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
+
+instance PrettyCode Name where
+  ppCode n =
+    return $ annotate (AnnKind (n ^. nameKind))
+           $ pretty (n ^. nameText) <> "_" <> pretty (n ^. nameId)
+
+instance PrettyCode Iden where
+  ppCode :: Member (Reader Options) r => Iden -> Sem r (Doc Ann)
+  ppCode i = case i of
+   IdenDefined na -> ppCode na
+   IdenConstructor na -> ppCode na
+   IdenVar na -> ppCode na
+
+instance PrettyCode Application where
+  ppCode a = do
+    l' <- ppLeftExpression appFixity (a ^. appLeft)
+    r' <- ppRightExpression appFixity (a ^. appRight)
+    return $ l' <+> r'
+
+instance PrettyCode Expression where
+  ppCode e = case e of
+    ExpressionIden i -> ppCode i
+    ExpressionApplication a -> ppCode a
+
+keyword :: Text -> Doc Ann
+keyword = annotate AnnKeyword . pretty
+
+kwArrow :: Doc Ann
+kwArrow = keyword Str.toAscii
+
+kwData :: Doc Ann
+kwData = keyword Str.data_
+
+kwEquals :: Doc Ann
+kwEquals = keyword Str.equal
+
+kwColonColon :: Doc Ann
+kwColonColon = keyword (Str.colon <> Str.colon)
+
+kwPipe :: Doc Ann
+kwPipe = keyword Str.pipe
+
+kwWhere :: Doc Ann
+kwWhere = keyword Str.where_
+
+kwModule :: Doc Ann
+kwModule = keyword Str.module_
+
+kwWildcard :: Doc Ann
+kwWildcard = keyword Str.underscore
+
+instance PrettyCode Function where
+  ppCode (Function l r) = do
+    l' <- ppLeftExpression funFixity l
+    r' <- ppRightExpression funFixity r
+    return $ l' <+> kwArrow <+> r'
+
+instance PrettyCode Type where
+  ppCode t = case t of
+    TypeIden (TypeIdenInductive n) -> ppCode n
+    TypeFunction f -> ppCode f
+
+instance PrettyCode InductiveConstructorDef where
+  ppCode c = do
+    constructorName' <- ppCode (c ^. constructorName)
+    constructorParameters' <- mapM ppCode (c ^. constructorParameters)
+    return (hsep $ constructorName' : constructorParameters')
+
+indent' :: Member (Reader Options) r => Doc a -> Sem r (Doc a)
+indent' d = do
+  i <- asks _optIndent
+  return $ indent i d
+
+instance PrettyCode InductiveDef where
+  ppCode d = do
+    inductiveName' <- ppCode (d ^. inductiveName)
+    inductiveConstructors' <- mapM ppCode (d ^. inductiveConstructors)
+    rhs <- indent' $ align $ concatWith (\a b -> a <> line <> kwPipe <+> b) inductiveConstructors'
+    return $ kwData <+> inductiveName' <+> kwEquals <> line <> rhs
+
+instance PrettyCode ConstructorApp where
+  ppCode c = do
+    constr' <- ppCode (c ^. constrAppConstructor)
+    params' <- mapM ppCodeAtom (c ^. constrAppParameters)
+    return $ hsep $ constr' : params'
+
+instance PrettyCode Pattern where
+  ppCode p = case p of
+    PatternVariable v -> ppCode v
+    PatternConstructorApp a -> ppCode a
+    PatternWildcard -> return kwWildcard
+
+instance PrettyCode FunctionDef where
+  ppCode f = do
+    funDefName' <- ppCode (f ^. funDefName)
+    funDefTypeSig' <- ppCode (f ^. funDefTypeSig)
+    clauses' <- mapM (ppClause funDefName') (f ^. funDefClauses)
+    return $ funDefName' <+> kwColonColon <+> funDefTypeSig' <> line
+      <> vsep (toList clauses')
+     where
+     ppClause fun c = do
+       clausePatterns' <- mapM ppCodeAtom (c ^. clausePatterns)
+       clauseBody' <- ppCode (c ^. clauseBody)
+       return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
+
+instance PrettyCode ForeignBlock where
+  ppCode ForeignBlock {..} = do
+    _foreignBackend' <- ppCode _foreignBackend
+    return $ kwForeign <+> _foreignBackend' <+> lbrace <> line
+        <> pretty _foreignCode <> line <> rbrace
+
+
+-- TODO Jonathan review
+instance PrettyCode ModuleBody where
+  ppCode m = do
+    types' <- mapM (mapM ppCode) (toList (m ^. moduleInductives))
+    funs' <- mapM (mapM ppCode) (toList (m ^. moduleFunctions))
+    let foreigns' = m ^. moduleForeign
+    let everything = map (^. indexedThing) (sortOn (^. indexedIx) (types' ++ funs'))
+    return $ vsep2 everything
+    where
+    vsep2 = concatWith (\a b -> a <> line <> line <> b)
+
+instance PrettyCode Module where
+  ppCode m = do
+    name' <- ppCode (m ^. moduleName)
+    body' <- ppCode (m ^. moduleBody)
+    return $ kwModule <+> name' <+> kwWhere
+      <> line <> line <> body' <> line
+
+parensCond :: Bool -> Doc Ann -> Doc Ann
+parensCond t d = if t then parens d else d
+
+ppPostExpression ::(PrettyCode a, HasAtomicity a, Member (Reader Options) r)  =>
+  Fixity -> a -> Sem r (Doc Ann)
+ppPostExpression = ppLRExpression isPostfixAssoc
+
+ppRightExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity -> a -> Sem r (Doc Ann)
+ppRightExpression = ppLRExpression isRightAssoc
+
+ppLeftExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity -> a -> Sem r (Doc Ann)
+ppLeftExpression = ppLRExpression isLeftAssoc
+
+ppLRExpression
+  :: (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
+     (Fixity -> Bool) -> Fixity -> a -> Sem r (Doc Ann)
+ppLRExpression associates fixlr e =
+  parensCond (atomParens associates (atomicity e) fixlr)
+      <$> ppCode e
+
+ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
+ppCodeAtom c = do
+  p' <- ppCode c
+  return $ if isAtomic c then p' else parens p'

src/MiniJuvix/Syntax/MiniHaskell/Language.hs

@@ -1,4 +1,3 @@
-{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
 module MiniJuvix.Syntax.MiniHaskell.Language (
   module MiniJuvix.Syntax.MiniHaskell.Language,
   module MiniJuvix.Syntax.Concrete.Scoped.Name.NameKind,
@@ -17,20 +16,10 @@ type InductiveName = Name
 
 data Name = Name {
     _nameText :: Text,
-    _nameId :: NameId,
     _nameKind :: NameKind
     }
 makeLenses ''Name
 
-instance Eq Name where
-  (==) = (==) `on` _nameId
-
-instance Ord Name where
-  compare = compare `on` _nameId
-
-instance Hashable Name where
-  hashWithSalt salt = hashWithSalt salt . _nameId
-
 instance HasNameKind Name where
   getNameKind = _nameKind
 
@@ -39,10 +28,14 @@ data Module = Module
     _moduleBody :: ModuleBody
   }
 
-data ModuleBody = ModuleBody {
-  _moduleInductives :: HashMap InductiveName InductiveDef,
-  _moduleFunctions :: HashMap FunctionName FunctionDef
+newtype ModuleBody = ModuleBody {
+  _moduleStatements :: [Statement]
   }
+  deriving newtype (Monoid, Semigroup)
+
+data Statement =
+  StatementInductiveDef InductiveDef
+  | StatementFunctionDef FunctionDef
 
 data FunctionDef = FunctionDef {
    _funDefName :: FunctionName,
@@ -55,10 +48,7 @@ data FunctionClause = FunctionClause {
     _clauseBody :: Expression
   }
 
-data Iden =
-  IdenDefined Name
-  | IdenConstructor Name
-  | IdenVar VarName
+type Iden = Name
 
 data Expression
   = ExpressionIden Iden
@@ -71,8 +61,8 @@ data Application = Application {
   }
 
 data Function = Function {
-  _funParameters :: NonEmpty Type,
-  _funReturn :: Type
+  _funLeft :: Type,
+  _funRight :: Type
   }
 
 -- | Fully applied constructor in a pattern.
@@ -96,8 +86,7 @@ data InductiveConstructorDef = InductiveConstructorDef
     _constructorParameters :: [Type]
   }
 
-newtype TypeIden =
-  TypeIdenInductive InductiveName
+type TypeIden = InductiveName
 
 data Type =
   TypeIden TypeIden
@@ -113,18 +102,6 @@ makeLenses ''Application
 makeLenses ''InductiveConstructorDef
 makeLenses ''ConstructorApp
 
-instance Semigroup ModuleBody where
-  a <> b = ModuleBody {
-    _moduleInductives = a ^. moduleInductives <> b ^. moduleInductives,
-    _moduleFunctions = a ^. moduleFunctions <> b ^. moduleFunctions
-    }
-
-instance Monoid ModuleBody where
-  mempty = ModuleBody {
-    _moduleInductives = mempty,
-    _moduleFunctions = mempty
-    }
-
 instance HasAtomicity Application where
   atomicity = const (Aggregate appFixity)
 

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

@@ -25,14 +25,7 @@ class PrettyCode c where
 instance PrettyCode Name where
   ppCode n =
     return $ annotate (AnnKind (n ^. nameKind))
-           $ pretty (n ^. nameText) <> "_" <> pretty (n ^. nameId)
-
-instance PrettyCode Iden where
-  ppCode :: Member (Reader Options) r => Iden -> Sem r (Doc Ann)
-  ppCode i = case i of
-   IdenDefined na -> ppCode na
-   IdenConstructor na -> ppCode na
-   IdenVar na -> ppCode na
+           $ pretty (n ^. nameText)
 
 instance PrettyCode Application where
   ppCode a = do
@@ -73,15 +66,14 @@ kwWildcard :: Doc Ann
 kwWildcard = keyword Str.underscore
 
 instance PrettyCode Function where
-  ppCode f = do
-    funParameters' <- mapM ppCode (f ^. funParameters)
-    funReturn' <- ppCodeAtom (f ^. funReturn)
-    return $ concatWith (\a b -> a <+> kwArrow <+> b)
-     (toList funParameters' ++ [funReturn'])
+  ppCode (Function l r) = do
+    l' <- ppLeftExpression funFixity l
+    r' <- ppRightExpression funFixity r
+    return $ l' <+> kwArrow <+> r'
 
 instance PrettyCode Type where
   ppCode t = case t of
-    TypeIden (TypeIdenInductive n) -> ppCode n
+    TypeIden n -> ppCode n
     TypeFunction f -> ppCode f
 
 instance PrettyCode InductiveConstructorDef where
@@ -127,11 +119,15 @@ instance PrettyCode FunctionDef where
        clauseBody' <- ppCode (c ^. clauseBody)
        return $ fun <+> hsep clausePatterns' <+> kwEquals <+> clauseBody'
 
+instance PrettyCode Statement where
+  ppCode = \case
+    StatementFunctionDef f -> ppCode f
+    StatementInductiveDef d -> ppCode d
+
 instance PrettyCode ModuleBody where
   ppCode m = do
-    types' <- mapM ppCode (toList (m ^. moduleInductives))
-    funs' <- mapM ppCode (toList (m ^. moduleFunctions))
-    return $ vsep2 types' <> line <> line <> vsep2 funs'
+    statements' <- mapM ppCode (m ^. moduleStatements)
+    return $ vsep2 statements'
     where
     vsep2 = concatWith (\a b -> a <> line <> line <> b)
 

src/MiniJuvix/Termination/CallMap.hs

@@ -81,8 +81,8 @@ checkModule m = checkModuleBody (m ^. moduleBody)
 
 checkModuleBody :: Members '[State CallMap] r => ModuleBody -> Sem r ()
 checkModuleBody body = do
-  mapM_ checkFunctionDef (toList $ body ^. moduleFunctions)
-  mapM_ checkLocalModule (toList $ body ^. moduleLocalModules)
+  mapM_ (checkFunctionDef . (^. indexedThing)) (toList $ body ^. moduleFunctions)
+  mapM_ (checkLocalModule . (^. indexedThing)) (toList $ body ^. moduleLocalModules)
 
 checkLocalModule :: Members '[State CallMap] r => LocalModule -> Sem r ()
 checkLocalModule m = checkModuleBody (m ^. moduleBody)

src/MiniJuvix/Translation/AbstractToMicroJuvix.hs

@@ -1,9 +1,9 @@
-module MiniJuvix.Translation.AbstractToMiniHaskell where
+module MiniJuvix.Translation.AbstractToMicroJuvix where
 
 import MiniJuvix.Prelude
 import qualified MiniJuvix.Syntax.Abstract.Language.Extra as A
 import qualified MiniJuvix.Syntax.Usage as A
-import MiniJuvix.Syntax.MiniHaskell.Language
+import MiniJuvix.Syntax.MicroJuvix.Language
 import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
 import qualified Data.HashMap.Strict as HashMap
 
@@ -37,12 +37,14 @@ goModuleBody b
  | not (HashMap.null (b ^. A.moduleLocalModules)) = unsupported "local modules"
  | otherwise = ModuleBody {
      _moduleInductives = HashMap.fromList
-       [ (d ^. inductiveName, d)
-        | d <- map goInductiveDef (toList (b ^. A.moduleInductives))],
+       [ (d ^. indexedThing . inductiveName, d)
+        | d <- map (fmap goInductiveDef) (toList (b ^. A.moduleInductives))],
      _moduleFunctions = HashMap.fromList
-        [ (f ^. funDefName, f) |
-          f <- map goFunctionDef (toList (b ^. A.moduleFunctions)) ]
-     } <> mconcatMap goImport (b ^. A.moduleImports)
+        [ (f ^. indexedThing . funDefName, f) |
+          f <- map (fmap goFunctionDef) (toList (b ^. A.moduleFunctions)) ],
+     _moduleForeign = b ^. A.moduleForeign
+     }
+     -- <> mconcatMap goImport (b ^. A.moduleImports)
 
 goTypeIden :: A.Iden -> TypeIden
 goTypeIden i = case i of
@@ -60,7 +62,7 @@ goFunctionParameter f = case f ^. A.paramName of
     _ -> unsupported "usages"
 
 goFunction :: A.Function -> Function
-goFunction = uncurry Function . viewFunctionType
+goFunction (A.Function l r) = Function (goFunctionParameter l) (goType r)
 
 goFunctionDef :: A.FunctionDef -> FunctionDef
 goFunctionDef f = FunctionDef {

src/MiniJuvix/Translation/ScopedToAbstract.hs

@@ -26,42 +26,48 @@ goModule (Module n par b) = case par of
   [] -> A.Module n <$> goModuleBody b
   _ -> unsupported "Module parameters"
 
--- | until we have modules with parameters, I think order of definitions is irrelevant
 goModuleBody :: forall r. Members '[Error Err] r => [Statement 'Scoped] -> Sem r A.ModuleBody
-goModuleBody ss = do
+goModuleBody ss' = do
   _moduleInductives <- inductives
   _moduleLocalModules <- locals
   _moduleFunctions <- functions
   _moduleImports <- imports
+  _moduleForeign <- foreigns
   return A.ModuleBody {..}
   where
-  inductives :: Sem r (HashMap A.InductiveName A.InductiveDef)
+  ss :: [Indexed (Statement 'Scoped)]
+  ss = zipWith Indexed [0 ..] ss'
+  inductives :: Sem r (HashMap A.InductiveName (Indexed A.InductiveDef))
   inductives = sequence $ HashMap.fromList
-    [ (def ^. inductiveName, goInductive def)
-    | StatementInductive def <- ss ]
-  locals :: Sem r (HashMap A.InductiveName A.LocalModule)
+    [ (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, goLocalModule m)
-    | StatementModule m <- ss ]
-  imports :: Sem r [A.TopModule]
+    [ (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 $
-    [ goModule m
-    | StatementImport (Import m) <- ss ]
-  functions :: Sem r (HashMap A.FunctionName A.FunctionDef)
+    [ 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, funDef)
-     | sig <- sigs,
+     [ (name, Indexed i <$> funDef)
+     | Indexed i sig <- sigs,
        let name = sig ^. sigName,
        let clauses = mapM goFunctionClause (getClauses name),
        let funDef = liftA2 (A.FunctionDef name) (goExpression (sig ^. sigType)) clauses ]
     where
     getClauses :: S.Symbol -> NonEmpty (FunctionClause 'Scoped)
     getClauses name = fromMaybe impossible $
-       nonEmpty [ c | StatementFunctionClause c <- ss,
+       nonEmpty [ c | StatementFunctionClause c <- ss',
                   name == c ^.clauseOwnerFunction ]
-    sigs :: [TypeSignature 'Scoped]
-    sigs = [ s | StatementTypeSignature s <- ss ]
+    sigs :: [Indexed (TypeSignature 'Scoped)]
+    sigs = [ Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss ]
 
 
 goFunctionClause :: forall r. Members '[Error Err] r => FunctionClause 'Scoped -> Sem r A.FunctionClause
@@ -110,6 +116,7 @@ goExpression e = case e of
   ExpressionApplication a -> A.ExpressionApplication <$> goApplication a
   ExpressionInfixApplication ia -> A.ExpressionApplication <$> goInfix ia
   ExpressionPostfixApplication pa -> A.ExpressionApplication <$> goPostfix pa
+  ExpressionLiteral l -> return $ A.ExpressionLiteral l
   ExpressionLambda {} -> unsupported "Lambda"
   ExpressionMatch {} -> unsupported "Match"
   ExpressionLetBlock {} -> unsupported "Let Block"

tests/positive/HelloWorld.mjuvix

@@ -24,7 +24,7 @@ axiom putStr : String -> Action;
 -- axiom to the given backend.
 compile Action ghc "IO ()";
 
-main : Action;
-main := putStr "hello world";
+-- main : Action;
+-- main := putStr "hello world";
 
 end;