diff --git a/Cargo.lock b/Cargo.lock index 37a2580d..3651bb3b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -86,9 +86,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.66" +version = "1.0.75" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "216261ddc8289130e551ddcd5ce8a064710c0d064a4d2895c67151c92b5443f6" +checksum = "a4668cab20f66d8d020e1fbc0ebe47217433c1b6c8f2040faf858554e394ace6" [[package]] name = "atty" @@ -476,9 +476,9 @@ dependencies = [ [[package]] name = "expect-test" -version = "1.4.0" +version = "1.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1d4661aca38d826eb7c72fe128e4238220616de4c0cc00db7bfc38e2e1364dd3" +checksum = "30d9eafeadd538e68fb28016364c9732d78e420b9ff8853fa5e4058861e9f8d3" dependencies = [ "dissimilar", "once_cell", @@ -561,8 +561,13 @@ dependencies = [ name = "formality-core" version = "0.1.0" dependencies = [ + "anyhow", + "contracts", "env_logger", + "expect-test", + "formality-macros", "lazy_static", + "stacker", "tracing", "tracing-subscriber", "tracing-tree", @@ -624,7 +629,6 @@ dependencies = [ "expect-test", "extension-trait", "formality-core", - "formality-macros", "lazy_static", "stacker", "tracing", diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index b365054a..2f43c2a2 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -1,6 +1,12 @@ # Summary - [Intro](./intro.md) -- [Formality](./formality.md) - - [Terms](./terms.md) - - [Inference rules](./inference_rules.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) + - [Implementing `Fold` and `Visit` by hand](./formality_core/impl_fold_visit.md) + - [Implementing `Parse` by hand](./formality_core/impl_parse.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) diff --git a/book/src/faq.md b/book/src/faq.md new file mode 100644 index 00000000..e9c7936d --- /dev/null +++ b/book/src/faq.md @@ -0,0 +1 @@ +# FAQ and troubleshooting diff --git a/book/src/formality_core.md b/book/src/formality_core.md new file mode 100644 index 00000000..c394e3fd --- /dev/null +++ b/book/src/formality_core.md @@ -0,0 +1,10 @@ +# `formality_core`: the Formality system + +`a-mir-formality` is build on the formality core system, +defined by the `formality_core` crate. +Formality core is a mildly opnionated series of macros, derives, and types +that let you write high-level Rust code +in a way that resembles standard type theory notation. +Its primary purpose is to be used by a-mir-formality +but it can be used for other projects. + diff --git a/book/src/formality_core/collections.md b/book/src/formality_core/collections.md new file mode 100644 index 00000000..9385853c --- /dev/null +++ b/book/src/formality_core/collections.md @@ -0,0 +1 @@ +# Collections diff --git a/book/src/formality_core/faq.md b/book/src/formality_core/faq.md new file mode 100644 index 00000000..ce7945fa --- /dev/null +++ b/book/src/formality_core/faq.md @@ -0,0 +1,7 @@ +# FAQ and troubleshooting + +## Why am I getting errors about undefined references to `crate::FormalityLang`? + +The various derive macros need to know what language you are working in. +To figure this out, they reference `crate::FormalityLang`, which you must define. +See the [chapter on defining your language](./lang.md) for more details. diff --git a/book/src/formality_core/impl_fold_visit.md b/book/src/formality_core/impl_fold_visit.md new file mode 100644 index 00000000..5fede039 --- /dev/null +++ b/book/src/formality_core/impl_fold_visit.md @@ -0,0 +1,22 @@ +# Implementing `Fold` and `Visit` by hand + +The `#[term]` macro auto-generates impls of `Fold`, `Visit`, and `Parse`. +But sometimes you don't want to use the macro. +Sometimes you want to write your own code. +One common reason is for substitution of a variable. +For example, in the Rust model, +the code that replaces type variables with types from a substitution +is defined by a manual impl of `Fold`. +Because `Fold` and `Visit` are trait aliases, you need to implement the underlying +trait (`CoreFold`) by hand. +Here is the custom impl of fold for `Ty` from `formality_types`: + +```rust +{{#include ../../../crates/formality-types/src/grammar/ty/term_impls.rs:core_fold_ty}} +``` + +That same module contains other examples, such as impls of `CoreVisit`. + +## Derives + +You can also manually derive `Visit` and `Fold` instead of using `#[term]`. \ No newline at end of file diff --git a/book/src/formality_core/impl_parse.md b/book/src/formality_core/impl_parse.md new file mode 100644 index 00000000..f804d53f --- /dev/null +++ b/book/src/formality_core/impl_parse.md @@ -0,0 +1,8 @@ +# Implementing Parse by hand + +The generic `#[term]` macro generates a simple parser, but sometimes you want more flexibility. +Here is the code that implements the parsing of Rust types: + +```rust +{{#include ../../../crates/formality-types/src/grammar/ty/parse_impls.rs:ty_parse_impl}} +``` diff --git a/book/src/formality_core/judgment_fn.md b/book/src/formality_core/judgment_fn.md new file mode 100644 index 00000000..eabbd3a6 --- /dev/null +++ b/book/src/formality_core/judgment_fn.md @@ -0,0 +1,185 @@ +# Judgment functions and inference rules + +The next thing is the `judgement_fn!` macro. This lets you write a *judgment* using *inference rules*. A "judgment" just means some kind of predicate that the computer can judge to hold or not hold. Inference rules are those rules you may have seen in papers and things: + +``` +premise1 +premise2 +premise3 +------------------ +conclusion +``` + +i.e., the conclusion is judged to be true if all the premises are true. + +[`prove_wc`]: https://github.com/rust-lang/a-mir-formality/blob/bca36ecd069d6bdff77bffbb628ae3b2ef4f8ef7/crates/formality-prove/src/prove/prove_wc.rs#L21-L125 + +Judgments in type system papers can look all kinds of ways. For example, a common type system judgment would be the following: + +``` +Γ ⊢ E : T +``` + +This can be read as, in the environment Γ, the expression E has type T. You might have rule like these: + +``` +Γ[X] = ty // lookup variable in the environment +--------------- "variable" +Γ ⊢ X : ty + +Γ ⊢ E1 : T // must have the same type +Γ ⊢ E2 : T +--------------- "add" +Γ ⊢ E1 + E2 : T +``` + +In a-mir-formality, you might write those rules like so: + +```rust +judgment_fn! { + pub fn has_type( + env: Env, + expr: Expr, + ) => Type { + ( + (env.get(&name) => ty) + --------------- + (has_type(env, name: Variable) => ty) + ) + + ( + (has_type(env, left) => ty_left) + (has_type(env, right) => ty_right) + (if ty_left == ty_right) + --------------- + (has_type(env, Expr::Add(left, right)) => ty_left) + ) + } +} +``` + +Unlike mathematical papers, where judgments can look like whatever you want, judgments in a-mir-formality always have a fixed form that distinguish inputs and outputs: + +``` +judgment_name(input1, input2, input3) => output +``` + +In this case, `has_type(env, expr) => ty` is the equivalent of `Γ ⊢ E : T`. Note that, by convention, we tend to use more English style names, so `env` and not `Γ`, and `expr` and not `E`. Of course nothing is stop you from using single letters, it's just a bit harder to read. + +When we write the `judgement_fn`, it is going to desugar into an actual Rust function that looks like this: + +```rust +pub fn has_type(arg0: impl Upcast, arg1: impl Upcast) -> Set { + let arg0: Env = arg0.upcast(); + let arg1: Expr = arg1.upcast(); + + ... +} +``` + +Some things to note. First, the function arguments (`arg0`, `arg1`) implicitly accept anything that "upcasts" (infallibly converts) into the desired types. `Upcast` is a trait defined within a-mir-formality and implemented by the `#[term]` macro automatically. + +Second, the function always returns a `Set`. This is because there can be more rules, and they may match in any ways. The generated code is going to exhaustively search to find all the ways that the rules could match. At a high-level the code looks like this (at least if we ignore the possibility of cycles; we'll come back to that later): + +```rust +pub fn has_type(arg0: impl Upcast, arg1: impl Upcast) -> Set { + let arg0: Env = arg0.upcast(); + let arg1: Expr = arg1.upcast(); + + let mut results = set![]; // we define this macro + + if /* inference rule 1 matches */ { + results.push(/* result from inference rule 1 */); + } + + if /* inference rule 2 matches */ { + results.push(/* result from inference rule 1 */); + } + + // ... + + if /* inference rule N matches */ { + results.push(/* result from inference rule N */); + } + + results +} +``` + +So how do we test if a particular inference rule matches? Let's look more closely at the code we would generate for this inference rule: + +```rust +( + (env.get(name) => ty) + --------------- + (has_type(env, name: Variable) => ty) +) +``` + +The first part of the final line, `has_type(env, name: Variable)`, defines patterns that are matched against the arguments. These are matched against the arguments (`arg0`, `arg1`) from the judgment. Patterns can either be trivial bindings (like `env`) or more complex (like `name: Variable` or `Expr::Add(left, right)`). In the latter case, they don't have to match the type of the argument precisely. Instead, we use the `Downcast` trait combined with pattern matching. So this inference rule would compile to something like... + +```rust +// Simple variable bindings just clone... +let env = arg0.clone(); + +// More complex patterns are downcasted and testing... +if let Some(name) = arg1.downcast::() { + ... // rule successfully matched! See below. +} +``` + +Once we've matched the arguments, we start trying to execute the inference rule conditions. We have one, `env.get(&name) => ty`. What does that do? A condition written like `$expr => $pat` basically becomes a for loop, so you get... + +```rust +let env = arg0.clone(); +if let Some(name) = arg1.downcast::() { + for ty in env.get(&name) { + ... // other conditions, if any + } +} +``` + +Once we run out of conditions, we can generate the final result, which comes from the `=> $expr` in the conclusion of the rule. In this case, something like this: + +```rust +let env = arg0.clone(); +if let Some(name) = arg1.downcast::() { + for ty in env.get(&name) { + result.push(ty); + } +} +``` + +Thus each inference rule is converted into a little block of code that may push results onto the final set. + +The second inference rule (for addition) looks like... + +```rust +// given this... +// ( +// (has_type(env, left) => ty_left) +// (has_type(env, right) => ty_right) +// (if ty_left == ty_right) +// --------------- +// (has_type(env, Expr::Add(left, right)) => ty_left) +// ) +// we generate this... +let env = arg0.clone(); +if let Some(Expr::Add(left, right)) = arg1.downcast() { + for ty_left in has_type(env, left) { + for ty_right in has_type(env, right) { + if ty_left == ty_right { + result.push(ty_left); + } + } + } +} +``` + +If you want to see a real judgement, take a look at the one for [proving where clauses][`prove_wc`]. + +[`prove_wc`]: https://github.com/rust-lang/a-mir-formality/blob/bca36ecd069d6bdff77bffbb628ae3b2ef4f8ef7/crates/formality-prove/src/prove/prove_wc.rs#L21-L125 + +### Handling cycles + +Judgment functions must be **inductive**, which means that cycles are considered failures. We have a tabling implementation, which means we detect cycles and try to handle them intelligently. Basically we track a stack and, if a cycle is detected, we return an empty set of results. But we remember that the cycle happened. Then, once we are done, we'll have computed some intermediate set of results `R[0]`, and we execute again. This time, when we get the cycle, we return `R[0]` instead of an empty set. This will compute some new set of results, `R[1]`. So then we try again. We keep doing this until the new set of results `R[i]` is equal to the previous set of results `R[i-1]`. At that point, we have reached a fixed point, so we stop. Of course, it could be that you get an infinitely growing set of results, and execution never terminates. This means your rules are broken. Don't do that. diff --git a/book/src/formality_core/lang.md b/book/src/formality_core/lang.md new file mode 100644 index 00000000..28b8d07e --- /dev/null +++ b/book/src/formality_core/lang.md @@ -0,0 +1,41 @@ +# Defining your language + +The very first thing you do to define your own language is to use the `formality_core::declare_language!` macro. +You use it like so: + +```rust +{{#include ../../../crates/formality-types/src/lib.rs:declare_rust_language}} +``` + +The `declare_language` macro will create a module with the name you specify (here, `rust`). +You have to tell it a few things: + +* The `NAME` of your language, a string for debugging. +* An enum defining the *kinds* of variables in your language; see the [variables](./variables.md) chapter for more information. For Rust, the kinds are types, lifetimes, and constants. +* An enum defining a *parameter*, which is the terms that can be used to represent the *value* of a variable; see the [variables](./variables.md) chapter for more information. +* Two characters `BINDER_OPEN` and `BINDER_CLOSED` defining the opening and closing characters for binders, e.g., `<` and `>`, to use when parsing. + +## Contents of the language module + +The language module you create has various items in it: + +* A `struct FormalityLang` that defines your language. Some of the contains of `formality_core` (notably the traits that involve bound variables) are + +## Specifying the language for a crate + +That module will contain a language struct named `FormalityLang`. It +Other parts of the formality system (e.g., autoderives and the like) +will need to know the current language you are defining, +and they expect to find it at `crate::FormalityLang`. +Best practice is to add a `use` at the top of your crate defining your language. +For example, the `formality_types` crate has: + +```rust +{{#include ../../../crates/formality-types/src/lib.rs:use_rust_language}} +``` + +and other crates like `formality_rust` have: + +```rust +{{#include ../../../crates/formality-rust/src/lib.rs:use_rust_language}} +``` diff --git a/book/src/formality_core/terms.md b/book/src/formality_core/terms.md new file mode 100644 index 00000000..fc328019 --- /dev/null +++ b/book/src/formality_core/terms.md @@ -0,0 +1,79 @@ +# Defining terms with the `term` macro + +There are two or three key things to understand. The first is the [`#[term]`][term] macro. This is a procedural macro that you can attach to a `struct` or `enum` declaration that represents a piece of Rust syntax or part of the trait checking rules. It auto-derives a bunch of traits and functionality... + +[term]: https://github.com/rust-lang/a-mir-formality/blob/bca36ecd069d6bdff77bffbb628ae3b2ef4f8ef7/crates/formality-macros/src/term.rs#L14-L36 + +* rules for parsing from a string +* a `Debug` impl to serialize back out +* folding and substitution +* upcasting and downcasting impls for convenient type conversion + +For some types, we opt not to use `#[term]`, and instead implement the traits by hand. There are also derives so you can derive some of the traits but not all. + +### Using `#[term]` + +Let's do a simple example. If we had a really simple language, we might define expressions like this: + +```rust +#[term] +enum Expr { + #[cast] + Variable(Variable), + + #[grammar($v0 + $v1)] + Add(Box, Box), +} + +#[term($name)] +struct Variable { + name: String +} +``` + +The `#[term]` macro says that these are terms and we should generate all the boilerplate automatically. Note that it will generate code that references `crate::FormalityLang` so be sure to [define your language appropriately](./lang.md). + +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` that lets you convert a variable to an expression, and a downcast impl `Expr: Downcast` 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`. +* `#[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`, 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)". + +We could also define types and an environment, perhaps something like + +```rust +#[term] +enum Type { + Integer, // Default grammar is just the word `integer` + String // Default grammar is just the word `string` +} + +#[term] // Default grammar is just `env($bindings)` +struct Env { + bindings: Set<(Variable, Type)> +} +``` + +You can see that the `#[term]` macro will generate some default parsing rules if you don't say anything. + +We can then write code like + +```rust +let env: Env = term("env({(x, integer)})"); +``` + +This will parse the string, panicking if either the string cannot be parsed or or if it is ambiguous (can be parsing in mutiple ways). This is super useful in tests. + +These terms are just Rust types, so you can define methods in the usual way, e.g. this `Env::get` method will search for a variable named `v`: + +```rust +impl Env { + pub fn get(&self, v: &Variable) -> Option<&Type> { + self.bindings.iter() + .filter(|b| &b.0 == v) + .map(|b| &b.1) + .next() + } +} +``` diff --git a/book/src/formality_core/variables.md b/book/src/formality_core/variables.md new file mode 100644 index 00000000..ee1fba42 --- /dev/null +++ b/book/src/formality_core/variables.md @@ -0,0 +1 @@ +# Variables diff --git a/book/src/intro.md b/book/src/intro.md new file mode 100644 index 00000000..1e0981f1 --- /dev/null +++ b/book/src/intro.md @@ -0,0 +1 @@ +# Intro diff --git a/crates/formality-check/src/coherence.rs b/crates/formality-check/src/coherence.rs index 9d57d29b..5f9abfd5 100644 --- a/crates/formality-check/src/coherence.rs +++ b/crates/formality-check/src/coherence.rs @@ -1,11 +1,9 @@ use anyhow::bail; use fn_error_context::context; +use formality_core::Downcasted; use formality_prove::Env; use formality_rust::grammar::{Crate, NegTraitImpl, TraitImpl}; -use formality_types::{ - cast::Downcasted, - grammar::{Fallible, Wc, Wcs}, -}; +use formality_types::grammar::{Fallible, Wc, Wcs}; use itertools::Itertools; use crate::Check; diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index 1fb4ae7d..a8e04a03 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -1,6 +1,7 @@ use anyhow::bail; use fn_error_context::context; +use formality_core::Downcasted; use formality_prove::Env; use formality_rust::{ grammar::{ @@ -11,9 +12,8 @@ use formality_rust::{ prove::ToWcs, }; use formality_types::{ - cast::Downcasted, grammar::{Binder, Fallible, Relation, Substitution, Wcs}, - term::Term, + rust::Term, }; impl super::Check<'_> { diff --git a/crates/formality-check/src/where_clauses.rs b/crates/formality-check/src/where_clauses.rs index 88b5cfe1..c0681cb9 100644 --- a/crates/formality-check/src/where_clauses.rs +++ b/crates/formality-check/src/where_clauses.rs @@ -1,13 +1,11 @@ use fn_error_context::context; +use formality_core::Upcast; use formality_prove::Env; use formality_rust::{ grammar::{WhereClause, WhereClauseData}, prove::ToWcs, }; -use formality_types::{ - cast::Upcast, - grammar::{ConstData, Fallible, Parameter, Relation, TraitRef}, -}; +use formality_types::grammar::{ConstData, Fallible, Parameter, Relation, TraitRef}; impl super::Check<'_> { pub(crate) fn prove_where_clauses_well_formed( diff --git a/crates/formality-core/Cargo.toml b/crates/formality-core/Cargo.toml index 1601ca9a..3e589107 100644 --- a/crates/formality-core/Cargo.toml +++ b/crates/formality-core/Cargo.toml @@ -8,6 +8,13 @@ edition = "2021" [dependencies] lazy_static = "1.4.0" env_logger = "*" +stacker = "0.1.15" tracing = "0.1" tracing-subscriber = {version = "0.3", default-features = false, features = ["env-filter", "fmt"]} tracing-tree = { version = "0.2" } +formality-macros = { path = "../formality-macros" } +anyhow = "1.0.75" +contracts = "0.6.3" + +[dev-dependencies] +expect-test = "1.4.1" diff --git a/crates/formality-core/src/binder.rs b/crates/formality-core/src/binder.rs new file mode 100644 index 00000000..94f10efe --- /dev/null +++ b/crates/formality-core/src/binder.rs @@ -0,0 +1,275 @@ +//! Manages binders so that the main rules can be nice and simple. + +use std::sync::atomic::{AtomicUsize, Ordering}; + +use anyhow::bail; +use lazy_static::lazy_static; + +use crate::{ + cast::{Downcast, DowncastFrom, DowncastTo, To, Upcast, UpcastFrom}, + fold::CoreFold, + fold::SubstitutionFn, + language::{CoreKind, CoreParameter, HasKind, Language}, + substitution::CoreSubstitution, + variable::{CoreBoundVar, CoreVariable, DebruijnIndex, VarIndex}, + visit::CoreVisit, + Fallible, +}; + +#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Default)] +pub struct CoreBinder { + kinds: Vec>, + term: T, +} + +impl> CoreBinder { + /// Accesses the contents of the binder. + /// + /// The variables inside will be renamed to fresh var indices + /// that do not alias any other indices seen during this computation. + /// + /// The expectation is that you will create a term and use `Binder::new`. + pub fn open(&self) -> (Vec>, T) { + let (bound_vars, substitution): (Vec>, CoreSubstitution) = self + .kinds + .iter() + .zip(0..) + .map(|(kind, index)| { + let old_bound_var = CoreBoundVar { + debruijn: Some(DebruijnIndex::INNERMOST), + var_index: VarIndex { index }, + kind: *kind, + }; + let new_bound_var = CoreBoundVar::fresh(*kind); + (new_bound_var, (old_bound_var, new_bound_var)) + }) + .unzip(); + + (bound_vars, substitution.apply(&self.term)) + } + + pub fn dummy(term: T) -> Self { + let v: Vec> = vec![]; + Self::new(v, term) + } + + /// Given a set of variables (X, Y, Z) and a term referecing some subset of them, + /// create a binder where exactly those variables are bound (even the ones not used). + pub fn new(variables: impl Upcast>>, term: T) -> Self { + let variables: Vec> = variables.upcast(); + let (kinds, substitution): (Vec>, CoreSubstitution) = variables + .iter() + .zip(0..) + .map(|(old_bound_var, index)| { + let old_bound_var: CoreVariable = old_bound_var.upcast(); + assert!(old_bound_var.is_free()); + let new_bound_var: CoreParameter = CoreBoundVar { + debruijn: Some(DebruijnIndex::INNERMOST), + var_index: VarIndex { index }, + kind: old_bound_var.kind(), + } + .upcast(); + (old_bound_var.kind(), (old_bound_var, new_bound_var)) + }) + .unzip(); + + let term = substitution.apply(&term); + CoreBinder { kinds, term } + } + + /// Given a set of variables (X, Y, Z) and a term referecing some subset of them, + /// create a binder for just those variables that are mentioned. + pub fn mentioned(variables: impl Upcast>>, term: T) -> Self { + let mut variables: Vec> = variables.upcast(); + let fv = term.free_variables(); + variables.retain(|v| fv.contains(v)); + let variables: Vec> = variables.into_iter().collect(); + CoreBinder::new(variables, term) + } + + pub fn into(self) -> CoreBinder + where + T: Into, + { + CoreBinder { + kinds: self.kinds, + term: self.term.into(), + } + } + + /// Number of variables bound by this binder + pub fn len(&self) -> usize { + self.kinds.len() + } + + pub fn is_empty(&self) -> bool { + self.kinds.is_empty() + } + + /// Instantiate the binder with the given parameters, returning an err if the parameters + /// are the wrong number or ill-kinded. + pub fn instantiate_with(&self, parameters: &[impl Upcast>]) -> Fallible { + if parameters.len() != self.kinds.len() { + bail!("wrong number of parameters"); + } + + for ((p, k), i) in parameters.iter().zip(&self.kinds).zip(0..) { + let p: CoreParameter = p.upcast(); + if p.kind() != *k { + bail!( + "parameter {i} has kind {:?} but should have kind {:?}", + p.kind(), + k + ); + } + } + + Ok(self.instantiate(|_kind, index| parameters[index.index].to())) + } + + /// Instantiate the term, replacing each bound variable with `op(i)`. + pub fn instantiate(&self, mut op: impl FnMut(CoreKind, VarIndex) -> CoreParameter) -> T { + let substitution: Vec> = self + .kinds + .iter() + .zip(0..) + .map(|(&kind, index)| op(kind, VarIndex { index })) + .collect(); + + self.term.substitute(&mut |var| match var { + CoreVariable::BoundVar(CoreBoundVar { + debruijn: Some(DebruijnIndex::INNERMOST), + var_index, + kind: _, + }) => Some(substitution[var_index.index].clone()), + + _ => None, + }) + } + + /// Accesses the data inside the binder. Use this for simple tests that extract data + /// that is independent of the bound variables. If that's not the case, use `open`. + pub fn peek(&self) -> &T { + &self.term + } + + /// Returns the kinds of each variable bound by this binder + pub fn kinds(&self) -> &[CoreKind] { + &self.kinds + } + + pub fn map>(&self, op: impl FnOnce(T) -> U) -> CoreBinder { + let (vars, t) = self.open(); + let u = op(t); + CoreBinder::new(vars, u) + } +} + +impl CoreBoundVar { + /// Creates a fresh bound var of the given kind that is not yet part of a binder. + /// You can put this into a term and then use `Binder::new`. + pub fn fresh(kind: CoreKind) -> Self { + lazy_static! { + static ref COUNTER: AtomicUsize = AtomicUsize::new(0); + } + + let index = COUNTER.fetch_add(1, Ordering::SeqCst); + let var_index = VarIndex { index }; + CoreBoundVar { + debruijn: None, + var_index, + kind, + } + } +} + +impl> CoreVisit for CoreBinder { + fn free_variables(&self) -> Vec> { + self.term.free_variables() + } + + fn size(&self) -> usize { + self.term.size() + } + + fn assert_valid(&self) { + self.term.assert_valid(); + } +} + +impl> CoreFold for CoreBinder { + fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self { + let term = self.term.substitute(&mut |v| { + // Shift this variable out through the binder. If that fails, + // it's a variable bound by this binder, so the substitution can't + // affect it, and we can just return None. + let v1 = v.shift_out()?; + + // Get the result of the subst (if any). + let parameter = substitution_fn(v1)?; + + // Shift that result in to account for this binder. + Some(parameter.shift_in()) + }); + + CoreBinder { + kinds: self.kinds.clone(), + term, + } + } + + fn shift_in(&self) -> Self { + let term = self.term.shift_in(); + CoreBinder { + kinds: self.kinds.clone(), + term, + } + } +} + +impl UpcastFrom> for CoreBinder +where + T: Clone, + U: Clone, + T: Upcast, +{ + fn upcast_from(term: CoreBinder) -> Self { + let CoreBinder { kinds, term } = term; + CoreBinder { + kinds, + term: term.upcast(), + } + } +} + +impl DowncastTo> for CoreBinder +where + T: DowncastFrom, +{ + fn downcast_to(&self) -> Option> { + let CoreBinder { kinds, term } = self; + let term = term.downcast()?; + Some(CoreBinder { + kinds: kinds.clone(), + term, + }) + } +} + +impl std::fmt::Debug for CoreBinder +where + T: std::fmt::Debug, +{ + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "<")?; + for (kind, i) in self.kinds.iter().zip(0..) { + if i > 0 { + write!(f, ", ")?; + } + write!(f, "{:?}", kind)?; + } + write!(f, "> ")?; + write!(f, "{:?}", &self.term)?; + Ok(()) + } +} diff --git a/crates/formality-types/src/cast.rs b/crates/formality-core/src/cast.rs similarity index 86% rename from crates/formality-types/src/cast.rs rename to crates/formality-core/src/cast.rs index 7041633b..9be3c84f 100644 --- a/crates/formality-types/src/cast.rs +++ b/crates/formality-core/src/cast.rs @@ -1,6 +1,6 @@ use std::sync::Arc; -use crate::{collections::Set, derive_links::Term}; +use crate::collections::Set; pub trait To { fn to(&self) -> T @@ -295,13 +295,30 @@ where #[macro_export] macro_rules! cast_impl { ($e:ident :: $v:ident ($u:ty)) => { - impl $crate::cast::UpcastFrom<$u> for $e { + impl $crate::UpcastFrom<$u> for $e { fn upcast_from(v: $u) -> $e { $e::$v(v) } } - impl $crate::cast::DowncastTo<$u> for $e { + impl $crate::DowncastTo<$u> for $e { + fn downcast_to(&self) -> Option<$u> { + match self { + $e::$v(u) => Some(Clone::clone(u)), + _ => None, + } + } + } + }; + + (impl($($p:tt)*) $e:ident ($($ep:tt)*) :: $v:ident ($u:ty)) => { + impl<$($p)*> $crate::UpcastFrom<$u> for $e<$($ep)*> { + fn upcast_from(v: $u) -> $e<$($ep)*> { + $e::$v(v) + } + } + + impl<$($p)*> $crate::DowncastTo<$u> for $e<$($ep)*> { fn downcast_to(&self) -> Option<$u> { match self { $e::$v(u) => Some(Clone::clone(u)), @@ -312,13 +329,13 @@ macro_rules! cast_impl { }; (impl($($p:tt)*) $t:ty) => { - impl<$($p)*> $crate::cast::UpcastFrom<$t> for $t { + impl<$($p)*> $crate::UpcastFrom<$t> for $t { fn upcast_from(v: $t) -> $t { v } } - impl<$($p)*> $crate::cast::DowncastTo<$t> for $t { + impl<$($p)*> $crate::DowncastTo<$t> for $t { fn downcast_to(&self) -> Option<$t> { Some(Self::clone(self)) } @@ -326,36 +343,36 @@ macro_rules! cast_impl { }; ($t:ty) => { - impl $crate::cast::UpcastFrom<$t> for $t { + impl $crate::UpcastFrom<$t> for $t { fn upcast_from(v: $t) -> $t { v } } - impl $crate::cast::DowncastTo<$t> for $t { + impl $crate::DowncastTo<$t> for $t { fn downcast_to(&self) -> Option<$t> { Some(Self::clone(self)) } } }; - (($bot:ty) <: ($($mid:ty),*) <: ($top:ty)) => { - impl $crate::cast::UpcastFrom<$bot> for $top { + ($(impl($($p:tt)*))? ($bot:ty) <: ($($mid:ty),*) <: ($top:ty)) => { + impl$(<$($p)*>)? $crate::UpcastFrom<$bot> for $top { fn upcast_from(v: $bot) -> $top { $( - let v: $mid = $crate::cast::Upcast::upcast(v); + let v: $mid = $crate::Upcast::upcast(v); )* - $crate::cast::Upcast::upcast(v) + $crate::Upcast::upcast(v) } } - impl $crate::cast::DowncastTo<$bot> for $top { + impl$(<$($p)*>)? $crate::DowncastTo<$bot> for $top { fn downcast_to(&self) -> Option<$bot> { let v: &$top = self; $( - let v: &$mid = &$crate::cast::DowncastFrom::downcast_from(v)?; + let v: &$mid = &$crate::DowncastFrom::downcast_from(v)?; )* - $crate::cast::DowncastFrom::downcast_from(v) + $crate::DowncastFrom::downcast_from(v) } } }; @@ -371,15 +388,6 @@ impl UpcastFrom<&str> for String { } } -impl UpcastFrom<&str> for T -where - T: Term, -{ - fn upcast_from(text: &str) -> Self { - crate::parse::term(text) - } -} - pub trait Upcasted<'a, T> { fn upcasted(self) -> Box + 'a>; } diff --git a/crates/formality-types/src/collections.rs b/crates/formality-core/src/collections.rs similarity index 96% rename from crates/formality-types/src/collections.rs rename to crates/formality-core/src/collections.rs index 8f33a485..2ecbbe19 100644 --- a/crates/formality-types/src/collections.rs +++ b/crates/formality-core/src/collections.rs @@ -11,11 +11,11 @@ pub type Set = BTreeSet; #[macro_export] macro_rules! set { () => { - $crate::collections::Set::new() + $crate::Set::new() }; ($($t:tt)*) => { - $crate::seq![$($t)*].into_iter().collect::<$crate::collections::Set<_>>() + $crate::seq![$($t)*].into_iter().collect::<$crate::Set<_>>() }; } diff --git a/crates/formality-types/src/derive_links.rs b/crates/formality-core/src/derive_links.rs similarity index 83% rename from crates/formality-types/src/derive_links.rs rename to crates/formality-core/src/derive_links.rs index 37453605..d56e9ae1 100644 --- a/crates/formality-types/src/derive_links.rs +++ b/crates/formality-core/src/derive_links.rs @@ -8,9 +8,7 @@ pub use crate::cast::UpcastFrom; pub use crate::fixed_point; pub use crate::fold::Fold; pub use crate::fold::SubstitutionFn; -pub use crate::grammar::Parameter; -pub use crate::grammar::ParameterKind; -pub use crate::grammar::Variable; pub use crate::parse; pub use crate::term::Term; +pub use crate::variable::Variable; pub use crate::visit::Visit; diff --git a/crates/formality-types/src/fixed_point.rs b/crates/formality-core/src/fixed_point.rs similarity index 100% rename from crates/formality-types/src/fixed_point.rs rename to crates/formality-core/src/fixed_point.rs diff --git a/crates/formality-types/src/fixed_point/stack.rs b/crates/formality-core/src/fixed_point/stack.rs similarity index 100% rename from crates/formality-types/src/fixed_point/stack.rs rename to crates/formality-core/src/fixed_point/stack.rs diff --git a/crates/formality-core/src/fold.rs b/crates/formality-core/src/fold.rs new file mode 100644 index 00000000..6c0cff75 --- /dev/null +++ b/crates/formality-core/src/fold.rs @@ -0,0 +1,99 @@ +use std::sync::Arc; + +use crate::{ + cast::Upcast, + collections::Set, + language::{CoreParameter, HasKind, Language}, + variable::CoreVariable, + visit::CoreVisit, +}; + +/// Invoked for each variable that we find when folding, ignoring variables bound by binders +/// that we traverse. The arguments are as follows: +/// +/// * ParameterKind -- the kind of term in which the variable appeared (type vs lifetime, etc) +/// * Variable -- the variable we encountered +pub type SubstitutionFn<'a, L: Language> = + &'a mut dyn FnMut(CoreVariable) -> Option>; + +pub trait CoreFold: Sized + CoreVisit { + /// Replace uses of variables with values from the substitution. + fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self; + + /// Produce a version of this term where any debruijn indices which appear free are incremented by one. + fn shift_in(&self) -> Self { + self.substitute(&mut |v| Some(v.shift_in().upcast())) + } + + /// Replace all appearances of free variable `v` with `p`. + fn replace_free_var( + &self, + v: impl Upcast>, + p: impl Upcast>, + ) -> Self { + let v: CoreVariable = v.upcast(); + let p: CoreParameter = p.upcast(); + assert!(v.is_free()); + assert!(v.kind() == p.kind()); + self.substitute(&mut |v1| if v == v1 { Some(p.clone()) } else { None }) + } +} + +impl> CoreFold for Vec { + fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self { + self.iter().map(|e| e.substitute(substitution_fn)).collect() + } +} + +impl + Ord> CoreFold for Set { + fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self { + self.iter().map(|e| e.substitute(substitution_fn)).collect() + } +} + +impl> CoreFold for Option { + fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self { + self.as_ref().map(|e| e.substitute(substitution_fn)) + } +} + +impl> CoreFold for Arc { + fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self { + let data = T::substitute(self, substitution_fn); + Arc::new(data) + } +} + +impl CoreFold for usize { + fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self { + *self + } +} + +impl CoreFold for u32 { + fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self { + *self + } +} + +impl CoreFold for () { + fn substitute(&self, _substitution_fn: SubstitutionFn<'_, L>) -> Self {} +} + +impl, B: CoreFold> CoreFold for (A, B) { + fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self { + let (a, b) = self; + (a.substitute(substitution_fn), b.substitute(substitution_fn)) + } +} + +impl, B: CoreFold, C: CoreFold> CoreFold for (A, B, C) { + fn substitute(&self, substitution_fn: SubstitutionFn<'_, L>) -> Self { + let (a, b, c) = self; + ( + a.substitute(substitution_fn), + b.substitute(substitution_fn), + c.substitute(substitution_fn), + ) + } +} diff --git a/crates/formality-types/src/judgment.rs b/crates/formality-core/src/judgment.rs similarity index 91% rename from crates/formality-types/src/judgment.rs rename to crates/formality-core/src/judgment.rs index e206ac45..5547ee66 100644 --- a/crates/formality-types/src/judgment.rs +++ b/crates/formality-core/src/judgment.rs @@ -1,4 +1,4 @@ -use std::{cell::RefCell, collections::BTreeSet, sync::Arc}; +use std::{cell::RefCell, collections::BTreeSet}; use crate::fixed_point::FixedPointStack; @@ -7,13 +7,6 @@ mod test_reachable; pub type JudgmentStack = RefCell>>; -type InferenceRuleClosure = Arc Vec + Send>; - -#[derive(Clone)] -struct InferenceRule { - closure: InferenceRuleClosure, -} - #[macro_export] macro_rules! judgment_fn { ( @@ -26,7 +19,7 @@ macro_rules! judgment_fn { } ) => { $(#[$attr])* - $v fn $name($($input_name : impl $crate::cast::Upcast<$input_ty>),*) -> $crate::collections::Set<$output> { + $v fn $name($($input_name : impl $crate::Upcast<$input_ty>),*) -> $crate::Set<$output> { #[derive(Ord, PartialOrd, Eq, PartialEq, Hash, Clone)] struct __JudgmentStruct($($input_ty),*); @@ -43,7 +36,7 @@ macro_rules! judgment_fn { } } - $(let $input_name: $input_ty = $crate::cast::Upcast::upcast($input_name);)* + $(let $input_name: $input_ty = $crate::Upcast::upcast($input_name);)* $( // Assertions are preconditions @@ -60,7 +53,7 @@ macro_rules! judgment_fn { $crate::fixed_point::fixed_point::< __JudgmentStruct, - $crate::collections::Set<$output>, + $crate::Set<$output>, >( // Tracing span: |input| { @@ -87,7 +80,7 @@ macro_rules! judgment_fn { // Next value: |input: __JudgmentStruct| { - let mut output = $crate::collections::Set::new(); + let mut output = $crate::Set::new(); $crate::push_rules!( $name, @@ -158,6 +151,7 @@ macro_rules! push_rules { // give the user a type error if the name they gave // in the conclusion is not the same as the name of the // function + #[allow(dead_code)] struct WrongJudgmentNameInConclusion; const _: WrongJudgmentNameInConclusion = { let $judgment_name = WrongJudgmentNameInConclusion; @@ -204,7 +198,7 @@ macro_rules! push_rules { (@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:ident : $ty0:ty, $($pats:tt)*) args $args:tt) => { { - if let Some($pat0) = $crate::cast::Downcast::downcast::<$ty0>($in0) { + if let Some($pat0) = $crate::Downcast::downcast::<$ty0>($in0) { $crate::push_rules!(@match inputs($($inputs)*) patterns($($pats)*) args $args); } } @@ -212,20 +206,20 @@ macro_rules! push_rules { (@match inputs($in0:ident) patterns($pat0:ident : $ty0:ty) args $args:tt) => { { - if let Some($pat0) = $crate::cast::Downcast::downcast::<$ty0>($in0) { + if let Some($pat0) = $crate::Downcast::downcast::<$ty0>($in0) { $crate::push_rules!(@match inputs() patterns() args $args); } } }; (@match inputs($in0:ident $($inputs:tt)*) patterns($pat0:pat, $($pats:tt)*) args $args:tt) => { - if let Some($pat0) = $crate::cast::Downcast::downcast(&$in0) { + if let Some($pat0) = $crate::Downcast::downcast(&$in0) { $crate::push_rules!(@match inputs($($inputs)*) patterns($($pats)*) args $args); } }; (@match inputs($in0:ident) patterns($pat0:pat) args $args:tt) => { - if let Some($pat0) = $crate::cast::Downcast::downcast(&$in0) { + if let Some($pat0) = $crate::Downcast::downcast(&$in0) { $crate::push_rules!(@match inputs() patterns() args $args); } }; @@ -277,7 +271,7 @@ macro_rules! push_rules { (@body ($judgment_name:ident, $rule_name:literal, $v:expr, $output:expr)) => { { - let result = $crate::cast::Upcast::upcast($v); + let result = $crate::Upcast::upcast($v); tracing::debug!("produced {:?} from rule {:?} in judgment {:?}", result, $rule_name, stringify!($judgment_name)); $output.insert(result) } diff --git a/crates/formality-types/src/judgment/test_filtered.rs b/crates/formality-core/src/judgment/test_filtered.rs similarity index 91% rename from crates/formality-types/src/judgment/test_filtered.rs rename to crates/formality-core/src/judgment/test_filtered.rs index 458c5971..d162c22a 100644 --- a/crates/formality-types/src/judgment/test_filtered.rs +++ b/crates/formality-core/src/judgment/test_filtered.rs @@ -1,16 +1,17 @@ #![cfg(test)] use std::sync::Arc; +use crate::cast_impl; -use formality_macros::{term, test}; +use crate::judgment_fn; -use crate::{judgment_fn}; - -#[term($edges)] +#[derive(Ord, PartialOrd, Eq, PartialEq, Clone, Debug, Hash)] struct Graph { edges: Vec<(u32, u32)>, } +cast_impl!(Graph); + impl Graph { fn successors(&self, n: u32) -> Vec { self.edges diff --git a/crates/formality-types/src/judgment/test_reachable.rs b/crates/formality-core/src/judgment/test_reachable.rs similarity index 88% rename from crates/formality-types/src/judgment/test_reachable.rs rename to crates/formality-core/src/judgment/test_reachable.rs index e3176b88..4f1c27e4 100644 --- a/crates/formality-types/src/judgment/test_reachable.rs +++ b/crates/formality-core/src/judgment/test_reachable.rs @@ -2,15 +2,15 @@ use std::sync::Arc; -use formality_macros::term; +use crate::{cast_impl, judgment_fn}; -use crate::judgment_fn; - -#[term($edges)] +#[derive(Ord, PartialOrd, Eq, PartialEq, Clone, Debug, Hash)] struct Graph { edges: Vec<(u32, u32)>, } +cast_impl!(Graph); + impl Graph { fn successors(&self, n: u32) -> Vec { self.edges @@ -20,9 +20,6 @@ impl Graph { } } -#[term(reachable($v0,$v1))] -struct TransitiveReachability(Arc, u32); - judgment_fn! { fn transitive_reachable( graph: Arc, diff --git a/crates/formality-core/src/language.rs b/crates/formality-core/src/language.rs new file mode 100644 index 00000000..cd5fb375 --- /dev/null +++ b/crates/formality-core/src/language.rs @@ -0,0 +1,40 @@ +use crate::cast::UpcastFrom; +use crate::term::CoreTerm; +use crate::variable::{CoreBoundVar, CoreExistentialVar, CoreUniversalVar, CoreVariable}; +use std::fmt::Debug; +use std::hash::Hash; + +/// The definition of a "language" +pub trait Language: 'static + Copy + Ord + Hash + Debug + Default { + /// Name of the language, e.g., `"Rust"` + const NAME: &'static str; + + /// An enum defining the *kinds* of generic parameters (e.g., for Rust, + /// types, lifetimes, and constants). + type Kind: Copy + CoreTerm; + + /// An enum defining the *value* of a generic parameter (e.g., a + /// type, a lifetime, etc) + type Parameter: HasKind + + CoreTerm + + UpcastFrom> + + UpcastFrom> + + UpcastFrom> + + UpcastFrom>; + + /// The character (typically `<`) used to open binders. + const BINDING_OPEN: char; + + /// The character (typically `>`) used to open binders. + const BINDING_CLOSE: char; +} + +/// For consistency with types like `CoreVariable`, we write `CoreKind` instead of `Kind`. +pub type CoreKind = L::Kind; + +/// For consistency with types like `CoreVariable`, we write `CoreParameter` instead of `Parameter`. +pub type CoreParameter = L::Parameter; + +pub trait HasKind { + fn kind(&self) -> CoreKind; +} diff --git a/crates/formality-core/src/lib.rs b/crates/formality-core/src/lib.rs index 28b0a023..da0aa334 100644 --- a/crates/formality-core/src/lib.rs +++ b/crates/formality-core/src/lib.rs @@ -1,9 +1,47 @@ +//! `formality-core` contains core definitions that can be used for +//! languages that are not Rust. It is intended to play a role similar +//! to +//! + +#![allow(type_alias_bounds)] + +// Re-export things from dependencies to avoid everybody repeating same set +// in their Cargo.toml. +pub use anyhow::bail; +pub use contracts::requires; pub use tracing::debug; pub use tracing::instrument; pub use tracing::trace; +// Re-export things from formality-macros. +pub use formality_macros::{fixed_point, term, test, Visit}; + +pub type Fallible = anyhow::Result; + +// Modules are *pub* if the items they export aren't meant to be directly +// used, or at least not most of the time. The idea is that you should use +// the names from `declare_language`. +pub mod binder; +mod cast; +mod collections; +pub mod fixed_point; +pub mod fold; +pub mod judgment; +pub mod language; +pub mod parse; +pub mod substitution; +pub mod term; +pub mod variable; +pub mod visit; + +pub use cast::{Downcast, DowncastFrom, DowncastTo, Downcasted, To, Upcast, UpcastFrom, Upcasted}; +pub use collections::Deduplicate; +pub use collections::Map; +pub use collections::Set; +pub use collections::SetExt; + /// Run an action with a tracing log subscriber. The logging level is loaded -/// from `RUST_LOG`. +/// from `RUST_LOG`. The `formality_macro::test` expansion uses this to enable logs. pub fn with_tracing_logs(action: impl FnOnce() -> T) -> T { use tracing_subscriber::{layer::SubscriberExt, EnvFilter, Registry}; use tracing_tree::HierarchicalLayer; @@ -13,3 +51,206 @@ pub fn with_tracing_logs(action: impl FnOnce() -> T) -> T { .with(HierarchicalLayer::new(2).with_writer(std::io::stdout)); tracing::subscriber::with_default(subscriber, action) } + +#[macro_export] +macro_rules! trait_alias { + ( + $(#[$m:meta])* + $v:vis trait $t:ident = $($u:tt)* + ) => { + $($m)* + $v trait $t: $($u)* { } + + impl $t for T + where + T: $($u)* + { } + } +} + +/// Declares a new formality language. +/// This will generate a module with a name you choose that contains various items; +/// among them will be a struct named `FormalityLang` that implements the +/// [`Language`](`crate::language::Language`) trait. +/// When you use the auto-derives or the [`term`](`crate::term`) macro, they will generate +/// code that references `crate::FormalityLang`, so you need to bring that in scope at the root +/// of your crate (e.g., if you called the module `mylang`, you might +/// add `use crate::mylang::FormalityLang` at the root of your crate, +/// so that the auto-derives can find it.) +/// +/// See the mdbook for more coverage of how it works. +#[macro_export] +macro_rules! declare_language { + ( + $(#[$the_lang_m:meta])* + $the_lang_v:vis mod $the_lang:ident { + const NAME = $name:expr; + type Kind = $kind:ty; + type Parameter = $param:ty; + const BINDING_OPEN = $binding_open:expr; + const BINDING_CLOSE = $binding_close:expr; + } + ) => { + $(#[$the_lang_m:meta])* + $the_lang_v mod $the_lang { + use super::*; + + #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug, Default)] + pub struct FormalityLang; + + impl $crate::language::Language for FormalityLang { + const NAME: &'static str = $name; + type Kind = $kind; + type Parameter = $param; + const BINDING_OPEN: char = $binding_open; + const BINDING_CLOSE: char = $binding_close; + } + + $crate::trait_alias! { + pub trait Fold = $crate::fold::CoreFold + } + + $crate::trait_alias! { + pub trait Visit = $crate::visit::CoreVisit + } + + $crate::trait_alias! { + pub trait Parse = $crate::parse::CoreParse + } + + $crate::trait_alias! { + pub trait Term = $crate::term::CoreTerm + } + + pub type Variable = $crate::variable::CoreVariable; + pub type ExistentialVar = $crate::variable::CoreExistentialVar; + pub type UniversalVar = $crate::variable::CoreUniversalVar; + pub type BoundVar = $crate::variable::CoreBoundVar; + pub type DebruijnIndex = $crate::variable::DebruijnIndex; + pub type VarIndex = $crate::variable::VarIndex; + pub type Binder = $crate::binder::CoreBinder; + pub type Substitution = $crate::substitution::CoreSubstitution; + pub type VarSubstitution = $crate::substitution::CoreVarSubstitution; + + /// Parses `text` as a term with no bindings in scope. + #[track_caller] + pub fn term(text: &str) -> T + where + T: Parse, + { + try_term(text).unwrap() + } + + /// Parses `text` as a term with no bindings in scope. + #[track_caller] + pub fn try_term(text: &str) -> anyhow::Result + where + T: Parse, + { + term_with(None::<(String, $param)>, text) + } + + /// Parses `text` as a term with the given bindings in scope. + /// + /// References to the given string will be replaced with the given parameter + /// when parsing types, lifetimes, etc. + #[track_caller] + pub fn term_with(bindings: impl IntoIterator, text: &str) -> anyhow::Result + 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) + } + } + } +} + +/// Declares a newtyped struct that is an arbitrary (string) identifier, +/// like the name of a module or something. +#[macro_export] +macro_rules! id { + ($n:ident) => { + #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] + pub struct $n { + data: std::sync::Arc, + } + + const _: () = { + use $crate::fold::{self, CoreFold}; + use $crate::parse::{self, CoreParse}; + use $crate::variable::CoreVariable; + use $crate::visit::CoreVisit; + + $crate::cast_impl!($n); + + impl $n { + pub fn new(s: &str) -> $n { + $n { + data: std::sync::Arc::new(s.to_string()), + } + } + } + + impl std::ops::Deref for $n { + type Target = String; + + fn deref(&self) -> &String { + &self.data + } + } + + impl CoreVisit for $n { + fn free_variables(&self) -> Vec> { + vec![] + } + + fn size(&self) -> usize { + 1 + } + + fn assert_valid(&self) {} + } + + impl CoreFold for $n { + fn substitute( + &self, + _substitution_fn: fold::SubstitutionFn<'_, crate::FormalityLang>, + ) -> Self { + self.clone() + } + } + + impl CoreParse for $n { + fn parse<'t>( + _scope: &parse::Scope, + text: &'t str, + ) -> parse::ParseResult<'t, Self> { + let (string, text) = parse::identifier(text)?; + let n = $n::new(&string); + Ok((n, text)) + } + } + + impl std::fmt::Debug for $n { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{}", &self.data) + } + } + }; + }; +} diff --git a/crates/formality-types/src/parse.rs b/crates/formality-core/src/parse.rs similarity index 77% rename from crates/formality-types/src/parse.rs rename to crates/formality-core/src/parse.rs index 49ab1490..9e434e38 100644 --- a/crates/formality-types/src/parse.rs +++ b/crates/formality-core/src/parse.rs @@ -1,71 +1,26 @@ use std::{str::FromStr, sync::Arc}; use crate::{ - cast::{To, Upcast}, + binder::CoreBinder, + cast::To, collections::Set, - derive_links::{Fold, Parameter, ParameterKind, Term}, - grammar::{Binder, BoundVar}, + language::{CoreKind, CoreParameter, Language}, set, + term::CoreTerm, + variable::CoreBoundVar, }; use std::fmt::Debug; -mod test; - -/// Parses `text` as a term with no bindings in scope. -#[track_caller] -pub fn term(text: &str) -> T -where - T: Parse, -{ - try_term(text).unwrap() -} - -/// Parses `text` as a term with no bindings in scope. -#[track_caller] -pub fn try_term(text: &str) -> anyhow::Result -where - T: Parse, -{ - term_with(None::<(String, Parameter)>, text) -} - -/// Parses `text` as a term with the given bindings in scope. -/// -/// References to the given string will be replaced with the given parameter -/// when parsing types, lifetimes, etc. -#[track_caller] -pub fn term_with(bindings: impl IntoIterator, text: &str) -> anyhow::Result -where - T: Parse, - B: Upcast<(String, Parameter)>, -{ - let scope = 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 !skip_whitespace(remainder).is_empty() { - anyhow::bail!("extra tokens after parsing {text:?} to {t:?}: {remainder:?}"); - } - Ok(t) -} - -/// Trait for parsing a [`Term`](`crate::term::Term`) as input. -pub trait Parse: Sized + Debug { +/// Trait for parsing a [`Term`](`crate::term::Term`) as input. +pub trait CoreParse: Sized + Debug { /// Parse a single instance of this type, returning an error if no such /// instance is present. - fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self>; + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self>; /// Parse many instances of self, expecting `close_char` to appear after the last instance /// (`close_char` is not consumed). fn parse_many<'t>( - scope: &Scope, + scope: &Scope, mut text: &'t str, close_char: char, ) -> ParseResult<'t, Vec> { @@ -80,7 +35,7 @@ pub trait Parse: Sized + Debug { /// Comma separated list with optional trailing comma. fn parse_comma<'t>( - scope: &Scope, + scope: &Scope, mut text: &'t str, close_char: char, ) -> ParseResult<'t, Vec> { @@ -144,20 +99,20 @@ pub type ParseResult<'t, T> = Result<(T, &'t str), Set>>; /// Tracks the variables in scope at this point in parsing. #[derive(Clone, Debug)] -pub struct Scope { - bindings: Vec<(String, Parameter)>, +pub struct Scope { + bindings: Vec<(String, CoreParameter)>, } -impl Scope { +impl Scope { /// Creates a new scope with the given set of bindings. - pub fn new(bindings: impl IntoIterator) -> Self { + pub fn new(bindings: impl IntoIterator)>) -> Self { Self { bindings: bindings.into_iter().collect(), } } /// Look for a variable with the given name. - pub fn lookup(&self, name: &str) -> Option { + pub fn lookup(&self, name: &str) -> Option> { self.bindings .iter() .rev() @@ -166,7 +121,10 @@ impl Scope { } /// Create a new scope that extends `self` with `bindings`. - pub fn with_bindings(&self, bindings: impl IntoIterator) -> Self { + pub fn with_bindings( + &self, + bindings: impl IntoIterator)>, + ) -> Self { let mut s = self.clone(); s.bindings.extend(bindings); s @@ -175,20 +133,21 @@ impl Scope { /// Records a single binding, used when parsing [`Binder`]. #[derive(Clone, Debug)] -pub struct Binding { +pub struct Binding { /// Name the user during during parsing pub name: String, /// The bound var representation. - pub bound_var: BoundVar, + pub bound_var: CoreBoundVar, } -impl Parse for Vec +impl CoreParse for Vec where - T: Parse, + L: Language, + T: CoreParse, { #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { let ((), text) = expect_char('[', text)?; let (v, text) = T::parse_comma(scope, text, ']')?; let ((), text) = expect_char(']', text)?; @@ -196,12 +155,13 @@ where } } -impl Parse for Set +impl CoreParse for Set where - T: Parse + Ord, + L: Language, + T: CoreParse + Ord, { #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { let ((), text) = expect_char('{', text)?; let (v, text) = T::parse_comma(scope, text, '}')?; let ((), text) = expect_char('}', text)?; @@ -210,12 +170,13 @@ where } } -impl Parse for Option +impl CoreParse for Option where - T: Parse, + L: Language, + T: CoreParse, { #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { match T::parse(scope, text) { Ok((value, text)) => Ok((Some(value), text)), Err(_) => Ok((None, text)), @@ -224,65 +185,76 @@ where } /// Binding grammar is `$kind $name`, e.g., `ty Foo`. -impl Parse for Binding { +impl CoreParse for Binding { #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { - let (kind, text) = ParameterKind::parse(scope, text)?; + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + let (kind, text) = >::parse(scope, text)?; let (name, text) = identifier(text)?; - let bound_var = crate::grammar::fresh_bound_var(kind); + let bound_var = CoreBoundVar::fresh(kind); Ok((Binding { name, bound_var }, text)) } } /// Parse a binder: find the names in scope, parse the contents, and then /// replace names with debruijn indices. -impl Parse for Binder +impl CoreParse for CoreBinder where - T: Term + Parse + Fold, + L: Language, + T: CoreTerm, { #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { - let ((), text) = expect_char('<', text)?; + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + let ((), text) = expect_char(L::BINDING_OPEN, text)?; let (bindings, text) = Binding::parse_comma(scope, text, '>')?; - let ((), text) = expect_char('>', text)?; + let ((), text) = expect_char(L::BINDING_CLOSE, text)?; // parse the contents with those names in scope let scope1 = scope.with_bindings(bindings.iter().map(|b| (b.name.clone(), b.bound_var.to()))); let (data, text) = T::parse(&scope1, text)?; - let kvis: Vec = bindings.iter().map(|b| b.bound_var).collect(); - Ok((Binder::new(kvis, data), text)) + let kvis: Vec> = bindings.iter().map(|b| b.bound_var).collect(); + Ok((CoreBinder::new(kvis, data), text)) } } -impl Parse for Arc +impl CoreParse for Arc where - T: Parse, + L: Language, + T: CoreParse, { - fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { let (data, text) = T::parse(scope, text)?; Ok((Arc::new(data), text)) } } -impl Parse for usize { +impl CoreParse for usize +where + L: Language, +{ #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(_scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + fn parse<'t>(_scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { number(text) } } -impl Parse for u32 { +impl CoreParse for u32 +where + L: Language, +{ #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(_scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + fn parse<'t>(_scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { number(text) } } -impl Parse for u64 { +impl CoreParse for u64 +where + L: Language, +{ #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(_scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + fn parse<'t>(_scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { number(text) } } @@ -442,9 +414,9 @@ fn accumulate<'t>( Ok((buffer, text1)) } -impl Parse for (A, B) { +impl, B: CoreParse> CoreParse for (A, B) { #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { let ((), text) = expect_char('(', text)?; let (a, text) = A::parse(scope, text)?; let ((), text) = expect_char(',', text)?; @@ -455,18 +427,18 @@ impl Parse for (A, B) { } } -impl Parse for () { +impl CoreParse for () { #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { let ((), text) = expect_char('(', text)?; let ((), text) = expect_char(')', text)?; Ok(((), text)) } } -impl Parse for (A, B, C) { +impl, B: CoreParse, C: CoreParse> CoreParse for (A, B, C) { #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { let ((), text) = expect_char('(', text)?; let (a, text) = A::parse(scope, text)?; let ((), text) = expect_char(',', text)?; diff --git a/crates/formality-core/src/parse/test.rs b/crates/formality-core/src/parse/test.rs new file mode 100644 index 00000000..8b137891 --- /dev/null +++ b/crates/formality-core/src/parse/test.rs @@ -0,0 +1 @@ + diff --git a/crates/formality-core/src/substitution.rs b/crates/formality-core/src/substitution.rs new file mode 100644 index 00000000..c5d0a257 --- /dev/null +++ b/crates/formality-core/src/substitution.rs @@ -0,0 +1,216 @@ +use crate::{ + cast::{Upcast, UpcastFrom}, + collections::{Map, Set}, + fold::CoreFold, + language::{CoreParameter, Language}, + variable::CoreVariable, + visit::CoreVisit, +}; + +#[derive(Clone, Default, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct CoreSubstitution { + map: Map, CoreParameter>, +} + +impl CoreSubstitution { + /// Returns the variables that will be substituted for a new value. + pub fn domain(&self) -> Set> { + self.map.keys().cloned().collect() + } + + /// Returns the parameters that that will be substituted for a new value. + pub fn range(&self) -> Set> { + self.map.values().cloned().collect() + } + + /// True if `v` is in this substitution's domain + pub fn maps(&self, v: CoreVariable) -> bool { + self.map.contains_key(&v) + } + + pub fn iter(&self) -> impl Iterator, CoreParameter)> + '_ { + self.map.iter().map(|(v, p)| (*v, p.clone())) + } + + /// An empty substitution is just the identity function. + pub fn is_empty(&self) -> bool { + self.map.is_empty() + } +} + +impl std::fmt::Debug for CoreSubstitution { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let mut f = f.debug_set(); + for (v, p) in self.iter() { + f.entry(&Entry { v, p }); + struct Entry { + v: CoreVariable, + p: CoreParameter, + } + impl std::fmt::Debug for Entry { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{:?} => {:?}", self.v, self.p) + } + } + } + f.finish() + } +} + +impl std::ops::SubAssign for CoreSubstitution +where + Vs: Upcast>>, +{ + fn sub_assign(&mut self, rhs: Vs) { + let rhs: Vec> = rhs.upcast(); + + for v in rhs { + self.map.remove(&v); + } + } +} + +impl IntoIterator for CoreSubstitution { + type Item = (CoreVariable, CoreParameter); + + type IntoIter = std::collections::btree_map::IntoIter, CoreParameter>; + + fn into_iter(self) -> Self::IntoIter { + self.map.into_iter() + } +} + +impl Extend<(A, B)> for CoreSubstitution +where + A: Upcast>, + B: Upcast>, +{ + fn extend>(&mut self, iter: T) { + self.map + .extend(iter.into_iter().map(|(v, p)| (v.upcast(), p.upcast()))); + } +} + +impl FromIterator<(A, B)> for CoreSubstitution +where + A: Upcast>, + B: Upcast>, +{ + fn from_iter>(iter: T) -> Self { + let mut s = CoreSubstitution::default(); + s.extend(iter); + s + } +} + +impl UpcastFrom<(A, B)> for CoreSubstitution +where + A: Upcast>, + B: Upcast>, +{ + fn upcast_from(term: (A, B)) -> Self { + let term: (CoreVariable, CoreParameter) = term.upcast(); + std::iter::once(term).collect() + } +} + +impl CoreSubstitution { + pub fn apply>(&self, t: &T) -> T { + t.substitute(&mut |v| self.map.get(&v).cloned()) + } + + pub fn get(&self, v: CoreVariable) -> Option> { + self.map.get(&v).cloned() + } +} + +impl CoreFold for CoreSubstitution { + fn substitute(&self, substitution_fn: crate::fold::SubstitutionFn<'_, L>) -> Self { + self.iter() + .map(|(v, p)| (v, p.substitute(substitution_fn))) + .collect() + } +} + +impl CoreVisit for CoreSubstitution { + fn free_variables(&self) -> Vec> { + let mut v = self.range().free_variables(); + v.extend(self.domain()); + v + } + + fn size(&self) -> usize { + self.range().iter().map(|r| r.size()).sum() + } + + fn assert_valid(&self) { + self.range().assert_valid() + } +} + +impl std::ops::Index> for CoreSubstitution { + type Output = CoreParameter; + + fn index(&self, index: CoreVariable) -> &Self::Output { + &self.map[&index] + } +} + +/// A substitution that is only between variables. +/// These are reversible. +#[derive(Clone, Default, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct CoreVarSubstitution { + map: Map, CoreVariable>, +} + +impl Extend<(A, B)> for CoreVarSubstitution +where + L: Language, + A: Upcast>, + B: Upcast>, +{ + fn extend>(&mut self, iter: T) { + self.map + .extend(iter.into_iter().map(|(v, p)| (v.upcast(), p.upcast()))); + } +} + +impl FromIterator<(A, B)> for CoreVarSubstitution +where + L: Language, + A: Upcast>, + B: Upcast>, +{ + fn from_iter>(iter: T) -> Self { + let mut s = CoreVarSubstitution::default(); + s.extend(iter); + s + } +} + +impl CoreVarSubstitution { + pub fn reverse(&self) -> CoreVarSubstitution { + self.map.iter().map(|(k, v)| (*v, *k)).collect() + } + + pub fn apply>(&self, t: &T) -> T { + t.substitute(&mut |v| Some(self.map.get(&v)?.upcast())) + } + + pub fn map_var(&self, v: CoreVariable) -> Option> { + self.map.get(&v).copied() + } + + pub fn maps_var(&self, v: CoreVariable) -> bool { + self.map.contains_key(&v) + } + + pub fn insert_mapping( + &mut self, + from: impl Upcast>, + to: impl Upcast>, + ) { + let x = self.map.insert(from.upcast(), to.upcast()); + assert!(x.is_none()); + } +} diff --git a/crates/formality-core/src/term.rs b/crates/formality-core/src/term.rs new file mode 100644 index 00000000..664adf40 --- /dev/null +++ b/crates/formality-core/src/term.rs @@ -0,0 +1,43 @@ +use std::{fmt::Debug, hash::Hash, sync::Arc}; + +use crate::{ + binder::CoreBinder, + cast::{DowncastFrom, Upcast}, + collections::Set, + fold::CoreFold, + language::Language, + parse::CoreParse, +}; + +pub trait CoreTerm: + Clone + + CoreFold + + CoreParse + + Ord + + Eq + + Hash + + Debug + + Upcast + + DowncastFrom + + 'static + + Sized +{ +} + +impl> CoreTerm for Vec {} + +impl> CoreTerm for Set {} + +impl> CoreTerm for Option {} + +impl> CoreTerm for Arc {} + +impl CoreTerm for usize {} + +impl CoreTerm for u32 {} + +impl, B: CoreTerm> CoreTerm for (A, B) {} + +impl> CoreTerm for CoreBinder {} + +impl CoreTerm for () {} diff --git a/crates/formality-core/src/variable.rs b/crates/formality-core/src/variable.rs new file mode 100644 index 00000000..4e3d7ff5 --- /dev/null +++ b/crates/formality-core/src/variable.rs @@ -0,0 +1,214 @@ +use crate::cast::Upcast; +use crate::language::CoreKind; +use crate::language::Language; +use crate::visit::CoreVisit; + +/// A term representing a variable. +#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum CoreVariable { + /// A "universal free variable" is a variable that appears + /// free in all terms because it is bound in the environment. + /// Universal means that it arose from a "forall" binder. + /// Universal variables are a kind of placeholder meant to represent + /// "some value" about which you know nothing except what you are + /// told to assume. + UniversalVar(CoreUniversalVar), + + /// An "existential free variable" is a variable that appears + /// free in all terms because it is bound in the environment. + /// Existential means that it arose from a "exists" binder. + /// Existential variables are a kind of placeholder for which + /// you will eventually find some specific value, so the rules typically + /// accumulate constraints. + ExistentialVar(CoreExistentialVar), + + /// A bound variable is one that is bound by some enclosing `Binder` + /// in this term (or a binder about to be constructex; see `fresh_bound_var`). + BoundVar(CoreBoundVar), +} + +impl CoreVariable { + pub fn kind(&self) -> CoreKind { + match self { + CoreVariable::UniversalVar(v) => v.kind, + CoreVariable::ExistentialVar(v) => v.kind, + CoreVariable::BoundVar(v) => v.kind, + } + } + + /// Shift a variable in through `binders` binding levels. + /// Only affects bound variables. + pub fn shift_in(&self) -> Self { + if let CoreVariable::BoundVar(CoreBoundVar { + debruijn: Some(db), + var_index, + kind, + }) = self + { + CoreBoundVar { + debruijn: Some(db.shift_in()), + var_index: *var_index, + kind: *kind, + } + .upcast() + } else { + *self + } + } + + /// Shift a variable out through `binders` binding levels. + /// Only affects bound variables. Returns None if the variable + /// is bound within those binding levels. + pub fn shift_out(&self) -> Option { + if let CoreVariable::BoundVar(CoreBoundVar { + debruijn: Some(db), + var_index, + kind, + }) = self + { + db.shift_out().map(|db1| { + CoreBoundVar { + debruijn: Some(db1), + var_index: *var_index, + kind: *kind, + } + .upcast() + }) + } else { + Some(*self) + } + } + + /// A variable is *free* (i.e., not bound by any internal binder) + /// if it is an existential variable, a universal, or has a debruijn + /// index of `None`. The latter occurs when you `open` a binder (and before + /// you close it back up again). + pub fn is_free(&self) -> bool { + match self { + CoreVariable::UniversalVar(_) + | CoreVariable::ExistentialVar(_) + | CoreVariable::BoundVar(CoreBoundVar { + debruijn: None, + var_index: _, + kind: _, + }) => true, + + CoreVariable::BoundVar(CoreBoundVar { + debruijn: Some(_), + var_index: _, + kind: _, + }) => false, + } + } + + pub fn is_universal(&self) -> bool { + match self { + CoreVariable::UniversalVar(_) => true, + CoreVariable::ExistentialVar(_) => false, + CoreVariable::BoundVar(_) => false, + } + } +} + +impl CoreVisit for CoreVariable { + fn free_variables(&self) -> Vec> { + if self.is_free() { + vec![*self] + } else { + vec![] + } + } + + fn size(&self) -> usize { + 1 + } + + fn assert_valid(&self) {} +} + +#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct CoreExistentialVar { + pub kind: CoreKind, + pub var_index: VarIndex, +} + +impl CoreVisit for CoreExistentialVar { + fn free_variables(&self) -> Vec> { + vec![self.upcast()] + } + + fn size(&self) -> usize { + 1 + } + + fn assert_valid(&self) {} +} + +/// A *universal variable* is a dummy variable about which nothing is known except +/// that which we see in the environment. When we want to prove something +/// is true for all `T` (`∀T`), we replace `T` with a universal variable. +#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct CoreUniversalVar { + pub kind: CoreKind, + pub var_index: VarIndex, +} + +/// Identifies a bound variable. +#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct CoreBoundVar { + /// Identifies the binder that contained this variable, counting "outwards". + /// When you create a binder with `Binder::new`, + /// When you open a Binder, you get back `Bound + pub debruijn: Option, + pub var_index: VarIndex, + pub kind: CoreKind, +} + +#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct DebruijnIndex { + pub index: usize, +} + +impl DebruijnIndex { + pub const INNERMOST: DebruijnIndex = DebruijnIndex { index: 0 }; + + /// Adjust this debruijn index through a binder level. + pub fn shift_in(&self) -> Self { + DebruijnIndex { + index: self.index + 1, + } + } + + /// Adjust this debruijn index *outward* through a binder level, if possible. + pub fn shift_out(&self) -> Option { + if self.index > 0 { + Some(DebruijnIndex { + index: self.index - 1, + }) + } else { + None + } + } +} + +#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct VarIndex { + pub index: usize, +} + +impl VarIndex { + pub const ZERO: VarIndex = VarIndex { index: 0 }; +} + +impl std::ops::Add for VarIndex { + type Output = VarIndex; + + fn add(self, rhs: usize) -> Self::Output { + VarIndex { + index: self.index + rhs, + } + } +} + +mod cast_impls; +mod debug_impls; diff --git a/crates/formality-core/src/variable/cast_impls.rs b/crates/formality-core/src/variable/cast_impls.rs new file mode 100644 index 00000000..68c72c95 --- /dev/null +++ b/crates/formality-core/src/variable/cast_impls.rs @@ -0,0 +1,10 @@ +use super::*; +use crate::cast_impl; + +cast_impl!(impl(L: Language) CoreVariable); +cast_impl!(impl(L: Language) CoreBoundVar); +cast_impl!(impl(L: Language) CoreExistentialVar); +cast_impl!(impl(L: Language) CoreUniversalVar); +cast_impl!(impl(L: Language) CoreVariable(L)::ExistentialVar(CoreExistentialVar)); +cast_impl!(impl(L: Language) CoreVariable(L)::BoundVar(CoreBoundVar)); +cast_impl!(impl(L: Language) CoreVariable(L)::UniversalVar(CoreUniversalVar)); diff --git a/crates/formality-core/src/variable/debug_impls.rs b/crates/formality-core/src/variable/debug_impls.rs new file mode 100644 index 00000000..e981fa8f --- /dev/null +++ b/crates/formality-core/src/variable/debug_impls.rs @@ -0,0 +1,54 @@ +use super::*; + +impl std::fmt::Debug for CoreVariable { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + Self::UniversalVar(arg0) => write!(f, "{:?}", arg0), + Self::ExistentialVar(arg0) => write!(f, "{:?}", arg0), + Self::BoundVar(arg0) => write!(f, "{:?}", arg0), + } + } +} + +impl std::fmt::Debug for CoreUniversalVar { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let CoreUniversalVar { var_index, kind } = self; + write!(f, "!{:?}_{:?}", kind, var_index) + } +} + +impl std::fmt::Debug for CoreExistentialVar { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let CoreExistentialVar { var_index, kind } = self; + write!(f, "?{:?}_{:?}", kind, var_index) + } +} + +impl std::fmt::Debug for VarIndex { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{}", self.index) + } +} + +impl std::fmt::Debug for CoreBoundVar { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + CoreBoundVar { + debruijn: None, + var_index, + kind, + } => write!(f, "^{:?}_{:?}", kind, var_index), + CoreBoundVar { + debruijn: Some(db), + var_index, + kind, + } => write!(f, "^{:?}{:?}_{:?}", kind, db.index, var_index), + } + } +} + +impl std::fmt::Debug for DebruijnIndex { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "^{}", self.index) + } +} diff --git a/crates/formality-core/src/visit.rs b/crates/formality-core/src/visit.rs new file mode 100644 index 00000000..2f31114d --- /dev/null +++ b/crates/formality-core/src/visit.rs @@ -0,0 +1,208 @@ +use std::sync::Arc; + +use crate::{collections::Set, language::Language, variable::CoreVariable}; + +pub trait CoreVisit { + /// Extract the list of free variables (for the purposes of this function, defined by `Variable::is_free`). + /// The list may contain duplicates and must be in a determinstic order (though the order itself isn't important). + fn free_variables(&self) -> Vec>; + + /// Measures the overall size of the term by counting constructors etc. + /// Used to determine overflow. + fn size(&self) -> usize; + + /// Asserts various validity constraints and panics if they are not held. + /// These validition constraints should never fail unless there is a bug in our logic. + /// This is to aid with fuzzing and bug detection. + fn assert_valid(&self); + + /// True if this term references only universal variables. + /// This means that it contains no existential variables. + /// If this is a goal, then when we prove it true, we don't expect any substitution. + /// This is similar, but not *identical*, to the commonly used term "ground term", + /// which in Prolog refers to a term that contains no variables. The difference here + /// is that the term may contain variables, but only those instantiated universally (∀). + fn references_only_universal_variables(&self) -> bool { + self.free_variables().iter().all(|v| match v { + CoreVariable::UniversalVar(_) => true, + CoreVariable::ExistentialVar(_) => false, + CoreVariable::BoundVar(_) => false, + }) + } +} + +impl> CoreVisit for Vec { + fn free_variables(&self) -> Vec> { + self.iter().flat_map(|e| e.free_variables()).collect() + } + + fn size(&self) -> usize { + self.iter().map(|e| e.size()).sum() + } + + fn assert_valid(&self) { + self.iter().for_each(|e| e.assert_valid()); + } +} + +impl + Ord> CoreVisit for Set { + fn free_variables(&self) -> Vec> { + self.iter().flat_map(|e| e.free_variables()).collect() + } + + fn size(&self) -> usize { + self.iter().map(|e| e.size()).sum() + } + + fn assert_valid(&self) { + self.iter().for_each(|e| e.assert_valid()); + } +} + +impl> CoreVisit for Option { + fn free_variables(&self) -> Vec> { + self.iter().flat_map(|e| e.free_variables()).collect() + } + + fn size(&self) -> usize { + self.as_ref().map(|e| e.size()).unwrap_or(0) + } + + fn assert_valid(&self) { + self.iter().for_each(|e| e.assert_valid()); + } +} + +impl + ?Sized> CoreVisit for Arc { + fn free_variables(&self) -> Vec> { + T::free_variables(self) + } + + fn size(&self) -> usize { + T::size(self) + } + + fn assert_valid(&self) { + T::assert_valid(self) + } +} + +impl CoreVisit for usize { + fn free_variables(&self) -> Vec> { + vec![] + } + + fn size(&self) -> usize { + 1 + } + + fn assert_valid(&self) {} +} + +impl CoreVisit for u32 { + fn free_variables(&self) -> Vec> { + vec![] + } + + fn size(&self) -> usize { + 1 + } + + fn assert_valid(&self) {} +} + +impl CoreVisit for u128 { + fn free_variables(&self) -> Vec> { + vec![] + } + + fn size(&self) -> usize { + std::mem::size_of::() + } + + fn assert_valid(&self) {} +} + +impl CoreVisit for () { + fn free_variables(&self) -> Vec> { + vec![] + } + + fn size(&self) -> usize { + 0 + } + + fn assert_valid(&self) {} +} + +impl, B: CoreVisit> CoreVisit for (A, B) { + fn free_variables(&self) -> Vec> { + let (a, b) = self; + let mut fv = vec![]; + fv.extend(a.free_variables()); + fv.extend(b.free_variables()); + fv + } + + fn size(&self) -> usize { + let (a, b) = self; + a.size() + b.size() + } + + fn assert_valid(&self) { + let (a, b) = self; + a.assert_valid(); + b.assert_valid(); + } +} + +impl, B: CoreVisit, C: CoreVisit> CoreVisit for (A, B, C) { + fn free_variables(&self) -> Vec> { + let (a, b, c) = self; + let mut fv = vec![]; + fv.extend(a.free_variables()); + fv.extend(b.free_variables()); + fv.extend(c.free_variables()); + fv + } + + fn size(&self) -> usize { + let (a, b, c) = self; + a.size() + b.size() + c.size() + } + + fn assert_valid(&self) { + let (a, b, c) = self; + a.assert_valid(); + b.assert_valid(); + c.assert_valid(); + } +} + +impl + ?Sized> CoreVisit for &A { + fn free_variables(&self) -> Vec> { + A::free_variables(self) + } + + fn size(&self) -> usize { + A::size(self) + } + + fn assert_valid(&self) { + A::assert_valid(self) + } +} + +impl> CoreVisit for [A] { + fn free_variables(&self) -> Vec> { + self.iter().flat_map(|e| A::free_variables(e)).collect() + } + + fn size(&self) -> usize { + self.iter().map(|e| A::size(e)).sum() + } + + fn assert_valid(&self) { + self.iter().for_each(|e| A::assert_valid(e)); + } +} diff --git a/crates/formality-macros/src/cast.rs b/crates/formality-macros/src/cast.rs index 9a69d38e..ef05b221 100644 --- a/crates/formality-macros/src/cast.rs +++ b/crates/formality-macros/src/cast.rs @@ -15,7 +15,7 @@ pub(crate) fn upcast_impls(s: synstructure::Structure) -> Vec { fn self_upcast(s: &synstructure::Structure) -> TokenStream { s.gen_impl(quote! { - use crate::derive_links::{UpcastFrom}; + use formality_core::UpcastFrom; gen impl UpcastFrom for @Self { fn upcast_from(term: Self) -> Self { @@ -31,7 +31,7 @@ fn upcast_to_variant(s: &synstructure::Structure, v: &VariantInfo) -> TokenStrea let variant_construct = v.construct(|_field, index| &binding_names[index]); s.gen_impl(quote! { - use crate::derive_links::{UpcastFrom}; + use formality_core::{UpcastFrom}; gen impl UpcastFrom<(#(#binding_tys),*)> for @Self { fn upcast_from(term: (#(#binding_tys),*)) -> Self { @@ -54,7 +54,7 @@ pub(crate) fn downcast_impls(s: synstructure::Structure) -> Vec { fn self_downcast(s: &synstructure::Structure) -> TokenStream { s.gen_impl(quote! { - use crate::derive_links::{DowncastTo}; + use formality_core::{DowncastTo}; gen impl DowncastTo for @Self { fn downcast_to(&self) -> Option { @@ -78,7 +78,7 @@ fn downcast_to_variant(s: &synstructure::Structure, v: &VariantInfo) -> TokenStr }); s.gen_impl(quote! { - use crate::derive_links::{DowncastTo}; + use formality_core::{DowncastTo}; gen impl DowncastTo<(#(#binding_tys),*)> for @Self { fn downcast_to(&self) -> Option<(#(#binding_tys),*)> { diff --git a/crates/formality-macros/src/fixed_point.rs b/crates/formality-macros/src/fixed_point.rs index 71a84762..1d7daa43 100644 --- a/crates/formality-macros/src/fixed_point.rs +++ b/crates/formality-macros/src/fixed_point.rs @@ -82,7 +82,7 @@ pub(crate) fn fixed_point( thread_local! { static __CACHE: std::cell::RefCell< - crate::derive_links::fixed_point::FixedPointStack< + formality_core::fixed_point::FixedPointStack< (#(#input_tys),*), #output_ty > @@ -145,7 +145,7 @@ pub(crate) fn fixed_point( quote! { { #thread_local - crate::derive_links::fixed_point::fixed_point( + formality_core::fixed_point::fixed_point( &__CACHE, #input_expr, #default_expr, diff --git a/crates/formality-macros/src/fold.rs b/crates/formality-macros/src/fold.rs index 33fc450c..139efbab 100644 --- a/crates/formality-macros/src/fold.rs +++ b/crates/formality-macros/src/fold.rs @@ -12,17 +12,17 @@ pub(crate) fn derive_fold(mut s: synstructure::Structure) -> TokenStream { vi.construct(|_, index| { let bind = &bindings[index]; quote! { - Fold::substitute(#bind, substitution_fn) + CoreFold::substitute(#bind, substitution_fn) } }) }); // s.add_bounds(synstructure::AddBounds::None); s.gen_impl(quote! { - use crate::derive_links::{Fold, SubstitutionFn, Parameter, ParameterKind}; + use formality_core::{fold::CoreFold, fold::SubstitutionFn}; - gen impl Fold for @Self { - fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self { + gen impl CoreFold for @Self { + fn substitute(&self, substitution_fn: SubstitutionFn<'_, crate::FormalityLang>) -> Self { match self { #substitute_body } diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs index 668862a9..a3fa1f16 100644 --- a/crates/formality-macros/src/parse.rs +++ b/crates/formality-macros/src/parse.rs @@ -46,10 +46,10 @@ pub(crate) fn derive_parse_with_spec( let type_name = as_literal(&s.ast().ident); Ok(s.gen_impl(quote! { - use crate::derive_links::{parse}; + use formality_core::parse; - gen impl parse::Parse for @Self { - fn parse<'t>(scope: &parse::Scope, text: &'t str) -> parse::ParseResult<'t, Self> + gen impl parse::CoreParse for @Self { + fn parse<'t>(scope: &parse::Scope, text: &'t str) -> parse::ParseResult<'t, Self> { let __span = tracing::span!(tracing::Level::TRACE, "parse", type_name = #type_name, ?scope, ?text); let __guard = __span.enter(); @@ -142,7 +142,7 @@ fn parse_variant_with_attr( mode: FieldMode::Single, } => { quote_spanned! { - name.span() => let (#name, text) = parse::Parse::parse(scope, text)?; + name.span() => let (#name, text) = parse::CoreParse::parse(scope, text)?; } } @@ -152,7 +152,7 @@ fn parse_variant_with_attr( } => { let lookahead = lookahead(name, next_op)?; quote_spanned! { - name.span() => let (#name, text) = parse::Parse::parse_many(scope, text, #lookahead)?; + name.span() => let (#name, text) = parse::CoreParse::parse_many(scope, text, #lookahead)?; } } @@ -162,7 +162,7 @@ fn parse_variant_with_attr( } => { let lookahead = lookahead(name, next_op)?; quote_spanned! { - name.span() => let (#name, text) = parse::Parse::parse_comma(scope, text, #lookahead)?; + name.span() => let (#name, text) = parse::CoreParse::parse_comma(scope, text, #lookahead)?; } } @@ -242,7 +242,7 @@ fn parse_bindings(bindings: &[BindingInfo]) -> Vec { }; quote! { #parse_comma - let (#name, text) = parse::Parse::parse(scope, text)?; + let (#name, text) = parse::CoreParse::parse(scope, text)?; } }) .collect() diff --git a/crates/formality-macros/src/term.rs b/crates/formality-macros/src/term.rs index a3ca2036..a34609df 100644 --- a/crates/formality-macros/src/term.rs +++ b/crates/formality-macros/src/term.rs @@ -51,9 +51,9 @@ fn derive_term(mut s: synstructure::Structure) -> TokenStream { // s.add_bounds(synstructure::AddBounds::None); s.gen_impl(quote! { - use crate::derive_links::{Term}; + use formality_core::term::CoreTerm; - gen impl Term for @Self { + gen impl CoreTerm for @Self { } }) } diff --git a/crates/formality-macros/src/visit.rs b/crates/formality-macros/src/visit.rs index 8ce9dd61..c9569a90 100644 --- a/crates/formality-macros/src/visit.rs +++ b/crates/formality-macros/src/visit.rs @@ -7,18 +7,22 @@ pub(crate) fn derive_visit(mut s: synstructure::Structure) -> TokenStream { s.underscore_const(true); s.bind_with(|_| synstructure::BindStyle::Move); - let free_variables_body = s.each(|field| quote!(output.extend(Visit::free_variables(#field)))); + let free_variables_body = s.each( + |field| quote!(output.extend(<_ as CoreVisit>::free_variables(#field))), + ); - let size_body = s.each(|field| quote!(__sum += Visit::size(#field))); + let size_body = + s.each(|field| quote!(__sum += <_ as CoreVisit>::size(#field))); - let assert_valid_body = s.each(|field| quote!(Visit::assert_valid(#field))); + let assert_valid_body = + s.each(|field| quote!(<_ as CoreVisit>::assert_valid(#field))); // s.add_bounds(synstructure::AddBounds::None); s.gen_impl(quote! { - use crate::derive_links::{Visit, Variable}; + use formality_core::{visit::CoreVisit, variable::CoreVariable}; - gen impl Visit for @Self { - fn free_variables(&self) -> Vec { + gen impl CoreVisit for @Self { + fn free_variables(&self) -> Vec> { let mut output = vec![]; match self { #free_variables_body diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index fe59c3eb..a64ba6c8 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -1,12 +1,8 @@ +use formality_core::{set, Set, Upcast}; use formality_macros::term; -use formality_types::{ - cast::Upcast, - collections::Set, - grammar::{ - AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, - Wc, Wcs, PR, - }, - set, +use formality_types::grammar::{ + AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, + Wcs, PR, }; #[term] diff --git a/crates/formality-prove/src/lib.rs b/crates/formality-prove/src/lib.rs index 88431404..f41ef19b 100644 --- a/crates/formality-prove/src/lib.rs +++ b/crates/formality-prove/src/lib.rs @@ -1,4 +1,5 @@ -use formality_types::derive_links; +// Defines the language used by derive(term) and friends. +use formality_types::rust::FormalityLang; mod db; mod decls; diff --git a/crates/formality-prove/src/prove.rs b/crates/formality-prove/src/prove.rs index ed9e7a04..6862db34 100644 --- a/crates/formality-prove/src/prove.rs +++ b/crates/formality-prove/src/prove.rs @@ -1,3 +1,4 @@ +mod combinators; mod constraints; mod env; mod is_local; @@ -9,10 +10,11 @@ mod prove_via; mod prove_wc; mod prove_wc_list; mod prove_wf; -mod combinators; pub use constraints::Constraints; -use formality_types::{cast::Upcast, collections::Set, grammar::Wcs, set, visit::Visit}; +use formality_core::visit::CoreVisit; +use formality_core::{set, Set, Upcast}; +use formality_types::grammar::Wcs; use tracing::Level; use crate::decls::Decls; diff --git a/crates/formality-prove/src/prove/combinators.rs b/crates/formality-prove/src/prove/combinators.rs index 54583e46..76640c9a 100644 --- a/crates/formality-prove/src/prove/combinators.rs +++ b/crates/formality-prove/src/prove/combinators.rs @@ -1,6 +1,6 @@ -use formality_types::{cast::Upcast, collections::Set, set, term::Term}; - use crate::decls::Decls; +use formality_core::{set, Set, Upcast}; +use formality_types::rust::Term; use super::{Constraints, Env}; diff --git a/crates/formality-prove/src/prove/constraints.rs b/crates/formality-prove/src/prove/constraints.rs index ba85296c..726b5a20 100644 --- a/crates/formality-prove/src/prove/constraints.rs +++ b/crates/formality-prove/src/prove/constraints.rs @@ -1,13 +1,10 @@ +use super::env::Env; +use formality_core::{cast_impl, visit::CoreVisit, Downcast, Upcast, UpcastFrom}; use formality_types::{ - cast::{Downcast, Upcast}, - cast_impl, - derive_links::UpcastFrom, grammar::{ExistentialVar, Parameter, Substitution, Variable}, - visit::Visit, + rust::Visit, }; -use super::env::Env; - #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug, Hash)] pub struct Constraints { pub env: Env, @@ -133,7 +130,7 @@ impl Constraints { } } -impl Visit for Constraints { +impl CoreVisit for Constraints { fn free_variables(&self) -> Vec { let Constraints { env, diff --git a/crates/formality-prove/src/prove/env.rs b/crates/formality-prove/src/prove/env.rs index cb986b4b..aaacc541 100644 --- a/crates/formality-prove/src/prove/env.rs +++ b/crates/formality-prove/src/prove/env.rs @@ -1,13 +1,10 @@ +use formality_core::{cast_impl, visit::CoreVisit, Set, To, Upcast}; use formality_macros::term; use formality_types::{ - cast::{To, Upcast}, - cast_impl, - collections::Set, - fold::Fold, grammar::{ Binder, ExistentialVar, ParameterKind, UniversalVar, VarIndex, VarSubstitution, Variable, }, - visit::Visit, + rust::{Fold, Visit}, }; #[derive(Default, Debug, Clone, Hash, Ord, Eq, PartialEq, PartialOrd)] @@ -220,7 +217,7 @@ impl Env { } } -impl Visit for Env { +impl CoreVisit for Env { fn free_variables(&self) -> Vec { self.variables.clone() } diff --git a/crates/formality-prove/src/prove/is_local.rs b/crates/formality-prove/src/prove/is_local.rs index 8876081a..9e4202e5 100644 --- a/crates/formality-prove/src/prove/is_local.rs +++ b/crates/formality-prove/src/prove/is_local.rs @@ -1,7 +1,6 @@ -use formality_types::{ - collections::Set, - grammar::{Lt, Parameter, RigidName, RigidTy, TraitRef, TyData, Variable, Wcs}, - judgment_fn, set, +use formality_core::{judgment_fn, set, Set}; +use formality_types::grammar::{ + Lt, Parameter, RigidName, RigidTy, TraitRef, TyData, Variable, Wcs, }; use crate::{ diff --git a/crates/formality-prove/src/prove/minimize.rs b/crates/formality-prove/src/prove/minimize.rs index be496bf6..605edb2b 100644 --- a/crates/formality-prove/src/prove/minimize.rs +++ b/crates/formality-prove/src/prove/minimize.rs @@ -1,10 +1,9 @@ +use formality_core::{Deduplicate, Downcast, Upcast}; use formality_types::{ - cast::{Downcast, Upcast}, - collections::Deduplicate, grammar::{ ExistentialVar, Parameter, Substitution, UniversalVar, VarIndex, VarSubstitution, Variable, }, - term::Term, + rust::Term, }; use super::{Constraints, Env}; diff --git a/crates/formality-prove/src/prove/minimize/test.rs b/crates/formality-prove/src/prove/minimize/test.rs index 1531c3c1..f8acdf00 100644 --- a/crates/formality-prove/src/prove/minimize/test.rs +++ b/crates/formality-prove/src/prove/minimize/test.rs @@ -1,9 +1,9 @@ use expect_test::expect; +use formality_core::To; use formality_macros::test; use formality_types::{ - cast::To, grammar::{Binder, Parameter, ScalarId, Ty}, - parse::term, + rust::term, }; use crate::prove::{Constraints, Env}; diff --git a/crates/formality-prove/src/prove/prove_after.rs b/crates/formality-prove/src/prove/prove_after.rs index 7f3b5c65..3bdbe16b 100644 --- a/crates/formality-prove/src/prove/prove_after.rs +++ b/crates/formality-prove/src/prove/prove_after.rs @@ -1,4 +1,5 @@ -use formality_types::{grammar::Wcs, judgment_fn}; +use formality_core::judgment_fn; +use formality_types::grammar::Wcs; use crate::{decls::Decls, prove::prove}; diff --git a/crates/formality-prove/src/prove/prove_eq.rs b/crates/formality-prove/src/prove/prove_eq.rs index 5f27238f..cf35477c 100644 --- a/crates/formality-prove/src/prove/prove_eq.rs +++ b/crates/formality-prove/src/prove/prove_eq.rs @@ -1,12 +1,9 @@ -use formality_types::{ - cast::{Downcast, Upcast, Upcasted}, - collections::{Deduplicate, Set}, - grammar::{ - AliasTy, ExistentialVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar, - Variable, Wcs, - }, - judgment_fn, set, - visit::Visit, +use formality_core::visit::CoreVisit; +use formality_core::{judgment_fn, set, Downcast, Set, Upcast}; +use formality_core::{Deduplicate, Upcasted}; +use formality_types::grammar::{ + AliasTy, ExistentialVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar, + Variable, Wcs, }; use crate::{ diff --git a/crates/formality-prove/src/prove/prove_normalize.rs b/crates/formality-prove/src/prove/prove_normalize.rs index 49435692..b12a92c5 100644 --- a/crates/formality-prove/src/prove/prove_normalize.rs +++ b/crates/formality-prove/src/prove/prove_normalize.rs @@ -1,9 +1,6 @@ -use formality_types::{ - cast::Downcast, - grammar::{ - AliasTy, ExistentialVar, Parameter, Relation, RigidTy, TyData, Variable, Wc, WcData, Wcs, - }, - judgment_fn, +use formality_core::{judgment_fn, Downcast}; +use formality_types::grammar::{ + AliasTy, ExistentialVar, Parameter, Relation, RigidTy, TyData, Variable, Wc, WcData, Wcs, }; use crate::{ diff --git a/crates/formality-prove/src/prove/prove_via.rs b/crates/formality-prove/src/prove/prove_via.rs index 666a68cc..32b51045 100644 --- a/crates/formality-prove/src/prove/prove_via.rs +++ b/crates/formality-prove/src/prove/prove_via.rs @@ -1,13 +1,9 @@ -use formality_types::{ - grammar::{WcData, Wcs, PR}, - judgment_fn, -}; +use formality_core::judgment_fn; +use formality_types::grammar::{WcData, Wcs, PR}; use crate::{ decls::Decls, - prove::{ - constraints::Constraints, env::Env, prove, prove_after::prove_after, - }, + prove::{constraints::Constraints, env::Env, prove, prove_after::prove_after}, }; judgment_fn! { diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 70e06632..9c75dd2c 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -1,7 +1,5 @@ -use formality_types::{ - grammar::{Predicate, Relation, Wc, WcData, Wcs}, - judgment_fn, -}; +use formality_core::judgment_fn; +use formality_types::grammar::{Predicate, Relation, Wc, WcData, Wcs}; use crate::{ decls::Decls, diff --git a/crates/formality-prove/src/prove/prove_wc_list.rs b/crates/formality-prove/src/prove/prove_wc_list.rs index f8ca5401..1b2213a0 100644 --- a/crates/formality-prove/src/prove/prove_wc_list.rs +++ b/crates/formality-prove/src/prove/prove_wc_list.rs @@ -1,4 +1,5 @@ -use formality_types::{grammar::Wcs, judgment_fn}; +use formality_core::judgment_fn; +use formality_types::grammar::Wcs; use crate::{ decls::Decls, diff --git a/crates/formality-prove/src/prove/prove_wf.rs b/crates/formality-prove/src/prove/prove_wf.rs index 635167f1..4b700be7 100644 --- a/crates/formality-prove/src/prove/prove_wf.rs +++ b/crates/formality-prove/src/prove/prove_wf.rs @@ -1,6 +1,6 @@ -use formality_types::{ - grammar::{ConstData, Parameter, RigidName, RigidTy, UniversalVar, Wcs, AliasTy, Parameters, AliasName}, - judgment_fn, collections::Set, +use formality_core::{judgment_fn, Set}; +use formality_types::grammar::{ + AliasName, AliasTy, ConstData, Parameter, Parameters, RigidName, RigidTy, UniversalVar, Wcs, }; use crate::{decls::Decls, prove::combinators::for_all}; diff --git a/crates/formality-prove/src/test/eq_assumptions.rs b/crates/formality-prove/src/test/eq_assumptions.rs index ac443b11..87bd887e 100644 --- a/crates/formality-prove/src/test/eq_assumptions.rs +++ b/crates/formality-prove/src/test/eq_assumptions.rs @@ -1,6 +1,6 @@ use expect_test::expect; use formality_macros::test; -use formality_types::parse::term; +use formality_types::rust::term; use crate::decls::Decls; diff --git a/crates/formality-prove/src/test/eq_partial_eq.rs b/crates/formality-prove/src/test/eq_partial_eq.rs index bdfff075..a51360e7 100644 --- a/crates/formality-prove/src/test/eq_partial_eq.rs +++ b/crates/formality-prove/src/test/eq_partial_eq.rs @@ -2,7 +2,7 @@ use expect_test::expect; use formality_macros::test; use formality_types::{ grammar::{Wc, Wcs}, - parse::term, + rust::term, }; use crate::{decls::Decls, prove::prove}; diff --git a/crates/formality-prove/src/test/exists_constraints.rs b/crates/formality-prove/src/test/exists_constraints.rs index 9b5ba9ac..34ccb5b9 100644 --- a/crates/formality-prove/src/test/exists_constraints.rs +++ b/crates/formality-prove/src/test/exists_constraints.rs @@ -1,6 +1,6 @@ use expect_test::expect; use formality_macros::test; -use formality_types::parse::term; +use formality_types::rust::term; use crate::decls::Decls; diff --git a/crates/formality-prove/src/test/expanding.rs b/crates/formality-prove/src/test/expanding.rs index 06c931c0..ac654021 100644 --- a/crates/formality-prove/src/test/expanding.rs +++ b/crates/formality-prove/src/test/expanding.rs @@ -1,6 +1,6 @@ use expect_test::expect; use formality_macros::test; -use formality_types::parse::term; +use formality_types::rust::term; use crate::{test_util::test_prove, Decls}; diff --git a/crates/formality-prove/src/test/is_local.rs b/crates/formality-prove/src/test/is_local.rs index 7319c5a0..3031f30a 100644 --- a/crates/formality-prove/src/test/is_local.rs +++ b/crates/formality-prove/src/test/is_local.rs @@ -1,6 +1,6 @@ use expect_test::expect; use formality_macros::test; -use formality_types::parse::term; +use formality_types::rust::term; use crate::decls::Decls; diff --git a/crates/formality-prove/src/test/magic_copy.rs b/crates/formality-prove/src/test/magic_copy.rs index a3327cbb..04ded95b 100644 --- a/crates/formality-prove/src/test/magic_copy.rs +++ b/crates/formality-prove/src/test/magic_copy.rs @@ -1,6 +1,6 @@ use expect_test::expect; use formality_macros::test; -use formality_types::parse::term; +use formality_types::rust::term; use crate::decls::Decls; diff --git a/crates/formality-prove/src/test/occurs_check.rs b/crates/formality-prove/src/test/occurs_check.rs index 8bd3dcae..874d9d51 100644 --- a/crates/formality-prove/src/test/occurs_check.rs +++ b/crates/formality-prove/src/test/occurs_check.rs @@ -1,6 +1,6 @@ use expect_test::expect; use formality_macros::test; -use formality_types::parse::term; +use formality_types::rust::term; use crate::decls::Decls; diff --git a/crates/formality-prove/src/test/simple_impl.rs b/crates/formality-prove/src/test/simple_impl.rs index 591c7347..ded1a560 100644 --- a/crates/formality-prove/src/test/simple_impl.rs +++ b/crates/formality-prove/src/test/simple_impl.rs @@ -1,6 +1,7 @@ use expect_test::expect; use formality_macros::test; -use formality_types::{grammar::Wc, parse::term}; +use formality_types::grammar::Wc; +use formality_types::rust::term; use crate::{decls::Decls, prove::prove}; diff --git a/crates/formality-prove/src/test/universes.rs b/crates/formality-prove/src/test/universes.rs index de0f9ab9..5cd6d1d7 100644 --- a/crates/formality-prove/src/test/universes.rs +++ b/crates/formality-prove/src/test/universes.rs @@ -1,6 +1,6 @@ use expect_test::expect; use formality_macros::test; -use formality_types::parse::term; +use formality_types::rust::term; use crate::decls::Decls; diff --git a/crates/formality-prove/src/test_util.rs b/crates/formality-prove/src/test_util.rs index b4e90afe..a750ff8f 100644 --- a/crates/formality-prove/src/test_util.rs +++ b/crates/formality-prove/src/test_util.rs @@ -1,10 +1,8 @@ use std::sync::Arc; +use formality_core::Set; use formality_macros::term; -use formality_types::{ - collections::Set, - grammar::{Binder, Wcs}, -}; +use formality_types::grammar::{Binder, Wcs}; use crate::{ decls::Decls, diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 33da1b4b..424a3790 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -1,13 +1,12 @@ use std::sync::Arc; -use formality_macros::term; +use formality_core::{term, Upcast}; use formality_types::{ - cast::Upcast, grammar::{ - AdtId, AssociatedItemId, Binder, Const, CrateId, Fallible, FieldId, FnId, Lt, Parameter, - TraitId, TraitRef, Ty, Wc, AliasTy, + AdtId, AliasTy, AssociatedItemId, Binder, Const, CrateId, Fallible, FieldId, FnId, Lt, + Parameter, TraitId, TraitRef, Ty, Wc, }, - term::Term, + rust::Term, }; use crate::grammar::mir::MirFnBody; @@ -117,7 +116,7 @@ pub enum FieldName { Index(usize), } -formality_types::id!(VariantId); +formality_core::id!(VariantId); impl VariantId { /// Returns the special variant-id used for the single variant of a struct. diff --git a/crates/formality-rust/src/grammar/mir.rs b/crates/formality-rust/src/grammar/mir.rs index 5b6bce83..946673ed 100644 --- a/crates/formality-rust/src/grammar/mir.rs +++ b/crates/formality-rust/src/grammar/mir.rs @@ -1,9 +1,7 @@ use super::VariantId; +use formality_core::{Downcast, DowncastFrom, Upcast}; use formality_macros::term; -use formality_types::{ - cast::{Downcast, DowncastFrom, Upcast}, - grammar::{AdtId, Binder, FieldId, FnId, Lt, Parameter, RefKind, Ty}, -}; +use formality_types::grammar::{AdtId, Binder, FieldId, FnId, Lt, Parameter, RefKind, Ty}; #[term(mir($binder))] pub struct MirFnBody { @@ -25,8 +23,8 @@ pub struct LocalDecl { pub mutability: RefKind, } -formality_types::id!(LocalId); -formality_types::id!(BasicBlockId); +formality_core::id!(LocalId); +formality_core::id!(BasicBlockId); #[term] pub struct BasicBlockDecl { diff --git a/crates/formality-rust/src/lib.rs b/crates/formality-rust/src/lib.rs index 3b583e08..e56d3c4f 100644 --- a/crates/formality-rust/src/lib.rs +++ b/crates/formality-rust/src/lib.rs @@ -1,4 +1,7 @@ -use formality_types::derive_links; +// ANCHOR: use_rust_language +// Defines the language used by derive(term) and friends. +use formality_types::rust::FormalityLang; +// ANCHOR_END: use_rust_language pub mod grammar; pub mod prove; diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index 04c271fb..89a548e7 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -4,15 +4,13 @@ use crate::grammar::{ TraitImpl, TraitImplBoundData, TraitItem, WhereBound, WhereBoundData, WhereClause, WhereClauseData, }; +use formality_core::{seq, Set, To, Upcast, Upcasted}; use formality_prove as prove; use formality_types::{ - cast::{To, Upcast, Upcasted}, - collections::Set, grammar::{ - fresh_bound_var, AdtId, AliasTy, Binder, ParameterKind, Predicate, Relation, TraitId, Ty, - Wc, Wcs, PR, + AdtId, AliasTy, Binder, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, Wcs, PR, }, - seq, + rust::BoundVar, }; impl Program { @@ -258,7 +256,7 @@ impl Crate { ensures .iter() .map(|e| { - let fresh_var = fresh_bound_var(ParameterKind::Ty); + let fresh_var = BoundVar::fresh(ParameterKind::Ty); let ensures = Binder::new(vec![fresh_var], e.to_wc(fresh_var)); prove::AliasBoundDecl { diff --git a/crates/formality-rust/src/trait_binder.rs b/crates/formality-rust/src/trait_binder.rs index 9d901ad8..9845390d 100644 --- a/crates/formality-rust/src/trait_binder.rs +++ b/crates/formality-rust/src/trait_binder.rs @@ -1,16 +1,18 @@ use std::fmt::Debug; +use formality_core::{ + fold::CoreFold, + parse::{expect_char, Binding, CoreParse, ParseResult, Scope}, + term::CoreTerm, + visit::CoreVisit, + DowncastTo, To, UpcastFrom, +}; use formality_types::{ - cast::To, - derive_links::{DowncastTo, UpcastFrom}, - fold::Fold, - grammar::{fresh_bound_var, Binder, BoundVar, ParameterKind}, - parse::{expect_char, Binding, Parse, ParseResult}, - term::Term, - visit::Visit, + grammar::{Binder, BoundVar, ParameterKind}, + rust::Term, }; -use crate::grammar::TraitBinder; +use crate::{grammar::TraitBinder, FormalityLang}; impl TraitBinder where @@ -21,7 +23,7 @@ where } } -impl Term for TraitBinder where T: Term {} +impl CoreTerm for TraitBinder where T: Term {} impl DowncastTo> for TraitBinder where @@ -41,7 +43,7 @@ where } } -impl Visit for TraitBinder +impl CoreVisit for TraitBinder where T: Term, { @@ -58,11 +60,14 @@ where } } -impl Fold for TraitBinder +impl CoreFold for TraitBinder where T: Term, { - fn substitute(&self, substitution_fn: formality_types::fold::SubstitutionFn<'_>) -> Self { + fn substitute( + &self, + substitution_fn: formality_core::fold::SubstitutionFn<'_, FormalityLang>, + ) -> Self { TraitBinder { explicit_binder: self.explicit_binder.substitute(substitution_fn), } @@ -78,19 +83,19 @@ where } } -impl Parse for TraitBinder +impl CoreParse for TraitBinder where T: Term, { #[tracing::instrument(level = "trace", ret)] - fn parse<'t>(scope: &formality_types::parse::Scope, text: &'t str) -> ParseResult<'t, Self> { + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { // parse the explicit bindings written by the user let ((), text) = expect_char('<', text)?; let (mut bindings, text) = Binding::parse_comma(scope, text, '>')?; let ((), text) = expect_char('>', text)?; // insert the `Self` binding at position 0 - let bound_var = fresh_bound_var(ParameterKind::Ty); + let bound_var = BoundVar::fresh(ParameterKind::Ty); bindings.insert( 0, Binding { diff --git a/crates/formality-smir/src/lib.rs b/crates/formality-smir/src/lib.rs index 17e928e8..9decaf59 100644 --- a/crates/formality-smir/src/lib.rs +++ b/crates/formality-smir/src/lib.rs @@ -1,5 +1,7 @@ #![feature(rustc_private)] +use formality_types::grammar::ParameterKind; + /// This import is needed, because `stable_mir` on its own doesn't have the `scoped_tls` rlib. extern crate rustc_driver; /// Access to the pre-0.1 stable_mir crate @@ -14,11 +16,9 @@ pub trait ToFormality { } impl ToFormality for stable_mir::ty::GenericParamDefKind { - type T = formality_types::derive_links::ParameterKind; + type T = ParameterKind; fn formality(&self) -> Self::T { - use formality_types::derive_links::ParameterKind; - match self { stable_mir::ty::GenericParamDefKind::Lifetime => ParameterKind::Lt, stable_mir::ty::GenericParamDefKind::Type { .. } => ParameterKind::Ty, diff --git a/crates/formality-types/Cargo.toml b/crates/formality-types/Cargo.toml index afc10fc9..898bc5e9 100644 --- a/crates/formality-types/Cargo.toml +++ b/crates/formality-types/Cargo.toml @@ -9,7 +9,6 @@ edition = "2021" anyhow = "1.0.65" lazy_static = "1.4.0" formality-core = { path = "../formality-core" } -formality-macros = { path = "../formality-macros" } tracing = "0.1" contracts = "0.6.3" stacker = "0.1.15" diff --git a/crates/formality-types/src/fold.rs b/crates/formality-types/src/fold.rs deleted file mode 100644 index 07858872..00000000 --- a/crates/formality-types/src/fold.rs +++ /dev/null @@ -1,143 +0,0 @@ -use std::sync::Arc; - -use crate::{ - cast::Upcast, - collections::Set, - grammar::{Const, ConstData, Lt, LtData, Parameter, Ty, TyData, ValTree, Variable}, - visit::Visit, -}; - -/// Invoked for each variable that we find when folding, ignoring variables bound by binders -/// that we traverse. The arguments are as follows: -/// -/// * ParameterKind -- the kind of term in which the variable appeared (type vs lifetime, etc) -/// * Variable -- the variable we encountered -pub type SubstitutionFn<'a> = &'a mut dyn FnMut(Variable) -> Option; - -pub trait Fold: Sized + Visit { - /// Replace uses of variables with values from the substitution. - fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self; - - /// Produce a version of this term where any debruijn indices which appear free are incremented by one. - fn shift_in(&self) -> Self { - self.substitute(&mut |v| Some(v.shift_in().upcast())) - } - - /// Replace all appearances of free variable `v` with `p`. - fn replace_free_var(&self, v: impl Upcast, p: impl Upcast) -> Self { - let v: Variable = v.upcast(); - let p: Parameter = p.upcast(); - assert!(v.is_free()); - assert!(v.kind() == p.kind()); - self.substitute(&mut |v1| if v == v1 { Some(p.clone()) } else { None }) - } -} - -impl Fold for Vec { - fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self { - self.iter().map(|e| e.substitute(substitution_fn)).collect() - } -} - -impl Fold for Set { - fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self { - self.iter().map(|e| e.substitute(substitution_fn)).collect() - } -} - -impl Fold for Option { - fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self { - self.as_ref().map(|e| e.substitute(substitution_fn)) - } -} - -impl Fold for Arc { - fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self { - let data = T::substitute(self, substitution_fn); - Arc::new(data) - } -} - -impl Fold for Ty { - fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self { - match self.data() { - TyData::RigidTy(v) => v.substitute(substitution_fn).upcast(), - TyData::AliasTy(v) => v.substitute(substitution_fn).upcast(), - TyData::PredicateTy(v) => v.substitute(substitution_fn).upcast(), - TyData::Variable(v) => match substitution_fn(*v) { - None => self.clone(), - Some(Parameter::Ty(t)) => t, - Some(param) => panic!("ill-kinded substitute: expected type, got {param:?}"), - }, - } - } -} - -impl Fold for Const { - fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self { - match self.data() { - ConstData::Value(v, ty) => Self::valtree( - v.substitute(substitution_fn), - ty.substitute(substitution_fn), - ), - ConstData::Variable(v) => match substitution_fn(*v) { - None => self.clone(), - Some(Parameter::Const(c)) => c, - Some(param) => panic!("ill-kinded substitute: expected const, got {param:?}"), - }, - } - } -} - -impl Fold for ValTree { - fn substitute(&self, _substitution_fn: SubstitutionFn<'_>) -> Self { - self.clone() - } -} - -impl Fold for Lt { - fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self { - match self.data() { - LtData::Static => self.clone(), - LtData::Variable(v) => match substitution_fn(*v) { - None => self.clone(), - Some(Parameter::Lt(t)) => t, - Some(param) => panic!("ill-kinded substitute: expected lifetime, got {param:?}"), - }, - } - } -} - -impl Fold for usize { - fn substitute(&self, _substitution_fn: SubstitutionFn<'_>) -> Self { - *self - } -} - -impl Fold for u32 { - fn substitute(&self, _substitution_fn: SubstitutionFn<'_>) -> Self { - *self - } -} - -impl Fold for () { - fn substitute(&self, _substitution_fn: SubstitutionFn<'_>) -> Self {} -} - -impl Fold for (A, B) { - fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self { - let (a, b) = self; - (a.substitute(substitution_fn), b.substitute(substitution_fn)) - } -} - -impl Fold for (A, B, C) { - fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self { - let (a, b, c) = self; - ( - a.substitute(substitution_fn), - b.substitute(substitution_fn), - c.substitute(substitution_fn), - ) - } -} diff --git a/crates/formality-types/src/grammar.rs b/crates/formality-types/src/grammar.rs index 22d60aad..285576f6 100644 --- a/crates/formality-types/src/grammar.rs +++ b/crates/formality-types/src/grammar.rs @@ -1,4 +1,3 @@ -mod binder; mod consts; mod formulas; mod ids; @@ -6,7 +5,10 @@ mod kinded; mod ty; mod wc; -pub use binder::*; +pub use crate::rust::{ + Binder, BoundVar, DebruijnIndex, ExistentialVar, Substitution, UniversalVar, VarIndex, + VarSubstitution, Variable, +}; pub use consts::*; pub use formulas::*; pub use ids::*; diff --git a/crates/formality-types/src/grammar/consts.rs b/crates/formality-types/src/grammar/consts.rs index 28922e4e..980c2058 100644 --- a/crates/formality-types/src/grammar/consts.rs +++ b/crates/formality-types/src/grammar/consts.rs @@ -1,9 +1,7 @@ mod valtree; -use crate::cast::{DowncastTo, Upcast, UpcastFrom}; - use super::{Parameter, Ty, Variable}; -use formality_macros::{term, Visit}; +use formality_core::{term, DowncastTo, Upcast, UpcastFrom, Visit}; use std::sync::Arc; pub use valtree::*; diff --git a/crates/formality-types/src/grammar/consts/valtree.rs b/crates/formality-types/src/grammar/consts/valtree.rs index 694c1b89..d40da934 100644 --- a/crates/formality-types/src/grammar/consts/valtree.rs +++ b/crates/formality-types/src/grammar/consts/valtree.rs @@ -1,6 +1,6 @@ -use formality_macros::Visit; +use formality_core::Visit; -use crate::cast::{Upcast, UpcastFrom}; +use formality_core::{Upcast, UpcastFrom}; use super::Bool; diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index 220e2c0f..51adc299 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -1,8 +1,8 @@ -use formality_macros::term; +use formality_core::term; -use crate::cast::To; -use crate::cast::Upcast; -use crate::cast_impl; +use formality_core::cast_impl; +use formality_core::To; +use formality_core::Upcast; use super::AliasName; use super::AliasTy; @@ -119,11 +119,7 @@ impl Predicate { Predicate::AliasEq(AliasTy { name, parameters }, ty) => { let mut params = parameters.clone(); params.push(ty.clone().upcast()); - ( - Skeleton::AliasEq(name.clone()), - params, - ) - + (Skeleton::AliasEq(name.clone()), params) } Predicate::WellFormedTraitRef(TraitRef { trait_id, diff --git a/crates/formality-types/src/grammar/ids.rs b/crates/formality-types/src/grammar/ids.rs index f2a142fe..b76a5b4c 100644 --- a/crates/formality-types/src/grammar/ids.rs +++ b/crates/formality-types/src/grammar/ids.rs @@ -1,69 +1,4 @@ -#[macro_export] -macro_rules! id { - ($n:ident) => { - #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] - pub struct $n { - data: std::sync::Arc, - } - - const _: () = { - use $crate::fold::{self, Fold}; - use $crate::grammar::Variable; - use $crate::parse::{self, Parse}; - use $crate::visit::Visit; - - $crate::cast_impl!($n); - - impl $n { - pub fn new(s: &str) -> $n { - $n { - data: std::sync::Arc::new(s.to_string()), - } - } - } - - impl std::ops::Deref for $n { - type Target = String; - - fn deref(&self) -> &String { - &self.data - } - } - - impl Visit for $n { - fn free_variables(&self) -> Vec { - vec![] - } - - fn size(&self) -> usize { - 1 - } - - fn assert_valid(&self) {} - } - - impl Fold for $n { - fn substitute(&self, _substitution_fn: fold::SubstitutionFn<'_>) -> Self { - self.clone() - } - } - - impl Parse for $n { - fn parse<'t>(_scope: &parse::Scope, text: &'t str) -> parse::ParseResult<'t, Self> { - let (string, text) = parse::identifier(text)?; - let n = $n::new(&string); - Ok((n, text)) - } - } - - impl std::fmt::Debug for $n { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "{}", &self.data) - } - } - }; - }; -} +use formality_core::id; id!(FnId); id!(AdtId); diff --git a/crates/formality-types/src/grammar/kinded.rs b/crates/formality-types/src/grammar/kinded.rs index 4bbe6856..a5f77f65 100644 --- a/crates/formality-types/src/grammar/kinded.rs +++ b/crates/formality-types/src/grammar/kinded.rs @@ -1,6 +1,6 @@ -use crate::cast::Upcast; +use formality_core::Upcast; -use super::{fresh_bound_var, BoundVar, Lt, ParameterKind, Ty}; +use super::{BoundVar, Lt, LtData, ParameterKind, Ty, TyData}; /// Trait implemented by the various kinds of generic parameters. /// Used in some of the fluent APIs for creating binders to select @@ -11,15 +11,15 @@ pub trait Kinded { impl Kinded for Ty { fn instantiate() -> (Vec, Self) { - let bvar = fresh_bound_var(ParameterKind::Ty); - (vec![bvar], bvar.ty()) + let bvar = BoundVar::fresh(ParameterKind::Ty); + (vec![bvar], TyData::Variable(bvar.upcast()).upcast()) } } impl Kinded for Lt { fn instantiate() -> (Vec, Self) { - let bvar = fresh_bound_var(ParameterKind::Lt); - (vec![bvar], bvar.lt()) + let bvar = BoundVar::fresh(ParameterKind::Lt); + (vec![bvar], LtData::Variable(bvar.upcast()).upcast()) } } diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs index 0446e8cf..b96785b3 100644 --- a/crates/formality-types/src/grammar/ty.rs +++ b/crates/formality-types/src/grammar/ty.rs @@ -1,20 +1,16 @@ -use contracts::requires; -use formality_macros::{term, Visit}; -use std::{collections::BTreeSet, sync::Arc}; +use formality_core::{cast_impl, term, Visit}; +use std::sync::Arc; mod debug_impls; mod parse_impls; +mod term_impls; +use crate::rust::{BoundVar, Variable}; +use formality_core::{DowncastTo, To, Upcast, UpcastFrom}; -use crate::{ - cast::{DowncastTo, To, Upcast, UpcastFrom}, - cast_impl, - collections::Map, - derive_links::Visit, - fold::Fold, +use super::{ + consts::Const, AdtId, AssociatedItemId, Binder, ExistentialVar, FnId, TraitId, UniversalVar, }; -use super::{consts::Const, AdtId, AssociatedItemId, Binder, FnId, TraitId}; - #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct Ty { data: Arc, @@ -121,26 +117,6 @@ impl UpcastFrom for TyData { } } -#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct ExistentialVar { - pub kind: ParameterKind, - pub var_index: VarIndex, -} - -cast_impl!(ExistentialVar); - -impl Visit for ExistentialVar { - fn free_variables(&self) -> Vec { - vec![self.upcast()] - } - - fn size(&self) -> usize { - 1 - } - - fn assert_valid(&self) {} -} - #[term((rigid $name $*parameters))] pub struct RigidTy { pub name: RigidName, @@ -250,21 +226,6 @@ pub enum PredicateTy { ForAll(Binder), } -/// A *universal variable* is a dummy variable about which nothing is known except -/// that which we see in the environment. When we want to prove something -/// is true for all `T` (`∀T`), we replace `T` with a universal variable. -#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct UniversalVar { - pub kind: ParameterKind, - pub var_index: VarIndex, -} - -#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub enum QuantifierKind { - ForAll, - Exists, -} - #[term] pub enum Parameter { #[cast] @@ -376,143 +337,6 @@ impl UpcastFrom for LtData { } } -impl Visit for LtData { - fn free_variables(&self) -> Vec { - match self { - LtData::Variable(v) => { - if v.is_free() { - vec![*v] - } else { - vec![] - } - } - LtData::Static => vec![], - } - } - - fn size(&self) -> usize { - match self { - LtData::Variable(v) => v.size(), - LtData::Static => 1, - } - } - - fn assert_valid(&self) { - match self { - LtData::Variable(v) => v.assert_valid(), - LtData::Static => (), - } - } -} - -#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub enum Variable { - UniversalVar(UniversalVar), - ExistentialVar(ExistentialVar), - BoundVar(BoundVar), -} - -cast_impl!(Variable); - -impl Variable { - pub fn kind(&self) -> ParameterKind { - match self { - Variable::UniversalVar(v) => v.kind, - Variable::ExistentialVar(v) => v.kind, - Variable::BoundVar(v) => v.kind, - } - } - - /// Shift a variable in through `binders` binding levels. - /// Only affects bound variables. - pub fn shift_in(&self) -> Self { - if let Variable::BoundVar(BoundVar { - debruijn: Some(db), - var_index, - kind, - }) = self - { - BoundVar { - debruijn: Some(db.shift_in()), - var_index: *var_index, - kind: *kind, - } - .upcast() - } else { - *self - } - } - - /// Shift a variable out through `binders` binding levels. - /// Only affects bound variables. Returns None if the variable - /// is bound within those binding levels. - pub fn shift_out(&self) -> Option { - if let Variable::BoundVar(BoundVar { - debruijn: Some(db), - var_index, - kind, - }) = self - { - db.shift_out().map(|db1| { - BoundVar { - debruijn: Some(db1), - var_index: *var_index, - kind: *kind, - } - .upcast() - }) - } else { - Some(*self) - } - } - - /// A variable is *free* (i.e., not bound by any internal binder) - /// if it is an existential variable, a universal, or has a debruijn - /// index of `None`. The latter occurs when you `open` a binder (and before - /// you close it back up again). - pub fn is_free(&self) -> bool { - match self { - Variable::UniversalVar(_) - | Variable::ExistentialVar(_) - | Variable::BoundVar(BoundVar { - debruijn: None, - var_index: _, - kind: _, - }) => true, - - Variable::BoundVar(BoundVar { - debruijn: Some(_), - var_index: _, - kind: _, - }) => false, - } - } - - pub fn is_universal(&self) -> bool { - match self { - Variable::UniversalVar(_) => true, - Variable::ExistentialVar(_) => false, - Variable::BoundVar(_) => false, - } - } -} - -impl Visit for Variable { - fn free_variables(&self) -> Vec { - if self.is_free() { - vec![*self] - } else { - vec![] - } - } - - fn size(&self) -> usize { - 1 - } - - fn assert_valid(&self) {} -} - impl UpcastFrom for Parameter { fn upcast_from(v: Variable) -> Parameter { match v.kind() { @@ -529,288 +353,6 @@ impl DowncastTo for Parameter { } } -cast_impl!(BoundVar); -cast_impl!((ExistentialVar) <: (Variable) <: (Parameter)); -cast_impl!((BoundVar) <: (Variable) <: (Parameter)); -cast_impl!((UniversalVar) <: (Variable) <: (Parameter)); - -/// Identifies a bound variable. -#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct BoundVar { - /// Identifies the binder that contained this variable, counting "outwards". - /// When you create a binder with `Binder::new`, - /// When you open a Binder, you get back `Bound - pub debruijn: Option, - pub var_index: VarIndex, - pub kind: ParameterKind, -} - -impl BoundVar { - /// Packages up this bound variable as a type. - /// Only appropriate to call this if the variable - /// does indeed represent a type. - #[requires(self.kind == ParameterKind::Ty)] - pub fn ty(self) -> Ty { - Ty::new(TyData::Variable(Variable::upcast_from(self))) - } - - /// Packages up this bound variable as a lifetime. - /// Only appropriate to call this if the variable - /// does indeed represent a lifetime. - #[requires(self.kind == ParameterKind::Lt)] - pub fn lt(self) -> Lt { - Lt::new(LtData::Variable(Variable::upcast_from(self))) - } -} - -#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct DebruijnIndex { - pub index: usize, -} - -impl DebruijnIndex { - pub const INNERMOST: DebruijnIndex = DebruijnIndex { index: 0 }; - - /// Adjust this debruijn index through a binder level. - pub fn shift_in(&self) -> Self { - DebruijnIndex { - index: self.index + 1, - } - } - - /// Adjust this debruijn index *outward* through a binder level, if possible. - pub fn shift_out(&self) -> Option { - if self.index > 0 { - Some(DebruijnIndex { - index: self.index - 1, - }) - } else { - None - } - } -} - -#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct VarIndex { - pub index: usize, -} - -impl VarIndex { - pub const ZERO: VarIndex = VarIndex { index: 0 }; -} - -impl std::ops::Add for VarIndex { - type Output = VarIndex; - - fn add(self, rhs: usize) -> Self::Output { - VarIndex { - index: self.index + rhs, - } - } -} - -#[derive(Clone, Default, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct Substitution { - map: Map, -} - -impl Substitution { - /// Returns the variables that will be substituted for a new value. - pub fn domain(&self) -> BTreeSet { - self.map.keys().cloned().collect() - } - - /// Returns the parameters that that will be substituted for a new value. - pub fn range(&self) -> BTreeSet { - self.map.values().cloned().collect() - } - - /// True if `v` is in this substitution's domain - pub fn maps(&self, v: Variable) -> bool { - self.map.contains_key(&v) - } - - pub fn iter(&self) -> impl Iterator + '_ { - self.map.iter().map(|(v, p)| (*v, p.clone())) - } - - /// An empty substitution is just the identity function. - pub fn is_empty(&self) -> bool { - self.map.is_empty() - } -} - -impl std::fmt::Debug for Substitution { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let mut f = f.debug_set(); - for (v, p) in self.iter() { - f.entry(&Entry { v, p }); - struct Entry { - v: Variable, - p: Parameter, - } - impl std::fmt::Debug for Entry { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "{:?} => {:?}", self.v, self.p) - } - } - } - f.finish() - } -} - -impl std::ops::SubAssign for Substitution -where - Vs: Upcast>, -{ - fn sub_assign(&mut self, rhs: Vs) { - let rhs: Vec = rhs.upcast(); - - for v in rhs { - self.map.remove(&v); - } - } -} - -impl IntoIterator for Substitution { - type Item = (Variable, Parameter); - - type IntoIter = std::collections::btree_map::IntoIter; - - fn into_iter(self) -> Self::IntoIter { - self.map.into_iter() - } -} - -impl Extend<(A, B)> for Substitution -where - A: Upcast, - B: Upcast, -{ - fn extend>(&mut self, iter: T) { - self.map - .extend(iter.into_iter().map(|(v, p)| (v.upcast(), p.upcast()))); - } -} - -impl FromIterator<(A, B)> for Substitution -where - A: Upcast, - B: Upcast, -{ - fn from_iter>(iter: T) -> Self { - let mut s = Substitution::default(); - s.extend(iter); - s - } -} - -impl UpcastFrom<(A, B)> for Substitution -where - A: Upcast, - B: Upcast, -{ - fn upcast_from(term: (A, B)) -> Self { - let term: (Variable, Parameter) = term.upcast(); - std::iter::once(term).collect() - } -} - -impl Substitution { - pub fn apply(&self, t: &T) -> T { - t.substitute(&mut |v| self.map.get(&v).cloned()) - } - - pub fn get(&self, v: Variable) -> Option { - self.map.get(&v).cloned() - } -} - -impl Fold for Substitution { - fn substitute(&self, substitution_fn: crate::fold::SubstitutionFn<'_>) -> Self { - self.iter() - .map(|(v, p)| (v, p.substitute(substitution_fn))) - .collect() - } -} - -impl Visit for Substitution { - fn free_variables(&self) -> Vec { - let mut v = self.range().free_variables(); - v.extend(self.domain()); - v - } - - fn size(&self) -> usize { - self.range().iter().map(|r| r.size()).sum() - } - - fn assert_valid(&self) { - self.range().assert_valid() - } -} - -impl std::ops::Index for Substitution { - type Output = Parameter; - - fn index(&self, index: Variable) -> &Self::Output { - &self.map[&index] - } -} - -/// A substitution that is only between variables. -/// These are reversible. -#[derive(Clone, Default, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] -pub struct VarSubstitution { - map: Map, -} - -impl Extend<(A, B)> for VarSubstitution -where - A: Upcast, - B: Upcast, -{ - fn extend>(&mut self, iter: T) { - self.map - .extend(iter.into_iter().map(|(v, p)| (v.upcast(), p.upcast()))); - } -} - -impl FromIterator<(A, B)> for VarSubstitution -where - A: Upcast, - B: Upcast, -{ - fn from_iter>(iter: T) -> Self { - let mut s = VarSubstitution::default(); - s.extend(iter); - s - } -} - -impl VarSubstitution { - pub fn reverse(&self) -> VarSubstitution { - self.map.iter().map(|(k, v)| (*v, *k)).collect() - } - - pub fn apply(&self, t: &T) -> T { - t.substitute(&mut |v| Some(self.map.get(&v)?.upcast())) - } - - pub fn map_var(&self, v: Variable) -> Option { - self.map.get(&v).copied() - } - - pub fn maps_var(&self, v: Variable) -> bool { - self.map.contains_key(&v) - } - - pub fn insert_mapping(&mut self, from: impl Upcast, to: impl Upcast) { - let x = self.map.insert(from.upcast(), to.upcast()); - assert!(x.is_none()); - } -} - cast_impl!(Ty); cast_impl!((RigidTy) <: (TyData) <: (Ty)); cast_impl!((AliasTy) <: (TyData) <: (Ty)); @@ -833,6 +375,9 @@ cast_impl!((ScalarId) <: (RigidTy) <: (TyData)); cast_impl!((UniversalVar) <: (Variable) <: (Ty)); cast_impl!((ExistentialVar) <: (Variable) <: (Ty)); cast_impl!((BoundVar) <: (Variable) <: (Ty)); +cast_impl!((UniversalVar) <: (Variable) <: (Parameter)); +cast_impl!((ExistentialVar) <: (Variable) <: (Parameter)); +cast_impl!((BoundVar) <: (Variable) <: (Parameter)); cast_impl!(Lt); cast_impl!(LtData::Variable(Variable)); cast_impl!((ExistentialVar) <: (Variable) <: (LtData)); @@ -841,6 +386,3 @@ cast_impl!((BoundVar) <: (Variable) <: (LtData)); cast_impl!((UniversalVar) <: (LtData) <: (Lt)); cast_impl!((ExistentialVar) <: (LtData) <: (Lt)); cast_impl!((BoundVar) <: (LtData) <: (Lt)); -cast_impl!(Variable::UniversalVar(UniversalVar)); -cast_impl!(Variable::ExistentialVar(ExistentialVar)); -cast_impl!(Variable::BoundVar(BoundVar)); diff --git a/crates/formality-types/src/grammar/ty/debug_impls.rs b/crates/formality-types/src/grammar/ty/debug_impls.rs index 8f1988cb..a266f024 100644 --- a/crates/formality-types/src/grammar/ty/debug_impls.rs +++ b/crates/formality-types/src/grammar/ty/debug_impls.rs @@ -28,56 +28,3 @@ impl std::fmt::Debug for super::Lt { } } } - -impl std::fmt::Debug for super::Variable { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - match self { - Self::UniversalVar(arg0) => write!(f, "{:?}", arg0), - Self::ExistentialVar(arg0) => write!(f, "{:?}", arg0), - Self::BoundVar(arg0) => write!(f, "{:?}", arg0), - } - } -} - -impl std::fmt::Debug for super::UniversalVar { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let super::UniversalVar { var_index, kind } = self; - write!(f, "!{:?}_{:?}", kind, var_index) - } -} - -impl std::fmt::Debug for super::ExistentialVar { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let super::ExistentialVar { var_index, kind } = self; - write!(f, "?{:?}_{:?}", kind, var_index) - } -} - -impl std::fmt::Debug for super::VarIndex { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "{}", self.index) - } -} - -impl std::fmt::Debug for super::BoundVar { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - match self { - super::BoundVar { - debruijn: None, - var_index, - kind, - } => write!(f, "^{:?}_{:?}", kind, var_index), - super::BoundVar { - debruijn: Some(db), - var_index, - kind, - } => write!(f, "^{:?}{:?}_{:?}", kind, db.index, var_index), - } - } -} - -impl std::fmt::Debug for super::DebruijnIndex { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - write!(f, "^{}", self.index) - } -} diff --git a/crates/formality-types/src/grammar/ty/parse_impls.rs b/crates/formality-types/src/grammar/ty/parse_impls.rs index f544b1e0..e77fc677 100644 --- a/crates/formality-types/src/grammar/ty/parse_impls.rs +++ b/crates/formality-types/src/grammar/ty/parse_impls.rs @@ -1,18 +1,22 @@ //! Handwritten parser impls. -use crate::{ - cast::Upcast, - grammar::{AdtId, AssociatedItemId, Bool, Const, RigidName, Scalar, TraitId}, - parse::{self, expect_char, expect_keyword, reject_keyword, Parse, ParseError, ParseResult}, - seq, +use formality_core::parse::{ + self, expect_char, expect_keyword, reject_keyword, CoreParse, ParseError, ParseResult, Scope, }; +use formality_core::seq; +use formality_core::Upcast; + +use crate::grammar::{AdtId, AssociatedItemId, Bool, Const, RigidName, Scalar, TraitId}; use super::{AliasTy, AssociatedTyName, Lt, LtData, Parameter, PredicateTy, RigidTy, ScalarId, Ty}; +use crate::rust::FormalityLang as Rust; + +// ANCHOR: ty_parse_impl // For types, we invest some effort into parsing them decently because it makes // writing tests so much more pleasant. -impl Parse for Ty { - fn parse<'t>(scope: &crate::parse::Scope, text0: &'t str) -> ParseResult<'t, Self> { +impl CoreParse for Ty { + fn parse<'t>(scope: &Scope, text0: &'t str) -> ParseResult<'t, Self> { // Support writing `u8` etc and treat them as keywords if let Ok((scalar_ty, text1)) = ScalarId::parse(scope, text0) { return Ok((scalar_ty.upcast(), text1)); @@ -54,9 +58,10 @@ impl Parse for Ty { ) } } +// ANCHOR_END: ty_parse_impl #[tracing::instrument(level = "trace", ret)] -fn parse_adt_ty<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult<'t, Ty> { +fn parse_adt_ty<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Ty> { // Treat plain identifiers as adt ids, with or without parameters. let ((), text) = reject_keyword("static", text)?; let ((), text) = reject_keyword("const", text)?; @@ -66,7 +71,7 @@ fn parse_adt_ty<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult<' } #[tracing::instrument(level = "trace", ret)] -fn parse_ref_ty<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult<'t, Ty> { +fn parse_ref_ty<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Ty> { let ((), text) = expect_char('&', text)?; let (lt, text) = Lt::parse(scope, text)?; let (ty, text) = Ty::parse(scope, text)?; @@ -82,7 +87,7 @@ fn parse_ref_ty<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult<' } #[tracing::instrument(level = "trace", ret)] -fn parse_ref_mut_ty<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult<'t, Ty> { +fn parse_ref_mut_ty<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Ty> { let ((), text) = expect_char('&', text)?; let ((), text) = expect_keyword("mut", text)?; let (lt, text) = Lt::parse(scope, text)?; @@ -99,7 +104,7 @@ fn parse_ref_mut_ty<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResu } #[tracing::instrument(level = "trace", ret)] -fn parse_tuple_ty<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult<'t, Ty> { +fn parse_tuple_ty<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Ty> { let ((), text) = expect_char('(', text)?; let ((), text) = reject_keyword("rigid", text)?; let ((), text) = reject_keyword("alias", text)?; @@ -118,7 +123,7 @@ fn parse_tuple_ty<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult } #[tracing::instrument(level = "trace", ret)] -fn parse_assoc_ty<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult<'t, Ty> { +fn parse_assoc_ty<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Ty> { // Treat plain identifiers as adt ids, with or without parameters. let ((), text) = expect_char('<', text)?; let (ty0, text) = Ty::parse(scope, text)?; @@ -140,10 +145,7 @@ fn parse_assoc_ty<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult } #[tracing::instrument(level = "trace", ret)] -fn parse_parameters<'t>( - scope: &crate::parse::Scope, - text: &'t str, -) -> ParseResult<'t, Vec> { +fn parse_parameters<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Vec> { let text = match expect_char('<', text) { Err(_) => return Ok((vec![], text)), Ok(((), text)) => text, @@ -153,8 +155,8 @@ fn parse_parameters<'t>( Ok((parameters, text)) } -impl Parse for Lt { - fn parse<'t>(scope: &crate::parse::Scope, text0: &'t str) -> ParseResult<'t, Self> { +impl CoreParse for Lt { + fn parse<'t>(scope: &Scope, text0: &'t str) -> ParseResult<'t, Self> { parse::require_unambiguous( text0, vec![ @@ -179,7 +181,7 @@ impl Parse for Lt { } #[tracing::instrument(level = "trace", ret)] -fn parse_variable<'t>(scope: &crate::parse::Scope, text0: &'t str) -> ParseResult<'t, Parameter> { +fn parse_variable<'t>(scope: &Scope, text0: &'t str) -> ParseResult<'t, Parameter> { let (id, text1) = parse::identifier(text0)?; match scope.lookup(&id) { Some(parameter) => Ok((parameter, text1)), @@ -189,8 +191,8 @@ fn parse_variable<'t>(scope: &crate::parse::Scope, text0: &'t str) -> ParseResul // For consts, we invest some effort into parsing them decently because it makes // writing tests so much more pleasant. -impl Parse for Const { - fn parse<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult<'t, Self> { +impl CoreParse for Const { + fn parse<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Self> { let text = parse::skip_whitespace(text); if let Ok((bool, text)) = Bool::parse(scope, text) { return Ok((bool.upcast(), text)); @@ -214,7 +216,7 @@ impl Parse for Const { } #[tracing::instrument(level = "trace", ret)] -fn parse_int<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult<'t, Const> { +fn parse_int<'t>(scope: &Scope, text: &'t str) -> ParseResult<'t, Const> { let (num, text) = text.split_once('_').ok_or_else(|| { ParseError::at( text, diff --git a/crates/formality-types/src/grammar/ty/term_impls.rs b/crates/formality-types/src/grammar/ty/term_impls.rs new file mode 100644 index 00000000..fe80ffcc --- /dev/null +++ b/crates/formality-types/src/grammar/ty/term_impls.rs @@ -0,0 +1,135 @@ +use crate::grammar::{Const, ConstData, Lt, LtData, Parameter, Ty, TyData, ValTree}; +use crate::rust::Variable; +use crate::FormalityLang; +use formality_core::{ + fold::{CoreFold, SubstitutionFn}, + language::CoreKind, + term::CoreTerm, + visit::CoreVisit, + Upcast, +}; + +use super::ParameterKind; + +impl CoreVisit for LtData { + fn free_variables(&self) -> Vec { + match self { + LtData::Variable(v) => { + if v.is_free() { + vec![*v] + } else { + vec![] + } + } + LtData::Static => vec![], + } + } + + fn size(&self) -> usize { + match self { + LtData::Variable(v) => v.size(), + LtData::Static => 1, + } + } + + fn assert_valid(&self) { + match self { + LtData::Variable(v) => v.assert_valid(), + LtData::Static => (), + } + } +} + +impl CoreTerm for Ty {} + +impl CoreTerm for Lt {} + +impl formality_core::language::HasKind for Parameter { + fn kind(&self) -> CoreKind { + match self { + Parameter::Ty(_) => ParameterKind::Ty, + Parameter::Lt(_) => ParameterKind::Lt, + Parameter::Const(_) => ParameterKind::Const, + } + } +} + +// ANCHOR: core_fold_ty +impl CoreFold for Ty { + fn substitute(&self, substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self { + match self.data() { + TyData::RigidTy(v) => v.substitute(substitution_fn).upcast(), + TyData::AliasTy(v) => v.substitute(substitution_fn).upcast(), + TyData::PredicateTy(v) => v.substitute(substitution_fn).upcast(), + TyData::Variable(v) => match substitution_fn(*v) { + None => self.clone(), + Some(Parameter::Ty(t)) => t, + Some(param) => panic!("ill-kinded substitute: expected type, got {param:?}"), + }, + } + } +} +// ANCHOR_END: core_fold_ty + +impl CoreFold for Const { + fn substitute(&self, substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self { + match self.data() { + ConstData::Value(v, ty) => Self::valtree( + v.substitute(substitution_fn), + ty.substitute(substitution_fn), + ), + ConstData::Variable(v) => match substitution_fn(*v) { + None => self.clone(), + Some(Parameter::Const(c)) => c, + Some(param) => panic!("ill-kinded substitute: expected const, got {param:?}"), + }, + } + } +} + +impl CoreFold for ValTree { + fn substitute(&self, _substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self { + self.clone() + } +} + +impl CoreFold for Lt { + fn substitute(&self, substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self { + match self.data() { + LtData::Static => self.clone(), + LtData::Variable(v) => match substitution_fn(*v) { + None => self.clone(), + Some(Parameter::Lt(t)) => t, + Some(param) => panic!("ill-kinded substitute: expected lifetime, got {param:?}"), + }, + } + } +} + +impl CoreVisit for Ty { + fn free_variables(&self) -> Vec { + self.data().free_variables() + } + + fn size(&self) -> usize { + self.data().size() + } + + fn assert_valid(&self) { + self.data().assert_valid() + } +} + +impl CoreVisit for Lt { + fn free_variables(&self) -> Vec { + self.data().free_variables() + } + + fn size(&self) -> usize { + self.data().size() + } + + fn assert_valid(&self) { + self.data().assert_valid() + } +} diff --git a/crates/formality-types/src/grammar/wc.rs b/crates/formality-types/src/grammar/wc.rs index 37e1741a..a3231c00 100644 --- a/crates/formality-types/src/grammar/wc.rs +++ b/crates/formality-types/src/grammar/wc.rs @@ -1,15 +1,11 @@ use std::sync::Arc; -use formality_macros::term; - -use crate::{ - cast::{DowncastFrom, DowncastTo, Upcast, UpcastFrom, Upcasted}, - cast_impl, - collections::{Set, SetExt}, - grammar::PR, - set, +use formality_core::{ + cast_impl, set, term, DowncastFrom, DowncastTo, Set, SetExt, Upcast, UpcastFrom, Upcasted, }; +use crate::grammar::PR; + use super::{Binder, BoundVar, Parameter, Predicate, Relation, TraitRef}; #[term($set)] diff --git a/crates/formality-types/src/lib.rs b/crates/formality-types/src/lib.rs index cd99bd70..e30835d4 100644 --- a/crates/formality-types/src/lib.rs +++ b/crates/formality-types/src/lib.rs @@ -1,15 +1,19 @@ #![allow(dead_code)] -pub mod collections; -pub mod fixed_point; -pub mod fold; pub mod grammar; -pub mod judgment; -pub mod matcher; -pub mod parse; -pub mod term; -pub mod visit; -pub mod derive_links; +// ANCHOR: declare_rust_language +formality_core::declare_language! { + pub mod rust { + const NAME = "Rust"; + type Kind = crate::grammar::ParameterKind; + type Parameter = crate::grammar::Parameter; + const BINDING_OPEN = '<'; + const BINDING_CLOSE = '>'; + } +} +// ANCHOR_END: declare_rust_language -pub mod cast; +// ANCHOR: use_rust_language +use crate::rust::FormalityLang; +// ANCHOR_END: use_rust_language diff --git a/crates/formality-types/src/matcher.rs b/crates/formality-types/src/matcher.rs deleted file mode 100644 index e69de29b..00000000 diff --git a/crates/formality-types/src/parse/test.rs b/crates/formality-types/src/parse/test.rs deleted file mode 100644 index 09f57072..00000000 --- a/crates/formality-types/src/parse/test.rs +++ /dev/null @@ -1,80 +0,0 @@ -#![cfg(test)] -#![cfg(FIXME)] - -use super::term; -use crate::grammar::{AtomicPredicate, Goal, Ty}; -use expect_test::expect; -use formality_macros::test; - -#[test] -fn parse_atomic_predicate() { - let program: AtomicPredicate = term("is_implemented(Debug(u32))"); - expect![[r#" - is_implemented( - Debug((rigid (scalar u32))), - ) - "#]] - .assert_debug_eq(&program); -} - -#[test] -fn parse_forall_goal() { - let program: Goal = term("for_all( is_implemented(Debug(T)))"); - expect![[r#" - for_all( is_implemented(Debug(^ty0_0))) - "#]] - .assert_debug_eq(&program); -} - -#[test] -fn parse_nested_binders() { - // T should have a debruijn index of 1, U should have a debruijn index of 0 - let program: Goal = term("for_all( exists( is_implemented(Debug(T, U))))"); - expect![[r#" - for_all( exists( is_implemented(Debug(^ty1_0, ^ty0_0)))) - "#]] - .assert_debug_eq(&program); -} - -#[test] -fn parse_all() { - // T should have a debruijn index of 1 the first time, 0 the second time - let program: Goal = term( - "for_all( all( - exists( is_implemented(PartialEq(T, U))), - has_impl(Debug(T)), - ))", - ); - expect![[r#" - for_all( all(exists( is_implemented(PartialEq(^ty1_0, ^ty0_0))), has_impl(Debug(^ty0_0)))) - "#]] - .assert_debug_eq(&program); -} - -#[test] -fn parse_scalar_id() { - let ty1: Ty = term("u8"); - let ty2: Ty = term("(rigid (scalar u8))"); - assert_eq!(ty1, ty2); -} - -#[test] -fn parse_adts_with_parameters() { - let ty1: Ty = term("Vec"); - let ty2: Ty = term("(rigid (adt Vec) (rigid (adt String)))"); - assert_eq!(ty1, ty2); -} - -#[test] -fn parse_assoc_type() { - let ty1: Ty = term("::Item"); - let ty2: Ty = term("(alias (Iterator::Item) String)"); - assert_eq!(ty1, ty2); -} - -#[test] -fn parse_gat() { - let ty1: Ty = term("::Item"); - let ty2: Ty = term("(alias (Iterator::Item) String (rigid (scalar u32)))"); - assert_eq!(ty1, ty2); -} diff --git a/crates/formality-types/src/term.rs b/crates/formality-types/src/term.rs deleted file mode 100644 index 4b0c7cab..00000000 --- a/crates/formality-types/src/term.rs +++ /dev/null @@ -1,36 +0,0 @@ -use std::{fmt::Debug, hash::Hash, sync::Arc}; - -use crate::{ - cast::{DowncastFrom, Upcast}, - collections::Set, - fold::Fold, - grammar::{Binder, Lt, Ty}, - parse::Parse, -}; - -pub trait Term: - Clone + Fold + Parse + Ord + Eq + Hash + Debug + Upcast + DowncastFrom + 'static + Sized -{ -} - -impl Term for Vec {} - -impl Term for Set {} - -impl Term for Option {} - -impl Term for Arc {} - -impl Term for Ty {} - -impl Term for Lt {} - -impl Term for usize {} - -impl Term for u32 {} - -impl Term for (A, B) {} - -impl Term for Binder {} - -impl Term for () {} diff --git a/crates/formality-types/src/visit.rs b/crates/formality-types/src/visit.rs index 3ab72dfb..f41c5e7d 100644 --- a/crates/formality-types/src/visit.rs +++ b/crates/formality-types/src/visit.rs @@ -1,246 +1,5 @@ -use std::sync::Arc; +use formality_core::visit::CoreVisit; -use crate::{ - collections::Set, - grammar::{Lt, Parameter, Ty, Variable}, -}; +use crate::grammar::{Lt, Ty, Variable}; -/// Invoked for each variable that we find when Visiting, ignoring variables bound by binders -/// that we traverse. The arguments are as follows: -/// -/// * ParameterKind -- the kind of term in which the variable appeared (type vs lifetime, etc) -/// * Variable -- the variable we encountered -pub type SubstitutionFn<'a> = &'a mut dyn FnMut(Variable) -> Option; - -pub trait Visit { - /// Extract the list of free variables (for the purposes of this function, defined by `Variable::is_free`). - /// The list may contain duplicates and must be in a determinstic order (though the order itself isn't important). - fn free_variables(&self) -> Vec; - - /// Measures the overall size of the term by counting constructors etc. - /// Used to determine overflow. - fn size(&self) -> usize; - - /// Asserts various validity constraints and panics if they are not held. - /// These validition constraints should never fail unless there is a bug in our logic. - /// This is to aid with fuzzing and bug detection. - fn assert_valid(&self); - - /// True if this term references only universal variables. - /// This means that it contains no existential variables. - /// If this is a goal, then when we prove it true, we don't expect any substitution. - /// This is similar, but not *identical*, to the commonly used term "ground term", - /// which in Prolog refers to a term that contains no variables. The difference here - /// is that the term may contain variables, but only those instantiated universally (∀). - fn references_only_universal_variables(&self) -> bool { - self.free_variables().iter().all(|v| match v { - Variable::UniversalVar(_) => true, - Variable::ExistentialVar(_) => false, - Variable::BoundVar(_) => false, - }) - } -} - -impl Visit for Vec { - fn free_variables(&self) -> Vec { - self.iter().flat_map(|e| e.free_variables()).collect() - } - - fn size(&self) -> usize { - self.iter().map(|e| e.size()).sum() - } - - fn assert_valid(&self) { - self.iter().for_each(|e| e.assert_valid()); - } -} - -impl Visit for Set { - fn free_variables(&self) -> Vec { - self.iter().flat_map(|e| e.free_variables()).collect() - } - - fn size(&self) -> usize { - self.iter().map(|e| e.size()).sum() - } - - fn assert_valid(&self) { - self.iter().for_each(|e| e.assert_valid()); - } -} - -impl Visit for Option { - fn free_variables(&self) -> Vec { - self.iter().flat_map(|e| e.free_variables()).collect() - } - - fn size(&self) -> usize { - self.as_ref().map(|e| e.size()).unwrap_or(0) - } - - fn assert_valid(&self) { - self.iter().for_each(|e| e.assert_valid()); - } -} - -impl Visit for Arc { - fn free_variables(&self) -> Vec { - T::free_variables(self) - } - - fn size(&self) -> usize { - T::size(self) - } - - fn assert_valid(&self) { - T::assert_valid(self) - } -} - -impl Visit for Ty { - fn free_variables(&self) -> Vec { - self.data().free_variables() - } - - fn size(&self) -> usize { - self.data().size() - } - - fn assert_valid(&self) { - self.data().assert_valid() - } -} - -impl Visit for Lt { - fn free_variables(&self) -> Vec { - self.data().free_variables() - } - - fn size(&self) -> usize { - self.data().size() - } - - fn assert_valid(&self) { - self.data().assert_valid() - } -} - -impl Visit for usize { - fn free_variables(&self) -> Vec { - vec![] - } - - fn size(&self) -> usize { - 1 - } - - fn assert_valid(&self) {} -} - -impl Visit for u32 { - fn free_variables(&self) -> Vec { - vec![] - } - - fn size(&self) -> usize { - 1 - } - - fn assert_valid(&self) {} -} - -impl Visit for u128 { - fn free_variables(&self) -> Vec { - vec![] - } - - fn size(&self) -> usize { - std::mem::size_of::() - } - - fn assert_valid(&self) {} -} - -impl Visit for () { - fn free_variables(&self) -> Vec { - vec![] - } - - fn size(&self) -> usize { - 0 - } - - fn assert_valid(&self) {} -} - -impl Visit for (A, B) { - fn free_variables(&self) -> Vec { - let (a, b) = self; - let mut fv = vec![]; - fv.extend(a.free_variables()); - fv.extend(b.free_variables()); - fv - } - - fn size(&self) -> usize { - let (a, b) = self; - a.size() + b.size() - } - - fn assert_valid(&self) { - let (a, b) = self; - a.assert_valid(); - b.assert_valid(); - } -} - -impl Visit for (A, B, C) { - fn free_variables(&self) -> Vec { - let (a, b, c) = self; - let mut fv = vec![]; - fv.extend(a.free_variables()); - fv.extend(b.free_variables()); - fv.extend(c.free_variables()); - fv - } - - fn size(&self) -> usize { - let (a, b, c) = self; - a.size() + b.size() + c.size() - } - - fn assert_valid(&self) { - let (a, b, c) = self; - a.assert_valid(); - b.assert_valid(); - c.assert_valid(); - } -} - -impl Visit for &A { - fn free_variables(&self) -> Vec { - A::free_variables(self) - } - - fn size(&self) -> usize { - A::size(self) - } - - fn assert_valid(&self) { - A::assert_valid(self) - } -} - -impl Visit for [A] { - fn free_variables(&self) -> Vec { - self.iter().flat_map(|e| A::free_variables(e)).collect() - } - - fn size(&self) -> usize { - self.iter().map(|e| A::size(e)).sum() - } - - fn assert_valid(&self) { - self.iter().for_each(|e| A::assert_valid(e)); - } -} +use crate::FormalityLang as Rust; diff --git a/src/lib.rs b/src/lib.rs index 82ee1e12..f1761b6b 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -2,9 +2,10 @@ use std::{path::PathBuf, sync::Arc}; use clap::Parser; use formality_check::check_all_crates; +use formality_core::Set; use formality_prove::{test_util::TestAssertion, Constraints}; use formality_rust::grammar::Program; -use formality_types::{collections::Set, parse::try_term}; +use formality_types::rust::try_term; #[derive(Parser, Debug)] #[command(author, version, about, long_about = None)]