{-# LANGUAGE TypeFamilies, FlexibleContexts, RecordWildCards, BangPatterns, OverloadedStrings, MultiParamTypeClasses, ScopedTypeVariables, GeneralizedNewtypeDeriving #-}
module Twee.Rule where
import Twee.Base
import Twee.Constraints hiding (funs)
import qualified Twee.Index as Index
import Twee.Index(Index)
import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.Trans.State.Strict
import Data.Maybe
import Data.List
import Twee.Utils
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import qualified Twee.Term as Term
import Data.Ord
import Twee.Equation
import qualified Twee.Proof as Proof
import Twee.Proof(Derivation, Proof)
import Data.Tuple
data Rule f =
Rule {
Rule f -> Orientation f
orientation :: Orientation f,
Rule f -> Proof f
rule_proof :: !(Proof f),
Rule f -> Term f
lhs :: {-# UNPACK #-} !(Term f),
Rule f -> Term f
rhs :: {-# UNPACK #-} !(Term f) }
deriving Int -> Rule f -> ShowS
[Rule f] -> ShowS
Rule f -> String
(Int -> Rule f -> ShowS)
-> (Rule f -> String) -> ([Rule f] -> ShowS) -> Show (Rule f)
forall f. (Labelled f, Show f) => Int -> Rule f -> ShowS
forall f. (Labelled f, Show f) => [Rule f] -> ShowS
forall f. (Labelled f, Show f) => Rule f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rule f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [Rule f] -> ShowS
show :: Rule f -> String
$cshow :: forall f. (Labelled f, Show f) => Rule f -> String
showsPrec :: Int -> Rule f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> Rule f -> ShowS
Show
instance Eq (Rule f) where
Rule f
x == :: Rule f -> Rule f -> Bool
== Rule f
y = Rule f -> Rule f -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Rule f
x Rule f
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ
instance Ord (Rule f) where
compare :: Rule f -> Rule f -> Ordering
compare = (Rule f -> (Term f, Term f)) -> Rule f -> Rule f -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (\Rule f
rule -> (Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
rule, Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
rule))
type RuleOf a = Rule (ConstantOf a)
ruleDerivation :: Rule f -> Derivation f
ruleDerivation :: Rule f -> Derivation f
ruleDerivation Rule f
r =
case (Equation f -> Equation f -> Maybe (Subst f)
forall f. Equation f -> Equation f -> Maybe (Subst f)
matchEquation (Proof f -> Equation f
forall f. Proof f -> Equation f
Proof.equation (Rule f -> Proof f
forall f. Rule f -> Proof f
rule_proof Rule f
r)) (Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
r Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
r),
Equation f -> Equation f -> Maybe (Subst f)
forall f. Equation f -> Equation f -> Maybe (Subst f)
matchEquation (Proof f -> Equation f
forall f. Proof f -> Equation f
Proof.equation (Rule f -> Proof f
forall f. Rule f -> Proof f
rule_proof Rule f
r)) (Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
r Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
r)) of
(Just Subst f
sub, Maybe (Subst f)
_) -> Proof f -> Subst f -> Derivation f
forall f. Proof f -> Subst f -> Derivation f
Proof.lemma (Rule f -> Proof f
forall f. Rule f -> Proof f
rule_proof Rule f
r) Subst f
sub
(Maybe (Subst f)
_, Just Subst f
sub) -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
Proof.symm (Proof f -> Subst f -> Derivation f
forall f. Proof f -> Subst f -> Derivation f
Proof.lemma (Rule f -> Proof f
forall f. Rule f -> Proof f
rule_proof Rule f
r) Subst f
sub)
(Maybe (Subst f), Maybe (Subst f))
_ -> String -> Derivation f
forall a. HasCallStack => String -> a
error String
"rule out of sync with proof"
data Orientation f =
Oriented
| WeaklyOriented {-# UNPACK #-} !(Fun f) [Term f]
| Permutative [(Term f, Term f)]
| Unoriented
deriving Int -> Orientation f -> ShowS
[Orientation f] -> ShowS
Orientation f -> String
(Int -> Orientation f -> ShowS)
-> (Orientation f -> String)
-> ([Orientation f] -> ShowS)
-> Show (Orientation f)
forall f. (Labelled f, Show f) => Int -> Orientation f -> ShowS
forall f. (Labelled f, Show f) => [Orientation f] -> ShowS
forall f. (Labelled f, Show f) => Orientation f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Orientation f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [Orientation f] -> ShowS
show :: Orientation f -> String
$cshow :: forall f. (Labelled f, Show f) => Orientation f -> String
showsPrec :: Int -> Orientation f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> Orientation f -> ShowS
Show
instance Eq (Orientation f) where Orientation f
_ == :: Orientation f -> Orientation f -> Bool
== Orientation f
_ = Bool
True
instance Ord (Orientation f) where compare :: Orientation f -> Orientation f -> Ordering
compare Orientation f
_ Orientation f
_ = Ordering
EQ
oriented :: Orientation f -> Bool
oriented :: Orientation f -> Bool
oriented Oriented{} = Bool
True
oriented WeaklyOriented{} = Bool
True
oriented Orientation f
_ = Bool
False
instance Symbolic (Rule f) where
type ConstantOf (Rule f) = f
termsDL :: Rule f -> DList (TermListOf (Rule f))
termsDL (Rule Orientation f
_ Proof f
_ Term f
t Term f
_) = Term f -> DList (TermListOf (Term f))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Term f
t
subst_ :: (Var -> BuilderOf (Rule f)) -> Rule f -> Rule f
subst_ Var -> BuilderOf (Rule f)
sub (Rule Orientation f
or Proof f
pf Term f
t Term f
u) = Orientation f -> Proof f -> Term f -> Term f -> Rule f
forall f. Orientation f -> Proof f -> Term f -> Term f -> Rule f
Rule ((Var -> BuilderOf (Orientation f))
-> Orientation f -> Orientation f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Orientation f)
Var -> BuilderOf (Rule f)
sub Orientation f
or) Proof f
pf ((Var -> BuilderOf (Term f)) -> Term f -> Term f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Term f)
Var -> BuilderOf (Rule f)
sub Term f
t) ((Var -> BuilderOf (Term f)) -> Term f -> Term f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Term f)
Var -> BuilderOf (Rule f)
sub Term f
u)
instance f ~ g => Has (Rule f) (Term g) where
the :: Rule f -> Term g
the = Rule f -> Term g
forall f. Rule f -> Term f
lhs
instance Symbolic (Orientation f) where
type ConstantOf (Orientation f) = f
termsDL :: Orientation f -> DList (TermListOf (Orientation f))
termsDL Orientation f
Oriented = DList (TermListOf (Orientation f))
forall (m :: * -> *) a. MonadPlus m => m a
mzero
termsDL (WeaklyOriented Fun f
_ [Term f]
ts) = [Term f] -> DList (TermListOf [Term f])
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL [Term f]
ts
termsDL (Permutative [(Term f, Term f)]
ts) = [(Term f, Term f)] -> DList (TermListOf [(Term f, Term f)])
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL [(Term f, Term f)]
ts
termsDL Orientation f
Unoriented = DList (TermListOf (Orientation f))
forall (m :: * -> *) a. MonadPlus m => m a
mzero
subst_ :: (Var -> BuilderOf (Orientation f))
-> Orientation f -> Orientation f
subst_ Var -> BuilderOf (Orientation f)
_ Orientation f
Oriented = Orientation f
forall f. Orientation f
Oriented
subst_ Var -> BuilderOf (Orientation f)
sub (WeaklyOriented Fun f
min [Term f]
ts) = Fun f -> [Term f] -> Orientation f
forall f. Fun f -> [Term f] -> Orientation f
WeaklyOriented Fun f
min ((Var -> BuilderOf [Term f]) -> [Term f] -> [Term f]
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf [Term f]
Var -> BuilderOf (Orientation f)
sub [Term f]
ts)
subst_ Var -> BuilderOf (Orientation f)
sub (Permutative [(Term f, Term f)]
ts) = [(Term f, Term f)] -> Orientation f
forall f. [(Term f, Term f)] -> Orientation f
Permutative ((Var -> BuilderOf [(Term f, Term f)])
-> [(Term f, Term f)] -> [(Term f, Term f)]
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf [(Term f, Term f)]
Var -> BuilderOf (Orientation f)
sub [(Term f, Term f)]
ts)
subst_ Var -> BuilderOf (Orientation f)
_ Orientation f
Unoriented = Orientation f
forall f. Orientation f
Unoriented
instance (Labelled f, PrettyTerm f) => Pretty (Rule f) where
pPrint :: Rule f -> Doc
pPrint (Rule Orientation f
or Proof f
_ Term f
l Term f
r) =
Term f -> Doc
forall a. Pretty a => a -> Doc
pPrint Term f
l Doc -> Doc -> Doc
<+> String -> Doc
text (Orientation f -> String
forall p f. IsString p => Orientation f -> p
showOrientation Orientation f
or) Doc -> Doc -> Doc
<+> Term f -> Doc
forall a. Pretty a => a -> Doc
pPrint Term f
r
where
showOrientation :: Orientation f -> p
showOrientation Orientation f
Oriented = p
"->"
showOrientation WeaklyOriented{} = p
"~>"
showOrientation Permutative{} = p
"<->"
showOrientation Orientation f
Unoriented = p
"="
unorient :: Rule f -> Equation f
unorient :: Rule f -> Equation f
unorient (Rule Orientation f
_ Proof f
_ Term f
l Term f
r) = Term f
l Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
r
orient :: Function f => Equation f -> Proof f -> Rule f
orient :: Equation f -> Proof f -> Rule f
orient (Term f
t :=: Term f
u) Proof f
pf = Orientation f -> Proof f -> Term f -> Term f -> Rule f
forall f. Orientation f -> Proof f -> Term f -> Term f -> Rule f
Rule Orientation f
o Proof f
pf Term f
t Term f
u
where
o :: Orientation f
o | Term f -> Term f -> Bool
forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
u Term f
t =
case Term f -> Term f -> Maybe (Subst f)
forall f. Term f -> Term f -> Maybe (Subst f)
unify Term f
t Term f
u of
Maybe (Subst f)
Nothing -> Orientation f
forall f. Orientation f
Oriented
Just Subst f
sub
| (Var -> TermList f -> Bool) -> Subst f -> Bool
forall f. (Var -> TermList f -> Bool) -> Subst f -> Bool
allSubst (\Var
_ (Cons Term f
t TermList f
Empty) -> Term f -> Bool
forall f. Minimal f => Term f -> Bool
isMinimal Term f
t) Subst f
sub ->
Fun f -> [Term f] -> Orientation f
forall f. Fun f -> [Term f] -> Orientation f
WeaklyOriented Fun f
forall f. Minimal f => Fun f
minimal (((Var, Term f) -> Term f) -> [(Var, Term f)] -> [Term f]
forall a b. (a -> b) -> [a] -> [b]
map (Builder f -> Term f
forall a. Build a => a -> Term (BuildFun a)
build (Builder f -> Term f)
-> ((Var, Term f) -> Builder f) -> (Var, Term f) -> Term f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Builder f
forall f. Var -> Builder f
var (Var -> Builder f)
-> ((Var, Term f) -> Var) -> (Var, Term f) -> Builder f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Term f) -> Var
forall a b. (a, b) -> a
fst) (Subst f -> [(Var, Term f)]
forall f. Subst f -> [(Var, Term f)]
substToList Subst f
sub))
| Bool
otherwise -> Orientation f
forall f. Orientation f
Unoriented
| Term f -> Term f -> Bool
forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
t Term f
u = String -> Orientation f
forall a. HasCallStack => String -> a
error String
"wrongly-oriented rule"
| Bool -> Bool
not ([Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
u) [Var] -> [Var] -> [Var]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars Term f
t))) =
String -> Orientation f
forall a. HasCallStack => String -> a
error String
"unbound variables in rule"
| Just [(Term f, Term f)]
ts <- StateT [(Var, Term f)] Maybe [(Term f, Term f)]
-> [(Var, Term f)] -> Maybe [(Term f, Term f)]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Term f -> Term f -> StateT [(Var, Term f)] Maybe [(Term f, Term f)]
forall f f f.
Term f -> Term f -> StateT [(Var, Term f)] Maybe [(Term f, Term f)]
makePermutative Term f
t Term f
u) [],
Term f -> Term f -> [(Term f, Term f)] -> Bool
forall f f f.
(Minimal f, Ordered f) =>
Term f -> Term f -> [(Term f, Term f)] -> Bool
permutativeOK Term f
t Term f
u [(Term f, Term f)]
ts =
[(Term f, Term f)] -> Orientation f
forall f. [(Term f, Term f)] -> Orientation f
Permutative [(Term f, Term f)]
ts
| Bool
otherwise = Orientation f
forall f. Orientation f
Unoriented
permutativeOK :: Term f -> Term f -> [(Term f, Term f)] -> Bool
permutativeOK Term f
_ Term f
_ [] = Bool
True
permutativeOK Term f
t Term f
u ((Var Var
x, Var Var
y):[(Term f, Term f)]
xs) =
Model f -> Term f -> Term f -> Maybe Strictness
forall f.
Ordered f =>
Model f -> Term f -> Term f -> Maybe Strictness
lessIn Model f
model Term f
u Term f
t Maybe Strictness -> Maybe Strictness -> Bool
forall a. Eq a => a -> a -> Bool
== Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
Strict Bool -> Bool -> Bool
&&
Term f -> Term f -> [(Term f, Term f)] -> Bool
permutativeOK Term f
t' Term f
u' [(Term f, Term f)]
xs
where
model :: Model f
model = [Atom f] -> Model f
forall f. (Minimal f, Ord f) => [Atom f] -> Model f
modelFromOrder [Var -> Atom f
forall f. Var -> Atom f
Variable Var
y, Var -> Atom f
forall f. Var -> Atom f
Variable Var
x]
sub :: Var -> Builder f
sub Var
x' = if Var
x Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
x' then Var -> Builder f
forall f. Var -> Builder f
var Var
y else Var -> Builder f
forall f. Var -> Builder f
var Var
x'
t' :: Term f
t' = (Var -> Builder f) -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Var -> Builder f
sub Term f
t
u' :: Term f
u' = (Var -> Builder f) -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Var -> Builder f
sub Term f
u
makePermutative :: Term f -> Term f -> StateT [(Var, Term f)] Maybe [(Term f, Term f)]
makePermutative Term f
t Term f
u = do
Maybe (Subst f)
msub <- ([(Var, Term f)] -> Maybe (Subst f))
-> StateT [(Var, Term f)] Maybe (Maybe (Subst f))
forall (m :: * -> *) s a. Monad m => (s -> a) -> StateT s m a
gets [(Var, Term f)] -> Maybe (Subst f)
forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst
Subst f
sub <- Maybe (Subst f) -> StateT [(Var, Term f)] Maybe (Subst f)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Maybe (Subst f)
msub
Term f -> Term f -> StateT [(Var, Term f)] Maybe [(Term f, Term f)]
aux (Subst f -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
t) (Subst f -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
u)
where
aux :: Term f -> Term f -> StateT [(Var, Term f)] Maybe [(Term f, Term f)]
aux (Var Var
x) (Var Var
y)
| Var
x Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
y = [(Term f, Term f)]
-> StateT [(Var, Term f)] Maybe [(Term f, Term f)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do
([(Var, Term f)] -> [(Var, Term f)])
-> StateT [(Var, Term f)] Maybe ()
forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify ((Var
x, Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Builder f -> Term (BuildFun (Builder f)))
-> Builder f -> Term (BuildFun (Builder f))
forall a b. (a -> b) -> a -> b
$ Var -> Builder f
forall f. Var -> Builder f
var Var
y)(Var, Term f) -> [(Var, Term f)] -> [(Var, Term f)]
forall a. a -> [a] -> [a]
:)
[(Term f, Term f)]
-> StateT [(Var, Term f)] Maybe [(Term f, Term f)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Builder f -> Term (BuildFun (Builder f)))
-> Builder f -> Term (BuildFun (Builder f))
forall a b. (a -> b) -> a -> b
$ Var -> Builder f
forall f. Var -> Builder f
var Var
x, Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Builder f -> Term (BuildFun (Builder f)))
-> Builder f -> Term (BuildFun (Builder f))
forall a b. (a -> b) -> a -> b
$ Var -> Builder f
forall f. Var -> Builder f
var Var
y)]
aux (App Fun f
f TermList f
ts) (App Fun f
g TermList f
us)
| Fun f
f Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
g =
([[(Term f, Term f)]] -> [(Term f, Term f)])
-> StateT [(Var, Term f)] Maybe [[(Term f, Term f)]]
-> StateT [(Var, Term f)] Maybe [(Term f, Term f)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(Term f, Term f)]] -> [(Term f, Term f)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Term f
-> Term f -> StateT [(Var, Term f)] Maybe [(Term f, Term f)])
-> [Term f]
-> [Term f]
-> StateT [(Var, Term f)] Maybe [[(Term f, Term f)]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Term f -> Term f -> StateT [(Var, Term f)] Maybe [(Term f, Term f)]
makePermutative (TermList f -> [Term f]
forall f. TermList f -> [Term f]
unpack TermList f
ts) (TermList f -> [Term f]
forall f. TermList f -> [Term f]
unpack TermList f
us))
aux Term f
_ Term f
_ = StateT [(Var, Term f)] Maybe [(Term f, Term f)]
forall (m :: * -> *) a. MonadPlus m => m a
mzero
backwards :: Rule f -> Rule f
backwards :: Rule f -> Rule f
backwards (Rule Orientation f
or Proof f
pf Term f
t Term f
u) = Orientation f -> Proof f -> Term f -> Term f -> Rule f
forall f. Orientation f -> Proof f -> Term f -> Term f -> Rule f
Rule (Orientation f -> Orientation f
forall f. Orientation f -> Orientation f
back Orientation f
or) Proof f
pf Term f
u Term f
t
where
back :: Orientation f -> Orientation f
back (Permutative [(Term f, Term f)]
xs) = [(Term f, Term f)] -> Orientation f
forall f. [(Term f, Term f)] -> Orientation f
Permutative (((Term f, Term f) -> (Term f, Term f))
-> [(Term f, Term f)] -> [(Term f, Term f)]
forall a b. (a -> b) -> [a] -> [b]
map (Term f, Term f) -> (Term f, Term f)
forall a b. (a, b) -> (b, a)
swap [(Term f, Term f)]
xs)
back Orientation f
Unoriented = Orientation f
forall f. Orientation f
Unoriented
back Orientation f
_ = String -> Orientation f
forall a. HasCallStack => String -> a
error String
"Can't turn oriented rule backwards"
{-# INLINEABLE simplify #-}
{-# SCC simplify #-}
simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
simplify :: Index f a -> Term f -> Term f
simplify = Index f a -> Term f -> Term f
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplifyOutermost
simplifyOutermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
simplifyOutermost :: Index f a -> Term f -> Term f
simplifyOutermost !Index f a
idx !Term f
t
| Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
Term (BuildFun (Builder f))
u = Term f
t
| Bool
otherwise = Index f a -> Term f -> Term f
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplify Index f a
idx Term f
Term (BuildFun (Builder f))
u
where
u :: Term (BuildFun (Builder f))
u = Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (TermList f -> Builder f
simp (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
t))
simp :: TermList f -> Builder f
simp TermList f
Empty = Builder f
forall a. Monoid a => a
mempty
simp (Cons (Var Var
x) TermList f
t) = Var -> Builder f
forall f. Var -> Builder f
var Var
x Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` TermList f -> Builder f
simp TermList f
t
simp (Cons Term f
t TermList f
u)
| Just (Rule f
rule, Subst f
sub) <- Index f a -> Term f -> Maybe (Rule f, Subst f)
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Maybe (Rule f, Subst f)
simpleRewrite Index f a
idx Term f
t =
Subst f
-> Term (SubstFun (Subst f)) -> Builder (SubstFun (Subst f))
forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
Term.subst Subst f
sub (Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
rule) Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` TermList f -> Builder f
simp TermList f
u
simp (Cons (App Fun f
f TermList f
ts) TermList f
us) =
Fun (BuildFun (Builder f))
-> Builder f -> Builder (BuildFun (Builder f))
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
Fun (BuildFun (Builder f))
f (TermList f -> Builder f
simp TermList f
ts) Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` TermList f -> Builder f
simp TermList f
us
simplifyInnermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
simplifyInnermost :: Index f a -> Term f -> Term f
simplifyInnermost !Index f a
idx !Term f
t = Term f -> Term f
simp Term f
t
where
simp :: Term f -> Term f
simp Term f
t =
case [(Rule f, Subst f)
rw | Term f
u <- Term f -> [Term f]
forall f. Term f -> [Term f]
reverseSubterms Term f
t, Just (Rule f, Subst f)
rw <- [Index f a -> Term f -> Maybe (Rule f, Subst f)
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Maybe (Rule f, Subst f)
simpleRewrite Index f a
idx Term f
u]] of
[] -> Term f
t
(Rule f
rule, Subst f
sub):[(Rule f, Subst f)]
_ ->
let l :: Term (BuildFun (Builder f))
l = Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Subst f
-> Term (SubstFun (Subst f)) -> Builder (SubstFun (Subst f))
forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
Term.subst Subst f
sub (Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
rule))
r :: Term (BuildFun (Builder f))
r = Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Subst f
-> Term (SubstFun (Subst f)) -> Builder (SubstFun (Subst f))
forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
Term.subst Subst f
sub (Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
rule))
in Term f -> Term f
simp (Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Term f -> Term f -> TermList f -> Builder f
forall a f.
(Build a, BuildFun a ~ f) =>
Term f -> a -> TermList f -> Builder f
replace Term f
Term (BuildFun (Builder f))
l Term f
Term (BuildFun (Builder f))
r (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
t)))
{-# INLINEABLE simpleRewrite #-}
{-# SCC simpleRewrite #-}
simpleRewrite :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Maybe (Rule f, Subst f)
simpleRewrite :: Index f a -> Term f -> Maybe (Rule f, Subst f)
simpleRewrite Index f a
idx Term f
t =
((Rule f, Subst f)
-> Maybe (Rule f, Subst f) -> Maybe (Rule f, Subst f))
-> Maybe (Rule f, Subst f)
-> [(Rule f, Subst f)]
-> Maybe (Rule f, Subst f)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Rule f, Subst f)
x Maybe (Rule f, Subst f)
_ -> (Rule f, Subst f) -> Maybe (Rule f, Subst f)
forall a. a -> Maybe a
Just (Rule f, Subst f)
x) Maybe (Rule f, Subst f)
forall a. Maybe a
Nothing ([(Rule f, Subst f)] -> Maybe (Rule f, Subst f))
-> [(Rule f, Subst f)] -> Maybe (Rule f, Subst f)
forall a b. (a -> b) -> a -> b
$ do
Rule f
rule <- a -> Rule f
forall a b. Has a b => a -> b
the (a -> Rule f) -> [a] -> [Rule f]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term f -> Index f a -> [a]
forall f a. Term f -> Index f a -> [a]
Index.approxMatches Term f
t Index f a
idx
Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Orientation f -> Bool
forall f. Orientation f -> Bool
oriented (Rule f -> Orientation f
forall f. Rule f -> Orientation f
orientation Rule f
rule))
Subst f
sub <- Maybe (Subst f) -> [Subst f]
forall a. Maybe a -> [a]
maybeToList (Term f -> Term f -> Maybe (Subst f)
forall f. Term f -> Term f -> Maybe (Subst f)
match (Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
rule) Term f
t)
Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reducesOriented Rule f
rule Subst f
sub)
(Rule f, Subst f) -> [(Rule f, Subst f)]
forall (m :: * -> *) a. Monad m => a -> m a
return (Rule f
rule, Subst f
sub)
type Strategy f = Term f -> [Reduction f]
type Reduction f = [Rule f]
trans :: Reduction f -> Reduction f -> Reduction f
trans :: Reduction f -> Reduction f -> Reduction f
trans Reduction f
p Reduction f
q = Reduction f
q Reduction f -> Reduction f -> Reduction f
forall a. [a] -> [a] -> [a]
++ Reduction f
p
result :: Term f -> Reduction f -> Term f
result :: Term f -> Reduction f -> Term f
result Term f
t [] = Term f
t
result Term f
t (Rule f
r:Reduction f
rs) = Term f -> Rule f -> Term f
forall f. Term f -> Rule f -> Term f
ruleResult Term f
u Rule f
r
where
u :: Term f
u = Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
t Reduction f
rs
reductionProof :: Function f => Term f -> Reduction f -> Derivation f
reductionProof :: Term f -> Reduction f -> Derivation f
reductionProof Term f
t Reduction f
ps = Term f -> Derivation f -> Reduction f -> Derivation f
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
Labelled f) =>
Term f -> Derivation f -> [Rule f] -> Derivation f
red Term f
t (Term f -> Derivation f
forall f. Term f -> Derivation f
Proof.Refl Term f
t) (Reduction f -> Reduction f
forall a. [a] -> [a]
reverse Reduction f
ps)
where
red :: Term f -> Derivation f -> [Rule f] -> Derivation f
red Term f
_ Derivation f
p [] = Derivation f
p
red Term f
t Derivation f
p (Rule f
q:[Rule f]
qs) =
Term f -> Derivation f -> [Rule f] -> Derivation f
red (Term f -> Rule f -> Term f
forall f. Term f -> Rule f -> Term f
ruleResult Term f
t Rule f
q) (Derivation f
p Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans` Term f -> Rule f -> Derivation f
forall f. Function f => Term f -> Rule f -> Derivation f
ruleProof Term f
t Rule f
q) [Rule f]
qs
ruleResult :: Term f -> Rule f -> Term f
ruleResult :: Term f -> Rule f -> Term f
ruleResult Term f
t Rule f
r = Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Term f -> Term f -> TermList f -> Builder f
forall a f.
(Build a, BuildFun a ~ f) =>
Term f -> a -> TermList f -> Builder f
replace (Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
r) (Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
r) (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
t))
ruleProof :: Function f => Term f -> Rule f -> Derivation f
ruleProof :: Term f -> Rule f -> Derivation f
ruleProof Term f
t r :: Rule f
r@(Rule Orientation f
_ Proof f
_ Term f
lhs Term f
_)
| Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
lhs = Rule f -> Derivation f
forall f. Rule f -> Derivation f
ruleDerivation Rule f
r
| Term f -> Int
forall f. Term f -> Int
len Term f
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Term f -> Int
forall f. Term f -> Int
len Term f
lhs = Term f -> Derivation f
forall f. Term f -> Derivation f
Proof.Refl Term f
t
ruleProof (App Fun f
f TermList f
ts) Rule f
rule =
Fun f -> [Derivation f] -> Derivation f
forall f. Fun f -> [Derivation f] -> Derivation f
Proof.cong Fun f
f [Term f -> Rule f -> Derivation f
forall f. Function f => Term f -> Rule f -> Derivation f
ruleProof Term f
u Rule f
rule | Term f
u <- TermList f -> [Term f]
forall f. TermList f -> [Term f]
unpack TermList f
ts]
ruleProof Term f
t Rule f
_ = Term f -> Derivation f
forall f. Term f -> Derivation f
Proof.Refl Term f
t
{-# INLINE normaliseWith #-}
{-# SCC normaliseWith #-}
normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith :: (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith Term f -> Bool
ok Strategy f
strat Term f
t = Reduction f
res
where
res :: Reduction f
res = Integer -> Reduction f -> Term f -> Reduction f
aux Integer
0 [] Term f
t
aux :: Integer -> Reduction f -> Term f -> Reduction f
aux Integer
1000 Reduction f
p Term f
_ =
String -> Reduction f
forall a. HasCallStack => String -> a
error (String -> Reduction f) -> String -> Reduction f
forall a b. (a -> b) -> a -> b
$
String
"Possibly nonterminating rewrite:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Reduction f -> String
forall a. Pretty a => a -> String
prettyShow Reduction f
p
aux Integer
n Reduction f
p Term f
t =
case Strategy f -> Strategy f
forall f. Strategy f -> Strategy f
anywhere Strategy f
strat Term f
t of
(Reduction f
q:[Reduction f]
_) | Term f
u <- Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
t Reduction f
q, Term f -> Bool
ok Term f
u ->
Integer -> Reduction f -> Term f -> Reduction f
aux (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Reduction f
p Reduction f -> Reduction f -> Reduction f
forall f. Reduction f -> Reduction f -> Reduction f
`trans` Reduction f
q) Term f
u
[Reduction f]
_ -> Reduction f
p
normalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
normalForms :: Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
normalForms Strategy f
strat Map (Term f) (Reduction f)
ps = (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
-> Map (Term f) (Term f, Reduction f)
forall a b. (a, b) -> b
snd (Strategy f
-> Map (Term f) (Reduction f)
-> (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f)
-> (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
successorsAndNormalForms Strategy f
strat Map (Term f) (Reduction f)
ps)
successors :: Function f => Strategy f -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
successors :: Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
successors Strategy f
strat Map (Term f) (Reduction f)
ps =
Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map (Term f) (Term f, Reduction f)
qs Map (Term f) (Term f, Reduction f)
rs
where
(Map (Term f) (Term f, Reduction f)
qs, Map (Term f) (Term f, Reduction f)
rs) = Strategy f
-> Map (Term f) (Reduction f)
-> (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f)
-> (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
successorsAndNormalForms Strategy f
strat Map (Term f) (Reduction f)
ps
{-# INLINEABLE successorsAndNormalForms #-}
{-# SCC successorsAndNormalForms #-}
successorsAndNormalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) ->
(Map (Term f) (Term f, Reduction f), Map (Term f) (Term f, Reduction f))
successorsAndNormalForms :: Strategy f
-> Map (Term f) (Reduction f)
-> (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
successorsAndNormalForms Strategy f
strat Map (Term f) (Reduction f)
ps =
Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
go Map (Term f) (Term f, Reduction f)
forall k a. Map k a
Map.empty Map (Term f) (Term f, Reduction f)
forall k a. Map k a
Map.empty ((Term f -> Reduction f -> (Term f, Reduction f))
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\Term f
t Reduction f
red -> (Term f
t, Reduction f
red)) Map (Term f) (Reduction f)
ps)
where
go :: Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
go Map (Term f) (Term f, Reduction f)
dead Map (Term f) (Term f, Reduction f)
norm Map (Term f) (Term f, Reduction f)
ps =
case Map (Term f) (Term f, Reduction f)
-> Maybe
((Term f, (Term f, Reduction f)),
Map (Term f) (Term f, Reduction f))
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.minViewWithKey Map (Term f) (Term f, Reduction f)
ps of
Maybe
((Term f, (Term f, Reduction f)),
Map (Term f) (Term f, Reduction f))
Nothing -> (Map (Term f) (Term f, Reduction f)
dead, Map (Term f) (Term f, Reduction f)
norm)
Just ((Term f
t, (Term f, Reduction f)
p), Map (Term f) (Term f, Reduction f)
ps)
| Term f
t Term f -> Map (Term f) (Term f, Reduction f) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map (Term f) (Term f, Reduction f)
dead -> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
go Map (Term f) (Term f, Reduction f)
dead Map (Term f) (Term f, Reduction f)
norm Map (Term f) (Term f, Reduction f)
ps
| Term f
t Term f -> Map (Term f) (Term f, Reduction f) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map (Term f) (Term f, Reduction f)
norm -> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
go Map (Term f) (Term f, Reduction f)
dead Map (Term f) (Term f, Reduction f)
norm Map (Term f) (Term f, Reduction f)
ps
| [(Term f, (Term f, Reduction f))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Term f, (Term f, Reduction f))]
qs -> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
go Map (Term f) (Term f, Reduction f)
dead (Term f
-> (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Term f
t (Term f, Reduction f)
p Map (Term f) (Term f, Reduction f)
norm) Map (Term f) (Term f, Reduction f)
ps
| Bool
otherwise ->
Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> (Map (Term f) (Term f, Reduction f),
Map (Term f) (Term f, Reduction f))
go (Term f
-> (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Term f
t (Term f, Reduction f)
p Map (Term f) (Term f, Reduction f)
dead) Map (Term f) (Term f, Reduction f)
norm ([(Term f, (Term f, Reduction f))]
-> Map (Term f) (Term f, Reduction f)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Term f, (Term f, Reduction f))]
qs Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map (Term f) (Term f, Reduction f)
ps)
where
qs :: [(Term f, (Term f, Reduction f))]
qs =
[ (Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
t Reduction f
q, ((Term f, Reduction f) -> Term f
forall a b. (a, b) -> a
fst (Term f, Reduction f)
p, ((Term f, Reduction f) -> Reduction f
forall a b. (a, b) -> b
snd (Term f, Reduction f)
p Reduction f -> Reduction f -> Reduction f
forall f. Reduction f -> Reduction f -> Reduction f
`trans` Reduction f
q)))
| Reduction f
q <- Strategy f -> Strategy f
forall f. Strategy f -> Strategy f
anywhere Strategy f
strat Term f
t ]
anywhere :: Strategy f -> Strategy f
anywhere :: Strategy f -> Strategy f
anywhere = Strategy f -> Strategy f
forall f. Strategy f -> Strategy f
anywhereOutermost
anywhereOutermost :: Strategy f -> Strategy f
anywhereOutermost :: Strategy f -> Strategy f
anywhereOutermost Strategy f
strat Term f
t = Strategy f -> [Term f] -> [Reduction f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Strategy f
strat (Term f -> [Term f]
forall f. Term f -> [Term f]
subterms Term f
t)
anywhereInnermost :: Strategy f -> Strategy f
anywhereInnermost :: Strategy f -> Strategy f
anywhereInnermost Strategy f
strat Term f
t = Strategy f -> [Term f] -> [Reduction f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Strategy f
strat (Term f -> [Term f]
forall f. Term f -> [Term f]
reverseSubterms Term f
t)
{-# INLINE rewrite #-}
rewrite :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite :: (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite Rule f -> Subst f -> Bool
p Index f a
rules Term f
t = do
a
rule <- Term f -> Index f a -> [a]
forall f a. Term f -> Index f a -> [a]
Index.approxMatches Term f
t Index f a
rules
(Rule f -> Subst f -> Bool) -> a -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> a -> Strategy f
tryRule Rule f -> Subst f -> Bool
p a
rule Term f
t
{-# INLINEABLE tryRule #-}
tryRule :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f
tryRule :: (Rule f -> Subst f -> Bool) -> a -> Strategy f
tryRule Rule f -> Subst f -> Bool
p a
rule Term f
t = do
Subst f
sub <- Maybe (Subst f) -> [Subst f]
forall a. Maybe a -> [a]
maybeToList (Term f -> Term f -> Maybe (Subst f)
forall f. Term f -> Term f -> Maybe (Subst f)
match (Rule f -> Term f
forall f. Rule f -> Term f
lhs (a -> Rule f
forall a b. Has a b => a -> b
the a
rule)) Term f
t)
Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rule f -> Subst f -> Bool
p (a -> Rule f
forall a b. Has a b => a -> b
the a
rule) Subst f
sub)
Reduction f -> [Reduction f]
forall (m :: * -> *) a. Monad m => a -> m a
return [Subst f -> Rule f -> Rule f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub (a -> Rule f
forall a b. Has a b => a -> b
the a
rule)]
{-# INLINEABLE reducesWith #-}
reducesWith :: Function f => (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reducesWith :: (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reducesWith Term f -> Term f -> Bool
_ (Rule Orientation f
Oriented Proof f
_ Term f
_ Term f
_) Subst f
_ = Bool
True
reducesWith Term f -> Term f -> Bool
_ (Rule (WeaklyOriented Fun f
min [Term f]
ts) Proof f
_ Term f
_ Term f
_) Subst f
sub =
(Term f -> Bool) -> [Term f] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (Term f -> Bool) -> Term f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> Bool
isMinimal (Term f -> Bool) -> (Term f -> Term f) -> Term f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> Term f
expand) [Term f]
ts
where
expand :: Term f -> Term f
expand t :: Term f
t@(Var Var
x) = Term f -> Maybe (Term f) -> Term f
forall a. a -> Maybe a -> a
fromMaybe Term f
t (Var -> Subst f -> Maybe (Term f)
forall f. Var -> Subst f -> Maybe (Term f)
Term.lookup Var
x Subst f
sub)
expand Term f
t = Term f
t
isMinimal :: Term f -> Bool
isMinimal (App Fun f
f TermList f
Empty) = Fun f
f Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
min
isMinimal Term f
_ = Bool
False
reducesWith Term f -> Term f -> Bool
p (Rule (Permutative [(Term f, Term f)]
ts) Proof f
_ Term f
_ Term f
_) Subst f
sub =
[(Term f, Term f)] -> Bool
aux [(Term f, Term f)]
ts
where
aux :: [(Term f, Term f)] -> Bool
aux [] = Bool
False
aux ((Term f
t, Term f
u):[(Term f, Term f)]
ts)
| Term f
t' Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
u' = [(Term f, Term f)] -> Bool
aux [(Term f, Term f)]
ts
| Bool
otherwise = Term f -> Term f -> Bool
p Term f
u' Term f
t'
where
t' :: Term f
t' = Subst f -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
t
u' :: Term f
u' = Subst f -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
u
reducesWith Term f -> Term f -> Bool
p (Rule Orientation f
Unoriented Proof f
_ Term f
t Term f
u) Subst f
sub =
Term f
t' Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
/= Term f
u' Bool -> Bool -> Bool
&& Term f -> Term f -> Bool
p Term f
u' Term f
t'
where
t' :: Term f
t' = Subst f -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
t
u' :: Term f
u' = Subst f -> Term f -> Term f
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
u
{-# INLINEABLE reduces #-}
reduces :: Function f => Rule f -> Subst f -> Bool
reduces :: Rule f -> Subst f -> Bool
reduces Rule f
rule Subst f
sub = (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
forall f.
Function f =>
(Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reducesWith Term f -> Term f -> Bool
forall f. Ordered f => Term f -> Term f -> Bool
lessEq Rule f
rule Subst f
sub
{-# INLINEABLE reducesOriented #-}
reducesOriented :: Function f => Rule f -> Subst f -> Bool
reducesOriented :: Rule f -> Subst f -> Bool
reducesOriented Rule f
rule Subst f
sub =
Orientation f -> Bool
forall f. Orientation f -> Bool
oriented (Rule f -> Orientation f
forall f. Rule f -> Orientation f
orientation Rule f
rule) Bool -> Bool -> Bool
&& (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
forall f.
Function f =>
(Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reducesWith Term f -> Term f -> Bool
forall a. HasCallStack => a
undefined Rule f
rule Subst f
sub
{-# INLINEABLE reducesInModel #-}
reducesInModel :: Function f => Model f -> Rule f -> Subst f -> Bool
reducesInModel :: Model f -> Rule f -> Subst f -> Bool
reducesInModel Model f
cond Rule f
rule Subst f
sub =
(Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
forall f.
Function f =>
(Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reducesWith (\Term f
t Term f
u -> Maybe Strictness -> Bool
forall a. Maybe a -> Bool
isJust (Model f -> Term f -> Term f -> Maybe Strictness
forall f.
Ordered f =>
Model f -> Term f -> Term f -> Maybe Strictness
lessIn Model f
cond Term f
t Term f
u)) Rule f
rule Subst f
sub
{-# INLINEABLE reducesSkolem #-}
reducesSkolem :: Function f => Rule f -> Subst f -> Bool
reducesSkolem :: Rule f -> Subst f -> Bool
reducesSkolem Rule f
rule Subst f
sub =
(Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
forall f.
Function f =>
(Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reducesWith (\Term f
t Term f
u -> Term f -> Term f -> Bool
forall f. Ordered f => Term f -> Term f -> Bool
lessEqSkolem Term f
t Term f
u) Rule f
rule Subst f
sub