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.

beginning work on proof construction interface

+58 -7
+3
src/HOTerm.res
··· 20 20 let mapSubst = (m: subst, f: t => t): subst => { 21 21 m->Belt.Map.Int.map(f) 22 22 } 23 + let makeSubst = () => { 24 + Belt.Map.Int.empty 25 + } 23 26 let rec equivalent = (a: t, b: t) => { 24 27 switch (a, b) { 25 28 | (Symbol({name: na}), Symbol({name: nb})) => na == nb
+27 -1
src/Method.res
··· 16 16 type t<'a> 17 17 let keywords: array<string> 18 18 let check: (t<'a>, Context.t, Judgment.t, ('a, Rule.t) => 'b) => result<t<'b>, string> 19 + let apply: (Context.t, Judgment.t, Term.gen, (Rule.t => 'a)) => Dict.t<(t<'a>, Term.subst)> 19 20 let uncheck: (t<'a>, 'a => 'b) => t<'b> 20 21 let parse: ( 21 22 string, ··· 126 127 Error("Expected (") 127 128 } 128 129 } 130 + let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => { 131 + let ret = Dict.make() 132 + ctx.facts->Dict.forEachWithKey((rule, key) => { 133 + let insts = rule.vars 134 + ->Array.map(m => Term.place(gen->Term.fresh(~replacing=m),~scope=ctx.fixes)) 135 + let res = rule->Rule.instantiate(insts) 136 + let substs = Judgment.unify(res.conclusion,j,~gen) 137 + substs->Array.forEach(subst => { 138 + let new = { 139 + ruleName: key, 140 + instantiation: insts, 141 + subgoals: res.premises->Array.map(f) 142 + } 143 + ret->Dict.set("intro " ++ key, (new, subst)) 144 + }) 145 + }) 146 + ret 147 + } 129 148 let check = (it: t<'a>, ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => { 130 149 switch ctx.facts->Dict.get(it.ruleName) { 131 150 | None => Error("Cannot find rule '"->String.concat(it.ruleName)->String.concat("'")) ··· 201 220 | Error(e) => Error(e) 202 221 } 203 222 } 223 + let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => { 224 + Dict.make() 225 + } 204 226 let check = (it: t<'a>, _ctx: Context.t, j: Judgment.t, f: ('a, Rule.t) => 'b) => { 205 227 let first = f(it.proof, it.rule) 206 228 let second = f(it.show, {vars: [], premises: [it.rule], conclusion: j}) ··· 222 244 | Second(m) => Second(Method2.uncheck(m, f)) 223 245 } 224 246 let keywords = Array.concat(Method1.keywords, Method2.keywords) 225 - 247 + let apply = (ctx: Context.t, j: Judgment.t, gen: Term.gen, f: Rule.t => 'a) => { 248 + let d1 = Method1.apply(ctx,j,gen,f)->Dict.mapValues(((m,s)) => (First(m),s)) 249 + let d2 = Method2.apply(ctx,j,gen,f)->Dict.mapValues(((m,s)) => (Second(m),s)) 250 + d1->Dict.assign(d2) 251 + } 226 252 let check = (it, ctx, j, f) => 227 253 switch it { 228 254 | First(m) => m->Method1.check(ctx, j, f)->Result.map(x => First(x))
+22 -4
src/Proof.res
··· 13 13 assumptions: array<string>, 14 14 method: option<Method.t<t>>, 15 15 } 16 + 16 17 type rec checked = 17 18 | Checked({ 18 19 fixes: array<Term.meta>, 19 20 assumptions: array<string>, 20 - method: option<Method.t<checked>>, 21 + method: checked_option_method, 21 22 rule: Rule.t, 22 23 }) 23 24 | ProofError({raw: t, rule: Rule.t, msg: string}) 25 + and checked_option_method = 26 + | Do(Method.t<checked>) 27 + | Goal(Term.gen => Dict.t<(Method.t<checked>,Term.subst)>) 24 28 let parseKeyword = input => { 25 29 Method.keywords 26 30 ->Array.concat(["?"]) ··· 117 121 | Checked({fixes, assumptions, method, rule: _}) => { 118 122 fixes, 119 123 assumptions, 120 - method: method->Option.map(xs => xs->Method.uncheck(uncheck)), 124 + method: switch method { 125 + | Do(m) => Some(m->Method.uncheck(uncheck)) 126 + | Goal(_) => None 127 + } 121 128 } 122 129 } 123 130 let rec check = (ctx: Context.t, prf: t, rule: Rule.t) => { ··· 133 140 rule, 134 141 fixes: prf.fixes, 135 142 assumptions: prf.assumptions, 136 - method: Some(m'), 143 + method: Do(m'), 137 144 }) 138 145 | Error(e) => ProofError({raw: prf, rule, msg: e}) 139 146 } ··· 142 149 rule, 143 150 fixes: prf.fixes, 144 151 assumptions: prf.assumptions, 145 - method: None, 152 + method: Goal(gen => { 153 + Method.apply(ctx',rule.conclusion,gen, rl => { 154 + check(ctx',{ 155 + fixes:rl.vars, 156 + method: None, 157 + assumptions:Array.fromInitializer( 158 + ~length=rl.premises->Array.length, 159 + i => Int.toString(i) 160 + ) 161 + },rl) 162 + }) 163 + }), 146 164 }) 147 165 } 148 166 | Error(e) => ProofError({raw: prf, rule, msg: e})
+2 -2
src/ProofView.res
··· 35 35 <div className="proof-show"> 36 36 <JudgmentView judgment={rule.conclusion} scope /> 37 37 {switch method { 38 - | None => React.null 39 - | Some(method) => 38 + | Goal(options) => <button onClick={_ => Console.log(options(Term.makeGen()))}> {React.string("Test")} </button> 39 + | Do(method) => 40 40 React.createElement( 41 41 MethodView.make(p => 42 42 make({proof: p["proof"], scope: p["scope"], ruleStyle: p["ruleStyle"]})
+3
src/SExp.res
··· 18 18 }) 19 19 nu 20 20 } 21 + let makeSubst = () => { 22 + Map.make() 23 + } 21 24 let equivalent = (a: t, b: t) => { 22 25 a == b 23 26 }
+1
src/Signatures.res
··· 6 6 let mapSubst: (subst, t => t) => subst 7 7 type gen 8 8 let substitute: (t, subst) => t 9 + let makeSubst: () => subst 9 10 let unify: (t, t, ~gen: gen=?) => array<subst> 10 11 // law: unify(a,b) == [{}] iff equivalent(a,b) 11 12 let equivalent: (t, t) => bool