Skip to content

Commit e4aab6f

Browse files
brendanzabbrendanzab
committed
Rename Universe to TypeType
1 parent f260440 commit e4aab6f

File tree

6 files changed

+29
-29
lines changed

6 files changed

+29
-29
lines changed

‎pikelet/src/lang/core.rs

+10-10
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@ pub enum Term {
7676
Ann(Arc<Term>, Arc<Term>),
7777

7878
/// The type of types.
79-
Universe(UniverseLevel),
79+
TypeType(UniverseLevel),
8080
/// Lift a term by the given number of universe levels.
8181
Lift(Arc<Term>, UniverseOffset),
8282

@@ -113,9 +113,9 @@ pub enum Term {
113113
}
114114

115115
impl Term {
116-
/// Create a universe at the given level.
117-
pub fn universe(level: impl Into<UniverseLevel>) -> Term {
118-
Term::Universe(level.into())
116+
/// Create a type of types at the given level.
117+
pub fn type_type(level: impl Into<UniverseLevel>) -> Term {
118+
Term::TypeType(level.into())
119119
}
120120

121121
/// Create a global variable.
@@ -158,8 +158,8 @@ impl Default for Globals {
158158
entries.insert(
159159
"Type".to_owned(),
160160
(
161-
Arc::new(Term::universe(1)),
162-
Some(Arc::new(Term::universe(0))),
161+
Arc::new(Term::type_type(1)),
162+
Some(Arc::new(Term::type_type(0))),
163163
),
164164
);
165165
entries.insert("Bool".to_owned(), (Arc::new(Term::global("Type")), None));
@@ -185,8 +185,8 @@ impl Default for Globals {
185185
Arc::new(Term::Global("U32".to_owned())),
186186
Arc::new(Term::FunctionType(
187187
None,
188-
Arc::new(Term::universe(0)),
189-
Arc::new(Term::universe(0)),
188+
Arc::new(Term::type_type(0)),
189+
Arc::new(Term::type_type(0)),
190190
)),
191191
)),
192192
None,
@@ -197,8 +197,8 @@ impl Default for Globals {
197197
(
198198
Arc::new(Term::FunctionType(
199199
None,
200-
Arc::new(Term::universe(0)),
201-
Arc::new(Term::universe(0)),
200+
Arc::new(Term::type_type(0)),
201+
Arc::new(Term::type_type(0)),
202202
)),
203203
None,
204204
),

‎pikelet/src/lang/core/semantics.rs

+8-8
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ pub enum Value {
4141
Unstuck(Head, Vec<Elim>, Arc<LazyValue>),
4242

4343
/// The type of types.
44-
Universe(UniverseLevel),
44+
TypeType(UniverseLevel),
4545

4646
/// Function types.
4747
///
@@ -68,9 +68,9 @@ pub enum Value {
6868
}
6969

7070
impl Value {
71-
/// Create a universe at the given level.
72-
pub fn universe(level: impl Into<UniverseLevel>) -> Value {
73-
Value::Universe(level.into())
71+
/// Create a type of types at the given level.
72+
pub fn type_type(level: impl Into<UniverseLevel>) -> Value {
73+
Value::TypeType(level.into())
7474
}
7575

7676
/// Create a global variable.
@@ -286,7 +286,7 @@ pub fn eval_term(
286286

287287
Term::Ann(term, _) => eval_term(globals, universe_offset, values, term),
288288

289-
Term::Universe(level) => Arc::new(Value::universe(
289+
Term::TypeType(level) => Arc::new(Value::type_type(
290290
(*level + universe_offset).unwrap(), // FIXME: Handle overflow
291291
)),
292292
Term::Lift(term, offset) => {
@@ -458,7 +458,7 @@ pub fn read_back_value(
458458
Unfold::All => read_back_value(globals, local_size, unfold, value.force(globals)),
459459
},
460460

461-
Value::Universe(level) => Term::Universe(*level),
461+
Value::TypeType(level) => Term::TypeType(*level),
462462

463463
Value::FunctionType(input_name_hint, input_type, output_closure) => {
464464
let local = Arc::new(Value::local(local_size.next_level()));
@@ -575,7 +575,7 @@ fn is_equal(globals: &Globals, local_size: LocalSize, value0: &Value, value1: &V
575575
is_equal(globals, local_size, value0, value1.force(globals))
576576
}
577577

578-
(Value::Universe(level0), Value::Universe(level1)) => level0 == level1,
578+
(Value::TypeType(level0), Value::TypeType(level1)) => level0 == level1,
579579

580580
(
581581
Value::FunctionType(_, input_type0, output_closure0),
@@ -697,7 +697,7 @@ pub fn is_subtype(
697697
is_subtype(globals, local_size, value0, value1.force(globals))
698698
}
699699

700-
(Value::Universe(level0), Value::Universe(level1)) => level0 <= level1,
700+
(Value::TypeType(level0), Value::TypeType(level1)) => level0 <= level1,
701701

702702
(
703703
Value::FunctionType(_, input_type0, output_closure0),

‎pikelet/src/lang/core/typing.rs

+5-5
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,7 @@ impl<'me> State<'me> {
116116
pub fn is_type(state: &mut State<'_>, term: &Term) -> Option<UniverseLevel> {
117117
let r#type = synth_type(state, term);
118118
match r#type.force(state.globals) {
119-
Value::Universe(level) => Some(*level),
119+
Value::TypeType(level) => Some(*level),
120120
Value::Error => None,
121121
_ => {
122122
state.report(Message::MismatchedTypes {
@@ -243,8 +243,8 @@ pub fn synth_type(state: &mut State<'_>, term: &Term) -> Arc<Value> {
243243
r#type
244244
}
245245

246-
Term::Universe(level) => match *level + UniverseOffset(1) {
247-
Some(level) => Arc::new(Value::universe(level)),
246+
Term::TypeType(level) => match *level + UniverseOffset(1) {
247+
Some(level) => Arc::new(Value::type_type(level)),
248248
None => {
249249
state.report(Message::MaximumUniverseLevelReached);
250250
Arc::new(Value::Error)
@@ -276,7 +276,7 @@ pub fn synth_type(state: &mut State<'_>, term: &Term) -> Arc<Value> {
276276

277277
match (input_level, output_level) {
278278
(Some(input_level), Some(output_level)) => {
279-
Arc::new(Value::Universe(std::cmp::max(input_level, output_level)))
279+
Arc::new(Value::TypeType(std::cmp::max(input_level, output_level)))
280280
}
281281
(_, _) => Arc::new(Value::Error),
282282
}
@@ -345,7 +345,7 @@ pub fn synth_type(state: &mut State<'_>, term: &Term) -> Arc<Value> {
345345
state.report(Message::InvalidRecordType { duplicate_labels });
346346
}
347347

348-
Arc::new(Value::Universe(max_level))
348+
Arc::new(Value::TypeType(max_level))
349349
}
350350
Term::RecordElim(head_term, label) => {
351351
let head_type = synth_type(state, head_term);

‎pikelet/src/pass/core_to_pretty.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ where
5252
),
5353
),
5454

55-
Term::Universe(level) => (alloc.nil())
55+
Term::TypeType(level) => (alloc.nil())
5656
.append("Type")
5757
.append("^")
5858
.append(alloc.as_string(level.0)),

‎pikelet/src/pass/core_to_surface.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,7 @@ pub fn from_term(state: &mut State<'_>, term: &Term) -> surface::Term<String> {
120120
Box::new(from_term(state, r#type)),
121121
),
122122

123-
Term::Universe(level) => {
123+
Term::TypeType(level) => {
124124
let universe0 = match state.globals.get("Type") {
125125
Some(_) => surface::Term::Name(0..0, "Type".to_owned()),
126126
None => surface::Term::Error(0..0), // TODO: Log error?

‎pikelet/src/pass/surface_to_core.rs

+4-4
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ pub fn is_type<S: AsRef<str>>(
157157
) -> (core::Term, Option<core::UniverseLevel>) {
158158
let (core_term, r#type) = synth_type(state, term);
159159
match r#type.force(state.globals) {
160-
Value::Universe(level) => (core_term, Some(*level)),
160+
Value::TypeType(level) => (core_term, Some(*level)),
161161
Value::Error => (core::Term::Error, None),
162162
found_type => {
163163
let found_type = state.read_back_value(&found_type);
@@ -491,7 +491,7 @@ pub fn synth_type<S: AsRef<str>>(
491491
)
492492
},
493493
),
494-
Arc::new(Value::Universe(max_level)),
494+
Arc::new(Value::TypeType(max_level)),
495495
),
496496
}
497497
}
@@ -513,7 +513,7 @@ pub fn synth_type<S: AsRef<str>>(
513513
Arc::new(core_input_type),
514514
Arc::new(core_output_type),
515515
),
516-
Arc::new(Value::Universe(std::cmp::max(input_level, output_level))),
516+
Arc::new(Value::TypeType(std::cmp::max(input_level, output_level))),
517517
),
518518
(_, _) => (core::Term::Error, Arc::new(Value::Error)),
519519
}
@@ -622,7 +622,7 @@ pub fn synth_type<S: AsRef<str>>(
622622
state.pop_many_locals(seen_labels.len());
623623
(
624624
core::Term::RecordType(core_type_entries.into()),
625-
Arc::new(Value::Universe(max_level)),
625+
Arc::new(Value::TypeType(max_level)),
626626
)
627627
}
628628
Term::RecordElim(head_term, label_range, label) => {

0 commit comments

Comments
 (0)