+7 -6

src/HOTermMethod.res

reviewed

··· 11 11 module Term = HOTerm 12 12 module Rule = Rule.Make(HOTerm, Judgment) 13 13 module Context = Context(HOTerm, Judgment) 14 14 - 14 14 + module Results = MethodResults(HOTerm) 15 15 + 15 16 let extractEqualityTermsFromJudgment = (judgment: Judgment.t): option<(HOTerm.t, HOTerm.t)> => { 16 17 let term: HOTerm.t = judgment 17 18 switch HOTerm.strip(term) { ··· 201 202 } 202 203 }) 203 204 204 204 - ret 205 205 + ret->Dict.toArray->Array.map(((s,(a,b))) => Results.Action(s,a,b)) 205 206 } 206 207 207 208 let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, f: ('a, Rule.t) => 'b) => { ··· 269 270 module Term = HOTerm 270 271 module Rule = Rule.Make(HOTerm, Judgment) 271 272 module Context = Context(HOTerm, Judgment) 272 272 - 273 273 + module Results = MethodResults(HOTerm) 273 274 type t<'a> = unit 274 275 275 276 type constructorHead = {name: string, args: array<HOTerm.t>} ··· 336 337 ret->Dict.set(`constructor_neq ${lhs} ${rhs}`, ((), HOTerm.makeSubst())) 337 338 | _ => () 338 339 } 339 339 - ret 340 340 + ret->Dict.toArray->Array.map(((s,(a,b))) => Results.Action(s,a,b)) 340 341 } 341 342 342 343 let check = (_it: t<'a>, _ctx: Context.t, goal: Judgment.t, _f: ('a, Rule.t) => 'b) => ··· 354 355 module ConstructorInj = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => { 355 356 module Rule = Rule.Make(HOTerm, Judgment) 356 357 module Context = Context(HOTerm, Judgment) 357 357 - 358 358 + module Results = MethodResults(HOTerm) 358 359 // we need to define this to workaround a type error for map 359 360 type inner = { 360 361 source: string, ··· 445 446 }) 446 447 | _ => () 447 448 } 448 448 - ret 449 449 + ret->Dict.toArray->Array.map(((s,(a,b))) => Results.Action(s,a,b)) 449 450 } 450 451 451 452 let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, _f: ('a, Rule.t) => 'b) => {

+63 -33

src/Method.res

reviewed

··· 9 9 let facts = t => t.localFacts->Dict.copy->Dict.assign(t.globalFacts) 10 10 } 11 11 12 12 + module MethodResults = (Term : TERM) => { 13 13 + 14 14 + // Currently all three options produce a button 15 15 + // with both Group and Delay producing sub-menus 16 16 + // I may change Group in future to just present 17 17 + // a boxed group of buttons without nesting it in sub-menus. 18 18 + // So use Delay() if sub-menus is what you actually want. 19 19 + type rec t<'a> = Action(string, 'a, Term.subst) 20 20 + | Delay(string, () => array<t<'a>>) 21 21 + | Group(string, array<t<'a>>) 22 22 + 23 23 + 24 24 + 25 25 + let rec map = (x: t<'a>, f: 'a => 'b ) => 26 26 + switch x { 27 27 + | Action(str, a, sub) => Action(str,f(a), sub) 28 28 + | Delay(str, g) => Delay(str, () => g(())->Array.map(x => x->map(f))) 29 29 + | Group(str, gs) => Group(str, gs->Array.map(x => x->map(f))) 30 30 + } 31 31 + } 32 32 + 33 33 + 34 34 + 12 35 module type PROOF_METHOD = { 13 36 module Term: TERM 14 37 module Judgment: JUDGMENT with module Term := Term 15 38 module Rule: module type of Rule.Make(Term, Judgment) 16 39 module Context: module type of Context(Term, Judgment) 40 40 + module Results: module type of MethodResults(Term) 17 41 type t<'a> 18 42 let keywords: array<string> 19 43 let substitute: (t<'a>, Term.subst) => t<'a> 20 44 let check: (t<'a>, Context.t, Judgment.t, ('a, Rule.t) => 'b) => result<t<'b>, string> 21 21 - let apply: (Context.t, Judgment.t, Term.gen, Rule.t => 'a) => Dict.t<(t<'a>, Term.subst)> 45 45 + let apply: (Context.t, Judgment.t, Term.gen, Rule.t => 'a) => array<Results.t<t<'a>>> 22 46 let map: (t<'a>, 'a => 'b) => t<'b> 23 47 let parse: ( 24 48 string, ··· 41 65 module Derivation = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 42 66 module Rule = Rule.Make(Term, Judgment) 43 67 module Context = Context(Term, Judgment) 68 68 + module Results = MethodResults(Term) 44 69 type t<'a> = { 45 70 ruleName: string, 46 71 instantiation: array<Term.t>, ··· 166 191 ret->Dict.set("intro " ++ key, (new, subst)) 167 192 }) 168 193 }) 169 169 - ret 194 194 + ret->Dict.toArray->Array.map(((key, (new, subst))) => Results.Action(key,new,subst)) 170 195 } 171 196 let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => { 172 197 switch ctx->Context.facts->Dict.get(it.ruleName) { ··· 208 233 module Elimination = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 209 234 module Rule = Rule.Make(Term, Judgment) 210 235 module Context = Context(Term, Judgment) 236 236 + module Results = MethodResults(Term) 211 237 type t<'a> = { 212 238 ruleName: string, 213 239 elimName: string, ··· 360 386 } 361 387 362 388 let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => { 363 363 - let ret = Dict.make() 364 389 let possibleRules = 365 390 ctx.globalFacts 366 391 ->Dict.toArray ··· 374 399 ctx.localFacts 375 400 ->Dict.toArray 376 401 ->Array.filter(((_, r)) => r.premises->Array.length == 0 && r.vars->Array.length == 0) 377 377 - possibleRules->Array.forEach(((ruleName, rule)) => { 378 378 - possibleElims->Array.forEach(((elimName, elim)) => { 379 379 - let ruleInsts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes) 380 380 - let rule' = rule->Rule.instantiate(ruleInsts) 381 381 - Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion, ~gen) 382 382 - ->Seq.take(seqSizeLimit) 383 383 - ->Seq.forEach( 384 384 - elimSub => { 385 385 - let rule'' = rule'->Rule.substituteBare(elimSub) 386 386 - Judgment.unify(rule''.conclusion, j, ~gen) 387 387 - ->Seq.take(seqSizeLimit) 388 388 - ->Seq.forEach( 389 389 - ruleSub => { 390 390 - let new = { 391 391 - ruleName, 392 392 - elimName, 393 393 - instantiation: ruleInsts, 394 394 - subgoals: rule.premises->Array.sliceToEnd(~start=1)->Array.map(f), 395 395 - } 396 396 - let subst = Term.mergeSubsts(elimSub, ruleSub) 397 397 - ret->Dict.set(`elim ${ruleName} with ${elimName}`, (new, subst)) 398 398 - }, 399 399 - ) 400 400 - }, 401 401 - ) 402 402 + possibleElims->Array.map(((elimName, elim)) => { 403 403 + Results.Delay("elim " + elimName,() => { 404 404 + let subtree = [] 405 405 + possibleRules->Array.forEach(((ruleName, rule)) => { 406 406 + let ruleInsts = rule->Rule.genSchemaInsts(gen, ~scope=ctx.fixes) 407 407 + let rule' = rule->Rule.instantiate(ruleInsts) 408 408 + Judgment.unify((rule'.premises[0]->Option.getExn).conclusion, elim.conclusion, ~gen) 409 409 + ->Seq.take(seqSizeLimit) 410 410 + ->Seq.forEach( 411 411 + elimSub => { 412 412 + let rule'' = rule'->Rule.substituteBare(elimSub) 413 413 + Judgment.unify(rule''.conclusion, j, ~gen) 414 414 + ->Seq.take(seqSizeLimit) 415 415 + ->Seq.forEach( 416 416 + ruleSub => { 417 417 + let new = { 418 418 + ruleName, 419 419 + elimName, 420 420 + instantiation: ruleInsts, 421 421 + subgoals: rule.premises->Array.sliceToEnd(~start=1)->Array.map(f), 422 422 + } 423 423 + let subst = Term.mergeSubsts(elimSub, ruleSub) 424 424 + subtree->Array.push(Results.Action("with " ++ ruleName, new, subst)) 425 425 + }, 426 426 + ) 427 427 + }, 428 428 + ) 429 429 + }) 430 430 + subtree 402 431 }) 403 432 }) 404 404 - ret 405 433 } 406 434 } 407 435 408 436 module Lemma = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { 409 437 module Rule = Rule.Make(Term, Judgment) 410 438 module Context = Context(Term, Judgment) 439 439 + module Results = MethodResults(Term) 411 440 type t<'a> = { 412 441 rule: Rule.t, 413 442 proof: 'a, ··· 457 486 } 458 487 } 459 488 let apply = (_ctx: Context.t, _j: Judgment.t, _gen: Term.gen, _f: Rule.t => 'a) => { 460 460 - Dict.make() 489 489 + [] 461 490 } 462 491 let check = (it: t<'a>, _ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => { 463 492 let first = f(it.proof, it.rule) ··· 473 502 ) => { 474 503 module Rule = Rule.Make(Term, Judgment) 475 504 module Context = Context(Term, Judgment) 505 505 + module Results = MethodResults(Term) 476 506 type t<'a> = First(Method1.t<'a>) | Second(Method2.t<'a>) 477 507 let map = (it, f) => 478 508 switch it { ··· 486 516 } 487 517 let keywords = Array.concat(Method1.keywords, Method2.keywords) 488 518 let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => { 489 489 - let d1 = Method1.apply(ctx, j, gen, f)->Dict.mapValues(((m, s)) => (First(m), s)) 490 490 - let d2 = Method2.apply(ctx, j, gen, f)->Dict.mapValues(((m, s)) => (Second(m), s)) 491 491 - d1->Dict.assign(d2) 519 519 + let d1 = Method1.apply(ctx, j, gen, f)->Array.map(me => me->Results.map(m => First(m))) 520 520 + Array.pushMany(d1,Method2.apply(ctx, j, gen, f)->Array.map(me => me->Results.map(m => Second(m)))) 521 521 + d1 492 522 } 493 523 let check = (it, ctx, j, f) => 494 524 switch it {

+2 -1

src/Proof.res

reviewed

··· 8 8 ) => { 9 9 module Rule = Rule.Make(Term, Judgment) 10 10 module Context = Context(Term, Judgment) 11 11 + module Results = MethodResults(Term) 11 12 type rec t = { 12 13 fixes: array<Term.meta>, 13 14 assumptions: array<string>, ··· 24 25 | ProofError({raw: t, rule: Rule.t, msg: string}) 25 26 and checked_option_method = 26 27 | Do(Method.t<checked>) 27 27 - | Goal(Term.gen => Dict.t<(Method.t<checked>, Term.subst)>) 28 28 + | Goal(Term.gen => array<Results.t<Method.t<checked>>>) 28 29 let parseKeyword = input => { 29 30 Method.keywords 30 31 ->Array.concat(["?"])

+72 -15

src/ProofView.res

reviewed

··· 13 13 module Rule = Rule.Make(Term, Judgment) 14 14 module ScopeView = ScopeView.Make(Term, JudgmentView.TermView) 15 15 module Proof = Proof.Make(Term, Judgment, MethodView.Method) 16 16 - 16 16 + module Results = Method.MethodResults(Term) 17 17 + module ResultsView = { 18 18 + type menuState<'a> = { 19 19 + history: list<array<Results.t<MethodView.Method.t<Proof.checked>>>>, // Stack of previous menus 20 20 + current: array<Results.t<MethodView.Method.t<Proof.checked>>>, // What is currently visible 21 21 + } 22 22 + type props = { 23 23 + initialNodes: array<Results.t<MethodView.Method.t<Proof.checked>>>, 24 24 + onApply: (MethodView.Method.t<Proof.checked>, Term.subst) => (), 25 25 + onBlur: (ReactEvent.Focus.t) => () 26 26 + } 27 27 + @react.componentWithProps 28 28 + let make = (props: props) => { 29 29 + let (state, setState) = React.useState(_ => { 30 30 + history: list{}, 31 31 + current: props.initialNodes, 32 32 + }) 33 33 + 34 34 + let goBack = _ => { 35 35 + setState(prev => { 36 36 + switch prev.history { 37 37 + | list{parent, ...rest} => {current: parent, history: rest} 38 38 + | list{} => prev // Already at the root 39 39 + } 40 40 + }) 41 41 + } 42 42 + 43 43 + let drillDown = (newNodes: array<Results.t<'a>>) => { 44 44 + setState(prev => { 45 45 + history: list{prev.current, ...prev.history}, 46 46 + current: newNodes, 47 47 + }) 48 48 + } 49 49 + 50 50 + <div className="drill-down-container"> 51 51 + {state.history != list{} 52 52 + ? <button tabIndex=0 onBlur={props.onBlur} onClick={goBack} className="back-button"> {React.string("← Back")} </button> 53 53 + : React.null} 54 54 + 55 55 + <div className="menu-options"> 56 56 + {state.current->Array.mapWithIndex((node, i) => { 57 57 + switch node { 58 58 + | Action(label, nextTree, subst) => 59 59 + <button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => props.onApply(nextTree, subst)}> 60 60 + {React.string(label ++ "")} 61 61 + </button> 62 62 + 63 63 + | Group(label, children) => 64 64 + <button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => drillDown(children)}> 65 65 + {React.string(label ++ " →")} 66 66 + </button> 67 67 + 68 68 + | Delay(label, getChildren) => 69 69 + <button tabIndex=0 onBlur={props.onBlur} key={label ++ i->Int.toString} onClick={_ => drillDown(getChildren())}> 70 70 + {React.string(label ++ " ...")} 71 71 + </button> 72 72 + } 73 73 + })->React.array} 74 74 + </div> 75 75 + </div> 76 76 + } 77 77 + } 78 78 + 79 79 + 17 80 type props = { 18 81 proof: Proof.checked, 19 82 scope: array<Term.meta>, ··· 55 118 let portal = switch sidebarRef.current->Nullable.toOption { 56 119 | None => React.null 57 120 | Some(node) => 58 58 - Portal.createPortal( 121 121 + let res = options(props.gen); 122 122 + Portal.createPortal( 59 123 <> 60 60 - {options(props.gen) 61 61 - ->Dict.toArray 62 62 - ->Array.map(((str, (opt, subst))) => { 63 63 - <button 64 64 - tabIndex=0 65 65 - onBlur 66 66 - key=str 67 67 - onClick={_ => 124 124 + { 125 125 + <ResultsView initialNodes=res 126 126 + onBlur 127 127 + onApply={(opt,subst)=> 68 128 props.onChange( 69 129 Proof.Checked({fixes, assumptions, method: Do(opt), rule}), 70 130 subst, 71 131 )} 72 72 - > 73 73 - {React.string(str)} 74 74 - </button> 75 75 - }) 76 76 - ->React.array} 132 132 + ></ResultsView> 133 133 + } 77 134 </>, 78 135 node, 79 136 )