summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/AssociatedTypes.ml1
-rw-r--r--compiler/Extract.ml58
-rw-r--r--compiler/ExtractBase.ml29
-rw-r--r--compiler/ExtractTypes.ml24
4 files changed, 52 insertions, 60 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index 38615777..0ed46e8c 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -418,7 +418,6 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
| TraitRef trait_ref ->
(* The trait instance id necessarily refers to a local sub-clause. We
can't project over it and can only peel off the [TraitRef] wrapper *)
-(* let meta = (TraitDeclId.Map.find trait_ref.trait_decl_ref.trait_decl_id ctx.trait_decls).meta in *)
cassert_opt_meta (trait_instance_id_is_local_clause trait_ref.trait_id) ctx.meta "Trait instance id is not a local sub-clause";
cassert_opt_meta (trait_ref.generics = empty_generic_args) ctx.meta "TODO: error message";
(trait_ref.trait_id, None)
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 3d0fe75f..564ffafb 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -452,7 +452,7 @@ and extract_function_call (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.for
cassert (lp_id = None) trait_decl.meta "TODO: Error message";
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) =
@@ -2236,7 +2236,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
@@ -2252,7 +2252,7 @@ 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.meta f.llbc_name f.signature.llbc_generics generics ctx (* TODO: confirm it's the right meta*)
+ ctx_add_generic_params decl.meta f.llbc_name f.signature.llbc_generics generics ctx (* TODO: confirm it's the right meta*)
in
let backend_uses_forall =
match !backend with Coq | Lean -> true | FStar | HOL4 -> false
@@ -2261,7 +2261,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 f.meta 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; (* TODO: confirm it's the right meta*)
if use_forall then F.pp_print_string fmt ",";
@@ -2275,7 +2275,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 *)
@@ -2331,7 +2331,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 ())
@@ -2340,7 +2340,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 "{");
@@ -2354,7 +2354,7 @@ 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 ();
@@ -2367,7 +2367,7 @@ 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 decl.meta)
@@ -2377,11 +2377,11 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
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)
@@ -2392,11 +2392,11 @@ 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;
@@ -2433,25 +2433,25 @@ 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)
@@ -2460,7 +2460,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;
@@ -2468,7 +2468,7 @@ 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 *)
@@ -2493,7 +2493,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
@@ -2533,16 +2533,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.meta f.llbc_name f.signature.llbc_generics f_generics
+ 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 f.meta ctx fmt TypeDeclId.Set.empty ~use_forall f_generics
+ 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.meta 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
@@ -2565,7 +2565,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 *)
@@ -2629,7 +2629,7 @@ 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 ())
@@ -2653,7 +2653,7 @@ 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 () =
@@ -2683,7 +2683,7 @@ 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 impl.meta ctx fmt TypeDeclId.Set.empty false ty
@@ -2693,7 +2693,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
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 ();
@@ -2707,7 +2707,7 @@ 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 ();
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 6e799bd9..c2e3e35f 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -688,48 +688,41 @@ let ctx_get_local_type (meta : Meta.meta) (id : TypeDeclId.id) (ctx : extraction
let ctx_get_assumed_type ?(meta = None) (id : assumed_ty) (ctx : extraction_ctx) : string =
ctx_get_type ~meta:meta (TAssumed id) ctx
-let ctx_get_trait_constructor (id : trait_decl_id) (ctx : extraction_ctx) :
+let ctx_get_trait_constructor (meta : Meta.meta) (id : trait_decl_id) (ctx : extraction_ctx) :
string =
- let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
ctx_get ~meta:(Some meta) (TraitDeclConstructorId id) ctx
let ctx_get_trait_self_clause (meta : Meta.meta) (ctx : extraction_ctx) : string =
ctx_get ~meta:(Some meta) TraitSelfClauseId ctx
-let ctx_get_trait_decl (id : trait_decl_id) (ctx : extraction_ctx) : string =
- let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
+let ctx_get_trait_decl (meta : Meta.meta) (id : trait_decl_id) (ctx : extraction_ctx) : string =
ctx_get ~meta:(Some meta) (TraitDeclId id) ctx
-let ctx_get_trait_impl (id : trait_impl_id) (ctx : extraction_ctx) : string =
- let meta = (TraitImplId.Map.find id ctx.trans_trait_impls).meta in
+let ctx_get_trait_impl (meta : Meta.meta) (id : trait_impl_id) (ctx : extraction_ctx) : string =
ctx_get ~meta:(Some meta) (TraitImplId id) ctx
-let ctx_get_trait_item (id : trait_decl_id) (item_name : string)
+let ctx_get_trait_item (meta : Meta.meta) (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
- let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
ctx_get ~meta:(Some meta) (TraitItemId (id, item_name)) ctx
-let ctx_get_trait_const (id : trait_decl_id) (item_name : string)
+let ctx_get_trait_const (meta : Meta.meta) (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
- ctx_get_trait_item id item_name ctx
+ ctx_get_trait_item meta id item_name ctx
-let ctx_get_trait_type (id : trait_decl_id) (item_name : string)
+let ctx_get_trait_type (meta : Meta.meta) (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
- ctx_get_trait_item id item_name ctx
+ ctx_get_trait_item meta id item_name ctx
-let ctx_get_trait_method (id : trait_decl_id) (item_name : string)
+let ctx_get_trait_method (meta : Meta.meta) (id : trait_decl_id) (item_name : string)
(ctx : extraction_ctx) : string =
- let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
ctx_get ~meta:(Some meta) (TraitMethodId (id, item_name)) ctx
-let ctx_get_trait_parent_clause (id : trait_decl_id) (clause : trait_clause_id)
+let ctx_get_trait_parent_clause (meta : Meta.meta) (id : trait_decl_id) (clause : trait_clause_id)
(ctx : extraction_ctx) : string =
- let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
ctx_get ~meta:(Some meta) (TraitParentClauseId (id, clause)) ctx
-let ctx_get_trait_item_clause (id : trait_decl_id) (item : string)
+let ctx_get_trait_item_clause (meta : Meta.meta) (id : trait_decl_id) (item : string)
(clause : trait_clause_id) (ctx : extraction_ctx) : string =
- let meta = (TraitDeclId.Map.find id ctx.trans_trait_decls).meta in
ctx_get ~meta:(Some meta) (TraitItemClauseId (id, item, clause)) ctx
let ctx_get_var (meta : Meta.meta) (id : VarId.id) (ctx : extraction_ctx) : string =
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 0329d968..b26704ce 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -533,7 +533,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
if !parameterize_trait_types then craise meta "Unimplemented"
else
let type_name =
- ctx_get_trait_type trait_ref.trait_decl_ref.trait_decl_id type_name
+ ctx_get_trait_type meta trait_ref.trait_decl_ref.trait_decl_id type_name
ctx
in
let add_brackets (s : string) =
@@ -548,7 +548,7 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
*)
match trait_ref.trait_id with
| Self ->
- assert (trait_ref.generics = empty_generic_args);
+ cassert (trait_ref.generics = empty_generic_args) "TODO: Error message";
extract_trait_instance_id_with_dot meta ctx fmt no_params_tys false
trait_ref.trait_id;
F.pp_print_string fmt type_name
@@ -587,7 +587,7 @@ and extract_trait_decl_ref (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.fo
(no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_decl_ref) :
unit =
let use_brackets = tr.decl_generics <> empty_generic_args && inside in
- let name = ctx_get_trait_decl tr.trait_decl_id ctx in
+ let name = ctx_get_trait_decl meta tr.trait_decl_id ctx in
if use_brackets then F.pp_print_string fmt "(";
F.pp_print_string fmt name;
(* There is something subtle here: the trait obligations for the implemented
@@ -665,19 +665,19 @@ and extract_trait_instance_id (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F
craise meta "Unexpected occurrence of `Self`"
else F.pp_print_string fmt "ERROR(\"Unexpected Self\")"
| TraitImpl id ->
- let name = ctx_get_trait_impl id ctx in
+ let name = ctx_get_trait_impl meta id ctx in
F.pp_print_string fmt name
| Clause id ->
let name = ctx_get_local_trait_clause meta id ctx in
F.pp_print_string fmt name
| ParentClause (inst_id, decl_id, clause_id) ->
(* Use the trait decl id to lookup the name *)
- let name = ctx_get_trait_parent_clause decl_id clause_id ctx in
+ let name = ctx_get_trait_parent_clause meta decl_id clause_id ctx in
extract_trait_instance_id_with_dot meta ctx fmt no_params_tys true inst_id;
F.pp_print_string fmt (add_brackets name)
| ItemClause (inst_id, decl_id, item_name, clause_id) ->
(* Use the trait decl id to lookup the name *)
- let name = ctx_get_trait_item_clause decl_id item_name clause_id ctx in
+ let name = ctx_get_trait_item_clause meta decl_id item_name clause_id ctx in
extract_trait_instance_id_with_dot meta ctx fmt no_params_tys true inst_id;
F.pp_print_string fmt (add_brackets name)
| TraitRef trait_ref ->
@@ -1130,12 +1130,12 @@ let extract_comment_with_span (ctx : extraction_ctx) (fmt : F.formatter)
in
extract_comment fmt (sl @ [ span ] @ name)
-let extract_trait_clause_type (* (meta : Meta.meta) TODO check if right meta*) (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_trait_clause_type (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit =
- let trait_name = ctx_get_trait_decl clause.trait_id ctx in
+ let trait_name = ctx_get_trait_decl meta clause.trait_id ctx in
F.pp_print_string fmt trait_name;
- let meta = (TraitDeclId.Map.find clause.trait_id ctx.trans_trait_decls).meta in
- extract_generic_args meta ctx fmt no_params_tys clause.generics
+ (* let meta = (TraitDeclId.Map.find clause.trait_id ctx.trans_trait_decls).meta in
+ *)extract_generic_args meta ctx fmt no_params_tys clause.generics
(** Insert a space, if necessary *)
let insert_req_space (fmt : F.formatter) (space : bool ref) : unit =
@@ -1155,7 +1155,7 @@ let extract_trait_self_clause (insert_req_space : unit -> unit)
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- let trait_id = ctx_get_trait_decl trait_decl.def_id ctx in
+ let trait_id = ctx_get_trait_decl trait_decl.meta trait_decl.def_id ctx in
F.pp_print_string fmt trait_id;
List.iter
(fun p ->
@@ -1258,7 +1258,7 @@ let extract_generic_params (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.fo
F.pp_print_space fmt ();
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
- extract_trait_clause_type ctx fmt no_params_tys clause;
+ extract_trait_clause_type meta ctx fmt no_params_tys clause;
(* ) *)
right_bracket as_implicits;
if use_arrows then (
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 02:52:14 +0000