Adjust function naming

- argument -> input
- parameter-> input
- body -> output

Author: brendanzab

examples/prelude.pi

@@ -32,10 +32,10 @@ record {
             (a-b-c : Fun (a : A) (b : B a) -> C a b)
             -> (Fun (a : A) -> C a (a-b a)),
 
-    ||| Flip the order of the first two arguments to a function
+    ||| Flip the order of the first two inputs to a function
     flip : Fun (A B C : Type) -> (A -> B -> C) -> (B -> A -> C),
 
-    ||| Flip the order of the first two arguments to a dependent function.
+    ||| Flip the order of the first two inputs to a dependent function.
     dep-flip :
         Fun (A B : Type)
             (C : A -> B -> Type)
@@ -47,9 +47,8 @@ record {
 
     ||| Dependent substitution.
     |||
-    ||| Takes three arguments and then returns the first argument applied to the
-    ||| third, which is then applied to the result of the second argument applied to
-    ||| the third.
+    ||| Takes three inputs and then returns the first input applied to the third,
+    ||| which is then applied to the result of the second input applied to the third.
     |||
     ||| Also known as the 'S Combinator' in the [SKI combinator calculus][ski-wiki].
     |||

pikelet/src/lang/core/semantics.rs

@@ -132,9 +132,9 @@ impl Closure {
     }
 
     /// Eliminate a closure.
-    pub fn elim(&self, globals: &Globals, argument: Arc<Value>) -> Arc<Value> {
+    pub fn elim(&self, globals: &Globals, input: Arc<Value>) -> Arc<Value> {
         let mut values = self.values.clone();
-        values.push(argument);
+        values.push(input);
         eval_term(globals, self.universe_offset, &mut values, &self.term)
     }
 }
@@ -232,8 +232,8 @@ impl LazyValue {
             Some(LazyInit::ApplyElim(head, Elim::Record(label))) => {
                 apply_record_elim(head.force(globals), &label)
             }
-            Some(LazyInit::ApplyElim(head, Elim::Function(argument))) => {
-                apply_function_elim(globals, head.force(globals), argument)
+            Some(LazyInit::ApplyElim(head, Elim::Function(input))) => {
+                apply_function_elim(globals, head.force(globals), input)
             }
             None => panic!("Lazy instance has previously been poisoned"),
         })
@@ -312,21 +312,21 @@ pub fn eval_term(
             let head = eval_term(globals, universe_offset, values, head);
             apply_record_elim(&head, label)
         }
-        Term::FunctionType(param_name_hint, param_type, body_type) => {
-            let param_name_hint = param_name_hint.clone();
-            let param_type = eval_term(globals, universe_offset, values, param_type);
-            let body_type = Closure::new(universe_offset, values.clone(), body_type.clone());
-
-            Arc::new(Value::FunctionType(param_name_hint, param_type, body_type))
+        Term::FunctionType(input_name_hint, input_type, output_type) => {
+            Arc::new(Value::FunctionType(
+                input_name_hint.clone(),
+                eval_term(globals, universe_offset, values, input_type),
+                Closure::new(universe_offset, values.clone(), output_type.clone()),
+            ))
         }
-        Term::FunctionTerm(param_name, body) => Arc::new(Value::FunctionTerm(
-            param_name.clone(),
-            Closure::new(universe_offset, values.clone(), body.clone()),
+        Term::FunctionTerm(input_name, output_term) => Arc::new(Value::FunctionTerm(
+            input_name.clone(),
+            Closure::new(universe_offset, values.clone(), output_term.clone()),
         )),
-        Term::FunctionElim(head, argument) => {
+        Term::FunctionElim(head, input) => {
             let head = eval_term(globals, universe_offset, values, head);
-            let argument = LazyValue::eval_term(universe_offset, values.clone(), argument.clone());
-            apply_function_elim(globals, &head, Arc::new(argument))
+            let input = LazyValue::eval_term(universe_offset, values.clone(), input.clone());
+            apply_function_elim(globals, &head, Arc::new(input))
         }
         Term::Lift(term, offset) => {
             let universe_offset = (universe_offset + *offset).unwrap(); // FIXME: Handle overflow
@@ -379,26 +379,22 @@ fn apply_record_elim(head_value: &Value, label: &str) -> Arc<Value> {
 }
 
 /// Apply a function term elimination.
-fn apply_function_elim(
-    globals: &Globals,
-    head_value: &Value,
-    argument: Arc<LazyValue>,
-) -> Arc<Value> {
+fn apply_function_elim(globals: &Globals, head_value: &Value, input: Arc<LazyValue>) -> Arc<Value> {
     match head_value {
         Value::Stuck(head, spine) => {
             let mut spine = spine.clone(); // FIXME: Avoid clone of spine?
-            spine.push(Elim::Function(argument));
+            spine.push(Elim::Function(input));
             Arc::new(Value::Stuck(head.clone(), spine))
         }
         Value::Unstuck(head, spine, value) => {
             let mut spine = spine.clone(); // FIXME: Avoid clone of spine?
-            spine.push(Elim::Function(argument.clone()));
-            let value = LazyValue::apply_elim(value.clone(), Elim::Function(argument));
+            spine.push(Elim::Function(input.clone()));
+            let value = LazyValue::apply_elim(value.clone(), Elim::Function(input));
             Arc::new(Value::Unstuck(head.clone(), spine, Arc::new(value)))
         }
 
-        Value::FunctionTerm(_, body_closure) => {
-            body_closure.elim(globals, argument.force(globals).clone())
+        Value::FunctionTerm(_, output_closure) => {
+            output_closure.elim(globals, input.force(globals).clone())
         }
 
         _ => Arc::new(Value::Error),
@@ -430,9 +426,9 @@ fn read_back_spine(
 
     spine.iter().fold(head, |head, elim| match elim {
         Elim::Record(label) => Term::RecordElim(Arc::new(head), label.clone()),
-        Elim::Function(argument) => {
-            let argument = read_back_value(globals, local_size, unfold, argument.force(globals));
-            Term::FunctionElim(Arc::new(head), Arc::new(argument))
+        Elim::Function(input) => {
+            let input = read_back_value(globals, local_size, unfold, input.force(globals));
+            Term::FunctionElim(Arc::new(head), Arc::new(input))
         }
     })
 }
@@ -490,20 +486,22 @@ pub fn read_back_value(
 
             Term::RecordTerm(term_entries)
         }
-        Value::FunctionType(param_name_hint, param_type, body_closure) => {
+        Value::FunctionType(input_name_hint, input_type, output_closure) => {
             let local = Arc::new(Value::local(local_size.next_level()));
-            let param_type = Arc::new(read_back_value(globals, local_size, unfold, param_type));
-            let body_type = body_closure.elim(globals, local);
-            let body_type = read_back_value(globals, local_size.increment(), unfold, &body_type);
+            let input_type = Arc::new(read_back_value(globals, local_size, unfold, input_type));
+            let output_type = output_closure.elim(globals, local);
+            let output_type =
+                read_back_value(globals, local_size.increment(), unfold, &output_type);
 
-            Term::FunctionType(param_name_hint.clone(), param_type, Arc::new(body_type))
+            Term::FunctionType(input_name_hint.clone(), input_type, Arc::new(output_type))
         }
-        Value::FunctionTerm(param_name_hint, body_closure) => {
+        Value::FunctionTerm(input_name_hint, output_closure) => {
             let local = Arc::new(Value::local(local_size.next_level()));
-            let body = body_closure.elim(globals, local);
-            let body = read_back_value(globals, local_size.increment(), unfold, &body);
+            let output_term = output_closure.elim(globals, local);
+            let output_term =
+                read_back_value(globals, local_size.increment(), unfold, &output_term);
 
-            Term::FunctionTerm(param_name_hint.clone(), Arc::new(body))
+            Term::FunctionTerm(input_name_hint.clone(), Arc::new(output_term))
         }
 
         Value::Error => Term::Error,
@@ -523,11 +521,11 @@ pub fn is_equal_spine(
 
     for (elim0, elim1) in Iterator::zip(spine0.iter(), spine1.iter()) {
         match (elim0, elim1) {
-            (Elim::Function(argument0), Elim::Function(argument1)) => {
-                let argument0 = argument0.force(globals);
-                let argument1 = argument1.force(globals);
+            (Elim::Function(input0), Elim::Function(input1)) => {
+                let input0 = input0.force(globals);
+                let input1 = input1.force(globals);
 
-                if !is_equal(globals, local_size, argument0, argument1) {
+                if !is_equal(globals, local_size, input0, input1) {
                     return false;
                 }
             }
@@ -620,25 +618,29 @@ fn is_equal(globals: &Globals, local_size: LocalSize, value0: &Value, value1: &V
             )
         }
         (
-            Value::FunctionType(_, param_type0, body_closure0),
-            Value::FunctionType(_, param_type1, body_closure1),
+            Value::FunctionType(_, input_type0, output_closure0),
+            Value::FunctionType(_, input_type1, output_closure1),
         ) => {
-            if !is_equal(globals, local_size, param_type1, param_type0) {
+            if !is_equal(globals, local_size, input_type1, input_type0) {
                 return false;
             }
 
             let local = Arc::new(Value::local(local_size.next_level()));
-            let body_term0 = body_closure0.elim(globals, local.clone());
-            let body_term1 = body_closure1.elim(globals, local);
-
-            is_equal(globals, local_size.increment(), &body_term0, &body_term1)
+            is_equal(
+                globals,
+                local_size.increment(),
+                &output_closure0.elim(globals, local.clone()),
+                &output_closure1.elim(globals, local),
+            )
         }
-        (Value::FunctionTerm(_, body_closure0), Value::FunctionTerm(_, body_closure1)) => {
+        (Value::FunctionTerm(_, output_closure0), Value::FunctionTerm(_, output_closure1)) => {
             let local = Arc::new(Value::local(local_size.next_level()));
-            let body_value0 = body_closure0.elim(globals, local.clone());
-            let body_value1 = body_closure1.elim(globals, local);
-
-            is_equal(globals, local_size.increment(), &body_value0, &body_value1)
+            is_equal(
+                globals,
+                local_size.increment(),
+                &output_closure0.elim(globals, local.clone()),
+                &output_closure1.elim(globals, local),
+            )
         }
 
         // Errors are always treated as subtypes, regardless of what they are compared with.
@@ -711,18 +713,23 @@ pub fn is_subtype(
             true
         }
         (
-            Value::FunctionType(_, param_type0, body_closure0),
-            Value::FunctionType(_, param_type1, body_closure1),
+            Value::FunctionType(_, input_type0, output_closure0),
+            Value::FunctionType(_, input_type1, output_closure1),
         ) => {
-            if !is_subtype(globals, local_size, param_type1, param_type0) {
+            if !is_subtype(globals, local_size, input_type1, input_type0) {
                 return false;
             }
 
             let local = Arc::new(Value::local(local_size.next_level()));
-            let body_term0 = body_closure0.elim(globals, local.clone());
-            let body_term1 = body_closure1.elim(globals, local);
-
-            is_subtype(globals, local_size.increment(), &body_term0, &body_term1)
+            let output_term0 = output_closure0.elim(globals, local.clone());
+            let output_term1 = output_closure1.elim(globals, local);
+
+            is_subtype(
+                globals,
+                local_size.increment(),
+                &output_term0,
+                &output_term1,
+            )
         }
 
         // Errors are always treated as subtypes, regardless of what they are compared with.

pikelet/src/lang/core/typing.rs

@@ -190,13 +190,17 @@ pub fn check_type(state: &mut State<'_>, term: &Term, expected_type: &Arc<Value>
                 });
             }
         }
-        (Term::FunctionTerm(_, body), Value::FunctionType(_, param_type, body_closure)) => {
-            let param = state.push_local_param(param_type.clone());
-            check_type(state, body, &body_closure.elim(state.globals, param));
+        (
+            Term::FunctionTerm(_, output_term),
+            Value::FunctionType(_, input_type, output_closure),
+        ) => {
+            let input_term = state.push_local_param(input_type.clone());
+            let output_type = output_closure.elim(state.globals, input_term);
+            check_type(state, output_term, &output_type);
             state.pop_local();
         }
         (Term::FunctionTerm(_, _), _) => {
-            state.report(Message::TooManyParameters);
+            state.report(Message::TooManyInputsInFunctionTerm);
         }
         (term, _) => match synth_type(state, term) {
             found_type if state.is_subtype(&found_type, expected_type) => {}
@@ -304,12 +308,12 @@ pub fn synth_type(state: &mut State<'_>, term: &Term) -> Arc<Value> {
 
             Arc::new(Value::Universe(max_level))
         }
-        Term::RecordElim(head, label) => {
-            let head_type = synth_type(state, head);
+        Term::RecordElim(head_term, label) => {
+            let head_type = synth_type(state, head_term);
 
             match head_type.force(state.globals) {
                 Value::RecordType(closure) => {
-                    let head_value = state.eval_term(head);
+                    let head_value = state.eval_term(head_term);
 
                     if let Some(entry_type) = state.record_elim_type(&head_value, label, closure) {
                         return entry_type;
@@ -325,20 +329,20 @@ pub fn synth_type(state: &mut State<'_>, term: &Term) -> Arc<Value> {
             });
             Arc::new(Value::Error)
         }
-        Term::FunctionType(_, param_type, body_type) => {
-            let param_level = is_type(state, param_type);
-            let param_type = match param_level {
+        Term::FunctionType(_, input_type, output_type) => {
+            let input_level = is_type(state, input_type);
+            let input_type = match input_level {
                 None => Arc::new(Value::Error),
-                Some(_) => state.eval_term(param_type),
+                Some(_) => state.eval_term(input_type),
             };
 
-            state.push_local_param(param_type);
-            let body_level = is_type(state, body_type);
+            state.push_local_param(input_type);
+            let output_level = is_type(state, output_type);
             state.pop_local();
 
-            match (param_level, body_level) {
-                (Some(param_level), Some(body_level)) => {
-                    Arc::new(Value::Universe(std::cmp::max(param_level, body_level)))
+            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::Error),
             }
@@ -349,17 +353,17 @@ pub fn synth_type(state: &mut State<'_>, term: &Term) -> Arc<Value> {
             });
             Arc::new(Value::Error)
         }
-        Term::FunctionElim(head, argument) => {
-            let head_type = synth_type(state, head);
+        Term::FunctionElim(head_term, input_term) => {
+            let head_type = synth_type(state, head_term);
             match head_type.force(state.globals) {
-                Value::FunctionType(_, param_type, body_closure) => {
-                    check_type(state, argument, &param_type);
-                    let argument_value = state.eval_term(argument);
-                    body_closure.elim(state.globals, argument_value)
+                Value::FunctionType(_, input_type, output_closure) => {
+                    check_type(state, input_term, &input_type);
+                    let input_value = state.eval_term(input_term);
+                    output_closure.elim(state.globals, input_value)
                 }
                 Value::Error => Arc::new(Value::Error),
                 _ => {
-                    state.report(Message::TooManyArguments { head_type });
+                    state.report(Message::TooManyInputsInFunctionElim { head_type });
                     Arc::new(Value::Error)
                 }
             }

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

@@ -20,8 +20,8 @@ pub enum Message {
         expected_label: String,
         head_type: Arc<Value>,
     },
-    TooManyParameters,
-    TooManyArguments {
+    TooManyInputsInFunctionTerm,
+    TooManyInputsInFunctionElim {
         head_type: Arc<Value>,
     },
     MismatchedSequenceLength {

pikelet/src/lang/surface.rs

@@ -26,8 +26,8 @@ pub enum Literal<S> {
 pub type TypeEntry<S> = (Range<usize>, S, Option<S>, Term<S>);
 /// Entry in a [record term](Term::RecordTerm).
 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>);
+/// A group of function inputs that are elements of the same type.
+pub type InputGroup<S> = (Vec<(Range<usize>, S)>, Term<S>);
 
 /// Terms in the surface language.
 #[derive(Debug, Clone)]
@@ -51,7 +51,7 @@ pub enum Term<S> {
     /// Function types.
     ///
     /// Also known as: pi type, dependent product type.
-    FunctionType(RangeFrom<usize>, Vec<ParameterGroup<S>>, Box<Term<S>>),
+    FunctionType(RangeFrom<usize>, Vec<InputGroup<S>>, Box<Term<S>>),
     /// Arrow function types.
     ///
     /// Also known as: non-dependent function type.
@@ -94,14 +94,14 @@ impl<T> Term<T> {
             | Term::Error(range) => range.clone(),
             Term::Ann(term, r#type) => term.range().start..r#type.range().end,
             Term::RecordElim(term, label_range, _) => term.range().start..label_range.end,
-            Term::FunctionType(range, _, body_type) => range.start..body_type.range().end,
-            Term::FunctionArrowType(param_type, body_type) => {
-                param_type.range().start..body_type.range().end
+            Term::FunctionType(range, _, output_type) => range.start..output_type.range().end,
+            Term::FunctionArrowType(input_type, output_type) => {
+                input_type.range().start..output_type.range().end
             }
-            Term::FunctionTerm(range, _, body) => range.start..body.range().end,
-            Term::FunctionElim(head, arguments) => match arguments.last() {
-                Some(argument) => head.range().start..argument.range().end,
-                None => head.range(),
+            Term::FunctionTerm(range, _, output_term) => range.start..output_term.range().end,
+            Term::FunctionElim(head_term, input_terms) => match input_terms.last() {
+                Some(input_term) => head_term.range().start..input_term.range().end,
+                None => head_term.range(),
             },
         }
     }