+4 -2

src/AtomDef.res

reviewed

··· 34 34 let coerce: anyValue => option<t> 35 35 } 36 36 37 37 - type loweredSExp = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>}) 38 38 - type atomTag<_> += SExpTag: atomTag<loweredSExp> 37 37 + type varBase = Var({idx: int}) | Schematic({schematic: int, allowed: array<int>}) 38 38 + module VarBase = MakeBaseAtom({ 39 39 + type t = varBase 40 40 + }) 39 41 40 42 exception AtomExpected 41 43

+2 -2

src/HOTerm.res

reviewed

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

+1 -1

src/Method.res

reviewed

··· 172 172 ->Array.filterMap(((key, rule)) => { 173 173 let insts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes) 174 174 let res = rule->Rule.instantiate(insts) 175 175 - if !Judgment.concrete(res.conclusion) { 175 175 + if Judgment.concrete(res.conclusion) { 176 176 Some((key, res, insts)) 177 177 } else { 178 178 None

+4 -4

src/SExp.res

reviewed

··· 150 150 let rec lower = (term: t): option<Atom.t> => 151 151 switch term { 152 152 | Atom(s) => Some(s) 153 153 - | Var({idx}) => Atom.coerce(AnyValue(AtomDef.SExpTag, AtomDef.Var({idx: idx}))) 153 153 + | Var({idx}) => Atom.coerce(AtomDef.VarBase.wrap(Var({idx: idx}))) 154 154 | Schematic({schematic, allowed}) => 155 155 - Atom.coerce(AnyValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed}))) 155 155 + Atom.coerce(AtomDef.VarBase.wrap(Schematic({schematic, allowed}))) 156 156 | Compound({subexps: [e1]}) => lower(e1) 157 157 | _ => None 158 158 } ··· 311 311 312 312 let rec concrete = t => 313 313 switch t { 314 314 - | Schematic(_) => true 314 314 + | Schematic(_) => false 315 315 | Atom(s) => Atom.concrete(s) 316 316 - | Compound({subexps}) => subexps->Array.every(concrete) 316 316 + | Compound({subexps}) => subexps->Array.some(concrete) 317 317 | _ => false 318 318 } 319 319 let mapTerms = (t, f) => f(t)

+3 -3

src/StringA.res

reviewed

··· 462 462 let concrete = t => 463 463 t->Array.every(p => 464 464 switch p { 465 465 - | Schematic(_) => true 466 466 - | _ => false 465 465 + | Schematic(_) => false 466 466 + | _ => true 467 467 } 468 468 ) 469 469 let coerce = (AtomDef.AnyValue(tag, a)) => 470 470 switch tag { 471 471 | Symbolic.BaseAtom.Tag => Some([String(a)]) 472 472 - | AtomDef.SExpTag => 472 472 + | AtomDef.VarBase.Tag => 473 473 Some([ 474 474 switch a { 475 475 | Var({idx}) => Var({idx: idx})

+1 -2

src/Symbolic.res

reviewed

··· 21 21 } 22 22 let substitute = (name, _) => name 23 23 let substDeBruijn = (name, _, ~from as _=?) => name 24 24 - let concrete = _ => false 24 24 + let concrete = _ => true 25 25 let upshift = (t, _, ~from as _=?) => t 26 26 let coerce = _ => None 27 27 - let wrap = a => AtomDef.AnyValue(BaseAtom.Tag, a) 28 27 } 29 28 30 29 module AtomView = {