catlog/tt/
toplevel.rs

1//! Data structures for managing toplevel declarations in the type theory.
2//!
3//! The three kinds mirror the comprehension category of `D`-models: a [Type]
4//! is a model (a context, i.e. an object of the base), a [Def] is a tight
5//! transformation (a substitution, i.e. a morphism of the base), and an
6//! [Instance] is an object of a fiber (a type in context).
7
8use derive_more::Constructor;
9
10use super::{prelude::*, stx::*, theory::*, val::*};
11use crate::zero::QualifiedName;
12
13/// A toplevel declaration.
14#[derive(Clone)]
15pub enum TopDecl {
16    /// See [Type].
17    Type(Type),
18    /// See [Def].
19    Def(Def),
20    /// See [Instance].
21    Instance(Instance),
22}
23
24/// A toplevel declaration of a type.
25///
26/// Also stores the evaluation of that type. Because this is an evaluation in
27/// the empty context, this is OK to use in any other context as well.
28#[derive(Constructor, Clone)]
29pub struct Type {
30    /// The theory for the type.
31    pub theory: Theory,
32    /// The syntax of the type (unnormalized).
33    pub stx: BaseTyS,
34    /// The value of the type (normalized).
35    pub val: BaseTyV,
36}
37
38/// A toplevel declaration of an instance of a model.
39///
40/// An instance is an object of the fiber over its codomain model `X` in the
41/// comprehension category of `D`-models: a generator/equation/sub-instance
42/// body packaged as the presentation of an `X`-instance. It is declared with
43/// `instance NAME : X := [...]`.
44///
45/// The instance is represented directly as a fiber type — a fiber
46/// [`Record`](super::stx::FiberTyS_::Record) whose fields are its
47/// generators ([`Over`](super::stx::FiberTyS_::Over)), sub-instance
48/// imports (nested records), and equations
49/// ([`Id`](super::stx::FiberTyS_::Id)). A sub-instance import `we : Edge`
50/// uses this fiber type directly.
51#[derive(Constructor, Clone)]
52pub struct Instance {
53    /// The theory that the instance is defined in.
54    pub theory: Theory,
55    /// The syntax of the instance, as a fiber record type.
56    pub stx: FiberTyS,
57    /// The value of the instance, as a fiber record type.
58    pub val: FiberTyV,
59    /// The codomain model `X` that this is an instance of.
60    pub codomain: BaseTyV,
61}
62
63/// A toplevel declaration of a term judgment.
64#[derive(Constructor, Clone)]
65pub struct Def {
66    /// The theory that the definition is defined in.
67    pub theory: Theory,
68    /// The arguments for the definition.
69    pub args: Row<BaseTyS>,
70    /// The return type of the definition (to be evaluated in an environment
71    /// with values for the arguments).
72    pub ret_ty: BaseTyS,
73    /// The body of the definition (to be evaluated in an environment with
74    /// values for the arguments).
75    pub body: BaseTmS,
76}
77
78impl TopDecl {
79    /// Unwraps the type for a toplevel-declaration of a type, or panics.
80    ///
81    /// This should only be used after type checking, when we know that a toplevel
82    /// variable name does in fact point to a toplevel declaration for a type.
83    pub fn unwrap_ty(self) -> Type {
84        match self {
85            TopDecl::Type(ty) => ty,
86            _ => panic!("top-level should be a type declaration"),
87        }
88    }
89
90    /// Unwraps the definition for a toplevel term judgment, or panics.
91    pub fn unwrap_def(self) -> Def {
92        match self {
93            TopDecl::Def(d) => d,
94            _ => panic!("top-level should be a term judgment"),
95        }
96    }
97}
98
99/// Storage for toplevel declarations.
100#[derive(Default)]
101pub struct Toplevel {
102    /// Library of theories, indexed by name.
103    pub theory_library: HashMap<QualifiedName, Theory>,
104    /// The toplevel declarations, indexed by their name.
105    pub declarations: HashMap<TopVarName, TopDecl>,
106}
107
108impl Toplevel {
109    /// Constructs an empty [Toplevel].
110    pub fn new(theory_library: HashMap<QualifiedName, Theory>) -> Self {
111        Toplevel {
112            theory_library,
113            declarations: HashMap::new(),
114        }
115    }
116
117    /// Lookup a toplevel declaration by name.
118    pub fn lookup(&self, name: TopVarName) -> Option<&TopDecl> {
119        self.declarations.get(&name)
120    }
121}
catlog/tt/toplevel.rs

catlog/tt/
toplevel.rs
