formality-core

name	formality-core
description	Idiomatic patterns for writing code with formality-core (a-mir-formality). Use when writing or reviewing judgment functions, type definitions, or parser-related code in projects built on formality-core.
depends-on	formality-core

Idiomatic formality-core

This skill covers patterns and anti-patterns when writing code with formality-core. Following these idioms produces cleaner, more concise code and avoids subtle bugs.

Generated constructors from #[term]

The #[term] macro generates constructor methods on every type it annotates.

Structs get ::new(...)

#[term($name $[?parameters])]
pub struct NamedTy {
    pub name: TypeName,
    pub parameters: Parameters,
}

Generates: NamedTy::new(name, parameters) where each parameter accepts impl Upcast<FieldType>.

Enums get ::snake_case_variant(...)

#[term]
pub enum Perm {
    #[grammar(given_from $[v0])]
    Mv(Set<Place>),
    Given,
    Shared,
    #[grammar(ref $[?v0])]
    Rf(Set<Place>),
    #[grammar(mut $[v0])]
    Mt(Set<Place>),
    #[variable(Kind::Perm)]
    Var(Variable),
    Apply(Arc<Perm>, Arc<Perm>),
}

Generates lowercase snake_case methods. Rust keywords get a trailing _:

Variant	Generated method
Mv(Set<Place>)	Perm::mv(places)
Given	(no method — zero fields)
Shared	(no method — zero fields)
Rf(Set<Place>)	Perm::rf(places)
Mt(Set<Place>)	Perm::mt(places)
Var(Variable)	Perm::var(v)
Apply(Arc<Perm>, Arc<Perm>)	Perm::apply(p1, p2)

Zero-field variants (like Given, Shared) get no generated constructor — use the enum literal Perm::Given directly.

Rule: always prefer generated constructors

// ✅ Good — generated constructor, accepts impl Upcast
Perm::var(perm_var)
Perm::rf(set![place])
NamedTy::new(name, substitution)
Predicate::parameter(ParameterPredicate::Copy, perm_var)

// ❌ Bad — manual construction, requires explicit conversion
Perm::Var(perm_var.upcast())
Perm::Var(Variable::from(perm_var.clone()))
Perm::Rf(set![place.clone()])

The generated constructors accept impl Upcast<T> for every field, so they handle conversions (e.g., UniversalVar → Variable → Perm::Var) and cloning automatically. You never need to manually .upcast(), .into(), or .clone() when calling a generated constructor.

Upcast coercions: avoiding explicit clones

The Upcast/UpcastFrom system provides automatic coercions. The key blanket impl:

impl<T: Clone, U> UpcastFrom<&T> for U where U: UpcastFrom<T> { ... }

This means: anywhere impl Upcast<T> is expected, you can pass &T and it will clone for you. This eliminates most explicit .clone() calls.

Where this applies

1. Generated constructors — all parameters accept impl Upcast<FieldType>
2. judgment_fn! parameters — the function signature is fn f(x: impl Upcast<T>)
3. Env methods — push_local_variable, add_assumptions, etc. accept impl Upcast<T>
4. Judgment return positions — results upcast automatically to the declared return type

Common coercion chains

Source	Target	How
&T	T	auto-clone via UpcastFrom<&T>
UniversalVar	Variable	UpcastFrom
UniversalVar	Parameter	via Variable → Parameter
NamedTy	Ty	UpcastFrom on Ty::NamedTy variant
Ty	Parameter	UpcastFrom on Parameter::Ty variant
Perm	Parameter	UpcastFrom on Parameter::Perm variant
Place	via Var	UpcastFrom<Var> for Place
Vec<T>	Vec<U>	element-wise upcast
&[T]	Vec<U>	element-wise upcast

Upcasted iterator adapter

Use .upcasted() (from formality_core::Upcasted) for element-wise upcast in iterator chains:

// ✅ Good
let perms: Vec<Perm> = chains.into_iter().upcasted().collect();

// ❌ Verbose
let perms: Vec<Perm> = chains.into_iter().map(|c| c.upcast()).collect();

Examples

// ✅ Good — pass &reference, upcast handles cloning
let env = env.push_local_variable(Var::This, &class_ty)?;
Predicate::parameter(ParameterPredicate::Copy, &perm_var)

// ❌ Bad — unnecessary explicit clone
let env = env.push_local_variable(Var::This, class_ty.clone())?;
Predicate::parameter(ParameterPredicate::Copy, perm_var.clone())

Exception: When the value is already owned and you're done with it, just pass it directly — no & needed:

// ✅ Good — class_ty is owned and consumed here
let env = env.push_local_variable(Var::This, class_ty)?;

judgment_fn! patterns

Parameters are owned inside the body

The macro expands fn f(x: impl Upcast<T>) and immediately does let x: T = Upcast::upcast(x). Inside the rule body, x is an owned T. However, within pattern-matched destructuring, fields from a matched struct/enum are references (standard Rust match ergonomics).

judgment_fn! {
    fn check(env: Env, decl: ClassDecl) => () {
        (
            // `decl` is owned ClassDecl
            // After destructuring, `name` is `&ValueId`, `binder` is `&Binder<...>`
            (let ClassDecl { name, binder, .. } = decl)
            // But generated constructors accept `impl Upcast<T>`,
            // which includes `&T`, so this just works:
            (let class_ty = NamedTy::new(name, substitution))  // ✅ name is &ValueId, auto-cloned
            ...
        )
    }
}

Pattern matching in conclusions for dispatch

Use pattern matching in the conclusion to dispatch on variants — cleaner than if guards:

// ✅ Good — pattern match directly
(
    (let env = env.push_local_variable(Var::This, class_ty)?)
    ...
    ----------------------------------- ("given_class_drop")
    (check_drop_body(class_ty, ClassPredicate::Given, env, body) => ())
)

(
    ...
    ----------------------------------- ("share_class_drop")
    (check_drop_body(class_ty, ClassPredicate::Share | ClassPredicate::Shared, env, body) => ())
)

// ❌ Avoid — if-guard when pattern match works
(
    (if *class_predicate == ClassPredicate::Given)
    ...
    ----------------------------------- ("given_class_drop")
    (check_drop_body(class_ty, class_predicate, env, body) => ())
)

Struct patterns in conclusions

Destructure structs directly in the conclusion instead of matching a wrapper and then destructuring with let:

// ✅ Good — destructure in conclusion, result auto-upcasts
(
    (normalize_params(env, parameters) => norm_params)
    --- ("named")
    (normalize_ty(env, NamedTy { name, parameters }) => NamedTy::new(name, norm_params))
)

// ❌ Verbose — extra let + explicit wrapping
(
    (let NamedTy { name, parameters } = named_ty)
    (normalize_params(env, parameters) => norm_params)
    --- ("named")
    (normalize_ty(env, Ty::NamedTy(named_ty))
        => Ty::NamedTy(NamedTy { name: name.clone(), parameters: norm_params.to_vec() }))
)

Note: NamedTy::new(name, norm_params) returns a NamedTy, which auto-upcasts to Ty (via the Ty::NamedTy variant cast) when the judgment's return type is Ty.

Upcast in return values

Judgment results upcast to the declared return type automatically. If your judgment returns Parameter, you can return a Ty or Perm directly:

// ✅ Good — Ty auto-upcasts to Parameter
(
    (normalize_ty(env, ty) => norm_ty)
    --- ("ty")
    (normalize_param(env, Parameter::Ty(ty)) => norm_ty)
)

// ❌ Verbose — manual wrapping
(
    (normalize_ty(env, ty) => norm_ty)
    --- ("ty")
    (normalize_param(env, Parameter::Ty(ty)) => Parameter::ty(norm_ty))
)

Building collections with Cons and ()

For recursive list/set processing in judgments, use Cons(head, tail) in both pattern matching and return positions. Use () for empty collections.

judgment_fn! {
    fn process_list(env: Env, items: Vec<Item>) => Vec<Item> {
        // Base case: empty → empty (() upcasts to empty Vec)
        (
            --- ("nil")
            (process_list(_env, ()) => ())
        )

        // Recursive: Cons destructures the head, Cons builds the result
        (
            (transform(env, item) => new_item)
            (process_list(env, rest) => new_rest)
            --- ("cons")
            (process_list(env, Cons(item, rest)) => Cons(new_item, new_rest))
        )
    }
}

This works for both Vec<T> and Set<T>. No need for prepend helpers, Vec::new(), or std::iter::once(...).chain(...).collect().

Cut points with !

Place ! after a condition to mark a match commit point. Rules that fail before the cut are excluded from error reports. Use cuts on guard conditions that definitively select or reject a rule:

// ✅ Good — cut prevents "empty_drop failed" noise in error messages
(
    (if drop_body.block.statements.is_empty())!
    ----------------------------------- ("empty_drop")
    (check_drop_body(_class_ty, _class_predicate, _env, drop_body) => ())
)

Without the !, if the empty check passes but a later rule fails, error reports would unhelpfully include "empty_drop failed because condition was false" for non-empty bodies.

Complementary guards should both have cuts. When two rules partition cases with a boolean check, put ! on both:

// ✅ Good — both branches cut
(
    (if !needs_work(&value))!
    --- ("no work needed")
    (process(_env, value) => value)
)

(
    (if needs_work(&value))!
    (do_work(env, value) => result)
    --- ("do work")
    (process(env, value) => result)
)

Arc<T> gotcha

Fields declared as Arc<T> become &Arc<T> when destructured (standard Rust). Calling .clone() gives you Arc<T>, not T. When passing to a judgment or generated constructor that accepts impl Upcast<T>, use &**x to get &T — the UpcastFrom<&T> blanket impl handles the clone:

// Inside a judgment rule where `inner_ty` is `&Arc<Ty>`:
(some_judgment(env, &**inner_ty) => result)  // ✅ &**inner_ty is &Ty, upcast clones it
(some_judgment(env, inner_ty.clone()) => result)  // ❌ Passes Arc<Ty>, not Ty

For non-Arc fields (e.g., perm: &Perm from ApplyPerm(Perm, Arc<Ty>)), just pass perm directly — &Perm upcasts to Perm automatically.

for_all vs in

• (x in collection) — existential: there exists some x in collection that satisfies the remaining conditions
• (for_all(x in collection) (condition)) — universal: all x in collection must satisfy condition

// Check ALL fields
(for_all(field in fields)
    (check_field(env, field) => ()))

// Find SOME method matching the name
(MethodDecl { name: _, binder } in methods.into_iter().filter(|m| m.name == *method_name))

Using judgment results outside judgment_fn!

Judgment functions return ProvenSet<T>, not T or Result<T>. Inside judgment_fn! rules, the => syntax handles this automatically. Outside, you must extract results explicitly:

// Check if a judgment succeeds (bool)
prove_is_copy(&env, &param).is_proven()

// Extract a single result (when exactly one is expected).
// into_singleton() returns Result<(T, ProofTree), Box<FailedJudgment>>.
// Box<FailedJudgment> is compatible with `?` in anyhow contexts — no map_err needed.
let (result, _proof) = red_perm(&env, &live_after, &perm)
    .into_singleton()?;

// Get all results as a map
let results = my_judgment(&env, &x)
    .into_map()?;

Common mistake: calling .is_ok() on a ProvenSet — it doesn't have that method. Use .is_proven() instead.

Parser / grammar conventions

Kind keywords are lowercase

formality-core parses Kind variants as their lowercase names. For a Kind enum with Ty and Perm variants, the parser keywords are ty and perm:

// ✅ Correct in test strings / parsed programs
"class Wrapper[ty T] { ... }"
"class Foo[perm P, ty T] { ... }"

// ❌ Wrong — "type" is not a keyword
"class Wrapper[type T] { ... }"

KEYWORDS vs grammar keywords

Words in the KEYWORDS list in declare_language! are globally reserved — they can never be used as identifiers anywhere. Grammar keywords (#[grammar(x)] on enum variants) work without being in KEYWORDS — they're only recognized in the specific parsing context.

Only add to KEYWORDS when you want to block identifier use. Don't add a word to KEYWORDS just because it appears in a #[grammar(...)] annotation.

Prefix ambiguity

If one variant's keyword is a prefix of another's in the same enum (e.g., given vs given_from[...]), the parser silently matches the shorter one. Use distinct keywords to avoid this.

$? for optional fields

$?field in a grammar annotation makes the field optional. The field type must implement Default. When the field is absent in the input, the Default value is used:

#[term($:where $,predicates { $*fields $*methods $?drop_body })]
pub struct ClassDeclBoundData {
    pub predicates: Vec<Predicate>,
    pub fields: Vec<FieldDecl>,
    pub methods: Vec<MethodDecl>,
    pub drop_body: DropBody,  // Default::default() when omitted
}

Generated constructor name collisions

The #[term] macro generates EnumName::snake_case_variant(...) for each variant. For example, Perm::Or(Set<Perm>) generates Perm::or(...). If you add a hand-written method with the same name in an impl block, you get a "duplicate definitions" error. Use a distinct name:

// ❌ Fails — collides with generated Perm::or()
impl Perm {
    pub fn or(perms: impl IntoIterator<Item = Perm>) -> Perm { ... }
}

// ✅ Good — distinct name
impl Perm {
    pub fn flat_or(perms: impl IntoIterator<Item = Perm>) -> Perm { ... }
}

Summary of rules

1. Use generated constructors (Perm::var(x) not Perm::Var(x.upcast()))
2. Pass references where impl Upcast<T> is expected — the framework clones for you
3. Pattern match in judgment conclusions instead of if guards
4. Destructure structs in conclusions, not with separate let bindings
5. Let upcast handle return values — norm_ty auto-upcasts to Parameter, NamedTy to Ty
6. Use Cons/() for collections in judgment return positions, not manual Vec building
7. Use ! cuts on guard conditions, including both sides of complementary pairs
8. Use &**x for Arc<T> fields, not .clone()
9. Use ty/perm as kind keywords in parsed strings, not type/perm
10. Use .into_singleton()? directly — no map_err needed
11. Use .upcasted() for element-wise iterator upcast
12. Don't add to KEYWORDS unless you need to reserve the word globally