diff options
| author | Alasdair Armstrong | 2019-02-19 17:02:19 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-02-19 17:02:19 +0000 |
| commit | fc7d360e9442ab2e945e0d2da97faaf0eefec66f (patch) | |
| tree | a823d0c949dde68bdf117c836c3c2e28f9cf9088 /src/initial_check.ml | |
| parent | 3c967f9075d890b8ba0e3fa1fb990a41a36ddd80 (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/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 = |