From 4f607bab4eeb8dd59474180bc9759d715b77bc3b Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 27 Sep 2024 23:36:48 +0200 Subject: [PATCH] remove old code --- .../FromInternal/Analysis/Positivity.hs | 6 +- .../Analysis/Positivity/Checker.hs | 250 ------------------ .../FromInternal/Analysis/Positivity/Error.hs | 18 -- .../Analysis/TypeChecking/CheckerNew.hs | 16 +- .../Analysis/TypeChecking/Error.hs | 4 - test/Typecheck/Negative.hs | 1 - test/Typecheck/NegativeNew.hs | 7 +- 7 files changed, 12 insertions(+), 290 deletions(-) delete mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs delete mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs index 98c2a83dc7..c96a099916 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs @@ -1,8 +1,6 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity - ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker, - module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error, + ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.CheckerNew, ) where -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.CheckerNew diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs deleted file mode 100644 index 621089b2cb..0000000000 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ /dev/null @@ -1,250 +0,0 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker where - -import Data.HashMap.Strict qualified as HashMap -import Data.HashSet qualified as HashSet -import Juvix.Compiler.Internal.Data.InfoTable -import Juvix.Compiler.Internal.Extra -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error -import Juvix.Compiler.Pipeline.EntryPoint qualified as E -import Juvix.Prelude hiding (fromEither) - -type NegativeTypeParameters = HashSet VarName - -type CheckPositivityEffects r = - Members - '[ Reader E.EntryPoint, - Reader InfoTable, - Error TypeCheckerError, - Inference, - State NegativeTypeParameters - ] - r - -data CheckPositivityArgs = CheckPositivityArgs - { _checkPositivityArgsInductive :: InductiveInfo, - _checkPositivityArgsConstructorName :: Name, - _checkPositivityArgsInductiveName :: Name, - _checkPositivityArgsRecursionLimit :: Int, - _checkPositivityArgsErrorReference :: Maybe Expression, - _checkPositivityArgsTypeOfConstructorArg :: Expression - } - -makeLenses ''CheckPositivityArgs - -checkPositivity :: - forall r. - (CheckPositivityEffects r) => - InductiveInfo -> - Sem r () -checkPositivity indInfo = do - unlessM (asks (^. E.entryPointNoPositivity)) $ - forM_ (indInfo ^. inductiveInfoConstructors) $ \ctorName -> do - ctor <- asks (fromJust . HashMap.lookup ctorName . (^. infoConstructors)) - unless (indInfo ^. inductiveInfoPositive) $ do - numInductives <- length <$> asks (^. infoInductives) - forM_ - (constructorArgs (ctor ^. constructorInfoType)) - $ \typeOfConstr -> - checkStrictlyPositiveOccurrences - CheckPositivityArgs - { _checkPositivityArgsInductive = indInfo, - _checkPositivityArgsConstructorName = ctorName, - _checkPositivityArgsInductiveName = indInfo ^. inductiveInfoName, - _checkPositivityArgsRecursionLimit = numInductives, - _checkPositivityArgsErrorReference = Nothing, - _checkPositivityArgsTypeOfConstructorArg = typeOfConstr ^. paramType - } - -checkStrictlyPositiveOccurrences :: - forall r. - (CheckPositivityEffects r) => - CheckPositivityArgs -> - Sem r () -checkStrictlyPositiveOccurrences p = do - -- traceM (prettyText (p ^. checkPositivityArgsInductiveName) <> " # " <> prettyText (p ^. checkPositivityArgsConstructorName)) - typeOfConstrArg <- strongNormalize_ (p ^. checkPositivityArgsTypeOfConstructorArg) - goExpression False typeOfConstrArg - where - indInfo = p ^. checkPositivityArgsInductive - ctorName = p ^. checkPositivityArgsConstructorName - name = p ^. checkPositivityArgsInductiveName - recLimit = p ^. checkPositivityArgsRecursionLimit - ref = p ^. checkPositivityArgsErrorReference - - indName :: Name - indName = indInfo ^. inductiveInfoName - - {- The following `go` function determines if there is any negative - occurrence 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. - -} - goExpression :: Bool -> Expression -> Sem r () - goExpression inside expr = case expr of - ExpressionApplication tyApp -> goApp tyApp - ExpressionCase l -> goCase l - ExpressionFunction (Function l r) -> goLeft (l ^. paramType) >> go r - ExpressionHole {} -> return () - ExpressionInstanceHole {} -> return () - ExpressionIden i -> goIden i - ExpressionLambda l -> goLambda l - ExpressionLet l -> goLet l - ExpressionLiteral {} -> return () - ExpressionSimpleLambda l -> goSimpleLambda l - ExpressionUniverse {} -> return () - where - go :: Expression -> Sem r () - go = goExpression inside - - goLeft :: Expression -> Sem r () - goLeft = goExpression True - - goCase :: Case -> Sem r () - goCase l = do - go (l ^. caseExpression) - mapM_ goCaseBranch (l ^. caseBranches) - - goSideIfBranch :: SideIfBranch -> Sem r () - goSideIfBranch b = do - go (b ^. sideIfBranchCondition) - go (b ^. sideIfBranchBody) - - goSideIfs :: SideIfs -> Sem r () - goSideIfs s = do - mapM_ goSideIfBranch (s ^. sideIfBranches) - mapM_ go (s ^. sideIfElse) - - goCaseBranchRhs :: CaseBranchRhs -> Sem r () - goCaseBranchRhs = \case - CaseBranchRhsExpression e -> go e - CaseBranchRhsIf s -> goSideIfs s - - goCaseBranch :: CaseBranch -> Sem r () - goCaseBranch b = goCaseBranchRhs (b ^. caseBranchRhs) - - goLet :: Let -> Sem r () - goLet l = do - go (l ^. letExpression) - mapM_ goLetClause (l ^. letClauses) - - goLetClause :: LetClause -> Sem r () - goLetClause = \case - LetFunDef f -> goFunctionDef f - LetMutualBlock b -> goMutualBlockLet b - - goMutualBlockLet :: MutualBlockLet -> Sem r () - goMutualBlockLet b = mapM_ goFunctionDef (b ^. mutualLet) - - goFunctionDef :: FunctionDef -> Sem r () - goFunctionDef d = do - go (d ^. funDefType) - go (d ^. funDefBody) - - goSimpleLambda :: SimpleLambda -> Sem r () - goSimpleLambda (SimpleLambda (SimpleBinder _ lamVarTy) lamBody) = do - go lamVarTy - go lamBody - - goLambda :: Lambda -> Sem r () - goLambda l = mapM_ goClause (l ^. lambdaClauses) - where - goClause :: LambdaClause -> Sem r () - goClause (LambdaClause _ b) = go b - - goIden :: Iden -> Sem r () - goIden = \case - IdenInductive ty' -> - when (inside && name == ty') (throwNegativePositonError expr) - IdenVar name' - | not inside -> return () - | name == name' -> throwNegativePositonError expr - | name' `elem` indInfo ^.. inductiveInfoParameters . each . inductiveParamName -> modify (HashSet.insert name') - | otherwise -> return () - _ -> return () - - goApp :: Application -> Sem r () - goApp tyApp = do - let (hdExpr, args) = unfoldApplication tyApp - case hdExpr of - ax@(ExpressionIden IdenAxiom {}) -> do - when (isJust $ find (varOrInductiveInExpression name) args) $ - throwTypeAsArgumentOfBoundVarError ax - var@(ExpressionIden IdenVar {}) -> do - when (isJust $ find (varOrInductiveInExpression name) args) $ - throwTypeAsArgumentOfBoundVarError var - ExpressionIden (IdenInductive ty') -> do - when (inside && name == ty') (throwNegativePositonError expr) - indInfo' <- lookupInductive ty' - {- We now need to know whether `name` negatively occurs at - `indTy'` or not. The way to know is by checking that the type ty' - preserves the positivity condition, i.e., its type parameters are - no negative. - -} - let paramsTy' = indInfo' ^. inductiveInfoParameters - goInductiveApp indInfo' (zipExact paramsTy' (toList args)) - _ -> return () - - goInductiveApp :: InductiveInfo -> [(InductiveParameter, Expression)] -> Sem r () - goInductiveApp indInfo' = mapM_ (uncurry goInductiveAppArg) - where - goInductiveAppArg :: InductiveParameter -> Expression -> Sem r () - goInductiveAppArg param tyArg = do - let parName = param ^. inductiveParamName - negParms :: NegativeTypeParameters <- get - when (varOrInductiveInExpression name tyArg) $ do - when - (HashSet.member parName negParms) - (throwNegativePositonError tyArg) - when (recLimit > 0) $ - forM_ (indInfo' ^. inductiveInfoConstructors) $ \ctorName' -> do - ctorType' <- lookupConstructorType ctorName' - let errorRef = fromMaybe tyArg ref - args = constructorArgs ctorType' - forM_ args $ - \tyConstr' -> - checkStrictlyPositiveOccurrences - CheckPositivityArgs - { _checkPositivityArgsInductive = indInfo', - _checkPositivityArgsConstructorName = ctorName', - _checkPositivityArgsInductiveName = parName, - _checkPositivityArgsRecursionLimit = recLimit - 1, - _checkPositivityArgsErrorReference = Just errorRef, - _checkPositivityArgsTypeOfConstructorArg = tyConstr' ^. paramType - } - - throwNegativePositonError :: Expression -> Sem r () - throwNegativePositonError expr = do - let errLoc = fromMaybe expr ref - throw - . ErrNonStrictlyPositive - . ErrTypeInNegativePosition - $ TypeInNegativePosition - { _typeInNegativePositionType = indName, - _typeInNegativePositionConstructor = ctorName, - _typeInNegativePositionArgument = errLoc - } - - throwTypeAsArgumentOfBoundVarError :: Expression -> Sem r () - throwTypeAsArgumentOfBoundVarError expr = do - let errLoc = fromMaybe expr ref - throw - . ErrNonStrictlyPositive - . ErrTypeAsArgumentOfBoundVar - $ TypeAsArgumentOfBoundVar - { _typeAsArgumentOfBoundVarType = indName, - _typeAsArgumentOfBoundVarConstructor = ctorName, - _typeAsArgumentOfBoundVarReference = 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/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs deleted file mode 100644 index 64d00e1f16..0000000000 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs +++ /dev/null @@ -1,18 +0,0 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error - ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error, - module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error.Types, - ) -where - -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error.Types -import Juvix.Prelude - -data NonStrictlyPositiveError - = ErrTypeInNegativePosition TypeInNegativePosition - | ErrTypeAsArgumentOfBoundVar TypeAsArgumentOfBoundVar - -instance ToGenericError NonStrictlyPositiveError where - genericError :: (Member (Reader GenericOptions) r) => NonStrictlyPositiveError -> Sem r GenericError - genericError = \case - ErrTypeInNegativePosition e -> genericError e - ErrTypeAsArgumentOfBoundVar e -> genericError e diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index 1fa0708b8b..f5d3dfeb6b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -19,7 +19,6 @@ import Juvix.Compiler.Internal.Extra qualified as Extra import Juvix.Compiler.Internal.Extra.CoercionInfo import Juvix.Compiler.Internal.Extra.InstanceInfo import Juvix.Compiler.Internal.Pretty -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.CheckerNew qualified as New import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (Termination) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity @@ -153,9 +152,8 @@ checkModule :: Sem r Module checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do _moduleBody' <- - evalState (mempty :: NegativeTypeParameters) - . checkModuleBody - $ _moduleBody + checkModuleBody $ + _moduleBody return Module { _moduleBody = _moduleBody', @@ -165,7 +163,7 @@ checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do } checkModuleBody :: - (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => ModuleBody -> Sem r ModuleBody checkModuleBody ModuleBody {..} = do @@ -181,14 +179,14 @@ checkImport :: Import -> Sem r Import checkImport = return checkMutualBlock :: - (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock checkMutualBlock s = runReader emptyLocalVars (checkTopMutualBlock s) checkInductiveDef :: forall r. - (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, State NegativeTypeParameters, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) => InductiveDef -> Sem r InductiveDef checkInductiveDef InductiveDef {..} = runInferenceDef $ do @@ -249,7 +247,7 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do ) checkTopMutualBlock :: - (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock checkTopMutualBlock (MutualBlock ds) = @@ -305,7 +303,7 @@ resolveCastHoles s = do getNatTy = mkBuiltinInductive BuiltinNat checkMutualStatement :: - (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualStatement -> Sem r MutualStatement checkMutualStatement = \case diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs index e26e833543..3ed51dda37 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -8,7 +8,6 @@ where import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Types (BuiltinNotDefined) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Pretty import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Types import Juvix.Prelude @@ -23,7 +22,6 @@ data TypeCheckerError | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType | ErrInvalidPatternMatching InvalidPatternMatching - | ErrNonStrictlyPositive NonStrictlyPositiveError | ErrNonStrictlyPositiveNew NonStrictlyPositiveNew | ErrUnsupportedTypeFunction UnsupportedTypeFunction | ErrInvalidInstanceType InvalidInstanceType @@ -54,7 +52,6 @@ instance ToGenericError TypeCheckerError where ErrTooManyArgumentsIndType e -> genericError e ErrTooFewArgumentsIndType e -> genericError e ErrInvalidPatternMatching e -> genericError e - ErrNonStrictlyPositive e -> genericError e ErrUnsupportedTypeFunction e -> genericError e ErrInvalidInstanceType e -> genericError e ErrInvalidCoercionType e -> genericError e @@ -85,7 +82,6 @@ instance Show TypeCheckerError where ErrTooFewArgumentsIndType {} -> "ErrTooFewArgumentsIndType" ErrInvalidPatternMatching {} -> "ErrInvalidPatternMatching" ErrUnsupportedTypeFunction {} -> "ErrUnsupportedTypeFunction" - ErrNonStrictlyPositive {} -> "ErrNonStrictlyPositive" ErrInvalidInstanceType {} -> "ErrInvalidInstanceType" ErrInvalidCoercionType {} -> "ErrInvalidCoercionType" ErrWrongCoercionArgument {} -> "ErrWrongCoercionArgument" diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index f277a2f9a3..1a192a374c 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -1,7 +1,6 @@ module Typecheck.Negative where import Base -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error type FailMsg = String diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs index 3fcfb9a8a0..81f48e4c94 100644 --- a/test/Typecheck/NegativeNew.hs +++ b/test/Typecheck/NegativeNew.hs @@ -2,7 +2,6 @@ module Typecheck.NegativeNew where import Base import Data.HashSet qualified as HashSet -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error import Typecheck.Negative qualified as Old @@ -149,14 +148,14 @@ arityTests = _ -> wrongError, negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $ \case - ErrNonStrictlyPositive ErrTypeAsArgumentOfBoundVar {} -> Nothing + ErrNonStrictlyPositiveNew {} -> Nothing _ -> wrongError, negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $ \case - ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing + ErrNonStrictlyPositiveNew {} -> Nothing _ -> wrongError, negTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $ \case - ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing + ErrNonStrictlyPositiveNew {} -> Nothing _ -> wrongError ]