From fc7d360e9442ab2e945e0d2da97faaf0eefec66f Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 19 Feb 2019 17:02:19 +0000
Subject: Refactor specialization

specialize functions now take a 'specialization' parameter that
specifies how they will specialize the AST. typ_ord_specialization
gives the previous behaviour, whereas int_specialization allows
specializing on Int-kinded arguments. Note that this can loop forever
unless the appropriate case splits are inserted beforehand, presumably
by monomorphisation.

rename is_nat_kopt -> is_int_kopt for consistency
---
 src/initial_check.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src/initial_check.ml')

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 07316c6d..003da64e 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -824,15 +824,15 @@ let val_spec_ids (Defs defs) =
   IdSet.of_list (vs_ids defs)
 
 let quant_item_param = function
-  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
+  | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
   | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [prepend_id "typ_" (id_of_kid (kopt_kid kopt))]
   | _ -> []
 let quant_item_typ = function
-  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [atom_typ (nvar (kopt_kid kopt))]
+  | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [atom_typ (nvar (kopt_kid kopt))]
   | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ (Typ_var (kopt_kid kopt))]
   | _ -> []
 let quant_item_arg = function
-  | QI_aux (QI_id kopt, _) when is_nat_kopt kopt -> [mk_typ_arg (A_nexp (nvar (kopt_kid kopt)))]
+  | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [mk_typ_arg (A_nexp (nvar (kopt_kid kopt)))]
   | QI_aux (QI_id kopt, _) when is_typ_kopt kopt -> [mk_typ_arg (A_typ (mk_typ (Typ_var (kopt_kid kopt))))]
   | _ -> []
 let undefined_typschm id typq =
-- 
cgit v1.2.3