diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 181 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 159 | ||||
| -rw-r--r-- | compiler/Extract.ml | 44 | ||||
| -rw-r--r-- | compiler/Translate.ml | 75 |
4 files changed, 378 insertions, 81 deletions
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 4a1f5fdd..8cd54f33 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -1661,6 +1661,9 @@ val vec_to_list_num_bounds = new_axiom ("vec_to_list_num_bounds", “!v. (0:num) <= LENGTH (vec_to_list v) /\ LENGTH (vec_to_list v) <= Num usize_max”) +val mk_vec_axiom = new_axiom ("mk_vec_axiom", + “∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l”) + Theorem update_len: ∀ls i y. len (update ls i y) = len ls Proof @@ -1732,41 +1735,61 @@ Proof fs [] QED -val vec_index_def = Define ‘ - vec_index i v = - if usize_to_int i ≤ usize_to_int (vec_len v) - then Return (index (usize_to_int i) (vec_to_list v)) - else Fail Failure’ +Definition vec_new_def: + vec_new = mk_vec [] +End -val mk_vec_axiom = new_axiom ("mk_vec_axiom", - “∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l”) +Theorem vec_to_list_vec_new: + vec_to_list vec_new = [] +Proof + fs [vec_new_def] >> + sg_dep_rewrite_all_tac mk_vec_axiom >> fs [len_def] >> + assume_tac usize_bounds >> fs [u16_max_def] >> int_tac +QED +val _ = BasicProvers.export_rewrites ["vec_to_list_vec_new"] -(* A custom unfolding theorem for evaluation *) +Theorem vec_len_vec_new: + vec_len vec_new = int_to_usize 0 +Proof + fs [vec_len_def, vec_new_def] >> + sg_dep_rewrite_all_tac usize_to_int_int_to_usize >> fs [len_def, u16_max_def] >> + assume_tac usize_bounds >> fs [u16_max_def] >> int_tac +QED +val _ = BasicProvers.export_rewrites ["vec_len_vec_new"] + +(* A custom unfolding theorem for evaluation - we compare to “u16_max” rather + than “usize_max” on purpose. *) Theorem mk_vec_unfold: - ∀l. vec_to_list (mk_vec l) = if len l ≤ usize_max then l else vec_to_list (mk_vec l) + ∀l. vec_to_list (mk_vec l) = if len l ≤ u16_max then l else vec_to_list (mk_vec l) Proof + rw [] >> Cases_on ‘len l ≤ u16_max’ >> fs [] >> + assume_tac usize_bounds >> + sg ‘len l ≤ usize_max’ >- int_tac >> metis_tac [mk_vec_axiom] QED val _ = evalLib.add_unfold_thm "mk_vec_unfold" -(* Defining ‘vec_insert_back’ *) -val vec_insert_back_def = Define ‘ - vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = - if usize_to_int i < usize_to_int (vec_len v) then - Return (mk_vec (update (vec_to_list v) (usize_to_int i) x)) - else Fail Failure’ +(* Helper *) +Definition vec_index_def: + vec_index v i = index (usize_to_int i) (vec_to_list v) +End -Theorem vec_insert_back_spec: - ∀v i x. - usize_to_int i < usize_to_int (vec_len v) ⇒ - ∃ nv. vec_insert_back v i x = Return nv ∧ - vec_len v = vec_len nv ∧ - vec_index i nv = Return x ∧ - (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ - usize_to_int j ≠ usize_to_int i ⇒ - vec_index j nv = vec_index j v) -Proof - rpt strip_tac >> fs [vec_insert_back_def] >> +(* Helper *) +Definition vec_update_def: + vec_update v i x = mk_vec (update (vec_to_list v) (usize_to_int i) x) +End + +Theorem vec_update_eq: + ∀ v i x. + usize_to_int i < usize_to_int (vec_len v) ⇒ + let nv = vec_update v i x in + vec_len v = vec_len nv ∧ + vec_index nv i = x ∧ + (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ + usize_to_int j ≠ usize_to_int i ⇒ + vec_index nv j = vec_index v j) +Proof + rpt strip_tac >> fs [vec_update_def] >> qspec_assume ‘update (vec_to_list v) (usize_to_int i) x’ mk_vec_axiom >> sg_dep_rewrite_all_tac update_len >> fs [] >> qspec_assume ‘v’ vec_len_spec >> gvs [] >> @@ -1778,4 +1801,110 @@ Proof sg_dep_rewrite_all_tac index_update_same >- cooper_tac >> fs [] QED +Definition vec_index_fwd_def: + vec_index_fwd v i = + if usize_to_int i ≤ usize_to_int (vec_len v) + then Return (vec_index v i) + else Fail Failure +End + +Definition vec_index_back_def: + vec_index_back v i = + if usize_to_int i < usize_to_int (vec_len v) then Return () else Fail Failure +End + +Definition vec_index_mut_fwd_def: + vec_index_mut_fwd v i = + if usize_to_int i ≤ usize_to_int (vec_len v) + then Return (vec_index v i) + else Fail Failure +End + +Definition vec_index_mut_back_def: + vec_index_mut_back v i x = + if usize_to_int i ≤ usize_to_int (vec_len v) + then Return (vec_update v i x) + else Fail Failure +End + +Theorem vec_index_fwd_spec: + ∀v i. + usize_to_int i < usize_to_int (vec_len v) ⇒ + vec_index_fwd v i = Return (vec_index v i) +Proof + rw [vec_index_fwd_def] +QED + +Theorem vec_index_back_spec: + ∀v i. + usize_to_int i < usize_to_int (vec_len v) ⇒ + vec_index_back v i = Return () +Proof + rw [vec_index_back_def] +QED + +Theorem vec_index_mut_fwd_spec: + ∀v i. + usize_to_int i < usize_to_int (vec_len v) ⇒ + vec_index_mut_fwd v i = Return (vec_index v i) +Proof + rw [vec_index_mut_fwd_def] +QED + +Theorem vec_index_mut_back_spec: + ∀v i x. + usize_to_int i < usize_to_int (vec_len v) ⇒ + vec_index_mut_back v i x = Return (vec_update v i x) +Proof + rw [vec_index_mut_back_def] +QED + +Definition vec_insert_back_def: + vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = + if usize_to_int i < usize_to_int (vec_len v) then + Return (vec_update v i x) + else Fail Failure +End + +Theorem vec_insert_back_spec: + ∀v i x. + usize_to_int i < usize_to_int (vec_len v) ⇒ + vec_insert_back v i x = Return (vec_update v i x) +Proof + rw [vec_insert_back_def] +QED + +Definition vec_push_back_def: + vec_push_back (v : 'a vec) (x : 'a) : ('a vec) result = + if usize_to_int (vec_len v) < usize_max then + Return (mk_vec ((vec_to_list v) ++ [x])) + else Fail Failure +End + +Theorem vec_push_back_unfold: + ∀ v x. vec_push_back (v : 'a vec) (x : 'a) : ('a vec) result = + if usize_to_int (vec_len v) < u16_max ∨ usize_to_int (vec_len v) < usize_max then + Return (mk_vec ((vec_to_list v) ++ [x])) + else Fail Failure +Proof + assume_tac usize_bounds >> + rw [vec_push_back_def] >> fs [] >> + int_tac +QED +val _ = evalLib.add_unfold_thm "vec_push_back_unfold" + +Theorem vec_push_back_spec: + ∀ v x. + usize_to_int (vec_len v) < usize_max ⇒ + ∃ nv. vec_push_back v x = Return nv ∧ + vec_to_list nv = vec_to_list v ++ [x] +Proof + rw [vec_push_back_def, vec_len_def] >> + qspec_assume ‘v’ vec_len_spec >> + sg_dep_rewrite_all_tac usize_to_int_int_to_usize >- int_tac >> fs [] >> + sg_dep_rewrite_all_tac mk_vec_axiom + >- (fs [len_append, len_def, vec_len_def] >> int_tac) >> + fs [] +QED + val _ = export_theory () diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index 45caf234..2407e2f2 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -201,9 +201,16 @@ sig val usize_mul_def : thm val usize_rem_def : thm val usize_sub_def : thm + val vec_index_back_def : thm val vec_index_def : thm + val vec_index_fwd_def : thm + val vec_index_mut_back_def : thm + val vec_index_mut_fwd_def : thm val vec_insert_back_def : thm val vec_len_def : thm + val vec_new_def : thm + val vec_push_back_def : thm + val vec_update_def : thm (* Theorems *) val datatype_error : thm @@ -327,9 +334,18 @@ sig val usize_rem_eq : thm val usize_sub_eq : thm val usize_to_int_int_to_usize_unfold : thm + val vec_index_back_spec : thm + val vec_index_fwd_spec : thm + val vec_index_mut_back_spec : thm + val vec_index_mut_fwd_spec : thm val vec_insert_back_spec : thm val vec_len_spec : thm + val vec_len_vec_new : thm + val vec_push_back_spec : thm + val vec_push_back_unfold : thm val vec_to_list_int_bounds : thm + val vec_to_list_vec_new : thm + val vec_update_eq : thm val primitives_grammars : type_grammar.grammar * term_grammar.grammar (* @@ -1285,12 +1301,39 @@ sig ⊢ ∀x y. usize_sub x y = mk_usize (usize_to_int x − usize_to_int y) + [vec_index_back_def] Definition + + ⊢ ∀v i. + vec_index_back v i = + if usize_to_int i < usize_to_int (vec_len v) then Return () + else Fail Failure + [vec_index_def] Definition - ⊢ ∀i v. - vec_index i v = + ⊢ ∀v i. vec_index v i = index (usize_to_int i) (vec_to_list v) + + [vec_index_fwd_def] Definition + + ⊢ ∀v i. + vec_index_fwd v i = + if usize_to_int i ≤ usize_to_int (vec_len v) then + Return (vec_index v i) + else Fail Failure + + [vec_index_mut_back_def] Definition + + ⊢ ∀v i x. + vec_index_mut_back v i x = + if usize_to_int i ≤ usize_to_int (vec_len v) then + Return (vec_update v i x) + else Fail Failure + + [vec_index_mut_fwd_def] Definition + + ⊢ ∀v i. + vec_index_mut_fwd v i = if usize_to_int i ≤ usize_to_int (vec_len v) then - Return (index (usize_to_int i) (vec_to_list v)) + Return (vec_index v i) else Fail Failure [vec_insert_back_def] Definition @@ -1298,13 +1341,31 @@ sig ⊢ ∀v i x. vec_insert_back v i x = if usize_to_int i < usize_to_int (vec_len v) then - Return (mk_vec (update (vec_to_list v) (usize_to_int i) x)) + Return (vec_update v i x) else Fail Failure [vec_len_def] Definition ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) + [vec_new_def] Definition + + ⊢ vec_new = mk_vec [] + + [vec_push_back_def] Definition + + ⊢ ∀v x. + vec_push_back v x = + if usize_to_int (vec_len v) < usize_max then + Return (mk_vec (vec_to_list v ⧺ [x])) + else Fail Failure + + [vec_update_def] Definition + + ⊢ ∀v i x. + vec_update v i x = + mk_vec (update (vec_to_list v) (usize_to_int i) x) + [datatype_error] Theorem ⊢ DATATYPE (error Failure) @@ -1851,9 +1912,9 @@ sig [mk_vec_unfold] Theorem - [oracles: DISK_THM] [axioms: mk_vec_axiom] [] + [oracles: DISK_THM] [axioms: mk_vec_axiom, usize_bounds] [] ⊢ ∀l. vec_to_list (mk_vec l) = - if len l ≤ usize_max then l else vec_to_list (mk_vec l) + if len l ≤ u16_max then l else vec_to_list (mk_vec l) [num2error_11] Theorem @@ -2295,20 +2356,35 @@ sig if 0 ≤ n ∧ n ≤ u16_max then n else usize_to_int (int_to_usize n) + [vec_index_back_spec] Theorem + + ⊢ ∀v i. + usize_to_int i < usize_to_int (vec_len v) ⇒ + vec_index_back v i = Return () + + [vec_index_fwd_spec] Theorem + + ⊢ ∀v i. + usize_to_int i < usize_to_int (vec_len v) ⇒ + vec_index_fwd v i = Return (vec_index v i) + + [vec_index_mut_back_spec] Theorem + + ⊢ ∀v i x. + usize_to_int i < usize_to_int (vec_len v) ⇒ + vec_index_mut_back v i x = Return (vec_update v i x) + + [vec_index_mut_fwd_spec] Theorem + + ⊢ ∀v i. + usize_to_int i < usize_to_int (vec_len v) ⇒ + vec_index_mut_fwd v i = Return (vec_index v i) + [vec_insert_back_spec] Theorem - [oracles: DISK_THM] - [axioms: vec_to_list_num_bounds, usize_bounds, - int_to_usize_usize_to_int, usize_to_int_bounds, - usize_to_int_int_to_usize, mk_vec_axiom] [] ⊢ ∀v i x. usize_to_int i < usize_to_int (vec_len v) ⇒ - ∃nv. - vec_insert_back v i x = Return nv ∧ vec_len v = vec_len nv ∧ - vec_index i nv = Return x ∧ - ∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ - usize_to_int j ≠ usize_to_int i ⇒ - vec_index j nv = vec_index j v + vec_insert_back v i x = Return (vec_update v i x) [vec_len_spec] Theorem @@ -2318,11 +2394,62 @@ sig ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) ∧ 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max + [vec_len_vec_new] Theorem + + [oracles: DISK_THM] + [axioms: mk_vec_axiom, int_to_usize_usize_to_int, + usize_to_int_int_to_usize, usize_bounds] [] + ⊢ vec_len vec_new = int_to_usize 0 + + [vec_push_back_spec] Theorem + + [oracles: DISK_THM] + [axioms: usize_to_int_int_to_usize, mk_vec_axiom, + int_to_usize_usize_to_int, usize_bounds, vec_to_list_num_bounds] [] + ⊢ ∀v x. + usize_to_int (vec_len v) < usize_max ⇒ + ∃nv. + vec_push_back v x = Return nv ∧ + vec_to_list nv = vec_to_list v ⧺ [x] + + [vec_push_back_unfold] Theorem + + [oracles: DISK_THM] [axioms: usize_bounds] [] + ⊢ ∀v x. + vec_push_back v x = + if + usize_to_int (vec_len v) < u16_max ∨ + usize_to_int (vec_len v) < usize_max + then + Return (mk_vec (vec_to_list v ⧺ [x])) + else Fail Failure + [vec_to_list_int_bounds] Theorem [oracles: DISK_THM] [axioms: usize_bounds, vec_to_list_num_bounds] [] ⊢ ∀v. 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max + [vec_to_list_vec_new] Theorem + + [oracles: DISK_THM] [axioms: mk_vec_axiom, usize_bounds] [] + ⊢ vec_to_list vec_new = [] + + [vec_update_eq] Theorem + + [oracles: DISK_THM] + [axioms: vec_to_list_num_bounds, usize_bounds, + int_to_usize_usize_to_int, usize_to_int_bounds, + usize_to_int_int_to_usize, mk_vec_axiom] [] + ⊢ ∀v i x. + usize_to_int i < usize_to_int (vec_len v) ⇒ + (let + nv = vec_update v i x + in + vec_len v = vec_len nv ∧ vec_index nv i = x ∧ + ∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ + usize_to_int j ≠ usize_to_int i ⇒ + vec_index nv j = vec_index v j) + *) end diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 7e4aeab4..d624d9ca 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -249,7 +249,7 @@ let assumed_adts () : (assumed_ty * string) list = (Result, "result"); (Error, "error"); (Fuel, "num"); - (Option, "OPTION"); + (Option, "option"); (Vec, "vec"); ]) @@ -1532,7 +1532,7 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter) (* Generate the declaration *) F.pp_print_space fmt (); F.pp_print_string fmt - ("val _ = new_type (\"" ^ def_name ^ ", " ^ string_of_int num_params ^ ")"); + ("val _ = new_type (\"" ^ def_name ^ "\", " ^ string_of_int num_params ^ ")"); F.pp_print_space fmt () (** Extract an empty record type declaration to HOL4. @@ -1874,7 +1874,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) F.pp_print_space fmt (); F.pp_print_string fmt "Type0" | HOL4 -> - F.pp_print_string fmt ("val _ = new_type (" ^ state_name ^ ", 0)") + F.pp_print_string fmt ("val _ = new_type (\"" ^ state_name ^ "\", 0)") | Coq | Lean -> print_axiom ()) | Declared -> ( match !backend with @@ -1887,7 +1887,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) F.pp_print_space fmt (); F.pp_print_string fmt "Type0" | HOL4 -> - F.pp_print_string fmt ("val _ = new_type (" ^ state_name ^ ", 0)") + F.pp_print_string fmt ("val _ = new_type (\"" ^ state_name ^ "\", 0)") | Coq | Lean -> print_axiom ())); (* Close the box for the definition *) F.pp_close_box fmt (); @@ -3158,26 +3158,34 @@ let extract_fun_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_function with_opaque_pre def.def_id None None ctx + 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 + (* Add breaks to insert new lines between definitions *) + F.pp_print_break fmt 0 0; (* Open a box for the whole definition *) - F.pp_open_hovbox fmt ctx.indent_incr; + F.pp_open_hvbox fmt ctx.indent_incr; (* Generate: `val _ = new_constant ("...",` *) - F.pp_print_string fmt ("val _ = new_constant (\"" ^ def_name ^ ", "); + F.pp_print_string fmt ("val _ = new_constant (\"" ^ def_name ^ "\","); + F.pp_print_space fmt (); (* Open a box for the type *) - F.pp_open_hvbox fmt 0; + F.pp_open_hovbox fmt 0; + F.pp_print_string fmt "“:"; (* Generate the type *) extract_fun_input_parameters_types ctx fmt def; extract_ty ctx fmt TypeDeclId.Set.empty false def.signature.output; (* Close the box for the type *) + F.pp_print_string fmt "”"; F.pp_close_box fmt (); (* Close the parenthesis opened for the inputs of `new_constant` *) F.pp_print_string fmt ")"; (* Close the box for the definition *) - F.pp_close_box fmt () + F.pp_close_box fmt (); + (* Add breaks to insert new lines between definitions *) + F.pp_print_break fmt 0 0 (** Extract a function declaration. @@ -3211,6 +3219,15 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) (extract_body : (F.formatter -> unit) Option.t) : unit = let is_opaque = Option.is_none extract_body in + (* HOL4: Definition wrapper *) + if !backend = HOL4 then ( + (* Open a vertical box: we *must* break lines *) + F.pp_open_vbox fmt 0; + F.pp_print_string fmt ("Definition " ^ name ^ "_def:"); + F.pp_print_space fmt (); + F.pp_open_vbox fmt ctx.indent_incr; + F.pp_print_string fmt (String.make ctx.indent_incr ' ')); + (* Open the definition boxes (depth=0) *) F.pp_open_hvbox fmt 0; F.pp_open_hvbox fmt ctx.indent_incr; @@ -3267,7 +3284,14 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "."); (* Close the outer definition box (depth=0) *) - F.pp_close_box fmt () + F.pp_close_box fmt (); + + (* HOL4: Definition wrapper *) + if !backend = HOL4 then ( + F.pp_close_box fmt (); + F.pp_print_space fmt (); + F.pp_print_string fmt "End"; + F.pp_close_box fmt ()) (** Extract an opaque global declaration for HOL4. diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 1107a123..75fc7fe9 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -567,36 +567,51 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config) (odd (i : num) : bool result = if i = 0 then Return F else even (i - 1)) ` ]} + + TODO: in practice splitting the code this way doesn't work so well: merge + the start/end decl group functions with the extract_fun_decl function? *) - Extract.start_fun_decl_group ctx.extract_ctx fmt is_rec decls; - List.iteri - (fun i def -> - let is_opaque = Option.is_none def.Pure.body in - let kind = - if is_opaque then - if config.interface then ExtractBase.Declared else ExtractBase.Assumed - else if not is_rec then ExtractBase.SingleNonRec - else if is_mut_rec then - (* If the functions are mutually recursive, we need to distinguish: - * - the first of the group - * - the last of the group - * - the inner functions - *) - if i = 0 then ExtractBase.MutRecFirst - else if i = decls_length - 1 then ExtractBase.MutRecLast - else ExtractBase.MutRecInner - else ExtractBase.SingleRec - in - let has_decr_clause = - has_decreases_clause def && config.extract_decreases_clauses - in - (* Check if the definition needs to be filtered or not *) - if - ((not is_opaque) && config.extract_transparent) - || (is_opaque && config.extract_opaque) - then Extract.extract_fun_decl ctx.extract_ctx fmt kind has_decr_clause def) - decls; - Extract.end_fun_decl_group fmt is_rec decls + (* Filter the definitions - we generate a list of continuations *) + let extract_defs = + List.mapi + (fun i def -> + let is_opaque = Option.is_none def.Pure.body in + let kind = + if is_opaque then + if config.interface then ExtractBase.Declared + else ExtractBase.Assumed + else if not is_rec then ExtractBase.SingleNonRec + else if is_mut_rec then + (* If the functions are mutually recursive, we need to distinguish: + * - the first of the group + * - the last of the group + * - the inner functions + *) + if i = 0 then ExtractBase.MutRecFirst + else if i = decls_length - 1 then ExtractBase.MutRecLast + else ExtractBase.MutRecInner + else ExtractBase.SingleRec + in + let has_decr_clause = + has_decreases_clause def && config.extract_decreases_clauses + in + (* Check if the definition needs to be filtered or not *) + if + ((not is_opaque) && config.extract_transparent) + || (is_opaque && config.extract_opaque) + then + Some + (fun () -> + Extract.extract_fun_decl ctx.extract_ctx fmt kind has_decr_clause + def) + else None) + decls + in + let extract_defs = List.filter_map (fun x -> x) extract_defs in + if extract_defs <> [] then ( + Extract.start_fun_decl_group ctx.extract_ctx fmt is_rec decls; + List.iter (fun f -> f ()) extract_defs; + Extract.end_fun_decl_group fmt is_rec decls) (** Export a group of function declarations. @@ -828,6 +843,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) Printf.fprintf out "open primitivesLib divDefLib\n"; (* Add the custom imports and includes *) let imports = custom_imports @ custom_includes in + (* The imports are a list of module names: we need to add a "Theory" suffix *) + let imports = List.map (fun s -> s ^ "Theory") imports in if imports <> [] then let imports = String.concat " " imports in Printf.fprintf out "open %s\n\n" imports |