Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/dev' into haz3l-module
Browse files Browse the repository at this point in the history
  • Loading branch information
@gensofubi
gensofubi committed May 30, 2024
2 parents 42f59bb + 60102ea commit 67986f0
Show file tree
Hide file tree
Showing 14 changed files with 612 additions and 326 deletions.
9 changes: 7 additions & 2 deletions src/haz3lcore/dynamics/Elaborator.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ let rec dhexp_of_uexp =
dhexp_of_uexp(m, uexp, in_filter);
};
switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) {
| Some(InfoExp({mode, self, ctx, ancestors, _})) =>
| Some(InfoExp({mode, self, ctx, ancestors, co_ctx, _})) =>
let err_status = Info.status_exp(ctx, mode, self);
let id = Term.UExp.rep_id(uexp); /* NOTE: using term uids for hole ids */
let+ d: DHExp.t =
Expand Down Expand Up @@ -252,7 +252,12 @@ let rec dhexp_of_uexp =
let* ddef = dhexp_of_uexp(m, def);
let* dbody = dhexp_of_uexp(m, body);
let+ ty = fixed_pat_typ(m, p);
if (!Statics.is_recursive(ctx, p, def, ty)) {
let is_recursive =
Statics.is_recursive(ctx, p, def, ty)
&& Term.UPat.get_bindings(p)
|> Option.get
|> List.exists(f => VarMap.lookup(co_ctx, f) != None);
if (!is_recursive) {
/* not recursive */
DHExp.Let(
dp,
Expand Down
222 changes: 210 additions & 12 deletions src/haz3lcore/dynamics/EvaluatorStep.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -150,15 +150,6 @@ module Decompose = {
module Decomp = Transition(DecomposeEVMode);
let rec decompose = (state, env, exp) => {
switch (exp) {
| DHExp.Filter(flt, d1) =>
DecomposeEVMode.(
{
let. _ = otherwise(env, (d1) => (Filter(flt, d1): DHExp.t))
and. d1 =
req_final(decompose(state, env), d1 => Filter(flt, d1), d1);
Step({apply: () => d1, kind: CompleteFilter, value: true});
}
)
| _ => Decomp.transition(decompose, state, env, exp)
};
};
Expand Down Expand Up @@ -362,12 +353,219 @@ let decompose = (d: DHExp.t) => {
Decompose.Result.unbox(rs);
};

let evaluate_with_history = d => {
let rec matches =
(
env: ClosureEnvironment.t,
flt: FilterEnvironment.t,
ctx: EvalCtx.t,
exp: DHExp.t,
act: FilterAction.t,
idx: int,
)
: (FilterAction.t, int, EvalCtx.t) => {
let composed = compose(ctx, exp);
let (pact, pidx) = (act, idx);
let (mact, midx) = FilterMatcher.matches(~env, ~exp=composed, ~act, flt);
let (act, idx) =
switch (ctx) {
| Filter(_, _) => (pact, pidx)
| _ => midx > pidx ? (mact, midx) : (pact, pidx)
};
let map = ((a, i, c), f: EvalCtx.t => EvalCtx.t) => {
(a, i, f(c));
};
let (let+) = map;
let (ract, ridx, rctx) =
switch (ctx) {
| Mark => (act, idx, EvalCtx.Mark)
| Closure(env, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Closure(env, ctx);
| Filter(Filter(flt'), ctx) =>
let flt = flt |> FilterEnvironment.extends(flt');
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Filter(Filter(flt'), ctx);
| Filter(Residue(idx', act'), ctx) =>
let (ract, ridx, rctx) =
if (idx > idx') {
matches(env, flt, ctx, exp, act, idx);
} else {
matches(env, flt, ctx, exp, act', idx');
};
if (act' |> snd == All) {
(ract, ridx, Filter(Residue(idx', act'), rctx));
} else {
(ract, ridx, rctx);
};
| Sequence1(ctx, d2) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Sequence1(ctx, d2);
| Sequence2(d1, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Sequence2(d1, ctx);
| Let1(d1, ctx, d3) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Let1(d1, ctx, d3);
| Let2(d1, d2, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Let2(d1, d2, ctx);
| Module1(d1, ctx, d3) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Module1(d1, ctx, d3);
| Module2(d1, d2, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Module2(d1, d2, ctx);
| Dot1(ctx, d2) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Dot1(ctx, d2);
| Dot2(d1, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Dot2(d1, ctx);
| Fun(dp, ty, ctx, name) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Fun(dp, ty, ctx, name);
| FixF(name, ty, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
FixF(name, ty, ctx);
| Ap1(ctx, d2) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Ap1(ctx, d2);
| Ap2(d1, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Ap2(d1, ctx);
| IfThenElse1(c, ctx, d2, d3) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
IfThenElse1(c, ctx, d2, d3);
| IfThenElse2(c, d1, ctx, d3) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
IfThenElse2(c, d1, ctx, d3);
| IfThenElse3(c, d1, d2, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
IfThenElse3(c, d1, d2, ctx);
| BinBoolOp1(op, ctx, d1) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
BinBoolOp1(op, ctx, d1);
| BinBoolOp2(op, d1, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
BinBoolOp2(op, d1, ctx);
| BinIntOp1(op, ctx, d2) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
BinIntOp1(op, ctx, d2);
| BinIntOp2(op, d1, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
BinIntOp2(op, d1, ctx);
| BinFloatOp1(op, ctx, d2) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
BinFloatOp1(op, ctx, d2);
| BinFloatOp2(op, d1, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
BinFloatOp2(op, d1, ctx);
| BinStringOp1(op, ctx, d2) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
BinStringOp1(op, ctx, d2);
| BinStringOp2(op, d1, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
BinStringOp2(op, d1, ctx);
| Tuple(ctx, ds) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Tuple(ctx, ds);
| ApBuiltin(name, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
ApBuiltin(name, ctx);
| Test(id, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Test(id, ctx);
| ListLit(u, i, ty, ctx, ds) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
ListLit(u, i, ty, ctx, ds);
| Cons1(ctx, d2) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Cons1(ctx, d2);
| Cons2(d1, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Cons2(d1, ctx);
| ListConcat1(ctx, d2) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
ListConcat1(ctx, d2);
| ListConcat2(d1, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
ListConcat2(d1, ctx);
| Prj(ctx, n) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Prj(ctx, n);
| NonEmptyHole(e, u, i, ctx) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
NonEmptyHole(e, u, i, ctx);
| Cast(ctx, ty, ty') =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
Cast(ctx, ty, ty');
| FailedCast(ctx, ty, ty') =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
FailedCast(ctx, ty, ty');
| InvalidOperation(ctx, error) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
InvalidOperation(ctx, error);
| ConsistentCase(Case(ctx, rs, i)) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
ConsistentCase(Case(ctx, rs, i));
| ConsistentCaseRule(dexp, dpat, ctx, rs, i) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
ConsistentCaseRule(dexp, dpat, ctx, rs, i);
| InconsistentBranches(u, i, Case(ctx, rs, ri)) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
InconsistentBranches(u, i, Case(ctx, rs, ri));
| InconsistentBranchesRule(dexp, u, i, dpat, ctx, rs, ri) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
InconsistentBranchesRule(dexp, u, i, dpat, ctx, rs, ri);
| TypAp(ctx, ty) =>
let+ ctx = matches(env, flt, ctx, exp, act, idx);
TypAp(ctx, ty);
};
switch (ctx) {
| Filter(_) => (ract, ridx, rctx)
| _ when midx > pidx && mact |> snd == All => (
ract,
ridx,
Filter(Residue(midx, mact), rctx),
)
| _ => (ract, ridx, rctx)
};
};

let should_hide_eval_obj =
(~settings, x: EvalObj.t): (FilterAction.action, EvalObj.t) =>
if (should_hide_step_kind(~settings, x.knd)) {
(Eval, x);
} else {
let (act, _, ctx) =
matches(ClosureEnvironment.empty, [], x.ctx, x.d_loc, (Step, One), 0);
switch (act) {
| (Eval, _) => (Eval, {...x, ctx})
| (Step, _) => (Step, {...x, ctx})
};
};

let should_hide_step = (~settings, x: step): (FilterAction.action, step) =>
if (should_hide_step_kind(~settings, x.knd)) {
(Eval, x);
} else {
let (act, _, ctx) =
matches(ClosureEnvironment.empty, [], x.ctx, x.d_loc, (Step, One), 0);
switch (act) {
| (Eval, _) => (Eval, {...x, ctx})
| (Step, _) => (Step, {...x, ctx})
};
};

let decompose = (~settings, d) =>
d |> decompose |> List.map(should_hide_eval_obj(~settings));

let evaluate_with_history = (~settings, d) => {
let state = ref(EvaluatorState.init);
let rec go = d =>
switch (decompose(d)) {
switch (decompose(~settings, d)) {
| [] => []
| [x, ..._] =>
| [(_, x), ..._] =>
switch (take_step(state, x.env, x.d_loc)) {
| None => []
| Some(d) =>
Expand Down
Loading

0 comments on commit 67986f0

Please sign in to comment.