remove \left-assoc and \right-assoc of \and and \or (#337)

Blocked on runtimeverification/k#3679

This completes the changes to the booster with respect to multi-ary \and
and \or. Once the \left-assoc and \right-assoc syntax are no longer
being emitted by the frontend, we can remove them from the backends.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>

cabal.project

@@ -17,7 +17,7 @@ source-repository-package
 source-repository-package
     type: git
     location: https://github.com/runtimeverification/haskell-backend.git
-    tag: 3e1dd2a92e8a1f537260fe347f2d93462235d229
-    --sha256: sha256-6Jfoa9vocBdhqrNLdX7aC2a5guixAj8CQUH9clw26Sg=
+    tag: c209383c259aee0ca8b0859a4160d5c5757721b6
+    --sha256: sha256-GOf7T8VeC3sdpxNf5QyjzDWHAYeIZfbyCLd1aJVvfTI=
     subdir: kore kore-rpc-types
 

deps/haskell-backend_release

@@ -1 +1 @@
-3e1dd2a92e8a1f537260fe347f2d93462235d229
+c209383c259aee0ca8b0859a4160d5c5757721b6

deps/k_release

@@ -1 +1 @@
-6.0.125
+6.0.146

flake.nix

@@ -2,7 +2,7 @@
   description = "hs-backend-booster";
 
   inputs = {
-    haskell-backend.url = "github:runtimeverification/haskell-backend/3e1dd2a92e8a1f537260fe347f2d93462235d229";
+    haskell-backend.url = "github:runtimeverification/haskell-backend/c209383c259aee0ca8b0859a4160d5c5757721b6";
     haskell-nix.follows = "haskell-backend/haskell-nix";
     nixpkgs.follows = "haskell-backend/haskell-nix/nixpkgs-unstable";
     flake-compat = {

library/Booster/Syntax/ParsedKore/Parser.y

@@ -206,24 +206,8 @@ StringLiteral :: { Text }
 ApplicationPattern :: { KorePattern }
 		    : leftAssoc '{' '}' '(' ident SortsBrace NePatterns ')'
                       { mkAssoc True $5 $6 $7 }
-		    | leftAssoc '{' '}' '(' and SortsBrace NePatterns ')'
-                      { mkAssoc True $5 $6 $7 }
-		    | leftAssoc '{' '}' '(' or SortsBrace NePatterns ')'
-                      { mkAssoc True $5 $6 $7 }
-		    | leftAssoc '{' '}' '(' implies SortsBrace NePatterns ')'
-                      { mkAssoc True $5 $6 $7 }
-		    | leftAssoc '{' '}' '(' iff SortsBrace NePatterns ')'
-                      { mkAssoc True $5 $6 $7 }
                     | rightAssoc '{' '}' '(' ident SortsBrace NePatterns ')'
                       { mkAssoc False $5 $6 $7 }
-                    | rightAssoc '{' '}' '(' and SortsBrace NePatterns ')'
-                      { mkAssoc False $5 $6 $7 }
-                    | rightAssoc '{' '}' '(' or SortsBrace NePatterns ')'
-                      { mkAssoc False $5 $6 $7 }
-                    | rightAssoc '{' '}' '(' implies SortsBrace NePatterns ')'
-                      { mkAssoc False $5 $6 $7 }
-                    | rightAssoc '{' '}' '(' iff SortsBrace NePatterns ')'
-                      { mkAssoc False $5 $6 $7 }
                     | top '{' Sort '}' '(' ')'
                       { KJTop {sort = $3} }
                     | bottom '{' Sort '}' '(' ')'
@@ -419,11 +403,6 @@ the result. Namely, \\and, \\or, \\implies, and \\iff. Designed to be passed to
 foldl1' or foldr1.
 -}
 mkApply :: Token -> [Sort] -> KorePattern -> KorePattern -> KorePattern
-mkApply tok [sort] first second
-    | Token _ TokenAnd <- tok = KJAnd sort [first, second]
-    | Token _ TokenOr <- tok = KJOr sort [first, second]
-    | Token _ TokenImplies <- tok = KJImplies sort first second
-    | Token _ TokenIff <- tok = KJIff sort first second
 mkApply tok sorts@[_, _] first second
     | Token _ (TokenIdent _) <- tok = KJApp (mkId tok) sorts [first, second]
 mkApply other _ _ _ = error $ "mkApply: unsupported token " <> show other

stack.yaml

@@ -11,7 +11,7 @@ extra-deps:
   - typerep-map-0.5.0.0
   - monad-validate-1.2.0.1
   - git: https://github.com/runtimeverification/haskell-backend.git
-    commit: 3e1dd2a92e8a1f537260fe347f2d93462235d229
+    commit: c209383c259aee0ca8b0859a4160d5c5757721b6
     subdirs:
       - kore
       - kore-rpc-types

stack.yaml.lock

@@ -40,20 +40,20 @@ packages:
   original:
     hackage: monad-validate-1.2.0.1
 - completed:
-    commit: 3e1dd2a92e8a1f537260fe347f2d93462235d229
+    commit: c209383c259aee0ca8b0859a4160d5c5757721b6
     git: https://github.com/runtimeverification/haskell-backend.git
     name: kore
     pantry-tree:
-      sha256: 6c277d8786183e157d20488aef9f76fe5b7a4cdb6da5b4b9965a1d15a2e1b1cb
+      sha256: a6d0a2d6a079a06a1988249ced87ce7ddd58ab6bf151e3a8861f18b263f66f32
       size: 44685
     subdir: kore
     version: 0.60.0.0
   original:
-    commit: 3e1dd2a92e8a1f537260fe347f2d93462235d229
+    commit: c209383c259aee0ca8b0859a4160d5c5757721b6
     git: https://github.com/runtimeverification/haskell-backend.git
     subdir: kore
 - completed:
-    commit: 3e1dd2a92e8a1f537260fe347f2d93462235d229
+    commit: c209383c259aee0ca8b0859a4160d5c5757721b6
     git: https://github.com/runtimeverification/haskell-backend.git
     name: kore-rpc-types
     pantry-tree:
@@ -62,7 +62,7 @@ packages:
     subdir: kore-rpc-types
     version: 0.60.0.0
   original:
-    commit: 3e1dd2a92e8a1f537260fe347f2d93462235d229
+    commit: c209383c259aee0ca8b0859a4160d5c5757721b6
     git: https://github.com/runtimeverification/haskell-backend.git
     subdir: kore-rpc-types
 snapshots:

test/rpc-integration/resources/diamond.kore

@@ -318,18 +318,18 @@ module TEST
   axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(K0:SortSet{}))) [functional{}()] // functional
   axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(K0:SortMap{}, K1:SortMap{}))) [functional{}()] // functional
   axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lbl'Tild'Int'Unds'{}(K0:SortInt{}))) [functional{}()] // functional
-  axiom{} \right-assoc{}(\or{SortKItem{}} (\exists{SortKItem{}} (Val:SortIntCellOpt{}, inj{SortIntCellOpt{}, SortKItem{}} (Val:SortIntCellOpt{})), \exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortKItem{}} (Val:SortIntCell{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \exists{SortKItem{}} (Val:SortState{}, inj{SortState{}, SortKItem{}} (Val:SortState{})), \bottom{SortKItem{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortIntCellOpt{}} (LblnoIntCell{}(), \exists{SortIntCellOpt{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortIntCellOpt{}} (Val:SortIntCell{})), \bottom{SortIntCellOpt{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortKConfigVar{}} (\top{SortKConfigVar{}}(), \bottom{SortKConfigVar{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv)
-  axiom{} \right-assoc{}(\or{SortGeneratedCounterCell{}} (\exists{SortGeneratedCounterCell{}} (X0:SortInt{}, Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{})), \bottom{SortGeneratedCounterCell{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortBool{}} (\top{SortBool{}}(), \bottom{SortBool{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv)
-  axiom{} \right-assoc{}(\or{SortIntCell{}} (\exists{SortIntCell{}} (X0:SortInt{}, Lbl'-LT-'int'-GT-'{}(X0:SortInt{})), \bottom{SortIntCell{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortKCell{}} (\exists{SortKCell{}} (X0:SortK{}, Lbl'-LT-'k'-GT-'{}(X0:SortK{})), \bottom{SortKCell{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortKCellOpt{}} (LblnoKCell{}(), \exists{SortKCellOpt{}} (Val:SortKCell{}, inj{SortKCell{}, SortKCellOpt{}} (Val:SortKCell{})), \bottom{SortKCellOpt{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortInt{}} (\top{SortInt{}}(), \bottom{SortInt{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv)
-  axiom{} \right-assoc{}(\or{SortGeneratedTopCell{}} (\exists{SortGeneratedTopCell{}} (X0:SortKCell{}, \exists{SortGeneratedTopCell{}} (X1:SortIntCell{}, \exists{SortGeneratedTopCell{}} (X2:SortGeneratedCounterCell{}, Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortIntCell{}, X2:SortGeneratedCounterCell{})))), \bottom{SortGeneratedTopCell{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortIntCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortIntCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}())) [constructor{}()] // no junk
-  axiom{} \right-assoc{}(\or{SortState{}} (\top{SortState{}}(), \bottom{SortState{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv)
+  axiom{} \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortIntCellOpt{}, inj{SortIntCellOpt{}, SortKItem{}} (Val:SortIntCellOpt{})), \exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortKItem{}} (Val:SortIntCell{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \exists{SortKItem{}} (Val:SortState{}, inj{SortState{}, SortKItem{}} (Val:SortState{})), \bottom{SortKItem{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortIntCellOpt{}} (LblnoIntCell{}(), \exists{SortIntCellOpt{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortIntCellOpt{}} (Val:SortIntCell{})), \bottom{SortIntCellOpt{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortKConfigVar{}} (\top{SortKConfigVar{}}(), \bottom{SortKConfigVar{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv)
+  axiom{} \or{SortGeneratedCounterCell{}} (\exists{SortGeneratedCounterCell{}} (X0:SortInt{}, Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{})), \bottom{SortGeneratedCounterCell{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortBool{}} (\top{SortBool{}}(), \bottom{SortBool{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv)
+  axiom{} \or{SortIntCell{}} (\exists{SortIntCell{}} (X0:SortInt{}, Lbl'-LT-'int'-GT-'{}(X0:SortInt{})), \bottom{SortIntCell{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortKCell{}} (\exists{SortKCell{}} (X0:SortK{}, Lbl'-LT-'k'-GT-'{}(X0:SortK{})), \bottom{SortKCell{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortKCellOpt{}} (LblnoKCell{}(), \exists{SortKCellOpt{}} (Val:SortKCell{}, inj{SortKCell{}, SortKCellOpt{}} (Val:SortKCell{})), \bottom{SortKCellOpt{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortInt{}} (\top{SortInt{}}(), \bottom{SortInt{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv)
+  axiom{} \or{SortGeneratedTopCell{}} (\exists{SortGeneratedTopCell{}} (X0:SortKCell{}, \exists{SortGeneratedTopCell{}} (X1:SortIntCell{}, \exists{SortGeneratedTopCell{}} (X2:SortGeneratedCounterCell{}, Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortIntCell{}, X2:SortGeneratedCounterCell{})))), \bottom{SortGeneratedTopCell{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortIntCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortIntCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}()) [constructor{}()] // no junk
+  axiom{} \or{SortState{}} (\top{SortState{}}(), \bottom{SortState{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv)
 
 // rules
 // rule #Ceil{Int,#SortParam}(`_%Int_`(@I1,@I2))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_=/=Int_`(@I2,#token("0","Int")),#token("true","Bool")),#Ceil{Int,#SortParam}(@I1)),#Ceil{Int,#SortParam}(@I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(277564ad2537209fd698729ceaa01973f97125176cf1078f98e2edb7cc190f34), org.kframework.attributes.Location(Location(1369,8,1369,102)), org.kframework.attributes.Source(Source(/nix/store/392hsax8839a1kk18xkx3cs4hvz3411w-k-6.0.87-3997d65c227fde4e67cedfca83a8a2d2436229e6-maven/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]