diff --git a/app/Commands/Dev/Termination/CallGraph.hs b/app/Commands/Dev/Termination/CallGraph.hs index 308b97636d..2f4077dd2b 100644 --- a/app/Commands/Dev/Termination/CallGraph.hs +++ b/app/Commands/Dev/Termination/CallGraph.hs @@ -4,15 +4,15 @@ import Commands.Base import Commands.Dev.Termination.CallGraph.Options import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Internal.Pretty qualified as Internal -import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context qualified as Internal import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination qualified as Termination +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Internal import Juvix.Compiler.Store.Extra qualified as Stored import Juvix.Prelude.Pretty runCommand :: (Members '[EmbedIO, TaggedLock, App] r) => CallGraphOptions -> Sem r () runCommand CallGraphOptions {..} = do globalOpts <- askGlobalOptions - PipelineResult {..} <- runPipelineTermination _graphInputFile upToInternal + PipelineResult {..} <- runPipelineTermination _graphInputFile upToInternalTyped let mainModule = _pipelineResult ^. Internal.resultModule toAnsiText' :: forall a. (HasAnsiBackend a, HasTextBackend a) => a -> Text toAnsiText' = toAnsiText (not (globalOpts ^. globalNoColors)) diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index dc4e531656..a5320567b3 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -58,7 +58,7 @@ fromInternal i = do } res <- execInfoTableBuilder md - . evalState (i ^. InternalTyped.resultFunctions) + . runReader (i ^. InternalTyped.resultFunctions) . runReader (i ^. InternalTyped.resultIdenTypes) $ do when @@ -95,13 +95,13 @@ fromInternalExpression importTab res exp = do fmap snd . runReader mtab . runInfoTableBuilder (res ^. coreResultModule) - . evalState (res ^. coreResultInternalTypedResult . InternalTyped.resultFunctions) + . runReader (res ^. coreResultInternalTypedResult . InternalTyped.resultFunctions) . runReader (res ^. coreResultInternalTypedResult . InternalTyped.resultIdenTypes) $ fromTopIndex (goExpression exp) goModule :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => Internal.Module -> Sem r () goModule m = do @@ -110,7 +110,7 @@ goModule m = do -- | predefine an inductive definition preInductiveDef :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => Internal.InductiveDef -> Sem r PreInductiveDef preInductiveDef i = do @@ -149,7 +149,7 @@ preInductiveDef i = do goInductiveDef :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => PreInductiveDef -> Sem r () goInductiveDef PreInductiveDef {..} = do @@ -163,7 +163,7 @@ goInductiveDef PreInductiveDef {..} = do goConstructor :: forall r. - (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, NameIdGen] r) => Symbol -> Internal.ConstructorDef -> Sem r ConstructorInfo @@ -228,7 +228,7 @@ goConstructor sym ctor = do goMutualBlock :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => Internal.MutualBlock -> Sem r () goMutualBlock (Internal.MutualBlock m) = preMutual m >>= goMutual @@ -267,7 +267,7 @@ goMutualBlock (Internal.MutualBlock m) = preMutual m >>= goMutual preFunctionDef :: forall r. - (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, NameIdGen] r) => Internal.FunctionDef -> Sem r PreFunctionDef preFunctionDef f = do @@ -336,7 +336,7 @@ preFunctionDef f = do goFunctionDef :: forall r. - (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, NameIdGen] r) => PreFunctionDef -> Sem r () goFunctionDef PreFunctionDef {..} = do @@ -355,21 +355,18 @@ goFunctionDef PreFunctionDef {..} = do let (is, _) = unfoldLambdas node setIdentArgs _preFunSym (map (^. lambdaLhsBinder) is) -strongNormalizeHelper :: (Members '[State InternalTyped.FunctionsTable, NameIdGen] r) => Internal.Expression -> Sem r Internal.Expression -strongNormalizeHelper ty = evalState InternalTyped.iniState (InternalTyped.strongNormalize' ty) - goType :: forall r. - (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, NameIdGen, Reader IndexTable] r) => + (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, NameIdGen, Reader IndexTable] r) => Internal.Expression -> Sem r Type goType ty = do - normTy <- strongNormalizeHelper ty + normTy <- InternalTyped.strongNormalize'' ty squashApps <$> goExpression normTy mkFunBody :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => Type -> -- converted type of the function Internal.FunctionDef -> Sem r Node @@ -381,7 +378,7 @@ mkFunBody ty f = mkBody :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => Type -> -- type of the function Location -> NonEmpty ([Internal.PatternArg], Internal.Expression) -> @@ -468,7 +465,7 @@ mkBody ty loc clauses goCase :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => Internal.Case -> Sem r Node goCase c = do @@ -502,7 +499,7 @@ goCase c = do goLambda :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => Internal.Lambda -> Sem r Node goLambda l = do @@ -511,7 +508,7 @@ goLambda l = do goLet :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => Internal.Let -> Sem r Node goLet l = goClauses (toList (l ^. Internal.letClauses)) @@ -549,7 +546,7 @@ goLet l = goClauses (toList (l ^. Internal.letClauses)) goAxiomInductive :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => Internal.AxiomDef -> Sem r () goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive @@ -612,7 +609,7 @@ fromTopIndex = runReader initIndexTable goAxiomDef :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, NameIdGen] r) => Internal.AxiomDef -> Sem r () goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) @@ -767,7 +764,7 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin) fromPatternArg :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, State IndexTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, State IndexTable, NameIdGen] r) => Internal.PatternArg -> Sem r Pattern fromPatternArg pa = case pa ^. Internal.patternArgName of @@ -851,7 +848,7 @@ fromPatternArg pa = case pa ^. Internal.patternArgName of goPatternArgs :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => Level -> -- the level of the first binder for the matched value Internal.Expression -> [Internal.PatternArg] -> @@ -909,7 +906,7 @@ addPatternVariableNames p lvl vars = goIden :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) => Internal.Iden -> Sem r Node goIden i = do @@ -988,7 +985,7 @@ goIden i = do goExpression :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => Internal.Expression -> Sem r Node goExpression = \case @@ -1008,7 +1005,7 @@ goExpression = \case goFunction :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => ([Internal.FunctionParameter], Internal.Expression) -> Sem r Node goFunction (params, returnTypeExpr) = go params @@ -1031,7 +1028,7 @@ goFunction (params, returnTypeExpr) = go params goSimpleLambda :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => Internal.SimpleLambda -> Sem r Node goSimpleLambda l = do @@ -1043,7 +1040,7 @@ goSimpleLambda l = do goApplication :: forall r. - (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => + (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable, NameIdGen] r) => Internal.Application -> Sem r Node goApplication a = do diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs index cf817de6b1..f0c17477ef 100644 --- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Internal/Data/InfoTable.hs @@ -1,6 +1,7 @@ module Juvix.Compiler.Internal.Data.InfoTable ( module Juvix.Compiler.Store.Internal.Language, computeInternalModule, + computeInternalModuleInfoTable, extendWithReplExpression, lookupConstructor, lookupConstructorArgTypes, @@ -21,9 +22,9 @@ where import Data.Generics.Uniplate.Data import Data.HashMap.Strict qualified as HashMap -import Juvix.Compiler.Internal.Data.CoercionInfo -import Juvix.Compiler.Internal.Data.InstanceInfo import Juvix.Compiler.Internal.Extra +import Juvix.Compiler.Internal.Extra.CoercionInfo +import Juvix.Compiler.Internal.Extra.InstanceInfo import Juvix.Compiler.Internal.Pretty (ppTrace) import Juvix.Compiler.Store.Internal.Data.FunctionsTable import Juvix.Compiler.Store.Internal.Data.TypesTable @@ -80,19 +81,21 @@ letFunctionDefs e = LetFunDef f -> pure f LetMutualBlock (MutualBlockLet fs) -> fs -computeInternalModule :: TypesTable -> FunctionsTable -> Module -> InternalModule -computeInternalModule tysTab funsTab m@Module {..} = +computeInternalModule :: InstanceTable -> CoercionTable -> TypesTable -> FunctionsTable -> Module -> InternalModule +computeInternalModule instTab coeTab tysTab funsTab m@Module {..} = InternalModule { _internalModuleId = _moduleId, _internalModuleName = _moduleName, _internalModuleImports = _moduleBody ^. moduleImports, - _internalModuleInfoTable = computeInfoTable m, + _internalModuleInfoTable = computeInternalModuleInfoTable m, _internalModuleTypesTable = tysTab, - _internalModuleFunctionsTable = funsTab + _internalModuleFunctionsTable = funsTab, + _internalModuleInstanceTable = instTab, + _internalModuleCoercionTable = coeTab } -computeInfoTable :: Module -> InfoTable -computeInfoTable m = InfoTable {..} +computeInternalModuleInfoTable :: Module -> InfoTable +computeInternalModuleInfoTable m = InfoTable {..} where mutuals :: [MutualStatement] mutuals = @@ -168,36 +171,6 @@ computeInfoTable m = InfoTable {..} _axiomInfoDef ^. axiomBuiltin >>= (\b -> Just (BuiltinsAxiom b, _axiomInfoDef ^. axiomName)) - _infoInstances :: InstanceTable - _infoInstances = foldr (flip updateInstanceTable) mempty $ mapMaybe mkInstance (HashMap.elems _infoFunctions) - where - mkInstance :: FunctionInfo -> Maybe InstanceInfo - mkInstance (FunctionInfo {..}) - | _functionInfoInstance = - instanceFromTypedExpression - ( TypedExpression - { _typedType = _functionInfoType, - _typedExpression = ExpressionIden (IdenFunction _functionInfoName) - } - ) - | otherwise = - Nothing - - _infoCoercions :: CoercionTable - _infoCoercions = foldr (flip updateCoercionTable) mempty $ mapMaybe mkCoercion (HashMap.elems _infoFunctions) - where - mkCoercion :: FunctionInfo -> Maybe CoercionInfo - mkCoercion (FunctionInfo {..}) - | _functionInfoCoercion = - coercionFromTypedExpression - ( TypedExpression - { _typedType = _functionInfoType, - _typedExpression = ExpressionIden (IdenFunction _functionInfoName) - } - ) - | otherwise = - Nothing - ss :: [MutualBlock] ss = m ^. moduleBody . moduleStatements diff --git a/src/Juvix/Compiler/Internal/Data/CoercionInfo.hs b/src/Juvix/Compiler/Internal/Extra/CoercionInfo.hs similarity index 59% rename from src/Juvix/Compiler/Internal/Data/CoercionInfo.hs rename to src/Juvix/Compiler/Internal/Extra/CoercionInfo.hs index 79fb5744c8..4210eb707e 100644 --- a/src/Juvix/Compiler/Internal/Data/CoercionInfo.hs +++ b/src/Juvix/Compiler/Internal/Extra/CoercionInfo.hs @@ -1,50 +1,18 @@ -module Juvix.Compiler.Internal.Data.CoercionInfo where +module Juvix.Compiler.Internal.Extra.CoercionInfo + ( module Juvix.Compiler.Store.Internal.Data.CoercionInfo, + module Juvix.Compiler.Internal.Extra.CoercionInfo, + ) +where import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet import Data.List qualified as List -import Juvix.Compiler.Internal.Data.InstanceInfo import Juvix.Compiler.Internal.Extra.Base +import Juvix.Compiler.Internal.Extra.InstanceInfo import Juvix.Compiler.Internal.Language -import Juvix.Extra.Serialize +import Juvix.Compiler.Store.Internal.Data.CoercionInfo import Juvix.Prelude -data CoercionInfo = CoercionInfo - { _coercionInfoInductive :: Name, - _coercionInfoParams :: [InstanceParam], - _coercionInfoTarget :: InstanceApp, - _coercionInfoResult :: Expression, - _coercionInfoArgs :: [FunctionParameter] - } - deriving stock (Eq, Generic) - -instance Hashable CoercionInfo where - hashWithSalt salt CoercionInfo {..} = hashWithSalt salt _coercionInfoResult - -instance Serialize CoercionInfo - --- | Maps trait names to available coercions -newtype CoercionTable = CoercionTable - { _coercionTableMap :: HashMap InductiveName [CoercionInfo] - } - deriving stock (Eq, Generic) - -instance Serialize CoercionTable - -makeLenses ''CoercionInfo -makeLenses ''CoercionTable - -instance Semigroup CoercionTable where - t1 <> t2 = - CoercionTable $ - HashMap.unionWith combine (t1 ^. coercionTableMap) (t2 ^. coercionTableMap) - where - combine :: [CoercionInfo] -> [CoercionInfo] -> [CoercionInfo] - combine ii1 ii2 = nubHashable (ii1 ++ ii2) - -instance Monoid CoercionTable where - mempty = CoercionTable mempty - updateCoercionTable :: CoercionTable -> CoercionInfo -> CoercionTable updateCoercionTable tab ci@CoercionInfo {..} = over coercionTableMap (HashMap.alter go _coercionInfoInductive) tab diff --git a/src/Juvix/Compiler/Internal/Data/InstanceInfo.hs b/src/Juvix/Compiler/Internal/Extra/InstanceInfo.hs similarity index 66% rename from src/Juvix/Compiler/Internal/Data/InstanceInfo.hs rename to src/Juvix/Compiler/Internal/Extra/InstanceInfo.hs index 83d92589c6..884cb09876 100644 --- a/src/Juvix/Compiler/Internal/Data/InstanceInfo.hs +++ b/src/Juvix/Compiler/Internal/Extra/InstanceInfo.hs @@ -1,79 +1,16 @@ -module Juvix.Compiler.Internal.Data.InstanceInfo where +module Juvix.Compiler.Internal.Extra.InstanceInfo + ( module Juvix.Compiler.Store.Internal.Data.InstanceInfo, + module Juvix.Compiler.Internal.Extra.InstanceInfo, + ) +where import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet import Juvix.Compiler.Internal.Extra.Base import Juvix.Compiler.Internal.Language -import Juvix.Extra.Serialize +import Juvix.Compiler.Store.Internal.Data.InstanceInfo import Juvix.Prelude -data InstanceParam - = InstanceParamVar VarName - | InstanceParamApp InstanceApp - | InstanceParamFun InstanceFun - | InstanceParamHole Hole - | InstanceParamMeta VarName - deriving stock (Eq, Generic) - -instance Serialize InstanceParam - -data InstanceApp = InstanceApp - { _instanceAppHead :: Name, - _instanceAppArgs :: [InstanceParam], - -- | The original expression from which this InstanceApp was created - _instanceAppExpression :: Expression - } - deriving stock (Eq, Generic) - -instance Serialize InstanceApp - -data InstanceFun = InstanceFun - { _instanceFunLeft :: InstanceParam, - _instanceFunRight :: InstanceParam, - -- | The original expression from which this InstanceFun was created - _instanceFunExpression :: Expression - } - deriving stock (Eq, Generic) - -instance Serialize InstanceFun - -data InstanceInfo = InstanceInfo - { _instanceInfoInductive :: InductiveName, - _instanceInfoParams :: [InstanceParam], - _instanceInfoResult :: Expression, - _instanceInfoArgs :: [FunctionParameter] - } - deriving stock (Eq, Generic) - -instance Hashable InstanceInfo where - hashWithSalt salt InstanceInfo {..} = hashWithSalt salt _instanceInfoResult - -instance Serialize InstanceInfo - --- | Maps trait names to available instances -newtype InstanceTable = InstanceTable - { _instanceTableMap :: HashMap InductiveName [InstanceInfo] - } - deriving stock (Eq, Generic) - -instance Serialize InstanceTable - -makeLenses ''InstanceApp -makeLenses ''InstanceFun -makeLenses ''InstanceInfo -makeLenses ''InstanceTable - -instance Semigroup InstanceTable where - t1 <> t2 = - InstanceTable $ - HashMap.unionWith combine (t1 ^. instanceTableMap) (t2 ^. instanceTableMap) - where - combine :: [InstanceInfo] -> [InstanceInfo] -> [InstanceInfo] - combine ii1 ii2 = nubHashable (ii1 ++ ii2) - -instance Monoid InstanceTable where - mempty = InstanceTable mempty - updateInstanceTable :: InstanceTable -> InstanceInfo -> InstanceTable updateInstanceTable tab ii@InstanceInfo {..} = over instanceTableMap (HashMap.alter go _instanceInfoInductive) tab diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 2300de6e26..301a44199a 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -6,7 +6,6 @@ module Juvix.Compiler.Internal.Pretty.Base where import Data.HashMap.Strict qualified as HashMap -import Juvix.Compiler.Internal.Data.InstanceInfo (instanceInfoResult, instanceTableMap) import Juvix.Compiler.Internal.Data.LocalVars import Juvix.Compiler.Internal.Data.NameDependencyInfo import Juvix.Compiler.Internal.Data.TypedHole @@ -366,7 +365,6 @@ instance PrettyCode InfoTable where inds <- ppCode (HashMap.keys (tbl ^. infoInductives)) constrs <- ppCode (HashMap.keys (tbl ^. infoConstructors)) funs <- ppCode (HashMap.keys (tbl ^. infoFunctions)) - insts <- ppCode $ map (map (^. instanceInfoResult)) $ HashMap.elems (tbl ^. infoInstances . instanceTableMap) return $ header "InfoTable" <> "\n=========" @@ -376,8 +374,6 @@ instance PrettyCode InfoTable where <> constrs <> header "\nFunctions: " <> funs - <> header "\nInstances: " - <> insts ppPostExpression :: (PrettyCode a, HasAtomicity a, Member (Reader Options) r) => diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 04548cd4c5..10d79bdb49 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -20,7 +20,6 @@ import Juvix.Compiler.Concrete.Gen qualified as Gen import Juvix.Compiler.Concrete.Language qualified as Concrete import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error -import Juvix.Compiler.Internal.Data.InfoTable qualified as Internal import Juvix.Compiler.Internal.Data.NameDependencyInfo qualified as Internal import Juvix.Compiler.Internal.Extra (mkLetClauses) import Juvix.Compiler.Internal.Extra qualified as Internal @@ -79,7 +78,6 @@ fromConcrete _resultScoper = do . runReader @DefaultArgsStack mempty . evalBuiltins (BuiltinsState blts) $ goTopModule m - let _resultInternalModule = Internal.computeInternalModule mempty mempty _resultModule return InternalResult {..} where m = _resultScoper ^. Scoper.resultModule diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs index 1a4e09876f..b21e3088e6 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete/Data/Context.hs @@ -11,7 +11,6 @@ import Juvix.Prelude data InternalResult = InternalResult { _resultScoper :: Concrete.ScoperResult, - _resultInternalModule :: InternalModule, _resultModule :: Module } diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs index 2a96d6c713..6f75820379 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs @@ -7,6 +7,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal where import Juvix.Compiler.Concrete.Data.Highlight.Input +import Juvix.Compiler.Internal.Data.InfoTable import Juvix.Compiler.Internal.Data.LocalVars import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context as Internal @@ -27,8 +28,7 @@ typeCheckExpressionType :: typeCheckExpressionType exp = do -- TODO: refactor: modules outside of REPL should not refer to Artifacts table <- extendedTableReplArtifacts exp - runTypesTableArtifacts - . runFunctionsTableArtifacts + runResultBuilderArtifacts . runBuiltinsArtifacts . runNameIdGenArtifacts . ignoreHighlightBuilder @@ -55,28 +55,38 @@ typeCheckingNew :: Sem (Termination ': r) InternalResult -> Sem r InternalTypedResult typeCheckingNew a = do - (termin, (res, (idens, (funs, r)))) <- runTermination iniTerminationState $ do + (termin, (res, (bst, checkedModule))) <- runTermination iniTerminationState $ do res <- a itab <- getInternalModuleTable <$> ask - let md :: InternalModule - md = res ^. Internal.resultInternalModule - itab' :: InternalModuleTable - itab' = insertInternalModule itab md - table :: InfoTable - table = computeCombinedInfoTable itab' + let table :: InfoTable + table = computeCombinedInfoTable itab <> computeInternalModuleInfoTable (res ^. Internal.resultModule) + importCtx = + ImportContext + { _importContextTypesTable = computeTypesTable itab, + _importContextFunctionsTable = computeFunctionsTable itab, + _importContextInstances = computeInstanceTable itab, + _importContextCoercions = computeCoercionTable itab + } fmap (res,) - . runState (computeTypesTable itab') - . runState (computeFunctionsTable itab') . runReader table + . runResultBuilder importCtx . mapError (JuvixError @TypeCheckerError) - $ checkTable >> checkModule (res ^. Internal.resultModule) - let md = computeInternalModule idens funs r + $ checkTopModule (res ^. Internal.resultModule) + let md = + computeInternalModule + (bst ^. resultBuilderStateInstanceTable) + (bst ^. resultBuilderStateCoercionTable) + (bst ^. resultBuilderStateTypesTable) + (bst ^. resultBuilderStateFunctionsTable) + checkedModule return InternalTypedResult { _resultInternal = res, - _resultModule = r, + _resultModule = checkedModule, _resultInternalModule = md, _resultTermination = termin, - _resultIdenTypes = idens, - _resultFunctions = funs + _resultIdenTypes = bst ^. resultBuilderStateCombinedTypesTable, + _resultFunctions = bst ^. resultBuilderStateCombinedFunctionsTable, + _resultInstances = bst ^. resultBuilderStateCombinedInstanceTable, + _resultCoercions = bst ^. resultBuilderStateCombinedCoercionTable } diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs index dd91ec44d0..807fb42ed5 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -156,7 +156,6 @@ checkStrictlyPositiveOccurrences p = do ExpressionIden (IdenInductive ty') -> do when (inside && name == ty') (throwNegativePositonError expr) indInfo' <- lookupInductive ty' - {- We now need to know whether `name` negatively occurs at `indTy'` or not. The way to know is by checking that the type ty' preserves the positivity condition, i.e., its type parameters are diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking.hs index 493778aa57..a1a39f28ab 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking.hs @@ -2,13 +2,19 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew, module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference, module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context, + module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.ResultBuilder, module Juvix.Compiler.Store.Internal.Data.FunctionsTable, module Juvix.Compiler.Store.Internal.Data.TypesTable, + module Juvix.Compiler.Store.Internal.Data.InstanceInfo, + module Juvix.Compiler.Store.Internal.Data.CoercionInfo, ) where import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.ResultBuilder +import Juvix.Compiler.Store.Internal.Data.CoercionInfo import Juvix.Compiler.Store.Internal.Data.FunctionsTable +import Juvix.Compiler.Store.Internal.Data.InstanceInfo import Juvix.Compiler.Store.Internal.Data.TypesTable diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index fb436f9156..d016e3cb0b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -1,8 +1,6 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error, - checkModule, - checkTable, - checkImport, + checkTopModule, withEmptyInsertedArgsStack, inferExpression, ) @@ -14,18 +12,19 @@ import Data.List.NonEmpty qualified as NonEmpty import Juvix.Compiler.Builtins.Error (NotDefined (..)) import Juvix.Compiler.Concrete.Data.Highlight import Juvix.Compiler.Internal.Data.Cast -import Juvix.Compiler.Internal.Data.CoercionInfo -import Juvix.Compiler.Internal.Data.InstanceInfo import Juvix.Compiler.Internal.Data.LocalVars import Juvix.Compiler.Internal.Data.TypedHole import Juvix.Compiler.Internal.Extra hiding (freshHole) import Juvix.Compiler.Internal.Extra qualified as Extra +import Juvix.Compiler.Internal.Extra.CoercionInfo +import Juvix.Compiler.Internal.Extra.InstanceInfo import Juvix.Compiler.Internal.Pretty import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (Termination) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.ResultBuilder import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Traits.Resolver import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Traits.Termination @@ -104,29 +103,38 @@ instance HasExpressions AppBuilderArg where _appBuilderArgIsDefault } -registerConstructor :: (Members '[HighlightBuilder, State TypesTable, Reader InfoTable] r) => ConstructorDef -> Sem r () +registerConstructor :: (Members '[HighlightBuilder, Reader InfoTable, ResultBuilder] r) => ConstructorDef -> Sem r () registerConstructor ctr = do ty <- lookupConstructorType (ctr ^. inductiveConstructorName) registerNameIdType (ctr ^. inductiveConstructorName . nameId) ty -registerNameIdType :: (Members '[HighlightBuilder, State TypesTable, Reader InfoTable] r) => NameId -> Expression -> Sem r () +registerNameIdType :: (Members '[HighlightBuilder, ResultBuilder] r) => NameId -> Expression -> Sem r () registerNameIdType uid ty = do - modify (over typesTable (HashMap.insert uid ty)) + addIdenType uid ty modify (over (highlightTypes . typesTable) (HashMap.insert uid ty)) -checkTable :: - (Members '[Reader InfoTable, Error TypeCheckerError] r) => +checkCoercionCycles :: + (Members '[ResultBuilder, Error TypeCheckerError] r) => Sem r () -checkTable = do - tab <- ask - let s = toList $ cyclicCoercions (tab ^. infoCoercions) +checkCoercionCycles = do + ctab <- getCombinedCoercionTable + let s = toList $ cyclicCoercions ctab whenJust (nonEmpty s) $ throw . ErrCoercionCycles . CoercionCycles +checkTopModule :: + (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination] r) => + Module -> + Sem r Module +checkTopModule md = do + checkCoercionCycles + md' <- checkModule md + return md' + checkModule :: - (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Termination] r) => + (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination] r) => Module -> Sem r Module checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do @@ -143,7 +151,7 @@ checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do } checkModuleBody :: - (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => ModuleBody -> Sem r ModuleBody checkModuleBody ModuleBody {..} = do @@ -159,14 +167,14 @@ checkImport :: Import -> Sem r Import checkImport = return checkMutualBlock :: - (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock checkMutualBlock s = runReader emptyLocalVars (checkTopMutualBlock s) checkInductiveDef :: forall r. - (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) => + (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, State NegativeTypeParameters, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) => InductiveDef -> Sem r InductiveDef checkInductiveDef InductiveDef {..} = runInferenceDef $ do @@ -225,7 +233,7 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do ) checkTopMutualBlock :: - (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock checkTopMutualBlock (MutualBlock ds) = @@ -233,7 +241,7 @@ checkTopMutualBlock (MutualBlock ds) = resolveCastHoles :: forall a r. - (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, State TypesTable, Termination, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Reader InsertedArgsStack] r) => Sem (Output CastHole ': r) a -> Sem r a resolveCastHoles s = do @@ -262,7 +270,7 @@ resolveCastHoles s = do getNatTy = mkBuiltinInductive BuiltinNat checkMutualStatement :: - (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualStatement -> Sem r MutualStatement checkMutualStatement = \case @@ -290,7 +298,7 @@ unfoldFunType' e = do checkFunctionDef :: forall r. - (Members '[Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => FunctionDef -> Sem r FunctionDef checkFunctionDef FunctionDef {..} = do @@ -338,7 +346,7 @@ checkFunctionDef FunctionDef {..} = do withLocalTypeMaybe (p ^. paramName) (p ^. paramType) (go rest) checkIsType :: - (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, State TypesTable, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => Interval -> Expression -> Sem r Expression @@ -346,7 +354,7 @@ checkIsType = checkExpression . smallUniverseE checkDefType :: forall r. - (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, State TypesTable, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Sem r Expression checkDefType ty = checkIsType loc ty @@ -355,30 +363,33 @@ checkDefType ty = checkIsType loc ty checkInstanceType :: forall r. - (Members '[Error TypeCheckerError, Reader InfoTable, Inference, NameIdGen] r) => + (Members '[Error TypeCheckerError, Reader InfoTable, Inference, NameIdGen, ResultBuilder] r) => FunctionDef -> Sem r () -checkInstanceType FunctionDef {..} = case mi of - Just ii@InstanceInfo {..} -> do - tab <- ask - unless (isTrait tab _instanceInfoInductive) $ - throw (ErrTargetNotATrait (TargetNotATrait _funDefType)) - is <- subsumingInstances (tab ^. infoInstances) ii - unless (null is) $ - throw (ErrSubsumedInstance (SubsumedInstance ii is (getLoc _funDefName))) - let metaVars = HashSet.fromList $ mapMaybe (^. paramName) _instanceInfoArgs - mapM_ (checkArg tab metaVars ii) _instanceInfoArgs - Nothing -> - throw (ErrInvalidInstanceType (InvalidInstanceType _funDefType)) +checkInstanceType FunctionDef {..} = do + ty <- strongNormalize _funDefType + let mi = + instanceFromTypedExpression + ( TypedExpression + { _typedType = ty, + _typedExpression = ExpressionIden (IdenFunction _funDefName) + } + ) + case mi of + Just ii@InstanceInfo {..} -> do + tab <- ask + unless (isTrait tab _instanceInfoInductive) $ + throw (ErrTargetNotATrait (TargetNotATrait _funDefType)) + itab <- getCombinedInstanceTable + is <- subsumingInstances itab ii + unless (null is) $ + throw (ErrSubsumedInstance (SubsumedInstance ii is (getLoc _funDefName))) + let metaVars = HashSet.fromList $ mapMaybe (^. paramName) _instanceInfoArgs + mapM_ (checkArg tab metaVars ii) _instanceInfoArgs + addInstanceInfo ii + Nothing -> + throw (ErrInvalidInstanceType (InvalidInstanceType _funDefType)) where - mi = - instanceFromTypedExpression - ( TypedExpression - { _typedType = _funDefType, - _typedExpression = ExpressionIden (IdenFunction _funDefName) - } - ) - checkArg :: InfoTable -> HashSet VarName -> InstanceInfo -> FunctionParameter -> Sem r () checkArg tab metaVars ii fp@FunctionParameter {..} = case _paramImplicit of Implicit -> return () @@ -397,28 +408,31 @@ checkInstanceParam tab ty = case traitFromExpression mempty ty of checkCoercionType :: forall r. - (Members '[Error TypeCheckerError, Reader InfoTable, Inference] r) => + (Members '[Error TypeCheckerError, Reader InfoTable, Inference, ResultBuilder] r) => FunctionDef -> Sem r () -checkCoercionType FunctionDef {..} = case mi of - Just CoercionInfo {..} -> do - tab <- ask - unless (isTrait tab _coercionInfoInductive) $ - throw (ErrTargetNotATrait (TargetNotATrait _funDefType)) - unless (isTrait tab (_coercionInfoTarget ^. instanceAppHead)) $ +checkCoercionType FunctionDef {..} = do + ty <- strongNormalize _funDefType + let mi = + coercionFromTypedExpression + ( TypedExpression + { _typedType = ty, + _typedExpression = ExpressionIden (IdenFunction _funDefName) + } + ) + case mi of + Just ci@CoercionInfo {..} -> do + tab <- ask + unless (isTrait tab _coercionInfoInductive) $ + throw (ErrTargetNotATrait (TargetNotATrait _funDefType)) + unless (isTrait tab (_coercionInfoTarget ^. instanceAppHead)) $ + throw (ErrInvalidCoercionType (InvalidCoercionType _funDefType)) + mapM_ checkArg _coercionInfoArgs + addCoercionInfo ci + checkCoercionCycles + Nothing -> throw (ErrInvalidCoercionType (InvalidCoercionType _funDefType)) - mapM_ checkArg _coercionInfoArgs - Nothing -> - throw (ErrInvalidCoercionType (InvalidCoercionType _funDefType)) where - mi = - coercionFromTypedExpression - ( TypedExpression - { _typedType = _funDefType, - _typedExpression = ExpressionIden (IdenFunction _funDefName) - } - ) - checkArg :: FunctionParameter -> Sem r () checkArg fp@FunctionParameter {..} = case _paramImplicit of Implicit -> return () @@ -427,7 +441,7 @@ checkCoercionType FunctionDef {..} = case mi of checkExpression :: forall r. - (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, State TypesTable, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Expression -> Sem r Expression @@ -454,7 +468,7 @@ checkExpression expectedTy e = do resolveInstanceHoles :: forall a r. (HasExpressions a) => - (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Inference, State TypesTable, Termination, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, Reader InsertedArgsStack] r) => Sem (Output TypedHole ': r) a -> Sem r a resolveInstanceHoles s = do @@ -472,12 +486,12 @@ resolveInstanceHoles s = do $ checkExpression _typedHoleType t checkFunctionParameter :: - (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, State TypesTable, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => FunctionParameter -> Sem r FunctionParameter checkFunctionParameter FunctionParameter {..} = do - let ty = _paramType - ty' <- checkIsType (getLoc ty) ty + ty <- checkIsType (getLoc _paramType) _paramType + ty' <- strongNormalize ty when (_paramImplicit == ImplicitInstance) $ do tab <- ask checkInstanceParam tab ty' @@ -489,7 +503,7 @@ checkFunctionParameter FunctionParameter {..} = do } inferExpression :: - (Members '[Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, State TypesTable, Termination, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Reader InsertedArgsStack] r) => -- | type hint Maybe Expression -> Expression -> @@ -504,7 +518,7 @@ lookupVar v = do err = error $ "internal error: could not find var " <> ppTrace v <> " at " <> ppTrace (getLoc v) checkFunctionBody :: - (Members '[Reader LocalVars, Reader InfoTable, NameIdGen, Error TypeCheckerError, Output TypedHole, State TypesTable, State FunctionsTable, Inference, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader LocalVars, Reader InfoTable, NameIdGen, Error TypeCheckerError, Output TypedHole, ResultBuilder, Inference, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Expression -> Sem r Expression @@ -530,7 +544,7 @@ checkFunctionBody expectedTy body = -- | helper function for lambda functions and case branches checkClause :: forall r. - (Members '[Reader InfoTable, State FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, State TypesTable, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => Interval -> -- | Type Expression -> @@ -673,7 +687,7 @@ addPatternVar v ty argName = do checkPattern :: forall r. - (Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference, NameIdGen, State FunctionsTable] r) => + (Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference, NameIdGen, ResultBuilder] r) => FunctionParameter -> PatternArg -> Sem r PatternArg @@ -808,7 +822,7 @@ checkPattern = go inferExpression' :: forall r. - (Members '[Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression @@ -817,7 +831,7 @@ inferExpression' = holesHelper -- | Checks anything but an Application. Does not insert holes inferLeftAppExpression :: forall r. - (Members '[Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression @@ -1045,7 +1059,7 @@ inferLeftAppExpression mhint e = case e of return (TypedExpression kind (ExpressionIden i)) -- | The hint is used for trailing holes only -holesHelper :: forall r. (Members '[Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression +holesHelper :: forall r. (Members '[Reader InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression holesHelper mhint expr = do let (f, args) = unfoldExpressionApp expr hint @@ -1388,7 +1402,7 @@ holesHelper mhint expr = do return (head <$> nonEmpty (b ^. appBuilderArgs)) viewInductiveApp :: - (Members '[Error TypeCheckerError, Inference, State FunctionsTable] r) => + (Members '[Error TypeCheckerError, Inference, ResultBuilder] r) => Expression -> Sem r (Either Hole (InductiveName, [Expression])) viewInductiveApp ty = do diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs index 34282b68c1..ddd581b236 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Context.hs @@ -10,20 +10,29 @@ import Juvix.Compiler.Internal.Data.InfoTable import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context qualified as Internal import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (TerminationState) +import Juvix.Compiler.Store.Internal.Data.CoercionInfo import Juvix.Compiler.Store.Internal.Data.FunctionsTable +import Juvix.Compiler.Store.Internal.Data.InstanceInfo import Juvix.Compiler.Store.Internal.Data.TypesTable import Juvix.Prelude -type NormalizedTable = HashMap NameId Expression - data InternalTypedResult = InternalTypedResult { _resultInternal :: Internal.InternalResult, _resultModule :: Module, _resultInternalModule :: InternalModule, _resultTermination :: TerminationState, _resultIdenTypes :: TypesTable, - _resultFunctions :: FunctionsTable + _resultFunctions :: FunctionsTable, + _resultInstances :: InstanceTable, + _resultCoercions :: CoercionTable + } + +data ImportContext = ImportContext + { _importContextTypesTable :: TypesTable, + _importContextFunctionsTable :: FunctionsTable, + _importContextInstances :: InstanceTable, + _importContextCoercions :: CoercionTable } -makeLenses ''TypesTable makeLenses ''InternalTypedResult +makeLenses ''ImportContext diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs index e1d2915596..fc0da9cb8a 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs @@ -7,7 +7,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Da matchErrorRight, queryMetavar, registerIdenType, - strongNormalize', + strongNormalize'', iniState, strongNormalize, weakNormalize, @@ -24,6 +24,7 @@ import Juvix.Compiler.Internal.Extra import Juvix.Compiler.Internal.Pretty import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.ResultBuilder import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error import Juvix.Compiler.Store.Internal.Data.FunctionsTable import Juvix.Prelude hiding (fromEither) @@ -130,7 +131,7 @@ queryMetavarFinal h = do Just (ExpressionHole h') -> queryMetavarFinal h' _ -> return m -strongNormalize' :: forall r. (Members '[State FunctionsTable, State InferenceState, NameIdGen] r) => Expression -> Sem r Expression +strongNormalize' :: forall r. (Members '[ResultBuilder, State InferenceState, NameIdGen] r) => Expression -> Sem r Expression strongNormalize' = go where go :: Expression -> Sem r Expression @@ -233,7 +234,7 @@ strongNormalize' = go goIden :: Iden -> Sem r Expression goIden i = case i of IdenFunction f -> do - f' <- askFunctionDef f + f' <- lookupFunctionDef f case f' of Nothing -> return i' Just x -> go x @@ -241,7 +242,7 @@ strongNormalize' = go where i' = ExpressionIden i -weakNormalize' :: forall r. (Members '[State FunctionsTable, State InferenceState, NameIdGen] r) => Expression -> Sem r Expression +weakNormalize' :: forall r. (Members '[ResultBuilder, State InferenceState, NameIdGen] r) => Expression -> Sem r Expression weakNormalize' = go where go :: Expression -> Sem r Expression @@ -260,7 +261,7 @@ weakNormalize' = go goIden :: Iden -> Sem r Expression goIden i = case i of IdenFunction f -> do - f' <- askFunctionDef f + f' <- lookupFunctionDef f case f' of Nothing -> return i' Just x -> go x @@ -295,7 +296,7 @@ queryMetavar' h = do Just (Refined e) -> return (Just e) runInferenceState :: - (Members '[State FunctionsTable, Error TypeCheckerError, NameIdGen] r) => + (Members '[ResultBuilder, Error TypeCheckerError, NameIdGen] r) => InferenceState -> Sem (Inference ': r) a -> Sem r (InferenceState, a) @@ -311,14 +312,14 @@ runInferenceState inis = reinterpret (runState inis) $ \case registerIdenType' i ty = modify (over (inferenceIdens . typesTable) (HashMap.insert (i ^. nameId) ty)) -- Supports alpha equivalence. - matchTypes' :: (Members '[State InferenceState, State FunctionsTable, Error TypeCheckerError, NameIdGen] r) => Expression -> Expression -> Sem r (Maybe MatchError) + matchTypes' :: (Members '[State InferenceState, ResultBuilder, Error TypeCheckerError, NameIdGen] r) => Expression -> Expression -> Sem r (Maybe MatchError) matchTypes' ty = runReader ini . go ty where ini :: HashMap VarName VarName ini = mempty go :: forall r. - (Members '[State InferenceState, Reader (HashMap VarName VarName), State FunctionsTable, Error TypeCheckerError, NameIdGen] r) => + (Members '[State InferenceState, Reader (HashMap VarName VarName), ResultBuilder, Error TypeCheckerError, NameIdGen] r) => Expression -> Expression -> Sem r (Maybe MatchError) @@ -450,7 +451,7 @@ runInferenceState inis = reinterpret (runState inis) $ \case matchPatterns :: forall r. - (Members '[State InferenceState, State (HashMap VarName VarName), State FunctionsTable] r) => + (Members '[State InferenceState, State (HashMap VarName VarName), ResultBuilder] r) => PatternArg -> PatternArg -> Sem r Bool @@ -484,7 +485,7 @@ matchPatterns (PatternArg impl1 name1 pat1) (PatternArg impl2 name2 pat2) = err = return False runInferenceDefs :: - (Members '[Termination, Error TypeCheckerError, State FunctionsTable, State TypesTable, NameIdGen] r, HasExpressions funDef) => + (Members '[Termination, Error TypeCheckerError, ResultBuilder, NameIdGen] r, HasExpressions funDef) => Sem (Inference ': r) (NonEmpty funDef) -> Sem r (NonEmpty funDef) runInferenceDefs a = do @@ -493,19 +494,15 @@ runInferenceDefs a = do idens' <- mapM (subsHoles subs) (idens ^. typesTable) stash' <- mapM (subsHoles subs) (finalState ^. inferenceFunctionsStash) forM_ stash' registerFunctionDef - addIdens (TypesTable idens') + addIdenTypes (TypesTable idens') mapM (subsHoles subs) expr runInferenceDef :: - (Members '[Termination, Error TypeCheckerError, State FunctionsTable, State TypesTable, NameIdGen] r, HasExpressions funDef) => + (Members '[Termination, Error TypeCheckerError, ResultBuilder, NameIdGen] r, HasExpressions funDef) => Sem (Inference ': r) funDef -> Sem r funDef runInferenceDef = fmap head . runInferenceDefs . fmap pure -addIdens :: (Members '[State TypesTable] r) => TypesTable -> Sem r () -addIdens idens = do - modify (over typesTable (HashMap.union (idens ^. typesTable))) - -- | Assumes the given function has been type checked. Does *not* register the -- function. -- Conditions: @@ -515,14 +512,14 @@ addIdens idens = do -- -- Throws an error if the return type is Type and it does not satisfy the -- above conditions. -functionDefEval :: forall r'. (Members '[State FunctionsTable, Termination, Error TypeCheckerError, NameIdGen] r') => FunctionDef -> Sem r' (Maybe Expression) +functionDefEval :: forall r'. (Members '[ResultBuilder, Termination, Error TypeCheckerError, NameIdGen] r') => FunctionDef -> Sem r' (Maybe Expression) functionDefEval f = do (params :: [FunctionParameter], ret :: Expression) <- unfoldFunType <$> strongNorm (f ^. funDefType) r <- runFail (goTop params (canBeUniverse ret)) when (isNothing r && isUniverse ret) (throw (ErrUnsupportedTypeFunction (UnsupportedTypeFunction f))) return r where - strongNorm :: (Members '[State FunctionsTable, NameIdGen] r) => Expression -> Sem r Expression + strongNorm :: (Members '[ResultBuilder, NameIdGen] r) => Expression -> Sem r Expression strongNorm = evalState iniState . strongNormalize' isUniverse :: Expression -> Bool @@ -539,7 +536,7 @@ functionDefEval f = do goTop :: forall r. - (Members '[Fail, State FunctionsTable, Error TypeCheckerError, Termination] r) => + (Members '[Fail, ResultBuilder, Error TypeCheckerError, Termination] r) => [FunctionParameter] -> Bool -> Sem r Expression @@ -581,6 +578,21 @@ functionDefEval f = do | isImplicitOrInstance (p ^. patternArgIsImplicit) -> fail | otherwise -> go ps >>= goPattern (p ^. patternArgPattern, ty) -registerFunctionDef :: (Members '[State FunctionsTable, Error TypeCheckerError, NameIdGen, Termination] r) => FunctionDef -> Sem r () +registerFunctionDef :: (Members '[ResultBuilder, Error TypeCheckerError, NameIdGen, Termination] r) => FunctionDef -> Sem r () registerFunctionDef f = whenJustM (functionDefEval f) $ \e -> - modify (over functionsTable (HashMap.insert (f ^. funDefName) e)) + addFunctionDef (f ^. funDefName) e + +strongNormalize'' :: (Members '[Reader FunctionsTable, NameIdGen] r) => Expression -> Sem r Expression +strongNormalize'' ty = do + ftab <- ask + let importCtx = + ImportContext + { _importContextCoercions = mempty, + _importContextInstances = mempty, + _importContextTypesTable = mempty, + _importContextFunctionsTable = ftab + } + fmap snd + . runResultBuilder importCtx + . evalState iniState + $ strongNormalize' ty diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs new file mode 100644 index 0000000000..42b50a6bbb --- /dev/null +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs @@ -0,0 +1,88 @@ +module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.ResultBuilder where + +import Data.HashMap.Strict qualified as HashMap +import Juvix.Compiler.Internal.Extra.CoercionInfo +import Juvix.Compiler.Internal.Extra.InstanceInfo +import Juvix.Compiler.Internal.Language +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context +import Juvix.Prelude + +data ResultBuilder :: Effect where + AddFunctionDef :: FunctionName -> Expression -> ResultBuilder m () + AddIdenType :: NameId -> Expression -> ResultBuilder m () + AddIdenTypes :: TypesTable -> ResultBuilder m () + AddInstanceInfo :: InstanceInfo -> ResultBuilder m () + AddCoercionInfo :: CoercionInfo -> ResultBuilder m () + LookupFunctionDef :: FunctionName -> ResultBuilder m (Maybe Expression) + LookupIdenType :: NameId -> ResultBuilder m (Maybe Expression) + LookupInstanceInfo :: Name -> ResultBuilder m (Maybe [InstanceInfo]) + LookupCoercionInfo :: Name -> ResultBuilder m (Maybe [CoercionInfo]) + GetCombinedInstanceTable :: ResultBuilder m InstanceTable + GetCombinedCoercionTable :: ResultBuilder m CoercionTable + +makeSem ''ResultBuilder + +data ResultBuilderState = ResultBuilderState + { _resultBuilderStateTypesTable :: TypesTable, + _resultBuilderStateFunctionsTable :: FunctionsTable, + _resultBuilderStateInstanceTable :: InstanceTable, + _resultBuilderStateCoercionTable :: CoercionTable, + _resultBuilderStateCombinedTypesTable :: TypesTable, + _resultBuilderStateCombinedFunctionsTable :: FunctionsTable, + _resultBuilderStateCombinedInstanceTable :: InstanceTable, + _resultBuilderStateCombinedCoercionTable :: CoercionTable + } + +makeLenses ''ResultBuilderState + +initResultBuilderState :: ImportContext -> ResultBuilderState +initResultBuilderState ctx = + ResultBuilderState + { _resultBuilderStateFunctionsTable = mempty, + _resultBuilderStateTypesTable = mempty, + _resultBuilderStateInstanceTable = mempty, + _resultBuilderStateCoercionTable = mempty, + _resultBuilderStateCombinedFunctionsTable = ctx ^. importContextFunctionsTable, + _resultBuilderStateCombinedTypesTable = ctx ^. importContextTypesTable, + _resultBuilderStateCombinedInstanceTable = ctx ^. importContextInstances, + _resultBuilderStateCombinedCoercionTable = ctx ^. importContextCoercions + } + +runResultBuilder' :: + ResultBuilderState -> + Sem (ResultBuilder ': r) a -> + Sem r (ResultBuilderState, a) +runResultBuilder' inis = reinterpret (runState inis) $ \case + AddFunctionDef name def -> do + modify' (over (resultBuilderStateFunctionsTable . functionsTable) (HashMap.insert name def)) + modify' (over (resultBuilderStateCombinedFunctionsTable . functionsTable) (HashMap.insert name def)) + AddIdenType nid ty -> do + modify' (over (resultBuilderStateTypesTable . typesTable) (HashMap.insert nid ty)) + modify' (over (resultBuilderStateCombinedTypesTable . typesTable) (HashMap.insert nid ty)) + AddIdenTypes itab -> do + modify' (over (resultBuilderStateTypesTable . typesTable) (HashMap.union (itab ^. typesTable))) + modify' (over (resultBuilderStateCombinedTypesTable . typesTable) (HashMap.union (itab ^. typesTable))) + AddInstanceInfo ii -> do + modify' (over (resultBuilderStateInstanceTable) (flip updateInstanceTable ii)) + modify' (over (resultBuilderStateCombinedInstanceTable) (flip updateInstanceTable ii)) + AddCoercionInfo ii -> do + modify' (over (resultBuilderStateCoercionTable) (flip updateCoercionTable ii)) + modify' (over (resultBuilderStateCombinedCoercionTable) (flip updateCoercionTable ii)) + LookupFunctionDef name -> + gets (^. resultBuilderStateCombinedFunctionsTable . functionsTable . at name) + LookupIdenType nid -> + gets (^. resultBuilderStateCombinedTypesTable . typesTable . at nid) + LookupInstanceInfo name -> do + tab <- gets (^. resultBuilderStateCombinedInstanceTable) + return $ lookupInstanceTable tab name + LookupCoercionInfo name -> do + tab <- gets (^. resultBuilderStateCombinedCoercionTable) + return $ lookupCoercionTable tab name + GetCombinedInstanceTable -> + gets (^. resultBuilderStateCombinedInstanceTable) + GetCombinedCoercionTable -> + gets (^. resultBuilderStateCombinedCoercionTable) + +runResultBuilder :: ImportContext -> Sem (ResultBuilder ': r) a -> Sem r (ResultBuilderState, a) +runResultBuilder ctx a = + runResultBuilder' (initResultBuilderState ctx) a diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs index 254f04f728..2518b40448 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs @@ -1,10 +1,10 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Types where -import Juvix.Compiler.Internal.Data.InstanceInfo import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Pretty (fromGenericOptions) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Pretty +import Juvix.Compiler.Store.Internal.Data.InstanceInfo import Juvix.Data.PPOutput import Juvix.Prelude diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs index f54a5c10c4..872e9c8da2 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs @@ -6,13 +6,14 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Tr where import Data.HashMap.Strict qualified as HashMap -import Juvix.Compiler.Internal.Data.CoercionInfo import Juvix.Compiler.Internal.Data.InfoTable -import Juvix.Compiler.Internal.Data.InstanceInfo import Juvix.Compiler.Internal.Data.LocalVars import Juvix.Compiler.Internal.Data.TypedHole import Juvix.Compiler.Internal.Extra +import Juvix.Compiler.Internal.Extra.CoercionInfo +import Juvix.Compiler.Internal.Extra.InstanceInfo import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.ResultBuilder import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error import Juvix.Prelude @@ -27,14 +28,17 @@ isTrait :: InfoTable -> Name -> Bool isTrait tab name = maybe False (^. inductiveInfoTrait) (HashMap.lookup name (tab ^. infoInductives)) resolveTraitInstance :: - (Members '[Error TypeCheckerError, NameIdGen, Inference, Reader InfoTable] r) => + (Members '[Error TypeCheckerError, NameIdGen, Inference, ResultBuilder, Reader InfoTable] r) => TypedHole -> Sem r Expression resolveTraitInstance TypedHole {..} = do - tbl <- ask - let tab = foldr (flip updateInstanceTable) (tbl ^. infoInstances) (varsToInstances tbl _typedHoleLocalVars) + vars <- overM localTypes (mapM strongNormalize) _typedHoleLocalVars + infoTab <- ask + tab0 <- getCombinedInstanceTable + let tab = foldr (flip updateInstanceTable) tab0 (varsToInstances infoTab vars) ty <- strongNormalize _typedHoleType - is <- lookupInstance (tbl ^. infoCoercions) tab ty + ctab <- getCombinedCoercionTable + is <- lookupInstance ctab tab ty case is of [(cs, ii, subs)] -> expandArity loc (subsIToE subs) (ii ^. instanceInfoArgs) (ii ^. instanceInfoResult) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs index 0be85b798d..81d3392446 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Termination.hs @@ -3,7 +3,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Tr ) where -import Juvix.Compiler.Internal.Data.InstanceInfo +import Juvix.Compiler.Internal.Extra.InstanceInfo import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error import Juvix.Prelude diff --git a/src/Juvix/Compiler/Pipeline/Artifacts.hs b/src/Juvix/Compiler/Pipeline/Artifacts.hs index 1001fe5973..0d80d18698 100644 --- a/src/Juvix/Compiler/Pipeline/Artifacts.hs +++ b/src/Juvix/Compiler/Pipeline/Artifacts.hs @@ -19,6 +19,7 @@ import Juvix.Compiler.Internal.Language qualified as Internal import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.ResultBuilder import Juvix.Compiler.Pipeline.Artifacts.Base import Juvix.Compiler.Store.Extra import Juvix.Compiler.Store.Language @@ -67,8 +68,8 @@ runNameIdGenArtifacts :: Sem r a runNameIdGenArtifacts = runStateLikeArtifacts runNameIdGen artifactNameIdState -runFunctionsTableArtifacts :: (Members '[State Artifacts] r) => Sem (State FunctionsTable ': r) a -> Sem r a -runFunctionsTableArtifacts = runStateArtifacts artifactFunctions +readerFunctionsTableArtifacts :: (Members '[State Artifacts] r) => Sem (Reader FunctionsTable ': r) a -> Sem r a +readerFunctionsTableArtifacts = runReaderArtifacts artifactFunctions readerTypesTableArtifacts :: (Members '[State Artifacts] r) => Sem (Reader TypesTable ': r) a -> Sem r a readerTypesTableArtifacts = runReaderArtifacts artifactTypes @@ -76,9 +77,6 @@ readerTypesTableArtifacts = runReaderArtifacts artifactTypes runTerminationArtifacts :: (Members '[Error JuvixError, State Artifacts] r) => Sem (Termination ': r) a -> Sem r a runTerminationArtifacts = runStateLikeArtifacts runTermination artifactTerminationState -runTypesTableArtifacts :: (Members '[State Artifacts] r) => Sem (State TypesTable ': r) a -> Sem r a -runTypesTableArtifacts = runStateArtifacts artifactTypes - runStateArtifacts :: (Members '[State Artifacts] r) => Lens' Artifacts f -> Sem (State f ': r) a -> Sem r a runStateArtifacts = runStateLikeArtifacts runState @@ -98,3 +96,23 @@ runStateLikeArtifacts runner l m = do (s', a) <- runner s m modify' (set l s') return a + +runResultBuilderArtifacts :: forall r a. (Members '[State Artifacts] r) => Sem (ResultBuilder ': r) a -> Sem r a +runResultBuilderArtifacts m = do + ftab <- gets (^. artifactFunctions) + ttab <- gets (^. artifactTypes) + itab <- gets (^. artifactInstances) + ctab <- gets (^. artifactCoercions) + let importCtx = + ImportContext + { _importContextCoercions = ctab, + _importContextInstances = itab, + _importContextFunctionsTable = ftab, + _importContextTypesTable = ttab + } + (s, a) <- runResultBuilder importCtx m + modify' (set artifactFunctions (s ^. resultBuilderStateCombinedFunctionsTable)) + modify' (set artifactTypes (s ^. resultBuilderStateCombinedTypesTable)) + modify' (set artifactInstances (s ^. resultBuilderStateCombinedInstanceTable)) + modify' (set artifactCoercions (s ^. resultBuilderStateCombinedCoercionTable)) + return a diff --git a/src/Juvix/Compiler/Pipeline/Artifacts/Base.hs b/src/Juvix/Compiler/Pipeline/Artifacts/Base.hs index b500bb35bd..a1ebb26d74 100644 --- a/src/Juvix/Compiler/Pipeline/Artifacts/Base.hs +++ b/src/Juvix/Compiler/Pipeline/Artifacts/Base.hs @@ -9,6 +9,8 @@ import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context import Juvix.Compiler.Pipeline.Loader.PathResolver.Data +import Juvix.Compiler.Store.Internal.Data.CoercionInfo +import Juvix.Compiler.Store.Internal.Data.InstanceInfo import Juvix.Compiler.Store.Language qualified as Store import Juvix.Prelude @@ -29,6 +31,8 @@ data Artifacts = Artifacts -- Typechecking _artifactTypes :: TypesTable, _artifactFunctions :: FunctionsTable, + _artifactInstances :: InstanceTable, + _artifactCoercions :: CoercionTable, -- | This includes the InfoTable from all type checked modules _artifactInternalTypedTable :: Internal.InfoTable, -- Core diff --git a/src/Juvix/Compiler/Pipeline/Repl.hs b/src/Juvix/Compiler/Pipeline/Repl.hs index 870f11123b..d87c6c295d 100644 --- a/src/Juvix/Compiler/Pipeline/Repl.hs +++ b/src/Juvix/Compiler/Pipeline/Repl.hs @@ -138,7 +138,7 @@ fromInternalExpression exp = do runNameIdGenArtifacts . runReader typedTable . tmpCoreInfoTableBuilderArtifacts - . runFunctionsTableArtifacts + . readerFunctionsTableArtifacts . readerTypesTableArtifacts . runReader Core.initIndexTable $ Core.goExpression exp diff --git a/src/Juvix/Compiler/Pipeline/Run.hs b/src/Juvix/Compiler/Pipeline/Run.hs index 01a417c902..5f92bdb638 100644 --- a/src/Juvix/Compiler/Pipeline/Run.hs +++ b/src/Juvix/Compiler/Pipeline/Run.hs @@ -193,6 +193,12 @@ runReplPipelineIOEither' lockMode entry = do functionsTable :: Typed.FunctionsTable functionsTable = typedResult ^. Typed.resultFunctions + instanceTable :: Typed.InstanceTable + instanceTable = typedResult ^. Typed.resultInstances + + coercionTable :: Typed.CoercionTable + coercionTable = typedResult ^. Typed.resultCoercions + typedTable :: Internal.InfoTable typedTable = typedResult ^. Typed.resultInternalModule . Typed.internalModuleInfoTable @@ -226,6 +232,8 @@ runReplPipelineIOEither' lockMode entry = do _artifactScopeExports = scopedResult ^. Scoped.resultExports, _artifactTypes = typesTable, _artifactFunctions = functionsTable, + _artifactInstances = instanceTable, + _artifactCoercions = coercionTable, _artifactScoperState = scopedResult ^. Scoped.resultScoperState, _artifactResolver = art ^. artifactResolver, _artifactBuiltins = art ^. artifactBuiltins, @@ -244,6 +252,8 @@ runReplPipelineIOEither' lockMode entry = do _artifactNameIdState = genNameIdState defaultModuleId, _artifactTypes = mempty, _artifactFunctions = mempty, + _artifactInstances = mempty, + _artifactCoercions = mempty, _artifactCoreModule = Core.emptyModule, _artifactScopeTable = mempty, _artifactBuiltins = iniBuiltins, diff --git a/src/Juvix/Compiler/Store/Internal/Data/CoercionInfo.hs b/src/Juvix/Compiler/Store/Internal/Data/CoercionInfo.hs new file mode 100644 index 0000000000..9b09ef1db9 --- /dev/null +++ b/src/Juvix/Compiler/Store/Internal/Data/CoercionInfo.hs @@ -0,0 +1,43 @@ +module Juvix.Compiler.Store.Internal.Data.CoercionInfo where + +import Data.HashMap.Strict qualified as HashMap +import Juvix.Compiler.Internal.Language +import Juvix.Compiler.Store.Internal.Data.InstanceInfo +import Juvix.Extra.Serialize +import Juvix.Prelude + +data CoercionInfo = CoercionInfo + { _coercionInfoInductive :: Name, + _coercionInfoParams :: [InstanceParam], + _coercionInfoTarget :: InstanceApp, + _coercionInfoResult :: Expression, + _coercionInfoArgs :: [FunctionParameter] + } + deriving stock (Eq, Generic) + +instance Hashable CoercionInfo where + hashWithSalt salt CoercionInfo {..} = hashWithSalt salt _coercionInfoResult + +instance Serialize CoercionInfo + +-- | Maps trait names to available coercions +newtype CoercionTable = CoercionTable + { _coercionTableMap :: HashMap InductiveName [CoercionInfo] + } + deriving stock (Eq, Generic) + +instance Serialize CoercionTable + +makeLenses ''CoercionInfo +makeLenses ''CoercionTable + +instance Semigroup CoercionTable where + t1 <> t2 = + CoercionTable $ + HashMap.unionWith combine (t1 ^. coercionTableMap) (t2 ^. coercionTableMap) + where + combine :: [CoercionInfo] -> [CoercionInfo] -> [CoercionInfo] + combine ii1 ii2 = nubHashable (ii1 ++ ii2) + +instance Monoid CoercionTable where + mempty = CoercionTable mempty diff --git a/src/Juvix/Compiler/Store/Internal/Data/FunctionsTable.hs b/src/Juvix/Compiler/Store/Internal/Data/FunctionsTable.hs index 8cd0a54602..3dc289992c 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/FunctionsTable.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/FunctionsTable.hs @@ -13,6 +13,3 @@ newtype FunctionsTable = FunctionsTable instance Serialize FunctionsTable makeLenses ''FunctionsTable - -askFunctionDef :: (Member (State FunctionsTable) r) => FunctionName -> Sem r (Maybe Expression) -askFunctionDef f = gets (^. functionsTable . at f) diff --git a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs index 5452d47344..615c5e6750 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs @@ -1,7 +1,5 @@ module Juvix.Compiler.Store.Internal.Data.InfoTable where -import Juvix.Compiler.Internal.Data.CoercionInfo -import Juvix.Compiler.Internal.Data.InstanceInfo import Juvix.Compiler.Internal.Language import Juvix.Extra.Serialize import Juvix.Prelude @@ -58,9 +56,7 @@ data InfoTable = InfoTable _infoAxioms :: HashMap Name AxiomInfo, _infoFunctions :: HashMap Name FunctionInfo, _infoInductives :: HashMap Name InductiveInfo, - _infoBuiltins :: HashMap BuiltinPrim Name, - _infoInstances :: InstanceTable, - _infoCoercions :: CoercionTable + _infoBuiltins :: HashMap BuiltinPrim Name } deriving stock (Generic) @@ -79,9 +75,7 @@ instance Semigroup InfoTable where _infoAxioms = a ^. infoAxioms <> b ^. infoAxioms, _infoFunctions = a ^. infoFunctions <> b ^. infoFunctions, _infoInductives = a ^. infoInductives <> b ^. infoInductives, - _infoBuiltins = a ^. infoBuiltins <> b ^. infoBuiltins, - _infoInstances = a ^. infoInstances <> b ^. infoInstances, - _infoCoercions = a ^. infoCoercions <> b ^. infoCoercions + _infoBuiltins = a ^. infoBuiltins <> b ^. infoBuiltins } instance Monoid InfoTable where @@ -91,7 +85,5 @@ instance Monoid InfoTable where _infoAxioms = mempty, _infoFunctions = mempty, _infoInductives = mempty, - _infoBuiltins = mempty, - _infoInstances = mempty, - _infoCoercions = mempty + _infoBuiltins = mempty } diff --git a/src/Juvix/Compiler/Store/Internal/Data/InstanceInfo.hs b/src/Juvix/Compiler/Store/Internal/Data/InstanceInfo.hs new file mode 100644 index 0000000000..45c5edc46a --- /dev/null +++ b/src/Juvix/Compiler/Store/Internal/Data/InstanceInfo.hs @@ -0,0 +1,73 @@ +module Juvix.Compiler.Store.Internal.Data.InstanceInfo where + +import Data.HashMap.Strict qualified as HashMap +import Juvix.Compiler.Internal.Language +import Juvix.Extra.Serialize +import Juvix.Prelude + +data InstanceParam + = InstanceParamVar VarName + | InstanceParamApp InstanceApp + | InstanceParamFun InstanceFun + | InstanceParamHole Hole + | InstanceParamMeta VarName + deriving stock (Eq, Generic) + +instance Serialize InstanceParam + +data InstanceApp = InstanceApp + { _instanceAppHead :: Name, + _instanceAppArgs :: [InstanceParam], + -- | The original expression from which this InstanceApp was created + _instanceAppExpression :: Expression + } + deriving stock (Eq, Generic) + +instance Serialize InstanceApp + +data InstanceFun = InstanceFun + { _instanceFunLeft :: InstanceParam, + _instanceFunRight :: InstanceParam, + -- | The original expression from which this InstanceFun was created + _instanceFunExpression :: Expression + } + deriving stock (Eq, Generic) + +instance Serialize InstanceFun + +data InstanceInfo = InstanceInfo + { _instanceInfoInductive :: InductiveName, + _instanceInfoParams :: [InstanceParam], + _instanceInfoResult :: Expression, + _instanceInfoArgs :: [FunctionParameter] + } + deriving stock (Eq, Generic) + +instance Hashable InstanceInfo where + hashWithSalt salt InstanceInfo {..} = hashWithSalt salt _instanceInfoResult + +instance Serialize InstanceInfo + +-- | Maps trait names to available instances +newtype InstanceTable = InstanceTable + { _instanceTableMap :: HashMap InductiveName [InstanceInfo] + } + deriving stock (Eq, Generic) + +instance Serialize InstanceTable + +makeLenses ''InstanceApp +makeLenses ''InstanceFun +makeLenses ''InstanceInfo +makeLenses ''InstanceTable + +instance Semigroup InstanceTable where + t1 <> t2 = + InstanceTable $ + HashMap.unionWith combine (t1 ^. instanceTableMap) (t2 ^. instanceTableMap) + where + combine :: [InstanceInfo] -> [InstanceInfo] -> [InstanceInfo] + combine ii1 ii2 = nubHashable (ii1 ++ ii2) + +instance Monoid InstanceTable where + mempty = InstanceTable mempty diff --git a/src/Juvix/Compiler/Store/Internal/Data/TypesTable.hs b/src/Juvix/Compiler/Store/Internal/Data/TypesTable.hs index d5f3b41236..317ccbd460 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/TypesTable.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/TypesTable.hs @@ -11,3 +11,5 @@ newtype TypesTable = TypesTable deriving stock (Generic) instance Serialize TypesTable + +makeLenses ''TypesTable diff --git a/src/Juvix/Compiler/Store/Internal/Language.hs b/src/Juvix/Compiler/Store/Internal/Language.hs index a5cb3cdf73..78e2f11f0c 100644 --- a/src/Juvix/Compiler/Store/Internal/Language.hs +++ b/src/Juvix/Compiler/Store/Internal/Language.hs @@ -6,8 +6,10 @@ where import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Internal.Language +import Juvix.Compiler.Store.Internal.Data.CoercionInfo import Juvix.Compiler.Store.Internal.Data.FunctionsTable import Juvix.Compiler.Store.Internal.Data.InfoTable +import Juvix.Compiler.Store.Internal.Data.InstanceInfo import Juvix.Compiler.Store.Internal.Data.TypesTable import Juvix.Extra.Serialize import Juvix.Prelude @@ -17,6 +19,8 @@ data InternalModule = InternalModule _internalModuleName :: Name, _internalModuleImports :: [Import], _internalModuleInfoTable :: InfoTable, + _internalModuleInstanceTable :: InstanceTable, + _internalModuleCoercionTable :: CoercionTable, _internalModuleTypesTable :: TypesTable, _internalModuleFunctionsTable :: FunctionsTable } @@ -49,3 +53,9 @@ computeTypesTable = mconcatMap (^. internalModuleTypesTable) . (^. internalModul computeFunctionsTable :: InternalModuleTable -> FunctionsTable computeFunctionsTable = mconcatMap (^. internalModuleFunctionsTable) . (^. internalModuleTable) + +computeInstanceTable :: InternalModuleTable -> InstanceTable +computeInstanceTable = mconcatMap (^. internalModuleInstanceTable) . (^. internalModuleTable) + +computeCoercionTable :: InternalModuleTable -> CoercionTable +computeCoercionTable = mconcatMap (^. internalModuleCoercionTable) . (^. internalModuleTable) diff --git a/tests/Compilation/positive/test052.juvix b/tests/Compilation/positive/test052.juvix index 0a1e4d749e..c165143647 100644 --- a/tests/Compilation/positive/test052.juvix +++ b/tests/Compilation/positive/test052.juvix @@ -23,6 +23,7 @@ type Lambda' (v : Type) := mkLambda : Expr' v -> Lambda' v; type App' (v : Type) := mkApp : Expr' v -> Expr' v -> App' v; +--- Expression with ;Nat; atoms Expr : Type := Expr' Nat; Lambda : Type := Lambda' Nat; @@ -68,7 +69,7 @@ exprToString : Expr -> String --- ;Show; instance for ;Expr;. instance -showExprI : Show (Expr' Nat) := mkShow exprToString; +showExprI : Show Expr := mkShow exprToString; terminating valToString : Val -> String @@ -81,7 +82,7 @@ valToString : Val -> String --- ;Show; instance for ;Val;. terminating instance -showValI : Show (Val' Nat) := mkShow valToString; +showValI : Show Val := mkShow valToString; syntax operator >>= seq; --- Monadic binding for ;Either;. diff --git a/tests/Compilation/positive/test061.juvix b/tests/Compilation/positive/test061.juvix index 717032647c..a99ef36e04 100644 --- a/tests/Compilation/positive/test061.juvix +++ b/tests/Compilation/positive/test061.juvix @@ -6,11 +6,14 @@ import Stdlib.Prelude open hiding {Show; mkShow; module Show}; trait type Show A := mkShow {show : A → String}; +Show' : Type -> Type := Show; +Bool' : Type := Bool; + instance showStringI : Show String := mkShow (show := id); instance -showBoolI : Show Bool := +showBoolI : Show' Bool' := mkShow@{ show (x : Bool) : String := if x "true" "false" }; @@ -21,9 +24,9 @@ showNatI : Show Nat := mkShow (show := natToString); g : {A : Type} → {{Show A}} → Nat := 5; instance -showListI {A} {{Show A}} : Show (List A) := +showListI {A} {{Show' A}} : Show (List A) := mkShow@{ - show {A} : {{Show A}} → List A → String + show {A} : {{Show' A}} → List A → String | nil := "nil" | (h :: t) := Show.show h ++str " :: " ++str show t }; @@ -49,7 +52,7 @@ f'3 {A} {{M : Show A}} : A → String := Show.show {{M}}; f'4 {A} {{_ : Show A}} : A → String := Show.show; -f5 {A} {{Show A}} (n : String) (a : A) : String := +f5 {A} {{Show' A}} (n : String) (a : A) : String := n ++str Show.show a; instance @@ -63,7 +66,7 @@ showBoolFunI : Show (Bool → Bool) := mkShow@{ }; instance -showPairI {A B} {{Show A}} {{Show B}} : Show (A × B) := +showPairI {A B} {{Show A}} {{Show' B}} : Show' (A × B) := mkShow λ {(x, y) := Show.show x ++str ", " ++str Show.show y}; trait