dada_ir_sym/check/universe.rs
1use std::num::NonZeroU32;
2
3use serde::Serialize;
4
5/// A "universe" defines the set of all terms (types/permissions/etc) in a program.
6/// The root universe [`Universe::ROOT`][] consists of the terms the user wrote.
7/// We create other universes synthetically to create free universal variables.
8/// For example, in a closure body, we are in a distinct universe, which allows us to
9/// define closures that can reference a (generic) type `T` that doesn't exist in the parent universe.
10///
11/// Universes are ordered. `U1 < U2` means that `U2` can contain strictly more terms than `U1`.
12/// `Universe::ROOT <= U` for all `U`.
13#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize)]
14pub(crate) struct Universe(NonZeroU32);
15
16impl Universe {
17 /// The universe containing the things the user themselves wrote.
18 /// `ROOT` <= all other universes.
19 pub const ROOT: Universe = Universe(NonZeroU32::new(1).unwrap());
20
21 /// Create a universe one larger than the current universe.
22 pub fn next(self) -> Universe {
23 Universe(self.0.checked_add(1).unwrap())
24 }
25}