Skip to content

Commit

Permalink
Chain prelude evaluation so that primitives can depend on each other (#…
Browse files Browse the repository at this point in the history
…94)

This PR allows evaluating a second prelude (like the one in
`inferno-ml`) in an environment that already has the first prelude (the
core/builtin one), so that the second prelude can use ops and primitives
defined in the first one.

It creates a new `Prelude` type (that subsumes the type alias
`ModuleMap`) and refactors existing code to use it.
  • Loading branch information
siddharth-krishna authored Nov 8, 2023
1 parent db87eac commit 3e90036
Show file tree
Hide file tree
Showing 25 changed files with 255 additions and 263 deletions.
3 changes: 3 additions & 0 deletions inferno-core/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
# Revision History for inferno-core
*Note*: we use https://pvp.haskell.org/ (MAJOR.MAJOR.MINOR.PATCH)

## 0.9.0.0 -- 2023-11-07
* Breaking change: Chain prelude evaluation. New Prelude type. Interpreter API changes slightly.

## 0.8.2.0 -- 2023-11-02
* Add median

Expand Down
4 changes: 2 additions & 2 deletions inferno-core/app/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ module Main where
import qualified Data.Map as Map
import qualified Data.Text.IO as Text
import Inferno.Core (Interpreter (..), mkInferno)
import Inferno.Module.Prelude (builtinModules)
import Inferno.Module.Prelude (builtinPrelude)
import Inferno.Utils.Prettyprinter (showPretty)
import System.Environment (getArgs)
import System.Exit (exitFailure)
Expand All @@ -17,7 +17,7 @@ main = do
file <- head <$> getArgs
src <- Text.readFile file
Interpreter {evalExpr, defaultEnv, parseAndInferTypeReps} <-
mkInferno builtinModules [] :: IO (Interpreter IO ())
mkInferno builtinPrelude [] :: IO (Interpreter IO ())
case parseAndInferTypeReps src of
Left err -> do
hPutStrLn stderr $ show err
Expand Down
4 changes: 1 addition & 3 deletions inferno-core/inferno-core.cabal
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
cabal-version: 2.4
name: inferno-core
version: 0.8.2.0
version: 0.9.0.0
synopsis: A statically-typed functional scripting language
description: Parser, type inference, and interpreter for a statically-typed functional scripting language
category: DSL,Scripting
Expand Down Expand Up @@ -38,7 +38,6 @@ library
, Inferno.Parse.Commented
, Inferno.Parse.Error
, Inferno.Instances.Arbitrary
, Inferno.Utils.QQ.Script
, Inferno.Utils.QQ.Module
other-modules:
Inferno.Infer.Error
Expand All @@ -61,7 +60,6 @@ library
, inferno-vc >= 0.3.0 && < 0.4
, inferno-types >= 0.3.0 && < 0.4
, megaparsec >= 9.2.1 && < 9.3
, memory >= 0.18.0 && < 0.19
, mtl >= 2.2.2 && < 2.3
, parser-combinators >= 1.3.0 && < 1.4
, picosat >= 0.1.6 && < 0.2
Expand Down
18 changes: 9 additions & 9 deletions inferno-core/src/Inferno/Core.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE ScopedTypeVariables #-}
Expand All @@ -18,9 +19,8 @@ import Inferno.Eval.Error (EvalError)
import Inferno.Infer (TypeError, inferExpr, inferTypeReps)
import Inferno.Infer.Error (Location)
import Inferno.Infer.Pinned (pinExpr)
import Inferno.Module (Module (..))
import Inferno.Module (Module (..), Prelude (..), baseOpsTable, moduleOpsTables, preludeNameToTypeMap, preludePinMap, preludeTermEnv)
import Inferno.Module.Builtin (builtinModule)
import Inferno.Module.Prelude (ModuleMap, baseOpsTable, builtinModulesOpsTable, builtinModulesPinMap, builtinModulesTerms, preludeNameToTypeMap)
import Inferno.Parse (InfernoParsingError, parseExpr)
import Inferno.Types.Syntax (Comment, CustomType, Expr (App, TypeRep), ExtIdent, ModuleName, Namespace, SourcePos, TypeClass, TypeMetadata, collectArrs)
import Inferno.Types.Type (ImplType (ImplType), TCScheme (ForallTC))
Expand Down Expand Up @@ -71,11 +71,11 @@ data Interpreter m c = Interpreter
Set.Set TypeClass
}

mkInferno :: forall m c. (MonadThrow m, MonadCatch m, MonadFix m, Eq c, Pretty c) => ModuleMap m c -> [CustomType] -> m (Interpreter m c)
mkInferno prelude customTypes = do
mkInferno :: forall m c. (MonadThrow m, MonadCatch m, MonadFix m, Eq c, Pretty c) => Prelude m c -> [CustomType] -> m (Interpreter m c)
mkInferno prelude@(Prelude {moduleMap}) customTypes = do
-- We pre-compute envs that only depend on the prelude so that they can be
-- shared among evaluations of different scripts
(preludeIdentEnv, preludePinnedEnv) <- runImplEnvM Map.empty $ builtinModulesTerms prelude
(preludeIdentEnv, preludePinnedEnv) <- runImplEnvM Map.empty $ preludeTermEnv prelude
return $
Interpreter
{ evalExpr = runEvalM,
Expand All @@ -89,16 +89,16 @@ mkInferno prelude customTypes = do
where
parseAndInfer src =
-- parse
case parseExpr (baseOpsTable prelude) (builtinModulesOpsTable prelude) customTypes src of
case parseExpr (baseOpsTable prelude) (moduleOpsTables prelude) customTypes src of
Left err ->
Left $ ParseError err
Right (ast, comments) ->
-- pin free variables to builtin prelude function hashes
case pinExpr (builtinModulesPinMap prelude) ast of
case pinExpr (preludePinMap prelude) ast of
Left err -> Left $ PinError err
Right pinnedAST ->
-- typecheck
case inferExpr prelude pinnedAST of
case inferExpr moduleMap pinnedAST of
Left err -> Left $ InferenceError err
Right (pinnedAST', sch, tyMap) ->
Right (pinnedAST', sch, tyMap, comments)
Expand All @@ -120,7 +120,7 @@ mkInferno prelude customTypes = do
[TypeRep (initialPos "dummy") ty | ty <- runtimeReps]
in Right finalAst

typeClasses = Set.unions $ moduleTypeClasses builtinModule : [cls | Module {moduleTypeClasses = cls} <- Map.elems prelude]
typeClasses = Set.unions $ moduleTypeClasses builtinModule : [cls | Module {moduleTypeClasses = cls} <- Map.elems moduleMap]

-- TODO at some point: instead of evaluating closure and putting into pinned env,
-- add closure into the expression being evaluated by using let bindings.
Expand Down
3 changes: 2 additions & 1 deletion inferno-core/src/Inferno/Instances/Arbitrary.hs
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ import qualified Data.Set as Set
import qualified Data.Text as Text (Text, all, null, pack)
import GHC.Generics (Generic (..), Rep)
import Inferno.Infer.Env (closeOver)
import qualified Inferno.Module as Prelude (baseOpsTable)
import qualified Inferno.Module.Prelude as Prelude
import qualified Inferno.Types.Module as Module (Module)
import Inferno.Types.Syntax
Expand Down Expand Up @@ -102,7 +103,7 @@ instance (Generic a, GArbitrary ga, ga ~ Rep a) => Arbitrary (GenericArbitrary a
arbitrary = GenericArbitrary <$> genericArbitrary

baseOpsTable :: OpsTable
baseOpsTable = Prelude.baseOpsTable @IO @() $ Prelude.builtinModules @IO @()
baseOpsTable = Prelude.baseOpsTable @() $ Prelude.builtinPrelude @IO @()

-- | Arbitrary and ToADTArbitrary instances for Inferno.Types.Module
deriving instance Arbitrary objs => ToADTArbitrary (Module.Module objs)
Expand Down
110 changes: 89 additions & 21 deletions inferno-core/src/Inferno/Module.hs
Original file line number Diff line number Diff line change
@@ -1,15 +1,24 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TemplateHaskell #-}

module Inferno.Module
( Module (..),
PinnedModule,
Prelude (..),
BuiltinModuleHash (..),
BuiltinFunHash (..),
BuiltinEnumHash (..),
baseOpsTable,
moduleOpsTables,
preludePinMap,
preludeTermEnv,
preludeNameToTypeMap,
buildPinnedQQModules,
combineTermEnvs,
emptyPrelude,
buildInitPrelude,
pinnedModuleNameToHash,
pinnedModuleHashToTy,
pinnedModuleTerms,
Expand All @@ -29,6 +38,7 @@ import Inferno.Infer (inferExpr)
import Inferno.Infer.Env (Namespace (..), TypeMetadata (..))
import Inferno.Infer.Pinned (pinExpr)
import qualified Inferno.Infer.Pinned as Pinned
import Inferno.Module.Builtin (builtinModule)
import Inferno.Module.Cast (ToValue (..))
import Inferno.Parse (OpsTable, TopLevelDefn (..))
import Inferno.Types.Module
Expand Down Expand Up @@ -62,36 +72,94 @@ import Inferno.Types.VersionControl (Pinned (..), VCObjectHash, pinnedToMaybe, v
import Prettyprinter (Pretty)
import Text.Megaparsec (SourcePos)

data Prelude m c = Prelude
{ moduleMap :: Map.Map ModuleName (PinnedModule (ImplEnvM m c (TermEnv VCObjectHash c (ImplEnvM m c)))),
pinnedModuleMap :: Map.Map (Scoped ModuleName) (Map.Map Namespace (Pinned VCObjectHash))
-- TODO is pinnedModuleMap not the same as the first component of the PinnedModule of moduleMap above?
}

emptyPrelude :: Prelude m c
emptyPrelude = Prelude mempty mempty

baseOpsTable :: (Pretty c, Eq c) => Prelude m c -> OpsTable
baseOpsTable Prelude {moduleMap} =
case Map.lookup "Base" moduleMap of
Just (Module {moduleOpsTable = ops, moduleName = modNm}) ->
-- TODO is 'Scope modNm' below correct? or should it be the name of the module '_' below?
IntMap.unionWith (<>) ops (IntMap.map (\xs -> [(fix, Scope modNm, op) | (fix, _, op) <- xs]) ops)
Nothing -> mempty

moduleOpsTables :: (Pretty c, Eq c) => Prelude m c -> Map.Map ModuleName OpsTable
moduleOpsTables Prelude {moduleMap} = Map.map (\Module {moduleOpsTable} -> moduleOpsTable) moduleMap

-- | Map from Module.name to the pinned hash for all names in the given prelude.
-- This functions includes the Inferno.Module.Builtin module and also "exports"
-- the Base module so that it can be used without prefix.
preludePinMap :: (MonadThrow m, Pretty c, Eq c) => Prelude m c -> Map.Map (Scoped ModuleName) (Map.Map Namespace (Pinned VCObjectHash))
preludePinMap prelude =
Pinned.openModule "Base" $
Pinned.insertBuiltinModule $
Map.foldrWithKey Pinned.insertHardcodedModule mempty $
Map.map (Map.map Builtin . pinnedModuleNameToHash) $
moduleMap prelude

preludeTermEnv :: (MonadThrow m, Pretty c, Eq c) => Prelude m c -> ImplEnvM m c (TermEnv VCObjectHash c (ImplEnvM m c))
preludeTermEnv = combineTermEnvs . moduleMap

preludeNameToTypeMap :: (MonadThrow m, Pretty c, Eq c) => Prelude m c -> Map.Map (Maybe ModuleName, Namespace) (TypeMetadata TCScheme)
preludeNameToTypeMap prelude =
let unqualifiedN2h = pinnedModuleNameToHash $ modules Map.! "Base"
n2h =
Map.unions $
Map.mapKeys (Nothing,) (pinnedModuleNameToHash builtinModule)
: Map.mapKeys (Nothing,) unqualifiedN2h
: [Map.mapKeys (Just nm,) (pinnedModuleNameToHash m `Map.difference` unqualifiedN2h) | (nm, m) <- Map.toList modules]
h2ty = Map.unions $ pinnedModuleHashToTy builtinModule : [pinnedModuleHashToTy m | m <- Map.elems modules]
in Map.mapMaybe (`Map.lookup` h2ty) n2h
where
modules = moduleMap prelude

combineTermEnvs ::
MonadThrow m =>
Map.Map ModuleName (PinnedModule (ImplEnvM m c (TermEnv VCObjectHash c (ImplEnvM m c)))) ->
ImplEnvM m c (TermEnv VCObjectHash c (ImplEnvM m c))
combineTermEnvs modules = foldM (\env m -> (env <>) <$> pinnedModuleTerms m) mempty $ Map.elems modules

-- | A specialiazation of @buildPinnedQQModules@ below with an empty initial prelude.
-- This is to be used in the QuasiQuoter to build the initial/core Inferno prelude.
-- We can't use @buildPinnedQQModules emptyPrelude@ in the QuasiQuoter because TH
-- doesn't like that.
buildInitPrelude ::
(MonadThrow m, Pretty c) =>
[(ModuleName, OpsTable, [TopLevelDefn (Either (TCScheme, ImplEnvM m c (Value c (ImplEnvM m c))) (Maybe TCScheme, Expr () SourcePos))])] ->
Prelude m c
buildInitPrelude = buildPinnedQQModules emptyPrelude

buildPinnedQQModules ::
(MonadThrow m, Pretty c) =>
Prelude m c ->
[(ModuleName, OpsTable, [TopLevelDefn (Either (TCScheme, ImplEnvM m c (Value c (ImplEnvM m c))) (Maybe TCScheme, Expr () SourcePos))])] ->
Map.Map ModuleName (PinnedModule (ImplEnvM m c (TermEnv VCObjectHash c (ImplEnvM m c))))
buildPinnedQQModules modules =
snd $
foldl'
( \(alreadyPinnedModulesMap, alreadyBuiltModules) (moduleNm, opsTable, sigs) ->
-- first build the new module
let newMod =
buildModule alreadyPinnedModulesMap alreadyBuiltModules sigs $
Module
{ moduleName = moduleNm,
moduleOpsTable = opsTable,
moduleTypeClasses = mempty,
moduleObjects = (Map.singleton (ModuleNamespace moduleNm) $ vcHash $ BuiltinModuleHash moduleNm, mempty, pure mempty)
}
in -- then insert it into the temporary module pin map as well as the final module map
( Pinned.insertHardcodedModule moduleNm (Map.map Builtin $ pinnedModuleNameToHash newMod) alreadyPinnedModulesMap,
Map.insert moduleNm newMod alreadyBuiltModules
)
)
mempty
modules
Prelude m c
buildPinnedQQModules initPrelude modules =
foldl'
( \Prelude {pinnedModuleMap, moduleMap} (moduleNm, opsTable, sigs) ->
-- first build the new module
let newMod =
buildModule pinnedModuleMap moduleMap sigs $
Module
{ moduleName = moduleNm,
moduleOpsTable = opsTable,
moduleTypeClasses = mempty,
moduleObjects = (Map.singleton (ModuleNamespace moduleNm) $ vcHash $ BuiltinModuleHash moduleNm, mempty, pure mempty)
}
in -- then insert it into the temporary module pin map as well as the final module map
Prelude
{ pinnedModuleMap = Pinned.insertHardcodedModule moduleNm (Map.map Builtin $ pinnedModuleNameToHash newMod) pinnedModuleMap,
moduleMap = Map.insert moduleNm newMod moduleMap
}
)
initPrelude
modules
where
buildModule ::
(MonadThrow m, Pretty c) =>
Expand Down
53 changes: 6 additions & 47 deletions inferno-core/src/Inferno/Module/Prelude.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,8 @@ module Inferno.Module.Prelude where

import Control.Monad.Catch (MonadCatch (..), MonadThrow (..))
import Control.Monad.IO.Class (MonadIO)
import qualified Data.IntMap as IntMap
import qualified Data.Map as Map
import Inferno.Eval (TermEnv)
import qualified Inferno.Infer.Pinned as Pinned
import Inferno.Module (Module (..), PinnedModule, combineTermEnvs, pinnedModuleHashToTy, pinnedModuleNameToHash)
import Inferno.Module.Builtin (builtinModule)
import Inferno.Module.Cast (Kind0 (toType), ToValue (toValue))
import Inferno.Module (Prelude)
import Inferno.Module.Cast (Kind0 (toType))
import Inferno.Module.Prelude.Defs
( absFun,
andFun,
Expand Down Expand Up @@ -117,45 +112,9 @@ import Inferno.Module.Prelude.Defs
zeroFun,
zipFun,
)
import Inferno.Parse (OpsTable)
import Inferno.Types.Syntax (ModuleName, Scoped (..))
import Inferno.Types.Type (Namespace, TCScheme, TypeMetadata)
import Inferno.Types.Value (ImplEnvM)
import Inferno.Types.VersionControl (Pinned (..), VCObjectHash)
import Inferno.Utils.QQ.Module (infernoModules)
import Inferno.Utils.QQ.Module (builtinPreludeQuoter)
import Prettyprinter (Pretty)

type ModuleMap m c = Map.Map ModuleName (PinnedModule (ImplEnvM m c (TermEnv VCObjectHash c (ImplEnvM m c))))

baseOpsTable :: forall m c. (MonadThrow m, Pretty c, Eq c) => ModuleMap m c -> OpsTable
baseOpsTable moduleMap =
let Module {moduleOpsTable = ops, moduleName = modNm} = moduleMap Map.! "Base"
in IntMap.unionWith (<>) ops (IntMap.map (\xs -> [(fix, Scope modNm, op) | (fix, _, op) <- xs]) ops)

builtinModulesOpsTable :: forall m c. (MonadThrow m, Pretty c, Eq c) => ModuleMap m c -> Map.Map ModuleName OpsTable
builtinModulesOpsTable = Map.map (\Module {moduleOpsTable} -> moduleOpsTable)

builtinModulesPinMap :: forall m c. (MonadThrow m, Pretty c, Eq c) => ModuleMap m c -> Map.Map (Scoped ModuleName) (Map.Map Namespace (Pinned VCObjectHash))
builtinModulesPinMap moduleMap =
Pinned.openModule "Base" $
Pinned.insertBuiltinModule $
Map.foldrWithKey Pinned.insertHardcodedModule mempty $
Map.map (Map.map Builtin . pinnedModuleNameToHash) moduleMap

builtinModulesTerms :: forall m c. (MonadThrow m, Pretty c, Eq c) => ModuleMap m c -> ImplEnvM m c (TermEnv VCObjectHash c (ImplEnvM m c))
builtinModulesTerms = combineTermEnvs

preludeNameToTypeMap :: forall m c. (MonadThrow m, Pretty c, Eq c) => ModuleMap m c -> Map.Map (Maybe ModuleName, Namespace) (TypeMetadata TCScheme)
preludeNameToTypeMap moduleMap =
let unqualifiedN2h = pinnedModuleNameToHash $ moduleMap Map.! "Base"
n2h =
Map.unions $
Map.mapKeys (Nothing,) (pinnedModuleNameToHash builtinModule)
: Map.mapKeys (Nothing,) unqualifiedN2h
: [Map.mapKeys (Just nm,) (pinnedModuleNameToHash m `Map.difference` unqualifiedN2h) | (nm, m) <- Map.toList moduleMap]
h2ty = Map.unions $ pinnedModuleHashToTy builtinModule : [pinnedModuleHashToTy m | m <- Map.elems moduleMap]
in Map.mapMaybe (`Map.lookup` h2ty) n2h

-- In the definitions below, ###!x### is an anti-quotation to a haskell variable `x` of type `Monad m => (Value m)`
-- This sort of Value is necessary for polymorphic functions such as `map` or `id`
-- The inferno type of this function must be explicitly specified, otherwise a runtime error will occur when typechecking
Expand All @@ -166,9 +125,9 @@ preludeNameToTypeMap moduleMap =
-- as these require an accompanying definition of a typeclass, via the syntax:
-- `define typeclass_name on t1 ... tn;`.

builtinModules :: (MonadIO m, MonadThrow m, MonadCatch m, Pretty c, Eq c) => ModuleMap m c
builtinModules =
[infernoModules|
builtinPrelude :: (MonadIO m, MonadThrow m, MonadCatch m, Pretty c, Eq c) => Prelude m c
builtinPrelude =
[builtinPreludeQuoter|

module Number

Expand Down
Loading

0 comments on commit 3e90036

Please sign in to comment.