From 6a1c7643d3cf4793c441febd68a86bed5be581c8 Mon Sep 17 00:00:00 2001 From: iTitus Date: Fri, 3 May 2024 14:18:53 +0200 Subject: [PATCH 1/4] Add support for label and expression predicates --- .clj-kondo/lisb/translation/lisb2ir.clj | 4 +++- CHANGELOG | 2 ++ doc/Lisb.md | 21 +++++++++++++++++- project.clj | 2 +- src/lisb/translation/ast2lisb.clj | 25 ++++++++++++++------- src/lisb/translation/ir2ast.clj | 16 ++++++++++++++ src/lisb/translation/lisb2ir.clj | 29 +++++++++++++++++++++++-- src/lisb/translation/util.clj | 2 ++ test/lisb/translation/ast2lisb_test.clj | 6 +++++ test/lisb/translation/circle_test.clj | 6 +++++ test/lisb/translation/ir2ast_test.clj | 6 +++++ 11 files changed, 106 insertions(+), 13 deletions(-) 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 d110ceb..0581966 100644 --- a/doc/Lisb.md +++ b/doc/Lisb.md @@ -243,6 +243,12 @@ | `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 | @@ -301,7 +307,20 @@ | `name == sub` | `(substitution-definition name [] sub)` | `{:tag :substitution-definition :name name :args [] :sub sub}` | | | `name(arg1,arg2,...) == sub` | `(substitution-definition name args sub)` | `{:tag :substitution-definition :name name :args args :sub sub}` | | | `"FILE.def"` | `(file-definition "FILE.def")` | `{:tag :file-definition :file "FILE.def"}` | | - +### Free types +| B | Lisb | IR | Description | +|----------------------------|------------------------|------------------------------------|-------------| +| `FREETYPES ft-def1;ft-def2...` | `(freetypes & ft-defs)` | `{:tag :freetypes :values ft-defs}` | | +#### Free type definitions +| B | Lisb | IR | Description | +|-------------------------------------|---------------------------------------------|---------------------------------------------------------------------------|---------------------------| +| `name = constructor1,...` | `(freetype name [] & constructors)` | `{:tag :freetype :name name :args [] :constructors constructors}` | | +| `name(arg1,...) = constructor1,...` | `(freetype name [arg1 ...] & constructors)` | `{:tag :freetype :name name :args [arg1 ...] :constructors constructors}` | `args` are paramter types | +#### Free type constructors +| B | Lisb | IR | Description | +|-------------|--------------------------|---------------------------------------------|-----------------------------| +| `name` | `(constructor name)` | `{:tag :ft-element :id name}` | | +| `name(arg)` | `(constructor name arg)` | `{:tag :ft-constructor :id name :expr arg}` | `arg` is the contained type | ## Machine | B | Lisb | IR | Description | diff --git a/project.clj b/project.clj index 4913e8e..aaf374d 100644 --- a/project.clj +++ b/project.clj @@ -8,7 +8,7 @@ :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.2"] + :dependencies [[org.clojure/clojure "1.11.3"] [org.clojure/math.combinatorics "0.3.0"] [potemkin "0.4.7"] [com.rpl/specter "1.1.4"] 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..37cf967 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 ::label ::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)))))) From 2c9345375e8bee38c9a464377a46320f0d48f7d9 Mon Sep 17 00:00:00 2001 From: iTitus Date: Fri, 3 May 2024 14:21:13 +0200 Subject: [PATCH 2/4] fix typo --- doc/Lisb.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/Lisb.md b/doc/Lisb.md index 0581966..0c90198 100644 --- a/doc/Lisb.md +++ b/doc/Lisb.md @@ -312,10 +312,10 @@ |----------------------------|------------------------|------------------------------------|-------------| | `FREETYPES ft-def1;ft-def2...` | `(freetypes & ft-defs)` | `{:tag :freetypes :values ft-defs}` | | #### Free type definitions -| B | Lisb | IR | Description | -|-------------------------------------|---------------------------------------------|---------------------------------------------------------------------------|---------------------------| -| `name = constructor1,...` | `(freetype name [] & constructors)` | `{:tag :freetype :name name :args [] :constructors constructors}` | | -| `name(arg1,...) = constructor1,...` | `(freetype name [arg1 ...] & constructors)` | `{:tag :freetype :name name :args [arg1 ...] :constructors constructors}` | `args` are paramter types | +| B | Lisb | IR | Description | +|-------------------------------------|---------------------------------------------|---------------------------------------------------------------------------|--------------------------------| +| `name = constructor1,...` | `(freetype name [] & constructors)` | `{:tag :freetype :name name :args [] :constructors constructors}` | | +| `name(arg1,...) = constructor1,...` | `(freetype name [arg1 ...] & constructors)` | `{:tag :freetype :name name :args [arg1 ...] :constructors constructors}` | `args` are the parameter types | #### Free type constructors | B | Lisb | IR | Description | |-------------|--------------------------|---------------------------------------------|-----------------------------| From ac4842eba07b0fefbae3581cee11dd9b65486488 Mon Sep 17 00:00:00 2001 From: iTitus Date: Fri, 3 May 2024 14:22:12 +0200 Subject: [PATCH 3/4] fix typo --- src/lisb/translation/lisb2ir.clj | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lisb/translation/lisb2ir.clj b/src/lisb/translation/lisb2ir.clj index 37cf967..9010996 100644 --- a/src/lisb/translation/lisb2ir.clj +++ b/src/lisb/translation/lisb2ir.clj @@ -1610,7 +1610,7 @@ :pred pred}) (s/fdef bdescription :args (s/cat :description ::description :pred ::pred) - :ret (s/and (s/keys :req-un [::tag ::label ::pred]) + :ret (s/and (s/keys :req-un [::tag ::description ::pred]) #(= :description (:tag %)))) ;;; misc From 08a86de054e52132e853ae2bdc1ce837c7f29e01 Mon Sep 17 00:00:00 2001 From: iTitus Date: Mon, 6 May 2024 18:59:02 +0200 Subject: [PATCH 4/4] fix merge error --- doc/Lisb.md | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) diff --git a/doc/Lisb.md b/doc/Lisb.md index 1f734ee..7e15500 100644 --- a/doc/Lisb.md +++ b/doc/Lisb.md @@ -249,6 +249,7 @@ | `/*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 | @@ -322,20 +323,6 @@ | `name` | `(constructor name)` | `{:tag :ft-element :id name}` | | | `name(arg)` | `(constructor name arg)` | `{:tag :ft-constructor :id name :expr arg}` | `arg` is the contained type | -### Free types -| B | Lisb | IR | Description | -|----------------------------|------------------------|------------------------------------|-------------| -| `FREETYPES ft-def1;ft-def2...` | `(freetypes & ft-defs)` | `{:tag :freetypes :values ft-defs}` | | -#### Free type definitions -| B | Lisb | IR | Description | -|-------------------------------------|---------------------------------------------|---------------------------------------------------------------------------|--------------------------------| -| `name = constructor1,...` | `(freetype name [] & constructors)` | `{:tag :freetype :name name :args [] :constructors constructors}` | | -| `name(arg1,...) = constructor1,...` | `(freetype name [arg1 ...] & constructors)` | `{:tag :freetype :name name :args [arg1 ...] :constructors constructors}` | `args` are the parameter types | -#### Free type constructors -| B | Lisb | IR | Description | -|-------------|--------------------------|---------------------------------------------|-----------------------------| -| `name` | `(constructor name)` | `{:tag :ft-element :id name}` | | -| `name(arg)` | `(constructor name arg)` | `{:tag :ft-constructor :id name :expr arg}` | `arg` is the contained type | ## Machine | B | Lisb | IR | Description |