@@ -8,26 +8,27 @@ This module is intended to be imported qualified.
8
8
-}
9
9
module Booster.Pattern.Substitution (
10
10
mkEq ,
11
- destructEq ,
12
11
asEquations ,
13
- partitionPredicates ,
14
12
compose ,
15
13
substituteInPredicate ,
16
14
substituteInTerm ,
17
15
) where
18
16
19
17
import Data.Bifunctor (bimap )
20
18
import Data.Coerce (coerce )
21
- import Data.List (partition )
22
19
import Data.Map.Strict (Map )
23
20
import Data.Map.Strict qualified as Map
24
- import Data.Maybe (fromMaybe , isJust , mapMaybe )
21
+ import Data.Maybe (fromMaybe )
25
22
import Data.Set qualified as Set
26
23
27
24
import Booster.Pattern.Base
28
25
import Booster.Pattern.Bool
29
26
import Booster.Pattern.Util (sortOfTerm )
30
27
28
+ {- | Compose substitutions:
29
+ - apply the left one to the assignments in the right one
30
+ - merge left with the result of above, left takes priority
31
+ -}
31
32
compose :: Substitution -> Substitution -> Substitution
32
33
compose newSubst oldSubst =
33
34
let substitutedOldSubst = Map. map (substituteInTerm newSubst) oldSubst
@@ -40,27 +41,10 @@ mkEq x t = Predicate $ case sortOfTerm t of
40
41
SortBool -> EqualsBool (Var x) t
41
42
otherSort -> EqualsK (KSeq otherSort (Var x)) (KSeq otherSort t)
42
43
43
- {- | Pattern match on an equality predicate and try extracting a variable assignment.
44
- This is a partial inverse of @'mkEq'@
45
- -}
46
- destructEq :: Predicate -> Maybe (Variable , Term )
47
- destructEq = \ case
48
- Predicate (EqualsInt (Var x) t) -> Just (x, t)
49
- Predicate (EqualsBool (Var x) t) -> Just (x, t)
50
- Predicate
51
- (EqualsK (KSeq _lhsSort (Var x)) (KSeq _rhsSort t)) -> Just (x, t)
52
- _ -> Nothing
53
-
54
44
-- | turns a substitution into a list of equations
55
45
asEquations :: Map Variable Term -> [Predicate ]
56
46
asEquations = map (uncurry mkEq) . Map. assocs
57
47
58
- -- | Extract substitution items from a list of generic predicates. Return empty substitution if none are found
59
- partitionPredicates :: [Predicate ] -> (Map Variable Term , [Predicate ])
60
- partitionPredicates ps =
61
- let (substItems, normalPreds) = partition (isJust . destructEq) ps
62
- in (Map. fromList . mapMaybe destructEq $ substItems, normalPreds)
63
-
64
48
substituteInTerm :: Substitution -> Term -> Term
65
49
substituteInTerm substitution = goSubst
66
50
where
0 commit comments