Merge pull request #160 from nikomatsakis/upcast-arc-and-more

Usability improvements

Cargo.toml

@@ -18,6 +18,7 @@ pretty_assertions = "1.3.0"
 expect-test = "1.4.0"
 formality-macros = { version = "0.1.0", path = "crates/formality-macros" }
 formality-core = { version = "0.1.0", path = "crates/formality-core" }
+tracing = "0.1.40"
 
 
 [dependencies]

book/src/SUMMARY.md

@@ -2,11 +2,12 @@
 
 - [Intro](./intro.md)
 - [`formality_core`: the Formality system](./formality_core.md)
-    - [Defining your lang](./formality_core/lang.md)
-    - [Defining terms with the `term` macro](./formality_core/terms.md)
-        - [Parsing](./formality_core/parse.md)
-        - [Customizing debug](./formality_core/debug.md)
-    - [Variables](./formality_core/variables.md)
-    - [Collections](./formality_core/collections.md)
-    - [Judgment functions and inference rules](./formality_core/judgment_fn.md)
-    - [FAQ and troubleshooting](./formality_core/faq.md)
+  - [Defining your lang](./formality_core/lang.md)
+  - [Defining terms with the `term` macro](./formality_core/terms.md)
+    - [Parsing](./formality_core/parse.md)
+    - [Customizing debug](./formality_core/debug.md)
+  - [Constructors](./formality_core/constructors.md)
+  - [Variables](./formality_core/variables.md)
+  - [Collections](./formality_core/collections.md)
+  - [Judgment functions and inference rules](./formality_core/judgment_fn.md)
+  - [FAQ and troubleshooting](./formality_core/faq.md)

book/src/formality_core/parse.md

@@ -23,8 +23,8 @@ struct MyEnum {
 
 When parsing an enum there will be multiple possibilities. We will attempt to parse them all. If more than one succeeds, the parser will attempt to resolve the ambiguity by looking for the **longest match**. However, we don't just consider the number of characters, we look for a **reduction prefix**:
 
-* When parsing, we track the list of things we had to parse. If there are two variants at the same precedence level, but one of them had to parse strictly more things than the other and in the same way, we'll prefer the longer one. So for example if one variant parsed a `Ty` and the other parsed a `Ty Ty`, we'd take the `Ty Ty`.
-    * When considering whether a reduction is "significant", we take casts into account. See `ActiveVariant::mark_as_cast_variant` for a more detailed explanation and set of examples.
+- When parsing, we track the list of things we had to parse. If there are two variants at the same precedence level, but one of them had to parse strictly more things than the other and in the same way, we'll prefer the longer one. So for example if one variant parsed a `Ty` and the other parsed a `Ty Ty`, we'd take the `Ty Ty`.
+  - When considering whether a reduction is "significant", we take casts into account. See `ActiveVariant::mark_as_cast_variant` for a more detailed explanation and set of examples.
 
 ### Precedence and left-recursive grammars
 
@@ -36,42 +36,41 @@ We support left-recursive grammars like this one from the `parse-torture-tests`:
 
 We also support ambiguous grammars. For example, you can code up arithmetic expressions like this:
 
-
 ```rust
 {{#include ../../../tests/parser-torture-tests/left_associative.rs:Expr}}
 ```
 
 When specifying the `#[precedence]` of a variant, the default is left-associativity, which can be written more explicitly as `#[precedence(L, left)]`. If you prefer, you can specify right-associativity (`#[precedence(L, right)]`) or non-associativity `#[precedence(L, none)]`. This affects how things of the same level are parsed:
 
-* `1 + 1 + 1` when left-associative is `(1 + 1) + 1`
-* `1 + 1 + 1` when right-associative is `1 + (1 + 1)`
-* `1 + 1 + 1` when none-associative is an error.
+- `1 + 1 + 1` when left-associative is `(1 + 1) + 1`
+- `1 + 1 + 1` when right-associative is `1 + (1 + 1)`
+- `1 + 1 + 1` when none-associative is an error.
 
 ### Symbols
 
-A grammar consists of a series of *symbols*. Each symbol matches some text in the input string. Symbols come in two varieties:
-
-* Most things are *terminals* or *tokens*: this means they just match themselves:
-    * For example, the `*` in `#[grammar($v0 * $v1)]` is a terminal, and it means to parse a `*` from the input.
-    * Delimeters are accepted but must be matched, e.g., `( /* tokens */ )` or `[ /* tokens */ ]`.
-* Things beginning with `$` are *nonterminals* -- they parse the contents of a field. The grammar for a field is generally determined from its type.
-    * If fields have names, then `$field` should name the field.
-    * For position fields (e.g., the T and U in `Mul(Expr, Expr)`), use `$v0`, `$v1`, etc.
-    * Exception: `$$` is treated as the terminal `'$'`.
-* Nonterminals have various modes:
-    * `$field` -- just parse the field's type
-    * `$*field` -- the field must be a `Vec<T>` -- parse any number of `T` instances. Something like `[ $*field ]` would parse `[f1 f2 f3]`, assuming `f1`, `f2`, and `f3` are valid values for `field`.
-    * `$,field` -- similar to the above, but uses a comma separated list (with optional trailing comma). So `[ $,field ]` will parse something like `[f1, f2, f3]`.
-    * `$?field` -- will parse `field` and use `Default::default()` value if not present.
-    * `$<field>` -- parse `<E1, E2, E3>`, where `field: Vec<E>` 
-    * `$<?field>` -- parse `<E1, E2, E3>`, where `field: Vec<E>`, but accept empty string as empty vector
-    * `$(field)` -- parse `(E1, E2, E3)`, where `field: Vec<E>` 
-    * `$(?field)` -- parse `(E1, E2, E3)`, where `field: Vec<E>`, but accept empty string as empty vector
-    * `$[field]` -- parse `[E1, E2, E3]`, where `field: Vec<E>` 
-    * `$[?field]` -- parse `[E1, E2, E3]`, where `field: Vec<E>`, but accept empty string as empty vector
-    * `${field}` -- parse `{E1, E2, E3}`, where `field: Vec<E>` 
-    * `${?field}` -- parse `{E1, E2, E3}`, where `field: Vec<E>`, but accept empty string as empty vector
-    * `$:guard <nonterminal>` -- parses `<nonterminal>` but only if the keyword `guard` is present. For example, `$:where $,where_clauses` would parse `where WhereClause1, WhereClause2, WhereClause3` but would also accept nothing (in which case, you would get an empty vector).
+A grammar consists of a series of _symbols_. Each symbol matches some text in the input string. Symbols come in two varieties:
+
+- Most things are _terminals_ or _tokens_: this means they just match themselves:
+  - For example, the `*` in `#[grammar($v0 * $v1)]` is a terminal, and it means to parse a `*` from the input.
+  - Delimeters are accepted but must be matched, e.g., `( /* tokens */ )` or `[ /* tokens */ ]`.
+- Things beginning with `$` are _nonterminals_ -- they parse the contents of a field. The grammar for a field is generally determined from its type.
+  - If fields have names, then `$field` should name the field.
+  - For position fields (e.g., the T and U in `Mul(Expr, Expr)`), use `$v0`, `$v1`, etc.
+  - Exception: `$$` is treated as the terminal `'$'`.
+- Nonterminals have various modes:
+  - `$field` -- just parse the field's type
+  - `$*field` -- the field must be a collection of `T` (e.g., `Vec<T>`, `Set<T>`) -- parse any number of `T` instances. Something like `[ $*field ]` would parse `[f1 f2 f3]`, assuming `f1`, `f2`, and `f3` are valid values for `field`.
+  - `$,field` -- similar to the above, but uses a comma separated list (with optional trailing comma). So `[ $,field ]` will parse something like `[f1, f2, f3]`.
+  - `$?field` -- will parse `field` and use `Default::default()` value if not present.
+  - `$<field>` -- parse `<E1, E2, E3>`, where `field` is a collection of `E`
+  - `$<?field>` -- parse `<E1, E2, E3>`, where `field` is a collection of `E`, but accept empty string as empty vector
+  - `$(field)` -- parse `(E1, E2, E3)`, where `field` is a collection of `E`
+  - `$(?field)` -- parse `(E1, E2, E3)`, where `field` is a collection of `E`, but accept empty string as empty vector
+  - `$[field]` -- parse `[E1, E2, E3]`, where `field` is a collection of `E`
+  - `$[?field]` -- parse `[E1, E2, E3]`, where `field` is a collection of `E`, but accept empty string as empty vector
+  - `${field}` -- parse `{E1, E2, E3}`, where `field` is a collection of `E`
+  - `${?field}` -- parse `{E1, E2, E3}`, where `field` is a collection of `E`, but accept empty string as empty vector
+  - `$:guard <nonterminal>` -- parses `<nonterminal>` but only if the keyword `guard` is present. For example, `$:where $,where_clauses` would parse `where WhereClause1, WhereClause2, WhereClause3` but would also accept nothing (in which case, you would get an empty vector).
 
 ### Greediness
 
@@ -81,8 +80,8 @@ Parsing is generally greedy. So `$*x` and `$,x`, for example, consume as many en
 
 If no grammar is supplied, the default grammar is determined as follows:
 
-* If a `#[cast]` or `#[variable]` annotation is present, then the default grammar is just `$v0`.
-* Otherwise, the default grammar is the name of the type (for structs) or variant (for enums), followed by `()`, with the values for the fields in order. So `Mul(Expr, Expr)` would have a default grammar `mul($v0, $v1)`.
+- If a `#[cast]` or `#[variable]` annotation is present, then the default grammar is just `$v0`.
+- Otherwise, the default grammar is the name of the type (for structs) or variant (for enums), followed by `()`, with the values for the fields in order. So `Mul(Expr, Expr)` would have a default grammar `mul($v0, $v1)`.
 
 ### Customizing the parse
 
@@ -96,7 +95,6 @@ You must then supply an impl of `Parse` yourself. Because `Parse` is a trait ali
 
 In the Rust code, the impl for `RigidTy` looks as follows:
 
-
 ```rust
 {{#include ../../../crates/formality-types/src/grammar/ty/parse_impls.rs:RigidTy_impl}}
-```
+```

crates/formality-check/src/lib.rs

@@ -99,6 +99,7 @@ impl Check<'_> {
         assert!(env.encloses((&assumptions, &goal)));
 
         let cs = formality_prove::prove(self.decls, env, &assumptions, &goal);
+        let cs = cs.into_set()?;
         if cs.iter().any(|c| c.unconditionally_true()) {
             return Ok(());
         }
@@ -145,10 +146,10 @@ impl Check<'_> {
             &existential_goal,
         );
 
-        if cs.is_empty() {
+        if !cs.is_proven() {
             return Ok(());
         }
 
-        bail!("failed to disprove\n    {goal:?}\ngiven\n    {assumptions:?}\ngot\n{cs:#?}")
+        bail!("failed to disprove\n    {goal:?}\ngiven\n    {assumptions:?}\ngot\n{cs:?}")
     }
 }

crates/formality-core/Cargo.toml

@@ -21,6 +21,10 @@ formality-macros = { version = "0.1.0", path = "../formality-macros" }
 anyhow = "1.0.75"
 contracts = "0.6.3"
 final_fn = "0.1.0"
+itertools = "0.12.0"
+either = "1.9.0"
+expect-test = "1.4.1"
+regex = "1.10.2"
 
 [dev-dependencies]
 expect-test = "1.4.1"

crates/formality-core/src/binder.rs

@@ -261,17 +261,24 @@ where
     T: std::fmt::Debug,
 {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        if !self.kinds.is_empty() {
-            write!(f, "{}", L::BINDING_OPEN)?;
-            for (kind, i) in self.kinds.iter().zip(0..) {
-                if i > 0 {
-                    write!(f, ", ")?;
+        if f.alternate() {
+            f.debug_struct("Binder")
+                .field("kinds", &self.kinds)
+                .field("term", &self.term)
+                .finish()
+        } else {
+            if !self.kinds.is_empty() {
+                write!(f, "{}", L::BINDING_OPEN)?;
+                for (kind, i) in self.kinds.iter().zip(0..) {
+                    if i > 0 {
+                        write!(f, ", ")?;
+                    }
+                    write!(f, "{:?}", kind)?;
                 }
-                write!(f, "{:?}", kind)?;
+                write!(f, "{} ", L::BINDING_CLOSE)?;
             }
-            write!(f, "{} ", L::BINDING_CLOSE)?;
+            write!(f, "{:?}", &self.term)?;
+            Ok(())
         }
-        write!(f, "{:?}", &self.term)?;
-        Ok(())
     }
 }