{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE FlexibleContexts      #-}

module Language.Haskell.Liquid.Constraint.Qualifier
  ( giQuals
  , useSpcQuals
  )
  where

import           Prelude hiding (error)
import           Data.List                (delete, nub)
import           Data.Maybe               (isJust, catMaybes, fromMaybe, isNothing)
import qualified Data.HashSet        as S
import qualified Data.HashMap.Strict as M
import           Debug.Trace (trace)
import           Language.Fixpoint.Types                  hiding (panic, mkQual)
import qualified Language.Fixpoint.Types.Config as FC
import           Language.Fixpoint.SortCheck
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.GHC.Misc         (getSourcePos)
import           Language.Haskell.Liquid.Misc             (condNull)
import           Language.Haskell.Liquid.Types.PredType
import           Liquid.GHC.API hiding (Expr, mkQual, panic)

import           Language.Haskell.Liquid.Types


--------------------------------------------------------------------------------
giQuals :: TargetInfo -> SEnv Sort -> [Qualifier]
--------------------------------------------------------------------------------
giQuals :: TargetInfo -> SEnv Sort -> [Qualifier]
giQuals TargetInfo
info SEnv Sort
lEnv
  =  forall a. PPrint a => [Char] -> a -> a
notracepp ([Char]
"GI-QUALS: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp SEnv Sort
lEnv)
  forall a b. (a -> b) -> a -> b
$  forall m. Monoid m => Bool -> m -> m
condNull (forall t. HasConfig t => t -> Bool
useSpcQuals TargetInfo
info) (GhcSpecQual -> [Qualifier]
gsQualifiers forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecQual
gsQual forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec forall a b. (a -> b) -> a -> b
$ TargetInfo
info)
  forall a. [a] -> [a] -> [a]
++ forall m. Monoid m => Bool -> m -> m
condNull (forall t. HasConfig t => t -> Bool
useSigQuals TargetInfo
info) (TargetInfo -> SEnv Sort -> [Qualifier]
sigQualifiers  TargetInfo
info SEnv Sort
lEnv)
  forall a. [a] -> [a] -> [a]
++ forall m. Monoid m => Bool -> m -> m
condNull (forall t. HasConfig t => t -> Bool
useAlsQuals TargetInfo
info) (TargetInfo -> SEnv Sort -> [Qualifier]
alsQualifiers  TargetInfo
info SEnv Sort
lEnv)

-- --------------------------------------------------------------------------------
-- qualifiers :: GhcInfo -> SEnv Sort -> [Qualifier]
-- --------------------------------------------------------------------------------
-- qualifiers info env = spcQs ++ genQs
  -- where
    -- spcQs           = gsQualifiers spc
    -- genQs           = specificationQualifiers info env
    -- n               = maxParams (getConfig spc)
    -- spc             = spec info

maxQualParams :: (HasConfig t) => t -> Int
maxQualParams :: forall t. HasConfig t => t -> Int
maxQualParams = Config -> Int
maxParams forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. HasConfig t => t -> Config
getConfig

-- | Use explicitly given qualifiers .spec or source (.hs, .lhs) files
useSpcQuals :: (HasConfig t) => t -> Bool
useSpcQuals :: forall t. HasConfig t => t -> Bool
useSpcQuals t
i = forall t. HasConfig t => t -> Bool
useQuals t
i Bool -> Bool -> Bool
&& Bool -> Bool
not (forall t. HasConfig t => t -> Bool
useAlsQuals t
i)

-- | Scrape qualifiers from function signatures (incr :: x:Int -> {v:Int | v > x})
useSigQuals :: (HasConfig t) => t -> Bool
useSigQuals :: forall t. HasConfig t => t -> Bool
useSigQuals t
i = forall t. HasConfig t => t -> Bool
useQuals t
i Bool -> Bool -> Bool
&& Bool -> Bool
not (forall t. HasConfig t => t -> Bool
useAlsQuals t
i)

-- | Scrape qualifiers from refinement type aliases (type Nat = {v:Int | 0 <= 0})
useAlsQuals :: (HasConfig t) => t -> Bool
useAlsQuals :: forall t. HasConfig t => t -> Bool
useAlsQuals t
i = forall t. HasConfig t => t -> Bool
useQuals t
i Bool -> Bool -> Bool
&& t
i forall t. HasConfig t => t -> (Config -> Bool) -> Bool
`hasOpt` forall t. HasConfig t => t -> Bool
higherOrderFlag Bool -> Bool -> Bool
&& Bool -> Bool
not (forall t. HasConfig t => t -> Bool
needQuals t
i)

useQuals :: (HasConfig t) => t -> Bool
useQuals :: forall t. HasConfig t => t -> Bool
useQuals = (Eliminate
FC.All forall a. Eq a => a -> a -> Bool
/=) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Eliminate
eliminate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. HasConfig t => t -> Config
getConfig

needQuals :: (HasConfig t) => t -> Bool
needQuals :: forall t. HasConfig t => t -> Bool
needQuals = (Eliminate
FC.None forall a. Eq a => a -> a -> Bool
== ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Eliminate
eliminate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. HasConfig t => t -> Config
getConfig

--------------------------------------------------------------------------------
alsQualifiers :: TargetInfo -> SEnv Sort -> [Qualifier]
--------------------------------------------------------------------------------
alsQualifiers :: TargetInfo -> SEnv Sort -> [Qualifier]
alsQualifiers TargetInfo
info SEnv Sort
lEnv
  = [ Qualifier
q | Located SpecRTAlias
a <- GhcSpecQual -> [Located SpecRTAlias]
gsRTAliases forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecQual
gsQual forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec forall a b. (a -> b) -> a -> b
$ TargetInfo
info
        , Qualifier
q <- SEnv Sort -> SourcePos -> TCEmb TyCon -> SpecType -> [Qualifier]
refTypeQuals SEnv Sort
lEnv (forall a. Located a -> SourcePos
loc Located SpecRTAlias
a) TCEmb TyCon
tce (forall x a. RTAlias x a -> a
rtBody (forall a. Located a -> a
val Located SpecRTAlias
a))
        , forall (t :: * -> *) a. Foldable t => t a -> Int
length (Qualifier -> [QualParam]
qParams Qualifier
q) forall a. Ord a => a -> a -> Bool
<= Int
k forall a. Num a => a -> a -> a
+ Int
1
        , SEnv Sort -> Qualifier -> Bool
validQual SEnv Sort
lEnv Qualifier
q
    ]
    where
      k :: Int
k   = forall t. HasConfig t => t -> Int
maxQualParams TargetInfo
info
      tce :: TCEmb TyCon
tce = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecNames
gsName forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec forall a b. (a -> b) -> a -> b
$ TargetInfo
info

validQual :: SEnv Sort -> Qualifier -> Bool
validQual :: SEnv Sort -> Qualifier -> Bool
validQual SEnv Sort
lEnv Qualifier
q = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ SrcSpan -> SEnv Sort -> Expr -> Maybe Sort
checkSortExpr (forall a. Loc a => a -> SrcSpan
srcSpan Qualifier
q) SEnv Sort
env (Qualifier -> Expr
qBody Qualifier
q)
  where
    env :: SEnv Sort
env          = forall a. SEnv a -> HashMap Symbol a -> SEnv a
unionSEnv SEnv Sort
lEnv HashMap Symbol Sort
qEnv
    qEnv :: HashMap Symbol Sort
qEnv         = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (Qualifier -> [(Symbol, Sort)]
qualBinds Qualifier
q)


--------------------------------------------------------------------------------
sigQualifiers :: TargetInfo -> SEnv Sort -> [Qualifier]
--------------------------------------------------------------------------------
sigQualifiers :: TargetInfo -> SEnv Sort -> [Qualifier]
sigQualifiers TargetInfo
info SEnv Sort
lEnv
  = [ Qualifier
q | (Var
x, LocSpecType
t) <- TargetInfo -> [(Var, LocSpecType)]
specBinders TargetInfo
info
        , Var
x forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Var
qbs
        , Qualifier
q <- SEnv Sort -> SourcePos -> TCEmb TyCon -> SpecType -> [Qualifier]
refTypeQuals SEnv Sort
lEnv (forall a. NamedThing a => a -> SourcePos
getSourcePos Var
x) TCEmb TyCon
tce (forall a. Located a -> a
val LocSpecType
t)
        -- NOTE: large qualifiers are VERY expensive, so we only mine
        -- qualifiers up to a given size, controlled with --max-params
        , forall (t :: * -> *) a. Foldable t => t a -> Int
length (Qualifier -> [QualParam]
qParams Qualifier
q) forall a. Ord a => a -> a -> Bool
<= Int
k forall a. Num a => a -> a -> a
+ Int
1
    ]
    where
      k :: Int
k   = forall t. HasConfig t => t -> Int
maxQualParams TargetInfo
info
      tce :: TCEmb TyCon
tce = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecNames
gsName forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec forall a b. (a -> b) -> a -> b
$ TargetInfo
info
      qbs :: HashSet Var
qbs = TargetInfo -> HashSet Var
qualifyingBinders TargetInfo
info

qualifyingBinders :: TargetInfo -> S.HashSet Var
qualifyingBinders :: TargetInfo -> HashSet Var
qualifyingBinders TargetInfo
info = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference HashSet Var
sTake HashSet Var
sDrop
  where
    sTake :: HashSet Var
sTake              = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ TargetSrc -> [Var]
giDefVars TargetSrc
src forall a. [a] -> [a] -> [a]
++ TargetSrc -> [Var]
giUseVars TargetSrc
src forall a. [a] -> [a] -> [a]
++ Config -> TargetSrc -> [Var]
scrapeVars Config
cfg TargetSrc
src
    sDrop :: HashSet Var
sDrop              = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ TargetInfo -> [Var]
specAxiomVars TargetInfo
info
    cfg :: Config
cfg                = forall t. HasConfig t => t -> Config
getConfig TargetInfo
info
    src :: TargetSrc
src                = TargetInfo -> TargetSrc
giSrc     TargetInfo
info

-- NOTE: this mines extra, useful qualifiers but causes
-- a significant increase in running time, so we hide it
-- behind `--scrape-imports` and `--scrape-used-imports`
scrapeVars :: Config -> TargetSrc -> [Var]
scrapeVars :: Config -> TargetSrc -> [Var]
scrapeVars Config
cfg TargetSrc
src
  | Config
cfg forall t. HasConfig t => t -> (Config -> Bool) -> Bool
`hasOpt` Config -> Bool
scrapeUsedImports = TargetSrc -> [Var]
giUseVars TargetSrc
src
  | Config
cfg forall t. HasConfig t => t -> (Config -> Bool) -> Bool
`hasOpt` Config -> Bool
scrapeImports     = TargetSrc -> [Var]
giImpVars TargetSrc
src
  | Bool
otherwise                      = []

specBinders :: TargetInfo -> [(Var, LocSpecType)]
specBinders :: TargetInfo -> [(Var, LocSpecType)]
specBinders TargetInfo
info = forall a. Monoid a => [a] -> a
mconcat
  [ GhcSpecSig -> [(Var, LocSpecType)]
gsTySigs  (TargetSpec -> GhcSpecSig
gsSig  TargetSpec
sp)
  , GhcSpecSig -> [(Var, LocSpecType)]
gsAsmSigs (TargetSpec -> GhcSpecSig
gsSig  TargetSpec
sp)
  , GhcSpecSig -> [(Var, LocSpecType)]
gsRefSigs (TargetSpec -> GhcSpecSig
gsSig  TargetSpec
sp)
  , GhcSpecData -> [(Var, LocSpecType)]
gsCtors   (TargetSpec -> GhcSpecData
gsData TargetSpec
sp)
  , if TargetInfo
info forall t. HasConfig t => t -> (Config -> Bool) -> Bool
`hasOpt` Config -> Bool
scrapeInternals then GhcSpecSig -> [(Var, LocSpecType)]
gsInSigs (TargetSpec -> GhcSpecSig
gsSig TargetSpec
sp) else []
  ]
  where
    sp :: TargetSpec
sp  = TargetInfo -> TargetSpec
giSpec TargetInfo
info

specAxiomVars :: TargetInfo -> [Var]
specAxiomVars :: TargetInfo -> [Var]
specAxiomVars =  GhcSpecRefl -> [Var]
gsReflects forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecRefl
gsRefl forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec

-- GRAVEYARD: scraping quals from imports kills the system with too much crap
-- specificationQualifiers info = {- filter okQual -} qs
--   where
--     qs                       = concatMap refTypeQualifiers ts
--     refTypeQualifiers        = refTypeQuals $ tcEmbeds spc
--     ts                       = val <$> t1s ++ t2s
--     t1s                      = [t | (x, t) <- tySigs spc, x `S.member` definedVars]
--     t2s                      = [] -- [t | (_, t) <- ctor spc                            ]
--     definedVars              = S.fromList $ defVars info
--     spc                      = spec info
--
-- okQual                       = not . any isPred . map snd . q_params
--   where
--     isPred (FApp tc _)       = tc == stringFTycon "Pred"
--     isPred _                 = False


-- TODO: rewrite using foldReft'
--------------------------------------------------------------------------------
refTypeQuals :: SEnv Sort -> SourcePos -> TCEmb TyCon -> SpecType -> [Qualifier]
--------------------------------------------------------------------------------
refTypeQuals :: SEnv Sort -> SourcePos -> TCEmb TyCon -> SpecType -> [Qualifier]
refTypeQuals SEnv Sort
lEnv SourcePos
l TCEmb TyCon
tce SpecType
t0    = SEnv Sort -> SpecType -> [Qualifier]
go forall a. SEnv a
emptySEnv SpecType
t0
  where
    scrape :: SEnv Sort -> SpecType -> [Qualifier]
scrape                    = forall t r.
(PPrint t, Reftable t, SubsTy RTyVar RSort t,
 Reftable (RTProp RTyCon RTyVar (UReft t))) =>
SEnv Sort
-> SourcePos
-> TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnv Sort
-> RRType (UReft t)
-> [Qualifier]
refTopQuals SEnv Sort
lEnv SourcePos
l TCEmb TyCon
tce SpecType
t0
    add :: Symbol -> RRType r -> SEnv Sort -> SEnv Sort
add Symbol
x RRType r
t SEnv Sort
γ                 = forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
x (forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce RRType r
t) SEnv Sort
γ
    goBind :: Symbol -> SpecType -> SEnv Sort -> SpecType -> [Qualifier]
goBind Symbol
x SpecType
t SEnv Sort
γ SpecType
t'           = SEnv Sort -> SpecType -> [Qualifier]
go (forall {r}.
(PPrint r, SubsTy RTyVar RSort r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
Symbol -> RRType r -> SEnv Sort -> SEnv Sort
add Symbol
x SpecType
t SEnv Sort
γ) SpecType
t'
    go :: SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ t :: SpecType
t@(RVar RTyVar
_ UReft Reft
_)         = SEnv Sort -> SpecType -> [Qualifier]
scrape SEnv Sort
γ SpecType
t
    go SEnv Sort
γ (RAllT RTVU RTyCon RTyVar
_ SpecType
t UReft Reft
_)        = SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ SpecType
t
    go SEnv Sort
γ (RAllP PVU RTyCon RTyVar
p SpecType
t)          = SEnv Sort -> SpecType -> [Qualifier]
go (forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv (forall t. PVar t -> Symbol
pname PVU RTyCon RTyVar
p) (forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce (forall r. (PPrint r, Reftable r) => PVU RTyCon RTyVar -> RRType r
pvarRType PVU RTyCon RTyVar
p :: RSort)) SEnv Sort
γ) SpecType
t
    go SEnv Sort
γ t :: SpecType
t@(RAppTy SpecType
t1 SpecType
t2 UReft Reft
_)   = SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ SpecType
t1 forall a. [a] -> [a] -> [a]
++ SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ SpecType
t2 forall a. [a] -> [a] -> [a]
++ SEnv Sort -> SpecType -> [Qualifier]
scrape SEnv Sort
γ SpecType
t
    go SEnv Sort
γ (RFun Symbol
x RFInfo
_ SpecType
t SpecType
t' UReft Reft
_)    = SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ SpecType
t forall a. [a] -> [a] -> [a]
++ Symbol -> SpecType -> SEnv Sort -> SpecType -> [Qualifier]
goBind Symbol
x SpecType
t SEnv Sort
γ SpecType
t'
    go SEnv Sort
γ t :: SpecType
t@(RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar (UReft Reft)]
rs UReft Reft
_)   = SEnv Sort -> SpecType -> [Qualifier]
scrape SEnv Sort
γ SpecType
t forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ') [SpecType]
ts forall a. [a] -> [a] -> [a]
++ RTyCon
-> SEnv Sort -> [RTProp RTyCon RTyVar (UReft Reft)] -> [Qualifier]
goRefs RTyCon
c SEnv Sort
γ' [RTProp RTyCon RTyVar (UReft Reft)]
rs
                                where γ' :: SEnv Sort
γ' = forall {r}.
(PPrint r, SubsTy RTyVar RSort r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
Symbol -> RRType r -> SEnv Sort -> SEnv Sort
add (forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar SpecType
t) SpecType
t SEnv Sort
γ
    go SEnv Sort
γ (RAllE Symbol
x SpecType
t SpecType
t')       = SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ SpecType
t forall a. [a] -> [a] -> [a]
++ Symbol -> SpecType -> SEnv Sort -> SpecType -> [Qualifier]
goBind Symbol
x SpecType
t SEnv Sort
γ SpecType
t'
    go SEnv Sort
γ (REx Symbol
x SpecType
t SpecType
t')         = SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ SpecType
t forall a. [a] -> [a] -> [a]
++ Symbol -> SpecType -> SEnv Sort -> SpecType -> [Qualifier]
goBind Symbol
x SpecType
t SEnv Sort
γ SpecType
t'
    go SEnv Sort
_ SpecType
_                    = []
    goRefs :: RTyCon
-> SEnv Sort -> [RTProp RTyCon RTyVar (UReft Reft)] -> [Qualifier]
goRefs RTyCon
c SEnv Sort
g [RTProp RTyCon RTyVar (UReft Reft)]
rs             = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SEnv Sort
-> RTProp RTyCon RTyVar (UReft Reft)
-> PVU RTyCon RTyVar
-> [Qualifier]
goRef SEnv Sort
g) [RTProp RTyCon RTyVar (UReft Reft)]
rs (RTyCon -> [PVU RTyCon RTyVar]
rTyConPVs RTyCon
c)
    goRef :: SEnv Sort
-> RTProp RTyCon RTyVar (UReft Reft)
-> PVU RTyCon RTyVar
-> [Qualifier]
goRef SEnv Sort
_ (RProp [(Symbol, RSort)]
_ (RHole UReft Reft
_)) PVU RTyCon RTyVar
_ = []
    goRef SEnv Sort
g (RProp [(Symbol, RSort)]
s SpecType
t)  PVU RTyCon RTyVar
_    = SEnv Sort -> SpecType -> [Qualifier]
go (SEnv Sort -> [(Symbol, RSort)] -> SEnv Sort
insertsSEnv' SEnv Sort
g [(Symbol, RSort)]
s) SpecType
t
    insertsSEnv' :: SEnv Sort -> [(Symbol, RSort)] -> SEnv Sort
insertsSEnv'              = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Symbol
x, RSort
t) SEnv Sort
γ -> forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
x (forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce RSort
t) SEnv Sort
γ)


refTopQuals :: (PPrint t, Reftable t, SubsTy RTyVar RSort t, Reftable (RTProp RTyCon RTyVar (UReft t)))
            => SEnv Sort
            -> SourcePos
            -> TCEmb TyCon
            -> RType RTyCon RTyVar r
            -> SEnv Sort
            -> RRType (UReft t)
            -> [Qualifier]
refTopQuals :: forall t r.
(PPrint t, Reftable t, SubsTy RTyVar RSort t,
 Reftable (RTProp RTyCon RTyVar (UReft t))) =>
SEnv Sort
-> SourcePos
-> TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnv Sort
-> RRType (UReft t)
-> [Qualifier]
refTopQuals SEnv Sort
lEnv SourcePos
l TCEmb TyCon
tce RType RTyCon RTyVar r
t0 SEnv Sort
γ RRType (UReft t)
rrt
  = [ Symbol -> Sort -> Expr -> Qualifier
mkQ' Symbol
v Sort
so Expr
pa  | let (RR Sort
so (Reft (Symbol
v, Expr
ra))) = forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
tce RRType (UReft t)
rrt
                   , Expr
pa                        <- Expr -> [Expr]
conjuncts Expr
ra
                   , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Expr -> Bool
isHole    Expr
pa
                   , Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. HasGradual a => a -> Bool
isGradual Expr
pa
                   , forall a. PPrint a => [Char] -> a -> a
notracepp ([Char]
"refTopQuals: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Expr
pa)
                     forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ forall a. Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc
checkSorted (forall a. Loc a => a -> SrcSpan
srcSpan SourcePos
l) (forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
v Sort
so SEnv Sort
γ') Expr
pa
    ]
    forall a. [a] -> [a] -> [a]
++
    [ RSort -> Expr -> Qualifier
mkP RSort
s Expr
e | let (MkUReft t
_ (Pr [UsedPVar]
ps)) = forall a. a -> Maybe a -> a
fromMaybe (forall {a} {a}. PPrint a => a -> a
msg RRType (UReft t)
rrt) forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RRType (UReft t)
rrt
              , PVU RTyCon RTyVar
p                      <- forall c tv.
[PVar (RType c tv ())] -> UsedPVar -> PVar (RType c tv ())
findPVar (forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RType RTyCon RTyVar r
t0) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
ps
              , (RSort
s, Symbol
_, Expr
e)              <- forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVU RTyCon RTyVar
p
    ]
    where
      mkQ' :: Symbol -> Sort -> Expr -> Qualifier
mkQ'  = forall t.
SEnv Sort
-> SourcePos
-> t
-> SEnv Sort
-> Symbol
-> Sort
-> Expr
-> Qualifier
mkQual  SEnv Sort
lEnv SourcePos
l     RType RTyCon RTyVar r
t0 SEnv Sort
γ
      mkP :: RSort -> Expr -> Qualifier
mkP   = forall r t.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
SEnv Sort
-> SourcePos
-> TCEmb TyCon
-> t
-> SEnv Sort
-> RRType r
-> Expr
-> Qualifier
mkPQual SEnv Sort
lEnv SourcePos
l TCEmb TyCon
tce RType RTyCon RTyVar r
t0 SEnv Sort
γ
      msg :: a -> a
msg a
t = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ [Char]
"Qualifier.refTopQuals: no typebase" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp a
t
      γ' :: SEnv Sort
γ'    = forall a. SEnv a -> SEnv a -> SEnv a
unionSEnv' SEnv Sort
γ SEnv Sort
lEnv

mkPQual :: (PPrint r, Reftable r, SubsTy RTyVar RSort r, Reftable (RTProp RTyCon RTyVar r))
        => SEnv Sort
        -> SourcePos
        -> TCEmb TyCon
        -> t
        -> SEnv Sort
        -> RRType r
        -> Expr
        -> Qualifier
mkPQual :: forall r t.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
SEnv Sort
-> SourcePos
-> TCEmb TyCon
-> t
-> SEnv Sort
-> RRType r
-> Expr
-> Qualifier
mkPQual SEnv Sort
lEnv SourcePos
l TCEmb TyCon
tce t
t0 SEnv Sort
γ RRType r
t Expr
e = forall t.
SEnv Sort
-> SourcePos
-> t
-> SEnv Sort
-> Symbol
-> Sort
-> Expr
-> Qualifier
mkQual SEnv Sort
lEnv SourcePos
l t
t0 SEnv Sort
γ' Symbol
v Sort
so Expr
pa
  where
    v :: Symbol
v                      = Symbol
"vv"
    so :: Sort
so                     = forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce RRType r
t
    γ' :: SEnv Sort
γ'                     = forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
v Sort
so SEnv Sort
γ
    pa :: Expr
pa                     = Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq (Symbol -> Expr
EVar Symbol
v) Expr
e

mkQual :: SEnv Sort
       -> SourcePos
       -> t
       -> SEnv Sort
       -> Symbol
       -> Sort
       -> Expr
       -> Qualifier
mkQual :: forall t.
SEnv Sort
-> SourcePos
-> t
-> SEnv Sort
-> Symbol
-> Sort
-> Expr
-> Qualifier
mkQual SEnv Sort
lEnv SourcePos
l t
_ SEnv Sort
γ Symbol
v Sort
so Expr
p   = Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
mkQ Symbol
"Auto" ((Symbol
v, Sort
so) forall a. a -> [a] -> [a]
: [(Symbol, Sort)]
xts) Expr
p SourcePos
l
  where
    xs :: [Symbol]
xs   = forall a. Eq a => a -> [a] -> [a]
delete Symbol
v forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a. Subable a => a -> [Symbol]
syms Expr
p
    xts :: [(Symbol, Sort)]
xts  = forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SourcePos
-> SEnv Sort
-> SEnv Sort
-> Symbol
-> Integer
-> Maybe (Symbol, Sort)
envSort SourcePos
l SEnv Sort
lEnv SEnv Sort
γ) [Symbol]
xs [Integer
0..]

envSort :: SourcePos -> SEnv Sort -> SEnv Sort -> Symbol -> Integer -> Maybe (Symbol, Sort)
envSort :: SourcePos
-> SEnv Sort
-> SEnv Sort
-> Symbol
-> Integer
-> Maybe (Symbol, Sort)
envSort SourcePos
l SEnv Sort
lEnv SEnv Sort
tEnv Symbol
x Integer
i
  | Just Sort
t <- forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x SEnv Sort
tEnv = forall a. a -> Maybe a
Just (Symbol
x, Sort
t)
  | Just Sort
_ <- forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x SEnv Sort
lEnv = forall a. Maybe a
Nothing
  | Bool
otherwise                   = forall a. a -> Maybe a
Just (Symbol
x, Sort
ai)
  where
    ai :: Sort
ai             = forall a. [Char] -> a -> a
trace [Char]
msg forall a b. (a -> b) -> a -> b
$ LocSymbol -> Sort
fObj forall a b. (a -> b) -> a -> b
$ forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l forall a b. (a -> b) -> a -> b
$ Symbol -> Integer -> Symbol
tempSymbol Symbol
"LHTV" Integer
i
    msg :: [Char]
msg            = [Char]
"Unknown symbol in qualifier: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Symbol
x