diff options
Diffstat (limited to 'compiler/Extract.ml')
| -rw-r--r-- | compiler/Extract.ml | 137 |
1 files changed, 105 insertions, 32 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 46f6a1ca..aa097a4f 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -185,9 +185,17 @@ let extract_adt_g_value | _ -> raise (Failure "Inconsistent typed value") (* Extract globals in the same way as variables *) -let extract_global (ctx : extraction_ctx) (fmt : F.formatter) - (id : A.GlobalDeclId.id) : unit = - F.pp_print_string fmt (ctx_get_global id ctx) +let extract_global (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); + (* Extract the generics *) + extract_generic_args ctx fmt TypeDeclId.Set.empty generics; + if use_brackets then F.pp_print_string fmt ")"; + F.pp_close_box fmt () (* Filter the generics of a function if it is builtin *) let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list) @@ -321,16 +329,15 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) match qualif.id with | FunOrOp fun_id -> extract_function_call ctx fmt inside fun_id qualif.generics args - | Global global_id -> extract_global ctx fmt global_id + | Global global_id -> + assert (args = []); + extract_global ctx fmt inside global_id qualif.generics | AdtCons adt_cons_id -> extract_adt_cons ctx fmt inside adt_cons_id qualif.generics args | Proj proj -> extract_field_projector ctx fmt inside app proj qualif.generics args - | TraitConst (trait_ref, generics, const_name) -> - let use_brackets = generics <> empty_generic_args in - if use_brackets then F.pp_print_string fmt "("; - extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref; - extract_generic_args ctx fmt TypeDeclId.Set.empty generics; + | TraitConst (trait_ref, const_name) -> + extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref; let name = ctx_get_trait_const trait_ref.trait_decl_ref.trait_decl_id const_name ctx @@ -338,7 +345,6 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) let add_brackets (s : string) = if !backend = Coq then "(" ^ s ^ ")" else s in - if use_brackets then F.pp_print_string fmt ")"; F.pp_print_string fmt ("." ^ add_brackets name)) | _ -> (* "Regular" expression *) @@ -1695,7 +1701,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) 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) (ty : ty) + (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 @@ -1712,9 +1720,9 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) F.pp_open_hvbox fmt 0; F.pp_open_hvbox fmt ctx.indent_incr; - (* Open "QUALIF NAME : TYPE =" box (depth=1) *) + (* Open "QUALIF NAME PARAMS : TYPE =" box (depth=1) *) F.pp_open_hovbox fmt ctx.indent_incr; - (* Print "QUALIF NAME " *) + (* Print "QUALIF NAME PARAMS " *) (match fun_decl_kind_to_qualif kind with | Some qualif -> F.pp_print_string fmt qualif; @@ -1723,6 +1731,12 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt name; F.pp_print_space fmt (); + (* Extract the generic parameters *) + let space = ref true in + extract_generic_params ctx fmt TypeDeclId.Set.empty ~space:(Some space) + generics type_params cg_params trait_clauses; + if not !space then F.pp_print_space fmt (); + (* Open ": TYPE =" box (depth=2) *) F.pp_open_hvbox fmt 0; (* Print ": " *) @@ -1779,7 +1793,9 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) but I could not find a better way. *) let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) - (name : string) (ty : ty) : unit = + (name : string) (generics : generic_params) (ty : ty) : unit = + (* TODO: non-empty generics *) + assert (generics = empty_generic_params); (* Open the definition boxe (depth=0) *) F.pp_open_hvbox fmt ctx.indent_incr; (* [val ..._def = new_constant ("...",] *) @@ -1819,58 +1835,94 @@ let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) and {!extract_fun_decl}. *) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) - (global : A.global_decl) (body : fun_decl) (interface : bool) : unit = + (global : global_decl) (body : fun_decl) (interface : bool) : unit = assert body.is_global_decl_body; assert (body.signature.inputs = []); - assert (body.signature.generics = empty_generic_params); (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; let name = if !Config.extract_external_name_patterns && not global.is_local then - Some global.name + Some global.llbc_name else None in extract_comment_with_span ctx fmt - [ "[" ^ name_to_string ctx global.name ^ "]" ] + [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ] name global.meta.span; F.pp_print_space fmt (); let decl_name = ctx_get_global global.def_id ctx in let body_name = - ctx_get_function (FromLlbc (Pure.FunId (FRegular global.body), None)) ctx + ctx_get_function (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) 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 + 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 decl_ty - else extract_global_decl_body_gen ctx fmt kind decl_name decl_ty None + extract_global_decl_hol4_opaque ctx fmt decl_name global.generics + decl_ty + else + extract_global_decl_body_gen 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 body_ty + extract_global_decl_body_gen 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)); 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 decl_ty + extract_global_decl_body_gen ctx fmt SingleNonRec decl_name + global.generics type_params cg_params trait_clauses decl_ty (Some (fun fmt -> - let body = + let all_params = + List.concat [ type_params; cg_params; trait_clauses ] + in + let extract_params () = + List.iter + (fun p -> + F.pp_print_space fmt (); + F.pp_print_string fmt p) + all_params + in + let use_brackets = all_params <> [] in + (* Extract the name *) + let before, after = match !backend with - | FStar | Lean -> "eval_global " ^ body_name - | Coq -> body_name ^ "%global" - | HOL4 -> "get_return_value " ^ body_name + | FStar | Lean -> + ( (fun () -> + F.pp_print_string fmt "eval_global"; + F.pp_print_space fmt ()), + fun () -> () ) + | Coq -> + ((fun () -> ()), fun () -> F.pp_print_string fmt "%global") + | HOL4 -> + ( (fun () -> + F.pp_print_string fmt "get_return_value"; + F.pp_print_space fmt ()), + fun () -> () ) in - F.pp_print_string fmt body)); + before (); + if use_brackets then F.pp_print_string fmt "("; + F.pp_print_string fmt body_name; + (* Extract the generic params *) + extract_params (); + if use_brackets then F.pp_print_string fmt ")"; + (* *) + after ())); (* Add a break to insert lines between declarations *) F.pp_print_break fmt 0 0 @@ -2589,18 +2641,39 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) * Extract the items *) let trait_decl_id = impl.impl_trait.trait_decl_id in + let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in + let trait_decl_provided_consts = + List.map (fun (_, (_, x)) -> x) trait_decl.consts + in (* The constants *) List.iter - (fun (name, (_, id)) -> + (fun (provided_id, (name, (_, id))) -> let item_name = ctx_get_trait_const 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 + impl.impl_trait.decl_generics + else + let all_params = + List.concat [ type_params; cg_params; trait_clauses ] + in + List.iter + (fun p -> + F.pp_print_space fmt (); + F.pp_print_string fmt p) + all_params + 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 id ctx); + print_params () in extract_trait_impl_item ctx fmt item_name ty) - impl.consts; + (List.combine trait_decl_provided_consts impl.consts); (* The types *) List.iter |