{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE TupleSections        #-}
{-# LANGUAGE PatternGuards        #-}
{-# LANGUAGE OverloadedStrings    #-}

--------------------------------------------------------------------------------
-- | `defunctionalize` traverses the query to:
--      1. "normalize" lambda terms by renaming binders,
--      2. generate alpha- and beta-equality axioms for
--   The lambdas and redexes found in the query.
--
--   NOTE: `defunctionalize` should happen **BEFORE**
--   `elaborate` as the latter converts all actual `EApp`
--   into the (uninterpreted) `smt_apply`.
--   We cannot elaborate prior to `defunc` as we need the
--   `EApp` and `ELam` to determine the lambdas and redexes.
--------------------------------------------------------------------------------

module Language.Fixpoint.Defunctionalize 
  ( defunctionalize
  , Defunc(..)
  , defuncAny
  ) where 

import qualified Data.HashMap.Strict as M
import           Data.Hashable
import           Control.Monad.State
import           Language.Fixpoint.Misc            (fM, secondM, mapSnd)
import           Language.Fixpoint.Solver.Sanitize (symbolEnv)
import           Language.Fixpoint.Types        hiding (allowHO)
import           Language.Fixpoint.Types.Config
import           Language.Fixpoint.Types.Visitor   (mapMExpr)
-- import Debug.Trace (trace)

defunctionalize :: (Fixpoint a) => Config -> SInfo a -> SInfo a
defunctionalize :: Config -> SInfo a -> SInfo a
defunctionalize Config
cfg SInfo a
si = State DFST (SInfo a) -> DFST -> SInfo a
forall s a. State s a -> s -> a
evalState (SInfo a -> State DFST (SInfo a)
forall a. Defunc a => a -> DF a
defunc SInfo a
si) (Config -> SInfo a -> DFST
forall a. Config -> SInfo a -> DFST
makeInitDFState Config
cfg SInfo a
si)

defuncAny :: Defunc a => Config -> SymEnv -> a -> a
defuncAny :: Config -> SymEnv -> a -> a
defuncAny Config
cfg SymEnv
env a
e = State DFST a -> DFST -> a
forall s a. State s a -> s -> a
evalState (a -> State DFST a
forall a. Defunc a => a -> DF a
defunc a
e) (Config -> SymEnv -> IBindEnv -> DFST
makeDFState Config
cfg SymEnv
env IBindEnv
emptyIBindEnv)


---------------------------------------------------------------------------------------------
-- | Expressions defunctionalization --------------------------------------------------------
---------------------------------------------------------------------------------------------
txExpr :: Expr -> DF Expr
txExpr :: Expr -> DF Expr
txExpr Expr
e = do
  Bool
hoFlag <- (DFST -> Bool) -> StateT DFST Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets DFST -> Bool
dfHO
  if Bool
hoFlag then Expr -> DF Expr
defuncExpr Expr
e else Expr -> DF Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

defuncExpr :: Expr -> DF Expr
defuncExpr :: Expr -> DF Expr
defuncExpr = (Expr -> DF Expr) -> Expr -> DF Expr
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Expr -> m Expr
mapMExpr Expr -> DF Expr
reBind
         (Expr -> DF Expr) -> (Expr -> DF Expr) -> Expr -> DF Expr
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Expr -> DF Expr) -> Expr -> DF Expr
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Expr -> m Expr
mapMExpr ((Expr -> Expr) -> Expr -> DF Expr
forall (m :: * -> *) a b. Monad m => (a -> b) -> a -> m b
fM Expr -> Expr
normalizeLams)

reBind :: Expr -> DF Expr
reBind :: Expr -> DF Expr
reBind (ELam (Symbol
x, Sort
s) Expr
e) = ((\Symbol
y -> (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
y, Sort
s) (Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
e (Symbol
x, Symbol -> Expr
EVar Symbol
y))) (Symbol -> Expr) -> StateT DFST Identity Symbol -> DF Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> StateT DFST Identity Symbol
freshSym Sort
s)
reBind Expr
e               = Expr -> DF Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
shiftLam :: Int -> Symbol -> Sort -> Expr -> Expr
shiftLam :: Int -> Symbol -> Sort -> Expr -> Expr
shiftLam Int
i Symbol
x Sort
t Expr
e = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x_i, Sort
t) (Expr
e Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
`subst1` (Symbol
x, Expr
x_i_t))
  where
    x_i :: Symbol
x_i          = Int -> Symbol
lamArgSymbol Int
i
    x_i_t :: Expr
x_i_t        = Expr -> Sort -> Expr
ECst (Symbol -> Expr
EVar Symbol
x_i) Sort
t

-- normalize lambda arguments [TODO: example]

normalizeLams :: Expr -> Expr
normalizeLams :: Expr -> Expr
normalizeLams Expr
e = (Int, Expr) -> Expr
forall a b. (a, b) -> b
snd ((Int, Expr) -> Expr) -> (Int, Expr) -> Expr
forall a b. (a -> b) -> a -> b
$ Int -> Expr -> (Int, Expr)
normalizeLamsFromTo Int
1 Expr
e

normalizeLamsFromTo :: Int -> Expr -> (Int, Expr)
normalizeLamsFromTo :: Int -> Expr -> (Int, Expr)
normalizeLamsFromTo Int
i   = Expr -> (Int, Expr)
go
  where
    go :: Expr -> (Int, Expr)
go (ELam (Symbol
y, Sort
sy) Expr
e) = (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int -> Symbol -> Sort -> Expr -> Expr
shiftLam Int
i Symbol
y Sort
sy Expr
e') where (Int
i, Expr
e') = Expr -> (Int, Expr)
go Expr
e
                          -- let (i', e') = go e
                          --    y'       = lamArgSymbol i'  -- SHIFTLAM
                          -- in (i' + 1, ELam (y', sy) (e' `subst1` (y, EVar y')))
    go (EApp Expr
e1 Expr
e2)     = let (Int
i1, Expr
e1') = Expr -> (Int, Expr)
go Expr
e1
                              (Int
i2, Expr
e2') = Expr -> (Int, Expr)
go Expr
e2
                          in (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
i1 Int
i2, Expr -> Expr -> Expr
EApp Expr
e1' Expr
e2')
    go (ECst Expr
e Sort
s)       = (Expr -> Expr) -> (Int, Expr) -> (Int, Expr)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (Expr -> Sort -> Expr
`ECst` Sort
s) (Expr -> (Int, Expr)
go Expr
e)
    go (PAll [(Symbol, Sort)]
bs Expr
e)      = (Expr -> Expr) -> (Int, Expr) -> (Int, Expr)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd ([(Symbol, Sort)] -> Expr -> Expr
PAll [(Symbol, Sort)]
bs) (Expr -> (Int, Expr)
go Expr
e)
    go Expr
e                = (Int
i, Expr
e)


--------------------------------------------------------------------------------
-- | Containers defunctionalization --------------------------------------------
--------------------------------------------------------------------------------

class Defunc a where
  defunc :: a -> DF a

instance (Defunc (c a), TaggedC c a) => Defunc (GInfo c a) where
  defunc :: GInfo c a -> DF (GInfo c a)
defunc GInfo c a
fi = do
    HashMap SubcId (c a)
cm'    <- HashMap SubcId (c a) -> DF (HashMap SubcId (c a))
forall a. Defunc a => a -> DF a
defunc (HashMap SubcId (c a) -> DF (HashMap SubcId (c a)))
-> HashMap SubcId (c a) -> DF (HashMap SubcId (c a))
forall a b. (a -> b) -> a -> b
$ GInfo c a -> HashMap SubcId (c a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm    GInfo c a
fi
    HashMap KVar (WfC a)
ws'    <- HashMap KVar (WfC a) -> DF (HashMap KVar (WfC a))
forall a. Defunc a => a -> DF a
defunc (HashMap KVar (WfC a) -> DF (HashMap KVar (WfC a)))
-> HashMap KVar (WfC a) -> DF (HashMap KVar (WfC a))
forall a b. (a -> b) -> a -> b
$ GInfo c a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws    GInfo c a
fi
    -- NOPROP setBinds $ mconcat ((senv <$> M.elems (cm fi)) ++ (wenv <$> M.elems (ws fi)))
    SEnv Sort
gLits' <- SEnv Sort -> DF (SEnv Sort)
forall a. Defunc a => a -> DF a
defunc (SEnv Sort -> DF (SEnv Sort)) -> SEnv Sort -> DF (SEnv Sort)
forall a b. (a -> b) -> a -> b
$ GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits GInfo c a
fi
    SEnv Sort
dLits' <- SEnv Sort -> DF (SEnv Sort)
forall a. Defunc a => a -> DF a
defunc (SEnv Sort -> DF (SEnv Sort)) -> SEnv Sort -> DF (SEnv Sort)
forall a b. (a -> b) -> a -> b
$ GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits GInfo c a
fi
    BindEnv
bs'    <- BindEnv -> DF BindEnv
forall a. Defunc a => a -> DF a
defunc (BindEnv -> DF BindEnv) -> BindEnv -> DF BindEnv
forall a b. (a -> b) -> a -> b
$ GInfo c a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs    GInfo c a
fi
    [Triggered Expr]
ass'   <- [Triggered Expr] -> DF [Triggered Expr]
forall a. Defunc a => a -> DF a
defunc ([Triggered Expr] -> DF [Triggered Expr])
-> [Triggered Expr] -> DF [Triggered Expr]
forall a b. (a -> b) -> a -> b
$ GInfo c a -> [Triggered Expr]
forall (c :: * -> *) a. GInfo c a -> [Triggered Expr]
asserts GInfo c a
fi
    -- NOPROP quals' <- defunc $ quals fi
    GInfo c a -> DF (GInfo c a)
forall (m :: * -> *) a. Monad m => a -> m a
return (GInfo c a -> DF (GInfo c a)) -> GInfo c a -> DF (GInfo c a)
forall a b. (a -> b) -> a -> b
$ GInfo c a
fi { cm :: HashMap SubcId (c a)
cm      = HashMap SubcId (c a)
cm'
                , ws :: HashMap KVar (WfC a)
ws      = HashMap KVar (WfC a)
ws'
                , gLits :: SEnv Sort
gLits   = SEnv Sort
gLits'
                , dLits :: SEnv Sort
dLits   = SEnv Sort
dLits'
                , bs :: BindEnv
bs      = BindEnv
bs'
                , asserts :: [Triggered Expr]
asserts = [Triggered Expr]
ass'
                }

instance (Defunc a) => Defunc (Triggered a) where
  defunc :: Triggered a -> DF (Triggered a)
defunc (TR Trigger
t a
e) = Trigger -> a -> Triggered a
forall a. Trigger -> a -> Triggered a
TR Trigger
t (a -> Triggered a) -> StateT DFST Identity a -> DF (Triggered a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> StateT DFST Identity a
forall a. Defunc a => a -> DF a
defunc a
e

instance Defunc (SimpC a) where
  defunc :: SimpC a -> DF (SimpC a)
defunc SimpC a
sc = do Expr
crhs' <- Expr -> DF Expr
forall a. Defunc a => a -> DF a
defunc (Expr -> DF Expr) -> Expr -> DF Expr
forall a b. (a -> b) -> a -> b
$ SimpC a -> Expr
forall a. SimpC a -> Expr
_crhs SimpC a
sc
                 SimpC a -> DF (SimpC a)
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpC a -> DF (SimpC a)) -> SimpC a -> DF (SimpC a)
forall a b. (a -> b) -> a -> b
$ SimpC a
sc {_crhs :: Expr
_crhs = Expr
crhs'}

instance Defunc (WfC a)   where
  defunc :: WfC a -> DF (WfC a)
defunc wf :: WfC a
wf@(WfC {}) = do
    let (Symbol
x, Sort
t, KVar
k) = WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
wf
    Sort
t' <- Sort -> DF Sort
forall a. Defunc a => a -> DF a
defunc Sort
t
    WfC a -> DF (WfC a)
forall (m :: * -> *) a. Monad m => a -> m a
return (WfC a -> DF (WfC a)) -> WfC a -> DF (WfC a)
forall a b. (a -> b) -> a -> b
$ WfC a
wf { wrft :: (Symbol, Sort, KVar)
wrft = (Symbol
x, Sort
t', KVar
k) }
  defunc wf :: WfC a
wf@(GWfC {}) = do
    let (Symbol
x, Sort
t, KVar
k) = WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
wf
    Sort
t' <- Sort -> DF Sort
forall a. Defunc a => a -> DF a
defunc Sort
t
    Expr
e' <- Expr -> DF Expr
forall a. Defunc a => a -> DF a
defunc (Expr -> DF Expr) -> Expr -> DF Expr
forall a b. (a -> b) -> a -> b
$ WfC a -> Expr
forall a. WfC a -> Expr
wexpr WfC a
wf
    WfC a -> DF (WfC a)
forall (m :: * -> *) a. Monad m => a -> m a
return (WfC a -> DF (WfC a)) -> WfC a -> DF (WfC a)
forall a b. (a -> b) -> a -> b
$ WfC a
wf { wrft :: (Symbol, Sort, KVar)
wrft = (Symbol
x, Sort
t', KVar
k), wexpr :: Expr
wexpr = Expr
e' }

instance Defunc SortedReft where
  defunc :: SortedReft -> DF SortedReft
defunc (RR Sort
s Reft
r) = Sort -> Reft -> SortedReft
RR Sort
s (Reft -> SortedReft) -> StateT DFST Identity Reft -> DF SortedReft
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Reft -> StateT DFST Identity Reft
forall a. Defunc a => a -> DF a
defunc Reft
r

instance Defunc (Symbol, SortedReft) where
  defunc :: (Symbol, SortedReft) -> DF (Symbol, SortedReft)
defunc (Symbol
x, SortedReft
sr) = (Symbol
x,) (SortedReft -> (Symbol, SortedReft))
-> DF SortedReft -> DF (Symbol, SortedReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SortedReft -> DF SortedReft
forall a. Defunc a => a -> DF a
defunc SortedReft
sr

instance Defunc (Symbol, Sort) where
  defunc :: (Symbol, Sort) -> DF (Symbol, Sort)
defunc (Symbol
x, Sort
t) = (Symbol
x,) (Sort -> (Symbol, Sort)) -> DF Sort -> DF (Symbol, Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> DF Sort
forall a. Defunc a => a -> DF a
defunc Sort
t

instance Defunc Reft where
  defunc :: Reft -> StateT DFST Identity Reft
defunc (Reft (Symbol
x, Expr
e)) = (Symbol, Expr) -> Reft
Reft ((Symbol, Expr) -> Reft)
-> (Expr -> (Symbol, Expr)) -> Expr -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x,) (Expr -> Reft) -> DF Expr -> StateT DFST Identity Reft
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> DF Expr
forall a. Defunc a => a -> DF a
defunc Expr
e

instance Defunc Expr where
  defunc :: Expr -> DF Expr
defunc = Expr -> DF Expr
txExpr

instance Defunc a => Defunc (SEnv a) where
  defunc :: SEnv a -> DF (SEnv a)
defunc = (a -> StateT DFST Identity a) -> SEnv a -> DF (SEnv a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SEnv a -> m (SEnv b)
mapMSEnv a -> StateT DFST Identity a
forall a. Defunc a => a -> DF a
defunc

instance Defunc BindEnv   where
  defunc :: BindEnv -> DF BindEnv
defunc BindEnv
bs = do IBindEnv
dfbs <- (DFST -> IBindEnv) -> StateT DFST Identity IBindEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets DFST -> IBindEnv
dfBEnv
                 let f :: (Int, (t, SortedReft))
-> StateT DFST Identity (Int, (t, SortedReft))
f (Int
i, (t, SortedReft)
xs) = if Int
i Int -> IBindEnv -> Bool
`memberIBindEnv` IBindEnv
dfbs
                                       then  (Int
i,) ((t, SortedReft) -> (Int, (t, SortedReft)))
-> StateT DFST Identity (t, SortedReft)
-> StateT DFST Identity (Int, (t, SortedReft))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (t, SortedReft) -> StateT DFST Identity (t, SortedReft)
forall a. Defunc a => a -> DF a
defunc (t, SortedReft)
xs
                                       else  (Int
i,) ((t, SortedReft) -> (Int, (t, SortedReft)))
-> StateT DFST Identity (t, SortedReft)
-> StateT DFST Identity (Int, (t, SortedReft))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (t, SortedReft) -> StateT DFST Identity (t, SortedReft)
forall t. (t, SortedReft) -> StateT DFST Identity (t, SortedReft)
matchSort (t, SortedReft)
xs
                 ((Int, (Symbol, SortedReft))
 -> StateT DFST Identity (Int, (Symbol, SortedReft)))
-> BindEnv -> DF BindEnv
forall (m :: * -> *).
Monad m =>
((Int, (Symbol, SortedReft)) -> m (Int, (Symbol, SortedReft)))
-> BindEnv -> m BindEnv
mapWithKeyMBindEnv (Int, (Symbol, SortedReft))
-> StateT DFST Identity (Int, (Symbol, SortedReft))
forall t.
Defunc (t, SortedReft) =>
(Int, (t, SortedReft))
-> StateT DFST Identity (Int, (t, SortedReft))
f BindEnv
bs
   where
    -- The refinement cannot be elaborated thus defunc-ed because
    -- the bind does not appear in any contraint,
    -- thus unique binders does not perform properly
    -- The sort should be defunc, to ensure same sort on double binders
    matchSort :: (t, SortedReft) -> StateT DFST Identity (t, SortedReft)
matchSort (t
x, RR Sort
s Reft
r) = ((t
x,) (SortedReft -> (t, SortedReft))
-> (Sort -> SortedReft) -> Sort -> (t, SortedReft)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort -> Reft -> SortedReft
`RR` Reft
r)) (Sort -> (t, SortedReft))
-> DF Sort -> StateT DFST Identity (t, SortedReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> DF Sort
forall a. Defunc a => a -> DF a
defunc Sort
s

-- Sort defunctionalization [should be done by elaboration]
instance Defunc Sort where
  defunc :: Sort -> DF Sort
defunc = Sort -> DF Sort
forall (m :: * -> *) a. Monad m => a -> m a
return

instance Defunc a => Defunc [a] where
  defunc :: [a] -> DF [a]
defunc = (a -> StateT DFST Identity a) -> [a] -> DF [a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> StateT DFST Identity a
forall a. Defunc a => a -> DF a
defunc

instance (Defunc a, Eq k, Hashable k) => Defunc (M.HashMap k a) where
  defunc :: HashMap k a -> DF (HashMap k a)
defunc HashMap k a
m = [(k, a)] -> HashMap k a
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(k, a)] -> HashMap k a)
-> StateT DFST Identity [(k, a)] -> DF (HashMap k a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((k, a) -> StateT DFST Identity (k, a))
-> [(k, a)] -> StateT DFST Identity [(k, a)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((a -> StateT DFST Identity a)
-> (k, a) -> StateT DFST Identity (k, a)
forall (f :: * -> *) b c a.
Functor f =>
(b -> f c) -> (a, b) -> f (a, c)
secondM a -> StateT DFST Identity a
forall a. Defunc a => a -> DF a
defunc) (HashMap k a -> [(k, a)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap k a
m)

type DF    = State DFST

data DFST = DFST
  { DFST -> Int
dfFresh :: !Int
  , DFST -> SymEnv
dfEnv   :: !SymEnv
  , DFST -> IBindEnv
dfBEnv  :: !IBindEnv
  , DFST -> Bool
dfHO    :: !Bool        -- ^ allow higher order thus defunctionalize
  , DFST -> [Expr]
dfLams  :: ![Expr]      -- ^ lambda expressions appearing in the expressions
  , DFST -> [Expr]
dfRedex :: ![Expr]      -- ^ redexes appearing in the expressions
  , DFST -> SEnv Sort
dfBinds :: !(SEnv Sort) -- ^ sorts of new lambda-binders
  }

makeDFState :: Config -> SymEnv -> IBindEnv -> DFST
makeDFState :: Config -> SymEnv -> IBindEnv -> DFST
makeDFState Config
cfg SymEnv
env IBindEnv
ibind = DFST :: Int
-> SymEnv
-> IBindEnv
-> Bool
-> [Expr]
-> [Expr]
-> SEnv Sort
-> DFST
DFST
  { dfFresh :: Int
dfFresh = Int
0
  , dfEnv :: SymEnv
dfEnv   = SymEnv
env
  , dfBEnv :: IBindEnv
dfBEnv  = IBindEnv
ibind
  , dfHO :: Bool
dfHO    = Config -> Bool
allowHO Config
cfg  Bool -> Bool -> Bool
|| Config -> Bool
defunction Config
cfg
  -- INVARIANT: lambads and redexes are not defunctionalized
  , dfLams :: [Expr]
dfLams  = []
  , dfRedex :: [Expr]
dfRedex = []
  , dfBinds :: SEnv Sort
dfBinds = SEnv Sort
forall a. Monoid a => a
mempty
  }

makeInitDFState :: Config -> SInfo a -> DFST
makeInitDFState :: Config -> SInfo a -> DFST
makeInitDFState Config
cfg SInfo a
si
  = Config -> SymEnv -> IBindEnv -> DFST
makeDFState Config
cfg
      (Config -> SInfo a -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si)
      ([IBindEnv] -> IBindEnv
forall a. Monoid a => [a] -> a
mconcat ((SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv (SimpC a -> IBindEnv) -> [SimpC a] -> [IBindEnv]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap SubcId (SimpC a) -> [SimpC a]
forall k v. HashMap k v -> [v]
M.elems (SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
si)) [IBindEnv] -> [IBindEnv] -> [IBindEnv]
forall a. [a] -> [a] -> [a]
++ (WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
wenv (WfC a -> IBindEnv) -> [WfC a] -> [IBindEnv]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap KVar (WfC a) -> [WfC a]
forall k v. HashMap k v -> [v]
M.elems (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws SInfo a
si))))

--------------------------------------------------------------------------------
-- | Low level monad manipulation ----------------------------------------------
--------------------------------------------------------------------------------
freshSym :: Sort -> DF Symbol
freshSym :: Sort -> StateT DFST Identity Symbol
freshSym Sort
t = do
  Int
n    <- (DFST -> Int) -> StateT DFST Identity Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets DFST -> Int
dfFresh
  let x :: Symbol
x = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"lambda_fun_" Int
n
  (DFST -> DFST) -> StateT DFST Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((DFST -> DFST) -> StateT DFST Identity ())
-> (DFST -> DFST) -> StateT DFST Identity ()
forall a b. (a -> b) -> a -> b
$ \DFST
s -> DFST
s {dfFresh :: Int
dfFresh = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, dfBinds :: SEnv Sort
dfBinds = Symbol -> Sort -> SEnv Sort -> SEnv Sort
forall a. Symbol -> a -> SEnv a -> SEnv a
insertSEnv Symbol
x Sort
t (DFST -> SEnv Sort
dfBinds DFST
s)}
  Symbol -> StateT DFST Identity Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return Symbol
x


-- | getLams and getRedexes return the (previously seen) lambdas and redexes,
--   after "closing" them by quantifying out free vars corresponding to the
--   fresh binders in `dfBinds`.