summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml1
-rw-r--r--src/ast_util.mli5
-rw-r--r--src/nl_flow.ml2
-rw-r--r--src/type_check.ml54
-rw-r--r--src/type_error.ml49
5 files changed, 58 insertions, 53 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index a771291e..795a41fe 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -365,6 +365,7 @@ let range_typ nexp1 nexp2 =
mk_typ (Typ_app (mk_id "range", [mk_typ_arg (A_nexp (nexp_simp nexp1));
mk_typ_arg (A_nexp (nexp_simp nexp2))]))
let bool_typ = mk_id_typ (mk_id "bool")
+let atom_bool_typ nc = mk_typ (Typ_app (mk_id "atom_bool", [mk_typ_arg (A_bool nc)]))
let string_typ = mk_id_typ (mk_id "string")
let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (A_typ typ)]))
let tuple_typ typs = mk_typ (Typ_tup typs)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index ca3a9598..7a44322d 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -113,7 +113,7 @@ val is_nat_kopt : kinded_id -> bool
val is_order_kopt : kinded_id -> bool
val is_typ_kopt : kinded_id -> bool
val is_bool_kopt : kinded_id -> bool
-
+
(* Some handy utility functions for constructing types. *)
val mk_typ : typ_aux -> typ
val mk_typ_arg : typ_arg_aux -> typ_arg
@@ -127,6 +127,7 @@ val atom_typ : nexp -> typ
val range_typ : nexp -> nexp -> typ
val bit_typ : typ
val bool_typ : typ
+val atom_bool_typ : n_constraint -> typ
val app_typ : id -> typ_arg list -> typ
val register_typ : typ -> typ
val unit_typ : typ
@@ -191,7 +192,7 @@ val quant_map_items : (quant_item -> quant_item) -> typquant -> typquant
val is_quant_kopt : quant_item -> bool
val is_quant_constraint : quant_item -> bool
-
+
(* Functions to map over the annotations in sub-expressions *)
val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
val map_pat_annot : ('a annot -> 'b annot) -> 'a pat -> 'b pat
diff --git a/src/nl_flow.ml b/src/nl_flow.ml
index e38e5fa5..6196f23b 100644
--- a/src/nl_flow.ml
+++ b/src/nl_flow.ml
@@ -91,7 +91,7 @@ let add_assert cond (E_aux (aux, (l, ())) as exp) =
let modify_unsigned id value (E_aux (aux, annot) as exp) =
match aux with
| E_let (LB_aux (LB_val (pat, E_aux (E_app (f, [E_aux (E_id id', _)]), _)), _) as lb, exp')
- when string_of_id f = "unsigned" && Id.compare id id' = 0 ->
+ when (string_of_id f = "unsigned" || string_of_id f = "UInt") && Id.compare id id' = 0 ->
begin match pat_id pat with
| None -> exp
| Some uid ->
diff --git a/src/type_check.ml b/src/type_check.ml
index 53d87a05..09ee3380 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -259,10 +259,19 @@ let destruct_numeric typ =
Some ([kid], nc_true, nvar kid)
| _, _ -> None
+let destruct_boolean = function
+ | Typ_aux (Typ_id (Id_aux (Id "bool", _)), _) ->
+ let kid = kopt_kid (fresh_existential K_bool) in
+ Some (kid, nc_var kid)
+ | _ -> None
+
let destruct_exist typ =
match destruct_numeric typ with
| Some (kids, nc, nexp) -> Some (List.map (mk_kopt K_int) kids, nc, atom_typ nexp)
- | None -> destruct_exist_plain typ
+ | None ->
+ match destruct_boolean typ with
+ | Some (kid, nc) -> Some ([mk_kopt K_bool kid], nc_true, atom_bool_typ nc)
+ | None -> destruct_exist_plain typ
let adding = Util.("Adding " |> darkgray |> clear)
@@ -700,8 +709,7 @@ end = struct
| NC_var kid ->
begin match get_typ_var kid env with
| K_bool -> ()
- | kind -> typ_error l ("Set constraint is badly formed, "
- ^ string_of_kid kid ^ " has kind "
+ | kind -> typ_error l (string_of_kid kid ^ " has kind "
^ string_of_kind_aux kind ^ " but should have kind Bool")
end
| NC_true | NC_false -> ()
@@ -1243,7 +1251,7 @@ let prove_z3 env (NC_aux (_, l) as nc) =
| Constraint.Sat -> typ_debug (lazy "sat"); false
| Constraint.Unknown -> typ_debug (lazy "unknown"); false
-let solve env (Nexp_aux (_, l) as nexp) =
+let solve env (Nexp_aux (_, l) as nexp) =
typ_print (lazy (Util.("Solve " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env)
^ " |- " ^ string_of_nexp nexp ^ " = ?"));
match nexp with
@@ -1621,10 +1629,21 @@ and kid_order_arg kind_map (A_aux (aux, l) as arg) =
| A_order _ -> ([], kind_map)
and kid_order_constraint kind_map (NC_aux (aux, l) as nc) =
match aux with
- | NC_var kid when KBindings.mem kid kind_map ->
+ | NC_var kid | NC_set (kid, _) when KBindings.mem kid kind_map ->
([mk_kopt (unaux_kind (KBindings.find kid kind_map)) kid], KBindings.remove kid kind_map)
- | NC_var _ -> ([], kind_map)
- | _ -> unreachable l __POS__ "bad constraint type"
+ | NC_var _ | NC_set _ -> ([], kind_map)
+ | NC_true | NC_false -> ([], kind_map)
+ | NC_equal (n1, n2) | NC_not_equal (n1, n2) | NC_bounded_le (n1, n2) | NC_bounded_ge (n1, n2) ->
+ let ord1, kind_map = kid_order_nexp kind_map n1 in
+ let ord2, kind_map = kid_order_nexp kind_map n2 in
+ (ord1 @ ord2, kind_map)
+ | NC_app (_, args) ->
+ List.fold_left (fun (ord, kind_map) arg -> let ord', kind_map = kid_order_arg kind_map arg in (ord @ ord', kind_map))
+ ([], kind_map) args
+ | NC_and (nc1, nc2) | NC_or (nc1, nc2) ->
+ let ord1, kind_map = kid_order_constraint kind_map nc1 in
+ let ord2, kind_map = kid_order_constraint kind_map nc2 in
+ (ord1 @ ord2, kind_map)
let rec alpha_equivalent env typ1 typ2 =
let counter = ref 0 in
@@ -1779,7 +1798,7 @@ and subtyp_arg l env (A_aux (aux1, _) as arg1) (A_aux (aux2, _) as arg2) =
| A_nexp n1, A_nexp n2 when prove env (nc_eq n1 n2) -> ()
| A_typ typ1, A_typ typ2 -> subtyp l env typ1 typ2
| A_order ord1, A_order ord2 when ord_identical ord1 ord2 -> ()
- | A_bool nc1, A_bool nc2 when nc_identical nc1 nc2 -> ()
+ | A_bool nc1, A_bool nc2 when prove env (nc_and (nc_or (nc_not nc1) nc2) (nc_or (nc_not nc2) nc1)) -> ()
| _, _ -> typ_error l "Mismatched argument types in subtype check"
let typ_equality l env typ1 typ2 =
@@ -1827,8 +1846,8 @@ let infer_lit env (L_aux (lit_aux, l) as lit) =
| L_zero -> bit_typ
| L_one -> bit_typ
| L_num n -> atom_typ (nconstant n)
- | L_true -> bool_typ
- | L_false -> bool_typ
+ | L_true -> atom_bool_typ nc_true
+ | L_false -> atom_bool_typ nc_false
| L_string _ -> string_typ
| L_real _ -> real_typ
| L_bin str ->
@@ -2256,16 +2275,25 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
end
| E_app_infix (x, op, y), _ ->
check_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) typ
- | E_app (f, [E_aux (E_constraint nc, _)]), _ when Id.compare f (mk_id "_prove") = 0 ->
+ | E_app (f, [E_aux (E_constraint nc, _)]), _ when string_of_id f = "_prove" ->
Env.wf_constraint env nc;
if prove env nc
then annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
else typ_error l ("Cannot prove " ^ string_of_n_constraint nc)
- | E_app (f, [E_aux (E_constraint nc, _)]), _ when Id.compare f (mk_id "_not_prove") = 0 ->
+ | E_app (f, [E_aux (E_constraint nc, _)]), _ when string_of_id f = "_not_prove" ->
Env.wf_constraint env nc;
if prove env nc
then typ_error l ("Can prove " ^ string_of_n_constraint nc)
else annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
+ | E_app (f, [E_aux (E_cast (typ, exp), _)]), _ when string_of_id f = "_check" ->
+ Env.wf_typ env typ;
+ let _ = crule check_exp env exp typ in
+ annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
+ | E_app (f, [E_aux (E_cast (typ, exp), _)]), _ when string_of_id f = "_not_check" ->
+ Env.wf_typ env typ;
+ if (try (ignore (crule check_exp env exp typ); false) with Type_error _ -> true)
+ then annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
+ else typ_error l (Printf.sprintf "Expected _not_check(%s : %s) to fail" (string_of_exp exp) (string_of_typ typ))
(* All constructors and mappings are treated as having one argument
so Ctor(x, y) is checked as Ctor((x, y)) *)
| E_app (f, x :: y :: zs), _ when Env.is_union_constructor f env || Env.is_mapping f env ->
@@ -3060,7 +3088,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
| E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (A_nexp nexp)])))
| E_constraint nc ->
Env.wf_constraint env nc;
- annot_exp (E_constraint nc) bool_typ
+ annot_exp (E_constraint nc) (atom_bool_typ nc)
| E_field (exp, field) ->
begin
let inferred_exp = irule infer_exp env exp in
diff --git a/src/type_error.ml b/src/type_error.ml
index 9144e993..f28e4de8 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -67,38 +67,6 @@ let pp_nexp, pp_n_constraint =
in
pp_nexp', pp_n_constraint'
-let rec nexp_subst sv subst (Nexp_aux (nexp, l)) = Nexp_aux (nexp_subst_aux sv subst nexp, l)
-and nexp_subst_aux sv subst = function
- | Nexp_id v -> Nexp_id v
- | Nexp_var kid -> if Kid.compare kid sv = 0 then subst else Nexp_var kid
- | Nexp_constant c -> Nexp_constant c
- | Nexp_times (nexp1, nexp2) -> Nexp_times (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
- | Nexp_sum (nexp1, nexp2) -> Nexp_sum (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
- | Nexp_minus (nexp1, nexp2) -> Nexp_minus (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2)
- | Nexp_app (id, nexps) -> Nexp_app (id, List.map (nexp_subst sv subst) nexps)
- | Nexp_exp nexp -> Nexp_exp (nexp_subst sv subst nexp)
- | Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp)
-
-let rec nexp_set_to_or l subst = function
- | [] -> typ_error l "Cannot substitute into empty nexp set"
- | [int] -> NC_equal (subst, nconstant int)
- | (int :: ints) -> NC_or (mk_nc (NC_equal (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints))
-
-let rec nc_subst_nexp sv subst (NC_aux (nc, l)) = NC_aux (nc_subst_nexp_aux l sv subst nc, l)
-and nc_subst_nexp_aux l sv subst = function
- | NC_equal (n1, n2) -> NC_equal (nexp_subst sv subst n1, nexp_subst sv subst n2)
- | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2)
- | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2)
- | NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2)
- | NC_set (kid, ints) as set_nc ->
- if Kid.compare kid sv = 0
- then nexp_set_to_or l (mk_nexp subst) ints
- else set_nc
- | NC_or (nc1, nc2) -> NC_or (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
- | NC_and (nc1, nc2) -> NC_and (nc_subst_nexp sv subst nc1, nc_subst_nexp sv subst nc2)
- | NC_false -> NC_false
- | NC_true -> NC_true
-
type suggestion =
| Suggest_add_constraint of n_constraint
| Suggest_none
@@ -126,7 +94,7 @@ let rec analyze_unresolved_quant2 locals ncs = function
| _ -> []
in
let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_subst v nc) ncs)) gen_kids) in
- let nc = List.fold_left (fun nc (v, nexp) -> nc_subst_nexp v (unaux_nexp nexp) nc) nc substs in
+ let nc = List.fold_left (fun nc (v, nexp) -> constraint_subst v (arg_nexp nexp) nc) nc substs in
if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then
Suggest_add_constraint nc
else
@@ -140,7 +108,7 @@ let rec analyze_unresolved_quant2 locals ncs = function
[]
in
let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_linked v nc) (Bindings.bindings locals))) gen_kids) in
- let nc = List.fold_left (fun nc (v, nexp, _) -> nc_subst_nexp v (unaux_nexp nexp) nc) nc substs in
+ let nc = List.fold_left (fun nc (v, nexp, _) -> constraint_subst v (arg_nexp nexp) nc) nc substs in
if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then
Suggest_none
else
@@ -171,7 +139,7 @@ let rec analyze_unresolved_quant locals ncs = function
| _ -> []
in
let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_subst v nc) ncs)) gen_kids) in
- let nc = List.fold_left (fun nc (v, nexp) -> nc_subst_nexp v (unaux_nexp nexp) nc) nc substs in
+ let nc = List.fold_left (fun nc (v, nexp) -> constraint_subst v (arg_nexp nexp) nc) nc substs in
if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then
string ("Try adding the constraint " ^ string_of_n_constraint nc)
else
@@ -188,7 +156,7 @@ let rec analyze_unresolved_quant locals ncs = function
(string "Try adding named type variables for"
^//^ string (Util.string_of_list ", " (fun (_, nexp, typ) -> string_of_nexp nexp ^ " : " ^ string_of_typ typ) substs))
^^ twice hardline ^^
- let nc = List.fold_left (fun nc (v, nexp, _) -> nc_subst_nexp v (unaux_nexp nexp) nc) nc substs in
+ let nc = List.fold_left (fun nc (v, nexp, _) -> constraint_subst v (arg_nexp nexp) nc) nc substs in
if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then
string ("The property " ^ string_of_n_constraint nc ^ " must hold")
else
@@ -239,7 +207,7 @@ let rec pp_type_error = function
pp_type_error err
^^ hardline ^^ string "This error occured because of a previous error:"
^//^ pp_type_error err'
-
+
| Err_other str -> string str
let rec string_of_type_error err =
@@ -264,6 +232,13 @@ let rec collapse_errors = function
| Some _ -> err
| None -> no_collapse
end
+ | Err_because (err1, err2) as no_collapse ->
+ let err1 = collapse_errors err1 in
+ let err2 = collapse_errors err2 in
+ if string_of_type_error err1 = string_of_type_error err2 then
+ err1
+ else
+ Err_because (err1, err2)
| err -> err
let check : 'a. Env.t -> 'a defs -> tannot defs * Env.t =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:40:56 +0000