From f16570e54686498b65edf5b77222254e95a1ce5e Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Mon, 30 May 2022 13:40:52 +0200 Subject: [PATCH] Add the termination checker to the pipeline (#111) * [WIP] EntryPoint now has options. --no-termination is a new global opt. * Add TerminationChecking to the pipeline * Add TerminationChecking to the pipeline * Keep GlobalOptions in App * Fix reviewer's comments * delete unnecessary parens Co-authored-by: Jan Mas Rovira --- app/GlobalOptions.hs | 14 +- app/Main.hs | 70 +++-- src/MiniJuvix/Pipeline.hs | 3 +- src/MiniJuvix/Pipeline/EntryPoint.hs | 22 +- src/MiniJuvix/Prelude/Base.hs | 11 +- .../Syntax/Abstract/AbstractResult.hs | 5 + src/MiniJuvix/Syntax/Concrete/Parser.hs | 4 +- .../Syntax/Concrete/Scoped/Error/Types.hs | 2 +- .../Syntax/Concrete/Scoped/Scoper.hs | 2 +- .../Syntax/MicroJuvix/TypeChecker.hs | 2 +- src/MiniJuvix/Termination/Checker.hs | 32 ++- src/MiniJuvix/Termination/Error/Types.hs | 2 +- .../Translation/AbstractToMicroJuvix.hs | 244 ++++++++++-------- src/MiniJuvix/Translation/ScopedToAbstract.hs | 5 +- test/BackendC/Positive.hs | 2 +- test/Base.hs | 5 +- test/Main.hs | 2 + test/MonoJuvix/Positive.hs | 2 +- test/Scope/Negative.hs | 2 +- test/Scope/Positive.hs | 14 +- test/Termination.hs | 8 + test/Termination/Negative.hs | 84 ++++++ test/Termination/Positive.hs | 78 ++++++ test/TypeCheck/Negative.hs | 2 +- test/TypeCheck/Positive.hs | 2 +- tests/negative/Termination/Data/Bool.mjuvix | 25 ++ tests/negative/Termination/Data/Nat.mjuvix | 28 ++ .../Termination/Data/QuickSort.mjuvix | 38 +++ .../Termination/Data/Tree.mjuvix | 0 .../{Loop.mjuvix => Mutual.mjuvix} | 2 +- tests/negative/Termination/Ord.mjuvix | 20 ++ tests/positive/Polymorphism.mjuvix | 1 + tests/positive/Termination/Data/List.mjuvix | 89 ++----- tests/positive/Termination/Data/Maybe.mjuvix | 8 - tests/positive/Termination/Data/Ord.mjuvix | 7 - .../positive/Termination/Data/Product.mjuvix | 9 - 36 files changed, 583 insertions(+), 263 deletions(-) create mode 100644 test/Termination.hs create mode 100644 test/Termination/Negative.hs create mode 100644 test/Termination/Positive.hs create mode 100644 tests/negative/Termination/Data/Bool.mjuvix create mode 100644 tests/negative/Termination/Data/Nat.mjuvix create mode 100644 tests/negative/Termination/Data/QuickSort.mjuvix rename tests/{positive => negative}/Termination/Data/Tree.mjuvix (100%) rename tests/negative/Termination/{Loop.mjuvix => Mutual.mjuvix} (86%) create mode 100644 tests/negative/Termination/Ord.mjuvix delete mode 100644 tests/positive/Termination/Data/Maybe.mjuvix delete mode 100644 tests/positive/Termination/Data/Ord.mjuvix delete mode 100644 tests/positive/Termination/Data/Product.mjuvix diff --git a/app/GlobalOptions.hs b/app/GlobalOptions.hs index b0c4865ef..9f83c512c 100644 --- a/app/GlobalOptions.hs +++ b/app/GlobalOptions.hs @@ -1,6 +1,9 @@ {-# LANGUAGE ApplicativeDo #-} -module GlobalOptions where +module GlobalOptions + ( module GlobalOptions, + ) +where import MiniJuvix.Prelude import Options.Applicative @@ -8,8 +11,10 @@ import Options.Applicative data GlobalOptions = GlobalOptions { _globalNoColors :: Bool, _globalShowNameIds :: Bool, - _globalOnlyErrors :: Bool + _globalOnlyErrors :: Bool, + _globalNoTermination :: Bool } + deriving stock (Eq, Show) makeLenses ''GlobalOptions @@ -30,4 +35,9 @@ parseGlobalOptions = do ( long "only-errors" <> help "Only print errors in a uniform format (used by minijuvix-mode)" ) + _globalNoTermination <- + switch + ( long "no-termination" + <> help "Disable the termination checker" + ) pure GlobalOptions {..} diff --git a/app/Main.hs b/app/Main.hs index 9e454d6cc..a744c8f9c 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -66,40 +66,62 @@ findRoot cli = do dir0 = takeDirectory <$> cliMainFile cli class HasEntryPoint a where - getEntryPoint :: FilePath -> a -> EntryPoint + getEntryPoint :: FilePath -> GlobalOptions -> a -> EntryPoint instance HasEntryPoint ScopeOptions where - getEntryPoint root = EntryPoint root . (^. scopeInputFiles) + getEntryPoint r opts = EntryPoint r nT . (^. scopeInputFiles) + where + nT = opts ^. globalNoTermination instance HasEntryPoint ParseOptions where - getEntryPoint root = EntryPoint root . pure . (^. parseInputFile) + getEntryPoint r opts = EntryPoint r nT . pure . (^. parseInputFile) + where + nT = opts ^. globalNoTermination instance HasEntryPoint HighlightOptions where - getEntryPoint root = EntryPoint root . pure . (^. highlightInputFile) + getEntryPoint r opts = EntryPoint r nT . pure . (^. highlightInputFile) + where + nT = opts ^. globalNoTermination instance HasEntryPoint HtmlOptions where - getEntryPoint root = EntryPoint root . pure . (^. htmlInputFile) + getEntryPoint r opts = EntryPoint r nT . pure . (^. htmlInputFile) + where + nT = opts ^. globalNoTermination instance HasEntryPoint MicroJuvixTypeOptions where - getEntryPoint root = EntryPoint root . pure . (^. microJuvixTypeInputFile) + getEntryPoint r opts = EntryPoint r nT . pure . (^. microJuvixTypeInputFile) + where + nT = opts ^. globalNoTermination instance HasEntryPoint MicroJuvixPrettyOptions where - getEntryPoint root = EntryPoint root . pure . (^. microJuvixPrettyInputFile) + getEntryPoint r opts = EntryPoint r nT . pure . (^. microJuvixPrettyInputFile) + where + nT = opts ^. globalNoTermination instance HasEntryPoint MonoJuvixOptions where - getEntryPoint root = EntryPoint root . pure . (^. monoJuvixInputFile) + getEntryPoint r opts = EntryPoint r nT . pure . (^. monoJuvixInputFile) + where + nT = opts ^. globalNoTermination instance HasEntryPoint MiniHaskellOptions where - getEntryPoint root = EntryPoint root . pure . (^. miniHaskellInputFile) + getEntryPoint r opts = EntryPoint r nT . pure . (^. miniHaskellInputFile) + where + nT = opts ^. globalNoTermination instance HasEntryPoint MiniCOptions where - getEntryPoint root = EntryPoint root . pure . (^. miniCInputFile) + getEntryPoint r opts = EntryPoint r nT . pure . (^. miniCInputFile) + where + nT = opts ^. globalNoTermination instance HasEntryPoint CallsOptions where - getEntryPoint root = EntryPoint root . pure . (^. callsInputFile) + getEntryPoint r opts = EntryPoint r nT . pure . (^. callsInputFile) + where + nT = opts ^. globalNoTermination instance HasEntryPoint CallGraphOptions where - getEntryPoint root = EntryPoint root . pure . (^. graphInputFile) + getEntryPoint r opts = EntryPoint r nT . pure . (^. graphInputFile) + where + nT = opts ^. globalNoTermination runCLI :: Members '[Embed IO, App] r => CLI -> Sem r () runCLI cli = do @@ -111,7 +133,7 @@ runCLI cli = do DisplayVersion -> embed runDisplayVersion DisplayRoot -> say (pack root) Highlight o -> do - res <- runPipelineEither (upToScoping (getEntryPoint root o)) + res <- runPipelineEither (upToScoping (getEntryPoint root globalOptions o)) absP <- embed (makeAbsolute (o ^. highlightInputFile)) case res of Left err -> say (Highlight.goError (errorIntervals err)) @@ -128,25 +150,27 @@ runCLI cli = do } say (Highlight.go hinput) Parse opts -> do - m <- head . (^. Parser.resultModules) <$> runPipeline (upToParsing (getEntryPoint root opts)) + m <- + head . (^. Parser.resultModules) + <$> runPipeline (upToParsing (getEntryPoint root globalOptions opts)) if opts ^. parseNoPrettyShow then say (show m) else say (pack (ppShow m)) Scope opts -> do - l <- (^. Scoper.resultModules) <$> runPipeline (upToScoping (getEntryPoint root opts)) + l <- (^. Scoper.resultModules) <$> runPipeline (upToScoping (getEntryPoint root globalOptions opts)) forM_ l $ \s -> do renderStdOut (Scoper.ppOut (mkScopePrettyOptions globalOptions opts) s) Html o@HtmlOptions {..} -> do - res <- runPipeline (upToScoping (getEntryPoint root o)) + res <- runPipeline (upToScoping (getEntryPoint root globalOptions o)) let m = head (res ^. Scoper.resultModules) embed (genHtml Scoper.defaultOptions _htmlRecursive _htmlTheme m) MicroJuvix (Pretty opts) -> do - micro <- head . (^. Micro.resultModules) <$> runPipeline (upToMicroJuvix (getEntryPoint root opts)) + micro <- head . (^. Micro.resultModules) <$> runPipeline (upToMicroJuvix (getEntryPoint root globalOptions opts)) let ppOpts = Micro.defaultOptions { Micro._optShowNameId = globalOptions ^. globalShowNameIds } App.renderStdOut (Micro.ppOut ppOpts micro) MicroJuvix (TypeCheck opts) -> do - res <- runPipeline (upToMicroJuvixTyped (getEntryPoint root opts)) + res <- runPipeline (upToMicroJuvixTyped (getEntryPoint root globalOptions opts)) say "Well done! It type checks" when (opts ^. microJuvixTypePrint) $ do let ppOpts = @@ -166,16 +190,16 @@ runCLI cli = do Mono.defaultOptions { Mono._optShowNameIds = globalOptions ^. globalShowNameIds } - monojuvix <- head . (^. Mono.resultModules) <$> runPipeline (upToMonoJuvix (getEntryPoint root o)) + monojuvix <- head . (^. Mono.resultModules) <$> runPipeline (upToMonoJuvix (getEntryPoint root globalOptions o)) renderStdOut (Mono.ppOut ppOpts monojuvix) MiniHaskell o -> do - minihaskell <- head . (^. MiniHaskell.resultModules) <$> runPipeline (upToMiniHaskell (getEntryPoint root o)) + minihaskell <- head . (^. MiniHaskell.resultModules) <$> runPipeline (upToMiniHaskell (getEntryPoint root globalOptions o)) renderStdOut (MiniHaskell.ppOutDefault minihaskell) MiniC o -> do - miniC <- (^. MiniC.resultCCode) <$> runPipeline (upToMiniC (getEntryPoint root o)) + miniC <- (^. MiniC.resultCCode) <$> runPipeline (upToMiniC (getEntryPoint root globalOptions o)) say miniC Termination (Calls opts@CallsOptions {..}) -> do - results <- runPipeline (upToAbstract (getEntryPoint root opts)) + results <- runPipeline (upToAbstract (getEntryPoint root globalOptions opts)) let topModule = head (results ^. Abstract.resultModules) infotable = results ^. Abstract.resultTable callMap0 = Termination.buildCallMap infotable topModule @@ -186,7 +210,7 @@ runCLI cli = do renderStdOut (Abstract.ppOut opts' callMap) newline Termination (CallGraph opts@CallGraphOptions {..}) -> do - results <- runPipeline (upToAbstract (getEntryPoint root opts)) + results <- runPipeline (upToAbstract (getEntryPoint root globalOptions opts)) let topModule = head (results ^. Abstract.resultModules) infotable = results ^. Abstract.resultTable callMap = Termination.buildCallMap infotable topModule diff --git a/src/MiniJuvix/Pipeline.hs b/src/MiniJuvix/Pipeline.hs index ce7338ae5..ab4923a91 100644 --- a/src/MiniJuvix/Pipeline.hs +++ b/src/MiniJuvix/Pipeline.hs @@ -121,9 +121,10 @@ pipelineAbstract :: pipelineAbstract = Abstract.entryAbstract pipelineMicroJuvix :: + Members '[Error MiniJuvixError] r => Abstract.AbstractResult -> Sem r MicroJuvix.MicroJuvixResult -pipelineMicroJuvix = MicroJuvix.entryMicroJuvix +pipelineMicroJuvix = mapError (MiniJuvixError @MicroJuvix.TerminationError) . MicroJuvix.entryMicroJuvix pipelineMicroJuvixTyped :: Members '[Files, NameIdGen, Error MiniJuvixError] r => diff --git a/src/MiniJuvix/Pipeline/EntryPoint.hs b/src/MiniJuvix/Pipeline/EntryPoint.hs index 8669b9f68..fd5ffaf79 100644 --- a/src/MiniJuvix/Pipeline/EntryPoint.hs +++ b/src/MiniJuvix/Pipeline/EntryPoint.hs @@ -1,15 +1,27 @@ -module MiniJuvix.Pipeline.EntryPoint where +module MiniJuvix.Pipeline.EntryPoint + ( module MiniJuvix.Pipeline.EntryPoint, + ) +where import MiniJuvix.Prelude --- | The head of _entryModulePaths is assumed to be the Main module. +-- | The head of _entryModulePaths is assumed to be the Main module data EntryPoint = EntryPoint - { _entryRoot :: FilePath, - _entryModulePaths :: NonEmpty FilePath + { _entryPointRoot :: FilePath, + _entryPointNoTermination :: Bool, + _entryPointModulePaths :: NonEmpty FilePath } deriving stock (Eq, Show) +defaultEntryPoint :: FilePath -> EntryPoint +defaultEntryPoint mainFile = + EntryPoint + { _entryPointRoot = ".", + _entryPointNoTermination = False, + _entryPointModulePaths = pure mainFile + } + makeLenses ''EntryPoint mainModulePath :: Lens' EntryPoint FilePath -mainModulePath = entryModulePaths . _head +mainModulePath = entryPointModulePaths . _head diff --git a/src/MiniJuvix/Prelude/Base.hs b/src/MiniJuvix/Prelude/Base.hs index 08a77ddf7..a386d289a 100644 --- a/src/MiniJuvix/Prelude/Base.hs +++ b/src/MiniJuvix/Prelude/Base.hs @@ -213,8 +213,15 @@ mconcatMap f = List.mconcatMap f . toList -- HashMap -------------------------------------------------------------------------------- -tableInsert :: Hashable k => (a -> v) -> (a -> v -> v) -> k -> a -> HashMap k v -> HashMap k v -tableInsert s f k a m = over (at k) (Just . aux) m +tableInsert :: + Hashable k => + (a -> v) -> + (a -> v -> v) -> + k -> + a -> + HashMap k v -> + HashMap k v +tableInsert s f k a = over (at k) (Just . aux) where aux = \case Just v -> f a v diff --git a/src/MiniJuvix/Syntax/Abstract/AbstractResult.hs b/src/MiniJuvix/Syntax/Abstract/AbstractResult.hs index 622a388d7..c71b40387 100644 --- a/src/MiniJuvix/Syntax/Abstract/AbstractResult.hs +++ b/src/MiniJuvix/Syntax/Abstract/AbstractResult.hs @@ -4,9 +4,11 @@ module MiniJuvix.Syntax.Abstract.AbstractResult ) where +import MiniJuvix.Pipeline.EntryPoint qualified as E import MiniJuvix.Prelude import MiniJuvix.Syntax.Abstract.InfoTable import MiniJuvix.Syntax.Abstract.Language +import MiniJuvix.Syntax.Concrete.Parser.ParserResult import MiniJuvix.Syntax.Concrete.Scoped.Scoper.ScoperResult data AbstractResult = AbstractResult @@ -16,3 +18,6 @@ data AbstractResult = AbstractResult } makeLenses ''AbstractResult + +abstractResultEntryPoint :: Lens' AbstractResult E.EntryPoint +abstractResultEntryPoint = resultScoper . resultParserResult . resultEntry diff --git a/src/MiniJuvix/Syntax/Concrete/Parser.hs b/src/MiniJuvix/Syntax/Concrete/Parser.hs index 35a0210e2..4d0991286 100644 --- a/src/MiniJuvix/Syntax/Concrete/Parser.hs +++ b/src/MiniJuvix/Syntax/Concrete/Parser.hs @@ -27,7 +27,7 @@ entryParser :: EntryPoint -> Sem r ParserResult entryParser e = do - (_resultTable, _resultModules) <- runInfoTableBuilder (runReader e (mapM goFile (e ^. entryModulePaths))) + (_resultTable, _resultModules) <- runInfoTableBuilder (runReader e (mapM goFile (e ^. entryPointModulePaths))) let _resultEntry = e return ParserResult {..} where @@ -37,7 +37,7 @@ entryParser e = do Sem r (Module 'Parsed 'ModuleTop) goFile fileName = do input <- readFile' fileName - case runModuleParser (e ^. entryRoot) fileName input of + case runModuleParser (e ^. entryPointRoot) fileName input of Left er -> throw er Right (tbl, m) -> mergeTable tbl $> m diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs index 63127b410..5075ec96a 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Error/Types.hs @@ -247,7 +247,7 @@ makeLenses ''NotInScope instance ToGenericError NotInScope where genericError e@NotInScope {..} = GenericError - { _genericErrorLoc = (e ^. notInScopeSymbol . symbolLoc), + { _genericErrorLoc = e ^. notInScopeSymbol . symbolLoc, _genericErrorMessage = prettyError msg, _genericErrorIntervals = [e ^. notInScopeSymbol . symbolLoc] } diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs index c30b0a548..8c0e79120 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs @@ -34,7 +34,7 @@ entryScoper :: ParserResult -> Sem r ScoperResult entryScoper pr = do - let root = pr ^. Parser.resultEntry . entryRoot + let root = pr ^. Parser.resultEntry . entryPointRoot modules = pr ^. Parser.resultModules scopeCheck pr root modules diff --git a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs index 1b4cfb2f8..21323df90 100644 --- a/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs +++ b/src/MiniJuvix/Syntax/MicroJuvix/TypeChecker.hs @@ -252,7 +252,7 @@ checkPattern :: FunctionArgType -> Pattern -> Sem r () -checkPattern funName type_ pat = go type_ pat +checkPattern funName = go where go :: FunctionArgType -> Pattern -> Sem r () go argTy p = do diff --git a/src/MiniJuvix/Termination/Checker.hs b/src/MiniJuvix/Termination/Checker.hs index 1025daff4..f3a3071e2 100644 --- a/src/MiniJuvix/Termination/Checker.hs +++ b/src/MiniJuvix/Termination/Checker.hs @@ -1,16 +1,44 @@ module MiniJuvix.Termination.Checker ( module MiniJuvix.Termination.Checker, module MiniJuvix.Termination.FunctionCall, + module MiniJuvix.Termination.Error, ) where +import Data.HashMap.Internal.Strict qualified as HashMap import MiniJuvix.Prelude -import MiniJuvix.Syntax.Abstract.InfoTable -import MiniJuvix.Syntax.Abstract.Language.Extra +import MiniJuvix.Syntax.Abstract.InfoTable as Abstract +import MiniJuvix.Syntax.Abstract.Language as Abstract import MiniJuvix.Syntax.Concrete.Scoped.Name (unqualifiedSymbol) +import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as Scoper +import MiniJuvix.Termination.Error import MiniJuvix.Termination.FunctionCall +import MiniJuvix.Termination.LexOrder import MiniJuvix.Termination.Types +checkTermination :: + Members '[Error TerminationError] r => + Abstract.TopModule -> + Abstract.InfoTable -> + Sem r () +checkTermination topModule infotable = do + let callmap = buildCallMap infotable topModule + completeGraph = completeCallGraph callmap + rEdges = reflexiveEdges completeGraph + recBehav = map recursiveBehaviour rEdges + forM_ recBehav $ \r -> do + let funSym = r ^. recursiveBehaviourFun + funName = Scoper.unqualifiedSymbol funSym + funRef = Abstract.FunctionRef funName + funInfo = HashMap.lookupDefault impossible funRef (infotable ^. Abstract.infoFunctions) + markedTerminating = funInfo ^. (Abstract.functionInfoDef . Abstract.funDefTerminating) + if + | markedTerminating -> return () + | otherwise -> + case findOrder r of + Nothing -> throw (ErrNoLexOrder (NoLexOrder funName)) + Just _ -> return () + buildCallMap :: InfoTable -> TopModule -> CallMap buildCallMap infotable = run . execState mempty . runReader infotable . checkModule diff --git a/src/MiniJuvix/Termination/Error/Types.hs b/src/MiniJuvix/Termination/Error/Types.hs index aa38f3841..98a75ba97 100644 --- a/src/MiniJuvix/Termination/Error/Types.hs +++ b/src/MiniJuvix/Termination/Error/Types.hs @@ -26,5 +26,5 @@ instance ToGenericError NoLexOrder where msg :: Doc Eann msg = - "The function" <+> pretty (Scoped.nameUnqualifiedText name) + "The function" <+> highlight (pretty (Scoped.nameUnqualifiedText name)) <+> "fails the termination checker." diff --git a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs index ff91df986..dc790980b 100644 --- a/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs +++ b/src/MiniJuvix/Translation/AbstractToMicroJuvix.hs @@ -1,23 +1,26 @@ module MiniJuvix.Translation.AbstractToMicroJuvix ( module MiniJuvix.Translation.AbstractToMicroJuvix, module MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult, + module MiniJuvix.Termination.Checker, ) where import Data.HashSet qualified as HashSet +import MiniJuvix.Pipeline.EntryPoint qualified as E import MiniJuvix.Prelude import MiniJuvix.Syntax.Abstract.AbstractResult qualified as Abstract -import MiniJuvix.Syntax.Abstract.Language.Extra qualified as A +import MiniJuvix.Syntax.Abstract.Language qualified as Abstract import MiniJuvix.Syntax.Concrete.Name (symbolLoc) -import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S +import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as Scoper import MiniJuvix.Syntax.MicroJuvix.Language import MiniJuvix.Syntax.MicroJuvix.MicroJuvixResult import MiniJuvix.Syntax.Universe -import MiniJuvix.Syntax.Usage qualified as A +import MiniJuvix.Syntax.Usage +import MiniJuvix.Termination.Checker newtype TranslationState = TranslationState { -- | Top modules are supposed to be included at most once. - _translationStateIncluded :: HashSet A.TopModuleName + _translationStateIncluded :: HashSet Abstract.TopModuleName } iniState :: TranslationState @@ -29,57 +32,68 @@ iniState = makeLenses ''TranslationState entryMicroJuvix :: + Members '[Error TerminationError] r => Abstract.AbstractResult -> Sem r MicroJuvixResult -entryMicroJuvix ares = do +entryMicroJuvix abstractResults = do + unless noTerminationOption (checkTermination topModule infoTable) _resultModules' <- evalState iniState - (mapM goModule (ares ^. Abstract.resultModules)) + (mapM goModule (abstractResults ^. Abstract.resultModules)) return MicroJuvixResult - { _resultAbstract = ares, + { _resultAbstract = abstractResults, _resultModules = _resultModules' } + where + topModule = head (abstractResults ^. Abstract.resultModules) + infoTable = abstractResults ^. Abstract.resultTable + noTerminationOption = + abstractResults + ^. Abstract.abstractResultEntryPoint . E.entryPointNoTermination -goModule :: Member (State TranslationState) r => A.TopModule -> Sem r Module +goModule :: + Member (State TranslationState) r => + Abstract.TopModule -> + Sem r Module goModule m = do - _moduleBody' <- goModuleBody (m ^. A.moduleBody) + _moduleBody' <- goModuleBody (m ^. Abstract.moduleBody) return Module - { _moduleName = goTopModuleName (m ^. A.moduleName), + { _moduleName = goTopModuleName (m ^. Abstract.moduleName), _moduleBody = _moduleBody' } -goTopModuleName :: A.TopModuleName -> Name -goTopModuleName = goSymbol . S.topModulePathName +goTopModuleName :: Abstract.TopModuleName -> Name +goTopModuleName = goSymbol . Scoper.topModulePathName -goName :: S.Name -> Name -goName = goSymbol . S.nameUnqualify +goName :: Scoper.Name -> Name +goName = goSymbol . Scoper.nameUnqualify -goSymbol :: S.Symbol -> Name +goSymbol :: Scoper.Symbol -> Name goSymbol s = Name - { _nameText = S.symbolText s, - _nameId = s ^. S.nameId, + { _nameText = Scoper.symbolText s, + _nameId = s ^. Scoper.nameId, _nameKind = getNameKind s, - _nameDefined = s ^. S.nameDefined, - _nameLoc = s ^. S.nameConcrete . symbolLoc + _nameDefined = s ^. Scoper.nameDefined, + _nameLoc = s ^. Scoper.nameConcrete . symbolLoc } unsupported :: Text -> a unsupported thing = error ("Abstract to MicroJuvix: Not yet supported: " <> thing) -goModuleBody :: Member (State TranslationState) r => A.ModuleBody -> Sem r ModuleBody -goModuleBody b = ModuleBody <$> mapMaybeM goStatement (b ^. A.moduleStatements) +goModuleBody :: Member (State TranslationState) r => Abstract.ModuleBody -> Sem r ModuleBody +goModuleBody b = ModuleBody <$> mapMaybeM goStatement (b ^. Abstract.moduleStatements) -goImport :: Member (State TranslationState) r => A.TopModule -> Sem r (Maybe Include) +goImport :: Member (State TranslationState) r => Abstract.TopModule -> Sem r (Maybe Include) goImport m = do - inc <- gets (HashSet.member (m ^. A.moduleName) . (^. translationStateIncluded)) + inc <- gets (HashSet.member (m ^. Abstract.moduleName) . (^. translationStateIncluded)) if | inc -> return Nothing | otherwise -> do - modify (over translationStateIncluded (HashSet.insert (m ^. A.moduleName))) + modify (over translationStateIncluded (HashSet.insert (m ^. Abstract.moduleName))) m' <- goModule m return ( Just @@ -88,58 +102,62 @@ goImport m = do } ) -goStatement :: Member (State TranslationState) r => A.Statement -> Sem r (Maybe Statement) +goStatement :: + Member (State TranslationState) r => + Abstract.Statement -> + Sem r (Maybe Statement) goStatement = \case - A.StatementAxiom d -> Just . StatementAxiom <$> goAxiomDef d - A.StatementForeign f -> return (Just (StatementForeign f)) - A.StatementFunction f -> Just . StatementFunction <$> goFunctionDef f - A.StatementImport i -> fmap StatementInclude <$> goImport i - A.StatementLocalModule {} -> unsupported "local modules" - A.StatementInductive i -> Just . StatementInductive <$> goInductiveDef i + Abstract.StatementAxiom d -> Just . StatementAxiom <$> goAxiomDef d + Abstract.StatementForeign f -> return (Just (StatementForeign f)) + Abstract.StatementFunction f -> Just . StatementFunction <$> goFunctionDef f + Abstract.StatementImport i -> fmap StatementInclude <$> goImport i + Abstract.StatementLocalModule {} -> unsupported "local modules" + Abstract.StatementInductive i -> Just . StatementInductive <$> goInductiveDef i -goTypeIden :: A.Iden -> TypeIden +goTypeIden :: Abstract.Iden -> TypeIden goTypeIden i = case i of - A.IdenFunction {} -> unsupported "functions in types" - A.IdenConstructor {} -> unsupported "constructors in types" - A.IdenVar v -> TypeIdenVariable (goSymbol v) - A.IdenInductive d -> TypeIdenInductive (goName (d ^. A.inductiveRefName)) - A.IdenAxiom a -> TypeIdenAxiom (goName (a ^. A.axiomRefName)) + Abstract.IdenFunction {} -> unsupported "functions in types" + Abstract.IdenConstructor {} -> unsupported "constructors in types" + Abstract.IdenVar v -> TypeIdenVariable (goSymbol v) + Abstract.IdenInductive d -> TypeIdenInductive (goName (d ^. Abstract.inductiveRefName)) + Abstract.IdenAxiom a -> TypeIdenAxiom (goName (a ^. Abstract.axiomRefName)) -goAxiomDef :: A.AxiomDef -> Sem r AxiomDef +goAxiomDef :: Abstract.AxiomDef -> Sem r AxiomDef goAxiomDef a = do - _axiomType' <- goType (a ^. A.axiomType) + _axiomType' <- goType (a ^. Abstract.axiomType) return AxiomDef - { _axiomName = goSymbol (a ^. A.axiomName), + { _axiomName = goSymbol (a ^. Abstract.axiomName), _axiomType = _axiomType' } -goFunctionParameter :: A.FunctionParameter -> Sem r (Either VarName Type) -goFunctionParameter f = case f ^. A.paramName of +goFunctionParameter :: Abstract.FunctionParameter -> Sem r (Either VarName Type) +goFunctionParameter f = case f ^. Abstract.paramName of Just var - | isSmallType (f ^. A.paramType) && isOmegaUsage (f ^. A.paramUsage) -> return (Left (goSymbol var)) + | isSmallType (f ^. Abstract.paramType) && isOmegaUsage (f ^. Abstract.paramUsage) -> + return (Left (goSymbol var)) | otherwise -> unsupported "named function arguments only for small types without usages" Nothing - | isOmegaUsage (f ^. A.paramUsage) -> Right <$> goType (f ^. A.paramType) + | isOmegaUsage (f ^. Abstract.paramUsage) -> Right <$> goType (f ^. Abstract.paramType) | otherwise -> unsupported "usages" -isOmegaUsage :: A.Usage -> Bool +isOmegaUsage :: Usage -> Bool isOmegaUsage u = case u of - A.UsageOmega -> True + UsageOmega -> True _ -> False -goFunction :: A.Function -> Sem r Type -goFunction (A.Function l r) = do +goFunction :: Abstract.Function -> Sem r Type +goFunction (Abstract.Function l r) = do l' <- goFunctionParameter l r' <- goType r return $ case l' of Left tyvar -> TypeAbs (TypeAbstraction tyvar r') Right ty -> TypeFunction (Function ty r') -goFunctionDef :: A.FunctionDef -> Sem r FunctionDef +goFunctionDef :: Abstract.FunctionDef -> Sem r FunctionDef goFunctionDef f = do - _funDefClauses' <- mapM (goFunctionClause _funDefName') (f ^. A.funDefClauses) - _funDefType' <- goType (f ^. A.funDefTypeSig) + _funDefClauses' <- mapM (goFunctionClause _funDefName') (f ^. Abstract.funDefClauses) + _funDefType' <- goType (f ^. Abstract.funDefTypeSig) return FunctionDef { _funDefName = _funDefName', @@ -148,12 +166,12 @@ goFunctionDef f = do } where _funDefName' :: Name - _funDefName' = goSymbol (f ^. A.funDefName) + _funDefName' = goSymbol (f ^. Abstract.funDefName) -goFunctionClause :: Name -> A.FunctionClause -> Sem r FunctionClause +goFunctionClause :: Name -> Abstract.FunctionClause -> Sem r FunctionClause goFunctionClause n c = do - _clauseBody' <- goExpression (c ^. A.clauseBody) - _clausePatterns' <- mapM goPattern (c ^. A.clausePatterns) + _clauseBody' <- goExpression (c ^. Abstract.clauseBody) + _clausePatterns' <- mapM goPattern (c ^. Abstract.clausePatterns) return FunctionClause { _clauseName = n, @@ -161,25 +179,25 @@ goFunctionClause n c = do _clauseBody = _clauseBody' } -goPattern :: A.Pattern -> Sem r Pattern +goPattern :: Abstract.Pattern -> Sem r Pattern goPattern p = case p of - A.PatternVariable v -> return (PatternVariable (goSymbol v)) - A.PatternConstructorApp c -> PatternConstructorApp <$> goConstructorApp c - A.PatternWildcard -> return PatternWildcard - A.PatternEmpty -> unsupported "pattern empty" + Abstract.PatternVariable v -> return (PatternVariable (goSymbol v)) + Abstract.PatternConstructorApp c -> PatternConstructorApp <$> goConstructorApp c + Abstract.PatternWildcard -> return PatternWildcard + Abstract.PatternEmpty -> unsupported "pattern empty" -goConstructorApp :: A.ConstructorApp -> Sem r ConstructorApp +goConstructorApp :: Abstract.ConstructorApp -> Sem r ConstructorApp goConstructorApp c = do - _constrAppParameters' <- mapM goPattern (c ^. A.constrAppParameters) + _constrAppParameters' <- mapM goPattern (c ^. Abstract.constrAppParameters) return ConstructorApp - { _constrAppConstructor = goName (c ^. A.constrAppConstructor . A.constructorRefName), + { _constrAppConstructor = goName (c ^. Abstract.constrAppConstructor . Abstract.constructorRefName), _constrAppParameters = _constrAppParameters' } -isSmallType :: A.Expression -> Bool +isSmallType :: Abstract.Expression -> Bool isSmallType e = case e of - A.ExpressionUniverse u -> isSmallUni u + Abstract.ExpressionUniverse u -> isSmallUni u _ -> False isSmallUni :: Universe -> Bool @@ -190,52 +208,52 @@ goTypeUniverse u | isSmallUni u = TypeUniverse | otherwise = unsupported "big universes" -goType :: A.Expression -> Sem r Type +goType :: Abstract.Expression -> Sem r Type goType e = case e of - A.ExpressionIden i -> return (TypeIden (goTypeIden i)) - A.ExpressionUniverse u -> return (goTypeUniverse u) - A.ExpressionApplication a -> TypeApp <$> goTypeApplication a - A.ExpressionFunction f -> goFunction f - A.ExpressionLiteral {} -> unsupported "literals in types" + Abstract.ExpressionIden i -> return (TypeIden (goTypeIden i)) + Abstract.ExpressionUniverse u -> return (goTypeUniverse u) + Abstract.ExpressionApplication a -> TypeApp <$> goTypeApplication a + Abstract.ExpressionFunction f -> goFunction f + Abstract.ExpressionLiteral {} -> unsupported "literals in types" -goApplication :: A.Application -> Sem r Application -goApplication (A.Application f x) = do +goApplication :: Abstract.Application -> Sem r Application +goApplication (Abstract.Application f x) = do f' <- goExpression f x' <- goExpression x return (Application f' x') -goIden :: A.Iden -> Iden +goIden :: Abstract.Iden -> Iden goIden i = case i of - A.IdenFunction n -> IdenFunction (goName (n ^. A.functionRefName)) - A.IdenConstructor c -> IdenConstructor (goName (c ^. A.constructorRefName)) - A.IdenVar v -> IdenVar (goSymbol v) - A.IdenAxiom a -> IdenAxiom (goName (a ^. A.axiomRefName)) - A.IdenInductive a -> IdenInductive (goName (a ^. A.inductiveRefName)) + Abstract.IdenFunction n -> IdenFunction (goName (n ^. Abstract.functionRefName)) + Abstract.IdenConstructor c -> IdenConstructor (goName (c ^. Abstract.constructorRefName)) + Abstract.IdenVar v -> IdenVar (goSymbol v) + Abstract.IdenAxiom a -> IdenAxiom (goName (a ^. Abstract.axiomRefName)) + Abstract.IdenInductive a -> IdenInductive (goName (a ^. Abstract.inductiveRefName)) -goExpressionFunction :: forall r. A.Function -> Sem r FunctionExpression +goExpressionFunction :: forall r. Abstract.Function -> Sem r FunctionExpression goExpressionFunction f = do - l' <- goParam (f ^. A.funParameter) - r' <- goExpression (f ^. A.funReturn) + l' <- goParam (f ^. Abstract.funParameter) + r' <- goExpression (f ^. Abstract.funReturn) return (FunctionExpression l' r') where - goParam :: A.FunctionParameter -> Sem r Expression + goParam :: Abstract.FunctionParameter -> Sem r Expression goParam p - | isJust (p ^. A.paramName) = unsupported "named type parameters" - | isOmegaUsage (p ^. A.paramUsage) = goExpression (p ^. A.paramType) + | isJust (p ^. Abstract.paramName) = unsupported "named type parameters" + | isOmegaUsage (p ^. Abstract.paramUsage) = goExpression (p ^. Abstract.paramType) | otherwise = unsupported "usages" -goExpression :: A.Expression -> Sem r Expression +goExpression :: Abstract.Expression -> Sem r Expression goExpression e = case e of - A.ExpressionIden i -> return (ExpressionIden (goIden i)) - A.ExpressionUniverse {} -> unsupported "universes in expression" - A.ExpressionFunction f -> ExpressionFunction <$> goExpressionFunction f - A.ExpressionApplication a -> ExpressionApplication <$> goApplication a - A.ExpressionLiteral l -> return (ExpressionLiteral l) + Abstract.ExpressionIden i -> return (ExpressionIden (goIden i)) + Abstract.ExpressionUniverse {} -> unsupported "universes in expression" + Abstract.ExpressionFunction f -> ExpressionFunction <$> goExpressionFunction f + Abstract.ExpressionApplication a -> ExpressionApplication <$> goApplication a + Abstract.ExpressionLiteral l -> return (ExpressionLiteral l) -goInductiveParameter :: A.FunctionParameter -> Sem r InductiveParameter +goInductiveParameter :: Abstract.FunctionParameter -> Sem r InductiveParameter goInductiveParameter f = - case (f ^. A.paramName, f ^. A.paramUsage, f ^. A.paramType) of - (Just var, A.UsageOmega, A.ExpressionUniverse u) + case (f ^. Abstract.paramName, f ^. Abstract.paramUsage, f ^. Abstract.paramType) of + (Just var, UsageOmega, Abstract.ExpressionUniverse u) | isSmallUni u -> return InductiveParameter @@ -244,12 +262,12 @@ goInductiveParameter f = (Just {}, _, _) -> unsupported "only type variables of small types are allowed" (Nothing, _, _) -> unsupported "unnamed inductive parameters" -goInductiveDef :: forall r. A.InductiveDef -> Sem r InductiveDef -goInductiveDef i = case i ^. A.inductiveType of +goInductiveDef :: forall r. Abstract.InductiveDef -> Sem r InductiveDef +goInductiveDef i = case i ^. Abstract.inductiveType of Just {} -> unsupported "inductive indices" _ -> do - _inductiveParameters' <- mapM goInductiveParameter (i ^. A.inductiveParameters) - _inductiveConstructors' <- mapM goConstructorDef (i ^. A.inductiveConstructors) + _inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters) + _inductiveConstructors' <- mapM goConstructorDef (i ^. Abstract.inductiveConstructors) return InductiveDef { _inductiveName = indName, @@ -257,21 +275,21 @@ goInductiveDef i = case i ^. A.inductiveType of _inductiveConstructors = _inductiveConstructors' } where - indName = goSymbol (i ^. A.inductiveName) - goConstructorDef :: A.InductiveConstructorDef -> Sem r InductiveConstructorDef + indName = goSymbol (i ^. Abstract.inductiveName) + goConstructorDef :: Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef goConstructorDef c = do - _constructorParameters' <- goConstructorType (c ^. A.constructorType) + _constructorParameters' <- goConstructorType (c ^. Abstract.constructorType) return InductiveConstructorDef - { _constructorName = goSymbol (c ^. A.constructorName), + { _constructorName = goSymbol (c ^. Abstract.constructorName), _constructorParameters = _constructorParameters' } -- TODO check that the return type corresponds with the inductive type - goConstructorType :: A.Expression -> Sem r [Type] + goConstructorType :: Abstract.Expression -> Sem r [Type] goConstructorType = fmap fst . viewConstructorType -goTypeApplication :: A.Application -> Sem r TypeApplication -goTypeApplication (A.Application l r) = do +goTypeApplication :: Abstract.Application -> Sem r TypeApplication +goTypeApplication (Abstract.Application l r) = do l' <- goType l r' <- goType r return @@ -280,18 +298,18 @@ goTypeApplication (A.Application l r) = do _typeAppRight = r' } -viewConstructorType :: A.Expression -> Sem r ([Type], Type) +viewConstructorType :: Abstract.Expression -> Sem r ([Type], Type) viewConstructorType e = case e of - A.ExpressionFunction f -> first toList <$> viewFunctionType f - A.ExpressionIden i -> return ([], TypeIden (goTypeIden i)) - A.ExpressionApplication a -> do + Abstract.ExpressionFunction f -> first toList <$> viewFunctionType f + Abstract.ExpressionIden i -> return ([], TypeIden (goTypeIden i)) + Abstract.ExpressionApplication a -> do a' <- goTypeApplication a return ([], TypeApp a') - A.ExpressionUniverse {} -> return ([], TypeUniverse) - A.ExpressionLiteral {} -> unsupported "literal in a type" + Abstract.ExpressionUniverse {} -> return ([], TypeUniverse) + Abstract.ExpressionLiteral {} -> unsupported "literal in a type" where - viewFunctionType :: A.Function -> Sem r (NonEmpty Type, Type) - viewFunctionType (A.Function p r) = do + viewFunctionType :: Abstract.Function -> Sem r (NonEmpty Type, Type) + viewFunctionType (Abstract.Function p r) = do (args, ret) <- viewConstructorType r p' <- goFunctionParameter p return $ case p' of diff --git a/src/MiniJuvix/Translation/ScopedToAbstract.hs b/src/MiniJuvix/Translation/ScopedToAbstract.hs index e77e0318d..4a46053a8 100644 --- a/src/MiniJuvix/Translation/ScopedToAbstract.hs +++ b/src/MiniJuvix/Translation/ScopedToAbstract.hs @@ -20,10 +20,7 @@ unsupported msg = error $ msg <> "Scoped to Abstract: not yet supported" entryAbstract :: Scoper.ScoperResult -> Sem r AbstractResult entryAbstract _resultScoper = do (_resultTable, _resultModules) <- runInfoTableBuilder (mapM goTopModule ms) - return - AbstractResult - { .. - } + return AbstractResult {..} where ms = _resultScoper ^. Scoper.resultModules diff --git a/test/BackendC/Positive.hs b/test/BackendC/Positive.hs index 3b3159498..cf860888f 100644 --- a/test/BackendC/Positive.hs +++ b/test/BackendC/Positive.hs @@ -44,7 +44,7 @@ testDescr PosTest {..} = "WASI_SYSROOT_PATH" step "C Generation" - let entryPoint = EntryPoint "." (pure mainFile) + let entryPoint = defaultEntryPoint mainFile p :: MiniC.MiniCResult <- runIO (upToMiniC entryPoint) expected <- TIO.readFile expectedFile diff --git a/test/Base.hs b/test/Base.hs index ca9717033..7410a6615 100644 --- a/test/Base.hs +++ b/test/Base.hs @@ -44,7 +44,10 @@ assertEqDiff msg a b pb = lines $ ppShow b assertCmdExists :: FilePath -> Assertion -assertCmdExists cmd = assertBool ("Command: " <> cmd <> " is not present on $PATH") . isJust =<< findExecutable cmd +assertCmdExists cmd = + assertBool ("Command: " <> cmd <> " is not present on $PATH") + . isJust + =<< findExecutable cmd assertEnvVar :: String -> String -> IO String assertEnvVar msg varName = fromMaybeM (assertFailure msg) (lookupEnv varName) diff --git a/test/Main.hs b/test/Main.hs index 9720e4f45..a2486bf87 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -4,6 +4,7 @@ import BackendC qualified import Base import MonoJuvix qualified import Scope qualified +import Termination qualified import TypeCheck qualified slowTests :: TestTree @@ -17,6 +18,7 @@ fastTests = testGroup "MiniJuvix fast tests" [ Scope.allTests, + Termination.allTests, TypeCheck.allTests, MonoJuvix.allTests ] diff --git a/test/MonoJuvix/Positive.hs b/test/MonoJuvix/Positive.hs index e9f2033a8..71bc2c85f 100644 --- a/test/MonoJuvix/Positive.hs +++ b/test/MonoJuvix/Positive.hs @@ -19,7 +19,7 @@ testDescr PosTest {..} = { _testName = _name, _testRoot = tRoot, _testAssertion = Single $ do - let entryPoint = EntryPoint "." (pure _file) + let entryPoint = defaultEntryPoint _file (void . runIO) (upToMonoJuvix entryPoint) } diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index ba7402c02..c9cdcea97 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -23,7 +23,7 @@ testDescr NegTest {..} = { _testName = _name, _testRoot = tRoot, _testAssertion = Single $ do - let entryPoint = EntryPoint "." (pure _file) + let entryPoint = defaultEntryPoint _file res <- runIOEither (upToScoping entryPoint) case mapLeft fromMiniJuvixError res of Left (Just err) -> whenJust (_checkErr err) assertFailure diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs index 97119e979..3627090b5 100644 --- a/test/Scope/Positive.hs +++ b/test/Scope/Positive.hs @@ -33,7 +33,7 @@ testDescr PosTest {..} = _testAssertion = Steps $ \step -> do cwd <- getCurrentDirectory entryFile <- makeAbsolute _file - let entryPoint = EntryPoint cwd (pure entryFile) + let entryPoint = EntryPoint cwd False (pure entryFile) step "Parsing" p :: Parser.ParserResult <- runIO (upToParsing entryPoint) @@ -57,14 +57,20 @@ testDescr PosTest {..} = step "Parsing pretty scoped" let fs2 = HashMap.singleton entryFile scopedPretty - p' :: Parser.ParserResult <- (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs2) (upToParsing entryPoint) + p' :: Parser.ParserResult <- + (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs2) + (upToParsing entryPoint) step "Parsing pretty parsed" let fs3 = HashMap.singleton entryFile parsedPretty - parsedPretty' :: Parser.ParserResult <- (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs3) (upToParsing entryPoint) + parsedPretty' :: Parser.ParserResult <- + (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs3) + (upToParsing entryPoint) step "Scoping the scoped" - s' :: Scoper.ScoperResult <- (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs) (upToScoping entryPoint) + s' :: Scoper.ScoperResult <- + (runM . runErrorIO @MiniJuvixError . runNameIdGen . runFilesPure fs) + (upToScoping entryPoint) step "Checks" let smodules = s ^. Scoper.resultModules diff --git a/test/Termination.hs b/test/Termination.hs new file mode 100644 index 000000000..615ec8a65 --- /dev/null +++ b/test/Termination.hs @@ -0,0 +1,8 @@ +module Termination (allTests) where + +import Base +import Termination.Negative qualified as N +import Termination.Positive qualified as P + +allTests :: TestTree +allTests = testGroup "Termination checker tests" [P.allTests, N.allTests] diff --git a/test/Termination/Negative.hs b/test/Termination/Negative.hs new file mode 100644 index 000000000..2ff38b21d --- /dev/null +++ b/test/Termination/Negative.hs @@ -0,0 +1,84 @@ +module Termination.Negative (module Termination.Negative) where + +import Base +import MiniJuvix.Pipeline +import MiniJuvix.Termination + +type FailMsg = String + +data NegTest = NegTest + { _name :: String, + _relDir :: FilePath, + _file :: FilePath, + _checkErr :: TerminationError -> Maybe FailMsg + } + +testDescr :: NegTest -> TestDescr +testDescr NegTest {..} = + let tRoot = root _relDir + in TestDescr + { _testName = _name, + _testRoot = tRoot, + _testAssertion = Single $ do + let entryPoint = defaultEntryPoint _file + result <- runIOEither (upToMicroJuvix entryPoint) + case mapLeft fromMiniJuvixError result of + Left (Just lexError) -> whenJust (_checkErr lexError) assertFailure + Left Nothing -> assertFailure "The termination checker did not find an error." + Right _ -> assertFailure "An error ocurred but it was not by the termination checker." + } + +allTests :: TestTree +allTests = + testGroup + "Termination negative tests" + (map (mkTest . testDescr) tests) + +root :: FilePath +root = "tests/negative/Termination" + +tests :: [NegTest] +tests = + [ NegTest + "Mutual recursive functions non terminating" + "." + "Mutual.mjuvix" + $ \case + ErrNoLexOrder {} -> Nothing, + NegTest + "Another mutual block non terminating" + "." + "Ord.mjuvix" + $ \case + ErrNoLexOrder {} -> Nothing, + NegTest + "Only one function, f, marked terminating in a mutual block" + "." + "TerminatingF.mjuvix" + $ \case + ErrNoLexOrder {} -> Nothing, + NegTest + "Only one function, g, marked terminating in a mutual block" + "." + "TerminatingG.mjuvix" + $ \case + ErrNoLexOrder {} -> Nothing, + NegTest + "f x := f x is not terminating" + "." + "ToEmpty.mjuvix" + $ \case + ErrNoLexOrder {} -> Nothing, + NegTest + "Tree" + "." + "Data/Tree.mjuvix" + $ \case + ErrNoLexOrder {} -> Nothing, + NegTest + "Quicksort is not terminating" + "." + "Data/QuickSort.mjuvix" + $ \case + ErrNoLexOrder {} -> Nothing + ] diff --git a/test/Termination/Positive.hs b/test/Termination/Positive.hs new file mode 100644 index 000000000..6321e0bc5 --- /dev/null +++ b/test/Termination/Positive.hs @@ -0,0 +1,78 @@ +module Termination.Positive where + +import Base +import MiniJuvix.Pipeline +import Termination.Negative qualified as N + +data PosTest = PosTest + { _name :: String, + _relDir :: FilePath, + _file :: FilePath + } + +root :: FilePath +root = "tests/positive/Termination" + +testDescr :: PosTest -> TestDescr +testDescr PosTest {..} = + let tRoot = root _relDir + in TestDescr + { _testName = _name, + _testRoot = tRoot, + _testAssertion = Single $ do + let entryPoint = defaultEntryPoint _file + (void . runIO) (upToMicroJuvix entryPoint) + } + +-------------------------------------------------------------------------------- +-- Testing --no-termination flag with all termination negative tests +-------------------------------------------------------------------------------- + +rootNegTests :: FilePath +rootNegTests = "tests/negative/Termination" + +testDescrFlag :: N.NegTest -> TestDescr +testDescrFlag N.NegTest {..} = + let tRoot = rootNegTests _relDir + in TestDescr + { _testName = _name, + _testRoot = tRoot, + _testAssertion = Single $ do + let entryPoint = EntryPoint "." True (pure _file) + (void . runIO) (upToMicroJuvix entryPoint) + } + +-------------------------------------------------------------------------------- + +tests :: [PosTest] +tests = + [ PosTest "Ackerman nice def. is terminating" "." "Ack.mjuvix", + PosTest "Recursive functions on Lists" "." "Data/List.mjuvix" + ] + +testsWithKeyword :: [PosTest] +testsWithKeyword = + [ PosTest "terminating added to fx:=fx" "." "ToEmpty.mjuvix", + PosTest "terminating for all functions in the mutual block" "." "Mutual.mjuvix", + PosTest "Undefined is terminating by assumption" "." "Undefined.mjuvix" + ] + +negTests :: [N.NegTest] +negTests = N.tests + +-------------------------------------------------------------------------------- + +allTests :: TestTree +allTests = + testGroup + "Positive tests" + [ testGroup + "Well-known terminating functions" + (map (mkTest . testDescr) tests), + testGroup + "Bypass checking using --non-termination flag on negative tests" + (map (mkTest . testDescrFlag) negTests), + testGroup + "Terminating keyword" + (map (mkTest . testDescr) testsWithKeyword) + ] diff --git a/test/TypeCheck/Negative.hs b/test/TypeCheck/Negative.hs index 326060095..df3373e22 100644 --- a/test/TypeCheck/Negative.hs +++ b/test/TypeCheck/Negative.hs @@ -20,7 +20,7 @@ testDescr NegTest {..} = { _testName = _name, _testRoot = tRoot, _testAssertion = Single $ do - let entryPoint = EntryPoint "." (pure _file) + let entryPoint = defaultEntryPoint _file result <- runIOEither (upToMicroJuvixTyped entryPoint) case mapLeft fromMiniJuvixError result of Left (Just tyError) -> whenJust (_checkErr tyError) assertFailure diff --git a/test/TypeCheck/Positive.hs b/test/TypeCheck/Positive.hs index 5dc70de4a..937b9bc2b 100644 --- a/test/TypeCheck/Positive.hs +++ b/test/TypeCheck/Positive.hs @@ -19,7 +19,7 @@ testDescr PosTest {..} = { _testName = _name, _testRoot = tRoot, _testAssertion = Single $ do - let entryPoint = EntryPoint "." (pure _file) + let entryPoint = defaultEntryPoint _file (void . runIO) (upToMicroJuvixTyped entryPoint) } diff --git a/tests/negative/Termination/Data/Bool.mjuvix b/tests/negative/Termination/Data/Bool.mjuvix new file mode 100644 index 000000000..f1d697dd2 --- /dev/null +++ b/tests/negative/Termination/Data/Bool.mjuvix @@ -0,0 +1,25 @@ +module Data.Bool; + inductive Bool { + true : Bool; + false : Bool; + }; + + not : Bool → Bool; + not true ≔ false; + not false ≔ true; + + infixr 2 ||; + || : Bool → Bool → Bool; + || false a ≔ a; + || true _ ≔ true; + + infixr 2 &&; + && : Bool → Bool → Bool; + && false _ ≔ false; + && true a ≔ a; + + ite : (a : Type) → Bool → a → a → a; + ite _ true a _ ≔ a; + ite _ false _ b ≔ b; + +end; diff --git a/tests/negative/Termination/Data/Nat.mjuvix b/tests/negative/Termination/Data/Nat.mjuvix new file mode 100644 index 000000000..ddf832bbf --- /dev/null +++ b/tests/negative/Termination/Data/Nat.mjuvix @@ -0,0 +1,28 @@ +module Data.Nat; + inductive ℕ { + zero : ℕ; + suc : ℕ → ℕ; + }; + + infixl 6 +; + + : ℕ → ℕ → ℕ; + + zero b ≔ b; + + (suc a) b ≔ suc (a + b); + + infixl 7 *; + * : ℕ → ℕ → ℕ; + * zero b ≔ zero; + * (suc a) b ≔ b + a * b; + + import Data.Bool; + open Data.Bool; + + even : ℕ → Bool; + odd : ℕ → Bool; + + even zero ≔ true; + even (suc n) ≔ odd n; + + odd zero ≔ false; + odd (suc n) ≔ even n; +end; diff --git a/tests/negative/Termination/Data/QuickSort.mjuvix b/tests/negative/Termination/Data/QuickSort.mjuvix new file mode 100644 index 000000000..02f1ee57b --- /dev/null +++ b/tests/negative/Termination/Data/QuickSort.mjuvix @@ -0,0 +1,38 @@ +module Data.QuickSort; + +import Data.Bool; +open Data.Bool; + +import Data.Nat; +open Data.Nat; + +inductive List (A : Type) { + nil : List A; + cons : A → List A → List A; +}; + +filter : (A : Type) → (A → Bool) → List A → List A; +filter A f nil ≔ nil A; +filter A f (cons h hs) ≔ ite (List A) (f h) + (cons A h (filter A f hs)) + (filter A f hs); + +concat : (A : Type) → List A → List A → List A; +concat A nil ys ≔ ys; +concat A (cons x xs) ys ≔ cons A x (concat A xs ys); + +ltx : (A : Type) → (A → A → Bool) → A → A → Bool; +ltx A lessThan x y ≔ lessThan y x; + +gex : (A : Type) → (A → A → Bool) → A → A → Bool; +gex A lessThan x y ≔ not (ltx A lessThan x y) ; + +quicksort : (A : Type) → (A → A → Bool) → List A → List A; +quicksort A _ nil ≔ nil A; +quicksort A _ (cons x nil) ≔ cons A x (nil A); +quicksort A lessThan (cons x ys) ≔ + concat A (quicksort A lessThan (filter A (ltx A lessThan x) ys)) + (concat A + (cons A x (nil A)) + (quicksort A lessThan (filter A (gex A lessThan x)) ys)); +end; diff --git a/tests/positive/Termination/Data/Tree.mjuvix b/tests/negative/Termination/Data/Tree.mjuvix similarity index 100% rename from tests/positive/Termination/Data/Tree.mjuvix rename to tests/negative/Termination/Data/Tree.mjuvix diff --git a/tests/negative/Termination/Loop.mjuvix b/tests/negative/Termination/Mutual.mjuvix similarity index 86% rename from tests/negative/Termination/Loop.mjuvix rename to tests/negative/Termination/Mutual.mjuvix index 9a9131c43..a27a7fbac 100644 --- a/tests/negative/Termination/Loop.mjuvix +++ b/tests/negative/Termination/Mutual.mjuvix @@ -1,4 +1,4 @@ -module Loop; +module Mutual; axiom A : Type; diff --git a/tests/negative/Termination/Ord.mjuvix b/tests/negative/Termination/Ord.mjuvix new file mode 100644 index 000000000..1c2b87d94 --- /dev/null +++ b/tests/negative/Termination/Ord.mjuvix @@ -0,0 +1,20 @@ +module Ord; + +import Data.Nat; +open Data.Nat; + +inductive Ord { + ZOrd : Ord; + SOrd : Ord -> Ord; + Lim : (ℕ -> Ord) -> Ord; +}; + +addord : Ord -> Ord -> Ord; +aux-addord : (ℕ -> Ord) -> Ord -> (ℕ -> Ord); + +addord (Zord) y := y; +addord (SOrd x) y := SOrd (addord x y); +addord (Lim f) y := Lim (aux-addord f y); +aux-addord f y z := addord (f z) y; + +end; diff --git a/tests/positive/Polymorphism.mjuvix b/tests/positive/Polymorphism.mjuvix index 9a9be50ef..39f1ab1a1 100644 --- a/tests/positive/Polymorphism.mjuvix +++ b/tests/positive/Polymorphism.mjuvix @@ -23,6 +23,7 @@ inductive Bool { id : (A : Type) → A → A; id _ a ≔ a; +terminating undefined : (A : Type) → A; undefined A ≔ undefined A; diff --git a/tests/positive/Termination/Data/List.mjuvix b/tests/positive/Termination/Data/List.mjuvix index 66b405843..7fdb2fe99 100644 --- a/tests/positive/Termination/Data/List.mjuvix +++ b/tests/positive/Termination/Data/List.mjuvix @@ -7,100 +7,49 @@ import Data.Nat; open Data.Nat; inductive List (A : Type) { - nil : List A; + nil : List A; cons : A → List A → List A; }; foldr : (A : Type) → (B : Type) → (A → B → B) → B → List A → B; -foldr _ _ _ z (nil _) ≔ z; -foldr A B f z (cons _ h hs) ≔ f h (foldr A B f z hs); +foldr _ _ _ z nil ≔ z; +foldr A B f z (cons h hs) ≔ f h (foldr A B f z hs); foldl : (A : Type) → (B : Type) → (B → A → B) → B → List A → B; -foldl A B f z (nil _) ≔ z ; -foldl A B f z (cons _ h hs) ≔ foldl A B f (f z h) hs; +foldl A B f z nil ≔ z ; +foldl A B f z (cons h hs) ≔ foldl A B f (f z h) hs; map : (A : Type) → (B : Type) → (A → B) → List A → List B; -map _ B f (nil _) ≔ nil B; -map A B f (cons _ h hs) ≔ cons A (f h) (map A B f hs); +map _ B f nil ≔ nil B; +map A B f (cons h hs) ≔ cons B (f h) (map A B f hs); filter : (A : Type) → (A → Bool) → List A → List A; -filter A f (nil _) ≔ nil A; -filter A f (cons _ h hs) ≔ ite (List A) (f h) +filter A f nil ≔ nil A; +filter A f (cons h hs) ≔ ite (List A) (f h) (cons A h (filter A f hs)) (filter A f hs); length : (A : Type) → List A → ℕ; -length _ (nil _) ≔ zero; -length A (cons _ _ l) ≔ suc (length A l); +length _ nil ≔ zero; +length A (cons _ l) ≔ suc (length A l); rev : (A : Type) → List A → List A → List A; -rev _ (nil _) l ≔ l; -rev A (cons _ x xs) l ≔ rev A xs (cons A x l); +rev _ nil l ≔ l; +rev A (cons x xs) l ≔ rev A xs (cons A x l); reverse : (A : Type) → List A → List A; -reverse A l ≔ rev l (nil A); +reverse A l ≔ rev A l (nil A); replicate : (A : Type) → ℕ → A → List A; -replicate A zero _ ≔ nil A; +replicate A zero _ ≔ nil A; replicate A (suc n) x ≔ cons A x (replicate A n x); take : (A : Type) → ℕ → List A → List A; -take A (suc n) (cons _ x xs) ≔ cons A x (take A n xs); -take A _ _ ≔ nil A; - -alternate : (A : Type) → List A → List A → List A; -alternate A (nil _) b ≔ b; -alternate A (cons _ h t) b ≔ cons A h (alternate A b t); - -merge : (A : Type) → (A → A → Bool) → List A → List A → List A; -merge _ _ (nil _) ys ≔ ys; -merge _ _ xs (nil _) ≔ xs; -merge A lessThan (cons _ x xs) (cons _ y ys) ≔ - ite (List A) (lessThan x y) - (cons A x (merge A lessThan xs (cons A y ys))) - (cons A y (merge A lessThan ys (cons A x xs))); +take A (suc n) (cons x xs) ≔ cons A x (take A n xs); +take A _ _ ≔ nil A; concat : (A : Type) → List A → List A → List A; -concat A (nil _) ys ≔ ys; -concat A (cons _ x xs) ys ≔ cons A x (concat A xs ys); - -ltx : (A : Type) → (A → A → Bool) → A → A → Bool; -ltx A lessThan x y ≔ lessThan y x; - -gex : (A : Type) → (A → A → Bool) → A → A → Bool; -gex A lessThan x y ≔ not (ltx A lessThan x y) ; - -quickSort : (A : Type) → (A → A → Bool) → List A → List A; -quickSort A _ (nil _) ≔ nil A; -quickSort A _ (cons _ x (nil _)) ≔ cons A x (nil A); -quickSort A lessThan (cons _ x ys) ≔ - concat A (quickSort A (filter A ltx) ys) - (concat A (cons A x (nil A)) (quickSort A (filter A gex) ys)); - --- Mutual recursive function example - -aux : (A : Type) → A → List A → List A; -flat : (A : Type) → List A → List A; - -aux A (nil _) ls := flat A ls; -aux A (cons _ x xs) ls := cons A x (aux A xs ls); - -flat A (nil _) := nil A; -flat A (cons _ x xs) := aux A x xs; - -inductive Ord { - ZOrd : Ord; - SOrd : Ord -> Ord; - Lim : (ℕ -> Ord) -> Ord; -}; - -addord : Ord -> Ord -> Ord; -aux-addord : (ℕ -> Ord) -> Ord -> (ℕ -> Ord); - -addord (Zord) y := y; -addord (SOrd x) y := SOrd (addord x y); -addord (Lim f) y := Lim (aux-addord f y); --- where -aux-addord f y z := addord (f z) y; +concat A nil ys ≔ ys; +concat A (cons x xs) ys ≔ cons A x (concat A xs ys); end; diff --git a/tests/positive/Termination/Data/Maybe.mjuvix b/tests/positive/Termination/Data/Maybe.mjuvix deleted file mode 100644 index 384bbc003..000000000 --- a/tests/positive/Termination/Data/Maybe.mjuvix +++ /dev/null @@ -1,8 +0,0 @@ -module Data.Maybe; - - inductive Maybe (a : Type) { - nothing : Maybe a; - just : a → Maybe a; - } - -end; diff --git a/tests/positive/Termination/Data/Ord.mjuvix b/tests/positive/Termination/Data/Ord.mjuvix deleted file mode 100644 index dd85147ef..000000000 --- a/tests/positive/Termination/Data/Ord.mjuvix +++ /dev/null @@ -1,7 +0,0 @@ -module Data.Ord; - inductive Ordering { - LT : Ordering; - EQ : Ordering; - GT : Ordering; - }; -end; diff --git a/tests/positive/Termination/Data/Product.mjuvix b/tests/positive/Termination/Data/Product.mjuvix deleted file mode 100644 index 9e6b8b76f..000000000 --- a/tests/positive/Termination/Data/Product.mjuvix +++ /dev/null @@ -1,9 +0,0 @@ -module Data.Product; - -infixr 2 ×; --- infixr 4 ,; waiting for implicit arguments -inductive × (a : Type) (b : Type) { - , : a → b → a × b; -}; - -end;