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

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


import           Language.Haskell.Liquid.Constraint.ToFixpoint

import           Liquid.GHC.API                   as Ghc hiding ( Located
                                                                                 , text
                                                                                 , (<+>)
                                                                                 , panic
                                                                                 , ($+$)
                                                                                 , empty
                                                                                 )
import           Control.Applicative                       ((<|>))
import           Control.Arrow                             ((&&&))
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               (checkSorted, checkSortedReftFull, checkSortFull)
import qualified Language.Fixpoint.Types                   as F
import qualified Language.Haskell.Liquid.GHC.Misc          as GM
import           Language.Haskell.Liquid.GHC.Play          (getNonPositivesTyCon)
import           Language.Haskell.Liquid.Misc              (condNull, thd5)
import           Language.Haskell.Liquid.Types
import           Language.Haskell.Liquid.WiredIn
import           Language.Haskell.Liquid.LawInstances      (checkLawInstances)

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


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


checkPositives :: [TyCon] -> Diagnostics
checkPositives :: [TyCon] -> Diagnostics
checkPositives [TyCon]
tys = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [] forall a b. (a -> b) -> a -> b
$ [(TyCon, [DataCon])] -> [Error]
mkNonPosError ([TyCon] -> [(TyCon, [DataCon])]
getNonPositivesTyCon [TyCon]
tys)

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

----------------------------------------------------------------------------------------------
-- | Checking BareSpec ------------------------------------------------------------------------
----------------------------------------------------------------------------------------------
checkBareSpec :: ModName -> Ms.BareSpec -> Either Diagnostics ()
checkBareSpec :: ModName -> BareSpec -> Either Diagnostics ()
checkBareSpec ModName
_ BareSpec
sp
  | Diagnostics
allChecks forall a. Eq a => a -> a -> Bool
== Diagnostics
emptyDiagnostics = forall a b. b -> Either a b
Right ()
  | Bool
otherwise = forall a b. a -> Either a b
Left Diagnostics
allChecks
  where
    allChecks :: Diagnostics
allChecks = forall a. Monoid a => [a] -> a
mconcat [ String -> [LocSymbol] -> Diagnostics
checkUnique   String
"measure"    [LocSymbol]
measures
                        , String -> [LocSymbol] -> Diagnostics
checkUnique   String
"field"      [LocSymbol]
fields
                        , [HashSet LocSymbol] -> Diagnostics
checkDisjoints             [ HashSet LocSymbol
inlines
                                                     , HashSet LocSymbol
hmeasures
                                                     , forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol]
measures
                                                     , HashSet LocSymbol
reflects
                                                     , forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [LocSymbol]
fields
                                                     ]
                        ]
    inlines :: HashSet LocSymbol
inlines   = forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.inlines    BareSpec
sp
    hmeasures :: HashSet LocSymbol
hmeasures = forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas      BareSpec
sp
    reflects :: HashSet LocSymbol
reflects  = forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects   BareSpec
sp
    measures :: [LocSymbol]
measures  = forall ty ctor. Measure ty ctor -> LocSymbol
msName    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.measures BareSpec
sp
    fields :: [LocSymbol]
fields    = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataDecl -> [LocSymbol]
dataDeclFields (forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.dataDecls BareSpec
sp)

dataDeclFields :: DataDecl -> [F.LocSymbol]
dataDeclFields :: DataDecl -> [LocSymbol]
dataDeclFields = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
GM.isTmpSymbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
F.val)
               forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.hashNubWith forall a. Located a -> a
val
               forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataCtor -> [LocSymbol]
dataCtorFields
               forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe []
               forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDecl -> Maybe [DataCtor]
tycDCons

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

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

checkUnique :: String -> [F.LocSymbol] -> Diagnostics
checkUnique :: String -> [LocSymbol] -> Diagnostics
checkUnique String
_ = [Warning] -> [Error] -> Diagnostics
mkDiagnostics forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a t.
(PPrint a, Eq a, Hashable a) =>
(t -> a) -> (t -> SrcSpan) -> [t] -> [Error]
checkUnique' forall a. Located a -> a
F.val 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 = [forall t. SrcSpan -> Doc -> [SrcSpan] -> TError t
ErrDupSpecs SrcSpan
l (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]
_) <- 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 LocSymbol] -> Diagnostics
checkDisjoints []     = Diagnostics
emptyDiagnostics
checkDisjoints [HashSet LocSymbol
_]    = Diagnostics
emptyDiagnostics
checkDisjoints (HashSet LocSymbol
s:[HashSet LocSymbol]
ss) = HashSet LocSymbol -> HashSet LocSymbol -> Diagnostics
checkDisjoint HashSet LocSymbol
s (forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions [HashSet LocSymbol]
ss) forall a. Semigroup a => a -> a -> a
<> [HashSet LocSymbol] -> Diagnostics
checkDisjoints [HashSet LocSymbol]
ss

checkDisjoint :: S.HashSet F.LocSymbol -> S.HashSet F.LocSymbol -> Diagnostics
checkDisjoint :: HashSet LocSymbol -> HashSet LocSymbol -> Diagnostics
checkDisjoint HashSet LocSymbol
s1 HashSet LocSymbol
s2 = String -> [LocSymbol] -> Diagnostics
checkUnique String
"disjoint" (forall a. HashSet a -> [a]
S.toList HashSet LocSymbol
s1 forall a. [a] -> [a] -> [a]
++ forall a. HashSet a -> [a]
S.toList HashSet LocSymbol
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 forall a. Eq a => a -> a -> Bool
== Diagnostics
emptyDiagnostics = forall a b. b -> Either a b
Right ()
  | Bool
otherwise                       = forall a b. a -> Either a b
Left Diagnostics
diagnostics
  where
    diagnostics      :: Diagnostics
    diagnostics :: Diagnostics
diagnostics      =  forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"measure"      TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) (GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas       (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp))
                     forall a. Semigroup a => a -> a -> a
<> forall m. Monoid m => Bool -> m -> m
condNull Bool
noPrune
                        (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"constructor"  TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) (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 forall a b. (a -> b) -> a -> b
$ GhcSpecData -> [(Var, LocSpecType)]
gsCtors      (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp)))
                     forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"assume"       TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) (GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs    (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"reflect"      TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\sig :: (Var, LocSpecType)
sig@(Var
_,LocSpecType
s) -> forall a. PPrint a => String -> a -> a
F.notracepp (forall a. Show a => a -> String
show (forall c tv r. RTypeRep c tv r -> [RFInfo]
ty_info (forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (forall a. Located a -> a
F.val LocSpecType
s)))) (Var, LocSpecType)
sig)) (GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     forall a. Semigroup a => a -> a -> a
<> Bool
-> Bool
-> [CoreBind]
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> GhcSpecSig
-> Diagnostics
checkTySigs Bool
allowHO Bool
bsc [CoreBind]
cbs            TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env                (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp)
                     -- ++ mapMaybe (checkTerminationExpr             emb       env) (gsTexprs     (gsSig  sp))
                     forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"class method" TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) (GhcSpecSig -> [(Var, LocSpecType)]
clsSigs      (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Maybe Var, LocSpecType)
-> Diagnostics
checkInv Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env)                 (GhcSpecData -> [(Maybe Var, LocSpecType)]
gsInvariants (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp))
                     forall a. Semigroup a => a -> a -> a
<> Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> [(LocSpecType, LocSpecType)]
-> Diagnostics
checkIAl Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env                            (GhcSpecData -> [(LocSpecType, LocSpecType)]
gsIaliases   (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp))
                     forall a. Semigroup a => a -> a -> a
<> TCEmb TyCon
-> SEnv SortedReft
-> [Measure (RType RTyCon RTyVar RReft) DataCon]
-> Diagnostics
checkMeasures TCEmb TyCon
emb SEnv SortedReft
env [Measure (RType RTyCon RTyVar RReft) DataCon]
ms
                     forall a. Semigroup a => a -> a -> a
<> [Measure (RType RTyCon RTyVar RReft) DataCon] -> Diagnostics
checkClassMeasures                                        (GhcSpecData -> [Measure (RType RTyCon RTyVar RReft) DataCon]
gsMeasures (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp))
                     forall a. Semigroup a => a -> a -> a
<> Maybe [ClsInst] -> [Var] -> [(Var, LocSpecType)] -> Diagnostics
checkClassMethods (TargetSrc -> Maybe [ClsInst]
gsCls TargetSrc
src) (GhcSpecVars -> [Var]
gsCMethods (TargetSpec -> GhcSpecVars
gsVars TargetSpec
tsp)) (GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs     (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     -- <> foldMap checkMismatch sigs
                     forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Var, LocSpecType) -> Diagnostics
checkMismatch (forall a. (a -> Bool) -> [a] -> [a]
L.filter (\(Var
v,LocSpecType
_) -> Bool -> Bool
not (forall a. Symbolic a => a -> Bool
GM.isSCSel Var
v Bool -> Bool -> Bool
|| forall a. Symbolic a => a -> Bool
GM.isMethod Var
v)) [(Var, LocSpecType)]
sigs)
                     forall a. Semigroup a => a -> a -> a
<> [(Var, LocSpecType)] -> Diagnostics
checkDuplicate                                            (GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs     (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     -- TODO-REBARE ++ checkQualifiers env                                       (gsQualifiers (gsQual sp))
                     forall a. Semigroup a => a -> a -> a
<> [(Var, LocSpecType)] -> Diagnostics
checkDuplicate                                            (GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs    (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     forall a. Semigroup a => a -> a -> a
<> [(Var, LocSpecType)] -> [(Var, LocSpecType)] -> Diagnostics
checkDupIntersect                                         (GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp)) (GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     forall a. Semigroup a => a -> a -> a
<> forall t s a. String -> t -> [Located (RTAlias s a)] -> Diagnostics
checkRTAliases String
"Type Alias" SEnv SortedReft
env            [Located (RTAlias Symbol BareType)]
tAliases
                     forall a. Semigroup a => a -> a -> a
<> forall t s a. String -> t -> [Located (RTAlias s a)] -> Diagnostics
checkRTAliases String
"Pred Alias" SEnv SortedReft
env            [Located (RTAlias Symbol Expr)]
eAliases
                     -- ++ _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
                     forall a. Semigroup a => a -> a -> a
<> TCEmb TyCon -> SEnv SortedReft -> [TyConP] -> Diagnostics
checkSizeFun TCEmb TyCon
emb SEnv SortedReft
env                                      (GhcSpecNames -> [TyConP]
gsTconsP (TargetSpec -> GhcSpecNames
gsName TargetSpec
tsp))
                     forall a. Semigroup a => a -> a -> a
<> forall v. PPrint v => [(v, LocSpecType)] -> Diagnostics
checkPlugged (forall a. [Maybe a] -> [a]
catMaybes [ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Symbol -> Symbol
F.dropSym Int
2 forall a b. (a -> b) -> a -> b
$ forall t. NamedThing t => t -> Symbol
GM.simplesymbol Var
x,) (forall t. MethodType t -> Maybe t
getMethodType MethodType LocSpecType
t) | (Var
x, MethodType LocSpecType
t) <- GhcSpecSig -> [(Var, MethodType LocSpecType)]
gsMethods (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp) ])
                     forall a. Semigroup a => a -> a -> a
<> GhcSpecLaws -> Diagnostics
checkLawInstances (TargetSpec -> GhcSpecLaws
gsLaws TargetSpec
tsp)
                     forall a. Semigroup a => a -> a -> a
<> TargetSpec -> Diagnostics
checkRewrites TargetSpec
tsp

    _rClasses :: [RClass LocBareType]
_rClasses         = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall ty bndr. Spec ty bndr -> [RClass ty]
Ms.classes [BareSpec]
specs
    _rInsts :: [RInstance LocBareType]
_rInsts           = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall ty bndr. Spec ty bndr -> [RInstance ty]
Ms.rinstance [BareSpec]
specs
    tAliases :: [Located (RTAlias Symbol BareType)]
tAliases          = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol BareType)]
Ms.aliases BareSpec
sp  | BareSpec
sp <- [BareSpec]
specs]
    eAliases :: [Located (RTAlias Symbol Expr)]
eAliases          = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
Ms.ealiases BareSpec
sp | BareSpec
sp <- [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 :: [Measure (RType RTyCon RTyVar RReft) DataCon]
ms               = GhcSpecData -> [Measure (RType RTyCon RTyVar RReft) DataCon]
gsMeasures (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp)
    clsSigs :: GhcSpecSig -> [(Var, LocSpecType)]
clsSigs GhcSpecSig
sp       = [ (Var
v, LocSpecType
t) | (Var
v, LocSpecType
t) <- GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
sp, forall a. Maybe a -> Bool
isJust (Var -> Maybe Class
isClassOpId_maybe Var
v) ]
    sigs :: [(Var, LocSpecType)]
sigs             = GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp) forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp) forall a. [a] -> [a] -> [a]
++ GhcSpecData -> [(Var, LocSpecType)]
gsCtors (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp)
    -- allowTC          = typeclass (getConfig sp)
    allowHO :: Bool
allowHO          = forall t. HasConfig t => t -> Bool
higherOrderFlag TargetSpec
tsp
    bsc :: Bool
bsc              = Config -> Bool
bscope (forall t. HasConfig t => t -> Config
getConfig TargetSpec
tsp)
    noPrune :: Bool
noPrune          = Bool -> Bool
not (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, forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 forall a b. (a -> b) -> a -> b
$ GhcSpecData -> [([Symbol], Expr)]
gsUnsorted forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecData
gsData TargetSpec
tsp
    -- env'             = L.foldl' (\e (x, s) -> insertSEnv x (RR s mempty) e) env wiredSortedSyms





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


--------------------------------------------------------------------------------
checkTySigs :: Bool
            -> BScope
            -> [CoreBind]
            -> F.TCEmb TyCon
            -> Bare.TyConMap
            -> F.SEnv F.SortedReft
            -> GhcSpecSig
            -> Diagnostics
--------------------------------------------------------------------------------
checkTySigs :: Bool
-> Bool
-> [CoreBind]
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> GhcSpecSig
-> Diagnostics
checkTySigs Bool
allowHO Bool
bsc [CoreBind]
cbs TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
senv GhcSpecSig
sig
                   = forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map (SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr])) -> Diagnostics
check SEnv SortedReft
senv) [(Var, (LocSpecType, Maybe [Located Expr]))]
topTs)
                   -- = concatMap (check env) topTs
                   -- (mapMaybe   (checkT env) [ (x, t)     | (x, (t, _)) <- topTs])
                   -- ++ (mapMaybe   (checkE env) [ (x, t, es) | (x, (t, Just es)) <- topTs])
                  forall a. Semigroup a => a -> a -> a
<> forall env acc.
CoreVisitor env acc -> env -> acc -> [CoreBind] -> acc
coreVisitor CoreVisitor (SEnv SortedReft) Diagnostics
checkVisitor SEnv SortedReft
senv Diagnostics
emptyDiagnostics [CoreBind]
cbs
                   -- ++ coreVisitor checkVisitor env [] cbs
  where
    check :: SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr])) -> Diagnostics
check SEnv SortedReft
env      = Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr]))
-> Diagnostics
checkSigTExpr Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env
    locTm :: HashMap Var (LocSpecType, Maybe [Located Expr])
locTm          = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Var, (LocSpecType, Maybe [Located Expr]))]
locTs
    ([(Var, (LocSpecType, Maybe [Located Expr]))]
locTs, [(Var, (LocSpecType, Maybe [Located Expr]))]
topTs) = forall a. [(Var, a)] -> ([(Var, a)], [(Var, a)])
Bare.partitionLocalBinds [(Var, (LocSpecType, Maybe [Located Expr]))]
vtes
    vtes :: [(Var, (LocSpecType, Maybe [Located Expr]))]
vtes           = [ (Var
x, (LocSpecType
t, Maybe [Located Expr]
es)) | (Var
x, LocSpecType
t) <- GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs GhcSpecSig
sig, let es :: Maybe [Located Expr]
es = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Var
x HashMap Var [Located Expr]
vExprs]
    vExprs :: HashMap Var [Located Expr]
vExprs         = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList  [ (Var
x, [Located Expr]
es) | (Var
x, LocSpecType
_, [Located Expr]
es) <- GhcSpecSig -> [(Var, LocSpecType, [Located Expr])]
gsTexprs GhcSpecSig
sig ]

    checkVisitor  :: CoreVisitor (F.SEnv F.SortedReft) Diagnostics
    checkVisitor :: CoreVisitor (SEnv SortedReft) Diagnostics
checkVisitor   = CoreVisitor
                       { envF :: SEnv SortedReft -> Var -> SEnv SortedReft
envF  = \SEnv SortedReft
env Var
v     -> forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv (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 -> SEnv SortedReft -> Var -> Diagnostics
errs SEnv SortedReft
env Var
v 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 :: SEnv SortedReft -> Var -> Diagnostics
errs SEnv SortedReft
env Var
v       = case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Var
v HashMap Var (LocSpecType, Maybe [Located Expr])
locTm of
                         Maybe (LocSpecType, Maybe [Located Expr])
Nothing -> Diagnostics
emptyDiagnostics
                         Just (LocSpecType, Maybe [Located Expr])
t  -> SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr])) -> Diagnostics
check SEnv SortedReft
env (Var
v, (LocSpecType, Maybe [Located Expr])
t)

checkSigTExpr :: Bool -> BScope -> F.TCEmb TyCon -> Bare.TyConMap -> F.SEnv F.SortedReft
              -> (Var, (LocSpecType, Maybe [Located F.Expr]))
              -> Diagnostics
checkSigTExpr :: Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr]))
-> Diagnostics
checkSigTExpr Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (Var
x, (LocSpecType
t, Maybe [Located Expr]
es))
           = Diagnostics
mbErr1 forall a. Semigroup a => a -> a -> a
<> Diagnostics
mbErr2
   where
    mbErr1 :: Diagnostics
mbErr1 = forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
empty TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (Var
x, LocSpecType
t)
    mbErr2 :: Diagnostics
mbErr2 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Diagnostics
emptyDiagnostics (forall v.
(Eq v, PPrint v) =>
TCEmb TyCon
-> SEnv SortedReft
-> (v, LocSpecType, [Located Expr])
-> Diagnostics
checkTerminationExpr TCEmb TyCon
emb SEnv SortedReft
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var
x, LocSpecType
t,)) Maybe [Located Expr]
es
    -- mbErr2 = checkTerminationExpr emb env . (x, t,) =<< es

_checkQualifiers :: F.SEnv F.SortedReft -> [F.Qualifier] -> [Error]
_checkQualifiers :: SEnv SortedReft -> [Qualifier] -> [Error]
_checkQualifiers = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEnv SortedReft -> Qualifier -> Maybe Error
checkQualifier

checkQualifier       :: F.SEnv F.SortedReft -> F.Qualifier -> Maybe Error
checkQualifier :: SEnv SortedReft -> Qualifier -> Maybe Error
checkQualifier SEnv SortedReft
env Qualifier
q =  forall {t}. Doc -> TError t
mkE forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc
checkSortFull (forall a. Loc a => a -> SrcSpan
F.srcSpan Qualifier
q) SEnv SortedReft
γ Sort
F.boolSort  (Qualifier -> Expr
F.qBody Qualifier
q)
  where
    γ :: SEnv SortedReft
γ                = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\SEnv SortedReft
e (Symbol
x, Sort
s) -> forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
x (Sort -> Reft -> SortedReft
F.RR Sort
s forall a. Monoid a => a
mempty) SEnv SortedReft
e) SEnv SortedReft
env (Qualifier -> [(Symbol, Sort)]
F.qualBinds Qualifier
q forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
wiredSortedSyms)
    mkE :: Doc -> TError t
mkE              = forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadQual (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Qualifier
q) (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ Qualifier -> Symbol
F.qName Qualifier
q)

-- | 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] -> Diagnostics
checkSizeFun :: TCEmb TyCon -> SEnv SortedReft -> [TyConP] -> Diagnostics
checkSizeFun TCEmb TyCon
emb SEnv SortedReft
env [TyConP]
tys = [Warning] -> [Error] -> Diagnostics
mkDiagnostics forall a. Monoid a => a
mempty (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {t}.
PPrint a =>
((Symbol -> a, TyConP), Doc) -> TError t
mkError (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TyConP -> Maybe ((Symbol -> Expr, TyConP), Doc)
go [TyConP]
tys))
  where
    mkError :: ((Symbol -> a, TyConP), Doc) -> TError t
mkError ((Symbol -> a
f, TyConP
tcp), Doc
msg)  = forall t. SrcSpan -> Doc -> Doc -> TError t
ErrTyCon (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ TyConP -> SourcePos
tcpLoc TyConP
tcp)
                                 (String -> Doc
text String
"Size function" Doc -> Doc -> 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
<+> forall a. PPrint a => a -> Doc
pprint (TyConP -> TyCon
tcpCon TyConP
tcp)
                                                       Doc -> Doc -> Doc
<+> String -> Doc
text String
"."
                                                       Doc -> Doc -> Doc
$+$   Doc
msg)
                                 (forall a. PPrint a => a -> Doc
pprint (TyConP -> TyCon
tcpCon TyConP
tcp))
    go :: TyConP -> Maybe ((Symbol -> Expr, TyConP), Doc)
go TyConP
tcp = case TyConP -> Maybe SizeFun
tcpSizeFun TyConP
tcp of
               Maybe SizeFun
Nothing                   -> forall a. Maybe a
Nothing
               Just SizeFun
f | SizeFun -> Bool
isWiredInLenFn SizeFun
f -> forall a. Maybe a
Nothing -- Skip the check.
               Just SizeFun
f                    -> forall {a}.
Checkable a =>
(Symbol -> a) -> TyConP -> Maybe ((Symbol -> a, TyConP), Doc)
checkWFSize (SizeFun -> Symbol -> Expr
szFun SizeFun
f) TyConP
tcp

    checkWFSize :: (Symbol -> a) -> TyConP -> Maybe ((Symbol -> a, TyConP), Doc)
checkWFSize Symbol -> a
f TyConP
tcp = ((Symbol -> a
f, TyConP
tcp),) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc
checkSortFull (forall a. Loc a => a -> SrcSpan
F.srcSpan TyConP
tcp) (forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
x (TyCon -> SortedReft
mkTySort (TyConP -> TyCon
tcpCon TyConP
tcp)) SEnv SortedReft
env) Sort
F.intSort (Symbol -> a
f Symbol
x)
    x :: Symbol
x                 = Symbol
"x" :: F.Symbol
    mkTySort :: TyCon -> SortedReft
mkTySort TyCon
tc       = forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb (forall r. Monoid r => Type -> RRType r
ofType forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type
TyConApp TyCon
tc (Var -> Type
TyVarTy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Var]
tyConTyVars TyCon
tc) :: RRType ())

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

_checkRefinedClasses :: [RClass LocBareType] -> [RInstance LocBareType] -> [Error]
_checkRefinedClasses :: [RClass LocBareType] -> [RInstance LocBareType] -> [Error]
_checkRefinedClasses [RClass LocBareType]
definitions [RInstance LocBareType]
instances
  = forall {t}. (BTyCon, [RInstance LocBareType]) -> TError t
mkError forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(BTyCon, [RInstance LocBareType])]
duplicates
  where
    duplicates :: [(BTyCon, [RInstance LocBareType])]
duplicates
      = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (BTyCon -> Maybe (BTyCon, [RInstance LocBareType])
checkCls forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty. RClass ty -> BTyCon
rcName) [RClass LocBareType]
definitions
    checkCls :: BTyCon -> Maybe (BTyCon, [RInstance LocBareType])
checkCls BTyCon
cls
      = case BTyCon -> [RInstance LocBareType]
findConflicts BTyCon
cls of
          []        -> forall a. Maybe a
Nothing
          [RInstance LocBareType]
conflicts -> forall a. a -> Maybe a
Just (BTyCon
cls, [RInstance LocBareType]
conflicts)
    findConflicts :: BTyCon -> [RInstance LocBareType]
findConflicts BTyCon
cls
      = forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
== BTyCon
cls) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. RInstance t -> BTyCon
riclass) [RInstance LocBareType]
instances
    mkError :: (BTyCon, [RInstance LocBareType]) -> TError t
mkError (BTyCon
cls, [RInstance LocBareType]
conflicts)
      = forall t. SrcSpan -> Doc -> [(SrcSpan, Doc)] -> TError t
ErrRClass (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc forall a b. (a -> b) -> a -> b
$ BTyCon -> LocSymbol
btc_tc BTyCon
cls)
                  (forall a. PPrint a => a -> Doc
pprint BTyCon
cls) (RInstance LocBareType -> (SrcSpan, Doc)
ofConflict forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RInstance LocBareType]
conflicts)
    ofConflict :: RInstance LocBareType -> (SrcSpan, Doc)
ofConflict
      = SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> SourcePos
loc forall b c a. (b -> c) -> (a -> b) -> a -> c
. BTyCon -> LocSymbol
btc_tc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. RInstance t -> BTyCon
riclass forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall a. PPrint a => a -> Doc
pprint forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. RInstance t -> [t]
ritype

_checkDuplicateFieldNames :: [(DataCon, DataConP)]  -> [Error]
_checkDuplicateFieldNames :: [(DataCon, DataConP)] -> [Error]
_checkDuplicateFieldNames = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a} {t}. PPrint a => (a, DataConP) -> Maybe (TError t)
go
  where
    go :: (a, DataConP) -> Maybe (TError t)
go (a
d, DataConP
dts)          = forall {a} {t}.
PPrint a =>
SourcePos -> a -> [Symbol] -> Maybe (TError t)
checkNoDups (DataConP -> SourcePos
dcpLoc DataConP
dts) a
d (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataConP -> [(Symbol, RType RTyCon RTyVar RReft)]
dcpTyArgs DataConP
dts)
    checkNoDups :: SourcePos -> a -> [Symbol] -> Maybe (TError t)
checkNoDups SourcePos
l a
d [Symbol]
xs   = forall {a} {t}. PPrint a => SourcePos -> a -> Symbol -> TError t
mkError SourcePos
l a
d forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Ord a => [a] -> Maybe a
_firstDuplicate [Symbol]
xs

    mkError :: SourcePos -> a -> Symbol -> TError t
mkError SourcePos
l a
d Symbol
x = forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l)
                             (forall a. PPrint a => a -> Doc
pprint a
d)
                             (String -> Doc
text String
"Multiple declarations of record selector" Doc -> Doc -> Doc
<+> Symbol -> Doc
pprintSymbol Symbol
x)

_firstDuplicate :: Ord a => [a] -> Maybe a
_firstDuplicate :: forall a. Ord a => [a] -> Maybe a
_firstDuplicate = forall {a}. Eq a => [a] -> Maybe a
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
L.sort
  where
    go :: [a] -> Maybe a
go (a
y:a
x:[a]
xs) | a
x forall a. Eq a => a -> a -> Bool
== a
y    = forall a. a -> Maybe a
Just a
x
                | Bool
otherwise = [a] -> Maybe a
go (a
xforall a. a -> [a] -> [a]
:[a]
xs)
    go [a]
_                    = forall a. Maybe a
Nothing

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

checkIAl :: Bool
         -> BScope
         -> F.TCEmb TyCon
         -> Bare.TyConMap
         -> F.SEnv F.SortedReft
         -> [(LocSpecType, LocSpecType)]
         -> Diagnostics
checkIAl :: Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> [(LocSpecType, LocSpecType)]
-> Diagnostics
checkIAl Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env = forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (LocSpecType, LocSpecType)
-> Diagnostics
checkIAlOne Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env)

checkIAlOne :: Bool
            -> BScope
            -> F.TCEmb TyCon
            -> Bare.TyConMap
            -> F.SEnv F.SortedReft
            -> (LocSpecType, LocSpecType)
            -> Diagnostics
checkIAlOne :: Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (LocSpecType, LocSpecType)
-> Diagnostics
checkIAlOne Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (LocSpecType
t1, LocSpecType
t2) = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ Diagnostics
checkEq forall a. a -> [a] -> [a]
: (LocSpecType -> Diagnostics
tcheck forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSpecType
t1, LocSpecType
t2])
  where
    tcheck :: LocSpecType -> Diagnostics
tcheck LocSpecType
t = Bool
-> Bool
-> (Doc -> Error)
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> LocSpecType
-> Diagnostics
checkTy Bool
allowHO Bool
bsc (forall {t}. Located t -> Doc -> TError t
err LocSpecType
t) TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env LocSpecType
t
    err :: Located t -> Doc -> TError t
err    Located t
t = forall t. SrcSpan -> t -> Doc -> TError t
ErrIAl (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc Located t
t) (forall a. Located a -> a
val Located t
t)
    t1'      :: RSort
    t1' :: RSort
t1'      = forall c tv r. RType c tv r -> RType c tv ()
toRSort forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSpecType
t1
    t2'      :: RSort
    t2' :: RSort
t2'      = forall c tv r. RType c tv r -> RType c tv ()
toRSort forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSpecType
t2
    checkEq :: Diagnostics
checkEq  = if RSort
t1' forall a. Eq a => a -> a -> Bool
== RSort
t2' then Diagnostics
emptyDiagnostics else [Warning] -> [Error] -> Diagnostics
mkDiagnostics forall a. Monoid a => a
mempty [Error
errmis]
    errmis :: Error
errmis   = forall t. SrcSpan -> t -> t -> Doc -> TError t
ErrIAlMis (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc LocSpecType
t1) (forall a. Located a -> a
val LocSpecType
t1) (forall a. Located a -> a
val LocSpecType
t2) Doc
emsg
    emsg :: Doc
emsg     = forall a. PPrint a => a -> Doc
pprint LocSpecType
t1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"does not match with" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint LocSpecType
t2


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

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


checkTerminationExpr :: (Eq v, PPrint v)
                     => F.TCEmb TyCon
                     -> F.SEnv F.SortedReft
                     -> (v, LocSpecType, [F.Located F.Expr])
                     -> Diagnostics
checkTerminationExpr :: forall v.
(Eq v, PPrint v) =>
TCEmb TyCon
-> SEnv SortedReft
-> (v, LocSpecType, [Located Expr])
-> Diagnostics
checkTerminationExpr TCEmb TyCon
emb SEnv SortedReft
env (v
v, Loc SourcePos
l SourcePos
_ RType RTyCon RTyVar RReft
st, [Located Expr]
les)
            = Doc -> Maybe (Expr, Doc) -> Diagnostics
mkError Doc
"ill-sorted" ([Located Expr] -> Maybe (Expr, Doc)
go [Located Expr]
les) forall a. Semigroup a => a -> a -> a
<> Doc -> Maybe (Expr, Doc) -> Diagnostics
mkError Doc
"non-numeric" ([Located Expr] -> Maybe (Expr, Doc)
go' [Located Expr]
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 forall a. Monoid a => a
mempty [(\ (Expr
e, Doc
d) -> forall t. SrcSpan -> Doc -> Doc -> Expr -> t -> Doc -> TError t
ErrTermSpec (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l) (forall a. PPrint a => a -> Doc
pprint v
v) Doc
k Expr
e RType RTyCon RTyVar RReft
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 :: [F.Located F.Expr] -> Maybe (F.Expr, Doc)
    go :: [Located Expr] -> Maybe (Expr, Doc)
go      = 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 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall a. Located a -> a
val Located Expr
e,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc
checkSorted (forall a. Loc a => a -> SrcSpan
F.srcSpan Located Expr
e) SEnv Sort
env' (forall a. Located a -> a
val Located Expr
e))     forall a. Maybe a
Nothing

    go' :: [F.Located F.Expr] -> Maybe (F.Expr, Doc)
    go' :: [Located Expr] -> Maybe (Expr, Doc)
go'     = 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 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall a. Located a -> a
val Located Expr
e,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc
checkSorted (forall a. Loc a => a -> SrcSpan
F.srcSpan Located Expr
e) SEnv Sort
env' (Located Expr -> Expr
cmpZero Located Expr
e)) forall a. Maybe a
Nothing

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

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

    rSort :: RType RTyCon RTyVar RReft -> SortedReft
rSort   = forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb
    cmpZero :: Located Expr -> Expr
cmpZero Located Expr
e = Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Le (forall a. Expression a => a -> Expr
F.expr (Int
0 :: Int)) (forall a. Located a -> a
val Located Expr
e)

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

checkDupIntersect     :: [(Var, LocSpecType)] -> [(Var, LocSpecType)] -> Diagnostics
checkDupIntersect :: [(Var, LocSpecType)] -> [(Var, LocSpecType)] -> Diagnostics
checkDupIntersect [(Var, LocSpecType)]
xts [(Var, LocSpecType)]
asmSigs =
  [Warning] -> [Error] -> Diagnostics
mkDiagnostics (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. Show a => (a, Located a) -> Warning
mkWrn {- trace msg -} [(Var, LocSpecType)]
dups) 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 forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc Located a
t) (forall {a}. Show a => a -> Doc
pprWrn a
x)
    dups :: [(Var, LocSpecType)]
dups           = forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
L.intersectBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) [(Var, LocSpecType)]
asmSigs [(Var, LocSpecType)]
xts
    pprWrn :: a -> Doc
pprWrn a
v       = String -> Doc
text forall a b. (a -> b) -> a -> b
$ String
"Assume Overwrites Specifications for " forall a. [a] -> [a] -> [a]
++ 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, LocSpecType)] -> Diagnostics
checkDuplicate = [Warning] -> [Error] -> Diagnostics
mkDiagnostics forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a t.
(PPrint a, Eq a, Hashable a) =>
(t -> a) -> (t -> SrcSpan) -> [t] -> [Error]
checkUnique' forall a b. (a, b) -> a
fst (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)

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

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


checkMismatch        :: (Var, LocSpecType) -> Diagnostics
checkMismatch :: (Var, LocSpecType) -> Diagnostics
checkMismatch (Var
x, LocSpecType
t) = if Bool
ok then Diagnostics
emptyDiagnostics else [Warning] -> [Error] -> Diagnostics
mkDiagnostics forall a. Monoid a => a
mempty [Error
err]
  where
    ok :: Bool
ok               = forall r. Var -> RType RTyCon RTyVar r -> Bool
tyCompat Var
x (forall a. Located a -> a
val LocSpecType
t)
    err :: Error
err              = Var -> LocSpecType -> Error
errTypeMismatch Var
x LocSpecType
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         = RSort
lqT forall a. Eq a => a -> a -> Bool
== RSort
hsT
  where
    RSort
lqT :: RSort     = forall c tv r. RType c tv r -> RType c tv ()
toRSort RType RTyCon RTyVar r
t
    RSort
hsT :: RSort     = forall r. Monoid r => Type -> RRType r
ofType (Var -> Type
varType Var
x)
    _msg :: String
_msg             = String
"TY-COMPAT: " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> String
GM.showPpr Var
x forall a. [a] -> [a] -> [a]
++ String
": hs = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp RSort
hsT forall a. [a] -> [a] -> [a]
++ String
" :lq = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp RSort
lqT

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

------------------------------------------------------------------------------------------------
-- | @checkRType@ determines if a type is malformed in a given environment ---------------------
------------------------------------------------------------------------------------------------
checkRType :: Bool -> BScope -> F.TCEmb TyCon -> F.SEnv F.SortedReft -> LocSpecType -> Maybe Doc
------------------------------------------------------------------------------------------------
checkRType :: Bool
-> Bool
-> TCEmb TyCon
-> SEnv SortedReft
-> LocSpecType
-> Maybe Doc
checkRType Bool
allowHO Bool
bsc TCEmb TyCon
emb SEnv SortedReft
senv LocSpecType
lt
  =   forall t t1. RType RTyCon t t1 -> Maybe Doc
checkAppTys RType RTyCon RTyVar RReft
st
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall t.
(PPrint t, Reftable t, SubsTy RTyVar RSort t,
 Reftable (RTProp RTyCon RTyVar (UReft t))) =>
RType RTyCon RTyVar (UReft t) -> Maybe Doc
checkAbstractRefs RType RTyCon RTyVar RReft
st
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall r c tv a b.
(Reftable r, TyConable c) =>
(Symbol -> RType c tv r -> Bool)
-> Bool
-> (c -> [RType c tv r] -> [(Symbol, a)])
-> (RTVar tv (RType c tv ()) -> [(Symbol, a)])
-> (RType c tv r -> a)
-> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b)
-> (PVar (RType c tv ()) -> SEnv a -> SEnv a)
-> SEnv a
-> b
-> RType c tv r
-> b
efoldReft forall {p} {t} {t1} {t2}. p -> RType t t1 t2 -> Bool
farg Bool
bsc RTyCon -> [RType RTyCon RTyVar RReft] -> [(Symbol, SortedReft)]
cb (TCEmb TyCon -> RTVar RTyVar RSort -> [(Symbol, SortedReft)]
tyToBind TCEmb TyCon
emb) (forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb) forall {r}.
(PPrint r, SubsTy RTyVar RSort r, Reftable r,
 Reftable (RTProp RTyCon RTyVar (UReft r))) =>
SEnv SortedReft
-> Maybe (RRType (UReft r)) -> UReft r -> Maybe Doc -> Maybe Doc
f PVar RSort -> SEnv SortedReft -> SEnv SortedReft
insertPEnv SEnv SortedReft
senv forall a. Maybe a
Nothing RType RTyCon RTyVar RReft
st
  where
    -- isErasable         = if allowTC then isEmbeddedDict else isClass
    st :: RType RTyCon RTyVar RReft
st                 = forall a. Located a -> a
val LocSpecType
lt
    cb :: RTyCon -> [RType RTyCon RTyVar RReft] -> [(Symbol, SortedReft)]
cb RTyCon
c [RType RTyCon RTyVar RReft]
ts            = TCEmb TyCon -> RType RTyCon RTyVar RReft -> [(Symbol, SortedReft)]
classBinds TCEmb TyCon
emb (forall r c tv. Monoid r => c -> [RType c tv r] -> RType c tv r
rRCls RTyCon
c [RType RTyCon RTyVar RReft]
ts)
    farg :: p -> RType t t1 t2 -> Bool
farg p
_ RType t t1 t2
t           = Bool
allowHO Bool -> Bool -> Bool
|| forall t t1 t2. RType t t1 t2 -> Bool
isBase RType t t1 t2
t  -- NOTE: this check should be the same as the one in addCGEnv
    f :: SEnv SortedReft
-> Maybe (RRType (UReft r)) -> UReft r -> Maybe Doc -> Maybe Doc
f SEnv SortedReft
env Maybe (RRType (UReft r))
me UReft r
r Maybe Doc
err     = Maybe Doc
err forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar (UReft r))) =>
SrcSpan
-> SEnv SortedReft
-> TCEmb TyCon
-> Maybe (RRType (UReft r))
-> UReft r
-> Maybe Doc
checkReft (forall a. Loc a => a -> SrcSpan
F.srcSpan LocSpecType
lt) SEnv SortedReft
env TCEmb TyCon
emb Maybe (RRType (UReft r))
me UReft r
r
    insertPEnv :: PVar RSort -> SEnv SortedReft -> SEnv SortedReft
insertPEnv PVar RSort
p SEnv SortedReft
γ     = forall a. SEnv a -> [(Symbol, a)] -> SEnv a
insertsSEnv SEnv SortedReft
γ (forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd (forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVar RSort -> [(Symbol, RSort)]
pbinds PVar RSort
p)
    pbinds :: PVar RSort -> [(Symbol, RSort)]
pbinds PVar RSort
p           = (forall t. PVar t -> Symbol
pname PVar RSort
p, forall r. (PPrint r, Reftable r) => PVar RSort -> RRType r
pvarRType PVar RSort
p :: RSort) forall a. a -> [a] -> [a]
: [(Symbol
x, RSort
tx) | (RSort
tx, Symbol
x, Expr
_) <- forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar RSort
p]

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

checkAppTys :: RType RTyCon t t1 -> Maybe Doc
checkAppTys :: forall t t1. RType RTyCon t t1 -> Maybe Doc
checkAppTys = forall t t1. RType RTyCon t t1 -> Maybe Doc
go
  where
    go :: RType RTyCon tv r -> Maybe Doc
go (RAllT RTVU RTyCon tv
_ RType RTyCon tv r
t r
_)    = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t
    go (RAllP PVU RTyCon tv
_ RType RTyCon tv r
t)      = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t
    go (RApp RTyCon
rtc [RType RTyCon tv r]
ts [RTProp RTyCon tv r]
_ r
_)
      = RTyCon -> Int -> Maybe Doc
checkTcArity RTyCon
rtc (forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon tv r]
ts) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
        forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\Maybe Doc
merr RType RTyCon tv r
t -> Maybe Doc
merr forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t) forall a. Maybe a
Nothing [RType RTyCon tv r]
ts
    go (RFun Symbol
_ RFInfo
_ RType RTyCon tv r
t1 RType RTyCon tv r
t2 r
_) = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t1 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t2
    go (RVar tv
_ r
_)       = forall a. Maybe a
Nothing
    go (RAllE Symbol
_ RType RTyCon tv r
t1 RType RTyCon tv r
t2)  = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t1 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t2
    go (REx Symbol
_ RType RTyCon tv r
t1 RType RTyCon tv r
t2)    = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t1 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t2
    go (RAppTy RType RTyCon tv r
t1 RType RTyCon tv r
t2 r
_) = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t1 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t2
    go (RRTy [(Symbol, RType RTyCon tv r)]
_ r
_ Oblig
_ RType RTyCon tv r
t)   = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t
    go (RExprArg Located Expr
_)     = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Logical expressions cannot appear inside a Haskell type"
    go (RHole r
_)        = 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 forall a. Ord a => a -> a -> Bool
< Int
givenArity
    = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Type constructor" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint TyCon
tc
        Doc -> Doc -> Doc
<+> String -> Doc
text String
"expects a maximum" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Int
expectedArity
        Doc -> Doc -> Doc
<+> String -> Doc
text String
"arguments but was given" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Int
givenArity
        Doc -> Doc -> Doc
<+> String -> Doc
text String
"arguments"
  | Bool
otherwise
    = forall a. Maybe a
Nothing
  where
    expectedArity :: Int
expectedArity = TyCon -> Int
tyConRealArity TyCon
tc


checkAbstractRefs
  :: (PPrint t, F.Reftable t, SubsTy RTyVar RSort t, F.Reftable (RTProp RTyCon RTyVar (UReft t))) =>
     RType RTyCon RTyVar (UReft t) -> Maybe Doc
checkAbstractRefs :: forall t.
(PPrint t, Reftable t, SubsTy RTyVar RSort t,
 Reftable (RTProp RTyCon RTyVar (UReft t))) =>
RType RTyCon RTyVar (UReft t) -> Maybe Doc
checkAbstractRefs RType RTyCon RTyVar (UReft t)
rt = forall {r}. RType RTyCon RTyVar (UReft r) -> Maybe Doc
go RType RTyCon RTyVar (UReft t)
rt
  where
    penv :: [PVar RSort]
penv = forall {c} {tv} {r}. RType c tv r -> [PVU c tv]
mkPEnv RType RTyCon RTyVar (UReft t)
rt

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

    go' :: RTyCon -> [RTProp RTyCon RTyVar (UReft r)] -> Maybe Doc
go' RTyCon
c [RTProp RTyCon RTyVar (UReft r)]
rs = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\Maybe Doc
acc (RTProp RTyCon RTyVar (UReft r)
x, PVar RSort
y) -> Maybe Doc
acc forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTProp RTyCon RTyVar (UReft r) -> PVar RSort -> Maybe Doc
checkOne' RTProp RTyCon RTyVar (UReft r)
x PVar RSort
y) forall a. Maybe a
Nothing (forall a b. [a] -> [b] -> [(a, b)]
zip [RTProp RTyCon RTyVar (UReft r)]
rs (RTyCon -> [PVar RSort]
rTyConPVs RTyCon
c))

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


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

    check :: RSort -> UReft r -> Maybe Doc
check RSort
s (MkUReft r
_ (Pr [UsedPVar]
ps)) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\Maybe Doc
acc UsedPVar
pp -> Maybe Doc
acc forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {t}. RSort -> PVar t -> Maybe Doc
checkOne RSort
s UsedPVar
pp) forall a. Maybe a
Nothing [UsedPVar]
ps

    checkOne :: RSort -> PVar t -> Maybe Doc
checkOne RSort
s PVar t
p | forall {t}. PVar t -> RSort
pvType' PVar t
p forall a. Eq a => a -> a -> Bool
/= RSort
s
                 = forall a. a -> Maybe a
Just 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
<+> forall a. PPrint a => a -> Doc
pprint (forall {t}. PVar t -> RSort
pvType' PVar t
p)
                       Doc -> Doc -> Doc
<+> String -> Doc
text String
"is applied to"
                       Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint RSort
s
                       Doc -> Doc -> Doc
<+> String -> Doc
text String
"\n\t In" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint PVar t
p
                 | Bool
otherwise
                 = forall a. Maybe a
Nothing

    mkPEnv :: RType c tv r -> [PVU c tv]
mkPEnv (RAllT RTVU c tv
_ RType c tv r
t r
_) = RType c tv r -> [PVU c tv]
mkPEnv RType c tv r
t
    mkPEnv (RAllP PVU c tv
p RType c tv r
t)   = PVU c tv
pforall a. a -> [a] -> [a]
:RType c tv r -> [PVU c tv]
mkPEnv RType c tv r
t
    mkPEnv RType c tv r
_             = []
    pvType' :: PVar t -> RSort
pvType' PVar t
p          = forall a. (?callStack::CallStack) => String -> ListNE a -> a
Misc.safeHead (forall a. PPrint a => a -> String
showpp PVar t
p forall a. [a] -> [a] -> [a]
++ String
" not in env of " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp RType RTyCon RTyVar (UReft t)
rt) [forall t. PVar t -> t
pvType PVar RSort
q | PVar RSort
q <- [PVar RSort]
penv, forall t. PVar t -> Symbol
pname PVar t
p forall a. Eq a => a -> a -> Bool
== forall t. PVar t -> Symbol
pname PVar RSort
q]


checkReft                    :: (PPrint r, F.Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, F.Reftable (RTProp RTyCon RTyVar (UReft r)))
                             => F.SrcSpan -> F.SEnv F.SortedReft -> F.TCEmb TyCon -> Maybe (RRType (UReft r)) -> UReft r -> Maybe Doc
checkReft :: forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar (UReft r))) =>
SrcSpan
-> SEnv SortedReft
-> TCEmb TyCon
-> Maybe (RRType (UReft r))
-> UReft r
-> Maybe Doc
checkReft SrcSpan
_ SEnv SortedReft
_   TCEmb TyCon
_   Maybe (RRType (UReft r))
Nothing UReft r
_   = 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
_ = (\Doc
z -> Doc
dr Doc -> Doc -> Doc
$+$ Doc
z) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> a -> Maybe Doc
checkSortedReftFull SrcSpan
sp SEnv SortedReft
env SortedReft
r
  where
    r :: SortedReft
r                           = forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar 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
<+> 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] -> Diagnostics
---------------------------------------------------------------------------------------------------
checkMeasures :: TCEmb TyCon
-> SEnv SortedReft
-> [Measure (RType RTyCon RTyVar RReft) DataCon]
-> Diagnostics
checkMeasures TCEmb TyCon
emb SEnv SortedReft
env = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (TCEmb TyCon
-> SEnv SortedReft
-> Measure (RType RTyCon RTyVar RReft) DataCon
-> Diagnostics
checkMeasure TCEmb TyCon
emb SEnv SortedReft
env)

checkMeasure :: F.TCEmb TyCon -> F.SEnv F.SortedReft -> Measure SpecType DataCon -> Diagnostics
checkMeasure :: TCEmb TyCon
-> SEnv SortedReft
-> Measure (RType RTyCon RTyVar RReft) DataCon
-> Diagnostics
checkMeasure TCEmb TyCon
emb SEnv SortedReft
γ (M name :: LocSymbol
name@(Loc SourcePos
src SourcePos
_ Symbol
n) RType RTyCon RTyVar RReft
sort [Def (RType RTyCon RTyVar RReft) DataCon]
body MeasureKind
_ [([Symbol], Expr)]
_)
  = [Warning] -> [Error] -> Diagnostics
mkDiagnostics forall a. Monoid a => a
mempty [ forall {t}. Doc -> TError t
txerror Doc
e | Just Doc
e <- forall r t.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
SEnv SortedReft
-> TCEmb TyCon
-> t
-> RType RTyCon RTyVar RReft
-> Def (RRType r) DataCon
-> Maybe Doc
checkMBody SEnv SortedReft
γ TCEmb TyCon
emb LocSymbol
name RType RTyCon RTyVar RReft
sort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Def (RType RTyCon RTyVar RReft) DataCon]
body ]
  where
    txerror :: Doc -> TError t
txerror = forall t. SrcSpan -> Doc -> Doc -> TError t
ErrMeas (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
src) (forall a. PPrint a => a -> Doc
pprint Symbol
n)

checkMBody :: (PPrint r, F.Reftable r,SubsTy RTyVar RSort r, F.Reftable (RTProp RTyCon RTyVar r))
           => F.SEnv F.SortedReft
           -> F.TCEmb TyCon
           -> t
           -> SpecType
           -> Def (RRType r) DataCon
           -> Maybe Doc
checkMBody :: forall r t.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
SEnv SortedReft
-> TCEmb TyCon
-> t
-> RType RTyCon RTyVar RReft
-> Def (RRType r) DataCon
-> Maybe Doc
checkMBody SEnv SortedReft
senv TCEmb TyCon
emb t
_ RType RTyCon RTyVar RReft
sort (Def LocSymbol
m DataCon
c Maybe (RRType r)
_ [(Symbol, Maybe (RRType r))]
bs Body
body) = forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnv SortedReft
-> SrcSpan
-> Body
-> Maybe Doc
checkMBody' TCEmb TyCon
emb RType RTyCon RTyVar RReft
sort SEnv SortedReft
γ' SrcSpan
sp Body
body
  where
    sp :: SrcSpan
sp    = forall a. Loc a => a -> SrcSpan
F.srcSpan LocSymbol
m
    γ' :: SEnv SortedReft
γ'    = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\SEnv SortedReft
γ (Symbol
x, SortedReft
t) -> forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
x SortedReft
t SEnv SortedReft
γ) SEnv SortedReft
senv [(Symbol, SortedReft)]
xts
    xts :: [(Symbol, SortedReft)]
xts   = forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Maybe (RRType r))]
bs) forall a b. (a -> b) -> a -> b
$ forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv (t :: * -> *) r c.
(Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarsMeet [(RTyVar, RSort, RType RTyCon RTyVar RReft)]
su  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            forall a. (a -> Bool) -> [a] -> [a]
filter forall {t} {t1}. RType RTyCon t t1 -> Bool
keep (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep)
    keep :: RType RTyCon t t1 -> Bool
keep | Bool
allowTC = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass
         | Bool
otherwise = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType
    -- YL: extract permitTC information from sort
    allowTC :: Bool
allowTC = forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. a -> Maybe a -> a
fromMaybe Bool
False forall b c a. (b -> c) -> (a -> b) -> a -> c
. RFInfo -> Maybe Bool
permitTC) (forall c tv r. RTypeRep c tv r -> [RFInfo]
ty_info forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType RTyCon RTyVar RReft
sort)
    trep :: RTypeRep RTyCon RTyVar RReft
trep  = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType RTyCon RTyVar RReft
ct
    su :: [(RTyVar, RSort, RType RTyCon RTyVar RReft)]
su    = forall t t2 t1 c tv r.
RType t t2 t1
-> RType c tv r -> [(t2, RType c tv (), RType c tv r)]
checkMBodyUnify (forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
trep) (forall a. [a] -> a
last [RType RTyCon RTyVar RReft]
txs)
    txs :: [RType RTyCon RTyVar RReft]
txs   = forall t0 t1 t2 t3 t4. (t0, t1, t2, t3, t4) -> t2
thd5 forall a b. (a -> b) -> a -> b
$ forall t t1 a.
RType t t1 a
-> ([Symbol], [RFInfo], [RType t t1 a], [a], RType t t1 a)
bkArrowDeep RType RTyCon RTyVar RReft
sort
    ct :: RType RTyCon RTyVar RReft
ct    = forall r. Monoid r => Type -> RRType r
ofType 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 (),RType c tv r)]
checkMBodyUnify :: forall t t2 t1 c tv r.
RType t t2 t1
-> RType c tv r -> [(t2, RType c tv (), RType c tv r)]
checkMBodyUnify = forall t t2 t1 c tv r.
RType t t2 t1
-> RType c tv r -> [(t2, RType c tv (), RType c tv r)]
go
  where
    go :: RType c tv r -> RType c tv r -> [(tv, RType c tv (), RType c tv r)]
go (RVar tv
tv r
_) RType c tv r
t      = [(tv
tv, forall c tv r. RType c tv r -> RType c tv ()
toRSort RType c tv r
t, RType c tv r
t)]
    go t :: RType c tv r
t@RApp{} t' :: RType c tv r
t'@RApp{} = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith RType c tv r -> RType c tv r -> [(tv, RType c tv (), RType c tv r)]
go (forall c tv r. RType c tv r -> [RType c tv r]
rt_args RType c tv r
t) (forall c tv r. RType c tv r -> [RType c tv r]
rt_args RType c tv r
t')
    go RType c tv r
_ RType c tv r
_                = []

checkMBody' :: (PPrint r, F.Reftable r,SubsTy RTyVar RSort r, F.Reftable (RTProp RTyCon RTyVar r))
            => F.TCEmb TyCon
            -> RType RTyCon RTyVar r
            -> F.SEnv F.SortedReft
            -> F.SrcSpan
            -> Body
            -> Maybe Doc
checkMBody' :: forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnv SortedReft
-> SrcSpan
-> Body
-> Maybe Doc
checkMBody' TCEmb TyCon
emb RType RTyCon RTyVar r
sort SEnv SortedReft
γ SrcSpan
sp Body
body = case Body
body of
    E Expr
e   -> forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc
checkSortFull SrcSpan
sp SEnv SortedReft
γ (forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
emb RType RTyCon RTyVar r
sort') Expr
e
    P Expr
p   -> forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc
checkSortFull SrcSpan
sp SEnv SortedReft
γ Sort
F.boolSort  Expr
p
    R Symbol
s Expr
p -> forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc
checkSortFull SrcSpan
sp (forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
s SortedReft
sty SEnv SortedReft
γ) Sort
F.boolSort Expr
p
  where
    sty :: SortedReft
sty   = forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb RType RTyCon RTyVar r
sort'
    sort' :: RType RTyCon RTyVar r
sort' = 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 = forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep forall a b. (a -> b) -> a -> b
$ RTypeRep RTyCon RTyVar r
trep {ty_binds :: [Symbol]
ty_binds = [Symbol]
xs, ty_info :: [RFInfo]
ty_info = [RFInfo]
is, ty_args :: [RType RTyCon RTyVar r]
ty_args = [RType RTyCon RTyVar r]
ts, ty_refts :: [r]
ty_refts = [r]
rs}
  where
    xs :: [Symbol]
xs   = forall a. Int -> [a] -> [a]
drop Int
i forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar r
trep
    ts :: [RType RTyCon RTyVar r]
ts   = forall a. Int -> [a] -> [a]
drop Int
i forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep RTyCon RTyVar r
trep
    rs :: [r]
rs   = forall a. Int -> [a] -> [a]
drop Int
i forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> [r]
ty_refts RTypeRep RTyCon RTyVar r
trep
    is :: [RFInfo]
is   = forall a. Int -> [a] -> [a]
drop Int
i forall a b. (a -> b) -> a -> b
$ forall c tv r. RTypeRep c tv r -> [RFInfo]
ty_info RTypeRep RTyCon RTyVar r
trep
    trep :: RTypeRep RTyCon RTyVar r
trep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType RTyCon RTyVar r
t


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


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

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

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


checkClassMeasures :: [Measure SpecType DataCon] -> Diagnostics
checkClassMeasures :: [Measure (RType RTyCon RTyVar RReft) DataCon] -> Diagnostics
checkClassMeasures [Measure (RType RTyCon RTyVar RReft) DataCon]
measures = [Warning] -> [Error] -> Diagnostics
mkDiagnostics forall a. Monoid a => a
mempty (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {ty} {t}. [Measure ty DataCon] -> Maybe (TError t)
checkOne [[Measure (RType RTyCon RTyVar RReft) DataCon]]
byTyCon)
  where
  byName :: [[Measure (RType RTyCon RTyVar RReft) DataCon]]
byName = forall a. (a -> a -> Bool) -> [a] -> [[a]]
L.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (forall a. Located a -> a
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty ctor. Measure ty ctor -> LocSymbol
msName)) [Measure (RType RTyCon RTyVar RReft) DataCon]
measures

  byTyCon :: [[Measure (RType RTyCon RTyVar RReft) DataCon]]
byTyCon = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a. (a -> a -> Bool) -> [a] -> [[a]]
L.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (DataCon -> TyCon
dataConTyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty ctor. Def ty ctor -> ctor
ctor forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns)))
                      [[Measure (RType RTyCon RTyVar RReft) DataCon]]
byName

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