diff --git a/app/Commands/Dev/Asm/Compile.hs b/app/Commands/Dev/Asm/Compile.hs index 14d8db5c0..9dd419f70 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 12da3cec6..48e07b214 100644 --- a/app/Commands/Dev/Core/Compile.hs +++ b/app/Commands/Dev/Core/Compile.hs @@ -7,37 +7,65 @@ import Data.Text.IO qualified as TIO import Juvix.Compiler.Asm.Options qualified as Asm import Juvix.Compiler.Backend qualified as Backend import Juvix.Compiler.Backend.C qualified as C +import Juvix.Compiler.Backend.Geb qualified as Geb import Juvix.Compiler.Core.Data.InfoTable qualified as Core import Juvix.Compiler.Core.Translation.FromSource qualified as Core +data PipelineArg = PipelineArg + { _pipelineArgOptions :: CoreCompileOptions, + _pipelineArgFile :: Path Abs File, + _pipelineArgInfoTable :: Core.InfoTable + } + +makeLenses ''PipelineArg + runCommand :: forall r. (Members '[Embed IO, App] r) => CoreCompileOptions -> Sem r () runCommand opts = do file <- getFile s <- embed (readFile (toFilePath file)) tab <- getRight (mapLeft JuvixError (Core.runParserMain file Core.emptyInfoTable s)) - C.MiniCResult {..} <- getRight (run (runError (coreToMiniC asmOpts tab :: Sem '[Error JuvixError] C.MiniCResult))) - buildDir <- askBuildDir - ensureDir buildDir - cFile <- inputCFile file - embed $ TIO.writeFile (toFilePath cFile) _resultCCode - Compile.runCommand opts {_compileInputFile = AppPath (Abs cFile) False} + case opts ^. compileTarget of + TargetGeb -> runGebPipeline (PipelineArg opts file tab) + TargetWasm32Wasi -> runCPipeline (PipelineArg opts file tab) + TargetNative64 -> runCPipeline (PipelineArg opts file tab) + TargetC -> runCPipeline (PipelineArg opts file tab) where getFile :: Sem r (Path Abs File) getFile = someBaseToAbs' (opts ^. compileInputFile . pathPath) +runCPipeline :: + forall r. + (Members '[Embed IO, App] r) => + PipelineArg -> + Sem r () +runCPipeline PipelineArg {..} = do + C.MiniCResult {..} <- getRight (run (runError (coreToMiniC asmOpts _pipelineArgInfoTable :: Sem '[Error JuvixError] C.MiniCResult))) + cFile <- inputFile _pipelineArgFile ".c" + embed $ TIO.writeFile (toFilePath cFile) _resultCCode + Compile.runCommand _pipelineArgOptions {_compileInputFile = AppPath (Abs cFile) False} + where asmOpts :: Asm.Options - asmOpts = Asm.makeOptions (asmTarget (opts ^. compileTarget)) (opts ^. compileDebug) + asmOpts = Asm.makeOptions (asmTarget (_pipelineArgOptions ^. compileTarget)) (_pipelineArgOptions ^. compileDebug) asmTarget :: CompileTarget -> Backend.Target asmTarget = \case TargetWasm32Wasi -> Backend.TargetCWasm32Wasi TargetNative64 -> Backend.TargetCNative64 TargetC -> Backend.TargetCWasm32Wasi + TargetGeb -> impossible -inputCFile :: (Members '[App] r) => Path Abs File -> Sem r (Path Abs File) -inputCFile inputFileCompile = do +runGebPipeline :: + forall r. + (Members '[Embed IO, App] r) => + PipelineArg -> + Sem r () +runGebPipeline PipelineArg {..} = do + Geb.Result {..} <- getRight (run (runError (coreToGeb _pipelineArgInfoTable :: Sem '[Error JuvixError] Geb.Result))) + gebFile <- inputFile _pipelineArgFile ".geb" + embed $ TIO.writeFile (toFilePath gebFile) _resultCode + +inputFile :: (Members '[Embed IO, App] r) => Path Abs File -> String -> Sem r (Path Abs File) +inputFile inputFileCompile ext = do buildDir <- askBuildDir - return (buildDir outputMiniCFile) - where - outputMiniCFile :: Path Rel File - outputMiniCFile = replaceExtension' ".c" (filename inputFileCompile) + ensureDir buildDir + return (buildDir replaceExtension' ext (filename inputFileCompile)) diff --git a/app/Commands/Extra/Compile.hs b/app/Commands/Extra/Compile.hs index 0d8eb17c6..2b287ac10 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 6536ce94e..db66c1465 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/cntlines.sh b/cntlines.sh index 593a79873..dda4adbc6 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" diff --git a/src/Juvix/Compiler/Asm/Pretty/Base.hs b/src/Juvix/Compiler/Asm/Pretty/Base.hs index 08fbadd05..4deb9d2a9 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.hs b/src/Juvix/Compiler/Backend/Geb.hs new file mode 100644 index 000000000..321aed451 --- /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/Extra.hs b/src/Juvix/Compiler/Backend/Geb/Extra.hs new file mode 100644 index 000000000..1ba05a2d4 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Extra.hs @@ -0,0 +1,10 @@ +module Juvix.Compiler.Backend.Geb.Extra where + +import Juvix.Compiler.Backend.Geb.Language + +-- | Destructs a product in a right-associative way, e.g., (a, (b, c)) is +-- destructed to [a, b, c] +destructProduct :: Object -> [Object] +destructProduct = \case + ObjectProduct Product {..} -> _productLeft : destructProduct _productRight + x -> [x] diff --git a/src/Juvix/Compiler/Backend/Geb/Language.hs b/src/Juvix/Compiler/Backend/Geb/Language.hs new file mode 100644 index 000000000..63611ea06 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Language.hs @@ -0,0 +1,137 @@ +module Juvix.Compiler.Backend.Geb.Language + ( module Juvix.Compiler.Backend.Geb.Language, + module Juvix.Prelude, + ) +where + +import Juvix.Prelude hiding (First, Product) + +{- + The following datatypes correspond to GEB types for terms + (https://github.com/anoma/geb/blob/main/src/specs/lambda.lisp) and types + (https://github.com/anoma/geb/blob/main/src/specs/geb.lisp). +-} + +-- | Represents GEB's `case-on`. `_caseOn` is the value matched on of type +-- `Dom`, `_caseLeft` has type `_caseLeftType -> _caseCodomainType` and +-- `_caseRight` has type `_caseRightType -> _caseCodomainType`. +data Case = Case + { _caseLeftType :: Object, + _caseRightType :: Object, + _caseCodomainType :: Object, + _caseOn :: Morphism, + _caseLeft :: Morphism, + _caseRight :: Morphism + } + +data Pair = Pair + { _pairLeftType :: Object, + _pairRightType :: Object, + _pairLeft :: Morphism, + _pairRight :: Morphism + } + +data First = First + { _firstLeftType :: Object, + _firstRightType :: Object, + _firstValue :: Morphism + } + +data Second = Second + { _secondLeftType :: Object, + _secondRightType :: Object, + _secondValue :: Morphism + } + +data Lambda = Lambda + { _lambdaVarType :: Object, + _lambdaBodyType :: Object, + _lambdaBody :: Morphism + } + +data Application = Application + { _applicationDomainType :: Object, + _applicationCodomainType :: Object, + _applicationLeft :: Morphism, + _applicationRight :: Morphism + } + +newtype Var = Var {_varIndex :: Int} + +-- | Corresponds to the GEB type for morphisms (terms): `stlc` +-- (https://github.com/anoma/geb/blob/main/src/specs/lambda.lisp). +data Morphism + = MorphismAbsurd Morphism + | MorphismUnit + | MorphismLeft Morphism + | MorphismRight Morphism + | MorphismCase Case + | MorphismPair Pair + | MorphismFirst First + | MorphismSecond Second + | MorphismLambda Lambda + | MorphismApplication Application + | MorphismVar Var + +data Product = Product + { _productLeft :: Object, + _productRight :: Object + } + +data Coproduct = Coproduct + { _coproductLeft :: Object, + _coproductRight :: Object + } + +-- | Function type +data Hom = Hom + { _homDomain :: Object, + _homCodomain :: Object + } + +-- | Corresponds to the GEB type for types (objects of the category): `substobj` +-- (https://github.com/anoma/geb/blob/main/src/specs/geb.lisp). +data Object + = -- | empty type + ObjectInitial + | -- | unit type + ObjectTerminal + | ObjectProduct Product + | ObjectCoproduct Coproduct + | -- | function type + ObjectHom Hom + +instance HasAtomicity Morphism where + atomicity = \case + MorphismAbsurd {} -> Aggregate appFixity + MorphismUnit -> Atom + MorphismLeft {} -> Aggregate appFixity + MorphismRight {} -> Aggregate appFixity + MorphismCase {} -> Aggregate appFixity + MorphismPair {} -> Aggregate appFixity + MorphismFirst {} -> Aggregate appFixity + MorphismSecond {} -> Aggregate appFixity + MorphismLambda {} -> Aggregate appFixity + MorphismApplication {} -> Aggregate appFixity + MorphismVar {} -> Aggregate appFixity + +instance HasAtomicity Object where + atomicity = \case + ObjectInitial -> Atom + ObjectTerminal -> Atom + ObjectProduct {} -> Aggregate appFixity + ObjectCoproduct {} -> Aggregate appFixity + ObjectHom {} -> Aggregate appFixity + +makeLenses ''Case +makeLenses ''Pair +makeLenses ''First +makeLenses ''Second +makeLenses ''Lambda +makeLenses ''Var +makeLenses ''Application +makeLenses ''Morphism +makeLenses ''Product +makeLenses ''Coproduct +makeLenses ''Hom +makeLenses ''Object diff --git a/src/Juvix/Compiler/Backend/Geb/Pretty.hs b/src/Juvix/Compiler/Backend/Geb/Pretty.hs new file mode 100644 index 000000000..a20fb1624 --- /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 :: (HasAtomicity c, PrettyCode c) => c -> AnsiText +ppOutDefault = AnsiText . PPOutput . doc defaultOptions + +ppOut :: (CanonicalProjection a Options, HasAtomicity c, PrettyCode c) => a -> c -> AnsiText +ppOut o = AnsiText . PPOutput . doc (project o) + +ppTrace' :: (CanonicalProjection a Options, HasAtomicity c, PrettyCode c) => a -> c -> Text +ppTrace' opts = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc (project opts) + +ppTrace :: (HasAtomicity c, PrettyCode c) => c -> Text +ppTrace = ppTrace' traceOptions + +ppPrint :: (HasAtomicity c, PrettyCode c) => c -> Text +ppPrint = show . ppOutDefault 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 000000000..86543095e --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Base.hs @@ -0,0 +1,207 @@ +module Juvix.Compiler.Backend.Geb.Pretty.Base + ( module Juvix.Compiler.Backend.Geb.Pretty.Base, + module Juvix.Data.CodeAnn, + module Juvix.Compiler.Backend.Geb.Pretty.Options, + ) +where + +import Juvix.Compiler.Backend.Geb.Language +import Juvix.Compiler.Backend.Geb.Pretty.Options +import Juvix.Data.CodeAnn +import Juvix.Extra.Strings qualified as Str + +doc :: (HasAtomicity c, PrettyCode c) => Options -> c -> Doc Ann +doc opts x = + run $ + runReader opts $ + case atomicity x of + Atom -> ppCode x + Aggregate _ -> parens <$> ppCode x + +class PrettyCode c where + ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann) + +instance PrettyCode Case where + ppCode Case {..} = do + lty <- ppArg _caseLeftType + rty <- ppArg _caseRightType + cod <- ppArg _caseCodomainType + val <- ppArg _caseOn + left <- ppArg _caseLeft + right <- ppArg _caseRight + return $ kwCase <+> lty <+> rty <+> cod <+> val <+> left <+> right + +instance PrettyCode Pair where + ppCode Pair {..} = do + lty <- ppArg _pairLeftType + rty <- ppArg _pairRightType + left <- ppArg _pairLeft + right <- ppArg _pairRight + return $ kwPair <+> lty <+> rty <+> left <+> right + +instance PrettyCode First where + ppCode First {..} = do + lty <- ppArg _firstLeftType + rty <- ppArg _firstRightType + val <- ppArg _firstValue + return $ kwFst <+> lty <+> rty <+> val + +instance PrettyCode Second where + ppCode Second {..} = do + lty <- ppArg _secondLeftType + rty <- ppArg _secondRightType + val <- ppArg _secondValue + return $ kwSnd <+> lty <+> rty <+> val + +instance PrettyCode Lambda where + ppCode Lambda {..} = do + vty <- ppArg _lambdaVarType + bty <- ppArg _lambdaBodyType + body <- ppArg _lambdaBody + return $ kwLamb <+> vty <+> bty <+> body + +instance PrettyCode Application where + ppCode Application {..} = do + dom <- ppArg _applicationDomainType + cod <- ppArg _applicationCodomainType + left <- ppArg _applicationLeft + right <- ppArg _applicationRight + return $ kwApp <+> dom <+> cod <+> left <+> right + +instance PrettyCode Var where + ppCode Var {..} = return $ annotate AnnLiteralInteger (pretty _varIndex) + +instance PrettyCode Morphism where + ppCode = \case + MorphismAbsurd val -> do + v <- ppArg val + return $ kwAbsurd <+> v + MorphismUnit -> + return kwUnit + MorphismLeft val -> do + v <- ppArg val + return $ kwLeft <+> v + MorphismRight val -> do + v <- ppArg val + return $ kwRight <+> v + MorphismCase x -> ppCode x + MorphismPair x -> ppCode x + MorphismFirst x -> ppCode x + MorphismSecond x -> ppCode x + MorphismLambda x -> ppCode x + MorphismApplication x -> ppCode x + MorphismVar idx -> do + i <- ppCode idx + return $ kwVar <+> i + +instance PrettyCode Product where + ppCode Product {..} = do + left <- ppArg _productLeft + right <- ppArg _productRight + return $ kwProd <+> left <+> right + +instance PrettyCode Coproduct where + ppCode Coproduct {..} = do + left <- ppArg _coproductLeft + right <- ppArg _coproductRight + return $ kwCoprod <+> left <+> right + +instance PrettyCode Hom where + ppCode Hom {..} = do + dom <- ppArg _homDomain + cod <- ppArg _homCodomain + return $ kwHom <+> dom <+> cod + +instance PrettyCode Object where + ppCode = \case + ObjectInitial -> return kwInitial + ObjectTerminal -> return kwTerminal + ObjectProduct x -> ppCode x + ObjectCoproduct x -> ppCode x + ObjectHom x -> ppCode x + +-------------------------------------------------------------------------------- +-- helper functions +-------------------------------------------------------------------------------- + +ppArg :: + (PrettyCode a, HasAtomicity a, Member (Reader Options) r) => + a -> + Sem r (Doc Ann) +ppArg = ppRightExpression appFixity + +ppRightExpression :: + (PrettyCode a, HasAtomicity a, Member (Reader Options) r) => + Fixity -> + a -> + Sem r (Doc Ann) +ppRightExpression = ppLRExpression isRightAssoc + +ppLeftExpression :: + (PrettyCode a, HasAtomicity a, Member (Reader Options) r) => + Fixity -> + a -> + Sem r (Doc Ann) +ppLeftExpression = ppLRExpression isLeftAssoc + +ppLRExpression :: + (HasAtomicity a, PrettyCode a, Member (Reader Options) r) => + (Fixity -> Bool) -> + Fixity -> + a -> + Sem r (Doc Ann) +ppLRExpression associates fixlr e = + parensIf (atomParens associates (atomicity e) fixlr) + <$> ppCode e + +-------------------------------------------------------------------------------- +-- keywords +-------------------------------------------------------------------------------- + +kwAbsurd :: Doc Ann +kwAbsurd = keyword Str.gebAbsurd + +kwUnit :: Doc Ann +kwUnit = keyword Str.gebUnit + +kwLeft :: Doc Ann +kwLeft = keyword Str.gebLeft + +kwRight :: Doc Ann +kwRight = keyword Str.gebRight + +kwFst :: Doc Ann +kwFst = keyword Str.gebFst + +kwSnd :: Doc Ann +kwSnd = keyword Str.gebSnd + +kwCase :: Doc Ann +kwCase = keyword Str.gebCase + +kwPair :: Doc Ann +kwPair = keyword Str.gebPair + +kwLamb :: Doc Ann +kwLamb = keyword Str.gebLamb + +kwApp :: Doc Ann +kwApp = keyword Str.gebApp + +kwVar :: Doc Ann +kwVar = keyword Str.gebVar + +kwInitial :: Doc Ann +kwInitial = keyword Str.gebInitial + +kwTerminal :: Doc Ann +kwTerminal = keyword Str.gebTerminal + +kwProd :: Doc Ann +kwProd = keyword Str.gebProd + +kwCoprod :: Doc Ann +kwCoprod = keyword Str.gebCoprod + +kwHom :: Doc Ann +kwHom = keyword Str.gebHom 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 000000000..b6123a31a --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Pretty/Options.hs @@ -0,0 +1,21 @@ +module Juvix.Compiler.Backend.Geb.Pretty.Options where + +import Juvix.Prelude + +-- no fields for now, but make it easier to add options in the future I don't +-- remove this datatype entirely +data Options = Options + +makeLenses ''Options + +defaultOptions :: Options +defaultOptions = Options + +traceOptions :: Options +traceOptions = Options + +fromGenericOptions :: GenericOptions -> Options +fromGenericOptions _ = defaultOptions + +instance CanonicalProjection GenericOptions Options where + project = fromGenericOptions diff --git a/src/Juvix/Compiler/Backend/Geb/Translation.hs b/src/Juvix/Compiler/Backend/Geb/Translation.hs new file mode 100644 index 000000000..ff811337e --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Translation.hs @@ -0,0 +1,16 @@ +module Juvix.Compiler.Backend.Geb.Translation + ( module Juvix.Compiler.Backend.Geb.Translation, + module Juvix.Compiler.Backend.Geb.Translation.FromCore, + ) +where + +import Juvix.Compiler.Backend.Geb.Language +import Juvix.Compiler.Backend.Geb.Pretty +import Juvix.Compiler.Backend.Geb.Translation.FromCore + +newtype Result = Result + { _resultCode :: Text + } + +toResult :: Morphism -> Result +toResult geb = Result (ppPrint geb <> "\n") 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 000000000..236357267 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs @@ -0,0 +1,397 @@ +module Juvix.Compiler.Backend.Geb.Translation.FromCore where + +import Data.HashMap.Strict qualified as HashMap +import Data.List qualified as List +import Juvix.Compiler.Backend.Geb.Extra +import Juvix.Compiler.Backend.Geb.Language +import Juvix.Compiler.Core.Data.InfoTable qualified as Core +import Juvix.Compiler.Core.Extra qualified as Core +import Juvix.Compiler.Core.Info.TypeInfo qualified as Info +import Juvix.Compiler.Core.Language (Index, Level, Symbol) +import Juvix.Compiler.Core.Language qualified as Core + +fromCore :: Core.InfoTable -> Morphism +fromCore tab = case tab ^. Core.infoMain of + Just sym -> + let node = fromJust $ HashMap.lookup sym (tab ^. Core.identContext) + idents = HashMap.delete sym (tab ^. Core.infoIdentifiers) + in goIdents mempty 0 [] node (HashMap.elems idents) + Nothing -> + error "no main function" + where + unsupported :: forall a. a + unsupported = error "unsupported" + + {- + The translation of each identifier is saved separately to avoid exponential + blow-up. For example, the program: + ``` + a : A + + f : A -> A + f x = F + + g : A -> A + g x = f (f x) + + main : A + main = g (g a) + ``` + is translated as if it were a single node: + ``` + (\a -> (\f -> (\g -> g (g a)) (\x -> f (f x))) (\x -> F)) a + ``` + -} + goIdents :: HashMap Symbol Level -> Level -> [Level] -> Core.Node -> [Core.IdentifierInfo] -> Morphism + goIdents identMap level shiftLevels node = \case + ii : idents -> + MorphismApplication + Application + { _applicationDomainType = argty, + _applicationCodomainType = nodeType, + _applicationLeft = lamb, + _applicationRight = convertNode identMap 0 shiftLevels fundef + } + where + sym = ii ^. Core.identifierSymbol + fundef = fromJust $ HashMap.lookup sym (tab ^. Core.identContext) + argty = convertType (Info.getNodeType fundef) + body = goIdents (HashMap.insert sym level identMap) (level + 1) (0 : shiftLevels) node idents + lamb = + MorphismLambda + Lambda + { _lambdaVarType = argty, + _lambdaBodyType = nodeType, + _lambdaBody = body + } + [] -> + convertNode identMap 0 shiftLevels node + where + nodeType = convertType (Info.getNodeType node) + + -- `shiftLevels` contains the de Bruijn levels immediately before which a + -- binder was inserted + convertNode :: HashMap Symbol Level -> Level -> [Level] -> Core.Node -> Morphism + convertNode identMap varsNum shiftLevels = \case + Core.NVar x -> convertVar identMap varsNum shiftLevels x + Core.NIdt x -> convertIdent identMap varsNum shiftLevels x + Core.NCst x -> convertConstant identMap varsNum shiftLevels x + Core.NApp x -> convertApp identMap varsNum shiftLevels x + Core.NBlt x -> convertBuiltinApp identMap varsNum shiftLevels x + Core.NCtr x -> convertConstr identMap varsNum shiftLevels x + Core.NLam x -> convertLambda identMap varsNum shiftLevels x + Core.NLet x -> convertLet identMap varsNum shiftLevels x + Core.NRec {} -> unsupported -- LetRecs should be lifted out beforehand + Core.NCase x -> convertCase identMap varsNum shiftLevels x + Core.NMatch {} -> unsupported -- Pattern matching should be compiled beforehand + Core.NPi {} -> unsupported + Core.NUniv {} -> unsupported + Core.NTyp {} -> unsupported + Core.NPrim {} -> unsupported + Core.NDyn {} -> unsupported + Core.Closure {} -> unsupported + + insertedBinders :: Level -> [Level] -> Index -> Int + insertedBinders varsNum shiftLevels idx = + length (filter ((varsNum - idx) <=) shiftLevels) + + convertVar :: HashMap Symbol Level -> Level -> [Level] -> Core.Var -> Morphism + convertVar _ varsNum shiftLevels Core.Var {..} = + MorphismVar (Var (_varIndex + insertedBinders varsNum shiftLevels _varIndex)) + + convertIdent :: HashMap Symbol Level -> Level -> [Level] -> Core.Ident -> Morphism + convertIdent identMap varsNum shiftLevels Core.Ident {..} = + MorphismVar (Var (varsNum + length shiftLevels - fromJust (HashMap.lookup _identSymbol identMap) - 1)) + + convertConstant :: HashMap Symbol Level -> Level -> [Level] -> Core.Constant -> Morphism + convertConstant _ _ _ Core.Constant {} = unsupported + + convertApp :: HashMap Symbol Level -> Level -> [Level] -> Core.App -> Morphism + convertApp identMap varsNum shiftLevels Core.App {..} = + MorphismApplication + Application + { _applicationDomainType = convertType (Info.getNodeType _appRight), + _applicationCodomainType = convertType (Info.getInfoType _appInfo), + _applicationLeft = convertNode identMap varsNum shiftLevels _appLeft, + _applicationRight = convertNode identMap varsNum shiftLevels _appRight + } + + convertBuiltinApp :: HashMap Symbol Level -> Level -> [Level] -> Core.BuiltinApp -> Morphism + convertBuiltinApp _ _ _ Core.BuiltinApp {} = unsupported + + convertConstr :: HashMap Symbol Level -> Level -> [Level] -> Core.Constr -> Morphism + convertConstr identMap varsNum shiftLevels Core.Constr {..} = + foldr ($) prod (replicate tagNum MorphismRight) + where + ci = fromJust $ HashMap.lookup _constrTag (tab ^. Core.infoConstructors) + sym = ci ^. Core.constructorInductive + ctrs = fromJust (HashMap.lookup sym (tab ^. Core.infoInductives)) ^. Core.inductiveConstructors + tagNum = fromJust $ elemIndex _constrTag (sort (map (^. Core.constructorTag) ctrs)) + prod = + (if tagNum == length ctrs - 1 then id else MorphismLeft) + (convertProduct identMap varsNum shiftLevels _constrArgs) + + convertProduct :: HashMap Symbol Level -> Level -> [Level] -> [Core.Node] -> Morphism + convertProduct identMap varsNum shiftLevels args = case reverse args of + h : t -> + fst $ + foldr + (\x -> mkPair (convertNode identMap varsNum shiftLevels x, convertType (Info.getNodeType x))) + (convertNode identMap varsNum shiftLevels h, convertType (Info.getNodeType h)) + (reverse t) + [] -> + MorphismUnit + where + mkPair :: (Morphism, Object) -> (Morphism, Object) -> (Morphism, Object) + mkPair (x, xty) (y, yty) = (z, zty) + where + z = + MorphismPair + Pair + { _pairLeftType = xty, + _pairRightType = yty, + _pairLeft = x, + _pairRight = y + } + zty = ObjectProduct (Product xty yty) + + convertLet :: HashMap Symbol Level -> Level -> [Level] -> Core.Let -> Morphism + convertLet identMap varsNum shiftLevels Core.Let {..} = + MorphismApplication + Application + { _applicationCodomainType = domty, + _applicationDomainType = codty, + _applicationLeft = + MorphismLambda + Lambda + { _lambdaVarType = domty, + _lambdaBodyType = codty, + _lambdaBody = convertNode identMap varsNum shiftLevels _letBody + }, + _applicationRight = convertNode identMap varsNum shiftLevels (_letItem ^. Core.letItemValue) + } + where + domty = convertType (_letItem ^. Core.letItemBinder . Core.binderType) + codty = convertType (Info.getNodeType _letBody) + + convertLambda :: HashMap Symbol Level -> Level -> [Level] -> Core.Lambda -> Morphism + convertLambda identMap varsNum shiftLevels Core.Lambda {..} = + MorphismLambda + Lambda + { _lambdaVarType = convertType (_lambdaBinder ^. Core.binderType), + _lambdaBodyType = convertType (Info.getNodeType _lambdaBody), + _lambdaBody = convertNode identMap (varsNum + 1) shiftLevels _lambdaBody + } + + convertCase :: HashMap Symbol Level -> Level -> [Level] -> Core.Case -> Morphism + convertCase identMap varsNum shiftLevels Core.Case {..} = + if + | null branches -> + MorphismAbsurd (convertNode identMap varsNum shiftLevels _caseValue) + | missingCtrsNum > 1 -> + let ty = convertType (Info.getNodeType defaultNode) + in MorphismApplication + Application + { _applicationDomainType = ty, + _applicationCodomainType = ty, + _applicationLeft = + MorphismLambda + Lambda + { _lambdaVarType = ty, + _lambdaBodyType = ty, + _lambdaBody = go indty (varsNum : shiftLevels) _caseValue branches + }, + _applicationRight = convertNode identMap varsNum shiftLevels defaultNode + } + | otherwise -> go indty shiftLevels _caseValue branches + where + indty = convertInductive _caseInductive + ii = fromJust $ HashMap.lookup _caseInductive (tab ^. Core.infoInductives) + missingCtrs = + filter + ( \x -> + isNothing (find (\y -> x ^. Core.constructorTag == y ^. Core.caseBranchTag) _caseBranches) + ) + (ii ^. Core.inductiveConstructors) + missingCtrsNum = length missingCtrs + ctrBrs = map mkCtrBranch missingCtrs + defaultNode = fromMaybe (error "not all cases covered") _caseDefault + -- `branches` contains one branch for each constructor of the inductive type. + -- `_caseDefault` is the body of those branches which were not present in + -- `_caseBranches`. + branches = sortOn (^. Core.caseBranchTag) (_caseBranches ++ ctrBrs) + codty = convertType (Info.getNodeType (List.head branches ^. Core.caseBranchBody)) + + mkCtrBranch :: Core.ConstructorInfo -> Core.CaseBranch + mkCtrBranch ci = + Core.CaseBranch + { _caseBranchInfo = mempty, + _caseBranchTag = ci ^. Core.constructorTag, + _caseBranchBinders = map (Core.Binder "?" Nothing) tyargs, + _caseBranchBindersNum = n, + _caseBranchBody = defaultBody n + } + where + tyargs = Core.typeArgs (ci ^. Core.constructorType) + n = length tyargs + defaultBody = + if + | missingCtrsNum > 1 -> Core.mkVar' + | otherwise -> (`Core.shift` defaultNode) + + go :: Object -> [Level] -> Core.Node -> [Core.CaseBranch] -> Morphism + go ty lvls val = \case + [br] -> + -- there is only one constructor, so `ty` is a product of its argument types + mkBranch ty lvls val br + br : brs -> + MorphismCase + Case + { _caseLeftType = lty, + _caseRightType = rty, + _caseCodomainType = codty, + _caseOn = convertNode identMap varsNum lvls val, + _caseLeft = + MorphismLambda + Lambda + { _lambdaVarType = lty, + _lambdaBodyType = codty, + _lambdaBody = mkBranch lty (varsNum : lvls) val br + }, + _caseRight = + MorphismLambda + Lambda + { _lambdaVarType = rty, + _lambdaBodyType = codty, + _lambdaBody = go rty (varsNum : lvls) (Core.mkVar' 0) brs + } + } + where + (lty, rty) = case ty of + ObjectCoproduct Coproduct {..} -> (_coproductLeft, _coproductRight) + _ -> impossible + [] -> impossible + + mkBranch :: Object -> [Level] -> Core.Node -> Core.CaseBranch -> Morphism + mkBranch valty lvls val Core.CaseBranch {..} = + if + | _caseBranchBindersNum == 0 -> + branch + | otherwise -> + mkApps (mkLambs argtys) (convertNode identMap varsNum lvls val) valty argtys + where + branch = convertNode identMap (varsNum + _caseBranchBindersNum) lvls _caseBranchBody + argtys = destructProduct valty + + mkApps :: Morphism -> Morphism -> Object -> [Object] -> Morphism + mkApps acc v vty = \case + ty : tys -> + mkApps acc' v' rty tys + where + v' = + MorphismSecond + Second + { _secondLeftType = lty, + _secondRightType = rty, + _secondValue = v + } + acc' = + MorphismApplication + Application + { _applicationDomainType = ty, + _applicationCodomainType = vty, + _applicationLeft = acc, + _applicationRight = + if + | null tys -> + v + | otherwise -> + MorphismFirst + First + { _firstLeftType = lty, + _firstRightType = rty, + _firstValue = v + } + } + (lty, rty) = case vty of + ObjectProduct Product {..} -> (_productLeft, _productRight) + _ -> impossible + [] -> + acc + + mkLambs :: [Object] -> Morphism + mkLambs = + fst + . foldr + ( \ty (acc, accty) -> + ( MorphismLambda + Lambda + { _lambdaVarType = ty, + _lambdaBodyType = accty, + _lambdaBody = acc + }, + ObjectHom (Hom ty accty) + ) + ) + (branch, codty) + + convertType :: Core.Type -> Object + convertType = \case + Core.NPi x -> + convertPi x + Core.NUniv {} -> + unsupported -- no polymorphism yet + Core.NTyp x -> + convertTypeConstr x + Core.NPrim x -> + convertTypePrim x + Core.NDyn {} -> + error "incomplete type information (dynamic type encountered)" + Core.NLam Core.Lambda {..} -> + convertType _lambdaBody + _ -> + unsupported + + convertPi :: Core.Pi -> Object + convertPi Core.Pi {..} = + ObjectHom + Hom + { _homDomain = convertType (_piBinder ^. Core.binderType), + _homCodomain = convertType _piBody + } + + convertTypeConstr :: Core.TypeConstr -> Object + convertTypeConstr Core.TypeConstr {..} = convertInductive _typeConstrSymbol + + convertTypePrim :: Core.TypePrim -> Object + convertTypePrim Core.TypePrim {..} = + case _typePrimPrimitive of + Core.PrimInteger _ -> unsupported + Core.PrimBool _ -> ObjectCoproduct (Coproduct ObjectTerminal ObjectTerminal) + Core.PrimString -> unsupported + + convertInductive :: Symbol -> Object + convertInductive sym = + case reverse ctrs of + ci : ctrs' -> + foldr + (\x acc -> ObjectCoproduct (Coproduct (convertConstructorType (x ^. Core.constructorType)) acc)) + (convertConstructorType (ci ^. Core.constructorType)) + (reverse ctrs') + [] -> + ObjectInitial + where + ctrs = + sortOn (^. Core.constructorTag) $ + fromJust (HashMap.lookup sym (tab ^. Core.infoInductives)) ^. Core.inductiveConstructors + + convertConstructorType :: Core.Node -> Object + convertConstructorType ty = + case reverse (Core.typeArgs ty) of + hty : tys -> + foldr + (\x acc -> ObjectProduct (Product (convertType x) acc)) + (convertType hty) + (reverse tys) + [] -> + ObjectTerminal diff --git a/src/Juvix/Compiler/Core/Data/BinderList.hs b/src/Juvix/Compiler/Core/Data/BinderList.hs index 514c760f0..102992b4b 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/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs index 073307195..3931a62b9 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 032d9bca0..b6d29a7e6 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 @@ -67,6 +69,8 @@ transformation = <|> symbol strMoveApps $> MoveApps <|> symbol strNatToInt $> NatToInt <|> symbol strConvertBuiltinTypes $> ConvertBuiltinTypes + <|> symbol strUnrollRecursion $> UnrollRecursion + <|> symbol strComputeTypeInfo $> ComputeTypeInfo allStrings :: [Text] allStrings = @@ -76,7 +80,9 @@ allStrings = strRemoveTypeArgs, strMoveApps, strNatToInt, - strConvertBuiltinTypes + strConvertBuiltinTypes, + strUnrollRecursion, + strComputeTypeInfo ] strLifting :: Text @@ -99,3 +105,9 @@ strNatToInt = "nat-to-int" strConvertBuiltinTypes :: Text strConvertBuiltinTypes = "convert-builtin-types" + +strComputeTypeInfo :: Text +strComputeTypeInfo = "compute-type-info" + +strUnrollRecursion :: Text +strUnrollRecursion = "unroll-recursion" diff --git a/src/Juvix/Compiler/Core/Info/TypeInfo.hs b/src/Juvix/Compiler/Core/Info/TypeInfo.hs new file mode 100644 index 000000000..0d888fb02 --- /dev/null +++ b/src/Juvix/Compiler/Core/Info/TypeInfo.hs @@ -0,0 +1,33 @@ +module Juvix.Compiler.Core.Info.TypeInfo where + +import Juvix.Compiler.Core.Extra.Base +import Juvix.Compiler.Core.Extra.Info +import Juvix.Compiler.Core.Info qualified as Info +import Juvix.Compiler.Core.Language + +newtype TypeInfo = TypeInfo {_infoType :: Type} + +instance IsInfo TypeInfo + +kTypeInfo :: Key TypeInfo +kTypeInfo = Proxy + +makeLenses ''TypeInfo + +getInfoType :: Info -> Type +getInfoType i = + case Info.lookup kTypeInfo i of + Just TypeInfo {..} -> _infoType + Nothing -> mkDynamic' + +setInfoType :: Type -> Info -> Info +setInfoType = Info.insert . TypeInfo + +getNodeType :: Node -> Type +getNodeType = getInfoType . getInfo + +setNodeType :: Type -> Node -> Node +setNodeType = modifyInfo . setInfoType + +removeTypeInfo :: Node -> Node +removeTypeInfo = removeInfo kTypeInfo diff --git a/src/Juvix/Compiler/Core/Language/Base.hs b/src/Juvix/Compiler/Core/Language/Base.hs index 880d7e384..388d858ea 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 273b9013d..a3aa694bc 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 diff --git a/src/Juvix/Compiler/Core/Pipeline.hs b/src/Juvix/Compiler/Core/Pipeline.hs index ae4ce79f8..197a48a56 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/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 4e93b8b66..1ff66c0bd 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/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs index b4f8988d7..aa34a59d8 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,6 +19,7 @@ import Juvix.Compiler.Core.Transformation.MoveApps import Juvix.Compiler.Core.Transformation.NatToInt import Juvix.Compiler.Core.Transformation.RemoveTypeArgs import Juvix.Compiler.Core.Transformation.TopEtaExpand +import Juvix.Compiler.Core.Transformation.UnrollRecursion applyTransformations :: [TransformationId] -> InfoTable -> InfoTable applyTransformations ts tbl = foldl' (flip appTrans) tbl ts @@ -31,3 +33,5 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts MoveApps -> moveApps NatToInt -> natToInt ConvertBuiltinTypes -> convertBuiltinTypes + ComputeTypeInfo -> computeTypeInfo + UnrollRecursion -> unrollRecursion diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs new file mode 100644 index 000000000..d4661dd00 --- /dev/null +++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs @@ -0,0 +1,96 @@ +module Juvix.Compiler.Core.Transformation.ComputeTypeInfo (computeTypeInfo) where + +import Data.HashMap.Strict qualified as HashMap +import Juvix.Compiler.Core.Data.BinderList qualified as BL +import Juvix.Compiler.Core.Extra +import Juvix.Compiler.Core.Info.TypeInfo qualified as Info +import Juvix.Compiler.Core.Transformation.Base + +-- | Computes the TypeInfo for each subnode. +-- +-- Assumptions: +-- 1. All binders and identifiers are decorated with full type information. +-- 2. No polymorphism. +-- 3. No dynamic type. +-- 4. All cases have at least one branch. +-- 5. No `Match` nodes. +-- 6. All inductives and function types are in universe 0. +computeNodeTypeInfo :: InfoTable -> Node -> Node +computeNodeTypeInfo tab = umapL go + where + go :: BinderList Binder -> Node -> Node + go bl node = Info.setNodeType (nodeType bl node) node + + nodeType :: BinderList Binder -> Node -> Type + nodeType bl = \case + NVar Var {..} -> + BL.lookup _varIndex bl ^. binderType + NIdt Ident {..} -> + fromJust (HashMap.lookup _identSymbol (tab ^. infoIdentifiers)) ^. identifierType + NCst Constant {..} -> + case _constantValue of + ConstInteger {} -> mkTypeInteger' + ConstString {} -> mkTypeString' + NApp App {..} -> + let lty = Info.getNodeType _appLeft + rty = Info.getNodeType _appRight + in case lty of + NPi Pi {..} + | rty == _piBinder ^. binderType -> + _piBody + _ -> + error "incorrect type information (application)" + NBlt BuiltinApp {..} -> + case _builtinAppOp of + OpIntAdd -> mkTypeInteger' + OpIntSub -> mkTypeInteger' + OpIntMul -> mkTypeInteger' + OpIntDiv -> mkTypeInteger' + OpIntMod -> mkTypeInteger' + OpIntLt -> mkTypeBool' + OpIntLe -> mkTypeBool' + OpEq -> mkTypeBool' + OpShow -> mkTypeString' + OpStrConcat -> mkTypeString' + OpStrToInt -> mkTypeInteger' + OpTrace -> case _builtinAppArgs of + [_, arg2] -> Info.getNodeType arg2 + _ -> error "incorrect trace builtin application" + OpFail -> mkDynamic' + NCtr Constr {..} -> + let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors) + ii = fromJust $ HashMap.lookup (ci ^. constructorInductive) (tab ^. infoInductives) + in case ii ^. inductiveBuiltin of + Just BuiltinBool -> + mkTypeBool' + _ -> + mkTypeConstr' (ci ^. constructorInductive) (take (length (ii ^. inductiveParams)) _constrArgs) + NLam Lambda {..} -> + mkPi' (_lambdaBinder ^. binderType) (Info.getNodeType _lambdaBody) + NLet Let {..} -> + Info.getNodeType _letBody + NRec LetRec {..} -> + Info.getNodeType _letRecBody + NCase Case {..} -> case _caseDefault of + Just nd -> Info.getNodeType nd + Nothing -> case _caseBranches of + CaseBranch {..} : _ -> + Info.getNodeType _caseBranchBody + [] -> error "case with no branches" + NMatch Match {} -> + error "match unsupported" + NPi Pi {} -> + mkUniv' 0 + NUniv Univ {..} -> + mkUniv' (_univLevel + 1) + NTyp TypeConstr {} -> + mkUniv' 0 + NPrim TypePrim {} -> + mkUniv' 0 + NDyn Dynamic {} -> + mkUniv' 0 + Closure {} -> + impossible + +computeTypeInfo :: InfoTable -> InfoTable +computeTypeInfo tab = mapT (const (computeNodeTypeInfo tab)) tab diff --git a/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs b/src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs new file mode 100644 index 000000000..3e2638e72 --- /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 diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs index 48e54744a..f4b2ef0ec 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/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs index 07d3db9a0..fa593e08f 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 ef4df4e0d..3a7ec41fe 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -542,7 +542,55 @@ instrReturn = "ret" instrBr :: (IsString s) => s instrBr = "br" -juvixFunctionT :: (IsString s) => s +gebAbsurd :: IsString s => s +gebAbsurd = "absurd" + +gebUnit :: IsString s => s +gebUnit = "unit" + +gebLeft :: IsString s => s +gebLeft = "left" + +gebRight :: IsString s => s +gebRight = "right" + +gebCase :: IsString s => s +gebCase = "case-on" + +gebPair :: IsString s => s +gebPair = "pair" + +gebFst :: IsString s => s +gebFst = "fst" + +gebSnd :: IsString s => s +gebSnd = "snd" + +gebLamb :: IsString s => s +gebLamb = "lamb" + +gebApp :: IsString s => s +gebApp = "app" + +gebVar :: IsString s => s +gebVar = "index" + +gebInitial :: IsString s => s +gebInitial = "so0" + +gebTerminal :: IsString s => s +gebTerminal = "so1" + +gebProd :: IsString s => s +gebProd = "prod" + +gebCoprod :: IsString s => s +gebCoprod = "coprod" + +gebHom :: IsString s => s +gebHom = "hom" + +juvixFunctionT :: IsString s => s juvixFunctionT = "juvix_function_t" juvixDotOrg :: (IsString s) => s diff --git a/tests/Geb/positive/Core/out/test001.out b/tests/Geb/positive/Core/out/test001.out new file mode 100644 index 000000000..f3c260ef6 --- /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 000000000..a0a32923d --- /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 000000000..a0a32923d --- /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 000000000..a0a32923d --- /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 new file mode 100644 index 000000000..deb183aae --- /dev/null +++ b/tests/Geb/positive/Core/test001.jvc @@ -0,0 +1,2 @@ + +(\(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 new file mode 100644 index 000000000..1ff1c338d --- /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 } }) false (Just true) diff --git a/tests/Geb/positive/Core/test003.jvc b/tests/Geb/positive/Core/test003.jvc new file mode 100644 index 000000000..d7e277178 --- /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 000000000..0281a995f --- /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))