twee-lib 2.4.2 → 2.5
raw patch · 11 files changed
+861/−104 lines, 11 filesdep +QuickCheck
Dependencies added: QuickCheck
Files
- Twee.hs +181/−33
- Twee/Base.hs +40/−3
- Twee/CP.hs +4/−5
- Twee/Generate.hs +121/−0
- Twee/Join.hs +2/−2
- Twee/Profile.hs +15/−1
- Twee/Proof.hs +8/−19
- Twee/Rule.hs +466/−29
- Twee/Term.hs +12/−3
- Twee/Term/Core.hs +5/−5
- twee-lib.cabal +7/−4
Twee.hs view
@@ -1,5 +1,5 @@ -- | The main prover loop.-{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies, FlexibleInstances #-}+{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies, FlexibleInstances, RankNTypes, TupleSections #-} module Twee where import Twee.Base@@ -39,6 +39,11 @@ import Data.Ord import Data.PackedSequence(PackedSequence) import qualified Data.PackedSequence as PackedSequence+import Test.QuickCheck.Gen hiding (sample)+import Test.QuickCheck.Random+import Debug.Trace+import Twee.Generate+import qualified System.Random as Random ---------------------------------------------------------------------- -- * Configuration and prover state.@@ -47,23 +52,31 @@ -- | The prover configuration. data Config f = Config {- cfg_accept_term :: Maybe (Term f -> Bool),- cfg_max_critical_pairs :: Int64,- cfg_max_cp_depth :: Int,- cfg_simplify :: Bool,- cfg_renormalise_percent :: Int,- cfg_cp_sample_size :: Int,- cfg_renormalise_threshold :: Int,- cfg_set_join_goals :: Bool,- cfg_always_simplify :: Bool,- cfg_complete_subsets :: Bool,- cfg_critical_pairs :: CP.Config,- cfg_join :: Join.Config,- cfg_proof_presentation :: Proof.Config f }+ cfg_accept_term :: Maybe (Term f -> Bool),+ cfg_max_critical_pairs :: Int64,+ cfg_max_cp_depth :: Int,+ cfg_max_rules :: Int,+ cfg_simplify :: Bool,+ cfg_renormalise_percent :: Int,+ cfg_cp_sample_size :: Int,+ cfg_renormalise_threshold :: Int,+ cfg_set_join_goals :: Bool,+ cfg_always_simplify :: Bool,+ cfg_complete_subsets :: Bool,+ cfg_score_cp :: Depth -> Equation f -> Float,+ cfg_join :: Join.Config,+ cfg_proof_presentation :: Proof.Config f,+ cfg_eliminate_axioms :: [Axiom f],+ cfg_random_mode :: Bool,+ cfg_random_mode_goal_directed :: Bool,+ cfg_random_mode_simple :: Bool,+ cfg_random_mode_best_of :: Int,+ cfg_always_complete :: Bool } -- | The prover state. data State f = State {+ st_axioms :: ![Axiom f], st_rules :: !(RuleIndex f (Rule f)), st_active_set :: !(IntMap (Active f)), st_joinable :: !(Index f (Equation f)),@@ -75,15 +88,18 @@ st_cp_sample :: !(Sample (Maybe (Overlap (Active f) f))), st_not_complete :: !IntSet, st_complete :: !(Index f (Rule f)),- st_messages_rev :: ![Message f] }+ st_messages_rev :: ![Message f],+ st_random_seed :: Maybe QCGen,+ st_problem_term :: Maybe (ConfluenceFailure f) } -- | The default prover configuration.-defaultConfig :: Config f+defaultConfig :: Function f => Config f defaultConfig = Config { cfg_accept_term = Nothing, cfg_max_critical_pairs = maxBound, cfg_max_cp_depth = maxBound,+ cfg_max_rules = maxBound, cfg_simplify = True, cfg_renormalise_percent = 5, cfg_renormalise_threshold = 20,@@ -91,21 +107,29 @@ cfg_set_join_goals = True, cfg_always_simplify = False, cfg_complete_subsets = False,- cfg_critical_pairs = CP.defaultConfig,+ cfg_score_cp = \d eqn -> fromIntegral (score CP.defaultConfig d eqn), cfg_join = Join.defaultConfig,- cfg_proof_presentation = Proof.defaultConfig }+ cfg_proof_presentation = Proof.defaultConfig,+ cfg_eliminate_axioms = [],+ cfg_random_mode = False,+ cfg_random_mode_goal_directed = False,+ cfg_random_mode_best_of = 1,+ cfg_random_mode_simple = False,+ cfg_always_complete = False } -- | Does this configuration run the prover in a complete mode? configIsComplete :: Config f -> Bool configIsComplete Config{..} = isNothing (cfg_accept_term) && cfg_max_critical_pairs == maxBound &&- cfg_max_cp_depth == maxBound+ cfg_max_cp_depth == maxBound &&+ cfg_max_rules == maxBound -- | The initial state. initialState :: Config f -> State f initialState Config{..} = State {+ st_axioms = [], st_rules = RuleIndex.empty, st_active_set = IntMap.empty, st_joinable = Index.empty,@@ -117,7 +141,12 @@ st_cp_sample = emptySample cfg_cp_sample_size, st_not_complete = IntSet.empty, st_complete = Index.empty,- st_messages_rev = [] }+ st_messages_rev = [],+ st_random_seed =+ case cfg_random_mode of+ False -> Nothing+ True -> Just (mkQCGen 12345),+ st_problem_term = Nothing } ---------------------------------------------------------------------- -- * Messages.@@ -139,9 +168,12 @@ | Interreduce -- | Status update: how many queued critical pairs there are. | Status !Int+ -- | New problem term discovered.+ | NewProblemTerm !(ConfluenceFailure f) instance Function f => Pretty (Message f) where pPrint (NewActive rule) = pPrint rule+ -- $$ case cp_top (active_cp rule) of { Just t -> text " (normal forms of term" <+> pPrint t <#> text ")"; Nothing -> pPrintEmpty } pPrint (NewEquation eqn) = text " (hard)" <+> pPrint eqn pPrint (DeleteActive rule) =@@ -158,6 +190,17 @@ text " (simplifying rules with respect to one another...)" pPrint (Status n) = text " (" <#> pPrint n <+> text "queued critical pairs)"+ pPrint (NewProblemTerm cf) =+ text "" $$+ text "Problem term:" <+> pPrint (cf_term cf) $$+ text " NF 1:" $$ ppR (cf_term cf) (cf_left cf) $$+ text " NF 2:" $$ ppR (cf_term cf) (cf_right cf)+ where+ ppR _ [] = pPrintEmpty+ ppR t (rr@(r,_,_):rs) =+ text " -> {by" <+> pPrint r <#> text "}" $$+ text " " <#> pPrint (ruleResult1 t rr) $$+ ppR (ruleResult1 t rr) rs -- | Emit a message. message :: PrettyTerm f => Message f -> State f -> State f@@ -180,6 +223,8 @@ -- | Compute all critical pairs from a rule. {-# INLINEABLE makePassives #-} makePassives :: Function f => Config f -> State f -> Active f -> [Passive]+-- don't generate critical pairs when in random mode+makePassives Config{cfg_random_mode = True} _ _ = [] makePassives config@Config{..} State{..} rule = -- XXX factor out depth calculation stampWith "make critical pair" length@@ -192,7 +237,7 @@ data Passive = Passive {- passive_score :: {-# UNPACK #-} !Int32,+ passive_score :: {-# UNPACK #-} !Float, passive_rule1 :: {-# UNPACK #-} !Id, passive_rule2 :: {-# UNPACK #-} !Id, passive_how :: !How }@@ -212,7 +257,7 @@ batch_kind :: !BatchKind, batch_rule :: {-# UNPACK #-} !Id, batch_best :: {-# UNPACK #-} !Passive,- batch_rest :: {-# UNPACK #-} !(PackedSequence (Int32, Id, How)) }+ batch_rest :: {-# UNPACK #-} !(PackedSequence (Float, Id, How)) } data BatchKind = Rule1 | Rule2 deriving Eq @@ -252,9 +297,9 @@ {-# INLINEABLE makePassive #-} makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive-makePassive Config{..} overlap@Overlap{..} =+makePassive Config{..} Overlap{..} = Passive {- passive_score = fromIntegral (score cfg_critical_pairs depth overlap),+ passive_score = cfg_score_cp depth overlap_eqn, passive_rule1 = active_id overlap_rule1, passive_rule2 = active_id overlap_rule2, passive_how = overlap_how }@@ -280,10 +325,10 @@ let r1 = overlap_rule1 overlap r2 = overlap_rule2 overlap return passive {- passive_score = fromIntegral $- fromIntegral (passive_score passive) `intMin`+ passive_score =+ passive_score passive `min` -- XXX factor out depth calculation- score cfg_critical_pairs (succ (the r1 `max` the r2)) overlap }+ cfg_score_cp (succ (the r1 `max` the r2)) (overlap_eqn overlap) } -- | Check if we should renormalise the queue. {-# INLINEABLE shouldSimplifyQueue #-}@@ -489,8 +534,22 @@ Nothing -> state' Left (cp, model) ->+ generaliseCP cp $ foldl' (\state cp -> addCP config model state info cp) state (split cp) + where+ generaliseCP cp state+ | null cfg_eliminate_axioms = state+ | canonicalise (cp_eqn cp) == canonicalise (cp_eqn cp') = state+ | otherwise =+ consider config{cfg_eliminate_axioms = []} state info cp'+ where+ deriv =+ let d1 = Proof.eliminateDefinitions cfg_eliminate_axioms (cp_proof cp)+ [d2] = fixpointOn (map (equation . certify)) (Proof.generaliseProof False) [d1]+ in d2+ cp' = cp { cp_eqn = equation (certify deriv), cp_proof = deriv }+ {-# INLINEABLE addCP #-} addCP :: Function f => Config f -> Model f -> State f -> Info -> CriticalPair f -> State f addCP config model state@State{..} info CriticalPair{..} =@@ -512,7 +571,7 @@ {-# INLINEABLE addAxiom #-} addAxiom :: Function f => Config f -> State f -> Axiom f -> State f addAxiom config state axiom =- consider config state+ consider config state{st_axioms = axiom:st_axioms state} Info { info_depth = 0, info_max = IntSet.fromList [axiom_number axiom | cfg_complete_subsets config] } CriticalPair { cp_eqn = axiom_eqn axiom,@@ -764,14 +823,103 @@ {-# INLINEABLE complete1 #-} complete1 :: Function f => Config f -> State f -> (Bool, State f) complete1 config@Config{..} state+ | fromIntegral (st_next_active state) > cfg_max_rules =+ (False, state) | st_considered state >= cfg_max_critical_pairs = (False, state)- | solved state = (False, state)+ | solved state && not cfg_always_complete = (False, state) | otherwise =- case dequeue config state of- (Nothing, state) -> (False, state)- (Just (info, overlap, _, _), state) ->- (True, consider config state info overlap)+ case st_random_seed state of+ Nothing -> -- normal mode+ case dequeue config state of+ (Nothing, state) -> (False, state)+ (Just (info, overlap, _, _), state) ->+ (True, consider config state info overlap)+ Just g -> -- random mode+ let (g1, g2) = Random.split g in+ let state' = state { st_random_seed = Just g2 } in+ case findCriticalPair config state' g1 of+ Nothing -> (True, state'{st_problem_term = Nothing})+ Just (info, overlap, changed, cf) ->+ let maybeMessage st =+ case st_problem_term st of+ Just cf | changed -> message (NewProblemTerm cf) st+ _ -> st+ state'' = consider config (maybeMessage state'{st_problem_term = Just cf}) info overlap+ progress = st_next_active state' /= st_next_active state'' in+ (True, state''{st_problem_term = if progress then st_problem_term state'' else Nothing})++{-# INLINEABLE findCriticalPair #-}+findCriticalPair :: Function f => Config f -> State f -> QCGen -> Maybe (Info, CriticalPair f, Bool, ConfluenceFailure f)+findCriticalPair config state g = retry `mplus` random+ where+ trace _ x = x+ traceM _ = return ()+ sizes = concat [replicate 10 i | i <- [10,20..100]]++ retry = (hasUNFRetry strat <$> st_problem_term state) >>= toOverlap False >>= return . snd+ random = pickBest randoms+ where+ pickBest =+ listToMaybe . map snd . sortBy (comparing fst) . take (cfg_random_mode_best_of config) . catMaybes+ randoms = unGen (sequence [resize n test | n <- sizes]) g 0++ test = do+ !(t, rs) <- gen+ () <- traceM ("checking " ++ prettyShow t)+ --toOverlap True <$> (hasUNF strat t rs <>) <$> hasUNFRandom strat t+ return $ toOverlap True $ if cfg_random_mode_simple config then hasUNFSimple strat t rs else hasUNF strat t rs++ gen =+ if cfg_random_mode_goal_directed config then+ generateGoalTerm (goalTerms state) (Index.elems (index_all (st_rules state)))+ else do+ t <- generateTerm lhss+ r <- normaliseWith1Random (const True) strat t+ return (t, r)++ strat = basic (rewrite reducesSkolem (index_all (st_rules state)))+ lhss = map lhs (Index.elems (index_all (st_rules state)))++ toOverlap _ UniqueNormalForm{} = Nothing+ toOverlap changed (HasCriticalPair r1 (r2, n) cf) =+ {-+ Debug.Trace.trace+ (prettyShow $+ text "" $$+ text "Problem term before shrinking:" <+> pPrint (cf_orig_term cf) $$+ text " NF 1:" <+> pPrint (cf_orig_left_term cf) $$+ text " NF 2:" <+> pPrint (cf_orig_right_term cf)) $+ -}+ trace ("Term " ++ prettyShow (cf_term cf) ++ " has critical pair (" ++ prettyShow r1 ++ ", " ++ prettyShow r2 ++ ", " ++ show n ++ ")") $+ let r2' = renameAvoiding r1 r2 in+ let Just o = overlapAt (How n Forwards Forwards) r1 r2' r1 r2' in+ case simplifyOverlap (index_all (st_rules state)) o of+ Nothing ->+ trace ("Overlap " ++ prettyShow (overlap_eqn o) ++ " was spurious") Nothing -- should be rare+ Just o' ->+ Just (cfg_score_cp config 0 (overlap_eqn o'), (Info 0 IntSet.empty, makeCriticalPair o, changed, cf))++-- Return all goal terms. Handles the $equals coding.+goalTerms :: Function f => State f -> [Term f]+goalTerms state =+ -- Goals that are not related to $equals.+ [ t+ | eqn <- map goal_eqn (st_goals state),+ t <- concatMap unpack (terms eqn), + True ]+{-+ not (isTrueTerm t), not (isFalseTerm t)] +++ -- Axioms of the form $equals(t, u) = $false.+ [ goalTerm+ | t :=: u <- map axiom_eqn (st_axioms state),+ (lhs, rhs) <- maybeToList $+ if isFalseTerm t then decodeEquality u + else if isFalseTerm u then decodeEquality t+ else Nothing,+ goalTerm <- [t, u] ]+-}+ {-# INLINEABLE solved #-} solved :: Function f => State f -> Bool
Twee/Base.hs view
@@ -1,19 +1,21 @@ -- | Useful operations on terms and similar. Also re-exports some generally -- useful modules such as 'Twee.Term' and 'Twee.Pretty'. -{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards #-}+{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards, BangPatterns #-} module Twee.Base( -- * Re-exported functionality module Twee.Term, module Twee.Pretty, -- * The 'Symbolic' typeclass Symbolic(..), subst, terms, TermOf, TermListOf, SubstOf, TriangleSubstOf, BuilderOf, FunOf,- vars, isGround, funs, occ, occVar, canonicalise, renameAvoiding, renameManyAvoiding, freshVar,+ vars, isGround, funs, occ, occVar, occs, nests, canonicalise, renameAvoiding, renameManyAvoiding, freshVar, -- * General-purpose functionality Id(..), Has(..), -- * Typeclasses Minimal(..), minimalTerm, isMinimal, erase, eraseExcept, ground,- Ordered(..), lessThan, orientTerms, EqualsBonus(..), Strictness(..), Function) where+ Ordered(..), lessThan, orientTerms,+ EqualsBonus(..), isTrueTerm, isFalseTerm, decodeEquality,+ Strictness(..), Function) where import Prelude hiding (lookup) import Control.Monad@@ -147,6 +149,29 @@ occVar :: Symbolic a => Var -> a -> Int occVar x t = length (filter (== x) (vars t)) +-- | Count how many times all function symbols occur in the argument.+{-# INLINE occs #-}+occs :: Symbolic a => a -> IntMap.IntMap Int+occs = foldl' insert IntMap.empty . funs+ where+ insert !m !f = IntMap.insertWith (+) (fun_id f) 1 m++-- | 'nest' from Fuchs, "The application of goal-oriented heuristics+-- for proving equational theorems via the unfailing Knuth-Bendix+-- completion procedure"+{-# INLINE nests #-}+nests :: Symbolic a => a -> IntMap.IntMap Int+nests t = foldl' (hnest 0 0) IntMap.empty (terms t)++-- helper function for nests+hnest :: Int -> Int -> IntMap.IntMap Int -> TermList f -> IntMap.IntMap Int+hnest !f !c !as Empty = IntMap.insertWith max f c as+hnest f c as (Cons (Var _) ts) = hnest f c as ts+hnest f c as (Cons (App _ Empty) ts) = hnest f c as ts+hnest f c as (Cons (App g ts) us) =+ let as' = hnest (fun_id g) (if f == fun_id g then c+1 else 1) as ts+ in hnest f c as' us+ -- | Rename the argument so that variables are introduced in a canonical order -- (starting with V0, then V1 and so on). {-# INLINEABLE canonicalise #-}@@ -228,6 +253,18 @@ isEquals _ = False isTrue _ = False isFalse _ = False++isFalseTerm, isTrueTerm :: (EqualsBonus f, Labelled f) => Term f -> Bool+isFalseTerm (App false _) = isFalse false+isFalseTerm _ = False+isTrueTerm (App true _) = isTrue true+isTrueTerm _ = False++-- Decode $equals(t,u) into an equation t=u.+decodeEquality :: (EqualsBonus f, Labelled f) => Term f -> Maybe (Term f, Term f)+decodeEquality (App equals (Cons t (Cons u Empty)))+ | isEquals equals = Just (t, u)+decodeEquality _ = Nothing instance (Labelled f, EqualsBonus f) => EqualsBonus (Fun f) where hasEqualsBonus = hasEqualsBonus . fun_value
Twee/CP.hs view
@@ -158,7 +158,7 @@ {-# INLINE overlapAt' #-} overlapAt' :: How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f) overlapAt' how@How{how_pos = n} r1 r2 (!outer :=: (!outer')) (!inner :=: (!inner')) = do- let t = at n (singleton outer)+ let t = outer `at` n sub <- unifyTri inner t let -- Make sure to keep in sync with overlapProof@@ -223,13 +223,12 @@ -- where l is the biggest term and r is the smallest, -- and variables have weight 1 and functions have weight cfg_funweight. {-# INLINEABLE score #-}-score :: Function f => Config -> Depth -> Overlap a f -> Int-score Config{..} depth Overlap{..} =+score :: Function f => Config -> Depth -> Equation f -> Int+score Config{..} depth (l :=: r) = fromIntegral depth * cfg_depthweight + (m + n) * cfg_rhsweight + intMax m n * (cfg_lhsweight - cfg_rhsweight) where- l :=: r = overlap_eqn m = size' 0 (singleton l) n = size' 0 (singleton r) @@ -360,7 +359,7 @@ Just rightSub = match (lhs right) inner path = positionToPath (lhs left) (how_pos overlap_how)- inner = at (pathToPosition overlap_top path) (singleton overlap_top)+ inner = overlap_top `atPath` path proof = Proof.symm (ruleDerivation (subst leftSub left))
+ Twee/Generate.hs view
@@ -0,0 +1,121 @@+{-# LANGUAGE OverloadedStrings #-}+module Twee.Generate(generateTerm, generateGoalTerm, permuteVars) where++import Test.QuickCheck hiding (Function)+import Twee.Base+import Twee.Rule+import Data.Maybe+import Twee.Profile+import Twee.Utils+import Debug.Trace++type Pat f = Term f+type LHS f = Term f++-- the generator++generateTerm :: Function f => [LHS f] -> Gen (Term f)+generateTerm lhss = generateTerm' lhss (build (var (V 0)))++generateTerm' :: Function f => [LHS f] -> Pat f -> Gen (Term f)+generateTerm' lhss pat =+ stampGen "generateTerm'" $ do+ sized $ \n -> do+ sub <- gen n lhss pat emptyTriangleSubst+ permuteVars (subst sub pat)++gen :: Function f => Int -> [LHS f] -> Pat f -> TriangleSubst f -> Gen (TriangleSubst f)+gen n lhss p sub =+ -- TODO: play around with frequencies+ frequency $+ [ (1, return sub) ] +++ -- commit to top-level function...+ [ (n, genList (reduce n (length ps)) lhss ps sub)+ | App f psl <- [p]+ , let ps = unpack psl+ ] +++ -- ...or use a LHS for inspiration+ [ (n, gen n lhss p' sub')+ | n > 0+ , lhs <- map (renameAvoiding p) lhss+ , Just sub' <- [unifyTriFrom lhs p sub]+ , let p' = subst sub' p+ , n >= (len p' - len p)+ , not (isVariantOf p' p) -- make progress+ ]+ where+ reduce n m+ | m <= 1 = n-1+ | otherwise = n `div` m++-- just a helper function+genList :: Function f => Int -> [LHS f] -> [Pat f] -> TriangleSubst f -> Gen (TriangleSubst f)+genList _n _lhss [] sub =+ do return sub++genList n lhss (p:ps) sub =+ do sub' <- gen n lhss (subst sub p) sub+ sub'' <- genList n lhss ps sub'+ return sub''++-- Generate a term by starting with a goal term and rewriting+-- backwawrds a certain number of times.+generateGoalTerm :: Function f => [Term f] -> [Rule f] -> Gen (Term f, Reduction1 f)+generateGoalTerm goals rules = stampGen "generateGoalTerm" $ sized $ \n -> do+ t <- frequency [(len u, return u) | u <- goals]+ -- () <- traceM ("Goal term: " ++ prettyShow t)+ let ok u = len u <= n+ (u, r) <- loop (n `div` 5 + 1) (rewriteBackwardsWithReduction ok rules) (t, [])+ -- () <- traceM ("intermediate generated " ++ prettyShow u)+ -- fill in any holes with randomly-generated terms+ v <- generateTerm' (map lhs rules) u+ -- () <- traceM ("generated " ++ prettyShow v)+ -- () <- traceM ("proof " ++ prettyShow r)+ return (v, rematchReduction1 v r)++loop :: Monad m => Int -> (a -> m a) -> a -> m a+loop 0 _ x = return x+loop n f x | n > 0 = f x >>= loop (n-1) f++-- Apply a rule backwards at a given position in a term.+-- The goal rhs and the subterm must be unifiable.+tryBackwardsRewrite :: Rule f -> Term f -> Int -> Maybe (Term f, Reduction1 f)+tryBackwardsRewrite rule t n = do+ sub <- unify (rhs rule) (t `at` n)+ return $+ (build (replacePositionSub sub n (singleton (lhs rule)) (singleton t)),+ [(rule, sub, positionToPath t n)])++rewriteBackwardsWithReduction :: Function f => (Term f -> Bool) -> [Rule f] -> (Term f, Reduction1 f) -> Gen (Term f, Reduction1 f)+rewriteBackwardsWithReduction ok rules (t, r) = do+ res <- rewriteBackwards ok rules t+ case res of+ Nothing -> return (t, r)+ Just (u, r') -> return (u, r' `trans1` r)++-- Pick a random rule and rewrite the term backwards using it.+rewriteBackwards :: Function f => (Term f -> Bool) -> [Rule f] -> Term f -> Gen (Maybe (Term f, Reduction1 f))+rewriteBackwards ok rules t0+ | not (ok t0) = return Nothing+ | otherwise = + frequency $+ [(1, return Nothing)] ++ -- in case no rules work+ [ -- penalise unification with a variable as it can result in "type-incorrect" terms+ (if isVar (t `at` n) then 1 else 10*(overlap (t `at` n) (rhs rule)+1)*(if n == 0 then 2 else 1),+ return (Just (u, r)))+ | n <- [0..len t-1],+ rule <- rules,+ (u, r) <- maybeToList (tryBackwardsRewrite rule t n),+ ok u ]+ where+ t = renameAvoiding rules t0+ overlap (App f ts) (App g us) | f == g =+ 1 + sum (zipWith overlap (unpack ts) (unpack us))+ overlap _ _ = 0++permuteVars :: Term f -> Gen (Term f)+permuteVars t = do+ let vs = usort (vars t)+ ws <- shuffle vs+ let Just sub = listToSubst [(v, build (var w)) | (v, w) <- zip vs ws]+ return (subst sub t)
Twee/Join.hs view
@@ -237,8 +237,8 @@ {-# INLINEABLE valid #-} valid :: Function f => Model f -> Reduction f -> Bool valid model red =- and [ reducesInModel model rule emptySubst- | rule <- red ]+ and [ reducesInModel model (subst sub rule) emptySubst+ | (rule, sub) <- red ] optimise :: (a -> [a]) -> (a -> Bool) -> a -> a optimise f p x =
Twee/Profile.hs view
@@ -1,6 +1,6 @@ -- Basic support for profiling. {-# LANGUAGE BangPatterns, RecordWildCards, CPP, OverloadedStrings #-}-module Twee.Profile(stamp, stampWith, stampM, profile) where+module Twee.Profile(stamp, stampWith, stampM, stampGen, stampGen', profile) where #ifdef PROFILE import System.IO.Unsafe@@ -17,6 +17,7 @@ import Data.Symbol import Data.Symbol.Unsafe import Data.Hashable+import Test.QuickCheck.Gen instance Hashable Symbol where hashWithSalt s (Symbol n _) = hashWithSalt s n@@ -97,6 +98,12 @@ liftIO (exit m str) return x +stampGen :: Symbol -> Gen a -> Gen a+stampGen sym gen = MkGen (\g n -> stamp sym (unGen gen g n))++stampGen' :: (a -> Symbol) -> Gen a -> Gen a+stampGen' sym gen = MkGen (\g n -> let x = unGen gen g n in stamp (sym x) x)+ report :: (Record -> Word64) -> HashMap Symbol Record -> IO () report f cs = mapM_ pr ts where@@ -126,6 +133,7 @@ report rec_cumulative log #else import Control.Monad.IO.Class+import Test.QuickCheck stamp :: symbol -> a -> a stamp _ = id@@ -135,6 +143,12 @@ stampM :: MonadIO m => symbol -> m a -> m a stampM _ = id++stampGen :: symbol -> Gen a -> Gen a+stampGen _ = id++stampGen' :: (a -> symbol) -> Gen a -> Gen a+stampGen' _ = id profile :: IO () profile = return ()
Twee/Proof.hs view
@@ -10,6 +10,7 @@ -- * Analysing proofs simplify, steps, usedLemmas, usedAxioms, usedLemmasAndSubsts, usedAxiomsAndSubsts, groundAxiomsAndSubsts, eliminateDefinitions, eliminateDefinitionsFromGoal,+ simplifyProof, generaliseProof, -- * Pretty-printing proofs Config(..), defaultConfig, Presentation(..),@@ -556,7 +557,7 @@ inlineTrivialLemmas config . tightenProof - simp = simpCore . generaliseProof+ simp = simpCore . generaliseProof True -- generaliseProof undoes the effect of groundProof! -- But we still want to run generaliseProof first, to simplify the proof simp' = (simpCore . groundProof) `onlyIf` cfg_ground_proof@@ -666,14 +667,14 @@ sub <- maybeToList (match u t), subst sub (eqn_rhs eq) == eqn_rhs eq ] -generaliseProof :: Function f => [Derivation f] -> [Derivation f]-generaliseProof =+generaliseProof :: Function f => Bool -> [Derivation f] -> [Derivation f]+generaliseProof instGoal = simplificationPass (const generaliseLemma) (const generaliseGoal) where generaliseLemma p = lemma (certify q) sub where (q, sub) = generalise p- generaliseGoal p = subst sub q+ generaliseGoal p = if instGoal then subst sub q else q where (q, sub) = generalise (certify p) @@ -892,12 +893,6 @@ -- * a proof that both sides of the conjecture are equal -- and we can present that to the user. --- Decode $equals(t,u) into an equation t=u.-decodeEquality :: Function f => Term f -> Maybe (Equation f)-decodeEquality (App equals (Cons t (Cons u Empty)))- | isEquals equals = Just (t :=: u)-decodeEquality _ = Nothing- -- Tries to transform a proof of $true = $false into a proof of -- the original existentially-quantified formula. decodeGoal :: Function f => ProvedGoal f -> ProvedGoal f@@ -922,12 +917,6 @@ | isFalseTerm t = extract (steps (symm deriv)) | otherwise = Nothing where- isFalseTerm, isTrueTerm :: Term f -> Bool- isFalseTerm (App false _) = isFalse false- isFalseTerm _ = False- isTrueTerm (App true _) = isTrue true- isTrueTerm _ = False- t :=: u = equation pg_proof deriv = derivation pg_proof @@ -935,7 +924,7 @@ decodeReflexivity :: Derivation f -> Maybe (Term f) decodeReflexivity (Symm (UseAxiom Axiom{..} sub)) = do guard (isTrueTerm (eqn_rhs axiom_eqn))- (t :=: u) <- decodeEquality (eqn_lhs axiom_eqn)+ (t, u) <- decodeEquality (eqn_lhs axiom_eqn) guard (t == u) return (subst sub t) decodeReflexivity _ = Nothing@@ -944,8 +933,8 @@ decodeConjecture :: Derivation f -> Maybe (String, Equation f, Subst f) decodeConjecture (UseAxiom Axiom{..} sub) = do guard (isFalseTerm (eqn_rhs axiom_eqn))- eqn <- decodeEquality (eqn_lhs axiom_eqn)- return (axiom_name, eqn, sub)+ (t, u) <- decodeEquality (eqn_lhs axiom_eqn)+ return (axiom_name, t :=: u, sub) decodeConjecture _ = Nothing extract (p:ps) = do
Twee/Rule.hs view
@@ -20,6 +20,19 @@ import qualified Twee.Proof as Proof import Twee.Proof(Derivation, Proof) import Data.Tuple+import Twee.Profile+import Data.MemoUgly+import Debug.Trace+import Twee.Pretty+import Data.Function+import Control.Arrow((***))+import GHC.Stack+import Test.QuickCheck hiding (Function, subterms, Fun)+import Twee.Profile+import Test.QuickCheck.Gen+import Data.Semigroup+import qualified Data.List.NonEmpty as NonEmpty+import Test.QuickCheck.Random -------------------------------------------------------------------------------- -- * Rewrite rules.@@ -189,13 +202,13 @@ -- | 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 = simplifyOutermost+simplify idx t = stamp "simplify" (simplifyOutermost idx t) -- | 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+ | otherwise = simplifyOutermost idx u where u = build (simp (singleton t)) @@ -238,41 +251,44 @@ -- | 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]+-- | A reduction proof is just a sequence of rewrite steps. 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, Subst f)] -- | Transitivity for reduction sequences. trans :: Reduction f -> Reduction f -> Reduction f-trans p q = q ++ p+trans p q = p ++ q -- | Compute the final term resulting from a reduction, given the -- starting term. result :: Term f -> Reduction f -> Term f result t [] = t-result t (r:rs) = ruleResult u r+result t (r:rs) = result u rs where- u = result t rs+ !u = ruleResult t r -- | Turn a reduction into a proof. reductionProof :: Function f => Term f -> Reduction f -> Derivation f-reductionProof t ps = red t (Proof.Refl t) (reverse ps)+reductionProof t ps = red t (Proof.Refl t) ps where red _ p [] = p red t p (q:qs) = red (ruleResult t q) (p `Proof.trans` ruleProof t q) qs -- Helpers for result and reductionProof.-ruleResult :: Term f -> Rule f -> Term f-ruleResult t r = build (replace (lhs r) (rhs r) (singleton t))+ruleResult :: Term f -> (Rule f, Subst f) -> Term f+ruleResult t (r0, sub) = build (replace (lhs r) (rhs r) (singleton t))+ where+ r = subst sub r0 -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+ruleProof :: Function f => Term f -> (Rule f, Subst f) -> Derivation f+ruleProof t (r0, sub)+ | t == lhs r = ruleDerivation r+ | len t < len (lhs r) = Proof.Refl t+ where+ r = subst sub r0 ruleProof (App f ts) rule = Proof.cong f [ruleProof u rule | u <- unpack ts] ruleProof t _ = Proof.Refl t@@ -284,17 +300,12 @@ -- | Normalise a term wrt a particular strategy. {-# INLINE normaliseWith #-} normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Reduction f-normaliseWith ok strat t = res+normaliseWith ok strat t = aux t where- res = aux 0 [] t- aux 1000 p _ =- error $- "Possibly nonterminating rewrite:\n" ++ prettyShow p- aux n p t =+ aux t = case anywhere strat t of- (q:_) | u <- result t q, ok u ->- aux (n+1) (p `trans` q) u- _ -> p+ (p:_) | u <- result t p, ok u -> p `trans` aux u+ _ -> [] -- | 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)@@ -350,7 +361,7 @@ rewrite p rules t = do (sub, rule) <- Index.matches t rules guard (p (the rule) sub)- return [subst sub (the rule)]+ return [(the rule, sub)] -- | A strategy which applies one rule only. {-# INLINEABLE tryRule #-}@@ -358,7 +369,7 @@ tryRule p rule t = do sub <- maybeToList (match (lhs (the rule)) t) guard (p (the rule) sub)- return [subst sub (the rule)]+ return [(the rule, sub)] -- | Check if a rule can be applied, given an ordering <= on terms. {-# INLINEABLE reducesWith #-}@@ -414,3 +425,429 @@ reducesSkolem :: Function f => Rule f -> Subst f -> Bool reducesSkolem rule sub = reducesWith (\t u -> lessEqSkolem t u) rule sub++--------------------------------------------------------------------------------+-- * Rewriting that performs only a single step at a time (not in parallel).+--------------------------------------------------------------------------------++-- | A reduction proof is a sequence of rewrite steps, stored as a+-- list. Each rewrite step is coded as a rule, a+-- substitution and a path to be rewritten.+type Reduction1 f = [(Rule f, Subst f, [Int])]++-- | Transitivity for reduction sequences.+trans1 :: Reduction1 f -> Reduction1 f -> Reduction1 f+trans1 p q = p ++ q++-- TODO: get rid of the below copy-and-pasting by introducing a typeclass++-- | Compute the final term resulting from a reduction, given the+-- starting term.+result1 :: HasCallStack => Term f -> Reduction1 f -> Term f+result1 t [] = t+result1 t (r:rs) = result1 u rs+ where+ !u = ruleResult1 t r++-- | Turn a reduction into a proof.+reductionProof1 :: Function f => Term f -> Reduction1 f -> Derivation f+reductionProof1 t ps = red t (Proof.Refl t) ps+ where+ red _ p [] = p+ red t p (q:qs) =+ red (ruleResult1 t q) (p `Proof.trans` ruleProof1 t q) qs++-- Helpers for result1 and reductionProof1.+ruleResult1 :: HasCallStack => Term f -> (Rule f, Subst f, [Int]) -> Term f+ruleResult1 t (r0, sub, p)+ | t `at` n == lhs r =+ build (replacePosition n (rhs r) (singleton t))+ | otherwise = error "ruleResult1: selected subterm is not equal to lhs of rule"+ where+ r = subst sub r0+ n = pathToPosition t p++ruleProof1 :: Function f => Term f -> (Rule f, Subst f, [Int]) -> Derivation f+ruleProof1 t (r0, sub, p)+ | t `atPath` p == lhs r =+ Proof.congPath p t (ruleDerivation r) + | otherwise = error "ruleProof1: selected subterm is not equal to lhs of rule"+ where+ r = subst sub r0++-- | A strategy gives a set of possible reductions for a term.+type Strategy1 f = Term f -> [(Rule f, Subst f, [Int])]++-- | Apply a strategy anywhere in a term.+anywhere1 :: Strategy1 f -> Strategy1 f+anywhere1 strat t =+ stamp "anywhere1 (whnf)"+ [ (r, sub, p ++ p')+ | n <- reverse [0..len t-1], -- innermost+ let p = positionToPath t n,+ (r, sub, p') <- strat (t `at` n) ]++-- | Apply a basic strategy to a term.+basic :: Strategy f -> Strategy1 f+basic strat t = [(r, sub, []) | [(r, sub)] <- strat t]++-- | Normalise a term wrt a particular strategy.+{-# INLINE normaliseWith1 #-}+normaliseWith1 :: Function f => (Term f -> Bool) -> Strategy1 f -> Term f -> Reduction1 f+normaliseWith1 ok strat t = aux t+ where+ aux t =+ case anywhere1 strat t of+ (p:_) | u <- ruleResult1 t p, ok u ->+ [p] `trans1` aux u+ _ -> []++-- | Normalise a term wrt a particular strategy, picking random+-- rewrites at every step.+{-# INLINE normaliseWith1Random #-}+normaliseWith1Random :: Function f => (Term f -> Bool) -> Strategy1 f -> Term f -> Gen (Reduction1 f)+normaliseWith1Random ok strat t = aux t+ where+ aux t =+ let choices = [(p, u) | p <- anywhere1 strat t, let u = stamp "normaliseWith1Random.result1" (ruleResult1 t p), ok u] in+ case choices of+ [] -> return []+ _ -> do+ (p, u) <- elements choices+ fmap ([p] `trans1`) (aux u)++rematchReduction1 :: HasCallStack => Term f -> Reduction1 f -> Reduction1 f+rematchReduction1 _ [] = []+rematchReduction1 t ((r, _, pos):rs) =+ case match (lhs r) (t `atPath` pos) of+ Just sub ->+ let red = (r, sub, pos) in+ red:rematchReduction1 (ruleResult1 t red) rs+ Nothing -> error "rematch failed"++--------------------------------------------------------------------------------+-- * Testing whether a term has a unique normal form.+--------------------------------------------------------------------------------++data UNF f =+ -- Function has a unique normal form+ UniqueNormalForm (Term f) (Reduction1 f)+ | -- This pair of rules has an unjoinable critical pair+ HasCriticalPair (Rule f) (Rule f, Int) (ConfluenceFailure f)++data ConfluenceFailure f =+ ConfluenceFailure {+ cf_term :: Term f,+ cf_left :: Reduction1 f,+ cf_right :: Reduction1 f,+ cf_orig_term :: Term f,+ cf_orig_left :: Reduction1 f }++cf_left_term, cf_right_term :: ConfluenceFailure f -> Term f+cf_left_term ConfluenceFailure{..} = result1 cf_term cf_left+cf_right_term ConfluenceFailure{..} = result1 cf_term cf_right+{-+cf_orig_left_term, cf_orig_right_term :: ConfluenceFailure f -> Term f+cf_orig_left_term ConfluenceFailure{..} = result1 cf_orig_term cf_orig_left+cf_orig_right_term ConfluenceFailure{..} = result1 cf_orig_term cf_orig_right+-}+instance Semigroup (UNF f) where+ -- mconcat finds the first HasCriticalPair in the list+ UniqueNormalForm{} <> x = x+ x@HasCriticalPair{} <> _ = x++instance Function f => Pretty (UNF f) where+ pPrint UniqueNormalForm{} = text "unique normal form"+ pPrint (HasCriticalPair r1 (r2, n) _) = text "critical pair" <+> pPrint r1 <+> pPrint (r2, n)++hasUNFRetry :: Function f => Strategy1 f -> ConfluenceFailure f -> UNF f+hasUNFRetry strat ConfluenceFailure{..} =+ hasUNF strat cf_orig_term cf_orig_left {- <>+ hasUNF strat cf_term cf_right -}++hasUNFRandom :: Function f => Strategy1 f -> Term f -> Gen (UNF f)+hasUNFRandom strat t =+ sconcat . NonEmpty.fromList <$> sequence+ [ do r <- normaliseWith1Random (const True) strat u+ return (hasUNF strat u r)+ | u <- reverseSubterms t,+ _ <- [1..5] ]++hasUNFSimple :: Function f => Strategy1 f -> Term f -> Reduction1 f -> UNF f+hasUNFSimple strat t0 r0 = magic t0 r0+ where+ normSteps t = normaliseWith1 (const True) strat t+ norm =+ memo $ \t ->+ stamp "hasUNF.norm" $+ case anywhere1 strat t of+ [] -> t+ r:_ -> norm (ruleResult1 t r)++ magic t [] = UniqueNormalForm (norm t) (normSteps t)+ magic t (r@(rule, sub, pos):rs) =+ case magic (ruleResult1 t r) rs of+ res@HasCriticalPair{} -> res+ UniqueNormalForm v rsu ->+ maybe (UniqueNormalForm v (r:rsu)) sconcat $ NonEmpty.nonEmpty $ outer `mplus` inner+ where+ outer = do+ let t' = t `atPath` pos+ n <- [1..len t'-1] -- 0 case is handled in inner+ let pos' = positionToPath t' n+ guard (not (isVar (t' `at` n)))+ guard (criticalOverlap (lhs rule) pos')+ (rule', sub', []) <- strat (t' `at` n)++ guard (norm (ruleResult1 t (rule', sub', pos ++ pos')) /= norm (ruleResult1 t r))+ return $+ HasCriticalPair rule (rule', pathToPosition (lhs rule) pos') $+ ConfluenceFailure t' [(rule, sub, [])] [(rule', sub', pos')] t0 r0++ inner = do+ pos' <- inits pos+ let t' = t `atPath` pos'+ (rule', sub', []) <- strat t'+ let posInner = drop (length pos') pos+ guard (criticalOverlap (lhs rule') posInner)++ guard (norm (ruleResult1 t (rule', sub', pos')) /= norm (ruleResult1 t r))+ return $+ HasCriticalPair rule' (rule, pathToPosition (lhs rule') posInner) $+ ConfluenceFailure t' [(rule', sub', [])] [(rule, sub, posInner)] t0 r0++ criticalOverlap (Var _) _ = False+ criticalOverlap App{} [] = True+ criticalOverlap t (p:ps) = criticalOverlap (unpack (children t) !! p) ps++hasUNF :: (HasCallStack, Function f) => Strategy1 f -> Term f -> Reduction1 f -> UNF f+hasUNF strat t0 r0 =+ let res = magic t0 r0+ in stamp (case res of { UniqueNormalForm{} -> "hasUNF.UNF"; HasCriticalPair{} -> "hasUNF.CP" }) res+ where+ trace _ x = x+ --normFirstStep t = trace (prettyShow (t, take 1 $ anywhere1 strat t)) $ head (head (anywhere1 strat t))+ normSteps t = normaliseWith1 (const True) strat t+ normStepsVia r t = r `trans1` normSteps (result1 t r)+ norm =+ memo $ \t ->+ stamp "hasUNF.norm" $+ case anywhere1 strat t of+ [] -> t+ r:_ -> norm (ruleResult1 t r)++ normStepsR t = unGen (replicateM 10 (normaliseWith1Random (const True) strat t)) (mkQCGen 1234) 10+ --normR t = result1 t (normStepsR t)++ --magic :: Term f -> Reduction1 f -> UNF f+ magic t [] = UniqueNormalForm (norm t) (normSteps t)+ magic t (r:rs) =+ let u = ruleResult1 t r in+ case magic u rs of+ res@HasCriticalPair{} -> res+ UniqueNormalForm v rsu ->+ sconcat (NonEmpty.fromList [magic1 t rst r u rsu v | rst <- normStepsR t])++ magic1 t rst (r, sub, p) u rsu v+ | nt == v = UniqueNormalForm v rst+ | not (oriented (orientation r)) && not (reducesSkolem r sub) =+ -- v <-* u -> t, nt /= v+ conflict u rsu v ([(backwards r, sub, p)] `trans1` rst) nt+ | otherwise = conflict t ([(r, sub, p)] `trans1` rsu) v rst nt+ where+ nt = result1 t rst+ + -- precondition: normR t r1 /= normR t r2+ --conflict, conflict' :: Term f -> Reduction1 f -> Term f -> Reduction1 f -> Term f -> UNF f+ conflict t rs1 u rs2 v = stamp "conflict" (conflict' t rs1 u rs2 v)+ conflict' t (r1:rs1) u (r2:rs2) v+ | trace "" $+ trace ("Conflicting term: " ++ prettyShow t) $+ trace ("Rule 1: " ++ prettyShow r1) $+ trace ("Rule 2: " ++ prettyShow r2) $+ trace "" False = undefined++ conflict' t (r1:rs1) u (r2:rs2) v+ | not ok = error "not ok"+ | r1 == r2 = conflict' (ruleResult1 t r1) rs1 u rs2 v+ | otherwise =+ case commute t r1 r2 of+ Nothing -> criticalPair t r1 r2+ Just (rs1', rs2') ->+ trace "" $+ trace ("t = " ++ prettyShow t) $+ trace ("r1 = " ++ prettyShow r1) $+ trace ("u = " ++ prettyShow (ruleResult1 t r1)) $+ trace ("r2 = " ++ prettyShow r2) $+ trace ("v = " ++ prettyShow (ruleResult1 t r2)) $+ trace ("rs1' = " ++ prettyShow rs1') $+ trace ("rs2' = " ++ prettyShow rs2') $+ let w = result1 t (r1:rs1') in+ if norm w == u then+ conflict' (ruleResult1 t r2) (rs2' ++ normSteps w) u rs2 v+ else+ conflict' (ruleResult1 t r1) rs1 u (rs1' ++ normSteps w) (norm w)+ where+ ok =+ norm u == u && norm v == v &&+ result1 t (r1:rs1) == u &&+ result1 t (r2:rs2) == v++ criticalPair t (r1, sub1, (p1:ps1)) (r2, sub2, (p2:ps2))+ | p1 == p2 = criticalPair (unpack (children t) !! p1) (r1, sub1, ps1) (r2, sub2, ps2)+ criticalPair t (r1, sub1, []) (r2, sub2, p) =+ makeCriticalPair t r1 sub1 r2 sub2 p+ criticalPair t (r1, sub1, p) (r2, sub2, []) =+ makeCriticalPair t r2 sub2 r1 sub1 p++ makeCriticalPair t r1 sub1 r2 sub2 p =+ HasCriticalPair r1 (r2, pathToPosition (lhs r1) p) $+ ConfluenceFailure t [(r1, sub1, [])] [(r2, sub2, p)] t0 r0+ + --commute :: Term f -> (Rule f, Subst f, [Int]) -> (Rule f, Subst f, [Int]) -> Maybe (Reduction1 f, Reduction1 f)+ commute t r1@(rule1, sub1, (p1:ps1)) r2@(rule2, sub2, (p2:ps2))+ | p1 == p2 =+ -- descend into same subterm+ fmap (both (map (atPos p1))) (commute (unpack (children t) !! p1) (rule1, sub1, ps1) (rule2, sub2, ps2))+ | otherwise =+ -- parallel subterms+ trace "parallel subterms" $ Just ([r2], [r1])+ commute t r1@(_, _, _:_) r2@(_, _, []) =+ -- swap rules so the one which rewrites the root comes first+ fmap (\(x, y) -> (y, x)) $ commute t r2 r1+ commute t r1@(rule1, _, []) r2@(_, _, ps)+ | not (criticalOverlap (lhs rule1) ps) =+ trace "non-overlapping" $ Just (nonOverlapping t r1 r2)+ commute t r1 r2+ | norm u == norm v = trace "joinable" $ Just (normSteps u, normSteps v)+ where+ u = ruleResult1 t r1+ v = ruleResult1 t r2+ commute _ _ _ = Nothing++ -- Precondition: r1 can be commuted with some number of parallel+ -- rewrites of r2+ nonOverlapping t r1 r2 = stamp "nonOverlapping" (nonOverlapping' t r1 r2)+ nonOverlapping' t r1@(rule1, _, p1) r2@(rule2, _, p2)+ | trace "" $+ trace ("Non-overlapping reduction: " ++ prettyShow t) $+ trace ("First rule: " ++ prettyShow r1) $+ trace ("Second rule: " ++ prettyShow r2) $+ trace ("Reduction of first rule: " ++ prettyShow u) $+ trace ("Reduction of second rule: " ++ prettyShow v) $+ trace ("Positions before: " ++ prettyShow ps2Before) $+ trace ("Positions after: " ++ prettyShow ps2After) $+ trace ("Rules before: " ++ prettyShow rs2Before) $+ trace ("Rules after: " ++ prettyShow rs2After) $+ trace ("Final step: " +++ if correctlyOriented && not reflexivity then "right " ++ prettyShow [(rule1, sub1After, p1)]+ else if not (correctlyOriented || reflexivity) then "left " ++ prettyShow [(backwards rule1, sub1After, p1)]+ else "none") $+ trace ("Final term: " ++ prettyShow w) $+ trace ("Rewrite proof:\n" ++ prettyShow (Proof.certify (reductionProof1 t ([r1] `trans1` conf1)))) $+ trace ("Rewrite proof:\n" ++ prettyShow (Proof.certify (reductionProof1 t ([r2] `trans1` conf2)))) $+ False = undefined+ | otherwise = (conf1, conf2)+ where+ u = result1 t [r1]+ v = result1 t [r2]+ (ps2Before, ps2After) = track rule1 p1 p2+ rs2Before = [(rule2, rematch rule2 p t, p) | p <- ps2Before, p /= p2]+ rs2After = [(rule2, rematch rule2 p u, p) | p <- ps2After]++ -- Two paths:+ -- (1) r1; rs2After+ -- (2) rs2Before; r1+ -- But, in (2), if r1 is oriented the wrong way, we do this instead:+ -- (1) r1; rs2After; backwards r1+ -- (2) rs2Before++ -- TODO don't code term ordering+ correctlyOriented = oriented (orientation rule1) || reducesSkolem rule1 sub1After+ reflexivity = subst sub1After (lhs rule1) == subst sub1After (rhs rule1)+ sub1After = rematch rule1 p1 (result1 v rs2Before)++ -- The two reductions are: [red1] `trans` conf1, [red2] `trans` conf2+ conf1 = rs2After `trans1` (if correctlyOriented || reflexivity then [] else [(backwards rule1, sub1After, p1)])+ conf2 = rs2Before `trans1` (if correctlyOriented && not reflexivity then [(rule1, sub1After, p1)] else [])++ -- Check that both reductions give the same result+ w1 = result1 u conf1+ w2 = result1 v conf2+ w | w1 == w2 = w1+ + criticalOverlap (Var _) _ = False+ criticalOverlap App{} [] = True+ criticalOverlap t (p:ps) = criticalOverlap (unpack (children t) !! p) ps++ atPos p (r, sub, ps) = (r, sub, p:ps)+ both f (x, y) = (f x, f y)++ -- find the substitution for a rewrite+ rematch r pos t = sub+ where+ Just sub = match (lhs r) (t `atPath` pos)++-- Given a path in a term which is below a variable, find the variable+-- and the part of the path below the variable+decomposePath (Var x) ps = (x, ps)+decomposePath t (p:ps) = decomposePath (unpack (children t) !! p) ps++-- positions of a variable in a term+varPos :: Var -> Term f -> [Int]+varPos x t = [n | n <- [0..len t-1], t `at` n == build (var x)]++-- Consider a rewrite t -> u at position pr in a term, and a position+-- pt that does not overlap with the rewrite:+-- (1) Suppose that right now the rewrite could be applied, but+-- instead do a different rewrite at position pt. What other+-- positions must be also rewrite for the original rewrite to+-- still be applicable?+-- (e.g.: if the rule is f(x,x)->..., and the position is one of+-- the "x"s, if we rewrite one "x" we must also rewrite the other)+-- (2) Where does the position pt "move to" after the rewrite?+track :: Rule f -> [Int] -> [Int] -> ([[Int]], [[Int]])+track r (p:pr) (p':pt)+ -- common prefix+ | p == p' = (map (p:) *** map (p:)) (track r pr pt)+ -- parallel prefix+ | otherwise = ([p':pt], [p':pt])+track _ (_:_) [] =+ -- position being tracked < position of rewrite+ ([[]], [[]])+track Rule{lhs = lhs, rhs = rhs} [] pt =+ -- strategy: find what variable position pt occurs under in the lhs of the rule,+ -- then find all occurrences of that variable in the rhs of the rule+ let+ (x, p) = decomposePath lhs pt+ in+ ([positionToPath lhs n ++ p | n <- varPos x lhs],+ [positionToPath rhs n ++ p | n <- varPos x rhs])++{-+hasUNFSlow :: Function f => Strategy1 f -> Term f -> UNF f+hasUNFSlow strat t0 =+ head $+ -- optimisation: check if any subterm has a non-unique normal form first+ [r | r@HasCriticalPair{} <- map magic (sortBy (comparing len) (properSubterms t0))] +++ [magic t0]+ where+ magic = memo $ \t ->+ --trace ("magic " ++ prettyShow t) $+ let+ as = [(red, {-trace ("recursing from " ++ prettyShow t ++ " to " ++ prettyShow (result1 t red) ++ " via " ++ prettyShow red) $-} magic (result1 t red)) | red <- strat t, if result1 t red == t then error "oops" else True]++ conflict (r1, []) (r2, p) = HasCriticalPair r1 (r2, pathToPosition (lhs r1) p)+ conflict (r1, p) (r2, []) = HasCriticalPair r2 (r1, pathToPosition (lhs r2) p)+ conflict (r1, (m:ms)) (r2, (n:ns)) | m == n = conflict (r1, ms) (r2, ns)+ conflict _ _ = error "something has gone wrong in the magic function"++ res = head $+ [r | r@HasCriticalPair{} <- map snd as] +++ case nubBy ((==) `on` snd) ([(red, t) | (red, UniqueNormalForm t) <- as]) of+ [] -> [UniqueNormalForm t]+ [(_, t)] -> [UniqueNormalForm t]+ ((r1, _, n1):_, t1):((r2, _, n2):_, t2):_ ->+ [conflict (r1, positionToPath t n1) (r2, positionToPath t n2)]+ in {-traceShow (pPrint res)-} res+-}
Twee/Term.hs view
@@ -33,7 +33,7 @@ build, buildList, con, app, var, -- * Access to subterms- children, properSubterms, subtermsList, subterms, reverseSubtermsList, reverseSubterms, occurs, isSubtermOf, isSubtermOfList, at,+ children, properSubterms, subtermsList, subterms, reverseSubtermsList, reverseSubterms, occurs, isSubtermOf, isSubtermOfList, at, listAt, atPath, -- * Substitutions Substitution(..), subst,@@ -79,6 +79,7 @@ import Twee.Utils import qualified Data.Label as Label import Data.Typeable+import GHC.Stack -------------------------------------------------------------------------------- -- * A type class for builders@@ -520,6 +521,14 @@ empty :: forall f. TermList f empty = buildList (mempty :: Builder f) +-- | Index into a term.+at :: Term f -> Int -> Term f+t `at` n = singleton t `listAt` n++-- | Index into a term using a path.+atPath :: Term f -> [Int] -> Term f+t `atPath` p = t `at` pathToPosition t p+ -- | Get the children (direct subterms) of a term. children :: Term f -> TermList f children t =@@ -607,7 +616,7 @@ {-# INLINE reverseSubtermsList #-} reverseSubtermsList :: TermList f -> [Term f] reverseSubtermsList t =- [ unsafeAt n t | n <- [k-1,k-2..0] ]+ [ t `unsafeListAt` n | n <- [k-1,k-2..0] ] where k = lenList t @@ -711,7 +720,7 @@ | otherwise = list (k+1) u (n-len t) -- | Convert a path in a term into a position.-pathToPosition :: Term f -> [Int] -> Int+pathToPosition :: HasCallStack => Term f -> [Int] -> Int pathToPosition t ns = term 0 t ns where term k _ [] = k
Twee/Term/Core.hs view
@@ -85,14 +85,14 @@ type role TermList nominal -- | Index into a termlist.-at :: Int -> TermList f -> Term f-at n t+listAt :: TermList f -> Int -> Term f+t `listAt` n | n < 0 || low t + n >= high t = error "term index out of bounds"- | otherwise = unsafeAt n t+ | otherwise = t `unsafeListAt` n -- | Index into a termlist, without bounds checking.-unsafeAt :: Int -> TermList f -> Term f-unsafeAt n (TermList lo hi arr) =+unsafeListAt :: TermList f -> Int -> Term f+TermList lo hi arr `unsafeListAt` n = case TermList (lo+n) hi arr of UnsafeCons t _ -> t
twee-lib.cabal view
@@ -1,5 +1,5 @@ name: twee-lib-version: 2.4.2+version: 2.5 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3@@ -51,6 +51,7 @@ Twee.Constraints Twee.CP Twee.Equation+ Twee.Generate Twee.Index Twee.Join Twee.KBO@@ -62,6 +63,7 @@ Twee.Term Twee.Task Twee.Utils+ Twee.Term.Core Data.Label other-modules: Data.BatchedQueue@@ -70,10 +72,10 @@ Data.Heap Data.Numbered Data.PackedSequence- Twee.Term.Core build-depends:- base >= 4 && < 5,+ -- base >= 4.11 for Semigroup in Prelude+ base >= 4.11 && < 5, containers, transformers, dlist,@@ -83,7 +85,8 @@ uglymemo, random, bytestring,- cereal+ cereal,+ QuickCheck hs-source-dirs: . ghc-options: -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports default-language: Haskell2010