From 16654e7ed90893f80aca3e475da1d29db7ca0dab Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Mon, 9 Sep 2024 22:34:49 +0800 Subject: [PATCH 1/4] refactor: use debug .. in for filter expression --- src/haz3lcore/dynamics/Casts.re | 1 + src/haz3lcore/dynamics/DHExp.re | 2 + src/haz3lcore/dynamics/Elaborator.re | 27 +++-- src/haz3lcore/dynamics/EvalCtx.re | 10 +- src/haz3lcore/dynamics/EvaluatorStep.re | 20 ++-- src/haz3lcore/dynamics/FilterAction.re | 10 ++ src/haz3lcore/dynamics/FilterEnvironment.re | 11 +- src/haz3lcore/dynamics/FilterMatcher.re | 29 ++++-- src/haz3lcore/dynamics/Stepper.re | 15 +-- src/haz3lcore/dynamics/Substitution.re | 25 +++-- src/haz3lcore/dynamics/Transition.re | 19 +++- src/haz3lcore/dynamics/TypeAssignment.re | 3 +- src/haz3lcore/dynamics/Unboxing.re | 1 + src/haz3lcore/lang/Form.re | 14 +-- src/haz3lcore/lang/term/Typ.re | 16 ++- src/haz3lcore/statics/MakeTerm.re | 9 +- src/haz3lcore/statics/Statics.re | 39 +++++-- src/haz3lcore/statics/Term.re | 6 ++ src/haz3lcore/statics/TermBase.re | 103 ++++--------------- src/haz3lcore/zipper/EditorUtil.re | 7 +- src/haz3lschool/Exercise.re | 14 ++- src/haz3lschool/SyntaxTest.re | 12 ++- src/haz3lweb/explainthis/Example.re | 8 +- src/haz3lweb/explainthis/ExplainThisForm.re | 2 + src/haz3lweb/explainthis/data/TerminalTyp.re | 13 +++ src/haz3lweb/view/ExplainThis.re | 12 ++- src/haz3lweb/view/Type.re | 1 + src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 51 ++++----- src/haz3lweb/view/dhcode/layout/HTypDoc.re | 2 + 29 files changed, 269 insertions(+), 213 deletions(-) diff --git a/src/haz3lcore/dynamics/Casts.re b/src/haz3lcore/dynamics/Casts.re index 170d057e76..9733d5f755 100644 --- a/src/haz3lcore/dynamics/Casts.re +++ b/src/haz3lcore/dynamics/Casts.re @@ -58,6 +58,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => { | Int | Float | String + | Filter | Var(_) | Rec(_) | Forall(_, {term: Unknown(_), _}) diff --git a/src/haz3lcore/dynamics/DHExp.re b/src/haz3lcore/dynamics/DHExp.re index f7651ba963..d89eb0f86f 100644 --- a/src/haz3lcore/dynamics/DHExp.re +++ b/src/haz3lcore/dynamics/DHExp.re @@ -51,6 +51,7 @@ let rec strip_casts = | MultiHole(_) | Seq(_) | Filter(_) + | Residue(_) | Let(_) | FixF(_) | TyAlias(_) @@ -129,6 +130,7 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => { | Match(_) | DynamicErrorHole(_) | Filter(_) + | Residue(_) | If(_) | EmptyHole | Invalid(_) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index c1f3aa12d7..ab40352d67 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -385,14 +385,27 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { Test(fresh_cast(e', t, Bool |> Typ.temp)) |> rewrap |> cast_from(Prod([]) |> Typ.temp); - | Filter(kind, e) => + | Filter(_, p, e) => + switch (p.term) { + | Ap(_, {term: Var(name), _}, arg) => + switch (FilterAction.t_of_string(name)) { + | Some(act) => + let (e', t) = elaborate(m, e); + let (p', _) = elaborate(m, arg); + Filter(Some(act), p', e') |> rewrap |> cast_from(t); + | None => + let (e', t) = elaborate(m, e); + let (p', _) = elaborate(m, p); + Filter(None, p', e') |> rewrap |> cast_from(t); + } + | _ => + let (e', t) = elaborate(m, e); + let (p', _) = elaborate(m, p); + Filter(None, p', e') |> rewrap |> cast_from(t); + } + | Residue(i, a, e) => let (e', t) = elaborate(m, e); - let kind' = - switch (kind) { - | Residue(_) => kind - | Filter({act, pat}) => Filter({act, pat: elaborate(m, pat) |> fst}) - }; - Filter(kind', e') |> rewrap |> cast_from(t); + Residue(i, a, e') |> rewrap |> cast_from(t); | Closure(env, e) => // Should we be elaborating the contents of the environment? let (e', t) = elaborate(m, e); diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re index bed931c8d3..e1ff329ced 100644 --- a/src/haz3lcore/dynamics/EvalCtx.re +++ b/src/haz3lcore/dynamics/EvalCtx.re @@ -3,7 +3,8 @@ open Util; [@deriving (show({with_path: false}), sexp, yojson)] type term = | Closure([@show.opaque] ClosureEnvironment.t, t) - | Filter(TermBase.StepperFilterKind.t, t) + | Filter(option(FilterAction.t), DHExp.t, t) + | Residue(int, FilterAction.t, t) | Seq1(t, DHExp.t) | Seq2(DHExp.t, t) | Let1(Pat.t, t, DHExp.t) @@ -56,9 +57,12 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => { | Closure(env, ctx) => let d = compose(ctx, d); Closure(env, d) |> wrap; - | Filter(flt, ctx) => + | Filter(act, pat, ctx) => let d = compose(ctx, d); - Filter(flt, d) |> wrap; + Filter(act, pat, d) |> wrap; + | Residue(idx, act, ctx) => + let d = compose(ctx, d); + Residue(idx, act, d) |> wrap; | Seq1(ctx, d2) => let d1 = compose(ctx, d); Seq(d1, d2) |> wrap; diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re index f25f25603f..caff2caf63 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -227,7 +227,7 @@ let rec matches = let (mact, midx) = FilterMatcher.matches(~env, ~exp=composed, ~act, flt); let (act, idx) = switch (ctx) { - | Term({term: Filter(_, _), _}) => (pact, pidx) + | Term({term: Filter(_, _, _), _}) => (pact, pidx) | _ => midx > pidx ? (mact, midx) : (pact, pidx) }; let map = ((a, i, c), f: EvalCtx.t => EvalCtx.t) => { @@ -243,11 +243,14 @@ let rec matches = | Closure(env, ctx) => let+ ctx = matches(env, flt, ctx, exp, act, idx); Closure(env, ctx) |> wrap_ids(ids); - | Filter(Filter(flt'), ctx) => - let flt = flt |> FilterEnvironment.extends(flt'); + | Filter(Some(fact), pat, ctx) => + let flt = flt |> FilterEnvironment.extends({act: fact, pat}); let+ ctx = matches(env, flt, ctx, exp, act, idx); - Filter(Filter(flt'), ctx) |> wrap_ids(ids); - | Filter(Residue(idx', act'), ctx) => + Filter(Some(fact), pat, ctx) |> wrap_ids(ids); + | Filter(fact, pat, ctx) => + let+ ctx = matches(env, flt, ctx, exp, act, idx); + Filter(fact, pat, ctx) |> wrap_ids(ids); + | Residue(idx', act', ctx) => let (ract, ridx, rctx) = if (idx > idx') { matches(env, flt, ctx, exp, act, idx); @@ -258,10 +261,7 @@ let rec matches = ( ract, ridx, - Term({ - term: Filter(Residue(idx', act'), rctx), - ids: [Id.mk()], - }), + Term({term: Residue(idx', act', rctx), ids: [Id.mk()]}), ); } else { (ract, ridx, rctx); @@ -380,7 +380,7 @@ let rec matches = | _ when midx > pidx && mact |> snd == All => ( ract, ridx, - Term({term: Filter(Residue(midx, mact), rctx), ids: [Id.mk()]}), + Term({term: Residue(midx, mact, rctx), ids: [Id.mk()]}), ) | _ => (ract, ridx, rctx) }; diff --git a/src/haz3lcore/dynamics/FilterAction.re b/src/haz3lcore/dynamics/FilterAction.re index 6a4dce5ca3..782b2cc755 100644 --- a/src/haz3lcore/dynamics/FilterAction.re +++ b/src/haz3lcore/dynamics/FilterAction.re @@ -11,6 +11,16 @@ type count = [@deriving (show({with_path: false}), sexp, yojson)] type t = (action, count); +let t_of_string = s => { + switch (s) { + | "pause" => Some((Step, One)) + | "debug" => Some((Step, All)) + | "hide" => Some((Eval, One)) + | "eval" => Some((Eval, All)) + | _ => None + }; +}; + let string_of_t = v => { switch (v) { | (Step, One) => "pause" diff --git a/src/haz3lcore/dynamics/FilterEnvironment.re b/src/haz3lcore/dynamics/FilterEnvironment.re index 284e7353d3..d5034a4c3c 100644 --- a/src/haz3lcore/dynamics/FilterEnvironment.re +++ b/src/haz3lcore/dynamics/FilterEnvironment.re @@ -1,2 +1,9 @@ -type t = list(TermBase.StepperFilterKind.filter); -let extends = (flt, env) => [flt, ...env]; +type filter = { + act: FilterAction.t, + pat: Exp.t, +}; +type t = list(filter); +let extends = (flt: filter, env: list(filter)): list(filter) => [ + flt, + ...env, +]; diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index d6d0bcc543..4e65071dc3 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -100,6 +100,8 @@ let rec matches_exp = : bool => { let matches_exp = (~denv=denv, ~fenv=fenv, d, f) => matches_exp(~denv, d, ~fenv, f); + Printf.printf("d: %s\n", DHExp.show(d)); + Printf.printf("f: %s\n", DHExp.show(f)); if (d == f) { true; } else { @@ -154,7 +156,12 @@ let rec matches_exp = | (_, EmptyHole) | (_, Constructor("$e", _)) => true - | (Cast(d, _, _), Cast(f, _, _)) => matches_exp(d, f) + | (Cast(d, dty1, dty2), Cast(f, fty1, fty2)) => + matches_exp(d, f) + && matches_typ(dty1, fty1) + && matches_typ(dty2, fty2) + | (Cast(_), _) => false + | (Closure(denv, d), Closure(fenv, f)) => matches_exp(~denv, d, ~fenv, f) @@ -163,9 +170,8 @@ let rec matches_exp = | (_, FailedCast(f, _, _)) => matches_exp(d, f) | (Closure(denv, d), _) => matches_exp(~denv, d, f) - | (Cast(d, _, _), _) => matches_exp(d, f) | (FailedCast(d, _, _), _) => matches_exp(d, f) - | (Filter(Residue(_), d), _) => matches_exp(d, f) + | (Residue(_, _, d), _) => matches_exp(d, f) | (Var(dx), Var(fx)) => if (String.starts_with(~prefix=alpha_magic, dx) @@ -198,8 +204,8 @@ let rec matches_exp = | (Deferral(x), Deferral(y)) => x == y | (Deferral(_), _) => false - | (Filter(df, dd), Filter(ff, fd)) => - TermBase.StepperFilterKind.fast_equal(df, ff) && matches_exp(dd, fd) + | (Filter(da, dp, dd), Filter(fa, fp, fd)) => + da == fa && matches_exp(dp, fp) && matches_exp(dd, fd) | (Filter(_), _) => false | (Bool(dv), Bool(fv)) => dv == fv @@ -225,8 +231,15 @@ let rec matches_exp = | (BuiltinFun(dn), BuiltinFun(fn)) => dn == fn | (BuiltinFun(_), _) => false - | (TypFun(pat1, d1, s1), TypFun(pat2, d2, s2)) => - s1 == s2 && matches_utpat(pat1, pat2) && matches_exp(d1, d2) + | (TypFun(dpat, d, _), TypFun(fpat, f, _)) => + switch (dpat |> IdTagged.term_of, fpat |> IdTagged.term_of) { + | (_, EmptyHole) => matches_exp(d, f) + | _ => + let id = alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4)); + let d' = DHExp.ty_subst(Typ.Var(id) |> IdTagged.fresh, dpat, d); + let f' = DHExp.ty_subst(Typ.Var(id) |> IdTagged.fresh, fpat, f); + matches_exp(d', f'); + } | (TypFun(_), _) => false | (Fun(dp1, d1, Some(denv), _), Fun(fp1, f1, Some(fenv), _)) => @@ -390,7 +403,7 @@ let matches = ( ~env: ClosureEnvironment.t, ~exp: DHExp.t, - ~flt: TermBase.StepperFilterKind.filter, + ~flt: FilterEnvironment.filter, ) : option(FilterAction.t) => if (matches_exp(~denv=env, exp, ~fenv=env, flt.pat)) { diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re index 8b977cdf5f..f1341493c3 100644 --- a/src/haz3lcore/dynamics/Stepper.re +++ b/src/haz3lcore/dynamics/Stepper.re @@ -36,7 +36,7 @@ let rec matches = let (mact, midx) = FilterMatcher.matches(~env, ~exp=composed, ~act, flt); let (act, idx) = switch (ctx) { - | Term({term: Filter(_, _), _}) => (pact, pidx) + | Term({term: Filter(_, _, _), _}) => (pact, pidx) | _ => midx > pidx ? (mact, midx) : (pact, pidx) }; let map = ((a, i, c), f) => { @@ -52,11 +52,12 @@ let rec matches = | Closure(env, ctx) => let+ ctx = matches(env, flt, ctx, exp, act, idx); Closure(env, ctx) |> rewrap; - | Filter(Filter(flt'), ctx) => - let flt = flt |> FilterEnvironment.extends(flt'); + | Filter(Some(fact), fpat, ctx) => + let flt = flt |> FilterEnvironment.extends({act: fact, pat: fpat}); let+ ctx = matches(env, flt, ctx, exp, act, idx); - Filter(Filter(flt'), ctx) |> rewrap; - | Filter(Residue(idx', act'), ctx) => + Filter(Some(fact), fpat, ctx) |> rewrap; + | Filter(None, _, _) => failwith("Invalid filter expression") + | Residue(idx', act', ctx) => let (ract, ridx, rctx) = if (idx > idx') { matches(env, flt, ctx, exp, act, idx); @@ -64,7 +65,7 @@ let rec matches = matches(env, flt, ctx, exp, act', idx'); }; if (act' |> snd == All) { - (ract, ridx, Filter(Residue(idx', act'), rctx) |> rewrap); + (ract, ridx, Residue(idx', act', rctx) |> rewrap); } else { (ract, ridx, rctx); }; @@ -167,7 +168,7 @@ let rec matches = | _ when midx > pidx && mact |> snd == All => ( ract, ridx, - Term({term: Filter(Residue(midx, mact), rctx), ids: [Id.mk()]}), + Term({term: Residue(midx, mact, rctx), ids: [Id.mk()]}), ) | _ => (ract, ridx, rctx) }; diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re index 5d918e520b..0178dac440 100644 --- a/src/haz3lcore/dynamics/Substitution.re +++ b/src/haz3lcore/dynamics/Substitution.re @@ -14,10 +14,23 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => { let d3 = subst_var(m, d1, x, d3); let d4 = subst_var(m, d1, x, d4); Seq(d3, d4) |> rewrap; - | Filter(filter, dbody) => + | Filter(None, pat, dbody) => + let pat = + switch (pat.term) { + | Ap(direction, fn, arg) => + let arg = subst_var(m, d1, x, arg); + {...pat, term: TermBase.Exp.Ap(direction, fn, arg)}; + | _ => pat + }; + let dbody = subst_var(m, d1, x, dbody); + Filter(None, pat, dbody) |> rewrap; + | Filter(Some(act), pat, dbody) => + let pat = subst_var(m, d1, x, pat); + let dbody = subst_var(m, d1, x, dbody); + Filter(Some(act), pat, dbody) |> rewrap; + | Residue(idx, act, dbody) => let dbody = subst_var(m, d1, x, dbody); - let filter = subst_var_filter(m, d1, x, filter); - Filter(filter, dbody) |> rewrap; + Residue(idx, act, dbody) |> rewrap; | Let(dp, d3, d4) => let d3 = subst_var(m, d1, x, d3); let d4 = @@ -159,12 +172,6 @@ and subst_var_env = ); ClosureEnvironment.wrap(id, map); -} - -and subst_var_filter = - (m, d1: DHExp.t, x: Var.t, flt: TermBase.StepperFilterKind.t) - : TermBase.StepperFilterKind.t => { - flt |> TermBase.StepperFilterKind.map(subst_var(m, d1, x)); }; let subst = (m, env: Environment.t, d: DHExp.t): DHExp.t => diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index a54c9d18d8..b9d922c645 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -768,10 +768,23 @@ module Transition = (EV: EV_MODE) => { | TyAlias(_, _, d) => let. _ = otherwise(env, d); Step({expr: d, state_update, kind: RemoveTypeAlias, is_value: false}); - | Filter(f1, d1) => - let. _ = otherwise(env, d1 => Filter(f1, d1) |> rewrap) + | Filter(a1, p1, d1) => + let. _ = otherwise(env, d1 => Filter(a1, p1, d1) |> rewrap) and. d1 = - req_final(req(state, env), d1 => Filter(f1, d1) |> wrap_ctx, d1); + req_final( + req(state, env), + d1 => Filter(a1, p1, d1) |> wrap_ctx, + d1, + ); + Step({expr: d1, state_update, kind: CompleteFilter, is_value: true}); + | Residue(a1, p1, d1) => + let. _ = otherwise(env, d1 => Residue(a1, p1, d1) |> rewrap) + and. d1 = + req_final( + req(state, env), + d1 => Residue(a1, p1, d1) |> wrap_ctx, + d1, + ); Step({expr: d1, state_update, kind: CompleteFilter, is_value: true}); }; }; diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re index f4979d94bf..c03308df32 100644 --- a/src/haz3lcore/dynamics/TypeAssignment.re +++ b/src/haz3lcore/dynamics/TypeAssignment.re @@ -132,7 +132,8 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) => | Closure(env, d) => let* ctx' = env_extend_ctx(env, m, ctx); typ_of_dhexp(ctx', m, d); - | Filter(_, d) => typ_of_dhexp(ctx, m, d) + | Filter(_, _, d) => typ_of_dhexp(ctx, m, d) + | Residue(_, _, d) => typ_of_dhexp(ctx, m, d) | Var(name) => let* var = Ctx.lookup_var(ctx, name); Some(var.typ); diff --git a/src/haz3lcore/dynamics/Unboxing.re b/src/haz3lcore/dynamics/Unboxing.re index 400620026c..639f7a32c5 100644 --- a/src/haz3lcore/dynamics/Unboxing.re +++ b/src/haz3lcore/dynamics/Unboxing.re @@ -185,6 +185,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) = Seq(_) | Test(_) | Filter(_) | + Residue(_) | Closure(_) | Parens(_) | Cons(_) | diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 1990461239..5e3e871fc0 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -318,11 +318,7 @@ let forms: list((string, t)) = [ mk(ds, ["|", "=>"], mk_bin'(P.rule_sep, Rul, Exp, [Pat], Exp)), ), ("pipeline", mk_infix("|>", Exp, P.eqs)), // in OCaml, pipeline precedence is in same class as '=', '<', etc. - // DOUBLE DELIMITERS - ("filter_hide", mk(ds, ["hide", "in"], mk_pre(P.let_, Exp, [Exp]))), - ("filter_eval", mk(ds, ["eval", "in"], mk_pre(P.let_, Exp, [Exp]))), - ("filter_pause", mk(ds, ["pause", "in"], mk_pre(P.let_, Exp, [Exp]))), - ("filter_debug", mk(ds, ["debug", "in"], mk_pre(P.let_, Exp, [Exp]))), + ("filter", mk(ds, ["debug", "in"], mk_pre(P.let_, Exp, [Exp]))), // TRIPLE DELIMITERS ("let_", mk(ds, ["let", "=", "in"], mk_pre(P.let_, Exp, [Pat, Exp]))), ( @@ -332,8 +328,12 @@ let forms: list((string, t)) = [ ("if_", mk(ds, ["if", "then", "else"], mk_pre(P.if_, Exp, [Exp, Exp]))), ]; -let get: String.t => t = - name => Util.ListUtil.assoc_err(name, forms, "Forms.get"); +let get: String.t => t = { + name => { + print_endline("Forms.get: name = " ++ name); + Util.ListUtil.assoc_err(name, forms, "Forms.get"); + }; +}; let delims: list(Token.t) = forms diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re index 5dc0b73aaa..9bf7cdae2c 100644 --- a/src/haz3lcore/lang/term/Typ.re +++ b/src/haz3lcore/lang/term/Typ.re @@ -12,6 +12,7 @@ type cls = | Float | Bool | String + | Filter | Arrow | Prod | Sum @@ -51,6 +52,7 @@ let cls_of_term: term => cls = | Float => Float | Bool => Bool | String => String + | Filter => Filter | List(_) => List | Arrow(_) => Arrow | Var(_) => Var @@ -72,6 +74,7 @@ let show_cls: cls => string = | Float | String | Bool => "Base type" + | Filter => "Filter type" | Var => "Type variable" | Constructor => "Sum constructor" | List => "List type" @@ -92,6 +95,7 @@ let rec is_arrow = (typ: t) => { | Float | Bool | String + | Filter | List(_) | Prod(_) | Var(_) @@ -111,6 +115,7 @@ let rec is_forall = (typ: t) => { | Float | Bool | String + | Filter | Arrow(_) | List(_) | Prod(_) @@ -155,7 +160,8 @@ let rec free_vars = (~bound=[], ty: t): list(Var.t) => | Int | Float | Bool - | String => [] + | String + | Filter => [] | Ap(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2) | Var(v) => List.mem(v, bound) ? [] : [v] | Parens(ty) => free_vars(~bound, ty) @@ -256,6 +262,8 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) => | (Bool, _) => None | (String, String) => Some(ty1) | (String, _) => None + | (Filter, Filter) => Some(ty1) + | (Filter, _) => None | (Arrow(ty1, ty2), Arrow(ty1', ty2')) => let* ty1 = join'(ty1, ty1'); let+ ty2 = join'(ty2, ty2'); @@ -291,6 +299,7 @@ let rec match_synswitch = (t1: t, t2: t) => { | (Float, _) | (Bool, _) | (String, _) + | (Filter, _) | (Var(_), _) | (Ap(_), _) | (Rec(_), _) @@ -347,7 +356,8 @@ let rec normalize = (ctx: Ctx.t, ty: t): t => { | Int | Float | Bool - | String => ty + | String + | Filter => ty | Parens(t) => Parens(normalize(ctx, t)) |> rewrap | List(t) => List(normalize(ctx, t)) |> rewrap | Ap(t1, t2) => Ap(normalize(ctx, t1), normalize(ctx, t2)) |> rewrap @@ -478,6 +488,7 @@ let rec needs_parens = (ty: t): bool => | Float | String | Bool + | Filter | Var(_) => false | Rec(_, _) | Forall(_, _) => true @@ -505,6 +516,7 @@ let rec pretty_print = (ty: t): string => | Float => "Float" | Bool => "Bool" | String => "String" + | Filter => "Filter" | Var(tvar) => tvar | List(t) => "[" ++ pretty_print(t) ++ "]" | Arrow(t1, t2) => paren_pretty_print(t1) ++ " -> " ++ pretty_print(t2) diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 673af0bb89..5e81712624 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -220,14 +220,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | (["fix", "->"], [Pat(pat)]) => FixF(pat, r, None) | (["typfun", "->"], [TPat(tpat)]) => TypFun(tpat, r, None) | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r) - | (["hide", "in"], [Exp(filter)]) => - Filter(Filter({act: (Eval, One), pat: filter}), r) - | (["eval", "in"], [Exp(filter)]) => - Filter(Filter({act: (Eval, All), pat: filter}), r) - | (["pause", "in"], [Exp(filter)]) => - Filter(Filter({act: (Step, One), pat: filter}), r) - | (["debug", "in"], [Exp(filter)]) => - Filter(Filter({act: (Step, All), pat: filter}), r) + | (["debug", "in"], [Exp(pat)]) => Filter(None, pat, r) | (["type", "=", "in"], [TPat(tpat), Typ(def)]) => TyAlias(tpat, def, r) | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) => diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index aca1ce0389..e86f972bca 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -311,15 +311,35 @@ and uexp_to_info_map = | Test(e) => let (e, m) = go(~mode=Ana(Bool |> Typ.temp), e, m); add(~self=Just(Prod([]) |> Typ.temp), ~co_ctx=e.co_ctx, m); - | Filter(Filter({pat: cond, _}), body) => - let (cond, m) = go(~mode=Syn, cond, m, ~is_in_filter=true); + | Filter(_, pat, body) => let (body, m) = go(~mode, body, m); - add( - ~self=Just(body.ty), - ~co_ctx=CoCtx.union([cond.co_ctx, body.co_ctx]), - m, - ); - | Filter(Residue(_), body) => + switch (pat.term) { + | Ap(_, fn, arg) => + switch (fn.term) { + | Var("eval" | "hide" | "pause" | "debug") => + let (arg, m) = go(~mode=Syn, arg, m, ~is_in_filter=true); + add( + ~self=Just(body.ty), + ~co_ctx=CoCtx.union([arg.co_ctx, body.co_ctx]), + m, + ); + | _ => + let (pat, m) = go(~mode=Ana(Filter |> Typ.temp), pat, m); + add( + ~self=Just(body.ty), + ~co_ctx=CoCtx.union([pat.co_ctx, body.co_ctx]), + m, + ); + } + | _ => + let (pat, m) = go(~mode=Ana(Filter |> Typ.temp), pat, m); + add( + ~self=Just(body.ty), + ~co_ctx=CoCtx.union([pat.co_ctx, body.co_ctx]), + m, + ); + }; + | Residue(_, _, body) => let (body, m) = go(~mode, body, m); add(~self=Just(body.ty), ~co_ctx=CoCtx.union([body.co_ctx]), m); | Seq(e1, e2) => @@ -841,7 +861,8 @@ and utyp_to_info_map = | Int | Float | Bool - | String => add(m) + | String + | Filter => add(m) | Var(_) => /* Names are resolved in Info.status_typ */ add(m) diff --git a/src/haz3lcore/statics/Term.re b/src/haz3lcore/statics/Term.re index 0493150865..29434c426e 100644 --- a/src/haz3lcore/statics/Term.re +++ b/src/haz3lcore/statics/Term.re @@ -308,6 +308,7 @@ module Exp = { | Seq | Test | Filter + | Residue | Closure | Parens | Cons @@ -357,6 +358,7 @@ module Exp = { | Seq(_) => Seq | Test(_) => Test | Filter(_) => Filter + | Residue(_) => Residue | Closure(_) => Closure | Parens(_) => Parens | Cons(_) => Cons @@ -399,6 +401,7 @@ module Exp = { | Seq => "Sequence expression" | Test => "Test" | Filter => "Filter" + | Residue => "Residue" | Closure => "Closure" | Parens => "Parenthesized expression" | Cons => "Cons" @@ -442,6 +445,7 @@ module Exp = { | Seq(_) | Test(_) | Filter(_) + | Residue(_) | Cons(_) | ListConcat(_) | Closure(_) @@ -486,6 +490,7 @@ module Exp = { | Seq(_) | Test(_) | Filter(_) + | Residue(_) | Cons(_) | ListConcat(_) | UnOp(_) @@ -536,6 +541,7 @@ module Exp = { | Var(_) | Let(_) | Filter(_) + | Residue(_) | TyAlias(_) | Ap(_) | TypAp(_) diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index f0585955c6..f6d3775745 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -164,7 +164,8 @@ and Exp: { | If(t, t, t) | Seq(t, t) | Test(t) - | Filter(StepperFilterKind.t, t) + | Filter(option(FilterAction.t), t, t) + | Residue(int, FilterAction.t, t) | Closure([@show.opaque] ClosureEnvironment.t, t) | Parens(t) // ( | Cons(t, t) @@ -231,7 +232,8 @@ and Exp: { | If(t, t, t) | Seq(t, t) | Test(t) - | Filter(StepperFilterKind.t, t) + | Filter(option(FilterAction.t), t, t) + | Residue(int, FilterAction.t, t) | Closure([@show.opaque] ClosureEnvironment.t, t) | Parens(t) | Cons(t, t) @@ -263,15 +265,6 @@ and Exp: { TPat.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any); let any_map_term = Any.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any); - let flt_map_term = - StepperFilterKind.map_term( - ~f_exp, - ~f_pat, - ~f_typ, - ~f_tpat, - ~f_rul, - ~f_any, - ); let rec_call = ({term, _} as exp: t) => { ...exp, term: @@ -307,7 +300,9 @@ and Exp: { If(exp_map_term(e1), exp_map_term(e2), exp_map_term(e3)) | Seq(e1, e2) => Seq(exp_map_term(e1), exp_map_term(e2)) | Test(e) => Test(exp_map_term(e)) - | Filter(f, e) => Filter(flt_map_term(f), exp_map_term(e)) + | Filter(act, pat, e) => + Filter(act, exp_map_term(pat), exp_map_term(e)) + | Residue(idx, act, e) => Residue(idx, act, exp_map_term(e)) | Closure(env, e) => Closure(env, exp_map_term(e)) | Parens(e) => Parens(exp_map_term(e)) | Cons(e1, e2) => Cons(exp_map_term(e1), exp_map_term(e2)) @@ -387,8 +382,10 @@ and Exp: { | (Seq(e1, e2), Seq(e3, e4)) => fast_equal(e1, e3) && fast_equal(e2, e4) | (Test(e1), Test(e2)) => fast_equal(e1, e2) - | (Filter(f1, e1), Filter(f2, e2)) => - StepperFilterKind.fast_equal(f1, f2) && fast_equal(e1, e2) + | (Filter(_, f1, e1), Filter(_, f2, e2)) => + fast_equal(f1, f2) && fast_equal(e1, e2) + | (Residue(i1, a1, e1), Residue(i2, a2, e2)) => + i1 == i2 && a1 == a2 && fast_equal(e1, e2) | (Closure(c1, e1), Closure(c2, e2)) => ClosureEnvironment.id_equal(c1, c2) && fast_equal(e1, e2) | (Cons(e1, e2), Cons(e3, e4)) => @@ -433,6 +430,7 @@ and Exp: { | (Seq(_), _) | (Test(_), _) | (Filter(_), _) + | (Residue(_), _) | (Closure(_), _) | (Cons(_), _) | (ListConcat(_), _) @@ -610,6 +608,7 @@ and Typ: { | Float | Bool | String + | Filter | Var(string) | List(t) | Arrow(t, t) @@ -662,6 +661,7 @@ and Typ: { | Float | Bool | String + | Filter | Var(string) | List(t) | Arrow(t, t) @@ -703,6 +703,7 @@ and Typ: { | Int | Float | String + | Filter | Var(_) => term | List(t) => List(typ_map_term(t)) | Unknown(Hole(MultiHole(things))) => @@ -738,6 +739,7 @@ and Typ: { | Float => Float |> rewrap | Bool => Bool |> rewrap | String => String |> rewrap + | Filter => Filter |> rewrap | Unknown(prov) => Unknown(prov) |> rewrap | Arrow(ty1, ty2) => Arrow(subst(s, x, ty1), subst(s, x, ty2)) |> rewrap @@ -786,6 +788,8 @@ and Typ: { | (Bool, _) => false | (String, String) => true | (String, _) => false + | (Filter, Filter) => true + | (Filter, _) => false | (Ap(t1, t2), Ap(t1', t2')) => eq_internal(n, t1, t1') && eq_internal(n, t2, t2') | (Ap(_), _) => false @@ -1097,75 +1101,4 @@ and ClosureEnvironment: { let placeholder = wrap(Id.invalid, Environment.empty); let without_keys = keys => update(Environment.without_keys(keys)); -} -and StepperFilterKind: { - [@deriving (show({with_path: false}), sexp, yojson)] - type filter = { - pat: Exp.t, - act: FilterAction.t, - }; - - [@deriving (show({with_path: false}), sexp, yojson)] - type t = - | Filter(filter) - | Residue(int, FilterAction.t); - - let map_term: - ( - ~f_exp: (Exp.t => Exp.t, Exp.t) => Exp.t=?, - ~f_pat: (Pat.t => Pat.t, Pat.t) => Pat.t=?, - ~f_typ: (Typ.t => Typ.t, Typ.t) => Typ.t=?, - ~f_tpat: (TPat.t => TPat.t, TPat.t) => TPat.t=?, - ~f_rul: (Rul.t => Rul.t, Rul.t) => Rul.t=?, - ~f_any: (Any.t => Any.t, Any.t) => Any.t=?, - t - ) => - t; - - let map: (Exp.t => Exp.t, t) => t; - - let fast_equal: (t, t) => bool; -} = { - [@deriving (show({with_path: false}), sexp, yojson)] - type filter = { - pat: Exp.t, - act: FilterAction.t, - }; - - [@deriving (show({with_path: false}), sexp, yojson)] - type t = - | Filter(filter) - | Residue(int, FilterAction.t); - - let map = (mapper, filter) => { - switch (filter) { - | Filter({act, pat}) => Filter({act, pat: mapper(pat)}) - | Residue(idx, act) => Residue(idx, act) - }; - }; - - let map_term = - ( - ~f_exp=continue, - ~f_pat=continue, - ~f_typ=continue, - ~f_tpat=continue, - ~f_rul=continue, - ~f_any=continue, - ) => { - let exp_map_term = - Exp.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any); - fun - | Filter({pat: e, act}) => Filter({pat: exp_map_term(e), act}) - | Residue(i, a) => Residue(i, a); - }; - - let fast_equal = (f1, f2) => - switch (f1, f2) { - | (Filter({pat: e1, act: a1}), Filter({pat: e2, act: a2})) => - Exp.fast_equal(e1, e2) && a1 == a2 - | (Residue(i1, a1), Residue(i2, a2)) => i1 == i2 && a1 == a2 - | (Filter(_), _) - | (Residue(_), _) => false - }; }; diff --git a/src/haz3lcore/zipper/EditorUtil.re b/src/haz3lcore/zipper/EditorUtil.re index ff59e48f55..886e213264 100644 --- a/src/haz3lcore/zipper/EditorUtil.re +++ b/src/haz3lcore/zipper/EditorUtil.re @@ -36,9 +36,12 @@ let rec append_exp = (e1: Exp.t, e2: Exp.t): Exp.t => { | Seq(e11, e12) => let e12' = append_exp(e12, e2); {ids: e1.ids, copied: false, term: Seq(e11, e12')}; - | Filter(kind, ebody) => + | Filter(act, pat, ebody) => let ebody' = append_exp(ebody, e2); - {ids: e1.ids, copied: false, term: Filter(kind, ebody')}; + {ids: e1.ids, copied: false, term: Filter(act, pat, ebody')}; + | Residue(idx, act, ebody) => + let ebody' = append_exp(ebody, e2); + {ids: e1.ids, copied: false, term: Residue(idx, act, ebody')}; | Let(p, edef, ebody) => let ebody' = append_exp(ebody, e2); {ids: e1.ids, copied: false, term: Let(p, edef, ebody')}; diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re index b5e7dfc76d..f9a93790b9 100644 --- a/src/haz3lschool/Exercise.re +++ b/src/haz3lschool/Exercise.re @@ -572,14 +572,12 @@ module F = (ExerciseEnv: ExerciseEnv) => { Exp.{ term: Exp.Filter( - Filter({ - act: FilterAction.(act, One), - pat: { - term: Constructor("$e", Unknown(Internal) |> Typ.temp), - copied: false, - ids: [Id.mk()], - }, - }), + Some(FilterAction.(act, One)), + { + term: Constructor("$e", Unknown(Internal) |> Typ.temp), + copied: false, + ids: [Id.mk()], + }, term, ), copied: false, diff --git a/src/haz3lschool/SyntaxTest.re b/src/haz3lschool/SyntaxTest.re index 23dff72251..9f557adf4e 100644 --- a/src/haz3lschool/SyntaxTest.re +++ b/src/haz3lschool/SyntaxTest.re @@ -98,7 +98,8 @@ let rec find_fn = | TyAlias(_, _, u1) | Test(u1) | Closure(_, u1) - | Filter(_, u1) => l |> find_fn(name, u1) + | Filter(_, _, u1) + | Residue(_, _, u1) => l |> find_fn(name, u1) | Ap(_, u1, u2) | Seq(u1, u2) | Cons(u1, u2) @@ -194,7 +195,8 @@ let rec var_mention = (name: string, uexp: Exp.t): bool => { | Parens(u) | UnOp(_, u) | TyAlias(_, _, u) - | Filter(_, u) => var_mention(name, u) + | Filter(_, _, u) + | Residue(_, _, u) => var_mention(name, u) | DynamicErrorHole(u, _) => var_mention(name, u) | FailedCast(u, _, _) => var_mention(name, u) | FixF(args, body, _) => @@ -255,7 +257,8 @@ let rec var_applied = (name: string, uexp: Exp.t): bool => { | Parens(u) | UnOp(_, u) | TyAlias(_, _, u) - | Filter(_, u) => var_applied(name, u) + | Filter(_, _, u) + | Residue(_, _, u) => var_applied(name, u) | TypAp(u, _) => switch (u.term) { | Var(x) => x == name ? true : false @@ -346,7 +349,8 @@ let rec tail_check = (name: string, uexp: Exp.t): bool => { | Test(_) => false | TyAlias(_, _, u) | Cast(u, _, _) - | Filter(_, u) + | Filter(_, _, u) + | Residue(_, _, u) | Closure(_, u) | TypFun(_, u, _) | TypAp(u, _) diff --git a/src/haz3lweb/explainthis/Example.re b/src/haz3lweb/explainthis/Example.re index 9408167cf6..c811fded3c 100644 --- a/src/haz3lweb/explainthis/Example.re +++ b/src/haz3lweb/explainthis/Example.re @@ -118,10 +118,10 @@ let mk_if = mk_tile(Form.get("if_")); let mk_test = mk_tile(Form.get("test")); let mk_case = mk_tile(Form.get("case")); let mk_rule = mk_tile(Form.get("rule")); -let mk_hide = mk_tile(Form.get("filter_hide")); -let mk_eval = mk_tile(Form.get("filter_eval")); -let mk_pause = mk_tile(Form.get("filter_pause")); -let mk_debug = mk_tile(Form.get("filter_debug")); +let mk_hide = mk_tile(Form.get("filter")); +let mk_eval = mk_tile(Form.get("filter")); +let mk_pause = mk_tile(Form.get("filter")); +let mk_debug = mk_tile(Form.get("filter")); let mk_unquote = mk_tile(Form.get("unquote")); let linebreak = () => mk_secondary(Form.linebreak); let space = () => mk_secondary(Form.space); diff --git a/src/haz3lweb/explainthis/ExplainThisForm.re b/src/haz3lweb/explainthis/ExplainThisForm.re index a2291253e5..c243e7091a 100644 --- a/src/haz3lweb/explainthis/ExplainThisForm.re +++ b/src/haz3lweb/explainthis/ExplainThisForm.re @@ -209,6 +209,7 @@ type form_id = | FloatTyp | BoolTyp | StrTyp + | FilterTyp | VarTyp | ListTyp | ForallTyp @@ -303,6 +304,7 @@ type group_id = | FloatTyp | BoolTyp | StrTyp + | FilterTyp | VarTyp | ListTyp | ForallTyp diff --git a/src/haz3lweb/explainthis/data/TerminalTyp.re b/src/haz3lweb/explainthis/data/TerminalTyp.re index 8566be4762..b4adad00b8 100644 --- a/src/haz3lweb/explainthis/data/TerminalTyp.re +++ b/src/haz3lweb/explainthis/data/TerminalTyp.re @@ -45,6 +45,17 @@ let str_typ: form = { }; }; +let filter_typ: form = { + let explanation = "The `Filter` type classifies the filter used in `debug .. in` statement."; + { + id: FilterTyp, + syntactic_form: [typ("Filter")], + expandable_id: None, + explanation, + examples: [], + }; +}; + let var_typ = (name: string): form => { let explanation = "`%s` is a type variable."; { @@ -65,3 +76,5 @@ let bool: group = {id: BoolTyp, forms: [bool_typ]}; let str: group = {id: StrTyp, forms: [str_typ]}; let var = (name: string): group => {id: VarTyp, forms: [var_typ(name)]}; + +let filter: group = {id: FilterTyp, forms: [filter_typ]}; diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re index cbfdf4df9f..f6902276a0 100644 --- a/src/haz3lweb/view/ExplainThis.re +++ b/src/haz3lweb/view/ExplainThis.re @@ -1710,35 +1710,36 @@ let get_doc = ), SeqExp.seqs, ); - | Filter(Filter({act: (Step, One), pat}), body) => + | Filter(Some((Step, One)), pat, body) => message_single( FilterExp.filter_pause( ~p_id=UExp.rep_id(pat), ~body_id=UExp.rep_id(body), ), ) - | Filter(Filter({act: (Step, All), pat}), body) => + | Filter(Some((Step, All)), pat, body) => message_single( FilterExp.filter_debug( ~p_id=UExp.rep_id(pat), ~body_id=UExp.rep_id(body), ), ) - | Filter(Filter({act: (Eval, All), pat}), body) => + | Filter(Some((Eval, All)), pat, body) => message_single( FilterExp.filter_eval( ~p_id=UExp.rep_id(pat), ~body_id=UExp.rep_id(body), ), ) - | Filter(Filter({act: (Eval, One), pat}), body) => + | Filter(Some((Eval, One)), pat, body) => message_single( FilterExp.filter_hide( ~p_id=UExp.rep_id(pat), ~body_id=UExp.rep_id(body), ), ) - | Filter(_) => simple("Internal expression") + | Filter(None, _, _) + | Residue(_) => simple("Internal expression") | Test(body) => let body_id = List.nth(body.ids, 0); get_message( @@ -2137,6 +2138,7 @@ let get_doc = | Float => get_message(TerminalTyp.float) | Bool => get_message(TerminalTyp.bool) | String => get_message(TerminalTyp.str) + | Filter => get_message(TerminalTyp.str) | List(elem) => let elem_id = List.nth(elem.ids, 0); get_message( diff --git a/src/haz3lweb/view/Type.re b/src/haz3lweb/view/Type.re index 622dcf766e..812f4e89cf 100644 --- a/src/haz3lweb/view/Type.re +++ b/src/haz3lweb/view/Type.re @@ -29,6 +29,7 @@ let rec view_ty = (~strip_outer_parens=false, ty: Haz3lcore.Typ.t): Node.t => | Int => ty_view("Int", "Int") | Float => ty_view("Float", "Float") | String => ty_view("String", "String") + | Filter => ty_view("Filter", "Filter") | Bool => ty_view("Bool", "Bool") | Var(name) => ty_view("Var", name) | Rec(name, t) => diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re index ffb0eed0c5..f55762bca5 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re @@ -63,7 +63,8 @@ let rec precedence = (~show_function_bodies, ~show_casts: bool, d: DHExp.t) => { | BuiltinFun(_) | Deferral(_) | Undefined - | Filter(_) => DHDoc_common.precedence_const + | Filter(_) + | Residue(_) => DHDoc_common.precedence_const | Cast(d1, _, _) => show_casts ? DHDoc_common.precedence_Ap : precedence'(d1) | DeferredAp(_) @@ -252,34 +253,26 @@ let mk = switch (DHExp.term_of(d)) { | Parens(d') => go'(d') | Closure(env', d') => go'(d', ~env=env') - | Filter(flt, d') => - if (settings.show_stepper_filters) { - switch (flt) { - | Filter({pat, act}) => - let keyword = FilterAction.string_of_t(act); - let flt_doc = go_formattable(pat); - vseps([ - hcats([ - DHDoc_common.Delim.mk(keyword), - flt_doc - |> DHDoc_common.pad_child( - ~inline_padding=(space(), space()), - ~enforce_inline=false, - ), - DHDoc_common.Delim.mk("in"), - ]), - go'(d'), - ]); - | Residue(_, act) => - let keyword = FilterAction.string_of_t(act); - vseps([DHDoc_common.Delim.mk(keyword), go'(d')]); - }; - } else { - switch (flt) { - | Residue(_) => go'(d') - | Filter(_) => go'(d') - }; - } + | Filter(Some(act), pat, d') when settings.show_stepper_filters => + let keyword = FilterAction.string_of_t(act); + let flt_doc = go_formattable(pat); + vseps([ + hcats([ + DHDoc_common.Delim.mk(keyword), + flt_doc + |> DHDoc_common.pad_child( + ~inline_padding=(space(), space()), + ~enforce_inline=false, + ), + DHDoc_common.Delim.mk("in"), + ]), + go'(d'), + ]); + | Filter(_, _, d') => go'(d') + | Residue(_, act, d') when settings.show_stepper_filters => + let keyword = FilterAction.string_of_t(act); + vseps([DHDoc_common.Delim.mk(keyword), go'(d')]); + | Residue(_, _, d') => go'(d') /* Hole expressions must appear within a closure in the postprocessed result */ diff --git a/src/haz3lweb/view/dhcode/layout/HTypDoc.re b/src/haz3lweb/view/dhcode/layout/HTypDoc.re index 996d01f607..17298c9cb4 100644 --- a/src/haz3lweb/view/dhcode/layout/HTypDoc.re +++ b/src/haz3lweb/view/dhcode/layout/HTypDoc.re @@ -18,6 +18,7 @@ let precedence = (ty: Typ.t): int => | Float | Bool | String + | Filter | Unknown(_) | Var(_) | Forall(_) @@ -75,6 +76,7 @@ let rec mk = (~parenthesize=false, ~enforce_inline: bool, ty: Typ.t): t => { | Float => (text("Float"), parenthesize) | Bool => (text("Bool"), parenthesize) | String => (text("String"), parenthesize) + | Filter => (text("Filter"), parenthesize) | Var(name) => (text(name), parenthesize) | List(ty) => ( hcats([ From 5af8b12f9b9539622bc43ded775d17620ba03bac Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Mon, 23 Sep 2024 21:37:41 +0800 Subject: [PATCH 2/4] support completion in debug ... in --- src/haz3lcore/dynamics/Builtins.re | 19 +++++++ src/haz3lcore/dynamics/FilterAction.re | 8 +-- src/haz3lcore/lang/Form.re | 1 - src/haz3lcore/statics/Statics.re | 78 ++++++++++++++++++-------- 4 files changed, 77 insertions(+), 29 deletions(-) diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re index 4479989fd5..ddcf9bfc8e 100644 --- a/src/haz3lcore/dynamics/Builtins.re +++ b/src/haz3lcore/dynamics/Builtins.re @@ -371,6 +371,25 @@ let ctx_init: Ctx.t = { |> Ctx.add_ctrs(_, "$Meta", Id.invalid, meta_cons_map); }; +let filter_keyword_ctx_init: Ctx.t = { + let impl = _ => failwith("evaluating filter keyword"); + Pervasives.builtins + |> fn("eval", Unknown(Internal), Filter, impl) + |> fn("hide", Unknown(Internal), Filter, impl) + |> fn("stop", Unknown(Internal), Filter, impl) + |> fn("step", Unknown(Internal), Filter, impl) + |> List.map( + fun + | (name, Const(typ, _)) => Ctx.VarEntry({name, typ, id: Id.invalid}) + | (name, Fn(t1, t2, _)) => + Ctx.VarEntry({ + name, + typ: Arrow(t1, t2) |> Typ.fresh, + id: Id.invalid, + }), + ); +}; + let forms_init: forms = List.filter_map( fun diff --git a/src/haz3lcore/dynamics/FilterAction.re b/src/haz3lcore/dynamics/FilterAction.re index 782b2cc755..014f2db2a6 100644 --- a/src/haz3lcore/dynamics/FilterAction.re +++ b/src/haz3lcore/dynamics/FilterAction.re @@ -13,8 +13,8 @@ type t = (action, count); let t_of_string = s => { switch (s) { - | "pause" => Some((Step, One)) - | "debug" => Some((Step, All)) + | "stop" => Some((Step, One)) + | "step" => Some((Step, All)) | "hide" => Some((Eval, One)) | "eval" => Some((Eval, All)) | _ => None @@ -23,8 +23,8 @@ let t_of_string = s => { let string_of_t = v => { switch (v) { - | (Step, One) => "pause" - | (Step, All) => "debug" + | (Step, One) => "stop" + | (Step, All) => "step" | (Eval, One) => "hide" | (Eval, All) => "eval" }; diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re index 5e3e871fc0..7412fa15be 100644 --- a/src/haz3lcore/lang/Form.re +++ b/src/haz3lcore/lang/Form.re @@ -330,7 +330,6 @@ let forms: list((string, t)) = [ let get: String.t => t = { name => { - print_endline("Forms.get: name = " ++ name); Util.ListUtil.assoc_err(name, forms, "Forms.get"); }; }; diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index e86f972bca..e8af1667fd 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -312,33 +312,57 @@ and uexp_to_info_map = let (e, m) = go(~mode=Ana(Bool |> Typ.temp), e, m); add(~self=Just(Prod([]) |> Typ.temp), ~co_ctx=e.co_ctx, m); | Filter(_, pat, body) => - let (body, m) = go(~mode, body, m); - switch (pat.term) { - | Ap(_, fn, arg) => - switch (fn.term) { - | Var("eval" | "hide" | "pause" | "debug") => - let (arg, m) = go(~mode=Syn, arg, m, ~is_in_filter=true); - add( - ~self=Just(body.ty), - ~co_ctx=CoCtx.union([arg.co_ctx, body.co_ctx]), - m, - ); + let (pat, m) = { + let uexp = pat; + let ids = pat.ids; + let add' = (~self, ~co_ctx, m) => { + let info = + Info.derived_exp(~uexp, ~ctx, ~mode, ~ancestors, ~self, ~co_ctx); + (info, add_info(ids, InfoExp(info), m)); + }; + let add = (~self, ~co_ctx, m) => add'(~self=Common(self), ~co_ctx, m); + let ancestors = [UExp.rep_id(uexp)] @ ancestors; + let uexp_to_info_map = + ( + ~ctx, + ~mode=Mode.Syn, + ~is_in_filter=is_in_filter, + ~ancestors=ancestors, + uexp: UExp.t, + m: Map.t, + ) => { + uexp_to_info_map(~ctx, ~mode, ~is_in_filter, ~ancestors, uexp, m); + }; + let go' = uexp_to_info_map(~ancestors); + let go = go'(~ctx); + switch (pat.term) { + | Ap(_, fn, arg) => + let fn_mode = + Mode.of_ap(ctx, Ana(Filter |> Typ.temp), UExp.ctr_name(fn)); + let (fn, m) = + go'(~ctx=Builtins.filter_keyword_ctx_init, ~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); | _ => - let (pat, m) = go(~mode=Ana(Filter |> Typ.temp), pat, m); - add( - ~self=Just(body.ty), - ~co_ctx=CoCtx.union([pat.co_ctx, body.co_ctx]), + go'( + ~ctx=Builtins.filter_keyword_ctx_init, + ~mode=Ana(Filter |> Typ.temp), + pat, m, - ); - } - | _ => - let (pat, m) = go(~mode=Ana(Filter |> Typ.temp), pat, m); - add( - ~self=Just(body.ty), - ~co_ctx=CoCtx.union([pat.co_ctx, body.co_ctx]), - m, - ); + ) + }; }; + let (body, m) = go(~mode, body, m); + add( + ~self=Just(body.ty), + ~co_ctx=CoCtx.union([pat.co_ctx, body.co_ctx]), + m, + ); | Residue(_, _, body) => let (body, m) = go(~mode, body, m); add(~self=Just(body.ty), ~co_ctx=CoCtx.union([body.co_ctx]), m); @@ -351,6 +375,12 @@ and uexp_to_info_map = 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); + Printf.printf("uexp_to_info_map: Ap: uexp = %s\n", UExp.show(uexp)); + Printf.printf( + "uexp_to_info_map: Ap: ty_in = %s, ty_out = %s\n", + Typ.show(ty_in), + Typ.show(ty_out), + ); let (arg, m) = go(~mode=Ana(ty_in), arg, m); let self: Self.t = Id.is_nullary_ap_flag(arg.term.ids) From b28c2603456633445268f941d3543313ebc13b33 Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Fri, 4 Oct 2024 16:29:02 +0800 Subject: [PATCH 3/4] fix: typing error for $e and $v --- src/haz3lcore/dynamics/EvaluatorStep.re | 16 -- src/haz3lcore/dynamics/EvaluatorStep.rei | 59 +++++++ src/haz3lcore/dynamics/FilterMatcher.re | 2 - src/haz3lcore/dynamics/Stepper.re | 178 --------------------- src/haz3lcore/statics/Statics.re | 10 +- src/haz3lweb/explainthis/data/FilterExp.re | 19 ++- src/haz3lweb/view/ExplainThis.re | 32 ++++ 7 files changed, 107 insertions(+), 209 deletions(-) create mode 100644 src/haz3lcore/dynamics/EvaluatorStep.rei diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re index caff2caf63..d86417ec42 100644 --- a/src/haz3lcore/dynamics/EvaluatorStep.re +++ b/src/haz3lcore/dynamics/EvaluatorStep.re @@ -413,19 +413,3 @@ let should_hide_step = (~settings, x: step): (FilterAction.action, step) => let decompose = (~settings, d, st) => decompose(d, st) |> List.map(should_hide_eval_obj(~settings)); - -let evaluate_with_history = (~settings, d) => { - let state = ref(EvaluatorState.init); - let rec go = d => - switch (decompose(~settings, d, state^)) { - | [] => [] - | [(_, x), ..._] => - switch (take_step(state, x.env, x.d_loc)) { - | None => [] - | Some(d) => - let next = EvalCtx.compose(x.ctx, d); - [next, ...go(next)]; - } - }; - go(d); -}; diff --git a/src/haz3lcore/dynamics/EvaluatorStep.rei b/src/haz3lcore/dynamics/EvaluatorStep.rei new file mode 100644 index 0000000000..71b1db2792 --- /dev/null +++ b/src/haz3lcore/dynamics/EvaluatorStep.rei @@ -0,0 +1,59 @@ +[@deriving (show({with_path: false}), sexp, yojson)] +type step = { + d: DHExp.t, // technically can be calculated from d_loc and ctx + state: EvaluatorState.t, + d_loc: DHExp.t, // the expression at the location given by ctx + d_loc': DHExp.t, + ctx: EvalCtx.t, + knd: Transition.step_kind, +}; + +module EvalObj: { + [@deriving (show({with_path: false}), sexp, yojson)] + type t = { + env: ClosureEnvironment.t, // technically can be calculated from ctx + d_loc: DHExp.t, + ctx: EvalCtx.t, + knd: Transition.step_kind, + }; + + let mk: + (EvalCtx.t, ClosureEnvironment.t, DHExp.t, Transition.step_kind) => t; + let get_ctx: t => EvalCtx.t; + let get_kind: t => Transition.step_kind; + let wrap: (EvalCtx.t => EvalCtx.t, t) => t; +}; + +let decompose: + (~settings: CoreSettings.Evaluation.t, DHExp.t, EvaluatorState.t) => + list((FilterAction.action, EvalObj.t)); + +module TakeStep: { + module TakeStepEVMode: { + include + Transition.EV_MODE with + type result = option(DHExp.t) and type state = ref(EvaluatorState.t); + }; +}; + +let take_step: + (TakeStep.TakeStepEVMode.state, ClosureEnvironment.t, DHExp.t) => + TakeStep.TakeStepEVMode.result; + +let matches: + ( + ClosureEnvironment.t, + FilterEnvironment.t, + EvalCtx.t, + DHExp.t, + FilterAction.t, + int + ) => + (FilterAction.t, int, EvalCtx.t); + +let should_hide_eval_obj: + (~settings: CoreSettings.Evaluation.t, EvalObj.t) => + (FilterAction.action, EvalObj.t); + +let should_hide_step: + (~settings: CoreSettings.Evaluation.t, step) => (FilterAction.action, step); diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index 4e65071dc3..f5f69aac85 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -100,8 +100,6 @@ let rec matches_exp = : bool => { let matches_exp = (~denv=denv, ~fenv=fenv, d, f) => matches_exp(~denv, d, ~fenv, f); - Printf.printf("d: %s\n", DHExp.show(d)); - Printf.printf("f: %s\n", DHExp.show(f)); if (d == f) { true; } else { diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re index f1341493c3..6bed91b06e 100644 --- a/src/haz3lcore/dynamics/Stepper.re +++ b/src/haz3lcore/dynamics/Stepper.re @@ -21,184 +21,6 @@ type t = { stepper_state, }; -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 = EvalCtx.compose(ctx, exp); - let (pact, pidx) = (act, idx); - let (mact, midx) = FilterMatcher.matches(~env, ~exp=composed, ~act, flt); - let (act, idx) = - switch (ctx) { - | Term({term: Filter(_, _, _), _}) => (pact, pidx) - | _ => midx > pidx ? (mact, midx) : (pact, pidx) - }; - let map = ((a, i, c), f) => { - (a, i, f(c)); - }; - let (let+) = map; - let (ract, ridx, rctx) = - switch (ctx) { - | Mark => (act, idx, EvalCtx.Mark) - | Term({term, ids}) => - let rewrap = term => EvalCtx.Term({term, ids}); - switch ((term: EvalCtx.term)) { - | Closure(env, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Closure(env, ctx) |> rewrap; - | Filter(Some(fact), fpat, ctx) => - let flt = flt |> FilterEnvironment.extends({act: fact, pat: fpat}); - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Filter(Some(fact), fpat, ctx) |> rewrap; - | Filter(None, _, _) => failwith("Invalid filter expression") - | 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, Residue(idx', act', rctx) |> rewrap); - } else { - (ract, ridx, rctx); - }; - | Seq1(ctx, d2) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Seq1(ctx, d2) |> rewrap; - | Seq2(d1, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Seq2(d1, ctx) |> rewrap; - | Let1(d1, ctx, d3) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Let1(d1, ctx, d3) |> rewrap; - | Let2(d1, d2, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Let2(d1, d2, ctx) |> rewrap; - | Fun(dp, ctx, env', name) => - let+ ctx = - matches(Option.value(~default=env, env'), flt, ctx, exp, act, idx); - Fun(dp, ctx, env', name) |> rewrap; - | FixF(name, ctx, env') => - let+ ctx = - matches(Option.value(~default=env, env'), flt, ctx, exp, act, idx); - FixF(name, ctx, env') |> rewrap; - | Ap1(dir, ctx, d2) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Ap1(dir, ctx, d2) |> rewrap; - | Ap2(dir, d1, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Ap2(dir, d1, ctx) |> rewrap; - | TypAp(ctx, ty) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - TypAp(ctx, ty) |> rewrap; - | DeferredAp1(ctx, d2) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - DeferredAp1(ctx, d2) |> rewrap; - | DeferredAp2(d1, ctx, ds) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - DeferredAp2(d1, ctx, ds) |> rewrap; - | If1(ctx, d2, d3) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - If1(ctx, d2, d3) |> rewrap; - | If2(d1, ctx, d3) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - If2(d1, ctx, d3) |> rewrap; - | If3(d1, d2, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - If3(d1, d2, ctx) |> rewrap; - | UnOp(op, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - UnOp(op, ctx) |> rewrap; - | BinOp1(op, ctx, d1) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - BinOp1(op, ctx, d1) |> rewrap; - | BinOp2(op, d1, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - BinOp2(op, d1, ctx) |> rewrap; - | Tuple(ctx, ds) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Tuple(ctx, ds) |> rewrap; - | Test(ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Test(ctx) |> rewrap; - | ListLit(ctx, ds) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - ListLit(ctx, ds) |> rewrap; - | Cons1(ctx, d2) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Cons1(ctx, d2) |> rewrap; - | Cons2(d1, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Cons2(d1, ctx) |> rewrap; - | ListConcat1(ctx, d2) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - ListConcat1(ctx, d2) |> rewrap; - | ListConcat2(d1, ctx) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - ListConcat2(d1, ctx) |> rewrap; - | MultiHole(ctx, (dl, dr)) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - MultiHole(ctx, (dl, dr)) |> rewrap; - | Cast(ctx, ty, ty') => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - Cast(ctx, ty, ty') |> rewrap; - | FailedCast(ctx, ty, ty') => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - FailedCast(ctx, ty, ty') |> rewrap; - | DynamicErrorHole(ctx, error) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - DynamicErrorHole(ctx, error) |> rewrap; - | MatchScrut(ctx, rs) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - MatchScrut(ctx, rs) |> rewrap; - | MatchRule(scr, p, ctx, rs) => - let+ ctx = matches(env, flt, ctx, exp, act, idx); - MatchRule(scr, p, ctx, rs) |> rewrap; - }; - }; - switch (ctx) { - | Term({term: Filter(_), _}) => (ract, ridx, rctx) - | _ when midx > pidx && mact |> snd == All => ( - ract, - ridx, - Term({term: Residue(midx, mact, rctx), ids: [Id.mk()]}), - ) - | _ => (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 get_elab = ({history, _}: t): Elaborator.Elaboration.t => { let (d, _) = Aba.last_a(history); {d: d}; diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index e8af1667fd..ffd2a5f377 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -281,7 +281,7 @@ and uexp_to_info_map = | _ => e.term }, }; - let ty_in = Typ.Var("$Meta") |> Typ.temp; + let ty_in = Typ.Unknown(Internal) |> Typ.temp; let ty_out = Typ.Unknown(Internal) |> Typ.temp; let (e, m) = go(~mode=Ana(ty_in), e, m); add(~self=Just(ty_out), ~co_ctx=e.co_ctx, m); @@ -342,7 +342,7 @@ and uexp_to_info_map = let (fn, m) = go'(~ctx=Builtins.filter_keyword_ctx_init, ~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 (arg, m) = go(~mode=Ana(ty_in), arg, m, ~is_in_filter=true); let self: Self.t = Id.is_nullary_ap_flag(arg.term.ids) && !Typ.is_consistent(ctx, ty_in, Prod([]) |> Typ.temp) @@ -375,12 +375,6 @@ and uexp_to_info_map = 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); - Printf.printf("uexp_to_info_map: Ap: uexp = %s\n", UExp.show(uexp)); - Printf.printf( - "uexp_to_info_map: Ap: ty_in = %s, ty_out = %s\n", - Typ.show(ty_in), - Typ.show(ty_out), - ); let (arg, m) = go(~mode=Ana(ty_in), arg, m); let self: Self.t = Id.is_nullary_ap_flag(arg.term.ids) diff --git a/src/haz3lweb/explainthis/data/FilterExp.re b/src/haz3lweb/explainthis/data/FilterExp.re index 9e66a0b7fd..98dc073e4c 100644 --- a/src/haz3lweb/explainthis/data/FilterExp.re +++ b/src/haz3lweb/explainthis/data/FilterExp.re @@ -18,8 +18,9 @@ let filter_pause = (~p_id: Id.t, ~body_id: Id.t): Simple.t => { examples: [ { sub_id: FilterStep, - term: mk_example("eval $e + $e in\n(1 + 2) * (3 + 4)"), - message: "The expression (1 * 2) + (3 * 4) is guarded by a pause filter expression pause $v + $v, which instruct the evaluator to pause the evaluation when it sees a value is added to another value. After evaluating subterms (1 * 2) and (3 * 4), the expression turns into 2 + 12. 2 matches the first $v pattern, and 12 matches the second $v pattern. Therefore, the evaluator stops when the expression steps to 2 + 12", + term: mk_example({|debug stop($v + $v) in +(1 + 2) * (3 + 4)|}), + message: "The expression (1 * 2) + (3 * 4) is guarded by a pause filter expression debug pause($v + $v), which instruct the evaluator to pause the evaluation when it sees a value is added to another value. After evaluating subterms (1 * 2) and (3 * 4), the expression turns into 2 + 12. 2 matches the first $v pattern, and 12 matches the second $v pattern. Therefore, the evaluator stops when the expression steps to 2 + 12", }, ], }; @@ -42,9 +43,13 @@ let filter_eval = (~p_id: Id.t, ~body_id: Id.t): Simple.t => { sub_id: FilterEval, term: mk_example( - "pause $e in\nhide let = in in\nlet x = 1 in\nlet y = 2 in\nx + y", + {|debug stop($e) in +debug eval(let = in) in +let x = 1 in +let x = y in +x + y|}, ), - message: "pause $e in instruct the evaluator to act like a single-stepper, e.g. stop at every step. The hide filter expression instructs the evaluator to skip over all evaluator steps that destructs perform substitution on a let-expression. Here, the substitution of variable x and y is skipped over and we directly got 1 + 2 in the result area.", + message: "debug stop($e) in instruct the evaluator to act like a single-stepper, e.g. stop at every step. The hide filter expression debug eval(let = in) instructs the evaluator to evaluate all let-expressions. Here, the evaluation of the two let-expressions are skipped over, and we get the final answer 2 immediately.", }, ], }; @@ -67,7 +72,11 @@ let filter_hide = (~p_id: Id.t, ~body_id: Id.t): Simple.t => { sub_id: FilterHide, term: mk_example( - "pause $e in\nhide let = in in\nlet x = 1 in\nlet y = 2 in\nx + y", + {|debug stop($e) in +debug hide(let = in) in +let x = 1 in +let y = 2 in +x + y|}, ), message: "pause $e in instruct the evaluator to act like a single-stepper, e.g. stop at every step. The hide filter expression instructs the evaluator to skip over all evaluator steps that destructs perform substitution on a let-expression. Here, the substitution of variable x and y is skipped over and we directly got 1 + 2 in the result area.", }, diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re index f6902276a0..5b9907c63a 100644 --- a/src/haz3lweb/view/ExplainThis.re +++ b/src/haz3lweb/view/ExplainThis.re @@ -1738,6 +1738,38 @@ let get_doc = ~body_id=UExp.rep_id(body), ), ) + | Filter(None, {term: Ap(_, {term: Var(var), _}, _), _} as pat, body) => + switch (var) { + | "stop" => + message_single( + FilterExp.filter_pause( + ~p_id=UExp.rep_id(pat), + ~body_id=UExp.rep_id(body), + ), + ) + | "step" => + message_single( + FilterExp.filter_debug( + ~p_id=UExp.rep_id(pat), + ~body_id=UExp.rep_id(body), + ), + ) + | "hide" => + message_single( + FilterExp.filter_hide( + ~p_id=UExp.rep_id(pat), + ~body_id=UExp.rep_id(body), + ), + ) + | "eval" => + message_single( + FilterExp.filter_eval( + ~p_id=UExp.rep_id(pat), + ~body_id=UExp.rep_id(body), + ), + ) + | _ => simple("Internal expression") + } | Filter(None, _, _) | Residue(_) => simple("Internal expression") | Test(body) => From 5bb445fcce7b184d0abeb8f152fad580630fc3bf Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Mon, 23 Dec 2024 22:46:34 +0800 Subject: [PATCH 4/4] fix statics --- src/haz3lcore/dynamics/EvalCtx.re | 3 +-- src/haz3lcore/dynamics/FilterMatcher.re | 16 +++++++++++--- src/haz3lcore/statics/Statics.re | 16 +++++++------- src/haz3lschool/Exercise.re | 29 ++++++++++++------------- 4 files changed, 36 insertions(+), 28 deletions(-) diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re index 218165f5e8..7aea680536 100644 --- a/src/haz3lcore/dynamics/EvalCtx.re +++ b/src/haz3lcore/dynamics/EvalCtx.re @@ -121,8 +121,7 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => { ListLit(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap; | MultiHole(ctx, (ld, rd)) => let d = compose(ctx, d); - MultiHole(ListUtil.rev_concat(ld, [TermBase.Exp(d), ...rd])) - |> wrap; + MultiHole(ListUtil.rev_concat(ld, [TermBase.Exp(d), ...rd])) |> wrap; | Let1(dp, ctx, d2) => let d = compose(ctx, d); Let(dp, d, d2) |> wrap; diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index 390fc3765b..4d90f79b75 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -203,7 +203,7 @@ let rec matches_exp = | (Deferral(_), _) => false | (Filter(da, dp, dd), Filter(fa, fp, fd)) => - da == fa && matches_exp(dp, fp) && matches_exp(dd, fd) + da == fa && matches_exp(dd, fd) | (Filter(_), _) => false | (Bool(dv), Bool(fv)) => dv == fv @@ -234,8 +234,18 @@ let rec matches_exp = | (_, EmptyHole) => matches_exp(d, f) | _ => let id = alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4)); - let d' = DHExp.ty_subst((Var(id) : TermBase.typ_term) |> IdTagged.fresh, dpat, d); - let f' = DHExp.ty_subst((Var(id) : TermBase.typ_term) |> IdTagged.fresh, fpat, f); + let d' = + DHExp.ty_subst( + (Var(id): TermBase.typ_term) |> IdTagged.fresh, + dpat, + d, + ); + let f' = + DHExp.ty_subst( + (Var(id): TermBase.typ_term) |> IdTagged.fresh, + fpat, + f, + ); matches_exp(d', f'); } | (TypFun(_), _) => false diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index 8710a5683d..a2e29b4df6 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -337,17 +337,17 @@ and uexp_to_info_map = let go = go'(~ctx); switch (pat.term) { | Ap(_, fn, arg) => - let fn_mode = - Mode.of_ap(ctx, Ana(Filter |> Typ.temp), UExp.ctr_name(fn)); + let self_ty = Unknown(Internal) |> Typ.temp; + let fn_mode = Mode.of_ap(ctx, Ana(self_ty), UExp.ctr_name(fn)); let (fn, m) = go'(~ctx=Builtins.filter_keyword_ctx_init, ~mode=fn_mode, fn, m); - let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty); + let (ty_in, _) = Typ.matched_arrow(ctx, fn.ty); let (arg, m) = go(~mode=Ana(ty_in), arg, m, ~is_in_filter=true); - 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); + add( + ~self=Just(self_ty), + ~co_ctx=CoCtx.union([fn.co_ctx, arg.co_ctx]), + m, + ); | _ => go'( ~ctx=Builtins.filter_keyword_ctx_init, diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re index 05274e938b..2b2d0706de 100644 --- a/src/haz3lschool/Exercise.re +++ b/src/haz3lschool/Exercise.re @@ -568,21 +568,20 @@ module F = (ExerciseEnv: ExerciseEnv) => { hidden_tests: 'a, }; - let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t => - { - term: - Filter( - Some(FilterAction.(act, One)), - { - term: Constructor("$e", Unknown(Internal) |> Typ.temp), - copied: false, - ids: [Id.mk()], - }, - term, - ), - copied: false, - ids: [Id.mk()], - }; + let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t => { + term: + Filter( + Some(FilterAction.(act, One)), + { + term: Constructor("$e", Unknown(Internal) |> Typ.temp), + copied: false, + ids: [Id.mk()], + }, + term, + ), + copied: false, + ids: [Id.mk()], + }; let term_of = (editor: Editor.t): UExp.t => MakeTerm.from_zip_for_sem(editor.state.zipper).term;