diff options
| -rw-r--r-- | src/ExtractToFStar.ml | 17 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 31 | ||||
| -rw-r--r-- | src/Translate.ml | 17 |
3 files changed, 63 insertions, 2 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index a28d8c6d..9ad3c94c 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -274,6 +274,16 @@ 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 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 + (* Concatenate *) + fname ^ suffix + in + let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty) : string = (* If there is a basename, we use it *) @@ -342,6 +352,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : struct_constructor; type_name; fun_name; + decrease_clause_name; var_basename; type_var_basename; append_index; @@ -633,8 +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) - (def : pure_fun_translation) : extraction_ctx = + (has_decrease_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 + in (* Register the forward function name *) let ctx = ctx_add_fun_def (keep_fwd, def) fwd ctx in (* Register the backward functions' names *) diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index c61338b9..bb010a05 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -79,6 +79,17 @@ type formatter = { some of them) - region group information in case of a backward function (`None` if forward function) + TODO: use the fun id for the assumed functions. + *) + decrease_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. + + Inputs: + - function id: this is especially useful to identify whether the + function is an assumed function or a local function + - function basename *) var_basename : StringSet.t -> string option -> ty -> string; (** Generates a variable basename. @@ -163,6 +174,12 @@ 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. + 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. + *) | TypeId of type_id | StructId of type_id (** We use this when we manipulate the names of the structure @@ -320,6 +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 -> + 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 | TypeId id -> "type name: " ^ get_type_name id | StructId id -> "struct constructor of: " ^ get_type_name id | VariantId (id, variant_id) -> @@ -503,6 +528,11 @@ 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) : + 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 ctx_add_fun_def (trans_group : bool * pure_fun_translation) (def : fun_def) (ctx : extraction_ctx) : extraction_ctx = (* Lookup the CFIM def to compute the region group information *) @@ -531,6 +561,7 @@ let ctx_add_fun_def (trans_group : bool * pure_fun_translation) (def : fun_def) let name = ctx.fmt.fun_name def_id def.basename num_rgs rg_info (keep_fwd, num_backs) in + (* Add the function name *) let ctx = ctx_add (FunId (def_id, def.back_id)) name ctx in ctx diff --git a/src/Translate.ml b/src/Translate.ml index ba3effc5..8d9c0270 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -306,6 +306,16 @@ let translate_module (filename : string) (dest_dir : string) (config : config) { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 } in + (* We need to compute which functions are recursive, in order to know + * whether we should generate a decrease clause or not. *) + let rec_functions = + Pure.FunDefId.Set.of_list + (List.concat + (List.map + (fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> []) + m.declarations)) + in + (* Register unique names for all the top-level types and functions. * Note that the order in which we generate the names doesn't matter: * we just need to generate a mapping from identifier to name, and make @@ -320,7 +330,12 @@ let translate_module (filename : string) (dest_dir : string) (config : config) let extract_ctx = List.fold_left (fun extract_ctx (keep_fwd, def) -> - ExtractToFStar.extract_fun_def_register_names extract_ctx keep_fwd def) + (* Note that we generate a decrease clause for all the recursive functions *) + let gen_decr_clause = + Pure.FunDefId.Set.mem (fst def).Pure.def_id rec_functions + in + ExtractToFStar.extract_fun_def_register_names extract_ctx keep_fwd + gen_decr_clause def) extract_ctx trans_funs in |