From 8659b386e5d2c8e66c5a6ef63f11381dba1c8892 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 31 Jan 2023 16:05:44 +0100 Subject: [PATCH] address review comments --- src/Juvix/Compiler/Backend/Geb/Extra.hs | 8 +- src/Juvix/Compiler/Backend/Geb/Language.hs | 152 ++++++------ src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs | 94 ++++---- .../Compiler/Backend/Geb/Pretty/Options.hs | 16 +- src/Juvix/Compiler/Backend/Geb/Translation.hs | 9 +- .../Backend/Geb/Translation/FromCore.hs | 217 +++++++++--------- 6 files changed, 254 insertions(+), 242 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Geb/Extra.hs b/src/Juvix/Compiler/Backend/Geb/Extra.hs index b18cda5476..1ba05a2d45 100644 --- a/src/Juvix/Compiler/Backend/Geb/Extra.hs +++ b/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] diff --git a/src/Juvix/Compiler/Backend/Geb/Language.hs b/src/Juvix/Compiler/Backend/Geb/Language.hs index aa97fe3acd..63611ea066 100644 --- a/src/Juvix/Compiler/Backend/Geb/Language.hs +++ b/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 diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs index edbb6c2edd..86543095ed 100644 --- a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs +++ b/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 -------------------------------------------------------------------------------- diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs index 2598029409..b6123a31ac 100644 --- a/src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs +++ b/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 diff --git a/src/Juvix/Compiler/Backend/Geb/Translation.hs b/src/Juvix/Compiler/Backend/Geb/Translation.hs index 425910db2f..ff811337ec 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation.hs +++ b/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") diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs index 9c269be75e..236357267a 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs @@ -9,9 +9,8 @@ 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 -import Juvix.Prelude -fromCore :: Core.InfoTable -> Geb +fromCore :: Core.InfoTable -> Morphism fromCore tab = case tab ^. Core.infoMain of Just sym -> let node = fromJust $ HashMap.lookup sym (tab ^. Core.identContext) @@ -43,15 +42,15 @@ fromCore tab = case tab ^. Core.infoMain of (\a -> (\f -> (\g -> g (g a)) (\x -> f (f x))) (\x -> F)) a ``` -} - goIdents :: HashMap Symbol Level -> Level -> [Level] -> Core.Node -> [Core.IdentifierInfo] -> Geb + goIdents :: HashMap Symbol Level -> Level -> [Level] -> Core.Node -> [Core.IdentifierInfo] -> Morphism goIdents identMap level shiftLevels node = \case ii : idents -> - GebApp - App - { _appDomainType = argty, - _appCodomainType = nodeType, - _appLeft = lamb, - _appRight = convertNode identMap 0 shiftLevels fundef + MorphismApplication + Application + { _applicationDomainType = argty, + _applicationCodomainType = nodeType, + _applicationLeft = lamb, + _applicationRight = convertNode identMap 0 shiftLevels fundef } where sym = ii ^. Core.identifierSymbol @@ -59,11 +58,11 @@ fromCore tab = case tab ^. Core.infoMain of argty = convertType (Info.getNodeType fundef) body = goIdents (HashMap.insert sym level identMap) (level + 1) (0 : shiftLevels) node idents lamb = - GebLamb - Lamb - { _lambVarType = argty, - _lambBodyType = nodeType, - _lambBody = body + MorphismLambda + Lambda + { _lambdaVarType = argty, + _lambdaBodyType = nodeType, + _lambdaBody = body } [] -> convertNode identMap 0 shiftLevels node @@ -72,7 +71,7 @@ fromCore tab = case tab ^. Core.infoMain of -- `shiftLevels` contains the de Bruijn levels immediately before which a -- binder was inserted - convertNode :: HashMap Symbol Level -> Level -> [Level] -> Core.Node -> Geb + 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 @@ -96,43 +95,43 @@ fromCore tab = case tab ^. Core.infoMain of insertedBinders varsNum shiftLevels idx = length (filter ((varsNum - idx) <=) shiftLevels) - convertVar :: HashMap Symbol Level -> Level -> [Level] -> Core.Var -> Geb + convertVar :: HashMap Symbol Level -> Level -> [Level] -> Core.Var -> Morphism convertVar _ varsNum shiftLevels Core.Var {..} = - GebVar (_varIndex + insertedBinders varsNum shiftLevels _varIndex) + MorphismVar (Var (_varIndex + insertedBinders varsNum shiftLevels _varIndex)) - convertIdent :: HashMap Symbol Level -> Level -> [Level] -> Core.Ident -> Geb + convertIdent :: HashMap Symbol Level -> Level -> [Level] -> Core.Ident -> Morphism convertIdent identMap varsNum shiftLevels Core.Ident {..} = - GebVar (varsNum + length shiftLevels - fromJust (HashMap.lookup _identSymbol identMap) - 1) + MorphismVar (Var (varsNum + length shiftLevels - fromJust (HashMap.lookup _identSymbol identMap) - 1)) - convertConstant :: HashMap Symbol Level -> Level -> [Level] -> Core.Constant -> Geb + convertConstant :: HashMap Symbol Level -> Level -> [Level] -> Core.Constant -> Morphism convertConstant _ _ _ Core.Constant {} = unsupported - convertApp :: HashMap Symbol Level -> Level -> [Level] -> Core.App -> Geb + convertApp :: HashMap Symbol Level -> Level -> [Level] -> Core.App -> Morphism convertApp identMap varsNum shiftLevels Core.App {..} = - GebApp - App - { _appDomainType = convertType (Info.getNodeType _appRight), - _appCodomainType = convertType (Info.getInfoType _appInfo), - _appLeft = convertNode identMap varsNum shiftLevels _appLeft, - _appRight = convertNode identMap varsNum shiftLevels _appRight + 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 -> Geb + convertBuiltinApp :: HashMap Symbol Level -> Level -> [Level] -> Core.BuiltinApp -> Morphism convertBuiltinApp _ _ _ Core.BuiltinApp {} = unsupported - convertConstr :: HashMap Symbol Level -> Level -> [Level] -> Core.Constr -> Geb + convertConstr :: HashMap Symbol Level -> Level -> [Level] -> Core.Constr -> Morphism convertConstr identMap varsNum shiftLevels Core.Constr {..} = - foldr ($) prod (replicate tagNum GebRight) + 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 GebLeft) + (if tagNum == length ctrs - 1 then id else MorphismLeft) (convertProduct identMap varsNum shiftLevels _constrArgs) - convertProduct :: HashMap Symbol Level -> Level -> [Level] -> [Core.Node] -> Geb + convertProduct :: HashMap Symbol Level -> Level -> [Level] -> [Core.Node] -> Morphism convertProduct identMap varsNum shiftLevels args = case reverse args of h : t -> fst $ @@ -141,68 +140,68 @@ fromCore tab = case tab ^. Core.infoMain of (convertNode identMap varsNum shiftLevels h, convertType (Info.getNodeType h)) (reverse t) [] -> - GebUnit + MorphismUnit where - mkPair :: (Geb, Object) -> (Geb, Object) -> (Geb, Object) + mkPair :: (Morphism, Object) -> (Morphism, Object) -> (Morphism, Object) mkPair (x, xty) (y, yty) = (z, zty) where z = - GebPair + MorphismPair Pair { _pairLeftType = xty, _pairRightType = yty, _pairLeft = x, _pairRight = y } - zty = ObjectProd (Prod xty yty) + zty = ObjectProduct (Product xty yty) - convertLet :: HashMap Symbol Level -> Level -> [Level] -> Core.Let -> Geb + convertLet :: HashMap Symbol Level -> Level -> [Level] -> Core.Let -> Morphism convertLet identMap varsNum shiftLevels Core.Let {..} = - GebApp - App - { _appCodomainType = domty, - _appDomainType = codty, - _appLeft = - GebLamb - Lamb - { _lambVarType = domty, - _lambBodyType = codty, - _lambBody = convertNode identMap varsNum shiftLevels _letBody + MorphismApplication + Application + { _applicationCodomainType = domty, + _applicationDomainType = codty, + _applicationLeft = + MorphismLambda + Lambda + { _lambdaVarType = domty, + _lambdaBodyType = codty, + _lambdaBody = convertNode identMap varsNum shiftLevels _letBody }, - _appRight = convertNode identMap varsNum shiftLevels (_letItem ^. Core.letItemValue) + _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 -> Geb + convertLambda :: HashMap Symbol Level -> Level -> [Level] -> Core.Lambda -> Morphism convertLambda identMap varsNum shiftLevels Core.Lambda {..} = - GebLamb - Lamb - { _lambVarType = convertType (_lambdaBinder ^. Core.binderType), - _lambBodyType = convertType (Info.getNodeType _lambdaBody), - _lambBody = convertNode identMap (varsNum + 1) shiftLevels _lambdaBody + 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 -> Geb + convertCase :: HashMap Symbol Level -> Level -> [Level] -> Core.Case -> Morphism convertCase identMap varsNum shiftLevels Core.Case {..} = if | null branches -> - GebAbsurd (convertNode identMap varsNum shiftLevels _caseValue) + MorphismAbsurd (convertNode identMap varsNum shiftLevels _caseValue) | missingCtrsNum > 1 -> let ty = convertType (Info.getNodeType defaultNode) - in GebApp - App - { _appDomainType = ty, - _appCodomainType = ty, - _appLeft = - GebLamb - Lamb - { _lambVarType = ty, - _lambBodyType = ty, - _lambBody = go indty (varsNum : shiftLevels) _caseValue branches + in MorphismApplication + Application + { _applicationDomainType = ty, + _applicationCodomainType = ty, + _applicationLeft = + MorphismLambda + Lambda + { _lambdaVarType = ty, + _lambdaBodyType = ty, + _lambdaBody = go indty (varsNum : shiftLevels) _caseValue branches }, - _appRight = convertNode identMap varsNum shiftLevels defaultNode + _applicationRight = convertNode identMap varsNum shiftLevels defaultNode } | otherwise -> go indty shiftLevels _caseValue branches where @@ -240,40 +239,40 @@ fromCore tab = case tab ^. Core.infoMain of | missingCtrsNum > 1 -> Core.mkVar' | otherwise -> (`Core.shift` defaultNode) - go :: Object -> [Level] -> Core.Node -> [Core.CaseBranch] -> Geb + 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 -> - GebCase + MorphismCase Case { _caseLeftType = lty, _caseRightType = rty, _caseCodomainType = codty, _caseOn = convertNode identMap varsNum lvls val, _caseLeft = - GebLamb - Lamb - { _lambVarType = lty, - _lambBodyType = codty, - _lambBody = mkBranch lty (varsNum : lvls) val br + MorphismLambda + Lambda + { _lambdaVarType = lty, + _lambdaBodyType = codty, + _lambdaBody = mkBranch lty (varsNum : lvls) val br }, _caseRight = - GebLamb - Lamb - { _lambVarType = rty, - _lambBodyType = codty, - _lambBody = go rty (varsNum : lvls) (Core.mkVar' 0) brs + MorphismLambda + Lambda + { _lambdaVarType = rty, + _lambdaBodyType = codty, + _lambdaBody = go rty (varsNum : lvls) (Core.mkVar' 0) brs } } where (lty, rty) = case ty of - ObjectCoprod Coprod {..} -> (_coprodLeft, _coprodRight) + ObjectCoproduct Coproduct {..} -> (_coproductLeft, _coproductRight) _ -> impossible [] -> impossible - mkBranch :: Object -> [Level] -> Core.Node -> Core.CaseBranch -> Geb + mkBranch :: Object -> [Level] -> Core.Node -> Core.CaseBranch -> Morphism mkBranch valty lvls val Core.CaseBranch {..} = if | _caseBranchBindersNum == 0 -> @@ -282,54 +281,54 @@ fromCore tab = case tab ^. Core.infoMain of mkApps (mkLambs argtys) (convertNode identMap varsNum lvls val) valty argtys where branch = convertNode identMap (varsNum + _caseBranchBindersNum) lvls _caseBranchBody - argtys = destructProd valty + argtys = destructProduct valty - mkApps :: Geb -> Geb -> Object -> [Object] -> Geb + mkApps :: Morphism -> Morphism -> Object -> [Object] -> Morphism mkApps acc v vty = \case ty : tys -> mkApps acc' v' rty tys where v' = - GebSnd - Snd - { _sndLeftType = lty, - _sndRightType = rty, - _sndValue = v + MorphismSecond + Second + { _secondLeftType = lty, + _secondRightType = rty, + _secondValue = v } acc' = - GebApp - App - { _appDomainType = ty, - _appCodomainType = vty, - _appLeft = acc, - _appRight = + MorphismApplication + Application + { _applicationDomainType = ty, + _applicationCodomainType = vty, + _applicationLeft = acc, + _applicationRight = if | null tys -> v | otherwise -> - GebFst - Fst - { _fstLeftType = lty, - _fstRightType = rty, - _fstValue = v + MorphismFirst + First + { _firstLeftType = lty, + _firstRightType = rty, + _firstValue = v } } (lty, rty) = case vty of - ObjectProd Prod {..} -> (_prodLeft, _prodRight) + ObjectProduct Product {..} -> (_productLeft, _productRight) _ -> impossible [] -> acc - mkLambs :: [Object] -> Geb + mkLambs :: [Object] -> Morphism mkLambs = fst . foldr ( \ty (acc, accty) -> - ( GebLamb - Lamb - { _lambVarType = ty, - _lambBodyType = accty, - _lambBody = acc + ( MorphismLambda + Lambda + { _lambdaVarType = ty, + _lambdaBodyType = accty, + _lambdaBody = acc }, ObjectHom (Hom ty accty) ) @@ -368,7 +367,7 @@ fromCore tab = case tab ^. Core.infoMain of convertTypePrim Core.TypePrim {..} = case _typePrimPrimitive of Core.PrimInteger _ -> unsupported - Core.PrimBool _ -> ObjectCoprod (Coprod ObjectTerminal ObjectTerminal) + Core.PrimBool _ -> ObjectCoproduct (Coproduct ObjectTerminal ObjectTerminal) Core.PrimString -> unsupported convertInductive :: Symbol -> Object @@ -376,7 +375,7 @@ fromCore tab = case tab ^. Core.infoMain of case reverse ctrs of ci : ctrs' -> foldr - (\x acc -> ObjectCoprod (Coprod (convertConstructorType (x ^. Core.constructorType)) acc)) + (\x acc -> ObjectCoproduct (Coproduct (convertConstructorType (x ^. Core.constructorType)) acc)) (convertConstructorType (ci ^. Core.constructorType)) (reverse ctrs') [] -> @@ -391,7 +390,7 @@ fromCore tab = case tab ^. Core.infoMain of case reverse (Core.typeArgs ty) of hty : tys -> foldr - (\x acc -> ObjectProd (Prod (convertType x) acc)) + (\x acc -> ObjectProduct (Product (convertType x) acc)) (convertType hty) (reverse tys) [] ->