{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE ViewPatterns          #-}
{-# 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           TyCon
import           Var (Var)
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           Language.Haskell.Liquid.Types


--------------------------------------------------------------------------------
giQuals :: TargetInfo -> SEnv Sort -> [Qualifier]
--------------------------------------------------------------------------------
giQuals :: TargetInfo -> SEnv Sort -> [Qualifier]
giQuals TargetInfo
info SEnv Sort
lEnv
  =  String -> [Qualifier] -> [Qualifier]
forall a. PPrint a => String -> a -> a
notracepp (String
"GI-QUALS: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SEnv Sort -> String
forall a. PPrint a => a -> String
showpp SEnv Sort
lEnv)
  ([Qualifier] -> [Qualifier]) -> [Qualifier] -> [Qualifier]
forall a b. (a -> b) -> a -> b
$  Bool -> [Qualifier] -> [Qualifier]
forall m. Monoid m => Bool -> m -> m
condNull (TargetInfo -> Bool
forall t. HasConfig t => t -> Bool
useSpcQuals TargetInfo
info) (GhcSpecQual -> [Qualifier]
gsQualifiers (GhcSpecQual -> [Qualifier])
-> (TargetInfo -> GhcSpecQual) -> TargetInfo -> [Qualifier]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecQual
gsQual (TargetSpec -> GhcSpecQual)
-> (TargetInfo -> TargetSpec) -> TargetInfo -> GhcSpecQual
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec (TargetInfo -> [Qualifier]) -> TargetInfo -> [Qualifier]
forall a b. (a -> b) -> a -> b
$ TargetInfo
info)
  [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. [a] -> [a] -> [a]
++ Bool -> [Qualifier] -> [Qualifier]
forall m. Monoid m => Bool -> m -> m
condNull (TargetInfo -> Bool
forall t. HasConfig t => t -> Bool
useSigQuals TargetInfo
info) (TargetInfo -> SEnv Sort -> [Qualifier]
sigQualifiers  TargetInfo
info SEnv Sort
lEnv)
  [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. [a] -> [a] -> [a]
++ Bool -> [Qualifier] -> [Qualifier]
forall m. Monoid m => Bool -> m -> m
condNull (TargetInfo -> Bool
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 :: t -> Int
maxQualParams = Config -> Int
maxParams (Config -> Int) -> (t -> Config) -> t -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Config
forall t. HasConfig t => t -> Config
getConfig

-- | Use explicitly given qualifiers .spec or source (.hs, .lhs) files
useSpcQuals :: (HasConfig t) => t -> Bool
useSpcQuals :: t -> Bool
useSpcQuals t
i = t -> Bool
forall t. HasConfig t => t -> Bool
useQuals t
i Bool -> Bool -> Bool
&& Bool -> Bool
not (t -> Bool
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 :: t -> Bool
useSigQuals t
i = t -> Bool
forall t. HasConfig t => t -> Bool
useQuals t
i Bool -> Bool -> Bool
&& Bool -> Bool
not (t -> Bool
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 :: t -> Bool
useAlsQuals t
i = t -> Bool
forall t. HasConfig t => t -> Bool
useQuals t
i Bool -> Bool -> Bool
&& t
i t -> (Config -> Bool) -> Bool
forall t. HasConfig t => t -> (Config -> Bool) -> Bool
`hasOpt` Config -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag Bool -> Bool -> Bool
&& Bool -> Bool
not (t -> Bool
forall t. HasConfig t => t -> Bool
needQuals t
i)

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

needQuals :: (HasConfig t) => t -> Bool
needQuals :: t -> Bool
needQuals = (Eliminate
FC.None Eliminate -> Eliminate -> Bool
forall a. Eq a => a -> a -> Bool
== ) (Eliminate -> Bool) -> (t -> Eliminate) -> t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Eliminate
eliminate (Config -> Eliminate) -> (t -> Config) -> t -> Eliminate
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Config
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 (GhcSpecQual -> [Located SpecRTAlias])
-> (TargetInfo -> GhcSpecQual)
-> TargetInfo
-> [Located SpecRTAlias]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecQual
gsQual (TargetSpec -> GhcSpecQual)
-> (TargetInfo -> TargetSpec) -> TargetInfo -> GhcSpecQual
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec (TargetInfo -> [Located SpecRTAlias])
-> TargetInfo -> [Located SpecRTAlias]
forall a b. (a -> b) -> a -> b
$ TargetInfo
info
        , Qualifier
q <- SEnv Sort -> SourcePos -> TCEmb TyCon -> SpecType -> [Qualifier]
refTypeQuals SEnv Sort
lEnv (Located SpecRTAlias -> SourcePos
forall a. Located a -> SourcePos
loc Located SpecRTAlias
a) TCEmb TyCon
tce (SpecRTAlias -> SpecType
forall x a. RTAlias x a -> a
rtBody (Located SpecRTAlias -> SpecRTAlias
forall a. Located a -> a
val Located SpecRTAlias
a))
        , [QualParam] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Qualifier -> [QualParam]
qParams Qualifier
q) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
        , SEnv Sort -> Qualifier -> Bool
validQual SEnv Sort
lEnv Qualifier
q
    ]
    where
      k :: Int
k   = TargetInfo -> Int
forall t. HasConfig t => t -> Int
maxQualParams TargetInfo
info
      tce :: TCEmb TyCon
tce = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (GhcSpecNames -> TCEmb TyCon)
-> (TargetInfo -> GhcSpecNames) -> TargetInfo -> TCEmb TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecNames
gsName (TargetSpec -> GhcSpecNames)
-> (TargetInfo -> TargetSpec) -> TargetInfo -> GhcSpecNames
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec (TargetInfo -> TCEmb TyCon) -> TargetInfo -> TCEmb TyCon
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 = Maybe Sort -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Sort -> Bool) -> Maybe Sort -> Bool
forall a b. (a -> b) -> a -> b
$ SrcSpan -> SEnv Sort -> Expr -> Maybe Sort
checkSortExpr (Qualifier -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan Qualifier
q) SEnv Sort
env (Qualifier -> Expr
qBody Qualifier
q)
  where
    env :: SEnv Sort
env          = SEnv Sort -> HashMap Symbol Sort -> SEnv Sort
forall a. SEnv a -> HashMap Symbol a -> SEnv a
unionSEnv SEnv Sort
lEnv HashMap Symbol Sort
qEnv
    qEnv :: HashMap Symbol Sort
qEnv         = [(Symbol, Sort)] -> HashMap Symbol Sort
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 Var -> HashSet Var -> Bool
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 (Var -> SourcePos
forall a. NamedThing a => a -> SourcePos
getSourcePos Var
x) TCEmb TyCon
tce (LocSpecType -> SpecType
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
        , [QualParam] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Qualifier -> [QualParam]
qParams Qualifier
q) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
    ]
    where
      k :: Int
k   = TargetInfo -> Int
forall t. HasConfig t => t -> Int
maxQualParams TargetInfo
info
      tce :: TCEmb TyCon
tce = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (GhcSpecNames -> TCEmb TyCon)
-> (TargetInfo -> GhcSpecNames) -> TargetInfo -> TCEmb TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecNames
gsName (TargetSpec -> GhcSpecNames)
-> (TargetInfo -> TargetSpec) -> TargetInfo -> GhcSpecNames
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> TargetSpec
giSpec (TargetInfo -> TCEmb TyCon) -> TargetInfo -> TCEmb TyCon
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 = HashSet Var -> HashSet Var -> HashSet Var
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              = [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
$ TargetSrc -> [Var]
giDefVars TargetSrc
src [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ TargetSrc -> [Var]
giUseVars TargetSrc
src [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ Config -> TargetSrc -> [Var]
scrapeVars Config
cfg TargetSrc
src 
    sDrop :: HashSet Var
sDrop              = [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
$ TargetInfo -> [Var]
specAxiomVars TargetInfo
info
    cfg :: Config
cfg                = TargetInfo -> Config
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 Config -> (Config -> Bool) -> Bool
forall t. HasConfig t => t -> (Config -> Bool) -> Bool
`hasOpt` Config -> Bool
scrapeUsedImports = TargetSrc -> [Var]
giUseVars TargetSrc
src 
  | Config
cfg Config -> (Config -> Bool) -> Bool
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 = [[(Var, LocSpecType)]] -> [(Var, LocSpecType)]
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 TargetInfo -> (Config -> Bool) -> Bool
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 (GhcSpecRefl -> [Var])
-> (TargetInfo -> GhcSpecRefl) -> TargetInfo -> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetSpec -> GhcSpecRefl
gsRefl (TargetSpec -> GhcSpecRefl)
-> (TargetInfo -> TargetSpec) -> TargetInfo -> GhcSpecRefl
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 SEnv Sort
forall a. SEnv a
emptySEnv SpecType
t0
  where
    scrape :: SEnv Sort -> SpecType -> [Qualifier]
scrape                    = SEnv Sort
-> SourcePos
-> TCEmb TyCon
-> SpecType
-> SEnv Sort
-> SpecType
-> [Qualifier]
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
γ                 = Symbol -> Sort -> SEnv Sort -> SEnv Sort
forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
x (TCEmb TyCon -> RRType r -> Sort
forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
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 (Symbol -> SpecType -> SEnv Sort -> 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 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 (Symbol -> Sort -> SEnv Sort -> SEnv Sort
forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv (PVU RTyCon RTyVar -> Symbol
forall t. PVar t -> Symbol
pname PVU RTyCon RTyVar
p) (TCEmb TyCon -> RSort -> Sort
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 -> Sort) -> RSort -> Sort
forall a b. (a -> b) -> a -> b
$ (PVU RTyCon RTyVar -> RSort
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 [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. [a] -> [a] -> [a]
++ SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ SpecType
t2 [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. [a] -> [a] -> [a]
++ SEnv Sort -> SpecType -> [Qualifier]
scrape SEnv Sort
γ SpecType
t
    go SEnv Sort
γ (RFun Symbol
x SpecType
t SpecType
t' UReft Reft
_)      = SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ SpecType
t [Qualifier] -> [Qualifier] -> [Qualifier]
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 [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. [a] -> [a] -> [a]
++ (SpecType -> [Qualifier]) -> [SpecType] -> [Qualifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ') [SpecType]
ts [Qualifier] -> [Qualifier] -> [Qualifier]
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
γ' = Symbol -> SpecType -> SEnv Sort -> 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 (SpecType -> Symbol
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 [Qualifier] -> [Qualifier] -> [Qualifier]
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 [Qualifier] -> [Qualifier] -> [Qualifier]
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             = [[Qualifier]] -> [Qualifier]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Qualifier]] -> [Qualifier]) -> [[Qualifier]] -> [Qualifier]
forall a b. (a -> b) -> a -> b
$ (RTProp RTyCon RTyVar (UReft Reft)
 -> PVU RTyCon RTyVar -> [Qualifier])
-> [RTProp RTyCon RTyVar (UReft Reft)]
-> [PVU RTyCon RTyVar]
-> [[Qualifier]]
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               = ((Symbol, RSort) -> SEnv Sort -> SEnv Sort)
-> SEnv Sort -> [(Symbol, RSort)] -> SEnv Sort
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Symbol
x, RSort
t) SEnv Sort
γ -> Symbol -> Sort -> SEnv Sort -> SEnv Sort
forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
x (TCEmb TyCon -> RSort -> Sort
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 :: 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)
t
  = [ Symbol -> Sort -> Expr -> Qualifier
mkQ Symbol
v Sort
so Expr
pa  | let (RR Sort
so (Reft (Symbol
v, Expr
ra))) = TCEmb TyCon -> RRType (UReft t) -> SortedReft
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)
t
                   , Expr
pa                        <- Expr -> [Expr]
conjuncts Expr
ra
                   , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Bool
isHole    Expr
pa
                   , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Bool
forall a. HasGradual a => a -> Bool
isGradual Expr
pa
                   , String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
notracepp (String
"refTopQuals: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
pa) 
                     (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe Doc -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe Doc -> Bool) -> Maybe Doc -> Bool
forall a b. (a -> b) -> a -> b
$ SrcSpan -> SEnv Sort -> Expr -> Maybe Doc
forall a. Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc
checkSorted (SourcePos -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan SourcePos
l) (Symbol -> Sort -> SEnv Sort -> SEnv Sort
forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
v Sort
so SEnv Sort
γ') Expr
pa
    ]
    [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. [a] -> [a] -> [a]
++
    [ RSort -> Expr -> Qualifier
mkP RSort
s Expr
e | let (MkUReft t
_ (Pr [UsedPVar]
ps)) = UReft t -> Maybe (UReft t) -> UReft t
forall a. a -> Maybe a -> a
fromMaybe (RRType (UReft t) -> UReft t
forall a a. PPrint a => a -> a
msg RRType (UReft t)
t) (Maybe (UReft t) -> UReft t) -> Maybe (UReft t) -> UReft t
forall a b. (a -> b) -> a -> b
$ RRType (UReft t) -> Maybe (UReft t)
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RRType (UReft t)
t
              , PVU RTyCon RTyVar
p                      <- [PVU RTyCon RTyVar] -> UsedPVar -> PVU RTyCon RTyVar
forall c tv.
[PVar (RType c tv ())] -> UsedPVar -> PVar (RType c tv ())
findPVar (RTypeRep RTyCon RTyVar r -> [PVU RTyCon RTyVar]
forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds (RTypeRep RTyCon RTyVar r -> [PVU RTyCon RTyVar])
-> RTypeRep RTyCon RTyVar r -> [PVU RTyCon RTyVar]
forall a b. (a -> b) -> a -> b
$ 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
t0) (UsedPVar -> PVU RTyCon RTyVar)
-> [UsedPVar] -> [PVU RTyCon RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
ps
              , (RSort
s, Symbol
_, Expr
e)              <- PVU RTyCon RTyVar -> [(RSort, Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVU RTyCon RTyVar
p
    ]
    where
      mkQ :: Symbol -> Sort -> Expr -> Qualifier
mkQ   = SEnv Sort
-> SourcePos
-> RType RTyCon RTyVar r
-> SEnv Sort
-> Symbol
-> Sort
-> Expr
-> Qualifier
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   = SEnv Sort
-> SourcePos
-> TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnv Sort
-> RSort
-> Expr
-> Qualifier
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 = Maybe SrcSpan -> String -> a
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Qualifier.refTopQuals: no typebase" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. PPrint a => a -> String
showpp a
t
      γ' :: SEnv Sort
γ'    = SEnv Sort -> SEnv Sort -> 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 :: 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 = SEnv Sort
-> SourcePos
-> t
-> SEnv Sort
-> Symbol
-> Sort
-> Expr
-> Qualifier
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                     = TCEmb TyCon -> RRType r -> Sort
forall r.
(PPrint r, Reftable r, SubsTy RTyVar RSort r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce RRType r
t
    γ' :: SEnv Sort
γ'                     = Symbol -> Sort -> SEnv Sort -> 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 :: 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) (Symbol, Sort) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. a -> [a] -> [a]
: [(Symbol, Sort)]
xts) Expr
p SourcePos
l
  where
    xs :: [Symbol]
xs   = Symbol -> [Symbol] -> [Symbol]
forall a. Eq a => a -> [a] -> [a]
delete Symbol
v ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms Expr
p
    xts :: [(Symbol, Sort)]
xts  = [Maybe (Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Symbol, Sort)] -> [(Symbol, Sort)])
-> [Maybe (Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ (Symbol -> Integer -> Maybe (Symbol, Sort))
-> [Symbol] -> [Integer] -> [Maybe (Symbol, Sort)]
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 <- Symbol -> SEnv Sort -> Maybe Sort
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x SEnv Sort
tEnv = (Symbol, Sort) -> Maybe (Symbol, Sort)
forall a. a -> Maybe a
Just (Symbol
x, Sort
t)
  | Just Sort
_ <- Symbol -> SEnv Sort -> Maybe Sort
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv Symbol
x SEnv Sort
lEnv = Maybe (Symbol, Sort)
forall a. Maybe a
Nothing
  | Bool
otherwise                   = (Symbol, Sort) -> Maybe (Symbol, Sort)
forall a. a -> Maybe a
Just (Symbol
x, Sort
ai)
  where
    ai :: Sort
ai             = String -> Sort -> Sort
forall a. String -> a -> a
trace String
msg (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Sort
fObj (LocSymbol -> Sort) -> LocSymbol -> Sort
forall a b. (a -> b) -> a -> b
$ SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l (Symbol -> LocSymbol) -> Symbol -> LocSymbol
forall a b. (a -> b) -> a -> b
$ Symbol -> Integer -> Symbol
tempSymbol Symbol
"LHTV" Integer
i
    msg :: String
msg            = String
"Unknown symbol in qualifier: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show Symbol
x