summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml14
-rw-r--r--src/ast_util.mli2
-rw-r--r--src/initial_check.ml7
-rw-r--r--src/monomorphise.ml4
-rw-r--r--src/pretty_print_coq.ml5
-rw-r--r--src/pretty_print_lem.ml2
-rw-r--r--src/pretty_print_sail.ml3
-rw-r--r--src/spec_analysis.ml1
-rw-r--r--src/state.ml2
-rw-r--r--src/type_check.ml13
10 files changed, 16 insertions, 37 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 6c67e6e7..bd7a51bb 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -126,13 +126,11 @@ let mk_letbind pat exp = LB_aux (LB_val (pat, exp), no_annot)
let mk_val_spec vs_aux =
DEF_spec (VS_aux (vs_aux, no_annot))
-let kopt_kid (KOpt_aux (kopt_aux, _)) =
- match kopt_aux with
- | KOpt_none kid | KOpt_kind (_, kid) -> kid
+let kopt_kid (KOpt_aux (KOpt_kind (_, kid), _)) = kid
+let kopt_kind (KOpt_aux (KOpt_kind (k, _), _)) = k
let is_nat_kopt = function
| KOpt_aux (KOpt_kind (K_aux (K_int, _), _), _) -> true
- | KOpt_aux (KOpt_none _, _) -> true
| _ -> false
let is_order_kopt = function
@@ -713,9 +711,7 @@ and string_of_n_constraint = function
| NC_aux (NC_true, _) -> "true"
| NC_aux (NC_false, _) -> "false"
-let string_of_kinded_id = function
- | KOpt_aux (KOpt_none kid, _) -> string_of_kid kid
- | KOpt_aux (KOpt_kind (k, kid), _) -> "(" ^ string_of_kid kid ^ " : " ^ string_of_kind k ^ ")"
+let string_of_kinded_id (KOpt_aux (KOpt_kind (k, kid), _)) = "(" ^ string_of_kid kid ^ " : " ^ string_of_kind k ^ ")"
let string_of_quant_item_aux = function
| QI_id kopt -> string_of_kinded_id kopt
@@ -1192,7 +1188,7 @@ and tyvars_of_typ_arg (A_aux (ta,_)) =
| A_bool nc -> tyvars_of_constraint nc
let tyvars_of_quant_item (QI_aux (qi, _)) = match qi with
- | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) ->
+ | QI_id (KOpt_aux (KOpt_kind (_, kid), _)) ->
KidSet.singleton kid
| QI_const nc -> tyvars_of_constraint nc
@@ -1660,8 +1656,6 @@ let subst_kid subst sv v x =
|> subst sv (mk_typ_arg (A_typ (mk_typ (Typ_var v))))
let quant_item_subst_kid_aux sv subst = function
- | QI_id (KOpt_aux (KOpt_none kid, l)) as qid ->
- if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_none subst, l)) else qid
| QI_id (KOpt_aux (KOpt_kind (k, kid), l)) as qid ->
if Kid.compare kid sv = 0 then QI_id (KOpt_aux (KOpt_kind (k, subst), l)) else qid
| QI_const nc ->
diff --git a/src/ast_util.mli b/src/ast_util.mli
index c0123ce1..8155acde 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -108,6 +108,7 @@ val dec_ord : order
(* Utilites for working with kinded_ids *)
val kopt_kid : kinded_id -> kid
+val kopt_kind : kinded_id -> kind
val is_nat_kopt : kinded_id -> bool
val is_order_kopt : kinded_id -> bool
val is_typ_kopt : kinded_id -> bool
@@ -173,6 +174,7 @@ val nc_true : n_constraint
val nc_false : n_constraint
val nc_set : kid -> Big_int.num list -> n_constraint
val nc_int_set : kid -> int list -> n_constraint
+val nc_var : kid -> n_constraint
val arg_nexp : ?loc:l -> nexp -> typ_arg
val arg_order : ?loc:l -> order -> typ_arg
diff --git a/src/initial_check.ml b/src/initial_check.ml
index da6c7b84..62f0dcf4 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -234,7 +234,7 @@ let to_ast_quant_item ctx (P.QI_aux (aux, l)) =
let aux, ctx = match aux with
| P.KOpt_none v ->
let v = to_ast_var v in
- KOpt_none v, { ctx with kinds = KBindings.add v K_int ctx.kinds }
+ KOpt_kind (K_aux (K_int, gen_loc kopt_l), v), { ctx with kinds = KBindings.add v K_int ctx.kinds }
| P.KOpt_kind (k, v) ->
let v = to_ast_var v in
let k = to_ast_kind k in
@@ -496,11 +496,6 @@ let to_ast_type_union ctx (P.Tu_aux (P.Tu_ty_id (atyp, id), l)) =
let typ = to_ast_typ ctx atyp in
Tu_aux (Tu_ty_id (typ, to_ast_id id), l)
-let kopt_kind (KOpt_aux (aux, l)) =
- match aux with
- | KOpt_none _ -> K_aux (K_int, gen_loc l)
- | KOpt_kind (k, _) -> k
-
let add_constructor id typq ctx =
let kinds = List.map (fun kopt -> unaux_kind (kopt_kind kopt)) (quant_kopts typq) in
{ ctx with type_constructors = Bindings.add id kinds ctx.type_constructors }
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 113db3a2..9206332d 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3358,7 +3358,7 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions =
in aux pat
in
let quant = function
- | QI_aux (QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_,kid)),_)),_) ->
+ | QI_aux (QI_id (KOpt_aux (KOpt_kind (_,kid),_)),_) ->
Some kid
| QI_aux (QI_const _,_) -> None
in
@@ -4264,7 +4264,7 @@ let rewrite_toplevel_nexps (Defs defs) =
match nexp_map with
| [] -> None
| _ ->
- let new_vars = List.map (fun (kid,nexp) -> QI_aux (QI_id (KOpt_aux (KOpt_none kid,Generated Unknown)), Generated tq_l)) nexp_map in
+ let new_vars = List.map (fun (kid,nexp) -> QI_aux (QI_id (mk_kopt K_int kid), Generated tq_l)) nexp_map in
let new_constraints = List.map (fun (kid,nexp) -> QI_aux (QI_const (nc_eq (nvar kid) nexp), Generated tq_l)) nexp_map in
let tqs = TypQ_aux (TypQ_tq (qs @ new_vars @ new_constraints),tq_l) in
let vs =
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index f00a93b7..6dfc6191 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -595,9 +595,6 @@ let doc_lit (L_aux(lit,l)) =
let doc_quant_item_id ctx delimit (QI_aux (qi,_)) =
match qi with
- | QI_id (KOpt_aux (KOpt_none kid,_)) ->
- if KBindings.mem kid ctx.kid_id_renames then None else
- Some (delimit (separate space [doc_var ctx kid; colon; string "Z"]))
| QI_id (KOpt_aux (KOpt_kind (K_aux (kind,_),kid),_)) -> begin
if KBindings.mem kid ctx.kid_id_renames then None else
match kind with
@@ -605,7 +602,6 @@ let doc_quant_item_id ctx delimit (QI_aux (qi,_)) =
| K_int -> Some (delimit (separate space [doc_var ctx kid; colon; string "Z"]))
| K_order -> None
end
- | QI_id _ -> failwith "Quantifier with multiple kinds"
| QI_const nc -> None
let doc_quant_item_constr ctx delimit (QI_aux (qi,_)) =
@@ -1726,7 +1722,6 @@ let doc_typdef generic_eq_types (TD_aux(td, (l, annot))) = match td with
let rectyp = match typq with
| TypQ_aux (TypQ_tq qs, _) ->
let quant_item = function
- | QI_aux (QI_id (KOpt_aux (KOpt_none kid, _)), l)
| QI_aux (QI_id (KOpt_aux (KOpt_kind (_, kid), _)), l) ->
[A_aux (A_nexp (Nexp_aux (Nexp_var kid, l)), l)]
| _ -> [] in
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 1764ab92..6e2a2b55 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -412,7 +412,6 @@ let doc_lit_lem (L_aux(lit,l)) =
(* typ_doc is the doc for the type being quantified *)
let doc_quant_item vars_included (QI_aux (qi, _)) = match qi with
-| QI_id (KOpt_aux (KOpt_none kid, _))
| QI_id (KOpt_aux (KOpt_kind (_, kid), _)) ->
(match vars_included with
None -> doc_var kid
@@ -1020,7 +1019,6 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
let rectyp = match typq with
| TypQ_aux (TypQ_tq qs, _) ->
let quant_item = function
- | QI_aux (QI_id (KOpt_aux (KOpt_none kid, _)), l)
| QI_aux (QI_id (KOpt_aux (KOpt_kind (_, kid), _)), l) ->
[A_aux (A_nexp (Nexp_aux (Nexp_var kid, l)), l)]
| _ -> [] in
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index f756f3d2..d779b3a7 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -195,7 +195,6 @@ and doc_arg_typs = function
| typs -> parens (separate_map (comma ^^ space) doc_typ typs)
let doc_kopt = function
- | KOpt_aux (KOpt_none kid, _) -> doc_kid kid
| kopt when is_nat_kopt kopt -> doc_kid (kopt_kid kopt)
| kopt when is_typ_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])
| kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])
@@ -203,7 +202,6 @@ let doc_kopt = function
let doc_quants quants =
let doc_qi_kopt (QI_aux (qi_aux, _)) =
match qi_aux with
- | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid]
| QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
| QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])]
| QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
@@ -224,7 +222,6 @@ let doc_quants quants =
let doc_param_quants quants =
let doc_qi_kopt (QI_aux (qi_aux, _)) =
match qi_aux with
- | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid]
| QI_id kopt when is_nat_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"]
| QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"]
| QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"]
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 2ab64f1c..65614b8d 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -151,7 +151,6 @@ let typq_bindings (TypQ_aux(tq,_)) = match tq with
match qi with
| QI_id (KOpt_aux(k,_)) ->
(match k with
- | KOpt_none (Kid_aux (Var s,_)) -> Nameset.add s bounds
| KOpt_kind (_, Kid_aux (Var s,_)) -> Nameset.add s bounds)
| _ -> bounds) quants mt
| TypQ_no_forall -> mt
diff --git a/src/state.ml b/src/state.ml
index 4fc2e1e8..c9a47b06 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -128,7 +128,7 @@ let generate_initial_regstate defs =
| _ -> raise Not_found
in
let typ_subst_quant_item typ (QI_aux (qi, _)) arg = match qi with
- | QI_id (KOpt_aux ((KOpt_none kid | KOpt_kind (_, kid)), _)) ->
+ | QI_id (KOpt_aux (KOpt_kind (_, kid), _)) ->
typ_subst kid arg typ
| _ -> typ
in
diff --git a/src/type_check.ml b/src/type_check.ml
index 2f4561b5..f1d9b961 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -210,7 +210,6 @@ and strip_qi_aux = function
and strip_kinded_id = function
| KOpt_aux (kinded_id_aux, _) -> KOpt_aux (strip_kinded_id_aux kinded_id_aux, Parse_ast.Unknown)
and strip_kinded_id_aux = function
- | KOpt_none kid -> KOpt_none (strip_kid kid)
| KOpt_kind (kind, kid) -> KOpt_kind (strip_kind kind, strip_kid kid)
and strip_kind = function
| K_aux (k_aux, _) -> K_aux (k_aux, Parse_ast.Unknown)
@@ -1108,7 +1107,6 @@ let add_typquant l (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 l kid K_int env
| QI_id (KOpt_aux (KOpt_kind (K_aux (k, _), kid), _)) -> Env.add_typ_var l kid k env
in
match quant with
@@ -1823,7 +1821,6 @@ let infer_lit env (L_aux (lit_aux, l) as lit) =
let is_nat_kid kid = function
| KOpt_aux (KOpt_kind (K_aux (K_int, _), kid'), _) -> Kid.compare kid kid' = 0
- | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0
| _ -> false
let is_order_kid kid = function
@@ -4228,12 +4225,14 @@ let check_default env (DT_aux (ds, l)) =
let kinded_id_arg kind_id =
let typ_arg arg = A_aux (arg, Parse_ast.Unknown) in
match kind_id with
- | KOpt_aux (KOpt_none kid, _) -> typ_arg (A_nexp (nvar kid))
- | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid), _) -> typ_arg (A_nexp (nvar kid))
+ | KOpt_aux (KOpt_kind (K_aux (K_int, _), kid), _) ->
+ typ_arg (A_nexp (nvar kid))
| KOpt_aux (KOpt_kind (K_aux (K_order, _), kid), _) ->
typ_arg (A_order (Ord_aux (Ord_var kid, Parse_ast.Unknown)))
| KOpt_aux (KOpt_kind (K_aux (K_type, _), kid), _) ->
typ_arg (A_typ (mk_typ (Typ_var kid)))
+ | KOpt_aux (KOpt_kind (K_aux (K_bool, _), kid), _) ->
+ typ_arg (A_bool (nc_var kid))
let fold_union_quant quants (QI_aux (qi, l)) =
match qi with
@@ -4403,13 +4402,13 @@ let initial_env =
|> Env.add_extern (mk_id "size_itself_int") (fun _ -> Some "size_itself_int")
|> Env.add_val_spec (mk_id "size_itself_int")
- (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
+ (TypQ_aux (TypQ_tq [QI_aux (QI_id (mk_kopt K_int (mk_kid "n")),
Parse_ast.Unknown)],Parse_ast.Unknown),
function_typ [app_typ (mk_id "itself") [mk_typ_arg (A_nexp (nvar (mk_kid "n")))]]
(atom_typ (nvar (mk_kid "n"))) no_effect)
|> Env.add_extern (mk_id "make_the_value") (fun _ -> Some "make_the_value")
|> Env.add_val_spec (mk_id "make_the_value")
- (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
+ (TypQ_aux (TypQ_tq [QI_aux (QI_id (mk_kopt K_int (mk_kid "n")),
Parse_ast.Unknown)],Parse_ast.Unknown),
function_typ [atom_typ (nvar (mk_kid "n"))]
(app_typ (mk_id "itself") [mk_typ_arg (A_nexp (nvar (mk_kid "n")))]) no_effect)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 01:20:31 +0000