Basic Geb integration (#1748)

This PR:

- Closes #1647 

It gives compilation errors for language features that require more
substantial support (recursion, polymorphism). The additional features
are to be implemented in future separate PRs.
* Adds a new target `geb` to the CLI command `juvix dev core compile`,
which produces a `*.geb` output file in the `.juvix-build` directory.
* Adds a few tests. These are not yet checked automatically because
there is no GEB evaluator; checking the `*.geb` output would be too
brittle.

app/Commands/Dev/Asm/Compile.hs

@@ -35,6 +35,7 @@ runCommand opts = do
       TargetWasm32Wasi -> Backend.TargetCWasm32Wasi
       TargetNative64 -> Backend.TargetCNative64
       TargetC -> Backend.TargetCWasm32Wasi
+      TargetGeb -> error "GEB target not supported for JuvixAsm"
 
 inputCFile :: (Members '[App] r) => Path Abs File -> Sem r (Path Abs File)
 inputCFile inputFileCompile = do

app/Commands/Dev/Core/Compile.hs

@@ -7,37 +7,65 @@ import Data.Text.IO qualified as TIO
 import Juvix.Compiler.Asm.Options qualified as Asm
 import Juvix.Compiler.Backend qualified as Backend
 import Juvix.Compiler.Backend.C qualified as C
+import Juvix.Compiler.Backend.Geb qualified as Geb
 import Juvix.Compiler.Core.Data.InfoTable qualified as Core
 import Juvix.Compiler.Core.Translation.FromSource qualified as Core
 
+data PipelineArg = PipelineArg
+  { _pipelineArgOptions :: CoreCompileOptions,
+    _pipelineArgFile :: Path Abs File,
+    _pipelineArgInfoTable :: Core.InfoTable
+  }
+
+makeLenses ''PipelineArg
+
 runCommand :: forall r. (Members '[Embed IO, App] r) => CoreCompileOptions -> Sem r ()
 runCommand opts = do
   file <- getFile
   s <- embed (readFile (toFilePath file))
   tab <- getRight (mapLeft JuvixError (Core.runParserMain file Core.emptyInfoTable s))
-  C.MiniCResult {..} <- getRight (run (runError (coreToMiniC asmOpts tab :: Sem '[Error JuvixError] C.MiniCResult)))
-  buildDir <- askBuildDir
-  ensureDir buildDir
-  cFile <- inputCFile file
-  embed $ TIO.writeFile (toFilePath cFile) _resultCCode
-  Compile.runCommand opts {_compileInputFile = AppPath (Abs cFile) False}
+  case opts ^. compileTarget of
+    TargetGeb -> runGebPipeline (PipelineArg opts file tab)
+    TargetWasm32Wasi -> runCPipeline (PipelineArg opts file tab)
+    TargetNative64 -> runCPipeline (PipelineArg opts file tab)
+    TargetC -> runCPipeline (PipelineArg opts file tab)
   where
     getFile :: Sem r (Path Abs File)
     getFile = someBaseToAbs' (opts ^. compileInputFile . pathPath)
 
+runCPipeline ::
+  forall r.
+  (Members '[Embed IO, App] r) =>
+  PipelineArg ->
+  Sem r ()
+runCPipeline PipelineArg {..} = do
+  C.MiniCResult {..} <- getRight (run (runError (coreToMiniC asmOpts _pipelineArgInfoTable :: Sem '[Error JuvixError] C.MiniCResult)))
+  cFile <- inputFile _pipelineArgFile ".c"
+  embed $ TIO.writeFile (toFilePath cFile) _resultCCode
+  Compile.runCommand _pipelineArgOptions {_compileInputFile = AppPath (Abs cFile) False}
+  where
     asmOpts :: Asm.Options
-    asmOpts = Asm.makeOptions (asmTarget (opts ^. compileTarget)) (opts ^. compileDebug)
+    asmOpts = Asm.makeOptions (asmTarget (_pipelineArgOptions ^. compileTarget)) (_pipelineArgOptions ^. compileDebug)
 
     asmTarget :: CompileTarget -> Backend.Target
     asmTarget = \case
       TargetWasm32Wasi -> Backend.TargetCWasm32Wasi
       TargetNative64 -> Backend.TargetCNative64
       TargetC -> Backend.TargetCWasm32Wasi
+      TargetGeb -> impossible
 
-inputCFile :: (Members '[App] r) => Path Abs File -> Sem r (Path Abs File)
-inputCFile inputFileCompile = do
+runGebPipeline ::
+  forall r.
+  (Members '[Embed IO, App] r) =>
+  PipelineArg ->
+  Sem r ()
+runGebPipeline PipelineArg {..} = do
+  Geb.Result {..} <- getRight (run (runError (coreToGeb _pipelineArgInfoTable :: Sem '[Error JuvixError] Geb.Result)))
+  gebFile <- inputFile _pipelineArgFile ".geb"
+  embed $ TIO.writeFile (toFilePath gebFile) _resultCode
+
+inputFile :: (Members '[Embed IO, App] r) => Path Abs File -> String -> Sem r (Path Abs File)
+inputFile inputFileCompile ext = do
   buildDir <- askBuildDir
-  return (buildDir <//> outputMiniCFile)
-  where
-    outputMiniCFile :: Path Rel File
-    outputMiniCFile = replaceExtension' ".c" (filename inputFileCompile)
+  ensureDir buildDir
+  return (buildDir <//> replaceExtension' ext (filename inputFileCompile))

app/Commands/Extra/Compile.hs

@@ -30,6 +30,7 @@ runCompile inputFile o = do
     TargetWasm32Wasi -> runError (clangWasmWasiCompile inputFile o)
     TargetNative64 -> runError (clangNativeCompile inputFile o)
     TargetC -> return $ Right ()
+    TargetGeb -> return $ Right ()
 
 prepareRuntime :: forall r. (Members '[App, Embed IO] r) => Path Abs Dir -> CompileOptions -> Sem r ()
 prepareRuntime buildDir o = do
@@ -40,6 +41,7 @@ prepareRuntime buildDir o = do
     TargetNative64 | o ^. compileDebug -> writeRuntime nativeDebugRuntime
     TargetNative64 -> writeRuntime nativeReleaseRuntime
     TargetC -> return ()
+    TargetGeb -> return ()
   where
     wasiReleaseRuntime :: BS.ByteString
     wasiReleaseRuntime = $(FE.makeRelativeToProject "runtime/_build.wasm32-wasi/libjuvix.a" >>= FE.embedFile)

app/Commands/Extra/Compile/Options.hs

@@ -6,6 +6,7 @@ data CompileTarget
   = TargetWasm32Wasi
   | TargetNative64
   | TargetC
+  | TargetGeb
   deriving stock (Show, Data)
 
 data CompileOptions = CompileOptions
@@ -54,13 +55,15 @@ optCompileTarget =
         <> metavar "TARGET"
         <> value TargetNative64
         <> showDefaultWith targetShow
-        <> help "select a target: wasm32-wasi, native, c"
+        <> help "select a target: wasm32-wasi, native, c, geb"
     )
   where
     parseTarget :: String -> Either String CompileTarget
     parseTarget = \case
       "wasm32-wasi" -> Right TargetWasm32Wasi
       "native" -> Right TargetNative64
+      "c" -> Right TargetC
+      "geb" -> Right TargetGeb
       s -> Left $ "unrecognised target: " <> s
 
     targetShow :: CompileTarget -> String
@@ -68,3 +71,4 @@ optCompileTarget =
       TargetWasm32Wasi -> "wasm32-wasi"
       TargetNative64 -> "native"
       TargetC -> "c"
+      TargetGeb -> "geb"

cntlines.sh

@@ -3,6 +3,7 @@
 RUNTIME=`find runtime/src/ -name '*.c' -or -name '*.h' | xargs wc -l | tail -1 | tr -d ' toal'`
 
 BACKENDC=`find src/Juvix/Compiler/Backend/C/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
+GEB=`find src/Juvix/Compiler/Backend/Geb/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
 REG=`find src/Juvix/Compiler/Reg/ -name '*.hs' -print | xargs wc -l | tail -1 | tr -d ' toal'`
 ASM=`find src/Juvix/Compiler/Asm/ -name '*.hs' -print | xargs wc -l | tail -1 | tr -d ' toal'`
 CORE=`find src/Juvix/Compiler/Core/ -name '*.hs' -print | xargs wc -l | tail -1 | tr -d ' toal'`
@@ -20,7 +21,7 @@ DATA=`find src/Juvix/Data/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
 PRELUDE=`find src/Juvix/Prelude/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
 
 FRONT=$((CONCRETE + ABSTRACT + INTERNAL + BUILTINS + PIPELINE))
-BACK=$((BACKENDC + REG + ASM + CORE))
+BACK=$((BACKENDC + GEB + REG + ASM + CORE))
 OTHER=$((APP + HTML + EXTRA + DATA + PRELUDE))
 
 echo "Front end: $FRONT LOC"
@@ -31,6 +32,7 @@ echo "   Builtins: $BUILTINS LOC"
 echo "   Pipeline: $PIPELINE LOC"
 echo "Middle and back end: $BACK LOC"
 echo "   C backend: $BACKENDC LOC"
+echo "   GEB backend: $GEB LOC"
 echo "   JuvixReg: $REG LOC"
 echo "   JuvixAsm: $ASM LOC"
 echo "   JuvixCore: $CORE LOC"

src/Juvix/Compiler/Asm/Pretty/Base.hs

@@ -26,9 +26,6 @@ doc opts =
 class PrettyCode c where
   ppCode :: (Member (Reader Options) r) => c -> Sem r (Doc Ann)
 
-runPrettyCode :: (PrettyCode c) => Options -> c -> Doc Ann
-runPrettyCode opts = run . runReader opts . ppCode
-
 wrapCore ::
   forall r' c.
   (Member (Reader Options) r') =>
@@ -373,9 +370,6 @@ instance PrettyCode InfoTable where
 {--------------------------------------------------------------------------------}
 {- helper functions -}
 
-parensIf :: Bool -> Doc Ann -> Doc Ann
-parensIf t = if t then parens else id
-
 braces' :: Doc Ann -> Doc Ann
 braces' d = braces (line <> indent' d <> line)
 

src/Juvix/Compiler/Backend/Geb.hs

@@ -0,0 +1,4 @@
+module Juvix.Compiler.Backend.Geb (module Juvix.Compiler.Backend.Geb.Language, module Juvix.Compiler.Backend.Geb.Translation) where
+
+import Juvix.Compiler.Backend.Geb.Language
+import Juvix.Compiler.Backend.Geb.Translation

src/Juvix/Compiler/Backend/Geb/Extra.hs

@@ -0,0 +1,10 @@
+module Juvix.Compiler.Backend.Geb.Extra where
+
+import Juvix.Compiler.Backend.Geb.Language
+
+-- | Destructs a product in a right-associative way, e.g., (a, (b, c)) is
+-- destructed to [a, b, c]
+destructProduct :: Object -> [Object]
+destructProduct = \case
+  ObjectProduct Product {..} -> _productLeft : destructProduct _productRight
+  x -> [x]

src/Juvix/Compiler/Backend/Geb/Language.hs

@@ -0,0 +1,137 @@
+module Juvix.Compiler.Backend.Geb.Language
+  ( module Juvix.Compiler.Backend.Geb.Language,
+    module Juvix.Prelude,
+  )
+where
+
+import Juvix.Prelude hiding (First, Product)
+
+{-
+  The following datatypes correspond to GEB types for terms
+  (https://github.com/anoma/geb/blob/main/src/specs/lambda.lisp) and types
+  (https://github.com/anoma/geb/blob/main/src/specs/geb.lisp).
+-}
+
+-- | Represents GEB's `case-on`. `_caseOn` is the value matched on of type
+-- `Dom`, `_caseLeft` has type `_caseLeftType -> _caseCodomainType` and
+-- `_caseRight` has type `_caseRightType -> _caseCodomainType`.
+data Case = Case
+  { _caseLeftType :: Object,
+    _caseRightType :: Object,
+    _caseCodomainType :: Object,
+    _caseOn :: Morphism,
+    _caseLeft :: Morphism,
+    _caseRight :: Morphism
+  }
+
+data Pair = Pair
+  { _pairLeftType :: Object,
+    _pairRightType :: Object,
+    _pairLeft :: Morphism,
+    _pairRight :: Morphism
+  }
+
+data First = First
+  { _firstLeftType :: Object,
+    _firstRightType :: Object,
+    _firstValue :: Morphism
+  }
+
+data Second = Second
+  { _secondLeftType :: Object,
+    _secondRightType :: Object,
+    _secondValue :: Morphism
+  }
+
+data Lambda = Lambda
+  { _lambdaVarType :: Object,
+    _lambdaBodyType :: Object,
+    _lambdaBody :: Morphism
+  }
+
+data Application = Application
+  { _applicationDomainType :: Object,
+    _applicationCodomainType :: Object,
+    _applicationLeft :: Morphism,
+    _applicationRight :: Morphism
+  }
+
+newtype Var = Var {_varIndex :: Int}
+
+-- | Corresponds to the GEB type for morphisms (terms): `stlc`
+-- (https://github.com/anoma/geb/blob/main/src/specs/lambda.lisp).
+data Morphism
+  = MorphismAbsurd Morphism
+  | MorphismUnit
+  | MorphismLeft Morphism
+  | MorphismRight Morphism
+  | MorphismCase Case
+  | MorphismPair Pair
+  | MorphismFirst First
+  | MorphismSecond Second
+  | MorphismLambda Lambda
+  | MorphismApplication Application
+  | MorphismVar Var
+
+data Product = Product
+  { _productLeft :: Object,
+    _productRight :: Object
+  }
+
+data Coproduct = Coproduct
+  { _coproductLeft :: Object,
+    _coproductRight :: Object
+  }
+
+-- | Function type
+data Hom = Hom
+  { _homDomain :: Object,
+    _homCodomain :: Object
+  }
+
+-- | Corresponds to the GEB type for types (objects of the category): `substobj`
+-- (https://github.com/anoma/geb/blob/main/src/specs/geb.lisp).
+data Object
+  = -- | empty type
+    ObjectInitial
+  | -- | unit type
+    ObjectTerminal
+  | ObjectProduct Product
+  | ObjectCoproduct Coproduct
+  | -- | function type
+    ObjectHom Hom
+
+instance HasAtomicity Morphism where
+  atomicity = \case
+    MorphismAbsurd {} -> Aggregate appFixity
+    MorphismUnit -> Atom
+    MorphismLeft {} -> Aggregate appFixity
+    MorphismRight {} -> Aggregate appFixity
+    MorphismCase {} -> Aggregate appFixity
+    MorphismPair {} -> Aggregate appFixity
+    MorphismFirst {} -> Aggregate appFixity
+    MorphismSecond {} -> Aggregate appFixity
+    MorphismLambda {} -> Aggregate appFixity
+    MorphismApplication {} -> Aggregate appFixity
+    MorphismVar {} -> Aggregate appFixity
+
+instance HasAtomicity Object where
+  atomicity = \case
+    ObjectInitial -> Atom
+    ObjectTerminal -> Atom
+    ObjectProduct {} -> Aggregate appFixity
+    ObjectCoproduct {} -> Aggregate appFixity
+    ObjectHom {} -> Aggregate appFixity
+
+makeLenses ''Case
+makeLenses ''Pair
+makeLenses ''First
+makeLenses ''Second
+makeLenses ''Lambda
+makeLenses ''Var
+makeLenses ''Application
+makeLenses ''Morphism
+makeLenses ''Product
+makeLenses ''Coproduct
+makeLenses ''Hom
+makeLenses ''Object

src/Juvix/Compiler/Backend/Geb/Pretty.hs

@@ -0,0 +1,28 @@
+module Juvix.Compiler.Backend.Geb.Pretty
+  ( module Juvix.Compiler.Backend.Geb.Pretty,
+    module Juvix.Compiler.Backend.Geb.Pretty.Base,
+    module Juvix.Compiler.Backend.Geb.Pretty.Options,
+    module Juvix.Data.PPOutput,
+  )
+where
+
+import Juvix.Compiler.Backend.Geb.Pretty.Base
+import Juvix.Compiler.Backend.Geb.Pretty.Options
+import Juvix.Data.PPOutput
+import Juvix.Prelude
+import Prettyprinter.Render.Terminal qualified as Ansi
+
+ppOutDefault :: (HasAtomicity c, PrettyCode c) => c -> AnsiText
+ppOutDefault = AnsiText . PPOutput . doc defaultOptions
+
+ppOut :: (CanonicalProjection a Options, HasAtomicity c, PrettyCode c) => a -> c -> AnsiText
+ppOut o = AnsiText . PPOutput . doc (project o)
+
+ppTrace' :: (CanonicalProjection a Options, HasAtomicity c, PrettyCode c) => a -> c -> Text
+ppTrace' opts = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc (project opts)
+
+ppTrace :: (HasAtomicity c, PrettyCode c) => c -> Text
+ppTrace = ppTrace' traceOptions
+
+ppPrint :: (HasAtomicity c, PrettyCode c) => c -> Text
+ppPrint = show . ppOutDefault

src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs

@@ -0,0 +1,207 @@
+module Juvix.Compiler.Backend.Geb.Pretty.Base
+  ( module Juvix.Compiler.Backend.Geb.Pretty.Base,
+    module Juvix.Data.CodeAnn,
+    module Juvix.Compiler.Backend.Geb.Pretty.Options,
+  )
+where
+
+import Juvix.Compiler.Backend.Geb.Language
+import Juvix.Compiler.Backend.Geb.Pretty.Options
+import Juvix.Data.CodeAnn
+import Juvix.Extra.Strings qualified as Str
+
+doc :: (HasAtomicity c, PrettyCode c) => Options -> c -> Doc Ann
+doc opts x =
+  run $
+    runReader opts $
+      case atomicity x of
+        Atom -> ppCode x
+        Aggregate _ -> parens <$> ppCode x
+
+class PrettyCode c where
+  ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
+
+instance PrettyCode Case where
+  ppCode Case {..} = do
+    lty <- ppArg _caseLeftType
+    rty <- ppArg _caseRightType
+    cod <- ppArg _caseCodomainType
+    val <- ppArg _caseOn
+    left <- ppArg _caseLeft
+    right <- ppArg _caseRight
+    return $ kwCase <+> lty <+> rty <+> cod <+> val <+> left <+> right
+
+instance PrettyCode Pair where
+  ppCode Pair {..} = do
+    lty <- ppArg _pairLeftType
+    rty <- ppArg _pairRightType
+    left <- ppArg _pairLeft
+    right <- ppArg _pairRight
+    return $ kwPair <+> lty <+> rty <+> left <+> right
+
+instance PrettyCode First where
+  ppCode First {..} = do
+    lty <- ppArg _firstLeftType
+    rty <- ppArg _firstRightType
+    val <- ppArg _firstValue
+    return $ kwFst <+> lty <+> rty <+> val
+
+instance PrettyCode Second where
+  ppCode Second {..} = do
+    lty <- ppArg _secondLeftType
+    rty <- ppArg _secondRightType
+    val <- ppArg _secondValue
+    return $ kwSnd <+> lty <+> rty <+> val
+
+instance PrettyCode Lambda where
+  ppCode Lambda {..} = do
+    vty <- ppArg _lambdaVarType
+    bty <- ppArg _lambdaBodyType
+    body <- ppArg _lambdaBody
+    return $ kwLamb <+> vty <+> bty <+> body
+
+instance PrettyCode Application where
+  ppCode Application {..} = do
+    dom <- ppArg _applicationDomainType
+    cod <- ppArg _applicationCodomainType
+    left <- ppArg _applicationLeft
+    right <- ppArg _applicationRight
+    return $ kwApp <+> dom <+> cod <+> left <+> right
+
+instance PrettyCode Var where
+  ppCode Var {..} = return $ annotate AnnLiteralInteger (pretty _varIndex)
+
+instance PrettyCode Morphism where
+  ppCode = \case
+    MorphismAbsurd val -> do
+      v <- ppArg val
+      return $ kwAbsurd <+> v
+    MorphismUnit ->
+      return kwUnit
+    MorphismLeft val -> do
+      v <- ppArg val
+      return $ kwLeft <+> v
+    MorphismRight val -> do
+      v <- ppArg val
+      return $ kwRight <+> v
+    MorphismCase x -> ppCode x
+    MorphismPair x -> ppCode x
+    MorphismFirst x -> ppCode x
+    MorphismSecond x -> ppCode x
+    MorphismLambda x -> ppCode x
+    MorphismApplication x -> ppCode x
+    MorphismVar idx -> do
+      i <- ppCode idx
+      return $ kwVar <+> i
+
+instance PrettyCode Product where
+  ppCode Product {..} = do
+    left <- ppArg _productLeft
+    right <- ppArg _productRight
+    return $ kwProd <+> left <+> right
+
+instance PrettyCode Coproduct where
+  ppCode Coproduct {..} = do
+    left <- ppArg _coproductLeft
+    right <- ppArg _coproductRight
+    return $ kwCoprod <+> left <+> right
+
+instance PrettyCode Hom where
+  ppCode Hom {..} = do
+    dom <- ppArg _homDomain
+    cod <- ppArg _homCodomain
+    return $ kwHom <+> dom <+> cod
+
+instance PrettyCode Object where
+  ppCode = \case
+    ObjectInitial -> return kwInitial
+    ObjectTerminal -> return kwTerminal
+    ObjectProduct x -> ppCode x
+    ObjectCoproduct x -> ppCode x
+    ObjectHom x -> ppCode x
+
+--------------------------------------------------------------------------------
+-- helper functions
+--------------------------------------------------------------------------------
+
+ppArg ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  a ->
+  Sem r (Doc Ann)
+ppArg = ppRightExpression appFixity
+
+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 =
+  parensIf (atomParens associates (atomicity e) fixlr)
+    <$> ppCode e
+
+--------------------------------------------------------------------------------
+-- keywords
+--------------------------------------------------------------------------------
+
+kwAbsurd :: Doc Ann
+kwAbsurd = keyword Str.gebAbsurd
+
+kwUnit :: Doc Ann
+kwUnit = keyword Str.gebUnit
+
+kwLeft :: Doc Ann
+kwLeft = keyword Str.gebLeft
+
+kwRight :: Doc Ann
+kwRight = keyword Str.gebRight
+
+kwFst :: Doc Ann
+kwFst = keyword Str.gebFst
+
+kwSnd :: Doc Ann
+kwSnd = keyword Str.gebSnd
+
+kwCase :: Doc Ann
+kwCase = keyword Str.gebCase
+
+kwPair :: Doc Ann
+kwPair = keyword Str.gebPair
+
+kwLamb :: Doc Ann
+kwLamb = keyword Str.gebLamb
+
+kwApp :: Doc Ann
+kwApp = keyword Str.gebApp
+
+kwVar :: Doc Ann
+kwVar = keyword Str.gebVar
+
+kwInitial :: Doc Ann
+kwInitial = keyword Str.gebInitial
+
+kwTerminal :: Doc Ann
+kwTerminal = keyword Str.gebTerminal
+
+kwProd :: Doc Ann
+kwProd = keyword Str.gebProd
+
+kwCoprod :: Doc Ann
+kwCoprod = keyword Str.gebCoprod
+
+kwHom :: Doc Ann
+kwHom = keyword Str.gebHom

src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs

@@ -0,0 +1,21 @@
+module Juvix.Compiler.Backend.Geb.Pretty.Options where
+
+import Juvix.Prelude
+
+-- no fields for now, but make it easier to add options in the future I don't
+-- remove this datatype entirely
+data Options = Options
+
+makeLenses ''Options
+
+defaultOptions :: Options
+defaultOptions = Options
+
+traceOptions :: Options
+traceOptions = Options
+
+fromGenericOptions :: GenericOptions -> Options
+fromGenericOptions _ = defaultOptions
+
+instance CanonicalProjection GenericOptions Options where
+  project = fromGenericOptions

src/Juvix/Compiler/Backend/Geb/Translation.hs

@@ -0,0 +1,16 @@
+module Juvix.Compiler.Backend.Geb.Translation
+  ( module Juvix.Compiler.Backend.Geb.Translation,
+    module Juvix.Compiler.Backend.Geb.Translation.FromCore,
+  )
+where
+
+import Juvix.Compiler.Backend.Geb.Language
+import Juvix.Compiler.Backend.Geb.Pretty
+import Juvix.Compiler.Backend.Geb.Translation.FromCore
+
+newtype Result = Result
+  { _resultCode :: Text
+  }
+
+toResult :: Morphism -> Result
+toResult geb = Result (ppPrint geb <> "\n")

src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs

@@ -0,0 +1,397 @@
+module Juvix.Compiler.Backend.Geb.Translation.FromCore where
+
+import Data.HashMap.Strict qualified as HashMap
+import Data.List qualified as List
+import Juvix.Compiler.Backend.Geb.Extra
+import Juvix.Compiler.Backend.Geb.Language
+import Juvix.Compiler.Core.Data.InfoTable qualified as Core
+import Juvix.Compiler.Core.Extra qualified as Core
+import Juvix.Compiler.Core.Info.TypeInfo qualified as Info
+import Juvix.Compiler.Core.Language (Index, Level, Symbol)
+import Juvix.Compiler.Core.Language qualified as Core
+
+fromCore :: Core.InfoTable -> Morphism
+fromCore tab = case tab ^. Core.infoMain of
+  Just sym ->
+    let node = fromJust $ HashMap.lookup sym (tab ^. Core.identContext)
+        idents = HashMap.delete sym (tab ^. Core.infoIdentifiers)
+     in goIdents mempty 0 [] node (HashMap.elems idents)
+  Nothing ->
+    error "no main function"
+  where
+    unsupported :: forall a. a
+    unsupported = error "unsupported"
+
+    {-
+      The translation of each identifier is saved separately to avoid exponential
+      blow-up. For example, the program:
+      ```
+      a : A
+
+      f : A -> A
+      f x = F
+
+      g : A -> A
+      g x = f (f x)
+
+      main : A
+      main = g (g a)
+      ```
+      is translated as if it were a single node:
+      ```
+      (\a -> (\f -> (\g -> g (g a)) (\x -> f (f x))) (\x -> F)) a
+      ```
+    -}
+    goIdents :: HashMap Symbol Level -> Level -> [Level] -> Core.Node -> [Core.IdentifierInfo] -> Morphism
+    goIdents identMap level shiftLevels node = \case
+      ii : idents ->
+        MorphismApplication
+          Application
+            { _applicationDomainType = argty,
+              _applicationCodomainType = nodeType,
+              _applicationLeft = lamb,
+              _applicationRight = convertNode identMap 0 shiftLevels fundef
+            }
+        where
+          sym = ii ^. Core.identifierSymbol
+          fundef = fromJust $ HashMap.lookup sym (tab ^. Core.identContext)
+          argty = convertType (Info.getNodeType fundef)
+          body = goIdents (HashMap.insert sym level identMap) (level + 1) (0 : shiftLevels) node idents
+          lamb =
+            MorphismLambda
+              Lambda
+                { _lambdaVarType = argty,
+                  _lambdaBodyType = nodeType,
+                  _lambdaBody = body
+                }
+      [] ->
+        convertNode identMap 0 shiftLevels node
+      where
+        nodeType = convertType (Info.getNodeType node)
+
+    -- `shiftLevels` contains the de Bruijn levels immediately before which a
+    -- binder was inserted
+    convertNode :: HashMap Symbol Level -> Level -> [Level] -> Core.Node -> Morphism
+    convertNode identMap varsNum shiftLevels = \case
+      Core.NVar x -> convertVar identMap varsNum shiftLevels x
+      Core.NIdt x -> convertIdent identMap varsNum shiftLevels x
+      Core.NCst x -> convertConstant identMap varsNum shiftLevels x
+      Core.NApp x -> convertApp identMap varsNum shiftLevels x
+      Core.NBlt x -> convertBuiltinApp identMap varsNum shiftLevels x
+      Core.NCtr x -> convertConstr identMap varsNum shiftLevels x
+      Core.NLam x -> convertLambda identMap varsNum shiftLevels x
+      Core.NLet x -> convertLet identMap varsNum shiftLevels x
+      Core.NRec {} -> unsupported -- LetRecs should be lifted out beforehand
+      Core.NCase x -> convertCase identMap varsNum shiftLevels x
+      Core.NMatch {} -> unsupported -- Pattern matching should be compiled beforehand
+      Core.NPi {} -> unsupported
+      Core.NUniv {} -> unsupported
+      Core.NTyp {} -> unsupported
+      Core.NPrim {} -> unsupported
+      Core.NDyn {} -> unsupported
+      Core.Closure {} -> unsupported
+
+    insertedBinders :: Level -> [Level] -> Index -> Int
+    insertedBinders varsNum shiftLevels idx =
+      length (filter ((varsNum - idx) <=) shiftLevels)
+
+    convertVar :: HashMap Symbol Level -> Level -> [Level] -> Core.Var -> Morphism
+    convertVar _ varsNum shiftLevels Core.Var {..} =
+      MorphismVar (Var (_varIndex + insertedBinders varsNum shiftLevels _varIndex))
+
+    convertIdent :: HashMap Symbol Level -> Level -> [Level] -> Core.Ident -> Morphism
+    convertIdent identMap varsNum shiftLevels Core.Ident {..} =
+      MorphismVar (Var (varsNum + length shiftLevels - fromJust (HashMap.lookup _identSymbol identMap) - 1))
+
+    convertConstant :: HashMap Symbol Level -> Level -> [Level] -> Core.Constant -> Morphism
+    convertConstant _ _ _ Core.Constant {} = unsupported
+
+    convertApp :: HashMap Symbol Level -> Level -> [Level] -> Core.App -> Morphism
+    convertApp identMap varsNum shiftLevels Core.App {..} =
+      MorphismApplication
+        Application
+          { _applicationDomainType = convertType (Info.getNodeType _appRight),
+            _applicationCodomainType = convertType (Info.getInfoType _appInfo),
+            _applicationLeft = convertNode identMap varsNum shiftLevels _appLeft,
+            _applicationRight = convertNode identMap varsNum shiftLevels _appRight
+          }
+
+    convertBuiltinApp :: HashMap Symbol Level -> Level -> [Level] -> Core.BuiltinApp -> Morphism
+    convertBuiltinApp _ _ _ Core.BuiltinApp {} = unsupported
+
+    convertConstr :: HashMap Symbol Level -> Level -> [Level] -> Core.Constr -> Morphism
+    convertConstr identMap varsNum shiftLevels Core.Constr {..} =
+      foldr ($) prod (replicate tagNum MorphismRight)
+      where
+        ci = fromJust $ HashMap.lookup _constrTag (tab ^. Core.infoConstructors)
+        sym = ci ^. Core.constructorInductive
+        ctrs = fromJust (HashMap.lookup sym (tab ^. Core.infoInductives)) ^. Core.inductiveConstructors
+        tagNum = fromJust $ elemIndex _constrTag (sort (map (^. Core.constructorTag) ctrs))
+        prod =
+          (if tagNum == length ctrs - 1 then id else MorphismLeft)
+            (convertProduct identMap varsNum shiftLevels _constrArgs)
+
+    convertProduct :: HashMap Symbol Level -> Level -> [Level] -> [Core.Node] -> Morphism
+    convertProduct identMap varsNum shiftLevels args = case reverse args of
+      h : t ->
+        fst $
+          foldr
+            (\x -> mkPair (convertNode identMap varsNum shiftLevels x, convertType (Info.getNodeType x)))
+            (convertNode identMap varsNum shiftLevels h, convertType (Info.getNodeType h))
+            (reverse t)
+      [] ->
+        MorphismUnit
+      where
+        mkPair :: (Morphism, Object) -> (Morphism, Object) -> (Morphism, Object)
+        mkPair (x, xty) (y, yty) = (z, zty)
+          where
+            z =
+              MorphismPair
+                Pair
+                  { _pairLeftType = xty,
+                    _pairRightType = yty,
+                    _pairLeft = x,
+                    _pairRight = y
+                  }
+            zty = ObjectProduct (Product xty yty)
+
+    convertLet :: HashMap Symbol Level -> Level -> [Level] -> Core.Let -> Morphism
+    convertLet identMap varsNum shiftLevels Core.Let {..} =
+      MorphismApplication
+        Application
+          { _applicationCodomainType = domty,
+            _applicationDomainType = codty,
+            _applicationLeft =
+              MorphismLambda
+                Lambda
+                  { _lambdaVarType = domty,
+                    _lambdaBodyType = codty,
+                    _lambdaBody = convertNode identMap varsNum shiftLevels _letBody
+                  },
+            _applicationRight = convertNode identMap varsNum shiftLevels (_letItem ^. Core.letItemValue)
+          }
+      where
+        domty = convertType (_letItem ^. Core.letItemBinder . Core.binderType)
+        codty = convertType (Info.getNodeType _letBody)
+
+    convertLambda :: HashMap Symbol Level -> Level -> [Level] -> Core.Lambda -> Morphism
+    convertLambda identMap varsNum shiftLevels Core.Lambda {..} =
+      MorphismLambda
+        Lambda
+          { _lambdaVarType = convertType (_lambdaBinder ^. Core.binderType),
+            _lambdaBodyType = convertType (Info.getNodeType _lambdaBody),
+            _lambdaBody = convertNode identMap (varsNum + 1) shiftLevels _lambdaBody
+          }
+
+    convertCase :: HashMap Symbol Level -> Level -> [Level] -> Core.Case -> Morphism
+    convertCase identMap varsNum shiftLevels Core.Case {..} =
+      if
+          | null branches ->
+              MorphismAbsurd (convertNode identMap varsNum shiftLevels _caseValue)
+          | missingCtrsNum > 1 ->
+              let ty = convertType (Info.getNodeType defaultNode)
+               in MorphismApplication
+                    Application
+                      { _applicationDomainType = ty,
+                        _applicationCodomainType = ty,
+                        _applicationLeft =
+                          MorphismLambda
+                            Lambda
+                              { _lambdaVarType = ty,
+                                _lambdaBodyType = ty,
+                                _lambdaBody = go indty (varsNum : shiftLevels) _caseValue branches
+                              },
+                        _applicationRight = convertNode identMap varsNum shiftLevels defaultNode
+                      }
+          | otherwise -> go indty shiftLevels _caseValue branches
+      where
+        indty = convertInductive _caseInductive
+        ii = fromJust $ HashMap.lookup _caseInductive (tab ^. Core.infoInductives)
+        missingCtrs =
+          filter
+            ( \x ->
+                isNothing (find (\y -> x ^. Core.constructorTag == y ^. Core.caseBranchTag) _caseBranches)
+            )
+            (ii ^. Core.inductiveConstructors)
+        missingCtrsNum = length missingCtrs
+        ctrBrs = map mkCtrBranch missingCtrs
+        defaultNode = fromMaybe (error "not all cases covered") _caseDefault
+        -- `branches` contains one branch for each constructor of the inductive type.
+        -- `_caseDefault` is the body of those branches which were not present in
+        -- `_caseBranches`.
+        branches = sortOn (^. Core.caseBranchTag) (_caseBranches ++ ctrBrs)
+        codty = convertType (Info.getNodeType (List.head branches ^. Core.caseBranchBody))
+
+        mkCtrBranch :: Core.ConstructorInfo -> Core.CaseBranch
+        mkCtrBranch ci =
+          Core.CaseBranch
+            { _caseBranchInfo = mempty,
+              _caseBranchTag = ci ^. Core.constructorTag,
+              _caseBranchBinders = map (Core.Binder "?" Nothing) tyargs,
+              _caseBranchBindersNum = n,
+              _caseBranchBody = defaultBody n
+            }
+          where
+            tyargs = Core.typeArgs (ci ^. Core.constructorType)
+            n = length tyargs
+            defaultBody =
+              if
+                  | missingCtrsNum > 1 -> Core.mkVar'
+                  | otherwise -> (`Core.shift` defaultNode)
+
+        go :: Object -> [Level] -> Core.Node -> [Core.CaseBranch] -> Morphism
+        go ty lvls val = \case
+          [br] ->
+            -- there is only one constructor, so `ty` is a product of its argument types
+            mkBranch ty lvls val br
+          br : brs ->
+            MorphismCase
+              Case
+                { _caseLeftType = lty,
+                  _caseRightType = rty,
+                  _caseCodomainType = codty,
+                  _caseOn = convertNode identMap varsNum lvls val,
+                  _caseLeft =
+                    MorphismLambda
+                      Lambda
+                        { _lambdaVarType = lty,
+                          _lambdaBodyType = codty,
+                          _lambdaBody = mkBranch lty (varsNum : lvls) val br
+                        },
+                  _caseRight =
+                    MorphismLambda
+                      Lambda
+                        { _lambdaVarType = rty,
+                          _lambdaBodyType = codty,
+                          _lambdaBody = go rty (varsNum : lvls) (Core.mkVar' 0) brs
+                        }
+                }
+            where
+              (lty, rty) = case ty of
+                ObjectCoproduct Coproduct {..} -> (_coproductLeft, _coproductRight)
+                _ -> impossible
+          [] -> impossible
+
+        mkBranch :: Object -> [Level] -> Core.Node -> Core.CaseBranch -> Morphism
+        mkBranch valty lvls val Core.CaseBranch {..} =
+          if
+              | _caseBranchBindersNum == 0 ->
+                  branch
+              | otherwise ->
+                  mkApps (mkLambs argtys) (convertNode identMap varsNum lvls val) valty argtys
+          where
+            branch = convertNode identMap (varsNum + _caseBranchBindersNum) lvls _caseBranchBody
+            argtys = destructProduct valty
+
+            mkApps :: Morphism -> Morphism -> Object -> [Object] -> Morphism
+            mkApps acc v vty = \case
+              ty : tys ->
+                mkApps acc' v' rty tys
+                where
+                  v' =
+                    MorphismSecond
+                      Second
+                        { _secondLeftType = lty,
+                          _secondRightType = rty,
+                          _secondValue = v
+                        }
+                  acc' =
+                    MorphismApplication
+                      Application
+                        { _applicationDomainType = ty,
+                          _applicationCodomainType = vty,
+                          _applicationLeft = acc,
+                          _applicationRight =
+                            if
+                                | null tys ->
+                                    v
+                                | otherwise ->
+                                    MorphismFirst
+                                      First
+                                        { _firstLeftType = lty,
+                                          _firstRightType = rty,
+                                          _firstValue = v
+                                        }
+                        }
+                  (lty, rty) = case vty of
+                    ObjectProduct Product {..} -> (_productLeft, _productRight)
+                    _ -> impossible
+              [] ->
+                acc
+
+            mkLambs :: [Object] -> Morphism
+            mkLambs =
+              fst
+                . foldr
+                  ( \ty (acc, accty) ->
+                      ( MorphismLambda
+                          Lambda
+                            { _lambdaVarType = ty,
+                              _lambdaBodyType = accty,
+                              _lambdaBody = acc
+                            },
+                        ObjectHom (Hom ty accty)
+                      )
+                  )
+                  (branch, codty)
+
+    convertType :: Core.Type -> Object
+    convertType = \case
+      Core.NPi x ->
+        convertPi x
+      Core.NUniv {} ->
+        unsupported -- no polymorphism yet
+      Core.NTyp x ->
+        convertTypeConstr x
+      Core.NPrim x ->
+        convertTypePrim x
+      Core.NDyn {} ->
+        error "incomplete type information (dynamic type encountered)"
+      Core.NLam Core.Lambda {..} ->
+        convertType _lambdaBody
+      _ ->
+        unsupported
+
+    convertPi :: Core.Pi -> Object
+    convertPi Core.Pi {..} =
+      ObjectHom
+        Hom
+          { _homDomain = convertType (_piBinder ^. Core.binderType),
+            _homCodomain = convertType _piBody
+          }
+
+    convertTypeConstr :: Core.TypeConstr -> Object
+    convertTypeConstr Core.TypeConstr {..} = convertInductive _typeConstrSymbol
+
+    convertTypePrim :: Core.TypePrim -> Object
+    convertTypePrim Core.TypePrim {..} =
+      case _typePrimPrimitive of
+        Core.PrimInteger _ -> unsupported
+        Core.PrimBool _ -> ObjectCoproduct (Coproduct ObjectTerminal ObjectTerminal)
+        Core.PrimString -> unsupported
+
+    convertInductive :: Symbol -> Object
+    convertInductive sym =
+      case reverse ctrs of
+        ci : ctrs' ->
+          foldr
+            (\x acc -> ObjectCoproduct (Coproduct (convertConstructorType (x ^. Core.constructorType)) acc))
+            (convertConstructorType (ci ^. Core.constructorType))
+            (reverse ctrs')
+        [] ->
+          ObjectInitial
+      where
+        ctrs =
+          sortOn (^. Core.constructorTag) $
+            fromJust (HashMap.lookup sym (tab ^. Core.infoInductives)) ^. Core.inductiveConstructors
+
+    convertConstructorType :: Core.Node -> Object
+    convertConstructorType ty =
+      case reverse (Core.typeArgs ty) of
+        hty : tys ->
+          foldr
+            (\x acc -> ObjectProduct (Product (convertType x) acc))
+            (convertType hty)
+            (reverse tys)
+        [] ->
+          ObjectTerminal

src/Juvix/Compiler/Core/Data/BinderList.hs

@@ -68,17 +68,14 @@ lookupsSortedRev bl = go [] 0 bl
 -- | lookup de Bruijn Index
 lookup :: Index -> BinderList a -> a
 lookup idx bl
-  | target < bl ^. blLength = (bl ^. blMap) !! target
+  | idx < bl ^. blLength = (bl ^. blMap) !! idx
   | otherwise = err
   where
-    target = idx
     err :: a
     err =
       error
         ( "invalid binder lookup. Got index "
             <> show idx
-            <> " that targets "
-            <> show target
             <> " and the length is "
             <> show (bl ^. blLength)
             <> ". Actual length is "
@@ -87,16 +84,16 @@ lookup idx bl
 
 -- | lookup de Bruijn Level
 lookupLevel :: Level -> BinderList a -> a
-lookupLevel idx bl
+lookupLevel lvl bl
   | target < bl ^. blLength = (bl ^. blMap) !! target
   | otherwise = err
   where
-    target = bl ^. blLength - 1 - idx
+    target = bl ^. blLength - 1 - lvl
     err :: a
     err =
       error
-        ( "invalid binder lookup. Got index "
-            <> show idx
+        ( "invalid binder lookup. Got de Bruijn level "
+            <> show lvl
             <> " that targets "
             <> show target
             <> " and the length is "

src/Juvix/Compiler/Core/Data/TransformationId.hs

@@ -10,4 +10,6 @@ data TransformationId
   | NatToInt
   | ConvertBuiltinTypes
   | Identity
+  | UnrollRecursion
+  | ComputeTypeInfo
   deriving stock (Data)

src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs

@@ -48,6 +48,8 @@ pcompletions = do
       MoveApps -> strMoveApps
       NatToInt -> strNatToInt
       ConvertBuiltinTypes -> strConvertBuiltinTypes
+      ComputeTypeInfo -> strComputeTypeInfo
+      UnrollRecursion -> strUnrollRecursion
 
 lexeme :: (MonadParsec e Text m) => m a -> m a
 lexeme = L.lexeme L.hspace
@@ -67,6 +69,8 @@ transformation =
     <|> symbol strMoveApps $> MoveApps
     <|> symbol strNatToInt $> NatToInt
     <|> symbol strConvertBuiltinTypes $> ConvertBuiltinTypes
+    <|> symbol strUnrollRecursion $> UnrollRecursion
+    <|> symbol strComputeTypeInfo $> ComputeTypeInfo
 
 allStrings :: [Text]
 allStrings =
@@ -76,7 +80,9 @@ allStrings =
     strRemoveTypeArgs,
     strMoveApps,
     strNatToInt,
-    strConvertBuiltinTypes
+    strConvertBuiltinTypes,
+    strUnrollRecursion,
+    strComputeTypeInfo
   ]
 
 strLifting :: Text
@@ -99,3 +105,9 @@ strNatToInt = "nat-to-int"
 
 strConvertBuiltinTypes :: Text
 strConvertBuiltinTypes = "convert-builtin-types"
+
+strComputeTypeInfo :: Text
+strComputeTypeInfo = "compute-type-info"
+
+strUnrollRecursion :: Text
+strUnrollRecursion = "unroll-recursion"

src/Juvix/Compiler/Core/Info/TypeInfo.hs

@@ -0,0 +1,33 @@
+module Juvix.Compiler.Core.Info.TypeInfo where
+
+import Juvix.Compiler.Core.Extra.Base
+import Juvix.Compiler.Core.Extra.Info
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Language
+
+newtype TypeInfo = TypeInfo {_infoType :: Type}
+
+instance IsInfo TypeInfo
+
+kTypeInfo :: Key TypeInfo
+kTypeInfo = Proxy
+
+makeLenses ''TypeInfo
+
+getInfoType :: Info -> Type
+getInfoType i =
+  case Info.lookup kTypeInfo i of
+    Just TypeInfo {..} -> _infoType
+    Nothing -> mkDynamic'
+
+setInfoType :: Type -> Info -> Info
+setInfoType = Info.insert . TypeInfo
+
+getNodeType :: Node -> Type
+getNodeType = getInfoType . getInfo
+
+setNodeType :: Type -> Node -> Node
+setNodeType = modifyInfo . setInfoType
+
+removeTypeInfo :: Node -> Node
+removeTypeInfo = removeInfo kTypeInfo

src/Juvix/Compiler/Core/Language/Base.hs

@@ -25,7 +25,7 @@ uniqueName txt sym = txt <> "_" <> show sym
 -- common "builtin" constructors, e.g., unit, nat, so that the code generator
 -- can treat them specially.
 data Tag = BuiltinTag BuiltinDataTag | UserTag Word
-  deriving stock (Eq, Generic)
+  deriving stock (Eq, Ord, Generic)
 
 instance Hashable Tag
 

src/Juvix/Compiler/Core/Language/Builtins.hs

@@ -28,7 +28,7 @@ data BuiltinDataTag
   | TagBind
   | TagWrite
   | TagReadLn
-  deriving stock (Eq, Generic)
+  deriving stock (Eq, Ord, Generic)
 
 instance Hashable BuiltinDataTag
 

src/Juvix/Compiler/Core/Pipeline.hs

@@ -14,3 +14,10 @@ toStrippedTransformations = [NatToInt, ConvertBuiltinTypes, LambdaLifting, MoveA
 -- Core.Stripped
 toStripped :: InfoTable -> InfoTable
 toStripped = applyTransformations toStrippedTransformations
+
+toGebTransformations :: [TransformationId]
+toGebTransformations = [NatToInt, ConvertBuiltinTypes, UnrollRecursion, ComputeTypeInfo]
+
+-- | Perform transformations on Core necessary before the translation to GEB
+toGeb :: InfoTable -> InfoTable
+toGeb = applyTransformations toGebTransformations

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -28,9 +28,6 @@ doc opts =
 class PrettyCode c where
   ppCode :: (Member (Reader Options) r) => c -> Sem r (Doc Ann)
 
-runPrettyCode :: (PrettyCode c) => Options -> c -> Doc Ann
-runPrettyCode opts = run . runReader opts . ppCode
-
 instance PrettyCode BuiltinOp where
   ppCode = \case
     OpIntAdd -> return primPlus
@@ -431,9 +428,6 @@ instance (PrettyCode a) => PrettyCode [a] where
 {--------------------------------------------------------------------------------}
 {- helper functions -}
 
-parensIf :: Bool -> Doc Ann -> Doc Ann
-parensIf t = if t then parens else id
-
 ppPostExpression ::
   (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
   Fixity ->

src/Juvix/Compiler/Core/Transformation.hs

@@ -10,6 +10,7 @@ where
 
 import Juvix.Compiler.Core.Data.TransformationId
 import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation.ComputeTypeInfo
 import Juvix.Compiler.Core.Transformation.ConvertBuiltinTypes
 import Juvix.Compiler.Core.Transformation.Eta
 import Juvix.Compiler.Core.Transformation.Identity
@@ -18,6 +19,7 @@ import Juvix.Compiler.Core.Transformation.MoveApps
 import Juvix.Compiler.Core.Transformation.NatToInt
 import Juvix.Compiler.Core.Transformation.RemoveTypeArgs
 import Juvix.Compiler.Core.Transformation.TopEtaExpand
+import Juvix.Compiler.Core.Transformation.UnrollRecursion
 
 applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
 applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
@@ -31,3 +33,5 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
       MoveApps -> moveApps
       NatToInt -> natToInt
       ConvertBuiltinTypes -> convertBuiltinTypes
+      ComputeTypeInfo -> computeTypeInfo
+      UnrollRecursion -> unrollRecursion

src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs

@@ -0,0 +1,96 @@
+module Juvix.Compiler.Core.Transformation.ComputeTypeInfo (computeTypeInfo) where
+
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Core.Data.BinderList qualified as BL
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info.TypeInfo qualified as Info
+import Juvix.Compiler.Core.Transformation.Base
+
+-- | Computes the TypeInfo for each subnode.
+--
+-- Assumptions:
+-- 1. All binders and identifiers are decorated with full type information.
+-- 2. No polymorphism.
+-- 3. No dynamic type.
+-- 4. All cases have at least one branch.
+-- 5. No `Match` nodes.
+-- 6. All inductives and function types are in universe 0.
+computeNodeTypeInfo :: InfoTable -> Node -> Node
+computeNodeTypeInfo tab = umapL go
+  where
+    go :: BinderList Binder -> Node -> Node
+    go bl node = Info.setNodeType (nodeType bl node) node
+
+    nodeType :: BinderList Binder -> Node -> Type
+    nodeType bl = \case
+      NVar Var {..} ->
+        BL.lookup _varIndex bl ^. binderType
+      NIdt Ident {..} ->
+        fromJust (HashMap.lookup _identSymbol (tab ^. infoIdentifiers)) ^. identifierType
+      NCst Constant {..} ->
+        case _constantValue of
+          ConstInteger {} -> mkTypeInteger'
+          ConstString {} -> mkTypeString'
+      NApp App {..} ->
+        let lty = Info.getNodeType _appLeft
+            rty = Info.getNodeType _appRight
+         in case lty of
+              NPi Pi {..}
+                | rty == _piBinder ^. binderType ->
+                    _piBody
+              _ ->
+                error "incorrect type information (application)"
+      NBlt BuiltinApp {..} ->
+        case _builtinAppOp of
+          OpIntAdd -> mkTypeInteger'
+          OpIntSub -> mkTypeInteger'
+          OpIntMul -> mkTypeInteger'
+          OpIntDiv -> mkTypeInteger'
+          OpIntMod -> mkTypeInteger'
+          OpIntLt -> mkTypeBool'
+          OpIntLe -> mkTypeBool'
+          OpEq -> mkTypeBool'
+          OpShow -> mkTypeString'
+          OpStrConcat -> mkTypeString'
+          OpStrToInt -> mkTypeInteger'
+          OpTrace -> case _builtinAppArgs of
+            [_, arg2] -> Info.getNodeType arg2
+            _ -> error "incorrect trace builtin application"
+          OpFail -> mkDynamic'
+      NCtr Constr {..} ->
+        let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors)
+            ii = fromJust $ HashMap.lookup (ci ^. constructorInductive) (tab ^. infoInductives)
+         in case ii ^. inductiveBuiltin of
+              Just BuiltinBool ->
+                mkTypeBool'
+              _ ->
+                mkTypeConstr' (ci ^. constructorInductive) (take (length (ii ^. inductiveParams)) _constrArgs)
+      NLam Lambda {..} ->
+        mkPi' (_lambdaBinder ^. binderType) (Info.getNodeType _lambdaBody)
+      NLet Let {..} ->
+        Info.getNodeType _letBody
+      NRec LetRec {..} ->
+        Info.getNodeType _letRecBody
+      NCase Case {..} -> case _caseDefault of
+        Just nd -> Info.getNodeType nd
+        Nothing -> case _caseBranches of
+          CaseBranch {..} : _ ->
+            Info.getNodeType _caseBranchBody
+          [] -> error "case with no branches"
+      NMatch Match {} ->
+        error "match unsupported"
+      NPi Pi {} ->
+        mkUniv' 0
+      NUniv Univ {..} ->
+        mkUniv' (_univLevel + 1)
+      NTyp TypeConstr {} ->
+        mkUniv' 0
+      NPrim TypePrim {} ->
+        mkUniv' 0
+      NDyn Dynamic {} ->
+        mkUniv' 0
+      Closure {} ->
+        impossible
+
+computeTypeInfo :: InfoTable -> InfoTable
+computeTypeInfo tab = mapT (const (computeNodeTypeInfo tab)) tab

src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs

@@ -0,0 +1,7 @@
+module Juvix.Compiler.Core.Transformation.UnrollRecursion (unrollRecursion) where
+
+import Juvix.Compiler.Core.Transformation.Base
+
+-- TODO: not yet implemented / at first only check for recursion and give an error
+unrollRecursion :: InfoTable -> InfoTable
+unrollRecursion tab = tab

src/Juvix/Compiler/Pipeline.hs

@@ -11,6 +11,7 @@ import Juvix.Compiler.Asm.Pipeline qualified as Asm
 import Juvix.Compiler.Asm.Translation.FromCore qualified as Asm
 import Juvix.Compiler.Backend qualified as Backend
 import Juvix.Compiler.Backend.C qualified as C
+import Juvix.Compiler.Backend.Geb qualified as Geb
 import Juvix.Compiler.Builtins
 import Juvix.Compiler.Concrete qualified as Concrete
 import Juvix.Compiler.Concrete.Translation.FromParsed qualified as Scoper
@@ -173,6 +174,9 @@ asmToMiniC opts = Asm.toReg opts >=> regToMiniC (opts ^. Asm.optLimits) . Reg.fr
 regToMiniC :: Backend.Limits -> Reg.InfoTable -> Sem r C.MiniCResult
 regToMiniC lims = return . C.fromReg lims
 
+coreToGeb :: Core.InfoTable -> Sem r Geb.Result
+coreToGeb = return . Geb.toResult . Geb.fromCore . Core.toGeb
+
 --------------------------------------------------------------------------------
 -- Run pipeline
 --------------------------------------------------------------------------------

src/Juvix/Data/CodeAnn.hs

@@ -221,6 +221,9 @@ parens = enclose kwParenL kwParenR
 bracesIf :: Bool -> Doc Ann -> Doc Ann
 bracesIf t = if t then braces else id
 
+parensIf :: Bool -> Doc Ann -> Doc Ann
+parensIf t = if t then parens else id
+
 implicitDelim :: IsImplicit -> Doc Ann -> Doc Ann
 implicitDelim = \case
   Implicit -> braces

src/Juvix/Extra/Strings.hs

@@ -542,7 +542,55 @@ instrReturn = "ret"
 instrBr :: (IsString s) => s
 instrBr = "br"
 
-juvixFunctionT :: (IsString s) => s
+gebAbsurd :: IsString s => s
+gebAbsurd = "absurd"
+
+gebUnit :: IsString s => s
+gebUnit = "unit"
+
+gebLeft :: IsString s => s
+gebLeft = "left"
+
+gebRight :: IsString s => s
+gebRight = "right"
+
+gebCase :: IsString s => s
+gebCase = "case-on"
+
+gebPair :: IsString s => s
+gebPair = "pair"
+
+gebFst :: IsString s => s
+gebFst = "fst"
+
+gebSnd :: IsString s => s
+gebSnd = "snd"
+
+gebLamb :: IsString s => s
+gebLamb = "lamb"
+
+gebApp :: IsString s => s
+gebApp = "app"
+
+gebVar :: IsString s => s
+gebVar = "index"
+
+gebInitial :: IsString s => s
+gebInitial = "so0"
+
+gebTerminal :: IsString s => s
+gebTerminal = "so1"
+
+gebProd :: IsString s => s
+gebProd = "prod"
+
+gebCoprod :: IsString s => s
+gebCoprod = "coprod"
+
+gebHom :: IsString s => s
+gebHom = "hom"
+
+juvixFunctionT :: IsString s => s
 juvixFunctionT = "juvix_function_t"
 
 juvixDotOrg :: (IsString s) => s

tests/Geb/positive/Core/out/test001.out

@@ -0,0 +1 @@
+(right unit)

tests/Geb/positive/Core/out/test002.out

@@ -0,0 +1 @@
+(left unit)

tests/Geb/positive/Core/out/test003.out

@@ -0,0 +1 @@
+(left unit)

tests/Geb/positive/Core/out/test004.out

@@ -0,0 +1 @@
+(left unit)

tests/Geb/positive/Core/test001.jvc

@@ -0,0 +1,2 @@
+
+(\(x : bool) if x then false else true) true

tests/Geb/positive/Core/test002.jvc

@@ -0,0 +1,7 @@
+
+type optbool {
+  Just : bool -> optbool;
+  Nothing : optbool;
+};
+
+(\(x : bool) \(o : optbool) { case o of { Just b := if x then true else b; Nothing := false } }) false (Just true)

tests/Geb/positive/Core/test003.jvc

@@ -0,0 +1,14 @@
+
+type enum {
+  opt0 : enum;
+  opt1 : bool -> enum;
+  opt2 : bool -> (bool -> bool) -> enum;
+  opt3 : bool -> (bool -> bool -> bool) -> bool -> enum;
+};
+
+(\(e : enum) case e of {
+  opt0 := false;
+  opt1 b := b;
+  opt2 b f := f b;
+  opt3 b1 f b2 := f b1 b2;
+}) (opt3 true (\(x : bool) \(y : bool) if y then false else x) false)

tests/Geb/positive/Core/test004.jvc

@@ -0,0 +1,5 @@
+
+def not : bool -> bool := \(x : bool) if x then false else true;
+def and : bool -> bool -> bool := \(x : bool) \(y : bool) if x then y else false;
+
+and (not false) (not (not true))