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

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

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

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

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

expand :: Config -> SInfo a -> SInfo a
expand :: Config -> SInfo a -> SInfo a
expand Config
cfg SInfo a
si = State ExSt (SInfo a) -> ExSt -> SInfo a
forall s a. State s a -> s -> a
evalState (SInfo a -> State ExSt (SInfo a)
forall a. Extend a => a -> Ex a
extend SInfo a
si) (ExSt -> SInfo a) -> ExSt -> SInfo a
forall a b. (a -> b) -> a -> b
$ SymEnv -> [DataDecl] -> ExSt
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)


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


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

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

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

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

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


extendExpr :: Pos -> Expr -> Ex Expr 
extendExpr :: Pos -> Expr -> Ex Expr
extendExpr Pos
p Expr
e 
  | Pos
p Pos -> Pos -> Bool
forall a. Eq a => a -> a -> Bool
== Pos
Pos 
  = Pos -> (Pos -> Expr -> Ex Expr) -> Expr -> Ex Expr
forall (m :: * -> *).
Monad m =>
Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr
mapMPosExpr Pos
Pos Pos -> Expr -> Ex Expr
goP Expr
e' Ex Expr -> (Expr -> Ex Expr) -> Ex Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Pos -> (Pos -> Expr -> Ex Expr) -> Expr -> Ex Expr
forall (m :: * -> *).
Monad m =>
Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr
mapMPosExpr Pos
Pos Pos -> Expr -> Ex Expr
goN 
  | Bool
otherwise
  = Pos -> (Pos -> Expr -> Ex Expr) -> Expr -> Ex Expr
forall (m :: * -> *).
Monad m =>
Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr
mapMPosExpr Pos
Neg Pos -> Expr -> Ex Expr
goP Expr
e' Ex Expr -> (Expr -> Ex Expr) -> Ex Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Pos -> (Pos -> Expr -> Ex Expr) -> Expr -> Ex Expr
forall (m :: * -> *).
Monad m =>
Pos -> (Pos -> Expr -> m Expr) -> Expr -> m Expr
mapMPosExpr Pos
Neg Pos -> Expr -> Ex Expr
goN 
    where  
      e' :: Expr
e' = Expr -> Expr
normalize Expr
e
      goP :: Pos -> Expr -> Ex 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
e) (Expr -> Expr) -> Ex Expr -> Ex Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Brel -> Expr -> Expr -> Sort -> Ex Expr
extendRHS Brel
b Expr
e1 Expr
e2 Sort
s Ex Expr -> (Expr -> Ex Expr) -> Ex Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Pos -> Expr -> Ex Expr
goP Pos
Pos) 
      goP Pos
_ Expr
e = Expr -> Ex Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e 
      goN :: Pos -> Expr -> Ex 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
e) (Expr -> Expr) -> Ex Expr -> Ex Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Brel -> Expr -> Expr -> Sort -> Ex Expr
extendLHS Brel
b Expr
e1 Expr
e2 Sort
s Ex Expr -> (Expr -> Ex Expr) -> Ex Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Pos -> Expr -> Ex Expr
goN Pos
Neg) 
      goN Pos
_ Expr
e = Expr -> Ex Expr
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 :: Brel -> Expr -> Expr -> Sort -> Ex Expr
extendRHS :: Brel -> Expr -> Expr -> Sort -> Ex Expr
extendRHS Brel
b Expr
e1 Expr
e2 Sort
s = 
  do [Expr]
es <- Sort -> Ex [Expr]
generateArguments 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
pAnd) ([Expr] -> Expr) -> Ex [Expr] -> Ex Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> Ex Expr) -> [Expr] -> Ex [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Brel -> Expr -> Expr -> Expr -> Ex Expr
makeEq Brel
b Expr
e1 Expr
e2) [Expr]
es

extendLHS :: Brel -> Expr -> Expr -> Sort -> Ex Expr
extendLHS Brel
b Expr
e1 Expr
e2 Sort
s = 
  do [Expr]
es  <- Sort -> Ex [Expr]
generateArguments Sort
s 
     [DataDecl]
dds <- ExSt -> [DataDecl]
exddecl (ExSt -> [DataDecl])
-> StateT ExSt Identity ExSt -> StateT ExSt Identity [DataDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ExSt Identity ExSt
forall s (m :: * -> *). MonadState s m => m s
get 
     [Expr]
is  <- [DataDecl] -> Sort -> Ex [Expr]
instantiate [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
pAnd ([Expr] -> Expr) -> ([Expr] -> [Expr]) -> [Expr] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Brel -> Expr -> Expr -> Expr
PAtom Brel
b Expr
e1 Expr
e2Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:)) ([Expr] -> Expr) -> Ex [Expr] -> Ex Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> Ex Expr) -> [Expr] -> Ex [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Brel -> Expr -> Expr -> Expr -> Ex Expr
makeEq Brel
b Expr
e1 Expr
e2) ([Expr]
es [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
is)


generateArguments :: Sort -> Ex [Expr]
generateArguments :: Sort -> Ex [Expr]
generateArguments Sort
s = do 
  ExSt
st   <- StateT ExSt Identity ExSt
forall s (m :: * -> *). MonadState s m => m s
get 
  case [DataDecl] -> Sort -> Either [(LocSymbol, [Sort])] Sort
breakSort (ExSt -> [DataDecl]
exddecl ExSt
st) Sort
s of 
    Left [(LocSymbol, [Sort])]
dds -> ((LocSymbol, [Sort]) -> Ex Expr)
-> [(LocSymbol, [Sort])] -> Ex [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (LocSymbol, [Sort]) -> Ex Expr
freshArgDD [(LocSymbol, [Sort])]
dds  
    Right Sort
s  -> (\Symbol
x -> [Symbol -> Expr
EVar Symbol
x]) (Symbol -> [Expr]) -> StateT ExSt Identity Symbol -> Ex [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> StateT ExSt Identity Symbol
freshArgOne Sort
s 

makeEq :: Brel-> Expr -> Expr -> Expr -> Ex Expr 
makeEq :: Brel -> Expr -> Expr -> Expr -> Ex Expr
makeEq Brel
b Expr
e1 Expr
e2 Expr
e = do 
  SymEnv
env <- ExSt -> SymEnv
exenv (ExSt -> SymEnv)
-> StateT ExSt Identity ExSt -> StateT ExSt Identity SymEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ExSt Identity ExSt
forall s (m :: * -> *). MonadState s m => m s
get 
  let elab :: Expr -> Expr
elab = Located String -> SymEnv -> Expr -> Expr
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (String -> Located String
forall a. a -> Located a
dummyLoc String
"extensionality") SymEnv
env
  Expr -> Ex Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Ex Expr) -> Expr -> Ex Expr
forall a b. (a -> b) -> a -> b
$ Brel -> Expr -> Expr -> Expr
PAtom Brel
b (Expr -> Expr
elab (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
EApp (Expr -> Expr
forall t. Visitable t => t -> t
unElab Expr
e1) Expr
e)  (Expr -> Expr
elab (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
EApp (Expr -> Expr
forall t. Visitable t => t -> t
unElab Expr
e2) Expr
e)

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

instantiateOne :: Either [(LocSymbol, [Sort])] Sort  -> Ex [Expr]
instantiateOne :: Either [(LocSymbol, [Sort])] Sort -> Ex [Expr]
instantiateOne (Right s :: Sort
s@(FVar Int
_)) = 
  (\Symbol
x -> [Symbol -> Expr
EVar Symbol
x]) (Symbol -> [Expr]) -> StateT ExSt Identity Symbol -> Ex [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> StateT ExSt Identity Symbol
freshArgOne Sort
s
instantiateOne (Right Sort
s) = do 
  [(Symbol, Sort)]
xss <- ExSt -> [(Symbol, Sort)]
excbs (ExSt -> [(Symbol, Sort)])
-> StateT ExSt Identity ExSt
-> StateT ExSt Identity [(Symbol, Sort)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ExSt Identity ExSt
forall s (m :: * -> *). MonadState s m => m s
get 
  [Expr] -> Ex [Expr]
forall (m :: * -> *) a. Monad m => a -> m a
return [Symbol -> Expr
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 (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 Identity [[Expr]] -> Ex [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  (Either [(LocSymbol, [Sort])] Sort -> Ex [Expr])
-> [Either [(LocSymbol, [Sort])] Sort]
-> StateT ExSt Identity [[Expr]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Either [(LocSymbol, [Sort])] Sort -> Ex [Expr]
instantiateOne (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 Either [(LocSymbol, [Sort])] Sort
_ = Ex [Expr]
forall a. HasCallStack => a
undefined 

combine :: [[a]] -> [[a]]
combine :: [[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
/= :: 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 :: 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 (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr
ENeg        (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ((Expr -> Sort -> Expr
`ECst` Sort
t)  (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Sort -> Sort -> Expr -> Expr
ECoerc Sort
a Sort
t  (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
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 (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
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 (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
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 (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
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 (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) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([Expr] -> Expr
PAnd        ([Expr] -> Expr) -> m [Expr] -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pos -> Expr -> m Expr
go Pos
p (Expr -> m Expr) -> [Expr] -> m [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
<$$> [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) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Expr -> Expr
PNot        (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
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 (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
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 (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 (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) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([Expr] -> Expr
POr         ([Expr] -> Expr) -> m [Expr] -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pos -> Expr -> m Expr
go Pos
p (Expr -> m Expr) -> [Expr] -> m [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
<$$> [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) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([(Symbol, Sort)] -> Expr -> Expr
PAll   [(Symbol, Sort)]
xts  (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ((Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x,Sort
t)  (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([(Symbol, Sort)] -> Expr -> Expr
PExist [(Symbol, Sort)]
xts  (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ((Expr -> Sort -> Expr
`ETApp` Sort
s) (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ((Expr -> Symbol -> Expr
`ETAbs` Symbol
s) (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 (Expr -> m Expr) -> m Expr -> m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k Subst
s GradInfo
i (Expr -> Expr) -> m Expr -> m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  Pos -> Expr -> m Expr
go Pos
p Expr
e                     )

normalize :: Expr -> Expr 
normalize :: Expr -> Expr
normalize Expr
e = 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
e) (Expr -> Expr) -> Expr -> Expr
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 Sort
_ Sort
_ Expr
_)  = Expr
e
    go e :: Expr
e@(EApp Expr
_ Expr
_)      = Expr
e 
    go e :: Expr
e@(EBin Bop
_ Expr
_ Expr
_)    = 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 Brel
_ Expr
_ Expr
_)   = Expr
e 
    go (EIte Expr
e Expr
e1 Expr
e2)    = Expr -> Expr
go (Expr -> Expr) -> Expr -> Expr
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 (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
ps)
    go (POr  [Expr]
ps)         = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
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 KVar
_ Subst
_ GradInfo
_ Expr
_) = Expr
e -- Cannot appear

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

initST :: SymEnv -> [DataDecl]  -> ExSt
initST :: SymEnv -> [DataDecl] -> ExSt
initST SymEnv
env [DataDecl]
dd = Int
-> [DataDecl]
-> SymEnv
-> BindEnv
-> IBindEnv
-> [(Symbol, Sort)]
-> ExSt
ExSt Int
0 (DataDecl
dDataDecl -> [DataDecl] -> [DataDecl]
forall a. a -> [a] -> [a]
:[DataDecl]
dd) SymEnv
env BindEnv
forall a. Monoid a => a
mempty IBindEnv
forall a. Monoid a => a
mempty [(Symbol, Sort)]
forall a. Monoid a => a
mempty
  where 
    -- NV: hardcore Haskell pairs because they do not appear in DataDecl (why?)
    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
tupConName)) Int
2 [DataCtor
ct]
    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.(,)")) [
            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.(,)$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.(,)$2")) (Int -> Sort
FVar Int
1)
          ]


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

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


freshArgDD :: (LocSymbol, [Sort]) -> Ex Expr 
freshArgDD :: (LocSymbol, [Sort]) -> Ex Expr
freshArgDD (LocSymbol
dc, [Sort]
xs) = do  
  [Symbol]
xs <- (Sort -> StateT ExSt Identity Symbol)
-> [Sort] -> StateT ExSt Identity [Symbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Sort -> StateT ExSt Identity Symbol
freshArgOne [Sort]
xs
  Expr -> Ex Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Ex Expr) -> Expr -> Ex Expr
forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Expr] -> Expr
mkEApp LocSymbol
dc (Symbol -> Expr
EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs)


freshArgOne :: Sort -> Ex Symbol 
freshArgOne :: Sort -> StateT ExSt Identity Symbol
freshArgOne Sort
s = do 
  ExSt
st   <- StateT ExSt Identity ExSt
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 -> Int
unique ExSt
st))
  let (Int
id, BindEnv
benv') = Symbol -> SortedReft -> BindEnv -> (Int, BindEnv)
insertBindEnv Symbol
x (Sort -> SortedReft
trueSortedReft Sort
s) (ExSt -> BindEnv
exbenv ExSt
st)
  (ExSt -> ExSt) -> Ex ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ExSt
st -> ExSt
st{ exenv :: SymEnv
exenv   = Symbol -> Sort -> SymEnv -> SymEnv
insertSymEnv Symbol
x Sort
s (ExSt -> SymEnv
exenv ExSt
st)
                   , exbenv :: BindEnv
exbenv  = BindEnv
benv'
                   , exbinds :: IBindEnv
exbinds = [Int] -> IBindEnv -> IBindEnv
insertsIBindEnv [Int
id] (ExSt -> IBindEnv
exbinds ExSt
st)
                   , unique :: Int
unique   = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (ExSt -> Int
unique ExSt
st) 
                   , excbs :: [(Symbol, Sort)]
excbs = (Symbol
x,Sort
s)(Symbol, Sort) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. a -> [a] -> [a]
:(ExSt -> [(Symbol, Sort)]
excbs ExSt
st)
                   })
  Symbol -> StateT ExSt Identity Symbol
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 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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)