twee-lib 2.5 → 2.6.1
raw patch · 17 files changed
+588/−431 lines, 17 files
Files
- Data/BatchedQueue.hs +1/−1
- Data/Intern.hs +147/−0
- Data/Label.hs +0/−137
- Twee.hs +67/−16
- Twee/Base.hs +26/−21
- Twee/CP.hs +54/−31
- Twee/Constraints.hs +33/−20
- Twee/Equation.hs +5/−5
- Twee/Index.hs +31/−25
- Twee/Join.hs +44/−23
- Twee/KBO.hs +18/−17
- Twee/Pretty.hs +12/−8
- Twee/Proof.hs +74/−27
- Twee/Rule.hs +5/−5
- Twee/Term.hs +38/−63
- Twee/Term/Core.hs +28/−28
- twee-lib.cabal +5/−4
Data/BatchedQueue.hs view
@@ -83,7 +83,7 @@ if not (ok (batchLabel batch)) then removeMinFilter ok (Queue q) else case unconsBatch batch of (entry, Just batch') ->- Just (entry, Queue (Heap.insert (Best batch') q))+ Just (entry, Queue (Heap.insert (Best batch') q)) -- TODO: investigate if this can be made more efficient (removeMin+insert causes two merges even if the same batch is at the root before and after (entry, Nothing) -> Just (entry, Queue q)
+ Data/Intern.hs view
@@ -0,0 +1,147 @@+-- | Interning, annotating values with unique IDs.++{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns, MagicHash, RoleAnnotations, CPP, PatternSynonyms, ViewPatterns, ConstraintKinds #-}+module Data.Intern(Intern, Sym, pattern Sym, intern, unintern, unsafeMkSym, symId) where++import Data.IORef+import System.IO.Unsafe+import qualified Data.Map.Strict as Map+import Data.Map.Strict(Map)+import qualified Data.DynamicArray as DynamicArray+import Data.DynamicArray(Array)+import Data.Typeable+import GHC.Exts+import GHC.Int+import Unsafe.Coerce++-- | Type class constraints for a value to be internable.+type Intern a = (Typeable a, Ord a)++-- | An interned value of type @a@.+newtype Sym a = MkSym Int32+ deriving (Eq, Ord)++instance Show a => Show (Sym a) where+ show = show . unintern++-- | The unique ID of a symbol.+symId :: Sym a -> Int+symId (MkSym x) = fromIntegral x++type role Sym nominal -- no coercions please++-- | Construct a @'Sym' a@ from its unique ID, which must be the 'symId' of+-- an already existing 'Sym'. Extremely unsafe!+unsafeMkSym :: Int -> Sym a+unsafeMkSym = MkSym . fromIntegral++-- The global cache of interned values.+{-# NOINLINE cachesRef #-}+cachesRef :: IORef Caches+cachesRef = unsafePerformIO (newIORef (Caches 0 Map.empty DynamicArray.newArray))++data Caches =+ Caches {+ -- The next id number to assign.+ caches_nextId :: {-# UNPACK #-} !Int32,+ -- A map from values to IDs.+ caches_from :: !(Map TypeRep (Cache Any)),+ -- The reverse map from IDs to values.+ caches_to :: !(Array Any) }++type Cache a = Map a Int32++atomicModifyCaches :: (Caches -> (Caches, a)) -> IO a+atomicModifyCaches f = do+ -- N.B. atomicModifyIORef' ref f evaluates f ref *after* doing the+ -- compare-and-swap. This causes bad things to happen when 'intern'+ -- is used reentrantly (i.e. the Ord instance itself calls intern).+ -- This function only lets the swap happen if caches_nextId didn't+ -- change (i.e., no new values were inserted).+ !caches <- readIORef cachesRef+ -- First compute the update.+ let !(!caches', !x) = f caches+ -- Now see if anyone else updated the cache in between+ -- (can happen if f called 'intern', or in a concurrent setting).+ ok <- atomicModifyIORef' cachesRef $ \cachesNow ->+ if caches_nextId caches == caches_nextId cachesNow+ then (caches', True)+ else (cachesNow, False)+ if ok then return x else atomicModifyCaches f++-- Versions of unsafeCoerce with slightly more type checking+toAnyCache :: Cache a -> Cache Any+toAnyCache = unsafeCoerce++fromAnyCache :: Cache Any -> Cache a+fromAnyCache = unsafeCoerce++toAny :: a -> Any+toAny = unsafeCoerce++fromAny :: Any -> a+fromAny = unsafeCoerce++-- | Intern a value.+{-# NOINLINE intern #-}+intern :: forall a. Intern a => a -> Sym a+intern x =+ unsafeDupablePerformIO $ do+ -- Common case: symbol is already interned.+ caches <- readIORef cachesRef+ case tryFind caches of+ Just s -> return s+ Nothing -> do+ -- Rare case: symbol has not yet been interned.+ x <- atomicModifyCaches $ \caches ->+ case tryFind caches of+ Just s -> (caches, s)+ Nothing ->+ insert caches+ return x++ where+ ty = typeOf x++ tryFind :: Caches -> Maybe (Sym a)+ tryFind Caches{..} =+ MkSym <$> (Map.lookup ty caches_from >>= Map.lookup x . fromAnyCache)++ insert :: Caches -> (Caches, Sym a)+ insert caches@Caches{..} =+ if n < 0 then error "label overflow" else+ (caches {+ caches_nextId = n+1,+ caches_from = Map.insert ty (toAnyCache (Map.insert x n cache)) caches_from,+ caches_to = DynamicArray.updateWithDefault undefined (fromIntegral n) (toAny x) caches_to },+ MkSym n)+ where+ n = caches_nextId+ cache =+ fromAnyCache $+ Map.findWithDefault Map.empty ty caches_from++-- | Recover the underlying value from a 'Sym'.+unintern :: Sym a -> a+-- N.B. must force n before calling readIORef, otherwise a call of+-- the form+-- unintern (intern x)+-- doesn't work.+unintern (MkSym !(I32# n#)) = uninternWorker n#++{-# NOINLINE uninternWorker #-}+#if __GLASGOW_HASKELL__ >= 902+uninternWorker :: Int32# -> a+#else+uninternWorker :: Int# -> a+#endif+uninternWorker n# =+ unsafeDupablePerformIO $ do+ let n = I32# n#+ Caches{..} <- readIORef cachesRef+ x <- return $! fromAny (DynamicArray.getWithDefault undefined (fromIntegral n) caches_to)+ return x++pattern Sym :: Intern a => a -> Sym a+pattern Sym x <- (unintern -> x) where+ Sym x = intern x
− Data/Label.hs
@@ -1,137 +0,0 @@--- | Assignment of unique IDs to values.--- Inspired by the 'intern' package.--{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns, MagicHash, RoleAnnotations, CPP #-}-module Data.Label(Label, unsafeMkLabel, labelNum, label, find) where--import Data.IORef-import System.IO.Unsafe-import qualified Data.Map.Strict as Map-import Data.Map.Strict(Map)-import qualified Data.DynamicArray as DynamicArray-import Data.DynamicArray(Array)-import Data.Typeable-import GHC.Exts-import GHC.Int-import Unsafe.Coerce---- | A value of type @a@ which has been given a unique ID.-newtype Label a =- Label {- -- | The unique ID of a label.- labelNum :: Int32 }- deriving (Eq, Ord, Show)--type role Label nominal---- | Construct a @'Label' a@ from its unique ID, which must be the 'labelNum' of--- an already existing 'Label'. Extremely unsafe!-unsafeMkLabel :: Int32 -> Label a-unsafeMkLabel = Label---- The global cache of labels.-{-# NOINLINE cachesRef #-}-cachesRef :: IORef Caches-cachesRef = unsafePerformIO (newIORef (Caches 0 Map.empty DynamicArray.newArray))--data Caches =- Caches {- -- The next id number to assign.- caches_nextId :: {-# UNPACK #-} !Int32,- -- A map from values to labels.- caches_from :: !(Map TypeRep (Cache Any)),- -- The reverse map from labels to values.- caches_to :: !(Array Any) }--type Cache a = Map a Int32--atomicModifyCaches :: (Caches -> (Caches, a)) -> IO a-atomicModifyCaches f = do- -- N.B. atomicModifyIORef' ref f evaluates f ref *after* doing the- -- compare-and-swap. This causes bad things to happen when 'label'- -- is used reentrantly (i.e. the Ord instance itself calls label).- -- This function only lets the swap happen if caches_nextId didn't- -- change (i.e., no new values were inserted).- !caches <- readIORef cachesRef- -- First compute the update.- let !(!caches', !x) = f caches- -- Now see if anyone else updated the cache in between- -- (can happen if f called 'label', or in a concurrent setting).- ok <- atomicModifyIORef' cachesRef $ \cachesNow ->- if caches_nextId caches == caches_nextId cachesNow- then (caches', True)- else (cachesNow, False)- if ok then return x else atomicModifyCaches f---- Versions of unsafeCoerce with slightly more type checking-toAnyCache :: Cache a -> Cache Any-toAnyCache = unsafeCoerce--fromAnyCache :: Cache Any -> Cache a-fromAnyCache = unsafeCoerce--toAny :: a -> Any-toAny = unsafeCoerce--fromAny :: Any -> a-fromAny = unsafeCoerce---- | Assign a label to a value.-{-# NOINLINE label #-}-label :: forall a. (Typeable a, Ord a) => a -> Label a-label x =- unsafeDupablePerformIO $ do- -- Common case: label is already there.- caches <- readIORef cachesRef- case tryFind caches of- Just l -> return l- Nothing -> do- -- Rare case: label was not there.- x <- atomicModifyCaches $ \caches ->- case tryFind caches of- Just l -> (caches, l)- Nothing ->- insert caches- return x-- where- ty = typeOf x-- tryFind :: Caches -> Maybe (Label a)- tryFind Caches{..} =- Label <$> (Map.lookup ty caches_from >>= Map.lookup x . fromAnyCache)-- insert :: Caches -> (Caches, Label a)- insert caches@Caches{..} =- if n < 0 then error "label overflow" else- (caches {- caches_nextId = n+1,- caches_from = Map.insert ty (toAnyCache (Map.insert x n cache)) caches_from,- caches_to = DynamicArray.updateWithDefault undefined (fromIntegral n) (toAny x) caches_to },- Label n)- where- n = caches_nextId- cache =- fromAnyCache $- Map.findWithDefault Map.empty ty caches_from---- | Recover the underlying value from a label.-find :: Label a -> a--- N.B. must force n before calling readIORef, otherwise a call of--- the form--- find (label x)--- doesn't work.-find (Label !(I32# n#)) = findWorker n#--{-# NOINLINE findWorker #-}-#if __GLASGOW_HASKELL__ >= 902-findWorker :: Int32# -> a-#else-findWorker :: Int# -> a-#endif-findWorker n# =- unsafeDupablePerformIO $ do- let n = I32# n#- Caches{..} <- readIORef cachesRef- x <- return $! fromAny (DynamicArray.getWithDefault undefined (fromIntegral n) caches_to)- return x
Twee.hs view
@@ -56,6 +56,7 @@ cfg_max_critical_pairs :: Int64, cfg_max_cp_depth :: Int, cfg_max_rules :: Int,+ cfg_max_time :: Maybe Double, cfg_simplify :: Bool, cfg_renormalise_percent :: Int, cfg_cp_sample_size :: Int,@@ -63,7 +64,7 @@ cfg_set_join_goals :: Bool, cfg_always_simplify :: Bool, cfg_complete_subsets :: Bool,- cfg_score_cp :: Depth -> Equation f -> Float,+ cfg_score_cp :: Depth -> Index f (Hint f) -> Equation f -> Float, cfg_join :: Join.Config, cfg_proof_presentation :: Proof.Config f, cfg_eliminate_axioms :: [Axiom f],@@ -71,7 +72,10 @@ cfg_random_mode_goal_directed :: Bool, cfg_random_mode_simple :: Bool, cfg_random_mode_best_of :: Int,- cfg_always_complete :: Bool }+ cfg_always_complete :: Bool,+ cfg_hint_skel_cost :: Float,+ cfg_hint_skel_factor :: Float,+ cfg_print_score :: Bool } -- | The prover state. data State f =@@ -82,6 +86,7 @@ st_joinable :: !(Index f (Equation f)), st_goals :: ![Goal f], st_queue :: !(Queue Batch),+ st_hints :: !(Index f (Hint f)), st_next_active :: {-# UNPACK #-} !Id, st_considered :: {-# UNPACK #-} !Int64, st_simplified_at :: {-# UNPACK #-} !Id,@@ -100,6 +105,7 @@ cfg_max_critical_pairs = maxBound, cfg_max_cp_depth = maxBound, cfg_max_rules = maxBound,+ cfg_max_time = Nothing, cfg_simplify = True, cfg_renormalise_percent = 5, cfg_renormalise_threshold = 20,@@ -107,7 +113,7 @@ cfg_set_join_goals = True, cfg_always_simplify = False, cfg_complete_subsets = False,- cfg_score_cp = \d eqn -> fromIntegral (score CP.defaultConfig d eqn),+ cfg_score_cp = \d hints eqn -> score CP.defaultConfig d hints eqn, cfg_join = Join.defaultConfig, cfg_proof_presentation = Proof.defaultConfig, cfg_eliminate_axioms = [],@@ -115,12 +121,16 @@ cfg_random_mode_goal_directed = False, cfg_random_mode_best_of = 1, cfg_random_mode_simple = False,- cfg_always_complete = False }+ cfg_always_complete = False,+ cfg_hint_skel_cost = 1,+ cfg_hint_skel_factor = 0,+ cfg_print_score = False } -- | Does this configuration run the prover in a complete mode? configIsComplete :: Config f -> Bool configIsComplete Config{..} =- isNothing (cfg_accept_term) &&+ isNothing cfg_accept_term &&+ isNothing cfg_max_time && cfg_max_critical_pairs == maxBound && cfg_max_cp_depth == maxBound && cfg_max_rules == maxBound@@ -135,6 +145,7 @@ st_joinable = Index.empty, st_goals = [], st_queue = Queue.empty,+ st_hints = Index.empty, st_next_active = 1, st_considered = 0, st_simplified_at = 1,@@ -155,7 +166,7 @@ -- | A message which is produced by the prover when something interesting happens. data Message f = -- | A new rule.- NewActive !(Active f)+ NewActive !(Maybe Float) !(Active f) -- | A new joinable equation. | NewEquation !(Equation f) -- | A rule was deleted.@@ -172,7 +183,10 @@ | NewProblemTerm !(ConfluenceFailure f) instance Function f => Pretty (Message f) where- pPrint (NewActive rule) = pPrint rule+ pPrint (NewActive mscore rule) =+ case mscore of+ Nothing -> pPrint rule+ Just score -> parens (pPrint score) <+> 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@@ -225,10 +239,10 @@ 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 =+makePassives config@Config{..} state@State{..} rule = -- XXX factor out depth calculation stampWith "make critical pair" length- [ makePassive config overlap+ [ makePassive config state overlap | ok rule, overlap <- overlaps (index_oriented st_rules) (filter ok rules) rule ] where@@ -296,10 +310,10 @@ batchSize Batch{..} = 1 + PackedSequence.size batch_rest {-# INLINEABLE makePassive #-}-makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive-makePassive Config{..} Overlap{..} =+makePassive :: Function f => Config f -> State f -> Overlap (Active f) f -> Passive+makePassive Config{..} State{..} Overlap{..} = Passive {- passive_score = cfg_score_cp depth overlap_eqn,+ passive_score = cfg_score_cp depth st_hints overlap_eqn, passive_rule1 = active_id overlap_rule1, passive_rule2 = active_id overlap_rule2, passive_how = overlap_how }@@ -328,7 +342,7 @@ passive_score = passive_score passive `min` -- XXX factor out depth calculation- cfg_score_cp (succ (the r1 `max` the r2)) (overlap_eqn overlap) }+ cfg_score_cp (succ (the r1 `max` the r2)) st_hints (overlap_eqn overlap) } -- | Check if we should renormalise the queue. {-# INLINEABLE shouldSimplifyQueue #-}@@ -407,6 +421,10 @@ cp_top = active_top, cp_proof = derivation active_proof } +activeScore :: Config f -> State f -> Active f -> Float+activeScore Config{..} State{..} Active{..} =+ cfg_score_cp (info_depth active_info) st_hints (equation active_proof)+ activeRules :: Active f -> [Rule f] activeRules Active{..} = case active_positions of@@ -436,8 +454,11 @@ addActive config state@State{..} active0 = let active@Active{..} = active0 st_next_active+ mscore+ | cfg_print_score config = Just (activeScore config state active)+ | otherwise = Nothing state' =- message (NewActive active) $+ message (NewActive mscore active) $ addActiveOnly state{st_next_active = st_next_active+1} active in if subsumed (st_joinable, st_complete) st_rules (unorient active_rule) then state@@ -497,6 +518,16 @@ insertRule rules rule = RuleIndex.insert (lhs rule) rule rules +-- Add an active without generating critical pairs. Used in interreduction.+{-# INLINEABLE addActiveSimp #-}+addActiveSimp :: Function f => State f -> Active f -> State f+addActiveSimp state@State{..} active@Active{..} =+ state {+ st_rules = foldl' insertRule st_rules (activeRules active) }+ where+ insertRule rules rule =+ RuleIndex.insert (lhs rule) rule rules+ -- Delete an active. Used in interreduction, not suitable for general use. {-# INLINE deleteActive #-} deleteActive :: Function f => State f -> Active f -> State f@@ -578,6 +609,16 @@ cp_top = Nothing, cp_proof = Proof.axiom axiom } +-- Add a new hint.+{-# INLINEABLE addHint #-}+addHint :: Function f => Config f -> State f -> Term f -> State f+addHint Config{..} state@State{..} hint =+ state { st_hints = Index.insert hint (Hint hint cost) st_hints }+ where+ cost = fromIntegral (len hint - length (vars hint)) * cfg_hint_skel_factor + cfg_hint_skel_cost ++ -- Add a cost for duplicated variables (since they only get counted once otherwise)+ fromIntegral (length (vars hint) - length (usort (vars hint)))+ -- Record an equation as being joinable. {-# INLINEABLE addJoinable #-} addJoinable :: Function f => State f -> Equation f -> State f@@ -754,11 +795,13 @@ (Just active_model) (active_cp active) of Right (_, cps) ->+ flip addActiveSimp active $ flip (foldl' (\state cp -> consider config state active_info cp)) cps $ message (DeleteActive active) $ deleteActive state active Left (cp, model) | cp_eqn cp `simplerThan` cp_eqn (active_cp active) ->+ flip addActiveSimp active $ flip (foldl' (\state cp -> consider config state active_info cp)) (split cp) $ message (DeleteActive active) $ deleteActive state active@@ -805,6 +848,13 @@ let !n = Queue.size st_queue lift $ output_message (Status n)] + checkTimeout <-+ case cfg_max_time of+ Nothing -> return (return False)+ Just timeout -> do+ task <- newTask timeout 100 (return ())+ return $ fmap isJust (checkTask task)+ let loop = do progress <- StateM.state (complete1 config)@@ -816,7 +866,8 @@ lift $ mapM_ output_message (messages state) StateM.put (clearMessages state) mapM_ checkTask tasks- when progress loop+ timedOut <- checkTimeout+ when (progress && not timedOut) loop loop @@ -898,7 +949,7 @@ 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))+ Just (cfg_score_cp config 0 (st_hints state) (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]
Twee/Base.hs view
@@ -1,18 +1,18 @@ -- | 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, BangPatterns #-}+{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards, BangPatterns, PatternSynonyms #-} module Twee.Base( -- * Re-exported functionality module Twee.Term, module Twee.Pretty, -- * The 'Symbolic' typeclass Symbolic(..), subst, terms,- TermOf, TermListOf, SubstOf, TriangleSubstOf, BuilderOf, FunOf,+ TermOf, TermListOf, SubstOf, TriangleSubstOf, BuilderOf, SymOf, vars, isGround, funs, occ, occVar, occs, nests, canonicalise, renameAvoiding, renameManyAvoiding, freshVar, -- * General-purpose functionality- Id(..), Has(..),+ Id(..), Has(..), Intern, Sym, pattern Sym, -- * Typeclasses- Minimal(..), minimalTerm, isMinimal, erase, eraseExcept, ground,+ Minimal(..), minimalTerm, isMinimal, erase, eraseExcept, ground, skolemise, Ordered(..), lessThan, orientTerms, EqualsBonus(..), isTrueTerm, isFalseTerm, decodeEquality, Strictness(..), Function) where@@ -31,6 +31,7 @@ import Data.Maybe import qualified Data.IntMap.Strict as IntMap import Data.Serialize+import Data.Intern -- | Represents a unique identifier (e.g., for a rule). newtype Id = Id { unId :: Int32 }@@ -72,7 +73,7 @@ -- | A builder compatible with a given 'Symbolic'. type BuilderOf a = Builder (ConstantOf a) -- | The underlying type of function symbols of a given 'Symbolic'.-type FunOf a = Fun (ConstantOf a)+type SymOf a = Sym (ConstantOf a) instance Symbolic (Term f) where type ConstantOf (Term f) = f@@ -136,12 +137,12 @@ -- | Find the function symbols occurring in the argument. {-# INLINE funs #-}-funs :: Symbolic a => a -> [FunOf a]+funs :: Symbolic a => a -> [SymOf a] funs x = [ f | t <- DList.toList (termsDL x), App f _ <- subtermsList t ] -- | Count how many times a function symbol occurs in the argument. {-# INLINE occ #-}-occ :: Symbolic a => FunOf a -> a -> Int+occ :: Symbolic a => SymOf a -> a -> Int occ x t = length (filter (== x) (funs t)) -- | Count how many times a variable occurs in the argument.@@ -154,7 +155,7 @@ occs :: Symbolic a => a -> IntMap.IntMap Int occs = foldl' insert IntMap.empty . funs where- insert !m !f = IntMap.insertWith (+) (fun_id f) 1 m+ insert !m !f = IntMap.insertWith (+) (symId f) 1 m -- | 'nest' from Fuchs, "The application of goal-oriented heuristics -- for proving equational theorems via the unfailing Knuth-Bendix@@ -165,11 +166,11 @@ -- 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 Nil = 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 _ Nil) 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+ let as' = hnest (symId g) (if f == symId 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@@ -214,7 +215,7 @@ -- | Check if a term is the minimal constant. isMinimal :: Minimal f => Term f -> Bool-isMinimal (App f Empty) | f == minimal = True+isMinimal (App f Nil) | f == minimal = True isMinimal _ = False -- | Build the minimal constant as a term.@@ -239,10 +240,14 @@ ground :: (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a ground t = erase (vars t) t +-- | Skolemise the argument.+skolemise :: (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a+skolemise t = subst (\(V x) -> con (skolem x)) t+ -- | For types which have a notion of size. -- | The collection of constraints which the type of function symbols must -- satisfy in order to be used by twee.-type Function f = (Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f)+type Function f = (Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Intern f) -- | A hack for encoding Horn clauses. See 'Twee.CP.Score'. -- The default implementation of 'hasEqualsBonus' should work OK.@@ -254,20 +259,20 @@ isTrue _ = False isFalse _ = False -isFalseTerm, isTrueTerm :: (EqualsBonus f, Labelled f) => Term f -> Bool+isFalseTerm, isTrueTerm :: (EqualsBonus f, Intern 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)))+decodeEquality :: (EqualsBonus f, Intern f) => Term f -> Maybe (Term f, Term f)+decodeEquality (App equals (Cons t (Cons u Nil))) | isEquals equals = Just (t, u) decodeEquality _ = Nothing -instance (Labelled f, EqualsBonus f) => EqualsBonus (Fun f) where- hasEqualsBonus = hasEqualsBonus . fun_value- isEquals = isEquals . fun_value- isTrue = isTrue . fun_value- isFalse = isFalse . fun_value+instance (Intern f, EqualsBonus f) => EqualsBonus (Sym f) where+ hasEqualsBonus = hasEqualsBonus . unintern+ isEquals = isEquals . unintern+ isTrue = isTrue . unintern+ isFalse = isFalse . unintern
Twee/CP.hs view
@@ -6,6 +6,7 @@ import Twee.Base import Twee.Rule import Twee.Index(Index)+import qualified Twee.Index as Index import qualified Data.Set as Set import Control.Monad import Data.List hiding (singleton)@@ -18,6 +19,7 @@ import Data.Bits import Data.Serialize import Data.Int+--import Debug.Trace -- | The set of positions at which a term can have critical overlaps. data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)@@ -33,7 +35,7 @@ positions t = aux 0 Set.empty (singleton t) where -- Consider only general superpositions.- aux !_ !_ Empty = NilP+ aux !_ !_ Nil = NilP aux n m (Cons (Var _) t) = aux (n+1) m t aux n m ConsSym{hd = t@App{}, rest = u} | t `Set.member` m = aux (n+1) m u@@ -196,25 +198,37 @@ -- | The configuration for the critical pair weighting heuristic. data Config = Config {- cfg_lhsweight :: !Int,- cfg_rhsweight :: !Int,- cfg_funweight :: !Int,- cfg_varweight :: !Int,- cfg_depthweight :: !Int,- cfg_dupcost :: !Int,- cfg_dupfactor :: !Int }+ cfg_lhsweight :: !Float,+ cfg_rhsweight :: !Float,+ cfg_funweight :: !Float,+ cfg_varweight :: !Float,+ cfg_depthweight :: !Float,+ cfg_dupcost :: !Float,+ cfg_dupfactor :: !Float,+ cfg_resonance :: !Bool } +data Hint f =+ Hint {+ hint_term :: {-# UNPACK #-} !(Term f),+ hint_cost :: {-# UNPACK #-} !Float }++instance Symbolic (Hint f) where+ type ConstantOf (Hint f) = f+ termsDL Hint{..} = termsDL hint_term+ subst_ sub (Hint t c) = Hint (subst_ sub t) c+ -- | The default heuristic configuration. defaultConfig :: Config defaultConfig = Config { cfg_lhsweight = 4, cfg_rhsweight = 1,- cfg_funweight = 7,- cfg_varweight = 6,- cfg_depthweight = 16,- cfg_dupcost = 7,- cfg_dupfactor = 0 }+ cfg_funweight = 1,+ cfg_varweight = 6/7,+ cfg_depthweight = 2,+ cfg_dupcost = 1,+ cfg_dupfactor = 0,+ cfg_resonance = False } -- | Compute a score for a critical pair. @@ -223,31 +237,40 @@ -- 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 -> Equation f -> Int-score Config{..} depth (l :=: r) =+score :: Function f => Config -> Depth -> Index f (Hint f) -> Equation f -> Float+score Config{..} depth hints (l :=: r) = fromIntegral depth * cfg_depthweight + (m + n) * cfg_rhsweight +- intMax m n * (cfg_lhsweight - cfg_rhsweight)+ max m n * (cfg_lhsweight - cfg_rhsweight) where- m = size' 0 (singleton l)- n = size' 0 (singleton r)+ m = size' 0 (singleton l) []+ n = size' 0 (singleton r) [] - size' !n Empty = n- size' n (Cons t ts)- | len t > 1, t `isSubtermOfList` ts =- size' (n+cfg_dupcost+cfg_dupfactor*len t) ts- size' n ts+ size' !_ !_ !_ | False = undefined+ size' n Nil ts =+ case ts of+ [] -> n+ u:us -> size' n u us+ size' n (Cons t ts) us+ | len t > 1, t `isSubtermOfList` ts || any (t `isSubtermOfList`) us =+ size' (n+cfg_dupcost+cfg_dupfactor*fromIntegral (len t)) ts us+ size' n (Cons t ts) us+ | len t > 1, (sub, Hint{..}):_ <- Index.matches t hints,+ not cfg_resonance || allSubst (\_ t -> case t of { UnsafeCons (Var _) _ -> True; _ -> False }) sub =+ size' (n + hint_cost) ts (map snd (Term.substToList' sub) ++ us)+ --trace ("hint: len " ++ show (len t) ++ ", new cost " ++ show new_cost ++ ": " ++ prettyShow t) $+ size' n ts xs | Cons (App f ws@(Cons a (Cons b us))) vs <- ts, not (isVar a), not (isVar b),- hasEqualsBonus (fun_value f),+ hasEqualsBonus f, Just sub <- unify a b =- size' (n+cfg_funweight) ws `min`- size' (size' (n+1) (subst sub us)) (subst sub vs)- size' n (Cons (Var _) ts) =- size' (n+cfg_varweight) ts- size' n ConsSym{hd = App{}, rest = ts} =- size' (n+cfg_funweight) ts+ size' (n+cfg_funweight) ws xs `min`+ size' (n+1) (subst sub us) (subst sub (vs:xs))+ size' n (Cons (Var _) ts) us =+ size' (n+cfg_varweight) ts us+ size' n ConsSym{hd = App{}, rest = ts} us =+ size' (n+cfg_funweight) ts us ---------------------------------------------------------------------- -- * Higher-level handling of critical pairs.@@ -274,7 +297,7 @@ cp_top = subst_ sub cp_top, cp_proof = subst_ sub cp_proof } -instance (Labelled f, PrettyTerm f) => Pretty (CriticalPair f) where+instance (Intern f, PrettyTerm f) => Pretty (CriticalPair f) where pPrint CriticalPair{..} = vcat [ pPrint cp_eqn,
Twee/Constraints.hs view
@@ -14,15 +14,19 @@ import Data.Map.Strict(Map) import Data.Ord import Twee.Term hiding (lookup)+import Test.QuickCheck(shuffle)+import Test.QuickCheck.Gen(unGen)+import Test.QuickCheck.Random(mkQCGen)+import Data.Intern -data Atom f = Constant (Fun f) | Variable Var deriving (Show, Eq, Ord)+data Atom f = Constant (Sym f) | Variable Var deriving (Show, Eq, Ord) {-# INLINE atoms #-} atoms :: Term f -> [Atom f] atoms t = aux (singleton t) where- aux Empty = []- aux (Cons (App f Empty) t) = Constant f:aux t+ aux Nil = []+ aux (Cons (App f Nil) t) = Constant f:aux t aux (Cons (Var x) t) = Variable x:aux t aux ConsSym{rest = t} = aux t @@ -31,11 +35,11 @@ toTerm (Variable x) = build (var x) fromTerm :: Flat.Term f -> Maybe (Atom f)-fromTerm (App f Empty) = Just (Constant f)+fromTerm (App f Nil) = Just (Constant f) fromTerm (Var x) = Just (Variable x) fromTerm _ = Nothing -instance (Labelled f, PrettyTerm f) => Pretty (Atom f) where+instance (Intern f, PrettyTerm f) => Pretty (Atom f) where pPrint = pPrint . toTerm data Formula f =@@ -45,7 +49,7 @@ | Or [Formula f] deriving (Eq, Ord, Show) -instance (Labelled f, PrettyTerm f) => Pretty (Formula f) where+instance (Intern 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"@@ -98,12 +102,12 @@ data Branch f = -- Branches are kept normalised wrt equals Branch {- funs :: [Fun f],+ funs :: [Sym f], less :: [(Atom f, Atom f)], -- sorted equals :: [(Atom f, Atom f)] } -- sorted, greatest atom first in each pair deriving (Eq, Ord) -instance (Labelled f, PrettyTerm f) => Pretty (Branch f) where+instance (Intern f, PrettyTerm f) => Pretty (Branch f) where pPrint Branch{..} = braces $ fsep $ punctuate (text ",") $ [pPrint x <+> text "<" <+> pPrint y | (x, y) <- less ] ++@@ -115,7 +119,7 @@ norm :: Eq f => Branch f -> Atom f -> Atom f norm Branch{..} x = fromMaybe x (lookup x equals) -contradictory :: (Minimal f, Ord f, Labelled f) => Branch f -> Bool+contradictory :: (Minimal f, Ord f, Intern f) => Branch f -> Bool contradictory Branch{..} = or [f == minimal | (_, Constant f) <- less] || or [f /= g | (Constant f, Constant g) <- equals] ||@@ -125,7 +129,7 @@ cyclic (AcyclicSCC _) = False cyclic (CyclicSCC _) = True -formAnd :: (Minimal f, Ordered f, Labelled f) => Formula f -> [Branch f] -> [Branch f]+formAnd :: (Minimal f, Ordered f, Intern f) => Formula f -> [Branch f] -> [Branch f] formAnd f bs = usort (bs >>= add f) where add (Less t u) b = addLess t u b@@ -134,7 +138,7 @@ add (And (f:fs)) b = add f b >>= add (And fs) add (Or fs) b = usort (concat [ add f b | f <- fs ]) -branches :: (Minimal f, Ordered f, Labelled f) => Formula f -> [Branch f]+branches :: (Minimal f, Ordered f, Intern f) => Formula f -> [Branch f] branches x = aux [x] where aux [] = [Branch [] [] []]@@ -146,7 +150,7 @@ concatMap (addLess t u) (aux xs) ++ concatMap (addEquals u t) (aux xs) -addLess :: (Minimal f, Ordered f, Labelled f) => Atom f -> Atom f -> Branch f -> [Branch f]+addLess :: (Minimal f, Ordered f, Intern f) => Atom f -> Atom f -> Branch f -> [Branch f] addLess _ (Constant min) _ | min == minimal = [] addLess (Constant min) _ b | min == minimal = [b] addLess t0 u0 b@Branch{..} =@@ -156,7 +160,7 @@ t = norm b t0 u = norm b u0 -addEquals :: (Minimal f, Ordered f, Labelled f) => Atom f -> Atom f -> Branch f -> [Branch f]+addEquals :: (Minimal f, Ordered f, Intern f) => Atom f -> Atom f -> Branch f -> [Branch f] addEquals t0 u0 b@Branch{..} | t == u || (t, u) `elem` equals = [b] | otherwise =@@ -172,7 +176,7 @@ | x == t = u | otherwise = x -addTerm :: (Minimal f, Ordered f, Labelled f) => Atom f -> Branch f -> Branch f+addTerm :: (Minimal f, Ordered f, Intern f) => Atom f -> Branch f -> Branch f addTerm (Constant f) b | f `notElem` funs b = b {@@ -189,7 +193,7 @@ -- x < y if major x < major y -- x <= y if major x = major y and minor x < minor y -instance (Labelled f, PrettyTerm f) => Pretty (Model f) where+instance (Intern 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)))@@ -233,7 +237,14 @@ varInModel :: (Minimal f, Ord f) => Model f -> Var -> Bool varInModel (Model m) x = Variable x `Map.member` m -varGroups :: (Minimal f, Ord f) => Model f -> [(Fun f, [Var], Maybe (Fun f))]+modelVarMaxBound :: Model f -> Int+modelVarMaxBound (Model m) =+ maximum (0:map (succ . fst) (Map.elems m))++modelVarValue :: Model f -> Var -> Maybe Var+modelVarValue (Model m) x = V . fst <$> Map.lookup (Variable x) m++varGroups :: (Minimal f, Ord f) => Model f -> [(Sym f, [Var], Maybe (Sym f))] varGroups (Model m) = filter nonempty (go minimal (map fst (sortBy (comparing snd) (Map.toList m)))) where go f xs =@@ -248,10 +259,11 @@ nonempty _ = True class Minimal f where- minimal :: Fun f+ minimal :: Sym f+ skolem :: Int -> Sym f {-# INLINE lessEqInModel #-}-lessEqInModel :: (Minimal f, Ordered f, Labelled f) => Model f -> Atom f -> Atom f -> Maybe Strictness+lessEqInModel :: (Minimal f, Ordered f, Intern f) => Model f -> Atom f -> Atom f -> Maybe Strictness lessEqInModel (Model m) x y | Just (a, _) <- Map.lookup x m, Just (b, _) <- Map.lookup y m,@@ -264,7 +276,7 @@ | Constant a <- x, a == minimal = Just Nonstrict | otherwise = Nothing -solve :: (Minimal f, Ordered f, PrettyTerm f, Labelled f) => [Atom f] -> Branch f -> Either (Model f) (Subst f)+solve :: (Minimal f, Ordered f, PrettyTerm f, Intern f) => [Atom f] -> Branch f -> Either (Model f) (Subst f) solve xs branch@Branch{..} | null equals && not (all true less) = error $ "Model " ++ prettyShow model ++ " is not a model of " ++ prettyShow branch ++ " (edges = " ++ prettyShow edges ++ ", vs = " ++ prettyShow vs ++ ")"@@ -274,8 +286,9 @@ sub = fromMaybe undefined . listToSubst $ [(x, toTerm y) | (Variable x, y) <- equals] ++ [(y, toTerm x) | (x@Constant{}, Variable y) <- equals]- vs = Constant minimal:reverse (flattenSCCs (stronglyConnComp edges))+ vs = Constant minimal:reverse (flattenSCCs (stronglyConnComp edges')) edges = [(x, x, [y | (x', y) <- less', x == x']) | x <- as, x /= Constant minimal]+ edges' = unGen (shuffle edges) (mkQCGen 12345) 0 less' = less ++ [(Constant x, Constant y) | Constant x <- as, Constant y <- as, x << y] as = usort $ xs ++ map fst less ++ map snd less model = modelFromOrder vs
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 (Labelled f, PrettyTerm f) => Pretty (Equation f) where+instance (Intern f, PrettyTerm f) => Pretty (Equation f) where pPrint (x :=: y) = pPrint x <+> text "=" <+> pPrint y -- | Order an equation roughly left-to-right, and@@ -32,15 +32,15 @@ -- If the two terms have the same skeleton, -- then take whichever orientation gives a simpler equation | gl == gr =- let eq1 = canonicalise (l :=: r)- eq2 = canonicalise (r :=: l) in if eq1 == eq2 || orderedSimplerThan eq1 eq2 then eq1 else eq2 -- Otherwise, the LHS should be the term with the greater skeleton- | gl `lessEq` gr = r :=: l- | otherwise = l :=: r+ | gl `lessEq` gr = eq2+ | otherwise = eq1 where gl = ground l gr = ground r+ eq1 = canonicalise (l :=: r)+ eq2 = canonicalise (r :=: l) -- Helper for 'order' and 'simplerThan' orderedSimplerThan :: Function f => Equation f -> Equation f -> Bool
Twee/Index.hs view
@@ -22,12 +22,14 @@ delete, lookup, matches,+ member, elems, fromList, fromListWith, invariant) where import Prelude hiding (null, lookup)+import qualified Prelude (null) import Twee.Base hiding (var, fun, empty, singleton, prefix, funs, lookupList, lookup, at) import qualified Twee.Term as Term import Data.DynamicArray hiding (singleton)@@ -36,8 +38,8 @@ import Data.Numbered(Numbered) import qualified Data.Numbered as Numbered import qualified Data.IntMap.Strict as IntMap-import qualified Twee.Term.Core as Core import Twee.Profile+import Data.Intern -- The term index in this module is a _perfect discrimination tree_. -- This is a trie whose keys are terms, represented as flat lists of symbols@@ -93,26 +95,26 @@ -- The array is indexed by function number. fun :: {-# UNPACK #-} !(Array (Index f a)), -- List of variable edges indexed by variable number.- -- Invariant: all edges present in the list are non-Nil.+ -- Invariant: all edges present in the list are non-Empty. -- -- Invariant: variables in terms are introduced in ascending -- order, with no gaps (i.e. if the term so far has the variables -- x1..xn, then the edges here must be drawn from x1...x{n+1}). var :: {-# UNPACK #-} !(Numbered (Index f a)) } | -- An empty index.- Nil+ Empty deriving Show minSize :: Index f a -> Int-minSize Nil = maxBound+minSize Empty = maxBound minSize idx = minSize_ idx -- | Check the invariant of an index. For debugging purposes. invariant :: Index f a -> Bool-invariant Nil = True+invariant Empty = True invariant Index{..} = nonEmpty &&- noNilVars &&+ noEmptyVars && maxPrefix && sizeCorrect && all invariant (map snd (toList fun)) &&@@ -122,7 +124,7 @@ not (List.null here) || not (List.null (filter (not . null . snd) (toList fun))) || not (List.null (Numbered.toList var))- noNilVars = -- the var field should not contain any Nils+ noEmptyVars = -- the var field should not contain any Emptys all (not . null . snd) (Numbered.toList var) maxPrefix -- prefix should be used if possible | List.null here =@@ -137,15 +139,15 @@ | otherwise = minSize_ == lenList prefix -instance Default (Index f a) where def = Nil+instance Default (Index f a) where def = Empty -- | An empty index. empty :: Index f a-empty = Nil+empty = Empty -- | Is the index empty? null :: Index f a -> Bool-null Nil = True+null Empty = True null _ = False -- | An index with one entry.@@ -154,12 +156,12 @@ -- A leaf node, perhaps with a prefix. leaf :: TermList f -> [a] -> Index f a-leaf !_ [] = Nil+leaf !_ [] = Empty leaf t xs = Index (lenList t) t xs newArray Numbered.empty -- Add a prefix (given as a list of symbols) to all terms in an index. addPrefix :: [Term f] -> Index f a -> Index f a-addPrefix _ Nil = Nil+addPrefix _ Empty = Empty addPrefix [] idx = idx addPrefix ts idx = idx {@@ -174,10 +176,10 @@ index here fun var = case (here, fun', Numbered.toList var') of ([], [], []) ->- Nil+ Empty ([], [(f, idx)], []) -> idx{minSize_ = succ (minSize_ idx),- prefix = buildList (con (Core.F f) `mappend` builder (prefix idx))}+ prefix = buildList (con (unsafeMkSym f) `mappend` builder (prefix idx))} ([], [], [(x, idx)]) -> idx{minSize_ = succ (minSize_ idx), prefix = buildList (Term.var (V x) `mappend` builder (prefix idx))}@@ -216,7 +218,7 @@ where (!t, !v) = canonicalise (t0, v0) - aux [] t Nil =+ aux [] t Empty = leaf t (f v []) -- Non-empty prefix@@ -233,18 +235,18 @@ aux syms@(_:_) t idx = addPrefix (reverse syms) $ aux [] t idx - -- Empty prefix- aux [] Empty idx =+ -- Nil prefix+ aux [] Nil idx = index (f v (here idx)) (fun idx) (var idx) aux [] ConsSym{hd = App f _, rest = u} idx = index (here idx)- (update (fun_id f) idx' (fun idx))+ (update (symId f) idx' (fun idx)) (var idx) where- idx' = aux [] u (fun idx ! fun_id f)+ idx' = aux [] u (fun idx ! symId f) aux [] ConsSym{hd = Var x, rest = u} idx = index (here idx) (fun idx)- (Numbered.modify (var_id x) Nil (aux [] u) (var idx))+ (Numbered.modify (var_id x) Empty (aux [] u) (var idx)) -- Helper for modify: -- Take an index with a prefix and pull out the first symbol of the prefix,@@ -265,7 +267,7 @@ minSize_ = size, prefix = Term.empty, here = [],- fun = Array.singleton (fun_id f) idx { prefix = ts, minSize_ = size - 1 },+ fun = Array.singleton (symId f) idx { prefix = ts, minSize_ = size - 1 }, var = Numbered.empty } -- | Look up a term in the index. Finds all key-value such that the search term@@ -292,9 +294,13 @@ matchesList t idx = run (search t emptyBindings idx Stop) +-- | Check if a term is present in the index.+member :: Term f -> Index f a -> Bool+member t idx = not (Prelude.null (matches t idx))+ -- | Return all elements of the index. elems :: Index f a -> [a]-elems Nil = []+elems Empty = [] elems idx = here idx ++ concatMap elems (map snd (toList (fun idx))) ++@@ -402,7 +408,7 @@ search !_ !_ !_ _ | False = undefined search t binds idx rest = case idx of- Nil -> rest+ Empty -> rest Index{..} | lenList t < minSize idx -> rest -- the search term is smaller than any in this index@@ -442,7 +448,7 @@ -- We've exhausted the prefix, so let's descend into the tree. -- Seems to work better to explore the function node first. case thd of- App f _ | idx@Index{} <- fun ! fun_id f ->+ App f _ | idx@Index{} <- fun ! symId f -> -- Avoid creating a frame unnecessarily. case Numbered.size var of 0 -> search trest binds idx rest@@ -453,7 +459,7 @@ _ -> searchVars thd ttl binds var 0 rest _ -> case prefix of- Empty ->+ Nil -> -- The search term matches this node. case here of [] -> rest
Twee/Join.hs view
@@ -22,7 +22,9 @@ cfg_ground_join :: !Bool, cfg_use_connectedness_standalone :: !Bool, cfg_use_connectedness_in_ground_joining :: !Bool,- cfg_set_join :: !Bool }+ cfg_set_join :: !Bool,+ cfg_ground_join_limit :: !Int,+ cfg_ground_join_incomplete_limit :: !Int } defaultConfig :: Config defaultConfig =@@ -30,7 +32,9 @@ cfg_ground_join = True, cfg_use_connectedness_standalone = True, cfg_use_connectedness_in_ground_joining = False,- cfg_set_join = False }+ cfg_set_join = False,+ cfg_ground_join_limit = maxBound,+ cfg_ground_join_incomplete_limit = maxBound } {-# INLINEABLE joinCriticalPair #-} joinCriticalPair ::@@ -58,9 +62,9 @@ (normalForms (rewrite reduces (index_all idx)) (Map.singleton u []))) -> Right (Just cp, []) Just cp ->- case groundJoinFromMaybe config eqns idx mmodel (branches (And [])) cp of- Left model -> Left (cp, model)- Right (mcp, cps) -> Right (mcp, cps)+ case groundJoinFromMaybe config 0 eqns idx mmodel (branches (And [])) cp of+ (_, Left model) -> Left (cp, model)+ (_, Right (mcp, cps)) -> Right (mcp, cps) {-# INLINEABLE step1 #-} {-# INLINEABLE step2 #-}@@ -141,7 +145,8 @@ (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Equation f -> Bool subsumed (eqns, complete) idx (t :=: u) | t == u = True- | otherwise = subsumed1 eqns idx (norm t :=: norm u)+ | norm t == norm u = True+ | otherwise = subsumed1 eqns idx (t :=: u) where norm t | Index.null complete = t@@ -157,7 +162,7 @@ subsumed1 eqns idx (App f ts :=: App g us) | f == g = let- sub Empty Empty = True+ sub Nil Nil = True sub (Cons t ts) (Cons u us) = subsumed1 eqns idx (t :=: u) && sub ts us sub _ _ = error "Function used with multiple arities"@@ -168,22 +173,25 @@ {-# INLINEABLE groundJoin #-} groundJoin :: (Function f, Has a (Rule f)) =>- Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])-groundJoin config eqns idx ctx cp@CriticalPair{cp_eqn = t :=: u, ..} =+ Config -> Int -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> [Branch f] -> CriticalPair f -> (Int, Either (Model f) (Maybe (CriticalPair f), [CriticalPair f]))+groundJoin config ticks _ _ _ cp+ | ticks >= cfg_ground_join_incomplete_limit config =+ (ticks, Right (Just cp, []))+groundJoin config ticks eqns idx ctx cp@CriticalPair{cp_eqn = t :=: u, ..} = case partitionEithers (map (solve (usort (atoms t ++ atoms u))) ctx) of ([], instances) -> let cps = [ subst sub cp | sub <- instances ] in- Right (Just cp, usortBy (comparing (order . cp_eqn)) cps)+ (ticks, Right (Just cp, usortBy (comparing (order . cp_eqn)) cps)) (model:_, _) ->- groundJoinFrom config eqns idx model ctx cp+ groundJoinFrom config (ticks+1) eqns idx model ctx cp {-# INLINEABLE groundJoinFrom #-} groundJoinFrom :: (Function f, Has a (Rule f)) =>- Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Model f -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])-groundJoinFrom config@Config{..} eqns idx model ctx cp@CriticalPair{cp_eqn = t :=: u, ..}- | not cfg_ground_join = Left model- | modelOK model && isJust (allSteps config' eqns idx cp { cp_eqn = t' :=: u' }) = Left model+ Config -> Int -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Model f -> [Branch f] -> CriticalPair f -> (Int, Either (Model f) (Maybe (CriticalPair f), [CriticalPair f]))+groundJoinFrom config@Config{..} ticks eqns idx model ctx cp@CriticalPair{cp_eqn = t :=: u, ..}+ | ticks >= cfg_ground_join_limit || not cfg_ground_join = (ticks, Left model)+ | modelOK model && isJust (allSteps config' eqns idx cp { cp_eqn = t' :=: u' }) = (ticks, Left model) | otherwise = let model'@@ -199,9 +207,9 @@ weaken x = x ctx' = formAnd (diag (modelToLiterals model')) ctx in - case groundJoin config eqns idx ctx' cp of- Right (_, cps) | not (modelOK model) ->- Right (Nothing, cps)+ case groundJoin config ticks eqns idx ctx' cp of+ (ticks', Right (_, cps)) | not (modelOK model) ->+ (ticks', Right (Nothing, cps)) res -> res where config' = config{cfg_use_connectedness_standalone = False}@@ -211,10 +219,23 @@ normaliseWith (connectedIn m top) (rewrite (ok t u model) (index_all idx)) t _ -> normaliseWith (const True) (rewrite (ok t u m) (index_all idx)) t ok t u m rule sub =- reducesInModel m rule sub &&- unorient rule `simplerThan` (t :=: u)+ case cp_top of+ Just top | cfg_use_connectedness_in_ground_joining ->+ reducesWith lessEqSkolemModel rule sub &&+ unorient rule `simplerThan` (t :=: u)+ _ ->+ reducesInModel m rule sub &&+ unorient rule `simplerThan` (t :=: u) connectedIn m top t = lessIn m t top == Just Strict+ lessEqSkolemModel t u =+ lessEqSkolem (subst reorderVars t) (subst reorderVars u)+ reorderVars x =+ var $+ case modelVarValue model x of+ Nothing -> V (var_id x + firstUnusedVar)+ Just y -> y+ firstUnusedVar = modelVarMaxBound model nt = normaliseIn model t u nu = normaliseIn model u t@@ -230,9 +251,9 @@ {-# INLINEABLE groundJoinFromMaybe #-} groundJoinFromMaybe :: (Function f, Has a (Rule f)) =>- Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Maybe (Model f) -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])-groundJoinFromMaybe config eqns idx Nothing = groundJoin config eqns idx-groundJoinFromMaybe config eqns idx (Just model) = groundJoinFrom config eqns idx model+ Config -> Int -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Maybe (Model f) -> [Branch f] -> CriticalPair f -> (Int, Either (Model f) (Maybe (CriticalPair f), [CriticalPair f]))+groundJoinFromMaybe config ticks eqns idx Nothing = groundJoin config ticks eqns idx+groundJoinFromMaybe config ticks eqns idx (Just model) = groundJoinFrom config ticks eqns idx model {-# INLINEABLE valid #-} valid :: Function f => Model f -> Reduction f -> Bool
Twee/KBO.hs view
@@ -11,6 +11,7 @@ import Data.Maybe import Control.Monad import Twee.Utils+import Data.Intern lessEqSkolem :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool lessEqSkolem !t !u@@ -19,19 +20,19 @@ where m = size t n = size u-lessEqSkolem (App x Empty) _+lessEqSkolem (App x Nil) _ | x == minimal = True-lessEqSkolem _ (App x Empty)+lessEqSkolem _ (App x Nil) | x == minimal = False lessEqSkolem (Var x) (Var y) = x <= y lessEqSkolem (Var _) _ = True lessEqSkolem _ (Var _) = False-lessEqSkolem (App (F _ f) ts) (App (F _ g) us) =+lessEqSkolem (App (Sym f) ts) (App (Sym g) us) = case compare f g of LT -> True GT -> False EQ ->- let loop Empty Empty = True+ let loop Nil Nil = True loop (Cons t ts) (Cons u us) | t == u = loop ts us | otherwise = lessEqSkolem t u@@ -39,7 +40,7 @@ -- | Check if one term is less than another in KBO. lessEq :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool-lessEq (App f Empty) _ | f == minimal = True+lessEq (App f Nil) _ | f == minimal = True lessEq (Var x) (Var y) | x == y = True lessEq _ (Var _) = False lessEq (Var x) t = x `elem` vars t@@ -49,7 +50,7 @@ (st == su && f == g && lexLess ts us)) && xs `lessVars` ys where- lexLess Empty Empty = True+ lexLess Nil Nil = True lexLess (Cons t ts) (Cons u us) | t == u = lexLess ts us | otherwise =@@ -57,7 +58,7 @@ case unify t u of Nothing -> True Just sub- | not (allSubst (\_ (Cons t Empty) -> isMinimal t) sub) -> error "weird term inequality"+ | not (allSubst (\_ (Cons t Nil) -> isMinimal t) sub) -> error "weird term inequality" | otherwise -> lexLess (subst sub ts) (subst sub us) lexLess _ _ = error "incorrect function arity" xs = weightedVars t@@ -138,7 +139,7 @@ | f << g = Just Strict | otherwise = Nothing where- loop Empty Empty = Just Nonstrict+ loop Nil Nil = Just Nonstrict loop (Cons t ts) (Cons u us) | t == u = loop ts us | otherwise =@@ -159,30 +160,30 @@ class Weighted f where argWeight :: f -> Integer -instance (Weighted f, Labelled f) => Weighted (Fun f) where- argWeight = argWeight . fun_value+instance (Weighted f, Intern f) => Weighted (Sym f) where+ argWeight = argWeight . unintern -weightedVars :: (Weighted f, Labelled f) => Term f -> [(Var, Integer)]+weightedVars :: (Weighted f, Intern f) => Term f -> [(Var, Integer)] weightedVars t = collate sum (loop 1 t) where loop k (Var x) = [(x, k)] loop k (App f ts) = concatMap (loop (k * argWeight f)) (unpack ts) -instance (Labelled f, Sized f) => Sized (Fun f) where- size = size . fun_value+instance (Intern f, Sized f) => Sized (Sym f) where+ size = size . unintern -instance (Labelled f, Sized f, Weighted f) => Sized (TermList f) where+instance (Intern f, Sized f, Weighted f) => Sized (TermList f) where size = aux 0 where- aux n Empty = n+ aux n Nil = n aux n (Cons (App f t) u) = aux (n + size f + argWeight f * size t) u aux n (Cons (Var _) t) = aux (n+1) t -instance (Labelled f, Sized f, Weighted f) => Sized (Term f) where+instance (Intern f, Sized f, Weighted f) => Sized (Term f) where size = size . singleton -instance (Labelled f, Sized f, Weighted f) => Sized (Equation f) where+instance (Intern f, Sized f, Weighted f) => Sized (Equation f) where size (x :=: y) = size x + size y
Twee/Pretty.hs view
@@ -11,6 +11,7 @@ import Data.Set(Set) import Data.Ratio import Twee.Term+import Data.Intern -- * Miscellaneous 'Pretty' instances and utilities. @@ -69,13 +70,13 @@ -- * Pretty-printing of terms. -instance (Pretty f, Labelled f) => Pretty (Fun f) where- pPrintPrec l p = pPrintPrec l p . fun_value+instance (Pretty f, Intern f) => Pretty (Sym f) where+ pPrintPrec l p = pPrintPrec l p . unintern -instance (Labelled f, PrettyTerm f) => Pretty (Term f) where+instance (Intern 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)+ pPrintTerm (termStyle f) l p (pPrint f) (unpack xs) data HighlightedTerm f = HighlightedTerm [ANSICode] (Maybe [Int]) (Term f) @@ -94,12 +95,12 @@ maybeHighlight cs (Just []) d = highlight cs d maybeHighlight _ _ d = d -instance (Labelled f, PrettyTerm f) => Pretty (HighlightedTerm f) where+instance (Intern 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)) = maybeHighlight cs h $- pPrintTerm (termStyle (fun_value f)) l p (pPrint f)+ pPrintTerm (termStyle f) l p (pPrint f) (zipWith annotate [0..] (unpack xs)) where annotate i t =@@ -107,10 +108,10 @@ Just (n:ns) | i == n -> HighlightedTerm cs (Just ns) t _ -> HighlightedTerm cs Nothing t -instance (Labelled f, PrettyTerm f) => Pretty (TermList f) where+instance (Intern f, PrettyTerm f) => Pretty (TermList f) where pPrintPrec _ _ = pPrint . unpack -instance (Labelled f, PrettyTerm f) => Pretty (Subst f) where+instance (Intern f, PrettyTerm f) => Pretty (Subst f) where pPrint sub = text "{" <#> fsep (punctuate (text ",") docs) <#> text "}" where docs =@@ -122,6 +123,9 @@ -- | The style of the function symbol. Defaults to 'curried'. termStyle :: f -> TermStyle termStyle _ = curried++instance (Intern f, PrettyTerm f) => PrettyTerm (Sym f) where+ termStyle = termStyle . unintern -- | Defines how to print out a function symbol. newtype TermStyle =
Twee/Proof.hs view
@@ -8,7 +8,7 @@ lemma, autoSubst, simpleLemma, axiom, symm, trans, cong, congPath, -- * Analysing proofs- simplify, steps, usedLemmas, usedAxioms, usedLemmasAndSubsts, usedAxiomsAndSubsts,+ simplify, steps, stepTerms, usedLemmas, usedAxioms, usedLemmasAndSubsts, usedAxiomsAndSubsts, groundAxiomsAndSubsts, eliminateDefinitions, eliminateDefinitionsFromGoal, simplifyProof, generaliseProof, @@ -64,7 +64,7 @@ -- | Congruence. -- Parallel, i.e., takes a function symbol and one derivation for each -- argument of that function.- | Cong {-# UNPACK #-} !(Fun f) ![Derivation f]+ | Cong {-# UNPACK #-} !(Sym f) ![Derivation f] deriving (Eq, Show) -- | An axiom, which comes without proof.@@ -148,7 +148,7 @@ instance Function f => Pretty (Proof f) where pPrint = pPrintLemma defaultConfig (prettyShow . axiom_number) (prettyShow . equation)-instance (Labelled f, PrettyTerm f) => Pretty (Derivation f) where+instance (Intern 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) =@@ -162,12 +162,12 @@ pPrint (Cong f ps) = text "cong" <#> pPrintTuple (pPrint f:map pPrint ps) -instance (Labelled f, PrettyTerm f) => Pretty (Axiom f) where+instance (Intern f, PrettyTerm f) => Pretty (Axiom f) where pPrint Axiom{..} = text "axiom" <#> pPrintTuple [pPrint axiom_number, text axiom_name, pPrint axiom_eqn] -foldLemmas :: (Labelled f, PrettyTerm f) => (Map (Proof f) a -> Derivation f -> a) -> [Derivation f] -> Map (Proof f) a+foldLemmas :: (Intern 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@@ -247,7 +247,7 @@ Trans p (trans q r) trans p q = Trans p q -cong :: Fun f -> [Derivation f] -> Derivation f+cong :: Sym f -> [Derivation f] -> Derivation f cong f ps = case sequence (map unRefl ps) of Nothing -> Cong f ps@@ -312,6 +312,28 @@ fromSteps (t :=: _) [] = Refl t fromSteps _ ps = foldr1 Trans ps +-- | Given a derivation, compute which terms it goes through.+stepTerms :: Function f => Derivation f -> [Term f]+stepTerms p =+ case steps p of+ [] -> [eqn_lhs (equation (certify p))]+ s:ss ->+ eqn_lhs (equation (certify s)):+ map (eqn_rhs . equation . certify) (s:ss)++-- | Find peak terms in a derivation.+peakTerms :: Function f => Derivation f -> [Term f]+peakTerms = peaks . stepTerms+ where+ peaks [] = []+ peaks [t] = [t]+ peaks (t:u:ts)+ | lessEq t u = peaks (u:ts)+ | lessEq u t = peaks (t:ts)+ | otherwise = t:peaks (u:ts)+ -- TODO do more carefully?+ -- handle this case t --> v <-- u where e.g. t <= u (should still be counted as a peak perhaps)+ -- | Find all lemmas which are used in a derivation. usedLemmas :: Derivation f -> [Proof f] usedLemmas p = map fst (usedLemmasAndSubsts p)@@ -383,7 +405,7 @@ case find (build (app f (map var vs))) of Nothing -> Cong f (map elim ps) Just (rhs, Subst sub) ->- let proof (Cons (Var (V x)) Empty) = qs !! x in+ let proof (Cons (Var (V x)) Nil) = qs !! x in replace (proof <$> sub) rhs where vs = map V [0..length ps-1]@@ -391,7 +413,7 @@ elimSubst (Subst sub) = Subst (singleton <$> term <$> unsingleton <$> sub) where- unsingleton (Cons t Empty) = t+ unsingleton (Cons t Nil) = t term = build . term' term' (Var x) = var x@@ -445,7 +467,13 @@ -- | Print out proofs in colour. cfg_use_colour :: !Bool, -- | Print out which instances of some axioms were used.- cfg_show_uses_of_axioms :: Axiom f -> Bool }+ cfg_show_uses_of_axioms :: Axiom f -> Bool,+ -- | Print out peaks of each lemma.+ cfg_show_peaks :: !Bool,+ -- | Eliminate $equals from the proofs.+ cfg_eliminate_existentials_coding :: !Bool,+ -- | Show which subterm is rewritten.+ cfg_show_subterms :: !Bool } -- | The default configuration. defaultConfig :: Config f@@ -456,7 +484,10 @@ cfg_ground_proof = False, cfg_show_instances = False, cfg_use_colour = False,- cfg_show_uses_of_axioms = const False }+ cfg_show_uses_of_axioms = const False,+ cfg_show_peaks = False,+ cfg_eliminate_existentials_coding = True,+ cfg_show_subterms = False } -- | A proof, with all axioms and lemmas explicitly listed. data Presentation f =@@ -514,8 +545,8 @@ pPrint = pPrintPresentation defaultConfig -- | Simplify and present a proof.-present :: Function f => Config f -> [ProvedGoal f] -> Presentation f-present config@Config{..} goals =+present :: Function f => Config f -> [Proof f] -> [ProvedGoal f] -> Presentation f+present config@Config{..} extraLemmas goals = Presentation axioms lemmas goals' where ps =@@ -523,14 +554,14 @@ simplifyProof config $ map (derivation . pg_proof) goals goals' =- [ decodeGoal (goal{pg_proof = certify p})+ [ decodeGoal config (goal{pg_proof = certify p}) | (goal, p) <- zip goals ps ] axioms = usort $ concatMap (usedAxioms . derivation . pg_proof) goals' ++ concatMap (usedAxioms . derivation) lemmas - lemmas = allLemmas (map (derivation . pg_proof) goals')+ lemmas = allLemmas (map simpleLemma extraLemmas ++ map (derivation . pg_proof) goals') groundProof :: Function f => [Derivation f] -> [Derivation f] groundProof ds@@ -598,9 +629,10 @@ shouldInline p = cfg_no_lemmas || length (filter (not . invisible) (map (equation . certify) (steps (derivation p)))) <= 1 ||- (not cfg_all_lemmas &&- (isJust (decodeEquality (eqn_lhs (equation p))) ||- isJust (decodeEquality (eqn_rhs (equation p)))))+ (cfg_eliminate_existentials_coding &&+ (any (isJust . decodeEquality) [eqn_lhs (equation p), eqn_rhs (equation p)] ||+ any isFalseTerm [eqn_lhs (equation p), eqn_rhs (equation p)] ||+ any isTrueTerm [eqn_lhs (equation p), eqn_rhs (equation p)])) subsuming lem (t :=: u) = subsuming1 lem (t :=: u) ++@@ -742,16 +774,22 @@ pPrintLemma Config{..} axiomNum lemmaNum p | null qs = text "Reflexivity." | equation (certify (fromSteps (equation p) qs)) == equation p =- vcat (zipWith pp hl qs) $$ ppTerm (eqn_rhs (equation p))+ vcat (zipWith pp hl qs) $$ ppTerm (HighlightedTerm [] Nothing) (eqn_rhs (equation p)) | otherwise = error "lemma changed by pretty-printing!" where qs = steps (derivation p) hl = map highlightStep qs+ peaks = Set.fromList (peakTerms (derivation p)) pp _ p | invisible (equation (certify p)) = pPrintEmpty pp h p =- ppTerm (HighlightedTerm [green | cfg_use_colour] (Just h) (eqn_lhs (equation (certify p)))) $$- text "=" <+> highlight [bold | cfg_use_colour] (text "{ by" <+> ppStep p <+> text "}")+ ppTerm (HighlightedTerm [green | cfg_use_colour] (Just h)) (eqn_lhs (equation (certify p))) $$+ text "=" <+> highlight [bold | cfg_use_colour] (text "{" <+> ((text "by" <+> ppStep p) $$ if cfg_show_subterms then subtermInfo else pPrintEmpty) <+> text "}")+ where+ subtermInfo =+ (text "from" <+> pPrint t) $$+ (text "to" <+> pPrint u)+ t :=: u = rewrittenSubterms p highlightStep UseAxiom{} = [] highlightStep UseLemma{} = []@@ -760,8 +798,16 @@ where [(i, p)] = filter (not . isRefl . snd) (zip [0..] ps) - ppTerm t = text " " <#> pPrint t+ rewrittenSubterms (Symm p) = u :=: t+ where+ t :=: u = rewrittenSubterms p+ rewrittenSubterms (Cong _ ps) = rewrittenSubterms p+ where+ [p] = filter (not . isRefl) ps+ rewrittenSubterms p = equation (certify p) + ppTerm decorate t = text " " <#> pPrint (decorate t) <+> (if cfg_show_peaks && t `Set.member` peaks then text "(peak)" else pPrintEmpty)+ ppStep = pp True where pp dir (UseAxiom axiom@Axiom{..} sub) =@@ -826,7 +872,7 @@ [ pPrint x <+> text "=" <+> pPrint t | (x, t) <- substToList sub ], if minimal `elem` funs sub then- text "where" <+> doubleQuotes (pPrint (minimal :: Fun f)) <+>+ text "where" <+> doubleQuotes (pPrint (minimal :: Sym f)) <+> text "stands for an arbitrary term of your choice." else pPrintEmpty, text ""]@@ -895,9 +941,9 @@ -- Tries to transform a proof of $true = $false into a proof of -- the original existentially-quantified formula.-decodeGoal :: Function f => ProvedGoal f -> ProvedGoal f-decodeGoal pg =- case maybeDecodeGoal pg of+decodeGoal :: Function f => Config f -> ProvedGoal f -> ProvedGoal f+decodeGoal config pg =+ case maybeDecodeGoal config pg of Nothing -> pg Just (name, witness, goal, deriv) -> checkProvedGoal $@@ -908,8 +954,9 @@ pg_witness_hint = witness } maybeDecodeGoal :: forall f. Function f =>- ProvedGoal f -> Maybe (String, Subst f, Equation f, Derivation f)-maybeDecodeGoal ProvedGoal{..}+ Config f -> ProvedGoal f -> Maybe (String, Subst f, Equation f, Derivation f)+maybeDecodeGoal Config{..} ProvedGoal{..}+ | not cfg_eliminate_existentials_coding = Nothing -- N.B. presentWithGoals takes care of expanding any lemma which mentions -- $equals, and flattening the proof. | isFalseTerm u = extract (steps deriv)
Twee/Rule.hs view
@@ -84,7 +84,7 @@ -- -- A rule with orientation @'WeaklyOriented' k ts@ can be used unless -- all terms in @ts@ are equal to @k@.- | WeaklyOriented {-# UNPACK #-} !(Fun f) [Term f]+ | WeaklyOriented {-# UNPACK #-} !(Sym f) [Term f] -- | A permutative rule. -- -- A rule with orientation @'Permutative' ts@ can be used if@@ -124,7 +124,7 @@ subst_ sub (Permutative ts) = Permutative (subst_ sub ts) subst_ _ Unoriented = Unoriented -instance (Labelled f, PrettyTerm f) => Pretty (Rule f) where+instance (Intern f, PrettyTerm f) => Pretty (Rule f) where pPrint (Rule or _ l r) = pPrint l <+> text (showOrientation or) <+> pPrint r where@@ -149,7 +149,7 @@ case unify t u of Nothing -> Oriented Just sub- | allSubst (\_ (Cons t Empty) -> isMinimal t) sub ->+ | allSubst (\_ (Cons t Nil) -> isMinimal t) sub -> WeaklyOriented minimal (map (build . var . fst) (substToList sub)) | otherwise -> Unoriented | lessEq t u = error "wrongly-oriented rule"@@ -212,7 +212,7 @@ where u = build (simp (singleton t)) - simp Empty = mempty+ simp Nil = mempty simp (Cons (Var x) t) = var x `mappend` simp t simp (Cons t u) | Just (rule, sub) <- simpleRewrite idx t =@@ -385,7 +385,7 @@ expand t@(Var x) = fromMaybe t (Term.lookup x sub) expand t = t - isMinimal (App f Empty) = f == min+ isMinimal (App f Nil) = f == min isMinimal _ = False reducesWith p (Rule (Permutative ts) _ _ _) sub = aux ts
Twee/Term.hs view
@@ -1,7 +1,7 @@ -- | Terms and substitutions. -- -- Terms in twee are represented as arrays rather than as an algebraic data--- type. This module defines pattern synonyms ('App', 'Var', 'Cons', 'Empty')+-- type. This module defines pattern synonyms ('App', 'Var', 'Cons', 'Nil') -- which means that pattern matching on terms works just as normal. -- The pattern synonyms can not be used to create new terms; for that you -- have to use a builder interface ('Build').@@ -20,26 +20,24 @@ #endif module Twee.Term( -- * Terms- Term, pattern Var, pattern App, isApp, isVar, singleton, len,+ Term, Var(..), pattern Var, pattern App, isApp, isVar, singleton, len, -- * Termlists- TermList, pattern Empty, pattern Cons, pattern ConsSym, hd, tl, rest,+ TermList, pattern Nil, pattern Cons, pattern ConsSym, hd, tl, rest, pattern UnsafeCons, pattern UnsafeConsSym, uhd, utl, urest, empty, unpack, lenList,- -- * Function symbols and variables- Fun, fun, fun_id, fun_value, pattern F, Var(..), Labelled(..), -- * Building terms Build(..), Builder, build, buildList, con, app, var, -- * Access to subterms- children, properSubterms, subtermsList, subterms, reverseSubtermsList, reverseSubterms, occurs, isSubtermOf, isSubtermOfList, at, listAt, atPath,+ children, properSubterms, subtermsList, subterms, reverseSubtermsList, reverseSubterms, occurs, isSubtermOf, isSubtermOfList, at, listAt, atPath, listDrop, -- * Substitutions Substitution(..), subst, Subst(..), -- ** Constructing and querying substitutions- emptySubst, listToSubst, substToList,+ emptySubst, listToSubst, substToList, substToList', lookup, lookupList, extend, extendList, unsafeExtendList, retract,@@ -77,8 +75,7 @@ import qualified Data.IntMap.Strict as IntMap import Control.Arrow((&&&)) import Twee.Utils-import qualified Data.Label as Label-import Data.Typeable+import Data.Intern import GHC.Stack --------------------------------------------------------------------------------@@ -116,21 +113,21 @@ build :: Build a => a -> Term (BuildFun a) build x = case buildList x of- Cons t Empty -> t+ Cons t Nil -> t -- | Build a termlist. {-# INLINE buildList #-} buildList :: Build a => a -> TermList (BuildFun a)-buildList x = buildTermList (builder x)+buildList x = buildTermList 16 (builder x) -- | Build a constant (a function with no arguments). {-# INLINE con #-}-con :: Fun f -> Builder f+con :: Sym f -> Builder f con x = emitApp x mempty -- | Build a function application. {-# INLINE app #-}-app :: Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)+app :: Build a => Sym (BuildFun a) -> a -> Builder (BuildFun a) app f ts = emitApp f (builder ts) -- | Build a variable.@@ -149,7 +146,7 @@ {-# INLINE substToList #-} substToList :: Subst f -> [(Var, Term f)] substToList sub =- [(x, t) | (x, Cons t Empty) <- substToList' sub]+ [(x, t) | (x, Cons t Nil) <- substToList' sub] -- | Fold a function over a substitution. {-# INLINE foldSubst #-}@@ -185,7 +182,7 @@ substList :: s -> TermList (SubstFun s) -> Builder (SubstFun s) substList sub ts = aux ts where- aux Empty = mempty+ aux Nil = mempty aux (Cons (Var x) ts) = evalSubst sub x <> aux ts aux (Cons (App f ts) us) = app f (aux ts) <> aux us @@ -277,7 +274,7 @@ idempotentOn :: Subst f -> TermList f -> Bool idempotentOn !sub = aux where- aux Empty = True+ aux Nil = True aux ConsSym{hd = App{}, rest = t} = aux t aux (Cons (Var x) t) = isNothing (lookupList x sub) && aux t @@ -298,15 +295,15 @@ where (V m, V n) = boundLists (t:ts) vars =- buildTermList $+ buildTermList (n-m+2) $ -- Produces two variables when the term is ground -- (n = minBound, m = maxBound), which is OK. mconcat [emitVar (V x) | x <- [0..n-m+1]] loop !_ !_ !_ !_ | never = undefined- loop sub _ Empty [] = sub- loop sub Empty _ _ = sub- loop sub vs Empty (t:ts) = loop sub vs t ts+ loop sub _ Nil [] = sub+ loop sub Nil _ _ = sub+ loop sub vs Nil (t:ts) = loop sub vs t ts loop sub vs ConsSym{hd = App{}, rest = t} ts = loop sub vs t ts loop sub vs0@(Cons v vs) (Cons (Var x) t) ts = case extend x v sub of@@ -364,7 +361,7 @@ sub <- extend x t sub loop sub pats ts _ -> Nothing- loop sub _ Empty = Just sub+ loop sub _ Nil = Just sub loop _ _ _ = Nothing in loop sub pat t @@ -416,7 +413,7 @@ {-# INLINE substList #-} substList (Triangle sub) ts = aux ts where- aux Empty = mempty+ aux Nil = mempty aux (Cons (Var x) ts) = auxVar x <> aux ts aux (Cons (App f ts) us) = app f (aux ts) <> aux us @@ -480,7 +477,7 @@ sub <- var sub x t loop sub ts us _ -> Nothing- loop sub _ Empty = Just sub+ loop sub _ Nil = Just sub loop _ _ _ = Nothing {-# INLINE var #-}@@ -539,18 +536,18 @@ unpack :: TermList f -> [Term f] unpack t = unfoldr op t where- op Empty = Nothing+ op Nil = Nothing op (Cons t ts) = Just (t, ts) -instance (Labelled f, Show f) => Show (Term f) where+instance (Intern f, Show f) => Show (Term f) where show (Var x) = show x- show (App f Empty) = show f+ show (App f Nil) = show f show (App f ts) = show f ++ "(" ++ intercalate "," (map show (unpack ts)) ++ ")" -instance (Labelled f, Show f) => Show (TermList f) where+instance (Intern f, Show f) => Show (TermList f) where show = show . unpack -instance (Labelled f, Show f) => Show (Subst f) where+instance (Intern f, Show f) => Show (Subst f) where show subst = show [ (i, t)@@ -561,7 +558,7 @@ {-# INLINE lookup #-} lookup :: Var -> Subst f -> Maybe (Term f) lookup x s = do- Cons t Empty <- lookupList x s+ Cons t Nil <- lookupList x s return t -- | Add a new binding to a substitution.@@ -604,7 +601,7 @@ subtermsList :: TermList f -> [Term f] subtermsList t = unfoldr op t where- op Empty = Nothing+ op Nil = Nothing op ConsSym{hd = t, rest = u} = Just (t, u) -- | Find all subterms of a term.@@ -652,20 +649,20 @@ t `isSubtermOf` u = t `isSubtermOfList` singleton u -- | Map a function over the function symbols in a term.-mapFun :: (Fun f -> Fun g) -> Term f -> Builder g+mapFun :: (Sym f -> Sym g) -> Term f -> Builder g mapFun f = mapFunList f . singleton -- | Map a function over the function symbols in a termlist.-mapFunList :: (Fun f -> Fun g) -> TermList f -> Builder g+mapFunList :: (Sym f -> Sym g) -> TermList f -> Builder g mapFunList f ts = aux ts where- aux Empty = mempty+ aux Nil = mempty aux (Cons (Var x) ts) = var x `mappend` aux ts aux (Cons (App ff ts) us) = app (f ff) (aux ts) `mappend` aux us {-# INLINE replace #-} replace :: (Build a, BuildFun a ~ f) => Term f -> a -> TermList f -> Builder f-replace !_ !_ Empty = mempty+replace !_ !_ Nil = 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@@ -680,7 +677,7 @@ replacePosition n !x = aux n where aux !_ !_ | never = undefined- aux _ Empty = mempty+ aux _ Nil = mempty aux 0 (Cons _ t) = builder x `mappend` builder t aux n (Cons (Var x) t) = var x `mappend` aux (n-1) t aux n (Cons t@(App f ts) u)@@ -696,7 +693,7 @@ replacePositionSub sub n !x = aux n where aux !_ !_ | never = undefined- aux _ Empty = mempty+ aux _ Nil = mempty aux n (Cons t u) | n < len t = inside n t `mappend` outside u | otherwise = outside (singleton t) `mappend` aux (n-len t) u@@ -714,7 +711,7 @@ term _ 0 = [] term t n = list 0 (children t) (n-1) - list _ Empty _ = error "bad position"+ list _ Nil _ = error "bad position" list k (Cons t u) n | n < len t = k:term t n | otherwise = list (k+1) u (n-len t)@@ -726,33 +723,11 @@ term k _ [] = k term k t (n:ns) = list (k+1) (children t) n ns - list _ Empty _ _ = error "bad path"+ list _ Nil _ _ = error "bad path" list k (Cons t _) 0 ns = term k t ns list k (Cons t u) n ns = list (k+len t) u (n-1) ns -class Labelled f where- label :: f -> Label.Label f- default label :: (Ord f, Typeable f) => f -> Label.Label f- label = Label.label--instance (Labelled f, Show f) => Show (Fun f) where show = show . fun_value---- | 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))-{-# COMPLETE F #-}---- | Compare the 'fun_value's of two 'Fun's.-(<<) :: (Labelled f, Ord f) => Fun f -> Fun f -> Bool-f << g = fun_value f < fun_value g---- | Construct a 'Fun' from a function symbol.-{-# NOINLINE fun #-}-fun :: Labelled f => f -> Fun f-fun f = Core.F (fromIntegral (Label.labelNum (label f)))---- | The underlying function symbol of a 'Fun'.-{-# INLINE fun_value #-}-fun_value :: Labelled f => Fun f -> f-fun_value x = Label.find (Label.unsafeMkLabel (fromIntegral (fun_id x)))+-- | Compare the values of two 'Sym's.+(<<) :: (Intern f, Ord f) => Sym f -> Sym f -> Bool+f << g = unintern f < unintern g
Twee/Term/Core.hs view
@@ -25,6 +25,7 @@ import GHC.ST hiding (liftST) import Data.Ord import Twee.Profile+import Data.Intern -------------------------------------------------------------------------------- -- Symbols. A symbol is a single function or variable in a flatterm.@@ -72,7 +73,7 @@ -------------------------------------------------------------------------------- -- | @'TermList' f@ is a list of terms whose function symbols have type @f@.--- It is either a 'Cons' or an 'Empty'. You can turn it into a @['Term' f]@+-- It is either a 'Cons' or an 'Nil'. You can turn it into a @['Term' f]@ -- with 'Twee.Term.unpack'. -- A TermList is a slice of an unboxed array of symbols.@@ -90,12 +91,22 @@ | n < 0 || low t + n >= high t = error "term index out of bounds" | otherwise = t `unsafeListAt` n +-- | Get a suffix of a termlist.+listDrop :: TermList f -> Int -> TermList f+t `listDrop` n+ | n < 0 || low t + n > high t = error "term index out of bounds"+ | otherwise = t `unsafeListDrop` n+ -- | Index into a termlist, without bounds checking. unsafeListAt :: TermList f -> Int -> Term f TermList lo hi arr `unsafeListAt` n = case TermList (lo+n) hi arr of UnsafeCons t _ -> t +-- | Get a suffix of a termlist, without bounds checking.+unsafeListDrop :: TermList f -> Int -> TermList f+TermList lo hi arr `unsafeListDrop` n = TermList (lo+n) hi arr+ {-# INLINE lenList #-} -- | The length of (number of symbols in) a termlist. lenList :: TermList f -> Int@@ -120,8 +131,8 @@ compare = comparing termlist -- Pattern synonyms for termlists:--- * Empty :: TermList f--- Empty is the empty termlist.+-- * Nil :: TermList f+-- Nil is the empty termlist. -- * Cons t ts :: Term f -> TermList f -> TermList f -- Cons t ts is the termlist t:ts. -- * ConsSym t ts :: Term f -> TermList f -> TermList f@@ -131,15 +142,15 @@ -- that the termlist is non-empty. -- | Matches the empty termlist.-pattern Empty :: TermList f-pattern Empty <- (patHead -> Nothing)+pattern Nil :: TermList f+pattern Nil <- (patHead -> Nothing) -- | Matches a non-empty termlist, unpacking it into head and tail. pattern Cons :: Term f -> TermList f -> TermList f pattern Cons t ts <- (patHead -> Just (t, _, ts)) -{-# COMPLETE Empty, Cons #-}-{-# COMPLETE Empty, ConsSym #-}+{-# COMPLETE Nil, Cons #-}+{-# COMPLETE Nil, ConsSym #-} -- | Like 'Cons', but does not check that the termlist is non-empty. Use only if -- you are sure the termlist is non-empty.@@ -183,17 +194,7 @@ -- Pattern synonyms for single terms. -- * Var :: Var -> Term f--- * App :: Fun f -> TermList f -> Term f---- | A function symbol. @f@ is the underlying type of function symbols defined--- by the user; @'Fun' f@ is an @f@ together with an automatically-generated unique number.-newtype Fun f =- F {- -- | The unique number of a 'Fun'. Must fit in 32 bits.- fun_id :: Int }- deriving (Eq, Ord)--type role Fun nominal+-- * App :: Sym f -> TermList f -> Term f -- | A variable. newtype Var =@@ -210,16 +211,16 @@ pattern Var x <- (patTerm -> Left x) -- | Matches a function application.-pattern App :: Fun f -> TermList f -> Term f+pattern App :: Sym f -> TermList f -> Term f pattern App f ts <- (patTerm -> Right (f, ts)) {-# COMPLETE Var, App #-} -- A helper function for Var and App. {-# INLINE patTerm #-}-patTerm :: Term f -> Either Var (Fun f, TermList f)+patTerm :: Term f -> Either Var (Sym f, TermList f) patTerm Term{..}- | isFun = Right (F index, ts)+ | isFun = Right (unsafeMkSym index, ts) | otherwise = Left (V index) where Symbol{..} = toSymbol root@@ -277,11 +278,10 @@ -- Build a termlist from a Builder. {-# INLINE buildTermList #-}-buildTermList :: Builder f -> TermList f-buildTermList (Builder m) = stamp "build term" $ runST $ do+buildTermList :: Int -> Builder f -> TermList f+buildTermList initialSize (Builder m) = stamp "build term" $ runST $ do MutableByteArray marr# <-- -- Start with a capacity of 16 symbols (arbitrary choice)- newByteArray (16 * symbolSize)+ newByteArray (max 1 initialSize * symbolSize) (marr, n) <- ST $ \s -> case m s marr# 0# of@@ -326,8 +326,8 @@ -- Emit a function application. {-# INLINE emitApp #-}-emitApp :: Fun f -> Builder f -> Builder f-emitApp (F n) inner = emitSymbolBuilder (Symbol True n 0) inner+emitApp :: Sym f -> Builder f -> Builder f+emitApp f inner = emitSymbolBuilder (Symbol True (symId f) 0) inner -- Emit a variable. {-# INLINE emitVar #-}@@ -394,5 +394,5 @@ occursList (V x) t = symbolOccursList (fromSymbol (Symbol False x 1)) t symbolOccursList :: Int64 -> TermList f -> Bool-symbolOccursList !_ Empty = False+symbolOccursList !_ Nil = False symbolOccursList n ConsSym{hd = t, rest = ts} = root t == n || symbolOccursList n ts
twee-lib.cabal view
@@ -1,5 +1,5 @@ name: twee-lib-version: 2.5+version: 2.6.1 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3@@ -26,7 +26,7 @@ source-repository head type: git- location: git://github.com/nick8325/twee.git+ location: https://github.com/nick8325/twee.git branch: master flag llvm@@ -64,7 +64,7 @@ Twee.Task Twee.Utils Twee.Term.Core- Data.Label+ Data.Intern other-modules: Data.BatchedQueue Data.ChurchList@@ -88,8 +88,9 @@ cereal, QuickCheck hs-source-dirs: .- ghc-options: -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports+ ghc-options: -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports -fno-warn-x-partial default-language: Haskell2010+ default-extensions: TypeOperators if flag(llvm) cpp-options: -DUSE_LLVM