summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorEscherichia2024-06-18 22:47:35 +0200
committerGitHub2024-06-18 22:47:35 +0200
commitaa8e74197687ecc6d8f925babc8ba3cd6c739990 (patch)
treef9975ae9f6276e8bd9db866621497a53485007d1 /compiler
parent370f2668f0a36fb31ed9abb4ba613dad333cf406 (diff)
Support for renaming using the rename attribute in charon (#239)
* support for renaming using the rename attribute in charon * support for global decl * add support for renaming field * applied suggested changes and began adding support for variant * finished support for renaming variant * applied suggested changes * add tests * fixed variant and field renaming * update charon-pin * update flake.lock * Update the charon pin * Fix an issue with renaming trait method implementations * Fix an issue with the renaming of trait implementations * Fix an issue when renaming enumerations * Update the Charon pin * Fix the F* tests * Fix an issue with the spans for the loops * Fix the tests * Update a comment * Use fuel in the coq tests * Generate the template decreases clauses by default --------- Co-authored-by: Escherichia <escherichia@charlotte> Co-authored-by: Son Ho <hosonmarc@gmail.com>
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Config.ml9
-rw-r--r--compiler/Extract.ml293
-rw-r--r--compiler/ExtractBase.ml187
-rw-r--r--compiler/ExtractTypes.ml162
-rw-r--r--compiler/Main.ml17
-rw-r--r--compiler/PrintPure.ml4
-rw-r--r--compiler/Pure.ml24
-rw-r--r--compiler/PureMicroPasses.ml59
-rw-r--r--compiler/PureUtils.ml4
-rw-r--r--compiler/SymbolicToPure.ml16
10 files changed, 484 insertions, 291 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 584635bc..98a5eea1 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -214,10 +214,13 @@ let test_trans_unit_functions = ref false
let extract_decreases_clauses = ref false
(** In order to help the user, we can generate "template" decrease clauses/ termination
- measures (i.e., definitions with proper signatures but dummy bodies) in a dedicated
- file.
+ measures (i.e., definitions with proper signatures but dummy bodies) in a dedicated
+ file.
+
+ We initialize it to [true], then deactivate it depending on the CL options
+ given by the user.
*)
-let extract_template_decreases_clauses = ref false
+let extract_template_decreases_clauses = ref true
(** {1 Micro passes} *)
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index b1adb936..6c6b7f0e 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -46,7 +46,8 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
let f = def.f in
let open ExtractBuiltin in
let fun_id = (Pure.FunId (FRegular f.def_id), f.loop_id) in
- ctx_add f.span (FunId (FromLlbc fun_id)) fun_info.extract_name ctx
+ ctx_add f.item_meta.span (FunId (FromLlbc fun_id))
+ fun_info.extract_name ctx
| None ->
(* Not builtin *)
(* If this is a trait method implementation, we prefix the name with the
@@ -60,7 +61,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
(* Add the decreases proof for Lean only *)
match backend () with
| Coq | FStar -> ctx
- | HOL4 -> craise __FILE__ __LINE__ def.span "Unexpected"
+ | HOL4 -> craise __FILE__ __LINE__ def.item_meta.span "Unexpected"
| Lean -> ctx_add_decreases_proof def ctx
else ctx
in
@@ -467,9 +468,10 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
if not method_id.is_provided then (
(* Required method *)
- sanity_check __FILE__ __LINE__ (lp_id = None) trait_decl.span;
- extract_trait_ref trait_decl.span ctx fmt TypeDeclId.Set.empty true
- trait_ref;
+ sanity_check __FILE__ __LINE__ (lp_id = None)
+ trait_decl.item_meta.span;
+ extract_trait_ref trait_decl.item_meta.span ctx fmt
+ TypeDeclId.Set.empty true trait_ref;
let fun_name =
ctx_get_trait_method span trait_ref.trait_decl_ref.trait_decl_id
method_name ctx
@@ -482,7 +484,9 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
(* Provided method: we see it as a regular function call, and use
the function name *)
let fun_id = FromLlbc (FunId (FRegular method_id.id), lp_id) in
- let fun_name = ctx_get_function trait_decl.span fun_id ctx in
+ let fun_name =
+ ctx_get_function trait_decl.item_meta.span fun_id ctx
+ in
F.pp_print_string fmt fun_name;
(* Note that we do not need to print the generics for the trait
@@ -491,8 +495,8 @@ and extract_function_call (span : Meta.span) (ctx : extraction_ctx)
Print the trait ref (to instantate the self clause) *)
F.pp_print_space fmt ();
- extract_trait_ref trait_decl.span ctx fmt TypeDeclId.Set.empty true
- trait_ref
+ extract_trait_ref trait_decl.item_meta.span ctx fmt
+ TypeDeclId.Set.empty true trait_ref
| _ ->
let fun_name = ctx_get_function span fun_id ctx in
F.pp_print_string fmt fun_name);
@@ -1146,7 +1150,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
match def.kind with
| TraitItemProvided (decl_id, _) ->
let trait_decl = T.TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
- let ctx, _ = ctx_add_trait_self_clause def.span ctx in
+ let ctx, _ = ctx_add_trait_self_clause def.item_meta.span ctx in
let ctx = { ctx with is_provided_method = true } in
(ctx, Some trait_decl)
| _ -> (ctx, None)
@@ -1154,14 +1158,14 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
(* Add the type parameters - note that we need those bindings only for the
* body translation (they are not top-level) *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params def.span def.llbc_name def.signature.llbc_generics
- def.signature.generics ctx
+ ctx_add_generic_params def.item_meta.span def.llbc_name
+ def.signature.llbc_generics def.signature.generics ctx
in
(* Print the generics *)
(* Open a box for the generics *)
F.pp_open_hovbox fmt 0;
(let space = Some space in
- extract_generic_params def.span ctx fmt TypeDeclId.Set.empty ~space
+ extract_generic_params def.item_meta.span ctx fmt TypeDeclId.Set.empty ~space
~trait_decl def.signature.generics type_params cg_params trait_clauses);
(* Close the box for the generics *)
F.pp_close_box fmt ();
@@ -1176,11 +1180,14 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
(* Open a box for the input parameter *)
F.pp_open_hovbox fmt 0;
F.pp_print_string fmt "(";
- let ctx = extract_typed_pattern def.span ctx fmt true false lv in
+ let ctx =
+ extract_typed_pattern def.item_meta.span ctx fmt true false lv
+ in
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- extract_ty def.span ctx fmt TypeDeclId.Set.empty false lv.ty;
+ extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty false
+ lv.ty;
F.pp_print_string fmt ")";
(* Close the box for the input parameters *)
F.pp_close_box fmt ();
@@ -1199,7 +1206,7 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : unit =
let extract_param (ty : ty) : unit =
let inside = false in
- extract_ty def.span ctx fmt TypeDeclId.Set.empty inside ty;
+ extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty inside ty;
F.pp_print_space fmt ();
extract_arrow fmt ();
F.pp_print_space fmt ()
@@ -1209,7 +1216,8 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx)
let extract_fun_inputs_output_parameters_types (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : unit =
extract_fun_input_parameters_types ctx fmt def;
- extract_ty def.span ctx fmt TypeDeclId.Set.empty false def.signature.output
+ extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty false
+ def.signature.output
let assert_backend_supports_decreases_clauses (span : Meta.span) =
match backend () with
@@ -1238,13 +1246,13 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : unit =
cassert __FILE__ __LINE__
(backend () = FStar)
- def.span
+ def.item_meta.span
"The generation of template decrease clauses is only supported for the F* \
backend";
(* Retrieve the function name *)
let def_name =
- ctx_get_termination_measure def.span def.def_id def.loop_id ctx
+ ctx_get_termination_measure def.item_meta.span def.def_id def.loop_id ctx
in
(* Add a break before *)
F.pp_print_break fmt 0 0;
@@ -1256,7 +1264,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
in
extract_comment_with_raw_span ctx fmt
[ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
- name def.span.span);
+ name def.item_meta.span.span);
F.pp_print_space fmt ();
(* Open a box for the definition, so that whenever possible it gets printed on
* one line *)
@@ -1309,7 +1317,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : unit =
cassert __FILE__ __LINE__
(backend () = Lean)
- def.span
+ def.item_meta.span
"The generation of template termination and decreasing clauses is only \
supported for the Lean backend";
(*
@@ -1317,7 +1325,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
*)
(* Retrieve the function name *)
let def_name =
- ctx_get_termination_measure def.span def.def_id def.loop_id ctx
+ ctx_get_termination_measure def.item_meta.span def.def_id def.loop_id ctx
in
let def_body = Option.get def.body in
(* Add a break before *)
@@ -1325,7 +1333,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(* Print a comment to link the extracted type to its original rust definition *)
extract_comment_with_raw_span ctx fmt
[ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]
- None def.span.span;
+ None def.item_meta.span.span;
F.pp_print_space fmt ();
(* Open a box for the definition, so that whenever possible it gets printed on
* one line *)
@@ -1353,7 +1361,8 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
let vars = List.map (fun (v : var) -> v.id) def_body.inputs in
if List.length vars = 1 then
- F.pp_print_string fmt (ctx_get_var def.span (List.hd vars) ctx_body)
+ F.pp_print_string fmt
+ (ctx_get_var def.item_meta.span (List.hd vars) ctx_body)
else (
F.pp_open_hovbox fmt 0;
F.pp_print_string fmt "(";
@@ -1361,7 +1370,8 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(fun () ->
F.pp_print_string fmt ",";
F.pp_print_space fmt ())
- (fun v -> F.pp_print_string fmt (ctx_get_var def.span v ctx_body))
+ (fun v ->
+ F.pp_print_string fmt (ctx_get_var def.item_meta.span v ctx_body))
vars;
F.pp_print_string fmt ")";
F.pp_close_box fmt ());
@@ -1375,12 +1385,14 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(*
* Extract a template for the decreases proof
*)
- let def_name = ctx_get_decreases_proof def.span def.def_id def.loop_id ctx in
+ let def_name =
+ ctx_get_decreases_proof def.item_meta.span def.def_id def.loop_id ctx
+ in
(* syntax <def_name> term ... term : tactic *)
F.pp_print_break fmt 0 0;
extract_comment_with_raw_span ctx fmt
[ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]
- None def.span.span;
+ None def.item_meta.span.span;
F.pp_print_space fmt ();
F.pp_open_hvbox fmt 0;
F.pp_print_string fmt "syntax \"";
@@ -1398,7 +1410,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(fun v ->
F.pp_print_space fmt ();
F.pp_print_string fmt "$";
- F.pp_print_string fmt (ctx_get_var def.span v ctx_body))
+ F.pp_print_string fmt (ctx_get_var def.item_meta.span v ctx_body))
vars;
F.pp_print_string fmt ") =>";
F.pp_close_box fmt ();
@@ -1425,7 +1437,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
Some def.llbc_name
else None
in
- extract_comment_with_raw_span ctx fmt comment name def.span.span
+ extract_comment_with_raw_span ctx fmt comment name def.item_meta.span.span
(** Extract a function declaration.
@@ -1436,9 +1448,13 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
- sanity_check __FILE__ __LINE__ (not def.is_global_decl_body) def.span;
+ sanity_check __FILE__ __LINE__
+ (not def.is_global_decl_body)
+ def.item_meta.span;
(* Retrieve the function name *)
- let def_name = ctx_get_local_function def.span def.def_id def.loop_id ctx in
+ let def_name =
+ ctx_get_local_function def.item_meta.span def.def_id def.loop_id ctx
+ in
(* Add a break before *)
if backend () <> HOL4 || not (decl_is_first_from_group kind) then
F.pp_print_break fmt 0 0;
@@ -1512,18 +1528,18 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
if is_opaque then extract_fun_input_parameters_types ctx fmt def;
(* [Tot] *)
if has_decreases_clause then (
- assert_backend_supports_decreases_clauses def.span;
+ assert_backend_supports_decreases_clauses def.item_meta.span;
if backend () = FStar then (
F.pp_print_string fmt "Tot";
F.pp_print_space fmt ()));
- extract_ty def.span ctx fmt TypeDeclId.Set.empty has_decreases_clause
- def.signature.output;
+ extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty
+ has_decreases_clause def.signature.output;
(* Close the box for the return type *)
F.pp_close_box fmt ();
(* Print the decrease clause - rk.: a function with a decreases clause
* is necessarily a transparent function *)
if has_decreases_clause && backend () = FStar then (
- assert_backend_supports_decreases_clauses def.span;
+ assert_backend_supports_decreases_clauses def.item_meta.span;
F.pp_print_space fmt ();
(* Open a box for the decreases clause *)
F.pp_open_hovbox fmt ctx.indent_incr;
@@ -1534,7 +1550,8 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_open_hovbox fmt ctx.indent_incr;
(* The name of the decrease clause *)
let decr_name =
- ctx_get_termination_measure def.span def.def_id def.loop_id ctx
+ ctx_get_termination_measure def.item_meta.span def.def_id def.loop_id
+ ctx
in
F.pp_print_string fmt decr_name;
(* Print the generic parameters - TODO: we do this many
@@ -1565,7 +1582,9 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
List.fold_left
(fun ctx (lv : typed_pattern) ->
F.pp_print_space fmt ();
- let ctx = extract_typed_pattern def.span ctx fmt true false lv in
+ let ctx =
+ extract_typed_pattern def.item_meta.span ctx fmt true false lv
+ in
ctx)
ctx inputs_lvs
in
@@ -1592,7 +1611,8 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_open_hvbox fmt 0;
(* Extract the body *)
let _ =
- extract_texpression def.span ctx_body fmt false (Option.get def.body).body
+ extract_texpression def.item_meta.span ctx_body fmt false
+ (Option.get def.body).body
in
(* Close the box for the body *)
F.pp_close_box fmt ());
@@ -1609,7 +1629,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* termination_by *)
let terminates_name =
- ctx_get_termination_measure def.span def.def_id def.loop_id ctx
+ ctx_get_termination_measure def.item_meta.span def.def_id def.loop_id ctx
in
F.pp_print_break fmt 0 0;
(* Open a box for the whole [termination_by CALL => DECREASES] *)
@@ -1622,7 +1642,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
List.iter
(fun v ->
F.pp_print_space fmt ();
- F.pp_print_string fmt (ctx_get_var def.span v ctx_body))
+ F.pp_print_string fmt (ctx_get_var def.item_meta.span v ctx_body))
all_vars;
F.pp_print_space fmt ();
F.pp_print_string fmt "=>";
@@ -1642,7 +1662,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
List.iter
(fun v ->
F.pp_print_space fmt ();
- F.pp_print_string fmt (ctx_get_var def.span v ctx_body))
+ F.pp_print_string fmt (ctx_get_var def.item_meta.span v ctx_body))
vars;
(* Close the box for [DECREASES] *)
F.pp_close_box fmt ();
@@ -1653,7 +1673,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the [decreasing by ...] *)
F.pp_open_hvbox fmt ctx.indent_incr;
let decreases_name =
- ctx_get_decreases_proof def.span def.def_id def.loop_id ctx
+ ctx_get_decreases_proof def.item_meta.span def.def_id def.loop_id ctx
in
F.pp_print_string fmt "decreasing_by";
F.pp_print_space fmt ();
@@ -1662,7 +1682,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
List.iter
(fun v ->
F.pp_print_space fmt ();
- F.pp_print_string fmt (ctx_get_var def.span v ctx_body))
+ F.pp_print_string fmt (ctx_get_var def.item_meta.span v ctx_body))
vars;
F.pp_close_box fmt ();
(* Close the box for the [decreasing by ...] *)
@@ -1692,16 +1712,18 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
(def : fun_decl) : unit =
(* Retrieve the definition name *)
- let def_name = ctx_get_local_function def.span def.def_id def.loop_id ctx in
+ let def_name =
+ ctx_get_local_function def.item_meta.span def.def_id def.loop_id ctx
+ in
cassert __FILE__ __LINE__
(def.signature.generics.const_generics = [])
- def.span
+ def.item_meta.span
"Constant generics are not supported yet when generating code for HOL4";
(* Add the type/const gen parameters - note that we need those bindings
only for the generation of the type (they are not top-level) *)
let ctx, _, _, _ =
- ctx_add_generic_params def.span def.llbc_name def.signature.llbc_generics
- def.signature.generics ctx
+ ctx_add_generic_params def.item_meta.span def.llbc_name
+ def.signature.llbc_generics def.signature.generics ctx
in
(* Add breaks to insert new lines between definitions *)
F.pp_print_break fmt 0 0;
@@ -1717,7 +1739,8 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "“:";
(* Generate the type *)
extract_fun_input_parameters_types ctx fmt def;
- extract_ty def.span ctx fmt TypeDeclId.Set.empty false def.signature.output;
+ extract_ty def.item_meta.span ctx fmt TypeDeclId.Set.empty false
+ def.signature.output;
(* Close the box for the type *)
F.pp_print_string fmt "”";
F.pp_close_box fmt ();
@@ -1742,7 +1765,9 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
- sanity_check __FILE__ __LINE__ (not def.is_global_decl_body) def.span;
+ sanity_check __FILE__ __LINE__
+ (not def.is_global_decl_body)
+ def.item_meta.span;
(* We treat HOL4 opaque functions in a specific manner *)
if backend () = HOL4 && Option.is_none def.body then
extract_fun_decl_hol4_opaque ctx fmt def
@@ -1892,7 +1917,7 @@ let extract_global_decl_hol4_opaque (span : Meta.span) (ctx : extraction_ctx)
*)
let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
(global : global_decl) (body : fun_decl) (interface : bool) : unit =
- let span = body.span in
+ let span = body.item_meta.span in
sanity_check __FILE__ __LINE__ body.is_global_decl_body span;
sanity_check __FILE__ __LINE__ (body.signature.inputs = []) span;
@@ -2018,7 +2043,7 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
(* Register the names *)
List.fold_left
(fun ctx (cid, cname) ->
- ctx_add trait_decl.span
+ ctx_add trait_decl.item_meta.span
(TraitParentClauseId (trait_decl.def_id, cid))
cname ctx)
ctx clause_names
@@ -2053,7 +2078,7 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
(* Register the names *)
List.fold_left
(fun ctx (item_name, name) ->
- ctx_add trait_decl.span
+ ctx_add trait_decl.item_meta.span
(TraitItemId (trait_decl.def_id, item_name))
name ctx)
ctx constant_names
@@ -2114,13 +2139,13 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
List.fold_left
(fun ctx (item_name, (type_name, clauses)) ->
let ctx =
- ctx_add trait_decl.span
+ ctx_add trait_decl.item_meta.span
(TraitItemId (trait_decl.def_id, item_name))
type_name ctx
in
List.fold_left
(fun ctx (clause_id, clause_name) ->
- ctx_add trait_decl.span
+ ctx_add trait_decl.item_meta.span
(TraitItemClauseId (trait_decl.def_id, item_name, clause_id))
clause_name ctx)
ctx clauses)
@@ -2172,7 +2197,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
(* Register the names *)
List.fold_left
(fun ctx (item_name, fun_name) ->
- ctx_add trait_decl.span
+ ctx_add trait_decl.item_meta.span
(TraitMethodId (trait_decl.def_id, item_name))
fun_name ctx)
ctx method_names
@@ -2195,9 +2220,10 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
| Some info -> (info.extract_name, info.constructor)
in
let ctx =
- ctx_add trait_decl.span (TraitDeclId trait_decl.def_id) trait_name ctx
+ ctx_add trait_decl.item_meta.span (TraitDeclId trait_decl.def_id)
+ trait_name ctx
in
- ctx_add trait_decl.span (TraitDeclConstructorId trait_decl.def_id)
+ ctx_add trait_decl.item_meta.span (TraitDeclConstructorId trait_decl.def_id)
trait_constructor ctx
in
(* Parent clauses *)
@@ -2254,7 +2280,7 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
(* For now we do not support overriding provided methods *)
cassert __FILE__ __LINE__
(trait_impl.provided_methods = [])
- trait_impl.span
+ trait_impl.item_meta.span
("Overriding trait provided methods in trait implementations is not \
supported yet (overriden methods: "
^ String.concat ", " (List.map fst trait_impl.provided_methods)
@@ -2267,7 +2293,7 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
| None -> ctx_compute_trait_impl_name ctx trait_decl trait_impl
| Some name -> name
in
- ctx_add trait_decl.span (TraitImplId trait_impl.def_id) name ctx
+ ctx_add trait_decl.item_meta.span (TraitImplId trait_impl.def_id) name ctx
(** Small helper.
@@ -2316,7 +2342,9 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
let trans = A.FunDeclId.Map.find id ctx.trans_funs in
(* Extract the items *)
let f = trans.f in
- let fun_name = ctx_get_trait_method decl.span decl.def_id item_name ctx in
+ let fun_name =
+ ctx_get_trait_method decl.item_meta.span decl.def_id item_name ctx
+ in
let ty () =
(* Extract the generics *)
(* We need to add the generics specific to the method, by removing those
@@ -2332,8 +2360,8 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
- we only generate trait clauses for the clauses we find in the
pure generics *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params decl.span f.llbc_name f.signature.llbc_generics
- generics ctx
+ ctx_add_generic_params decl.item_meta.span f.llbc_name
+ f.signature.llbc_generics generics ctx
in
let backend_uses_forall =
match backend () with Coq | Lean -> true | FStar | HOL4 -> false
@@ -2342,8 +2370,8 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
let use_forall = generics_not_empty && backend_uses_forall in
let use_arrows = generics_not_empty && not backend_uses_forall in
let use_forall_use_sep = false in
- extract_generic_params decl.span ctx fmt TypeDeclId.Set.empty ~use_forall
- ~use_forall_use_sep ~use_arrows generics type_params cg_params
+ extract_generic_params decl.item_meta.span ctx fmt TypeDeclId.Set.empty
+ ~use_forall ~use_forall_use_sep ~use_arrows generics type_params cg_params
trait_clauses;
if use_forall then F.pp_print_string fmt ",";
(* Extract the inputs and output *)
@@ -2356,7 +2384,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(decl : trait_decl) : unit =
(* Retrieve the trait name *)
- let decl_name = ctx_get_trait_decl decl.span decl.def_id ctx in
+ let decl_name = ctx_get_trait_decl decl.item_meta.span decl.def_id ctx in
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
@@ -2367,7 +2395,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
in
extract_comment_with_raw_span ctx fmt
[ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
- name decl.span.span);
+ name decl.item_meta.span.span);
F.pp_print_break fmt 0 0;
(* Open two outer boxes for the definition, so that whenever possible it gets printed on
one line and indents are correct.
@@ -2384,7 +2412,8 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Open the box for the name + generics *)
F.pp_open_hovbox fmt ctx.indent_incr;
let qualif =
- Option.get (type_decl_kind_to_qualif decl.span SingleNonRec (Some Struct))
+ Option.get
+ (type_decl_kind_to_qualif decl.item_meta.span SingleNonRec (Some Struct))
in
(* When checking if the trait declaration is empty: we ignore the provided
methods, because for now they are extracted separately *)
@@ -2400,11 +2429,11 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add the type and const generic params - note that we need those bindings only for the
* body translation (they are not top-level) *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params decl.span decl.llbc_name decl.llbc_generics generics
- ctx
+ ctx_add_generic_params decl.item_meta.span decl.llbc_name decl.llbc_generics
+ generics ctx
in
- extract_generic_params decl.span ctx fmt TypeDeclId.Set.empty generics
- type_params cg_params trait_clauses;
+ extract_generic_params decl.item_meta.span ctx fmt TypeDeclId.Set.empty
+ generics type_params cg_params trait_clauses;
F.pp_print_space fmt ();
if is_empty && backend () = FStar then (
@@ -2413,7 +2442,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_close_box fmt ())
else if is_empty && backend () = Coq then (
(* Coq is not very good at infering constructors *)
- let cons = ctx_get_trait_constructor decl.span decl.def_id ctx in
+ let cons = ctx_get_trait_constructor decl.item_meta.span decl.def_id ctx in
F.pp_print_string fmt (":= " ^ cons ^ "{}.");
(* Outer box *)
F.pp_close_box fmt ())
@@ -2422,7 +2451,9 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
| Lean -> F.pp_print_string fmt "where"
| FStar -> F.pp_print_string fmt "= {"
| Coq ->
- let cons = ctx_get_trait_constructor decl.span decl.def_id ctx in
+ let cons =
+ ctx_get_trait_constructor decl.item_meta.span decl.def_id ctx
+ in
F.pp_print_string fmt (":= " ^ cons ^ " {")
| _ -> F.pp_print_string fmt "{");
@@ -2436,11 +2467,13 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* The constants *)
List.iter
(fun (name, (ty, _)) ->
- let item_name = ctx_get_trait_const decl.span decl.def_id name ctx in
+ let item_name =
+ ctx_get_trait_const decl.item_meta.span decl.def_id name ctx
+ in
let ty () =
let inside = false in
F.pp_print_space fmt ();
- extract_ty decl.span ctx fmt TypeDeclId.Set.empty inside ty
+ extract_ty decl.item_meta.span ctx fmt TypeDeclId.Set.empty inside ty
in
extract_trait_decl_item ctx fmt item_name ty)
decl.consts;
@@ -2449,23 +2482,25 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
List.iter
(fun (name, (clauses, _)) ->
(* Extract the type *)
- let item_name = ctx_get_trait_type decl.span decl.def_id name ctx in
+ let item_name =
+ ctx_get_trait_type decl.item_meta.span decl.def_id name ctx
+ in
let ty () =
F.pp_print_space fmt ();
- F.pp_print_string fmt (type_keyword decl.span)
+ F.pp_print_string fmt (type_keyword decl.item_meta.span)
in
extract_trait_decl_item ctx fmt item_name ty;
(* Extract the clauses *)
List.iter
(fun clause ->
let item_name =
- ctx_get_trait_item_clause decl.span decl.def_id name
+ ctx_get_trait_item_clause decl.item_meta.span decl.def_id name
clause.clause_id ctx
in
let ty () =
F.pp_print_space fmt ();
- extract_trait_clause_type decl.span ctx fmt TypeDeclId.Set.empty
- clause
+ extract_trait_clause_type decl.item_meta.span ctx fmt
+ TypeDeclId.Set.empty clause
in
extract_trait_decl_item ctx fmt item_name ty)
clauses)
@@ -2476,12 +2511,13 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
List.iter
(fun clause ->
let item_name =
- ctx_get_trait_parent_clause decl.span decl.def_id clause.clause_id ctx
+ ctx_get_trait_parent_clause decl.item_meta.span decl.def_id
+ clause.clause_id ctx
in
let ty () =
F.pp_print_space fmt ();
- extract_trait_clause_type decl.span ctx fmt TypeDeclId.Set.empty
- clause
+ extract_trait_clause_type decl.item_meta.span ctx fmt
+ TypeDeclId.Set.empty clause
in
extract_trait_decl_item ctx fmt item_name ty)
decl.parent_clauses;
@@ -2518,25 +2554,31 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
in
if num_params > 0 then (
(* The constructor *)
- let cons_name = ctx_get_trait_constructor decl.span decl.def_id ctx in
+ let cons_name =
+ ctx_get_trait_constructor decl.item_meta.span decl.def_id ctx
+ in
extract_coq_arguments_instruction ctx fmt cons_name num_params;
(* The constants *)
List.iter
(fun (name, _) ->
- let item_name = ctx_get_trait_const decl.span decl.def_id name ctx in
+ let item_name =
+ ctx_get_trait_const decl.item_meta.span decl.def_id name ctx
+ in
extract_coq_arguments_instruction ctx fmt item_name num_params)
decl.consts;
(* The types *)
List.iter
(fun (name, (clauses, _)) ->
(* The type *)
- let item_name = ctx_get_trait_type decl.span decl.def_id name ctx in
+ let item_name =
+ ctx_get_trait_type decl.item_meta.span decl.def_id name ctx
+ in
extract_coq_arguments_instruction ctx fmt item_name num_params;
(* The type clauses *)
List.iter
(fun clause ->
let item_name =
- ctx_get_trait_item_clause decl.span decl.def_id name
+ ctx_get_trait_item_clause decl.item_meta.span decl.def_id name
clause.clause_id ctx
in
extract_coq_arguments_instruction ctx fmt item_name num_params)
@@ -2546,7 +2588,8 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
List.iter
(fun clause ->
let item_name =
- ctx_get_trait_parent_clause decl.span decl.def_id clause.clause_id ctx
+ ctx_get_trait_parent_clause decl.item_meta.span decl.def_id
+ clause.clause_id ctx
in
extract_coq_arguments_instruction ctx fmt item_name num_params)
decl.parent_clauses;
@@ -2555,7 +2598,7 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
(fun (item_name, _) ->
(* Extract the items *)
let item_name =
- ctx_get_trait_method decl.span decl.def_id item_name ctx
+ ctx_get_trait_method decl.item_meta.span decl.def_id item_name ctx
in
extract_coq_arguments_instruction ctx fmt item_name num_params)
decl.required_methods;
@@ -2581,7 +2624,9 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
let trans = A.FunDeclId.Map.find id ctx.trans_funs in
(* Extract the items *)
let f = trans.f in
- let fun_name = ctx_get_trait_method impl.span trait_decl_id item_name ctx in
+ let fun_name =
+ ctx_get_trait_method impl.item_meta.span trait_decl_id item_name ctx
+ in
let ty () =
(* Filter the generics if the method is a builtin *)
let i_tys, _, _ = impl_generics in
@@ -2621,16 +2666,18 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
- we only generate trait clauses for the clauses we find in the
pure generics *)
let ctx, f_tys, f_cgs, f_tcs =
- ctx_add_generic_params impl.span f.llbc_name f.signature.llbc_generics
- f_generics ctx
+ ctx_add_generic_params impl.item_meta.span f.llbc_name
+ f.signature.llbc_generics f_generics ctx
in
let use_forall = f_generics <> empty_generic_params in
- extract_generic_params impl.span ctx fmt TypeDeclId.Set.empty ~use_forall
- f_generics f_tys f_cgs f_tcs;
+ extract_generic_params impl.item_meta.span ctx fmt TypeDeclId.Set.empty
+ ~use_forall f_generics f_tys f_cgs f_tcs;
if use_forall then F.pp_print_string fmt ",";
(* Extract the function call *)
F.pp_print_space fmt ();
- let fun_name = ctx_get_local_function impl.span f.def_id None ctx in
+ let fun_name =
+ ctx_get_local_function impl.item_meta.span f.def_id None ctx
+ in
F.pp_print_string fmt fun_name;
let all_generics =
let _, i_cgs, i_tcs = impl_generics in
@@ -2651,7 +2698,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(impl : trait_impl) : unit =
log#ldebug (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.llbc_name));
(* Retrieve the impl name *)
- let impl_name = ctx_get_trait_impl impl.span impl.def_id ctx in
+ let impl_name = ctx_get_trait_impl impl.item_meta.span impl.def_id ctx in
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
@@ -2667,7 +2714,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
extract_comment_with_raw_span ctx fmt
[ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
(* TODO: why option option for the generics? Looks like a bug in OCaml!? *)
- name ?generics:(Some generics) impl.span.span);
+ name ?generics:(Some generics) impl.item_meta.span.span);
F.pp_print_break fmt 0 0;
(* Open two outer boxes for the definition, so that whenever possible it gets printed on
@@ -2697,18 +2744,18 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add the type and const generic params - note that we need those bindings only for the
* body translation (they are not top-level) *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params impl.span impl.llbc_name impl.llbc_generics
+ ctx_add_generic_params impl.item_meta.span impl.llbc_name impl.llbc_generics
impl.generics ctx
in
let all_generics = (type_params, cg_params, trait_clauses) in
- extract_generic_params impl.span ctx fmt TypeDeclId.Set.empty impl.generics
- type_params cg_params trait_clauses;
+ extract_generic_params impl.item_meta.span ctx fmt TypeDeclId.Set.empty
+ impl.generics type_params cg_params trait_clauses;
(* Print the type *)
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- extract_trait_decl_ref impl.span ctx fmt TypeDeclId.Set.empty false
+ extract_trait_decl_ref impl.item_meta.span ctx fmt TypeDeclId.Set.empty false
impl.impl_trait;
(* When checking if the trait impl is empty: we ignore the provided
@@ -2723,7 +2770,8 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
else if is_empty && backend () = Coq then (
(* Coq is not very good at infering constructors *)
let cons =
- ctx_get_trait_constructor impl.span impl.impl_trait.trait_decl_id ctx
+ ctx_get_trait_constructor impl.item_meta.span
+ impl.impl_trait.trait_decl_id ctx
in
F.pp_print_string fmt (":= " ^ cons ^ ".");
(* Outer box *)
@@ -2748,13 +2796,15 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(* The constants *)
List.iter
(fun (provided_id, (name, (_, id))) ->
- let item_name = ctx_get_trait_const impl.span trait_decl_id name ctx in
+ let item_name =
+ ctx_get_trait_const impl.item_meta.span trait_decl_id name ctx
+ in
(* The parameters are not the same depending on whether the constant
is a provided constant or not *)
let print_params () =
if provided_id = Some id then
- extract_generic_args impl.span ctx fmt TypeDeclId.Set.empty
- impl.impl_trait.decl_generics
+ extract_generic_args impl.item_meta.span ctx fmt
+ TypeDeclId.Set.empty impl.impl_trait.decl_generics
else
let all_params =
List.concat [ type_params; cg_params; trait_clauses ]
@@ -2767,7 +2817,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
in
let ty () =
F.pp_print_space fmt ();
- F.pp_print_string fmt (ctx_get_global impl.span id ctx);
+ F.pp_print_string fmt (ctx_get_global impl.item_meta.span id ctx);
print_params ()
in
@@ -2778,23 +2828,25 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
List.iter
(fun (name, (trait_refs, ty)) ->
(* Extract the type *)
- let item_name = ctx_get_trait_type impl.span trait_decl_id name ctx in
+ let item_name =
+ ctx_get_trait_type impl.item_meta.span trait_decl_id name ctx
+ in
let ty () =
F.pp_print_space fmt ();
- extract_ty impl.span ctx fmt TypeDeclId.Set.empty false ty
+ extract_ty impl.item_meta.span ctx fmt TypeDeclId.Set.empty false ty
in
extract_trait_impl_item ctx fmt item_name ty;
(* Extract the clauses *)
TraitClauseId.iteri
(fun clause_id trait_ref ->
let item_name =
- ctx_get_trait_item_clause impl.span trait_decl_id name clause_id
- ctx
+ ctx_get_trait_item_clause impl.item_meta.span trait_decl_id name
+ clause_id ctx
in
let ty () =
F.pp_print_space fmt ();
- extract_trait_ref impl.span ctx fmt TypeDeclId.Set.empty false
- trait_ref
+ extract_trait_ref impl.item_meta.span ctx fmt TypeDeclId.Set.empty
+ false trait_ref
in
extract_trait_impl_item ctx fmt item_name ty)
trait_refs)
@@ -2804,12 +2856,13 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
TraitClauseId.iteri
(fun clause_id trait_ref ->
let item_name =
- ctx_get_trait_parent_clause impl.span trait_decl_id clause_id ctx
+ ctx_get_trait_parent_clause impl.item_meta.span trait_decl_id
+ clause_id ctx
in
let ty () =
F.pp_print_space fmt ();
- extract_trait_ref impl.span ctx fmt TypeDeclId.Set.empty false
- trait_ref
+ extract_trait_ref impl.item_meta.span ctx fmt TypeDeclId.Set.empty
+ false trait_ref
in
extract_trait_impl_item ctx fmt item_name ty)
impl.parent_trait_refs;
@@ -2873,7 +2926,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
let fun_name =
- ctx_get_local_function def.span def.def_id def.loop_id ctx
+ ctx_get_local_function def.item_meta.span def.def_id def.loop_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
@@ -2883,7 +2936,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "=";
F.pp_print_space fmt ();
let success =
- ctx_get_variant def.span (TAssumed TResult) result_ok_id ctx
+ ctx_get_variant def.item_meta.span (TAssumed TResult) result_ok_id ctx
in
F.pp_print_string fmt (success ^ " ())")
| Coq ->
@@ -2891,7 +2944,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
let fun_name =
- ctx_get_local_function def.span def.def_id def.loop_id ctx
+ ctx_get_local_function def.item_meta.span def.def_id def.loop_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
@@ -2904,7 +2957,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
let fun_name =
- ctx_get_local_function def.span def.def_id def.loop_id ctx
+ ctx_get_local_function def.item_meta.span def.def_id def.loop_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
@@ -2914,14 +2967,14 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "==";
F.pp_print_space fmt ();
let success =
- ctx_get_variant def.span (TAssumed TResult) result_ok_id ctx
+ ctx_get_variant def.item_meta.span (TAssumed TResult) result_ok_id ctx
in
F.pp_print_string fmt (success ^ " ())")
| HOL4 ->
F.pp_print_string fmt "val _ = assert_ok (";
F.pp_print_string fmt "“";
let fun_name =
- ctx_get_local_function def.span def.def_id def.loop_id ctx
+ ctx_get_local_function def.item_meta.span def.def_id def.loop_id ctx
in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 4aac270f..fb65bd5e 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -252,6 +252,14 @@ let empty_names_map : names_map =
names_set = StringSet.empty;
}
+(** Small helper to update an LLBC name if the rename attribute has been set *)
+let rename_llbc_name (item_meta : Meta.item_meta) (llbc_name : llbc_name) =
+ match item_meta.rename with
+ | Some rename ->
+ let name_prefix = List.tl (List.rev llbc_name) in
+ List.rev (T.PeIdent (rename, Disambiguator.zero) :: name_prefix)
+ | None -> llbc_name
+
(** Small helper to report name collision *)
let report_name_collision (id_to_string : id -> string)
((id1, span1) : id * Meta.span option) (id2 : id) (span2 : Meta.span option)
@@ -1384,15 +1392,20 @@ let ctx_compute_simple_name (span : Meta.span) (ctx : extraction_ctx)
let ctx_compute_simple_type_name = ctx_compute_simple_name
(** Helper *)
+let ctx_compute_type_name_no_suffix (ctx : extraction_ctx)
+ (item_meta : Meta.item_meta) (name : llbc_name) : string =
+ let name = rename_llbc_name item_meta name in
+ flatten_name (ctx_compute_simple_type_name item_meta.span ctx name)
-let ctx_compute_type_name_no_suffix (span : Meta.span) (ctx : extraction_ctx)
- (name : llbc_name) : string =
- flatten_name (ctx_compute_simple_type_name span ctx name)
+(** Provided a basename, compute a type name.
-(** Provided a basename, compute a type name. *)
-let ctx_compute_type_name (span : Meta.span) (ctx : extraction_ctx)
+ This is an auxiliary helper that we use to compute type declaration names, but also
+ for instance field and variant names when we need to add the name of the type as a
+ prefix.
+ *)
+let ctx_compute_type_name (item_meta : Meta.item_meta) (ctx : extraction_ctx)
(name : llbc_name) =
- let name = ctx_compute_type_name_no_suffix span ctx name in
+ let name = ctx_compute_type_name_no_suffix ctx item_meta name in
match backend () with
| FStar -> StringUtils.lowercase_first_letter (name ^ "_t")
| Coq | HOL4 -> name ^ "_t"
@@ -1404,45 +1417,57 @@ let ctx_compute_type_name (span : Meta.span) (ctx : extraction_ctx)
- field name
Note that fields don't always have names, but we still need to
- generate some names if we want to extract the structures to records...
- We might want to extract such structures to tuples, later, but field
- access then causes trouble because not all provers accept syntax like
- [x.3] where [x] is a tuple.
+ generate some names if we want to extract the structures to records.
+ For nameless fields, we generate a name based on the index.
+
+ Note that in most situations we extract structures with nameless fields
+ to tuples, meaning generating names by using indices shouldn't be too
+ much of a problem.
*)
-let ctx_compute_field_name (span : Meta.span) (ctx : extraction_ctx)
- (def_name : llbc_name) (field_id : FieldId.id) (field_name : string option)
- : string =
+let ctx_compute_field_name (def : type_decl) (field_meta : Meta.item_meta)
+ (ctx : extraction_ctx) (def_name : llbc_name) (field_id : FieldId.id)
+ (field_name : string option) : string =
+ (* If the user did not provide a name, use the field index. *)
let field_name_s =
- match field_name with
- | Some field_name -> field_name
- | None ->
- (* TODO: extract structs with no field names to tuples *)
- FieldId.to_string field_id
+ Option.value field_name ~default:(FieldId.to_string field_id)
in
- if !Config.record_fields_short_names then
- if field_name = None then (* TODO: this is a bit ugly *)
- "_" ^ field_name_s
- else field_name_s
- else
- let def_name =
- ctx_compute_type_name_no_suffix span ctx def_name ^ "_" ^ field_name_s
- in
- match backend () with
- | Lean | HOL4 -> def_name
- | Coq | FStar -> StringUtils.lowercase_first_letter def_name
+ (* Replace the name of the field if the user annotated it with the [rename] attribute. *)
+ let field_name_s = Option.value field_meta.rename ~default:field_name_s in
+ (* Prefix the name with the name of the type, if necessary (some backends don't
+ support field name collisions) *)
+ let def_name = rename_llbc_name def.item_meta def_name in
+ let name =
+ if !Config.record_fields_short_names then
+ if field_name = None then (* TODO: this is a bit ugly *)
+ "_" ^ field_name_s
+ else field_name_s
+ else
+ ctx_compute_type_name_no_suffix ctx def.item_meta def_name
+ ^ "_" ^ field_name_s
+ in
+ match backend () with
+ | Lean | HOL4 -> name
+ | Coq | FStar -> StringUtils.lowercase_first_letter name
(** Inputs:
- type name
- variant name
*)
-let ctx_compute_variant_name (span : Meta.span) (ctx : extraction_ctx)
- (def_name : llbc_name) (variant : string) : string =
+let ctx_compute_variant_name (ctx : extraction_ctx) (def : type_decl)
+ (variant : variant) : string =
+ (* Replace the name of the variant if the user annotated it with the [rename] attribute. *)
+ let variant =
+ Option.value variant.item_meta.rename ~default:variant.variant_name
+ in
match backend () with
| FStar | Coq | HOL4 ->
let variant = to_camel_case variant in
+ (* Prefix the name of the variant with the name of the type, if necessary
+ (some backends don't support collision of variant names) *)
if !variant_concatenate_type_name then
StringUtils.capitalize_first_letter
- (ctx_compute_type_name_no_suffix span ctx def_name ^ "_" ^ variant)
+ (ctx_compute_type_name_no_suffix ctx def.item_meta def.llbc_name
+ ^ "_" ^ variant)
else variant
| Lean -> variant
@@ -1457,9 +1482,9 @@ let ctx_compute_variant_name (span : Meta.span) (ctx : extraction_ctx)
Inputs:
- type name
*)
-let ctx_compute_struct_constructor (span : Meta.span) (ctx : extraction_ctx)
+let ctx_compute_struct_constructor (def : type_decl) (ctx : extraction_ctx)
(basename : llbc_name) : string =
- let tname = ctx_compute_type_name span ctx basename in
+ let tname = ctx_compute_type_name def.item_meta ctx basename in
ExtractBuiltin.mk_struct_constructor tname
let ctx_compute_fun_name_no_suffix (span : Meta.span) (ctx : extraction_ctx)
@@ -1522,7 +1547,8 @@ let ctx_compute_fun_name (span : Meta.span) (ctx : extraction_ctx)
let ctx_compute_trait_decl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
: string =
- ctx_compute_type_name trait_decl.span ctx trait_decl.llbc_name
+ let llbc_name = rename_llbc_name trait_decl.item_meta trait_decl.llbc_name in
+ ctx_compute_type_name trait_decl.item_meta ctx llbc_name
let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
(trait_impl : trait_impl) : string =
@@ -1531,14 +1557,25 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
for `<foo::Foo, u32>`, we generate the name: "trait.TraitFooFooU32Inst".
Importantly, it is to be noted that the name is independent of the place
where the instance has been defined (it is indepedent of the file, etc.).
+
+ Note that if the user provided a [rename] attribute, we simply use that.
*)
let name =
- let params = trait_impl.llbc_generics in
- let args = trait_impl.llbc_impl_trait.decl_generics in
- let name = ctx_prepare_name trait_impl.span ctx trait_decl.llbc_name in
- trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
+ match trait_impl.item_meta.rename with
+ | None ->
+ let name =
+ let params = trait_impl.llbc_generics in
+ let args = trait_impl.llbc_impl_trait.decl_generics in
+ let name =
+ ctx_prepare_name trait_impl.item_meta.span ctx trait_decl.llbc_name
+ in
+ let name = rename_llbc_name trait_impl.item_meta name in
+ trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
+ in
+ flatten_name name
+ | Some name -> name
in
- let name = flatten_name name in
+ (* Additional modifications to make sure we comply with the backends restrictions *)
match backend () with
| FStar -> StringUtils.lowercase_first_letter name
| Coq | HOL4 | Lean -> name
@@ -1969,21 +2006,23 @@ let ctx_add_generic_params (span : Meta.span) (current_def_name : Types.name)
let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
+ let name = rename_llbc_name def.item_meta def.llbc_name in
let name =
- ctx_compute_decreases_proof_name def.span ctx def.def_id def.llbc_name
+ ctx_compute_decreases_proof_name def.item_meta.span ctx def.def_id name
def.num_loops def.loop_id
in
- ctx_add def.span
+ ctx_add def.item_meta.span
(DecreasesProofId (FRegular def.def_id, def.loop_id))
name ctx
let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
+ let name = rename_llbc_name def.item_meta def.llbc_name in
let name =
- ctx_compute_termination_measure_name def.span ctx def.def_id def.llbc_name
+ ctx_compute_termination_measure_name def.item_meta.span ctx def.def_id name
def.num_loops def.loop_id
in
- ctx_add def.span
+ ctx_add def.item_meta.span
(TerminationMeasureId (FRegular def.def_id, def.loop_id))
name ctx
@@ -2001,7 +2040,8 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
ctx_add def.item_meta.span decl name ctx
| None ->
(* Not the case: "standard" registration *)
- let name = ctx_compute_global_name def.item_meta.span ctx def.name in
+ let name = rename_llbc_name def.item_meta def.name in
+ let name = ctx_compute_global_name def.item_meta.span ctx name in
let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in
(* If this is a provided constant (i.e., the default value for a constant
@@ -2016,21 +2056,66 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
ctx
let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
- (* Add the function name *)
- ctx_compute_fun_name def.span ctx def.llbc_name def.num_loops def.loop_id
+ (* Rename the function, if the user added a [rename] attribute.
+
+ We have to do something peculiar for the implementation of trait
+ methods, by looking up the meta information of the method *declaration*
+ because this is where the attribute is.
+
+ Note that if the user also added an attribute for the *implementation*,
+ we keep this one.
+ *)
+ let item_meta =
+ match def.kind with
+ | TraitItemImpl (_, trait_decl_id, item_name, _) -> (
+ if Option.is_some def.item_meta.rename then def.item_meta
+ else
+ (* Lookup the declaration. TODO: the trait item impl info
+ should directly give us the id of the method declaration. *)
+ match
+ TraitDeclId.Map.find_opt trait_decl_id ctx.trans_trait_decls
+ with
+ | None -> def.item_meta
+ | Some trait_decl -> (
+ let methods =
+ trait_decl.required_methods
+ @ List.filter_map
+ (fun (name, opt_id) ->
+ match opt_id with
+ | None -> None
+ | Some id -> Some (name, id))
+ trait_decl.provided_methods
+ in
+ match
+ List.find_opt (fun (name, _) -> name = item_name) methods
+ with
+ | None -> def.item_meta
+ | Some (_, id) ->
+ Option.value
+ (Option.map
+ (fun (def : A.fun_decl) -> def.item_meta)
+ (FunDeclId.Map.find_opt id
+ ctx.trans_ctx.fun_ctx.fun_decls))
+ ~default:def.item_meta))
+ | _ -> def.item_meta
+ in
+ let llbc_name = rename_llbc_name item_meta def.llbc_name in
+ ctx_compute_fun_name def.item_meta.span ctx llbc_name def.num_loops
+ def.loop_id
(* TODO: move to Extract *)
let ctx_add_fun_decl (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
(* Sanity check: the function should not be a global body - those are handled
* separately *)
- sanity_check __FILE__ __LINE__ (not def.is_global_decl_body) def.span;
- (* Lookup the LLBC def to compute the region group information *)
+ sanity_check __FILE__ __LINE__
+ (not def.is_global_decl_body)
+ def.item_meta.span;
let def_id = def.def_id in
(* Add the function name *)
let def_name = ctx_compute_fun_name def ctx in
let fun_id = (Pure.FunId (FRegular def_id), def.loop_id) in
- ctx_add def.span (FunId (FromLlbc fun_id)) def_name ctx
+ ctx_add def.item_meta.span (FunId (FromLlbc fun_id)) def_name ctx
let ctx_compute_type_decl_name (ctx : extraction_ctx) (def : type_decl) : string
=
- ctx_compute_type_name def.span ctx def.llbc_name
+ ctx_compute_type_name def.item_meta ctx def.llbc_name
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index edd9d58e..a242e950 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -6,6 +6,7 @@ open TranslateCore
open Config
open Errors
include ExtractBase
+module T = Types
(** Format a constant value.
@@ -288,7 +289,8 @@ let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
if is_single_opaque_fun_decl_group dg then ()
else
let compute_fun_def_name (def : Pure.fun_decl) : string =
- ctx_get_local_function def.span def.def_id def.loop_id ctx ^ "_def"
+ ctx_get_local_function def.item_meta.span def.def_id def.loop_id ctx
+ ^ "_def"
in
let names = List.map compute_fun_def_name dg in
(* Add a break before *)
@@ -750,13 +752,15 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
}
| _ -> ctx
in
- (* Compute and register the type def name *)
+ (* Compute and register the type decl name *)
let def_name =
match info with
- | None -> ctx_compute_type_name def.span ctx def.llbc_name
+ | None -> ctx_compute_type_decl_name ctx def
| Some info -> info.extract_name
in
- let ctx = ctx_add def.span (TypeId (TAdtId def.def_id)) def_name ctx in
+ let ctx =
+ ctx_add def.item_meta.span (TypeId (TAdtId def.def_id)) def_name ctx
+ in
(* Compute and register:
* - the variant names, if this is an enumeration
* - the field names, if this is a structure
@@ -778,12 +782,12 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
FieldId.mapi
(fun fid (field : field) ->
( fid,
- ctx_compute_field_name def.span ctx def.llbc_name fid
- field.field_name ))
+ ctx_compute_field_name def field.item_meta ctx
+ def.llbc_name fid field.field_name ))
fields
in
let cons_name =
- ctx_compute_struct_constructor def.span ctx def.llbc_name
+ ctx_compute_struct_constructor def ctx def.llbc_name
in
(field_names, cons_name)
| Some { body_info = Some (Struct (cons_name, field_names)); _ } ->
@@ -800,34 +804,32 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
in
(field_names, cons_name)
| Some info ->
- craise __FILE__ __LINE__ def.span
+ craise __FILE__ __LINE__ def.item_meta.span
("Invalid builtin information: " ^ show_builtin_type_info info)
in
(* Add the fields *)
let ctx =
List.fold_left
(fun ctx (fid, name) ->
- ctx_add def.span (FieldId (TAdtId def.def_id, fid)) name ctx)
+ ctx_add def.item_meta.span
+ (FieldId (TAdtId def.def_id, fid))
+ name ctx)
ctx field_names
in
(* Add the constructor name *)
- ctx_add def.span (StructId (TAdtId def.def_id)) cons_name ctx
+ ctx_add def.item_meta.span (StructId (TAdtId def.def_id)) cons_name
+ ctx
| Enum variants ->
let variant_names =
match info with
| None ->
VariantId.mapi
(fun variant_id (variant : variant) ->
- let name =
- ctx_compute_variant_name def.span ctx def.llbc_name
- variant.variant_name
- in
+ let name = ctx_compute_variant_name ctx def variant in
(* Add the type name prefix for Lean *)
let name =
if Config.backend () = Lean then
- let type_name =
- ctx_compute_type_name def.span ctx def.llbc_name
- in
+ let type_name = ctx_compute_type_decl_name ctx def in
type_name ^ "." ^ name
else name
in
@@ -847,11 +849,14 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
(variant_id, StringMap.find variant.variant_name variant_map))
variants
| _ ->
- craise __FILE__ __LINE__ def.span "Invalid builtin information"
+ craise __FILE__ __LINE__ def.item_meta.span
+ "Invalid builtin information"
in
List.fold_left
(fun ctx (vid, vname) ->
- ctx_add def.span (VariantId (TAdtId def.def_id, vid)) vname ctx)
+ ctx_add def.item_meta.span
+ (VariantId (TAdtId def.def_id, vid))
+ vname ctx)
ctx variant_names
| Opaque ->
(* Nothing to do *)
@@ -971,12 +976,10 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
let print_variant _variant_id (v : variant) =
(* We don't lookup the name, because it may have a prefix for the type
id (in the case of Lean) *)
- let cons_name =
- ctx_compute_variant_name def.span ctx def.llbc_name v.variant_name
- in
+ let cons_name = ctx_compute_variant_name ctx def v in
let fields = v.fields in
- extract_type_decl_variant def.span ctx fmt type_decl_group def_name
- type_params cg_params cons_name fields
+ extract_type_decl_variant def.item_meta.span ctx fmt type_decl_group
+ def_name type_params cg_params cons_name fields
in
(* Print the variants *)
let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in
@@ -1073,7 +1076,8 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(* If Coq: print the constructor name *)
(* TODO: remove superfluous test not is_rec below *)
if backend () = Coq && not is_rec then (
- F.pp_print_string fmt (ctx_get_struct def.span (TAdtId def.def_id) ctx);
+ F.pp_print_string fmt
+ (ctx_get_struct def.item_meta.span (TAdtId def.def_id) ctx);
F.pp_print_string fmt " ");
(match backend () with
| Lean -> ()
@@ -1088,7 +1092,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(* Print the fields *)
let print_field (field_id : FieldId.id) (f : field) : unit =
let field_name =
- ctx_get_field def.span (TAdtId def.def_id) field_id ctx
+ ctx_get_field def.item_meta.span (TAdtId def.def_id) field_id ctx
in
(* Open a box for the field *)
F.pp_open_box fmt ctx.indent_incr;
@@ -1096,7 +1100,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- extract_ty def.span ctx fmt type_decl_group false f.field_ty;
+ extract_ty def.item_meta.span ctx fmt type_decl_group false f.field_ty;
if backend () <> Lean then F.pp_print_string fmt ";";
(* Close the box for the field *)
F.pp_close_box fmt ()
@@ -1120,7 +1124,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
a group of mutually recursive types: we extract it as an inductive type *)
cassert __FILE__ __LINE__
(is_rec && (backend () = Coq || backend () = Lean))
- def.span
+ def.item_meta.span
"Constant generics are not supported yet when generating code for HOL4";
(* Small trick: in Lean we use namespaces, meaning we don't need to prefix
the constructor name with the name of the type at definition site,
@@ -1128,11 +1132,11 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
we generate `inductive Foo := | mk ... *)
let cons_name =
if backend () = Lean then "mk"
- else ctx_get_struct def.span (TAdtId def.def_id) ctx
+ else ctx_get_struct def.item_meta.span (TAdtId def.def_id) ctx
in
- let def_name = ctx_get_local_type def.span def.def_id ctx in
- extract_type_decl_variant def.span ctx fmt type_decl_group def_name
- type_params cg_params cons_name fields)
+ let def_name = ctx_get_local_type def.item_meta.span def.def_id ctx in
+ extract_type_decl_variant def.item_meta.span ctx fmt type_decl_group
+ def_name type_params cg_params cons_name fields)
in
()
@@ -1198,12 +1202,14 @@ let extract_trait_self_clause (insert_req_space : unit -> unit)
(params : string list) : unit =
insert_req_space ();
F.pp_print_string fmt "(";
- let self_clause = ctx_get_trait_self_clause trait_decl.span ctx in
+ let self_clause = ctx_get_trait_self_clause trait_decl.item_meta.span ctx in
F.pp_print_string fmt self_clause;
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- let trait_id = ctx_get_trait_decl trait_decl.span trait_decl.def_id ctx in
+ let trait_id =
+ ctx_get_trait_decl trait_decl.item_meta.span trait_decl.def_id ctx
+ in
F.pp_print_string fmt trait_id;
List.iter
(fun p ->
@@ -1352,11 +1358,13 @@ let extract_generic_params (span : Meta.span) (ctx : extraction_ctx)
dtype_params;
map
(fun (cg : const_generic_var) ->
- ctx_get_const_generic_var trait_decl.span cg.index ctx)
+ ctx_get_const_generic_var trait_decl.item_meta.span cg.index
+ ctx)
dcgs;
map
(fun c ->
- ctx_get_local_trait_clause trait_decl.span c.clause_id ctx)
+ ctx_get_local_trait_clause trait_decl.item_meta.span
+ c.clause_id ctx)
dtrait_clauses;
]
in
@@ -1375,7 +1383,9 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl)
(extract_body : bool) : unit =
(* Sanity check *)
- sanity_check __FILE__ __LINE__ (extract_body || backend () <> HOL4) def.span;
+ sanity_check __FILE__ __LINE__
+ (extract_body || backend () <> HOL4)
+ def.item_meta.span;
let is_tuple_struct =
TypesUtils.type_decl_from_decl_id_is_tuple_struct
ctx.trans_ctx.type_ctx.type_infos def.def_id
@@ -1403,12 +1413,12 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
let is_opaque_coq = backend () = Coq && is_opaque in
let use_forall = is_opaque_coq && def.generics <> empty_generic_params in
(* Retrieve the definition name *)
- let def_name = ctx_get_local_type def.span def.def_id ctx in
+ let def_name = ctx_get_local_type def.item_meta.span def.def_id ctx in
(* Add the type and const generic params - note that we need those bindings only for the
* body translation (they are not top-level) *)
let ctx_body, type_params, cg_params, trait_clauses =
- ctx_add_generic_params def.span def.llbc_name def.llbc_generics def.generics
- ctx
+ ctx_add_generic_params def.item_meta.span def.llbc_name def.llbc_generics
+ def.generics ctx
in
(* Add a break before *)
if backend () <> HOL4 || not (decl_is_first_from_group kind) then
@@ -1421,7 +1431,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
in
extract_comment_with_raw_span ctx fmt
[ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]
- name def.span.span);
+ name def.item_meta.span.span);
F.pp_print_break fmt 0 0;
(* Open a box for the definition, so that whenever possible it gets printed on
* one line. Note however that in the case of Lean line breaks are important
@@ -1441,7 +1451,7 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ())
else ();
(* > "type TYPE_NAME" *)
- let qualif = type_decl_kind_to_qualif def.span kind type_kind in
+ let qualif = type_decl_kind_to_qualif def.item_meta.span kind type_kind in
(match qualif with
| Some qualif -> F.pp_print_string fmt (qualif ^ " " ^ def_name)
| None -> F.pp_print_string fmt def_name);
@@ -1449,12 +1459,12 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
support trait clauses *)
cassert __FILE__ __LINE__
((cg_params = [] && trait_clauses = []) || backend () <> HOL4)
- def.span
+ def.item_meta.span
"Constant generics and type definitions with trait clauses are not \
supported yet when generating code for HOL4";
(* Print the generic parameters *)
- extract_generic_params def.span ctx_body fmt type_decl_group ~use_forall
- def.generics type_params cg_params trait_clauses;
+ extract_generic_params def.item_meta.span ctx_body fmt type_decl_group
+ ~use_forall def.generics type_params cg_params trait_clauses;
(* Print the "=" if we extract the body*)
if extract_body then (
F.pp_print_space fmt ();
@@ -1480,21 +1490,22 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt ":");
F.pp_print_space fmt ();
- F.pp_print_string fmt (type_keyword def.span));
+ F.pp_print_string fmt (type_keyword def.item_meta.span));
(* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *)
F.pp_close_box fmt ();
(if extract_body then
match def.kind with
| Struct fields ->
if is_tuple_struct then
- extract_type_decl_tuple_struct_body def.span ctx_body fmt fields
+ extract_type_decl_tuple_struct_body def.item_meta.span ctx_body fmt
+ fields
else
extract_type_decl_struct_body ctx_body fmt type_decl_group kind def
type_params cg_params fields
| Enum variants ->
extract_type_decl_enum_body ctx_body fmt type_decl_group def def_name
type_params cg_params variants
- | Opaque -> craise __FILE__ __LINE__ def.span "Unreachable");
+ | Opaque -> craise __FILE__ __LINE__ def.item_meta.span "Unreachable");
(* Add the definition end delimiter *)
if backend () = HOL4 && decl_is_not_last_from_group kind then (
F.pp_print_space fmt ();
@@ -1518,16 +1529,16 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
(def : type_decl) : unit =
(* Retrieve the definition name *)
- let def_name = ctx_get_local_type def.span def.def_id ctx in
+ let def_name = ctx_get_local_type def.item_meta.span def.def_id ctx in
(* Generic parameters are unsupported *)
cassert __FILE__ __LINE__
(def.generics.const_generics = [])
- def.span
+ def.item_meta.span
"Constant generics are not supported yet when generating code for HOL4";
(* Trait clauses on type definitions are unsupported *)
cassert __FILE__ __LINE__
(def.generics.trait_clauses = [])
- def.span
+ def.item_meta.span
"Types with trait clauses are not supported yet when generating code for \
HOL4";
(* Types *)
@@ -1550,9 +1561,11 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
let extract_type_decl_hol4_empty_record (ctx : extraction_ctx)
(fmt : F.formatter) (def : type_decl) : unit =
(* Retrieve the definition name *)
- let def_name = ctx_get_local_type def.span def.def_id ctx in
+ let def_name = ctx_get_local_type def.item_meta.span def.def_id ctx in
(* Sanity check *)
- sanity_check __FILE__ __LINE__ (def.generics = empty_generic_params) def.span;
+ sanity_check __FILE__ __LINE__
+ (def.generics = empty_generic_params)
+ def.item_meta.span;
(* Generate the declaration *)
F.pp_print_space fmt ();
F.pp_print_string fmt ("Type " ^ def_name ^ " = “: unit”");
@@ -1628,7 +1641,7 @@ let extract_coq_arguments_instruction (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
(kind : decl_kind) (decl : type_decl) : unit =
- sanity_check __FILE__ __LINE__ (backend () = Coq) decl.span;
+ sanity_check __FILE__ __LINE__ (backend () = Coq) decl.item_meta.span;
(* Generating the [Arguments] instructions is useful only if there are parameters *)
let num_params =
List.length decl.generics.types
@@ -1643,14 +1656,16 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
| Struct fields ->
let adt_id = TAdtId decl.def_id in
(* Generate the instruction for the record constructor *)
- let cons_name = ctx_get_struct decl.span adt_id ctx in
+ let cons_name = ctx_get_struct decl.item_meta.span adt_id ctx in
extract_coq_arguments_instruction ctx fmt cons_name num_params;
(* Generate the instruction for the record projectors, if there are *)
let is_rec = decl_is_from_rec_group kind in
if not is_rec then
FieldId.iteri
(fun fid _ ->
- let cons_name = ctx_get_field decl.span adt_id fid ctx in
+ let cons_name =
+ ctx_get_field decl.item_meta.span adt_id fid ctx
+ in
extract_coq_arguments_instruction ctx fmt cons_name num_params)
fields;
(* Add breaks to insert new lines between definitions *)
@@ -1660,7 +1675,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
VariantId.iteri
(fun vid (_ : variant) ->
let cons_name =
- ctx_get_variant decl.span (TAdtId decl.def_id) vid ctx
+ ctx_get_variant decl.item_meta.span (TAdtId decl.def_id) vid ctx
in
extract_coq_arguments_instruction ctx fmt cons_name num_params)
variants;
@@ -1679,7 +1694,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
(fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
sanity_check __FILE__ __LINE__
(backend () = Coq || backend () = Lean)
- decl.span;
+ decl.item_meta.span;
match decl.kind with
| Opaque | Enum _ -> ()
| Struct fields ->
@@ -1688,18 +1703,24 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
if is_rec then
(* Add the type params *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params decl.span decl.llbc_name decl.llbc_generics
- decl.generics ctx
+ ctx_add_generic_params decl.item_meta.span decl.llbc_name
+ decl.llbc_generics decl.generics ctx
in
(* Record_var will be the ADT argument to the projector *)
- let ctx, record_var = ctx_add_var decl.span "x" (VarId.of_int 0) ctx in
+ let ctx, record_var =
+ ctx_add_var decl.item_meta.span "x" (VarId.of_int 0) ctx
+ in
(* Field_var will be the variable in the constructor that is returned by the projector *)
- let ctx, field_var = ctx_add_var decl.span "x" (VarId.of_int 1) ctx in
+ let ctx, field_var =
+ ctx_add_var decl.item_meta.span "x" (VarId.of_int 1) ctx
+ in
(* Name of the ADT *)
- let def_name = ctx_get_local_type decl.span decl.def_id ctx in
+ let def_name = ctx_get_local_type decl.item_meta.span decl.def_id ctx in
(* Name of the ADT constructor. As we are in the struct case, we only have
one constructor *)
- let cons_name = ctx_get_struct decl.span (TAdtId decl.def_id) ctx in
+ let cons_name =
+ ctx_get_struct decl.item_meta.span (TAdtId decl.def_id) ctx
+ in
let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
F.pp_print_space fmt ();
@@ -1725,14 +1746,14 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
(match backend () with
| Lean -> F.pp_print_string fmt "def"
| Coq -> F.pp_print_string fmt "Definition"
- | _ -> internal_error __FILE__ __LINE__ decl.span);
+ | _ -> internal_error __FILE__ __LINE__ decl.item_meta.span);
F.pp_print_space fmt ();
(* Print the function name. In Lean, the syntax ADT.proj will
allow us to call x.proj for any x of type ADT. In Coq,
we will have to introduce a notation for the projector. *)
let field_name =
- ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx
+ ctx_get_field decl.item_meta.span (TAdtId decl.def_id) field_id ctx
in
if backend () = Lean then (
F.pp_print_string fmt def_name;
@@ -1741,8 +1762,9 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
(* Print the generics *)
let as_implicits = true in
- extract_generic_params decl.span ctx fmt TypeDeclId.Set.empty
- ~as_implicits decl.generics type_params cg_params trait_clauses;
+ extract_generic_params decl.item_meta.span ctx fmt
+ TypeDeclId.Set.empty ~as_implicits decl.generics type_params
+ cg_params trait_clauses;
(* Print the record parameter as "(x : ADT)" *)
F.pp_print_space fmt ();
@@ -1826,12 +1848,12 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
(* Inner box for the projector definition *)
F.pp_open_hovbox fmt ctx.indent_incr;
let ctx, record_var =
- ctx_add_var decl.span "x" (VarId.of_int 0) ctx
+ ctx_add_var decl.item_meta.span "x" (VarId.of_int 0) ctx
in
F.pp_print_string fmt "Notation";
F.pp_print_space fmt ();
let field_name =
- ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx
+ ctx_get_field decl.item_meta.span (TAdtId decl.def_id) field_id ctx
in
F.pp_print_string fmt ("\"" ^ record_var ^ " .(" ^ field_name ^ ")\"");
F.pp_print_space fmt ();
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 1bf9196a..d78b9081 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -97,10 +97,11 @@ let () =
( "-backward-no-state-update",
Arg.Set backward_no_state_update,
" Forbid backward functions from updating the state" );
- ( "-template-clauses",
- Arg.Set extract_template_decreases_clauses,
- " Generate templates for the required decreases clauses/termination \
- measures, in a dedicated file. Implies -decreases-clauses" );
+ ( "-no-template-clauses",
+ Arg.Clear extract_template_decreases_clauses,
+ " Do not generate templates for the required decreases \
+ clauses/termination measures, in a dedicated file, if you also put \
+ the option -decreases-clauses" );
( "-split-files",
Arg.Set split_files,
" Split the definitions between different files for types, functions, \
@@ -180,10 +181,12 @@ let () =
if !print_llbc then main_log#set_level EL.Debug;
- (* Sanity check (now that the arguments are parsed!): -template-clauses ==> decrease-clauses *)
+ (* Sanity check (now that the arguments are parsed!) *)
check_arg_implies
- !extract_template_decreases_clauses
- "-template-clauses" !extract_decreases_clauses "-decreases-clauses";
+ (not !extract_template_decreases_clauses)
+ "-no-template-clauses" !extract_decreases_clauses "-decreases-clauses";
+ if not !extract_decreases_clauses then
+ extract_template_decreases_clauses := false;
(* Sanity check: -backward-no-state-update ==> -state *)
check_arg_implies !backward_no_state_update "-backward-no-state-update"
!use_state "-state";
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index b1b42207..fe7c1234 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -798,7 +798,7 @@ let fun_decl_to_string (env : fmt_env) (def : fun_decl) : string =
else " fun " ^ String.concat " " inputs ^ " ->\n" ^ indent
in
let body =
- texpression_to_string ~spandata:(Some def.span) env inside indent indent
- body.body
+ texpression_to_string ~spandata:(Some def.item_meta.span) env inside
+ indent indent body.body
in
"let " ^ name ^ " :\n " ^ signature ^ " =\n" ^ inputs ^ body
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index f7445575..2ff8c272 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1,4 +1,5 @@
open Identifiers
+open Meta
module T = Types
module V = Values
module E = Expressions
@@ -351,8 +352,19 @@ and trait_instance_id =
polymorphic = false;
}]
-type field = { field_name : string option; field_ty : ty } [@@deriving show]
-type variant = { variant_name : string; fields : field list } [@@deriving show]
+type field = {
+ field_name : string option;
+ field_ty : ty;
+ item_meta : item_meta;
+}
+[@@deriving show]
+
+type variant = {
+ variant_name : string;
+ fields : field list;
+ item_meta : item_meta;
+}
+[@@deriving show]
type type_decl_kind = Struct of field list | Enum of variant list | Opaque
[@@deriving show]
@@ -393,7 +405,7 @@ type type_decl = {
the name used at extraction time will be derived from the
llbc_name.
*)
- span : span;
+ item_meta : item_meta;
generics : generic_params;
llbc_generics : Types.generic_params;
(** We use the LLBC generics to generate "pretty" names, for instance
@@ -1086,7 +1098,7 @@ type backend_attributes = {
type fun_decl = {
def_id : FunDeclId.id;
is_local : bool;
- span : span;
+ item_meta : item_meta;
kind : item_kind;
backend_attributes : backend_attributes;
num_loops : int;
@@ -1133,7 +1145,7 @@ type trait_decl = {
is_local : bool;
llbc_name : llbc_name;
name : string;
- span : span;
+ item_meta : item_meta;
generics : generic_params;
llbc_generics : Types.generic_params;
(** We use the LLBC generics to generate "pretty" names, for instance
@@ -1156,7 +1168,7 @@ type trait_impl = {
is_local : bool;
llbc_name : llbc_name;
name : string;
- span : span;
+ item_meta : item_meta;
impl_trait : trait_decl_ref;
llbc_impl_trait : Types.trait_decl_ref;
(** Same remark as for {!field:llbc_generics}. *)
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 8b95f729..543b2bee 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -224,7 +224,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
let register_var (ctx : pn_ctx) (v : var) : pn_ctx =
sanity_check __FILE__ __LINE__
(not (VarId.Map.mem v.id ctx.pure_vars))
- def.span;
+ def.item_meta.span;
match v.basename with
| None -> ctx
| Some name ->
@@ -614,7 +614,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
| App _ -> (
let app, args = destruct_apps e in
let ignore () =
- mk_apps def.span
+ mk_apps def.item_meta.span
(self#visit_texpression env app)
(List.map (self#visit_texpression env) args)
in
@@ -759,7 +759,7 @@ let simplify_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
else if variant_id = result_fail_id then
(* Fail case *)
self#visit_expression env rv.e
- else craise __FILE__ __LINE__ def.span "Unexpected"
+ else craise __FILE__ __LINE__ def.item_meta.span "Unexpected"
| App _ ->
(* This might be the tuple case *)
if not monadic then
@@ -914,7 +914,7 @@ let inline_useless_var_reassignments (ctx : trans_ctx) ~(inline_named : bool)
} ) ->
(* Second case: we deconstruct a structure with one field that we will
extract as tuple. *)
- let adt_id, _ = PureUtils.ty_as_adt def.span re.ty in
+ let adt_id, _ = PureUtils.ty_as_adt def.item_meta.span re.ty in
(* Update the rhs (we may perform substitutions inside, and it is
* better to do them *before* we inline it *)
let re = self#visit_texpression env re in
@@ -1152,7 +1152,7 @@ let simplify_let_then_ok _ctx (def : fun_decl) =
| Some e ->
if match_pattern_and_expr lv e then
(* We need to wrap the right-value in a ret *)
- (mk_result_ok_texpression def.span rv).e
+ (mk_result_ok_texpression def.item_meta.span rv).e
else not_simpl_e
| None ->
if match_pattern_and_expr lv next_e then rv.e else not_simpl_e
@@ -1203,13 +1203,14 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
let fields =
match adt_decl.kind with
| Enum _ | Alias _ | Opaque ->
- craise __FILE__ __LINE__ def.span "Unreachable"
+ craise __FILE__ __LINE__ def.item_meta.span "Unreachable"
| Struct fields -> fields
in
let num_fields = List.length fields in
(* In order to simplify, there must be as many arguments as
* there are fields *)
- sanity_check __FILE__ __LINE__ (num_fields > 0) def.span;
+ sanity_check __FILE__ __LINE__ (num_fields > 0)
+ def.item_meta.span;
if num_fields = List.length args then
(* We now need to check that all the arguments are of the form:
* [x.field] for some variable [x], and where the projection
@@ -1249,7 +1250,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
(List.for_all
(fun (generics1, _) -> generics1 = generics)
args)
- def.span;
+ def.item_meta.span;
{ e with e = Var x })
else super#visit_texpression env e
else super#visit_texpression env e
@@ -1406,7 +1407,7 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
in
sanity_check __FILE__ __LINE__
(fun_sig_info_is_wf loop_fwd_sig_info)
- def.span;
+ def.item_meta.span;
let inputs_tys =
let fuel = if !Config.use_fuel then [ mk_fuel_ty ] else [] in
@@ -1449,7 +1450,7 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
sanity_check __FILE__ __LINE__
(loop_fwd_effect_info.stateful
= Option.is_some loop.input_state)
- def.span;
+ def.item_meta.span;
match loop.input_state with
| None -> ([], [])
| Some input_state ->
@@ -1486,17 +1487,20 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
match fuel_vars with
| None -> loop.loop_body
| Some (fuel0, fuel) ->
- SymbolicToPure.wrap_in_match_fuel def.span fuel0 fuel
- loop.loop_body
+ SymbolicToPure.wrap_in_match_fuel def.item_meta.span fuel0
+ fuel loop.loop_body
in
let loop_body = { inputs; inputs_lvs; body = loop_body } in
+ (* We retrieve the meta information from the parent function
+ *but* replace its span with the span of the loop *)
+ let item_meta = { def.item_meta with span = loop.span } in
let loop_def : fun_decl =
{
def_id = def.def_id;
is_local = def.is_local;
- span = loop.span;
+ item_meta;
kind = def.kind;
backend_attributes = def.backend_attributes;
num_loops;
@@ -1581,9 +1585,10 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
match aid with
| BoxNew ->
let arg, args = Collections.List.pop args in
- mk_apps def.span arg args
+ mk_apps def.item_meta.span arg args
| BoxFree ->
- sanity_check __FILE__ __LINE__ (args = []) def.span;
+ sanity_check __FILE__ __LINE__ (args = [])
+ def.item_meta.span;
mk_unit_rvalue
| SliceIndexShared | SliceIndexMut | ArrayIndexShared
| ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
@@ -1777,8 +1782,10 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
*)
(* TODO: this information should be computed in SymbolicToPure and
* store in an enum ("monadic" should be an enum, not a bool). *)
- let re_ty = Option.get (opt_destruct_result def.span re.ty) in
- sanity_check __FILE__ __LINE__ (lv.ty = re_ty) def.span;
+ let re_ty =
+ Option.get (opt_destruct_result def.item_meta.span re.ty)
+ in
+ sanity_check __FILE__ __LINE__ (lv.ty = re_ty) def.item_meta.span;
let err_vid = fresh_id () in
let err_var : var =
{
@@ -1790,7 +1797,9 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
let err_pat = mk_typed_pattern_from_var err_var None in
let fail_pat = mk_result_fail_pattern err_pat.value lv.ty in
let err_v = mk_texpression_from_var err_var in
- let fail_value = mk_result_fail_texpression def.span err_v e.ty in
+ let fail_value =
+ mk_result_fail_texpression def.item_meta.span err_v e.ty
+ in
let fail_branch = { pat = fail_pat; branch = fail_value } in
let success_pat = mk_result_ok_pattern lv in
let success_branch = { pat = success_pat; branch = e } in
@@ -2031,7 +2040,9 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
^ String.concat ", " (List.map (var_to_string ctx) inputs_prefix)
^ "\n"));
let inputs_set = VarId.Set.of_list (List.map var_get_id inputs_prefix) in
- sanity_check __FILE__ __LINE__ (Option.is_some decl.loop_id) decl.span;
+ sanity_check __FILE__ __LINE__
+ (Option.is_some decl.loop_id)
+ decl.item_meta.span;
let fun_id = (E.FRegular decl.def_id, decl.loop_id) in
@@ -2183,7 +2194,9 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
in
let fwd_info = { fwd_info; effect_info; ignore_output } in
- sanity_check __FILE__ __LINE__ (fun_sig_info_is_wf fwd_info) decl.span;
+ sanity_check __FILE__ __LINE__
+ (fun_sig_info_is_wf fwd_info)
+ decl.item_meta.span;
let signature =
{
generics;
@@ -2249,17 +2262,17 @@ let filter_loop_inputs (ctx : trans_ctx) (transl : pure_fun_translation list) :
in
(* Rebuild *)
- mk_apps decl.span e_app args)
+ mk_apps decl.item_meta.span e_app args)
| _ ->
let e_app = self#visit_texpression env e_app in
let args =
List.map (self#visit_texpression env) args
in
- mk_apps decl.span e_app args)
+ mk_apps decl.item_meta.span e_app args)
| _ ->
let e_app = self#visit_texpression env e_app in
let args = List.map (self#visit_texpression env) args in
- mk_apps decl.span e_app args)
+ mk_apps decl.item_meta.span e_app args)
| _ -> super#visit_texpression env e
end
in
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index fe5d3414..5a85628c 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -692,7 +692,7 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool =
is_local = _;
name = _;
llbc_name = _;
- span = _;
+ item_meta = _;
generics = _;
llbc_generics = _;
preds = _;
@@ -714,7 +714,7 @@ let trait_impl_is_empty (trait_impl : trait_impl) : bool =
is_local = _;
name = _;
llbc_name = _;
- span = _;
+ item_meta = _;
impl_trait = _;
llbc_impl_trait = _;
generics = _;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index ad61ddd1..1b5da858 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -545,7 +545,8 @@ let translate_generic_params (span : Meta.span) (generics : T.generic_params) :
let translate_field (span : Meta.span) (f : T.field) : field =
let field_name = f.field_name in
let field_ty = translate_sty span f.field_ty in
- { field_name; field_ty }
+ let item_meta = f.item_meta in
+ { field_name; field_ty; item_meta }
let translate_fields (span : Meta.span) (fl : T.field list) : field list =
List.map (translate_field span) fl
@@ -553,7 +554,8 @@ let translate_fields (span : Meta.span) (fl : T.field list) : field list =
let translate_variant (span : Meta.span) (v : T.variant) : variant =
let variant_name = v.variant_name in
let fields = translate_fields span v.fields in
- { variant_name; fields }
+ let item_meta = v.item_meta in
+ { variant_name; fields; item_meta }
let translate_variants (span : Meta.span) (vl : T.variant list) : variant list =
List.map (translate_variant span) vl
@@ -597,13 +599,13 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
let kind = translate_type_decl_kind def.item_meta.span def.T.kind in
let preds = translate_predicates def.item_meta.span def.preds in
let is_local = def.is_local in
- let span = def.item_meta.span in
+ let item_meta = def.item_meta in
{
def_id;
is_local;
llbc_name;
name;
- span;
+ item_meta;
generics;
llbc_generics = def.generics;
kind;
@@ -3899,7 +3901,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
{
def_id;
is_local = def.is_local;
- span = def.item_meta.span;
+ item_meta = def.item_meta;
kind = def.kind;
backend_attributes;
num_loops;
@@ -3988,7 +3990,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
is_local;
llbc_name;
name;
- span = item_meta.span;
+ item_meta;
generics;
llbc_generics;
preds;
@@ -4057,7 +4059,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
is_local;
llbc_name;
name;
- span = item_meta.span;
+ item_meta;
impl_trait;
llbc_impl_trait;
generics;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 10:47:24 +0000