Implement generalization

examples/infinite_recursion.g

@@ -1,2 +1,2 @@
-f = x => f x
+f = (x : bool) => f x
 f true

examples/infinite_type.g

@@ -1,3 +1,3 @@
 t = int -> t
-f : t = x => f
+f : t = (x : int) => f
 f 1 2 3

src/de_bruijn.rs

@@ -6,11 +6,7 @@ use crate::term::{
         Quotient, Sum, True, Type, Unifier, Variable,
     },
 };
-use std::{
-    cmp::{min, Ordering},
-    convert::TryFrom,
-    rc::Rc,
-};
+use std::{cmp::Ordering, convert::TryFrom, rc::Rc};
 
 // Shifting refers to adjusting the De Bruijn indices of free variables. A cutoff determines which
 // variables are considered free. This function is used to raise or lower a term into a different
@@ -23,25 +19,27 @@ pub fn signed_shift<'a>(term: &Term<'a>, cutoff: usize, amount: isize) -> Option
             // We `clone` the borrowed `subterm` to avoid holding the dynamic borrow for too long.
             let borrow = { subterm.borrow().clone() };
 
-            match borrow {
-                Ok(subterm) => {
-                    signed_shift(
-                        // The `unwrap` is safe due to [ref:unifier_shifts_valid].
-                        &signed_shift(&subterm, 0, *subterm_shift).unwrap(),
-                        cutoff,
-                        amount,
-                    )
-                }
-                Err(min_shift) => {
-                    let new_shift = subterm_shift + amount;
-
-                    *subterm.borrow_mut() = Err(min(min_shift, new_shift));
+            if let Some(subterm) = borrow {
+                signed_shift(&unsigned_shift(&subterm, 0, *subterm_shift), cutoff, amount)
+            } else if *subterm_shift >= cutoff {
+                // This `unwrap` is "virtually safe", unless the conversion overflows.
+                let signed_subterm_shift = isize::try_from(*subterm_shift).unwrap();
 
+                // Adjust the shift if it results in a non-negative quantity.
+                if signed_subterm_shift >= -amount {
                     Some(Term {
                         source_range: term.source_range,
-                        variant: Unifier(subterm.clone(), new_shift),
+                        variant: Unifier(
+                            subterm.clone(),
+                            // This `unwrap` is safe due to the check above.
+                            usize::try_from(signed_subterm_shift + amount).unwrap(),
+                        ),
                     })
+                } else {
+                    None
                 }
+            } else {
+                Some(term.clone())
             }
         }
         Type | Integer | IntegerLiteral(_) | Boolean | True | False => Some(term.clone()),
@@ -189,8 +187,8 @@ pub fn signed_shift<'a>(term: &Term<'a>, cutoff: usize, amount: isize) -> Option
 // is total.
 pub fn unsigned_shift<'a>(term: &Term<'a>, cutoff: usize, amount: usize) -> Term<'a> {
     // The inner `unwrap` is "essentially safe" in that it can only fail in the virtually
-    // impossible case of the conversion overflowing. The outer `unwrap` is safe due to
-    // [ref:unifier_shifts_valid].
+    // impossible case of the conversion overflowing. The outer `unwrap` is safe because `amount`
+    // is non-negative.
     signed_shift(term, cutoff, isize::try_from(amount).unwrap()).unwrap()
 }
 
@@ -211,16 +209,15 @@ pub fn open<'a>(
             // We `clone` the borrowed `subterm` to avoid holding the dynamic borrow for too long.
             let borrow = { subterm.borrow().clone() };
 
-            if let Ok(subterm) = borrow {
+            if let Some(subterm) = borrow {
                 open(
-                    // The `unwrap` is safe due to [ref:unifier_shifts_valid].
-                    &signed_shift(&subterm, 0, *subterm_shift).unwrap(),
+                    &unsigned_shift(&subterm, 0, *subterm_shift),
                     index_to_replace,
                     term_to_insert,
                     shift_amount,
                 )
             } else {
-                // The `unwrap` is safe because shifting an unresolved unifier is always safe.
+                // The `unwrap` is NOT justified!
                 signed_shift(term_to_open, 0, -1).unwrap()
             }
         }
@@ -431,31 +428,46 @@ mod tests {
     use std::{cell::RefCell, rc::Rc};
 
     #[test]
-    fn signed_shift_unifier_none() {
+    fn signed_shift_unifier_none_valid() {
         assert_same!(
             signed_shift(
                 &Term {
                     source_range: None,
-                    variant: Unifier(Rc::new(RefCell::new(Err(0))), 0),
+                    variant: Unifier(Rc::new(RefCell::new(None)), 10),
                 },
                 0,
-                -42,
+                -4,
             ),
             Some(Term {
                 source_range: None,
-                variant: Unifier(Rc::new(RefCell::new(Err(-42))), -42),
+                variant: Unifier(Rc::new(RefCell::new(None)), 6),
             }),
         );
     }
 
+    #[test]
+    fn signed_shift_unifier_none_invalid() {
+        assert_same!(
+            signed_shift(
+                &Term {
+                    source_range: None,
+                    variant: Unifier(Rc::new(RefCell::new(None)), 0),
+                },
+                0,
+                -42,
+            ),
+            None,
+        );
+    }
+
     #[test]
     fn signed_shift_unifier_some() {
         assert_same!(
             signed_shift(
                 &Term {
                     source_range: None,
                     variant: Unifier(
-                        Rc::new(RefCell::new(Ok(Term {
+                        Rc::new(RefCell::new(Some(Term {
                             source_range: None,
                             variant: Variable("x", 10),
                         }))),
@@ -529,14 +541,14 @@ mod tests {
             unsigned_shift(
                 &Term {
                     source_range: None,
-                    variant: Unifier(Rc::new(RefCell::new(Err(0))), 0),
+                    variant: Unifier(Rc::new(RefCell::new(None)), 0),
                 },
                 0,
                 42,
             ),
             Term {
                 source_range: None,
-                variant: Unifier(Rc::new(RefCell::new(Err(0))), 42),
+                variant: Unifier(Rc::new(RefCell::new(None)), 42),
             },
         );
     }
@@ -548,7 +560,7 @@ mod tests {
                 &Term {
                     source_range: None,
                     variant: Unifier(
-                        Rc::new(RefCell::new(Ok(Term {
+                        Rc::new(RefCell::new(Some(Term {
                             source_range: None,
                             variant: Variable("x", 0),
                         }))),
@@ -1299,7 +1311,7 @@ mod tests {
             open(
                 &Term {
                     source_range: None,
-                    variant: Unifier(Rc::new(RefCell::new(Err(0))), 0),
+                    variant: Unifier(Rc::new(RefCell::new(None)), 10),
                 },
                 0,
                 &Term {
@@ -1310,7 +1322,7 @@ mod tests {
             ),
             Term {
                 source_range: None,
-                variant: Unifier(Rc::new(RefCell::new(Err(-1))), -1),
+                variant: Unifier(Rc::new(RefCell::new(None)), 9),
             },
         );
     }
@@ -1322,7 +1334,7 @@ mod tests {
                 &Term {
                     source_range: None,
                     variant: Unifier(
-                        Rc::new(RefCell::new(Ok(Term {
+                        Rc::new(RefCell::new(Some(Term {
                             source_range: None,
                             variant: Variable("x", 0),
                         }))),

src/equality.rs

@@ -1,5 +1,5 @@
 use crate::{
-    de_bruijn::signed_shift,
+    de_bruijn::unsigned_shift,
     term::{
         Term,
         Variant::{
@@ -20,16 +20,8 @@ pub fn syntactically_equal<'a>(term1: &Term<'a>, term2: &Term<'a>) -> bool {
     loop {
         term1 = if let Unifier(subterm, subterm_shift) = &term1.variant {
             // We `clone` the borrowed `subterm` to avoid holding the dynamic borrow for too long.
-            let borrow = { subterm.borrow().clone() };
-
-            if let Ok(subterm) = borrow {
-                if let Some(shifted_term) = signed_shift(&subterm, 0, *subterm_shift) {
-                    shifted_term
-                } else {
-                    // The `signed_shift` failed. This means the term is malformed. The error will
-                    // be reported during type checking.
-                    return false;
-                }
+            if let Some(subterm) = { subterm.borrow().clone() } {
+                unsigned_shift(&subterm, 0, *subterm_shift)
             } else {
                 break;
             }
@@ -43,16 +35,8 @@ pub fn syntactically_equal<'a>(term1: &Term<'a>, term2: &Term<'a>) -> bool {
     loop {
         term2 = if let Unifier(subterm, subterm_shift) = &term2.variant {
             // We `clone` the borrowed `subterm` to avoid holding the dynamic borrow for too long.
-            let borrow = { subterm.borrow().clone() };
-
-            if let Ok(subterm) = borrow {
-                if let Some(shifted_term) = signed_shift(&subterm, 0, *subterm_shift) {
-                    shifted_term
-                } else {
-                    // The `signed_shift` failed. This means the term is malformed. The error will
-                    // be reported during type checking.
-                    return false;
-                }
+            if let Some(subterm) = { subterm.borrow().clone() } {
+                unsigned_shift(&subterm, 0, *subterm_shift)
             } else {
                 break;
             }
@@ -177,7 +161,7 @@ mod tests {
         let term1 = Term {
             source_range: None,
             variant: Unifier(
-                Rc::new(RefCell::new(Ok(Term {
+                Rc::new(RefCell::new(Some(Term {
                     source_range: None,
                     variant: Variable("x", 0),
                 }))),
@@ -203,7 +187,7 @@ mod tests {
         let term2 = Term {
             source_range: None,
             variant: Unifier(
-                Rc::new(RefCell::new(Ok(Term {
+                Rc::new(RefCell::new(Some(Term {
                     source_range: None,
                     variant: Variable("x", 0),
                 }))),
@@ -216,7 +200,7 @@ mod tests {
 
     #[test]
     fn syntactically_equal_unifier_same_pointer_same_shift() {
-        let rc = Rc::new(RefCell::new(Err(0)));
+        let rc = Rc::new(RefCell::new(None));
 
         let term1 = Term {
             source_range: None,
@@ -233,7 +217,7 @@ mod tests {
 
     #[test]
     fn syntactically_inequal_unifier_same_pointer_different_shift() {
-        let rc = Rc::new(RefCell::new(Err(0)));
+        let rc = Rc::new(RefCell::new(None));
 
         let term1 = Term {
             source_range: None,
@@ -252,12 +236,12 @@ mod tests {
     fn syntactically_inequal_unifier_different_pointer_same_shift() {
         let term1 = Term {
             source_range: None,
-            variant: Unifier(Rc::new(RefCell::new(Err(0))), 5),
+            variant: Unifier(Rc::new(RefCell::new(None)), 5),
         };
 
         let term2 = Term {
             source_range: None,
-            variant: Unifier(Rc::new(RefCell::new(Err(0))), 5),
+            variant: Unifier(Rc::new(RefCell::new(None)), 5),
         };
 
         assert!(!syntactically_equal(&term1, &term2));

src/evaluator.rs

@@ -1,5 +1,5 @@
 use crate::{
-    de_bruijn::{open, signed_shift, unsigned_shift},
+    de_bruijn::{open, unsigned_shift},
     error::Error,
     format::CodeStr,
     term::{
@@ -48,13 +48,9 @@ pub fn step<'a>(term: &Term<'a>) -> Option<Term<'a>> {
         | True
         | False => None,
         Unifier(subterm, subterm_shift) => {
-            // We `clone` the borrowed `subterm` to avoid holding the dynamic borrow for too long.
-            let borrow = { subterm.borrow().clone() };
-
-            // If the unifier points to something, step to it. Otherwise, we're stuck.
-            borrow
-                .ok()
-                .and_then(|subterm| signed_shift(&subterm, 0, *subterm_shift))
+            // If the unifier points to something, step to it. Otherwise, we're stuck. We `clone`
+            // the borrowed `subterm` to avoid holding the dynamic borrow for too long.
+            { subterm.borrow().clone() }.map(|subterm| unsigned_shift(&subterm, 0, *subterm_shift))
         }
         Application(applicand, argument) => {
             // Try to step the applicand.

src/main.rs

@@ -161,7 +161,7 @@ fn run(source_path: &Path, check_only: bool) -> Result<(), Error> {
     // Type check the term.
     let mut typing_context = vec![];
     let mut definitions_context = vec![];
-    let _ = type_check(
+    let (elaborated_term, elaborated_type) = type_check(
         Some(source_path),
         &source_contents,
         &term,
@@ -170,9 +170,18 @@ fn run(source_path: &Path, check_only: bool) -> Result<(), Error> {
     )
     .map_err(collect_errors)?;
 
-    // Evaluate the term.
-    if !check_only {
-        let value = evaluate(&term)?;
+    // Evaluate the term if applicable.
+    if check_only {
+        println!(
+            "Elaborated term:\n\n{}",
+            elaborated_term.to_string().code_str(),
+        );
+        println!(
+            "\nElaborated type:\n\n{}",
+            elaborated_type.to_string().code_str(),
+        );
+    } else {
+        let value = evaluate(&elaborated_term)?;
         println!("{}", value.to_string().code_str());
     }
 

src/normalizer.rs

@@ -1,5 +1,5 @@
 use crate::{
-    de_bruijn::{open, signed_shift, unsigned_shift},
+    de_bruijn::{open, unsigned_shift},
     term::{
         Term,
         Variant::{
@@ -35,12 +35,11 @@ pub fn normalize_weak_head<'a>(
             let borrow = { subterm.borrow().clone() };
 
             // If the unifier points to something, normalize it. Otherwise, we're stuck.
-            if let Ok(subterm) = borrow {
-                if let Some(subterm) = signed_shift(&subterm, 0, *subterm_shift) {
-                    normalize_weak_head(&subterm, definitions_context)
-                } else {
-                    term.clone()
-                }
+            if let Some(subterm) = borrow {
+                normalize_weak_head(
+                    &unsigned_shift(&subterm, 0, *subterm_shift),
+                    definitions_context,
+                )
             } else {
                 term.clone()
             }