+1 -1

src/HOTerm.res

reviewed

··· 752 752 } 753 753 754 754 let ghostTerm = Unallowed 755 755 - let unifiesWithAnything = t => 755 755 + let concrete = t => 756 756 switch t { 757 757 | Schematic(_) => true 758 758 | _ => false

+1 -1

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 - if !Judgment.unifiesWithAnything(res.conclusion) { 150 150 + if !Judgment.concrete(res.conclusion) { 151 151 Some((key, res, insts)) 152 152 } else { 153 153 None

+1 -1

src/SExp.res

reviewed

··· 19 19 let lowerSchematic = (_, _) => None 20 20 let ghost = "" 21 21 let substDeBruijn = (name, _, ~from as _=?, ~to as _) => name 22 22 - let unifiesWithAnything = _ => false 22 22 + let concrete = _ => false 23 23 let upshift = (t, _, ~from as _=?) => t 24 24 } 25 25

+4 -4

src/SExpFunc.res

reviewed

··· 11 11 let lowerSchematic: (int, array<int>) => option<t> 12 12 let ghost: t 13 13 let substDeBruijn: (t, Map.t<int, t>, ~from: int=?, ~to: int) => t 14 14 - let unifiesWithAnything: t => bool 14 14 + let concrete: t => bool 15 15 } 16 16 17 17 module IntCmp = Belt.Id.MakeComparable({ ··· 431 431 } 432 432 433 433 let ghostTerm = Ghost 434 434 - let rec unifiesWithAnything = t => 434 434 + let rec concrete = t => 435 435 switch t { 436 436 | Schematic(_) => true 437 437 - | Atom(s) => Atom.unifiesWithAnything(s) 438 438 - | Compound({subexps}) => subexps->Array.every(unifiesWithAnything) 437 437 + | Atom(s) => Atom.concrete(s) 438 438 + | Compound({subexps}) => subexps->Array.every(concrete) 439 439 | _ => false 440 440 } 441 441 let mapTerms = (t, f) => f(t)

+3 -2

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 28 + let concrete: t => bool 29 29 } 30 30 31 31 module type JUDGMENT = { ··· 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 45 + // will unifying t with a term give meaningful substitutions? 46 46 + let concrete: t => bool 46 47 } 47 48 48 49 module type TERM_VIEW = {

+1 -1

src/StringAtom.res

reviewed

··· 505 505 let lowerSchematic = (schematic, allowed) => Some([Schematic({schematic, allowed})]) 506 506 let lowerVar = idx => Some([Var({idx: idx})]) 507 507 let ghost = [Ghost] 508 508 - let unifiesWithAnything = t => 508 508 + let concrete = t => 509 509 t->Array.every(p => 510 510 switch p { 511 511 | Schematic(_) => true

+2 -2

src/StringSExp.res

reviewed

··· 67 67 } 68 68 | ConstS(s) => ConstS(s) 69 69 } 70 70 - let unifiesWithAnything = s => 70 70 + let concrete = s => 71 71 switch s { 72 72 - | StringS(s) => StringAtom.unifiesWithAnything(s) 72 72 + | StringS(s) => StringAtom.concrete(s) 73 73 | ConstS(_) => false 74 74 } 75 75 }