diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ocaml_backend.ml | 10 | ||||
| -rw-r--r-- | src/sail.ml | 12 |
2 files changed, 14 insertions, 8 deletions
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 51c9638a..0da745ae 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -649,9 +649,9 @@ let val_spec_typs (Defs defs) = !typs let orig_types_for_ocaml_generator (Defs defs) = - Some (Util.map_filter (function + Util.map_filter (function | DEF_type td -> Some td - | _ -> None) defs) + | _ -> None) defs let ocaml_pp_generators ctx defs orig_types required = let add_def typemap td = @@ -852,7 +852,7 @@ required separate hardline (List.map make_rand_gen (IdSet.elements required)) ^^ rand_record_pp -let ocaml_defs (Defs defs) generator_types = +let ocaml_defs (Defs defs) generator_info = let ctx = { register_inits = get_initialize_registers defs; externs = get_externs (Defs defs); val_specs = val_spec_typs (Defs defs) @@ -866,9 +866,9 @@ let ocaml_defs (Defs defs) generator_types = else empty in let gen_pp = - match generator_types with + match generator_info with | None -> empty - | Some types -> ocaml_pp_generators ctx defs types [mk_id "ast"] + | Some (types, req) -> ocaml_pp_generators ctx defs types (List.map mk_id req) in (string "open Sail_lib;;" ^^ hardline) ^^ (string "module Big_int = Nat_big_num" ^^ ocaml_def_end) diff --git a/src/sail.ml b/src/sail.ml index b535d1d3..9526d6fe 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -71,6 +71,7 @@ let opt_libs_lem = ref ([]:string list) let opt_libs_coq = ref ([]:string list) let opt_file_arguments = ref ([]:string list) let opt_process_elf : string option ref = ref None +let opt_ocaml_generators = ref ([]:string list) let options = Arg.align ([ ( "-o", @@ -104,6 +105,9 @@ let options = Arg.align ([ ( "-ocaml-coverage", Arg.Set Ocaml_backend.opt_ocaml_coverage, " Build ocaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx)."); + ( "-ocaml_generators", + Arg.String (fun s -> opt_ocaml_generators := s::!opt_ocaml_generators), + "<types> produce random generators for the given types"); ( "-latex", Arg.Set opt_print_latex, " pretty print the input to latex"); @@ -299,8 +303,10 @@ let main() = | None, _ -> () end; - let orig_types_for_ocaml_generator = - Ocaml_backend.orig_types_for_ocaml_generator ast + let ocaml_generator_info = + match !opt_ocaml_generators with + | [] -> None + | _ -> Some (Ocaml_backend.orig_types_for_ocaml_generator ast, !opt_ocaml_generators) in (*let _ = Printf.eprintf "Type checked, next to pretty print" in*) @@ -321,7 +327,7 @@ let main() = then let ast_ocaml = rewrite_ast_ocaml ast in let out = match !opt_file_out with None -> "out" | Some s -> s in - Ocaml_backend.ocaml_compile out ast_ocaml orig_types_for_ocaml_generator + Ocaml_backend.ocaml_compile out ast_ocaml ocaml_generator_info else ()); (if !(opt_print_c) then |