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

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

import           Prelude hiding (error)
import           Data.List                (delete, nub, partition)
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.Misc                  (fst3)
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 -> SEnvB Symbol Sort -> [QualifierV Symbol]
giQuals TargetInfo
info SEnvB Symbol Sort
lEnv
  =  [Char] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. PPrint a => [Char] -> a -> a
notracepp ([Char]
"GI-QUALS: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SEnvB Symbol Sort -> [Char]
forall a. PPrint a => a -> [Char]
showpp SEnvB Symbol Sort
lEnv)
  ([QualifierV Symbol] -> [QualifierV Symbol])
-> [QualifierV Symbol] -> [QualifierV Symbol]
forall a b. (a -> b) -> a -> b
$  [QualifierV Symbol]
currentSpec
  [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++ Bool -> [QualifierV Symbol] -> [QualifierV Symbol]
forall m. Monoid m => Bool -> m -> m
condNull (TargetInfo -> Bool
forall t. HasConfig t => t -> Bool
useSpcQuals TargetInfo
info) [QualifierV Symbol]
otherSpecs
  [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++ Bool -> [QualifierV Symbol] -> [QualifierV Symbol]
forall m. Monoid m => Bool -> m -> m
condNull (TargetInfo -> Bool
forall t. HasConfig t => t -> Bool
useSigQuals TargetInfo
info) (TargetInfo -> SEnvB Symbol Sort -> [QualifierV Symbol]
sigQualifiers  TargetInfo
info SEnvB Symbol Sort
lEnv)
  [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++ Bool -> [QualifierV Symbol] -> [QualifierV Symbol]
forall m. Monoid m => Bool -> m -> m
condNull (TargetInfo -> Bool
forall t. HasConfig t => t -> Bool
useAlsQuals TargetInfo
info) (TargetInfo -> SEnvB Symbol Sort -> [QualifierV Symbol]
alsQualifiers  TargetInfo
info SEnvB Symbol Sort
lEnv)
  where
    ([QualifierV Symbol]
currentSpec, [QualifierV Symbol]
otherSpecs) = (QualifierV Symbol -> Bool)
-> [QualifierV Symbol]
-> ([QualifierV Symbol], [QualifierV Symbol])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition QualifierV Symbol -> Bool
forall {v}. QualifierV v -> Bool
isQualifierFromCurrentModule (GhcSpecQual -> [QualifierV Symbol]
gsQualifiers (GhcSpecQual -> [QualifierV Symbol])
-> (TargetInfo -> GhcSpecQual) -> TargetInfo -> [QualifierV Symbol]
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 -> [QualifierV Symbol])
-> TargetInfo -> [QualifierV Symbol]
forall a b. (a -> b) -> a -> b
$ TargetInfo
info)
    isQualifierFromCurrentModule :: QualifierV v -> Bool
isQualifierFromCurrentModule QualifierV v
qual =
      ([Char], Line, Line) -> [Char]
forall a b c. (a, b, c) -> a
fst3 (SourcePos -> ([Char], Line, Line)
sourcePosElts (QualifierV v -> SourcePos
forall v. QualifierV v -> SourcePos
qPos QualifierV v
qual)) [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== TargetSrc -> [Char]
giTarget (TargetInfo -> TargetSrc
giSrc TargetInfo
info)


-- --------------------------------------------------------------------------------
-- 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 -> SEnvB Symbol Sort -> [QualifierV Symbol]
alsQualifiers TargetInfo
info SEnvB Symbol Sort
lEnv
  = [ QualifierV Symbol
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
        , QualifierV Symbol
q <- SEnvB Symbol Sort
-> ElabFlags
-> SourcePos
-> TCEmb TyCon
-> SpecType
-> [QualifierV Symbol]
refTypeQuals SEnvB Symbol 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 (QualifierV Symbol -> [QualParam]
forall v. QualifierV v -> [QualParam]
qParams QualifierV Symbol
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
        , SEnvB Symbol Sort -> QualifierV Symbol -> Bool
validQual SEnvB Symbol Sort
lEnv QualifierV Symbol
q
    ]
    where
      ef :: ElabFlags
ef  = TargetInfo -> ElabFlags
forall t. HasConfig t => t -> ElabFlags
elabFlag 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

elabFlag :: (HasConfig t) => t -> FC.ElabFlags
elabFlag :: forall t. HasConfig t => t -> ElabFlags
elabFlag t
info = Bool -> Bool -> ElabFlags
FC.ElabFlags Bool
setBag Bool
False
  where
      setBag :: Bool
setBag = Bool -> (SMTSolver -> Bool) -> Maybe SMTSolver -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False SMTSolver -> Bool
elabSetBag (Maybe SMTSolver -> Bool) -> (t -> Maybe SMTSolver) -> t -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Maybe SMTSolver
smtsolver (Config -> Maybe SMTSolver)
-> (t -> Config) -> t -> Maybe SMTSolver
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Config
forall t. HasConfig t => t -> Config
getConfig (t -> Bool) -> t -> Bool
forall a b. (a -> b) -> a -> b
$ t
info
      elabSetBag :: FC.SMTSolver -> Bool
      elabSetBag :: SMTSolver -> Bool
elabSetBag SMTSolver
FC.Z3    = Bool
True
      elabSetBag SMTSolver
FC.Z3mem = Bool
True
      elabSetBag SMTSolver
_        = Bool
False




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


--------------------------------------------------------------------------------
sigQualifiers :: TargetInfo -> SEnv Sort -> [Qualifier]
--------------------------------------------------------------------------------
sigQualifiers :: TargetInfo -> SEnvB Symbol Sort -> [QualifierV Symbol]
sigQualifiers TargetInfo
info SEnvB Symbol Sort
lEnv
  = [ QualifierV Symbol
q | (Var
x, LocSpecType
t) <- TargetInfo -> [(Var, LocSpecType)]
specBinders TargetInfo
info
        , Bool -> Bool
not (Var
x Var -> HashSet Var -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
`S.member` [Var] -> HashSet Var
forall a. Hashable a => [a] -> HashSet a
S.fromList (TargetInfo -> [Var]
specAxiomVars TargetInfo
info))
        , QualifierV Symbol
q <- SEnvB Symbol Sort
-> ElabFlags
-> SourcePos
-> TCEmb TyCon
-> SpecType
-> [QualifierV Symbol]
refTypeQuals SEnvB Symbol 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 (QualifierV Symbol -> [QualParam]
forall v. QualifierV v -> [QualParam]
qParams QualifierV Symbol
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  = TargetInfo -> ElabFlags
forall t. HasConfig t => t -> ElabFlags
elabFlag 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 :: SEnvB Symbol Sort
-> ElabFlags
-> SourcePos
-> TCEmb TyCon
-> SpecType
-> [QualifierV Symbol]
refTypeQuals SEnvB Symbol Sort
lEnv ElabFlags
ef SourcePos
l TCEmb TyCon
tce SpecType
t0    = SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go SEnvB Symbol Sort
forall b a. SEnvB b a
emptySEnv SpecType
t0
  where
    scrape :: SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
scrape                    = SEnvB Symbol Sort
-> ElabFlags
-> SourcePos
-> TCEmb TyCon
-> SpecType
-> SEnvB Symbol Sort
-> SpecType
-> [QualifierV Symbol]
forall t r.
(PPrint t, IsReft t, ReftBind t ~ Symbol, ReftVar t ~ Symbol,
 SubsTy RTyVar RSort t) =>
SEnvB Symbol Sort
-> ElabFlags
-> SourcePos
-> TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnvB Symbol Sort
-> RRType (UReft t)
-> [QualifierV Symbol]
refTopQuals SEnvB Symbol Sort
lEnv ElabFlags
ef SourcePos
l TCEmb TyCon
tce SpecType
t0
    add :: b
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> SEnvB b Sort
-> SEnvB b Sort
add b
x RTypeBV Symbol Symbol RTyCon RTyVar r
t SEnvB b Sort
γ                 = b -> Sort -> SEnvB b Sort -> SEnvB b Sort
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
insertSEnv b
x (TCEmb TyCon -> RTypeBV Symbol Symbol RTyCon RTyVar r -> Sort
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar RSort r) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce RTypeBV Symbol Symbol RTyCon RTyVar r
t) SEnvB b Sort
γ
    goBind :: Symbol
-> SpecType -> SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
goBind Symbol
x SpecType
t SEnvB Symbol Sort
γ SpecType
t'           = SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go (Symbol -> SpecType -> SEnvB Symbol Sort -> SEnvB Symbol Sort
forall {r} {b}.
(ReftBind r ~ Symbol, ReftVar r ~ Symbol, Hashable b, PPrint r,
 IsReft r, SubsTy RTyVar RSort r) =>
b
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> SEnvB b Sort
-> SEnvB b Sort
add Symbol
x SpecType
t SEnvB Symbol Sort
γ) SpecType
t'
    go :: SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go SEnvB Symbol Sort
γ t :: SpecType
t@(RVar RTyVar
_ UReft (ReftBV Symbol Symbol)
_)         = SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
scrape SEnvB Symbol Sort
γ SpecType
t
    go SEnvB Symbol Sort
γ (RAllT RTVUBV Symbol Symbol RTyCon RTyVar
_ SpecType
t UReft (ReftBV Symbol Symbol)
_)        = SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go SEnvB Symbol Sort
γ SpecType
t
    go SEnvB Symbol Sort
γ (RAllP PVUBV Symbol Symbol RTyCon RTyVar
p SpecType
t)          = SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go (Symbol -> Sort -> SEnvB Symbol Sort -> SEnvB Symbol Sort
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
insertSEnv (PVUBV Symbol Symbol RTyCon RTyVar -> Symbol
forall b v t. PVarBV b v t -> b
pname PVUBV Symbol Symbol RTyCon RTyVar
p) (TCEmb TyCon -> RSort -> Sort
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar RSort r) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce (PVUBV Symbol Symbol RTyCon RTyVar -> RSort
forall r.
(PPrint r, IsReft r) =>
PVUBV Symbol Symbol RTyCon RTyVar -> RRType r
pvarRType PVUBV Symbol Symbol RTyCon RTyVar
p :: RSort)) SEnvB Symbol Sort
γ) SpecType
t
    go SEnvB Symbol Sort
γ t :: SpecType
t@(RAppTy SpecType
t1 SpecType
t2 UReft (ReftBV Symbol Symbol)
_)   = SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go SEnvB Symbol Sort
γ SpecType
t1 [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++ SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go SEnvB Symbol Sort
γ SpecType
t2 [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++ SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
scrape SEnvB Symbol Sort
γ SpecType
t
    go SEnvB Symbol Sort
γ (RFun Symbol
x RFInfo
_ SpecType
t SpecType
t' UReft (ReftBV Symbol Symbol)
_)    = SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go SEnvB Symbol Sort
γ SpecType
t [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++ Symbol
-> SpecType -> SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
goBind Symbol
x SpecType
t SEnvB Symbol Sort
γ SpecType
t'
    go SEnvB Symbol Sort
γ t :: SpecType
t@(RApp RTyCon
c [SpecType]
ts [RTPropBV
   Symbol Symbol RTyCon RTyVar (UReft (ReftBV Symbol Symbol))]
rs UReft (ReftBV Symbol Symbol)
_)   = SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
scrape SEnvB Symbol Sort
γ SpecType
t [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++ (SpecType -> [QualifierV Symbol])
-> [SpecType] -> [QualifierV Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go SEnvB Symbol Sort
γ') [SpecType]
ts [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++ RTyCon
-> SEnvB Symbol Sort
-> [RTPropBV
      Symbol Symbol RTyCon RTyVar (UReft (ReftBV Symbol Symbol))]
-> [QualifierV Symbol]
goRefs RTyCon
c SEnvB Symbol Sort
γ' [RTPropBV
   Symbol Symbol RTyCon RTyVar (UReft (ReftBV Symbol Symbol))]
rs
                                where γ' :: SEnvB Symbol Sort
γ' = Symbol -> SpecType -> SEnvB Symbol Sort -> SEnvB Symbol Sort
forall {r} {b}.
(ReftBind r ~ Symbol, ReftVar r ~ Symbol, Hashable b, PPrint r,
 IsReft r, SubsTy RTyVar RSort r) =>
b
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> SEnvB b Sort
-> SEnvB b Sort
add (SpecType -> ReftBind (UReft (ReftBV Symbol Symbol))
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBind r
rTypeValueVar SpecType
t) SpecType
t SEnvB Symbol Sort
γ
    go SEnvB Symbol Sort
γ (RAllE Symbol
x SpecType
t SpecType
t')       = SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go SEnvB Symbol Sort
γ SpecType
t [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++ Symbol
-> SpecType -> SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
goBind Symbol
x SpecType
t SEnvB Symbol Sort
γ SpecType
t'
    go SEnvB Symbol Sort
γ (REx Symbol
x SpecType
t SpecType
t')         = SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go SEnvB Symbol Sort
γ SpecType
t [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++ Symbol
-> SpecType -> SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
goBind Symbol
x SpecType
t SEnvB Symbol Sort
γ SpecType
t'
    go SEnvB Symbol Sort
_ SpecType
_                    = []
    goRefs :: RTyCon
-> SEnvB Symbol Sort
-> [RTPropBV
      Symbol Symbol RTyCon RTyVar (UReft (ReftBV Symbol Symbol))]
-> [QualifierV Symbol]
goRefs RTyCon
c SEnvB Symbol Sort
g [RTPropBV
   Symbol Symbol RTyCon RTyVar (UReft (ReftBV Symbol Symbol))]
rs             = [[QualifierV Symbol]] -> [QualifierV Symbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[QualifierV Symbol]] -> [QualifierV Symbol])
-> [[QualifierV Symbol]] -> [QualifierV Symbol]
forall a b. (a -> b) -> a -> b
$ (RTPropBV
   Symbol Symbol RTyCon RTyVar (UReft (ReftBV Symbol Symbol))
 -> PVUBV Symbol Symbol RTyCon RTyVar -> [QualifierV Symbol])
-> [RTPropBV
      Symbol Symbol RTyCon RTyVar (UReft (ReftBV Symbol Symbol))]
-> [PVUBV Symbol Symbol RTyCon RTyVar]
-> [[QualifierV Symbol]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SEnvB Symbol Sort
-> RTPropBV
     Symbol Symbol RTyCon RTyVar (UReft (ReftBV Symbol Symbol))
-> PVUBV Symbol Symbol RTyCon RTyVar
-> [QualifierV Symbol]
goRef SEnvB Symbol Sort
g) [RTPropBV
   Symbol Symbol RTyCon RTyVar (UReft (ReftBV Symbol Symbol))]
rs (RTyCon -> [PVUBV Symbol Symbol RTyCon RTyVar]
rTyConPVs RTyCon
c)
    goRef :: SEnvB Symbol Sort
-> RTPropBV
     Symbol Symbol RTyCon RTyVar (UReft (ReftBV Symbol Symbol))
-> PVUBV Symbol Symbol RTyCon RTyVar
-> [QualifierV Symbol]
goRef SEnvB Symbol Sort
_ (RProp [(Symbol, RSort)]
_ (RHole UReft (ReftBV Symbol Symbol)
_)) PVUBV Symbol Symbol RTyCon RTyVar
_ = []
    goRef SEnvB Symbol Sort
g (RProp [(Symbol, RSort)]
s SpecType
t)  PVUBV Symbol Symbol RTyCon RTyVar
_    = SEnvB Symbol Sort -> SpecType -> [QualifierV Symbol]
go (SEnvB Symbol Sort -> [(Symbol, RSort)] -> SEnvB Symbol Sort
insertsSEnv' SEnvB Symbol Sort
g [(Symbol, RSort)]
s) SpecType
t
    insertsSEnv' :: SEnvB Symbol Sort -> [(Symbol, RSort)] -> SEnvB Symbol Sort
insertsSEnv'              = ((Symbol, RSort) -> SEnvB Symbol Sort -> SEnvB Symbol Sort)
-> SEnvB Symbol Sort -> [(Symbol, RSort)] -> SEnvB Symbol 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) SEnvB Symbol Sort
γ -> Symbol -> Sort -> SEnvB Symbol Sort -> SEnvB Symbol Sort
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
insertSEnv Symbol
x (TCEmb TyCon -> RSort -> Sort
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar RSort r) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce RSort
t) SEnvB Symbol Sort
γ)


refTopQuals :: (PPrint t, IsReft t,  ReftBind t ~ Symbol, ReftVar t ~ Symbol, SubsTy RTyVar RSort t)
            => SEnv Sort
            -> ElabFlags
            -> SourcePos
            -> TCEmb TyCon
            -> RType RTyCon RTyVar r
            -> SEnv Sort
            -> RRType (UReft t)
            -> [Qualifier]
refTopQuals :: forall t r.
(PPrint t, IsReft t, ReftBind t ~ Symbol, ReftVar t ~ Symbol,
 SubsTy RTyVar RSort t) =>
SEnvB Symbol Sort
-> ElabFlags
-> SourcePos
-> TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnvB Symbol Sort
-> RRType (UReft t)
-> [QualifierV Symbol]
refTopQuals SEnvB Symbol Sort
lEnv ElabFlags
ef SourcePos
l TCEmb TyCon
tce RType RTyCon RTyVar r
t0 SEnvB Symbol Sort
γ RRType (UReft t)
rrt
  = [ Symbol -> Sort -> Expr -> QualifierV Symbol
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, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar RSort r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft TCEmb TyCon
tce RRType (UReft t)
rrt
                   , Expr
pa                        <- Expr -> [Expr]
forall b v. (Eq b, Eq v) => ExprBV b v -> [ExprBV b v]
conjuncts Expr
ra
                   , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Bool
isHole    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
-> SEnvB Symbol Sort -> Expr -> Reader ElabFlags (Maybe Doc)
forall a.
Checkable a =>
SrcSpan -> SEnvB Symbol Sort -> a -> Reader ElabFlags (Maybe Doc)
checkSorted (SourcePos -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan SourcePos
l) (Symbol -> Sort -> SEnvB Symbol Sort -> SEnvB Symbol Sort
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
insertSEnv Symbol
v Sort
so SEnvB Symbol Sort
γ') Expr
pa) ElabFlags
ef
    ]
    [QualifierV Symbol] -> [QualifierV Symbol] -> [QualifierV Symbol]
forall a. [a] -> [a] -> [a]
++
    [ RSort -> Expr -> QualifierV Symbol
mkP RSort
s Expr
e | let (MkUReft t
_ (Pr [UsedPVarBV Symbol Symbol]
ps)) = UReft t -> Maybe (UReft t) -> UReft t
forall a. a -> Maybe a -> a
fromMaybe (RRType (UReft t) -> UReft t
forall {a} {b}. PPrint a => a -> b
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 b v c tv r. RTypeBV b v c tv r -> Maybe r
stripRTypeBase RRType (UReft t)
rrt
              , PVUBV Symbol Symbol RTyCon RTyVar
p                      <- [PVUBV Symbol Symbol RTyCon RTyVar]
-> UsedPVarBV Symbol Symbol -> PVUBV Symbol Symbol RTyCon RTyVar
forall c tv.
[PVar (RType c tv NoReft)]
-> UsedPVarBV Symbol Symbol -> PVar (RType c tv NoReft)
findPVar (RTypeRepBV Symbol Symbol RTyCon RTyVar r
-> [PVUBV Symbol Symbol RTyCon RTyVar]
forall b v c tv r.
RTypeRepBV b v c tv r
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
ty_preds (RTypeRepBV Symbol Symbol RTyCon RTyVar r
 -> [PVUBV Symbol Symbol RTyCon RTyVar])
-> RTypeRepBV Symbol Symbol RTyCon RTyVar r
-> [PVUBV Symbol Symbol RTyCon RTyVar]
forall a b. (a -> b) -> a -> b
$ RType RTyCon RTyVar r -> RTypeRepBV Symbol Symbol RTyCon RTyVar r
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep RType RTyCon RTyVar r
t0) (UsedPVarBV Symbol Symbol -> PVUBV Symbol Symbol RTyCon RTyVar)
-> [UsedPVarBV Symbol Symbol]
-> [PVUBV Symbol Symbol RTyCon RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVarBV Symbol Symbol]
ps
              , (RSort
s, Symbol
_, Expr
e)              <- PVUBV Symbol Symbol RTyCon RTyVar -> [(RSort, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVUBV Symbol Symbol RTyCon RTyVar
p
    ]
    where
      mkQ' :: Symbol -> Sort -> Expr -> QualifierV Symbol
mkQ'  = SEnvB Symbol Sort
-> SourcePos
-> RType RTyCon RTyVar r
-> SEnvB Symbol Sort
-> Symbol
-> Sort
-> Expr
-> QualifierV Symbol
forall t.
SEnvB Symbol Sort
-> SourcePos
-> t
-> SEnvB Symbol Sort
-> Symbol
-> Sort
-> Expr
-> QualifierV Symbol
mkQual  SEnvB Symbol Sort
lEnv SourcePos
l     RType RTyCon RTyVar r
t0 SEnvB Symbol Sort
γ
      mkP :: RSort -> Expr -> QualifierV Symbol
mkP   = SEnvB Symbol Sort
-> SourcePos
-> TCEmb TyCon
-> RType RTyCon RTyVar r
-> SEnvB Symbol Sort
-> RSort
-> Expr
-> QualifierV Symbol
forall r t.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar RSort r) =>
SEnvB Symbol Sort
-> SourcePos
-> TCEmb TyCon
-> t
-> SEnvB Symbol Sort
-> RRType r
-> Expr
-> QualifierV Symbol
mkPQual SEnvB Symbol Sort
lEnv SourcePos
l TCEmb TyCon
tce RType RTyCon RTyVar r
t0 SEnvB Symbol Sort
γ
      msg :: a -> b
msg a
t = Maybe SrcSpan -> [Char] -> b
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> b) -> [Char] -> b
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
      γ' :: SEnvB Symbol Sort
γ'    = SEnvB Symbol Sort -> SEnvB Symbol Sort -> SEnvB Symbol Sort
forall b a. Eq b => SEnvB b a -> SEnvB b a -> SEnvB b a
unionSEnv' SEnvB Symbol Sort
γ SEnvB Symbol Sort
lEnv

mkPQual :: (PPrint r, IsReft r,  ReftBind r ~ Symbol, ReftVar r ~ Symbol, SubsTy RTyVar RSort r)
        => SEnv Sort
        -> SourcePos
        -> TCEmb TyCon
        -> t
        -> SEnv Sort
        -> RRType r
        -> Expr
        -> Qualifier
mkPQual :: forall r t.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar RSort r) =>
SEnvB Symbol Sort
-> SourcePos
-> TCEmb TyCon
-> t
-> SEnvB Symbol Sort
-> RRType r
-> Expr
-> QualifierV Symbol
mkPQual SEnvB Symbol Sort
lEnv SourcePos
l TCEmb TyCon
tce t
t0 SEnvB Symbol Sort
γ RRType r
t Expr
e = SEnvB Symbol Sort
-> SourcePos
-> t
-> SEnvB Symbol Sort
-> Symbol
-> Sort
-> Expr
-> QualifierV Symbol
forall t.
SEnvB Symbol Sort
-> SourcePos
-> t
-> SEnvB Symbol Sort
-> Symbol
-> Sort
-> Expr
-> QualifierV Symbol
mkQual SEnvB Symbol Sort
lEnv SourcePos
l t
t0 SEnvB Symbol 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, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar RSort r) =>
TCEmb TyCon -> RRType r -> Sort
rTypeSort TCEmb TyCon
tce RRType r
t
    γ' :: SEnvB Symbol Sort
γ'                     = Symbol -> Sort -> SEnvB Symbol Sort -> SEnvB Symbol Sort
forall b a. Hashable b => b -> a -> SEnvB b a -> SEnvB b a
insertSEnv Symbol
v Sort
so SEnvB Symbol Sort
γ
    pa :: Expr
pa                     = Brel -> Expr -> Expr -> Expr
forall b v. Brel -> ExprBV b v -> ExprBV b v -> ExprBV b v
PAtom Brel
Eq (Symbol -> Expr
forall b v. v -> ExprBV b v
EVar Symbol
v) Expr
e

mkQual :: SEnv Sort
       -> SourcePos
       -> t
       -> SEnv Sort
       -> Symbol
       -> Sort
       -> Expr
       -> Qualifier
mkQual :: forall t.
SEnvB Symbol Sort
-> SourcePos
-> t
-> SEnvB Symbol Sort
-> Symbol
-> Sort
-> Expr
-> QualifierV Symbol
mkQual SEnvB Symbol Sort
lEnv SourcePos
l t
_ SEnvB Symbol Sort
γ Symbol
v Sort
so Expr
p   = Symbol
-> [(Symbol, Sort)] -> Expr -> SourcePos -> QualifierV Symbol
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 -> [Variable Expr]
forall a. Subable a => a -> [Variable a]
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
-> SEnvB Symbol Sort
-> SEnvB Symbol Sort
-> Symbol
-> Integer
-> Maybe (Symbol, Sort)
envSort SourcePos
l SEnvB Symbol Sort
lEnv SEnvB Symbol Sort
γ) [Symbol]
xs [Integer
0..]

envSort :: SourcePos -> SEnv Sort -> SEnv Sort -> Symbol -> Integer -> Maybe (Symbol, Sort)
envSort :: SourcePos
-> SEnvB Symbol Sort
-> SEnvB Symbol Sort
-> Symbol
-> Integer
-> Maybe (Symbol, Sort)
envSort SourcePos
l SEnvB Symbol Sort
lEnv SEnvB Symbol Sort
tEnv Symbol
x Integer
i
  | Just Sort
t <- Symbol -> SEnvB Symbol Sort -> Maybe Sort
forall b a. Hashable b => b -> SEnvB b a -> Maybe a
lookupSEnv Symbol
x SEnvB Symbol Sort
tEnv = (Symbol, Sort) -> Maybe (Symbol, Sort)
forall a. a -> Maybe a
Just (Symbol
x, Sort
t)
  | Just Sort
_ <- Symbol -> SEnvB Symbol Sort -> Maybe Sort
forall b a. Hashable b => b -> SEnvB b a -> Maybe a
lookupSEnv Symbol
x SEnvB Symbol 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