From 7091e0f21a1b6d4729b9735ec3f86e9237a5b461 Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Thu, 17 Oct 2024 19:39:57 +0200 Subject: [PATCH] Add symmetrical cases --- booster/library/Booster/Pattern/Substitution.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/booster/library/Booster/Pattern/Substitution.hs b/booster/library/Booster/Pattern/Substitution.hs index fac9072927..93d0a416c7 100644 --- a/booster/library/Booster/Pattern/Substitution.hs +++ b/booster/library/Booster/Pattern/Substitution.hs @@ -46,9 +46,13 @@ mkEq x t = Predicate $ case sortOfTerm t of destructEq :: Predicate -> Maybe (Variable, Term) destructEq = \case Predicate (EqualsInt (Var x) t) -> Just (x, t) + Predicate (EqualsInt t (Var x)) -> Just (x, t) Predicate (EqualsBool (Var x) t) -> Just (x, t) + Predicate (EqualsBool t (Var x)) -> Just (x, t) Predicate (EqualsK (KSeq _lhsSort (Var x)) (KSeq _rhsSort t)) -> Just (x, t) + Predicate + (EqualsK (KSeq _lhsSort t) (KSeq _rhsSort (Var x))) -> Just (x, t) _ -> Nothing -- | turns a substitution into a list of equations