Skip to content

Commit

Permalink
added more test livelits, patched statics, elaborator update
Browse files Browse the repository at this point in the history
  • Loading branch information
gcrois committed Nov 5, 2024
1 parent 20b6aef commit e195409
Show file tree
Hide file tree
Showing 6 changed files with 76 additions and 29 deletions.
2 changes: 1 addition & 1 deletion src/haz3lcore/Measured.re
Original file line number Diff line number Diff line change
Expand Up @@ -286,7 +286,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 + 1 // Add one for margin
| Some(_ll) => 10 + 1 // Add one for margin
| None => 0
}
| _ => 0
Expand Down
2 changes: 1 addition & 1 deletion src/haz3lcore/dynamics/Elaborator.re
Original file line number Diff line number Diff line change
Expand Up @@ -252,7 +252,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
Exp.ListLit(ds') |> rewrap |> cast_from(List(inner_type) |> Typ.temp);
| LivelitInvocation(livelit_name) =>
switch (Livelit.elaborate_livelit(livelit_name)) {
| Some(t) => uexp |> cast_from(t)
| Some((_t, uexp_f)) => uexp_f(uexp)
| None => uexp |> cast_from(Typ.temp(Typ.Unknown(Internal)))
}
| Constructor(c, _) =>
Expand Down
4 changes: 2 additions & 2 deletions src/haz3lcore/lang/Form.re
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ let is_potential_operand = match(regexp("^[\\^a-zA-Z0-9_'\\.?]+$"));
* delimiters, string delimiters, or the instant expanding paired
* delimiters: ()[]| */
let potential_operator_regexp =
regexp("^[\\^a-zA-Z0-9_'?\"#\n\\s\\[\\]\\(\\)]+$"); /* Multiline operators not supported */
regexp("^[^a-zA-Z0-9_'?\"#\n\\s\\[\\]\\(\\)]+$"); /* Multiline operators not supported */
let is_potential_operator = match(potential_operator_regexp);
let is_potential_token = t =>
is_potential_operand(t)
Expand Down Expand Up @@ -155,7 +155,7 @@ let is_livelit = str => {
let result = match(re, str);
result;
};
let parse_livelit = str =>
let parse_livelit = (str): string =>
if (String.length(str) > 1 && String.sub(str, 0, 1) == "^") {
String.sub(str, 1, String.length(str) - 1);
} else {
Expand Down
6 changes: 6 additions & 0 deletions src/haz3lcore/statics/Ctx.re
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,12 @@ type tvar_entry = {
kind,
};

type livelit_entry = {
name: string,
id: Id.t,
typ: TermBase.Typ.t,
};

[@deriving (show({with_path: false}), sexp, yojson)]
type entry =
| VarEntry(var_entry)
Expand Down
4 changes: 2 additions & 2 deletions src/haz3lcore/statics/Statics.re
Original file line number Diff line number Diff line change
Expand Up @@ -733,8 +733,8 @@ and upat_to_info_map =
)
| String(string) =>
atomic(Just(String |> Typ.temp), Constraint.String(string))
| LivelitInvocation(_) =>
atomic(Just(String |> Typ.temp), Constraint.Truth)
| LivelitInvocation(name) =>
atomic(Just(Livelit.get_livelit_type(name)), Constraint.Truth)
| ListLit(ps) =>
let ids = List.map(UPat.rep_id, ps);
let modes = Mode.of_list_lit(ctx, List.length(ps), mode);
Expand Down
87 changes: 64 additions & 23 deletions src/haz3lcore/tiles/Livelit.re
Original file line number Diff line number Diff line change
Expand Up @@ -3,41 +3,82 @@ open Util;
[@deriving (show({with_path: false}), sexp, yojson)]
type t = {
name: string,
width: int,
default: Pat.term,
expansion_type: Typ.t,
model_t: Typ.t,
// init: UExp.term,
expansion_t: Typ.t,
expansion_f: UExp.t => UExp.t,
};

type state = Id.Map.t(t);
let slider: t = {
name: "slider\t",
width: 10,
default: Int(30),
expansion_type: Typ.temp(Typ.Int),
name: "slider",
expansion_t: Typ.temp(Typ.Int),
expansion_f: (_model: UExp.t) => DHExp.fresh(Int(3)),
model_t: Typ.temp(Typ.Int),
};

let checkbox: t = {
name: "checkbox\t",
width: 1,
default: Bool(false),
expansion_type: Typ.temp(Typ.Bool),
let timestamp: t = {
name: "timestamp",
expansion_t: Typ.temp(Typ.Int),
expansion_f: (_model: UExp.t) =>
DHExp.fresh(Int(Float.to_int(JsUtil.timestamp()))),
model_t: Typ.temp(Typ.Int),
};

let fslider: t = {
name: "fslider\t",
width: 10,
default: Float(0.5),
expansion_type: Typ.temp(Typ.Float),
let func_test: t = {
name: "func_test",
expansion_t: Typ.temp(Typ.Arrow(Typ.temp(Typ.Int), Typ.temp(Typ.Int))),
expansion_f: (_model: UExp.t) => DHExp.fresh(Int(3)),
model_t: Typ.temp(Typ.Int),
};

let livelits: list(t) = [checkbox, fslider, slider];
// let checkbox: t = {
// name: "checkbox",
// width: 1,
// default: Bool(false),
// expansion_type: Typ.temp(Typ.Bool),
// };

// let fslider: t = {
// name: "fslider",
// width: 10,
// default: Float(0.5),
// expansion_type: Typ.temp(Typ.Float),
// };

let livelits: list(t) = [slider, timestamp, func_test];

let find_livelit = (livelit_name: string): option(t) =>
List.find_opt(l => l.name == livelit_name, livelits);

let elaborate_livelit = (livelit_name: string): option(Typ.t) => {
let elaborate_livelit =
(livelit_name: string): option((Typ.t, UExp.t => UExp.t)) => {
let r =
switch (find_livelit(livelit_name)) {
| Some(l) => Some((l.expansion_t, l.expansion_f))
| None => None
};
r;
};

let get_livelit_type = (livelit_name: string): Typ.t =>
switch (find_livelit(livelit_name)) {
| Some(l) => Some(l.expansion_type)
| None => None
| Some(l) => l.expansion_t
| None => Typ.temp(Typ.Unknown(Internal))
};

let project_livelit = (livelit_name: string): string => {
switch (find_livelit(livelit_name)) {
| Some(l) => l.name
| None => "Not found"
};
};

// [@deriving (show({with_path: false}), sexp, yojson)]
// type t =
// name: string,
// model_t: Typ.t,
// init: UExp.t,
// default: UExp.term,
// expansion_t: Typ.t,
// // view
// // action_t
// // update

0 comments on commit e195409

Please sign in to comment.