computing polarities

src/Juvix/Compiler/Internal/Data/Name.hs

@@ -105,6 +105,8 @@ type InductiveName = Name
 
 type InductiveId = NameId
 
+type InductiveParam = Name
+
 fromConcreteSymbol :: Interval -> S.Symbol -> Name
 fromConcreteSymbol loc s = fromConcreteSymbolPretty loc (S.symbolText s) s
 

src/Juvix/Compiler/Internal/Language.hs

@@ -484,6 +484,8 @@ data NormalizedExpression = NormalizedExpression
   }
 
 makePrisms ''Expression
+makePrisms ''MutualStatement
+
 makeLenses ''SideIfBranch
 makeLenses ''SideIfs
 makeLenses ''CaseBranchRhs

src/Juvix/Compiler/Internal/Pretty/Base.hs

@@ -11,6 +11,7 @@ import Juvix.Compiler.Internal.Data.NameDependencyInfo
 import Juvix.Compiler.Internal.Data.TypedHole
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Pretty.Options
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New
 import Juvix.Compiler.Store.Internal.Data.InfoTable
 import Juvix.Data.CodeAnn
@@ -407,6 +408,34 @@ instance PrettyCode TypedHole where
     vars <- ppCode _typedHoleLocalVars
     return (h <+> kwColon <+> ty <> kwAt <> vars)
 
+instance PrettyCode Polarity where
+  ppCode = return . annotate AnnKeyword . pretty
+
+instance (PrettyCode k, PrettyCode v) => PrettyCode (HashMap k v) where
+  ppCode m = do
+    res <- forM (HashMap.toList m) $ \(k, v) -> do
+      k' <- ppCode k
+      v' <- ppCode v
+      return (k' <+> "↦" <+> v')
+    return (bracesEnclose res)
+
+instance PrettyCode AppLhs where
+  ppCode = \case
+    AppVar v -> ppCode v
+    AppAxiom v -> ppCode v
+    AppInductive v -> ppCode v
+
+instance PrettyCode Occurrences where
+  ppCode Occurrences {..} = do
+    ps <- ppCode _occurrencesPolarity
+    args <- ppCode _occurrencesTree
+    return
+      ( bracesEnclose
+          [ header "occurrences" <+> kwAssign <+> ps,
+            header "recursive-args" <+> kwAssign <+> args
+          ]
+      )
+
 instance PrettyCode InfoTable where
   ppCode tbl = do
     inds <- ppCode (HashMap.keys (tbl ^. infoInductives))
@@ -463,6 +492,9 @@ instance (PrettyCode a) => PrettyCode (Maybe a) where
     Nothing -> return "Nothing"
     Just p -> ("Just" <+>) <$> ppCode p
 
+bracesEnclose :: (Foldable l) => l (Doc ann) -> Doc ann
+bracesEnclose = encloseSep "{" "}" "; " . toList
+
 tuple :: [Doc ann] -> Doc ann
 tuple = encloseSep "(" ")" ", "
 

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs

@@ -63,7 +63,7 @@ checkStrictlyPositiveOccurrences ::
   CheckPositivityArgs ->
   Sem r ()
 checkStrictlyPositiveOccurrences p = do
-  traceM (prettyText (p ^. checkPositivityArgsInductiveName) <> " # " <> prettyText (p ^. checkPositivityArgsConstructorName))
+  -- traceM (prettyText (p ^. checkPositivityArgsInductiveName) <> " # " <> prettyText (p ^. checkPositivityArgsConstructorName))
   typeOfConstrArg <- strongNormalize_ (p ^. checkPositivityArgsTypeOfConstructorArg)
   goExpression False typeOfConstrArg
   where

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/CheckerNew.hs

@@ -0,0 +1,186 @@
+module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.CheckerNew where
+
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Internal.Data.InfoTable
+import Juvix.Compiler.Internal.Extra
+import Juvix.Compiler.Internal.Pretty
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.ResultBuilder
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
+import Juvix.Prelude hiding (fromEither)
+
+data CheckPositivityArgs = CheckPositivityArgs
+  { _checkPositivityArgsInductive :: InductiveInfo,
+    _checkPositivityArgsConstructorName :: Name,
+    _checkPositivityArgsInductiveName :: Name,
+    _checkPositivityArgsRecursionLimit :: Int,
+    _checkPositivityArgsErrorReference :: Maybe Expression,
+    _checkPositivityArgsTypeOfConstructorArg :: Expression
+  }
+
+data Builder = Builder
+  { _builderPolarities :: HashMap InductiveParam Polarity,
+    _builderBlocking :: [Blocking]
+  }
+
+data Blocking = Blocking
+  { _blockingContext :: Polarity,
+    _blockingUnblocker :: InductiveParam,
+    -- | The unblocker has to have at least this polarity to unblock
+    _blockingUnblockerMinimum :: Polarity,
+    _blockingOccurrences :: Occurrences
+  }
+
+makeLenses ''CheckPositivityArgs
+makeLenses ''Builder
+
+emptyBuilder :: Builder
+emptyBuilder =
+  Builder
+    { _builderPolarities = mempty,
+      _builderBlocking = mempty
+    }
+
+checkPositivity ::
+  forall r.
+  ( Members
+      '[ Reader InfoTable,
+         Error TypeCheckerError,
+         ResultBuilder,
+         Inference
+       ]
+      r
+  ) =>
+  MutualBlock ->
+  Sem r ()
+checkPositivity mut = do
+  let ldefs :: [InductiveDef] =
+        mut
+          ^.. mutualStatements
+            . each
+            . _StatementInductive
+
+  whenJust (nonEmpty ldefs) $ \defs -> do
+    args :: [ConstructorArg] <-
+      concatMapM
+        (strongNormalize >=> mkConstructorArg)
+        ( defs
+            ^.. each
+              . inductiveConstructors
+              . each
+              . inductiveConstructorType
+        )
+    poltab <- (^. typeCheckingTablesPolarityTable) <$> getCombinedTables
+    let occ :: Occurrences = mkOccurrences args
+        inferredPolarities = computePolarities poltab defs occ
+    forM_ defs $ \def -> do
+      let params :: [InductiveParam] = def ^.. inductiveParameters . each . inductiveParamName
+          getPol p = fromMaybe PolarityUnused (inferredPolarities ^. at p)
+          polarities :: [Polarity] = map getPol params
+          defName = def ^. inductiveName
+      traceM ("add polarities " <> ppTrace defName <> ": " <> prettyText polarities)
+      addPolarities (defName ^. nameId) polarities
+
+computePolarities :: PolarityTable -> NonEmpty InductiveDef -> Occurrences -> HashMap InductiveParam Polarity
+computePolarities tab defs topOccurrences =
+  (^. builderPolarities)
+    . run
+    . runReader PolarityStrictlyPositive
+    . execState emptyBuilder
+    . go
+    $ topOccurrences
+  where
+    defsByName :: HashMap InductiveName InductiveDef
+    defsByName = indexedByHash (^. inductiveName) defs
+
+    getDef :: InductiveName -> InductiveDef
+    getDef d = fromJust (defsByName ^. at d)
+
+    -- Gets the current polarities of an inductive definition in the current mutual block
+    getInductivePolarities ::
+      (Members '[State Builder] r) =>
+      InductiveName ->
+      Sem r [(InductiveParam, Maybe Polarity)]
+    getInductivePolarities d = do
+      b <- get
+      let params = getDef d ^. inductiveParameters
+      return
+        [ (name, b ^. builderPolarities . at name)
+          | p :: InductiveParameter <- params,
+            let name = p ^. inductiveParamName
+        ]
+
+    go :: forall r. (Members '[State Builder, Reader Polarity] r) => Occurrences -> Sem r ()
+    go o = do
+      forM_ (HashMap.toList (o ^. occurrencesPolarity)) (uncurry addPolarity)
+      forM_ (HashMap.toList (o ^. occurrencesTree)) (uncurry goApp)
+      where
+        addPolarity :: InductiveParam -> Polarity -> Sem r ()
+        addPolarity var p = do
+          modif <- ask
+          b <- get
+          let old :: Maybe Polarity = b ^. builderPolarities . at var
+              new :: Polarity = maybe id (<>) old (p <> modif)
+          modify (set (builderPolarities . at var) (Just new))
+          when (old < Just new) (unblock var new)
+
+    unblock :: InductiveParam -> Polarity -> Sem r ()
+    unblock p newPol = undefined
+
+    goApp :: forall r. (Members '[State Builder, Reader Polarity] r) => AppLhs -> [Occurrences] -> Sem r ()
+    goApp lhs os = case lhs of
+      AppVar {} -> goVarArgs os
+      AppAxiom {} -> goAxiomArgs os
+      AppInductive a -> goInductive a os
+
+    localPolarity :: (Members '[Reader Polarity] r) => Polarity -> Sem r () -> Sem r ()
+    localPolarity = \case
+      PolarityUnused -> const (return ())
+      PolarityNegative -> local (const PolarityNegative)
+      PolarityStrictlyPositive -> local (const PolarityStrictlyPositive)
+
+    -- NOTE we assume that axioms have all variables in strictly positive positions
+    goAxiomArgs :: (Members '[State Builder, Reader Polarity] r) => [Occurrences] -> Sem r ()
+    goAxiomArgs os = mapM_ go os
+
+    goVarArgs :: (Members '[State Builder, Reader Polarity] r) => [Occurrences] -> Sem r ()
+    goVarArgs os = mapM_ go os
+
+    blockOn ::
+      (Members '[State Builder, Reader Polarity] r) =>
+      Polarity ->
+      InductiveParam ->
+      Occurrences ->
+      Sem r ()
+    blockOn minPol param o = do
+      ctx <- ask
+      let b =
+            Blocking
+              { _blockingContext = ctx,
+                _blockingUnblocker = param,
+                _blockingOccurrences = o,
+                _blockingUnblockerMinimum = minPol
+              }
+      modify (over builderBlocking (b :))
+
+    goInductive :: (Members '[State Builder, Reader Polarity] r) => InductiveName -> [Occurrences] -> Sem r ()
+    goInductive d os =
+      case tab ^. polarityTable . at (d ^. nameId) of
+        Just pols ->
+          forM_ (zipExact pols os) $ \(pol :: Polarity, o :: Occurrences) -> do
+            localPolarity pol (go o)
+        Nothing -> do
+          pols :: [(InductiveParam, Maybe Polarity)] <- getInductivePolarities d
+          traceM ("mutually recursive TODO" <> ppTrace d <> "\n" <> ppTrace topOccurrences <> "\n" <> ppTrace pols)
+          forM_ (zipExact pols os) $ \((p :: InductiveParam, mpol :: Maybe Polarity), o :: Occurrences) -> do
+            traceM ("mpol " <> ppTrace mpol)
+            case mpol of
+              Nothing -> blockOn PolarityStrictlyPositive p o
+              Just pol -> case pol of
+                PolarityNegative -> localPolarity pol (go o)
+                PolarityStrictlyPositive -> do
+                  blockOn (succ pol) p o
+                  localPolarity pol (go o)
+                PolarityUnused -> impossible

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs

@@ -1,58 +1,49 @@
-module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg where
+module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg
+  ( mkConstructorArg,
+    module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base,
+  )
+where
 
 import Juvix.Compiler.Internal.Extra.Base
 import Juvix.Compiler.Internal.Language
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base
+import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error
 import Juvix.Prelude
 
-data ConstructorArg
-  = ConstructorArgFun Fun
-  | ConstructorArgApp App
+mkConstructorArg :: (Members '[Error TypeCheckerError] r) => NormalizedExpression -> Sem r [ConstructorArg]
+mkConstructorArg = mapM (goArg . (^. paramType)) . fst . unfoldFunType . (^. normalizedExpression)
 
-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
+goArg :: forall r. (Members '[Error TypeCheckerError] r) => Expression -> Sem r ConstructorArg
+goArg ty = case ty of
   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 ()
+  ExpressionLiteral {} -> invalid
+  ExpressionHole {} -> invalid
+  ExpressionInstanceHole {} -> invalid
+  ExpressionLet {} -> invalid
+  ExpressionUniverse {} -> invalid
+  ExpressionSimpleLambda {} -> invalid
+  ExpressionLambda {} -> invalid
+  ExpressionCase {} -> invalid
   where
+    invalid :: forall a. Sem r a
+    invalid =
+      throw $
+        ErrInvalidConstructorArgType
+          InvalidConstructorArgType
+            { _invalidConstructorArgType = ty
+            }
+
     getIden :: Expression -> Sem r Iden
     getIden = \case
       ExpressionIden i -> return i
-      _ -> throw ()
+      _ -> invalid
 
     goFunction :: Function -> Sem r ConstructorArg
     goFunction fun = do
-      l <- mkConstructorArg' (fun ^. functionLeft . paramType)
-      r <- mkConstructorArg' (fun ^. functionRight)
+      l <- goArg (fun ^. functionLeft . paramType)
+      r <- goArg (fun ^. functionRight)
       return $
         ConstructorArgFun
           Fun
@@ -66,10 +57,10 @@ mkConstructorArg' = \case
     goApplicationHelper :: (Expression, [Expression]) -> Sem r ConstructorArg
     goApplicationHelper (f, args) = do
       i <- getIden f
-      cargs <- mapM mkConstructorArg' args
+      cargs <- mapM goArg args
       lhs :: AppLhs <- case i of
-        IdenFunction {} -> throw ()
-        IdenConstructor {} -> throw ()
+        IdenFunction {} -> invalid
+        IdenConstructor {} -> invalid
         IdenVar v -> return (AppVar v)
         IdenAxiom v -> return (AppAxiom v)
         IdenInductive v -> return (AppInductive v)

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg/Base.hs

@@ -0,0 +1,26 @@
+module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base where
+
+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, Show, Generic)
+
+instance Hashable AppLhs
+
+data App = App
+  { _appLhs :: AppLhs,
+    _appArgs :: [ConstructorArg]
+  }