make 'bound variable exceeded' error non-fatal

mm0-rs/components/mm0_util/src/lib.rs

@@ -522,7 +522,7 @@ impl From<PathBuf> for FileRef {
 impl From<lsp_types::Uri> for FileRef {
   fn from(uri: lsp_types::Uri) -> FileRef {
     fn to_file_path(uri: &lsp_types::Uri) -> Option<PathBuf> {
-      if uri.scheme()?.as_str() != "file" || uri.authority().is_some() { return None }
+      if uri.scheme()?.as_str() != "file" || !uri.authority()?.as_str().is_empty() { return None }
       Some(PathBuf::from(uri.path().as_str()))
     }
     #[cfg(not(target_arch = "wasm32"))]

mm0-rs/src/elab/environment.rs

@@ -7,6 +7,7 @@ use std::fmt::Write;
 use std::collections::HashMap;
 use debug_derive::EnvDebug;
 #[cfg(feature = "memory")] use mm0_deepsize_derive::DeepSizeOf;
+use mm0b_parser::MAX_BOUND_VARS;
 use super::{BoxError, ElabError, FrozenEnv, FrozenLispVal, spans::Spans, verify::VERIFY_ON_ADD};
 use crate::{ArcString, AtomId, AtomVec, DocComment, FileRef, FileSpan, HashMapExt, Modifiers,
   Prec, SortId, SortVec, Span, TermId, TermVec, ThmId, ThmVec,
@@ -1161,9 +1162,34 @@ pub enum AddItemError<A> {
   Verify(String),
 }
 
+/// Non-fatal errors produced by add item functions.
+#[allow(missing_copy_implementations)]
+#[derive(Debug)]
+pub enum AddItemNonFatalError {
+  /// The declaration used more bound variables than the verifier supports
+  MaxBoundVars,
+}
+
+impl AddItemNonFatalError {
+  fn from_verify_err(e: &VerifyError<'_>) -> Option<Self> {
+    match e {
+      VerifyError::MaxBoundVars => Some(Self::MaxBoundVars),
+      _ => None
+    }
+  }
+
+  /// Convert this error into an [`ElabError`] at the provided location.
+  #[must_use] pub fn into_elab_error(self, sp: Span) -> ElabError {
+    match self {
+      Self::MaxBoundVars =>
+        ElabError::new_e(sp, format!("too many bound variables (max {MAX_BOUND_VARS})")),
+    }
+  }
+}
+
 /// Most add item functions return [`AddItemError`]`<Option<A>>`, meaning that in the
 /// redeclaration case they can still return an `A`, namely the ID of the old declaration
-type AddItemResult<A> = Result<A, AddItemError<Option<A>>>;
+type AddItemResult<A> = Result<(A, Option<AddItemNonFatalError>), AddItemError<Option<A>>>;
 
 impl<A> AddItemError<A> {
   /// Convert this error into an [`ElabError`] at the provided location.
@@ -1229,7 +1255,7 @@ impl Environment {
       let (res, sp) = match key {
         DeclKey::Term(old_id) => {
           let sp = &self.terms[old_id].span;
-          if *sp == *new { return Ok(old_id) }
+          if *sp == *new { return Ok((old_id, None)) }
           (Some(old_id), sp)
         }
         DeclKey::Thm(old_id) => (None, &self.thms[old_id].span)
@@ -1241,20 +1267,24 @@ impl Environment {
       }))
     } else {
       let t = t();
+      let mut err = None;
       if verify {
         match self.verify_termdef(&Default::default(), &t) {
           Ok(()) | Err(VerifyError::UsesSorry) => {}
           Err(e) => {
-            let mut msg = format!("while adding {}: ", data.name);
-            e.render(self, &mut msg).expect("impossible");
-            return Err(AddItemError::Verify(msg))
+            err = AddItemNonFatalError::from_verify_err(&e);
+            if err.is_none() {
+              let mut msg = format!("while adding {}: ", data.name);
+              e.render(self, &mut msg).expect("impossible");
+              return Err(AddItemError::Verify(msg))
+            }
           }
         }
       }
       self.data[a].decl = Some(DeclKey::Term(new_id));
       self.terms.push(t);
       self.stmts.push(StmtTrace::Decl(a));
-      Ok(new_id)
+      Ok((new_id, err))
     }
   }
 
@@ -1273,7 +1303,7 @@ impl Environment {
       let (res, sp) = match key {
         DeclKey::Thm(old_id) => {
           let sp = &self.thms[old_id].span;
-          if *sp == *new { return Ok(old_id) }
+          if *sp == *new { return Ok((old_id, None)) }
           (Some(old_id), sp)
         }
         DeclKey::Term(old_id) => (None, &self.terms[old_id].span)
@@ -1285,20 +1315,24 @@ impl Environment {
       }))
     } else {
       let t = t();
+      let mut err = None;
       if verify {
         match self.verify_thmdef(&Default::default(), &t) {
           Ok(()) | Err(VerifyError::UsesSorry) => {}
           Err(e) => {
-            let mut msg = format!("while adding {}: ", data.name);
-            e.render(self, &mut msg).expect("impossible");
-            return Err(AddItemError::Verify(msg))
+            err = AddItemNonFatalError::from_verify_err(&e);
+            if err.is_none() {
+              let mut msg = format!("while adding {}: ", data.name);
+              e.render(self, &mut msg).expect("impossible");
+              return Err(AddItemError::Verify(msg))
+            }
           }
         }
       }
       self.data[a].decl = Some(DeclKey::Thm(new_id));
       self.thms.push(t);
       self.stmts.push(StmtTrace::Decl(a));
-      Ok(new_id)
+      Ok((new_id, err))
     }
   }
 
@@ -1369,7 +1403,10 @@ impl Environment {
         DeclKey::Term(tid) => {
           let otd: &Term = other.term(tid);
           let id = match self.try_add_term(false, a.remap(remap), &otd.span, || otd.remap(remap)) {
-            Ok(id) => id,
+            Ok((id, err)) => {
+              if let Some(e) = err { errors.push(e.into_elab_error(sp)) }
+              id
+            }
             Err(AddItemError::Redeclaration(id, r)) => {
               let e = ElabError::with_info(sp, r.msg.into(), vec![
                 (otd.span.clone(), r.othermsg.clone().into()),
@@ -1385,7 +1422,10 @@ impl Environment {
         DeclKey::Thm(tid) => {
           let otd: &Thm = other.thm(tid);
           let id = match self.try_add_thm(false, a.remap(remap), &otd.span, || otd.remap(remap)) {
-            Ok(id) => id,
+            Ok((id, err)) => {
+              if let Some(e) = err { errors.push(e.into_elab_error(sp)) }
+              id
+            }
             Err(AddItemError::Redeclaration(id, r)) => {
               let e = ElabError::with_info(sp, r.msg.into(), vec![
                 (otd.span.clone(), r.othermsg.clone().into()),

mm0-rs/src/elab/local_context.rs

@@ -908,7 +908,8 @@ impl Elaborator {
           full,
         };
         if atom != AtomId::UNDER {
-          let tid = self.env.add_term(t).map_err(|e| e.into_elab_error(d.id))?;
+          let (tid, err) = self.env.add_term(t).map_err(|e| e.into_elab_error(d.id))?;
+          if let Some(e) = err { self.report(e.into_elab_error(d.id)) }
           self.spans.insert(d.id, ObjectKind::Term(true, tid));
         } else if VERIFY_ON_ADD {
           match self.env.verify_termdef(&Default::default(), &t) {
@@ -1024,7 +1025,8 @@ impl Elaborator {
           args: args.into(), heap, store: store.into(), hyps, ret, kind
         };
         if atom != AtomId::UNDER {
-          let tid = self.env.add_thm(t).map_err(|e| e.into_elab_error(d.id))?;
+          let (tid, err) = self.env.add_thm(t).map_err(|e| e.into_elab_error(d.id))?;
+          if let Some(e) = err { self.report(e.into_elab_error(d.id)) }
           self.spans.insert(d.id, ObjectKind::Thm(true, tid));
         } else if VERIFY_ON_ADD {
           match self.verify_thmdef(&Default::default(), &t) {

mm0-rs/src/elab/verify.rs

@@ -213,7 +213,8 @@ impl VerifyError<'_> {
         "theorem {} was referenced before it was declared", env.data[env.thms[t].atom].name),
       VerifyError::DepsOutOfBounds => write!(w,
         "A variable depends on a bound variable which has not yet been declared."),
-      VerifyError::MaxBoundVars => write!(w, "Maximum number of bound variables exceeded"),
+      VerifyError::MaxBoundVars => write!(w,
+        "Maximum number of bound variables exceeded (max {MAX_BOUND_VARS})"),
       VerifyError::BoundInStrictSort => write!(w, "Bound variable declared in a `strict` sort"),
       VerifyError::DummyInFreeSort => write!(w, "Dummy variable declared in a `free` sort"),
       VerifyError::TermInPureSort => write!(w, "Term declared in a `pure` sort"),

mm0-rs/src/mmc/proof/assembler.rs

@@ -1370,15 +1370,15 @@ impl<'a> BuildAssembly<'a> {
     };
 
     let (code, doc) = self.mangler.get_data(self.elab, Name::ProcContent(proc.name()));
-    let code = self.elab.env.add_term({
+    let (code, _) = self.elab.env.add_term({
       let mut de = ExprDedup::new(self.pd, &[]);
       let e = build.thm.to_expr(&mut de, s);
       de.build_def0(code, Modifiers::LOCAL,
         self.span.clone(), self.full, Some(doc), e, self.pd.string)
     }).map_err(|e| e.into_elab_error(self.full))?;
 
     let (asm, doc) = self.mangler.get_data(self.elab, Name::ProcAsm(proc.name()));
-    let asm = self.elab.env.add_term({
+    let (asm, _) = self.elab.env.add_term({
       let mut de = ExprDedup::new(self.pd, &[]);
       let e = build.thm.to_expr(&mut de, a);
       de.build_def0(asm, Modifiers::LOCAL,
@@ -1388,7 +1388,7 @@ impl<'a> BuildAssembly<'a> {
     let th = thm!(build.thm, ((assemble ({code}) start end (asmProc start ({asm})))) =>
       CONV({th} => (assemble (UNFOLD({code}); s) start end (asmProc start (UNFOLD({asm}); a)))));
     let (asm_thm, doc) = self.mangler.get_data(self.elab, Name::ProcAsmThm(proc.name()));
-    let asm_thm = self.elab.env
+    let (asm_thm, _) = self.elab.env
       .add_thm(build.thm.build_thm0(asm_thm, Modifiers::empty(),
         self.span.clone(), self.full, Some(doc), th))
       .map_err(|e| e.into_elab_error(self.full))?;
@@ -1421,15 +1421,15 @@ impl<'a> BuildAssembly<'a> {
       assembledI(a, res, c, *end, filesz, memsz, h1, h2, h3, h4));
 
     let (content, doc) = self.mangler.get_data(self.elab, Name::Content);
-    let content = self.elab.env.add_term({
+    let (content, _) = self.elab.env.add_term({
       let mut de = ExprDedup::new(self.pd, &[]);
       let e = self.thm.to_expr(&mut de, c);
       de.build_def0(content, Modifiers::LOCAL,
         self.span.clone(), self.full, Some(doc), e, self.pd.string)
     }).map_err(|e| e.into_elab_error(self.full))?;
 
     let (gctx, doc) = self.mangler.get_data(self.elab, Name::GCtx);
-    let gctx = self.elab.env.add_term({
+    let (gctx, _) = self.elab.env.add_term({
       let mut de = ExprDedup::new(self.pd, &[]);
       let filesz = self.thm.to_expr(&mut de, filesz);
       let memsz = self.thm.to_expr(&mut de, memsz);
@@ -1443,7 +1443,7 @@ impl<'a> BuildAssembly<'a> {
       CONV({th} => (assembled (UNFOLD({gctx});
         (mkGCtx (UNFOLD({content}); c) filesz memsz res)) a)));
     let (asmd_thm, doc) = self.mangler.get_data(self.elab, Name::AsmdThm);
-    let asmd_thm = self.elab.env
+    let (asmd_thm, _) = self.elab.env
       .add_thm(self.thm.build_thm0(asmd_thm, Modifiers::empty(),
         self.span.clone(), self.full, Some(doc), th))
       .map_err(|e| e.into_elab_error(self.full))?;
@@ -1460,10 +1460,11 @@ impl<'a> BuildAssembly<'a> {
     let th = mk_proof(self, &mut de).1;
     let (lem, doc) = self.mangler.get_data(self.elab, Name::AsmdThmLemma(self.asmd_lemmas));
     self.asmd_lemmas += 1;
-    self.elab.env
+    let (lem, _) = self.elab.env
       .add_thm(de.build_thm0(lem, Modifiers::empty(),
         self.span.clone(), self.full, Some(doc), th))
-      .map_err(|e| e.into_elab_error(self.full))
+      .map_err(|e| e.into_elab_error(self.full))?;
+    Ok(lem)
   }
 
   fn prove_conjuncts(&mut self,
@@ -1478,7 +1479,7 @@ impl<'a> BuildAssembly<'a> {
       match item {
         AssemblyItem::Proc(proc) => {
           let (asmd_thm, doc) = self.mangler.get_data(self.elab, Name::ProcAsmdThm(proc.name()));
-          let asmd_thm = self.elab.env
+          let (asmd_thm, _) = self.elab.env
             .add_thm(de.build_thm0(asmd_thm, Modifiers::empty(),
               self.span.clone(), self.full, Some(doc), th))
             .map_err(|e| e.into_elab_error(self.full))?;

mm0-rs/src/mmc/proof/compiler.rs

@@ -1672,7 +1672,7 @@ pub(super) fn compile_proof(
     let th = build.prove_proc(root());
     let (ok_thm, doc) = mangler.get_data(build.elab,
       proc.name().map_or(Name::StartOkThm, Name::ProcOkThm));
-    let ok_thm = build.elab.env
+    let (ok_thm, _) = build.elab.env
       .add_thm(build.thm.build_thm0(ok_thm, Modifiers::empty(), span.clone(), full, Some(doc), th))
       .map_err(|e| e.into_elab_error(full))?;
     proc_proof.insert(proc.id, ok_thm);