77{-# LANGUAGE MultiParamTypeClasses #-}
88{-# LANGUAGE OverloadedStrings #-}
99{-# LANGUAGE ImplicitParams #-}
10+ {-# LANGUAGE NamedFieldPuns #-}
1011
1112{-# OPTIONS_GHC -Wno-orphans #-}
1213{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
@@ -28,8 +29,9 @@ import qualified Language.Haskell.Liquid.GHC.Resugar as Rs
2829import qualified Language.Haskell.Liquid.GHC.SpanStack as Sp
2930import qualified Language.Haskell.Liquid.GHC.Misc as GM -- ( isInternal, collectArguments, tickSrcSpan, showPpr )
3031import Text.PrettyPrint.HughesPJ ( text )
31- import Control.Monad ( foldM , forM , forM_ , when , void )
32+ import Control.Monad ( foldM , forM , forM_ , when , void , unless )
3233import Control.Monad.State
34+ import Data.Bifunctor (first )
3335import Data.Maybe (fromMaybe , isJust , mapMaybe )
3436import Data.Either.Extra (eitherToMaybe )
3537import qualified Data.HashMap.Strict as M
@@ -97,12 +99,110 @@ consAct γ cfg info = do
9799 hws <- gets hsWfs
98100 fcs <- concat <$> mapM (splitC (typeclass (getConfig info))) hcs
99101 fws <- concat <$> mapM splitW hws
102+ checkStratCtors γ sSpc
100103 modify $ \ st -> st { fEnv = fEnv st `mappend` feEnv (fenv γ)
101104 , cgLits = litEnv γ
102105 , cgConsts = cgConsts st `mappend` constEnv γ
103106 , fixCs = fcs
104107 , fixWfs = fws }
105108
109+
110+ ---------------------------------
111+ -- | Checking stratified ctors --
112+ ---------------------------------
113+ type FExpr = F. ExprVF. Symbol
114+ type FRef = F. ReftVF. Symbol
115+ type Ctors = S. HashSetF. Symbol
116+
117+ checkStratCtors :: CGEnv -> GhcSpecSig -> CG ()
118+ checkStratCtors env sSpc = do
119+ let ctors = S. fromList $ M. keys $ F. seBinds $ constEnv env
120+ let ctorRefinements = filter (isStrat . fst ) $ gsTySigs sSpc
121+ forM_ ctorRefinements $ uncurry $ checkCtor ctors
122+ where
123+ -- (Alecs): For some reason it can't see that they are the same
124+ -- GHC name, probably is due to some worker wrapper shenannigans
125+ hack = occNameString . nameOccName
126+ isStrat nm = hack (varName nm) `elem` map hack (gsStratCtos sSpc)
127+
128+ uncurryPi :: SpecType -> ([SpecType ], SpecType )
129+ uncurryPi (RFun _ _ dom cod _) = first (dom : ) $ uncurryPi cod
130+ uncurryPi rest = ([] , rest)
131+
132+ getIndex :: FRef -> Maybe FExpr
133+ getIndex (F. ReftF. PAtomF. EqF. EAppF. EVarF. EVar
134+ | n == " Language.Haskell.Liquid.ProofCombinators.prop"
135+ , v == v'
136+ = Just to
137+ getIndex _ = Nothing
138+
139+ getTyConName :: SpecType -> Name
140+ getTyConName a = Ghc. tyConName $ rtc_tc $ rt_tycon a
141+
142+ checkCtor :: Ctors -> Var -> LocSpecType -> CG ()
143+ checkCtor ctors name typ = do
144+ let loc = GM. fSrcSpan $ F. loc typ
145+ let (args, ret) = uncurryPi $ val typ
146+ -- The constuctor that we want not to appear negatrive
147+ let tyName = getTyConName ret
148+ -- Its index information
149+ retIdx <- case getIndex $ ur_reft $ rt_reft ret of
150+ Just idx -> pure idx
151+ Nothing -> uError $ ErrStratNotPropRet loc (pprint tyName) (pprint name) (F. pprint ret)
152+ -- For every argument of the constructor we check that in negative
153+ -- position all the self-refernce are refined by a "smaller" `prop`
154+ -- annotation
155+ forM_ args $ checkNg ctors loc name tyName retIdx
156+
157+ checkNg :: Ctors -> SrcSpan -> Var -> Name -> FExpr -> SpecType -> CG ()
158+ checkNg ctors loc ctorName tyName retIdx = go
159+ where
160+ go :: SpecType -> CG ()
161+ go RVar {} = pure ()
162+ go RAllT { rt_ty } = go rt_ty
163+ go RAllP { rt_ty } = go rt_ty
164+ go RFun { rt_in, rt_out } = do
165+ go rt_in
166+ go rt_out
167+ go r@ RApp { rt_tycon = RTyCon { rtc_tc }, rt_args, rt_reft } = do
168+ if Ghc. tyConName rtc_tc == tyName then do
169+ case getIndex $ ur_reft rt_reft of
170+ (Just arg) -> do
171+ -- We compare index information
172+ -- The engativer occurrence is safe iff the index of the
173+ -- return type is strictly bigger than the one in negative
174+ -- position
175+ unless (isStructurallySmaller ctors arg retIdx) $ do
176+ uError $ ErrStratIdxNotSmall loc
177+ (pprint tyName) (pprint ctorName) (F. pprint retIdx) (F. pprint arg)
178+ -- We don't have index information for both so we bail
179+ _ -> uError $ ErrStratOccProp loc (pprint tyName) (pprint ctorName) (F. pprint r)
180+ else do
181+ forM_ rt_args go
182+ go _ = lift $ impossible (Just loc) " checkNg unexpected type"
183+
184+
185+ isStructurallySmaller :: Ctors -> FExpr -> FExpr -> Bool
186+ isStructurallySmaller ctors l r
187+ -- Congruence rule
188+ | (F. EVar<- F. splitEAppThroughECst l
189+ , (F. EVar<- F. splitEAppThroughECst r
190+ , nl == nr
191+ , length argsl == length argsr
192+ , nl `elem` ctors
193+ = any (uncurry $ isStructurallySmaller ctors) $ zip argsl argsr
194+ | otherwise = isSubterm ctors l r && l /= r
195+
196+ isSubterm :: Ctors -> FExpr -> FExpr -> Bool
197+ isSubterm ctors l r | l == r
198+ = True
199+ -- Congruence rule
200+ | (F. EVar<- F. splitEAppThroughECst r
201+ , nm `elem` ctors
202+ = any (isSubterm ctors l) args
203+ | otherwise
204+ = False
205+
106206--------------------------------------------------------------------------------
107207-- | Ensure that the instance type is a subtype of the class type --------------
108208--------------------------------------------------------------------------------
0 commit comments