diff --git a/src/Juvix/Compiler/Internal/Data/Name.hs b/src/Juvix/Compiler/Internal/Data/Name.hs index 1d2596358c..63fcc46af8 100644 --- a/src/Juvix/Compiler/Internal/Data/Name.hs +++ b/src/Juvix/Compiler/Internal/Data/Name.hs @@ -103,6 +103,8 @@ type ConstrName = Name type InductiveName = Name +type InductiveId = NameId + fromConcreteSymbol :: Interval -> S.Symbol -> Name fromConcreteSymbol loc s = fromConcreteSymbolPretty loc (S.symbolText s) s diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs index 757bfab83c..556ccea620 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -64,7 +64,6 @@ checkStrictlyPositiveOccurrences :: Sem r () checkStrictlyPositiveOccurrences p = do traceM (prettyText (p ^. checkPositivityArgsInductiveName) <> " # " <> prettyText (p ^. checkPositivityArgsConstructorName)) - traceM ("reclimit = " <> prettyText recLimit) typeOfConstrArg <- strongNormalize_ (p ^. checkPositivityArgsTypeOfConstructorArg) goExpression False typeOfConstrArg where diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs new file mode 100644 index 0000000000..984ea7628d --- /dev/null +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs @@ -0,0 +1,76 @@ +module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg where + +import Juvix.Compiler.Internal.Extra.Base +import Juvix.Compiler.Internal.Language +import Juvix.Prelude + +data ConstructorArg + = ConstructorArgFun Fun + | ConstructorArgApp App + +data Fun = Fun + { _funLeft :: ConstructorArg, + _funRight :: ConstructorArg + } + +data AppLhs + = AppVar VarName + | AppAxiom AxiomName + | AppInductive InductiveName + deriving stock (Eq, Generic) + +instance Hashable AppLhs + +data App = App + { _appLhs :: AppLhs, + _appArgs :: [ConstructorArg] + } + +-- | The +mkConstructorArg :: (Members '[Error ()] r) => NormalizedExpression -> Sem r ConstructorArg +mkConstructorArg = mkConstructorArg' . (^. normalizedExpression) + +mkConstructorArg' :: forall r. (Members '[Error ()] r) => Expression -> Sem r ConstructorArg +mkConstructorArg' = \case + ExpressionIden i -> goApplicationHelper (ExpressionIden i, []) + ExpressionApplication i -> goApplication i + ExpressionFunction i -> goFunction i + ExpressionLiteral {} -> throw () + ExpressionHole {} -> throw () + ExpressionInstanceHole {} -> throw () + ExpressionLet {} -> throw () + ExpressionUniverse {} -> throw () + ExpressionSimpleLambda {} -> throw () + ExpressionLambda {} -> throw () + ExpressionCase {} -> throw () + where + getIden :: Expression -> Sem r Iden + getIden = \case + ExpressionIden i -> return i + _ -> throw () + + goFunction :: Function -> Sem r ConstructorArg + goFunction fun = do + l <- mkConstructorArg' (fun ^. functionLeft . paramType) + r <- mkConstructorArg' (fun ^. functionRight) + return $ + ConstructorArgFun + Fun + { _funLeft = l, + _funRight = r + } + + goApplication :: Application -> Sem r ConstructorArg + goApplication = goApplicationHelper . second toList . unfoldApplication + + goApplicationHelper :: (Expression, [Expression]) -> Sem r ConstructorArg + goApplicationHelper (f, args) = do + i <- getIden f + cargs <- mapM mkConstructorArg' args + lhs :: AppLhs <- case i of + IdenFunction {} -> throw () + IdenConstructor {} -> throw () + IdenVar v -> return (AppVar v) + IdenAxiom v -> return (AppAxiom v) + IdenInductive v -> return (AppInductive v) + return (ConstructorArgApp (App lhs cargs)) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs new file mode 100644 index 0000000000..fbc3527f6f --- /dev/null +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs @@ -0,0 +1,136 @@ +module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences + ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences, + module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg, + ) +where + +import Juvix.Compiler.Internal.Language +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg +import Juvix.Prelude + +type IxParam = Int + +type IxArg = Int + +data FunctionSide + = FunctionLeft + | FunctionRight + +instance Semigroup FunctionSide where + a <> b = case (a, b) of + (FunctionLeft, _) -> FunctionLeft + (_, FunctionLeft) -> FunctionLeft + (FunctionRight, FunctionRight) -> FunctionRight + +instance Monoid FunctionSide where + mempty = FunctionRight + +data ParamId = ParamId + { _paramIdInductiveId :: InductiveId, + _paramIdIx :: IxParam + } + deriving stock (Eq, Generic) + +instance Hashable ParamId + +data Occurrence = Occurrence + { _occurrencePolarity :: Polarity, + _occurrenceId :: ParamId + } + +data Occurrences = Occurrences + { _occurrencesPolarity :: HashMap ParamId Polarity, + _occurrencesTree :: HashMap AppLhs [Occurrences] + } + +newtype Polarities = Polarities + { _polarities :: HashMap (InductiveId, IxParam) Polarity + } + +makeLenses ''Occurrences +makeLenses ''Occurrence +makeLenses ''ParamId + +emptyOccurrences :: Occurrences +emptyOccurrences = + Occurrences + { _occurrencesPolarity = mempty, + _occurrencesTree = mempty + } + +stateOn :: forall t r. (Members '[State t] r) => t -> Lens' t (Maybe t) -> Sem r () -> Sem r () +stateOn tempty l m = do + st <- get + put (fromMaybe tempty (st ^. l)) + m + field' <- get + modify (set l (Just field')) + +mkOccurrences :: HashMap VarName ParamId -> [ConstructorArg] -> Occurrences +mkOccurrences tbl = + run + . runReader FunctionRight + . execState emptyOccurrences + . mapM_ addArg + where + getInductiveParamId :: VarName -> ParamId + getInductiveParamId v = fromJust (tbl ^. at v) + + getOccurrence :: forall r'. (Members '[Reader FunctionSide] r') => VarName -> Sem r' Occurrence + getOccurrence v = do + let pid = getInductiveParamId v + p <- getPolarity + return + Occurrence + { _occurrencePolarity = p, + _occurrenceId = pid + } + where + getPolarity :: Sem r' Polarity + getPolarity = + ask <&> \case + FunctionLeft -> PolarityNegative + FunctionRight -> PolarityStrictlyPositive + + addArg :: forall r'. (Members '[Reader FunctionSide, State Occurrences] r') => ConstructorArg -> Sem r' () + addArg = \case + ConstructorArgFun fun -> goFun fun + ConstructorArgApp a -> goApp a + where + registerOccurrence :: VarName -> Sem r' () + registerOccurrence v = do + occ <- getOccurrence v + let pid = occ ^. occurrenceId + pol = occ ^. occurrencePolarity + modify (over (occurrencesPolarity . at pid) (Just . maybe pol (<> pol))) + + goApp :: App -> Sem r' () + goApp (App lhs args) = case lhs of + AppVar v -> goVar v + AppAxiom {} -> goArgs + AppInductive {} -> goArgs + where + goVar :: VarName -> Sem r' () + goVar v = do + registerOccurrence v + goArgs + + goArgs :: Sem r' () + goArgs = do + let numArgs = length args + iniOccs = replicate numArgs emptyOccurrences + occs :: [Occurrences] <- fromMaybe iniOccs <$> gets (^. occurrencesTree . at lhs) + st :: Occurrences <- get + occs' :: [Occurrences] <- for (zipExact occs args) $ \(occ, arg) -> do + put occ + addArg arg + get + put (set (occurrencesTree . at lhs) (Just occs') st) + + goFun :: Fun -> Sem r' () + goFun (Fun funl funr) = do + onSide FunctionLeft (addArg funl) + onSide FunctionRight (addArg funr) + where + onSide :: FunctionSide -> Sem r' () -> Sem r' () + onSide side = local (side <>) 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 987471e72b..c24f4e48c7 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -209,7 +209,6 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do _inductivePragmas, _inductiveDocComment } - checkPositivity (inductiveInfoFromInductiveDef d) return d where checkParams :: Sem (Inference ': r) [(Name, Expression)] @@ -252,8 +251,31 @@ checkTopMutualBlock :: (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock -checkTopMutualBlock (MutualBlock ds) = - MutualBlock <$> runInferenceDefs (mapM checkMutualStatement ds) +checkTopMutualBlock (MutualBlock ds) = do + m <- MutualBlock <$> runInferenceDefs (mapM checkMutualStatement ds) + checkBlockPositivity m + return m + +checkBlockPositivity :: + -- ( Members + -- '[ + -- HighlightBuilder, + -- Reader BuiltinsTable, + -- State NegativeTypeParameters, + -- Reader EntryPoint, + -- Reader LocalVars, + -- Reader InfoTable, + -- Error TypeCheckerError, + -- NameIdGen, + -- ResultBuilder, + -- Termination, + -- Reader InsertedArgsStack + -- ] + -- r + -- ) => + MutualBlock -> + Sem r () +checkBlockPositivity _ = return () resolveCastHoles :: forall a r. diff --git a/src/Juvix/Compiler/Store/Internal/Data/PolarityTable.hs b/src/Juvix/Compiler/Store/Internal/Data/PolarityTable.hs new file mode 100644 index 0000000000..450809a4a5 --- /dev/null +++ b/src/Juvix/Compiler/Store/Internal/Data/PolarityTable.hs @@ -0,0 +1,18 @@ +module Juvix.Compiler.Store.Internal.Data.PolarityTable where + +import Juvix.Compiler.Internal.Language +import Juvix.Extra.Serialize +import Juvix.Prelude + +newtype PolarityTable = PolarityTable + { -- | The value should have the same length as the length of _inductiveParameters + _polarityTable :: HashMap InductiveId [Polarity] + } + deriving newtype (Semigroup, Monoid) + deriving stock (Generic) + +instance Serialize PolarityTable + +instance NFData PolarityTable + +makeLenses ''PolarityTable diff --git a/src/Juvix/Data.hs b/src/Juvix/Data.hs index 80d71a58cc..dad143f1c7 100644 --- a/src/Juvix/Data.hs +++ b/src/Juvix/Data.hs @@ -23,6 +23,7 @@ module Juvix.Data module Juvix.Data.DependencyInfo, module Juvix.Data.TopModulePathKey, module Juvix.Data.Keyword, + module Juvix.Data.Polarity, ) where @@ -41,6 +42,7 @@ import Juvix.Data.Loc import Juvix.Data.Logger import Juvix.Data.NameId qualified import Juvix.Data.NumThreads +import Juvix.Data.Polarity import Juvix.Data.Pragmas import Juvix.Data.Processed import Juvix.Data.ProjectionKind diff --git a/src/Juvix/Data/Polarity.hs b/src/Juvix/Data/Polarity.hs new file mode 100644 index 0000000000..1c6d6e6e5e --- /dev/null +++ b/src/Juvix/Data/Polarity.hs @@ -0,0 +1,35 @@ +module Juvix.Data.Polarity where + +import Juvix.Extra.Serialize +import Juvix.Prelude.Base +import Juvix.Prelude.Pretty + +data Polarity + = -- TODO rename PolarityNegative to PolarityNotStrictlyPositive + PolarityNegative + | PolarityStrictlyPositive + | PolarityUnused + deriving stock (Eq, Generic, Data, Show) + +instance Hashable Polarity + +instance Serialize Polarity + +instance NFData Polarity + +instance Semigroup Polarity where + a <> b = case (a, b) of + (PolarityUnused, p) -> p + (p, PolarityUnused) -> p + (PolarityNegative, _) -> PolarityNegative + (_, PolarityNegative) -> PolarityNegative + (PolarityStrictlyPositive, PolarityStrictlyPositive) -> PolarityStrictlyPositive + +instance Monoid Polarity where + mempty = PolarityUnused + +instance Pretty Polarity where + pretty = \case + PolarityNegative -> "negative" + PolarityStrictlyPositive -> "strictly-positive" + PolarityUnused -> "unused" diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index 9c957268ba..54528419ae 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -268,48 +268,22 @@ tests = negPositivityTests :: [NegTest] negPositivityTests = - [ negTest "E1" $(mkRelDir "Internal/Positivity") $(mkRelFile "E1.juvix") $ - \case - ErrNonStrictlyPositive ErrTypeInNegativePosition {} -> Nothing - _ -> wrongError, - negTest "E2" $(mkRelDir "Internal/Positivity") $(mkRelFile "E2.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E3" $(mkRelDir "Internal/Positivity") $(mkRelFile "E3.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E4" $(mkRelDir "Internal/Positivity") $(mkRelFile "E4.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E5" $(mkRelDir "Internal/Positivity") $(mkRelFile "E5.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E6" $(mkRelDir "Internal/Positivity") $(mkRelFile "E6.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E7" $(mkRelDir "Internal/Positivity") $(mkRelFile "E7.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E8" $(mkRelDir "Internal/Positivity") $(mkRelFile "E8.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E9" $(mkRelDir "Internal/Positivity") $(mkRelFile "E9.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E10 uses type synonym" $(mkRelDir "Internal/Positivity") $(mkRelFile "E10.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E11 uses type synonym" $(mkRelDir "Internal/Positivity") $(mkRelFile "E11.juvix") $ + [ mk "E1" $(mkRelFile "E1.juvix"), + mk "E2" $(mkRelFile "E2.juvix"), + mk "E3" $(mkRelFile "E3.juvix"), + mk "E4" $(mkRelFile "E4.juvix"), + mk "E5" $(mkRelFile "E5.juvix"), + mk "E6" $(mkRelFile "E6.juvix"), + mk "E7" $(mkRelFile "E7.juvix"), + mk "E8" $(mkRelFile "E8.juvix"), + mk "E9" $(mkRelFile "E9.juvix"), + mk "E10 uses type synonym" $(mkRelFile "E10.juvix"), + mk "E11 uses type synonym" $(mkRelFile "E11.juvix"), + mk "Phantom parameter" $(mkRelFile "phantom.juvix") + ] + where + mk :: String -> Path Rel File -> NegTest + mk testname testfile = negTest testname $(mkRelDir "Internal/Positivity") testfile $ \case ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing _ -> wrongError - ]