Add support for label and expression predicates

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

@@ -219,7 +219,9 @@
            '=> 'lisb.translation.lisb2ir/bimplication                                ; sugar
            'not 'lisb.translation.lisb2ir/bnot
            'for-all 'lisb.translation.lisb2ir/bfor-all
-           'exists 'lisb.translation.lisb2ir/bexists}
+           'exists 'lisb.translation.lisb2ir/bexists
+           'label 'lisb.translation.lisb2ir/blabel
+           'description 'lisb.translation.lisb2ir/bdescription}
           form
           form))
    lisb))

CHANGELOG

@@ -5,6 +5,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
 ## [0.0.6] - SNAPSHOT
+  ### Added
+  - Added support for label and expression predicates
 
 ## [0.0.5]
   ### Added

doc/Lisb.md

@@ -243,6 +243,13 @@
 | `CASE expr OF EITHER cond1 THEN sub1 OR cond2 THEN sub2 ... END END`               | `(case expr & cases)`                         |                                                         |                                        |
 | `CASE expr OF EITHER cond1 THEN sub1 OR cond2 THEN sub2 ... ELSE sub-else END END` | `(case expr & case)`                          |                                                         |                                        |
 
+## Pragmas
+| B                     | Lisb                      | IR                                                 | Description                                                       |
+|-----------------------|---------------------------|----------------------------------------------------|-------------------------------------------------------------------|
+| `/*label LBL */ pred` | `(label LBL pred)`        | `{:tag :label :label LBL :pred pred}`              | labelled predicate                                                |
+| `pred /*desc DESC */` | `(description DESC pred)` | `{:tag :description :description DESC :pred pred}` | predicate with description (can use special descriptions as well) |
+
+
 ## Machine clauses
 ### Machine inclusion
 | B                                | Lisb                              | IR                                            | Description                          |

src/lisb/translation/ast2lisb.clj

@@ -47,6 +47,8 @@
             AIntSetExpression
             ANat1SetExpression
             TIdentifierLiteral
+            TPragmaIdOrString
+            TPragmaFreeText
             AConjunctPredicate
             ADisjunctPredicate
             ANegationPredicate
@@ -541,7 +543,7 @@
 ;;; strings
 
 (defmethod ast->lisb AStringExpression [node]
-  (.getText (.getContent node)))
+  (ast->lisb (.getContent node)))
 
 (defmethod ast->lisb AStringSetExpression [_]
   'string-set)
@@ -859,7 +861,6 @@
 (defmethod ast->lisb AExistsPredicate [node]
   (lisbify 'exists (.getIdentifiers node) (.getPredicate node)))
 
-
 ;;; identifier
 
 (defmethod ast->lisb AIdentifierExpression [node]
@@ -869,16 +870,24 @@
   (keyword (.getText node)))
 
 ;;; Label and Descriptions
-;;TODO: implement real behavior
 
-(defmethod ast->lisb ADescriptionExpression [node]
-  (ast->lisb (.getExpression node)))
+(defmethod ast->lisb TPragmaIdOrString [node]
+  (str (.getText node)))
 
-(defmethod ast->lisb ADescriptionPredicate [node]
-  (ast->lisb (.getPredicate node)))
+(defmethod ast->lisb TPragmaFreeText [node]
+  (str (.getText node)))
 
 (defmethod ast->lisb ALabelPredicate [node]
-  (ast->lisb (.getPredicate node)))
+  (lisbify 'label (.getName node) (.getPredicate node)))
+
+(defmethod ast->lisb ADescriptionPredicate [node]
+  (lisbify 'description (.getContent node) (.getPredicate node)))
+
+; this is used for identifiers
+; there are also ADecription[Event|Operation|Set]
+(defmethod ast->lisb ADescriptionExpression [node]
+    (ast->lisb (.getExpression node)))
+
 
 ;;; Event-B specific
 

src/lisb/translation/ir2ast.clj

@@ -100,6 +100,8 @@
                                                AImplicationPredicate
                                                AForallPredicate
                                                AExistsPredicate
+                                               ALabelPredicate
+                                               ADescriptionPredicate
                                                AIntervalExpression
                                                ASequenceExtensionExpression
                                                AEmptySequenceExpression
@@ -135,6 +137,8 @@
                                                AStringExpression
                                                AStringSetExpression
                                                TStringLiteral 
+                                               TPragmaIdOrString
+                                               TPragmaFreeText
                                                ALetExpressionExpression
                                                ALetPredicatePredicate
                                                AConstantsMachineClause
@@ -316,6 +320,9 @@
 (s/def ::name keyword?)
 (s/def ::abstract-machine-name keyword?)
 (s/def ::op keyword?)
+(s/def ::file string?)
+(s/def ::label string?)
+(s/def ::description string?)
 
 (s/def ::machine-clause (s/and (s/keys :req-un [::tag])
                                #(contains? machine-clause-tags (:tag %))))
@@ -1170,6 +1177,15 @@
   (s/assert (s/keys :req-un [::ids ::pred]) ir-node)
   (AExistsPredicate. (ir-node-ids->ast ir-node) (ir-node-pred->ast ir-node)))
 
+;;; pragmas
+
+(defmethod ir-node->ast-node :label [ir-node]
+  (s/assert (s/keys :req-un [::label ::pred]) ir-node)
+  (ALabelPredicate. (TPragmaIdOrString. (:label ir-node)) (ir-node-pred->ast ir-node)))
+
+(defmethod ir-node->ast-node :description [ir-node]
+  (s/assert (s/keys :req-un [::description ::pred]) ir-node)
+  (ADescriptionPredicate. (TPragmaFreeText. (:description ir-node)) (ir-node-pred->ast ir-node)))
 
 ;;; misc
 

src/lisb/translation/lisb2ir.clj

@@ -64,7 +64,8 @@
                  :member :subset :strict-subset
                  ; number predicates
                  :greater :less :greater-equals :less-equals
-                 })
+                 ; pragmas
+                 :label :description})
 
 (declare b=)
 (declare band)
@@ -1592,6 +1593,26 @@
         :ret (s/and (s/keys :req-un [::tag] :req [::ids ::pred])
                     #(= :exists (:tag %))))
 
+;;; pragmas
+
+(defn blabel [label pred]
+  {:tag :label
+   :label label
+   :pred pred})
+(s/fdef blabel
+  :args (s/cat :label ::label :pred ::pred)
+  :ret (s/and (s/keys :req-un [::tag ::label ::pred])
+              #(= :label (:tag %))))
+
+(defn bdescription [description pred]
+  {:tag :description
+   :description description
+   :pred pred})
+(s/fdef bdescription
+  :args (s/cat :description ::description :pred ::pred)
+  :ret (s/and (s/keys :req-un [::tag ::description ::pred])
+              #(= :description (:tag %))))
+
 ;;; misc
 
 
@@ -1914,7 +1935,11 @@
            ~'=> bimplication                                ; sugar
            ~'not bnot
            ~'for-all bfor-all
-           ~'exists bexists]
+           ~'exists bexists
+
+           ;;; pragmas
+           ~'label blabel
+           ~'description bdescription]
        ~pre-processed-lisb
        )))
 

src/lisb/translation/util.clj

@@ -56,6 +56,8 @@
               b= bnot= bdistinct?
               ;;; logical predicates
               band bor bimplication bequivalence bnot bfor-all bexists
+              ;;; pragmas
+              blabel bdescription
               ;;; misc
               bset-enum bmap-set defpred pred almost-flatten wrap bempty-machine])
 

test/lisb/translation/ast2lisb_test.clj

@@ -365,3 +365,9 @@
     (testing "translation to vector"
       (is (vector? (second (b-predicate->lisb "!(x).(x:NAT => 0<x)"))))
       (is (vector? (second (b-predicate->lisb "#(x).(1=1 & 2=2)")))))))
+
+(deftest pragma-predicates-test
+  (testing "pragma-predicates"
+    (are [lisb b-pred] (= lisb (b-predicate->lisb b-pred))
+      '(label "test" (= 1 1)) "/*@label test */ 1=1"
+      '(description "test" (= 1 1)) "1=1 /*@desc test */")))

test/lisb/translation/circle_test.clj

@@ -274,6 +274,12 @@
               (b (for-all [:x] (contains? nat-set :x) (< 0 :x)))
               (b (exists [:x] (and (= 1 1) (= 2 2)))))))
 
+(deftest pragmas-test
+  (testing "pragmas"
+    (are [ir] (= ir (ast->ir (ir->ast ir)))
+      (b (label "test" (= 1 1)))
+      (b (description "test" (= 1 1))))))
+
 (deftest self-nested-operators-test
   (testing "The AST classes offer a copy constructor.
            This can be an issue for unary operators

test/lisb/translation/ir2ast_test.clj

@@ -435,3 +435,9 @@
                 "#(x).(x:NAT & 0=x)" (b (exists [:x] (and (member? :x nat-set) (= 0 :x))))
                 "#(x,y).(x:NAT & y:NAT & 0=x+y)" (b (exists [:x :y] (and (member? :x nat-set) (member? :y nat-set) (= 0 (+ :x :y)))))
                 )))
+
+(deftest pragmas-test
+  (testing "pragmas"
+    (are [b ir] (= b (ast->b (ir->ast ir)))
+      "/*@label test */ 1=1" (b (label "test" (= 1 1)))
+      "1=1 /*@desc test */" (b (description "test" (= 1 1))))))