diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | src/Translate.ml | 10 | ||||
| -rw-r--r-- | src/main.ml | 16 |
3 files changed, 28 insertions, 2 deletions
@@ -23,8 +23,8 @@ build: test: build translate-no_nested_borrows translate-hashmap # Add specific options to some tests -translate-no_nested_borrows: TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) +translate-no_nested_borrows: TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-decrease-clauses +translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses # Generic rule to extract the CFIM from a rust file .PHONY: gen-cfim-% diff --git a/src/Translate.ml b/src/Translate.ml index aa73ab7c..da0b32a4 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -24,6 +24,16 @@ type config = { let _ = assert_norm (FUNCTION () = Success ()) ``` *) + extract_decrease_clauses : bool; + (** If true, insert `decrease` clauses for all the recursive definitions. + + The body of such clauses must be defined by the user. + *) + extract_template_decrease_clauses : bool; + (** In order to help the user, we can generate "template" decrease clauses + (i.e., definitions with proper signatures but dummy bodies) in a + dedicated file. + *) } type symbolic_fun_translation = V.symbolic_value list * SA.expression diff --git a/src/main.ml b/src/main.ml index 2297f106..e0f16d8c 100644 --- a/src/main.ml +++ b/src/main.ml @@ -30,6 +30,8 @@ let () = let filter_useless_functions = ref true in let test_units = ref false in let test_trans_units = ref false in + let no_decrease_clauses = ref false in + let template_decrease_clauses = ref false in let spec = [ @@ -61,8 +63,20 @@ let () = Arg.Set test_trans_units, " Test the translated unit functions with the target theorem\n\ \ prover's normalizer" ); + ( "-no-decrease-clauses", + Arg.Set no_decrease_clauses, + " Do not add decrease clauses to the recursive definitions" ); + ( "-template-clauses", + Arg.Set template_decrease_clauses, + " Generate templates for the required decrease clauses, in a\n\ + `\n\ + \ dedicated file. Incompatible with \ + -no-decrease-clauses" ); ] in + (* Sanity check: -template-clauses ==> not -no-decrease-clauses *) + assert ((not !no_decrease_clauses) || not !template_decrease_clauses); + let spec = Arg.align spec in let filenames = ref [] in let add_filename f = filenames := f :: !filenames in @@ -156,6 +170,8 @@ let () = Translate.eval_config; mp_config = micro_passes_config; test_unit_functions; + extract_decrease_clauses = not !no_decrease_clauses; + extract_template_decrease_clauses = !template_decrease_clauses; } in Translate.translate_module filename dest_dir trans_config m |