Merge pull request #25 from joshcbrown/string-in-sexp

+169 -109

index.html

··· 452 452 <h2>Basic</h2> 453 453 <hol-string id="index.html/mexp" deps="index.html/myconfig"> 454 454 ---- M-Empty 455 - "" M 455 + ("" M) 456 456 457 457 s. 458 - "$s" M 458 + ("$s" M) 459 459 ------- M-Surround 460 - "($s)" M 460 + ("($s)" M) 461 461 462 462 s1. s2. 463 - "$s1" M "$s2" M 463 + ("$s1" M) ("$s2" M) 464 464 ------- M-Juxtapose 465 - "$s1 $s2" M 465 + ("$s1 $s2" M) 466 466 </hol-string> 467 467 <hol-string-proof id="index.html/stringprooftest" deps="index.html/myconfig index.html/mexp"> 468 - -------- paren 469 - "()(())" M 470 - |- by (Concat "()" "(())") { 471 - |- by (Surround "") { 472 - |- by (Empty) {} 473 - } 474 - |- by (Surround "()") { 475 - |- by (Surround "") { 476 - |- by (Empty) {} 477 - } 478 - } 479 - } 480 - </hol-string-proof> 481 - <hol-string id="index.html/bool" deps="index.html/myconfig"> 482 - ------- T-Atom 483 - "T" Atom 484 - ------- F-Atom 485 - "F" Atom 486 - 487 - e. 488 - "$e" Atom 489 - --------- Atom-AE 490 - "$e" AE 491 - 492 - e1.e2. 493 - "$e1" Atom "$e2" AE 494 - -------------------- And 495 - "$e1 /\\ $e2" AE 496 - 497 - e. 498 - "$e" AE 499 - --------- AE-B 500 - "$e" B 468 + ---- paren 469 + ("( ) ( ( ) )" M) 501 470 502 - e1.e2. 503 - "$e1" AE "$e2" B 504 - ----------------- Or 505 - "$e1 \\/ $e2" B 506 - 507 - e. 508 - "$e" B 509 - ----------- Paren 510 - "($e)" Atom 511 - </hol-string> 512 - <hol-string-proof id="index.html/boolprooftest" deps="index.html/myconfig index.html/bool"> 513 - ------------- bool 514 - "T/\\(T\\/F)" AE 515 - |- by (And "T" "(T\\/F)") { 516 - |- by (T-Atom) {} 517 - |- by (Atom-AE "(T\\/F)") { 518 - |- by (Paren "T\\/F") { 519 - |- by (Or "T" "F") { 520 - |- by (Atom-AE "T") { 521 - |- by (T-Atom) {} 522 - } 523 - |- by (AE-B "F") { 524 - |- by (Atom-AE "F") { 525 - |- by (F-Atom) {} 526 - } 527 - } 528 - } 529 - } 530 - } 531 - } 471 + |- by (M-Juxtapose "( )" "( ( ) )") { 472 + |- by (M-Surround "") { 473 + |- by (M-Empty) {}} 474 + |- by (M-Surround "( )") { 475 + |- by (M-Surround "") { 476 + |- by (M-Empty) {}}}} 532 477 </hol-string-proof> 533 - <h2>With first-order term judgments</h2> 534 - <hol-string id="index.html/m-exp-parse" deps="index.html/myconfig"> 535 - ---- MParse-Empty 536 - "" (MP emp) 537 - 538 - s1. p1. 539 - "$s1" (MP p1) 540 - ------------- MParse-Surround 541 - "($s1)" (MP (p1)) 542 - 543 - s1. s2. p1. p2. 544 - "$s1" p1 545 - "$s1" p2 546 - ------------------- MParse-Juxtapose 547 - "$s1 $s2" (MP (p1 p2)) 548 - </hol-string> 549 - <hol-string id="index.html/mexp-induct" deps="index.html/myconfig"> 550 - s. p. 551 - "$s" M "" p [s1. "$s1" p |- "($s1)" p] [s1. s2. "$s1" p "$s2" p |- "$s1 $s2" p] 552 - ---------------------------------- M-Induct 553 - "$s" p 554 - </hol-string> 478 +  479 +  480 +  481 +  482 +  483 +  484 +  485 +  486 +  487 +  488 +  489 +  490 +  491 +  492 +  493 +  494 +  495 +  496 +  497 +  498 +  499 +  500 +  501 +  502 +  503 +  504 +  505 +  506 +  507 +  508 +  509 +  510 +  511 +  512 +  513 +  514 +  515 +  516 +  517 +  518 +  519 +  520 +  521 +  522 +  523 +  524 +  525 +  526 +  527 +  528 +  529 +  530 +  531 +  532 +  533 +  534 +  535 +  536 +  537 +  538 +  539 +  540 +  541 +  542 +  543 +  544 +  545 +  546 +  547 +  548 +  549 +  550 +  551 +  552 +  553 +  554 +  555 555 <hol-string id="index.html/lexp" deps="index.html/myconfig"> 556 - s. "$s" L 556 + s. ("$s" L) 557 557 -----N-Surr 558 - "($s)" N 558 + ("($s)" N) 559 559 560 560 -----L-Empty 561 - "" L 561 + ("" L) 562 562 563 563 s1. s2. 564 - "$s1" N "$s2" L 564 + ("$s1" N) ("$s2" L) 565 565 -----L-Juxtapose 566 - "$s1 $s2" L 566 + ("$s1 $s2" L) 567 567 </hol-string> 568 - 569 - <hol-string-proof id="index.html/lexp-n" deps="index.html/myconfig index.html/mexp index.html/mexp-induct index.html/lexp"> 570 - s. "$s" N 568 + <hol-string-proof id="index.html/lexp-n" deps="index.html/lexp index.html/myconfig"> 569 + s. ("$s" N) 571 570 --------N-L 572 - "$s" L 571 + ("$s" L) 573 572 s. sn |- by (L-Juxtapose s "") { 574 573 |- by (sn) {} 575 574 |- by (L-Empty) {} 576 575 } 577 576 </hol-string-proof> 578 - <hol-string-proof id="index.html/lexp-juxt" deps="index.html/myconfig index.html/mexp index.html/mexp-induct index.html/lexp"> 579 - s1.s2. "$s1" L "$s2" L 577 + <hol-string-proof id="index.html/lexp-juxt" deps="index.html/myconfig index.html/mexp index.html/lexp"> 578 + s1.s2. ("$s1" L) ("$s2" L) 580 579 --------------------- lexp-juxt 581 - "$s1 $s2" L 580 + ("$s1 $s2" L) 582 581 s1. s2. s1L s2L |- ? 583 582 </hol-string-proof> 584 - <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"> 585 - s. "$s" M 583 + <hol-string-proof id="index.html/mexp-lexp" deps="index.html/myconfig index.html/mexp index.html/lexp index.html/lexp-juxt index.html/lexp-n"> 584 + s. ("$s" M) 586 585 ----------- mexp-lexp 587 - "$s" L 586 + ("$s" L) 588 587 s. sM |- ? 589 588 </hol-string-proof> 590 - <hol-string-proof id="index.html/lexp-mexp" deps="index.html/myconfig index.html/mexp index.html/mexp-induct index.html/lexp index.html/lexp-n"> 591 - s. "$s" L 589 + <hol-string-proof id="index.html/lexp-mexp" deps="index.html/myconfig index.html/mexp index.html/lexp index.html/lexp-n"> 590 + s. ("$s" L) 592 591 ----------- mexp-lexp 593 - "$s" M 594 - s. sL |- elim (L_mutualInduct sL "" "$s" "" "M" "M") { 592 + ("$s" M) 593 + s. sL |- elim (L_mutualInduct sL "" "$s" "" M M) { 595 594 |- by (M-Empty) {} 596 595 s1.s2. 0 1 2 3 |- elim (M-Juxtapose 2 "$s1" "$s2") { 597 596 |- by (3) {}} 598 597 s. 0 1 |- elim (M-Surround 1 "$s") {}} 598 + </hol-string-proof> 599 + <hol-string id="index.html/string-arithmetic" deps="index.html/myconfig"> 600 + -------- nat-z 601 + (Nat Z) 602 + 603 + n. (Nat n) 604 + -------- nat-s 605 + (Nat (S n)) 606 + 607 + n1. 608 + -------- nat-plus-z 609 + (Eval (Plus n1 Z) n1) 610 + 611 + n1. n2. res. 612 + (Eval (Plus n1 n2) res) 613 + --------- nat-plus-s 614 + (Eval (Plus n1 (S n2)) (S res)) 615 + 616 + ------- string-zero 617 + (Parse "0" Z) 618 + 619 + ------- string-one 620 + (Parse "1" (S Z)) 621 + 622 + -------- string-two 623 + (Parse "2" (S (S Z))) 624 + 625 + -------- string-three 626 + (Parse "3" (S (S (S Z)))) 627 + 628 + s1. s2. n2. 629 + (Parse s2 n2) 630 + --------- string-prod 631 + (Parse "$s1 * $s2" (Prod s1 n2)) 632 + 633 + s1. 634 + ---------- eval-prod-Z 635 + (Eval (Prod s1 Z) "") 636 + 637 + s1. s1n. n. 638 + (Eval (Prod s1 n) s1n) 639 + ----------- eval-prod-S 640 + (Eval (Prod s1 (S n)) "$s1$s1n") 641 + 642 + s. ast. res. 643 + (Parse s ast) 644 + (Eval ast res) 645 + --------------- program-eval 646 + (PEval s res) 647 + 648 + </hol-string> 649 + <hol-string-proof id="index.html/sexp-nat-toy" deps="index.html/myconfig index.html/string-arithmetic"> 650 + ----------- mexp-lexp 651 + (Eval (Plus (S Z) (S (S Z))) (S (S (S Z)))) 652 + |- ? 653 + </hol-string-proof> 654 + <hol-string-proof id="index.html/string-prod-toy" deps="index.html/myconfig index.html/string-arithmetic"> 655 + ------------- foo-3 656 + (PEval "foo * 3" "foo foo foo") 657 + |- ? 658 + 599 659 </hol-string-proof> 600 660 <script type="module" src="./src/testcomponent.tsx"></script> 601 661 </body>

+6 -1

src/HOTerm.res

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

+1

src/HOTerm.resi

··· 17 17 let strip: t => (t, array<t>) 18 18 let app: (t, array<t>) => t 19 19 let mkvars: int => array<t> 20 + let mapTerms: (t, t => t) => t 20 21 // exposed for testing purposes 21 22 exception UnifyFail(string) 22 23 let substAdd: (subst, schematic, t) => subst

+1 -3

src/HOTermJView.resi

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

+13 -17

src/HOTermMethod.res

··· 2 2 open Method 3 3 4 4 module MakeRewriteHOTerm = ( 5 - Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 5 + Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 6 6 Config: { 7 7 let keyword: string 8 8 let reversed: bool ··· 43 43 44 44 type t<'a> = { 45 45 equalityName: string, 46 - instantiation: array<Judgment.substCodom>, 46 + instantiation: array<Term.t>, 47 47 subgoal: 'a, 48 48 } 49 49 ··· 57 57 } 58 58 } 59 59 60 - let substitute = (it: t<'a>, subst: Judgment.subst) => { 60 + let substitute = (it: t<'a>, subst: Term.subst) => { 61 61 { 62 62 equalityName: it.equalityName, 63 - instantiation: it.instantiation->Array.map(t => t->Judgment.substituteSubstCodom(subst)), 63 + instantiation: it.instantiation->Array.map(t => t->Judgment.substitute(subst)), 64 64 subgoal: it.subgoal, 65 65 } 66 66 } ··· 72 72 ~subprinter: ('a, ~scope: array<HOTerm.meta>, ~indentation: int=?) => string, 73 73 ) => { 74 74 let ind = String.repeat(" ", indentation) 75 - let args = it.instantiation->Array.map(t => Judgment.prettyPrintSubstCodom(t, ~scope)) 75 + let args = it.instantiation->Array.map(t => Term.prettyPrint(t, ~scope)) 76 76 let argsStr = if Array.length(args) > 0 { 77 77 " " ++ Array.join(args, " ") 78 78 } else { ··· 98 98 let instantiation = [] 99 99 let it = ref(Error("")) 100 100 while { 101 - it := Judgment.parseSubstCodom(cur.contents, ~scope, ~gen) 101 + it := Term.parse(cur.contents, ~scope, ~gen) 102 102 it.contents->Result.isOk 103 103 } { 104 104 let (val, rest) = it.contents->Result.getExn ··· 157 157 } 158 158 159 159 let apply = (ctx: Context.t, j: Judgment.t, gen: HOTerm.gen, f: Rule.t => 'a) => { 160 - let ret: Dict.t<(t<'a>, Judgment.subst)> = Dict.make() 160 + let ret: Dict.t<(t<'a>, Term.subst)> = Dict.make() 161 161 162 162 ctx 163 163 ->Context.facts ··· 246 246 } 247 247 248 248 module Rewrite = ( 249 - Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 249 + Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 250 250 ) => MakeRewriteHOTerm( 251 251 Judgment, 252 252 { ··· 256 256 ) 257 257 258 258 module RewriteReverse = ( 259 - Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 259 + Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 260 260 ) => MakeRewriteHOTerm( 261 261 Judgment, 262 262 { ··· 265 265 }, 266 266 ) 267 267 268 - module ConstructorNeq = ( 269 - Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 270 - ) => { 268 + module ConstructorNeq = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => { 271 269 module Term = HOTerm 272 270 module Rule = Rule.Make(HOTerm, Judgment) 273 271 module Context = Context(HOTerm, Judgment) ··· 321 319 322 320 let map = (it: t<'a>, _f: 'a => 'b): t<'b> => it 323 321 324 - let substitute = (it: t<'a>, _subst: Judgment.subst) => it 322 + let substitute = (it: t<'a>, _subst: Term.subst) => it 325 323 326 324 let prettyPrint = (_it: t<'a>, ~scope as _, ~indentation=0, ~subprinter as _) => 327 325 String.repeat(" ", indentation)->String.concat("constructor_neq") ··· 353 351 } 354 352 } 355 353 356 - module ConstructorInj = ( 357 - Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 358 - ) => { 354 + module ConstructorInj = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => { 359 355 module Rule = Rule.Make(HOTerm, Judgment) 360 356 module Context = Context(HOTerm, Judgment) 361 357 ··· 370 366 371 367 let map = (it: t<'a>, _f: 'a => 'b): t<'b> => it 372 368 373 - let substitute = (it: t<'a>, _subst: Judgment.subst) => it 369 + let substitute = (it: t<'a>, _subst: HOTerm.subst) => it 374 370 375 371 let prettyPrint = (it: t<'a>, ~scope as _, ~indentation=0, ~subprinter as _) => 376 372 String.repeat(" ", indentation)->String.concat(

+3 -4

src/InductiveSet.res

··· 1 1 open Signatures 2 2 open Component 3 - open Util 4 3 5 4 // InductiveSet is specific to HOTerm to allow pattern matching on term structure 6 5 module Make = ( ··· 57 56 let generateInductionRule = (group: predicateGroup, allGroups: array<predicateGroup>): Rule.t => { 58 57 let {name: str, arity: i} = group 59 58 let numFormers = Array.length(allGroups) 60 - let groupIndex = mustFindIndex(allGroups, g => g.name == str && g.arity == i) 59 + let groupIndex = Util.mustFindIndex(allGroups, g => g.name == str && g.arity == i) 61 60 62 61 let findFormerIndex = (name, arity) => 63 - mustFindIndex(allGroups, g => g.name == name && g.arity == arity) 62 + Util.mustFindIndex(allGroups, g => g.name == name && g.arity == arity) 64 63 65 64 let generateInductiveHypothesis = (premise: Rule.t, offset: int): option<Rule.t> => { 66 65 let (head, args) = HOTerm.strip(premise.conclusion) ··· 89 88 let (conclusionHead, conclusionArgs) = HOTerm.strip(constructorRule.conclusion) 90 89 let typeIndex = switch conclusionHead { 91 90 | Symbol({name}) => findFormerIndex(name, Array.length(conclusionArgs)) 92 - | _ => throw(Unreachable("Constructor conclusion must have a Symbol head")) 91 + | _ => throw(Util.Unreachable("Constructor conclusion must have a Symbol head")) 93 92 } 94 93 95 94 {

+16 -17

src/Method.res

··· 1 1 open Signatures 2 - open Util 3 2 module Context = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 4 3 module Rule = Rule.Make(Term, Judgment) 5 4 type t = { ··· 17 16 module Context: module type of Context(Term, Judgment) 18 17 type t<'a> 19 18 let keywords: array<string> 20 - let substitute: (t<'a>, Judgment.subst) => t<'a> 19 + let substitute: (t<'a>, Term.subst) => t<'a> 21 20 let check: (t<'a>, Context.t, Judgment.t, ('a, Rule.t) => 'b) => result<t<'b>, string> 22 - let apply: (Context.t, Judgment.t, Term.gen, Rule.t => 'a) => Dict.t<(t<'a>, Judgment.subst)> 21 + let apply: (Context.t, Judgment.t, Term.gen, Rule.t => 'a) => Dict.t<(t<'a>, Term.subst)> 23 22 let map: (t<'a>, 'a => 'b) => t<'b> 24 23 let parse: ( 25 24 string, ··· 37 36 } 38 37 39 38 let seqSizeLimit = 100 39 + let newline = Util.newline 40 40 41 41 module Derivation = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 42 42 module Rule = Rule.Make(Term, Judgment) 43 43 module Context = Context(Term, Judgment) 44 44 type t<'a> = { 45 45 ruleName: string, 46 - instantiation: array<Judgment.substCodom>, 46 + instantiation: array<Term.t>, 47 47 subgoals: array<'a>, 48 48 } 49 49 let map = (it: t<'a>, f) => { ··· 53 53 subgoals: it.subgoals->Array.map(f), 54 54 } 55 55 } 56 - let substitute = (it: t<'a>, subst: Judgment.subst) => { 56 + let substitute = (it: t<'a>, subst: Term.subst) => { 57 57 { 58 58 ruleName: it.ruleName, 59 - instantiation: it.instantiation->Array.map(t => t->Judgment.substituteSubstCodom(subst)), 59 + instantiation: it.instantiation->Array.map(t => t->Term.substitute(subst)), 60 60 subgoals: it.subgoals, 61 61 } 62 62 } ··· 68 68 ~indentation=0, 69 69 ~subprinter: ('a, ~scope: array<Term.meta>, ~indentation: int=?) => string, 70 70 ) => { 71 - let args = it.instantiation->Array.map(t => Judgment.prettyPrintSubstCodom(t, ~scope)) 71 + let args = it.instantiation->Array.map(t => Term.prettyPrint(t, ~scope)) 72 72 "by (" 73 73 ->String.concat(Array.join([it.ruleName]->Array.concat(args), " ")) 74 74 ->String.concat(") {") ··· 95 95 let instantiation = [] 96 96 let it = ref(Error("")) 97 97 while { 98 - it := Judgment.parseSubstCodom(cur.contents, ~scope, ~gen) 98 + it := Term.parse(cur.contents, ~scope, ~gen) 99 99 it.contents->Result.isOk 100 100 } { 101 101 let (val, rest) = it.contents->Result.getExn ··· 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 - let ghostSubs = Judgment.unify(Judgment.ghostJudgment, res.conclusion) 151 - if ghostSubs->Seq.head->Option.isNone { 150 + if !Judgment.concrete(res.conclusion) { 152 151 Some((key, res, insts)) 153 152 } else { 154 153 None ··· 212 211 type t<'a> = { 213 212 ruleName: string, 214 213 elimName: string, 215 - instantiation: array<Judgment.substCodom>, 214 + instantiation: array<Term.t>, 216 215 subgoals: array<'a>, 217 216 } 218 217 exception InternalParseError(string) ··· 229 228 "" 230 229 } 231 230 let instantiation = Array.join( 232 - it.instantiation->Array.map(t => Judgment.prettyPrintSubstCodom(t, ~scope)), 231 + it.instantiation->Array.map(t => Term.prettyPrint(t, ~scope)), 233 232 " ", 234 233 ) 235 234 let subgoalsStr = ··· 248 247 } 249 248 } 250 249 251 - let substitute = (it: t<'a>, subst: Judgment.subst) => { 250 + let substitute = (it: t<'a>, subst: Term.subst) => { 252 251 { 253 252 ruleName: it.ruleName, 254 253 elimName: it.elimName, 255 - instantiation: it.instantiation->Array.map(t => t->Judgment.substituteSubstCodom(subst)), 254 + instantiation: it.instantiation->Array.map(t => t->Term.substitute(subst)), 256 255 subgoals: it.subgoals, 257 256 } 258 257 } ··· 270 269 let instantiation = [] 271 270 let it = ref(Error("")) 272 271 while { 273 - it := Judgment.parseSubstCodom(cur.contents, ~scope, ~gen) 272 + it := Term.parse(cur.contents, ~scope, ~gen) 274 273 it.contents->Result.isOk 275 274 } { 276 275 let (val, rest) = it.contents->Result.getExn ··· 394 393 instantiation: ruleInsts, 395 394 subgoals: rule.premises->Array.sliceToEnd(~start=1)->Array.map(f), 396 395 } 397 - let subst = Judgment.mergeSubsts(elimSub, ruleSub) 396 + let subst = Term.mergeSubsts(elimSub, ruleSub) 398 397 ret->Dict.set(`elim ${ruleName} with ${elimName}`, (new, subst)) 399 398 }, 400 399 ) ··· 421 420 show: f(it.show), 422 421 } 423 422 } 424 - let substitute = (it: t<'a>, subst: Judgment.subst) => { 423 + let substitute = (it: t<'a>, subst: Term.subst) => { 425 424 { 426 425 rule: it.rule->Rule.substitute(subst), 427 426 proof: it.proof,

+25 -27

src/MethodView.res

··· 10 10 scope: array<Term.meta>, 11 11 ruleStyle: RuleView.style, 12 12 gen: Term.gen, 13 - onChange: (Method.t<'a>, Judgment.subst) => unit, 13 + onChange: (Method.t<'a>, Term.subst) => unit, 14 14 } 15 15 type srProps<'a> = { 16 16 "proof": 'a, 17 17 "scope": array<Term.meta>, 18 18 "ruleStyle": RuleView.style, 19 19 "gen": Term.gen, 20 - "onChange": ('a, Judgment.subst) => unit, 20 + "onChange": ('a, Term.subst) => unit, 21 21 } 22 22 let make: (srProps<'a> => React.element) => props<'a> => React.element 23 23 } ··· 29 29 scope: array<Term.meta>, 30 30 ruleStyle: RuleView.style, 31 31 gen: Term.gen, 32 - onChange: (Method.t<'a>, Judgment.subst) => unit, 32 + onChange: (Method.t<'a>, Term.subst) => unit, 33 33 } 34 34 type srProps<'a> = { 35 35 "proof": 'a, 36 36 "scope": array<Term.meta>, 37 37 "ruleStyle": RuleView.style, 38 38 "gen": Term.gen, 39 - "onChange": ('a, Judgment.subst) => unit, 39 + "onChange": ('a, Term.subst) => unit, 40 40 } 41 41 let make = (subRender: srProps<'a> => React.element) => 42 42 props => { ··· 54 54 "scope": props.scope, 55 55 "ruleStyle": props.ruleStyle, 56 56 "gen": props.gen, 57 - "onChange": (newa, subst: Judgment.subst) => 57 + "onChange": (newa, subst: Term.subst) => 58 58 props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst), 59 59 }, 60 60 )} ··· 73 73 scope: array<Term.meta>, 74 74 ruleStyle: RuleView.style, 75 75 gen: Term.gen, 76 - onChange: (Method.t<'a>, Judgment.subst) => unit, 76 + onChange: (Method.t<'a>, Term.subst) => unit, 77 77 } 78 78 type srProps<'a> = { 79 79 "proof": 'a, 80 80 "scope": array<Term.meta>, 81 81 "ruleStyle": RuleView.style, 82 82 "gen": Term.gen, 83 - "onChange": ('a, Judgment.subst) => unit, 83 + "onChange": ('a, Term.subst) => unit, 84 84 } 85 85 let make = (subRender: srProps<'a> => React.element) => 86 86 props => { ··· 98 98 "scope": props.scope, 99 99 "ruleStyle": props.ruleStyle, 100 100 "gen": props.gen, 101 - "onChange": (newa, subst: Judgment.subst) => 101 + "onChange": (newa, subst: Term.subst) => 102 102 props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst), 103 103 }, 104 104 )} ··· 121 121 scope: array<Term.meta>, 122 122 ruleStyle: RuleView.style, 123 123 gen: Term.gen, 124 - onChange: (Method.t<'a>, Judgment.subst) => unit, 124 + onChange: (Method.t<'a>, Term.subst) => unit, 125 125 } 126 126 type srProps<'a> = { 127 127 "proof": 'a, 128 128 "scope": array<Term.meta>, 129 129 "ruleStyle": RuleView.style, 130 130 "gen": Term.gen, 131 - "onChange": ('a, Judgment.subst) => unit, 131 + "onChange": ('a, Term.subst) => unit, 132 132 } 133 133 module RuleView = RuleView.Make(Term, Judgment, JudgmentView) 134 134 let make = (subRender: srProps<'a> => React.element) => ··· 162 162 } 163 163 } 164 164 165 - module RewriteView = ( 166 - Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 167 - ) => { 165 + module RewriteView = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => { 168 166 module Method = Rewrite(Judgment) 169 167 type props<'a> = { 170 168 method: Method.t<'a>, 171 169 scope: array<HOTerm.meta>, 172 170 ruleStyle: RuleView.style, 173 171 gen: HOTerm.gen, 174 - onChange: (Method.t<'a>, Judgment.subst) => unit, 172 + onChange: (Method.t<'a>, HOTerm.subst) => unit, 175 173 } 176 174 type srProps<'a> = { 177 175 "proof": 'a, 178 176 "scope": array<HOTerm.meta>, 179 177 "ruleStyle": RuleView.style, 180 178 "gen": HOTerm.gen, 181 - "onChange": ('a, Judgment.subst) => unit, 179 + "onChange": ('a, HOTerm.subst) => unit, 182 180 } 183 181 let make = (subRender: srProps<'a> => React.element) => 184 182 props => { ··· 194 192 "scope": props.scope, 195 193 "ruleStyle": props.ruleStyle, 196 194 "gen": props.gen, 197 - "onChange": (subgoal, subst: Judgment.subst) => 195 + "onChange": (subgoal, subst: HOTerm.subst) => 198 196 props.onChange({...props.method, subgoal}, subst), 199 197 }, 200 198 )} ··· 205 203 } 206 204 207 205 module RewriteReverseView = ( 208 - Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 206 + Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 209 207 ) => { 210 208 module Method = RewriteReverse(Judgment) 211 209 type props<'a> = { ··· 213 211 scope: array<HOTerm.meta>, 214 212 ruleStyle: RuleView.style, 215 213 gen: HOTerm.gen, 216 - onChange: (Method.t<'a>, Judgment.subst) => unit, 214 + onChange: (Method.t<'a>, HOTerm.subst) => unit, 217 215 } 218 216 type srProps<'a> = { 219 217 "proof": 'a, 220 218 "scope": array<HOTerm.meta>, 221 219 "ruleStyle": RuleView.style, 222 220 "gen": HOTerm.gen, 223 - "onChange": ('a, Judgment.subst) => unit, 221 + "onChange": ('a, HOTerm.subst) => unit, 224 222 } 225 223 let make = (subRender: srProps<'a> => React.element) => 226 224 props => { ··· 236 234 "scope": props.scope, 237 235 "ruleStyle": props.ruleStyle, 238 236 "gen": props.gen, 239 - "onChange": (subgoal, subst: Judgment.subst) => 237 + "onChange": (subgoal, subst: HOTerm.subst) => 240 238 props.onChange({...props.method, subgoal}, subst), 241 239 }, 242 240 )} ··· 247 245 } 248 246 249 247 module ConstructorNeqView = ( 250 - Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 248 + Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 251 249 ) => { 252 250 module Method = ConstructorNeq(Judgment) 253 251 type props<'a> = { ··· 255 253 scope: array<HOTerm.meta>, 256 254 ruleStyle: RuleView.style, 257 255 gen: HOTerm.gen, 258 - onChange: (Method.t<'a>, Judgment.subst) => unit, 256 + onChange: (Method.t<'a>, HOTerm.subst) => unit, 259 257 } 260 258 type srProps<'a> = { 261 259 "proof": 'a, 262 260 "scope": array<HOTerm.meta>, 263 261 "ruleStyle": RuleView.style, 264 262 "gen": HOTerm.gen, 265 - "onChange": ('a, Judgment.subst) => unit, 263 + "onChange": ('a, HOTerm.subst) => unit, 266 264 } 267 265 let make = (_subRender: srProps<'a> => React.element) => 268 266 _props => { ··· 273 271 } 274 272 275 273 module ConstructorInjView = ( 276 - Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 274 + Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 277 275 ) => { 278 276 module Method = ConstructorInj(Judgment) 279 277 type props<'a> = { ··· 281 279 scope: array<HOTerm.meta>, 282 280 ruleStyle: RuleView.style, 283 281 gen: HOTerm.gen, 284 - onChange: (Method.t<'a>, Judgment.subst) => unit, 282 + onChange: (Method.t<'a>, HOTerm.subst) => unit, 285 283 } 286 284 type srProps<'a> = { 287 285 "proof": 'a, 288 286 "scope": array<HOTerm.meta>, 289 287 "ruleStyle": RuleView.style, 290 288 "gen": HOTerm.gen, 291 - "onChange": ('a, Judgment.subst) => unit, 289 + "onChange": ('a, HOTerm.subst) => unit, 292 290 } 293 291 let make = (_subRender: srProps<'a> => React.element) => 294 292 props => { ··· 317 315 scope: array<Term.meta>, 318 316 ruleStyle: RuleView.style, 319 317 gen: Term.gen, 320 - onChange: (Method.t<'a>, Judgment.subst) => unit, 318 + onChange: (Method.t<'a>, Term.subst) => unit, 321 319 } 322 320 type srProps<'a> = Method1View.srProps<'a> 323 321 let make = (subrender: srProps<'a> => React.element) =>

+3 -3

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>, Judgment.subst)>) 27 + | Goal(Term.gen => Dict.t<(Method.t<checked>, Term.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: Judgment.subst) => { 33 + let rec substitute = (prf: t, subst: Term.subst) => { 34 34 fixes: prf.fixes, 35 35 assumptions: prf.assumptions, 36 36 method: prf.method->Option.map(m => ··· 191 191 } 192 192 } // result<checked,string> 193 193 194 - let substituteChecked = (prf: checked, ctx: Context.t, subst: Judgment.subst) => { 194 + let substituteChecked = (prf: checked, ctx: Context.t, subst: Term.subst) => { 195 195 switch prf { 196 196 | Checked(prf) => 197 197 check(ctx, Checked(prf)->uncheck->substitute(subst), prf.rule->Rule.substitute(subst))

+27 -17

src/ProofView.res

··· 19 19 scope: array<Term.meta>, 20 20 ruleStyle: RuleView.style, 21 21 gen: Term.gen, 22 - onChange: (Proof.checked, Judgment.subst) => unit, 22 + onChange: (Proof.checked, Term.subst) => unit, 23 23 } 24 24 module RuleView = RuleView.Make(Term, Judgment, JudgmentView) 25 25 @react.componentWithProps 26 26 let rec make = (props: props) => { 27 27 let {sidebarRef} = React.useContext(SidebarContext.context) 28 28 let (isFocused, setFocused) = React.useState(() => false) 29 - 29 + 30 30 let onBlur = e => { 31 - let leavingProof = ReactEvent.Focus.relatedTarget(e) 31 + let leavingProof = 32 + ReactEvent.Focus.relatedTarget(e) 32 33 ->Option.flatMap(el => el->closest(".sidebar")->Nullable.toOption) 33 34 ->Option.isNone 34 35 if leavingProof { ··· 53 54 | Goal(options) => 54 55 let portal = switch sidebarRef.current->Nullable.toOption { 55 56 | None => React.null 56 - | Some(node) => Portal.createPortal(<> { 57 - options(props.gen) 57 + | Some(node) => 58 + Portal.createPortal( 59 + <> 60 + {options(props.gen) 58 61 ->Dict.toArray 59 62 ->Array.map(((str, (opt, subst))) => { 60 - <button tabIndex=0 onBlur 63 + <button 64 + tabIndex=0 65 + onBlur 61 66 key=str 62 67 onClick={_ => 63 68 props.onChange( ··· 68 73 {React.string(str)} 69 74 </button> 70 75 }) 71 - ->React.array } 72 - </>, node) 76 + ->React.array} 77 + </>, 78 + node, 79 + ) 73 80 } 74 - <div className="proof-goal" tabIndex=0 81 + <div 82 + className="proof-goal" 83 + tabIndex=0 75 84 onBlur 76 85 onFocus={e => { 77 86 setFocused(_ => true) 78 87 ReactEvent.Focus.stopPropagation(e) 79 - }}> 80 - {if (isFocused) { 81 - <> 82 - 83 - {portal} 84 - </> 85 - } else { 86 - 88 + }} 89 + > 90 + {if isFocused { 91 + <> 92 + 93 + {portal} 94 + </> 95 + } else { 96 + 87 97 }} 88 98 </div> 89 99 | Do(method) =>

+8 -9

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

-364

src/SExp.res

··· 1 - module IntCmp = Belt.Id.MakeComparable({ 2 - type t = int 3 - let cmp = Pervasives.compare 4 - }) 5 - 6 - type rec t = 7 - | Symbol({name: string}) 8 - | Compound({subexps: array<t>}) 9 - | Var({idx: int}) 10 - | Schematic({schematic: int, allowed: array<int>}) 11 - | Ghost 12 - type meta = string 13 - type schematic = int 14 - type subst = Map.t<schematic, t> 15 - let substEqual = Util.mapEqual 16 - let mapSubst = Util.mapMapValues 17 - let makeSubst = () => { 18 - Map.make() 19 - } 20 - let equivalent = (a: t, b: t) => { 21 - a == b 22 - } 23 - let reduce = (term: t) => term 24 - let rec schematicsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) => 25 - switch it { 26 - | Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic) 27 - | Compound({subexps}) => 28 - subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) => 29 - Belt.Set.union(s, schematicsIn(x)) 30 - ) 31 - | _ => Belt.Set.make(~id=module(IntCmp)) 32 - } 33 - let rec freeVarsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) => 34 - switch it { 35 - | Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx) 36 - | Compound({subexps}) => 37 - subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) => 38 - Belt.Set.union(s, freeVarsIn(x)) 39 - ) 40 - | _ => Belt.Set.make(~id=module(IntCmp)) 41 - } 42 - let rec substitute = (term: t, subst: subst) => 43 - switch term { 44 - | Compound({subexps}) => Compound({subexps: Array.map(subexps, x => substitute(x, subst))}) 45 - | Schematic({schematic, _}) => 46 - switch Map.get(subst, schematic) { 47 - | None => term 48 - | Some(found) => found 49 - } 50 - | _ => term 51 - } 52 - 53 - let combineSubst = (s: subst, t: subst) => { 54 - let nu = Map.make() 55 - Map.entries(s)->Iterator.forEach(opt => 56 - switch opt { 57 - | None => () 58 - | Some((key, term)) => nu->Map.set(key, term->substitute(t)) 59 - } 60 - ) 61 - Map.entries(t)->Iterator.forEach(opt => 62 - switch opt { 63 - | None => () 64 - | Some((key, term)) => nu->Map.set(key, term->substitute(s)) 65 - } 66 - ) 67 - nu 68 - } 69 - let emptySubst: subst = Map.make() 70 - let singletonSubst: (int, t) => subst = (schematic, term) => { 71 - let s = Map.make() 72 - s->Map.set(schematic, term) 73 - s 74 - } 75 - let rec unifyTerm = (a: t, b: t) => 76 - switch (a, b) { 77 - | (Symbol({name: na}), Symbol({name: nb})) if na == nb => Some(emptySubst) 78 - | (Var({idx: ia}), Var({idx: ib})) if ia == ib => Some(emptySubst) 79 - | (Schematic({schematic: sa, _}), Schematic({schematic: sb, _})) if sa == sb => Some(emptySubst) 80 - | (Compound({subexps: xa}), Compound({subexps: xb})) if Array.length(xa) == Array.length(xb) => 81 - unifyArray(Belt.Array.zip(xa, xb)) 82 - | (Schematic({schematic, allowed}), t) 83 - if !Belt.Set.has(schematicsIn(t), schematic) && 84 - Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) => 85 - Some(singletonSubst(schematic, t)) 86 - | (t, Schematic({schematic, allowed})) 87 - if !Belt.Set.has(schematicsIn(t), schematic) && 88 - Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) => 89 - Some(singletonSubst(schematic, t)) 90 - | (_, _) => None 91 - } 92 - and unifyArray = (a: array<(t, t)>) => { 93 - if Array.length(a) == 0 { 94 - Some(emptySubst) 95 - } else { 96 - let (x, y) = a[0]->Option.getUnsafe 97 - switch unifyTerm(x, y) { 98 - | None => None 99 - | Some(s1) => 100 - switch a 101 - ->Array.sliceToEnd(~start=1) 102 - ->Array.map(((t1, t2)) => (substitute(t1, s1), substitute(t2, s1))) 103 - ->unifyArray { 104 - | None => None 105 - | Some(s2) => Some(combineSubst(s1, s2)) 106 - } 107 - } 108 - } 109 - } 110 - let unify = (a: t, b: t, ~gen as _=?) => { 111 - Seq.fromArray( 112 - switch unifyTerm(a, b) { 113 - | None => [] 114 - | Some(s) => [s] 115 - }, 116 - ) 117 - } 118 - let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) => 119 - switch term { 120 - | Symbol(_) => term 121 - | Compound({subexps}) => 122 - Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))}) 123 - | Var({idx: var}) => 124 - if var < from { 125 - term 126 - } else if var - from < Array.length(substs) && var - from >= 0 { 127 - Option.getUnsafe(substs[var - from]) 128 - } else { 129 - Var({idx: var - Array.length(substs)}) 130 - } 131 - | Schematic({schematic, allowed}) => 132 - Schematic({ 133 - schematic, 134 - allowed: Array.filterMap(allowed, i => 135 - if i < from + Array.length(substs) { 136 - None 137 - } else { 138 - Some(i - (from + Array.length(substs))) 139 - } 140 - ), 141 - }) 142 - | Ghost => Ghost 143 - } 144 - let rec upshift = (term: t, amount: int, ~from: int=0) => 145 - switch term { 146 - | Symbol(_) => term 147 - | Compound({subexps}) => Compound({subexps: Array.map(subexps, x => upshift(x, amount, ~from))}) 148 - | Var({idx}) => 149 - Var({ 150 - idx: if idx >= from { 151 - idx + amount 152 - } else { 153 - idx 154 - }, 155 - }) 156 - | Schematic({schematic, allowed}) => 157 - Schematic({ 158 - schematic, 159 - allowed: Array.map(allowed, i => 160 - if i >= from { 161 - i + amount 162 - } else { 163 - i 164 - } 165 - ), 166 - }) 167 - | Ghost => Ghost 168 - } 169 - let place = (x: int, ~scope: array<string>) => Schematic({ 170 - schematic: x, 171 - allowed: Array.fromInitializer(~length=Array.length(scope), i => i), 172 - }) 173 - let mergeSubsts = Util.mapUnion 174 - 175 - type gen = ref<int> 176 - let seen = (g: gen, s: int) => { 177 - if s >= g.contents { 178 - g := s + 1 179 - } 180 - } 181 - let fresh = (g: gen, ~replacing as _=?) => { 182 - let v = g.contents 183 - g := g.contents + 1 184 - v 185 - } 186 - let prettyPrintVar = (idx: int, scope: array<string>) => { 187 - Console.log(("ppVar", "idx", idx, "scope[idx]", scope[idx], "scope", scope)) 188 - switch scope[idx] { 189 - | Some(n) if Array.indexOf(scope, n) == idx => n 190 - | _ => "\\"->String.concat(String.make(idx)) 191 - } 192 - } 193 - let makeGen = () => { 194 - ref(0) 195 - } 196 - let rec prettyPrint = (it: t, ~scope: array<string>) => 197 - switch it { 198 - | Symbol({name}) => name 199 - | Var({idx}) => prettyPrintVar(idx, scope) 200 - | Schematic({schematic, allowed}) => 201 - "?" 202 - ->String.concat(String.make(schematic)) 203 - ->String.concat("(") 204 - ->String.concat(Array.join(allowed->Array.map(idx => prettyPrintVar(idx, scope)), " ")) 205 - ->String.concat(")") 206 - | Compound({subexps}) => 207 - "(" 208 - ->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e, ~scope)), " ")) 209 - ->String.concat(")") 210 - | Ghost => "§SExp.Ghost" 211 - } 212 - 213 - let prettyPrintSubst = (sub, ~scope) => Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope)) 214 - let symbolRegexpString = `^([^\\s()\\[\\]]+)` 215 - let varRegexpString = "^\\\\([0-9]+)$" 216 - let schematicRegexpString = "^\\?([0-9]+)$" 217 - type lexeme = LParen | RParen | VarT(int) | SymbolT(string) | SchematicT(int) 218 - let nameRES = "^([^\\s.\\[\\]()]+)\\." 219 - let prettyPrintMeta = (str: string) => { 220 - String.concat(str, ".") 221 - } 222 - let parseMeta = (str: string) => { 223 - let re = RegExp.fromStringWithFlags(nameRES, ~flags="y") 224 - switch re->RegExp.exec(str->String.trim) { 225 - | None => Error("not a meta name") 226 - | Some(res) => 227 - switch RegExp.Result.matches(res) { 228 - | [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re))) 229 - | _ => Error("impossible happened") 230 - } 231 - } 232 - } 233 - let parse = (str: string, ~scope: array<string>, ~gen=?) => { 234 - let cur = ref(String.make(str)) 235 - let lex: unit => option<lexeme> = () => { 236 - let str = String.trim(cur.contents) 237 - cur := str 238 - let checkVariable = (candidate: string) => { 239 - let varRegexp = RegExp.fromString(varRegexpString) 240 - switch Array.indexOf(scope, candidate) { 241 - | -1 => 242 - switch varRegexp->RegExp.exec(candidate) { 243 - | Some(res') => 244 - switch RegExp.Result.matches(res') { 245 - | [idx] => Some(idx->Int.fromString->Option.getUnsafe) 246 - | _ => None 247 - } 248 - | None => None 249 - } 250 - | idx => Some(idx) 251 - } 252 - } 253 - if String.get(str, 0) == Some("(") { 254 - cur := String.sliceToEnd(str, ~start=1) 255 - Some(LParen) 256 - } else if String.get(str, 0) == Some(")") { 257 - cur := String.sliceToEnd(str, ~start=1) 258 - Some(RParen) 259 - } else { 260 - let symbolRegexp = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y") 261 - switch symbolRegexp->RegExp.exec(str) { 262 - | None => None 263 - | Some(res) => 264 - switch RegExp.Result.matches(res) { 265 - | [symb] => { 266 - cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp)) 267 - switch checkVariable(symb) { 268 - | Some(idx) => Some(VarT(idx)) 269 - | None => { 270 - let schematicRegexp = RegExp.fromString(schematicRegexpString) 271 - switch schematicRegexp->RegExp.exec(symb) { 272 - | None => Some(SymbolT(symb)) 273 - | Some(res') => 274 - switch RegExp.Result.matches(res') { 275 - | [s] => Some(SchematicT(s->Int.fromString->Option.getUnsafe)) 276 - | _ => Some(SymbolT(symb)) 277 - } 278 - } 279 - } 280 - } 281 - } 282 - | _ => None 283 - } 284 - } 285 - } 286 - } 287 - 288 - let peek = () => { 289 - // a bit slow, better would be to keep a backlog of lexed tokens.. 290 - let str = String.make(cur.contents) 291 - let tok = lex() 292 - cur := str 293 - tok 294 - } 295 - exception ParseError(string) 296 - let rec parseExp = () => { 297 - let tok = peek() 298 - switch tok { 299 - | Some(SymbolT(s)) => { 300 - let _ = lex() 301 - Some(Symbol({name: s})) 302 - } 303 - | Some(VarT(idx)) => { 304 - let _ = lex() 305 - Some(Var({idx: idx})) 306 - } 307 - | Some(SchematicT(num)) => { 308 - let _ = lex() 309 - switch lex() { 310 - | Some(LParen) => { 311 - let it = ref(None) 312 - let bits = [] 313 - let getVar = (t: option<lexeme>) => 314 - switch t { 315 - | Some(VarT(idx)) => Some(idx) 316 - | _ => None 317 - } 318 - while { 319 - it := lex() 320 - it.contents->getVar->Option.isSome 321 - } { 322 - Array.push(bits, it.contents->getVar->Option.getUnsafe) 323 - } 324 - switch it.contents { 325 - | Some(RParen) => 326 - switch gen { 327 - | Some(g) => { 328 - seen(g, num) 329 - Some(Schematic({schematic: num, allowed: bits})) 330 - } 331 - | None => throw(ParseError("Schematics not allowed here")) 332 - } 333 - | _ => throw(ParseError("Expected closing parenthesis")) 334 - } 335 - } 336 - | _ => throw(ParseError("Expected opening parenthesis")) 337 - } 338 - } 339 - | Some(LParen) => { 340 - let _ = lex() 341 - let bits = [] 342 - let it = ref(None) 343 - while { 344 - it := parseExp() 345 - it.contents->Option.isSome 346 - } { 347 - Array.push(bits, it.contents->Option.getUnsafe) 348 - } 349 - switch lex() { 350 - | Some(RParen) => Some(Compound({subexps: bits})) 351 - | _ => throw(ParseError("Expected closing parenthesis")) 352 - } 353 - } 354 - | _ => None 355 - } 356 - } 357 - switch parseExp() { 358 - | exception ParseError(s) => Error(s) 359 - | None => Error("No expression to parse") 360 - | Some(e) => Ok((e, cur.contents)) 361 - } 362 - } 363 - 364 - let ghostTerm = Ghost

-12

src/SExp.resi

··· 1 - type rec t = 2 - | Symbol({name: string}) 3 - | Compound({subexps: array<t>}) 4 - | Var({idx: int}) 5 - | Schematic({schematic: int, allowed: array<int>}) 6 - | Ghost 7 - 8 - include Signatures.TERM 9 - with type t := t 10 - and type meta = string 11 - and type schematic = int 12 - and type subst = Map.t<int, t>

+435

src/SExpFunc.res

··· 1 + module type ATOM = { 2 + type t 3 + type subst = Map.t<int, t> 4 + let unify: (t, t, ~gen: ref<int>=?) => Seq.t<subst> 5 + let prettyPrint: (t, ~scope: array<string>) => string 6 + let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string> 7 + let substitute: (t, subst) => t 8 + let upshift: (t, int, ~from: int=?) => t 9 + // used for when trying to substitute a variable of the wrong type 10 + let lowerVar: int => option<t> 11 + let lowerSchematic: (int, array<int>) => option<t> 12 + let substDeBruijn: (t, Map.t<int, t>, ~from: int=?, ~to: int) => t 13 + let concrete: t => bool 14 + } 15 + 16 + module IntCmp = Belt.Id.MakeComparable({ 17 + type t = int 18 + let cmp = Pervasives.compare 19 + }) 20 + 21 + module Make = (Atom: ATOM): { 22 + type rec t = 23 + | Atom(Atom.t) 24 + | Compound({subexps: array<t>}) 25 + | Var({idx: int}) 26 + | Schematic({schematic: int, allowed: array<int>}) 27 + 28 + include Signatures.TERM 29 + with type t := t 30 + and type meta = string 31 + and type schematic = int 32 + and type subst = Map.t<int, t> 33 + let mapTerms: (t, t => t) => t 34 + } => { 35 + type rec t = 36 + | Atom(Atom.t) 37 + | Compound({subexps: array<t>}) 38 + | Var({idx: int}) 39 + | Schematic({schematic: int, allowed: array<int>}) 40 + module Atom = Atom 41 + type meta = string 42 + type schematic = int 43 + type subst = Map.t<schematic, t> 44 + let substEqual = Util.mapEqual 45 + let mapSubst = Util.mapMapValues 46 + let makeSubst = () => { 47 + Map.make() 48 + } 49 + let equivalent = (a: t, b: t) => { 50 + a == b 51 + } 52 + let reduce = (term: t) => term 53 + let rec schematicsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) => 54 + switch it { 55 + | Schematic({schematic, _}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(schematic) 56 + | Compound({subexps}) => 57 + subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) => 58 + Belt.Set.union(s, schematicsIn(x)) 59 + ) 60 + | _ => Belt.Set.make(~id=module(IntCmp)) 61 + } 62 + let rec freeVarsIn: t => Belt.Set.t<int, IntCmp.identity> = (it: t) => 63 + switch it { 64 + | Var({idx}) => Belt.Set.make(~id=module(IntCmp))->Belt.Set.add(idx) 65 + | Compound({subexps}) => 66 + subexps->Array.reduce(Belt.Set.make(~id=module(IntCmp)), (s, x) => 67 + Belt.Set.union(s, freeVarsIn(x)) 68 + ) 69 + | _ => Belt.Set.make(~id=module(IntCmp)) 70 + } 71 + let rec substitute = (term: t, subst: subst) => 72 + switch term { 73 + | Compound({subexps}) => Compound({subexps: Array.map(subexps, x => substitute(x, subst))}) 74 + | Schematic({schematic, _}) => 75 + switch Map.get(subst, schematic) { 76 + | None => term 77 + | Some(found) => found 78 + } 79 + | Atom(name) => { 80 + let symbolSubs = 81 + subst 82 + ->Map.entries 83 + ->Iterator.toArray 84 + ->Array.filterMap(((name, v)) => 85 + switch v { 86 + | Atom(v) => Some((name, v)) 87 + | _ => None 88 + } 89 + ) 90 + ->Map.fromArray 91 + Atom(name->Atom.substitute(symbolSubs)) 92 + } 93 + | _ => term 94 + } 95 + 96 + let combineSubst = (s: subst, t: subst) => { 97 + let nu = Map.make() 98 + Map.entries(s)->Iterator.forEach(opt => 99 + switch opt { 100 + | None => () 101 + | Some((key, term)) => nu->Map.set(key, term->substitute(t)) 102 + } 103 + ) 104 + Map.entries(t)->Iterator.forEach(opt => 105 + switch opt { 106 + | None => () 107 + | Some((key, term)) => nu->Map.set(key, term->substitute(s)) 108 + } 109 + ) 110 + nu 111 + } 112 + let emptySubst: subst = Map.make() 113 + let singletonSubst: (int, t) => subst = (schematic, term) => { 114 + let s = Map.make() 115 + s->Map.set(schematic, term) 116 + s 117 + } 118 + let rec unifyTerm = (a: t, b: t): Seq.t<subst> => 119 + switch (a, b) { 120 + | (Atom(na), Atom(nb)) => 121 + Atom.unify(na, nb)->Seq.map(subst => subst->Util.mapMapValues(v => Atom(v))) 122 + | (Compound({subexps: xa}), Compound({subexps: xb})) if Array.length(xa) == Array.length(xb) => 123 + unifyArray(Belt.Array.zip(xa, xb)) 124 + | (Var({idx: ia}), Var({idx: ib})) if ia == ib => Seq.once(emptySubst) 125 + | (Schematic({schematic: sa, _}), Schematic({schematic: sb, _})) if sa == sb => 126 + Seq.once(emptySubst) 127 + | (Schematic({schematic, allowed}), t) 128 + if !Belt.Set.has(schematicsIn(t), schematic) && 129 + Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) => 130 + Seq.once(singletonSubst(schematic, t)) 131 + | (t, Schematic({schematic, allowed})) 132 + if !Belt.Set.has(schematicsIn(t), schematic) && 133 + Belt.Set.subset(freeVarsIn(t), Belt.Set.fromArray(allowed, ~id=module(IntCmp))) => 134 + Seq.once(singletonSubst(schematic, t)) 135 + | (_, _) => Seq.empty 136 + } 137 + and unifyArray = (a: array<(t, t)>): Seq.t<subst> => { 138 + if Array.length(a) == 0 { 139 + Seq.once(emptySubst) 140 + } else { 141 + let (x, y) = a[0]->Option.getUnsafe 142 + unifyTerm(x, y)->Seq.flatMap(s1 => 143 + a 144 + ->Array.sliceToEnd(~start=1) 145 + ->Array.map(((t1, t2)) => (substitute(t1, s1), substitute(t2, s1))) 146 + ->unifyArray 147 + ->Seq.map(s2 => combineSubst(s1, s2)) 148 + ) 149 + } 150 + } 151 + let unify = (a: t, b: t, ~gen as _=?) => unifyTerm(a, b) 152 + 153 + let rec lower = (term: t): option<Atom.t> => 154 + switch term { 155 + | Atom(s) => Some(s) 156 + | Var({idx}) => Atom.lowerVar(idx) 157 + | Schematic({schematic, allowed}) => Atom.lowerSchematic(schematic, allowed) 158 + | Compound({subexps: [e1]}) => lower(e1) 159 + | _ => None 160 + } 161 + let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) => 162 + switch term { 163 + | Atom(s) => { 164 + let symbolSubsts = 165 + substs 166 + ->Array.mapWithIndex((t, i) => lower(t)->Option.map(a => (i, a))) 167 + ->Array.keepSome 168 + ->Map.fromArray 169 + 170 + Atom(Atom.substDeBruijn(s, symbolSubsts, ~from, ~to=Array.length(substs))) 171 + } 172 + 173 + | Compound({subexps}) => 174 + Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))}) 175 + | Var({idx: var}) => 176 + if var < from { 177 + term 178 + } else if var - from < Array.length(substs) && var - from >= 0 { 179 + Option.getUnsafe(substs[var - from]) 180 + } else { 181 + Var({idx: var - Array.length(substs)}) 182 + } 183 + | Schematic({schematic, allowed}) => 184 + Schematic({ 185 + schematic, 186 + allowed: Array.filterMap(allowed, i => 187 + if i < from + Array.length(substs) { 188 + None 189 + } else { 190 + Some(i - (from + Array.length(substs))) 191 + } 192 + ), 193 + }) 194 + } 195 + let rec upshift = (term: t, amount: int, ~from: int=0) => 196 + switch term { 197 + | Atom(s) => Atom(s->Atom.upshift(amount, ~from)) 198 + | Compound({subexps}) => Compound({subexps: Array.map(subexps, x => upshift(x, amount, ~from))}) 199 + | Var({idx}) => 200 + Var({ 201 + idx: if idx >= from { 202 + idx + amount 203 + } else { 204 + idx 205 + }, 206 + }) 207 + | Schematic({schematic, allowed}) => 208 + Schematic({ 209 + schematic, 210 + allowed: Array.map(allowed, i => 211 + if i >= from { 212 + i + amount 213 + } else { 214 + i 215 + } 216 + ), 217 + }) 218 + } 219 + let place = (x: int, ~scope: array<string>) => Schematic({ 220 + schematic: x, 221 + allowed: Array.fromInitializer(~length=Array.length(scope), i => i), 222 + }) 223 + let mergeSubsts = Util.mapUnion 224 + 225 + type gen = ref<int> 226 + let seen = (g: gen, s: int) => { 227 + if s >= g.contents { 228 + g := s + 1 229 + } 230 + } 231 + let fresh = (g: gen, ~replacing as _=?) => { 232 + let v = g.contents 233 + g := g.contents + 1 234 + v 235 + } 236 + let prettyPrintVar = (idx: int, scope: array<string>) => { 237 + switch scope[idx] { 238 + | Some(n) if Array.indexOf(scope, n) == idx => n 239 + | _ => "\\"->String.concat(String.make(idx)) 240 + } 241 + } 242 + let makeGen = () => { 243 + ref(0) 244 + } 245 + let rec prettyPrint = (it: t, ~scope: array<string>) => 246 + switch it { 247 + | Atom(name) => Atom.prettyPrint(name, ~scope) 248 + | Var({idx}) => prettyPrintVar(idx, scope) 249 + | Schematic({schematic, allowed}) => 250 + "?" 251 + ->String.concat(String.make(schematic)) 252 + ->String.concat("(") 253 + ->String.concat(Array.join(allowed->Array.map(idx => prettyPrintVar(idx, scope)), " ")) 254 + ->String.concat(")") 255 + | Compound({subexps}) => 256 + "(" 257 + ->String.concat(Array.join(subexps->Array.map(e => prettyPrint(e, ~scope)), " ")) 258 + ->String.concat(")") 259 + } 260 + 261 + let prettyPrintSubst = (sub, ~scope) => 262 + Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope)) 263 + let symbolRegexpString = `^([^\\s()\\[\\]]+)` 264 + let varRegexpString = "^\\\\([0-9]+)$" 265 + let schematicRegexpString = "^\\?([0-9]+)$" 266 + type lexeme = LParen | RParen | VarT(int) | AtomT(Atom.t) | SchematicT(int) 267 + let nameRES = "^([^\\s.\\[\\]()]+)\\." 268 + let prettyPrintMeta = (str: string) => { 269 + String.concat(str, ".") 270 + } 271 + let parseMeta = (str: string) => { 272 + let re = RegExp.fromStringWithFlags(nameRES, ~flags="y") 273 + switch re->RegExp.exec(str->String.trim) { 274 + | None => Error("not a meta name") 275 + | Some(res) => 276 + switch RegExp.Result.matches(res) { 277 + | [n] => Ok(n, String.sliceToEnd(str->String.trim, ~start=RegExp.lastIndex(re))) 278 + | _ => Error("impossible happened") 279 + } 280 + } 281 + } 282 + let parse = (str: string, ~scope: array<string>, ~gen=?) => { 283 + let cur = ref(String.make(str)) 284 + let lex: unit => option<lexeme> = () => { 285 + let str = String.trim(cur.contents) 286 + cur := str 287 + let checkVariable = (candidate: string) => { 288 + let varRegexp = RegExp.fromString(varRegexpString) 289 + switch Array.indexOf(scope, candidate) { 290 + | -1 => 291 + switch varRegexp->RegExp.exec(candidate) { 292 + | Some(res') => 293 + switch RegExp.Result.matches(res') { 294 + | [idx] => Some(idx->Int.fromString->Option.getUnsafe) 295 + | _ => None 296 + } 297 + | None => None 298 + } 299 + | idx => Some(idx) 300 + } 301 + } 302 + if String.get(str, 0) == Some("(") { 303 + cur := String.sliceToEnd(str, ~start=1) 304 + Some(LParen) 305 + } else if String.get(str, 0) == Some(")") { 306 + cur := String.sliceToEnd(str, ~start=1) 307 + Some(RParen) 308 + } else { 309 + let symbolRegexp = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y") 310 + switch symbolRegexp->RegExp.exec(str) { 311 + | None => None 312 + | Some(res) => 313 + switch RegExp.Result.matches(res) { 314 + | [symb] => { 315 + let specialSymb = tok => { 316 + cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp)) 317 + Some(tok) 318 + } 319 + let regularSymb = () => { 320 + // FIX: not ideal to throw away symbol error message 321 + Console.log(("current", cur.contents)) 322 + Atom.parse(cur.contents, ~scope) 323 + ->Util.Result.ok 324 + ->Option.map(((s, rest)) => { 325 + cur := rest 326 + Console.log(("parsed", s, cur.contents)) 327 + AtomT(s) 328 + }) 329 + } 330 + switch checkVariable(symb) { 331 + | Some(idx) => specialSymb(VarT(idx)) 332 + | None => { 333 + let schematicRegexp = RegExp.fromString(schematicRegexpString) 334 + switch schematicRegexp->RegExp.exec(symb) { 335 + | None => regularSymb() 336 + | Some(res') => 337 + switch RegExp.Result.matches(res') { 338 + | [s] => specialSymb(SchematicT(s->Int.fromString->Option.getUnsafe)) 339 + | _ => regularSymb() 340 + } 341 + } 342 + } 343 + } 344 + } 345 + | _ => None 346 + } 347 + } 348 + } 349 + } 350 + 351 + let peek = () => { 352 + // a bit slow, better would be to keep a backlog of lexed tokens.. 353 + let str = String.make(cur.contents) 354 + let tok = lex() 355 + cur := str 356 + tok 357 + } 358 + exception ParseError(string) 359 + let rec parseExp = () => { 360 + let tok = peek() 361 + switch tok { 362 + | Some(AtomT(s)) => { 363 + let _ = lex() 364 + Some(Atom(s)) 365 + } 366 + | Some(VarT(idx)) => { 367 + let _ = lex() 368 + Some(Var({idx: idx})) 369 + } 370 + | Some(SchematicT(num)) => { 371 + let _ = lex() 372 + switch lex() { 373 + | Some(LParen) => { 374 + let it = ref(None) 375 + let bits = [] 376 + let getVar = (t: option<lexeme>) => 377 + switch t { 378 + | Some(VarT(idx)) => Some(idx) 379 + | _ => None 380 + } 381 + while { 382 + it := lex() 383 + it.contents->getVar->Option.isSome 384 + } { 385 + Array.push(bits, it.contents->getVar->Option.getUnsafe) 386 + } 387 + switch it.contents { 388 + | Some(RParen) => 389 + switch gen { 390 + | Some(g) => { 391 + seen(g, num) 392 + Some(Schematic({schematic: num, allowed: bits})) 393 + } 394 + | None => throw(ParseError("Schematics not allowed here")) 395 + } 396 + | _ => throw(ParseError("Expected closing parenthesis")) 397 + } 398 + } 399 + | _ => throw(ParseError("Expected opening parenthesis")) 400 + } 401 + } 402 + | Some(LParen) => { 403 + let _ = lex() 404 + let bits = [] 405 + let it = ref(None) 406 + while { 407 + it := parseExp() 408 + it.contents->Option.isSome 409 + } { 410 + Array.push(bits, it.contents->Option.getUnsafe) 411 + } 412 + switch lex() { 413 + | Some(RParen) => Some(Compound({subexps: bits})) 414 + | _ => throw(ParseError("Expected closing parenthesis")) 415 + } 416 + } 417 + | _ => None 418 + } 419 + } 420 + switch parseExp() { 421 + | exception ParseError(s) => Error(s) 422 + | None => Error("No expression to parse") 423 + | Some(e) => Ok((e, cur.contents)) 424 + } 425 + } 426 + 427 + let rec concrete = t => 428 + switch t { 429 + | Schematic(_) => true 430 + | Atom(s) => Atom.concrete(s) 431 + | Compound({subexps}) => subexps->Array.every(concrete) 432 + | _ => false 433 + } 434 + let mapTerms = (t, f) => f(t) 435 + }

-6

src/SExpJView.res

··· 1 - module TermView = SExpView 2 - type props = { 3 - judgment: SExp.t, 4 - scope: array<string>, 5 - } 6 - let make = ({judgment, scope}) => SExpView.make({term: judgment, scope})

-3

src/SExpJView.resi

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

-63

src/SExpView.res

··· 1 - type props = {term: SExp.t, scope: array<string>} 2 - open Util 3 - type idx_props = {idx: int, scope: array<string>} 4 - let viewVar = (props: idx_props) => 5 - switch props.scope[props.idx] { 6 - | Some(n) if Array.indexOf(props.scope, n) == props.idx => 7 - {React.string(n)} 8 - | _ => 9 - 10 - {React.string("\\")} 11 - {React.int(props.idx)} 12 - 13 - } 14 - 15 - let makeMeta = (str: string) => 16 - 17 - {React.string(str)} 18 - {React.string(".")} 19 - 20 - 21 - let parenthesise = f => 22 - [ 23 - {React.string("(")} , 24 - ...f, 25 - {React.string(")")} , 26 - ] 27 - 28 - let intersperse = a => 29 - a->Array.flatMapWithIndex((e, i) => 30 - if i == 0 { 31 - [e] 32 - } else { 33 - [React.string(" "), e] 34 - } 35 - ) 36 - 37 - @react.componentWithProps 38 - let rec make = ({term, scope}) => 39 - switch term { 40 - | Compound({subexps: bits}) => 41 - 42 - {bits 43 - ->Array.mapWithIndex((t, i) => React.createElement(make, withKey({term: t, scope}, i))) 44 - ->intersperse 45 - ->parenthesise 46 - ->React.array} 47 - 48 - | Var({idx}) => viewVar({idx, scope}) 49 - | Symbol({name: s}) => {React.string(s)} 50 - | Schematic({schematic: s, allowed: vs}) => 51 - 52 - {React.string("?")} 53 - {React.int(s)} 54 - 55 - {vs 56 - ->Array.mapWithIndex((v, i) => React.createElement(viewVar, withKey({idx: v, scope}, i))) 57 - ->intersperse 58 - ->parenthesise 59 - ->React.array} 60 - 61 - 62 - | Ghost => React.null 63 - }

-1

src/SExpView.resi

··· 1 - include Signatures.TERM_VIEW with module Term := SExp

+79

src/SExpViewFunc.res

··· 1 + module type ATOM_VIEW = { 2 + module Atom: SExpFunc.ATOM 3 + type props = {name: Atom.t, scope: array<string>} 4 + let make: props => React.element 5 + } 6 + 7 + module Make = ( 8 + Atom: SExpFunc.ATOM, 9 + AtomView: ATOM_VIEW with module Atom := Atom, 10 + SExp: module type of SExpFunc.Make(Atom), 11 + ): { 12 + include Signatures.TERM_VIEW with module Term := SExp 13 + } => { 14 + type props = {term: SExp.t, scope: array<string>} 15 + open Util 16 + type idx_props = {idx: int, scope: array<string>} 17 + let viewVar = (props: idx_props) => 18 + switch props.scope[props.idx] { 19 + | Some(n) if Array.indexOf(props.scope, n) == props.idx => 20 + {React.string(n)} 21 + | _ => 22 + 23 + {React.string("\\")} 24 + {React.int(props.idx)} 25 + 26 + } 27 + 28 + let makeMeta = (str: string) => 29 + 30 + {React.string(str)} 31 + {React.string(".")} 32 + 33 + 34 + let parenthesise = f => 35 + [ 36 + {React.string("(")} , 37 + ...f, 38 + {React.string(")")} , 39 + ] 40 + 41 + let intersperse = a => 42 + a->Array.flatMapWithIndex((e, i) => 43 + if i == 0 { 44 + [e] 45 + } else { 46 + [React.string(" "), e] 47 + } 48 + ) 49 + 50 + @react.componentWithProps 51 + let rec make = ({term, scope}) => 52 + switch term { 53 + | Compound({subexps: bits}) => 54 + 55 + {bits 56 + ->Array.mapWithIndex((t, i) => React.createElement(make, withKey({term: t, scope}, i))) 57 + ->intersperse 58 + ->parenthesise 59 + ->React.array} 60 + 61 + | Var({idx}) => viewVar({idx, scope}) 62 + | Atom(name) => 63 + 64 + <AtomView name scope /> 65 + 66 + | Schematic({schematic: s, allowed: vs}) => 67 + 68 + {React.string("?")} 69 + {React.int(s)} 70 + 71 + {vs 72 + ->Array.mapWithIndex((v, i) => React.createElement(viewVar, withKey({idx: v, scope}, i))) 73 + ->intersperse 74 + ->parenthesise 75 + ->React.array} 76 + 77 + 78 + } 79 + }

+31 -34

src/Scratch.res

··· 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)) 1 + module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTerm, HOTermJView)) 2 + module InductiveS = Editable.TextArea(InductiveSet.Make(HOTerm, HOTerm, HOTermJView)) 5 3 6 4 module EqualityViews = MethodView.CombineMethodView( 7 5 HOTerm, 8 - HOTermJ, 9 - MethodView.RewriteView(HOTermJ), 10 - MethodView.RewriteReverseView(HOTermJ), 6 + HOTerm, 7 + MethodView.RewriteView(HOTerm), 8 + MethodView.RewriteReverseView(HOTerm), 11 9 ) 12 10 module ConstructorEqualityViews = MethodView.CombineMethodView( 13 11 HOTerm, 14 - HOTermJ, 12 + HOTerm, 15 13 EqualityViews, 16 - MethodView.ConstructorNeqView(HOTermJ), 14 + MethodView.ConstructorNeqView(HOTerm), 17 15 ) 18 16 module RewritesView = MethodView.CombineMethodView( 19 17 HOTerm, 20 - HOTermJ, 18 + HOTerm, 21 19 ConstructorEqualityViews, 22 - MethodView.ConstructorInjView(HOTermJ), 20 + MethodView.ConstructorInjView(HOTerm), 23 21 ) 24 22 module DerivationsOrLemmasView = MethodView.CombineMethodView( 25 23 HOTerm, 26 - HOTermJ, 24 + HOTerm, 27 25 MethodView.CombineMethodView( 28 26 HOTerm, 29 - HOTermJ, 30 - MethodView.DerivationView(HOTerm, HOTermJ), 31 - MethodView.LemmaView(HOTerm, HOTermJ, HOTermJView), 27 + HOTerm, 28 + MethodView.DerivationView(HOTerm, HOTerm), 29 + MethodView.LemmaView(HOTerm, HOTerm, HOTermJView), 32 30 ), 33 - MethodView.EliminationView(HOTerm, HOTermJ), 31 + MethodView.EliminationView(HOTerm, HOTerm), 34 32 ) 35 - module DLRView = MethodView.CombineMethodView( 33 + module DLRView = MethodView.CombineMethodView(HOTerm, HOTerm, DerivationsOrLemmasView, RewritesView) 34 + module DLREView = MethodView.CombineMethodView( 36 35 HOTerm, 37 - HOTermJ, 38 - DerivationsOrLemmasView, 39 - RewritesView, 40 - ) 41 - module DLREView = MethodView.CombineMethodView( 42 36 HOTerm, 43 - HOTermJ, 44 37 DLRView, 45 - MethodView.EliminationView(HOTerm, HOTermJ), 38 + MethodView.EliminationView(HOTerm, HOTerm), 46 39 ) 47 40 48 41 // Temporarily use DLRView (without Elimination) due to HOTerm unification bug 49 - module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTermJ, HOTermJView, DLRView)) 50 - module ConfS = ConfigBlock.Make(HOTerm, HOTermJ) 42 + module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView)) 43 + module ConfS = ConfigBlock.Make(HOTerm, HOTerm) 51 44 45 + module StringSExp = SExpFunc.Make(StringSymbol.Atom) 46 + module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp) 47 + module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView) 52 48 module AxiomStr = Editable.TextArea(StringAxiomSet) 49 + 53 50 module DerivationsOrLemmasStrView = MethodView.CombineMethodView( 54 - StringTerm, 55 - StringTermJudgment, 56 - MethodView.DerivationView(StringTerm, StringTermJudgment), 57 - MethodView.LemmaView(StringTerm, StringTermJudgment, StringTermJView), 51 + StringSExp, 52 + StringSExp, 53 + MethodView.DerivationView(StringSExp, StringSExp), 54 + MethodView.LemmaView(StringSExp, StringSExp, StringSExpJView), 58 55 ) 59 56 module DLEStrView = MethodView.CombineMethodView( 60 - StringTerm, 61 - StringTermJudgment, 57 + StringSExp, 58 + StringSExp, 62 59 DerivationsOrLemmasStrView, 63 - MethodView.EliminationView(StringTerm, StringTermJudgment), 60 + MethodView.EliminationView(StringSExp, StringSExp), 64 61 ) 65 62 module TheoremStr = Editable.TextArea( 66 - Theorem.Make(StringTerm, StringTermJudgment, StringTermJView, DLEStrView), 63 + Theorem.Make(StringSExp, StringSExp, StringSExpJView, DLEStrView), 67 64 )

+6 -20

src/Signatures.res

··· 24 24 let parseMeta: string => result<(meta, string), string> 25 25 let prettyPrint: (t, ~scope: array<meta>) => string 26 26 let prettyPrintMeta: meta => string 27 - let ghostTerm: t 27 + // will unifying t with a term give meaningful substitutions? 28 + let concrete: t => bool 28 29 } 29 30 30 31 module type JUDGMENT = { 31 32 module Term: TERM 32 33 type t 33 - type subst 34 - type substCodom 35 - type schematic = Term.schematic 36 - type meta = Term.meta 37 - let mapSubst: (subst, substCodom => substCodom) => subst 38 - let mergeSubsts: (subst, subst) => subst 39 - let substitute: (t, subst) => t 40 - let substituteSubstCodom: (substCodom, subst) => substCodom 34 + let substitute: (t, Term.subst) => t 41 35 let equivalent: (t, t) => bool 42 - let unify: (t, t, ~gen: Term.gen=?) => Seq.t<subst> 43 - let substDeBruijn: (t, array<substCodom>, ~from: int=?) => t 36 + let unify: (t, t, ~gen: Term.gen=?) => Seq.t<Term.subst> 37 + let substDeBruijn: (t, array<Term.t>, ~from: int=?) => t 44 38 let reduce: t => t 45 39 let upshift: (t, int, ~from: int=?) => t 46 - let upshiftSubstCodom: (substCodom, int, ~from: int=?) => substCodom 47 - let placeSubstCodom: (schematic, ~scope: array<meta>) => substCodom 48 40 // Map a function over all terms in the judgment 49 41 let mapTerms: (t, Term.t => Term.t) => t 50 42 let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string> 51 - let parseSubstCodom: ( 52 - string, 53 - ~scope: array<Term.meta>, 54 - ~gen: Term.gen=?, 55 - ) => result<(substCodom, string), string> 56 43 let prettyPrint: (t, ~scope: array<Term.meta>) => string 57 - let prettyPrintSubstCodom: (substCodom, ~scope: array<Term.meta>) => string 58 - let ghostJudgment: t 44 + let concrete: t => bool 59 45 } 60 46 61 47 module type TERM_VIEW = {

+541

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

+8

src/StringA.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 + 7 + module Atom: SExpFunc.ATOM with type t = t 8 + module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom

+49 -26

src/StringAxiomSet.res

··· 1 1 open Component 2 2 3 - module Term = StringTerm 4 - module Judgment = StringTermJudgment 5 - module JudgmentView = StringTermJView 3 + module StringSExp = SExpFunc.Make(StringSymbol.Atom) 4 + module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp) 5 + module JudgmentView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView) 6 6 7 - module Rule = Rule.Make(Term, Judgment) 8 - module RuleView = RuleView.Make(Term, Judgment, JudgmentView) 9 - module Ports = Ports(Term, Judgment) 7 + module Rule = Rule.Make(StringSExp, StringSExp) 8 + module RuleView = RuleView.Make(StringSExp, StringSExp, JudgmentView) 9 + module Ports = Ports(StringSExp, StringSExp) 10 10 type state = { 11 11 raw: dict<Rule.t>, 12 12 derived: dict<Rule.t>, ··· 30 30 ) 31 31 } 32 32 33 - let getSExpName = (t: SExp.t): option<string> => 33 + let getSExpName = (t: StringSExp.t): option<string> => 34 34 switch t { 35 - | Symbol({name}) => Some(name) 35 + | Atom(name) => Some(name->StringSymbol.Atom.prettyPrint(~scope=[])) 36 36 | _ => None 37 37 } 38 38 39 + let destructure = (r: StringSExp.t): (StringA.Atom.t, string) => 40 + switch r { 41 + | Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => (s, name) 42 + | _ => throw(Util.Unreachable("expected valid induction rule")) 43 + } 44 + let destructureOpt = (r: StringSExp.t): option<(StringA.Atom.t, string)> => 45 + switch r { 46 + | Compound({subexps: [Atom(StringS(s)), Atom(ConstS(name))]}) => Some((s, name)) 47 + | _ => None 48 + } 49 + let structure = (lhs: StringSExp.t, rhs: StringSExp.t): StringSExp.t => Compound({ 50 + subexps: [lhs, rhs], 51 + }) 39 52 let findMentionedRuleGroups = (group: judgeGroup, allGroups: array<judgeGroup>): array< 40 53 judgeGroup, 41 54 > => { ··· 45 58 group.rules 46 59 ->Array.flatMap(r => 47 60 r.premises 48 - ->Array.map(p => p.conclusion->Pair.second->getSExpName) 49 - ->Array.keepSome 61 + ->Array.filterMap(p => p.conclusion->destructureOpt->Option.map(Pair.second)) 50 62 ->Array.filter(name => allGroupNames->Array.find(name' => name' == name)->Option.isSome) 51 63 ) 52 64 ->Set.fromArray ··· 74 86 let xIdx = vars->Array.findIndex(i => i == x) 75 87 let aIdx = vars->Array.findIndex(i => i == a) 76 88 let bIdx = vars->Array.findIndex(i => i == b) 77 - let surround = (t: StringTerm.t, aIdx: int, bIdx: int) => { 78 - Array.concat(Array.concat([StringTerm.Var({idx: aIdx})], t), [StringTerm.Var({idx: bIdx})]) 89 + let surround = (t: StringA.Atom.t, aIdx: int, bIdx: int) => { 90 + Array.concat(Array.concat([StringA.Var({idx: aIdx})], t), [StringA.Var({idx: bIdx})]) 79 91 } 80 - let lookupGroup = (t: SExp.t): option<int> => 81 - mentionedGroups->Array.findIndexOpt(g => t == SExp.Symbol({name: g.name})) 92 + let lookupGroup = (name: string): option<int> => 93 + mentionedGroups->Array.findIndexOpt(g => name == g.name) 82 94 let rec replaceJudgeRHS = (rule: Rule.t, baseIdx: int): Rule.t => { 83 95 let baseIdx = baseIdx + Array.length(rule.vars) 96 + let (s, name) = destructure(rule.conclusion) 84 97 let inductionHyps = 85 98 rule.premises 86 - ->Array.filter(r => lookupGroup(r.conclusion->Pair.second)->Option.isSome) 99 + ->Array.filter(r => 100 + r.conclusion 101 + ->destructureOpt 102 + ->Option.flatMap(conclusion => conclusion->Pair.second->lookupGroup) 103 + ->Option.isSome 104 + ) 87 105 ->Array.map(r => replaceJudgeRHS(r, baseIdx)) 88 - let pIdx = lookupGroup(rule.conclusion->Pair.second)->Option.getExn 106 + let pIdx = lookupGroup(name)->Option.getExn 89 107 { 90 108 vars: rule.vars, 91 109 premises: rule.premises->Array.concat(inductionHyps), 92 - conclusion: ( 93 - surround(rule.conclusion->Pair.first, aIdx + baseIdx, bIdx + baseIdx), 110 + conclusion: structure( 111 + surround(s, aIdx + baseIdx, bIdx + baseIdx)->StringS->Atom, 94 112 Var({idx: pIdx + baseIdx}), 95 113 ), 96 114 } ··· 102 120 { 103 121 Rule.vars: [], 104 122 premises: [], 105 - conclusion: ([StringTerm.Var({idx: xIdx})], Symbol({name: group.name})), 123 + conclusion: structure(Var({idx: xIdx}), Atom(ConstS(group.name))), 106 124 }, 107 125 ], 108 126 mentionedGroups->Array.flatMap(g => g.rules->Array.map(r => replaceJudgeRHS(r, 0))), 109 127 ), 110 - conclusion: (surround([StringTerm.Var({idx: xIdx})], aIdx, bIdx), Var({idx: 0})), // TODO: clean here 128 + conclusion: structure( 129 + surround([StringA.Var({idx: xIdx})], aIdx, bIdx)->StringS->Atom, 130 + Var({idx: 0}), 131 + ), // TODO: clean here 111 132 } 112 133 } 113 134 ··· 143 164 getBase(str)->Result.map(raw => { 144 165 let grouped: dict<array<Rule.t>> = Dict.make() 145 166 raw->Dict.forEach(rule => 146 - switch rule.conclusion->Pair.second { 147 - | Symbol({name: a}) => 148 - switch grouped->Dict.get(a) { 149 - | None => grouped->Dict.set(a, [rule]) 167 + switch rule.conclusion { 168 + | Compound({subexps: [Atom(StringS(_)), Atom(ConstS(name))]}) => 169 + switch grouped->Dict.get(name) { 170 + | None => grouped->Dict.set(name, [rule]) 150 171 | Some(rs) => rs->Array.push(rule) 151 172 } 152 173 | _ => () ··· 178 199 <div 179 200 className={"axiom-set axiom-set-"->String.concat( 180 201 String.make(props.imports.ruleStyle->Option.getOr(Hybrid)), 181 - )}> 202 + )} 203 + > 182 204 {content 183 205 ->Dict.toArray 184 206 ->Array.mapWithIndex(((n, r), i) => ··· 186 208 rule={r} 187 209 scope={[]} 188 210 key={String.make(i)} 189 - style={props.imports.ruleStyle->Option.getOr(Hybrid)}> 211 + style={props.imports.ruleStyle->Option.getOr(Hybrid)} 212 + > 190 213 {React.string(n)} 191 214 </RuleView> 192 215 )

+86

src/StringSymbol.res

··· 1 + type t = StringS(StringA.Atom.t) | ConstS(string) 2 + 3 + module Atom: SExpFunc.ATOM with type t = t = { 4 + type t = t 5 + type subst = Map.t<int, t> 6 + type gen = ref<int> 7 + let parse = (s, ~scope, ~gen: option<gen>=?) => { 8 + StringA.Atom.parse(s, ~scope, ~gen?) 9 + ->Result.map(((r, rest)) => (StringS(r), rest)) 10 + ->Util.Result.or(() => 11 + Symbolic.Atom.parse(s, ~scope, ~gen?)->Result.map(((r, rest)) => (ConstS(r), rest)) 12 + ) 13 + } 14 + let prettyPrint = (s, ~scope) => 15 + switch s { 16 + | StringS(s) => StringA.Atom.prettyPrint(s, ~scope) 17 + | ConstS(s) => Symbolic.Atom.prettyPrint(s, ~scope) 18 + } 19 + let unify = (s1, s2, ~gen=?) => 20 + switch (s1, s2) { 21 + | (StringS(s1), StringS(s2)) => 22 + StringA.Atom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => StringS(v))) 23 + | (ConstS(s1), ConstS(s2)) => 24 + Symbolic.Atom.unify(s1, s2, ~gen?)->Seq.map(subst => subst->Util.mapMapValues(v => ConstS(v))) 25 + | (_, _) => Seq.empty 26 + } 27 + let substitute = (s, subst: subst) => 28 + switch s { 29 + | StringS(s) => { 30 + let stringSubs = 31 + subst 32 + ->Map.entries 33 + ->Iterator.toArrayWithMapper(((i, v)) => 34 + switch v { 35 + | StringS(s) => Some((i, s)) 36 + | _ => None 37 + } 38 + ) 39 + ->Array.keepSome 40 + ->Map.fromArray 41 + StringS(StringA.Atom.substitute(s, stringSubs)) 42 + } 43 + | ConstS(s) => ConstS(s) 44 + } 45 + let upshift = (s, amount: int, ~from=?) => 46 + switch s { 47 + | StringS(s) => StringS(s->StringA.Atom.upshift(amount, ~from?)) 48 + | ConstS(s) => ConstS(s) 49 + } 50 + let lowerVar = idx => Some(StringS([StringA.Var({idx: idx})])) 51 + let lowerSchematic = (schematic, allowed) => Some( 52 + StringS([StringA.Schematic({schematic, allowed})]), 53 + ) 54 + let substDeBruijn = (s, substs: Map.t<int, t>, ~from=?, ~to: int) => 55 + switch s { 56 + | StringS(s) => { 57 + let stringSubs = 58 + substs 59 + ->Map.entries 60 + ->Iterator.toArrayWithMapper(((i, v)) => 61 + switch v { 62 + | StringS(s) => Some((i, s)) 63 + | _ => None 64 + } 65 + ) 66 + ->Array.keepSome 67 + ->Map.fromArray 68 + StringS(StringA.Atom.substDeBruijn(s, stringSubs, ~from?, ~to)) 69 + } 70 + | ConstS(s) => ConstS(s) 71 + } 72 + let concrete = s => 73 + switch s { 74 + | StringS(s) => StringA.Atom.concrete(s) 75 + | ConstS(_) => false 76 + } 77 + } 78 + 79 + module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom = { 80 + type props = {name: Atom.t, scope: array<string>} 81 + let make = ({name, scope}: props) => 82 + switch name { 83 + | StringS(name) => <StringA.AtomView name scope /> 84 + | ConstS(name) => <Symbolic.AtomView name scope /> 85 + } 86 + }

+3

src/StringSymbol.resi

··· 1 + type t = StringS(StringA.Atom.t) | ConstS(string) 2 + module Atom: SExpFunc.ATOM with type t = t 3 + module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom

-529

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

-16

src/StringTerm.resi

··· 1 - type rec piece = 2 - | String(string) 3 - | Var({idx: int}) 4 - | Schematic({schematic: int, allowed: array<int>}) 5 - | Ghost 6 - type t = array<piece> 7 - type subst = Map.t<int, t> 8 - 9 - include Signatures.TERM 10 - with type t := t 11 - and type meta = string 12 - and type schematic = int 13 - and type subst := subst 14 - 15 - let fromSExp: SExp.t => t 16 - 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 - 8 - <StringTermView term scope /> 9 - {React.string(" ")} 10 - <SExpView term=j scope /> 11 - 12 - }

-3

src/StringTermJView.resi

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

-118

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 mapTerms = ((t, j): t, f: StringTerm.t => StringTerm.t): t => { 80 - // Apply the function to both the string term and the sexp (converted to/from string term) 81 - let newT = f(t) 82 - let newJ = j->StringTerm.fromSExp->f->StringTerm.toSExp 83 - (newT, newJ) 84 - } 85 - 86 - let parse = (str: string, ~scope: array<StringTerm.meta>, ~gen=?) => { 87 - StringTerm.parse(str, ~scope, ~gen?)->Result.flatMap(((t, str)) => 88 - SExp.parse(str, ~scope)->Result.map(((j, str)) => ((t, j), str)) 89 - ) 90 - } 91 - 92 - // HACK: this does work due to the hacky string-sexp conversion we have inplace with substitutions, 93 - // but a different solution would be preferable 94 - let placeSubstCodom = (x: int, ~scope: array<string>) => StringV(StringTerm.place(x, ~scope)) 95 - 96 - let parseSubstCodom = (str: string, ~scope: array<StringTerm.meta>, ~gen=?) => { 97 - switch StringTerm.parse(str, ~scope, ~gen?) { 98 - | Ok(t, str) => Ok(StringV(t), str) 99 - | Error(stringE) => 100 - switch SExp.parse(str, ~scope) { 101 - | Ok(t, str) => Ok(SExpV(t), str) 102 - | Error(sExpE) => 103 - Error( 104 - `string or sexp expected.\nstring parsing failed with error: ${stringE}\nsexp parsing failed with error: ${sExpE}`, 105 - ) 106 - } 107 - } 108 - } 109 - 110 - let prettyPrint = ((t, j): t, ~scope: array<StringTerm.meta>) => 111 - `${StringTerm.prettyPrint(t, ~scope)} ${SExp.prettyPrint(j, ~scope)}` 112 - let prettyPrintSubstCodom = (v: substCodom, ~scope: array<StringTerm.meta>) => 113 - switch v { 114 - | StringV(t) => StringTerm.prettyPrint(t, ~scope) 115 - | SExpV(t) => SExp.prettyPrint(t, ~scope) 116 - } 117 - 118 - let ghostJudgment = (StringTerm.ghostTerm, SExp.ghostTerm)

-3

src/StringTermJudgment.resi

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

-65

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 - {React.string(n)} 7 - | _ => 8 - 9 - {React.string("\\")} 10 - {React.int(props.idx)} 11 - 12 - } 13 - 14 - let makeMeta = (str: string) => 15 - 16 - {React.string(str)} 17 - {React.string(".")} 18 - 19 - 20 - let parenthesise = f => 21 - [ 22 - {React.string("(")} , 23 - ...f, 24 - {React.string(")")} , 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) => {React.string(s)} 35 - | Schematic({schematic: s, allowed: vs}) => 36 - 37 - {React.string("?")} 38 - {React.int(s)} 39 - 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 - 48 - 49 - | Ghost => {React.string("§String.Ghost")} 50 - } 51 - } 52 - 53 - @react.componentWithProps 54 - let make = ({term, scope}) => 55 - 56 - {React.string("\"")} 57 - {term 58 - ->Array.mapWithIndex((piece, i) => { 59 - let key = Int.toString(i) 60 - <Piece piece scope key /> 61 - }) 62 - ->intersperse 63 - ->React.array} 64 - {React.string("\"")} 65 -

-1

src/StringTermView.resi

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

+29

src/Symbolic.res

··· 1 + type t = string 2 + module Atom = { 3 + type t = string 4 + type subst = Map.t<int, string> 5 + let unify = (a, b, ~gen as _=?) => 6 + if a == b { 7 + Seq.once(Map.make()) 8 + } else { 9 + Seq.empty 10 + } 11 + let prettyPrint = (name, ~scope as _: array<string>) => name 12 + let symbolRegex = /^([^\s()\[\]]+)/ 13 + let parse = (string, ~scope as _: array<string>, ~gen as _=?) => 14 + switch Util.execRe(symbolRegex, string) { 15 + | Some(([res], l)) => Ok((res, string->String.substringToEnd(~start=l))) 16 + | _ => Error("constant symbol parse error") 17 + } 18 + let substitute = (name, _) => name 19 + let lowerVar = _ => None 20 + let lowerSchematic = (_, _) => None 21 + let substDeBruijn = (name, _, ~from as _=?, ~to as _) => name 22 + let concrete = _ => false 23 + let upshift = (t, _, ~from as _=?) => t 24 + } 25 + 26 + module AtomView = { 27 + type props = {name: string, scope: array<string>} 28 + let make = (props: props) => React.string(props.name) 29 + }

+3

src/Symbolic.resi

··· 1 + type t = string 2 + module Atom: SExpFunc.ATOM with type t = t 3 + module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom

-18

src/TermAsJudgment.res

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

+12

src/TermViewAsJudgmentView.res

··· 1 + module Make = ( 2 + Term: Signatures.TERM, 3 + Judgment: Signatures.JUDGMENT with module Term := Term and type t = Term.t, 4 + TermView: Signatures.TERM_VIEW with module Term := Term, 5 + ): (Signatures.JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment) => { 6 + module TermView = TermView 7 + type props = { 8 + judgment: Judgment.t, 9 + scope: array<Term.meta>, 10 + } 11 + let make = ({judgment, scope}) => TermView.make({term: judgment, scope}) 12 + }

+13

src/Util.res

··· 117 117 | i => i 118 118 } 119 119 } 120 + 121 + module Result = { 122 + let ok = (r: result<'a, 'b>): option<'a> => 123 + switch r { 124 + | Ok(a) => Some(a) 125 + | Error(_) => None 126 + } 127 + let or = (r1: result<'a, 'b>, r2: unit => result<'a, 'b>): result<'a, 'b> => 128 + switch r1 { 129 + | Ok(_) => r1 130 + | Error(_) => r2() 131 + } 132 + }

+23 -20

tests/RuleTest.res

··· 31 31 } 32 32 } 33 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 - }) 34 + // zoraBlock("string terms", t => { 35 + // module T = MakeTest(StringSExp, StringSExpJ) 36 + // t->T.testParseInner( 37 + // `[s1. ("$s1" p) |- ("($s1)" p)]`, 38 + // { 39 + // vars: ["s1"], 40 + // premises: [ 41 + // { 42 + // vars: [], 43 + // premises: [], 44 + // conclusion: StringSExp.Compound( 45 + // [StringA.Atom.Var({idx: 0})], 46 + // SExp.pAtom("p")->StringA.AtomJudgment.ConstS->StringSymbolic.Atom, 47 + // ), 48 + // }, 49 + // ], 50 + // conclusion: ( 51 + // [StringA.Atom.String("("), StringA.Atom.Var({idx: 0}), StringA.Atom.String(")")], 52 + // SExp.pAtom("p")->StringA.AtomJudgment.ConstS->StringSymbolic.Atom, 53 + // ), 54 + // }, 55 + // ) 56 + // })

+7 -11

tests/SExpTest.res

··· 1 1 open Zora 2 + 3 + module SExp = SExpFunc.Make(Symbolic.Atom) 2 4 open SExp 3 5 4 6 module Util = TestUtil.MakeTerm(SExp) 5 7 6 8 zoraBlock("parse symbol", t => { 7 - t->block("single char", t => t->Util.testParse("x", Symbol({name: "x"}))) 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 + t->block("single char", t => t->Util.testParse("x", Atom("x"))) 10 + t->block("multi char", t => t->Util.testParse("xyz", Atom("xyz"))) 11 + t->block("judgement terminal", t => t->Util.testParse("a]", Atom("a"), ~expectRemaining="]")) 12 12 }) 13 13 14 14 zoraBlock("parse var", t => { ··· 29 29 30 30 zoraBlock("parse compound", t => { 31 31 t->block("unit", t => t->Util.testParse("()", Compound({subexps: []}))) 32 - t->block("single", t => t->Util.testParse("(a)", Compound({subexps: [Symbol({name: "a"})]}))) 32 + t->block("single", t => t->Util.testParse("(a)", Compound({subexps: [Atom("a")]}))) 33 33 t->block("multiple", t => { 34 34 t->Util.testParse( 35 35 "(a \\1 ?1())", 36 36 Compound({ 37 - subexps: [Symbol({name: "a"}), Var({idx: 1}), Schematic({schematic: 1, allowed: []})], 37 + subexps: [Atom("a"), Var({idx: 1}), Schematic({schematic: 1, allowed: []})], 38 38 }), 39 39 ) 40 40 }) ··· 63 63 }) 64 64 t->block("comp-schema comp neq", t => { 65 65 t->Util.testUnify(schemaComp, comp1, ~expect=[]) 66 - }) 67 - t->block("ghost", t => { 68 - t->Util.testUnifyFail(x, SExp.ghostTerm) 69 - t->Util.testUnify(schema1, SExp.ghostTerm) 70 66 }) 71 67 })

+49 -45

tests/StringTermTest.res

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

+150 -3

tests/TestUtil.res

··· 1 1 open Signatures 2 2 open Zora 3 - open Util 4 3 5 4 let stringifyExn = (t: 'a) => JSON.stringifyAny(t, ~space=2)->Option.getExn 6 5 6 + module type CAN_PARSE = { 7 + type t 8 + type meta 9 + type gen 10 + let parse: (string, ~scope: array<meta>, ~gen: gen=?) => result<(t, string), string> 11 + let prettyPrint: (t, ~scope: array<meta>) => string 12 + let makeGen: unit => gen 13 + } 14 + 15 + module MakeParseTester = (Subj: CAN_PARSE) => { 16 + let testParse = ( 17 + t: Zora.t, 18 + input: string, 19 + expect: Subj.t, 20 + ~scope=[], 21 + ~msg=?, 22 + ~expectRemaining=?, 23 + ) => { 24 + let res = Subj.parse(input, ~scope, ~gen=Subj.makeGen()) 25 + switch res { 26 + | Ok((parsed, parsedRemaining)) => { 27 + t->equal( 28 + parsedRemaining, 29 + expectRemaining->Option.getOr(""), 30 + ~msg=input ++ " input consumed", 31 + ) 32 + // NOTE: we're checking for equality here, not equivalency 33 + // error messages are better this way 34 + t->equal(parsed, expect, ~msg?) 35 + } 36 + | Error(msg) => t->fail(~msg="parse failed: " ++ msg) 37 + } 38 + } 39 + let testParseFail = (t: Zora.t, input: string, ~scope=[]) => { 40 + let res = Subj.parse(input, ~scope, ~gen=Subj.makeGen()) 41 + switch res { 42 + | Ok((p, remaining)) => 43 + t->fail( 44 + ~msg=`parse intended to fail, but succeeded: ${Subj.prettyPrint( 45 + p, 46 + ~scope, 47 + )}\nremaining: ${remaining}`, 48 + ) 49 + | Error(_) => t->ok(true) 50 + } 51 + } 52 + let testParsePrettyPrint = (t: Zora.t, input, expected, ~scope=[]) => { 53 + let res = Subj.parse(input, ~scope=[], ~gen=Subj.makeGen()) 54 + 55 + switch res { 56 + | Ok(res) => { 57 + let result = Subj.prettyPrint(res->Pair.first, ~scope) 58 + t->equal(result, expected, ~msg="prettyPrint output matches expected") 59 + } 60 + | Error(msg) => t->fail(~msg="parse failed: " ++ msg) 61 + } 62 + } 63 + let parse = (t: Zora.t, input: string): Subj.t => { 64 + let res = Subj.parse(input, ~scope=[], ~gen=Subj.makeGen()) 65 + switch res { 66 + | Ok((term, "")) => term 67 + | Ok((_, rest)) => { 68 + t->fail(~msg="parse incomplete: " ++ rest) 69 + throw(Util.Unreachable("")) 70 + } 71 + | Error(msg) => { 72 + t->fail(~msg="parse failed: " ++ msg) 73 + throw(Util.Unreachable("")) 74 + } 75 + } 76 + } 77 + } 78 + 79 + module type CAN_UNIFY = { 80 + type t 81 + type subst 82 + type gen 83 + type meta 84 + let unify: (t, t, ~gen: gen=?) => Seq.t<subst> 85 + let substEqual: (subst, subst) => bool 86 + let prettyPrintSubst: (subst, ~scope: array<meta>) => string 87 + } 88 + 89 + module MakeUnifyTester = (Subj: CAN_UNIFY) => { 90 + let testUnify = ( 91 + t: Zora.t, 92 + t1: Subj.t, 93 + t2: Subj.t, 94 + ~expect: option<array<Subj.subst>>=?, 95 + ~msg=?, 96 + ) => { 97 + let res = Subj.unify(t1, t2)->Seq.take(10) 98 + switch expect { 99 + | Some(expect) => { 100 + let expect = Seq.fromArray(expect) 101 + let noMatches = 102 + expect 103 + ->Seq.filter(sub1 => Seq.find(res, sub2 => Subj.substEqual(sub1, sub2))->Option.isNone) 104 + ->Seq.map(t => Subj.prettyPrintSubst(t, ~scope=[])) 105 + ->Seq.toArray 106 + let msg = 107 + msg->Option.getOr("each substitution in `expect` should have a match in solutions") 108 + t->equal(noMatches, [], ~msg) 109 + } 110 + | None => { 111 + let msg = msg->Option.getOr("expect non-nil substitution sequence") 112 + t->ok(res->Seq.head->Option.isSome, ~msg) 113 + } 114 + } 115 + } 116 + 117 + let testUnifyFail = (t: Zora.t, a: Subj.t, b: Subj.t, ~msg=?) => { 118 + let res = Subj.unify(a, b) 119 + if res->Seq.length != 0 { 120 + t->fail(~msg="unification succeeded: " ++ stringifyExn(a) ++ " and " ++ stringifyExn(b)) 121 + } else { 122 + t->ok(true, ~msg=msg->Option.getOr("unification failed")) 123 + } 124 + } 125 + } 126 + 127 + module MakeAtomTester = (Atom: SExpFunc.ATOM) => { 128 + module ParseWrapper: CAN_PARSE 129 + with type t = Atom.t 130 + and type meta = string 131 + and type gen = ref<int> = { 132 + include Atom 133 + type gen = ref<int> 134 + type meta = string 135 + let makeGen = () => ref(0) 136 + } 137 + module ParseTester = MakeParseTester(ParseWrapper) 138 + module UnifyWrapper: CAN_UNIFY 139 + with type t = Atom.t 140 + and type meta = string 141 + and type gen = ref<int> 142 + and type subst = Atom.subst = { 143 + include Atom 144 + type meta = string 145 + type gen = ref<int> 146 + let prettyPrintSubst = (sub, ~scope) => 147 + Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope)) 148 + let substEqual = Util.mapEqual 149 + } 150 + module UnifyTester = MakeUnifyTester(UnifyWrapper) 151 + } 152 + 153 + // TODO: modularise in the same way as AtomTester 7 154 module MakeTerm = (Term: TERM) => { 8 155 let termEquivalent = (t: Zora.t, t1: Term.t, t2: Term.t, ~msg=?) => { 9 156 t->ok( ··· 64 211 | Ok((term, "")) => term 65 212 | Ok((_, rest)) => { 66 213 t->fail(~msg="parse incomplete: " ++ rest) 67 - throw(Unreachable("")) 214 + throw(Util.Unreachable("")) 68 215 } 69 216 | Error(msg) => { 70 217 t->fail(~msg="parse failed: " ++ msg) 71 - throw(Unreachable("")) 218 + throw(Util.Unreachable("")) 72 219 } 73 220 } 74 221 }

Configure Feed

Configure Feed