twee-lib 2.1.3 → 2.1.4
raw patch · 7 files changed
+69/−33 lines, 7 files
Files
- Twee.hs +34/−11
- Twee/Base.hs +3/−0
- Twee/CP.hs +2/−0
- Twee/Join.hs +2/−2
- Twee/Rule.hs +21/−17
- Twee/Term.hs +6/−2
- twee-lib.cabal +1/−1
Twee.hs view
@@ -434,11 +434,11 @@ -- Name and number are for information only. data Goal f = Goal {- goal_name :: String,- goal_number :: Int,- goal_eqn :: Equation f,- goal_lhs :: Set (Resulting f),- goal_rhs :: Set (Resulting f) }+ goal_name :: String,+ goal_number :: Int,+ goal_eqn :: Equation f,+ goal_lhs :: Set (Resulting f),+ goal_rhs :: Set (Resulting f) } -- Add a new goal. {-# INLINEABLE addGoal #-}@@ -450,14 +450,35 @@ {-# INLINEABLE normaliseGoals #-} normaliseGoals :: Function f => State f -> State f normaliseGoals state@State{..} =- {-# SCC normaliseGoals #-} state { st_goals =- map (goalMap (successors (rewrite reduces (index_all st_rules)) . Set.toList)) st_goals }+ map (goalMap (Rule.normalForms (rewrite reduces (index_all st_rules)))) st_goals } where goalMap f goal@Goal{..} = goal { goal_lhs = f goal_lhs, goal_rhs = f goal_rhs } +-- Recompute all normal forms of all goals. Starts from the original goal term.+-- Different from normalising all goals, because there may be an intermediate+-- term on one of the reduction paths which we can now rewrite in a different+-- way.+{-# INLINEABLE recomputeGoals #-}+recomputeGoals :: Function f => State f -> State f+recomputeGoals state =+ -- Make this strict so that newTask can time it correctly+ forceList (map goal_lhs (st_goals state')) `seq`+ forceList (map goal_rhs (st_goals state')) `seq`+ state'+ where+ state' =+ normaliseGoals (state { st_goals = map reset (st_goals state) })++ reset goal@Goal{goal_eqn = t :=: u, ..} =+ goal { goal_lhs = Set.singleton (reduce (Refl t)),+ goal_rhs = Set.singleton (reduce (Refl u)) }++ forceList [] = ()+ forceList (x:xs) = x `seq` forceList xs+ -- Create a goal. {-# INLINE goal #-} goal :: Int -> String -> Equation f -> Goal f@@ -517,7 +538,6 @@ sub <- match t' t matchIn sub u' u - ---------------------------------------------------------------------- -- The main loop. ----------------------------------------------------------------------@@ -535,11 +555,14 @@ lift $ output_message SimplifyQueue state <- StateM.get StateM.put $! simplifyQueue config state,- newTask 0.25 0.05 $ do+ newTask 1 0.05 $ do when cfg_simplify $ do lift $ output_message Interreduce state <- StateM.get- StateM.put $! interreduce config state]+ StateM.put $! interreduce config state,+ newTask 1 0.02 $ do+ state <- StateM.get+ StateM.put $! recomputeGoals state ] let loop = do@@ -608,7 +631,7 @@ {-# INLINEABLE normalForms #-} normalForms :: Function f => State f -> Term f -> Set (Resulting f) normalForms State{..} t =- Rule.normalForms (rewrite reduces (index_all st_rules)) [reduce (Refl t)]+ Rule.normalForms (rewrite reduces (index_all st_rules)) (Set.singleton (reduce (Refl t))) {-# INLINEABLE simplifyTerm #-} simplifyTerm :: Function f => State f -> Term f -> Term f
Twee/Base.hs view
@@ -193,6 +193,7 @@ class Skolem f where -- | Turn a variable into a Skolem constant. skolem :: Var -> Fun f+ getSkolem :: Fun f -> Maybe Var -- | For types which have a notion of arity. class Arity f where@@ -273,6 +274,8 @@ instance (Typeable f, Ord f) => Skolem (Extended f) where skolem x = fun (Skolem x)+ getSkolem (F (Skolem x)) = Just x+ getSkolem _ = Nothing instance EqualsBonus f => EqualsBonus (Extended f) where hasEqualsBonus (Function f) = hasEqualsBonus f
Twee/CP.hs view
@@ -184,6 +184,8 @@ size' n ts | Cons (App f ws@(Cons a (Cons b us))) vs <- ts, hasEqualsBonus (fun_value f),+ not (isVar a),+ not (isVar b), Just sub <- unify a b = size' (n+cfg_funweight*size f) ws `min` size' (size' (n+1) (subst sub us)) (subst sub vs)
Twee/Join.hs view
@@ -54,8 +54,8 @@ Right (Nothing, []) _ | cfg_set_join config && not (null $ Set.intersection- (normalForms (rewrite reduces (index_all idx)) [reduce (Refl t)])- (normalForms (rewrite reduces (index_all idx)) [reduce (Refl u)])) ->+ (normalForms (rewrite reduces (index_all idx)) (Set.singleton (reduce (Refl t))))+ (normalForms (rewrite reduces (index_all idx)) (Set.singleton (reduce (Refl u))))) -> Right (Just cp, []) Just cp -> case groundJoinFromMaybe config eqns idx mmodel (branches (And [])) cp of
Twee/Rule.hs view
@@ -3,7 +3,7 @@ module Twee.Rule where import Twee.Base-import Twee.Constraints+import Twee.Constraints hiding (funs) import qualified Twee.Index as Index import Twee.Index(Index) import Control.Monad@@ -351,33 +351,36 @@ _ -> Resulting t p -- | Compute all normal forms of a set of terms wrt a particular strategy.-normalForms :: Function f => Strategy f -> [Resulting f] -> Set (Resulting f)+normalForms :: Function f => Strategy f -> Set (Resulting f) -> Set (Resulting f) normalForms strat ps = snd (successorsAndNormalForms strat 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 -> [Resulting f] -> Set (Resulting f)-successors strat ps = Set.union qs rs+successors :: Function f => Strategy f -> Set (Resulting f) -> Set (Resulting f)+successors strat ps =+ Set.union qs rs where (qs, rs) = successorsAndNormalForms strat ps {-# INLINEABLE successorsAndNormalForms #-}-successorsAndNormalForms :: Function f => Strategy f -> [Resulting f] ->+successorsAndNormalForms :: Function f => Strategy f -> Set (Resulting f) -> (Set (Resulting f), Set (Resulting f)) successorsAndNormalForms strat ps = {-# SCC successorsAndNormalForms #-} go Set.empty Set.empty ps where- go dead norm [] = (dead, norm)- go dead norm (p:ps)- | p `Set.member` dead = go dead norm ps- | p `Set.member` norm = go dead norm ps- | null qs = go dead (Set.insert p norm) ps- | otherwise =- go (Set.insert p dead) norm (qs ++ ps)- where- qs =- [ reduce (reduction p `Trans` q)- | q <- anywhere strat (result p) ]+ go dead norm ps =+ case Set.minView ps of+ Nothing -> (dead, norm)+ Just (p, ps)+ | p `Set.member` dead -> go dead norm ps+ | p `Set.member` norm -> go dead norm ps+ | null qs -> go dead (Set.insert p norm) ps+ | otherwise ->+ go (Set.insert p dead) norm (Set.fromList qs `Set.union` ps)+ where+ qs =+ [ reduce (reduction p `trans` q)+ | q <- anywhere strat (result p) ] -- | Apply a strategy anywhere in a term. anywhere :: Strategy f -> Strategy f@@ -485,4 +488,5 @@ reducesSkolem rule sub = reducesWith (\t u -> lessEq (subst skolemise t) (subst skolemise u)) rule sub where- skolemise = con . skolem+ skolemise (V x) = con (skolem (V (x + k)))+ V k = maximum (V 0:map succ (catMaybes (map getSkolem (funs rule))))
Twee/Term.hs view
@@ -48,7 +48,7 @@ match, matchIn, matchList, matchListIn, isInstanceOf, isVariantOf, -- * Unification unify, unifyList,- unifyTri, unifyListTri,+ unifyTri, unifyListTri, unifyListTriFrom, TriangleSubst(..), close, -- * Positions in terms@@ -401,7 +401,11 @@ -- | Unify two termlists, returning a triangle substitution. -- This is slightly faster than 'unify'. unifyListTri :: TermList f -> TermList f -> Maybe (TriangleSubst f)-unifyListTri !t !u = fmap Triangle ({-# SCC unify #-} loop emptySubst t u)+unifyListTri t u = unifyListTriFrom t u (Triangle emptySubst)++unifyListTriFrom :: TermList f -> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)+unifyListTriFrom !t !u (Triangle !sub) =+ fmap Triangle ({-# SCC unify #-} loop sub t u) where loop !_ !_ !_ | False = undefined loop sub Empty Empty = Just sub
twee-lib.cabal view
@@ -1,5 +1,5 @@ name: twee-lib-version: 2.1.3+version: 2.1.4 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3