Parse stratified keyword and don't check for positivity stratified types

Author: AlecsFerra

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare.hs

@@ -93,7 +93,7 @@ makeTargetSpec :: Config
                -> TargetDependencies
                -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
 makeTargetSpec cfg localVars lnameEnv lmap targetSrc bareSpec dependencies = do
-  let targDiagnostics     = Bare.checkTargetSrc cfg targetSrc
+  let targDiagnostics     = Bare.checkTargetSrc cfg bareSpec targetSrc
   let depsDiagnostics     = mapM (Bare.checkBareSpec . snd) legacyDependencies
   let bareSpecDiagnostics = Bare.checkBareSpec bareSpec
   case targDiagnostics >> depsDiagnostics >> bareSpecDiagnostics of

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Check.hs

@@ -55,19 +55,25 @@ import qualified Language.Haskell.Liquid.Bare.Resolve      as Bare
 import           Language.Haskell.Liquid.UX.Config
 import Language.Fixpoint.Types.Config (ElabFlags (ElabFlags), solverFlags)
 
+-- import Debug.Trace
 
 ----------------------------------------------------------------------------------------------
 -- | Checking TargetSrc ------------------------------------------------------------------------
 ----------------------------------------------------------------------------------------------
-checkTargetSrc :: Config -> TargetSrc -> Either Diagnostics ()
-checkTargetSrc cfg spec
+checkTargetSrc :: Config -> BareSpec -> TargetSrc -> Either Diagnostics ()
+checkTargetSrc cfg bare spec
   |  nopositivity cfg
   || nopositives == emptyDiagnostics
   = Right ()
   | otherwise
   = Left nopositives
-  where nopositives = checkPositives (gsTcs spec)
+  where nopositives = checkPositives $ filter (not . isStratifiedTyCon bare) $ gsTcs spec
 
+isStratifiedTyCon :: BareSpec -> TyCon -> Bool
+isStratifiedTyCon bs tc = (Ghc.tyConName tc) `elem` sn
+  where sn = mapMaybe ctorName $ S.toList $ stratified bs
+        ctorName (F.Loc _ _ (LHNResolved (LHRGHC c) _)) = Just c
+        ctorName _                                      = Nothing
 
 checkPositives :: [TyCon] -> Diagnostics
 checkPositives tys = mkDiagnostics [] $ mkNonPosError (getNonPositivesTyCon tys)

liquidhaskell-boot/src/Language/Haskell/Liquid/Parse.hs

@@ -899,6 +899,7 @@ data BPspec
   | Insts   (Located LHName)                              -- ^ 'auto-inst' or 'ple' annotation; use ple locally on binder
   | HMeas   (Located LHName)                              -- ^ 'measure' annotation; lift Haskell binder as measure
   | Reflect (Located LHName)                              -- ^ 'reflect' annotation; reflect Haskell binder as function in logic
+  | Stratified (Located LHName)                           -- ^ 'stratified' annotation; stratification check for type declarations
   | PrivateReflect LocSymbol                              -- ^ 'private-reflect' annotation
   | OpaqueReflect (Located LHName)                        -- ^ 'opaque-reflect' annotation
   | Inline  (Located LHName)                              -- ^ 'inline' annotation;  inline (non-recursive) binder as an alias
@@ -984,6 +985,8 @@ ppPspec k (HMeas   lx)
   = "measure" <+> pprintTidy k (val lx)
 ppPspec k (Reflect lx)
   = "reflect" <+> pprintTidy k (val lx)
+ppPspec k (Stratified lx)
+  = "stratified" <+> pprintTidy k (val lx)
 ppPspec k (PrivateReflect lx)
   = "private-reflect" <+> pprintTidy k (val lx)
 ppPspec k (OpaqueReflect lx)
@@ -1106,6 +1109,7 @@ mkSpec xs = Measure.Spec
   , Measure.rewriteWith = M.fromList [s | Rewritewith s <- xs]
   , Measure.bounds     = M.fromList [(bname i, i) | PBound i <- xs]
   , Measure.reflects   = S.fromList [s | Reflect s <- xs]
+  , Measure.stratified = S.fromList [s | Stratified s <- xs]
   , Measure.privateReflects = S.fromList [s | PrivateReflect s <- xs]
   , Measure.opaqueReflects = S.fromList [s | OpaqueReflect s <- xs]
   , Measure.hmeas      = S.fromList [s | HMeas  s <- xs]
@@ -1129,6 +1133,7 @@ specP
     -- TODO: These next two are synonyms, kill one
     <|> fallbackSpecP "axiomatize"  (fmap Reflect locBinderLHNameP)
     <|> fallbackSpecP "reflect"     (fmap Reflect locBinderLHNameP)
+    <|> fallbackSpecP "stratified"  (fmap Stratified tyConBindLHNameP)
     <|> (reserved "private-reflect" >> fmap PrivateReflect axiomP  )
     <|> (reserved "opaque-reflect" >> fmap OpaqueReflect locBinderLHNameP  )
 

liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs

@@ -398,6 +398,7 @@ data Spec lname ty = Spec
   , rewriteWith :: !(M.HashMap (F.Located LHName) [F.Located LHName]) -- ^ Definitions using rewrite rules
   , fails      :: !(S.HashSet (F.Located LHName))                     -- ^ These Functions should be unsafe
   , reflects   :: !(S.HashSet (F.Located LHName))                     -- ^ Binders to reflect
+  , stratified :: !(S.HashSet (F.Located LHName))                     -- ^ Type declaration to check for stratification
   , privateReflects :: !(S.HashSet F.LocSymbol)                       -- ^ Private binders to reflect
   , opaqueReflects :: !(S.HashSet (F.Located LHName))                 -- ^ Binders to opaque-reflect
   , autois     :: !(S.HashSet (F.Located LHName))                     -- ^ Automatically instantiate axioms in these Functions
@@ -624,6 +625,7 @@ instance Semigroup (Spec lname ty) where
            , rewriteWith = M.union  (rewriteWith s1)  (rewriteWith s2)
            , fails      = S.union   (fails    s1)  (fails    s2)
            , reflects   = S.union   (reflects s1)  (reflects s2)
+           , stratified = S.union (stratified s1) (stratified s2)
            , privateReflects = S.union (privateReflects s1) (privateReflects s2)
            , opaqueReflects   = S.union   (opaqueReflects s1)  (opaqueReflects s2)
            , hmeas      = S.union   (hmeas    s1)  (hmeas    s2)
@@ -660,6 +662,7 @@ instance Monoid (Spec lname ty) where
            , autois     = S.empty
            , hmeas      = S.empty
            , reflects   = S.empty
+           , stratified = S.empty
            , privateReflects = S.empty
            , opaqueReflects = S.empty
            , inlines    = S.empty
@@ -1012,6 +1015,7 @@ unsafeFromLiftedSpec a = Spec
   , rewrites   = mempty
   , rewriteWith = mempty
   , reflects   = mempty
+  , stratified = mempty
   , privateReflects = liftedPrivateReflects a
   , opaqueReflects   = mempty
   , autois     = liftedAutois a