From 61df63dd75f2179317c297ed699d80b68ceaecef Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 23 Jan 2023 15:26:00 +0100 Subject: [PATCH 01/20] Geb data structures and S-expression output --- src/Juvix/Compiler/Asm/Pretty/Base.hs | 6 - src/Juvix/Compiler/Backend/Geb/Language.hs | 104 ++++++++++ src/Juvix/Compiler/Backend/Geb/Pretty.hs | 28 +++ src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs | 188 ++++++++++++++++++ .../Compiler/Backend/Geb/Pretty/Options.hs | 27 +++ .../Backend/Geb/Translation/FromCore.hs | 1 + src/Juvix/Compiler/Core/Info/TypeInfo.hs | 30 +++ src/Juvix/Compiler/Core/Pretty/Base.hs | 6 - src/Juvix/Data/CodeAnn.hs | 3 + src/Juvix/Extra/Strings.hs | 47 ++++- 10 files changed, 427 insertions(+), 13 deletions(-) create mode 100644 src/Juvix/Compiler/Backend/Geb/Language.hs create mode 100644 src/Juvix/Compiler/Backend/Geb/Pretty.hs create mode 100644 src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs create mode 100644 src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs create mode 100644 src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs create mode 100644 src/Juvix/Compiler/Core/Info/TypeInfo.hs diff --git a/src/Juvix/Compiler/Asm/Pretty/Base.hs b/src/Juvix/Compiler/Asm/Pretty/Base.hs index 08fbadd05c..4deb9d2a9e 100644 --- a/src/Juvix/Compiler/Asm/Pretty/Base.hs +++ b/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) diff --git a/src/Juvix/Compiler/Backend/Geb/Language.hs b/src/Juvix/Compiler/Backend/Geb/Language.hs new file mode 100644 index 0000000000..bd3ef84afc --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Language.hs @@ -0,0 +1,104 @@ +module Juvix.Compiler.Backend.Geb.Language where + +import Juvix.Prelude + +{- + 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). +-} + +data Case = Case { + _caseLeftType :: Type, + _caseRightType :: Type, + _caseCodomainType :: Type, + _caseOn :: Geb, + _caseLeft :: Geb, + _caseRight :: Geb +} + +data Pair = Pair { + _pairLeftType :: Type, + _pairRightType :: Type, + _pairLeft :: Geb, + _pairRight :: Geb +} + +data Fst = Fst { + _fstLeftType :: Type, + _fstRightType :: Type, + _fstValue :: Geb +} + +data Snd = Snd { + _sndLeftType :: Type, + _sndRightType :: Type, + _sndValue :: Geb +} + +data Lamb = Lamb { + _lambVarType :: Type, + _lambBodyType :: Type, + _lambBody :: Geb +} + +data App = App { + _appDomainType :: Type, + _appCodomainType :: Type, + _appLeft :: Geb, + _appRight :: Geb +} + +-- | Corresponds to the GEB type for 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 :: Type, + _prodRight :: Type +} + +data Coprod = Coprod { + _coprodLeft :: Type, + _coprodRight :: Type +} + +-- | Corresponds to a subset of the GEB type `substobj` +-- (https://github.com/anoma/geb/blob/main/src/specs/geb.lisp). +data Type + = TypeInitial -- the empty type + | TypeTerminal -- the unit type + | TypeProd Prod + | TypeCoprod Coprod + +instance HasAtomicity Geb 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 + +instance HasAtomicity Type where + atomicity = \case + TypeInitial -> Atom + TypeTerminal -> Atom + TypeProd {} -> Aggregate appFixity + TypeCoprod {} -> Aggregate appFixity diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty.hs b/src/Juvix/Compiler/Backend/Geb/Pretty.hs new file mode 100644 index 0000000000..3c03d6d1c0 --- /dev/null +++ b/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 :: PrettyCode c => c -> AnsiText +ppOutDefault = AnsiText . PPOutput . doc defaultOptions + +ppOut :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> AnsiText +ppOut o = AnsiText . PPOutput . doc (project o) + +ppTrace' :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> Text +ppTrace' opts = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc (project opts) + +ppTrace :: PrettyCode c => c -> Text +ppTrace = ppTrace' traceOptions + +ppPrint :: PrettyCode c => c -> Text +ppPrint = show . ppOutDefault diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs new file mode 100644 index 0000000000..8e390407fc --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs @@ -0,0 +1,188 @@ +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.Prelude +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 :: PrettyCode c => Options -> c -> Doc Ann +doc opts = + run + . runReader opts + . ppCode + +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 + val <- ppArg _caseOn + left <- ppArg _caseLeft + right <- ppArg _caseRight + return $ kwCase <+> lty <+> rty <+> 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 Fst where + ppCode Fst {..} = do + lty <- ppArg _fstLeftType + rty <- ppArg _fstRightType + val <- ppArg _fstValue + return $ kwFst <+> lty <+> rty <+> val + +instance PrettyCode Snd where + ppCode Snd {..} = do + lty <- ppArg _sndLeftType + rty <- ppArg _sndRightType + val <- ppArg _sndValue + return $ kwSnd <+> lty <+> rty <+> val + +instance PrettyCode Lamb where + ppCode Lamb {..} = do + vty <- ppArg _lambVarType + bty <- ppArg _lambBodyType + body <- ppArg _lambBody + return $ kwLamb <+> vty <+> bty <+> body + +instance PrettyCode App where + ppCode App {..} = do + dom <- ppArg _appDomainType + cod <- ppArg _appCodomainType + left <- ppArg _appLeft + right <- ppArg _appRight + return $ kwApp <+> dom <+> cod <+> left <+> right + +instance PrettyCode Geb where + ppCode = \case + GebAbsurd val -> do + v <- ppArg val + return $ kwAbsurd <+> v + GebUnit -> + return kwUnit + GebLeft val -> do + v <- ppArg val + return $ kwLeft <+> v + GebRight 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 + return $ kwProd <+> left <+> right + +instance PrettyCode Coprod where + ppCode Coprod {..} = do + left <- ppArg _coprodLeft + right <- ppArg _coprodRight + return $ kwCoprod <+> left <+> right + +instance PrettyCode Type where + ppCode = \case + TypeInitial -> return kwInitial + TypeTerminal -> return kwTerminal + TypeProd x -> ppCode x + TypeCoprod 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 diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs new file mode 100644 index 0000000000..2598029409 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs @@ -0,0 +1,27 @@ +module Juvix.Compiler.Backend.Geb.Pretty.Options where + +import Juvix.Prelude + +newtype Options = Options + { _optIndent :: Int + } + +makeLenses ''Options + +defaultOptions :: Options +defaultOptions = + Options + { _optIndent = 2 + } + +traceOptions :: Options +traceOptions = + Options + { _optIndent = 2 + } + +fromGenericOptions :: GenericOptions -> Options +fromGenericOptions _ = defaultOptions + +instance CanonicalProjection GenericOptions Options where + project = fromGenericOptions diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs new file mode 100644 index 0000000000..adc95c60e1 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs @@ -0,0 +1 @@ +module Juvix.Compiler.Backend.Geb.Translation.FromCore where diff --git a/src/Juvix/Compiler/Core/Info/TypeInfo.hs b/src/Juvix/Compiler/Core/Info/TypeInfo.hs new file mode 100644 index 0000000000..571c5c8c3c --- /dev/null +++ b/src/Juvix/Compiler/Core/Info/TypeInfo.hs @@ -0,0 +1,30 @@ +module Juvix.Compiler.Core.Info.TypeInfo where + +import Juvix.Compiler.Core.Info qualified as Info +import Juvix.Compiler.Core.Language +import Juvix.Compiler.Core.Extra +import Juvix.Compiler.Core.Data.InfoTable + +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 + +removeTypeInfo :: Node -> Node +removeTypeInfo = removeInfo kTypeInfo + +inferTypeInfo :: InfoTable -> Node -> Node +inferTypeInfo _ = umap id -- TODO: store the type of each node in its info diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 4e93b8b66d..1ff66c0bd7 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/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 -> diff --git a/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs index 07d3db9a07..fa593e08f2 100644 --- a/src/Juvix/Data/CodeAnn.hs +++ b/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 diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index ef4df4e0d0..2d861d29fb 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -542,7 +542,52 @@ 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" + +juvixFunctionT :: IsString s => s juvixFunctionT = "juvix_function_t" juvixDotOrg :: (IsString s) => s From a56f6d2973f4b9944024d8667ec3f38c40b350df Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 23 Jan 2023 15:26:21 +0100 Subject: [PATCH 02/20] make ormolu happy --- src/Juvix/Compiler/Backend/Geb/Language.hs | 86 +++++++++---------- src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs | 2 +- src/Juvix/Compiler/Core/Info/TypeInfo.hs | 4 +- 3 files changed, 46 insertions(+), 46 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Geb/Language.hs b/src/Juvix/Compiler/Backend/Geb/Language.hs index bd3ef84afc..958e0a0950 100644 --- a/src/Juvix/Compiler/Backend/Geb/Language.hs +++ b/src/Juvix/Compiler/Backend/Geb/Language.hs @@ -8,46 +8,46 @@ import Juvix.Prelude (https://github.com/anoma/geb/blob/main/src/specs/geb.lisp). -} -data Case = Case { - _caseLeftType :: Type, - _caseRightType :: Type, - _caseCodomainType :: Type, - _caseOn :: Geb, - _caseLeft :: Geb, - _caseRight :: Geb -} +data Case = Case + { _caseLeftType :: Type, + _caseRightType :: Type, + _caseCodomainType :: Type, + _caseOn :: Geb, + _caseLeft :: Geb, + _caseRight :: Geb + } -data Pair = Pair { - _pairLeftType :: Type, - _pairRightType :: Type, - _pairLeft :: Geb, - _pairRight :: Geb -} +data Pair = Pair + { _pairLeftType :: Type, + _pairRightType :: Type, + _pairLeft :: Geb, + _pairRight :: Geb + } -data Fst = Fst { - _fstLeftType :: Type, - _fstRightType :: Type, - _fstValue :: Geb -} +data Fst = Fst + { _fstLeftType :: Type, + _fstRightType :: Type, + _fstValue :: Geb + } -data Snd = Snd { - _sndLeftType :: Type, - _sndRightType :: Type, - _sndValue :: Geb -} +data Snd = Snd + { _sndLeftType :: Type, + _sndRightType :: Type, + _sndValue :: Geb + } -data Lamb = Lamb { - _lambVarType :: Type, - _lambBodyType :: Type, - _lambBody :: Geb -} +data Lamb = Lamb + { _lambVarType :: Type, + _lambBodyType :: Type, + _lambBody :: Geb + } -data App = App { - _appDomainType :: Type, - _appCodomainType :: Type, - _appLeft :: Geb, - _appRight :: Geb -} +data App = App + { _appDomainType :: Type, + _appCodomainType :: Type, + _appLeft :: Geb, + _appRight :: Geb + } -- | Corresponds to the GEB type for terms: `stlc` -- (https://github.com/anoma/geb/blob/main/src/specs/lambda.lisp). @@ -64,15 +64,15 @@ data Geb | GebApp App | GebVar Int -data Prod = Prod { - _prodLeft :: Type, - _prodRight :: Type -} +data Prod = Prod + { _prodLeft :: Type, + _prodRight :: Type + } -data Coprod = Coprod { - _coprodLeft :: Type, - _coprodRight :: Type -} +data Coprod = Coprod + { _coprodLeft :: Type, + _coprodRight :: Type + } -- | Corresponds to a subset of the GEB type `substobj` -- (https://github.com/anoma/geb/blob/main/src/specs/geb.lisp). diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs index 8e390407fc..9b1cba2b59 100644 --- a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs @@ -5,11 +5,11 @@ module Juvix.Compiler.Backend.Geb.Pretty.Base ) where -import Juvix.Prelude 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 :: PrettyCode c => Options -> c -> Doc Ann doc opts = diff --git a/src/Juvix/Compiler/Core/Info/TypeInfo.hs b/src/Juvix/Compiler/Core/Info/TypeInfo.hs index 571c5c8c3c..0c2e3cc5c4 100644 --- a/src/Juvix/Compiler/Core/Info/TypeInfo.hs +++ b/src/Juvix/Compiler/Core/Info/TypeInfo.hs @@ -1,9 +1,9 @@ module Juvix.Compiler.Core.Info.TypeInfo where +import Juvix.Compiler.Core.Data.InfoTable +import Juvix.Compiler.Core.Extra import Juvix.Compiler.Core.Info qualified as Info import Juvix.Compiler.Core.Language -import Juvix.Compiler.Core.Extra -import Juvix.Compiler.Core.Data.InfoTable newtype TypeInfo = TypeInfo {_infoType :: Type} From 01a1530d26994e5d3938022a191a7f7ae25da5fd Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 23 Jan 2023 16:45:29 +0100 Subject: [PATCH 03/20] Adjustments after conversation with Terence --- src/Juvix/Compiler/Backend/Geb/Language.hs | 64 +++++++++++-------- src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs | 20 ++++-- src/Juvix/Extra/Strings.hs | 3 + 3 files changed, 54 insertions(+), 33 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Geb/Language.hs b/src/Juvix/Compiler/Backend/Geb/Language.hs index 958e0a0950..7bc35d5a94 100644 --- a/src/Juvix/Compiler/Backend/Geb/Language.hs +++ b/src/Juvix/Compiler/Backend/Geb/Language.hs @@ -9,42 +9,42 @@ import Juvix.Prelude -} data Case = Case - { _caseLeftType :: Type, - _caseRightType :: Type, - _caseCodomainType :: Type, + { _caseLeftType :: Obj, + _caseRightType :: Obj, + _caseCodomainType :: Obj, _caseOn :: Geb, _caseLeft :: Geb, _caseRight :: Geb } data Pair = Pair - { _pairLeftType :: Type, - _pairRightType :: Type, + { _pairLeftType :: Obj, + _pairRightType :: Obj, _pairLeft :: Geb, _pairRight :: Geb } data Fst = Fst - { _fstLeftType :: Type, - _fstRightType :: Type, + { _fstLeftType :: Obj, + _fstRightType :: Obj, _fstValue :: Geb } data Snd = Snd - { _sndLeftType :: Type, - _sndRightType :: Type, + { _sndLeftType :: Obj, + _sndRightType :: Obj, _sndValue :: Geb } data Lamb = Lamb - { _lambVarType :: Type, - _lambBodyType :: Type, + { _lambVarType :: Obj, + _lambBodyType :: Obj, _lambBody :: Geb } data App = App - { _appDomainType :: Type, - _appCodomainType :: Type, + { _appDomainType :: Obj, + _appCodomainType :: Obj, _appLeft :: Geb, _appRight :: Geb } @@ -65,22 +65,29 @@ data Geb | GebVar Int data Prod = Prod - { _prodLeft :: Type, - _prodRight :: Type + { _prodLeft :: Obj, + _prodRight :: Obj } data Coprod = Coprod - { _coprodLeft :: Type, - _coprodRight :: Type + { _coprodLeft :: Obj, + _coprodRight :: Obj } --- | Corresponds to a subset of the GEB type `substobj` +-- | Function type +data Hom = Hom + { _homDomain :: Obj, + _homCodomain :: Obj + } + +-- | Corresponds to the GEB type for types (objects of the category): `substobj` -- (https://github.com/anoma/geb/blob/main/src/specs/geb.lisp). -data Type - = TypeInitial -- the empty type - | TypeTerminal -- the unit type - | TypeProd Prod - | TypeCoprod Coprod +data Obj + = ObjInitial -- the empty type + | ObjTerminal -- the unit type + | ObjProd Prod + | ObjCoprod Coprod + | ObjHom Hom instance HasAtomicity Geb where atomicity = \case @@ -96,9 +103,10 @@ instance HasAtomicity Geb where GebApp {} -> Aggregate appFixity GebVar {} -> Aggregate appFixity -instance HasAtomicity Type where +instance HasAtomicity Obj where atomicity = \case - TypeInitial -> Atom - TypeTerminal -> Atom - TypeProd {} -> Aggregate appFixity - TypeCoprod {} -> Aggregate appFixity + ObjInitial -> Atom + ObjTerminal -> Atom + ObjProd {} -> Aggregate appFixity + ObjCoprod {} -> Aggregate appFixity + ObjHom {} -> Aggregate appFixity diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs index 9b1cba2b59..6611039f5d 100644 --- a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs @@ -99,12 +99,19 @@ instance PrettyCode Coprod where right <- ppArg _coprodRight return $ kwCoprod <+> left <+> right -instance PrettyCode Type where +instance PrettyCode Hom where + ppCode Hom {..} = do + dom <- ppArg _homDomain + cod <- ppArg _homCodomain + return $ kwHom <+> dom <+> cod + +instance PrettyCode Obj where ppCode = \case - TypeInitial -> return kwInitial - TypeTerminal -> return kwTerminal - TypeProd x -> ppCode x - TypeCoprod x -> ppCode x + ObjInitial -> return kwInitial + ObjTerminal -> return kwTerminal + ObjProd x -> ppCode x + ObjCoprod x -> ppCode x + ObjHom x -> ppCode x {--------------------------------------------------------------------------------} {- helper functions -} @@ -186,3 +193,6 @@ kwProd = keyword Str.gebProd kwCoprod :: Doc Ann kwCoprod = keyword Str.gebCoprod + +kwHom :: Doc Ann +kwHom = keyword Str.gebHom diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 2d861d29fb..3a7ec41fe2 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -587,6 +587,9 @@ gebProd = "prod" gebCoprod :: IsString s => s gebCoprod = "coprod" +gebHom :: IsString s => s +gebHom = "hom" + juvixFunctionT :: IsString s => s juvixFunctionT = "juvix_function_t" From 059a3832b79d1b473b2e37bb9a35fc18a966e9aa Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 23 Jan 2023 18:57:03 +0100 Subject: [PATCH 04/20] stubs --- src/Juvix/Compiler/Backend/Geb/Language.hs | 21 +++- .../Backend/Geb/Translation/FromCore.hs | 118 ++++++++++++++++++ .../Compiler/Core/Data/TransformationId.hs | 2 + .../Core/Data/TransformationId/Parser.hs | 8 ++ src/Juvix/Compiler/Core/Info/TypeInfo.hs | 13 +- src/Juvix/Compiler/Core/Pipeline.hs | 7 ++ src/Juvix/Compiler/Core/Transformation.hs | 4 + .../Core/Transformation/ComputeTypeInfo.hs | 12 ++ .../Core/Transformation/UnrollRecursion.hs | 7 ++ 9 files changed, 184 insertions(+), 8 deletions(-) create mode 100644 src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs create mode 100644 src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs diff --git a/src/Juvix/Compiler/Backend/Geb/Language.hs b/src/Juvix/Compiler/Backend/Geb/Language.hs index 7bc35d5a94..1186bea993 100644 --- a/src/Juvix/Compiler/Backend/Geb/Language.hs +++ b/src/Juvix/Compiler/Backend/Geb/Language.hs @@ -8,6 +8,9 @@ import Juvix.Prelude (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`, +-- `_caseLeftType` has the form `Dom -> _caseCodomainType` and `_caseRightType` +-- has the form `Dom -> _caseCodomainType`. data Case = Case { _caseLeftType :: Obj, _caseRightType :: Obj, @@ -83,11 +86,11 @@ 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 Obj - = ObjInitial -- the empty type - | ObjTerminal -- the unit type + = ObjInitial -- empty type + | ObjTerminal -- unit type | ObjProd Prod | ObjCoprod Coprod - | ObjHom Hom + | ObjHom Hom -- function type instance HasAtomicity Geb where atomicity = \case @@ -110,3 +113,15 @@ instance HasAtomicity Obj where ObjProd {} -> Aggregate appFixity ObjCoprod {} -> Aggregate appFixity ObjHom {} -> Aggregate appFixity + +makeLenses ''Case +makeLenses ''Pair +makeLenses ''Fst +makeLenses ''Snd +makeLenses ''Lamb +makeLenses ''App +makeLenses ''Geb +makeLenses ''Prod +makeLenses ''Coprod +makeLenses ''Hom +makeLenses ''Obj diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs index adc95c60e1..80c2acadd4 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs @@ -1 +1,119 @@ module Juvix.Compiler.Backend.Geb.Translation.FromCore where + +import Data.HashMap.Strict qualified as HashMap +import Juvix.Compiler.Backend.Geb.Language +import Juvix.Compiler.Core.Data.InfoTable qualified as Core +import Juvix.Compiler.Core.Info.TypeInfo qualified as Info +import Juvix.Compiler.Core.Language qualified as Core +import Juvix.Prelude + +{- + TODO: The translation of each identifier should be 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) + ``` + should be translated as: + ``` + (\a -> (\f -> (\g -> g (g a)) (\x -> f (f x))) (\x -> F')) a' + ``` +-} + +fromCore :: Core.InfoTable -> Core.Node -> Geb +fromCore tab = convertNode + where + unimplemented :: forall a. a + unimplemented = error "not yet implemented" + + unsupported :: forall a. a + unsupported = error "unsupported" + + convertNode :: Core.Node -> Geb + convertNode = \case + Core.NVar x -> convertVar x + Core.NIdt x -> convertIdent x + Core.NCst x -> convertConstant x + Core.NApp x -> convertApp x + Core.NBlt x -> convertBuiltinApp x + Core.NCtr x -> convertConstr x + Core.NLam x -> convertLambda x + Core.NLet x -> convertLet x + Core.NRec {} -> unsupported -- LetRecs should be lifted out beforehand + Core.NCase x -> convertCase 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 + + convertVar :: Core.Var -> Geb + convertVar Core.Var {} = unimplemented + + convertIdent :: Core.Ident -> Geb + convertIdent Core.Ident {..} = + -- TODO: unroll / check for recursion; + -- TODO: memoize the result to avoid recomputing it each time a reference + -- to the identifier is encountered + convertNode node + where + node = fromJust $ HashMap.lookup _identSymbol (tab ^. Core.identContext) + + convertConstant :: Core.Constant -> Geb + convertConstant Core.Constant {} = unsupported + + convertApp :: Core.App -> Geb + convertApp Core.App {} = unimplemented + + convertBuiltinApp :: Core.BuiltinApp -> Geb + convertBuiltinApp Core.BuiltinApp {} = unsupported + + convertConstr :: Core.Constr -> Geb + convertConstr Core.Constr {} = unimplemented + + convertLet :: Core.Let -> Geb + convertLet Core.Let {} = unimplemented + + convertLambda :: Core.Lambda -> Geb + convertLambda Core.Lambda {..} = + GebLamb + Lamb + { _lambVarType = convertType (_lambdaBinder ^. Core.binderType), + _lambBodyType = convertType (Info.getNodeType _lambdaBody), + _lambBody = convertNode _lambdaBody + } + + convertCase :: Core.Case -> Geb + convertCase Core.Case {} = unimplemented + + convertType :: Core.Type -> Obj + 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 {} -> unsupported -- no dynamic type in GEB + _ -> unsupported -- not a type + convertPi :: Core.Pi -> Obj + convertPi Core.Pi {..} = + ObjHom + Hom + { _homDomain = convertType (_piBinder ^. Core.binderType), + _homCodomain = convertType _piBody + } + + convertTypeConstr :: Core.TypeConstr -> Obj + convertTypeConstr Core.TypeConstr {} = unimplemented + + convertTypePrim :: Core.TypePrim -> Obj + convertTypePrim Core.TypePrim {} = unimplemented diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs index 073307195c..3931a62b95 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId.hs +++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs @@ -10,4 +10,6 @@ data TransformationId | NatToInt | ConvertBuiltinTypes | Identity + | UnrollRecursion + | ComputeTypeInfo deriving stock (Data) diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs index 032d9bca0e..4efc10f660 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs +++ b/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 @@ -99,3 +101,9 @@ strNatToInt = "nat-to-int" strConvertBuiltinTypes :: Text strConvertBuiltinTypes = "convert-builtin-types" + +strComputeTypeInfo :: Text +strComputeTypeInfo = "compute-type-info" + +strUnrollRecursion :: Text +strUnrollRecursion = "unroll-recursion" diff --git a/src/Juvix/Compiler/Core/Info/TypeInfo.hs b/src/Juvix/Compiler/Core/Info/TypeInfo.hs index 0c2e3cc5c4..0d888fb025 100644 --- a/src/Juvix/Compiler/Core/Info/TypeInfo.hs +++ b/src/Juvix/Compiler/Core/Info/TypeInfo.hs @@ -1,7 +1,7 @@ module Juvix.Compiler.Core.Info.TypeInfo where -import Juvix.Compiler.Core.Data.InfoTable -import Juvix.Compiler.Core.Extra +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 @@ -23,8 +23,11 @@ getInfoType i = 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 - -inferTypeInfo :: InfoTable -> Node -> Node -inferTypeInfo _ = umap id -- TODO: store the type of each node in its info diff --git a/src/Juvix/Compiler/Core/Pipeline.hs b/src/Juvix/Compiler/Core/Pipeline.hs index ae4ce79f86..197a48a565 100644 --- a/src/Juvix/Compiler/Core/Pipeline.hs +++ b/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 diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs index b4f8988d7d..140c6125b2 100644 --- a/src/Juvix/Compiler/Core/Transformation.hs +++ b/src/Juvix/Compiler/Core/Transformation.hs @@ -18,6 +18,8 @@ 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.ComputeTypeInfo +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 diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs new file mode 100644 index 0000000000..37f5c67754 --- /dev/null +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -0,0 +1,12 @@ +module Juvix.Compiler.Core.Transformation.ComputeTypeInfo(computeTypeInfo) where + +import Juvix.Compiler.Core.Transformation.Base +import Juvix.Compiler.Core.Extra +import Juvix.Compiler.Core.Info.TypeInfo qualified as Info + +-- TODO: store the type of each node in its info +computeNodeTypeInfo :: InfoTable -> Node -> Node +computeNodeTypeInfo _ = umap (Info.setNodeType mkDynamic') + +computeTypeInfo :: InfoTable -> InfoTable +computeTypeInfo tab = mapT (const (computeNodeTypeInfo tab)) tab diff --git a/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs b/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs new file mode 100644 index 0000000000..30d2e71908 --- /dev/null +++ b/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 From 19c74a34325dece3e74a338ec714c35db3aa7e53 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 23 Jan 2023 18:57:30 +0100 Subject: [PATCH 05/20] make ormolu happy --- src/Juvix/Compiler/Core/Transformation.hs | 2 +- src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs | 4 ++-- src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs index 140c6125b2..aa34a59d84 100644 --- a/src/Juvix/Compiler/Core/Transformation.hs +++ b/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,7 +19,6 @@ 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.ComputeTypeInfo import Juvix.Compiler.Core.Transformation.UnrollRecursion applyTransformations :: [TransformationId] -> InfoTable -> InfoTable diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index 37f5c67754..b2d52bceb4 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -1,8 +1,8 @@ -module Juvix.Compiler.Core.Transformation.ComputeTypeInfo(computeTypeInfo) where +module Juvix.Compiler.Core.Transformation.ComputeTypeInfo (computeTypeInfo) where -import Juvix.Compiler.Core.Transformation.Base import Juvix.Compiler.Core.Extra import Juvix.Compiler.Core.Info.TypeInfo qualified as Info +import Juvix.Compiler.Core.Transformation.Base -- TODO: store the type of each node in its info computeNodeTypeInfo :: InfoTable -> Node -> Node diff --git a/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs b/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs index 30d2e71908..3e2638e726 100644 --- a/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs +++ b/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs @@ -1,4 +1,4 @@ -module Juvix.Compiler.Core.Transformation.UnrollRecursion(unrollRecursion) where +module Juvix.Compiler.Core.Transformation.UnrollRecursion (unrollRecursion) where import Juvix.Compiler.Core.Transformation.Base From 7cd34da16eb53954b19bfc8df956d0dd60b98e29 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 24 Jan 2023 13:18:33 +0100 Subject: [PATCH 06/20] transformations --- src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs index 4efc10f660..b6d29a7e6a 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs +++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs @@ -69,6 +69,8 @@ transformation = <|> symbol strMoveApps $> MoveApps <|> symbol strNatToInt $> NatToInt <|> symbol strConvertBuiltinTypes $> ConvertBuiltinTypes + <|> symbol strUnrollRecursion $> UnrollRecursion + <|> symbol strComputeTypeInfo $> ComputeTypeInfo allStrings :: [Text] allStrings = @@ -78,7 +80,9 @@ allStrings = strRemoveTypeArgs, strMoveApps, strNatToInt, - strConvertBuiltinTypes + strConvertBuiltinTypes, + strUnrollRecursion, + strComputeTypeInfo ] strLifting :: Text From 1b2445eac4724934893a3597d9e543cf5a4a84f3 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 25 Jan 2023 15:48:57 +0100 Subject: [PATCH 07/20] basic translation to GEB --- src/Juvix/Compiler/Backend/Geb/Extra.hs | 8 + src/Juvix/Compiler/Backend/Geb/Language.hs | 70 ++-- src/Juvix/Compiler/Backend/Geb/Pretty.hs | 10 +- src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs | 24 +- .../Backend/Geb/Translation/FromCore.hs | 314 +++++++++++++++--- src/Juvix/Compiler/Core/Language/Base.hs | 2 +- src/Juvix/Compiler/Core/Language/Builtins.hs | 2 +- 7 files changed, 330 insertions(+), 100 deletions(-) create mode 100644 src/Juvix/Compiler/Backend/Geb/Extra.hs diff --git a/src/Juvix/Compiler/Backend/Geb/Extra.hs b/src/Juvix/Compiler/Backend/Geb/Extra.hs new file mode 100644 index 0000000000..b18cda5476 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Extra.hs @@ -0,0 +1,8 @@ +module Juvix.Compiler.Backend.Geb.Extra where + +import Juvix.Compiler.Backend.Geb.Language + +destructProd :: Object -> [Object] +destructProd = \case + ObjectProd Prod {..} -> _prodLeft : destructProd _prodRight + x -> [x] diff --git a/src/Juvix/Compiler/Backend/Geb/Language.hs b/src/Juvix/Compiler/Backend/Geb/Language.hs index 1186bea993..aa97fe3acd 100644 --- a/src/Juvix/Compiler/Backend/Geb/Language.hs +++ b/src/Juvix/Compiler/Backend/Geb/Language.hs @@ -8,46 +8,46 @@ import Juvix.Prelude (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`, --- `_caseLeftType` has the form `Dom -> _caseCodomainType` and `_caseRightType` --- has the form `Dom -> _caseCodomainType`. +-- | 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 :: Obj, - _caseRightType :: Obj, - _caseCodomainType :: Obj, + { _caseLeftType :: Object, + _caseRightType :: Object, + _caseCodomainType :: Object, _caseOn :: Geb, _caseLeft :: Geb, _caseRight :: Geb } data Pair = Pair - { _pairLeftType :: Obj, - _pairRightType :: Obj, + { _pairLeftType :: Object, + _pairRightType :: Object, _pairLeft :: Geb, _pairRight :: Geb } data Fst = Fst - { _fstLeftType :: Obj, - _fstRightType :: Obj, + { _fstLeftType :: Object, + _fstRightType :: Object, _fstValue :: Geb } data Snd = Snd - { _sndLeftType :: Obj, - _sndRightType :: Obj, + { _sndLeftType :: Object, + _sndRightType :: Object, _sndValue :: Geb } data Lamb = Lamb - { _lambVarType :: Obj, - _lambBodyType :: Obj, + { _lambVarType :: Object, + _lambBodyType :: Object, _lambBody :: Geb } data App = App - { _appDomainType :: Obj, - _appCodomainType :: Obj, + { _appDomainType :: Object, + _appCodomainType :: Object, _appLeft :: Geb, _appRight :: Geb } @@ -68,29 +68,29 @@ data Geb | GebVar Int data Prod = Prod - { _prodLeft :: Obj, - _prodRight :: Obj + { _prodLeft :: Object, + _prodRight :: Object } data Coprod = Coprod - { _coprodLeft :: Obj, - _coprodRight :: Obj + { _coprodLeft :: Object, + _coprodRight :: Object } -- | Function type data Hom = Hom - { _homDomain :: Obj, - _homCodomain :: Obj + { _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 Obj - = ObjInitial -- empty type - | ObjTerminal -- unit type - | ObjProd Prod - | ObjCoprod Coprod - | ObjHom Hom -- function type +data Object + = ObjectInitial -- empty type + | ObjectTerminal -- unit type + | ObjectProd Prod + | ObjectCoprod Coprod + | ObjectHom Hom -- function type instance HasAtomicity Geb where atomicity = \case @@ -106,13 +106,13 @@ instance HasAtomicity Geb where GebApp {} -> Aggregate appFixity GebVar {} -> Aggregate appFixity -instance HasAtomicity Obj where +instance HasAtomicity Object where atomicity = \case - ObjInitial -> Atom - ObjTerminal -> Atom - ObjProd {} -> Aggregate appFixity - ObjCoprod {} -> Aggregate appFixity - ObjHom {} -> Aggregate appFixity + ObjectInitial -> Atom + ObjectTerminal -> Atom + ObjectProd {} -> Aggregate appFixity + ObjectCoprod {} -> Aggregate appFixity + ObjectHom {} -> Aggregate appFixity makeLenses ''Case makeLenses ''Pair @@ -124,4 +124,4 @@ makeLenses ''Geb makeLenses ''Prod makeLenses ''Coprod makeLenses ''Hom -makeLenses ''Obj +makeLenses ''Object diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty.hs b/src/Juvix/Compiler/Backend/Geb/Pretty.hs index 3c03d6d1c0..a20fb16242 100644 --- a/src/Juvix/Compiler/Backend/Geb/Pretty.hs +++ b/src/Juvix/Compiler/Backend/Geb/Pretty.hs @@ -12,17 +12,17 @@ import Juvix.Data.PPOutput import Juvix.Prelude import Prettyprinter.Render.Terminal qualified as Ansi -ppOutDefault :: PrettyCode c => c -> AnsiText +ppOutDefault :: (HasAtomicity c, PrettyCode c) => c -> AnsiText ppOutDefault = AnsiText . PPOutput . doc defaultOptions -ppOut :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> AnsiText +ppOut :: (CanonicalProjection a Options, HasAtomicity c, PrettyCode c) => a -> c -> AnsiText ppOut o = AnsiText . PPOutput . doc (project o) -ppTrace' :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> Text +ppTrace' :: (CanonicalProjection a Options, HasAtomicity c, PrettyCode c) => a -> c -> Text ppTrace' opts = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc (project opts) -ppTrace :: PrettyCode c => c -> Text +ppTrace :: (HasAtomicity c, PrettyCode c) => c -> Text ppTrace = ppTrace' traceOptions -ppPrint :: PrettyCode c => c -> Text +ppPrint :: (HasAtomicity c, PrettyCode c) => c -> Text ppPrint = show . ppOutDefault diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs index 6611039f5d..55e79d7311 100644 --- a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs @@ -11,11 +11,13 @@ import Juvix.Data.CodeAnn import Juvix.Extra.Strings qualified as Str import Juvix.Prelude -doc :: PrettyCode c => Options -> c -> Doc Ann -doc opts = - run - . runReader opts - . ppCode +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) @@ -105,13 +107,13 @@ instance PrettyCode Hom where cod <- ppArg _homCodomain return $ kwHom <+> dom <+> cod -instance PrettyCode Obj where +instance PrettyCode Object where ppCode = \case - ObjInitial -> return kwInitial - ObjTerminal -> return kwTerminal - ObjProd x -> ppCode x - ObjCoprod x -> ppCode x - ObjHom x -> ppCode x + ObjectInitial -> return kwInitial + ObjectTerminal -> return kwTerminal + ObjectProd x -> ppCode x + ObjectCoprod x -> ppCode x + ObjectHom x -> ppCode x {--------------------------------------------------------------------------------} {- helper functions -} diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs index 80c2acadd4..50be936683 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs @@ -1,9 +1,13 @@ 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 (Level, Symbol) import Juvix.Compiler.Core.Language qualified as Core import Juvix.Prelude @@ -29,26 +33,25 @@ import Juvix.Prelude -} fromCore :: Core.InfoTable -> Core.Node -> Geb -fromCore tab = convertNode +fromCore tab = convertNode mempty 0 [] where - unimplemented :: forall a. a - unimplemented = error "not yet implemented" - unsupported :: forall a. a unsupported = error "unsupported" - convertNode :: Core.Node -> Geb - convertNode = \case - Core.NVar x -> convertVar x - Core.NIdt x -> convertIdent x - Core.NCst x -> convertConstant x - Core.NApp x -> convertApp x - Core.NBlt x -> convertBuiltinApp x - Core.NCtr x -> convertConstr x - Core.NLam x -> convertLambda x - Core.NLet x -> convertLet x + -- `shiftLevels` contains the de Bruijn levels immediately after which a + -- binder was inserted + convertNode :: HashMap Symbol Level -> Level -> [Level] -> Core.Node -> Geb + 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 x + Core.NCase x -> convertCase identMap varsNum shiftLevels x Core.NMatch {} -> unsupported -- Pattern matching should be compiled beforehand Core.NPi {} -> unsupported Core.NUniv {} -> unsupported @@ -57,46 +60,233 @@ fromCore tab = convertNode Core.NDyn {} -> unsupported Core.Closure {} -> unsupported - convertVar :: Core.Var -> Geb - convertVar Core.Var {} = unimplemented + convertVar :: HashMap Symbol Level -> Level -> [Level] -> Core.Var -> Geb + convertVar _ varsNum shiftLevels Core.Var {..} = + GebVar (_varIndex + length (filter ((varsNum - _varIndex - 1) <=) shiftLevels)) - convertIdent :: Core.Ident -> Geb - convertIdent Core.Ident {..} = - -- TODO: unroll / check for recursion; - -- TODO: memoize the result to avoid recomputing it each time a reference - -- to the identifier is encountered - convertNode node - where - node = fromJust $ HashMap.lookup _identSymbol (tab ^. Core.identContext) + convertIdent :: HashMap Symbol Level -> Level -> [Level] -> Core.Ident -> Geb + convertIdent identMap varsNum _ Core.Ident {..} = + GebVar (varsNum - fromJust (HashMap.lookup _identSymbol identMap) - 1) - convertConstant :: Core.Constant -> Geb - convertConstant Core.Constant {} = unsupported + convertConstant :: HashMap Symbol Level -> Level -> [Level] -> Core.Constant -> Geb + convertConstant _ _ _ Core.Constant {} = unsupported - convertApp :: Core.App -> Geb - convertApp Core.App {} = unimplemented + convertApp :: HashMap Symbol Level -> Level -> [Level] -> Core.App -> Geb + 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 + } - convertBuiltinApp :: Core.BuiltinApp -> Geb - convertBuiltinApp Core.BuiltinApp {} = unsupported + convertBuiltinApp :: HashMap Symbol Level -> Level -> [Level] -> Core.BuiltinApp -> Geb + convertBuiltinApp _ _ _ Core.BuiltinApp {} = unsupported - convertConstr :: Core.Constr -> Geb - convertConstr Core.Constr {} = unimplemented + convertConstr :: HashMap Symbol Level -> Level -> [Level] -> Core.Constr -> Geb + convertConstr identMap varsNum shiftLevels Core.Constr {..} = + foldr ($) (GebLeft (convertProduct identMap varsNum shiftLevels _constrArgs)) (replicate tagNum GebRight) + 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)) - convertLet :: Core.Let -> Geb - convertLet Core.Let {} = unimplemented + convertProduct :: HashMap Symbol Level -> Level -> [Level] -> [Core.Node] -> Geb + convertProduct identMap varsNum shiftLevels = \case + h : t -> + fst $ + foldr + (\x -> mkPair (convertNode identMap varsNum shiftLevels x, convertType (Info.getNodeType x))) + (convertNode identMap varsNum shiftLevels h, convertType (Info.getNodeType h)) + t + [] -> + GebUnit + where + mkPair :: (Geb, Object) -> (Geb, Object) -> (Geb, Object) + mkPair (x, xty) (y, yty) = (z, zty) + where + z = + GebPair + Pair + { _pairLeftType = xty, + _pairRightType = yty, + _pairLeft = x, + _pairRight = y + } + zty = ObjectProd (Prod xty yty) - convertLambda :: Core.Lambda -> Geb - convertLambda Core.Lambda {..} = + convertLet :: HashMap Symbol Level -> Level -> [Level] -> Core.Let -> Geb + 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 + }, + _appRight = 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 identMap varsNum shiftLevels Core.Lambda {..} = GebLamb Lamb { _lambVarType = convertType (_lambdaBinder ^. Core.binderType), _lambBodyType = convertType (Info.getNodeType _lambdaBody), - _lambBody = convertNode _lambdaBody + _lambBody = convertNode identMap (varsNum + 1) shiftLevels _lambdaBody } - convertCase :: Core.Case -> Geb - convertCase Core.Case {} = unimplemented + convertCase :: HashMap Symbol Level -> Level -> [Level] -> Core.Case -> Geb + convertCase identMap varsNum shiftLevels Core.Case {..} = + if + | null branches -> + GebAbsurd (convertNode identMap varsNum shiftLevels _caseValue) + | length ctrBrs > 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 - 1 : shiftLevels) _caseValue branches + }, + _appRight = convertNode identMap varsNum shiftLevels defaultNode + } + | otherwise -> go indty shiftLevels _caseValue branches + where + indty = convertInductive _caseInductive + ii = fromJust $ HashMap.lookup _caseInductive (tab ^. Core.infoInductives) + ctrBranches = map mkCtrBranch (ii ^. Core.inductiveConstructors) + ctrBrs = + filter + ( \x -> + isNothing (find (\y -> x ^. Core.caseBranchTag == y ^. Core.caseBranchTag) _caseBranches) + ) + ctrBranches + 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)) - convertType :: Core.Type -> Obj + 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 + | length ctrBrs > 1 -> Core.mkVar' + | otherwise -> (`Core.shift` defaultNode) + + go :: Object -> [Level] -> Core.Node -> [Core.CaseBranch] -> Geb + 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 + Case + { _caseLeftType = lty, + _caseRightType = rty, + _caseCodomainType = codty, + _caseOn = convertNode identMap varsNum lvls val, + _caseLeft = mkBranch lty lvls val br, + _caseRight = + GebLamb + Lamb + { _lambVarType = rty, + _lambBodyType = codty, + _lambBody = go rty (varsNum - 1 : lvls) (Core.mkVar' 0) brs + } + } + where + (lty, rty) = case ty of + ObjectCoprod Coprod {..} -> (_coprodLeft, _coprodRight) + _ -> impossible + [] -> impossible + + mkBranch :: Object -> [Level] -> Core.Node -> Core.CaseBranch -> Geb + mkBranch valty lvls val Core.CaseBranch {..} = + mkApps (mkLambs argtys) (convertNode identMap varsNum lvls val) valty argtys + where + argtys = destructProd valty + lvls' = replicate _caseBranchBindersNum (varsNum - 1) ++ lvls + + mkApps :: Geb -> Geb -> Object -> [Object] -> Geb + mkApps acc v vty = \case + ty : tys -> + mkApps acc' v' rty tys + where + v' = + GebSnd + Snd + { _sndLeftType = lty, + _sndRightType = rty, + _sndValue = v + } + acc' = + GebApp + App + { _appDomainType = ty, + _appCodomainType = vty, + _appLeft = acc, + _appRight = + if + | null tys -> + v + | otherwise -> + GebFst + Fst + { _fstLeftType = lty, + _fstRightType = rty, + _fstValue = v + } + } + (lty, rty) = case vty of + ObjectProd Prod {..} -> (_prodLeft, _prodRight) + _ -> impossible + [] -> + acc + + mkLambs :: [Object] -> Geb + mkLambs = + fst + . foldr + ( \ty (acc, accty) -> + ( GebLamb + Lamb + { _lambVarType = ty, + _lambBodyType = accty, + _lambBody = acc + }, + ObjectHom (Hom ty accty) + ) + ) + (convertNode identMap varsNum lvls' _caseBranchBody, codty) + + convertType :: Core.Type -> Object convertType = \case Core.NPi x -> convertPi x Core.NUniv {} -> unsupported -- no polymorphism yet @@ -104,16 +294,46 @@ fromCore tab = convertNode Core.NPrim x -> convertTypePrim x Core.NDyn {} -> unsupported -- no dynamic type in GEB _ -> unsupported -- not a type - convertPi :: Core.Pi -> Obj + convertPi :: Core.Pi -> Object convertPi Core.Pi {..} = - ObjHom + ObjectHom Hom { _homDomain = convertType (_piBinder ^. Core.binderType), _homCodomain = convertType _piBody } - convertTypeConstr :: Core.TypeConstr -> Obj - convertTypeConstr Core.TypeConstr {} = unimplemented + convertTypeConstr :: Core.TypeConstr -> Object + convertTypeConstr Core.TypeConstr {..} = convertInductive _typeConstrSymbol + + convertTypePrim :: Core.TypePrim -> Object + convertTypePrim Core.TypePrim {..} = + case _typePrimPrimitive of + Core.PrimInteger _ -> unsupported + Core.PrimBool _ -> ObjectCoprod (Coprod ObjectTerminal ObjectTerminal) + Core.PrimString -> unsupported + + convertInductive :: Symbol -> Object + convertInductive sym = + case ctrs of + ci : ctrs' -> + foldr + (\x acc -> ObjectCoprod (Coprod (convertConstructorType (x ^. Core.constructorType)) acc)) + (convertConstructorType (ci ^. Core.constructorType)) + ctrs' + [] -> + ObjectInitial + where + ctrs = + sortOn (^. Core.constructorTag) $ + fromJust (HashMap.lookup sym (tab ^. Core.infoInductives)) ^. Core.inductiveConstructors - convertTypePrim :: Core.TypePrim -> Obj - convertTypePrim Core.TypePrim {} = unimplemented + convertConstructorType :: Core.Node -> Object + convertConstructorType ty = + case Core.typeArgs ty of + hty : tys -> + foldr + (\x acc -> ObjectProd (Prod (convertType x) acc)) + (convertType hty) + tys + [] -> + ObjectTerminal diff --git a/src/Juvix/Compiler/Core/Language/Base.hs b/src/Juvix/Compiler/Core/Language/Base.hs index 880d7e3849..388d858ea6 100644 --- a/src/Juvix/Compiler/Core/Language/Base.hs +++ b/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 diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs index 273b9013da..a3aa694bc0 100644 --- a/src/Juvix/Compiler/Core/Language/Builtins.hs +++ b/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 From e9357055a6d06a735e45321de68902c13508ed3c Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 25 Jan 2023 18:13:20 +0100 Subject: [PATCH 08/20] translate identifiers --- .../Backend/Geb/Translation/FromCore.hs | 92 ++++++++++++------- 1 file changed, 61 insertions(+), 31 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs index 50be936683..82b3e3c36b 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs @@ -7,38 +7,65 @@ 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 (Level, Symbol) +import Juvix.Compiler.Core.Language (Index, Level, Symbol) import Juvix.Compiler.Core.Language qualified as Core import Juvix.Prelude -{- - TODO: The translation of each identifier should be 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) - ``` - should be translated as: - ``` - (\a -> (\f -> (\g -> g (g a)) (\x -> f (f x))) (\x -> F')) a' - ``` --} - fromCore :: Core.InfoTable -> Core.Node -> Geb -fromCore tab = convertNode mempty 0 [] +fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentifiers)) where unsupported :: forall a. a unsupported = error "unsupported" - -- `shiftLevels` contains the de Bruijn levels immediately after which a + nodeType :: Object + nodeType = convertType (Info.getNodeType node) + + {- + 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.IdentifierInfo] -> Geb + goIdents identMap level shiftLevels = \case + ii : idents -> + GebApp + App + { _appDomainType = argty, + _appCodomainType = nodeType, + _appLeft = lamb, + _appRight = 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) idents + lamb = + GebLamb + Lamb + { _lambVarType = argty, + _lambBodyType = nodeType, + _lambBody = body + } + [] -> + convertNode identMap 0 shiftLevels node + + -- `shiftLevels` contains the de Bruijn levels immediately before which a -- binder was inserted convertNode :: HashMap Symbol Level -> Level -> [Level] -> Core.Node -> Geb convertNode identMap varsNum shiftLevels = \case @@ -60,13 +87,17 @@ fromCore tab = convertNode mempty 0 [] 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 -> Geb convertVar _ varsNum shiftLevels Core.Var {..} = - GebVar (_varIndex + length (filter ((varsNum - _varIndex - 1) <=) shiftLevels)) + GebVar (_varIndex + insertedBinders varsNum shiftLevels _varIndex) convertIdent :: HashMap Symbol Level -> Level -> [Level] -> Core.Ident -> Geb - convertIdent identMap varsNum _ Core.Ident {..} = - GebVar (varsNum - fromJust (HashMap.lookup _identSymbol identMap) - 1) + convertIdent identMap varsNum shiftLevels Core.Ident {..} = + GebVar (varsNum + length shiftLevels - fromJust (HashMap.lookup _identSymbol identMap) - 1) convertConstant :: HashMap Symbol Level -> Level -> [Level] -> Core.Constant -> Geb convertConstant _ _ _ Core.Constant {} = unsupported @@ -161,7 +192,7 @@ fromCore tab = convertNode mempty 0 [] Lamb { _lambVarType = ty, _lambBodyType = ty, - _lambBody = go indty (varsNum - 1 : shiftLevels) _caseValue branches + _lambBody = go indty (varsNum : shiftLevels) _caseValue branches }, _appRight = convertNode identMap varsNum shiftLevels defaultNode } @@ -218,7 +249,7 @@ fromCore tab = convertNode mempty 0 [] Lamb { _lambVarType = rty, _lambBodyType = codty, - _lambBody = go rty (varsNum - 1 : lvls) (Core.mkVar' 0) brs + _lambBody = go rty (varsNum : lvls) (Core.mkVar' 0) brs } } where @@ -232,7 +263,6 @@ fromCore tab = convertNode mempty 0 [] mkApps (mkLambs argtys) (convertNode identMap varsNum lvls val) valty argtys where argtys = destructProd valty - lvls' = replicate _caseBranchBindersNum (varsNum - 1) ++ lvls mkApps :: Geb -> Geb -> Object -> [Object] -> Geb mkApps acc v vty = \case @@ -284,7 +314,7 @@ fromCore tab = convertNode mempty 0 [] ObjectHom (Hom ty accty) ) ) - (convertNode identMap varsNum lvls' _caseBranchBody, codty) + (convertNode identMap (varsNum + _caseBranchBindersNum) lvls _caseBranchBody, codty) convertType :: Core.Type -> Object convertType = \case From ebf5b43faaee50556bdfcbcc70e8187bd9aa5b1b Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 26 Jan 2023 10:53:30 +0100 Subject: [PATCH 09/20] compute simple types in Core --- src/Juvix/Compiler/Core/Data/BinderList.hs | 13 ++- .../Core/Transformation/ComputeTypeInfo.hs | 81 ++++++++++++++++++- 2 files changed, 84 insertions(+), 10 deletions(-) diff --git a/src/Juvix/Compiler/Core/Data/BinderList.hs b/src/Juvix/Compiler/Core/Data/BinderList.hs index 514c760f0b..102992b4ba 100644 --- a/src/Juvix/Compiler/Core/Data/BinderList.hs +++ b/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 " diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index b2d52bceb4..ad3c597420 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -1,12 +1,89 @@ 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 --- TODO: store the type of each node in its info +-- | Computes the TypeInfo for each subnode. +-- +-- Assumptions: +-- 1. No polymorphism. +-- 2. No dynamic type. +-- 3. All binders and identifiers are decorated with full type information. +-- 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 _ = umap (Info.setNodeType mkDynamic') +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' + 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 mkTypeConstr' (ci ^. constructorInductive) (take (length (ii ^. inductiveParams)) _constrArgs) + NLam Lambda {..} -> + mkPi' (_lambdaBinder ^. binderType) (mkLambda' (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 From 1c857cd6b4c8869eb9e886bc88a32f220fab2d45 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 26 Jan 2023 17:49:48 +0100 Subject: [PATCH 10/20] CLI & bugfixes --- app/Commands/Dev/Asm/Compile.hs | 1 + app/Commands/Dev/Core/Compile.hs | 46 +++++-- app/Commands/Extra/Compile.hs | 2 + app/Commands/Extra/Compile/Options.hs | 6 +- src/Juvix/Compiler/Backend/Geb.hs | 4 + src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs | 3 +- src/Juvix/Compiler/Backend/Geb/Translation.hs | 13 ++ .../Backend/Geb/Translation/FromCore.hs | 126 +++++++++++------- .../Core/Transformation/ComputeTypeInfo.hs | 6 +- src/Juvix/Compiler/Pipeline.hs | 4 + tests/Geb/positive/Core/test001.jvc | 2 + tests/Geb/positive/Core/test002.jvc | 7 + 12 files changed, 157 insertions(+), 63 deletions(-) create mode 100644 src/Juvix/Compiler/Backend/Geb.hs create mode 100644 src/Juvix/Compiler/Backend/Geb/Translation.hs create mode 100644 tests/Geb/positive/Core/test001.jvc create mode 100644 tests/Geb/positive/Core/test002.jvc diff --git a/app/Commands/Dev/Asm/Compile.hs b/app/Commands/Dev/Asm/Compile.hs index 14d8db5c0f..9dd419f704 100644 --- a/app/Commands/Dev/Asm/Compile.hs +++ b/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 diff --git a/app/Commands/Dev/Core/Compile.hs b/app/Commands/Dev/Core/Compile.hs index 12da3cec62..08ad86865f 100644 --- a/app/Commands/Dev/Core/Compile.hs +++ b/app/Commands/Dev/Core/Compile.hs @@ -7,6 +7,7 @@ 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 @@ -15,16 +16,26 @@ 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 opts file tab + _ -> runCPipeline opts file tab where getFile :: Sem r (Path Abs File) getFile = someBaseToAbs' (opts ^. compileInputFile . pathPath) +runCPipeline :: + forall r. + (Members '[Embed IO, App] r) => + CoreCompileOptions -> + Path Abs File -> + Core.InfoTable -> + Sem r () +runCPipeline opts file tab = do + C.MiniCResult {..} <- getRight (run (runError (coreToMiniC asmOpts tab :: Sem '[Error JuvixError] C.MiniCResult))) + cFile <- inputFile file ".c" + embed $ TIO.writeFile (toFilePath cFile) _resultCCode + Compile.runCommand opts {_compileInputFile = AppPath (Abs cFile) False} + where asmOpts :: Asm.Options asmOpts = Asm.makeOptions (asmTarget (opts ^. compileTarget)) (opts ^. compileDebug) @@ -33,11 +44,22 @@ runCommand opts = do 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) => + CoreCompileOptions -> + Path Abs File -> + Core.InfoTable -> + Sem r () +runGebPipeline _ file tab = do + Geb.Result {..} <- getRight (run (runError (coreToGeb tab :: Sem '[Error JuvixError] Geb.Result))) + gebFile <- inputFile file ".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)) diff --git a/app/Commands/Extra/Compile.hs b/app/Commands/Extra/Compile.hs index 0d8eb17c63..2b287ac104 100644 --- a/app/Commands/Extra/Compile.hs +++ b/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) diff --git a/app/Commands/Extra/Compile/Options.hs b/app/Commands/Extra/Compile/Options.hs index 6536ce94e5..db66c1465b 100644 --- a/app/Commands/Extra/Compile/Options.hs +++ b/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" diff --git a/src/Juvix/Compiler/Backend/Geb.hs b/src/Juvix/Compiler/Backend/Geb.hs new file mode 100644 index 0000000000..52f5c73f0b --- /dev/null +++ b/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 diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs index 55e79d7311..888ef6e5cb 100644 --- a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs @@ -26,10 +26,11 @@ 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 <+> val <+> left <+> right + return $ kwCase <+> lty <+> rty <+> cod <+> val <+> left <+> right instance PrettyCode Pair where ppCode Pair {..} = do diff --git a/src/Juvix/Compiler/Backend/Geb/Translation.hs b/src/Juvix/Compiler/Backend/Geb/Translation.hs new file mode 100644 index 0000000000..af44126057 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Translation.hs @@ -0,0 +1,13 @@ +module Juvix.Compiler.Backend.Geb.Translation(module Juvix.Compiler.Backend.Geb.Translation, module Juvix.Compiler.Backend.Geb.Translation.FromCore) where + +import Juvix.Prelude +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 :: Geb -> 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 82b3e3c36b..c0e60d331a 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs @@ -9,17 +9,21 @@ 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.Compiler.Core.Pretty qualified as Core import Juvix.Prelude -fromCore :: Core.InfoTable -> Core.Node -> Geb -fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentifiers)) +fromCore :: Core.InfoTable -> Geb +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" - nodeType :: Object - nodeType = convertType (Info.getNodeType node) - {- The translation of each identifier is saved separately to avoid exponential blow-up. For example, the program: @@ -40,8 +44,8 @@ fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentif (\a -> (\f -> (\g -> g (g a)) (\x -> f (f x))) (\x -> F)) a ``` -} - goIdents :: HashMap Symbol Level -> Level -> [Level] -> [Core.IdentifierInfo] -> Geb - goIdents identMap level shiftLevels = \case + goIdents :: HashMap Symbol Level -> Level -> [Level] -> Core.Node -> [Core.IdentifierInfo] -> Geb + goIdents identMap level shiftLevels node = \case ii : idents -> GebApp App @@ -54,7 +58,7 @@ fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentif 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) idents + body = goIdents (HashMap.insert sym level identMap) (level + 1) (0 : shiftLevels) node idents lamb = GebLamb Lamb @@ -64,11 +68,13 @@ fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentif } [] -> 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 -> Geb - convertNode identMap varsNum shiftLevels = \case + convertNode identMap varsNum shiftLevels node = trace (Core.ppTrace node) $ case node of Core.NVar x -> convertVar identMap varsNum shiftLevels x Core.NIdt x -> convertIdent identMap varsNum shiftLevels x Core.NCst x -> convertConstant identMap varsNum shiftLevels x @@ -117,12 +123,15 @@ fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentif convertConstr :: HashMap Symbol Level -> Level -> [Level] -> Core.Constr -> Geb convertConstr identMap varsNum shiftLevels Core.Constr {..} = - foldr ($) (GebLeft (convertProduct identMap varsNum shiftLevels _constrArgs)) (replicate tagNum GebRight) + foldr ($) prod (replicate tagNum GebRight) 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) + (convertProduct identMap varsNum shiftLevels _constrArgs) convertProduct :: HashMap Symbol Level -> Level -> [Level] -> [Core.Node] -> Geb convertProduct identMap varsNum shiftLevels = \case @@ -178,35 +187,37 @@ fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentif convertCase :: HashMap Symbol Level -> Level -> [Level] -> Core.Case -> Geb convertCase identMap varsNum shiftLevels Core.Case {..} = - if - | null branches -> - GebAbsurd (convertNode identMap varsNum shiftLevels _caseValue) - | length ctrBrs > 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 - }, - _appRight = convertNode identMap varsNum shiftLevels defaultNode - } - | otherwise -> go indty shiftLevels _caseValue branches + trace (show missingCtrsNum) $ + if + | null branches -> + GebAbsurd (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 + }, + _appRight = convertNode identMap varsNum shiftLevels defaultNode + } + | otherwise -> go indty shiftLevels _caseValue branches where indty = convertInductive _caseInductive ii = fromJust $ HashMap.lookup _caseInductive (tab ^. Core.infoInductives) - ctrBranches = map mkCtrBranch (ii ^. Core.inductiveConstructors) - ctrBrs = + missingCtrs = filter ( \x -> - isNothing (find (\y -> x ^. Core.caseBranchTag == y ^. Core.caseBranchTag) _caseBranches) + isNothing (find (\y -> x ^. Core.constructorTag == y ^. Core.caseBranchTag) _caseBranches) ) - ctrBranches + (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 @@ -228,7 +239,7 @@ fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentif n = length tyargs defaultBody = if - | length ctrBrs > 1 -> Core.mkVar' + | missingCtrsNum > 1 -> Core.mkVar' | otherwise -> (`Core.shift` defaultNode) go :: Object -> [Level] -> Core.Node -> [Core.CaseBranch] -> Geb @@ -243,7 +254,13 @@ fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentif _caseRightType = rty, _caseCodomainType = codty, _caseOn = convertNode identMap varsNum lvls val, - _caseLeft = mkBranch lty lvls val br, + _caseLeft = + GebLamb + Lamb + { _lambVarType = lty, + _lambBodyType = codty, + _lambBody = mkBranch lty (varsNum : lvls) val br + }, _caseRight = GebLamb Lamb @@ -260,8 +277,13 @@ fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentif mkBranch :: Object -> [Level] -> Core.Node -> Core.CaseBranch -> Geb mkBranch valty lvls val Core.CaseBranch {..} = - mkApps (mkLambs argtys) (convertNode identMap varsNum lvls val) valty argtys + if + | _caseBranchBindersNum == 0 -> + branch + | otherwise -> + mkApps (mkLambs argtys) (convertNode identMap varsNum lvls val) valty argtys where + branch = convertNode identMap (varsNum + _caseBranchBindersNum) lvls _caseBranchBody argtys = destructProd valty mkApps :: Geb -> Geb -> Object -> [Object] -> Geb @@ -314,16 +336,24 @@ fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentif ObjectHom (Hom ty accty) ) ) - (convertNode identMap (varsNum + _caseBranchBindersNum) lvls _caseBranchBody, codty) + (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 {} -> unsupported -- no dynamic type in GEB - _ -> unsupported -- not a type + convertType ty = trace (Core.ppTrace ty) $ case ty of + Core.NPi x -> + convertPi x + Core.NUniv {} -> + unsupported -- no polymorphism yet + Core.NTyp x -> + convertTypeConstr x + Core.NPrim x -> + convertTypePrim x + Core.NDyn {} -> + unsupported -- no dynamic type in GEB + Core.NLam Core.Lambda {..} -> + convertType _lambdaBody + _ -> + unsupported -- not a type convertPi :: Core.Pi -> Object convertPi Core.Pi {..} = ObjectHom @@ -344,12 +374,12 @@ fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentif convertInductive :: Symbol -> Object convertInductive sym = - case ctrs of + case reverse ctrs of ci : ctrs' -> foldr (\x acc -> ObjectCoprod (Coprod (convertConstructorType (x ^. Core.constructorType)) acc)) (convertConstructorType (ci ^. Core.constructorType)) - ctrs' + (reverse ctrs') [] -> ObjectInitial where @@ -359,11 +389,11 @@ fromCore tab node = goIdents mempty 0 [] (HashMap.elems (tab ^. Core.infoIdentif convertConstructorType :: Core.Node -> Object convertConstructorType ty = - case Core.typeArgs ty of + case reverse (Core.typeArgs ty) of hty : tys -> foldr (\x acc -> ObjectProd (Prod (convertType x) acc)) (convertType hty) - tys + (reverse tys) [] -> ObjectTerminal diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index ad3c597420..9bba961c84 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -57,7 +57,11 @@ computeNodeTypeInfo tab = umapL go NCtr Constr {..} -> let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors) ii = fromJust $ HashMap.lookup (ci ^. constructorInductive) (tab ^. infoInductives) - in mkTypeConstr' (ci ^. constructorInductive) (take (length (ii ^. inductiveParams)) _constrArgs) + in case ii ^. inductiveBuiltin of + Just BuiltinBool -> + mkTypeBool' + _ -> + mkTypeConstr' (ci ^. constructorInductive) (take (length (ii ^. inductiveParams)) _constrArgs) NLam Lambda {..} -> mkPi' (_lambdaBinder ^. binderType) (mkLambda' (Info.getNodeType _lambdaBody)) NLet Let {..} -> diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs index 48e54744ab..f4b2ef0ec6 100644 --- a/src/Juvix/Compiler/Pipeline.hs +++ b/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 -------------------------------------------------------------------------------- diff --git a/tests/Geb/positive/Core/test001.jvc b/tests/Geb/positive/Core/test001.jvc new file mode 100644 index 0000000000..dd7e6babca --- /dev/null +++ b/tests/Geb/positive/Core/test001.jvc @@ -0,0 +1,2 @@ + +\(x : bool) if x then false else true diff --git a/tests/Geb/positive/Core/test002.jvc b/tests/Geb/positive/Core/test002.jvc new file mode 100644 index 0000000000..6c0d0c687f --- /dev/null +++ b/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 } } From 9fd2f25e39fdd5b334948fdf49df725fec0398cb Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 26 Jan 2023 17:54:20 +0100 Subject: [PATCH 11/20] remove debug trace --- src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs index c0e60d331a..1700aba79a 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs @@ -9,7 +9,6 @@ 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.Compiler.Core.Pretty qualified as Core import Juvix.Prelude fromCore :: Core.InfoTable -> Geb @@ -74,7 +73,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 identMap varsNum shiftLevels node = trace (Core.ppTrace node) $ case node of + 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 @@ -187,7 +186,6 @@ fromCore tab = case tab ^. Core.infoMain of convertCase :: HashMap Symbol Level -> Level -> [Level] -> Core.Case -> Geb convertCase identMap varsNum shiftLevels Core.Case {..} = - trace (show missingCtrsNum) $ if | null branches -> GebAbsurd (convertNode identMap varsNum shiftLevels _caseValue) @@ -339,7 +337,7 @@ fromCore tab = case tab ^. Core.infoMain of (branch, codty) convertType :: Core.Type -> Object - convertType ty = trace (Core.ppTrace ty) $ case ty of + convertType = \case Core.NPi x -> convertPi x Core.NUniv {} -> From 059831c6f7ab424698a67e8dcee3af40fffefaed Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Thu, 26 Jan 2023 17:55:25 +0100 Subject: [PATCH 12/20] make ormolu happy --- src/Juvix/Compiler/Backend/Geb.hs | 2 +- src/Juvix/Compiler/Backend/Geb/Translation.hs | 10 ++--- .../Backend/Geb/Translation/FromCore.hs | 38 +++++++++---------- 3 files changed, 25 insertions(+), 25 deletions(-) diff --git a/src/Juvix/Compiler/Backend/Geb.hs b/src/Juvix/Compiler/Backend/Geb.hs index 52f5c73f0b..321aed4519 100644 --- a/src/Juvix/Compiler/Backend/Geb.hs +++ b/src/Juvix/Compiler/Backend/Geb.hs @@ -1,4 +1,4 @@ -module Juvix.Compiler.Backend.Geb(module Juvix.Compiler.Backend.Geb.Language, module Juvix.Compiler.Backend.Geb.Translation) where +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 diff --git a/src/Juvix/Compiler/Backend/Geb/Translation.hs b/src/Juvix/Compiler/Backend/Geb/Translation.hs index af44126057..425910db2f 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation.hs +++ b/src/Juvix/Compiler/Backend/Geb/Translation.hs @@ -1,13 +1,13 @@ -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.Prelude 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 -} +newtype Result = Result + { _resultCode :: Text + } toResult :: Geb -> 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 1700aba79a..d5b6ae236c 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs @@ -186,25 +186,25 @@ fromCore tab = case tab ^. Core.infoMain of convertCase :: HashMap Symbol Level -> Level -> [Level] -> Core.Case -> Geb convertCase identMap varsNum shiftLevels Core.Case {..} = - if - | null branches -> - GebAbsurd (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 - }, - _appRight = convertNode identMap varsNum shiftLevels defaultNode - } - | otherwise -> go indty shiftLevels _caseValue branches + if + | null branches -> + GebAbsurd (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 + }, + _appRight = convertNode identMap varsNum shiftLevels defaultNode + } + | otherwise -> go indty shiftLevels _caseValue branches where indty = convertInductive _caseInductive ii = fromJust $ HashMap.lookup _caseInductive (tab ^. Core.infoInductives) From 8f3884722996d1d9b7993a03469d6dbb0bc7dc9d Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 27 Jan 2023 13:25:03 +0100 Subject: [PATCH 13/20] tests & bugfixes --- .../Compiler/Backend/Geb/Translation/FromCore.hs | 9 +++++---- .../Core/Transformation/ComputeTypeInfo.hs | 4 ++-- tests/Geb/positive/Core/out/test001.out | 1 + tests/Geb/positive/Core/out/test002.out | 1 + tests/Geb/positive/Core/out/test003.out | 1 + tests/Geb/positive/Core/out/test004.out | 1 + tests/Geb/positive/Core/test001.jvc | 2 +- tests/Geb/positive/Core/test002.jvc | 2 +- tests/Geb/positive/Core/test003.jvc | 14 ++++++++++++++ tests/Geb/positive/Core/test004.jvc | 5 +++++ 10 files changed, 32 insertions(+), 8 deletions(-) create mode 100644 tests/Geb/positive/Core/out/test001.out create mode 100644 tests/Geb/positive/Core/out/test002.out create mode 100644 tests/Geb/positive/Core/out/test003.out create mode 100644 tests/Geb/positive/Core/out/test004.out create mode 100644 tests/Geb/positive/Core/test003.jvc create mode 100644 tests/Geb/positive/Core/test004.jvc diff --git a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs index d5b6ae236c..9c269be75e 100644 --- a/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs @@ -133,13 +133,13 @@ fromCore tab = case tab ^. Core.infoMain of (convertProduct identMap varsNum shiftLevels _constrArgs) convertProduct :: HashMap Symbol Level -> Level -> [Level] -> [Core.Node] -> Geb - convertProduct identMap varsNum shiftLevels = \case + 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)) - t + (reverse t) [] -> GebUnit where @@ -347,11 +347,12 @@ fromCore tab = case tab ^. Core.infoMain of Core.NPrim x -> convertTypePrim x Core.NDyn {} -> - unsupported -- no dynamic type in GEB + error "incomplete type information (dynamic type encountered)" Core.NLam Core.Lambda {..} -> convertType _lambdaBody _ -> - unsupported -- not a type + unsupported + convertPi :: Core.Pi -> Object convertPi Core.Pi {..} = ObjectHom diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index 9bba961c84..8bd82b34f9 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -37,7 +37,7 @@ computeNodeTypeInfo tab = umapL go in case lty of NPi Pi {..} | rty == _piBinder ^. binderType -> - _piBody + _piBody _ -> error "incorrect type information (application)" NBlt BuiltinApp {..} -> @@ -63,7 +63,7 @@ computeNodeTypeInfo tab = umapL go _ -> mkTypeConstr' (ci ^. constructorInductive) (take (length (ii ^. inductiveParams)) _constrArgs) NLam Lambda {..} -> - mkPi' (_lambdaBinder ^. binderType) (mkLambda' (Info.getNodeType _lambdaBody)) + mkPi' (_lambdaBinder ^. binderType) (Info.getNodeType _lambdaBody) NLet Let {..} -> Info.getNodeType _letBody NRec LetRec {..} -> diff --git a/tests/Geb/positive/Core/out/test001.out b/tests/Geb/positive/Core/out/test001.out new file mode 100644 index 0000000000..f3c260ef69 --- /dev/null +++ b/tests/Geb/positive/Core/out/test001.out @@ -0,0 +1 @@ +(right unit) diff --git a/tests/Geb/positive/Core/out/test002.out b/tests/Geb/positive/Core/out/test002.out new file mode 100644 index 0000000000..a0a32923d2 --- /dev/null +++ b/tests/Geb/positive/Core/out/test002.out @@ -0,0 +1 @@ +(left unit) diff --git a/tests/Geb/positive/Core/out/test003.out b/tests/Geb/positive/Core/out/test003.out new file mode 100644 index 0000000000..a0a32923d2 --- /dev/null +++ b/tests/Geb/positive/Core/out/test003.out @@ -0,0 +1 @@ +(left unit) diff --git a/tests/Geb/positive/Core/out/test004.out b/tests/Geb/positive/Core/out/test004.out new file mode 100644 index 0000000000..a0a32923d2 --- /dev/null +++ b/tests/Geb/positive/Core/out/test004.out @@ -0,0 +1 @@ +(left unit) diff --git a/tests/Geb/positive/Core/test001.jvc b/tests/Geb/positive/Core/test001.jvc index dd7e6babca..deb183aae0 100644 --- a/tests/Geb/positive/Core/test001.jvc +++ b/tests/Geb/positive/Core/test001.jvc @@ -1,2 +1,2 @@ -\(x : bool) if x then false else true +(\(x : bool) if x then false else true) true diff --git a/tests/Geb/positive/Core/test002.jvc b/tests/Geb/positive/Core/test002.jvc index 6c0d0c687f..1ff1c338dd 100644 --- a/tests/Geb/positive/Core/test002.jvc +++ b/tests/Geb/positive/Core/test002.jvc @@ -4,4 +4,4 @@ type optbool { Nothing : optbool; }; -\(x : bool) \(o : optbool) { case o of { Just b := if x then true else b; Nothing := false } } +(\(x : bool) \(o : optbool) { case o of { Just b := if x then true else b; Nothing := false } }) false (Just true) diff --git a/tests/Geb/positive/Core/test003.jvc b/tests/Geb/positive/Core/test003.jvc new file mode 100644 index 0000000000..d7e2771785 --- /dev/null +++ b/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) diff --git a/tests/Geb/positive/Core/test004.jvc b/tests/Geb/positive/Core/test004.jvc new file mode 100644 index 0000000000..0281a995fd --- /dev/null +++ b/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)) From bb45b25934f7651fce1a50c67e6e6f8f956d3009 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Fri, 27 Jan 2023 13:49:50 +0100 Subject: [PATCH 14/20] make ormolu happy --- src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index 8bd82b34f9..65472a869f 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -37,7 +37,7 @@ computeNodeTypeInfo tab = umapL go in case lty of NPi Pi {..} | rty == _piBinder ^. binderType -> - _piBody + _piBody _ -> error "incorrect type information (application)" NBlt BuiltinApp {..} -> From 7c5f2b2395fb6e0d65afacdd0b7bfcaac8d97033 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 30 Jan 2023 11:16:24 +0100 Subject: [PATCH 15/20] Adjust comment --- src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index 65472a869f..16ce40a529 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -9,9 +9,9 @@ import Juvix.Compiler.Core.Transformation.Base -- | Computes the TypeInfo for each subnode. -- -- Assumptions: --- 1. No polymorphism. --- 2. No dynamic type. --- 3. All binders and identifiers are decorated with full type information. +-- 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. From a657695a3f5545cc4544174e153660acfb3d02c6 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 31 Jan 2023 11:47:08 +0100 Subject: [PATCH 16/20] update cntlines.sh --- cntlines.sh | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/cntlines.sh b/cntlines.sh index 593a79873e..dda4adbc60 100755 --- a/cntlines.sh +++ b/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" From 8008d5a582f6578410e7525da71a4bea830851f9 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 31 Jan 2023 13:43:29 +0100 Subject: [PATCH 17/20] address review comments --- app/Commands/Dev/Core/Compile.hs | 38 +++++++++++-------- src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs | 10 +++-- 2 files changed, 28 insertions(+), 20 deletions(-) diff --git a/app/Commands/Dev/Core/Compile.hs b/app/Commands/Dev/Core/Compile.hs index 08ad86865f..cf547f39e6 100644 --- a/app/Commands/Dev/Core/Compile.hs +++ b/app/Commands/Dev/Core/Compile.hs @@ -11,14 +11,24 @@ 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)) case opts ^. compileTarget of - TargetGeb -> runGebPipeline opts file tab - _ -> runCPipeline opts file tab + 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) @@ -26,18 +36,16 @@ runCommand opts = do runCPipeline :: forall r. (Members '[Embed IO, App] r) => - CoreCompileOptions -> - Path Abs File -> - Core.InfoTable -> + PipelineArg -> Sem r () -runCPipeline opts file tab = do - C.MiniCResult {..} <- getRight (run (runError (coreToMiniC asmOpts tab :: Sem '[Error JuvixError] C.MiniCResult))) - cFile <- inputFile file ".c" +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 opts {_compileInputFile = AppPath (Abs cFile) False} + 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 @@ -49,13 +57,11 @@ runCPipeline opts file tab = do runGebPipeline :: forall r. (Members '[Embed IO, App] r) => - CoreCompileOptions -> - Path Abs File -> - Core.InfoTable -> + PipelineArg -> Sem r () -runGebPipeline _ file tab = do - Geb.Result {..} <- getRight (run (runError (coreToGeb tab :: Sem '[Error JuvixError] Geb.Result))) - gebFile <- inputFile file ".geb" +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) diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs index 888ef6e5cb..edbb6c2edd 100644 --- a/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs @@ -116,8 +116,9 @@ instance PrettyCode Object where ObjectCoprod x -> ppCode x ObjectHom x -> ppCode x -{--------------------------------------------------------------------------------} -{- helper functions -} +-------------------------------------------------------------------------------- +-- helper functions +-------------------------------------------------------------------------------- ppArg :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) => @@ -149,8 +150,9 @@ ppLRExpression associates fixlr e = parensIf (atomParens associates (atomicity e) fixlr) <$> ppCode e -{--------------------------------------------------------------------------------} -{- keywords -} +-------------------------------------------------------------------------------- +-- keywords +-------------------------------------------------------------------------------- kwAbsurd :: Doc Ann kwAbsurd = keyword Str.gebAbsurd From cc595b6e28b98c4786aa02bb67235d51444a77b7 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 31 Jan 2023 13:44:47 +0100 Subject: [PATCH 18/20] make ormolu happy --- app/Commands/Dev/Core/Compile.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/app/Commands/Dev/Core/Compile.hs b/app/Commands/Dev/Core/Compile.hs index cf547f39e6..48e07b2142 100644 --- a/app/Commands/Dev/Core/Compile.hs +++ b/app/Commands/Dev/Core/Compile.hs @@ -11,11 +11,11 @@ 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 -} +data PipelineArg = PipelineArg + { _pipelineArgOptions :: CoreCompileOptions, + _pipelineArgFile :: Path Abs File, + _pipelineArgInfoTable :: Core.InfoTable + } makeLenses ''PipelineArg From 1a549f628cc2e381a12eec33c472924637dd9af2 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 31 Jan 2023 16:05:44 +0100 Subject: [PATCH 19/20] 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) [] -> From 56bcde2b72f77bc574e0de7d5c8f767ad6e9e169 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 1 Feb 2023 11:11:52 +0100 Subject: [PATCH 20/20] fix ComputeTypeInfo --- src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs index 16ce40a529..d4661dd00a 100644 --- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -50,6 +50,9 @@ computeNodeTypeInfo tab = umapL go 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"