Something went wrong. Try again.
the next generation of the in-browser educational proof assistant
Something went wrong. Try again.
10 kB · 348 lines
at main
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349open Signaturesopen Methodopen HOTermMethodmodule 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>, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => unit, } type srProps<'a> = { "proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style, "gen": Term.gen, "onChange": ('a, Term.subst) => unit, } let make: (srProps<'a> => React.element) => props<'a> => React.element}
module DerivationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { module Method = Derivation(Term, Judgment) type props<'a> = { method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => unit, } type srProps<'a> = { "proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style, "gen": Term.gen, "onChange": ('a, Term.subst) => unit, } let make = (subRender: srProps<'a> => React.element) => props => { <div> <b> {React.string("by ")} </b> {React.string(props.method.ruleName)} <ul> {props.method.subgoals ->Array.mapWithIndex((sg, i) => { <li key={String.make(i)}> {React.createElement( React.component(subRender), { "proof": sg, "scope": props.scope, "ruleStyle": props.ruleStyle, "gen": props.gen, "onChange": (newa, subst: Term.subst) => props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst), }, )} </li> }) ->React.array} </ul> </div> }}
module EliminationView = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { module Method = Elimination(Term, Judgment) type props<'a> = { method: Method.t<'a>, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => unit, } type srProps<'a> = { "proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style, "gen": Term.gen, "onChange": ('a, Term.subst) => unit, } let make = (subRender: srProps<'a> => React.element) => props => { <div> <b> {React.string("elim ")} </b> {React.string(`${props.method.ruleName} ${props.method.elimName}`)} <ul> {props.method.subgoals ->Array.mapWithIndex((sg, i) => { <li key={String.make(i)}> {React.createElement( React.component(subRender), { "proof": sg, "scope": props.scope, "ruleStyle": props.ruleStyle, "gen": props.gen, "onChange": (newa, subst: Term.subst) => props.onChange(props.method->Method.updateAtKey(i, _ => newa), subst), }, )} </li> }) ->React.array} </ul> </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>, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => unit, } type srProps<'a> = { "proof": 'a, "scope": array<Term.meta>, "ruleStyle": RuleView.style, "gen": Term.gen, "onChange": ('a, Term.subst) => unit, } 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.scope} style={props.ruleStyle}> {React.null} </RuleView> {React.createElement( React.component(subRender), { "proof": props.method.proof, "scope": props.scope, "ruleStyle": props.ruleStyle, "gen": props.gen, "onChange": (proof, subst) => {props.onChange({...props.method, proof}, subst)}, }, )} {React.createElement( React.component(subRender), { "proof": props.method.show, "scope": props.scope, "ruleStyle": props.ruleStyle, "gen": props.gen, "onChange": (show, subst) => {props.onChange({...props.method, show}, subst)}, }, )} </div> }}
module RewriteView = ( HOTerm: HOTerm.S, Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,) => { module Method = Rewrite(HOTerm, Judgment) type props<'a> = { method: Method.t<'a>, scope: array<HOTerm.meta>, ruleStyle: RuleView.style, gen: HOTerm.gen, onChange: (Method.t<'a>, HOTerm.subst) => unit, } type srProps<'a> = { "proof": 'a, "scope": array<HOTerm.meta>, "ruleStyle": RuleView.style, "gen": HOTerm.gen, "onChange": ('a, HOTerm.subst) => unit, } let make = (subRender: srProps<'a> => React.element) => props => { <div> <b> {React.string("rewrite ")} </b> {React.string(props.method.equalityName)} <ul> <li> {React.createElement( React.component(subRender), { "proof": props.method.subgoal, "scope": props.scope, "ruleStyle": props.ruleStyle, "gen": props.gen, "onChange": (subgoal, subst: HOTerm.subst) => props.onChange({...props.method, subgoal}, subst), }, )} </li> </ul> </div> }}
module RewriteReverseView = ( HOTerm: HOTerm.S, Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,) => { module Method = RewriteReverse(HOTerm, Judgment) type props<'a> = { method: Method.t<'a>, scope: array<HOTerm.meta>, ruleStyle: RuleView.style, gen: HOTerm.gen, onChange: (Method.t<'a>, HOTerm.subst) => unit, } type srProps<'a> = { "proof": 'a, "scope": array<HOTerm.meta>, "ruleStyle": RuleView.style, "gen": HOTerm.gen, "onChange": ('a, HOTerm.subst) => unit, } let make = (subRender: srProps<'a> => React.element) => props => { <div> <b> {React.string("rewrite_reverse ")} </b> {React.string(props.method.equalityName)} <ul> <li> {React.createElement( React.component(subRender), { "proof": props.method.subgoal, "scope": props.scope, "ruleStyle": props.ruleStyle, "gen": props.gen, "onChange": (subgoal, subst: HOTerm.subst) => props.onChange({...props.method, subgoal}, subst), }, )} </li> </ul> </div> }}
module ConstructorNeqView = ( HOTerm: HOTerm.S, Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,) => { module Method = ConstructorNeq(HOTerm, Judgment) type props<'a> = { method: Method.t<'a>, scope: array<HOTerm.meta>, ruleStyle: RuleView.style, gen: HOTerm.gen, onChange: (Method.t<'a>, HOTerm.subst) => unit, } type srProps<'a> = { "proof": 'a, "scope": array<HOTerm.meta>, "ruleStyle": RuleView.style, "gen": HOTerm.gen, "onChange": ('a, HOTerm.subst) => unit, } let make = (_subRender: srProps<'a> => React.element) => _props => { <div> <b> {React.string("constructor_neq")} </b> </div> }}
module ConstructorInjView = ( HOTerm: HOTerm.S, Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t,) => { module Method = ConstructorInj(HOTerm, Judgment) type props<'a> = { method: Method.t<'a>, scope: array<HOTerm.meta>, ruleStyle: RuleView.style, gen: HOTerm.gen, onChange: (Method.t<'a>, HOTerm.subst) => unit, } type srProps<'a> = { "proof": 'a, "scope": array<HOTerm.meta>, "ruleStyle": RuleView.style, "gen": HOTerm.gen, "onChange": ('a, HOTerm.subst) => unit, } let make = (_subRender: srProps<'a> => React.element) => props => { <div> <b> {React.string( `constructor_inj ${props.method.source} ${Int.toString(props.method.argIndex)}`, )} </b> </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>, scope: array<Term.meta>, ruleStyle: RuleView.style, gen: Term.gen, onChange: (Method.t<'a>, Term.subst) => unit, } type srProps<'a> = Method1View.srProps<'a> let make = (subrender: srProps<'a> => React.element) => props => { switch props.method { | First(m) => Method1View.make(subrender)({ method: m, scope: props.scope, ruleStyle: props.ruleStyle, gen: props.gen, onChange: (n, s) => props.onChange(First(n), s), }) | Second(m) => Method2View.make(subrender)({ method: m, scope: props.scope, ruleStyle: props.ruleStyle, gen: props.gen, onChange: (n, s) => props.onChange(Second(n), s), }) } }}