summaryrefslogtreecommitdiff
path: root/compiler/Extract.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Extract.ml')
-rw-r--r--compiler/Extract.ml572
1 files changed, 328 insertions, 244 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index aa097a4f..1f9c9117 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -7,6 +7,7 @@ open Pure
open PureUtils
open TranslateCore
open Config
+open Errors
include ExtractTypes
(** Compute the names for all the pure functions generated from a rust function.
@@ -45,7 +46,7 @@ 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 (FunId (FromLlbc fun_id)) fun_info.extract_name ctx
+ ctx_add f.meta (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
@@ -59,7 +60,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
(* Add the decreases proof for Lean only *)
match !Config.backend with
| Coq | FStar -> ctx
- | HOL4 -> raise (Failure "Unexpected")
+ | HOL4 -> craise __FILE__ __LINE__ def.meta "Unexpected"
| Lean -> ctx_add_decreases_proof def ctx
else ctx
in
@@ -89,7 +90,7 @@ let extract_global_decl_register_names (ctx : extraction_ctx)
TODO: we don't need something very generic anymore (some definitions used
to be polymorphic).
*)
-let extract_adt_g_value
+let extract_adt_g_value (meta : Meta.meta)
(extract_value : extraction_ctx -> bool -> 'v -> extraction_ctx)
(fmt : F.formatter) (ctx : extraction_ctx) (is_single_pat : bool)
(inside : bool) (variant_id : VariantId.id option) (field_values : 'v list)
@@ -127,8 +128,12 @@ let extract_adt_g_value
| TAdt (TTuple, generics) ->
(* Tuple *)
(* For now, we only support fully applied tuple constructors *)
- assert (List.length generics.types = List.length field_values);
- assert (generics.const_generics = [] && generics.trait_refs = []);
+ cassert __FILE__ __LINE__
+ (List.length generics.types = List.length field_values)
+ meta "Only fully applied tuple constructors are currently supported";
+ cassert __FILE__ __LINE__
+ (generics.const_generics = [] && generics.trait_refs = [])
+ meta "Only fully applied tuple constructors are currently supported";
extract_as_tuple ()
| TAdt (adt_id, _) ->
(* "Regular" ADT *)
@@ -167,8 +172,8 @@ let extract_adt_g_value
*)
let cons =
match variant_id with
- | Some vid -> ctx_get_variant adt_id vid ctx
- | None -> ctx_get_struct adt_id ctx
+ | Some vid -> ctx_get_variant meta adt_id vid ctx
+ | None -> ctx_get_struct meta adt_id ctx
in
let use_parentheses = inside && field_values <> [] in
if use_parentheses then F.pp_print_string fmt "(";
@@ -182,18 +187,18 @@ let extract_adt_g_value
in
if use_parentheses then F.pp_print_string fmt ")";
ctx
- | _ -> raise (Failure "Inconsistent typed value")
+ | _ -> craise __FILE__ __LINE__ meta "Inconsistent typed value"
(* Extract globals in the same way as variables *)
-let extract_global (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
- (id : A.GlobalDeclId.id) (generics : generic_args) : unit =
+let extract_global (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
+ (inside : bool) (id : A.GlobalDeclId.id) (generics : generic_args) : unit =
let use_brackets = inside && generics <> empty_generic_args in
F.pp_open_hvbox fmt ctx.indent_incr;
if use_brackets then F.pp_print_string fmt "(";
(* Extract the global name *)
- F.pp_print_string fmt (ctx_get_global id ctx);
+ F.pp_print_string fmt (ctx_get_global meta id ctx);
(* Extract the generics *)
- extract_generic_args ctx fmt TypeDeclId.Set.empty generics;
+ extract_generic_args meta ctx fmt TypeDeclId.Set.empty generics;
if use_brackets then F.pp_print_string fmt ")";
F.pp_close_box fmt ()
@@ -231,19 +236,19 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
As a pattern can introduce new variables, we return an extraction context
updated with new bindings.
*)
-let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
- (is_let : bool) (inside : bool) ?(with_type = false) (v : typed_pattern) :
- extraction_ctx =
+let rec extract_typed_pattern (meta : Meta.meta) (ctx : extraction_ctx)
+ (fmt : F.formatter) (is_let : bool) (inside : bool) ?(with_type = false)
+ (v : typed_pattern) : extraction_ctx =
if with_type then F.pp_print_string fmt "(";
let inside = inside && not with_type in
let ctx =
match v.value with
| PatConstant cv ->
- extract_literal fmt inside cv;
+ extract_literal meta fmt inside cv;
ctx
| PatVar (v, _) ->
- let vname = ctx_compute_var_basename ctx v.basename v.ty in
- let ctx, vname = ctx_add_var vname v.id ctx in
+ let vname = ctx_compute_var_basename meta ctx v.basename v.ty in
+ let ctx, vname = ctx_add_var meta vname v.id ctx in
F.pp_print_string fmt vname;
ctx
| PatDummy ->
@@ -251,23 +256,23 @@ let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
ctx
| PatAdt av ->
let extract_value ctx inside v =
- extract_typed_pattern ctx fmt is_let inside v
+ extract_typed_pattern meta ctx fmt is_let inside v
in
- extract_adt_g_value extract_value fmt ctx is_let inside av.variant_id
- av.field_values v.ty
+ extract_adt_g_value meta extract_value fmt ctx is_let inside
+ av.variant_id av.field_values v.ty
in
if with_type then (
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- extract_ty ctx fmt TypeDeclId.Set.empty false v.ty;
+ extract_ty meta ctx fmt TypeDeclId.Set.empty false v.ty;
F.pp_print_string fmt ")");
ctx
(** Return true if we need to wrap a succession of let-bindings in a [do ...]
block (because some of them are monadic) *)
-let lets_require_wrap_in_do (lets : (bool * typed_pattern * texpression) list) :
- bool =
+let lets_require_wrap_in_do (meta : Meta.meta)
+ (lets : (bool * typed_pattern * texpression) list) : bool =
match !backend with
| Lean ->
(* For Lean, we wrap in a block iff at least one of the let-bindings is monadic *)
@@ -275,7 +280,10 @@ let lets_require_wrap_in_do (lets : (bool * typed_pattern * texpression) list) :
| HOL4 ->
(* HOL4 is similar to HOL4, but we add a sanity check *)
let wrap_in_do = List.exists (fun (m, _, _) -> m) lets in
- if wrap_in_do then assert (List.for_all (fun (m, _, _) -> m) lets);
+ if wrap_in_do then
+ sanity_check __FILE__ __LINE__
+ (List.for_all (fun (m, _, _) -> m) lets)
+ meta;
wrap_in_do
| FStar | Coq -> false
@@ -289,38 +297,38 @@ let lets_require_wrap_in_do (lets : (bool * typed_pattern * texpression) list) :
- application argument: [f (exp)]
- match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
*)
-let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
- (inside : bool) (e : texpression) : unit =
+let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx)
+ (fmt : F.formatter) (inside : bool) (e : texpression) : unit =
match e.e with
| Var var_id ->
- let var_name = ctx_get_var var_id ctx in
+ let var_name = ctx_get_var meta var_id ctx in
F.pp_print_string fmt var_name
| CVar var_id ->
- let var_name = ctx_get_const_generic_var var_id ctx in
+ let var_name = ctx_get_const_generic_var meta var_id ctx in
F.pp_print_string fmt var_name
- | Const cv -> extract_literal fmt inside cv
+ | Const cv -> extract_literal meta fmt inside cv
| App _ ->
let app, args = destruct_apps e in
- extract_App ctx fmt inside app args
+ extract_App meta ctx fmt inside app args
| Lambda _ ->
let xl, e = destruct_lambdas e in
- extract_Lambda ctx fmt inside xl e
+ extract_Lambda (meta : Meta.meta) ctx fmt inside xl e
| Qualif _ ->
(* We use the app case *)
- extract_App ctx fmt inside e []
- | Let (_, _, _, _) -> extract_lets ctx fmt inside e
- | Switch (scrut, body) -> extract_Switch ctx fmt inside scrut body
- | Meta (_, e) -> extract_texpression ctx fmt inside e
- | StructUpdate supd -> extract_StructUpdate ctx fmt inside e.ty supd
+ extract_App meta ctx fmt inside e []
+ | Let (_, _, _, _) -> extract_lets meta ctx fmt inside e
+ | Switch (scrut, body) -> extract_Switch meta ctx fmt inside scrut body
+ | Meta (_, e) -> extract_texpression meta ctx fmt inside e
+ | StructUpdate supd -> extract_StructUpdate meta ctx fmt inside e.ty supd
| Loop _ ->
(* The loop nodes should have been eliminated in {!PureMicroPasses} *)
- raise (Failure "Unreachable")
+ craise __FILE__ __LINE__ meta "Unreachable"
(* Extract an application *or* a top-level qualif (function extraction has
* to handle top-level qualifiers, so it seemed more natural to merge the
* two cases) *)
-and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
- (app : texpression) (args : texpression list) : unit =
+and extract_App (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
+ (inside : bool) (app : texpression) (args : texpression list) : unit =
(* We don't do the same thing if the app is a top-level identifier (function,
* ADT constructor...) or a "regular" expression *)
match app.e with
@@ -328,18 +336,19 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(* Top-level qualifier *)
match qualif.id with
| FunOrOp fun_id ->
- extract_function_call ctx fmt inside fun_id qualif.generics args
+ extract_function_call meta ctx fmt inside fun_id qualif.generics args
| Global global_id ->
assert (args = []);
- extract_global ctx fmt inside global_id qualif.generics
+ extract_global meta ctx fmt inside global_id qualif.generics
| AdtCons adt_cons_id ->
- extract_adt_cons ctx fmt inside adt_cons_id qualif.generics args
+ extract_adt_cons meta ctx fmt inside adt_cons_id qualif.generics args
| Proj proj ->
- extract_field_projector ctx fmt inside app proj qualif.generics args
+ extract_field_projector meta ctx fmt inside app proj qualif.generics
+ args
| TraitConst (trait_ref, const_name) ->
- extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref;
+ extract_trait_ref meta ctx fmt TypeDeclId.Set.empty true trait_ref;
let name =
- ctx_get_trait_const trait_ref.trait_decl_ref.trait_decl_id
+ ctx_get_trait_const meta trait_ref.trait_decl_ref.trait_decl_id
const_name ctx
in
let add_brackets (s : string) =
@@ -354,12 +363,12 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the app expression *)
let app_inside = (inside && args = []) || args <> [] in
- extract_texpression ctx fmt app_inside app;
+ extract_texpression meta ctx fmt app_inside app;
(* Print the arguments *)
List.iter
(fun ve ->
F.pp_print_space fmt ();
- extract_texpression ctx fmt true ve)
+ extract_texpression meta ctx fmt true ve)
args;
(* Close the box for the application *)
F.pp_close_box fmt ();
@@ -367,20 +376,20 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
if inside then F.pp_print_string fmt ")"
(** Subcase of the app case: function call *)
-and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
- (inside : bool) (fid : fun_or_op_id) (generics : generic_args)
- (args : texpression list) : unit =
+and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx)
+ (fmt : F.formatter) (inside : bool) (fid : fun_or_op_id)
+ (generics : generic_args) (args : texpression list) : unit =
match (fid, args) with
| Unop unop, [ arg ] ->
(* A unop can have *at most* one argument (the result can't be a function!).
* Note that the way we generate the translation, we shouldn't get the
* case where we have no argument (all functions are fully instantiated,
* and no AST transformation introduces partial calls). *)
- extract_unop (extract_texpression ctx fmt) fmt inside unop arg
+ extract_unop meta (extract_texpression meta ctx fmt) fmt inside unop arg
| Binop (binop, int_ty), [ arg0; arg1 ] ->
(* Number of arguments: similar to unop *)
- extract_binop
- (extract_texpression ctx fmt)
+ extract_binop meta
+ (extract_texpression meta ctx fmt)
fmt inside binop int_ty arg0 arg1
| Fun fun_id, _ ->
if inside then F.pp_print_string fmt "(";
@@ -447,10 +456,11 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
if not method_id.is_provided then (
(* Required method *)
- assert (lp_id = None);
- extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref;
+ sanity_check __FILE__ __LINE__ (lp_id = None) trait_decl.meta;
+ extract_trait_ref trait_decl.meta ctx fmt TypeDeclId.Set.empty true
+ trait_ref;
let fun_name =
- ctx_get_trait_method trait_ref.trait_decl_ref.trait_decl_id
+ ctx_get_trait_method meta trait_ref.trait_decl_ref.trait_decl_id
method_name ctx
in
let add_brackets (s : string) =
@@ -461,7 +471,7 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
(* 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 fun_id ctx in
+ let fun_name = ctx_get_function trait_decl.meta fun_id ctx in
F.pp_print_string fmt fun_name;
(* Note that we do not need to print the generics for the trait
@@ -470,13 +480,16 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
Print the trait ref (to instantate the self clause) *)
F.pp_print_space fmt ();
- extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref
+ extract_trait_ref trait_decl.meta ctx fmt TypeDeclId.Set.empty true
+ trait_ref
| _ ->
- let fun_name = ctx_get_function fun_id ctx in
+ let fun_name = ctx_get_function meta fun_id ctx in
F.pp_print_string fmt fun_name);
(* Sanity check: HOL4 doesn't support const generics *)
- assert (generics.const_generics = [] || !backend <> HOL4);
+ sanity_check __FILE__ __LINE__
+ (generics.const_generics = [] || !backend <> HOL4)
+ meta;
(* Print the generics.
We might need to filter some of the type arguments, if the type
@@ -491,54 +504,53 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
in
(match types with
| Ok types ->
- extract_generic_args ctx fmt TypeDeclId.Set.empty
+ extract_generic_args meta ctx fmt TypeDeclId.Set.empty
{ generics with types }
| Error (types, err) ->
- extract_generic_args ctx fmt TypeDeclId.Set.empty
+ extract_generic_args meta ctx fmt TypeDeclId.Set.empty
{ generics with types };
- if !Config.fail_hard then raise (Failure err)
- else
- F.pp_print_string fmt
- "(\"ERROR: ill-formed builtin: invalid number of filtering \
- arguments\")");
+ save_error __FILE__ __LINE__ (Some meta) err;
+ F.pp_print_string fmt
+ "(\"ERROR: ill-formed builtin: invalid number of filtering \
+ arguments\")");
(* Print the arguments *)
List.iter
(fun ve ->
F.pp_print_space fmt ();
- extract_texpression ctx fmt true ve)
+ extract_texpression meta ctx fmt true ve)
args;
(* Close the box for the function call *)
F.pp_close_box fmt ();
(* Return *)
if inside then F.pp_print_string fmt ")"
| (Unop _ | Binop _), _ ->
- raise
- (Failure
- ("Unreachable:\n" ^ "Function: " ^ show_fun_or_op_id fid
- ^ ",\nNumber of arguments: "
- ^ string_of_int (List.length args)
- ^ ",\nArguments: "
- ^ String.concat " " (List.map show_texpression args)))
+ craise __FILE__ __LINE__ meta
+ ("Unreachable:\n" ^ "Function: " ^ show_fun_or_op_id fid
+ ^ ",\nNumber of arguments: "
+ ^ string_of_int (List.length args)
+ ^ ",\nArguments: "
+ ^ String.concat " " (List.map show_texpression args))
(** Subcase of the app case: ADT constructor *)
-and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
- (adt_cons : adt_cons_id) (generics : generic_args) (args : texpression list)
- : unit =
+and extract_adt_cons (meta : Meta.meta) (ctx : extraction_ctx)
+ (fmt : F.formatter) (inside : bool) (adt_cons : adt_cons_id)
+ (generics : generic_args) (args : texpression list) : unit =
let e_ty = TAdt (adt_cons.adt_id, generics) in
let is_single_pat = false in
let _ =
- extract_adt_g_value
+ extract_adt_g_value meta
(fun ctx inside e ->
- extract_texpression ctx fmt inside e;
+ extract_texpression meta ctx fmt inside e;
ctx)
fmt ctx is_single_pat inside adt_cons.variant_id args e_ty
in
()
(** Subcase of the app case: ADT field projector. *)
-and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
- (inside : bool) (original_app : texpression) (proj : projection)
- (_generics : generic_args) (args : texpression list) : unit =
+and extract_field_projector (meta : Meta.meta) (ctx : extraction_ctx)
+ (fmt : F.formatter) (inside : bool) (original_app : texpression)
+ (proj : projection) (_generics : generic_args) (args : texpression list) :
+ unit =
(* We isolate the first argument (if there is), in order to pretty print the
* projection ([x.field] instead of [MkAdt?.field x] *)
match args with
@@ -562,7 +574,7 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
match num_fields with Some len -> len = 1 | None -> false
in
if is_tuple_struct && has_one_field then
- extract_texpression ctx fmt inside arg
+ extract_texpression meta ctx fmt inside arg
else
(* Exactly one argument: pretty-print *)
let field_name =
@@ -613,12 +625,12 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
if field_id + 1 = Option.get num_fields then twos_prefix
else twos_prefix ^ ".1"
else "#" ^ string_of_int field_id
- else ctx_get_field proj.adt_id proj.field_id ctx
+ else ctx_get_field meta proj.adt_id proj.field_id ctx
in
(* Open a box *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Extract the expression *)
- extract_texpression ctx fmt true arg;
+ extract_texpression meta ctx fmt true arg;
(* We allow to break where the "." appears (except Lean, it's a syntax error) *)
if !backend <> Lean then F.pp_print_break fmt 0 0;
F.pp_print_string fmt ".";
@@ -631,26 +643,26 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
| arg :: args ->
(* Call extract_App again, but in such a way that the first argument is
* isolated *)
- extract_App ctx fmt inside (mk_app original_app arg) args
+ extract_App meta ctx fmt inside (mk_app meta original_app arg) args
| [] ->
(* No argument: shouldn't happen *)
- raise (Failure "Unreachable")
+ craise __FILE__ __LINE__ meta "Unreachable"
-and extract_Lambda (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
- (xl : typed_pattern list) (e : texpression) : unit =
+and extract_Lambda (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
+ (inside : bool) (xl : typed_pattern list) (e : texpression) : unit =
(* Open a box for the abs expression *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Open parentheses *)
if inside then F.pp_print_string fmt "(";
(* Print the lambda - note that there should always be at least one variable *)
- assert (xl <> []);
+ sanity_check __FILE__ __LINE__ (xl <> []) meta;
F.pp_print_string fmt "fun";
let with_type = !backend = Coq in
let ctx =
List.fold_left
(fun ctx x ->
F.pp_print_space fmt ();
- extract_typed_pattern ctx fmt true true ~with_type x)
+ extract_typed_pattern meta ctx fmt true true ~with_type x)
ctx xl
in
F.pp_print_space fmt ();
@@ -658,14 +670,14 @@ and extract_Lambda (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
else F.pp_print_string fmt "->";
F.pp_print_space fmt ();
(* Print the body *)
- extract_texpression ctx fmt false e;
+ extract_texpression meta ctx fmt false e;
(* Close parentheses *)
if inside then F.pp_print_string fmt ")";
(* Close the box for the abs expression *)
F.pp_close_box fmt ()
-and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
- (e : texpression) : unit =
+and extract_lets (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
+ (inside : bool) (e : texpression) : unit =
(* Destruct the lets.
Note that in the case of HOL4, we stop destructing the lets if at some point
@@ -690,7 +702,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
*)
let lets, next_e =
match !backend with
- | HOL4 -> destruct_lets_no_interleave e
+ | HOL4 -> destruct_lets_no_interleave meta e
| FStar | Coq | Lean -> destruct_lets e
in
(* Extract the let-bindings *)
@@ -711,16 +723,16 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
* TODO: cleanup
* *)
if monadic && (!backend = Coq || !backend = HOL4) then (
- let ctx = extract_typed_pattern ctx fmt true true lv in
+ let ctx = extract_typed_pattern meta ctx fmt true true lv in
F.pp_print_space fmt ();
let arrow =
match !backend with
| Coq | HOL4 -> "<-"
- | FStar | Lean -> raise (Failure "impossible")
+ | FStar | Lean -> craise __FILE__ __LINE__ meta "impossible"
in
F.pp_print_string fmt arrow;
F.pp_print_space fmt ();
- extract_texpression ctx fmt false re;
+ extract_texpression meta ctx fmt false re;
F.pp_print_string fmt ";";
ctx)
else (
@@ -737,7 +749,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
else (
F.pp_print_string fmt "let";
F.pp_print_space fmt ());
- let ctx = extract_typed_pattern ctx fmt true true lv in
+ let ctx = extract_typed_pattern meta ctx fmt true true lv in
F.pp_print_space fmt ();
let eq =
match !backend with
@@ -748,7 +760,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
in
F.pp_print_string fmt eq;
F.pp_print_space fmt ();
- extract_texpression ctx fmt false re;
+ extract_texpression meta ctx fmt false re;
(* End the let-binding *)
(match !backend with
| Lean ->
@@ -776,7 +788,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
if inside && !backend <> Lean then F.pp_print_string fmt "(";
(* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box
immediately *)
- let wrap_in_do_od = lets_require_wrap_in_do lets in
+ let wrap_in_do_od = lets_require_wrap_in_do meta lets in
if wrap_in_do_od then (
F.pp_print_string fmt "do";
F.pp_print_space fmt ());
@@ -788,7 +800,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(* Open a box for the next expression *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the next expression *)
- extract_texpression ctx fmt false next_e;
+ extract_texpression meta ctx fmt false next_e;
(* Close the box for the next expression *)
F.pp_close_box fmt ();
@@ -802,8 +814,8 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(* Close the box for the whole expression *)
F.pp_close_box fmt ()
-and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool)
- (scrut : texpression) (body : switch_body) : unit =
+and extract_Switch (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
+ (_inside : bool) (scrut : texpression) (body : switch_body) : unit =
(* Remark: we don't use the [inside] parameter because we extract matches in
a conservative manner: we always make sure they are parenthesized/delimited
with keywords such as [end] *)
@@ -821,8 +833,10 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool)
F.pp_print_string fmt "if";
if !backend = Lean && ctx.use_dep_ite then F.pp_print_string fmt " h:";
F.pp_print_space fmt ();
- let scrut_inside = PureUtils.texpression_requires_parentheses scrut in
- extract_texpression ctx fmt scrut_inside scrut;
+ let scrut_inside =
+ PureUtils.texpression_requires_parentheses meta scrut
+ in
+ extract_texpression meta ctx fmt scrut_inside scrut;
(* Close the box for the [if e] *)
F.pp_close_box fmt ();
@@ -835,7 +849,9 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool)
F.pp_open_hovbox fmt 0;
let then_or_else = if is_then then "then" else "else" in
F.pp_print_string fmt then_or_else;
- let parenth = PureUtils.texpression_requires_parentheses e_branch in
+ let parenth =
+ PureUtils.texpression_requires_parentheses meta e_branch
+ in
(* Open the parenthesized expression *)
let print_space_after_parenth =
if parenth then (
@@ -856,7 +872,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool)
(* Open a box for the branch *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the branch expression *)
- extract_texpression ctx fmt false e_branch;
+ extract_texpression meta ctx fmt false e_branch;
(* Close the box for the branch *)
F.pp_close_box fmt ();
(* Close the parenthesized expression *)
@@ -887,8 +903,10 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool)
in
F.pp_print_string fmt match_begin;
F.pp_print_space fmt ();
- let scrut_inside = PureUtils.texpression_requires_parentheses scrut in
- extract_texpression ctx fmt scrut_inside scrut;
+ let scrut_inside =
+ PureUtils.texpression_requires_parentheses meta scrut
+ in
+ extract_texpression meta ctx fmt scrut_inside scrut;
F.pp_print_space fmt ();
let match_scrut_end =
match !backend with FStar | Coq | Lean -> "with" | HOL4 -> "of"
@@ -907,7 +925,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool)
(* Print the pattern *)
F.pp_print_string fmt "|";
F.pp_print_space fmt ();
- let ctx = extract_typed_pattern ctx fmt false false br.pat in
+ let ctx = extract_typed_pattern meta ctx fmt false false br.pat in
F.pp_print_space fmt ();
let arrow =
match !backend with FStar -> "->" | Coq | Lean | HOL4 -> "=>"
@@ -919,7 +937,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool)
(* Open a box for the branch *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the branch itself *)
- extract_texpression ctx fmt false br.branch;
+ extract_texpression meta ctx fmt false br.branch;
(* Close the box for the branch *)
F.pp_close_box fmt ();
(* Close the box for the pattern+branch *)
@@ -938,11 +956,12 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool)
(* Close the box for the whole expression *)
F.pp_close_box fmt ()
-and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
- (inside : bool) (e_ty : ty) (supd : struct_update) : unit =
+and extract_StructUpdate (meta : Meta.meta) (ctx : extraction_ctx)
+ (fmt : F.formatter) (inside : bool) (e_ty : ty) (supd : struct_update) :
+ unit =
(* We can't update a subset of the fields in Coq (i.e., we can do
[{| x:= 3; y := 4 |}], but there is no syntax for [{| s with x := 3 |}]) *)
- assert (!backend <> Coq || supd.init = None);
+ sanity_check __FILE__ __LINE__ (!backend <> Coq || supd.init = None) meta;
(* In the case of HOL4, records with no fields are not supported and are
thus extracted to unit. We need to check that by looking up the definition *)
let extract_as_unit =
@@ -1007,7 +1026,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
if need_paren then F.pp_print_string fmt "(";
F.pp_open_hvbox fmt ctx.indent_incr;
if supd.init <> None then (
- let var_name = ctx_get_var (Option.get supd.init) ctx in
+ let var_name = ctx_get_var meta (Option.get supd.init) ctx in
F.pp_print_string fmt var_name;
F.pp_print_space fmt ();
F.pp_print_string fmt "with";
@@ -1026,12 +1045,12 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ())
(fun (fid, fe) ->
F.pp_open_hvbox fmt ctx.indent_incr;
- let f = ctx_get_field supd.struct_id fid ctx in
+ let f = ctx_get_field meta supd.struct_id fid ctx in
F.pp_print_string fmt f;
F.pp_print_string fmt (" " ^ assign);
F.pp_print_space fmt ();
F.pp_open_hvbox fmt ctx.indent_incr;
- extract_texpression ctx fmt true fe;
+ extract_texpression meta ctx fmt true fe;
F.pp_close_box fmt ();
F.pp_close_box fmt ())
supd.updates;
@@ -1050,16 +1069,16 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
(* Open the box for `Array.replicate T N [` *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the array constructor *)
- let cs = ctx_get_struct (TAssumed TArray) ctx in
+ let cs = ctx_get_struct meta (TAssumed TArray) ctx in
F.pp_print_string fmt cs;
(* Print the parameters *)
- let _, generics = ty_as_adt e_ty in
+ let _, generics = ty_as_adt meta e_ty in
let ty = Collections.List.to_cons_nil generics.types in
F.pp_print_space fmt ();
- extract_ty ctx fmt TypeDeclId.Set.empty true ty;
+ extract_ty meta ctx fmt TypeDeclId.Set.empty true ty;
let cg = Collections.List.to_cons_nil generics.const_generics in
F.pp_print_space fmt ();
- extract_const_generic ctx fmt true cg;
+ extract_const_generic meta ctx fmt true cg;
F.pp_print_space fmt ();
F.pp_print_string fmt "[";
(* Close the box for `Array.mk T N [` *)
@@ -1074,7 +1093,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
(fun () ->
F.pp_print_string fmt delimiter;
F.pp_print_space fmt ())
- (fun (_, fe) -> extract_texpression ctx fmt false fe)
+ (fun (_, fe) -> extract_texpression meta ctx fmt false fe)
supd.updates;
(* Close the boxes *)
F.pp_close_box fmt ();
@@ -1082,7 +1101,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "]";
if need_paren then F.pp_print_string fmt ")";
F.pp_close_box fmt ()
- | _ -> raise (Failure "Unreachable")
+ | _ -> craise __FILE__ __LINE__ meta "Unreachable"
(** A small utility to print the parameters of a function signature.
@@ -1116,7 +1135,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 ctx in
+ let ctx, _ = ctx_add_trait_self_clause def.meta ctx in
let ctx = { ctx with is_provided_method = true } in
(ctx, Some trait_decl)
| _ -> (ctx, None)
@@ -1124,15 +1143,15 @@ 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.llbc_name def.signature.llbc_generics
+ ctx_add_generic_params def.meta 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 ctx fmt TypeDeclId.Set.empty ~space ~trait_decl
- def.signature.generics type_params cg_params trait_clauses);
+ extract_generic_params def.meta 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 ();
(* The input parameters - note that doing this adds bindings to the context *)
@@ -1146,11 +1165,11 @@ 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 ctx fmt true false lv in
+ let ctx = extract_typed_pattern def.meta ctx fmt true false lv in
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- extract_ty ctx fmt TypeDeclId.Set.empty false lv.ty;
+ extract_ty def.meta 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 ();
@@ -1169,7 +1188,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 ctx fmt TypeDeclId.Set.empty inside ty;
+ extract_ty def.meta ctx fmt TypeDeclId.Set.empty inside ty;
F.pp_print_space fmt ();
extract_arrow fmt ();
F.pp_print_space fmt ()
@@ -1179,14 +1198,14 @@ 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 ctx fmt TypeDeclId.Set.empty false def.signature.output
+ extract_ty def.meta ctx fmt TypeDeclId.Set.empty false def.signature.output
-let assert_backend_supports_decreases_clauses () =
+let assert_backend_supports_decreases_clauses (meta : Meta.meta) =
match !backend with
| FStar | Lean -> ()
| _ ->
- raise
- (Failure "decreases clauses only supported for the Lean & F* backends")
+ craise __FILE__ __LINE__ meta
+ "Decreases clauses are only supported for the Lean and F* backends"
(** Extract a decreases clause function template body.
@@ -1206,10 +1225,14 @@ let assert_backend_supports_decreases_clauses () =
*)
let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : unit =
- assert (!backend = FStar);
+ cassert __FILE__ __LINE__ (!backend = FStar) def.meta
+ "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.def_id def.loop_id ctx in
+ let def_name =
+ ctx_get_termination_measure def.meta def.def_id def.loop_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 *)
@@ -1271,12 +1294,16 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
*)
let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : unit =
- assert (!backend = Lean);
+ cassert __FILE__ __LINE__ (!backend = Lean) def.meta
+ "The generation of template termination and decreasing clauses is only \
+ supported for the Lean backend";
(*
* Extract a template for the termination measure
*)
(* Retrieve the function name *)
- let def_name = ctx_get_termination_measure def.def_id def.loop_id ctx in
+ let def_name =
+ ctx_get_termination_measure def.meta def.def_id def.loop_id ctx
+ in
let def_body = Option.get def.body in
(* Add a break before *)
F.pp_print_break fmt 0 0;
@@ -1311,7 +1338,7 @@ 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 (List.hd vars) ctx_body)
+ F.pp_print_string fmt (ctx_get_var def.meta (List.hd vars) ctx_body)
else (
F.pp_open_hovbox fmt 0;
F.pp_print_string fmt "(";
@@ -1319,7 +1346,7 @@ 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 v ctx_body))
+ (fun v -> F.pp_print_string fmt (ctx_get_var def.meta v ctx_body))
vars;
F.pp_print_string fmt ")";
F.pp_close_box fmt ());
@@ -1333,7 +1360,7 @@ 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.def_id def.loop_id ctx in
+ let def_name = ctx_get_decreases_proof def.meta def.def_id def.loop_id ctx in
(* syntax <def_name> term ... term : tactic *)
F.pp_print_break fmt 0 0;
extract_comment_with_span ctx fmt
@@ -1356,7 +1383,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 v ctx_body))
+ F.pp_print_string fmt (ctx_get_var def.meta v ctx_body))
vars;
F.pp_print_string fmt ") =>";
F.pp_close_box fmt ();
@@ -1394,9 +1421,9 @@ 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 =
- assert (not def.is_global_decl_body);
+ sanity_check __FILE__ __LINE__ (not def.is_global_decl_body) def.meta;
(* Retrieve the function name *)
- let def_name = ctx_get_local_function def.def_id def.loop_id ctx in
+ let def_name = ctx_get_local_function def.meta 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;
@@ -1466,18 +1493,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 ();
+ assert_backend_supports_decreases_clauses def.meta;
if !backend = FStar then (
F.pp_print_string fmt "Tot";
F.pp_print_space fmt ()));
- extract_ty ctx fmt TypeDeclId.Set.empty has_decreases_clause
+ extract_ty def.meta 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 ();
+ assert_backend_supports_decreases_clauses def.meta;
F.pp_print_space fmt ();
(* Open a box for the decreases clause *)
F.pp_open_hovbox fmt ctx.indent_incr;
@@ -1487,7 +1514,9 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the decreases term *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* The name of the decrease clause *)
- let decr_name = ctx_get_termination_measure def.def_id def.loop_id ctx in
+ let decr_name =
+ ctx_get_termination_measure def.meta def.def_id def.loop_id ctx
+ in
F.pp_print_string fmt decr_name;
(* Print the generic parameters - TODO: we do this many
times, we should have a helper to factor it out *)
@@ -1517,7 +1546,7 @@ 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 ctx fmt true false lv in
+ let ctx = extract_typed_pattern def.meta ctx fmt true false lv in
ctx)
ctx inputs_lvs
in
@@ -1543,7 +1572,9 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the body *)
F.pp_open_hvbox fmt 0;
(* Extract the body *)
- let _ = extract_texpression ctx_body fmt false (Option.get def.body).body in
+ let _ =
+ extract_texpression def.meta ctx_body fmt false (Option.get def.body).body
+ in
(* Close the box for the body *)
F.pp_close_box fmt ());
(* Close the inner box for the definition *)
@@ -1559,7 +1590,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* termination_by *)
let terminates_name =
- ctx_get_termination_measure def.def_id def.loop_id ctx
+ ctx_get_termination_measure def.meta 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] *)
@@ -1572,7 +1603,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 v ctx_body))
+ F.pp_print_string fmt (ctx_get_var def.meta v ctx_body))
all_vars;
F.pp_print_space fmt ();
F.pp_print_string fmt "=>";
@@ -1592,7 +1623,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 v ctx_body))
+ F.pp_print_string fmt (ctx_get_var def.meta v ctx_body))
vars;
(* Close the box for [DECREASES] *)
F.pp_close_box fmt ();
@@ -1602,7 +1633,9 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_break fmt 0 0;
(* Open a box for the [decreasing by ...] *)
F.pp_open_hvbox fmt ctx.indent_incr;
- let decreases_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in
+ let decreases_name =
+ ctx_get_decreases_proof def.meta def.def_id def.loop_id ctx
+ in
F.pp_print_string fmt "decreasing_by";
F.pp_print_space fmt ();
F.pp_open_hvbox fmt ctx.indent_incr;
@@ -1610,7 +1643,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 v ctx_body))
+ F.pp_print_string fmt (ctx_get_var def.meta v ctx_body))
vars;
F.pp_close_box fmt ();
(* Close the box for the [decreasing by ...] *)
@@ -1640,12 +1673,15 @@ 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.def_id def.loop_id ctx in
- assert (def.signature.generics.const_generics = []);
+ let def_name = ctx_get_local_function def.meta def.def_id def.loop_id ctx in
+ cassert __FILE__ __LINE__
+ (def.signature.generics.const_generics = [])
+ def.meta
+ "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.llbc_name def.signature.llbc_generics
+ ctx_add_generic_params def.meta def.llbc_name def.signature.llbc_generics
def.signature.generics ctx
in
(* Add breaks to insert new lines between definitions *)
@@ -1662,7 +1698,7 @@ 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 ctx fmt TypeDeclId.Set.empty false def.signature.output;
+ extract_ty def.meta 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 ();
@@ -1687,7 +1723,7 @@ 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 =
- assert (not def.is_global_decl_body);
+ sanity_check __FILE__ __LINE__ (not def.is_global_decl_body) def.meta;
(* 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
@@ -1700,10 +1736,10 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
extracted to two declarations, and we can actually factor out the generation
of those declarations. See {!extract_global_decl} for more explanations.
*)
-let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
- (kind : decl_kind) (name : string) (generics : generic_params)
- (type_params : string list) (cg_params : string list)
- (trait_clauses : string list) (ty : ty)
+let extract_global_decl_body_gen (meta : Meta.meta) (ctx : extraction_ctx)
+ (fmt : F.formatter) (kind : decl_kind) (name : string)
+ (generics : generic_params) (type_params : string list)
+ (cg_params : string list) (trait_clauses : string list) (ty : ty)
(extract_body : (F.formatter -> unit) Option.t) : unit =
let is_opaque = Option.is_none extract_body in
@@ -1733,7 +1769,7 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Extract the generic parameters *)
let space = ref true in
- extract_generic_params ctx fmt TypeDeclId.Set.empty ~space:(Some space)
+ extract_generic_params meta ctx fmt TypeDeclId.Set.empty ~space:(Some space)
generics type_params cg_params trait_clauses;
if not !space then F.pp_print_space fmt ();
@@ -1746,7 +1782,7 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Open "TYPE" box (depth=3) *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print "TYPE" *)
- extract_ty ctx fmt TypeDeclId.Set.empty false ty;
+ extract_ty meta ctx fmt TypeDeclId.Set.empty false ty;
(* Close "TYPE" box (depth=3) *)
F.pp_close_box fmt ();
@@ -1792,8 +1828,9 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
Remark (SH): having to treat this specific case separately is very annoying,
but I could not find a better way.
*)
-let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
- (name : string) (generics : generic_params) (ty : ty) : unit =
+let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx)
+ (fmt : F.formatter) (name : string) (generics : generic_params) (ty : ty) :
+ unit =
(* TODO: non-empty generics *)
assert (generics = empty_generic_params);
(* Open the definition boxe (depth=0) *)
@@ -1805,7 +1842,7 @@ let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_close_box fmt ();
(* Print the type *)
F.pp_open_hovbox fmt 0;
- extract_ty ctx fmt TypeDeclId.Set.empty false ty;
+ extract_ty meta ctx fmt TypeDeclId.Set.empty false ty;
(* Close the definition *)
F.pp_print_string fmt ")";
F.pp_close_box fmt ();
@@ -1836,8 +1873,9 @@ let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
*)
let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
(global : global_decl) (body : fun_decl) (interface : bool) : unit =
- assert body.is_global_decl_body;
- assert (body.signature.inputs = []);
+ let meta = body.meta in
+ sanity_check __FILE__ __LINE__ body.is_global_decl_body meta;
+ sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta;
(* Add a break then the name of the corresponding LLBC declaration *)
F.pp_print_break fmt 0 0;
@@ -1851,40 +1889,42 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
name global.meta.span;
F.pp_print_space fmt ();
- let decl_name = ctx_get_global global.def_id ctx in
+ let decl_name = ctx_get_global meta global.def_id ctx in
let body_name =
- ctx_get_function (FromLlbc (Pure.FunId (FRegular global.body_id), None)) ctx
+ ctx_get_function meta
+ (FromLlbc (Pure.FunId (FRegular global.body_id), None))
+ ctx
in
let decl_ty, body_ty =
let ty = body.signature.output in
if body.signature.fwd_info.effect_info.can_fail then
- (unwrap_result_ty ty, ty)
+ (unwrap_result_ty meta ty, ty)
else (ty, mk_result_ty ty)
in
(* Add the type parameters *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params global.llbc_name global.llbc_generics global.generics
- ctx
+ ctx_add_generic_params meta global.llbc_name global.llbc_generics
+ global.generics ctx
in
match body.body with
| None ->
(* No body: only generate a [val x_c : u32] declaration *)
let kind = if interface then Declared else Assumed in
if !backend = HOL4 then
- extract_global_decl_hol4_opaque ctx fmt decl_name global.generics
+ extract_global_decl_hol4_opaque meta ctx fmt decl_name global.generics
decl_ty
else
- extract_global_decl_body_gen ctx fmt kind decl_name global.generics
+ extract_global_decl_body_gen meta ctx fmt kind decl_name global.generics
type_params cg_params trait_clauses decl_ty None
| Some body ->
(* There is a body *)
(* Generate: [let x_body : result u32 = Return 3] *)
- extract_global_decl_body_gen ctx fmt SingleNonRec body_name
+ extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name
global.generics type_params cg_params trait_clauses body_ty
- (Some (fun fmt -> extract_texpression ctx fmt false body.body));
+ (Some (fun fmt -> extract_texpression meta ctx fmt false body.body));
F.pp_print_break fmt 0 0;
(* Generate: [let x_c : u32 = eval_global x_body] *)
- extract_global_decl_body_gen ctx fmt SingleNonRec decl_name
+ extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name
global.generics type_params cg_params trait_clauses decl_ty
(Some
(fun fmt ->
@@ -1953,7 +1993,9 @@ let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx)
(* Register the names *)
List.fold_left
(fun ctx (cid, cname) ->
- ctx_add (TraitParentClauseId (trait_decl.def_id, cid)) cname ctx)
+ ctx_add trait_decl.meta
+ (TraitParentClauseId (trait_decl.def_id, cid))
+ cname ctx)
ctx clause_names
(** Similar to {!extract_trait_decl_register_names} *)
@@ -1986,7 +2028,9 @@ let extract_trait_decl_register_constant_names (ctx : extraction_ctx)
(* Register the names *)
List.fold_left
(fun ctx (item_name, name) ->
- ctx_add (TraitItemId (trait_decl.def_id, item_name)) name ctx)
+ ctx_add trait_decl.meta
+ (TraitItemId (trait_decl.def_id, item_name))
+ name ctx)
ctx constant_names
(** Similar to {!extract_trait_decl_register_names} *)
@@ -2045,11 +2089,13 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
List.fold_left
(fun ctx (item_name, (type_name, clauses)) ->
let ctx =
- ctx_add (TraitItemId (trait_decl.def_id, item_name)) type_name ctx
+ ctx_add trait_decl.meta
+ (TraitItemId (trait_decl.def_id, item_name))
+ type_name ctx
in
List.fold_left
(fun ctx (clause_id, clause_name) ->
- ctx_add
+ ctx_add trait_decl.meta
(TraitItemClauseId (trait_decl.def_id, item_name, clause_id))
clause_name ctx)
ctx clauses)
@@ -2101,7 +2147,9 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
(* Register the names *)
List.fold_left
(fun ctx (item_name, fun_name) ->
- ctx_add (TraitMethodId (trait_decl.def_id, item_name)) fun_name ctx)
+ ctx_add trait_decl.meta
+ (TraitMethodId (trait_decl.def_id, item_name))
+ fun_name ctx)
ctx method_names
(** Similar to {!extract_type_decl_register_names} *)
@@ -2121,8 +2169,11 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
ctx_compute_trait_decl_constructor ctx trait_decl )
| Some info -> (info.extract_name, info.constructor)
in
- let ctx = ctx_add (TraitDeclId trait_decl.def_id) trait_name ctx in
- ctx_add (TraitDeclConstructorId trait_decl.def_id) trait_constructor ctx
+ let ctx =
+ ctx_add trait_decl.meta (TraitDeclId trait_decl.def_id) trait_name ctx
+ in
+ ctx_add trait_decl.meta (TraitDeclConstructorId trait_decl.def_id)
+ trait_constructor ctx
in
(* Parent clauses *)
let ctx =
@@ -2176,7 +2227,13 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
in
(* For now we do not support overriding provided methods *)
- assert (trait_impl.provided_methods = []);
+ cassert __FILE__ __LINE__
+ (trait_impl.provided_methods = [])
+ trait_impl.meta
+ ("Overriding trait provided methods in trait implementations is not \
+ supported yet (overriden methods: "
+ ^ String.concat ", " (List.map fst trait_impl.provided_methods)
+ ^ ")");
(* Everything is taken care of by {!extract_trait_decl_register_names} *but*
the name of the implementation itself *)
(* Compute the name *)
@@ -2185,7 +2242,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 (TraitImplId trait_impl.def_id) name ctx
+ ctx_add trait_decl.meta (TraitImplId trait_impl.def_id) name ctx
(** Small helper.
@@ -2234,7 +2291,7 @@ 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.def_id item_name ctx in
+ let fun_name = ctx_get_trait_method decl.meta 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
@@ -2250,7 +2307,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 f.llbc_name f.signature.llbc_generics generics ctx
+ ctx_add_generic_params decl.meta f.llbc_name f.signature.llbc_generics
+ generics ctx
in
let backend_uses_forall =
match !backend with Coq | Lean -> true | FStar | HOL4 -> false
@@ -2259,7 +2317,7 @@ 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 ctx fmt TypeDeclId.Set.empty ~use_forall
+ extract_generic_params decl.meta 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 ",";
@@ -2273,7 +2331,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.def_id ctx in
+ let decl_name = ctx_get_trait_decl decl.meta 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 *)
@@ -2301,7 +2359,7 @@ 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 SingleNonRec (Some Struct))
+ Option.get (type_decl_kind_to_qualif decl.meta SingleNonRec (Some Struct))
in
(* When checking if the trait declaration is empty: we ignore the provided
methods, because for now they are extracted separately *)
@@ -2317,10 +2375,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.llbc_name decl.llbc_generics generics ctx
+ ctx_add_generic_params decl.meta decl.llbc_name decl.llbc_generics generics
+ ctx
in
- extract_generic_params ctx fmt TypeDeclId.Set.empty generics type_params
- cg_params trait_clauses;
+ extract_generic_params decl.meta ctx fmt TypeDeclId.Set.empty generics
+ type_params cg_params trait_clauses;
F.pp_print_space fmt ();
if is_empty && !backend = FStar then (
@@ -2329,7 +2388,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.def_id ctx in
+ let cons = ctx_get_trait_constructor decl.meta decl.def_id ctx in
F.pp_print_string fmt (":= " ^ cons ^ "{}.");
(* Outer box *)
F.pp_close_box fmt ())
@@ -2338,7 +2397,7 @@ 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.def_id ctx in
+ let cons = ctx_get_trait_constructor decl.meta decl.def_id ctx in
F.pp_print_string fmt (":= " ^ cons ^ " {")
| _ -> F.pp_print_string fmt "{");
@@ -2352,11 +2411,11 @@ 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.def_id name ctx in
+ let item_name = ctx_get_trait_const decl.meta decl.def_id name ctx in
let ty () =
let inside = false in
F.pp_print_space fmt ();
- extract_ty ctx fmt TypeDeclId.Set.empty inside ty
+ extract_ty decl.meta ctx fmt TypeDeclId.Set.empty inside ty
in
extract_trait_decl_item ctx fmt item_name ty)
decl.consts;
@@ -2365,21 +2424,23 @@ 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.def_id name ctx in
+ let item_name = ctx_get_trait_type decl.meta decl.def_id name ctx in
let ty () =
F.pp_print_space fmt ();
- F.pp_print_string fmt (type_keyword ())
+ F.pp_print_string fmt (type_keyword decl.meta)
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.def_id name clause.clause_id ctx
+ ctx_get_trait_item_clause decl.meta decl.def_id name
+ clause.clause_id ctx
in
let ty () =
F.pp_print_space fmt ();
- extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause
+ extract_trait_clause_type decl.meta ctx fmt TypeDeclId.Set.empty
+ clause
in
extract_trait_decl_item ctx fmt item_name ty)
clauses)
@@ -2390,11 +2451,12 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
List.iter
(fun clause ->
let item_name =
- ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx
+ ctx_get_trait_parent_clause decl.meta decl.def_id clause.clause_id ctx
in
let ty () =
F.pp_print_space fmt ();
- extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause
+ extract_trait_clause_type decl.meta ctx fmt TypeDeclId.Set.empty
+ clause
in
extract_trait_decl_item ctx fmt item_name ty)
decl.parent_clauses;
@@ -2431,25 +2493,26 @@ 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.def_id ctx in
+ let cons_name = ctx_get_trait_constructor decl.meta 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.def_id name ctx in
+ let item_name = ctx_get_trait_const decl.meta 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.def_id name ctx in
+ let item_name = ctx_get_trait_type decl.meta 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.def_id name clause.clause_id ctx
+ ctx_get_trait_item_clause decl.meta decl.def_id name
+ clause.clause_id ctx
in
extract_coq_arguments_instruction ctx fmt item_name num_params)
clauses)
@@ -2458,7 +2521,7 @@ 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.def_id clause.clause_id ctx
+ ctx_get_trait_parent_clause decl.meta decl.def_id clause.clause_id ctx
in
extract_coq_arguments_instruction ctx fmt item_name num_params)
decl.parent_clauses;
@@ -2466,7 +2529,9 @@ let extract_trait_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
List.iter
(fun (item_name, _) ->
(* Extract the items *)
- let item_name = ctx_get_trait_method decl.def_id item_name ctx in
+ let item_name =
+ ctx_get_trait_method decl.meta decl.def_id item_name ctx
+ in
extract_coq_arguments_instruction ctx fmt item_name num_params)
decl.required_methods;
(* Add a space *)
@@ -2491,7 +2556,7 @@ 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 trait_decl_id item_name ctx in
+ let fun_name = ctx_get_trait_method impl.meta trait_decl_id item_name ctx in
let ty () =
(* Filter the generics if the method is a builtin *)
let i_tys, _, _ = impl_generics in
@@ -2531,16 +2596,16 @@ 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 f.llbc_name f.signature.llbc_generics f_generics
- ctx
+ ctx_add_generic_params impl.meta f.llbc_name f.signature.llbc_generics
+ f_generics ctx
in
let use_forall = f_generics <> empty_generic_params in
- extract_generic_params ctx fmt TypeDeclId.Set.empty ~use_forall f_generics
- f_tys f_cgs f_tcs;
+ extract_generic_params impl.meta 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 f.def_id None ctx in
+ let fun_name = ctx_get_local_function impl.meta f.def_id None ctx in
F.pp_print_string fmt fun_name;
let all_generics =
let _, i_cgs, i_tcs = impl_generics in
@@ -2561,7 +2626,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.def_id ctx in
+ let impl_name = ctx_get_trait_impl impl.meta 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 *)
@@ -2602,17 +2667,19 @@ 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.llbc_name impl.llbc_generics impl.generics ctx
+ ctx_add_generic_params impl.meta impl.llbc_name impl.llbc_generics
+ impl.generics ctx
in
let all_generics = (type_params, cg_params, trait_clauses) in
- extract_generic_params ctx fmt TypeDeclId.Set.empty impl.generics type_params
- cg_params trait_clauses;
+ extract_generic_params impl.meta 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 ctx fmt TypeDeclId.Set.empty false impl.impl_trait;
+ extract_trait_decl_ref impl.meta ctx fmt TypeDeclId.Set.empty false
+ impl.impl_trait;
(* When checking if the trait impl is empty: we ignore the provided
methods, because for now they are extracted separately *)
@@ -2625,7 +2692,9 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_close_box fmt ())
else if is_empty && !Config.backend = Coq then (
(* Coq is not very good at infering constructors *)
- let cons = ctx_get_trait_constructor impl.impl_trait.trait_decl_id ctx in
+ let cons =
+ ctx_get_trait_constructor impl.meta impl.impl_trait.trait_decl_id ctx
+ in
F.pp_print_string fmt (":= " ^ cons ^ ".");
(* Outer box *)
F.pp_close_box fmt ())
@@ -2649,12 +2718,12 @@ 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 trait_decl_id name ctx in
+ let item_name = ctx_get_trait_const impl.meta 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 ctx fmt TypeDeclId.Set.empty
+ extract_generic_args impl.meta ctx fmt TypeDeclId.Set.empty
impl.impl_trait.decl_generics
else
let all_params =
@@ -2668,7 +2737,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 id ctx);
+ F.pp_print_string fmt (ctx_get_global impl.meta id ctx);
print_params ()
in
@@ -2679,21 +2748,23 @@ 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 trait_decl_id name ctx in
+ let item_name = ctx_get_trait_type impl.meta trait_decl_id name ctx in
let ty () =
F.pp_print_space fmt ();
- extract_ty ctx fmt TypeDeclId.Set.empty false ty
+ extract_ty impl.meta 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 trait_decl_id name clause_id ctx
+ ctx_get_trait_item_clause impl.meta trait_decl_id name clause_id
+ ctx
in
let ty () =
F.pp_print_space fmt ();
- extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref
+ extract_trait_ref impl.meta ctx fmt TypeDeclId.Set.empty false
+ trait_ref
in
extract_trait_impl_item ctx fmt item_name ty)
trait_refs)
@@ -2703,11 +2774,12 @@ 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 trait_decl_id clause_id ctx
+ ctx_get_trait_parent_clause impl.meta trait_decl_id clause_id ctx
in
let ty () =
F.pp_print_space fmt ();
- extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref
+ extract_trait_ref impl.meta ctx fmt TypeDeclId.Set.empty false
+ trait_ref
in
extract_trait_impl_item ctx fmt item_name ty)
impl.parent_trait_refs;
@@ -2770,7 +2842,9 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "assert_norm";
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
- let fun_name = ctx_get_local_function def.def_id def.loop_id ctx in
+ let fun_name =
+ ctx_get_local_function def.meta def.def_id def.loop_id ctx
+ in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
F.pp_print_space fmt ();
@@ -2778,13 +2852,17 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt "=";
F.pp_print_space fmt ();
- let success = ctx_get_variant (TAssumed TResult) result_return_id ctx in
+ let success =
+ ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx
+ in
F.pp_print_string fmt (success ^ " ())")
| Coq ->
F.pp_print_string fmt "Check";
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
- let fun_name = ctx_get_local_function def.def_id def.loop_id ctx in
+ let fun_name =
+ ctx_get_local_function def.meta def.def_id def.loop_id ctx
+ in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
F.pp_print_space fmt ();
@@ -2795,7 +2873,9 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "#assert";
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
- let fun_name = ctx_get_local_function def.def_id def.loop_id ctx in
+ let fun_name =
+ ctx_get_local_function def.meta def.def_id def.loop_id ctx
+ in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
F.pp_print_space fmt ();
@@ -2803,12 +2883,16 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt "==";
F.pp_print_space fmt ();
- let success = ctx_get_variant (TAssumed TResult) result_return_id ctx in
+ let success =
+ ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx
+ in
F.pp_print_string fmt (success ^ " ())")
| HOL4 ->
F.pp_print_string fmt "val _ = assert_return (";
F.pp_print_string fmt "“";
- let fun_name = ctx_get_local_function def.def_id def.loop_id ctx in
+ let fun_name =
+ ctx_get_local_function def.meta def.def_id def.loop_id ctx
+ in
F.pp_print_string fmt fun_name;
if sg.inputs <> [] then (
F.pp_print_space fmt ();
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 05:41:08 +0000