the next generation of the in-browser educational proof assistant
1open Signatures
2open Component
3
4module Make = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => {
5 module Ports = Ports(Term, Judgment)
6 open RuleView
7 type props = {
8 content: style,
9 imports: Ports.t,
10 onChange: (style, ~exports: Ports.t=?) => unit,
11 }
12 let deserialise = str =>
13 switch str {
14 | "Gentzen" => Ok((Gentzen, Ports.empty))
15 | "Linear" => Ok((Linear, Ports.empty))
16 | "Hybrid" => Ok((Hybrid, Ports.empty))
17 | _ => Error("unknown rule style")
18 }
19 let serialise = style =>
20 switch style {
21 | Gentzen => "Gentzen"
22 | Linear => "Linear"
23 | Hybrid => "Hybrid"
24 }
25
26 let make = props => {
27 let (style, setStyle) = React.useState(_ => props.content)
28 let onChange = e => {
29 let target = JsxEvent.Form.target(e)
30 let value: string = target["value"]
31 switch deserialise(value) {
32 | Ok((sty, _)) => {
33 setStyle(_ => sty)
34 props.onChange(sty, ~exports={Ports.facts: Dict.make(), ruleStyle: Some(sty)})
35 }
36 | Error(_) => ()
37 }
38 }
39 [Gentzen, Linear, Hybrid]
40 ->Array.map(n =>
41 <input
42 type_="radio"
43 id={"style_"->String.concat(String.make(n))}
44 key={String.make(n)}
45 name="style"
46 onChange
47 value={String.make(n)}
48 checked={style == n}
49 />
50 )
51 ->React.array
52 }
53}