Rename Universe to TypeType

pikelet-lang · Aug 12, 2020 · e7d2bbb · e7d2bbb
1 parent f260440
commit e7d2bbb
Show file tree

Hide file tree

Showing 8 changed files with 31 additions and 31 deletions.
diff --git a/pikelet-editor/src/lib.rs b/pikelet-editor/src/lib.rs
@@ -92,7 +92,7 @@ fn view_term<M: 'static>(term: &pikelet::lang::core::Term) -> Element<M> {
     use pikelet::lang::core::{Constant, Term, UniverseLevel, UniverseOffset};
 
     match term {
-        Term::Universe(UniverseLevel(level)) => Row::new()
+        Term::TypeType(UniverseLevel(level)) => Row::new()
             .push(Text::new(format!("Univ^{}", level))) // TODO: superscript?
             .into(),
         Term::Global(name) => Text::new(name).into(),

diff --git a/pikelet/src/lang/anf.rs b/pikelet/src/lang/anf.rs
@@ -32,7 +32,7 @@ pub enum Value {
     Ann(Box<Value>, Box<Configuration>),
 
     /// The type of types.
-    Universe(UniverseLevel),
+    TypeType(UniverseLevel),
     /// Lift a value by the given number of universe levels.
     Lift(Box<Value>, UniverseOffset),
 

diff --git a/pikelet/src/lang/core.rs b/pikelet/src/lang/core.rs
@@ -76,7 +76,7 @@ pub enum Term {
     Ann(Arc<Term>, Arc<Term>),
 
     /// The type of types.
-    Universe(UniverseLevel),
+    TypeType(UniverseLevel),
     /// Lift a term by the given number of universe levels.
     Lift(Arc<Term>, UniverseOffset),
 
@@ -113,9 +113,9 @@ pub enum Term {
 }
 
 impl Term {
-    /// Create a universe at the given level.
-    pub fn universe(level: impl Into<UniverseLevel>) -> Term {
-        Term::Universe(level.into())
+    /// Create a type of types at the given level.
+    pub fn type_type(level: impl Into<UniverseLevel>) -> Term {
+        Term::TypeType(level.into())
     }
 
     /// Create a global variable.
@@ -158,8 +158,8 @@ impl Default for Globals {
         entries.insert(
             "Type".to_owned(),
             (
-                Arc::new(Term::universe(1)),
-                Some(Arc::new(Term::universe(0))),
+                Arc::new(Term::type_type(1)),
+                Some(Arc::new(Term::type_type(0))),
             ),
         );
         entries.insert("Bool".to_owned(), (Arc::new(Term::global("Type")), None));
@@ -185,8 +185,8 @@ impl Default for Globals {
                     Arc::new(Term::Global("U32".to_owned())),
                     Arc::new(Term::FunctionType(
                         None,
-                        Arc::new(Term::universe(0)),
-                        Arc::new(Term::universe(0)),
+                        Arc::new(Term::type_type(0)),
+                        Arc::new(Term::type_type(0)),
                     )),
                 )),
                 None,
@@ -197,8 +197,8 @@ impl Default for Globals {
             (
                 Arc::new(Term::FunctionType(
                     None,
-                    Arc::new(Term::universe(0)),
-                    Arc::new(Term::universe(0)),
+                    Arc::new(Term::type_type(0)),
+                    Arc::new(Term::type_type(0)),
                 )),
                 None,
             ),

diff --git a/pikelet/src/lang/core/semantics.rs b/pikelet/src/lang/core/semantics.rs
@@ -41,7 +41,7 @@ pub enum Value {
     Unstuck(Head, Vec<Elim>, Arc<LazyValue>),
 
     /// The type of types.
-    Universe(UniverseLevel),
+    TypeType(UniverseLevel),
 
     /// Function types.
     ///
@@ -68,9 +68,9 @@ pub enum Value {
 }
 
 impl Value {
-    /// Create a universe at the given level.
-    pub fn universe(level: impl Into<UniverseLevel>) -> Value {
-        Value::Universe(level.into())
+    /// Create a type of types at the given level.
+    pub fn type_type(level: impl Into<UniverseLevel>) -> Value {
+        Value::TypeType(level.into())
     }
 
     /// Create a global variable.
@@ -286,7 +286,7 @@ pub fn eval_term(
 
         Term::Ann(term, _) => eval_term(globals, universe_offset, values, term),
 
-        Term::Universe(level) => Arc::new(Value::universe(
+        Term::TypeType(level) => Arc::new(Value::type_type(
             (*level + universe_offset).unwrap(), // FIXME: Handle overflow
         )),
         Term::Lift(term, offset) => {
@@ -458,7 +458,7 @@ pub fn read_back_value(
             Unfold::All => read_back_value(globals, local_size, unfold, value.force(globals)),
         },
 
-        Value::Universe(level) => Term::Universe(*level),
+        Value::TypeType(level) => Term::TypeType(*level),
 
         Value::FunctionType(input_name_hint, input_type, output_closure) => {
             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
             is_equal(globals, local_size, value0, value1.force(globals))
         }
 
-        (Value::Universe(level0), Value::Universe(level1)) => level0 == level1,
+        (Value::TypeType(level0), Value::TypeType(level1)) => level0 == level1,
 
         (
             Value::FunctionType(_, input_type0, output_closure0),
@@ -697,7 +697,7 @@ pub fn is_subtype(
             is_subtype(globals, local_size, value0, value1.force(globals))
         }
 
-        (Value::Universe(level0), Value::Universe(level1)) => level0 <= level1,
+        (Value::TypeType(level0), Value::TypeType(level1)) => level0 <= level1,
 
         (
             Value::FunctionType(_, input_type0, output_closure0),

diff --git a/pikelet/src/lang/core/typing.rs b/pikelet/src/lang/core/typing.rs
@@ -116,7 +116,7 @@ impl<'me> State<'me> {
 pub fn is_type(state: &mut State<'_>, term: &Term) -> Option<UniverseLevel> {
     let r#type = synth_type(state, term);
     match r#type.force(state.globals) {
-        Value::Universe(level) => Some(*level),
+        Value::TypeType(level) => Some(*level),
         Value::Error => None,
         _ => {
             state.report(Message::MismatchedTypes {
@@ -243,8 +243,8 @@ pub fn synth_type(state: &mut State<'_>, term: &Term) -> Arc<Value> {
             r#type
         }
 
-        Term::Universe(level) => match *level + UniverseOffset(1) {
-            Some(level) => Arc::new(Value::universe(level)),
+        Term::TypeType(level) => match *level + UniverseOffset(1) {
+            Some(level) => Arc::new(Value::type_type(level)),
             None => {
                 state.report(Message::MaximumUniverseLevelReached);
                 Arc::new(Value::Error)
@@ -276,7 +276,7 @@ pub fn synth_type(state: &mut State<'_>, term: &Term) -> Arc<Value> {
 
             match (input_level, output_level) {
                 (Some(input_level), Some(output_level)) => {
-                    Arc::new(Value::Universe(std::cmp::max(input_level, output_level)))
+                    Arc::new(Value::TypeType(std::cmp::max(input_level, output_level)))
                 }
                 (_, _) => Arc::new(Value::Error),
             }
@@ -345,7 +345,7 @@ pub fn synth_type(state: &mut State<'_>, term: &Term) -> Arc<Value> {
                 state.report(Message::InvalidRecordType { duplicate_labels });
             }
 
-            Arc::new(Value::Universe(max_level))
+            Arc::new(Value::TypeType(max_level))
         }
         Term::RecordElim(head_term, label) => {
             let head_type = synth_type(state, head_term);

diff --git a/pikelet/src/pass/core_to_pretty.rs b/pikelet/src/pass/core_to_pretty.rs
@@ -52,7 +52,7 @@ where
                 ),
         ),
 
-        Term::Universe(level) => (alloc.nil())
+        Term::TypeType(level) => (alloc.nil())
             .append("Type")
             .append("^")
             .append(alloc.as_string(level.0)),

diff --git a/pikelet/src/pass/core_to_surface.rs b/pikelet/src/pass/core_to_surface.rs
@@ -120,7 +120,7 @@ pub fn from_term(state: &mut State<'_>, term: &Term) -> surface::Term<String> {
             Box::new(from_term(state, r#type)),
         ),
 
-        Term::Universe(level) => {
+        Term::TypeType(level) => {
             let universe0 = match state.globals.get("Type") {
                 Some(_) => surface::Term::Name(0..0, "Type".to_owned()),
                 None => surface::Term::Error(0..0), // TODO: Log error?

diff --git a/pikelet/src/pass/surface_to_core.rs b/pikelet/src/pass/surface_to_core.rs
@@ -157,7 +157,7 @@ pub fn is_type<S: AsRef<str>>(
 ) -> (core::Term, Option<core::UniverseLevel>) {
     let (core_term, r#type) = synth_type(state, term);
     match r#type.force(state.globals) {
-        Value::Universe(level) => (core_term, Some(*level)),
+        Value::TypeType(level) => (core_term, Some(*level)),
         Value::Error => (core::Term::Error, None),
         found_type => {
             let found_type = state.read_back_value(&found_type);
@@ -491,7 +491,7 @@ pub fn synth_type<S: AsRef<str>>(
                             )
                         },
                     ),
-                    Arc::new(Value::Universe(max_level)),
+                    Arc::new(Value::TypeType(max_level)),
                 ),
             }
         }
@@ -513,7 +513,7 @@ pub fn synth_type<S: AsRef<str>>(
                         Arc::new(core_input_type),
                         Arc::new(core_output_type),
                     ),
-                    Arc::new(Value::Universe(std::cmp::max(input_level, output_level))),
+                    Arc::new(Value::TypeType(std::cmp::max(input_level, output_level))),
                 ),
                 (_, _) => (core::Term::Error, Arc::new(Value::Error)),
             }
@@ -622,7 +622,7 @@ pub fn synth_type<S: AsRef<str>>(
             state.pop_many_locals(seen_labels.len());
             (
                 core::Term::RecordType(core_type_entries.into()),
-                Arc::new(Value::Universe(max_level)),
+                Arc::new(Value::TypeType(max_level)),
             )
         }
         Term::RecordElim(head_term, label_range, label) => {