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.

Merge pull request #15 from mio-19/main

equality

authored by

Liam O'Connor and committed by
GitHub 8f7759d5 3c5c7e50

+424 -25
+31 -2
index.html
··· 329 329 (P 0) 330 330 [k. (P k) |- (P (S (S k)))] 331 331 --------------------------- E-ind 332 - (P n) </hol-comp> 332 + (P n) 333 + 334 + a. 335 + ---- refl 336 + (= a a) 337 + 338 + a. b. f. 339 + (= a b) (f a) 340 + -------- eq-ap 341 + (f b) 342 + </hol-comp> 333 343 <hol-config id="index.html/myconfig">Gentzen</hol-config> 334 344 <hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz index.html/nat"> 335 345 a. 336 346 (Nat a) 337 347 ------- 338 348 (Nat (S (S a))) 349 + 350 + a. asm |- ? 351 + </hol-proof> 352 + 353 + <hol-proof id="index.html/prooftest2" deps="index.html/myconfig index.html/baz index.html/nat"> 354 + a. b. f. 355 + (= a b) 356 + ------- 357 + (= (f a) (f b)) 339 358 340 - a. asm |- ? 359 + a. b. f. asm |- ? 360 + </hol-proof> 361 + 362 + <hol-proof id="index.html/eq-trans" deps="index.html/myconfig index.html/baz index.html/nat"> 363 + a. b. c. 364 + (= a b) 365 + (= b c) 366 + ------- eq-trans 367 + (= a c) 368 + 369 + a. b. c. ab bc |- ? 341 370 </hol-proof> 342 371 <h1>String</h1> 343 372 <h2>Basic</h2>
+22 -1
package-lock.json
··· 8 8 "name": "holbert-ng", 9 9 "version": "0.0.0", 10 10 "dependencies": { 11 + "@jmagaram/rescript-seq": "^4.4.1", 11 12 "@rescript/react": "^0.13.1", 12 13 "react": "^19.1.0", 13 14 "react-dom": "^19.1.0", ··· 724 725 "url": "https://github.com/sponsors/nzakas" 725 726 } 726 727 }, 728 + "node_modules/@jmagaram/rescript-seq": { 729 + "version": "4.4.1", 730 + "resolved": "https://registry.npmjs.org/@jmagaram/rescript-seq/-/rescript-seq-4.4.1.tgz", 731 + "integrity": "sha512-+OdQX3csszdwMAqiVDiSkqGauq564KaxyvXH21oHPMCwD+Z8VdBxsH9t+XkpQ4wS14YbnEd13R4+Z/fg8pkawQ==", 732 + "license": "ISC", 733 + "dependencies": { 734 + "@rescript/core": "^1.1.0", 735 + "rescript": "^11.0.1" 736 + } 737 + }, 727 738 "node_modules/@nodelib/fs.scandir": { 728 739 "version": "2.1.5", 729 740 "resolved": "https://registry.npmjs.org/@nodelib/fs.scandir/-/fs.scandir-2.1.5.tgz", ··· 766 777 "version": "1.6.1", 767 778 "resolved": "https://registry.npmjs.org/@rescript/core/-/core-1.6.1.tgz", 768 779 "integrity": "sha512-vyb5k90ck+65Fgui+5vCja/mUfzKaK3kOPT4Z6aAJdHLH1eljEi1zKhXroCiCtpNLSWp8k4ulh1bdB5WS0hvqA==", 769 - "dev": true, 770 780 "license": "MIT", 771 781 "peerDependencies": { 772 782 "rescript": ">=11.1.0" ··· 1335 1345 "integrity": "sha512-AwAfQ2Wa5bCx9WP8nZL2uMZWod7J7/JSplxbTmBQ5ms6QpqNYm672H0Vu9ZVKVngQ+ii4R/byguVEUZQyeg44g==", 1336 1346 "dev": true, 1337 1347 "license": "MIT", 1348 + "peer": true, 1338 1349 "dependencies": { 1339 1350 "csstype": "^3.0.2" 1340 1351 } ··· 1395 1406 "integrity": "sha512-vxXJV1hVFx3IXz/oy2sICsJukaBrtDEQSBiV48/YIV5KWjX1dO+bcIr/kCPrW6weKXvsaGKFNlwH0v2eYdRRbA==", 1396 1407 "dev": true, 1397 1408 "license": "MIT", 1409 + "peer": true, 1398 1410 "dependencies": { 1399 1411 "@typescript-eslint/scope-manager": "8.34.0", 1400 1412 "@typescript-eslint/types": "8.34.0", ··· 1626 1638 "integrity": "sha512-NZyJarBfL7nWwIq+FDL6Zp/yHEhePMNnnJ0y3qfieCrmNvYct8uvtiV41UvlSe6apAfk0fY1FbWx+NwfmpvtTg==", 1627 1639 "dev": true, 1628 1640 "license": "MIT", 1641 + "peer": true, 1629 1642 "bin": { 1630 1643 "acorn": "bin/acorn" 1631 1644 }, ··· 2056 2069 "integrity": "sha512-ocgh41VhRlf9+fVpe7QKzwLj9c92fDiqOj8Y3Sd4/ZmVA4Btx4PlUYPq4pp9JDyupkf1upbEXecxL2mwNV7jPQ==", 2057 2070 "dev": true, 2058 2071 "license": "MIT", 2072 + "peer": true, 2059 2073 "dependencies": { 2060 2074 "@eslint-community/eslint-utils": "^4.2.0", 2061 2075 "@eslint-community/regexpp": "^4.12.1", ··· 3098 3112 "resolved": "https://registry.npmjs.org/react/-/react-19.1.0.tgz", 3099 3113 "integrity": "sha512-FS+XFBNvn3GTAWq26joslQgWNoFu08F4kl0J4CgdNKADkdSGXQyTCnKteIAJy96Br6YbpEU1LSzV5dYtjMkMDg==", 3100 3114 "license": "MIT", 3115 + "peer": true, 3101 3116 "engines": { 3102 3117 "node": ">=0.10.0" 3103 3118 } ··· 3107 3122 "resolved": "https://registry.npmjs.org/react-dom/-/react-dom-19.1.0.tgz", 3108 3123 "integrity": "sha512-Xs1hdnE+DyKgeHJeJznQmYMIBG3TKIHJJT95Q58nHLSrElKlGQqDTR2HQ9fx5CN/Gk6Vh/kupBTDLU11/nDk/g==", 3109 3124 "license": "MIT", 3125 + "peer": true, 3110 3126 "dependencies": { 3111 3127 "scheduler": "^0.26.0" 3112 3128 }, ··· 3133 3149 "integrity": "sha512-0bGU0bocihjSC6MsE3TMjHjY0EUpchyrREquLS8VsZ3ohSMD+VHUEwimEfB3kpBI1vYkw3UFZ3WD8R28guz/Vw==", 3134 3150 "hasInstallScript": true, 3135 3151 "license": "SEE LICENSE IN LICENSE", 3152 + "peer": true, 3136 3153 "bin": { 3137 3154 "bsc": "bsc", 3138 3155 "bstracing": "lib/bstracing", ··· 3473 3490 "integrity": "sha512-M7BAV6Rlcy5u+m6oPhAPFgJTzAioX/6B0DxyvDlo9l8+T3nLKbrczg2WLUyzd45L8RqfUMyGPzekbMvX2Ldkwg==", 3474 3491 "dev": true, 3475 3492 "license": "MIT", 3493 + "peer": true, 3476 3494 "engines": { 3477 3495 "node": ">=12" 3478 3496 }, ··· 3535 3553 "integrity": "sha512-p1diW6TqL9L07nNxvRMM7hMMw4c5XOo/1ibL4aAIGmSAt9slTE1Xgw5KWuof2uTOvCg9BY7ZRi+GaF+7sfgPeQ==", 3536 3554 "dev": true, 3537 3555 "license": "Apache-2.0", 3556 + "peer": true, 3538 3557 "bin": { 3539 3558 "tsc": "bin/tsc", 3540 3559 "tsserver": "bin/tsserver" ··· 3595 3614 "integrity": "sha512-0msEVHJEScQbhkbVTb/4iHZdJ6SXp/AvxL2sjwYQFfBqleHtnCqv1J3sa9zbWz/6kW1m9Tfzn92vW+kZ1WV6QA==", 3596 3615 "dev": true, 3597 3616 "license": "MIT", 3617 + "peer": true, 3598 3618 "dependencies": { 3599 3619 "esbuild": "^0.25.0", 3600 3620 "fdir": "^6.4.4", ··· 3685 3705 "integrity": "sha512-M7BAV6Rlcy5u+m6oPhAPFgJTzAioX/6B0DxyvDlo9l8+T3nLKbrczg2WLUyzd45L8RqfUMyGPzekbMvX2Ldkwg==", 3686 3706 "dev": true, 3687 3707 "license": "MIT", 3708 + "peer": true, 3688 3709 "engines": { 3689 3710 "node": ">=12" 3690 3711 },
+1 -1
src/HOTerm.res
··· 155 155 switch term { 156 156 | App({func, arg}) => 157 157 App({func: discharge(subst, func, ~prune), arg: discharge(subst, arg, ~prune)}) 158 - // Lam case is not actually needed by FCU 158 + // Lam case is not actually needed by FCU but needed by rewriting 159 159 | Lam({name, body}) => Lam({name, body: discharge(upshift_tt(subst), body, ~prune)}) 160 160 | Var(_) if prune => Unallowed 161 161 | Var(_) | Schematic(_) | Symbol(_) | Unallowed => term
+2
src/HOTerm.resi
··· 22 22 let substAdd: (subst, schematic, t) => subst 23 23 let unifyTerm: (t, t, subst, ~gen: option<gen>) => subst 24 24 let reduceSubst: subst => subst 25 + let discharge: (array<(t, t)>, t, ~prune: bool) => t 26 + let upshift_tt: (array<(t, t)>, ~amount: int=?) => array<(t, t)>
+24 -11
src/HOTermView.res
··· 1 - type props = {term: HOTerm.t, scope: array<string>} 2 1 open Util 3 2 type idx_props = {idx: int, scope: array<string>} 4 3 let viewVar = (props: idx_props) => ··· 33 32 [React.string(" "), e] 34 33 } 35 34 ) 36 - 35 + type props1 = {term: HOTerm.t, scope: array<string>, brackets: bool} 37 36 @react.componentWithProps 38 - let rec make = ({term, scope}) => 37 + let rec make1 = ({term, scope, brackets}) => 39 38 switch term { 40 39 | Var({idx}) => viewVar({idx, scope}) 41 40 | Symbol({name: s}) => <span className="term-const"> {React.string(s)} </span> ··· 46 45 </span> 47 46 | App(_) => 48 47 switch HOTerm.strip(term) { 48 + | (Symbol({name: "="}), args) if Array.length(args) == 2 => 49 + <span className="term-equality"> 50 + {React.createElement(make1, {term: args->Array.getUnsafe(0), scope, brackets: true})} 51 + {React.string("=")} 52 + {React.createElement(make1, {term: args->Array.getUnsafe(1), scope, brackets: true})} 53 + </span> 49 54 | (func, args) => 50 - <span className="term-app"> 51 - {React.createElement(make, {term: func, scope})} 52 - <span className="term-app-telescope"> 53 - {args 54 - ->Array.mapWithIndex((t, i) => React.createElement(make, withKey({term: t, scope}, i))) 55 + let xs = Array.concat([func], args) 56 + let a = 57 + <span className="term-app"> 58 + {xs 59 + ->Array.mapWithIndex((t, i) => 60 + React.createElement(make1, withKey({term: t, scope, brackets: true}, i)) 61 + ) 55 62 ->intersperse 56 - ->parenthesise 57 63 ->React.array} 58 64 </span> 59 - </span> 65 + if brackets { 66 + [a]->parenthesise->React.array 67 + } else { 68 + a 69 + } 60 70 } 61 71 | Lam({name, body}) => { 62 72 let newScope = Array.concat([name], scope) 63 73 <span className="term-lambda"> 64 74 {React.string(name)} 65 - {React.createElement(make, {term: body, scope: newScope})} 75 + {React.createElement(make1, {term: body, scope: newScope, brackets: false})} 66 76 </span> 67 77 } 68 78 | Unallowed => <p> {React.string("Internal error: unallowed")} </p> 69 79 } 80 + type props = {term: HOTerm.t, scope: array<string>} 81 + @react.componentWithProps 82 + let make = ({term, scope}) => make1({term, scope, brackets: false})
+49 -4
src/InductiveSet.res
··· 177 177 allGroups->Array.filter(g => Belt.Set.has(reachableKeys, makeKey(g.name, g.arity))) 178 178 } 179 179 180 + let generateCasesRule = (group: constructorGroup): Rule.t => { 181 + let {name: str, arity: _i} = group 182 + 183 + let caseSubgoal = ((_constructorName: string, constructorRule: Rule.t)): Rule.t => { 184 + let offset = Array.length(constructorRule.vars) 185 + 186 + let equalityPremise = { 187 + Rule.vars: [], 188 + premises: [], 189 + conclusion: HOTerm.app( 190 + HOTerm.Symbol({name: "="}), 191 + [HOTerm.Var({idx: offset}), constructorRule.conclusion], 192 + ), 193 + } 194 + 195 + { 196 + Rule.vars: constructorRule.vars, 197 + premises: Array.concat([equalityPremise], constructorRule.premises), 198 + conclusion: HOTerm.Var({idx: offset + 1}), 199 + } 200 + } 201 + 202 + let subgoals = Array.map(group.rules, ((name, rule)) => caseSubgoal((name, rule))) 203 + 204 + { 205 + Rule.vars: Array.concat(["§0"], ["§P"]), 206 + premises: [ 207 + { 208 + Rule.vars: [], 209 + premises: [], 210 + conclusion: HOTerm.app(HOTerm.Symbol({name: str}), [HOTerm.Var({idx: 0})]), 211 + }, 212 + ...subgoals, 213 + ], 214 + conclusion: HOTerm.Var({idx: 1}), 215 + } 216 + } 217 + 180 218 let derived = (state: state): state => 181 219 state 182 220 ->groupByConstructor 183 - ->Array.map(group => { 221 + ->Array.flatMap(group => { 184 222 let mutualComponent = findMutuallyInductiveComponent(group, groupByConstructor(state)) 185 - let rule = generateInductionRule(group, mutualComponent) 186 - ("§induction-" ++ makeKey(group.name, group.arity), rule) 223 + let inductionRule = generateInductionRule(group, mutualComponent) 224 + let casesRule = generateCasesRule(group) 225 + [ 226 + ("§induction-" ++ makeKey(group.name, group.arity), inductionRule), 227 + ("§cases-" ++ makeKey(group.name, group.arity), casesRule), 228 + ] 187 229 }) 188 230 ->Dict.fromArray 189 231 let serialise = (state: state) => ··· 217 259 } 218 260 } 219 261 } 220 - ret.contents->Result.map(state => (state, {Ports.facts: state->Dict.copy->Dict.assign(derived(state)), ruleStyle: None})) 262 + ret.contents->Result.map(state => ( 263 + state, 264 + {Ports.facts: state->Dict.copy->Dict.assign(derived(state)), ruleStyle: None}, 265 + )) 221 266 } 222 267 223 268 let make = props => {
+181 -1
src/Method.res
··· 184 184 } 185 185 let updateAtKey = (it: t<'a>, key: int, f: 'a => 'a) => { 186 186 let newsgs = it.subgoals->Array.copy 187 - newsgs->Array.set(key, f(newsgs[key]->Option.getExn)) 187 + newsgs->Array.set(key, f(newsgs[key]->Option.getExn)) 188 188 {...it, subgoals: newsgs} 189 189 } 190 190 } ··· 489 489 } 490 490 } 491 491 } 492 + 493 + module MakeRewriteHOTerm = ( 494 + Judgment: JUDGMENT with module Term := HOTerm, 495 + Config: { 496 + let keyword: string 497 + let reversed: bool 498 + }, 499 + ) => { 500 + module Term = HOTerm 501 + module Rule = Rule.Make(HOTerm, Judgment) 502 + module Context = Context(HOTerm, Judgment) 503 + 504 + let isEqualityRule = (rule: Rule.t): bool => { 505 + Array.length(rule.vars) == 0 && Array.length(rule.premises) == 0 506 + } 507 + 508 + let extractEqualityTerms = (judgment: Judgment.t): option<(HOTerm.t, HOTerm.t)> => { 509 + let term: HOTerm.t = Obj.magic(judgment) 510 + switch HOTerm.strip(term) { 511 + | (HOTerm.Symbol({name: "="}), args) if Array.length(args) == 2 => 512 + Some((args->Array.getUnsafe(0), args->Array.getUnsafe(1))) 513 + | _ => None 514 + } 515 + } 516 + 517 + type t<'a> = { 518 + equalityName: string, 519 + subgoal: 'a, 520 + } 521 + 522 + let keywords = [Config.keyword] 523 + 524 + let map = (it: t<'a>, f) => { 525 + { 526 + equalityName: it.equalityName, 527 + subgoal: f(it.subgoal), 528 + } 529 + } 530 + 531 + let substitute = (it: t<'a>, _subst: Judgment.subst) => { 532 + // Rewrite method itself doesn't contain terms that need substitution 533 + it 534 + } 535 + 536 + let prettyPrint = ( 537 + it: t<'a>, 538 + ~scope, 539 + ~indentation=0, 540 + ~subprinter: ('a, ~scope: array<HOTerm.meta>, ~indentation: int=?) => string, 541 + ) => { 542 + let ind = String.repeat(" ", indentation) 543 + `${ind}${Config.keyword} ${it.equalityName} {\n` 544 + ->String.concat(subprinter(it.subgoal, ~scope, ~indentation=indentation + 2)) 545 + ->String.concat("\n") 546 + ->String.concat(ind) 547 + ->String.concat("}") 548 + } 549 + 550 + exception InternalParseError(string) 551 + 552 + let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => { 553 + let cur = ref(String.trim(input)) 554 + 555 + switch Rule.parseRuleName(cur.contents) { 556 + | Error(e) => Error(e) 557 + | Ok((equalityName, rest)) => { 558 + cur := String.trim(rest) 559 + 560 + if cur.contents->String.get(0) == Some("{") { 561 + cur := String.trim(String.sliceToEnd(cur.contents, ~start=1)) 562 + 563 + try { 564 + switch subparser(cur.contents, ~scope, ~gen) { 565 + | Error(e) => raise(InternalParseError(e)) 566 + | Ok((subgoal, rest2)) => { 567 + cur := String.trim(rest2) 568 + 569 + if cur.contents->String.get(0) == Some("}") { 570 + cur := String.trim(String.sliceToEnd(cur.contents, ~start=1)) 571 + Ok(({equalityName, subgoal}, cur.contents)) 572 + } else { 573 + Error("Expected } after subgoal") 574 + } 575 + } 576 + } 577 + } catch { 578 + | InternalParseError(e) => Error(e) 579 + } 580 + } else { 581 + Error("Expected { after equality name") 582 + } 583 + } 584 + } 585 + } 586 + 587 + let rewriteJudgmentTerms = (judgment: Judgment.t, from: HOTerm.t, to: HOTerm.t): Judgment.t => { 588 + Judgment.mapTerms(judgment, term => HOTerm.discharge([(from, to)], term, ~prune=false)) 589 + } 590 + 591 + let apply = (ctx: Context.t, j: Judgment.t, _gen: HOTerm.gen, f: Rule.t => 'a) => { 592 + let ret = Dict.make() 593 + // For HOTermJ, Judgment.subst is the same as HOTerm.subst 594 + let emptySubst: Judgment.subst = Obj.magic(HOTerm.makeSubst()) 595 + 596 + ctx.facts->Dict.forEachWithKey((eqRule, name) => { 597 + if isEqualityRule(eqRule) { 598 + switch extractEqualityTerms(eqRule.conclusion) { 599 + | Some((lhs, rhs)) => { 600 + let (from, to) = if Config.reversed { 601 + (rhs, lhs) 602 + } else { 603 + (lhs, rhs) 604 + } 605 + 606 + let rewrittenGoal = rewriteJudgmentTerms(j, from, to) 607 + if !Judgment.equivalent(j, rewrittenGoal) { 608 + let method = { 609 + equalityName: name, 610 + subgoal: f(eqRule), 611 + } 612 + ret->Dict.set(`${Config.keyword} ${name}`, (method, emptySubst)) 613 + } 614 + } 615 + | None => () 616 + } 617 + } 618 + }) 619 + 620 + ret 621 + } 622 + 623 + let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, f: ('a, Rule.t) => 'b) => { 624 + switch ctx.facts->Dict.get(it.equalityName) { 625 + | None => Error(`Cannot find equality '${it.equalityName}'`) 626 + | Some(eqRule) if !isEqualityRule(eqRule) => 627 + Error(`'${it.equalityName}' is not a valid equality (has variables or premises)`) 628 + | Some(eqRule) => 629 + switch extractEqualityTerms(eqRule.conclusion) { 630 + | None => 631 + Error(`Cannot extract equality from '${it.equalityName}' - not in expected equality form`) 632 + | Some((lhs, rhs)) => { 633 + let (from, to) = if Config.reversed { 634 + (rhs, lhs) 635 + } else { 636 + (lhs, rhs) 637 + } 638 + 639 + let rewrittenGoal = rewriteJudgmentTerms(goal, from, to) 640 + 641 + let rewrittenRule: Rule.t = { 642 + vars: [], 643 + premises: [], 644 + conclusion: rewrittenGoal, 645 + } 646 + 647 + Ok({ 648 + equalityName: it.equalityName, 649 + subgoal: f(it.subgoal, rewrittenRule), 650 + }) 651 + } 652 + } 653 + } 654 + } 655 + } 656 + 657 + module Rewrite = (Judgment: JUDGMENT with module Term := HOTerm) => MakeRewriteHOTerm( 658 + Judgment, 659 + { 660 + let keyword = "rewrite" 661 + let reversed = false 662 + }, 663 + ) 664 + 665 + module RewriteReverse = (Judgment: JUDGMENT with module Term := HOTerm) => MakeRewriteHOTerm( 666 + Judgment, 667 + { 668 + let keyword = "rewrite_reverse" 669 + let reversed = true 670 + }, 671 + )
+79
src/MethodView.res
··· 157 157 </div> 158 158 } 159 159 } 160 + 161 + module RewriteView = (Judgment: JUDGMENT with module Term := HOTerm) => { 162 + module Method = Rewrite(Judgment) 163 + type props<'a> = { 164 + method: Method.t<'a>, 165 + scope: array<HOTerm.meta>, 166 + ruleStyle: RuleView.style, 167 + gen: HOTerm.gen, 168 + onChange: (Method.t<'a>, Judgment.subst) => unit, 169 + } 170 + type srProps<'a> = { 171 + "proof": 'a, 172 + "scope": array<HOTerm.meta>, 173 + "ruleStyle": RuleView.style, 174 + "gen": HOTerm.gen, 175 + "onChange": ('a, Judgment.subst) => unit, 176 + } 177 + let make = (subRender: srProps<'a> => React.element) => props => { 178 + <div> 179 + <b> {React.string("rewrite ")} </b> 180 + {React.string(props.method.equalityName)} 181 + <ul> 182 + <li> 183 + {React.createElement( 184 + subRender, 185 + { 186 + "proof": props.method.subgoal, 187 + "scope": props.scope, 188 + "ruleStyle": props.ruleStyle, 189 + "gen": props.gen, 190 + "onChange": (subgoal, subst: Judgment.subst) => 191 + props.onChange({...props.method, subgoal}, subst), 192 + }, 193 + )} 194 + </li> 195 + </ul> 196 + </div> 197 + } 198 + } 199 + 200 + module RewriteReverseView = (Judgment: JUDGMENT with module Term := HOTerm) => { 201 + module Method = RewriteReverse(Judgment) 202 + type props<'a> = { 203 + method: Method.t<'a>, 204 + scope: array<HOTerm.meta>, 205 + ruleStyle: RuleView.style, 206 + gen: HOTerm.gen, 207 + onChange: (Method.t<'a>, Judgment.subst) => unit, 208 + } 209 + type srProps<'a> = { 210 + "proof": 'a, 211 + "scope": array<HOTerm.meta>, 212 + "ruleStyle": RuleView.style, 213 + "gen": HOTerm.gen, 214 + "onChange": ('a, Judgment.subst) => unit, 215 + } 216 + let make = (subRender: srProps<'a> => React.element) => props => { 217 + <div> 218 + <b> {React.string("rewrite_reverse ")} </b> 219 + {React.string(props.method.equalityName)} 220 + <ul> 221 + <li> 222 + {React.createElement( 223 + subRender, 224 + { 225 + "proof": props.method.subgoal, 226 + "scope": props.scope, 227 + "ruleStyle": props.ruleStyle, 228 + "gen": props.gen, 229 + "onChange": (subgoal, subst: Judgment.subst) => 230 + props.onChange({...props.method, subgoal}, subst), 231 + }, 232 + )} 233 + </li> 234 + </ul> 235 + </div> 236 + } 237 + } 238 + 160 239 module CombineMethodView = ( 161 240 Term: TERM, 162 241 Judgment: JUDGMENT with module Term := Term,
+2 -1
src/Rule.res
··· 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 8 let rec substitute = (rule: t, subst: Judgment.subst) => { 9 - let subst' = subst->Judgment.mapSubst(v => v->Judgment.upshiftSubstCodom(Array.length(rule.vars))) 9 + let subst' = 10 + subst->Judgment.mapSubst(v => v->Judgment.upshiftSubstCodom(Array.length(rule.vars))) 10 11 { 11 12 vars: rule.vars, 12 13 premises: rule.premises->Array.map(premise => premise->substitute(subst')),
+21 -2
src/Scratch.res
··· 2 2 3 3 module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTermJ, HOTermJView)) 4 4 module InductiveS = Editable.TextArea(InductiveSet.Make(HOTerm, HOTermJ, HOTermJView)) 5 + 6 + module RewritesView = MethodView.CombineMethodView( 7 + HOTerm, 8 + HOTermJ, 9 + MethodView.RewriteView(HOTermJ), 10 + MethodView.RewriteReverseView(HOTermJ), 11 + ) 5 12 module DerivationsOrLemmasView = MethodView.CombineMethodView( 6 13 HOTerm, 7 14 HOTermJ, 8 15 MethodView.DerivationView(HOTerm, HOTermJ), 9 16 MethodView.LemmaView(HOTerm, HOTermJ, HOTermJView), 10 17 ) 11 - module TheoremS = Editable.TextArea( 12 - Theorem.Make(HOTerm, HOTermJ, HOTermJView, DerivationsOrLemmasView), 18 + module DLRView = MethodView.CombineMethodView( 19 + HOTerm, 20 + HOTermJ, 21 + DerivationsOrLemmasView, 22 + RewritesView, 23 + ) 24 + module DLREView = MethodView.CombineMethodView( 25 + HOTerm, 26 + HOTermJ, 27 + DLRView, 28 + MethodView.EliminationView(HOTerm, HOTermJ), 13 29 ) 30 + 31 + // Temporarily use DLRView (without Elimination) due to HOTerm unification bug 32 + module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTermJ, HOTermJView, DLRView)) 14 33 module ConfS = ConfigBlock.Make(HOTerm, HOTermJ) 15 34 16 35 module AxiomStr = Editable.TextArea(StringAxiomSet)
+2
src/Signatures.res
··· 44 44 let upshift: (t, int, ~from: int=?) => t 45 45 let upshiftSubstCodom: (substCodom, int, ~from: int=?) => substCodom 46 46 let placeSubstCodom: (schematic, ~scope: array<meta>) => substCodom 47 + // Map a function over all terms in the judgment 48 + let mapTerms: (t, Term.t => Term.t) => t 47 49 let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string> 48 50 let parseSubstCodom: ( 49 51 string,
+7
src/StringTermJudgment.res
··· 76 76 | SExpV(j) => SExpV(SExp.upshift(j, amount, ~from)) 77 77 } 78 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 + 79 86 let parse = (str: string, ~scope: array<StringTerm.meta>, ~gen=?) => { 80 87 StringTerm.parse(str, ~scope, ~gen?)->Result.flatMap(((t, str)) => 81 88 SExp.parse(str, ~scope)->Result.map(((j, str)) => ((t, j), str))
+1
src/TermAsJudgment.res
··· 8 8 let placeSubstCodom = Term.place 9 9 let upshiftSubstCodom = Term.upshift 10 10 let substituteSubstCodom = Term.substitute 11 + let mapTerms = (t: Term.t, f: Term.t => Term.t): Term.t => f(t) 11 12 } 12 13 13 14 module SExpJ = Make(SExp)
+2 -2
tests/HOTermTest.res
··· 313 313 t->testUnify(c, b, ~subst=emptySubst->substAdd(6, t->Util.parse("(x. S \\0)"))) 314 314 }) 315 315 t->block("tests from induction examples", t => { 316 - let r = ("((?0 \\0) (?1 \\0))") 317 - let g = ("(f \\0)") 316 + let r = "((?0 \\0) (?1 \\0))" 317 + let g = "(f \\0)" 318 318 // what it's currently doing: 319 319 // 0 := (x. y. f x) 320 320 // 1 := doesn't matter