Tidy up monomorphisation interface

3 files changed, 71 insertions, 7 deletions

diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 9ed5d799..72db4c9d 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -2591,14 +2591,14 @@ let mono_rewrite defs =
     defs
 end
 
-(* TODO: put in a proper mli for this stuff *)
 type options = {
   auto : bool;
   debug_analysis : int;
-  rewrites : bool
+  rewrites : bool;
+  rewrite_size_parameters : bool
 }
 
-let monomorphise mwords opts splits env defs =
+let monomorphise opts splits env defs =
   let (defs,env) =
     if opts.rewrites then
       let defs = MonoRewrites.mono_rewrite defs in
@@ -2615,7 +2615,7 @@ let monomorphise mwords opts splits env defs =
   (* TODO: currently doing this because constant propagation leaves numeric literals as
      int, try to avoid this later; also use final env for DEF_spec case above, because the
      type checker doesn't store the env at that point :( *)
-  if mwords then
+  if opts.rewrite_size_parameters then
     let (defs,env) = Type_check.check (Type_check.Env.no_casts Type_check.initial_env) defs in
     let defs = AtomToItself.rewrite_size_parameters env defs in
     defs
diff --git a/src/monomorphise.mli b/src/monomorphise.mli
new file mode 100644
index 00000000..39b4e244
--- /dev/null
+++ b/src/monomorphise.mli
@@ -0,0 +1,63 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+type options = {
+  auto : bool;                   (* Analyse ast to find splits for monomorphisation *)
+  debug_analysis : int;          (* Debug output level for the automatic analysis *)
+  rewrites : bool;               (* Experimental rewrites for variable-sized operations *)
+  rewrite_size_parameters : bool (* Make implicit type parameters explicit for (e.g.) lem *)
+}
+
+val monomorphise :
+  options ->
+  ((string * int) * string) list -> (* List of splits from the command line *)
+  Type_check.Env.t ->
+  Type_check.tannot Ast.defs ->
+  Type_check.tannot Ast.defs
diff --git a/src/process_file.ml b/src/process_file.ml
index 127a5aee..3755a83d 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -133,9 +133,10 @@ let monomorphise_ast locs type_env ast =
   let opts = {
     auto = !opt_auto_mono;
     debug_analysis = !opt_dmono_analysis;
-    rewrites = !opt_mono_rewrites } in
-  let ast = monomorphise (!Pretty_print_lem.opt_mwords) opts
-    locs type_env ast in
+    rewrites = !opt_mono_rewrites;
+    rewrite_size_parameters = !Pretty_print_lem.opt_mwords
+  } in
+  let ast = monomorphise opts locs type_env ast in
   let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in
   let ienv = Type_check.Env.no_casts Type_check.initial_env in
   Type_check.check ienv ast