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

{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# LANGUAGE MultiParamTypeClasses #-}

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

import           Control.Monad.State
import qualified Data.HashMap.Strict       as M
import           Data.Maybe  (fromMaybe)
import           Data.List (foldl')

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 = 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 = forall s a. State s a -> s -> a
evalState (forall a. SInfo a -> Ex a (SInfo a)
ext SInfo a
si) forall a b. (a -> b) -> a -> b
$ forall ann. SymEnv -> [DataDecl] -> ExSt ann
initST (forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si) (forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls SInfo a
si)
  where
    ext ::SInfo a -> Ex a (SInfo a)
    ext :: forall a. SInfo a -> Ex a (SInfo a)
ext = 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
    forall a. BindEnv a -> Ex a ()
setBEnv (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
si)
    HashMap SubcId (SimpC a)
cm'      <- forall ann a. Extend ann a => a -> Ex ann a
extend (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
si)
    BindEnv a
bs'      <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a. ExSt a -> BindEnv a
exbenv
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SInfo a
si{ cm :: HashMap SubcId (SimpC a)
cm = HashMap SubcId (SimpC a)
cm' , bs :: BindEnv a
bs = BindEnv a
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 = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall ann a. Extend ann a => a -> Ex ann a
extend (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) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ann a. Extend ann a => a -> Ex ann a
extend a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f 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 = 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
    forall a. IBindEnv -> Ex a ()
setExBinds (forall a. SimpC a -> IBindEnv
_cenv SimpC a
c)
    Expr
rhs <- forall a. a -> Pos -> Expr -> Ex a Expr
extendExpr (forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SimpC a
c) Pos
Pos (forall a. SimpC a -> Expr
_crhs SimpC a
c)
    IBindEnv
is  <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a. ExSt a -> IBindEnv
exbinds
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SimpC a
c{_crhs :: Expr
_crhs = Expr
rhs, _cenv :: IBindEnv
_cenv = IBindEnv
is }


extendExpr :: a -> Pos -> Expr -> Ex a Expr
extendExpr :: forall a. a -> Pos -> Expr -> Ex a Expr
extendExpr a
ann Pos
p Expr
e
  | Pos
p forall a. Eq a => a -> a -> Bool
== Pos
Pos
  = 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' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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
  = 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' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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
e
      goP :: Pos -> Expr -> StateT (ExSt a) Identity Expr
goP Pos
Pos (PAtom Brel
b Expr
e1 Expr
e2)
       | Brel
b forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
b forall a. Eq a => a -> a -> Bool
== Brel
Ne
       , Just Sort
s <- Sort -> Maybe Sort
getArg (String -> Expr -> Sort
exprSort String
"extensionality" Expr
e1)
       = forall a. PPrint a => String -> a -> a
mytracepp (String
"extending POS = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
e) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. a -> Brel -> Expr -> Expr -> Sort -> Ex a Expr
extendRHS a
ann Brel
b Expr
e1 Expr
e2 Sort
s 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 = 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 forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
b forall a. Eq a => a -> a -> Bool
== Brel
Ne
       , Just Sort
s <- Sort -> Maybe Sort
getArg (String -> Expr -> Sort
exprSort String
"extensionality" Expr
e1)
       = forall a. PPrint a => String -> a -> a
mytracepp (String
"extending NEG = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
e) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. a -> Brel -> Expr -> Expr -> Sort -> Ex a Expr
extendLHS a
ann Brel
b Expr
e1 Expr
e2 Sort
s 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 = 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]
_) -> forall a. a -> Maybe a
Just Sort
a
             Maybe (Int, [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 <- forall a. a -> Sort -> Ex a [Expr]
generateArguments a
ann Sort
s
     forall a. PPrint a => String -> a -> a
mytracepp String
"extendRHS = " forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
pAnd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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  <- forall a. a -> Sort -> Ex a [Expr]
generateArguments a
ann Sort
s
     [DataDecl]
dds <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a. ExSt a -> [DataDecl]
exddecl
     [Expr]
is  <- forall a. a -> [DataDecl] -> Sort -> Ex a [Expr]
instantiate a
ann [DataDecl]
dds Sort
s
     forall a. PPrint a => String -> a -> a
mytracepp String
"extendLHS = " forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
pAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Brel -> Expr -> Expr -> Expr
PAtom Brel
b Expr
e1 Expr
e2forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall ann. Brel -> Expr -> Expr -> Expr -> Ex ann Expr
makeEq Brel
b Expr
e1 Expr
e2) ([Expr]
es 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
s = do
  [DataDecl]
ddecls   <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a. ExSt a -> [DataDecl]
exddecl
  case [DataDecl] -> Sort -> Either [(LocSymbol, [Sort])] Sort
breakSort [DataDecl]
ddecls Sort
s of
    Left [(LocSymbol, [Sort])]
dds -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a. a -> (LocSymbol, [Sort]) -> Ex a Expr
freshArgDD a
ann) [(LocSymbol, [Sort])]
dds
    Right Sort
s  -> (\Symbol
x -> [Symbol -> Expr
EVar Symbol
x]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a. ExSt a -> SymEnv
exenv
  let elab :: Expr -> Expr
elab = forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (forall a. a -> Located a
dummyLoc String
"extensionality") SymEnv
env
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Brel -> Expr -> Expr -> Expr
PAtom Brel
b (Expr -> Expr
elab forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
EApp (Expr -> Expr
unElab Expr
e1) Expr
e)  (Expr -> Expr
elab forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
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 = 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
EVar Symbol
x]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ann. ann -> Sort -> Ex ann Symbol
freshArgOne a
ann Sort
s
instantiateOne a
_ (Right Sort
s) = do
  [(Symbol, Sort)]
xss <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a. ExSt a -> [(Symbol, Sort)]
excbs
  forall (m :: * -> *) a. Monad m => a -> m a
return [Symbol -> Expr
EVar Symbol
x | (Symbol
x,Sort
xs) <- [(Symbol, Sort)]
xss, Sort
xs forall a. Eq a => a -> a -> Bool
== Sort
s ]
instantiateOne a
ann (Left [(LocSymbol
dc, [Sort]
ts)]) =
  forall a b. (a -> b) -> [a] -> [b]
map (LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
dc) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [[a]] -> [[a]]
combine forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a. a -> Either [(LocSymbol, [Sort])] Sort -> Ex a [Expr]
instantiateOne a
ann) (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts)
instantiateOne a
_ Either [(LocSymbol, [Sort])] Sort
_ = forall a. HasCallStack => a
undefined

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


data Pos = Pos | Neg deriving Pos -> Pos -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pos -> Pos -> Bool
$c/= :: Pos -> Pos -> Bool
== :: Pos -> Pos -> Bool
$c== :: 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
p Pos -> Expr -> m Expr
f = Pos -> Expr -> m Expr
go Pos
p
  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
_ Subst
_)   = Pos -> Expr -> m Expr
f Pos
p Expr
e
    go Pos
p (ENeg Expr
e)        = Pos -> Expr -> m Expr
f Pos
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
ENeg 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Sort -> Expr
`ECst` Sort
t) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Sort -> Expr -> Expr
ECoerc Sort
a Sort
t 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
EApp        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go Pos
p Expr
g  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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Bop -> Expr -> Expr -> Expr
EBin Bop
o      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go Pos
p Expr
e1 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Brel -> Expr -> Expr -> Expr
PAtom Brel
r     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go Pos
p Expr
e1 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
PImp        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go (Pos -> Pos
negatePos Pos
p) Expr
p1 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
PAnd forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Pos -> Expr -> m Expr
go Pos
p forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [Expr]
ps)

    -- The below cannot appear due to normalization
    go Pos
p (PNot Expr
e)        = Pos -> Expr -> m Expr
f Pos
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
PNot 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr
PIff        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go Pos
p Expr
p1 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr -> Expr -> Expr
EIte        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go Pos
p Expr
e  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pos -> Expr -> m Expr
go Pos
p Expr
e1 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
POr forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Pos -> Expr -> m Expr
go Pos
p forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> Expr -> Expr
PAll   [(Symbol, Sort)]
xts 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x,Sort
t) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, Sort)] -> Expr -> Expr
PExist [(Symbol, Sort)]
xts 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Sort -> Expr
`ETApp` Sort
s) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Symbol -> Expr
`ETAbs` Symbol
s) 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 Subst
s GradInfo
i Expr
e) = Pos -> Expr -> m Expr
f Pos
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
s GradInfo
i 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
e = forall a. PPrint a => String -> a -> a
mytracepp (String
"normalize: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp Expr
e) forall a b. (a -> b) -> a -> b
$ Expr -> Expr
go Expr
e
  where
    go :: Expr -> Expr
go e :: Expr
e@(ESym SymConst
_)        = Expr
e
    go e :: Expr
e@(ECon Constant
_)        = Expr
e
    go e :: Expr
e@(EVar Symbol
_)        = Expr
e
    go e :: Expr
e@(PKVar KVar
_ Subst
_)     = Expr
e
    go e :: Expr
e@(ENeg Expr
_)        = Expr
e
    go (PNot Expr
e)          = Expr -> Expr -> Expr
PImp Expr
e Expr
PFalse
    go e :: Expr
e@(ECst Expr
_ Sort
_)      = Expr
e
    go e :: Expr
e@ECoerc{}        = Expr
e
    go e :: Expr
e@(EApp Expr
_ Expr
_)      = Expr
e
    go e :: Expr
e@EBin{}          = Expr
e
    go (PImp Expr
p1 Expr
p2)      = Expr -> Expr -> Expr
PImp (Expr -> Expr
go Expr
p1) (Expr -> Expr
go Expr
p2)
    go (PIff Expr
p1 Expr
p2)      = [Expr] -> Expr
PAnd [Expr -> Expr -> Expr
PImp Expr
p1' Expr
p2', Expr -> Expr -> Expr
PImp Expr
p2' Expr
p1'] where (Expr
p1', Expr
p2') = (Expr -> Expr
go Expr
p1, Expr -> Expr
go Expr
p2)
    go e :: Expr
e@PAtom{}         = Expr
e
    go (EIte Expr
e Expr
e1 Expr
e2)    = Expr -> Expr
go forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
PAnd [Expr -> Expr -> Expr
PImp Expr
e Expr
e1, Expr -> Expr -> Expr
PImp (Expr -> Expr
PNot Expr
e) Expr
e2]
    go (PAnd [Expr]
ps)         = [Expr] -> Expr
pAnd (Expr -> Expr
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
ps)
    go (POr  [Expr]
ps)         = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Expr
x Expr
y -> Expr -> Expr -> Expr
PImp (Expr -> Expr -> Expr
PImp (Expr -> Expr
go Expr
x) Expr
PFalse) Expr
y) Expr
PFalse [Expr]
ps
    go e :: Expr
e@(PAll [(Symbol, Sort)]
_ Expr
_)      = Expr
e -- Cannot appear
    go e :: Expr
e@(ELam (Symbol, Sort)
_ Expr
_)      = Expr
e -- Cannot appear
    go e :: Expr
e@(PExist [(Symbol, Sort)]
_ Expr
_)    = Expr
e -- Cannot appear
    go e :: Expr
e@(ETApp Expr
_ Sort
_)     = Expr
e -- Cannot appear
    go e :: Expr
e@(ETAbs Expr
_ Symbol
_)     = Expr
e -- Cannot appear
    go e :: Expr
e@PGrad{}         = Expr
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)]
  }

initST :: SymEnv -> [DataDecl]  -> ExSt ann
initST :: forall ann. SymEnv -> [DataDecl] -> ExSt ann
initST SymEnv
env [DataDecl]
dd = forall a.
Int
-> [DataDecl]
-> SymEnv
-> BindEnv a
-> IBindEnv
-> [(Symbol, Sort)]
-> ExSt a
ExSt Int
0 (DataDecl
dforall a. a -> [a] -> [a]
:[DataDecl]
dd) SymEnv
env forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
  where
    -- NV: hardcore Haskell pairs because they do not appear in DataDecl (why?)
    d :: DataDecl
d = forall a. PPrint a => String -> a -> a
mytracepp String
"Tuple DataDecl" forall a b. (a -> b) -> a -> b
$ FTycon -> Int -> [DataCtor] -> DataDecl
DDecl (LocSymbol -> FTycon
symbolFTycon (forall a. a -> Located a
dummyLoc Symbol
tupConName)) Int
2 [DataCtor
ct]
    ct :: DataCtor
ct = LocSymbol -> [DataField] -> DataCtor
DCtor (forall a. a -> Located a
dummyLoc (forall a. Symbolic a => a -> Symbol
symbol String
"GHC.Tuple.(,)")) [
            LocSymbol -> Sort -> DataField
DField (forall a. a -> Located a
dummyLoc (forall a. Symbolic a => a -> Symbol
symbol String
"lqdc$select$GHC.Tuple.(,)$1")) (Int -> Sort
FVar Int
0)
          , LocSymbol -> Sort -> DataField
DField (forall a. a -> Located a
dummyLoc (forall a. Symbolic a => a -> Symbol
symbol String
"lqdc$select$GHC.Tuple.(,)$2")) (Int -> Sort
FVar Int
1)
          ]


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

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


freshArgDD :: a -> (LocSymbol, [Sort]) -> Ex a Expr
freshArgDD :: forall a. a -> (LocSymbol, [Sort]) -> Ex a Expr
freshArgDD a
ann (LocSymbol
dc, [Sort]
xs) = do
  [Symbol]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall ann. ann -> Sort -> Ex ann Symbol
freshArgOne a
ann) [Sort]
xs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
dc (Symbol -> Expr
EVar 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
st   <- forall s (m :: * -> *). MonadState s m => m s
get
  let x :: Symbol
x = forall a. Symbolic a => a -> Symbol
symbol (String
"ext$" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. ExSt a -> Int
unique ExSt ann
st))
  let (Int
id, BindEnv ann
benv') = forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
insertBindEnv Symbol
x (Sort -> SortedReft
trueSortedReft Sort
s) ann
ann (forall a. ExSt a -> BindEnv a
exbenv ExSt ann
st)
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ExSt ann
st -> ExSt ann
st{ exenv :: SymEnv
exenv   = Symbol -> Sort -> SymEnv -> SymEnv
insertSymEnv Symbol
x Sort
s (forall a. ExSt a -> SymEnv
exenv ExSt ann
st)
                   , exbenv :: BindEnv ann
exbenv  = BindEnv ann
benv'
                   , exbinds :: IBindEnv
exbinds = [Int] -> IBindEnv -> IBindEnv
insertsIBindEnv [Int
id] (forall a. ExSt a -> IBindEnv
exbinds ExSt ann
st)
                   , unique :: Int
unique   = Int
1 forall a. Num a => a -> a -> a
+ forall a. ExSt a -> Int
unique ExSt ann
st
                   , excbs :: [(Symbol, Sort)]
excbs = (Symbol
x,Sort
s) forall a. a -> [a] -> [a]
: forall a. ExSt a -> [(Symbol, Sort)]
excbs ExSt ann
st
                   })
  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]
ddecls 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]
ddecls, DataDecl -> FTycon
ddTyCon DataDecl
dd forall a. Eq a => a -> a -> Bool
== FTycon
tc ]
    = forall a b. a -> Either a b
Left ((\DataCtor
dd -> (DataCtor -> LocSymbol
dcName DataCtor
dd, Sub -> Sort -> Sort
instSort  ([(Int, Sort)] -> Sub
Sub forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..(Int
iforall a. Num a => a -> a -> a
-Int
1)] [Sort]
ts) forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataField -> Sort
dfSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtor -> [DataField]
dcFields DataCtor
dd)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCtor]
dds)
    | Bool
otherwise
    = 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) = forall a. a -> Maybe a -> a
fromMaybe (Int -> Sort
FVar Int
i) forall a b. (a -> b) -> a -> b
$ 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
     = forall a. a -> Maybe a
Just (FTycon
f, [Sort]
ts)
     | Bool
otherwise
     = 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
s2forall a. a -> [a] -> [a]
:[Sort]
acc) Sort
s1
          go [Sort]
acc Sort
s            = (Sort
s, [Sort]
acc)