diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 57 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 20 | ||||
| -rw-r--r-- | src/Translate.ml | 44 | ||||
| -rw-r--r-- | src/main.ml | 20 |
5 files changed, 58 insertions, 85 deletions
@@ -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 |