packages feed

twee-lib 2.3 → 2.3.1

raw patch · 10 files changed

+88/−32 lines, 10 files

Files

Twee.hs view
@@ -549,6 +549,13 @@     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 =
Twee/CP.hs view
@@ -229,7 +229,7 @@       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,
Twee/Constraints.hs view
@@ -35,7 +35,7 @@ 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 @@   | 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 @@     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 @@ -- 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)))
Twee/Equation.hs view
@@ -21,7 +21,7 @@   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.
Twee/Pretty.hs view
@@ -72,7 +72,7 @@ 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 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 @@           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 @@         | (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
Twee/Proof.hs view
@@ -86,7 +86,7 @@ -- 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 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 @@   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 @@     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 @@ 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 @@ --   * 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 @@ -- -- 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 <#>
Twee/Rule.hs view
@@ -109,7 +109,7 @@   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 @@ {-# 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 @@     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 @@     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 @@ 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 @@  -- | 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.
Twee/Term.hs view
@@ -26,14 +26,14 @@   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 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 @@ 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 !_ !_ 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@@ -708,6 +723,12 @@   find :: Int -> f  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
Twee/Term/Core.hs view
@@ -79,11 +79,15 @@  -- | 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.
twee-lib.cabal view
@@ -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