diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Extract.ml | 414 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 47 |
2 files changed, 237 insertions, 224 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 4238a152..3c4feca5 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -836,6 +836,11 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) to_snake_case basename | Coq | Lean -> basename in + let trait_clause_basename (_varset : StringSet.t) (_clause : trait_clause) : + string = + (* TODO: actually use the clause to derive the name *) + "cl" + in let append_index (basename : string) (i : int) : string = basename ^ string_of_int i in @@ -931,6 +936,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) var_basename; type_var_basename; const_generic_var_basename; + trait_clause_basename; append_index; extract_literal; extract_unop; @@ -1246,16 +1252,18 @@ and extract_trait_ref (ctx : extraction_ctx) (fmt : F.formatter) and extract_generic_args (ctx : extraction_ctx) (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (generics : generic_args) : unit = let { types; const_generics; trait_refs } = generics in - if types <> [] then ( - F.pp_print_space fmt (); - Collections.List.iter_link (F.pp_print_space fmt) - (extract_ty ctx fmt no_params_tys true) - types); - if const_generics <> [] then ( - F.pp_print_space fmt (); - Collections.List.iter_link (F.pp_print_space fmt) - (extract_const_generic ctx fmt true) - const_generics); + if !backend <> HOL4 then ( + if types <> [] then ( + F.pp_print_space fmt (); + Collections.List.iter_link (F.pp_print_space fmt) + (extract_ty ctx fmt no_params_tys true) + types); + if const_generics <> [] then ( + assert (!backend <> HOL4); + F.pp_print_space fmt (); + Collections.List.iter_link (F.pp_print_space fmt) + (extract_const_generic ctx fmt true) + const_generics)); if trait_refs <> [] then ( F.pp_print_space fmt (); Collections.List.iter_link (F.pp_print_space fmt) @@ -1588,6 +1596,93 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit = F.pp_print_string fmt rd; F.pp_close_box fmt () +let extract_trait_clause_type (ctx : extraction_ctx) (fmt : F.formatter) + (no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit = + let with_opaque_pre = false in + let trait_name = ctx_get_trait_decl with_opaque_pre clause.trait_id ctx in + F.pp_print_string fmt trait_name; + extract_generic_args ctx fmt no_params_tys clause.generics + +(** Insert a space, if necessary *) +let insert_req_space (fmt : F.formatter) (space : bool ref) : unit = + if !space then space := false else F.pp_print_space fmt () + +let extract_generic_params (ctx : extraction_ctx) (fmt : F.formatter) + (no_params_tys : TypeDeclId.Set.t) (use_forall : bool) (as_implicits : bool) + (space : bool ref option) (generics : generic_params) + (type_params : string list) (cg_params : string list) + (trait_clauses : string list) : unit = + let all_params = List.concat [ type_params; cg_params; trait_clauses ] in + (* HOL4 doesn't support const generics *) + assert (cg_params = [] || !backend <> HOL4); + let left_bracket () = + if as_implicits then F.pp_print_string fmt "{" + else F.pp_print_string fmt "(" + in + let right_bracket () = + if as_implicits then F.pp_print_string fmt "}" + else F.pp_print_string fmt ")" + in + let insert_req_space () = + match space with + | None -> F.pp_print_space fmt () + | Some space -> insert_req_space fmt space + in + (* Print the type/const generic parameters *) + if all_params <> [] then ( + if use_forall then ( + insert_req_space (); + F.pp_print_string fmt ":"; + F.pp_print_space fmt (); + F.pp_print_string fmt "forall"); + (* Note that in HOL4 we don't print the type parameters. *) + if !backend <> HOL4 then ( + (* Print the type parameters *) + if type_params <> [] then ( + insert_req_space (); + (* ( *) + left_bracket (); + List.iter + (fun s -> + F.pp_print_string fmt s; + F.pp_print_space fmt ()) + type_params; + F.pp_print_string fmt ":"; + F.pp_print_space fmt (); + F.pp_print_string fmt (type_keyword ()); + (* ) *) + right_bracket ()); + (* Print the const generic parameters *) + List.iter + (fun (var : const_generic_var) -> + insert_req_space (); + (* ( *) + left_bracket (); + let n = ctx_get_const_generic_var var.index ctx in + F.pp_print_string fmt n; + F.pp_print_space fmt (); + F.pp_print_string fmt ":"; + F.pp_print_space fmt (); + extract_literal_type ctx fmt var.ty; + (* ) *) + right_bracket ()) + generics.const_generics); + (* Print the trait clauses *) + List.iter + (fun (clause : trait_clause) -> + insert_req_space (); + (* ( *) + left_bracket (); + let n = ctx_get_trait_clause_var clause.clause_id ctx in + F.pp_print_string fmt n; + 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; + (* ) *) + right_bracket ()) + generics.trait_clauses) + (** Extract a type declaration. This function is for all type declarations and all backends **at the exception** @@ -1624,7 +1719,6 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) let ctx_body, type_params, cg_params, trait_clauses = ctx_add_generic_params def.generics ctx in - let all_params = List.concat [ type_params; cg_params; trait_clauses ] in (* Add a break before *) if !backend <> HOL4 || not (decl_is_first_from_group kind) then F.pp_print_break fmt 0 0; @@ -1644,40 +1738,13 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (match qualif with | Some qualif -> F.pp_print_string fmt (qualif ^ " " ^ def_name) | None -> F.pp_print_string fmt def_name); - (* HOL4 doesn't support const generics *) - assert (cg_params = [] || !backend <> HOL4); - (* Print the type/const generic parameters *) - if all_params <> [] && !backend <> HOL4 then ( - if use_forall then ( - F.pp_print_space fmt (); - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - F.pp_print_string fmt "forall"); - (* Print the type parameters *) - if type_params <> [] then ( - F.pp_print_space fmt (); - F.pp_print_string fmt "("; - List.iter - (fun s -> - F.pp_print_string fmt s; - F.pp_print_space fmt ()) - type_params; - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - F.pp_print_string fmt (type_keyword () ^ ")")); - (* Print the const generic parameters *) - List.iter - (fun (var : const_generic_var) -> - F.pp_print_space fmt (); - F.pp_print_string fmt "("; - let n = ctx_get_const_generic_var var.index ctx in - F.pp_print_string fmt n; - F.pp_print_space fmt (); - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - extract_literal_type ctx fmt var.ty; - F.pp_print_string fmt ")") - def.const_generic_params); + (* HOL4 doesn't support const generics, and type definitions in HOL4 don't + support trait clauses *) + assert ((cg_params = [] && trait_clauses = []) || !backend <> HOL4); + (* Print the generic parameters *) + let as_implicits = false in + extract_generic_params ctx_body fmt type_decl_group use_forall as_implicits + None def.generics type_params cg_params trait_clauses; (* Print the "=" if we extract the body*) if extract_body then ( F.pp_print_space fmt (); @@ -1737,9 +1804,12 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) let with_opaque_pre = false in let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in (* Generic parameters are unsupported *) - assert (def.const_generic_params = []); + assert (def.generics.const_generics = []); + (* Trait clauses on type definitions are unsupported *) + assert (def.generics.trait_clauses = []); + (* Types *) (* Count the number of parameters *) - let num_params = List.length def.type_params in + let num_params = List.length def.generics.types in (* Generate the declaration *) F.pp_print_space fmt (); F.pp_print_string fmt @@ -1760,8 +1830,7 @@ let extract_type_decl_hol4_empty_record (ctx : extraction_ctx) let with_opaque_pre = false in let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in (* Sanity check *) - assert (def.type_params = []); - assert (def.const_generic_params = []); + assert (def.generics = empty_generic_params); (* Generate the declaration *) F.pp_print_space fmt (); F.pp_print_string fmt ("Type " ^ def_name ^ " = “: unit”"); @@ -1801,13 +1870,12 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = assert (!backend = Coq); (* Generating the [Arguments] instructions is useful only if there are type parameters *) - if decl.type_params = [] && decl.const_generic_params = [] then () + if decl.generics.types = [] && decl.generics.const_generics = [] then () else (* Add the type params - note that we need those bindings only for the * body translation (they are not top-level) *) - let _ctx_body, type_params, cg_params = - ctx_add_type_const_generic_params decl.type_params - decl.const_generic_params ctx + let _ctx_body, type_params, cg_params, trait_clauses = + ctx_add_generic_params decl.generics ctx in (* Auxiliary function to extract an [Arguments Cons {T} _ _.] instruction *) let extract_arguments_info (cons_name : string) (fields : 'a list) : unit = @@ -1815,27 +1883,22 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_break fmt 0 0; (* Open a box *) F.pp_open_hovbox fmt ctx.indent_incr; - (* Small utility *) - let print_vars () = - List.iter - (fun (var : string) -> - F.pp_print_space fmt (); - F.pp_print_string fmt ("{" ^ var ^ "}")) - (List.append type_params cg_params) - in - let print_fields () = - List.iter - (fun _ -> - F.pp_print_space fmt (); - F.pp_print_string fmt "_") - fields - in F.pp_print_break fmt 0 0; F.pp_print_string fmt "Arguments"; F.pp_print_space fmt (); F.pp_print_string fmt cons_name; - print_vars (); - print_fields (); + (* Print the type/const params and the trait clauses (`{T}`) *) + List.iter + (fun (var : string) -> + F.pp_print_space fmt (); + F.pp_print_string fmt ("{" ^ var ^ "}")) + (List.concat [ type_params; cg_params; trait_clauses ]); + (* Print the fields (`_`) *) + List.iter + (fun _ -> + F.pp_print_space fmt (); + F.pp_print_string fmt "_") + fields; F.pp_print_string fmt "."; (* Close the box *) @@ -1888,9 +1951,8 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) let is_rec = decl_is_from_rec_group kind in if is_rec then (* Add the type params *) - let ctx, type_params, cg_params = - ctx_add_type_const_generic_params decl.type_params - decl.const_generic_params ctx + let ctx, type_params, cg_params, trait_clauses = + ctx_add_generic_params decl.generics ctx in let ctx, record_var = ctx_add_var "x" (VarId.of_int 0) ctx in let ctx, field_var = ctx_add_var "x" (VarId.of_int 1) ctx in @@ -1911,33 +1973,13 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) F.pp_print_space fmt (); let field_name = ctx_get_field (AdtId decl.def_id) field_id ctx in F.pp_print_string fmt field_name; - F.pp_print_space fmt (); - (* Print the type parameters *) - if type_params <> [] then ( - F.pp_print_string fmt "{"; - List.iter - (fun p -> - F.pp_print_string fmt p; - F.pp_print_space fmt ()) - type_params; - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - F.pp_print_string fmt "Type}"; - F.pp_print_space fmt ()); - (* Print the const generic parameters *) - if cg_params <> [] then - List.iter - (fun (v : const_generic_var) -> - F.pp_print_string fmt "{"; - let n = ctx_get_const_generic_var v.index ctx in - F.pp_print_string fmt n; - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - extract_literal_type ctx fmt v.ty; - F.pp_print_string fmt "}"; - F.pp_print_space fmt ()) - decl.const_generic_params; + (* Print the generics *) + let use_forall = false in + let as_implicits = true in + extract_generic_params ctx fmt TypeDeclId.Set.empty use_forall + as_implicits None decl.generics type_params cg_params trait_clauses; (* Print the record parameter *) + F.pp_print_space fmt (); F.pp_print_string fmt "("; F.pp_print_string fmt record_var; F.pp_print_space fmt (); @@ -2183,11 +2225,11 @@ let extract_adt_g_value (inside : bool) (variant_id : VariantId.id option) (field_values : 'v list) (ty : ty) : extraction_ctx = match ty with - | Adt (Tuple, type_args, cg_args) -> + | Adt (Tuple, generics) -> (* Tuple *) (* For now, we only support fully applied tuple constructors *) - assert (List.length type_args = List.length field_values); - assert (cg_args = []); + assert (List.length generics.types = List.length field_values); + assert (generics.const_generics = [] && generics.trait_refs = []); (* This is very annoying: in Coq, we can't write [()] for the value of type [unit], we have to write [tt]. *) if !backend = Coq && field_values = [] then ( @@ -2205,7 +2247,7 @@ let extract_adt_g_value in F.pp_print_string fmt ")"; ctx) - | Adt (adt_id, _, _) -> + | Adt (adt_id, _) -> (* "Regular" ADT *) (* If we are generating a pattern for a let-binding and we target Lean, @@ -2343,14 +2385,12 @@ 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.type_args - qualif.const_generic_args args + extract_function_call ctx fmt inside fun_id qualif.generics args | Global global_id -> extract_global ctx fmt global_id | AdtCons adt_cons_id -> - extract_adt_cons ctx fmt inside adt_cons_id qualif.type_args - qualif.const_generic_args args + extract_adt_cons ctx fmt inside adt_cons_id qualif.generics args | Proj proj -> - extract_field_projector ctx fmt inside app proj qualif.type_args args) + extract_field_projector ctx fmt inside app proj qualif.generics args) | _ -> (* "Regular" expression *) (* Open parentheses *) @@ -2373,8 +2413,8 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (** Subcase of the app case: function call *) and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) - (inside : bool) (fid : fun_or_op_id) (type_args : ty list) - (cg_args : const_generic list) (args : texpression list) : unit = + (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!). @@ -2396,19 +2436,9 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) let fun_name = ctx_get_function with_opaque_pre fun_id ctx in F.pp_print_string fmt fun_name; (* Sanity check: HOL4 doesn't support const generics *) - assert (cg_args = [] || !backend <> HOL4); - (* Print the type parameters, if the backend is not HOL4 *) - if !backend <> HOL4 then ( - List.iter - (fun ty -> - F.pp_print_space fmt (); - extract_ty ctx fmt TypeDeclId.Set.empty true ty) - type_args; - List.iter - (fun cg -> - F.pp_print_space fmt (); - extract_const_generic ctx fmt true cg) - cg_args); + assert (generics.const_generics = [] || !backend <> HOL4); + (* Print the generics *) + extract_generic_args ctx fmt TypeDeclId.Set.empty generics; (* Print the arguments *) List.iter (fun ve -> @@ -2430,9 +2460,9 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter) (** Subcase of the app case: ADT constructor *) and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) - (adt_cons : adt_cons_id) (type_args : ty list) - (cg_args : const_generic list) (args : texpression list) : unit = - let e_ty = Adt (adt_cons.adt_id, type_args, cg_args) in + (adt_cons : adt_cons_id) (generics : generic_args) (args : texpression list) + : unit = + let e_ty = Adt (adt_cons.adt_id, generics) in let is_single_pat = false in let _ = extract_adt_g_value @@ -2446,7 +2476,7 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (** 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) - (_proj_type_params : ty list) (args : texpression list) : unit = + (_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 @@ -2905,11 +2935,11 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter) let cs = ctx_get_struct false (Assumed Array) ctx in F.pp_print_string fmt cs; (* Print the parameters *) - let _, tys, cgs = ty_as_adt e_ty in - let ty = Collections.List.to_cons_nil tys in + let _, generics = ty_as_adt 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; - let cg = Collections.List.to_cons_nil cgs in + let cg = Collections.List.to_cons_nil generics.const_generics in F.pp_print_space fmt (); extract_const_generic ctx fmt true cg; F.pp_print_space fmt (); @@ -2936,10 +2966,6 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter) F.pp_close_box fmt () | _ -> raise (Failure "Unreachable") -(** Insert a space, if necessary *) -let insert_req_space (fmt : F.formatter) (space : bool ref) : unit = - if !space then space := false else F.pp_print_space fmt () - (** A small utility to print the parameters of a function signature. We return two contexts: @@ -2947,6 +2973,8 @@ let insert_req_space (fmt : F.formatter) (space : bool ref) : unit = - the context augmented with bindings for the type parameters *and* bindings for the input values + We also return names for the type parameters, const generics, etc. + TODO: do we really need the first one? We should probably always use the second one. It comes from the fact that when we print the input values for the @@ -2954,57 +2982,22 @@ let insert_req_space (fmt : F.formatter) (space : bool ref) : unit = patterns, not the variables). We should figure a cleaner way. *) let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx) - (fmt : F.formatter) (def : fun_decl) : extraction_ctx * extraction_ctx = + (fmt : F.formatter) (def : fun_decl) : + extraction_ctx * extraction_ctx * string list = (* 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 = - ctx_add_type_const_generic_params def.signature.type_params - def.signature.const_generic_params ctx + let ctx, type_params, cg_params, trait_clauses = + ctx_add_generic_params def.signature.generics ctx in - (* Print the parameters - rem.: we should have filtered the functions - * with no input parameters *) - (* The type parameters. - - Note that in HOL4 we don't print the type parameters. - *) - if (type_params <> [] || cg_params <> []) && !backend <> HOL4 then ( - (* Open a box for the type and const generic parameters *) - F.pp_open_hovbox fmt 0; - (* The type parameters *) - if type_params <> [] then ( - insert_req_space fmt space; - F.pp_print_string fmt "("; - List.iter - (fun (p : type_var) -> - let pname = ctx_get_type_var p.index ctx in - F.pp_print_string fmt pname; - F.pp_print_space fmt ()) - def.signature.type_params; - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - let type_keyword = - match !backend with - | FStar -> "Type0" - | Coq | Lean -> "Type" - | HOL4 -> raise (Failure "Unreachable") - in - F.pp_print_string fmt (type_keyword ^ ")")); - (* The const generic parameters *) - if cg_params <> [] then - List.iter - (fun (p : const_generic_var) -> - let pname = ctx_get_const_generic_var p.index ctx in - insert_req_space fmt space; - F.pp_print_string fmt "("; - F.pp_print_string fmt pname; - F.pp_print_space fmt (); - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - extract_literal_type ctx fmt p.ty; - F.pp_print_string fmt ")") - def.signature.const_generic_params; - (* Close the box for the type parameters *) - F.pp_close_box fmt ()); + (* Print the generics *) + (* Open a box for the generics *) + F.pp_open_hovbox fmt 0; + let use_forall = false in + let as_implicits = false in + extract_generic_params ctx fmt TypeDeclId.Set.empty use_forall as_implicits + (Some space) 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 *) let ctx_body = match def.body with @@ -3027,7 +3020,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx) ctx) ctx body.inputs_lvs in - (ctx, ctx_body) + (ctx, ctx_body, List.concat [ type_params; cg_params; trait_clauses ]) (** A small utility to print the types of the input parameters in the form: [u32 -> list u32 -> ...] @@ -3096,7 +3089,7 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx) F.pp_print_space fmt (); (* Extract the parameters *) let space = ref true in - let _, _ = extract_fun_parameters space ctx fmt def in + let _, _, _ = extract_fun_parameters space ctx fmt def in insert_req_space fmt space; F.pp_print_string fmt ":"; (* Print the signature *) @@ -3158,7 +3151,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) F.pp_print_space fmt (); (* Extract the parameters *) let space = ref true in - let _, ctx_body = extract_fun_parameters space ctx fmt def in + let _, ctx_body, _ = extract_fun_parameters space ctx fmt def in (* Print the ":=" *) F.pp_print_space fmt (); F.pp_print_string fmt ":="; @@ -3298,9 +3291,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) *) let is_opaque_coq = !backend = Coq && is_opaque in let use_forall = - is_opaque_coq - && (def.signature.type_params <> [] - || def.signature.const_generic_params <> []) + is_opaque_coq && def.signature.generics <> empty_generic_params in (* Print the qualifier ("assume", etc.). @@ -3326,7 +3317,7 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* Open a box for "(PARAMS) :" *) F.pp_open_hovbox fmt 0; let space = ref true in - let ctx, ctx_body = extract_fun_parameters space ctx fmt def in + let ctx, ctx_body, all_params = extract_fun_parameters space ctx fmt def in (* Print the return type - note that we have to be careful when * printing the input values for the decrease clause, because * it introduces bindings in the context... We thus "forget" @@ -3374,20 +3365,13 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* The name of the decrease clause *) let decr_name = ctx_get_termination_measure def.def_id def.loop_id ctx in F.pp_print_string fmt decr_name; - (* Print the type/const generic parameters - TODO: we do this many + (* Print the generic parameters - TODO: we do this many times, we should have a helper to factor it out *) List.iter - (fun (p : type_var) -> - let pname = ctx_get_type_var p.index ctx in - F.pp_print_space fmt (); - F.pp_print_string fmt pname) - def.signature.type_params; - List.iter - (fun (p : const_generic_var) -> - let pname = ctx_get_const_generic_var p.index ctx in + (fun (name : string) -> F.pp_print_space fmt (); - F.pp_print_string fmt pname) - def.signature.const_generic_params; + F.pp_print_string fmt name) + all_params; (* Print the input values: we have to be careful here to print * only the input values which are in common with the *forward* * function (the additional input values "given back" to the @@ -3474,19 +3458,12 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* Open the box for [DECREASES] *) F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt terminates_name; - (* Print the type/const generic params - TODO: factor out *) + (* Print the generic params - TODO: factor out *) List.iter - (fun (p : type_var) -> - let pname = ctx_get_type_var p.index ctx in + (fun (name : string) -> F.pp_print_space fmt (); - F.pp_print_string fmt pname) - def.signature.type_params; - List.iter - (fun (p : const_generic_var) -> - let pname = ctx_get_const_generic_var p.index ctx in - F.pp_print_space fmt (); - F.pp_print_string fmt pname) - def.signature.const_generic_params; + F.pp_print_string fmt name) + all_params; (* Print the variables *) List.iter (fun v -> @@ -3544,13 +3521,10 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) ctx_get_local_function with_opaque_pre def.def_id def.loop_id def.back_id ctx in - assert (def.signature.const_generic_params = []); + assert (def.signature.generics.const_generics = []); (* 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_type_const_generic_params def.signature.type_params - def.signature.const_generic_params ctx - in + let ctx, _, _, _ = ctx_add_generic_params def.signature.generics ctx in (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0; (* Open a box for the whole definition *) @@ -3726,10 +3700,9 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (global : A.global_decl) (body : fun_decl) (interface : bool) : unit = assert body.is_global_decl_body; assert (Option.is_none body.back_id); - assert (List.length body.signature.inputs = 0); + assert (body.signature.inputs = []); assert (List.length body.signature.doutputs = 1); - assert (List.length body.signature.type_params = 0); - assert (List.length body.signature.const_generic_params = 0); + 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; @@ -3799,8 +3772,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) (* Check if this is a unit function *) let sg = def.signature in if - sg.type_params = [] - && sg.const_generic_params = [] + sg.generics = empty_generic_params && (sg.inputs = [ mk_unit_ty ] || sg.inputs = []) && sg.output = mk_result_ty mk_unit_ty then ( diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 96ecfd42..2c704d3e 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -111,10 +111,10 @@ let decl_is_first_from_group (kind : decl_kind) : bool = let decl_is_not_last_from_group (kind : decl_kind) : bool = not (decl_is_last_from_group kind) -(* TODO: this should a module we give to a functor! *) - type type_decl_kind = Enum | Struct +(* TODO: this should be a module we give to a functor! *) + (** A formatter's role is twofold: 1. Come up with name suggestions. For instance, provided some information about a function (its basename, @@ -125,6 +125,9 @@ type type_decl_kind = Enum | Struct snake case, adding prefixes/suffixes, etc. 2. Format some specific terms, like constants. + + TODO: unclear that this is useful now that all the backends are so much + entangled in Extract.ml *) type formatter = { bool_name : string; @@ -288,6 +291,13 @@ type formatter = { (** Generates a type variable basename. *) const_generic_var_basename : StringSet.t -> string -> string; (** Generates a const generic variable basename. *) + trait_clause_basename : StringSet.t -> trait_clause -> string; + (** Return a base name for a trait clause. We might add a suffix to prevent + collisions. + + In the traduction we explicitely manipulate the trait clause instances, + that is we introduce one input variable for each trait clause. + *) append_index : string -> int -> string; (** Appends an index to a name - we use this to generate unique names: when doing so, the role of the formatter is just to concatenate @@ -396,6 +406,9 @@ type id = | TypeVarId of TypeVarId.id | ConstGenericVarId of ConstGenericVarId.id | VarId of VarId.id + | TraitDeclId of TraitDeclId.id + | TraitImplId of TraitImplId.id + | TraitClauseId of TraitClauseId.id | UnknownId (** Used for stored various strings like keywords, definitions which should always be in context, etc. and which can't be linked to one @@ -718,6 +731,9 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = | ConstGenericVarId id -> "const_generic_var_id: " ^ ConstGenericVarId.to_string id | VarId id -> "var_id: " ^ VarId.to_string id + | TraitDeclId id -> "trait_decl_id: " ^ TraitDeclId.to_string id + | TraitImplId id -> "trait_impl_id: " ^ TraitImplId.to_string id + | TraitClauseId id -> "trait_clause_id: " ^ TraitClauseId.to_string id (** We might not check for collisions for some specific ids (ex.: field names) *) let allow_collisions (id : id) : bool = @@ -787,6 +803,14 @@ let ctx_get_assumed_type (id : assumed_ty) (ctx : extraction_ctx) : string = let is_opaque = false in ctx_get_type is_opaque (Assumed id) ctx +let ctx_get_trait_decl (with_opaque_pre : bool) (id : trait_decl_id) + (ctx : extraction_ctx) : string = + ctx_get with_opaque_pre (TraitDeclId id) ctx + +let ctx_get_trait_impl (with_opaque_pre : bool) (id : trait_impl_id) + (ctx : extraction_ctx) : string = + ctx_get with_opaque_pre (TraitImplId id) ctx + let ctx_get_var (id : VarId.id) (ctx : extraction_ctx) : string = let is_opaque = false in ctx_get is_opaque (VarId id) ctx @@ -800,6 +824,11 @@ let ctx_get_const_generic_var (id : ConstGenericVarId.id) (ctx : extraction_ctx) let is_opaque = false in ctx_get is_opaque (ConstGenericVarId id) ctx +let ctx_get_trait_clause_var (id : TraitClauseId.id) (ctx : extraction_ctx) : + string = + let is_opaque = false in + ctx_get is_opaque (TraitClauseId id) ctx + let ctx_get_field (type_id : type_id) (field_id : FieldId.id) (ctx : extraction_ctx) : string = let is_opaque = false in @@ -865,6 +894,16 @@ let ctx_add_var (basename : string) (id : VarId.id) (ctx : extraction_ctx) : let ctx = ctx_add is_opaque (VarId id) name ctx in (ctx, name) +(** Generate a unique trait clause name and add it to the context *) +let ctx_add_trait_clause (basename : string) (id : TraitClauseId.id) + (ctx : extraction_ctx) : extraction_ctx * string = + let is_opaque = false in + let name = + basename_to_unique ctx.names_map.names_set ctx.fmt.append_index basename + in + let ctx = ctx_add is_opaque (TraitClauseId id) name ctx in + (ctx, name) + (** See {!ctx_add_var} *) let ctx_add_vars (vars : var list) (ctx : extraction_ctx) : extraction_ctx * string list = @@ -890,7 +929,9 @@ let ctx_add_const_generic_params (vars : const_generic_var list) let ctx_add_trait_clauses (clauses : trait_clause list) (ctx : extraction_ctx) : extraction_ctx * string list = List.fold_left_map - (fun ctx (c : trait_clause) -> ctx_add_trait_clause c ctx) + (fun ctx (c : trait_clause) -> + let basename = ctx.fmt.trait_clause_basename ctx.names_map.names_set c in + ctx_add_trait_clause basename c.clause_id ctx) ctx clauses (** Returns the lists of names for: |