Something went wrong. Try again.
the next generation of the in-browser educational proof assistant
Something went wrong. Try again.
2.4 kB · 75 lines
at main
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475open Signaturesmodule Make = (Term: TERM, Judgment : REWRITABLE_JUDGMENT with module Term := Term) => { module Context = Method.Context(Term, Judgment) module Method = Rewrite.Make(Term, Judgment)
type props<'a> = { method: Method.t<'a>, ctx: Context.t, ruleStyle: RuleView.style, grammar: Term.grammar, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => unit, }
type srProps<'a> = { "proof": 'a, "ctx": Context.t, "ruleStyle": RuleView.style, "grammar": Term.grammar, "gen": Term.gen, "onChange": ('a, Term.subst) => unit, } let summary = props => <span className="rule-rulename-rewrite"> <MethodView.RuleRefView ruleRef=props.method.ruleName assms=props.ctx.localFactNames /> <sup>{ switch props.method.direction { | Method.Forward => React.string("→") | Method.Backward => React.string("←") } }</sup> </span> let make = (subRender: srProps<'a> => React.element) => props => { <div> <span className="typcn typcn-media-play"></span>{summary(props)} { if props.method.subgoals->Array.length > 0 { <ul className="subgoals"> {props.method.subgoals ->Array.mapWithIndex((sg, i) => { <li key={String.make(i)}> {React.createElement( subRender, { "proof": sg, "ctx": props.ctx, "ruleStyle": props.ruleStyle, "grammar": props.grammar, "gen": props.gen, "onChange": (newa, subst: Term.subst) => props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst), }, )} </li> }) ->React.array} </ul> } else { React.string("") } } <div className="proof-denest"> {React.createElement(subRender,{ "proof": props.method.newGoal, "ctx": props.ctx, "ruleStyle": props.ruleStyle, "grammar": props.grammar, "gen": props.gen, "onChange": (newa, subst: Term.subst) => props.onChange(props.method->Method.updateGoal(_=>newa), subst), })} </div> </div> }}