{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE TupleSections        #-}
{-# 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           Data.Bifunctor (bimap)
import           Control.Monad ((>=>))
import           Control.Monad.State
import           Language.Fixpoint.Misc            (fM, secondM)
import           Language.Fixpoint.Solver.Sanitize (symbolEnv)
import           Language.Fixpoint.Types        hiding (GInfo(..), allowHO, fi)
import qualified Language.Fixpoint.Types           as Types (GInfo(..))
import           Language.Fixpoint.Types.Config
import           Language.Fixpoint.Types.Visitor   (mapMExpr)


-- import Debug.Trace (trace)

defunctionalize :: (Fixpoint a) => Config -> SInfo a -> SInfo a
defunctionalize :: forall a. Fixpoint a => 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 :: forall a. Defunc a => 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 :: ExprV Symbol -> DF (ExprV Symbol)
txExpr ExprV Symbol
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 ExprV Symbol -> DF (ExprV Symbol)
defuncExpr ExprV Symbol
e else ExprV Symbol -> DF (ExprV Symbol)
forall a. a -> StateT DFST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ExprV Symbol
e

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

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

-- | normalize lambda arguments [TODO: example]
--
-- Renames lambda bindings to lamb_arg##i. Each use of a lambda binding
-- is surrounded with a cast.

normalizeLams :: Expr -> Expr
normalizeLams :: ExprV Symbol -> ExprV Symbol
normalizeLams = (Int, ExprV Symbol) -> ExprV Symbol
forall a b. (a, b) -> b
snd ((Int, ExprV Symbol) -> ExprV Symbol)
-> (ExprV Symbol -> (Int, ExprV Symbol))
-> ExprV Symbol
-> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ExprV Symbol -> (Int, ExprV Symbol)
normalizeLamsFromTo Int
1

normalizeLamsFromTo :: Int -> Expr -> (Int, Expr)
normalizeLamsFromTo :: Int -> ExprV Symbol -> (Int, ExprV Symbol)
normalizeLamsFromTo Int
i   = ExprV Symbol -> (Int, ExprV Symbol)
go
  where
    go :: Expr -> (Int, Expr)
    go :: ExprV Symbol -> (Int, ExprV Symbol)
go (ELam (Symbol
y, Sort
sy) ExprV Symbol
e) = (Int
i' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int -> Symbol -> Sort -> ExprV Symbol -> ExprV Symbol
shiftLam Int
i' Symbol
y Sort
sy ExprV Symbol
e') where (Int
i', ExprV Symbol
e') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e
                          -- let (i', e') = go e
                          --    y'       = lamArgSymbol i'  -- SHIFTLAM
                          -- in (i' + 1, ELam (y', sy) (e' `subst1` (y, EVar y')))
    go (EApp ExprV Symbol
e1 ExprV Symbol
e2)     = let (Int
i1, ExprV Symbol
e1') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e1
                              (Int
i2, ExprV Symbol
e2') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e2
                          in (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
i1 Int
i2, ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
EApp ExprV Symbol
e1' ExprV Symbol
e2')
    go (ECst ExprV Symbol
e Sort
s)       = (ExprV Symbol -> ExprV Symbol)
-> (Int, ExprV Symbol) -> (Int, ExprV Symbol)
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
`ECst` Sort
s) (ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e)
    go (EIte ExprV Symbol
e1 ExprV Symbol
e2 ExprV Symbol
e3)  = let (Int
i1, ExprV Symbol
e1') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e1
                              (Int
i2, ExprV Symbol
e2') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e2
                              (Int
i3, ExprV Symbol
e3') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e3
                          in ([Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int
i1, Int
i2, Int
i3], ExprV Symbol -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte ExprV Symbol
e1' ExprV Symbol
e2' ExprV Symbol
e3')
    go (ENeg ExprV Symbol
e)         = (ExprV Symbol -> ExprV Symbol)
-> (Int, ExprV Symbol) -> (Int, ExprV Symbol)
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
ENeg (ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e)
    go (EBin Bop
op ExprV Symbol
e1 ExprV Symbol
e2)  = let (Int
i1, ExprV Symbol
e1') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e1
                              (Int
i2, ExprV Symbol
e2') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e2
                          in (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
i1 Int
i2, Bop -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
op ExprV Symbol
e1' ExprV Symbol
e2')
    go (ETApp ExprV Symbol
e Sort
s)      = (ExprV Symbol -> ExprV Symbol)
-> (Int, ExprV Symbol) -> (Int, ExprV Symbol)
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
`ETApp` Sort
s) (ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e)
    go (ETAbs ExprV Symbol
e Symbol
s)      = (ExprV Symbol -> ExprV Symbol)
-> (Int, ExprV Symbol) -> (Int, ExprV Symbol)
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ExprV Symbol -> Symbol -> ExprV Symbol
forall v. ExprV v -> Symbol -> ExprV v
`ETAbs` Symbol
s) (ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e)
    go (PAnd [])        = (Int
i, [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
PAnd [])
    go (POr [])         = (Int
i, [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
POr  [])
    go (PAnd [ExprV Symbol]
es)        = ([Int] -> Int)
-> ([ExprV Symbol] -> ExprV Symbol)
-> ([Int], [ExprV Symbol])
-> (Int, ExprV Symbol)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
PAnd (([Int], [ExprV Symbol]) -> (Int, ExprV Symbol))
-> ([Int], [ExprV Symbol]) -> (Int, ExprV Symbol)
forall a b. (a -> b) -> a -> b
$ [(Int, ExprV Symbol)] -> ([Int], [ExprV Symbol])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Int, ExprV Symbol)] -> ([Int], [ExprV Symbol]))
-> [(Int, ExprV Symbol)] -> ([Int], [ExprV Symbol])
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> (Int, ExprV Symbol))
-> [ExprV Symbol] -> [(Int, ExprV Symbol)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ExprV Symbol -> (Int, ExprV Symbol)
go [ExprV Symbol]
es
    go (POr [ExprV Symbol]
es)         = ([Int] -> Int)
-> ([ExprV Symbol] -> ExprV Symbol)
-> ([Int], [ExprV Symbol])
-> (Int, ExprV Symbol)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
POr  (([Int], [ExprV Symbol]) -> (Int, ExprV Symbol))
-> ([Int], [ExprV Symbol]) -> (Int, ExprV Symbol)
forall a b. (a -> b) -> a -> b
$ [(Int, ExprV Symbol)] -> ([Int], [ExprV Symbol])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Int, ExprV Symbol)] -> ([Int], [ExprV Symbol]))
-> [(Int, ExprV Symbol)] -> ([Int], [ExprV Symbol])
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> (Int, ExprV Symbol))
-> [ExprV Symbol] -> [(Int, ExprV Symbol)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ExprV Symbol -> (Int, ExprV Symbol)
go [ExprV Symbol]
es
    go (PNot ExprV Symbol
e)         = (ExprV Symbol -> ExprV Symbol)
-> (Int, ExprV Symbol) -> (Int, ExprV Symbol)
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
PNot (ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e)
    go (PImp ExprV Symbol
e1 ExprV Symbol
e2)     = let (Int
i1, ExprV Symbol
e1') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e1
                              (Int
i2, ExprV Symbol
e2') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e2
                          in (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
i1 Int
i2, ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
PImp ExprV Symbol
e1' ExprV Symbol
e2')
    go (PIff ExprV Symbol
e1 ExprV Symbol
e2)     = let (Int
i1, ExprV Symbol
e1') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e1
                              (Int
i2, ExprV Symbol
e2') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e2
                          in (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
i1 Int
i2, ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
PIff ExprV Symbol
e1' ExprV Symbol
e2')
    go (PAtom Brel
r ExprV Symbol
e1 ExprV Symbol
e2)  = let (Int
i1, ExprV Symbol
e1') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e1
                              (Int
i2, ExprV Symbol
e2') = ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e2
                          in (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
i1 Int
i2, Brel -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r ExprV Symbol
e1' ExprV Symbol
e2')
    go (PAll [(Symbol, Sort)]
bs ExprV Symbol
e)      = (ExprV Symbol -> ExprV Symbol)
-> (Int, ExprV Symbol) -> (Int, ExprV Symbol)
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Symbol, Sort)] -> ExprV Symbol -> ExprV Symbol
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll [(Symbol, Sort)]
bs) (ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e)
    go (PExist [(Symbol, Sort)]
bs ExprV Symbol
e)    = (ExprV Symbol -> ExprV Symbol)
-> (Int, ExprV Symbol) -> (Int, ExprV Symbol)
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Symbol, Sort)] -> ExprV Symbol -> ExprV Symbol
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
bs) (ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e)
    go (ECoerc Sort
s1 Sort
s2 ExprV Symbol
e) = (ExprV Symbol -> ExprV Symbol)
-> (Int, ExprV Symbol) -> (Int, ExprV Symbol)
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sort -> Sort -> ExprV Symbol -> ExprV Symbol
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
s1 Sort
s2) (ExprV Symbol -> (Int, ExprV Symbol)
go ExprV Symbol
e)
    go ExprV Symbol
e                = (Int
i, ExprV Symbol
e)


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

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

instance (Defunc (c a), TaggedC c a) => Defunc (Types.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)
Types.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)
Types.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
Types.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
Types.dLits GInfo c a
fi
    BindEnv a
bs'    <- BindEnv a -> DF (BindEnv a)
forall a. Defunc a => a -> DF a
defunc (BindEnv a -> DF (BindEnv a)) -> BindEnv a -> DF (BindEnv a)
forall a b. (a -> b) -> a -> b
$ GInfo c a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
Types.bs    GInfo c a
fi
    [Triggered (ExprV Symbol)]
ass'   <- [Triggered (ExprV Symbol)] -> DF [Triggered (ExprV Symbol)]
forall a. Defunc a => a -> DF a
defunc ([Triggered (ExprV Symbol)] -> DF [Triggered (ExprV Symbol)])
-> [Triggered (ExprV Symbol)] -> DF [Triggered (ExprV Symbol)]
forall a b. (a -> b) -> a -> b
$ GInfo c a -> [Triggered (ExprV Symbol)]
forall (c :: * -> *) a. GInfo c a -> [Triggered (ExprV Symbol)]
Types.asserts GInfo c a
fi
    -- NOPROP quals' <- defunc $ quals fi
    GInfo c a -> DF (GInfo c a)
forall a. a -> StateT DFST Identity 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 { Types.cm      = cm'
                , Types.ws      = ws'
                , Types.gLits   = gLits'
                , Types.dLits   = dLits'
                , Types.bs      = bs'
                , Types.asserts = 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 ExprV Symbol
crhs' <- ExprV Symbol -> DF (ExprV Symbol)
forall a. Defunc a => a -> DF a
defunc (ExprV Symbol -> DF (ExprV Symbol))
-> ExprV Symbol -> DF (ExprV Symbol)
forall a b. (a -> b) -> a -> b
$ SimpC a -> ExprV Symbol
forall a. SimpC a -> ExprV Symbol
_crhs SimpC a
sc
                 SimpC a -> DF (SimpC a)
forall a. a -> StateT DFST Identity 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 = 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 a. a -> StateT DFST Identity 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 = (x, t', 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
    ExprV Symbol
e' <- ExprV Symbol -> DF (ExprV Symbol)
forall a. Defunc a => a -> DF a
defunc (ExprV Symbol -> DF (ExprV Symbol))
-> ExprV Symbol -> DF (ExprV Symbol)
forall a b. (a -> b) -> a -> b
$ WfC a -> ExprV Symbol
forall a. WfC a -> ExprV Symbol
wexpr WfC a
wf
    WfC a -> DF (WfC a)
forall a. a -> StateT DFST Identity 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 = (x, t', k), wexpr = 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, ExprV Symbol
e)) = (Symbol, ExprV Symbol) -> Reft
forall v. (Symbol, ExprV v) -> ReftV v
Reft ((Symbol, ExprV Symbol) -> Reft)
-> (ExprV Symbol -> (Symbol, ExprV Symbol)) -> ExprV Symbol -> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x,) (ExprV Symbol -> Reft)
-> DF (ExprV Symbol) -> StateT DFST Identity Reft
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExprV Symbol -> DF (ExprV Symbol)
forall a. Defunc a => a -> DF a
defunc ExprV Symbol
e

instance Defunc Expr where
  defunc :: ExprV Symbol -> DF (ExprV Symbol)
defunc = ExprV Symbol -> DF (ExprV Symbol)
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 a) where
  defunc :: BindEnv a -> DF (BindEnv a)
defunc BindEnv a
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 a -> DF (BindEnv a)
forall (m :: * -> *) a.
Monad m =>
((Int, (Symbol, SortedReft)) -> m (Int, (Symbol, SortedReft)))
-> BindEnv a -> m (BindEnv a)
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 a
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 a. a -> StateT DFST Identity a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 -> [ExprV Symbol]
dfLams  :: ![Expr]      -- ^ lambda expressions appearing in the expressions
  , DFST -> [ExprV Symbol]
dfRedex :: ![Expr]      -- ^ redexes appearing in the expressions
  , DFST -> SEnv Sort
dfBinds :: !(SEnv Sort) -- ^ sorts of new lambda-binders
  } deriving Int -> DFST -> ShowS
[DFST] -> ShowS
DFST -> String
(Int -> DFST -> ShowS)
-> (DFST -> String) -> ([DFST] -> ShowS) -> Show DFST
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DFST -> ShowS
showsPrec :: Int -> DFST -> ShowS
$cshow :: DFST -> String
show :: DFST -> String
$cshowList :: [DFST] -> ShowS
showList :: [DFST] -> ShowS
Show

makeDFState :: Config -> SymEnv -> IBindEnv -> DFST
makeDFState :: Config -> SymEnv -> IBindEnv -> DFST
makeDFState Config
cfg SymEnv
env IBindEnv
ibind = 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: lambdas and redexes are not defunctionalized
  , dfLams :: [ExprV Symbol]
dfLams  = []
  , dfRedex :: [ExprV Symbol]
dfRedex = []
  , dfBinds :: SEnv Sort
dfBinds = SEnv Sort
forall a. Monoid a => a
mempty
  }

makeInitDFState :: Config -> SInfo a -> DFST
makeInitDFState :: forall a. 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)
Types.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)
Types.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 = n + 1, dfBinds = insertSEnv x t (dfBinds s)}
  Symbol -> StateT DFST Identity Symbol
forall a. a -> StateT DFST Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Symbol
x