respect --no-positivity

anoma · Sep 28, 2024 · a34aff1 · a34aff1
1 parent e895301
commit a34aff1
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 7 deletions.
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/CheckerNew.hs
@@ -55,9 +55,10 @@ checkPositivity ::
        ]
       r
   ) =>
+  Bool ->
   MutualBlock ->
   Sem r ()
-checkPositivity mut = do
+checkPositivity noPositivityFlag mut = do
   let ldefs :: [InductiveDef] =
         mut
           ^.. mutualStatements
@@ -86,9 +87,14 @@ checkPositivity mut = do
       addPolarities (defName ^. nameId) polarities
     poltab' <- (^. typeCheckingTablesPolarityTable) <$> getCombinedTables
     let names :: NonEmpty InductiveName = (^. inductiveName) <$> defs
-    checkStrictlyPositive poltab' names occ
+    unless noPositivityFlag (checkStrictlyPositive poltab' names occ)
 
-checkStrictlyPositive :: (Members '[Error TypeCheckerError] r) => PolarityTable -> NonEmpty InductiveName -> Occurrences -> Sem r ()
+checkStrictlyPositive ::
+  (Members '[Error TypeCheckerError] r) =>
+  PolarityTable ->
+  NonEmpty InductiveName ->
+  Occurrences ->
+  Sem r ()
 checkStrictlyPositive tbl mutual = runReader PolarityStrictlyPositive . go
   where
     getPolarities :: InductiveName -> [Polarity]

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@@ -151,9 +151,7 @@ checkModule ::
   Module ->
   Sem r Module
 checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do
-  _moduleBody' <-
-    checkModuleBody $
-      _moduleBody
+  _moduleBody' <- checkModuleBody _moduleBody
   return
     Module
       { _moduleBody = _moduleBody',
@@ -264,13 +262,16 @@ checkBlockPositivity ::
       '[ Reader InfoTable,
          Error TypeCheckerError,
          ResultBuilder,
+         Reader EntryPoint,
          Inference
        ]
       r
   ) =>
   MutualBlock ->
   Sem r ()
-checkBlockPositivity = New.checkPositivity
+checkBlockPositivity m = do
+  noPos <- asks (^. entryPointNoPositivity)
+  New.checkPositivity noPos m
 
 resolveCastHoles ::
   forall a r.