-- | 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 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
import           Control.Monad.State
import           Data.Functor ((<&>))
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 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
modName BareSpec
mySpec ModSpecs
iSpecs LogicMap
lmap
          = BareRTEnv -> BareRTEnv
renameRTArgs forall a b. (a -> b) -> a -> b
$ [Located (RTAlias Symbol BareType)] -> BareRTEnv -> BareRTEnv
makeRTAliases [Located (RTAlias Symbol BareType)]
tAs 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 <- 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 <- forall ty bndr. Spec ty bndr -> [Located (RTAlias Symbol Expr)]
Ms.ealiases BareSpec
s ]
         forall a. [a] -> [a] -> [a]
++ if Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig Env
env) then []
                                              -- lmap expansion happens during elaboration
                                              -- this clearly breaks things if a signature
                                              -- contains lmap functions but never gets
                                              -- elaborated
              else [ Env
-> ModName
-> Located (RTAlias Symbol Expr)
-> Located (RTAlias Symbol Expr)
specREAlias Env
env ModName
modName Located (RTAlias Symbol Expr)
e | (Symbol
_, LMap
xl) <- 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
modName, BareSpec
mySpec) forall a. a -> [a] -> [a]
: 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
  { typeAliases :: HashMap Symbol (Located (RTAlias Symbol BareType))
typeAliases = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RTAlias Symbol BareType -> RTAlias Symbol BareType
renameTys forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTAlias Symbol BareType -> RTAlias Symbol BareType
renameVV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. (PPrint a, Subable a) => RTAlias x a -> RTAlias x a
renameRTVArgs)) (forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases BareRTEnv
rte)
  , exprAliases :: HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap                         forall a x. (PPrint a, Subable a) => RTAlias x a -> RTAlias x a
renameRTVArgs) (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 = forall t x thing.
PPrint t =>
(AliasTable x t -> t -> [Symbol])
-> (thing -> Located (RTAlias x t) -> thing)
-> thing
-> [Located (RTAlias x t)]
-> thing
graphExpand forall a. HashMap Symbol a -> Expr -> [Symbol]
buildExprEdges BareRTEnv -> Located (RTAlias Symbol Expr) -> BareRTEnv
f forall a. Monoid a => a
mempty
  where
    f :: BareRTEnv -> Located (RTAlias Symbol Expr) -> BareRTEnv
f BareRTEnv
rtEnv Located (RTAlias Symbol Expr)
xt = forall x t. RTEnv x t -> Located (RTAlias Symbol Expr) -> RTEnv x t
setREAlias BareRTEnv
rtEnv (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
sbts (forall x a. RTAlias x a -> a
rtBody RTAlias Symbol BareType
rt) (forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [Symbol]
ys) }
  where
    xs :: [Symbol]
xs    = forall x a. RTAlias x a -> [x]
rtTArgs RTAlias Symbol BareType
rt
    ys :: [Symbol]
ys    = (Symbol -> Symbol -> Symbol
`F.suffixSymbol` forall x a. RTAlias x a -> Symbol
rtName RTAlias Symbol BareType
rt) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs
    sbts :: BareType -> [(Symbol, Symbol)] -> BareType
sbts  = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 = forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
RT.shiftVV (forall x a. RTAlias x a -> a
rtBody RTAlias Symbol BareType
rt) (Maybe Integer -> Symbol
F.vv (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 :: forall a x. (PPrint a, Subable a) => RTAlias x a -> RTAlias x a
renameRTVArgs RTAlias x a
rt = RTAlias x a
rt { rtVArgs :: [Symbol]
rtVArgs = [Symbol]
newArgs
                      , rtBody :: a
rtBody  = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
msg forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
F.subst Subst
su (forall x a. RTAlias x a -> a
rtBody RTAlias x a
rt)
                      }
  where
    msg :: [Char]
msg          = [Char]
"renameRTVArgs: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp Subst
su
    su :: Subst
su           = [(Symbol, Expr)] -> Subst
F.mkSubst (forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
oldArgs (forall a. Symbolic a => a -> Expr
F.eVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
newArgs))
    newArgs :: [Symbol]
newArgs      = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a}. Show a => Symbol -> a -> Symbol
rtArg (forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias x a
rt) [(Int
0::Int)..]
    oldArgs :: [Symbol]
oldArgs      = 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 (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 = forall t x thing.
PPrint t =>
(AliasTable x t -> t -> [Symbol])
-> (thing -> Located (RTAlias x t) -> thing)
-> thing
-> [Located (RTAlias x t)]
-> thing
graphExpand 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         = forall x t. RTEnv x t -> Located (RTAlias x t) -> RTEnv x t
setRTAlias BareRTEnv
rtEnv (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 = forall l b. Loc l => l -> b -> Located b
F.atLoc Located (RTAlias Symbol Expr)
la forall a b. (a -> b) -> a -> b
$ RTAlias Symbol Expr
a { rtBody :: Expr
rtBody = forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
Bare.qualify Env
env ModName
m (forall a. Located a -> SourcePos
loc Located (RTAlias Symbol Expr)
la) (forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol Expr
a) (forall x a. RTAlias x a -> a
rtBody RTAlias Symbol Expr
a) }
  where
    a :: RTAlias Symbol Expr
a     = 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 :: forall t x thing.
PPrint t =>
(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
           = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' thing -> Located (RTAlias x t) -> thing
expBody thing
env (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  = forall x t. [Located (RTAlias x t)] -> AliasTable x t
buildAliasTable [Located (RTAlias x t)]
lxts
    graph :: Graph Symbol
graph  = 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' = 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 :: forall x t. 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 =  forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
n Located (RTAlias x t)
a (forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases RTEnv x t
env) }
  where
    n :: Symbol
n            = forall x a. RTAlias x a -> Symbol
rtName (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 :: forall x t. 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 = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
n Located (RTAlias Symbol Expr)
a (forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases RTEnv x t
env) }
  where
    n :: Symbol
n            = forall x a. RTAlias x a -> Symbol
rtName (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 :: forall x t. [Located (RTAlias x t)] -> AliasTable x t
buildAliasTable = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\Located (RTAlias x t)
rta -> (forall x a. RTAlias x a -> Symbol
rtName (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 :: forall x t. AliasTable x t -> Symbol -> Located (RTAlias x t)
fromAliasSymbol AliasTable x t
table Symbol
sym
  = forall a. a -> Maybe a -> a
fromMaybe forall {a}. a
err (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 = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing ([Char]
"fromAliasSymbol: Dangling alias symbol: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
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 :: forall t x.
PPrint t =>
(t -> [Symbol]) -> [Located (RTAlias x t)] -> Graph Symbol
buildAliasGraph t -> [Symbol]
buildEdges = forall a b. (a -> b) -> [a] -> [b]
map (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 :: forall t x.
PPrint t =>
(t -> [Symbol]) -> Located (RTAlias x t) -> Node Symbol
buildAliasNode t -> [Symbol]
f Located (RTAlias x t)
la = (forall x a. RTAlias x a -> Symbol
rtName RTAlias x t
a, forall x a. RTAlias x a -> Symbol
rtName RTAlias x t
a, t -> [Symbol]
f (forall x a. RTAlias x a -> a
rtBody RTAlias x t
a))
  where
    a :: RTAlias x t
a               = forall a. Located a -> a
val Located (RTAlias x t)
la

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

cycleAliasErr :: AliasTable x t -> [F.Symbol] -> Error
cycleAliasErr :: forall x t. AliasTable x t -> [Symbol] -> Error
cycleAliasErr AliasTable x t
_ []          = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"checkCyclicAliases: No type aliases in reported cycle"
cycleAliasErr AliasTable x t
t symList :: [Symbol]
symList@(Symbol
rta:[Symbol]
_) = ErrAliasCycle { pos :: SrcSpan
pos    = forall a b. (a, b) -> a
fst (Symbol -> (SrcSpan, Doc)
locate Symbol
rta)
                                                , acycle :: [(SrcSpan, Doc)]
acycle = forall a b. (a -> b) -> [a] -> [b]
map Symbol -> (SrcSpan, Doc)
locate [Symbol]
symList }
  where
    locate :: Symbol -> (SrcSpan, Doc)
locate Symbol
sym = ( forall a. Loc a => a -> SrcSpan
GM.fSrcSpan forall a b. (a -> b) -> a -> b
$ forall x t. AliasTable x t -> Symbol -> Located (RTAlias x t)
fromAliasSymbol AliasTable x t
t Symbol
sym
                 , forall a. PPrint a => a -> Doc
pprint Symbol
sym )


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

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

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

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

buildExprEdges :: M.HashMap F.Symbol a -> F.Expr -> [F.Symbol]
buildExprEdges :: forall a. HashMap Symbol a -> Expr -> [Symbol]
buildExprEdges HashMap Symbol a
table  = forall a. Ord a => [a] -> [a]
ordNub 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 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 forall a. [a] -> [a] -> [a]
++ Expr -> [Symbol]
go Expr
e2
    go (EIte Expr
_ Expr
e1 Expr
e2) = Expr -> [Symbol]
go Expr
e1 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)       = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Symbol]
go [Expr]
ps
    go (POr [Expr]
ps)        = 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 forall a. [a] -> [a] -> [a]
++ Expr -> [Symbol]
go Expr
q
    go (PIff Expr
p Expr
q)      = Expr -> [Symbol]
go Expr
p 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 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 | 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.
--
-- When expanding, it's important we pass around a 'BareRTEnv' where the type aliases have been qualified as well.
-- This is subtle, see for example T1761. In that test, we had a type alias \"OneTyAlias a = {v:a | oneFunPred v}\" where
-- \"oneFunPred\" was marked inline. However, inlining couldn't happen because the 'BareRTEnv' had an
-- entry for \"T1761.oneFunPred\", so the relevant expansion of \"oneFunPred\" couldn't happen. This was
-- because the type alias entry inside 'BareRTEnv' mentioned the tuple (\"OneTyAlias\", \"{v:a | oneFunPred v}\") but
-- the 'snd' element needed to be qualified as well, before trying to expand anything.
----------------------------------------------------------------------------------
qualifyExpand :: (PPrint a, Expand a, Bare.Qualify a)
              => Bare.Env -> ModName -> BareRTEnv -> F.SourcePos -> [F.Symbol] -> a -> a
----------------------------------------------------------------------------------
qualifyExpand :: forall a.
(PPrint a, Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [Symbol]
bs
  = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
qualifiedRTEnv SourcePos
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
Bare.qualify Env
env ModName
name SourcePos
l [Symbol]
bs
  where
    qualifiedRTEnv :: BareRTEnv
    qualifiedRTEnv :: BareRTEnv
qualifiedRTEnv = BareRTEnv
rtEnv { typeAliases :: HashMap Symbol (Located (RTAlias Symbol BareType))
typeAliases = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (forall a.
Qualify a =>
Env -> ModName -> SourcePos -> [Symbol] -> a -> a
Bare.qualify Env
env ModName
name SourcePos
l [Symbol]
bs) (forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases BareRTEnv
rtEnv) }

----------------------------------------------------------------------------------
expandLoc :: (Expand a) => BareRTEnv -> Located a -> Located a
expandLoc :: forall a. Expand a => BareRTEnv -> Located a -> Located a
expandLoc BareRTEnv
rtEnv Located a
lx = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv (forall a. Located a -> SourcePos
F.loc Located a
lx) 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, 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 :: forall r c tv.
Expand r =>
BareRTEnv -> SourcePos -> RType c tv r -> RType c tv r
expandReft BareRTEnv
rtEnv SourcePos
l = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 = 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
    = forall r c tv.
Expand r =>
BareRTEnv -> SourcePos -> RType c tv r -> RType c tv r
expandReft     BareRTEnv
rtEnv SourcePos
l -- apply expression aliases
    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 = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (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 = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (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   (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   (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 (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  = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (DataCtor -> [BareType]
dcTheta DataCtor
c)
    , dcFields :: [(Symbol, BareType)]
dcFields = [(Symbol
x, 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 = 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 :: Maybe [DataCtor]
tycDCons  = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (DataDecl -> Maybe [DataCtor]
tycDCons  DataDecl
d)
    , tycPropTy :: Maybe BareType
tycPropTy = 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
-> Measure LocBareType LocSymbol
-> Measure LocBareType LocSymbol
expand BareRTEnv
rtEnv SourcePos
l Measure LocBareType LocSymbol
m = Measure LocBareType LocSymbol
m
    { msSort :: LocBareType
msSort = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (forall ty ctor. Measure ty ctor -> ty
msSort Measure LocBareType LocSymbol
m)
    , msEqns :: [Def LocBareType LocSymbol]
msEqns = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (forall ty ctor. Measure ty ctor -> [Def ty ctor]
msEqns Measure LocBareType LocSymbol
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 = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (forall ty ctor. Def ty ctor -> Maybe ty
dsort Def LocBareType LocSymbol
d)
    , binds :: [(Symbol, Maybe LocBareType)]
binds = [ (Symbol
x, forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l Maybe LocBareType
t) | (Symbol
x, Maybe LocBareType
t) <- forall ty ctor. Def ty ctor -> [(Symbol, Maybe ty)]
binds Def LocBareType LocSymbol
d]
    , body :: Body
body  = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (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
_ = 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, 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l)

-- | Expands a 'BareSpec'.
expandBareSpec :: BareRTEnv -> F.SourcePos -> Ms.BareSpec -> Ms.BareSpec
expandBareSpec :: BareRTEnv -> SourcePos -> BareSpec -> BareSpec
expandBareSpec BareRTEnv
rtEnv SourcePos
l BareSpec
sp = BareSpec
sp
  { measures :: [Measure LocBareType LocSymbol]
measures   = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures   BareSpec
sp)
  , asmSigs :: [(LocSymbol, LocBareType)]
asmSigs    = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
asmSigs    BareSpec
sp)
  , sigs :: [(LocSymbol, LocBareType)]
sigs       = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
sigs       BareSpec
sp)
  , localSigs :: [(LocSymbol, LocBareType)]
localSigs  = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
localSigs  BareSpec
sp)
  , reflSigs :: [(LocSymbol, LocBareType)]
reflSigs   = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (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) <- forall ty bndr. Spec ty bndr -> [(ty, ty)]
ialiases BareSpec
sp ]
  , dataDecls :: [DataDecl]
dataDecls  = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls  BareSpec
sp)
  , newtyDecls :: [DataDecl]
newtyDecls = forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (forall ty bndr. Spec ty bndr -> [DataDecl]
newtyDecls BareSpec
sp)
  }
  where f :: LocBareType -> LocBareType
f      = 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 (forall a. Loc a => a -> SourcePos
GM.fSourcePos BTyCon
c) Located (RTAlias Symbol BareType)
rta (BareType -> BareType
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
ts) RReft
r
                             Maybe (Located (RTAlias Symbol BareType))
Nothing  -> forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp BTyCon
c (BareType -> BareType
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
ts) (RTProp BTyCon BTyVar RReft -> RTProp BTyCon BTyVar RReft
goRef 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)  = 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 (RFun  Symbol
x RFInfo
i BareType
t1 BareType
t2 RReft
r) = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun  Symbol
x RFInfo
i (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2) RReft
r
    go (RAllT RTVar BTyVar (RType BTyCon BTyVar ())
a BareType
t RReft
r)     = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar BTyVar (RType BTyCon BTyVar ())
a (BareType -> BareType
go BareType
t) RReft
r
    go (RAllP PVU BTyCon BTyVar
a BareType
t)       = 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)   = 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)     = 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)    = 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)   = 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 = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (forall a. Symbolic a => a -> Symbol
F.symbol BTyCon
c) (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     -> forall a e. Exception e => e -> a
Ex.throw Error
e
  Maybe Error
Nothing    -> forall a. Subable a => Subst -> a -> a
F.subst Subst
esu forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` RReft
r) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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.subsTyVarsMeet [(BTyVar, RType BTyCon BTyVar (), BareType)]
tsu forall a b. (a -> b) -> a -> b
$ forall x a. RTAlias x a -> a
rtBody RTAlias Symbol BareType
rta
  where
    tsu :: [(BTyVar, RType BTyCon BTyVar (), BareType)]
tsu       = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\BTyVar
α BareType
t -> (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 forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
εs) [Expr]
es
    es :: [Expr]
es        = SourcePos -> [Char] -> BareType -> Expr
exprArg SourcePos
l [Char]
msg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
es0
    ([BareType]
ts, [BareType]
es0) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
nαs [BareType]
args
    ([BTyVar]
αs, [Symbol]
εs)  = (Symbol -> BTyVar
BTV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall x a. RTAlias x a -> [x]
rtTArgs RTAlias Symbol BareType
rta, forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol BareType
rta)
    targs :: [BareType]
targs     = forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. RType c tv r -> Bool
isRExprArg) [BareType]
args
    eargs :: [BareType]
eargs     = forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. RType c tv r -> Bool
isRExprArg) [BareType]
args

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

isRExprArg :: RType c tv r -> Bool
isRExprArg :: forall c tv r. 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 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. SrcSpan -> Doc -> SrcSpan -> Doc -> TError t
ErrAliasApp  SrcSpan
sp Doc
name SrcSpan
sp'
  where
    name :: Doc
name            = forall a. PPrint a => a -> Doc
pprint              (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 -> [Char] -> BareType -> Expr
exprArg SourcePos
l [Char]
msg = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"exprArg: " forall a. [a] -> [a] -> [a]
++ [Char]
msg) 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)     = forall a. Located a -> a
val Located Expr
e
    go (RVar BTyVar
x RReft
_)       = Symbol -> Expr
EVar (forall a. Symbolic a => a -> Symbol
F.symbol BTyVar
x)
    go (RApp BTyCon
x [] [] RReft
_) = Symbol -> Expr
EVar (forall a. Symbolic a => a -> Symbol
F.symbol BTyCon
x)
    go (RApp BTyCon
f [BareType]
ts [] RReft
_) = LocSymbol -> [Expr] -> Expr
F.mkEApp (forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BTyCon -> LocSymbol
btc_tc BTyCon
f) (BareType -> Expr
go 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                = forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
sp forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => [Char] -> r
Printf.printf [Char]
"Unexpected expression parameter: %s in %s" (forall a. Show a => a -> [Char]
show BareType
z) [Char]
msg
    sp :: Maybe SrcSpan
sp                  = 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
         = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a e. Exception e => e -> a
Ex.throw forall a. a -> a
id (Env
-> SigEnv
-> ModName
-> PlugTV Var
-> LocBareType
-> Lookup LocSpecType
cookSpecTypeE Env
env SigEnv
sigEnv ModName
name PlugTV Var
x LocBareType
bt)
  where
    _msg :: [Char]
_msg = [Char]
"cookSpecType: " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr (Maybe Var
z, Var -> Kind
Ghc.varType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Var
z)
    z :: Maybe Var
z    = forall v. PlugTV v -> Maybe v
Bare.plugSrc PlugTV Var
x


-----------------------------------------------------------------------------------------
cookSpecTypeE :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.PlugTV Ghc.Var -> LocBareType
              -> Bare.Lookup LocSpecType
-----------------------------------------------------------------------------------------
cookSpecTypeE :: Env
-> SigEnv
-> ModName
-> PlugTV Var
-> LocBareType
-> Lookup LocSpecType
cookSpecTypeE Env
env SigEnv
sigEnv name :: ModName
name@(ModName ModType
_ ModuleName
_) PlugTV Var
x LocBareType
bt
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LocSpecType -> LocSpecType
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> LocBareType -> Lookup LocSpecType
bareSpecType Env
env ModName
name forall a b. (a -> b) -> a -> b
$ BareRTEnv -> LocBareType -> LocBareType
bareExpandType BareRTEnv
rtEnv LocBareType
bt
  where
    f :: LocSpecType -> LocSpecType
f = (if Bool
doplug Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
allowTC then Bool
-> SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType
plugHoles Bool
allowTC SigEnv
sigEnv ModName
name PlugTV Var
x else forall a. a -> a
id)
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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)
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
Bare.txRefSort TyConMap
tyi TCEmb TyCon
embs
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> SpecType
txExpToBind -- What does this function DO
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BareRTEnv -> LocSpecType -> LocSpecType
specExpandType BareRTEnv
rtEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PlugTV Var -> SpecType -> SpecType
generalizeWith PlugTV Var
x))
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Bool
doplug Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
allowTC then Bool
-> SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType
maybePlug Bool
allowTC SigEnv
sigEnv ModName
name PlugTV Var
x else forall a. a -> a
id)
        -- we do not qualify/resolve Expr/Pred when typeclass is enabled
        -- since ghci will not be able to recognize fully qualified names
        -- instead, we leave qualification to ghc elaboration
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
Bare.qualifyTop Env
env ModName
name SourcePos
l

    allowTC :: Bool
allowTC = Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig Env
env)
    -- modT   = mname `S.member` wiredInMods
    doplug :: Bool
doplug
      | Bare.LqTV Var
v <- PlugTV Var
x
      , forall a. Symbolic a => a -> Bool
GM.isMethod Var
v Bool -> Bool -> Bool
|| forall a. Symbolic a => a -> Bool
GM.isSCSel Var
v
      , Bool -> Bool
not (ModName -> Bool
isTarget ModName
name)
      = Bool
False
      | Bool
otherwise
      = Bool
True
    _msg :: a -> [Char]
_msg a
i = [Char]
"cook-" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show a
i forall a. [a] -> [a] -> [a]
++ [Char]
" : " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
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      = 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 = 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 = 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 (forall a b. [a] -> [b] -> [(a, b)]
zip [RTVar RTyVar (RType RTyCon RTyVar ())]
as (forall a. a -> [a]
repeat forall a. Monoid a => a
mempty)) [] SpecType
t
  where
    as :: [RTVar RTyVar (RType RTyCon RTyVar ())]
as            = forall a. (a -> Bool) -> [a] -> [a]
filter forall {s}. RTVar RTyVar s -> Bool
isGen (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.splitForAllTyCoVars (Var -> Kind
GM.expandVarType Var
v)
    isGen :: RTVar RTyVar s -> Bool
isGen (RTVar (RTV Var
a) RTVInfo s
_) = Var
a forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
vas

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


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

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

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

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

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

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

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

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

-}

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


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

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

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

--------------------------------------------------------------------------------
-- | @expandExpr@ applies the aliases and inlines in @BareRTEnv@ to its argument
--   @Expr@. It must first @resolve@ the symbols in the refinement to see if
--   they correspond to alias definitions. However, we ensure that we do not
--   resolve bound variables (e.g. those bound in output refinements by input
--   parameters), and we use the @bs@ parameter to pass in the bound symbols.
--------------------------------------------------------------------------------
expandExpr :: BareRTEnv -> F.SourcePos -> Expr -> Expr
expandExpr :: 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
ps)
    go (POr [Expr]
ps)         = [Expr] -> Expr
POr        (Expr -> Expr
go 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 -> 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     = forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases BareRTEnv
rtEnv
    mBody :: Maybe (Located (RTAlias Symbol Expr))
mBody   = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
f HashMap Symbol (Located (RTAlias Symbol Expr))
eAs forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` 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 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 :: forall ty.
Subable ty =>
SourcePos -> Located (RTAlias Symbol ty) -> [Expr] -> ty
expandApp SourcePos
l Located (RTAlias Symbol ty)
lre [Expr]
es
  | Just Subst
su <- Maybe Subst
args = forall a. Subable a => Subst -> a -> a
F.subst Subst
su (forall x a. RTAlias x a -> a
rtBody RTAlias Symbol ty
re)
  | Bool
otherwise       = forall a e. Exception e => e -> a
Ex.throw UserError
err
  where
    re :: RTAlias Symbol ty
re              = forall a. Located a -> a
F.val Located (RTAlias Symbol ty)
lre
    args :: Maybe Subst
args            = [(Symbol, Expr)] -> Subst
F.mkSubst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. [a] -> [b] -> Maybe [(a, b)]
Misc.zipMaybe (forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol ty
re) [Expr]
es
    err             :: UserError
    err :: UserError
err             = 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           = forall a. PPrint a => a -> Doc
pprint           (forall x a. RTAlias x a -> Symbol
rtName RTAlias Symbol ty
re)
    sp' :: SrcSpan
sp'             = 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.<+> forall a. PPrint a => a -> Doc
pprint (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ 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.<+> forall a. PPrint a => a -> Doc
pprint (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es)


-------------------------------------------------------------------------------
-- | Replace Predicate Arguments With Existentials ----------------------------
-------------------------------------------------------------------------------
txExpToBind   :: SpecType -> SpecType
-------------------------------------------------------------------------------
txExpToBind :: SpecType -> SpecType
txExpToBind SpecType
t = forall s a. State s a -> s -> a
evalState (SpecType -> State ExSt SpecType
expToBindT SpecType
t) (Int
-> HashMap Symbol (RType RTyCon RTyVar (), Expr)
-> HashMap Symbol RPVar
-> ExSt
ExSt Int
0 forall k v. HashMap k v
M.empty HashMap Symbol RPVar
πs)
  where
    πs :: HashMap Symbol RPVar
πs        = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(forall t. PVar t -> Symbol
pname RPVar
p, RPVar
p) | RPVar
p <- forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
t ]

data ExSt = ExSt { ExSt -> Int
fresh :: Int
                 , ExSt -> HashMap Symbol (RType RTyCon RTyVar (), Expr)
emap  :: M.HashMap F.Symbol (RSort, F.Expr)
                 , ExSt -> HashMap Symbol RPVar
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)
  = forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
v
expToBindT (RFun Symbol
x RFInfo
i 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
       forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i 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
       forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 RPVar
p SpecType
t)
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP RPVar
p) (SpecType -> State ExSt SpecType
expToBindT SpecType
t)
expToBindT (RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs RReft
r)
  = do [SpecType]
ts' <- 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' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM RTProp RTyCon RTyVar RReft
-> State ExSt (RTProp RTyCon RTyVar RReft)
expToBindReft [RTProp RTyCon RTyVar RReft]
rs
       forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
       forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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' <- forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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'   <- forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r
       SpecType
t'   <- SpecType -> State ExSt SpecType
expToBindT SpecType
t
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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) = forall a b. [(a, b)] -> ([a], [b])
unzip [(Symbol, SpecType)]
xts
expToBindT SpecType
t
  = forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

expToBindReft              :: SpecProp -> State ExSt SpecProp
expToBindReft :: RTProp RTyCon RTyVar RReft
-> State ExSt (RTProp RTyCon RTyVar RReft)
expToBindReft (RProp [(Symbol, RType RTyCon RTyVar ())]
s (RHole RReft
r)) = forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [(Symbol, RType RTyCon RTyVar ())]
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r. UReft r -> State ExSt (UReft r)
expToBindRef RReft
r
expToBindReft (RProp [(Symbol, RType RTyCon RTyVar ())]
s SpecType
t)  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RType RTyCon RTyVar ())]
s  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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt -> HashMap Symbol (RType RTyCon RTyVar (), Expr)
emap
       forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ExSt
st -> ExSt
st{emap :: HashMap Symbol (RType RTyCon RTyVar (), Expr)
emap = forall k v. HashMap k v
M.empty}
       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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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) = 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'               = forall r c tv. Reftable r => RType c tv () -> RType c tv r
ofRSort RType RTyCon RTyVar ()
tx forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`strengthen` forall r. r -> UReft r
uTop Reft
r
    r :: Reft
r                = forall a. Expression a => a -> Reft
F.exprReft Expr
e

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

expToBind :: UsedPVar -> State ExSt UsedPVar
expToBind :: UsedPVar -> State ExSt UsedPVar
expToBind UsedPVar
p = do
  Maybe RPVar
res <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (forall t. PVar t -> Symbol
pname UsedPVar
p) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExSt -> HashMap Symbol RPVar
pmap)
  case Maybe RPVar
res of
    Maybe RPVar
Nothing ->
      forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing ([Char]
"expToBind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show UsedPVar
p)
    Just RPVar
π  -> do
      let pargs0 :: [(((), Symbol, Expr), RType RTyCon RTyVar ())]
pargs0 = forall a b. [a] -> [b] -> [(a, b)]
zip (forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
p) (forall a b c. (a, b, c) -> a
Misc.fst3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. PVar t -> [(t, Symbol, Expr)]
pargs RPVar
π)
      [((), Symbol, Expr)]
pargs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (((), Symbol, Expr), RType RTyCon RTyVar ())
-> State ExSt ((), Symbol, Expr)
expToBindParg [(((), Symbol, Expr), RType RTyCon RTyVar ())]
pargs0
      forall (m :: * -> *) a. Monad m => a -> m a
return 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 ())
-> State ExSt ((), Symbol, Expr)
expToBindParg ((()
t, Symbol
s, Expr
e), RType RTyCon RTyVar ()
s') = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,,) ()
t Symbol
s) (Expr -> RType RTyCon RTyVar () -> State ExSt Expr
expToBindExpr Expr
e RType RTyCon RTyVar ()
s')

expToBindExpr :: F.Expr ->  RSort -> State ExSt F.Expr
expToBindExpr :: Expr -> RType RTyCon RTyVar () -> State ExSt Expr
expToBindExpr e :: Expr
e@(EVar Symbol
s) RType RTyCon RTyVar ()
_
  | Char -> Bool
Char.isLower forall a b. (a -> b) -> a -> b
$ Symbol -> Char
F.headSym forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol Symbol
s
  = 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
       forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ExSt
st -> ExSt
st{emap :: HashMap Symbol (RType RTyCon RTyVar (), Expr)
emap = 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)}
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
EVar Symbol
s

freshSymbol :: State ExSt F.Symbol
freshSymbol :: State ExSt Symbol
freshSymbol
  = do Int
n <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt -> Int
fresh
       forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ExSt
s -> ExSt
s {fresh :: Int
fresh = Int
nforall a. Num a => a -> a -> a
+Int
1}
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol forall a b. (a -> b) -> a -> b
$ [Char]
"ex#" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n


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