Suggestions for User Manual

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 `<symbol>` to denote an SMT-LIB 3.0 symbol, `<term>` to denote an SMT-LIB term and `<type>` to denote a term whose type is `Type`. The syntactic category `<typed-param>` is defined, BNF-style, as `(<symbol> <type> <attr>*)`. It binds `<symbol>` as a fresh parameter of the given type and attributes (if provided).
 
@@ -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 <symbol> Type)` if `<type>*` is empty, and for
   `(declare-const <symbol> (-> <type>* Type))` otherwise.
+<!--HL In the publically available version of the SMT-LIB 3 proposal it says that this syntax is not allowed even though one could be seen as an abbreviation. Maybe add the same disclaimer here unless this was changed on purpose? -->
 
 <!--CT Do we really need `define-type`? -->
 - `(define-type <symbol> (<type>*) <type>)` defines `<symbol>` to be a lambda term whose type is given by the argument and return types.
@@ -122,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 <symbol> (<typed-param>*) <term> <attr>*)`, defines `<symbol>` 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 <symbol> (<typed-param>*) <term> <attr>*)`, defines `<symbol>` 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 <symbol> (<typed-param>*) <type> <attr>*)` declares a globally scoped variable named `<symbol>` whose type is `<type>`.
 
@@ -140,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.
 
@@ -151,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.
@@ -163,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
@@ -240,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 (<term> <term>)` 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 (<term> <term>)` to denote an equality condition that is required for applications of the term to type check.
 
 ```smt
 (declare-type Int ())
@@ -259,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:
 
@@ -298,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`.
 
@@ -493,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`,
@@ -581,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]`.
+<!-- HL: This is unclear to me (why not \u d6 d4 d3 d2 d1?) and in the SMT-LIB standard it seems to say that "" is the only escape character?-->  
 
 > __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.
 
@@ -649,6 +651,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)`.
+<!-- HL: Maybe move after the description of to_z? It seems weird that this is a core operator when it builds up on a non core operator. However, I see that this is not a conversion operator. Same actually with the next couple of operators. --> 
 - `(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)`
@@ -1224,7 +1227,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 <term><term>`. For example:
+A rule can take an arbitrary number of premises via the syntax `:premise-list <term>*`. For example:
 
 ```smt
 (declare-const and (-> Bool Bool Bool) :right-assoc-nil true)
@@ -1234,7 +1237,7 @@ A rule can take an arbitrary number of premises via the syntax `:premise-list <t
 ```
 
 This syntax specifies that the number of premises that are provided to this rule are arbitrary.
-When applying this rule, the formulas proven to this rule (say `F1 ... Fn`) will be collected and constructed as a single formula via the provided operator (`and`), and subsequently matched against the premise pattern `F`.
+When applying this rule, the formulas previously proven and given to this rule (say `F1 ... Fn`) will be collected and constructed as a single formula via the provided operator (`and`), and subsequently matched against the premise pattern `F`.
 In particular, in this case `F` is bound to `(and F1 ... Fn)`.
 The conclusion of the rule returns `F` itself.