liamoc.net / holbert-ng
the next generation of the in-browser educational proof assistant
1
fork

Configure Feed

Select the types of activity you want to include in your feed.

lots of fixes

Josh Brown 581be60b bed17e0b

+166 -130
+108 -119
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 468 + ---- paren 469 + ("( ) ( ( ) )" M) 486 470 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 501 - 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/string-rhs" deps="index.html/myconfig"> 550 - ---- Expr-e 551 - "e" (Expr e) 552 - 553 - s1. 554 - s2. e2. 555 - "$s2" (Expr e2) 556 - ------------- Stmt-Let 557 - "let $s1 = $s2" (Let (ID "$s1") e2) 558 - </hol-string> 559 - <hol-string id="index.html/mexp-induct" deps="index.html/myconfig"> 560 - s. p. 561 - "$s" M "" p [s1. "$s1" p |- "($s1)" p] [s1. s2. "$s1" p "$s2" p |- "$s1 $s2" p] 562 - ---------------------------------- M-Induct 563 - "$s" p 564 - </hol-string> 478 + <!-- <hol-string id="index.html/bool" deps="index.html/myconfig"> --> 479 + <!-- ------- T-Atom --> 480 + <!-- "T" Atom --> 481 + <!-- ------- F-Atom --> 482 + <!-- "F" Atom --> 483 + <!----> 484 + <!-- e. --> 485 + <!-- "$e" Atom --> 486 + <!-- --------- Atom-AE --> 487 + <!-- "$e" AE --> 488 + <!----> 489 + <!-- e1.e2. --> 490 + <!-- "$e1" Atom "$e2" AE --> 491 + <!-- -------------------- And --> 492 + <!-- "$e1 /\\ $e2" AE --> 493 + <!----> 494 + <!-- e. --> 495 + <!-- "$e" AE --> 496 + <!-- --------- AE-B --> 497 + <!-- "$e" B --> 498 + <!----> 499 + <!-- e1.e2. --> 500 + <!-- "$e1" AE "$e2" B --> 501 + <!-- ----------------- Or --> 502 + <!-- "$e1 \\/ $e2" B --> 503 + <!----> 504 + <!-- e. --> 505 + <!-- "$e" B --> 506 + <!-- ----------- Paren --> 507 + <!-- "($e)" Atom --> 508 + <!-- </hol-string> --> 509 + <!-- <hol-string-proof id="index.html/boolprooftest" deps="index.html/myconfig index.html/bool"> --> 510 + <!-- ------------- bool --> 511 + <!-- "T/\\(T\\/F)" AE --> 512 + <!-- |- by (And "T" "(T\\/F)") { --> 513 + <!-- |- by (T-Atom) {} --> 514 + <!-- |- by (Atom-AE "(T\\/F)") { --> 515 + <!-- |- by (Paren "T\\/F") { --> 516 + <!-- |- by (Or "T" "F") { --> 517 + <!-- |- by (Atom-AE "T") { --> 518 + <!-- |- by (T-Atom) {} --> 519 + <!-- } --> 520 + <!-- |- by (AE-B "F") { --> 521 + <!-- |- by (Atom-AE "F") { --> 522 + <!-- |- by (F-Atom) {} --> 523 + <!-- } --> 524 + <!-- } --> 525 + <!-- } --> 526 + <!-- } --> 527 + <!-- } --> 528 + <!-- } --> 529 + <!-- </hol-string-proof> --> 530 + <!-- <hol-string id="index.html/m-exp-parse" deps="index.html/myconfig"> --> 531 + <!-- ---- MParse-Empty --> 532 + <!-- "" (MP emp) --> 533 + <!----> 534 + <!-- s1. p1. --> 535 + <!-- "$s1" (MP p1) --> 536 + <!-- ------------- MParse-Surround --> 537 + <!-- "($s1)" (MP (p1)) --> 538 + <!----> 539 + <!-- s1. s2. p1. p2. --> 540 + <!-- "$s1" p1 --> 541 + <!-- "$s1" p2 --> 542 + <!-- ------------------- MParse-Juxtapose --> 543 + <!-- "$s1 $s2" (MP (p1 p2)) --> 544 + <!-- </hol-string> --> 545 + <!-- <hol-string id="index.html/string-rhs" deps="index.html/myconfig"> --> 546 + <!-- ---- Expr-e --> 547 + <!-- "e" (Expr e) --> 548 + <!----> 549 + <!-- s1. --> 550 + <!-- s2. e2. --> 551 + <!-- "$s2" (Expr e2) --> 552 + <!-- ------------- Stmt-Let --> 553 + <!-- "let $s1 = $s2" (Let (ID "$s1") e2) --> 554 + <!-- </hol-string> --> 565 555 <hol-string id="index.html/lexp" deps="index.html/myconfig"> 566 - s. "$s" L 556 + s. ("$s" L) 567 557 -----N-Surr 568 - "($s)" N 558 + ("($s)" N) 569 559 570 560 -----L-Empty 571 - "" L 561 + ("" L) 572 562 573 563 s1. s2. 574 - "$s1" N "$s2" L 564 + ("$s1" N) ("$s2" L) 575 565 -----L-Juxtapose 576 - "$s1 $s2" L 566 + ("$s1 $s2" L) 577 567 </hol-string> 578 - 579 - <hol-string-proof id="index.html/lexp-n" deps="index.html/myconfig index.html/mexp index.html/mexp-induct index.html/lexp"> 580 - s. "$s" N 568 + <hol-string-proof id="index.html/lexp-n" deps="index.html/lexp index.html/myconfig"> 569 + s. ("$s" N) 581 570 --------N-L 582 - "$s" L 571 + ("$s" L) 583 572 s. sn |- by (L-Juxtapose s "") { 584 573 |- by (sn) {} 585 574 |- by (L-Empty) {} 586 575 } 587 576 </hol-string-proof> 588 - <hol-string-proof id="index.html/lexp-juxt" deps="index.html/myconfig index.html/mexp index.html/mexp-induct index.html/lexp"> 589 - 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) 590 579 --------------------- lexp-juxt 591 - "$s1 $s2" L 580 + ("$s1 $s2" L) 592 581 s1. s2. s1L s2L |- ? 593 582 </hol-string-proof> 594 - <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"> 595 - 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) 596 585 ----------- mexp-lexp 597 - "$s" L 586 + ("$s" L) 598 587 s. sM |- ? 599 588 </hol-string-proof> 600 - <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"> 601 - 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) 602 591 ----------- mexp-lexp 603 - "$s" M 604 - s. sL |- elim (L_mutualInduct sL "" "$s" "" "M" "M") { 592 + ("$s" M) 593 + s. sL |- elim (L_mutualInduct sL "" "$s" "" M M) { 605 594 |- by (M-Empty) {} 606 595 s1.s2. 0 1 2 3 |- elim (M-Juxtapose 2 "$s1" "$s2") { 607 596 |- by (3) {}}
+10 -1
src/SExp.res
··· 8 8 Seq.empty 9 9 } 10 10 let prettyPrint = (name, ~scope as _: array<string>) => name 11 - let parse = (string, ~scope as _: array<string>, ~gen as _=?) => Ok((string, "")) 11 + let symbolRegex = /^([^\s()\[\]]+)/ 12 + let parse = (string, ~scope as _: array<string>, ~gen as _=?) => 13 + switch Util.execRe(symbolRegex, string) { 14 + | Some(([res], l)) => Ok((res, string->String.substringToEnd(~start=l))) 15 + | _ => Error("constant symbol parse error") 16 + } 12 17 let substitute = (name, _) => name 18 + let lowerVar = _ => "" 19 + let lowerSchematic = (_, _) => "" 20 + let ghost = "" 21 + let substDeBruijn = (name, _, ~from as _) => name 13 22 let constSymbol = name => Some(name) 14 23 } 15 24
+31 -9
src/SExpFunc.res
··· 5 5 let prettyPrint: (t, ~scope: array<string>) => string 6 6 let parse: (string, ~scope: array<string>, ~gen: ref<int>=?) => result<(t, string), string> 7 7 let substitute: (t, subst) => t 8 + // used for when trying to substitute a variable of the wrong type 9 + let lowerVar: int => t 10 + let lowerSchematic: (int, array<int>) => t 11 + let ghost: t 12 + let substDeBruijn: (t, array<t>, ~from: int) => t 8 13 // used for grouping judgments together for rule induction 9 14 let constSymbol: t => option<string> 10 15 } ··· 147 152 } 148 153 let unify = (a: t, b: t, ~gen as _=?) => unifyTerm(a, b) 149 154 155 + let rec lower = (term: t): Symbol.t => 156 + switch term { 157 + | Symbol(s) => s 158 + | Var({idx}) => Symbol.lowerVar(idx) 159 + | Schematic({schematic, allowed}) => Symbol.lowerSchematic(schematic, allowed) 160 + | Compound({subexps: [e1]}) => lower(e1) 161 + | _ => Symbol.ghost 162 + } 150 163 let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) => 151 164 switch term { 152 - | Symbol(_) => term 165 + | Symbol(s) => { 166 + let symbolSubsts = substs->Array.map(lower) 167 + Symbol(Symbol.substDeBruijn(s, symbolSubsts, ~from)) 168 + } 169 + 153 170 | Compound({subexps}) => 154 171 Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))}) 155 172 | Var({idx: var}) => ··· 295 312 | Some(res) => 296 313 switch RegExp.Result.matches(res) { 297 314 | [symb] => { 298 - cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp)) 299 - let parseSymb = () => { 315 + let specialSymb = tok => { 316 + cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp)) 317 + Some(tok) 318 + } 319 + let regularSymb = () => { 300 320 // FIX: not ideal to throw away symbol error message 301 - Symbol.parse(symb, ~scope) 321 + Console.log(("current", cur.contents)) 322 + Symbol.parse(cur.contents, ~scope) 302 323 ->Util.Result.ok 303 324 ->Option.map(((s, rest)) => { 304 - cur := rest->String.concat(cur.contents) 325 + cur := rest 326 + Console.log(("parsed", s, cur.contents)) 305 327 SymbolT(s) 306 328 }) 307 329 } 308 330 switch checkVariable(symb) { 309 - | Some(idx) => Some(VarT(idx)) 331 + | Some(idx) => specialSymb(VarT(idx)) 310 332 | None => { 311 333 let schematicRegexp = RegExp.fromString(schematicRegexpString) 312 334 switch schematicRegexp->RegExp.exec(symb) { 313 - | None => parseSymb() 335 + | None => regularSymb() 314 336 | Some(res') => 315 337 switch RegExp.Result.matches(res') { 316 - | [s] => Some(SchematicT(s->Int.fromString->Option.getUnsafe)) 317 - | _ => parseSymb() 338 + | [s] => specialSymb(SchematicT(s->Int.fromString->Option.getUnsafe)) 339 + | _ => regularSymb() 318 340 } 319 341 } 320 342 }
+17 -1
src/StringTermJudgment.res
··· 30 30 let stringSubs = subst->Util.mapMapValues(v => 31 31 switch v { 32 32 | StringS(s) => s 33 - | _ => throw(Util.Unreachable("const should not have map values")) 33 + | _ => [StringTerm.Ghost] 34 34 } 35 35 ) 36 36 StringS(StringTerm.substitute(s, stringSubs)) 37 + } 38 + | ConstS(s) => ConstS(s) 39 + } 40 + let lowerVar = idx => StringS([StringTerm.Var({idx: idx})]) 41 + let lowerSchematic = (schematic, allowed) => StringS([StringTerm.Schematic({schematic, allowed})]) 42 + let ghost = StringS([StringTerm.Ghost]) 43 + let substDeBruijn = (s, substs: array<t>, ~from) => 44 + switch s { 45 + | StringS(s) => { 46 + let stringSubs = substs->Array.map(v => 47 + switch v { 48 + | StringS(s) => s 49 + | _ => [StringTerm.String("AYAYAYSLKDJFLSKDJ")] 50 + } 51 + ) 52 + StringS(StringTerm.substDeBruijn(s, stringSubs, ~from)) 37 53 } 38 54 | ConstS(s) => ConstS(s) 39 55 }