Something went wrong. Try again.
the next generation of the in-browser educational proof assistant
Something went wrong. Try again.
9.1 kB · 291 lines
at main
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292open Signaturesopen Methodmodule type METHOD_VIEW = { module Term: TERM module Judgment: JUDGMENT with module Term := Term module Method: PROOF_METHOD with module Term := Term and module Judgment := Judgment type props<'a> = { method: Method.t<'a>, ctx:Method.Context.t, ruleStyle: RuleView.style, grammar: Term.grammar, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => unit, } type srProps<'a> = { "proof": 'a, "ctx": Method.Context.t, "ruleStyle": RuleView.style, "grammar": Term.grammar, "gen": Term.gen, "onChange": ('a, Term.subst) => unit, } let make: (srProps<'a> => React.element) => props<'a> => React.element let summary: props<'a> => React.element}
module RuleRefView = {
@react.component let make = (~assms: array<string>, ~ruleRef: RuleRef.t) => { switch ruleRef { | Local({index}) => switch assms[index] { | None => <span className="rule-ref rule-ref--invalid"> {React.string(`#${Belt.Int.toString(index)}`)} </span> | Some(name) => let lastIndexWithName = assms->Belt.Array.reduceWithIndex(-1, (acc, n, i) => n == name ? i : acc ) let shadowed = lastIndexWithName != index if shadowed { <span className="rule-ref rule-rulename-local rule-ref-shadowed"> {React.string(name)} <span className="rule-ref__index"> {React.string(`@${Belt.Int.toString(index)}`)} </span> </span> } else { <span className="rule-ref rule-rulename-local"> <IdentifierView identifier=name /> </span> } } | Global({name}) => let shadowedByLocal = assms->Belt.Array.some(n => n == name) if shadowedByLocal { <span className="rule-ref rule-rulename-global rule-ref--shadowed"> {React.string(name)} </span> } else { <span className="rule-ref rule-rulename-global"> <IdentifierView identifier=name /> </span> } } }}
module DerivationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { module Method = Derivation(Term, Judgment) type props<'a> = { method: Method.t<'a>, ctx: Method.Context.t, ruleStyle: RuleView.style, grammar: Term.grammar, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => unit, } type srProps<'a> = { "proof": 'a, "ctx": Method.Context.t, "ruleStyle": RuleView.style, "grammar": Term.grammar, "gen": Term.gen, "onChange": ('a, Term.subst) => unit, } let summary = props => <RuleRefView ruleRef=props.method.ruleName assms=props.ctx.localFactNames /> 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.setSubproof(i, newa), subst), }, )} </li> }) ->React.array} </ul> } else { React.null } } </div> }}
module EliminationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { module Method = Elimination(Term, Judgment) type props<'a> = { method: Method.t<'a>, ctx: Method.Context.t, ruleStyle: RuleView.style, grammar: Term.grammar, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => unit, } type srProps<'a> = { "proof": 'a, "ctx": Method.Context.t, "ruleStyle": RuleView.style, "grammar": Term.grammar, "gen": Term.gen, "onChange": ('a, Term.subst) => unit, } let summary = props => <> <span className="rule-rulename-elim"> <RuleRefView ruleRef=props.method.ruleName assms=props.ctx.localFactNames /> </span> <sup> <RuleRefView ruleRef=props.method.elimName assms=props.ctx.localFactNames /> </sup> </> 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.setSubproof(i, newa), subst), }, )} </li> }) ->React.array} </ul> } else { React.null } } </div> }}
module LemmaView = ( Term: TERM, Judgment: JUDGMENT with module Term := Term, JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment,) => { module Method = Lemma(Term, Judgment) type props<'a> = { method: Method.t<'a>, ctx: Method.Context.t, ruleStyle: RuleView.style, grammar: Term.grammar, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => unit, } type srProps<'a> = { "proof": 'a, "ctx": Method.Context.t, "ruleStyle": RuleView.style, "grammar": Term.grammar, "gen": Term.gen, "onChange": ('a, Term.subst) => unit, } let summary = props => <span>{React.string("lemma")}</span> module RuleView = RuleView.Make(Term, Judgment, JudgmentView) let make = (subRender: srProps<'a> => React.element) => props => { <div> <b> {React.string("have ")} </b> <RuleView rule={props.method.rule} scope={props.ctx.fixes} grammar={props.grammar} style={props.ruleStyle}> {React.null} </RuleView> {React.createElement( subRender, { "proof": props.method.proof, "ctx": props.ctx, "ruleStyle": props.ruleStyle, "grammar": props.grammar, "gen": props.gen, "onChange": (proof, subst) => {props.onChange({...props.method, proof}, subst)}, }, )} {React.createElement( subRender, { "proof": props.method.show, "ctx": props.ctx, "ruleStyle": props.ruleStyle, "grammar": props.grammar, "gen": props.gen, "onChange": (show, subst) => {props.onChange({...props.method, show}, subst)}, }, )} </div> }}
module CombineMethodView = ( Term: TERM, Judgment: JUDGMENT with module Term := Term, Method1View: METHOD_VIEW with module Term := Term and module Judgment := Judgment, Method2View: METHOD_VIEW with module Term := Term and module Judgment := Judgment and type srProps<'a> = Method1View.srProps<'a>,) => { module Method = Combine(Term, Judgment, Method1View.Method, Method2View.Method) type props<'a> = { method: Method.t<'a>, ctx: Method.Context.t, ruleStyle: RuleView.style, grammar: Term.grammar, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => unit, } type srProps<'a> = Method1View.srProps<'a> let summary = props => switch props.method { | First(m) => Method1View.summary({ method: m, ctx: props.ctx, ruleStyle: props.ruleStyle, grammar: props.grammar, gen: props.gen, onChange: (n, s) => props.onChange(First(n), s), }) | Second(m) => Method2View.summary({ method: m, ctx: props.ctx, ruleStyle: props.ruleStyle, grammar: props.grammar, gen: props.gen, onChange: (n, s) => props.onChange(Second(n), s), }) } let make = (subrender: srProps<'a> => React.element) => props => { switch props.method { | First(m) => Method1View.make(subrender)({ method: m, ctx: props.ctx, ruleStyle: props.ruleStyle, grammar: props.grammar, gen: props.gen, onChange: (n, s) => props.onChange(First(n), s), }) | Second(m) => Method2View.make(subrender)({ method: m, ctx: props.ctx, ruleStyle: props.ruleStyle, grammar: props.grammar, gen: props.gen, onChange: (n, s) => props.onChange(Second(n), s), }) } }}