{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE TupleSections       #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# OPTIONS_GHC -Wno-x-partial #-}

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


import           Language.Haskell.Liquid.Constraint.ToFixpoint

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

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


----------------------------------------------------------------------------------------------
-- | 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 Diagnostics -> Diagnostics -> Bool
forall a. Eq a => a -> a -> Bool
== Diagnostics
emptyDiagnostics
  = () -> Either Diagnostics ()
forall a b. b -> Either a b
Right ()
  | Bool
otherwise
  = Diagnostics -> Either Diagnostics ()
forall a b. a -> Either a b
Left Diagnostics
nopositives
  where nopositives :: Diagnostics
nopositives = [TyCon] -> Diagnostics
checkPositives (TargetSrc -> [TyCon]
gsTcs TargetSrc
spec)


checkPositives :: [TyCon] -> Diagnostics
checkPositives :: [TyCon] -> Diagnostics
checkPositives [TyCon]
tys = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [] ([Error] -> Diagnostics) -> [Error] -> Diagnostics
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 = [ SrcSpan -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrPosTyCon (TyCon -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan TyCon
tc) (TyCon -> Doc
forall a. PPrint a => a -> Doc
pprint TyCon
tc) (DataCon -> Doc
forall a. PPrint a => a -> Doc
pprint DataCon
dc Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Type -> Doc
forall a. PPrint a => a -> Doc
pprint (DataCon -> Type
dataConRepType DataCon
dc))
                    | (TyCon
tc, DataCon
dc:[DataCon]
_) <- [(TyCon, [DataCon])]
tcs]

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

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

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

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

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

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

checkDisjoints :: [S.HashSet F.LocSymbol] -> Diagnostics
checkDisjoints :: [HashSet 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 ([HashSet LocSymbol] -> HashSet LocSymbol
forall a. Eq a => [HashSet a] -> HashSet a
S.unions [HashSet LocSymbol]
ss) Diagnostics -> Diagnostics -> Diagnostics
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" (HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList HashSet LocSymbol
s1 [LocSymbol] -> [LocSymbol] -> [LocSymbol]
forall a. [a] -> [a] -> [a]
++ HashSet LocSymbol -> [LocSymbol]
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 Diagnostics -> Diagnostics -> Bool
forall a. Eq a => a -> a -> Bool
== Diagnostics
emptyDiagnostics = () -> Either Diagnostics ()
forall a b. b -> Either a b
Right ()
  | Bool
otherwise                       = Diagnostics -> Either Diagnostics ()
forall a b. a -> Either a b
Left Diagnostics
diagnostics
  where
    diagnostics      :: Diagnostics
    diagnostics :: Diagnostics
diagnostics      =  Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Symbol, LocSpecType) -> Reader ElabFlags Diagnostics)
-> [(Symbol, LocSpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Symbol, LocSpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Reader ElabFlags 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))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Bool -> Diagnostics -> Diagnostics
forall m. Monoid m => Bool -> m -> m
condNull Bool
noPrune
                        (Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Var, LocSpecType) -> Reader ElabFlags Diagnostics)
-> [(Var, LocSpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, LocSpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Reader ElabFlags Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"constructor"  TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) ([(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall {f :: * -> *} {f :: * -> *} {f :: * -> *} {b} {a}.
(Functor f, Functor f, Functor f, HasTemplates b) =>
[(a, f (f (f b)))] -> [(a, f (f (f b)))]
txCtors ([(Var, LocSpecType)] -> [(Var, LocSpecType)])
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ GhcSpecData -> [(Var, LocSpecType)]
gsCtors      (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp))) ElabFlags
ef)
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Var, LocSpecType) -> Reader ElabFlags Diagnostics)
-> [(Var, LocSpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, LocSpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Reader ElabFlags 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))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Var, LocSpecType) -> Reader ElabFlags Diagnostics)
-> [(Var, LocSpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, LocSpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Reader ElabFlags Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"reflect"      TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env ((Var, LocSpecType) -> Reader ElabFlags Diagnostics)
-> ((Var, LocSpecType) -> (Var, LocSpecType))
-> (Var, LocSpecType)
-> Reader ElabFlags Diagnostics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\sig :: (Var, LocSpecType)
sig@(Var
_,LocSpecType
s) -> String -> (Var, LocSpecType) -> (Var, LocSpecType)
forall a. PPrint a => String -> a -> a
F.notracepp ([RFInfo] -> String
forall a. Show a => a -> String
show (RTypeRepV Symbol RTyCon RTyVar RReft -> [RFInfo]
forall v c tv r. RTypeRepV v c tv r -> [RFInfo]
ty_info (SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep (LocSpecType -> SpecType
forall a. Located a -> a
F.val LocSpecType
s)))) (Var, LocSpecType)
sig)) (GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (Bool
-> Bool
-> [CoreBind]
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> GhcSpecSig
-> Reader ElabFlags Diagnostics
checkTySigs Bool
allowHO Bool
bsc [CoreBind]
cbs            TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env                (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp)) ElabFlags
ef
                     -- ++ mapMaybe (checkTerminationExpr             emb       env) (gsTexprs     (gsSig  sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Var, LocSpecType) -> Reader ElabFlags Diagnostics)
-> [(Var, LocSpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, LocSpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Reader ElabFlags 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))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (((Maybe Var, LocSpecType) -> Reader ElabFlags Diagnostics)
-> [(Maybe Var, LocSpecType)] -> Reader ElabFlags Diagnostics
forall b (m :: * -> *) (f :: * -> *) a.
(Monoid b, Monad m, Foldable f) =>
(a -> m b) -> f a -> m b
foldMapM (Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Maybe Var, LocSpecType)
-> Reader ElabFlags Diagnostics
checkInv Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env)                 (GhcSpecData -> [(Maybe Var, LocSpecType)]
gsInvariants (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> [(LocSpecType, LocSpecType)]
-> Reader ElabFlags Diagnostics
checkIAl Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env                            (GhcSpecData -> [(LocSpecType, LocSpecType)]
gsIaliases   (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (TCEmb TyCon
-> SEnv SortedReft
-> [MeasureV Symbol SpecType DataCon]
-> Reader ElabFlags Diagnostics
checkMeasures TCEmb TyCon
emb SEnv SortedReft
env [MeasureV Symbol SpecType DataCon]
ms) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> [MeasureV Symbol SpecType DataCon] -> Diagnostics
checkClassMeasures                                        [MeasureV Symbol SpecType DataCon]
ms
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Maybe [ClsInst] -> [Var] -> [(Var, 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
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> ((Var, LocSpecType) -> Diagnostics)
-> [(Var, LocSpecType)] -> Diagnostics
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Var, LocSpecType) -> Diagnostics
checkMismatch (((Var, LocSpecType) -> Bool)
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. (a -> Bool) -> [a] -> [a]
L.filter (\(Var
v,LocSpecType
_) -> Bool -> Bool
not (Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isSCSel Var
v Bool -> Bool -> Bool
|| Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isMethod Var
v)) [(Var, LocSpecType)]
sigs)
                     Diagnostics -> Diagnostics -> Diagnostics
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))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> [(Var, LocSpecType)] -> Diagnostics
checkDuplicate                                            (GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs    (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp))
                     Diagnostics -> Diagnostics -> Diagnostics
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))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> String
-> SEnv SortedReft
-> [Located (RTAlias Symbol BareType)]
-> Diagnostics
forall t s a. String -> t -> [Located (RTAlias s a)] -> Diagnostics
checkRTAliases String
"Type Alias" SEnv SortedReft
env            [Located (RTAlias Symbol BareType)]
tAliases
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> String
-> SEnv SortedReft
-> [Located (RTAlias Symbol Expr)]
-> Diagnostics
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
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (TCEmb TyCon
-> SEnv SortedReft -> [TyConP] -> Reader ElabFlags Diagnostics
checkSizeFun TCEmb TyCon
emb SEnv SortedReft
env                                      (GhcSpecNames -> [TyConP]
gsTconsP (TargetSpec -> GhcSpecNames
gsName TargetSpec
tsp))) ElabFlags
ef
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> [(Symbol, LocSpecType)] -> Diagnostics
forall v. PPrint v => [(v, LocSpecType)] -> Diagnostics
checkPlugged ([Maybe (Symbol, LocSpecType)] -> [(Symbol, LocSpecType)]
forall a. [Maybe a] -> [a]
catMaybes [ (LocSpecType -> (Symbol, LocSpecType))
-> Maybe LocSpecType -> Maybe (Symbol, LocSpecType)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Symbol -> Symbol
F.dropSym Int
2 (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Var -> Symbol
forall t. NamedThing t => t -> Symbol
GM.simplesymbol Var
x,) (MethodType LocSpecType -> Maybe LocSpecType
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) ])
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> TargetSpec -> Diagnostics
checkRewrites TargetSpec
tsp
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> if Config -> Bool
allowUnsafeConstructors (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ TargetSpec -> Config
forall t. HasConfig t => t -> Config
getConfig TargetSpec
tsp
                          then Diagnostics
forall a. Monoid a => a
mempty
                          else [(Var, LocSpecType)] -> Diagnostics
checkConstructorRefinement (GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs (GhcSpecSig -> [(Var, LocSpecType)])
-> GhcSpecSig -> [(Var, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp)

    _rClasses :: [RClass (Located BareType)]
_rClasses         = (BareSpec -> [RClass (Located BareType)])
-> [BareSpec] -> [RClass (Located BareType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap BareSpec -> [RClass (Located BareType)]
forall lname ty. Spec lname ty -> [RClass (Located ty)]
Ms.classes [BareSpec]
specs
    _rInsts :: [RInstance (Located BareType)]
_rInsts           = (BareSpec -> [RInstance (Located BareType)])
-> [BareSpec] -> [RInstance (Located BareType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap BareSpec -> [RInstance (Located BareType)]
forall lname ty. Spec lname ty -> [RInstance (Located ty)]
Ms.rinstance [BareSpec]
specs
    tAliases :: [Located (RTAlias Symbol BareType)]
tAliases          = [[Located (RTAlias Symbol BareType)]]
-> [Located (RTAlias Symbol BareType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [BareSpec -> [Located (RTAlias Symbol BareType)]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
Ms.aliases BareSpec
sp  | BareSpec
sp <- [BareSpec]
specs]
    eAliases :: [Located (RTAlias Symbol Expr)]
eAliases          = [[Located (RTAlias Symbol Expr)]]
-> [Located (RTAlias Symbol Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [BareSpec -> [Located (RTAlias Symbol Expr)]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
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 :: [MeasureV Symbol SpecType DataCon]
ms               = GhcSpecData -> [MeasureV Symbol SpecType 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, Maybe Class -> Bool
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) [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
tsp) [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecData -> [(Var, LocSpecType)]
gsCtors (TargetSpec -> GhcSpecData
gsData TargetSpec
tsp)
    -- allowTC          = typeclass (getConfig sp)
    allowHO :: Bool
allowHO          = TargetSpec -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag TargetSpec
tsp
    bsc :: Bool
bsc              = Config -> Bool
bscope (TargetSpec -> Config
forall t. HasConfig t => t -> Config
getConfig TargetSpec
tsp)
    noPrune :: Bool
noPrune          = Bool -> Bool
not (TargetSpec -> Bool
forall t. HasConfig t => t -> Bool
pruneFlag TargetSpec
tsp)
    txCtors :: [(a, f (f (f b)))] -> [(a, f (f (f b)))]
txCtors [(a, f (f (f b)))]
ts       = [(a
v, (f (f b) -> f (f b)) -> f (f (f b)) -> f (f (f b))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f b -> f b) -> f (f b) -> f (f b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> b) -> f b -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Templates -> b -> b
forall a. HasTemplates a => Templates -> a -> a
F.filterUnMatched Templates
temps))) f (f (f b))
t) | (a
v, f (f (f b))
t) <- [(a, f (f (f b)))]
ts]
    temps :: Templates
temps            = [([Symbol], Expr)] -> Templates
F.makeTemplates ([([Symbol], Expr)] -> Templates)
-> [([Symbol], Expr)] -> Templates
forall a b. (a -> b) -> a -> b
$ GhcSpecData -> [([Symbol], Expr)]
gsUnsorted (GhcSpecData -> [([Symbol], Expr)])
-> GhcSpecData -> [([Symbol], Expr)]
forall a b. (a -> b) -> a -> b
$ TargetSpec -> GhcSpecData
gsData TargetSpec
tsp
    ef :: ElabFlags
ef               = ElabFlags
-> (SMTSolver -> ElabFlags) -> Maybe SMTSolver -> ElabFlags
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> ElabFlags
ElabFlags Bool
False) SMTSolver -> ElabFlags
solverFlags (Maybe SMTSolver -> ElabFlags) -> Maybe SMTSolver -> ElabFlags
forall a b. (a -> b) -> a -> b
$ Config -> Maybe SMTSolver
smtsolver (Config -> Maybe SMTSolver) -> Config -> Maybe SMTSolver
forall a b. (a -> b) -> a -> b
$ TargetSpec -> Config
forall t. HasConfig t => t -> Config
getConfig TargetSpec
tsp
    -- env'             = L.foldl' (\e (x, s) -> insertSEnv x (RR s mempty) e) env wiredSortedSyms



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

    getRetTyRef :: RTypeV v c tv (UReftV v t) -> t
getRetTyRef (RFun Symbol
_ RFInfo
_ RTypeV v c tv (UReftV v t)
_ RTypeV v c tv (UReftV v t)
t UReftV v t
_) = RTypeV v c tv (UReftV v t) -> t
getRetTyRef RTypeV v c tv (UReftV v t)
t
    getRetTyRef (RAllT RTVUV v c tv
_ RTypeV v c tv (UReftV v t)
t UReftV v t
_)    = RTypeV v c tv (UReftV v t) -> t
getRetTyRef RTypeV v c tv (UReftV v t)
t
    getRetTyRef RTypeV v c tv (UReftV v t)
t                = UReftV v t -> t
forall v r. UReftV v r -> r
ur_reft (UReftV v t -> t) -> UReftV v t -> t
forall a b. (a -> b) -> a -> b
$ RTypeV v c tv (UReftV v t) -> UReftV v t
forall v c tv r. RTypeV v c tv r -> r
rt_reft RTypeV v c tv (UReftV v t)
t

    -- True refinement
    validRef :: ReftV Symbol -> Bool
validRef (F.Reft (Symbol
_, Expr
F.PTrue))
                      = Bool
True
    -- Prop foo from ProofCombinators
    validRef (F.Reft (Symbol
v, F.PAtom Brel
F.Eq (F.EApp (F.EVar Symbol
n) (F.EVar Symbol
v')) Expr
_))
      | Symbol
n Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"Language.Haskell.Liquid.ProofCombinators.prop"
      , Symbol
v Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
v'
      = Bool
True
    validRef ReftV Symbol
_ = Bool
False

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


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


--------------------------------------------------------------------------------
checkTySigs :: Bool
            -> BScope
            -> [CoreBind]
            -> F.TCEmb TyCon
            -> Bare.TyConMap
            -> F.SEnv F.SortedReft
            -> GhcSpecSig
            -> ElabM Diagnostics
--------------------------------------------------------------------------------
checkTySigs :: Bool
-> Bool
-> [CoreBind]
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> GhcSpecSig
-> Reader ElabFlags Diagnostics
checkTySigs Bool
allowHO Bool
bsc [CoreBind]
cbs TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
senv GhcSpecSig
sig =
  do ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     pure $ mconcat (runReader (traverse (check senv) topTs) ef)
                   -- = concatMap (check env) topTs
                   -- (mapMaybe   (checkT env) [ (x, t)     | (x, (t, _)) <- topTs])
                   -- ++ (mapMaybe   (checkE env) [ (x, t, es) | (x, (t, Just es)) <- topTs])
                     <> coreVisitor (checkVisitor ef) senv emptyDiagnostics cbs
                   -- ++ coreVisitor checkVisitor env [] cbs
  where
    check :: F.SEnv F.SortedReft -> (Var, (LocSpecType, Maybe [Located F.Expr])) -> ElabM Diagnostics
    check :: SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr]))
-> Reader ElabFlags Diagnostics
check          = Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr]))
-> Reader ElabFlags Diagnostics
checkSigTExpr Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv
    locTm :: HashMap Var (LocSpecType, Maybe [Located Expr])
locTm          = [(Var, (LocSpecType, Maybe [Located Expr]))]
-> HashMap Var (LocSpecType, Maybe [Located Expr])
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) = [(Var, (LocSpecType, Maybe [Located Expr]))]
-> ([(Var, (LocSpecType, Maybe [Located Expr]))],
    [(Var, (LocSpecType, Maybe [Located Expr]))])
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 = Var -> HashMap Var [Located Expr] -> Maybe [Located Expr]
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         = [(Var, [Located Expr])] -> HashMap Var [Located Expr]
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  :: ElabFlags -> CoreVisitor (F.SEnv F.SortedReft) Diagnostics
    checkVisitor :: ElabFlags -> CoreVisitor (SEnv SortedReft) Diagnostics
checkVisitor ElabFlags
ef = CoreVisitor
                       { envF :: SEnv SortedReft -> Var -> SEnv SortedReft
envF  = \SEnv SortedReft
env Var
v     -> Symbol -> SortedReft -> SEnv SortedReft -> SEnv SortedReft
forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
v) (Var -> SortedReft
vSort Var
v) SEnv SortedReft
env
                       , bindF :: SEnv SortedReft -> Diagnostics -> Var -> Diagnostics
bindF = \SEnv SortedReft
env Diagnostics
acc Var
v -> Reader ElabFlags Diagnostics -> ElabFlags -> Diagnostics
forall r a. Reader r a -> r -> a
runReader (SEnv SortedReft -> Var -> Reader ElabFlags Diagnostics
errs SEnv SortedReft
env Var
v) ElabFlags
ef Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Diagnostics
acc
                       , exprF :: SEnv SortedReft -> Diagnostics -> CoreExpr -> Diagnostics
exprF = \SEnv SortedReft
_   Diagnostics
acc CoreExpr
_ -> Diagnostics
acc
                       }
    vSort :: Var -> SortedReft
vSort            = TCEmb TyCon -> Var -> SortedReft
Bare.varSortedReft TCEmb TyCon
emb
    errs :: F.SEnv F.SortedReft -> Var -> ElabM Diagnostics
    errs :: SEnv SortedReft -> Var -> Reader ElabFlags Diagnostics
errs SEnv SortedReft
env Var
v       = case Var
-> HashMap Var (LocSpecType, Maybe [Located Expr])
-> Maybe (LocSpecType, Maybe [Located Expr])
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 -> Reader ElabFlags Diagnostics
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Diagnostics
emptyDiagnostics
                         Just (LocSpecType, Maybe [Located Expr])
t  -> SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr]))
-> Reader ElabFlags 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]))
              -> ElabM Diagnostics
checkSigTExpr :: Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr]))
-> Reader ElabFlags Diagnostics
checkSigTExpr Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (Var
x, (LocSpecType
t, Maybe [Located Expr]
es)) =
  do ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     pure $ runReader mbErr1 ef <> runReader mbErr2 ef
   where
    mbErr1 :: Reader ElabFlags Diagnostics
mbErr1 = Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, LocSpecType)
-> Reader ElabFlags Diagnostics
forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Reader ElabFlags Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
empty TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (Var
x, LocSpecType
t)
    mbErr2 :: Reader ElabFlags Diagnostics
mbErr2 = Reader ElabFlags Diagnostics
-> ([Located Expr] -> Reader ElabFlags Diagnostics)
-> Maybe [Located Expr]
-> Reader ElabFlags Diagnostics
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Diagnostics -> Reader ElabFlags Diagnostics
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Diagnostics
emptyDiagnostics) (TCEmb TyCon
-> SEnv SortedReft
-> (Var, LocSpecType, [Located Expr])
-> Reader ElabFlags Diagnostics
forall v.
(Eq v, PPrint v) =>
TCEmb TyCon
-> SEnv SortedReft
-> (v, LocSpecType, [Located Expr])
-> Reader ElabFlags Diagnostics
checkTerminationExpr TCEmb TyCon
emb SEnv SortedReft
env ((Var, LocSpecType, [Located Expr])
 -> Reader ElabFlags Diagnostics)
-> ([Located Expr] -> (Var, LocSpecType, [Located Expr]))
-> [Located Expr]
-> Reader ElabFlags Diagnostics
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

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

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

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

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

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

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

checkIAlOne :: Bool
            -> BScope
            -> F.TCEmb TyCon
            -> Bare.TyConMap
            -> F.SEnv F.SortedReft
            -> (LocSpecType, LocSpecType)
            -> ElabM Diagnostics
checkIAlOne :: Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (LocSpecType, LocSpecType)
-> Reader ElabFlags Diagnostics
checkIAlOne Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (LocSpecType
t1, LocSpecType
t2) =
  do cs <- (LocSpecType -> Reader ElabFlags Diagnostics)
-> [LocSpecType] -> Reader ElabFlags [Diagnostics]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\LocSpecType
t -> Bool
-> Bool
-> (Doc -> Error)
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> LocSpecType
-> Reader ElabFlags Diagnostics
checkTy Bool
allowHO Bool
bsc (LocSpecType -> Doc -> Error
forall {t}. Located t -> Doc -> TError t
err LocSpecType
t) TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env LocSpecType
t) [LocSpecType
t1, LocSpecType
t2]
     pure $ mconcat $ checkEq : cs
  where
    err :: Located t -> Doc -> TError t
err    Located t
t = SrcSpan -> t -> Doc -> TError t
forall t. SrcSpan -> t -> Doc -> TError t
ErrIAl (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located t -> SourcePos
forall a. Located a -> SourcePos
loc Located t
t) (Located t -> t
forall a. Located a -> a
val Located t
t)
    t1'      :: RSort
    t1' :: RSort
t1'      = SpecType -> RSort
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv ()
toRSort (SpecType -> RSort) -> SpecType -> RSort
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t1
    t2'      :: RSort
    t2' :: RSort
t2'      = SpecType -> RSort
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv ()
toRSort (SpecType -> RSort) -> SpecType -> RSort
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t2
    checkEq :: Diagnostics
checkEq  = if RSort
t1' RSort -> RSort -> Bool
forall a. Eq a => a -> a -> Bool
== RSort
t2' then Diagnostics
emptyDiagnostics else [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [Error
errmis]
    errmis :: Error
errmis   = SrcSpan -> SpecType -> SpecType -> Doc -> Error
forall t. SrcSpan -> t -> t -> Doc -> TError t
ErrIAlMis (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SourcePos
forall a. Located a -> SourcePos
loc LocSpecType
t1) (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t1) (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t2) Doc
emsg
    emsg :: Doc
emsg     = LocSpecType -> Doc
forall a. PPrint a => a -> Doc
pprint LocSpecType
t1 Doc -> Doc -> Doc
<+> String -> Doc
text String
"does not match with" Doc -> Doc -> Doc
<+> LocSpecType -> 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               = String -> [Located (RTAlias s a)] -> Diagnostics
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)
          -> ElabM Diagnostics
checkBind :: forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Reader ElabFlags 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
-> Reader ElabFlags Diagnostics
checkTy Bool
allowHO Bool
bsc Doc -> Error
msg TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env LocSpecType
t
  where
    msg :: Doc -> Error
msg                      = SrcSpan -> Maybe Doc -> Doc -> SpecType -> Doc -> Error
forall t. SrcSpan -> Maybe Doc -> Doc -> t -> Doc -> TError t
ErrTySpec (LocSpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSpecType
t) (Doc -> Maybe Doc
forall a. a -> Maybe a
Just Doc
s) (v -> Doc
forall a. PPrint a => a -> Doc
pprint v
v) (LocSpecType -> SpecType
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])
                     -> ElabM Diagnostics
checkTerminationExpr :: forall v.
(Eq v, PPrint v) =>
TCEmb TyCon
-> SEnv SortedReft
-> (v, LocSpecType, [Located Expr])
-> Reader ElabFlags Diagnostics
checkTerminationExpr TCEmb TyCon
emb SEnv SortedReft
env (v
v, Loc SourcePos
l SourcePos
_ SpecType
st, [Located Expr]
les) =
  do ef <- ReaderT ElabFlags Identity ElabFlags
forall r (m :: * -> *). MonadReader r m => m r
ask
     pure $ mkError "ill-sorted" (go ef les) <> mkError "non-numeric" (go' ef les)
  where
    -- es      = val <$> les
    mkError :: Doc -> Maybe (F.Expr, Doc) -> Diagnostics
    mkError :: Doc -> Maybe (Expr, Doc) -> Diagnostics
mkError Doc
_ Maybe (Expr, Doc)
Nothing = Diagnostics
emptyDiagnostics
    mkError Doc
k (Just (Expr, Doc)
expr') =
      [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [(\ (Expr
e, Doc
d) -> SrcSpan -> Doc -> Doc -> Expr -> SpecType -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> Expr -> t -> Doc -> TError t
ErrTermSpec (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l) (v -> Doc
forall a. PPrint a => a -> Doc
pprint v
v) Doc
k Expr
e SpecType
st Doc
d) (Expr, Doc)
expr']
    -- mkErr   = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "ill-sorted" ) e t d)
    -- mkErr'  = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "non-numeric") e t d)

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

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

    env' :: SEnv Sort
env'    = SortedReft -> Sort
F.sr_sort (SortedReft -> Sort) -> SEnv SortedReft -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SEnv SortedReft -> (Symbol, SortedReft) -> SEnv SortedReft)
-> SEnv SortedReft -> [(Symbol, SortedReft)] -> SEnv SortedReft
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\SEnv SortedReft
e (Symbol
x,SortedReft
s) -> Symbol -> SortedReft -> SEnv SortedReft -> SEnv SortedReft
forall 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     = ((Symbol, SpecType) -> [(Symbol, SortedReft)])
-> [(Symbol, SpecType)] -> [(Symbol, SortedReft)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Symbol, SpecType) -> [(Symbol, SortedReft)]
mkClss ([(Symbol, SpecType)] -> [(Symbol, SortedReft)])
-> [(Symbol, SpecType)] -> [(Symbol, SortedReft)]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTypeRepV Symbol RTyCon RTyVar RReft -> [Symbol]
forall v c tv r. RTypeRepV v c tv r -> [Symbol]
ty_binds RTypeRepV Symbol RTyCon RTyVar RReft
trep) (RTypeRepV Symbol RTyCon RTyVar RReft -> [SpecType]
forall v c tv r. RTypeRepV v c tv r -> [RTypeV v c tv r]
ty_args RTypeRepV Symbol RTyCon RTyVar RReft
trep)
    trep :: RTypeRepV Symbol RTyCon RTyVar RReft
trep    = SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep SpecType
st

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

    rSort :: SpecType -> SortedReft
rSort   = TCEmb TyCon -> SpecType -> SortedReft
forall r.
(PPrint r, 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
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
F.PAtom Brel
F.Le (Int -> Expr
forall a. Expression a => a -> Expr
F.expr (Int
0 :: Int)) (Located Expr -> Expr
forall a. Located a -> a
val Located Expr
e)

checkTy :: Bool
        -> BScope
        -> (Doc -> Error)
        -> F.TCEmb TyCon
        -> Bare.TyConMap
        -> F.SEnv F.SortedReft
        -> LocSpecType
        -> ElabM Diagnostics
checkTy :: Bool
-> Bool
-> (Doc -> Error)
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> LocSpecType
-> Reader ElabFlags Diagnostics
checkTy Bool
allowHO Bool
bsc Doc -> Error
mkE TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env LocSpecType
t =
  do me <- Bool
-> Bool
-> TCEmb TyCon
-> SEnv SortedReft
-> LocSpecType
-> Reader ElabFlags (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)
     pure $ case me of
              Maybe Doc
Nothing -> Diagnostics
emptyDiagnostics
              Just Doc
d  -> [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [Doc -> Error
mkE Doc
d]
  where
    _msg :: String
_msg =  String
"CHECKTY: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. PPrint a => a -> String
showpp (LocSpecType -> SpecType
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 (((Var, LocSpecType) -> Warning)
-> [(Var, LocSpecType)] -> [Warning]
forall a b. (a -> b) -> [a] -> [b]
map (Var, LocSpecType) -> Warning
forall {a} {a}. Show a => (a, Located a) -> Warning
mkWrn {- trace msg -} [(Var, LocSpecType)]
dups) [Error]
forall a. Monoid a => a
mempty
  where
    mkWrn :: (a, Located a) -> Warning
mkWrn (a
x, Located a
t)   = SrcSpan -> Doc -> Warning
mkWarning (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located a -> SourcePos
forall a. Located a -> SourcePos
loc Located a
t) (a -> Doc
forall {a}. Show a => a -> Doc
pprWrn a
x)
    dups :: [(Var, LocSpecType)]
dups           = ((Var, LocSpecType) -> (Var, LocSpecType) -> Bool)
-> [(Var, LocSpecType)]
-> [(Var, LocSpecType)]
-> [(Var, LocSpecType)]
forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
L.intersectBy (Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Var -> Var -> Bool)
-> ((Var, LocSpecType) -> Var)
-> (Var, LocSpecType)
-> (Var, LocSpecType)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst) [(Var, LocSpecType)]
asmSigs [(Var, LocSpecType)]
xts
    pprWrn :: a -> Doc
pprWrn a
v       = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Assume Overwrites Specifications for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v
    -- msg              = "CHECKDUPINTERSECT:" ++ msg1 ++ msg2
    -- msg1             = "\nCheckd-SIGS:\n" ++ showpp (M.fromList xts)
    -- msg2             = "\nAssume-SIGS:\n" ++ showpp (M.fromList asmSigs)


checkDuplicate :: [(Var, LocSpecType)] -> Diagnostics
checkDuplicate :: [(Var, LocSpecType)] -> Diagnostics
checkDuplicate = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty ([Error] -> Diagnostics)
-> ([(Var, LocSpecType)] -> [Error])
-> [(Var, LocSpecType)]
-> Diagnostics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Var, LocSpecType) -> Var)
-> ((Var, LocSpecType) -> SrcSpan)
-> [(Var, LocSpecType)]
-> [Error]
forall a t.
(PPrint a, Eq a, Hashable a) =>
(t -> a) -> (t -> SrcSpan) -> [t] -> [Error]
checkUnique' (Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst (LocSpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (LocSpecType -> SrcSpan)
-> ((Var, LocSpecType) -> LocSpecType)
-> (Var, LocSpecType)
-> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, LocSpecType) -> LocSpecType
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 [Warning]
forall a. Monoid a => a
mempty [SrcSpan -> Doc -> Error
forall t. SrcSpan -> Doc -> TError t
ErrMClass (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SourcePos
forall a. Located a -> SourcePos
loc LocSpecType
t) (Var -> Doc
forall a. PPrint a => a -> Doc
pprint Var
x)| (Var
x,LocSpecType
t) <- [(Var, LocSpecType)]
dups ]
  where
    dups :: [(Var, LocSpecType)]
dups = String -> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. PPrint a => String -> a -> a
F.notracepp String
"DPS" ([(Var, LocSpecType)] -> [(Var, LocSpecType)])
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ ((Var, LocSpecType) -> Bool)
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
ms) (Var -> Bool)
-> ((Var, LocSpecType) -> Var) -> (Var, LocSpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst) [(Var, LocSpecType)]
xts'
    ms :: [Var]
ms   = String -> [Var] -> [Var]
forall a. PPrint a => String -> a -> a
F.notracepp String
"MS"  ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$ (ClsInst -> [Var]) -> [ClsInst] -> [Var]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Class -> [Var]
classMethods (Class -> [Var]) -> (ClsInst -> Class) -> ClsInst -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClsInst -> Class
is_cls) [ClsInst]
clsis
    xts' :: [(Var, LocSpecType)]
xts' = String -> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. PPrint a => String -> a -> a
F.notracepp String
"XTS" ([(Var, LocSpecType)] -> [(Var, LocSpecType)])
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ ((Var, LocSpecType) -> Bool)
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Var, LocSpecType) -> Bool) -> (Var, LocSpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
cls) (Var -> Bool)
-> ((Var, LocSpecType) -> Var) -> (Var, LocSpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst) [(Var, LocSpecType)]
xts
    cls :: [Var]
cls  = String -> [Var] -> [Var]
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 [Warning]
forall a. Monoid a => a
mempty (([Located (RTAlias s a)] -> Error)
-> [[Located (RTAlias s a)]] -> [Error]
forall a b. (a -> b) -> [a] -> [b]
map [Located (RTAlias s a)] -> Error
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)]
_)          = SrcSpan -> Doc -> Doc -> [SrcSpan] -> TError t
forall t. SrcSpan -> Doc -> Doc -> [SrcSpan] -> TError t
ErrDupAlias (Located (RTAlias x a) -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located (RTAlias x a)
x)
                                          (String -> Doc
text String
s)
                                          (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc)
-> (Located (RTAlias x a) -> Symbol)
-> Located (RTAlias x a)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias x a -> Symbol
forall x a. RTAlias x a -> Symbol
rtName (RTAlias x a -> Symbol)
-> (Located (RTAlias x a) -> RTAlias x a)
-> Located (RTAlias x a)
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RTAlias x a) -> RTAlias x a
forall a. Located a -> a
val (Located (RTAlias x a) -> Doc) -> Located (RTAlias x a) -> Doc
forall a b. (a -> b) -> a -> b
$ Located (RTAlias x a)
x)
                                          (Located (RTAlias x a) -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located (RTAlias x a) -> SrcSpan)
-> [Located (RTAlias x a)] -> [SrcSpan]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located (RTAlias x a)]
xs)
    mkError []                = Maybe SrcSpan -> String -> TError t
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"mkError: called on empty list"
    dups :: [[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)]
_) <- (Located (RTAlias s a) -> Symbol)
-> [Located (RTAlias s a)] -> [[Located (RTAlias s a)]]
forall b a. Ord b => (a -> b) -> [a] -> [[a]]
groupDuplicatesOn (RTAlias s a -> Symbol
forall x a. RTAlias x a -> Symbol
rtName (RTAlias s a -> Symbol)
-> (Located (RTAlias s a) -> RTAlias s a)
-> Located (RTAlias s a)
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RTAlias s a) -> RTAlias s a
forall a. Located a -> a
val) [Located (RTAlias s a)]
tas]

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

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

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

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

    insertPEnv :: PVar RSort -> SEnv SortedReft -> SEnv SortedReft
insertPEnv PVar RSort
p SEnv SortedReft
γ     = SEnv SortedReft -> [(Symbol, SortedReft)] -> SEnv SortedReft
forall a. SEnv a -> [(Symbol, a)] -> SEnv a
insertsSEnv SEnv SortedReft
γ ((RSort -> SortedReft) -> (Symbol, RSort) -> (Symbol, SortedReft)
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TCEmb TyCon -> RSort -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb) ((Symbol, RSort) -> (Symbol, SortedReft))
-> [(Symbol, RSort)] -> [(Symbol, SortedReft)]
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           = (PVar RSort -> Symbol
forall v t. PVarV v t -> Symbol
pname PVar RSort
p, PVar RSort -> RSort
forall r. (PPrint r, Reftable r) => PVar RSort -> RRType r
pvarRType PVar RSort
p :: RSort) (Symbol, RSort) -> [(Symbol, RSort)] -> [(Symbol, RSort)]
forall a. a -> [a] -> [a]
: [(Symbol
x, RSort
tx) | (RSort
tx, Symbol
x, Expr
_) <- PVar RSort -> [(RSort, Symbol, Expr)]
forall v t. PVarV v t -> [(t, Symbol, ExprV v)]
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 = RTVInfo RSort -> [(Symbol, SortedReft)]
forall {r}.
(PPrint r, SubsTy RTyVar RSort r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
RTVInfo (RRType r) -> [(Symbol, SortedReft)]
go (RTVInfo RSort -> [(Symbol, SortedReft)])
-> (RTVar RTyVar RSort -> RTVInfo RSort)
-> RTVar RTyVar RSort
-> [(Symbol, SortedReft)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTVar RTyVar RSort -> RTVInfo RSort
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_name :: Symbol
rtv_kind :: RRType r
rtv_is_val :: Bool
rtv_is_pol :: Bool
rtv_is_pol :: forall s. RTVInfo s -> Bool
rtv_is_val :: forall s. RTVInfo s -> Bool
rtv_kind :: forall s. RTVInfo s -> s
rtv_name :: forall s. RTVInfo s -> Symbol
..} = [(Symbol
rtv_name, TCEmb TyCon -> RRType r -> SortedReft
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 = RTypeV Symbol RTyCon t t1 -> Maybe Doc
forall {v} {tv} {r}. RTypeV v RTyCon tv r -> Maybe Doc
go
  where
    go :: RTypeV v RTyCon tv r -> Maybe Doc
go (RAllT RTVUV v RTyCon tv
_ RTypeV v RTyCon tv r
t r
_)    = RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t
    go (RAllP PVUV v RTyCon tv
_ RTypeV v RTyCon tv r
t)      = RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t
    go (RApp RTyCon
rtc [RTypeV v RTyCon tv r]
ts [RTPropV v RTyCon tv r]
_ r
_)
      = RTyCon -> Int -> Maybe Doc
checkTcArity RTyCon
rtc ([RTypeV v RTyCon tv r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTypeV v RTyCon tv r]
ts) Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
        (Maybe Doc -> RTypeV v RTyCon tv r -> Maybe Doc)
-> Maybe Doc -> [RTypeV v RTyCon tv r] -> Maybe Doc
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\Maybe Doc
merr RTypeV v RTyCon tv r
t -> Maybe Doc
merr Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t) Maybe Doc
forall a. Maybe a
Nothing [RTypeV v RTyCon tv r]
ts
    go (RFun Symbol
_ RFInfo
_ RTypeV v RTyCon tv r
t1 RTypeV v RTyCon tv r
t2 r
_) = RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t2
    go (RVar tv
_ r
_)       = Maybe Doc
forall a. Maybe a
Nothing
    go (RAllE Symbol
_ RTypeV v RTyCon tv r
t1 RTypeV v RTyCon tv r
t2)  = RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t2
    go (REx Symbol
_ RTypeV v RTyCon tv r
t1 RTypeV v RTyCon tv r
t2)    = RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t2
    go (RAppTy RTypeV v RTyCon tv r
t1 RTypeV v RTyCon tv r
t2 r
_) = RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t2
    go (RRTy [(Symbol, RTypeV v RTyCon tv r)]
_ r
_ Oblig
_ RTypeV v RTyCon tv r
t)   = RTypeV v RTyCon tv r -> Maybe Doc
go RTypeV v RTyCon tv r
t
    go (RExprArg Located (ExprV v)
_)     = Doc -> Maybe Doc
forall a. a -> Maybe a
Just (Doc -> Maybe Doc) -> Doc -> Maybe Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Logical expressions cannot appear inside a Haskell type"
    go (RHole r
_)        = Maybe Doc
forall a. Maybe a
Nothing

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


checkAbstractRefs
  :: (PPrint t, Reftable t, SubsTy RTyVar RSort t, 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 = RType RTyCon RTyVar (UReft t) -> Maybe Doc
forall {v} {r}.
PPrint (PVarV v ()) =>
RTypeV Symbol RTyCon RTyVar (UReftV v r) -> Maybe Doc
go RType RTyCon RTyVar (UReft t)
rt
  where
    penv :: [PVar RSort]
penv = RType RTyCon RTyVar (UReft t) -> [PVar RSort]
forall {v} {c} {tv} {r}. RTypeV v c tv r -> [PVUV v c tv]
mkPEnv RType RTyCon RTyVar (UReft t)
rt

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

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

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


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

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

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

    mkPEnv :: RTypeV v c tv r -> [PVUV v c tv]
mkPEnv (RAllT RTVUV v c tv
_ RTypeV v c tv r
t r
_) = RTypeV v c tv r -> [PVUV v c tv]
mkPEnv RTypeV v c tv r
t
    mkPEnv (RAllP PVUV v c tv
p RTypeV v c tv r
t)   = PVUV v c tv
pPVUV v c tv -> [PVUV v c tv] -> [PVUV v c tv]
forall a. a -> [a] -> [a]
:RTypeV v c tv r -> [PVUV v c tv]
mkPEnv RTypeV v c tv r
t
    mkPEnv RTypeV v c tv r
_             = []
    pvType' :: PVarV v t -> RSort
pvType' PVarV v t
p          = String -> ListNE RSort -> RSort
forall a. HasCallStack => String -> ListNE a -> a
Misc.safeHead (PVarV v t -> String
forall a. PPrint a => a -> String
showpp PVarV v t
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" not in env of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RType RTyCon RTyVar (UReft t) -> String
forall a. PPrint a => a -> String
showpp RType RTyCon RTyVar (UReft t)
rt) [PVar RSort -> RSort
forall v t. PVarV v t -> t
pvType PVar RSort
q | PVar RSort
q <- [PVar RSort]
penv, PVarV v t -> Symbol
forall v t. PVarV v t -> Symbol
pname PVarV v t
p Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== PVar RSort -> Symbol
forall v t. PVarV v t -> Symbol
pname PVar RSort
q]


checkReft                    :: (PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable (RTProp RTyCon RTyVar (UReft r)))
                             => F.SrcSpan -> F.SEnv F.SortedReft -> F.TCEmb TyCon -> Maybe (RRType (UReft r)) -> UReft r -> ElabM (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
-> Reader ElabFlags (Maybe Doc)
checkReft SrcSpan
_  SEnv SortedReft
_   TCEmb TyCon
_   Maybe (RRType (UReft r))
Nothing  UReft r
_ = Maybe Doc -> Reader ElabFlags (Maybe Doc)
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Doc
forall a. Maybe a
Nothing -- TODO:RPropP/Ref case, not sure how to check these yet.
checkReft SrcSpan
sp SEnv SortedReft
env TCEmb TyCon
emb (Just RRType (UReft r)
t) UReft r
_ = do me <- SrcSpan
-> SEnv SortedReft -> SortedReft -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> a -> Reader ElabFlags (Maybe Doc)
checkSortedReftFull SrcSpan
sp SEnv SortedReft
env SortedReft
r
                                     pure $ (\Doc
z -> Doc
dr Doc -> Doc -> Doc
$+$ Doc
z) <$> me
  where
    r :: SortedReft
r                           = TCEmb TyCon -> RRType (UReft r) -> SortedReft
forall r.
(PPrint r, 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
<+> SortedReft -> Doc
forall a. PPrint a => a -> Doc
pprint SortedReft
r

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

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

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

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

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

checkMBodyUnify
  :: RType t t2 t1 -> RType c tv r -> [(t2,RType c tv (),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 = RTypeV Symbol t t2 t1
-> RTypeV Symbol c tv r
-> [(t2, RTypeV Symbol c tv (), RTypeV Symbol c tv r)]
forall {v} {c} {tv} {r} {v} {c} {tv} {r}.
RTypeV v c tv r
-> RTypeV v c tv r -> [(tv, RTypeV v c tv (), RTypeV v c tv r)]
go
  where
    go :: RTypeV v c tv r
-> RTypeV v c tv r -> [(tv, RTypeV v c tv (), RTypeV v c tv r)]
go (RVar tv
tv r
_) RTypeV v c tv r
t      = [(tv
tv, RTypeV v c tv r -> RTypeV v c tv ()
forall v c tv r. RTypeV v c tv r -> RTypeV v c tv ()
toRSort RTypeV v c tv r
t, RTypeV v c tv r
t)]
    go t :: RTypeV v c tv r
t@RApp{} t' :: RTypeV v c tv r
t'@RApp{} = [[(tv, RTypeV v c tv (), RTypeV v c tv r)]]
-> [(tv, RTypeV v c tv (), RTypeV v c tv r)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(tv, RTypeV v c tv (), RTypeV v c tv r)]]
 -> [(tv, RTypeV v c tv (), RTypeV v c tv r)])
-> [[(tv, RTypeV v c tv (), RTypeV v c tv r)]]
-> [(tv, RTypeV v c tv (), RTypeV v c tv r)]
forall a b. (a -> b) -> a -> b
$ (RTypeV v c tv r
 -> RTypeV v c tv r -> [(tv, RTypeV v c tv (), RTypeV v c tv r)])
-> [RTypeV v c tv r]
-> [RTypeV v c tv r]
-> [[(tv, RTypeV v c tv (), RTypeV v c tv r)]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith RTypeV v c tv r
-> RTypeV v c tv r -> [(tv, RTypeV v c tv (), RTypeV v c tv r)]
go (RTypeV v c tv r -> [RTypeV v c tv r]
forall v c tv r. RTypeV v c tv r -> [RTypeV v c tv r]
rt_args RTypeV v c tv r
t) (RTypeV v c tv r -> [RTypeV v c tv r]
forall v c tv r. RTypeV v c tv r -> [RTypeV v c tv r]
rt_args RTypeV v c tv r
t')
    go RTypeV v c tv r
_ RTypeV v c tv r
_                = []

checkMBody' :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r))
            => F.TCEmb TyCon
            -> RType RTyCon RTyVar r
            -> F.SEnv F.SortedReft
            -> F.SrcSpan
            -> Body
            -> ElabM (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
-> BodyV Symbol
-> Reader ElabFlags (Maybe Doc)
checkMBody' TCEmb TyCon
emb RType RTyCon RTyVar r
sort SEnv SortedReft
γ SrcSpan
sp BodyV Symbol
body =
  case BodyV Symbol
body of
    E Expr
e   -> SrcSpan
-> SEnv SortedReft -> Sort -> Expr -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan
-> SEnv SortedReft -> Sort -> a -> Reader ElabFlags (Maybe Doc)
checkSortFull SrcSpan
sp SEnv SortedReft
γ (TCEmb TyCon -> RType RTyCon RTyVar r -> Sort
forall r.
(PPrint r, 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   -> SrcSpan
-> SEnv SortedReft -> Sort -> Expr -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan
-> SEnv SortedReft -> Sort -> a -> Reader ElabFlags (Maybe Doc)
checkSortFull SrcSpan
sp SEnv SortedReft
γ Sort
F.boolSort  Expr
p
    R Symbol
s Expr
p -> SrcSpan
-> SEnv SortedReft -> Sort -> Expr -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan
-> SEnv SortedReft -> Sort -> a -> Reader ElabFlags (Maybe Doc)
checkSortFull SrcSpan
sp (Symbol -> SortedReft -> SEnv SortedReft -> SEnv SortedReft
forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
s SortedReft
sty SEnv SortedReft
γ) Sort
F.boolSort Expr
p
  where
    sty :: SortedReft
sty   = TCEmb TyCon -> RType RTyCon RTyVar r -> SortedReft
forall r.
(PPrint r, 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' = Int -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
forall r. Int -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
dropNArgs Int
1 RType RTyCon RTyVar r
sort

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


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

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

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


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

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

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