diff --git a/.clj-kondo/lisb/translation/lisb2ir.clj b/.clj-kondo/lisb/translation/lisb2ir.clj index 1d8b9ef..f015b7d 100644 --- a/.clj-kondo/lisb/translation/lisb2ir.clj +++ b/.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)) diff --git a/CHANGELOG b/CHANGELOG index 7a6f64b..16862b1 100644 --- a/CHANGELOG +++ b/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 diff --git a/doc/Lisb.md b/doc/Lisb.md index bd0b077..7e15500 100644 --- a/doc/Lisb.md +++ b/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 | diff --git a/src/lisb/translation/ast2lisb.clj b/src/lisb/translation/ast2lisb.clj index 144ed72..ce6594f 100644 --- a/src/lisb/translation/ast2lisb.clj +++ b/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 diff --git a/src/lisb/translation/ir2ast.clj b/src/lisb/translation/ir2ast.clj index d405d37..d1a9788 100644 --- a/src/lisb/translation/ir2ast.clj +++ b/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 diff --git a/src/lisb/translation/lisb2ir.clj b/src/lisb/translation/lisb2ir.clj index 41218c1..9010996 100644 --- a/src/lisb/translation/lisb2ir.clj +++ b/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 ))) diff --git a/src/lisb/translation/util.clj b/src/lisb/translation/util.clj index ea6e0fc..63f5833 100644 --- a/src/lisb/translation/util.clj +++ b/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]) diff --git a/test/lisb/translation/ast2lisb_test.clj b/test/lisb/translation/ast2lisb_test.clj index 1478b59..8ce47cc 100644 --- a/test/lisb/translation/ast2lisb_test.clj +++ b/test/lisb/translation/ast2lisb_test.clj @@ -365,3 +365,9 @@ (testing "translation to vector" (is (vector? (second (b-predicate->lisb "!(x).(x:NAT => 0lisb "#(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 */"))) diff --git a/test/lisb/translation/circle_test.clj b/test/lisb/translation/circle_test.clj index 37da71a..be9170e 100644 --- a/test/lisb/translation/circle_test.clj +++ b/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 diff --git a/test/lisb/translation/ir2ast_test.clj b/test/lisb/translation/ir2ast_test.clj index 971f756..562db8b 100644 --- a/test/lisb/translation/ir2ast_test.clj +++ b/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))))))