From fb88a51fbfd74482a4e5bcbada7c4c749db4d5ba Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 15 Apr 2019 14:15:09 +0100
Subject: SMT: Allow partial specializations

Change specialisation so we only specialize integer parameters when
they are constant. This makes ensures that the integer-specialised
code is always type-correct.
---
 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 05f675b2..7aee3dd0 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -79,7 +79,7 @@ let int_specialization = {
 
 let int_specialization_with_externs = {
     is_polymorphic = is_int_kopt;
-    instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false);
+    instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp (Nexp_aux (Nexp_constant _, _)), _) -> true | _ -> false);
     extern_filter = (fun _ -> false)
   }
 
@@ -391,7 +391,7 @@ let specialize_id_valspec spec instantiations id ast =
        let kopts, constraints = quant_split typq in
        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 kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt && KBindings.mem (kopt_kid kopt) safe_instantiation)) kopts in
        let typq =
          if List.length (typ_frees @ int_frees) = 0 && List.length kopts = 0 then
            mk_typquant []
-- 
cgit v1.2.3