-- | This module has the code for applying refinement (and) type aliases
--   and the pipeline for "cooking" a @BareType@ into a @SpecType@.
--   TODO: _only_ export `makeRTEnv`, `cookSpecType` and maybe `qualifyExpand`...

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

module Language.Haskell.Liquid.Bare.Expand
  ( -- * Create alias expansion environment
    makeRTEnv

    -- * Expand
  , Expand(expand)

    -- * Converting BareType to SpecType
  , cookSpecType
  , cookSpecTypeE
  , specExpandType

    -- * Re-exported for data-constructors
  , plugHoles
  ) where

import Prelude hiding (error)
import Data.Graph hiding (Graph)
import Data.Maybe

import           Control.Monad
import           Control.Monad.Identity
import           Control.Monad.State
import           Data.Bifunctor (second)
import           Data.Functor ((<&>))
import qualified Control.Exception         as Ex
import qualified Data.HashMap.Strict       as M
import qualified Data.HashSet              as HS
import qualified Data.Char                 as Char
import qualified Data.List                 as L
import qualified Text.PrettyPrint.HughesPJ as PJ

import qualified Language.Fixpoint.Types               as F
-- import qualified Language.Fixpoint.Types.Visitor       as F
import qualified Language.Fixpoint.Misc                as Misc
import           Language.Fixpoint.Types (Expr, ExprV, ExprBV(..), SourcePos) -- , Symbol, symbol)
import qualified Language.Haskell.Liquid.GHC.Misc      as GM
import qualified Liquid.GHC.API       as Ghc
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.DataDecl
import           Language.Haskell.Liquid.Types.Names
import qualified Language.Haskell.Liquid.Types.RefType as RT
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.LHNameResolution (symbolToLHName)
import qualified Language.Haskell.Liquid.Misc          as Misc
import qualified Language.Haskell.Liquid.Measure       as Ms
import           Language.Haskell.Liquid.Name.LogicNameEnv (LogicNameEnv(..))
import qualified Language.Haskell.Liquid.Bare.Resolve  as Bare
import qualified Language.Haskell.Liquid.Bare.Types    as Bare
import qualified Language.Haskell.Liquid.Bare.Plugged  as Bare
import           Language.Haskell.Liquid.UX.Config
import qualified Text.Printf                           as Printf

--------------------------------------------------------------------------------
-- | `makeRTEnv` initializes the env needed to `expand` refinements and types,
--   that is, the below needs to be called *before* we use `Expand.expand`
--------------------------------------------------------------------------------
makeRTEnv
  :: LogicNameEnv
  -> ModName
  -> Ms.BareSpec
  -> [(ModName, Ms.BareSpec)]
  -> BareRTEnv
--------------------------------------------------------------------------------
makeRTEnv :: LogicNameEnv
-> ModName
-> BareSpec
-> [(ModName, BareSpec)]
-> RTEnv Symbol BareType
makeRTEnv LogicNameEnv
lenv ModName
modName BareSpec
mySpec [(ModName, BareSpec)]
dependencySpecs
          = RTEnv Symbol BareType -> RTEnv Symbol BareType
renameRTArgs (RTEnv Symbol BareType -> RTEnv Symbol BareType)
-> RTEnv Symbol BareType -> RTEnv Symbol BareType
forall a b. (a -> b) -> a -> b
$ [RTAlias Symbol BareType]
-> RTEnv Symbol BareType -> RTEnv Symbol BareType
makeRTAliases [RTAlias Symbol BareType]
tAs (RTEnv Symbol BareType -> RTEnv Symbol BareType)
-> RTEnv Symbol BareType -> RTEnv Symbol BareType
forall a b. (a -> b) -> a -> b
$ [RTAlias Symbol (ExprV LHName)] -> RTEnv Symbol BareType
makeREAliases [RTAlias Symbol (ExprV LHName)]
eAs
  where
    tAs :: [RTAlias Symbol BareType]
tAs     = ((ModName, BareSpec) -> [RTAlias Symbol BareType])
-> [(ModName, BareSpec)] -> [RTAlias Symbol BareType]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BareSpec -> [RTAlias Symbol BareType]
forall lname ty.
Spec lname ty -> [RTAlias Symbol (BareTypeV lname)]
Ms.aliases (BareSpec -> [RTAlias Symbol BareType])
-> ((ModName, BareSpec) -> BareSpec)
-> (ModName, BareSpec)
-> [RTAlias Symbol BareType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, BareSpec) -> BareSpec
forall a b. (a, b) -> b
snd) [(ModName, BareSpec)]
specs
    eAs :: [RTAlias Symbol (ExprV LHName)]
eAs     = ((ModName, BareSpec) -> [RTAlias Symbol (ExprV LHName)])
-> [(ModName, BareSpec)] -> [RTAlias Symbol (ExprV LHName)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BareSpec -> [RTAlias Symbol (ExprV LHName)]
getLHNameExprAliases (BareSpec -> [RTAlias Symbol (ExprV LHName)])
-> ((ModName, BareSpec) -> BareSpec)
-> (ModName, BareSpec)
-> [RTAlias Symbol (ExprV LHName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, BareSpec) -> BareSpec
forall a b. (a, b) -> b
snd) [(ModName, BareSpec)]
specs
    specs :: [(ModName, BareSpec)]
specs = (ModName
modName, BareSpec
mySpec) (ModName, BareSpec)
-> [(ModName, BareSpec)] -> [(ModName, BareSpec)]
forall a. a -> [a] -> [a]
: [(ModName, BareSpec)]
dependencySpecs

    -- | 'Symbol's are temporarily converted to 'LHName's in expression alias
    -- bodies to use the same lookup and expansion procedure for both
    -- kinds of aliases. Implemented as an specialization of
    -- 'toBareSpecLHName' for the expression aliases field.
    getLHNameExprAliases:: Ms.BareSpec -> [RTAlias F.Symbol (ExprV LHName)]
    getLHNameExprAliases :: BareSpec -> [RTAlias Symbol (ExprV LHName)]
getLHNameExprAliases = Identity [RTAlias Symbol (ExprV LHName)]
-> [RTAlias Symbol (ExprV LHName)]
forall a. Identity a -> a
runIdentity (Identity [RTAlias Symbol (ExprV LHName)]
 -> [RTAlias Symbol (ExprV LHName)])
-> (BareSpec -> Identity [RTAlias Symbol (ExprV LHName)])
-> BareSpec
-> [RTAlias Symbol (ExprV LHName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpec -> Identity [RTAlias Symbol (ExprV LHName)]
go

    go :: Ms.BareSpec -> Identity [RTAlias F.Symbol (ExprV LHName)]
    go :: BareSpec -> Identity [RTAlias Symbol (ExprV LHName)]
go = (RTAlias Symbol (ExprBV Symbol Symbol)
 -> Identity (RTAlias Symbol (ExprV LHName)))
-> [RTAlias Symbol (ExprBV Symbol Symbol)]
-> Identity [RTAlias Symbol (ExprV LHName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (([Symbol] -> ExprBV Symbol Symbol -> Identity (ExprV LHName))
-> RTAlias Symbol (ExprBV Symbol Symbol)
-> Identity (RTAlias Symbol (ExprV LHName))
forall (m :: * -> *) r0 r1.
Monad m =>
([Symbol] -> r0 -> m r1)
-> RTAlias Symbol r0 -> m (RTAlias Symbol r1)
emapRTAlias (\[Symbol]
e -> ([Symbol] -> Symbol -> Identity LHName)
-> ExprBV Symbol Symbol -> Identity (ExprV LHName)
forall (m :: * -> *) b v v'.
(Monad m, Hashable b) =>
([b] -> v -> m v') -> ExprBV b v -> m (ExprBV b v')
emapExprVM ([Symbol] -> Symbol -> Identity LHName
symToLHName ([Symbol] -> Symbol -> Identity LHName)
-> ([Symbol] -> [Symbol]) -> [Symbol] -> Symbol -> Identity LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ [Symbol]
e)))) ([RTAlias Symbol (ExprBV Symbol Symbol)]
 -> Identity [RTAlias Symbol (ExprV LHName)])
-> (BareSpec -> [RTAlias Symbol (ExprBV Symbol Symbol)])
-> BareSpec
-> Identity [RTAlias Symbol (ExprV LHName)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareSpec -> [RTAlias Symbol (ExprBV Symbol Symbol)]
forall lname ty. Spec lname ty -> [RTAlias Symbol (ExprV lname)]
ealiases

    symToLHName :: [Symbol] -> Symbol -> Identity LHName
symToLHName = [Char]
-> LogicNameEnv
-> HashSet Symbol
-> [Symbol]
-> Symbol
-> Identity LHName
symbolToLHName [Char]
"makeRTEnv" LogicNameEnv
lenv HashSet Symbol
unhandledNames
    unhandledNames :: HashSet Symbol
unhandledNames = [Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
HS.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ([(Symbol, Sort)] -> [Symbol]) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ BareSpec -> [(Symbol, Sort)]
forall lname ty. Spec lname ty -> [(lname, Sort)]
expSigs BareSpec
mySpec

-- | We apply @renameRTArgs@ *after* expanding each alias-definition, to
--   ensure that the substitutions work properly (i.e. don't miss expressions
--   hidden inside @RExprArg@ or as strange type parameters.
renameRTArgs :: BareRTEnv -> BareRTEnv
renameRTArgs :: RTEnv Symbol BareType -> RTEnv Symbol BareType
renameRTArgs RTEnv Symbol BareType
rte = RTE
  { typeAliases :: HashMap LHName (RTAlias Symbol BareType)
typeAliases = (RTAlias Symbol BareType -> RTAlias Symbol BareType)
-> HashMap LHName (RTAlias Symbol BareType)
-> HashMap LHName (RTAlias Symbol BareType)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (RTAlias Symbol BareType -> RTAlias Symbol BareType
renameTys (RTAlias Symbol BareType -> RTAlias Symbol BareType)
-> (RTAlias Symbol BareType -> RTAlias Symbol BareType)
-> RTAlias Symbol BareType
-> RTAlias Symbol BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol BareType -> RTAlias Symbol BareType
renameVV (RTAlias Symbol BareType -> RTAlias Symbol BareType)
-> (RTAlias Symbol BareType -> RTAlias Symbol BareType)
-> RTAlias Symbol BareType
-> RTAlias Symbol BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol BareType -> RTAlias Symbol BareType
forall a x.
(PPrint a, Subable a, Variable a ~ Symbol) =>
RTAlias x a -> RTAlias x a
renameRTVArgs) (RTEnv Symbol BareType -> HashMap LHName (RTAlias Symbol BareType)
forall tv t. RTEnv tv t -> HashMap LHName (RTAlias tv t)
typeAliases RTEnv Symbol BareType
rte)
  , exprAliases :: HashMap LHName (RTAlias Symbol (ExprBV Symbol Symbol))
exprAliases = (RTAlias Symbol (ExprBV Symbol Symbol)
 -> RTAlias Symbol (ExprBV Symbol Symbol))
-> HashMap LHName (RTAlias Symbol (ExprBV Symbol Symbol))
-> HashMap LHName (RTAlias Symbol (ExprBV Symbol Symbol))
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map RTAlias Symbol (ExprBV Symbol Symbol)
-> RTAlias Symbol (ExprBV Symbol Symbol)
forall a x.
(PPrint a, Subable a, Variable a ~ Symbol) =>
RTAlias x a -> RTAlias x a
renameRTVArgs (RTEnv Symbol BareType
-> HashMap LHName (RTAlias Symbol (ExprBV Symbol Symbol))
forall tv t.
RTEnv tv t
-> HashMap LHName (RTAlias Symbol (ExprBV Symbol Symbol))
exprAliases RTEnv Symbol BareType
rte)
  }

-- | Recursively expands expression aliases by unfolding the definitions of all
--   inner aliases and adds them to the environment.
--   Innermost aliases are unfolded and added first, and an error is thrown if
--   cyclic dependencies are detected.
makeREAliases :: [RTAlias F.Symbol (F.ExprV LHName)] -> BareRTEnv
makeREAliases :: [RTAlias Symbol (ExprV LHName)] -> RTEnv Symbol BareType
makeREAliases = (AliasTable Symbol (ExprV LHName) -> ExprV LHName -> [LHName])
-> (RTEnv Symbol BareType
    -> RTAlias Symbol (ExprV LHName) -> RTEnv Symbol BareType)
-> RTEnv Symbol BareType
-> [RTAlias Symbol (ExprV LHName)]
-> RTEnv Symbol BareType
forall t x thing.
PPrint t =>
(AliasTable x t -> t -> [LHName])
-> (thing -> RTAlias x t -> thing)
-> thing
-> [RTAlias x t]
-> thing
graphExpand AliasTable Symbol (ExprV LHName) -> ExprV LHName -> [LHName]
forall x t. AliasTable x t -> ExprV LHName -> [LHName]
buildExprEdges RTEnv Symbol BareType
-> RTAlias Symbol (ExprV LHName) -> RTEnv Symbol BareType
f RTEnv Symbol BareType
forall a. Monoid a => a
mempty
  where
    f :: RTEnv Symbol BareType
-> RTAlias Symbol (ExprV LHName) -> RTEnv Symbol BareType
f RTEnv Symbol BareType
rtEnv RTAlias Symbol (ExprV LHName)
xt = RTEnv Symbol BareType
-> RTAlias Symbol (ExprBV Symbol Symbol) -> RTEnv Symbol BareType
forall x t.
RTEnv x t -> RTAlias Symbol (ExprBV Symbol Symbol) -> RTEnv x t
setREAlias RTEnv Symbol BareType
rtEnv (RTEnv Symbol BareType
-> SourcePos
-> RTAlias Symbol (ExprBV Symbol Symbol)
-> RTAlias Symbol (ExprBV Symbol Symbol)
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv (Located LHName -> SourcePos
forall a. Located a -> SourcePos
F.loc (Located LHName -> SourcePos)
-> (RTAlias Symbol (ExprV LHName) -> Located LHName)
-> RTAlias Symbol (ExprV LHName)
-> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol (ExprV LHName) -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias Symbol (ExprV LHName) -> SourcePos)
-> RTAlias Symbol (ExprV LHName) -> SourcePos
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol (ExprV LHName)
xt) (RTAlias Symbol (ExprV LHName)
-> RTAlias Symbol (ExprBV Symbol Symbol)
lhNametoSymbol RTAlias Symbol (ExprV LHName)
xt))
    -- Expression aliases 'LHName's are transformed back to 'Symbol's for the
    -- actual expansion to take place and to be stored in the environment.
    lhNametoSymbol :: RTAlias F.Symbol (F.ExprV LHName) -> RTAlias F.Symbol Expr
    lhNametoSymbol :: RTAlias Symbol (ExprV LHName)
-> RTAlias Symbol (ExprBV Symbol Symbol)
lhNametoSymbol RTAlias Symbol (ExprV LHName)
xt = ((ExprV LHName -> ExprBV Symbol Symbol)
-> RTAlias Symbol (ExprV LHName)
-> RTAlias Symbol (ExprBV Symbol Symbol)
forall a b. (a -> b) -> RTAlias Symbol a -> RTAlias Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ExprV LHName -> ExprBV Symbol Symbol)
 -> RTAlias Symbol (ExprV LHName)
 -> RTAlias Symbol (ExprBV Symbol Symbol))
-> (ExprV LHName -> ExprBV Symbol Symbol)
-> RTAlias Symbol (ExprV LHName)
-> RTAlias Symbol (ExprBV Symbol Symbol)
forall a b. (a -> b) -> a -> b
$ (LHName -> Symbol) -> ExprV LHName -> ExprBV Symbol Symbol
forall a b. (a -> b) -> ExprBV Symbol a -> ExprBV Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
lhNameToResolvedSymbol) RTAlias Symbol (ExprV LHName)
xt


-- | @renameTys@ ensures that @RTAlias@ type parameters have distinct names
--   to avoid variable capture e.g. as in T1556.hs
renameTys :: RTAlias F.Symbol BareType -> RTAlias F.Symbol BareType
renameTys :: RTAlias Symbol BareType -> RTAlias Symbol BareType
renameTys RTAlias Symbol BareType
rt = RTAlias Symbol BareType
rt { rtTArgs = ys, rtBody = sbts (rtBody rt) (zip xs ys) }
  where
    xs :: [Symbol]
xs    = RTAlias Symbol BareType -> [Symbol]
forall x a. RTAlias x a -> [x]
rtTArgs RTAlias Symbol BareType
rt
    ys :: [Symbol]
ys    = (Symbol -> Symbol -> Symbol
`F.suffixSymbol` (HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol (LHName -> Symbol)
-> (RTAlias Symbol BareType -> LHName)
-> RTAlias Symbol BareType
-> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias Symbol BareType -> Located LHName)
-> RTAlias Symbol BareType
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol BareType -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias Symbol BareType -> Symbol)
-> RTAlias Symbol BareType -> Symbol
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol BareType
rt)) (Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs
    sbts :: BareType -> [(Symbol, Symbol)] -> BareType
sbts  = (BareType -> (Symbol, Symbol) -> BareType)
-> BareType -> [(Symbol, Symbol)] -> BareType
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (((Symbol, Symbol) -> BareType -> BareType)
-> BareType -> (Symbol, Symbol) -> BareType
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Symbol, Symbol) -> BareType -> BareType
forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt)


renameVV :: RTAlias F.Symbol BareType -> RTAlias F.Symbol BareType
renameVV :: RTAlias Symbol BareType -> RTAlias Symbol BareType
renameVV RTAlias Symbol BareType
rt = RTAlias Symbol BareType
rt { rtBody = RT.shiftVV (rtBody rt) (F.vv (Just 0)) }

-- | @renameRTVArgs@ ensures that @RTAlias@ value parameters have distinct names
--   to avoid variable capture e.g. as in tests-names-pos-Capture01.hs
renameRTVArgs :: (F.PPrint a, F.Subable a, F.Variable a ~ F.Symbol) => RTAlias x a -> RTAlias x a
renameRTVArgs :: forall a x.
(PPrint a, Subable a, Variable a ~ Symbol) =>
RTAlias x a -> RTAlias x a
renameRTVArgs RTAlias x a
rt = RTAlias x a
rt { rtVArgs = newArgs
                      , rtBody  = F.notracepp msg $ F.subst su (rtBody rt)
                      }
  where
    msg :: [Char]
msg          = [Char]
"renameRTVArgs: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SubstV Symbol -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp SubstV Symbol
su
    su :: SubstV Symbol
su           = [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst ([Symbol]
-> [ExprBV Symbol Symbol] -> [(Symbol, ExprBV Symbol Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
oldArgs (Symbol -> ExprBV Symbol Symbol
forall a. Symbolic a => a -> ExprBV Symbol Symbol
F.eVar (Symbol -> ExprBV Symbol Symbol)
-> [Symbol] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
newArgs))
    newArgs :: [Symbol]
newArgs      = (Symbol -> Int -> Symbol) -> [Symbol] -> [Int] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Symbol -> Int -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
rtArg (RTAlias x a -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias x a
rt) [(Int
0::Int)..]
    oldArgs :: [Symbol]
oldArgs      = RTAlias x a -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias x a
rt
    rtArg :: Symbol -> a -> Symbol
rtArg Symbol
x a
i    = Symbol -> Symbol -> Symbol
F.suffixSymbol Symbol
x (Symbol -> a -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
F.intSymbol Symbol
"rta" a
i)

-- | Recursively expands type aliases by unfolding the definitions of all inner
--   aliases and adds them to the environment.
--   Innermost aliases are unfolded and added first, and an error is thrown if
--   cyclic dependencies are detected.
--   Note that when called from 'makeRTEnv', the input environment contains only
--   expanded expression aliases.
makeRTAliases :: [RTAlias F.Symbol BareType] -> BareRTEnv -> BareRTEnv
makeRTAliases :: [RTAlias Symbol BareType]
-> RTEnv Symbol BareType -> RTEnv Symbol BareType
makeRTAliases [RTAlias Symbol BareType]
lxts RTEnv Symbol BareType
rte = (HashMap LHName (RTAlias Symbol BareType) -> BareType -> [LHName])
-> (RTEnv Symbol BareType
    -> RTAlias Symbol BareType -> RTEnv Symbol BareType)
-> RTEnv Symbol BareType
-> [RTAlias Symbol BareType]
-> RTEnv Symbol BareType
forall t x thing.
PPrint t =>
(AliasTable x t -> t -> [LHName])
-> (thing -> RTAlias x t -> thing)
-> thing
-> [RTAlias x t]
-> thing
graphExpand HashMap LHName (RTAlias Symbol BareType) -> BareType -> [LHName]
forall x t. AliasTable x t -> BareType -> [LHName]
buildTypeEdges RTEnv Symbol BareType
-> RTAlias Symbol BareType -> RTEnv Symbol BareType
f RTEnv Symbol BareType
rte [RTAlias Symbol BareType]
lxts
  where
    f :: RTEnv Symbol BareType
-> RTAlias Symbol BareType -> RTEnv Symbol BareType
f RTEnv Symbol BareType
rtEnv RTAlias Symbol BareType
xt = RTEnv Symbol BareType
-> RTAlias Symbol BareType -> RTEnv Symbol BareType
forall x t. RTEnv x t -> RTAlias x t -> RTEnv x t
setRTAlias RTEnv Symbol BareType
rtEnv (RTEnv Symbol BareType
-> SourcePos -> RTAlias Symbol BareType -> RTAlias Symbol BareType
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv (Located LHName -> SourcePos
forall a. Located a -> SourcePos
F.loc (Located LHName -> SourcePos)
-> (RTAlias Symbol BareType -> Located LHName)
-> RTAlias Symbol BareType
-> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol BareType -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias Symbol BareType -> SourcePos)
-> RTAlias Symbol BareType -> SourcePos
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol BareType
xt) RTAlias Symbol BareType
xt)

--------------------------------------------------------------------------------------------------------------

-- | Builds a directed graph of aliases, checks for cyclic dependencies,
--   reorders them so that inner aliases are processed first, and folds over
--   the graph to add each expanded node to the environment.
graphExpand :: (PPrint t)
            => (AliasTable x t -> t -> [LHName])         -- ^ dependencies
            -> (thing -> RTAlias x t -> thing) -- ^ update
            -> thing                                     -- ^ initial
            -> [RTAlias x t]                   -- ^ vertices
            -> thing                                     -- ^ final
graphExpand :: forall t x thing.
PPrint t =>
(AliasTable x t -> t -> [LHName])
-> (thing -> RTAlias x t -> thing)
-> thing
-> [RTAlias x t]
-> thing
graphExpand AliasTable x t -> t -> [LHName]
buildEdges thing -> RTAlias x t -> thing
expBody thing
env [RTAlias x t]
lxts
           = (thing -> RTAlias x t -> thing) -> thing -> [RTAlias x t] -> thing
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' thing -> RTAlias x t -> thing
expBody thing
env (AliasTable x t -> Graph LHName -> [RTAlias x t]
forall x t. AliasTable x t -> Graph LHName -> [RTAlias x t]
genExpandOrder AliasTable x t
table' Graph LHName
graph)
  where
    table :: AliasTable x t
table  = [RTAlias x t] -> AliasTable x t
forall x t. [RTAlias x t] -> AliasTable x t
buildAliasTable [RTAlias x t]
lxts
    graph :: Graph LHName
graph  = (t -> [LHName]) -> [RTAlias x t] -> Graph LHName
forall t x.
PPrint t =>
(t -> [LHName]) -> [RTAlias x t] -> Graph LHName
buildAliasGraph (AliasTable x t -> t -> [LHName]
buildEdges AliasTable x t
table) [RTAlias x t]
lxts
    table' :: AliasTable x t
table' = AliasTable x t -> Graph LHName -> AliasTable x t
forall x t. AliasTable x t -> Graph LHName -> AliasTable x t
checkCyclicAliases AliasTable x t
table Graph LHName
graph

-- | Inserts a type alias into the environment.
setRTAlias :: RTEnv x t -> RTAlias x t -> RTEnv x t
setRTAlias :: forall x t. RTEnv x t -> RTAlias x t -> RTEnv x t
setRTAlias RTEnv x t
env RTAlias x t
a = RTEnv x t
env { typeAliases =  M.insert n a (typeAliases env) }
  where
    n :: LHName
n            = Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias x t -> Located LHName) -> RTAlias x t -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias x t -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias x t -> LHName) -> RTAlias x t -> LHName
forall a b. (a -> b) -> a -> b
$ RTAlias x t
a

-- | Inserts an expression alias into the environment.
setREAlias :: RTEnv x t -> RTAlias F.Symbol F.Expr -> RTEnv x t
setREAlias :: forall x t.
RTEnv x t -> RTAlias Symbol (ExprBV Symbol Symbol) -> RTEnv x t
setREAlias RTEnv x t
env RTAlias Symbol (ExprBV Symbol Symbol)
a = RTEnv x t
env { exprAliases = M.insert n a (exprAliases env) }
  where
    n :: LHName
n            = Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias Symbol (ExprBV Symbol Symbol) -> Located LHName)
-> RTAlias Symbol (ExprBV Symbol Symbol)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol (ExprBV Symbol Symbol) -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias Symbol (ExprBV Symbol Symbol) -> LHName)
-> RTAlias Symbol (ExprBV Symbol Symbol) -> LHName
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol (ExprBV Symbol Symbol)
a

--------------------------------------------------------------------------------

type AliasTable x t = M.HashMap LHName (RTAlias x t)

buildAliasTable :: [RTAlias x t] -> AliasTable x t
buildAliasTable :: forall x t. [RTAlias x t] -> AliasTable x t
buildAliasTable = [(LHName, RTAlias x t)] -> HashMap LHName (RTAlias x t)
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList ([(LHName, RTAlias x t)] -> HashMap LHName (RTAlias x t))
-> ([RTAlias x t] -> [(LHName, RTAlias x t)])
-> [RTAlias x t]
-> HashMap LHName (RTAlias x t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RTAlias x t -> (LHName, RTAlias x t))
-> [RTAlias x t] -> [(LHName, RTAlias x t)]
forall a b. (a -> b) -> [a] -> [b]
map (\RTAlias x t
rta -> (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias x t -> Located LHName) -> RTAlias x t -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias x t -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias x t -> LHName) -> RTAlias x t -> LHName
forall a b. (a -> b) -> a -> b
$ RTAlias x t
rta, RTAlias x t
rta))

fromAliasLHName :: AliasTable x t -> LHName -> RTAlias x t
fromAliasLHName :: forall x t. AliasTable x t -> LHName -> RTAlias x t
fromAliasLHName AliasTable x t
table LHName
lhname
  = RTAlias x t -> Maybe (RTAlias x t) -> RTAlias x t
forall a. a -> Maybe a -> a
fromMaybe RTAlias x t
forall {a}. a
err (LHName -> AliasTable x t -> Maybe (RTAlias x t)
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup LHName
lhname AliasTable x t
table)
  where
    err :: a
err = Maybe SrcSpan -> [Char] -> a
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"fromAliasLHName: Dangling alias name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ LHName -> [Char]
forall a. Show a => a -> [Char]
show LHName
lhname)

-- | An adjacency list of nodes representing a directed graph.
--   Used to detect cyclic alias dependencies and to order the expansion
--   of aliases.
type Graph t = [Node t]
-- | A node described by a label, a key, and a list of connected nodes,
--   all parameterized by the same type. This type is used to represent
--   aliases nested within other aliases.
type Node  t = (t, t, [t])

buildAliasGraph :: (PPrint t) => (t -> [LHName]) -> [RTAlias x t]
                -> Graph LHName
buildAliasGraph :: forall t x.
PPrint t =>
(t -> [LHName]) -> [RTAlias x t] -> Graph LHName
buildAliasGraph t -> [LHName]
buildEdges = (RTAlias x t -> Node LHName) -> [RTAlias x t] -> Graph LHName
forall a b. (a -> b) -> [a] -> [b]
map ((t -> [LHName]) -> RTAlias x t -> Node LHName
forall t x.
PPrint t =>
(t -> [LHName]) -> RTAlias x t -> Node LHName
buildNode t -> [LHName]
buildEdges)
  where
    buildNode :: (PPrint t) => (t -> [LHName]) -> RTAlias x t
               -> Node LHName
    buildNode :: forall t x.
PPrint t =>
(t -> [LHName]) -> RTAlias x t -> Node LHName
buildNode t -> [LHName]
f RTAlias x t
a = (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias x t -> Located LHName) -> RTAlias x t -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias x t -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias x t -> LHName) -> RTAlias x t -> LHName
forall a b. (a -> b) -> a -> b
$ RTAlias x t
a, Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (RTAlias x t -> Located LHName) -> RTAlias x t -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias x t -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias x t -> LHName) -> RTAlias x t -> LHName
forall a b. (a -> b) -> a -> b
$ RTAlias x t
a, t -> [LHName]
f (RTAlias x t -> t
forall x a. RTAlias x a -> a
rtBody RTAlias x t
a))

checkCyclicAliases :: AliasTable x t -> Graph LHName -> AliasTable x t
checkCyclicAliases :: forall x t. AliasTable x t -> Graph LHName -> AliasTable x t
checkCyclicAliases AliasTable x t
table Graph LHName
graph
  = case (SCC LHName -> Maybe [LHName]) -> [SCC LHName] -> [[LHName]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SCC LHName -> Maybe [LHName]
forall {vertex}. SCC vertex -> Maybe [vertex]
go (Graph LHName -> [SCC LHName]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp Graph LHName
graph) of
      []   -> AliasTable x t
table
      [[LHName]]
sccs -> [TError SpecType] -> AliasTable x t
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (AliasTable x t -> [LHName] -> TError SpecType
forall x t. AliasTable x t -> [LHName] -> TError SpecType
cycleAliasErr AliasTable x t
table ([LHName] -> TError SpecType) -> [[LHName]] -> [TError SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[LHName]]
sccs)
    where
      go :: SCC vertex -> Maybe [vertex]
go (CyclicSCC [vertex]
vs) = [vertex] -> Maybe [vertex]
forall a. a -> Maybe a
Just [vertex]
vs
      go (AcyclicSCC vertex
_) = Maybe [vertex]
forall a. Maybe a
Nothing

cycleAliasErr :: AliasTable x t -> [LHName] -> Error
cycleAliasErr :: forall x t. AliasTable x t -> [LHName] -> TError SpecType
cycleAliasErr AliasTable x t
_ []          = Maybe SrcSpan -> [Char] -> TError SpecType
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"checkCyclicAliases: No aliases in reported cycle"
cycleAliasErr AliasTable x t
t nameList :: [LHName]
nameList@(LHName
name:[LHName]
_) = ErrAliasCycle { pos :: SrcSpan
pos    = (SrcSpan, Doc) -> SrcSpan
forall a b. (a, b) -> a
fst (LHName -> (SrcSpan, Doc)
locate LHName
name)
                                                , acycle :: [(SrcSpan, Doc)]
acycle = (LHName -> (SrcSpan, Doc)) -> [LHName] -> [(SrcSpan, Doc)]
forall a b. (a -> b) -> [a] -> [b]
map LHName -> (SrcSpan, Doc)
locate [LHName]
nameList }
  where
    locate :: LHName -> (SrcSpan, Doc)
locate LHName
n = ( Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located LHName -> SrcSpan)
-> (RTAlias x t -> Located LHName) -> RTAlias x t -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias x t -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias x t -> SrcSpan) -> RTAlias x t -> SrcSpan
forall a b. (a -> b) -> a -> b
$ AliasTable x t -> LHName -> RTAlias x t
forall x t. AliasTable x t -> LHName -> RTAlias x t
fromAliasLHName AliasTable x t
t LHName
n
                 , LHName -> Doc
forall a. PPrint a => a -> Doc
pprint LHName
n )

-- | Orders aliases so that nested ones are processed first.
genExpandOrder :: AliasTable x t -> Graph LHName -> [RTAlias x t]
genExpandOrder :: forall x t. AliasTable x t -> Graph LHName -> [RTAlias x t]
genExpandOrder AliasTable x t
table Graph LHName
graph
  = (LHName -> RTAlias x t) -> [LHName] -> [RTAlias x t]
forall a b. (a -> b) -> [a] -> [b]
map (AliasTable x t -> LHName -> RTAlias x t
forall x t. AliasTable x t -> LHName -> RTAlias x t
fromAliasLHName AliasTable x t
table) [LHName]
nameOrder
  where
    (Graph
digraph, Int -> Node LHName
lookupVertex, LHName -> Maybe Int
_)
      = Graph LHName -> (Graph, Int -> Node LHName, LHName -> Maybe Int)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Int -> (node, key, [key]), key -> Maybe Int)
graphFromEdges Graph LHName
graph
    nameOrder :: [LHName]
nameOrder
      = (Int -> LHName) -> [Int] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map (Node LHName -> LHName
forall a b c. (a, b, c) -> a
Misc.fst3 (Node LHName -> LHName) -> (Int -> Node LHName) -> Int -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Node LHName
lookupVertex) ([Int] -> [LHName]) -> [Int] -> [LHName]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. [a] -> [a]
reverse ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Graph -> [Int]
topSort Graph
digraph

--------------------------------------------------------------------------------

-- | Gathers all constructor names within a the body of a type alias
--   that match a key from the type 'AliasTable'.
buildTypeEdges :: AliasTable x t -> BareType -> [LHName]
buildTypeEdges :: forall x t. AliasTable x t -> BareType -> [LHName]
buildTypeEdges AliasTable x t
table = [LHName] -> [LHName]
forall a. Ord a => [a] -> [a]
Misc.ordNub ([LHName] -> [LHName])
-> (BareType -> [LHName]) -> BareType -> [LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> [LHName]
forall {a} {v} {tv} {r}. RTypeBV a v BTyCon tv r -> [LHName]
go
  where
    go :: RTypeBV a v BTyCon tv r -> [LHName]
go (RApp BTyCon
c [RTypeBV a v BTyCon tv r]
ts [RTPropBV a v BTyCon tv r]
rs r
_) = LHName -> [LHName]
go_alias (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located LHName
btc_tc BTyCon
c) [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ (RTypeBV a v BTyCon tv r -> [LHName])
-> [RTypeBV a v BTyCon tv r] -> [LHName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RTypeBV a v BTyCon tv r -> [LHName]
go [RTypeBV a v BTyCon tv r]
ts [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ (RTypeBV a v BTyCon tv r -> [LHName])
-> [RTypeBV a v BTyCon tv r] -> [LHName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RTypeBV a v BTyCon tv r -> [LHName]
go ((RTPropBV a v BTyCon tv r -> Maybe (RTypeBV a v BTyCon tv r))
-> [RTPropBV a v BTyCon tv r] -> [RTypeBV a v BTyCon tv r]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe RTPropBV a v BTyCon tv r -> Maybe (RTypeBV a v BTyCon tv r)
forall {b} {τ} {b} {v} {c} {tv} {r}.
RefB b τ (RTypeBV b v c tv r) -> Maybe (RTypeBV b v c tv r)
go_ref [RTPropBV a v BTyCon tv r]
rs)
    go (RFun a
_ RFInfo
_ RTypeBV a v BTyCon tv r
t1 RTypeBV a v BTyCon tv r
t2 r
_) = RTypeBV a v BTyCon tv r -> [LHName]
go RTypeBV a v BTyCon tv r
t1 [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ RTypeBV a v BTyCon tv r -> [LHName]
go RTypeBV a v BTyCon tv r
t2
    go (RAppTy RTypeBV a v BTyCon tv r
t1 RTypeBV a v BTyCon tv r
t2 r
_) = RTypeBV a v BTyCon tv r -> [LHName]
go RTypeBV a v BTyCon tv r
t1 [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ RTypeBV a v BTyCon tv r -> [LHName]
go RTypeBV a v BTyCon tv r
t2
    go (RAllE a
_ RTypeBV a v BTyCon tv r
t1 RTypeBV a v BTyCon tv r
t2)  = RTypeBV a v BTyCon tv r -> [LHName]
go RTypeBV a v BTyCon tv r
t1 [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ RTypeBV a v BTyCon tv r -> [LHName]
go RTypeBV a v BTyCon tv r
t2
    go (REx a
_ RTypeBV a v BTyCon tv r
t1 RTypeBV a v BTyCon tv r
t2)    = RTypeBV a v BTyCon tv r -> [LHName]
go RTypeBV a v BTyCon tv r
t1 [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ RTypeBV a v BTyCon tv r -> [LHName]
go RTypeBV a v BTyCon tv r
t2
    go (RAllT RTVUBV a v BTyCon tv
_ RTypeBV a v BTyCon tv r
t r
_)    = RTypeBV a v BTyCon tv r -> [LHName]
go RTypeBV a v BTyCon tv r
t
    go (RAllP PVUBV a v BTyCon tv
_ RTypeBV a v BTyCon tv r
t)      = RTypeBV a v BTyCon tv r -> [LHName]
go RTypeBV a v BTyCon tv r
t
    go (RVar tv
_ r
_)       = []
    go (RExprArg Located (ExprBV a v)
_)     = []
    go (RHole r
_)        = []
    go (RRTy [(a, RTypeBV a v BTyCon tv r)]
env r
_ Oblig
_ RTypeBV a v BTyCon tv r
t) = ((a, RTypeBV a v BTyCon tv r) -> [LHName])
-> [(a, RTypeBV a v BTyCon tv r)] -> [LHName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (RTypeBV a v BTyCon tv r -> [LHName]
go (RTypeBV a v BTyCon tv r -> [LHName])
-> ((a, RTypeBV a v BTyCon tv r) -> RTypeBV a v BTyCon tv r)
-> (a, RTypeBV a v BTyCon tv r)
-> [LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, RTypeBV a v BTyCon tv r) -> RTypeBV a v BTyCon tv r
forall a b. (a, b) -> b
snd) [(a, RTypeBV a v BTyCon tv r)]
env [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ RTypeBV a v BTyCon tv r -> [LHName]
go RTypeBV a v BTyCon tv r
t
    go_alias :: LHName -> [LHName]
go_alias LHName
c          = [LHName
c | LHName -> AliasTable x t -> Bool
forall k a. Hashable k => k -> HashMap k a -> Bool
M.member LHName
c AliasTable x t
table]
    go_ref :: RefB b τ (RTypeBV b v c tv r) -> Maybe (RTypeBV b v c tv r)
go_ref (RProp [(b, τ)]
_ (RHole r
_)) = Maybe (RTypeBV b v c tv r)
forall a. Maybe a
Nothing
    go_ref (RProp  [(b, τ)]
_ RTypeBV b v c tv r
t) = RTypeBV b v c tv r -> Maybe (RTypeBV b v c tv r)
forall a. a -> Maybe a
Just RTypeBV b v c tv r
t

-- | Gathers all variable names within the body of an expression alias
--   that match a key from the expression 'AliasTable'.
buildExprEdges :: AliasTable x t -> F.ExprV LHName -> [LHName]
buildExprEdges :: forall x t. AliasTable x t -> ExprV LHName -> [LHName]
buildExprEdges AliasTable x t
table  = [LHName] -> [LHName]
forall a. Ord a => [a] -> [a]
Misc.ordNub ([LHName] -> [LHName])
-> (ExprV LHName -> [LHName]) -> ExprV LHName -> [LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprV LHName -> [LHName]
forall {b}. ExprBV b LHName -> [LHName]
go
  where
    go :: ExprBV b LHName -> [LHName]
go (EApp ExprBV b LHName
e1 ExprBV b LHName
e2)   = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e1 [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ ExprBV b LHName -> [LHName]
go ExprBV b LHName
e2
    go (ENeg ExprBV b LHName
e)       = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e
    go (EBin Bop
_ ExprBV b LHName
e1 ExprBV b LHName
e2) = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e1 [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ ExprBV b LHName -> [LHName]
go ExprBV b LHName
e2
    go (EIte ExprBV b LHName
_ ExprBV b LHName
e1 ExprBV b LHName
e2) = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e1 [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ ExprBV b LHName -> [LHName]
go ExprBV b LHName
e2
    go (ECst ExprBV b LHName
e Sort
_)     = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e
    go (ESym SymConst
_)       = []
    go (ECon Constant
_)       = []
    go (EVar LHName
v)       = LHName -> [LHName]
go_alias LHName
v
    go (PAnd [ExprBV b LHName]
ps)       = (ExprBV b LHName -> [LHName]) -> [ExprBV b LHName] -> [LHName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExprBV b LHName -> [LHName]
go [ExprBV b LHName]
ps
    go (POr [ExprBV b LHName]
ps)        = (ExprBV b LHName -> [LHName]) -> [ExprBV b LHName] -> [LHName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExprBV b LHName -> [LHName]
go [ExprBV b LHName]
ps
    go (PNot ExprBV b LHName
p)        = ExprBV b LHName -> [LHName]
go ExprBV b LHName
p
    go (PImp ExprBV b LHName
p ExprBV b LHName
q)      = ExprBV b LHName -> [LHName]
go ExprBV b LHName
p [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ ExprBV b LHName -> [LHName]
go ExprBV b LHName
q
    go (PIff ExprBV b LHName
p ExprBV b LHName
q)      = ExprBV b LHName -> [LHName]
go ExprBV b LHName
p [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ ExprBV b LHName -> [LHName]
go ExprBV b LHName
q
    go (PAll [(b, Sort)]
_ ExprBV b LHName
p)      = ExprBV b LHName -> [LHName]
go ExprBV b LHName
p
    go (ELam (b, Sort)
_ ExprBV b LHName
e)      = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e
    go (ELet b
_ ExprBV b LHName
e1 ExprBV b LHName
e2)  = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e1 [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ ExprBV b LHName -> [LHName]
go ExprBV b LHName
e2
    go (ECoerc Sort
_ Sort
_ ExprBV b LHName
e)  = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e
    go (PAtom Brel
_ ExprBV b LHName
e1 ExprBV b LHName
e2) = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e1 [LHName] -> [LHName] -> [LHName]
forall a. [a] -> [a] -> [a]
++ ExprBV b LHName -> [LHName]
go ExprBV b LHName
e2
    go (ETApp ExprBV b LHName
e Sort
_)     = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e
    go (ETAbs ExprBV b LHName
e b
_)     = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e
    go PKVar{} = []
    go (PExist [(b, Sort)]
_ ExprBV b LHName
e)    = ExprBV b LHName -> [LHName]
go ExprBV b LHName
e
    go_alias :: LHName -> [LHName]
go_alias LHName
f         = [LHName
f | LHName -> AliasTable x t -> Bool
forall k a. Hashable k => k -> HashMap k a -> Bool
M.member LHName
f AliasTable x t
table ]


----------------------------------------------------------------------------------
-- | Using the `BareRTEnv` to do alias-expansion
----------------------------------------------------------------------------------
class Expand a where
  expand :: BareRTEnv -> F.SourcePos -> a -> a

----------------------------------------------------------------------------------
expandLoc :: (Expand a) => BareRTEnv -> Located a -> Located a
expandLoc :: forall a.
Expand a =>
RTEnv Symbol BareType -> Located a -> Located a
expandLoc RTEnv Symbol BareType
rtEnv Located a
lx = RTEnv Symbol BareType -> SourcePos -> a -> a
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv (Located a -> SourcePos
forall a. Located a -> SourcePos
F.loc Located a
lx) (a -> a) -> Located a -> Located a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located a
lx

instance Expand Expr where
  expand :: RTEnv Symbol BareType
-> SourcePos -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
expand = RTEnv Symbol BareType
-> SourcePos -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
expandExpr

instance Expand F.Reft where
  expand :: RTEnv Symbol BareType
-> SourcePos -> ReftBV Symbol Symbol -> ReftBV Symbol Symbol
expand RTEnv Symbol BareType
rtEnv SourcePos
l (F.Reft (Symbol
v, ExprBV Symbol Symbol
ra)) = (Symbol, ExprBV Symbol Symbol) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
v, RTEnv Symbol BareType
-> SourcePos -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l ExprBV Symbol Symbol
ra)

instance Expand RReft where
  expand :: RTEnv Symbol BareType
-> SourcePos
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
expand RTEnv Symbol BareType
rtEnv SourcePos
l = (ReftBV Symbol Symbol -> ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a b.
(a -> b) -> UReftBV Symbol Symbol a -> UReftBV Symbol Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RTEnv Symbol BareType
-> SourcePos -> ReftBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l)

expandReft :: (Expand r) => BareRTEnv -> F.SourcePos -> RType c tv r -> RType c tv r
expandReft :: forall r c tv.
Expand r =>
RTEnv Symbol BareType -> SourcePos -> RType c tv r -> RType c tv r
expandReft RTEnv Symbol BareType
rtEnv SourcePos
l = (r -> r)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
forall a b.
(a -> b)
-> RTypeBV Symbol Symbol c tv a -> RTypeBV Symbol Symbol c tv b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RTEnv Symbol BareType -> SourcePos -> r -> r
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l)
-- expandReft rtEnv l = emapReft (expand rtEnv l)


-- | @expand@ on a SpecType simply expands the refinements,
--   i.e. *does not* apply the type aliases, but just the
--   1. predicate aliases,
--   2. inlines,
--   3. stuff from @LogicMap@

instance Expand SpecType where
  expand :: RTEnv Symbol BareType -> SourcePos -> SpecType -> SpecType
expand = RTEnv Symbol BareType -> SourcePos -> SpecType -> SpecType
forall r c tv.
Expand r =>
RTEnv Symbol BareType -> SourcePos -> RType c tv r -> RType c tv r
expandReft

-- | @expand@ on a BareType actually applies the type- and expression- aliases.
instance Expand BareType where
  expand :: RTEnv Symbol BareType -> SourcePos -> BareType -> BareType
expand RTEnv Symbol BareType
rtEnv SourcePos
l
    = RTEnv Symbol BareType -> SourcePos -> BareType -> BareType
forall r c tv.
Expand r =>
RTEnv Symbol BareType -> SourcePos -> RType c tv r -> RType c tv r
expandReft     RTEnv Symbol BareType
rtEnv SourcePos
l -- apply expression aliases
    (BareType -> BareType)
-> (BareType -> BareType) -> BareType -> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTEnv Symbol BareType -> SourcePos -> BareType -> BareType
expandBareType RTEnv Symbol BareType
rtEnv SourcePos
l -- apply type       aliases

instance Expand (NoReftB b) where
  expand :: RTEnv Symbol BareType -> SourcePos -> NoReftB b -> NoReftB b
expand RTEnv Symbol BareType
_ SourcePos
_ = NoReftB b -> NoReftB b
forall a. a -> a
id

instance Expand (BRType NoReft) where
  expand :: RTEnv Symbol BareType
-> SourcePos
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
expand RTEnv Symbol BareType
rtEnv SourcePos
l
    = RTEnv Symbol BareType
-> SourcePos
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
forall r c tv.
Expand r =>
RTEnv Symbol BareType -> SourcePos -> RType c tv r -> RType c tv r
expandReft     RTEnv Symbol BareType
rtEnv SourcePos
l -- apply expression aliases
    (RTypeBV Symbol Symbol BTyCon BTyVar NoReft
 -> RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
-> (RTypeBV Symbol Symbol BTyCon BTyVar NoReft
    -> RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NoReft
forall b. NoReftB b
NoReft NoReft -> BareType -> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
forall a b.
a
-> RTypeBV Symbol Symbol BTyCon BTyVar b
-> RTypeBV Symbol Symbol BTyCon BTyVar a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$)
    (BareType -> RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
-> (RTypeBV Symbol Symbol BTyCon BTyVar NoReft -> BareType)
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTEnv Symbol BareType -> SourcePos -> BareType -> BareType
expandBareType RTEnv Symbol BareType
rtEnv SourcePos
l -- apply type       aliases
    (BareType -> BareType)
-> (RTypeBV Symbol Symbol BTyCon BTyVar NoReft -> BareType)
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
-> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NoReft -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft -> BareType
forall a b.
(a -> b)
-> RTypeBV Symbol Symbol BTyCon BTyVar a
-> RTypeBV Symbol Symbol BTyCon BTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> NoReft -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a b. a -> b -> a
const UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a. Monoid a => a
mempty)

instance Expand (RTAlias F.Symbol Expr) where
  expand :: RTEnv Symbol BareType
-> SourcePos
-> RTAlias Symbol (ExprBV Symbol Symbol)
-> RTAlias Symbol (ExprBV Symbol Symbol)
expand RTEnv Symbol BareType
rtEnv SourcePos
l RTAlias Symbol (ExprBV Symbol Symbol)
x = RTAlias Symbol (ExprBV Symbol Symbol)
x { rtBody = expand rtEnv l (rtBody x) }

instance Expand BareRTAlias where
  expand :: RTEnv Symbol BareType
-> SourcePos -> RTAlias Symbol BareType -> RTAlias Symbol BareType
expand RTEnv Symbol BareType
rtEnv SourcePos
l RTAlias Symbol BareType
x = RTAlias Symbol BareType
x { rtBody = expand rtEnv l (rtBody x) }

instance Expand Body where
  expand :: RTEnv Symbol BareType -> SourcePos -> Body -> Body
expand RTEnv Symbol BareType
rtEnv SourcePos
l (P   ExprBV Symbol Symbol
p) = ExprBV Symbol Symbol -> Body
forall v. ExprV v -> BodyV v
P   (RTEnv Symbol BareType
-> SourcePos -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l ExprBV Symbol Symbol
p)
  expand RTEnv Symbol BareType
rtEnv SourcePos
l (E   ExprBV Symbol Symbol
e) = ExprBV Symbol Symbol -> Body
forall v. ExprV v -> BodyV v
E   (RTEnv Symbol BareType
-> SourcePos -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l ExprBV Symbol Symbol
e)
  expand RTEnv Symbol BareType
rtEnv SourcePos
l (R Symbol
x ExprBV Symbol Symbol
p) = Symbol -> ExprBV Symbol Symbol -> Body
forall v. Symbol -> ExprV v -> BodyV v
R Symbol
x (RTEnv Symbol BareType
-> SourcePos -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l ExprBV Symbol Symbol
p)

instance Expand DataCtor where
  expand :: RTEnv Symbol BareType -> SourcePos -> DataCtor -> DataCtor
expand RTEnv Symbol BareType
rtEnv SourcePos
l DataCtor
c = DataCtor
c
    { dcTheta  = expand rtEnv l (dcTheta c)
    , dcFields = [(x, expand rtEnv l t) | (x, t) <- dcFields c ]
    , dcResult = expand rtEnv l (dcResult c)
    }

instance Expand DataDecl where
  expand :: RTEnv Symbol BareType
-> SourcePos
-> DataDeclP Symbol BareType
-> DataDeclP Symbol BareType
expand RTEnv Symbol BareType
rtEnv SourcePos
l DataDeclP Symbol BareType
d = DataDeclP Symbol BareType
d
    { tycDCons  = expand rtEnv l (tycDCons  d)
    , tycPropTy = expand rtEnv l (tycPropTy d)
    }

instance Expand BareMeasure where
  expand :: RTEnv Symbol BareType
-> SourcePos
-> MeasureV Symbol (Located BareType) (Located LHName)
-> MeasureV Symbol (Located BareType) (Located LHName)
expand RTEnv Symbol BareType
rtEnv SourcePos
l MeasureV Symbol (Located BareType) (Located LHName)
m = MeasureV Symbol (Located BareType) (Located LHName)
m
    { msSort = expand rtEnv l (msSort m)
    , msEqns = expand rtEnv l (msEqns m)
    }

instance Expand BareDef where
  expand :: RTEnv Symbol BareType
-> SourcePos
-> DefV Symbol (Located BareType) (Located LHName)
-> DefV Symbol (Located BareType) (Located LHName)
expand RTEnv Symbol BareType
rtEnv SourcePos
l DefV Symbol (Located BareType) (Located LHName)
d = DefV Symbol (Located BareType) (Located LHName)
d
    { dsort = expand rtEnv l (dsort d)
    , binds = [ (x, expand rtEnv l t) | (x, t) <- binds d]
    , body  = expand rtEnv l (body  d)
    }

instance Expand Ms.BareSpec where
  expand :: RTEnv Symbol BareType -> SourcePos -> BareSpec -> BareSpec
expand = RTEnv Symbol BareType -> SourcePos -> BareSpec -> BareSpec
expandBareSpec

instance Expand a => Expand (F.Located a) where
  expand :: RTEnv Symbol BareType -> SourcePos -> Located a -> Located a
expand RTEnv Symbol BareType
rtEnv SourcePos
_ = RTEnv Symbol BareType -> Located a -> Located a
forall a.
Expand a =>
RTEnv Symbol BareType -> Located a -> Located a
expandLoc RTEnv Symbol BareType
rtEnv

instance Expand a => Expand (F.LocSymbol, a) where
  expand :: RTEnv Symbol BareType
-> SourcePos -> (LocSymbol, a) -> (LocSymbol, a)
expand RTEnv Symbol BareType
rtEnv SourcePos
l (LocSymbol
x, a
y) = (LocSymbol
x, RTEnv Symbol BareType -> SourcePos -> a -> a
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l a
y)

instance Expand a => Expand (Maybe a) where
  expand :: RTEnv Symbol BareType -> SourcePos -> Maybe a -> Maybe a
expand RTEnv Symbol BareType
rtEnv SourcePos
l = (a -> a) -> Maybe a -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RTEnv Symbol BareType -> SourcePos -> a -> a
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l)

instance Expand a => Expand [a] where
  expand :: RTEnv Symbol BareType -> SourcePos -> [a] -> [a]
expand RTEnv Symbol BareType
rtEnv SourcePos
l = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RTEnv Symbol BareType -> SourcePos -> a -> a
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l)

instance Expand a => Expand (M.HashMap k a) where
  expand :: RTEnv Symbol BareType -> SourcePos -> HashMap k a -> HashMap k a
expand RTEnv Symbol BareType
rtEnv SourcePos
l = (a -> a) -> HashMap k a -> HashMap k a
forall a b. (a -> b) -> HashMap k a -> HashMap k b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RTEnv Symbol BareType -> SourcePos -> a -> a
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l)

-- | Expands a 'BareSpec'.
expandBareSpec :: BareRTEnv -> F.SourcePos -> Ms.BareSpec -> Ms.BareSpec
expandBareSpec :: RTEnv Symbol BareType -> SourcePos -> BareSpec -> BareSpec
expandBareSpec RTEnv Symbol BareType
rtEnv SourcePos
l BareSpec
sp = BareSpec
sp
  { measures   = expand rtEnv l (measures   sp)
  , asmSigs    = map (second (expand rtEnv l)) (asmSigs sp)
  , sigs       = map (second (expand rtEnv l)) (sigs sp)
  , ialiases   = [ (f x, f y) | (x, y) <- ialiases sp ]
  , dataDecls  = expand rtEnv l (dataDecls  sp)
  , newtyDecls = expand rtEnv l (newtyDecls sp)
  }
  where f :: Located BareType -> Located BareType
f      = RTEnv Symbol BareType
-> SourcePos -> Located BareType -> Located BareType
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l

expandBareType :: BareRTEnv -> F.SourcePos -> BareType -> BareType
expandBareType :: RTEnv Symbol BareType -> SourcePos -> BareType -> BareType
expandBareType RTEnv Symbol BareType
rtEnv SourcePos
l = BareType -> BareType
go
  where
    go :: BareType -> BareType
go (RApp BTyCon
c [BareType]
ts [RTPropBV
   Symbol
   Symbol
   BTyCon
   BTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)  = case BTyCon -> RTEnv Symbol BareType -> Maybe (RTAlias Symbol BareType)
lookupRTEnv BTyCon
c RTEnv Symbol BareType
rtEnv of
                             Just RTAlias Symbol BareType
rta -> SourcePos
-> RTAlias Symbol BareType
-> [BareType]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> BareType
expandRTAliasApp (BTyCon -> SourcePos
forall a. Loc a => a -> SourcePos
GM.fSourcePos BTyCon
c) RTAlias Symbol BareType
rta (BareType -> BareType
go (BareType -> BareType) -> [BareType] -> [BareType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
ts) UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
                             Maybe (RTAlias Symbol BareType)
Nothing  -> BTyCon
-> [BareType]
-> [RTPropBV
      Symbol
      Symbol
      BTyCon
      BTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> BareType
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp BTyCon
c (BareType -> BareType
go (BareType -> BareType) -> [BareType] -> [BareType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
ts) (RTPropBV
  Symbol
  Symbol
  BTyCon
  BTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTPropBV
     Symbol
     Symbol
     BTyCon
     BTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
goRef (RTPropBV
   Symbol
   Symbol
   BTyCon
   BTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> RTPropBV
      Symbol
      Symbol
      BTyCon
      BTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> [RTPropBV
      Symbol
      Symbol
      BTyCon
      BTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [RTPropBV
      Symbol
      Symbol
      BTyCon
      BTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropBV
   Symbol
   Symbol
   BTyCon
   BTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs) UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
    go (RAppTy BareType
t1 BareType
t2 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)  = BareType
-> BareType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> BareType
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2) UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
    go (RFun  Symbol
x RFInfo
i BareType
t1 BareType
t2 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) = Symbol
-> RFInfo
-> BareType
-> BareType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> BareType
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun  Symbol
x RFInfo
i (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2) UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
    go (RAllT RTVar BTyVar (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
a BareType
t UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)     = RTVar BTyVar (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
-> BareType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> BareType
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVar BTyVar (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
a (BareType -> BareType
go BareType
t) UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
    go (RAllP PVUBV Symbol Symbol BTyCon BTyVar
a BareType
t)       = PVUBV Symbol Symbol BTyCon BTyVar -> BareType -> BareType
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol BTyCon BTyVar
a (BareType -> BareType
go BareType
t)
    go (RAllE Symbol
x BareType
t1 BareType
t2)   = Symbol -> BareType -> BareType -> BareType
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllE Symbol
x (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2)
    go (REx Symbol
x BareType
t1 BareType
t2)     = Symbol -> BareType -> BareType -> BareType
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
REx   Symbol
x (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2)
    go (RRTy [(Symbol, BareType)]
e UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r Oblig
o BareType
t)    = [(Symbol, BareType)]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> Oblig
-> BareType
-> BareType
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RRTy  [(Symbol, BareType)]
e UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r Oblig
o     (BareType -> BareType
go BareType
t)
    go t :: BareType
t@RHole{}         = BareType
t
    go t :: BareType
t@RVar{}          = BareType
t
    go t :: BareType
t@RExprArg{}      = BareType
t
    goRef :: RTPropBV
  Symbol
  Symbol
  BTyCon
  BTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTPropBV
     Symbol
     Symbol
     BTyCon
     BTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
goRef (RProp [(Symbol, RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
ss BareType
t)   = [(Symbol, RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> BareType
-> RTPropBV
     Symbol
     Symbol
     BTyCon
     BTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp (((Symbol, RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
 -> (Symbol, RTypeBV Symbol Symbol BTyCon BTyVar NoReft))
-> [(Symbol, RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> [(Symbol, RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
forall a b. (a -> b) -> [a] -> [b]
map (RTEnv Symbol BareType
-> SourcePos
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
-> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
forall a. Expand a => RTEnv Symbol BareType -> SourcePos -> a -> a
expand RTEnv Symbol BareType
rtEnv SourcePos
l (RTypeBV Symbol Symbol BTyCon BTyVar NoReft
 -> RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
-> (Symbol, RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
-> (Symbol, RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) [(Symbol, RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
ss) (BareType -> BareType
go BareType
t)

lookupRTEnv :: BTyCon -> BareRTEnv -> Maybe BareRTAlias
lookupRTEnv :: BTyCon -> RTEnv Symbol BareType -> Maybe (RTAlias Symbol BareType)
lookupRTEnv BTyCon
c RTEnv Symbol BareType
rtEnv = LHName
-> HashMap LHName (RTAlias Symbol BareType)
-> Maybe (RTAlias Symbol BareType)
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located LHName
btc_tc BTyCon
c) (RTEnv Symbol BareType -> HashMap LHName (RTAlias Symbol BareType)
forall tv t. RTEnv tv t -> HashMap LHName (RTAlias tv t)
typeAliases RTEnv Symbol BareType
rtEnv)

expandRTAliasApp :: F.SourcePos -> BareRTAlias -> [BareType] -> RReft -> BareType
expandRTAliasApp :: SourcePos
-> RTAlias Symbol BareType
-> [BareType]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> BareType
expandRTAliasApp SourcePos
l rta :: RTAlias Symbol BareType
rta@(RTA {rtName :: forall x a. RTAlias x a -> Located LHName
rtName = Loc SourcePos
la SourcePos
_ LHName
_}) [BareType]
args UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r = case Maybe (TError SpecType)
isOK of
  Just TError SpecType
e     -> TError SpecType -> BareType
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw TError SpecType
e
  Maybe (TError SpecType)
Nothing    -> SubstV (Variable BareType) -> BareType -> BareType
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable BareType)
esu (BareType -> BareType)
-> (BareType -> BareType) -> BareType -> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BareType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> BareType
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`RT.strengthen` UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) (BareType -> BareType)
-> (BareType -> BareType) -> BareType -> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(BTyVar, RTypeBV Symbol Symbol BTyCon BTyVar NoReft, BareType)]
-> BareType -> BareType
forall tv (t :: * -> *) r c b v.
(Eq tv, Foldable t, Hashable tv, IsReft r, TyConable c, Binder b,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b)))) =>
t (tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
RT.subsTyVarsMeet [(BTyVar, RTypeBV Symbol Symbol BTyCon BTyVar NoReft, BareType)]
tsu (BareType -> BareType) -> BareType -> BareType
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol BareType -> BareType
forall x a. RTAlias x a -> a
rtBody RTAlias Symbol BareType
rta
  where
    tsu :: [(BTyVar, RTypeBV Symbol Symbol BTyCon BTyVar NoReft, BareType)]
tsu       = (BTyVar
 -> BareType
 -> (BTyVar, RTypeBV Symbol Symbol BTyCon BTyVar NoReft, BareType))
-> [BTyVar]
-> [BareType]
-> [(BTyVar, RTypeBV Symbol Symbol BTyCon BTyVar NoReft, BareType)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\BTyVar
α BareType
t -> (BTyVar
α, BareType -> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort BareType
t, BareType
t)) [BTyVar]
αs [BareType]
ts
    esu :: SubstV Symbol
esu       = [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst ([(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol)
-> [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall a b. (a -> b) -> a -> b
$ [Symbol]
-> [ExprBV Symbol Symbol] -> [(Symbol, ExprBV Symbol Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
εs) [ExprBV Symbol Symbol]
es
    es :: [ExprBV Symbol Symbol]
es        = SourcePos -> [Char] -> BareType -> ExprBV Symbol Symbol
exprArgFromBareType SourcePos
l [Char]
msg (BareType -> ExprBV Symbol Symbol)
-> [BareType] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
es0
    ([BareType]
ts, [BareType]
es0) = Int -> [BareType] -> ([BareType], [BareType])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
nαs [BareType]
args
    ([BTyVar]
αs, [Symbol]
εs)  = (LocSymbol -> BTyVar
BTV (LocSymbol -> BTyVar) -> (Symbol -> LocSymbol) -> Symbol -> BTyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Symbol -> BTyVar) -> [Symbol] -> [BTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTAlias Symbol BareType -> [Symbol]
forall x a. RTAlias x a -> [x]
rtTArgs RTAlias Symbol BareType
rta, RTAlias Symbol BareType -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol BareType
rta)
    targs :: [BareType]
targs     = (BareType -> Bool) -> [BareType] -> [BareType]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not (Bool -> Bool) -> (BareType -> Bool) -> BareType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> Bool
forall c tv r. RType c tv r -> Bool
isRExprArg) [BareType]
args
    eargs :: [BareType]
eargs     = (BareType -> Bool) -> [BareType] -> [BareType]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool) -> (BareType -> Bool) -> BareType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> Bool
forall c tv r. RType c tv r -> Bool
isRExprArg) [BareType]
args

    -- ERROR Checking Code
    msg :: [Char]
msg       = [Char]
"EXPAND-RTALIAS-APP: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Located LHName -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (RTAlias Symbol BareType -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName RTAlias Symbol BareType
rta)
    nαs :: Int
nαs       = [BTyVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BTyVar]
αs
    nεs :: Int
nεs       = [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
εs
    nargs :: Int
nargs     = [BareType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BareType]
args
    ntargs :: Int
ntargs    = [BareType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BareType]
targs
    neargs :: Int
neargs    = [BareType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BareType]
eargs
    err :: Doc -> Maybe (TError SpecType)
err       = SourcePos
-> SourcePos
-> RTAlias Symbol BareType
-> Doc
-> Maybe (TError SpecType)
errRTAliasApp SourcePos
l SourcePos
la RTAlias Symbol BareType
rta
    isOK :: Maybe Error
    isOK :: Maybe (TError SpecType)
isOK
      | Int
nargs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
ntargs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
neargs
      = Doc -> Maybe (TError SpecType)
err (Doc -> Maybe (TError SpecType)) -> Doc -> Maybe (TError SpecType)
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
PJ.hsep [Doc
"Expects", Int -> Doc
forall a. PPrint a => a -> Doc
pprint Int
nαs, Doc
"type arguments and then", Int -> Doc
forall a. PPrint a => a -> Doc
pprint Int
nεs, Doc
"expression arguments, but is given", Int -> Doc
forall a. PPrint a => a -> Doc
pprint Int
nargs]
      | Int
nargs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
nαs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nεs
      = Doc -> Maybe (TError SpecType)
err (Doc -> Maybe (TError SpecType)) -> Doc -> Maybe (TError SpecType)
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
PJ.hsep [Doc
"Expects", Int -> Doc
forall a. PPrint a => a -> Doc
pprint Int
nαs, Doc
"type arguments and"     , Int -> Doc
forall a. PPrint a => a -> Doc
pprint Int
nεs, Doc
"expression arguments, but is given", Int -> Doc
forall a. PPrint a => a -> Doc
pprint Int
nargs]
      | Int
nαs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
ntargs, Bool -> Bool
not ([BareType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [BareType]
eargs)
      = Doc -> Maybe (TError SpecType)
err (Doc -> Maybe (TError SpecType)) -> Doc -> Maybe (TError SpecType)
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
PJ.hsep [Doc
"Expects", Int -> Doc
forall a. PPrint a => a -> Doc
pprint Int
nαs, Doc
"type arguments before expression arguments"]
      | Bool
otherwise
      = Maybe (TError SpecType)
forall a. Maybe a
Nothing

-- | A copy of 'LHNameResolution.exprArg' tailored to the types needed in this
-- module.
exprArgFromBareType :: SourcePos -> String -> BareType -> Expr
exprArgFromBareType :: SourcePos -> [Char] -> BareType -> ExprBV Symbol Symbol
exprArgFromBareType SourcePos
l [Char]
msg = BareType -> ExprBV Symbol Symbol
go
  where
    go :: BareType -> Expr
    go :: BareType -> ExprBV Symbol Symbol
go (RExprArg Located (ExprBV Symbol Symbol)
e)     = Located (ExprBV Symbol Symbol) -> ExprBV Symbol Symbol
forall a. Located a -> a
val Located (ExprBV Symbol Symbol)
e
    go (RVar BTyVar
x UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_)       = Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
EVar (Symbol -> ExprBV Symbol Symbol) -> Symbol -> ExprBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ BTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol BTyVar
x
    go (RApp BTyCon
x [] [] UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_) = Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
EVar (LHName -> Symbol
getLHNameSymbol (LHName -> Symbol) -> LHName -> Symbol
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located LHName
btc_tc BTyCon
x)
    go (RApp BTyCon
f [BareType]
ts [] UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_) = ExprBV Symbol Symbol
-> [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> [ExprBV b v] -> ExprBV b v
F.eApps (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
EVar (LHName -> Symbol
getLHNameSymbol (LHName -> Symbol) -> LHName -> Symbol
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located LHName
btc_tc BTyCon
f)) (BareType -> ExprBV Symbol Symbol
go (BareType -> ExprBV Symbol Symbol)
-> [BareType] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
ts)
    go (RAppTy BareType
t1 BareType
t2 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_) = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
EApp (BareType -> ExprBV Symbol Symbol
go BareType
t1) (BareType -> ExprBV Symbol Symbol
go BareType
t2)
    go BareType
z                = Maybe SrcSpan -> [Char] -> ExprBV Symbol Symbol
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
sp ([Char] -> ExprBV Symbol Symbol) -> [Char] -> ExprBV Symbol Symbol
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
Printf.printf [Char]
"Unexpected expression parameter: %s in %s" (BareType -> [Char]
forall a. Show a => a -> [Char]
show BareType
z) [Char]
msg
    sp :: Maybe SrcSpan
sp                  = SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l)

isRExprArg :: RType c tv r -> Bool
isRExprArg :: forall c tv r. RType c tv r -> Bool
isRExprArg (RExprArg Located (ExprBV Symbol Symbol)
_) = Bool
True
isRExprArg RTypeBV Symbol Symbol c tv r
_            = Bool
False

errRTAliasApp :: F.SourcePos -> F.SourcePos -> BareRTAlias -> PJ.Doc -> Maybe Error
errRTAliasApp :: SourcePos
-> SourcePos
-> RTAlias Symbol BareType
-> Doc
-> Maybe (TError SpecType)
errRTAliasApp SourcePos
l SourcePos
la RTAlias Symbol BareType
rta = TError SpecType -> Maybe (TError SpecType)
forall a. a -> Maybe a
Just (TError SpecType -> Maybe (TError SpecType))
-> (Doc -> TError SpecType) -> Doc -> Maybe (TError SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan -> Doc -> SrcSpan -> Doc -> TError SpecType
forall t. SrcSpan -> Doc -> SrcSpan -> Doc -> TError t
ErrAliasApp  SrcSpan
sp Doc
name SrcSpan
sp'
  where
    name :: Doc
name            = Located LHName -> Doc
forall a. PPrint a => a -> Doc
pprint              (RTAlias Symbol BareType -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName RTAlias Symbol BareType
rta)
    sp :: SrcSpan
sp              = SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l
    sp' :: SrcSpan
sp'             = SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
la


----------------------------------------------------------------------------------------
-- | @cookSpecType@ is the central place where a @BareType@ gets processed,
--   in multiple steps, into a @SpecType@. See [NOTE:Cooking-SpecType] for
--   details of each of the individual steps.
----------------------------------------------------------------------------------------
cookSpecType :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocBareType
             -> LocSpecType
cookSpecType :: Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located BareType
-> Located SpecType
cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV Var
x Located BareType
bt =
  ([TError SpecType] -> Located SpecType)
-> (Located SpecType -> Located SpecType)
-> Either [TError SpecType] (Located SpecType)
-> Located SpecType
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [TError SpecType] -> Located SpecType
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw Located SpecType -> Located SpecType
forall a. a -> a
id (Either [TError SpecType] (Located SpecType) -> Located SpecType)
-> Either [TError SpecType] (Located SpecType) -> Located SpecType
forall a b. (a -> b) -> a -> b
$
  Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located BareType
-> Either [TError SpecType] (Located SpecType)
cookSpecTypeE Env
env SigEnv
sigEnv ModName
name PlugTV Var
x Located BareType
bt
  where
    _msg :: [Char]
_msg = [Char]
"cookSpecType: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Maybe Var, Maybe Type) -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (Maybe Var
z, Var -> Type
Ghc.varType (Var -> Type) -> Maybe Var -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Var
z)
    z :: Maybe Var
z    = PlugTV Var -> Maybe Var
forall v. PlugTV v -> Maybe v
Bare.plugSrc PlugTV Var
x


-----------------------------------------------------------------------------------------
cookSpecTypeE :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocBareType
              -> Bare.Lookup LocSpecType
-----------------------------------------------------------------------------------------
cookSpecTypeE :: Env
-> SigEnv
-> ModName
-> PlugTV Var
-> Located BareType
-> Either [TError SpecType] (Located SpecType)
cookSpecTypeE Env
env SigEnv
sigEnv name :: ModName
name@(ModName ModType
_ ModuleName
_) PlugTV Var
x Located BareType
bt
  = (Located SpecType -> Located SpecType)
-> Either [TError SpecType] (Located SpecType)
-> Either [TError SpecType] (Located SpecType)
forall a b.
(a -> b)
-> Either [TError SpecType] a -> Either [TError SpecType] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Located SpecType -> Located SpecType
f (Either [TError SpecType] (Located SpecType)
 -> Either [TError SpecType] (Located SpecType))
-> (Located BareType
    -> Either [TError SpecType] (Located SpecType))
-> Located BareType
-> Either [TError SpecType] (Located SpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> Located BareType -> Either [TError SpecType] (Located SpecType)
bareSpecType Env
env (Located BareType -> Either [TError SpecType] (Located SpecType))
-> Located BareType -> Either [TError SpecType] (Located SpecType)
forall a b. (a -> b) -> a -> b
$ RTEnv Symbol BareType -> Located BareType -> Located BareType
bareExpandType RTEnv Symbol BareType
rtEnv Located BareType
bt
  where
    f :: LocSpecType -> LocSpecType
    f :: Located SpecType -> Located SpecType
f =   (if Bool
doplug Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
allowTC then Bool
-> SigEnv
-> ModName
-> PlugTV Var
-> Located SpecType
-> Located SpecType
plugHoles Bool
allowTC SigEnv
sigEnv ModName
name PlugTV Var
x else Located SpecType -> Located SpecType
forall a. a -> a
id)
        (Located SpecType -> Located SpecType)
-> (Located SpecType -> Located SpecType)
-> Located SpecType
-> Located SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecType -> SpecType) -> Located SpecType -> Located SpecType
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TCEmb TyCon -> TyConMap -> SpecType -> SpecType
forall r.
(PPrint r, ToReft r, SubsTy RTyVar (RRType NoReft) r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 IsReft r) =>
TCEmb TyCon -> TyConMap -> RRType r -> RRType r
RT.addTyConInfo TCEmb TyCon
embs TyConMap
tyi)
        (Located SpecType -> Located SpecType)
-> (Located SpecType -> Located SpecType)
-> Located SpecType
-> Located SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> TCEmb TyCon -> Located SpecType -> Located SpecType
Bare.txRefSort TyConMap
tyi TCEmb TyCon
embs
        (Located SpecType -> Located SpecType)
-> (Located SpecType -> Located SpecType)
-> Located SpecType
-> Located SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> TyConMap -> Located SpecType -> Located SpecType
checkExtraAbsRef TCEmb TyCon
embs TyConMap
tyi
        (Located SpecType -> Located SpecType)
-> (Located SpecType -> Located SpecType)
-> Located SpecType
-> Located SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecType -> SpecType) -> Located SpecType -> Located SpecType
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> SpecType
txExpToBind -- What does this function DO
        (Located SpecType -> Located SpecType)
-> (Located SpecType -> Located SpecType)
-> Located SpecType
-> Located SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RTEnv Symbol BareType -> Located SpecType -> Located SpecType
specExpandType RTEnv Symbol BareType
rtEnv (Located SpecType -> Located SpecType)
-> (Located SpecType -> Located SpecType)
-> Located SpecType
-> Located SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecType -> SpecType) -> Located SpecType -> Located SpecType
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PlugTV Var -> SpecType -> SpecType
generalizeWith PlugTV Var
x))
        (Located SpecType -> Located SpecType)
-> (Located SpecType -> Located SpecType)
-> Located SpecType
-> Located SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Bool
doplug Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
allowTC then Bool
-> SigEnv
-> ModName
-> PlugTV Var
-> Located SpecType
-> Located SpecType
maybePlug Bool
allowTC SigEnv
sigEnv ModName
name PlugTV Var
x else Located SpecType -> Located SpecType
forall a. a -> a
id)

    allowTC :: Bool
allowTC = Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)
    -- modT   = mname `S.member` wiredInMods
    doplug :: Bool
doplug
      | Bare.LqTV Var
v <- PlugTV Var
x
      , Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isMethod Var
v Bool -> Bool -> Bool
|| Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isSCSel Var
v
      , Bool -> Bool
not (ModName -> Bool
isTarget ModName
name)
      = Bool
False
      | Bool
otherwise
      = Bool
True
    _msg :: a -> [Char]
_msg a
i = [Char]
"cook-" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PlugTV Var -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp PlugTV Var
x
    rtEnv :: RTEnv Symbol BareType
rtEnv  = SigEnv -> RTEnv Symbol BareType
Bare.sigRTEnv    SigEnv
sigEnv
    embs :: TCEmb TyCon
embs   = SigEnv -> TCEmb TyCon
Bare.sigEmbs     SigEnv
sigEnv
    tyi :: TyConMap
tyi    = SigEnv -> TyConMap
Bare.sigTyRTyMap SigEnv
sigEnv

-- | We don't want to generalize type variables that maybe bound in the
--   outer scope, e.g. see tests/basic/pos/LocalPlug00.hs

generalizeWith :: Bare.PlugTV Ghc.Var -> SpecType -> SpecType
generalizeWith :: PlugTV Var -> SpecType -> SpecType
generalizeWith (Bare.HsTV Var
v) SpecType
t = Var -> SpecType -> SpecType
generalizeVar Var
v SpecType
t
generalizeWith  PlugTV Var
Bare.RawTV   SpecType
t = SpecType
t
generalizeWith PlugTV Var
_             SpecType
t = SpecType -> SpecType
forall tv r c. (Eq tv, Monoid r) => RType c tv r -> RType c tv r
RT.generalize SpecType
t

-- | Check for extra abstract refinement arguments (lambda-form) on type
--   constructors that don't declare enough PVar parameters.  This must run
--   BEFORE 'txRefSort' and 'addTyConInfo' so that only user-written RProps
--   are present (system-generated default RProps from 'rtPropTop' have not
--   been added yet).  See GitHub issue #2603.
checkExtraAbsRef :: F.TCEmb Ghc.TyCon -> Bare.TyConMap -> LocSpecType -> LocSpecType
checkExtraAbsRef :: TCEmb TyCon -> TyConMap -> Located SpecType -> Located SpecType
checkExtraAbsRef TCEmb TyCon
embs TyConMap
tyi Located SpecType
lt = SrcSpan -> SpecType -> ()
forall {r}.
(ReftBind r ~ Symbol, ReftVar r ~ Symbol, IsReft r, PPrint r,
 SubsTy RTyVar (RRType NoReft) r) =>
SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck (Located SpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located SpecType
lt) (Located SpecType -> SpecType
forall a. Located a -> a
val Located SpecType
lt) () -> Located SpecType -> Located SpecType
forall a b. a -> b -> b
`seq` Located SpecType
lt
  where
    walkCheck :: SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp (RAllT RTVUBV Symbol Symbol RTyCon RTyVar
_ RTypeBV Symbol Symbol RTyCon RTyVar r
t r
_)      = SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t
    walkCheck SrcSpan
sp (RAllP PVUBV Symbol Symbol RTyCon RTyVar
_ RTypeBV Symbol Symbol RTyCon RTyVar r
t)        = SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t
    walkCheck SrcSpan
sp (RFun Symbol
_ RFInfo
_ RTypeBV Symbol Symbol RTyCon RTyVar r
t1 RTypeBV Symbol Symbol RTyCon RTyVar r
t2 r
_) = SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t1 () -> () -> ()
forall a b. a -> b -> b
`seq` SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t2
    walkCheck SrcSpan
sp (RApp RTyCon
rc [RTypeBV Symbol Symbol RTyCon RTyVar r]
ts [RTPropBV Symbol Symbol RTyCon RTyVar r]
rs r
_)
      | Bool -> Bool
not ([RTPropBV Symbol Symbol RTyCon RTyVar r] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RTPropBV Symbol Symbol RTyCon RTyVar r]
lambdaRest)
      = UserError -> ()
forall a. UserError -> a
uError (UserError -> ()) -> UserError -> ()
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> UserError
forall t. SrcSpan -> Doc -> TError t
ErrOther SrcSpan
sp (Doc -> UserError) -> Doc -> UserError
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
PJ.vcat
          [ [Char] -> Doc
PJ.text [Char]
"Type constructor" Doc -> Doc -> Doc
PJ.<+> [Char] -> Doc
PJ.text (TyCon -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr (RTyCon -> TyCon
rtc_tc RTyCon
rc))
              Doc -> Doc -> Doc
PJ.<+> if Int
nExpected Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
                       then [Char] -> Doc
PJ.text [Char]
"does not accept abstract refinement arguments,"
                       else [Char] -> Doc
PJ.text [Char]
"expects" Doc -> Doc -> Doc
PJ.<+> Int -> Doc
PJ.int Int
nExpected
                         Doc -> Doc -> Doc
PJ.<+> [Char] -> Doc
PJ.text [Char]
"abstract refinement argument(s),"
          , [Char] -> Doc
PJ.text [Char]
"but was given" Doc -> Doc -> Doc
PJ.<+> Int -> Doc
PJ.int Int
nGiven Doc -> Doc -> Doc
PJ.<> [Char] -> Doc
PJ.text [Char]
"."
          ]
      | Bool
otherwise = SrcSpan -> [RTypeBV Symbol Symbol RTyCon RTyVar r] -> ()
foldWalk SrcSpan
sp [RTypeBV Symbol Symbol RTyCon RTyVar r]
ts
      where
        (RTyCon
_, [PVUBV Symbol Symbol RTyCon RTyVar]
pvs)    = TCEmb TyCon
-> TyConMap
-> RTyCon
-> [RTypeBV Symbol Symbol RTyCon RTyVar r]
-> (RTyCon, [PVUBV Symbol Symbol RTyCon RTyVar])
forall r.
ToTypeable r =>
TCEmb TyCon
-> TyConMap
-> RTyCon
-> [RRType r]
-> (RTyCon, [PVUBV Symbol Symbol RTyCon RTyVar])
RT.appRTyCon TCEmb TyCon
embs TyConMap
tyi RTyCon
rc [RTypeBV Symbol Symbol RTyCon RTyVar r]
ts
        nExpected :: Int
nExpected   = [PVUBV Symbol Symbol RTyCon RTyVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PVUBV Symbol Symbol RTyCon RTyVar]
pvs
        nGiven :: Int
nGiven      = [RTPropBV Symbol Symbol RTyCon RTyVar r] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTPropBV Symbol Symbol RTyCon RTyVar r]
rs
        ([RTPropBV Symbol Symbol RTyCon RTyVar r]
_, [RTPropBV Symbol Symbol RTyCon RTyVar r]
rrest)  = Int
-> [RTPropBV Symbol Symbol RTyCon RTyVar r]
-> ([RTPropBV Symbol Symbol RTyCon RTyVar r],
    [RTPropBV Symbol Symbol RTyCon RTyVar r])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
nExpected [RTPropBV Symbol Symbol RTyCon RTyVar r]
rs
        lambdaRest :: [RTPropBV Symbol Symbol RTyCon RTyVar r]
lambdaRest  = [RTPropBV Symbol Symbol RTyCon RTyVar r
r | r :: RTPropBV Symbol Symbol RTyCon RTyVar r
r@(RProp [(Symbol, RRType NoReft)]
binds RTypeBV Symbol Symbol RTyCon RTyVar r
_) <- [RTPropBV Symbol Symbol RTyCon RTyVar r]
rrest, Bool -> Bool
not ([(Symbol, RRType NoReft)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Symbol, RRType NoReft)]
binds)]
    walkCheck SrcSpan
sp (RAllE Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar r
t1 RTypeBV Symbol Symbol RTyCon RTyVar r
t2)    = SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t1 () -> () -> ()
forall a b. a -> b -> b
`seq` SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t2
    walkCheck SrcSpan
sp (REx Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar r
t1 RTypeBV Symbol Symbol RTyCon RTyVar r
t2)      = SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t1 () -> () -> ()
forall a b. a -> b -> b
`seq` SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t2
    walkCheck SrcSpan
sp (RAppTy RTypeBV Symbol Symbol RTyCon RTyVar r
t1 RTypeBV Symbol Symbol RTyCon RTyVar r
t2 r
_)   = SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t1 () -> () -> ()
forall a b. a -> b -> b
`seq` SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t2
    walkCheck SrcSpan
sp (RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar r)]
xts r
_ Oblig
_ RTypeBV Symbol Symbol RTyCon RTyVar r
t)   = SrcSpan -> [RTypeBV Symbol Symbol RTyCon RTyVar r] -> ()
foldWalk SrcSpan
sp ((Symbol, RTypeBV Symbol Symbol RTyCon RTyVar r)
-> RTypeBV Symbol Symbol RTyCon RTyVar r
forall a b. (a, b) -> b
snd ((Symbol, RTypeBV Symbol Symbol RTyCon RTyVar r)
 -> RTypeBV Symbol Symbol RTyCon RTyVar r)
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar r)]
-> [RTypeBV Symbol Symbol RTyCon RTyVar r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar r)]
xts) () -> () -> ()
forall a b. a -> b -> b
`seq` SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t
    walkCheck SrcSpan
_  RTypeBV Symbol Symbol RTyCon RTyVar r
_                   = ()

    foldWalk :: SrcSpan -> [RTypeBV Symbol Symbol RTyCon RTyVar r] -> ()
foldWalk SrcSpan
sp = (() -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ())
-> () -> [RTypeBV Symbol Symbol RTyCon RTyVar r] -> ()
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (\()
acc RTypeBV Symbol Symbol RTyCon RTyVar r
t -> ()
acc () -> () -> ()
forall a b. a -> b -> b
`seq` SrcSpan -> RTypeBV Symbol Symbol RTyCon RTyVar r -> ()
walkCheck SrcSpan
sp RTypeBV Symbol Symbol RTyCon RTyVar r
t) ()

generalizeVar :: Ghc.Var -> SpecType -> SpecType
generalizeVar :: Var -> SpecType -> SpecType
generalizeVar Var
v SpecType
t = [(RTVUBV Symbol Symbol RTyCon RTyVar,
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [PVUBV Symbol Symbol RTyCon RTyVar] -> SpecType -> SpecType
forall (t :: * -> *) (t1 :: * -> *) tv b v c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RTypeBV b v c tv (NoReftB b)), r)
-> t1 (PVarBV b v (RTypeBV b v c tv (NoReftB b)))
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
mkUnivs [(RTVUBV Symbol Symbol RTyCon RTyVar
a, UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a. Monoid a => a
mempty) | RTVUBV Symbol Symbol RTyCon RTyVar
a <- [RTVUBV Symbol Symbol RTyCon RTyVar]
as] [] SpecType
t
  where
    as :: [RTVUBV Symbol Symbol RTyCon RTyVar]
as            = (RTVUBV Symbol Symbol RTyCon RTyVar -> Bool)
-> [RTVUBV Symbol Symbol RTyCon RTyVar]
-> [RTVUBV Symbol Symbol RTyCon RTyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter RTVUBV Symbol Symbol RTyCon RTyVar -> Bool
forall {s}. RTVar RTyVar s -> Bool
isGen (SpecType -> [RTVUBV Symbol Symbol RTyCon RTyVar]
forall tv v c r.
Eq tv =>
RTypeV v c tv r -> [RTVar tv (RTypeV v c tv NoReft)]
RT.freeTyVars SpecType
t)
    ([Var]
vas,Type
_)       = Type -> ([Var], Type)
Ghc.splitForAllTyCoVars (Var -> Type
GM.expandVarType Var
v)
    isGen :: RTVar RTyVar s -> Bool
isGen (RTVar (RTV Var
a) RTVInfo s
_) = Var
a Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
vas

-- splitForAllTyCoVars :: Type -> ([TyVar], Type)
--
-- generalize :: (Eq tv) => RType c tv r -> RType c tv r
-- generalize t = mkUnivs (freeTyVars t) [] [] t


bareExpandType :: BareRTEnv -> LocBareType -> LocBareType
bareExpandType :: RTEnv Symbol BareType -> Located BareType -> Located BareType
bareExpandType = RTEnv Symbol BareType -> Located BareType -> Located BareType
forall a.
Expand a =>
RTEnv Symbol BareType -> Located a -> Located a
expandLoc

specExpandType :: BareRTEnv -> LocSpecType -> LocSpecType
specExpandType :: RTEnv Symbol BareType -> Located SpecType -> Located SpecType
specExpandType = RTEnv Symbol BareType -> Located SpecType -> Located SpecType
forall a.
Expand a =>
RTEnv Symbol BareType -> Located a -> Located a
expandLoc

bareSpecType :: Bare.Env -> LocBareType -> Bare.Lookup LocSpecType
bareSpecType :: Env
-> Located BareType -> Either [TError SpecType] (Located SpecType)
bareSpecType Env
env Located BareType
bt =
  case HasCallStack =>
Env
-> SourcePos
-> Maybe [PVUBV Symbol Symbol BTyCon BTyVar]
-> BareType
-> Lookup SpecType
Env
-> SourcePos
-> Maybe [PVUBV Symbol Symbol BTyCon BTyVar]
-> BareType
-> Lookup SpecType
Bare.ofBareTypeE Env
env (Located BareType -> SourcePos
forall a. Located a -> SourcePos
F.loc Located BareType
bt) Maybe [PVUBV Symbol Symbol BTyCon BTyVar]
forall a. Maybe a
Nothing (Located BareType -> BareType
forall a. Located a -> a
val Located BareType
bt) of
    Left [TError SpecType]
e  -> [TError SpecType] -> Either [TError SpecType] (Located SpecType)
forall a b. a -> Either a b
Left [TError SpecType]
e
    Right SpecType
t -> Located SpecType -> Either [TError SpecType] (Located SpecType)
forall a b. b -> Either a b
Right (Located BareType -> SpecType -> Located SpecType
forall l b. Loc l => l -> b -> Located b
F.atLoc Located BareType
bt SpecType
t)

maybePlug :: Bool -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType
maybePlug :: Bool
-> SigEnv
-> ModName
-> PlugTV Var
-> Located SpecType
-> Located SpecType
maybePlug Bool
allowTC SigEnv
sigEnv ModName
name PlugTV Var
kx =
  case PlugTV Var -> Maybe Var
forall v. PlugTV v -> Maybe v
Bare.plugSrc PlugTV Var
kx of
    Maybe Var
Nothing -> Located SpecType -> Located SpecType
forall a. a -> a
id
    Just Var
_  -> Bool
-> SigEnv
-> ModName
-> PlugTV Var
-> Located SpecType
-> Located SpecType
plugHoles Bool
allowTC SigEnv
sigEnv ModName
name PlugTV Var
kx

plugHoles :: Bool -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType
plugHoles :: Bool
-> SigEnv
-> ModName
-> PlugTV Var
-> Located SpecType
-> Located SpecType
plugHoles Bool
allowTC SigEnv
sigEnv ModName
name =
  Bool
-> ModName
-> TCEmb TyCon
-> TyConMap
-> HashSet StableName
-> PlugTV Var
-> Located SpecType
-> Located SpecType
Bare.makePluggedSig Bool
allowTC ModName
name TCEmb TyCon
embs TyConMap
tyi HashSet StableName
exports
  where
    embs :: TCEmb TyCon
embs    = SigEnv -> TCEmb TyCon
Bare.sigEmbs     SigEnv
sigEnv
    tyi :: TyConMap
tyi     = SigEnv -> TyConMap
Bare.sigTyRTyMap SigEnv
sigEnv
    exports :: HashSet StableName
exports = SigEnv -> HashSet StableName
Bare.sigExports  SigEnv
sigEnv

{- [NOTE:Cooking-SpecType]
    A @SpecType@ is _raw_ when it is obtained directly from a @BareType@, i.e.
    just by replacing all the @BTyCon@ with @RTyCon@. Before it can be used
    for constraint generation, we need to _cook_ it via the following transforms:

    A @SigEnv@ should contain _all_ the information needed to do the below steps.

    - expand               : resolving all type/refinement etc. aliases
    - ofType               : convert BareType -> SpecType
    - plugged              : filling in any remaining "holes"
    - txRefSort            : filling in the abstract-refinement predicates etc. (YUCK)
    - resolve              : renaming / qualifying symbols?
    - expand (again)       : as the "resolve" step can rename variables to trigger more aliases (e.g. member -> Data.Set.Internal.Member -> Set_mem)
    - generalize           : (universally) quantify free type variables
    - strengthen-measures  : ?
    - strengthen-inline(?) : ?

-}

-----------------------------------------------------------------------------------------------
-- | From BareOLD.Expand
-----------------------------------------------------------------------------------------------


{- TODO-REBARE
instance Expand ty => Expand (Def ty ctor) where
  expand z (Def f xts c t bxts b) =
    Def f <$> expand z xts
          <*> pure c
          <*> expand z t
          <*> expand z bxts
          <*> expand z b

instance Expand ty => Expand (Measure ty ctor) where
  expand z (M n t ds k) =
    M n <$> expand z t <*> expand z ds <*> pure k

instance Expand DataConP where
  expand z d = do
    tyRes'    <- expand z (tyRes     d)
    tyConsts' <- expand z (tyConstrs d)
    tyArgs'   <- expand z (tyArgs    d)
    return d { tyRes =  tyRes', tyConstrs = tyConsts', tyArgs = tyArgs' }
-}

--------------------------------------------------------------------------------
-- | @expandExpr@ applies the aliases and inlines in @BareRTEnv@ to its argument
--   @Expr@. It must first @resolve@ the symbols in the refinement to see if
--   they correspond to alias definitions. However, we ensure that we do not
--   resolve bound variables (e.g. those bound in output refinements by input
--   parameters), and we use the @bs@ parameter to pass in the bound symbols.
--------------------------------------------------------------------------------
expandExpr :: BareRTEnv -> F.SourcePos -> Expr -> Expr
expandExpr :: RTEnv Symbol BareType
-> SourcePos -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
expandExpr RTEnv Symbol BareType
rtEnv SourcePos
l      = ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go
  where
    go :: ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go e :: ExprBV Symbol Symbol
e@(EApp ExprBV Symbol Symbol
_ ExprBV Symbol Symbol
_)     = RTEnv Symbol BareType
-> SourcePos
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
-> ExprBV Symbol Symbol
expandEApp RTEnv Symbol BareType
rtEnv SourcePos
l (ExprBV Symbol Symbol
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
forall b v. ExprBV b v -> (ExprBV b v, [ExprBV b v])
F.splitEApp ExprBV Symbol Symbol
e)
    go (EVar Symbol
x)         = RTEnv Symbol BareType
-> SourcePos -> Symbol -> ExprBV Symbol Symbol
expandSym  RTEnv Symbol BareType
rtEnv SourcePos
l Symbol
x
    go (ENeg ExprBV Symbol Symbol
e)         = ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v
ENeg       (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e)
    go (ECst ExprBV Symbol Symbol
e Sort
s)       = ExprBV Symbol Symbol -> Sort -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> Sort -> ExprBV b v
ECst       (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e) Sort
s
    go (PAnd [ExprBV Symbol Symbol]
ps)        = [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. [ExprBV b v] -> ExprBV b v
PAnd       (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> [ExprBV Symbol Symbol] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
ps)
    go (POr [ExprBV Symbol Symbol]
ps)         = [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. [ExprBV b v] -> ExprBV b v
POr        (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> [ExprBV Symbol Symbol] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
ps)
    go (PNot ExprBV Symbol Symbol
p)         = ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v
PNot       (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
p)
    go (PAll [(Symbol, Sort)]
xs ExprBV Symbol Symbol
p)      = [(Symbol, Sort)] -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. [(b, Sort)] -> ExprBV b v -> ExprBV b v
PAll [(Symbol, Sort)]
xs    (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
p)
    go (PExist [(Symbol, Sort)]
xs ExprBV Symbol Symbol
p)    = [(Symbol, Sort)] -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. [(b, Sort)] -> ExprBV b v -> ExprBV b v
PExist [(Symbol, Sort)]
xs  (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
p)
    go (ELam (Symbol, Sort)
xt ExprBV Symbol Symbol
e)      = (Symbol, Sort) -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. (b, Sort) -> ExprBV b v -> ExprBV b v
ELam (Symbol, Sort)
xt    (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e)
    go (ELet Symbol
x ExprBV Symbol Symbol
e1 ExprBV Symbol Symbol
e2)   = Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. b -> ExprBV b v -> ExprBV b v -> ExprBV b v
ELet Symbol
x     (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e2)
    go (ECoerc Sort
a Sort
t ExprBV Symbol Symbol
e)   = Sort -> Sort -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. Sort -> Sort -> ExprBV b v -> ExprBV b v
ECoerc Sort
a Sort
t (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e)
    go (ETApp ExprBV Symbol Symbol
e Sort
s)      = ExprBV Symbol Symbol -> Sort -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> Sort -> ExprBV b v
ETApp      (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e) Sort
s
    go (ETAbs ExprBV Symbol Symbol
e Symbol
s)      = ExprBV Symbol Symbol -> Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> b -> ExprBV b v
ETAbs      (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e) Symbol
s
    go (EBin Bop
op ExprBV Symbol Symbol
e1 ExprBV Symbol Symbol
e2)  = Bop
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. Bop -> ExprBV b v -> ExprBV b v -> ExprBV b v
EBin Bop
op    (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e2)
    go (PImp    ExprBV Symbol Symbol
e1 ExprBV Symbol Symbol
e2)  = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
PImp       (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e2)
    go (PIff    ExprBV Symbol Symbol
e1 ExprBV Symbol Symbol
e2)  = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
PIff       (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e2)
    go (PAtom Brel
b ExprBV Symbol Symbol
e1 ExprBV Symbol Symbol
e2)  = Brel
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. Brel -> ExprBV b v -> ExprBV b v -> ExprBV b v
PAtom Brel
b    (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e2)
    go (EIte  ExprBV Symbol Symbol
p ExprBV Symbol Symbol
e1 ExprBV Symbol Symbol
e2)  = ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v -> ExprBV b v
EIte (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
p)(ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e1) (ExprBV Symbol Symbol -> ExprBV Symbol Symbol
go ExprBV Symbol Symbol
e2)
    go e :: ExprBV Symbol Symbol
e@PKVar{}        = ExprBV Symbol Symbol
e
    go e :: ExprBV Symbol Symbol
e@(ESym SymConst
_)       = ExprBV Symbol Symbol
e
    go e :: ExprBV Symbol Symbol
e@(ECon Constant
_)       = ExprBV Symbol Symbol
e

expandSym :: BareRTEnv -> F.SourcePos -> F.Symbol -> Expr
expandSym :: RTEnv Symbol BareType
-> SourcePos -> Symbol -> ExprBV Symbol Symbol
expandSym RTEnv Symbol BareType
rtEnv SourcePos
l Symbol
s' = RTEnv Symbol BareType
-> SourcePos
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
-> ExprBV Symbol Symbol
expandEApp RTEnv Symbol BareType
rtEnv SourcePos
l (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
EVar Symbol
s', [])

-- REBARE :: expandSym' :: Symbol -> BareM Symbol
-- REBARE :: expandSym' s = do
  -- REBARE :: axs <- gets axSyms
  -- REBARE :: let s' = dropModuleNamesAndUnique s
  -- REBARE :: return $ if M.member s' axs then s' else s

expandEApp :: BareRTEnv -> F.SourcePos -> (Expr, [Expr]) -> Expr
expandEApp :: RTEnv Symbol BareType
-> SourcePos
-> (ExprBV Symbol Symbol, [ExprBV Symbol Symbol])
-> ExprBV Symbol Symbol
expandEApp RTEnv Symbol BareType
rtEnv SourcePos
l (EVar Symbol
f, [ExprBV Symbol Symbol]
es) = case Maybe (RTAlias Symbol (ExprBV Symbol Symbol))
mBody of
    Just RTAlias Symbol (ExprBV Symbol Symbol)
re -> SourcePos
-> RTAlias Symbol (ExprBV Symbol Symbol)
-> [ExprBV Symbol Symbol]
-> ExprBV Symbol Symbol
forall ty.
(Subable ty, Variable ty ~ Symbol) =>
SourcePos -> RTAlias Symbol ty -> [ExprBV Symbol Symbol] -> ty
expandApp SourcePos
l   RTAlias Symbol (ExprBV Symbol Symbol)
re       [ExprBV Symbol Symbol]
es'
    Maybe (RTAlias Symbol (ExprBV Symbol Symbol))
Nothing -> ExprBV Symbol Symbol
-> [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> [ExprBV b v] -> ExprBV b v
F.eApps       (Symbol -> ExprBV Symbol Symbol
forall b v. v -> ExprBV b v
EVar Symbol
f) [ExprBV Symbol Symbol]
es'
  where
    eAs :: HashMap Symbol (RTAlias Symbol (ExprBV Symbol Symbol))
eAs     = (LHName -> Symbol)
-> HashMap LHName (RTAlias Symbol (ExprBV Symbol Symbol))
-> HashMap Symbol (RTAlias Symbol (ExprBV Symbol Symbol))
forall k2 k1 v.
Hashable k2 =>
(k1 -> k2) -> HashMap k1 v -> HashMap k2 v
M.mapKeys LHName -> Symbol
lhNameToResolvedSymbol (HashMap LHName (RTAlias Symbol (ExprBV Symbol Symbol))
 -> HashMap Symbol (RTAlias Symbol (ExprBV Symbol Symbol)))
-> HashMap LHName (RTAlias Symbol (ExprBV Symbol Symbol))
-> HashMap Symbol (RTAlias Symbol (ExprBV Symbol Symbol))
forall a b. (a -> b) -> a -> b
$ RTEnv Symbol BareType
-> HashMap LHName (RTAlias Symbol (ExprBV Symbol Symbol))
forall tv t.
RTEnv tv t
-> HashMap LHName (RTAlias Symbol (ExprBV Symbol Symbol))
exprAliases RTEnv Symbol BareType
rtEnv
    mBody :: Maybe (RTAlias Symbol (ExprBV Symbol Symbol))
mBody   = Symbol
-> HashMap Symbol (RTAlias Symbol (ExprBV Symbol Symbol))
-> Maybe (RTAlias Symbol (ExprBV Symbol Symbol))
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Symbol
f HashMap Symbol (RTAlias Symbol (ExprBV Symbol Symbol))
eAs Maybe (RTAlias Symbol (ExprBV Symbol Symbol))
-> Maybe (RTAlias Symbol (ExprBV Symbol Symbol))
-> Maybe (RTAlias Symbol (ExprBV Symbol Symbol))
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Symbol
-> HashMap Symbol (RTAlias Symbol (ExprBV Symbol Symbol))
-> Maybe (RTAlias Symbol (ExprBV Symbol Symbol))
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup (Symbol -> Symbol
GM.dropModuleUnique Symbol
f) HashMap Symbol (RTAlias Symbol (ExprBV Symbol Symbol))
eAs
    es' :: [ExprBV Symbol Symbol]
es'     = RTEnv Symbol BareType
-> SourcePos -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
expandExpr RTEnv Symbol BareType
rtEnv SourcePos
l (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> [ExprBV Symbol Symbol] -> [ExprBV Symbol Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprBV Symbol Symbol]
es
    _f0 :: Symbol
_f0     = Symbol -> Symbol
GM.dropModuleNamesAndUnique Symbol
f

expandEApp RTEnv Symbol BareType
_ SourcePos
_ (ExprBV Symbol Symbol
f, [ExprBV Symbol Symbol]
es) = ExprBV Symbol Symbol
-> [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall b v. ExprBV b v -> [ExprBV b v] -> ExprBV b v
F.eApps ExprBV Symbol Symbol
f [ExprBV Symbol Symbol]
es

--------------------------------------------------------------------------------
-- | Expand Alias Application --------------------------------------------------
--------------------------------------------------------------------------------
expandApp :: (F.Subable ty, F.Variable ty ~ F.Symbol) => F.SourcePos -> RTAlias F.Symbol ty -> [Expr] -> ty
expandApp :: forall ty.
(Subable ty, Variable ty ~ Symbol) =>
SourcePos -> RTAlias Symbol ty -> [ExprBV Symbol Symbol] -> ty
expandApp SourcePos
l RTAlias Symbol ty
re [ExprBV Symbol Symbol]
es
  | Just SubstV Symbol
su <- Maybe (SubstV Symbol)
args = SubstV (Variable ty) -> ty -> ty
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable ty)
su (RTAlias Symbol ty -> ty
forall x a. RTAlias x a -> a
rtBody RTAlias Symbol ty
re)
  | Bool
otherwise       = UserError -> ty
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw UserError
err
  where
    args :: Maybe (SubstV Symbol)
args            = [(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst ([(Symbol, ExprBV Symbol Symbol)] -> SubstV Symbol)
-> Maybe [(Symbol, ExprBV Symbol Symbol)] -> Maybe (SubstV Symbol)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
-> [ExprBV Symbol Symbol] -> Maybe [(Symbol, ExprBV Symbol Symbol)]
forall a b. [a] -> [b] -> Maybe [(a, b)]
Misc.zipMaybe (RTAlias Symbol ty -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol ty
re) [ExprBV Symbol Symbol]
es
    err             :: UserError
    err :: UserError
err             = SrcSpan -> Doc -> SrcSpan -> Doc -> UserError
forall t. SrcSpan -> Doc -> SrcSpan -> Doc -> TError t
ErrAliasApp SrcSpan
sp Doc
alias SrcSpan
sp' Doc
msg
    sp :: SrcSpan
sp              = SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l
    alias :: Doc
alias           = Located LHName -> Doc
forall a. PPrint a => a -> Doc
pprint           (RTAlias Symbol ty -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName RTAlias Symbol ty
re)
    sp' :: SrcSpan
sp'             = Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located LHName -> SrcSpan)
-> (RTAlias Symbol ty -> Located LHName)
-> RTAlias Symbol ty
-> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol ty -> Located LHName
forall x a. RTAlias x a -> Located LHName
rtName (RTAlias Symbol ty -> SrcSpan) -> RTAlias Symbol ty -> SrcSpan
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol ty
re
    msg :: Doc
msg             =  Doc
"expects" Doc -> Doc -> Doc
PJ.<+> Int -> Doc
forall a. PPrint a => a -> Doc
pprint ([Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Symbol] -> Int) -> [Symbol] -> Int
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol ty -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol ty
re)
                   Doc -> Doc -> Doc
PJ.<+> Doc
"arguments but it is given"
                   Doc -> Doc -> Doc
PJ.<+> Int -> Doc
forall a. PPrint a => a -> Doc
pprint ([ExprBV Symbol Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExprBV Symbol Symbol]
es)


-------------------------------------------------------------------------------
-- | Replace Predicate Arguments With Existentials ----------------------------
-------------------------------------------------------------------------------
txExpToBind   :: SpecType -> SpecType
-------------------------------------------------------------------------------
txExpToBind :: SpecType -> SpecType
txExpToBind SpecType
t =
  State ExSt SpecType -> ExSt -> SpecType
forall s a. State s a -> s -> a
evalState (SpecType -> State ExSt SpecType
expToBindT SpecType
t) (Int
-> HashMap Symbol (RRType NoReft, ExprBV Symbol Symbol)
-> HashMap Symbol (PVUBV Symbol Symbol RTyCon RTyVar)
-> ExSt
ExSt Int
0 HashMap Symbol (RRType NoReft, ExprBV Symbol Symbol)
forall k v. HashMap k v
M.empty HashMap Symbol (PVUBV Symbol Symbol RTyCon RTyVar)
πs)
  where
    πs :: HashMap Symbol (PVUBV Symbol Symbol RTyCon RTyVar)
πs        = [(Symbol, PVUBV Symbol Symbol RTyCon RTyVar)]
-> HashMap Symbol (PVUBV Symbol Symbol RTyCon RTyVar)
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(PVUBV Symbol Symbol RTyCon RTyVar -> Symbol
forall b v t. PVarBV b v t -> b
pname PVUBV Symbol Symbol RTyCon RTyVar
p, PVUBV Symbol Symbol RTyCon RTyVar
p) | PVUBV Symbol Symbol RTyCon RTyVar
p <- RTypeRepBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [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
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> [PVUBV Symbol Symbol RTyCon RTyVar])
-> RTypeRepBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [PVUBV Symbol Symbol RTyCon RTyVar]
forall a b. (a -> b) -> a -> b
$ SpecType
-> RTypeRepBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep SpecType
t ]

data ExSt = ExSt { ExSt -> Int
fresh :: Int
                 , ExSt -> HashMap Symbol (RRType NoReft, ExprBV Symbol Symbol)
emap  :: M.HashMap F.Symbol (RSort, F.Expr)
                 , ExSt -> HashMap Symbol (PVUBV Symbol Symbol RTyCon RTyVar)
pmap  :: M.HashMap F.Symbol RPVar
                 }

-- | TODO: Niki please write more documentation for this, maybe an example?
--   I can't really tell whats going on... (RJ)

expToBindT :: SpecType -> State ExSt SpecType
expToBindT :: SpecType -> State ExSt SpecType
expToBindT (RVar RTyVar
v UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
  = UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> State ExSt (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall r. UReft r -> State ExSt (UReft r)
expToBindRef UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r State ExSt (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> (UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> State ExSt SpecType)
-> State ExSt SpecType
forall a b.
StateT ExSt Identity a
-> (a -> StateT ExSt Identity b) -> StateT ExSt Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists (SpecType -> State ExSt SpecType)
-> (UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> State ExSt SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTyVar -> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar RTyVar
v
expToBindT (RFun Symbol
x RFInfo
i SpecType
t1 SpecType
t2 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
  = do t1' <- SpecType -> State ExSt SpecType
expToBindT SpecType
t1
       t2' <- expToBindT t2
       expToBindRef r >>= addExists . RFun x i t1' t2'
expToBindT (RAllT RTVUBV Symbol Symbol RTyCon RTyVar
a SpecType
t UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
  = do t' <- SpecType -> State ExSt SpecType
expToBindT SpecType
t
       expToBindRef r >>= addExists . RAllT a t'
expToBindT (RAllP PVUBV Symbol Symbol RTyCon RTyVar
p SpecType
t)
  = (SpecType -> SpecType)
-> State ExSt SpecType -> State ExSt SpecType
forall a b.
(a -> b) -> StateT ExSt Identity a -> StateT ExSt Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PVUBV Symbol Symbol RTyCon RTyVar -> SpecType -> SpecType
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol Symbol RTyCon RTyVar
p) (SpecType -> State ExSt SpecType
expToBindT SpecType
t)
expToBindT (RApp RTyCon
c [SpecType]
ts [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
  = do ts' <- (SpecType -> State ExSt SpecType)
-> [SpecType] -> StateT ExSt Identity [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SpecType -> State ExSt SpecType
expToBindT [SpecType]
ts
       rs' <- mapM expToBindReft rs
       expToBindRef r >>= addExists . RApp c ts' rs'
expToBindT (RAppTy SpecType
t1 SpecType
t2 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
  = do t1' <- SpecType -> State ExSt SpecType
expToBindT SpecType
t1
       t2' <- expToBindT t2
       expToBindRef r >>= addExists . RAppTy t1' t2'
expToBindT (RRTy [(Symbol, SpecType)]
xts UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r Oblig
o SpecType
t)
  = do xts' <- [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs ([SpecType] -> [(Symbol, SpecType)])
-> StateT ExSt Identity [SpecType]
-> StateT ExSt Identity [(Symbol, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SpecType -> State ExSt SpecType)
-> [SpecType] -> StateT ExSt Identity [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SpecType -> State ExSt SpecType
expToBindT [SpecType]
ts
       r'   <- expToBindRef r
       t'   <- expToBindT t
       return $ RRTy xts' r' o t'
  where
     ([Symbol]
xs, [SpecType]
ts) = [(Symbol, SpecType)] -> ([Symbol], [SpecType])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Symbol, SpecType)]
xts
expToBindT SpecType
t
  = SpecType -> State ExSt SpecType
forall a. a -> StateT ExSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

expToBindReft              :: SpecProp -> State ExSt SpecProp
expToBindReft :: RTPropBV
  Symbol
  Symbol
  RTyCon
  RTyVar
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> StateT
     ExSt
     Identity
     (RTPropBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
expToBindReft (RProp [(Symbol, RRType NoReft)]
s (RHole UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)) = [(Symbol, RRType NoReft)]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b τ r v c tv. [(b, τ)] -> r -> RefB b τ (RTypeV v c tv r)
rPropP [(Symbol, RRType NoReft)]
s (UReftBV Symbol Symbol (ReftBV Symbol Symbol)
 -> RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> State ExSt (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> StateT
     ExSt
     Identity
     (RTPropBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> State ExSt (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall r. UReft r -> State ExSt (UReft r)
expToBindRef UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
expToBindReft (RProp [(Symbol, RRType NoReft)]
s SpecType
t)  = [(Symbol, RRType NoReft)]
-> SpecType
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RRType NoReft)]
s  (SpecType
 -> RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> State ExSt SpecType
-> StateT
     ExSt
     Identity
     (RTPropBV
        Symbol
        Symbol
        RTyCon
        RTyVar
        (UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> State ExSt SpecType
expToBindT SpecType
t


getBinds :: State ExSt (M.HashMap F.Symbol (RSort, F.Expr))
getBinds :: State ExSt (HashMap Symbol (RRType NoReft, ExprBV Symbol Symbol))
getBinds
  = do bds <- (ExSt -> HashMap Symbol (RRType NoReft, ExprBV Symbol Symbol))
-> State
     ExSt (HashMap Symbol (RRType NoReft, ExprBV Symbol Symbol))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt -> HashMap Symbol (RRType NoReft, ExprBV Symbol Symbol)
emap
       modify $ \ExSt
st -> ExSt
st{emap = M.empty}
       return bds

addExists :: SpecType -> State ExSt SpecType
addExists :: SpecType -> State ExSt SpecType
addExists SpecType
t = (HashMap Symbol (RRType NoReft, ExprBV Symbol Symbol) -> SpecType)
-> State
     ExSt (HashMap Symbol (RRType NoReft, ExprBV Symbol Symbol))
-> State ExSt SpecType
forall a b.
(a -> b) -> StateT ExSt Identity a -> StateT ExSt Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SpecType
 -> Symbol -> (RRType NoReft, ExprBV Symbol Symbol) -> SpecType)
-> SpecType
-> HashMap Symbol (RRType NoReft, ExprBV Symbol Symbol)
-> SpecType
forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
M.foldlWithKey' SpecType
-> Symbol -> (RRType NoReft, ExprBV Symbol Symbol) -> SpecType
addExist SpecType
t) State ExSt (HashMap Symbol (RRType NoReft, ExprBV Symbol Symbol))
getBinds

addExist :: SpecType -> F.Symbol -> (RSort, F.Expr) -> SpecType
addExist :: SpecType
-> Symbol -> (RRType NoReft, ExprBV Symbol Symbol) -> SpecType
addExist SpecType
t Symbol
x (RRType NoReft
tx, ExprBV Symbol Symbol
e) = Symbol -> SpecType -> SpecType -> SpecType
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
REx Symbol
x SpecType
t' SpecType
t
  where
    t' :: SpecType
t'               = RRType NoReft -> SpecType
forall r b v c tv.
IsReft r =>
RTypeBV b v c tv (NoReftB b) -> RTypeBV b v c tv r
ofRSort RRType NoReft
tx SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`RT.strengthen` ReftBV Symbol Symbol
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall r v. r -> UReftV v r
RT.uTop ReftBV Symbol Symbol
r
    r :: ReftBV Symbol Symbol
r                = ExprBV Symbol Symbol -> ReftBV Symbol Symbol
forall a. Expression a => a -> ReftBV Symbol Symbol
F.exprReft ExprBV Symbol Symbol
e

expToBindRef :: UReft r -> State ExSt (UReft r)
expToBindRef :: forall r. UReft r -> State ExSt (UReft r)
expToBindRef (MkUReft r
r (Pr [PVarBV Symbol Symbol ()]
p))
  = (PVarBV Symbol Symbol ()
 -> StateT ExSt Identity (PVarBV Symbol Symbol ()))
-> [PVarBV Symbol Symbol ()]
-> StateT ExSt Identity [PVarBV Symbol Symbol ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM PVarBV Symbol Symbol ()
-> StateT ExSt Identity (PVarBV Symbol Symbol ())
expToBind [PVarBV Symbol Symbol ()]
p StateT ExSt Identity [PVarBV Symbol Symbol ()]
-> ([PVarBV Symbol Symbol ()] -> UReftBV Symbol Symbol r)
-> StateT ExSt Identity (UReftBV Symbol Symbol r)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (r -> PredicateBV Symbol Symbol -> UReftBV Symbol Symbol r
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft r
r (PredicateBV Symbol Symbol -> UReftBV Symbol Symbol r)
-> ([PVarBV Symbol Symbol ()] -> PredicateBV Symbol Symbol)
-> [PVarBV Symbol Symbol ()]
-> UReftBV Symbol Symbol r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [PVarBV Symbol Symbol ()] -> PredicateBV Symbol Symbol
forall b v. [UsedPVarBV b v] -> PredicateBV b v
Pr)

expToBind :: UsedPVar -> State ExSt UsedPVar
expToBind :: PVarBV Symbol Symbol ()
-> StateT ExSt Identity (PVarBV Symbol Symbol ())
expToBind PVarBV Symbol Symbol ()
p = do
  res <- (ExSt -> Maybe (PVUBV Symbol Symbol RTyCon RTyVar))
-> StateT ExSt Identity (Maybe (PVUBV Symbol Symbol RTyCon RTyVar))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Symbol
-> HashMap Symbol (PVUBV Symbol Symbol RTyCon RTyVar)
-> Maybe (PVUBV Symbol Symbol RTyCon RTyVar)
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup (PVarBV Symbol Symbol () -> Symbol
forall b v t. PVarBV b v t -> b
pname PVarBV Symbol Symbol ()
p) (HashMap Symbol (PVUBV Symbol Symbol RTyCon RTyVar)
 -> Maybe (PVUBV Symbol Symbol RTyCon RTyVar))
-> (ExSt -> HashMap Symbol (PVUBV Symbol Symbol RTyCon RTyVar))
-> ExSt
-> Maybe (PVUBV Symbol Symbol RTyCon RTyVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExSt -> HashMap Symbol (PVUBV Symbol Symbol RTyCon RTyVar)
pmap)
  case res of
    Maybe (PVUBV Symbol Symbol RTyCon RTyVar)
Nothing ->
      Maybe SrcSpan
-> [Char] -> StateT ExSt Identity (PVarBV Symbol Symbol ())
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"expToBind: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PVarBV Symbol Symbol () -> [Char]
forall a. Show a => a -> [Char]
show PVarBV Symbol Symbol ()
p)
    Just PVUBV Symbol Symbol RTyCon RTyVar
π  -> do
      let pargs0 :: [(((), Symbol, ExprBV Symbol Symbol), RRType NoReft)]
pargs0 = [((), Symbol, ExprBV Symbol Symbol)]
-> [RRType NoReft]
-> [(((), Symbol, ExprBV Symbol Symbol), RRType NoReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip (PVarBV Symbol Symbol () -> [((), Symbol, ExprBV Symbol Symbol)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVarBV Symbol Symbol ()
p) ((RRType NoReft, Symbol, ExprBV Symbol Symbol) -> RRType NoReft
forall a b c. (a, b, c) -> a
Misc.fst3 ((RRType NoReft, Symbol, ExprBV Symbol Symbol) -> RRType NoReft)
-> [(RRType NoReft, Symbol, ExprBV Symbol Symbol)]
-> [RRType NoReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVUBV Symbol Symbol RTyCon RTyVar
-> [(RRType NoReft, Symbol, ExprBV Symbol Symbol)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVUBV Symbol Symbol RTyCon RTyVar
π)
      pargs' <- ((((), Symbol, ExprBV Symbol Symbol), RRType NoReft)
 -> StateT ExSt Identity ((), Symbol, ExprBV Symbol Symbol))
-> [(((), Symbol, ExprBV Symbol Symbol), RRType NoReft)]
-> StateT ExSt Identity [((), Symbol, ExprBV Symbol Symbol)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (((), Symbol, ExprBV Symbol Symbol), RRType NoReft)
-> StateT ExSt Identity ((), Symbol, ExprBV Symbol Symbol)
expToBindParg [(((), Symbol, ExprBV Symbol Symbol), RRType NoReft)]
pargs0
      return $ p { pargs = pargs' }

expToBindParg :: (((), F.Symbol, F.Expr), RSort) -> State ExSt ((), F.Symbol, F.Expr)
expToBindParg :: (((), Symbol, ExprBV Symbol Symbol), RRType NoReft)
-> StateT ExSt Identity ((), Symbol, ExprBV Symbol Symbol)
expToBindParg ((()
t, Symbol
s, ExprBV Symbol Symbol
e), RRType NoReft
s') = (ExprBV Symbol Symbol -> ((), Symbol, ExprBV Symbol Symbol))
-> StateT ExSt Identity (ExprBV Symbol Symbol)
-> StateT ExSt Identity ((), Symbol, ExprBV Symbol Symbol)
forall a b.
(a -> b) -> StateT ExSt Identity a -> StateT ExSt Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,,) ()
t Symbol
s) (ExprBV Symbol Symbol
-> RRType NoReft -> StateT ExSt Identity (ExprBV Symbol Symbol)
expToBindExpr ExprBV Symbol Symbol
e RRType NoReft
s')

expToBindExpr :: F.Expr ->  RSort -> State ExSt F.Expr
expToBindExpr :: ExprBV Symbol Symbol
-> RRType NoReft -> StateT ExSt Identity (ExprBV Symbol Symbol)
expToBindExpr e :: ExprBV Symbol Symbol
e@(EVar Symbol
s) RRType NoReft
_
  | Char -> Bool
Char.isLower (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> Char
F.headSym (Symbol -> Char) -> Symbol -> Char
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Symbol
s
  = ExprBV Symbol Symbol -> StateT ExSt Identity (ExprBV Symbol Symbol)
forall a. a -> StateT ExSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ExprBV Symbol Symbol
e
expToBindExpr ExprBV Symbol Symbol
e RRType NoReft
t
  = do s <- State ExSt Symbol
freshSymbol
       modify $ \ExSt
st -> ExSt
st{emap = M.insert s (t, e) (emap st)}
       return $ EVar s

freshSymbol :: State ExSt F.Symbol
freshSymbol :: State ExSt Symbol
freshSymbol
  = do n <- (ExSt -> Int) -> StateT ExSt Identity Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt -> Int
fresh
       modify $ \ExSt
s -> ExSt
s {fresh = n+1}
       return $ F.symbol $ "ex#" ++ show n


-- wiredInMods :: S.HashSet Ghc.ModuleName
-- wiredInMods = S.fromList $ Ghc.mkModuleName <$>
--   ["Language.Haskell.Liquid.String",
--   "Language.Haskell.Liquid.Prelude",
--   "Language.Haskell.Liquid.Foreign",
--   "Language.Haskell.Liquid.Bag",
--   "Prelude",
--   "System.IO",
--   "Data.Word",
--   "Data.Time.Calendar",
--   "Data.Set",
--   "Data.Either",
--   "Data.ByteString.Unsafe",
--   "Data.ByteString.Lazy",
--   "Data.ByteString.Short",
--   "Data.Foldable",
--   "Data.OldList",
--   "Data.Text",
--   "Data.Tuple",
--   "Data.Bits",
--   "Data.Chare",
--   "Data.String",
--   "Data.Vector",
--   "Data.Time",
--   "Data.Int",
--   "Data.Text.Fusion",
--   "Data.Map",
--   "Data.Text.Fusion.Common",
--   "KMeansHelper",
--   "Data.Text.Lazy.Fusion",
--   "Control.Exception",
--   "Control.Parallel.Strategies",
--   "Data.Traversable",
--   "GHC.Read",
--   "Data.ByteString",
--   "GHC.Classes",
--   "GHC.Ptr",
--   "GHC.Word",
--   "Language.Haskell.Liquid.Equational",
--   "GHC.Types",
--   "GHC.Num",
--   "GHC.CString",
--   "GHC.IO.Handle",
--   "GHC.Prim",
--   "GHC.Int",
--   "GHC.Base",
--   "Foreign.Ptr",
--   "GHC.ForeignPtr",
--   "GHC.List",
--   "Foreign.C.String",
--   "GHC.Exts",
--   "Foreign.Marshal.Alloc",
--   "Foreign.Marshal.Array",
--   "Foreign.C.Types",
--   "GHC.Real",
--   "Foreign.Storable",
--   "Foreign.ForeignPtr"]