diff options
Diffstat (limited to '')
| -rw-r--r-- | src/ExtractToFStar.ml | 26 | ||||
| -rw-r--r-- | src/Translate.ml | 46 |
2 files changed, 60 insertions, 12 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 1f59075a..9d96d058 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -1192,7 +1192,7 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) *) let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) (qualif : fun_decl_qualif) (has_decreases_clause : bool) - (fwd_def : fun_decl) (def : fun_decl) : unit = + (has_state_param : bool) (fwd_def : fun_decl) (def : fun_decl) : unit = (* Retrieve the function name *) let def_name = ctx_get_local_function def.def_id def.back_id ctx in (* (* Add the type parameters - note that we need those bindings only for the @@ -1279,12 +1279,30 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter) * backward functions have no influence on termination: we thus * share the decrease clauses between the forward and the backward * functions). + * Something annoying is that there may be a state parameter, for + * the state-error monad, in which case we need to forget the input + * parameter before last: + * ``` + * val f_fwd (x : u32) (st : state) : + * Tot (result (state & u32)) (decreases (f_decreases x st)) + * + * We ignore this parameter + * VVV + * val f_back (x : u32) (ret : u32) (st : state) : + * Tot (result (state & u32)) (decreases (f_decreases x st)) + * ``` * Rk.: if a function has a decreases clause, it is necessarily * a transparent function *) let inputs_lvs = - Collections.List.prefix - (List.length (Option.get fwd_def.body).inputs_lvs) - (Option.get def.body).inputs_lvs + let num_fwd_inputs = List.length (Option.get fwd_def.body).inputs_lvs in + let num_fwd_inputs = + if has_state_param then num_fwd_inputs - 1 else num_fwd_inputs + in + let all_inputs = (Option.get def.body).inputs_lvs in + let inputs = Collections.List.prefix num_fwd_inputs all_inputs in + if has_state_param then + inputs @ [ List.nth all_inputs (List.length all_inputs - 1) ] + else inputs in let _ = List.fold_left diff --git a/src/Translate.ml b/src/Translate.ml index 29f8f5ba..c29dd963 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -347,6 +347,7 @@ type gen_ctx = { (** Extraction context *) type gen_config = { + mp_config : Micro.config; extract_types : bool; extract_decreases_clauses : bool; extract_template_decreases_clauses : bool; @@ -470,13 +471,19 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config) let has_decr_clause = has_decreases_clause def && config.extract_decreases_clauses in + (* Is there an input parameter "visible" for the state used in + * the state error monad (if we use a state error monad)? *) + let has_state_param = + config.mp_config.use_state_monad + && config.mp_config.unfold_monadic_let_bindings + in (* Check if the definition needs to be filtered or not *) if ((not is_opaque) && config.extract_transparent) || (is_opaque && config.extract_opaque) then ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif - has_decr_clause fwd_def def) + has_decr_clause has_state_param fwd_def def) fls); (* Insert unit tests if necessary *) if config.test_unit_functions then @@ -579,7 +586,10 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) Format.pp_print_newline fmt (); (* Some logging *) - log#linfo (lazy ("Generated: " ^ filename)) + log#linfo (lazy ("Generated: " ^ filename)); + + (* Flush and close the file *) + close_out out (** Translate a module and write the synthesized code to an output file. TODO: rename to translate_crate @@ -665,6 +675,30 @@ let translate_module (filename : string) (dest_dir : string) (config : config) trans_funs) in + (* Create the directory, if necessary *) + if not (Sys.file_exists dest_dir) then ( + log#linfo (lazy ("Creating missing directory: " ^ dest_dir)); + (* Create a directory with *default* permissions *) + Core.Unix.mkdir_p dest_dir); + + (* Copy "Primitives.fst" - I couldn't find a "cp" function in the OCaml + * libraries... *) + let _ = + let src = open_in "fstar/Primitives.fst" in + let tgt_filename = Filename.concat dest_dir "Primitives.fst" in + let tgt = open_out tgt_filename in + try + while true do + (* We copy line by line *) + let line = input_line src in + Printf.fprintf tgt "%s\n" line + done + with End_of_file -> + close_in src; + close_out tgt; + log#linfo (lazy ("Copied: " ^ tgt_filename)) + in + (* Extract the file(s) *) let gen_ctx = { @@ -676,18 +710,13 @@ let translate_module (filename : string) (dest_dir : string) (config : config) } in - (* Create the directory, if necessary *) - if not (Sys.file_exists dest_dir) then ( - log#linfo (lazy ("Creating missing directory: " ^ dest_dir)); - (* Create a directory with *default* permissions *) - Core.Unix.mkdir_p dest_dir); - let use_state = config.mp_config.use_state_monad in (* Extract one or several files, depending on the configuration *) if config.split_files then ( let base_gen_config = { + mp_config = config.mp_config; extract_types = false; extract_decreases_clauses = config.extract_decreases_clauses; extract_template_decreases_clauses = false; @@ -776,6 +805,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) else let gen_config = { + mp_config = config.mp_config; extract_types = true; extract_decreases_clauses = config.extract_decreases_clauses; extract_template_decreases_clauses = |