Merge pull request #152 from nikomatsakis/reusability-tweaks

improve term macros

Author: nikomatsakis

book/src/SUMMARY.md

@@ -4,8 +4,8 @@
 - [`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)
-        - [Implementing `Fold` and `Visit` by hand](./formality_core/impl_fold_visit.md)
-        - [Implementing `Parse` by hand](./formality_core/impl_parse.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)

book/src/formality_core/collections.md

@@ -1 +1,25 @@
 # Collections
+
+When using formality, it's best to use the following collection types:
+
+* for sequences, use the standard `Vec` type
+* `formality_core::Set<T>` -- equivalent to `BTreeSet` but shorter. We use a `BTreeSet` because it has deterministic ordering for all operations.
+* `formality_core::Map<K, V>` -- equivalent to `BTreeMap` but shorter. We use a `BTreeMap` because it has deterministic ordering for all operations.
+
+## Macros
+
+We also define macros:
+
+* `seq![...]` -- equivalent to `vec![]` but permits flattening with `..` notation, as described below
+* `set![...]` -- like `seq!`, but produces a `Set`
+
+In these macros you can "flatten" things that support `IntoIterator`, so `set![..a, ..b]` will effectively perform a set union of `a` and `b`.
+
+## Casting between collections and tuples
+
+It is possible to upcast from variable tuple types to produce collections:
+
+* A `Vec<E1>` can be upcast to a `Vec<E2>` if `E1: Upcast<E2>`.
+* A `Set<E1>` can be upcast to a `Set<E2>` if `E1: Upcast<E2>`.
+* Tuples of elements (e.g., `(E1, E2)` or `(E1, E2, E3)`) can be **upcast** to sets up to a fixed arity.
+* Sets and vectors can be **downcast** to `()` and `(E, C)`, where `()` succeeds only for empty collections, and `(E, C)` extracts the first element `E` and a collection `C` with all remaining elements (note that elements in sets are always ordered, so the first element is well defined there). This is useful when writing judgment rules that operate over sequences and sets.

book/src/formality_core/debug.md

@@ -0,0 +1,14 @@
+# Customizing the debug
+
+By default, the `#[term]` macro will generate a `Debug` impl that is guided by the `#[grammar]` attributes on your type (see the [parsing](./parse.md) section for more details). But sometimes you want to generate custom logic. You can include a `#[customize(debug)]` declaration to allow that. Most of the type, when you do this, you will also want to [customize parsing](./parse.md#customizing-the-parse), as the `RigidTy` does:
+
+```rust
+{{#include ../../../crates/formality-types/src/grammar/ty.rs:RigidTy_decl}}
+```
+
+Now you must simply implement `Debug` in the usual way. Here is the `RigidTy` declaration:
+
+
+```rust
+{{#include ../../../crates/formality-types/src/grammar/ty/debug_impls.rs:RigidTy_impl}}
+```

book/src/formality_core/impl_fold_visit.md

@@ -0,0 +1,74 @@
+# Parsing
+
+Formality's `#[term]` and `#[grammar]` attributes let you specify the grammar that will be used to parse your structs/enums.
+
+For structs, there is a single grammar, specified as part of the term:
+
+```rust
+#[term( /* grammar here */ )]
+struct MyStruct { }
+```
+
+For enums, the grammar is placed in `#[grammar]` attributes on each variant:
+
+```rust
+#[term]
+struct MyEnum {
+    #[grammar( /* grammar here */ )]
+    Foo(...),
+}
+```
+
+### Ambiguity and precedence
+
+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. Ambiguity can be resolved in two ways:
+
+* Explicit precedence: By default, every variant has precedence 0, but you can override this by annotating variants with `#[precedence(N)]` (where `N` is some integer). This will override the precedence for that variant. Variants with higher precedences are preferred.
+* 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`.
+
+Otherwise, the parser will panic and report ambiguity. The parser panics rather than returning an error because ambiguity doesn't mean that there is no way to parse the given text as the nonterminal -- rather that there are multiple ways. Errors mean that the text does not match the grammar for that nonterminal.
+
+### 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 can also accept 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.
+
+### Greediness
+
+Parsing is generally greedy. So `$*x` and `$,x`, for example, consume as many entries as they can. Typically this works best if `x` begins with some symbol that indicates whether it is present.
+
+### Default grammar
+
+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)`.
+
+### Customizing the parse
+
+If you prefer, you can customize the parse by annotating your term with `#[customize(parse)]`. In the Rust case, for example, the parsing of `RigidTy` is customized ([as is the debug impl](./debug.md)):
+
+```rust
+{{#include ../../../crates/formality-types/src/grammar/ty.rs:RigidTy_decl}}
+```
+
+You must then supply an impl of `Parse` yourself. Because `Parse` is a trait alias, you actually want to implement `CoreParse<L>` for your language type `L`. Inside the code you will want to instantiate a `Parser` and then invoke `parse_variant` for every variant, finally invoking `finish`.
+
+In the Rust code, the impl for `RigidTy` looks as follows:
+
+
+```rust
+{{#include ../../../crates/formality-types/src/grammar/ty/parse_impls.rs:RigidTy_impl}}
+```

book/src/formality_core/parse.md

@@ -35,7 +35,8 @@ The `#[term]` macro says that these are terms and we should generate all the boi
 
 The `#[term]` also accepts some internal annotations:
 
-* `#[cast]` can be applied on an enum variant with a single argument. It says that we should generate upcast/downcast impls to allow conversion. In this case, between a `Variable` and an `Expr`. This would generate an impl `Variable: Upcast<Expr>` that lets you convert a variable to an expression, and a downcast impl `Expr: Downcast<Variable>` that lets you try to convert from an expression to a variable. Downcasting is *fallible*, which means that the downcast will only succeed if this is an `Expr::Variable`. If this is a `Expr::Add`, the downcast would return `None`.
+* `#[cast]` can be applied on an enum variant with a single argument. It says that this variant represents an "is-a" relationship and hence we should generate upcast/downcast impls to allow conversion. In this case, a variable is a kind of expression -- i.e,. wrapping a variable up into an expression doesn't carry any semantic meaning -- so we want variables to be upcastable to expressions (and expressions to be downcast to variables). The `#[cast]` attribute will therefore generate an impl `Variable: Upcast<Expr>` that lets you convert a variable to an expression, and a downcast impl `Expr: Downcast<Variable>` that lets you try to convert from an expression to a variable. Downcasting is *fallible*, which means that the downcast will only succeed if this is an `Expr::Variable`. If this is a `Expr::Add`, the downcast would return `None`.
+    * There is a special case version of `#[cast]` called `#[variable]`. It indicates that the variant represents a (type) variable -- we are not using it here because this an expression variable. Variables are rather specially in folding/parsing to allow for substitution, binders, etc.
 * `#[grammar]` tells the parser and pretty printer how to parse this variant. The `$v0` and `$v1` mean "recursively parse the first and second arguments". This will parse a `Box<Expr>`, which of course is implemented to just parse an `Expr`.
 
 If you are annotating a struct, the `#[term]` just accepts the grammar directly, so `#[term($name)] struct Variable`  means "to parse a variable, just parse the name field (a string)".

book/src/formality_core/terms.md

@@ -216,6 +216,16 @@ where
     }
 }
 
+impl<T: Clone, U, E> UpcastFrom<Result<T, E>> for Result<U, E>
+where
+    T: Upcast<U>,
+    E: Clone,
+{
+    fn upcast_from(term: Result<T, E>) -> Self {
+        term.map(|t| t.upcast())
+    }
+}
+
 impl DowncastTo<()> for () {
     fn downcast_to(&self) -> Option<()> {
         Some(())

crates/formality-core/src/cast.rs

@@ -22,11 +22,17 @@ pub trait Language: 'static + Copy + Ord + Hash + Debug + Default {
         + UpcastFrom<CoreExistentialVar<Self>>
         + UpcastFrom<CoreBoundVar<Self>>;
 
-    /// The character (typically `<`) used to open binders.
+    /// The token (typically `<`) used to open binders.
     const BINDING_OPEN: char;
 
-    /// The character (typically `>`) used to open binders.
+    /// The token (typically `>`) used to open binders.
     const BINDING_CLOSE: char;
+
+    /// Keywords to disallow as identifiers everywhere.
+    /// It is possible to do positional keywords too, if you want,
+    /// but it requires custom parsing impls for your types.
+    /// No fun.
+    const KEYWORDS: &'static [&'static str];
 }
 
 /// For consistency with types like `CoreVariable<L>`, we write `CoreKind<L>` instead of `Kind<L>`.

crates/formality-core/src/language.rs

@@ -7,6 +7,7 @@
 
 // Re-export things from dependencies to avoid everybody repeating same set
 // in their Cargo.toml.
+pub use anyhow::anyhow;
 pub use anyhow::bail;
 pub use contracts::requires;
 pub use tracing::debug;
@@ -89,6 +90,7 @@ macro_rules! declare_language {
             type Parameter = $param:ty;
             const BINDING_OPEN = $binding_open:expr;
             const BINDING_CLOSE = $binding_close:expr;
+            const KEYWORDS = [$($kw:expr),* $(,)?];
         }
     ) => {
         $(#[$the_lang_m:meta])*
@@ -104,6 +106,7 @@ macro_rules! declare_language {
                 type Parameter = $param;
                 const BINDING_OPEN: char = $binding_open;
                 const BINDING_CLOSE: char = $binding_close;
+                const KEYWORDS: &'static [&'static str] = &[$($kw),*];
             }
 
             $crate::trait_alias! {
@@ -143,7 +146,7 @@ macro_rules! declare_language {
 
             /// Parses `text` as a term with no bindings in scope.
             #[track_caller]
-            pub fn try_term<T>(text: &str) -> anyhow::Result<T>
+            pub fn try_term<T>(text: &str) -> $crate::Fallible<T>
             where
                 T: Parse,
             {
@@ -155,26 +158,12 @@ macro_rules! declare_language {
             /// References to the given string will be replaced with the given parameter
             /// when parsing types, lifetimes, etc.
             #[track_caller]
-            pub fn term_with<T, B>(bindings: impl IntoIterator<Item = B>, text: &str) -> anyhow::Result<T>
+            pub fn term_with<T, B>(bindings: impl IntoIterator<Item = B>, text: &str) -> $crate::Fallible<T>
             where
                 T: Parse,
                 B: $crate::Upcast<(String, $param)>,
             {
-                let scope = $crate::parse::Scope::new(bindings.into_iter().map(|b| b.upcast()));
-                let (t, remainder) = match T::parse(&scope, text) {
-                    Ok(v) => v,
-                    Err(errors) => {
-                        let mut err = anyhow::anyhow!("failed to parse {text}");
-                        for error in errors {
-                            err = err.context(error.text.to_owned()).context(error.message);
-                        }
-                        return Err(err);
-                    }
-                };
-                if !$crate::parse::skip_whitespace(remainder).is_empty() {
-                    anyhow::bail!("extra tokens after parsing {text:?} to {t:?}: {remainder:?}");
-                }
-                Ok(t)
+                $crate::parse::core_term_with::<FormalityLang, T, B>(bindings, text)
             }
         }
     }
@@ -237,12 +226,13 @@ macro_rules! id {
 
             impl CoreParse<crate::FormalityLang> for $n {
                 fn parse<'t>(
-                    _scope: &parse::Scope<crate::FormalityLang>,
+                    scope: &parse::Scope<crate::FormalityLang>,
                     text: &'t str,
                 ) -> parse::ParseResult<'t, Self> {
-                    let (string, text) = parse::identifier(text)?;
-                    let n = $n::new(&string);
-                    Ok((n, text))
+                    $crate::parse::Parser::single_variant(scope, text, stringify!($n), |p| {
+                        let string = p.identifier()?;
+                        Ok($n::new(&string))
+                    })
                 }
             }