address review comments

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

@@ -2,7 +2,9 @@ module Juvix.Compiler.Backend.Geb.Extra where
 
 import Juvix.Compiler.Backend.Geb.Language
 
-destructProd :: Object -> [Object]
-destructProd = \case
-  ObjectProd Prod {..} -> _prodLeft : destructProd _prodRight
+-- | 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

@@ -1,6 +1,10 @@
-module Juvix.Compiler.Backend.Geb.Language where
+module Juvix.Compiler.Backend.Geb.Language
+  ( module Juvix.Compiler.Backend.Geb.Language,
+    module Juvix.Prelude,
+  )
+where
 
-import Juvix.Prelude
+import Juvix.Prelude hiding (First, Product)
 
 {-
   The following datatypes correspond to GEB types for terms
@@ -15,66 +19,68 @@ data Case = Case
   { _caseLeftType :: Object,
     _caseRightType :: Object,
     _caseCodomainType :: Object,
-    _caseOn :: Geb,
-    _caseLeft :: Geb,
-    _caseRight :: Geb
+    _caseOn :: Morphism,
+    _caseLeft :: Morphism,
+    _caseRight :: Morphism
   }
 
 data Pair = Pair
   { _pairLeftType :: Object,
     _pairRightType :: Object,
-    _pairLeft :: Geb,
-    _pairRight :: Geb
+    _pairLeft :: Morphism,
+    _pairRight :: Morphism
   }
 
-data Fst = Fst
-  { _fstLeftType :: Object,
-    _fstRightType :: Object,
-    _fstValue :: Geb
+data First = First
+  { _firstLeftType :: Object,
+    _firstRightType :: Object,
+    _firstValue :: Morphism
   }
 
-data Snd = Snd
-  { _sndLeftType :: Object,
-    _sndRightType :: Object,
-    _sndValue :: Geb
+data Second = Second
+  { _secondLeftType :: Object,
+    _secondRightType :: Object,
+    _secondValue :: Morphism
   }
 
-data Lamb = Lamb
-  { _lambVarType :: Object,
-    _lambBodyType :: Object,
-    _lambBody :: Geb
+data Lambda = Lambda
+  { _lambdaVarType :: Object,
+    _lambdaBodyType :: Object,
+    _lambdaBody :: Morphism
   }
 
-data App = App
-  { _appDomainType :: Object,
-    _appCodomainType :: Object,
-    _appLeft :: Geb,
-    _appRight :: Geb
+data Application = Application
+  { _applicationDomainType :: Object,
+    _applicationCodomainType :: Object,
+    _applicationLeft :: Morphism,
+    _applicationRight :: Morphism
   }
 
--- | Corresponds to the GEB type for terms: `stlc`
+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 Geb
-  = GebAbsurd Geb
-  | GebUnit
-  | GebLeft Geb
-  | GebRight Geb
-  | GebCase Case
-  | GebPair Pair
-  | GebFst Fst
-  | GebSnd Snd
-  | GebLamb Lamb
-  | GebApp App
-  | GebVar Int
-
-data Prod = Prod
-  { _prodLeft :: Object,
-    _prodRight :: Object
+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 Coprod = Coprod
-  { _coprodLeft :: Object,
-    _coprodRight :: Object
+data Coproduct = Coproduct
+  { _coproductLeft :: Object,
+    _coproductRight :: Object
   }
 
 -- | Function type
@@ -86,42 +92,46 @@ data Hom = Hom
 -- | 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
-  = ObjectInitial -- empty type
-  | ObjectTerminal -- unit type
-  | ObjectProd Prod
-  | ObjectCoprod Coprod
-  | ObjectHom Hom -- function type
-
-instance HasAtomicity Geb where
+  = -- | empty type
+    ObjectInitial
+  | -- | unit type
+    ObjectTerminal
+  | ObjectProduct Product
+  | ObjectCoproduct Coproduct
+  | -- | function type
+    ObjectHom Hom
+
+instance HasAtomicity Morphism where
   atomicity = \case
-    GebAbsurd {} -> Aggregate appFixity
-    GebUnit -> Atom
-    GebLeft {} -> Aggregate appFixity
-    GebRight {} -> Aggregate appFixity
-    GebCase {} -> Aggregate appFixity
-    GebPair {} -> Aggregate appFixity
-    GebFst {} -> Aggregate appFixity
-    GebSnd {} -> Aggregate appFixity
-    GebLamb {} -> Aggregate appFixity
-    GebApp {} -> Aggregate appFixity
-    GebVar {} -> Aggregate appFixity
+    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
-    ObjectProd {} -> Aggregate appFixity
-    ObjectCoprod {} -> Aggregate appFixity
+    ObjectProduct {} -> Aggregate appFixity
+    ObjectCoproduct {} -> Aggregate appFixity
     ObjectHom {} -> Aggregate appFixity
 
 makeLenses ''Case
 makeLenses ''Pair
-makeLenses ''Fst
-makeLenses ''Snd
-makeLenses ''Lamb
-makeLenses ''App
-makeLenses ''Geb
-makeLenses ''Prod
-makeLenses ''Coprod
+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/Base.hs

@@ -9,7 +9,6 @@ import Juvix.Compiler.Backend.Geb.Language
 import Juvix.Compiler.Backend.Geb.Pretty.Options
 import Juvix.Data.CodeAnn
 import Juvix.Extra.Strings qualified as Str
-import Juvix.Prelude
 
 doc :: (HasAtomicity c, PrettyCode c) => Options -> c -> Doc Ann
 doc opts x =
@@ -40,66 +39,71 @@ instance PrettyCode Pair where
     right <- ppArg _pairRight
     return $ kwPair <+> lty <+> rty <+> left <+> right
 
-instance PrettyCode Fst where
-  ppCode Fst {..} = do
-    lty <- ppArg _fstLeftType
-    rty <- ppArg _fstRightType
-    val <- ppArg _fstValue
+instance PrettyCode First where
+  ppCode First {..} = do
+    lty <- ppArg _firstLeftType
+    rty <- ppArg _firstRightType
+    val <- ppArg _firstValue
     return $ kwFst <+> lty <+> rty <+> val
 
-instance PrettyCode Snd where
-  ppCode Snd {..} = do
-    lty <- ppArg _sndLeftType
-    rty <- ppArg _sndRightType
-    val <- ppArg _sndValue
+instance PrettyCode Second where
+  ppCode Second {..} = do
+    lty <- ppArg _secondLeftType
+    rty <- ppArg _secondRightType
+    val <- ppArg _secondValue
     return $ kwSnd <+> lty <+> rty <+> val
 
-instance PrettyCode Lamb where
-  ppCode Lamb {..} = do
-    vty <- ppArg _lambVarType
-    bty <- ppArg _lambBodyType
-    body <- ppArg _lambBody
+instance PrettyCode Lambda where
+  ppCode Lambda {..} = do
+    vty <- ppArg _lambdaVarType
+    bty <- ppArg _lambdaBodyType
+    body <- ppArg _lambdaBody
     return $ kwLamb <+> vty <+> bty <+> body
 
-instance PrettyCode App where
-  ppCode App {..} = do
-    dom <- ppArg _appDomainType
-    cod <- ppArg _appCodomainType
-    left <- ppArg _appLeft
-    right <- ppArg _appRight
+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 Geb where
+instance PrettyCode Var where
+  ppCode Var {..} = return $ annotate AnnLiteralInteger (pretty _varIndex)
+
+instance PrettyCode Morphism where
   ppCode = \case
-    GebAbsurd val -> do
+    MorphismAbsurd val -> do
       v <- ppArg val
       return $ kwAbsurd <+> v
-    GebUnit ->
+    MorphismUnit ->
       return kwUnit
-    GebLeft val -> do
+    MorphismLeft val -> do
       v <- ppArg val
       return $ kwLeft <+> v
-    GebRight val -> do
+    MorphismRight val -> do
       v <- ppArg val
       return $ kwRight <+> v
-    GebCase x -> ppCode x
-    GebPair x -> ppCode x
-    GebFst x -> ppCode x
-    GebSnd x -> ppCode x
-    GebLamb x -> ppCode x
-    GebApp x -> ppCode x
-    GebVar idx -> return $ kwVar <+> annotate AnnLiteralInteger (pretty idx)
-
-instance PrettyCode Prod where
-  ppCode Prod {..} = do
-    left <- ppArg _prodLeft
-    right <- ppArg _prodRight
+    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 Coprod where
-  ppCode Coprod {..} = do
-    left <- ppArg _coprodLeft
-    right <- ppArg _coprodRight
+instance PrettyCode Coproduct where
+  ppCode Coproduct {..} = do
+    left <- ppArg _coproductLeft
+    right <- ppArg _coproductRight
     return $ kwCoprod <+> left <+> right
 
 instance PrettyCode Hom where
@@ -112,8 +116,8 @@ instance PrettyCode Object where
   ppCode = \case
     ObjectInitial -> return kwInitial
     ObjectTerminal -> return kwTerminal
-    ObjectProd x -> ppCode x
-    ObjectCoprod x -> ppCode x
+    ObjectProduct x -> ppCode x
+    ObjectCoproduct x -> ppCode x
     ObjectHom x -> ppCode x
 
 --------------------------------------------------------------------------------

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

@@ -2,23 +2,17 @@ module Juvix.Compiler.Backend.Geb.Pretty.Options where
 
 import Juvix.Prelude
 
-newtype Options = Options
-  { _optIndent :: Int
-  }
+-- 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
-    { _optIndent = 2
-    }
+defaultOptions = Options
 
 traceOptions :: Options
-traceOptions =
-  Options
-    { _optIndent = 2
-    }
+traceOptions = Options
 
 fromGenericOptions :: GenericOptions -> Options
 fromGenericOptions _ = defaultOptions

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

@@ -1,13 +1,16 @@
-module Juvix.Compiler.Backend.Geb.Translation (module Juvix.Compiler.Backend.Geb.Translation, module Juvix.Compiler.Backend.Geb.Translation.FromCore) where
+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
-import Juvix.Prelude
 
 newtype Result = Result
   { _resultCode :: Text
   }
 
-toResult :: Geb -> Result
+toResult :: Morphism -> Result
 toResult geb = Result (ppPrint geb <> "\n")