From fc9e071bb633fd7c7241db79146934e4ab2b33b5 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 22 Feb 2019 16:58:58 +0000
Subject: Fix more bugs in int-specialization

---
 src/sail.ml       |  1 +
 src/specialize.ml | 12 ++++++++----
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/sail.ml b/src/sail.ml
index eaf96eb4..bd953992 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -407,6 +407,7 @@ let main() =
        then
          let ast_c = rewrite_ast_c type_envs ast in
          let ast_c, type_envs = Specialize.(specialize typ_ord_specialization ast_c type_envs) in
+         (* let ast_c, type_envs = Specialize.(specialize' 2 int_specialization ast_c type_envs) in *)
          (* let ast_c = Spec_analysis.top_sort_defs ast_c in *)
          Util.opt_warnings := true;
          C_backend.compile_ast (C_backend.initial_ctx type_envs) (!opt_includes_c) ast_c
diff --git a/src/specialize.ml b/src/specialize.ml
index f34dc85f..591a415a 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -380,10 +380,14 @@ let specialize_id_valspec spec instantiations id ast =
        let constraints = instantiate_constraints safe_instantiation constraints in
        let constraints = instantiate_constraints reverse constraints in
        let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt)) kopts in
-       let typq = mk_typquant (List.map (mk_qi_id K_type) typ_frees
-                               @ List.map (mk_qi_id K_int) int_frees
-                               @ List.map mk_qi_kopt kopts
-                               @ List.map mk_qi_nc constraints) in
+       let typq =
+         if List.length (typ_frees @ int_frees) = 0 && List.length kopts = 0 then
+           mk_typquant []
+         else
+           mk_typquant (List.map (mk_qi_id K_type) typ_frees
+                        @ List.map (mk_qi_id K_int) int_frees
+                        @ List.map mk_qi_kopt kopts
+                        @ List.map mk_qi_nc constraints) in
        let typschm = mk_typschm typq typ in
 
        let spec_id = id_of_instantiation id instantiation in
-- 
cgit v1.2.3