From ddfe50ac438e43af6b1f3d39d74b741150bbd05f Mon Sep 17 00:00:00 2001 From: Hanna Lachnitt Date: Tue, 24 Sep 2024 14:16:40 -0700 Subject: [PATCH 01/10] Fixed typo about hidden types (hopefully as intended) --- user_manual.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/user_manual.md b/user_manual.md index 5c96f9ac..41854f3c 100644 --- a/user_manual.md +++ b/user_manual.md @@ -94,7 +94,7 @@ For this purpose, the Eunoia language has the following builtin constants: - `Bool`, denoting the Boolean type, - `true` and `false`, denoting the two values of type `Bool`. -> __Note:__ The core logic of the Ethos also uses several builtin types (e.g. `Proof` and `Quote`) which define the semantics of proof rules. These types are intentionally to exposed to the Eunoia user. Details on then can be found throughout this document. More details on the core logic of the Ethos will be available in a forthcoming publication. +> __Note:__ The core logic of the Ethos also uses several builtin types (e.g. `Proof` and `Quote`) which define the semantics of proof rules. These types are intentionally not exposed to the Eunoia user. Details on then can be found throughout this document. More details on the core logic of the Ethos will be available in a forthcoming publication. In the following, we informally use the syntactic categories `` to denote an SMT-LIB 3.0 symbol, `` to denote an SMT-LIB term and `` to denote a term whose type is `Type`. The syntactic category `` is defined, BNF-style, as `( *)`. It binds `` as a fresh parameter of the given type and attributes (if provided). From c80c2b89ab4c1df5329bd1f32f46fc687c41c514 Mon Sep 17 00:00:00 2001 From: Hanna Lachnitt Date: Tue, 24 Sep 2024 14:47:07 -0700 Subject: [PATCH 02/10] Add question about SMT-LIB 3 proposal discrepancy --- user_manual.md | 1 + 1 file changed, 1 insertion(+) diff --git a/user_manual.md b/user_manual.md index 41854f3c..7e905231 100644 --- a/user_manual.md +++ b/user_manual.md @@ -109,6 +109,7 @@ The following commands are supported for declaring and defining types and terms. This is a derived command as it is a shorthand for `(declare-const Type)` if `*` is empty, and for `(declare-const (-> * Type))` otherwise. + - `(define-type (*) )` defines `` to be a lambda term whose type is given by the argument and return types. From 5ea5dcb2ec8a48f03dad028008e921adfbf0a731 Mon Sep 17 00:00:00 2001 From: Hanna Lachnitt Date: Tue, 24 Sep 2024 14:51:04 -0700 Subject: [PATCH 03/10] Fix potential typo --- user_manual.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/user_manual.md b/user_manual.md index 7e905231..0239e60d 100644 --- a/user_manual.md +++ b/user_manual.md @@ -123,7 +123,7 @@ The following commands are supported for declaring and defining types and terms. The Eunoia language contains further commands for declaring symbols that are not standard SMT-LIB version 3.0: -- `(define (*) *)`, defines `` to be a lambda term whose arguments and body and given by the command, or the body if the argument list is empty. Note that in contrast to the SMT-LIB command `define-fun`, a return type is not provided. The provided attributes may instruct the checker to perform e.g. type checking on the given term see [type checking define](#tcdefine). +- `(define (*) *)`, defines `` to be a lambda term whose arguments and body are given by the command, or the body if the argument list is empty. Note that in contrast to the SMT-LIB command `define-fun`, a return type is not provided. The provided attributes may instruct the checker to perform e.g. type checking on the given term see [type checking define](#tcdefine). - `(declare-parameterized-const (*) *)` declares a globally scoped variable named `` whose type is ``. From 7e3d8005edf5161fb2058f3566c0687415153a9c Mon Sep 17 00:00:00 2001 From: Hanna Lachnitt Date: Tue, 24 Sep 2024 15:08:02 -0700 Subject: [PATCH 04/10] Changes two types in example cannot imagine how this types otherwise --- user_manual.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/user_manual.md b/user_manual.md index 0239e60d..0c7f3d99 100644 --- a/user_manual.md +++ b/user_manual.md @@ -141,7 +141,7 @@ The Eunoia language contains further commands for declaring symbols that are not (declare-const P (-> Int Bool)) ``` -Since Ethos does not assume any builtin definitions of SMT-LIB theories, definitions of standard symbols in SMT-LIB theories(such as `Int`, `+`, etc.) must be provided in Eunoia signatures. In the above example, symbol `c` is declared to be a constant (0-ary) symbol of type `Int`. The symbol `f` is a function taking two integers and returning an integer. +Since Ethos does not assume any builtin definitions of SMT-LIB theories, definitions of standard symbols in SMT-LIB theories (such as `Int`, `+`, etc.) must be provided in Eunoia signatures. In the above example, symbol `c` is declared to be a constant (0-ary) symbol of type `Int`. The symbol `f` is a function taking two integers and returning an integer. Observe that despite the use of different syntax in their declarations, the types of `f` and `g` in the above example are identical as `->` is a right-associative binary type constructor. @@ -152,7 +152,7 @@ Observe that despite the use of different syntax in their declarations, the type ```smt (declare-const not (-> Bool Bool)) (define id ((x Bool)) x) -(define notId ((x Int)) (not (id x))) +(define notId ((x Bool)) (not (id x))) ``` In the example above, `not` is declared to be a unary function over Booleans. Two defined functions are given, the first being an identity function over Booleans, and the second returning the negation of the first. @@ -164,7 +164,7 @@ In other words, the following sequence of commands is equivalent to the one abov ```smt (declare-const not (-> Bool Bool)) (define id ((x Bool)) x) -(define notId ((x Int)) (not x)) +(define notId ((x Bool)) (not x)) ``` #### Example: Polymorphic types From d8df109029933e4cb7154146be4638a417b8726b Mon Sep 17 00:00:00 2001 From: Hanna Lachnitt Date: Tue, 24 Sep 2024 15:46:43 -0700 Subject: [PATCH 05/10] a vs. an typo? --- user_manual.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/user_manual.md b/user_manual.md index 0c7f3d99..4a322ef8 100644 --- a/user_manual.md +++ b/user_manual.md @@ -241,7 +241,7 @@ We call `T` in the above definitions a _parameter_. The free parameters of the r ### The :requires annotation -Arguments to functions can also be annotated with the attribute `:requires ( )` to denote a equality condition that is required for applications of the term to type check. +Arguments to functions can also be annotated with the attribute `:requires ( )` to denote an equality condition that is required for applications of the term to type check. ```smt (declare-type Int ()) From b12daef34b3ae59e114f4f06bd6bd8f5513d1bc5 Mon Sep 17 00:00:00 2001 From: Hanna Lachnitt Date: Tue, 24 Sep 2024 17:40:09 -0700 Subject: [PATCH 06/10] fix typos --- user_manual.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/user_manual.md b/user_manual.md index 4a322ef8..a95ba295 100644 --- a/user_manual.md +++ b/user_manual.md @@ -260,7 +260,7 @@ Furthermore, the function type `(-> (eo::requires t s T) S)` is treated as `(-> ### The :opaque annotation -The attribute `:opaque` can be used to denote that a distinguished argument to a function. +The attribute `:opaque` can be used to denote a distinguished argument to a function. In particular, functions with opaque arguments intuitively can be considered a _family_ of functions indexed by their opaque arguments. An example of this annotation is the following: @@ -299,7 +299,7 @@ For example: (define d () (@purify_fun f a) :type Int) ``` -In this example, `@purify_fun` is declared as a function with one opaque argument, and ordinary integer argument, and returns an integer. +In this example, `@purify_fun` is declared as a function with one opaque argument, an ordinary integer argument, and returns an integer. Intuitively, this definition is introducing a new function, indexed by a function, that is of type `(-> Int Int)`. After parsing, the term `(@purify_fun f a)` is a function application whose operator is `(@purify_fun f)` and has a single child `a`. From 9d9dffa8a004858f45923d4847450935b9171868 Mon Sep 17 00:00:00 2001 From: Hanna Lachnitt Date: Tue, 24 Sep 2024 17:43:17 -0700 Subject: [PATCH 07/10] fix chainable example --- user_manual.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/user_manual.md b/user_manual.md index a95ba295..0f894370 100644 --- a/user_manual.md +++ b/user_manual.md @@ -494,7 +494,7 @@ In contrast, `(or x)` denotes the `or` whose children are `x` and `false`. (define Q ((x Int) (y Int)) (>= x y)) ``` -In the above example, `(>= x y z w)` is syntax sugar for `(and (>= x y) (>= y z))`, +In the above example, `(>= x y z w)` is syntax sugar for `(and (>= x y) (>= y z) (>= z w))`, whereas the term `(>= x y)` is not impacted by the annotation `:chainable` since it has fewer than 3 children. Note that the type for chainable operators is typically `(-> T T S)` for some types `T` and `S`, From 9083f7362a57b5bd3f7b665d96e1c34d909097a1 Mon Sep 17 00:00:00 2001 From: Hanna Lachnitt Date: Wed, 2 Oct 2024 12:32:08 -0700 Subject: [PATCH 08/10] Add more comments --- user_manual.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/user_manual.md b/user_manual.md index 0f894370..40822918 100644 --- a/user_manual.md +++ b/user_manual.md @@ -582,6 +582,7 @@ Also note in contrast to SMT-LIB version 2, negative arithmetic can be provided String values use the standard escape sequences as specified in SMT-LIB version 2.6, namely `""` within a string literal denotes `"`. The only other escape sequences are of the form `\u{dn ...d1}` for `1<=n<=5` and `\u d4 d3 d2 d1` for hexadecimal digits `d1...d5` where `d5` is in the range `[0-2]`. + > __Note:__ Numeral, rational and decimal values are implemented by the arbitrary precision arithmetic library GMP. Binary and hexadecimal values are implemented as layer on top of numeral values that tracks a bit width. String values are implemented as a vector of unsigned integers whose maximum value is specified by SMT-LIB version 2.6, namely the character set corresponds to Unicode values 0 to 196607. @@ -598,6 +599,8 @@ The following gives an example of how to define the class of numeral constants. (declare-consts Int) (define P ((x Int)) (> x 7)) ``` + + In the above example, the `declare-consts` command specifies that numerals (`1`, `2`, `3`, and so on) are constants of type `Int`. The signature can now refer to arbitrary numerals in definitions, e.g. `7` in the definition of `P`. @@ -650,6 +653,7 @@ Note however that the evaluation of these operators is handled by more efficient - Equivalent to `(eo::is_neg (eo::add (eo::neg (eo::hash t1)) (eo::hash t2)))`. Note that this method corresponds to an arbitrary total order on terms. - `(eo::is_z t)` - Equivalent to `(eo::is_eq (eo::to_z t) t)`. + - `(eo::is_q t)` - Equivalent to `(eo::is_eq (eo::to_q t) t)`. Note this returns false for decimal literals. - `(eo::is_bin t)` From bd427a908f8152a08bfb16f7a0a33190e9fd330f Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Thu, 3 Oct 2024 12:32:25 -0700 Subject: [PATCH 09/10] Update user_manual.md --- user_manual.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/user_manual.md b/user_manual.md index 40822918..8d9b0078 100644 --- a/user_manual.md +++ b/user_manual.md @@ -599,8 +599,6 @@ The following gives an example of how to define the class of numeral constants. (declare-consts Int) (define P ((x Int)) (> x 7)) ``` - - In the above example, the `declare-consts` command specifies that numerals (`1`, `2`, `3`, and so on) are constants of type `Int`. The signature can now refer to arbitrary numerals in definitions, e.g. `7` in the definition of `P`. From 5d5ddbb404b2e4d2f45e5c0dd3ac6005f4f14e71 Mon Sep 17 00:00:00 2001 From: Hanna Lachnitt Date: Thu, 3 Oct 2024 17:10:17 -0700 Subject: [PATCH 10/10] Two fixes on premise lists --- user_manual.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/user_manual.md b/user_manual.md index 40822918..b682e73a 100644 --- a/user_manual.md +++ b/user_manual.md @@ -1229,7 +1229,7 @@ It requires that the left hand side of this inequality `x` is a negative numeral ### Premise lists -A rule can take an arbitrary number of premises via the syntax `:premise-list `. For example: +A rule can take an arbitrary number of premises via the syntax `:premise-list *`. For example: ```smt (declare-const and (-> Bool Bool Bool) :right-assoc-nil true) @@ -1239,7 +1239,7 @@ A rule can take an arbitrary number of premises via the syntax `:premise-list