wip

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
 

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

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))

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 <>)

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.

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

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

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"