summaryrefslogtreecommitdiff
path: root/src/ast_util.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-02-19 17:02:19 +0000
committerAlasdair Armstrong2019-02-19 17:02:19 +0000
commitfc7d360e9442ab2e945e0d2da97faaf0eefec66f (patch)
treea823d0c949dde68bdf117c836c3c2e28f9cf9088 /src/ast_util.ml
parent3c967f9075d890b8ba0e3fa1fb990a41a36ddd80 (diff)
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
Diffstat (limited to 'src/ast_util.ml')
-rw-r--r--src/ast_util.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index e4287249..8942b3b1 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -129,7 +129,7 @@ let mk_val_spec vs_aux =
let kopt_kid (KOpt_aux (KOpt_kind (_, kid), _)) = kid
let kopt_kind (KOpt_aux (KOpt_kind (k, _), _)) = k
-let is_nat_kopt = function
+let is_int_kopt = function
| KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> true
| _ -> false