-- | Term rewriting.
{-# 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 hiding (singleton)
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

--------------------------------------------------------------------------------
-- * Rewrite rules.
--------------------------------------------------------------------------------

-- | A rewrite rule.
data Rule f =
  Rule {
    -- | Information about whether and how the rule is oriented.
    forall f. Rule f -> Orientation f
orientation :: Orientation f,
    -- Invariant:
    -- For oriented rules: vars rhs `isSubsetOf` vars lhs
    -- For unoriented rules: vars lhs == vars rhs
    
    -- | A proof that the rule holds.
    forall f. Rule f -> Proof f
rule_proof :: !(Proof f),

    -- | The left-hand side of the rule.
    forall f. Rule f -> Term f
lhs :: {-# UNPACK #-} !(Term f),
    -- | The right-hand side of the rule.
    forall f. Rule f -> Term f
rhs :: {-# UNPACK #-} !(Term f) }
  deriving Int -> Rule f -> ShowS
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 = forall a. Ord a => a -> a -> Ordering
compare Rule f
x Rule f
y forall a. Eq a => a -> a -> Bool
== Ordering
EQ
instance Ord (Rule f) where
  compare :: Rule f -> Rule f -> Ordering
compare = forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (\Rule f
rule -> (forall f. Rule f -> Term f
lhs Rule f
rule, forall f. Rule f -> Term f
rhs Rule f
rule))
instance f ~ g => Has (Rule f) (Rule g) where
  the :: Rule f -> Rule g
the = forall a. a -> a
id
type RuleOf a = Rule (ConstantOf a)

ruleDerivation :: Rule f -> Derivation f
ruleDerivation :: forall f. Rule f -> Derivation f
ruleDerivation Rule f
r =
  case (forall f. Equation f -> Equation f -> Maybe (Subst f)
matchEquation (forall f. Proof f -> Equation f
Proof.equation (forall f. Rule f -> Proof f
rule_proof Rule f
r)) (forall f. Rule f -> Term f
lhs Rule f
r forall f. Term f -> Term f -> Equation f
:=: forall f. Rule f -> Term f
rhs Rule f
r),
        forall f. Equation f -> Equation f -> Maybe (Subst f)
matchEquation (forall f. Proof f -> Equation f
Proof.equation (forall f. Rule f -> Proof f
rule_proof Rule f
r)) (forall f. Rule f -> Term f
rhs Rule f
r forall f. Term f -> Term f -> Equation f
:=: forall f. Rule f -> Term f
lhs Rule f
r)) of
    (Just Subst f
sub, Maybe (Subst f)
_) -> forall f. Proof f -> Subst f -> Derivation f
Proof.lemma (forall f. Rule f -> Proof f
rule_proof Rule f
r) Subst f
sub
    (Maybe (Subst f)
_, Just Subst f
sub) -> forall f. Derivation f -> Derivation f
Proof.symm (forall f. Proof f -> Subst f -> Derivation f
Proof.lemma (forall f. Rule f -> Proof f
rule_proof Rule f
r) Subst f
sub)
    (Maybe (Subst f), Maybe (Subst f))
_ -> forall a. HasCallStack => String -> a
error String
"rule out of sync with proof"

-- | A rule's orientation.
--
-- 'Oriented' and 'WeaklyOriented' rules are used only left-to-right.
-- 'Permutative' and 'Unoriented' rules are used bidirectionally.
data Orientation f =
    -- | An oriented rule.
    Oriented
    -- | A weakly oriented rule.
    -- The first argument is the minimal constant, the second argument is a list
    -- of terms which are weakly oriented in the rule.
    -- 
    -- A rule with orientation @'WeaklyOriented' k ts@ can be used unless
    -- all terms in @ts@ are equal to @k@.
  | WeaklyOriented {-# UNPACK #-} !(Fun f) [Term f]
    -- | A permutative rule.
    --
    -- A rule with orientation @'Permutative' ts@ can be used if
    -- @map fst ts@ is lexicographically greater than @map snd ts@.
  | Permutative [(Term f, Term f)]
    -- | An unoriented rule.
  | Unoriented
  deriving Int -> Orientation f -> ShowS
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

-- | Is a rule oriented or weakly oriented?
oriented :: Orientation f -> Bool
oriented :: forall f. 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
_) = 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) = forall f. Orientation f -> Proof f -> Term f -> Term f -> Rule f
Rule (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Rule f)
sub Orientation f
or) Proof f
pf (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Rule f)
sub Term f
t) (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Rule f)
sub Term f
u)

instance f ~ g => Has (Rule f) (Term g) where
  the :: Rule f -> Term g
the = 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 = forall (m :: * -> *) a. MonadPlus m => m a
mzero
  termsDL (WeaklyOriented Fun f
_ [Term f]
ts) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL [Term f]
ts
  termsDL (Permutative [(Term f, Term f)]
ts) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL [(Term f, Term f)]
ts
  termsDL Orientation f
Unoriented = 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 = forall f. Orientation f
Oriented
  subst_ Var -> BuilderOf (Orientation f)
sub (WeaklyOriented Fun f
min [Term f]
ts) = forall f. Fun f -> [Term f] -> Orientation f
WeaklyOriented Fun f
min (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Orientation f)
sub [Term f]
ts)
  subst_ Var -> BuilderOf (Orientation f)
sub (Permutative [(Term f, Term f)]
ts) = forall f. [(Term f, Term f)] -> Orientation f
Permutative (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Orientation f)
sub [(Term f, Term f)]
ts)
  subst_ Var -> BuilderOf (Orientation f)
_   Orientation f
Unoriented = 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) =
    forall a. Pretty a => a -> Doc
pPrint Term f
l Doc -> Doc -> Doc
<+> String -> Doc
text (forall {a} {f}. IsString a => Orientation f -> a
showOrientation Orientation f
or) Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint Term f
r
    where
      showOrientation :: Orientation f -> a
showOrientation Orientation f
Oriented = a
"->"
      showOrientation WeaklyOriented{} = a
"~>"
      showOrientation Permutative{} = a
"<->"
      showOrientation Orientation f
Unoriented = a
"="

-- | Turn a rule into an equation.
unorient :: Rule f -> Equation f
unorient :: forall f. Rule f -> Equation f
unorient (Rule Orientation f
_ Proof f
_ Term f
l Term f
r) = Term f
l forall f. Term f -> Term f -> Equation f
:=: Term f
r

-- | Turn an equation t :=: u into a rule t -> u by computing the
-- orientation info (e.g. oriented, permutative or unoriented).
--
-- Crashes if either @t < u@, or there is a variable in @u@ which is
-- not in @t@. To avoid this problem, combine with 'Twee.CP.split'.
orient :: Function f => Equation f -> Proof f -> Rule f
orient :: forall f. Function f => Equation f -> Proof f -> Rule f
orient (Term f
t :=: Term f
u) Proof f
pf = 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 | forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
u Term f
t =
        case forall f. Term f -> Term f -> Maybe (Subst f)
unify Term f
t Term f
u of
          Maybe (Subst f)
Nothing -> forall f. Orientation f
Oriented
          Just Subst f
sub
            | forall f. (Var -> TermList f -> Bool) -> Subst f -> Bool
allSubst (\Var
_ (Cons Term f
t TermList f
Empty) -> forall f. Minimal f => Term f -> Bool
isMinimal Term f
t) Subst f
sub ->
              forall f. Fun f -> [Term f] -> Orientation f
WeaklyOriented forall f. Minimal f => Fun f
minimal (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Build a => a -> Term (BuildFun a)
build forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Var -> Builder f
var forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (forall f. Subst f -> [(Var, Term f)]
substToList Subst f
sub))
            | Bool
otherwise -> forall f. Orientation f
Unoriented
      | forall f. Ordered f => Term f -> Term f -> Bool
lessEq Term f
t Term f
u = forall a. HasCallStack => String -> a
error String
"wrongly-oriented rule"
      | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. Ord a => [a] -> [a]
usort (forall a. Symbolic a => a -> [Var]
vars Term f
u) forall a. Eq a => [a] -> [a] -> [a]
\\ forall a. Ord a => [a] -> [a]
usort (forall a. Symbolic a => a -> [Var]
vars Term f
t))) =
        forall a. HasCallStack => String -> a
error String
"unbound variables in rule"
      | Just [(Term f, Term f)]
ts <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall {f} {f} {f}.
Term f -> Term f -> StateT [(Var, Term f)] Maybe [(Term f, Term f)]
makePermutative Term f
t Term f
u) [],
        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 =
        forall f. [(Term f, Term f)] -> Orientation f
Permutative [(Term f, Term f)]
ts
      | Bool
otherwise = 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) =
      forall f.
Ordered f =>
Model f -> Term f -> Term f -> Maybe Strictness
lessIn Model f
model Term f
u Term f
t forall a. Eq a => a -> a -> Bool
== 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 = forall f. (Minimal f, Ord f) => [Atom f] -> Model f
modelFromOrder [forall f. Var -> Atom f
Variable Var
y, forall f. Var -> Atom f
Variable Var
x]
        sub :: Var -> Builder f
sub Var
x' = if Var
x forall a. Eq a => a -> a -> Bool
== Var
x' then forall f. Var -> Builder f
var Var
y else forall f. Var -> Builder f
var Var
x'
        t' :: Term f
t' = 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' = 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 <- forall (m :: * -> *) s a. Monad m => (s -> a) -> StateT s m a
gets forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst
      Subst f
sub  <- 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 (forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
t) (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 forall a. Eq a => a -> a -> Bool
== Var
y = forall (m :: * -> *) a. Monad m => a -> m a
return []
            | Bool
otherwise = do
              forall (m :: * -> *) s. Monad m => (s -> s) -> StateT s m ()
modify ((Var
x, forall a. Build a => a -> Term (BuildFun a)
build forall a b. (a -> b) -> a -> b
$ forall f. Var -> Builder f
var Var
y)forall a. a -> [a] -> [a]
:)
              forall (m :: * -> *) a. Monad m => a -> m a
return [(forall a. Build a => a -> Term (BuildFun a)
build forall a b. (a -> b) -> a -> b
$ forall f. Var -> Builder f
var Var
x, forall a. Build a => a -> Term (BuildFun a)
build forall a b. (a -> b) -> a -> b
$ 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 forall a. Eq a => a -> a -> Bool
== Fun f
g =
              forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (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 (forall f. TermList f -> [Term f]
unpack TermList f
ts) (forall f. TermList f -> [Term f]
unpack TermList f
us))

          aux Term f
_ Term f
_ = forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- | Flip an unoriented rule so that it goes right-to-left.
backwards :: Rule f -> Rule f
backwards :: forall f. Rule f -> Rule f
backwards (Rule Orientation f
or Proof f
pf Term f
t Term f
u) = forall f. Orientation f -> Proof f -> Term f -> Term f -> Rule f
Rule (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) = forall f. [(Term f, Term f)] -> Orientation f
Permutative (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> (b, a)
swap [(Term f, Term f)]
xs)
    back Orientation f
Unoriented = forall f. Orientation f
Unoriented
    back Orientation f
_ = forall a. HasCallStack => String -> a
error String
"Can't turn oriented rule backwards"

--------------------------------------------------------------------------------
-- * Extra-fast rewriting, without proof output or unorientable rules.
--------------------------------------------------------------------------------

-- | Compute the normal form of a term wrt only oriented rules.
{-# INLINEABLE simplify #-}
simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
simplify :: forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplify = forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplifyOutermost

-- | Compute the normal form of a term wrt only oriented rules, using outermost reduction.
simplifyOutermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
simplifyOutermost :: forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplifyOutermost !Index f a
idx !Term f
t
  | Term f
t forall a. Eq a => a -> a -> Bool
== Term (BuildFun (Builder f))
u = Term f
t
  | Bool
otherwise = forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplify Index f a
idx Term (BuildFun (Builder f))
u
  where
    u :: Term (BuildFun (Builder f))
u = forall a. Build a => a -> Term (BuildFun a)
build (TermList f -> Builder f
simp (forall f. Term f -> TermList f
singleton Term f
t))

    simp :: TermList f -> Builder f
simp TermList f
Empty = forall a. Monoid a => a
mempty
    simp (Cons (Var Var
x) TermList f
t) = forall f. Var -> Builder f
var Var
x 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) <- 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 =
        forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
Term.subst Subst f
sub (forall f. Rule f -> Term f
rhs Rule f
rule) 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) =
      forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
f (TermList f -> Builder f
simp TermList f
ts) forall a. Monoid a => a -> a -> a
`mappend` TermList f -> Builder f
simp TermList f
us

-- | Compute the normal form of a term wrt only oriented rules, using innermost reduction.
simplifyInnermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
simplifyInnermost :: forall f a.
(Function f, Has a (Rule f)) =>
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 <- forall f. Term f -> [Term f]
reverseSubterms Term f
t, Just (Rule f, Subst f)
rw <- [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 = forall a. Build a => a -> Term (BuildFun a)
build (forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
Term.subst Subst f
sub (forall f. Rule f -> Term f
lhs Rule f
rule))
              r :: Term (BuildFun (Builder f))
r = forall a. Build a => a -> Term (BuildFun a)
build (forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
Term.subst Subst f
sub (forall f. Rule f -> Term f
rhs Rule f
rule))
          in Term f -> Term f
simp (forall a. Build a => a -> Term (BuildFun a)
build (forall a f.
(Build a, BuildFun a ~ f) =>
Term f -> a -> TermList f -> Builder f
replace Term (BuildFun (Builder f))
l Term (BuildFun (Builder f))
r (forall f. Term f -> TermList f
singleton Term f
t)))

-- | Find a simplification step that applies to a term.
{-# INLINEABLE simpleRewrite #-}
simpleRewrite :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Maybe (Rule f, Subst f)
simpleRewrite :: 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 =
  -- Use instead of maybeToList to make fusion work
  forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Rule f, Subst f)
x Maybe (Rule f, Subst f)
_ -> forall a. a -> Maybe a
Just (Rule f, Subst f)
x) forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ do
    (Subst f
sub, a
rule0) <- forall f a. Term f -> Index f a -> [(Subst f, a)]
Index.matches Term f
t Index f a
idx
    let rule :: Rule f
rule = forall a b. Has a b => a -> b
the a
rule0
    forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall f. Orientation f -> Bool
oriented (forall f. Rule f -> Orientation f
orientation Rule f
rule))
    forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall f. Function f => Rule f -> Subst f -> Bool
reducesOriented Rule f
rule Subst f
sub)
    forall (m :: * -> *) a. Monad m => a -> m a
return (Rule f
rule, Subst f
sub)

--------------------------------------------------------------------------------
-- * Rewriting, with proof output.
--------------------------------------------------------------------------------

-- | A strategy gives a set of possible reductions for a term.
type Strategy f = Term f -> [Reduction f]

-- | A reduction proof is just a sequence of rewrite steps, stored
-- as a list in reverse order. In each rewrite step, all subterms that
-- are exactly equal to the LHS of the rule are replaced by the RHS,
-- i.e. the rewrite step is performed as a parallel rewrite without
-- matching.
type Reduction f = [Rule f]

-- | Transitivity for reduction sequences.
trans :: Reduction f -> Reduction f -> Reduction f
trans :: forall f. Reduction f -> Reduction f -> Reduction f
trans Reduction f
p Reduction f
q = Reduction f
q forall a. [a] -> [a] -> [a]
++ Reduction f
p

-- | Compute the final term resulting from a reduction, given the
-- starting term.
result :: Term f -> Reduction f -> Term f
result :: forall f. Term f -> Reduction f -> Term f
result Term f
t [] = Term f
t
result Term f
t (Rule f
r:[Rule f]
rs) = forall f. Term f -> Rule f -> Term f
ruleResult Term f
u Rule f
r
  where
    u :: Term f
u = forall f. Term f -> Reduction f -> Term f
result Term f
t [Rule f]
rs

-- | Turn a reduction into a proof.
reductionProof :: Function f => Term f -> Reduction f -> Derivation f
reductionProof :: forall f. Function f => Term f -> Reduction f -> Derivation f
reductionProof Term f
t Reduction f
ps = forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
Term f -> Derivation f -> [Rule f] -> Derivation f
red Term f
t (forall f. Term f -> Derivation f
Proof.Refl Term f
t) (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 (forall f. Term f -> Rule f -> Term f
ruleResult Term f
t Rule f
q) (Derivation f
p forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans` forall f. Function f => Term f -> Rule f -> Derivation f
ruleProof Term f
t Rule f
q) [Rule f]
qs

-- Helpers for result and reductionProof.
ruleResult :: Term f -> Rule f -> Term f
ruleResult :: forall f. Term f -> Rule f -> Term f
ruleResult Term f
t Rule f
r = forall a. Build a => a -> Term (BuildFun a)
build (forall a f.
(Build a, BuildFun a ~ f) =>
Term f -> a -> TermList f -> Builder f
replace (forall f. Rule f -> Term f
lhs Rule f
r) (forall f. Rule f -> Term f
rhs Rule f
r) (forall f. Term f -> TermList f
singleton Term f
t))

ruleProof :: Function f => Term f -> Rule f -> Derivation f
ruleProof :: forall f. Function f => 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 forall a. Eq a => a -> a -> Bool
== Term f
lhs = forall f. Rule f -> Derivation f
ruleDerivation Rule f
r
  | forall f. Term f -> Int
len Term f
t forall a. Ord a => a -> a -> Bool
< forall f. Term f -> Int
len Term f
lhs = forall f. Term f -> Derivation f
Proof.Refl Term f
t
ruleProof (App Fun f
f TermList f
ts) Rule f
rule =
  forall f. Fun f -> [Derivation f] -> Derivation f
Proof.cong Fun f
f [forall f. Function f => Term f -> Rule f -> Derivation f
ruleProof Term f
u Rule f
rule | Term f
u <- forall f. TermList f -> [Term f]
unpack TermList f
ts]
ruleProof Term f
t Rule f
_ = forall f. Term f -> Derivation f
Proof.Refl Term f
t

--------------------------------------------------------------------------------
-- * Normalisation.
--------------------------------------------------------------------------------

-- | Normalise a term wrt a particular strategy.
{-# INLINE normaliseWith #-}
normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith :: forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith Term f -> Bool
ok Strategy f
strat Term f
t = [Rule f]
res
  where
    res :: [Rule f]
res = Integer -> [Rule f] -> Term f -> [Rule f]
aux Integer
0 [] Term f
t
    aux :: Integer -> [Rule f] -> Term f -> [Rule f]
aux Integer
1000 [Rule f]
p Term f
_ =
      forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
        String
"Possibly nonterminating rewrite:\n" forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow [Rule f]
p
    aux Integer
n [Rule f]
p Term f
t =
      case forall f. Strategy f -> Strategy f
anywhere Strategy f
strat Term f
t of
        ([Rule f]
q:[[Rule f]]
_) | Term f
u <- forall f. Term f -> Reduction f -> Term f
result Term f
t [Rule f]
q, Term f -> Bool
ok Term f
u ->
          Integer -> [Rule f] -> Term f -> [Rule f]
aux (Integer
nforall a. Num a => a -> a -> a
+Integer
1) ([Rule f]
p forall f. Reduction f -> Reduction f -> Reduction f
`trans` [Rule f]
q) Term f
u
        [[Rule f]]
_ -> [Rule f]
p

-- | Compute all normal forms of a set of terms wrt a particular strategy.
normalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
normalForms :: forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
normalForms Strategy f
strat Map (Term f) (Reduction f)
ps = forall a b. (a, b) -> b
snd (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)

-- | Compute all successors of a set of terms (a successor of a term @t@
-- is a term @u@ such that @t ->* u@).
successors :: Function f => Strategy f -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
successors :: forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
successors Strategy f
strat Map (Term f) (Reduction f)
ps =
  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) = 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 #-}
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 :: 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 =
  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 forall k a. Map k a
Map.empty forall k a. Map k a
Map.empty (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 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 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 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
          | 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 (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 (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 (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Term f, (Term f, Reduction f))]
qs 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 =
              [ (forall f. Term f -> Reduction f -> Term f
result Term f
t Reduction f
q, (forall a b. (a, b) -> a
fst (Term f, Reduction f)
p, (forall a b. (a, b) -> b
snd (Term f, Reduction f)
p forall f. Reduction f -> Reduction f -> Reduction f
`trans` Reduction f
q)))
              | Reduction f
q <- forall f. Strategy f -> Strategy f
anywhere Strategy f
strat Term f
t ]

-- | Apply a strategy anywhere in a term.
anywhere :: Strategy f -> Strategy f
anywhere :: forall f. Strategy f -> Strategy f
anywhere = forall f. Strategy f -> Strategy f
anywhereOutermost

-- | Apply a strategy anywhere in a term, preferring outermost reductions.
anywhereOutermost :: Strategy f -> Strategy f
anywhereOutermost :: forall f. Strategy f -> Strategy f
anywhereOutermost Strategy f
strat Term f
t = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Strategy f
strat (forall f. Term f -> [Term f]
subterms Term f
t)

-- | Apply a strategy anywhere in a term, preferring innermost reductions.
anywhereInnermost :: Strategy f -> Strategy f
anywhereInnermost :: forall f. Strategy f -> Strategy f
anywhereInnermost Strategy f
strat Term f
t = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Strategy f
strat (forall f. Term f -> [Term f]
reverseSubterms Term f
t)

--------------------------------------------------------------------------------
-- * Basic strategies. These only apply at the root of the term.
--------------------------------------------------------------------------------

-- | A strategy which rewrites using an index.
{-# INLINE rewrite #-}
rewrite :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite :: forall f a.
(Function f, Has a (Rule f)) =>
(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
  (Subst f
sub, a
rule) <- forall f a. Term f -> Index f a -> [(Subst f, a)]
Index.matches Term f
t Index f a
rules
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rule f -> Subst f -> Bool
p (forall a b. Has a b => a -> b
the a
rule) Subst f
sub)
  forall (m :: * -> *) a. Monad m => a -> m a
return [forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub (forall a b. Has a b => a -> b
the a
rule)]

-- | A strategy which applies one rule only.
{-# INLINEABLE tryRule #-}
tryRule :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f
tryRule :: 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 = do
  Subst f
sub <- forall a. Maybe a -> [a]
maybeToList (forall f. Term f -> Term f -> Maybe (Subst f)
match (forall f. Rule f -> Term f
lhs (forall a b. Has a b => a -> b
the a
rule)) Term f
t)
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Rule f -> Subst f -> Bool
p (forall a b. Has a b => a -> b
the a
rule) Subst f
sub)
  forall (m :: * -> *) a. Monad m => a -> m a
return [forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub (forall a b. Has a b => a -> b
the a
rule)]

-- | Check if a rule can be applied, given an ordering <= on terms.
{-# INLINEABLE reducesWith #-}
reducesWith :: Function f => (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reducesWith :: forall f.
Function f =>
(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 =
  -- Be a bit careful here not to build new terms
  -- (reducesWith is used in simplify).
  -- This is the same as:
  --   any (not . isMinimal) (subst sub ts)
  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> Bool
isMinimal 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) = forall a. a -> Maybe a -> a
fromMaybe Term f
t (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 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' 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' = 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' = 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' 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' = 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' = forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub Term f
u

-- | Check if a rule can be applied normally.
{-# INLINEABLE reduces #-}
reduces :: Function f => Rule f -> Subst f -> Bool
reduces :: forall f. Function f => Rule f -> Subst f -> Bool
reduces Rule f
rule Subst f
sub = forall f.
Function f =>
(Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reducesWith forall f. Ordered f => Term f -> Term f -> Bool
lessEq Rule f
rule Subst f
sub

-- | Check if a rule can be applied and is oriented.
{-# INLINEABLE reducesOriented #-}
reducesOriented :: Function f => Rule f -> Subst f -> Bool
reducesOriented :: forall f. Function f => Rule f -> Subst f -> Bool
reducesOriented Rule f
rule Subst f
sub =
  forall f. Orientation f -> Bool
oriented (forall f. Rule f -> Orientation f
orientation Rule f
rule) Bool -> Bool -> Bool
&& forall f.
Function f =>
(Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reducesWith forall a. HasCallStack => a
undefined Rule f
rule Subst f
sub

-- | Check if a rule can be applied in a particular model.
{-# INLINEABLE reducesInModel #-}
reducesInModel :: Function f => Model f -> Rule f -> Subst f -> Bool
reducesInModel :: forall f. Function f => Model f -> Rule f -> Subst f -> Bool
reducesInModel Model f
cond Rule f
rule Subst f
sub =
  forall f.
Function f =>
(Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reducesWith (\Term f
t Term f
u -> forall a. Maybe a -> Bool
isJust (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

-- | Check if a rule can be applied to the Skolemised version of a term.
{-# INLINEABLE reducesSkolem #-}
reducesSkolem :: Function f => Rule f -> Subst f -> Bool
reducesSkolem :: forall f. Function f => Rule f -> Subst f -> Bool
reducesSkolem Rule f
rule Subst f
sub =
  forall f.
Function f =>
(Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reducesWith (\Term f
t Term f
u -> forall f. Ordered f => Term f -> Term f -> Bool
lessEqSkolem Term f
t Term f
u) Rule f
rule Subst f
sub