From 31e836b252a97cc3c23c281bcf19b3728729ecf0 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 7 Jan 2023 15:35:50 -0600 Subject: [PATCH 01/52] Start messing around with LiveLit definitions --- src/haz3lcore/dynamics/elaborator.re | 1 + src/haz3lcore/lang/Form.re | 4 ++++ src/haz3lcore/statics/Statics.re | 2 ++ src/haz3lcore/statics/Term.re | 8 ++++++-- src/haz3lcore/statics/TermBase.re | 22 ++++++++++++++++++++-- src/haz3lweb/LangDocMessages.re | 2 ++ src/haz3lweb/view/LangDoc.re | 13 +++++++++++++ 7 files changed, 48 insertions(+), 4 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index fd8f01cb3c..18477a2e00 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -296,6 +296,7 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) => Some(DHExp.InconsistentBranches(u, 0, d)) | _ => wrap(ConsistentCase(d)) }; + | LivelitDef(livelit_record) => dhexp_of_uexp(m, livelit_record.init) // TODO abandukwala }; | Some(InfoPat(_) | InfoTyp(_) | InfoRul(_) | Invalid(_)) | None => None diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 99b980817c..52d28586af 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -183,6 +183,10 @@ let forms: list((string, t)) = [ ("ap_exp", mk(ii, ["(", ")"], mk_post(P.ap, Exp, [Exp]))), ("ap_pat", mk(ii, ["(", ")"], mk_post(P.ap, Pat, [Pat]))), ("let_", mk(ds, ["let", "=", "in"], mk_pre(P.let_, Exp, [Pat, Exp]))), + ( + "livelit_def", + mk(ds, ["livelit", "at", "in"], mk_pre(P.let_, Exp, [Pat, Typ])), // TODO: How do we syntactically want to handle the rest of the information in haz3l + ), ("typeann", mk(ss, [":"], mk_bin'(P.ann, Pat, Pat, [], Typ))), ("case", mk(ds, ["case", "end"], mk_op(Exp, [Rul]))), ( diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 889623909c..9f902fa560 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -440,6 +440,8 @@ 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]), ); + | LivelitDef(livelit_record) => + atomic(Just(Term.utyp_to_ty(livelit_record.expansion_type))) // TODO: I don't actually know what I'm doing here. I just did something close to list literals. | Match(scrut, rules) => let (ty_scrut, free_scrut, m_scrut) = go(~mode=Syn, scrut); let (pats, branches) = List.split(rules); diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 81297af417..03ad934a98 100644 --- a/src/haz3lcore/statics/Term.re +++ b/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 + | LivelitDef(_) => LivelitDef; 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" + | LivelitDef => "Livelit Expression"; let rec is_fun = (e: t) => { switch (e.term) { @@ -461,6 +463,7 @@ module UExp = { | UnOp(_) | BinOp(_) | Match(_) + | LivelitDef(_) | Tag(_) => false }; }; @@ -491,6 +494,7 @@ module UExp = { | UnOp(_) | BinOp(_) | Match(_) + | LivelitDef(_) | Tag(_) => false } ); diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index 05fb1d354d..a310c85bac 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -84,6 +84,13 @@ and UExp: { | Bool(op_bin_bool) | String(op_bin_string); + [@deriving (show({with_path: false}), sexp, yojson)] + type livelit_record = { + name: string, + expansion_type: UTyp.t, + init: UExp.t, + // TODO: The rest of the stuff + }; [@deriving (show({with_path: false}), sexp, yojson)] type cls = | Invalid @@ -108,7 +115,8 @@ and UExp: { | Cons | UnOp(op_un) | BinOp(op_bin) - | Match; + | Match + | LivelitDef; [@deriving (show({with_path: false}), sexp, yojson)] type term = @@ -136,6 +144,7 @@ and UExp: { | UnOp(op_un, t) | BinOp(op_bin, t, t) | Match(t, list((UPat.t, t))) + | LivelitDef(livelit_record) and t = { // invariant: nonempty ids: list(Id.t), @@ -192,6 +201,13 @@ and UExp: { | Bool(op_bin_bool) | String(op_bin_string); + [@deriving (show({with_path: false}), sexp, yojson)] + type livelit_record = { + name: string, + expansion_type: UTyp.t, + init: UExp.t, + }; + [@deriving (show({with_path: false}), sexp, yojson)] type cls = | Invalid @@ -216,7 +232,8 @@ and UExp: { | Cons | UnOp(op_un) | BinOp(op_bin) - | Match; + | Match + | LivelitDef; [@deriving (show({with_path: false}), sexp, yojson)] type term = @@ -244,6 +261,7 @@ and UExp: { | UnOp(op_un, t) | BinOp(op_bin, t, t) | Match(t, list((UPat.t, t))) + | LivelitDef(livelit_record) and t = { // invariant: nonempty ids: list(Id.t), diff --git a/src/haz3lweb/LangDocMessages.re b/src/haz3lweb/LangDocMessages.re index 24053441fb..5a14fecc35 100644 --- a/src/haz3lweb/LangDocMessages.re +++ b/src/haz3lweb/LangDocMessages.re @@ -2495,6 +2495,8 @@ let str_eq_exp: form = { }; }; +let livelit_def_exp_group = "livelit_def_exp_group"; + let case_exp_group = "case_exp_group"; let case_rules_group = "case_rules_group"; let case_example_wild_simple = { diff --git a/src/haz3lweb/view/LangDoc.re b/src/haz3lweb/view/LangDoc.re index 7b27d72878..6b6b9fa863 100644 --- a/src/haz3lweb/view/LangDoc.re +++ b/src/haz3lweb/view/LangDoc.re @@ -2146,6 +2146,19 @@ let get_doc = ), [], ); + | LivelitDef(_livelit_def) => + let (doc, options) = + LangDocMessages.get_form_and_options( + LangDocMessages.livelit_def_exp_group, + docs, + ); + get_message( + doc, + options, + LangDocMessages.livelit_def_exp_group, + doc.explanation.message, + [], + ); }; get_message_exp(term.term); | Some(InfoPat({term, _})) => From f288323e9ae8ef654ee16c0ec564f7144d70aadf Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 7 Jan 2023 15:41:26 -0600 Subject: [PATCH 02/52] Fix Term.show_cls --- src/haz3lcore/statics/Term.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 03ad934a98..0620e609aa 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -437,7 +437,7 @@ module UExp = { | BinOp(op) => show_binop(op) | UnOp(op) => show_unop(op) | Match => "Match Expression" - | LivelitDef => "Livelit Expression"; + | LivelitDef => "Livelit Definition"; let rec is_fun = (e: t) => { switch (e.term) { From df0e31b5ad49bff8b21a38a873d9a36d9da33bb8 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 7 Jan 2023 20:33:02 -0600 Subject: [PATCH 03/52] Temp commit debugging --- src/haz3lcore/dynamics/elaborator.re | 11 ++++++++- src/haz3lcore/lang/Form.re | 3 ++- src/haz3lcore/statics/MakeTerm.re | 7 ++++++ src/haz3lcore/statics/Statics.re | 1 + src/haz3lcore/statics/Term.re | 8 ++++-- src/haz3lcore/statics/TermBase.re | 14 ++++++++--- src/haz3lweb/LangDocMessages.re | 37 ++++++++++++++++++++++++++++ src/haz3lweb/view/LangDoc.re | 13 ++++++++++ 8 files changed, 86 insertions(+), 8 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index 18477a2e00..43bd62a0ea 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -54,6 +54,7 @@ let exp_binop_of: Term.UExp.op_bin => (Typ.t, (_, _) => DHExp.t) = ); let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) => { + print_endline(Term.UExp.show(uexp)); /* NOTE: Left out delta for now */ switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) { | Some(InfoExp({mode, self, _})) => @@ -296,7 +297,15 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) => Some(DHExp.InconsistentBranches(u, 0, d)) | _ => wrap(ConsistentCase(d)) }; - | LivelitDef(livelit_record) => dhexp_of_uexp(m, livelit_record.init) // TODO abandukwala + | LivelitDef(livelit_record) => + print_endline(TermBase.UExp.show_livelit_record(livelit_record)); + let foo = dhexp_of_uexp(m, livelit_record.body); // TODO abandukwala + switch (foo) { + | Some(t) => print_endline(DHExp.show(t)) + | None => print_endline("No value") + }; + foo; + | LivelitAp({livelit_name: _}) => assert(false) // TODO }; | Some(InfoPat(_) | InfoTyp(_) | InfoRul(_) | Invalid(_)) | None => None diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 52d28586af..c9e2874859 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -185,8 +185,9 @@ let forms: list((string, t)) = [ ("let_", mk(ds, ["let", "=", "in"], mk_pre(P.let_, Exp, [Pat, Exp]))), ( "livelit_def", - mk(ds, ["livelit", "at", "in"], mk_pre(P.let_, Exp, [Pat, Typ])), // TODO: How do we syntactically want to handle the rest of the information in haz3l + mk(ds, ["livelit", "at", "in"], mk_pre(P.let_, Exp, [Pat, Typ])) // TODO: How do we syntactically want to handle the rest of the information in haz3l ), + ("livelit_ap", mk(ss, ["$"], mk_pre(P.ap, Exp, [Pat]))), ("typeann", mk(ss, [":"], mk_bin'(P.ann, Pat, Pat, [], Typ))), ("case", mk(ds, ["case", "end"], mk_op(Exp, [Rul]))), ( diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 0b16fc1e4f..93650b1b70 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -10,6 +10,8 @@ WARNING: This module is still structurally in flux. */ +// TODO Livelit Expression and Term + open Util; open Term; @@ -247,6 +249,11 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | (["-"], []) => UnOp(Int(Minus), r) | (["fun", "->"], [Pat(pat)]) => Fun(pat, r) | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r) + | ( + ["livelit", "at", "in"], + [Pat({ids: [_var_id], term: Var(livelit_name)}), Typ(typ)], + ) => + LivelitDef({name: livelit_name, expansion_type: typ, body: r}) | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) => If(cond, conseq, r) | _ => hole(tm) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 9f902fa560..ef86e7099b 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -442,6 +442,7 @@ and uexp_to_info_map = ); | LivelitDef(livelit_record) => atomic(Just(Term.utyp_to_ty(livelit_record.expansion_type))) // TODO: I don't actually know what I'm doing here. I just did something close to list literals. + | LivelitAp({livelit_name: _livelit_name}) => assert(false) // TODO | Match(scrut, rules) => let (ty_scrut, free_scrut, m_scrut) = go(~mode=Syn, scrut); let (pats, branches) = List.split(rules); diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 0620e609aa..037d3c4fe8 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -360,7 +360,8 @@ module UExp = { | UnOp(op, _) => UnOp(op) | BinOp(op, _, _) => BinOp(op) | Match(_) => Match - | LivelitDef(_) => LivelitDef; + | LivelitDef(_) => LivelitDef + | LivelitAp(_) => LivelitAp; let show_op_un_int: op_un_int => string = fun @@ -437,7 +438,8 @@ module UExp = { | BinOp(op) => show_binop(op) | UnOp(op) => show_unop(op) | Match => "Match Expression" - | LivelitDef => "Livelit Definition"; + | LivelitDef => "Livelit Definition" + | LivelitAp => "Livelit Application"; let rec is_fun = (e: t) => { switch (e.term) { @@ -464,6 +466,7 @@ module UExp = { | BinOp(_) | Match(_) | LivelitDef(_) + | LivelitAp(_) | Tag(_) => false }; }; @@ -495,6 +498,7 @@ module UExp = { | BinOp(_) | Match(_) | LivelitDef(_) + | LivelitAp(_) | Tag(_) => false } ); diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index a310c85bac..fe3ab74674 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -88,8 +88,9 @@ and UExp: { type livelit_record = { name: string, expansion_type: UTyp.t, - init: UExp.t, + // init: UExp.t, // TODO: The rest of the stuff + body: UExp.t, }; [@deriving (show({with_path: false}), sexp, yojson)] type cls = @@ -116,7 +117,8 @@ and UExp: { | UnOp(op_un) | BinOp(op_bin) | Match - | LivelitDef; + | LivelitDef + | LivelitAp; [@deriving (show({with_path: false}), sexp, yojson)] type term = @@ -145,6 +147,7 @@ and UExp: { | BinOp(op_bin, t, t) | Match(t, list((UPat.t, t))) | LivelitDef(livelit_record) + | LivelitAp({livelit_name: string}) and t = { // invariant: nonempty ids: list(Id.t), @@ -205,7 +208,8 @@ and UExp: { type livelit_record = { name: string, expansion_type: UTyp.t, - init: UExp.t, + // init: UExp.t + body: UExp.t, }; [@deriving (show({with_path: false}), sexp, yojson)] @@ -233,7 +237,8 @@ and UExp: { | UnOp(op_un) | BinOp(op_bin) | Match - | LivelitDef; + | LivelitDef + | LivelitAp; [@deriving (show({with_path: false}), sexp, yojson)] type term = @@ -262,6 +267,7 @@ and UExp: { | BinOp(op_bin, t, t) | Match(t, list((UPat.t, t))) | LivelitDef(livelit_record) + | LivelitAp({livelit_name: string}) and t = { // invariant: nonempty ids: list(Id.t), diff --git a/src/haz3lweb/LangDocMessages.re b/src/haz3lweb/LangDocMessages.re index 5a14fecc35..9cc42bc702 100644 --- a/src/haz3lweb/LangDocMessages.re +++ b/src/haz3lweb/LangDocMessages.re @@ -2497,6 +2497,32 @@ let str_eq_exp: form = { let livelit_def_exp_group = "livelit_def_exp_group"; +let livelit_def_exp: form = { + let explanation = {message: "Livelit Definition", feedback: Unselected}; + let form = []; + { + id: "livelit_def_exp", + syntactic_form: form, + expandable_id: None, + explanation, + examples: [], + }; +}; + +let livelit_ap_exp_group = "livelit_ap_exp_group"; + +let livelit_ap_exp: form = { + let explanation = {message: "Livelit Application", feedback: Unselected}; + let form = []; + { + id: "livelit_ap_exp", + syntactic_form: form, + expandable_id: None, + explanation, + examples: [], + }; +}; + let case_exp_group = "case_exp_group"; let case_rules_group = "case_rules_group"; let case_example_wild_simple = { @@ -3190,6 +3216,7 @@ let get_group = (group_id, doc: t) => { }; let get_form_and_options = (group_id, doc: t) => { + print_endline(group_id); let form_group = get_group(group_id, doc); let (selected_id, _) = List.nth(form_group.options, form_group.current_selection); @@ -3279,6 +3306,8 @@ let init = { function_tuple3_exp, function_tag_exp, function_ap_exp, + livelit_ap_exp, + livelit_def_exp, tuple_exp, tuple_exp_size2, tuple_exp_size3, @@ -3510,6 +3539,14 @@ let init = { ), ]), ), + ( + livelit_ap_exp_group, + init_options([(livelit_ap_exp.id, [pat("p")])]), + ), + ( + livelit_def_exp_group, + init_options([(livelit_def_exp.id, [pat("p")])]), + ), (tuple_exp_group, init_options([(tuple_exp.id, [])])), ( tuple_exp_2_group, diff --git a/src/haz3lweb/view/LangDoc.re b/src/haz3lweb/view/LangDoc.re index 6b6b9fa863..9503cb24f0 100644 --- a/src/haz3lweb/view/LangDoc.re +++ b/src/haz3lweb/view/LangDoc.re @@ -2159,6 +2159,19 @@ let get_doc = doc.explanation.message, [], ); + | LivelitAp(_) => + let (doc, options) = + LangDocMessages.get_form_and_options( + LangDocMessages.livelit_ap_exp_group, + docs, + ); + get_message( + doc, + options, + LangDocMessages.livelit_ap_exp_group, + doc.explanation.message, + [], + ); }; get_message_exp(term.term); | Some(InfoPat({term, _})) => From 7dc7ae69e199419312d445d5ccd557efd1020ae0 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 12 Jan 2023 21:20:09 -0600 Subject: [PATCH 04/52] mock livelit application --- src/haz3lcore/dynamics/elaborator.re | 20 +++++++++++++------- src/haz3lcore/statics/MakeTerm.re | 26 ++++++++++++++++++++++++++ src/haz3lcore/statics/Statics.re | 8 +++++++- 3 files changed, 46 insertions(+), 8 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index 43bd62a0ea..ebb85e8561 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -54,9 +54,10 @@ let exp_binop_of: Term.UExp.op_bin => (Typ.t, (_, _) => DHExp.t) = ); let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) => { - print_endline(Term.UExp.show(uexp)); /* NOTE: Left out delta for now */ switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) { + // print_endline(Term.UExp.show(uexp)); + | Some(InfoExp({mode, self, _})) => let err_status = Statics.error_status(mode, self); let maybe_reason: option(ErrStatus.HoleReason.t) = @@ -298,14 +299,19 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) => | _ => wrap(ConsistentCase(d)) }; | LivelitDef(livelit_record) => - print_endline(TermBase.UExp.show_livelit_record(livelit_record)); + // print_endline(TermBase.UExp.show_livelit_record(livelit_record)); let foo = dhexp_of_uexp(m, livelit_record.body); // TODO abandukwala - switch (foo) { - | Some(t) => print_endline(DHExp.show(t)) - | None => print_endline("No value") - }; + // switch (foo) { + // | Some(t) => print_endline(DHExp.show(t)) + // | None => print_endline("No value") + // }; foo; - | LivelitAp({livelit_name: _}) => assert(false) // TODO + | LivelitAp({livelit_name}) => + switch (livelit_name) { + | "int" => Some(IntLit(1)) + | "str" => Some(StringLit("livelit string")) + | _ => None + } }; | Some(InfoPat(_) | InfoTyp(_) | InfoRul(_) | Invalid(_)) | None => None diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 93650b1b70..d63b11abea 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -211,6 +211,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { let ret = (tm: UExp.term) => (tm, []); let _unrecog = UExp.Invalid(UnrecognizedTerm); let hole = unsorted => Term.UExp.hole(kids_of_unsorted(unsorted)); + fun | Op(tiles) as tm => switch (tiles) { @@ -261,6 +262,31 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { ) | _ => ret(hole(tm)) } + | Pre(tiles, Pat(r)) as tm => { + print_endline("tiles: " ++ show_tiles(tiles)); + print_endline("r: " ++ UPat.show(r)); + + switch (tiles) { + | ([(_id, t)], []) => + let (foo, bar) = t; + List.iter(a => print_endline("a: " ++ a), foo); + List.iter(b => print_endline("b: " ++ show(b)), bar); + ret( + switch (t) { + | (["$"], []) => + switch (r.term) { + | Var(var_name) => + print_endline("Made livelit" ++ var_name); + LivelitAp({livelit_name: var_name}); + | _ => hole(tm) + } + | _ => hole(tm) + }, + ); + | _ => ret(hole(tm)) + }; + } + | Post(Exp(l), tiles) as tm => switch (tiles) { | ([(_id, t)], []) => diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index ef86e7099b..69ccc43200 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -442,7 +442,13 @@ and uexp_to_info_map = ); | LivelitDef(livelit_record) => atomic(Just(Term.utyp_to_ty(livelit_record.expansion_type))) // TODO: I don't actually know what I'm doing here. I just did something close to list literals. - | LivelitAp({livelit_name: _livelit_name}) => assert(false) // TODO + | LivelitAp({livelit_name}) => + print_endline("Statics for livelit: " ++ livelit_name); + switch (livelit_name) { + | "int" => atomic(Just(Int)) + | "str" => atomic(Just(String)) + | _ => atomic(Just(Unknown(TypeHole))) + }; | Match(scrut, rules) => let (ty_scrut, free_scrut, m_scrut) = go(~mode=Syn, scrut); let (pats, branches) = List.split(rules); From 142d2bd3f08319bdedf613b8c6c444b3d7cd3e56 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 19 Jan 2023 19:35:05 -0600 Subject: [PATCH 05/52] Started working on livelit application rather than definition --- src/haz3lcore/Measured.re | 11 +++++++++++ src/haz3lcore/dynamics/elaborator.re | 16 ++++++++-------- src/haz3lcore/statics/MakeTerm.re | 10 +++++----- src/haz3lcore/statics/Statics.re | 4 ++-- src/haz3lcore/statics/Term.re | 8 ++++---- src/haz3lcore/statics/TermBase.re | 8 ++++---- src/haz3lcore/tiles/Livelit.re | 4 ++++ src/haz3lweb/view/LangDoc.re | 26 +++++++++++++------------- 8 files changed, 51 insertions(+), 36 deletions(-) create mode 100644 src/haz3lcore/tiles/Livelit.re diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index f94966e628..54e28f8407 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -97,6 +97,7 @@ type t = { whitespace: Id.Map.t(measurement), rows: Rows.t, linebreaks: Id.Map.t(rel_indent), + livelits: Id.Map.t(measurement), }; let empty = { @@ -105,6 +106,7 @@ let empty = { whitespace: Id.Map.empty, rows: Rows.empty, linebreaks: Id.Map.empty, + livelits: Id.Map.empty, }; let add_s = (id: Id.t, i: int, m, map) => { @@ -143,6 +145,11 @@ let add_w = (w: Whitespace.t, m, map) => { ...map, whitespace: map.whitespace |> Id.Map.add(w.id, m), }; + +let add_l = (l: Livelit.t, m, map) => { + ...map, + livelits: map.livelits |> Id.Map.add(l.id, m), +}; let add_p = (p: Piece.t, m, map) => p |> Piece.get( @@ -187,6 +194,9 @@ let find_t = (t: Tile.t, map): measurement => { let last = List.assoc(Tile.r_shard(t), shards); {origin: first.origin, last: last.last}; }; +let find_l = (l: Livelit.t, map): measurement => + Id.Map.find(l.id, map.livelits); + // let find_a = ({shards: (l, r), _} as a: Ancestor.t, map) => // List.assoc(l @ r, Id.Map.find(a.id, map.tiles)); let find_p = (p: Piece.t, map): measurement => @@ -235,6 +245,7 @@ let union2 = (map: t, map': t) => { ), linebreaks: Id.Map.union((_, i, _) => Some(i), map.linebreaks, map'.linebreaks), + livelits: Id.Map.union((_, m, _) => Some(m), map.livelits, map'.livelits), }; let union = List.fold_left(union2, empty); diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index ebb85e8561..03cfd05305 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -298,14 +298,14 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) => Some(DHExp.InconsistentBranches(u, 0, d)) | _ => wrap(ConsistentCase(d)) }; - | LivelitDef(livelit_record) => - // print_endline(TermBase.UExp.show_livelit_record(livelit_record)); - let foo = dhexp_of_uexp(m, livelit_record.body); // TODO abandukwala - // switch (foo) { - // | Some(t) => print_endline(DHExp.show(t)) - // | None => print_endline("No value") - // }; - foo; + // | LivelitDef(livelit_record) => + // // print_endline(TermBase.UExp.show_livelit_record(livelit_record)); + // let foo = dhexp_of_uexp(m, livelit_record.body); // TODO abandukwala + // // switch (foo) { + // // | Some(t) => print_endline(DHExp.show(t)) + // // | None => print_endline("No value") + // // }; + // foo; | LivelitAp({livelit_name}) => switch (livelit_name) { | "int" => Some(IntLit(1)) diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index d63b11abea..5c53f55ea9 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -250,11 +250,11 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | (["-"], []) => UnOp(Int(Minus), r) | (["fun", "->"], [Pat(pat)]) => Fun(pat, r) | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r) - | ( - ["livelit", "at", "in"], - [Pat({ids: [_var_id], term: Var(livelit_name)}), Typ(typ)], - ) => - LivelitDef({name: livelit_name, expansion_type: typ, body: r}) + // | ( + // ["livelit", "at", "in"], + // [Pat({ids: [_var_id], term: Var(livelit_name)}), Typ(typ)], + // ) => + // LivelitDef({name: livelit_name, expansion_type: typ, body: r}) | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) => If(cond, conseq, r) | _ => hole(tm) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 69ccc43200..e838ce035c 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -440,8 +440,8 @@ 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]), ); - | LivelitDef(livelit_record) => - atomic(Just(Term.utyp_to_ty(livelit_record.expansion_type))) // TODO: I don't actually know what I'm doing here. I just did something close to list literals. + // | LivelitDef(livelit_record) => + // atomic(Just(Term.utyp_to_ty(livelit_record.expansion_type))) // TODO: I don't actually know what I'm doing here. I just did something close to list literals. | LivelitAp({livelit_name}) => print_endline("Statics for livelit: " ++ livelit_name); switch (livelit_name) { diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 037d3c4fe8..343b6ff95b 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -360,7 +360,7 @@ module UExp = { | UnOp(op, _) => UnOp(op) | BinOp(op, _, _) => BinOp(op) | Match(_) => Match - | LivelitDef(_) => LivelitDef + // | LivelitDef(_) => LivelitDef | LivelitAp(_) => LivelitAp; let show_op_un_int: op_un_int => string = @@ -438,7 +438,7 @@ module UExp = { | BinOp(op) => show_binop(op) | UnOp(op) => show_unop(op) | Match => "Match Expression" - | LivelitDef => "Livelit Definition" + // | LivelitDef => "Livelit Definition" | LivelitAp => "Livelit Application"; let rec is_fun = (e: t) => { @@ -465,7 +465,7 @@ module UExp = { | UnOp(_) | BinOp(_) | Match(_) - | LivelitDef(_) + // | LivelitDef(_) | LivelitAp(_) | Tag(_) => false }; @@ -497,7 +497,7 @@ module UExp = { | UnOp(_) | BinOp(_) | Match(_) - | LivelitDef(_) + // | LivelitDef(_) | LivelitAp(_) | Tag(_) => false } diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index fe3ab74674..c1678f5036 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -117,7 +117,7 @@ and UExp: { | UnOp(op_un) | BinOp(op_bin) | Match - | LivelitDef + // | LivelitDef | LivelitAp; [@deriving (show({with_path: false}), sexp, yojson)] @@ -146,7 +146,7 @@ and UExp: { | UnOp(op_un, t) | BinOp(op_bin, t, t) | Match(t, list((UPat.t, t))) - | LivelitDef(livelit_record) + // | LivelitDef(livelit_record) | LivelitAp({livelit_name: string}) and t = { // invariant: nonempty @@ -237,7 +237,7 @@ and UExp: { | UnOp(op_un) | BinOp(op_bin) | Match - | LivelitDef + // | LivelitDef | LivelitAp; [@deriving (show({with_path: false}), sexp, yojson)] @@ -266,7 +266,7 @@ and UExp: { | UnOp(op_un, t) | BinOp(op_bin, t, t) | Match(t, list((UPat.t, t))) - | LivelitDef(livelit_record) + // | LivelitDef(livelit_record) | LivelitAp({livelit_name: string}) and t = { // invariant: nonempty diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re new file mode 100644 index 0000000000..78542bfa87 --- /dev/null +++ b/src/haz3lcore/tiles/Livelit.re @@ -0,0 +1,4 @@ +[@deriving (show({with_path: false}), sexp, yojson)] +type t = {id: Id.t}; + +let id = w => w.id; diff --git a/src/haz3lweb/view/LangDoc.re b/src/haz3lweb/view/LangDoc.re index 9503cb24f0..f8014ee060 100644 --- a/src/haz3lweb/view/LangDoc.re +++ b/src/haz3lweb/view/LangDoc.re @@ -2146,19 +2146,19 @@ let get_doc = ), [], ); - | LivelitDef(_livelit_def) => - let (doc, options) = - LangDocMessages.get_form_and_options( - LangDocMessages.livelit_def_exp_group, - docs, - ); - get_message( - doc, - options, - LangDocMessages.livelit_def_exp_group, - doc.explanation.message, - [], - ); + // | LivelitDef(_livelit_def) => + // let (doc, options) = + // LangDocMessages.get_form_and_options( + // LangDocMessages.livelit_def_exp_group, + // docs, + // ); + // get_message( + // doc, + // options, + // LangDocMessages.livelit_def_exp_group, + // doc.explanation.message, + // [], + // ); | LivelitAp(_) => let (doc, options) = LangDocMessages.get_form_and_options( From 624aad0438eb793b2f50471e4b5ef38fa745c75e Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Fri, 20 Jan 2023 20:05:15 -0600 Subject: [PATCH 06/52] Add input boxes for int and str --- src/haz3lweb/view/Code.re | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 085fe8786f..e054d5dcfd 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -17,11 +17,17 @@ let of_delim' = | _ when !is_complete => "delim-incomplete" | _ => "delim" }; + let livelit_nodes: list(t) = + switch (label) { + | ["int"] => [Node.input(~attr=Attr.create("type", "range"), ())] + | ["str"] => [Node.input(~attr=Attr.create("type", "text"), ())] + | _ => [] + }; [ span( ~attr= Attr.classes(["token", cls, "text-" ++ Sort.to_string(sort)]), - [Node.text(List.nth(label, i))], + List.append([Node.text(List.nth(label, i))], livelit_nodes), ), ]; }, @@ -58,15 +64,16 @@ module Text = (M: { let rec of_segment = (~no_sorts=false, ~sort=Sort.root, seg: Segment.t): list(Node.t) => { //note: no_sorts flag is used for backback - let expected_sorts = + let expected_sorts: list((int, Sort.t)) = no_sorts ? List.init(List.length(seg), i => (i, Sort.Any)) : Segment.expected_sorts(sort, seg); - let sort_of_p_idx = idx => - switch (List.assoc_opt(idx, expected_sorts)) { - | None => Sort.Any - | Some(sort) => sort - }; + let sort_of_p_idx: int => Sort.t = + idx => + switch (List.assoc_opt(idx, expected_sorts)) { + | None => Sort.Any + | Some(sort) => sort + }; seg |> List.mapi((i, p) => (i, p)) |> List.concat_map(((i, p)) => of_piece(sort_of_p_idx(i), p)); @@ -140,7 +147,7 @@ let view = let map = measured; let settings = settings; }); - let unselected = + let unselected: list(t) = TimeUtil.measure_time("Code.view/unselected", settings.benchmark, () => Text.of_segment(unselected) ); From 93e00236dbb8f9169b4bb784c4ffa523d062ca9a Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 23 Jan 2023 20:36:23 -0600 Subject: [PATCH 07/52] Make livelit atomic form --- src/haz3lcore/dynamics/elaborator.re | 4 ++-- src/haz3lcore/lang/Form.re | 5 ++++- src/haz3lcore/statics/MakeTerm.re | 27 ++------------------------- src/haz3lcore/statics/Statics.re | 4 ++-- src/haz3lweb/view/Code.re | 6 ++++-- 5 files changed, 14 insertions(+), 32 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index 03cfd05305..0091b4927a 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -308,8 +308,8 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) => // foo; | LivelitAp({livelit_name}) => switch (livelit_name) { - | "int" => Some(IntLit(1)) - | "str" => Some(StringLit("livelit string")) + | "$int" => Some(IntLit(1)) + | "$str" => Some(StringLit("livelit string")) | _ => None } }; diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index c9e2874859..5cbb7cae9e 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -101,6 +101,9 @@ let is_bad_lit = str => there are at most two quotes, in order to prevent merges */ let is_string = t => regexp("^\".*\"$", t) && List.length(String.split_on_char('"', t)) < 4; + +let is_livelit = t => regexp("^\\$[a-z][A-Za-z0-9_]*$", t); + let string_delim = "\""; let is_string_delim = str => str == string_delim; @@ -131,6 +134,7 @@ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [ ("wild", (is_wild, [mk_op(Pat, [])])), ("listnil", (is_listnil, [mk_op(Exp, []), mk_op(Pat, [])])), ("string", (is_string, [mk_op(Exp, []), mk_op(Pat, [])])), + ("livelit", (is_livelit, [mk_op(Pat, [])])), ]; /* C. Compound Forms: @@ -187,7 +191,6 @@ let forms: list((string, t)) = [ "livelit_def", mk(ds, ["livelit", "at", "in"], mk_pre(P.let_, Exp, [Pat, Typ])) // TODO: How do we syntactically want to handle the rest of the information in haz3l ), - ("livelit_ap", mk(ss, ["$"], mk_pre(P.ap, Exp, [Pat]))), ("typeann", mk(ss, [":"], mk_bin'(P.ann, Pat, Pat, [], Typ))), ("case", mk(ds, ["case", "end"], mk_op(Exp, [Rul]))), ( diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 5c53f55ea9..7e819dabb5 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -224,6 +224,8 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | ([t], []) when Form.is_float(t) => ret(Float(float_of_string(t))) | ([t], []) when Form.is_int(t) => ret(Int(int_of_string(t))) | ([t], []) when Form.is_var(t) => ret(Var(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_tag(t) => ret(Tag(t)) | (["test", "end"], [Exp(test)]) => ret(Test(test)) @@ -262,31 +264,6 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { ) | _ => ret(hole(tm)) } - | Pre(tiles, Pat(r)) as tm => { - print_endline("tiles: " ++ show_tiles(tiles)); - print_endline("r: " ++ UPat.show(r)); - - switch (tiles) { - | ([(_id, t)], []) => - let (foo, bar) = t; - List.iter(a => print_endline("a: " ++ a), foo); - List.iter(b => print_endline("b: " ++ show(b)), bar); - ret( - switch (t) { - | (["$"], []) => - switch (r.term) { - | Var(var_name) => - print_endline("Made livelit" ++ var_name); - LivelitAp({livelit_name: var_name}); - | _ => hole(tm) - } - | _ => hole(tm) - }, - ); - | _ => ret(hole(tm)) - }; - } - | Post(Exp(l), tiles) as tm => switch (tiles) { | ([(_id, t)], []) => diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index e838ce035c..ee19752129 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -445,8 +445,8 @@ and uexp_to_info_map = | LivelitAp({livelit_name}) => print_endline("Statics for livelit: " ++ livelit_name); switch (livelit_name) { - | "int" => atomic(Just(Int)) - | "str" => atomic(Just(String)) + | "$int" => atomic(Just(Int)) + | "$str" => atomic(Just(String)) | _ => atomic(Just(Unknown(TypeHole))) }; | Match(scrut, rules) => diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index e054d5dcfd..6006b72c1a 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -17,10 +17,11 @@ let of_delim' = | _ when !is_complete => "delim-incomplete" | _ => "delim" }; + let livelit_nodes: list(t) = switch (label) { - | ["int"] => [Node.input(~attr=Attr.create("type", "range"), ())] - | ["str"] => [Node.input(~attr=Attr.create("type", "text"), ())] + | ["$int"] => [Node.input(~attr=Attr.create("type", "range"), ())] + | ["$str"] => [Node.input(~attr=Attr.create("type", "text"), ())] | _ => [] }; [ @@ -87,6 +88,7 @@ module Text = (M: { }; } and of_tile = (expected_sort: Sort.t, t: Tile.t): list(Node.t) => { + // print_endline("Tile:" ++ Tile.show(t)); let children_and_sorts = List.mapi( (i, (l, child, r)) => From aa6f72c9f529646222f41b7cc3054d32929b550d Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 26 Jan 2023 20:26:52 -0600 Subject: [PATCH 08/52] Switch livelits to use % over $ --- src/haz3lcore/dynamics/elaborator.re | 4 ++-- src/haz3lcore/lang/Form.re | 8 ++------ src/haz3lcore/statics/Statics.re | 4 ++-- src/haz3lweb/view/Code.re | 4 ++-- 4 files changed, 8 insertions(+), 12 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index ffcdcd309a..4503042a98 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -277,8 +277,8 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) => }; | LivelitAp({livelit_name}) => switch (livelit_name) { - | "$int" => Some(IntLit(1)) - | "$str" => Some(StringLit("livelit string")) + | "%int" => Some(IntLit(1)) + | "%str" => Some(StringLit("livelit string")) | _ => None } | Match(scrut, rules) => diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index fad77f71d9..c6624ca091 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -104,7 +104,7 @@ let is_bad_lit = str => let is_string = t => regexp("^\".*\"$", t) && List.length(String.split_on_char('"', t)) < 4; -let is_livelit = t => regexp("^\\$[a-z][A-Za-z0-9_]*$", t); +let is_livelit = t => regexp("^[%]\\([a-z][A-Za-z0-9_]*\\)?$", t); let string_delim = "\""; let is_string_delim = str => str == string_delim; @@ -137,7 +137,7 @@ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [ ("wild", (is_wild, [mk_op(Pat, [])])), ("listnil", (is_listnil, [mk_op(Exp, []), mk_op(Pat, [])])), ("string", (is_string, [mk_op(Exp, []), mk_op(Pat, [])])), - ("livelit", (is_livelit, [mk_op(Pat, [])])), + ("livelit", (is_livelit, [mk_op(Exp, [])])), ]; /* C. Compound Forms: @@ -191,10 +191,6 @@ let forms: list((string, t)) = [ ("ap_exp", mk(ii, ["(", ")"], mk_post(P.ap, Exp, [Exp]))), ("ap_pat", mk(ii, ["(", ")"], mk_post(P.ap, Pat, [Pat]))), ("let_", mk(ds, ["let", "=", "in"], mk_pre(P.let_, Exp, [Pat, Exp]))), - ( - "livelit_def", - mk(ds, ["livelit", "at", "in"], mk_pre(P.let_, Exp, [Pat, Typ])) // TODO: How do we syntactically want to handle the rest of the information in haz3l - ), ("typeann", mk(ss, [":"], mk_bin'(P.ann, Pat, Pat, [], Typ))), ("case", mk(ds, ["case", "end"], mk_op(Exp, [Rul]))), ( diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index a18a748bb9..961d7475a1 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -464,8 +464,8 @@ and uexp_to_info_map = | LivelitAp({livelit_name}) => print_endline("Statics for livelit: " ++ livelit_name); switch (livelit_name) { - | "$int" => atomic(Just(Int)) - | "$str" => atomic(Just(String)) + | "%int" => atomic(Just(Int)) + | "%str" => atomic(Just(String)) | _ => atomic(Just(Unknown(TypeHole))) }; | Match(scrut, rules) => diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 3037709bc6..731946d58d 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -20,8 +20,8 @@ let of_delim' = let livelit_nodes: list(t) = switch (label) { - | ["$int"] => [Node.input(~attr=Attr.create("type", "range"), ())] - | ["$str"] => [Node.input(~attr=Attr.create("type", "text"), ())] + | ["%int"] => [Node.input(~attr=Attr.create("type", "range"), ())] + | ["%str"] => [Node.input(~attr=Attr.create("type", "text"), ())] | _ => [] }; [ From 82d67fe0f1ad42721781232d85306b4bcc578546 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 26 Jan 2023 20:40:55 -0600 Subject: [PATCH 09/52] Add a fixed padding to slider livelit --- src/haz3lcore/Measured.re | 10 +++++++++- src/haz3lcore/statics/Statics.re | 3 +-- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index 037d6667a8..81d543db55 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -386,12 +386,20 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => { let map = map |> add_g(g, {origin, last}); (contained_indent, last, map); | Tile(t) => + let livelit_padding = + switch (t.label) { + | ["%int"] => 15 // TODO Pull off of livelit + | _ => 0 + }; let token = List.nth(t.label); let add_shard = (origin, shard, map) => { let last = Point.{ ...origin, - col: origin.col + String.length(token(shard)), + col: + origin.col + + String.length(token(shard)) + + livelit_padding, }; let map = map |> add_s(t.id, shard, {origin, last}); (last, map); diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 961d7475a1..68798363dd 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -462,12 +462,11 @@ and uexp_to_info_map = // | LivelitDef(livelit_record) => // atomic(Just(Term.utyp_to_ty(livelit_record.expansion_type))) // TODO: I don't actually know what I'm doing here. I just did something close to list literals. | LivelitAp({livelit_name}) => - print_endline("Statics for livelit: " ++ livelit_name); switch (livelit_name) { | "%int" => atomic(Just(Int)) | "%str" => atomic(Just(String)) | _ => atomic(Just(Unknown(TypeHole))) - }; + } | Match(scrut, rules) => let (ty_scrut, free_scrut, m_scrut) = go(~mode=Syn, scrut); let (pats, branches) = List.split(rules); From 5848c9f68dfbbd26b44b33780e95266f459b7055 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 31 Jan 2023 12:33:23 -0600 Subject: [PATCH 10/52] Switch livelit to caret --- src/haz3lcore/Measured.re | 2 +- src/haz3lcore/dynamics/elaborator.re | 4 ++-- src/haz3lcore/lang/Form.re | 2 +- src/haz3lcore/statics/Statics.re | 4 ++-- src/haz3lweb/view/Code.re | 4 ++-- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index 81d543db55..d7e38924e0 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -388,7 +388,7 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => { | Tile(t) => let livelit_padding = switch (t.label) { - | ["%int"] => 15 // TODO Pull off of livelit + | ["^int"] => 15 // TODO Pull off of livelit | _ => 0 }; let token = List.nth(t.label); diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index 4503042a98..4c1b2750e7 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -277,8 +277,8 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) => }; | LivelitAp({livelit_name}) => switch (livelit_name) { - | "%int" => Some(IntLit(1)) - | "%str" => Some(StringLit("livelit string")) + | "^int" => Some(IntLit(1)) + | "^str" => Some(StringLit("livelit string")) | _ => None } | Match(scrut, rules) => diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index c6624ca091..bb469acccd 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -104,7 +104,7 @@ let is_bad_lit = str => let is_string = t => regexp("^\".*\"$", t) && List.length(String.split_on_char('"', t)) < 4; -let is_livelit = t => regexp("^[%]\\([a-z][A-Za-z0-9_]*\\)?$", t); +let is_livelit = t => regexp("^[\\^]\\([a-z][A-Za-z0-9_]*\\)?$", t); let string_delim = "\""; let is_string_delim = str => str == string_delim; diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 68798363dd..3093267162 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -463,8 +463,8 @@ and uexp_to_info_map = // atomic(Just(Term.utyp_to_ty(livelit_record.expansion_type))) // TODO: I don't actually know what I'm doing here. I just did something close to list literals. | LivelitAp({livelit_name}) => switch (livelit_name) { - | "%int" => atomic(Just(Int)) - | "%str" => atomic(Just(String)) + | "^int" => atomic(Just(Int)) + | "^str" => atomic(Just(String)) | _ => atomic(Just(Unknown(TypeHole))) } | Match(scrut, rules) => diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 731946d58d..c36958e0c5 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -20,8 +20,8 @@ let of_delim' = let livelit_nodes: list(t) = switch (label) { - | ["%int"] => [Node.input(~attr=Attr.create("type", "range"), ())] - | ["%str"] => [Node.input(~attr=Attr.create("type", "text"), ())] + | ["^int"] => [Node.input(~attr=Attr.create("type", "range"), ())] + | ["^str"] => [Node.input(~attr=Attr.create("type", "text"), ())] | _ => [] }; [ From 0018e1f247bf3d5cc7fd662c0705a4b37cca55d7 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 31 Jan 2023 14:45:13 -0600 Subject: [PATCH 11/52] Fix padding code --- src/haz3lcore/Measured.re | 2 +- src/haz3lcore/dynamics/elaborator.re | 2 +- src/haz3lcore/statics/MakeTerm.re | 2 +- src/haz3lcore/statics/Statics.re | 2 +- src/haz3lcore/statics/TermBase.re | 10 ++++++++-- src/haz3lweb/view/Code.re | 26 +++++++++++++++++++++++--- 6 files changed, 35 insertions(+), 9 deletions(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index d7e38924e0..bcdb184d4c 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -388,7 +388,7 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => { | Tile(t) => let livelit_padding = switch (t.label) { - | ["^int"] => 15 // TODO Pull off of livelit + | ["^int"] => 10 // TODO Pull of livelit | _ => 0 }; let token = List.nth(t.label); diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index 4c1b2750e7..23430dfbc5 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -275,7 +275,7 @@ 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}) => + | LivelitAp({livelit_name, width: _}) => switch (livelit_name) { | "^int" => Some(IntLit(1)) | "^str" => Some(StringLit("livelit string")) diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index bc89c05d7e..ad78758df3 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -225,7 +225,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | ([t], []) when Form.is_int(t) => ret(Int(int_of_string(t))) | ([t], []) when Form.is_var(t) => ret(Var(t)) | ([t], []) when Form.is_livelit(t) => - ret(LivelitAp({livelit_name: t})) + ret(LivelitAp({livelit_name: t, width: 10})) // Context | ([t], []) when Form.is_string(t) => ret(String(t)) | ([t], []) when Form.is_tag(t) => ret(Tag(t)) | (["test", "end"], [Exp(test)]) => ret(Test(test)) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 3093267162..80987114fe 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -461,7 +461,7 @@ and uexp_to_info_map = ); // | LivelitDef(livelit_record) => // atomic(Just(Term.utyp_to_ty(livelit_record.expansion_type))) // TODO: I don't actually know what I'm doing here. I just did something close to list literals. - | LivelitAp({livelit_name}) => + | LivelitAp({livelit_name, width: _}) => switch (livelit_name) { | "^int" => atomic(Just(Int)) | "^str" => atomic(Just(String)) diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index 1ac4a5b2ca..1bb86bbefe 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -147,7 +147,10 @@ and UExp: { | BinOp(op_bin, t, t) | Match(t, list((UPat.t, t))) // | LivelitDef(livelit_record) - | LivelitAp({livelit_name: string}) + | LivelitAp({ + livelit_name: string, + width: int, + }) and t = { // invariant: nonempty ids: list(Id.t), @@ -267,7 +270,10 @@ and UExp: { | BinOp(op_bin, t, t) | Match(t, list((UPat.t, t))) // | LivelitDef(livelit_record) - | LivelitAp({livelit_name: string}) + | LivelitAp({ + livelit_name: string, + width: int, + }) and t = { // invariant: nonempty ids: list(Id.t), diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index c36958e0c5..f4478a3a2d 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -17,10 +17,30 @@ let of_delim' = | _ when !is_complete => "delim-incomplete" | _ => "delim" }; + // TODO FontMetrics + let font_height = 10.0; + let font_width = 10.0; + let livelit_width = 10.0; // TODO Pull from livelit - let livelit_nodes: list(t) = + let style = + Printf.sprintf( + "width: %fpx; height: %fpx;", + livelit_width ** font_width, + font_height, + ); + + let livelit_node: list(t) = switch (label) { - | ["^int"] => [Node.input(~attr=Attr.create("type", "range"), ())] + | ["^int"] => [ + Node.input( + ~attr= + Attr.many([ + Attr.create("type", "range"), + Attr.create("style", style), + ]), + (), + ), + ] | ["^str"] => [Node.input(~attr=Attr.create("type", "text"), ())] | _ => [] }; @@ -28,7 +48,7 @@ let of_delim' = span( ~attr= Attr.classes(["token", cls, "text-" ++ Sort.to_string(sort)]), - List.append([Node.text(List.nth(label, i))], livelit_nodes), + List.append([Node.text(List.nth(label, i))], livelit_node), ), ]; }, From e6dbcef27a00d9d7c191f6d491701263a6ca0e99 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 31 Jan 2023 15:07:24 -0600 Subject: [PATCH 12/52] Fix floating multiplication --- src/haz3lweb/view/Code.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index f4478a3a2d..82cc29de2f 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -25,7 +25,7 @@ let of_delim' = let style = Printf.sprintf( "width: %fpx; height: %fpx;", - livelit_width ** font_width, + livelit_width *. font_width, font_height, ); From 9f4a0d5d2b52047735d669091236498cd2cf6eaf Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Tue, 31 Jan 2023 15:15:24 -0600 Subject: [PATCH 13/52] Add style for text input --- src/haz3lcore/Measured.re | 1 + src/haz3lweb/view/Code.re | 11 ++++++++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index bcdb184d4c..ec1d4996e2 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -389,6 +389,7 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => { let livelit_padding = switch (t.label) { | ["^int"] => 10 // TODO Pull of livelit + | ["^str"] => 10 // TODO Pull of livelit | _ => 0 }; let token = List.nth(t.label); diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 82cc29de2f..b3b449cab7 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -41,7 +41,16 @@ let of_delim' = (), ), ] - | ["^str"] => [Node.input(~attr=Attr.create("type", "text"), ())] + | ["^str"] => [ + Node.input( + ~attr= + Attr.many([ + Attr.create("type", "text"), + Attr.create("style", style), + ]), + (), + ), + ] | _ => [] }; [ From fc21785fbd64372f2b4494e02176e5ff974ce667 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 2 Feb 2023 18:21:31 -0600 Subject: [PATCH 14/52] Hack for persisting slider state --- src/haz3lcore/zipper/Editor.re | 6 ++- src/haz3lweb/Log.re | 1 + src/haz3lweb/Update.re | 19 ++++++++ src/haz3lweb/UpdateAction.re | 3 +- src/haz3lweb/view/BackpackView.re | 8 +++- src/haz3lweb/view/Cell.re | 10 ++++- src/haz3lweb/view/Code.re | 72 +++++++++++++++++++++++++------ src/haz3lweb/view/LangDoc.re | 16 +++++-- 8 files changed, 114 insertions(+), 21 deletions(-) diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index 70d7f76542..ddb4c1f20e 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -7,6 +7,7 @@ module Meta = { measured: Measured.t, term_ranges: TermRanges.t, col_target: int, + livelit_state: int // TODO Replace with map of id to state or somehting }; let init = (z: Zipper.t) => { @@ -16,6 +17,7 @@ module Meta = { measured: Measured.of_segment(unselected), term_ranges: TermRanges.mk(unselected), col_target: 0, + livelit_state: 50, }; }; @@ -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, livelit_state, _} = 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, livelit_state}; }; }; diff --git a/src/haz3lweb/Log.re b/src/haz3lweb/Log.re index 1fb6aee273..8994a2489a 100644 --- a/src/haz3lweb/Log.re +++ b/src/haz3lweb/Log.re @@ -37,6 +37,7 @@ let is_action_logged: UpdateAction.t => bool = | Undo | Redo | MoveToNextHole(_) + | LivelitStateChange(_) | UpdateLangDocMessages(_) => true; let storage_key = "LOG_" ++ SchoolSettings.log_key; diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index 97a575f919..ab30926bcb 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -170,6 +170,7 @@ let reevaluate_post_update = | Cut | Paste(_) | Undo + | LivelitStateChange(_) | Redo => true; let evaluate_and_schedule = @@ -415,6 +416,24 @@ let apply = | DebugAction(a) => DebugAction.perform(a); Ok(model); + | LivelitStateChange(livelit_state) => + let (id, ed) = Editors.get_editor_and_id(model.editors); + let editor = + Editors.put_editor_and_id( + id, + { + ...ed, + state: { + ...ed.state, + meta: { + ...ed.state.meta, + livelit_state, + }, + }, + }, + model.editors, + ); + Ok({...model, editors: editor}); }; reevaluate_post_update(update) ? m |> Result.map(~f=evaluate_and_schedule(state, ~schedule_action)) : m; diff --git a/src/haz3lweb/UpdateAction.re b/src/haz3lweb/UpdateAction.re index 5e99b62eca..724596b86f 100644 --- a/src/haz3lweb/UpdateAction.re +++ b/src/haz3lweb/UpdateAction.re @@ -42,7 +42,8 @@ type t = | MoveToNextHole(Direction.t) | UpdateResult(ModelResults.Key.t, ModelResult.current) | UpdateLangDocMessages(LangDocMessages.update) - | DebugAction(DebugAction.t); + | DebugAction(DebugAction.t) + | LivelitStateChange(int); module Failure = { [@deriving (show({with_path: false}), sexp, yojson)] diff --git a/src/haz3lweb/view/BackpackView.re b/src/haz3lweb/view/BackpackView.re index b10cd24724..ac567651b7 100644 --- a/src/haz3lweb/view/BackpackView.re +++ b/src/haz3lweb/view/BackpackView.re @@ -32,7 +32,13 @@ let backpack_sel_view = ), ]), // zwsp necessary for containing box to stretch to contain trailing newline - Text.of_segment(~no_sorts=true, content) @ [text(Unicode.zwsp)], + Text.of_segment( + ~no_sorts=true, + content, + ~inject=_ => Ui_effect.Ignore, + ~livelit_state=0, + ) // TODO Livelit state + @ [text(Unicode.zwsp)], ); }; diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re index 4dd25aa037..106b68ca7c 100644 --- a/src/haz3lweb/view/Cell.re +++ b/src/haz3lweb/view/Cell.re @@ -274,7 +274,15 @@ let editor_view = let unselected = Zipper.unselect_and_zip(zipper); let measured = editor.state.meta.measured; let code_base_view = - Code.view(~font_metrics, ~segment, ~unselected, ~measured, ~settings); + Code.view( + ~font_metrics, + ~segment, + ~unselected, + ~measured, + ~settings, + ~inject, + ~livelit_state=editor.state.meta.livelit_state, + ); let deco_view = deco( ~zipper, diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index b3b449cab7..3d2605bbda 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -7,7 +7,7 @@ open Util.Web; let of_delim' = Core.Memo.general( ~cache_size_bound=100000, - ((sort, is_consistent, is_complete, label, i)) => { + ((sort, is_consistent, is_complete, label, i, inject, livelit_state)) => { let cls = switch (label) { | [_] when !is_consistent => "mono-inconsistent" @@ -28,7 +28,11 @@ let of_delim' = livelit_width *. font_width, font_height, ); + let callback = (_evt, str): Virtual_dom.Vdom.Effect.t(unit) => { + inject(UpdateAction.LivelitStateChange(int_of_string(str))); + }; + let attr: Attr.t = Attr.on_input(callback); let livelit_node: list(t) = switch (label) { | ["^int"] => [ @@ -37,6 +41,8 @@ let of_delim' = Attr.many([ Attr.create("type", "range"), Attr.create("style", style), + Attr.create("value", string_of_int(livelit_state)), + attr, ]), (), ), @@ -47,6 +53,7 @@ let of_delim' = Attr.many([ Attr.create("type", "text"), Attr.create("style", style), + attr, ]), (), ), @@ -63,8 +70,24 @@ let of_delim' = }, ); let of_delim = - (sort: Sort.t, is_consistent, t: Piece.tile, i: int): list(Node.t) => - of_delim'((sort, is_consistent, Tile.is_complete(t), t.label, i)); + ( + sort: Sort.t, + is_consistent, + t: Piece.tile, + i: int, + ~inject, + ~livelit_state, + ) + : list(Node.t) => + of_delim'(( + sort, + is_consistent, + Tile.is_complete(t), + t.label, + i, + inject, + livelit_state, + )); let of_grout = [Node.text(Unicode.nbsp)]; @@ -94,7 +117,14 @@ module Text = (M: { }) => { let m = p => Measured.find_p(p, M.map); let rec of_segment = - (~no_sorts=false, ~sort=Sort.root, seg: Segment.t): list(Node.t) => { + ( + ~no_sorts=false, + ~sort=Sort.root, + seg: Segment.t, + ~inject, + ~livelit_state, + ) + : list(Node.t) => { //note: no_sorts flag is used for backback let expected_sorts: list((int, Sort.t)) = no_sorts @@ -108,17 +138,23 @@ module Text = (M: { }; seg |> List.mapi((i, p) => (i, p)) - |> List.concat_map(((i, p)) => of_piece(sort_of_p_idx(i), p)); + |> List.concat_map(((i, p)) => + of_piece(sort_of_p_idx(i), p, ~inject, ~livelit_state) + ); } - and of_piece = (expected_sort: Sort.t, p: Piece.t): list(Node.t) => { + and of_piece = + (expected_sort: Sort.t, p: Piece.t, ~inject, ~livelit_state) + : list(Node.t) => { switch (p) { - | Tile(t) => of_tile(expected_sort, t) + | Tile(t) => of_tile(expected_sort, t, ~inject, ~livelit_state) | Grout(_) => of_grout | Secondary({content, _}) => of_secondary((M.settings.secondary_icons, m(p).last.col, content)) }; } - and of_tile = (expected_sort: Sort.t, t: Tile.t): list(Node.t) => { + and of_tile = + (expected_sort: Sort.t, t: Tile.t, ~inject, ~livelit_state) + : list(Node.t) => { // print_endline("Tile:" ++ Tile.show(t)); let children_and_sorts = List.mapi( @@ -129,8 +165,10 @@ module Text = (M: { ); let is_consistent = Sort.consistent(t.mold.out, expected_sort); Aba.mk(t.shards, children_and_sorts) - |> Aba.join(of_delim(t.mold.out, is_consistent, t), ((seg, sort)) => - of_segment(~sort, seg) + |> Aba.join( + of_delim(t.mold.out, is_consistent, t, ~inject, ~livelit_state), + ((seg, sort)) => + of_segment(~sort, seg, ~inject, ~livelit_state) ) |> List.concat; }; @@ -154,7 +192,8 @@ let rec holes = ], ); -let simple_view = (~unselected, ~map, ~settings: Model.settings): Node.t => { +let simple_view = + (~unselected, ~map, ~settings: Model.settings, ~inject): Node.t => { module Text = Text({ let map = map; @@ -162,7 +201,12 @@ let simple_view = (~unselected, ~map, ~settings: Model.settings): Node.t => { }); div( ~attr=Attr.class_("code"), - [span_c("code-text", Text.of_segment(unselected))], + [ + span_c( + "code-text", + Text.of_segment(unselected, ~inject, ~livelit_state=0), + ), + ] // TODO livelit_state ); }; @@ -173,6 +217,8 @@ let view = ~unselected, ~measured, ~settings: Model.settings, + ~inject, + ~livelit_state, ) : Node.t => { module Text = @@ -182,7 +228,7 @@ let view = }); let unselected: list(t) = TimeUtil.measure_time("Code.view/unselected", settings.benchmark, () => - Text.of_segment(unselected) + Text.of_segment(unselected, ~inject, ~livelit_state) ); let holes = TimeUtil.measure_time("Code.view/holes", settings.benchmark, () => diff --git a/src/haz3lweb/view/LangDoc.re b/src/haz3lweb/view/LangDoc.re index f8014ee060..c23c7c62d7 100644 --- a/src/haz3lweb/view/LangDoc.re +++ b/src/haz3lweb/view/LangDoc.re @@ -273,7 +273,12 @@ let deco = (index, (id, segment)) => { let map = Measured.of_segment(segment); let code_view = - Code.simple_view(~unselected=segment, ~map, ~settings); + Code.simple_view( + ~unselected=segment, + ~map, + ~settings, + ~inject, + ); let classes = get_clss(segment); id == form_id ? Node.div( @@ -378,7 +383,7 @@ let syntactic_form_view = ~form_id, ) => { let map = Measured.of_segment(unselected); - let code_view = Code.simple_view(~unselected, ~map, ~settings); + let code_view = Code.simple_view(~unselected, ~map, ~settings, ~inject); let deco_view = deco( ~doc, @@ -415,7 +420,12 @@ let example_view = ({term, message, _} as example: LangDocMessages.example) => { let map_code = Measured.of_segment(term); let code_view = - Code.simple_view(~unselected=term, ~map=map_code, ~settings); + Code.simple_view( + ~unselected=term, + ~map=map_code, + ~settings, + ~inject, + ); let (uhexp, _) = MakeTerm.go(term); let info_map = Statics.mk_map(uhexp); let result_view = From 788110165317f70c0df38b5d87761b89b5adc5cb Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 2 Feb 2023 18:49:00 -0600 Subject: [PATCH 15/52] Stop memoizing function with function parameter --- src/haz3lweb/view/Code.re | 115 +++++++++++++++++++------------------- 1 file changed, 56 insertions(+), 59 deletions(-) diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 3d2605bbda..4ac0238dda 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -5,70 +5,67 @@ open Util; open Util.Web; let of_delim' = - Core.Memo.general( - ~cache_size_bound=100000, ((sort, is_consistent, is_complete, label, i, inject, livelit_state)) => { - let cls = - switch (label) { - | [_] when !is_consistent => "mono-inconsistent" - | [s] when Form.is_string(s) => "mono-string-lit" - | [_] => "mono" - | _ when !is_consistent => "delim-inconsistent" - | _ when !is_complete => "delim-incomplete" - | _ => "delim" - }; - // TODO FontMetrics - let font_height = 10.0; - let font_width = 10.0; - let livelit_width = 10.0; // TODO Pull from livelit + let cls = + switch (label) { + | [_] when !is_consistent => "mono-inconsistent" + | [s] when Form.is_string(s) => "mono-string-lit" + | [_] => "mono" + | _ when !is_consistent => "delim-inconsistent" + | _ when !is_complete => "delim-incomplete" + | _ => "delim" + }; + // TODO FontMetrics + let font_height = 10.0; + let font_width = 10.0; + let livelit_width = 10.0; // TODO Pull from livelit - let style = - Printf.sprintf( - "width: %fpx; height: %fpx;", - livelit_width *. font_width, - font_height, - ); - let callback = (_evt, str): Virtual_dom.Vdom.Effect.t(unit) => { - inject(UpdateAction.LivelitStateChange(int_of_string(str))); - }; + let style = + Printf.sprintf( + "width: %fpx; height: %fpx;", + livelit_width *. font_width, + font_height, + ); + let callback = (_evt, str): Virtual_dom.Vdom.Effect.t(unit) => { + inject(UpdateAction.LivelitStateChange(int_of_string(str))); + }; - let attr: Attr.t = Attr.on_input(callback); - let livelit_node: list(t) = - switch (label) { - | ["^int"] => [ - Node.input( - ~attr= - Attr.many([ - Attr.create("type", "range"), - Attr.create("style", style), - Attr.create("value", string_of_int(livelit_state)), - attr, - ]), - (), - ), - ] - | ["^str"] => [ - Node.input( - ~attr= - Attr.many([ - Attr.create("type", "text"), - Attr.create("style", style), - attr, - ]), - (), - ), - ] - | _ => [] - }; - [ - span( + let attr: Attr.t = Attr.on_input(callback); + let livelit_node: list(t) = + switch (label) { + | ["^int"] => [ + Node.input( ~attr= - Attr.classes(["token", cls, "text-" ++ Sort.to_string(sort)]), - List.append([Node.text(List.nth(label, i))], livelit_node), + Attr.many([ + Attr.create("type", "range"), + Attr.create("style", style), + Attr.create("value", string_of_int(livelit_state)), + attr, + ]), + (), ), - ]; - }, - ); + ] + | ["^str"] => [ + Node.input( + ~attr= + Attr.many([ + Attr.create("type", "text"), + Attr.create("style", style), + attr, + ]), + (), + ), + ] + | _ => [] + }; + [ + span( + ~attr=Attr.classes(["token", cls, "text-" ++ Sort.to_string(sort)]), + List.append([Node.text(List.nth(label, i))], livelit_node), + ), + ]; +}; + let of_delim = ( sort: Sort.t, From 04eb7fb9e11983f96f77cce513e6b68c05c2c1e7 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 2 Feb 2023 19:35:42 -0600 Subject: [PATCH 16/52] Wire slider state into elaborator --- src/haz3lcore/dynamics/elaborator.re | 57 ++++++++++++++++------------ src/haz3lcore/prog/Interface.re | 4 +- src/haz3lweb/ScratchSlide.re | 11 +++++- src/haz3lweb/view/Cell.re | 6 ++- 4 files changed, 49 insertions(+), 29 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index 23430dfbc5..d677c14391 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/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, livelit_state: int) + : option(DHExp.t) => { /* NOTE: Left out delta for now */ switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) { // print_endline(Term.UExp.show(uexp)); @@ -172,20 +174,23 @@ 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, _, livelit_state)) + |> 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, livelit_state); 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, livelit_state); [d, ...ds]; }, es, @@ -194,24 +199,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, livelit_state); + let+ dc2 = dhexp_of_uexp(m, e2, livelit_state); DHExp.Cons(dc1, dc2); | UnOp(Int(Minus), e) => - let+ dc = dhexp_of_uexp(m, e); + let+ dc = dhexp_of_uexp(m, e, livelit_state); 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, livelit_state); + let+ dc2 = dhexp_of_uexp(m, e2, livelit_state); cons(dc1, dc2); - | Parens(e) => dhexp_of_uexp(m, e) + | Parens(e) => dhexp_of_uexp(m, e, livelit_state) | Seq(e1, e2) => - let* d1 = dhexp_of_uexp(m, e1); - let+ d2 = dhexp_of_uexp(m, e2); + let* d1 = dhexp_of_uexp(m, e1, livelit_state); + let+ d2 = dhexp_of_uexp(m, e2, livelit_state); DHExp.Sequence(d1, d2); | Test(test) => - let+ dtest = dhexp_of_uexp(m, test); + let+ dtest = dhexp_of_uexp(m, test, livelit_state); DHExp.Ap(TestLit(id), dtest); | Var(name) => switch (err_status) { @@ -226,8 +231,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, livelit_state); + let+ dbody = dhexp_of_uexp(m, body, livelit_state); let ty = Statics.pat_self_typ(m, p); switch (Term.UPat.get_recursive_bindings(p)) { | None => @@ -260,13 +265,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, livelit_state); + let+ c_arg = dhexp_of_uexp(m, arg, livelit_state); 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, livelit_state); + let* d1 = dhexp_of_uexp(m, e1, livelit_state); + let+ d2 = dhexp_of_uexp(m, e2, livelit_state); let d_rules = DHExp.[Rule(BoolLit(true), d1), Rule(BoolLit(false), d2)]; let d = DHExp.Case(d_scrut, d_rules, 0); @@ -277,17 +282,17 @@ let rec dhexp_of_uexp = (m: Statics.map, uexp: Term.UExp.t): option(DHExp.t) => }; | LivelitAp({livelit_name, width: _}) => switch (livelit_name) { - | "^int" => Some(IntLit(1)) + | "^int" => Some(IntLit(livelit_state)) | "^str" => Some(StringLit("livelit string")) | _ => None } | Match(scrut, rules) => - let* d_scrut = dhexp_of_uexp(m, scrut); + let* d_scrut = dhexp_of_uexp(m, scrut, livelit_state); 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, livelit_state); DHExp.Rule(d_p, d_e); }, rules, @@ -380,8 +385,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, livelit_state: int) + : ElaborationResult.t => + switch (dhexp_of_uexp(m, uexp, livelit_state)) { | None => DoesNotElaborate | Some(d) => let d = uexp_elab_wrap_builtins(d); diff --git a/src/haz3lcore/prog/Interface.re b/src/haz3lcore/prog/Interface.re index cc156ed05c..da59f267b2 100644 --- a/src/haz3lcore/prog/Interface.re +++ b/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 = (~livelit_state=0, map, term): DHExp.t => + switch (Elaborator.uexp_elab(map, term, livelit_state)) { | DoesNotElaborate => print_endline("Interface.elaborate EXCEPTION"); //HACK(andrew): supress exceptions for release diff --git a/src/haz3lweb/ScratchSlide.re b/src/haz3lweb/ScratchSlide.re index 374358077e..1c85f638c8 100644 --- a/src/haz3lweb/ScratchSlide.re +++ b/src/haz3lweb/ScratchSlide.re @@ -17,7 +17,16 @@ let spliced_elabs = ((_, editor)) => { let seg = Editor.get_seg(editor); let (term, _) = MakeTerm.go(seg); let info_map = Statics.mk_map(term); - [(scratch_key, Interface.elaborate(info_map, term))]; + [ + ( + scratch_key, + Interface.elaborate( + info_map, + term, + ~livelit_state=editor.state.meta.livelit_state, + ), + ), + ]; }; let persist = ((id, editor: Editor.t)) => { diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re index 106b68ca7c..58b0659cf4 100644 --- a/src/haz3lweb/view/Cell.re +++ b/src/haz3lweb/view/Cell.re @@ -318,7 +318,11 @@ let get_elab = (editor: Editor.t): DHExp.t => { let seg = Editor.get_seg(editor); let (term, _) = MakeTerm.go(seg); let info_map = Statics.mk_map(term); - Interface.elaborate(info_map, term); + Interface.elaborate( + info_map, + term, + ~livelit_state=editor.state.meta.livelit_state, + ); }; let editor_with_result_view = From 4da8970ecb84f7e6d9b3ff1106381cbb6a723b0f Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Fri, 3 Feb 2023 21:24:38 -0600 Subject: [PATCH 17/52] Add livelit_state map --- src/haz3lcore/dynamics/elaborator.re | 14 +++++++--- src/haz3lcore/prog/Interface.re | 2 +- src/haz3lcore/zipper/Editor.re | 4 +-- src/haz3lweb/Update.re | 9 +++++-- src/haz3lweb/UpdateAction.re | 2 +- src/haz3lweb/view/BackpackView.re | 2 +- src/haz3lweb/view/Code.re | 39 +++++++++++++++++++++------- 7 files changed, 52 insertions(+), 20 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index d677c14391..d96bc4b14a 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -136,7 +136,7 @@ let wrap = (u, mode, self, d: DHExp.t): option(DHExp.t) => }; let rec dhexp_of_uexp = - (m: Statics.map, uexp: Term.UExp.t, livelit_state: int) + (m: Statics.map, uexp: Term.UExp.t, livelit_state: Id.Map.t(int)) : option(DHExp.t) => { /* NOTE: Left out delta for now */ switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) { @@ -281,11 +281,17 @@ let rec dhexp_of_uexp = | _ => ConsistentCase(d) }; | LivelitAp({livelit_name, width: _}) => + let id = Term.UExp.rep_id(uexp); + let livelit_value = + switch (Id.Map.find_opt(id, livelit_state)) { + | Some(v) => v + | None => 50 + }; switch (livelit_name) { - | "^int" => Some(IntLit(livelit_state)) + | "^int" => Some(IntLit(livelit_value)) | "^str" => Some(StringLit("livelit string")) | _ => None - } + }; | Match(scrut, rules) => let* d_scrut = dhexp_of_uexp(m, scrut, livelit_state); let+ d_rules = @@ -386,7 +392,7 @@ let uexp_elab_wrap_builtins = (d: DHExp.t): DHExp.t => ); let uexp_elab = - (m: Statics.map, uexp: Term.UExp.t, livelit_state: int) + (m: Statics.map, uexp: Term.UExp.t, livelit_state: Id.Map.t(int)) : ElaborationResult.t => switch (dhexp_of_uexp(m, uexp, livelit_state)) { | None => DoesNotElaborate diff --git a/src/haz3lcore/prog/Interface.re b/src/haz3lcore/prog/Interface.re index da59f267b2..35e009f4be 100644 --- a/src/haz3lcore/prog/Interface.re +++ b/src/haz3lcore/prog/Interface.re @@ -1,5 +1,5 @@ exception DoesNotElaborate; -let elaborate = (~livelit_state=0, map, term): DHExp.t => +let elaborate = (~livelit_state=Id.Map.empty, map, term): DHExp.t => switch (Elaborator.uexp_elab(map, term, livelit_state)) { | DoesNotElaborate => print_endline("Interface.elaborate EXCEPTION"); diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index ddb4c1f20e..572a6f694b 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -7,7 +7,7 @@ module Meta = { measured: Measured.t, term_ranges: TermRanges.t, col_target: int, - livelit_state: int // TODO Replace with map of id to state or somehting + livelit_state: Id.Map.t(int) // TODO Replace int with actual types for livelit states }; let init = (z: Zipper.t) => { @@ -17,7 +17,7 @@ module Meta = { measured: Measured.of_segment(unselected), term_ranges: TermRanges.mk(unselected), col_target: 0, - livelit_state: 50, + livelit_state: Id.Map.empty, }; }; diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index ab30926bcb..6398014b2d 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -416,7 +416,7 @@ let apply = | DebugAction(a) => DebugAction.perform(a); Ok(model); - | LivelitStateChange(livelit_state) => + | LivelitStateChange(livelit_id, livelit_state) => let (id, ed) = Editors.get_editor_and_id(model.editors); let editor = Editors.put_editor_and_id( @@ -427,7 +427,12 @@ let apply = ...ed.state, meta: { ...ed.state.meta, - livelit_state, + livelit_state: + Id.Map.add( + livelit_id, + livelit_state, + ed.state.meta.livelit_state, + ), }, }, }, diff --git a/src/haz3lweb/UpdateAction.re b/src/haz3lweb/UpdateAction.re index 724596b86f..8c07167455 100644 --- a/src/haz3lweb/UpdateAction.re +++ b/src/haz3lweb/UpdateAction.re @@ -43,7 +43,7 @@ type t = | UpdateResult(ModelResults.Key.t, ModelResult.current) | UpdateLangDocMessages(LangDocMessages.update) | DebugAction(DebugAction.t) - | LivelitStateChange(int); + | LivelitStateChange(Id.t, int); module Failure = { [@deriving (show({with_path: false}), sexp, yojson)] diff --git a/src/haz3lweb/view/BackpackView.re b/src/haz3lweb/view/BackpackView.re index ac567651b7..5057b8caae 100644 --- a/src/haz3lweb/view/BackpackView.re +++ b/src/haz3lweb/view/BackpackView.re @@ -36,7 +36,7 @@ let backpack_sel_view = ~no_sorts=true, content, ~inject=_ => Ui_effect.Ignore, - ~livelit_state=0, + ~livelit_state=Id.Map.empty, ) // TODO Livelit state @ [text(Unicode.zwsp)], ); diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 4ac0238dda..2f22a6cadd 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -5,7 +5,18 @@ open Util; open Util.Web; let of_delim' = - ((sort, is_consistent, is_complete, label, i, inject, livelit_state)) => { + ( + ( + sort, + is_consistent, + is_complete, + label, + i, + inject, + livelit_state: Id.Map.t(int), + tile_id: Id.t, + ), + ) => { let cls = switch (label) { | [_] when !is_consistent => "mono-inconsistent" @@ -27,7 +38,7 @@ let of_delim' = font_height, ); let callback = (_evt, str): Virtual_dom.Vdom.Effect.t(unit) => { - inject(UpdateAction.LivelitStateChange(int_of_string(str))); + inject(UpdateAction.LivelitStateChange(tile_id, int_of_string(str))); }; let attr: Attr.t = Attr.on_input(callback); @@ -39,7 +50,15 @@ let of_delim' = Attr.many([ Attr.create("type", "range"), Attr.create("style", style), - Attr.create("value", string_of_int(livelit_state)), + Attr.create( + "value", + string_of_int( + switch (Id.Map.find_opt(tile_id, livelit_state)) { + | Some(v) => v + | None => 50 + }, + ), + ), attr, ]), (), @@ -73,7 +92,7 @@ let of_delim = t: Piece.tile, i: int, ~inject, - ~livelit_state, + ~livelit_state: Id.Map.t(int), ) : list(Node.t) => of_delim'(( @@ -84,6 +103,7 @@ let of_delim = i, inject, livelit_state, + Tile.id(t), )); let of_grout = [Node.text(Unicode.nbsp)]; @@ -119,7 +139,7 @@ module Text = (M: { ~sort=Sort.root, seg: Segment.t, ~inject, - ~livelit_state, + ~livelit_state: Id.Map.t(int), ) : list(Node.t) => { //note: no_sorts flag is used for backback @@ -152,7 +172,7 @@ module Text = (M: { and of_tile = (expected_sort: Sort.t, t: Tile.t, ~inject, ~livelit_state) : list(Node.t) => { - // print_endline("Tile:" ++ Tile.show(t)); + print_endline("Tile:" ++ Tile.show(t)); let children_and_sorts = List.mapi( (i, (l, child, r)) => @@ -161,7 +181,8 @@ module Text = (M: { Aba.aba_triples(Aba.mk(t.shards, t.children)), ); let is_consistent = Sort.consistent(t.mold.out, expected_sort); - Aba.mk(t.shards, children_and_sorts) + let foo = Aba.mk(t.shards, children_and_sorts); + foo |> Aba.join( of_delim(t.mold.out, is_consistent, t, ~inject, ~livelit_state), ((seg, sort)) => @@ -201,7 +222,7 @@ let simple_view = [ span_c( "code-text", - Text.of_segment(unselected, ~inject, ~livelit_state=0), + Text.of_segment(unselected, ~inject, ~livelit_state=Id.Map.empty), ), ] // TODO livelit_state ); @@ -215,7 +236,7 @@ let view = ~measured, ~settings: Model.settings, ~inject, - ~livelit_state, + ~livelit_state: Id.Map.t(int), ) : Node.t => { module Text = From 24f9598c0d87c748866df4439f06a2a742e11eb4 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sat, 4 Feb 2023 11:10:48 -0600 Subject: [PATCH 18/52] Remove unused code --- src/haz3lcore/Measured.re | 10 ---------- src/haz3lcore/tiles/Livelit.re | 4 ---- 2 files changed, 14 deletions(-) delete mode 100644 src/haz3lcore/tiles/Livelit.re diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index ec1d4996e2..59277bdf9a 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -97,7 +97,6 @@ type t = { secondary: Id.Map.t(measurement), rows: Rows.t, linebreaks: Id.Map.t(rel_indent), - livelits: Id.Map.t(measurement), }; let empty = { @@ -106,7 +105,6 @@ let empty = { secondary: Id.Map.empty, rows: Rows.empty, linebreaks: Id.Map.empty, - livelits: Id.Map.empty, }; let add_s = (id: Id.t, i: int, m, map) => { @@ -146,10 +144,6 @@ let add_w = (w: Secondary.t, m, map) => { secondary: map.secondary |> Id.Map.add(w.id, m), }; -let add_l = (l: Livelit.t, m, map) => { - ...map, - livelits: map.livelits |> Id.Map.add(l.id, m), -}; let add_p = (p: Piece.t, m, map) => p |> Piece.get( @@ -194,9 +188,6 @@ let find_t = (t: Tile.t, map): measurement => { let last = List.assoc(Tile.r_shard(t), shards); {origin: first.origin, last: last.last}; }; -let find_l = (l: Livelit.t, map): measurement => - Id.Map.find(l.id, map.livelits); - // let find_a = ({shards: (l, r), _} as a: Ancestor.t, map) => // List.assoc(l @ r, Id.Map.find(a.id, map.tiles)); let find_p = (p: Piece.t, map): measurement => @@ -245,7 +236,6 @@ let union2 = (map: t, map': t) => { ), linebreaks: Id.Map.union((_, i, _) => Some(i), map.linebreaks, map'.linebreaks), - livelits: Id.Map.union((_, m, _) => Some(m), map.livelits, map'.livelits), }; let union = List.fold_left(union2, empty); diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re deleted file mode 100644 index 78542bfa87..0000000000 --- a/src/haz3lcore/tiles/Livelit.re +++ /dev/null @@ -1,4 +0,0 @@ -[@deriving (show({with_path: false}), sexp, yojson)] -type t = {id: Id.t}; - -let id = w => w.id; From 6961d6f1d72c6bc1a025a29e736cff5798ca22d7 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 5 Feb 2023 09:33:39 -0600 Subject: [PATCH 19/52] Switch livelit_state to DHExp --- src/haz3lcore/dynamics/elaborator.re | 10 +++++++--- src/haz3lcore/zipper/Editor.re | 2 +- src/haz3lweb/UpdateAction.re | 2 +- src/haz3lweb/view/Code.re | 18 ++++++++++-------- 4 files changed, 19 insertions(+), 13 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index d96bc4b14a..bd0690c2c5 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -136,7 +136,7 @@ let wrap = (u, mode, self, d: DHExp.t): option(DHExp.t) => }; let rec dhexp_of_uexp = - (m: Statics.map, uexp: Term.UExp.t, livelit_state: Id.Map.t(int)) + (m: Statics.map, uexp: Term.UExp.t, livelit_state: Id.Map.t(DHExp.t)) : option(DHExp.t) => { /* NOTE: Left out delta for now */ switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) { @@ -284,7 +284,11 @@ let rec dhexp_of_uexp = let id = Term.UExp.rep_id(uexp); let livelit_value = switch (Id.Map.find_opt(id, livelit_state)) { - | Some(v) => v + | Some(v) => + switch (v) { + | IntLit(i) => i + | _ => assert(false) + } | None => 50 }; switch (livelit_name) { @@ -392,7 +396,7 @@ let uexp_elab_wrap_builtins = (d: DHExp.t): DHExp.t => ); let uexp_elab = - (m: Statics.map, uexp: Term.UExp.t, livelit_state: Id.Map.t(int)) + (m: Statics.map, uexp: Term.UExp.t, livelit_state: Id.Map.t(DHExp.t)) : ElaborationResult.t => switch (dhexp_of_uexp(m, uexp, livelit_state)) { | None => DoesNotElaborate diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index 572a6f694b..575804fd54 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -7,7 +7,7 @@ module Meta = { measured: Measured.t, term_ranges: TermRanges.t, col_target: int, - livelit_state: Id.Map.t(int) // TODO Replace int with actual types for livelit states + livelit_state: Id.Map.t(DHExp.t), }; let init = (z: Zipper.t) => { diff --git a/src/haz3lweb/UpdateAction.re b/src/haz3lweb/UpdateAction.re index 8c07167455..aaa08084bc 100644 --- a/src/haz3lweb/UpdateAction.re +++ b/src/haz3lweb/UpdateAction.re @@ -43,7 +43,7 @@ type t = | UpdateResult(ModelResults.Key.t, ModelResult.current) | UpdateLangDocMessages(LangDocMessages.update) | DebugAction(DebugAction.t) - | LivelitStateChange(Id.t, int); + | LivelitStateChange(Id.t, DHExp.t); module Failure = { [@deriving (show({with_path: false}), sexp, yojson)] diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 2f22a6cadd..cc387cbd99 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -13,7 +13,7 @@ let of_delim' = label, i, inject, - livelit_state: Id.Map.t(int), + livelit_state: Id.Map.t(DHExp.t), tile_id: Id.t, ), ) => { @@ -38,7 +38,9 @@ let of_delim' = font_height, ); let callback = (_evt, str): Virtual_dom.Vdom.Effect.t(unit) => { - inject(UpdateAction.LivelitStateChange(tile_id, int_of_string(str))); + inject( + UpdateAction.LivelitStateChange(tile_id, IntLit(int_of_string(str))), + ); }; let attr: Attr.t = Attr.on_input(callback); @@ -54,8 +56,8 @@ let of_delim' = "value", string_of_int( switch (Id.Map.find_opt(tile_id, livelit_state)) { - | Some(v) => v - | None => 50 + | Some(IntLit(i)) => i + | _ => 50 }, ), ), @@ -68,7 +70,7 @@ let of_delim' = Node.input( ~attr= Attr.many([ - Attr.create("type", "text"), + Attr.create("type", "checkbox"), Attr.create("style", style), attr, ]), @@ -92,7 +94,7 @@ let of_delim = t: Piece.tile, i: int, ~inject, - ~livelit_state: Id.Map.t(int), + ~livelit_state: Id.Map.t(DHExp.t), ) : list(Node.t) => of_delim'(( @@ -139,7 +141,7 @@ module Text = (M: { ~sort=Sort.root, seg: Segment.t, ~inject, - ~livelit_state: Id.Map.t(int), + ~livelit_state: Id.Map.t(DHExp.t), ) : list(Node.t) => { //note: no_sorts flag is used for backback @@ -236,7 +238,7 @@ let view = ~measured, ~settings: Model.settings, ~inject, - ~livelit_state: Id.Map.t(int), + ~livelit_state: Id.Map.t(DHExp.t), ) : Node.t => { module Text = From acfdc88c04781d0f368d93224c91889684d5c43c Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 5 Feb 2023 10:23:17 -0600 Subject: [PATCH 20/52] Switch the livelit names and shrink the checkbox --- src/haz3lcore/Measured.re | 4 ++-- src/haz3lcore/dynamics/elaborator.re | 4 ++-- src/haz3lcore/statics/Statics.re | 4 ++-- src/haz3lweb/view/Code.re | 28 ++++++++++++++++++---------- 4 files changed, 24 insertions(+), 16 deletions(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index 59277bdf9a..11ad222e0a 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -378,8 +378,8 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => { | Tile(t) => let livelit_padding = switch (t.label) { - | ["^int"] => 10 // TODO Pull of livelit - | ["^str"] => 10 // TODO Pull of livelit + | ["^slider"] => 10 // TODO Pull of livelit + | ["^checkbox"] => 1 // TODO Pull of livelit | _ => 0 }; let token = List.nth(t.label); diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index bd0690c2c5..4759a60242 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -292,8 +292,8 @@ let rec dhexp_of_uexp = | None => 50 }; switch (livelit_name) { - | "^int" => Some(IntLit(livelit_value)) - | "^str" => Some(StringLit("livelit string")) + | "^slider" => Some(IntLit(livelit_value)) + | "^checkbox" => Some(StringLit("livelit string")) | _ => None }; | Match(scrut, rules) => diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 80987114fe..b079245789 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -463,8 +463,8 @@ and uexp_to_info_map = // atomic(Just(Term.utyp_to_ty(livelit_record.expansion_type))) // TODO: I don't actually know what I'm doing here. I just did something close to list literals. | LivelitAp({livelit_name, width: _}) => switch (livelit_name) { - | "^int" => atomic(Just(Int)) - | "^str" => atomic(Just(String)) + | "^slider" => atomic(Just(Int)) + | "^checkbox" => atomic(Just(String)) | _ => atomic(Just(Unknown(TypeHole))) } | Match(scrut, rules) => diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index cc387cbd99..00d6faee99 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -31,12 +31,6 @@ let of_delim' = let font_width = 10.0; let livelit_width = 10.0; // TODO Pull from livelit - let style = - Printf.sprintf( - "width: %fpx; height: %fpx;", - livelit_width *. font_width, - font_height, - ); let callback = (_evt, str): Virtual_dom.Vdom.Effect.t(unit) => { inject( UpdateAction.LivelitStateChange(tile_id, IntLit(int_of_string(str))), @@ -46,12 +40,19 @@ let of_delim' = let attr: Attr.t = Attr.on_input(callback); let livelit_node: list(t) = switch (label) { - | ["^int"] => [ + | ["^slider"] => [ Node.input( ~attr= Attr.many([ Attr.create("type", "range"), - Attr.create("style", style), + Attr.create( + "style", + Printf.sprintf( + "width: %fpx; height: %fpx;", + livelit_width *. font_width, + font_height, + ), + ), Attr.create( "value", string_of_int( @@ -66,12 +67,19 @@ let of_delim' = (), ), ] - | ["^str"] => [ + | ["^checkbox"] => [ Node.input( ~attr= Attr.many([ Attr.create("type", "checkbox"), - Attr.create("style", style), + Attr.create( + "style", + Printf.sprintf( + "width: %fpx; height: %fpx; margin: 0", + 1.0 *. font_width, + font_height, + ), + ), attr, ]), (), From 19a66cf2e55c88d7c138fe5d220a813e711c8edb Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 5 Feb 2023 11:56:57 -0600 Subject: [PATCH 21/52] Wired in checkbox state --- src/haz3lcore/dynamics/elaborator.re | 35 +++++++++++++------- src/haz3lcore/statics/Statics.re | 2 +- src/haz3lweb/view/Code.re | 48 ++++++++++++++++++++-------- 3 files changed, 59 insertions(+), 26 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index 4759a60242..2f9e8a2102 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -282,18 +282,31 @@ let rec dhexp_of_uexp = }; | LivelitAp({livelit_name, width: _}) => let id = Term.UExp.rep_id(uexp); - let livelit_value = - switch (Id.Map.find_opt(id, livelit_state)) { - | Some(v) => - switch (v) { - | IntLit(i) => i - | _ => assert(false) - } - | None => 50 - }; + switch (livelit_name) { - | "^slider" => Some(IntLit(livelit_value)) - | "^checkbox" => Some(StringLit("livelit string")) + | "^slider" => + let livelit_value = + switch (Id.Map.find_opt(id, livelit_state)) { + | Some(v) => + switch (v) { + | IntLit(i) => i + | _ => assert(false) + } + | None => 50 + }; + Some(IntLit(livelit_value)); + | "^checkbox" => + let livelit_value = + switch (Id.Map.find_opt(id, livelit_state)) { + | Some(v) => + switch (v) { + | BoolLit(b) => b + | _ => assert(false) + } + | None => false + }; + + Some(BoolLit(livelit_value)); | _ => None }; | Match(scrut, rules) => diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index b079245789..0f608bc1c5 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -464,7 +464,7 @@ and uexp_to_info_map = | LivelitAp({livelit_name, width: _}) => switch (livelit_name) { | "^slider" => atomic(Just(Int)) - | "^checkbox" => atomic(Just(String)) + | "^checkbox" => atomic(Just(Bool)) | _ => atomic(Just(Unknown(TypeHole))) } | Match(scrut, rules) => diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 00d6faee99..83296ac962 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -29,15 +29,7 @@ let of_delim' = // TODO FontMetrics let font_height = 10.0; let font_width = 10.0; - let livelit_width = 10.0; // TODO Pull from livelit - let callback = (_evt, str): Virtual_dom.Vdom.Effect.t(unit) => { - inject( - UpdateAction.LivelitStateChange(tile_id, IntLit(int_of_string(str))), - ); - }; - - let attr: Attr.t = Attr.on_input(callback); let livelit_node: list(t) = switch (label) { | ["^slider"] => [ @@ -49,7 +41,7 @@ let of_delim' = "style", Printf.sprintf( "width: %fpx; height: %fpx;", - livelit_width *. font_width, + 10.0 *. font_width, font_height, ), ), @@ -62,12 +54,40 @@ let of_delim' = }, ), ), - attr, + Attr.on_input((_evt, str) => + ( + { + inject( + UpdateAction.LivelitStateChange( + tile_id, + IntLit(int_of_string(str)), + ), + ); + }: + Virtual_dom.Vdom.Effect.t(unit) + ) + ), ]), (), ), ] - | ["^checkbox"] => [ + | ["^checkbox"] => + let checkbox_state: bool = + switch (Id.Map.find_opt(tile_id, livelit_state)) { + | Some(BoolLit(b)) => b + | _ => false + }; + let checkbox_callback: Attr.t = + Attr.on_change((_evt, _str) => { + inject( + UpdateAction.LivelitStateChange( + tile_id, + BoolLit(!checkbox_state), + ), + ) + }); + + [ Node.input( ~attr= Attr.many([ @@ -80,11 +100,12 @@ let of_delim' = font_height, ), ), - attr, + checkbox_state ? Attr.checked : Attr.create("foo", "bar"), + checkbox_callback, ]), (), ), - ] + ]; | _ => [] }; [ @@ -182,7 +203,6 @@ module Text = (M: { and of_tile = (expected_sort: Sort.t, t: Tile.t, ~inject, ~livelit_state) : list(Node.t) => { - print_endline("Tile:" ++ Tile.show(t)); let children_and_sorts = List.mapi( (i, (l, child, r)) => From 26ced8a0dabb43d8f6c3cf832ca4728bf4879e64 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 5 Feb 2023 21:29:29 -0600 Subject: [PATCH 22/52] Fix livelit LangDocMessages --- src/haz3lweb/LangDocMessages.re | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/haz3lweb/LangDocMessages.re b/src/haz3lweb/LangDocMessages.re index 1732b641ef..69e81182b7 100644 --- a/src/haz3lweb/LangDocMessages.re +++ b/src/haz3lweb/LangDocMessages.re @@ -2513,7 +2513,7 @@ let livelit_ap_exp_group = "livelit_ap_exp_group"; let livelit_ap_exp: form = { let explanation = {message: "Livelit Application", feedback: Unselected}; - let form = []; + let form = [exp("^slider")]; { id: "livelit_ap_exp", syntactic_form: form, @@ -3218,6 +3218,9 @@ let get_group = (group_id, doc: t) => { let get_form_and_options = (group_id, doc: t) => { print_endline(group_id); let form_group = get_group(group_id, doc); + print_endline( + Printf.sprintf("%s : %s", group_id, show_form_group(form_group)), + ); let (selected_id, _) = List.nth(form_group.options, form_group.current_selection); let form = List.find(({id, _}) => id == selected_id, doc.forms); @@ -3541,7 +3544,7 @@ let init = { ), ( livelit_ap_exp_group, - init_options([(livelit_ap_exp.id, [pat("p")])]), + init_options([(livelit_ap_exp.id, [exp("e")])]), ), ( livelit_def_exp_group, From d3a4af5f1b5ab5c7a5e39a4abfb4e25f24435555 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 9 Feb 2023 20:01:21 -0600 Subject: [PATCH 23/52] Stop propagating mouse down from livelit --- src/haz3lweb/view/Code.re | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 83296ac962..944542bd08 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -29,6 +29,11 @@ let of_delim' = // TODO FontMetrics let font_height = 10.0; let font_width = 10.0; + let stop_mousedown_propagation = + Attr.on_mousedown(evt => { + Js_of_ocaml.Dom_html.stopPropagation(evt); + Virtual_dom.Vdom.Effect.Ignore; + }); let livelit_node: list(t) = switch (label) { @@ -67,6 +72,7 @@ let of_delim' = Virtual_dom.Vdom.Effect.t(unit) ) ), + stop_mousedown_propagation, ]), (), ), @@ -102,6 +108,7 @@ let of_delim' = ), checkbox_state ? Attr.checked : Attr.create("foo", "bar"), checkbox_callback, + stop_mousedown_propagation, ]), (), ), From a93abbc468380290103bf048c504017dc977cd65 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 9 Feb 2023 20:51:37 -0600 Subject: [PATCH 24/52] Add livelit type and start integrating font metrics --- src/haz3lcore/dynamics/elaborator.re | 33 ++++------------ src/haz3lcore/tiles/Livelit.re | 19 +++++++++ src/haz3lweb/view/BackpackView.re | 12 +++++- src/haz3lweb/view/Code.re | 58 +++++++++++++++++++++++----- src/haz3lweb/view/LangDoc.re | 5 ++- 5 files changed, 89 insertions(+), 38 deletions(-) create mode 100644 src/haz3lcore/tiles/Livelit.re diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index 2f9e8a2102..5c1fcd4e93 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -282,32 +282,13 @@ let rec dhexp_of_uexp = }; | LivelitAp({livelit_name, width: _}) => let id = Term.UExp.rep_id(uexp); - - switch (livelit_name) { - | "^slider" => - let livelit_value = - switch (Id.Map.find_opt(id, livelit_state)) { - | Some(v) => - switch (v) { - | IntLit(i) => i - | _ => assert(false) - } - | None => 50 - }; - Some(IntLit(livelit_value)); - | "^checkbox" => - let livelit_value = - switch (Id.Map.find_opt(id, livelit_state)) { - | Some(v) => - switch (v) { - | BoolLit(b) => b - | _ => assert(false) - } - | None => false - }; - - Some(BoolLit(livelit_value)); - | _ => None + switch (Id.Map.find_opt(id, livelit_state)) { + | Some(t) => Some(t) + | None => + switch (Livelit.find_livelit(livelit_name)) { + | Some(l) => Some(l.default) + | None => None + } }; | Match(scrut, rules) => let* d_scrut = dhexp_of_uexp(m, scrut, livelit_state); diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re new file mode 100644 index 0000000000..8435cef2f7 --- /dev/null +++ b/src/haz3lcore/tiles/Livelit.re @@ -0,0 +1,19 @@ +open Sexplib.Std; + +[@deriving (show({with_path: false}), sexp, yojson)] +type t = { + name: string, + width: int, + default: DHExp.t, +}; + +let slider: t = {name: "^slider", width: 10, default: IntLit(50)}; + +let checkbox: t = {name: "^checkbox", width: 1, default: BoolLit(false)}; + +let find_livelit = (livelit_name: string): option(t) => + switch (livelit_name) { + | "^slider" => Some(slider) + | "^checkbox" => Some(checkbox) + | _ => None + }; diff --git a/src/haz3lweb/view/BackpackView.re b/src/haz3lweb/view/BackpackView.re index 5057b8caae..b63b041491 100644 --- a/src/haz3lweb/view/BackpackView.re +++ b/src/haz3lweb/view/BackpackView.re @@ -9,6 +9,7 @@ let backpack_sel_view = scale: float, opacity: float, {focus: _, content}: Selection.t, + ~font_metrics, ) => { module Text = Code.Text({ @@ -36,6 +37,7 @@ let backpack_sel_view = ~no_sorts=true, content, ~inject=_ => Ui_effect.Ignore, + ~font_metrics, ~livelit_state=Id.Map.empty, ) // TODO Livelit state @ [text(Unicode.zwsp)], @@ -101,7 +103,15 @@ let view = let scale = scale_fn(idx); let x_offset = x_fn(idx); let new_y_offset = y_offset -. dy_fn(idx, base_height); - let v = backpack_sel_view(x_offset, new_y_offset, scale, opacity, s); + let v = + backpack_sel_view( + x_offset, + new_y_offset, + scale, + opacity, + s, + ~font_metrics, + ); let new_idx = idx + 1; let new_opacity = opacity -. opacity_reduction; //TODO(andrew): am i making this difficult by going backwards? diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 944542bd08..8d4d868103 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -14,6 +14,7 @@ let of_delim' = i, inject, livelit_state: Id.Map.t(DHExp.t), + _font_metrics: FontMetrics.t, tile_id: Id.t, ), ) => { @@ -29,6 +30,7 @@ let of_delim' = // TODO FontMetrics let font_height = 10.0; let font_width = 10.0; + let stop_mousedown_propagation = Attr.on_mousedown(evt => { Js_of_ocaml.Dom_html.stopPropagation(evt); @@ -42,6 +44,7 @@ let of_delim' = ~attr= Attr.many([ Attr.create("type", "range"), + Attr.create("vertical-align", "middle"), Attr.create( "style", Printf.sprintf( @@ -131,6 +134,7 @@ let of_delim = i: int, ~inject, ~livelit_state: Id.Map.t(DHExp.t), + ~font_metrics: FontMetrics.t, ) : list(Node.t) => of_delim'(( @@ -141,6 +145,7 @@ let of_delim = i, inject, livelit_state, + font_metrics, Tile.id(t), )); @@ -177,6 +182,7 @@ module Text = (M: { ~sort=Sort.root, seg: Segment.t, ~inject, + ~font_metrics: FontMetrics.t, ~livelit_state: Id.Map.t(DHExp.t), ) : list(Node.t) => { @@ -194,21 +200,40 @@ module Text = (M: { seg |> List.mapi((i, p) => (i, p)) |> List.concat_map(((i, p)) => - of_piece(sort_of_p_idx(i), p, ~inject, ~livelit_state) + of_piece( + sort_of_p_idx(i), + p, + ~inject, + ~font_metrics, + ~livelit_state, + ) ); } and of_piece = - (expected_sort: Sort.t, p: Piece.t, ~inject, ~livelit_state) + ( + expected_sort: Sort.t, + p: Piece.t, + ~inject, + ~font_metrics, + ~livelit_state, + ) : list(Node.t) => { switch (p) { - | Tile(t) => of_tile(expected_sort, t, ~inject, ~livelit_state) + | Tile(t) => + of_tile(expected_sort, t, ~inject, ~font_metrics, ~livelit_state) | Grout(_) => of_grout | Secondary({content, _}) => of_secondary((M.settings.secondary_icons, m(p).last.col, content)) }; } and of_tile = - (expected_sort: Sort.t, t: Tile.t, ~inject, ~livelit_state) + ( + expected_sort: Sort.t, + t: Tile.t, + ~inject, + ~font_metrics, + ~livelit_state, + ) : list(Node.t) => { let children_and_sorts = List.mapi( @@ -221,9 +246,16 @@ module Text = (M: { let foo = Aba.mk(t.shards, children_and_sorts); foo |> Aba.join( - of_delim(t.mold.out, is_consistent, t, ~inject, ~livelit_state), + of_delim( + t.mold.out, + is_consistent, + t, + ~inject, + ~font_metrics, + ~livelit_state, + ), ((seg, sort)) => - of_segment(~sort, seg, ~inject, ~livelit_state) + of_segment(~sort, seg, ~inject, ~font_metrics, ~livelit_state) ) |> List.concat; }; @@ -248,7 +280,8 @@ let rec holes = ); let simple_view = - (~unselected, ~map, ~settings: Model.settings, ~inject): Node.t => { + (~unselected, ~map, ~settings: Model.settings, ~inject, ~font_metrics) + : Node.t => { module Text = Text({ let map = map; @@ -259,9 +292,14 @@ let simple_view = [ span_c( "code-text", - Text.of_segment(unselected, ~inject, ~livelit_state=Id.Map.empty), + Text.of_segment( + unselected, + ~inject, + ~font_metrics, + ~livelit_state=Id.Map.empty, + ), ), - ] // TODO livelit_state + ], ); }; @@ -283,7 +321,7 @@ let view = }); let unselected: list(t) = TimeUtil.measure_time("Code.view/unselected", settings.benchmark, () => - Text.of_segment(unselected, ~inject, ~livelit_state) + Text.of_segment(unselected, ~inject, ~font_metrics, ~livelit_state) ); let holes = TimeUtil.measure_time("Code.view/holes", settings.benchmark, () => diff --git a/src/haz3lweb/view/LangDoc.re b/src/haz3lweb/view/LangDoc.re index c23c7c62d7..d20063719d 100644 --- a/src/haz3lweb/view/LangDoc.re +++ b/src/haz3lweb/view/LangDoc.re @@ -278,6 +278,7 @@ let deco = ~map, ~settings, ~inject, + ~font_metrics, ); let classes = get_clss(segment); id == form_id @@ -383,7 +384,8 @@ let syntactic_form_view = ~form_id, ) => { let map = Measured.of_segment(unselected); - let code_view = Code.simple_view(~unselected, ~map, ~settings, ~inject); + let code_view = + Code.simple_view(~unselected, ~map, ~settings, ~inject, ~font_metrics); let deco_view = deco( ~doc, @@ -425,6 +427,7 @@ let example_view = ~map=map_code, ~settings, ~inject, + ~font_metrics, ); let (uhexp, _) = MakeTerm.go(term); let info_map = Statics.mk_map(uhexp); From a35bebda44f55f00df9a3d38cee941b4a6639b70 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 9 Feb 2023 21:06:29 -0600 Subject: [PATCH 25/52] Integrate font metrics --- src/haz3lweb/view/Code.re | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 8d4d868103..479380c155 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -14,7 +14,7 @@ let of_delim' = i, inject, livelit_state: Id.Map.t(DHExp.t), - _font_metrics: FontMetrics.t, + font_metrics: FontMetrics.t, tile_id: Id.t, ), ) => { @@ -27,9 +27,6 @@ let of_delim' = | _ when !is_complete => "delim-incomplete" | _ => "delim" }; - // TODO FontMetrics - let font_height = 10.0; - let font_width = 10.0; let stop_mousedown_propagation = Attr.on_mousedown(evt => { @@ -44,13 +41,12 @@ let of_delim' = ~attr= Attr.many([ Attr.create("type", "range"), - Attr.create("vertical-align", "middle"), Attr.create( "style", Printf.sprintf( - "width: %fpx; height: %fpx;", - 10.0 *. font_width, - font_height, + "width: %fpx; height: %fpx; margin: 0; vertical-align: bottom", + 10.0 *. font_metrics.col_width, + font_metrics.row_height, ), ), Attr.create( @@ -104,9 +100,9 @@ let of_delim' = Attr.create( "style", Printf.sprintf( - "width: %fpx; height: %fpx; margin: 0", - 1.0 *. font_width, - font_height, + "width: %fpx; height: %fpx; margin: 0; vertical-align: bottom", + 1.0 *. font_metrics.col_width, + font_metrics.row_height, ), ), checkbox_state ? Attr.checked : Attr.create("foo", "bar"), From 9061fcf521ff46f7c9bc049eff5a087a0a19680b Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 9 Feb 2023 21:15:15 -0600 Subject: [PATCH 26/52] Breakout LivelitView --- src/haz3lweb/view/Code.re | 88 ++---------------------------- src/haz3lweb/view/LivelitView.re | 92 ++++++++++++++++++++++++++++++++ 2 files changed, 96 insertions(+), 84 deletions(-) create mode 100644 src/haz3lweb/view/LivelitView.re diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 479380c155..cb08a62b07 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -28,96 +28,16 @@ let of_delim' = | _ => "delim" }; - let stop_mousedown_propagation = - Attr.on_mousedown(evt => { - Js_of_ocaml.Dom_html.stopPropagation(evt); - Virtual_dom.Vdom.Effect.Ignore; - }); - - let livelit_node: list(t) = + let livelit_nodes: list(t) = switch (label) { - | ["^slider"] => [ - Node.input( - ~attr= - Attr.many([ - Attr.create("type", "range"), - Attr.create( - "style", - Printf.sprintf( - "width: %fpx; height: %fpx; margin: 0; vertical-align: bottom", - 10.0 *. font_metrics.col_width, - font_metrics.row_height, - ), - ), - Attr.create( - "value", - string_of_int( - switch (Id.Map.find_opt(tile_id, livelit_state)) { - | Some(IntLit(i)) => i - | _ => 50 - }, - ), - ), - Attr.on_input((_evt, str) => - ( - { - inject( - UpdateAction.LivelitStateChange( - tile_id, - IntLit(int_of_string(str)), - ), - ); - }: - Virtual_dom.Vdom.Effect.t(unit) - ) - ), - stop_mousedown_propagation, - ]), - (), - ), - ] - | ["^checkbox"] => - let checkbox_state: bool = - switch (Id.Map.find_opt(tile_id, livelit_state)) { - | Some(BoolLit(b)) => b - | _ => false - }; - let checkbox_callback: Attr.t = - Attr.on_change((_evt, _str) => { - inject( - UpdateAction.LivelitStateChange( - tile_id, - BoolLit(!checkbox_state), - ), - ) - }); - - [ - Node.input( - ~attr= - Attr.many([ - Attr.create("type", "checkbox"), - Attr.create( - "style", - Printf.sprintf( - "width: %fpx; height: %fpx; margin: 0; vertical-align: bottom", - 1.0 *. font_metrics.col_width, - font_metrics.row_height, - ), - ), - checkbox_state ? Attr.checked : Attr.create("foo", "bar"), - checkbox_callback, - stop_mousedown_propagation, - ]), - (), - ), - ]; + | [name] => + LivelitView.view(font_metrics, inject, name, livelit_state, tile_id) | _ => [] }; [ span( ~attr=Attr.classes(["token", cls, "text-" ++ Sort.to_string(sort)]), - List.append([Node.text(List.nth(label, i))], livelit_node), + List.append([Node.text(List.nth(label, i))], livelit_nodes), ), ]; }; diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re new file mode 100644 index 0000000000..5ad363db86 --- /dev/null +++ b/src/haz3lweb/view/LivelitView.re @@ -0,0 +1,92 @@ +open Virtual_dom.Vdom; +open Haz3lcore; + +let stop_mousedown_propagation = + Attr.on_mousedown(evt => { + Js_of_ocaml.Dom_html.stopPropagation(evt); + Virtual_dom.Vdom.Effect.Ignore; + }); +let view = + ( + font_metrics: FontMetrics.t, + inject, + name, + livelit_state: Id.Map.t(DHExp.t), + tile_id, + ) => + switch (name) { + | "^slider" => [ + Node.input( + ~attr= + Attr.many([ + Attr.create("type", "range"), + Attr.create( + "style", + Printf.sprintf( + "width: %fpx; height: %fpx; margin: 0; vertical-align: bottom", + 10.0 *. font_metrics.col_width, + font_metrics.row_height, + ), + ), + Attr.create( + "value", + string_of_int( + switch (Id.Map.find_opt(tile_id, livelit_state)) { + | Some(IntLit(i)) => i + | _ => 50 + }, + ), + ), + Attr.on_input((_evt, str) => + ( + { + inject( + UpdateAction.LivelitStateChange( + tile_id, + IntLit(int_of_string(str)), + ), + ); + }: + Virtual_dom.Vdom.Effect.t(unit) + ) + ), + stop_mousedown_propagation, + ]), + (), + ), + ] + | "^checkbox" => + let checkbox_state: bool = + switch (Id.Map.find_opt(tile_id, livelit_state)) { + | Some(BoolLit(b)) => b + | _ => false + }; + let checkbox_callback: Attr.t = + Attr.on_change((_evt, _str) => { + inject( + UpdateAction.LivelitStateChange(tile_id, BoolLit(!checkbox_state)), + ) + }); + + [ + Node.input( + ~attr= + Attr.many([ + Attr.create("type", "checkbox"), + Attr.create( + "style", + Printf.sprintf( + "width: %fpx; height: %fpx; margin: 0; vertical-align: bottom", + 1.0 *. font_metrics.col_width, + font_metrics.row_height, + ), + ), + checkbox_state ? Attr.checked : Attr.create("foo", "bar"), + checkbox_callback, + stop_mousedown_propagation, + ]), + (), + ), + ]; + | _ => [] + }; From efef346ffc261261cafc84fae01b0c872e05a94d Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 9 Feb 2023 21:21:24 -0600 Subject: [PATCH 27/52] Simplify LivelitView --- src/haz3lweb/view/LivelitView.re | 46 +++++++++++++++----------------- 1 file changed, 22 insertions(+), 24 deletions(-) diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index 5ad363db86..85668663a7 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -6,6 +6,16 @@ let stop_mousedown_propagation = Js_of_ocaml.Dom_html.stopPropagation(evt); Virtual_dom.Vdom.Effect.Ignore; }); + +let livelit_style = (font_metrics: FontMetrics.t, livelit_width: int) => + Attr.create( + "style", + Printf.sprintf( + "width: %fpx; height: %fpx; margin: 0; vertical-align: bottom", + float_of_int(livelit_width) *. font_metrics.col_width, + font_metrics.row_height, + ), + ); let view = ( font_metrics: FontMetrics.t, @@ -13,21 +23,14 @@ let view = name, livelit_state: Id.Map.t(DHExp.t), tile_id, - ) => + ) => { switch (name) { | "^slider" => [ Node.input( ~attr= Attr.many([ Attr.create("type", "range"), - Attr.create( - "style", - Printf.sprintf( - "width: %fpx; height: %fpx; margin: 0; vertical-align: bottom", - 10.0 *. font_metrics.col_width, - font_metrics.row_height, - ), - ), + livelit_style(font_metrics, 10), Attr.create( "value", string_of_int( @@ -61,28 +64,22 @@ let view = | Some(BoolLit(b)) => b | _ => false }; - let checkbox_callback: Attr.t = - Attr.on_change((_evt, _str) => { - inject( - UpdateAction.LivelitStateChange(tile_id, BoolLit(!checkbox_state)), - ) - }); [ Node.input( ~attr= Attr.many([ Attr.create("type", "checkbox"), - Attr.create( - "style", - Printf.sprintf( - "width: %fpx; height: %fpx; margin: 0; vertical-align: bottom", - 1.0 *. font_metrics.col_width, - font_metrics.row_height, - ), - ), + livelit_style(font_metrics, 1), checkbox_state ? Attr.checked : Attr.create("foo", "bar"), - checkbox_callback, + Attr.on_change((_evt, _str) => { + inject( + UpdateAction.LivelitStateChange( + tile_id, + BoolLit(!checkbox_state), + ), + ) + }), stop_mousedown_propagation, ]), (), @@ -90,3 +87,4 @@ let view = ]; | _ => [] }; +}; From 0f090db1a29528a645de2fd3317667edb4092e97 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 9 Feb 2023 21:22:20 -0600 Subject: [PATCH 28/52] Remove superfulous code --- src/haz3lweb/view/LivelitView.re | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index 85668663a7..b15a26ef42 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -68,20 +68,22 @@ let view = [ Node.input( ~attr= - Attr.many([ - Attr.create("type", "checkbox"), - livelit_style(font_metrics, 1), - checkbox_state ? Attr.checked : Attr.create("foo", "bar"), - Attr.on_change((_evt, _str) => { - inject( - UpdateAction.LivelitStateChange( - tile_id, - BoolLit(!checkbox_state), - ), - ) - }), - stop_mousedown_propagation, - ]), + Attr.many( + [ + Attr.create("type", "checkbox"), + livelit_style(font_metrics, 1), + Attr.on_change((_evt, _str) => { + inject( + UpdateAction.LivelitStateChange( + tile_id, + BoolLit(!checkbox_state), + ), + ) + }), + stop_mousedown_propagation, + ] + @ (checkbox_state ? [Attr.checked] : []), + ), (), ), ]; From cd9b7f035f9b799434f013ea193714e7776b3669 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 9 Feb 2023 21:35:21 -0600 Subject: [PATCH 29/52] Code cleanup --- src/haz3lcore/Measured.re | 8 ++++++-- src/haz3lcore/dynamics/elaborator.re | 2 -- src/haz3lcore/statics/MakeTerm.re | 8 -------- src/haz3lcore/statics/Statics.re | 9 +++------ src/haz3lcore/statics/Term.re | 4 ---- src/haz3lcore/statics/TermBase.re | 16 ---------------- src/haz3lcore/tiles/Livelit.re | 15 +++++++++++++-- 7 files changed, 22 insertions(+), 40 deletions(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index 11ad222e0a..9ca92ed22e 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -378,10 +378,14 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => { | Tile(t) => let livelit_padding = switch (t.label) { - | ["^slider"] => 10 // TODO Pull of livelit - | ["^checkbox"] => 1 // TODO Pull of livelit + | [possible_livelit_name] => + switch (Livelit.find_livelit(possible_livelit_name)) { + | Some(ll) => ll.width + | None => 0 + } | _ => 0 }; + let token = List.nth(t.label); let add_shard = (origin, shard, map) => { let last = diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index 5c1fcd4e93..c6c0dfaff6 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -140,8 +140,6 @@ let rec dhexp_of_uexp = : option(DHExp.t) => { /* NOTE: Left out delta for now */ switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) { - // print_endline(Term.UExp.show(uexp)); - | Some(InfoExp({mode, self, _})) => let err_status = Statics.error_status(mode, self); let id = Term.UExp.rep_id(uexp); /* NOTE: using term uids for hole ids */ diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index ad78758df3..ee3bd1df7a 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -10,8 +10,6 @@ WARNING: This module is still structurally in flux. */ -// TODO Livelit Expression and Term - open Util; open Term; @@ -211,7 +209,6 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { let ret = (tm: UExp.term) => (tm, []); let _unrecog = UExp.Invalid(UnrecognizedTerm); let hole = unsorted => Term.UExp.hole(kids_of_unsorted(unsorted)); - fun | Op(tiles) as tm => switch (tiles) { @@ -252,11 +249,6 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | (["-"], []) => UnOp(Int(Minus), r) | (["fun", "->"], [Pat(pat)]) => Fun(pat, r) | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r) - // | ( - // ["livelit", "at", "in"], - // [Pat({ids: [_var_id], term: Var(livelit_name)}), Typ(typ)], - // ) => - // LivelitDef({name: livelit_name, expansion_type: typ, body: r}) | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) => If(cond, conseq, r) | _ => hole(tm) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 0f608bc1c5..95da395589 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -459,13 +459,10 @@ 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]), ); - // | LivelitDef(livelit_record) => - // atomic(Just(Term.utyp_to_ty(livelit_record.expansion_type))) // TODO: I don't actually know what I'm doing here. I just did something close to list literals. | LivelitAp({livelit_name, width: _}) => - switch (livelit_name) { - | "^slider" => atomic(Just(Int)) - | "^checkbox" => atomic(Just(Bool)) - | _ => atomic(Just(Unknown(TypeHole))) + 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); diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 343b6ff95b..b54e8c23e4 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -360,7 +360,6 @@ module UExp = { | UnOp(op, _) => UnOp(op) | BinOp(op, _, _) => BinOp(op) | Match(_) => Match - // | LivelitDef(_) => LivelitDef | LivelitAp(_) => LivelitAp; let show_op_un_int: op_un_int => string = @@ -438,7 +437,6 @@ module UExp = { | BinOp(op) => show_binop(op) | UnOp(op) => show_unop(op) | Match => "Match Expression" - // | LivelitDef => "Livelit Definition" | LivelitAp => "Livelit Application"; let rec is_fun = (e: t) => { @@ -465,7 +463,6 @@ module UExp = { | UnOp(_) | BinOp(_) | Match(_) - // | LivelitDef(_) | LivelitAp(_) | Tag(_) => false }; @@ -497,7 +494,6 @@ module UExp = { | UnOp(_) | BinOp(_) | Match(_) - // | LivelitDef(_) | LivelitAp(_) | Tag(_) => false } diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index 1bb86bbefe..ad7286bc0d 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -84,14 +84,6 @@ and UExp: { | Bool(op_bin_bool) | String(op_bin_string); - [@deriving (show({with_path: false}), sexp, yojson)] - type livelit_record = { - name: string, - expansion_type: UTyp.t, - // init: UExp.t, - // TODO: The rest of the stuff - body: UExp.t, - }; [@deriving (show({with_path: false}), sexp, yojson)] type cls = | Invalid @@ -207,14 +199,6 @@ and UExp: { | Bool(op_bin_bool) | String(op_bin_string); - [@deriving (show({with_path: false}), sexp, yojson)] - type livelit_record = { - name: string, - expansion_type: UTyp.t, - // init: UExp.t - body: UExp.t, - }; - [@deriving (show({with_path: false}), sexp, yojson)] type cls = | Invalid diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re index 8435cef2f7..6fd9c89c7c 100644 --- a/src/haz3lcore/tiles/Livelit.re +++ b/src/haz3lcore/tiles/Livelit.re @@ -5,11 +5,22 @@ type t = { name: string, width: int, default: DHExp.t, + expansion_type: Typ.t, }; -let slider: t = {name: "^slider", width: 10, default: IntLit(50)}; +let slider: t = { + name: "^slider", + width: 10, + default: IntLit(50), + expansion_type: Int, +}; -let checkbox: t = {name: "^checkbox", width: 1, default: BoolLit(false)}; +let checkbox: t = { + name: "^checkbox", + width: 1, + default: BoolLit(false), + expansion_type: Bool, +}; let find_livelit = (livelit_name: string): option(t) => switch (livelit_name) { From 0a77b4a5cb83bc0c310e4fe41e5e4384f6f3ccba Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 9 Feb 2023 21:40:21 -0600 Subject: [PATCH 30/52] More code cleanup --- src/haz3lcore/dynamics/elaborator.re | 2 +- src/haz3lcore/statics/MakeTerm.re | 2 +- src/haz3lcore/statics/Statics.re | 2 +- src/haz3lcore/statics/TermBase.re | 14 ++------------ src/haz3lweb/LangDocMessages.re | 4 ---- src/haz3lweb/view/Code.re | 3 +-- src/haz3lweb/view/LangDoc.re | 13 ------------- 7 files changed, 6 insertions(+), 34 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index c6c0dfaff6..e97ebb9b0d 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -278,7 +278,7 @@ let rec dhexp_of_uexp = DHExp.InconsistentBranches(id, 0, d) | _ => ConsistentCase(d) }; - | LivelitAp({livelit_name, width: _}) => + | LivelitAp({livelit_name}) => let id = Term.UExp.rep_id(uexp); switch (Id.Map.find_opt(id, livelit_state)) { | Some(t) => Some(t) diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index ee3bd1df7a..8b9529b4bc 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -222,7 +222,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | ([t], []) when Form.is_int(t) => ret(Int(int_of_string(t))) | ([t], []) when Form.is_var(t) => ret(Var(t)) | ([t], []) when Form.is_livelit(t) => - ret(LivelitAp({livelit_name: t, width: 10})) // Context + ret(LivelitAp({livelit_name: t})) | ([t], []) when Form.is_string(t) => ret(String(t)) | ([t], []) when Form.is_tag(t) => ret(Tag(t)) | (["test", "end"], [Exp(test)]) => ret(Test(test)) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 95da395589..d53a90944d 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -459,7 +459,7 @@ 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, width: _}) => + | LivelitAp({livelit_name}) => switch (Livelit.find_livelit(livelit_name)) { | Some(ll) => atomic(Just(ll.expansion_type)) | None => atomic(Just(Unknown(TypeHole))) diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index ad7286bc0d..2de44b2021 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -109,7 +109,6 @@ and UExp: { | UnOp(op_un) | BinOp(op_bin) | Match - // | LivelitDef | LivelitAp; [@deriving (show({with_path: false}), sexp, yojson)] @@ -138,11 +137,7 @@ and UExp: { | UnOp(op_un, t) | BinOp(op_bin, t, t) | Match(t, list((UPat.t, t))) - // | LivelitDef(livelit_record) - | LivelitAp({ - livelit_name: string, - width: int, - }) + | LivelitAp({livelit_name: string}) and t = { // invariant: nonempty ids: list(Id.t), @@ -224,7 +219,6 @@ and UExp: { | UnOp(op_un) | BinOp(op_bin) | Match - // | LivelitDef | LivelitAp; [@deriving (show({with_path: false}), sexp, yojson)] @@ -253,11 +247,7 @@ and UExp: { | UnOp(op_un, t) | BinOp(op_bin, t, t) | Match(t, list((UPat.t, t))) - // | LivelitDef(livelit_record) - | LivelitAp({ - livelit_name: string, - width: int, - }) + | LivelitAp({livelit_name: string}) and t = { // invariant: nonempty ids: list(Id.t), diff --git a/src/haz3lweb/LangDocMessages.re b/src/haz3lweb/LangDocMessages.re index 69e81182b7..03a8922f98 100644 --- a/src/haz3lweb/LangDocMessages.re +++ b/src/haz3lweb/LangDocMessages.re @@ -3216,11 +3216,7 @@ let get_group = (group_id, doc: t) => { }; let get_form_and_options = (group_id, doc: t) => { - print_endline(group_id); let form_group = get_group(group_id, doc); - print_endline( - Printf.sprintf("%s : %s", group_id, show_form_group(form_group)), - ); let (selected_id, _) = List.nth(form_group.options, form_group.current_selection); let form = List.find(({id, _}) => id == selected_id, doc.forms); diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index cb08a62b07..3dae93316d 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -159,8 +159,7 @@ module Text = (M: { Aba.aba_triples(Aba.mk(t.shards, t.children)), ); let is_consistent = Sort.consistent(t.mold.out, expected_sort); - let foo = Aba.mk(t.shards, children_and_sorts); - foo + Aba.mk(t.shards, children_and_sorts) |> Aba.join( of_delim( t.mold.out, diff --git a/src/haz3lweb/view/LangDoc.re b/src/haz3lweb/view/LangDoc.re index d20063719d..3ca39d7186 100644 --- a/src/haz3lweb/view/LangDoc.re +++ b/src/haz3lweb/view/LangDoc.re @@ -2159,19 +2159,6 @@ let get_doc = ), [], ); - // | LivelitDef(_livelit_def) => - // let (doc, options) = - // LangDocMessages.get_form_and_options( - // LangDocMessages.livelit_def_exp_group, - // docs, - // ); - // get_message( - // doc, - // options, - // LangDocMessages.livelit_def_exp_group, - // doc.explanation.message, - // [], - // ); | LivelitAp(_) => let (doc, options) = LangDocMessages.get_form_and_options( From 0495cc50adabd9d3a7447f71eaf258dc5d8fd9bd Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 16 Mar 2023 20:48:13 -0500 Subject: [PATCH 31/52] Add unknown livelits to bad_lit --- src/haz3lcore/lang/Form.re | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 7a774f2531..7d4a3e3aea 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -90,19 +90,28 @@ 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_]*)?$", 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 */ let is_string = t => regexp("^\".*\"$", t) && List.length(String.split_on_char('"', t)) < 4; -let is_livelit = t => regexp("^[\\^]\\([a-z][A-Za-z0-9_]*\\)?$", t); - let string_delim = "\""; let is_string_delim = (==)(string_delim); @@ -286,10 +295,10 @@ let is_delim = t => List.mem(t, delims); let is_valid_token = t => is_atomic(t) || is_secondary(t) || is_delim(t); let is_valid_char = t => - is_valid_token(t) - || is_string_delim(t) - || is_comment_delim(t) - || is_whitelisted_char(t); + is_valid_token(t) + || is_string_delim(t) + || is_comment_delim(t) + || is_whitelisted_char(t); let mk_atomic = (sort: Sort.t, t: Token.t) => { assert(is_atomic(t)); From 26709a8a1d1ad48d86d1ec1944f784fb31127176 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 16 Mar 2023 21:26:03 -0500 Subject: [PATCH 32/52] Extract Livelit.elaborate_livelit --- src/haz3lcore/dynamics/elaborator.re | 14 +++++--------- src/haz3lcore/lang/Form.re | 8 ++++---- src/haz3lcore/tiles/Livelit.re | 13 +++++++++++++ 3 files changed, 22 insertions(+), 13 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index e97ebb9b0d..865d36a1c6 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -279,15 +279,11 @@ let rec dhexp_of_uexp = | _ => ConsistentCase(d) }; | LivelitAp({livelit_name}) => - let id = Term.UExp.rep_id(uexp); - switch (Id.Map.find_opt(id, livelit_state)) { - | Some(t) => Some(t) - | None => - switch (Livelit.find_livelit(livelit_name)) { - | Some(l) => Some(l.default) - | None => None - } - }; + Livelit.elaborate_livelit( + livelit_name, + Term.UExp.rep_id(uexp), + livelit_state, + ) | Match(scrut, rules) => let* d_scrut = dhexp_of_uexp(m, scrut, livelit_state); let+ d_rules = diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 7d4a3e3aea..bcb236ad5b 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -295,10 +295,10 @@ let is_delim = t => List.mem(t, delims); let is_valid_token = t => is_atomic(t) || is_secondary(t) || is_delim(t); let is_valid_char = t => - is_valid_token(t) - || is_string_delim(t) - || is_comment_delim(t) - || is_whitelisted_char(t); + is_valid_token(t) + || is_string_delim(t) + || is_comment_delim(t) + || is_whitelisted_char(t); let mk_atomic = (sort: Sort.t, t: Token.t) => { assert(is_atomic(t)); diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re index 6fd9c89c7c..94d5c2ca81 100644 --- a/src/haz3lcore/tiles/Livelit.re +++ b/src/haz3lcore/tiles/Livelit.re @@ -28,3 +28,16 @@ let find_livelit = (livelit_name: string): option(t) => | "^checkbox" => Some(checkbox) | _ => None }; + +let elaborate_livelit = + (livelit_name: string, uexp_id: int, livelit_state: Id.Map.t(DHExp.t)) + : option(DHExp.t) => { + switch (Id.Map.find_opt(uexp_id, livelit_state)) { + | Some(t) => Some(t) + | None => + switch (find_livelit(livelit_name)) { + | Some(l) => Some(l.default) + | None => None + } + }; +}; From f4369b156db0618245ed50bd34436f8ad6d3f233 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 16 Mar 2023 21:31:05 -0500 Subject: [PATCH 33/52] Extract Livelit.state type --- src/haz3lcore/dynamics/elaborator.re | 4 ++-- src/haz3lcore/tiles/Livelit.re | 3 ++- src/haz3lcore/zipper/Editor.re | 2 +- src/haz3lweb/view/Code.re | 8 ++++---- src/haz3lweb/view/LivelitView.re | 2 +- 5 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index 865d36a1c6..af7afc0ca5 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -136,7 +136,7 @@ let wrap = (u, mode, self, d: DHExp.t): option(DHExp.t) => }; let rec dhexp_of_uexp = - (m: Statics.map, uexp: Term.UExp.t, livelit_state: Id.Map.t(DHExp.t)) + (m: Statics.map, uexp: Term.UExp.t, livelit_state: Livelit.state) : option(DHExp.t) => { /* NOTE: Left out delta for now */ switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) { @@ -384,7 +384,7 @@ let uexp_elab_wrap_builtins = (d: DHExp.t): DHExp.t => ); let uexp_elab = - (m: Statics.map, uexp: Term.UExp.t, livelit_state: Id.Map.t(DHExp.t)) + (m: Statics.map, uexp: Term.UExp.t, livelit_state: Livelit.state) : ElaborationResult.t => switch (dhexp_of_uexp(m, uexp, livelit_state)) { | None => DoesNotElaborate diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re index 94d5c2ca81..d5a6c607bc 100644 --- a/src/haz3lcore/tiles/Livelit.re +++ b/src/haz3lcore/tiles/Livelit.re @@ -8,6 +8,7 @@ type t = { expansion_type: Typ.t, }; +type state = Id.Map.t(DHExp.t); let slider: t = { name: "^slider", width: 10, @@ -30,7 +31,7 @@ let find_livelit = (livelit_name: string): option(t) => }; let elaborate_livelit = - (livelit_name: string, uexp_id: int, livelit_state: Id.Map.t(DHExp.t)) + (livelit_name: string, uexp_id: int, livelit_state: state) : option(DHExp.t) => { switch (Id.Map.find_opt(uexp_id, livelit_state)) { | Some(t) => Some(t) diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index 575804fd54..1938f9fb53 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -7,7 +7,7 @@ module Meta = { measured: Measured.t, term_ranges: TermRanges.t, col_target: int, - livelit_state: Id.Map.t(DHExp.t), + livelit_state: Livelit.state, }; let init = (z: Zipper.t) => { diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 2bd64a9c18..7406956339 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -13,7 +13,7 @@ let of_delim' = label, i, inject, - livelit_state: Id.Map.t(DHExp.t), + livelit_state: Livelit.state, font_metrics: FontMetrics.t, tile_id: Id.t, ), @@ -49,7 +49,7 @@ let of_delim = t: Piece.tile, i: int, ~inject, - ~livelit_state: Id.Map.t(DHExp.t), + ~livelit_state: Livelit.state, ~font_metrics: FontMetrics.t, ) : list(Node.t) => @@ -99,7 +99,7 @@ module Text = (M: { seg: Segment.t, ~inject, ~font_metrics: FontMetrics.t, - ~livelit_state: Id.Map.t(DHExp.t), + ~livelit_state: Livelit.state, ) : list(Node.t) => { //note: no_sorts flag is used for backback @@ -226,7 +226,7 @@ let view = ~measured, ~settings: ModelSettings.t, ~inject, - ~livelit_state: Id.Map.t(DHExp.t), + ~livelit_state: Livelit.state, ) : Node.t => { module Text = diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index b15a26ef42..f64ea39096 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -21,7 +21,7 @@ let view = font_metrics: FontMetrics.t, inject, name, - livelit_state: Id.Map.t(DHExp.t), + livelit_state: Livelit.state, tile_id, ) => { switch (name) { From 1e73d1f26b83abdc0395fc71ffb6569b72607650 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 16 Mar 2023 21:35:46 -0500 Subject: [PATCH 34/52] Extract Livelit.empty_state --- src/haz3lcore/tiles/Livelit.re | 1 + src/haz3lcore/zipper/Editor.re | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re index d5a6c607bc..16a5991c2c 100644 --- a/src/haz3lcore/tiles/Livelit.re +++ b/src/haz3lcore/tiles/Livelit.re @@ -9,6 +9,7 @@ type t = { }; type state = Id.Map.t(DHExp.t); +let empty_state: state = Id.Map.empty; let slider: t = { name: "^slider", width: 10, diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index 1938f9fb53..f06a4684ee 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -17,7 +17,7 @@ module Meta = { measured: Measured.of_segment(unselected), term_ranges: TermRanges.mk(unselected), col_target: 0, - livelit_state: Id.Map.empty, + livelit_state: Livelit.empty_state, }; }; From 0abde16e81a1f11a4a076b1ba2439cdc9ba5a3e7 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 19 Mar 2023 12:17:40 -0500 Subject: [PATCH 35/52] Simplify updating livelit_state for Editors --- src/haz3lcore/zipper/Editor.re | 11 +++++++++++ src/haz3lweb/Editors.re | 5 +++++ src/haz3lweb/Update.re | 24 +++++++----------------- 3 files changed, 23 insertions(+), 17 deletions(-) diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index f06a4684ee..1aa2fce468 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -174,3 +174,14 @@ let trailing_hole_ctx = (ed: t, info_map: Statics.map) => { }; }; }; + +let update_livelit_state = (f: Livelit.state => Livelit.state, ed: t): t => { + let new_state: State.t = { + ...ed.state, + meta: { + ...ed.state.meta, + livelit_state: f(ed.state.meta.livelit_state), + }, + }; + {...ed, state: new_state}; +}; diff --git a/src/haz3lweb/Editors.re b/src/haz3lweb/Editors.re index eafd68a308..651cdf309e 100644 --- a/src/haz3lweb/Editors.re +++ b/src/haz3lweb/Editors.re @@ -98,3 +98,8 @@ let cur_slide = (editors: t): int => | Scratch(n, _) | School(n, _, _) => n }; + +let update_editor = (f: Editor.t => Editor.t, editors: t): t => { + let (id, old_editor) = get_editor_and_id(editors); + put_editor_and_id(id, f(old_editor), editors); +}; diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index 1250b6d8b4..ed0986c557 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -427,27 +427,17 @@ let apply = DebugAction.perform(a); Ok(model); | LivelitStateChange(livelit_id, livelit_state) => - let (id, ed) = Editors.get_editor_and_id(model.editors); let editor = - Editors.put_editor_and_id( - id, - { - ...ed, - state: { - ...ed.state, - meta: { - ...ed.state.meta, - livelit_state: - Id.Map.add( - livelit_id, - livelit_state, - ed.state.meta.livelit_state, - ), - }, - }, + Editors.update_editor( + ed => { + Editor.update_livelit_state( + Id.Map.add(livelit_id, livelit_state), + ed, + ) }, model.editors, ); + Ok({...model, editors: editor}); }; reevaluate_post_update(update) From 106ef2386182caecfa69a5431001599c11712f7b Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 19 Mar 2023 12:20:49 -0500 Subject: [PATCH 36/52] Use Livelit.empty_state --- src/haz3lweb/view/BackpackView.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/haz3lweb/view/BackpackView.re b/src/haz3lweb/view/BackpackView.re index 6876aeda85..6cedcf5de9 100644 --- a/src/haz3lweb/view/BackpackView.re +++ b/src/haz3lweb/view/BackpackView.re @@ -38,7 +38,7 @@ let backpack_sel_view = content, ~inject=_ => Ui_effect.Ignore, ~font_metrics, - ~livelit_state=Id.Map.empty, + ~livelit_state=Livelit.empty_state, ) // TODO Livelit state @ [text(Unicode.zwsp)], ); From 8445767c0ad595448cdd35ebb10c59b1b510c51e Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 19 Mar 2023 12:27:32 -0500 Subject: [PATCH 37/52] Break livelit_padding into a function --- src/haz3lcore/Measured.re | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index 9ca92ed22e..956fa1ff41 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -283,6 +283,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 + | None => 0 + } + | _ => 0 + }; + let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => { let is_indented = is_indented_map(seg); @@ -376,16 +386,6 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => { let map = map |> add_g(g, {origin, last}); (contained_indent, last, map); | Tile(t) => - let livelit_padding = - switch (t.label) { - | [possible_livelit_name] => - switch (Livelit.find_livelit(possible_livelit_name)) { - | Some(ll) => ll.width - | None => 0 - } - | _ => 0 - }; - let token = List.nth(t.label); let add_shard = (origin, shard, map) => { let last = @@ -394,7 +394,7 @@ let of_segment = (~old: t=empty, ~touched=Touched.empty, seg: Segment.t): t => { col: origin.col + String.length(token(shard)) - + livelit_padding, + + livelit_padding(t), }; let map = map |> add_s(t.id, shard, {origin, last}); (last, map); From 6b96a5a8a789169b06901bae1212630757c6f6fe Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 19 Mar 2023 12:36:05 -0500 Subject: [PATCH 38/52] Rename livelit_state to livelits --- src/haz3lcore/dynamics/elaborator.re | 52 +++++++++++++--------------- src/haz3lcore/prog/Interface.re | 4 +-- src/haz3lcore/tiles/Livelit.re | 5 ++- src/haz3lcore/zipper/Editor.re | 12 +++---- src/haz3lweb/ScratchSlide.re | 2 +- src/haz3lweb/Update.re | 7 ++-- src/haz3lweb/view/BackpackView.re | 2 +- src/haz3lweb/view/Cell.re | 8 ++--- src/haz3lweb/view/Code.re | 47 ++++++++----------------- src/haz3lweb/view/LivelitView.re | 6 ++-- 10 files changed, 58 insertions(+), 87 deletions(-) diff --git a/src/haz3lcore/dynamics/elaborator.re b/src/haz3lcore/dynamics/elaborator.re index af7afc0ca5..7a8581ec11 100644 --- a/src/haz3lcore/dynamics/elaborator.re +++ b/src/haz3lcore/dynamics/elaborator.re @@ -136,7 +136,7 @@ let wrap = (u, mode, self, d: DHExp.t): option(DHExp.t) => }; let rec dhexp_of_uexp = - (m: Statics.map, uexp: Term.UExp.t, livelit_state: Livelit.state) + (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)) { @@ -173,22 +173,20 @@ let rec dhexp_of_uexp = | String(s) => Some(StringLit(s)) | ListLit(es) => let+ ds = - es - |> List.map(dhexp_of_uexp(m, _, livelit_state)) - |> OptUtil.sequence; + 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, livelit_state); + 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, livelit_state); + let+ d = dhexp_of_uexp(m, e, livelits); [d, ...ds]; }, es, @@ -197,24 +195,24 @@ let rec dhexp_of_uexp = DHExp.Tuple(ds); | Tag(name) => Some(Tag(name)) | Cons(e1, e2) => - let* dc1 = dhexp_of_uexp(m, e1, livelit_state); - let+ dc2 = dhexp_of_uexp(m, e2, livelit_state); + 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, livelit_state); + 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, livelit_state); - let+ dc2 = dhexp_of_uexp(m, e2, livelit_state); + 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, livelit_state) + | Parens(e) => dhexp_of_uexp(m, e, livelits) | Seq(e1, e2) => - let* d1 = dhexp_of_uexp(m, e1, livelit_state); - let+ d2 = dhexp_of_uexp(m, e2, livelit_state); + 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, livelit_state); + let+ dtest = dhexp_of_uexp(m, test, livelits); DHExp.Ap(TestLit(id), dtest); | Var(name) => switch (err_status) { @@ -229,8 +227,8 @@ let rec dhexp_of_uexp = | d => d ); let* dp = dhpat_of_upat(m, p); - let* ddef = dhexp_of_uexp(m, def, livelit_state); - let+ dbody = dhexp_of_uexp(m, body, livelit_state); + 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 => @@ -263,13 +261,13 @@ let rec dhexp_of_uexp = Let(dp, FixF(self_id, ty, substituted_def), dbody); }; | Ap(fn, arg) => - let* c_fn = dhexp_of_uexp(m, fn, livelit_state); - let+ c_arg = dhexp_of_uexp(m, arg, livelit_state); + 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, livelit_state); - let* d1 = dhexp_of_uexp(m, e1, livelit_state); - let+ d2 = dhexp_of_uexp(m, e2, livelit_state); + 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); @@ -282,15 +280,15 @@ let rec dhexp_of_uexp = Livelit.elaborate_livelit( livelit_name, Term.UExp.rep_id(uexp), - livelit_state, + livelits, ) | Match(scrut, rules) => - let* d_scrut = dhexp_of_uexp(m, scrut, livelit_state); + 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, livelit_state); + let+ d_e = dhexp_of_uexp(m, e, livelits); DHExp.Rule(d_p, d_e); }, rules, @@ -384,9 +382,9 @@ let uexp_elab_wrap_builtins = (d: DHExp.t): DHExp.t => ); let uexp_elab = - (m: Statics.map, uexp: Term.UExp.t, livelit_state: Livelit.state) + (m: Statics.map, uexp: Term.UExp.t, livelits: Livelit.state) : ElaborationResult.t => - switch (dhexp_of_uexp(m, uexp, livelit_state)) { + switch (dhexp_of_uexp(m, uexp, livelits)) { | None => DoesNotElaborate | Some(d) => let d = uexp_elab_wrap_builtins(d); diff --git a/src/haz3lcore/prog/Interface.re b/src/haz3lcore/prog/Interface.re index 35e009f4be..de75b3fbf5 100644 --- a/src/haz3lcore/prog/Interface.re +++ b/src/haz3lcore/prog/Interface.re @@ -1,6 +1,6 @@ exception DoesNotElaborate; -let elaborate = (~livelit_state=Id.Map.empty, map, term): DHExp.t => - switch (Elaborator.uexp_elab(map, term, livelit_state)) { +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 diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re index 16a5991c2c..3a5c3a11ec 100644 --- a/src/haz3lcore/tiles/Livelit.re +++ b/src/haz3lcore/tiles/Livelit.re @@ -32,9 +32,8 @@ let find_livelit = (livelit_name: string): option(t) => }; let elaborate_livelit = - (livelit_name: string, uexp_id: int, livelit_state: state) - : option(DHExp.t) => { - switch (Id.Map.find_opt(uexp_id, livelit_state)) { + (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)) { diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index 1aa2fce468..68f493a473 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -7,7 +7,7 @@ module Meta = { measured: Measured.t, term_ranges: TermRanges.t, col_target: int, - livelit_state: Livelit.state, + livelits: Livelit.state, }; let init = (z: Zipper.t) => { @@ -17,7 +17,7 @@ module Meta = { measured: Measured.of_segment(unselected), term_ranges: TermRanges.mk(unselected), col_target: 0, - livelit_state: Livelit.empty_state, + livelits: Livelit.empty_state, }; }; @@ -44,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, livelit_state, _} = 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); @@ -55,7 +55,7 @@ module Meta = { | Select(Resize(Local(Up | Down))) => col_target | _ => Zipper.caret_point(measured, z).col }; - {touched, measured, term_ranges, col_target, livelit_state}; + {touched, measured, term_ranges, col_target, livelits}; }; }; @@ -175,12 +175,12 @@ let trailing_hole_ctx = (ed: t, info_map: Statics.map) => { }; }; -let update_livelit_state = (f: Livelit.state => Livelit.state, ed: t): t => { +let update_livelits = (f: Livelit.state => Livelit.state, ed: t): t => { let new_state: State.t = { ...ed.state, meta: { ...ed.state.meta, - livelit_state: f(ed.state.meta.livelit_state), + livelits: f(ed.state.meta.livelits), }, }; {...ed, state: new_state}; diff --git a/src/haz3lweb/ScratchSlide.re b/src/haz3lweb/ScratchSlide.re index 1c85f638c8..19f592eb63 100644 --- a/src/haz3lweb/ScratchSlide.re +++ b/src/haz3lweb/ScratchSlide.re @@ -23,7 +23,7 @@ let spliced_elabs = ((_, editor)) => { Interface.elaborate( info_map, term, - ~livelit_state=editor.state.meta.livelit_state, + ~livelits=editor.state.meta.livelits, ), ), ]; diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index ed0986c557..abeeb7f3fb 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -426,14 +426,11 @@ let apply = | DebugAction(a) => DebugAction.perform(a); Ok(model); - | LivelitStateChange(livelit_id, livelit_state) => + | LivelitStateChange(livelit_id, livelits) => let editor = Editors.update_editor( ed => { - Editor.update_livelit_state( - Id.Map.add(livelit_id, livelit_state), - ed, - ) + Editor.update_livelits(Id.Map.add(livelit_id, livelits), ed) }, model.editors, ); diff --git a/src/haz3lweb/view/BackpackView.re b/src/haz3lweb/view/BackpackView.re index 6cedcf5de9..4087aaa82d 100644 --- a/src/haz3lweb/view/BackpackView.re +++ b/src/haz3lweb/view/BackpackView.re @@ -38,7 +38,7 @@ let backpack_sel_view = content, ~inject=_ => Ui_effect.Ignore, ~font_metrics, - ~livelit_state=Livelit.empty_state, + ~livelits=Livelit.empty_state, ) // TODO Livelit state @ [text(Unicode.zwsp)], ); diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re index 7d7b451490..b82f78f04e 100644 --- a/src/haz3lweb/view/Cell.re +++ b/src/haz3lweb/view/Cell.re @@ -294,7 +294,7 @@ let editor_view = ~measured, ~settings, ~inject, - ~livelit_state=editor.state.meta.livelit_state, + ~livelits=editor.state.meta.livelits, ); let deco_view = deco( @@ -331,11 +331,7 @@ let get_elab = (editor: Editor.t): DHExp.t => { let seg = Editor.get_seg(editor); let (term, _) = MakeTerm.go(seg); let info_map = Statics.mk_map(term); - Interface.elaborate( - info_map, - term, - ~livelit_state=editor.state.meta.livelit_state, - ); + Interface.elaborate(info_map, term, ~livelits=editor.state.meta.livelits); }; let editor_with_result_view = diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 7406956339..f5d315ebda 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -13,7 +13,7 @@ let of_delim' = label, i, inject, - livelit_state: Livelit.state, + livelits: Livelit.state, font_metrics: FontMetrics.t, tile_id: Id.t, ), @@ -31,7 +31,7 @@ let of_delim' = let livelit_nodes: list(t) = switch (label) { | [name] => - LivelitView.view(font_metrics, inject, name, livelit_state, tile_id) + LivelitView.view(font_metrics, inject, name, livelits, tile_id) | _ => [] }; [ @@ -49,7 +49,7 @@ let of_delim = t: Piece.tile, i: int, ~inject, - ~livelit_state: Livelit.state, + ~livelits: Livelit.state, ~font_metrics: FontMetrics.t, ) : list(Node.t) => @@ -60,7 +60,7 @@ let of_delim = t.label, i, inject, - livelit_state, + livelits, font_metrics, Tile.id(t), )); @@ -99,7 +99,7 @@ module Text = (M: { seg: Segment.t, ~inject, ~font_metrics: FontMetrics.t, - ~livelit_state: Livelit.state, + ~livelits: Livelit.state, ) : list(Node.t) => { //note: no_sorts flag is used for backback @@ -116,40 +116,21 @@ module Text = (M: { seg |> List.mapi((i, p) => (i, p)) |> List.concat_map(((i, p)) => - of_piece( - sort_of_p_idx(i), - p, - ~inject, - ~font_metrics, - ~livelit_state, - ) + of_piece(sort_of_p_idx(i), p, ~inject, ~font_metrics, ~livelits) ); } and of_piece = - ( - expected_sort: Sort.t, - p: Piece.t, - ~inject, - ~font_metrics, - ~livelit_state, - ) + (expected_sort: Sort.t, p: Piece.t, ~inject, ~font_metrics, ~livelits) : list(Node.t) => { switch (p) { - | Tile(t) => - of_tile(expected_sort, t, ~inject, ~font_metrics, ~livelit_state) + | Tile(t) => of_tile(expected_sort, t, ~inject, ~font_metrics, ~livelits) | Grout(_) => of_grout | Secondary({content, _}) => of_secondary((M.settings.secondary_icons, m(p).last.col, content)) }; } and of_tile = - ( - expected_sort: Sort.t, - t: Tile.t, - ~inject, - ~font_metrics, - ~livelit_state, - ) + (expected_sort: Sort.t, t: Tile.t, ~inject, ~font_metrics, ~livelits) : list(Node.t) => { let children_and_sorts = List.mapi( @@ -167,10 +148,10 @@ module Text = (M: { t, ~inject, ~font_metrics, - ~livelit_state, + ~livelits, ), ((seg, sort)) => - of_segment(~sort, seg, ~inject, ~font_metrics, ~livelit_state) + of_segment(~sort, seg, ~inject, ~font_metrics, ~livelits) ) |> List.concat; }; @@ -211,7 +192,7 @@ let simple_view = unselected, ~inject, ~font_metrics, - ~livelit_state=Id.Map.empty, + ~livelits=Id.Map.empty, ), ), ], @@ -226,7 +207,7 @@ let view = ~measured, ~settings: ModelSettings.t, ~inject, - ~livelit_state: Livelit.state, + ~livelits: Livelit.state, ) : Node.t => { module Text = @@ -236,7 +217,7 @@ let view = }); let unselected: list(t) = TimeUtil.measure_time("Code.view/unselected", settings.benchmark, () => - Text.of_segment(unselected, ~inject, ~font_metrics, ~livelit_state) + Text.of_segment(unselected, ~inject, ~font_metrics, ~livelits) ); let holes = TimeUtil.measure_time("Code.view/holes", settings.benchmark, () => diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index f64ea39096..7c68a16888 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -21,7 +21,7 @@ let view = font_metrics: FontMetrics.t, inject, name, - livelit_state: Livelit.state, + livelits: Livelit.state, tile_id, ) => { switch (name) { @@ -34,7 +34,7 @@ let view = Attr.create( "value", string_of_int( - switch (Id.Map.find_opt(tile_id, livelit_state)) { + switch (Id.Map.find_opt(tile_id, livelits)) { | Some(IntLit(i)) => i | _ => 50 }, @@ -60,7 +60,7 @@ let view = ] | "^checkbox" => let checkbox_state: bool = - switch (Id.Map.find_opt(tile_id, livelit_state)) { + switch (Id.Map.find_opt(tile_id, livelits)) { | Some(BoolLit(b)) => b | _ => false }; From d52669ea55633a8be6a376b244cf1a088b6d03cb Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 20 Mar 2023 20:06:56 -0500 Subject: [PATCH 39/52] Move livelit rendering outside of of_delim' --- src/haz3lweb/view/Code.re | 89 ++++++++++++++------------------------- 1 file changed, 32 insertions(+), 57 deletions(-) diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index f5d315ebda..7c1f69ec77 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -5,65 +5,40 @@ open Util; open Util.Web; let of_delim' = - ( - ( - sort, - is_consistent, - is_complete, - label, - i, - inject, - livelits: Livelit.state, - font_metrics: FontMetrics.t, - tile_id: Id.t, - ), - ) => { - let cls = - switch (label) { - | [_] when !is_consistent => "mono-inconsistent" - | [s] when Form.is_string(s) => "mono-string-lit" - | [_] => "mono" - | _ when !is_consistent => "delim-inconsistent" - | _ when !is_complete => "delim-incomplete" - | _ => "delim" - }; + Core.Memo.general( + ~cache_size_bound=100000, + ((sort, is_consistent, is_complete, label, i)) => { + let cls = + switch (label) { + | [_] when !is_consistent => "mono-inconsistent" + | [s] when Form.is_string(s) => "mono-string-lit" + | [_] => "mono" + | _ when !is_consistent => "delim-inconsistent" + | _ when !is_complete => "delim-incomplete" + | _ => "delim" + }; - let livelit_nodes: list(t) = - switch (label) { - | [name] => - LivelitView.view(font_metrics, inject, name, livelits, tile_id) - | _ => [] - }; - [ - span( - ~attr=Attr.classes(["token", cls, "text-" ++ Sort.to_string(sort)]), - List.append([Node.text(List.nth(label, i))], livelit_nodes), - ), - ]; -}; + [ + span( + ~attr= + Attr.classes(["token", cls, "text-" ++ Sort.to_string(sort)]), + [Node.text(List.nth(label, i))], + ), + ]; + }, + ); let of_delim = ( sort: Sort.t, is_consistent, t: Piece.tile, + livelit_nodes: list(t), i: int, - ~inject, - ~livelits: Livelit.state, - ~font_metrics: FontMetrics.t, ) : list(Node.t) => - of_delim'(( - sort, - is_consistent, - Tile.is_complete(t), - t.label, - i, - inject, - livelits, - font_metrics, - Tile.id(t), - )); + of_delim'((sort, is_consistent, Tile.is_complete(t), t.label, i)) + @ livelit_nodes; let of_grout = [Node.text(Unicode.nbsp)]; @@ -132,6 +107,13 @@ module Text = (M: { and of_tile = (expected_sort: Sort.t, t: Tile.t, ~inject, ~font_metrics, ~livelits) : list(Node.t) => { + let livelit_nodes: list(t) = + switch (t.label) { + | [name] => + LivelitView.view(font_metrics, inject, name, livelits, t.id) + | _ => [] + }; + let children_and_sorts = List.mapi( (i, (l, child, r)) => @@ -142,14 +124,7 @@ module Text = (M: { let is_consistent = Sort.consistent(t.mold.out, expected_sort); Aba.mk(t.shards, children_and_sorts) |> Aba.join( - of_delim( - t.mold.out, - is_consistent, - t, - ~inject, - ~font_metrics, - ~livelits, - ), + of_delim(t.mold.out, is_consistent, t, livelit_nodes), ((seg, sort)) => of_segment(~sort, seg, ~inject, ~font_metrics, ~livelits) ) From 003a68290ac1fc0602594cb34c6ff5ef87cf49e5 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Mon, 20 Mar 2023 21:11:25 -0500 Subject: [PATCH 40/52] Added left/right margin for livelits --- src/haz3lcore/Measured.re | 2 +- src/haz3lweb/view/LivelitView.re | 15 ++++++++------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index 956fa1ff41..c7dc26e5fa 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -287,7 +287,7 @@ 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 + | Some(ll) => ll.width + 1 // Add one for margin | None => 0 } | _ => 0 diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index 7c68a16888..3d4d792c3f 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -7,13 +7,15 @@ let stop_mousedown_propagation = Virtual_dom.Vdom.Effect.Ignore; }); -let livelit_style = (font_metrics: FontMetrics.t, livelit_width: int) => +let livelit_style = (font_metrics: FontMetrics.t, livelit_width: float) => Attr.create( "style", Printf.sprintf( - "width: %fpx; height: %fpx; margin: 0; vertical-align: bottom", - float_of_int(livelit_width) *. font_metrics.col_width, + "width: %fpx; height: %fpx; margin-top: 0; margin-bottom: 0; margin-left: %fpx; margin-right: %fpx; vertical-align: bottom; display: inline-block", + livelit_width *. font_metrics.col_width, font_metrics.row_height, + livelit_width *. 0.5, + livelit_width *. 0.5, ), ); let view = @@ -23,14 +25,14 @@ let view = name, livelits: Livelit.state, tile_id, - ) => { + ) => switch (name) { | "^slider" => [ Node.input( ~attr= Attr.many([ Attr.create("type", "range"), - livelit_style(font_metrics, 10), + livelit_style(font_metrics, float_of_int(10)), Attr.create( "value", string_of_int( @@ -71,7 +73,7 @@ let view = Attr.many( [ Attr.create("type", "checkbox"), - livelit_style(font_metrics, 1), + livelit_style(font_metrics, float_of_int(1)), Attr.on_change((_evt, _str) => { inject( UpdateAction.LivelitStateChange( @@ -89,4 +91,3 @@ let view = ]; | _ => [] }; -}; From 0037c1a76fa51a2654554694a3007ee92c6527c8 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Wed, 29 Mar 2023 19:16:58 -0500 Subject: [PATCH 41/52] Use curryied function application --- src/haz3lweb/Update.re | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index abeeb7f3fb..cf339c2f95 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -429,9 +429,7 @@ let apply = | LivelitStateChange(livelit_id, livelits) => let editor = Editors.update_editor( - ed => { - Editor.update_livelits(Id.Map.add(livelit_id, livelits), ed) - }, + Editor.update_livelits(Id.Map.add(livelit_id, livelits)), model.editors, ); From 58eb82ba66e6969bffe2e710918d2f917cecf5ff Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Wed, 29 Mar 2023 19:26:30 -0500 Subject: [PATCH 42/52] Switch checkbox to use on_input --- src/haz3lweb/view/LivelitView.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index 3d4d792c3f..3a8aee7d96 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -74,7 +74,7 @@ let view = [ Attr.create("type", "checkbox"), livelit_style(font_metrics, float_of_int(1)), - Attr.on_change((_evt, _str) => { + Attr.on_input((_evt, _str) => { inject( UpdateAction.LivelitStateChange( tile_id, From 520bde182a920a87d4e6cf6c890bed25f4027398 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Wed, 29 Mar 2023 19:42:00 -0500 Subject: [PATCH 43/52] Fix checkbox margins --- src/haz3lweb/view/LivelitView.re | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index 3a8aee7d96..9316d6cdc4 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -14,8 +14,8 @@ let livelit_style = (font_metrics: FontMetrics.t, livelit_width: float) => "width: %fpx; height: %fpx; margin-top: 0; margin-bottom: 0; margin-left: %fpx; margin-right: %fpx; vertical-align: bottom; display: inline-block", livelit_width *. font_metrics.col_width, font_metrics.row_height, - livelit_width *. 0.5, - livelit_width *. 0.5, + font_metrics.col_width *. 0.5, + font_metrics.col_width *. 0.5, ), ); let view = From f2c6b1e3308cb56f4f872efe20a9b4a8a1718559 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Wed, 29 Mar 2023 20:22:19 -0500 Subject: [PATCH 44/52] Try alternate livelit insertion mechanism --- src/haz3lcore/lang/Form.re | 2 +- src/haz3lcore/tiles/Livelit.re | 8 ++++---- src/haz3lweb/LangDocMessages.re | 2 +- src/haz3lweb/view/Code.re | 29 ++++++++++++++++++++++------- src/haz3lweb/view/LivelitView.re | 4 ++-- 5 files changed, 30 insertions(+), 15 deletions(-) diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index bcb236ad5b..da2693297b 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -96,7 +96,7 @@ let is_livelit = t => | _ => false }; let is_unknown_livelit = str => { - regexp("^[\\^]([a-z][A-Za-z0-9_]*)?$", str) && !is_livelit(str); + regexp("^([a-z][A-Za-z0-9_]*)?[\\^]$", str) && !is_livelit(str); }; /* The below case represents tokens which we want the user to be able to diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re index 3a5c3a11ec..5d6c3b7bf5 100644 --- a/src/haz3lcore/tiles/Livelit.re +++ b/src/haz3lcore/tiles/Livelit.re @@ -11,14 +11,14 @@ type t = { type state = Id.Map.t(DHExp.t); let empty_state: state = Id.Map.empty; let slider: t = { - name: "^slider", + name: "slider^", width: 10, default: IntLit(50), expansion_type: Int, }; let checkbox: t = { - name: "^checkbox", + name: "checkbox^", width: 1, default: BoolLit(false), expansion_type: Bool, @@ -26,8 +26,8 @@ let checkbox: t = { let find_livelit = (livelit_name: string): option(t) => switch (livelit_name) { - | "^slider" => Some(slider) - | "^checkbox" => Some(checkbox) + | "slider^" => Some(slider) + | "checkbox^" => Some(checkbox) | _ => None }; diff --git a/src/haz3lweb/LangDocMessages.re b/src/haz3lweb/LangDocMessages.re index 181b43c3f3..aa50dcbf39 100644 --- a/src/haz3lweb/LangDocMessages.re +++ b/src/haz3lweb/LangDocMessages.re @@ -2513,7 +2513,7 @@ let livelit_ap_exp_group = "livelit_ap_exp_group"; let livelit_ap_exp: form = { let explanation = {message: "Livelit Application", feedback: Unselected}; - let form = [exp("^slider")]; + let form = [exp("slider^")]; { id: "livelit_ap_exp", syntactic_form: form, diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 7c1f69ec77..c4aa652cab 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -18,13 +18,28 @@ let of_delim' = | _ => "delim" }; - [ - span( - ~attr= - Attr.classes(["token", cls, "text-" ++ Sort.to_string(sort)]), - [Node.text(List.nth(label, i))], - ), - ]; + switch (label) { + | [s] when Form.is_livelit(s) => [ + span( + ~attr= + Attr.classes(["token", cls, "text-" ++ Sort.to_string(sort)]), + [ + Node.text(String.sub(s, 0, String.length(s) - 1)), + span( + ~attr=Attr.create("style", "color: #d9d2be;"), + [Node.text("^")], + ), + ], + ), + ] + | _ => [ + span( + ~attr= + Attr.classes(["token", cls, "text-" ++ Sort.to_string(sort)]), + [Node.text(List.nth(label, i))], + ), + ] + }; }, ); diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index 9316d6cdc4..eb0a4d254c 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -27,7 +27,7 @@ let view = tile_id, ) => switch (name) { - | "^slider" => [ + | "slider^" => [ Node.input( ~attr= Attr.many([ @@ -60,7 +60,7 @@ let view = (), ), ] - | "^checkbox" => + | "checkbox^" => let checkbox_state: bool = switch (Id.Map.find_opt(tile_id, livelits)) { | Some(BoolLit(b)) => b From 9c2343bcf63bcf46a7eab53c362a4a2d2e64558c Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Wed, 29 Mar 2023 21:04:02 -0500 Subject: [PATCH 45/52] Hacky implementation of not rendering livelit name when rendering livelit --- src/haz3lcore/Measured.re | 4 ++-- src/haz3lweb/view/Code.re | 14 +------------- 2 files changed, 3 insertions(+), 15 deletions(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index c7dc26e5fa..675a5e8081 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -388,13 +388,13 @@ 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 foo = livelit_padding(t); let last = Point.{ ...origin, col: origin.col - + String.length(token(shard)) - + livelit_padding(t), + + (foo > 0 ? foo : String.length(token(shard))), }; let map = map |> add_s(t.id, shard, {origin, last}); (last, map); diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index c4aa652cab..90df07c8d6 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -19,19 +19,7 @@ let of_delim' = }; switch (label) { - | [s] when Form.is_livelit(s) => [ - span( - ~attr= - Attr.classes(["token", cls, "text-" ++ Sort.to_string(sort)]), - [ - Node.text(String.sub(s, 0, String.length(s) - 1)), - span( - ~attr=Attr.create("style", "color: #d9d2be;"), - [Node.text("^")], - ), - ], - ), - ] + | [s] when Form.is_livelit(s) => [] | _ => [ span( ~attr= From b2e50549acca03d281effcdbcf0b545e4f18c74e Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 2 Apr 2023 15:15:45 -0500 Subject: [PATCH 46/52] Fix left/right navigation --- src/haz3lcore/zipper/action/Move.re | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/haz3lcore/zipper/action/Move.re b/src/haz3lcore/zipper/action/Move.re index 913b4cb5b6..4f407184de 100644 --- a/src/haz3lcore/zipper/action/Move.re +++ b/src/haz3lcore/zipper/action/Move.re @@ -36,7 +36,11 @@ let neighbor_movability = let (l_nhbr, r_nhbr) = Siblings.neighbors(siblings); let l = switch (l_nhbr) { - | Some(Tile({label, _})) => movability(label, List.length(label) - 1) + | Some(Tile({label, _})) => + switch (label) { + | [s] when Option.is_some(Livelit.find_livelit(s)) => CanPass + | _ => movability(label, List.length(label) - 1) + } | Some(Secondary(w)) when Secondary.is_comment(w) => // Comments are always length >= 2 let content_string = Secondary.get_string(w.content); @@ -49,7 +53,11 @@ let neighbor_movability = }; let r = switch (r_nhbr) { - | Some(Tile({label, _})) => movability(label, 0) + | Some(Tile({label, _})) => + switch (label) { + | [s] when Option.is_some(Livelit.find_livelit(s)) => CanPass + | _ => movability(label, List.length(label) - 1) + } | Some(Secondary(w)) when Secondary.is_comment(w) => // Comments are always length >= 2 let content_string = Secondary.get_string(w.content); From 9e33a292cff652b760028521454abec633b9870d Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 20 Apr 2023 20:02:06 -0500 Subject: [PATCH 47/52] Switch livelit insertion to use tab --- src/haz3lcore/lang/Form.re | 2 +- src/haz3lcore/tiles/Livelit.re | 8 ++--- src/haz3lcore/zipper/action/Perform.re | 41 ++++++++++++++++---------- src/haz3lweb/view/LivelitView.re | 4 +-- 4 files changed, 32 insertions(+), 23 deletions(-) diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index da2693297b..409ad3392e 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -96,7 +96,7 @@ let is_livelit = t => | _ => false }; let is_unknown_livelit = str => { - regexp("^([a-z][A-Za-z0-9_]*)?[\\^]$", str) && !is_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 diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re index 5d6c3b7bf5..fc9904b121 100644 --- a/src/haz3lcore/tiles/Livelit.re +++ b/src/haz3lcore/tiles/Livelit.re @@ -11,14 +11,14 @@ type t = { type state = Id.Map.t(DHExp.t); let empty_state: state = Id.Map.empty; let slider: t = { - name: "slider^", + name: "slider\t", width: 10, default: IntLit(50), expansion_type: Int, }; let checkbox: t = { - name: "checkbox^", + name: "checkbox\t", width: 1, default: BoolLit(false), expansion_type: Bool, @@ -26,8 +26,8 @@ let checkbox: t = { let find_livelit = (livelit_name: string): option(t) => switch (livelit_name) { - | "slider^" => Some(slider) - | "checkbox^" => Some(checkbox) + | "slider\t" => Some(slider) + | "checkbox\t" => Some(checkbox) | _ => None }; diff --git a/src/haz3lcore/zipper/action/Perform.re b/src/haz3lcore/zipper/action/Perform.re index fc2fec547b..42b0dc1c84 100644 --- a/src/haz3lcore/zipper/action/Perform.re +++ b/src/haz3lcore/zipper/action/Perform.re @@ -16,14 +16,14 @@ let is_write_action = (a: Action.t) => { }; }; -let go_z = - ( - ~meta: option(Editor.Meta.t)=?, - a: Action.t, - z: Zipper.t, - id_gen: IdGen.state, - ) - : Action.Result.t((Zipper.t, IdGen.state)) => { +let rec go_z = + ( + ~meta: option(Editor.Meta.t)=?, + a: Action.t, + z: Zipper.t, + id_gen: IdGen.state, + ) + : Action.Result.t((Zipper.t, IdGen.state)) => { let meta = switch (meta) { | Some(m) => m @@ -92,15 +92,24 @@ let go_z = |> Result.of_option(~error=Action.Failure.Cant_insert) | Pick_up => Ok(remold_regrout(Left, Zipper.pick_up(z), id_gen)) | Put_down => - let z = + let current_livelit = + Zipper.left_neighbor_monotile(z.relatives.siblings) + |> Option.bind(_, t => Livelit.find_livelit(t ++ "\t")); + + switch (current_livelit) { + | Some(_) => go_z(Insert("\t"), z, id_gen) + | _ => /* Alternatively, putting down inside token could eiter merge-in or split */ - switch (z.caret) { - | Inner(_) => None - | Outer => Zipper.put_down(Left, z) - }; - z - |> Option.map(z => remold_regrout(Left, z, id_gen)) - |> Result.of_option(~error=Action.Failure.Cant_put_down); + ( + switch (z.caret) { + | Inner(_) => None + | Outer => Zipper.put_down(Left, z) + } + ) + |> Option.map(z => remold_regrout(Left, z, id_gen)) + |> Result.of_option(~error=Action.Failure.Cant_put_down) + }; + | RotateBackpack => let z = {...z, backpack: Util.ListUtil.rotate(z.backpack)}; Ok((z, id_gen)); diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index eb0a4d254c..53f42eafac 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -27,7 +27,7 @@ let view = tile_id, ) => switch (name) { - | "slider^" => [ + | "slider\t" => [ Node.input( ~attr= Attr.many([ @@ -60,7 +60,7 @@ let view = (), ), ] - | "checkbox^" => + | "checkbox\t" => let checkbox_state: bool = switch (Id.Map.find_opt(tile_id, livelits)) { | Some(BoolLit(b)) => b From ee832bde37888a11176581047bcc1254ddf0edb5 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Thu, 20 Apr 2023 20:30:22 -0500 Subject: [PATCH 48/52] Add fslider for floats --- src/haz3lcore/tiles/Livelit.re | 15 ++++++++---- src/haz3lweb/view/LivelitView.re | 41 +++++++++++++++++++++++++++++--- 2 files changed, 48 insertions(+), 8 deletions(-) diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re index fc9904b121..7819fb7d52 100644 --- a/src/haz3lcore/tiles/Livelit.re +++ b/src/haz3lcore/tiles/Livelit.re @@ -24,12 +24,17 @@ let checkbox: t = { 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) => - switch (livelit_name) { - | "slider\t" => Some(slider) - | "checkbox\t" => Some(checkbox) - | _ => None - }; + List.find_opt(l => l.name == livelit_name, livelits); let elaborate_livelit = (livelit_name: string, uexp_id: int, livelits: state): option(DHExp.t) => { diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index 53f42eafac..dc2cda508c 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -18,6 +18,7 @@ let livelit_style = (font_metrics: FontMetrics.t, livelit_width: float) => font_metrics.col_width *. 0.5, ), ); + let view = ( font_metrics: FontMetrics.t, @@ -25,9 +26,9 @@ let view = name, livelits: Livelit.state, tile_id, - ) => + ) => { switch (name) { - | "slider\t" => [ + | x when x == Livelit.slider.name => [ Node.input( ~attr= Attr.many([ @@ -60,7 +61,40 @@ let view = (), ), ] - | "checkbox\t" => + | x when x == Livelit.fslider.name => [ + Node.input( + ~attr= + Attr.many([ + Attr.create("type", "range"), + livelit_style(font_metrics, float_of_int(10)), + Attr.create( + "value", + string_of_int( + switch (Id.Map.find_opt(tile_id, livelits)) { + | Some(FloatLit(i)) => int_of_float(i *. 100.0) + | _ => 50 + }, + ), + ), + Attr.on_input((_evt, str) => + ( + { + inject( + UpdateAction.LivelitStateChange( + tile_id, + FloatLit(float_of_string(str) /. 100.0), + ), + ); + }: + Virtual_dom.Vdom.Effect.t(unit) + ) + ), + stop_mousedown_propagation, + ]), + (), + ), + ] + | x when x == Livelit.checkbox.name => let checkbox_state: bool = switch (Id.Map.find_opt(tile_id, livelits)) { | Some(BoolLit(b)) => b @@ -91,3 +125,4 @@ let view = ]; | _ => [] }; +}; From 07ba4a6883e5f5c0cec5cbb809dcf487cd6633a3 Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 23 Apr 2023 20:48:02 -0500 Subject: [PATCH 49/52] Code cleanup --- src/haz3lcore/Measured.re | 6 +- src/haz3lcore/lang/Form.re | 1 - src/haz3lcore/zipper/action/Perform.re | 2 +- src/haz3lweb/LangDocMessages.re | 2 +- src/haz3lweb/view/LivelitView.re | 132 ++++++++++++++----------- 5 files changed, 76 insertions(+), 67 deletions(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index 675a5e8081..6c820c629c 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -143,7 +143,6 @@ let add_w = (w: Secondary.t, m, map) => { ...map, secondary: map.secondary |> Id.Map.add(w.id, m), }; - let add_p = (p: Piece.t, m, map) => p |> Piece.get( @@ -388,13 +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 foo = livelit_padding(t); + let lp = livelit_padding(t); let last = Point.{ ...origin, col: - origin.col - + (foo > 0 ? foo : String.length(token(shard))), + origin.col + (lp > 0 ? lp : String.length(token(shard))), }; let map = map |> add_s(t.id, shard, {origin, last}); (last, map); diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 409ad3392e..57019148dd 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -111,7 +111,6 @@ let is_bad_lit = str => there are at most two quotes, in order to prevent merges */ let is_string = t => regexp("^\".*\"$", t) && List.length(String.split_on_char('"', t)) < 4; - let string_delim = "\""; let is_string_delim = (==)(string_delim); diff --git a/src/haz3lcore/zipper/action/Perform.re b/src/haz3lcore/zipper/action/Perform.re index 42b0dc1c84..d9cf5f8277 100644 --- a/src/haz3lcore/zipper/action/Perform.re +++ b/src/haz3lcore/zipper/action/Perform.re @@ -97,7 +97,7 @@ let rec go_z = |> Option.bind(_, t => Livelit.find_livelit(t ++ "\t")); switch (current_livelit) { - | Some(_) => go_z(Insert("\t"), z, id_gen) + | Some(_) => go_z(Insert("\t"), z, id_gen) // Tab complete inserts livelit | _ => /* Alternatively, putting down inside token could eiter merge-in or split */ ( diff --git a/src/haz3lweb/LangDocMessages.re b/src/haz3lweb/LangDocMessages.re index aa50dcbf39..7650cd1fde 100644 --- a/src/haz3lweb/LangDocMessages.re +++ b/src/haz3lweb/LangDocMessages.re @@ -2513,7 +2513,7 @@ let livelit_ap_exp_group = "livelit_ap_exp_group"; let livelit_ap_exp: form = { let explanation = {message: "Livelit Application", feedback: Unselected}; - let form = [exp("slider^")]; + let form = [exp(Livelit.slider.name)]; { id: "livelit_ap_exp", syntactic_form: form, diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index dc2cda508c..a4846b15fb 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -19,6 +19,54 @@ let livelit_style = (font_metrics: FontMetrics.t, livelit_width: float) => ), ); +let view_slider = + ( + font_metrics: FontMetrics.t, + inject, + livelits: Livelit.state, + tile_id, + decode: int => DHExp.t, + encode: DHExp.t => option(int), + ) => { + // let encode = t => { + // switch ((t: DHExp.t)) { + // | IntLit(i) => Some(i) + // | _ => None + // }; + // }; + // let decode = (i: int): DHExp.t => IntLit(i); + Node.input( + ~attr= + Attr.many([ + Attr.create("type", "range"), + livelit_style(font_metrics, float_of_int(10)), + Attr.create( + "value", + string_of_int( + Id.Map.find_opt(tile_id, livelits) + |> Option.bind(_, encode) + |> Option.value(~default=50), + ), + ), + Attr.on_input((_evt, str) => + ( + { + inject( + UpdateAction.LivelitStateChange( + tile_id, + decode(int_of_string(str)), + ), + ); + }: + Virtual_dom.Vdom.Effect.t(unit) + ) + ), + stop_mousedown_propagation, + ]), + (), + ); +}; + let view = ( font_metrics: FontMetrics.t, @@ -29,69 +77,33 @@ let view = ) => { switch (name) { | x when x == Livelit.slider.name => [ - Node.input( - ~attr= - Attr.many([ - Attr.create("type", "range"), - livelit_style(font_metrics, float_of_int(10)), - Attr.create( - "value", - string_of_int( - switch (Id.Map.find_opt(tile_id, livelits)) { - | Some(IntLit(i)) => i - | _ => 50 - }, - ), - ), - Attr.on_input((_evt, str) => - ( - { - inject( - UpdateAction.LivelitStateChange( - tile_id, - IntLit(int_of_string(str)), - ), - ); - }: - Virtual_dom.Vdom.Effect.t(unit) - ) - ), - stop_mousedown_propagation, - ]), - (), + view_slider( + font_metrics, + inject, + livelits, + tile_id, + i => IntLit(i), + t => { + switch (t) { + | IntLit(i) => Some(i) + | _ => None + } + }, ), ] | x when x == Livelit.fslider.name => [ - Node.input( - ~attr= - Attr.many([ - Attr.create("type", "range"), - livelit_style(font_metrics, float_of_int(10)), - Attr.create( - "value", - string_of_int( - switch (Id.Map.find_opt(tile_id, livelits)) { - | Some(FloatLit(i)) => int_of_float(i *. 100.0) - | _ => 50 - }, - ), - ), - Attr.on_input((_evt, str) => - ( - { - inject( - UpdateAction.LivelitStateChange( - tile_id, - FloatLit(float_of_string(str) /. 100.0), - ), - ); - }: - Virtual_dom.Vdom.Effect.t(unit) - ) - ), - stop_mousedown_propagation, - ]), - (), + view_slider( + font_metrics, + inject, + livelits, + tile_id, + i => FloatLit(float_of_int(i) /. 100.0), + t => { + switch (t) { + | FloatLit(i) => Some(int_of_float(i *. 100.0)) + | _ => None + } + }, ), ] | x when x == Livelit.checkbox.name => From e0a0dfc2076af6ff8f1e022a15c3f9c9f88946db Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 23 Apr 2023 20:49:13 -0500 Subject: [PATCH 50/52] Remove unused code --- src/haz3lweb/view/LivelitView.re | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index a4846b15fb..28c5ed75ac 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -28,13 +28,6 @@ let view_slider = decode: int => DHExp.t, encode: DHExp.t => option(int), ) => { - // let encode = t => { - // switch ((t: DHExp.t)) { - // | IntLit(i) => Some(i) - // | _ => None - // }; - // }; - // let decode = (i: int): DHExp.t => IntLit(i); Node.input( ~attr= Attr.many([ From 9ba000ebf257cdd36a7be51b18ce9313590562df Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Wed, 26 Apr 2023 18:31:31 -0500 Subject: [PATCH 51/52] Livelits begin with a caret --- src/haz3lcore/lang/Form.re | 2 +- src/haz3lcore/tiles/Livelit.re | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 57019148dd..acf2063d19 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -96,7 +96,7 @@ let is_livelit = t => | _ => false }; let is_unknown_livelit = str => { - regexp("^([a-z][A-Za-z0-9_]*)?\t$", str) && !is_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 diff --git a/src/haz3lcore/tiles/Livelit.re b/src/haz3lcore/tiles/Livelit.re index 7819fb7d52..412ef44c77 100644 --- a/src/haz3lcore/tiles/Livelit.re +++ b/src/haz3lcore/tiles/Livelit.re @@ -11,21 +11,21 @@ type t = { type state = Id.Map.t(DHExp.t); let empty_state: state = Id.Map.empty; let slider: t = { - name: "slider\t", + name: "^slider\t", width: 10, default: IntLit(50), expansion_type: Int, }; let checkbox: t = { - name: "checkbox\t", + name: "^checkbox\t", width: 1, default: BoolLit(false), expansion_type: Bool, }; let fslider: t = { - name: "fslider\t", + name: "^fslider\t", width: 10, default: FloatLit(0.5), expansion_type: Float, From 958f3bec2f158e32ec1f276a91c7ec5e26b5e32a Mon Sep 17 00:00:00 2001 From: Alexander Bandukwala <7h3kk1d@gmail.com> Date: Sun, 7 May 2023 19:14:55 -0500 Subject: [PATCH 52/52] Fix compatibility OCaml 5 --- src/haz3lweb/view/LivelitView.re | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/haz3lweb/view/LivelitView.re b/src/haz3lweb/view/LivelitView.re index 28c5ed75ac..f29dbb427e 100644 --- a/src/haz3lweb/view/LivelitView.re +++ b/src/haz3lweb/view/LivelitView.re @@ -56,7 +56,7 @@ let view_slider = ), stop_mousedown_propagation, ]), - (), + [], ); }; @@ -125,7 +125,7 @@ let view = ] @ (checkbox_state ? [Attr.checked] : []), ), - (), + [], ), ]; | _ => []