better naming for the typecheck functions

src/cli.rs

@@ -57,7 +57,7 @@ pub fn cli() -> rustyline::Result<()> {
         };
         let parse_duration = start.elapsed();
         let start = Instant::now();
-        let typed = match parsed.typecheck2(t) {
+        let typed = match parsed.global_typecheck(t) {
             Ok(t) => t,
             Err(e) => {
                 print!("type error: ");

src/compile.rs

@@ -192,7 +192,7 @@ pub fn compile() {
     let mut t = Typer::new();
     let t = &mut t;
     let i = parse(p1, t).unwrap();
-    let i = match i.typecheck2(t) {
+    let i = match i.global_typecheck(t) {
         Ok(i) => i,
         Err(e) => {
             print!("type error: ");

src/ir/gen.rs

@@ -68,7 +68,7 @@ pub fn generate_terms(reps: usize, t: &mut Typer) -> Vec<Expr<TypeRef>> {
         let t2: Vec<_> = t0
             .into_iter()
             .chain(t1.into_iter())
-            .map(|e| (e.typecheck(&mut Context::new(), &mut Context::new(), t), e))
+            .map(|e| (e.local_typecheck(&mut Context::new(), &mut Context::new(), t), e))
             .collect();
 
         terms = HashSet::new();
@@ -92,6 +92,6 @@ pub fn generate_terms(reps: usize, t: &mut Typer) -> Vec<Expr<TypeRef>> {
 
     terms
         .into_iter()
-        .filter_map(|e| e.typecheck2(t).ok())
+        .filter_map(|e| e.global_typecheck(t).ok())
         .collect()
 }

src/ir/mod.rs

@@ -745,15 +745,15 @@ impl Typed for Expr<TypeRef> {
 }
 
 impl Type {
-    fn typecheck(&self, typs: &mut Context<()>) -> Result<(), TypeErrors<()>> {
+    fn local_typecheck(&self, typs: &mut Context<()>) -> Result<(), TypeErrors<()>> {
         match self {
             Type::Fun(_, i, o) => {
-                let i = i.typecheck(typs);
-                let o = o.typecheck(typs);
+                let i = i.local_typecheck(typs);
+                let o = o.local_typecheck(typs);
                 merge_ty_error!(i, o);
                 Ok(())
             }
-            Type::ForAll(t) => typs.with((), |typs| t.typecheck(typs)),
+            Type::ForAll(t) => typs.with((), |typs| t.local_typecheck(typs)),
             Type::Var(typvar) => match typs.lookup(typvar.0) {
                 Some(_) => Ok(()),
                 None => Err(TypeErrorKind::UnknownTypeVar.with(()))?,
@@ -822,15 +822,15 @@ pub struct Binding {
 }
 
 impl<T: Clone> Expr<T> {
-    pub fn typecheck2(&self, t: &mut Typer) -> Result<Expr<TypeRef>, TypeErrors<T>> {
+    pub fn global_typecheck(&self, t: &mut Typer) -> Result<Expr<TypeRef>, TypeErrors<T>> {
         let mut vars = Context::new();
         let mut typs = Context::new();
-        let tc = self.typecheck(&mut vars, &mut typs, t)?;
+        let tc = self.local_typecheck(&mut vars, &mut typs, t)?;
         assert!(vars.ctx.is_empty());
         assert!(typs.ctx.is_empty());
         Ok(tc)
     }
-    pub fn typecheck(
+    pub fn local_typecheck(
         &self,
         vars: &mut Context<Binding>,
         typs: &mut Context<()>,
@@ -847,12 +847,12 @@ impl<T: Clone> Expr<T> {
             },
             ExprNode::Abs(abs) => {
                 abs.arg_ty
-                    .typecheck(typs)
+                    .local_typecheck(typs)
                     .map_err(|t| t.with(self.data.clone()))?;
 
                 if let Some(ret_ty) = abs.ret_ty {
                     ret_ty
-                        .typecheck(typs)
+                        .local_typecheck(typs)
                         .map_err(|t| t.with(self.data.clone()))?;
                 }
 
@@ -864,7 +864,7 @@ impl<T: Clone> Expr<T> {
                         ctx_mul: abs.mul,
                     },
                     |vars| -> Result<Expr<TypeRef>, TypeErrors<T>> {
-                        let body = abs.body.typecheck(vars, typs, t)?;
+                        let body = abs.body.local_typecheck(vars, typs, t)?;
 
                         let v = vars.lookup(0).unwrap();
 
@@ -904,7 +904,7 @@ impl<T: Clone> Expr<T> {
                 }
             }
             ExprNode::App(fun0, arg0) => {
-                let fun = fun0.typecheck(vars, typs, t)?;
+                let fun = fun0.local_typecheck(vars, typs, t)?;
 
                 let Type::Fun(mul, in_ty, out_ty) = *fun.data else {
                     return Err(TypeErrorKind::ExpectedFunction { actual: fun.data }
@@ -919,7 +919,7 @@ impl<T: Clone> Expr<T> {
                 });
 
                 // typecheck with new multiplicities
-                let arg = arg0.typecheck(&mut vars2, typs, t)?;
+                let arg = arg0.local_typecheck(&mut vars2, typs, t)?;
 
                 // check that the effective multiplicities haven't been violated
                 for var in vars2.iter() {
@@ -971,7 +971,7 @@ impl<T: Clone> Expr<T> {
             ExprNode::TAbs(expr) => {
                 let mut vars2 = vars.clone();
                 vars2.map(|var| var.ty = var.ty.lift(t, 0, 1));
-                let expr = typs.with((), |typs| expr.typecheck(&mut vars2, typs, t))?;
+                let expr = typs.with((), |typs| expr.local_typecheck(&mut vars2, typs, t))?;
                 vars.merge(&vars2, |v1, v2| {
                     v1.refs += v2.refs;
                 });
@@ -982,9 +982,9 @@ impl<T: Clone> Expr<T> {
                 }
             }
             ExprNode::TApp(expr0, ty_arg) => {
-                let expr = expr0.typecheck(vars, typs, t)?;
+                let expr = expr0.local_typecheck(vars, typs, t)?;
                 ty_arg
-                    .typecheck(typs)
+                    .local_typecheck(typs)
                     .map_err(|e| e.with(self.data.clone()))?;
 
                 let Type::ForAll(_) = expr.data else {

src/ir/test.rs

@@ -23,7 +23,7 @@ fn typecheck(src: &str, expect_fail: bool) {
     println!("source: {src}");
     let fun = parse(src, &mut t).unwrap();
     println!("parsed: {}", fun.node);
-    match fun.typecheck2(&mut t) {
+    match fun.global_typecheck(&mut t) {
         Ok(_fun) => {
             println!("type: {}", _fun.data);
             assert!(!format!(