diff --git a/mm0-rs/Cargo.lock b/mm0-rs/Cargo.lock index 970d8024..d55b1417 100644 --- a/mm0-rs/Cargo.lock +++ b/mm0-rs/Cargo.lock @@ -10,15 +10,22 @@ checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe" [[package]] name = "ahash" -version = "0.7.8" +version = "0.8.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "891477e0c6a8957309ee5c45a6368af3ae14bb510732d2684ffa19af310920f9" +checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011" dependencies = [ - "getrandom", + "cfg-if", "once_cell", "version_check", + "zerocopy", ] +[[package]] +name = "allocator-api2" +version = "0.2.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c6cb57a04249c6480766f7f7cef5467412af1490f8d1e243141daddada3264f" + [[package]] name = "android-tzdata" version = "0.1.1" @@ -123,15 +130,9 @@ version = "0.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f0481a0e032742109b1133a095184ee93d88f3dc9e0d28a5d033dc77a073f44f" dependencies = [ - "bit-vec 0.7.0", + "bit-vec", ] -[[package]] -name = "bit-vec" -version = "0.6.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "349f9b6a179ed607305526ca489b34ad0a41aed5f7980fa90eb03160b69598fb" - [[package]] name = "bit-vec" version = "0.7.0" @@ -538,24 +539,14 @@ dependencies = [ "unicode-width", ] -[[package]] -name = "getrandom" -version = "0.2.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7" -dependencies = [ - "cfg-if", - "libc", - "wasi", -] - [[package]] name = "hashbrown" -version = "0.12.3" +version = "0.14.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" +checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1" dependencies = [ "ahash", + "allocator-api2", ] [[package]] @@ -831,7 +822,7 @@ name = "mm0_deepsize" version = "0.1.3" dependencies = [ "bit-set", - "bit-vec 0.7.0", + "bit-vec", "futures", "lsp-types", "memmap", @@ -895,7 +886,7 @@ version = "0.1.0" dependencies = [ "arrayvec 0.7.4", "bit-set", - "bit-vec 0.6.3", + "bit-vec", "bitflags 2.6.0", "bumpalo", "byteorder", @@ -1577,12 +1568,6 @@ dependencies = [ "winapi-util", ] -[[package]] -name = "wasi" -version = "0.11.0+wasi-snapshot-preview1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" - [[package]] name = "wasm-bindgen" version = "0.2.92" diff --git a/mm0-rs/components/mm0_util/src/lib.rs b/mm0-rs/components/mm0_util/src/lib.rs index a9e7cb99..32193191 100644 --- a/mm0-rs/components/mm0_util/src/lib.rs +++ b/mm0-rs/components/mm0_util/src/lib.rs @@ -522,7 +522,7 @@ impl From for FileRef { impl From for FileRef { fn from(uri: lsp_types::Uri) -> FileRef { fn to_file_path(uri: &lsp_types::Uri) -> Option { - 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"))] diff --git a/mm0-rs/src/elab/environment.rs b/mm0-rs/src/elab/environment.rs index 607deda6..41a3b6f5 100644 --- a/mm0-rs/src/elab/environment.rs +++ b/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 { 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 { + 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`]`>`, meaning that in the /// redeclaration case they can still return an `A`, namely the ID of the old declaration -type AddItemResult = Result>>; +type AddItemResult = Result<(A, Option), AddItemError>>; impl AddItemError { /// 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()), diff --git a/mm0-rs/src/elab/local_context.rs b/mm0-rs/src/elab/local_context.rs index 289d97c7..ecf206e9 100644 --- a/mm0-rs/src/elab/local_context.rs +++ b/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) { diff --git a/mm0-rs/src/elab/verify.rs b/mm0-rs/src/elab/verify.rs index 9b7ad921..496f7782 100644 --- a/mm0-rs/src/elab/verify.rs +++ b/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"), diff --git a/mm0-rs/src/mmc/proof/assembler.rs b/mm0-rs/src/mmc/proof/assembler.rs index e657fed1..c0e4f7ee 100644 --- a/mm0-rs/src/mmc/proof/assembler.rs +++ b/mm0-rs/src/mmc/proof/assembler.rs @@ -1370,7 +1370,7 @@ 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, @@ -1378,7 +1378,7 @@ impl<'a> BuildAssembly<'a> { }).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,7 +1421,7 @@ 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, @@ -1429,7 +1429,7 @@ impl<'a> BuildAssembly<'a> { }).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))?; diff --git a/mm0-rs/src/mmc/proof/compiler.rs b/mm0-rs/src/mmc/proof/compiler.rs index 7eaf4710..3ab8aef6 100644 --- a/mm0-rs/src/mmc/proof/compiler.rs +++ b/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);