+5

src/HOTerm.res

reviewed

··· 752 752 } 753 753 754 754 let ghostTerm = Unallowed 755 755 + let unifiesWithAnything = t => 756 756 + switch t { 757 757 + | Schematic(_) => true 758 758 + | _ => false 759 759 + } 755 760 let mapTerms = (t, f) => f(t)

+1 -2

src/Method.res

reviewed

··· 147 147 ->Array.filterMap(((key, rule)) => { 148 148 let insts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes) 149 149 let res = rule->Rule.instantiate(insts) 150 150 - let ghostSubs = Judgment.unify(Judgment.ghostTerm, res.conclusion) 151 151 - if ghostSubs->Seq.head->Option.isNone { 150 150 + if !Judgment.unifiesWithAnything(res.conclusion) { 152 151 Some((key, res, insts)) 153 152 } else { 154 153 None

+1

src/SExp.res

reviewed

··· 19 19 let lowerSchematic = (_, _) => "" 20 20 let ghost = "" 21 21 let substDeBruijn = (name, _, ~from as _) => name 22 22 + let unifiesWithAnything = _ => false 22 23 } 23 24 24 25 include SExpFunc.Make(ConstSymbol)

+8

src/SExpFunc.res

reviewed

··· 10 10 let lowerSchematic: (int, array<int>) => t 11 11 let ghost: t 12 12 let substDeBruijn: (t, array<t>, ~from: int) => t 13 13 + let unifiesWithAnything: t => bool 13 14 } 14 15 15 16 module IntCmp = Belt.Id.MakeComparable({ ··· 426 427 } 427 428 428 429 let ghostTerm = Ghost 430 430 + let rec unifiesWithAnything = t => 431 431 + switch t { 432 432 + | Schematic(_) => true 433 433 + | Symbol(s) => Symbol.unifiesWithAnything(s) 434 434 + | Compound({subexps}) => subexps->Array.every(unifiesWithAnything) 435 435 + | _ => false 436 436 + } 429 437 let mapTerms = (t, f) => f(t) 430 438 }

+2 -1

src/Signatures.res

reviewed

··· 25 25 let prettyPrint: (t, ~scope: array<meta>) => string 26 26 let prettyPrintMeta: meta => string 27 27 let ghostTerm: t 28 28 + let unifiesWithAnything: t => bool 28 29 } 29 30 30 31 module type JUDGMENT = { ··· 37 38 let reduce: t => t 38 39 let upshift: (t, int, ~from: int=?) => t 39 40 // Map a function over all terms in the judgment 40 40 - // NOTE(josh): we should return to whether this is necessary. 41 41 let mapTerms: (t, Term.t => Term.t) => t 42 42 let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string> 43 43 let prettyPrint: (t, ~scope: array<Term.meta>) => string 44 44 let ghostTerm: t 45 45 + let unifiesWithAnything: t => bool 45 46 } 46 47 47 48 module type TERM_VIEW = {

+5

src/StringSExp.res

reviewed

··· 53 53 } 54 54 | ConstS(s) => ConstS(s) 55 55 } 56 56 + let unifiesWithAnything = s => 57 57 + switch s { 58 58 + | StringS(s) => StringTerm.unifiesWithAnything(s) 59 59 + | ConstS(_) => false 60 60 + } 56 61 } 57 62 58 63 include SExpFunc.Make(StringSymbol)

+7

src/StringTerm.res

reviewed

··· 504 504 } 505 505 506 506 let ghostTerm = [Ghost] 507 507 + let unifiesWithAnything = t => 508 508 + t->Array.every(p => 509 509 + switch p { 510 510 + | Schematic(_) => true 511 511 + | _ => false 512 512 + } 513 513 + )