diff --git a/Cargo.lock b/Cargo.lock index 4915be5..f4a8f26 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1,140 +1,231 @@ -[root] -name = "smetamath" -version = "3.0.1-1" -dependencies = [ - "clap 2.5.2 (registry+https://github.com/rust-lang/crates.io-index)", - "filetime 0.1.10 (registry+https://github.com/rust-lang/crates.io-index)", - "fnv 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)", - "regex 0.1.71 (registry+https://github.com/rust-lang/crates.io-index)", -] +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 [[package]] name = "aho-corasick" -version = "0.5.2" +version = "0.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ca972c2ea5f742bfce5687b9aef75506a764f61d37f8f649047846a9686ddb66" dependencies = [ - "memchr 0.1.11 (registry+https://github.com/rust-lang/crates.io-index)", + "memchr", ] [[package]] name = "ansi_term" -version = "0.7.2" +version = "0.12.1" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2" +dependencies = [ + "winapi 0.3.9", +] + +[[package]] +name = "atty" +version = "0.2.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8" +dependencies = [ + "hermit-abi", + "libc", + "winapi 0.3.9", +] [[package]] name = "bitflags" -version = "0.5.0" +version = "1.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" + +[[package]] +name = "cfg-if" +version = "0.1.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4785bdd1c96b2a846b2bd7cc02e86b6b3dbf14e7e53446c4f54c92a361040822" [[package]] name = "clap" -version = "2.5.2" +version = "2.34.0" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a0610544180c38b88101fecf2dd634b174a62eef6946f84dfc6a7127512b381c" dependencies = [ - "ansi_term 0.7.2 (registry+https://github.com/rust-lang/crates.io-index)", - "bitflags 0.5.0 (registry+https://github.com/rust-lang/crates.io-index)", - "libc 0.2.11 (registry+https://github.com/rust-lang/crates.io-index)", - "strsim 0.4.1 (registry+https://github.com/rust-lang/crates.io-index)", - "unicode-width 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)", - "vec_map 0.6.0 (registry+https://github.com/rust-lang/crates.io-index)", + "ansi_term", + "atty", + "bitflags", + "strsim", + "textwrap", + "unicode-width", + "vec_map", ] [[package]] name = "filetime" -version = "0.1.10" +version = "0.1.15" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "714653f3e34871534de23771ac7b26e999651a0a228f47beb324dfdf1dd4b10f" dependencies = [ - "libc 0.2.11 (registry+https://github.com/rust-lang/crates.io-index)", + "cfg-if", + "libc", + "redox_syscall", ] [[package]] name = "fnv" -version = "1.0.2" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" + +[[package]] +name = "hermit-abi" +version = "0.1.19" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33" +dependencies = [ + "libc", +] [[package]] name = "kernel32-sys" version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7507624b29483431c0ba2d82aece8ca6cdba9382bff4ddd0f7490560c056098d" dependencies = [ - "winapi 0.2.7 (registry+https://github.com/rust-lang/crates.io-index)", - "winapi-build 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)", + "winapi 0.2.8", + "winapi-build", ] [[package]] name = "libc" -version = "0.2.11" +version = "0.2.144" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b00cc1c228a6782d0f076e7b232802e0c5689d41bb5df366f2a6b6621cfdfe1" [[package]] name = "memchr" version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d8b629fb514376c675b98c1421e80b151d3817ac42d7c667717d282761418d20" dependencies = [ - "libc 0.2.11 (registry+https://github.com/rust-lang/crates.io-index)", + "libc", ] +[[package]] +name = "redox_syscall" +version = "0.1.57" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41cc0f7e4d5d4544e8861606a285bb08d3e70712ccc7d2b84d7c0ccfaf4b05ce" + [[package]] name = "regex" -version = "0.1.71" +version = "0.1.80" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4fd4ace6a8cf7860714a2c2280d6c1f7e6a413486c13298bbc86fd3da019402f" dependencies = [ - "aho-corasick 0.5.2 (registry+https://github.com/rust-lang/crates.io-index)", - "memchr 0.1.11 (registry+https://github.com/rust-lang/crates.io-index)", - "regex-syntax 0.3.3 (registry+https://github.com/rust-lang/crates.io-index)", - "thread_local 0.2.6 (registry+https://github.com/rust-lang/crates.io-index)", - "utf8-ranges 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)", + "aho-corasick", + "memchr", + "regex-syntax", + "thread_local", + "utf8-ranges", ] [[package]] name = "regex-syntax" -version = "0.3.3" +version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f9ec002c35e86791825ed294b50008eea9ddfc8def4420124fbc6b08db834957" + +[[package]] +name = "smetamath" +version = "3.0.1-1" +dependencies = [ + "clap", + "filetime", + "fnv", + "regex", +] [[package]] name = "strsim" -version = "0.4.1" +version = "0.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" + +[[package]] +name = "textwrap" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d326610f408c7a4eb6f51c37c330e496b08506c9457c9d34287ecc38809fb060" +dependencies = [ + "unicode-width", +] [[package]] name = "thread-id" version = "2.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a9539db560102d1cef46b8b78ce737ff0bb64e7e18d35b2a5688f7d097d0ff03" dependencies = [ - "kernel32-sys 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)", - "libc 0.2.11 (registry+https://github.com/rust-lang/crates.io-index)", + "kernel32-sys", + "libc", ] [[package]] name = "thread_local" -version = "0.2.6" +version = "0.2.7" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8576dbbfcaef9641452d5cf0df9b0e7eeab7694956dd33bb61515fb8f18cfdd5" dependencies = [ - "thread-id 2.0.0 (registry+https://github.com/rust-lang/crates.io-index)", + "thread-id", ] [[package]] name = "unicode-width" -version = "0.1.3" +version = "0.1.10" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c0edd1e5b14653f783770bce4a4dabb4a5108a5370a5f5d8cfe8710c361f6c8b" [[package]] name = "utf8-ranges" version = "0.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1ca13c08c41c9c3e04224ed9ff80461d97e121589ff27c753a16cb10830ae0f" [[package]] name = "vec_map" -version = "0.6.0" +version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191" [[package]] name = "winapi" -version = "0.2.7" +version = "0.2.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "167dc9d6949a9b857f3451275e911c3f44255842c1f7a76f33c55103a909087a" + +[[package]] +name = "winapi" +version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419" +dependencies = [ + "winapi-i686-pc-windows-gnu", + "winapi-x86_64-pc-windows-gnu", +] [[package]] name = "winapi-build" version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2d315eee3b34aca4797b2da6b13ed88266e6d612562a0c46390af8299fc699bc" + +[[package]] +name = "winapi-i686-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" +[[package]] +name = "winapi-x86_64-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" diff --git a/src/database.rs b/src/database.rs index 57a0e8f..3c81fdf 100644 --- a/src/database.rs +++ b/src/database.rs @@ -149,7 +149,7 @@ pub struct DbOptions { /// Wraps a heap-allocated closure with a difficulty score which can be used for /// sorting; this might belong in the standard library as `CompareFirst` or such. -struct Job(usize, Box); +struct Job(usize, Box); impl PartialEq for Job { fn eq(&self, other: &Job) -> bool { self.0 == other.0 @@ -187,7 +187,7 @@ impl fmt::Debug for Executor { } } -fn queue_work(exec: &Executor, estimate: usize, mut f: Box) { +fn queue_work(exec: &Executor, estimate: usize, mut f: Box) { if exec.concurrency <= 1 { f(); return; @@ -228,8 +228,8 @@ impl Executor { } Executor { - concurrency: concurrency, - mutex: mutex, + concurrency, + mutex, work_cv: cv, } } @@ -277,7 +277,7 @@ impl Executor { /// computation to a thread pool. There are several other methods to attach /// code to promises; these do **not** parallelize, and are intended to do very /// cheap tasks for interface consistency purposes only. -pub struct Promise(Box T + Send>); +pub struct Promise(Box T + Send>); impl Promise { /// Wait for a value to be available and return it, rethrowing any panic. @@ -389,7 +389,7 @@ impl Database { let exec = Executor::new(options.jobs); Database { segments: Some(Arc::new(SegmentSet::new(options.clone(), &exec))), - options: options, + options, nameset: None, scopes: None, verify: None, @@ -454,7 +454,7 @@ impl Database { } let pr = self.parse_result().clone(); { - let mut ns = Arc::make_mut(self.prev_nameset.as_mut().unwrap()); + let ns = Arc::make_mut(self.prev_nameset.as_mut().unwrap()); ns.update(&pr); } self.nameset = self.prev_nameset.clone(); @@ -480,7 +480,7 @@ impl Database { let parse = self.parse_result().clone(); let name = self.name_result().clone(); { - let mut ns = Arc::make_mut(self.prev_scopes.as_mut().unwrap()); + let ns = Arc::make_mut(self.prev_scopes.as_mut().unwrap()); scopeck::scope_check(ns, &parse, &name); } self.scopes = self.prev_scopes.clone(); @@ -507,7 +507,7 @@ impl Database { let scope = self.scope_result().clone(); let name = self.name_result().clone(); { - let mut ver = Arc::make_mut(self.prev_verify.as_mut().unwrap()); + let ver = Arc::make_mut(self.prev_verify.as_mut().unwrap()); verify::verify(ver, &parse, &name, &scope); } self.verify = self.prev_verify.clone(); diff --git a/src/diag.rs b/src/diag.rs index 051553c..1e169bc 100644 --- a/src/diag.rs +++ b/src/diag.rs @@ -177,7 +177,7 @@ fn annotate_diagnostic(notes: &mut Vec, info.notes.push(Notation { source: info.sset.source_info(info.stmt.segment().id).clone(), message: info.s, - span: span, + span, level: info.level, args: mem::replace(&mut info.args, Vec::new()), }) @@ -192,9 +192,9 @@ fn annotate_diagnostic(notes: &mut Vec, } let mut info = AnnInfo { - notes: notes, - sset: sset, - stmt: stmt, + notes, + sset, + stmt, level: Error, s: "", args: Vec::new(), diff --git a/src/export.rs b/src/export.rs index 3736f37..1456254 100644 --- a/src/export.rs +++ b/src/export.rs @@ -48,14 +48,8 @@ impl fmt::Display for ExportError { } impl error::Error for ExportError { - fn description(&self) -> &str { - match *self { - ExportError::Io(ref err) => err.description(), - ExportError::Verify(_) => "verification error", - } - } - fn cause(&self) -> Option<&error::Error> { + fn cause(&self) -> Option<&dyn error::Error> { match *self { ExportError::Io(ref err) => Some(err), ExportError::Verify(_) => None, @@ -71,9 +65,9 @@ pub fn export_mmp(sset: &SegmentSet, out: &mut W) -> Result<(), ExportError> { let thm_label = stmt.label(); - try!(writeln!(out, + writeln!(out, "$( THEOREM={} LOC_AFTER=?\n", - as_str(thm_label))); + as_str(thm_label))?; if let Some(comment) = stmt.associated_comment() { let mut span = comment.span(); span.start += 2; @@ -82,10 +76,10 @@ pub fn export_mmp(sset: &SegmentSet, .unwrap() .replace_all(as_str(span.as_ref(&comment.segment().segment.buffer)), "\n "); - try!(writeln!(out, "*{}\n", cstr)); + writeln!(out, "*{}\n", cstr)?; } - let arr = try!(ProofTreeArray::new(sset, nset, scope, stmt)); + let arr = ProofTreeArray::new(sset, nset, scope, stmt)?; // TODO remove hardcoded logical step symbol let provable_tc = "|-".as_bytes(); @@ -162,22 +156,22 @@ pub fn export_mmp(sset: &SegmentSet, } line.push_str(&str::from_utf8(&tc).unwrap()); line.push_str(&String::from_utf8_lossy(&arr.exprs[cur])); - try!(writeln!(out, "{}", line)); + writeln!(out, "{}", line)?; } - try!(writeln!(out, + writeln!(out, "\n$={}", ProofTreePrinter { sset: sset, nset: nset, scope: scope, thm_label: thm_label, - style: ProofStyle::PackedExplicit, + style: ProofStyle::Packed, arr: &arr, initial_chr: 2, indent: 6, line_width: 79, - })); + })?; - try!(writeln!(out, "\n$)")); + writeln!(out, "\n$)")?; Ok(()) } diff --git a/src/nameck.rs b/src/nameck.rs index bb722e5..b9a5ac5 100644 --- a/src/nameck.rs +++ b/src/nameck.rs @@ -25,6 +25,7 @@ use parser::SegmentId; use parser::SegmentOrder; use parser::SegmentRef; use parser::StatementAddress; +use parser::StatementRef; use parser::SymbolType; use parser::Token; use parser::TokenAddress; @@ -209,7 +210,7 @@ impl Nameset { self.segments.insert(id, seg.clone()); let sref = SegmentRef { segment: &seg, - id: id, + id, }; for symdef in &seg.symbols { @@ -274,7 +275,7 @@ impl Nameset { if let Some(seg) = self.segments.remove(&id) { let sref = SegmentRef { segment: &seg, - id: id, + id, }; let gen = self.generation; for &ref symdef in &seg.symbols { @@ -342,14 +343,18 @@ impl Nameset { self.symbols.get(symbol).and_then(|&ref syminfo| { syminfo.all.first().map(|&(addr, stype)| { LookupSymbol { - stype: stype, + stype, atom: syminfo.atom, address: addr, const_address: syminfo.constant.first().map(|&(addr, _)| addr), } }) }) + } + /// Looks up the atom from a $f statement. + pub fn var_atom(&self, stmt: StatementRef) -> Option { + self.lookup_symbol(&stmt.math_at(1)).map(|lookup| lookup.atom) } } @@ -422,7 +427,7 @@ impl<'a> NameReader<'a> { /// used. pub fn new(nameset: &'a Nameset) -> Self { NameReader { - nameset: nameset, + nameset, incremental: nameset.options.incremental, found_symbol: new_set(), not_found_symbol: new_set(), diff --git a/src/parser.rs b/src/parser.rs index f733a25..631bb70 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -105,8 +105,8 @@ impl Span { fn new2(start: FilePos, end: FilePos) -> Span { Span { - start: start, - end: end, + start, + end, } } @@ -260,8 +260,8 @@ impl StatementAddress { /// Constructs a statement address from its parts. pub fn new(segment_id: SegmentId, index: StatementIndex) -> Self { StatementAddress { - segment_id: segment_id, - index: index, + segment_id, + index, } } } @@ -464,7 +464,7 @@ impl<'a> SegmentRef<'a> { StatementRef { segment: self, statement: &self.segment.statements[index as usize], - index: index, + index, } } @@ -746,7 +746,7 @@ impl<'a> Iterator for StatementIter<'a> { StatementRef { segment: self.segment, statement: st_ref, - index: index, + index, } }) } @@ -1011,8 +1011,8 @@ impl<'a> Scanner<'a> { /// statements and non-comment. fn out_statement(&mut self, stype: StatementType, label: Span) -> Statement { Statement { - stype: stype, - label: label, + stype, + label, math_start: self.statement_math_start, proof_start: self.statement_proof_start, proof_end: self.span_pool.len(), @@ -1421,7 +1421,7 @@ fn collect_definitions(seg: &mut Segment) { for (index, &ref stmt) in seg.statements.iter().enumerate() { let index = index as StatementIndex; if stmt.stype.takes_label() { - seg.labels.push(LabelDef { index: index }); + seg.labels.push(LabelDef { index }); } if stmt.group_end != NO_STATEMENT { @@ -1429,7 +1429,7 @@ fn collect_definitions(seg: &mut Segment) { let math = &seg.span_pool[stmt.math_start..stmt.proof_start]; for sindex in 0..math.len() { seg.local_vars.push(LocalVarDef { - index: index, + index, ordinal: sindex as TokenIndex, }); } diff --git a/src/proof.rs b/src/proof.rs index 3943b1a..a90cf5b 100644 --- a/src/proof.rs +++ b/src/proof.rs @@ -5,19 +5,22 @@ use nameck::Nameset; use parser::as_str; use parser::StatementAddress; use parser::StatementRef; +use parser::StatementType::*; use parser::TokenPtr; use scopeck::ScopeResult; use segment_set::SegmentSet; +use std::cmp::max; use std::cmp::Ord; use std::cmp::Ordering; use std::cmp::PartialOrd; use std::collections::BinaryHeap; use std::collections::HashMap; +use std::collections::hash_map; +use std::collections::VecDeque; use std::fmt; use std::fmt::Write; use std::hash::Hash; use std::hash::Hasher; -use std::hash::SipHasher; use std::ops::Range; use std::u16; use verify::ProofBuilder; @@ -52,14 +55,14 @@ impl Hash for ProofTree { impl ProofTree { /// Create a new proof tree using the given atom and children. pub fn new(parent: &ProofTreeArray, address: StatementAddress, children: Vec) -> Self { - let mut hasher = SipHasher::new(); + let mut hasher = hash_map::DefaultHasher::new(); address.hash(&mut hasher); for &ix in &children { parent.trees[ix].hash(&mut hasher); } ProofTree { - address: address, - children: children, + address, + children, hash: hasher.finish(), } } @@ -127,7 +130,7 @@ impl ProofTreeArray { stmt: StatementRef) -> Result { let mut arr = ProofTreeArray::default(); - arr.qed = try!(verify_one(sset, nset, scopes, &mut arr, stmt)); + arr.qed = verify_one(sset, nset, scopes, &mut arr, stmt)?; arr.indent = arr.calc_indent(); Ok(arr) } @@ -247,20 +250,20 @@ impl ProofTreeArray { 0 }, addr: tree.address, - hyp: hyp, + hyp, } } else { RPNStep::Backref { backref: env.backrefs[step], - hyp: hyp, + hyp, } }; env.out.push(step); } let mut env = Env { arr: self, - parents: parents, - explicit: explicit, + parents, + explicit, out: vec![], backrefs: vec![0; self.trees.len()], count: 0, @@ -275,7 +278,7 @@ impl ProofTreeArray { pub fn normal_iter(&self, explicit: bool) -> NormalIter { NormalIter { arr: self, - explicit: explicit, + explicit, stack: vec![(self.qed, 0)], } } @@ -318,7 +321,7 @@ impl<'a> Iterator for NormalIter<'a> { let out = RPNStep::Normal { fwdref: 0, addr: self.arr.trees[ix].address, - hyp: hyp, + hyp, }; return Some(out); } @@ -361,7 +364,7 @@ impl ProofBuilder for ProofTreeArray { } /// List of possible proof output types. -#[derive(Debug,PartialEq,Eq)] +#[derive(Copy,Clone,Debug,PartialEq,Eq)] pub enum ProofStyle { /// `/compressed` proof output (default). Label list followed by step letters. Compressed, @@ -375,6 +378,30 @@ pub enum ProofStyle { PackedExplicit, } +impl ProofStyle { + /// Returns `true` if this is in explicit style (showing proof hypotheses labels + /// on each step) + pub fn explicit(self) -> bool { + match self { + ProofStyle::Explicit | + ProofStyle::PackedExplicit => true, + _ => false, + } + } + + /// Returns `true` if this is in packed style, meaning duplicate subtrees are + /// referred to by backreferences instead of inlined. (Compressed proofs are + /// considered packed by this definition.) + pub fn packed(self) -> bool { + match self { + ProofStyle::Compressed | + ProofStyle::Packed | + ProofStyle::PackedExplicit => true, + _ => false, + } + } +} + /// A struct for storing display parameters for printing proofs. pub struct ProofTreePrinter<'a> { /// The segment set, for looking up statements @@ -397,89 +424,304 @@ pub struct ProofTreePrinter<'a> { pub line_width: u16, } -impl<'a> fmt::Display for ProofTreePrinter<'a> { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - let mut indent = "\n".to_string(); - for _ in 0..self.indent { - indent.push(' '); +/// The local variables of `ProofTreePrinter::fmt()`, extracted into a struct +/// so that the inner functions can be broken out. +struct ProofTreePrinterImpl<'a, 'b: 'a> { + p: &'a ProofTreePrinter<'a>, + f: &'a mut fmt::Formatter<'b>, + indent: String, + chr: u16, + stmt_lookup: HashMap)>, + backref_alloc: Vec, + backref_max: usize, +} + +impl<'a, 'b> ProofTreePrinterImpl<'a, 'b> { + fn write_word(&mut self, word: &str) -> fmt::Result { + let len = word.len() as u16; + if self.chr + len < self.p.line_width { + self.chr += len + 1; + self.f.write_char(' ')?; + } else { + self.chr = self.p.indent + len; + self.f.write_str(&self.indent)?; } - try!(f.write_str(&indent[(self.initial_chr + 2) as usize..])); - let mut chr = self.indent - 1; - let parents = self.arr.count_parents(); + self.f.write_str(word) + } - let explicit = match self.style { - ProofStyle::Explicit | - ProofStyle::PackedExplicit => true, - _ => false, + fn estr(&self, hyp: Option<(StatementAddress, usize)>) -> String { + if self.p.style.explicit() { + format!("{}=", + match hyp { + Some((stmt, i)) => self.stmt_lookup[&stmt].1[i], + None => as_str(self.p.thm_label), + }) + } else { + String::new() + } + } + + fn print_step(&mut self, item: RPNStep) -> fmt::Result { + let word = match item { + RPNStep::Normal { fwdref, addr, hyp } => { + if fwdref == 0 { + format!("{}{}", self.estr(hyp), self.stmt_lookup[&addr].0) + } else { + format!("{}:{}{}", + if fwdref <= self.backref_alloc.len() { + &self.backref_alloc[fwdref - 1] + } else { + let mut s; + while { + self.backref_max += 1; + s = self.backref_max.to_string(); + self.p.nset.lookup_label(s.as_bytes()).is_some() + } {} + self.backref_alloc.push(s); + self.backref_alloc.last().unwrap() + }, + self.estr(hyp), + self.stmt_lookup[&addr].0) + } + } + RPNStep::Backref { backref, hyp } => { + format!("{}{}", self.estr(hyp), self.backref_alloc[backref - 1]) + } }; + self.write_word(&word) + } - let mut stmt_lookup: HashMap)> = HashMap::new(); - for tree in &self.arr.trees { - stmt_lookup.entry(tree.address) - .or_insert_with(|| { - let label = self.sset.statement(tree.address).label(); - (as_str(label), - if explicit { - match self.scope.get(label) { - Some(frame) => { - frame.hypotheses - .iter() - .map(|hyp| as_str(self.sset.statement(hyp.address()).label())) - .collect() - } - None => vec![], + fn init_stmt_lookup(&mut self) { + for tree in &self.p.arr.trees { + if !self.stmt_lookup.contains_key(&tree.address) { + let label = self.p.sset.statement(tree.address).label(); + let hyps = if self.p.style.explicit() { + match self.p.scope.get(label) { + Some(frame) => { + frame.hypotheses + .iter() + .map(|hyp| { + as_str(self.p + .sset + .statement(hyp.address()) + .label()) + }) + .collect() } - } else { - vec![] - }) - }); + None => vec![], + } + } else { + vec![] + }; + self.stmt_lookup.insert(tree.address, (as_str(label), hyps)); + } } + } - let mut print_step = |item: RPNStep| -> fmt::Result { - let estr = |hyp| if explicit { - format!("{}=", - match hyp { - Some((stmt, i)) => stmt_lookup[&stmt].1[i], - None => as_str(self.thm_label), - }) + fn fmt_compressed(&mut self) -> fmt::Result { + let parents = self.p.arr.count_parents(); + let rpn = self.p.arr.to_rpn(&parents, false); + let mut proof_ordered_hyps = vec![]; + let mut proof_ordered: Vec<(StatementRef, usize)> = vec![]; + let frame = self.p.scope.get(self.p.thm_label).unwrap(); + for item in &rpn { + if let &RPNStep::Normal { addr, .. } = item { + let stmt = self.p.sset.statement(addr); + let vec = match stmt.statement_type() { + Floating => { + let atom = self.p.nset.var_atom(stmt).unwrap(); + if frame.var_list[..frame.mandatory_count].contains(&atom) { + continue; + } + &mut proof_ordered_hyps + } + Essential => &mut proof_ordered_hyps, + Axiom | Provable => &mut proof_ordered, + _ => unreachable!(), + }; + match vec.iter().position(|&(s, _)| s.address() == addr) { + Some(n) => vec[n].1 += 1, + None => vec.push((stmt, 1)), + } + } + } + proof_ordered_hyps.append(&mut proof_ordered); + proof_ordered = proof_ordered_hyps; + let values: Vec = + proof_ordered.iter().map(|&(s, _)| s.label().len() as u16 + 1).collect(); + + let mut sorted_by_refs = (0..proof_ordered.len()).collect::>(); + sorted_by_refs.sort_by(|&a, &b| proof_ordered[b].1.cmp(&proof_ordered[a].1)); + let mut i = frame.mandatory_count; + let mut cutoff = 20; + while cutoff <= i { + i -= cutoff; + cutoff *= 5; + } + let mut length_block = vec![]; + let mut line_pos = 2u16; + let mut paren_stmt = vec![]; + let width = self.p.line_width - self.p.indent + 1; + + let mut knapsack = VecDeque::new(); // scratch space used in knapsack_fit + let mut process_block = |paren_stmt: &mut Vec>, + length_block: &mut Vec| { + length_block.sort(); + while !length_block.is_empty() { + knapsack_fit(&length_block, + &values, + (width - line_pos) as usize, + &mut knapsack); + for &p in &knapsack { + line_pos += values[p]; + paren_stmt.push(proof_ordered[p].0); + if let Ok(n) = length_block.binary_search(&p) { + length_block.remove(n); + } + } + if !knapsack.is_empty() || line_pos >= width - 1 { + line_pos = 0; + } + } + }; + + for pos in sorted_by_refs { + if i == cutoff { + i = 1; + cutoff *= 5; + process_block(&mut paren_stmt, &mut length_block); } else { - String::new() - }; - let fmt = match item { - RPNStep::Normal { fwdref, addr, hyp } => { - if fwdref == 0 { - format!("{}{}", estr(hyp), stmt_lookup[&addr].0) + i += 1; + } + length_block.push(pos); + } + process_block(&mut paren_stmt, &mut length_block); + + let mut letters: Vec = vec![]; + for item in &rpn { + let (is_fwdref, mut letter) = match item { + &RPNStep::Normal { fwdref, addr, .. } => { + let stmt = self.p.sset.statement(addr); + let pos = if stmt.statement_type() == Floating { + let atom = self.p.nset.var_atom(stmt).unwrap(); + frame.var_list[..frame.mandatory_count] + .iter() + .position(|&a| a == atom) } else { - format!("{}:{}{}", fwdref, estr(hyp), stmt_lookup[&addr].0) - } + None + }; + (fwdref != 0, + pos.unwrap_or_else(|| { + frame.mandatory_count + + paren_stmt.iter().position(|s| s.address() == addr).unwrap() + })) + } + &RPNStep::Backref { backref, .. } => { + (false, frame.mandatory_count + paren_stmt.len() + backref - 1) } - RPNStep::Backref { backref, hyp } => format!("{}{}", estr(hyp), backref), }; + let code_start = letters.len(); + letters.push(b'A' + (letter % 20) as u8); + letter /= 20; + while letter != 0 { + letter -= 1; + letters.insert(code_start, b'U' + (letter % 5) as u8); + letter /= 5; + } + if is_fwdref { + letters.push(b'Z'); + } + } - if chr + (fmt.len() as u16) < self.line_width { - chr += (fmt.len() as u16) + 1; - try!(f.write_char(' ')); + self.write_word("(")?; + for s in paren_stmt { + self.write_word(as_str(s.label()))?; + } + self.write_word(")")?; + let mut letters: &[u8] = &letters; + loop { + let ll = (self.p.line_width - self.chr) + .checked_sub(1) + .unwrap_or(self.p.line_width - self.p.indent) as usize; + if ll < letters.len() { + let (left, right) = letters.split_at(ll); + letters = right; + self.write_word(as_str(left))?; } else { - chr = self.indent + (fmt.len() as u16); - try!(f.write_str(&indent)); + return self.write_word(as_str(letters)); } - f.write_str(&fmt) - }; + } + } + + fn fmt(&mut self) -> fmt::Result { + self.f.write_str(&self.indent[(self.p.initial_chr + 2) as usize..])?; - match self.style { - ProofStyle::Compressed => unimplemented!(), + match self.p.style { ProofStyle::Normal | ProofStyle::Explicit => { - for item in self.arr.normal_iter(explicit) { - try!(print_step(item)); + self.init_stmt_lookup(); + for item in self.p.arr.normal_iter(self.p.style.explicit()) { + self.print_step(item)?; } } ProofStyle::Packed | ProofStyle::PackedExplicit => { - for item in self.arr.to_rpn(&parents, explicit) { - try!(print_step(item)); + self.init_stmt_lookup(); + let parents = self.p.arr.count_parents(); + for item in self.p.arr.to_rpn(&parents, self.p.style.explicit()) { + self.print_step(item)?; } } + ProofStyle::Compressed => self.fmt_compressed()?, + } + self.write_word("$.") + } +} + +/// Given an array of items, such that `values[i]` is the cost of the `i`th item, +/// and the items are labeled by `items` (so only the values `i = items[j]` are +/// relevant), find the best fit of items whose total cost is no more than `size`, +/// and return the result in the `included` array. +/// +/// Implements the algorithm given in https://en.wikipedia.org/wiki/Knapsack_problem#0.2F1_knapsack_problem. +fn knapsack_fit(items: &[usize], values: &[u16], mut size: usize, included: &mut VecDeque) { + let mut worth: Vec> = vec![vec![0; size+1]; items.len()+1]; + for (i, &item) in items.iter().enumerate() { + let value = values[item]; + for s in 0..size + 1 { + worth[i + 1][s] = if s >= value as usize { + max(worth[i][s], value + worth[i][s - value as usize]) + } else { + worth[i][s] + } + } + } + included.clear(); + for (i, &item) in items.iter().enumerate().rev() { + if worth[i + 1][size] != worth[i][size] { + included.push_front(item); + size -= values[item] as usize; + if size == 0 { + break; + } } - Ok(()) } -} \ No newline at end of file +} + +impl<'a> fmt::Display for ProofTreePrinter<'a> { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + let mut indent = "\n".to_string(); + for _ in 0..self.indent { + indent.push(' '); + } + ProofTreePrinterImpl { + p: &self, + f, + indent, + chr: self.indent - 1, + stmt_lookup: hash_map::HashMap::new(), + backref_alloc: vec![], + backref_max: 0, + } + .fmt() + } +} diff --git a/src/scopeck.rs b/src/scopeck.rs index 2265d09..0cc21d6 100644 --- a/src/scopeck.rs +++ b/src/scopeck.rs @@ -101,7 +101,6 @@ struct LocalDvInfo { #[derive(Clone,Debug)] struct LocalEssentialInfo<'a> { valid: GlobalRange, - label: TokenPtr<'a>, string: Vec>, } @@ -419,7 +418,7 @@ fn construct_stub_frame(state: &mut ScopeState, valid: sref.scope_range(), hypotheses: Box::default(), target: VerifyExpr { - typecode: typecode, + typecode, rump: 0..0, tail: Box::default(), }, @@ -587,7 +586,7 @@ fn construct_full_frame<'a>(state: &mut ScopeState<'a>, state.frames_out.push(Frame { stype: sref.statement_type(), - label_atom: label_atom, + label_atom, valid: sref.address().unbounded_range(), hypotheses: hyps.into_boxed_slice(), target: scan_res, @@ -673,7 +672,7 @@ fn scope_check_dv<'a>(state: &mut ScopeState<'a>, sref: StatementRef<'a>) { // construct_full_frame when it's no longer in scope state.local_dv.push(LocalDvInfo { valid: sref.scope_range(), - vars: vars, + vars, }); } } @@ -685,7 +684,6 @@ fn scope_check_essential<'a>(state: &mut ScopeState<'a>, sref: StatementRef<'a>) // construct_full_frame when it's no longer in scope state.local_essen.push(LocalEssentialInfo { valid: sref.scope_range(), - label: sref.label(), string: expr, }); } diff --git a/src/segment_set.rs b/src/segment_set.rs index ca87b61..2f6cc55 100644 --- a/src/segment_set.rs +++ b/src/segment_set.rs @@ -328,7 +328,7 @@ impl SegmentSet { fn canonicalize_and_read(state: &mut RecState, path: String) -> io::Result> { - let metadata = try!(fs::metadata(&path)); + let metadata = fs::metadata(&path)?; let time = FileTime::from_last_modification_time(&metadata); // probe 1st cache @@ -337,10 +337,11 @@ impl SegmentSet { None => { // miss, but we have the file size, so try to read in one // call to a buffer we won't have to move - let mut fh = try!(File::open(&path)); + let mut fh = + File::open(&path)?; let mut buf = Vec::with_capacity(metadata.len() as usize + 1); // note: File's read_to_end uses the buffer capacity to choose how much to read - try!(fh.read_to_end(&mut buf)); + fh.read_to_end(&mut buf)?; Ok(split_and_parse(state, path, Some(time), buf)) } diff --git a/src/util.rs b/src/util.rs index dec2922..bef6f85 100644 --- a/src/util.rs +++ b/src/util.rs @@ -79,7 +79,7 @@ pub fn fast_extend(vec: &mut Vec, other: &[T]) { #[inline(always)] pub fn copy_portion(vec: &mut Vec, from: Range) { let Range { start: copy_start, end: copy_end } = from.clone(); - &vec[from]; // for the bounds check + let _ = &vec[from]; // for the bounds check unsafe { let copy_len = copy_end - copy_start; vec.reserve(copy_len); diff --git a/src/verify.rs b/src/verify.rs index 2c763cd..a3de5d5 100644 --- a/src/verify.rs +++ b/src/verify.rs @@ -63,15 +63,6 @@ use util::HashMap; use util::new_map; use util::ptr_eq; -// Proofs are very fragile and there are very few situations where errors are -// recoverable, so we bail out using Result on any error. -macro_rules! try_assert { - ( $cond:expr , $($arg:tt)+ ) => { - if !$cond { - try!(Err($($arg)+)) - } - } -} /// Preparing a step means that it can be referenced using a varint in a /// compressed proof. Compressed steps are either saved prior @@ -258,12 +249,13 @@ fn prepare_step(state: &mut VerifyState

, label: TokenPtr) -> // disallow circular reasoning let valid = frame.valid; let pos = state.cur_frame.valid.start; - try_assert!(state.order.cmp(&pos, &valid.start) == Ordering::Greater, - Diagnostic::StepUsedBeforeDefinition(copy_token(label))); + assert!(state.order.cmp(&pos, &valid.start) == Ordering::Greater, + "{:?}", Diagnostic::StepUsedBeforeDefinition(copy_token(label))); + - try_assert!(valid.end == NO_STATEMENT || + assert!(valid.end == NO_STATEMENT || pos.segment_id == valid.start.segment_id && pos.index < valid.end, - Diagnostic::StepUsedAfterScope(copy_token(label))); + "{:?}", Diagnostic::StepUsedAfterScope(copy_token(label))); if frame.stype == StatementType::Axiom || frame.stype == StatementType::Provable { state.prepared.push(Assert(frame)); @@ -364,7 +356,7 @@ fn do_substitute_vars(expr: &[ExprFragment], vars: &[(Range, Bitset)]) -> /// This is the main "VM" function, and responsible for ~30% of CPU time during /// a one-shot verify operation. fn execute_step(state: &mut VerifyState

, index: usize) -> Result<()> { - try_assert!(index < state.prepared.len(), Diagnostic::StepOutOfRange); + assert!(index < state.prepared.len(), "{:?}", Diagnostic::StepOutOfRange); let fref = match state.prepared[index] { Hyp(ref vars, code, ref expr, ref data) => { @@ -373,7 +365,7 @@ fn execute_step(state: &mut VerifyState

, index: usize) -> Re state.stack.push((data.clone(), StackSlot { vars: vars.clone(), - code: code, + code, expr: expr.clone(), })); return Ok(()); @@ -381,10 +373,10 @@ fn execute_step(state: &mut VerifyState

, index: usize) -> Re Assert(fref) => fref, }; - let sbase = try!(state.stack + let sbase = state.stack .len() .checked_sub(fref.hypotheses.len()) - .ok_or(Diagnostic::ProofUnderflow)); + .ok_or(Diagnostic::ProofUnderflow)?; while state.subst_info.len() < fref.mandatory_count { // this is mildly unhygenic, since slots corresponding to $e hyps won't get cleared, but @@ -407,17 +399,17 @@ fn execute_step(state: &mut VerifyState

, index: usize) -> Re state.builder.push(&mut datavec, data.clone()); match hyp { &Floating(_addr, var_index, typecode) => { - try_assert!(slot.code == typecode, Diagnostic::StepFloatWrongType); + assert!(slot.code == typecode, "{:?}", Diagnostic::StepFloatWrongType); state.subst_info[var_index] = (slot.expr.clone(), slot.vars.clone()); } &Essential(_addr, ref expr) => { - try_assert!(slot.code == expr.typecode, Diagnostic::StepEssenWrongType); - try_assert!(do_substitute_eq(&state.stack_buffer[slot.expr.clone()], + assert!(slot.code == expr.typecode, "{:?}", Diagnostic::StepEssenWrongType); + assert!(do_substitute_eq(&state.stack_buffer[slot.expr.clone()], fref, &expr, &state.subst_info, &state.stack_buffer), - Diagnostic::StepEssenWrong); + "{:?}", Diagnostic::StepEssenWrong); } } } @@ -449,8 +441,8 @@ fn execute_step(state: &mut VerifyState

, index: usize) -> Re for &(ix1, ix2) in &*fref.mandatory_dv { for var1 in &state.subst_info[ix1].1 { for var2 in &state.subst_info[ix2].1 { - try_assert!(var1 < state.dv_map.len() && state.dv_map[var1].has_bit(var2), - Diagnostic::ProofDvViolation); + assert!(var1 < state.dv_map.len() && state.dv_map[var1].has_bit(var2), + "{:?}", Diagnostic::ProofDvViolation); } } } @@ -460,17 +452,17 @@ fn execute_step(state: &mut VerifyState

, index: usize) -> Re fn finalize_step(state: &mut VerifyState

) -> Result { // if we get here, it's a valid proof, but was it the _right_ valid proof? - try_assert!(state.stack.len() <= 1, Diagnostic::ProofExcessEnd); - let &(ref data, ref tos) = try!(state.stack.last().ok_or(Diagnostic::ProofNoSteps)); + assert!(state.stack.len() <= 1, "{:?}", Diagnostic::ProofExcessEnd); + let &(ref data, ref tos) = state.stack.last().ok_or(Diagnostic::ProofNoSteps)?; - try_assert!(tos.code == state.cur_frame.target.typecode, - Diagnostic::ProofWrongTypeEnd); + assert!(tos.code == state.cur_frame.target.typecode, + "{:?}", Diagnostic::ProofWrongTypeEnd); fast_clear(&mut state.temp_buffer); do_substitute_raw(&mut state.temp_buffer, &state.cur_frame, state.nameset); - try_assert!(state.stack_buffer[tos.expr.clone()] == state.temp_buffer[..], - Diagnostic::ProofWrongExprEnd); + assert!(state.stack_buffer[tos.expr.clone()] == state.temp_buffer[..], + "{:?}", Diagnostic::ProofWrongExprEnd); Ok(data.clone()) } @@ -512,7 +504,7 @@ fn verify_proof<'a, P: ProofBuilder>(state: &mut VerifyState<'a, P>, // parse and prepare the label list before the ) loop { - try_assert!(i < stmt.proof_len(), Diagnostic::ProofUnterminatedRoster); + assert!(i < stmt.proof_len(), "{:?}", Diagnostic::ProofUnterminatedRoster); let chunk = stmt.proof_slice_at(i); i += 1; @@ -520,7 +512,7 @@ fn verify_proof<'a, P: ProofBuilder>(state: &mut VerifyState<'a, P>, break; } - try!(prepare_step(state, chunk)); + prepare_step(state, chunk)?; } // after ) is a packed list of varints. decode them and execute the @@ -533,35 +525,35 @@ fn verify_proof<'a, P: ProofBuilder>(state: &mut VerifyState<'a, P>, for &ch in chunk { if ch >= b'A' && ch <= b'T' { k = k * 20 + (ch - b'A') as usize; - try!(execute_step(state, k)); + execute_step(state, k)?; k = 0; can_save = true; } else if ch >= b'U' && ch <= b'Y' { k = k * 5 + 1 + (ch - b'U') as usize; - try_assert!(k < (u32::max_value() as usize / 20) - 1, - Diagnostic::ProofMalformedVarint); + assert!(k < (u32::max_value() as usize / 20) - 1, + "{:?}", Diagnostic::ProofMalformedVarint); can_save = false; } else if ch == b'Z' { - try_assert!(can_save, Diagnostic::ProofInvalidSave); + assert!(can_save, "{:?}", Diagnostic::ProofInvalidSave); save_step(state); can_save = false; } else if ch == b'?' { - try_assert!(k == 0, Diagnostic::ProofMalformedVarint); + assert!(k == 0, "{:?}", Diagnostic::ProofMalformedVarint); return Err(Diagnostic::ProofIncomplete); } } i += 1; } - try_assert!(k == 0, Diagnostic::ProofMalformedVarint); + assert!(k == 0, "{:?}", Diagnostic::ProofMalformedVarint); } else { let mut count = 0; // NORMAL mode proofs are just a list of steps, with no saving provision for i in 0..stmt.proof_len() { let chunk = stmt.proof_slice_at(i); - try_assert!(chunk != b"?", Diagnostic::ProofIncomplete); - try!(prepare_step(state, chunk)); - try!(execute_step(state, count)); + assert!(chunk != b"?", "{:?}", Diagnostic::ProofIncomplete); + prepare_step(state, chunk)?; + execute_step(state, count)?; count += 1; } } @@ -635,7 +627,7 @@ fn verify_segment(sset: &SegmentSet, } VerifySegment { source: (*sref).clone(), - diagnostics: diagnostics, + diagnostics, scope_usage: state.scoper.into_usage(), } } @@ -688,7 +680,7 @@ pub fn verify_one(sset: &SegmentSet, this_seg: stmt.segment(), scoper: ScopeReader::new(scopes), nameset: nset, - builder: builder, + builder, order: &sset.order, cur_frame: &dummy_frame, stack: Vec::new(), diff --git a/th1.mmp b/th1.mmp new file mode 100644 index 0000000..b25f044 --- /dev/null +++ b/th1.mmp @@ -0,0 +1,12 @@ +$( THEOREM=th1 LOC_AFTER=? + +* Prove a theorem + +1::a2 |- ( t + 0 ) = t +2::a1 |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) +3:1,2:mp |- ( ( t + 0 ) = t -> t = t ) +qed:1,3:mp |- t = t + +$= tt tze 1:tpl tt 2:weq tt tt 3:weq tt 4:a2 2 2 3 wim 4 1 tt tt a1 mp mp $. + +$)