From d3c903e7d4716a44e5e38b79dfe671542f8d5afa Mon Sep 17 00:00:00 2001 From: Georgy Lukyanov Date: Tue, 30 Jul 2024 10:19:47 +0200 Subject: [PATCH] Allow matching functions when rewriting --- booster/library/Booster/Pattern/Match.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index 2e7d3e43ee..8f10d5f60d 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -294,6 +294,7 @@ match1 _ t1@FunctionApplication{} t2@KSet{} match1 Eval (FunctionApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 match1 _ t1@FunctionApplication{} t2@ConsApplication{} = addIndeterminate t1 t2 match1 Eval (FunctionApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2 +match1 Rewrite (FunctionApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Rewrite symbol1 sorts1 args1 symbol2 sorts2 args2 match1 _ t1@FunctionApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2 match1 Rewrite t1@FunctionApplication{} (Var t2) = failWith $ SubjectVariableMatch t1 t2 match1 _ t1@FunctionApplication{} t2@Var{} = addIndeterminate t1 t2