summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-09 18:32:18 +0100
committerSon Ho2022-02-09 18:32:18 +0100
commit1f6798412509e0020f3ad468bfe91d3b15a7ce75 (patch)
tree01083cda8fd141bc4355de736353203986c3fb54
parentb6b77b38a16a102d3ccbc8bfad5a81a04eb3643d (diff)
Cleanup a bit
Diffstat (limited to '')
-rw-r--r--Makefile2
-rw-r--r--src/ExtractToFStar.ml57
-rw-r--r--src/PureToExtract.ml20
-rw-r--r--src/Translate.ml44
-rw-r--r--src/main.ml20
5 files changed, 58 insertions, 85 deletions
diff --git a/Makefile b/Makefile
index 33f98089..3d318ebc 100644
--- a/Makefile
+++ b/Makefile
@@ -23,7 +23,7 @@ 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 -no-split -no-decrease-clauses
+translate-no_nested_borrows: TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split -no-decreases-clauses
translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses
# Generic rule to extract the CFIM from a rust file
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index a481affd..83eaae9d 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -274,12 +274,12 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
fname ^ suffix
in
- let decrease_clause_name (_fid : FunDefId.id) (fname : name) : string =
+ let decreases_clause_name (_fid : FunDefId.id) (fname : name) : string =
let fname = get_fun_name fname in
(* Converting to snake case should be a no-op, but it doesn't cost much *)
let fname = to_snake_case fname in
(* Compute the suffix *)
- let suffix = "_decrease" in
+ let suffix = "_decreases" in
(* Concatenate *)
fname ^ suffix
in
@@ -352,7 +352,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) :
struct_constructor;
type_name;
fun_name;
- decrease_clause_name;
+ decreases_clause_name;
var_basename;
type_var_basename;
append_index;
@@ -644,11 +644,12 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter)
(forward function and backward functions).
*)
let extract_fun_def_register_names (ctx : extraction_ctx) (keep_fwd : bool)
- (has_decrease_clause : bool) (def : pure_fun_translation) : extraction_ctx =
+ (has_decreases_clause : bool) (def : pure_fun_translation) : extraction_ctx
+ =
let fwd, back_ls = def in
(* Register the decrease clause, if necessary *)
let ctx =
- if has_decrease_clause then ctx_add_decrase_clause fwd ctx else ctx
+ if has_decreases_clause then ctx_add_decrases_clause fwd ctx else ctx
in
(* Register the forward function name *)
let ctx = ctx_add_fun_def (keep_fwd, def) fwd ctx in
@@ -997,15 +998,15 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
let f_fwd (t : Type0) (x : t) : Tot ... (decreases (f_decrease t x)) = ...
```
*)
-let extract_template_decrease_clause (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
(def : fun_def) : unit =
(* Retrieve the function name *)
- let def_name = ctx_get_decrease_clause def.def_id ctx in
+ let def_name = ctx_get_decreases_clause def.def_id ctx in
(* Add a break before *)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
F.pp_print_string fmt
- ("(** [" ^ Print.name_to_string def.basename ^ "]: decrease clause *)");
+ ("(** [" ^ Print.name_to_string def.basename ^ "]: decreases clause *)");
F.pp_print_space fmt ();
(* Open a box for the definition, so that whenever possible it gets printed on
* one line - TODO: remove? *)
@@ -1043,7 +1044,7 @@ let extract_template_decrease_clause (ctx : extraction_ctx) (fmt : F.formatter)
it is useful for the decrease clause.
*)
let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
- (qualif : fun_def_qualif) (has_decrease_clause : bool) (fwd_def : fun_def)
+ (qualif : fun_def_qualif) (has_decreases_clause : bool) (fwd_def : fun_def)
(def : fun_def) : unit =
(* Retrieve the function name *)
let def_name = ctx_get_local_function def.def_id def.back_id ctx in
@@ -1066,36 +1067,6 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
in
F.pp_print_string fmt (qualif ^ " " ^ def_name);
let ctx, ctx_body = extract_fun_parameters ctx fmt def in
- (*(* Print the parameters - rk.: we should have filtered the functions
- * with no input parameters *)
- (* The type parameters *)
- if def.signature.type_params <> [] then (
- F.pp_print_space fmt ();
- 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 ();
- F.pp_print_string fmt "Type0)");
- (* The input parameters - note that doing this adds bindings to the context *)
- let ctx_body =
- List.fold_left
- (fun ctx (lv : typed_lvalue) ->
- F.pp_print_space fmt ();
- F.pp_print_string fmt "(";
- let ctx = extract_typed_lvalue ctx fmt false lv in
- F.pp_print_space fmt ();
- F.pp_print_string fmt ":";
- F.pp_print_space fmt ();
- extract_ty ctx fmt false lv.ty;
- F.pp_print_string fmt ")";
- ctx)
- ctx def.inputs_lvs
- in*)
(* Print the return type - note that we have to be careful when
* printing the input values for the decrease clause, because
* it introduces bindings in the context... We thus "forget"
@@ -1109,15 +1080,15 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt ":";
F.pp_print_space fmt ();
(* `Tot` *)
- if has_decrease_clause then (
+ if has_decreases_clause then (
F.pp_print_string fmt "Tot";
F.pp_print_space fmt ());
- extract_ty ctx fmt has_decrease_clause
+ extract_ty ctx fmt has_decreases_clause
(Collections.List.to_cons_nil def.signature.outputs);
(* Close the box for the return type *)
F.pp_close_box fmt ();
(* Print the decrease clause *)
- if has_decrease_clause then (
+ if has_decreases_clause then (
F.pp_print_space fmt ();
(* Open a box for the decrease clause *)
F.pp_open_hovbox fmt 0;
@@ -1126,7 +1097,7 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt "(";
(* The name of the decrease clause *)
- let decr_name = ctx_get_decrease_clause def.def_id ctx in
+ let decr_name = ctx_get_decreases_clause def.def_id ctx in
F.pp_print_string fmt decr_name;
(* Print the type parameters *)
List.iter
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 4d29d517..04f3c8b9 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -81,7 +81,7 @@ type formatter = {
(`None` if forward function)
TODO: use the fun id for the assumed functions.
*)
- decrease_clause_name : FunDefId.id -> name -> string;
+ decreases_clause_name : FunDefId.id -> name -> string;
(** Generates the name of the definition used to prove/reason about
termination. The generated code uses this clause where needed,
but its body must be defined by the user.
@@ -174,8 +174,8 @@ type formatter = {
(** We use identifiers to look for name clashes *)
type id =
| FunId of A.fun_id * RegionGroupId.id option
- | DecreaseClauseId of A.fun_id
- (** The definition which provides the decrease/termination clause.
+ | DecreasesClauseId of A.fun_id
+ (** The definition which provides the decreases/termination clause.
We insert calls to this clause to prove/reason about termination:
the body of those clauses must be defined by the user, in the
proper files.
@@ -337,14 +337,14 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
| Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id
in
"fun name (" ^ fun_kind ^ "): " ^ fun_name
- | DecreaseClauseId fid ->
+ | DecreasesClauseId fid ->
let fun_name =
match fid with
| A.Local fid ->
Print.name_to_string (FunDefId.Map.find fid fun_defs).name
| A.Assumed aid -> A.show_assumed_fun_id aid
in
- "decrease clause for function: " ^ fun_name
+ "decreases clause for function: " ^ fun_name
| TypeId id -> "type name: " ^ get_type_name id
| StructId id -> "struct constructor of: " ^ get_type_name id
| VariantId (id, variant_id) ->
@@ -446,9 +446,9 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id)
(ctx : extraction_ctx) : string =
ctx_get (VariantId (def_id, variant_id)) ctx
-let ctx_get_decrease_clause (def_id : FunDefId.id) (ctx : extraction_ctx) :
+let ctx_get_decreases_clause (def_id : FunDefId.id) (ctx : extraction_ctx) :
string =
- ctx_get (DecreaseClauseId (A.Local def_id)) ctx
+ ctx_get (DecreasesClauseId (A.Local def_id)) ctx
(** Generate a unique type variable name and add it to the context *)
let ctx_add_type_var (basename : string) (id : TypeVarId.id)
@@ -532,10 +532,10 @@ let ctx_add_struct (def : type_def) (ctx : extraction_ctx) :
let ctx = ctx_add (StructId (AdtId def.def_id)) name ctx in
(ctx, name)
-let ctx_add_decrase_clause (def : fun_def) (ctx : extraction_ctx) :
+let ctx_add_decrases_clause (def : fun_def) (ctx : extraction_ctx) :
extraction_ctx =
- let name = ctx.fmt.decrease_clause_name def.def_id def.basename in
- ctx_add (DecreaseClauseId (A.Local def.def_id)) name ctx
+ let name = ctx.fmt.decreases_clause_name def.def_id def.basename in
+ ctx_add (DecreasesClauseId (A.Local def.def_id)) name ctx
let ctx_add_fun_def (trans_group : bool * pure_fun_translation) (def : fun_def)
(ctx : extraction_ctx) : extraction_ctx =
diff --git a/src/Translate.ml b/src/Translate.ml
index 82b9f9cc..5a00db64 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -29,12 +29,12 @@ type config = {
let _ = assert_norm (FUNCTION () = Success ())
```
*)
- extract_decrease_clauses : bool;
- (** If true, insert `decrease` clauses for all the recursive definitions.
+ extract_decreases_clauses : bool;
+ (** If true, insert `decreases` clauses for all the recursive definitions.
The body of such clauses must be defined by the user.
*)
- extract_template_decrease_clauses : bool;
+ extract_template_decreases_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.
@@ -306,14 +306,14 @@ 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;
- functions_with_decrease_clause : Pure.FunDefId.Set.t;
+ functions_with_decreases_clause : Pure.FunDefId.Set.t;
}
(** Extraction context *)
type gen_config = {
extract_types : bool;
- extract_decrease_clauses : bool;
- extract_template_decrease_clauses : bool;
+ extract_decreases_clauses : bool;
+ extract_template_decreases_clauses : bool;
extract_fun_defs : bool;
test_unit_functions : bool;
}
@@ -332,8 +332,8 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
in
(* Utility to check a function has a decrease clause *)
- let has_decrease_clause (def : Pure.fun_def) : bool =
- Pure.FunDefId.Set.mem def.def_id ctx.functions_with_decrease_clause
+ let has_decreases_clause (def : Pure.fun_def) : bool =
+ Pure.FunDefId.Set.mem def.def_id ctx.functions_with_decreases_clause
in
(* In case of (non-mutually) recursive functions, we use a simple procedure to
@@ -353,12 +353,12 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
pure_ls)
in
(* Extract the decrease clauses template bodies *)
- if config.extract_template_decrease_clauses then
+ if config.extract_template_decreases_clauses then
List.iter
(fun (_, (fwd, _)) ->
- let has_decr_clause = has_decrease_clause fwd in
+ let has_decr_clause = has_decreases_clause fwd in
if has_decr_clause then
- ExtractToFStar.extract_template_decrease_clause ctx.extract_ctx fmt
+ ExtractToFStar.extract_template_decreases_clause ctx.extract_ctx fmt
fwd)
pure_ls;
(* Extract the function definitions *)
@@ -382,7 +382,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
else ExtractToFStar.LetRec
in
let has_decr_clause =
- has_decrease_clause def && config.extract_decrease_clauses
+ has_decreases_clause def && config.extract_decreases_clauses
in
ExtractToFStar.extract_fun_def ctx.extract_ctx fmt qualif
has_decr_clause fwd_def def)
@@ -571,7 +571,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
extract_ctx = ctx;
trans_types;
trans_funs;
- functions_with_decrease_clause = rec_functions;
+ functions_with_decreases_clause = rec_functions;
}
in
@@ -580,8 +580,8 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
let base_gen_config =
{
extract_types = false;
- extract_decrease_clauses = config.extract_decrease_clauses;
- extract_template_decrease_clauses = false;
+ extract_decreases_clauses = config.extract_decreases_clauses;
+ extract_template_decreases_clauses = false;
extract_fun_defs = false;
test_unit_functions = false;
}
@@ -596,15 +596,17 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(* Extract the template clauses *)
(if
- config.extract_decrease_clauses && config.extract_template_decrease_clauses
+ config.extract_decreases_clauses
+ && config.extract_template_decreases_clauses
then
let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in
let clauses_module = module_name ^ ".Clauses.Template" in
let clauses_config =
- { base_gen_config with extract_template_decrease_clauses = true }
+ { base_gen_config with extract_template_decreases_clauses = true }
in
extract_file clauses_config gen_ctx clauses_filename m.M.name
- clauses_module ": templates for the decrease clauses" [ types_module ] []);
+ clauses_module ": templates for the decreases clauses" [ types_module ]
+ []);
(* Extract the functions *)
let fun_filename = extract_filebasename ^ ".Funs.fst" in
@@ -624,9 +626,9 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
let gen_config =
{
extract_types = true;
- extract_decrease_clauses = config.extract_decrease_clauses;
- extract_template_decrease_clauses =
- config.extract_template_decrease_clauses;
+ extract_decreases_clauses = config.extract_decreases_clauses;
+ extract_template_decreases_clauses =
+ config.extract_template_decreases_clauses;
extract_fun_defs = true;
test_unit_functions = config.test_unit_functions;
}
diff --git a/src/main.ml b/src/main.ml
index fdd0576e..7bec093d 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -30,8 +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 no_decreases_clauses = ref false in
+ let template_decreases_clauses = ref false in
let no_split = ref false in
let spec =
@@ -64,15 +64,15 @@ 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,
+ ( "-no-decreases-clauses",
+ Arg.Set no_decreases_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\
+ Arg.Set template_decreases_clauses,
+ " Generate templates for the required decreases clauses, in a\n\
`\n\
\ dedicated file. Incompatible with \
- -no-decrease-clauses" );
+ -no-decreases-clauses" );
( "-no-split",
Arg.Set no_split,
" Don't split the definitions between different files for types, \
@@ -80,7 +80,7 @@ let () =
]
in
(* Sanity check: -template-clauses ==> not -no-decrease-clauses *)
- assert ((not !no_decrease_clauses) || not !template_decrease_clauses);
+ assert ((not !no_decreases_clauses) || not !template_decreases_clauses);
let spec = Arg.align spec in
let filenames = ref [] in
@@ -176,8 +176,8 @@ let () =
mp_config = micro_passes_config;
split_files = not !no_split;
test_unit_functions;
- extract_decrease_clauses = not !no_decrease_clauses;
- extract_template_decrease_clauses = !template_decrease_clauses;
+ extract_decreases_clauses = not !no_decreases_clauses;
+ extract_template_decreases_clauses = !template_decreases_clauses;
}
in
Translate.translate_module filename dest_dir trans_config m