replace strings with gadts in projector models

src/haz3lcore/pretty/ExpToSegment.re

@@ -699,8 +699,10 @@ let fold_fun_if = (condition, f_name: string, pieces) =>
     let str = FoldProj.sexp_of_t({text: f_name}) |> Sexplib.Sexp.to_string;
     switch (MakeTerm.for_projection([syntax])) {
     | None => failwith("ExpToSegment.fold_fun_if")
-    | Some(any) => [
-        ProjectorInit.init_or_noop_from_str(Fold, syntax, any, str),
+    | Some(_) => [
+        Base.Projector(
+          ProjectorCore.mk(Fold, syntax, V(Fold, {text: str})),
+        ),
       ]
     };
   } else {

src/haz3lcore/projectors/ProjectorBase.re

@@ -131,6 +131,7 @@ module type Projector = {
    * need other state beyond the underlying syntax */
   [@deriving (show({with_path: false}), sexp, yojson)]
   type model;
+  let kind: ProjectorCore.Kind.gadt(model);
   /* An internal action type to be used in actions which
    * update the model. Use `unit` if the basic projector
    * actions (type `action`) above suffice */
@@ -169,39 +170,6 @@ module type Projector = {
   let update: (model, info, action) => model;
 };
 
-/* A cooked projector is the same as the base module
- * signature except model & action are serialized so
- * they may be used by the Editor without it having
- * specialized knowledge of projector internals */
-module type Cooked =
-  Projector with type model = string and type action = string;
-
-module Cook = (C: Projector) : Cooked => {
-  [@deriving (show({with_path: false}), sexp, yojson)]
-  type model = string;
-  [@deriving (show({with_path: false}), sexp, yojson)]
-  type action = string;
-  let serialize_m = m => m |> C.sexp_of_model |> Sexplib.Sexp.to_string;
-  let deserialize_m = s => s |> Sexplib.Sexp.of_string |> C.model_of_sexp;
-  let serialize_a = a => a |> C.sexp_of_action |> Sexplib.Sexp.to_string;
-  let deserialize_a = s => s |> Sexplib.Sexp.of_string |> C.action_of_sexp;
-  let init = any => C.init(any) |> Option.map(serialize_m);
-  let focusable = C.focusable;
-  let dynamics = C.dynamics;
-  let view = (m, info, ~local, ~parent, ~view_seg) =>
-    C.view(
-      deserialize_m(m),
-      info,
-      ~local=a => local(serialize_a(a)),
-      ~parent,
-      ~view_seg,
-    );
-  let placeholder = m =>
-    m |> Sexplib.Sexp.of_string |> C.model_of_sexp |> C.placeholder;
-  let update = (m, i, a) =>
-    C.update(m |> deserialize_m, i, a |> deserialize_a) |> serialize_m;
-};
-
 /* Projectors currently are all convex */
 let shapes = (_: ProjectorCore.t(syntax)): Nibs.shapes =>
   Nib.Shape.(Convex, Convex);

src/haz3lcore/projectors/ProjectorCore.re

@@ -27,6 +27,60 @@
     | Card
     | TextArea;
 
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type type_model =
+    | Expected
+    | Self;
+
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type card_mode =
+    | Show
+    | Choose(int)
+    | Flipped;
+
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type fold_model = {
+    [@default "⋱"]
+    text: string,
+  };
+
+  type gadt('a) =
+    | Fold: gadt(fold_model)
+    | Info: gadt(type_model)
+    | Probe: gadt(unit)
+    | Checkbox: gadt(unit)
+    | Slider: gadt(unit)
+    | SliderF: gadt(unit)
+    | Card: gadt(card_mode)
+    | TextArea: gadt(unit);
+
+  let of_gadt = (type a, kind: gadt(a)): t =>
+    switch (kind) {
+    | Fold => Fold
+    | Info => Info
+    | Probe => Probe
+    | Checkbox => Checkbox
+    | Slider => Slider
+    | SliderF => SliderF
+    | Card => Card
+    | TextArea => TextArea
+    };
+
+  type w =
+    | W(gadt('a)): w;
+
+  let (let.gadt) = (type b, kind: t, f: w => b) =>
+    switch (kind) {
+    | Fold => f(W(Fold))
+    | Info => f(W(Info))
+    | Probe => f(W(Probe))
+    | Checkbox => f(W(Checkbox))
+    | Slider => f(W(Slider))
+    | SliderF => f(W(SliderF))
+    | Card => f(W(Card))
+    | TextArea => f(W(TextArea))
+    };
+
   let livelit_projectors: list(t) = [
     Checkbox,
     Slider,
@@ -69,13 +123,82 @@
     };
 };
 
+type model =
+  | V(Kind.gadt('a), 'a): model;
+
+let pp_model = (f, model) =>
+  Format.fprintf(
+    f,
+    switch (model) {
+    | V(Fold, _) => "Fold"
+    | V(Info, _) => "Info"
+    | V(Probe, _) => "Probe"
+    | V(Checkbox, _) => "Checkbox"
+    | V(Slider, _) => "Slider"
+    | V(SliderF, _) => "SliderF"
+    | V(Card, _) => "Card"
+    | V(TextArea, _) => "TextArea"
+    },
+  );
+
+let model_of_sexp = (sexp: Sexplib.Sexp.t): model =>
+  // take s-expressions of the form ("fold", m), deserialize m, and turn it into V(Fold, m)
+  switch (sexp) {
+  | List([Atom("fold"), m]) => V(Fold, m |> Kind.fold_model_of_sexp)
+  | List([Atom("info"), m]) => V(Info, m |> Kind.type_model_of_sexp)
+  | List([Atom("probe"), _]) => V(Probe, ())
+  | List([Atom("checkbox"), _]) => V(Checkbox, ())
+  | List([Atom("slider"), _]) => V(Slider, ())
+  | List([Atom("sliderf"), _]) => V(SliderF, ())
+  | List([Atom("card"), m]) => V(Card, m |> Kind.card_mode_of_sexp)
+  | List([Atom("text"), _]) => V(TextArea, ())
+  | _ => failwith("Unknown projector kind")
+  };
+
+let sexp_of_model = (model: model): Sexplib.Sexp.t =>
+  switch (model) {
+  | V(Fold, m) => List([Atom("fold"), m |> Kind.sexp_of_fold_model])
+  | V(Info, m) => List([Atom("info"), m |> Kind.sexp_of_type_model])
+  | V(Probe, _) => List([Atom("probe"), () |> sexp_of_unit])
+  | V(Checkbox, _) => List([Atom("checkbox"), () |> sexp_of_unit])
+  | V(Slider, _) => List([Atom("slider"), () |> sexp_of_unit])
+  | V(SliderF, _) => List([Atom("sliderf"), () |> sexp_of_unit])
+  | V(Card, m) => List([Atom("card"), m |> Kind.sexp_of_card_mode])
+  | V(TextArea, _) => List([Atom("text"), () |> sexp_of_unit])
+  };
+
+let model_of_yojson = (yojson: Yojson.Safe.t): model =>
+  switch (yojson) {
+  | `List([`String("fold"), m]) => V(Fold, m |> Kind.fold_model_of_yojson)
+  | `List([`String("info"), m]) => V(Info, m |> Kind.type_model_of_yojson)
+  | `List([`String("probe"), _]) => V(Probe, ())
+  | `List([`String("checkbox"), _]) => V(Checkbox, ())
+  | `List([`String("slider"), _]) => V(Slider, ())
+  | `List([`String("sliderf"), _]) => V(SliderF, ())
+  | `List([`String("card"), m]) => V(Card, m |> Kind.card_mode_of_yojson)
+  | `List([`String("text"), _]) => V(TextArea, ())
+  | _ => failwith("Unknown projector kind")
+  };
+
+let yojson_of_model = (model: model): Yojson.Safe.t =>
+  switch (model) {
+  | V(Fold, m) => `List([`String("fold"), m |> Kind.yojson_of_fold_model])
+  | V(Info, m) => `List([`String("info"), m |> Kind.yojson_of_type_model])
+  | V(Probe, _) => `List([`String("probe"), () |> yojson_of_unit])
+  | V(Checkbox, _) => `List([`String("checkbox"), () |> yojson_of_unit])
+  | V(Slider, _) => `List([`String("slider"), () |> yojson_of_unit])
+  | V(SliderF, _) => `List([`String("sliderf"), () |> yojson_of_unit])
+  | V(Card, m) => `List([`String("card"), m |> Kind.yojson_of_card_mode])
+  | V(TextArea, _) => `List([`String("text"), () |> yojson_of_unit])
+  };
+
 /* Projectors in syntax */
 [@deriving (show({with_path: false}), sexp, yojson)]
 type t('syntax) = {
   id: Id.t,
   kind: Kind.t,
   syntax: 'syntax,
-  model: string,
+  model,
 };
 
 let mk = (kind, syntax, model) => {

src/haz3lcore/projectors/ProjectorInfo.re

@@ -39,8 +39,9 @@
   let from_semantics =
       (statics: Statics.Map.t, dynamics: Dynamics.Map.t, p: Base.projector)
       : ProjectorCore.Shape.t => {
-    let (module P) = ProjectorInit.to_module(p.kind);
-    P.placeholder(p.model, mk_info(p, ~statics, ~dynamics));
+    let V(kind, model) = p.model;
+    let (module P) = ProjectorInit.to_module(kind);
+    P.placeholder(model, mk_info(p, ~statics, ~dynamics));
   };
 
   let mk =

src/haz3lcore/projectors/ProjectorInit.re

@@ -4,25 +4,32 @@
  * it can be instantiated. The first-class module created by
  * this function must be reified whenever projector methods
  * are to be called; see `shape` below for an example */
-let to_module = (kind: ProjectorCore.Kind.t): (module Cooked) =>
+let to_module =
+    (type a, kind: ProjectorCore.Kind.gadt(a))
+    : (module Projector with type model = a) =>
   switch (kind) {
-  | Fold => (module Cook(FoldProj.M))
-  | Info => (module Cook(TypeProj.M))
-  | Probe => (module Cook(ProbeProj.M))
-  | Slider => (module Cook(SliderProj.M))
-  | SliderF => (module Cook(SliderFProj.M))
-  | Checkbox => (module Cook(CheckboxProj.M))
-  | TextArea => (module Cook(TextAreaProj.M))
-  | Card => (module Cook(CardProj.M))
+  | Fold => (module FoldProj.M)
+  | Info => (module TypeProj.M)
+  | Probe => (module ProbeProj.M)
+  | Slider => (module SliderProj.M)
+  | SliderF => (module SliderFProj.M)
+  | Checkbox => (module CheckboxProj.M)
+  | TextArea => (module TextAreaProj.M)
+  | Card => (module CardProj.M)
   };
 
 let init =
     (kind: ProjectorCore.Kind.t, syntax: syntax, any: Term.Any.t)
     : option(syntax) => {
-  let (module P) = to_module(kind);
+  open ProjectorCore.Kind;
+  let.gadt W(kind_gadt) = kind;
+  let (module P) = to_module(kind_gadt);
   switch (P.init(any)) {
   | None => None
-  | Some(model) => Some(Projector(ProjectorCore.mk(kind, syntax, model)))
+  | Some(model) =>
+    Some(
+      Base.Projector(ProjectorCore.mk(kind, syntax, V(kind_gadt, model))),
+    )
   };
 };
 
@@ -32,18 +39,3 @@
   | Some(pr) => pr
   | None => syntax
   };
-
-let init_or_noop_from_str =
-    (
-      kind: ProjectorCore.Kind.t,
-      syntax: syntax,
-      any: Term.Any.t,
-      model_str: string,
-    )
-    : syntax => {
-  let (module P) = to_module(kind);
-  switch (P.init(any)) {
-  | None => syntax
-  | Some(_) => Projector(ProjectorCore.mk(kind, syntax, model_str))
-  };
-};

src/haz3lcore/projectors/ProjectorPerform.re

@@ -146,6 +146,8 @@ let go =
       ),
     )
   | Focus(id, kind, d) =>
+    open ProjectorCore.Kind;
+    let.gadt W(kind) = kind;
     switch (d) {
     | None =>
       /* Focus by mouse click */
@@ -171,7 +173,7 @@ let go =
       | None => ()
       };
       Ok(z);
-    }
+    };
   | Escape(id, d) => Ok(jump_to_side_of_id(d, z, id))
   };
 };

src/haz3lcore/projectors/implementations/CardProj.re

@@ -3,20 +3,17 @@
 open ProjectorBase;
 
 [@deriving (show({with_path: false}), sexp, yojson)]
-type mode =
-  | Show
-  | Choose(int)
-  | Flipped;
+type mode = ProjectorCore.Kind.card_mode;
 
 [@deriving (show({with_path: false}), sexp, yojson)]
-type model = {mode};
+type model = mode;
 [@deriving (show({with_path: false}), sexp, yojson)]
 type action =
   | SetMode(mode);
 
 let model_of_sexp = (sexp: Sexplib.Sexp.t): model =>
   switch (model_of_sexp(sexp)) {
-  | exception _ => {mode: Show}
+  | exception _ => Show
   | m => m
   };
 
@@ -454,6 +451,8 @@
     );
 };
 
+open ProjectorCore.Kind;
+
 module Singleton = {
   let view =
       (
@@ -605,16 +604,17 @@
 [@deriving (show({with_path: false}), sexp, yojson)]
 type a = action;
 
-module M: Projector = {
+module M: Projector with type model = m = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type model = m;
+  let kind = ProjectorCore.Kind.Card;
   [@deriving (show({with_path: false}), sexp, yojson)]
   type action = a;
   let focusable = Focusable.non;
   let dynamics = false;
 
   let init = (info: TermBase.Any.t): option(model) =>
-    SyntaxTerm.get_opt(info) != None ? Some({mode: Show}) : None;
+    SyntaxTerm.get_opt(info) != None ? Some(Show) : None;
 
   let placeholder = (_, info): ProjectorCore.Shape.t => {
     horizontal: SyntaxTerm.width_of_any(info),
@@ -623,7 +623,7 @@
 
   let update = (_model, _, action) =>
     switch (action) {
-    | SetMode(mode) => {mode: mode}
+    | SetMode(mode) => mode
     };
 
   let view =
@@ -638,9 +638,9 @@
     inline:
       switch (SyntaxTerm.get(info)) {
       | (sort, Card(card)) =>
-        Singleton.view(info, model.mode, parent, local, to_sort(sort), card)
+        Singleton.view(info, model, parent, local, to_sort(sort), card)
       | (sort, Hand(hand)) =>
-        Hand.view(info, model.mode, parent, local, to_sort(sort), hand)
+        Hand.view(info, model, parent, local, to_sort(sort), hand)
       },
     offside: None,
     overlay: None,

src/haz3lcore/projectors/implementations/CheckboxProj.re

@@ -2,9 +2,10 @@ open Util;
 open ProjectorBase;
 open Virtual_dom.Vdom;
 
-module M: Projector = {
+module M: Projector with type model = unit = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type model = unit;
+  let kind = ProjectorCore.Kind.Checkbox;
   [@deriving (show({with_path: false}), sexp, yojson)]
   type action = unit;