-- | 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 TupleSections         #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE OverloadedStrings     #-}


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

    -- * Expand and Qualify 
  , qualifyExpand 

    -- * 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.State
import qualified Control.Exception         as Ex
import qualified Data.HashMap.Strict       as M
import qualified Data.Char                 as Char
import qualified Data.List                 as L
import qualified Text.Printf               as Printf 
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(..)) -- , Symbol, symbol) 
import qualified Language.Haskell.Liquid.GHC.Misc      as GM 
import qualified Language.Haskell.Liquid.GHC.API       as Ghc 
import qualified Language.Haskell.Liquid.Types.RefType as RT 
import           Language.Haskell.Liquid.Types         hiding (fresh)
import qualified Language.Haskell.Liquid.Misc          as Misc 
import qualified Language.Haskell.Liquid.Measure       as Ms
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

--------------------------------------------------------------------------------
-- | `makeRTEnv` initializes the env needed to `expand` refinements and types,
--   that is, the below needs to be called *before* we use `Expand.expand`
--------------------------------------------------------------------------------
makeRTEnv :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.ModSpecs -> LogicMap 
          -> BareRTEnv 
--------------------------------------------------------------------------------
makeRTEnv :: Env -> ModName -> BareSpec -> ModSpecs -> LogicMap -> BareRTEnv
makeRTEnv Env
env ModName
m BareSpec
mySpec ModSpecs
iSpecs LogicMap
lmap 
          = BareRTEnv -> BareRTEnv
renameRTArgs (BareRTEnv -> BareRTEnv) -> BareRTEnv -> BareRTEnv
forall a b. (a -> b) -> a -> b
$ [Located (RTAlias Symbol BareType)] -> BareRTEnv -> BareRTEnv
makeRTAliases [Located (RTAlias Symbol BareType)]
tAs (BareRTEnv -> BareRTEnv) -> BareRTEnv -> BareRTEnv
forall a b. (a -> b) -> a -> b
$ [Located (RTAlias Symbol Expr)] -> BareRTEnv
makeREAliases [Located (RTAlias Symbol Expr)]
eAs
  where
    tAs :: [Located (RTAlias Symbol BareType)]
tAs   = [ Located (RTAlias Symbol BareType)
t                   | (ModName
_, BareSpec
s)  <- [(ModName, BareSpec)]
specs, Located (RTAlias Symbol BareType)
t <- BareSpec -> [Located (RTAlias Symbol BareType)]
forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol BareType)]
Ms.aliases  BareSpec
s ]
    eAs :: [Located (RTAlias Symbol Expr)]
eAs   = [ Env
-> ModName
-> Located (RTAlias Symbol Expr)
-> Located (RTAlias Symbol Expr)
specREAlias Env
env ModName
m Located (RTAlias Symbol Expr)
e | (ModName
m, BareSpec
s)  <- [(ModName, BareSpec)]
specs, Located (RTAlias Symbol Expr)
e <- BareSpec -> [Located (RTAlias Symbol Expr)]
forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
Ms.ealiases BareSpec
s ]
         [Located (RTAlias Symbol Expr)]
-> [Located (RTAlias Symbol Expr)]
-> [Located (RTAlias Symbol Expr)]
forall a. [a] -> [a] -> [a]
++ [ Env
-> ModName
-> Located (RTAlias Symbol Expr)
-> Located (RTAlias Symbol Expr)
specREAlias Env
env ModName
m Located (RTAlias Symbol Expr)
e | (Symbol
_, LMap
xl) <- HashMap Symbol LMap -> [(Symbol, LMap)]
forall k v. HashMap k v -> [(k, v)]
M.toList (LogicMap -> HashMap Symbol LMap
lmSymDefs LogicMap
lmap)
                                  , let e :: Located (RTAlias Symbol Expr)
e    = LMap -> Located (RTAlias Symbol Expr)
lmapEAlias LMap
xl             ]
    specs :: [(ModName, BareSpec)]
specs = (ModName
m, BareSpec
mySpec) (ModName, BareSpec)
-> [(ModName, BareSpec)] -> [(ModName, BareSpec)]
forall a. a -> [a] -> [a]
: ModSpecs -> [(ModName, BareSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList ModSpecs
iSpecs

-- | 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 :: BareRTEnv -> BareRTEnv
renameRTArgs BareRTEnv
rte = RTE :: forall tv t.
HashMap Symbol (Located (RTAlias tv t))
-> HashMap Symbol (Located (RTAlias Symbol Expr)) -> RTEnv tv t
RTE 
  { typeAliases :: HashMap Symbol (Located (RTAlias Symbol BareType))
typeAliases = (Located (RTAlias Symbol BareType)
 -> Located (RTAlias Symbol BareType))
-> HashMap Symbol (Located (RTAlias Symbol BareType))
-> HashMap Symbol (Located (RTAlias Symbol BareType))
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((RTAlias Symbol BareType -> RTAlias Symbol BareType)
-> Located (RTAlias Symbol BareType)
-> Located (RTAlias Symbol BareType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ( 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) => RTAlias x a -> RTAlias x a
renameRTVArgs)) (BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol BareType))
forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases BareRTEnv
rte) 
  , exprAliases :: HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases = (Located (RTAlias Symbol Expr) -> Located (RTAlias Symbol Expr))
-> HashMap Symbol (Located (RTAlias Symbol Expr))
-> HashMap Symbol (Located (RTAlias Symbol Expr))
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ((RTAlias Symbol Expr -> RTAlias Symbol Expr)
-> Located (RTAlias Symbol Expr) -> Located (RTAlias Symbol Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (                        RTAlias Symbol Expr -> RTAlias Symbol Expr
forall a x. (PPrint a, Subable a) => RTAlias x a -> RTAlias x a
renameRTVArgs)) (BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol Expr))
forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases BareRTEnv
rte) 
  } 

makeREAliases :: [Located (RTAlias F.Symbol F.Expr)] -> BareRTEnv 
makeREAliases :: [Located (RTAlias Symbol Expr)] -> BareRTEnv
makeREAliases = (HashMap Symbol (Located (RTAlias Symbol Expr))
 -> Expr -> [Symbol])
-> (BareRTEnv -> Located (RTAlias Symbol Expr) -> BareRTEnv)
-> BareRTEnv
-> [Located (RTAlias Symbol Expr)]
-> BareRTEnv
forall t x thing.
PPrint t =>
(AliasTable x t -> t -> [Symbol])
-> (thing -> Located (RTAlias x t) -> thing)
-> thing
-> [Located (RTAlias x t)]
-> thing
graphExpand HashMap Symbol (Located (RTAlias Symbol Expr)) -> Expr -> [Symbol]
forall a. HashMap Symbol a -> Expr -> [Symbol]
buildExprEdges BareRTEnv -> Located (RTAlias Symbol Expr) -> BareRTEnv
f BareRTEnv
forall a. Monoid a => a
mempty 
  where
    f :: BareRTEnv -> Located (RTAlias Symbol Expr) -> BareRTEnv
f BareRTEnv
rtEnv Located (RTAlias Symbol Expr)
xt = BareRTEnv -> Located (RTAlias Symbol Expr) -> BareRTEnv
forall x t. RTEnv x t -> Located (RTAlias Symbol Expr) -> RTEnv x t
setREAlias BareRTEnv
rtEnv (BareRTEnv
-> Located (RTAlias Symbol Expr) -> Located (RTAlias Symbol Expr)
forall a. Expand a => BareRTEnv -> Located a -> Located a
expandLoc BareRTEnv
rtEnv Located (RTAlias Symbol Expr)
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 :: [Symbol]
rtTArgs = [Symbol]
ys, rtBody :: BareType
rtBody = BareType -> [(Symbol, Symbol)] -> BareType
subts (RTAlias Symbol BareType -> BareType
forall x a. RTAlias x a -> a
rtBody RTAlias Symbol BareType
rt) ([Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [Symbol]
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` RTAlias Symbol BareType -> Symbol
forall x a. RTAlias x a -> Symbol
rtName RTAlias Symbol BareType
rt) (Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs
    subts :: BareType -> [(Symbol, Symbol)] -> BareType
subts = (BareType -> (Symbol, Symbol) -> BareType)
-> BareType -> [(Symbol, Symbol)] -> BareType
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 :: BareType
rtBody = BareType -> Symbol -> BareType
forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
RT.shiftVV (RTAlias Symbol BareType -> BareType
forall x a. RTAlias x a -> a
rtBody RTAlias Symbol BareType
rt) (Maybe Integer -> Symbol
F.vv (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
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) => RTAlias x a -> RTAlias x a 
renameRTVArgs :: RTAlias x a -> RTAlias x a
renameRTVArgs RTAlias x a
rt = RTAlias x a
rt { rtVArgs :: [Symbol]
rtVArgs = [Symbol]
newArgs
                      , rtBody :: a
rtBody  = String -> a -> a
forall a. PPrint a => String -> a -> a
F.notracepp String
msg (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Subst -> a -> a
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (RTAlias x a -> a
forall x a. RTAlias x a -> a
rtBody RTAlias x a
rt) 
                      } 
  where 
    msg :: String
msg          = String
"renameRTVArgs: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Subst -> String
forall a. PPrint a => a -> String
F.showpp Subst
su
    su :: Subst
su           = [(Symbol, Expr)] -> Subst
F.mkSubst ([Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
oldArgs (Symbol -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
newArgs)) 
    newArgs :: [Symbol]
newArgs      = (Symbol -> Integer -> Symbol) -> [Symbol] -> [Integer] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Symbol -> Integer -> 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) [Integer
0..]
    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) 

makeRTAliases :: [Located (RTAlias F.Symbol BareType)] -> BareRTEnv -> BareRTEnv  
makeRTAliases :: [Located (RTAlias Symbol BareType)] -> BareRTEnv -> BareRTEnv
makeRTAliases [Located (RTAlias Symbol BareType)]
lxts BareRTEnv
rte = (HashMap Symbol (Located (RTAlias Symbol BareType))
 -> BareType -> [Symbol])
-> (BareRTEnv -> Located (RTAlias Symbol BareType) -> BareRTEnv)
-> BareRTEnv
-> [Located (RTAlias Symbol BareType)]
-> BareRTEnv
forall t x thing.
PPrint t =>
(AliasTable x t -> t -> [Symbol])
-> (thing -> Located (RTAlias x t) -> thing)
-> thing
-> [Located (RTAlias x t)]
-> thing
graphExpand HashMap Symbol (Located (RTAlias Symbol BareType))
-> BareType -> [Symbol]
forall c x t tv r.
Symbolic c =>
AliasTable x t -> RType c tv r -> [Symbol]
buildTypeEdges BareRTEnv -> Located (RTAlias Symbol BareType) -> BareRTEnv
f BareRTEnv
rte [Located (RTAlias Symbol BareType)]
lxts 
  where
    f :: BareRTEnv -> Located (RTAlias Symbol BareType) -> BareRTEnv
f BareRTEnv
rtEnv Located (RTAlias Symbol BareType)
xt         = BareRTEnv -> Located (RTAlias Symbol BareType) -> BareRTEnv
forall x t. RTEnv x t -> Located (RTAlias x t) -> RTEnv x t
setRTAlias BareRTEnv
rtEnv (BareRTEnv
-> Located (RTAlias Symbol BareType)
-> Located (RTAlias Symbol BareType)
forall a. Expand a => BareRTEnv -> Located a -> Located a
expandLoc BareRTEnv
rtEnv Located (RTAlias Symbol BareType)
xt)

specREAlias :: Bare.Env -> ModName -> Located (RTAlias F.Symbol F.Expr) -> Located (RTAlias F.Symbol F.Expr) 
specREAlias :: Env
-> ModName
-> Located (RTAlias Symbol Expr)
-> Located (RTAlias Symbol Expr)
specREAlias Env
env ModName
m Located (RTAlias Symbol Expr)
la = Located (RTAlias Symbol Expr)
-> RTAlias Symbol Expr -> Located (RTAlias Symbol Expr)
forall l b. Loc l => l -> b -> Located b
F.atLoc Located (RTAlias Symbol Expr)
la (RTAlias Symbol Expr -> Located (RTAlias Symbol Expr))
-> RTAlias Symbol Expr -> Located (RTAlias Symbol Expr)
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol Expr
a { rtBody :: Expr
rtBody = Env -> ModName -> SourcePos -> [Symbol] -> Expr -> Expr
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
Bare.qualify Env
env ModName
m (Located (RTAlias Symbol Expr) -> SourcePos
forall a. Located a -> SourcePos
loc Located (RTAlias Symbol Expr)
la) (RTAlias Symbol Expr -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol Expr
a) (RTAlias Symbol Expr -> Expr
forall x a. RTAlias x a -> a
rtBody RTAlias Symbol Expr
a) } 
  where 
    a :: RTAlias Symbol Expr
a     = Located (RTAlias Symbol Expr) -> RTAlias Symbol Expr
forall a. Located a -> a
val Located (RTAlias Symbol Expr)
la 

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

graphExpand :: (PPrint t)
            => (AliasTable x t -> t -> [F.Symbol])         -- ^ dependencies
            -> (thing -> Located (RTAlias x t) -> thing) -- ^ update
            -> thing                                     -- ^ initial
            -> [Located (RTAlias x t)]                   -- ^ vertices
            -> thing                                     -- ^ final 
graphExpand :: (AliasTable x t -> t -> [Symbol])
-> (thing -> Located (RTAlias x t) -> thing)
-> thing
-> [Located (RTAlias x t)]
-> thing
graphExpand AliasTable x t -> t -> [Symbol]
buildEdges thing -> Located (RTAlias x t) -> thing
expBody thing
env [Located (RTAlias x t)]
lxts 
           = (thing -> Located (RTAlias x t) -> thing)
-> thing -> [Located (RTAlias x t)] -> thing
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' thing -> Located (RTAlias x t) -> thing
expBody thing
env (AliasTable x t -> Graph Symbol -> [Located (RTAlias x t)]
forall x t.
AliasTable x t -> Graph Symbol -> [Located (RTAlias x t)]
genExpandOrder AliasTable x t
table' Graph Symbol
graph)
  where 
    -- xts    = val <$> lxts
    table :: AliasTable x t
table  = [Located (RTAlias x t)] -> AliasTable x t
forall x t. [Located (RTAlias x t)] -> AliasTable x t
buildAliasTable [Located (RTAlias x t)]
lxts
    graph :: Graph Symbol
graph  = (t -> [Symbol]) -> [Located (RTAlias x t)] -> Graph Symbol
forall t x.
PPrint t =>
(t -> [Symbol]) -> [Located (RTAlias x t)] -> Graph Symbol
buildAliasGraph (AliasTable x t -> t -> [Symbol]
buildEdges AliasTable x t
table) [Located (RTAlias x t)]
lxts
    table' :: AliasTable x t
table' = AliasTable x t -> Graph Symbol -> AliasTable x t
forall x t. AliasTable x t -> Graph Symbol -> AliasTable x t
checkCyclicAliases AliasTable x t
table Graph Symbol
graph

setRTAlias :: RTEnv x t -> Located (RTAlias x t) -> RTEnv x t 
setRTAlias :: RTEnv x t -> Located (RTAlias x t) -> RTEnv x t
setRTAlias RTEnv x t
env Located (RTAlias x t)
a = RTEnv x t
env { typeAliases :: HashMap Symbol (Located (RTAlias x t))
typeAliases =  Symbol
-> Located (RTAlias x t)
-> HashMap Symbol (Located (RTAlias x t))
-> HashMap Symbol (Located (RTAlias x t))
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
n Located (RTAlias x t)
a (RTEnv x t -> HashMap Symbol (Located (RTAlias x t))
forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases RTEnv x t
env) } 
  where 
    n :: Symbol
n            = RTAlias x t -> Symbol
forall x a. RTAlias x a -> Symbol
rtName (Located (RTAlias x t) -> RTAlias x t
forall a. Located a -> a
val Located (RTAlias x t)
a)  

setREAlias :: RTEnv x t -> Located (RTAlias F.Symbol F.Expr) -> RTEnv x t 
setREAlias :: RTEnv x t -> Located (RTAlias Symbol Expr) -> RTEnv x t
setREAlias RTEnv x t
env Located (RTAlias Symbol Expr)
a = RTEnv x t
env { exprAliases :: HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases = Symbol
-> Located (RTAlias Symbol Expr)
-> HashMap Symbol (Located (RTAlias Symbol Expr))
-> HashMap Symbol (Located (RTAlias Symbol Expr))
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
n Located (RTAlias Symbol Expr)
a (RTEnv x t -> HashMap Symbol (Located (RTAlias Symbol Expr))
forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases RTEnv x t
env) } 
  where 
    n :: Symbol
n            = RTAlias Symbol Expr -> Symbol
forall x a. RTAlias x a -> Symbol
rtName (Located (RTAlias Symbol Expr) -> RTAlias Symbol Expr
forall a. Located a -> a
val Located (RTAlias Symbol Expr)
a)



--------------------------------------------------------------------------------
type AliasTable x t = M.HashMap F.Symbol (Located (RTAlias x t))

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

fromAliasSymbol :: AliasTable x t -> F.Symbol -> Located (RTAlias x t)
fromAliasSymbol :: AliasTable x t -> Symbol -> Located (RTAlias x t)
fromAliasSymbol AliasTable x t
table Symbol
sym
  = Located (RTAlias x t)
-> Maybe (Located (RTAlias x t)) -> Located (RTAlias x t)
forall a. a -> Maybe a -> a
fromMaybe Located (RTAlias x t)
forall a. a
err (Symbol -> AliasTable x t -> Maybe (Located (RTAlias x t))
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
sym AliasTable x t
table)
  where
    err :: a
err = Maybe SrcSpan -> String -> a
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String
"fromAliasSymbol: Dangling alias symbol: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show Symbol
sym)

type Graph t = [Node t]
type Node  t = (t, t, [t])

buildAliasGraph :: (PPrint t) => (t -> [F.Symbol]) -> [Located (RTAlias x t)] 
                -> Graph F.Symbol
buildAliasGraph :: (t -> [Symbol]) -> [Located (RTAlias x t)] -> Graph Symbol
buildAliasGraph t -> [Symbol]
buildEdges = (Located (RTAlias x t) -> Node Symbol)
-> [Located (RTAlias x t)] -> Graph Symbol
forall a b. (a -> b) -> [a] -> [b]
map ((t -> [Symbol]) -> Located (RTAlias x t) -> Node Symbol
forall t x.
PPrint t =>
(t -> [Symbol]) -> Located (RTAlias x t) -> Node Symbol
buildAliasNode t -> [Symbol]
buildEdges)

buildAliasNode :: (PPrint t) => (t -> [F.Symbol]) -> Located (RTAlias x t) 
               -> Node F.Symbol
buildAliasNode :: (t -> [Symbol]) -> Located (RTAlias x t) -> Node Symbol
buildAliasNode t -> [Symbol]
f Located (RTAlias x t)
la = (RTAlias x t -> Symbol
forall x a. RTAlias x a -> Symbol
rtName RTAlias x t
a, RTAlias x t -> Symbol
forall x a. RTAlias x a -> Symbol
rtName RTAlias x t
a, t -> [Symbol]
f (RTAlias x t -> t
forall x a. RTAlias x a -> a
rtBody RTAlias x t
a))
  where 
    a :: RTAlias x t
a               = Located (RTAlias x t) -> RTAlias x t
forall a. Located a -> a
val Located (RTAlias x t)
la 

checkCyclicAliases :: AliasTable x t -> Graph F.Symbol -> AliasTable x t 
checkCyclicAliases :: AliasTable x t -> Graph Symbol -> AliasTable x t
checkCyclicAliases AliasTable x t
table Graph Symbol
graph
  = case (SCC Symbol -> Maybe [Symbol]) -> [SCC Symbol] -> [[Symbol]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SCC Symbol -> Maybe [Symbol]
forall vertex. SCC vertex -> Maybe [vertex]
go (Graph Symbol -> [SCC Symbol]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp Graph Symbol
graph) of
      []   -> AliasTable x t
table 
      [[Symbol]]
sccs -> [Error] -> AliasTable x t
forall a e. Exception e => e -> a
Ex.throw (AliasTable x t -> [Symbol] -> Error
forall x t. AliasTable x t -> [Symbol] -> Error
cycleAliasErr AliasTable x t
table ([Symbol] -> Error) -> [[Symbol]] -> [Error]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Symbol]]
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 -> [F.Symbol] -> Error
cycleAliasErr :: AliasTable x t -> [Symbol] -> Error
cycleAliasErr AliasTable x t
_ []          = Maybe SrcSpan -> String -> Error
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"checkCyclicAliases: No type aliases in reported cycle"
cycleAliasErr AliasTable x t
t scc :: [Symbol]
scc@(Symbol
rta:[Symbol]
_) = ErrAliasCycle :: forall t. SrcSpan -> [(SrcSpan, Doc)] -> TError t
ErrAliasCycle { pos :: SrcSpan
pos    = (SrcSpan, Doc) -> SrcSpan
forall a b. (a, b) -> a
fst (Symbol -> (SrcSpan, Doc)
locate Symbol
rta)
                                            , acycle :: [(SrcSpan, Doc)]
acycle = (Symbol -> (SrcSpan, Doc)) -> [Symbol] -> [(SrcSpan, Doc)]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> (SrcSpan, Doc)
locate [Symbol]
scc }
  where
    locate :: Symbol -> (SrcSpan, Doc)
locate Symbol
sym = ( Located (RTAlias x t) -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located (RTAlias x t) -> SrcSpan)
-> Located (RTAlias x t) -> SrcSpan
forall a b. (a -> b) -> a -> b
$ AliasTable x t -> Symbol -> Located (RTAlias x t)
forall x t. AliasTable x t -> Symbol -> Located (RTAlias x t)
fromAliasSymbol AliasTable x t
t Symbol
sym
                 , Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
sym )


genExpandOrder :: AliasTable x t -> Graph F.Symbol -> [Located (RTAlias x t)]
genExpandOrder :: AliasTable x t -> Graph Symbol -> [Located (RTAlias x t)]
genExpandOrder AliasTable x t
table Graph Symbol
graph
  = (Symbol -> Located (RTAlias x t))
-> [Symbol] -> [Located (RTAlias x t)]
forall a b. (a -> b) -> [a] -> [b]
map (AliasTable x t -> Symbol -> Located (RTAlias x t)
forall x t. AliasTable x t -> Symbol -> Located (RTAlias x t)
fromAliasSymbol AliasTable x t
table) [Symbol]
symOrder
  where
    (Graph
digraph, Vertex -> Node Symbol
lookupVertex, Symbol -> Maybe Vertex
_)
      = Graph Symbol
-> (Graph, Vertex -> Node Symbol, Symbol -> Maybe Vertex)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Vertex -> (node, key, [key]), key -> Maybe Vertex)
graphFromEdges Graph Symbol
graph
    symOrder :: [Symbol]
symOrder
      = (Vertex -> Symbol) -> [Vertex] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Node Symbol -> Symbol
forall a b c. (a, b, c) -> a
Misc.fst3 (Node Symbol -> Symbol)
-> (Vertex -> Node Symbol) -> Vertex -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vertex -> Node Symbol
lookupVertex) ([Vertex] -> [Symbol]) -> [Vertex] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ [Vertex] -> [Vertex]
forall a. [a] -> [a]
reverse ([Vertex] -> [Vertex]) -> [Vertex] -> [Vertex]
forall a b. (a -> b) -> a -> b
$ Graph -> [Vertex]
topSort Graph
digraph

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

ordNub :: Ord a => [a] -> [a]
ordNub :: [a] -> [a]
ordNub = ([a] -> a) -> [[a]] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> a
forall a. [a] -> a
head ([[a]] -> [a]) -> ([a] -> [[a]]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [[a]]
forall a. Eq a => [a] -> [[a]]
L.group ([a] -> [[a]]) -> ([a] -> [a]) -> [a] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [a]
forall a. Ord a => [a] -> [a]
L.sort

buildTypeEdges :: (F.Symbolic c) => AliasTable x t -> RType c tv r -> [F.Symbol]
buildTypeEdges :: AliasTable x t -> RType c tv r -> [Symbol]
buildTypeEdges AliasTable x t
table = [Symbol] -> [Symbol]
forall a. Ord a => [a] -> [a]
ordNub ([Symbol] -> [Symbol])
-> (RType c tv r -> [Symbol]) -> RType c tv r -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType c tv r -> [Symbol]
forall c tv r. Symbolic c => RType c tv r -> [Symbol]
go
  where
    -- go :: t -> [Symbol]
    go :: RType c tv r -> [Symbol]
go (RApp c
c [RType c tv r]
ts [RTProp c tv r]
rs r
_) = Symbol -> [Symbol]
go_alias (c -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol c
c) [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (RType c tv r -> [Symbol]) -> [RType c tv r] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RType c tv r -> [Symbol]
go [RType c tv r]
ts [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (RType c tv r -> [Symbol]) -> [RType c tv r] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RType c tv r -> [Symbol]
go ((RTProp c tv r -> Maybe (RType c tv r))
-> [RTProp c tv r] -> [RType c tv r]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe RTProp c tv r -> Maybe (RType c tv r)
forall τ c tv r. Ref τ (RType c tv r) -> Maybe (RType c tv r)
go_ref [RTProp c tv r]
rs)
    go (RImpF Symbol
_ RType c tv r
t1 RType c tv r
t2 r
_) = RType c tv r -> [Symbol]
go RType c tv r
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RType c tv r -> [Symbol]
go RType c tv r
t2
    go (RFun Symbol
_ RType c tv r
t1 RType c tv r
t2 r
_) = RType c tv r -> [Symbol]
go RType c tv r
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RType c tv r -> [Symbol]
go RType c tv r
t2
    go (RAppTy RType c tv r
t1 RType c tv r
t2 r
_) = RType c tv r -> [Symbol]
go RType c tv r
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RType c tv r -> [Symbol]
go RType c tv r
t2
    go (RAllE Symbol
_ RType c tv r
t1 RType c tv r
t2)  = RType c tv r -> [Symbol]
go RType c tv r
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RType c tv r -> [Symbol]
go RType c tv r
t2
    go (REx Symbol
_ RType c tv r
t1 RType c tv r
t2)    = RType c tv r -> [Symbol]
go RType c tv r
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RType c tv r -> [Symbol]
go RType c tv r
t2
    go (RAllT RTVU c tv
_ RType c tv r
t r
_)    = RType c tv r -> [Symbol]
go RType c tv r
t
    go (RAllP PVU c tv
_ RType c tv r
t)      = RType c tv r -> [Symbol]
go RType c tv r
t
    go (RVar tv
_ r
_)       = []
    go (RExprArg Located Expr
_)     = []
    go (RHole r
_)        = []
    go (RRTy [(Symbol, RType c tv r)]
env r
_ Oblig
_ RType c tv r
t) = ((Symbol, RType c tv r) -> [Symbol])
-> [(Symbol, RType c tv r)] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (RType c tv r -> [Symbol]
go (RType c tv r -> [Symbol])
-> ((Symbol, RType c tv r) -> RType c tv r)
-> (Symbol, RType c tv r)
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, RType c tv r) -> RType c tv r
forall a b. (a, b) -> b
snd) [(Symbol, RType c tv r)]
env [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RType c tv r -> [Symbol]
go RType c tv r
t
    go_alias :: Symbol -> [Symbol]
go_alias Symbol
c          = [Symbol
c | Symbol -> AliasTable x t -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Symbol
c AliasTable x t
table]
    go_ref :: Ref τ (RType c tv r) -> Maybe (RType c tv r)
go_ref (RProp [(Symbol, τ)]
_ (RHole r
_)) = Maybe (RType c tv r)
forall a. Maybe a
Nothing
    go_ref (RProp  [(Symbol, τ)]
_ RType c tv r
t) = RType c tv r -> Maybe (RType c tv r)
forall a. a -> Maybe a
Just RType c tv r
t

buildExprEdges :: M.HashMap F.Symbol a -> F.Expr -> [F.Symbol]
buildExprEdges :: HashMap Symbol a -> Expr -> [Symbol]
buildExprEdges HashMap Symbol a
table  = [Symbol] -> [Symbol]
forall a. Ord a => [a] -> [a]
ordNub ([Symbol] -> [Symbol]) -> (Expr -> [Symbol]) -> Expr -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Symbol]
go
  where
    go :: F.Expr -> [F.Symbol]
    go :: Expr -> [Symbol]
go (EApp Expr
e1 Expr
e2)   = Expr -> [Symbol]
go Expr
e1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ Expr -> [Symbol]
go Expr
e2
    go (ENeg Expr
e)       = Expr -> [Symbol]
go Expr
e
    go (EBin Bop
_ Expr
e1 Expr
e2) = Expr -> [Symbol]
go Expr
e1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ Expr -> [Symbol]
go Expr
e2
    go (EIte Expr
_ Expr
e1 Expr
e2) = Expr -> [Symbol]
go Expr
e1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ Expr -> [Symbol]
go Expr
e2
    go (ECst Expr
e Sort
_)     = Expr -> [Symbol]
go Expr
e
    go (ESym SymConst
_)       = []
    go (ECon Constant
_)       = []
    go (EVar Symbol
v)       = Symbol -> [Symbol]
go_alias Symbol
v
    go (PAnd [Expr]
ps)       = (Expr -> [Symbol]) -> [Expr] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Symbol]
go [Expr]
ps
    go (POr [Expr]
ps)        = (Expr -> [Symbol]) -> [Expr] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Symbol]
go [Expr]
ps
    go (PNot Expr
p)        = Expr -> [Symbol]
go Expr
p
    go (PImp Expr
p Expr
q)      = Expr -> [Symbol]
go Expr
p [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ Expr -> [Symbol]
go Expr
q
    go (PIff Expr
p Expr
q)      = Expr -> [Symbol]
go Expr
p [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ Expr -> [Symbol]
go Expr
q
    go (PAll [(Symbol, Sort)]
_ Expr
p)      = Expr -> [Symbol]
go Expr
p
    go (ELam (Symbol, Sort)
_ Expr
e)      = Expr -> [Symbol]
go Expr
e
    go (ECoerc Sort
_ Sort
_ Expr
e)  = Expr -> [Symbol]
go Expr
e
    go (PAtom Brel
_ Expr
e1 Expr
e2) = Expr -> [Symbol]
go Expr
e1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ Expr -> [Symbol]
go Expr
e2
    go (ETApp Expr
e Sort
_)     = Expr -> [Symbol]
go Expr
e
    go (ETAbs Expr
e Symbol
_)     = Expr -> [Symbol]
go Expr
e
    go (PKVar KVar
_ Subst
_)     = []
    go (PExist [(Symbol, Sort)]
_ Expr
e)    = Expr -> [Symbol]
go Expr
e
    go (PGrad KVar
_ Subst
_ GradInfo
_ Expr
e) = Expr -> [Symbol]
go Expr
e
    go_alias :: Symbol -> [Symbol]
go_alias Symbol
f         = [Symbol
f | Symbol -> HashMap Symbol a -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Symbol
f HashMap Symbol a
table ]


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

----------------------------------------------------------------------------------
-- | @qualifyExpand@ first qualifies names so that we can successfully resolve 
--   them during expansion. 
----------------------------------------------------------------------------------
qualifyExpand :: (Expand a, Bare.Qualify a) 
              => Bare.Env -> ModName -> BareRTEnv -> F.SourcePos -> [F.Symbol] -> a -> a 
----------------------------------------------------------------------------------
qualifyExpand :: Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [Symbol]
bs
  = BareRTEnv -> SourcePos -> a -> a
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l  
  (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> SourcePos -> [Symbol] -> a -> a
forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
Bare.qualify Env
env ModName
name SourcePos
l [Symbol]
bs

----------------------------------------------------------------------------------
expandLoc :: (Expand a) => BareRTEnv -> Located a -> Located a 
expandLoc :: BareRTEnv -> Located a -> Located a
expandLoc BareRTEnv
rtEnv Located a
lx = BareRTEnv -> SourcePos -> a -> a
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
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 :: BareRTEnv -> SourcePos -> Expr -> Expr
expand = BareRTEnv -> SourcePos -> Expr -> Expr
expandExpr 

instance Expand F.Reft where
  expand :: BareRTEnv -> SourcePos -> Reft -> Reft
expand BareRTEnv
rtEnv SourcePos
l (F.Reft (Symbol
v, Expr
ra)) = (Symbol, Expr) -> Reft
F.Reft (Symbol
v, BareRTEnv -> SourcePos -> Expr -> Expr
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l Expr
ra) 

instance Expand RReft where
  expand :: BareRTEnv -> SourcePos -> RReft -> RReft
expand BareRTEnv
rtEnv SourcePos
l = (Reft -> Reft) -> RReft -> RReft
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BareRTEnv -> SourcePos -> Reft -> Reft
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l)

expandReft :: (Expand r) => BareRTEnv -> F.SourcePos -> RType c tv r -> RType c tv r 
expandReft :: BareRTEnv -> SourcePos -> RType c tv r -> RType c tv r
expandReft BareRTEnv
rtEnv SourcePos
l = (r -> r) -> RType c tv r -> RType c tv r
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BareRTEnv -> SourcePos -> r -> r
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
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 :: BareRTEnv -> SourcePos -> SpecType -> SpecType
expand = BareRTEnv -> SourcePos -> SpecType -> SpecType
forall r c tv.
Expand r =>
BareRTEnv -> 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 :: BareRTEnv -> SourcePos -> BareType -> BareType
expand BareRTEnv
rtEnv SourcePos
l 
    = BareRTEnv -> SourcePos -> BareType -> BareType
forall r c tv.
Expand r =>
BareRTEnv -> SourcePos -> RType c tv r -> RType c tv r
expandReft     BareRTEnv
rtEnv SourcePos
l -- apply expression aliases 
    (BareType -> BareType)
-> (BareType -> BareType) -> BareType -> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareRTEnv -> SourcePos -> BareType -> BareType
expandBareType BareRTEnv
rtEnv SourcePos
l -- apply type       aliases 

instance Expand (RTAlias F.Symbol Expr) where 
  expand :: BareRTEnv
-> SourcePos -> RTAlias Symbol Expr -> RTAlias Symbol Expr
expand BareRTEnv
rtEnv SourcePos
l RTAlias Symbol Expr
x = RTAlias Symbol Expr
x { rtBody :: Expr
rtBody = BareRTEnv -> SourcePos -> Expr -> Expr
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (RTAlias Symbol Expr -> Expr
forall x a. RTAlias x a -> a
rtBody RTAlias Symbol Expr
x) } 

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

instance Expand Body where 
  expand :: BareRTEnv -> SourcePos -> Body -> Body
expand BareRTEnv
rtEnv SourcePos
l (P   Expr
p) = Expr -> Body
P   (BareRTEnv -> SourcePos -> Expr -> Expr
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l Expr
p) 
  expand BareRTEnv
rtEnv SourcePos
l (E   Expr
e) = Expr -> Body
E   (BareRTEnv -> SourcePos -> Expr -> Expr
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l Expr
e)
  expand BareRTEnv
rtEnv SourcePos
l (R Symbol
x Expr
p) = Symbol -> Expr -> Body
R Symbol
x (BareRTEnv -> SourcePos -> Expr -> Expr
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l Expr
p)

instance Expand DataCtor where 
  expand :: BareRTEnv -> SourcePos -> DataCtor -> DataCtor
expand BareRTEnv
rtEnv SourcePos
l DataCtor
c = DataCtor
c
    { dcTheta :: [BareType]
dcTheta  = BareRTEnv -> SourcePos -> [BareType] -> [BareType]
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (DataCtor -> [BareType]
dcTheta DataCtor
c) 
    , dcFields :: [(Symbol, BareType)]
dcFields = [(Symbol
x, BareRTEnv -> SourcePos -> BareType -> BareType
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l BareType
t) | (Symbol
x, BareType
t) <- DataCtor -> [(Symbol, BareType)]
dcFields DataCtor
c ] 
    , dcResult :: Maybe BareType
dcResult = BareRTEnv -> SourcePos -> Maybe BareType -> Maybe BareType
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (DataCtor -> Maybe BareType
dcResult DataCtor
c)
    }
 
instance Expand DataDecl where 
  expand :: BareRTEnv -> SourcePos -> DataDecl -> DataDecl
expand BareRTEnv
rtEnv SourcePos
l DataDecl
d = DataDecl
d 
    { tycDCons :: [DataCtor]
tycDCons  = BareRTEnv -> SourcePos -> [DataCtor] -> [DataCtor]
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (DataDecl -> [DataCtor]
tycDCons  DataDecl
d)
    , tycPropTy :: Maybe BareType
tycPropTy = BareRTEnv -> SourcePos -> Maybe BareType -> Maybe BareType
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (DataDecl -> Maybe BareType
tycPropTy DataDecl
d) 
    } 

instance Expand BareMeasure where 
  expand :: BareRTEnv -> SourcePos -> BareMeasure -> BareMeasure
expand BareRTEnv
rtEnv SourcePos
l BareMeasure
m = BareMeasure
m 
    { msSort :: LocBareType
msSort = BareRTEnv -> SourcePos -> LocBareType -> LocBareType
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (BareMeasure -> LocBareType
forall ty ctor. Measure ty ctor -> ty
msSort BareMeasure
m) 
    , msEqns :: [Def LocBareType LocSymbol]
msEqns = BareRTEnv
-> SourcePos
-> [Def LocBareType LocSymbol]
-> [Def LocBareType LocSymbol]
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (BareMeasure -> [Def LocBareType LocSymbol]
forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns BareMeasure
m)
    } 

instance Expand BareDef where 
  expand :: BareRTEnv
-> SourcePos
-> Def LocBareType LocSymbol
-> Def LocBareType LocSymbol
expand BareRTEnv
rtEnv SourcePos
l Def LocBareType LocSymbol
d = Def LocBareType LocSymbol
d 
    { dsort :: Maybe LocBareType
dsort = BareRTEnv -> SourcePos -> Maybe LocBareType -> Maybe LocBareType
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (Def LocBareType LocSymbol -> Maybe LocBareType
forall ty ctor. Def ty ctor -> Maybe ty
dsort Def LocBareType LocSymbol
d) 
    , binds :: [(Symbol, Maybe LocBareType)]
binds = [ (Symbol
x, BareRTEnv -> SourcePos -> Maybe LocBareType -> Maybe LocBareType
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l Maybe LocBareType
t) | (Symbol
x, Maybe LocBareType
t) <- Def LocBareType LocSymbol -> [(Symbol, Maybe LocBareType)]
forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def LocBareType LocSymbol
d] 
    , body :: Body
body  = BareRTEnv -> SourcePos -> Body -> Body
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (Def LocBareType LocSymbol -> Body
forall ty ctor. Def ty ctor -> Body
body  Def LocBareType LocSymbol
d) 
    } 

instance Expand Ms.BareSpec where 
  expand :: BareRTEnv -> SourcePos -> BareSpec -> BareSpec
expand = BareRTEnv -> SourcePos -> BareSpec -> BareSpec
expandBareSpec

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

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

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

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

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

expandBareSpec :: BareRTEnv -> F.SourcePos -> Ms.BareSpec -> Ms.BareSpec
expandBareSpec :: BareRTEnv -> SourcePos -> BareSpec -> BareSpec
expandBareSpec BareRTEnv
rtEnv SourcePos
l BareSpec
sp = BareSpec
sp 
  { measures :: [BareMeasure]
measures   = BareRTEnv -> SourcePos -> [BareMeasure] -> [BareMeasure]
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (BareSpec -> [BareMeasure]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures   BareSpec
sp) 
  , asmSigs :: [(LocSymbol, LocBareType)]
asmSigs    = BareRTEnv
-> SourcePos
-> [(LocSymbol, LocBareType)]
-> [(LocSymbol, LocBareType)]
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs    BareSpec
sp)
  , sigs :: [(LocSymbol, LocBareType)]
sigs       = BareRTEnv
-> SourcePos
-> [(LocSymbol, LocBareType)]
-> [(LocSymbol, LocBareType)]
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs       BareSpec
sp)
  , localSigs :: [(LocSymbol, LocBareType)]
localSigs  = BareRTEnv
-> SourcePos
-> [(LocSymbol, LocBareType)]
-> [(LocSymbol, LocBareType)]
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
localSigs  BareSpec
sp)
  , reflSigs :: [(LocSymbol, LocBareType)]
reflSigs   = BareRTEnv
-> SourcePos
-> [(LocSymbol, LocBareType)]
-> [(LocSymbol, LocBareType)]
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (BareSpec -> [(LocSymbol, LocBareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
reflSigs   BareSpec
sp)
  , ialiases :: [(LocBareType, LocBareType)]
ialiases   = [ (LocBareType -> LocBareType
f LocBareType
x, LocBareType -> LocBareType
f LocBareType
y) | (LocBareType
x, LocBareType
y) <- BareSpec -> [(LocBareType, LocBareType)]
forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases BareSpec
sp ]
  , dataDecls :: [DataDecl]
dataDecls  = BareRTEnv -> SourcePos -> [DataDecl] -> [DataDecl]
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (BareSpec -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls  BareSpec
sp)
  , newtyDecls :: [DataDecl]
newtyDecls = BareRTEnv -> SourcePos -> [DataDecl] -> [DataDecl]
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (BareSpec -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls BareSpec
sp)
  } 
  where f :: LocBareType -> LocBareType
f      = BareRTEnv -> SourcePos -> LocBareType -> LocBareType
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l 
  
expandBareType :: BareRTEnv -> F.SourcePos -> BareType -> BareType 
expandBareType :: BareRTEnv -> SourcePos -> BareType -> BareType
expandBareType BareRTEnv
rtEnv SourcePos
_ = BareType -> BareType
go 
  where
    go :: BareType -> BareType
go (RApp BTyCon
c [BareType]
ts [RTProp BTyCon BTyVar RReft]
rs RReft
r)  = case BTyCon -> BareRTEnv -> Maybe (Located (RTAlias Symbol BareType))
lookupRTEnv BTyCon
c BareRTEnv
rtEnv of 
                             Just Located (RTAlias Symbol BareType)
rta -> SourcePos
-> Located (RTAlias Symbol BareType)
-> [BareType]
-> RReft
-> BareType
expandRTAliasApp (BTyCon -> SourcePos
forall a. Loc a => a -> SourcePos
GM.fSourcePos BTyCon
c) Located (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) RReft
r 
                             Maybe (Located (RTAlias Symbol BareType))
Nothing  -> BTyCon
-> [BareType] -> [RTProp BTyCon BTyVar RReft] -> RReft -> BareType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType 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) (RTProp BTyCon BTyVar RReft -> RTProp BTyCon BTyVar RReft
goRef (RTProp BTyCon BTyVar RReft -> RTProp BTyCon BTyVar RReft)
-> [RTProp BTyCon BTyVar RReft] -> [RTProp BTyCon BTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTProp BTyCon BTyVar RReft]
rs) RReft
r 
    go (RAppTy BareType
t1 BareType
t2 RReft
r)  = BareType -> BareType -> RReft -> BareType
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2) RReft
r
    go (RImpF Symbol
x BareType
t1 BareType
t2 RReft
r) = Symbol -> BareType -> BareType -> RReft -> BareType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RImpF Symbol
x (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2) RReft
r 
    go (RFun  Symbol
x BareType
t1 BareType
t2 RReft
r) = Symbol -> BareType -> BareType -> RReft -> BareType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun  Symbol
x (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2) RReft
r 
    go (RAllT RTVU BTyCon BTyVar
a BareType
t RReft
r)     = RTVU BTyCon BTyVar -> BareType -> RReft -> BareType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU BTyCon BTyVar
a (BareType -> BareType
go BareType
t) RReft
r
    go (RAllP PVU BTyCon BTyVar
a BareType
t)       = PVU BTyCon BTyVar -> BareType -> BareType
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVU BTyCon BTyVar
a (BareType -> BareType
go BareType
t) 
    go (RAllE Symbol
x BareType
t1 BareType
t2)   = Symbol -> BareType -> BareType -> BareType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType 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 c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx   Symbol
x (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2)
    go (RRTy [(Symbol, BareType)]
e RReft
r Oblig
o BareType
t)    = [(Symbol, BareType)] -> RReft -> Oblig -> BareType -> BareType
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy  [(Symbol, BareType)]
e RReft
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 :: RTProp BTyCon BTyVar RReft -> RTProp BTyCon BTyVar RReft
goRef (RProp [(Symbol, RType BTyCon BTyVar ())]
ss BareType
t)   = [(Symbol, RType BTyCon BTyVar ())]
-> BareType -> RTProp BTyCon BTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType BTyCon BTyVar ())]
ss (BareType -> BareType
go BareType
t)

lookupRTEnv :: BTyCon -> BareRTEnv -> Maybe (Located BareRTAlias)
lookupRTEnv :: BTyCon -> BareRTEnv -> Maybe (Located (RTAlias Symbol BareType))
lookupRTEnv BTyCon
c BareRTEnv
rtEnv = Symbol
-> HashMap Symbol (Located (RTAlias Symbol BareType))
-> Maybe (Located (RTAlias Symbol BareType))
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (BTyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol BTyCon
c) (BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol BareType))
forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases BareRTEnv
rtEnv)

expandRTAliasApp :: F.SourcePos -> Located BareRTAlias -> [BareType] -> RReft -> BareType 
expandRTAliasApp :: SourcePos
-> Located (RTAlias Symbol BareType)
-> [BareType]
-> RReft
-> BareType
expandRTAliasApp SourcePos
l (Loc SourcePos
la SourcePos
_ RTAlias Symbol BareType
rta) [BareType]
args RReft
r = case Maybe Error
isOK of 
  Just Error
e     -> Error -> BareType
forall a e. Exception e => e -> a
Ex.throw Error
e
  Maybe Error
Nothing    -> Subst -> BareType -> BareType
forall a. Subable a => Subst -> a -> a
F.subst Subst
esu (BareType -> BareType)
-> (BareType -> BareType) -> BareType -> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BareType -> RReft -> BareType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` RReft
r) (BareType -> BareType)
-> (BareType -> BareType) -> BareType -> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(BTyVar, RType BTyCon BTyVar (), BareType)]
-> BareType -> BareType
forall tv (t :: * -> *) r c.
(Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
RT.subsTyVars_meet [(BTyVar, RType BTyCon BTyVar (), 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, RType BTyCon BTyVar (), BareType)]
tsu       = (BTyVar -> BareType -> (BTyVar, RType BTyCon BTyVar (), BareType))
-> [BTyVar]
-> [BareType]
-> [(BTyVar, RType BTyCon BTyVar (), BareType)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\BTyVar
α BareType
t -> (BTyVar
α, BareType -> RType BTyCon BTyVar ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort BareType
t, BareType
t)) [BTyVar]
αs [BareType]
ts
    esu :: Subst
esu       = [(Symbol, Expr)] -> Subst
F.mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
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) [Expr]
es
    es :: [Expr]
es        = SourcePos -> String -> BareType -> Expr
exprArg SourcePos
l String
msg (BareType -> Expr) -> [BareType] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
es0
    ([BareType]
ts, [BareType]
es0) = Vertex -> [BareType] -> ([BareType], [BareType])
forall a. Vertex -> [a] -> ([a], [a])
splitAt Vertex
nαs [BareType]
args
    ([BTyVar]
αs, [Symbol]
εs)  = (Symbol -> BTyVar
BTV (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 :: String
msg       = String
"EXPAND-RTALIAS-APP: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
F.showpp (RTAlias Symbol BareType -> Symbol
forall x a. RTAlias x a -> Symbol
rtName RTAlias Symbol BareType
rta)
    nαs :: Vertex
nαs       = [BTyVar] -> Vertex
forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [BTyVar]
αs
    nεs :: Vertex
nεs       = [Symbol] -> Vertex
forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [Symbol]
εs 
    nargs :: Vertex
nargs     = [BareType] -> Vertex
forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [BareType]
args 
    ntargs :: Vertex
ntargs    = [BareType] -> Vertex
forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [BareType]
targs
    neargs :: Vertex
neargs    = [BareType] -> Vertex
forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [BareType]
eargs
    err :: Doc -> Maybe Error
err       = SourcePos
-> SourcePos -> RTAlias Symbol BareType -> Doc -> Maybe Error
errRTAliasApp SourcePos
l SourcePos
la RTAlias Symbol BareType
rta 
    isOK :: Maybe Error
    isOK :: Maybe Error
isOK
      | Vertex
nargs Vertex -> Vertex -> Bool
forall a. Eq a => a -> a -> Bool
/= Vertex
ntargs Vertex -> Vertex -> Vertex
forall a. Num a => a -> a -> a
+ Vertex
neargs
      = Doc -> Maybe Error
err (Doc -> Maybe Error) -> Doc -> Maybe Error
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
PJ.hsep [Doc
"Expects", Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint Vertex
nαs, Doc
"type arguments and then", Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint Vertex
nεs, Doc
"expression arguments, but is given", Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint Vertex
nargs]
      | Vertex
nargs Vertex -> Vertex -> Bool
forall a. Eq a => a -> a -> Bool
/= Vertex
nαs Vertex -> Vertex -> Vertex
forall a. Num a => a -> a -> a
+ Vertex
nεs
      = Doc -> Maybe Error
err (Doc -> Maybe Error) -> Doc -> Maybe Error
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
PJ.hsep [Doc
"Expects", Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint Vertex
nαs, Doc
"type arguments and "    , Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint Vertex
nεs, Doc
"expression arguments, but is given", Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint Vertex
nargs]
      | Vertex
nαs Vertex -> Vertex -> Bool
forall a. Eq a => a -> a -> Bool
/= Vertex
ntargs, Bool -> Bool
not ([BareType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [BareType]
eargs)
      = Doc -> Maybe Error
err (Doc -> Maybe Error) -> Doc -> Maybe Error
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
PJ.hsep [Doc
"Expects", Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint Vertex
nαs, Doc
"type arguments before expression arguments"]
      | Bool
otherwise
      = Maybe Error
forall a. Maybe a
Nothing

isRExprArg :: RType c tv r -> Bool
isRExprArg :: RType c tv r -> Bool
isRExprArg (RExprArg Located Expr
_) = Bool
True 
isRExprArg RType c tv r
_            = Bool
False 

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



--------------------------------------------------------------------------------
-- | exprArg converts a tyVar to an exprVar because parser cannot tell
--   this function allows us to treating (parsed) "types" as "value"
--   arguments, e.g. type Matrix a Row Col = List (List a Row) Col
--   Note that during parsing, we don't necessarily know whether a
--   string is a type or a value expression. E.g. in tests/pos/T1189.hs,
--   the string `Prop (Ev (plus n n))` where `Prop` is the alias:
--     {-@ type Prop E = {v:_ | prop v = E} @-}
--   the parser will chomp in `Ev (plus n n)` as a `BareType` and so
--   `exprArg` converts that `BareType` into an `Expr`.
--------------------------------------------------------------------------------
exprArg :: F.SourcePos -> String -> BareType -> Expr
exprArg :: SourcePos -> String -> BareType -> Expr
exprArg SourcePos
l String
msg = String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
F.notracepp (String
"exprArg: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg) (Expr -> Expr) -> (BareType -> Expr) -> BareType -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> Expr
go 
  where 
    go :: BareType -> Expr
    go :: BareType -> Expr
go (RExprArg Located Expr
e)     = Located Expr -> Expr
forall a. Located a -> a
val Located Expr
e
    go (RVar BTyVar
x RReft
_)       = Symbol -> Expr
EVar (BTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol BTyVar
x)
    go (RApp BTyCon
x [] [] RReft
_) = Symbol -> Expr
EVar (BTyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol BTyCon
x)
    go (RApp BTyCon
f [BareType]
ts [] RReft
_) = LocSymbol -> [Expr] -> Expr
F.mkEApp (Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Symbol -> Symbol) -> LocSymbol -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BTyCon -> LocSymbol
btc_tc BTyCon
f) (BareType -> Expr
go (BareType -> Expr) -> [BareType] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
ts)
    go (RAppTy BareType
t1 BareType
t2 RReft
_) = Expr -> Expr -> Expr
F.EApp (BareType -> Expr
go BareType
t1) (BareType -> Expr
go BareType
t2)
    go BareType
z                = Maybe SrcSpan -> String -> Expr
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
sp (String -> Expr) -> String -> Expr
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> String
forall r. PrintfType r => String -> r
Printf.printf String
"Unexpected expression parameter: %s in %s" (BareType -> String
forall a. Show a => a -> String
show BareType
z) String
msg
    sp :: Maybe SrcSpan
sp                  = SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l)


----------------------------------------------------------------------------------------
-- | @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 -> LocBareType -> LocSpecType
cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV Var
x LocBareType
bt
         = (UserError -> LocSpecType)
-> (LocSpecType -> LocSpecType)
-> Either UserError LocSpecType
-> LocSpecType
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either UserError -> LocSpecType
forall a e. Exception e => e -> a
Ex.throw LocSpecType -> LocSpecType
forall a. a -> a
id (Env
-> SigEnv
-> ModName
-> PlugTV Var
-> LocBareType
-> Either UserError LocSpecType
cookSpecTypeE Env
env SigEnv
sigEnv ModName
name PlugTV Var
x LocBareType
bt)
  where 
    _msg :: String
_msg = String
"cookSpecType: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe Var, Maybe Kind) -> String
forall a. Outputable a => a -> String
GM.showPpr (Maybe Var
z, Var -> Kind
Ghc.varType (Var -> Kind) -> Maybe Var -> Maybe Kind
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 
              -> Either UserError LocSpecType 
-----------------------------------------------------------------------------------------
cookSpecTypeE :: Env
-> SigEnv
-> ModName
-> PlugTV Var
-> LocBareType
-> Either UserError LocSpecType
cookSpecTypeE Env
env SigEnv
sigEnv ModName
name PlugTV Var
x LocBareType
bt
  = Either UserError LocSpecType -> Either UserError LocSpecType
forall a. a -> a
id 
  (Either UserError LocSpecType -> Either UserError LocSpecType)
-> (LocBareType -> Either UserError LocSpecType)
-> LocBareType
-> Either UserError LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSpecType -> LocSpecType)
-> Either UserError LocSpecType -> Either UserError LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType
plugHoles SigEnv
sigEnv ModName
name PlugTV Var
x)
  (Either UserError LocSpecType -> Either UserError LocSpecType)
-> (LocBareType -> Either UserError LocSpecType)
-> LocBareType
-> Either UserError LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSpecType -> LocSpecType)
-> Either UserError LocSpecType -> Either UserError LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SpecType -> SpecType) -> LocSpecType -> LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TCEmb TyCon -> TyConMap -> SpecType -> SpecType
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> TyConMap -> RRType r -> RRType r
addTyConInfo   TCEmb TyCon
embs TyConMap
tyi))
  (Either UserError LocSpecType -> Either UserError LocSpecType)
-> (LocBareType -> Either UserError LocSpecType)
-> LocBareType
-> Either UserError LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSpecType -> LocSpecType)
-> Either UserError LocSpecType -> Either UserError LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
Bare.txRefSort TyConMap
tyi TCEmb TyCon
embs)     
  (Either UserError LocSpecType -> Either UserError LocSpecType)
-> (LocBareType -> Either UserError LocSpecType)
-> LocBareType
-> Either UserError LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSpecType -> LocSpecType)
-> Either UserError LocSpecType -> Either UserError LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SpecType -> SpecType) -> LocSpecType -> LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> SpecType
txExpToBind)      -- What does this function DO
  (Either UserError LocSpecType -> Either UserError LocSpecType)
-> (LocBareType -> Either UserError LocSpecType)
-> LocBareType
-> Either UserError LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSpecType -> LocSpecType)
-> Either UserError LocSpecType -> Either UserError LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BareRTEnv -> LocSpecType -> LocSpecType
specExpandType BareRTEnv
rtEnv)                        
  (Either UserError LocSpecType -> Either UserError LocSpecType)
-> (LocBareType -> Either UserError LocSpecType)
-> LocBareType
-> Either UserError LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSpecType -> LocSpecType)
-> Either UserError LocSpecType -> Either UserError LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SpecType -> SpecType) -> LocSpecType -> LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PlugTV Var -> SpecType -> SpecType
generalizeWith PlugTV Var
x))
  (Either UserError LocSpecType -> Either UserError LocSpecType)
-> (LocBareType -> Either UserError LocSpecType)
-> LocBareType
-> Either UserError LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSpecType -> LocSpecType)
-> Either UserError LocSpecType -> Either UserError LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType
maybePlug       SigEnv
sigEnv ModName
name PlugTV Var
x)
  (Either UserError LocSpecType -> Either UserError LocSpecType)
-> (LocBareType -> Either UserError LocSpecType)
-> LocBareType
-> Either UserError LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSpecType -> LocSpecType)
-> Either UserError LocSpecType -> Either UserError LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> ModName -> SourcePos -> LocSpecType -> LocSpecType
forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
Bare.qualifyTop    Env
env ModName
name SourcePos
l) 
  (Either UserError LocSpecType -> Either UserError LocSpecType)
-> (LocBareType -> Either UserError LocSpecType)
-> LocBareType
-> Either UserError LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> LocBareType -> Either UserError LocSpecType
bareSpecType       Env
env ModName
name 
  (LocBareType -> Either UserError LocSpecType)
-> (LocBareType -> LocBareType)
-> LocBareType
-> Either UserError LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareRTEnv -> LocBareType -> LocBareType
bareExpandType     BareRTEnv
rtEnv
  (LocBareType -> Either UserError LocSpecType)
-> LocBareType -> Either UserError LocSpecType
forall a b. (a -> b) -> a -> b
$ LocBareType
bt 
  where 
    _msg :: a -> String
_msg a
i = String
"cook-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PlugTV Var -> String
forall a. PPrint a => a -> String
F.showpp PlugTV Var
x
    rtEnv :: BareRTEnv
rtEnv  = SigEnv -> BareRTEnv
Bare.sigRTEnv    SigEnv
sigEnv
    embs :: TCEmb TyCon
embs   = SigEnv -> TCEmb TyCon
Bare.sigEmbs     SigEnv
sigEnv 
    tyi :: TyConMap
tyi    = SigEnv -> TyConMap
Bare.sigTyRTyMap SigEnv
sigEnv
    l :: SourcePos
l      = LocBareType -> SourcePos
forall a. Located a -> SourcePos
F.loc LocBareType
bt

-- | 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 

generalizeVar :: Ghc.Var -> SpecType -> SpecType 
generalizeVar :: Var -> SpecType -> SpecType
generalizeVar Var
v SpecType
t = [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [PVar (RType RTyCon RTyVar ())] -> SpecType -> SpecType
forall (t :: * -> *) (t1 :: * -> *) tv c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RType c tv ()), r)
-> t1 (PVar (RType c tv ())) -> RType c tv r -> RType c tv r
mkUnivs ([RTVar RTyVar (RType RTyCon RTyVar ())]
-> [RReft] -> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RTVar RTyVar (RType RTyCon RTyVar ())]
as (RReft -> [RReft]
forall a. a -> [a]
repeat RReft
forall a. Monoid a => a
mempty)) [] SpecType
t 
  where 
    as :: [RTVar RTyVar (RType RTyCon RTyVar ())]
as            = (RTVar RTyVar (RType RTyCon RTyVar ()) -> Bool)
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
forall a. (a -> Bool) -> [a] -> [a]
filter RTVar RTyVar (RType RTyCon RTyVar ()) -> Bool
forall s. RTVar RTyVar s -> Bool
isGen (SpecType -> [RTVar RTyVar (RType RTyCon RTyVar ())]
forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars SpecType
t)
    ([Var]
vas,Kind
_)       = Kind -> ([Var], Kind)
Ghc.splitForAllTys (Var -> Kind
GM.expandVarType Var
v) 
    isGen :: RTVar RTyVar s -> Bool
isGen (RTVar (RTV Var
a) RTVInfo s
_) = Var
a Var -> [Var] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
vas 

-- splitForAllTys :: 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 :: BareRTEnv -> LocBareType -> LocBareType
bareExpandType = BareRTEnv -> LocBareType -> LocBareType
forall a. Expand a => BareRTEnv -> Located a -> Located a
expandLoc 

specExpandType :: BareRTEnv -> LocSpecType -> LocSpecType
specExpandType :: BareRTEnv -> LocSpecType -> LocSpecType
specExpandType = BareRTEnv -> LocSpecType -> LocSpecType
forall a. Expand a => BareRTEnv -> Located a -> Located a
expandLoc 

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

maybePlug :: Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType 
maybePlug :: SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType
maybePlug 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 -> LocSpecType -> LocSpecType
forall a. a -> a
id  
                             Just Var
_  -> SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType
plugHoles SigEnv
sigEnv ModName
name PlugTV Var
kx 

plugHoles :: Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocSpecType -> LocSpecType 
plugHoles :: SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType
plugHoles SigEnv
sigEnv ModName
name = ModName
-> TCEmb TyCon
-> TyConMap
-> HashSet StableName
-> PlugTV Var
-> LocSpecType
-> LocSpecType
Bare.makePluggedSig 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 :: BareRTEnv -> SourcePos -> Expr -> Expr
expandExpr BareRTEnv
rtEnv SourcePos
l      = Expr -> Expr
go
  where
    go :: Expr -> Expr
go e :: Expr
e@(EApp Expr
_ Expr
_)     = BareRTEnv -> SourcePos -> (Expr, [Expr]) -> Expr
expandEApp BareRTEnv
rtEnv SourcePos
l (Expr -> (Expr, [Expr])
F.splitEApp Expr
e)
    go (EVar Symbol
x)         = BareRTEnv -> SourcePos -> Symbol -> Expr
expandSym  BareRTEnv
rtEnv SourcePos
l Symbol
x
    go (ENeg Expr
e)         = Expr -> Expr
ENeg       (Expr -> Expr
go Expr
e)
    go (ECst Expr
e Sort
s)       = Expr -> Sort -> Expr
ECst       (Expr -> Expr
go Expr
e) Sort
s 
    go (PAnd [Expr]
ps)        = [Expr] -> Expr
PAnd       (Expr -> Expr
go (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
ps)
    go (POr [Expr]
ps)         = [Expr] -> Expr
POr        (Expr -> Expr
go (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
ps)
    go (PNot Expr
p)         = Expr -> Expr
PNot       (Expr -> Expr
go Expr
p)
    go (PAll [(Symbol, Sort)]
xs Expr
p)      = [(Symbol, Sort)] -> Expr -> Expr
PAll [(Symbol, Sort)]
xs    (Expr -> Expr
go Expr
p)
    go (PExist [(Symbol, Sort)]
xs Expr
p)    = [(Symbol, Sort)] -> Expr -> Expr
PExist [(Symbol, Sort)]
xs  (Expr -> Expr
go Expr
p)
    go (ELam (Symbol, Sort)
xt Expr
e)      = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol, Sort)
xt    (Expr -> Expr
go Expr
e)
    go (ECoerc Sort
a Sort
t Expr
e)   = Sort -> Sort -> Expr -> Expr
ECoerc Sort
a Sort
t (Expr -> Expr
go Expr
e)
    go (ETApp Expr
e Sort
s)      = Expr -> Sort -> Expr
ETApp      (Expr -> Expr
go Expr
e) Sort
s 
    go (ETAbs Expr
e Symbol
s)      = Expr -> Symbol -> Expr
ETAbs      (Expr -> Expr
go Expr
e) Symbol
s 
    go (EBin Bop
op Expr
e1 Expr
e2)  = Bop -> Expr -> Expr -> Expr
EBin Bop
op    (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PImp    Expr
e1 Expr
e2)  = Expr -> Expr -> Expr
PImp       (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PIff    Expr
e1 Expr
e2)  = Expr -> Expr -> Expr
PIff       (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PAtom Brel
b Expr
e1 Expr
e2)  = Brel -> Expr -> Expr -> Expr
PAtom Brel
b    (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (EIte  Expr
p Expr
e1 Expr
e2)  = Expr -> Expr -> Expr -> Expr
EIte (Expr -> Expr
go Expr
p)(Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PGrad KVar
k Subst
su GradInfo
i Expr
e) = KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
su GradInfo
i (Expr -> Expr
go Expr
e)
    go e :: Expr
e@(PKVar KVar
_ Subst
_)    = Expr
e
    go e :: Expr
e@(ESym SymConst
_)       = Expr
e
    go e :: Expr
e@(ECon Constant
_)       = Expr
e

expandSym :: BareRTEnv -> F.SourcePos -> F.Symbol -> Expr
expandSym :: BareRTEnv -> SourcePos -> Symbol -> Expr
expandSym BareRTEnv
rtEnv SourcePos
l Symbol
s' = BareRTEnv -> SourcePos -> (Expr, [Expr]) -> Expr
expandEApp BareRTEnv
rtEnv SourcePos
l (Symbol -> Expr
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 :: BareRTEnv -> SourcePos -> (Expr, [Expr]) -> Expr
expandEApp BareRTEnv
rtEnv SourcePos
l (EVar Symbol
f, [Expr]
es) = case Maybe (Located (RTAlias Symbol Expr))
mBody of
    Just Located (RTAlias Symbol Expr)
re -> SourcePos -> Located (RTAlias Symbol Expr) -> [Expr] -> Expr
forall ty.
Subable ty =>
SourcePos -> Located (RTAlias Symbol ty) -> [Expr] -> ty
expandApp SourcePos
l   Located (RTAlias Symbol Expr)
re       [Expr]
es' 
    Maybe (Located (RTAlias Symbol Expr))
Nothing -> Expr -> [Expr] -> Expr
F.eApps       (Symbol -> Expr
EVar Symbol
f) [Expr]
es' 
  where
    eAs :: HashMap Symbol (Located (RTAlias Symbol Expr))
eAs     = BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol Expr))
forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases BareRTEnv
rtEnv
    mBody :: Maybe (Located (RTAlias Symbol Expr))
mBody   = [Maybe (Located (RTAlias Symbol Expr))]
-> Maybe (Located (RTAlias Symbol Expr))
forall a. [Maybe a] -> Maybe a
Misc.firstMaybes [Symbol
-> HashMap Symbol (Located (RTAlias Symbol Expr))
-> Maybe (Located (RTAlias Symbol Expr))
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
f HashMap Symbol (Located (RTAlias Symbol Expr))
eAs, Symbol
-> HashMap Symbol (Located (RTAlias Symbol Expr))
-> Maybe (Located (RTAlias Symbol Expr))
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (Symbol -> Symbol
GM.dropModuleUnique Symbol
f) HashMap Symbol (Located (RTAlias Symbol Expr))
eAs]
    es' :: [Expr]
es'     = BareRTEnv -> SourcePos -> Expr -> Expr
expandExpr BareRTEnv
rtEnv SourcePos
l (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es
    _f0 :: Symbol
_f0     = Symbol -> Symbol
GM.dropModuleNamesAndUnique Symbol
f

expandEApp BareRTEnv
_ SourcePos
_ (Expr
f, [Expr]
es) = Expr -> [Expr] -> Expr
F.eApps Expr
f [Expr]
es

--------------------------------------------------------------------------------
-- | Expand Alias Application --------------------------------------------------
--------------------------------------------------------------------------------
expandApp :: F.Subable ty => F.SourcePos -> Located (RTAlias F.Symbol ty) -> [Expr] -> ty
expandApp :: SourcePos -> Located (RTAlias Symbol ty) -> [Expr] -> ty
expandApp SourcePos
l Located (RTAlias Symbol ty)
lre [Expr]
es
  | Just Subst
su <- Maybe Subst
args = Subst -> ty -> ty
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (RTAlias Symbol ty -> ty
forall x a. RTAlias x a -> a
rtBody RTAlias Symbol ty
re)
  | Bool
otherwise       = UserError -> ty
forall a e. Exception e => e -> a
Ex.throw UserError
err
  where
    re :: RTAlias Symbol ty
re              = Located (RTAlias Symbol ty) -> RTAlias Symbol ty
forall a. Located a -> a
F.val Located (RTAlias Symbol ty)
lre
    args :: Maybe Subst
args            = [(Symbol, Expr)] -> Subst
F.mkSubst ([(Symbol, Expr)] -> Subst)
-> Maybe [(Symbol, Expr)] -> Maybe Subst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol] -> [Expr] -> Maybe [(Symbol, Expr)]
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) [Expr]
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           = Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint           (RTAlias Symbol ty -> Symbol
forall x a. RTAlias x a -> Symbol
rtName RTAlias Symbol ty
re)
    sp' :: SrcSpan
sp'             = Located (RTAlias Symbol ty) -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located (RTAlias Symbol ty)
lre -- sourcePosSrcSpan (rtPos re)
    msg :: Doc
msg             =  Doc
"expects" Doc -> Doc -> Doc
PJ.<+> Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint ([Symbol] -> Vertex
forall (t :: * -> *) a. Foldable t => t a -> Vertex
length ([Symbol] -> Vertex) -> [Symbol] -> Vertex
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.<+> Vertex -> Doc
forall a. PPrint a => a -> Doc
pprint ([Expr] -> Vertex
forall (t :: * -> *) a. Foldable t => t a -> Vertex
length [Expr]
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) (Vertex
-> HashMap Symbol (RType RTyCon RTyVar (), Expr)
-> HashMap Symbol (PVar (RType RTyCon RTyVar ()))
-> ExSt
ExSt Vertex
0 HashMap Symbol (RType RTyCon RTyVar (), Expr)
forall k v. HashMap k v
M.empty HashMap Symbol (PVar (RType RTyCon RTyVar ()))
πs)
  where 
    πs :: HashMap Symbol (PVar (RType RTyCon RTyVar ()))
πs        = [(Symbol, PVar (RType RTyCon RTyVar ()))]
-> HashMap Symbol (PVar (RType RTyCon RTyVar ()))
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(PVar (RType RTyCon RTyVar ()) -> Symbol
forall t. PVar t -> Symbol
pname PVar (RType RTyCon RTyVar ())
p, PVar (RType RTyCon RTyVar ())
p) | PVar (RType RTyCon RTyVar ())
p <- RTypeRep RTyCon RTyVar RReft -> [PVar (RType RTyCon RTyVar ())]
forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds (RTypeRep RTyCon RTyVar RReft -> [PVar (RType RTyCon RTyVar ())])
-> RTypeRep RTyCon RTyVar RReft -> [PVar (RType RTyCon RTyVar ())]
forall a b. (a -> b) -> a -> b
$ SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t ]

data ExSt = ExSt { ExSt -> Vertex
fresh :: Int
                 , ExSt -> HashMap Symbol (RType RTyCon RTyVar (), Expr)
emap  :: M.HashMap F.Symbol (RSort, F.Expr)
                 , ExSt -> HashMap Symbol (PVar (RType 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 RReft
r)
  = RReft -> State ExSt RReft
forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r State ExSt RReft
-> (RReft -> State ExSt SpecType) -> State ExSt SpecType
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists (SpecType -> State ExSt SpecType)
-> (RReft -> SpecType) -> RReft -> State ExSt SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTyVar -> RReft -> SpecType
forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
v
expToBindT (RFun Symbol
x SpecType
t1 SpecType
t2 RReft
r)
  = do SpecType
t1' <- SpecType -> State ExSt SpecType
expToBindT SpecType
t1
       SpecType
t2' <- SpecType -> State ExSt SpecType
expToBindT SpecType
t2
       RReft -> State ExSt RReft
forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r State ExSt RReft
-> (RReft -> State ExSt SpecType) -> State ExSt SpecType
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists (SpecType -> State ExSt SpecType)
-> (RReft -> SpecType) -> RReft -> State ExSt SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x SpecType
t1' SpecType
t2'
expToBindT (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
a SpecType
t RReft
r)
  = do SpecType
t' <- SpecType -> State ExSt SpecType
expToBindT SpecType
t 
       RReft -> State ExSt RReft
forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r State ExSt RReft
-> (RReft -> State ExSt SpecType) -> State ExSt SpecType
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists (SpecType -> State ExSt SpecType)
-> (RReft -> SpecType) -> RReft -> State ExSt SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTVar RTyVar (RType RTyCon RTyVar ())
-> SpecType -> RReft -> SpecType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
a SpecType
t' 
expToBindT (RAllP PVar (RType RTyCon RTyVar ())
p SpecType
t)
  = (SpecType -> SpecType)
-> State ExSt SpecType -> State ExSt SpecType
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (PVar (RType RTyCon RTyVar ()) -> SpecType -> SpecType
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVar (RType RTyCon RTyVar ())
p) (SpecType -> State ExSt SpecType
expToBindT SpecType
t)
expToBindT (RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs RReft
r)
  = do [SpecType]
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)
mapM SpecType -> State ExSt SpecType
expToBindT [SpecType]
ts
       [RTProp RTyCon RTyVar RReft]
rs' <- (RTProp RTyCon RTyVar RReft
 -> StateT ExSt Identity (RTProp RTyCon RTyVar RReft))
-> [RTProp RTyCon RTyVar RReft]
-> StateT ExSt Identity [RTProp RTyCon RTyVar RReft]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM RTProp RTyCon RTyVar RReft
-> StateT ExSt Identity (RTProp RTyCon RTyVar RReft)
expToBindReft [RTProp RTyCon RTyVar RReft]
rs
       RReft -> State ExSt RReft
forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r State ExSt RReft
-> (RReft -> State ExSt SpecType) -> State ExSt SpecType
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists (SpecType -> State ExSt SpecType)
-> (RReft -> SpecType) -> RReft -> State ExSt SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [SpecType]
ts' [RTProp RTyCon RTyVar RReft]
rs'
expToBindT (RAppTy SpecType
t1 SpecType
t2 RReft
r)
  = do SpecType
t1' <- SpecType -> State ExSt SpecType
expToBindT SpecType
t1
       SpecType
t2' <- SpecType -> State ExSt SpecType
expToBindT SpecType
t2
       RReft -> State ExSt RReft
forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r State ExSt RReft
-> (RReft -> State ExSt SpecType) -> State ExSt SpecType
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists (SpecType -> State ExSt SpecType)
-> (RReft -> SpecType) -> RReft -> State ExSt SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType -> RReft -> SpecType
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy SpecType
t1' SpecType
t2'
expToBindT (RRTy [(Symbol, SpecType)]
xts RReft
r Oblig
o SpecType
t)
  = do [(Symbol, SpecType)]
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)
mapM SpecType -> State ExSt SpecType
expToBindT [SpecType]
ts
       RReft
r'   <- RReft -> State ExSt RReft
forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r
       SpecType
t'   <- SpecType -> State ExSt SpecType
expToBindT SpecType
t
       SpecType -> State ExSt SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecType -> State ExSt SpecType)
-> SpecType -> State ExSt SpecType
forall a b. (a -> b) -> a -> b
$ [(Symbol, SpecType)] -> RReft -> Oblig -> SpecType -> SpecType
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, SpecType)]
xts' RReft
r' Oblig
o SpecType
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 (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

expToBindReft              :: SpecProp -> State ExSt SpecProp
expToBindReft :: RTProp RTyCon RTyVar RReft
-> StateT ExSt Identity (RTProp RTyCon RTyVar RReft)
expToBindReft (RProp [(Symbol, RType RTyCon RTyVar ())]
s (RHole RReft
r)) = [(Symbol, RType RTyCon RTyVar ())]
-> RReft -> RTProp RTyCon RTyVar RReft
forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [(Symbol, RType RTyCon RTyVar ())]
s (RReft -> RTProp RTyCon RTyVar RReft)
-> State ExSt RReft
-> StateT ExSt Identity (RTProp RTyCon RTyVar RReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RReft -> State ExSt RReft
forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r
expToBindReft (RProp [(Symbol, RType RTyCon RTyVar ())]
s SpecType
t)  = [(Symbol, RType RTyCon RTyVar ())]
-> SpecType -> RTProp RTyCon RTyVar RReft
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
s  (SpecType -> RTProp RTyCon RTyVar RReft)
-> State ExSt SpecType
-> StateT ExSt Identity (RTProp RTyCon RTyVar RReft)
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 (RType RTyCon RTyVar (), Expr))
getBinds
  = do HashMap Symbol (RType RTyCon RTyVar (), Expr)
bds <- ExSt -> HashMap Symbol (RType RTyCon RTyVar (), Expr)
emap (ExSt -> HashMap Symbol (RType RTyCon RTyVar (), Expr))
-> StateT ExSt Identity ExSt
-> State ExSt (HashMap Symbol (RType RTyCon RTyVar (), Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ExSt Identity ExSt
forall s (m :: * -> *). MonadState s m => m s
get
       (ExSt -> ExSt) -> StateT ExSt Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ExSt -> ExSt) -> StateT ExSt Identity ())
-> (ExSt -> ExSt) -> StateT ExSt Identity ()
forall a b. (a -> b) -> a -> b
$ \ExSt
st -> ExSt
st{emap :: HashMap Symbol (RType RTyCon RTyVar (), Expr)
emap = HashMap Symbol (RType RTyCon RTyVar (), Expr)
forall k v. HashMap k v
M.empty}
       HashMap Symbol (RType RTyCon RTyVar (), Expr)
-> State ExSt (HashMap Symbol (RType RTyCon RTyVar (), Expr))
forall (m :: * -> *) a. Monad m => a -> m a
return HashMap Symbol (RType RTyCon RTyVar (), Expr)
bds

addExists :: SpecType -> State ExSt SpecType
addExists :: SpecType -> State ExSt SpecType
addExists SpecType
t = (HashMap Symbol (RType RTyCon RTyVar (), Expr) -> SpecType)
-> State ExSt (HashMap Symbol (RType RTyCon RTyVar (), Expr))
-> State ExSt SpecType
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((SpecType -> Symbol -> (RType RTyCon RTyVar (), Expr) -> SpecType)
-> SpecType
-> HashMap Symbol (RType RTyCon RTyVar (), Expr)
-> SpecType
forall a k v. (a -> k -> v -> a) -> a -> HashMap k v -> a
M.foldlWithKey' SpecType -> Symbol -> (RType RTyCon RTyVar (), Expr) -> SpecType
addExist SpecType
t) State ExSt (HashMap Symbol (RType RTyCon RTyVar (), Expr))
getBinds

addExist :: SpecType -> F.Symbol -> (RSort, F.Expr) -> SpecType
addExist :: SpecType -> Symbol -> (RType RTyCon RTyVar (), Expr) -> SpecType
addExist SpecType
t Symbol
x (RType RTyCon RTyVar ()
tx, Expr
e) = Symbol -> SpecType -> SpecType -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
x SpecType
t' SpecType
t
  where 
    t' :: SpecType
t'               = (RType RTyCon RTyVar () -> SpecType
forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType RTyCon RTyVar ()
tx) SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` Reft -> RReft
forall r. r -> UReft r
uTop Reft
r
    r :: Reft
r                = Expr -> Reft
forall a. Expression a => a -> Reft
F.exprReft Expr
e

expToBindRef :: UReft r -> State ExSt (UReft r)
expToBindRef :: UReft r -> State ExSt (UReft r)
expToBindRef (MkUReft r
r (Pr [UsedPVar]
p))
  = (UsedPVar -> StateT ExSt Identity UsedPVar)
-> [UsedPVar] -> StateT ExSt Identity [UsedPVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM UsedPVar -> StateT ExSt Identity UsedPVar
expToBind [UsedPVar]
p StateT ExSt Identity [UsedPVar]
-> ([UsedPVar] -> State ExSt (UReft r)) -> State ExSt (UReft r)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UReft r -> State ExSt (UReft r)
forall (m :: * -> *) a. Monad m => a -> m a
return (UReft r -> State ExSt (UReft r))
-> ([UsedPVar] -> UReft r) -> [UsedPVar] -> State ExSt (UReft r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (r -> Predicate -> UReft r
forall r. r -> Predicate -> UReft r
MkUReft r
r) (Predicate -> UReft r)
-> ([UsedPVar] -> Predicate) -> [UsedPVar] -> UReft r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UsedPVar] -> Predicate
Pr

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

expToBindParg :: (((), F.Symbol, F.Expr), RSort) -> State ExSt ((), F.Symbol, F.Expr)
expToBindParg :: (((), Symbol, Expr), RType RTyCon RTyVar ())
-> StateT ExSt Identity ((), Symbol, Expr)
expToBindParg ((()
t, Symbol
s, Expr
e), RType RTyCon RTyVar ()
s') = (Expr -> ((), Symbol, Expr))
-> StateT ExSt Identity Expr
-> StateT ExSt Identity ((), Symbol, Expr)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((,,) ()
t Symbol
s) (Expr -> RType RTyCon RTyVar () -> StateT ExSt Identity Expr
expToBindExpr Expr
e RType RTyCon RTyVar ()
s')

expToBindExpr :: F.Expr ->  RSort -> State ExSt F.Expr
expToBindExpr :: Expr -> RType RTyCon RTyVar () -> StateT ExSt Identity Expr
expToBindExpr e :: Expr
e@(EVar Symbol
s) RType RTyCon RTyVar ()
_ 
  | 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
  = Expr -> StateT ExSt Identity Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
expToBindExpr Expr
e RType RTyCon RTyVar ()
t
  = do Symbol
s <- State ExSt Symbol
freshSymbol
       (ExSt -> ExSt) -> StateT ExSt Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ExSt -> ExSt) -> StateT ExSt Identity ())
-> (ExSt -> ExSt) -> StateT ExSt Identity ()
forall a b. (a -> b) -> a -> b
$ \ExSt
st -> ExSt
st{emap :: HashMap Symbol (RType RTyCon RTyVar (), Expr)
emap = Symbol
-> (RType RTyCon RTyVar (), Expr)
-> HashMap Symbol (RType RTyCon RTyVar (), Expr)
-> HashMap Symbol (RType RTyCon RTyVar (), Expr)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
s (RType RTyCon RTyVar ()
t, Expr
e) (ExSt -> HashMap Symbol (RType RTyCon RTyVar (), Expr)
emap ExSt
st)}
       Expr -> StateT ExSt Identity Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT ExSt Identity Expr)
-> Expr -> StateT ExSt Identity Expr
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
EVar Symbol
s

freshSymbol :: State ExSt F.Symbol
freshSymbol :: State ExSt Symbol
freshSymbol
  = do Vertex
n <- ExSt -> Vertex
fresh (ExSt -> Vertex)
-> StateT ExSt Identity ExSt -> StateT ExSt Identity Vertex
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ExSt Identity ExSt
forall s (m :: * -> *). MonadState s m => m s
get
       (ExSt -> ExSt) -> StateT ExSt Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ExSt -> ExSt) -> StateT ExSt Identity ())
-> (ExSt -> ExSt) -> StateT ExSt Identity ()
forall a b. (a -> b) -> a -> b
$ \ExSt
s -> ExSt
s {fresh :: Vertex
fresh = Vertex
nVertex -> Vertex -> Vertex
forall a. Num a => a -> a -> a
+Vertex
1}
       Symbol -> State ExSt Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol -> State ExSt Symbol) -> Symbol -> State ExSt Symbol
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ String
"ex#" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Vertex -> String
forall a. Show a => a -> String
show Vertex
n