summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml247
-rw-r--r--compiler/ExtractBase.ml14
2 files changed, 186 insertions, 75 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 3cb2be2c..bcfe4369 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1059,6 +1059,13 @@ let extract_const_generic (ctx : extraction_ctx) (fmt : F.formatter)
let s = ctx_get_const_generic_var id ctx in
F.pp_print_string fmt s
+let extract_literal_type (ctx : extraction_ctx) (fmt : F.formatter)
+ (ty : literal_type) : unit =
+ match ty with
+ | Bool -> F.pp_print_string fmt ctx.fmt.bool_name
+ | Char -> F.pp_print_string fmt ctx.fmt.char_name
+ | Integer int_ty -> F.pp_print_string fmt (ctx.fmt.int_name int_ty)
+
(** [inside] constrols whether we should add parentheses or not around type
applications (if [true] we add parentheses).
@@ -1132,6 +1139,8 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
cgs);
if print_paren then F.pp_print_string fmt ")"
| HOL4 ->
+ (* Const generics are unsupported in HOL4 *)
+ assert (cgs = []);
let print_tys =
match type_id with
| AdtId id -> not (TypeDeclId.Set.mem id no_params_tys)
@@ -1150,9 +1159,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ());
F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx)))
| TypeVar vid -> F.pp_print_string fmt (ctx_get_type_var vid ctx)
- | Literal Bool -> F.pp_print_string fmt ctx.fmt.bool_name
- | Literal Char -> F.pp_print_string fmt ctx.fmt.char_name
- | Literal (Integer int_ty) -> F.pp_print_string fmt (ctx.fmt.int_name int_ty)
+ | Literal lty -> extract_literal_type ctx fmt lty
| Arrow (arg_ty, ret_ty) ->
if inside then F.pp_print_string fmt "(";
extract_rec false arg_ty;
@@ -1202,8 +1209,8 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
(** Print the variants *)
let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter)
(type_decl_group : TypeDeclId.Set.t) (type_name : string)
- (type_params : string list) (cons_name : string) (fields : field list) :
- unit =
+ (type_params : string list) (cg_params : string list) (cons_name : string)
+ (fields : field list) : unit =
F.pp_print_space fmt ();
(* variant box *)
F.pp_open_hvbox fmt ctx.indent_incr;
@@ -1255,16 +1262,18 @@ let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter)
let _ =
List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
in
+ (* Sanity check: HOL4 doesn't support const generics *)
+ assert (cg_params = [] || !backend <> HOL4);
(* Print the final type *)
if !backend <> HOL4 then (
F.pp_print_space fmt ();
F.pp_open_hovbox fmt 0;
F.pp_print_string fmt type_name;
List.iter
- (fun type_param ->
+ (fun p ->
F.pp_print_space fmt ();
- F.pp_print_string fmt type_param)
- type_params;
+ F.pp_print_string fmt p)
+ (List.append type_params cg_params);
F.pp_close_box fmt ());
(* Close the variant box *)
F.pp_close_box fmt ()
@@ -1272,7 +1281,8 @@ let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter)
(* TODO: we don' need the [def_name] paramter: it can be retrieved from the context *)
let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
(type_decl_group : TypeDeclId.Set.t) (def : type_decl) (def_name : string)
- (type_params : string list) (variants : variant list) : unit =
+ (type_params : string list) (cg_params : string list)
+ (variants : variant list) : unit =
(* We want to generate a definition which looks like this (taking F* as example):
{[
type list a = | Cons : a -> list a -> list a | Nil : list a
@@ -1311,7 +1321,7 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
let cons_name = ctx.fmt.variant_name def.name v.variant_name in
let fields = v.fields in
extract_type_decl_variant ctx fmt type_decl_group def_name type_params
- cons_name fields
+ cg_params cons_name fields
in
(* Print the variants *)
let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in
@@ -1319,7 +1329,8 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
(type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl)
- (type_params : string list) (fields : field list) : unit =
+ (type_params : string list) (cg_params : string list) (fields : field list)
+ : unit =
(* We want to generate a definition which looks like this (taking F* as example):
{[
type t = { x : int; y : bool; }
@@ -1446,7 +1457,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
in
let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
extract_type_decl_variant ctx fmt type_decl_group def_name type_params
- cons_name fields)
+ cg_params cons_name fields)
in
()
@@ -1493,19 +1504,25 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
else None
in
(* If in Coq and the declaration is opaque, it must have the shape:
- [Axiom Ident : forall (T0 ... Tn : Type), ... -> ... -> ...].
+ [Axiom Ident : forall (T0 ... Tn : Type) (N0 : ...) ... (Nn : ...), ... -> ... -> ...].
The boolean [is_opaque_coq] is used to detect this case.
*)
let is_opaque = type_kind = None in
let is_opaque_coq = !backend = Coq && is_opaque in
- let use_forall = is_opaque_coq && def.type_params <> [] in
+ let use_forall =
+ is_opaque_coq && (def.type_params <> [] || def.const_generic_params <> [])
+ in
(* Retrieve the definition name *)
let with_opaque_pre = false in
let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
- (* Add the type params - note that we need those bindings only for the
+ (* 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_body, type_params = ctx_add_type_params def.type_params ctx in
+ let ctx_body, type_params, cg_params =
+ ctx_add_type_const_generic_params def.type_params def.const_generic_params
+ ctx
+ in
+ let ty_cg_params = List.append type_params cg_params in
(* Add a break before *)
if !backend <> HOL4 || not (decl_is_first_from_group kind) then
F.pp_print_break fmt 0 0;
@@ -1518,31 +1535,47 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(match !backend with
| Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0
| Lean -> F.pp_open_vbox fmt 0);
- (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *)
+ (* Open a box for "type TYPE_NAME (TYPE_PARAMS CONST_GEN_PARAMS) =" *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* > "type TYPE_NAME" *)
let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind in
(match qualif with
| Some qualif -> F.pp_print_string fmt (qualif ^ " " ^ def_name)
| None -> F.pp_print_string fmt def_name);
- (* Print the type parameters *)
- if def.type_params <> [] && !backend <> HOL4 then (
+ (* HOL4 doesn't support const generics *)
+ assert (cg_params = [] || !backend <> HOL4);
+ (* Print the type/const generic parameters *)
+ if ty_cg_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");
- F.pp_print_space fmt ();
- F.pp_print_string fmt "(";
+ (* 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 (p : type_var) ->
- let pname = ctx_get_type_var p.index ctx_body in
- F.pp_print_string fmt pname;
- F.pp_print_space fmt ())
- def.type_params;
- F.pp_print_string fmt ":";
- F.pp_print_space fmt ();
- F.pp_print_string fmt (type_keyword () ^ ")"));
+ (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);
(* Print the "=" if we extract the body*)
if extract_body then (
F.pp_print_space fmt ();
@@ -1571,10 +1604,10 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
match def.kind with
| Struct fields ->
extract_type_decl_struct_body ctx_body fmt type_decl_group kind def
- type_params fields
+ type_params cg_params fields
| Enum variants ->
extract_type_decl_enum_body ctx_body fmt type_decl_group def def_name
- type_params variants
+ type_params cg_params variants
| Opaque -> raise (Failure "Unreachable"));
(* Add the definition end delimiter *)
if !backend = HOL4 && decl_is_not_last_from_group kind then (
@@ -1601,6 +1634,8 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
(* Retrieve the definition name *)
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 = []);
(* Count the number of parameters *)
let num_params = List.length def.type_params in
(* Generate the declaration *)
@@ -1624,6 +1659,7 @@ let extract_type_decl_hol4_empty_record (ctx : extraction_ctx)
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 = []);
(* Generate the declaration *)
F.pp_print_space fmt ();
F.pp_print_string fmt ("Type " ^ def_name ^ " = “: unit”");
@@ -1663,11 +1699,14 @@ 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 = [] then ()
+ if decl.type_params = [] && decl.const_generic_params = [] 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 = ctx_add_type_params decl.type_params ctx in
+ let _ctx_body, type_params, cg_params =
+ ctx_add_type_const_generic_params decl.type_params
+ decl.const_generic_params ctx
+ in
(* Auxiliary function to extract an [Arguments Cons {T} _ _.] instruction *)
let extract_arguments_info (cons_name : string) (fields : 'a list) : unit =
(* Add a break before *)
@@ -1675,12 +1714,12 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Small utility *)
- let print_type_vars () =
+ let print_vars () =
List.iter
(fun (var : string) ->
F.pp_print_space fmt ();
F.pp_print_string fmt ("{" ^ var ^ "}"))
- type_params
+ (List.append type_params cg_params)
in
let print_fields () =
List.iter
@@ -1693,7 +1732,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt "Arguments";
F.pp_print_space fmt ();
F.pp_print_string fmt cons_name;
- print_type_vars ();
+ print_vars ();
print_fields ();
F.pp_print_string fmt ".";
@@ -1747,7 +1786,10 @@ 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 = ctx_add_type_params decl.type_params ctx in
+ let ctx, type_params, cg_params =
+ ctx_add_type_const_generic_params decl.type_params
+ decl.const_generic_params 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
let with_opaque_pre = false in
@@ -1780,6 +1822,19 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
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 record parameter *)
F.pp_print_string fmt "(";
F.pp_print_string fmt record_var;
@@ -1968,16 +2023,6 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
(* Add breaks to insert new lines between definitions *)
F.pp_print_break fmt 0 0
-(** In some provers like HOL4, we don't print the type parameters when calling
- functions (and the polymorphism is uniform...).
-
- TODO: we may want to check that the polymorphism is indeed uniform when
- generating code for such backends, and print at least a warning to the
- user when it is not the case.
- *)
-let print_fun_type_params () : bool =
- match !backend with FStar | Coq | Lean -> true | HOL4 -> false
-
(** Compute the names for all the pure functions generated from a rust function
(forward function and backward functions).
*)
@@ -2193,7 +2238,8 @@ 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 args
+ extract_function_call ctx fmt inside fun_id qualif.type_args
+ qualif.const_generic_args 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
@@ -2223,7 +2269,7 @@ 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)
- (args : texpression list) : unit =
+ (cg_args : const_generic list) (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!).
@@ -2244,13 +2290,20 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
let with_opaque_pre = ctx.use_opaque_pre in
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
+ 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);
(* Print the arguments *)
List.iter
(fun ve ->
@@ -2751,33 +2804,52 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
(fmt : F.formatter) (def : fun_decl) : extraction_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, _ = ctx_add_type_params def.signature.type_params ctx in
+ let ctx, type_params, cg_params =
+ ctx_add_type_const_generic_params def.signature.type_params
+ def.signature.const_generic_params 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 def.signature.type_params <> [] && !backend <> HOL4 then (
- (* Open a box for 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;
- 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 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 ());
(* The input parameters - note that doing this adds bindings to the context *)
@@ -3072,7 +3144,11 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
The boolean [is_opaque_coq] is used to detect this case.
*)
let is_opaque_coq = !backend = Coq && is_opaque in
- let use_forall = is_opaque_coq && def.signature.type_params <> [] in
+ let use_forall =
+ is_opaque_coq
+ && (def.signature.type_params <> []
+ || def.signature.const_generic_params <> [])
+ in
(* Print the qualifier ("assume", etc.).
if `wrap_opaque_in_sig`: we generate a record of assumed funcions.
@@ -3145,13 +3221,20 @@ 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 parameters *)
+ (* Print the type/const 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
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt pname)
+ def.signature.const_generic_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
@@ -3238,6 +3321,7 @@ 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 *)
List.iter
(fun (p : type_var) ->
let pname = ctx_get_type_var p.index ctx in
@@ -3245,6 +3329,13 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
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;
+ (* Print the variables *)
+ List.iter
(fun v ->
F.pp_print_space fmt ();
F.pp_print_string fmt (ctx_get_var v ctx_body))
@@ -3300,9 +3391,13 @@ 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
- (* Add the type parameters - note that we need those bindings only for the
- * generation of the type (they are not top-level) *)
- let ctx, _ = ctx_add_type_params def.signature.type_params ctx in
+ assert (def.signature.const_generic_params = []);
+ (* 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
(* Add breaks to insert new lines between definitions *)
F.pp_print_break fmt 0 0;
(* Open a box for the whole definition *)
@@ -3481,6 +3576,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
assert (List.length body.signature.inputs = 0);
assert (List.length body.signature.doutputs = 1);
assert (List.length body.signature.type_params = 0);
+ assert (List.length body.signature.const_generic_params = 0);
(* Add a break then the name of the corresponding LLBC declaration *)
F.pp_print_break fmt 0 0;
@@ -3551,6 +3647,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
let sg = def.signature in
if
sg.type_params = []
+ && sg.const_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 3ba507a6..d733c763 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -878,6 +878,20 @@ let ctx_add_type_params (vars : type_var list) (ctx : extraction_ctx) :
(fun ctx (var : type_var) -> ctx_add_type_var var.name var.index ctx)
ctx vars
+let ctx_add_const_generic_params (vars : const_generic_var list)
+ (ctx : extraction_ctx) : extraction_ctx * string list =
+ List.fold_left_map
+ (fun ctx (var : const_generic_var) ->
+ ctx_add_const_generic_var var.name var.index ctx)
+ ctx vars
+
+let ctx_add_type_const_generic_params (tvars : type_var list)
+ (cgvars : const_generic_var list) (ctx : extraction_ctx) :
+ extraction_ctx * string list * string list =
+ let ctx, tys = ctx_add_type_params tvars ctx in
+ let ctx, cgs = ctx_add_const_generic_params cgvars ctx in
+ (ctx, tys, cgs)
+
let ctx_add_type_decl_struct (def : type_decl) (ctx : extraction_ctx) :
extraction_ctx * string =
assert (match def.kind with Struct _ -> true | _ -> false);
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 19:24:34 +0000