Skip to content

Commit

Permalink
Support patterns on arrays and opaque types.
Browse files Browse the repository at this point in the history
  • Loading branch information
@maximebuyse
maximebuyse committed Sep 18, 2024
1 parent ec8c2d8 commit 13cbc18
Show file tree
Hide file tree
Showing 21 changed files with 1,283 additions and 158 deletions.
1 change: 1 addition & 0 deletions engine/backends/fstar/fstar_backend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1697,6 +1697,7 @@ module TransformToInputLanguage =
|> Phases.Direct_and_mut
|> Phases.Reject.Arbitrary_lhs
|> Phases.Drop_blocks
|> Phases.Rewrite_patterns
|> Phases.Drop_match_guards
|> Phases.Drop_references
|> Phases.Trivialize_assign_lhs
Expand Down
2 changes: 1 addition & 1 deletion engine/lib/ast.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -203,7 +203,7 @@ functor
(* An or-pattern, e.g. `p | q`.
Invariant: `List.length subpats >= 2`. *)
| POr of { subpats : pat list }
| PArray of { args : pat list }
| PArray of { args : pat list; slice : bool; suffix : pat list }
| PDeref of { subpat : pat; witness : F.reference }
| PConstant of { lit : literal }
| PBinding of {
Expand Down
51 changes: 51 additions & 0 deletions engine/lib/ast_utils.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -798,6 +798,18 @@ module Make (F : Features.T) = struct
(span : span) : arm =
{ arm = { arm_pat; body; guard }; span }

let make_if_guard (cond : expr) (span : span) (witness : F.match_guard) =
{
guard =
IfLet
{
lhs = { p = PConstant { lit = Bool true }; span; typ = TBool };
rhs = cond;
witness;
};
span;
}

let make_unit_param (span : span) : param =
let typ = unit_typ in
let pat = make_wild_pat typ span in
Expand Down Expand Up @@ -907,6 +919,45 @@ module Make (F : Features.T) = struct
(`Concrete (Concrete_ident.of_name kind f_name))
args span ret_typ

let make_opt_type (result_type : ty) : ty =
TApp
{
ident = Global_ident.of_name Type Core__option__Option;
args = [ GType result_type ];
}

let make_opt_expr (value : expr option) (guard_span : span) (result_type : ty)
: expr =
let (name : Concrete_ident.name), args =
match value with
| Some v -> (Core__option__Option__Some, [ v ])
| None -> (Core__option__Option__None, [])
in
call_Constructor name false args guard_span (make_opt_type result_type)

let make_opt_pattern (binding : pat option) (guard_span : span)
(result_type : ty) : pat =
let (name : Concrete_ident.name), (args : field_pat list) =
match binding with
| Some b ->
( Core__option__Option__Some,
[ { field = `TupleField (0, 1); pat = b } ] )
| None -> (Core__option__Option__None, [])
in

{
p =
PConstruct
{
name = Global_ident.of_name (Constructor { is_struct = false }) name;
args;
is_record = false;
is_struct = false;
};
span = guard_span;
typ = make_opt_type result_type;
}

let make_closure (params : pat list) (body : expr) (span : span) : expr =
let params =
match params with [] -> [ make_wild_pat unit_typ span ] | _ -> params
Expand Down
1 change: 1 addition & 0 deletions engine/lib/diagnostics.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ module Phase = struct
| DropNeedlessReturns
| TransformHaxLibInline
| NewtypeAsRefinement
| RewritePatterns
| DummyA
| DummyB
| DummyC
Expand Down
12 changes: 8 additions & 4 deletions engine/lib/generic_printer/generic_printer.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -358,10 +358,14 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
^^ print#pat_at Pat_PBinding_subpat subpat
|> wrap_parens
| None -> p)
| PArray { args } ->
separate_map (break 0)
(print#pat_at Pat_PArray >> terminate comma >> group)
args
| PArray { args; slice; suffix } ->
let args = List.map ~f:(print#pat_at Pat_PArray) args in
let pats =
if slice then
args @ List.map ~f:(print#pat_at Pat_PArray) suffix
else args
in
separate_map (break 0) (terminate comma >> group) pats
|> iblock brackets
| PDeref { subpat; _ } ->
ampersand ^^ print#pat_at Pat_PDeref subpat
Expand Down
24 changes: 21 additions & 3 deletions engine/lib/import_thir.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -870,7 +870,13 @@ end) : EXPR = struct
and pat'_of_expr' (e : expr') span =
match e with
| Literal lit -> PConstant { lit }
| Array l -> PArray { args = List.map ~f:pat_of_expr l }
| Array l ->
PArray
{
args = List.map ~f:pat_of_expr l;
slice = false;
suffix = [];
}
| Borrow { kind = _; e; witness } ->
PDeref { subpat = pat_of_expr e; witness }
| _ ->
Expand All @@ -879,9 +885,21 @@ end) : EXPR = struct
in
(c_constant_expr value |> pat_of_expr).p
| InlineConstant { subpattern; _ } -> (c_pat subpattern).p
| Array _ -> unimplemented [ pat.span ] "Pat:Array"
| Array { prefix; slice; suffix } ->
PArray
{
args = List.map ~f:c_pat prefix;
slice = Option.is_some slice;
suffix = List.map ~f:c_pat suffix;
}
| Or { pats } -> POr { subpats = List.map ~f:c_pat pats }
| Slice _ -> unimplemented [ pat.span ] "pat Slice"
| Slice { prefix; slice; suffix } ->
PArray
{
args = List.map ~f:c_pat prefix;
slice = Option.is_some slice;
suffix = List.map ~f:c_pat suffix;
}
| Range _ -> unimplemented [ pat.span ] "pat Range"
| DerefPattern _ -> unimplemented [ pat.span ] "pat DerefPattern"
| Never -> unimplemented [ pat.span ] "pat Never"
Expand Down
71 changes: 18 additions & 53 deletions engine/lib/phases/phase_drop_match_guards.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,49 +101,10 @@ module%inlined_contents Make (F : Features.T) = struct
span;
}
:: remaining ->
let result_typ = dty span body.typ in
let opt_result_typ : B.ty =
TApp
{
ident = Global_ident.of_name Type Core__option__Option;
args = [ GType result_typ ];
}
in
let mk_opt_expr (value : B.expr option) : B.expr =
let (name : Concrete_ident.name), args =
match value with
| Some v -> (Core__option__Option__Some, [ v ])
| None -> (Core__option__Option__None, [])
in
UB.call_Constructor name false args guard_span opt_result_typ
in

let mk_opt_pattern (binding : B.pat option) : B.pat =
let (name : Concrete_ident.name), (args : B.field_pat list) =
match binding with
| Some b ->
( Core__option__Option__Some,
[ { field = `TupleField (0, 1); pat = b } ] )
| None -> (Core__option__Option__None, [])
in
{
p =
PConstruct
{
name =
Global_ident.of_name
(Constructor { is_struct = false })
name;
args;
is_record = false;
is_struct = false;
};
span = guard_span;
typ = opt_result_typ;
}
in
let result_type = dty span body.typ in
let opt_result_type = UB.make_opt_type result_type in

let expr_none = mk_opt_expr None in
let expr_none = UB.make_opt_expr None guard_span result_type in

(* This is the nested pattern matching equivalent to the guard *)
(* Example: .. if let pat = rhs => body *)
Expand All @@ -155,7 +116,9 @@ module%inlined_contents Make (F : Features.T) = struct
arms =
[
UB.make_arm (dpat lhs)
(mk_opt_expr (Some (dexpr body)))
(UB.make_opt_expr
(Some (dexpr body))
guard_span result_type)
span;
UB.make_arm
(UB.make_wild_pat (dty guard_span lhs.typ) guard_span)
Expand All @@ -177,7 +140,7 @@ module%inlined_contents Make (F : Features.T) = struct
{
e = guard_match;
span = guard_span;
typ = opt_result_typ;
typ = opt_result_type;
}
guard_span;
UB.make_arm
Expand All @@ -188,7 +151,7 @@ module%inlined_contents Make (F : Features.T) = struct
];
};
span = guard_span;
typ = opt_result_typ;
typ = opt_result_type;
}
in
let id = UB.fresh_local_ident_in [] "x" in
Expand All @@ -201,7 +164,7 @@ module%inlined_contents Make (F : Features.T) = struct
arms =
[
UB.make_arm
(mk_opt_pattern
(UB.make_opt_pattern
(Some
{
p =
Expand All @@ -210,25 +173,27 @@ module%inlined_contents Make (F : Features.T) = struct
mut = Immutable;
mode = ByValue;
var = id;
typ = result_typ;
typ = result_type;
subpat = None;
};
span;
typ = result_typ;
}))
{ e = LocalVar id; span; typ = result_typ }
typ = result_type;
})
guard_span result_type)
{ e = LocalVar id; span; typ = result_type }
guard_span;
UB.make_arm (mk_opt_pattern None)
UB.make_arm
(UB.make_opt_pattern None guard_span result_type)
{
e = maybe_simplified_match scrutinee treated;
span = guard_span;
typ = result_typ;
typ = result_type;
}
guard_span;
];
};
span = guard_span;
typ = result_typ;
typ = result_type;
}
in
let new_arm : B.arm =
Expand Down
Loading

0 comments on commit 13cbc18

Please sign in to comment.