Event-B and general improvements (#21)

* Add support for :sequence in eventb dsl

* make sure that implicit sequential substitutions are not ignored in eventb translation

* fix specter transform not recursing deeper into expression after finding match

* add support for sequences in eventb translation

* undo lambda change in i2eventb2

* update specter paths for IR to support Tuple

* do not return tags when visiting IR

this fixes transforming tags with specter when tag is named the same as a variable/definition

* add support for let-preds/exprs

* fix let-sub translation

* in progress: if in expressions/predicates

* implement tail

* allow multiple args for functions in eventb

* fix bug with previous commit

* reformat i2eventb

* improve specter Tuple nav

* do not quote sets in lisb ir

* implement if in expressions for eventb

still WIP

* revert previous commit  regarding sets and add comment explaining why

* cleanup

* use to-vec for all ::ids fields in lisb2ir

* update rest of b2eventb code

* simplify if-expr translation and fix let replacement being run to late

* add brackets around lambda expressions

* add new identifier for if-expr generated code

* implement eventb prj1/prj2

* add eventb-prj docs

* fix eventb printing by adding parentheses around all exprs

* add more spaces and brackets around exprs in eventb print

* use a different translation for seq(S)

* Wrap injector craetion in delay to not install/start probcli when not required

* update deps

* update deps

* update deps

* update deps

* set main component of eventb model if not already done

---------

Co-authored-by: Philipp Körner <p.koerner@hhu.de>

Author: iTitus

.clj-kondo/lisb/translation/eventb/dsl.clj

@@ -23,7 +23,9 @@
                          'event-extends 'lisb.translation.eventb.dsl/event-extends
                          'status 'lisb.translation.eventb.dsl/event-status
                          'with 'lisb.translation.eventb.dsl/event-with
-                         'finite 'lisb.translation.eventb.dsl/eventb-finite}
+                         'finite 'lisb.translation.eventb.dsl/eventb-finite
+                         'prj1 'lisb.translation.lisb2ir/beventb-prj1
+                         'prj2 'lisb.translation.lisb2ir/beventb-prj2}
                         (first form)
                         (first form))
                    (rest form))

.clj-kondo/lisb/translation/lisb2ir.clj

@@ -155,6 +155,8 @@
            'parallel-product 'lisb.translation.lisb2ir/bparallel-product
            'prj1 'lisb.translation.lisb2ir/bprj1
            'prj2 'lisb.translation.lisb2ir/bprj2
+           'eventb-prj1 'lisb.translation.lisb2ir/beventb-prj1
+           'eventb-prj2 'lisb.translation.lisb2ir/beventb-prj2
            'closure1 'lisb.translation.lisb2ir/bclosure1
            'closure 'lisb.translation.lisb2ir/bclosure
            'iterate 'lisb.translation.lisb2ir/biterate

doc/Lisb.md

@@ -132,6 +132,8 @@
 | <code>((rel1&#124;&#124;rel2)&#124;&#124;...)</code> | `(parallel-product & rels)`         | `{:tag :parallel-product, :rels rels}`           | parallel product <code>{((x,v),(y,w)) &#124; x,y:r1 & v,w:r2} </code>         | 
 | `prj1(set1, set2)`                                   | `(prj1 set1 set2)`                  | `{:tag :prj1, :set1 set1, :set2 set2}`           | projection function (usage prj1(Dom,Ran)(Pair))                  | 
 | `prj2(set1, set2)`                                   | `(prj2 set1 set2)`                  | `{:tag :prj2, :set1 set1, :set2 set2}`           | projection function (usage prj2(Dom,Ran)(Pair))                  | 
+| `prj1(expr)` and `@prj1(expr)`                       | `(eventb-prj1 expr)`                | `{:tag :eventb-prj1, :expr expr}`                | eventb projection function (usage prj1(Pair))                    | 
+| `prj2(expr)` and `@prj2(expr)`                       | `(eventb-prj2 expr)`                | `{:tag :eventb-prj2, :expr expr}`                | eventb projection function (usage prj2(Pair))                    | 
 | `closure1(rel)`                                      | `(closure1 rel)`                    | `{:tag :closure1, :rel rel}`                     | transitive closure                                               |
 | `closure(rel)`                                       | `(closure rel)`                     | `{:tag :closure, :rel rel}`                      | reflexive & transitive closure                                   |
 | `iterate(rel,num)`                                   | `(iterate rel num)`                 | `{:tag :iterate, :rel rel, :num num}`            | iteration of r with n>=0                                         |

project.clj

@@ -8,11 +8,11 @@
   :deploy-repositories [["releases"  {:sign-releases false :url "https://repo.clojars.org/"}]
                         ["snapshots" {:sign-releases false :url "https://repo.clojars.org/"}]]
   :jvm-opts ["-Xss1g"]
-  :dependencies [[org.clojure/clojure "1.11.3"]
+  :dependencies [[org.clojure/clojure "1.12.1"]
                  [org.clojure/math.combinatorics "0.3.0"]
                  [org.clojure/test.check "1.1.1"]
-                 [potemkin "0.4.7"]
+                 [potemkin "0.4.8"]
                  [com.rpl/specter "1.1.4"]
                  [de.hhu.stups/prob-java "4.15.0"]
                  [de.hhu.stups/value-translator "0.2.1"]
-                 ])
+                 ])

src/lisb/examples/crowded_chessboard.clj

@@ -85,7 +85,7 @@
 
 (defn crowded-empty-state-space []
   (let [machine (create-machine)]
-    (.b_load api machine {"KODKOD" "true"
+    (.b_load @api machine {"KODKOD" "true"
                           "TIME_OUT" "50000"})))
 
 (defn crowded-chessboard

src/lisb/prob/animator.clj

@@ -14,14 +14,14 @@
 
 ; XXX load an instance of MainModule.class to ensure Prob 2.0 is properly loaded.
 ; Among other things this sets prob.home to load files from the ProB stdlib.
-(def injector (Guice/createInjector Stage/PRODUCTION [(MainModule.)]))
+(def injector (delay (Guice/createInjector Stage/PRODUCTION [(MainModule.)])))
 
 
-(def api (.getInstance injector Api))
+(def api (delay (.getInstance @injector Api)))
 
 
 (defn state-space! [ast]
-  (.b_load api ast))
+  (.b_load @api ast))
 
 
 (defmulti get-result type)

src/lisb/translation/ast2lisb.clj

@@ -197,6 +197,10 @@
             ADescriptionExpression ADescriptionPredicate ALabelPredicate
             AExtendedExprExpression
             AExtendedPredPredicate
+            AEventBFirstProjectionExpression
+            AEventBSecondProjectionExpression
+            AEventBFirstProjectionV2Expression
+            AEventBSecondProjectionV2Expression
             ;; for some reason unused
             ; TIntegerLiteral
             ; AConcreteVariablesMachineClause
@@ -638,9 +642,10 @@
     (cond
       (= (class f) ASuccessorExpression) (concat-last 'inc params)
       (= (class f) APredecessorExpression) (concat-last 'dec params)
+      (= (class f) AEventBFirstProjectionV2Expression) (concat-last 'eventb-prj1 params)
+      (= (class f) AEventBSecondProjectionV2Expression) (concat-last 'eventb-prj2 params)
       :else (concat-last 'fn-call f params))))
 
-
 ;;; relations
 
 (defmethod ast->lisb ARelationsExpression [node]
@@ -683,6 +688,10 @@
   (list 'prj1 (ast->lisb (.getExp1 node)) (ast->lisb (.getExp2 node))))
 (defmethod ast->lisb ASecondProjectionExpression [node]
   (list 'prj2 (ast->lisb (.getExp1 node)) (ast->lisb (.getExp2 node))))
+(defmethod ast->lisb AEventBFirstProjectionExpression [node]
+  (list 'eventb-prj1 (ast->lisb (.getExpression node))))
+(defmethod ast->lisb AEventBSecondProjectionExpression [node]
+  (list 'eventb-prj2 (ast->lisb (.getExpression node))))
 (defmethod ast->lisb AClosureExpression [node]
   (expression 'closure1 node))
 (defmethod ast->lisb AReflexiveClosureExpression [node]