From c8e7ce8afd1e8a4c40fc42da58c577ea1e76fae8 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 1 Dec 2023 16:50:37 +0100 Subject: [PATCH] Remove old typechecker (#2545) --- app/Commands/Dev/Internal.hs | 2 - app/Commands/Dev/Internal/Arity.hs | 12 - app/Commands/Dev/Internal/Arity/Options.hs | 15 - app/Commands/Dev/Internal/Options.hs | 12 - app/GlobalOptions.hs | 14 +- .../Backend/Html/Translation/FromTyped.hs | 7 +- src/Juvix/Compiler/Internal/Pretty/Base.hs | 9 - .../Internal/Translation/FromConcrete.hs | 13 - .../Internal/Translation/FromInternal.hs | 76 +- .../FromInternal/Analysis/ArityChecking.hs | 10 - .../Analysis/ArityChecking/Checker.hs | 905 ------------------ .../Analysis/ArityChecking/Data.hs | 10 - .../Analysis/ArityChecking/Data/Context.hs | 23 - .../Analysis/ArityChecking/Data/LocalVars.hs | 25 - .../Analysis/ArityChecking/Data/Types.hs | 149 --- .../FromInternal/Analysis/Reachability.hs | 3 +- .../FromInternal/Analysis/TypeChecking.hs | 4 +- .../Analysis/TypeChecking/Checker.hs | 5 +- .../Analysis/TypeChecking/CheckerNew.hs | 9 +- .../Analysis/TypeChecking/Data/Context.hs | 9 +- .../Internal/Translation/FromInternal/Data.hs | 4 +- src/Juvix/Compiler/Pipeline.hs | 11 +- src/Juvix/Compiler/Pipeline/EntryPoint.hs | 6 +- src/Juvix/Compiler/Pipeline/Repl.hs | 11 +- src/Juvix/Compiler/Pipeline/Run.hs | 4 +- test/Arity.hs | 10 - test/Arity/Negative.hs | 116 --- test/Compilation.hs | 3 +- test/Compilation/Positive.hs | 732 +++++++------- test/Compilation/PositiveNew.hs | 56 -- test/Main.hs | 2 - test/Scope/Negative.hs | 7 - test/Typecheck.hs | 4 +- test/Typecheck/NegativeNew.hs | 2 +- test/Typecheck/PositiveNew.hs | 48 - tests/Compilation/positive/test046.juvix | 8 +- tests/negative/UnsupportedType.juvix | 5 - 37 files changed, 426 insertions(+), 1915 deletions(-) delete mode 100644 app/Commands/Dev/Internal/Arity.hs delete mode 100644 app/Commands/Dev/Internal/Arity/Options.hs delete mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking.hs delete mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs delete mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data.hs delete mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Context.hs delete mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/LocalVars.hs delete mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs delete mode 100644 test/Arity.hs delete mode 100644 test/Arity/Negative.hs delete mode 100644 test/Compilation/PositiveNew.hs delete mode 100644 test/Typecheck/PositiveNew.hs delete mode 100644 tests/negative/UnsupportedType.juvix diff --git a/app/Commands/Dev/Internal.hs b/app/Commands/Dev/Internal.hs index d592cd43b..2e89ac3d1 100644 --- a/app/Commands/Dev/Internal.hs +++ b/app/Commands/Dev/Internal.hs @@ -1,7 +1,6 @@ module Commands.Dev.Internal where import Commands.Base -import Commands.Dev.Internal.Arity qualified as Arity import Commands.Dev.Internal.Options import Commands.Dev.Internal.Pretty qualified as Pretty import Commands.Dev.Internal.Reachability qualified as Reachability @@ -10,6 +9,5 @@ import Commands.Dev.Internal.Typecheck qualified as Typecheck runCommand :: (Members '[Embed IO, App] r) => InternalCommand -> Sem r () runCommand = \case Pretty opts -> Pretty.runCommand opts - Arity opts -> Arity.runCommand opts TypeCheck opts -> Typecheck.runCommand opts Reachability opts -> Reachability.runCommand opts diff --git a/app/Commands/Dev/Internal/Arity.hs b/app/Commands/Dev/Internal/Arity.hs deleted file mode 100644 index 02568930d..000000000 --- a/app/Commands/Dev/Internal/Arity.hs +++ /dev/null @@ -1,12 +0,0 @@ -module Commands.Dev.Internal.Arity where - -import Commands.Base -import Commands.Dev.Internal.Arity.Options -import Juvix.Compiler.Internal.Pretty qualified as Internal -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as InternalArity - -runCommand :: (Members '[Embed IO, App] r) => InternalArityOptions -> Sem r () -runCommand opts = do - globalOpts <- askGlobalOptions - micro <- head . (^. InternalArity.resultModules) <$> runPipelineTermination (opts ^. internalArityInputFile) upToInternalArity - renderStdOut (Internal.ppOut globalOpts micro) diff --git a/app/Commands/Dev/Internal/Arity/Options.hs b/app/Commands/Dev/Internal/Arity/Options.hs deleted file mode 100644 index e60c80f06..000000000 --- a/app/Commands/Dev/Internal/Arity/Options.hs +++ /dev/null @@ -1,15 +0,0 @@ -module Commands.Dev.Internal.Arity.Options where - -import CommonOptions - -newtype InternalArityOptions = InternalArityOptions - { _internalArityInputFile :: AppPath File - } - deriving stock (Data) - -makeLenses ''InternalArityOptions - -parseInternalArity :: Parser InternalArityOptions -parseInternalArity = do - _internalArityInputFile <- parseInputFile FileExtJuvix - pure InternalArityOptions {..} diff --git a/app/Commands/Dev/Internal/Options.hs b/app/Commands/Dev/Internal/Options.hs index c038dfe21..6fc62ae7c 100644 --- a/app/Commands/Dev/Internal/Options.hs +++ b/app/Commands/Dev/Internal/Options.hs @@ -1,6 +1,5 @@ module Commands.Dev.Internal.Options where -import Commands.Dev.Internal.Arity.Options import Commands.Dev.Internal.Pretty.Options import Commands.Dev.Internal.Reachability.Options import Commands.Dev.Internal.Typecheck.Options @@ -9,7 +8,6 @@ import CommonOptions data InternalCommand = Pretty InternalPrettyOptions | TypeCheck InternalTypeOptions - | Arity InternalArityOptions | Reachability InternalReachabilityOptions deriving stock (Data) @@ -18,14 +16,10 @@ parseInternalCommand = hsubparser $ mconcat [ commandPretty, - commandArity, commandTypeCheck, commandReachability ] where - commandArity :: Mod CommandFields InternalCommand - commandArity = command "arity" arityInfo - commandPretty :: Mod CommandFields InternalCommand commandPretty = command "pretty" prettyInfo @@ -35,12 +29,6 @@ parseInternalCommand = commandReachability :: Mod CommandFields InternalCommand commandReachability = command "reachability" reachabilityInfo - arityInfo :: ParserInfo InternalCommand - arityInfo = - info - (Arity <$> parseInternalArity) - (progDesc "Translate a Juvix file to Internal and insert holes") - prettyInfo :: ParserInfo InternalCommand prettyInfo = info diff --git a/app/GlobalOptions.hs b/app/GlobalOptions.hs index 37296da5b..7591ae60d 100644 --- a/app/GlobalOptions.hs +++ b/app/GlobalOptions.hs @@ -20,8 +20,7 @@ data GlobalOptions = GlobalOptions _globalNoCoverage :: Bool, _globalNoStdlib :: Bool, _globalUnrollLimit :: Int, - _globalOffline :: Bool, - _globalNewTypecheckingAlgorithm :: Bool + _globalOffline :: Bool } deriving stock (Eq, Show) @@ -61,8 +60,7 @@ defaultGlobalOptions = _globalNoCoverage = False, _globalNoStdlib = False, _globalUnrollLimit = defaultUnrollLimit, - _globalOffline = False, - _globalNewTypecheckingAlgorithm = False + _globalOffline = False } -- | Get a parser for global flags which can be hidden or not depending on @@ -128,11 +126,6 @@ parseGlobalFlags = do ( long "show-name-ids" <> help "[DEV] Show the unique number of each identifier when pretty printing" ) - _globalNewTypecheckingAlgorithm <- - switch - ( long "new-typechecker" - <> help "[DEV] Use the new experimental typechecker" - ) return GlobalOptions {..} parseBuildDir :: Mod OptionFields (Prepath Dir) -> Parser (AppPath Dir) @@ -165,8 +158,7 @@ entryPointFromGlobalOptions root mainFile opts = do _entryPointUnrollLimit = opts ^. globalUnrollLimit, _entryPointGenericOptions = project opts, _entryPointBuildDir = maybe (def ^. entryPointBuildDir) (CustomBuildDir . Abs) mabsBuildDir, - _entryPointOffline = opts ^. globalOffline, - _entryPointNewTypeCheckingAlgorithm = opts ^. globalNewTypecheckingAlgorithm + _entryPointOffline = opts ^. globalOffline } where optBuildDir :: Maybe (Prepath Dir) diff --git a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs index 6df563c75..f394bc681 100644 --- a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs +++ b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs @@ -18,7 +18,6 @@ import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Print import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoped import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as InternalArity import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qualified as InternalTyped import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context import Juvix.Compiler.Pipeline.EntryPoint @@ -166,8 +165,7 @@ genJudocHtml JudocArgs {..} = cs :: Comments cs = _judocArgsCtx - ^. resultInternalArityResult - . InternalArity.resultInternalResult + ^. resultInternalResult . Internal.resultScoper . Scoped.comments @@ -180,8 +178,7 @@ genJudocHtml JudocArgs {..} = mainMod :: Module 'Scoped 'ModuleTop mainMod = _judocArgsCtx - ^. InternalTyped.resultInternalArityResult - . InternalArity.resultInternalResult + ^. InternalTyped.resultInternalResult . Internal.resultScoper . Scoped.mainModule diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index d157185df..46b3851e1 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -11,10 +11,8 @@ import Juvix.Compiler.Internal.Data.InstanceInfo (instanceInfoResult, instanceTa import Juvix.Compiler.Internal.Data.LocalVars import Juvix.Compiler.Internal.Data.NameDependencyInfo import Juvix.Compiler.Internal.Data.TypedHole -import Juvix.Compiler.Internal.Extra.Base import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Pretty.Options -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types (Arity) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New import Juvix.Data.CodeAnn import Juvix.Prelude @@ -113,13 +111,6 @@ ppMutual l = do return (braces (line <> indent' b' <> line)) return (kwMutual <+> defs') -instance PrettyCode Arity where - ppCode = return . pretty - -instance PrettyCode ApplicationArg where - ppCode ApplicationArg {..} = - implicitDelim _appArgIsImplicit <$> ppCode _appArg - instance PrettyCode LetClause where ppCode :: forall r. (Member (Reader Options) r) => LetClause -> Sem r (Doc Ann) ppCode = \case diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index d666edb90..49dd5d2c4 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -503,19 +503,6 @@ goInductiveParameters :: Sem r [Internal.InductiveParameter] goInductiveParameters params@InductiveParameters {..} = do paramType' <- goRhs _inductiveParametersRhs - newAlgo <- asks (^. entryPointNewTypeCheckingAlgorithm) - case paramType' of - Internal.ExpressionUniverse {} -> return () - Internal.ExpressionHole {} -> return () - _ -> - unless newAlgo - . throw - $ ErrUnsupported - Unsupported - { _unsupportedMsg = "only type variables of small types are allowed", - _unsupportedLoc = getLoc params - } - let goInductiveParameter :: S.Symbol -> Internal.InductiveParameter goInductiveParameter var = Internal.InductiveParameter diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs index dc8164323..6e92708b8 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs @@ -1,12 +1,9 @@ module Juvix.Compiler.Internal.Translation.FromInternal ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability, - arityChecking, typeChecking, typeCheckingNew, typeCheckExpression, typeCheckExpressionType, - arityCheckExpression, - arityCheckImport, typeCheckImport, ) where @@ -17,60 +14,14 @@ import Juvix.Compiler.Concrete.Data.Highlight.Input import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Pretty import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context as Internal -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as ArityChecking -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context (InternalArityResult (InternalArityResult)) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew qualified as New import Juvix.Compiler.Pipeline.Artifacts import Juvix.Compiler.Pipeline.EntryPoint import Juvix.Data.Effect.NameIdGen import Juvix.Prelude hiding (fromEither) -arityChecking :: - (Members '[Error JuvixError, NameIdGen] r) => - InternalResult -> - Sem r ArityChecking.InternalArityResult -arityChecking res@InternalResult {..} = - mapError (JuvixError @ArityChecking.ArityCheckerError) $ do - r <- - runReader table - . evalCacheEmpty ArityChecking.checkModuleIndexNoCache - $ mapM ArityChecking.checkModule _resultModules - return - ArityChecking.InternalArityResult - { _resultInternalResult = res, - _resultModules = r - } - where - table :: InfoTable - table = buildTable _resultModules - -arityCheckExpression :: - (Members '[Error JuvixError, State Artifacts] r) => - Expression -> - Sem r Expression -arityCheckExpression exp = do - table <- extendedTableReplArtifacts exp - mapError (JuvixError @ArityChecking.ArityCheckerError) - . runReader table - . runNameIdGenArtifacts - $ ArityChecking.inferReplExpression exp - -arityCheckImport :: - (Members '[Error JuvixError, State Artifacts] r) => - Import -> - Sem r Import -arityCheckImport i = do - artiTable <- gets (^. artifactInternalTypedTable) - let table = buildTable [i ^. importModule . moduleIxModule] <> artiTable - mapError (JuvixError @ArityChecking.ArityCheckerError) - . runReader table - . runNameIdGenArtifacts - . evalCacheEmpty ArityChecking.checkModuleIndexNoCache - $ ArityChecking.checkImport i - typeCheckExpressionType :: forall r. (Members '[Error JuvixError, State Artifacts, Termination] r) => @@ -85,7 +36,8 @@ typeCheckExpressionType exp = do . runNameIdGenArtifacts . runReader table . ignoreOutput @Example - . withEmptyVars + . withEmptyLocalVars + . withEmptyInsertedArgsStack . mapError (JuvixError @TypeCheckerError) . runInferenceDef $ inferExpression Nothing exp @@ -113,7 +65,7 @@ typeCheckImport i = do . runNameIdGenArtifacts . ignoreOutput @Example . runReader table - . withEmptyVars + . withEmptyLocalVars -- TODO Store cache in Artifacts and use it here . evalCacheEmpty checkModuleNoCache $ checkTable >> checkImport i @@ -121,16 +73,16 @@ typeCheckImport i = do typeChecking :: forall r. (Members '[HighlightBuilder, Error JuvixError, Builtins, NameIdGen] r) => - Sem (Termination ': r) ArityChecking.InternalArityResult -> + Sem (Termination ': r) Internal.InternalResult -> Sem r InternalTypedResult typeChecking a = do (termin, (res, table, (normalized, (idens, (funs, r))))) <- runTermination iniTerminationState $ do res <- a let table :: InfoTable - table = buildTable (res ^. ArityChecking.resultModules) + table = buildTable (res ^. Internal.resultModules) entryPoint :: EntryPoint - entryPoint = res ^. ArityChecking.internalArityResultEntryPoint + entryPoint = res ^. Internal.internalResultEntryPoint fmap (res,table,) . runOutputList . runReader entryPoint @@ -139,10 +91,10 @@ typeChecking a = do . runReader table . mapError (JuvixError @TypeCheckerError) . evalCacheEmpty checkModuleNoCache - $ checkTable >> mapM checkModule (res ^. ArityChecking.resultModules) + $ checkTable >> mapM checkModule (res ^. Internal.resultModules) return InternalTypedResult - { _resultInternalArityResult = res, + { _resultInternalResult = res, _resultModules = r, _resultTermination = termin, _resultNormalized = HashMap.fromList [(e ^. exampleId, e ^. exampleExpression) | e <- normalized], @@ -171,17 +123,11 @@ typeCheckingNew a = do . runState (mempty :: FunctionsTable) . runReader table . mapError (JuvixError @TypeCheckerError) - . evalCacheEmpty New.checkModuleNoCache - $ checkTable >> mapM New.checkModule (res ^. Internal.resultModules) - let ariRes :: InternalArityResult - ariRes = - InternalArityResult - { _resultInternalResult = res, - _resultModules = res ^. Internal.resultModules - } + . evalCacheEmpty checkModuleNoCache + $ checkTable >> mapM checkModule (res ^. Internal.resultModules) return InternalTypedResult - { _resultInternalArityResult = ariRes, + { _resultInternalResult = res, _resultModules = r, _resultTermination = termin, _resultNormalized = HashMap.fromList [(e ^. exampleId, e ^. exampleExpression) | e <- normalized], diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking.hs deleted file mode 100644 index 835803e64..000000000 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking.hs +++ /dev/null @@ -1,10 +0,0 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking - ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Checker, - module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data, - module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error, - ) -where - -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Checker -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs deleted file mode 100644 index 04d23ac45..000000000 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs +++ /dev/null @@ -1,905 +0,0 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Checker - ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Checker, - module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error, - ) -where - -import Data.List.NonEmpty qualified as NonEmpty -import Juvix.Compiler.Internal.Extra -import Juvix.Compiler.Internal.Extra qualified as Internal -import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.LocalVars -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error -import Juvix.Data.Effect.NameIdGen -import Juvix.Prelude hiding (fromEither) - -type MCache = Cache ModuleIndex Module - -checkModule :: - (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) => - Module -> - Sem r Module -checkModule = cacheGet . ModuleIndex - -checkModuleIndexNoCache :: - (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) => - ModuleIndex -> - Sem r Module -checkModuleIndexNoCache (ModuleIndex Module {..}) = do - _moduleBody' <- runReader @InsertedArgsStack mempty (checkModuleBody _moduleBody) - return - Module - { _moduleBody = _moduleBody', - .. - } - -checkModuleBody :: - (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) => - ModuleBody -> - Sem r ModuleBody -checkModuleBody ModuleBody {..} = do - _moduleStatements' <- mapM checkMutualBlock _moduleStatements - _moduleImports' <- mapM checkImport _moduleImports - return - ModuleBody - { _moduleStatements = _moduleStatements', - _moduleImports = _moduleImports' - } - -checkModuleIndex :: - (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) => - ModuleIndex -> - Sem r ModuleIndex -checkModuleIndex (ModuleIndex m) = ModuleIndex <$> checkModule m - -checkImport :: - (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r) => - Import -> - Sem r Import -checkImport = traverseOf importModule checkModuleIndex - -checkInductive :: forall r. (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => InductiveDef -> Sem r InductiveDef -checkInductive d = do - let _inductiveName = d ^. inductiveName - _inductiveBuiltin = d ^. inductiveBuiltin - _inductivePositive = d ^. inductivePositive - _inductiveTrait = d ^. inductiveTrait - _inductivePragmas = d ^. inductivePragmas - (localVars, _inductiveParameters) <- checkParameters (d ^. inductiveParameters) - _inductiveExamples <- runReader localVars (mapM checkExample (d ^. inductiveExamples)) - _inductiveConstructors <- runReader localVars (mapM checkConstructor (d ^. inductiveConstructors)) - _inductiveType <- runReader localVars (checkType (d ^. inductiveType)) - return InductiveDef {..} - where - checkParameters :: [InductiveParameter] -> Sem r (LocalVars, [InductiveParameter]) - checkParameters = runState emptyLocalVars . mapM checkParam - where - checkParam :: InductiveParameter -> Sem (State LocalVars ': r) InductiveParameter - checkParam param = do - lv1 <- get @LocalVars - ty' <- runReader lv1 (checkType (param ^. inductiveParamType)) - addArity (param ^. inductiveParamName) (typeArity ty') - return - InductiveParameter - { _inductiveParamName = param ^. inductiveParamName, - _inductiveParamType = ty' - } - -checkConstructor :: (Members '[Reader InsertedArgsStack, Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => ConstructorDef -> Sem r ConstructorDef -checkConstructor c = do - let _inductiveConstructorName = c ^. inductiveConstructorName - _inductiveConstructorPragmas = c ^. inductiveConstructorPragmas - _inductiveConstructorType <- checkType (c ^. inductiveConstructorType) - _inductiveConstructorExamples <- mapM checkExample (c ^. inductiveConstructorExamples) - return ConstructorDef {..} - --- | check the arity of some ty : Type -checkType :: (Members '[Reader InsertedArgsStack, Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => Expression -> Sem r Expression -checkType = checkExpression ArityUnit - -checkAxiom :: (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => AxiomDef -> Sem r AxiomDef -checkAxiom a = do - let _axiomName = a ^. axiomName - _axiomBuiltin = a ^. axiomBuiltin - _axiomPragmas = a ^. axiomPragmas - _axiomType <- withEmptyLocalVars (checkType (a ^. axiomType)) - return AxiomDef {..} - -checkMutualStatement :: - (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => - MutualStatement -> - Sem r MutualStatement -checkMutualStatement = \case - StatementFunction f -> StatementFunction <$> checkFunctionDef f - StatementInductive f -> StatementInductive <$> checkInductive f - StatementAxiom a -> StatementAxiom <$> checkAxiom a - -checkMutualBlockLet :: - (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => - MutualBlockLet -> - Sem r MutualBlockLet -checkMutualBlockLet (MutualBlockLet funs) = MutualBlockLet <$> mapM checkFunctionDef funs - -checkMutualBlock :: - (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => - MutualBlock -> - Sem r MutualBlock -checkMutualBlock (MutualBlock funs) = MutualBlock <$> mapM checkMutualStatement funs - -checkFunctionDef :: - forall r. - (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => - FunctionDef -> - Sem r FunctionDef -checkFunctionDef FunctionDef {..} = do - let arity = typeArity _funDefType - _funDefType' <- withEmptyLocalVars (checkType _funDefType) - _funDefBody' <- checkFunctionBody arity _funDefBody - _funDefExamples' <- withEmptyLocalVars (mapM checkExample _funDefExamples) - let argTys = fst (unfoldFunType _funDefType') - _funDefArgsInfo' <- withEmptyLocalVars (checkArgsInfo _funDefArgsInfo argTys) - return - FunctionDef - { _funDefBody = _funDefBody', - _funDefExamples = _funDefExamples', - _funDefType = _funDefType', - _funDefArgsInfo = _funDefArgsInfo', - _funDefName, - _funDefTerminating, - _funDefInstance, - _funDefCoercion, - _funDefBuiltin, - _funDefPragmas - } - -checkArgsInfo :: - forall r. - (Members '[Reader InsertedArgsStack, NameIdGen, Reader LocalVars, Error ArityCheckerError, Reader InfoTable] r) => - [ArgInfo] -> - [FunctionParameter] -> - Sem r [ArgInfo] -checkArgsInfo defaults = - execOutputList - . go defaults - where - go :: [ArgInfo] -> [FunctionParameter] -> Sem (Output ArgInfo ': r) () - go = \case - [] -> const (return ()) - d : ds' -> \case - [] -> impossible - p : ps' -> do - let ari = typeArity (p ^. paramType) - dval <- case (d ^. argInfoDefault, p ^. paramImplicit) of - (Nothing, _) -> return Nothing - (Just val, Implicit) -> - Just <$> checkExpression ari val - (Just {}, _) -> impossible - output (set argInfoDefault dval d) - withLocalVarMaybe ari (p ^. paramName) (go ds' ps') - -checkFunctionBody :: - (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => - Arity -> - Expression -> - Sem r Expression -checkFunctionBody ari body = do - case body of - ExpressionLambda {} -> - withEmptyLocalVars (checkExpression ari body) - _ -> do - hint <- guessArity body - (patterns', locals, bodyAri) <- checkLhs (getLoc body) hint ari [] - body' <- runReader locals (checkExpression bodyAri body) - return $ case nonEmpty patterns' of - Nothing -> body' - Just lambdaPatterns' -> - ExpressionLambda - Lambda - { _lambdaType = Nothing, - _lambdaClauses = - pure - LambdaClause - { _lambdaPatterns = lambdaPatterns', - _lambdaBody = body' - } - } - -simplelambda :: a -simplelambda = error "simple lambda expressions are not supported by the arity checker" - -withLocalVarMaybe :: (Members '[Reader LocalVars] r) => Arity -> Maybe VarName -> Sem r a -> Sem r a -withLocalVarMaybe ari mv = case mv of - Nothing -> id - Just v -> withLocalVar ari v - -withLocalVar :: (Members '[Reader LocalVars] r) => Arity -> VarName -> Sem r a -> Sem r a -withLocalVar ari v = local (withArity v ari) - -withEmptyLocalVars :: Sem (Reader LocalVars ': r) a -> Sem r a -withEmptyLocalVars = runReader emptyLocalVars - -arityLet :: (Members '[Reader InfoTable] r) => Let -> Sem r Arity -arityLet l = guessArity (l ^. letExpression) - -inferReplExpression :: (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => Expression -> Sem r Expression -inferReplExpression e = do - ari <- guessArity e - withEmptyLocalVars - . runReader @InsertedArgsStack mempty - $ checkExpression ari e - -guessArity :: - forall r. - (Members '[Reader InfoTable] r) => - Expression -> - Sem r Arity -guessArity = \case - ExpressionHole {} -> return ArityUnknown - ExpressionInstanceHole {} -> return ArityUnit - ExpressionFunction {} -> return ArityUnit - ExpressionLiteral {} -> return arityLiteral - ExpressionApplication a -> appHelper a - ExpressionIden i -> idenHelper i - ExpressionUniverse {} -> return arityUniverse - ExpressionSimpleLambda {} -> simplelambda - ExpressionLambda l -> return (arityLambda l) - ExpressionLet l -> arityLet l - ExpressionCase l -> arityCase l - where - idenHelper :: Iden -> Sem r Arity - idenHelper i = case i of - IdenVar {} -> return ArityUnknown - _ -> withEmptyLocalVars (idenArity i) - - appHelper :: Application -> Sem r Arity - appHelper a = do - f' <- arif - let u = unfoldArity' f' - return $ case refine args (u ^. ufoldArityParams) of - Nothing -> ArityUnknown - Just a' -> foldArity (set ufoldArityParams a' u) - where - (f, args) = second (map (^. appArgIsImplicit) . toList) (unfoldApplication' a) - - refine :: [IsImplicit] -> [ArityParameter] -> Maybe [ArityParameter] - refine as ps = case (as, ps) of - (Explicit : as', ArityParameter {_arityParameterImplicit = Explicit} : ps') -> refine as' ps' - (Implicit : as', ArityParameter {_arityParameterImplicit = Implicit} : ps') -> refine as' ps' - (ImplicitInstance : as', ArityParameter {_arityParameterImplicit = ImplicitInstance} : ps') -> refine as' ps' - (as'@(Explicit : _), ArityParameter {_arityParameterImplicit = Implicit} : ps') -> refine as' ps' - (as'@(Explicit : _), ArityParameter {_arityParameterImplicit = ImplicitInstance} : ps') -> refine as' ps' - (Implicit : _, ArityParameter {_arityParameterImplicit = Explicit} : _) -> Nothing - (ImplicitInstance : _, ArityParameter {_arityParameterImplicit = Explicit} : _) -> Nothing - (Implicit : _, ArityParameter {_arityParameterImplicit = ImplicitInstance} : _) -> Nothing - (ImplicitInstance : _, ArityParameter {_arityParameterImplicit = Implicit} : _) -> Nothing - ([], ps') -> Just ps' - (_ : _, []) -> Nothing - - arif :: Sem r Arity - arif = guessArity f - -arityLiteral :: Arity -arityLiteral = ArityUnit - -arityUniverse :: Arity -arityUniverse = ArityUnit - --- | All branches should have the same arity. If they are all the same, we --- return that, otherwise we return ArityUnknown. Probably something better can --- be done. -arityCase :: (Members '[Reader InfoTable] r) => Case -> Sem r Arity -arityCase c = do - aris <- mapM (guessArity . (^. caseBranchExpression)) (c ^. caseBranches) - return - if - | allSame aris -> head aris - | otherwise -> ArityUnknown - --- | Lambdas can only have explicit arguments. Since we do not have dependent --- types, it is ok to (partially) infer the arity of the lambda from the clause --- with the most patterns. -arityLambda :: Lambda -> Arity -arityLambda l = - foldArity - UnfoldedArity - { _ufoldArityParams = - replicate - (maximum1 (fmap numPatterns (l ^. lambdaClauses))) - ( ArityParameter - { _arityParameterArity = ArityUnknown, - _arityParameterImplicit = Explicit, - _arityParameterInfo = emptyArgInfo - } - ), - _ufoldArityRest = ArityRestUnknown - } - where - numPatterns :: LambdaClause -> Int - numPatterns (LambdaClause ps _) = length ps - -checkLhs :: - forall r. - (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => - Interval -> - Arity -> - Arity -> - [PatternArg] -> - Sem r ([PatternArg], LocalVars, Arity) -checkLhs loc guessedBody ariSignature pats = do - (locals, (pats', bodyAri)) <- runState emptyLocalVars (goLhs ariSignature pats) - return (pats', locals, bodyAri) - where - -- returns the expanded patterns and the rest of the Arity (the arity of the - -- body once all the patterns have been processed). - -- Does not insert holes greedily. I.e. implicit wildcards are only inserted - -- between explicit parameters already in the pattern. - goLhs :: Arity -> [PatternArg] -> Sem (State LocalVars ': r) ([PatternArg], Arity) - goLhs a = \case - [] -> case tailHelper a of - Nothing -> return ([], a) - Just tailUnderscores -> do - let n = length tailUnderscores - a' = foldArity (over ufoldArityParams (drop n) (unfoldArity' a)) - wildcards <- mapM genWildcard' tailUnderscores - return (wildcards, a') - lhs@(p : ps) -> case a of - ArityUnit -> - throw - ( ErrLhsTooManyPatterns - LhsTooManyPatterns - { _lhsTooManyPatternsRemaining = p :| ps - } - ) - ArityUnknown -> do - p' <- checkPattern ArityUnknown p - first (p' :) <$> goLhs ArityUnknown ps - ArityFunction (FunctionArity l r) -> - case (p ^. patternArgIsImplicit, l ^. arityParameterImplicit) of - (Implicit, Implicit {}) -> do - b' <- checkPattern (arityParameter l) p - first (b' :) <$> goLhs r ps - (Implicit, Explicit {}) -> - throw - ( ErrWrongPatternIsImplicit - WrongPatternIsImplicit - { _wrongPatternIsImplicitExpected = Explicit, - _wrongPatternIsImplicitActual = p - } - ) - (Implicit, ImplicitInstance {}) -> - throw - ( ErrWrongPatternIsImplicit - WrongPatternIsImplicit - { _wrongPatternIsImplicitExpected = ImplicitInstance, - _wrongPatternIsImplicitActual = p - } - ) - (ImplicitInstance, ImplicitInstance) -> do - b' <- checkPattern (arityParameter l) p - first (b' :) <$> goLhs r ps - (ImplicitInstance, Explicit {}) -> - throw - ( ErrWrongPatternIsImplicit - WrongPatternIsImplicit - { _wrongPatternIsImplicitExpected = Explicit, - _wrongPatternIsImplicitActual = p - } - ) - (ImplicitInstance, Implicit {}) -> do - wildcard <- genWildcard' Implicit - first (wildcard :) <$> goLhs r lhs - (Explicit, Implicit {}) -> do - wildcard <- genWildcard' Implicit - first (wildcard :) <$> goLhs r lhs - (Explicit, ImplicitInstance) -> do - wildcard <- genWildcard' ImplicitInstance - first (wildcard :) <$> goLhs r lhs - (Explicit, Explicit) -> do - p' <- checkPattern (l ^. arityParameterArity) p - first (p' :) <$> goLhs r ps - where - genWildcard' :: forall r'. (Members '[NameIdGen] r') => IsImplicit -> Sem r' PatternArg - genWildcard' = genWildcard loc - - -- This is an heuristic and it can have an undesired result. - -- Sometimes the outcome may even be confusing. - tailHelper :: Arity -> Maybe [IsImplicit] - tailHelper a - | 0 < pref = Just pref' - | otherwise = Nothing - where - pref' :: [IsImplicit] - pref' = map paramToImplicit (take pref (unfoldArity a)) - pref :: Int - pref = aI - targetI - preceedingImplicits :: Arity -> Int - preceedingImplicits = length . takeWhile (isImplicitOrInstance . (^. arityParameterImplicit)) . unfoldArity - aI :: Int - aI = preceedingImplicits a - targetI :: Int - targetI = preceedingImplicits guessedBody - paramToImplicit :: ArityParameter -> IsImplicit - paramToImplicit = (^. arityParameterImplicit) - -checkPattern :: - forall r. - (Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars, NameIdGen] r) => - Arity -> - PatternArg -> - Sem r PatternArg -checkPattern ari = traverseOf (patternArgName . each) nameAri >=> traverseOf patternArgPattern patternAri - where - nameAri :: VarName -> Sem r VarName - nameAri n = addArity n ari $> n - - patternAri :: Pattern -> Sem r Pattern - patternAri = \case - PatternVariable v -> addArity v ari $> PatternVariable v - PatternWildcardConstructor v -> PatternConstructorApp <$> checkWildcardConstructor v - PatternConstructorApp c -> case ari of - ArityUnit -> PatternConstructorApp <$> checkConstructorApp c - ArityUnknown -> PatternConstructorApp <$> checkConstructorApp c - ArityFunction {} -> - throw - ( ErrPatternFunction - PatternFunction - { _patternFunction = c - } - ) - -checkWildcardConstructor :: - forall r. - (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, State LocalVars] r) => - WildcardConstructor -> - Sem r ConstructorApp -checkWildcardConstructor w = do - let c = w ^. wildcardConstructor - numArgs <- length . constructorArgs . (^. constructorInfoType) <$> lookupConstructor c - holeArgs <- replicateM numArgs (genWildcard (getLoc w) Explicit) - return - ConstructorApp - { _constrAppConstructor = c, - _constrAppParameters = holeArgs, - _constrAppType = Nothing - } - -checkConstructorApp :: - forall r. - (Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars, NameIdGen] r) => - ConstructorApp -> - Sem r ConstructorApp -checkConstructorApp ca = do - let c = ca ^. constrAppConstructor - args <- constructorArgs . (^. constructorInfoType) <$> lookupConstructor c - let arities = map typeArity args - n = length arities - ps = ca ^. constrAppParameters - lps = length ps - when - (n /= lps) - ( throw - ( ErrWrongConstructorAppLength - WrongConstructorAppLength - { _wrongConstructorAppLength = ca, - _wrongConstructorAppLengthExpected = n - } - ) - ) - ps' <- zipWithM checkPattern arities ps - return (ConstructorApp c ps' Nothing) - -checkCase :: - forall r. - (Members '[Reader InsertedArgsStack, Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) => - Arity -> - Case -> - Sem r Case -checkCase ari l = do - _caseBranches <- mapM checkCaseBranch (l ^. caseBranches) - _caseExpression <- checkExpression ArityUnit (l ^. caseExpression) - let _caseParens = l ^. caseParens - _caseExpressionType :: Maybe Expression = Nothing - _caseExpressionWholeType :: Maybe Expression = Nothing - return Case {..} - where - checkCaseBranch :: CaseBranch -> Sem r CaseBranch - checkCaseBranch = traverseOf caseBranchExpression (checkExpression ari) - -checkLet :: - forall r. - (Members '[Reader InsertedArgsStack, Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) => - Arity -> - Let -> - Sem r Let -checkLet ari l = do - _letClauses <- mapM checkLetClause (l ^. letClauses) - _letExpression <- checkExpression ari (l ^. letExpression) - return Let {..} - where - checkLetClause :: LetClause -> Sem r LetClause - checkLetClause = \case - LetFunDef f -> LetFunDef <$> checkFunctionDef f - LetMutualBlock f -> LetMutualBlock <$> checkMutualBlockLet f - -checkLambda :: - forall r. - (Members '[Reader InsertedArgsStack, Error ArityCheckerError, Reader LocalVars, Reader InfoTable, NameIdGen] r) => - Arity -> - Lambda -> - Sem r Lambda -checkLambda ari l = do - let _lambdaType = l ^. lambdaType - _lambdaClauses <- mapM checkLambdaClause (l ^. lambdaClauses) - return Lambda {..} - where - checkLambdaClause :: - LambdaClause -> - Sem r LambdaClause - checkLambdaClause cl = do - hint <- guessArity (cl ^. lambdaBody) - (patterns', locals, bodyAri) <- checkLhs loc hint ari (toList (cl ^. lambdaPatterns)) - body' <- runReader locals (checkExpression bodyAri (cl ^. lambdaBody)) - return - LambdaClause - { _lambdaPatterns = nonEmpty' patterns', - _lambdaBody = body' - } - where - loc = getLoc cl - -idenArity :: (Members '[Reader LocalVars, Reader InfoTable] r) => Iden -> Sem r Arity -idenArity = \case - IdenVar v -> getLocalArity v - IdenInductive i -> typeArity <$> lookupInductiveType i - IdenFunction f -> do - fun <- (^. functionInfoDef) <$> lookupFunction f - let ari = typeArity (fun ^. funDefType) - defaults = fun ^. funDefArgsInfo - return (addArgsInfo defaults ari) - IdenConstructor c -> typeArity <$> lookupConstructorType c - IdenAxiom a -> typeArity . (^. axiomInfoDef . axiomType) <$> lookupAxiom a - -addArgsInfo :: [ArgInfo] -> Arity -> Arity -addArgsInfo = unfoldingArity . helper - where - helper :: [ArgInfo] -> UnfoldedArity -> UnfoldedArity - helper = over ufoldArityParams . go - - go :: [ArgInfo] -> [ArityParameter] -> [ArityParameter] - go infos params = case infos of - [] -> params - info : infos' -> case params of - [] -> impossible - para : params' -> - set arityParameterInfo info para : go infos' params' - --- | let x be some expression of type T. The argument of this function is T and it returns --- the arity of x. In other words, given (T : Type), it returns the arity of the elements of T. -typeArity :: Expression -> Arity -typeArity = go - where - go :: Expression -> Arity - go = \case - ExpressionIden i -> goIden i - ExpressionApplication a -> goApplication a - ExpressionLiteral {} -> ArityUnknown - ExpressionFunction f -> ArityFunction (goFun f) - ExpressionHole {} -> ArityUnknown - ExpressionInstanceHole {} -> ArityUnit - ExpressionLambda {} -> ArityUnknown - ExpressionCase {} -> ArityUnknown - ExpressionUniverse {} -> ArityUnit - ExpressionSimpleLambda {} -> simplelambda - ExpressionLet l -> goLet l - - goApplication :: Application -> Arity - goApplication a = case lhs of - ExpressionIden IdenInductive {} -> ArityUnit - _ -> ArityUnknown - where - lhs :: Expression - lhs = fst (unfoldApplication a) - - goLet :: Let -> Arity - goLet l = typeArity (l ^. letExpression) - - goIden :: Iden -> Arity - goIden = \case - IdenVar {} -> ArityUnknown - IdenInductive {} -> ArityUnit - IdenFunction {} -> ArityUnknown -- we need normalization to determine the arity - IdenConstructor {} -> ArityUnknown -- will be a type error - IdenAxiom {} -> ArityUnknown - - goParam :: FunctionParameter -> ArityParameter - goParam FunctionParameter {..} = - ArityParameter - { _arityParameterArity = case _paramImplicit of - Explicit -> go _paramType - Implicit -> go _paramType - ImplicitInstance -> ArityUnit, - _arityParameterImplicit = _paramImplicit, - _arityParameterInfo = emptyArgInfo - } - - goFun :: Function -> FunctionArity - goFun (Function l r) = - let l' = goParam l - r' = go r - in FunctionArity - { _functionArityLeft = l', - _functionArityRight = r' - } - -checkExample :: - forall r. - (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError, Reader LocalVars] r) => - Example -> - Sem r Example -checkExample = traverseOf exampleExpression (checkExpression ArityUnknown) - -checkExpression :: - forall r. - (Members '[Reader InsertedArgsStack, Reader InfoTable, NameIdGen, Error ArityCheckerError, Reader LocalVars] r) => - Arity -> - Expression -> - Sem r Expression -checkExpression hintArity expr = case expr of - ExpressionIden {} -> goApp expr [] - ExpressionApplication a -> uncurry goApp $ second toList (unfoldApplication' a) - ExpressionLiteral {} -> appHelper expr [] - ExpressionFunction f -> ExpressionFunction <$> goFunction f - ExpressionUniverse {} -> return expr - ExpressionHole {} -> return expr - ExpressionInstanceHole {} -> return expr - ExpressionSimpleLambda {} -> simplelambda - ExpressionLambda l -> ExpressionLambda <$> checkLambda hintArity l - ExpressionLet l -> ExpressionLet <$> checkLet hintArity l - ExpressionCase l -> ExpressionCase <$> checkCase hintArity l - where - goFunction :: Function -> Sem r Function - goFunction (Function l r) = do - l' <- goFunctionParameter l - let ari = typeArity (l' ^. paramType) - r' <- maybe id (withLocalVar ari) (l ^. paramName) (checkType r) - return (Function l' r') - where - goFunctionParameter :: FunctionParameter -> Sem r FunctionParameter - goFunctionParameter p = do - let _paramName = p ^. paramName - _paramImplicit = p ^. paramImplicit - _paramType <- checkType (p ^. paramType) - return FunctionParameter {..} - - goApp :: Expression -> [ApplicationArg] -> Sem r Expression - goApp f args = do - case f of - ExpressionIden (IdenAxiom n) -> do - blt <- getAxiomBuiltinInfo n - case blt of - Just BuiltinIOSequence -> goBuiltinApp n 0 2 f args - Just BuiltinTrace -> goBuiltinApp n 1 1 f args - _ -> appHelper f args - ExpressionIden (IdenFunction n) -> do - blt <- getFunctionBuiltinInfo n - case blt of - Just BuiltinBoolIf -> goBuiltinApp n 1 3 f args - Just BuiltinBoolOr -> goBuiltinApp n 0 2 f args - Just BuiltinBoolAnd -> goBuiltinApp n 0 2 f args - Just BuiltinSeq -> goBuiltinApp n 2 2 f args - _ -> appHelper f args - _ -> appHelper f args - - goBuiltinApp :: Name -> Int -> Int -> Expression -> [ApplicationArg] -> Sem r Expression - goBuiltinApp n implArgsNum argsNum f args = do - args' <- goImplArgs implArgsNum args - if - | length args' >= argsNum -> appHelper f args - | otherwise -> - throw $ - ErrBuiltinNotFullyApplied - BuiltinNotFullyApplied - { _builtinNotFullyAppliedName = n, - _builtinNotFullyAplliedExpectedArgsNum = argsNum - } - where - goImplArgs :: Int -> [ApplicationArg] -> Sem r [ApplicationArg] - goImplArgs 0 as = return as - goImplArgs k ((ApplicationArg Implicit _) : as) = goImplArgs (k - 1) as - goImplArgs _ as = return as - - appHelper :: Expression -> [ApplicationArg] -> Sem r Expression - appHelper fun0 args = do - (fun', args') :: (Expression, [ApplicationArg]) <- case fun0 of - ExpressionHole {} -> (fun0,) <$> mapM (traverseOf appArg (checkExpression ArityUnknown)) args - ExpressionInstanceHole {} -> (fun0,) <$> mapM (traverseOf appArg (checkExpression ArityUnknown)) args - ExpressionIden i -> (,[]) <$> goAppLeftIden i - ExpressionLiteral l -> (fun0,) <$> helper (getLoc l) arityLiteral - ExpressionUniverse l -> (fun0,) <$> helper (getLoc l) arityUniverse - ExpressionLambda l -> do - l' <- checkLambda ArityUnknown l - (ExpressionLambda l',) <$> helper (getLoc l') (arityLambda l') - ExpressionSimpleLambda {} -> simplelambda - ExpressionCase l -> do - l' <- checkCase ArityUnknown l - (ExpressionCase l',) <$> (arityCase l' >>= helper (getLoc l')) - ExpressionLet l -> do - l' <- checkLet ArityUnknown l - (ExpressionLet l',) <$> (arityLet l' >>= helper (getLoc l')) - ExpressionFunction f -> - throw - ( ErrFunctionApplied - FunctionApplied - { _functionAppliedFunction = f, - _functionAppliedArguments = args - } - ) - ExpressionApplication {} -> impossible - return (foldApplication fun' args') - where - goAppLeftIden :: Iden -> Sem r Expression - goAppLeftIden i = case i of - IdenFunction f -> do - infos <- (^. functionInfoDef . funDefArgsInfo) <$> lookupFunction f - let hasADefault = has (each . argInfoDefault . _Just) infos - if - | hasADefault -> goAppLeftIdenWithDefaults i - | otherwise -> noDefaults - _ -> noDefaults - where - noDefaults :: Sem r Expression - noDefaults = do - args' :: [ApplicationArg] <- map (^. insertedArg) <$> (idenArity i >>= helperDefaultArgs (getLoc i)) - return (foldApplication fun0 args') - - goAppLeftIdenWithDefaults :: Iden -> Sem r Expression - goAppLeftIdenWithDefaults i = do - namedArgs :: [InsertedArg] <- idenArity i >>= helperDefaultArgs (getLoc i) - case nonEmpty namedArgs of - Nothing -> return (toExpression i) - Just args' -> do - let mkClause :: InsertedArg -> Sem r Internal.PreLetStatement - mkClause InsertedArg {..} = do - -- TODO put actual type instead of hole? - let arg = _insertedArg - nm = _insertedArgName - ty <- mkFreshHole (getLoc arg) - return (Internal.PreLetFunctionDef (Internal.simpleFunDef nm ty (arg ^. appArg))) - mkAppArg :: InsertedArg -> ApplicationArg - mkAppArg InsertedArg {..} = - ApplicationArg - { _appArgIsImplicit = _insertedArg ^. appArgIsImplicit, - _appArg = toExpression _insertedArgName - } - clauses :: NonEmpty Internal.LetClause <- nonEmpty' . Internal.mkLetClauses <$> mapM mkClause args' - let app = foldApplication (toExpression fun0) (map mkAppArg namedArgs) - letexpr <- - Internal.substitutionE (renameKind KNameFunction (map (^. insertedArgName) namedArgs)) $ - ExpressionLet - Let - { _letClauses = clauses, - _letExpression = app - } - Internal.clone letexpr - - helper :: Interval -> Arity -> Sem r [ApplicationArg] - helper i ari = map (^. insertedArg) <$> helperDefaultArgs i ari - - helperDefaultArgs :: Interval -> Arity -> Sem r [InsertedArg] - helperDefaultArgs i ari = do - let argsAris :: [Arity] - argsAris = map arityParameter (unfoldArity ari) - argsWithHoles :: [InsertedArg] <- addHoles i hintArity ari args - let argsWithAris :: [(InsertedArg, Arity)] - argsWithAris = zip argsWithHoles (argsAris ++ repeat ArityUnknown) - forM argsWithAris $ \(ia, argAri) -> do - checkDefaultArgCycle ia - let adjustCtx - | ia ^. insertedArgDefault = over insertedArgsStack ((ia ^. insertedArgName) :) - | otherwise = id - local adjustCtx (traverseOf (insertedArg . appArg) (checkExpression argAri) ia) - where - checkDefaultArgCycle :: InsertedArg -> Sem r () - checkDefaultArgCycle ia = do - st <- asks (^. insertedArgsStack) - case span (/= (ia ^. insertedArgName)) st of - (_, []) -> return () - (c, _) -> - let cyc = NonEmpty.reverse (ia ^. insertedArgName :| c) - in throw (ErrDefaultArgCycle (DefaultArgCycle cyc)) - - addHoles :: - Interval -> - Arity -> - Arity -> - [ApplicationArg] -> - Sem r [InsertedArg] - addHoles loc hint ari0 = evalState 0 . execOutputList . go ari0 - where - go :: - Arity -> - [ApplicationArg] -> - Sem (Output InsertedArg ': State Int ': r) () - go ari goargs = do - let emitNoName :: Bool -> ApplicationArg -> Sem (Output InsertedArg ': State Int ': r) () - emitNoName isDef x = do - let l = getLoc x - v <- freshFunVar l "gen_helper" - emit isDef v x - emitWithParameter :: Bool -> ArityParameter -> ApplicationArg -> Sem (Output InsertedArg ': State Int ': r) () - emitWithParameter isDef p = maybe (emitNoName isDef) (emit isDef) (p ^. arityParameterName) - emitInstanceHole :: Sem (Output InsertedArg ': State Int ': r) () - emitInstanceHole = do - h <- newHoleInstance loc - emitNoName False (ApplicationArg ImplicitInstance (ExpressionInstanceHole h)) - emitImplicitHole :: ArityParameter -> Sem (Output InsertedArg ': State Int ': r) () - emitImplicitHole p = do - (isDef, h) <- newHoleImplicit p loc - emitWithParameter isDef p (ApplicationArg Implicit h) - emit :: Bool -> Name -> ApplicationArg -> Sem (Output InsertedArg ': State Int ': r) () - emit isDef n x = do - output - InsertedArg - { _insertedArg = x, - _insertedArgDefault = isDef, - _insertedArgName = n - } - modify' @Int succ - case (ari, goargs) of - (ArityFunction (FunctionArity (p@ArityParameter {_arityParameterImplicit = Implicit}) r), (ApplicationArg Implicit e) : rest) -> do - emitWithParameter False p (ApplicationArg Implicit e) - go r rest - (ArityFunction (FunctionArity (ArityParameter {_arityParameterImplicit = ImplicitInstance}) r), (ApplicationArg ImplicitInstance e) : rest) -> do - emitNoName False (ApplicationArg ImplicitInstance e) - go r rest - (ArityFunction (FunctionArity (p@ArityParameter {_arityParameterImplicit = Explicit}) r), (ApplicationArg Explicit e) : rest) -> do - emitWithParameter False p (ApplicationArg Explicit e) - go r rest - (ArityFunction (FunctionArity impl _), []) - -- When there are no remaining arguments and the expected arity of the - -- expression matches the current arity we should *not* insert a hole. - | arityParameterImplicitOrInstance impl - && ari == hint -> - return () - (ArityFunction (FunctionArity (p@ArityParameter {_arityParameterImplicit = Implicit}) r), _) -> do - -- h <- newHoleImplicit p loc - -- emitWithParameter p (ApplicationArg Implicit h) - emitImplicitHole p - go r goargs - (ArityFunction (FunctionArity (ArityParameter {_arityParameterImplicit = ImplicitInstance}) r), _) -> do - emitInstanceHole - go r goargs - (ArityFunction (FunctionArity (ArityParameter {_arityParameterImplicit = Explicit}) _), (ApplicationArg _ _) : _) -> do - idx <- get @Int - throw - ( ErrExpectedExplicitArgument - ExpectedExplicitArgument - { _expectedExplicitArgumentApp = (fun0, args), - _expectedExplicitArgumentIx = idx - } - ) - (ArityUnit, []) -> return () - (ArityFunction (FunctionArity (ArityParameter {_arityParameterImplicit = Explicit}) _), []) -> return () - (ArityUnit, _ : _) -> - throw - ( ErrTooManyArguments - TooManyArguments - { _tooManyArgumentsApp = (fun0, args), - _tooManyArgumentsUnexpected = length goargs - } - ) - (ArityUnknown, []) -> return () - (ArityUnknown, p : ps) -> do - emitNoName False p - go ArityUnknown ps - -newHoleImplicit :: (Member NameIdGen r) => ArityParameter -> Interval -> Sem r (Bool, Expression) -newHoleImplicit i loc = case i ^. arityParameterInfo . argInfoDefault of - Nothing -> (False,) . ExpressionHole . mkHole loc <$> freshNameId - Just e -> do - -- TODO update location - return (True, e) - -newHoleInstance :: (Member NameIdGen r) => Interval -> Sem r InstanceHole -newHoleInstance loc = mkInstanceHole loc <$> freshNameId diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data.hs deleted file mode 100644 index dac1f9dcb..000000000 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data.hs +++ /dev/null @@ -1,10 +0,0 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data - ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.LocalVars, - module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types, - module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context, - ) -where - -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.LocalVars -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Context.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Context.hs deleted file mode 100644 index b4180489f..000000000 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Context.hs +++ /dev/null @@ -1,23 +0,0 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context where - -import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context qualified as Scoped -import Juvix.Compiler.Internal.Language -import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context qualified as Internal -import Juvix.Compiler.Pipeline.EntryPoint qualified as E -import Juvix.Prelude - -data InternalArityResult = InternalArityResult - { _resultInternalResult :: Internal.InternalResult, - _resultModules :: NonEmpty Module - } - -makeLenses ''InternalArityResult - -mainModule :: Lens' InternalArityResult Module -mainModule = resultModules . _head1 - -internalArityResultEntryPoint :: Lens' InternalArityResult E.EntryPoint -internalArityResultEntryPoint = resultInternalResult . Internal.internalResultEntryPoint - -internalArityResultScoped :: Lens' InternalArityResult Scoped.ScoperResult -internalArityResultScoped = resultInternalResult . Internal.resultScoper diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/LocalVars.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/LocalVars.hs deleted file mode 100644 index a32594ee9..000000000 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/LocalVars.hs +++ /dev/null @@ -1,25 +0,0 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.LocalVars where - -import Data.HashMap.Strict qualified as HashMap -import Juvix.Compiler.Internal.Language -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types -import Juvix.Prelude - -newtype LocalVars = LocalVars - { _localArities :: HashMap VarName Arity - } - deriving newtype (Semigroup, Monoid) - -makeLenses ''LocalVars - -addArity :: (Member (State LocalVars) r) => VarName -> Arity -> Sem r () -addArity v t = modify (withArity v t) - -withArity :: VarName -> Arity -> LocalVars -> LocalVars -withArity v t = over localArities (HashMap.insert v t) - -getLocalArity :: (Member (Reader LocalVars) r) => VarName -> Sem r Arity -getLocalArity v = fromMaybe ArityUnknown <$> asks (^. localArities . at v) - -emptyLocalVars :: LocalVars -emptyLocalVars = mempty diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs deleted file mode 100644 index 89a6c9809..000000000 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Data/Types.hs +++ /dev/null @@ -1,149 +0,0 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types where - -import Juvix.Compiler.Internal.Extra.Base -import Juvix.Compiler.Internal.Language -import Juvix.Prelude -import Juvix.Prelude.Pretty - --- | Used to detect of cycles of default arguments in the arity checker. -newtype InsertedArgsStack = InsertedArgsStack - { _insertedArgsStack :: [Name] - } - deriving newtype (Monoid, Semigroup) - --- | Helper type used during insertion of default arguments in the arity --- checker. -data InsertedArg = InsertedArg - { _insertedArgName :: Name, - _insertedArg :: ApplicationArg, - -- | True if this corresponds to an automatically inserted default argument. - -- False if it is an inserted hole or an argument present in the source code. - _insertedArgDefault :: Bool - } - -data Arity - = ArityUnit - | ArityFunction FunctionArity - | ArityUnknown - deriving stock (Eq) - -data FunctionArity = FunctionArity - { _functionArityLeft :: ArityParameter, - _functionArityRight :: Arity - } - deriving stock (Eq) - -data ArityRest - = ArityRestUnit - | ArityRestUnknown - deriving stock (Eq) - -data UnfoldedArity = UnfoldedArity - { _ufoldArityParams :: [ArityParameter], - _ufoldArityRest :: ArityRest - } - deriving stock (Eq) - -data ArityParameter = ArityParameter - { _arityParameterArity :: Arity, - _arityParameterImplicit :: IsImplicit, - _arityParameterInfo :: ArgInfo - } - -instance Eq ArityParameter where - (ArityParameter ari impl _info) == (ArityParameter ari' impl' _info') = - (ari, impl) == (ari', impl') - -makeLenses ''UnfoldedArity -makeLenses ''InsertedArg -makeLenses ''ArityParameter -makeLenses ''InsertedArgsStack - -arityParameterName :: Lens' ArityParameter (Maybe Name) -arityParameterName = arityParameterInfo . argInfoName - -unfoldingArity :: (UnfoldedArity -> UnfoldedArity) -> Arity -> Arity -unfoldingArity f = foldArity . f . unfoldArity' - -arityParameter :: ArityParameter -> Arity -arityParameter = (^. arityParameterArity) - -arityParameterImplicitOrInstance :: ArityParameter -> Bool -arityParameterImplicitOrInstance a = case a ^. arityParameterImplicit of - Explicit {} -> False - Implicit {} -> True - ImplicitInstance -> True - -arityCommonPrefix :: Arity -> Arity -> [ArityParameter] -arityCommonPrefix p1 p2 = commonPrefix u1 u2 - where - u1 = unfoldArity p1 - u2 = unfoldArity p2 - -unfoldArity' :: Arity -> UnfoldedArity -unfoldArity' = \case - ArityUnit -> - UnfoldedArity - { _ufoldArityParams = [], - _ufoldArityRest = ArityRestUnit - } - ArityUnknown -> - UnfoldedArity - { _ufoldArityParams = [], - _ufoldArityRest = ArityRestUnknown - } - ArityFunction (FunctionArity l r) -> - over ufoldArityParams (l :) (unfoldArity' r) - -unfoldArity :: Arity -> [ArityParameter] -unfoldArity = (^. ufoldArityParams) . unfoldArity' - -foldArity :: UnfoldedArity -> Arity -foldArity UnfoldedArity {..} = go _ufoldArityParams - where - go :: [ArityParameter] -> Arity - go = \case - [] -> case _ufoldArityRest of - ArityRestUnit -> ArityUnit - ArityRestUnknown -> ArityUnknown - a : as -> ArityFunction (FunctionArity a (go as)) - -instance HasAtomicity FunctionArity where - atomicity = const (Aggregate funFixity) - -instance HasAtomicity Arity where - atomicity = \case - ArityUnit -> Atom - ArityUnknown -> Atom - ArityFunction f -> atomicity f - -instance Pretty ArityParameter where - pretty a = - let ari = arityParameter a - in case a ^. arityParameterImplicit of - Implicit -> "{" <> pretty ari <> "}" - ImplicitInstance -> "{{𝟙}}" - Explicit -> pretty ari - -instance HasAtomicity ArityParameter where - atomicity a = case a ^. arityParameterImplicit of - Explicit -> atomicity (a ^. arityParameterArity) - Implicit {} -> Atom - ImplicitInstance -> Atom - -instance Pretty FunctionArity where - pretty (FunctionArity l r) = - ppSide False l - <> " → " - <> ppSide True r - where - ppSide :: (HasAtomicity a, Pretty a) => Bool -> a -> Doc ann - ppSide isright lr = parensCond (atomParens (const isright) (atomicity lr) funFixity) (pretty lr) - parensCond :: Bool -> Doc a -> Doc a - parensCond t d = if t then parens d else d - -instance Pretty Arity where - pretty = \case - ArityUnit -> "𝟙" - ArityUnknown -> "?" - ArityFunction f -> pretty f diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs index 0d314d760..7bfe9db0b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs @@ -3,7 +3,6 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability (f import Juvix.Compiler.Internal.Data.NameDependencyInfo import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as Arity import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Typed import Juvix.Compiler.Pipeline.EntryPoint import Juvix.Prelude @@ -16,7 +15,7 @@ filterUnreachable r = do KeepAll -> return r FilterUnreachable -> return (set Typed.resultModules modules' r) where - depInfo = r ^. Typed.resultInternalArityResult . Arity.resultInternalResult . resultDepInfo + depInfo = r ^. Typed.resultInternalResult . resultDepInfo modules = r ^. Typed.resultModules modules' = run diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking.hs index 057f49c53..7b3aeb7a4 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking.hs @@ -1,12 +1,12 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking - ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Checker, + ( 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.FunctionsTable, module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context, ) where -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Checker +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.FunctionsTable import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs index 5af202871..a839b7ca4 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -166,9 +166,6 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do } ) -withEmptyVars :: Sem (Reader LocalVars ': r) a -> Sem r a -withEmptyVars = runReader emptyLocalVars - -- TODO should we register functions (type synonyms) first? checkTopMutualBlock :: (Members '[HighlightBuilder, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, Termination] r) => @@ -332,7 +329,7 @@ checkExample :: Example -> Sem r Example checkExample e = do - e' <- withEmptyVars (runInferenceDef (traverseOf exampleExpression (fmap (^. typedExpression) . inferExpression Nothing >=> strongNormalize) e)) + e' <- withEmptyLocalVars (runInferenceDef (traverseOf exampleExpression (fmap (^. typedExpression) . inferExpression Nothing >=> strongNormalize) e)) output e' return e' 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 6dd87e37f..7edaa3551 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -4,6 +4,10 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Ch checkTable, checkModuleIndex, checkModuleNoCache, + checkImport, + withEmptyInsertedArgsStack, + withEmptyLocalVars, + inferExpression, ) where @@ -138,11 +142,14 @@ checkModuleIndex :: Sem r ModuleIndex checkModuleIndex = fmap ModuleIndex . cacheGet +withEmptyInsertedArgsStack :: Sem (Reader InsertedArgsStack ': r) a -> Sem r a +withEmptyInsertedArgsStack = runReader (mempty @InsertedArgsStack) + checkModuleNoCache :: (Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache, Termination] r) => ModuleIndex -> Sem r Module -checkModuleNoCache (ModuleIndex Module {..}) = runReader (mempty @InsertedArgsStack) $ do +checkModuleNoCache (ModuleIndex Module {..}) = withEmptyInsertedArgsStack $ do _moduleBody' <- evalState (mempty :: NegativeTypeParameters) . checkModuleBody 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 3cd57a05b..c5654b0c2 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 @@ -8,8 +8,7 @@ where import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context qualified as Scoped import Juvix.Compiler.Internal.Data.InfoTable import Juvix.Compiler.Internal.Language -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context (InternalArityResult) -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as Arity +import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context qualified as Internal import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (TerminationState) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.FunctionsTable import Juvix.Compiler.Pipeline.EntryPoint qualified as E @@ -20,7 +19,7 @@ type TypesTable = HashMap NameId Expression type NormalizedTable = HashMap NameId Expression data InternalTypedResult = InternalTypedResult - { _resultInternalArityResult :: InternalArityResult, + { _resultInternalResult :: Internal.InternalResult, _resultModules :: NonEmpty Module, _resultTermination :: TerminationState, _resultNormalized :: NormalizedTable, @@ -35,7 +34,7 @@ mainModule :: Lens' InternalTypedResult Module mainModule = resultModules . _head1 internalTypedResultEntryPoint :: Lens' InternalTypedResult E.EntryPoint -internalTypedResultEntryPoint = resultInternalArityResult . Arity.internalArityResultEntryPoint +internalTypedResultEntryPoint = resultInternalResult . Internal.internalResultEntryPoint internalTypedResultScoped :: Lens' InternalTypedResult Scoped.ScoperResult -internalTypedResultScoped = resultInternalArityResult . Arity.internalArityResultScoped +internalTypedResultScoped = resultInternalResult . Internal.resultScoper diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Data.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Data.hs index 9402e5d34..82f1e9750 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Data.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Data.hs @@ -1,8 +1,6 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Data - ( Arity.InternalArityResult, - Typechecking.InternalTypedResult, + ( Typechecking.InternalTypedResult, ) where -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data qualified as Arity import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data qualified as Typechecking diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs index 619d9fb24..2a9739435 100644 --- a/src/Juvix/Compiler/Pipeline.hs +++ b/src/Juvix/Compiler/Pipeline.hs @@ -69,19 +69,10 @@ upToInternal :: Sem r Internal.InternalResult upToInternal = upToScoping >>= Internal.fromConcrete -upToInternalArity :: - (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, GitClone, PathResolver, Termination] r) => - Sem r Internal.InternalArityResult -upToInternalArity = upToInternal >>= Internal.arityChecking - upToInternalTyped :: (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, GitClone, PathResolver] r) => Sem r Internal.InternalTypedResult -upToInternalTyped = do - newAlgorithm <- asks (^. entryPointNewTypeCheckingAlgorithm) - if - | newAlgorithm -> Internal.typeCheckingNew upToInternal - | otherwise -> Internal.typeChecking upToInternalArity +upToInternalTyped = Internal.typeCheckingNew upToInternal upToInternalReachability :: (Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, GitClone, PathResolver] r) => diff --git a/src/Juvix/Compiler/Pipeline/EntryPoint.hs b/src/Juvix/Compiler/Pipeline/EntryPoint.hs index f9e0c08f1..3ecd9f480 100644 --- a/src/Juvix/Compiler/Pipeline/EntryPoint.hs +++ b/src/Juvix/Compiler/Pipeline/EntryPoint.hs @@ -38,8 +38,7 @@ data EntryPoint = EntryPoint _entryPointGenericOptions :: GenericOptions, _entryPointModulePaths :: [Path Abs File], _entryPointSymbolPruningMode :: SymbolPruningMode, - _entryPointOffline :: Bool, - _entryPointNewTypeCheckingAlgorithm :: Bool + _entryPointOffline :: Bool } deriving stock (Eq, Show) @@ -73,8 +72,7 @@ defaultEntryPointNoFile root = _entryPointInliningDepth = defaultInliningDepth, _entryPointModulePaths = [], _entryPointSymbolPruningMode = FilterUnreachable, - _entryPointOffline = False, - _entryPointNewTypeCheckingAlgorithm = False + _entryPointOffline = False } defaultUnrollLimit :: Int diff --git a/src/Juvix/Compiler/Pipeline/Repl.hs b/src/Juvix/Compiler/Pipeline/Repl.hs index cdfece57d..2f13b2d7f 100644 --- a/src/Juvix/Compiler/Pipeline/Repl.hs +++ b/src/Juvix/Compiler/Pipeline/Repl.hs @@ -23,18 +23,17 @@ import Juvix.Data.Effect.Process (runProcessIO) import Juvix.Data.Effect.TaggedLock import Juvix.Prelude -arityCheckExpression :: +upToInternalExpression :: (Members '[Error JuvixError, State Artifacts, Termination] r) => ExpressionAtoms 'Parsed -> Sem r Internal.Expression -arityCheckExpression p = do +upToInternalExpression p = do scopeTable <- gets (^. artifactScopeTable) runBuiltinsArtifacts . runScoperScopeArtifacts . runStateArtifacts artifactScoperState $ runNameIdGenArtifacts (Scoper.scopeCheckExpression scopeTable p) >>= runNameIdGenArtifacts . Internal.fromConcreteExpression - >>= Internal.arityCheckExpression expressionUpToAtomsParsed :: (Members '[State Artifacts, Error JuvixError] r) => @@ -111,7 +110,7 @@ importToInternalTyped :: (Members '[Reader EntryPoint, Error JuvixError, State Artifacts, Termination] r) => Internal.Import -> Sem r Internal.Import -importToInternalTyped = Internal.arityCheckImport >=> Internal.typeCheckImport +importToInternalTyped = Internal.typeCheckImport parseReplInput :: (Members '[PathResolver, Files, State Artifacts, Error JuvixError] r) => @@ -132,7 +131,7 @@ expressionUpToTyped :: expressionUpToTyped fp txt = do p <- expressionUpToAtomsParsed fp txt runTerminationArtifacts - ( arityCheckExpression p + ( upToInternalExpression p >>= Internal.typeCheckExpressionType ) @@ -142,7 +141,7 @@ compileExpression :: Sem r Core.Node compileExpression p = runTerminationArtifacts - ( arityCheckExpression p + ( upToInternalExpression p >>= Internal.typeCheckExpression ) >>= fromInternalExpression diff --git a/src/Juvix/Compiler/Pipeline/Run.hs b/src/Juvix/Compiler/Pipeline/Run.hs index d542967ff..6e020f716 100644 --- a/src/Juvix/Compiler/Pipeline/Run.hs +++ b/src/Juvix/Compiler/Pipeline/Run.hs @@ -15,7 +15,6 @@ import Juvix.Compiler.Concrete.Translation.FromSource qualified as P import Juvix.Compiler.Core.Data.InfoTable qualified as Core import Juvix.Compiler.Core.Translation.FromInternal.Data qualified as Core import Juvix.Compiler.Internal.Translation qualified as Internal -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as Arity import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qualified as Typed import Juvix.Compiler.Pipeline @@ -165,8 +164,7 @@ corePipelineIOEither' lockMode entry = do internalResult :: Internal.InternalResult internalResult = typedResult - ^. Typed.resultInternalArityResult - . Arity.resultInternalResult + ^. Typed.resultInternalResult coreTable :: Core.InfoTable coreTable = coreRes ^. Core.coreResultTable diff --git a/test/Arity.hs b/test/Arity.hs deleted file mode 100644 index bccf7b5c4..000000000 --- a/test/Arity.hs +++ /dev/null @@ -1,10 +0,0 @@ -module Arity - ( allTests, - ) -where - -import Arity.Negative qualified as N -import Base - -allTests :: TestTree -allTests = testGroup "Arity tests" [N.allTests] diff --git a/test/Arity/Negative.hs b/test/Arity/Negative.hs deleted file mode 100644 index ef27f1b7d..000000000 --- a/test/Arity/Negative.hs +++ /dev/null @@ -1,116 +0,0 @@ -module Arity.Negative where - -import Base -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error -import Juvix.Data.Effect.TaggedLock - -type FailMsg = String - -data NegTest = NegTest - { _name :: String, - _relDir :: Path Rel Dir, - _file :: Path Rel File, - _checkErr :: ArityCheckerError -> Maybe FailMsg - } - -testDescr :: NegTest -> TestDescr -testDescr NegTest {..} = - let tRoot = root _relDir - file' = tRoot _file - in TestDescr - { _testName = _name, - _testRoot = tRoot, - _testAssertion = Single $ do - entryPoint <- defaultEntryPointIO' LockModeExclusive tRoot file' - result <- runIOEitherTermination entryPoint upToInternalArity - case mapLeft fromJuvixError result of - Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure - Left Nothing -> assertFailure "The arity checker did not find an error." - Right _ -> assertFailure "An error ocurred but it was not in the arity checker." - } - -allTests :: TestTree -allTests = - testGroup - "Arity checker negative tests" - (map (mkTest . testDescr) tests) - -root :: Path Abs Dir -root = relToProject $(mkRelDir "tests/negative") - -wrongError :: Maybe FailMsg -wrongError = Just "Incorrect error" - -tests :: [NegTest] -tests = - [ NegTest - "Too many arguments in expression" - $(mkRelDir "Internal") - $(mkRelFile "TooManyArguments.juvix") - $ \case - ErrTooManyArguments {} -> Nothing - _ -> wrongError, - NegTest - "Pattern match a function type" - $(mkRelDir "Internal") - $(mkRelFile "FunctionPattern.juvix") - $ \case - ErrPatternFunction {} -> Nothing - _ -> wrongError, - NegTest - "Function type (* → *) application" - $(mkRelDir "Internal") - $(mkRelFile "FunctionApplied.juvix") - $ \case - ErrFunctionApplied {} -> Nothing - _ -> wrongError, - NegTest - "Expected explicit pattern" - $(mkRelDir "Internal") - $(mkRelFile "ExpectedExplicitPattern.juvix") - $ \case - ErrWrongPatternIsImplicit {} -> Nothing - _ -> wrongError, - NegTest - "Expected explicit argument" - $(mkRelDir "Internal") - $(mkRelFile "ExpectedExplicitArgument.juvix") - $ \case - ErrExpectedExplicitArgument {} -> Nothing - _ -> wrongError, - NegTest - "Function clause with two many patterns in the lhs" - $(mkRelDir "Internal") - $(mkRelFile "LhsTooManyPatterns.juvix") - $ \case - ErrLhsTooManyPatterns {} -> Nothing - _ -> wrongError, - NegTest - "Too many arguments for the return type of a constructor" - $(mkRelDir "Internal") - $(mkRelFile "WrongReturnTypeTooManyArguments.juvix") - $ \case - ErrTooManyArguments {} -> Nothing - _ -> wrongError, - NegTest - "Lazy builtin not fully applied" - $(mkRelDir "Internal") - $(mkRelFile "LazyBuiltin.juvix") - $ \case - ErrBuiltinNotFullyApplied {} -> Nothing - _ -> wrongError, - NegTest - "issue 2293: Non-terminating function with arity error" - $(mkRelDir "Internal") - $(mkRelFile "issue2293.juvix") - $ \case - ErrWrongConstructorAppLength {} -> Nothing - _ -> wrongError, - NegTest - "Detect default argument cycle in the arity checker" - $(mkRelDir "Internal") - $(mkRelFile "DefaultArgCycleArity.juvix") - $ \case - ErrDefaultArgCycle {} -> Nothing - _ -> wrongError - ] diff --git a/test/Compilation.hs b/test/Compilation.hs index 0da457bc1..0d8e28fd8 100644 --- a/test/Compilation.hs +++ b/test/Compilation.hs @@ -3,7 +3,6 @@ module Compilation where import Base import Compilation.Negative qualified as N import Compilation.Positive qualified as P -import Compilation.PositiveNew qualified as New allTests :: TestTree -allTests = testGroup "Juvix compilation pipeline tests" [New.allTestsNoOptimize, P.allTestsNoOptimize, P.allTests, N.allTests] +allTests = testGroup "Juvix compilation pipeline tests" [P.allTestsNoOptimize, P.allTests, N.allTests] diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs index 2e599b804..d4940892a 100644 --- a/test/Compilation/Positive.hs +++ b/test/Compilation/Positive.hs @@ -2,6 +2,7 @@ module Compilation.Positive where import Base import Compilation.Base +import Data.HashSet qualified as HashSet data PosTest = PosTest { _name :: String, @@ -60,362 +61,379 @@ posTest = posTest' EvalAndCompile posTestEval :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest posTestEval = posTest' EvalOnly +isIgnored :: PosTest -> Bool +isIgnored t = HashSet.member (t ^. name) ignored + +ignored :: HashSet String +ignored = + HashSet.fromList + [ -- TODO allow lambda branches of different number of patterns + "Test027: Church numerals" + ] + tests :: [PosTest] tests = - [ posTest - "Test001: Arithmetic operators" - $(mkRelDir ".") - $(mkRelFile "test001.juvix") - $(mkRelFile "out/test001.out"), - posTest - "Test002: Arithmetic operators inside lambdas" - $(mkRelDir ".") - $(mkRelFile "test002.juvix") - $(mkRelFile "out/test002.out"), - posTest - "Test003: Integer arithmetic" - $(mkRelDir ".") - $(mkRelFile "test003.juvix") - $(mkRelFile "out/test003.out"), - posTest - "Test004: IO builtins" - $(mkRelDir ".") - $(mkRelFile "test004.juvix") - $(mkRelFile "out/test004.out"), - posTest - "Test005: Higher-order functions" - $(mkRelDir ".") - $(mkRelFile "test005.juvix") - $(mkRelFile "out/test005.out"), - posTest - "Test006: If-then-else and lazy boolean operators" - $(mkRelDir ".") - $(mkRelFile "test006.juvix") - $(mkRelFile "out/test006.out"), - posTest - "Test007: Pattern matching and lambda-case" - $(mkRelDir ".") - $(mkRelFile "test007.juvix") - $(mkRelFile "out/test007.out"), - posTest - "Test008: Recursion" - $(mkRelDir ".") - $(mkRelFile "test008.juvix") - $(mkRelFile "out/test008.out"), - posTest - "Test009: Tail recursion" - $(mkRelDir ".") - $(mkRelFile "test009.juvix") - $(mkRelFile "out/test009.out"), - posTest - "Test010: Let" - $(mkRelDir ".") - $(mkRelFile "test010.juvix") - $(mkRelFile "out/test010.out"), - posTestEval - "Test011: Tail recursion: Fibonacci numbers in linear time" - $(mkRelDir ".") - $(mkRelFile "test011.juvix") - $(mkRelFile "out/test011.out"), - posTest - "Test012: Trees" - $(mkRelDir ".") - $(mkRelFile "test012.juvix") - $(mkRelFile "out/test012.out"), - posTest - "Test013: Functions returning functions with variable capture" - $(mkRelDir ".") - $(mkRelFile "test013.juvix") - $(mkRelFile "out/test013.out"), - posTest - "Test014: Arithmetic" - $(mkRelDir ".") - $(mkRelFile "test014.juvix") - $(mkRelFile "out/test014.out"), - posTest - "Test015: Local functions with free variables" - $(mkRelDir ".") - $(mkRelFile "test015.juvix") - $(mkRelFile "out/test015.out"), - posTest - "Test016: Recursion through higher-order functions" - $(mkRelDir ".") - $(mkRelFile "test016.juvix") - $(mkRelFile "out/test016.out"), - posTest - "Test017: Tail recursion through higher-order functions" - $(mkRelDir ".") - $(mkRelFile "test017.juvix") - $(mkRelFile "out/test017.out"), - posTest - "Test018: Higher-order functions and recursion" - $(mkRelDir ".") - $(mkRelFile "test018.juvix") - $(mkRelFile "out/test018.out"), - posTest - "Test019: Self-application" - $(mkRelDir ".") - $(mkRelFile "test019.juvix") - $(mkRelFile "out/test019.out"), - posTest - "Test020: Recursive functions: McCarthy's 91 function, subtraction by increments" - $(mkRelDir ".") - $(mkRelFile "test020.juvix") - $(mkRelFile "out/test020.out"), - posTest - "Test021: Fast exponentiation" - $(mkRelDir ".") - $(mkRelFile "test021.juvix") - $(mkRelFile "out/test021.out"), - posTest - "Test022: Lists" - $(mkRelDir ".") - $(mkRelFile "test022.juvix") - $(mkRelFile "out/test022.out"), - posTest - "Test023: Mutual recursion" - $(mkRelDir ".") - $(mkRelFile "test023.juvix") - $(mkRelFile "out/test023.out"), - posTest - "Test024: Nested binders with variable capture" - $(mkRelDir ".") - $(mkRelFile "test024.juvix") - $(mkRelFile "out/test024.out"), - posTest - "Test025: Euclid's algorithm" - $(mkRelDir ".") - $(mkRelFile "test025.juvix") - $(mkRelFile "out/test025.out"), - posTest - "Test026: Functional queues" - $(mkRelDir ".") - $(mkRelFile "test026.juvix") - $(mkRelFile "out/test026.out"), - posTest - "Test027: Church numerals" - $(mkRelDir ".") - $(mkRelFile "test027.juvix") - $(mkRelFile "out/test027.out"), - posTest - "Test028: Streams without memoization" - $(mkRelDir ".") - $(mkRelFile "test028.juvix") - $(mkRelFile "out/test028.out"), - posTest - "Test029: Ackermann function" - $(mkRelDir ".") - $(mkRelFile "test029.juvix") - $(mkRelFile "out/test029.out"), - posTest - "Test030: Ackermann function (higher-order definition)" - $(mkRelDir ".") - $(mkRelFile "test030.juvix") - $(mkRelFile "out/test030.out"), - posTest - "Test031: Nested lists" - $(mkRelDir ".") - $(mkRelFile "test031.juvix") - $(mkRelFile "out/test031.out"), - posTest - "Test032: Merge sort" - $(mkRelDir ".") - $(mkRelFile "test032.juvix") - $(mkRelFile "out/test032.out"), - posTest - "Test033: Eta-expansion of builtins and constructors" - $(mkRelDir ".") - $(mkRelFile "test033.juvix") - $(mkRelFile "out/test033.out"), - posTest - "Test034: Recursive let" - $(mkRelDir ".") - $(mkRelFile "test034.juvix") - $(mkRelFile "out/test034.out"), - posTest - "Test035: Pattern matching" - $(mkRelDir ".") - $(mkRelFile "test035.juvix") - $(mkRelFile "out/test035.out"), - posTest - "Test036: Eta-expansion" - $(mkRelDir ".") - $(mkRelFile "test036.juvix") - $(mkRelFile "out/test036.out"), - posTest - "Test037: Applications with lets and cases in function position" - $(mkRelDir ".") - $(mkRelFile "test037.juvix") - $(mkRelFile "out/test037.out"), - posTest - "Test038: Simple case expression" - $(mkRelDir ".") - $(mkRelFile "test038.juvix") - $(mkRelFile "out/test038.out"), - posTest - "Test039: Mutually recursive let expression" - $(mkRelDir ".") - $(mkRelFile "test039.juvix") - $(mkRelFile "out/test039.out"), - posTest - "Test040: Pattern matching nullary constructor" - $(mkRelDir ".") - $(mkRelFile "test040.juvix") - $(mkRelFile "out/test040.out"), - posTest - "Test041: Use a builtin inductive in an inductive constructor" - $(mkRelDir ".") - $(mkRelFile "test041.juvix") - $(mkRelFile "out/test041.out"), - posTest - "Test042: Builtin string-to-nat" - $(mkRelDir ".") - $(mkRelFile "test042.juvix") - $(mkRelFile "out/test042.out"), - posTest - "Test043: Builtin trace" - $(mkRelDir ".") - $(mkRelFile "test043.juvix") - $(mkRelFile "out/test043.out"), - posTestStdin - "Test044: Builtin readline" - $(mkRelDir ".") - $(mkRelFile "test044.juvix") - $(mkRelFile "out/test044.out") - "a\n", - posTest - "Test045: Implicit builtin bool" - $(mkRelDir ".") - $(mkRelFile "test045.juvix") - $(mkRelFile "out/test045.out"), - posTest - "Test046: Polymorphic type arguments" - $(mkRelDir ".") - $(mkRelFile "test046.juvix") - $(mkRelFile "out/test046.out"), - posTest - "Test047: Local Modules" - $(mkRelDir ".") - $(mkRelFile "test047.juvix") - $(mkRelFile "out/test047.out"), - posTest - "Test048: String quoting" - $(mkRelDir ".") - $(mkRelFile "test048.juvix") - $(mkRelFile "out/test048.out"), - posTest - "Test049: Builtin Int" - $(mkRelDir ".") - $(mkRelFile "test049.juvix") - $(mkRelFile "out/test049.out"), - posTest - "Test050: Pattern matching with integers" - $(mkRelDir ".") - $(mkRelFile "test050.juvix") - $(mkRelFile "out/test050.out"), - posTest - "Test051: Local recursive function using IO >>" - $(mkRelDir ".") - $(mkRelFile "test051.juvix") - $(mkRelFile "out/test051.out"), - posTest - "Test052: Simple lambda calculus" - $(mkRelDir ".") - $(mkRelFile "test052.juvix") - $(mkRelFile "out/test052.out"), - posTest - "Test053: Inlining" - $(mkRelDir ".") - $(mkRelFile "test053.juvix") - $(mkRelFile "out/test053.out"), - posTest - "Test054: Iterators" - $(mkRelDir ".") - $(mkRelFile "test054.juvix") - $(mkRelFile "out/test054.out"), - posTest - "Test055: Constructor printing" - $(mkRelDir ".") - $(mkRelFile "test055.juvix") - $(mkRelFile "out/test055.out"), - posTest - "Test056: Argument specialization" - $(mkRelDir ".") - $(mkRelFile "test056.juvix") - $(mkRelFile "out/test056.out"), - posTest - "Test057: Case folding" - $(mkRelDir ".") - $(mkRelFile "test057.juvix") - $(mkRelFile "out/test057.out"), - posTest - "Test058: Ranges" - $(mkRelDir ".") - $(mkRelFile "test058.juvix") - $(mkRelFile "out/test058.out"), - posTest - "Test059: Builtin list" - $(mkRelDir ".") - $(mkRelFile "test059.juvix") - $(mkRelFile "out/test059.out"), - posTest - "Test060: Record update" - $(mkRelDir ".") - $(mkRelFile "test060.juvix") - $(mkRelFile "out/test060.out"), - posTest - "Test061: Traits" - $(mkRelDir ".") - $(mkRelFile "test061.juvix") - $(mkRelFile "out/test061.out"), - posTest - "Test062: Overapplication" - $(mkRelDir ".") - $(mkRelFile "test062.juvix") - $(mkRelFile "out/test062.out"), - posTest - "Test063: Coercions" - $(mkRelDir ".") - $(mkRelFile "test063.juvix") - $(mkRelFile "out/test063.out"), - posTest - "Test064: Constant folding" - $(mkRelDir ".") - $(mkRelFile "test064.juvix") - $(mkRelFile "out/test064.out"), - posTest - "Test065: Arithmetic simplification" - $(mkRelDir ".") - $(mkRelFile "test065.juvix") - $(mkRelFile "out/test065.out"), - posTest - "Test066: Import function with a function call in default argument" - $(mkRelDir "test066") - $(mkRelFile "M.juvix") - $(mkRelFile "out/test066.out"), - posTest - "Test067: Dependent default values inserted during translation FromConcrete" - $(mkRelDir ".") - $(mkRelFile "test067.juvix") - $(mkRelFile "out/test067.out"), - posTest - "Test068: Dependent default values inserted in the arity checker" - $(mkRelDir ".") - $(mkRelFile "test068.juvix") - $(mkRelFile "out/test068.out"), - posTest - "Test069: Dependent default values for Ord trait" - $(mkRelDir ".") - $(mkRelFile "test069.juvix") - $(mkRelFile "out/test069.out"), - posTest - "Test070: Nested default values and named arguments" - $(mkRelDir ".") - $(mkRelFile "test070.juvix") - $(mkRelFile "out/test070.out"), - posTest - "Test071: Named application (Ord instance with default cmp)" - $(mkRelDir ".") - $(mkRelFile "test071.juvix") - $(mkRelFile "out/test071.out") - ] + filter + (not . isIgnored) + [ posTest + "Test001: Arithmetic operators" + $(mkRelDir ".") + $(mkRelFile "test001.juvix") + $(mkRelFile "out/test001.out"), + posTest + "Test002: Arithmetic operators inside lambdas" + $(mkRelDir ".") + $(mkRelFile "test002.juvix") + $(mkRelFile "out/test002.out"), + posTest + "Test003: Integer arithmetic" + $(mkRelDir ".") + $(mkRelFile "test003.juvix") + $(mkRelFile "out/test003.out"), + posTest + "Test004: IO builtins" + $(mkRelDir ".") + $(mkRelFile "test004.juvix") + $(mkRelFile "out/test004.out"), + posTest + "Test005: Higher-order functions" + $(mkRelDir ".") + $(mkRelFile "test005.juvix") + $(mkRelFile "out/test005.out"), + posTest + "Test006: If-then-else and lazy boolean operators" + $(mkRelDir ".") + $(mkRelFile "test006.juvix") + $(mkRelFile "out/test006.out"), + posTest + "Test007: Pattern matching and lambda-case" + $(mkRelDir ".") + $(mkRelFile "test007.juvix") + $(mkRelFile "out/test007.out"), + posTest + "Test008: Recursion" + $(mkRelDir ".") + $(mkRelFile "test008.juvix") + $(mkRelFile "out/test008.out"), + posTest + "Test009: Tail recursion" + $(mkRelDir ".") + $(mkRelFile "test009.juvix") + $(mkRelFile "out/test009.out"), + posTest + "Test010: Let" + $(mkRelDir ".") + $(mkRelFile "test010.juvix") + $(mkRelFile "out/test010.out"), + posTestEval + "Test011: Tail recursion: Fibonacci numbers in linear time" + $(mkRelDir ".") + $(mkRelFile "test011.juvix") + $(mkRelFile "out/test011.out"), + posTest + "Test012: Trees" + $(mkRelDir ".") + $(mkRelFile "test012.juvix") + $(mkRelFile "out/test012.out"), + posTest + "Test013: Functions returning functions with variable capture" + $(mkRelDir ".") + $(mkRelFile "test013.juvix") + $(mkRelFile "out/test013.out"), + posTest + "Test014: Arithmetic" + $(mkRelDir ".") + $(mkRelFile "test014.juvix") + $(mkRelFile "out/test014.out"), + posTest + "Test015: Local functions with free variables" + $(mkRelDir ".") + $(mkRelFile "test015.juvix") + $(mkRelFile "out/test015.out"), + posTest + "Test016: Recursion through higher-order functions" + $(mkRelDir ".") + $(mkRelFile "test016.juvix") + $(mkRelFile "out/test016.out"), + posTest + "Test017: Tail recursion through higher-order functions" + $(mkRelDir ".") + $(mkRelFile "test017.juvix") + $(mkRelFile "out/test017.out"), + posTest + "Test018: Higher-order functions and recursion" + $(mkRelDir ".") + $(mkRelFile "test018.juvix") + $(mkRelFile "out/test018.out"), + posTest + "Test019: Self-application" + $(mkRelDir ".") + $(mkRelFile "test019.juvix") + $(mkRelFile "out/test019.out"), + posTest + "Test020: Recursive functions: McCarthy's 91 function, subtraction by increments" + $(mkRelDir ".") + $(mkRelFile "test020.juvix") + $(mkRelFile "out/test020.out"), + posTest + "Test021: Fast exponentiation" + $(mkRelDir ".") + $(mkRelFile "test021.juvix") + $(mkRelFile "out/test021.out"), + posTest + "Test022: Lists" + $(mkRelDir ".") + $(mkRelFile "test022.juvix") + $(mkRelFile "out/test022.out"), + posTest + "Test023: Mutual recursion" + $(mkRelDir ".") + $(mkRelFile "test023.juvix") + $(mkRelFile "out/test023.out"), + posTest + "Test024: Nested binders with variable capture" + $(mkRelDir ".") + $(mkRelFile "test024.juvix") + $(mkRelFile "out/test024.out"), + posTest + "Test025: Euclid's algorithm" + $(mkRelDir ".") + $(mkRelFile "test025.juvix") + $(mkRelFile "out/test025.out"), + posTest + "Test026: Functional queues" + $(mkRelDir ".") + $(mkRelFile "test026.juvix") + $(mkRelFile "out/test026.out"), + posTest + "Test027: Church numerals" + $(mkRelDir ".") + $(mkRelFile "test027.juvix") + $(mkRelFile "out/test027.out"), + posTest + "Test028: Streams without memoization" + $(mkRelDir ".") + $(mkRelFile "test028.juvix") + $(mkRelFile "out/test028.out"), + posTest + "Test029: Ackermann function" + $(mkRelDir ".") + $(mkRelFile "test029.juvix") + $(mkRelFile "out/test029.out"), + posTest + "Test030: Ackermann function (higher-order definition)" + $(mkRelDir ".") + $(mkRelFile "test030.juvix") + $(mkRelFile "out/test030.out"), + posTest + "Test031: Nested lists" + $(mkRelDir ".") + $(mkRelFile "test031.juvix") + $(mkRelFile "out/test031.out"), + posTest + "Test032: Merge sort" + $(mkRelDir ".") + $(mkRelFile "test032.juvix") + $(mkRelFile "out/test032.out"), + posTest + "Test033: Eta-expansion of builtins and constructors" + $(mkRelDir ".") + $(mkRelFile "test033.juvix") + $(mkRelFile "out/test033.out"), + posTest + "Test034: Recursive let" + $(mkRelDir ".") + $(mkRelFile "test034.juvix") + $(mkRelFile "out/test034.out"), + posTest + "Test035: Pattern matching" + $(mkRelDir ".") + $(mkRelFile "test035.juvix") + $(mkRelFile "out/test035.out"), + posTest + "Test036: Eta-expansion" + $(mkRelDir ".") + $(mkRelFile "test036.juvix") + $(mkRelFile "out/test036.out"), + posTest + "Test037: Applications with lets and cases in function position" + $(mkRelDir ".") + $(mkRelFile "test037.juvix") + $(mkRelFile "out/test037.out"), + posTest + "Test038: Simple case expression" + $(mkRelDir ".") + $(mkRelFile "test038.juvix") + $(mkRelFile "out/test038.out"), + posTest + "Test039: Mutually recursive let expression" + $(mkRelDir ".") + $(mkRelFile "test039.juvix") + $(mkRelFile "out/test039.out"), + posTest + "Test040: Pattern matching nullary constructor" + $(mkRelDir ".") + $(mkRelFile "test040.juvix") + $(mkRelFile "out/test040.out"), + posTest + "Test041: Use a builtin inductive in an inductive constructor" + $(mkRelDir ".") + $(mkRelFile "test041.juvix") + $(mkRelFile "out/test041.out"), + posTest + "Test042: Builtin string-to-nat" + $(mkRelDir ".") + $(mkRelFile "test042.juvix") + $(mkRelFile "out/test042.out"), + posTest + "Test043: Builtin trace" + $(mkRelDir ".") + $(mkRelFile "test043.juvix") + $(mkRelFile "out/test043.out"), + posTestStdin + "Test044: Builtin readline" + $(mkRelDir ".") + $(mkRelFile "test044.juvix") + $(mkRelFile "out/test044.out") + "a\n", + posTest + "Test045: Implicit builtin bool" + $(mkRelDir ".") + $(mkRelFile "test045.juvix") + $(mkRelFile "out/test045.out"), + posTest + "Test046: Polymorphic type arguments" + $(mkRelDir ".") + $(mkRelFile "test046.juvix") + $(mkRelFile "out/test046.out"), + posTest + "Test047: Local Modules" + $(mkRelDir ".") + $(mkRelFile "test047.juvix") + $(mkRelFile "out/test047.out"), + posTest + "Test048: String quoting" + $(mkRelDir ".") + $(mkRelFile "test048.juvix") + $(mkRelFile "out/test048.out"), + posTest + "Test049: Builtin Int" + $(mkRelDir ".") + $(mkRelFile "test049.juvix") + $(mkRelFile "out/test049.out"), + posTest + "Test050: Pattern matching with integers" + $(mkRelDir ".") + $(mkRelFile "test050.juvix") + $(mkRelFile "out/test050.out"), + posTest + "Test051: Local recursive function using IO >>" + $(mkRelDir ".") + $(mkRelFile "test051.juvix") + $(mkRelFile "out/test051.out"), + posTest + "Test052: Simple lambda calculus" + $(mkRelDir ".") + $(mkRelFile "test052.juvix") + $(mkRelFile "out/test052.out"), + posTest + "Test053: Inlining" + $(mkRelDir ".") + $(mkRelFile "test053.juvix") + $(mkRelFile "out/test053.out"), + posTest + "Test054: Iterators" + $(mkRelDir ".") + $(mkRelFile "test054.juvix") + $(mkRelFile "out/test054.out"), + posTest + "Test055: Constructor printing" + $(mkRelDir ".") + $(mkRelFile "test055.juvix") + $(mkRelFile "out/test055.out"), + posTest + "Test056: Argument specialization" + $(mkRelDir ".") + $(mkRelFile "test056.juvix") + $(mkRelFile "out/test056.out"), + posTest + "Test057: Case folding" + $(mkRelDir ".") + $(mkRelFile "test057.juvix") + $(mkRelFile "out/test057.out"), + posTest + "Test058: Ranges" + $(mkRelDir ".") + $(mkRelFile "test058.juvix") + $(mkRelFile "out/test058.out"), + posTest + "Test059: Builtin list" + $(mkRelDir ".") + $(mkRelFile "test059.juvix") + $(mkRelFile "out/test059.out"), + posTest + "Test060: Record update" + $(mkRelDir ".") + $(mkRelFile "test060.juvix") + $(mkRelFile "out/test060.out"), + posTest + "Test061: Traits" + $(mkRelDir ".") + $(mkRelFile "test061.juvix") + $(mkRelFile "out/test061.out"), + posTest + "Test062: Overapplication" + $(mkRelDir ".") + $(mkRelFile "test062.juvix") + $(mkRelFile "out/test062.out"), + posTest + "Test063: Coercions" + $(mkRelDir ".") + $(mkRelFile "test063.juvix") + $(mkRelFile "out/test063.out"), + posTest + "Test064: Constant folding" + $(mkRelDir ".") + $(mkRelFile "test064.juvix") + $(mkRelFile "out/test064.out"), + posTest + "Test065: Arithmetic simplification" + $(mkRelDir ".") + $(mkRelFile "test065.juvix") + $(mkRelFile "out/test065.out"), + posTest + "Test066: Import function with a function call in default argument" + $(mkRelDir "test066") + $(mkRelFile "M.juvix") + $(mkRelFile "out/test066.out"), + posTest + "Test067: Dependent default values inserted during translation FromConcrete" + $(mkRelDir ".") + $(mkRelFile "test067.juvix") + $(mkRelFile "out/test067.out"), + posTest + "Test068: Dependent default values inserted in the arity checker" + $(mkRelDir ".") + $(mkRelFile "test068.juvix") + $(mkRelFile "out/test068.out"), + posTest + "Test069: Dependent default values for Ord trait" + $(mkRelDir ".") + $(mkRelFile "test069.juvix") + $(mkRelFile "out/test069.out"), + posTest + "Test070: Nested default values and named arguments" + $(mkRelDir ".") + $(mkRelFile "test070.juvix") + $(mkRelFile "out/test070.out"), + posTest + "Test071: Named application (Ord instance with default cmp)" + $(mkRelDir ".") + $(mkRelFile "test071.juvix") + $(mkRelFile "out/test071.out"), + posTest + "Test072: Monad transformers (ReaderT + StateT + Identity)" + $(mkRelDir "test072") + $(mkRelFile "ReaderT.juvix") + $(mkRelFile "out/test072.out") + ] diff --git a/test/Compilation/PositiveNew.hs b/test/Compilation/PositiveNew.hs deleted file mode 100644 index 154cd3574..000000000 --- a/test/Compilation/PositiveNew.hs +++ /dev/null @@ -1,56 +0,0 @@ -module Compilation.PositiveNew where - -import Base -import Compilation.Base -import Compilation.Positive qualified as Old -import Data.HashSet qualified as HashSet - -root :: Path Abs Dir -root = relToProject $(mkRelDir "tests/positive") - -posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> Old.PosTest -posTest = posTest' EvalAndCompile - -posTest' :: CompileAssertionMode -> String -> Path Rel Dir -> Path Rel File -> Path Rel File -> Old.PosTest -posTest' _assertionMode _name rdir rfile routfile = - let _dir = root rdir - _file = _dir rfile - _expectedFile = root routfile - in Old.PosTest {..} - -testDescr :: Int -> Old.PosTest -> TestDescr -testDescr optLevel Old.PosTest {..} = - TestDescr - { _testName = _name, - _testRoot = _dir, - _testAssertion = - Steps $ - let f = set entryPointNewTypeCheckingAlgorithm True - in compileAssertionEntry f _dir optLevel _assertionMode _file _expectedFile - } - -allTestsNoOptimize :: TestTree -allTestsNoOptimize = - testGroup - "New typechecker compilation positive tests (no optimization)" - (map (mkTest . testDescr 0) (filter (not . isIgnored) (extraTests <> Old.tests))) - -isIgnored :: Old.PosTest -> Bool -isIgnored t = HashSet.member (t ^. Old.name) ignored - -extraTests :: [Old.PosTest] -extraTests = - [ Old.posTest - "Test073: Monad transformers (ReaderT + StateT + Identity)" - $(mkRelDir "test072") - $(mkRelFile "ReaderT.juvix") - $(mkRelFile "out/test072.out") - ] - -ignored :: HashSet String -ignored = - HashSet.fromList - [ "Test046: Polymorphic type arguments", - -- TODO allow lambda branches of different number of patterns - "Test027: Church numerals" - ] diff --git a/test/Main.hs b/test/Main.hs index 787cf6a61..79acfdca1 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -1,6 +1,5 @@ module Main (main) where -import Arity qualified import Asm qualified import BackendGeb qualified import BackendMarkdown qualified @@ -41,7 +40,6 @@ fastTests = [ Parsing.allTests, Scope.allTests, Termination.allTests, - Arity.allTests, Typecheck.allTests, Reachability.allTests, Format.allTests, diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index a437def22..b18a9f1e6 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -380,13 +380,6 @@ scoperErrorTests = $ \case ErrWrongDefaultValue {} -> Nothing _ -> wrongError, - NegTest - "Unsupported type" - $(mkRelDir ".") - $(mkRelFile "UnsupportedType.juvix") - $ \case - ErrUnsupported {} -> Nothing - _ -> wrongError, NegTest "Default argument cycle in FromConcrete" $(mkRelDir ".") diff --git a/test/Typecheck.hs b/test/Typecheck.hs index d4def3866..9a39ab272 100644 --- a/test/Typecheck.hs +++ b/test/Typecheck.hs @@ -2,9 +2,7 @@ module Typecheck (allTests) where import Base import Typecheck.Negative qualified as N -import Typecheck.NegativeNew qualified as NewNeg import Typecheck.Positive qualified as P -import Typecheck.PositiveNew qualified as New allTests :: TestTree -allTests = testGroup "Type checker tests" [New.allTests, P.allTests, N.allTests, NewNeg.allTests] +allTests = testGroup "Type checker tests" [P.allTests, N.allTests] diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs index 5cc4e3945..f2be76999 100644 --- a/test/Typecheck/NegativeNew.hs +++ b/test/Typecheck/NegativeNew.hs @@ -30,7 +30,7 @@ testDescr Old.NegTest {..} = { _testName = _name, _testRoot = tRoot, _testAssertion = Single $ do - entryPoint <- set entryPointNewTypeCheckingAlgorithm True <$> defaultEntryPointIO' LockModeExclusive tRoot file' + entryPoint <- defaultEntryPointIO' LockModeExclusive tRoot file' result <- runIOEither' LockModeExclusive entryPoint upToCore case mapLeft fromJuvixError result of Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure diff --git a/test/Typecheck/PositiveNew.hs b/test/Typecheck/PositiveNew.hs deleted file mode 100644 index bec2e5a9c..000000000 --- a/test/Typecheck/PositiveNew.hs +++ /dev/null @@ -1,48 +0,0 @@ -module Typecheck.PositiveNew where - -import Base -import Data.HashSet qualified as HashSet -import Juvix.Data.Effect.TaggedLock -import Typecheck.Positive qualified as Old - -root :: Path Abs Dir -root = relToProject $(mkRelDir "tests/positive") - -posTest :: String -> Path Rel Dir -> Path Rel File -> Old.PosTest -posTest _name rdir rfile = - let _dir = root rdir - _file = _dir rfile - in Old.PosTest {..} - -testDescr :: Old.PosTest -> TestDescr -testDescr Old.PosTest {..} = - TestDescr - { _testName = _name, - _testRoot = _dir, - _testAssertion = Single $ do - entryPoint <- set entryPointNewTypeCheckingAlgorithm True <$> defaultEntryPointIO' LockModeExclusive _dir _file - (void . runIOExclusive entryPoint) upToInternalTyped - } - -allTests :: TestTree -allTests = - testGroup - "New typechecker positive tests" - [ testGroup - "New typechecker General typechecking tests" - (map (mkTest . testDescr) (filter (not . isIgnored) (extraTests <> Old.tests))) - ] - -isIgnored :: Old.PosTest -> Bool -isIgnored t = HashSet.member (t ^. Old.name) ignored - -extraTests :: [Old.PosTest] -extraTests = [] - --- | Default values are not supported by the new type checker at the moment -ignored :: HashSet String -ignored = - HashSet.fromList - [ -- This test does not pass with the new hole insertion algorithm - "Test046: Polymorphic type arguments" - ] diff --git a/tests/Compilation/positive/test046.juvix b/tests/Compilation/positive/test046.juvix index 839b3573e..ff692742f 100644 --- a/tests/Compilation/positive/test046.juvix +++ b/tests/Compilation/positive/test046.juvix @@ -1,13 +1,17 @@ -- polymorphic type arguments module test046; -import Stdlib.Prelude open; +import Stdlib.Data.Nat open; +import Stdlib.Function open; Ty : Type := {B : Type} -> B -> B; id' : Ty | {_} x := x; -fun : {A : Type} → A → Ty := id λ {_ := id'}; +-- In PR https://github.com/anoma/juvix/pull/2545 we had to slightly modify +-- the `fun` definition. The previous version is kept here as a comment. +-- fun : {A : Type} → A → Ty := id λ {_ := id'}; +fun {A : Type} : A → Ty := id { _ -> {C : Type} → C → C } λ {_ := id'}; main : Nat := fun 5 {Nat} 7; diff --git a/tests/negative/UnsupportedType.juvix b/tests/negative/UnsupportedType.juvix deleted file mode 100644 index 76fa64a9c..000000000 --- a/tests/negative/UnsupportedType.juvix +++ /dev/null @@ -1,5 +0,0 @@ -module UnsupportedType; - -type List' (A : Type -> Type) := - | nil' - | cons' A (List' A);