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

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

import           Language.Haskell.Liquid.Constraint.ToFixpoint
import           Language.Haskell.Liquid.GHC.API          as Ghc hiding (Located) 
import           Control.Applicative                       ((<|>))
import           Control.Arrow                             ((&&&))
import           Data.Maybe
import           Data.Function                             (on)
import           Text.PrettyPrint.HughesPJ                 hiding ((<>))
import qualified Data.List                                 as L
import qualified Data.HashMap.Strict                       as M
import qualified Data.HashSet                              as S
import           Data.Hashable
import qualified Language.Fixpoint.Misc                    as Misc  
import           Language.Fixpoint.SortCheck               (checkSorted, checkSortedReftFull, checkSortFull)
import qualified Language.Fixpoint.Types                   as F 
import qualified Language.Haskell.Liquid.GHC.Misc          as GM 
import           Language.Haskell.Liquid.Misc              (condNull, snd4)
import           Language.Haskell.Liquid.Types
import           Language.Haskell.Liquid.WiredIn
import           Language.Haskell.Liquid.LawInstances      (checkLawInstances)

import qualified Language.Haskell.Liquid.Measure           as Ms
import qualified Language.Haskell.Liquid.Bare.Types        as Bare 
import qualified Language.Haskell.Liquid.Bare.Resolve      as Bare 


----------------------------------------------------------------------------------------------
-- | Checking BareSpec ------------------------------------------------------------------------
----------------------------------------------------------------------------------------------
checkBareSpec :: ModName -> Ms.BareSpec -> Either Diagnostics ()
checkBareSpec :: ModName -> BareSpec -> Either Diagnostics ()
checkBareSpec ModName
_ 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   = BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.inlines    BareSpec
sp
    hmeasures :: HashSet LocSymbol
hmeasures = BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas      BareSpec
sp
    reflects :: HashSet LocSymbol
reflects  = BareSpec -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects   BareSpec
sp
    measures :: [LocSymbol]
measures  = Measure LocBareType LocSymbol -> LocSymbol
forall ty ctor. Measure ty ctor -> LocSymbol
msName    (Measure LocBareType LocSymbol -> LocSymbol)
-> [Measure LocBareType LocSymbol] -> [LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BareSpec -> [Measure LocBareType LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.measures BareSpec
sp
    fields :: [LocSymbol]
fields    = (DataDecl -> [LocSymbol]) -> [DataDecl] -> [LocSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataDecl -> [LocSymbol]
dataDeclFields (BareSpec -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.dataDecls BareSpec
sp)

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

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

isGadt :: DataCtor -> Bool 
isGadt :: DataCtor -> Bool
isGadt = 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
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' :: (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] 
-- mkErr <$> dups
  where
    -- mkErr (n, ls@(l:_))    = ErrDupSpecs l (pprint n) ls
    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, Hashable 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
sp
  | 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      =  ((Symbol, LocSpecType) -> Diagnostics)
-> [(Symbol, LocSpecType)] -> Diagnostics
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Symbol, LocSpecType)
-> Diagnostics
forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"measure"      TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) (GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas       (TargetSpec -> GhcSpecData
gsData TargetSpec
sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Bool -> Diagnostics -> Diagnostics
forall m. Monoid m => Bool -> m -> m
condNull Bool
noPrune
                        (((Var, LocSpecType) -> Diagnostics)
-> [(Var, LocSpecType)] -> Diagnostics
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, LocSpecType)
-> Diagnostics
forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"constructor"  TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) ([(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
sp)))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> ((Var, LocSpecType) -> Diagnostics)
-> [(Var, LocSpecType)] -> Diagnostics
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, LocSpecType)
-> Diagnostics
forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"assume"       TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) (GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs    (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> ((Var, LocSpecType) -> Diagnostics)
-> [(Var, LocSpecType)] -> Diagnostics
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, LocSpecType)
-> Diagnostics
forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"reflect"      TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) (GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs    (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Bool
-> Bool
-> [CoreBind]
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> GhcSpecSig
-> Diagnostics
checkTySigs         Bool
allowHO Bool
bsc [CoreBind]
cbs            TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env                (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp)
                     -- ++ mapMaybe (checkTerminationExpr             emb       env) (gsTexprs     (gsSig  sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> ((Var, LocSpecType) -> Diagnostics)
-> [(Var, LocSpecType)] -> Diagnostics
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, LocSpecType)
-> Diagnostics
forall v.
PPrint v =>
Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
"class method" TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env) (GhcSpecSig -> [(Var, LocSpecType)]
clsSigs      (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> ((Maybe Var, LocSpecType) -> Diagnostics)
-> [(Maybe Var, LocSpecType)] -> Diagnostics
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Maybe Var, LocSpecType)
-> Diagnostics
checkInv Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env)                 (GhcSpecData -> [(Maybe Var, LocSpecType)]
gsInvariants (TargetSpec -> GhcSpecData
gsData TargetSpec
sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> [(LocSpecType, LocSpecType)]
-> Diagnostics
checkIAl Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env                            (GhcSpecData -> [(LocSpecType, LocSpecType)]
gsIaliases   (TargetSpec -> GhcSpecData
gsData TargetSpec
sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> TCEmb TyCon
-> SEnv SortedReft -> [Measure SpecType DataCon] -> Diagnostics
checkMeasures TCEmb TyCon
emb SEnv SortedReft
env [Measure SpecType DataCon]
ms
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> [Measure SpecType DataCon] -> Diagnostics
checkClassMeasures                                        (GhcSpecData -> [Measure SpecType DataCon]
gsMeasures (TargetSpec -> GhcSpecData
gsData TargetSpec
sp))
                     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
sp)) (GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs     (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> ((Var, LocSpecType) -> Diagnostics)
-> [(Var, LocSpecType)] -> Diagnostics
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Var, LocSpecType) -> Diagnostics
checkMismatch [(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
sp))
                     -- 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
sp))
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> [(Var, LocSpecType)] -> [(Var, LocSpecType)] -> Diagnostics
checkDupIntersect                                         (GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp)) (GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp))
                     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
<> TCEmb TyCon -> SEnv SortedReft -> [TyConP] -> Diagnostics
checkSizeFun TCEmb TyCon
emb SEnv SortedReft
env                                      (GhcSpecNames -> [TyConP]
gsTconsP (TargetSpec -> GhcSpecNames
gsName TargetSpec
sp))
                     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 (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
sp) ])
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> GhcSpecLaws -> Diagnostics
checkLawInstances (TargetSpec -> GhcSpecLaws
gsLaws TargetSpec
sp)
                     Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> TargetSpec -> Diagnostics
checkRewrites TargetSpec
sp

    _rClasses :: [RClass LocBareType]
_rClasses         = (BareSpec -> [RClass LocBareType])
-> [BareSpec] -> [RClass LocBareType]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BareSpec -> [RClass LocBareType]
forall ty bndr. Spec ty bndr -> [RClass ty]
Ms.classes  ) [BareSpec]
specs
    _rInsts :: [RInstance LocBareType]
_rInsts           = (BareSpec -> [RInstance LocBareType])
-> [BareSpec] -> [RInstance LocBareType]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BareSpec -> [RInstance LocBareType]
forall ty bndr. Spec ty bndr -> [RInstance 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 ty bndr. Spec ty bndr -> [Located (RTAlias Symbol BareType)]
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 ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
Ms.ealiases BareSpec
sp | BareSpec
sp <- [BareSpec]
specs]
    emb :: TCEmb TyCon
emb              = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (TargetSpec -> GhcSpecNames
gsName TargetSpec
sp)
    tcEnv :: TyConMap
tcEnv            = GhcSpecNames -> TyConMap
gsTyconEnv (TargetSpec -> GhcSpecNames
gsName TargetSpec
sp)
    ms :: [Measure SpecType DataCon]
ms               = GhcSpecData -> [Measure SpecType DataCon]
gsMeasures (TargetSpec -> GhcSpecData
gsData TargetSpec
sp)
    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
sp) [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp) [(Var, LocSpecType)]
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecData -> [(Var, LocSpecType)]
gsCtors (TargetSpec -> GhcSpecData
gsData TargetSpec
sp)
    allowHO :: Bool
allowHO          = TargetSpec -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag TargetSpec
sp
    bsc :: Bool
bsc              = Config -> Bool
bscope (TargetSpec -> Config
forall t. HasConfig t => t -> Config
getConfig TargetSpec
sp)
    noPrune :: Bool
noPrune          = Bool -> Bool
not (TargetSpec -> Bool
forall t. HasConfig t => t -> Bool
pruneFlag TargetSpec
sp)
    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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f b -> f b) -> f (f b) -> f (f b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> b) -> f b -> 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
sp
    -- env'             = L.foldl' (\e (x, s) -> insertSEnv x (RR s mempty) e) env wiredSortedSyms





checkPlugged :: PPrint v => [(v, LocSpecType)] -> Diagnostics
checkPlugged :: [(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
mkErr (((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
    mkErr :: (a, Located a) -> TError t
mkErr (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
            -> Diagnostics
--------------------------------------------------------------------------------
checkTySigs :: Bool
-> Bool
-> [CoreBind]
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> GhcSpecSig
-> Diagnostics
checkTySigs Bool
allowHO Bool
bsc [CoreBind]
cbs TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env GhcSpecSig
sig
                   = [Diagnostics] -> Diagnostics
forall a. Monoid a => [a] -> a
mconcat (((Var, (LocSpecType, Maybe [Located Expr])) -> Diagnostics)
-> [(Var, (LocSpecType, Maybe [Located Expr]))] -> [Diagnostics]
forall a b. (a -> b) -> [a] -> [b]
map (SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr])) -> Diagnostics
check SEnv SortedReft
env) [(Var, (LocSpecType, Maybe [Located Expr]))]
topTs)
                     -- (mapMaybe   (checkT env) [ (x, t)     | (x, (t, _)) <- topTs])
                     -- ++ (mapMaybe   (checkE env) [ (x, t, es) | (x, (t, Just es)) <- topTs])
                  Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> CoreVisitor (SEnv SortedReft) Diagnostics
-> SEnv SortedReft -> Diagnostics -> [CoreBind] -> Diagnostics
forall env acc.
CoreVisitor env acc -> env -> acc -> [CoreBind] -> acc
coreVisitor CoreVisitor (SEnv SortedReft) Diagnostics
checkVisitor SEnv SortedReft
env Diagnostics
emptyDiagnostics [CoreBind]
cbs
  where
    check :: SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr])) -> Diagnostics
check SEnv SortedReft
env      = Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr]))
-> Diagnostics
checkSigTExpr Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env
    locTm :: HashMap Var (LocSpecType, Maybe [Located Expr])
locTm          = [(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  :: CoreVisitor (F.SEnv F.SortedReft) Diagnostics
    checkVisitor :: CoreVisitor (SEnv SortedReft) Diagnostics
checkVisitor   = CoreVisitor :: forall env acc.
(env -> Var -> env)
-> (env -> acc -> Var -> acc)
-> (env -> acc -> CoreExpr -> acc)
-> CoreVisitor env acc
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 -> SEnv SortedReft -> Var -> Diagnostics
errs SEnv SortedReft
env Var
v 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 :: SEnv SortedReft -> Var -> 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
emptyDiagnostics
                         Just (LocSpecType, Maybe [Located Expr])
t  -> SEnv SortedReft
-> (Var, (LocSpecType, Maybe [Located Expr])) -> Diagnostics
check SEnv SortedReft
env (Var
v, (LocSpecType, Maybe [Located Expr])
t) 

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

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

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

-- | Used for termination checking. If we have no \"len\" defined /yet/ (for example we are checking
-- 'GHC.Prim') then we want to skip this check.
checkSizeFun :: F.TCEmb TyCon -> F.SEnv F.SortedReft -> [TyConP] -> Diagnostics
checkSizeFun :: TCEmb TyCon -> SEnv SortedReft -> [TyConP] -> Diagnostics
checkSizeFun TCEmb TyCon
emb SEnv SortedReft
env [TyConP]
tys = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty ((((Symbol -> Expr, TyConP), Doc) -> Error)
-> [((Symbol -> Expr, TyConP), Doc)] -> [Error]
forall a b. (a -> b) -> [a] -> [b]
map ((Symbol -> Expr, TyConP), Doc) -> Error
forall a t. PPrint a => ((Symbol -> a, TyConP), Doc) -> TError t
mkError ((TyConP -> Maybe ((Symbol -> Expr, TyConP), Doc))
-> [TyConP] -> [((Symbol -> Expr, TyConP), Doc)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TyConP -> Maybe ((Symbol -> Expr, TyConP), Doc)
go [TyConP]
tys))
  where
    mkError :: ((Symbol -> a, TyConP), Doc) -> TError t
mkError ((Symbol -> a
f, TyConP
tcp), Doc
msg)  = 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 :: TyConP -> Maybe ((Symbol -> Expr, TyConP), Doc)
go 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                    -> (Symbol -> Expr) -> TyConP -> Maybe ((Symbol -> Expr, TyConP), Doc)
forall a.
Checkable a =>
(Symbol -> a) -> TyConP -> Maybe ((Symbol -> a, TyConP), Doc)
checkWFSize (SizeFun -> Symbol -> Expr
szFun SizeFun
f) TyConP
tcp

    checkWFSize :: (Symbol -> a) -> TyConP -> Maybe ((Symbol -> a, TyConP), Doc)
checkWFSize Symbol -> a
f TyConP
tcp = ((Symbol -> a
f, TyConP
tcp),) (Doc -> ((Symbol -> a, TyConP), Doc))
-> Maybe Doc -> Maybe ((Symbol -> a, TyConP), Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc
forall a.
Checkable a =>
SrcSpan -> SEnv SortedReft -> Sort -> a -> 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)
    x :: Symbol
x                 = Symbol
"x" :: F.Symbol
    mkTySort :: TyCon -> SortedReft
mkTySort TyCon
tc       = TCEmb TyCon -> RRType () -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RRType ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb (Type -> RRType ()
forall r. Monoid r => Type -> RRType r
ofType (Type -> RRType ()) -> Type -> RRType ()
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

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

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

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

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

checkInv :: Bool
         -> BScope
         -> F.TCEmb TyCon
         -> Bare.TyConMap
         -> F.SEnv F.SortedReft
         -> (Maybe Var, LocSpecType)
         -> Diagnostics
checkInv :: Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (Maybe Var, LocSpecType)
-> Diagnostics
checkInv Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (Maybe Var
_, LocSpecType
t) = Bool
-> Bool
-> (Doc -> Error)
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> LocSpecType
-> Diagnostics
checkTy Bool
allowHO Bool
bsc Doc -> Error
err TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env LocSpecType
t
  where
    err :: Doc -> Error
err              = 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)]
         -> Diagnostics
checkIAl :: Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> [(LocSpecType, LocSpecType)]
-> Diagnostics
checkIAl Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env = [Diagnostics] -> Diagnostics
forall a. Monoid a => [a] -> a
mconcat ([Diagnostics] -> Diagnostics)
-> ([(LocSpecType, LocSpecType)] -> [Diagnostics])
-> [(LocSpecType, LocSpecType)]
-> Diagnostics
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((LocSpecType, LocSpecType) -> Diagnostics)
-> [(LocSpecType, LocSpecType)] -> [Diagnostics]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (LocSpecType, LocSpecType)
-> Diagnostics
checkIAlOne Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env)

checkIAlOne :: Bool
            -> BScope
            -> F.TCEmb TyCon
            -> Bare.TyConMap
            -> F.SEnv F.SortedReft
            -> (LocSpecType, LocSpecType)
            -> Diagnostics
checkIAlOne :: Bool
-> Bool
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (LocSpecType, LocSpecType)
-> Diagnostics
checkIAlOne Bool
allowHO Bool
bsc TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (LocSpecType
t1, LocSpecType
t2) = [Diagnostics] -> Diagnostics
forall a. Monoid a => [a] -> a
mconcat ([Diagnostics] -> Diagnostics) -> [Diagnostics] -> Diagnostics
forall a b. (a -> b) -> a -> b
$ Diagnostics
checkEq Diagnostics -> [Diagnostics] -> [Diagnostics]
forall a. a -> [a] -> [a]
: (LocSpecType -> Diagnostics
tcheck (LocSpecType -> Diagnostics) -> [LocSpecType] -> [Diagnostics]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [LocSpecType
t1, LocSpecType
t2])
  where
    tcheck :: LocSpecType -> Diagnostics
tcheck LocSpecType
t = Bool
-> Bool
-> (Doc -> Error)
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> LocSpecType
-> Diagnostics
checkTy Bool
allowHO Bool
bsc (LocSpecType -> Doc -> Error
forall t. Located t -> Doc -> TError t
err LocSpecType
t) TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env LocSpecType
t
    err :: Located t -> Doc -> TError t
err    Located t
t = 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' :: RRType ()
t1'      = SpecType -> RRType ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort (SpecType -> RRType ()) -> SpecType -> RRType ()
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t1
    t2'      :: RSort
    t2' :: RRType ()
t2'      = SpecType -> RRType ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort (SpecType -> RRType ()) -> SpecType -> RRType ()
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t2
    checkEq :: Diagnostics
checkEq  = if RRType ()
t1' RRType () -> RRType () -> Bool
forall a. Eq a => a -> a -> Bool
== RRType ()
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 :: 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)
          -> Diagnostics
checkBind :: Bool
-> Bool
-> Doc
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> (v, LocSpecType)
-> Diagnostics
checkBind Bool
allowHO Bool
bsc Doc
s TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env (v
v, LocSpecType
t) = Bool
-> Bool
-> (Doc -> Error)
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> LocSpecType
-> Diagnostics
checkTy Bool
allowHO Bool
bsc Doc -> Error
msg TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env LocSpecType
t
  where
    msg :: Doc -> Error
msg                      = 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])
                     -> Diagnostics
checkTerminationExpr :: TCEmb TyCon
-> SEnv SortedReft
-> (v, LocSpecType, [Located Expr])
-> Diagnostics
checkTerminationExpr TCEmb TyCon
emb SEnv SortedReft
env (v
v, Loc SourcePos
l SourcePos
_ SpecType
t, [Located Expr]
les)
            = (Doc -> Maybe (Expr, Doc) -> Diagnostics
mkErr Doc
"ill-sorted" (Maybe (Expr, Doc) -> Diagnostics)
-> Maybe (Expr, Doc) -> Diagnostics
forall a b. (a -> b) -> a -> b
$ [Located Expr] -> Maybe (Expr, Doc)
go [Located Expr]
les) Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> (Doc -> Maybe (Expr, Doc) -> Diagnostics
mkErr Doc
"non-numeric" (Maybe (Expr, Doc) -> Diagnostics)
-> Maybe (Expr, Doc) -> Diagnostics
forall a b. (a -> b) -> a -> b
$ [Located Expr] -> Maybe (Expr, Doc)
go' [Located Expr]
les)
  where
    -- es      = val <$> les
    mkErr :: Doc -> Maybe (F.Expr, Doc) -> Diagnostics
    mkErr :: Doc -> Maybe (Expr, Doc) -> Diagnostics
mkErr Doc
_ Maybe (Expr, Doc)
Nothing = Diagnostics
emptyDiagnostics
    mkErr Doc
k (Just (Expr, Doc)
e) =
      [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty [(Expr -> Doc -> Error) -> (Expr, Doc) -> Error
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (\ 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
t Doc
d) (Expr, Doc)
e]
    -- mkErr   = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "ill-sorted" ) e t d)
    -- mkErr'  = uncurry (\ e d -> ErrTermSpec (GM.sourcePosSrcSpan l) (pprint v) (text "non-numeric") e t d)

    go :: [F.Located F.Expr] -> Maybe (F.Expr, Doc)
    go :: [Located Expr] -> Maybe (Expr, Doc)
go      = (Maybe (Expr, Doc) -> Located Expr -> Maybe (Expr, Doc))
-> Maybe (Expr, Doc) -> [Located Expr] -> Maybe (Expr, Doc)
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 (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
<$> SrcSpan -> SEnv Sort -> Expr -> Maybe Doc
forall a. Checkable a => SrcSpan -> SEnv Sort -> a -> 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))     Maybe (Expr, Doc)
forall a. Maybe a
Nothing

    go' :: [F.Located F.Expr] -> Maybe (F.Expr, Doc)
    go' :: [Located Expr] -> Maybe (Expr, Doc)
go'     = (Maybe (Expr, Doc) -> Located Expr -> Maybe (Expr, Doc))
-> Maybe (Expr, Doc) -> [Located Expr] -> Maybe (Expr, Doc)
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 (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
<$> SrcSpan -> SEnv Sort -> Expr -> Maybe Doc
forall a. Checkable a => SrcSpan -> SEnv Sort -> a -> 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)) 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 (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)]
mkClass ([(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 (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep) (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep)
    trep :: RTypeRep RTyCon RTyVar RReft
trep    = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t

    mkClass :: (Symbol, SpecType) -> [(Symbol, SortedReft)]
mkClass (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)
    mkClass (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 (RRType ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb
    cmpZero :: Located Expr -> Expr
cmpZero Located Expr
e = Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Le (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
        -> Diagnostics
checkTy :: Bool
-> Bool
-> (Doc -> Error)
-> TCEmb TyCon
-> TyConMap
-> SEnv SortedReft
-> LocSpecType
-> Diagnostics
checkTy Bool
allowHO Bool
bsc Doc -> Error
mkE TCEmb TyCon
emb TyConMap
tcEnv SEnv SortedReft
env LocSpecType
t =
  case Bool
-> Bool
-> TCEmb TyCon
-> SEnv SortedReft
-> LocSpecType
-> Maybe Doc
checkRType Bool
allowHO Bool
bsc TCEmb TyCon
emb SEnv SortedReft
env (TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
Bare.txRefSort TyConMap
tcEnv TCEmb TyCon
emb LocSpecType
t) of
    Maybe Doc
Nothing -> Diagnostics
emptyDiagnostics
    Just Doc
d  -> [Warning] -> [Error] -> Diagnostics
mkDiagnostics [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 (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 (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

-- checkDuplicate xts = mkErr <$> dups
  -- where
    -- mkErr (x, ts) = ErrDupSpecs (getSrcSpan x) (pprint x) (GM.fSrcSpan <$> ts)
    -- dups          = [z | z@(_, _:_:_) <- M.toList $ group xts ]

checkDuplicateRTAlias :: String -> [Located (RTAlias s a)] -> Diagnostics
checkDuplicateRTAlias :: 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
mkErr [[Located (RTAlias s a)]]
dups)
  where
    mkErr :: [Located (RTAlias x a)] -> TError t
mkErr 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)
    mkErr []                = Maybe SrcSpan -> String -> TError t
forall a. 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) -> Located (RTAlias s a) -> Bool)
-> [Located (RTAlias s a)] -> [[Located (RTAlias s a)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
L.groupBy (Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Symbol -> Symbol -> Bool)
-> (Located (RTAlias s a) -> Symbol)
-> Located (RTAlias s a)
-> Located (RTAlias s a)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (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]


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'
    t' :: LocSpecType
t'               = SpecType -> SpecType
forall c tv r. RType c tv r -> RType c tv r
dropImplicits (SpecType -> SpecType) -> LocSpecType -> LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSpecType
t

tyCompat :: Var -> RType RTyCon RTyVar r -> Bool
tyCompat :: Var -> RType RTyCon RTyVar r -> Bool
tyCompat Var
x RType RTyCon RTyVar r
t         = RRType ()
lqT RRType () -> RRType () -> Bool
forall a. Eq a => a -> a -> Bool
== RRType ()
hsT
  where
    RRType ()
lqT :: RSort     = RType RTyCon RTyVar r -> RRType ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort RType RTyCon RTyVar r
t
    RRType ()
hsT :: RSort     = Type -> RRType ()
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]
++ RRType () -> String
forall a. PPrint a => a -> String
F.showpp RRType ()
hsT String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :lq = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RRType () -> String
forall a. PPrint a => a -> String
F.showpp RRType ()
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
$ SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType (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 -> Maybe Doc
------------------------------------------------------------------------------------------------
checkRType :: Bool
-> Bool
-> TCEmb TyCon
-> SEnv SortedReft
-> LocSpecType
-> Maybe Doc
checkRType Bool
allowHO Bool
bsc TCEmb TyCon
emb SEnv SortedReft
env LocSpecType
lt
  =   SpecType -> Maybe Doc
forall t t1. RType RTyCon t t1 -> Maybe Doc
checkAppTys SpecType
t
  Maybe Doc -> Maybe Doc -> Maybe Doc
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SpecType -> Maybe Doc
forall t.
(PPrint t, Reftable t, SubsTy RTyVar (RRType ()) t,
 Reftable (RTProp RTyCon RTyVar (UReft t))) =>
RType RTyCon RTyVar (UReft t) -> Maybe Doc
checkAbstractRefs SpecType
t
  Maybe Doc -> Maybe Doc -> Maybe Doc
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Symbol -> SpecType -> Bool)
-> Bool
-> (RTyCon -> [SpecType] -> [(Symbol, SortedReft)])
-> (RTVar RTyVar (RRType ()) -> [(Symbol, SortedReft)])
-> (SpecType -> SortedReft)
-> (SEnv SortedReft
    -> Maybe SpecType -> RReft -> Maybe Doc -> Maybe Doc)
-> (PVar (RRType ()) -> SEnv SortedReft -> SEnv SortedReft)
-> SEnv SortedReft
-> Maybe Doc
-> SpecType
-> Maybe Doc
forall r c tv a b.
(Reftable r, TyConable c) =>
(Symbol -> RType c tv r -> Bool)
-> Bool
-> (c -> [RType c tv r] -> [(Symbol, a)])
-> (RTVar tv (RType c tv ()) -> [(Symbol, a)])
-> (RType c tv r -> a)
-> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b)
-> (PVar (RType c tv ()) -> SEnv a -> SEnv a)
-> SEnv a
-> b
-> RType c tv r
-> b
efoldReft Symbol -> SpecType -> Bool
forall p t t1 t2. p -> RType t t1 t2 -> Bool
farg Bool
bsc RTyCon -> [SpecType] -> [(Symbol, SortedReft)]
cb (TCEmb TyCon -> RTVar RTyVar (RRType ()) -> [(Symbol, SortedReft)]
tyToBind TCEmb TyCon
emb) (TCEmb TyCon -> SpecType -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RRType ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb) SEnv SortedReft
-> Maybe SpecType -> RReft -> Maybe Doc -> Maybe Doc
forall r.
(PPrint r, SubsTy RTyVar (RRType ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar (UReft r))) =>
SEnv SortedReft
-> Maybe (RRType (UReft r)) -> UReft r -> Maybe Doc -> Maybe Doc
f PVar (RRType ()) -> SEnv SortedReft -> SEnv SortedReft
insertPEnv SEnv SortedReft
env Maybe Doc
forall a. Maybe a
Nothing SpecType
t
  where
    t :: SpecType
t                  = 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
    f :: SEnv SortedReft
-> Maybe (RRType (UReft r)) -> UReft r -> Maybe Doc -> Maybe Doc
f SEnv SortedReft
env Maybe (RRType (UReft r))
me UReft r
r Maybe Doc
err     = Maybe Doc
err Maybe Doc -> Maybe Doc -> Maybe Doc
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SrcSpan
-> SEnv SortedReft
-> TCEmb TyCon
-> Maybe (RRType (UReft r))
-> UReft r
-> Maybe Doc
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RRType ()) r,
 Reftable (RTProp RTyCon RTyVar (UReft r))) =>
SrcSpan
-> SEnv SortedReft
-> TCEmb TyCon
-> Maybe (RRType (UReft r))
-> UReft r
-> 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
    insertPEnv :: PVar (RRType ()) -> SEnv SortedReft -> SEnv SortedReft
insertPEnv PVar (RRType ())
p SEnv SortedReft
γ     = SEnv SortedReft -> [(Symbol, SortedReft)] -> SEnv SortedReft
forall a. SEnv a -> [(Symbol, a)] -> SEnv a
insertsSEnv SEnv SortedReft
γ ((RRType () -> SortedReft)
-> (Symbol, RRType ()) -> (Symbol, SortedReft)
forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd (TCEmb TyCon -> RRType () -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RRType ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
emb) ((Symbol, RRType ()) -> (Symbol, SortedReft))
-> [(Symbol, RRType ())] -> [(Symbol, SortedReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVar (RRType ()) -> [(Symbol, RRType ())]
pbinds PVar (RRType ())
p)
    pbinds :: PVar (RRType ()) -> [(Symbol, RRType ())]
pbinds PVar (RRType ())
p           = (PVar (RRType ()) -> Symbol
forall t. PVar t -> Symbol
pname PVar (RRType ())
p, PVar (RRType ()) -> RRType ()
forall r. (PPrint r, Reftable r) => PVar (RRType ()) -> RRType r
pvarRType PVar (RRType ())
p :: RSort) (Symbol, RRType ())
-> [(Symbol, RRType ())] -> [(Symbol, RRType ())]
forall a. a -> [a] -> [a]
: [(Symbol
x, RRType ()
tx) | (RRType ()
tx, Symbol
x, Expr
_) <- PVar (RRType ()) -> [(RRType (), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar (RRType ())
p]

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

checkAppTys :: RType RTyCon t t1 -> Maybe Doc
checkAppTys :: RType RTyCon t t1 -> Maybe Doc
checkAppTys = RType RTyCon t t1 -> Maybe Doc
forall t t1. RType RTyCon t t1 -> Maybe Doc
go
  where
    go :: RType RTyCon tv r -> Maybe Doc
go (RAllT RTVU RTyCon tv
_ RType RTyCon tv r
t r
_)    = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t
    go (RAllP PVU RTyCon tv
_ RType RTyCon tv r
t)      = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t
    go (RApp RTyCon
rtc [RType RTyCon tv r]
ts [RTProp RTyCon tv r]
_ r
_)
      = RTyCon -> Int -> Maybe Doc
checkTcArity RTyCon
rtc ([RType RTyCon tv r] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType RTyCon tv r]
ts) Maybe Doc -> Maybe Doc -> Maybe Doc
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
        (Maybe Doc -> RType RTyCon tv r -> Maybe Doc)
-> Maybe Doc -> [RType RTyCon tv r] -> Maybe Doc
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\Maybe Doc
merr RType RTyCon tv r
t -> Maybe Doc
merr Maybe Doc -> Maybe Doc -> Maybe Doc
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t) Maybe Doc
forall a. Maybe a
Nothing [RType RTyCon tv r]
ts
    go (RImpF Symbol
_ RType RTyCon tv r
t1 RType RTyCon tv r
t2 r
_)= RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t2
    go (RFun Symbol
_ RType RTyCon tv r
t1 RType RTyCon tv r
t2 r
_) = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t2
    go (RVar tv
_ r
_)       = Maybe Doc
forall a. Maybe a
Nothing
    go (RAllE Symbol
_ RType RTyCon tv r
t1 RType RTyCon tv r
t2)  = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t2
    go (REx Symbol
_ RType RTyCon tv r
t1 RType RTyCon tv r
t2)    = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t2
    go (RAppTy RType RTyCon tv r
t1 RType RTyCon tv r
t2 r
_) = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t1 Maybe Doc -> Maybe Doc -> Maybe Doc
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t2
    go (RRTy [(Symbol, RType RTyCon tv r)]
_ r
_ Oblig
_ RType RTyCon tv r
t)   = RType RTyCon tv r -> Maybe Doc
go RType RTyCon tv r
t
    go (RExprArg Located Expr
_)     = 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, F.Reftable t, SubsTy RTyVar RSort t, F.Reftable (RTProp RTyCon RTyVar (UReft t))) =>
     RType RTyCon RTyVar (UReft t) -> Maybe Doc
checkAbstractRefs :: RType RTyCon RTyVar (UReft t) -> Maybe Doc
checkAbstractRefs RType RTyCon RTyVar (UReft t)
t = RType RTyCon RTyVar (UReft t) -> Maybe Doc
forall r. RType RTyCon RTyVar (UReft r) -> Maybe Doc
go RType RTyCon RTyVar (UReft t)
t
  where
    penv :: [PVar (RRType ())]
penv = RType RTyCon RTyVar (UReft t) -> [PVar (RRType ())]
forall c tv r. RType c tv r -> [PVU c tv]
mkPEnv RType RTyCon RTyVar (UReft t)
t

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

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

    checkOne' :: RTProp RTyCon RTyVar (UReft r) -> PVar (RRType ()) -> Maybe Doc
checkOne' (RProp [(Symbol, RRType ())]
xs (RHole UReft r
_)) PVar (RRType ())
p
      | [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [RRType ()
s1 RRType () -> RRType () -> Bool
forall a. Eq a => a -> a -> Bool
/= RRType ()
s2 | ((Symbol
_, RRType ()
s1), (RRType ()
s2, Symbol
_, Expr
_)) <- [(Symbol, RRType ())]
-> [(RRType (), Symbol, Expr)]
-> [((Symbol, RRType ()), (RRType (), Symbol, Expr))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Symbol, RRType ())]
xs (PVar (RRType ()) -> [(RRType (), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar (RRType ())
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 (RRType ()) -> Doc
forall a. PPrint a => a -> Doc
pprint PVar (RRType ())
p
      | [(Symbol, RRType ())] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RRType ())]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [(RRType (), Symbol, Expr)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PVar (RRType ()) -> [(RRType (), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar (RRType ())
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 (RRType ()) -> Doc
forall a. PPrint a => a -> Doc
pprint PVar (RRType ())
p
      | Bool
otherwise
      = Maybe Doc
forall a. Maybe a
Nothing
    checkOne' (RProp [(Symbol, RRType ())]
xs RType RTyCon RTyVar (UReft r)
t) PVar (RRType ())
p
      | PVar (RRType ()) -> RRType ()
forall t. PVar t -> t
pvType PVar (RRType ())
p RRType () -> RRType () -> Bool
forall a. Eq a => a -> a -> Bool
/= RType RTyCon RTyVar (UReft r) -> RRType ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort RType RTyCon RTyVar (UReft 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 (RRType ()) -> Doc
forall a. PPrint a => a -> Doc
pprint PVar (RRType ())
p
      | [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [RRType ()
s1 RRType () -> RRType () -> Bool
forall a. Eq a => a -> a -> Bool
/= RRType ()
s2 | ((Symbol
_, RRType ()
s1), (RRType ()
s2, Symbol
_, Expr
_)) <- [(Symbol, RRType ())]
-> [(RRType (), Symbol, Expr)]
-> [((Symbol, RRType ()), (RRType (), Symbol, Expr))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Symbol, RRType ())]
xs (PVar (RRType ()) -> [(RRType (), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar (RRType ())
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 (RRType ()) -> Doc
forall a. PPrint a => a -> Doc
pprint PVar (RRType ())
p
      | [(Symbol, RRType ())] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RRType ())]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [(RRType (), Symbol, Expr)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PVar (RRType ()) -> [(RRType (), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar (RRType ())
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 (RRType ()) -> Doc
forall a. PPrint a => a -> Doc
pprint PVar (RRType ())
p
      | Bool
otherwise
      = RType RTyCon RTyVar (UReft r) -> Maybe Doc
go RType RTyCon RTyVar (UReft r)
t


    efold :: (t -> Maybe a) -> t t -> Maybe a
efold t -> Maybe a
f = (Maybe a -> t -> Maybe a) -> Maybe a -> t t -> Maybe a
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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> t -> Maybe a
f t
x) Maybe a
forall a. Maybe a
Nothing

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

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

    mkPEnv :: RType c tv r -> [PVU c tv]
mkPEnv (RAllT RTVU c tv
_ RType c tv r
t r
_) = RType c tv r -> [PVU c tv]
mkPEnv RType c tv r
t
    mkPEnv (RAllP PVU c tv
p RType c tv r
t)   = PVU c tv
pPVU c tv -> [PVU c tv] -> [PVU c tv]
forall a. a -> [a] -> [a]
:RType c tv r -> [PVU c tv]
mkPEnv RType c tv r
t
    mkPEnv RType c tv r
_             = []
    pvType' :: PVar t -> RRType ()
pvType' PVar t
p          = String -> ListNE (RRType ()) -> RRType ()
forall a. (?callStack::CallStack) => String -> ListNE a -> a
Misc.safeHead (PVar t -> String
forall a. PPrint a => a -> String
showpp PVar 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)
t) [PVar (RRType ()) -> RRType ()
forall t. PVar t -> t
pvType PVar (RRType ())
q | PVar (RRType ())
q <- [PVar (RRType ())]
penv, PVar t -> Symbol
forall t. PVar t -> Symbol
pname PVar t
p Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== PVar (RRType ()) -> Symbol
forall t. PVar t -> Symbol
pname PVar (RRType ())
q]


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

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

checkMBody :: (PPrint r, F.Reftable r,SubsTy RTyVar RSort r, F.Reftable (RTProp RTyCon RTyVar r))
           => F.SEnv F.SortedReft
           -> F.TCEmb TyCon
           -> t
           -> SpecType
           -> Def (RRType r) DataCon
           -> Maybe Doc
checkMBody :: SEnv SortedReft
-> TCEmb TyCon
-> t
-> SpecType
-> Def (RRType r) DataCon
-> Maybe Doc
checkMBody SEnv SortedReft
γ TCEmb TyCon
emb t
_ SpecType
sort (Def LocSymbol
m DataCon
c Maybe (RRType r)
_ [(Symbol, Maybe (RRType r))]
bs Body
body) = TCEmb TyCon
-> SpecType -> SEnv SortedReft -> SrcSpan -> Body -> Maybe Doc
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RRType ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnv SortedReft
-> SrcSpan
-> Body
-> Maybe Doc
checkMBody' TCEmb TyCon
emb SpecType
sort SEnv SortedReft
γ' SrcSpan
sp Body
body
  where
    sp :: SrcSpan
sp    = LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan LocSymbol
m
    γ' :: SEnv SortedReft
γ'    = (SEnv SortedReft -> (Symbol, SortedReft) -> SEnv SortedReft)
-> SEnv SortedReft -> [(Symbol, SortedReft)] -> SEnv SortedReft
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
γ [(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 (RRType ()) 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, RRType (), 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
subsTyVars_meet [(RTyVar, RRType (), 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 (Bool -> Bool
not (Bool -> Bool) -> (SpecType -> Bool) -> SpecType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType) (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
trep)
    trep :: RTypeRep RTyCon RTyVar RReft
trep  = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
ct
    su :: [(RTyVar, RRType (), SpecType)]
su    = SpecType -> SpecType -> [(RTyVar, RRType (), 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 (RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
trep) ([SpecType] -> SpecType
forall a. [a] -> a
last [SpecType]
txs)
    txs :: [SpecType]
txs   = ([Symbol], [SpecType], [RReft], SpecType) -> [SpecType]
forall t t1 t2 t3. (t, t1, t2, t3) -> t1
snd4 (([Symbol], [SpecType], [RReft], SpecType) -> [SpecType])
-> ([Symbol], [SpecType], [RReft], SpecType) -> [SpecType]
forall a b. (a -> b) -> a -> b
$ SpecType -> ([Symbol], [SpecType], [RReft], SpecType)
forall t t1 a.
RType t t1 a -> ([Symbol], [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
dataConUserType DataCon
c :: SpecType

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

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


getRewriteErrors :: (Var, Located SpecType) -> [TError t]
getRewriteErrors :: (Var, LocSpecType) -> [TError t]
getRewriteErrors (Var
rw, LocSpecType
t)
  | [(Expr, Expr)] -> 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]
++ if Bool
cannotInstantiate then
        [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"]
        else []
    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 (t :: * -> *) a. Foldable t => t a -> Bool
null [(Expr, Expr)]
allowedRWs
        tyArgs :: [SpecType]
tyArgs = RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep RTyCon RTyVar RReft
tRep
        syms :: [Symbol]
syms   = RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
tRep
        tRep :: RTypeRep RTyCon RTyVar RReft
tRep   = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (SpecType -> RTypeRep RTyCon RTyVar RReft)
-> SpecType -> RTypeRep 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 :: F.Reftable r => RType c tv r -> Bool
isRefined :: 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
F.isTauto r
r
  | Bool
otherwise = Bool
False

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

checkRewrites :: TargetSpec -> Diagnostics
checkRewrites :: TargetSpec -> Diagnostics
checkRewrites TargetSpec
targetSpec = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [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, Hashable 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 :: [Measure SpecType DataCon] -> Diagnostics
checkClassMeasures [Measure SpecType DataCon]
ms = [Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
forall a. Monoid a => a
mempty (([Measure SpecType DataCon] -> Maybe Error)
-> [[Measure SpecType DataCon]] -> [Error]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [Measure SpecType DataCon] -> Maybe Error
forall ty t. [Measure ty DataCon] -> Maybe (TError t)
checkOne [[Measure SpecType DataCon]]
byTyCon)
  where
  byName :: [[Measure SpecType DataCon]]
byName = (Measure SpecType DataCon -> Measure SpecType DataCon -> Bool)
-> [Measure SpecType DataCon] -> [[Measure SpecType DataCon]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
L.groupBy (Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Symbol -> Symbol -> Bool)
-> (Measure SpecType DataCon -> Symbol)
-> Measure SpecType DataCon
-> Measure SpecType DataCon
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (LocSymbol -> Symbol
forall a. Located a -> a
val (LocSymbol -> Symbol)
-> (Measure SpecType DataCon -> LocSymbol)
-> Measure SpecType DataCon
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Measure SpecType DataCon -> LocSymbol
forall ty ctor. Measure ty ctor -> LocSymbol
msName)) [Measure SpecType DataCon]
ms

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

  checkOne :: [Measure 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 [Measure ty DataCon
_]    = Maybe (TError t)
forall a. Maybe a
Nothing
  checkOne (Measure ty DataCon
m:[Measure 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 (LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Measure ty DataCon -> LocSymbol
forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure ty DataCon
m))
                                      (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (LocSymbol -> Symbol
forall a. Located a -> a
val (Measure ty DataCon -> LocSymbol
forall ty ctor. Measure ty ctor -> LocSymbol
msName Measure ty DataCon
m)))
                                      (TyCon -> Doc
forall a. PPrint a => a -> Doc
pprint ((DataCon -> TyCon
dataConTyCon (DataCon -> TyCon)
-> (Measure ty DataCon -> DataCon) -> Measure ty DataCon -> TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Def ty DataCon -> DataCon
forall ty ctor. Def ty ctor -> ctor
ctor (Def ty DataCon -> DataCon)
-> (Measure ty DataCon -> Def ty DataCon)
-> Measure ty DataCon
-> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Def ty DataCon] -> Def ty DataCon
forall a. [a] -> a
head ([Def ty DataCon] -> Def ty DataCon)
-> (Measure ty DataCon -> [Def ty DataCon])
-> Measure ty DataCon
-> Def ty DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Measure ty DataCon -> [Def ty DataCon]
forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns) Measure ty DataCon
m))
                                      (Measure ty DataCon -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Measure ty DataCon -> SrcSpan)
-> [Measure ty DataCon] -> [SrcSpan]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Measure ty DataCon
mMeasure ty DataCon -> [Measure ty DataCon] -> [Measure ty DataCon]
forall a. a -> [a] -> [a]
:[Measure ty DataCon]
ms)))