Skip to content

Commit

Permalink
Add addition pattern
Browse files Browse the repository at this point in the history
  • Loading branch information
Negabinary committed Feb 25, 2025
1 parent 5f6af3c commit a6f60f9
Show file tree
Hide file tree
Showing 21 changed files with 300 additions and 18 deletions.
11 changes: 11 additions & 0 deletions src/haz3lcore/dynamics/PatternMatch.re
Original file line number Diff line number Diff line change
Expand Up @@ -61,4 +61,15 @@ let rec matches = (dp: Pat.t, d: DHExp.t): match_result =>
| Parens(p) => matches(p, d)
| Cast(p, t1, t2) =>
matches(p, Cast(d, t2, t1) |> DHExp.fresh |> Casts.transition_multiple)
| Add(p1, p2) =>
switch (Pat.is_const_int(p1), Pat.is_const_int(p2)) {
| (Some(n1), Some(n2)) => matches(Int(n1 + n2) |> Pat.fresh, d)
| (Some(n), None) =>
let* n1 = Unboxing.unbox(Int, d);
matches(p2, Int(n1 - n) |> DHExp.fresh);
| (None, Some(n)) =>
let* n2 = Unboxing.unbox(Int, d);
matches(p1, Int(n2 - n) |> DHExp.fresh);
| (None, None) => IndetMatch
}
};
1 change: 1 addition & 0 deletions src/haz3lcore/dynamics/Substitution.re
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ let rec binds_var = (m: Statics.Map.t, x: Var.t, dp: DHPat.t): bool =>
let new_list = List.map(binds_var(m, x), d_list);
List.fold_left((||), false, new_list);
| Ap(_, _) => false
| Add(dp1, dp2) => binds_var(m, x, dp1) || binds_var(m, x, dp2)
}
};

Expand Down
5 changes: 5 additions & 0 deletions src/haz3lcore/dynamics/TypeAssignment.re
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,10 @@ let dhpat_extend_ctx = (dhpat: DHPat.t, ty: Typ.t, ctx: Ctx.t): option(Ctx.t) =>
| Constructor(_) => Some([]) // TODO: make this stricter
| Cast(dhp, ty1, ty2) =>
Typ.equal(ty, ty2) ? dhpat_var_entry(dhp, ty1) : None
| Add(dhp1, dhp2) =>
let* l1 = dhpat_var_entry(dhp1, Int |> Typ.temp);
let* l2 = dhpat_var_entry(dhp2, Int |> Typ.temp);
Some(l1 @ l2);
};
};
let+ l = dhpat_var_entry(dhpat, ty);
Expand Down Expand Up @@ -131,6 +135,7 @@ let rec dhpat_synthesize = (dhpat: DHPat.t, ctx: Ctx.t): option(Typ.t) => {
| Bool(_) => Some(Bool |> Typ.temp)
| String(_) => Some(String |> Typ.temp)
| Cast(_, _, ty) => Some(ty)
| Add(_, _) => Some(Int |> Typ.temp)
};
};

Expand Down
2 changes: 2 additions & 0 deletions src/haz3lcore/lang/Form.re
Original file line number Diff line number Diff line change
Expand Up @@ -309,6 +309,7 @@ type compound_form =
| DotTyp
| TypeAsc
| TypPlus
| PatPlus
// UNARY PREFIX OPERATORS
| Not
| TypSumSingle
Expand Down Expand Up @@ -394,6 +395,7 @@ let get: compound_form => t =
| DotTyp => mk_infix(".", Typ, P.dot)
| TypeAsc => mk(ss, [":"], mk_bin'(P.cast, Exp, Exp, [], Typ))
| TypPlus => mk_infix("+", Typ, P.type_plus)
| PatPlus => mk_infix("+", Pat, P.plus)
// UNARY PREFIX OPERATORS
| Not => mk(ii, ["!"], mk_pre(P.not_, Exp, []))
| TypSumSingle => mk(ss, ["+"], mk_pre(P.or_, Typ, []))
Expand Down
12 changes: 12 additions & 0 deletions src/haz3lcore/pretty/ExpToSegment.re
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,7 @@ let external_precedence_pat = (dp: Pat.t) =>
| Ap(_) => Precedence.ap
| Cast(_) => Precedence.cast
| Tuple(_) => Precedence.prod
| Add(_, _) => Precedence.plus

// Matt: I think multiholes are min because we don't know the precedence of the `⟩?⟨`s
| MultiHole(_) => Precedence.min
Expand Down Expand Up @@ -431,6 +432,12 @@ and parenthesize_pat =
parenthesize_typ(t2) |> paren_typ_at(Precedence.max),
)
|> rewrap
| Add(p1, p2) =>
Add(
parenthesize_pat(p1) |> paren_pat_assoc_at(Precedence.plus),
parenthesize_pat(p2) |> paren_pat_at(Precedence.plus),
)
|> rewrap
};
}

Expand Down Expand Up @@ -1153,6 +1160,11 @@ and pat_to_pretty = (~settings: Settings.t, pat: Pat.t): pretty => {
let+ p = go(p)
and+ t = typ_to_pretty(~settings: Settings.t, t);
p @ [mk_form(Typeann, id, [])] @ t;
| Add(p1, p2) =>
let id = pat |> Pat.rep_id;
let+ p1 = go(p1)
and+ p2 = go(p2);
p1 @ [mk_form(PatPlus, id, [])] @ p2;
};
}
and typ_to_pretty = (~settings: Settings.t, typ: Typ.t): pretty => {
Expand Down
9 changes: 9 additions & 0 deletions src/haz3lcore/statics/Elaborator.re
Original file line number Diff line number Diff line change
Expand Up @@ -232,6 +232,15 @@ let rec elaborate_pattern =
| Cast(p, _, _) =>
let (p', ty) = elaborate_pattern(m, p);
p' |> cast_from(ty |> Typ.normalize(ctx) |> Typ.all_ids_temp);
| Add(p1, p2) =>
let (p1', ty1) = elaborate_pattern(m, p1);
let (p2', ty2) = elaborate_pattern(m, p2);
Add(
p1' |> fresh_pat_cast(_, ty1, Int |> Typ.temp),
p2' |> fresh_pat_cast(_, ty2, Int |> Typ.temp),
)
|> rewrap
|> cast_from(Int |> Typ.temp);
| Constructor(c, _) =>
let mode =
switch (Id.Map.find_opt(Pat.rep_id(upat), m)) {
Expand Down
12 changes: 10 additions & 2 deletions src/haz3lcore/statics/Info.re
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,9 @@ type error_common =
duplicate_labels: list(LabeledTuple.label),
invalid_labels: list(LabeledTuple.label),
typ: Typ.t,
});
})
/* Pattern add with two degrees of freedom (e.g. x + y instead of x + 1) */
| UnconstrainedPatternAdd;

[@deriving (show({with_path: false}), sexp, yojson, eq)]
type error_exp =
Expand Down Expand Up @@ -414,6 +416,9 @@ let rec status_common =
| (_, Some(syn_ty)) => status_common(ctx, mode, Just(syn_ty))
| _ => InHole(NoType(FreeConstructor(name)))
}
| (IsPatternAdd({left_const: None, right_const: None}), _) =>
InHole(UnconstrainedPatternAdd)
| (IsPatternAdd(_), _) => NotInHole(Syn(Int |> Typ.temp))
| (BadToken(name), _) => InHole(NoType(BadToken(name)))
| (BadTrivAp(ty), _) => InHole(NoType(BadTrivAp(ty)))
| (BadLabel(label), _) => InHole(NoType(BadLabel(label)))
Expand Down Expand Up @@ -467,6 +472,7 @@ let rec status_pat = (ctx: Ctx.t, mode: Mode.t, self: Self.pat): status_pat =>
let additional_err =
switch (status_pat(ctx, mode, self)) {
| InHole(Common(Inconsistent(Internal(_) | Expectation(_))) as err)
| InHole(Common(UnconstrainedPatternAdd) as err)
| InHole(Common(NoType(_)) as err) => Some(err)
| NotInHole(_) => None
| InHole(Common(DuplicateLabel(_)))
Expand Down Expand Up @@ -511,6 +517,7 @@ let rec status_exp = (ctx: Ctx.t, mode: Mode.t, self: Self.exp): status_exp =>
| InHole(Common(DuplicateLabel(_)))
| InHole(
FreeVariable(_) | InexhaustiveMatch(_) | UnusedDeferral |
Common(UnconstrainedPatternAdd) |
BadPartialAp(_),
) =>
failwith("InHole(InexhaustiveMatch(impossible_err))")
Expand Down Expand Up @@ -695,7 +702,8 @@ let fixed_typ_err_common: error_common => Typ.t =
| Inconsistent(Internal(_)) => Unknown(Internal) |> Typ.temp // Should this be some sort of meet?
| Inconsistent(WithArrow(_)) =>
Arrow(Unknown(Internal) |> Typ.temp, Unknown(Internal) |> Typ.temp)
|> Typ.temp;
|> Typ.temp
| UnconstrainedPatternAdd => Int |> Typ.temp;

let fixed_typ_err: error_exp => Typ.t =
fun
Expand Down
1 change: 1 addition & 0 deletions src/haz3lcore/statics/MakeTerm.re
Original file line number Diff line number Diff line change
Expand Up @@ -465,6 +465,7 @@ and pat_term: unsorted => (Pat.term, list(Id.t)) = {
);
}
| ([(_id, (["::"], []))], []) => ret(Cons(l, r))
| ([(_id, (["+"], []))], []) => ret(Add(l, r))
| _ => ret(hole(tm))
}
}
Expand Down
5 changes: 5 additions & 0 deletions src/haz3lcore/statics/Self.re
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,10 @@ type t =
typ: Typ.t,
}) /* Tuple/TupLabel contains malformed labels, duplicate labels, and/or invalid labels */
| IsMulti /* Multihole, treated as hole */
| IsPatternAdd({
left_const: option(int),
right_const: option(int),
}) /* Pattern add, to mark `let x + y = ?` as an error */
| IsConstructor({
name: Constructor.t,
syn_ty: option(Typ.t),
Expand Down Expand Up @@ -86,6 +90,7 @@ let typ_of: (Ctx.t, t) => option(Typ.t) =
| Duplicate(_, Just(typ))
| TupleLabelError({typ, _}) => Some(typ)
| IsConstructor({syn_ty, _}) => syn_ty
| IsPatternAdd({left_const, right_const}) => Some(Typ.temp(Int))
| BadToken(_)
| BadTrivAp(_)
| IsMulti
Expand Down
15 changes: 15 additions & 0 deletions src/haz3lcore/statics/Statics.re
Original file line number Diff line number Diff line change
Expand Up @@ -1427,6 +1427,21 @@ and upat_to_info_map =
let (p, m) =
go(~ctx, ~under_ascription=true, ~mode=Ana(ann.term), p, m);
add(~self=Just(ann.term), ~ctx=p.ctx, ~constraint_=p.constraint_, m);
| Add(p1, p2) =>
let left_const = Pat.is_const_int(p1);
let right_const = Pat.is_const_int(p2);
let (p1, m) = go(~ctx, ~mode=Ana(Typ.temp(Int)), p1, m);
let (p2, m) = go(~ctx=p1.ctx, ~mode=Ana(Typ.temp(Int)), p2, m);
add(
~self=IsPatternAdd({left_const, right_const}),
~ctx=p2.ctx,
~constraint_=
switch (left_const, right_const) {
| (Some(l), Some(r)) => Int(l + r)
| _ => Truth
},
m,
);
};

// This is to allow lifting single values into a singleton labeled tuple when the label is not present
Expand Down
63 changes: 53 additions & 10 deletions src/haz3lcore/statics/Term.re
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,8 @@ module Pat = {
| Tuple
| Parens
| Ap
| Cast;
| Cast
| Add;

include TermBase.Pat;

Expand Down Expand Up @@ -58,7 +59,8 @@ module Pat = {
| Tuple(_) => Tuple
| Parens(_) => Parens
| Ap(_) => Ap
| Cast(_) => Cast;
| Cast(_) => Cast
| Add(_, _) => Add;

let show_cls: cls => string =
fun
Expand All @@ -79,7 +81,8 @@ module Pat = {
| Tuple => "Tuple"
| Parens => "Parenthesized pattern"
| Ap => "Constructor application"
| Cast => "Annotation";
| Cast => "Annotation"
| Add => "Addition pattern";

let rec is_var = (pat: t) => {
switch (pat.term) {
Expand All @@ -100,7 +103,8 @@ module Pat = {
| Tuple(_)
| Label(_)
| Constructor(_)
| Ap(_) => false
| Ap(_)
| Add(_, _) => false
};
};

Expand All @@ -124,7 +128,8 @@ module Pat = {
| Label(_)
| Tuple(_)
| Constructor(_)
| Ap(_) => false
| Ap(_)
| Add(_, _) => false
};
};

Expand All @@ -149,7 +154,8 @@ module Pat = {
| Var(_)
| Cast(_)
| Constructor(_)
| Ap(_) => false
| Ap(_)
| Add(_, _) => false
}
);

Expand All @@ -174,7 +180,8 @@ module Pat = {
| Cons(_, _)
| Var(_)
| Constructor(_)
| Ap(_) => false
| Ap(_)
| Add(_, _) => false
}
);

Expand All @@ -197,7 +204,8 @@ module Pat = {
| Label(_)
| Tuple(_)
| Constructor(_)
| Ap(_) => None
| Ap(_)
| Add(_, _) => None
};
};

Expand Down Expand Up @@ -225,7 +233,8 @@ module Pat = {
| Label(_)
| Tuple(_)
| Constructor(_)
| Ap(_) => None
| Ap(_)
| Add(_, _) => None
};
};

Expand All @@ -244,6 +253,11 @@ module Pat = {
} else {
Some(List.map(Option.get, vars));
};
| Add(pat1, pat2) =>
switch (get_bindings(pat1), get_bindings(pat2)) {
| (Some(vars1), Some(vars2)) => Some(vars1 @ vars2)
| _ => None
}
| Label(_)
| Invalid(_)
| EmptyHole
Expand Down Expand Up @@ -284,7 +298,8 @@ module Pat = {
| Cons(_, _)
| Var(_)
| Constructor(_)
| Ap(_) => None
| Ap(_)
| Add(_, _) => None
};
};

Expand Down Expand Up @@ -327,9 +342,37 @@ module Pat = {
| TupLabel(_, dp) => bound_vars(dp)
| Tuple(dps) => List.flatten(List.map(bound_vars, dps))
| Cons(dp1, dp2) => bound_vars(dp1) @ bound_vars(dp2)
| Add(dp1, dp2) => bound_vars(dp1) @ bound_vars(dp2)
| ListLit(dps) => List.flatten(List.map(bound_vars, dps))
| Ap(_, dp1) => bound_vars(dp1)
};

let rec is_const_int = (dp: t): option(int) =>
switch (dp.term) {
| Int(n) => Some(n)
| Parens(dp) => is_const_int(dp)
| Cast(dp, _, _) => is_const_int(dp)
| Add(dp1, dp2) =>
switch (is_const_int(dp1), is_const_int(dp2)) {
| (Some(n1), Some(n2)) => Some(n1 + n2)
| _ => None
}
| EmptyHole
| MultiHole(_)
| Wild
| Invalid(_)
| Float(_)
| Bool(_)
| String(_)
| ListLit(_)
| Constructor(_)
| Cons(_, _)
| Var(_)
| Tuple(_)
| Label(_)
| TupLabel(_, _)
| Ap(_) => None
};
};

module Exp = {
Expand Down
5 changes: 4 additions & 1 deletion src/haz3lcore/statics/TermBase.re
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ and exp_term =
| Test(exp_t)
| Filter(stepper_filter_kind_t, exp_t)
| Closure([@show.opaque] closure_environment_t, exp_t)
| Parens(exp_t) // (
| Parens(exp_t)
| Cons(exp_t, exp_t)
| ListConcat(exp_t, exp_t)
| UnOp(Operators.op_un, exp_t)
Expand All @@ -110,6 +110,7 @@ and pat_term =
| ListLit(list(pat_t))
| Constructor(string, option(typ_t)) // Typ.t field is only meaningful in dynamic patterns
| Cons(pat_t, pat_t)
| Add(pat_t, pat_t)
| Var(Var.t)
| Tuple(list(pat_t))
| Parens(pat_t)
Expand Down Expand Up @@ -547,6 +548,7 @@ and Pat: {
| ListLit(ts) => ListLit(List.map(pat_map_term, ts))
| Ap(e1, e2) => Ap(pat_map_term(e1), pat_map_term(e2))
| Cons(e1, e2) => Cons(pat_map_term(e1), pat_map_term(e2))
| Add(e1, e2) => Add(pat_map_term(e1), pat_map_term(e2))
| Tuple(xs) => Tuple(List.map(pat_map_term, xs))
| TupLabel(label, e) =>
TupLabel(pat_map_term(label), pat_map_term(e))
Expand Down Expand Up @@ -600,6 +602,7 @@ and Pat: {
| (ListLit(_), _)
| (Constructor(_), _)
| (Cons(_), _)
| (Add(_), _)
| (Var(_), _)
| (TupLabel(_), _)
| (Tuple(_), _)
Expand Down
1 change: 1 addition & 0 deletions src/haz3lmenhir/AST.re
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,7 @@ type pat =
| TuplePat(list(pat))
| BoolPat(bool)
| ConsPat(pat, pat)
| AddPat(pat, pat)
| ListPat(list(pat))
| ApPat(pat, pat)
| InvalidPat(string) // Menhir parser doesn't actually support invalid pats
Expand Down
Loading

0 comments on commit a6f60f9

Please sign in to comment.