-- 
-- (C) Susumu Katayama
--
module MagicHaskeller.Analytical.Syntax where

import Control.Monad -- hiding (guard)
import Data.List(nub)

import qualified MagicHaskeller.Types as T

import Data.Word

import MagicHaskeller.CoreLang(Var)

--
-- Datatypes
--

data IOPair a = IOP { IOPair a -> Int
numUniIDs :: Int  -- ^ number of variables quantified with forall
                    , IOPair a -> [Expr a]
inputs    :: [Expr a] -- ^ input example for each argument. The last argument comes first.
                    , IOPair a -> Expr a
output    :: Expr a}
             deriving (Int -> IOPair a -> ShowS
[IOPair a] -> ShowS
IOPair a -> String
(Int -> IOPair a -> ShowS)
-> (IOPair a -> String) -> ([IOPair a] -> ShowS) -> Show (IOPair a)
forall a. Show a => Int -> IOPair a -> ShowS
forall a. Show a => [IOPair a] -> ShowS
forall a. Show a => IOPair a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IOPair a] -> ShowS
$cshowList :: forall a. Show a => [IOPair a] -> ShowS
show :: IOPair a -> String
$cshow :: forall a. Show a => IOPair a -> String
showsPrec :: Int -> IOPair a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> IOPair a -> ShowS
Show,IOPair a -> IOPair a -> Bool
(IOPair a -> IOPair a -> Bool)
-> (IOPair a -> IOPair a -> Bool) -> Eq (IOPair a)
forall a. IOPair a -> IOPair a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IOPair a -> IOPair a -> Bool
$c/= :: forall a. IOPair a -> IOPair a -> Bool
== :: IOPair a -> IOPair a -> Bool
$c== :: forall a. IOPair a -> IOPair a -> Bool
Eq)
instance Functor IOPair where
  fmap :: (a -> b) -> IOPair a -> IOPair b
fmap a -> b
f IOPair a
iop = IOPair a
iop{inputs :: [Expr b]
inputs = (Expr a -> Expr b) -> [Expr a] -> [Expr b]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> b) -> Expr a -> Expr b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) ([Expr a] -> [Expr b]) -> [Expr a] -> [Expr b]
forall a b. (a -> b) -> a -> b
$ IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs IOPair a
iop, output :: Expr b
output = (a -> b) -> Expr a -> Expr b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (Expr a -> Expr b) -> Expr a -> Expr b
forall a b. (a -> b) -> a -> b
$ IOPair a -> Expr a
forall a. IOPair a -> Expr a
output IOPair a
iop}

type TBS = [Bool]                 -- ^ the to-be-sought list
data Expr a = E {Expr a -> a
ann :: a, Expr a -> Int
iD :: Int} -- ^ existential variable. When doing analytical synthesis, there is no functional variable. 
            | U {ann :: a, iD :: Int} -- ^ universal variable. When doing analytical synthesis, there is no functional variable. 
                     --   IntではなくTH.Nameを直接使った方がよい？
            | C {ann :: a, Expr a -> Int
sz :: Int, Expr a -> Typed Constr
ctor :: T.Typed Constr, Expr a -> [Expr a]
fields :: [Expr a]}
            deriving (Int -> Expr a -> ShowS
[Expr a] -> ShowS
Expr a -> String
(Int -> Expr a -> ShowS)
-> (Expr a -> String) -> ([Expr a] -> ShowS) -> Show (Expr a)
forall a. Show a => Int -> Expr a -> ShowS
forall a. Show a => [Expr a] -> ShowS
forall a. Show a => Expr a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr a] -> ShowS
$cshowList :: forall a. Show a => [Expr a] -> ShowS
show :: Expr a -> String
$cshow :: forall a. Show a => Expr a -> String
showsPrec :: Int -> Expr a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Expr a -> ShowS
Show)
instance Eq (Expr a) where   -- We just ignore the annotations and compare syntactically.
  E{iD :: forall a. Expr a -> Int
iD=Int
i} == :: Expr a -> Expr a -> Bool
== E{iD :: forall a. Expr a -> Int
iD=Int
j} = Int
iInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
j
  U{iD :: forall a. Expr a -> Int
iD=Int
i} == U{iD :: forall a. Expr a -> Int
iD=Int
j} = Int
iInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
j
  C{ctor :: forall a. Expr a -> Typed Constr
ctor=Typed Constr
c,fields :: forall a. Expr a -> [Expr a]
fields=[Expr a]
fs} == C{ctor :: forall a. Expr a -> Typed Constr
ctor=Typed Constr
d,fields :: forall a. Expr a -> [Expr a]
fields=[Expr a]
gs} = Typed Constr -> Constr
forall a. Typed a -> a
T.typee Typed Constr
c Constr -> Constr -> Bool
forall a. Eq a => a -> a -> Bool
== Typed Constr -> Constr
forall a. Typed a -> a
T.typee Typed Constr
d Bool -> Bool -> Bool
&& [Expr a]
fs [Expr a] -> [Expr a] -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr a]
gs
                                               -- We do not chech the equivalence of sizes because that would force evaluation. 
  Expr a
_ == Expr a
_ = Bool
False
instance Functor Expr where
  fmap :: (a -> b) -> Expr a -> Expr b
fmap a -> b
f (E a
a Int
i) = b -> Int -> Expr b
forall a. a -> Int -> Expr a
E (a -> b
f a
a) Int
i
  fmap a -> b
f (U a
a Int
i) = b -> Int -> Expr b
forall a. a -> Int -> Expr a
U (a -> b
f a
a) Int
i
  fmap a -> b
f Expr a
c       = Expr a
c{ann :: b
ann = a -> b
f (Expr a -> a
forall a. Expr a -> a
ann Expr a
c), fields :: [Expr b]
fields = (Expr a -> Expr b) -> [Expr a] -> [Expr b]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> b) -> Expr a -> Expr b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) ([Expr a] -> [Expr b]) -> [Expr a] -> [Expr b]
forall a b. (a -> b) -> a -> b
$ Expr a -> [Expr a]
forall a. Expr a -> [Expr a]
fields Expr a
c}

type Constr  = Var
normalizeMkIOP :: [Expr a] -> Expr a -> IOPair a
normalizeMkIOP :: [Expr a] -> Expr a -> IOPair a
normalizeMkIOP [Expr a]
ins Expr a
out = let varIDs :: [Int]
varIDs = [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Expr a -> [Int]) -> [Expr a] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr a -> [Int]
forall a. Expr a -> [Int]
vr (Expr a
out Expr a -> [Expr a] -> [Expr a]
forall a. a -> [a] -> [a]
: [Expr a]
ins)
                             tup :: [(Int, Int)]
tup    = [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
varIDs [Int
0..]
                         in (Expr a -> Expr a) -> IOPair a -> IOPair a
forall a a. (Expr a -> Expr a) -> IOPair a -> IOPair a
mapIOP ((Int -> Int) -> Expr a -> Expr a
forall a. (Int -> Int) -> Expr a -> Expr a
mapU (\Int
tv -> case Int -> [(Int, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
tv [(Int, Int)]
tup of Just Int
n  -> Int
n)) IOP :: forall a. Int -> [Expr a] -> Expr a -> IOPair a
IOP{numUniIDs :: Int
numUniIDs = [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
varIDs, inputs :: [Expr a]
inputs = [Expr a]
ins, output :: Expr a
output = Expr a
out}
vr :: Expr a -> [Int]
vr (U a
_ Int
i)      = [Int
i]
vr (C{fields :: forall a. Expr a -> [Expr a]
fields=[Expr a]
es}) = (Expr a -> [Int]) -> [Expr a] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr a -> [Int]
vr [Expr a]
es
mapU :: (Int -> Int) -> Expr a -> Expr a
mapU Int -> Int
f (U a
a Int
i) = a -> Int -> Expr a
forall a. a -> Int -> Expr a
U a
a (Int -> Expr a) -> Int -> Expr a
forall a b. (a -> b) -> a -> b
$ Int -> Int
f Int
i
mapU Int -> Int
f e :: Expr a
e@(C{fields :: forall a. Expr a -> [Expr a]
fields=[Expr a]
xs}) = Expr a
e{fields :: [Expr a]
fields=(Expr a -> Expr a) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> Expr a -> Expr a
mapU Int -> Int
f) [Expr a]
xs}

maybeCtor :: Expr a -> Maybe (T.Typed Constr)
maybeCtor :: Expr a -> Maybe (Typed Constr)
maybeCtor (C{ctor :: forall a. Expr a -> Typed Constr
ctor=Typed Constr
c}) = Typed Constr -> Maybe (Typed Constr)
forall a. a -> Maybe a
Just Typed Constr
c
maybeCtor Expr a
_           = Maybe (Typed Constr)
forall a. Maybe a
Nothing

hasExistential :: Expr a -> Bool
hasExistential (E{}) = Bool
True
hasExistential (U{}) = Bool
False
hasExistential (C{fields :: forall a. Expr a -> [Expr a]
fields=[Expr a]
es}) = (Expr a -> Bool) -> [Expr a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr a -> Bool
hasExistential [Expr a]
es

visibles :: [Bool] -> [a] -> [a]
visibles [Bool]
tbs [a]
ins = [ a
i | (Bool
True,a
i) <- [Bool] -> [a] -> [(Bool, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Bool]
tbs [a]
ins ]

--
-- unification
--

type Subst a = [(Int, Expr a)]


unify :: Expr a -> Expr a -> m [(Int, Expr a)]
unify (C a
_ Int
_ Typed Constr
i [Expr a]
xs) (C a
_ Int
_ Typed Constr
j [Expr a]
ys) | Typed Constr -> Constr
forall a. Typed a -> a
T.typee Typed Constr
i Constr -> Constr -> Bool
forall a. Eq a => a -> a -> Bool
== Typed Constr -> Constr
forall a. Typed a -> a
T.typee Typed Constr
j = [Expr a] -> [Expr a] -> m [(Int, Expr a)]
unifyList [Expr a]
xs [Expr a]
ys
                                | Bool
otherwise = m [(Int, Expr a)]
forall (m :: * -> *) a. MonadPlus m => m a
mzero
unify Expr a
e          Expr a
f          | Expr a
eExpr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
==Expr a
f      = [(Int, Expr a)] -> m [(Int, Expr a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
unify (E a
_ Int
i)    Expr a
e          = Int -> Expr a -> m [(Int, Expr a)]
forall (m :: * -> *) a.
MonadPlus m =>
Int -> Expr a -> m [(Int, Expr a)]
bind Int
i Expr a
e
unify Expr a
e          (E a
_ Int
i)    = Int -> Expr a -> m [(Int, Expr a)]
forall (m :: * -> *) a.
MonadPlus m =>
Int -> Expr a -> m [(Int, Expr a)]
bind Int
i Expr a
e
unify Expr a
_        Expr a
_        = m [(Int, Expr a)]
forall (m :: * -> *) a. MonadPlus m => m a
mzero

unifyList :: [Expr a] -> [Expr a] -> m [(Int, Expr a)]
unifyList []     []     = [(Int, Expr a)] -> m [(Int, Expr a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
unifyList (Expr a
x:[Expr a]
xs) (Expr a
y:[Expr a]
ys) = do [(Int, Expr a)]
s1 <- Expr a -> Expr a -> m [(Int, Expr a)]
unify Expr a
x Expr a
y
                             [(Int, Expr a)]
s2 <- [Expr a] -> [Expr a] -> m [(Int, Expr a)]
unifyList ((Expr a -> Expr a) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map ([(Int, Expr a)] -> Expr a -> Expr a
forall a. [(Int, Expr a)] -> Expr a -> Expr a
apply [(Int, Expr a)]
s1) [Expr a]
xs) ((Expr a -> Expr a) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map ([(Int, Expr a)] -> Expr a -> Expr a
forall a. [(Int, Expr a)] -> Expr a -> Expr a
apply [(Int, Expr a)]
s1) [Expr a]
ys)
                             [(Int, Expr a)] -> m [(Int, Expr a)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, Expr a)] -> m [(Int, Expr a)])
-> [(Int, Expr a)] -> m [(Int, Expr a)]
forall a b. (a -> b) -> a -> b
$ [(Int, Expr a)]
s2 [(Int, Expr a)] -> [(Int, Expr a)] -> [(Int, Expr a)]
forall a. Subst a -> Subst a -> Subst a
`plusSubst` [(Int, Expr a)]
s1
unifyList [Expr a]
_      [Expr a]
_      = String -> m [(Int, Expr a)]
forall a. HasCallStack => String -> a
error String
"Partial application to a constructor." -- Can this happen?

bind :: Int -> Expr a -> m [(Int, Expr a)]
bind Int
i Expr a
e | Int
i Int -> Expr a -> Bool
forall a. Int -> Expr a -> Bool
`occursIn` Expr a
e = m [(Int, Expr a)]
forall (m :: * -> *) a. MonadPlus m => m a
mzero           -- I think permitting infinite data would break the unification algorithm.
         | Bool
otherwise      = [(Int, Expr a)] -> m [(Int, Expr a)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int
i,Expr a
e)]

-- | 'apply' applies a substitution which replaces existential variables to an expression.
apply :: [(Int, Expr a)] -> Expr a -> Expr a
apply [(Int, Expr a)]
subst v :: Expr a
v@(E a
_ Int
i)  = Expr a -> (Expr a -> Expr a) -> Maybe (Expr a) -> Expr a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr a
v Expr a -> Expr a
forall a. a -> a
id (Maybe (Expr a) -> Expr a) -> Maybe (Expr a) -> Expr a
forall a b. (a -> b) -> a -> b
$ Int -> [(Int, Expr a)] -> Maybe (Expr a)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
i [(Int, Expr a)]
subst
apply [(Int, Expr a)]
subst v :: Expr a
v@(U a
_ Int
_)  = Expr a
v
apply [(Int, Expr a)]
subst (C a
a Int
_ Typed Constr
i [Expr a]
xs) = a -> Typed Constr -> [Expr a] -> Expr a
forall a. a -> Typed Constr -> [Expr a] -> Expr a
cap a
a Typed Constr
i ((Expr a -> Expr a) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map ([(Int, Expr a)] -> Expr a -> Expr a
apply [(Int, Expr a)]
subst) [Expr a]
xs) -- 遅いかね

Int
i occursIn :: Int -> Expr a -> Bool
`occursIn` (E a
_ Int
j)      = Int
iInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
j
Int
i `occursIn` (U a
_ Int
_)      = Bool
False
Int
i `occursIn` (C a
_ Int
_ Typed Constr
_ [Expr a]
xs) = (Expr a -> Bool) -> [Expr a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Int
i Int -> Expr a -> Bool
`occursIn`) [Expr a]
xs


plusSubst :: Subst a -> Subst a -> Subst a
Subst a
s0 plusSubst :: Subst a -> Subst a -> Subst a
`plusSubst` Subst a
s1 = [(Int
u, Subst a -> Expr a -> Expr a
forall a. [(Int, Expr a)] -> Expr a -> Expr a
apply Subst a
s0 Expr a
t) | (Int
u,Expr a
t) <- Subst a
s1] Subst a -> Subst a -> Subst a
forall a. [a] -> [a] -> [a]
++ Subst a
s0

emptySubst :: [a]
emptySubst = []


fresh :: (Int -> Int) -> Expr a -> Expr a
fresh Int -> Int
f e :: Expr a
e@(E{})      = Expr a
e
fresh Int -> Int
f (U a
a Int
i)    = a -> Int -> Expr a
forall a. a -> Int -> Expr a
E a
a (Int -> Expr a) -> Int -> Expr a
forall a b. (a -> b) -> a -> b
$ Int -> Int
f Int
i
fresh Int -> Int
f (C a
a Int
s Typed Constr
c [Expr a]
xs) = a -> Int -> Typed Constr -> [Expr a] -> Expr a
forall a. a -> Int -> Typed Constr -> [Expr a] -> Expr a
C a
a Int
s Typed Constr
c ((Expr a -> Expr a) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> Expr a -> Expr a
fresh Int -> Int
f) [Expr a]
xs)
-- | fusion of @apply s@ and @fresh f@
apfresh :: [(Int, Expr a)] -> Expr a -> Expr a
apfresh [(Int, Expr a)]
s e :: Expr a
e@(E{})      = Expr a
e -- NB: this RHS is incorrect if apfresh is used for UniT (because s may include a replacement of e).
apfresh [(Int, Expr a)]
s (U a
a Int
i) = Expr a -> (Expr a -> Expr a) -> Maybe (Expr a) -> Expr a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (a -> Int -> Expr a
forall a. a -> Int -> Expr a
E a
a Int
i) Expr a -> Expr a
forall a. a -> a
id (Maybe (Expr a) -> Expr a) -> Maybe (Expr a) -> Expr a
forall a b. (a -> b) -> a -> b
$ Int -> [(Int, Expr a)] -> Maybe (Expr a)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
i [(Int, Expr a)]
s
apfresh [(Int, Expr a)]
s (C a
a Int
_sz Typed Constr
c [Expr a]
xs) = a -> Typed Constr -> [Expr a] -> Expr a
forall a. a -> Typed Constr -> [Expr a] -> Expr a
cap a
a Typed Constr
c ((Expr a -> Expr a) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map ([(Int, Expr a)] -> Expr a -> Expr a
apfresh [(Int, Expr a)]
s) [Expr a]
xs)
mapE :: (Int -> Int) -> Expr a -> Expr a
mapE Int -> Int
f e :: Expr a
e@(U{})    = Expr a
e
mapE Int -> Int
f (E a
a Int
i)      = a -> Int -> Expr a
forall a. a -> Int -> Expr a
E a
a (Int -> Expr a) -> Int -> Expr a
forall a b. (a -> b) -> a -> b
$ Int -> Int
f Int
i
mapE Int -> Int
f e :: Expr a
e@(C{fields :: forall a. Expr a -> [Expr a]
fields=[Expr a]
xs}) = Expr a
e{fields :: [Expr a]
fields=(Expr a -> Expr a) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> Expr a -> Expr a
mapE Int -> Int
f) [Expr a]
xs}


-- Note that numUniIDs will not be touched.
applyIOPs :: [(Int, Expr a)] -> [IOPair a] -> [IOPair a]
applyIOPs [(Int, Expr a)]
s [IOPair a]
iops = (IOPair a -> IOPair a) -> [IOPair a] -> [IOPair a]
forall a b. (a -> b) -> [a] -> [b]
map ([(Int, Expr a)] -> IOPair a -> IOPair a
forall a. [(Int, Expr a)] -> IOPair a -> IOPair a
applyIOP [(Int, Expr a)]
s) [IOPair a]
iops
applyIOP :: [(Int, Expr a)] -> IOPair a -> IOPair a
applyIOP [(Int, Expr a)]
s IOPair a
iop = (Expr a -> Expr a) -> IOPair a -> IOPair a
forall a a. (Expr a -> Expr a) -> IOPair a -> IOPair a
mapIOP ([(Int, Expr a)] -> Expr a -> Expr a
forall a. [(Int, Expr a)] -> Expr a -> Expr a
apply [(Int, Expr a)]
s) IOPair a
iop
mapIOP :: (Expr a -> Expr a) -> IOPair a -> IOPair a
mapIOP Expr a -> Expr a
f (IOP Int
bvs [Expr a]
ins Expr a
out) = Int -> [Expr a] -> Expr a -> IOPair a
forall a. Int -> [Expr a] -> Expr a -> IOPair a
IOP Int
bvs ((Expr a -> Expr a) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map Expr a -> Expr a
f [Expr a]
ins) (Expr a -> Expr a
f Expr a
out)
mapTypee :: (t -> a) -> Typed t -> Typed a
mapTypee t -> a
f (t
x T.::: Type
t) = t -> a
f t
x a -> Type -> Typed a
forall a. a -> Type -> Typed a
T.::: Type
t


--
-- termination
--

newtype TermStat = TS {TermStat -> [Bool]
unTS :: [Bool]} deriving Int -> TermStat -> ShowS
[TermStat] -> ShowS
TermStat -> String
(Int -> TermStat -> ShowS)
-> (TermStat -> String) -> ([TermStat] -> ShowS) -> Show TermStat
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TermStat] -> ShowS
$cshowList :: [TermStat] -> ShowS
show :: TermStat -> String
$cshow :: TermStat -> String
showsPrec :: Int -> TermStat -> ShowS
$cshowsPrec :: Int -> TermStat -> ShowS
Show

initTS :: TermStat
initTS :: TermStat
initTS = [Bool] -> TermStat
TS ([Bool] -> TermStat) -> [Bool] -> TermStat
forall a b. (a -> b) -> a -> b
$ Int -> Bool -> [Bool]
forall a. Int -> a -> [a]
replicate ([[Expr Any] -> [Expr Any] -> Bool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Expr Any] -> [Expr Any] -> Bool]
forall a. [[Expr a] -> [Expr a] -> Bool]
termCrit) Bool
True
updateTS :: [Expr a] -> [Expr a] -> TermStat -> TermStat
updateTS :: [Expr a] -> [Expr a] -> TermStat -> TermStat
updateTS [Expr a]
bkis [Expr a]
is (TS [Bool]
bs) = [Bool] -> TermStat
TS ([Bool] -> TermStat) -> [Bool] -> TermStat
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool -> Bool) -> [Bool] -> [Bool] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Bool -> Bool -> Bool
(&&) [Bool]
bs [ [Expr a]
bkis [Expr a] -> [Expr a] -> Bool
< [Expr a]
is | [Expr a] -> [Expr a] -> Bool
(<) <- [[Expr a] -> [Expr a] -> Bool]
forall a. [[Expr a] -> [Expr a] -> Bool]
termCrit ]
evalTS :: TermStat -> Bool
evalTS :: TermStat -> Bool
evalTS (TS [Bool]
bs) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool]
bs

-- termination criteria. Enumerate anything that come to your mind. (Should this be an option?)
termCrit :: [[Expr a]->[Expr a]->Bool]
-- termCrit = [fullyLex, aWise, revFullyLex, revAWise ] -- , linear
--termCrit = [aWise,revAWise]
termCrit :: [[Expr a] -> [Expr a] -> Bool]
termCrit = [[Expr a] -> [Expr a] -> Bool
forall a. [Expr a] -> [Expr a] -> Bool
aWise]

fullyLex, revFullyLex, aWise, revAWise, linear :: [Expr a]->[Expr a]->Bool
fullyLex :: [Expr a] -> [Expr a] -> Bool
fullyLex   = (Expr a -> Expr a -> Ordering) -> [Expr a] -> [Expr a] -> Bool
forall a.
(Expr a -> Expr a -> Ordering) -> [Expr a] -> [Expr a] -> Bool
lessRevListsLex Expr a -> Expr a -> Ordering
forall a a. Expr a -> Expr a -> Ordering
cmpExprs
revFullyLex :: [Expr a] -> [Expr a] -> Bool
revFullyLex= (Expr a -> Expr a -> Ordering) -> [Expr a] -> [Expr a] -> Bool
forall t t. (t -> t -> Ordering) -> [t] -> [t] -> Bool
lessListsLex Expr a -> Expr a -> Ordering
forall a a. Expr a -> Expr a -> Ordering
cmpExprs
aWise :: [Expr a] -> [Expr a] -> Bool
aWise      = (Expr a -> Expr a -> Ordering) -> [Expr a] -> [Expr a] -> Bool
forall a.
(Expr a -> Expr a -> Ordering) -> [Expr a] -> [Expr a] -> Bool
lessRevListsLex Expr a -> Expr a -> Ordering
forall a a. Expr a -> Expr a -> Ordering
cmpExprSzs
revAWise :: [Expr a] -> [Expr a] -> Bool
revAWise   = (Expr a -> Expr a -> Ordering) -> [Expr a] -> [Expr a] -> Bool
forall t t. (t -> t -> Ordering) -> [t] -> [t] -> Bool
lessListsLex Expr a -> Expr a -> Ordering
forall a a. Expr a -> Expr a -> Ordering
cmpExprSzs
-- linear is really slow, so is not recommended.
linear :: [Expr a] -> [Expr a] -> Bool
linear [Expr a]
ls [Expr a]
rs = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Expr a -> Int) -> [Expr a] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Expr a -> Int
forall a. Expr a -> Int
size [Expr a]
ls) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Expr a -> Int) -> [Expr a] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Expr a -> Int
forall a. Expr a -> Int
size [Expr a]
rs)
-- でも，caseでぶった切ったあとのすべての引数を比較しているから遅いのであって，一番最初の段階の引数だけで比較すれば速いのでは？
-- でも，Ackermann's functionで考えると，やっぱそれではダメっぽい．

revArgs :: ([Expr a]->[Expr a]->Bool) -> [Expr a]->[Expr a]->Bool
revArgs :: ([Expr a] -> [Expr a] -> Bool) -> [Expr a] -> [Expr a] -> Bool
revArgs [Expr a] -> [Expr a] -> Bool
cmp [Expr a]
ls [Expr a]
rs = [Expr a] -> [Expr a] -> Bool
cmp ([Expr a] -> [Expr a]
forall a. [a] -> [a]
reverse [Expr a]
ls) ([Expr a] -> [Expr a]
forall a. [a] -> [a]
reverse [Expr a]
rs)

lessRevListsLex :: (Expr a -> Expr a -> Ordering) -> [Expr a] -> [Expr a] -> Bool
lessRevListsLex Expr a -> Expr a -> Ordering
cmp  = ([Expr a] -> [Expr a] -> Bool) -> [Expr a] -> [Expr a] -> Bool
forall a.
([Expr a] -> [Expr a] -> Bool) -> [Expr a] -> [Expr a] -> Bool
revArgs ((Expr a -> Expr a -> Ordering) -> [Expr a] -> [Expr a] -> Bool
forall t t. (t -> t -> Ordering) -> [t] -> [t] -> Bool
lessListsLex Expr a -> Expr a -> Ordering
cmp)
lessListsLex :: (t -> t -> Ordering) -> [t] -> [t] -> Bool
lessListsLex t -> t -> Ordering
cmp []       [t]
_        = Bool
False -- In general, input arguments of BKs should be shorter, and we have to compare only this length.
lessListsLex t -> t -> Ordering
cmp (t
e0:[t]
es0) (t
e1:[t]
es1) = case t -> t -> Ordering
cmp t
e0 t
e1 of Ordering
LT -> Bool
True
                                                       Ordering
EQ -> (t -> t -> Ordering) -> [t] -> [t] -> Bool
lessListsLex t -> t -> Ordering
cmp [t]
es0 [t]
es1
                                                       Ordering
GT -> Bool
False
cmpExprss :: [Expr a] -> [Expr a] -> Ordering
cmpExprss []       []       = Ordering
EQ
cmpExprss []       [Expr a]
_        = Ordering
LT
cmpExprss [Expr a]
_        []       = Ordering
GT
cmpExprss (Expr a
e0:[Expr a]
es0) (Expr a
e1:[Expr a]
es1) = case Expr a -> Expr a -> Ordering
cmpExprs Expr a
e0 Expr a
e1 of Ordering
EQ -> [Expr a] -> [Expr a] -> Ordering
cmpExprss [Expr a]
es0 [Expr a]
es1
                                                     Ordering
c  -> Ordering
c
cmpExprs :: Expr a -> Expr a -> Ordering
cmpExprs (C a
_ Int
_ Typed Constr
_ [Expr a]
fs) (C a
_ Int
_ Typed Constr
_ [Expr a]
gs) = [Expr a] -> [Expr a] -> Ordering
cmpExprss [Expr a]
fs [Expr a]
gs
cmpExprs Expr a
_            (C a
_ Int
_ Typed Constr
_ [Expr a]
_)  = Ordering
LT
cmpExprs (C a
_ Int
_ Typed Constr
_ [Expr a]
_)  Expr a
_            = Ordering
GT
cmpExprs Expr a
_            Expr a
_            = Ordering
EQ

cmpExprSzs :: Expr a -> Expr a -> Ordering
cmpExprSzs Expr a
e0 Expr a
e1 = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Expr a -> Int
forall a. Expr a -> Int
size Expr a
e0) (Expr a -> Int
forall a. Expr a -> Int
size Expr a
e1)
size :: Expr a -> Int
size (C a
_ Int
sz Typed Constr
_ [Expr a]
fs) = Int
sz
size Expr a
_        = Int
1 -- questionable?
cap :: a -> Typed Constr -> [Expr a] -> Expr a
cap a
a Typed Constr
con [Expr a]
fs = a -> Int -> Typed Constr -> [Expr a] -> Expr a
forall a. a -> Int -> Typed Constr -> [Expr a] -> Expr a
C a
a (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Expr a -> Int) -> [Expr a] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Expr a -> Int
forall a. Expr a -> Int
size [Expr a]
fs)) Typed Constr
con [Expr a]
fs

-- Q: Are existential variables always smaller than constructor applications? A: No, I'm afraid.
-- If we want to make sure the termination, we can always return GT when questionable;
-- if we want to save all questionable expressions, we can always return LT when questionable.