summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ExtractToFStar.ml38
-rw-r--r--src/PrintPure.ml24
-rw-r--r--src/Pure.ml51
-rw-r--r--src/PureMicroPasses.ml74
-rw-r--r--src/PureUtils.ml60
-rw-r--r--src/SymbolicToPure.ml72
6 files changed, 159 insertions, 160 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 357b49b5..19e17260 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -758,7 +758,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
(** The following function factorizes the extraction of ADT values.
- Note that lvalues can introduce new variables: we thus return an extraction
+ Note that patterns can introduce new variables: we thus return an extraction
context updated with new bindings.
TODO: we don't need something very generic anymore
@@ -808,27 +808,27 @@ let extract_adt_g_value
(** [inside]: see [extract_ty].
- As an lvalue can introduce new variables, we return an extraction context
+ As an pattern can introduce new variables, we return an extraction context
updated with new bindings.
*)
-let rec extract_typed_lvalue (ctx : extraction_ctx) (fmt : F.formatter)
- (inside : bool) (v : typed_lvalue) : extraction_ctx =
+let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
+ (inside : bool) (v : typed_pattern) : extraction_ctx =
match v.value with
- | LvConcrete cv ->
+ | PatConcrete cv ->
ctx.fmt.extract_constant_value fmt inside cv;
ctx
- | LvVar (Var (v, _)) ->
+ | PatVar (Var (v, _)) ->
let vname =
ctx.fmt.var_basename ctx.names_map.names_set v.basename v.ty
in
let ctx, vname = ctx_add_var vname v.id ctx in
F.pp_print_string fmt vname;
ctx
- | LvVar Dummy ->
+ | PatVar Dummy ->
F.pp_print_string fmt "_";
ctx
- | LvAdt av ->
- let extract_value ctx inside v = extract_typed_lvalue ctx fmt inside v in
+ | PatAdt av ->
+ let extract_value ctx inside v = extract_typed_pattern ctx fmt inside v in
extract_adt_g_value extract_value fmt ctx inside av.variant_id
av.field_values v.ty
@@ -1014,7 +1014,7 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
raise (Failure "Unreachable")
and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
- (xl : typed_lvalue list) (e : texpression) : unit =
+ (xl : typed_pattern list) (e : texpression) : unit =
(* Open a box for the abs expression *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Open parentheses *)
@@ -1026,7 +1026,7 @@ and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
List.fold_left
(fun ctx x ->
F.pp_print_space fmt ();
- extract_typed_lvalue ctx fmt true x)
+ extract_typed_pattern ctx fmt true x)
ctx xl
in
F.pp_print_space fmt ();
@@ -1040,7 +1040,7 @@ and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
F.pp_close_box fmt ()
and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
- (monadic : bool) (lv : typed_lvalue) (re : texpression)
+ (monadic : bool) (lv : typed_pattern) (re : texpression)
(next_e : texpression) : unit =
(* Open a box for the whole expression *)
F.pp_open_hvbox fmt 0;
@@ -1052,7 +1052,7 @@ and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
if monadic then (
(* Note that in F*, the left value of a monadic let-binding can only be
* a variable *)
- let ctx = extract_typed_lvalue ctx fmt true lv in
+ let ctx = extract_typed_pattern ctx fmt true lv in
F.pp_print_space fmt ();
F.pp_print_string fmt "<--";
F.pp_print_space fmt ();
@@ -1062,7 +1062,7 @@ and extract_Let (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
else (
F.pp_print_string fmt "let";
F.pp_print_space fmt ();
- let ctx = extract_typed_lvalue ctx fmt true lv in
+ let ctx = extract_typed_pattern ctx fmt true lv in
F.pp_print_space fmt ();
F.pp_print_string fmt "=";
F.pp_print_space fmt ();
@@ -1148,7 +1148,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
F.pp_print_string fmt "|";
(* Print the pattern *)
F.pp_print_space fmt ();
- let ctx = extract_typed_lvalue ctx fmt false br.pat in
+ let ctx = extract_typed_pattern ctx fmt false br.pat in
F.pp_print_space fmt ();
F.pp_print_string fmt "->";
F.pp_print_space fmt ();
@@ -1208,11 +1208,11 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
| None -> ctx
| Some body ->
List.fold_left
- (fun ctx (lv : typed_lvalue) ->
+ (fun ctx (lv : typed_pattern) ->
(* Open a box for the input parameter *)
F.pp_open_hovbox fmt 0;
F.pp_print_string fmt "(";
- let ctx = extract_typed_lvalue ctx fmt false lv in
+ let ctx = extract_typed_pattern ctx fmt false lv in
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
@@ -1427,9 +1427,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
in
let _ =
List.fold_left
- (fun ctx (lv : typed_lvalue) ->
+ (fun ctx (lv : typed_pattern) ->
F.pp_print_space fmt ();
- let ctx = extract_typed_lvalue ctx fmt false lv in
+ let ctx = extract_typed_pattern ctx fmt false lv in
ctx)
ctx inputs_lvs
in
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 3adf4eee..e40a7b8b 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -288,7 +288,7 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
raise (Failure "Unreachable"))
(** TODO: we don't need a general function anymore (it is now only used for
- lvalues (i.e., patterns)
+ patterns (i.e., patterns)
*)
let adt_g_value_to_string (fmt : value_formatter)
(value_to_string : 'v -> string) (variant_id : VariantId.id option)
@@ -372,15 +372,15 @@ let var_or_dummy_to_string (fmt : ast_formatter) (v : var_or_dummy) : string =
^ ")"
| Dummy -> "_"
-let rec typed_lvalue_to_string (fmt : ast_formatter) (v : typed_lvalue) : string
- =
+let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) :
+ string =
match v.value with
- | LvConcrete cv -> Print.Values.constant_value_to_string cv
- | LvVar var -> var_or_dummy_to_string fmt var
- | LvAdt av ->
+ | PatConcrete cv -> Print.Values.constant_value_to_string cv
+ | PatVar var -> var_or_dummy_to_string fmt var
+ | PatAdt av ->
adt_g_value_to_string
(ast_to_value_formatter fmt)
- (typed_lvalue_to_string fmt)
+ (typed_pattern_to_string fmt)
av.variant_id av.field_values v.ty
let fun_sig_to_string (fmt : ast_formatter) (sg : fun_sig) : string =
@@ -542,19 +542,19 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
if all_args <> [] && inside then "(" ^ e ^ ")" else e
and abs_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string)
- (xl : typed_lvalue list) (e : texpression) : string =
- let xl = List.map (typed_lvalue_to_string fmt) xl in
+ (xl : typed_pattern list) (e : texpression) : string =
+ let xl = List.map (typed_pattern_to_string fmt) xl in
let e = texpression_to_string fmt false indent indent_incr e in
"λ " ^ String.concat " " xl ^ ". " ^ e
and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string)
- (monadic : bool) (lv : typed_lvalue) (re : texpression) (e : texpression) :
+ (monadic : bool) (lv : typed_pattern) (re : texpression) (e : texpression) :
string =
let indent1 = indent ^ indent_incr in
let inside = false in
let re = texpression_to_string fmt inside indent1 indent_incr re in
let e = texpression_to_string fmt inside indent indent_incr e in
- let lv = typed_lvalue_to_string fmt lv in
+ let lv = typed_pattern_to_string fmt lv in
if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e
else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e
@@ -575,7 +575,7 @@ and switch_to_string (fmt : ast_formatter) (indent : string)
^ indent ^ "else\n" ^ indent1 ^ e_false
| Match branches ->
let branch_to_string (b : match_branch) : string =
- let pat = typed_lvalue_to_string fmt b.pat in
+ let pat = typed_pattern_to_string fmt b.pat in
indent ^ "| " ^ pat ^ " ->\n" ^ indent1 ^ e_to_string b.branch
in
let branches = List.map branch_to_string branches in
diff --git a/src/Pure.ml b/src/Pure.ml
index 243b493e..05f7e199 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -287,28 +287,25 @@ type var_or_dummy =
polymorphic = false;
}]
-(** A left value (which appears on the left of assignments.
-
- TODO: rename to "pattern"
- *)
-type lvalue =
- | LvConcrete of constant_value
- (** [LvConcrete] is necessary because we merge the switches over integer
- values and the matches over enumerations *)
- | LvVar of var_or_dummy
- | LvAdt of adt_lvalue
-
-and adt_lvalue = {
+(** A pattern (which appears on the left of assignments, in matches, etc.). *)
+type pattern =
+ | PatConcrete of constant_value
+ (** [PatConcrete] is necessary because we merge the switches over integer
+ values and the matches over enumerations *)
+ | PatVar of var_or_dummy
+ | PatAdt of adt_pattern
+
+and adt_pattern = {
variant_id : variant_id option;
- field_values : typed_lvalue list;
+ field_values : typed_pattern list;
}
-and typed_lvalue = { value : lvalue; ty : ty }
+and typed_pattern = { value : pattern; ty : ty }
[@@deriving
show,
visitors
{
- name = "iter_typed_lvalue";
+ name = "iter_typed_pattern";
variety = "iter";
ancestors = [ "iter_var_or_dummy" ];
nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -317,7 +314,7 @@ and typed_lvalue = { value : lvalue; ty : ty }
},
visitors
{
- name = "map_typed_lvalue";
+ name = "map_typed_pattern";
variety = "map";
ancestors = [ "map_var_or_dummy" ];
nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -326,7 +323,7 @@ and typed_lvalue = { value : lvalue; ty : ty }
},
visitors
{
- name = "reduce_typed_lvalue";
+ name = "reduce_typed_pattern";
variety = "reduce";
ancestors = [ "reduce_var_or_dummy" ];
nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -334,7 +331,7 @@ and typed_lvalue = { value : lvalue; ty : ty }
},
visitors
{
- name = "mapreduce_typed_lvalue";
+ name = "mapreduce_typed_pattern";
variety = "mapreduce";
ancestors = [ "mapreduce_var_or_dummy" ];
nude = true (* Don't inherit [VisitorsRuntime.iter] *);
@@ -393,7 +390,7 @@ type var_id = VarId.id [@@deriving show]
(** Ancestor for [iter_expression] visitor *)
class ['self] iter_expression_base =
object (_self : 'self)
- inherit [_] iter_typed_lvalue
+ inherit [_] iter_typed_pattern
method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
@@ -405,7 +402,7 @@ class ['self] iter_expression_base =
(** Ancestor for [map_expression] visitor *)
class ['self] map_expression_base =
object (_self : 'self)
- inherit [_] map_typed_lvalue
+ inherit [_] map_typed_pattern
method visit_integer_type : 'env -> integer_type -> integer_type =
fun _ x -> x
@@ -418,7 +415,7 @@ class ['self] map_expression_base =
(** Ancestor for [reduce_expression] visitor *)
class virtual ['self] reduce_expression_base =
object (self : 'self)
- inherit [_] reduce_typed_lvalue
+ inherit [_] reduce_typed_pattern
method visit_integer_type : 'env -> integer_type -> 'a =
fun _ _ -> self#zero
@@ -431,7 +428,7 @@ class virtual ['self] reduce_expression_base =
(** Ancestor for [mapreduce_expression] visitor *)
class virtual ['self] mapreduce_expression_base =
object (self : 'self)
- inherit [_] mapreduce_typed_lvalue
+ inherit [_] mapreduce_typed_pattern
method visit_integer_type : 'env -> integer_type -> integer_type * 'a =
fun _ x -> (x, self#zero)
@@ -463,9 +460,9 @@ type expression =
field accesses with calls to projectors over fields (when there
are clashes of field names, some provers like F* get pretty bad...)
*)
- | Abs of typed_lvalue * texpression (** Lambda abstraction: `fun x -> e` *)
+ | Abs of typed_pattern * texpression (** Lambda abstraction: `fun x -> e` *)
| Qualif of qualif (** A top-level qualifier *)
- | Let of bool * typed_lvalue * texpression * texpression
+ | Let of bool * typed_pattern * texpression * texpression
(** Let binding.
TODO: the boolean should be replaced by an enum: sometimes we use
@@ -509,7 +506,7 @@ type expression =
and switch_body = If of texpression * texpression | Match of match_branch list
-and match_branch = { pat : typed_lvalue; branch : texpression }
+and match_branch = { pat : typed_pattern; branch : texpression }
and texpression = { e : expression; ty : ty }
@@ -587,8 +584,8 @@ type inst_fun_sig = { inputs : ty list; outputs : ty list }
type fun_body = {
inputs : var list;
- inputs_lvs : typed_lvalue list;
- (** The inputs seen as lvalues. Allows to make transformations, for example
+ inputs_lvs : typed_pattern list;
+ (** The inputs seen as patterns. Allows to make transformations, for example
to replace unused variables by `_` *)
body : texpression;
}
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index b4f4462b..c84bf7cd 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -93,7 +93,7 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator =
(* Get the maximum *)
method! visit_var _ v _ = v.id
- (** For the lvalues *)
+ (** For the patterns *)
method! visit_Local _ vid _ = vid
(** For the rvalues *)
@@ -117,7 +117,7 @@ type pn_ctx = {
The way it works is as follows:
- we only modify the names of the unnamed variables
- - whenever we see an rvalue/lvalue which is exactly an unnamed variable,
+ - whenever we see an rvalue/pattern which is exactly an unnamed variable,
and this value is linked to some meta-place information which contains
a name and an empty path, we consider we should use this name
- we try to propagate naming constraints on the pure variables use in the
@@ -290,16 +290,16 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
| Some basename -> { v with basename = Some basename }
else v)
in
- (* Update an lvalue - used to update an expression after we computed constraints *)
- let update_typed_lvalue ctx (lv : typed_lvalue) : typed_lvalue =
+ (* Update an pattern - used to update an expression after we computed constraints *)
+ let update_typed_pattern ctx (lv : typed_pattern) : typed_pattern =
let obj =
object
- inherit [_] map_typed_lvalue
+ inherit [_] map_typed_pattern
method! visit_Var _ v mp = Var (update_var ctx v mp, mp)
end
in
- obj#visit_typed_lvalue () lv
+ obj#visit_typed_pattern () lv
in
(* Register an mplace the first time we find one *)
@@ -353,10 +353,10 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
match (unmeta rv).e with Local vid -> add_constraint mp vid ctx | _ -> ctx
in
(* Specific case of constraint on left values *)
- let add_left_constraint (lv : typed_lvalue) (ctx : pn_ctx) : pn_ctx =
+ let add_left_constraint (lv : typed_pattern) (ctx : pn_ctx) : pn_ctx =
let obj =
object (self)
- inherit [_] reduce_typed_lvalue
+ inherit [_] reduce_typed_pattern
method zero _ = empty_ctx
@@ -369,19 +369,19 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
match mp with Some mp -> add_constraint mp v.id ctx | None -> ctx
end
in
- let ctx1 = obj#visit_typed_lvalue () lv () in
+ let ctx1 = obj#visit_typed_pattern () lv () in
merge_ctxs ctx ctx1
in
(* This is used to propagate constraint information about places in case of
* variable reassignments: we try to propagate the information from the
* rvalue to the left *)
- let add_left_right_constraint (lv : typed_lvalue) (re : texpression)
+ let add_left_right_constraint (lv : typed_pattern) (re : texpression)
(ctx : pn_ctx) : pn_ctx =
(* We propagate constraints across variable reassignments: `^0 = x`,
* if the destination doesn't have naming information *)
match lv.value with
- | LvVar (Var (({ id = _; basename = None; ty = _ } as lvar), lmp)) ->
+ | PatVar (Var (({ id = _; basename = None; ty = _ } as lvar), lmp)) ->
if
(* Check that there is not already a name for the variable *)
VarId.Map.mem lvar.id ctx.pure_vars
@@ -444,18 +444,18 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
in
(ctx, { e; ty })
(* *)
- and update_abs (x : typed_lvalue) (e : texpression) (ctx : pn_ctx) :
+ and update_abs (x : typed_pattern) (e : texpression) (ctx : pn_ctx) :
pn_ctx * expression =
(* We first add the left-constraint *)
let ctx = add_left_constraint x ctx in
(* Update the expression, and add additional constraints *)
let ctx, e = update_texpression e ctx in
(* Update the abstracted value *)
- let x = update_typed_lvalue ctx x in
+ let x = update_typed_pattern ctx x in
(* Put together *)
(ctx, Abs (x, e))
(* *)
- and update_let (monadic : bool) (lv : typed_lvalue) (re : texpression)
+ and update_let (monadic : bool) (lv : typed_pattern) (re : texpression)
(e : texpression) (ctx : pn_ctx) : pn_ctx * expression =
(* We first add the left-constraint *)
let ctx = add_left_constraint lv ctx in
@@ -464,7 +464,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
let ctx = add_left_right_constraint lv re ctx in
let ctx, re = update_texpression re ctx in
let ctx, e = update_texpression e ctx in
- let lv = update_typed_lvalue ctx lv in
+ let lv = update_typed_pattern ctx lv in
(ctx, Let (monadic, lv, re, e))
(* *)
and update_switch_body (scrut : texpression) (body : switch_body)
@@ -484,7 +484,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
(fun br ->
let ctx = add_left_constraint br.pat ctx in
let ctx, branch = update_texpression br.branch ctx in
- let pat = update_typed_lvalue ctx br.pat in
+ let pat = update_typed_pattern ctx br.pat in
(ctx, { pat; branch }))
branches
in
@@ -590,7 +590,7 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
* - the left-value is a variable
*)
match (monadic, lv.value) with
- | false, LvVar (Var (lv_var, _)) ->
+ | false, PatVar (Var (lv_var, _)) ->
(* We can filter if: *)
let filter = false in
(* 1. Either:
@@ -806,7 +806,7 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
*)
let lv_visitor =
object
- inherit [_] mapreduce_typed_lvalue
+ inherit [_] mapreduce_typed_pattern
method zero _ = true
@@ -820,9 +820,9 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
else (Dummy, fun _ -> true)
end
in
- let filter_typed_lvalue (used_vars : VarId.Set.t) (lv : typed_lvalue) :
- typed_lvalue * bool =
- let lv, all_dummies = lv_visitor#visit_typed_lvalue used_vars lv in
+ let filter_typed_pattern (used_vars : VarId.Set.t) (lv : typed_pattern) :
+ typed_pattern * bool =
+ let lv, all_dummies = lv_visitor#visit_typed_pattern used_vars lv in
(lv, all_dummies ())
in
@@ -854,7 +854,7 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
let e, used = self#visit_texpression env e in
let used = used () in
(* Filter the left values *)
- let lv, all_dummies = filter_typed_lvalue used lv in
+ let lv, all_dummies = filter_typed_pattern used lv in
(* Small utility - called if we can't filter the let-binding *)
let dont_filter () =
let re, used_re = self#visit_texpression env re in
@@ -906,7 +906,7 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
let inputs_lvs =
if false then
List.map
- (fun lv -> fst (filter_typed_lvalue used_vars lv))
+ (fun lv -> fst (filter_typed_pattern used_vars lv))
body.inputs_lvs
else body.inputs_lvs
in
@@ -974,7 +974,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
match v with
| Dummy -> Dummy
| Var (v, mp) -> if v.ty = unit_ty then Dummy else Var (v, mp)
- (** Replace in lvalues *)
+ (** Replace in patterns *)
method! visit_texpression env e =
if e.ty = unit_ty then unit_rvalue else super#visit_texpression env e
@@ -989,7 +989,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
| Some body ->
let body_exp = obj#visit_texpression () body.body in
(* Update the input parameters *)
- let inputs_lvs = List.map (obj#visit_typed_lvalue ()) body.inputs_lvs in
+ let inputs_lvs = List.map (obj#visit_typed_pattern ()) body.inputs_lvs in
(* Return *)
let body = Some { body with body = body_exp; inputs_lvs } in
{ def with body }
@@ -1089,7 +1089,7 @@ let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
* - if not, make the decomposition in two steps
*)
match lv.value with
- | LvVar _ ->
+ | PatVar _ ->
(* Variable: nothing to do *)
super#visit_Let env monadic lv re next_e
| _ ->
@@ -1098,7 +1098,7 @@ let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
* monadic binding *)
let vid = fresh_id () in
let tmp : var = { id = vid; basename = None; ty = lv.ty } in
- let ltmp = mk_typed_lvalue_from_var tmp None in
+ let ltmp = mk_typed_pattern_from_var tmp None in
let rtmp = mk_texpression_from_var tmp in
(* Visit the next expression *)
let next_e = self#visit_texpression env next_e in
@@ -1155,7 +1155,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
(* Generate a fresh state variable *)
let state_var = fresh_state_var () in
let state_value = mk_texpression_from_var state_var in
- let state_lvar = mk_typed_lvalue_from_var state_var None in
+ let state_lvar = mk_typed_pattern_from_var state_var None in
(* Apply in all the branches and reconstruct the switch *)
let mk_app e = mk_app e state_value in
let switch_body = map_switch_body_branches mk_app switch_body in
@@ -1219,17 +1219,17 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
mk_app re state_value
in
(* Create the match *)
- let fail_pat = mk_result_fail_lvalue re_no_monad_ty in
+ let fail_pat = mk_result_fail_pattern re_no_monad_ty in
let fail_value = mk_result_fail_rvalue e_no_monad_ty in
let fail_branch = { pat = fail_pat; branch = fail_value } in
(* The `Success` branch introduces a fresh state variable *)
let pat_state_var = fresh_state_var () in
- let pat_state_lvalue =
- mk_typed_lvalue_from_var pat_state_var None
+ let pat_state_pattern =
+ mk_typed_pattern_from_var pat_state_var None
in
let success_pat =
- mk_result_return_lvalue
- (mk_simpl_tuple_lvalue [ pat_state_lvalue; lv ])
+ mk_result_return_pattern
+ (mk_simpl_tuple_pattern [ pat_state_pattern; lv ])
in
let pat_state_rvalue = mk_texpression_from_var pat_state_var in
(* TODO: write a utility to create matches (and perform
@@ -1241,7 +1241,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
let e = Switch (re, switch_body) in
let e = { e; ty = e_no_arrow_ty } in
(* Add the lambda to introduce the state variable *)
- let e = mk_abs (mk_typed_lvalue_from_var state_var None) e in
+ let e = mk_abs (mk_typed_pattern_from_var state_var None) e in
(* Sanity check *)
assert (e0.ty = e.ty);
assert (fail_branch.branch.ty = success_branch.branch.ty);
@@ -1250,10 +1250,10 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
else
let re_ty = Option.get (opt_destruct_result re.ty) in
assert (lv.ty = re_ty);
- let fail_pat = mk_result_fail_lvalue lv.ty in
+ let fail_pat = mk_result_fail_pattern lv.ty in
let fail_value = mk_result_fail_rvalue e.ty in
let fail_branch = { pat = fail_pat; branch = fail_value } in
- let success_pat = mk_result_return_lvalue lv in
+ let success_pat = mk_result_return_pattern lv in
let success_branch = { pat = success_pat; branch = e } in
let switch_body = Match [ fail_branch; success_branch ] in
let e = Switch (re, switch_body) in
@@ -1282,7 +1282,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
let sg = { sg with inputs = sg_inputs; outputs = sg_outputs } in
(* Input list *)
let inputs = body.inputs @ [ state_var ] in
- let input_lv = mk_typed_lvalue_from_var state_var None in
+ let input_lv = mk_typed_pattern_from_var state_var None in
let inputs_lvs = body.inputs_lvs @ [ input_lv ] in
let body = { body = body_e; inputs; inputs_lvs } in
(body, sg)
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index aaae94ca..0d941079 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -57,16 +57,16 @@ let compute_constant_value_ty (cv : constant_value) : ty =
| Char _ -> Char
| String _ -> Str
-let mk_typed_lvalue_from_constant_value (cv : constant_value) : typed_lvalue =
+let mk_typed_pattern_from_constant_value (cv : constant_value) : typed_pattern =
let ty = compute_constant_value_ty cv in
- { value = LvConcrete cv; ty }
+ { value = PatConcrete cv; ty }
(*let mk_value_expression (v : typed_rvalue) (mp : mplace option) : texpression =
let e = Value (v, mp) in
let ty = v.ty in
{ e; ty }*)
-let mk_let (monadic : bool) (lv : typed_lvalue) (re : texpression)
+let mk_let (monadic : bool) (lv : typed_pattern) (re : texpression)
(next_e : texpression) : texpression =
let e = Let (monadic, lv, re, next_e) in
let ty = next_e.ty in
@@ -273,12 +273,12 @@ let destruct_result (ty : ty) : ty = Option.get (opt_destruct_result ty)
let opt_destruct_tuple (ty : ty) : ty list option =
match ty with Adt (Tuple, tys) -> Some tys | _ -> None
-let mk_abs (x : typed_lvalue) (e : texpression) : texpression =
+let mk_abs (x : typed_pattern) (e : texpression) : texpression =
let ty = Arrow (x.ty, e.ty) in
let e = Abs (x, e) in
{ e; ty }
-let rec destruct_abs_list (e : texpression) : typed_lvalue list * texpression =
+let rec destruct_abs_list (e : texpression) : typed_pattern list * texpression =
match e.e with
| Abs (x, e') ->
let xl, e'' = destruct_abs_list e' in
@@ -354,8 +354,8 @@ let mk_texpression_from_var (v : var) : texpression =
let ty = v.ty in
{ e; ty }
-let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue =
- let value = LvVar (Var (v, mp)) in
+let mk_typed_pattern_from_var (v : var) (mp : mplace option) : typed_pattern =
+ let value = PatVar (Var (v, mp)) in
let ty = v.ty in
{ value; ty }
@@ -375,16 +375,16 @@ let mk_opt_mplace_texpression (mp : mplace option) (e : texpression) :
- if there is exactly one value, just return it
- if there is > one value: wrap them in a tuple
*)
-let mk_simpl_tuple_lvalue (vl : typed_lvalue list) : typed_lvalue =
+let mk_simpl_tuple_pattern (vl : typed_pattern list) : typed_pattern =
match vl with
| [ v ] -> v
| _ ->
- let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in
+ let tys = List.map (fun (v : typed_pattern) -> v.ty) vl in
let ty = Adt (Tuple, tys) in
- let value = LvAdt { variant_id = None; field_values = vl } in
+ let value = PatAdt { variant_id = None; field_values = vl } in
{ value; ty }
-(** Similar to [mk_simpl_tuple_lvalue] *)
+(** Similar to [mk_simpl_tuple_pattern] *)
let mk_simpl_tuple_texpression (vl : texpression list) : texpression =
match vl with
| [ v ] -> v
@@ -400,9 +400,9 @@ let mk_simpl_tuple_texpression (vl : texpression list) : texpression =
let cons = { e = Qualif qualif; ty } in
mk_apps cons vl
-let mk_adt_lvalue (adt_ty : ty) (variant_id : VariantId.id)
- (vl : typed_lvalue list) : typed_lvalue =
- let value = LvAdt { variant_id = Some variant_id; field_values = vl } in
+let mk_adt_pattern (adt_ty : ty) (variant_id : VariantId.id)
+ (vl : typed_pattern list) : typed_pattern =
+ let value = PatAdt { variant_id = Some variant_id; field_values = vl } in
{ value; ty = adt_ty }
let ty_as_integer (t : ty) : T.integer_type =
@@ -442,15 +442,15 @@ let mk_result_return_rvalue (v : texpression) : texpression =
let cons = { e = cons_e; ty = cons_ty } in
mk_app cons v
-let mk_result_fail_lvalue (ty : ty) : typed_lvalue =
+let mk_result_fail_pattern (ty : ty) : typed_pattern =
let ty = Adt (Assumed Result, [ ty ]) in
- let value = LvAdt { variant_id = Some result_fail_id; field_values = [] } in
+ let value = PatAdt { variant_id = Some result_fail_id; field_values = [] } in
{ value; ty }
-let mk_result_return_lvalue (v : typed_lvalue) : typed_lvalue =
+let mk_result_return_pattern (v : typed_pattern) : typed_pattern =
let ty = Adt (Assumed Result, [ v.ty ]) in
let value =
- LvAdt { variant_id = Some result_return_id; field_values = [ v ] }
+ PatAdt { variant_id = Some result_return_id; field_values = [ v ] }
in
{ value; ty }
@@ -529,18 +529,18 @@ module TypeCheck = struct
| Bool, Bool _ | Char, Char _ | Str, String _ -> ()
| _ -> raise (Failure "Inconsistent type")
- let rec check_typed_lvalue (ctx : tc_ctx) (v : typed_lvalue) : tc_ctx =
- log#ldebug (lazy ("check_typed_lvalue: " ^ show_typed_lvalue v));
+ let rec check_typed_pattern (ctx : tc_ctx) (v : typed_pattern) : tc_ctx =
+ log#ldebug (lazy ("check_typed_pattern: " ^ show_typed_pattern v));
match v.value with
- | LvConcrete cv ->
+ | PatConcrete cv ->
check_constant_value cv v.ty;
ctx
- | LvVar Dummy -> ctx
- | LvVar (Var (var, _)) ->
+ | PatVar Dummy -> ctx
+ | PatVar (Var (var, _)) ->
assert (var.ty = v.ty);
let env = VarId.Map.add var.id var.ty ctx.env in
{ ctx with env }
- | LvAdt av ->
+ | PatAdt av ->
(* Compute the field types *)
let type_id, tys =
match v.ty with
@@ -550,13 +550,13 @@ module TypeCheck = struct
let field_tys =
get_adt_field_types ctx.type_decls type_id av.variant_id tys
in
- let check_value (ctx : tc_ctx) (ty : ty) (v : typed_lvalue) : tc_ctx =
+ let check_value (ctx : tc_ctx) (ty : ty) (v : typed_pattern) : tc_ctx =
if ty <> v.ty then (
log#serror
- ("check_typed_lvalue: not the same types:" ^ "\n- ty: "
+ ("check_typed_pattern: not the same types:" ^ "\n- ty: "
^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty);
raise (Failure "Inconsistent types"));
- check_typed_lvalue ctx v
+ check_typed_pattern ctx v
in
(* Check the field types - TODO: we might also want to check that the
* type of the applied constructor is correct *)
@@ -587,7 +587,7 @@ module TypeCheck = struct
assert (pat.ty = pat_ty);
assert (body.ty = body_ty);
(* Check the pattern and register the introduced variables at the same time *)
- let ctx = check_typed_lvalue ctx pat in
+ let ctx = check_typed_pattern ctx pat in
check_texpression ctx body
| Qualif qualif -> (
match qualif.id with
@@ -620,7 +620,7 @@ module TypeCheck = struct
(* Check the right-expression *)
check_texpression ctx re;
(* Check the pattern and register the introduced variables at the same time *)
- let ctx = check_typed_lvalue ctx pat in
+ let ctx = check_typed_pattern ctx pat in
(* Check the next expression *)
check_texpression ctx e_next
| Switch (scrut, switch_body) -> (
@@ -635,7 +635,7 @@ module TypeCheck = struct
| Match branches ->
let check_branch (br : match_branch) : unit =
assert (br.pat.ty = scrut.ty);
- let ctx = check_typed_lvalue ctx br.pat in
+ let ctx = check_typed_pattern ctx br.pat in
check_texpression ctx br.branch
in
List.iter check_branch branches)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 3a61784c..e8f37f1e 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -111,10 +111,10 @@ type bs_ctx = {
}
(** Body synthesis context *)
-let type_check_lvalue (ctx : bs_ctx) (v : typed_lvalue) : unit =
+let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
let env = VarId.Map.empty in
let ctx = { TypeCheck.type_decls = ctx.type_context.type_decls; env } in
- let _ = TypeCheck.check_typed_lvalue ctx v in
+ let _ = TypeCheck.check_typed_pattern ctx v in
()
let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
@@ -830,7 +830,7 @@ let translate_opt_mplace (p : S.mplace option) : mplace option =
(** Explore an abstraction value and convert it to a given back value
by collecting all the meta-values from the ended *borrows*.
- Given back values are lvalues, because when an abstraction ends, we
+ Given back values are patterns, because when an abstraction ends, we
introduce a call to a backward function in the synthesized program,
which introduces new values:
```
@@ -842,7 +842,7 @@ let translate_opt_mplace (p : S.mplace option) : mplace option =
the heuristics which later find pretty names for the variables.
*)
let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
- (ctx : bs_ctx) : bs_ctx * typed_lvalue option =
+ (ctx : bs_ctx) : bs_ctx * typed_pattern option =
let ctx, value =
match av.value with
| AConcrete _ -> raise (Failure "Unreachable")
@@ -872,9 +872,9 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
assert (variant_id = None);
if field_values = [] then (ctx, None)
else
- (* Note that if there is exactly one field value, [mk_simpl_tuple_lvalue]
+ (* Note that if there is exactly one field value, [mk_simpl_tuple_pattern]
* is the identity *)
- let lv = mk_simpl_tuple_lvalue field_values in
+ let lv = mk_simpl_tuple_pattern field_values in
(ctx, Some lv))
| ABottom -> raise (Failure "Unreachable")
| ALoan lc -> aloan_content_to_given_back mp lc ctx
@@ -884,12 +884,12 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
in
(* Sanity check - Rk.: we do this at every recursive call, which is a bit
* expansive... *)
- (match value with None -> () | Some value -> type_check_lvalue ctx value);
+ (match value with None -> () | Some value -> type_check_pattern ctx value);
(* Return *)
(ctx, value)
and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content)
- (ctx : bs_ctx) : bs_ctx * typed_lvalue option =
+ (ctx : bs_ctx) : bs_ctx * typed_pattern option =
match lc with
| AMutLoan (_, _) | ASharedLoan (_, _, _) -> raise (Failure "Unreachable")
| AEndedMutLoan { child = _; given_back = _; given_back_meta = _ }
@@ -907,14 +907,14 @@ and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content)
(ctx, None)
and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content)
- (ctx : bs_ctx) : bs_ctx * typed_lvalue option =
+ (ctx : bs_ctx) : bs_ctx * typed_pattern option =
match bc with
| V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
raise (Failure "Unreachable")
| AEndedMutBorrow (msv, _) ->
(* Return the meta-symbolic-value *)
let ctx, var = fresh_var_for_symbolic_value msv ctx in
- (ctx, Some (mk_typed_lvalue_from_var var mp))
+ (ctx, Some (mk_typed_pattern_from_var var mp))
| AEndedIgnoredMutBorrow _ ->
(* This happens with nested borrows: we need to dive in *)
raise Unimplemented
@@ -923,7 +923,7 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content)
(ctx, None)
and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) :
- bs_ctx * typed_lvalue option =
+ bs_ctx * typed_pattern option =
match aproj with
| V.AEndedProjLoans (_, child_projs) ->
(* There may be children borrow projections in case of nested borrows,
@@ -936,7 +936,7 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) :
| AEndedProjBorrows mv ->
(* Return the meta-value *)
let ctx, var = fresh_var_for_symbolic_value mv ctx in
- (ctx, Some (mk_typed_lvalue_from_var var mp))
+ (ctx, Some (mk_typed_pattern_from_var var mp))
| AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
raise (Failure "Unreachable")
@@ -945,7 +945,7 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) :
See [typed_avalue_to_given_back].
*)
let abs_to_given_back (mpl : mplace option list) (abs : V.abs) (ctx : bs_ctx) :
- bs_ctx * typed_lvalue list =
+ bs_ctx * typed_pattern list =
let avalues = List.combine mpl abs.avalues in
let ctx, values =
List.fold_left_map
@@ -957,7 +957,7 @@ let abs_to_given_back (mpl : mplace option list) (abs : V.abs) (ctx : bs_ctx) :
(** Simply calls [abs_to_given_back] *)
let abs_to_given_back_no_mp (abs : V.abs) (ctx : bs_ctx) :
- bs_ctx * typed_lvalue list =
+ bs_ctx * typed_pattern list =
let mpl = List.map (fun _ -> None) abs.avalues in
abs_to_given_back mpl abs ctx
@@ -1024,8 +1024,8 @@ and translate_panic (config : config) (ctx : bs_ctx) : texpression =
let _, state_var =
fresh_var (Some ConstStrings.state_basename) mk_state_ty ctx
in
- let state_lvalue = mk_typed_lvalue_from_var state_var None in
- mk_abs state_lvalue ret_v
+ let state_pattern = mk_typed_pattern_from_var state_var None in
+ mk_abs state_pattern ret_v
else mk_result_fail_rvalue ctx.ret_ty
and translate_return (config : config) (opt_v : V.typed_value option)
@@ -1054,7 +1054,7 @@ and translate_return (config : config) (opt_v : V.typed_value option)
mk_result_return_rvalue
(mk_simpl_tuple_texpression [ state_rvalue; v ])
in
- let state_var = mk_typed_lvalue_from_var state_var None in
+ let state_var = mk_typed_pattern_from_var state_var None in
mk_abs state_var ret_v
else mk_result_return_rvalue v
| Some bid ->
@@ -1078,7 +1078,7 @@ and translate_return (config : config) (opt_v : V.typed_value option)
mk_result_return_rvalue
(mk_simpl_tuple_texpression [ state_rvalue; ret_value ])
in
- let state_var = mk_typed_lvalue_from_var state_var None in
+ let state_var = mk_typed_pattern_from_var state_var None in
mk_abs state_var ret_value
else
let ret_value = mk_simpl_tuple_texpression field_values in
@@ -1126,7 +1126,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
(fun (arg, mp) -> mk_opt_mplace_texpression mp arg)
(List.combine args args_mplaces)
in
- let dest_v = mk_typed_lvalue_from_var dest dest_mplace in
+ let dest_v = mk_typed_pattern_from_var dest dest_mplace in
let func = { id = Func fun_id; type_params } in
let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
let ret_ty = mk_function_ret_ty config monadic state_monad dest_v.ty in
@@ -1192,7 +1192,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
let monadic = false in
List.fold_right
(fun (var, value) (e : texpression) ->
- mk_let monadic (mk_typed_lvalue_from_var var None) value e)
+ mk_let monadic (mk_typed_pattern_from_var var None) value e)
variables_values next_e
| V.FunCall ->
let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in
@@ -1221,7 +1221,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
List.append (List.map translate_opt_mplace call.args_places) [ None ]
in
let ctx, outputs = abs_to_given_back output_mpl abs ctx in
- let output = mk_simpl_tuple_lvalue outputs in
+ let output = mk_simpl_tuple_pattern outputs in
(* Sanity check: the inputs and outputs have the proper number and the proper type *)
let fun_id =
match call.call_id with
@@ -1244,7 +1244,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
^ "\n- expected outputs: "
^ string_of_int (List.length inst_sg.outputs)));
List.iter
- (fun (x, ty) -> assert ((x : typed_lvalue).ty = ty))
+ (fun (x, ty) -> assert ((x : typed_pattern).ty = ty))
(List.combine outputs inst_sg.outputs);
(* Retrieve the function id, and register the function call in the context
* if necessary *)
@@ -1326,7 +1326,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
let given_back_inputs = List.combine given_back inputs in
(* Sanity check *)
List.iter
- (fun ((given_back, input) : typed_lvalue * var) ->
+ (fun ((given_back, input) : typed_pattern * var) ->
log#ldebug
(lazy
("\n- given_back ty: "
@@ -1364,7 +1364,7 @@ and translate_expansion (config : config) (p : S.mplace option)
let next_e = translate_expression config e ctx in
let monadic = false in
mk_let monadic
- (mk_typed_lvalue_from_var var None)
+ (mk_typed_pattern_from_var var None)
(mk_opt_mplace_texpression scrutinee_mplace scrutinee)
next_e
| SeAdt _ ->
@@ -1388,9 +1388,9 @@ and translate_expansion (config : config) (p : S.mplace option)
(* This is an enumeration: introduce an [ExpandEnum] let-binding *)
let variant_id = Option.get variant_id in
let lvars =
- List.map (fun v -> mk_typed_lvalue_from_var v None) vars
+ List.map (fun v -> mk_typed_pattern_from_var v None) vars
in
- let lv = mk_adt_lvalue scrutinee.ty variant_id lvars in
+ let lv = mk_adt_pattern scrutinee.ty variant_id lvars in
let monadic = false in
mk_let monadic lv
@@ -1421,16 +1421,16 @@ and translate_expansion (config : config) (p : S.mplace option)
(fun (fid, var) e ->
let field_proj = gen_field_proj fid var in
mk_let monadic
- (mk_typed_lvalue_from_var var None)
+ (mk_typed_pattern_from_var var None)
field_proj e)
id_var_pairs branch
| T.Tuple ->
let vars =
- List.map (fun x -> mk_typed_lvalue_from_var x None) vars
+ List.map (fun x -> mk_typed_pattern_from_var x None) vars
in
let monadic = false in
mk_let monadic
- (mk_simpl_tuple_lvalue vars)
+ (mk_simpl_tuple_pattern vars)
(mk_opt_mplace_texpression scrutinee_mplace scrutinee)
branch
| T.Assumed T.Box ->
@@ -1444,7 +1444,7 @@ and translate_expansion (config : config) (p : S.mplace option)
* identity when extracted (`box a == a`) *)
let monadic = false in
mk_let monadic
- (mk_typed_lvalue_from_var var None)
+ (mk_typed_pattern_from_var var None)
(mk_opt_mplace_texpression scrutinee_mplace scrutinee)
branch
| T.Assumed T.Vec ->
@@ -1465,10 +1465,10 @@ and translate_expansion (config : config) (p : S.mplace option)
let variant_id = Option.get variant_id in
let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
let vars =
- List.map (fun x -> mk_typed_lvalue_from_var x None) vars
+ List.map (fun x -> mk_typed_pattern_from_var x None) vars
in
let pat_ty = scrutinee.ty in
- let pat = mk_adt_lvalue pat_ty variant_id vars in
+ let pat = mk_adt_pattern pat_ty variant_id vars in
let branch = translate_expression config branch ctx in
{ pat; branch }
in
@@ -1506,13 +1506,15 @@ and translate_expansion (config : config) (p : S.mplace option)
(* We don't need to update the context: we don't introduce any
* new values/variables *)
let branch = translate_expression config branch_e ctx in
- let pat = mk_typed_lvalue_from_constant_value (V.Scalar v) in
+ let pat = mk_typed_pattern_from_constant_value (V.Scalar v) in
{ pat; branch }
in
let branches = List.map translate_branch branches in
let otherwise = translate_expression config otherwise ctx in
let pat_ty = Integer int_ty in
- let otherwise_pat : typed_lvalue = { value = LvVar Dummy; ty = pat_ty } in
+ let otherwise_pat : typed_pattern =
+ { value = PatVar Dummy; ty = pat_ty }
+ in
let otherwise : match_branch =
{ pat = otherwise_pat; branch = otherwise }
in
@@ -1584,7 +1586,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
in
let inputs = List.append ctx.forward_inputs backward_inputs in
let inputs_lvs =
- List.map (fun v -> mk_typed_lvalue_from_var v None) inputs
+ List.map (fun v -> mk_typed_pattern_from_var v None) inputs
in
(* Sanity check *)
assert (
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 06:45:21 +0000