{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE TupleSections       #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE DeriveTraversable   #-}
{-# LANGUAGE TypeOperators       #-}

{-# OPTIONS_GHC -Wno-incomplete-record-selectors #-}

module Language.Haskell.Liquid.Bare.Check
  ( checkTargetSpec
  , checkBareSpec
  , checkTargetSrc
  , checkStratTys
  , tyCompat
  ) where

import           Language.Haskell.Liquid.Constraint.ToFixpoint

import           Liquid.GHC.API                   as Ghc hiding ( Located
                                                                                 , text
                                                                                 , (<+>)
                                                                                 , panic
                                                                                 , ($+$)
                                                                                 , empty
                                                                                 )
import           Control.Applicative                       ((<|>))
import           Control.Monad.Reader
import           Data.Maybe
import           Data.Function                             (on)
import           Text.PrettyPrint.HughesPJ                 hiding ((<>))
import qualified Data.List                                 as L
import qualified Data.HashMap.Strict                       as M
import qualified Data.HashSet                              as S
import           Data.Hashable
import qualified Language.Fixpoint.Misc                    as Misc
import           Language.Fixpoint.SortCheck               (ElabM, checkSorted, checkSortedReftFull, checkSortFull)
import qualified Language.Fixpoint.Types                   as F
import qualified Language.Fixpoint.Types.Config            as FC
import qualified Language.Haskell.Liquid.GHC.Misc          as GM
import           Language.Haskell.Liquid.GHC.Play          (getNonPositivesTyCon)
import           Language.Haskell.Liquid.Misc              (condNull, thd5, foldMapM)
import           Language.Haskell.Liquid.Types.DataDecl
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.PredType
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.Visitors
import           Language.Haskell.Liquid.WiredIn

import qualified Language.Haskell.Liquid.Measure           as Ms
import qualified Language.Haskell.Liquid.Bare.Types        as Bare
import qualified Language.Haskell.Liquid.Bare.Resolve      as Bare
import           Language.Haskell.Liquid.UX.Config
-- import Language.Fixpoint.Types.Config (ElabFlags (ElabFlags))

----------------------------------------------------------------------------------------------
-- | Checking TargetSrc ------------------------------------------------------------------------
----------------------------------------------------------------------------------------------
checkTargetSrc :: Config -> BareSpec -> TargetSrc -> Either Diagnostics ()
checkTargetSrc :: Config -> BareSpec -> TargetSrc -> Either Diagnostics ()
checkTargetSrc Config
cfg BareSpec
bare TargetSrc
spec
  |  Config -> Bool
nopositivity Config
cfg
  Bool -> Bool -> Bool
|| Diagnostics
nopositives Diagnostics -> Diagnostics -> Bool
forall a. Eq a => a -> a -> Bool
== Diagnostics
emptyDiagnostics
  = () -> Either Diagnostics ()
forall a b. b -> Either a b
Right ()
  | Bool
otherwise
  = Diagnostics -> Either Diagnostics ()
forall a b. a -> Either a b
Left Diagnostics
nopositives
  where nopositives :: Diagnostics
nopositives = BareSpec -> [TyCon] -> Diagnostics
checkPositives BareSpec
bare ([TyCon] -> Diagnostics) -> [TyCon] -> Diagnostics
forall a b. (a -> b) -> a -> b
$ TargetSrc -> [TyCon]
gsTcs TargetSrc
spec

isStratifiedTyCon :: BareSpec -> TyCon -> Bool
isStratifiedTyCon :: BareSpec -> TyCon -> Bool
isStratifiedTyCon BareSpec
bs TyCon
tc = TyCon -> Name
Ghc.tyConName TyCon
tc Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
sn
  where sn :: [Name]
sn = (Located LHName -> Maybe Name) -> [Located LHName] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (LHName -> Maybe Name
getLHGHCName (LHName -> Maybe Name)
-> (Located LHName -> LHName) -> Located LHName -> Maybe Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
F.val) ([Located LHName] -> [Name]) -> [Located LHName] -> [Name]
forall a b. (a -> b) -> a -> b
$ HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
S.toList (HashSet (Located LHName) -> [Located LHName])
-> HashSet (Located LHName) -> [Located LHName]
forall a b. (a -> b) -> a -> b
$ BareSpec -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
stratified BareSpec
bs

checkPositives :: BareSpec -> [TyCon] -> Diagnostics
checkPositives :: BareSpec -> [TyCon] -> Diagnostics
checkPositives BareSpec
bare [TyCon]
tys = [Warning] -> [Error] -> Diagnostics
mkDiagnostics []
                        ([Error] -> Diagnostics) -> [Error] -> Diagnostics
forall a b. (a -> b) -> a -> b
$ [(TyCon, [DataCon])] -> [Error]
mkNonPosError
                        ([(TyCon, [DataCon])] -> [Error])
-> [(TyCon, [DataCon])] -> [Error]
forall a b. (a -> b) -> a -> b
$ ((TyCon, [DataCon]) -> Bool)
-> [(TyCon, [DataCon])] -> [(TyCon, [DataCon])]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((TyCon, [DataCon]) -> Bool) -> (TyCon, [DataCon]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpec -> TyCon -> Bool
isStratifiedTyCon BareSpec
bare (TyCon -> Bool)
-> ((TyCon, [DataCon]) -> TyCon) -> (TyCon, [DataCon]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon, [DataCon]) -> TyCon
forall a b. (a, b) -> a
fst)
                        ([(TyCon, [DataCon])] -> [(TyCon, [DataCon])])
-> [(TyCon, [DataCon])] -> [(TyCon, [DataCon])]
forall a b. (a -> b) -> a -> b
$ [TyCon] -> [(TyCon, [DataCon])]
getNonPositivesTyCon [TyCon]
tys

mkNonPosError :: [(TyCon, [DataCon])]  -> [Error]
mkNonPosError :: [(TyCon, [DataCon])] -> [Error]
mkNonPosError [(TyCon, [DataCon])]
tcs = [ SrcSpan -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrPosTyCon (TyCon -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan TyCon
tc) (TyCon -> Doc
forall a. PPrint a => a -> Doc
pprint TyCon
tc) (DataCon -> Doc
forall a. PPrint a => a -> Doc
pprint DataCon
dc Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PPrint a => a -> Doc
pprint (DataCon -> Type
dataConRepType DataCon
dc))
                    | (TyCon
tc, DataCon
dc:[DataCon]
_) <- [(TyCon, [DataCon])]
tcs]

--------------------------------------------------
-- | Checking that stratified ctors are present --
--------------------------------------------------

--- | Like 'Either' but the 'Semigroup' instance combines the failure
--- | values.
data Validation e a
  = Failure e
  | Success a
  deriving (Int -> Validation e a -> ShowS
[Validation e a] -> ShowS
Validation e a -> String
(Int -> Validation e a -> ShowS)
-> (Validation e a -> String)
-> ([Validation e a] -> ShowS)
-> Show (Validation e a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall e a. (Show e, Show a) => Int -> Validation e a -> ShowS
forall e a. (Show e, Show a) => [Validation e a] -> ShowS
forall e a. (Show e, Show a) => Validation e a -> String
$cshowsPrec :: forall e a. (Show e, Show a) => Int -> Validation e a -> ShowS
showsPrec :: Int -> Validation e a -> ShowS
$cshow :: forall e a. (Show e, Show a) => Validation e a -> String
show :: Validation e a -> String
$cshowList :: forall e a. (Show e, Show a) => [Validation e a] -> ShowS
showList :: [Validation e a] -> ShowS
Show, Validation e a -> Validation e a -> Bool
(Validation e a -> Validation e a -> Bool)
-> (Validation e a -> Validation e a -> Bool)
-> Eq (Validation e a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall e a.
(Eq e, Eq a) =>
Validation e a -> Validation e a -> Bool
$c== :: forall e a.
(Eq e, Eq a) =>
Validation e a -> Validation e a -> Bool
== :: Validation e a -> Validation e a -> Bool
$c/= :: forall e a.
(Eq e, Eq a) =>
Validation e a -> Validation e a -> Bool
/= :: Validation e a -> Validation e a -> Bool
Eq, (forall a b. (a -> b) -> Validation e a -> Validation e b)
-> (forall a b. a -> Validation e b -> Validation e a)
-> Functor (Validation e)
forall a b. a -> Validation e b -> Validation e a
forall a b. (a -> b) -> Validation e a -> Validation e b
forall e a b. a -> Validation e b -> Validation e a
forall e a b. (a -> b) -> Validation e a -> Validation e b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall e a b. (a -> b) -> Validation e a -> Validation e b
fmap :: forall a b. (a -> b) -> Validation e a -> Validation e b
$c<$ :: forall e a b. a -> Validation e b -> Validation e a
<$ :: forall a b. a -> Validation e b -> Validation e a
Functor, (forall m. Monoid m => Validation e m -> m)
-> (forall m a. Monoid m => (a -> m) -> Validation e a -> m)
-> (forall m a. Monoid m => (a -> m) -> Validation e a -> m)
-> (forall a b. (a -> b -> b) -> b -> Validation e a -> b)
-> (forall a b. (a -> b -> b) -> b -> Validation e a -> b)
-> (forall b a. (b -> a -> b) -> b -> Validation e a -> b)
-> (forall b a. (b -> a -> b) -> b -> Validation e a -> b)
-> (forall a. (a -> a -> a) -> Validation e a -> a)
-> (forall a. (a -> a -> a) -> Validation e a -> a)
-> (forall a. Validation e a -> [a])
-> (forall a. Validation e a -> Bool)
-> (forall a. Validation e a -> Int)
-> (forall a. Eq a => a -> Validation e a -> Bool)
-> (forall a. Ord a => Validation e a -> a)
-> (forall a. Ord a => Validation e a -> a)
-> (forall a. Num a => Validation e a -> a)
-> (forall a. Num a => Validation e a -> a)
-> Foldable (Validation e)
forall a. Eq a => a -> Validation e a -> Bool
forall a. Num a => Validation e a -> a
forall a. Ord a => Validation e a -> a
forall m. Monoid m => Validation e m -> m
forall a. Validation e a -> Bool
forall a. Validation e a -> Int
forall a. Validation e a -> [a]
forall a. (a -> a -> a) -> Validation e a -> a
forall e a. Eq a => a -> Validation e a -> Bool
forall e a. Num a => Validation e a -> a
forall e a. Ord a => Validation e a -> a
forall e m. Monoid m => Validation e m -> m
forall m a. Monoid m => (a -> m) -> Validation e a -> m
forall e a. Validation e a -> Bool
forall e a. Validation e a -> Int
forall e a. Validation e a -> [a]
forall b a. (b -> a -> b) -> b -> Validation e a -> b
forall a b. (a -> b -> b) -> b -> Validation e a -> b
forall e a. (a -> a -> a) -> Validation e a -> a
forall e m a. Monoid m => (a -> m) -> Validation e a -> m
forall e b a. (b -> a -> b) -> b -> Validation e a -> b
forall e a b. (a -> b -> b) -> b -> Validation e a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall e m. Monoid m => Validation e m -> m
fold :: forall m. Monoid m => Validation e m -> m
$cfoldMap :: forall e m a. Monoid m => (a -> m) -> Validation e a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Validation e a -> m
$cfoldMap' :: forall e m a. Monoid m => (a -> m) -> Validation e a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Validation e a -> m
$cfoldr :: forall e a b. (a -> b -> b) -> b -> Validation e a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Validation e a -> b
$cfoldr' :: forall e a b. (a -> b -> b) -> b -> Validation e a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Validation e a -> b
$cfoldl :: forall e b a. (b -> a -> b) -> b -> Validation e a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Validation e a -> b
$cfoldl' :: forall e b a. (b -> a -> b) -> b -> Validation e a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Validation e a -> b
$cfoldr1 :: forall e a. (a -> a -> a) -> Validation e a -> a
foldr1 :: forall a. (a -> a -> a) -> Validation e a -> a
$cfoldl1 :: forall e a. (a -> a -> a) -> Validation e a -> a
foldl1 :: forall a. (a -> a -> a) -> Validation e a -> a
$ctoList :: forall e a. Validation e a -> [a]
toList :: forall a. Validation e a -> [a]
$cnull :: forall e a. Validation e a -> Bool
null :: forall a. Validation e a -> Bool
$clength :: forall e a. Validation e a -> Int
length :: forall a. Validation e a -> Int
$celem :: forall e a. Eq a => a -> Validation e a -> Bool
elem :: forall a. Eq a => a -> Validation e a -> Bool
$cmaximum :: forall e a. Ord a => Validation e a -> a
maximum :: forall a. Ord a => Validation e a -> a
$cminimum :: forall e a. Ord a => Validation e a -> a
minimum :: forall a. Ord a => Validation e a -> a
$csum :: forall e a. Num a => Validation e a -> a
sum :: forall a. Num a => Validation e a -> a
$cproduct :: forall e a. Num a => Validation e a -> a
product :: forall a. Num a => Validation e a -> a
Foldable, Functor (Validation e)
Foldable (Validation e)
(Functor (Validation e), Foldable (Validation e)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Validation e a -> f (Validation e b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Validation e (f a) -> f (Validation e a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Validation e a -> m (Validation e b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Validation e (m a) -> m (Validation e a))
-> Traversable (Validation e)
forall e. Functor (Validation e)
forall e. Foldable (Validation e)
forall e (m :: * -> *) a.
Monad m =>
Validation e (m a) -> m (Validation e a)
forall e (f :: * -> *) a.
Applicative f =>
Validation e (f a) -> f (Validation e a)
forall e (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Validation e a -> m (Validation e b)
forall e (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Validation e a -> f (Validation e b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
Validation e (m a) -> m (Validation e a)
forall (f :: * -> *) a.
Applicative f =>
Validation e (f a) -> f (Validation e a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Validation e a -> m (Validation e b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Validation e a -> f (Validation e b)
$ctraverse :: forall e (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Validation e a -> f (Validation e b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Validation e a -> f (Validation e b)
$csequenceA :: forall e (f :: * -> *) a.
Applicative f =>
Validation e (f a) -> f (Validation e a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Validation e (f a) -> f (Validation e a)
$cmapM :: forall e (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Validation e a -> m (Validation e b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Validation e a -> m (Validation e b)
$csequence :: forall e (m :: * -> *) a.
Monad m =>
Validation e (m a) -> m (Validation e a)
sequence :: forall (m :: * -> *) a.
Monad m =>
Validation e (m a) -> m (Validation e a)
Traversable)

instance (Semigroup e, Semigroup a) => Semigroup (Validation e a) where
  Failure e
e1 <> :: Validation e a -> Validation e a -> Validation e a
<> Failure e
e2 = e -> Validation e a
forall e a. e -> Validation e a
Failure (e
e1 e -> e -> e
forall a. Semigroup a => a -> a -> a
<> e
e2)
  Failure e
e  <> Validation e a
_          = e -> Validation e a
forall e a. e -> Validation e a
Failure e
e
  Validation e a
_          <> Failure e
e  = e -> Validation e a
forall e a. e -> Validation e a
Failure e
e
  Success a
x  <> Success a
y  = a -> Validation e a
forall e a. a -> Validation e a
Success (a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y)

instance (Semigroup e, Monoid a) => Monoid (Validation e a) where
  mempty :: Validation e a
mempty = a -> Validation e a
forall e a. a -> Validation e a
Success a
forall a. Monoid a => a
mempty
  mappend :: Validation e a -> Validation e a -> Validation e a
mappend = Validation e a -> Validation e a -> Validation e a
forall a. Semigroup a => a -> a -> a
(<>)

valToEither :: Validation e a -> Either e a
valToEither :: forall e a. Validation e a -> Either e a
valToEither (Failure e
e) = e -> Either e a
forall a b. a -> Either a b
Left e
e
valToEither (Success a
x) = a -> Either e a
forall a b. b -> Either a b
Right a
x

-- | Check that all stratified types have their constructors
-- defined with refinement type signatures in the BareSpec.
--
-- Yields the names of the data constructors of the stratified types.
checkStratTys :: BareSpec -> TargetSrc -> Either Diagnostics [Name]
checkStratTys :: BareSpec -> TargetSrc -> Either Diagnostics [Name]
checkStratTys BareSpec
bare TargetSrc
spec =
  Validation Diagnostics [Name] -> Either Diagnostics [Name]
forall e a. Validation e a -> Either e a
valToEither
  (Validation Diagnostics [Name] -> Either Diagnostics [Name])
-> Validation Diagnostics [Name] -> Either Diagnostics [Name]
forall a b. (a -> b) -> a -> b
$ (Located TyCon -> Validation Diagnostics [Name])
-> [Located TyCon] -> Validation Diagnostics [Name]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (BareSpec -> Located TyCon -> Validation Diagnostics [Name]
checkStratTy BareSpec
bare)
  ([Located TyCon] -> Validation Diagnostics [Name])
-> [Located TyCon] -> Validation Diagnostics [Name]
forall a b. (a -> b) -> a -> b
$ (Located LHName -> Maybe (Located TyCon))
-> [Located LHName] -> [Located TyCon]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((LHName -> Maybe TyCon) -> Located LHName -> Maybe (Located TyCon)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse ([TyCon] -> LHName -> Maybe TyCon
findTyCon (TargetSrc -> [TyCon]
gsTcs TargetSrc
spec)))
  ([Located LHName] -> [Located TyCon])
-> [Located LHName] -> [Located TyCon]
forall a b. (a -> b) -> a -> b
$ HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
S.toList (HashSet (Located LHName) -> [Located LHName])
-> HashSet (Located LHName) -> [Located LHName]
forall a b. (a -> b) -> a -> b
$ BareSpec -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
stratified BareSpec
bare

-- | Find the TyCon corresponding to the given LHName in the given list of TyCons
findTyCon :: [TyCon] -> LHName -> Maybe TyCon
findTyCon :: [TyCon] -> LHName -> Maybe TyCon
findTyCon [TyCon]
tcs LHName
nm = do
  c <- LHName -> Maybe Name
getLHGHCName LHName
nm
  L.find ((== c) . Ghc.tyConName) tcs

-- | Check that the given TyCon is an ADT and that all its constructors
-- have refinements in the BareSpec.
checkStratTy :: BareSpec -> Located TyCon -> Validation Diagnostics [Name]
checkStratTy :: BareSpec -> Located TyCon -> Validation Diagnostics [Name]
checkStratTy BareSpec
spec Located TyCon
ltycon =
  case TyCon -> Maybe [DataCon]
tyConDataCons_maybe (Located TyCon -> TyCon
forall a. Located a -> a
val Located TyCon
ltycon) of
    Just [DataCon]
ctors -> (DataCon -> Validation Diagnostics [Name])
-> [DataCon] -> Validation Diagnostics [Name]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Located TyCon
-> BareSpec -> DataCon -> Validation Diagnostics [Name]
checkStratCtor Located TyCon
ltycon BareSpec
spec) [DataCon]
ctors
    Maybe [DataCon]
Nothing    -> Diagnostics -> Validation Diagnostics [Name]
forall e a. e -> Validation e a
Failure (Diagnostics -> Validation Diagnostics [Name])
-> Diagnostics -> Validation Diagnostics [Name]
forall a b. (a -> b) -> a -> b
$ [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [ Error
forall {t}. TError t
err ]
  where
    pos :: SrcSpan
pos = SourcePos -> SourcePos -> SrcSpan
GM.sourcePos2SrcSpan (Located TyCon -> SourcePos
forall a. Located a -> SourcePos
loc Located TyCon
ltycon) (Located TyCon -> SourcePos
forall a. Located a -> SourcePos
locE Located TyCon
ltycon)
    err :: TError t
err = SrcSpan -> Doc -> TError t
forall t. SrcSpan -> Doc -> TError t
ErrStratNotAdt SrcSpan
pos (Name -> Doc
forall a. PPrint a => a -> Doc
pprint (TyCon -> Name
Ghc.tyConName (TyCon -> Name) -> TyCon -> Name
forall a b. (a -> b) -> a -> b
$ Located TyCon -> TyCon
forall a. Located a -> a
val Located TyCon
ltycon))

-- | Check that the given DataCon has a refinement type signature in the BareSpec.
--
-- Yields the names of the data constructors that are stratified.
checkStratCtor :: Located TyCon -> BareSpec -> DataCon -> Validation Diagnostics [Name]
checkStratCtor :: Located TyCon
-> BareSpec -> DataCon -> Validation Diagnostics [Name]
checkStratCtor Located TyCon
ltycon BareSpec
spec DataCon
datacon
  | DataCon -> [LHName] -> Bool
hasRefinementTypeSignature DataCon
datacon (((Located LHName, Located BareType) -> LHName)
-> [(Located LHName, Located BareType)] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> ((Located LHName, Located BareType) -> Located LHName)
-> (Located LHName, Located BareType)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located LHName, Located BareType) -> Located LHName
forall a b. (a, b) -> a
fst) ([(Located LHName, Located BareType)] -> [LHName])
-> [(Located LHName, Located BareType)] -> [LHName]
forall a b. (a -> b) -> a -> b
$ BareSpec -> [(Located LHName, Located BareType)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
sigs BareSpec
spec)
  = [Name] -> Validation Diagnostics [Name]
forall e a. a -> Validation e a
Success [ DataCon -> Name
dataConName DataCon
datacon ]
  | Bool
otherwise = Diagnostics -> Validation Diagnostics [Name]
forall e a. e -> Validation e a
Failure (Diagnostics -> Validation Diagnostics [Name])
-> Diagnostics -> Validation Diagnostics [Name]
forall a b. (a -> b) -> a -> b
$ [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [ Error
forall {t}. TError t
err ]
  where
    pos :: SrcSpan
pos = SourcePos -> SourcePos -> SrcSpan
GM.sourcePos2SrcSpan (Located TyCon -> SourcePos
forall a. Located a -> SourcePos
loc Located TyCon
ltycon) (Located TyCon -> SourcePos
forall a. Located a -> SourcePos
locE Located TyCon
ltycon)
    err :: TError t
err = SrcSpan -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrStratNotRefCtor SrcSpan
pos (Name -> Doc
forall a. PPrint a => a -> Doc
pprint (Name -> Doc) -> Name -> Doc
forall a b. (a -> b) -> a -> b
$ DataCon -> Name
dataConName DataCon
datacon) (Name -> Doc
forall a. PPrint a => a -> Doc
pprint (Name -> Doc) -> Name -> Doc
forall a b. (a -> b) -> a -> b
$ TyCon -> Name
Ghc.tyConName (TyCon -> Name) -> TyCon -> Name
forall a b. (a -> b) -> a -> b
$ Located TyCon -> TyCon
forall a. Located a -> a
val Located TyCon
ltycon)
    hasRefinementTypeSignature :: DataCon -> [LHName] -> Bool
    hasRefinementTypeSignature :: DataCon -> [LHName] -> Bool
hasRefinementTypeSignature DataCon
dc [LHName]
lns =
      DataCon -> Name
dataConName DataCon
dc Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (LHName -> Maybe Name) -> [LHName] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe LHName -> Maybe Name
getLHGHCName [LHName]
lns


----------------------------------------------------------------------------------------------
-- | Checking BareSpec ------------------------------------------------------------------------
----------------------------------------------------------------------------------------------
checkBareSpec :: Ms.BareSpec -> Either Diagnostics ()
checkBareSpec :: BareSpec -> Either Diagnostics ()
checkBareSpec BareSpec
sp
  | Diagnostics
allChecks Diagnostics -> Diagnostics -> Bool
forall a. Eq a => a -> a -> Bool
== Diagnostics
emptyDiagnostics = () -> Either Diagnostics ()
forall a b. b -> Either a b
Right ()
  | Bool
otherwise = Diagnostics -> Either Diagnostics ()
forall a b. a -> Either a b
Left Diagnostics
allChecks
  where
    allChecks :: Diagnostics
allChecks = [Diagnostics] -> Diagnostics
forall a. Monoid a => [a] -> a
mconcat [ String -> [Located Symbol] -> Diagnostics
checkUnique   String
"measure"    [Located Symbol]
measures
                        , String -> [Located Symbol] -> Diagnostics
checkUnique   String
"field"      [Located Symbol]
fields
                        , [HashSet (Located Symbol)] -> Diagnostics
checkDisjoints             [ HashSet (Located Symbol)
inlines
                                                     , HashSet (Located Symbol)
hmeasures
                                                     , [Located Symbol] -> HashSet (Located Symbol)
forall a. Hashable a => [a] -> HashSet a
S.fromList [Located Symbol]
measures
                                                     , HashSet (Located Symbol)
reflects
                                                     , [Located Symbol] -> HashSet (Located Symbol)
forall a. Hashable a => [a] -> HashSet a
S.fromList [Located Symbol]
fields
                                                     ]
                        ]
    inlines :: HashSet (Located Symbol)
inlines   = (Located LHName -> Located Symbol)
-> HashSet (Located LHName) -> HashSet (Located Symbol)
forall b a. Hashable b => (a -> b) -> HashSet a -> HashSet b
S.map ((LHName -> Symbol) -> Located LHName -> Located Symbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
getLHNameSymbol) (BareSpec -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.inlines BareSpec
sp)
    hmeasures :: HashSet (Located Symbol)
hmeasures = (Located LHName -> Located Symbol)
-> HashSet (Located LHName) -> HashSet (Located Symbol)
forall b a. Hashable b => (a -> b) -> HashSet a -> HashSet b
S.map ((LHName -> Symbol) -> Located LHName -> Located Symbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
getLHNameSymbol) (BareSpec -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.hmeas BareSpec
sp)
    reflects :: HashSet (Located Symbol)
reflects  = (Located LHName -> Located Symbol)
-> HashSet (Located LHName) -> HashSet (Located Symbol)
forall b a. Hashable b => (a -> b) -> HashSet a -> HashSet b
S.map ((LHName -> Symbol) -> Located LHName -> Located Symbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
getLHNameSymbol) (BareSpec -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.reflects BareSpec
sp)
    measures :: [Located Symbol]
measures  = (LHName -> Symbol) -> Located LHName -> Located Symbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
getLHNameSymbol (Located LHName -> Located Symbol)
-> (MeasureV Symbol (Located BareType) (Located LHName)
    -> Located LHName)
-> MeasureV Symbol (Located BareType) (Located LHName)
-> Located Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MeasureV Symbol (Located BareType) (Located LHName)
-> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName (MeasureV Symbol (Located BareType) (Located LHName)
 -> Located Symbol)
-> [MeasureV Symbol (Located BareType) (Located LHName)]
-> [Located Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [MeasureV Symbol (Located BareType) (Located LHName)]
forall lname ty.
Spec lname ty -> [MeasureV lname (Located ty) (Located LHName)]
Ms.measures BareSpec
sp
    fields :: [Located Symbol]
fields    = (Located LHName -> Located Symbol)
-> [Located LHName] -> [Located Symbol]
forall a b. (a -> b) -> [a] -> [b]
map ((LHName -> Symbol) -> Located LHName -> Located Symbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
getLHNameSymbol) ([Located LHName] -> [Located Symbol])
-> [Located LHName] -> [Located Symbol]
forall a b. (a -> b) -> a -> b
$ (DataDeclP Symbol BareType -> [Located LHName])
-> [DataDeclP Symbol BareType] -> [Located LHName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataDeclP Symbol BareType -> [Located LHName]
dataDeclFields (BareSpec -> [DataDeclP Symbol BareType]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
Ms.dataDecls BareSpec
sp)

dataDeclFields :: DataDecl -> [F.Located LHName]
dataDeclFields :: DataDeclP Symbol BareType -> [Located LHName]
dataDeclFields = (Located LHName -> Bool) -> [Located LHName] -> [Located LHName]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (Located LHName -> Bool) -> Located LHName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
GM.isTmpSymbol (Symbol -> Bool)
-> (Located LHName -> Symbol) -> Located LHName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LHName -> Symbol
getLHNameSymbol (LHName -> Symbol)
-> (Located LHName -> LHName) -> Located LHName -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
F.val)
               ([Located LHName] -> [Located LHName])
-> (DataDeclP Symbol BareType -> [Located LHName])
-> DataDeclP Symbol BareType
-> [Located LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located LHName -> LHName) -> [Located LHName] -> [Located LHName]
forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.hashNubWith Located LHName -> LHName
forall a. Located a -> a
val
               ([Located LHName] -> [Located LHName])
-> (DataDeclP Symbol BareType -> [Located LHName])
-> DataDeclP Symbol BareType
-> [Located LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCtorP BareType -> [Located LHName])
-> [DataCtorP BareType] -> [Located LHName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataCtorP BareType -> [Located LHName]
dataCtorFields
               ([DataCtorP BareType] -> [Located LHName])
-> (DataDeclP Symbol BareType -> [DataCtorP BareType])
-> DataDeclP Symbol BareType
-> [Located LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DataCtorP BareType]
-> Maybe [DataCtorP BareType] -> [DataCtorP BareType]
forall a. a -> Maybe a -> a
fromMaybe []
               (Maybe [DataCtorP BareType] -> [DataCtorP BareType])
-> (DataDeclP Symbol BareType -> Maybe [DataCtorP BareType])
-> DataDeclP Symbol BareType
-> [DataCtorP BareType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDeclP Symbol BareType -> Maybe [DataCtorP BareType]
forall v ty. DataDeclP v ty -> Maybe [DataCtorP ty]
tycDCons

dataCtorFields :: DataCtor -> [F.Located LHName]
dataCtorFields :: DataCtorP BareType -> [Located LHName]
dataCtorFields DataCtorP BareType
c
  | DataCtorP BareType -> Bool
isGadt DataCtorP BareType
c  = []
  | Bool
otherwise = DataCtorP BareType -> LHName -> Located LHName
forall l b. Loc l => l -> b -> Located b
F.atLoc DataCtorP BareType
c (LHName -> Located LHName) -> [LHName] -> [Located LHName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ LHName
f | (LHName
f,BareType
_) <- DataCtorP BareType -> [(LHName, BareType)]
forall ty. DataCtorP ty -> [(LHName, ty)]
dcFields DataCtorP BareType
c ]

isGadt :: DataCtor -> Bool
isGadt :: DataCtorP BareType -> Bool
isGadt = Maybe BareType -> Bool
forall a. Maybe a -> Bool
isJust (Maybe BareType -> Bool)
-> (DataCtorP BareType -> Maybe BareType)
-> DataCtorP BareType
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtorP BareType -> Maybe BareType
forall ty. DataCtorP ty -> Maybe ty
dcResult

checkUnique :: String -> [F.LocSymbol] -> Diagnostics
checkUnique :: String -> [Located Symbol] -> Diagnostics
checkUnique String
_ = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty ([Error] -> Diagnostics)
-> ([Located Symbol] -> [Error]) -> [Located Symbol] -> Diagnostics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located Symbol -> Symbol)
-> (Located Symbol -> SrcSpan) -> [Located Symbol] -> [Error]
forall a t.
(PPrint a, Eq a, Hashable a) =>
(t -> a) -> (t -> SrcSpan) -> [t] -> [Error]
checkUnique' Located Symbol -> Symbol
forall a. Located a -> a
F.val Located Symbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan

checkUnique' :: (PPrint a, Eq a, Hashable a)
             => (t -> a) -> (t -> Ghc.SrcSpan) -> [t] -> [Error]
checkUnique' :: forall a t.
(PPrint a, Eq a, Hashable a) =>
(t -> a) -> (t -> SrcSpan) -> [t] -> [Error]
checkUnique' t -> a
nameF t -> SrcSpan
locF [t]
ts = [SrcSpan -> Doc -> [SrcSpan] -> Error
forall t. SrcSpan -> Doc -> [SrcSpan] -> TError t
ErrDupSpecs SrcSpan
l (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
n) [SrcSpan]
ls | (a
n, ls :: [SrcSpan]
ls@(SrcSpan
l:[SrcSpan]
_)) <- [(a, [SrcSpan])]
dups]
  where
    dups :: [(a, [SrcSpan])]
dups                   = [ (a, [SrcSpan])
z      | z :: (a, [SrcSpan])
z@(a
_, SrcSpan
_:SrcSpan
_:[SrcSpan]
_) <- [(a, SrcSpan)] -> [(a, [SrcSpan])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(a, SrcSpan)]
nts       ]
    nts :: [(a, SrcSpan)]
nts                    = [ (a
n, SrcSpan
l) | t
t <- [t]
ts, let n :: a
n = t -> a
nameF t
t, let l :: SrcSpan
l = t -> SrcSpan
locF t
t ]

checkDisjoints :: [S.HashSet F.LocSymbol] -> Diagnostics
checkDisjoints :: [HashSet (Located Symbol)] -> Diagnostics
checkDisjoints []     = Diagnostics
emptyDiagnostics
checkDisjoints [HashSet (Located Symbol)
_]    = Diagnostics
emptyDiagnostics
checkDisjoints (HashSet (Located Symbol)
s:[HashSet (Located Symbol)]
ss) = HashSet (Located Symbol) -> HashSet (Located Symbol) -> Diagnostics
checkDisjoint HashSet (Located Symbol)
s ([HashSet (Located Symbol)] -> HashSet (Located Symbol)
forall a. Eq a => [HashSet a] -> HashSet a
S.unions [HashSet (Located Symbol)]
ss) Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> [HashSet (Located Symbol)] -> Diagnostics
checkDisjoints [HashSet (Located Symbol)]
ss

checkDisjoint :: S.HashSet F.LocSymbol -> S.HashSet F.LocSymbol -> Diagnostics
checkDisjoint :: HashSet (Located Symbol) -> HashSet (Located Symbol) -> Diagnostics
checkDisjoint HashSet (Located Symbol)
s1 HashSet (Located Symbol)
s2 = String -> [Located Symbol] -> Diagnostics
checkUnique String
"disjoint" (HashSet (Located Symbol) -> [Located Symbol]
forall a. HashSet a -> [a]
S.toList HashSet (Located Symbol)
s1 [Located Symbol] -> [Located Symbol] -> [Located Symbol]
forall a. [a] -> [a] -> [a]
++ HashSet (Located Symbol) -> [Located Symbol]
forall a. HashSet a -> [a]
S.toList HashSet (Located Symbol)
s2)

----------------------------------------------------------------------------------------------
-- | Checking TargetSpec
----------------------------------------------------------------------------------------------

checkTargetSpec :: [Ms.BareSpec]
                -> TargetSrc
                -> F.SEnv F.SortedReft
                -> [CoreBind]
                -> TargetSpec
                -> Either Diagnostics ()
checkTargetSpec :: [BareSpec]
-> TargetSrc
-> SEnv SortedReft
-> [CoreBind]
-> TargetSpec
-> Either Diagnostics ()
checkTargetSpec [BareSpec]
specs TargetSrc
src SEnv SortedReft
env [CoreBind]
cbs TargetSpec
tsp
  | Diagnostics
diagnostics Diagnostics -> Diagnostics -> Bool
forall a. Eq a => a -> a -> Bool
== Diagnostics
emptyDiagnostics = () -> Either Diagnostics ()
forall a b. b -> Either a b
Right ()
  | Bool
otherwise                       = Diagnostics -> Either Diagnostics ()
forall a b. a -> Either a b
Left Diagnostics
diagnostics
  where
    diagnostics      :: Diagnostics
    diagnostics :: Diagnostics
diagnostics      =  Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Symbol, Located SpecType) -> Reader ElabFlags Diagnostics)
-> [(Symbol, Located SpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Symbol, Located SpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, Located SpecType)
-> Reader ElabFlags Diagnostics
checkBind Bool
bsc Doc
"measure"      TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) (GhcSpecData -> [(Symbol, Located SpecType)]
gsMeas       (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Bool -> Diagnostics -> Diagnostics
forall m. Monoid m => Bool -> m -> m
condNull Bool
noPrune
                        (Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Var, Located SpecType) -> Reader ElabFlags Diagnostics)
-> [(Var, Located SpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, Located SpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, Located SpecType)
-> Reader ElabFlags Diagnostics
checkBind Bool
bsc Doc
"constructor"  TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) ([(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall {f :: * -> *} {f :: * -> *} {f :: * -> *} {b} {a}.
(Functor f, Functor f, Functor f, HasTemplates b) =>
[(a, f (f (f b)))] -> [(a, f (f (f b)))]
txCtors ([(Var, Located SpecType)] -> [(Var, Located SpecType)])
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a b. (a -> b) -> a -> b
$ GhcSpecData -> [(Var, Located SpecType)]
gsCtors      (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp))) ElabFlags
ef)
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Var, Located SpecType) -> Reader ElabFlags Diagnostics)
-> [(Var, Located SpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, Located SpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, Located SpecType)
-> Reader ElabFlags Diagnostics
checkBind Bool
bsc Doc
"assume"       TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) (GhcSpecSig -> [(Var, Located SpecType)]
gsAsmSigs    (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Var, Located SpecType) -> Reader ElabFlags Diagnostics)
-> [(Var, Located SpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, Located SpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, Located SpecType)
-> Reader ElabFlags Diagnostics
checkBind Bool
bsc Doc
"reflect"      TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env ((Var, Located SpecType) -> Reader ElabFlags Diagnostics)
-> ((Var, Located SpecType) -> (Var, Located SpecType))
-> (Var, Located SpecType)
-> Reader ElabFlags Diagnostics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\sig :: (Var, Located SpecType)
sig@(Var
_,Located SpecType
s) -> String -> (Var, Located SpecType) -> (Var, Located SpecType)
forall a. PPrint a => String -> a -> a
F.notracepp ([RFInfo] -> String
forall a. Show a => a -> String
show (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [RFInfo]
forall b v c tv r. RTypeRepBV b v c tv r -> [RFInfo]
ty_info (SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep (Located SpecType -> SpecType
forall a. Located a -> a
F.val Located SpecType
s)))) (Var, Located SpecType)
sig)) (GhcSpecSig -> [(Var, Located SpecType)]
gsRefSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (Bool
-> [CoreBind]
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> GhcSpecSig
-> Reader ElabFlags Diagnostics
checkTySigs Bool
bsc [CoreBind]
cbs            TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env                (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp)) ElabFlags
ef
                     -- ++ mapMaybe (checkTerminationExpr             emb       env) (gsTexprs     (gsSig  sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Var, Located SpecType) -> Reader ElabFlags Diagnostics)
-> [(Var, Located SpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, Located SpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, Located SpecType)
-> Reader ElabFlags Diagnostics
checkBind Bool
bsc Doc
"class method" TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) (GhcSpecSig -> [(Var, Located SpecType)]
clsSigs      (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Maybe Var, Located SpecType) -> Reader ElabFlags Diagnostics)
-> [(Maybe Var, Located SpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Maybe Var, Located SpecType)
-> Reader ElabFlags Diagnostics
checkInv Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env)                 (GhcSpecData -> [(Maybe Var, Located SpecType)]
gsInvariants (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> [(Located SpecType, Located SpecType)]
-> Reader ElabFlags Diagnostics
checkIAl Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env                            (GhcSpecData -> [(Located SpecType, Located SpecType)]
gsIaliases   (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (TCEmb TyCon
-> SEnv SortedReft
-> [MeasureV Symbol SpecType DataCon]
-> Reader ElabFlags Diagnostics
checkMeasures TCEmb TyCon
emb SEnv SortedReft
env [MeasureV Symbol SpecType DataCon]
ms) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> [MeasureV Symbol SpecType DataCon] -> Diagnostics
checkClassMeasures                                        [MeasureV Symbol SpecType DataCon]
ms
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Maybe [ClsInst]
-> [Var] -> [(Var, Located SpecType)] -> Diagnostics
checkClassMethods (TargetSrc -> Maybe [ClsInst]
gsCls TargetSrc
src) (GhcSpecVars -> [Var]
gsCMethods (TargetSpec -> GhcSpecVars
gsVars TargetSpec
tsp)) (GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs     (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     -- <> foldMap checkMismatch sigs
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> ((Var, Located SpecType) -> Diagnostics)
-> [(Var, Located SpecType)] -> Diagnostics
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Var, Located SpecType) -> Diagnostics
checkMismatch (((Var, Located SpecType) -> Bool)
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
L.filter (\(Var
v,Located SpecType
_) -> Bool -> Bool
not (Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isSCSel Var
v Bool -> Bool -> Bool
|| Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isMethod Var
v)) [(Var, Located SpecType)]
sigs)
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> [(Var, Located SpecType)] -> Diagnostics
checkDuplicate                                            (GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs     (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     -- TODO-REBARE ++ checkQualifiers env                                       (gsQualifiers (gsQual sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> [(Var, Located SpecType)] -> Diagnostics
checkDuplicate                                            (GhcSpecSig -> [(Var, Located SpecType)]
gsAsmSigs    (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> Diagnostics
checkDupIntersect                                         (GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp)) (GhcSpecSig -> [(Var, Located SpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> String
-> SEnv SortedReft -> [RTAlias Symbol BareType] -> Diagnostics
forall t s a. String -> t -> [RTAlias s a] -> Diagnostics
checkRTAliases String
"Type Alias" SEnv SortedReft
env [RTAlias Symbol BareType]
myTAliases
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> String -> SEnv SortedReft -> [RTAlias Symbol Expr] -> Diagnostics
forall t s a. String -> t -> [RTAlias s a] -> Diagnostics
checkRTAliases String
"Pred Alias" SEnv SortedReft
env [RTAlias Symbol Expr]
myPAliases
                     -- ++ _checkDuplicateFieldNames                   (gsDconsP sp)
                     -- NV TODO: allow instances of refined classes to be refined
                     -- but make sure that all the specs are checked.
                     -- ++ checkRefinedClasses                        rClasses rInsts
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (TCEmb TyCon
-> SEnv SortedReft -> [TyConP] -> Reader ElabFlags Diagnostics
checkSizeFun TCEmb TyCon
emb SEnv SortedReft
env                                      (GhcSpecNames -> [TyConP]
gsTconsP (TargetSpec -> GhcSpecNames
gsName TargetSpec
tsp))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> [(Symbol, Located SpecType)] -> Diagnostics
forall v. PPrint v => [(v, Located SpecType)] -> Diagnostics
checkPlugged ([Maybe (Symbol, Located SpecType)] -> [(Symbol, Located SpecType)]
forall a. [Maybe a] -> [a]
catMaybes [ (Located SpecType -> (Symbol, Located SpecType))
-> Maybe (Located SpecType) -> Maybe (Symbol, Located SpecType)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Symbol -> Symbol
F.dropSym Int
2 (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall t. NamedThing t => t -> Symbol
GM.simplesymbol Var
x,) (MethodType (Located SpecType) -> Maybe (Located SpecType)
forall t. MethodType t -> Maybe t
getMethodType MethodType (Located SpecType)
t) | (Var
x, MethodType (Located SpecType)
t) <- GhcSpecSig -> [(Var, MethodType (Located SpecType))]
gsMethods (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp) ])
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> TargetSpec -> Diagnostics
checkRewrites TargetSpec
tsp
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> if Config -> Bool
allowUnsafeConstructors (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ TargetSpec -> Config
forall t. HasConfig t => t -> Config
getConfig TargetSpec
tsp
                          then Diagnostics
forall a. Monoid a => a
mempty
                          else [(Var, Located SpecType)] -> Diagnostics
checkConstructorRefinement (GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs (GhcSpecSig -> [(Var, Located SpecType)])
-> GhcSpecSig -> [(Var, Located SpecType)]
forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp)

    _rClasses :: [RClass (Located BareType)]
_rClasses        = (BareSpec -> [RClass (Located BareType)])
-> [BareSpec] -> [RClass (Located BareType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap BareSpec -> [RClass (Located BareType)]
forall lname ty. Spec lname ty -> [RClass (Located ty)]
Ms.classes [BareSpec]
specs
    _rInsts :: [RInstance (Located BareType)]
_rInsts          = (BareSpec -> [RInstance (Located BareType)])
-> [BareSpec] -> [RInstance (Located BareType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap BareSpec -> [RInstance (Located BareType)]
forall lname ty. Spec lname ty -> [RInstance (Located ty)]
Ms.rinstance [BareSpec]
specs
    -- Duplicate alias (definition) is checked within the bare spec only.
    myTAliases :: [RTAlias Symbol BareType]
myTAliases       = BareSpec -> [RTAlias Symbol BareType]
forall lname ty.
Spec lname ty -> [RTAlias Symbol (BareTypeV lname)]
Ms.aliases ([BareSpec] -> BareSpec
forall a. HasCallStack => [a] -> a
head [BareSpec]
specs)
    myPAliases :: [RTAlias Symbol Expr]
myPAliases       = BareSpec -> [RTAlias Symbol Expr]
forall lname ty. Spec lname ty -> [RTAlias Symbol (ExprV lname)]
Ms.ealiases ([BareSpec] -> BareSpec
forall a. HasCallStack => [a] -> a
head [BareSpec]
specs)
    emb :: TCEmb TyCon
emb              = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (TargetSpec -> GhcSpecNames
gsName TargetSpec
tsp)
    tcEnv :: TyConMap
tcEnv            = GhcSpecNames -> TyConMap
gsTyconEnv (TargetSpec -> GhcSpecNames
gsName TargetSpec
tsp)
    ms :: [MeasureV Symbol SpecType DataCon]
ms               = GhcSpecData -> [MeasureV Symbol SpecType DataCon]
gsMeasures (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp)
    clsSigs :: GhcSpecSig -> [(Var, Located SpecType)]
clsSigs GhcSpecSig
sp       = [ (Var
v, Located SpecType
t) | (Var
v, Located SpecType
t) <- GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs GhcSpecSig
sp, Maybe Class -> Bool
forall a. Maybe a -> Bool
isJust (Var -> Maybe Class
isClassOpId_maybe Var
v) ]
    sigs :: [(Var, Located SpecType)]
sigs             = GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp) [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, Located SpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp) [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecData -> [(Var, Located SpecType)]
gsCtors (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp)
    -- allowTC          = typeclass (getConfig sp)
    bsc :: Bool
bsc              = Config -> Bool
bscope (TargetSpec -> Config
forall t. HasConfig t => t -> Config
getConfig TargetSpec
tsp)
    noPrune :: Bool
noPrune          = Bool -> Bool
not (TargetSpec -> Bool
forall t. HasConfig t => t -> Bool
pruneFlag TargetSpec
tsp)
    txCtors :: [(a, f (f (f b)))] -> [(a, f (f (f b)))]
txCtors [(a, f (f (f b)))]
ts       = [(a
v, (f (f b) -> f (f b)) -> f (f (f b)) -> f (f (f b))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f b -> f b) -> f (f b) -> f (f b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> b) -> f b -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Templates -> b -> b
forall a. HasTemplates a => Templates -> a -> a
F.filterUnMatched Templates
temps))) f (f (f b))
t) | (a
v, f (f (f b))
t) <- [(a, f (f (f b)))]
ts]
    temps :: Templates
temps            = [([Symbol], Expr)] -> Templates
F.makeTemplates ([([Symbol], Expr)] -> Templates)
-> [([Symbol], Expr)] -> Templates
forall a b. (a -> b) -> a -> b
$ GhcSpecData -> [([Symbol], Expr)]
gsUnsorted (GhcSpecData -> [([Symbol], Expr)])
-> GhcSpecData -> [([Symbol], Expr)]
forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecData
gsData TargetSpec
tsp
    ef :: ElabFlags
ef               = Maybe SMTSolver -> ElabFlags
mkElabFlags (Config -> Maybe SMTSolver
smtsolver (Config -> Maybe SMTSolver) -> Config -> Maybe SMTSolver
forall a b. (a -> b) -> a -> b
$ TargetSpec -> Config
forall t. HasConfig t => t -> Config
getConfig TargetSpec
tsp)

mkElabFlags :: Maybe FC.SMTSolver -> FC.ElabFlags
mkElabFlags :: Maybe SMTSolver -> ElabFlags
mkElabFlags Maybe SMTSolver
Nothing    = Bool -> Bool -> ElabFlags
FC.ElabFlags Bool
False Bool
False
mkElabFlags (Just SMTSolver
slv) = SMTSolver -> Bool -> ElabFlags
FC.mkElabFlags SMTSolver
slv Bool
False


-- | Tests that the returned refinement type of data constructors has predicate @True@ or @prop v == e@.
--
-- > data T = T Int
-- > {-@ T :: x:Int -> { v:T | v = T x } @-} -- Should be rejected
-- > {-@ T :: x:Int -> { v:T | True } @-} -- Should be fine
-- > {-@ T :: x:Int -> { v:T | prop v = True } @-} -- Should be fine
--
checkConstructorRefinement :: [(Var, LocSpecType)] -> Diagnostics
checkConstructorRefinement :: [(Var, Located SpecType)] -> Diagnostics
checkConstructorRefinement = [Diagnostics] -> Diagnostics
forall a. Monoid a => [a] -> a
mconcat ([Diagnostics] -> Diagnostics)
-> ([(Var, Located SpecType)] -> [Diagnostics])
-> [(Var, Located SpecType)]
-> Diagnostics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Var, Located SpecType) -> Diagnostics)
-> [(Var, Located SpecType)] -> [Diagnostics]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Located SpecType) -> Diagnostics
forall {b} {v} {c} {tv} {b} {v}.
(Var,
 Located (RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))))
-> Diagnostics
checkOne
  where
    checkOne :: (Var,
 Located (RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))))
-> Diagnostics
checkOne (Var
s, Located (RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol)))
ty) | Var -> Bool
isCtorName Var
s
                     , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ReftBV Symbol Symbol -> Bool
validRef (ReftBV Symbol Symbol -> Bool) -> ReftBV Symbol Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
-> ReftBV Symbol Symbol
forall {b} {v} {c} {tv} {b} {v} {t}.
RTypeBV b v c tv (UReftBV b v t) -> t
getRetTyRef (RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
 -> ReftBV Symbol Symbol)
-> RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
-> ReftBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ Located (RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol)))
-> RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))
forall a. Located a -> a
val Located (RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol)))
ty
                     = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [ SrcSpan -> Doc -> Error
forall t. SrcSpan -> Doc -> TError t
ErrCtorRefinement (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located (RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol)))
-> SourcePos
forall a. Located a -> SourcePos
loc Located (RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol)))
ty) (Var -> Doc
forall a. PPrint a => a -> Doc
pprint Var
s) ]
    checkOne (Var,
 Located (RTypeBV b v c tv (UReftBV b v (ReftBV Symbol Symbol))))
_       = Diagnostics
forall a. Monoid a => a
mempty

    getRetTyRef :: RTypeBV b v c tv (UReftBV b v t) -> t
getRetTyRef (RFun b
_ RFInfo
_ RTypeBV b v c tv (UReftBV b v t)
_ RTypeBV b v c tv (UReftBV b v t)
t UReftBV b v t
_) = RTypeBV b v c tv (UReftBV b v t) -> t
getRetTyRef RTypeBV b v c tv (UReftBV b v t)
t
    getRetTyRef (RAllT RTVUBV b v c tv
_ RTypeBV b v c tv (UReftBV b v t)
t UReftBV b v t
_)    = RTypeBV b v c tv (UReftBV b v t) -> t
getRetTyRef RTypeBV b v c tv (UReftBV b v t)
t
    getRetTyRef RTypeBV b v c tv (UReftBV b v t)
t                = UReftBV b v t -> t
forall b v r. UReftBV b v r -> r
ur_reft (UReftBV b v t -> t) -> UReftBV b v t -> t
forall a b. (a -> b) -> a -> b
$ RTypeBV b v c tv (UReftBV b v t) -> UReftBV b v t
forall b v c tv r. RTypeBV b v c tv r -> r
rt_reft RTypeBV b v c tv (UReftBV b v t)
t

    -- True refinement
    validRef :: ReftBV Symbol Symbol -> Bool
validRef (F.Reft (Symbol
_, Expr
F.PTrue))
                      = Bool
True
    -- Prop foo from ProofCombinators
    validRef ReftBV Symbol Symbol
n = Maybe Expr -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Expr -> Bool) -> Maybe Expr -> Bool
forall a b. (a -> b) -> a -> b
$ ReftBV Symbol Symbol -> Maybe Expr
getPropIndex ReftBV Symbol Symbol
n

    isCtorName :: Var -> Bool
isCtorName Var
x = case HasCallStack => Var -> IdDetails
Var -> IdDetails
idDetails Var
x of
      DataConWorkId DataCon
_ -> Bool
True
      DataConWrapId DataCon
_ -> Bool
True
      IdDetails
_               -> Bool
False


checkPlugged :: PPrint v => [(v, LocSpecType)] -> Diagnostics
checkPlugged :: forall v. PPrint v => [(v, Located SpecType)] -> Diagnostics
checkPlugged [(v, Located SpecType)]
xs = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty (((v, Located SpecType) -> Error)
-> [(v, Located SpecType)] -> [Error]
forall a b. (a -> b) -> [a] -> [b]
map (v, Located SpecType) -> Error
forall {a} {a} {t}. PPrint a => (a, Located a) -> TError t
mkError (((v, Located SpecType) -> Bool)
-> [(v, Located SpecType)] -> [(v, Located SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (SpecType -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
hasHoleTy (SpecType -> Bool)
-> ((v, Located SpecType) -> SpecType)
-> (v, Located SpecType)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located SpecType -> SpecType
forall a. Located a -> a
val (Located SpecType -> SpecType)
-> ((v, Located SpecType) -> Located SpecType)
-> (v, Located SpecType)
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v, Located SpecType) -> Located SpecType
forall a b. (a, b) -> b
snd) [(v, Located SpecType)]
xs))
  where
    mkError :: (a, Located a) -> TError t
mkError (a
x,Located a
t) = SrcSpan -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located a -> SourcePos
forall a. Located a -> SourcePos
loc Located a
t) (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
x) Doc
msg
    msg :: Doc
msg           = Doc
"Cannot resolve type hole `_`. Use explicit type instead."


--------------------------------------------------------------------------------
checkTySigs :: BScope
            -> [CoreBind]
            -> F.TCEmb TyCon
            -> Bare.TyConMap
            -> F.SEnv F.SortedReft
            -> GhcSpecSig
            -> ElabM Diagnostics
--------------------------------------------------------------------------------
checkTySigs :: Bool
-> [CoreBind]
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> GhcSpecSig
-> Reader ElabFlags Diagnostics
checkTySigs Bool
bsc [CoreBind]
cbs TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
senv GhcSpecSig
sig =
  do ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     pure $ mconcat (runReader (traverse (check senv) topTs) ef)
                   -- = concatMap (check env) topTs
                   -- (mapMaybe   (checkT env) [ (x, t)     | (x, (t, _)) <- topTs])
                   -- ++ (mapMaybe   (checkE env) [ (x, t, es) | (x, (t, Just es)) <- topTs])
                     <> coreVisitor (checkVisitor ef) senv emptyDiagnostics cbs
                   -- ++ coreVisitor checkVisitor env [] cbs
  where
    check :: F.SEnv F.SortedReft -> (Var, (LocSpecType, Maybe [Located F.Expr])) -> ElabM Diagnostics
    check :: SEnv SortedReft
-> (Var, (Located SpecType, Maybe [Located Expr]))
-> Reader ElabFlags Diagnostics
check          = Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, (Located SpecType, Maybe [Located Expr]))
-> Reader ElabFlags Diagnostics
checkSigTExpr Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv
    locTm :: HashMap Var (Located SpecType, Maybe [Located Expr])
locTm          = [(Var, (Located SpecType, Maybe [Located Expr]))]
-> HashMap Var (Located SpecType, Maybe [Located Expr])
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(Var, (Located SpecType, Maybe [Located Expr]))]
locTs
    ([(Var, (Located SpecType, Maybe [Located Expr]))]
locTs, [(Var, (Located SpecType, Maybe [Located Expr]))]
topTs) = [(Var, (Located SpecType, Maybe [Located Expr]))]
-> ([(Var, (Located SpecType, Maybe [Located Expr]))],
    [(Var, (Located SpecType, Maybe [Located Expr]))])
forall a. [(Var, a)] -> ([(Var, a)], [(Var, a)])
Bare.partitionLocalBinds [(Var, (Located SpecType, Maybe [Located Expr]))]
vtes
    vtes :: [(Var, (Located SpecType, Maybe [Located Expr]))]
vtes           = [ (Var
x, (Located SpecType
t, Maybe [Located Expr]
es)) | (Var
x, Located SpecType
t) <- GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs GhcSpecSig
sig, let es :: Maybe [Located Expr]
es = Var -> HashMap Var [Located Expr] -> Maybe [Located Expr]
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Var
x HashMap Var [Located Expr]
vExprs]
    vExprs :: HashMap Var [Located Expr]
vExprs         = [(Var, [Located Expr])] -> HashMap Var [Located Expr]
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList  [ (Var
x, [Located Expr]
es) | (Var
x, Located SpecType
_, [Located Expr]
es) <- GhcSpecSig -> [(Var, Located SpecType, [Located Expr])]
gsTexprs GhcSpecSig
sig ]

    checkVisitor  :: FC.ElabFlags -> CoreVisitor (F.SEnv F.SortedReft) Diagnostics
    checkVisitor :: ElabFlags -> CoreVisitor (SEnv SortedReft) Diagnostics
checkVisitor ElabFlags
ef = CoreVisitor
                       { envF :: SEnv SortedReft -> Var -> SEnv SortedReft
envF  = \SEnv SortedReft
env Var
v     -> Symbol -> SortedReft -> SEnv SortedReft -> SEnv SortedReft
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
F.insertSEnv (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v) (Var -> SortedReft
vSort Var
v) SEnv SortedReft
env
                       , bindF :: SEnv SortedReft -> Diagnostics -> Var -> Diagnostics
bindF = \SEnv SortedReft
env Diagnostics
acc Var
v -> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (SEnv SortedReft -> Var -> Reader ElabFlags Diagnostics
errs SEnv SortedReft
env Var
v) ElabFlags
ef Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Diagnostics
acc
                       , exprF :: SEnv SortedReft -> Diagnostics -> CoreExpr -> Diagnostics
exprF = \SEnv SortedReft
_   Diagnostics
acc CoreExpr
_ -> Diagnostics
acc
                       }
    vSort :: Var -> SortedReft
vSort            = TCEmb TyCon -> Var -> SortedReft
Bare.varSortedReft TCEmb TyCon
emb
    errs :: F.SEnv F.SortedReft -> Var -> ElabM Diagnostics
    errs :: SEnv SortedReft -> Var -> Reader ElabFlags Diagnostics
errs SEnv SortedReft
env Var
v       = case Var
-> HashMap Var (Located SpecType, Maybe [Located Expr])
-> Maybe (Located SpecType, Maybe [Located Expr])
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Var
v HashMap Var (Located SpecType, Maybe [Located Expr])
locTm of
                         Maybe (Located SpecType, Maybe [Located Expr])
Nothing -> Diagnostics -> Reader ElabFlags Diagnostics
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Diagnostics
emptyDiagnostics
                         Just (Located SpecType, Maybe [Located Expr])
t  -> SEnv SortedReft
-> (Var, (Located SpecType, Maybe [Located Expr]))
-> Reader ElabFlags Diagnostics
check SEnv SortedReft
env (Var
v, (Located SpecType, Maybe [Located Expr])
t)

checkSigTExpr :: BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft
              -> (Var, (LocSpecType, Maybe [Located F.Expr]))
              -> ElabM Diagnostics
checkSigTExpr :: Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, (Located SpecType, Maybe [Located Expr]))
-> Reader ElabFlags Diagnostics
checkSigTExpr Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (Var
x, (Located SpecType
t, Maybe [Located Expr]
es)) =
  do ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     pure $ runReader mbErr1 ef <> runReader mbErr2 ef
   where
    mbErr1 :: Reader ElabFlags Diagnostics
mbErr1 = Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, Located SpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, Located SpecType)
-> Reader ElabFlags Diagnostics
checkBind Bool
bsc Doc
"checkSigTExpr" TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (Var
x, Located SpecType
t)
    mbErr2 :: Reader ElabFlags Diagnostics
mbErr2 = Reader ElabFlags Diagnostics
-> ([Located Expr] -> Reader ElabFlags Diagnostics)
-> Maybe [Located Expr]
-> Reader ElabFlags Diagnostics
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Diagnostics -> Reader ElabFlags Diagnostics
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Diagnostics
emptyDiagnostics) (TCEmb TyCon
-> SEnv SortedReft
-> (Var, Located SpecType, [Located Expr])
-> Reader ElabFlags Diagnostics
forall v.
(Eq v, PPrint v) =>
TCEmb TyCon
-> SEnv SortedReft
-> (v, Located SpecType, [Located Expr])
-> Reader ElabFlags Diagnostics
checkTerminationExpr TCEmb TyCon
emb SEnv SortedReft
env ((Var, Located SpecType, [Located Expr])
 -> Reader ElabFlags Diagnostics)
-> ([Located Expr] -> (Var, Located SpecType, [Located Expr]))
-> [Located Expr]
-> Reader ElabFlags Diagnostics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var
x, Located SpecType
t,)) Maybe [Located Expr]
es
    -- mbErr2 = checkTerminationExpr emb env . (x, t,) =<< es

-- | Used for termination checking. If we have no \"len\" defined /yet/ (for example we are checking
-- 'GHC.Prim') then we want to skip this check.
checkSizeFun :: F.TCEmb TyCon -> F.SEnv F.SortedReft -> [TyConP] -> ElabM Diagnostics
checkSizeFun :: TCEmb TyCon
-> SEnv SortedReft -> [TyConP] -> Reader ElabFlags Diagnostics
checkSizeFun TCEmb TyCon
emb SEnv SortedReft
env [TyConP]
tys =
  do ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     pure $ mkDiagnostics mempty (map mkError (mapMaybe (go ef) tys))
  where
    mkError :: ((Symbol -> a, TyConP), Doc) -> TError t
mkError ((Symbol -> a
f, TyConP
tcp), Doc
msg)  = SrcSpan -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrTyCon (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ TyConP -> SourcePos
tcpLoc TyConP
tcp)
                                 (String -> Doc
text String
"Size function" Doc -> Doc -> Doc
<+> a -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> a
f Symbol
x)
                                                       Doc -> Doc -> Doc
<+> String -> Doc
text String
"should have type int, but it was "
                                                       Doc -> Doc -> Doc
<+> TyCon -> Doc
forall a. PPrint a => a -> Doc
pprint (TyConP -> TyCon
tcpCon TyConP
tcp)
                                                       Doc -> Doc -> Doc
<+> String -> Doc
text String
"."
                                                       Doc -> Doc -> Doc
$+$   Doc
msg)
                                 (TyCon -> Doc
forall a. PPrint a => a -> Doc
pprint (TyConP -> TyCon
tcpCon TyConP
tcp))

    go :: FC.ElabFlags -> TyConP -> Maybe ((F.Symbol -> F.Expr, TyConP), Doc)
    go :: ElabFlags -> TyConP -> Maybe ((Symbol -> Expr, TyConP), Doc)
go ElabFlags
ef TyConP
tcp = case TyConP -> Maybe SizeFun
tcpSizeFun TyConP
tcp of
               Maybe SizeFun
Nothing                   -> Maybe ((Symbol -> Expr, TyConP), Doc)
forall a. Maybe a
Nothing
               Just SizeFun
f | SizeFun -> Bool
isWiredInLenFn SizeFun
f -> Maybe ((Symbol -> Expr, TyConP), Doc)
forall a. Maybe a
Nothing -- Skip the check.
               Just SizeFun
f                    -> ElabFlags
-> (Symbol -> Expr)
-> TyConP
-> Maybe ((Symbol -> Expr, TyConP), Doc)
forall {a}.
Checkable a =>
ElabFlags
-> (Symbol -> a) -> TyConP -> Maybe ((Symbol -> a, TyConP), Doc)
checkWFSize ElabFlags
ef (SizeFun -> Symbol -> Expr
szFun SizeFun
f) TyConP
tcp

    checkWFSize :: ElabFlags
-> (Symbol -> a) -> TyConP -> Maybe ((Symbol -> a, TyConP), Doc)
checkWFSize ElabFlags
ef Symbol -> a
f TyConP
tcp = ((Symbol -> a
f, TyConP
tcp),) (Doc -> ((Symbol -> a, TyConP), Doc))
-> Maybe Doc -> Maybe ((Symbol -> a, TyConP), Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Reader ElabFlags (Maybe Doc) -> ElabFlags -> Maybe Doc
forall r a. Reader r a -> r -> a
runReader (SrcSpan
-> SEnv SortedReft -> Sort -> a -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan
-> SEnv SortedReft -> Sort -> a -> Reader ElabFlags (Maybe Doc)
checkSortFull (TyConP -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan TyConP
tcp) (Symbol -> SortedReft -> SEnv SortedReft -> SEnv SortedReft
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
F.insertSEnv Symbol
x (TyCon -> SortedReft
mkTySort (TyConP -> TyCon
tcpCon TyConP
tcp)) SEnv SortedReft
env) Sort
F.intSort (Symbol -> a
f Symbol
x)) ElabFlags
ef
    x :: Symbol
x                 = Symbol
"x" :: F.Symbol
    mkTySort :: TyCon -> SortedReft
mkTySort TyCon
tc       = TCEmb TyCon -> RType RTyCon RTyVar NoReft -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb (Type -> RType RTyCon RTyVar NoReft
forall r. IsReft r => Type -> RRType r
ofType (Type -> RType RTyCon RTyVar NoReft)
-> Type -> RType RTyCon RTyVar NoReft
forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type
TyConApp TyCon
tc (Var -> Type
TyVarTy (Var -> Type) -> [Var] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Var]
tyConTyVars TyCon
tc) :: RRType NoReft)

    isWiredInLenFn :: SizeFun -> Bool
    isWiredInLenFn :: SizeFun -> Bool
isWiredInLenFn SizeFun
IdSizeFun           = Bool
False
    isWiredInLenFn (SymSizeFun Located Symbol
locSym) = Located Symbol -> Bool
isWiredIn Located Symbol
locSym

checkInv :: BScope
         -> F.TCEmb TyCon
         -> Bare.TyConMap
         -> F.SEnv F.SortedReft
         -> (Maybe Var, LocSpecType)
         -> ElabM Diagnostics
checkInv :: Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Maybe Var, Located SpecType)
-> Reader ElabFlags Diagnostics
checkInv Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (Maybe Var
_, Located SpecType
t) =
  Bool
-> (Doc -> Error)
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> Located SpecType
-> Reader ElabFlags Diagnostics
checkTy Bool
bsc Doc -> Error
err TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env Located SpecType
t
  where
    err :: Doc -> Error
err              = SrcSpan -> SpecType -> Doc -> Error
forall t. SrcSpan -> t -> Doc -> TError t
ErrInvt (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located SpecType -> SourcePos
forall a. Located a -> SourcePos
loc Located SpecType
t) (Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t)

checkIAl :: BScope
         -> F.TCEmb TyCon
         -> Bare.TyConMap
         -> F.SEnv F.SortedReft
         -> [(LocSpecType, LocSpecType)]
         -> ElabM Diagnostics
checkIAl :: Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> [(Located SpecType, Located SpecType)]
-> Reader ElabFlags Diagnostics
checkIAl Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env [(Located SpecType, Located SpecType)]
ss =
  do ds <- ((Located SpecType, Located SpecType)
 -> Reader ElabFlags Diagnostics)
-> [(Located SpecType, Located SpecType)]
-> Reader ElabFlags [Diagnostics]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Located SpecType, Located SpecType)
-> Reader ElabFlags Diagnostics
checkIAlOne Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) [(Located SpecType, Located SpecType)]
ss
     pure $ mconcat ds

checkIAlOne :: BScope
            -> F.TCEmb TyCon
            -> Bare.TyConMap
            -> F.SEnv F.SortedReft
            -> (LocSpecType, LocSpecType)
            -> ElabM Diagnostics
checkIAlOne :: Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Located SpecType, Located SpecType)
-> Reader ElabFlags Diagnostics
checkIAlOne Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (Located SpecType
t1, Located SpecType
t2) =
  do cs <- (Located SpecType -> Reader ElabFlags Diagnostics)
-> [Located SpecType] -> Reader ElabFlags [Diagnostics]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\Located SpecType
t -> Bool
-> (Doc -> Error)
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> Located SpecType
-> Reader ElabFlags Diagnostics
checkTy Bool
bsc (Located SpecType -> Doc -> Error
forall {t}. Located t -> Doc -> TError t
err Located SpecType
t) TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env Located SpecType
t) [Located SpecType
t1, Located SpecType
t2]
     pure $ mconcat $ checkEq : cs
  where
    err :: Located t -> Doc -> TError t
err    Located t
t = SrcSpan -> t -> Doc -> TError t
forall t. SrcSpan -> t -> Doc -> TError t
ErrIAl (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located t -> SourcePos
forall a. Located a -> SourcePos
loc Located t
t) (Located t -> t
forall a. Located a -> a
val Located t
t)
    t1'      :: RSort
    t1' :: RType RTyCon RTyVar NoReft
t1'      = SpecType -> RType RTyCon RTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort (SpecType -> RType RTyCon RTyVar NoReft)
-> SpecType -> RType RTyCon RTyVar NoReft
forall a b. (a -> b) -> a -> b
$ Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t1
    t2'      :: RSort
    t2' :: RType RTyCon RTyVar NoReft
t2'      = SpecType -> RType RTyCon RTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort (SpecType -> RType RTyCon RTyVar NoReft)
-> SpecType -> RType RTyCon RTyVar NoReft
forall a b. (a -> b) -> a -> b
$ Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t2
    checkEq :: Diagnostics
checkEq  = if RType RTyCon RTyVar NoReft
t1' RType RTyCon RTyVar NoReft -> RType RTyCon RTyVar NoReft -> Bool
forall a. Eq a => a -> a -> Bool
== RType RTyCon RTyVar NoReft
t2' then Diagnostics
emptyDiagnostics else [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [Error
errmis]
    errmis :: Error
errmis   = SrcSpan -> SpecType -> SpecType -> Doc -> Error
forall t. SrcSpan -> t -> t -> Doc -> TError t
ErrIAlMis (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located SpecType -> SourcePos
forall a. Located a -> SourcePos
loc Located SpecType
t1) (Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t1) (Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t2) Doc
emsg
    emsg :: Doc
emsg     = Located SpecType -> Doc
forall a. PPrint a => a -> Doc
pprint Located SpecType
t1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"does not match with" Doc -> Doc -> Doc
<+> Located SpecType -> Doc
forall a. PPrint a => a -> Doc
pprint Located SpecType
t2


-- FIXME: Should _ be removed if it isn't used?
checkRTAliases :: String -> t -> [RTAlias s a] -> Diagnostics
checkRTAliases :: forall t s a. String -> t -> [RTAlias s a] -> Diagnostics
checkRTAliases String
msg t
_ [RTAlias s a]
as = Diagnostics
err1s
  where
    err1s :: Diagnostics
err1s               = String -> [RTAlias s a] -> Diagnostics
forall s a. String -> [RTAlias s a] -> Diagnostics
checkDuplicateRTAlias String
msg [RTAlias s a]
as

checkBind :: (PPrint v)
          => BScope
          -> Doc
          -> F.TCEmb TyCon
          -> Bare.TyConMap
          -> F.SEnv F.SortedReft
          -> (v, LocSpecType)
          -> ElabM Diagnostics
checkBind :: forall v.
PPrint v =>
Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, Located SpecType)
-> Reader ElabFlags Diagnostics
checkBind Bool
bsc Doc
s TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (v
v, Located SpecType
t) =
  Bool
-> (Doc -> Error)
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> Located SpecType
-> Reader ElabFlags Diagnostics
checkTy Bool
bsc Doc -> Error
msg TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env Located SpecType
t
  where
    msg :: Doc -> Error
msg                      = SrcSpan -> Maybe Doc -> Doc -> SpecType -> Doc -> Error
forall t. SrcSpan -> Maybe Doc -> Doc -> t -> Doc -> TError t
ErrTySpec (Located SpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located SpecType
t) (Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
s) (v -> Doc
forall a. PPrint a => a -> Doc
pprint v
v) (Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t)


checkTerminationExpr :: (Eq v, PPrint v)
                     => F.TCEmb TyCon
                     -> F.SEnv F.SortedReft
                     -> (v, LocSpecType, [F.Located F.Expr])
                     -> ElabM Diagnostics
checkTerminationExpr :: forall v.
(Eq v, PPrint v) =>
TCEmb TyCon
-> SEnv SortedReft
-> (v, Located SpecType, [Located Expr])
-> Reader ElabFlags Diagnostics
checkTerminationExpr TCEmb TyCon
emb SEnv SortedReft
env (v
v, Loc SourcePos
l SourcePos
_ SpecType
st, [Located Expr]
les) =
  do ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     pure $ mkError "ill-sorted" (go ef les) <> mkError "non-numeric" (go' ef les)
  where
    -- es      = val <$> les
    mkError :: Doc -> Maybe (F.Expr, Doc) -> Diagnostics
    mkError :: Doc -> Maybe (Expr, Doc) -> Diagnostics
mkError Doc
_ Maybe (Expr, Doc)
Nothing = Diagnostics
emptyDiagnostics
    mkError Doc
k (Just (Expr, Doc)
expr') =
      [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [(\ (Expr
e, Doc
d) -> SrcSpan -> Doc -> Doc -> Expr -> SpecType -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> Expr -> t -> Doc -> TError t
ErrTermSpec (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l) (v -> Doc
forall a. PPrint a => a -> Doc
pprint v
v) Doc
k Expr
e SpecType
st Doc
d) (Expr, Doc)
expr']
    -- mkErr   = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "ill-sorted" ) e t d)
    -- mkErr'  = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "non-numeric") e t d)

    go :: FC.ElabFlags -> [F.Located F.Expr] -> Maybe (F.Expr, Doc)
    go :: ElabFlags -> [Located Expr] -> Maybe (Expr, Doc)
go ElabFlags
ef     = (Maybe (Expr, Doc) -> Located Expr -> Maybe (Expr, Doc))
-> Maybe (Expr, Doc) -> [Located Expr] -> Maybe (Expr, Doc)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\Maybe (Expr, Doc)
err Located Expr
e -> Maybe (Expr, Doc)
err Maybe (Expr, Doc) -> Maybe (Expr, Doc) -> Maybe (Expr, Doc)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Located Expr -> Expr
forall a. Located a -> a
val Located Expr
e,) (Doc -> (Expr, Doc)) -> Maybe Doc -> Maybe (Expr, Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Reader ElabFlags (Maybe Doc) -> ElabFlags -> Maybe Doc
forall r a. Reader r a -> r -> a
runReader (SrcSpan -> SEnv Sort -> Expr -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan -> SEnv Sort -> a -> Reader ElabFlags (Maybe Doc)
checkSorted (Located Expr -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan Located Expr
e) SEnv Sort
env' (Located Expr -> Expr
forall a. Located a -> a
val Located Expr
e)) ElabFlags
ef)     Maybe (Expr, Doc)
forall a. Maybe a
Nothing

    go' :: FC.ElabFlags -> [F.Located F.Expr] -> Maybe (F.Expr, Doc)
    go' :: ElabFlags -> [Located Expr] -> Maybe (Expr, Doc)
go' ElabFlags
ef    = (Maybe (Expr, Doc) -> Located Expr -> Maybe (Expr, Doc))
-> Maybe (Expr, Doc) -> [Located Expr] -> Maybe (Expr, Doc)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\Maybe (Expr, Doc)
err Located Expr
e -> Maybe (Expr, Doc)
err Maybe (Expr, Doc) -> Maybe (Expr, Doc) -> Maybe (Expr, Doc)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Located Expr -> Expr
forall a. Located a -> a
val Located Expr
e,) (Doc -> (Expr, Doc)) -> Maybe Doc -> Maybe (Expr, Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Reader ElabFlags (Maybe Doc) -> ElabFlags -> Maybe Doc
forall r a. Reader r a -> r -> a
runReader (SrcSpan -> SEnv Sort -> Expr -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan -> SEnv Sort -> a -> Reader ElabFlags (Maybe Doc)
checkSorted (Located Expr -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan Located Expr
e) SEnv Sort
env' (Located Expr -> Expr
cmpZero Located Expr
e)) ElabFlags
ef) Maybe (Expr, Doc)
forall a. Maybe a
Nothing

    env' :: SEnv Sort
env'    = SortedReft -> Sort
F.sr_sort (SortedReft -> Sort) -> SEnv SortedReft -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SEnv SortedReft -> (Symbol, SortedReft) -> SEnv SortedReft)
-> SEnv SortedReft -> [(Symbol, SortedReft)] -> SEnv SortedReft
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\SEnv SortedReft
e (Symbol
x,SortedReft
s) -> Symbol -> SortedReft -> SEnv SortedReft -> SEnv SortedReft
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
F.insertSEnv Symbol
x SortedReft
s SEnv SortedReft
e) SEnv SortedReft
env [(Symbol, SortedReft)]
xts
    xts :: [(Symbol, SortedReft)]
xts     = ((Symbol, SpecType) -> [(Symbol, SortedReft)])
-> [(Symbol, SpecType)] -> [(Symbol, SortedReft)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Symbol, SpecType) -> [(Symbol, SortedReft)]
mkClss ([(Symbol, SpecType)] -> [(Symbol, SortedReft)])
-> [(Symbol, SpecType)] -> [(Symbol, SortedReft)]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol]
forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_binds RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep) (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [SpecType]
forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_args RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep)
    trep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep    = SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep SpecType
st

    mkClss :: (Symbol, SpecType) -> [(Symbol, SortedReft)]
mkClss (Symbol
_, RApp RTyCon
c [SpecType]
ts [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
_ RReft
_) | RTyCon -> Bool
forall c. TyConable c => c -> Bool
isClass RTyCon
c = TCEmb TyCon -> SpecType -> [(Symbol, SortedReft)]
classBinds TCEmb TyCon
emb (RTyCon -> [SpecType] -> SpecType
forall r c tv. IsReft r => c -> [RType c tv r] -> RType c tv r
rRCls RTyCon
c [SpecType]
ts)
    mkClss (Symbol
x, SpecType
t)                         = [(Symbol
x, SpecType -> SortedReft
rSort SpecType
t)]

    rSort :: SpecType -> SortedReft
rSort   = TCEmb TyCon -> SpecType -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb
    cmpZero :: Located Expr -> Expr
cmpZero Located Expr
e = Brel -> Expr -> Expr -> Expr
forall b v. Brel -> ExprBV b v -> ExprBV b v -> ExprBV b v
F.PAtom Brel
F.Le (Int -> Expr
forall a. Expression a => a -> Expr
F.expr (Int
0 :: Int)) (Located Expr -> Expr
forall a. Located a -> a
val Located Expr
e)

checkTy :: BScope
        -> (Doc -> Error)
        -> F.TCEmb TyCon
        -> Bare.TyConMap
        -> F.SEnv F.SortedReft
        -> LocSpecType
        -> ElabM Diagnostics
checkTy :: Bool
-> (Doc -> Error)
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> Located SpecType
-> Reader ElabFlags Diagnostics
checkTy Bool
bsc Doc -> Error
mkE TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env Located SpecType
t =
  do me <- Bool
-> TCEmb TyCon
-> SEnv SortedReft
-> Located SpecType
-> Reader ElabFlags (Maybe Doc)
checkRType Bool
bsc TCEmb TyCon
emb SEnv SortedReft
env (TyConMap -> TCEmb TyCon -> Located SpecType -> Located SpecType
Bare.txRefSort TyConMap
tcEnv TCEmb TyCon
emb Located SpecType
t)
     pure $ case me of
              Maybe Doc
Nothing -> Diagnostics
emptyDiagnostics
              Just Doc
d  -> [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [Doc -> Error
mkE Doc
d]
  where
    _msg :: String
_msg =  String
"CHECKTY: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. PPrint a => a -> String
showpp (Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t)

checkDupIntersect     :: [(Var, LocSpecType)] -> [(Var, LocSpecType)] -> Diagnostics
checkDupIntersect :: [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> Diagnostics
checkDupIntersect [(Var, Located SpecType)]
xts [(Var, Located SpecType)]
asmSigs =
  [Warning] -> [Error] -> Diagnostics
mkDiagnostics (((Var, Located SpecType) -> Warning)
-> [(Var, Located SpecType)] -> [Warning]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Located SpecType) -> Warning
forall {a} {a}. Show a => (a, Located a) -> Warning
mkWrn {- trace msg -} [(Var, Located SpecType)]
dups) [Error]
forall a. Monoid a => a
mempty
  where
    mkWrn :: (a, Located a) -> Warning
mkWrn (a
x, Located a
t)   = SrcSpan -> Doc -> Warning
mkWarning (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located a -> SourcePos
forall a. Located a -> SourcePos
loc Located a
t) (a -> Doc
forall {a}. Show a => a -> Doc
pprWrn a
x)
    dups :: [(Var, Located SpecType)]
dups           = ((Var, Located SpecType) -> (Var, Located SpecType) -> Bool)
-> [(Var, Located SpecType)]
-> [(Var, Located SpecType)]
-> [(Var, Located SpecType)]
forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
L.intersectBy (Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Var -> Var -> Bool)
-> ((Var, Located SpecType) -> Var)
-> (Var, Located SpecType)
-> (Var, Located SpecType)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Var, Located SpecType) -> Var
forall a b. (a, b) -> a
fst) [(Var, Located SpecType)]
asmSigs [(Var, Located SpecType)]
xts
    pprWrn :: a -> Doc
pprWrn a
v       = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Assume Overwrites Specifications for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v
    -- msg              = "CHECKDUPINTERSECT:" ++ msg1 ++ msg2
    -- msg1             = "\nCheckd-SIGS:\n" ++ showpp (M.fromList xts)
    -- msg2             = "\nAssume-SIGS:\n" ++ showpp (M.fromList asmSigs)


checkDuplicate :: [(Var, LocSpecType)] -> Diagnostics
checkDuplicate :: [(Var, Located SpecType)] -> Diagnostics
checkDuplicate = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty ([Error] -> Diagnostics)
-> ([(Var, Located SpecType)] -> [Error])
-> [(Var, Located SpecType)]
-> Diagnostics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Var, Located SpecType) -> Var)
-> ((Var, Located SpecType) -> SrcSpan)
-> [(Var, Located SpecType)]
-> [Error]
forall a t.
(PPrint a, Eq a, Hashable a) =>
(t -> a) -> (t -> SrcSpan) -> [t] -> [Error]
checkUnique' (Var, Located SpecType) -> Var
forall a b. (a, b) -> a
fst (Located SpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located SpecType -> SrcSpan)
-> ((Var, Located SpecType) -> Located SpecType)
-> (Var, Located SpecType)
-> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Located SpecType) -> Located SpecType
forall a b. (a, b) -> b
snd)

checkClassMethods :: Maybe [ClsInst] -> [Var] ->  [(Var, LocSpecType)] -> Diagnostics
checkClassMethods :: Maybe [ClsInst]
-> [Var] -> [(Var, Located SpecType)] -> Diagnostics
checkClassMethods Maybe [ClsInst]
Nothing      [Var]
_   [(Var, Located SpecType)]
_   = Diagnostics
emptyDiagnostics
checkClassMethods (Just [ClsInst]
clsis) [Var]
cms [(Var, Located SpecType)]
xts =
  [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [SrcSpan -> Doc -> Error
forall t. SrcSpan -> Doc -> TError t
ErrMClass (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located SpecType -> SourcePos
forall a. Located a -> SourcePos
loc Located SpecType
t) (Var -> Doc
forall a. PPrint a => a -> Doc
pprint Var
x)| (Var
x,Located SpecType
t) <- [(Var, Located SpecType)]
dups ]
  where
    dups :: [(Var, Located SpecType)]
dups = String -> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. PPrint a => String -> a -> a
F.notracepp String
"DPS" ([(Var, Located SpecType)] -> [(Var, Located SpecType)])
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a b. (a -> b) -> a -> b
$ ((Var, Located SpecType) -> Bool)
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
ms) (Var -> Bool)
-> ((Var, Located SpecType) -> Var)
-> (Var, Located SpecType)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Located SpecType) -> Var
forall a b. (a, b) -> a
fst) [(Var, Located SpecType)]
xts'
    ms :: [Var]
ms   = String -> [Var] -> [Var]
forall a. PPrint a => String -> a -> a
F.notracepp String
"MS"  ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$ (ClsInst -> [Var]) -> [ClsInst] -> [Var]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Class -> [Var]
classMethods (Class -> [Var]) -> (ClsInst -> Class) -> ClsInst -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClsInst -> Class
is_cls) [ClsInst]
clsis
    xts' :: [(Var, Located SpecType)]
xts' = String -> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. PPrint a => String -> a -> a
F.notracepp String
"XTS" ([(Var, Located SpecType)] -> [(Var, Located SpecType)])
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a b. (a -> b) -> a -> b
$ ((Var, Located SpecType) -> Bool)
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Var, Located SpecType) -> Bool)
-> (Var, Located SpecType)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
cls) (Var -> Bool)
-> ((Var, Located SpecType) -> Var)
-> (Var, Located SpecType)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Located SpecType) -> Var
forall a b. (a, b) -> a
fst) [(Var, Located SpecType)]
xts
    cls :: [Var]
cls  = String -> [Var] -> [Var]
forall a. PPrint a => String -> a -> a
F.notracepp String
"CLS" [Var]
cms

checkDuplicateRTAlias :: String -> [RTAlias s a] -> Diagnostics
checkDuplicateRTAlias :: forall s a. String -> [RTAlias s a] -> Diagnostics
checkDuplicateRTAlias String
s [RTAlias s a]
tas = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty (([RTAlias s a] -> Error) -> [[RTAlias s a]] -> [Error]
forall a b. (a -> b) -> [a] -> [b]
map [RTAlias s a] -> Error
forall {x} {a} {t}. [RTAlias x a] -> TError t
mkError [[RTAlias s a]]
dups)
  where
    mkError :: [RTAlias x a] -> TError t
mkError xs :: [RTAlias x a]
xs@(RTAlias x a
x:[RTAlias x a]
_) = SrcSpan -> Doc -> Doc -> [SrcSpan] -> TError t
forall t. SrcSpan -> Doc -> Doc -> [SrcSpan] -> TError t
ErrDupAlias (Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located LHName -> SrcSpan) -> Located LHName -> SrcSpan
forall a b. (a -> b) -> a -> b
$ RTAlias x a -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName RTAlias x a
x)
                                   (String -> Doc
text String
s)
                                   (Located LHName -> Doc
forall a. PPrint a => a -> Doc
pprint (Located LHName -> Doc) -> Located LHName -> Doc
forall a b. (a -> b) -> a -> b
$ RTAlias x a -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName RTAlias x a
x)
                                   (Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located LHName -> SrcSpan)
-> (RTAlias x a -> Located LHName) -> RTAlias x a -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias x a -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias x a -> SrcSpan) -> [RTAlias x a] -> [SrcSpan]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTAlias x a]
xs)
    mkError []       = Maybe SrcSpan -> String -> TError t
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"mkError: called on empty list"
    dups :: [[RTAlias s a]]
dups             = [[RTAlias s a]
z | z :: [RTAlias s a]
z@(RTAlias s a
_:RTAlias s a
_:[RTAlias s a]
_) <- (RTAlias s a -> Symbol) -> [RTAlias s a] -> [[RTAlias s a]]
forall b a. Ord b => (a -> b) -> [a] -> [[a]]
groupDuplicatesOn (HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol (LHName -> Symbol)
-> (RTAlias s a -> LHName) -> RTAlias s a -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias s a -> Located LHName) -> RTAlias s a -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias s a -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName) [RTAlias s a]
tas]

groupDuplicatesOn :: Ord b => (a -> b) -> [a] -> [[a]]
groupDuplicatesOn :: forall b a. Ord b => (a -> b) -> [a] -> [[a]]
groupDuplicatesOn a -> b
f = (a -> a -> Bool) -> [a] -> [[a]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
L.groupBy (b -> b -> Bool
forall a. Eq a => a -> a -> Bool
(==) (b -> b -> Bool) -> (a -> b) -> a -> a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f) ([a] -> [[a]]) -> ([a] -> [a]) -> [a] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> [a] -> [a]
forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn a -> b
f

checkMismatch        :: (Var, LocSpecType) -> Diagnostics
checkMismatch :: (Var, Located SpecType) -> Diagnostics
checkMismatch (Var
x, Located SpecType
t) = if Bool
ok then Diagnostics
emptyDiagnostics else [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [Error
err]
  where
    ok :: Bool
ok               = Var -> SpecType -> Bool
forall r. Var -> RType RTyCon RTyVar r -> Bool
tyCompat Var
x (Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t)
    err :: Error
err              = Var -> Located SpecType -> Error
errTypeMismatch Var
x Located SpecType
t

tyCompat :: Var -> RType RTyCon RTyVar r -> Bool
tyCompat :: forall r. Var -> RType RTyCon RTyVar r -> Bool
tyCompat Var
x RType RTyCon RTyVar r
t         = RType RTyCon RTyVar NoReft
lqT RType RTyCon RTyVar NoReft -> RType RTyCon RTyVar NoReft -> Bool
forall a. Eq a => a -> a -> Bool
== RType RTyCon RTyVar NoReft
hsT
  where
    RType RTyCon RTyVar NoReft
lqT :: RSort     = RType RTyCon RTyVar r -> RType RTyCon RTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort RType RTyCon RTyVar r
t
    RType RTyCon RTyVar NoReft
hsT :: RSort     = Type -> RType RTyCon RTyVar NoReft
forall r. IsReft r => Type -> RRType r
ofType (Var -> Type
varType Var
x)
    _msg :: String
_msg             = String
"TY-COMPAT: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var -> String
forall a. Outputable a => a -> String
GM.showPpr Var
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": hs = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RType RTyCon RTyVar NoReft -> String
forall a. PPrint a => a -> String
F.showpp RType RTyCon RTyVar NoReft
hsT String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :lq = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RType RTyCon RTyVar NoReft -> String
forall a. PPrint a => a -> String
F.showpp RType RTyCon RTyVar NoReft
lqT

errTypeMismatch     :: Var -> Located SpecType -> Error
errTypeMismatch :: Var -> Located SpecType -> Error
errTypeMismatch Var
x Located SpecType
t = SrcSpan
-> Doc -> Doc -> Doc -> Doc -> Maybe (Doc, Doc) -> SrcSpan -> Error
forall t.
SrcSpan
-> Doc
-> Doc
-> Doc
-> Doc
-> Maybe (Doc, Doc)
-> SrcSpan
-> TError t
ErrMismatch SrcSpan
lqSp (Var -> Doc
forall a. PPrint a => a -> Doc
pprint Var
x) (String -> Doc
text String
"Checked")  Doc
d1 Doc
d2 Maybe (Doc, Doc)
forall a. Maybe a
Nothing SrcSpan
hsSp
  where
    d1 :: Doc
d1              = Type -> Doc
forall a. PPrint a => a -> Doc
pprint (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x
    d2 :: Doc
d2              = Type -> Doc
forall a. PPrint a => a -> Doc
pprint (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False (SpecType -> Type) -> SpecType -> Type
forall a b. (a -> b) -> a -> b
$ Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t
    lqSp :: SrcSpan
lqSp            = Located SpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located SpecType
t
    hsSp :: SrcSpan
hsSp            = Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
x

------------------------------------------------------------------------------------------------
-- | @checkRType@ determines if a type is malformed in a given environment ---------------------
------------------------------------------------------------------------------------------------
checkRType :: BScope -> F.TCEmb TyCon -> F.SEnv F.SortedReft -> LocSpecType -> ElabM (Maybe Doc)
------------------------------------------------------------------------------------------------
checkRType :: Bool
-> TCEmb TyCon
-> SEnv SortedReft
-> Located SpecType
-> Reader ElabFlags (Maybe Doc)
checkRType Bool
bsc TCEmb TyCon
emb SEnv SortedReft
senv Located SpecType
lt =
  do ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     let f SEnv SortedReft
env Maybe (RRType (UReft r))
me UReft r
r Maybe Doc
err = Maybe Doc
err Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Reader ElabFlags (Maybe Doc) -> ElabFlags -> Maybe Doc
forall r a. Reader r a -> r -> a
runReader (SrcSpan
-> SEnv SortedReft
-> TCEmb TyCon
-> Maybe (RRType (UReft r))
-> UReft r
-> Reader ElabFlags (Maybe Doc)
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
SrcSpan
-> SEnv SortedReft
-> TCEmb TyCon
-> Maybe (RRType (UReft r))
-> UReft r
-> Reader ElabFlags (Maybe Doc)
checkReft (Located SpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan Located SpecType
lt) SEnv SortedReft
env TCEmb TyCon
emb Maybe (RRType (UReft r))
me UReft r
r) ElabFlags
ef
     pure $     checkAppTys st
            <|> checkAbstractRefs st
            <|> efoldReft bsc cb (tyToBind emb) (rTypeSortedReft emb) f insertPEnv senv Nothing st
  where
    -- isErasable         = if allowTC then isEmbeddedDict else isClass
    st :: SpecType
st                 = Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
lt
    cb :: RTyCon -> [SpecType] -> [(Symbol, SortedReft)]
cb RTyCon
c [SpecType]
ts            = TCEmb TyCon -> SpecType -> [(Symbol, SortedReft)]
classBinds TCEmb TyCon
emb (RTyCon -> [SpecType] -> SpecType
forall r c tv. IsReft r => c -> [RType c tv r] -> RType c tv r
rRCls RTyCon
c [SpecType]
ts)

    insertPEnv :: PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> SEnv SortedReft -> SEnv SortedReft
insertPEnv PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p SEnv SortedReft
γ     = SEnv SortedReft -> [(Symbol, SortedReft)] -> SEnv SortedReft
forall b a.
(Eq b, Hashable b) =>
SEnvB b a -> [(b, a)] -> SEnvB b a
insertsSEnv SEnv SortedReft
γ ((RType RTyCon RTyVar NoReft -> SortedReft)
-> (Symbol, RType RTyCon RTyVar NoReft) -> (Symbol, SortedReft)
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TCEmb TyCon -> RType RTyCon RTyVar NoReft -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb) ((Symbol, RType RTyCon RTyVar NoReft) -> (Symbol, SortedReft))
-> [(Symbol, RType RTyCon RTyVar NoReft)] -> [(Symbol, SortedReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> [(Symbol, RType RTyCon RTyVar NoReft)]
pbinds PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p)
    pbinds :: PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> [(Symbol, RType RTyCon RTyVar NoReft)]
pbinds PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p           = (PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft) -> Symbol
forall b v t. PVarBV b v t -> b
pname PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p, PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> RType RTyCon RTyVar NoReft
forall r.
(PPrint r, IsReft r) =>
PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft) -> RRType r
pvarRType PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p :: RSort) (Symbol, RType RTyCon RTyVar NoReft)
-> [(Symbol, RType RTyCon RTyVar NoReft)]
-> [(Symbol, RType RTyCon RTyVar NoReft)]
forall a. a -> [a] -> [a]
: [(Symbol
x, RType RTyCon RTyVar NoReft
tx) | (RType RTyCon RTyVar NoReft
tx, Symbol
x, Expr
_) <- PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p]

tyToBind :: F.TCEmb TyCon -> RTVar RTyVar RSort  -> [(F.Symbol, F.SortedReft)]
tyToBind :: TCEmb TyCon
-> RTVar RTyVar (RType RTyCon RTyVar NoReft)
-> [(Symbol, SortedReft)]
tyToBind TCEmb TyCon
emb = RTVInfo (RType RTyCon RTyVar NoReft) -> [(Symbol, SortedReft)]
forall {r}.
(ReftBind r ~ Symbol, ReftVar r ~ Symbol, PPrint r, IsReft r,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
RTVInfo (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> [(Symbol, SortedReft)]
go (RTVInfo (RType RTyCon RTyVar NoReft) -> [(Symbol, SortedReft)])
-> (RTVar RTyVar (RType RTyCon RTyVar NoReft)
    -> RTVInfo (RType RTyCon RTyVar NoReft))
-> RTVar RTyVar (RType RTyCon RTyVar NoReft)
-> [(Symbol, SortedReft)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTVar RTyVar (RType RTyCon RTyVar NoReft)
-> RTVInfo (RType RTyCon RTyVar NoReft)
forall tv s. RTVar tv s -> RTVInfo s
ty_var_info
  where
    go :: RTVInfo (RTypeBV Symbol Symbol RTyCon RTyVar r)
-> [(Symbol, SortedReft)]
go RTVInfo{Bool
Symbol
RTypeBV Symbol Symbol RTyCon RTyVar r
rtv_name :: Symbol
rtv_kind :: RTypeBV Symbol Symbol RTyCon RTyVar r
rtv_is_val :: Bool
rtv_is_pol :: Bool
rtv_is_pol :: forall s. RTVInfo s -> Bool
rtv_is_val :: forall s. RTVInfo s -> Bool
rtv_kind :: forall s. RTVInfo s -> s
rtv_name :: forall s. RTVInfo s -> Symbol
..} = [(Symbol
rtv_name, TCEmb TyCon -> RTypeBV Symbol Symbol RTyCon RTyVar r -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb RTypeBV Symbol Symbol RTyCon RTyVar r
rtv_kind)]
    go RTVNoInfo{} = []

checkAppTys :: RType RTyCon t t1 -> Maybe Doc
checkAppTys :: forall t t1. RType RTyCon t t1 -> Maybe Doc
checkAppTys = RTypeBV Symbol Symbol RTyCon t t1 -> Maybe Doc
forall {b} {v} {tv} {r}. RTypeBV b v RTyCon tv r -> Maybe Doc
go
  where
    go :: RTypeBV b v RTyCon tv r -> Maybe Doc
go (RAllT RTVUBV b v RTyCon tv
_ RTypeBV b v RTyCon tv r
t r
_)    = RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t
    go (RAllP PVUBV b v RTyCon tv
_ RTypeBV b v RTyCon tv r
t)      = RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t
    go (RApp RTyCon
rtc [RTypeBV b v RTyCon tv r]
ts [RTPropBV b v RTyCon tv r]
_ r
_)
      = RTyCon -> Int -> Maybe Doc
checkTcArity RTyCon
rtc ([RTypeBV b v RTyCon tv r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTypeBV b v RTyCon tv r]
ts) Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
        (Maybe Doc -> RTypeBV b v RTyCon tv r -> Maybe Doc)
-> Maybe Doc -> [RTypeBV b v RTyCon tv r] -> Maybe Doc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\Maybe Doc
merr RTypeBV b v RTyCon tv r
t -> Maybe Doc
merr Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t) Maybe Doc
forall a. Maybe a
Nothing [RTypeBV b v RTyCon tv r]
ts
    go (RFun b
_ RFInfo
_ RTypeBV b v RTyCon tv r
t1 RTypeBV b v RTyCon tv r
t2 r
_) = RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t2
    go (RVar tv
_ r
_)       = Maybe Doc
forall a. Maybe a
Nothing
    go (RAllE b
_ RTypeBV b v RTyCon tv r
t1 RTypeBV b v RTyCon tv r
t2)  = RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t2
    go (REx b
_ RTypeBV b v RTyCon tv r
t1 RTypeBV b v RTyCon tv r
t2)    = RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t2
    go (RAppTy RTypeBV b v RTyCon tv r
t1 RTypeBV b v RTyCon tv r
t2 r
_) = RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t2
    go (RRTy [(b, RTypeBV b v RTyCon tv r)]
_ r
_ Oblig
_ RTypeBV b v RTyCon tv r
t)   = RTypeBV b v RTyCon tv r -> Maybe Doc
go RTypeBV b v RTyCon tv r
t
    go (RExprArg Located (ExprBV b v)
_)     = Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> Doc -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Logical expressions cannot appear inside a Haskell type"
    go (RHole r
_)        = Maybe Doc
forall a. Maybe a
Nothing

checkTcArity :: RTyCon -> Arity -> Maybe Doc
checkTcArity :: RTyCon -> Int -> Maybe Doc
checkTcArity RTyCon{ rtc_tc :: RTyCon -> TyCon
rtc_tc = TyCon
tc } Int
givenArity
  | Int
expectedArity Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
givenArity
    = Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> Doc -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Type constructor" Doc -> Doc -> Doc
<+> TyCon -> Doc
forall a. PPrint a => a -> Doc
pprint TyCon
tc
        Doc -> Doc -> Doc
<+> String -> Doc
text String
"expects a maximum" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. PPrint a => a -> Doc
pprint Int
expectedArity
        Doc -> Doc -> Doc
<+> String -> Doc
text String
"arguments but was given" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. PPrint a => a -> Doc
pprint Int
givenArity
        Doc -> Doc -> Doc
<+> String -> Doc
text String
"arguments"
  | Bool
otherwise
    = Maybe Doc
forall a. Maybe a
Nothing
  where
    expectedArity :: Int
expectedArity = TyCon -> Int
tyConRealArity TyCon
tc


checkAbstractRefs
  :: (PPrint t, IsReft t, ReftBind t ~ F.Symbol, ReftVar t ~ F.Symbol, SubsTy RTyVar RSort t) =>
     RType RTyCon RTyVar (UReft t) -> Maybe Doc
checkAbstractRefs :: forall t.
(PPrint t, IsReft t, ReftBind t ~ Symbol, ReftVar t ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) t) =>
RType RTyCon RTyVar (UReft t) -> Maybe Doc
checkAbstractRefs RType RTyCon RTyVar (UReft t)
rt = RType RTyCon RTyVar (UReft t) -> Maybe Doc
forall {v} {r}.
(Fixpoint v, PPrint v, Ord v) =>
RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RType RTyCon RTyVar (UReft t)
rt
  where
    penv :: [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
penv = RType RTyCon RTyVar (UReft t)
-> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
forall {b} {v} {c} {tv} {r}.
RTypeBV b v c tv r -> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
mkPEnv RType RTyCon RTyVar (UReft t)
rt

    go :: RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go t :: RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t@(RAllT RTVar RTyVar (RType RTyCon RTyVar NoReft)
_ RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t1 UReftBV Symbol v r
r)   = RType RTyCon RTyVar NoReft -> UReftBV Symbol v r -> Maybe Doc
forall {v} {r}.
(Fixpoint v, PPrint v, Ord v) =>
RType RTyCon RTyVar NoReft -> UReftBV Symbol v r -> Maybe Doc
check (RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> RType RTyCon RTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t :: RSort) UReftBV Symbol v r
r Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t1
    go (RAllP PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
_ RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t)        = RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t
    go t :: RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t@(RApp RTyCon
c [RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
ts [RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
rs UReftBV Symbol v r
r) = RType RTyCon RTyVar NoReft -> UReftBV Symbol v r -> Maybe Doc
forall {v} {r}.
(Fixpoint v, PPrint v, Ord v) =>
RType RTyCon RTyVar NoReft -> UReftBV Symbol v r -> Maybe Doc
check (RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> RType RTyCon RTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t :: RSort) UReftBV Symbol v r
r Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  (RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
 -> Maybe Doc)
-> [RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
-> Maybe Doc
forall {t :: * -> *} {t} {a}.
Foldable t =>
(t -> Maybe a) -> t t -> Maybe a
efold RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go [RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
ts Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTyCon
-> [RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
-> Maybe Doc
go' RTyCon
c [RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
rs
    go t :: RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t@(RFun Symbol
_ RFInfo
_ RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t1 RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t2 UReftBV Symbol v r
r) = RType RTyCon RTyVar NoReft -> UReftBV Symbol v r -> Maybe Doc
forall {v} {r}.
(Fixpoint v, PPrint v, Ord v) =>
RType RTyCon RTyVar NoReft -> UReftBV Symbol v r -> Maybe Doc
check (RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> RType RTyCon RTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t :: RSort) UReftBV Symbol v r
r Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t2
    go t :: RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t@(RVar RTyVar
_ UReftBV Symbol v r
r)       = RType RTyCon RTyVar NoReft -> UReftBV Symbol v r -> Maybe Doc
forall {v} {r}.
(Fixpoint v, PPrint v, Ord v) =>
RType RTyCon RTyVar NoReft -> UReftBV Symbol v r -> Maybe Doc
check (RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> RType RTyCon RTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t :: RSort) UReftBV Symbol v r
r
    go (RAllE Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t1 RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t2)    = RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t2
    go (REx Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t1 RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t2)      = RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t2
    go t :: RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t@(RAppTy RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t1 RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t2 UReftBV Symbol v r
r) = RType RTyCon RTyVar NoReft -> UReftBV Symbol v r -> Maybe Doc
forall {v} {r}.
(Fixpoint v, PPrint v, Ord v) =>
RType RTyCon RTyVar NoReft -> UReftBV Symbol v r -> Maybe Doc
check (RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> RType RTyCon RTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t :: RSort) UReftBV Symbol v r
r Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t2
    go (RRTy [(Symbol,
  RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r))]
xts UReftBV Symbol v r
_ Oblig
_ RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t)   = (RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
 -> Maybe Doc)
-> [RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
-> Maybe Doc
forall {t :: * -> *} {t} {a}.
Foldable t =>
(t -> Maybe a) -> t t -> Maybe a
efold RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go ((Symbol, RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r))
-> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
forall a b. (a, b) -> b
snd ((Symbol, RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r))
 -> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r))
-> [(Symbol,
     RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r))]
-> [RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol,
  RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r))]
xts) Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t
    go (RExprArg Located Expr
_)       = Maybe Doc
forall a. Maybe a
Nothing
    go (RHole UReftBV Symbol v r
_)          = Maybe Doc
forall a. Maybe a
Nothing

    go' :: RTyCon
-> [RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
-> Maybe Doc
go' RTyCon
c [RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
rs = (Maybe Doc
 -> (RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r),
     PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft))
 -> Maybe Doc)
-> Maybe Doc
-> [(RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r),
     PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft))]
-> Maybe Doc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\Maybe Doc
acc (RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
x, PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
y) -> Maybe Doc
acc Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft) -> Maybe Doc
checkOne' RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
x PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
y) Maybe Doc
forall a. Maybe a
Nothing ([RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
-> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
-> [(RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r),
     PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft))]
forall a b. [a] -> [b] -> [(a, b)]
zip [RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)]
rs (RTyCon -> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
rTyConPVs RTyCon
c))

    checkOne' :: RTPropBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft) -> Maybe Doc
checkOne' (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
xs (RHole UReftBV Symbol v r
_)) PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p
      | [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [RType RTyCon RTyVar NoReft
s1 RType RTyCon RTyVar NoReft -> RType RTyCon RTyVar NoReft -> Bool
forall a. Eq a => a -> a -> Bool
/= RType RTyCon RTyVar NoReft
s2 | ((Symbol
_, RType RTyCon RTyVar NoReft
s1), (RType RTyCon RTyVar NoReft
s2, Symbol
_, Expr
_)) <- [(Symbol, RType RTyCon RTyVar NoReft)]
-> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
-> [((Symbol, RType RTyCon RTyVar NoReft),
     (RType RTyCon RTyVar NoReft, Symbol, Expr))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Symbol, RType RTyCon RTyVar NoReft)]
xs (PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p)]
      = Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> Doc -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Wrong Arguments in" Doc -> Doc -> Doc
<+> PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft) -> Doc
forall a. PPrint a => a -> Doc
pprint PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p
      | [(Symbol, RType RTyCon RTyVar NoReft)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType RTyCon RTyVar NoReft)]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [(RType RTyCon RTyVar NoReft, Symbol, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p)
      = Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> Doc -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Wrong Number of Arguments in" Doc -> Doc -> Doc
<+> PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft) -> Doc
forall a. PPrint a => a -> Doc
pprint PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p
      | Bool
otherwise
      = Maybe Doc
forall a. Maybe a
Nothing
    checkOne' (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
xs RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t) PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p
      | PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> RType RTyCon RTyVar NoReft
forall b v t. PVarBV b v t -> t
pvType PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p RType RTyCon RTyVar NoReft -> RType RTyCon RTyVar NoReft -> Bool
forall a. Eq a => a -> a -> Bool
/= RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> RType RTyCon RTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t
      = Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> Doc -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Unexpected Sort in" Doc -> Doc -> Doc
<+> PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft) -> Doc
forall a. PPrint a => a -> Doc
pprint PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p
      | [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [RType RTyCon RTyVar NoReft
s1 RType RTyCon RTyVar NoReft -> RType RTyCon RTyVar NoReft -> Bool
forall a. Eq a => a -> a -> Bool
/= RType RTyCon RTyVar NoReft
s2 | ((Symbol
_, RType RTyCon RTyVar NoReft
s1), (RType RTyCon RTyVar NoReft
s2, Symbol
_, Expr
_)) <- [(Symbol, RType RTyCon RTyVar NoReft)]
-> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
-> [((Symbol, RType RTyCon RTyVar NoReft),
     (RType RTyCon RTyVar NoReft, Symbol, Expr))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Symbol, RType RTyCon RTyVar NoReft)]
xs (PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p)]
      = Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> Doc -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Wrong Arguments in" Doc -> Doc -> Doc
<+> PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft) -> Doc
forall a. PPrint a => a -> Doc
pprint PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p
      | [(Symbol, RType RTyCon RTyVar NoReft)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RType RTyCon RTyVar NoReft)]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [(RType RTyCon RTyVar NoReft, Symbol, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> [(RType RTyCon RTyVar NoReft, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p)
      = Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> Doc -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Wrong Number of Arguments in" Doc -> Doc -> Doc
<+> PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft) -> Doc
forall a. PPrint a => a -> Doc
pprint PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p
      | Bool
otherwise
      = RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
-> Maybe Doc
go RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol v r)
t


    efold :: (t -> Maybe a) -> t t -> Maybe a
efold t -> Maybe a
f = (Maybe a -> t -> Maybe a) -> Maybe a -> t t -> Maybe a
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\Maybe a
acc t
x -> Maybe a
acc Maybe a -> Maybe a -> Maybe a
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> t -> Maybe a
f t
x) Maybe a
forall a. Maybe a
Nothing

    check :: RType RTyCon RTyVar NoReft -> UReftBV Symbol v r -> Maybe Doc
check RType RTyCon RTyVar NoReft
s (MkUReft r
_ (Pr [UsedPVarBV Symbol v]
ps)) = (Maybe Doc -> UsedPVarBV Symbol v -> Maybe Doc)
-> Maybe Doc -> [UsedPVarBV Symbol v] -> Maybe Doc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\Maybe Doc
acc UsedPVarBV Symbol v
pp -> Maybe Doc
acc Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon RTyVar NoReft -> UsedPVarBV Symbol v -> Maybe Doc
forall {v} {t}.
(Fixpoint v, PPrint v, Ord v) =>
RType RTyCon RTyVar NoReft -> PVarBV Symbol v t -> Maybe Doc
checkOne RType RTyCon RTyVar NoReft
s UsedPVarBV Symbol v
pp) Maybe Doc
forall a. Maybe a
Nothing [UsedPVarBV Symbol v]
ps

    checkOne :: RType RTyCon RTyVar NoReft -> PVarBV Symbol v t -> Maybe Doc
checkOne RType RTyCon RTyVar NoReft
s PVarBV Symbol v t
p | PVarBV Symbol v t -> RType RTyCon RTyVar NoReft
forall {v} {t}.
(Fixpoint v, PPrint v, Ord v) =>
PVarBV Symbol v t -> RType RTyCon RTyVar NoReft
pvType' PVarBV Symbol v t
p RType RTyCon RTyVar NoReft -> RType RTyCon RTyVar NoReft -> Bool
forall a. Eq a => a -> a -> Bool
/= RType RTyCon RTyVar NoReft
s
                 = Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> Doc -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Incorrect Sort:\n\t"
                       Doc -> Doc -> Doc
<+> String -> Doc
text String
"Abstract refinement with type"
                       Doc -> Doc -> Doc
<+> RType RTyCon RTyVar NoReft -> Doc
forall a. PPrint a => a -> Doc
pprint (PVarBV Symbol v t -> RType RTyCon RTyVar NoReft
forall {v} {t}.
(Fixpoint v, PPrint v, Ord v) =>
PVarBV Symbol v t -> RType RTyCon RTyVar NoReft
pvType' PVarBV Symbol v t
p)
                       Doc -> Doc -> Doc
<+> String -> Doc
text String
"is applied to"
                       Doc -> Doc -> Doc
<+> RType RTyCon RTyVar NoReft -> Doc
forall a. PPrint a => a -> Doc
pprint RType RTyCon RTyVar NoReft
s
                       Doc -> Doc -> Doc
<+> String -> Doc
text String
"\n\t In" Doc -> Doc -> Doc
<+> PVarBV Symbol v t -> Doc
forall a. PPrint a => a -> Doc
pprint PVarBV Symbol v t
p
                 | Bool
otherwise
                 = Maybe Doc
forall a. Maybe a
Nothing

    mkPEnv :: RTypeBV b v c tv r -> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
mkPEnv (RAllT RTVUBV b v c tv
_ RTypeBV b v c tv r
t r
_) = RTypeBV b v c tv r -> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
mkPEnv RTypeBV b v c tv r
t
    mkPEnv (RAllP PVarBV b v (RTypeBV b v c tv (NoReftB b))
p RTypeBV b v c tv r
t)   = PVarBV b v (RTypeBV b v c tv (NoReftB b))
pPVarBV b v (RTypeBV b v c tv (NoReftB b))
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
forall a. a -> [a] -> [a]
:RTypeBV b v c tv r -> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
mkPEnv RTypeBV b v c tv r
t
    mkPEnv RTypeBV b v c tv r
_             = []
    pvType' :: PVarBV Symbol v t -> RType RTyCon RTyVar NoReft
pvType' PVarBV Symbol v t
p          = String
-> ListNE (RType RTyCon RTyVar NoReft)
-> RType RTyCon RTyVar NoReft
forall a. HasCallStack => String -> ListNE a -> a
Misc.safeHead (PVarBV Symbol v t -> String
forall a. PPrint a => a -> String
showpp PVarBV Symbol v t
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not in env of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RType RTyCon RTyVar (UReft t) -> String
forall a. PPrint a => a -> String
showpp RType RTyCon RTyVar (UReft t)
rt) [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> RType RTyCon RTyVar NoReft
forall b v t. PVarBV b v t -> t
pvType PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
q | PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
q <- [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
penv, PVarBV Symbol v t -> Symbol
forall b v t. PVarBV b v t -> b
pname PVarBV Symbol v t
p Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft) -> Symbol
forall b v t. PVarBV b v t -> b
pname PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
q]

-- TODO remove the unused UReft arg
checkReft                    :: (PPrint r, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, SubsTy RTyVar (RType RTyCon RTyVar NoReft) r)
                             => F.SrcSpan -> F.SEnv F.SortedReft -> F.TCEmb TyCon -> Maybe (RRType (UReft r)) -> UReft r -> ElabM (Maybe Doc)
checkReft :: forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
SrcSpan
-> SEnv SortedReft
-> TCEmb TyCon
-> Maybe (RRType (UReft r))
-> UReft r
-> Reader ElabFlags (Maybe Doc)
checkReft SrcSpan
_  SEnv SortedReft
_   TCEmb TyCon
_   Maybe (RRType (UReft r))
Nothing  UReft r
_ = Maybe Doc -> Reader ElabFlags (Maybe Doc)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Doc
forall a. Maybe a
Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.
checkReft SrcSpan
sp SEnv SortedReft
env TCEmb TyCon
emb (Just RRType (UReft r)
t) UReft r
_ = do me <- SrcSpan
-> SEnv SortedReft -> SortedReft -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> a -> Reader ElabFlags (Maybe Doc)
checkSortedReftFull SrcSpan
sp SEnv SortedReft
env SortedReft
r
                                     pure $ (\Doc
z -> Doc
dr Doc -> Doc -> Doc
$+$ Doc
z) <$> me
  where
    r :: SortedReft
r                           = TCEmb TyCon -> RRType (UReft r) -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb RRType (UReft r)
t
    dr :: Doc
dr                          = String -> Doc
text String
"Sort Error in Refinement:" Doc -> Doc -> Doc
<+> SortedReft -> Doc
forall a. PPrint a => a -> Doc
pprint SortedReft
r

-- DONT DELETE the below till we've added pred-checking as well
-- checkReft env emb (Just t) _ = checkSortedReft env xs (rTypeSortedReft emb t)
--    where xs                  = fromMaybe [] $ params <$> stripRTypeBase t

-- checkSig env (x, t)
--   = case filter (not . (`S.member` env)) (freeSymbols t) of
--       [] -> TrueNGUAGE ScopedTypeVariables #-}
--       ys -> errorstar (msg ys)
--     where
--       msg ys = printf "Unkown free symbols: %s in specification for %s \n%s\n" (showpp ys) (showpp x) (showpp t)

---------------------------------------------------------------------------------------------------
-- | @checkMeasures@ determines if a measure definition is wellformed -----------------------------
---------------------------------------------------------------------------------------------------
checkMeasures :: F.TCEmb TyCon -> F.SEnv F.SortedReft -> [Measure SpecType DataCon] -> ElabM Diagnostics
---------------------------------------------------------------------------------------------------
checkMeasures :: TCEmb TyCon
-> SEnv SortedReft
-> [MeasureV Symbol SpecType DataCon]
-> Reader ElabFlags Diagnostics
checkMeasures TCEmb TyCon
emb SEnv SortedReft
env = (MeasureV Symbol SpecType DataCon -> Reader ElabFlags Diagnostics)
-> [MeasureV Symbol SpecType DataCon]
-> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (TCEmb TyCon
-> SEnv SortedReft
-> MeasureV Symbol SpecType DataCon
-> Reader ElabFlags Diagnostics
checkMeasure TCEmb TyCon
emb SEnv SortedReft
env)

checkMeasure :: F.TCEmb TyCon -> F.SEnv F.SortedReft -> Measure SpecType DataCon -> ElabM Diagnostics
checkMeasure :: TCEmb TyCon
-> SEnv SortedReft
-> MeasureV Symbol SpecType DataCon
-> Reader ElabFlags Diagnostics
checkMeasure TCEmb TyCon
emb SEnv SortedReft
γ (M name :: Located LHName
name@(Loc SourcePos
src SourcePos
_ LHName
n) SpecType
sort [DefV Symbol SpecType DataCon]
body MeasureKind
_ [([Symbol], Expr)]
_)
  = do me <- (DefV Symbol SpecType DataCon -> Reader ElabFlags (Maybe Doc))
-> [DefV Symbol SpecType DataCon]
-> ReaderT ElabFlags Identity [Maybe Doc]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (SEnv SortedReft
-> TCEmb TyCon
-> Located LHName
-> SpecType
-> DefV Symbol SpecType DataCon
-> Reader ElabFlags (Maybe Doc)
forall t r.
SEnv SortedReft
-> TCEmb TyCon
-> t
-> SpecType
-> Def (RRType r) DataCon
-> Reader ElabFlags (Maybe Doc)
checkMBody SEnv SortedReft
γ TCEmb TyCon
emb Located LHName
name SpecType
sort) [DefV Symbol SpecType DataCon]
body
       pure $ mkDiagnostics mempty [ txerror e | Just e <- me ]
  where
    txerror :: Doc -> TError t
txerror = SrcSpan -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrMeas (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
src) (LHName -> Doc
forall a. PPrint a => a -> Doc
pprint LHName
n)

checkMBody :: F.SEnv F.SortedReft
           -> F.TCEmb TyCon
           -> t
           -> SpecType
           -> Def (RRType r) DataCon
           -> ElabM (Maybe Doc)
checkMBody :: forall t r.
SEnv SortedReft
-> TCEmb TyCon
-> t
-> SpecType
-> Def (RRType r) DataCon
-> Reader ElabFlags (Maybe Doc)
checkMBody SEnv SortedReft
senv TCEmb TyCon
emb t
_ SpecType
sort (Def Located LHName
m DataCon
c Maybe (RRType r)
_ [(Symbol, Maybe (RRType r))]
bs BodyV Symbol
body) = TCEmb TyCon
-> SpecType
-> SEnv SortedReft
-> SrcSpan
-> BodyV Symbol
-> Reader ElabFlags (Maybe Doc)
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnv SortedReft
-> SrcSpan
-> BodyV Symbol
-> Reader ElabFlags (Maybe Doc)
checkMBody' TCEmb TyCon
emb SpecType
sort SEnv SortedReft
γ' SrcSpan
sp BodyV Symbol
body
  where
    sp :: SrcSpan
sp    = Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan Located LHName
m
    γ' :: SEnv SortedReft
γ'    = (SEnv SortedReft -> (Symbol, SortedReft) -> SEnv SortedReft)
-> SEnv SortedReft -> [(Symbol, SortedReft)] -> SEnv SortedReft
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\SEnv SortedReft
γ (Symbol
x, SortedReft
t) -> Symbol -> SortedReft -> SEnv SortedReft -> SEnv SortedReft
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
F.insertSEnv Symbol
x SortedReft
t SEnv SortedReft
γ) SEnv SortedReft
senv [(Symbol, SortedReft)]
xts
    xts :: [(Symbol, SortedReft)]
xts   = [Symbol] -> [SortedReft] -> [(Symbol, SortedReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Symbol, Maybe (RRType r)) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Maybe (RRType r)) -> Symbol)
-> [(Symbol, Maybe (RRType r))] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Maybe (RRType r))]
bs) ([SortedReft] -> [(Symbol, SortedReft)])
-> [SortedReft] -> [(Symbol, SortedReft)]
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon -> SpecType -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb (SpecType -> SortedReft)
-> (SpecType -> SpecType) -> SpecType -> SortedReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(RTyVar, RType RTyCon RTyVar NoReft, SpecType)]
-> SpecType -> SpecType
forall tv (t :: * -> *) r c b v.
(Eq tv, Foldable t, Hashable tv, IsReft r, TyConable c, Binder b,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b)))) =>
t (tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
subsTyVarsMeet [(RTyVar, RType RTyCon RTyVar NoReft, SpecType)]
su  (SpecType -> SortedReft) -> [SpecType] -> [SortedReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            (SpecType -> Bool) -> [SpecType] -> [SpecType]
forall a. (a -> Bool) -> [a] -> [a]
filter SpecType -> Bool
forall {v} {t} {t1}. RTypeBV Symbol v RTyCon t t1 -> Bool
keep (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [SpecType]
forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_args RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep)
    keep :: RTypeBV Symbol v RTyCon t t1 -> Bool
keep | Bool
allowTC = Bool -> Bool
not (Bool -> Bool)
-> (RTypeBV Symbol v RTyCon t t1 -> Bool)
-> RTypeBV Symbol v RTyCon t t1
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol v RTyCon t t1 -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isEmbeddedClass
         | Bool
otherwise = Bool -> Bool
not (Bool -> Bool)
-> (RTypeBV Symbol v RTyCon t t1 -> Bool)
-> RTypeBV Symbol v RTyCon t t1
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol v RTyCon t t1 -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType
    -- YL: extract permitTC information from sort
    allowTC :: Bool
allowTC = (RFInfo -> Bool) -> [RFInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False (Maybe Bool -> Bool) -> (RFInfo -> Maybe Bool) -> RFInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RFInfo -> Maybe Bool
permitTC) (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [RFInfo]
forall b v c tv r. RTypeRepBV b v c tv r -> [RFInfo]
ty_info (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [RFInfo])
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [RFInfo]
forall a b. (a -> b) -> a -> b
$ SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep SpecType
sort)
    trep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep  = SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep SpecType
ct
    su :: [(RTyVar, RType RTyCon RTyVar NoReft, SpecType)]
su    = SpecType
-> SpecType -> [(RTyVar, RType RTyCon RTyVar NoReft, SpecType)]
forall t t2 t1 c tv r.
RType t t2 t1
-> RType c tv r -> [(t2, RType c tv NoReft, RType c tv r)]
checkMBodyUnify (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> SpecType
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
ty_res RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
trep) ([SpecType] -> SpecType
forall a. HasCallStack => [a] -> a
last [SpecType]
txs)
    txs :: [SpecType]
txs   = ([Symbol], [RFInfo], [SpecType], [RReft], SpecType) -> [SpecType]
forall t0 t1 t2 t3 t4. (t0, t1, t2, t3, t4) -> t2
thd5 (([Symbol], [RFInfo], [SpecType], [RReft], SpecType) -> [SpecType])
-> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
-> [SpecType]
forall a b. (a -> b) -> a -> b
$ SpecType -> ([Symbol], [RFInfo], [SpecType], [RReft], SpecType)
forall t t1 a.
RType t t1 a
-> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep SpecType
sort
    ct :: SpecType
ct    = Type -> SpecType
forall r. IsReft r => Type -> RRType r
ofType (Type -> SpecType) -> Type -> SpecType
forall a b. (a -> b) -> a -> b
$ DataCon -> Type
dataConWrapperType DataCon
c :: SpecType

checkMBodyUnify
  :: RType t t2 t1 -> RType c tv r -> [(t2,RType c tv NoReft,RType c tv r)]
checkMBodyUnify :: forall t t2 t1 c tv r.
RType t t2 t1
-> RType c tv r -> [(t2, RType c tv NoReft, RType c tv r)]
checkMBodyUnify = RTypeBV Symbol Symbol t t2 t1
-> RTypeBV Symbol Symbol c tv r
-> [(t2, RTypeBV Symbol Symbol c tv NoReft,
     RTypeBV Symbol Symbol c tv r)]
forall {b} {b} {v} {c} {tv} {r} {v} {c} {tv} {r}.
Binder b =>
RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> [(tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)]
go
  where
    go :: RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> [(tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)]
go (RVar tv
tv r
_) RTypeBV b v c tv r
t      = [(tv
tv, RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort RTypeBV b v c tv r
t, RTypeBV b v c tv r
t)]
    go t :: RTypeBV b v c tv r
t@RApp{} t' :: RTypeBV b v c tv r
t'@RApp{} = [[(tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)]]
-> [(tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)]]
 -> [(tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)])
-> [[(tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)]]
-> [(tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)]
forall a b. (a -> b) -> a -> b
$ (RTypeBV b v c tv r
 -> RTypeBV b v c tv r
 -> [(tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)])
-> [RTypeBV b v c tv r]
-> [RTypeBV b v c tv r]
-> [[(tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> [(tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)]
go (RTypeBV b v c tv r -> [RTypeBV b v c tv r]
forall b v c tv r. RTypeBV b v c tv r -> [RTypeBV b v c tv r]
rt_args RTypeBV b v c tv r
t) (RTypeBV b v c tv r -> [RTypeBV b v c tv r]
forall b v c tv r. RTypeBV b v c tv r -> [RTypeBV b v c tv r]
rt_args RTypeBV b v c tv r
t')
    go RTypeBV b v c tv r
_ RTypeBV b v c tv r
_                = []

checkMBody' :: (PPrint r, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, SubsTy RTyVar RSort r)
            => F.TCEmb TyCon
            -> RType RTyCon RTyVar r
            -> F.SEnv F.SortedReft
            -> F.SrcSpan
            -> Body
            -> ElabM (Maybe Doc)
checkMBody' :: forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnv SortedReft
-> SrcSpan
-> BodyV Symbol
-> Reader ElabFlags (Maybe Doc)
checkMBody' TCEmb TyCon
emb RType RTyCon RTyVar r
sort SEnv SortedReft
γ SrcSpan
sp BodyV Symbol
body =
  case BodyV Symbol
body of
    E Expr
e   -> SrcSpan
-> SEnv SortedReft -> Sort -> Expr -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan
-> SEnv SortedReft -> Sort -> a -> Reader ElabFlags (Maybe Doc)
checkSortFull SrcSpan
sp SEnv SortedReft
γ (TCEmb TyCon -> RType RTyCon RTyVar r -> Sort
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
emb RType RTyCon RTyVar r
sort') Expr
e
    P Expr
p   -> SrcSpan
-> SEnv SortedReft -> Sort -> Expr -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan
-> SEnv SortedReft -> Sort -> a -> Reader ElabFlags (Maybe Doc)
checkSortFull SrcSpan
sp SEnv SortedReft
γ Sort
F.boolSort  Expr
p
    R Symbol
s Expr
p -> SrcSpan
-> SEnv SortedReft -> Sort -> Expr -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan
-> SEnv SortedReft -> Sort -> a -> Reader ElabFlags (Maybe Doc)
checkSortFull SrcSpan
sp (Symbol -> SortedReft -> SEnv SortedReft -> SEnv SortedReft
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
F.insertSEnv Symbol
s SortedReft
sty SEnv SortedReft
γ) Sort
F.boolSort Expr
p
  where
    sty :: SortedReft
sty   = TCEmb TyCon -> RType RTyCon RTyVar r -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb RType RTyCon RTyVar r
sort'
    sort' :: RType RTyCon RTyVar r
sort' = Int -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall r. Int -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
dropNArgs Int
1 RType RTyCon RTyVar r
sort

dropNArgs :: Int -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
dropNArgs :: forall r. Int -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
dropNArgs Int
i RType RTyCon RTyVar r
t = RTypeRepBV Symbol Symbol RTyCon RTyVar r -> RType RTyCon RTyVar r
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep (RTypeRepBV Symbol Symbol RTyCon RTyVar r -> RType RTyCon RTyVar r)
-> RTypeRepBV Symbol Symbol RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall a b. (a -> b) -> a -> b
$ RTypeRepBV Symbol Symbol RTyCon RTyVar r
trep {ty_binds = xs, ty_info = is, ty_args = ts, ty_refts = rs}
  where
    xs :: [Symbol]
xs   = Int -> [Symbol] -> [Symbol]
forall a. Int -> [a] -> [a]
drop Int
i ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ RTypeRepBV Symbol Symbol RTyCon RTyVar r -> [Symbol]
forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_binds RTypeRepBV Symbol Symbol RTyCon RTyVar r
trep
    ts :: [RType RTyCon RTyVar r]
ts   = Int -> [RType RTyCon RTyVar r] -> [RType RTyCon RTyVar r]
forall a. Int -> [a] -> [a]
drop Int
i ([RType RTyCon RTyVar r] -> [RType RTyCon RTyVar r])
-> [RType RTyCon RTyVar r] -> [RType RTyCon RTyVar r]
forall a b. (a -> b) -> a -> b
$ RTypeRepBV Symbol Symbol RTyCon RTyVar r -> [RType RTyCon RTyVar r]
forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_args  RTypeRepBV Symbol Symbol RTyCon RTyVar r
trep
    rs :: [r]
rs   = Int -> [r] -> [r]
forall a. Int -> [a] -> [a]
drop Int
i ([r] -> [r]) -> [r] -> [r]
forall a b. (a -> b) -> a -> b
$ RTypeRepBV Symbol Symbol RTyCon RTyVar r -> [r]
forall b v c tv r. RTypeRepBV b v c tv r -> [r]
ty_refts RTypeRepBV Symbol Symbol RTyCon RTyVar r
trep
    is :: [RFInfo]
is   = Int -> [RFInfo] -> [RFInfo]
forall a. Int -> [a] -> [a]
drop Int
i ([RFInfo] -> [RFInfo]) -> [RFInfo] -> [RFInfo]
forall a b. (a -> b) -> a -> b
$ RTypeRepBV Symbol Symbol RTyCon RTyVar r -> [RFInfo]
forall b v c tv r. RTypeRepBV b v c tv r -> [RFInfo]
ty_info RTypeRepBV Symbol Symbol RTyCon RTyVar r
trep
    trep :: RTypeRepBV Symbol Symbol RTyCon RTyVar r
trep = RType RTyCon RTyVar r -> RTypeRepBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep RType RTyCon RTyVar r
t


getRewriteErrors :: (Var, Located SpecType) -> [TError t]
getRewriteErrors :: forall t. (Var, Located SpecType) -> [TError t]
getRewriteErrors (Var
rw, Located SpecType
t)
  | [(Expr, Expr)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Expr, Expr)] -> Bool) -> [(Expr, Expr)] -> Bool
forall a b. (a -> b) -> a -> b
$ Located SpecType -> [(Expr, Expr)]
refinementEQs Located SpecType
t
  = [SrcSpan -> Doc -> TError t
forall t. SrcSpan -> Doc -> TError t
ErrRewrite (Located SpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located SpecType
t) (Doc -> TError t) -> Doc -> TError t
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
                String
"Unable to use "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var -> String
forall a. Show a => a -> String
show Var
rw
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" as a rewrite because it does not prove an equality, or the equality it proves is trivial." ]
  | Bool
otherwise
  = [TError t]
forall {t}. [TError t]
refErrs [TError t] -> [TError t] -> [TError t]
forall a. [a] -> [a] -> [a]
++
      [ SrcSpan -> Doc -> TError t
forall t. SrcSpan -> Doc -> TError t
ErrRewrite (Located SpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located SpecType
t) (Doc -> TError t) -> Doc -> TError t
forall a b. (a -> b) -> a -> b
$
        String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Could not generate any rewrites from equality. Likely causes: "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n - There are free (uninstantiatable) variables on both sides of the "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"equality\n - The rewrite would diverge"
      | Bool
cannotInstantiate]
    where
        refErrs :: [TError t]
refErrs = ((SpecType, Symbol) -> TError t)
-> [(SpecType, Symbol)] -> [TError t]
forall a b. (a -> b) -> [a] -> [b]
map (SpecType, Symbol) -> TError t
forall {a} {a} {t}. Show a => (a, a) -> TError t
getInnerRefErr (((SpecType, Symbol) -> Bool)
-> [(SpecType, Symbol)] -> [(SpecType, Symbol)]
forall a. (a -> Bool) -> [a] -> [a]
filter (SpecType -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
hasInnerRefinement (SpecType -> Bool)
-> ((SpecType, Symbol) -> SpecType) -> (SpecType, Symbol) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecType, Symbol) -> SpecType
forall a b. (a, b) -> a
fst) ([SpecType] -> [Symbol] -> [(SpecType, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [SpecType]
tyArgs [Symbol]
syms))
        allowedRWs :: [(Expr, Expr)]
allowedRWs = [ (Expr
lhs, Expr
rhs) | (Expr
lhs , Expr
rhs) <- Located SpecType -> [(Expr, Expr)]
refinementEQs Located SpecType
t
                 , HashSet Symbol -> Expr -> Expr -> Bool
canRewrite ([Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList [Symbol]
syms) Expr
lhs Expr
rhs Bool -> Bool -> Bool
||
                   HashSet Symbol -> Expr -> Expr -> Bool
canRewrite ([Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList [Symbol]
syms) Expr
rhs Expr
lhs
                 ]
        cannotInstantiate :: Bool
cannotInstantiate = [(Expr, Expr)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Expr, Expr)]
allowedRWs
        tyArgs :: [SpecType]
tyArgs = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [SpecType]
forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_args  RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
tRep
        syms :: [Symbol]
syms   = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol]
forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_binds RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
tRep
        tRep :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
tRep   = SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep (SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft)
-> SpecType -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
t
        getInnerRefErr :: (a, a) -> TError t
getInnerRefErr (a
_, a
sym) =
          SrcSpan -> Doc -> TError t
forall t. SrcSpan -> Doc -> TError t
ErrRewrite (Located SpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located SpecType
t) (Doc -> TError t) -> Doc -> TError t
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
          String
"Unable to use "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var -> String
forall a. Show a => a -> String
show Var
rw
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" as a rewrite. Functions whose parameters have inner refinements cannot be used as rewrites, but parameter "
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
sym
          String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" contains an inner refinement."


isRefined :: ToReft r => RType c tv r -> Bool
isRefined :: forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RType c tv r
ty
  | Just r
r <- RType c tv r -> Maybe r
forall b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase RType c tv r
ty = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ r -> Bool
forall r. ToReft r => r -> Bool
isTauto r
r
  | Bool
otherwise = Bool
False

hasInnerRefinement :: ToReft r => RType c tv r -> Bool
hasInnerRefinement :: forall r c tv. ToReft r => RType c tv r -> Bool
hasInnerRefinement (RFun Symbol
_ RFInfo
_ RTypeBV Symbol Symbol c tv r
rIn RTypeBV Symbol Symbol c tv r
rOut r
_) =
  RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RTypeBV Symbol Symbol c tv r
rIn Bool -> Bool -> Bool
|| RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RTypeBV Symbol Symbol c tv r
rOut
hasInnerRefinement (RAllT RTVUBV Symbol Symbol c tv
_ RTypeBV Symbol Symbol c tv r
ty  r
_) =
  RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RTypeBV Symbol Symbol c tv r
ty
hasInnerRefinement (RAllP PVUBV Symbol Symbol c tv
_ RTypeBV Symbol Symbol c tv r
ty) =
  RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RTypeBV Symbol Symbol c tv r
ty
hasInnerRefinement (RApp c
_ [RTypeBV Symbol Symbol c tv r]
args [RTPropBV Symbol Symbol c tv r]
_ r
_) =
  (RTypeBV Symbol Symbol c tv r -> Bool)
-> [RTypeBV Symbol Symbol c tv r] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined [RTypeBV Symbol Symbol c tv r]
args
hasInnerRefinement (RAllE Symbol
_ RTypeBV Symbol Symbol c tv r
allarg RTypeBV Symbol Symbol c tv r
ty) =
  RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RTypeBV Symbol Symbol c tv r
allarg Bool -> Bool -> Bool
|| RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RTypeBV Symbol Symbol c tv r
ty
hasInnerRefinement (REx Symbol
_ RTypeBV Symbol Symbol c tv r
allarg RTypeBV Symbol Symbol c tv r
ty) =
  RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RTypeBV Symbol Symbol c tv r
allarg Bool -> Bool -> Bool
|| RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RTypeBV Symbol Symbol c tv r
ty
hasInnerRefinement (RAppTy RTypeBV Symbol Symbol c tv r
arg RTypeBV Symbol Symbol c tv r
res r
_) =
  RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RTypeBV Symbol Symbol c tv r
arg Bool -> Bool -> Bool
|| RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RTypeBV Symbol Symbol c tv r
res
hasInnerRefinement (RRTy [(Symbol, RTypeBV Symbol Symbol c tv r)]
env r
_ Oblig
_ RTypeBV Symbol Symbol c tv r
ty) =
  RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined RTypeBV Symbol Symbol c tv r
ty Bool -> Bool -> Bool
|| ((Symbol, RTypeBV Symbol Symbol c tv r) -> Bool)
-> [(Symbol, RTypeBV Symbol Symbol c tv r)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RTypeBV Symbol Symbol c tv r -> Bool
forall r c tv. ToReft r => RType c tv r -> Bool
isRefined (RTypeBV Symbol Symbol c tv r -> Bool)
-> ((Symbol, RTypeBV Symbol Symbol c tv r)
    -> RTypeBV Symbol Symbol c tv r)
-> (Symbol, RTypeBV Symbol Symbol c tv r)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, RTypeBV Symbol Symbol c tv r)
-> RTypeBV Symbol Symbol c tv r
forall a b. (a, b) -> b
snd) [(Symbol, RTypeBV Symbol Symbol c tv r)]
env
hasInnerRefinement RTypeBV Symbol Symbol c tv r
_ = Bool
False

checkRewrites :: TargetSpec -> Diagnostics
checkRewrites :: TargetSpec -> Diagnostics
checkRewrites TargetSpec
targetSpec = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty (((Var, Located SpecType) -> [Error])
-> [(Var, Located SpecType)] -> [Error]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Var, Located SpecType) -> [Error]
forall t. (Var, Located SpecType) -> [TError t]
getRewriteErrors [(Var, Located SpecType)]
rwSigs)
  where
    rwSigs :: [(Var, Located SpecType)]
rwSigs = ((Var, Located SpecType) -> Bool)
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Var -> HashSet Var -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
`S.member` HashSet Var
rws) (Var -> Bool)
-> ((Var, Located SpecType) -> Var)
-> (Var, Located SpecType)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Located SpecType) -> Var
forall a b. (a, b) -> a
fst) [(Var, Located SpecType)]
sigs
    refl :: GhcSpecRefl
refl   = TargetSpec -> GhcSpecRefl
gsRefl TargetSpec
targetSpec
    sig :: GhcSpecSig
sig    = TargetSpec -> GhcSpecSig
gsSig TargetSpec
targetSpec
    sigs :: [(Var, Located SpecType)]
sigs   = GhcSpecSig -> [(Var, Located SpecType)]
gsTySigs GhcSpecSig
sig [(Var, Located SpecType)]
-> [(Var, Located SpecType)] -> [(Var, Located SpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, Located SpecType)]
gsAsmSigs GhcSpecSig
sig
    rws :: HashSet Var
rws    = HashSet Var -> HashSet Var -> HashSet Var
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union ((Located Var -> Var) -> HashSet (Located Var) -> HashSet Var
forall b a. Hashable b => (a -> b) -> HashSet a -> HashSet b
S.map Located Var -> Var
forall a. Located a -> a
val (HashSet (Located Var) -> HashSet Var)
-> HashSet (Located Var) -> HashSet Var
forall a b. (a -> b) -> a -> b
$ GhcSpecRefl -> HashSet (Located Var)
gsRewrites GhcSpecRefl
refl)
                   ([Var] -> HashSet Var
forall a. Hashable a => [a] -> HashSet a
S.fromList ([Var] -> HashSet Var) -> [Var] -> HashSet Var
forall a b. (a -> b) -> a -> b
$ [[Var]] -> [Var]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Var]] -> [Var]) -> [[Var]] -> [Var]
forall a b. (a -> b) -> a -> b
$ HashMap Var [Var] -> [[Var]]
forall k v. HashMap k v -> [v]
M.elems (GhcSpecRefl -> HashMap Var [Var]
gsRewritesWith GhcSpecRefl
refl))


checkClassMeasures :: [Measure SpecType DataCon] -> Diagnostics
checkClassMeasures :: [MeasureV Symbol SpecType DataCon] -> Diagnostics
checkClassMeasures [MeasureV Symbol SpecType DataCon]
measures = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty (([MeasureV Symbol SpecType DataCon] -> Maybe Error)
-> [[MeasureV Symbol SpecType DataCon]] -> [Error]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [MeasureV Symbol SpecType DataCon] -> Maybe Error
forall {v} {ty} {t}.
Loc (MeasureV v ty DataCon) =>
[MeasureV v ty DataCon] -> Maybe (TError t)
checkOne [[MeasureV Symbol SpecType DataCon]]
byTyCon)
  where
  byName :: [[MeasureV Symbol SpecType DataCon]]
byName = (MeasureV Symbol SpecType DataCon -> LHName)
-> [MeasureV Symbol SpecType DataCon]
-> [[MeasureV Symbol SpecType DataCon]]
forall b a. Ord b => (a -> b) -> [a] -> [[a]]
groupDuplicatesOn (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (MeasureV Symbol SpecType DataCon -> Located LHName)
-> MeasureV Symbol SpecType DataCon
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MeasureV Symbol SpecType DataCon -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName) [MeasureV Symbol SpecType DataCon]
measures

  byTyCon :: [[MeasureV Symbol SpecType DataCon]]
byTyCon = ([MeasureV Symbol SpecType DataCon]
 -> [[MeasureV Symbol SpecType DataCon]])
-> [[MeasureV Symbol SpecType DataCon]]
-> [[MeasureV Symbol SpecType DataCon]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((MeasureV Symbol SpecType DataCon -> TyCon)
-> [MeasureV Symbol SpecType DataCon]
-> [[MeasureV Symbol SpecType DataCon]]
forall b a. Ord b => (a -> b) -> [a] -> [[a]]
groupDuplicatesOn (DataCon -> TyCon
dataConTyCon (DataCon -> TyCon)
-> (MeasureV Symbol SpecType DataCon -> DataCon)
-> MeasureV Symbol SpecType DataCon
-> TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefV Symbol SpecType DataCon -> DataCon
forall v ty ctor. DefV v ty ctor -> ctor
ctor (DefV Symbol SpecType DataCon -> DataCon)
-> (MeasureV Symbol SpecType DataCon
    -> DefV Symbol SpecType DataCon)
-> MeasureV Symbol SpecType DataCon
-> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DefV Symbol SpecType DataCon] -> DefV Symbol SpecType DataCon
forall a. HasCallStack => [a] -> a
head ([DefV Symbol SpecType DataCon] -> DefV Symbol SpecType DataCon)
-> (MeasureV Symbol SpecType DataCon
    -> [DefV Symbol SpecType DataCon])
-> MeasureV Symbol SpecType DataCon
-> DefV Symbol SpecType DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MeasureV Symbol SpecType DataCon -> [DefV Symbol SpecType DataCon]
forall v ty ctor. MeasureV v ty ctor -> [DefV v ty ctor]
msEqns))
                      [[MeasureV Symbol SpecType DataCon]]
byName

  checkOne :: [MeasureV v ty DataCon] -> Maybe (TError t)
checkOne []     = Maybe SrcSpan -> String -> Maybe (TError t)
forall a. Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing String
"checkClassMeasures.checkOne on empty measure group"
  checkOne [MeasureV v ty DataCon
_]    = Maybe (TError t)
forall a. Maybe a
Nothing
  checkOne (MeasureV v ty DataCon
m:[MeasureV v ty DataCon]
ms) = TError t -> Maybe (TError t)
forall a. a -> Maybe a
Just (SrcSpan -> Doc -> Doc -> [SrcSpan] -> TError t
forall t. SrcSpan -> Doc -> Doc -> [SrcSpan] -> TError t
ErrDupIMeas (Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (MeasureV v ty DataCon -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName MeasureV v ty DataCon
m))
                                      (LHName -> Doc
forall a. PPrint a => a -> Doc
pprint (Located LHName -> LHName
forall a. Located a -> a
val (MeasureV v ty DataCon -> Located LHName
forall v ty ctor. MeasureV v ty ctor -> Located LHName
msName MeasureV v ty DataCon
m)))
                                      (TyCon -> Doc
forall a. PPrint a => a -> Doc
pprint ((DataCon -> TyCon
dataConTyCon (DataCon -> TyCon)
-> (MeasureV v ty DataCon -> DataCon)
-> MeasureV v ty DataCon
-> TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefV v ty DataCon -> DataCon
forall v ty ctor. DefV v ty ctor -> ctor
ctor (DefV v ty DataCon -> DataCon)
-> (MeasureV v ty DataCon -> DefV v ty DataCon)
-> MeasureV v ty DataCon
-> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DefV v ty DataCon] -> DefV v ty DataCon
forall a. HasCallStack => [a] -> a
head ([DefV v ty DataCon] -> DefV v ty DataCon)
-> (MeasureV v ty DataCon -> [DefV v ty DataCon])
-> MeasureV v ty DataCon
-> DefV v ty DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MeasureV v ty DataCon -> [DefV v ty DataCon]
forall v ty ctor. MeasureV v ty ctor -> [DefV v ty ctor]
msEqns) MeasureV v ty DataCon
m))
                                      (MeasureV v ty DataCon -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (MeasureV v ty DataCon -> SrcSpan)
-> [MeasureV v ty DataCon] -> [SrcSpan]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MeasureV v ty DataCon
mMeasureV v ty DataCon
-> [MeasureV v ty DataCon] -> [MeasureV v ty DataCon]
forall a. a -> [a] -> [a]
:[MeasureV v ty DataCon]
ms)))