summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--editors/sail2-mode.el6
-rw-r--r--language/sail.ott21
-rw-r--r--src/ast_util.ml4
-rw-r--r--src/initial_check.ml4
-rw-r--r--src/monomorphise.ml4
-rw-r--r--src/parse_ast.ml2
-rw-r--r--src/parser.mly2
-rw-r--r--src/pretty_print_lem_ast.ml2
-rw-r--r--src/rewrites.ml4
-rw-r--r--src/specialize.ml4
-rw-r--r--src/type_check.ml48
11 files changed, 51 insertions, 50 deletions
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index 9eefa654..43be664d 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -8,7 +8,8 @@
"else" "match" "in" "return" "register" "ref" "forall" "operator" "effect"
"overload" "cast" "sizeof" "constraint" "default" "assert" "newtype" "from"
"pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to"
- "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield"))
+ "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield"
+ "mapping"))
(defconst sail2-kinds
'("Int" "Type" "Order" "inc" "dec"
@@ -16,7 +17,7 @@
"exmem" "undef" "unspec" "nondet" "escape"))
(defconst sail2-types
- '("vector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string" "bits"
+ '("vector" "int" "nat" "atom" "range" "unit" "bit" "real" "list" "bool" "string" "bits" "option"
"uint64_t" "int64_t" "bv_t" "mpz_t"))
(defconst sail2-special
@@ -28,6 +29,7 @@
(,(regexp-opt sail2-types 'symbols) . font-lock-type-face)
(,(regexp-opt sail2-special 'symbols) . font-lock-preprocessor-face)
("~" . font-lock-negation-char-face)
+ ("<->" . font-lock-negation-char-face)
("\'[a-zA-Z0-9_]+" . font-lock-variable-name-face)
("\\([a-zA-Z0-9_]+\\)(" 1 font-lock-function-name-face)
("function \\([a-zA-Z0-9_]+\\)" 1 font-lock-function-name-face)
diff --git a/language/sail.ott b/language/sail.ott
index a437f915..ded3938b 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -177,21 +177,20 @@ kid :: '' ::=
grammar
-base_kind :: 'BK_' ::=
+base_kind :: 'BK_' ::=
{{ com base kind}}
{{ aux _ l }}
- | Type :: :: type {{ com kind of types }}
- | Nat :: :: nat {{ com kind of natural number size expressions }}
- | Order :: :: order {{ com kind of vector order specifications }}
+ | Type :: :: type {{ com kind of types }}
+ | Int :: :: int {{ com kind of natural number size expressions }}
+ | Order :: :: order {{ com kind of vector order specifications }}
-
-kind :: 'K_' ::=
+kind :: 'K_' ::=
{{ com kinds}}
{{ aux _ l }}
- | base_kind1 -> ... -> base_kindn :: :: kind
+ | base_kind1 -> ... -> base_kindn :: :: kind
% we'll never use ...-> Nat , .. Order , .. or Effects
-
-nexp :: 'Nexp_' ::=
+
+nexp :: 'Nexp_' ::=
{{ com numeric expression, of kind $[[Nat]]$ }}
{{ aux _ l }}
| id :: :: id {{ com abbreviation identifier }}
@@ -292,7 +291,7 @@ typ_arg :: 'Typ_arg_' ::=
{{ aux _ l }}
| nexp :: :: nexp
| typ :: :: typ
- | order :: :: order
+ | order :: :: order
% plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations ... ref typ
@@ -344,7 +343,7 @@ quant_item :: 'QI_' ::=
{{ com kinded identifier or $[[Nat]]$ constraint }}
{{ aux _ l }}
| kinded_id :: :: id {{ com optionally kinded identifier }}
- | n_constraint :: :: const {{ com $[[Nat]]$ constraint }}
+ | n_constraint :: :: const {{ com $[[Nat]]$ constraint }}
typquant :: 'TypQ_' ::=
{{ com type quantifiers and constraints}}
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 09fc9fc9..e003a1bc 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -122,7 +122,7 @@ let kopt_kid (KOpt_aux (kopt_aux, _)) =
| KOpt_none kid | KOpt_kind (_, kid) -> kid
let is_nat_kopt = function
- | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), _), _) -> true
+ | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_int, _)], _), _), _) -> true
| KOpt_aux (KOpt_none _, _) -> true
| _ -> false
@@ -528,7 +528,7 @@ let string_of_base_effect_aux = function
let string_of_base_kind_aux = function
| BK_type -> "Type"
- | BK_nat -> "Int"
+ | BK_int -> "Int"
| BK_order -> "Order"
let string_of_base_kind (BK_aux (bk, _)) = string_of_base_kind_aux bk
diff --git a/src/initial_check.ml b/src/initial_check.ml
index b8c70e57..c6bc5fbe 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -149,7 +149,7 @@ let to_ast_var (Parse_ast.Kid_aux(Parse_ast.Var v,l)) = Kid_aux(Var v,l)
let to_ast_base_kind (Parse_ast.BK_aux(k,l')) =
match k with
| Parse_ast.BK_type -> BK_aux(BK_type,l'), { k = K_Typ}
- | Parse_ast.BK_nat -> BK_aux(BK_nat,l'), { k = K_Nat }
+ | Parse_ast.BK_int -> BK_aux(BK_int,l'), { k = K_Nat }
| Parse_ast.BK_order -> BK_aux(BK_order,l'), { k = K_Ord }
let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),l)) : (Ast.kind * kind) =
@@ -1123,7 +1123,7 @@ let generate_enum_functions vs_ids (Defs defs) =
if IdSet.mem name vs_ids then []
else
[ enum_val_spec name
- [mk_qi_id BK_nat kid; mk_qi_nc (range_constraint kid)]
+ [mk_qi_id BK_int kid; mk_qi_nc (range_constraint kid)]
(function_typ (atom_typ (nvar kid)) (mk_typ (Typ_id id)) no_effect);
mk_fundef [funcl] ]
in
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index f417d292..06841bdf 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -734,7 +734,7 @@ let reduce_cast typ exp l annot =
let typ' = Env.base_typ_of env typ in
match exp, destruct_exist env typ' with
| E_aux (E_lit (L_aux (L_num n,_)),_), Some ([kid],nc,typ'') when atom_typ_kid kid typ'' ->
- let nc_env = Env.add_typ_var kid BK_nat env in
+ let nc_env = Env.add_typ_var kid BK_int env in
let nc_env = Env.add_constraint (nc_eq (nvar kid) (nconstant n)) nc_env in
if prove nc_env nc
then exp
@@ -3841,7 +3841,7 @@ let fill_in_type env typ =
match Env.get_typ_var kid env with
| BK_type
| BK_order -> subst
- | BK_nat ->
+ | BK_int ->
match solve env (nvar kid) with
| None -> subst
| Some n -> KBindings.add kid (nconstant n) subst) tyvars KBindings.empty in
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 73c2016e..826d8eb1 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -72,7 +72,7 @@ type ix = text (* infix identifier *)
type
base_kind_aux = (* base kind *)
BK_type (* kind of types *)
- | BK_nat (* kind of natural number size expressions *)
+ | BK_int (* kind of natural number size expressions *)
| BK_order (* kind of vector order specifications *)
diff --git a/src/parser.mly b/src/parser.mly
index 5b8c3af1..0846d4bb 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -557,7 +557,7 @@ typ_list:
base_kind:
| Int
- { BK_aux (BK_nat, loc $startpos $endpos) }
+ { BK_aux (BK_int, loc $startpos $endpos) }
| TYPE
{ BK_aux (BK_type, loc $startpos $endpos) }
| Order
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 228ddbb8..24b28eac 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -122,7 +122,7 @@ let pp_format_bkind_lem (BK_aux(k,l)) =
"(BK_aux " ^
(match k with
| BK_type -> "BK_type"
- | BK_nat -> "BK_nat"
+ | BK_int -> "BK_int"
| BK_order -> "BK_order") ^ " " ^
(pp_format_l_lem l) ^ ")"
diff --git a/src/rewrites.ml b/src/rewrites.ml
index b213a4bb..cb740772 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1964,7 +1964,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
let quant_tyvars = List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item qis) in
let typ_tyvars = tyvars_of_typ fun_typ in
let new_tyvars = KidSet.diff typ_tyvars quant_tyvars in
- List.map (mk_qi_id BK_nat) (KidSet.elements new_tyvars)
+ List.map (mk_qi_id BK_int) (KidSet.elements new_tyvars)
in
let typquant = match typquant with
| TypQ_aux (TypQ_tq qis, l) ->
@@ -1976,7 +1976,7 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
in
TypQ_aux (TypQ_tq qis, l)
| _ ->
- TypQ_aux (TypQ_tq (List.map (mk_qi_id BK_nat) (KidSet.elements (tyvars_of_typ fun_typ))), l)
+ TypQ_aux (TypQ_tq (List.map (mk_qi_id BK_int) (KidSet.elements (tyvars_of_typ fun_typ))), l)
in
let val_spec =
VS_aux (VS_val_spec
diff --git a/src/specialize.ml b/src/specialize.ml
index 151a185a..191ee3be 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -308,7 +308,7 @@ let specialize_id_valspec instantiations id ast =
let kopts, constraints = quant_split typq in
let kopts = List.filter (fun kopt -> not (is_typ_kopt kopt || is_order_kopt kopt)) kopts in
let typq = mk_typquant (List.map (mk_qi_id BK_type) typ_frees
- @ List.map (mk_qi_id BK_nat) int_frees
+ @ List.map (mk_qi_id BK_int) int_frees
@ List.map mk_qi_kopt kopts
@ List.map mk_qi_nc constraints) in
let typschm = mk_typschm typq typ in
@@ -467,7 +467,7 @@ let kinded_id_arg kind_id =
let typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) in
match kind_id with
| KOpt_aux (KOpt_none kid, _) -> typ_arg (Typ_arg_nexp (nvar kid))
- | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), kid), _) -> typ_arg (Typ_arg_nexp (nvar kid))
+ | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_int, _)], _), kid), _) -> typ_arg (Typ_arg_nexp (nvar kid))
| KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), kid), _) ->
typ_arg (Typ_arg_order (Ord_aux (Ord_var kid, Parse_ast.Unknown)))
| KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid), _) ->
diff --git a/src/type_check.ml b/src/type_check.ml
index 4b716ba8..9de6d7e7 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -432,9 +432,9 @@ end = struct
let builtin_typs =
List.fold_left (fun m (name, kinds) -> Bindings.add (mk_id name) (kinds_typq kinds) m) Bindings.empty
- [ ("range", [BK_nat; BK_nat]);
- ("atom", [BK_nat]);
- ("vector", [BK_nat; BK_order; BK_type]);
+ [ ("range", [BK_int; BK_int]);
+ ("atom", [BK_int]);
+ ("vector", [BK_int; BK_order; BK_type]);
("register", [BK_type]);
("ref", [BK_type]);
("bit", []);
@@ -445,7 +445,7 @@ end = struct
("real", []);
("list", [BK_type]);
("string", []);
- ("itself", [BK_nat])
+ ("itself", [BK_int])
]
let bound_typ_id env id =
@@ -545,9 +545,9 @@ end = struct
let rename_kid kid = if KBindings.mem kid env.typ_vars then prepend_kid "syn#" kid else kid in
let add_typ_var env kid =
if KBindings.mem kid env.typ_vars then
- (rebindings := kid :: !rebindings; { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) BK_nat env.typ_vars })
+ (rebindings := kid :: !rebindings; { env with typ_vars = KBindings.add (prepend_kid "syn#" kid) BK_int env.typ_vars })
else
- { env with typ_vars = KBindings.add kid BK_nat env.typ_vars }
+ { env with typ_vars = KBindings.add kid BK_int env.typ_vars }
in
let env = List.fold_left add_typ_var env kids in
@@ -600,7 +600,7 @@ end = struct
| Nexp_var kid ->
begin
match get_typ_var kid env with
- | BK_nat -> ()
+ | BK_int -> ()
| kind -> typ_error l ("Constraint is badly formed, "
^ string_of_kid kid ^ " has kind "
^ string_of_base_kind_aux kind ^ " but should have kind Nat")
@@ -954,7 +954,7 @@ let add_typquant (quant : typquant) (env : Env.t) : Env.t =
| QI_aux (qi, _) -> add_quant_item_aux env qi
and add_quant_item_aux env = function
| QI_const constr -> Env.add_constraint constr env
- | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var kid BK_nat env
+ | QI_id (KOpt_aux (KOpt_none kid, _)) -> Env.add_typ_var kid BK_int env
| QI_id (KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (k, _)], _), kid), _)) -> Env.add_typ_var kid k env
| QI_id (KOpt_aux (_, l)) -> typ_error l "Type variable had non base kinds!"
in
@@ -985,10 +985,10 @@ let destruct_exist env typ =
| _ -> None
let add_existential kids nc env =
- let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in
+ let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env kids in
Env.add_constraint nc env
-let add_typ_vars kids env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids
+let add_typ_vars kids env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env kids
let is_exist = function
| Typ_aux (Typ_exist (_, _, _), _) -> true
@@ -1234,7 +1234,7 @@ let solve env nexp =
try KBindings.find kid !bindings with
| Not_found -> fresh_var kid
in
- let env = Env.add_typ_var (mk_kid "solve#") BK_nat env in
+ let env = Env.add_typ_var (mk_kid "solve#") BK_int env in
let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env))
(nc_constraint env var_of (nc_eq (nvar (mk_kid "solve#")) nexp))
in
@@ -1768,7 +1768,7 @@ let rec subtyp l env typ1 typ2 =
(* Special case for two existentially quantified numeric (atom) types *)
| Some (kids1, nc1, typ1), Some (_ :: _ :: _ as kids2, nc2, typ2)
when is_some (destruct_atom_kid env typ1) && is_some (destruct_atom_kid env typ2) ->
- let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids1 in
+ let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env kids1 in
let env = Env.add_constraint nc1 env in
(* Guaranteed to succeed because of the guard *)
@@ -1777,7 +1777,7 @@ let rec subtyp l env typ1 typ2 =
let atom_kid2 = destruct_some (destruct_atom_kid env typ2) in
let kids2 = List.filter (fun kid -> Kid.compare atom_kid2 kid <> 0) kids2 in
- let env = Env.add_typ_var atom_kid2 BK_nat env in
+ let env = Env.add_typ_var atom_kid2 BK_int env in
let env = Env.add_constraint (nc_eq (nvar atom_kid1) (nvar atom_kid2)) env in
let constr var_of =
Constraint.forall (List.map var_of kids2) (Constraint.negate (nc_constraint env var_of nc2))
@@ -1785,12 +1785,12 @@ let rec subtyp l env typ1 typ2 =
if prove_z3' env constr then ()
else typ_error l ("Existential atom subtyping failed")
| Some (kids, nc, typ1), _ ->
- let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in
+ let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env kids in
let env = Env.add_constraint nc env in
subtyp l env typ1 typ2
| _, Some (kids, nc, typ2) ->
typ_debug "XXXXXXX";
- let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env kids in
+ let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env kids in
typ_debug "YYYYYYY";
let unifiers, existential_kids, existential_nc =
try unify l env typ2 typ1 with
@@ -1801,7 +1801,7 @@ let rec subtyp l env typ1 typ2 =
let env = match existential_kids, existential_nc with
| [], None -> env
| _, Some enc ->
- let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env existential_kids in
+ let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env existential_kids in
let env = List.fold_left uv_nexp_constraint env (KBindings.bindings unifiers) in
Env.add_constraint enc env
| _, None -> assert false (* Cannot have existential_kids without existential_nc *)
@@ -1855,7 +1855,7 @@ let infer_lit env (L_aux (lit_aux, l) as lit) =
| L_undef -> typ_error l "Cannot infer the type of undefined"
let is_nat_kid kid = function
- | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), kid'), _) -> Kid.compare kid kid' = 0
+ | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_int, _)], _), kid'), _) -> Kid.compare kid kid' = 0
| KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0
| _ -> false
@@ -2662,7 +2662,7 @@ and bind_typ_pat env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_aux (typ_aux, _)
begin
match typ_nexps typ with
| [nexp] ->
- Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var kid BK_nat env)
+ Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var kid BK_int env)
| [] ->
typ_error l ("No numeric expressions in " ^ string_of_typ typ ^ " to bind " ^ string_of_kid kid ^ " to")
| nexps ->
@@ -2675,7 +2675,7 @@ and bind_typ_pat_arg env (TP_aux (typ_pat_aux, l) as typ_pat) (Typ_arg_aux (typ_
match typ_pat_aux, typ_arg_aux with
| TP_wild, _ -> env
| TP_var kid, Typ_arg_nexp nexp ->
- Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var kid BK_nat env)
+ Env.add_constraint (nc_eq (nvar kid) nexp) (Env.add_typ_var kid BK_int env)
| _, Typ_arg_typ typ -> bind_typ_pat env typ_pat typ
| _, Typ_arg_order _ -> typ_error l "Cannot bind type pattern against order"
| _, _ -> typ_error l ("Couldn't bind type argument " ^ string_of_typ_arg typ_arg ^ " with " ^ string_of_typ_pat typ_pat)
@@ -3008,7 +3008,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
match destruct_numeric env (typ_of inferred_f), destruct_numeric env (typ_of inferred_t) with
| Some (kids1, nc1, nexp1), Some (kids2, nc2, nexp2) ->
let loop_kid = mk_kid ("loop_" ^ string_of_id v) in
- let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env (loop_kid :: kids1 @ kids2) in
+ let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env (loop_kid :: kids1 @ kids2) in
let env = Env.add_constraint (nc_and nc1 nc2) env in
let env = Env.add_constraint (nc_and (nc_lteq nexp1 (nvar loop_kid)) (nc_lteq (nvar loop_kid) nexp2)) env in
let loop_vtyp = atom_typ (nvar loop_kid) in
@@ -3159,7 +3159,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
| [], None -> env
| _, Some enc ->
let enc = List.fold_left (fun nc kid -> nc_subst_nexp kid (Nexp_var (prepend_kid ex_tag kid)) nc) enc ex_kids in
- let env = List.fold_left (fun env kid -> Env.add_typ_var (prepend_kid ex_tag kid) BK_nat env) env ex_kids in
+ let env = List.fold_left (fun env kid -> Env.add_typ_var (prepend_kid ex_tag kid) BK_int env) env ex_kids in
Env.add_constraint enc env
| _, None -> assert false (* Cannot have ex_kids without ex_nc *)
in
@@ -3195,7 +3195,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
typ_debug (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers));
if ex_kids = [] then () else (typ_debug ("EX GOAL: " ^ string_of_option string_of_n_constraint ex_nc); ex_goal := ex_nc);
record_unifiers unifiers;
- let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_nat env) env ex_kids in
+ let env = List.fold_left (fun env kid -> Env.add_typ_var kid BK_int env) env ex_kids in
let typs' = List.map (subst_unifiers unifiers) typs in
let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in
let ret_typ' =
@@ -3702,7 +3702,7 @@ let kinded_id_arg kind_id =
let typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) in
match kind_id with
| KOpt_aux (KOpt_none kid, _) -> typ_arg (Typ_arg_nexp (nvar kid))
- | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_nat, _)], _), kid), _) -> typ_arg (Typ_arg_nexp (nvar kid))
+ | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_int, _)], _), kid), _) -> typ_arg (Typ_arg_nexp (nvar kid))
| KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), kid), _) ->
typ_arg (Typ_arg_order (Ord_aux (Ord_var kid, Parse_ast.Unknown)))
| KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid), _) ->
@@ -3758,7 +3758,7 @@ let mk_synonym typq typ =
let check_kinddef env (KD_aux (kdef, (l, _))) =
let kd_err () = raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Unimplemented kind def") in
match kdef with
- | KD_nabbrev ((K_aux(K_kind([BK_aux (BK_nat, _)]),_) as kind), id, nmscm, nexp) ->
+ | KD_nabbrev ((K_aux(K_kind([BK_aux (BK_int, _)]),_) as kind), id, nmscm, nexp) ->
[DEF_kind (KD_aux (KD_nabbrev (kind, id, nmscm, nexp), (l, None)))],
Env.add_num_def id nexp env
| _ -> kd_err ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:33:44 +0000