{-# LANGUAGE CPP                  #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE PatternGuards        #-}
{-# LANGUAGE FlexibleContexts     #-}

{-# LANGUAGE MultiParamTypeClasses #-}

module Language.Fixpoint.Solver.Extensionality (expand) where

import           Control.Monad.State
import qualified Data.HashMap.Strict       as M
import           Data.Maybe  (fromMaybe)
#if !MIN_VERSION_base(4,20,0)
import           Data.List (foldl')
#endif

import           Language.Fixpoint.Types.Config
import           Language.Fixpoint.SortCheck
import           Language.Fixpoint.Solver.Sanitize (symbolEnv)
import           Language.Fixpoint.Types hiding (mapSort, Pos)
import           Language.Fixpoint.Types.Visitor (mapSort)

mytracepp :: (PPrint a) => String -> a -> a
mytracepp :: forall a. PPrint a => String -> a -> a
mytracepp = String -> a -> a
forall a. PPrint a => String -> a -> a
notracepp

expand :: Config -> SInfo a -> SInfo a
expand :: forall a. Config -> SInfo a -> SInfo a
expand Config
cfg SInfo a
si = State (ExSt a) (SInfo a) -> ExSt a -> SInfo a
forall s a. State s a -> s -> a
evalState (SInfo a -> State (ExSt a) (SInfo a)
forall a. SInfo a -> Ex a (SInfo a)
ext SInfo a
si) (ExSt a -> SInfo a) -> ExSt a -> SInfo a
forall a b. (a -> b) -> a -> b
$ SymEnv -> [DataDecl] -> ElabFlags -> ExSt a
forall ann. SymEnv -> [DataDecl] -> ElabFlags -> ExSt ann
initST (Config -> SInfo a -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si) (SInfo a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls SInfo a
si) (SMTSolver -> ElabFlags
solverFlags (SMTSolver -> ElabFlags) -> SMTSolver -> ElabFlags
forall a b. (a -> b) -> a -> b
$ Config -> SMTSolver
solver Config
cfg)
  where
    ext :: SInfo a -> Ex a (SInfo a)
    ext :: forall a. SInfo a -> Ex a (SInfo a)
ext = SInfo a -> Ex a (SInfo a)
forall ann a. Extend ann a => a -> Ex ann a
extend


class Extend ann a where
  extend :: a -> Ex ann a


instance Extend a (SInfo a) where
  extend :: SInfo a -> Ex a (SInfo a)
extend SInfo a
si = do
    BindEnv a -> Ex a ()
forall a. BindEnv a -> Ex a ()
setBEnv (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
si)
    HashMap SubcId (SimpC a)
cm'      <- HashMap SubcId (SimpC a) -> Ex a (HashMap SubcId (SimpC a))
forall ann a. Extend ann a => a -> Ex ann a
extend (SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
si)
    BindEnv a
bs'      <- (ExSt a -> BindEnv a) -> StateT (ExSt a) Identity (BindEnv a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt a -> BindEnv a
forall a. ExSt a -> BindEnv a
exbenv
    SInfo a -> Ex a (SInfo a)
forall a. a -> StateT (ExSt a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SInfo a -> Ex a (SInfo a)) -> SInfo a -> Ex a (SInfo a)
forall a b. (a -> b) -> a -> b
$ SInfo a
si{ cm = cm' , bs = bs' }

instance (Extend ann a) => Extend ann (M.HashMap SubcId a) where
  extend :: HashMap SubcId a -> Ex ann (HashMap SubcId a)
extend HashMap SubcId a
h  = [(SubcId, a)] -> HashMap SubcId a
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(SubcId, a)] -> HashMap SubcId a)
-> StateT (ExSt ann) Identity [(SubcId, a)]
-> Ex ann (HashMap SubcId a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((SubcId, a) -> StateT (ExSt ann) Identity (SubcId, a))
-> [(SubcId, a)] -> StateT (ExSt ann) Identity [(SubcId, 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 (SubcId, a) -> StateT (ExSt ann) Identity (SubcId, a)
forall ann a. Extend ann a => a -> Ex ann a
extend (HashMap SubcId a -> [(SubcId, a)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SubcId a
h)

instance (Extend ann a, Extend ann b) => Extend ann (a,b) where
  extend :: (a, b) -> Ex ann (a, b)
extend (a
a,b
b) = (,) (a -> b -> (a, b))
-> StateT (ExSt ann) Identity a
-> StateT (ExSt ann) Identity (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> StateT (ExSt ann) Identity a
forall ann a. Extend ann a => a -> Ex ann a
extend a
a StateT (ExSt ann) Identity (b -> (a, b))
-> StateT (ExSt ann) Identity b -> Ex ann (a, b)
forall a b.
StateT (ExSt ann) Identity (a -> b)
-> StateT (ExSt ann) Identity a -> StateT (ExSt ann) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> b -> StateT (ExSt ann) Identity b
forall ann a. Extend ann a => a -> Ex ann a
extend b
b

instance Extend ann SubcId where
  extend :: SubcId -> Ex ann SubcId
extend SubcId
i = SubcId -> Ex ann SubcId
forall a. a -> StateT (ExSt ann) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SubcId
i

instance Extend a (SimpC a) where
  extend :: SimpC a -> Ex a (SimpC a)
extend SimpC a
c = do
    IBindEnv -> Ex a ()
forall a. IBindEnv -> Ex a ()
setExBinds (SimpC a -> IBindEnv
forall a. SimpC a -> IBindEnv
_cenv SimpC a
c)
    Expr
rhs <- a -> Pos -> Expr -> Ex a Expr
forall a. a -> Pos -> Expr -> Ex a Expr
extendExpr (SimpC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SimpC a
c) Pos
Pos (SimpC a -> Expr
forall a. SimpC a -> Expr
_crhs SimpC a
c)
    IBindEnv
is  <- (ExSt a -> IBindEnv) -> StateT (ExSt a) Identity IBindEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt a -> IBindEnv
forall a. ExSt a -> IBindEnv
exbinds
    SimpC a -> Ex a (SimpC a)
forall a. a -> StateT (ExSt a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimpC a -> Ex a (SimpC a)) -> SimpC a -> Ex a (SimpC a)
forall a b. (a -> b) -> a -> b
$ SimpC a
c{_crhs = rhs, _cenv = is }


extendExpr :: a -> Pos -> Expr -> Ex a Expr
extendExpr :: forall a. a -> Pos -> Expr -> Ex a Expr
extendExpr a
ann Pos
p Expr
expr'
  | Pos
p Pos -> Pos -> Bool
forall a. Eq a => a -> a -> Bool
== Pos
Pos
  = Pos
-> (Pos -> Expr -> StateT (ExSt a) Identity Expr)
-> Expr
-> StateT (ExSt a) Identity Expr
forall (m :: * -> *).
Monad m =>
Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr
mapMPosExpr Pos
Pos Pos -> Expr -> StateT (ExSt a) Identity Expr
goP Expr
e' StateT (ExSt a) Identity Expr
-> (Expr -> StateT (ExSt a) Identity Expr)
-> StateT (ExSt a) Identity Expr
forall a b.
StateT (ExSt a) Identity a
-> (a -> StateT (ExSt a) Identity b) -> StateT (ExSt a) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Pos
-> (Pos -> Expr -> StateT (ExSt a) Identity Expr)
-> Expr
-> StateT (ExSt a) Identity Expr
forall (m :: * -> *).
Monad m =>
Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr
mapMPosExpr Pos
Pos Pos -> Expr -> StateT (ExSt a) Identity Expr
goN
  | Bool
otherwise
  = Pos
-> (Pos -> Expr -> StateT (ExSt a) Identity Expr)
-> Expr
-> StateT (ExSt a) Identity Expr
forall (m :: * -> *).
Monad m =>
Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr
mapMPosExpr Pos
Neg Pos -> Expr -> StateT (ExSt a) Identity Expr
goP Expr
e' StateT (ExSt a) Identity Expr
-> (Expr -> StateT (ExSt a) Identity Expr)
-> StateT (ExSt a) Identity Expr
forall a b.
StateT (ExSt a) Identity a
-> (a -> StateT (ExSt a) Identity b) -> StateT (ExSt a) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Pos
-> (Pos -> Expr -> StateT (ExSt a) Identity Expr)
-> Expr
-> StateT (ExSt a) Identity Expr
forall (m :: * -> *).
Monad m =>
Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr
mapMPosExpr Pos
Neg Pos -> Expr -> StateT (ExSt a) Identity Expr
goN
    where
      e' :: Expr
e' = Expr -> Expr
normalize Expr
expr'
      goP :: Pos -> Expr -> StateT (ExSt a) Identity Expr
goP Pos
Pos (PAtom Brel
b Expr
e1 Expr
e2)
       | Brel
b Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
b Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Ne
       , Just Sort
s <- Sort -> Maybe Sort
getArg (String -> Expr -> Sort
exprSort String
"extensionality" Expr
e1)
       = String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp (String
"extending POS = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
expr') (Expr -> Expr)
-> StateT (ExSt a) Identity Expr -> StateT (ExSt a) Identity Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Brel -> Expr -> Expr -> Sort -> StateT (ExSt a) Identity Expr
forall a. a -> Brel -> Expr -> Expr -> Sort -> Ex a Expr
extendRHS a
ann Brel
b Expr
e1 Expr
e2 Sort
s StateT (ExSt a) Identity Expr
-> (Expr -> StateT (ExSt a) Identity Expr)
-> StateT (ExSt a) Identity Expr
forall a b.
StateT (ExSt a) Identity a
-> (a -> StateT (ExSt a) Identity b) -> StateT (ExSt a) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Pos -> Expr -> StateT (ExSt a) Identity Expr
goP Pos
Pos)
      goP Pos
_ Expr
e = Expr -> StateT (ExSt a) Identity Expr
forall a. a -> StateT (ExSt a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
      goN :: Pos -> Expr -> StateT (ExSt a) Identity Expr
goN Pos
Neg (PAtom Brel
b Expr
e1 Expr
e2)
       | Brel
b Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
b Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Ne
       , Just Sort
s <- Sort -> Maybe Sort
getArg (String -> Expr -> Sort
exprSort String
"extensionality" Expr
e1)
       = String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp (String
"extending NEG = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
expr') (Expr -> Expr)
-> StateT (ExSt a) Identity Expr -> StateT (ExSt a) Identity Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Brel -> Expr -> Expr -> Sort -> StateT (ExSt a) Identity Expr
forall a. a -> Brel -> Expr -> Expr -> Sort -> Ex a Expr
extendLHS a
ann Brel
b Expr
e1 Expr
e2 Sort
s StateT (ExSt a) Identity Expr
-> (Expr -> StateT (ExSt a) Identity Expr)
-> StateT (ExSt a) Identity Expr
forall a b.
StateT (ExSt a) Identity a
-> (a -> StateT (ExSt a) Identity b) -> StateT (ExSt a) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Pos -> Expr -> StateT (ExSt a) Identity Expr
goN Pos
Neg)
      goN Pos
_ Expr
e = Expr -> StateT (ExSt a) Identity Expr
forall a. a -> StateT (ExSt a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

getArg :: Sort -> Maybe Sort
getArg :: Sort -> Maybe Sort
getArg Sort
s = case Sort -> Maybe (Int, [Sort])
bkFFunc Sort
s of
             Just (Int
_, Sort
a:Sort
_:[Sort]
_) -> Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
a
             Maybe (Int, [Sort])
_                -> Maybe Sort
forall a. Maybe a
Nothing

extendRHS, extendLHS :: a -> Brel -> Expr -> Expr -> Sort -> Ex a Expr
extendRHS :: forall a. a -> Brel -> Expr -> Expr -> Sort -> Ex a Expr
extendRHS a
ann Brel
b Expr
e1 Expr
e2 Sort
s =
  do [Expr]
es <- a -> Sort -> Ex a [Expr]
forall a. a -> Sort -> Ex a [Expr]
generateArguments a
ann Sort
s
     String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp String
"extendRHS = " (Expr -> Expr) -> ([Expr] -> Expr) -> [Expr] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd ([Expr] -> Expr) -> Ex a [Expr] -> Ex a Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> Ex a Expr) -> [Expr] -> Ex a [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 (Brel -> Expr -> Expr -> Expr -> Ex a Expr
forall ann. Brel -> Expr -> Expr -> Expr -> Ex ann Expr
makeEq Brel
b Expr
e1 Expr
e2) [Expr]
es

extendLHS :: forall a. a -> Brel -> Expr -> Expr -> Sort -> Ex a Expr
extendLHS a
ann Brel
b Expr
e1 Expr
e2 Sort
s =
  do [Expr]
es  <- a -> Sort -> Ex a [Expr]
forall a. a -> Sort -> Ex a [Expr]
generateArguments a
ann Sort
s
     [DataDecl]
dds <- (ExSt a -> [DataDecl]) -> StateT (ExSt a) Identity [DataDecl]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt a -> [DataDecl]
forall a. ExSt a -> [DataDecl]
exddecl
     [Expr]
is  <- a -> [DataDecl] -> Sort -> Ex a [Expr]
forall a. a -> [DataDecl] -> Sort -> Ex a [Expr]
instantiate a
ann [DataDecl]
dds Sort
s
     String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp String
"extendLHS = " (Expr -> Expr) -> ([Expr] -> Expr) -> [Expr] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd ([Expr] -> Expr) -> ([Expr] -> [Expr]) -> [Expr] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
b Expr
e1 Expr
e2Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:) ([Expr] -> Expr) -> Ex a [Expr] -> Ex a Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> Ex a Expr) -> [Expr] -> Ex a [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 (Brel -> Expr -> Expr -> Expr -> Ex a Expr
forall ann. Brel -> Expr -> Expr -> Expr -> Ex ann Expr
makeEq Brel
b Expr
e1 Expr
e2) ([Expr]
es [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
is)

generateArguments :: a -> Sort -> Ex a [Expr]
generateArguments :: forall a. a -> Sort -> Ex a [Expr]
generateArguments a
ann Sort
srt = do
  [DataDecl]
ddatadecls <- (ExSt a -> [DataDecl]) -> StateT (ExSt a) Identity [DataDecl]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt a -> [DataDecl]
forall a. ExSt a -> [DataDecl]
exddecl
  case [DataDecl] -> Sort -> Either [(LocSymbol, [Sort])] Sort
breakSort [DataDecl]
ddatadecls Sort
srt of
    Left [(LocSymbol, [Sort])]
dds -> ((LocSymbol, [Sort]) -> StateT (ExSt a) Identity Expr)
-> [(LocSymbol, [Sort])] -> Ex a [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 (a -> (LocSymbol, [Sort]) -> StateT (ExSt a) Identity Expr
forall a. a -> (LocSymbol, [Sort]) -> Ex a Expr
freshArgDD a
ann) [(LocSymbol, [Sort])]
dds
    Right Sort
s  -> (\Symbol
x -> [Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
x]) (Symbol -> [Expr])
-> StateT (ExSt a) Identity Symbol -> Ex a [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Sort -> StateT (ExSt a) Identity Symbol
forall ann. ann -> Sort -> Ex ann Symbol
freshArgOne a
ann Sort
s

makeEq :: Brel -> Expr -> Expr -> Expr -> Ex ann Expr
makeEq :: forall ann. Brel -> Expr -> Expr -> Expr -> Ex ann Expr
makeEq Brel
b Expr
e1 Expr
e2 Expr
e = do
  SymEnv
env <- (ExSt ann -> SymEnv) -> StateT (ExSt ann) Identity SymEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt ann -> SymEnv
forall a. ExSt a -> SymEnv
exenv
  ElabFlags
slv <- (ExSt ann -> ElabFlags) -> StateT (ExSt ann) Identity ElabFlags
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt ann -> ElabFlags
forall a. ExSt a -> ElabFlags
elabf
  let elab :: Expr -> Expr
elab = ElabParam -> Expr -> Expr
forall a. Elaborate a => ElabParam -> a -> a
elaborate (ElabFlags -> Located String -> SymEnv -> ElabParam
ElabParam ElabFlags
slv (String -> Located String
forall a. a -> Located a
dummyLoc String
"extensionality") SymEnv
env)
  Expr -> Ex ann Expr
forall a. a -> StateT (ExSt ann) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Ex ann Expr) -> Expr -> Ex ann Expr
forall a b. (a -> b) -> a -> b
$ Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
b (Expr -> Expr
elab (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr
unElab Expr
e1) Expr
e) (Expr -> Expr
elab (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Expr -> Expr
unElab Expr
e2) Expr
e)

instantiate :: a -> [DataDecl]  -> Sort -> Ex a [Expr]
instantiate :: forall a. a -> [DataDecl] -> Sort -> Ex a [Expr]
instantiate a
ann [DataDecl]
ds Sort
s = a -> Either [(LocSymbol, [Sort])] Sort -> Ex a [Expr]
forall a. a -> Either [(LocSymbol, [Sort])] Sort -> Ex a [Expr]
instantiateOne a
ann ([DataDecl] -> Sort -> Either [(LocSymbol, [Sort])] Sort
breakSort [DataDecl]
ds Sort
s)

instantiateOne :: a -> Either [(LocSymbol, [Sort])] Sort  -> Ex a [Expr]
instantiateOne :: forall a. a -> Either [(LocSymbol, [Sort])] Sort -> Ex a [Expr]
instantiateOne a
ann (Right s :: Sort
s@(FVar Int
_)) =
  (\Symbol
x -> [Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
x]) (Symbol -> [Expr])
-> StateT (ExSt a) Identity Symbol
-> StateT (ExSt a) Identity [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Sort -> StateT (ExSt a) Identity Symbol
forall ann. ann -> Sort -> Ex ann Symbol
freshArgOne a
ann Sort
s
instantiateOne a
_ (Right Sort
s) = do
  [(Symbol, Sort)]
xss <- (ExSt a -> [(Symbol, Sort)])
-> StateT (ExSt a) Identity [(Symbol, Sort)]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ExSt a -> [(Symbol, Sort)]
forall a. ExSt a -> [(Symbol, Sort)]
excbs
  [Expr] -> StateT (ExSt a) Identity [Expr]
forall a. a -> StateT (ExSt a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return [Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
x | (Symbol
x,Sort
xs) <- [(Symbol, Sort)]
xss, Sort
xs Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
s ]
instantiateOne a
ann (Left [(LocSymbol
dc, [Sort]
ts)]) =
  ([Expr] -> Expr) -> [[Expr]] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
dc) ([[Expr]] -> [Expr])
-> ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]]
combine ([[Expr]] -> [Expr])
-> StateT (ExSt a) Identity [[Expr]]
-> StateT (ExSt a) Identity [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  (Either [(LocSymbol, [Sort])] Sort
 -> StateT (ExSt a) Identity [Expr])
-> [Either [(LocSymbol, [Sort])] Sort]
-> StateT (ExSt a) Identity [[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 (a
-> Either [(LocSymbol, [Sort])] Sort
-> StateT (ExSt a) Identity [Expr]
forall a. a -> Either [(LocSymbol, [Sort])] Sort -> Ex a [Expr]
instantiateOne a
ann) (Sort -> Either [(LocSymbol, [Sort])] Sort
forall a b. b -> Either a b
Right (Sort -> Either [(LocSymbol, [Sort])] Sort)
-> [Sort] -> [Either [(LocSymbol, [Sort])] Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts)
instantiateOne a
_ Either [(LocSymbol, [Sort])] Sort
_ = StateT (ExSt a) Identity [Expr]
forall a. HasCallStack => a
undefined

combine :: [[a]] -> [[a]]
combine :: forall a. [[a]] -> [[a]]
combine []          = [[]]
combine ([]:[[a]]
_)      = []
combine ((a
x:[a]
xs):[[a]]
ys) = ([a] -> [a]) -> [[a]] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) ([[a]] -> [[a]]
forall a. [[a]] -> [[a]]
combine [[a]]
ys) [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [[a]] -> [[a]]
forall a. [[a]] -> [[a]]
combine ([a]
xs[a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:[[a]]
ys)


data Pos = Pos | Neg deriving Pos -> Pos -> Bool
(Pos -> Pos -> Bool) -> (Pos -> Pos -> Bool) -> Eq Pos
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Pos -> Pos -> Bool
== :: Pos -> Pos -> Bool
$c/= :: Pos -> Pos -> Bool
/= :: Pos -> Pos -> Bool
Eq
negatePos :: Pos -> Pos
negatePos :: Pos -> Pos
negatePos Pos
Pos = Pos
Neg
negatePos Pos
Neg = Pos
Pos

mapMPosExpr :: (Monad m) => Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr
mapMPosExpr :: forall (m :: * -> *).
Monad m =>
Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr
mapMPosExpr Pos
pos Pos -> Expr -> m Expr
f = Pos -> Expr -> m Expr
go Pos
pos
  where
    go :: Pos -> Expr -> m Expr
go Pos
p e :: Expr
e@(ESym SymConst
_)      = Pos -> Expr -> m Expr
f Pos
p Expr
e
    go Pos
p e :: Expr
e@(ECon Constant
_)      = Pos -> Expr -> m Expr
f Pos
p Expr
e
    go Pos
p e :: Expr
e@(EVar Symbol
_)      = Pos -> Expr -> m Expr
f Pos
p Expr
e
    go Pos
p e :: Expr
e@(PKVar KVar
_ SubstV Symbol
_)   = Pos -> Expr -> m Expr
f Pos
p Expr
e
    go Pos
p (ENeg Expr
e)        = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Pos -> Expr -> m Expr
go Pos
p Expr
e
    go Pos
p (ECst Expr
e Sort
t)      = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ECst` Sort
t) (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Pos -> Expr -> m Expr
go Pos
p Expr
e
    go Pos
p (ECoerc Sort
a Sort
t Expr
e)  = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
a Sort
t (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Pos -> Expr -> m Expr
go Pos
p Expr
e
    go Pos
p (EApp Expr
g Expr
e)      = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp        (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go Pos
p Expr
g  m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pos -> Expr -> m Expr
go Pos
p Expr
e             )
    go Pos
p (EBin Bop
o Expr
e1 Expr
e2)  = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
o      (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go Pos
p Expr
e1 m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pos -> Expr -> m Expr
go Pos
p Expr
e2            )
    go Pos
p (PAtom Brel
r Expr
e1 Expr
e2) = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r     (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go Pos
p Expr
e1 m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pos -> Expr -> m Expr
go Pos
p Expr
e2            )

    go Pos
p (PImp Expr
p1 Expr
p2)    = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp        (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go (Pos -> Pos
negatePos Pos
p) Expr
p1 m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pos -> Expr -> m Expr
go Pos
p Expr
p2)
    go Pos
p (PAnd [Expr]
ps)       = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> ([Expr] -> Expr) -> [Expr] -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd ([Expr] -> m Expr) -> m [Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Pos -> Expr -> m Expr
go Pos
p (Expr -> m Expr) -> [Expr] -> m [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
`traverse` [Expr]
ps)

    -- The below cannot appear due to normalization
    go Pos
p (PNot Expr
e)        = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
forall v. ExprV v -> ExprV v
PNot (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Pos -> Expr -> m Expr
go Pos
p Expr
e
    go Pos
p (PIff Expr
p1 Expr
p2)    = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff        (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go Pos
p Expr
p1 m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pos -> Expr -> m Expr
go Pos
p Expr
p2            )
    go Pos
p (EIte Expr
e Expr
e1 Expr
e2)  = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte        (Expr -> Expr -> Expr -> Expr)
-> m Expr -> m (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go Pos
p Expr
e  m (Expr -> Expr -> Expr) -> m Expr -> m (Expr -> Expr)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pos -> Expr -> m Expr
go Pos
p Expr
e1 m (Expr -> Expr) -> m Expr -> m Expr
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pos -> Expr -> m Expr
go Pos
p Expr
e2)
    go Pos
p (POr  [Expr]
ps)       = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> ([Expr] -> Expr) -> [Expr] -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr ([Expr] -> m Expr) -> m [Expr] -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Pos -> Expr -> m Expr
go Pos
p (Expr -> m Expr) -> [Expr] -> m [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
`traverse` [Expr]
ps)

    -- The following canot appear in general
    go Pos
p (PAll [(Symbol, Sort)]
xts Expr
e)    = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PAll   [(Symbol, Sort)]
xts (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Pos -> Expr -> m Expr
go Pos
p Expr
e
    go Pos
p (ELam (Symbol
x,Sort
t) Expr
e)  = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x,Sort
t) (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Pos -> Expr -> m Expr
go Pos
p Expr
e
    go Pos
p (PExist [(Symbol, Sort)]
xts Expr
e)  = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> Expr -> Expr
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
xts (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Pos -> Expr -> m Expr
go Pos
p Expr
e
    go Pos
p (ETApp Expr
e Sort
s)     = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ETApp` Sort
s) (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Pos -> Expr -> m Expr
go Pos
p Expr
e
    go Pos
p (ETAbs Expr
e Symbol
s)     = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
`ETAbs` Symbol
s) (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Pos -> Expr -> m Expr
go Pos
p Expr
e
    go Pos
p (PGrad KVar
k SubstV Symbol
s GradInfo
i Expr
e) = Pos -> Expr -> m Expr
f Pos
p (Expr -> m Expr) -> (Expr -> Expr) -> Expr -> m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> SubstV Symbol -> GradInfo -> Expr -> Expr
forall v. KVar -> SubstV v -> GradInfo -> ExprV v -> ExprV v
PGrad KVar
k SubstV Symbol
s GradInfo
i (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Pos -> Expr -> m Expr
go Pos
p Expr
e

normalize :: Expr -> Expr
normalize :: Expr -> Expr
normalize Expr
expr' = String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp (String
"normalize: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
expr') (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall {v}. (Fixpoint v, Ord v) => ExprV v -> ExprV v
go Expr
expr'
  where
    go :: ExprV v -> ExprV v
go e :: ExprV v
e@(ESym SymConst
_)        = ExprV v
e
    go e :: ExprV v
e@(ECon Constant
_)        = ExprV v
e
    go e :: ExprV v
e@(EVar v
_)        = ExprV v
e
    go e :: ExprV v
e@(PKVar KVar
_ SubstV v
_)     = ExprV v
e
    go e :: ExprV v
e@(ENeg ExprV v
_)        = ExprV v
e
    go (PNot ExprV v
e)          = ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
PImp ExprV v
e ExprV v
forall v. ExprV v
PFalse
    go e :: ExprV v
e@(ECst ExprV v
_ Sort
_)      = ExprV v
e
    go e :: ExprV v
e@ECoerc{}        = ExprV v
e
    go e :: ExprV v
e@(EApp ExprV v
_ ExprV v
_)      = ExprV v
e
    go e :: ExprV v
e@EBin{}          = ExprV v
e
    go (PImp ExprV v
p1 ExprV v
p2)      = ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
PImp (ExprV v -> ExprV v
go ExprV v
p1) (ExprV v -> ExprV v
go ExprV v
p2)
    go (PIff ExprV v
p1 ExprV v
p2)      = [ExprV v] -> ExprV v
forall v. [ExprV v] -> ExprV v
PAnd [ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
PImp ExprV v
p1' ExprV v
p2', ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
PImp ExprV v
p2' ExprV v
p1'] where (ExprV v
p1', ExprV v
p2') = (ExprV v -> ExprV v
go ExprV v
p1, ExprV v -> ExprV v
go ExprV v
p2)
    go e :: ExprV v
e@PAtom{}         = ExprV v
e
    go (EIte ExprV v
e ExprV v
e1 ExprV v
e2)    = ExprV v -> ExprV v
go (ExprV v -> ExprV v) -> ExprV v -> ExprV v
forall a b. (a -> b) -> a -> b
$ [ExprV v] -> ExprV v
forall v. [ExprV v] -> ExprV v
PAnd [ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
PImp ExprV v
e ExprV v
e1, ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
PImp (ExprV v -> ExprV v
forall v. ExprV v -> ExprV v
PNot ExprV v
e) ExprV v
e2]
    go (PAnd [ExprV v]
ps)         = [ExprV v] -> ExprV v
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd (ExprV v -> ExprV v
go (ExprV v -> ExprV v) -> [ExprV v] -> [ExprV v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV v]
ps)
    go (POr  [ExprV v]
ps)         = (ExprV v -> ExprV v -> ExprV v) -> ExprV v -> [ExprV v] -> ExprV v
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\ExprV v
x ExprV v
y -> ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
PImp (ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v
PImp (ExprV v -> ExprV v
go ExprV v
x) ExprV v
forall v. ExprV v
PFalse) ExprV v
y) ExprV v
forall v. ExprV v
PFalse [ExprV v]
ps
    go e :: ExprV v
e@(PAll [(Symbol, Sort)]
_ ExprV v
_)      = ExprV v
e -- Cannot appear
    go e :: ExprV v
e@(ELam (Symbol, Sort)
_ ExprV v
_)      = ExprV v
e -- Cannot appear
    go e :: ExprV v
e@(PExist [(Symbol, Sort)]
_ ExprV v
_)    = ExprV v
e -- Cannot appear
    go e :: ExprV v
e@(ETApp ExprV v
_ Sort
_)     = ExprV v
e -- Cannot appear
    go e :: ExprV v
e@(ETAbs ExprV v
_ Symbol
_)     = ExprV v
e -- Cannot appear
    go e :: ExprV v
e@PGrad{}         = ExprV v
e -- Cannot appear


type Ex a = State (ExSt a)
data ExSt a = ExSt
  { forall a. ExSt a -> Int
unique  :: Int
  , forall a. ExSt a -> [DataDecl]
exddecl :: [DataDecl]
  , forall a. ExSt a -> SymEnv
exenv   :: SymEnv        -- used for elaboration
  , forall a. ExSt a -> BindEnv a
exbenv  :: BindEnv a
  , forall a. ExSt a -> IBindEnv
exbinds :: IBindEnv
  , forall a. ExSt a -> [(Symbol, Sort)]
excbs   :: [(Symbol, Sort)]
  , forall a. ExSt a -> ElabFlags
elabf   :: ElabFlags
  }

initST :: SymEnv -> [DataDecl] -> ElabFlags -> ExSt ann
initST :: forall ann. SymEnv -> [DataDecl] -> ElabFlags -> ExSt ann
initST SymEnv
env [DataDecl]
dd ElabFlags
ef = Int
-> [DataDecl]
-> SymEnv
-> BindEnv ann
-> IBindEnv
-> [(Symbol, Sort)]
-> ElabFlags
-> ExSt ann
forall a.
Int
-> [DataDecl]
-> SymEnv
-> BindEnv a
-> IBindEnv
-> [(Symbol, Sort)]
-> ElabFlags
-> ExSt a
ExSt Int
0 (DataDecl
dDataDecl -> [DataDecl] -> [DataDecl]
forall a. a -> [a] -> [a]
:[DataDecl]
dd) SymEnv
env BindEnv ann
forall a. Monoid a => a
mempty IBindEnv
forall a. Monoid a => a
mempty [(Symbol, Sort)]
forall a. Monoid a => a
mempty ElabFlags
ef
  where
    -- NV: hardcore Haskell pairs because they do not appear in DataDecl (why?)
#if MIN_TOOL_VERSION_ghc(9,10,1)
    d = mytracepp "Tuple DataDecl" $ DDecl (symbolFTycon (dummyLoc $ symbol "Tuple2")) 2 [ct]
#else
    d :: DataDecl
d = String -> DataDecl -> DataDecl
forall a. PPrint a => String -> a -> a
mytracepp String
"Tuple DataDecl" (DataDecl -> DataDecl) -> DataDecl -> DataDecl
forall a b. (a -> b) -> a -> b
$ FTycon -> Int -> [DataCtor] -> DataDecl
DDecl (LocSymbol -> FTycon
symbolFTycon (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Symbol -> LocSymbol) -> Symbol -> LocSymbol
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
"Tuple")) Int
2 [DataCtor
ct]
#endif
#if MIN_TOOL_VERSION_ghc(9,6,0) && !MIN_TOOL_VERSION_ghc(9,10,0)
    ct :: DataCtor
ct = LocSymbol -> [DataField] -> DataCtor
DCtor (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
"GHC.Tuple.Prim.(,)")) [
            LocSymbol -> Sort -> DataField
DField (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
"lqdc$select$GHC.Tuple.Prim.(,)$1")) (Int -> Sort
FVar Int
0)
          , LocSymbol -> Sort -> DataField
DField (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
"lqdc$select$GHC.Tuple.Prim.(,)$2")) (Int -> Sort
FVar Int
1)
          ]
#elif MIN_TOOL_VERSION_ghc(9,13,0)
    ct = DCtor (dummyLoc (symbol "GHC.Internal.Tuple.(,)")) [
            DField (dummyLoc (symbol "lqdc$select$GHC.Internal.Tuple.(,)$1")) (FVar 0)
          , DField (dummyLoc (symbol "lqdc$select$GHC.Internal.Tuple.(,)$2")) (FVar 1)
          ]
#else
    ct = DCtor (dummyLoc (symbol "GHC.Tuple.(,)")) [
            DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.(,)$1")) (FVar 0)
          , DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.(,)$2")) (FVar 1)
          ]
#endif

setBEnv :: BindEnv a -> Ex a ()
setBEnv :: forall a. BindEnv a -> Ex a ()
setBEnv BindEnv a
benv = (ExSt a -> ExSt a) -> StateT (ExSt a) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ExSt a
st -> ExSt a
st{exbenv = benv})

setExBinds :: IBindEnv -> Ex a ()
setExBinds :: forall a. IBindEnv -> Ex a ()
setExBinds IBindEnv
bids = (ExSt a -> ExSt a) -> StateT (ExSt a) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ExSt a
st -> ExSt a
st{ exbinds = bids
                                   , excbs   = [ (x, sr_sort r) | (i, (x, r, _)) <- bindEnvToList (exbenv st)
                                                                , memberIBindEnv i bids]})


freshArgDD :: a -> (LocSymbol, [Sort]) -> Ex a Expr
freshArgDD :: forall a. a -> (LocSymbol, [Sort]) -> Ex a Expr
freshArgDD a
ann (LocSymbol
dc, [Sort]
sorts) = do
  [Symbol]
xs <- (Sort -> StateT (ExSt a) Identity Symbol)
-> [Sort] -> StateT (ExSt a) Identity [Symbol]
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 -> Sort -> StateT (ExSt a) Identity Symbol
forall ann. ann -> Sort -> Ex ann Symbol
freshArgOne a
ann) [Sort]
sorts
  Expr -> Ex a Expr
forall a. a -> StateT (ExSt a) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Ex a Expr) -> Expr -> Ex a Expr
forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
dc (Symbol -> Expr
forall v. v -> ExprV v
EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)


freshArgOne :: ann -> Sort -> Ex ann Symbol
freshArgOne :: forall ann. ann -> Sort -> Ex ann Symbol
freshArgOne ann
ann Sort
s = do
  ExSt ann
exst <- StateT (ExSt ann) Identity (ExSt ann)
forall s (m :: * -> *). MonadState s m => m s
get
  let x :: Symbol
x = String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"ext$" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (ExSt ann -> Int
forall a. ExSt a -> Int
unique ExSt ann
exst))
  let (Int
bindId, BindEnv ann
benv') = Symbol -> SortedReft -> ann -> BindEnv ann -> (Int, BindEnv ann)
forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
insertBindEnv Symbol
x (Sort -> SortedReft
trueSortedReft Sort
s) ann
ann (ExSt ann -> BindEnv ann
forall a. ExSt a -> BindEnv a
exbenv ExSt ann
exst)
  (ExSt ann -> ExSt ann) -> StateT (ExSt ann) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ExSt ann
st -> ExSt ann
st{ exenv   = insertSymEnv x s (exenv st)
                   , exbenv  = benv'
                   , exbinds = insertsIBindEnv [bindId] (exbinds st)
                   , unique   = 1 + unique st
                   , excbs = (x,s) : excbs st
                   })
  Symbol -> Ex ann Symbol
forall a. a -> StateT (ExSt ann) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Symbol
x


breakSort :: [DataDecl] -> Sort -> Either [(LocSymbol, [Sort])] Sort
breakSort :: [DataDecl] -> Sort -> Either [(LocSymbol, [Sort])] Sort
breakSort [DataDecl]
ddatadecls Sort
s
    | Just (FTycon
tc, [Sort]
ts) <- Sort -> Maybe (FTycon, [Sort])
splitTC Sort
s
    , [([DataCtor]
dds,Int
i)] <- [ (DataDecl -> [DataCtor]
ddCtors DataDecl
dd,DataDecl -> Int
ddVars DataDecl
dd) | DataDecl
dd <- [DataDecl]
ddatadecls, DataDecl -> FTycon
ddTyCon DataDecl
dd FTycon -> FTycon -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon
tc ]
    = [(LocSymbol, [Sort])] -> Either [(LocSymbol, [Sort])] Sort
forall a b. a -> Either a b
Left ((\DataCtor
dd -> (DataCtor -> LocSymbol
dcName DataCtor
dd, Sub -> Sort -> Sort
instSort  ([(Int, Sort)] -> Sub
Sub ([(Int, Sort)] -> Sub) -> [(Int, Sort)] -> Sub
forall a b. (a -> b) -> a -> b
$ [Int] -> [Sort] -> [(Int, Sort)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..(Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] [Sort]
ts) (Sort -> Sort) -> (DataField -> Sort) -> DataField -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataField -> Sort
dfSort (DataField -> Sort) -> [DataField] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtor -> [DataField]
dcFields DataCtor
dd)) (DataCtor -> (LocSymbol, [Sort]))
-> [DataCtor] -> [(LocSymbol, [Sort])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCtor]
dds)
    | Bool
otherwise
    = Sort -> Either [(LocSymbol, [Sort])] Sort
forall a b. b -> Either a b
Right Sort
s

instSort :: Sub -> Sort -> Sort
instSort :: Sub -> Sort -> Sort
instSort (Sub [(Int, Sort)]
su) Sort
x = (Sort -> Sort) -> Sort -> Sort
mapSort Sort -> Sort
go Sort
x
  where
    go :: Sort -> Sort
    go :: Sort -> Sort
go (FVar Int
i) = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
fromMaybe (Int -> Sort
FVar Int
i) (Maybe Sort -> Sort) -> Maybe Sort -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> [(Int, Sort)] -> Maybe Sort
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
i [(Int, Sort)]
su
    go Sort
s        = Sort
s

splitTC :: Sort -> Maybe (FTycon, [Sort])
splitTC :: Sort -> Maybe (FTycon, [Sort])
splitTC Sort
s
     | (FTC FTycon
f, [Sort]
ts) <- Sort -> (Sort, [Sort])
splitFApp Sort
s
     = (FTycon, [Sort]) -> Maybe (FTycon, [Sort])
forall a. a -> Maybe a
Just (FTycon
f, [Sort]
ts)
     | Bool
otherwise
     = Maybe (FTycon, [Sort])
forall a. Maybe a
Nothing

splitFApp :: Sort -> (Sort, [Sort])
splitFApp :: Sort -> (Sort, [Sort])
splitFApp = [Sort] -> Sort -> (Sort, [Sort])
go []
    where go :: [Sort] -> Sort -> (Sort, [Sort])
go [Sort]
acc (FApp Sort
s1 Sort
s2) = [Sort] -> Sort -> (Sort, [Sort])
go (Sort
s2Sort -> [Sort] -> [Sort]
forall a. a -> [a] -> [a]
:[Sort]
acc) Sort
s1
          go [Sort]
acc Sort
s            = (Sort
s, [Sort]
acc)