Skip to content

Commit

Permalink
Revert "add Mode.of_constraint"
Browse files Browse the repository at this point in the history
This reverts commit b3510ee.
  • Loading branch information
pigumar1 committed May 4, 2024
1 parent f1ce59d commit 1ba9e2e
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 20 deletions.
6 changes: 5 additions & 1 deletion src/haz3lcore/statics/Info.re
Original file line number Diff line number Diff line change
Expand Up @@ -575,7 +575,11 @@ let derived_pat =
let cls = Cls.Pat(UPat.cls_of_term(upat.term));
let status = status_pat(ctx, mode, self);
let ty = fixed_typ_pat(ctx, mode, self);
let constraint_mode = Mode.of_constraint(mode, constraint_ty);
let constraint_mode =
switch (constraint_ty) {
| None => mode
| Some(ty) => Ana(ty)
};
let constraint_ =
fixed_constraint_pat(upat, ctx, constraint_mode, self, constraint_);
{
Expand Down
6 changes: 0 additions & 6 deletions src/haz3lcore/statics/Mode.re
Original file line number Diff line number Diff line change
Expand Up @@ -127,9 +127,3 @@ let of_deferred_ap_args = (length: int, ty_ins: list(Typ.t)): list(t) =>
? ty_ins : List.init(length, _ => Typ.Unknown(Internal))
)
|> List.map(ty => Ana(ty));

let of_constraint = (mode: t, constraint_ty: option(Typ.t)): t =>
switch (constraint_ty) {
| None => mode
| Some(ty) => Ana(ty)
};
21 changes: 8 additions & 13 deletions src/haz3lcore/statics/Statics.re
Original file line number Diff line number Diff line change
Expand Up @@ -485,7 +485,6 @@ and uexp_to_info_map =
// Mark patterns as redundant at the top level
// because redundancy doesn't make sense in a smaller context
~constraint_=p_constraint,
~constraint_ty=Some(constraint_ty),
);
(
// Override the info for the single upat
Expand Down Expand Up @@ -680,24 +679,20 @@ and upat_to_info_map =
add(~self=Just(p.ty), ~ctx=p.ctx, ~constraint_=p.constraint_, m);
| Constructor(ctr) =>
let self = Self.of_ctr(ctx, ctr);
let constraint_mode = Mode.of_constraint(mode, constraint_ty);
atomic(self, Constraint.of_ctr(ctx, constraint_mode, ctr, self));
atomic(self, Constraint.of_ctr(ctx, mode, ctr, self));
| Ap(fn, arg) =>
let ctr = UPat.ctr_name(fn);
let fn_mode = Mode.of_ap(ctx, mode, ctr);
let (fn, m) = go(~ctx, ~mode=fn_mode, fn, m);
let (ty_in, ty_out) = Typ.matched_arrow(ctx, fn.ty);
let (arg, m) = go(~ctx, ~mode=Ana(ty_in), arg, m);
let constraint_mode = Mode.of_constraint(mode, constraint_ty);
let constraint_ =
Constraint.of_ap(
ctx,
constraint_mode,
ctr,
arg.constraint_,
Some(ty_out),
);
add(~self=Just(ty_out), ~ctx=arg.ctx, ~constraint_, m);
add(
~self=Just(ty_out),
~ctx=arg.ctx,
~constraint_=
Constraint.of_ap(ctx, mode, ctr, arg.constraint_, Some(ty_out)),
m,
);
| TypeAnn(p, ann) =>
let (ann, m) = utyp_to_info_map(~ctx, ~ancestors, ann, m);
let (p, m) = go(~ctx, ~mode=Ana(ann.ty), p, m);
Expand Down

0 comments on commit 1ba9e2e

Please sign in to comment.