From c47e349dedaaf0e3161869740ea769332ffd24ca Mon Sep 17 00:00:00 2001 From: Escherichia Date: Tue, 26 Mar 2024 17:00:47 +0100 Subject: changes to extract_ty and related functions to use the right meta --- compiler/AssociatedTypes.ml | 1 - compiler/Extract.ml | 58 ++++++++++++++++++++++----------------------- compiler/ExtractBase.ml | 29 +++++++++-------------- compiler/ExtractTypes.ml | 24 +++++++++---------- 4 files changed, 52 insertions(+), 60 deletions(-) (limited to 'compiler') 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 ( -- cgit v1.2.3