Merge pull request #4 from joshcbrown/push-vpprvrwsyxvt

+139

index.html

··· 339 339 340 340 a. asm |- ? 341 341 </hol-proof> 342 + <h1>String</h1> 343 + <h2>Basic</h2> 344 + <hol-string id="index.html/mexp" deps="index.html/myconfig"> 345 + ---- M-Empty 346 + "" M 347 + 348 + s. 349 + "$s" M 350 + ------- M-Surround 351 + "($s)" M 352 + 353 + s1. s2. 354 + "$s1" M "$s2" M 355 + ------- M-Juxtapose 356 + "$s1 $s2" M 357 + </hol-string> 358 + <hol-string-proof id="index.html/stringprooftest" deps="index.html/myconfig index.html/mexp"> 359 + -------- paren 360 + "()(())" M 361 + |- by (Concat "()" "(())") { 362 + |- by (Surround "") { 363 + |- by (Empty) {} 364 + } 365 + |- by (Surround "()") { 366 + |- by (Surround "") { 367 + |- by (Empty) {} 368 + } 369 + } 370 + } 371 + </hol-string-proof> 372 + <hol-string id="index.html/bool" deps="index.html/myconfig"> 373 + ------- T-Atom 374 + "T" Atom 375 + ------- F-Atom 376 + "F" Atom 377 + 378 + e. 379 + "$e" Atom 380 + --------- Atom-AE 381 + "$e" AE 382 + 383 + e1.e2. 384 + "$e1" Atom "$e2" AE 385 + -------------------- And 386 + "$e1 /\\ $e2" AE 387 + 388 + e. 389 + "$e" AE 390 + --------- AE-B 391 + "$e" B 392 + 393 + e1.e2. 394 + "$e1" AE "$e2" B 395 + ----------------- Or 396 + "$e1 \\/ $e2" B 397 + 398 + e. 399 + "$e" B 400 + ----------- Paren 401 + "($e)" Atom 402 + </hol-string> 403 + <hol-string-proof id="index.html/boolprooftest" deps="index.html/myconfig index.html/bool"> 404 + ------------- bool 405 + "T/\\(T\\/F)" AE 406 + |- by (And "T" "(T\\/F)") { 407 + |- by (T-Atom) {} 408 + |- by (Atom-AE "(T\\/F)") { 409 + |- by (Paren "T\\/F") { 410 + |- by (Or "T" "F") { 411 + |- by (Atom-AE "T") { 412 + |- by (T-Atom) {} 413 + } 414 + |- by (AE-B "F") { 415 + |- by (Atom-AE "F") { 416 + |- by (F-Atom) {} 417 + } 418 + } 419 + } 420 + } 421 + } 422 + } 423 + </hol-string-proof> 424 + <h2>With first-order term judgments</h2> 425 + <hol-string id="index.html/m-exp-parse" deps="index.html/myconfig"> 426 + ---- MParse-Empty 427 + "" (MP emp) 428 + 429 + s1. p1. 430 + "$s1" (MP p1) 431 + ------------- MParse-Surround 432 + "($s1)" (MP (p1)) 433 + 434 + s1. s2. p1. p2. 435 + "$s1" p1 436 + "$s1" p2 437 + ------------------- MParse-Juxtapose 438 + "$s1 $s2" (MP (p1 p2)) 439 + </hol-string> 440 + <hol-string id="index.html/mexp-induct" deps="index.html/myconfig"> 441 + s. p. 442 + "$s" M "" p [s1. "$s1" p |- "($s1)" p] [s1. s2. "$s1" p "$s2" p |- "$s1 $s2" p] 443 + ---------------------------------- M-Induct 444 + "$s" p 445 + </hol-string> 446 + <hol-string id="index.html/lexp" deps="index.html/myconfig"> 447 + s. "$s" L 448 + -----N-Surr 449 + "($s)" N 450 + 451 + -----L-Empty 452 + "" L 453 + 454 + s1. s2. 455 + "$s1" N "$s2" L 456 + -----L-Juxtapose 457 + "$s1 $s2" L 458 + </hol-string> 459 + 460 + <hol-string-proof id="index.html/lexp-n" deps="index.html/myconfig index.html/mexp index.html/mexp-induct index.html/lexp"> 461 + s. "$s" N 462 + --------N-L 463 + "$s" L 464 + s. sn |- by (L-Juxtapose s "") { 465 + |- by (sn) {} 466 + |- by (L-Empty) {} 467 + } 468 + </hol-string-proof> 469 + <hol-string-proof id="index.html/lexp-juxt" deps="index.html/myconfig index.html/mexp index.html/mexp-induct index.html/lexp"> 470 + s1.s2. "$s1" L "$s2" L 471 + --------------------- lexp-juxt 472 + "$s1 $s2" L 473 + s1. s2. s1L s2L |- ? 474 + </hol-string-proof> 475 + <hol-string-proof id="index.html/mexp-lexp" deps="index.html/myconfig index.html/mexp index.html/mexp-induct index.html/lexp index.html/lexp-juxt index.html/lexp-n"> 476 + s. "$s" M 477 + ----------- mexp-lexp 478 + "$s" L 479 + s. sM |- ? 480 + </hol-string-proof> 342 481 <script type="module" src="./src/testcomponent.tsx"></script> 343 482 </body> 344 483 </html>

+1

package.json

··· 17 17 "prepare": "husky" 18 18 }, 19 19 "dependencies": { 20 + "@jmagaram/rescript-seq": "^4.4.1", 20 21 "@rescript/react": "^0.13.1", 21 22 "react": "^19.1.0", 22 23 "react-dom": "^19.1.0",

+5 -1

rescript.json

··· 9 9 "in-source": true 10 10 }, 11 11 "suffix": ".mjs", 12 - "bs-dependencies": ["@rescript/core", "@rescript/react"], 12 + "bs-dependencies": [ 13 + "@rescript/core", 14 + "@rescript/react", 15 + "@jmagaram/rescript-seq" 16 + ], 13 17 "bs-dev-dependencies": ["@dusty-phillips/rescript-zora"], 14 18 "bsc-flags": ["-open RescriptCore"], 15 19 "jsx": { "version": 4 }

+20 -7

src/HOTerm.res

··· 20 20 let mapSubst = (m: subst, f: t => t): subst => { 21 21 m->Belt.Map.Int.map(f) 22 22 } 23 + let substEqual = (m1, m2) => m1 == m2 23 24 let makeSubst = () => { 24 25 Belt.Map.Int.empty 25 26 } 27 + let mergeSubsts = (m1: subst, m2: subst) => 28 + Belt.Map.Int.merge(m1, m2, (_, o1, o2) => 29 + switch (o1, o2) { 30 + | (Some(v), _) | (_, Some(v)) => Some(v) 31 + | (None, None) => None 32 + } 33 + ) 26 34 let rec equivalent = (a: t, b: t) => { 27 35 switch (a, b) { 28 36 | (Symbol({name: na}), Symbol({name: nb})) => na == nb ··· 180 188 }) 181 189 | Var(_) | Unallowed | Symbol(_) => term 182 190 } 191 + 183 192 // TODO: check how will this interact with meta variables (schematics) and check if it is needed to have a subst parameter - it should not be needed for subst produced by pattern unification 184 193 let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) => 185 194 switch term { ··· 453 462 } 454 463 unifyArray(xs, ys, subst, ~gen) 455 464 } 456 - let unify = (a: t, b: t, ~gen=?) => { 457 - try { 458 - [unifyTerm(a, b, emptySubst, ~gen)] 459 - } catch { 460 - | UnifyFail(_) => [] 461 - } 462 - } 465 + let unify = (a: t, b: t, ~gen=?) => 466 + Seq.fromArray( 467 + try { 468 + [unifyTerm(a, b, emptySubst, ~gen)] 469 + } catch { 470 + | UnifyFail(_) => [] 471 + }, 472 + ) 463 473 let place = (x: int, ~scope: array<string>) => 464 474 app( 465 475 Schematic({ ··· 467 477 }), 468 478 Array.fromInitializer(~length=Array.length(scope), i => Var({idx: i})), 469 479 ) 480 + 470 481 let prettyPrintVar = (idx: int, scope: array<string>) => 471 482 switch scope[idx] { 472 483 | Some(n) if Array.indexOf(scope, n) == idx => n ··· 506 517 ->String.concat(")") 507 518 | Unallowed => "" 508 519 } 520 + let prettyPrintSubst = (sub: subst, ~scope: array<string>) => 521 + Util.prettyPrintIntMap(sub, ~showV=t => prettyPrint(t, ~scope)) 509 522 let symbolRegexpString = "^([^\\s()]+)" 510 523 let nameRES = "^([^\\s.\\[\\]()]+)\\." 511 524 exception ParseError(string)

+3 -1

src/HOTermJView.resi

··· 1 - include Signatures.JUDGMENT_VIEW with module Term := HOTerm and module Judgment := HOTerm 1 + include Signatures.JUDGMENT_VIEW 2 + with module Term := HOTerm 3 + and module Judgment := TermAsJudgment.HOTermJ

+205 -14

src/Method.res

··· 2 2 open Util 3 3 module Context = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 4 4 module Rule = Rule.Make(Term, Judgment) 5 - type rec t = { 5 + type t = { 6 6 fixes: array<Term.meta>, 7 7 facts: Dict.t<Rule.t>, 8 8 } ··· 15 15 module Context: module type of Context(Term, Judgment) 16 16 type t<'a> 17 17 let keywords: array<string> 18 - let substitute: (t<'a>, Term.subst) => t<'a> 18 + let substitute: (t<'a>, Judgment.subst) => t<'a> 19 19 let check: (t<'a>, Context.t, Judgment.t, ('a, Rule.t) => 'b) => result<t<'b>, string> 20 - let apply: (Context.t, Judgment.t, Term.gen, Rule.t => 'a) => Dict.t<(t<'a>, Term.subst)> 20 + let apply: (Context.t, Judgment.t, Term.gen, Rule.t => 'a) => Dict.t<(t<'a>, Judgment.subst)> 21 21 let map: (t<'a>, 'a => 'b) => t<'b> 22 22 let parse: ( 23 23 string, ··· 39 39 module Context = Context(Term, Judgment) 40 40 type t<'a> = { 41 41 ruleName: string, 42 - instantiation: array<Term.t>, 42 + instantiation: array<Judgment.substCodom>, 43 43 subgoals: array<'a>, 44 44 } 45 45 let map = (it: t<'a>, f) => { ··· 49 49 subgoals: it.subgoals->Array.map(f), 50 50 } 51 51 } 52 - let substitute = (it: t<'a>, subst: Term.subst) => { 52 + let substitute = (it: t<'a>, subst: Judgment.subst) => { 53 53 { 54 54 ruleName: it.ruleName, 55 - instantiation: it.instantiation->Array.map(t => t->Term.substitute(subst)), 55 + instantiation: it.instantiation->Array.map(t => t->Judgment.substituteSubstCodom(subst)), 56 56 subgoals: it.subgoals, 57 57 } 58 58 } ··· 64 64 ~indentation=0, 65 65 ~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string, 66 66 ) => { 67 - let args = it.instantiation->Array.map(t => Term.prettyPrint(t, ~scope)) 67 + let args = it.instantiation->Array.map(t => Judgment.prettyPrintSubstCodom(t, ~scope)) 68 68 "by (" 69 - ->String.concat(Array.join([it.ruleName, ...args], " ")) 69 + ->String.concat(Array.join([it.ruleName]->Array.concat(args), " ")) 70 70 ->String.concat(") {") 71 71 ->String.concat( 72 72 if Array.length(it.subgoals) > 0 { ··· 91 91 let instantiation = [] 92 92 let it = ref(Error("")) 93 93 while { 94 - it := Term.parse(cur.contents, ~scope, ~gen) 94 + it := Judgment.parseSubstCodom(cur.contents, ~scope, ~gen) 95 95 it.contents->Result.isOk 96 96 } { 97 97 let (val, rest) = it.contents->Result.getExn ··· 138 138 let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => { 139 139 let ret = Dict.make() 140 140 ctx.facts->Dict.forEachWithKey((rule, key) => { 141 - let insts = 142 - rule.vars->Array.map(m => Term.place(gen->Term.fresh(~replacing=m), ~scope=ctx.fixes)) 141 + let insts = rule->Rule.schematise(gen, ~scope=ctx.fixes) 143 142 let res = rule->Rule.instantiate(insts) 144 143 let substs = Judgment.unify(res.conclusion, j, ~gen) 145 - substs->Array.forEach(subst => { 144 + substs->Seq.forEach(subst => { 146 145 let new = { 147 146 ruleName: key, 148 147 instantiation: insts, ··· 184 183 } 185 184 } 186 185 let updateAtKey = (it: t<'a>, key: int, f: 'a => 'a) => { 187 - let newsgs = [...it.subgoals] 186 + let newsgs = it.subgoals->Array.copy 187 + newsgs->Array.set(key, f(newsgs[key]->Option.getExn)) 188 + {...it, subgoals: newsgs} 189 + } 190 + } 191 + 192 + module Elimination = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 193 + module Rule = Rule.Make(Term, Judgment) 194 + module Context = Context(Term, Judgment) 195 + type t<'a> = { 196 + ruleName: string, 197 + elimName: string, 198 + instantiation: array<Judgment.substCodom>, 199 + subgoals: array<'a>, 200 + } 201 + exception InternalParseError(string) 202 + let keywords = ["elim"] 203 + let prettyPrint = ( 204 + it: t<'a>, 205 + ~scope, 206 + ~indentation=0, 207 + ~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string, 208 + ) => { 209 + let subgoalsSpacer = if Array.length(it.subgoals) > 0 { 210 + newline 211 + } else { 212 + "" 213 + } 214 + let instantiation = Array.join( 215 + it.instantiation->Array.map(t => Judgment.prettyPrintSubstCodom(t, ~scope)), 216 + " ", 217 + ) 218 + let subgoalsStr = 219 + it.subgoals 220 + ->Array.map(s => subprinter(s, ~scope, ~indentation=indentation + 2)) 221 + ->Array.join(newline) 222 + `elim (${it.ruleName} ${it.elimName} ${instantiation}) {${subgoalsSpacer}${subgoalsStr}}` 223 + } 224 + 225 + let map = (it: t<'a>, f) => { 226 + { 227 + ruleName: it.ruleName, 228 + elimName: it.elimName, 229 + instantiation: it.instantiation, 230 + subgoals: it.subgoals->Array.map(f), 231 + } 232 + } 233 + 234 + let substitute = (it: t<'a>, subst: Judgment.subst) => { 235 + { 236 + ruleName: it.ruleName, 237 + elimName: it.elimName, 238 + instantiation: it.instantiation->Array.map(t => t->Judgment.substituteSubstCodom(subst)), 239 + subgoals: it.subgoals, 240 + } 241 + } 242 + 243 + let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => { 244 + let cur = ref(String.trim(input)) 245 + if cur.contents->String.get(0) == Some("(") { 246 + Rule.parseRuleName(cur.contents->String.sliceToEnd(~start=1))->Result.flatMap((( 247 + ruleName, 248 + rest, 249 + )) => { 250 + cur := rest 251 + Rule.parseRuleName(cur.contents)->Result.flatMap(((elimName, rest)) => { 252 + cur := rest 253 + let instantiation = [] 254 + let it = ref(Error("")) 255 + while { 256 + it := Judgment.parseSubstCodom(cur.contents, ~scope, ~gen) 257 + it.contents->Result.isOk 258 + } { 259 + let (val, rest) = it.contents->Result.getExn 260 + Array.push(instantiation, val) 261 + cur := String.trim(rest) 262 + } 263 + if cur.contents->String.get(0) == Some(")") { 264 + cur := String.trim(cur.contents->String.sliceToEnd(~start=1)) 265 + let subgoals = [] 266 + if cur.contents->String.get(0) == Some("{") { 267 + cur := String.trim(cur.contents->String.sliceToEnd(~start=1)) 268 + try { 269 + while cur.contents->String.get(0) != Some("}") { 270 + switch subparser(cur.contents, ~scope, ~gen) { 271 + | Ok((sg, rest)) => { 272 + Array.push(subgoals, sg) 273 + cur := String.trim(rest) 274 + } 275 + | Error(e) => raise(InternalParseError(e)) 276 + } 277 + } 278 + if cur.contents->String.get(0) == Some("}") { 279 + cur := String.trim(cur.contents->String.sliceToEnd(~start=1)) 280 + let res = {ruleName, elimName, instantiation, subgoals} 281 + Console.log(("parsed elim", res)) 282 + Ok((res, cur.contents)) 283 + } else { 284 + Error("} or subgoal proof expected") 285 + } 286 + } catch { 287 + | InternalParseError(e) => Error(e) 288 + } 289 + } else { 290 + Error("{ expected") 291 + } 292 + } else { 293 + Error(") or term expected") 294 + } 295 + }) 296 + }) 297 + } else { 298 + Error("Expected (") 299 + } 300 + } 301 + 302 + let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => { 303 + switch (ctx.facts->Dict.get(it.ruleName), ctx.facts->Dict.get(it.elimName)) { 304 + | (None, _) => Error(`Cannot find rule '${it.ruleName}'`) 305 + | (_, None) => Error(`Cannot find elimination fact '${it.elimName}'`) 306 + | (Some(rule), Some(elim)) if rule.premises->Array.length > 0 => { 307 + let {premises, conclusion} = Rule.instantiate(rule, it.instantiation) 308 + let elimPremise = premises[0]->Option.getExn 309 + let remainingPremises = premises->Array.sliceToEnd(~start=1) 310 + if elimPremise.premises->Array.length > 0 { 311 + Error(`Premise to eliminate in rule ${it.ruleName} has non-empty premises`) 312 + } else if elim.premises->Array.length > 0 { 313 + Error(`Elimination motive (?) ${it.elimName} has non-empty premises`) 314 + } else if !Judgment.equivalent(elimPremise.conclusion, elim.conclusion) { 315 + Error(`Premise to eliminate and elimination motive (?) ${it.elimName} do not match`) 316 + } else if !Judgment.equivalent(conclusion, j) { 317 + let concString = Judgment.prettyPrint(conclusion, ~scope=ctx.fixes) 318 + let goalString = Judgment.prettyPrint(j, ~scope=ctx.fixes) 319 + Error(`Conclusion of rule '${concString}' doesn't match goal '${goalString}'`) 320 + } else if Array.length(it.subgoals) != Array.length(remainingPremises) { 321 + let subgoalsRem = Array.length(it.subgoals)->Int.toString 322 + let premsRem = Array.length(remainingPremises)->Int.toString 323 + Error( 324 + `Number of subgoals (${subgoalsRem}) doesn't match rule ${it.ruleName}'s remaining number (${premsRem})`, 325 + ) 326 + } else { 327 + Ok({ 328 + ruleName: it.ruleName, 329 + elimName: it.elimName, 330 + instantiation: it.instantiation, 331 + subgoals: Belt.Array.zipBy(it.subgoals, remainingPremises, f), 332 + }) 333 + } 334 + } 335 + | (Some(_), Some(_)) => Error(`Rule ${it.ruleName} doesn't have any premises`) 336 + } 337 + } 338 + 339 + let updateAtKey = (it: t<'a>, key: int, f: 'a => 'a) => { 340 + let newsgs = it.subgoals->Array.copy 188 341 newsgs->Array.set(key, f(newsgs[key]->Option.getExn)) 189 342 {...it, subgoals: newsgs} 190 343 } 344 + 345 + let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => { 346 + let ret = Dict.make() 347 + let possibleRules = 348 + ctx.facts 349 + ->Dict.toArray 350 + ->Array.filter(((_, r)) => 351 + r.premises->Array.length > 0 && (r.premises[0]->Option.getExn).premises->Array.length == 0 352 + ) 353 + let possibleElims = 354 + ctx.facts->Dict.toArray->Array.filter(((_, r)) => r.premises->Array.length == 0) 355 + possibleRules->Array.forEach(((ruleName, rule)) => { 356 + possibleElims->Array.forEach(((elimName, elim)) => { 357 + let ruleInsts = rule->Rule.schematise(gen, ~scope=ctx.fixes) 358 + let elimInsts = elim->Rule.schematise(gen, ~scope=ctx.fixes) 359 + let (rule', elim) = (rule->Rule.instantiate(ruleInsts), elim->Rule.instantiate(elimInsts)) 360 + Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion)->Seq.forEach( 361 + elimSub => { 362 + let rule'' = rule'->Rule.substituteBare(elimSub) 363 + Judgment.unify(rule''.conclusion, j, ~gen)->Seq.forEach( 364 + ruleSub => { 365 + let new = { 366 + ruleName, 367 + elimName, 368 + instantiation: ruleInsts, 369 + subgoals: rule.premises->Array.sliceToEnd(~start=1)->Array.map(f), 370 + } 371 + let subst = Judgment.mergeSubsts(elimSub, ruleSub) 372 + ret->Dict.set(`elim ${ruleName} with ${elimName}`, (new, subst)) 373 + }, 374 + ) 375 + }, 376 + ) 377 + }) 378 + }) 379 + ret 380 + } 191 381 } 382 + 192 383 module Lemma = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 193 384 module Rule = Rule.Make(Term, Judgment) 194 385 module Context = Context(Term, Judgment) ··· 204 395 show: f(it.show), 205 396 } 206 397 } 207 - let substitute = (it: t<'a>, subst: Term.subst) => { 398 + let substitute = (it: t<'a>, subst: Judgment.subst) => { 208 399 { 209 400 rule: it.rule->Rule.substitute(subst), 210 401 proof: it.proof,

+51 -8

src/MethodView.res

··· 9 9 scope: array<Term.meta>, 10 10 ruleStyle: RuleView.style, 11 11 gen: Term.gen, 12 - onChange: (Method.t<'a>, Term.subst) => unit, 12 + onChange: (Method.t<'a>, Judgment.subst) => unit, 13 13 } 14 14 type srProps<'a> = { 15 15 "proof": 'a, 16 16 "scope": array<Term.meta>, 17 17 "ruleStyle": RuleView.style, 18 18 "gen": Term.gen, 19 - "onChange": ('a, Term.subst) => unit, 19 + "onChange": ('a, Judgment.subst) => unit, 20 20 } 21 21 let make: (srProps<'a> => React.element) => props<'a> => React.element 22 22 } ··· 28 28 scope: array<Term.meta>, 29 29 ruleStyle: RuleView.style, 30 30 gen: Term.gen, 31 - onChange: (Method.t<'a>, Term.subst) => unit, 31 + onChange: (Method.t<'a>, Judgment.subst) => unit, 32 32 } 33 33 type srProps<'a> = { 34 34 "proof": 'a, 35 35 "scope": array<Term.meta>, 36 36 "ruleStyle": RuleView.style, 37 37 "gen": Term.gen, 38 - "onChange": ('a, Term.subst) => unit, 38 + "onChange": ('a, Judgment.subst) => unit, 39 39 } 40 40 let make = (subRender: srProps<'a> => React.element) => props => { 41 41 <div> ··· 52 52 "scope": props.scope, 53 53 "ruleStyle": props.ruleStyle, 54 54 "gen": props.gen, 55 - "onChange": (newa, subst) => 55 + "onChange": (newa, subst: Judgment.subst) => 56 + props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst), 57 + }, 58 + )} 59 + </li> 60 + }) 61 + ->React.array} 62 + </ul> 63 + </div> 64 + } 65 + } 66 + 67 + module EliminationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 68 + module Method = Elimination(Term, Judgment) 69 + type props<'a> = { 70 + method: Method.t<'a>, 71 + scope: array<Term.meta>, 72 + ruleStyle: RuleView.style, 73 + gen: Term.gen, 74 + onChange: (Method.t<'a>, Judgment.subst) => unit, 75 + } 76 + type srProps<'a> = { 77 + "proof": 'a, 78 + "scope": array<Term.meta>, 79 + "ruleStyle": RuleView.style, 80 + "gen": Term.gen, 81 + "onChange": ('a, Judgment.subst) => unit, 82 + } 83 + let make = (subRender: srProps<'a> => React.element) => props => { 84 + <div> 85 + <b> {React.string("elim ")} </b> 86 + {React.string(`${props.method.ruleName} ${props.method.elimName}`)} 87 + <ul> 88 + {props.method.subgoals 89 + ->Array.mapWithIndex((sg, i) => { 90 + <li key={String.make(i)}> 91 + {React.createElement( 92 + subRender, 93 + { 94 + "proof": sg, 95 + "scope": props.scope, 96 + "ruleStyle": props.ruleStyle, 97 + "gen": props.gen, 98 + "onChange": (newa, subst: Judgment.subst) => 56 99 props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst), 57 100 }, 58 101 )} ··· 75 118 scope: array<Term.meta>, 76 119 ruleStyle: RuleView.style, 77 120 gen: Term.gen, 78 - onChange: (Method.t<'a>, Term.subst) => unit, 121 + onChange: (Method.t<'a>, Judgment.subst) => unit, 79 122 } 80 123 type srProps<'a> = { 81 124 "proof": 'a, 82 125 "scope": array<Term.meta>, 83 126 "ruleStyle": RuleView.style, 84 127 "gen": Term.gen, 85 - "onChange": ('a, Term.subst) => unit, 128 + "onChange": ('a, Judgment.subst) => unit, 86 129 } 87 130 module RuleView = RuleView.Make(Term, Judgment, JudgmentView) 88 131 let make = (subRender: srProps<'a> => React.element) => props => { ··· 129 172 scope: array<Term.meta>, 130 173 ruleStyle: RuleView.style, 131 174 gen: Term.gen, 132 - onChange: (Method.t<'a>, Term.subst) => unit, 175 + onChange: (Method.t<'a>, Judgment.subst) => unit, 133 176 } 134 177 type srProps<'a> = Method1View.srProps<'a> 135 178 let make = (subrender: srProps<'a> => React.element) => props => {

+16 -6

src/Proof.res

··· 24 24 | ProofError({raw: t, rule: Rule.t, msg: string}) 25 25 and checked_option_method = 26 26 | Do(Method.t<checked>) 27 - | Goal(Term.gen => Dict.t<(Method.t<checked>, Term.subst)>) 27 + | Goal(Term.gen => Dict.t<(Method.t<checked>, Judgment.subst)>) 28 28 let parseKeyword = input => { 29 29 Method.keywords 30 30 ->Array.concat(["?"]) 31 31 ->Array.find(kw => String.trim(input)->String.startsWith(kw)) 32 32 } 33 - let rec substitute = (prf: t, subst: Term.subst) => { 33 + let rec substitute = (prf: t, subst: Judgment.subst) => { 34 34 fixes: prf.fixes, 35 35 assumptions: prf.assumptions, 36 36 method: prf.method->Option.map(m => ··· 109 109 } 110 110 } 111 111 let enter = (ctx: Context.t, prf: t, rule: Rule.t) => { 112 + let (nFixes, nVars) = (Array.length(prf.fixes), Array.length(rule.vars)) 112 113 if Array.length(prf.fixes) == Array.length(rule.vars) { 113 - if Array.length(prf.assumptions) == Array.length(rule.premises) { 114 + let (nAssumptions, nPremises) = (Array.length(prf.assumptions), Array.length(rule.premises)) 115 + if nAssumptions == nPremises { 114 116 let newFacts = Dict.fromArray(Belt.Array.zip(prf.assumptions, rule.premises)) 115 117 Ok({ 116 118 Context.fixes: rule.vars->Array.concat(ctx.fixes), 117 119 facts: Dict.copy(ctx.facts)->Dict.assign(newFacts), 118 120 }) 119 121 } else { 120 - Error("Proof introduces a different number of assumptions than the rule") 122 + Error( 123 + `Proof introduces a different number (${Int.toString( 124 + nAssumptions, 125 + )}) of assumptions than the rule (${Int.toString(nPremises)})`, 126 + ) 121 127 } 122 128 } else { 123 - Error("Proof introduces a different number of variables than the rule") 129 + Error( 130 + `Proof introduces a different number (${Int.toString( 131 + nFixes, 132 + )}) of variables than the rule (${Int.toString(nVars)})`, 133 + ) 124 134 } 125 135 } //result<Context, string> 126 136 ··· 180 190 } 181 191 } // result<checked,string> 182 192 183 - let substituteChecked = (prf: checked, ctx: Context.t, subst: Term.subst) => { 193 + let substituteChecked = (prf: checked, ctx: Context.t, subst: Judgment.subst) => { 184 194 switch prf { 185 195 | Checked(prf) => 186 196 check(ctx, Checked(prf)->uncheck->substitute(subst), prf.rule->Rule.substitute(subst))

+1 -1

src/ProofView.res

··· 16 16 scope: array<Term.meta>, 17 17 ruleStyle: RuleView.style, 18 18 gen: Term.gen, 19 - onChange: (Proof.checked, Term.subst) => unit, 19 + onChange: (Proof.checked, Judgment.subst) => unit, 20 20 } 21 21 module RuleView = RuleView.Make(Term, Judgment, JudgmentView) 22 22 @react.componentWithProps

+14 -5

src/Rule.res

··· 5 5 let vinculumRES = "^\s*\\n\\s*[-—][-—][\\-—]+[ \t]*([^()|\\s\\-—][^()\\s]*)?" 6 6 module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 7 7 type rec t = {vars: array<Term.meta>, premises: array<t>, conclusion: Judgment.t} 8 - let rec substitute = (rule: t, subst: Term.subst) => { 9 - let subst' = subst->Term.mapSubst(v => v->Term.upshift(Array.length(rule.vars))) 8 + let rec substitute = (rule: t, subst: Judgment.subst) => { 9 + let subst' = subst->Judgment.mapSubst(v => v->Judgment.upshiftSubstCodom(Array.length(rule.vars))) 10 10 { 11 11 vars: rule.vars, 12 12 premises: rule.premises->Array.map(premise => premise->substitute(subst')), 13 13 conclusion: rule.conclusion->Judgment.substitute(subst'), 14 14 } 15 15 } 16 - let rec substDeBruijn = (rule: t, substs: array<Term.t>, ~from: int=0) => { 16 + let rec substDeBruijn = (rule: t, substs: array<Judgment.substCodom>, ~from: int=0) => { 17 17 let len = Array.length(rule.vars) 18 - let substs' = substs->Array.map(v => v->Term.upshift(len, ~from)) 18 + let substs' = substs->Array.map(v => v->Judgment.upshiftSubstCodom(len, ~from)) 19 19 { 20 20 vars: rule.vars, 21 21 premises: rule.premises->Array.map(premise => ··· 35 35 } 36 36 } 37 37 type bare = {premises: array<t>, conclusion: Judgment.t} 38 - let instantiate = (rule: t, terms: array<Term.t>) => { 38 + let substituteBare = (rule: bare, subst: Judgment.subst) => { 39 + { 40 + premises: rule.premises->Array.map(premise => premise->substitute(subst)), 41 + conclusion: rule.conclusion->Judgment.substitute(subst), 42 + } 43 + } 44 + let instantiate = (rule: t, terms: array<Judgment.substCodom>) => { 39 45 assert(Array.length(terms) == Array.length(rule.vars)) 40 46 let terms' = [...terms] 41 47 Array.reverse(terms') ··· 43 49 premises: rule.premises->Array.map(r => r->substDeBruijn(terms')), 44 50 conclusion: rule.conclusion->Judgment.substDeBruijn(terms')->Judgment.reduce, 45 51 } 52 + } 53 + let schematise = (rule: t, gen: Term.gen, ~scope: array<Judgment.meta>) => { 54 + rule.vars->Array.map(m => Judgment.placeSubstCodom(gen->Term.fresh(~replacing=m), ~scope)) 46 55 } 47 56 let parseRuleName = str => { 48 57 let re = RegExp.fromStringWithFlags(ruleNamePattern, ~flags="y")

+16 -13

src/SExp.res

··· 11 11 type meta = string 12 12 type schematic = int 13 13 type subst = Map.t<schematic, t> 14 - let mapSubst = (m: subst, f: t => t): subst => { 15 - let nu = Map.make() 16 - m->Map.forEachWithKey((v, k) => { 17 - nu->Map.set(k, f(v)) 18 - }) 19 - nu 20 - } 14 + let substEqual = Util.mapEqual 15 + let mapSubst = Util.mapMapValues 21 16 let makeSubst = () => { 22 17 Map.make() 23 18 } ··· 112 107 } 113 108 } 114 109 let unify = (a: t, b: t, ~gen as _=?) => { 115 - switch unifyTerm(a, b) { 116 - | None => [] 117 - | Some(s) => [s] 118 - } 110 + Seq.fromArray( 111 + switch unifyTerm(a, b) { 112 + | None => [] 113 + | Some(s) => [s] 114 + }, 115 + ) 119 116 } 120 117 let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) => 121 118 switch term { ··· 170 167 schematic: x, 171 168 allowed: Array.fromInitializer(~length=Array.length(scope), i => i), 172 169 }) 170 + let mergeSubsts = Util.mapUnion 171 + 173 172 type gen = ref<int> 174 173 let seen = (g: gen, s: int) => { 175 174 if s >= g.contents { ··· 181 180 g := g.contents + 1 182 181 v 183 182 } 184 - let prettyPrintVar = (idx: int, scope: array<string>) => 183 + let prettyPrintVar = (idx: int, scope: array<string>) => { 184 + Console.log(("ppVar", "idx", idx, "scope[idx]", scope[idx], "scope", scope)) 185 185 switch scope[idx] { 186 186 | Some(n) if Array.indexOf(scope, n) == idx => n 187 187 | _ => "\\"->String.concat(String.make(idx)) 188 188 } 189 + } 189 190 let makeGen = () => { 190 191 ref(0) 191 192 } ··· 204 205 ->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e, ~scope)), " ")) 205 206 ->String.concat(")") 206 207 } 207 - let symbolRegexpString = "^([^\\s()]+)" 208 + 209 + let prettyPrintSubst = (sub, ~scope) => Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope)) 210 + let symbolRegexpString = `^([^\\s()\\[\\]]+)` 208 211 let varRegexpString = "^\\\\([0-9]+)$" 209 212 let schematicRegexpString = "^\\?([0-9]+)$" 210 213 type lexeme = LParen | RParen | VarT(int) | SymbolT(string) | SchematicT(int)

+3 -1

src/SExpJView.resi

··· 1 - include Signatures.JUDGMENT_VIEW with module Term := SExp and module Judgment := SExp 1 + include Signatures.JUDGMENT_VIEW 2 + with module Term := SExp 3 + and module Judgment := TermAsJudgment.SExpJ

+26 -7

src/Scratch.res

··· 1 - module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTerm, HOTermJView)) 2 - module InductiveS = Editable.TextArea(InductiveSet.Make(HOTerm, HOTerm, HOTermJView)) 1 + module HOTermJ = TermAsJudgment.HOTermJ 2 + 3 + module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTermJ, HOTermJView)) 4 + module InductiveS = Editable.TextArea(InductiveSet.Make(HOTerm, HOTermJ, HOTermJView)) 3 5 module DerivationsOrLemmasView = MethodView.CombineMethodView( 4 6 HOTerm, 5 - HOTerm, 6 - MethodView.DerivationView(HOTerm, HOTerm), 7 - MethodView.LemmaView(HOTerm, HOTerm, HOTermJView), 7 + HOTermJ, 8 + MethodView.DerivationView(HOTerm, HOTermJ), 9 + MethodView.LemmaView(HOTerm, HOTermJ, HOTermJView), 8 10 ) 9 11 module TheoremS = Editable.TextArea( 10 - Theorem.Make(HOTerm, HOTerm, HOTermJView, DerivationsOrLemmasView), 12 + Theorem.Make(HOTerm, HOTermJ, HOTermJView, DerivationsOrLemmasView), 13 + ) 14 + module ConfS = ConfigBlock.Make(HOTerm, HOTermJ) 15 + 16 + module AxiomStr = Editable.TextArea(StringAxiomSet) 17 + module DerivationsOrLemmasStrView = MethodView.CombineMethodView( 18 + StringTerm, 19 + StringTermJudgment, 20 + MethodView.DerivationView(StringTerm, StringTermJudgment), 21 + MethodView.LemmaView(StringTerm, StringTermJudgment, StringTermJView), 11 22 ) 12 - module ConfS = ConfigBlock.Make(HOTerm, HOTerm) 23 + module DLEStrView = MethodView.CombineMethodView( 24 + StringTerm, 25 + StringTermJudgment, 26 + DerivationsOrLemmasStrView, 27 + MethodView.EliminationView(StringTerm, StringTermJudgment), 28 + ) 29 + module TheoremStr = Editable.TextArea( 30 + Theorem.Make(StringTerm, StringTermJudgment, StringTermJView, DLEStrView), 31 + )

+23 -5

src/Signatures.res

··· 3 3 type schematic 4 4 type meta 5 5 type subst 6 + type gen 6 7 let mapSubst: (subst, t => t) => subst 7 - type gen 8 + let mergeSubsts: (subst, subst) => subst 9 + let substEqual: (subst, subst) => bool 10 + let prettyPrintSubst: (subst, ~scope: array<meta>) => string 8 11 let substitute: (t, subst) => t 12 + let unify: (t, t, ~gen: gen=?) => Seq.t<subst> 9 13 let makeSubst: unit => subst 10 - let unify: (t, t, ~gen: gen=?) => array<subst> 11 14 // law: unify(a,b) == [{}] iff equivalent(a,b) 12 15 let equivalent: (t, t) => bool 13 16 let substDeBruijn: (t, array<t>, ~from: int=?) => t ··· 26 29 module type JUDGMENT = { 27 30 module Term: TERM 28 31 type t 29 - let substitute: (t, Term.subst) => t 32 + type subst 33 + type substCodom 34 + type schematic = Term.schematic 35 + type meta = Term.meta 36 + let mapSubst: (subst, substCodom => substCodom) => subst 37 + let mergeSubsts: (subst, subst) => subst 38 + let substitute: (t, subst) => t 39 + let substituteSubstCodom: (substCodom, subst) => substCodom 30 40 let equivalent: (t, t) => bool 31 - let unify: (t, t, ~gen: Term.gen=?) => array<Term.subst> 32 - let substDeBruijn: (t, array<Term.t>, ~from: int=?) => t 41 + let unify: (t, t, ~gen: Term.gen=?) => Seq.t<subst> 42 + let substDeBruijn: (t, array<substCodom>, ~from: int=?) => t 33 43 let reduce: t => t 34 44 let upshift: (t, int, ~from: int=?) => t 45 + let upshiftSubstCodom: (substCodom, int, ~from: int=?) => substCodom 46 + let placeSubstCodom: (schematic, ~scope: array<meta>) => substCodom 35 47 let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string> 48 + let parseSubstCodom: ( 49 + string, 50 + ~scope: array<Term.meta>, 51 + ~gen: Term.gen=?, 52 + ) => result<(substCodom, string), string> 36 53 let prettyPrint: (t, ~scope: array<Term.meta>) => string 54 + let prettyPrintSubstCodom: (substCodom, ~scope: array<Term.meta>) => string 37 55 } 38 56 39 57 module type TERM_VIEW = {

+157

src/StringAxiomSet.res

··· 1 + open Component 2 + 3 + module Term = StringTerm 4 + module Judgment = StringTermJudgment 5 + module JudgmentView = StringTermJView 6 + 7 + module Rule = Rule.Make(Term, Judgment) 8 + module RuleView = RuleView.Make(Term, Judgment, JudgmentView) 9 + module Ports = Ports(Term, Judgment) 10 + type state = { 11 + raw: dict<Rule.t>, 12 + derived: dict<Rule.t>, 13 + } 14 + 15 + type props = { 16 + content: state, 17 + imports: Ports.t, 18 + onChange: (state, ~exports: Ports.t=?) => unit, 19 + } 20 + 21 + module Set = Belt.Set.String 22 + let varsInRule = (rule: Rule.t) => { 23 + rule.premises->Array.reduce(Set.fromArray(rule.vars), (s, r) => 24 + s->Set.union(Set.fromArray(r.vars)) 25 + ) 26 + } 27 + 28 + let derive = (name: string, rules: array<Rule.t>): Rule.t => { 29 + // TODO: can we remove some of the hardcoding? 30 + let allVars = rules->Array.reduce(Set.empty, (s, r) => s->Set.union(varsInRule(r))) 31 + let rec genVar = (base: string) => { 32 + if allVars->Set.has(base) { 33 + genVar(`${base}'`) 34 + } else { 35 + base 36 + } 37 + } 38 + let (p, b, x, a) = (genVar("P"), genVar("b"), genVar("x"), genVar("a")) 39 + let vars = [p, b, x, a] 40 + let xIdx = vars->Array.findIndex(i => i == x) 41 + let aIdx = vars->Array.findIndex(i => i == a) 42 + let bIdx = vars->Array.findIndex(i => i == b) 43 + let pIdx = vars->Array.findIndex(i => i == p) 44 + let surround = (t: StringTerm.t, aIdx: int, bIdx: int) => { 45 + Array.concat(Array.concat([StringTerm.Var({idx: aIdx})], t), [StringTerm.Var({idx: bIdx})]) 46 + } 47 + let rec replaceJudgeRHS = (rule: Rule.t, aIdx: int, bIdx: int, pIdx: int): Rule.t => { 48 + let n = Array.length(rule.vars) 49 + let (aIdx, bIdx, pIdx) = (aIdx + n, bIdx + n, pIdx + n) 50 + let inductionHyps = 51 + rule.premises 52 + ->Array.filter(r => r.conclusion->snd == Symbol({name: name})) 53 + ->Array.map(r => replaceJudgeRHS(r, aIdx, bIdx, pIdx)) 54 + { 55 + vars: rule.vars, 56 + premises: rule.premises->Array.concat(inductionHyps), 57 + conclusion: (surround(rule.conclusion->fst, aIdx, bIdx), Var({idx: pIdx})), 58 + } 59 + } 60 + { 61 + vars, 62 + premises: Array.concat( 63 + [ 64 + { 65 + Rule.vars: [], 66 + premises: [], 67 + conclusion: ([StringTerm.Var({idx: xIdx})], Symbol({name: name})), 68 + }, 69 + ], 70 + rules->Array.map(r => replaceJudgeRHS(r, aIdx, bIdx, pIdx)), 71 + ), 72 + conclusion: (surround([StringTerm.Var({idx: xIdx})], aIdx, bIdx), Var({idx: pIdx})), 73 + } 74 + } 75 + 76 + let deserialise = (str: string, ~imports as _: Ports.t) => { 77 + let getBase = (str: string) => { 78 + let cur = ref(str) 79 + let go = ref(true) 80 + let results = Dict.make() 81 + let ret = ref(Error("impossible")) 82 + while go.contents { 83 + switch Rule.parseTopLevel(cur.contents, ~scope=[]) { 84 + | Ok((t, n), rest) => 85 + if n->String.trim == "" { 86 + go := false 87 + ret := Error("Rule given with no name") 88 + } else { 89 + Dict.set(results, n, t) 90 + if rest->String.trim == "" { 91 + go := false 92 + ret := Ok(results) 93 + } else { 94 + cur := rest 95 + } 96 + } 97 + | Error(e) => { 98 + go := false 99 + ret := Error(e) 100 + } 101 + } 102 + } 103 + ret.contents 104 + } 105 + getBase(str)->Result.map(raw => { 106 + let grouped: dict<array<Rule.t>> = Dict.make() 107 + raw->Dict.forEach(rule => 108 + switch rule.conclusion->snd { 109 + | Symbol({name: a}) => 110 + switch grouped->Dict.get(a) { 111 + | None => grouped->Dict.set(a, [rule]) 112 + | Some(rs) => rs->Array.push(rule) 113 + } 114 + | _ => () 115 + } 116 + ) 117 + let derived: Dict.t<Rule.t> = Dict.make() 118 + grouped->Dict.forEachWithKey((rules, name) => { 119 + // NOTE: this can clash with other names. is this an issue? 120 + derived->Dict.set(`${name}_induct`, derive(name, rules)) 121 + }) 122 + ({raw, derived}, {Ports.facts: raw->Dict.copy->Dict.assign(derived), ruleStyle: None}) 123 + }) 124 + } 125 + 126 + let serialise = (state: state) => { 127 + state.raw 128 + ->Dict.toArray 129 + ->Array.map(((k, r)) => r->Rule.prettyPrintTopLevel(~name=k)) 130 + ->Array.join("\n") 131 + } 132 + 133 + let make = props => { 134 + let makeRules = content => 135 + <div 136 + className={"axiom-set axiom-set-"->String.concat( 137 + String.make(props.imports.ruleStyle->Option.getOr(Hybrid)), 138 + )}> 139 + {content 140 + ->Dict.toArray 141 + ->Array.mapWithIndex(((n, r), i) => 142 + <RuleView 143 + rule={r} 144 + scope={[]} 145 + key={String.make(i)} 146 + style={props.imports.ruleStyle->Option.getOr(Hybrid)}> 147 + {React.string(n)} 148 + </RuleView> 149 + ) 150 + ->React.array} 151 + </div> 152 + <div> 153 + {makeRules(props.content.raw)} 154 + <p> {React.string("derived")} </p> 155 + {makeRules(props.content.derived)} 156 + </div> 157 + }

+520

src/StringTerm.res

··· 1 + module IntCmp = Belt.Id.MakeComparable({ 2 + type t = int 3 + let cmp = Pervasives.compare 4 + }) 5 + 6 + type piece = 7 + | String(string) 8 + | Var({idx: int}) 9 + | Schematic({schematic: int, allowed: array<int>}) 10 + type t = array<piece> 11 + type meta = string 12 + type schematic = int 13 + type subst = Map.t<schematic, t> 14 + let mapSubst = Util.mapMapValues 15 + let substEqual = Util.mapEqual 16 + let makeSubst = () => Map.make() 17 + let mergeSubsts = Util.mapUnion 18 + 19 + let substitute = (term: t, subst: subst) => 20 + Array.flatMap(term, piece => { 21 + switch piece { 22 + | Schematic({schematic, _}) => 23 + switch Map.get(subst, schematic) { 24 + | None => [piece] 25 + | Some(found) => found 26 + } 27 + | _ => [piece] 28 + } 29 + }) 30 + let schematicsCountsIn: t => Belt.Map.Int.t<int> = (term: t) => 31 + Array.reduce(term, Belt.Map.Int.empty, (m, p) => 32 + switch p { 33 + | Schematic({schematic, _}) => 34 + m->Belt.Map.Int.update(schematic, o => 35 + o 36 + ->Option.map(v => v + 1) 37 + ->Option.orElse(Some(1)) 38 + ) 39 + | _ => m 40 + } 41 + ) 42 + let maxSchematicCount = (term: t) => { 43 + schematicsCountsIn(term)->Belt.Map.Int.maximum->Option.map(snd)->Option.getOr(0) 44 + } 45 + let reduce = t => t 46 + let freeVarsIn = (term: t): Belt.Set.t<int, IntCmp.identity> => 47 + Array.map(term, piece => { 48 + switch piece { 49 + | Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx) 50 + | _ => Belt.Set.make(~id=module(IntCmp)) 51 + } 52 + })->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s1, s2) => Belt.Set.union(s1, s2)) 53 + 54 + let combineSubst = (s: subst, t: subst) => { 55 + let nu = Map.make() 56 + Map.entries(s)->Iterator.forEach(opt => 57 + switch opt { 58 + | None => () 59 + | Some((key, term)) => nu->Map.set(key, term->substitute(t)) 60 + } 61 + ) 62 + Map.entries(t)->Iterator.forEach(opt => 63 + switch opt { 64 + | None => () 65 + | Some((key, term)) => nu->Map.set(key, term->substitute(s)) 66 + } 67 + ) 68 + nu 69 + } 70 + 71 + let emptySubst: subst = Map.make() 72 + let singletonSubst: (int, t) => subst = (schematic, term) => { 73 + let s = Map.make() 74 + s->Map.set(schematic, term) 75 + s 76 + } 77 + 78 + let uncons = (xs: array<'a>): ('a, array<'a>) => { 79 + switch xs { 80 + | [] => Error("expected nonempty array")->Result.getExn 81 + | _ => (xs[0]->Option.getExn, Array.sliceToEnd(xs, ~start=1)) 82 + } 83 + } 84 + 85 + type graphSub = Eps | PieceLitSub(piece) | SchemaSub(int, array<int>) 86 + let unify = (s: array<piece>, t: array<piece>, ~gen as _=?): Seq.t<subst> => { 87 + let match = (p1: piece, p2: piece) => { 88 + switch (p1, p2) { 89 + | (String(na), String(nb)) if na == nb => true 90 + | (Var({idx: ia}), Var({idx: ib})) if ia == ib => true 91 + | (_, _) => false 92 + } 93 + } 94 + let rec oneSide = (s, t) => { 95 + switch (s, t) { 96 + | ([], []) => [emptySubst] 97 + | ([], _) => [] 98 + | (_, _) => { 99 + let (s1, ss) = uncons(s) 100 + switch s1 { 101 + | Schematic({schematic, allowed}) => 102 + Belt.Array.range(0, Array.length(t)) 103 + ->Array.map(i => { 104 + let subTerm = Array.slice(t, ~start=0, ~end=i) 105 + let freeVars = freeVarsIn(subTerm) 106 + let allowedVars = Belt.Set.fromArray(allowed, ~id=module(IntCmp)) 107 + if Belt.Set.subset(freeVars, allowedVars) { 108 + let s1 = singletonSubst(schematic, subTerm) 109 + oneSide( 110 + substitute(ss, s1), 111 + Array.sliceToEnd(t, ~start=i)->substitute(s1), 112 + )->Array.map(s2 => combineSubst(s1, s2)) 113 + } else { 114 + [] 115 + } 116 + }) 117 + ->Array.flat 118 + | _ => 119 + switch t { 120 + | [] => [] 121 + | _ => { 122 + let (t1, ts) = uncons(t) 123 + if match(s1, t1) { 124 + oneSide(ss, ts) 125 + } else { 126 + [] 127 + } 128 + } 129 + } 130 + } 131 + } 132 + } 133 + } 134 + 135 + let pigPug = (s, t) => { 136 + let search = (targetCycles: int): (array<subst>, bool) => { 137 + let moreSolsMightExist = ref(false) 138 + // seen is an assoc list 139 + let rec inner = (s, t, cycle: int, seen: array<((t, t), int)>): array< 140 + array<(int, graphSub)>, 141 + > => { 142 + let (newSeen, thisCycle) = switch seen->Array.findIndexOpt(((e, _)) => e == (s, t)) { 143 + | Some(i) => { 144 + let (_, thisCycle) = seen[i]->Option.getExn 145 + let newSeen = seen->Array.mapWithIndex((e, j) => i == j ? ((s, t), cycle + 1) : e) 146 + (newSeen, thisCycle) 147 + } 148 + 149 + | None => (Array.concat([((s, t), 1)], seen), 0) 150 + } 151 + let cycle = max(thisCycle, cycle) 152 + let searchSub = (schematic: int, allowed: array<int>, edge: graphSub): array< 153 + array<(int, graphSub)>, 154 + > => { 155 + let piece = Schematic({schematic, allowed}) 156 + let sub = switch edge { 157 + | Eps => singletonSubst(schematic, []) 158 + | PieceLitSub(p) => singletonSubst(schematic, [p, piece]) 159 + | SchemaSub(s2, a2) => 160 + singletonSubst(schematic, [Schematic({schematic: s2, allowed: a2}), piece]) 161 + } 162 + inner(substitute(s, sub), substitute(t, sub), cycle, newSeen)->Array.map(path => 163 + Array.concat(path, [(schematic, edge)]) 164 + ) 165 + } 166 + if cycle > targetCycles { 167 + moreSolsMightExist := true 168 + [] 169 + } else { 170 + switch (s[0], t[0]) { 171 + | (None, None) => cycle == targetCycles ? [[]] : [] 172 + | (Some(Schematic({schematic, allowed})), other) 173 + | (other, Some(Schematic({schematic, allowed}))) => 174 + switch other { 175 + | None => searchSub(schematic, allowed, Eps) 176 + | Some(p) => 177 + switch p { 178 + | String(_) => 179 + Array.concat( 180 + searchSub(schematic, allowed, PieceLitSub(p)), 181 + searchSub(schematic, allowed, Eps), 182 + ) 183 + | Schematic({schematic: s2, allowed: a2}) => 184 + if schematic == s2 { 185 + inner( 186 + s->Array.sliceToEnd(~start=1), 187 + t->Array.sliceToEnd(~start=1), 188 + cycle, 189 + newSeen, 190 + ) 191 + } else { 192 + Array.concat( 193 + searchSub(schematic, allowed, Eps), 194 + searchSub(schematic, allowed, SchemaSub(s2, a2)), 195 + ) 196 + } 197 + | Var({idx}) => 198 + if Belt.Set.Int.fromArray(allowed)->Belt.Set.Int.has(idx) { 199 + Array.concat( 200 + searchSub(schematic, allowed, PieceLitSub(p)), 201 + searchSub(schematic, allowed, Eps), 202 + ) 203 + } else { 204 + searchSub(schematic, allowed, Eps) 205 + } 206 + } 207 + } 208 + | (p1, p2) if p1 == p2 => 209 + inner(s->Array.sliceToEnd(~start=1), t->Array.sliceToEnd(~start=1), cycle, newSeen) 210 + | _ => [] 211 + } 212 + } 213 + } 214 + let paths = inner(s, t, 0, []) 215 + let substs = paths->Array.map(path => { 216 + let sub = Map.make() 217 + path->Array.forEach(((schem, edge)) => { 218 + Map.set( 219 + sub, 220 + schem, 221 + switch edge { 222 + | Eps => [] 223 + | PieceLitSub(p) => Array.concat(Map.get(sub, schem)->Option.getOr([]), [p]) 224 + | SchemaSub(s2, _) => 225 + Array.concat( 226 + Map.get(sub, schem)->Option.getOr([]), 227 + Map.get(sub, s2)->Option.getOr([]), 228 + ) 229 + }, 230 + ) 231 + }) 232 + sub 233 + }) 234 + let substsSorted = substs->Array.toSorted((s1, s2) => { 235 + let substLength = s => 236 + s 237 + ->Util.mapMapValues(Array.length) 238 + ->Map.values 239 + ->Iterator.toArray 240 + ->Array.reduce(0, (acc, v) => acc + v) 241 + let (s1Length, s2Length) = (substLength(s1), substLength(s2)) 242 + s1Length < s2Length 243 + ? Ordering.less 244 + : s2Length < s1Length 245 + ? Ordering.greater 246 + : Ordering.equal 247 + }) 248 + (substsSorted, moreSolsMightExist.contents) 249 + } 250 + Seq.unfold((0, true), ((c, moreSolsMightExist)) => { 251 + if moreSolsMightExist { 252 + let (substs, moreSolsMightExist) = search(c) 253 + Some(substs->Seq.fromArray, (c + 1, moreSolsMightExist)) 254 + } else { 255 + None 256 + } 257 + })->Seq.flatten 258 + } 259 + 260 + // naive: assume schematics appear in at most one side 261 + let maxCountS = maxSchematicCount(s) 262 + let maxCountT = maxSchematicCount(t) 263 + if maxCountS == 0 { 264 + Seq.fromArray(oneSide(t, s)) 265 + } else if maxCountT == 0 { 266 + Seq.fromArray(oneSide(s, t)) 267 + } else if max(maxCountS, maxCountT) <= 2 { 268 + pigPug(s, t) 269 + } else { 270 + Seq.fromArray([]) 271 + } 272 + } 273 + 274 + // law: unify(a,b) == [{}] iff equivalent(a,b) 275 + let equivalent: (t, t) => bool = (s, t) => s == t 276 + let substDeBruijn = (string: t, substs: array<t>, ~from: int=0) => { 277 + Array.flatMap(string, piece => 278 + switch piece { 279 + | String(_) => [piece] 280 + | Var({idx: var}) => 281 + if var < from { 282 + [piece] 283 + } else if var - from < Array.length(substs) && var - from >= 0 { 284 + Option.getUnsafe(substs[var - from]) 285 + } else { 286 + [Var({idx: var - Array.length(substs)})] 287 + } 288 + | Schematic({schematic, allowed}) => [ 289 + Schematic({ 290 + schematic, 291 + allowed: Array.filterMap(allowed, i => 292 + if i < from + Array.length(substs) { 293 + None 294 + } else { 295 + Some(i - (from + Array.length(substs))) 296 + } 297 + ), 298 + }), 299 + ] 300 + } 301 + ) 302 + } 303 + 304 + let upshift = (term: t, amount: int, ~from: int=0) => 305 + Array.map(term, piece => { 306 + switch piece { 307 + | String(_) => piece 308 + | Var({idx}) => 309 + Var({ 310 + idx: if idx >= from { 311 + idx + amount 312 + } else { 313 + idx 314 + }, 315 + }) 316 + | Schematic({schematic, allowed}) => 317 + Schematic({ 318 + schematic, 319 + allowed: Array.map(allowed, i => 320 + if i >= from { 321 + i + amount 322 + } else { 323 + i 324 + } 325 + ), 326 + }) 327 + } 328 + }) 329 + 330 + let place = (x: int, ~scope: array<string>) => [ 331 + Schematic({ 332 + schematic: x, 333 + allowed: Array.fromInitializer(~length=Array.length(scope), i => i), 334 + }), 335 + ] 336 + 337 + type gen = ref<int> 338 + let seen = (g: gen, s: int) => { 339 + if s >= g.contents { 340 + g := s + 1 341 + } 342 + } 343 + let fresh = (g: gen, ~replacing as _=?) => { 344 + let v = g.contents 345 + g := g.contents + 1 346 + v 347 + } 348 + let makeGen = () => { 349 + ref(0) 350 + } 351 + 352 + let parseMeta = (str: string) => { 353 + let re = %re("/^([^\s.\[\]()]+)\./y") 354 + switch re->RegExp.exec(str->String.trim) { 355 + | None => Error("not a meta name") 356 + | Some(res) => 357 + switch RegExp.Result.matches(res) { 358 + | [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re))) 359 + | _ => Error("impossible happened") 360 + } 361 + } 362 + } 363 + let prettyPrintVar = (idx: int, scope: array<string>) => 364 + "$" ++ 365 + switch scope[idx] { 366 + | Some(n) if Array.indexOf(scope, n) == idx => n 367 + | _ => "\\"->String.concat(String.make(idx)) 368 + } 369 + let prettyPrint = (term: t, ~scope: array<string>) => 370 + `"${Array.map(term, piece => { 371 + switch piece { 372 + | String(str) => str 373 + | Var({idx}) => prettyPrintVar(idx, scope) 374 + | Schematic({schematic, allowed}) => { 375 + let allowedStr = 376 + allowed 377 + ->Array.map(idx => prettyPrintVar(idx, scope)) 378 + ->Array.join(" ") 379 + `?${Int.toString(schematic)}(${allowedStr})` 380 + } 381 + } 382 + })->Array.join(" ")}"` 383 + let prettyPrintMeta = (str: string) => `${str}.` 384 + let prettyPrintSubst = (sub, ~scope) => Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope)) 385 + 386 + type remaining = string 387 + type errorMessage = string 388 + type ident = string 389 + let parse: (string, ~scope: array<meta>, ~gen: gen=?) => result<(t, remaining), errorMessage> = ( 390 + str: string, 391 + ~scope: array<ident>, 392 + ~gen as _=?, 393 + ) => { 394 + let pos = ref(0) 395 + let seenCloseString = ref(false) 396 + let acc = ref(Ok([])) 397 + 398 + let error = (msg: errorMessage) => { 399 + let codeAroundLoc = String.slice(str, ~start=pos.contents, ~end=pos.contents + 5) 400 + acc := Error(`problem here: ${codeAroundLoc}...: ${msg}`) 401 + } 402 + 403 + let execRe = Util.execRe 404 + let advance = n => { 405 + pos := pos.contents + n 406 + } 407 + let advance1 = () => advance(1) 408 + let add = (token, ~nAdvance=?) => { 409 + acc.contents 410 + ->Result.map(acc => { 411 + Array.push(acc, token) 412 + }) 413 + ->ignore 414 + Option.map(nAdvance, advance)->ignore 415 + } 416 + let execRe = re => execRe(re, String.sliceToEnd(str, ~start=pos.contents)) 417 + let stringLit = () => { 418 + let identRegex = RegExp.fromString(`^${Util.identRegexStr}`) 419 + let symbolRegex = %re(`/^([!@#\$%\^~&*_+\-={};':|,.<>\/?]+)/`) 420 + let numberRegex = %re(`/^(\d+)/`) 421 + switch execRe(identRegex) 422 + ->Option.orElse(execRe(symbolRegex)) 423 + ->Option.orElse(execRe(numberRegex)) { 424 + | Some([match], l) => add(String(match), ~nAdvance=l) 425 + | Some(_) => error("regex string lit error") 426 + | None => error("expected string") 427 + } 428 + } 429 + let escaped = () => { 430 + let escapedRegex = %re(`/\$[\$\?\\\"])/`) 431 + switch execRe(escapedRegex) { 432 + | Some([char], l) => add(String(char), ~nAdvance=l) 433 + | Some(_) => error("regex escaped error") 434 + | None => error("expected valid escaped character") 435 + } 436 + } 437 + let readInt = s => Int.fromString(s)->Option.getExn 438 + let schema = () => { 439 + let schemaRegex = %re("/\?(\d+)\(((?:\d+\s*)*)$/") 440 + switch execRe(schemaRegex) { 441 + | Some([idStr, allowedStr], l) => { 442 + let schematic = readInt(idStr) 443 + let allowed = 444 + allowedStr 445 + ->String.trim 446 + ->String.splitByRegExp(%re("/\s+/")) 447 + ->Array.keepSome 448 + ->Array.filter(s => s != "") 449 + ->Array.map(readInt) 450 + add(Schematic({schematic, allowed}), ~nAdvance=l) 451 + } 452 + | Some(_) => error("schema lit regex error") 453 + | None => error("expected schematic literal") 454 + } 455 + } 456 + let var = () => { 457 + let varLitRegex = %re("/^\$\\(\d+)/") 458 + let varScopeRegex = %re("/^\$([a-zA-Z]\w*)/") 459 + switch execRe(varLitRegex) { 460 + | Some([match], l) => add(Var({idx: readInt(match)}), ~nAdvance=l) 461 + | Some(_) => error("var lit regex error") 462 + | None => 463 + switch execRe(varScopeRegex) { 464 + | Some([ident], l) => 465 + switch Array.indexOfOpt(scope, ident) { 466 + | Some(idx) => add(Var({idx: idx}), ~nAdvance=l) 467 + | None => error("expected variable in scope") 468 + } 469 + | Some(_) => error("var regex error") 470 + | None => error("expected var") 471 + } 472 + } 473 + } 474 + 475 + // consume leading whitespace + open quote 476 + switch execRe(%re(`/^\s*"/`)) { 477 + | Some(_, l) => pos := l 478 + | None => error("expected open quote") 479 + } 480 + while ( 481 + pos.contents < String.length(str) && Result.isOk(acc.contents) && !seenCloseString.contents 482 + ) { 483 + let c = String.get(str, pos.contents)->Option.getExn 484 + switch c { 485 + | "\"" => { 486 + advance1() 487 + seenCloseString := true 488 + } 489 + | "$" => var() 490 + | "?" => schema() 491 + | " " | "\t" | "\r" | "\n" => advance1() 492 + | ")" | "(" | "[" | "]" => add(String(c), ~nAdvance=1) 493 + | "\\" => escaped() 494 + | _ => stringLit() 495 + } 496 + } 497 + 498 + acc.contents->Result.map(r => (r, str->String.sliceToEnd(~start=pos.contents))) 499 + } 500 + 501 + let toSExp = t => { 502 + let convertPiece = p => 503 + switch p { 504 + | String(s) => SExp.Symbol({name: s}) 505 + | Var({idx}) => SExp.Var({idx: idx}) 506 + | Schematic({schematic, allowed}) => SExp.Schematic({schematic, allowed}) 507 + } 508 + switch Array.length(t) { 509 + | 1 => convertPiece(t[0]->Option.getExn) 510 + | _ => SExp.Compound({subexps: Array.map(t, convertPiece)}) 511 + } 512 + } 513 + 514 + let rec fromSExp = (t: SExp.t) => 515 + switch t { 516 + | SExp.Symbol({name}) => [String(name)] 517 + | SExp.Schematic({schematic, allowed}) => [Schematic({schematic, allowed})] 518 + | SExp.Var({idx}) => [Var({idx: idx})] 519 + | SExp.Compound({subexps}) => subexps->Array.flatMap(fromSExp) 520 + }

+15

src/StringTerm.resi

··· 1 + type rec piece = 2 + | String(string) 3 + | Var({idx: int}) 4 + | Schematic({schematic: int, allowed: array<int>}) 5 + type t = array<piece> 6 + type subst = Map.t<int, t> 7 + 8 + include Signatures.TERM 9 + with type t := t 10 + and type meta = string 11 + and type schematic = int 12 + and type subst := subst 13 + 14 + let fromSExp: SExp.t => t 15 + let toSExp: t => SExp.t

+12

src/StringTermJView.res

··· 1 + module TermView = StringTermView 2 + type props = { 3 + judgment: StringTermJudgment.t, 4 + scope: array<string>, 5 + } 6 + let make = ({judgment: (term, j), scope}) => { 7 + <span className="term-compound"> 8 + <StringTermView term scope /> 9 + {React.string(" ")} 10 + <SExpView term=j scope /> 11 + </span> 12 + }

+3

src/StringTermJView.resi

··· 1 + include Signatures.JUDGMENT_VIEW 2 + with module Term := StringTerm 3 + and module Judgment := StringTermJudgment

+109

src/StringTermJudgment.res

··· 1 + type t = (StringTerm.t, SExp.t) 2 + type substCodom = StringV(StringTerm.t) | SExpV(SExp.t) 3 + type subst = Map.t<int, substCodom> 4 + type schematic = int 5 + type meta = string 6 + 7 + let mapSubst = Util.mapMapValues 8 + let mergeSubsts: (subst, subst) => subst = Util.mapUnion 9 + let splitSub: subst => (StringTerm.subst, SExp.subst) = s => { 10 + let stringSub = Map.make() 11 + let judgeSub = Map.make() 12 + s->Map.forEachWithKey((v, k) => { 13 + switch v { 14 + | StringV(t) => { 15 + stringSub->Map.set(k, t) 16 + judgeSub->Map.set(k, t->StringTerm.toSExp) 17 + } 18 + | SExpV(t) => { 19 + stringSub->Map.set(k, t->StringTerm.fromSExp) 20 + judgeSub->Map.set(k, t) 21 + } 22 + } 23 + }) 24 + (stringSub, judgeSub) 25 + } 26 + let substitute = ((term, judge): t, sub) => { 27 + let (stringSub, judgeSub) = splitSub(sub) 28 + (StringTerm.substitute(term, stringSub), SExp.substitute(judge, judgeSub)) 29 + } 30 + 31 + let substituteSubstCodom = (s: substCodom, subst: subst) => { 32 + let (stringSub, judgeSub) = splitSub(subst) 33 + switch s { 34 + | StringV(t) => StringV(StringTerm.substitute(t, stringSub)) 35 + | SExpV(t) => SExpV(SExp.substitute(t, judgeSub)) 36 + } 37 + } 38 + let equivalent = ((t1, j1): t, (t2, j2): t) => 39 + StringTerm.equivalent(t1, t2) && SExp.equivalent(j1, j2) 40 + let reduce = t => t 41 + let unify = ((t1, j1): t, (t2, j2): t, ~gen as _=?) => { 42 + // cartesian prod of possible unifications 43 + let judgeSubs = SExp.unify(j1, j2)->Seq.map(s => s->Util.mapMapValues(t => SExpV(t))) 44 + let stringSubs = StringTerm.unify(t1, t2)->Seq.map(s => s->Util.mapMapValues(t => StringV(t))) 45 + judgeSubs->Seq.flatMap(judgeSub => 46 + // NOTE: silent failure mode here where substitution exists for a given schematic on both string 47 + // SExp side. for now, bias string sub. in future, maybe consider this not a valid judgement to begin with. 48 + stringSubs->Seq.map(stringSub => Util.mapUnion(stringSub, judgeSub)) 49 + ) 50 + } 51 + let substDeBruijn = ((t, j): t, scope: array<substCodom>, ~from: int=0) => { 52 + // NOTE: implicit type coercion here. if we unify and expect a string but get an sexp, 53 + // perform naive flattening of compound to substitute. likewise in opposite direction. 54 + let stringScope = scope->Array.map(v => 55 + switch v { 56 + | StringV(t) => t 57 + | SExpV(t) => StringTerm.fromSExp(t) 58 + } 59 + ) 60 + let judgeScope = scope->Array.map(v => 61 + switch v { 62 + | SExpV(t) => t 63 + | StringV(t) => StringTerm.toSExp(t) 64 + } 65 + ) 66 + (StringTerm.substDeBruijn(t, stringScope, ~from), SExp.substDeBruijn(j, judgeScope, ~from)) 67 + } 68 + let upshift = ((t, j): t, amount: int, ~from: int=0) => ( 69 + StringTerm.upshift(t, amount, ~from), 70 + SExp.upshift(j, amount, ~from), 71 + ) 72 + 73 + let upshiftSubstCodom = (v: substCodom, amount: int, ~from: int=0) => 74 + switch v { 75 + | StringV(t) => StringV(StringTerm.upshift(t, amount, ~from)) 76 + | SExpV(j) => SExpV(SExp.upshift(j, amount, ~from)) 77 + } 78 + 79 + let parse = (str: string, ~scope: array<StringTerm.meta>, ~gen=?) => { 80 + StringTerm.parse(str, ~scope, ~gen?)->Result.flatMap(((t, str)) => 81 + SExp.parse(str, ~scope)->Result.map(((j, str)) => ((t, j), str)) 82 + ) 83 + } 84 + 85 + // HACK: this does work due to the hacky string-sexp conversion we have inplace with substitutions, 86 + // but a different solution would be preferable 87 + let placeSubstCodom = (x: int, ~scope: array<string>) => StringV(StringTerm.place(x, ~scope)) 88 + 89 + let parseSubstCodom = (str: string, ~scope: array<StringTerm.meta>, ~gen=?) => { 90 + switch StringTerm.parse(str, ~scope, ~gen?) { 91 + | Ok(t, str) => Ok(StringV(t), str) 92 + | Error(stringE) => 93 + switch SExp.parse(str, ~scope) { 94 + | Ok(t, str) => Ok(SExpV(t), str) 95 + | Error(sExpE) => 96 + Error( 97 + `string or sexp expected.\nstring parsing failed with error: ${stringE}\nsexp parsing failed with error: ${sExpE}`, 98 + ) 99 + } 100 + } 101 + } 102 + 103 + let prettyPrint = ((t, j): t, ~scope: array<StringTerm.meta>) => 104 + `${StringTerm.prettyPrint(t, ~scope)} ${SExp.prettyPrint(j, ~scope)}` 105 + let prettyPrintSubstCodom = (v: substCodom, ~scope: array<StringTerm.meta>) => 106 + switch v { 107 + | StringV(t) => StringTerm.prettyPrint(t, ~scope) 108 + | SExpV(t) => SExp.prettyPrint(t, ~scope) 109 + }

+3

src/StringTermJudgment.resi

··· 1 + type t = (StringTerm.t, SExp.t) 2 + 3 + include Signatures.JUDGMENT with module Term := StringTerm and type t := t

+64

src/StringTermView.res

··· 1 + type props = {term: StringTerm.t, scope: array<string>} 2 + type idx_props = {idx: int, scope: array<string>} 3 + let viewVar = (props: idx_props) => 4 + switch props.scope[props.idx] { 5 + | Some(n) if Array.indexOf(props.scope, n) == props.idx => 6 + <span className="term-metavar"> {React.string(n)} </span> 7 + | _ => 8 + <span className="term-metavar-unnamed"> 9 + {React.string("\\")} 10 + {React.int(props.idx)} 11 + </span> 12 + } 13 + 14 + let makeMeta = (str: string) => 15 + <span className="rule-binder"> 16 + {React.string(str)} 17 + {React.string(".")} 18 + </span> 19 + 20 + let parenthesise = f => 21 + [ 22 + <span className="symbol" key={"-1"}> {React.string("(")} </span>, 23 + ...f, 24 + <span className="symbol" key={"-2"}> {React.string(")")} </span>, 25 + ] 26 + 27 + let intersperse = a => Util.intersperse(a, ~with=React.string(" ")) 28 + 29 + module Piece = { 30 + @react.component 31 + let make = (~piece: StringTerm.piece, ~scope) => 32 + switch piece { 33 + | Var({idx}) => viewVar({idx, scope}) 34 + | String(s) => <span className="term-const"> {React.string(s)} </span> 35 + | Schematic({schematic: s, allowed: vs}) => 36 + <span className="term-schematic"> 37 + {React.string("?")} 38 + {React.int(s)} 39 + <span className="term-schematic-telescope"> 40 + {vs 41 + ->Array.mapWithIndex((v, i) => 42 + React.createElement(viewVar, Util.withKey({idx: v, scope}, i)) 43 + ) 44 + ->intersperse 45 + ->parenthesise 46 + ->React.array} 47 + </span> 48 + </span> 49 + } 50 + } 51 + 52 + @react.componentWithProps 53 + let make = ({term, scope}) => 54 + <span className="term-compound"> 55 + {React.string("\"")} 56 + {term 57 + ->Array.mapWithIndex((piece, i) => { 58 + let key = Int.toString(i) 59 + <Piece piece scope key /> 60 + }) 61 + ->intersperse 62 + ->React.array} 63 + {React.string("\"")} 64 + </span>

+1

src/StringTermView.resi

··· 1 + include Signatures.TERM_VIEW with module Term := StringTerm

+14

src/TermAsJudgment.res

··· 1 + open Signatures 2 + 3 + module Make = (Term: TERM): (JUDGMENT with module Term := Term and type t = Term.t) => { 4 + include Term 5 + type substCodom = Term.t 6 + let prettyPrintSubstCodom = Term.prettyPrint 7 + let parseSubstCodom = Term.parse 8 + let placeSubstCodom = Term.place 9 + let upshiftSubstCodom = Term.upshift 10 + let substituteSubstCodom = Term.substitute 11 + } 12 + 13 + module SExpJ = Make(SExp) 14 + module HOTermJ = Make(HOTerm)

+105

src/Util.res

··· 1 1 let newline = "\n" 2 + let mapMapValues = (m: Map.t<'a, 'b>, f: 'b => 'c) => { 3 + let nu = Map.make() 4 + m->Map.forEachWithKey((v, k) => { 5 + nu->Map.set(k, f(v)) 6 + }) 7 + nu 8 + } 9 + 10 + @send external toString: 'a => string = "toString" 11 + let showArray: array<'a> => string = a => `[${Array.toString(a)}]` 12 + let showTuple: (('a, 'b)) => string = ((a, b)) => `(${toString(a)} ${toString(b)})` 13 + 14 + let prettyPrintMap = ( 15 + m: Map.t<'k, 'v>, 16 + ~showK: 'k => string=toString, 17 + ~showV: 'v => string=toString, 18 + ) => { 19 + m 20 + ->Map.entries 21 + ->Iterator.toArray 22 + ->Array.map(((k, v)) => { 23 + (showK(k), showV(v)) 24 + }) 25 + ->showArray 26 + } 27 + 28 + let prettyPrintIntMap = (m: Belt.Map.Int.t<'v>, ~showV: 'v => string=toString) => { 29 + m 30 + ->Belt.Map.Int.toArray 31 + ->Array.map(((k, v)) => { 32 + (Int.toString(k), showV(v)) 33 + }) 34 + ->showArray 35 + } 36 + 37 + let mapIntersectionWith = (m1: Map.t<'k, 'a>, m2: Map.t<'k, 'b>, f: ('a, 'b) => 'c) => { 38 + let go = (m1, m2) => { 39 + let nu: Map.t<'k, 'c> = Map.make() 40 + m1->Map.forEachWithKey((v1, k) => { 41 + switch m2->Map.get(k) { 42 + | Some(v2) => nu->Map.set(k, f(v1, v2)) 43 + | None => () 44 + } 45 + }) 46 + nu 47 + } 48 + if Map.size(m1) < Map.size(m2) { 49 + go(m1, m2) 50 + } else { 51 + go(m2, m1) 52 + } 53 + } 54 + 55 + let mapUnionWith = (m1: Map.t<'k, 'a>, m2: Map.t<'k, 'a>, f: ('a, 'a) => 'a) => { 56 + let nu = Map.make() 57 + m1->Map.forEachWithKey((v1, k) => { 58 + switch m2->Map.get(k) { 59 + | Some(v2) => nu->Map.set(k, f(v1, v2)) 60 + | None => nu->Map.set(k, v1) 61 + } 62 + }) 63 + m2->Map.forEachWithKey((v, k) => { 64 + switch nu->Map.get(k) { 65 + | Some(_) => () 66 + | None => nu->Map.set(k, v) 67 + } 68 + }) 69 + nu 70 + } 71 + 72 + // left biased 73 + let mapUnion = (m1, m2) => mapUnionWith(m1, m2, (v1, _v2) => v1) 74 + 75 + let mapIntersection = (m1: Map.t<'k, 'a>, m2: Map.t<'k, 'b>): Map.t<'k, ('a, 'b)> => 76 + mapIntersectionWith(m1, m2, (b, c) => (b, c)) 77 + 2 78 let withKey: ('props, int) => 'props = %raw(`(props, key) => ({...props, key})`) 3 79 80 + let mapEqual = (m1, m2) => { 81 + Map.size(m1) == Map.size(m1) && 82 + mapIntersection(m1, m2) 83 + ->Map.values 84 + ->Iterator.toArray 85 + ->Array.filter(((a, b)) => a == b) 86 + ->Array.length == Map.size(m2) 87 + } 88 + 4 89 let arrayWithIndex = (arr: array<React.element>) => { 5 90 React.array(arr->Array.mapWithIndex((m, i) => <span key={String.make(i)}> m </span>)) 6 91 } 92 + let execRe = (re, str) => { 93 + re 94 + ->RegExp.exec(str) 95 + ->Option.map(result => { 96 + open RegExp.Result 97 + (matches(result), fullMatch(result)->String.length) 98 + }) 99 + } 100 + 101 + let identRegexStr = `([a-zA-Z][a-zA-Z\\d]*)` 102 + 103 + let intersperse = (a: array<'a>, ~with: 'a) => 104 + a->Array.flatMapWithIndex((e, i) => 105 + if i == 0 { 106 + [e] 107 + } else { 108 + [with, e] 109 + } 110 + ) 111 + 7 112 exception Unreachable(string) 8 113 exception Err(string) 9 114 let mustFindIndex = (arr, f) => {

+11 -12

src/testcomponent.tsx

··· 1 - import * as ComponentGraph from './componentgraph' 2 - import { AxiomS, ConfS, TheoremS, InductiveS } from './Scratch.mjs' 3 - import ReactDOM from 'react-dom/client'; 4 - import React from 'react'; 5 - 6 - 1 + import * as ComponentGraph from "./componentgraph"; 2 + import { AxiomS, ConfS, TheoremS, InductiveS, AxiomStr, TheoremStr } from "./Scratch.mjs"; 3 + import ReactDOM from "react-dom/client"; 4 + import React from "react"; 7 5 8 - 9 - type Component = ComponentGraph.Component 6 + type Component = ComponentGraph.Component; 10 7 11 8 //A bridge between any module that implements the COMPONENT signature from ReScript-land 12 9 //and a ComponentGraph component. ··· 75 72 76 73 window.localStorage.clear() 77 74 ComponentGraph.setup({ 78 - "hol-comp": HolComp(AxiomS), 75 + "hol-comp": HolComp(AxiomS), 79 76 "hol-inductive": HolComp(InductiveS), 80 - "hol-config":HolComp(ConfS), 81 - "hol-proof": HolComp(TheoremS) 82 - }); 77 + "hol-config": HolComp(ConfS), 78 + "hol-proof": HolComp(TheoremS), 79 + "hol-string": HolComp(AxiomStr), 80 + "hol-string-proof": HolComp(TheoremStr), 81 + }); //"hol-config": ConfigComponent, "hol-proof":ProofComponent});

+11 -11

tests/HOTermTest.res

··· 136 136 let x = "x" 137 137 let y = "y" 138 138 t->testUnify(x, x) 139 - t->Util.testNotUnify(y, x) 140 - t->Util.testNotUnify(x, y) 139 + t->Util.testUnifyFail(y, x) 140 + t->Util.testUnifyFail(x, y) 141 141 }) 142 142 t->block("applications", t => { 143 143 let ab = "(a b)" 144 144 let cd = "(c d)" 145 145 t->testUnify(ab, ab) 146 146 t->testUnify(cd, cd) 147 - t->Util.testNotUnify(ab, cd) 148 - t->Util.testNotUnify(cd, ab) 147 + t->Util.testUnifyFail(ab, cd) 148 + t->Util.testUnifyFail(cd, ab) 149 149 }) 150 150 t->block("flex-rigid", t => { 151 151 let x = "?0" ··· 175 175 t->block("flex-rigid", t => { 176 176 let x = "(?0 \\10)" 177 177 let y = "(r (fst \\10))" 178 - t->Util.testUnify( 178 + t->Util.testUnify1( 179 179 x, 180 180 y, 181 181 ~subst=emptySubst->substAdd( ··· 193 193 t->block("flex-rigid-fcu-2", t => { 194 194 let x = "(?0 (fst \\10))" 195 195 let y = "(r (fst (fst \\10)))" 196 - t->Util.testUnify( 196 + t->Util.testUnify1( 197 197 x, 198 198 y, 199 199 ~subst=emptySubst->substAdd( ··· 205 205 t->block("flex-rigid-fcu-3", t => { 206 206 let x = "(?1 (fst \\10) (snd \\1))" 207 207 let y = "(r (q (snd \\1) (fst \\10)))" 208 - t->Util.testUnify( 208 + t->Util.testUnify1( 209 209 x, 210 210 y, 211 211 ~subst=emptySubst->substAdd( ··· 217 217 t->block("flex-rigid-fcu-4", t => { 218 218 let x = "(?1 (fst \\10) \\1)" 219 219 let y = "(r (q (snd \\1) (fst \\10)))" 220 - t->Util.testUnify( 220 + t->Util.testUnify1( 221 221 x, 222 222 y, 223 223 ~subst=emptySubst->substAdd( ··· 252 252 let a = "(x. ?0 x)" 253 253 let b = "(x. f (?0 x))" 254 254 // ?0 occurs in the rigid term on the right → should not unify 255 - t->Util.testNotUnify(a, b) 255 + t->Util.testUnifyFail(a, b) 256 256 }) 257 257 t->block("no capture", t => { 258 258 let a = "(x. ?0)" 259 259 let b = "(x. x)" 260 260 // Should fail: it cannot capture the bound variable. 261 - t->Util.testNotUnify(a, b) 261 + t->Util.testUnifyFail(a, b) 262 262 }) 263 263 t->block("eta", t => { 264 264 t->testUnify( ··· 309 309 let a = "(Nat (S ?6))" 310 310 let b = "(Nat (S (S \\0)))" 311 311 let c = "(Nat (S (?6 \\0)))" 312 - t->Util.testNotUnify(a, b) 312 + t->Util.testUnifyFail(a, b) 313 313 t->testUnify(c, b, ~subst=emptySubst->substAdd(6, t->Util.parse("(x. S \\0)"))) 314 314 }) 315 315 t->block("tests from induction examples", t => {

+53

tests/RuleTest.res

··· 1 + open Signatures 2 + open Zora 3 + 4 + module MakeTest = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 5 + module RuleInst = Rule.Make(Term, Judgment) 6 + let testParseInner = (t: Zora.t, input: string, expect: RuleInst.t, ~scope=[], ~msg=?) => { 7 + let res = RuleInst.parseInner(input, ~scope, ~gen=Term.makeGen()) 8 + switch res { 9 + | Ok(res) => { 10 + t->equal(res->snd, "", ~msg=input ++ " input consumed") 11 + t->equal(res->fst, expect, ~msg?) 12 + } 13 + | Error(msg) => t->fail(~msg="parse failed: " ++ msg) 14 + } 15 + } 16 + let testParseTopLevel = ( 17 + t: Zora.t, 18 + input: string, 19 + expect: (RuleInst.t, string), 20 + ~scope=[], 21 + ~msg=?, 22 + ) => { 23 + let res = RuleInst.parseTopLevel(input, ~scope, ~gen=Term.makeGen()) 24 + switch res { 25 + | Ok(res) => { 26 + t->equal(res->snd, "", ~msg=input ++ " input consumed") 27 + t->equal(res->fst, expect, ~msg?) 28 + } 29 + | Error(msg) => t->fail(~msg="parse failed: " ++ msg) 30 + } 31 + } 32 + } 33 + 34 + zoraBlock("string terms", t => { 35 + module T = MakeTest(StringTerm, StringTermJudgment) 36 + t->T.testParseInner( 37 + `[s1. "$s1" p |- "($s1)" p]`, 38 + { 39 + vars: ["s1"], 40 + premises: [ 41 + { 42 + vars: [], 43 + premises: [], 44 + conclusion: ([StringTerm.Var({idx: 0})], Symbol({name: "p"})), 45 + }, 46 + ], 47 + conclusion: ( 48 + [StringTerm.String("("), StringTerm.Var({idx: 0}), StringTerm.String(")")], 49 + SExp.Symbol({name: "p"}), 50 + ), 51 + }, 52 + ) 53 + })

+27

tests/SExpTest.res

··· 6 6 zoraBlock("parse symbol", t => { 7 7 t->block("single char", t => t->Util.testParse("x", Symbol({name: "x"}))) 8 8 t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz"}))) 9 + t->block("judgement terminal", t => 10 + t->Util.testParse("a]", Symbol({name: "a"}), ~expectRemaining="]") 11 + ) 9 12 }) 10 13 11 14 zoraBlock("parse var", t => { 12 15 t->block("single digit", t => t->Util.testParse("\\1", Var({idx: 1}))) 13 16 t->block("multi digit", t => t->Util.testParse("\\234", Var({idx: 234}))) 17 + t->block("scope", t => t->Util.testParse("p", ~scope=["q", "p"], Var({idx: 1}))) 14 18 }) 15 19 16 20 zoraBlock("parse schematic", t => { ··· 35 39 ) 36 40 }) 37 41 }) 42 + 43 + let parse = (input: string) => SExp.parse(input, ~scope=[], ~gen=SExp.makeGen())->Result.getExn->fst 44 + 45 + zoraBlock("unify var", t => { 46 + let x = parse("x") 47 + let y = parse("y") 48 + let comp1 = parse("(x y z)") 49 + let comp2 = parse("(x a y)") 50 + let schema1 = parse("?1()") 51 + let schemaComp = parse("(?1() a ?2())") 52 + t->block("var eq", t => t->Util.testUnify(x, x, [Map.make()])) 53 + t->block("var neq", t => t->Util.testUnify(x, y, [])) 54 + t->block("comp eq", t => t->Util.testUnify(comp1, comp1, [Map.make()])) 55 + t->block("comp neq", t => t->Util.testUnify(comp1, comp2, [])) 56 + t->block("schema var", t => t->Util.testUnify(schema1, x, [Map.fromArray([(1, x)])])) 57 + t->block("schema comp", t => t->Util.testUnify(schema1, comp2, [Map.fromArray([(1, comp2)])])) 58 + t->block("comp-schema comp eq", t => { 59 + t->Util.testUnify(schemaComp, comp2, [Map.fromArray([(1, x), (2, y)])]) 60 + }) 61 + t->block("comp-schema comp neq", t => { 62 + t->Util.testUnify(schemaComp, comp1, []) 63 + }) 64 + })

+113

tests/StringTermTest.res

··· 1 + open Zora 2 + open StringTerm 3 + 4 + module Util = TestUtil.MakeTerm(StringTerm) 5 + 6 + zoraBlock("parse", t => { 7 + t->block("empty", t => t->Util.testParse(`""`, [])) 8 + t->block("string literal", t => { 9 + t->Util.testParse(`"x"`, [String("x")]) 10 + t->Util.testParse(`"xyz123"`, [String("xyz123")]) 11 + t->Util.testParse(`"123y"`, [String("123"), String("y")]) 12 + t->Util.testParse(`"\\"\\$\\?\\\\"`, [String("\""), String("$"), String("?"), String("\\")]) 13 + t->Util.testParse( 14 + `"y(135ab!!)"`, 15 + [String("y"), String("("), String("135"), String("ab"), String("!!"), String(")")], 16 + ) 17 + t->Util.testParseFail(`foo`) 18 + t->Util.testParseFail(`a b" c`) 19 + }) 20 + t->block("variables", t => { 21 + t->Util.testParse(`"$\\1"`, [Var({idx: 1})]) 22 + t->Util.testParse(`"$\\10"`, [Var({idx: 10})]) 23 + t->Util.testParse(`"$x"`, ~scope=["x"], [Var({idx: 0})]) 24 + t->Util.testParse(`"?1()"`, [Schematic({schematic: 1, allowed: []})]) 25 + t->Util.testParseFail(`"?1"`) 26 + t->Util.testParse(`"?10()"`, [Schematic({schematic: 10, allowed: []})]) 27 + t->Util.testParse(`"?1(1 23 4)"`, [Schematic({schematic: 1, allowed: [1, 23, 4]})]) 28 + }) 29 + t->block("concat", t => { 30 + t->Util.testParse(`"x y"`, [String("x"), String("y")]) 31 + t->Util.testParse(`"x y"`, [String("x"), String("y")]) 32 + t->Util.testParse( 33 + `"x ?1(1 2 3) $\\1 $y"`, 34 + ~scope=["y"], 35 + [String("x"), Schematic({schematic: 1, allowed: [1, 2, 3]}), Var({idx: 1}), Var({idx: 0})], 36 + ) 37 + }) 38 + }) 39 + 40 + let parse = (input: string) => 41 + StringTerm.parse(input, ~scope=[], ~gen=StringTerm.makeGen())->Result.getExn->fst 42 + 43 + zoraBlock("unify", t => { 44 + let a = parse(`"a"`) 45 + let b = parse(`"b"`) 46 + let x = parse(`"?1()"`) 47 + let y = parse(`"?2()"`) 48 + t->block("schematics on at most one side", t => { 49 + t->Util.testUnify(a, a, [Map.make()]) 50 + t->Util.testUnify(x, a, [Map.fromArray([(1, a)])]) 51 + t->Util.testUnify(a, x, [Map.fromArray([(1, a)])]) 52 + 53 + let xy = parse(`"?1() ?2()"`) 54 + let ab = parse(`"a b"`) 55 + t->Util.testUnify(x, ab, [Map.fromArray([(1, ab)])]) 56 + t->Util.testUnify( 57 + xy, 58 + ab, 59 + [ 60 + Map.fromArray([(1, []), (2, ab)]), 61 + Map.fromArray([(1, a), (2, b)]), 62 + Map.fromArray([(1, ab), (2, [])]), 63 + ], 64 + ) 65 + 66 + t->Util.testUnify(parse(`"?1() b ?2()"`), ab, [Map.fromArray([(1, a), (2, [])])]) 67 + t->Util.testUnify( 68 + parse(`"?1() ?2() b"`), 69 + ab, 70 + [Map.fromArray([(1, []), (2, a)]), Map.fromArray([(1, a), (2, [])])], 71 + ) 72 + t->Util.testUnify( 73 + parse(`"a ?1() ?2()"`), 74 + ab, 75 + [Map.fromArray([(1, []), (2, b)]), Map.fromArray([(1, b), (2, [])])], 76 + ) 77 + 78 + let xax = parse(`"?1() a ?1()"`) 79 + t->Util.testUnify(xax, parse(`"a"`), [Map.fromArray([(1, [])])]) 80 + t->Util.testUnify(xax, parse(`"a a a"`), [Map.fromArray([(1, a)])]) 81 + t->Util.testUnify(xax, parse(`"a b a a b"`), [Map.fromArray([(1, parse(`"a b"`))])]) 82 + }) 83 + 84 + t->block("schematics appearing at most twice", t => { 85 + t->Util.testUnify(x, x, [Map.fromArray([(1, [])])]) 86 + t->Util.testUnify(x, y, [Map.fromArray([(1, []), (2, [])])]) 87 + 88 + t->Util.testUnify(a, parse(`"?1() a"`), [Map.fromArray([(1, [])])]) 89 + t->Util.testUnify( 90 + parse(`"?1() a"`), 91 + parse(`"a ?1()"`), 92 + [ 93 + Map.fromArray([(1, [])]), 94 + Map.fromArray([(1, parse(`"a"`))]), 95 + Map.fromArray([(1, parse(`"a a"`))]), 96 + Map.fromArray([(1, parse(`"a a a"`))]), 97 + Map.fromArray([(1, parse(`"a a a a"`))]), 98 + ], 99 + ) 100 + t->Util.testUnify(parse(`"a ?1()"`), parse(`"?2() b`), [Map.fromArray([(1, b), (2, a)])]) 101 + t->Util.testUnify(parse(`"a ?1() a"`), parse(`"?2() b a"`), [Map.fromArray([(1, b), (2, a)])]) 102 + t->Util.testUnify( 103 + parse(`"b ?1() a"`), 104 + parse(`"?2() a ?1()"`), 105 + [Map.fromArray([(1, a), (2, b)]), Map.fromArray([(1, []), (2, b)])], 106 + ) 107 + t->Util.testUnify( 108 + parse(`"a b ?1() c ?2()"`), 109 + parse(`"?2() c ?1() b a"`), 110 + [Map.fromArray([(1, a), (2, parse(`"a b a"`))])], 111 + ) 112 + }) 113 + })

+68 -22

tests/TestUtil.res

··· 11 11 ~msg=msg->Option.getOr(`${stringifyExn(t1)} equivalent to ${stringifyExn(t2)}`), 12 12 ) 13 13 } 14 - let testParse = (t: Zora.t, input: string, t2: Term.t, ~msg=?) => { 14 + let testParse = ( 15 + t: Zora.t, 16 + input: string, 17 + expect: Term.t, 18 + ~scope=[], 19 + ~msg=?, 20 + ~expectRemaining=?, 21 + ) => { 22 + let res = Term.parse(input, ~scope, ~gen=Term.makeGen()) 23 + switch res { 24 + | Ok((parsed, parsedRemaining)) => { 25 + t->equal( 26 + parsedRemaining, 27 + expectRemaining->Option.getOr(""), 28 + ~msg=input ++ " input consumed", 29 + ) 30 + // NOTE: we're checking for equality here, not equivalency 31 + // error messages are better this way 32 + t->equal(parsed, expect, ~msg?) 33 + } 34 + | Error(msg) => t->fail(~msg="parse failed: " ++ msg) 35 + } 36 + } 37 + let testParseFail = (t: Zora.t, input: string, ~scope=[]) => { 38 + let res = Term.parse(input, ~scope, ~gen=Term.makeGen()) 39 + switch res { 40 + | Ok((p, remaining)) => 41 + t->fail( 42 + ~msg=`parse intended to fail, but succeeded: ${Term.prettyPrint( 43 + p, 44 + ~scope, 45 + )}\nremaining: ${remaining}`, 46 + ) 47 + | Error(_) => t->ok(true) 48 + } 49 + } 50 + let testParsePrettyPrint = (t: Zora.t, input, expected, ~scope=[]) => { 15 51 let res = Term.parse(input, ~scope=[], ~gen=Term.makeGen()) 52 + 16 53 switch res { 17 54 | Ok(res) => { 18 - t->equal(res->snd, "", ~msg=input ++ " input consumed") 19 - // NOTE: we're checking for equality here, not equivalency 20 - // error messages are better this way 21 - t->equal(res->fst, t2, ~msg?) 55 + let result = Term.prettyPrint(res->fst, ~scope) 56 + t->equal(result, expected, ~msg="prettyPrint output matches expected") 22 57 } 23 58 | Error(msg) => t->fail(~msg="parse failed: " ++ msg) 24 59 } ··· 37 72 } 38 73 } 39 74 } 40 - let testUnify = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?) => { 75 + let testUnify1 = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?) => { 41 76 let gen = Term.makeGen() 42 77 let (a, _) = Term.parse(at, ~scope=[], ~gen)->Result.getExn 43 78 let (b, _) = Term.parse(bt, ~scope=[], ~gen)->Result.getExn 44 79 let res = Term.unify(a, b, ~gen) 45 - if res->Array.length == 0 { 80 + if res->Seq.length == 0 { 46 81 t->fail(~msg="unification failed: " ++ stringifyExn(a) ++ " and " ++ stringifyExn(b)) 47 82 } else { 48 83 switch subst { 49 84 | None => t->ok(true, ~msg=msg->Option.getOr("unification succeeded")) 50 85 | Some(subst) => { 51 - t->equal(res->Array.length, 1) 86 + t->equal(res->Seq.length, 1) 52 87 t->equal( 53 - res[0]->Option.getExn, 88 + res->Seq.head->Option.getExn, 54 89 subst, 55 90 ~msg=msg->Option.getOr("unification succeeded with substitution"), 56 91 ) ··· 58 93 } 59 94 } 60 95 } 61 - let testNotUnify = (t: Zora.t, at: string, bt: string, ~msg=?) => { 96 + 97 + let substArrayPrettyPrint = (ss: array<Term.subst>) => { 98 + ss->Array.map(t => Term.prettyPrintSubst(t, ~scope=[]))->Util.showArray 99 + } 100 + 101 + let testUnify = (t: Zora.t, t1: Term.t, t2: Term.t, expect: array<Term.subst>, ~msg=?) => { 102 + let expect = Seq.fromArray(expect) 103 + let res = Term.unify(t1, t2)->Seq.take(10) 104 + // Console.log( 105 + // `t1: ${Term.prettyPrint(t1, ~scope=[])} t2:${Term.prettyPrint(t2, ~scope=[])}\nsubsts: ${res 106 + // ->Seq.map(t => Term.prettyPrintSubst(t, ~scope=[])) 107 + // ->Seq.join(",")}\n`, 108 + // ) 109 + let noMatches = 110 + expect 111 + ->Seq.filter(sub1 => Seq.find(res, sub2 => Term.substEqual(sub1, sub2))->Option.isNone) 112 + ->Seq.map(t => Term.prettyPrintSubst(t, ~scope=[])) 113 + ->Seq.toArray 114 + let msg = msg->Option.getOr("each substitution in `expect` should have a match in solutions") 115 + t->equal(noMatches, [], ~msg) 116 + } 117 + 118 + let testUnifyFail = (t: Zora.t, at: string, bt: string, ~msg=?) => { 62 119 let gen = Term.makeGen() 63 120 let (a, _) = Term.parse(at, ~scope=[], ~gen)->Result.getExn 64 121 let (b, _) = Term.parse(bt, ~scope=[], ~gen)->Result.getExn 65 122 let res = Term.unify(a, b) 66 - if res->Array.length != 0 { 123 + if res->Seq.length != 0 { 67 124 t->fail(~msg="unification succeeded: " ++ stringifyExn(a) ++ " and " ++ stringifyExn(b)) 68 125 } else { 69 126 t->ok(true, ~msg=msg->Option.getOr("unification failed")) 70 - } 71 - } 72 - let testParsePrettyPrint = (t: Zora.t, input, expected, ~scope=[]) => { 73 - let res = Term.parse(input, ~scope=[], ~gen=Term.makeGen()) 74 - 75 - switch res { 76 - | Ok(res) => { 77 - let result = Term.prettyPrint(res->fst, ~scope) 78 - t->equal(result, expected, ~msg="prettyPrint output matches expected") 79 - } 80 - | Error(msg) => t->fail(~msg="parse failed: " ++ msg) 81 127 } 82 128 } 83 129 }

Configure Feed

Configure Feed