{"header":{"message":"bump version, refactor math parser, add prec disambiguation map","description":null,"timestamp":"2021-02-08T01:07:38.885959Z","authors":[{"email":"ammkrn@tuta.io","name":"ammkrn"}]},"hash":"O7HVFFGPDNLLC3NM7LRNJQTKEMZNACPJARIP35NGBKMGRW5CLEIAC","authors":[],"deps":{"hashes":[["O7HVFFGPDNLLC3NM7LRNJQTKEMZNACPJARIP35NGBKMGRW5CLEIAC","bump version, refactor math parser, add prec disambiguation map"],["AA",null],["F4Z7XBCF3K6TRYGQT5JW2Y7Z2Y2GELCWCBX2IC5WDYFDIKWBESZQC","forgot to add recursively"],["GR4ZOYWLFJRQARLVGMT4WT5TP5XSMGTBNF5UDUJISDM55CWN62VAC","first commit to pijul"]],"deps":["F4Z7XBCF3K6TRYGQT5JW2Y7Z2Y2GELCWCBX2IC5WDYFDIKWBESZQC"],"known":["GR4ZOYWLFJRQARLVGMT4WT5TP5XSMGTBNF5UDUJISDM55CWN62VAC"]},"hunks":[{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":17,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":39133}],"down_context":[{"change":2,"pos":39133}],"flag":"BLOCK","start":0,"end":10,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":" Assoc"}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":37,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":39411}],"down_context":[{"change":2,"pos":39411}],"flag":"BLOCK","start":11,"end":93,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":"/// Demand a Prec::Num (err owise);"},{"Add":"/// "},{"Add":"/// If true, return (Prec + 1) else Prec"}]}},{"Replacement":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":145,"ins":{"up_context":[{"change":2,"pos":42712}],"down_context":[{"change":2,"pos":42831}],"flag":"BLOCK","start":94,"end":215,"inode":{"change":2,"pos":38844}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":42712},"to":{"change":2,"start":42712,"end":42831},"introduced_by":2}],"inode":{"change":2,"pos":38844}},"ins_contents":[{"Add":" b\"output\" => return Err(VerifErr::Msg(format!(\"`output` statements are not currently supported\"))),"}],"del_contents":[{"Del":" b\"output\" => return Err(VerifErr::Msg(format!(\"Output statements are not currently supported\"))),\n"}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":397,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":50894}],"down_context":[{"change":2,"pos":50894}],"flag":"BLOCK","start":216,"end":221,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":" "}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":449,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":52292}],"down_context":[{"change":2,"pos":52292}],"flag":"BLOCK","start":222,"end":307,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":" /// Add the association of `tok: Str |-> prec: Prec` to the map `MmzMem::consts`"}]}},{"Replacement":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":452,"ins":{"up_context":[{"change":2,"pos":52418}],"down_context":[{"change":2,"pos":52507}],"flag":"BLOCK","start":308,"end":422,"inode":{"change":2,"pos":38844}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":52418},"to":{"change":2,"start":52418,"end":52507},"introduced_by":2}],"inode":{"change":2,"pos":38844}},"ins_contents":[{"Add":" return Err(VerifErr::Msg(format!(\"Parens not allowed as notation consts; they're reserved by mm0\")));"}],"del_contents":[{"Del":" return Err(VerifErr::Msg(format!(\"Parens not allowed as notation consts\")));\n"}]}},{"Replacement":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":457,"ins":{"up_context":[{"change":2,"pos":52617}],"down_context":[{"change":2,"pos":52710}],"flag":"BLOCK","start":423,"end":560,"inode":{"change":2,"pos":38844}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":52617},"to":{"change":2,"start":52617,"end":52710},"introduced_by":2}],"inode":{"change":2,"pos":38844}},"ins_contents":[{"Add":" Err(VerifErr::Msg(format!(\"Cannot redeclare const {:?} with new prec. It was already declared with {:?}\", tk, already)))"}],"del_contents":[{"Del":" Err(VerifErr::Msg(format!(\"Cannot redeclare const {:?} with new prec\", tk)))\n"}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":470,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":52963}],"down_context":[{"change":2,"pos":52963}],"flag":"BLOCK","start":561,"end":562,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":""}]}},{"Replacement":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":477,"ins":{"up_context":[{"change":2,"pos":53175}],"down_context":[{"change":2,"pos":53253}],"flag":"BLOCK","start":563,"end":647,"inode":{"change":2,"pos":38844}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":53175},"to":{"change":2,"start":53175,"end":53253},"introduced_by":2}],"inode":{"change":2,"pos":38844}},"ins_contents":[{"Add":" let (mut lits2, mut right_associative, tok, first_prec) = match it.next() {"}],"del_contents":[{"Del":" let (mut lits2, mut right_associative, tok, prec) = match it.next() {\n"}]}},{"Replacement":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":483,"ins":{"up_context":[{"change":2,"pos":53490}],"down_context":[{"change":2,"pos":53535}],"flag":"BLOCK","start":648,"end":699,"inode":{"change":2,"pos":38844}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":53490},"to":{"change":2,"start":53490,"end":53535},"introduced_by":2}],"inode":{"change":2,"pos":38844}},"ins_contents":[{"Add":" self.add_const(*tok, first_prec.clone())?;"}],"del_contents":[{"Del":" self.add_const(*tok, prec.clone())?;\n"}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":495,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":53877}],"down_context":[{"change":2,"pos":53877}],"flag":"BLOCK","start":700,"end":828,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":" // In assigning the variable its precedence..."},{"Add":" // If there's no const/symbol after it, "}]}},{"Replacement":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":498,"ins":{"up_context":[{"change":2,"pos":53926}],"down_context":[{"change":2,"pos":53996}],"flag":"BLOCK","start":829,"end":1044,"inode":{"change":2,"pos":38844}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":53926},"to":{"change":2,"start":53926,"end":53996},"introduced_by":2}],"inode":{"change":2,"pos":38844}},"ins_contents":[{"Add":" None => bump(right_associative, *tok, *first_prec),"},{"Add":" // If you have [.., var, symbol, .. ] then try to bump"},{"Add":" // the prec of the variable by one."}],"del_contents":[{"Del":" None => bump(right_associative, *tok, *prec),\n"}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":502,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":54073}],"down_context":[{"change":2,"pos":54073}],"flag":"BLOCK","start":1045,"end":1121,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":" // If the next token is another var, give Prec::Max"}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":522,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":54957}],"down_context":[{"change":2,"pos":54957}],"flag":"BLOCK","start":1122,"end":1414,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":" }"},{"Add":""},{"Add":" // If the notation declartion ends with a variable, it's considered "},{"Add":" // right-associative for the precedence disambiguation."},{"Add":" if let NotationLit::Var {..} = none_err!(lits2.last())? {"},{"Add":" self.mem.occupy_prec(term_ident, *first_prec, Assoc::Right)?;"}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":760,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":62709},"to":{"change":2,"start":62709,"end":62710},"introduced_by":2}],"inode":{"change":2,"pos":38844}}},"contents":[{"Del":"\n"}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":767,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":62883}],"down_context":[{"change":2,"pos":62883}],"flag":"BLOCK","start":1415,"end":1590,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":" // 0-ary prefixes don't affect the occupied map."},{"Add":" if term.num_args_no_ret() > 0 {"},{"Add":" self.mem.occupy_prec(term_ident, prec, Assoc::Right)?;"},{"Add":" }"},{"Add":""}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":826,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":64785}],"down_context":[{"change":2,"pos":64785}],"flag":"BLOCK","start":1591,"end":1813,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":" if is_infixr {"},{"Add":" self.mem.occupy_prec(term_ident, prec, Assoc::Right)?"},{"Add":" } else {"},{"Add":" self.mem.occupy_prec(term_ident, prec, Assoc::Left)?"},{"Add":" }"},{"Add":""}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":890,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":66641}],"down_context":[{"change":2,"pos":66641}],"flag":"BLOCK","start":1814,"end":1871,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":" /// Parse an `axiom` or a `theorem` from a .mm0 file"}]}},{"Edit":{"inode":{"change":2,"pos":38844},"path":"src/mmz/parse.rs","line":909,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":67165}],"down_context":[{"change":2,"pos":67165}],"flag":"BLOCK","start":1872,"end":2104,"inode":{"change":2,"pos":38844}}},"contents":[{"Add":" /// Parse an import statement. At this point, all of the imports have"},{"Add":" /// previously been parsed and resolved since they have to be handled"},{"Add":" /// before the main mmz parse, so this just identifies and skips the statement."}]}},{"Replacement":{"inode":{"change":2,"pos":76417},"path":"src/mmz/mod.rs","line":100,"ins":{"up_context":[{"change":2,"pos":78263}],"down_context":[{"change":2,"pos":78315}],"flag":"BLOCK","start":2105,"end":2158,"inode":{"change":2,"pos":76417}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":78263},"to":{"change":2,"start":78263,"end":78315},"introduced_by":2}],"inode":{"change":2,"pos":76417}},"ins_contents":[{"Add":"/// Operator precedence for user-declared notation. "}],"del_contents":[{"Del":"/// Operator precedence for user-declared notation.\n"}]}},{"Replacement":{"inode":{"change":2,"pos":76417},"path":"src/mmz/mod.rs","line":107,"ins":{"up_context":[{"change":2,"pos":78425}],"down_context":[{"change":2,"pos":78430}],"flag":"BLOCK","start":2159,"end":3417,"inode":{"change":2,"pos":76417}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":78425},"to":{"change":2,"start":78425,"end":78430},"introduced_by":2}],"inode":{"change":2,"pos":76417}},"ins_contents":[{"Add":"/// The corresponding term number, its ident (name), whether it's right-associative, and any"},{"Add":"/// literal items/symbols used in the declaration. For general notation declarations that "},{"Add":"/// start with a non-variable, that gets left out of `lits`, and instead becomes"},{"Add":"/// one of the keys in `prefixes`. When the math parser finds the initial token, it"},{"Add":"/// looksup the term using the `prefixes` mapping, and then uses the remaining consts"},{"Add":"/// as checks to make sure the item is syntactically correct, but it will have already"},{"Add":"/// parsed and gone past the initial const token."},{"Add":"///"},{"Add":"/// Examples of lits:"},{"Add":"///```text"},{"Add":"/// NotationInfo { "},{"Add":"/// term_num: 2, "},{"Add":"/// term_ident: an, "},{"Add":"/// rassoc: false, "},{"Add":"/// lits: [Var { pos: 0, prec: Num(34) }, Const(/\\), Var { pos: 1, prec: Num(35) }] "},{"Add":"/// }"},{"Add":"///"},{"Add":"/// NotationInfo { "},{"Add":"/// term_num: 1, "},{"Add":"/// term_ident: not, "},{"Add":"/// rassoc: true, "},{"Add":"/// lits: [Var { pos: 0, prec: Num(41) }] "},{"Add":"///}"},{"Add":"///"},{"Add":"/// // notice the missing `Const([)` at the front; it's a key in the `prefixes` map."},{"Add":"/// NotationInfo { "},{"Add":"/// term_num: 14, "},{"Add":"/// term_ident: sb, "},{"Add":"/// rassoc: true, "},{"Add":"/// lits: [Var { pos: 0, prec: Num(1) }, Const(/), Var { pos: 1, prec: Num(1) }, Const(]), Var { pos: 2, prec: Num(42) }] "},{"Add":"/// }"},{"Add":"///```"}],"del_contents":[{"Del":"/// \n"}]}},{"Edit":{"inode":{"change":2,"pos":76417},"path":"src/mmz/mod.rs","line":152,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":78722}],"down_context":[{"change":2,"pos":78722}],"flag":"BLOCK","start":3418,"end":3503,"inode":{"change":2,"pos":76417}}},"contents":[{"Add":"}"},{"Add":""},{"Add":"#[derive(Debug, Clone, Copy, PartialEq, Eq)]"},{"Add":"pub enum Assoc {"},{"Add":" Left,"},{"Add":" Right"}]}},{"Edit":{"inode":{"change":2,"pos":76417},"path":"src/mmz/mod.rs","line":195,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":79685}],"down_context":[{"change":2,"pos":79685}],"flag":"BLOCK","start":3504,"end":4609,"inode":{"change":2,"pos":76417}}},"contents":[{"Add":"/// The persistent (remains between the checking of each mm0 declaration) mm0 state."},{"Add":"/// "},{"Add":"/// The most complex part of this is the notation system. Users can declare 4 kinds of notation,"},{"Add":"/// prefix, infixl, infixr, and general. The verifier tracks these in only two maps, putting "},{"Add":"/// prefix and general notations in the `prefixes` map, and infixl/infixr declarations in the `infixes` map."},{"Add":"/// The reason for this grouping is because the math parser looks for these two things separately, and the places"},{"Add":"/// where a prefix item might be used are also the places where a general notation can be, and the same is true"},{"Add":"/// for both flavors of infix."},{"Add":"///"},{"Add":"/// There are four maps holding notation information. "},{"Add":"/// 1. `consts`: map of the item's name to its associated precedence."},{"Add":"/// 2. `occupied_precs`: Prevents parser ambiguities; see the doc comment above the field for more info about this."},{"Add":"/// 3. `prefixes`: Associates the items' name to its `NotationInfo { term_num, term_ident, rassoc, lits }`"},{"Add":"/// 3. `infixes`: Associates the items' name to its `NotationInfo { term_num, term_ident, rassoc, lits }`"}]}},{"Replacement":{"inode":{"change":2,"pos":76417},"path":"src/mmz/mod.rs","line":218,"ins":{"up_context":[{"change":2,"pos":79892}],"down_context":[{"change":2,"pos":80023}],"flag":"BLOCK","start":4610,"end":4810,"inode":{"change":2,"pos":76417}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":79892},"to":{"change":2,"start":79892,"end":80023},"introduced_by":2}],"inode":{"change":2,"pos":76417}},"ins_contents":[{"Add":" /// Maps the string representing a user-declared notation to its associated precedence value. For example:"},{"Add":" ///```text "},{"Add":" /// peano.mm0/and "},{"Add":" ///"},{"Add":" /// /\\ |-> `Prec::Num(34)`"},{"Add":" ///```"}],"del_contents":[{"Del":" /// Maps the string representing a user-declared notation to its associated precedence value.\n /// `/\\` |-> `Prec::Num(34)`\n"}]}},{"Replacement":{"inode":{"change":2,"pos":76417},"path":"src/mmz/mod.rs","line":225,"ins":{"up_context":[{"change":2,"pos":80063}],"down_context":[{"change":2,"pos":80105}],"flag":"BLOCK","start":4811,"end":4964,"inode":{"change":2,"pos":76417}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":80063},"to":{"change":2,"start":80063,"end":80105},"introduced_by":2}],"inode":{"change":2,"pos":76417}},"ins_contents":[{"Add":" /// A map containing both prefix and general notation declarations. "},{"Add":" ///"},{"Add":" /// `Ident |-> NotationInfo { term_num, term_ident, rassoc, lits }`"}],"del_contents":[{"Del":" /// A map containing prefix notations\n"}]}},{"Edit":{"inode":{"change":2,"pos":76417},"path":"src/mmz/mod.rs","line":230,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":80216}],"down_context":[{"change":2,"pos":80216}],"flag":"BLOCK","start":4965,"end":7443,"inode":{"change":2,"pos":76417}}},"contents":[{"Add":" /// A mapping of precedence levels to (prefix \\/ infixl \\/ infixr)."},{"Add":" /// This is necessary to prevent ambiguities in the math parser; while the math parser "},{"Add":" /// won't completely break without this, \"You will get _a_ parse, but part of the idea here "},{"Add":" /// is that you will also get _the_ parse\", where _the_ parse is the one that conforms to"},{"Add":" /// the context-free grammar laid out [here](https://github.com/digama0/mm0/blob/master/mm0.md#secondary-parsing)."},{"Add":" ///"},{"Add":" /// If the environment permits both an infixl and infixr at the same precednce level, for example:"},{"Add":" ///"},{"Add":" ///```text"},{"Add":" /// infixr im: $->$ prec 25;"},{"Add":" /// infixl an: $/\\$ prec 25;"},{"Add":" ///```"},{"Add":" ///"},{"Add":" /// Then beginning from state `Start`, and using rules 0, 1, and 2 taken from the mm0 expression grammar, we can derive "},{"Add":" /// both `(a -> (b /\\ c))` and `((a -> b) /\\ c)` as parses of `$ a -> b /\\ c $`:"},{"Add":" ///```text"},{"Add":" /// Start := $ expr(0) $;"},{"Add":" /// rule0 := expression(p1) -> expression(p2) (if p1 < p2)"},{"Add":" /// rule1 := expression(p) -> expression(p) OP expression(p+1) (if OP is infixl prec p)"},{"Add":" /// rule2 := expression(p) -> expression(p+1) OP expression(p) (if OP is infixr prec p)"},{"Add":" ///"},{"Add":" /// with both:"},{"Add":" /// infixr im: $->$ prec 25;"},{"Add":" /// infixl an: $/\\$ prec 25;"},{"Add":" ///"},{"Add":" /// To get ((a -> b) /\\ c):"},{"Add":" /// ($ a -> b /\\ c $, 0) ~rule0~> ($ a -> b /\\ c $, 25) "},{"Add":" /// ($ a -> b /\\ c $, 25) ~rule1~> ($ a -> b $, 25) /\\ ($ c $, 26)"},{"Add":" /// ($ a -> b $, 25) ~rule2~> ($ a $, 26) -> ($ b $, 25)"},{"Add":" ///"},{"Add":" /// To get (a -> (b /\\ c)):"},{"Add":" /// ($ a -> b /\\ c $, 0) ~rule0~> ($ a -> b /\\ c $, 25) by rule0"},{"Add":" /// ($ a -> b /\\ c $, 25) ~rule2~> ($ a $, 26) -> ($ b /\\ c $, 25) by rule2"},{"Add":" /// ($ b /\\ c $, 25) ~rule1~> ($ b $, 25) /\\ ($ c $, 26) by rule1"},{"Add":" ///```"},{"Add":" ///"},{"Add":" /// By disallowing both `-> infixr` and `/\\ infixl` to inhabit the same precedence, this ambiguity"},{"Add":" /// can be avoided."},{"Add":" ///"},{"Add":" /// `peano.mm1` and the mm1 files based on it adopt a convention of using even precedence numbers for "},{"Add":" /// left-associative infix operators, and odd precedence numbers for right-associative infix operators"},{"Add":" /// as a simple way to avoid this kind of collision."},{"Add":" /// infixl is L"},{"Add":" /// infixr is R"},{"Add":" /// (prefix w/ arity > 0) /\\ general ending with a variable are Rassoc"},{"Add":" /// 0ary prefix /\\ general ending with a const don't affect the map."},{"Add":" pub occupied_precs: HashMap, "}]}},{"Edit":{"inode":{"change":2,"pos":76417},"path":"src/mmz/mod.rs","line":290,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":80845}],"down_context":[{"change":2,"pos":80845}],"flag":"BLOCK","start":7444,"end":7445,"inode":{"change":2,"pos":76417}}},"contents":[{"Add":""}]}},{"Edit":{"inode":{"change":2,"pos":76417},"path":"src/mmz/mod.rs","line":314,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":81482}],"down_context":[{"change":2,"pos":81482}],"flag":"BLOCK","start":7446,"end":7490,"inode":{"change":2,"pos":76417}}},"contents":[{"Add":" occupied_precs: HashMap::new(),"}]}},{"Replacement":{"inode":{"change":2,"pos":76417},"path":"src/mmz/mod.rs","line":408,"ins":{"up_context":[{"change":2,"pos":84597}],"down_context":[{"change":2,"pos":84600}],"flag":"BLOCK","start":7491,"end":7872,"inode":{"change":2,"pos":76417}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":84597},"to":{"change":2,"start":84597,"end":84600},"introduced_by":2}],"inode":{"change":2,"pos":76417}},"ins_contents":[{"Add":""},{"Add":" pub fn occupy_prec(&mut self, term_ident: Str<'a>, prec: Prec, assoc: Assoc) -> Res<()> {"},{"Add":" if let Some(already) = self.occupied_precs.insert(prec, assoc) {"},{"Add":" if already != assoc {"},{"Add":" return Err(VerifErr::Msg(format!(\"{:?}; Cannot re-occupy prec {:?} with different associativity\", term_ident, prec)))"},{"Add":" }"},{"Add":" }"},{"Add":" Ok(())"},{"Add":" }"}],"del_contents":[{"Del":" \n"}]}},{"Edit":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":1,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":86855}],"down_context":[{"change":2,"pos":86856}],"flag":"BLOCK","start":7873,"end":8091,"inode":{"change":2,"pos":86855}}},"contents":[{"Add":"//! This module implements an operator precedence parser which aims to turn `$`-delimited math strings "},{"Add":"//! (sometimes also called \"formulas\") into mm0 expressions while allowing for the use of user-defined notation."},{"Add":""}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":138,"ins":{"up_context":[{"change":2,"pos":90946}],"down_context":[{"change":2,"pos":91062}],"flag":"BLOCK","start":8092,"end":8248,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":90946},"to":{"change":2,"start":90946,"end":91062},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" /// The main entry point to the math parser. When the mmz parser wants"},{"Add":" /// to parse an expression from a new math string (`$ .. $`), it calls this."}],"del_contents":[{"Del":"\n\n\n /// For initial calls to `expr`; expects the parser to have something \n /// surrounded by `$` delimiters.\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":142,"ins":{"up_context":[{"change":2,"pos":91150}],"down_context":[{"change":2,"pos":91196}],"flag":"BLOCK","start":8249,"end":8301,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":91150},"to":{"change":2,"start":91150,"end":91196},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" let out_e = self.expr(Prec::Num(0), None)?;"}],"del_contents":[{"Del":" let out_e = self.expr(Prec::Num(0))?;\n"}]}},{"Edit":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":147,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":91304},"to":{"change":2,"start":91304,"end":91313},"introduced_by":2}],"inode":{"change":2,"pos":86855}}},"contents":[{"Del":" \n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":150,"ins":{"up_context":[{"change":2,"pos":91342}],"down_context":[{"change":2,"pos":91544}],"flag":"BLOCK","start":8302,"end":9731,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":91342},"to":{"change":2,"start":91342,"end":91544},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" /// Gets a pair (prec, expr), and tries to continue parsing the rest"},{"Add":" /// of some math string held onto by `self`, which holds the mmz file,"},{"Add":" /// and by extension the math string we're working on."},{"Add":" fn expr(&mut self, initial_prec: Prec, accum: Option>) -> Res> {"},{"Add":" match accum {"},{"Add":" // This was an initial call to `expr`; there's no accumulating expression yet."},{"Add":" None => {"},{"Add":" let prefix = self.prefix(initial_prec)?;"},{"Add":" self.expr(initial_prec, Some(prefix))"},{"Add":" },"},{"Add":" // This is a continuation call, adding to some accumulating expression."},{"Add":" // These calls can only come from calls to `expr` made from within"},{"Add":" // the module."},{"Add":" Some(a) => match self.take_ge_infix(initial_prec).transpose()? {"},{"Add":" // We've reached the end of the current expression, either"},{"Add":" // because the math-string is over, or because initial_prec > next_prec"},{"Add":" None => Ok(a),"},{"Add":" // Continue adding to this accumulator."},{"Add":" // we have: (prec_low, a) .. $ `op2:prec_high` b .. $"},{"Add":" Some((op_term, op_prec)) => {"},{"Add":" let b = self.prefix(op_prec)?;"},{"Add":" let a_until_lt = self.lhs(a, (op_term, op_prec), b)?;"},{"Add":" self.expr(initial_prec, Some(a_until_lt))"},{"Add":" }"},{"Add":" }"},{"Add":" }"},{"Add":" }"}],"del_contents":[{"Del":" /// For recursive calls to `expr`; doesn't demand a leading `$` token\n fn expr(&mut self, p: Prec) -> Res> {\n let lhs_e = self.prefix(p)?;\n self.lhs(p, lhs_e)\n } \n"}]}},{"Edit":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":178,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":91545}],"down_context":[{"change":2,"pos":91545}],"flag":"BLOCK","start":9732,"end":9858,"inode":{"change":2,"pos":86855}}},"contents":[{"Add":" /// `prefix` determined we have a raw term application, so just parse the arguments"},{"Add":" /// and return `App { t, args* }`"}]}},{"Edit":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":182,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":91680}],"down_context":[{"change":2,"pos":91680}],"flag":"BLOCK","start":9859,"end":9895,"inode":{"change":2,"pos":86855}}},"contents":[{"Add":" // If this is a 0-ary term."}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":196,"ins":{"up_context":[{"change":2,"pos":92155}],"down_context":[{"change":2,"pos":92210}],"flag":"BLOCK","start":9896,"end":9957,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":92155},"to":{"change":2,"start":92155,"end":92210},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" if let Ok(e_) = self.expr(Prec::Max, None) {"}],"del_contents":[{"Del":" if let Ok(e_) = self.expr(Prec::Max) {\n"}]}},{"Edit":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":214,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":92697}],"down_context":[{"change":2,"pos":92697}],"flag":"BLOCK","start":9958,"end":10229,"inode":{"change":2,"pos":86855}}},"contents":[{"Add":" /// Parse one of the following:"},{"Add":" ///"},{"Add":" /// 1. An expression surrounded by parentheses"},{"Add":" /// 2. An expression using either a prefix notation or a general notation"},{"Add":" /// 3. An occurrence of a declared variable"},{"Add":" /// 4. A raw term application (like `not ph`)"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":224,"ins":{"up_context":[{"change":2,"pos":92860}],"down_context":[{"change":2,"pos":92906}],"flag":"BLOCK","start":10230,"end":10282,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":92860},"to":{"change":2,"start":92860,"end":92906},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" let e = self.expr(Prec::Num(0), None)?;"}],"del_contents":[{"Del":" let e = self.expr(Prec::Num(0))?;\n"}]}},{"Edit":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":239,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":93347}],"down_context":[{"change":2,"pos":93347}],"flag":"BLOCK","start":10283,"end":10513,"inode":{"change":2,"pos":86855}}},"contents":[{"Add":" /// If `prefix` determines we have either a prefix notation or a general notation,"},{"Add":" /// use this to try and aprse the correct arguments, applying them to whatever"},{"Add":" /// term corresponds to the notation symbol being used."}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":247,"ins":{"up_context":[{"change":2,"pos":93681}],"down_context":[{"change":2,"pos":93981}],"flag":"BLOCK","start":10514,"end":10587,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":93681},"to":{"change":2,"start":93681,"end":93981},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" return self.apply_notation(pfx_info.lits.as_ref(), term)"}],"del_contents":[{"Del":" let args = self.literals(pfx_info.lits.as_ref(), term)?;\n return Ok(MmzExpr::App {\n term_num,\n num_args: term.num_args_no_ret(),\n args: self.alloc(args),\n sort: term.sort(),\n })\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":253,"ins":{"up_context":[{"change":2,"pos":94073}],"down_context":[{"change":2,"pos":94090}],"flag":"BLOCK","start":10588,"end":10842,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":94073},"to":{"change":2,"start":94073,"end":94090},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" /// Having previously parsed a prefix or general notation and determined its"},{"Add":" /// corresponding `term`, parse and check the arguments demanded by that `term`"},{"Add":" /// and then apply them, returning the `App t e*` expression."},{"Add":" fn apply_notation("}],"del_contents":[{"Del":" fn literals(\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":258,"ins":{"up_context":[{"change":2,"pos":94110}],"down_context":[{"change":2,"pos":94145}],"flag":"BLOCK","start":10843,"end":10885,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":94110},"to":{"change":2,"start":94110,"end":94145},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" declar_lits: &[NotationLit<'a>], "}],"del_contents":[{"Del":" lits: &[NotationLit<'a>], \n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":260,"ins":{"up_context":[{"change":2,"pos":94170}],"down_context":[{"change":2,"pos":94211}],"flag":"BLOCK","start":10886,"end":11179,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":94170},"to":{"change":2,"start":94170,"end":94211},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" ) -> Res> {"},{"Add":" // A vec of `[None, .., None]` for as many `NotationLit::Var {..}` are demanded by the term's signature."},{"Add":" // The option stuff is a safe workaround for the fact that they may occur out of order relative to the"},{"Add":" // underlying term's signature."}],"del_contents":[{"Del":" ) -> Res>> {\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":265,"ins":{"up_context":[{"change":2,"pos":94267}],"down_context":[{"change":2,"pos":94342}],"flag":"BLOCK","start":11180,"end":11276,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":94267},"to":{"change":2,"start":94267,"end":94342},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" for declar_lit in declar_lits {"},{"Add":" if let NotationLit::Var {..} = declar_lit {"}],"del_contents":[{"Del":" for lit in lits {\n if let NotationLit::Var {..} = lit {\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":271,"ins":{"up_context":[{"change":2,"pos":94404}],"down_context":[{"change":2,"pos":94430}],"flag":"BLOCK","start":11277,"end":11470,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":94404},"to":{"change":2,"start":94404,"end":94430},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" // For each item (var or symbol) in the original notation declaration,"},{"Add":" // If it's a Const/symbol, make sure the one in the math string is right"},{"Add":" for lit in declar_lits {"}],"del_contents":[{"Del":" for lit in lits {\n"}]}},{"Edit":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":275,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":94454}],"down_context":[{"change":2,"pos":94454}],"flag":"BLOCK","start":11471,"end":11630,"inode":{"change":2,"pos":86855}}},"contents":[{"Add":" // Make sure the notation characters present in the math-string"},{"Add":" // match those specified in the original notation declaration."}]}},{"Edit":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":281,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":94619}],"down_context":[{"change":2,"pos":94619}],"flag":"BLOCK","start":11631,"end":11780,"inode":{"change":2,"pos":86855}}},"contents":[{"Add":" // Make sure the variable in the math string has the sort called"},{"Add":" // for by the variable in the notation declaration."}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":284,"ins":{"up_context":[{"change":2,"pos":94671}],"down_context":[{"change":2,"pos":94899}],"flag":"BLOCK","start":11781,"end":11966,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":94671},"to":{"change":2,"start":94671,"end":94899},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" let sig_e = none_err!(term.args().nth(*pos))?;"},{"Add":" let e = self.expr(*prec, None)?;"},{"Add":" let coerced = self.coerce(e, sig_e.sort())?;"}],"del_contents":[{"Del":" let e = self.expr(*prec)?;\n let nth_arg = none_err!(term.args().nth(*pos))?;\n let tgt_sort = nth_arg.sort();\n let coerced = self.coerce(e, tgt_sort)?;\n"}]}},{"Edit":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":295,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":95189}],"down_context":[{"change":2,"pos":95189}],"flag":"BLOCK","start":11967,"end":12109,"inode":{"change":2,"pos":86855}}},"contents":[{"Add":" // Collect the actual arguments that were present in the math-string"},{"Add":" // now that they've been checked, removing the `Option`."}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":305,"ins":{"up_context":[{"change":2,"pos":95474}],"down_context":[{"change":2,"pos":95500}],"flag":"BLOCK","start":12110,"end":12317,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":95474},"to":{"change":2,"start":95474,"end":95500},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" Ok(MmzExpr::App {"},{"Add":" term_num: term.term_num,"},{"Add":" num_args: term.num_args_no_ret(),"},{"Add":" args: self.alloc(out),"},{"Add":" sort: term.sort(),"},{"Add":" }) "},{"Add":""},{"Add":" } "}],"del_contents":[{"Del":" Ok(out)\n } \n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":315,"ins":{"up_context":[{"change":2,"pos":95599}],"down_context":[{"change":2,"pos":95784}],"flag":"BLOCK","start":12318,"end":12488,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":95599},"to":{"change":2,"start":95599,"end":95784},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" /// equal to the last precedence, return (token, Prec, notation info)"},{"Add":" fn peek_ge_infix(&mut self, last_prec: Prec) -> Option<(Str<'a>, Prec, NotationInfo<'a>)> {"}],"del_contents":[{"Del":" /// equal to the last precedence, return (notation token, Prec, notation info)\n fn peek_stronger_infix(&mut self, last_prec: Prec) -> Option<(Str<'a>, Prec, NotationInfo<'a>)> {\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":337,"ins":{"up_context":[{"change":2,"pos":96589}],"down_context":[{"change":2,"pos":96671}],"flag":"BLOCK","start":12489,"end":12565,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":96589},"to":{"change":2,"start":96589,"end":96671},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" let (_, next_prec, notation_info) = self.peek_ge_infix(last_prec)?;"}],"del_contents":[{"Del":" let (_, next_prec, notation_info) = self.peek_stronger_infix(last_prec)?;\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":351,"ins":{"up_context":[{"change":2,"pos":97113}],"down_context":[{"change":2,"pos":97667}],"flag":"BLOCK","start":12566,"end":12733,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":97113},"to":{"change":2,"start":97113,"end":97667},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" // From `(a, op1, b)`, either continue adding to the right-hand side if there's a stronger operator next"},{"Add":" // or finish and return `App { op1 a b }`"},{"Add":" fn lhs("}],"del_contents":[{"Del":" /// lhs and lhs2 are mutually recursive functions that form the part of the pratt parser\n /// that deals with the presence of infix tokens.\n fn lhs(&mut self, p: Prec, lhs_e: MmzExpr<'b>) -> Res> {\n if let Some((ge_infix_term, ge_infix_prec)) = self.take_ge_infix(p).transpose()? {\n let rhs_e = self.prefix(ge_infix_prec)?;\n let new_lhs_e = self.lhs2(lhs_e, (ge_infix_term, ge_infix_prec), rhs_e)?;\n self.lhs(p, new_lhs_e)\n } else {\n Ok(lhs_e)\n }\n }\n\n fn lhs2(\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":355,"ins":{"up_context":[{"change":2,"pos":97686}],"down_context":[{"change":2,"pos":97794}],"flag":"BLOCK","start":12734,"end":12830,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":97686},"to":{"change":2,"start":97686,"end":97794},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" a: MmzExpr<'b>,"},{"Add":" (op0_term, op0_prec): (Term<'a>, Prec),"},{"Add":" b: MmzExpr<'b>,"}],"del_contents":[{"Del":" lhs_e: MmzExpr<'b>,\n (infix_term, infix_prec): (Term<'a>, Prec),\n rhs_e: MmzExpr<'b>,\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":359,"ins":{"up_context":[{"change":2,"pos":97822}],"down_context":[{"change":2,"pos":98025}],"flag":"BLOCK","start":12831,"end":13234,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":97822},"to":{"change":2,"start":97822,"end":98025},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" // If the next token in the math-string is an infix, such that op0_prec <= op1_prec,"},{"Add":" // recurse with lhs(a, op0, (b op1 c*..))"},{"Add":" if let Some((op1_term, op1_prec)) = self.take_ge_infix(op0_prec).transpose()? {"},{"Add":" let c = self.prefix(op1_prec)?;"},{"Add":" let b_op_cprime = self.lhs(b, (op1_term, op1_prec), c)?;"},{"Add":" self.lhs(a, (op0_term, op0_prec), b_op_cprime)"}],"del_contents":[{"Del":" if let Some((_, next_prec, _)) = self.peek_stronger_infix(infix_prec) {\n let new_rhs_e = self.lhs(next_prec, rhs_e)?;\n self.lhs2(lhs_e, (infix_term, infix_prec), new_rhs_e)\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":366,"ins":{"up_context":[{"change":2,"pos":98042}],"down_context":[{"change":2,"pos":98406}],"flag":"BLOCK","start":13235,"end":13620,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":98042},"to":{"change":2,"start":98042,"end":98406},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" // Next item is None or a weaker infix, so return `App { op1 a b }`"},{"Add":" let mut plus_args = op0_term.args();"},{"Add":" if let (Some(fst), Some(snd), Some(_), None) = (plus_args.next(), plus_args.next(), plus_args.next(), plus_args.next()) {"},{"Add":" let a_coerced = self.coerce(a, fst.sort())?;"},{"Add":" let b_coerced = self.coerce(b, snd.sort())?;"}],"del_contents":[{"Del":" let mut args = infix_term.args();\n if let (Some(fst), Some(snd), Some(_), None) = (args.next(), args.next(), args.next(), args.next()) {\n let end_args = bumpalo::vec![\n in self.bump;\n self.coerce(lhs_e, fst.sort())?,\n self.coerce(rhs_e, snd.sort())?\n ];\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":373,"ins":{"up_context":[{"change":2,"pos":98441}],"down_context":[{"change":2,"pos":98644}],"flag":"BLOCK","start":13621,"end":13859,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":98441},"to":{"change":2,"start":98441,"end":98644},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" term_num: op0_term.term_num,"},{"Add":" num_args: op0_term.num_args_no_ret(),"},{"Add":" args: self.alloc(bumpalo::vec![in self.bump; a_coerced, b_coerced]),"},{"Add":" sort: op0_term.sort()"}],"del_contents":[{"Del":" term_num: infix_term.term_num,\n num_args: infix_term.num_args_no_ret(),\n args: self.alloc(end_args),\n sort: infix_term.sort()\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":379,"ins":{"up_context":[{"change":2,"pos":98684}],"down_context":[{"change":2,"pos":98709}],"flag":"BLOCK","start":13860,"end":14001,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":98684},"to":{"change":2,"start":98684,"end":98709},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" Err(VerifErr::Msg(format!(\"math_parser::lhs2 got a list of infix args that had some number of elems not equal to (2 + 1)\")))"}],"del_contents":[{"Del":" panic!()\n"}]}},{"Replacement":{"inode":{"change":2,"pos":86855},"path":"src/mmz/math_parser.rs","line":382,"ins":{"up_context":[{"change":2,"pos":98733}],"down_context":[{"change":2,"pos":98742}],"flag":"BLOCK","start":14002,"end":14014,"inode":{"change":2,"pos":86855}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":98733},"to":{"change":2,"start":98733,"end":98742},"introduced_by":2}],"inode":{"change":2,"pos":86855}},"ins_contents":[{"Add":" } "},{"Add":""}],"del_contents":[{"Del":" } \n"}]}},{"Edit":{"inode":{"change":3,"pos":40},"path":"changelog.md","line":19,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":830}],"down_context":[],"flag":"BLOCK","start":14015,"end":14133,"inode":{"change":3,"pos":40}}},"contents":[{"Add":""},{"Add":"## 0.1.2 -> 0.1.3"},{"Add":""},{"Add":"+ Add `occupied_precs` map for math-parser disambiguation."},{"Add":"+ refactor lhs handling in math-parser"}]}},{"Replacement":{"inode":{"change":3,"pos":843},"path":"README.md","line":8,"ins":{"up_context":[{"change":3,"pos":1001}],"down_context":[{"change":3,"pos":1032}],"flag":"BLOCK","start":14134,"end":14227,"inode":{"change":3,"pos":843}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1001},"to":{"change":3,"start":1001,"end":1032},"introduced_by":3}],"inode":{"change":3,"pos":843}},"ins_contents":[{"Add":"- Better errors/error-handling. "},{"Add":"- The mmz parser needs a smart way to skip past any errors."}],"del_contents":[{"Del":"- Better errors/error-handling\n"}]}},{"Replacement":{"inode":{"change":3,"pos":7887},"path":"Cargo.toml","line":3,"ins":{"up_context":[{"change":3,"pos":7922}],"down_context":[{"change":3,"pos":7940}],"flag":"BLOCK","start":14228,"end":14246,"inode":{"change":3,"pos":7887}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":7922},"to":{"change":3,"start":7922,"end":7940},"introduced_by":3}],"inode":{"change":3,"pos":7887}},"ins_contents":[{"Add":"version = \"0.1.3\""}],"del_contents":[{"Del":"version = \"0.1.2\"\n"}]}},{"Replacement":{"inode":{"change":3,"pos":8273},"path":"Cargo.lock","line":96,"ins":{"up_context":[{"change":3,"pos":10794}],"down_context":[{"change":3,"pos":10812}],"flag":"BLOCK","start":14247,"end":14265,"inode":{"change":3,"pos":8273}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":10794},"to":{"change":3,"start":10794,"end":10812},"introduced_by":3}],"inode":{"change":3,"pos":8273}},"ins_contents":[{"Add":"version = \"0.1.3\""}],"del_contents":[{"Del":"version = \"0.1.2\"\n"}]}}],"owner":"ammkrn","repo":"second_opinion","token":"SjPrD0E3UJC95HDRzbsQdISsbrsm7Fz30EVf1+nt8Yg=","login":null}

…

Dependencies

Change contents