Haz3l checkbox and slider livelits

src/haz3lcore/Measured.re

@@ -282,6 +282,16 @@ let is_indented_map = (seg: Segment.t) => {
   go(seg);
 };
 
+let livelit_padding = (t: Base.tile): abs_indent =>
+  switch (t.label) {
+  | [possible_livelit_name] =>
+    switch (Livelit.find_livelit(possible_livelit_name)) {
+    | Some(ll) => ll.width + 1 // Add one for margin
+    | None => 0
+    }
+  | _ => 0
+  };
+
 let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
   let is_indented = is_indented_map(seg);
 
@@ -377,10 +387,12 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => {
           | Tile(t) =>
             let token = List.nth(t.label);
             let add_shard = (origin, shard, map) => {
+              let lp = livelit_padding(t);
               let last =
                 Point.{
                   ...origin,
-                  col: origin.col + String.length(token(shard)),
+                  col:
+                    origin.col + (lp > 0 ? lp : String.length(token(shard))),
                 };
               let map = map |> add_s(t.id, shard, {origin, last});
               (last, map);

src/haz3lcore/dynamics/elaborator.re

@@ -135,7 +135,9 @@ let wrap = (u, mode, self, d: DHExp.t): option(DHExp.t) =>
   | InHole(_) => Some(NonEmptyHole(TypeInconsistent, u, 0, d))
   };
 
-let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) => {
+let rec dhexp_of_uexp =
+        (m: Statics.map, uexp: Term.UExp.t, livelits: Livelit.state)
+        : option(DHExp.t) => {
   /* NOTE: Left out delta for now */
   switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) {
   | Some(InfoExp({mode, self, _})) =>
@@ -170,20 +172,21 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) =>
       | Float(n) => Some(FloatLit(n))
       | String(s) => Some(StringLit(s))
       | ListLit(es) =>
-        let+ ds = es |> List.map(dhexp_of_uexp(m)) |> OptUtil.sequence;
+        let+ ds =
+          es |> List.map(dhexp_of_uexp(m, _, livelits)) |> OptUtil.sequence;
         let ty = Statics.exp_typ(m, uexp) |> Typ.matched_list;
         //TODO: why is there an err status on below?
         DHExp.ListLit(id, 0, StandardErrStatus(NotInHole), ty, ds);
       | Fun(p, body) =>
         let* dp = dhpat_of_upat(m, p);
-        let+ d1 = dhexp_of_uexp(m, body);
+        let+ d1 = dhexp_of_uexp(m, body, livelits);
         DHExp.Fun(dp, Statics.pat_typ(m, p), d1, None);
       | Tuple(es) =>
         let+ ds =
           List.fold_right(
             (e, ds_opt) => {
               let* ds = ds_opt;
-              let+ d = dhexp_of_uexp(m, e);
+              let+ d = dhexp_of_uexp(m, e, livelits);
               [d, ...ds];
             },
             es,
@@ -192,24 +195,24 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) =>
         DHExp.Tuple(ds);
       | Tag(name) => Some(Tag(name))
       | Cons(e1, e2) =>
-        let* dc1 = dhexp_of_uexp(m, e1);
-        let+ dc2 = dhexp_of_uexp(m, e2);
+        let* dc1 = dhexp_of_uexp(m, e1, livelits);
+        let+ dc2 = dhexp_of_uexp(m, e2, livelits);
         DHExp.Cons(dc1, dc2);
       | UnOp(Int(Minus), e) =>
-        let+ dc = dhexp_of_uexp(m, e);
+        let+ dc = dhexp_of_uexp(m, e, livelits);
         DHExp.BinIntOp(Minus, IntLit(0), dc);
       | BinOp(op, e1, e2) =>
         let (_, cons) = exp_binop_of(op);
-        let* dc1 = dhexp_of_uexp(m, e1);
-        let+ dc2 = dhexp_of_uexp(m, e2);
+        let* dc1 = dhexp_of_uexp(m, e1, livelits);
+        let+ dc2 = dhexp_of_uexp(m, e2, livelits);
         cons(dc1, dc2);
-      | Parens(e) => dhexp_of_uexp(m, e)
+      | Parens(e) => dhexp_of_uexp(m, e, livelits)
       | Seq(e1, e2) =>
-        let* d1 = dhexp_of_uexp(m, e1);
-        let+ d2 = dhexp_of_uexp(m, e2);
+        let* d1 = dhexp_of_uexp(m, e1, livelits);
+        let+ d2 = dhexp_of_uexp(m, e2, livelits);
         DHExp.Sequence(d1, d2);
       | Test(test) =>
-        let+ dtest = dhexp_of_uexp(m, test);
+        let+ dtest = dhexp_of_uexp(m, test, livelits);
         DHExp.Ap(TestLit(id), dtest);
       | Var(name) =>
         switch (err_status) {
@@ -224,8 +227,8 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) =>
             | d => d
         );
         let* dp = dhpat_of_upat(m, p);
-        let* ddef = dhexp_of_uexp(m, def);
-        let+ dbody = dhexp_of_uexp(m, body);
+        let* ddef = dhexp_of_uexp(m, def, livelits);
+        let+ dbody = dhexp_of_uexp(m, body, livelits);
         let ty = Statics.pat_self_typ(m, p);
         switch (Term.UPat.get_recursive_bindings(p)) {
         | None =>
@@ -258,13 +261,13 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) =>
           Let(dp, FixF(self_id, ty, substituted_def), dbody);
         };
       | Ap(fn, arg) =>
-        let* c_fn = dhexp_of_uexp(m, fn);
-        let+ c_arg = dhexp_of_uexp(m, arg);
+        let* c_fn = dhexp_of_uexp(m, fn, livelits);
+        let+ c_arg = dhexp_of_uexp(m, arg, livelits);
         DHExp.Ap(c_fn, c_arg);
       | If(scrut, e1, e2) =>
-        let* d_scrut = dhexp_of_uexp(m, scrut);
-        let* d1 = dhexp_of_uexp(m, e1);
-        let+ d2 = dhexp_of_uexp(m, e2);
+        let* d_scrut = dhexp_of_uexp(m, scrut, livelits);
+        let* d1 = dhexp_of_uexp(m, e1, livelits);
+        let+ d2 = dhexp_of_uexp(m, e2, livelits);
         let d_rules =
           DHExp.[Rule(BoolLit(true), d1), Rule(BoolLit(false), d2)];
         let d = DHExp.Case(d_scrut, d_rules, 0);
@@ -273,13 +276,19 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) =>
           DHExp.InconsistentBranches(id, 0, d)
         | _ => ConsistentCase(d)
         };
+      | LivelitAp({livelit_name}) =>
+        Livelit.elaborate_livelit(
+          livelit_name,
+          Term.UExp.rep_id(uexp),
+          livelits,
+        )
       | Match(scrut, rules) =>
-        let* d_scrut = dhexp_of_uexp(m, scrut);
+        let* d_scrut = dhexp_of_uexp(m, scrut, livelits);
         let+ d_rules =
           List.map(
             ((p, e)) => {
               let* d_p = dhpat_of_upat(m, p);
-              let+ d_e = dhexp_of_uexp(m, e);
+              let+ d_e = dhexp_of_uexp(m, e, livelits);
               DHExp.Rule(d_p, d_e);
             },
             rules,
@@ -372,8 +381,10 @@ let uexp_elab_wrap_builtins = (d: DHExp.t): DHExp.t =>
     Builtins.forms(Builtins.Pervasives.builtins),
   );
 
-let uexp_elab = (m: Statics.map, uexp: Term.UExp.t): ElaborationResult.t =>
-  switch (dhexp_of_uexp(m, uexp)) {
+let uexp_elab =
+    (m: Statics.map, uexp: Term.UExp.t, livelits: Livelit.state)
+    : ElaborationResult.t =>
+  switch (dhexp_of_uexp(m, uexp, livelits)) {
   | None => DoesNotElaborate
   | Some(d) =>
     let d = uexp_elab_wrap_builtins(d);

src/haz3lcore/lang/Form.re

@@ -90,11 +90,22 @@ let is_typ_var = t => is_capitalized_name(t) && !is_concrete_typ(t);
 let is_partial_concrete_typ = x =>
   !is_concrete_typ(x) && is_capitalized_name(x);
 let is_wild = regexp("^_$");
+let is_livelit = t =>
+  switch (Livelit.find_livelit(t)) {
+  | Some(_) => true
+  | _ => false
+  };
+let is_unknown_livelit = str => {
+  regexp("^[\\^]([a-z][A-Za-z0-9_]*)?\t?$", str) && !is_livelit(str);
+};
 
 /* The below case represents tokens which we want the user to be able to
    type in, but which have no reasonable semantic interpretation */
 let is_bad_lit = str =>
-  is_bad_int(str) || is_bad_float(str) || is_partial_concrete_typ(str);
+  is_bad_int(str)
+  || is_bad_float(str)
+  || is_partial_concrete_typ(str)
+  || is_unknown_livelit(str);
 
 /* is_string: last clause is a somewhat hacky way of making sure
    there are at most two quotes, in order to prevent merges */
@@ -174,6 +185,7 @@ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [
   ("int_lit", (is_int, [mk_op(Exp, []), mk_op(Pat, [])])),
   ("wild", (is_wild, [mk_op(Pat, [])])),
   ("string", (is_string, [mk_op(Exp, []), mk_op(Pat, [])])),
+  ("livelit", (is_livelit, [mk_op(Exp, [])])),
 ];
 
 /* C. Compound Forms:

src/haz3lcore/prog/Interface.re

@@ -1,6 +1,6 @@
 exception DoesNotElaborate;
-let elaborate = (map, term): DHExp.t =>
-  switch (Elaborator.uexp_elab(map, term)) {
+let elaborate = (~livelits=Livelit.empty_state, map, term): DHExp.t =>
+  switch (Elaborator.uexp_elab(map, term, livelits)) {
   | DoesNotElaborate =>
     print_endline("Interface.elaborate EXCEPTION");
     //HACK(andrew): supress exceptions for release

src/haz3lcore/statics/MakeTerm.re

@@ -219,6 +219,8 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
       | ([t], []) when Form.is_empty_list(t) => ret(ListLit([]))
       | ([t], []) when Form.is_bool(t) => ret(Bool(bool_of_string(t)))
       | ([t], []) when Form.is_int(t) => ret(Int(int_of_string(t)))
+      | ([t], []) when Form.is_livelit(t) =>
+        ret(LivelitAp({livelit_name: t}))
       | ([t], []) when Form.is_string(t) => ret(String(t))
       | ([t], []) when Form.is_float(t) => ret(Float(float_of_string(t)))
       | ([t], []) when Form.is_var(t) => ret(Var(t))

src/haz3lcore/statics/Statics.re

@@ -459,6 +459,11 @@ and uexp_to_info_map =
       ~free=Ctx.union([free_def, Ctx.subtract_typ(ctx_pat_ana, free_body)]),
       union_m([m_pat, m_def, m_body]),
     );
+  | LivelitAp({livelit_name}) =>
+    switch (Livelit.find_livelit(livelit_name)) {
+    | Some(ll) => atomic(Just(ll.expansion_type))
+    | None => atomic(Just(Unknown(TypeHole)))
+    }
   | Match(scrut, rules) =>
     let (ty_scrut, free_scrut, m_scrut) = go(~mode=Syn, scrut);
     let (pats, branches) = List.split(rules);

src/haz3lcore/statics/Term.re

@@ -359,7 +359,8 @@ module UExp = {
     | Cons(_) => Cons
     | UnOp(op, _) => UnOp(op)
     | BinOp(op, _, _) => BinOp(op)
-    | Match(_) => Match;
+    | Match(_) => Match
+    | LivelitAp(_) => LivelitAp;
 
   let show_op_un_int: op_un_int => string =
     fun
@@ -435,7 +436,8 @@ module UExp = {
     | Cons => "Cons"
     | BinOp(op) => show_binop(op)
     | UnOp(op) => show_unop(op)
-    | Match => "Match Expression";
+    | Match => "Match Expression"
+    | LivelitAp => "Livelit Application";
 
   let rec is_fun = (e: t) => {
     switch (e.term) {
@@ -461,6 +463,7 @@ module UExp = {
     | UnOp(_)
     | BinOp(_)
     | Match(_)
+    | LivelitAp(_)
     | Tag(_) => false
     };
   };
@@ -491,6 +494,7 @@ module UExp = {
       | UnOp(_)
       | BinOp(_)
       | Match(_)
+      | LivelitAp(_)
       | Tag(_) => false
       }
     );

src/haz3lcore/statics/TermBase.re

@@ -108,7 +108,8 @@ and UExp: {
     | Cons
     | UnOp(op_un)
     | BinOp(op_bin)
-    | Match;
+    | Match
+    | LivelitAp;
 
   [@deriving (show({with_path: false}), sexp, yojson)]
   type term =
@@ -136,6 +137,7 @@ and UExp: {
     | UnOp(op_un, t)
     | BinOp(op_bin, t, t)
     | Match(t, list((UPat.t, t)))
+    | LivelitAp({livelit_name: string})
   and t = {
     // invariant: nonempty
     ids: list(Id.t),
@@ -216,7 +218,8 @@ and UExp: {
     | Cons
     | UnOp(op_un)
     | BinOp(op_bin)
-    | Match;
+    | Match
+    | LivelitAp;
 
   [@deriving (show({with_path: false}), sexp, yojson)]
   type term =
@@ -244,6 +247,7 @@ and UExp: {
     | UnOp(op_un, t)
     | BinOp(op_bin, t, t)
     | Match(t, list((UPat.t, t)))
+    | LivelitAp({livelit_name: string})
   and t = {
     // invariant: nonempty
     ids: list(Id.t),

src/haz3lcore/tiles/Livelit.re

@@ -0,0 +1,49 @@
+open Sexplib.Std;
+
+[@deriving (show({with_path: false}), sexp, yojson)]
+type t = {
+  name: string,
+  width: int,
+  default: DHExp.t,
+  expansion_type: Typ.t,
+};
+
+type state = Id.Map.t(DHExp.t);
+let empty_state: state = Id.Map.empty;
+let slider: t = {
+  name: "^slider\t",
+  width: 10,
+  default: IntLit(50),
+  expansion_type: Int,
+};
+
+let checkbox: t = {
+  name: "^checkbox\t",
+  width: 1,
+  default: BoolLit(false),
+  expansion_type: Bool,
+};
+
+let fslider: t = {
+  name: "^fslider\t",
+  width: 10,
+  default: FloatLit(0.5),
+  expansion_type: Float,
+};
+
+let livelits: list(t) = [checkbox, fslider, slider];
+
+let find_livelit = (livelit_name: string): option(t) =>
+  List.find_opt(l => l.name == livelit_name, livelits);
+
+let elaborate_livelit =
+    (livelit_name: string, uexp_id: int, livelits: state): option(DHExp.t) => {
+  switch (Id.Map.find_opt(uexp_id, livelits)) {
+  | Some(t) => Some(t)
+  | None =>
+    switch (find_livelit(livelit_name)) {
+    | Some(l) => Some(l.default)
+    | None => None
+    }
+  };
+};

src/haz3lcore/zipper/Editor.re

@@ -7,6 +7,7 @@ module Meta = {
     measured: Measured.t,
     term_ranges: TermRanges.t,
     col_target: int,
+    livelits: Livelit.state,
   };
 
   let init = (z: Zipper.t) => {
@@ -16,6 +17,7 @@ module Meta = {
       measured: Measured.of_segment(unselected),
       term_ranges: TermRanges.mk(unselected),
       col_target: 0,
+      livelits: Livelit.empty_state,
     };
   };
 
@@ -42,7 +44,7 @@ module Meta = {
 
   let next =
       (~effects: list(Effect.t)=[], a: Action.t, z: Zipper.t, meta: t): t => {
-    let {touched, measured, col_target, _} = meta;
+    let {touched, measured, col_target, livelits, _} = meta;
     let touched = Touched.update(Time.tick(), effects, touched);
     let unselected = Zipper.unselect_and_zip(z);
     let measured = Measured.of_segment(~touched, ~old=measured, unselected);
@@ -53,7 +55,7 @@ module Meta = {
       | Select(Resize(Local(Up | Down))) => col_target
       | _ => Zipper.caret_point(measured, z).col
       };
-    {touched, measured, term_ranges, col_target};
+    {touched, measured, term_ranges, col_target, livelits};
   };
 };
 
@@ -172,3 +174,14 @@ let trailing_hole_ctx = (ed: t, info_map: Statics.map) => {
     };
   };
 };
+
+let update_livelits = (f: Livelit.state => Livelit.state, ed: t): t => {
+  let new_state: State.t = {
+    ...ed.state,
+    meta: {
+      ...ed.state.meta,
+      livelits: f(ed.state.meta.livelits),
+    },
+  };
+  {...ed, state: new_state};
+};