From 11e1583bc54d8e947160e7063efc4574b0a83450 Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Sun, 18 Aug 2024 01:48:07 +0800 Subject: [PATCH 1/8] fix fix-point matching --- src/haz3lcore/dynamics/FilterMatcher.re | 95 ++++++------------------- 1 file changed, 22 insertions(+), 73 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index fc70d83756..d5dfa07a2d 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -20,7 +20,7 @@ let rec matches_exp = // HACK[Matt]: ignore fixpoints in comparison, to allow pausing on fixpoint steps | (FixF(dp, dc, _), FixF(fp, fc, _)) => - dp == fp + matches_pat(dp, fp) && matches_exp( ~denv= denv |> ClosureEnvironment.without_keys(dp |> DHPat.bound_vars), @@ -33,14 +33,25 @@ let rec matches_exp = matches_exp( ~denv=denv |> ClosureEnvironment.without_keys(DHPat.bound_vars(dp)), dc, + ~fenv=fenv |> ClosureEnvironment.without_keys(DHPat.bound_vars(dp)), f, ) - | (_, FixF(fp, fc, _)) => - matches_exp( - d, - ~fenv=fenv |> ClosureEnvironment.without_keys(DHPat.bound_vars(fp)), - fc, - ) + | (_, FixF(fp, fc, Some(env))) => + let fenv = + switch (DHPat.get_var(fp)) { + | Some(fname) => + env + |> ClosureEnvironment.map_of + |> Environment.union( + Environment.singleton(( + fname, + {...f, term: TermBase.Exp.FixF(fp, fc, Some(env))}, + )), + ) + |> ClosureEnvironment.of_environment + | None => env + }; + matches_exp(~denv, d, ~fenv, fc); | (_, Constructor("$v", _)) => switch (ValueChecker.check_value((), denv, d)) { @@ -65,74 +76,12 @@ let rec matches_exp = | (FailedCast(d, _, _), _) => matches_exp(d, f) | (Filter(Residue(_), d), _) => matches_exp(d, f) - | (Var(dx), Var(fx)) when String.starts_with(dx, ~prefix="__mutual__") => - String.starts_with(fx, ~prefix="__mutual__") && dx == fx | (Var(dx), Var(fx)) => switch ( - ClosureEnvironment.lookup(denv, dx) |> Option.map(DHExp.term_of), - ClosureEnvironment.lookup(fenv, fx) |> Option.map(DHExp.term_of), + ClosureEnvironment.lookup(denv, dx), + ClosureEnvironment.lookup(fenv, fx), ) { - | ( - Some(Fun(_, _, Some(denv), Some(dname)) as d), - Some(Fun(_, _, Some(fenv), Some(fname)) as f), - ) - when - ClosureEnvironment.lookup(denv, dname) - |> Option.map(DHExp.term_of) == Some(d) - && ClosureEnvironment.lookup(fenv, fname) - |> Option.map(DHExp.term_of) == Some(f) => - matches_exp( - ~denv=ClosureEnvironment.without_keys([dname], denv), - d |> Exp.fresh, - ~fenv=ClosureEnvironment.without_keys([fname], fenv), - f |> Exp.fresh, - ) - | ( - Some(Fun(_, _, Some(denv), Some(dname)) as d), - Some(Fun(_, _, _, Some(fname)) as f), - ) - when - ClosureEnvironment.lookup(denv, dname) - |> Option.map(DHExp.term_of) == Some(d) - && ClosureEnvironment.lookup(fenv, fname) - |> Option.map(DHExp.term_of) == Some(f) => - matches_exp( - ~denv=ClosureEnvironment.without_keys([dname], denv), - d |> DHExp.fresh, - ~fenv=ClosureEnvironment.without_keys([fname], fenv), - f |> DHExp.fresh, - ) - | ( - Some(Fun(_, _, _, Some(dname)) as d), - Some(Fun(_, _, _, Some(fname)) as f), - ) - when - ClosureEnvironment.lookup(denv, dname) - |> Option.map(DHExp.term_of) == Some(d) - && ClosureEnvironment.lookup(fenv, fname) - |> Option.map(DHExp.term_of) == Some(f) => - matches_exp( - ~denv=ClosureEnvironment.without_keys([dname], denv), - d |> DHExp.fresh, - ~fenv=ClosureEnvironment.without_keys([fname], fenv), - f |> DHExp.fresh, - ) - | ( - Some(Fun(_, _, _, Some(dname)) as d), - Some(Fun(_, _, _, Some(fname)) as f), - ) - when - ClosureEnvironment.lookup(denv, dname) - |> Option.map(DHExp.term_of) == Some(d) - && ClosureEnvironment.lookup(fenv, fname) - |> Option.map(DHExp.term_of) == Some(f) => - matches_exp( - ~denv=ClosureEnvironment.without_keys([dname], denv), - d |> DHExp.fresh, - ~fenv=ClosureEnvironment.without_keys([fname], denv), - f |> DHExp.fresh, - ) - | (Some(d), Some(f)) => matches_exp(d |> Exp.fresh, f |> Exp.fresh) + | (Some(d), Some(f)) => matches_exp(d, f) | (Some(_), None) => false | (None, Some(_)) => false | (None, None) => true @@ -330,7 +279,7 @@ and matches_pat = (d: Pat.t, f: Pat.t): bool => { | (ListLit(_), _) => false | (Constructor(dt, _), Constructor(ft, _)) => dt == ft | (Constructor(_), _) => false - | (Var(_), Var(_)) => true + | (Var(dx), Var(fx)) => String.equal(dx, fx) | (Var(_), _) => false | (Tuple(dl), Tuple(fl)) => switch ( From a0489bdca38f0c152a5562786e4ed1f6fb5abb55 Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Sun, 18 Aug 2024 02:58:02 +0800 Subject: [PATCH 2/8] make it more generic --- src/haz3lcore/dynamics/FilterMatcher.re | 88 ++++++++++++++++++------- 1 file changed, 66 insertions(+), 22 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index d5dfa07a2d..62aa36803d 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -1,3 +1,58 @@ +let evaluate_extend_env = + (new_bindings: Environment.t, to_extend: ClosureEnvironment.t) + : ClosureEnvironment.t => { + to_extend + |> ClosureEnvironment.map_of + |> Environment.union(new_bindings) + |> ClosureEnvironment.of_environment; +}; + +let evaluate_extend_env_with_pat = + ( + ids: list(Uuidm.t), + copied: bool, + pat: DHPat.t, + exp: DHExp.t, + to_extend: ClosureEnvironment.t, + ) + : ClosureEnvironment.t => { + switch (DHPat.get_var(pat)) { + | Some(fname) => + evaluate_extend_env( + Environment.singleton(( + fname, + { + ids, + copied, + IdTagged.term: TermBase.Exp.FixF(pat, exp, Some(to_extend)), + }, + )), + to_extend, + ) + | None => + let bindings = DHPat.bound_vars(pat); + let substitutions = + List.map( + binding => + ( + binding, + TermBase.Exp.Let( + pat, + { + ids, + copied, + term: TermBase.Exp.FixF(pat, exp, Some(to_extend)), + }, + TermBase.Exp.Var(binding) |> IdTagged.fresh, + ) + |> IdTagged.fresh, + ), + bindings, + ); + evaluate_extend_env(Environment.of_list(substitutions), to_extend); + }; +}; + let rec matches_exp = ( ~denv: ClosureEnvironment.t, @@ -29,28 +84,17 @@ let rec matches_exp = fenv |> ClosureEnvironment.without_keys(fp |> DHPat.bound_vars), fc, ) - | (FixF(dp, dc, _), _) => - matches_exp( - ~denv=denv |> ClosureEnvironment.without_keys(DHPat.bound_vars(dp)), - dc, - ~fenv=fenv |> ClosureEnvironment.without_keys(DHPat.bound_vars(dp)), - f, - ) - | (_, FixF(fp, fc, Some(env))) => - let fenv = - switch (DHPat.get_var(fp)) { - | Some(fname) => - env - |> ClosureEnvironment.map_of - |> Environment.union( - Environment.singleton(( - fname, - {...f, term: TermBase.Exp.FixF(fp, fc, Some(env))}, - )), - ) - |> ClosureEnvironment.of_environment - | None => env - }; + | (FixF(dp, dc, None), _) => + let denv = evaluate_extend_env_with_pat(d.ids, d.copied, dp, dc, denv); + matches_exp(~denv, dc, ~fenv, f); + | (FixF(dp, dc, Some(denv)), _) => + let denv = evaluate_extend_env_with_pat(d.ids, d.copied, dp, dc, denv); + matches_exp(~denv, dc, ~fenv, f); + | (_, FixF(fp, fc, None)) => + let fenv = evaluate_extend_env_with_pat(f.ids, f.copied, fp, fc, fenv); + matches_exp(~denv, d, ~fenv, fc); + | (_, FixF(fp, fc, Some(fenv))) => + let fenv = evaluate_extend_env_with_pat(f.ids, f.copied, fp, fc, fenv); matches_exp(~denv, d, ~fenv, fc); | (_, Constructor("$v", _)) => From 46d112336cb54b0035a0198e7ff8600c9e3f5df0 Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Sun, 18 Aug 2024 14:05:04 +0800 Subject: [PATCH 3/8] use indices for function matching --- src/haz3lcore/dynamics/FilterMatcher.re | 91 ++++++++++++++++++------- 1 file changed, 67 insertions(+), 24 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index 62aa36803d..0471fd884b 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -53,6 +53,8 @@ let evaluate_extend_env_with_pat = }; }; +let alpha_magic = "__alpha_id__"; + let rec matches_exp = ( ~denv: ClosureEnvironment.t, @@ -75,15 +77,33 @@ let rec matches_exp = // HACK[Matt]: ignore fixpoints in comparison, to allow pausing on fixpoint steps | (FixF(dp, dc, _), FixF(fp, fc, _)) => - matches_pat(dp, fp) - && matches_exp( - ~denv= - denv |> ClosureEnvironment.without_keys(dp |> DHPat.bound_vars), - dc, - ~fenv= - fenv |> ClosureEnvironment.without_keys(fp |> DHPat.bound_vars), - fc, - ) + let dvars = DHPat.bound_vars(dp); + let fvars = DHPat.bound_vars(fp); + if (List.length(dvars) != List.length(fvars)) { + false; + } else { + let ids = + Array.init(List.length(dvars), _ => { + alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4)) + }); + let denv_subst: list((string, 'a)) = + List.mapi( + (i, binding) => + (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + dvars, + ); + let fenv_subst: list((string, 'a)) = + List.mapi( + (i, binding) => + (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + fvars, + ); + let denv = + evaluate_extend_env(Environment.of_list(denv_subst), denv); + let fenv = + evaluate_extend_env(Environment.of_list(fenv_subst), fenv); + matches_exp(~denv, dc, ~fenv, fc); + }; | (FixF(dp, dc, None), _) => let denv = evaluate_extend_env_with_pat(d.ids, d.copied, dp, dc, denv); matches_exp(~denv, dc, ~fenv, f); @@ -121,14 +141,19 @@ let rec matches_exp = | (Filter(Residue(_), d), _) => matches_exp(d, f) | (Var(dx), Var(fx)) => - switch ( - ClosureEnvironment.lookup(denv, dx), - ClosureEnvironment.lookup(fenv, fx), - ) { - | (Some(d), Some(f)) => matches_exp(d, f) - | (Some(_), None) => false - | (None, Some(_)) => false - | (None, None) => true + if (String.starts_with(~prefix=alpha_magic, dx) + && String.starts_with(~prefix=alpha_magic, fx)) { + String.equal(dx, fx); + } else { + switch ( + ClosureEnvironment.lookup(denv, dx), + ClosureEnvironment.lookup(fenv, fx), + ) { + | (Some(d), Some(f)) => matches_exp(d, f) + | (Some(_), None) => false + | (None, Some(_)) => false + | (None, None) => true + }; } | (Var(dx), _) => switch (ClosureEnvironment.lookup(denv, dx)) { @@ -284,13 +309,31 @@ and matches_fun = fp: DHPat.t, f: DHExp.t, ) => { - matches_pat(dp, fp) - && matches_exp( - ~denv=ClosureEnvironment.without_keys(DHPat.bound_vars(dp), denv), - d, - ~fenv=ClosureEnvironment.without_keys(DHPat.bound_vars(fp), fenv), - f, - ); + let dvars = DHPat.bound_vars(dp); + let fvars = DHPat.bound_vars(fp); + if (List.length(dvars) != List.length(fvars)) { + false; + } else { + let ids = + Array.init(List.length(dvars), _ => { + alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4)) + }); + let denv_subst: list((string, 'a)) = + List.mapi( + (i, binding) => + (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + dvars, + ); + let fenv_subst: list((string, 'a)) = + List.mapi( + (i, binding) => + (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + fvars, + ); + let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv); + let fenv = evaluate_extend_env(Environment.of_list(fenv_subst), fenv); + matches_exp(~denv, d, ~fenv, f); + }; } and matches_pat = (d: Pat.t, f: Pat.t): bool => { From c819ca157378071fe3a42e01cd915f8a353632ea Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Tue, 20 Aug 2024 20:58:18 +0800 Subject: [PATCH 4/8] use indices for let as well --- src/haz3lcore/dynamics/FilterMatcher.re | 28 ++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index 0471fd884b..23f23d62c2 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -213,7 +213,33 @@ let rec matches_exp = | (Fun(_), _) => false | (Let(dp, d1, d2), Let(fp, f1, f2)) => - matches_pat(dp, fp) && matches_exp(d1, f1) && matches_exp(d2, f2) + let dvars = DHPat.bound_vars(dp); + let fvars = DHPat.bound_vars(fp); + if (List.length(dvars) != List.length(fvars)) { + false; + } else { + let ids = + Array.init(List.length(dvars), _ => { + alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4)) + }); + let denv_subst: list((string, 'a)) = + List.mapi( + (i, binding) => + (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + dvars, + ); + let fenv_subst: list((string, 'a)) = + List.mapi( + (i, binding) => + (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + fvars, + ); + let denv = + evaluate_extend_env(Environment.of_list(denv_subst), denv); + let fenv = + evaluate_extend_env(Environment.of_list(fenv_subst), fenv); + matches_exp(d1, f1) && matches_exp(~denv, d2, ~fenv, f2); + }; | (Let(_), _) => false | (TypAp(d1, t1), TypAp(d2, t2)) => From 096c217c67c52054d9792f42704e38ebf2bfc753 Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Tue, 20 Aug 2024 20:58:29 +0800 Subject: [PATCH 5/8] remove excessive debug output --- src/haz3lcore/dynamics/Stepper.re | 1 - 1 file changed, 1 deletion(-) diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re index e922aacf52..8b977cdf5f 100644 --- a/src/haz3lcore/dynamics/Stepper.re +++ b/src/haz3lcore/dynamics/Stepper.re @@ -247,7 +247,6 @@ let rec evaluate_pending = (~settings, s: t) => { } ) |> DHExp.repair_ids; - let _ = print_endline(d_loc' |> DHExp.show); let d' = EvalCtx.compose(eo.ctx, d_loc'); let new_step = { d, From 919179c8c70ad1176b1ddd7dab7c04d8dd1744ad Mon Sep 17 00:00:00 2001 From: Haoxiang Fei Date: Tue, 20 Aug 2024 21:19:27 +0800 Subject: [PATCH 6/8] refactor: add tangle, remove matches_pat --- src/haz3lcore/dynamics/FilterMatcher.re | 173 +++++++++--------------- 1 file changed, 67 insertions(+), 106 deletions(-) diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index 23f23d62c2..d6d0bcc543 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -55,6 +55,41 @@ let evaluate_extend_env_with_pat = let alpha_magic = "__alpha_id__"; +let tangle = + ( + dp: DHPat.t, + denv: ClosureEnvironment.t, + fp: DHPat.t, + fenv: ClosureEnvironment.t, + ) + : option((ClosureEnvironment.t, ClosureEnvironment.t)) => { + let dvars = DHPat.bound_vars(dp); + let fvars = DHPat.bound_vars(fp); + if (List.length(dvars) != List.length(fvars)) { + None; + } else { + let ids = + Array.init(List.length(dvars), _ => { + alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4)) + }); + let denv_subst: list((string, 'a)) = + List.mapi( + (i, binding) => + (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + dvars, + ); + let fenv_subst: list((string, 'a)) = + List.mapi( + (i, binding) => + (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + fvars, + ); + let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv); + let fenv = evaluate_extend_env(Environment.of_list(fenv_subst), fenv); + Some((denv, fenv)); + }; +}; + let rec matches_exp = ( ~denv: ClosureEnvironment.t, @@ -76,34 +111,26 @@ let rec matches_exp = | (Constructor("$v", _), _) => failwith("$v in matched expression") // HACK[Matt]: ignore fixpoints in comparison, to allow pausing on fixpoint steps - | (FixF(dp, dc, _), FixF(fp, fc, _)) => - let dvars = DHPat.bound_vars(dp); - let fvars = DHPat.bound_vars(fp); - if (List.length(dvars) != List.length(fvars)) { - false; - } else { - let ids = - Array.init(List.length(dvars), _ => { - alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4)) - }); - let denv_subst: list((string, 'a)) = - List.mapi( - (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), - dvars, - ); - let fenv_subst: list((string, 'a)) = - List.mapi( - (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), - fvars, - ); - let denv = - evaluate_extend_env(Environment.of_list(denv_subst), denv); - let fenv = - evaluate_extend_env(Environment.of_list(fenv_subst), fenv); - matches_exp(~denv, dc, ~fenv, fc); - }; + | (FixF(dp, dc, None), FixF(fp, fc, None)) => + switch (tangle(dp, denv, fp, fenv)) { + | None => false + | Some((denv, fenv)) => matches_exp(~denv, dc, ~fenv, fc) + } + | (FixF(dp, dc, None), FixF(fp, fc, Some(fenv))) => + switch (tangle(dp, denv, fp, fenv)) { + | None => false + | Some((denv, fenv)) => matches_exp(~denv, dc, ~fenv, fc) + } + | (FixF(dp, dc, Some(denv)), FixF(fp, fc, None)) => + switch (tangle(dp, denv, fp, fenv)) { + | None => false + | Some((denv, fenv)) => matches_exp(~denv, dc, ~fenv, fc) + } + | (FixF(dp, dc, Some(denv)), FixF(fp, fc, Some(fenv))) => + switch (tangle(dp, denv, fp, fenv)) { + | None => false + | Some((denv, fenv)) => matches_exp(~denv, dc, ~fenv, fc) + } | (FixF(dp, dc, None), _) => let denv = evaluate_extend_env_with_pat(d.ids, d.copied, dp, dc, denv); matches_exp(~denv, dc, ~fenv, f); @@ -213,33 +240,11 @@ let rec matches_exp = | (Fun(_), _) => false | (Let(dp, d1, d2), Let(fp, f1, f2)) => - let dvars = DHPat.bound_vars(dp); - let fvars = DHPat.bound_vars(fp); - if (List.length(dvars) != List.length(fvars)) { - false; - } else { - let ids = - Array.init(List.length(dvars), _ => { - alpha_magic ++ Uuidm.to_string(Uuidm.v(`V4)) - }); - let denv_subst: list((string, 'a)) = - List.mapi( - (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), - dvars, - ); - let fenv_subst: list((string, 'a)) = - List.mapi( - (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), - fvars, - ); - let denv = - evaluate_extend_env(Environment.of_list(denv_subst), denv); - let fenv = - evaluate_extend_env(Environment.of_list(fenv_subst), fenv); - matches_exp(d1, f1) && matches_exp(~denv, d2, ~fenv, f2); - }; + switch (tangle(dp, denv, fp, fenv)) { + | None => false + | Some((denv, fenv)) => + matches_exp(d1, f1) && matches_exp(~denv, d2, ~fenv, f2) + } | (Let(_), _) => false | (TypAp(d1, t1), TypAp(d2, t2)) => @@ -301,8 +306,12 @@ let rec matches_exp = && ( switch ( List.for_all2( - ((dk, dv), (fk, fv)) => - matches_pat(dk, fk) && matches_exp(dv, fv), + ((dk, dv), (fk, fv)) => { + switch (tangle(dk, denv, fk, fenv)) { + | None => false + | Some((denv, fenv)) => matches_exp(~denv, dv, ~fenv, fv) + } + }, drule, frule, ) @@ -362,58 +371,10 @@ and matches_fun = }; } -and matches_pat = (d: Pat.t, f: Pat.t): bool => { - switch (d |> DHPat.term_of, f |> DHPat.term_of) { - // Matt: I'm not sure what the exact semantics of matching should be here. - | (Parens(x), _) => matches_pat(x, f) - | (_, Parens(x)) => matches_pat(d, x) - | (Cast(x, _, _), _) => matches_pat(x, f) - | (_, Cast(x, _, _)) => matches_pat(d, x) - | (_, EmptyHole) => true - | (MultiHole(_), MultiHole(_)) => true - | (MultiHole(_), _) => false - | (Wild, Wild) => true - | (Wild, _) => false - | (Int(dv), Int(fv)) => dv == fv - | (Int(_), _) => false - | (Float(dv), Float(fv)) => dv == fv - | (Float(_), _) => false - | (Bool(dv), Bool(fv)) => dv == fv - | (Bool(_), _) => false - | (String(dv), String(fv)) => dv == fv - | (String(_), _) => false - | (ListLit(dl), ListLit(fl)) => - switch ( - List.fold_left2((res, d, f) => res && matches_pat(d, f), true, dl, fl) - ) { - | exception (Invalid_argument(_)) => false - | res => res - } - | (ListLit(_), _) => false - | (Constructor(dt, _), Constructor(ft, _)) => dt == ft - | (Constructor(_), _) => false - | (Var(dx), Var(fx)) => String.equal(dx, fx) - | (Var(_), _) => false - | (Tuple(dl), Tuple(fl)) => - switch ( - List.fold_left2((res, d, f) => res && matches_pat(d, f), true, dl, fl) - ) { - | exception (Invalid_argument(_)) => false - | res => res - } - | (Tuple(_), _) => false - | (Ap(d1, d2), Ap(f1, f2)) => matches_pat(d1, f1) && matches_pat(d2, f2) - | (Ap(_), _) => false - | (Cons(d1, d2), Cons(f1, f2)) => - matches_pat(d1, f1) && matches_pat(d2, f2) - | (Cons(_), _) => false - | (EmptyHole, _) => false - | (Invalid(_), _) => false - }; -} and matches_typ = (d: Typ.t, f: Typ.t) => { Typ.eq(d, f); } + and matches_utpat = (d: TPat.t, f: TPat.t): bool => { switch (d.term, f.term) { | (Invalid(_), _) => false From 598965187aec7cd3cc1f9d2f2e6fbb0efdfc3451 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Fri, 23 Aug 2024 10:03:28 -0400 Subject: [PATCH 7/8] Remove parens in weak_head_normalize --- src/haz3lcore/lang/term/Typ.re | 1 + 1 file changed, 1 insertion(+) diff --git a/src/haz3lcore/lang/term/Typ.re b/src/haz3lcore/lang/term/Typ.re index 18d6e66284..5dc0b73aaa 100644 --- a/src/haz3lcore/lang/term/Typ.re +++ b/src/haz3lcore/lang/term/Typ.re @@ -326,6 +326,7 @@ let is_consistent = (ctx: Ctx.t, ty1: t, ty2: t): bool => let rec weak_head_normalize = (ctx: Ctx.t, ty: t): t => switch (term_of(ty)) { + | Parens(t) => weak_head_normalize(ctx, t) | Var(x) => switch (Ctx.lookup_alias(ctx, x)) { | Some(ty) => weak_head_normalize(ctx, ty) From f784b0fff4261ebedd1fcaa586162a72e8f76dfa Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Tue, 27 Aug 2024 12:17:08 -0400 Subject: [PATCH 8/8] Remove parens around hidden functions --- src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re index 34efdf0735..ffb0eed0c5 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re @@ -42,8 +42,8 @@ let precedence_bin_string_op = (bso: Operators.op_bin_string) => | Concat => DHDoc_common.precedence_Plus | Equals => DHDoc_common.precedence_Equals }; -let rec precedence = (~show_casts: bool, d: DHExp.t) => { - let precedence' = precedence(~show_casts); +let rec precedence = (~show_function_bodies, ~show_casts: bool, d: DHExp.t) => { + let precedence' = precedence(~show_function_bodies, ~show_casts); switch (DHExp.term_of(d)) { | Var(_) | Invalid(_) @@ -73,6 +73,8 @@ let rec precedence = (~show_casts: bool, d: DHExp.t) => { | ListConcat(_) => DHDoc_common.precedence_Plus | Tuple(_) => DHDoc_common.precedence_Comma | TypFun(_) + | Fun(_) when !show_function_bodies => DHDoc_common.precedence_const + | TypFun(_) | Fun(_) => DHDoc_common.precedence_max | Let(_) | TyAlias(_) @@ -117,7 +119,11 @@ let mk = d: DHExp.t, ) : DHDoc.t => { - let precedence = precedence(~show_casts=settings.show_casts); + let precedence = + precedence( + ~show_casts=settings.show_casts, + ~show_function_bodies=settings.show_fn_bodies, + ); let rec go = ( d: DHExp.t,