summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/hol4/primitivesScript.sml181
-rw-r--r--backends/hol4/primitivesTheory.sig159
-rw-r--r--compiler/Extract.ml44
-rw-r--r--compiler/Translate.ml75
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