From 8718a39778d4c673ceea1c7f9bb219b29788ebae Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Tue, 5 Mar 2019 03:09:16 +0000
Subject: Additional optimizations for C compilation

---
 src/specialize.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'src/specialize.ml')

diff --git a/src/specialize.ml b/src/specialize.ml
index 19c5df7a..a487fc2f 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -52,6 +52,8 @@ open Ast
 open Ast_util
 open Rewriter
 
+let opt_ddump_spec_ast = ref None
+   
 let is_typ_ord_arg = function
   | A_aux (A_typ _, _) -> true
   | A_aux (A_order _, _) -> true
@@ -565,6 +567,15 @@ let specialize_ids spec ids ast =
       (1, ast) (IdSet.elements ids)
   in
   let ast = reorder_typedefs ast in
+  begin match !opt_ddump_spec_ast with
+  | Some (f, i) ->
+     let filename = f ^ "_spec_" ^ string_of_int i ^ ".sail" in
+     let out_chan = open_out filename in
+     Pretty_print_sail.pp_defs out_chan ast;
+     close_out out_chan;
+     opt_ddump_spec_ast := Some (f, i + 1)
+  | None -> ()
+  end;
   let ast, _ = Type_error.check Type_check.initial_env ast in
   let ast =
     List.fold_left (fun ast id -> rewrite_polymorphic_calls spec id ast) ast (IdSet.elements ids)
-- 
cgit v1.2.3


From 2cd88a225adf5f382df85a046cd59c43e1436965 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Tue, 5 Mar 2019 23:54:07 +0000
Subject: Fix missing case in specialization

---
 src/specialize.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/specialize.ml')

diff --git a/src/specialize.ml b/src/specialize.ml
index a487fc2f..e2ab3c68 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -337,7 +337,8 @@ and remove_implicit_arg (A_aux (aux, l)) =
 let kopt_arg = function
   | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid), _) -> arg_nexp (nvar kid)
   | KOpt_aux (KOpt_kind (K_aux (K_type,_), kid), _) -> arg_typ (mk_typ (Typ_var kid))
-  | _ -> failwith "oh no"
+  | KOpt_aux (KOpt_kind (K_aux (K_bool, _), kid), _) -> arg_bool (nc_var kid)
+  | KOpt_aux (KOpt_kind (K_aux (K_order, _), kid), _) -> arg_order (mk_ord (Ord_var kid))
 
 (* For numeric type arguments we have to be careful not to run into a
    situation where we have an instantiation like
-- 
cgit v1.2.3


From 711de1e76e82026e361f232010304175f0542c3d Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 11 Mar 2019 13:03:07 +0000
Subject: Improve ocamldoc comments

Check in a slightly nicer stylesheet for OCamldoc generated
documentation in etc. Most just add a maximum width and increase the
font size because the default looks absolutely terrible on high-DPI
monitors.

Move val_spec_ids out of initial_check and into ast_util where it
probably belongs. Rename some functions in util.ml to better match the
OCaml stdlib.
---
 src/specialize.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/specialize.ml')

diff --git a/src/specialize.ml b/src/specialize.ml
index e2ab3c68..afce4b0f 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -256,7 +256,7 @@ let rec instantiations_of spec id ast =
   !instantiations
 
 let rec rewrite_polymorphic_calls spec id ast =
-  let vs_ids = Initial_check.val_spec_ids ast in
+  let vs_ids = val_spec_ids ast in
 
   let rewrite_e_aux = function
     | E_aux (E_app (id', args), annot) as exp when Id.compare id id' = 0 ->
@@ -495,7 +495,7 @@ let initial_calls = IdSet.of_list
 
 let remove_unused_valspecs ?(initial_calls=initial_calls) env ast =
   let calls = ref initial_calls in
-  let vs_ids = Initial_check.val_spec_ids ast in
+  let vs_ids = val_spec_ids ast in
 
   let inspect_exp = function
     | E_aux (E_app (call, _), _) as exp ->
-- 
cgit v1.2.3