summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNickSmallbone <>2021-04-07 14:51:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2021-04-07 14:51:00 (GMT)
commit02af902dd429324802f6da11702159bacfedc0e9 (patch)
tree2475ccce7ad7f02680a64142a003d059649b327e
parent3871ea7ea0c1377229b8b46041a6ee10cf444812 (diff)
version 2.3.1HEAD2.3.1master
-rw-r--r--Twee.hs7
-rw-r--r--Twee/CP.hs2
-rw-r--r--Twee/Constraints.hs8
-rw-r--r--Twee/Equation.hs2
-rw-r--r--Twee/Pretty.hs10
-rw-r--r--Twee/Proof.hs16
-rw-r--r--Twee/Rule.hs34
-rw-r--r--Twee/Term.hs25
-rw-r--r--Twee/Term/Core.hs14
-rw-r--r--twee-lib.cabal2
10 files changed, 88 insertions, 32 deletions
diff --git a/Twee.hs b/Twee.hs
index 1cfa44e..1051d05 100644
--- a/Twee.hs
+++ b/Twee.hs
@@ -549,6 +549,13 @@ checkCompleteness _config state =
rules = map rule_rule (filter ok (IntMap.elems (st_rule_ids state)))
ok r = unMax (rule_max r) `IntSet.disjoint` excluded
+-- Assume that all rules form a confluent rewrite system.
+{-# INLINEABLE assumeComplete #-}
+assumeComplete :: Function f => State f -> State f
+assumeComplete state =
+ state { st_not_complete = IntSet.empty,
+ st_complete = Index.fromListWith lhs (map rule_rule (IntMap.elems (st_rule_ids state))) }
+
-- For goal terms we store the set of all their normal forms.
-- Name and number are for information only.
data Goal f =
diff --git a/Twee/CP.hs b/Twee/CP.hs
index b99ff13..476fe8d 100644
--- a/Twee/CP.hs
+++ b/Twee/CP.hs
@@ -229,7 +229,7 @@ instance Symbolic (CriticalPair f) where
cp_top = subst_ sub cp_top,
cp_proof = subst_ sub cp_proof }
-instance PrettyTerm f => Pretty (CriticalPair f) where
+instance (Labelled f, PrettyTerm f) => Pretty (CriticalPair f) where
pPrint CriticalPair{..} =
vcat [
pPrint cp_eqn,
diff --git a/Twee/Constraints.hs b/Twee/Constraints.hs
index d212656..7834514 100644
--- a/Twee/Constraints.hs
+++ b/Twee/Constraints.hs
@@ -35,7 +35,7 @@ fromTerm (App f Empty) = Just (Constant f)
fromTerm (Var x) = Just (Variable x)
fromTerm _ = Nothing
-instance PrettyTerm f => Pretty (Atom f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Atom f) where
pPrint = pPrint . toTerm
data Formula f =
@@ -45,7 +45,7 @@ data Formula f =
| Or [Formula f]
deriving (Eq, Ord, Show)
-instance PrettyTerm f => Pretty (Formula f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Formula f) where
pPrintPrec _ _ (Less t u) = hang (pPrint t <+> text "<") 2 (pPrint u)
pPrintPrec _ _ (LessEq t u) = hang (pPrint t <+> text "<=") 2 (pPrint u)
pPrintPrec _ _ (And []) = text "true"
@@ -103,7 +103,7 @@ data Branch f =
equals :: [(Atom f, Atom f)] } -- sorted, greatest atom first in each pair
deriving (Eq, Ord)
-instance PrettyTerm f => Pretty (Branch f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Branch f) where
pPrint Branch{..} =
braces $ fsep $ punctuate (text ",") $
[pPrint x <+> text "<" <+> pPrint y | (x, y) <- less ] ++
@@ -189,7 +189,7 @@ newtype Model f = Model (Map (Atom f) (Int, Int))
-- x < y if major x < major y
-- x <= y if major x = major y and minor x < minor y
-instance PrettyTerm f => Pretty (Model f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Model f) where
pPrint (Model m)
| Map.size m <= 1 = text "empty"
| otherwise = fsep (go (sortBy (comparing snd) (Map.toList m)))
diff --git a/Twee/Equation.hs b/Twee/Equation.hs
index 4eb7715..c6aca7d 100644
--- a/Twee/Equation.hs
+++ b/Twee/Equation.hs
@@ -21,7 +21,7 @@ instance Symbolic (Equation f) where
termsDL (t :=: u) = termsDL t `mplus` termsDL u
subst_ sub (t :=: u) = subst_ sub t :=: subst_ sub u
-instance PrettyTerm f => Pretty (Equation f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Equation f) where
pPrint (x :=: y) = pPrint x <+> text "=" <+> pPrint y
-- | Order an equation roughly left-to-right.
diff --git a/Twee/Pretty.hs b/Twee/Pretty.hs
index 4910537..fc7f513 100644
--- a/Twee/Pretty.hs
+++ b/Twee/Pretty.hs
@@ -72,7 +72,7 @@ supply names =
instance (Pretty f, Labelled f) => Pretty (Fun f) where
pPrintPrec l p = pPrintPrec l p . fun_value
-instance PrettyTerm f => Pretty (Term f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Term f) where
pPrintPrec l p (Var x) = pPrintPrec l p x
pPrintPrec l p (App f xs) =
pPrintTerm (termStyle (fun_value f)) l p (pPrint f) (unpack xs)
@@ -94,7 +94,7 @@ maybeHighlight :: [ANSICode] -> Maybe [Int] -> Doc -> Doc
maybeHighlight cs (Just []) d = highlight cs d
maybeHighlight _ _ d = d
-instance PrettyTerm f => Pretty (HighlightedTerm f) where
+instance (Labelled f, PrettyTerm f) => Pretty (HighlightedTerm f) where
pPrintPrec l p (HighlightedTerm cs h (Var x)) =
maybeHighlight cs h (pPrintPrec l p x)
pPrintPrec l p (HighlightedTerm cs h (App f xs)) =
@@ -107,10 +107,10 @@ instance PrettyTerm f => Pretty (HighlightedTerm f) where
Just (n:ns) | i == n -> HighlightedTerm cs (Just ns) t
_ -> HighlightedTerm cs Nothing t
-instance PrettyTerm f => Pretty (TermList f) where
+instance (Labelled f, PrettyTerm f) => Pretty (TermList f) where
pPrintPrec _ _ = pPrint . unpack
-instance PrettyTerm f => Pretty (Subst f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Subst f) where
pPrint sub = text "{" <#> fsep (punctuate (text ",") docs) <#> text "}"
where
docs =
@@ -118,7 +118,7 @@ instance PrettyTerm f => Pretty (Subst f) where
| (x, t) <- substToList sub ]
-- | A class for customising the printing of function symbols.
-class (Pretty f, Labelled f) => PrettyTerm f where
+class Pretty f => PrettyTerm f where
-- | The style of the function symbol. Defaults to 'curried'.
termStyle :: f -> TermStyle
termStyle _ = curried
diff --git a/Twee/Proof.hs b/Twee/Proof.hs
index f91cb72..b26e6ef 100644
--- a/Twee/Proof.hs
+++ b/Twee/Proof.hs
@@ -86,7 +86,7 @@ data Axiom f =
-- This is the trusted core of the module.
{-# INLINEABLE certify #-}
{-# SCC certify #-}
-certify :: PrettyTerm f => Derivation f -> Proof f
+certify :: Function f => Derivation f -> Proof f
certify p =
case check p of
Nothing -> error ("Invalid proof created!\n" ++ prettyShow p)
@@ -146,7 +146,7 @@ instance Symbolic (Derivation f) where
instance Function f => Pretty (Proof f) where
pPrint = pPrintLemma defaultConfig (prettyShow . axiom_number) (prettyShow . equation)
-instance PrettyTerm f => Pretty (Derivation f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Derivation f) where
pPrint (UseLemma lemma sub) =
text "subst" <#> pPrintTuple [text "lemma" <+> pPrint (equation lemma), pPrint sub]
pPrint (UseAxiom axiom sub) =
@@ -160,12 +160,12 @@ instance PrettyTerm f => Pretty (Derivation f) where
pPrint (Cong f ps) =
text "cong" <#> pPrintTuple (pPrint f:map pPrint ps)
-instance PrettyTerm f => Pretty (Axiom f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Axiom f) where
pPrint Axiom{..} =
text "axiom" <#>
pPrintTuple [pPrint axiom_number, text axiom_name, pPrint axiom_eqn]
-foldLemmas :: PrettyTerm f => (Map (Proof f) a -> Derivation f -> a) -> [Derivation f] -> Map (Proof f) a
+foldLemmas :: (Labelled f, PrettyTerm f) => (Map (Proof f) a -> Derivation f -> a) -> [Derivation f] -> Map (Proof f) a
foldLemmas op ds =
execState (mapM_ foldGoal ds) Map.empty
where
@@ -190,7 +190,7 @@ mapLemmas f ds = map (derivation . op lem) ds
op lem = certify . f . unfoldLemmas (\pf -> Just (simpleLemma (lem Map.! pf)))
lem = foldLemmas op ds
-allLemmas :: PrettyTerm f => [Derivation f] -> [Proof f]
+allLemmas :: Function f => [Derivation f] -> [Proof f]
allLemmas ds =
reverse [p | (_, p, _) <- map vertex (topSort graph)]
where
@@ -215,7 +215,7 @@ unfoldLemmas _ p = p
lemma :: Proof f -> Subst f -> Derivation f
lemma p sub = UseLemma p sub
-simpleLemma :: PrettyTerm f => Proof f -> Derivation f
+simpleLemma :: Function f => Proof f -> Derivation f
simpleLemma p =
UseLemma p (autoSubst (equation p))
@@ -270,7 +270,7 @@ flattenDerivation p =
-- * Trans is right-associated
-- * Each Cong has at least one non-Refl argument
-- * Refl is not used unnecessarily
-simplify :: PrettyTerm f => Derivation f -> Derivation f
+simplify :: Function f => Derivation f -> Derivation f
simplify (Symm p) = symm (simplify p)
simplify (Trans p q) = trans (simplify p) (simplify q)
simplify (Cong f ps) = cong f (map simplify ps)
@@ -851,7 +851,7 @@ pPrintPresentation config (Presentation axioms lemmas goals) =
--
-- Used both here and in the main file.
describeEquation ::
- PrettyTerm f =>
+ Function f =>
String -> String -> Maybe String -> Equation f -> Doc
describeEquation kind num mname eqn =
text kind <+> text num <#>
diff --git a/Twee/Rule.hs b/Twee/Rule.hs
index 0f4e14c..a9d81c7 100644
--- a/Twee/Rule.hs
+++ b/Twee/Rule.hs
@@ -109,7 +109,7 @@ instance Symbolic (Orientation f) where
subst_ sub (Permutative ts) = Permutative (subst_ sub ts)
subst_ _ Unoriented = Unoriented
-instance PrettyTerm f => Pretty (Rule f) where
+instance (Labelled f, PrettyTerm f) => Pretty (Rule f) where
pPrint (Rule or _ l r) =
pPrint l <+> text (showOrientation or) <+> pPrint r
where
@@ -188,7 +188,11 @@ backwards (Rule or pf t u) = Rule (back or) pf u t
{-# INLINEABLE simplify #-}
{-# SCC simplify #-}
simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
-simplify !idx !t
+simplify = 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 !idx !t
| t == u = t
| otherwise = simplify idx u
where
@@ -202,6 +206,18 @@ simplify !idx !t
simp (Cons (App f ts) us) =
app f (simp ts) `mappend` simp 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 !idx !t = simp t
+ where
+ simp t =
+ case [rw | u <- reverseSubterms t, Just rw <- [simpleRewrite idx u]] of
+ [] -> t
+ (rule, sub):_ ->
+ let l = build (Term.subst sub (lhs rule))
+ r = build (Term.subst sub (rhs rule))
+ in simp (build (replace l r (singleton t)))
+
-- | Find a simplification step that applies to a term.
{-# INLINEABLE simpleRewrite #-}
{-# SCC simpleRewrite #-}
@@ -242,7 +258,7 @@ result t (r:rs) = ruleResult u r
u = result t rs
-- | Turn a reduction into a proof.
-reductionProof :: PrettyTerm f => Term f -> Reduction f -> Derivation f
+reductionProof :: Function f => Term f -> Reduction f -> Derivation f
reductionProof t ps = red t (Proof.Refl t) (reverse ps)
where
red _ p [] = p
@@ -253,7 +269,7 @@ reductionProof t ps = red t (Proof.Refl t) (reverse ps)
ruleResult :: Term f -> Rule f -> Term f
ruleResult t r = build (replace (lhs r) (rhs r) (singleton t))
-ruleProof :: PrettyTerm f => Term f -> Rule f -> Derivation f
+ruleProof :: Function f => Term f -> Rule f -> Derivation f
ruleProof t r@(Rule _ _ lhs _)
| t == lhs = ruleDerivation r
| len t < len lhs = Proof.Refl t
@@ -316,7 +332,15 @@ successorsAndNormalForms strat ps =
-- | Apply a strategy anywhere in a term.
anywhere :: Strategy f -> Strategy f
-anywhere strat t = concatMap strat (subterms t)
+anywhere = anywhereOutermost
+
+-- | Apply a strategy anywhere in a term, preferring outermost reductions.
+anywhereOutermost :: Strategy f -> Strategy f
+anywhereOutermost strat t = concatMap strat (subterms t)
+
+-- | Apply a strategy anywhere in a term, preferring innermost reductions.
+anywhereInnermost :: Strategy f -> Strategy f
+anywhereInnermost strat t = concatMap strat (reverseSubterms t)
--------------------------------------------------------------------------------
-- * Basic strategies. These only apply at the root of the term.
diff --git a/Twee/Term.hs b/Twee/Term.hs
index 6b77305..1065b9e 100644
--- a/Twee/Term.hs
+++ b/Twee/Term.hs
@@ -26,14 +26,14 @@ module Twee.Term(
pattern UnsafeCons, pattern UnsafeConsSym, uhd, utl, urest,
empty, unpack, lenList,
-- * Function symbols and variables
- Fun, fun, fun_id, fun_value, pattern F, Var(..), Labelled(..),
+ Fun, fun, fun_id, fun_value, pattern F, Var(..), Labelled(..), AutoLabel(..),
-- * Building terms
Build(..),
Builder,
build, buildList,
con, app, var,
-- * Access to subterms
- children, properSubterms, subtermsList, subterms, occurs, isSubtermOf, isSubtermOfList, at,
+ children, properSubterms, subtermsList, subterms, reverseSubtermsList, reverseSubterms, occurs, isSubtermOf, isSubtermOfList, at,
-- * Substitutions
Substitution(..),
subst,
@@ -75,6 +75,8 @@ import Data.IntMap.Strict(IntMap)
import qualified Data.IntMap.Strict as IntMap
import Control.Arrow((&&&))
import Twee.Utils
+import qualified Twee.Label as Label
+import Data.Typeable
--------------------------------------------------------------------------------
-- * A type class for builders
@@ -596,6 +598,18 @@ subtermsList t = unfoldr op t
subterms :: Term f -> [Term f]
subterms = subtermsList . singleton
+-- | Find all subterms of a term, but in reverse order.
+{-# INLINE reverseSubtermsList #-}
+reverseSubtermsList :: TermList f -> [Term f]
+reverseSubtermsList t =
+ [ unsafeAt n t | n <- [k-1,k-2..0] ]
+ where
+ k = lenList t
+
+{-# INLINE reverseSubterms #-}
+reverseSubterms :: Term f -> [Term f]
+reverseSubterms t = reverseSubtermsList (singleton t)
+
-- | Find all proper subterms of a term.
{-# INLINE properSubterms #-}
properSubterms :: Term f -> [Term f]
@@ -640,6 +654,7 @@ replace :: (Build a, BuildFun a ~ f) => Term f -> a -> TermList f -> Builder f
replace !_ !_ Empty = mempty
replace t u (Cons v vs)
| t == v = builder u `mappend` replace t u vs
+ | len v < len t = builder v `mappend` replace t u vs
| otherwise =
case v of
Var x -> var x `mappend` replace t u vs
@@ -709,6 +724,12 @@ class Labelled f where
instance (Labelled f, Show f) => Show (Fun f) where show = show . fun_value
+-- | For "deriving via": a Labelled instance which uses Twee.Label.
+newtype AutoLabel a = AutoLabel { unAutoLabel :: a }
+instance (Ord a, Typeable a) => Labelled (AutoLabel a) where
+ label = fromIntegral . Label.labelNum . Label.label . unAutoLabel
+ find = AutoLabel . Label.find . Label.unsafeMkLabel . fromIntegral
+
-- | A pattern which extracts the 'fun_value' from a 'Fun'.
pattern F :: Labelled f => Int -> f -> Fun f
pattern F x y <- (fun_id &&& fun_value -> (x, y))
diff --git a/Twee/Term/Core.hs b/Twee/Term/Core.hs
index 02db1ed..019c274 100644
--- a/Twee/Term/Core.hs
+++ b/Twee/Term/Core.hs
@@ -79,11 +79,15 @@ data TermList f =
-- | Index into a termlist.
at :: Int -> TermList f -> Term f
-at n (TermList lo hi arr)
- | n < 0 || lo+n >= hi = error "term index out of bounds"
- | otherwise =
- case TermList (lo+n) hi arr of
- UnsafeCons t _ -> t
+at n t
+ | n < 0 || low t + n >= high t = error "term index out of bounds"
+ | otherwise = unsafeAt n t
+
+-- | Index into a termlist, without bounds checking.
+unsafeAt :: Int -> TermList f -> Term f
+unsafeAt n (TermList lo hi arr) =
+ case TermList (lo+n) hi arr of
+ UnsafeCons t _ -> t
{-# INLINE lenList #-}
-- | The length of (number of symbols in) a termlist.
diff --git a/twee-lib.cabal b/twee-lib.cabal
index f18f64a..d0ac0db 100644
--- a/twee-lib.cabal
+++ b/twee-lib.cabal
@@ -1,5 +1,5 @@
name: twee-lib
-version: 2.3
+version: 2.3.1
synopsis: An equational theorem prover
homepage: http://github.com/nick8325/twee
license: BSD3