{-# 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           Control.Monad.Reader

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.Errors
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.UX.Config
import Language.Fixpoint.Types.Config (ElabFlags)


--------------------------------------------------------------------------------
giQuals :: TargetInfo -> SEnv Sort -> [Qualifier]
--------------------------------------------------------------------------------
giQuals :: TargetInfo -> SEnv Sort -> [Qualifier]
giQuals TargetInfo
info SEnv Sort
lEnv
  =  [Char] -> [Qualifier] -> [Qualifier]
forall a. PPrint a => [Char] -> a -> a
notracepp ([Char]
"GI-QUALS: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SEnv Sort -> [Char]
forall a. PPrint a => a -> [Char]
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 :: forall t. HasConfig t => 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
useSpcQuals :: (HasConfig t) => t -> Bool
useSpcQuals :: forall t. HasConfig t => 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 :: forall t. HasConfig t => 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 :: forall t. HasConfig t => 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 :: forall t. HasConfig t => t -> Bool
useQuals = (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 :: forall t. HasConfig t => 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
-> ElabFlags -> SourcePos -> TCEmb TyCon -> SpecType -> [Qualifier]
refTypeQuals SEnv Sort
lEnv ElabFlags
ef (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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Qualifier -> [QualParam]
forall v. QualifierV v -> [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
      ef :: ElabFlags
ef  = ElabFlags
-> (SMTSolver -> ElabFlags) -> Maybe SMTSolver -> ElabFlags
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> ElabFlags
FC.ElabFlags Bool
False) SMTSolver -> ElabFlags
FC.solverFlags (Maybe SMTSolver -> ElabFlags)
-> (TargetInfo -> Maybe SMTSolver) -> TargetInfo -> ElabFlags
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Maybe SMTSolver
smtsolver (Config -> Maybe SMTSolver)
-> (TargetInfo -> Config) -> TargetInfo -> Maybe SMTSolver
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig (TargetInfo -> ElabFlags) -> TargetInfo -> ElabFlags
forall a b. (a -> b) -> a -> b
$ TargetInfo
info
      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
forall v. QualifierV v -> ExprV v
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
        , Bool -> Bool
not (Var
x Var -> HashSet Var -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` [Var] -> HashSet Var
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (TargetInfo -> [Var]
specAxiomVars TargetInfo
info))
        , Qualifier
q <- SEnv Sort
-> ElabFlags -> SourcePos -> TCEmb TyCon -> SpecType -> [Qualifier]
refTypeQuals SEnv Sort
lEnv ElabFlags
ef (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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Qualifier -> [QualParam]
forall v. QualifierV v -> [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
      ef :: ElabFlags
ef  = ElabFlags
-> (SMTSolver -> ElabFlags) -> Maybe SMTSolver -> ElabFlags
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> ElabFlags
FC.ElabFlags Bool
False) SMTSolver -> ElabFlags
FC.solverFlags (Maybe SMTSolver -> ElabFlags)
-> (TargetInfo -> Maybe SMTSolver) -> TargetInfo -> ElabFlags
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Maybe SMTSolver
smtsolver (Config -> Maybe SMTSolver)
-> (TargetInfo -> Config) -> TargetInfo -> Maybe SMTSolver
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetInfo -> Config
forall t. HasConfig t => t -> Config
getConfig (TargetInfo -> ElabFlags) -> TargetInfo -> ElabFlags
forall a b. (a -> b) -> a -> b
$ TargetInfo
info
      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

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 -> ElabFlags -> SourcePos -> TCEmb TyCon -> SpecType -> [Qualifier]
--------------------------------------------------------------------------------
refTypeQuals :: SEnv Sort
-> ElabFlags -> SourcePos -> TCEmb TyCon -> SpecType -> [Qualifier]
refTypeQuals SEnv Sort
lEnv ElabFlags
ef 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
-> ElabFlags
-> 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
-> ElabFlags
-> SourcePos
-> TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnv Sort
-> RRType (UReft t)
-> [Qualifier]
refTopQuals SEnv Sort
lEnv ElabFlags
ef 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 (ReftV Symbol)
_)         = SEnv Sort -> SpecType -> [Qualifier]
scrape SEnv Sort
γ SpecType
t
    go SEnv Sort
γ (RAllT RTVar RTyVar RSort
_ SpecType
t UReft (ReftV Symbol)
_)        = SEnv Sort -> SpecType -> [Qualifier]
go SEnv Sort
γ SpecType
t
    go SEnv Sort
γ (RAllP PVUV Symbol 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 (PVUV Symbol RTyCon RTyVar -> Symbol
forall v t. PVarV v t -> Symbol
pname PVUV Symbol 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 (PVUV Symbol RTyCon RTyVar -> RSort
forall r.
(PPrint r, Reftable r) =>
PVUV Symbol RTyCon RTyVar -> RRType r
pvarRType PVUV Symbol RTyCon RTyVar
p :: RSort)) SEnv Sort
γ) SpecType
t
    go SEnv Sort
γ t :: SpecType
t@(RAppTy SpecType
t1 SpecType
t2 UReft (ReftV Symbol)
_)   = 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 RFInfo
_ SpecType
t SpecType
t' UReft (ReftV Symbol)
_)    = 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 (ReftV Symbol))]
rs UReft (ReftV Symbol)
_)   = 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 (ReftV Symbol))]
-> [Qualifier]
goRefs RTyCon
c SEnv Sort
γ' [RTProp RTyCon RTyVar (UReft (ReftV Symbol))]
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 (ReftV Symbol))]
-> [Qualifier]
goRefs RTyCon
c SEnv Sort
g [RTProp RTyCon RTyVar (UReft (ReftV Symbol))]
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 (ReftV Symbol))
 -> PVUV Symbol RTyCon RTyVar -> [Qualifier])
-> [RTProp RTyCon RTyVar (UReft (ReftV Symbol))]
-> [PVUV Symbol RTyCon RTyVar]
-> [[Qualifier]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SEnv Sort
-> RTProp RTyCon RTyVar (UReft (ReftV Symbol))
-> PVUV Symbol RTyCon RTyVar
-> [Qualifier]
goRef SEnv Sort
g) [RTProp RTyCon RTyVar (UReft (ReftV Symbol))]
rs (RTyCon -> [PVUV Symbol RTyCon RTyVar]
rTyConPVs RTyCon
c)
    goRef :: SEnv Sort
-> RTProp RTyCon RTyVar (UReft (ReftV Symbol))
-> PVUV Symbol RTyCon RTyVar
-> [Qualifier]
goRef SEnv Sort
_ (RProp [(Symbol, RSort)]
_ (RHole UReft (ReftV Symbol)
_)) PVUV Symbol RTyCon RTyVar
_ = []
    goRef SEnv Sort
g (RProp [(Symbol, RSort)]
s SpecType
t)  PVUV Symbol 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 a b. (a -> b -> b) -> b -> [a] -> b
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
            -> ElabFlags
            -> 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
-> ElabFlags
-> SourcePos
-> TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnv Sort
-> RRType (UReft t)
-> [Qualifier]
refTopQuals SEnv Sort
lEnv ElabFlags
ef 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))) = 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)
rrt
                   , Expr
pa                        <- Expr -> [Expr]
forall v. Eq v => ExprV v -> [ExprV v]
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
                   , [Char] -> Bool -> Bool
forall a. PPrint a => [Char] -> a -> a
notracepp ([Char]
"refTopQuals: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. PPrint a => a -> [Char]
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
$ Reader ElabFlags (Maybe Doc) -> ElabFlags -> Maybe Doc
forall r a. Reader r a -> r -> a
runReader (SrcSpan -> SEnv Sort -> Expr -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan -> SEnv Sort -> a -> Reader ElabFlags (Maybe Doc)
checkSorted (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) ElabFlags
ef
    ]
    [Qualifier] -> [Qualifier] -> [Qualifier]
forall a. [a] -> [a] -> [a]
++
    [ RSort -> Expr -> Qualifier
mkP RSort
s Expr
e | let (MkUReft t
_ (Pr [UsedPVarV Symbol]
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)
rrt) (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)
rrt
              , PVUV Symbol RTyCon RTyVar
p                      <- [PVUV Symbol RTyCon RTyVar]
-> UsedPVarV Symbol -> PVUV Symbol RTyCon RTyVar
forall c tv.
[PVar (RType c tv ())] -> UsedPVarV Symbol -> PVar (RType c tv ())
findPVar (RTypeRepV Symbol RTyCon RTyVar r -> [PVUV Symbol RTyCon RTyVar]
forall v c tv r. RTypeRepV v c tv r -> [PVarV v (RTypeV v c tv ())]
ty_preds (RTypeRepV Symbol RTyCon RTyVar r -> [PVUV Symbol RTyCon RTyVar])
-> RTypeRepV Symbol RTyCon RTyVar r -> [PVUV Symbol RTyCon RTyVar]
forall a b. (a -> b) -> a -> b
$ RType RTyCon RTyVar r -> RTypeRepV Symbol RTyCon RTyVar r
forall v c tv r. RTypeV v c tv r -> RTypeRepV v c tv r
toRTypeRep RType RTyCon RTyVar r
t0) (UsedPVarV Symbol -> PVUV Symbol RTyCon RTyVar)
-> [UsedPVarV Symbol] -> [PVUV Symbol RTyCon RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVarV Symbol]
ps
              , (RSort
s, Symbol
_, Expr
e)              <- PVUV Symbol RTyCon RTyVar -> [(RSort, Symbol, Expr)]
forall v t. PVarV v t -> [(t, Symbol, ExprV v)]
pargs PVUV Symbol 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 -> [Char] -> a
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"Qualifier.refTopQuals: no typebase" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. PPrint a => a -> [Char]
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 :: 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 = 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
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
Eq (Symbol -> Expr
forall v. v -> ExprV v
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) (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             = [Char] -> Sort -> Sort
forall a. [Char] -> a -> a
trace [Char]
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 :: [Char]
msg            = [Char]
"Unknown symbol in qualifier: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
x