From 423ccec70a53d25a773ea2583a5871ed88deaa76 Mon Sep 17 00:00:00 2001 From: Jonathan Cubides Date: Sat, 23 Jul 2022 09:27:12 +0200 Subject: [PATCH] Add positivity check for inductive types (#1393) * w.i.p * Added strict positivity condition for datatypes w.i.p * Add negative test for str.postivity check * Add some revisions * the branch is back to feet * w.i.p add lots of traces to check alg. * Add more test and revisions * Add negative and positive test to the new flag and the keyword * Fix shell tests. * Make pre-commit happy * Fix rebase conflicts * Make pre-commit happy * Add shell test, rename keyword, fix error msg * Revert change * Necessary changes * Remove wrong unless * Move the positivity checker to its own folder * Add missing juvix.yaml * Add a negative test thanks to jan * make some style changes * Make ormolu happy * Remove unnecessary instance of Show Co-authored-by: Jan Mas Rovira --- app/GlobalOptions.hs | 9 ++ app/Main.hs | 1 + docs/org/SUMMARY.org | 1 + .../notes/strictly-positive-data-types.org | 86 +++++++++++ src/Juvix/Analysis/Positivity/Checker.hs | 140 ++++++++++++++++++ src/Juvix/Internal/Strings.hs | 3 + src/Juvix/Pipeline/EntryPoint.hs | 2 + src/Juvix/Syntax/Abstract/Language.hs | 3 +- src/Juvix/Syntax/Concrete/Language.hs | 3 +- src/Juvix/Syntax/Concrete/Lexer.hs | 3 + src/Juvix/Syntax/Concrete/Parser.hs | 1 + src/Juvix/Syntax/Concrete/Scoped/Scoper.hs | 5 +- src/Juvix/Syntax/MicroJuvix/Error.hs | 2 + src/Juvix/Syntax/MicroJuvix/Error/Types.hs | 29 ++++ src/Juvix/Syntax/MicroJuvix/InfoTable.hs | 6 +- src/Juvix/Syntax/MicroJuvix/Language.hs | 8 +- src/Juvix/Syntax/MicroJuvix/Language/Extra.hs | 4 +- .../MicroJuvix/MicroJuvixArityResult.hs | 8 +- .../Syntax/MicroJuvix/MicroJuvixResult.hs | 4 + src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs | 4 +- src/Juvix/Syntax/MicroJuvix/TypeChecker.hs | 77 +++++++++- src/Juvix/Syntax/Universe.hs | 2 +- src/Juvix/Translation/AbstractToMicroJuvix.hs | 48 ++---- src/Juvix/Translation/MicroJuvixToMiniC.hs | 14 +- .../Translation/MicroJuvixToMonoJuvix.hs | 10 +- .../TypeCallsMapBuilder.hs | 2 +- src/Juvix/Translation/ScopedToAbstract.hs | 5 +- test/Scope/Positive.hs | 1 + test/Termination/Positive.hs | 12 +- test/TypeCheck/Negative.hs | 52 ++++++- test/TypeCheck/Positive.hs | 60 +++++++- tests/CLI/help.test | 3 +- tests/negative/MicroJuvix/Positivity/E1.juvix | 8 + tests/negative/MicroJuvix/Positivity/E2.juvix | 9 ++ tests/negative/MicroJuvix/Positivity/E3.juvix | 8 + tests/negative/MicroJuvix/Positivity/E4.juvix | 12 ++ tests/negative/MicroJuvix/Positivity/E5.juvix | 16 ++ tests/negative/MicroJuvix/Positivity/E6.juvix | 8 + tests/negative/MicroJuvix/Positivity/E7.juvix | 11 ++ tests/negative/MicroJuvix/Positivity/E8.juvix | 5 + tests/negative/MicroJuvix/Positivity/E9.juvix | 11 ++ .../MicroJuvix/Positivity/NegParam.juvix | 5 + .../MicroJuvix/Positivity/errorE5.test | 6 + .../MicroJuvix/Positivity/errorE9.test | 6 + .../negative/MicroJuvix/Positivity/juvix.yaml | 0 tests/positive/MicroJuvix/Positivity/E5.juvix | 17 +++ .../positive/MicroJuvix/Positivity/juvix.yaml | 0 47 files changed, 649 insertions(+), 81 deletions(-) create mode 100644 docs/org/notes/strictly-positive-data-types.org create mode 100644 src/Juvix/Analysis/Positivity/Checker.hs create mode 100644 tests/negative/MicroJuvix/Positivity/E1.juvix create mode 100644 tests/negative/MicroJuvix/Positivity/E2.juvix create mode 100644 tests/negative/MicroJuvix/Positivity/E3.juvix create mode 100644 tests/negative/MicroJuvix/Positivity/E4.juvix create mode 100644 tests/negative/MicroJuvix/Positivity/E5.juvix create mode 100644 tests/negative/MicroJuvix/Positivity/E6.juvix create mode 100644 tests/negative/MicroJuvix/Positivity/E7.juvix create mode 100644 tests/negative/MicroJuvix/Positivity/E8.juvix create mode 100644 tests/negative/MicroJuvix/Positivity/E9.juvix create mode 100644 tests/negative/MicroJuvix/Positivity/NegParam.juvix create mode 100644 tests/negative/MicroJuvix/Positivity/errorE5.test create mode 100644 tests/negative/MicroJuvix/Positivity/errorE9.test create mode 100644 tests/negative/MicroJuvix/Positivity/juvix.yaml create mode 100644 tests/positive/MicroJuvix/Positivity/E5.juvix create mode 100644 tests/positive/MicroJuvix/Positivity/juvix.yaml diff --git a/app/GlobalOptions.hs b/app/GlobalOptions.hs index 2cf4b6835..d6b2f0e9a 100644 --- a/app/GlobalOptions.hs +++ b/app/GlobalOptions.hs @@ -12,6 +12,7 @@ data GlobalOptions = GlobalOptions _globalShowNameIds :: Bool, _globalOnlyErrors :: Bool, _globalNoTermination :: Bool, + _globalNoPositivity :: Bool, _globalNoStdlib :: Bool, _globalInputFiles :: [FilePath] } @@ -26,6 +27,7 @@ defaultGlobalOptions = _globalShowNameIds = False, _globalOnlyErrors = False, _globalNoTermination = False, + _globalNoPositivity = False, _globalNoStdlib = False, _globalInputFiles = [] } @@ -37,6 +39,7 @@ instance Semigroup GlobalOptions where _globalShowNameIds = o1 ^. globalShowNameIds || o2 ^. globalShowNameIds, _globalOnlyErrors = o1 ^. globalOnlyErrors || o2 ^. globalOnlyErrors, _globalNoTermination = o1 ^. globalNoTermination || o2 ^. globalNoTermination, + _globalNoPositivity = o1 ^. globalNoPositivity || o2 ^. globalNoPositivity, _globalNoStdlib = o1 ^. globalNoStdlib || o2 ^. globalNoStdlib, _globalInputFiles = o1 ^. globalInputFiles ++ o2 ^. globalInputFiles } @@ -73,6 +76,12 @@ parseGlobalFlags b = do <> help "Disable termination checking" <> hidden b ) + _globalNoPositivity <- + switch + ( long "no-positivity" + <> help "Disable positivity checking for inductive types" + <> hidden b + ) _globalNoStdlib <- switch ( long "no-stdlib" diff --git a/app/Main.hs b/app/Main.hs index 1fe759a53..bf2592451 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -73,6 +73,7 @@ getEntryPoint r opts = nonEmpty (opts ^. globalInputFiles) >>= Just <$> entryPoi EntryPoint { _entryPointRoot = r, _entryPointNoTermination = opts ^. globalNoTermination, + _entryPointNoPositivity = opts ^. globalNoPositivity, _entryPointNoStdlib = opts ^. globalNoStdlib, _entryPointModulePaths = l } diff --git a/docs/org/SUMMARY.org b/docs/org/SUMMARY.org index 525738295..daab6163b 100755 --- a/docs/org/SUMMARY.org +++ b/docs/org/SUMMARY.org @@ -34,6 +34,7 @@ - [[./notes/README.md][Notes]] - [[./examples/validity-predicates/README.md][Validity predicates]] - [[./notes/monomorphization.md][Monomorphization]] + - [[./notes/strictly-positive-data-types.md][Strictly positive data types]] - [[./introduction/about/what-is.md][About]] # - [[./introduction/about/team.md][The dev team]] diff --git a/docs/org/notes/strictly-positive-data-types.org b/docs/org/notes/strictly-positive-data-types.org new file mode 100644 index 000000000..628dbf15f --- /dev/null +++ b/docs/org/notes/strictly-positive-data-types.org @@ -0,0 +1,86 @@ +* Strictly positive data types + +We follow a syntactic description of strictly positive inductive data types. + +An inductive type is said to be _strictly positive_ if it does not occur or occurs +strictly positively in the types of the arguments of its constructors. A name +qualified as strictly positive for an inductive type if it never occurs at a negative +position in the types of the arguments of its constructors. We refer to a negative +position as those occurrences on the left of an arrow in a type constructor argument. + +In the example below, the type =X= occurs strictly positive in =c0= and negatively at +the constructor =c1=. Therefore, =X= is not strictly positive. + +#+begin_src minijuvix +axiom B : Type; +inductive X { + c0 : (B -> X) -> X; + c1 : (X -> X) -> X; +}; +#+end_src + +We could also refer to positive parameters as such parameters occurring in no negative positions. +For example, the type =B= in the =c0= constructor above is on the left of the arrow =B->X=. +Then, =B= is at a negative position. Negative parameters need to be considered when checking strictly +positive data types as they may allow to define non-strictly positive data types. + +In the example below, the type =T0= is strictly positive. However, the type =T1= is not. +Only after unfolding the type application =T0 (T1 A)= in the data constructor =c1=, we can +find out that =T1= occurs at a negative position because of =T0=. More precisely, +the type parameter =A= of =T0= is negative. + +#+begin_src minijuvix +inductive T0 (A : Type) { + c0 : (A -> T0 A) -> T0 A; +}; + +inductive T1 { + c1 : T0 T1 -> T1; +}; +#+end_src + + +** Bypass the strict positivity condition + +To bypass the positivity check, a data type declaration can be annotated +with the keyword =positive=. Another way is to use the CLI global flag =--no-positivity= +when typechecking a =Juvix= File. + +#+begin_example +$ cat tests/negative/MicroJuvix/NoStrictlyPositiveDataTypes/E5.mjuvix +module E5; + positive + inductive T0 (A : Type){ + c0 : (T0 A -> A) -> T0 A; + }; +end; +#+end_example + +** Examples of non-strictly data types + +- =NSPos= is at a negative position in =c=. + #+begin_src minijuvix + inductive Empty {}; + inductive NSPos { + c : ((NSPos -> Empty) -> NSPos) -> NSPos; + }; + #+end_src + +- =Bad= is not strictly positive beceause of the negative parameter =A= of =Tree=. + #+begin_src minijuvix + inductive Tree (A : Type) { + leaf : Tree A; + node : (A -> Tree A) -> Tree A; + }; + + inductive Bad { + bad : Tree Bad -> Bad; + }; + #+end_src + +- =A= is a negative parameter. + #+begin_src minijuvix + inductive B (A : Type) { + b : (A -> B (B A -> A)) -> B A; + }; + #+end_src diff --git a/src/Juvix/Analysis/Positivity/Checker.hs b/src/Juvix/Analysis/Positivity/Checker.hs new file mode 100644 index 000000000..aa7c3a82b --- /dev/null +++ b/src/Juvix/Analysis/Positivity/Checker.hs @@ -0,0 +1,140 @@ +module Juvix.Analysis.Positivity.Checker where + +import Data.HashMap.Strict qualified as HashMap +import Data.HashSet qualified as HashSet +import Juvix.Pipeline.EntryPoint qualified as E +import Juvix.Prelude hiding (fromEither) +import Juvix.Syntax.MicroJuvix.Error +import Juvix.Syntax.MicroJuvix.InfoTable +import Juvix.Syntax.MicroJuvix.Language.Extra + +------------------------------------------------------------------------------- +-- Checker for strictly positive inductive data types +------------------------------------------------------------------------------- + +type NegativeTypeParameters = HashSet VarName + +type ErrorReference = Maybe Expression + +type RecursionLimit = Int + +checkPositivity :: + Members + '[ Reader E.EntryPoint, + Reader InfoTable, + Error TypeCheckerError, + State NegativeTypeParameters + ] + r => + InductiveDef -> + Sem r () +checkPositivity ty = do + let indName = ty ^. inductiveName + numInductives <- HashMap.size <$> asks (^. infoInductives) + noCheckPositivity <- asks (^. E.entryPointNoPositivity) + forM_ (ty ^. inductiveConstructors) $ \ctor -> do + let ctorName = ctor ^. inductiveConstructorName + unless (noCheckPositivity || ty ^. inductivePositive) $ + mapM_ + (checkStrictlyPositiveOccurrences ty ctorName indName numInductives Nothing) + (ctor ^. inductiveConstructorParameters) + +checkStrictlyPositiveOccurrences :: + forall r. + Members '[Reader InfoTable, Error TypeCheckerError, State NegativeTypeParameters] r => + InductiveDef -> + ConstrName -> + Name -> + RecursionLimit -> + ErrorReference -> + Expression -> + Sem r () +checkStrictlyPositiveOccurrences ty ctorName name recLimit ref = helper False + where + indName :: Name + indName = ty ^. inductiveName + + -- The following `helper` function determines if there is any negative + -- occurence of the symbol `name` in the given expression. The `inside` flag + -- used below indicates whether the current search is performed on the left + -- of an inner arrow or not. + + helper :: Bool -> Expression -> Sem r () + helper inside expr = case expr of + ExpressionIden i -> helperIden i + ExpressionFunction (Function l r) -> helper True (l ^. paramType) >> helper inside r + ExpressionApplication tyApp -> helperApp tyApp + ExpressionLiteral {} -> return () + ExpressionHole {} -> return () + ExpressionUniverse {} -> return () + where + helperIden :: Iden -> Sem r () + helperIden = \case + IdenInductive ty' -> when (inside && name == ty') (strictlyPositivityError expr) + IdenVar name' + | not inside -> return () + | name == name' -> strictlyPositivityError expr + | InductiveParameter name' `elem` ty ^. inductiveParameters -> modify (HashSet.insert name') + | otherwise -> return () + _ -> return () + + helperApp :: Application -> Sem r () + helperApp tyApp = do + let (hdExpr, args) = unfoldApplication tyApp + case hdExpr of + ExpressionIden (IdenInductive ty') -> do + when (inside && name == ty') (strictlyPositivityError expr) + InductiveInfo indTy' <- lookupInductive ty' + + -- We now need to know whether `name` negatively occurs at `indTy'` + -- or not. The way to know is by checking that the type ty' + -- preserves the positivity condition, i.e., its type parameters + -- are no negative. + + let paramsTy' = indTy' ^. inductiveParameters + helperInductiveApp indTy' (zip paramsTy' (toList args)) + _ -> return () + + helperInductiveApp :: InductiveDef -> [(InductiveParameter, Expression)] -> Sem r () + helperInductiveApp typ = \case + ((InductiveParameter pName, arg) : ps) -> do + negParms :: NegativeTypeParameters <- get + when (varOrInductiveInExpression name arg) $ do + when (HashSet.member pName negParms) (strictlyPositivityError arg) + when (recLimit > 0) $ + forM_ (typ ^. inductiveConstructors) $ \ctor' -> + mapM_ + ( checkStrictlyPositiveOccurrences + ty + ctorName + pName + (recLimit - 1) + (Just (fromMaybe arg ref)) + ) + (ctor' ^. inductiveConstructorParameters) + >> modify (HashSet.insert pName) + helperInductiveApp ty ps + [] -> return () + + strictlyPositivityError :: Expression -> Sem r () + strictlyPositivityError expr = do + let errLoc = fromMaybe expr ref + throw + ( ErrNoPositivity $ + NoPositivity + { _noStrictPositivityType = indName, + _noStrictPositivityConstructor = ctorName, + _noStrictPositivityArgument = errLoc + } + ) + +varOrInductiveInExpression :: Name -> Expression -> Bool +varOrInductiveInExpression n = \case + ExpressionIden (IdenVar var) -> n == var + ExpressionIden (IdenInductive ty) -> n == ty + ExpressionApplication (Application l r _) -> + varOrInductiveInExpression n l || varOrInductiveInExpression n r + ExpressionFunction (Function l r) -> + varOrInductiveInExpression n (l ^. paramType) + || varOrInductiveInExpression n r + _ -> False diff --git a/src/Juvix/Internal/Strings.hs b/src/Juvix/Internal/Strings.hs index 05f68edaf..b3c8d4011 100644 --- a/src/Juvix/Internal/Strings.hs +++ b/src/Juvix/Internal/Strings.hs @@ -182,6 +182,9 @@ cBackend = "c" terminating :: IsString s => s terminating = "terminating" +positive :: IsString s => s +positive = "positive" + waveArrow :: IsString s => s waveArrow = "↝" diff --git a/src/Juvix/Pipeline/EntryPoint.hs b/src/Juvix/Pipeline/EntryPoint.hs index a4213f6e4..c34669fb4 100644 --- a/src/Juvix/Pipeline/EntryPoint.hs +++ b/src/Juvix/Pipeline/EntryPoint.hs @@ -9,6 +9,7 @@ import Juvix.Prelude data EntryPoint = EntryPoint { _entryPointRoot :: FilePath, _entryPointNoTermination :: Bool, + _entryPointNoPositivity :: Bool, _entryPointNoStdlib :: Bool, _entryPointModulePaths :: NonEmpty FilePath } @@ -19,6 +20,7 @@ defaultEntryPoint mainFile = EntryPoint { _entryPointRoot = ".", _entryPointNoTermination = False, + _entryPointNoPositivity = False, _entryPointNoStdlib = False, _entryPointModulePaths = pure mainFile } diff --git a/src/Juvix/Syntax/Abstract/Language.hs b/src/Juvix/Syntax/Abstract/Language.hs index ea22791de..8d4bebfbd 100644 --- a/src/Juvix/Syntax/Abstract/Language.hs +++ b/src/Juvix/Syntax/Abstract/Language.hs @@ -174,7 +174,8 @@ data InductiveDef = InductiveDef _inductiveBuiltin :: Maybe BuiltinInductive, _inductiveParameters :: [FunctionParameter], _inductiveType :: Expression, - _inductiveConstructors :: [InductiveConstructorDef] + _inductiveConstructors :: [InductiveConstructorDef], + _inductivePositive :: Bool } deriving stock (Eq, Show) diff --git a/src/Juvix/Syntax/Concrete/Language.hs b/src/Juvix/Syntax/Concrete/Language.hs index 04185ec3a..60a2a2ed7 100644 --- a/src/Juvix/Syntax/Concrete/Language.hs +++ b/src/Juvix/Syntax/Concrete/Language.hs @@ -248,7 +248,8 @@ data InductiveDef (s :: Stage) = InductiveDef _inductiveName :: InductiveName s, _inductiveParameters :: [InductiveParameter s], _inductiveType :: Maybe (ExpressionType s), - _inductiveConstructors :: [InductiveConstructorDef s] + _inductiveConstructors :: [InductiveConstructorDef s], + _inductivePositive :: Bool } deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (InductiveDef s) diff --git a/src/Juvix/Syntax/Concrete/Lexer.hs b/src/Juvix/Syntax/Concrete/Lexer.hs index f8f359e9b..8f81c5d2c 100644 --- a/src/Juvix/Syntax/Concrete/Lexer.hs +++ b/src/Juvix/Syntax/Concrete/Lexer.hs @@ -266,6 +266,9 @@ kwType = keyword Str.type_ kwTerminating :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () kwTerminating = keyword Str.terminating +kwPositive :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () +kwPositive = keyword Str.positive + kwUsing :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () kwUsing = keyword Str.using diff --git a/src/Juvix/Syntax/Concrete/Parser.hs b/src/Juvix/Syntax/Concrete/Parser.hs index a78ec1fd9..028868970 100644 --- a/src/Juvix/Syntax/Concrete/Parser.hs +++ b/src/Juvix/Syntax/Concrete/Parser.hs @@ -428,6 +428,7 @@ lambda = do inductiveDef :: Members '[Reader ParserParams, InfoTableBuilder] r => Maybe BuiltinInductive -> ParsecS r (InductiveDef 'Parsed) inductiveDef _inductiveBuiltin = do + _inductivePositive <- isJust <$> optional kwPositive kwInductive _inductiveName <- symbol _inductiveParameters <- P.many inductiveParam diff --git a/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs b/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs index a56e546ae..8cb43ab6b 100644 --- a/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs +++ b/src/Juvix/Syntax/Concrete/Scoped/Scoper.hs @@ -460,7 +460,7 @@ checkInductiveDef :: Members '[Error ScoperError, State Scope, State ScoperState, Reader LocalVars, InfoTableBuilder, NameIdGen] r => InductiveDef 'Parsed -> Sem r (InductiveDef 'Scoped) -checkInductiveDef InductiveDef {..} = do +checkInductiveDef ty@InductiveDef {..} = do withParams _inductiveParameters $ \inductiveParameters' -> do inductiveType' <- mapM checkParseExpressionAtoms _inductiveType inductiveName' <- bindInductiveSymbol _inductiveName @@ -471,7 +471,8 @@ checkInductiveDef InductiveDef {..} = do _inductiveBuiltin = _inductiveBuiltin, _inductiveParameters = inductiveParameters', _inductiveType = inductiveType', - _inductiveConstructors = inductiveConstructors' + _inductiveConstructors = inductiveConstructors', + _inductivePositive = ty ^. inductivePositive } checkTopModule_ :: diff --git a/src/Juvix/Syntax/MicroJuvix/Error.hs b/src/Juvix/Syntax/MicroJuvix/Error.hs index ac9ee79c2..b023c4a15 100644 --- a/src/Juvix/Syntax/MicroJuvix/Error.hs +++ b/src/Juvix/Syntax/MicroJuvix/Error.hs @@ -21,6 +21,7 @@ data TypeCheckerError | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType | ErrImpracticalPatternMatching ImpracticalPatternMatching + | ErrNoPositivity NoPositivity instance ToGenericError TypeCheckerError where genericError :: TypeCheckerError -> GenericError @@ -34,3 +35,4 @@ instance ToGenericError TypeCheckerError where ErrTooManyArgumentsIndType e -> genericError e ErrTooFewArgumentsIndType e -> genericError e ErrImpracticalPatternMatching e -> genericError e + ErrNoPositivity e -> genericError e diff --git a/src/Juvix/Syntax/MicroJuvix/Error/Types.hs b/src/Juvix/Syntax/MicroJuvix/Error/Types.hs index 8fcd473f9..50e58fb38 100644 --- a/src/Juvix/Syntax/MicroJuvix/Error/Types.hs +++ b/src/Juvix/Syntax/MicroJuvix/Error/Types.hs @@ -260,3 +260,32 @@ instance ToGenericError ImpracticalPatternMatching where <+> ppCode ty <+> "is not an inductive data type." <+> "Therefore, pattern-matching is not available here" + +data NoPositivity = NoPositivity + { _noStrictPositivityType :: Name, + _noStrictPositivityConstructor :: Name, + _noStrictPositivityArgument :: Expression + } + +makeLenses ''NoPositivity + +instance ToGenericError NoPositivity where + genericError e = + GenericError + { _genericErrorLoc = j, + _genericErrorMessage = prettyError msg, + _genericErrorIntervals = [i, j] + } + where + ty = e ^. noStrictPositivityType + ctor = e ^. noStrictPositivityConstructor + arg = e ^. noStrictPositivityArgument + i = getLoc ty + j = getLoc arg + msg = + "The type" + <+> ppCode ty + <+> "is not strictly positive." + <> line + <> "It appears at a negative position in one of the arguments of the constructor" + <+> ppCode ctor <> "." diff --git a/src/Juvix/Syntax/MicroJuvix/InfoTable.hs b/src/Juvix/Syntax/MicroJuvix/InfoTable.hs index ecc329fbd..db9ce62c1 100644 --- a/src/Juvix/Syntax/MicroJuvix/InfoTable.hs +++ b/src/Juvix/Syntax/MicroJuvix/InfoTable.hs @@ -73,14 +73,14 @@ buildTable1 m = InfoTable {..} <> buildTable (map (^. includeModule) includes) _infoConstructors :: HashMap Name ConstructorInfo _infoConstructors = HashMap.fromList - [ (c ^. constructorName, ConstructorInfo params args ind builtin) + [ (c ^. inductiveConstructorName, ConstructorInfo params args ind builtin) | StatementInductive d <- ss, let ind = d ^. inductiveName, let n = length (d ^. inductiveConstructors), let params = d ^. inductiveParameters, let builtins = maybe (replicate n Nothing) (map Just . builtinConstructors) (d ^. inductiveBuiltin), (builtin, c) <- zipExact builtins (d ^. inductiveConstructors), - let args = c ^. constructorParameters + let args = c ^. inductiveConstructorParameters ] _infoFunctions :: HashMap Name FunctionInfo _infoFunctions = @@ -126,7 +126,7 @@ constructorArgTypes i = i ^. constructorInfoArgs ) -constructorType :: Member (Reader InfoTable) r => Name -> Sem r Expression +constructorType :: Member (Reader InfoTable) r => ConstrName -> Sem r Expression constructorType c = do info <- lookupConstructor c let (inductiveParams, constrArgs) = constructorArgTypes info diff --git a/src/Juvix/Syntax/MicroJuvix/Language.hs b/src/Juvix/Syntax/MicroJuvix/Language.hs index 2403290ef..7b0c017ac 100644 --- a/src/Juvix/Syntax/MicroJuvix/Language.hs +++ b/src/Juvix/Syntax/MicroJuvix/Language.hs @@ -135,12 +135,14 @@ data InductiveDef = InductiveDef { _inductiveName :: InductiveName, _inductiveBuiltin :: Maybe BuiltinInductive, _inductiveParameters :: [InductiveParameter], - _inductiveConstructors :: [InductiveConstructorDef] + _inductiveConstructors :: [InductiveConstructorDef], + _inductivePositive :: Bool } data InductiveConstructorDef = InductiveConstructorDef - { _constructorName :: ConstrName, - _constructorParameters :: [Expression] + { _inductiveConstructorName :: ConstrName, + _inductiveConstructorParameters :: [Expression], + _inductiveConstructorReturnType :: Expression } data FunctionParameter = FunctionParameter diff --git a/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs b/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs index 872370073..a9a5f86d0 100644 --- a/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs +++ b/src/Juvix/Syntax/MicroJuvix/Language/Extra.hs @@ -381,10 +381,10 @@ unfoldApplication' :: Application -> (Expression, NonEmpty (IsImplicit, Expressi unfoldApplication' (Application l' r' i') = second (|: (i', r')) (unfoldExpressionApp l') unfoldExpressionApp :: Expression -> (Expression, [(IsImplicit, Expression)]) -unfoldExpressionApp e = case e of +unfoldExpressionApp = \case ExpressionApplication (Application l r i) -> second (`snoc` (i, r)) (unfoldExpressionApp l) - _ -> (e, []) + e -> (e, []) unfoldApplication :: Application -> (Expression, NonEmpty Expression) unfoldApplication = fmap (fmap snd) . unfoldApplication' diff --git a/src/Juvix/Syntax/MicroJuvix/MicroJuvixArityResult.hs b/src/Juvix/Syntax/MicroJuvix/MicroJuvixArityResult.hs index e29d68b77..d27ad1c0e 100644 --- a/src/Juvix/Syntax/MicroJuvix/MicroJuvixArityResult.hs +++ b/src/Juvix/Syntax/MicroJuvix/MicroJuvixArityResult.hs @@ -3,12 +3,13 @@ module Juvix.Syntax.MicroJuvix.MicroJuvixArityResult ) where +import Juvix.Pipeline.EntryPoint qualified as E import Juvix.Prelude import Juvix.Syntax.MicroJuvix.Language -import Juvix.Syntax.MicroJuvix.MicroJuvixResult (MicroJuvixResult) +import Juvix.Syntax.MicroJuvix.MicroJuvixResult qualified as M data MicroJuvixArityResult = MicroJuvixArityResult - { _resultMicroJuvixResult :: MicroJuvixResult, + { _resultMicroJuvixResult :: M.MicroJuvixResult, _resultModules :: NonEmpty Module } @@ -16,3 +17,6 @@ makeLenses ''MicroJuvixArityResult mainModule :: Lens' MicroJuvixArityResult Module mainModule = resultModules . _head + +microJuvixArityResultEntryPoint :: Lens' MicroJuvixArityResult E.EntryPoint +microJuvixArityResultEntryPoint = resultMicroJuvixResult . M.microJuvixResultEntryPoint diff --git a/src/Juvix/Syntax/MicroJuvix/MicroJuvixResult.hs b/src/Juvix/Syntax/MicroJuvix/MicroJuvixResult.hs index 93afe8569..37dc686a0 100644 --- a/src/Juvix/Syntax/MicroJuvix/MicroJuvixResult.hs +++ b/src/Juvix/Syntax/MicroJuvix/MicroJuvixResult.hs @@ -4,6 +4,7 @@ module Juvix.Syntax.MicroJuvix.MicroJuvixResult ) where +import Juvix.Pipeline.EntryPoint qualified as E import Juvix.Prelude import Juvix.Syntax.Abstract.AbstractResult qualified as Abstract import Juvix.Syntax.MicroJuvix.InfoTable @@ -16,3 +17,6 @@ data MicroJuvixResult = MicroJuvixResult } makeLenses ''MicroJuvixResult + +microJuvixResultEntryPoint :: Lens' MicroJuvixResult E.EntryPoint +microJuvixResultEntryPoint = resultAbstract . Abstract.abstractResultEntryPoint diff --git a/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs b/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs index 7a421dc74..ed40428c5 100644 --- a/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs +++ b/src/Juvix/Syntax/MicroJuvix/Pretty/Base.hs @@ -154,8 +154,8 @@ instance PrettyCode Hole where instance PrettyCode InductiveConstructorDef where ppCode c = do - constructorName' <- ppCode (c ^. constructorName) - constructorParameters' <- mapM ppCodeAtom (c ^. constructorParameters) + constructorName' <- ppCode (c ^. inductiveConstructorName) + constructorParameters' <- mapM ppCodeAtom (c ^. inductiveConstructorParameters) return (hsep $ constructorName' : constructorParameters') indent' :: Member (Reader Options) r => Doc a -> Sem r (Doc a) diff --git a/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs b/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs index f16dee28f..a6d8055cc 100644 --- a/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs +++ b/src/Juvix/Syntax/MicroJuvix/TypeChecker.hs @@ -6,7 +6,9 @@ module Juvix.Syntax.MicroJuvix.TypeChecker where import Data.HashMap.Strict qualified as HashMap +import Juvix.Analysis.Positivity.Checker import Juvix.Internal.NameIdGen +import Juvix.Pipeline.EntryPoint qualified as E import Juvix.Prelude hiding (fromEither) import Juvix.Syntax.MicroJuvix.Error import Juvix.Syntax.MicroJuvix.InfoTable @@ -21,15 +23,19 @@ addIdens idens = modify (HashMap.union idens) registerConstructor :: Members '[State TypesTable, Reader InfoTable] r => InductiveConstructorDef -> Sem r () registerConstructor ctr = do - ty <- constructorType (ctr ^. constructorName) - modify (HashMap.insert (ctr ^. constructorName) ty) + ty <- constructorType (ctr ^. inductiveConstructorName) + modify (HashMap.insert (ctr ^. inductiveConstructorName) ty) entryMicroJuvixTyped :: Members '[Error TypeCheckerError, NameIdGen] r => MicroJuvixArityResult -> Sem r MicroJuvixTypedResult entryMicroJuvixTyped res@MicroJuvixArityResult {..} = do - (idens, r) <- runState (mempty :: TypesTable) (runReader table (mapM checkModule _resultModules)) + (idens, r) <- + runState (mempty :: TypesTable) + . runReader entryPoint + . runReader table + $ mapM checkModule _resultModules return MicroJuvixTypedResult { _resultMicroJuvixArityResult = res, @@ -40,12 +46,16 @@ entryMicroJuvixTyped res@MicroJuvixArityResult {..} = do table :: InfoTable table = buildTable _resultModules + entryPoint :: E.EntryPoint + entryPoint = res ^. microJuvixArityResultEntryPoint + checkModule :: - Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r => + Members '[Reader E.EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r => Module -> Sem r Module checkModule Module {..} = do - _moduleBody' <- checkModuleBody _moduleBody + _moduleBody' <- + (evalState (mempty :: NegativeTypeParameters) . checkModuleBody) _moduleBody return Module { _moduleBody = _moduleBody', @@ -53,7 +63,8 @@ checkModule Module {..} = do } checkModuleBody :: - Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r => + forall r. + Members '[Reader E.EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters] r => ModuleBody -> Sem r ModuleBody checkModuleBody ModuleBody {..} = do @@ -64,19 +75,20 @@ checkModuleBody ModuleBody {..} = do } checkInclude :: - Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r => + Members '[Reader E.EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r => Include -> Sem r Include checkInclude = traverseOf includeModule checkModule checkStatement :: - Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable] r => + Members '[Reader E.EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State NegativeTypeParameters] r => Statement -> Sem r Statement checkStatement s = case s of StatementFunction fun -> StatementFunction <$> checkFunctionDef fun StatementForeign {} -> return s StatementInductive ind -> do + checkInductiveDef ind mapM_ registerConstructor (ind ^. inductiveConstructors) ty <- inductiveType (ind ^. inductiveName) modify (HashMap.insert (ind ^. inductiveName) ty) @@ -138,6 +150,55 @@ checkFunctionParameter (FunctionParameter mv i e) = do e' <- checkExpression (smallUniverse (getLoc e)) e return (FunctionParameter mv i e') +checkInductiveDef :: + Members '[Reader InfoTable, Error TypeCheckerError, State NegativeTypeParameters, Reader E.EntryPoint] r => + InductiveDef -> + Sem r () +checkInductiveDef ty@InductiveDef {..} = do + checkPositivity ty + mapM_ (checkConstructorDef ty) _inductiveConstructors + +checkConstructorDef :: + Members + '[ Reader E.EntryPoint, + Reader InfoTable, + Error TypeCheckerError, + State NegativeTypeParameters + ] + r => + InductiveDef -> + InductiveConstructorDef -> + Sem r () +checkConstructorDef ty ctor = do + checkConstructorReturnType ty ctor + +checkConstructorReturnType :: + Members '[Reader InfoTable, Error TypeCheckerError] r => + InductiveDef -> + InductiveConstructorDef -> + Sem r () +checkConstructorReturnType indType ctor = do + let ctorName = ctor ^. inductiveConstructorName + ctorReturnType = ctor ^. inductiveConstructorReturnType + tyName = indType ^. inductiveName + indParams = map (^. inductiveParamName) (indType ^. inductiveParameters) + expectedReturnType = + foldExplicitApplication + (ExpressionIden (IdenInductive tyName)) + (map (ExpressionIden . IdenVar) indParams) + when + (ctorReturnType /= expectedReturnType) + ( throw + ( ErrWrongReturnType + ( WrongReturnType + { _wrongReturnTypeConstructorName = ctorName, + _wrongReturnTypeExpected = expectedReturnType, + _wrongReturnTypeActual = ctorReturnType + } + ) + ) + ) + inferExpression :: Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r => Expression -> diff --git a/src/Juvix/Syntax/Universe.hs b/src/Juvix/Syntax/Universe.hs index f9f2629c6..38baf2f79 100644 --- a/src/Juvix/Syntax/Universe.hs +++ b/src/Juvix/Syntax/Universe.hs @@ -12,7 +12,7 @@ data Universe = Universe newtype SmallUniverse = SmallUniverse { _smallUniverseLoc :: Interval } - deriving stock (Generic) + deriving stock (Generic, Show) instance Eq SmallUniverse where _ == _ = True diff --git a/src/Juvix/Translation/AbstractToMicroJuvix.hs b/src/Juvix/Translation/AbstractToMicroJuvix.hs index 10ad4296c..4f85e0ad9 100644 --- a/src/Juvix/Translation/AbstractToMicroJuvix.hs +++ b/src/Juvix/Translation/AbstractToMicroJuvix.hs @@ -267,8 +267,6 @@ goInductiveParameter f = (Nothing, _, _) -> unsupported "unnamed inductive parameters" goInductiveDef :: - forall r. - Member (Error TypeCheckerError) r => Abstract.InductiveDef -> Sem r InductiveDef goInductiveDef i = @@ -277,44 +275,28 @@ goInductiveDef i = | otherwise -> do inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters) let indTypeName = i ^. Abstract.inductiveName - indParamNames = map (^. inductiveParamName) inductiveParameters' - inductiveConstructors' <- mapM (goConstructorDef indTypeName indParamNames) (i ^. Abstract.inductiveConstructors) + inductiveConstructors' <- + mapM + goConstructorDef + (i ^. Abstract.inductiveConstructors) return InductiveDef { _inductiveName = indTypeName, _inductiveParameters = inductiveParameters', _inductiveBuiltin = i ^. Abstract.inductiveBuiltin, - _inductiveConstructors = inductiveConstructors' + _inductiveConstructors = inductiveConstructors', + _inductivePositive = i ^. Abstract.inductivePositive } where - goConstructorDef :: Name -> [Name] -> Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef - goConstructorDef indName paramNames c = do - (_constructorParameters', actualReturnType) <- viewConstructorType (c ^. Abstract.constructorType) - let ctorName = c ^. Abstract.constructorName - foldTypeAppName :: Name -> [Name] -> Expression - foldTypeAppName tyName indParams = - foldExplicitApplication - (ExpressionIden (IdenInductive tyName)) - (map (ExpressionIden . IdenVar) indParams) - expectedReturnType :: Expression - expectedReturnType = foldTypeAppName indName paramNames - if - | actualReturnType == expectedReturnType -> - return - InductiveConstructorDef - { _constructorName = ctorName, - _constructorParameters = _constructorParameters' - } - | otherwise -> - throw - ( ErrWrongReturnType - ( WrongReturnType - { _wrongReturnTypeConstructorName = ctorName, - _wrongReturnTypeExpected = expectedReturnType, - _wrongReturnTypeActual = actualReturnType - } - ) - ) + goConstructorDef :: Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef + goConstructorDef c = do + (cParams, cReturnType) <- viewConstructorType (c ^. Abstract.constructorType) + return + InductiveConstructorDef + { _inductiveConstructorName = c ^. Abstract.constructorName, + _inductiveConstructorParameters = cParams, + _inductiveConstructorReturnType = cReturnType + } goTypeApplication :: Abstract.Application -> Sem r Application goTypeApplication (Abstract.Application l r i) = do diff --git a/src/Juvix/Translation/MicroJuvixToMiniC.hs b/src/Juvix/Translation/MicroJuvixToMiniC.hs index da7eb728b..687ace3ea 100644 --- a/src/Juvix/Translation/MicroJuvixToMiniC.hs +++ b/src/Juvix/Translation/MicroJuvixToMiniC.hs @@ -485,7 +485,7 @@ mkInductiveName :: Micro.InductiveDef -> Text mkInductiveName i = mkName (i ^. Micro.inductiveName) mkInductiveConstructorNames :: Micro.InductiveDef -> [Text] -mkInductiveConstructorNames i = mkName . view Micro.constructorName <$> i ^. Micro.inductiveConstructors +mkInductiveConstructorNames i = mkName . view Micro.inductiveConstructorName <$> i ^. Micro.inductiveConstructors mkInductiveTypeDef :: Micro.InductiveDef -> [CCode] mkInductiveTypeDef i = @@ -638,13 +638,13 @@ goInductiveConstructorNew i ctor = ctorNewFun ctorNewFun = if null ctorParams then return ctorNewNullary else ctorNewNary baseName :: Text - baseName = mkName (ctor ^. Micro.constructorName) + baseName = mkName (ctor ^. Micro.inductiveConstructorName) inductiveName :: Text inductiveName = mkInductiveName i ctorParams :: [Micro.PolyType] - ctorParams = map mkPolyType' (ctor ^. Micro.constructorParameters) + ctorParams = map mkPolyType' (ctor ^. Micro.inductiveConstructorParameters) ctorNewNullary :: [CCode] ctorNewNullary = @@ -791,7 +791,7 @@ goInductiveConstructorNew i ctor = ctorNewFun ) inductiveCtorParams :: Members '[Reader Micro.InfoTable] r => Micro.InductiveConstructorDef -> Sem r [CDeclType] -inductiveCtorParams ctor = mapM (goType . mkPolyType') (ctor ^. Micro.constructorParameters) +inductiveCtorParams ctor = mapM (goType . mkPolyType') (ctor ^. Micro.inductiveConstructorParameters) inductiveCtorArgs :: Members '[Reader Micro.InfoTable] r => Micro.InductiveConstructorDef -> Sem r [Declaration] inductiveCtorArgs ctor = namedArgs asCtorArg <$> inductiveCtorParams ctor @@ -814,10 +814,10 @@ goInductiveConstructorDef ctor = do ctorDecl = if null ctorParams then return ctorBool else ctorStruct baseName :: Text - baseName = mkName (ctor ^. Micro.constructorName) + baseName = mkName (ctor ^. Micro.inductiveConstructorName) ctorParams :: [Micro.PolyType] - ctorParams = map mkPolyType' (ctor ^. Micro.constructorParameters) + ctorParams = map mkPolyType' (ctor ^. Micro.inductiveConstructorParameters) ctorBool :: Declaration ctorBool = typeDefWrap (asTypeDef baseName) BoolType @@ -848,7 +848,7 @@ goProjections inductiveTypeDef ctor = do return (ExternalFunc <$> zipWith projFunction [0 ..] params) where baseName :: Text - baseName = mkName (ctor ^. Micro.constructorName) + baseName = mkName (ctor ^. Micro.inductiveConstructorName) localName :: Text localName = "a" diff --git a/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs b/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs index 94aa25398..f0ef2b059 100644 --- a/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs +++ b/src/Juvix/Translation/MicroJuvixToMonoJuvix.hs @@ -125,7 +125,7 @@ buildConcreteTable info = let def :: Micro.InductiveDef def = info ^?! Micro.infoInductives . at ind . _Just . Micro.inductiveInfoDef constructorNames :: [Micro.Name] - constructorNames = def ^.. Micro.inductiveConstructors . each . Micro.constructorName + constructorNames = def ^.. Micro.inductiveConstructors . each . Micro.inductiveConstructorName k :: NonEmpty Micro.ConcreteType k = tc ^. Micro.typeCallArguments iden :: PolyIden @@ -265,10 +265,10 @@ goInductiveDefConcrete def = do where goConstructor :: Micro.InductiveConstructorDef -> Sem r InductiveConstructorDef goConstructor c = do - params' <- mapM (goType . Micro.mkConcreteType') (c ^. Micro.constructorParameters) + params' <- mapM (goType . Micro.mkConcreteType') (c ^. Micro.inductiveConstructorParameters) return InductiveConstructorDef - { _constructorName = c ^. Micro.constructorName, + { _constructorName = c ^. Micro.inductiveConstructorName, _constructorParameters = params' } @@ -380,14 +380,14 @@ goInductiveDefPoly def poly where goConstructorDef :: Micro.InductiveConstructorDef -> Sem r InductiveConstructorDef goConstructorDef cdef = do - cpolyInfo <- fromJust <$> lookupPolyConstructor (cdef ^. Micro.constructorName) + cpolyInfo <- fromJust <$> lookupPolyConstructor (cdef ^. Micro.inductiveConstructorName) let concrete :: ConcreteIdenInfo concrete = fromJust (cpolyInfo ^. polyConcretes . at k) params :: [Micro.ConcreteType] params = map (Micro.substitutionConcrete (concrete ^. concreteTypeSubs)) - (cdef ^. Micro.constructorParameters) + (cdef ^. Micro.inductiveConstructorParameters) _constructorParameters <- mapM goType params return InductiveConstructorDef diff --git a/src/Juvix/Translation/MicroJuvixToMonoJuvix/TypeCallsMapBuilder.hs b/src/Juvix/Translation/MicroJuvixToMonoJuvix/TypeCallsMapBuilder.hs index 8643fa32f..2ce1a86f4 100644 --- a/src/Juvix/Translation/MicroJuvixToMonoJuvix/TypeCallsMapBuilder.hs +++ b/src/Juvix/Translation/MicroJuvixToMonoJuvix/TypeCallsMapBuilder.hs @@ -57,7 +57,7 @@ goInductiveParameter :: InductiveParameter -> Sem r () goInductiveParameter _ = return () goInductiveConstructorDef :: Members '[State TypeCallsMap, Reader Caller, Reader InfoTable] r => InductiveConstructorDef -> Sem r () -goInductiveConstructorDef c = mapM_ goExpression (c ^. constructorParameters) +goInductiveConstructorDef c = mapM_ goExpression (c ^. inductiveConstructorParameters) goParam :: Members '[State TypeCallsMap, Reader Caller, Reader InfoTable] r => FunctionParameter -> Sem r () goParam (FunctionParameter _ _ ty) = goExpression ty diff --git a/src/Juvix/Translation/ScopedToAbstract.hs b/src/Juvix/Translation/ScopedToAbstract.hs index 9bc669dde..40ff7d58b 100644 --- a/src/Juvix/Translation/ScopedToAbstract.hs +++ b/src/Juvix/Translation/ScopedToAbstract.hs @@ -241,7 +241,7 @@ goInductive :: Members '[InfoTableBuilder, Builtins, Error ScoperError] r => InductiveDef 'Scoped -> Sem r Abstract.InductiveDef -goInductive InductiveDef {..} = do +goInductive ty@InductiveDef {..} = do _inductiveParameters' <- mapM goInductiveParameter _inductiveParameters _inductiveType' <- mapM goExpression _inductiveType _inductiveConstructors' <- mapM goConstructorDef _inductiveConstructors @@ -252,7 +252,8 @@ goInductive InductiveDef {..} = do _inductiveBuiltin = _inductiveBuiltin, _inductiveName = goSymbol _inductiveName, _inductiveType = fromMaybe (Abstract.ExpressionUniverse (smallUniverse loc)) _inductiveType', - _inductiveConstructors = _inductiveConstructors' + _inductiveConstructors = _inductiveConstructors', + _inductivePositive = ty ^. inductivePositive } whenJust _inductiveBuiltin (registerBuiltinInductive indDef) inductiveInfo <- registerInductive indDef diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs index 9cf8be078..fd2de294e 100644 --- a/test/Scope/Positive.hs +++ b/test/Scope/Positive.hs @@ -40,6 +40,7 @@ testDescr PosTest {..} = EntryPoint { _entryPointRoot = cwd, _entryPointNoTermination = False, + _entryPointNoPositivity = False, _entryPointNoStdlib = noStdlib, _entryPointModulePaths = pure entryFile } diff --git a/test/Termination/Positive.hs b/test/Termination/Positive.hs index 10b9d2102..5102942b9 100644 --- a/test/Termination/Positive.hs +++ b/test/Termination/Positive.hs @@ -38,7 +38,15 @@ testDescrFlag N.NegTest {..} = { _testName = _name, _testRoot = tRoot, _testAssertion = Single $ do - let entryPoint = EntryPoint "." True True (pure _file) + let entryPoint = + EntryPoint + { _entryPointRoot = ".", + _entryPointNoTermination = True, + _entryPointNoPositivity = False, + _entryPointNoStdlib = True, + _entryPointModulePaths = pure _file + } + (void . runIO) (upToMicroJuvix entryPoint) } @@ -70,7 +78,7 @@ allTests = "Well-known terminating functions" (map (mkTest . testDescr) tests), testGroup - "Bypass checking using --non-termination flag on negative tests" + "Bypass termination checking using --non-termination flag on negative tests" (map (mkTest . testDescrFlag) negTests), testGroup "Terminating keyword" diff --git a/test/TypeCheck/Negative.hs b/test/TypeCheck/Negative.hs index 499d3e3ad..17bd9cf59 100644 --- a/test/TypeCheck/Negative.hs +++ b/test/TypeCheck/Negative.hs @@ -1,4 +1,4 @@ -module TypeCheck.Negative (allTests) where +module TypeCheck.Negative where import Base import Juvix.Pipeline @@ -31,8 +31,14 @@ testDescr NegTest {..} = allTests :: TestTree allTests = testGroup - "TypeCheck negative tests" - (map (mkTest . testDescr) tests) + "Typecheck negative tests" + [ testGroup + "General typechecking errors" + (map (mkTest . testDescr) tests), + testGroup + "Non-strictly positive data types" + (map (mkTest . testDescr) negPositivityTests) + ] root :: FilePath root = "tests/negative" @@ -113,3 +119,43 @@ tests = ErrWrongReturnType {} -> Nothing _ -> wrongError ] + +negPositivityTests :: [NegTest] +negPositivityTests = + [ NegTest "E1" "MicroJuvix/Positivity" "E1.juvix" $ + \case + ErrNoPositivity {} -> Nothing + _ -> wrongError, + NegTest "E2" "MicroJuvix/Positivity" "E2.juvix" $ + \case + ErrNoPositivity {} -> Nothing + _ -> wrongError, + NegTest "E3" "MicroJuvix/Positivity" "E3.juvix" $ + \case + ErrNoPositivity {} -> Nothing + _ -> wrongError, + NegTest "E4" "MicroJuvix/Positivity" "E4.juvix" $ + \case + ErrNoPositivity {} -> Nothing + _ -> wrongError, + NegTest "E5" "MicroJuvix/Positivity" "E5.juvix" $ + \case + ErrNoPositivity {} -> Nothing + _ -> wrongError, + NegTest "E6" "MicroJuvix/Positivity" "E6.juvix" $ + \case + ErrNoPositivity {} -> Nothing + _ -> wrongError, + NegTest "E7" "MicroJuvix/Positivity" "E7.juvix" $ + \case + ErrNoPositivity {} -> Nothing + _ -> wrongError, + NegTest "E8" "MicroJuvix/Positivity" "E8.juvix" $ + \case + ErrNoPositivity {} -> Nothing + _ -> wrongError, + NegTest "E9" "MicroJuvix/Positivity" "E9.juvix" $ + \case + ErrNoPositivity {} -> Nothing + _ -> wrongError + ] diff --git a/test/TypeCheck/Positive.hs b/test/TypeCheck/Positive.hs index 252cd8300..2b0519965 100644 --- a/test/TypeCheck/Positive.hs +++ b/test/TypeCheck/Positive.hs @@ -2,6 +2,7 @@ module TypeCheck.Positive where import Base import Juvix.Pipeline +import TypeCheck.Negative qualified as N data PosTest = PosTest { _name :: String, @@ -23,11 +24,66 @@ testDescr PosTest {..} = (void . runIO) (upToMicroJuvixTyped entryPoint) } +-------------------------------------------------------------------------------- +-- Testing --no-positivity flag with all related negative tests +-------------------------------------------------------------------------------- + +rootNegTests :: FilePath +rootNegTests = "tests/negative/" + +testNoPositivityFlag :: N.NegTest -> TestDescr +testNoPositivityFlag N.NegTest {..} = + let tRoot = rootNegTests _relDir + in TestDescr + { _testName = _name, + _testRoot = tRoot, + _testAssertion = Single $ do + let entryPoint = + EntryPoint + { _entryPointRoot = ".", + _entryPointNoTermination = False, + _entryPointNoPositivity = True, + _entryPointNoStdlib = False, + _entryPointModulePaths = pure _file + } + + (void . runIO) (upToMicroJuvix entryPoint) + } + +negPositivityTests :: [N.NegTest] +negPositivityTests = N.negPositivityTests + +testPositivityKeyword :: [PosTest] +testPositivityKeyword = + [ PosTest + "Mark T0 data type as strictly positive" + "MicroJuvix/Positivity" + "E5.juvix" + ] + +positivityTestGroup :: TestTree +positivityTestGroup = + testGroup + "Positive tests for the positivity condition" + [ testGroup + "Bypass positivity checking using --non-positivity flag on negative tests" + (map (mkTest . testNoPositivityFlag) negPositivityTests), + testGroup + "Usages of the positive keyword" + (map (mkTest . testDescr) testPositivityKeyword) + ] + +-------------------------------------------------------------------------------- + allTests :: TestTree allTests = testGroup - "Scope positive tests" - (map (mkTest . testDescr) tests) + "Typecheck positive tests" + [ testGroup + "General typechecking tests" + (map (mkTest . testDescr) tests), + positivityTestGroup + ] tests :: [PosTest] tests = diff --git a/tests/CLI/help.test b/tests/CLI/help.test index c3d3af91f..e179931ff 100644 --- a/tests/CLI/help.test +++ b/tests/CLI/help.test @@ -1,6 +1,7 @@ $ juvix --help > /Usage: juvix \(\(\-v\|\-\-version\) \| \(\-h\|\-\-help\) \| \[\-\-no\-colors\] \[\-\-show\-name\-ids\] - \[\-\-only\-errors\] \[\-\-no\-termination\] \[\-\-no\-stdlib\] COMMAND\).*/ + \[\-\-only\-errors\] \[\-\-no\-termination\] \[\-\-no\-positivity\] + \[\-\-no\-stdlib\] COMMAND\).*/ >= 0 diff --git a/tests/negative/MicroJuvix/Positivity/E1.juvix b/tests/negative/MicroJuvix/Positivity/E1.juvix new file mode 100644 index 000000000..bbf42ee8e --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/E1.juvix @@ -0,0 +1,8 @@ +module E1; + +axiom B : Type; +inductive X { + c : (X -> B) -> X; +}; + +end; \ No newline at end of file diff --git a/tests/negative/MicroJuvix/Positivity/E2.juvix b/tests/negative/MicroJuvix/Positivity/E2.juvix new file mode 100644 index 000000000..d648dcaf1 --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/E2.juvix @@ -0,0 +1,9 @@ +module E2; + +open import NegParam; + +inductive D { +d : T D -> D; +}; + +end; diff --git a/tests/negative/MicroJuvix/Positivity/E3.juvix b/tests/negative/MicroJuvix/Positivity/E3.juvix new file mode 100644 index 000000000..083a9c0c7 --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/E3.juvix @@ -0,0 +1,8 @@ +module E3; + +axiom B : Type; +inductive X { + c : B -> (X -> B) -> X; +}; + +end; diff --git a/tests/negative/MicroJuvix/Positivity/E4.juvix b/tests/negative/MicroJuvix/Positivity/E4.juvix new file mode 100644 index 000000000..a7284ca02 --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/E4.juvix @@ -0,0 +1,12 @@ +module E4; + +inductive Tree (A : Type) { + leaf : Tree A; + node : (A -> Tree A) -> Tree A; +}; + +inductive Bad { + bad : Tree Bad -> Bad; +}; + +end; diff --git a/tests/negative/MicroJuvix/Positivity/E5.juvix b/tests/negative/MicroJuvix/Positivity/E5.juvix new file mode 100644 index 000000000..30445ddbf --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/E5.juvix @@ -0,0 +1,16 @@ +module E5; + +inductive T0 (A : Type){ +c0 : (A -> T0 A) -> T0 A; +}; + +axiom B : Type; +inductive T1 (A : Type) { +c1 : (B -> T0 A) -> T1 A; +}; + +inductive T2 { +c2 : (B -> (B -> T1 T2)) -> T2; +}; + +end; diff --git a/tests/negative/MicroJuvix/Positivity/E6.juvix b/tests/negative/MicroJuvix/Positivity/E6.juvix new file mode 100644 index 000000000..c919d837c --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/E6.juvix @@ -0,0 +1,8 @@ +module E6; + +axiom A : Type; +inductive T (A : Type) { +c : (A -> (A -> (T A -> A))) -> T A; +}; + +end; diff --git a/tests/negative/MicroJuvix/Positivity/E7.juvix b/tests/negative/MicroJuvix/Positivity/E7.juvix new file mode 100644 index 000000000..87902c48a --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/E7.juvix @@ -0,0 +1,11 @@ +module E7; + +inductive T0 (A : Type) (B : Type) { +c0 : (B -> A) -> T0 A B; +}; + +inductive T1 (A : Type) { +c1 : (A -> T0 A (T1 A)) -> T1 A; +}; + +end; diff --git a/tests/negative/MicroJuvix/Positivity/E8.juvix b/tests/negative/MicroJuvix/Positivity/E8.juvix new file mode 100644 index 000000000..dbaf2edba --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/E8.juvix @@ -0,0 +1,5 @@ +module E8; +inductive B (A : Type) { +b : (A -> B (B A -> A)) -> B A; +}; +end; diff --git a/tests/negative/MicroJuvix/Positivity/E9.juvix b/tests/negative/MicroJuvix/Positivity/E9.juvix new file mode 100644 index 000000000..776583018 --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/E9.juvix @@ -0,0 +1,11 @@ +module E9; + +inductive B { +b : B; +}; + +inductive T { + c : ((B → T) -> T) -> T; +}; + +end; \ No newline at end of file diff --git a/tests/negative/MicroJuvix/Positivity/NegParam.juvix b/tests/negative/MicroJuvix/Positivity/NegParam.juvix new file mode 100644 index 000000000..d09e21dfb --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/NegParam.juvix @@ -0,0 +1,5 @@ +module NegParam; +inductive T (A : Type) { +c : (A -> T A) -> T A; +}; +end; diff --git a/tests/negative/MicroJuvix/Positivity/errorE5.test b/tests/negative/MicroJuvix/Positivity/errorE5.test new file mode 100644 index 000000000..0da5b2d3e --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/errorE5.test @@ -0,0 +1,6 @@ +$ juvix typecheck tests/negative/MicroJuvix/Positivity/E5.juvix --no-colors +>2 /.*\.juvix\:13:21\-23\: error\: +The type T2 is not strictly positive. +It appears at a negative position in one of the arguments of the constructor c2. +/ +>= 1 \ No newline at end of file diff --git a/tests/negative/MicroJuvix/Positivity/errorE9.test b/tests/negative/MicroJuvix/Positivity/errorE9.test new file mode 100644 index 000000000..5e4efb1ca --- /dev/null +++ b/tests/negative/MicroJuvix/Positivity/errorE9.test @@ -0,0 +1,6 @@ +$ juvix typecheck tests/negative/MicroJuvix/Positivity/E9.juvix --no-colors +>2 /.*\.juvix\:8:13\-14\: error\: +The type T is not strictly positive. +It appears at a negative position in one of the arguments of the constructor c. +/ +>= 1 \ No newline at end of file diff --git a/tests/negative/MicroJuvix/Positivity/juvix.yaml b/tests/negative/MicroJuvix/Positivity/juvix.yaml new file mode 100644 index 000000000..e69de29bb diff --git a/tests/positive/MicroJuvix/Positivity/E5.juvix b/tests/positive/MicroJuvix/Positivity/E5.juvix new file mode 100644 index 000000000..b2e467f39 --- /dev/null +++ b/tests/positive/MicroJuvix/Positivity/E5.juvix @@ -0,0 +1,17 @@ +module E5; + +inductive T0 (A : Type){ +c0 : (A -> T0 A) -> T0 A; +}; + +axiom B : Type; +inductive T1 (A : Type) { +c1 : (B -> T0 A) -> T1 A; +}; + +positive +inductive T2 { +c2 : (B -> (B -> T1 T2)) -> T2; +}; + +end; diff --git a/tests/positive/MicroJuvix/Positivity/juvix.yaml b/tests/positive/MicroJuvix/Positivity/juvix.yaml new file mode 100644 index 000000000..e69de29bb