formality_core/
language.rs

1use crate::cast::UpcastFrom;
2use crate::term::CoreTerm;
3use crate::variable::{CoreBoundVar, CoreExistentialVar, CoreUniversalVar, CoreVariable};
4use std::fmt::Debug;
5use std::hash::Hash;
6
7/// The definition of a "language"
8pub trait Language: 'static + Copy + Ord + Hash + Debug + Default {
9    /// Name of the language, e.g., `"Rust"`
10    const NAME: &'static str;
11
12    /// An enum defining the *kinds* of generic parameters (e.g., for Rust,
13    /// types, lifetimes, and constants).
14    type Kind: Copy + CoreTerm<Self>;
15
16    /// An enum defining the *value* of a generic parameter (e.g., a
17    /// type, a lifetime, etc)
18    type Parameter: HasKind<Self>
19        + CoreTerm<Self>
20        + UpcastFrom<CoreVariable<Self>>
21        + UpcastFrom<CoreUniversalVar<Self>>
22        + UpcastFrom<CoreExistentialVar<Self>>
23        + UpcastFrom<CoreBoundVar<Self>>;
24
25    /// The character (typically `<`) used to open binders.
26    const BINDING_OPEN: char;
27
28    /// The character (typically `>`) used to open binders.
29    const BINDING_CLOSE: char;
30}
31
32/// For consistency with types like `CoreVariable<L>`, we write `CoreKind<L>` instead of `Kind<L>`.
33pub type CoreKind<L: Language> = L::Kind;
34
35/// For consistency with types like `CoreVariable<L>`, we write `CoreParameter<L>` instead of `Parameter<L>`.
36pub type CoreParameter<L: Language> = L::Parameter;
37
38pub trait HasKind<L: Language> {
39    fn kind(&self) -> CoreKind<L>;
40}
formality_core/language.rs

formality_core/
language.rs
