-- | 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     #-}
{-# OPTIONS_GHC -Wno-x-partial #-}

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

    -- * Expand
  , Expand(expand)

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

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

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

import           Control.Monad
import           Control.Monad.State
import           Data.Bifunctor (second)
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.PrettyPrint.HughesPJ as PJ

import qualified Language.Fixpoint.Types               as F
-- import qualified Language.Fixpoint.Types.Visitor       as F
import qualified Language.Fixpoint.Misc                as Misc
import           Language.Fixpoint.Types (Expr, ExprV(..), SourcePos) -- , Symbol, symbol)
import qualified Language.Haskell.Liquid.GHC.Misc      as GM
import qualified Liquid.GHC.API       as Ghc
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.DataDecl
import           Language.Haskell.Liquid.Types.Names
import qualified Language.Haskell.Liquid.Types.RefType as RT
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types
import 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
import           Language.Haskell.Liquid.UX.Config
import qualified Text.Printf                           as Printf

--------------------------------------------------------------------------------
-- | `makeRTEnv` initializes the env needed to `expand` refinements and types,
--   that is, the below needs to be called *before* we use `Expand.expand`
--------------------------------------------------------------------------------
makeRTEnv
  :: Bare.Env
  -> ModName
  -> Ms.BareSpec
  -> [(ModName, Ms.BareSpec)]
  -> LogicMap
  -> BareRTEnv
--------------------------------------------------------------------------------
makeRTEnv :: Env
-> ModName
-> BareSpec
-> [(ModName, BareSpec)]
-> LogicMap
-> BareRTEnv
makeRTEnv Env
env ModName
modName BareSpec
mySpec [(ModName, BareSpec)]
dependencySpecs 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 lname ty.
Spec lname ty -> [Located (RTAlias Symbol (BareTypeV lname))]
Ms.aliases  BareSpec
s ]
    eAs :: [Located (RTAlias Symbol Expr)]
eAs   = [ Located (RTAlias Symbol Expr)
e | (ModName
_m, BareSpec
s)  <- [(ModName, BareSpec)]
specs, Located (RTAlias Symbol Expr)
e <- BareSpec -> [Located (RTAlias Symbol Expr)]
forall lname ty.
Spec lname ty -> [Located (RTAlias Symbol (ExprV lname))]
Ms.ealiases BareSpec
s ]
         [Located (RTAlias Symbol Expr)]
-> [Located (RTAlias Symbol Expr)]
-> [Located (RTAlias Symbol Expr)]
forall a. [a] -> [a] -> [a]
++ if Config -> Bool
typeclass (Env -> Config
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 [ 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
modName, BareSpec
mySpec) (ModName, BareSpec)
-> [(ModName, BareSpec)] -> [(ModName, BareSpec)]
forall a. a -> [a] -> [a]
: [(ModName, BareSpec)]
dependencySpecs

-- | 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 = (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 a b. (a -> b) -> Located a -> Located b
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 a b. (a -> b) -> Located a -> Located b
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 = ys, rtBody = sbts (rtBody rt) (zip xs ys) }
  where
    xs :: [Symbol]
xs    = RTAlias Symbol BareType -> [Symbol]
forall x a. RTAlias x a -> [x]
rtTArgs RTAlias Symbol BareType
rt
    ys :: [Symbol]
ys    = (Symbol -> Symbol -> Symbol
`F.suffixSymbol` 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
    sbts :: BareType -> [(Symbol, Symbol)] -> BareType
sbts  = (BareType -> (Symbol, Symbol) -> BareType)
-> BareType -> [(Symbol, Symbol)] -> BareType
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (((Symbol, Symbol) -> BareType -> BareType)
-> BareType -> (Symbol, Symbol) -> BareType
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Symbol, Symbol) -> BareType -> BareType
forall tv ty a. SubsTy tv ty a => (tv, ty) -> a -> a
subt)


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

-- | @renameRTVArgs@ ensures that @RTAlias@ value parameters have distinct names
--   to avoid variable capture e.g. as in tests-names-pos-Capture01.hs
renameRTVArgs :: (F.PPrint a, F.Subable a) => 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 = newArgs
                      , rtBody  = F.notracepp msg $ F.subst su (rtBody rt)
                      }
  where
    msg :: [Char]
msg          = [Char]
"renameRTVArgs: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Subst -> [Char]
forall a. PPrint a => a -> [Char]
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 -> Int -> Symbol) -> [Symbol] -> [Int] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Symbol -> Int -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
rtArg (RTAlias x a -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias x a
rt) [(Int
0::Int)..]
    oldArgs :: [Symbol]
oldArgs      = RTAlias x a -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias x a
rt
    rtArg :: Symbol -> a -> Symbol
rtArg Symbol
x a
i    = Symbol -> Symbol -> Symbol
F.suffixSymbol Symbol
x (Symbol -> a -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
F.intSymbol Symbol
"rta" a
i)

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 x t. AliasTable x t -> BareType -> [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)

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

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
           = (thing -> Located (RTAlias x t) -> thing)
-> thing -> [Located (RTAlias x t)] -> thing
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' thing -> 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 :: 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 =  M.insert n a (typeAliases 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 :: 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 = M.insert n a (exprAliases 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 :: forall x t. [Located (RTAlias x t)] -> AliasTable x t
buildAliasTable = [(Symbol, Located (RTAlias x t))]
-> HashMap Symbol (Located (RTAlias x t))
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, Located (RTAlias x t))]
 -> HashMap Symbol (Located (RTAlias x t)))
-> ([Located (RTAlias x t)] -> [(Symbol, Located (RTAlias x t))])
-> [Located (RTAlias x t)]
-> HashMap Symbol (Located (RTAlias 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 :: forall x t. 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 -> [Char] -> a
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"fromAliasSymbol: Dangling alias symbol: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
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 = (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 :: forall t x.
PPrint t =>
(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 :: forall x t. 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. (HasCallStack, 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 :: forall x t. AliasTable x t -> [Symbol] -> Error
cycleAliasErr AliasTable x t
_ []          = Maybe SrcSpan -> [Char] -> Error
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
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    = (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]
symList }
  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 :: forall x t.
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, Int -> Node Symbol
lookupVertex, Symbol -> Maybe Int
_)
      = Graph Symbol -> (Graph, Int -> Node Symbol, 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
      = (Int -> Symbol) -> [Int] -> [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) -> (Int -> Node Symbol) -> Int -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Node Symbol
lookupVertex) ([Int] -> [Symbol]) -> [Int] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. [a] -> [a]
reverse ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ Graph -> [Int]
topSort Graph
digraph

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

ordNub :: Ord a => [a] -> [a]
ordNub :: forall a. Ord a => [a] -> [a]
ordNub = ([a] -> a) -> [[a]] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> a
forall a. HasCallStack => [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 :: AliasTable x t -> BareType -> [F.Symbol]
buildTypeEdges :: forall x t. AliasTable x t -> BareType -> [Symbol]
buildTypeEdges AliasTable x t
table = [Symbol] -> [Symbol]
forall a. Ord a => [a] -> [a]
ordNub ([Symbol] -> [Symbol])
-> (BareType -> [Symbol]) -> BareType -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> [Symbol]
forall {v} {tv} {r}. RTypeV v BTyCon tv r -> [Symbol]
go
  where
    -- go :: t -> [Symbol]
    go :: RTypeV v BTyCon tv r -> [Symbol]
go (RApp BTyCon
c [RTypeV v BTyCon tv r]
ts [RTPropV v BTyCon tv r]
rs r
_) = Symbol -> [Symbol]
go_alias (LHName -> Symbol
getLHNameSymbol (LHName -> Symbol) -> LHName -> Symbol
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located LHName
btc_tc BTyCon
c) [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (RTypeV v BTyCon tv r -> [Symbol])
-> [RTypeV v BTyCon tv r] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RTypeV v BTyCon tv r -> [Symbol]
go [RTypeV v BTyCon tv r]
ts [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (RTypeV v BTyCon tv r -> [Symbol])
-> [RTypeV v BTyCon tv r] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RTypeV v BTyCon tv r -> [Symbol]
go ((RTPropV v BTyCon tv r -> Maybe (RTypeV v BTyCon tv r))
-> [RTPropV v BTyCon tv r] -> [RTypeV v BTyCon tv r]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe RTPropV v BTyCon tv r -> Maybe (RTypeV v BTyCon tv r)
forall {τ} {v} {c} {tv} {r}.
Ref τ (RTypeV v c tv r) -> Maybe (RTypeV v c tv r)
go_ref [RTPropV v BTyCon tv r]
rs)
    go (RFun Symbol
_ RFInfo
_ RTypeV v BTyCon tv r
t1 RTypeV v BTyCon tv r
t2 r
_) = RTypeV v BTyCon tv r -> [Symbol]
go RTypeV v BTyCon tv r
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeV v BTyCon tv r -> [Symbol]
go RTypeV v BTyCon tv r
t2
    go (RAppTy RTypeV v BTyCon tv r
t1 RTypeV v BTyCon tv r
t2 r
_) = RTypeV v BTyCon tv r -> [Symbol]
go RTypeV v BTyCon tv r
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeV v BTyCon tv r -> [Symbol]
go RTypeV v BTyCon tv r
t2
    go (RAllE Symbol
_ RTypeV v BTyCon tv r
t1 RTypeV v BTyCon tv r
t2)  = RTypeV v BTyCon tv r -> [Symbol]
go RTypeV v BTyCon tv r
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeV v BTyCon tv r -> [Symbol]
go RTypeV v BTyCon tv r
t2
    go (REx Symbol
_ RTypeV v BTyCon tv r
t1 RTypeV v BTyCon tv r
t2)    = RTypeV v BTyCon tv r -> [Symbol]
go RTypeV v BTyCon tv r
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeV v BTyCon tv r -> [Symbol]
go RTypeV v BTyCon tv r
t2
    go (RAllT RTVUV v BTyCon tv
_ RTypeV v BTyCon tv r
t r
_)    = RTypeV v BTyCon tv r -> [Symbol]
go RTypeV v BTyCon tv r
t
    go (RAllP PVUV v BTyCon tv
_ RTypeV v BTyCon tv r
t)      = RTypeV v BTyCon tv r -> [Symbol]
go RTypeV v BTyCon tv r
t
    go (RVar tv
_ r
_)       = []
    go (RExprArg Located (ExprV v)
_)     = []
    go (RHole r
_)        = []
    go (RRTy [(Symbol, RTypeV v BTyCon tv r)]
env r
_ Oblig
_ RTypeV v BTyCon tv r
t) = ((Symbol, RTypeV v BTyCon tv r) -> [Symbol])
-> [(Symbol, RTypeV v BTyCon tv r)] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (RTypeV v BTyCon tv r -> [Symbol]
go (RTypeV v BTyCon tv r -> [Symbol])
-> ((Symbol, RTypeV v BTyCon tv r) -> RTypeV v BTyCon tv r)
-> (Symbol, RTypeV v BTyCon tv r)
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, RTypeV v BTyCon tv r) -> RTypeV v BTyCon tv r
forall a b. (a, b) -> b
snd) [(Symbol, RTypeV v BTyCon tv r)]
env [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeV v BTyCon tv r -> [Symbol]
go RTypeV v BTyCon 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 τ (RTypeV v c tv r) -> Maybe (RTypeV v c tv r)
go_ref (RProp [(Symbol, τ)]
_ (RHole r
_)) = Maybe (RTypeV v c tv r)
forall a. Maybe a
Nothing
    go_ref (RProp  [(Symbol, τ)]
_ RTypeV v c tv r
t) = RTypeV v c tv r -> Maybe (RTypeV v c tv r)
forall a. a -> Maybe a
Just RTypeV v 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  = [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

----------------------------------------------------------------------------------
expandLoc :: (Expand a) => BareRTEnv -> Located a -> Located a
expandLoc :: forall a. Expand a => 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 -> ReftV Symbol -> ReftV Symbol
expand BareRTEnv
rtEnv SourcePos
l (F.Reft (Symbol
v, Expr
ra)) = (Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
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 = (ReftV Symbol -> ReftV Symbol) -> RReft -> RReft
forall a b. (a -> b) -> UReftV Symbol a -> UReftV Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BareRTEnv -> SourcePos -> ReftV Symbol -> ReftV Symbol
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 = (r -> r) -> RTypeV Symbol c tv r -> RTypeV Symbol c tv r
forall a b.
(a -> b) -> RTypeV Symbol c tv a -> RTypeV Symbol c tv b
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 () where
  expand :: BareRTEnv -> SourcePos -> () -> ()
expand BareRTEnv
_ SourcePos
_ = () -> ()
forall a. a -> a
id

instance Expand (BRType ()) where
  expand :: BareRTEnv
-> SourcePos -> RType BTyCon BTyVar () -> RType BTyCon BTyVar ()
expand BareRTEnv
rtEnv SourcePos
l
    = BareRTEnv
-> SourcePos -> RType BTyCon BTyVar () -> RType BTyCon BTyVar ()
forall r c tv.
Expand r =>
BareRTEnv -> SourcePos -> RType c tv r -> RType c tv r
expandReft     BareRTEnv
rtEnv SourcePos
l -- apply expression aliases
    (RType BTyCon BTyVar () -> RType BTyCon BTyVar ())
-> (RType BTyCon BTyVar () -> RType BTyCon BTyVar ())
-> RType BTyCon BTyVar ()
-> RType BTyCon BTyVar ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> RType BTyCon BTyVar ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void
    (BareType -> RType BTyCon BTyVar ())
-> (RType BTyCon BTyVar () -> BareType)
-> RType BTyCon BTyVar ()
-> RType BTyCon BTyVar ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareRTEnv -> SourcePos -> BareType -> BareType
expandBareType BareRTEnv
rtEnv SourcePos
l -- apply type       aliases
    (BareType -> BareType)
-> (RType BTyCon BTyVar () -> BareType)
-> RType BTyCon BTyVar ()
-> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() -> RReft) -> RType BTyCon BTyVar () -> BareType
forall a b.
(a -> b)
-> RTypeV Symbol BTyCon BTyVar a -> RTypeV Symbol BTyCon BTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RReft -> () -> RReft
forall a b. a -> b -> a
const RReft
forall a. Monoid a => a
mempty)

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 = expand rtEnv l (rtBody 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 = expand rtEnv l (rtBody x) }

instance Expand Body where
  expand :: BareRTEnv -> SourcePos -> Body -> Body
expand BareRTEnv
rtEnv SourcePos
l (P   Expr
p) = Expr -> Body
forall v. ExprV v -> BodyV v
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
forall v. ExprV v -> BodyV v
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
forall v. Symbol -> ExprV v -> BodyV v
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  = expand rtEnv l (dcTheta c)
    , dcFields = [(x, expand rtEnv l t) | (x, t) <- dcFields c ]
    , dcResult = expand rtEnv l (dcResult c)
    }

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

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

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

instance Expand Ms.BareSpec where
  expand :: 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 a b. (a -> b) -> Maybe a -> Maybe b
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 a b. (a -> b) -> [a] -> [b]
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 a b. (a -> b) -> HashMap k a -> HashMap k b
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)

-- | 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   = expand rtEnv l (measures   sp)
  , asmSigs    = map (second (expand rtEnv l)) (asmSigs sp)
  , sigs       = map (second (expand rtEnv l)) (sigs sp)
  , ialiases   = [ (f x, f y) | (x, y) <- ialiases sp ]
  , dataDecls  = expand rtEnv l (dataDecls  sp)
  , newtyDecls = expand rtEnv l (newtyDecls sp)
  }
  where f :: 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
l = 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 v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp BTyCon
c (BareType -> BareType
go (BareType -> BareType) -> [BareType] -> [BareType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
ts) (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 v c tv r.
RTypeV v c tv r -> RTypeV v c tv r -> r -> RTypeV v 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) = Symbol -> RFInfo -> BareType -> BareType -> RReft -> BareType
forall v c tv r.
Symbol
-> RFInfo
-> RTypeV v c tv r
-> RTypeV v c tv r
-> r
-> RTypeV v 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)     = RTVar BTyVar (RType BTyCon BTyVar ())
-> BareType -> RReft -> BareType
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVar BTyVar (RType BTyCon BTyVar ())
a (BareType -> BareType
go BareType
t) RReft
r
    go (RAllP PVUV Symbol BTyCon BTyVar
a BareType
t)       = PVUV Symbol BTyCon BTyVar -> BareType -> BareType
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVUV Symbol BTyCon BTyVar
a (BareType -> BareType
go BareType
t)
    go (RAllE Symbol
x BareType
t1 BareType
t2)   = Symbol -> BareType -> BareType -> BareType
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v c tv r
RAllE Symbol
x (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2)
    go (REx Symbol
x BareType
t1 BareType
t2)     = Symbol -> BareType -> BareType -> BareType
forall v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v 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 v c tv r.
[(Symbol, RTypeV v c tv r)]
-> r -> Oblig -> RTypeV v c tv r -> RTypeV v 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 ())
 -> (Symbol, RType BTyCon BTyVar ()))
-> [(Symbol, RType BTyCon BTyVar ())]
-> [(Symbol, RType BTyCon BTyVar ())]
forall a b. (a -> b) -> [a] -> [b]
map (BareRTEnv
-> SourcePos -> RType BTyCon BTyVar () -> RType BTyCon BTyVar ()
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
expand BareRTEnv
rtEnv SourcePos
l (RType BTyCon BTyVar () -> RType BTyCon BTyVar ())
-> (Symbol, RType BTyCon BTyVar ())
-> (Symbol, RType BTyCon BTyVar ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) [(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 (LHName -> Symbol
getLHNameSymbol (LHName -> Symbol) -> LHName -> Symbol
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located LHName
btc_tc BTyCon
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. (HasCallStack, 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 v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v 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.subsTyVarsMeet [(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 v c tv r. RTypeV v c tv r -> RTypeV v 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 -> [Char] -> BareType -> Expr
exprArgFromBareType SourcePos
l [Char]
msg (BareType -> Expr) -> [BareType] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
es0
    ([BareType]
ts, [BareType]
es0) = Int -> [BareType] -> ([BareType], [BareType])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
nαs [BareType]
args
    ([BTyVar]
αs, [Symbol]
εs)  = (LocSymbol -> BTyVar
BTV (LocSymbol -> BTyVar) -> (Symbol -> LocSymbol) -> Symbol -> BTyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Symbol -> BTyVar) -> [Symbol] -> [BTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RTAlias Symbol BareType -> [Symbol]
forall x a. RTAlias x a -> [x]
rtTArgs RTAlias Symbol BareType
rta, RTAlias Symbol BareType -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol BareType
rta)
    targs :: [BareType]
targs     = (BareType -> Bool) -> [BareType] -> [BareType]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not (Bool -> Bool) -> (BareType -> Bool) -> BareType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> Bool
forall c tv r. RType c tv r -> Bool
isRExprArg) [BareType]
args
    eargs :: [BareType]
eargs     = (BareType -> Bool) -> [BareType] -> [BareType]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool) -> (BareType -> Bool) -> BareType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> Bool
forall c tv r. RType c tv r -> Bool
isRExprArg) [BareType]
args

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

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

isRExprArg :: RType c tv r -> Bool
isRExprArg :: forall c tv r. RType c tv r -> Bool
isRExprArg (RExprArg Located Expr
_) = Bool
True
isRExprArg RTypeV Symbol 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


----------------------------------------------------------------------------------------
-- | @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
         = ([Error] -> LocSpecType)
-> (LocSpecType -> LocSpecType)
-> Either [Error] LocSpecType
-> LocSpecType
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Error] -> LocSpecType
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw LocSpecType -> LocSpecType
forall a. a -> a
id (Env
-> SigEnv
-> ModName
-> PlugTV Var
-> LocBareType
-> Either [Error] LocSpecType
cookSpecTypeE Env
env SigEnv
sigEnv ModName
name PlugTV Var
x LocBareType
bt)
  where
    _msg :: [Char]
_msg = [Char]
"cookSpecType: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Maybe Var, Maybe Kind) -> [Char]
forall a. Outputable a => a -> [Char]
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
              -> Bare.Lookup LocSpecType
-----------------------------------------------------------------------------------------
cookSpecTypeE :: Env
-> SigEnv
-> ModName
-> PlugTV Var
-> LocBareType
-> Either [Error] LocSpecType
cookSpecTypeE Env
env SigEnv
sigEnv name :: ModName
name@(ModName ModType
_ ModuleName
_) PlugTV Var
x LocBareType
bt
  = (LocSpecType -> LocSpecType)
-> Either [Error] LocSpecType -> Either [Error] LocSpecType
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LocSpecType -> LocSpecType
f (Either [Error] LocSpecType -> Either [Error] LocSpecType)
-> (LocBareType -> Either [Error] LocSpecType)
-> LocBareType
-> Either [Error] LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> LocBareType -> Either [Error] LocSpecType
bareSpecType Env
env (LocBareType -> Either [Error] LocSpecType)
-> LocBareType -> Either [Error] LocSpecType
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 LocSpecType -> LocSpecType
forall a. a -> a
id)
        (LocSpecType -> LocSpecType)
-> (LocSpecType -> LocSpecType) -> LocSpecType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecType -> SpecType) -> LocSpecType -> LocSpecType
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TCEmb TyCon -> TyConMap -> SpecType -> SpecType
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> TyConMap -> RRType r -> RRType r
RT.addTyConInfo TCEmb TyCon
embs TyConMap
tyi)
        (LocSpecType -> LocSpecType)
-> (LocSpecType -> LocSpecType) -> LocSpecType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
Bare.txRefSort TyConMap
tyi TCEmb TyCon
embs
        (LocSpecType -> LocSpecType)
-> (LocSpecType -> LocSpecType) -> LocSpecType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecType -> SpecType) -> LocSpecType -> LocSpecType
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> SpecType
txExpToBind -- What does this function DO
        (LocSpecType -> LocSpecType)
-> (LocSpecType -> LocSpecType) -> LocSpecType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BareRTEnv -> LocSpecType -> LocSpecType
specExpandType BareRTEnv
rtEnv (LocSpecType -> LocSpecType)
-> (LocSpecType -> LocSpecType) -> LocSpecType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SpecType -> SpecType) -> LocSpecType -> LocSpecType
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PlugTV Var -> SpecType -> SpecType
generalizeWith PlugTV Var
x))
        (LocSpecType -> LocSpecType)
-> (LocSpecType -> LocSpecType) -> LocSpecType -> LocSpecType
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 LocSpecType -> LocSpecType
forall a. a -> a
id)

    allowTC :: Bool
allowTC = Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)
    -- modT   = mname `S.member` wiredInMods
    doplug :: Bool
doplug
      | Bare.LqTV Var
v <- PlugTV Var
x
      , Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isMethod Var
v Bool -> Bool -> Bool
|| Var -> Bool
forall a. Symbolic a => a -> Bool
GM.isSCSel Var
v
      , Bool -> Bool
not (ModName -> Bool
isTarget ModName
name)
      = Bool
False
      | Bool
otherwise
      = Bool
True
    _msg :: a -> [Char]
_msg a
i = [Char]
"cook-" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PlugTV Var -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp PlugTV Var
x
    rtEnv :: 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

-- | 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)]
-> [PVarV Symbol (RType RTyCon RTyVar ())] -> SpecType -> SpecType
forall (t :: * -> *) (t1 :: * -> *) tv v c r.
(Foldable t, Foldable t1) =>
t (RTVar tv (RTypeV v c tv ()), r)
-> t1 (PVarV v (RTypeV v c tv ()))
-> RTypeV v c tv r
-> RTypeV v 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 v c r.
Eq tv =>
RTypeV v c tv r -> [RTVar tv (RTypeV v c tv ())]
RT.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 Var -> [Var] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
vas

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


bareExpandType :: BareRTEnv -> LocBareType -> LocBareType
bareExpandType :: 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 -> LocBareType -> Bare.Lookup LocSpecType
bareSpecType :: Env -> LocBareType -> Either [Error] LocSpecType
bareSpecType Env
env LocBareType
bt = case HasCallStack =>
Env
-> SourcePos
-> Maybe [PVUV Symbol BTyCon BTyVar]
-> BareType
-> Lookup SpecType
Env
-> SourcePos
-> Maybe [PVUV Symbol BTyCon BTyVar]
-> BareType
-> Lookup SpecType
Bare.ofBareTypeE Env
env (LocBareType -> SourcePos
forall a. Located a -> SourcePos
F.loc LocBareType
bt) Maybe [PVUV Symbol BTyCon BTyVar]
forall a. Maybe a
Nothing (LocBareType -> BareType
forall a. Located a -> a
val LocBareType
bt) of
  Left [Error]
e  -> [Error] -> Either [Error] LocSpecType
forall a b. a -> Either a b
Left [Error]
e
  Right SpecType
t -> LocSpecType -> Either [Error] 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 :: 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 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
_  -> 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])
forall v. ExprV v -> (ExprV v, [ExprV v])
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
forall v. ExprV v -> ExprV v
ENeg       (Expr -> Expr
go Expr
e)
    go (ECst Expr
e Sort
s)       = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst       (Expr -> Expr
go Expr
e) Sort
s
    go (PAnd [Expr]
ps)        = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
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
forall v. [ExprV v] -> ExprV v
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
forall v. ExprV v -> ExprV v
PNot       (Expr -> Expr
go Expr
p)
    go (PAll [(Symbol, Sort)]
xs Expr
p)      = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll [(Symbol, Sort)]
xs    (Expr -> Expr
go Expr
p)
    go (PExist [(Symbol, Sort)]
xs Expr
p)    = [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
xs  (Expr -> Expr
go Expr
p)
    go (ELam (Symbol, Sort)
xt Expr
e)      = (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol, Sort)
xt    (Expr -> Expr
go Expr
e)
    go (ECoerc Sort
a Sort
t Expr
e)   = Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t (Expr -> Expr
go Expr
e)
    go (ETApp Expr
e Sort
s)      = Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ETApp      (Expr -> Expr
go Expr
e) Sort
s
    go (ETAbs Expr
e Symbol
s)      = Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
ETAbs      (Expr -> Expr
go Expr
e) Symbol
s
    go (EBin Bop
op Expr
e1 Expr
e2)  = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
op    (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PImp    Expr
e1 Expr
e2)  = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp       (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PIff    Expr
e1 Expr
e2)  = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff       (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PAtom Brel
b Expr
e1 Expr
e2)  = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
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
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
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
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
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
forall v. v -> ExprV v
EVar Symbol
s', [])

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

expandEApp :: BareRTEnv -> F.SourcePos -> (Expr, [Expr]) -> Expr
expandEApp :: 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
forall v. ExprV v -> [ExprV v] -> ExprV v
F.eApps       (Symbol -> Expr
forall v. v -> ExprV v
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   = 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 Maybe (Located (RTAlias Symbol Expr))
-> Maybe (Located (RTAlias Symbol Expr))
-> Maybe (Located (RTAlias Symbol Expr))
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` 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
forall v. ExprV v -> [ExprV v] -> ExprV v
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 = 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. (HasCallStack, 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.<+> Int -> Doc
forall a. PPrint a => a -> Doc
pprint ([Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Symbol] -> Int) -> [Symbol] -> Int
forall a b. (a -> b) -> a -> b
$ RTAlias Symbol ty -> [Symbol]
forall x a. RTAlias x a -> [Symbol]
rtVArgs RTAlias Symbol ty
re)
                   Doc -> Doc -> Doc
PJ.<+> Doc
"arguments but it is given"
                   Doc -> Doc -> Doc
PJ.<+> Int -> Doc
forall a. PPrint a => a -> Doc
pprint ([Expr] -> Int
forall a. [a] -> Int
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 = State ExSt SpecType -> ExSt -> SpecType
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 (PVarV Symbol (RType RTyCon RTyVar ()))
-> ExSt
ExSt Int
0 HashMap Symbol (RType RTyCon RTyVar (), Expr)
forall k v. HashMap k v
M.empty HashMap Symbol (PVarV Symbol (RType RTyCon RTyVar ()))
πs)
  where
    πs :: HashMap Symbol (PVarV Symbol (RType RTyCon RTyVar ()))
πs        = [(Symbol, PVarV Symbol (RType RTyCon RTyVar ()))]
-> HashMap Symbol (PVarV Symbol (RType RTyCon RTyVar ()))
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(PVarV Symbol (RType RTyCon RTyVar ()) -> Symbol
forall v t. PVarV v t -> Symbol
pname PVarV Symbol (RType RTyCon RTyVar ())
p, PVarV Symbol (RType RTyCon RTyVar ())
p) | PVarV Symbol (RType RTyCon RTyVar ())
p <- RTypeRepV Symbol RTyCon RTyVar RReft
-> [PVarV Symbol (RType RTyCon RTyVar ())]
forall v c tv r. RTypeRepV v c tv r -> [PVarV v (RTypeV v c tv ())]
ty_preds (RTypeRepV Symbol RTyCon RTyVar RReft
 -> [PVarV Symbol (RType RTyCon RTyVar ())])
-> RTypeRepV Symbol RTyCon RTyVar RReft
-> [PVarV Symbol (RType RTyCon RTyVar ())]
forall a b. (a -> b) -> a -> b
$ SpecType -> RTypeRepV Symbol RTyCon RTyVar RReft
forall v c tv r. RTypeV v c tv r -> RTypeRepV v 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 (PVarV Symbol (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 a b.
StateT ExSt Identity a
-> (a -> StateT ExSt Identity b) -> StateT ExSt Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SpecType -> State ExSt SpecType
addExists (SpecType -> State ExSt SpecType)
-> (RReft -> SpecType) -> RReft -> State ExSt SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTyVar -> RReft -> SpecType
forall v c tv r. tv -> r -> RTypeV v c tv r
RVar RTyVar
v
expToBindT (RFun Symbol
x RFInfo
i SpecType
t1 SpecType
t2 RReft
r)
  = do t1' <- SpecType -> State ExSt SpecType
expToBindT SpecType
t1
       t2' <- expToBindT t2
       expToBindRef r >>= addExists . RFun x i t1' t2'
expToBindT (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
a SpecType
t RReft
r)
  = do t' <- SpecType -> State ExSt SpecType
expToBindT SpecType
t
       expToBindRef r >>= addExists . RAllT a t'
expToBindT (RAllP PVarV Symbol (RType RTyCon RTyVar ())
p SpecType
t)
  = (SpecType -> SpecType)
-> State ExSt SpecType -> State ExSt SpecType
forall a b.
(a -> b) -> StateT ExSt Identity a -> StateT ExSt Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PVarV Symbol (RType RTyCon RTyVar ()) -> SpecType -> SpecType
forall v c tv r. PVUV v c tv -> RTypeV v c tv r -> RTypeV v c tv r
RAllP PVarV Symbol (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 ts' <- (SpecType -> State ExSt SpecType)
-> [SpecType] -> StateT ExSt Identity [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SpecType -> State ExSt SpecType
expToBindT [SpecType]
ts
       rs' <- mapM expToBindReft rs
       expToBindRef r >>= addExists . RApp c ts' rs'
expToBindT (RAppTy SpecType
t1 SpecType
t2 RReft
r)
  = do t1' <- SpecType -> State ExSt SpecType
expToBindT SpecType
t1
       t2' <- expToBindT t2
       expToBindRef r >>= addExists . RAppTy t1' t2'
expToBindT (RRTy [(Symbol, SpecType)]
xts RReft
r Oblig
o SpecType
t)
  = do xts' <- [Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs ([SpecType] -> [(Symbol, SpecType)])
-> StateT ExSt Identity [SpecType]
-> StateT ExSt Identity [(Symbol, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SpecType -> State ExSt SpecType)
-> [SpecType] -> StateT ExSt Identity [SpecType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SpecType -> State ExSt SpecType
expToBindT [SpecType]
ts
       r'   <- expToBindRef r
       t'   <- expToBindT t
       return $ RRTy xts' r' o t'
  where
     ([Symbol]
xs, [SpecType]
ts) = [(Symbol, SpecType)] -> ([Symbol], [SpecType])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Symbol, SpecType)]
xts
expToBindT SpecType
t
  = SpecType -> State ExSt SpecType
forall a. a -> StateT ExSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

expToBindReft              :: SpecProp -> State ExSt SpecProp
expToBindReft :: 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 v c tv. [(Symbol, τ)] -> r -> Ref τ (RTypeV v 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 bds <- (ExSt -> HashMap Symbol (RType RTyCon RTyVar (), Expr))
-> State ExSt (HashMap Symbol (RType RTyCon RTyVar (), Expr))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt -> HashMap Symbol (RType RTyCon RTyVar (), Expr)
emap
       modify $ \ExSt
st -> ExSt
st{emap = M.empty}
       return bds

addExists :: SpecType -> State ExSt SpecType
addExists :: SpecType -> State ExSt SpecType
addExists SpecType
t = (HashMap Symbol (RType RTyCon RTyVar (), Expr) -> SpecType)
-> State ExSt (HashMap Symbol (RType RTyCon RTyVar (), Expr))
-> State ExSt SpecType
forall a b.
(a -> b) -> StateT ExSt Identity a -> StateT ExSt Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SpecType -> Symbol -> (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 v c tv r.
Symbol -> RTypeV v c tv r -> RTypeV v c tv r -> RTypeV v 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 v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
`RT.strengthen` ReftV Symbol -> RReft
forall r v. r -> UReftV v r
RT.uTop ReftV Symbol
r
    r :: ReftV Symbol
r                = Expr -> ReftV Symbol
forall a. Expression a => a -> ReftV Symbol
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))
  = (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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM UsedPVar -> StateT ExSt Identity UsedPVar
expToBind [UsedPVar]
p StateT ExSt Identity [UsedPVar]
-> ([UsedPVar] -> UReftV Symbol r)
-> StateT ExSt Identity (UReftV Symbol r)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (r -> PredicateV Symbol -> UReftV Symbol r
forall v r. r -> PredicateV v -> UReftV v r
MkUReft r
r (PredicateV Symbol -> UReftV Symbol r)
-> ([UsedPVar] -> PredicateV Symbol)
-> [UsedPVar]
-> UReftV Symbol r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [UsedPVar] -> PredicateV Symbol
forall v. [UsedPVarV v] -> PredicateV v
Pr)

expToBind :: UsedPVar -> State ExSt UsedPVar
expToBind :: UsedPVar -> StateT ExSt Identity UsedPVar
expToBind UsedPVar
p = do
  res <- (ExSt -> Maybe (PVarV Symbol (RType RTyCon RTyVar ())))
-> StateT
     ExSt Identity (Maybe (PVarV Symbol (RType RTyCon RTyVar ())))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Symbol
-> HashMap Symbol (PVarV Symbol (RType RTyCon RTyVar ()))
-> Maybe (PVarV Symbol (RType RTyCon RTyVar ()))
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (UsedPVar -> Symbol
forall v t. PVarV v t -> Symbol
pname UsedPVar
p) (HashMap Symbol (PVarV Symbol (RType RTyCon RTyVar ()))
 -> Maybe (PVarV Symbol (RType RTyCon RTyVar ())))
-> (ExSt -> HashMap Symbol (PVarV Symbol (RType RTyCon RTyVar ())))
-> ExSt
-> Maybe (PVarV Symbol (RType RTyCon RTyVar ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExSt -> HashMap Symbol (PVarV Symbol (RType RTyCon RTyVar ()))
pmap)
  case res of
    Maybe (PVarV Symbol (RType RTyCon RTyVar ()))
Nothing ->
      Maybe SrcSpan -> [Char] -> StateT ExSt Identity UsedPVar
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"expToBind: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ UsedPVar -> [Char]
forall a. Show a => a -> [Char]
show UsedPVar
p)
    Just PVarV Symbol (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 v t. PVarV v t -> [(t, Symbol, ExprV v)]
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
<$> PVarV Symbol (RType RTyCon RTyVar ())
-> [(RType RTyCon RTyVar (), Symbol, Expr)]
forall v t. PVarV v t -> [(t, Symbol, ExprV v)]
pargs PVarV Symbol (RType RTyCon RTyVar ())
π)
      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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (((), Symbol, Expr), RType RTyCon RTyVar ())
-> StateT ExSt Identity ((), Symbol, Expr)
expToBindParg [(((), Symbol, Expr), RType RTyCon RTyVar ())]
pargs0
      return $ p { pargs = 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 a b.
(a -> b) -> StateT ExSt Identity a -> StateT ExSt Identity b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,,) ()
t Symbol
s) (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 a. a -> StateT ExSt Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
expToBindExpr Expr
e RType RTyCon RTyVar ()
t
  = do s <- State ExSt Symbol
freshSymbol
       modify $ \ExSt
st -> ExSt
st{emap = M.insert s (t, e) (emap st)}
       return $ EVar s

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


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