Skip to content

Commit

Permalink
refactor: add tangle, remove matches_pat
Browse files Browse the repository at this point in the history
  • Loading branch information
@tonyfettes
tonyfettes committed Aug 20, 2024
1 parent 096c217 commit 919179c
Showing 1 changed file with 67 additions and 106 deletions.
173 changes: 67 additions & 106 deletions src/haz3lcore/dynamics/FilterMatcher.re
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -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);
Expand Down Expand Up @@ -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)) =>
Expand Down Expand Up @@ -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,
)
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 919179c

Please sign in to comment.