summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-09 13:06:30 +0100
committerSon Ho2022-02-09 13:06:30 +0100
commit056e6af4cf469dc9d72dff5222363edd9b563588 (patch)
treef1fdc83f772454f9b8cd0204af4dac551ed30276
parente161eb47d51a01e54a21c4517c85ef4c5525709e (diff)
Start implementing selection of the extracted definitions
-rw-r--r--src/Translate.ml86
1 files changed, 49 insertions, 37 deletions
diff --git a/src/Translate.ml b/src/Translate.ml
index da0b32a4..9d5d2b75 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -301,20 +301,24 @@ type gen_ctx = {
extract_ctx : PureToExtract.extraction_ctx;
trans_types : Pure.type_def Pure.TypeDefId.Map.t;
trans_funs : (bool * pure_fun_translation) Pure.FunDefId.Map.t;
- extract_types : bool;
functions_with_decrease_clause : Pure.FunDefId.Set.t;
+}
+(** Extraction context *)
+
+type gen_config = {
+ extract_types : bool;
extract_decrease_clauses : bool;
extract_template_decrease_clauses : bool;
- extract_functions : bool;
+ extract_fun_defs : bool;
test_unit_functions : bool;
}
-(** Extraction context *)
(** A generic utility to generate the extracted definitions: as we may want to
split the definitions between different files (or not), we can control
what is precisely extracted.
*)
-let extract_definitions (fmt : Format.formatter) (ctx : gen_ctx) : unit =
+let extract_definitions (fmt : Format.formatter) (config : gen_config)
+ (ctx : gen_ctx) : unit =
(* Export the definition groups to the file, in the proper order *)
let export_type (qualif : ExtractToFStar.type_def_qualif)
(id : Pure.TypeDefId.id) : unit =
@@ -327,7 +331,7 @@ let extract_definitions (fmt : Format.formatter) (ctx : gen_ctx) : unit =
*)
let export_functions (is_rec : bool)
(pure_ls : (bool * pure_fun_translation) list) : unit =
- (* Generate the function definitions, filtering the uselss forward
+ (* Concatenate the function definitions, filtering the useless forward
* functions. *)
let fls =
List.concat
@@ -336,28 +340,30 @@ let extract_definitions (fmt : Format.formatter) (ctx : gen_ctx) : unit =
if keep_fwd then fwd :: back_ls else back_ls)
pure_ls)
in
- (* Check if the functions are mutually recursive - this really works
- * to check if the forward and backward translations of a single
- * recursive function are mutually recursive *)
- let is_mut_rec =
- if is_rec then
- if List.length pure_ls <= 1 then
- not (PureUtils.functions_not_mutually_recursive fls)
- else true
- else false
- in
- List.iteri
- (fun i def ->
- let qualif =
- if not is_rec then ExtractToFStar.Let
- else if is_mut_rec then
- if i = 0 then ExtractToFStar.LetRec else ExtractToFStar.And
- else ExtractToFStar.LetRec
- in
- ExtractToFStar.extract_fun_def ctx.extract_ctx fmt qualif def)
- fls;
+ (* Extract the function definitions *)
+ (if config.extract_fun_defs then
+ (* Check if the functions are mutually recursive - this really works
+ * to check if the forward and backward translations of a single
+ * recursive function are mutually recursive *)
+ let is_mut_rec =
+ if is_rec then
+ if List.length pure_ls <= 1 then
+ not (PureUtils.functions_not_mutually_recursive fls)
+ else true
+ else false
+ in
+ List.iteri
+ (fun i def ->
+ let qualif =
+ if not is_rec then ExtractToFStar.Let
+ else if is_mut_rec then
+ if i = 0 then ExtractToFStar.LetRec else ExtractToFStar.And
+ else ExtractToFStar.LetRec
+ in
+ ExtractToFStar.extract_fun_def ctx.extract_ctx fmt qualif def)
+ fls);
(* Insert unit tests if necessary *)
- if ctx.test_unit_functions then
+ if config.test_unit_functions then
List.iter
(fun (keep_fwd, (fwd, _)) ->
if keep_fwd then
@@ -367,15 +373,17 @@ let extract_definitions (fmt : Format.formatter) (ctx : gen_ctx) : unit =
let export_decl (decl : M.declaration_group) : unit =
match decl with
- | Type (NonRec id) -> export_type ExtractToFStar.Type id
+ | Type (NonRec id) ->
+ if config.extract_types then export_type ExtractToFStar.Type id
| Type (Rec ids) ->
- List.iteri
- (fun i id ->
- let qualif =
- if i = 0 then ExtractToFStar.Type else ExtractToFStar.And
- in
- export_type qualif id)
- ids
+ if config.extract_types then
+ List.iteri
+ (fun i id ->
+ let qualif =
+ if i = 0 then ExtractToFStar.Type else ExtractToFStar.And
+ in
+ export_type qualif id)
+ ids
| Fun (NonRec id) ->
(* Lookup *)
let pure_fun = Pure.FunDefId.Map.find id ctx.trans_funs in
@@ -506,15 +514,19 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
extract_ctx = ctx;
trans_types;
trans_funs;
- extract_types = true;
functions_with_decrease_clause = rec_functions;
+ }
+ in
+ let gen_config =
+ {
+ extract_types = true;
extract_decrease_clauses = true;
extract_template_decrease_clauses = false;
- extract_functions = true;
+ extract_fun_defs = true;
test_unit_functions = config.test_unit_functions;
}
in
- extract_definitions fmt gen_ctx;
+ extract_definitions fmt gen_config gen_ctx;
(* Close the box and end the formatting *)
Format.pp_close_box fmt ();