Skip to content

Commit

Permalink
statics progress, livelit proj can access args
Browse files Browse the repository at this point in the history
  • Loading branch information
gcrois committed Nov 7, 2024
1 parent 2dd93b0 commit a9f5774
Show file tree
Hide file tree
Showing 6 changed files with 126 additions and 103 deletions.
12 changes: 1 addition & 11 deletions src/haz3lcore/Measured.re
Original file line number Diff line number Diff line change
Expand Up @@ -282,16 +282,6 @@ let last_of_token = (token: string, origin: Point.t): Point.t =>
row: origin.row + StringUtil.num_linebreaks(token),
};

let livelit_padding = (t: Base.tile): abs_indent =>
switch (t.label) {
| [possible_livelit_name] =>
switch (Livelit.find_livelit(possible_livelit_name)) {
| Some(_ll) => 10 + 1 // Add one for margin
| None => 0
}
| _ => 0
};

let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
let is_indented = is_indented_map(seg);

Expand Down Expand Up @@ -372,7 +362,7 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
| Tile(t) =>
let token = List.nth(t.label);
let add_shard = (origin, shard, map) => {
let lp = livelit_padding(t);
let lp = 0;
let last =
Point.{
...origin,
Expand Down
28 changes: 15 additions & 13 deletions src/haz3lcore/dynamics/Elaborator.re
Original file line number Diff line number Diff line change
Expand Up @@ -250,13 +250,9 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
|> Option.value(~default=Typ.temp(Typ.Unknown(Internal)));
let ds' = List.map2((d, t) => fresh_cast(d, t, inner_type), ds, tys);
Exp.ListLit(ds') |> rewrap |> cast_from(List(inner_type) |> Typ.temp);
| LivelitInvocation(livelit_name) =>
switch (Livelit.elaborate_livelit(livelit_name)) {
| Some((t, uexp_f)) => uexp_f(uexp) |> cast_from(t)
| None =>
print_endline("Livelit not found");
uexp |> cast_from(Typ.temp(Typ.Unknown(Internal)));
}
| LivelitInvocation(_) =>
// This should never happen if the Livelit is invoked!
uexp |> cast_from(Typ.temp(Typ.Unknown(Internal)))
| Constructor(c, _) =>
let mode =
switch (Id.Map.find_opt(Exp.rep_id(uexp), m)) {
Expand Down Expand Up @@ -335,12 +331,18 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
let (e', tye) = elaborate(m, e);
e' |> cast_from(tye);
| Ap(dir, f, a) =>
let (f', tyf) = elaborate(m, f);
let (a', tya) = elaborate(m, a);
let (tyf1, tyf2) = Typ.matched_arrow(ctx, tyf);
let f'' = fresh_cast(f', tyf, Arrow(tyf1, tyf2) |> Typ.temp);
let a'' = fresh_cast(a', tya, tyf1);
Exp.Ap(dir, f'', a'') |> rewrap |> cast_from(tyf2);
switch (f.term) {
| LivelitInvocation(s) =>
let ll = Livelit.find_livelit(s);
ll.expansion_f(a) |> cast_from(ll.expansion_t);
| _ =>
let (f', tyf) = elaborate(m, f);
let (a', tya) = elaborate(m, a);
let (tyf1, tyf2) = Typ.matched_arrow(ctx, tyf);
let f'' = fresh_cast(f', tyf, Arrow(tyf1, tyf2) |> Typ.temp);
let a'' = fresh_cast(a', tya, tyf1);
Exp.Ap(dir, f'', a'') |> rewrap |> cast_from(tyf2);
}
| DeferredAp(f, args) =>
let (f', tyf) = elaborate(m, f);
let (args', tys) = List.map(elaborate(m), args) |> ListUtil.unzip;
Expand Down
39 changes: 27 additions & 12 deletions src/haz3lcore/statics/Statics.re
Original file line number Diff line number Diff line change
Expand Up @@ -231,7 +231,8 @@ and uexp_to_info_map =
| Int(_) => atomic(Just(Int |> Typ.temp))
| Float(_) => atomic(Just(Float |> Typ.temp))
| String(_) => atomic(Just(String |> Typ.temp))
| LivelitInvocation(name) => atomic(Just(Livelit.get_livelit_type(name)))
| LivelitInvocation(name) =>
atomic(Just(Livelit.find_livelit(name).expansion_t))
| ListLit(es) =>
let ids = List.map(UExp.rep_id, es);
let modes = Mode.of_list_lit(ctx, List.length(es), mode);
Expand Down Expand Up @@ -328,16 +329,30 @@ and uexp_to_info_map =
let (e2, m) = go(~mode, e2, m);
add(~self=Just(e2.ty), ~co_ctx=CoCtx.union([e1.co_ctx, e2.co_ctx]), m);
| Constructor(ctr, _) => atomic(Self.of_ctr(ctx, ctr))
| Ap(_, fn, arg) =>
let fn_mode = Mode.of_ap(ctx, mode, UExp.ctr_name(fn));
let (fn, m) = go(~mode=fn_mode, fn, m);
let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty);
let (arg, m) = go(~mode=Ana(ty_in), arg, m);
let self: Self.t =
Id.is_nullary_ap_flag(arg.term.ids)
&& !Typ.is_consistent(ctx, ty_in, Prod([]) |> Typ.temp)
? BadTrivAp(ty_in) : Just(ty_out);
add(~self, ~co_ctx=CoCtx.union([fn.co_ctx, arg.co_ctx]), m);
| Ap(_, fn_uexp, arg_uexp) =>
let fn_mode = Mode.of_ap(ctx, mode, UExp.ctr_name(fn_uexp));
let (fn, m) = go(~mode=fn_mode, fn_uexp, m);

switch (fn_uexp.term) {
| LivelitInvocation(s) =>
// refer to livelit context to find types
print_endline("Livelit invocation " ++ s);
let ll = Livelit.find_livelit(s);
let expansion_t = ll.expansion_t;
let model_t = ll.model_t;
let (arg, m) = go(~mode=Ana(model_t), arg_uexp, m);
let self: Self.t = Just(expansion_t);
add(~self, ~co_ctx=CoCtx.union([arg.co_ctx]), m);
| _ =>
// default for non-livelit applications
let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty);
let (arg, m) = go(~mode=Ana(ty_in), arg_uexp, m);
let self: Self.t =
Id.is_nullary_ap_flag(arg.term.ids)
&& !Typ.is_consistent(ctx, ty_in, Prod([]) |> Typ.temp)
? BadTrivAp(ty_in) : Just(ty_out);
add(~self, ~co_ctx=CoCtx.union([fn.co_ctx, arg.co_ctx]), m);
};
| TypAp(fn, utyp) =>
let typfn_mode = Mode.typap_mode;
let (fn, m) = go(~mode=typfn_mode, fn, m);
Expand Down Expand Up @@ -734,7 +749,7 @@ and upat_to_info_map =
| String(string) =>
atomic(Just(String |> Typ.temp), Constraint.String(string))
| LivelitInvocation(name) =>
atomic(Just(Livelit.get_livelit_type(name)), Constraint.Truth)
atomic(Just(Livelit.find_livelit(name).expansion_t), 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
96 changes: 37 additions & 59 deletions src/haz3lcore/tiles/Livelit.re
Original file line number Diff line number Diff line change
@@ -1,84 +1,62 @@
open Util;
open Virtual_dom.Vdom;

[@deriving (show({with_path: false}), sexp, yojson)]
type t = {
name: string,
model_t: Typ.t,
// init: UExp.term,
expansion_t: Typ.t,
expansion_f: UExp.t => UExp.t,
projector: UExp.t => Node.t,
};
let slider: t = {
name: "slider",
expansion_t: Typ.temp(Typ.Int),
expansion_f: (_model: UExp.t) => DHExp.fresh(Int(3)),
expansion_f: (model: UExp.t) =>
switch (model.term) {
| Int(n) => DHExp.fresh(Int(n))
| _ => DHExp.fresh(Int(-1))
},
model_t: Typ.temp(Typ.Int),
projector: (model: UExp.t) =>
Node.div(
~attrs=[Attr.class_("livelit")],
[Node.text("I am a slider and my model is " ++ UExp.show(model))],
),
};

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 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),
model_t: Typ.temp(Typ.Prod([])),
projector: (_model: UExp.t) =>
Node.div(
~attrs=[Attr.class_("livelit")],
[Node.text("Guess what guys -- I am a timestamp livelit!")],
),
};

// 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, UExp.t => UExp.t)) => {
let r =
switch (find_livelit(livelit_name)) {
| Some(l) => Some((l.expansion_t, l.expansion_f))
| None => None
};
r;
let not_found: t = {
name: "not_found",
expansion_t: Typ.temp(Typ.Unknown(Internal)),
expansion_f: (_model: UExp.t) => DHExp.fresh(String("No livelit found")),
model_t: Typ.temp(Typ.Unknown(Internal)),
projector: (_model: UExp.t) =>
Node.div(
~attrs=[Attr.class_("livelit")],
[Node.text("No livelit found")],
),
};

let get_livelit_type = (livelit_name: string): Typ.t =>
switch (find_livelit(livelit_name)) {
| Some(l) => l.expansion_t
| None => Typ.temp(Typ.Unknown(Internal))
};
let livelits: list(t) = [slider, timestamp];

let project_livelit = (livelit_name: string): string => {
switch (find_livelit(livelit_name)) {
| Some(l) => l.name
| None => "Not found"
let find_livelit = (livelit_name: string): t =>
// List.find_opt(l => l.name == livelit_name, livelits)
// |> Option.value(~default=not_found);
switch (List.find_opt(l => l.name == livelit_name, livelits)) {
| Some(l) => l
| None =>
print_endline("Livelit " ++ livelit_name ++ " not found");
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
50 changes: 44 additions & 6 deletions src/haz3lcore/zipper/projectors/LivelitProj.re
Original file line number Diff line number Diff line change
Expand Up @@ -13,24 +13,62 @@ let get = (piece: Piece.t): string =>
| Some(s) => s
};

let getApArgs = (term: UExp.term): list(UExp.t) =>
switch (term) {
| UExp.Parens(args) =>
switch (args.term) {
| Tuple(lst) => lst
| _ => [args]
}
| _ => failwith("Not an Ap term")
};

module M: Projector = {
[@deriving (show({with_path: false}), sexp, yojson)]
type model = unit;
[@deriving (show({with_path: false}), sexp, yojson)]
type action = unit;
let init = ();
let can_project = p => get_opt(p) != None;
let can_project = p => true;
let can_focus = false;
let placeholder = (_, _) => Inline(10);
let update = (model, _) => model;
let view =
(_, ~info, ~local as _, ~parent: external_action => Ui_effect.t(unit)) => {
let llname = get(info.syntax);
print_endline("Livelit: " ++ llname);
Node.div(
~attrs=[Attr.class_("livelit")],
[Node.text("Livelit: " ++ llname)],
let args: list(UExp.t) =
switch (info.ci) {
| Some(InfoExp(exp)) =>
print_endline("Livelit term: " ++ UExp.show(exp.term));
let (term, _) = UExp.unwrap(exp.term);
switch (term) {
| Parens(args) =>
switch (args.term) {
| Ap(_dir, _f, args) =>
let (term, _) = UExp.unwrap(args);
switch (term) {
| Tuple(lst) => lst
| _ => [args]
};
| _ => failwith("Not an Ap term")
}
| _ => failwith("Not an Ap term")
};
| _ => failwith("Not an Ap term")
};

print_endline(
"Livelit args: "
++ (args |> List.map(UExp.show) |> String.concat(", ")),
);

// print_endline("Livelit syntax: " ++ debug);
switch (info.ci) {
| _ =>
Node.div(
~attrs=[Attr.class_("livelit")],
[Node.text("I am a livelit")],
)
};
};
let focus = _ => ();
};
4 changes: 2 additions & 2 deletions src/haz3lweb/view/ProjectorView.re
Original file line number Diff line number Diff line change
Expand Up @@ -217,8 +217,8 @@ module Panel = {
| Pat(Float) => [SliderF]
| Exp(String)
| Pat(String) => [TextArea]
| Exp(LivelitInvocation)
| Pat(LivelitInvocation) => [Livelit]
| Exp(Parens)
| Pat(Parens) => [Livelit]
| _ => []
}
)
Expand Down

0 comments on commit a9f5774

Please sign in to comment.