packages feed

twee-lib 2.1.4 → 2.1.5

raw patch · 10 files changed

+48/−52 lines, 10 filesdep ~base

Dependency ranges changed: base

Files

Twee.hs view
@@ -122,7 +122,7 @@   pPrint (NewEquation eqn) =     text "  (hard)" <+> pPrint eqn   pPrint (DeleteActive rule) =-    text "  (delete rule " <> pPrint (active_id rule) <> text ")"+    text "  (delete rule " <#> pPrint (active_id rule) <#> text ")"   pPrint SimplifyQueue =     text "  (simplifying queued critical pairs...)"   pPrint Interreduce =@@ -293,7 +293,7 @@  instance Function f => Pretty (Active f) where   pPrint Active{..} =-    pPrint active_id <> text "." <+> pPrint (canonicalise active_rule)+    pPrint active_id <#> text "." <+> pPrint (canonicalise active_rule)  instance Has (ActiveRule f) Id where the = rule_active instance Has (ActiveRule f) RuleId where the = rule_rid
Twee/Base.hs view
@@ -254,7 +254,7 @@  instance Pretty f => Pretty (Extended f) where   pPrintPrec _ _ Minimal = text "?"-  pPrintPrec _ _ (Skolem (V n)) = text "sk" <> pPrint n+  pPrintPrec _ _ (Skolem (V n)) = text "sk" <#> pPrint n   pPrintPrec l p (Function f) = pPrintPrec l p f  instance PrettyTerm f => PrettyTerm (Extended f) where
Twee/Join.hs view
@@ -81,7 +81,10 @@     case cp_top cp of       Just top ->         case (join (cp, top), join (flipCP (cp, top))) of-          (Just _, Just _) -> Just cp+          (Just cp1, Just cp2) ->+            case simplerThan (cp_eqn cp1) (cp_eqn cp2) of+              True -> Just cp1+              False -> Just cp2           _ -> Nothing       _ -> Just cp   where
Twee/Pretty.hs view
@@ -3,7 +3,7 @@ {-# LANGUAGE Rank2Types #-} module Twee.Pretty(module Twee.Pretty, module Text.PrettyPrint.HughesPJClass, Pretty(..)) where -import Text.PrettyPrint.HughesPJClass hiding (empty)+import Text.PrettyPrint.HughesPJClass hiding (empty, (<>)) import qualified Text.PrettyPrint.HughesPJClass as PP import qualified Data.Map as Map import Data.Map(Map)@@ -18,6 +18,12 @@ prettyPrint :: Pretty a => a -> IO () prettyPrint x = putStrLn (prettyShow x) +-- | Put one document beside another, i.e., 'PP.<>'.+-- Renamed here because (a different) '<>' is exported by "Prelude".+infixl 6 <#>+(<#>) :: Doc -> Doc -> Doc+(<#>) = (PP.<>)+ -- | The empty document. Used to avoid name clashes with 'Twee.Term.empty'. pPrintEmpty :: Doc pPrintEmpty = PP.empty@@ -53,7 +59,7 @@ instance (Eq a, Integral a, Pretty a) => Pretty (Ratio a) where   pPrint a     | denominator a == 1 = pPrint (numerator a)-    | otherwise = text "(" <+> pPrint (numerator a) <> text "/" <> pPrint (denominator a) <+> text ")"+    | otherwise = text "(" <+> pPrint (numerator a) <#> text "/" <#> pPrint (denominator a) <+> text ")"  -- | Generate a list of candidate names for pretty-printing. supply :: [String] -> [String]@@ -78,7 +84,7 @@   pPrintPrec _ _ = pPrint . unpack  instance PrettyTerm f => Pretty (Subst f) where-  pPrint sub = text "{" <> fsep (punctuate (text ",") docs) <> text "}"+  pPrint sub = text "{" <#> fsep (punctuate (text ",") docs) <#> text "}"     where       docs =         [ hang (pPrint x <+> text "->") 2 (pPrint t)@@ -130,7 +136,7 @@     let       f [] = d       f xs =-        d <> parens (hsep (punctuate comma (map (pPrintPrec l 0) xs)))+        d <#> parens (hsep (punctuate comma (map (pPrintPrec l 0) xs)))     in f  -- | A helper function that deals with under- and oversaturated applications.@@ -158,13 +164,13 @@ prefix =   fixedArity 1 $   TermStyle $ \l _ d [x] ->-    d <> pPrintPrec l 11 x+    d <#> pPrintPrec l 11 x  -- | For postfix operators. postfix =   fixedArity 1 $   TermStyle $ \l _ d [x] ->-    pPrintPrec l 11 x <> d+    pPrintPrec l 11 x <#> d  -- | For infix operators. infixStyle :: Int -> TermStyle
Twee/Proof.hs view
@@ -117,7 +117,10 @@  ---------------------------------------------------------------------- -- Everything below this point need not be trusted, since all proof--- construction goes through the "proof" function.+-- construction goes through the "certify" function.+--+-- N.B.: For this reason, the code below must never directly invoke+-- the Proof constructor! ----------------------------------------------------------------------  -- Typeclass instances.@@ -150,26 +153,26 @@   pPrint = pPrintLemma defaultConfig prettyShow instance PrettyTerm f => Pretty (Derivation f) where   pPrint (UseLemma lemma sub) =-    text "subst" <> pPrintTuple [pPrint lemma, pPrint sub]+    text "subst" <#> pPrintTuple [pPrint lemma, pPrint sub]   pPrint (UseAxiom axiom sub) =-    text "subst" <> pPrintTuple [pPrint axiom, pPrint sub]+    text "subst" <#> pPrintTuple [pPrint axiom, pPrint sub]   pPrint (Refl t) =-    text "refl" <> pPrintTuple [pPrint t]+    text "refl" <#> pPrintTuple [pPrint t]   pPrint (Symm p) =-    text "symm" <> pPrintTuple [pPrint p]+    text "symm" <#> pPrintTuple [pPrint p]   pPrint (Trans p q) =-    text "trans" <> pPrintTuple [pPrint p, pPrint q]+    text "trans" <#> pPrintTuple [pPrint p, pPrint q]   pPrint (Cong f ps) =-    text "cong" <> pPrintTuple (pPrint f:map pPrint ps)+    text "cong" <#> pPrintTuple (pPrint f:map pPrint ps)  instance PrettyTerm f => Pretty (Axiom f) where   pPrint Axiom{..} =-    text "axiom" <>+    text "axiom" <#>     pPrintTuple [pPrint axiom_number, text axiom_name, pPrint axiom_eqn]  instance PrettyTerm f => Pretty (Lemma f) where   pPrint Lemma{..} =-    text "lemma" <>+    text "lemma" <#>     pPrintTuple [pPrint lemma_id, pPrint (equation lemma_proof)]  -- | Simplify a derivation.@@ -353,7 +356,7 @@     error $ show $       text "Invalid ProvedGoal!" $$       text "Claims to prove" <+> pPrint pg_goal_hint $$-      text "with witness" <+> pPrint pg_witness_hint <> text "," $$+      text "with witness" <+> pPrint pg_witness_hint <#> text "," $$       text "but actually proves" <+> pPrint (equation pg_proof)  instance Function f => Pretty (Presentation f) where@@ -484,7 +487,7 @@        text "}" $$        ppTerm (eqn_rhs (equation (certify p)))) -    ppTerm t = text "  " <> pPrint t+    ppTerm t = text "  " <#> pPrint t      ppStep [] = text "reflexivity" -- ??     ppStep [x] = text x@@ -494,13 +497,13 @@       text (last xs)      ppLemma (Lemma{..}, sub) =-      text "lemma" <+> text (lemmaName lemma_id) <> showSubst sub+      text "lemma" <+> text (lemmaName lemma_id) <#> showSubst sub     ppAxiom (Axiom{..}, sub) =-      text "axiom" <+> pPrint axiom_number <+> parens (text axiom_name) <> showSubst sub+      text "axiom" <+> pPrint axiom_number <+> parens (text axiom_name) <#> showSubst sub      showSubst sub       | cfg_show_instances && not (null (substToList sub)) =-        text " with " <>+        text " with " <#>         fsep (punctuate comma           [ pPrint x <+> text "->" <+> pPrint t           | (x, t) <- substToList sub ])@@ -612,11 +615,11 @@   PrettyTerm f =>   String -> String -> Maybe String -> Equation f -> Doc describeEquation kind num mname eqn =-  text kind <+> text num <>+  text kind <+> text num <#>   (case mname of      Nothing -> text ""-     Just name -> text (" (" ++ name ++ ")")) <>-  text ":" <+> pPrint eqn <> text "."+     Just name -> text (" (" ++ name ++ ")")) <#>+  text ":" <+> pPrint eqn <#> text "."  ---------------------------------------------------------------------- -- Making proofs of existential goals more readable.
Twee/Rule.hs view
@@ -489,4 +489,6 @@   reducesWith (\t u -> lessEq (subst skolemise t) (subst skolemise u)) rule sub   where     skolemise (V x) = con (skolem (V (x + k)))+    -- Make sure the Skolem constants we choose don't overlap with any+    -- already in the rule     V k = maximum (V 0:map succ (catMaybes (map getSkolem (funs rule))))
Twee/Term.hs view
@@ -62,7 +62,7 @@ import Twee.Term.Core hiding (F) import Data.List hiding (lookup, find) import Data.Maybe-import Data.Monoid+import Data.Semigroup(Semigroup(..)) import Data.IntMap.Strict(IntMap) import qualified Data.IntMap.Strict as IntMap
Twee/Term/Core.hs view
@@ -21,6 +21,7 @@ import Data.Ord import Twee.Label import Data.Typeable+import Data.Semigroup(Semigroup(..))  -------------------------------------------------------------------------------- -- Symbols. A symbol is a single function or variable in a flatterm.@@ -281,11 +282,14 @@  type Builder1 s f = State# s -> MutableByteArray# s -> Int# -> Int# -> (# State# s, Int# #) +instance Semigroup (Builder f) where+  {-# INLINE (<>) #-}+  Builder m1 <> Builder m2 = Builder (m1 `then_` m2) instance Monoid (Builder f) where   {-# INLINE mempty #-}   mempty = Builder built   {-# INLINE mappend #-}-  Builder m1 `mappend` Builder m2 = Builder (m1 `then_` m2)+  mappend = (<>)  -- Build a termlist from a Builder. -- Works by guessing an appropriate size, and retrying if that was too small.
Twee/Utils.hs view
@@ -58,28 +58,6 @@     (hSetBuffering stdout buf)     x -newtype Max a = Max { getMax :: Maybe a }--getMaxWith :: Ord a => a -> Max a -> a-getMaxWith x (Max (Just y)) = x `max` y-getMaxWith x (Max Nothing)  = x--instance Ord a => Monoid (Max a) where-  mempty = Max Nothing-  Max (Just x) `mappend` y = Max (Just (getMaxWith x y))-  Max Nothing  `mappend` y = y--newtype Min a = Min { getMin :: Maybe a }--getMinWith :: Ord a => a -> Min a -> a-getMinWith x (Min (Just y)) = x `min` y-getMinWith x (Min Nothing)  = x--instance Ord a => Monoid (Min a) where-  mempty = Min Nothing-  Min (Just x) `mappend` y = Min (Just (getMinWith x y))-  Min Nothing  `mappend` y = y- labelM :: Monad m => (a -> m b) -> [a] -> m [(a, b)] labelM f = mapM (\x -> do { y <- f x; return (x, y) })
twee-lib.cabal view
@@ -1,5 +1,5 @@ name:                twee-lib-version:             2.1.4+version:             2.1.5 synopsis:            An equational theorem prover homepage:            http://github.com/nick8325/twee license:             BSD3