Improve doc comments

Author: brendanzab

pikelet/src/lang/core.rs

@@ -83,13 +83,21 @@ pub enum Term {
     RecordType(Arc<[(String, Arc<Term>)]>),
     /// Record terms.
     RecordTerm(BTreeMap<String, Arc<Term>>),
-    /// Record eliminations (field access).
+    /// Record eliminations.
+    ///
+    /// Also known as: record projection, field lookup.
     RecordElim(Arc<Term>, String),
     /// Function types.
+    ///
+    /// Also known as: pi type, dependent product type.
     FunctionType(Option<String>, Arc<Term>, Arc<Term>),
-    /// Function terms (lambda abstractions).
+    /// Function terms.
+    ///
+    /// Also known as: lambda abstraction, anonymous function.
     FunctionTerm(String, Arc<Term>),
-    /// Function eliminations (function application).
+    /// Function eliminations.
+    ///
+    /// Also known as: function application.
     FunctionElim(Arc<Term>, Arc<Term>),
     /// Lift a term by the given number of universe levels.
     Lift(Arc<Term>, UniverseOffset),
@@ -193,15 +201,15 @@ impl Default for Globals {
     }
 }
 
-/// An index into the local environment.
+/// A De Bruijn index into the local environment.
 #[derive(Copy, Clone, Debug, PartialEq, Eq)]
 pub struct LocalIndex(pub u32);
 
-/// An level into the local environment.
+/// A De Bruijn level into the local environment.
 #[derive(Copy, Clone, Debug, PartialEq, Eq)]
 pub struct LocalLevel(u32);
 
-/// The size of the local environment.
+/// The size of the local environment, used for index-to-level conversions.
 #[derive(Copy, Clone, Debug, PartialEq, Eq)]
 pub struct LocalSize(u32);
 

pikelet/src/lang/core/semantics.rs

@@ -51,8 +51,12 @@ pub enum Value {
     /// Record terms.
     RecordTerm(BTreeMap<String, Arc<Value>>),
     /// Function types.
+    ///
+    /// Also known as: pi type, dependent product type.
     FunctionType(Option<String>, Arc<Value>, Closure),
-    /// Function terms (lambda abstractions).
+    /// Function terms.
+    ///
+    /// Also known as: lambda abstraction, anonymous function.
     FunctionTerm(String, Closure),
 
     /// Error sentinel.
@@ -96,9 +100,13 @@ pub enum Head {
 /// An eliminator, to be used in the spine of an elimination.
 #[derive(Clone, Debug)]
 pub enum Elim {
-    /// Record eliminators (field access).
+    /// Record eliminators.
+    ///
+    /// Also known as: record projections, field lookup.
     Record(String),
-    /// Function eliminatiors (function application).
+    /// Function eliminators.
+    ///
+    /// Also known as: function application.
     Function(Arc<LazyValue>),
 }
 

pikelet/src/lang/surface.rs

@@ -29,6 +29,7 @@ pub type TermEntry<S> = (Range<usize>, S, Term<S>);
 /// A group of function parameters that are elements of the same type.
 pub type ParameterGroup<S> = (Vec<(Range<usize>, S)>, Term<S>);
 
+/// Terms in the surface language.
 #[derive(Debug, Clone)]
 pub enum Term<S> {
     /// Names.
@@ -43,15 +44,25 @@ pub enum Term<S> {
     RecordType(Range<usize>, Vec<TypeEntry<S>>),
     /// Record terms.
     RecordTerm(Range<usize>, Vec<TermEntry<S>>),
-    /// Record eliminations (field access).
+    /// Record eliminations.
+    ///
+    /// Also known as: record projections, field lookup.
     RecordElim(Box<Term<S>>, Range<usize>, S),
     /// Function types.
+    ///
+    /// Also known as: pi type, dependent product type.
     FunctionType(RangeFrom<usize>, Vec<ParameterGroup<S>>, Box<Term<S>>),
     /// Arrow function types.
+    ///
+    /// Also known as: non-dependent function type.
     FunctionArrowType(Box<Term<S>>, Box<Term<S>>),
-    /// Function terms (lambda abstractions).
+    /// Function terms.
+    ///
+    /// Also known as: lambda abstraction, anonymous function.
     FunctionTerm(RangeFrom<usize>, Vec<(Range<usize>, S)>, Box<Term<S>>),
-    /// Function eliminations (function application).
+    /// Function eliminations.
+    ///
+    /// Also known as: function application.
     FunctionElim(Box<Term<S>>, Vec<Term<S>>),
     /// Lift a term by the given number of universe levels.
     Lift(Range<usize>, Box<Term<S>>, u32),