summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--editors/sail2-mode.el2
-rw-r--r--src/ast_util.ml2
-rw-r--r--src/initial_check.ml47
-rw-r--r--src/parse_ast.ml4
-rw-r--r--src/parser.mly8
-rw-r--r--src/pretty_print_lem.ml5
-rw-r--r--src/pretty_print_sail.ml17
-rw-r--r--src/rewrites.ml2
-rw-r--r--src/spec_analysis.ml9
-rw-r--r--src/type_check.ml94
-rw-r--r--src/type_check.mli2
-rw-r--r--test/typecheck/future/bool_constraint.sail35
-rw-r--r--test/typecheck/pass/exist_synonym/v3.expect2
-rw-r--r--test/typecheck/pass/exist_synonym/v4.expect2
-rw-r--r--test/typecheck/pass/global_type_var/v3.expect2
-rw-r--r--test/typecheck/pass/if_infer/v1.expect4
-rw-r--r--test/typecheck/pass/if_infer/v2.expect4
-rw-r--r--test/typecheck/pass/tautology.sail65
-rwxr-xr-xtest/typecheck/update_errors.sh17
19 files changed, 257 insertions, 66 deletions
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index b7998357..38404f14 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -21,7 +21,7 @@
"uint64_t" "int64_t" "bv_t" "mpz_t"))
(defconst sail2-special
- '("_prove" "create" "kill" "convert" "undefined"
+ '("_prove" "_not_prove" "create" "kill" "convert" "undefined"
"$define" "$include" "$ifdef" "$ifndef" "$else" "$endif" "$option" "$latex"))
(defconst sail2-font-lock-keywords
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 02e297cb..a771291e 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -739,6 +739,8 @@ and string_of_n_constraint = function
"(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
| NC_aux (NC_set (kid, ns), _) ->
string_of_kid kid ^ " in {" ^ string_of_list ", " Big_int.to_string ns ^ "}"
+ | NC_aux (NC_app (Id_aux (DeIid op, _), [arg1; arg2]), _) ->
+ "(" ^ string_of_typ_arg arg1 ^ " " ^ op ^ " " ^ string_of_typ_arg arg2 ^ ")"
| NC_aux (NC_app (id, args), _) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")"
| NC_aux (NC_var v, _) -> string_of_kid v
| NC_aux (NC_true, _) -> "true"
diff --git a/src/initial_check.ml b/src/initial_check.ml
index d394fde9..61cde224 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -129,6 +129,18 @@ let format_kind_aux_list = function
| [kind] -> string_of_kind_aux kind
| kinds -> "(" ^ Util.string_of_list ", " string_of_kind_aux kinds ^ ")"
+let to_ast_kopt ctx (P.KOpt_aux (aux, l)) =
+ let aux, ctx = match aux with
+ | P.KOpt_none v ->
+ let v = to_ast_var v in
+ KOpt_kind (K_aux (K_int, gen_loc 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
+ KOpt_kind (k, v), { ctx with kinds = KBindings.add v (unaux_kind k) ctx.kinds }
+ in
+ KOpt_aux (aux, l), ctx
+
let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
let aux = match aux with
| P.ATyp_id id -> Typ_id (to_ast_id id)
@@ -157,10 +169,11 @@ let rec to_ast_typ ctx (P.ATyp_aux (aux, l)) =
| Some kinds ->
Typ_app (id, List.map2 (to_ast_typ_arg ctx) args kinds)
end
- | P.ATyp_exist (kids, nc, atyp) ->
- let kids = List.map to_ast_var kids in
- let ctx = { ctx with kinds = List.fold_left (fun kinds kid -> KBindings.add kid K_int kinds) ctx.kinds kids } in
- Typ_exist (List.map (mk_kopt K_int) kids, to_ast_constraint ctx nc, to_ast_typ ctx atyp)
+ | P.ATyp_exist (kopts, nc, atyp) ->
+ let kopts, ctx =
+ List.fold_right (fun kopt (kopts, ctx) -> let kopt, ctx = to_ast_kopt ctx kopt in (kopt :: kopts, ctx)) kopts ([], ctx)
+ in
+ Typ_exist (kopts, to_ast_constraint ctx nc, to_ast_typ ctx atyp)
| P.ATyp_base (id, kind, nc) ->
raise (Reporting.err_unreachable l __POS__ "TODO")
| _ -> raise (Reporting.err_typ l "Invalid type")
@@ -197,7 +210,7 @@ and to_ast_order ctx (P.ATyp_aux (aux, l)) =
and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) =
let aux = match aux with
- | P.ATyp_app (Id_aux (DeIid op, _), [t1; t2]) ->
+ | P.ATyp_app (Id_aux (DeIid op, _) as id, [t1; t2]) ->
begin match op with
| "==" -> NC_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
| "!=" -> NC_equal (to_ast_nexp ctx t1, to_ast_nexp ctx t2)
@@ -207,7 +220,15 @@ and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) =
| "<" -> NC_bounded_le (nsum (to_ast_nexp ctx t1) (nint 1), to_ast_nexp ctx t2)
| "&" -> NC_and (to_ast_constraint ctx t1, to_ast_constraint ctx t2)
| "|" -> NC_or (to_ast_constraint ctx t1, to_ast_constraint ctx t2)
- | _ -> raise (Reporting.err_typ l ("Invalid operator in constraint"))
+ | _ ->
+ let id = to_ast_id id in
+ match Bindings.find_opt id ctx.type_constructors with
+ | None -> raise (Reporting.err_typ l (sprintf "Could not find type constructor %s" (string_of_id id)))
+ | Some kinds when List.length kinds <> 2 ->
+ raise (Reporting.err_typ l (sprintf "%s : %s -> Bool expected %d arguments, given 2"
+ (string_of_id id) (format_kind_aux_list kinds)
+ (List.length kinds)))
+ | Some kinds -> NC_app (id, List.map2 (to_ast_typ_arg ctx) [t1; t2] kinds)
end
| P.ATyp_app (id, args) ->
let id = to_ast_id id in
@@ -230,17 +251,9 @@ and to_ast_constraint ctx (P.ATyp_aux (aux, l) as atyp) =
let to_ast_quant_item ctx (P.QI_aux (aux, l)) =
match aux with
| P.QI_const nc -> QI_aux (QI_const (to_ast_constraint ctx nc), l), ctx
- | P.QI_id (KOpt_aux (aux, kopt_l)) ->
- let aux, ctx = match aux with
- | P.KOpt_none v ->
- let v = to_ast_var v in
- 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
- KOpt_kind (k, v), { ctx with kinds = KBindings.add v (unaux_kind k) ctx.kinds }
- in
- QI_aux (QI_id (KOpt_aux (aux, kopt_l)), l), ctx
+ | P.QI_id kopt ->
+ let kopt, ctx = to_ast_kopt ctx kopt in
+ QI_aux (QI_id kopt, l), ctx
let to_ast_typquant ctx (P.TypQ_aux (aux, l)) =
match aux with
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index a5dbf66e..9b855837 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -163,7 +163,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders
| ATyp_wild
| ATyp_tup of (atyp) list (* Tuple type *)
| ATyp_app of id * (atyp) list (* type constructor application *)
- | ATyp_exist of kid list * atyp * atyp
+ | ATyp_exist of kinded_id list * atyp * atyp
| ATyp_base of id * atyp * atyp
and atyp =
@@ -175,7 +175,7 @@ kinded_id_aux = (* optionally kind-annotated identifier *)
KOpt_none of kid (* identifier *)
| KOpt_kind of kind * kid (* kind-annotated variable *)
-type
+and
kinded_id =
KOpt_aux of kinded_id_aux * l
diff --git a/src/parser.mly b/src/parser.mly
index 544438c0..1957d7fd 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -78,6 +78,8 @@ let prepend_id str1 = function
let mk_id i n m = Id_aux (i, loc n m)
let mk_kid str n m = Kid_aux (Var str, loc n m)
+let mk_kopt k n m = KOpt_aux (k, loc n m)
+
let id_of_kid = function
| Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
@@ -550,10 +552,10 @@ atomic_typ:
{ let v = mk_kid "n" $startpos $endpos in
let atom_id = mk_id (Id "atom") $startpos $endpos in
let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in
- mk_typ (ATyp_exist ([v], ATyp_aux (ATyp_nset (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
- | Lcurly kid_list Dot typ Rcurly
+ mk_typ (ATyp_exist ([mk_kopt (KOpt_none v) $startpos $endpos], ATyp_aux (ATyp_nset (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
+ | Lcurly kopt_list Dot typ Rcurly
{ mk_typ (ATyp_exist ($2, ATyp_aux (ATyp_lit (L_aux (L_true, loc $startpos $endpos)), loc $startpos $endpos), $4)) $startpos $endpos }
- | Lcurly kid_list Comma typ Dot typ Rcurly
+ | Lcurly kopt_list Comma typ Dot typ Rcurly
{ mk_typ (ATyp_exist ($2, $4, $6)) $startpos $endpos }
| Lcurly id Colon typ Dot typ Rcurly
{ mk_typ (ATyp_base ($2, $4, $6)) $startpos $endpos }
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index ac0195aa..9d169108 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -247,6 +247,7 @@ and lem_nexps_of_typ_arg (A_aux (ta,_)) =
| A_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp))
| A_typ typ -> lem_nexps_of_typ typ
| A_order _ -> NexpSet.empty
+ | A_bool _ -> NexpSet.empty
let lem_tyvars_of_typ typ =
NexpSet.fold (fun nexp ks -> KidSet.union ks (tyvars_of_nexp nexp))
@@ -296,6 +297,8 @@ let doc_typ_lem, doc_atomic_typ_lem =
(string "integer")
| Typ_app(Id_aux (Id "atom", _), [A_aux(A_nexp n,_)]) ->
(string "integer")
+ | Typ_app(Id_aux (Id "atom_bool", _), [A_aux(A_bool nc,_)]) ->
+ (string "bool")
| Typ_app(id,args) ->
let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space doc_typ_arg_lem args) in
if atyp_needed then parens tpp else tpp
@@ -331,6 +334,7 @@ let doc_typ_lem, doc_atomic_typ_lem =
| A_typ t -> app_typ true t
| A_nexp n -> doc_nexp_lem (nexp_simp n)
| A_order o -> empty
+ | A_bool _ -> empty
in typ', atomic_typ
(* Check for variables in types that would be pretty-printed. *)
@@ -1013,6 +1017,7 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
doc_op equals
(separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem None typq])
(doc_typschm_lem false typschm)
+ | TD_abbrev _ -> empty
| TD_record(id,nm,typq,fs,_) ->
let fname fid = if prefix_recordtype && string_of_id id <> "regstate"
then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index e0223105..c4b9bdd3 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -70,7 +70,7 @@ let doc_kopt = function
| kopt when is_typ_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])
| kopt when is_order_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])
| kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])
-
+
let doc_int n = string (Big_int.to_string n)
let docstring (l, _) = match l with
@@ -168,6 +168,8 @@ and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
separate space [doc_typ_arg x; doc_typ_arg y]
| Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 ->
string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
+ | Typ_app (id, typs) when Id.compare id (mk_id "atom_bool") = 0 ->
+ string "bool" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
| Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs)
| Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs)
| Typ_var kid -> doc_kid kid
@@ -205,6 +207,7 @@ let doc_quants quants =
match qi_aux with
| 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 when is_bool_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])]
| QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
| QI_const nc -> []
in
@@ -225,6 +228,7 @@ let doc_param_quants quants =
match qi_aux with
| 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 when is_bool_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Bool"]
| QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"]
| QI_const nc -> []
in
@@ -567,14 +571,21 @@ let doc_field (typ, id) =
let doc_union (Tu_aux (Tu_ty_id (typ, id), l)) = separate space [doc_id id; colon; doc_typ typ]
+let doc_typ_arg_kind (A_aux (aux, _)) =
+ match aux with
+ | A_nexp _ -> space ^^ string "->" ^^ space ^^string "Int"
+ | A_bool _ -> space ^^ string "->" ^^ space ^^ string "Bool"
+ | A_order _ -> space ^^ string "->" ^^ space ^^ string "Order"
+ | A_typ _ -> empty
+
let doc_typdef (TD_aux(td,_)) = match td with
| TD_abbrev (id, typq, typ_arg) ->
begin
match doc_typquant typq with
| Some qdoc ->
- doc_op equals (concat [string "type"; space; doc_id id; qdoc]) (doc_typ_arg typ_arg)
+ doc_op equals (concat [string "type"; space; doc_id id; qdoc; doc_typ_arg_kind typ_arg]) (doc_typ_arg typ_arg)
| None ->
- doc_op equals (concat [string "type"; space; doc_id id]) (doc_typ_arg typ_arg)
+ doc_op equals (concat [string "type"; space; doc_id id; doc_typ_arg_kind typ_arg]) (doc_typ_arg typ_arg)
end
| TD_enum (id, _, ids, _) ->
separate space [string "enum"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 79b5f619..30318e3f 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -271,6 +271,8 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
A_aux (A_typ (rewrite_typ env typ), l)
| A_order ord ->
A_aux (A_order ord, l)
+ | A_bool nc ->
+ A_aux (A_bool nc, l)
in
let rewrite_annot (l, tannot) =
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 0f8db0ff..940fbfe5 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -310,10 +310,13 @@ let typ_variants consider_var bound tunions =
let fv_of_kind_def consider_var (KD_aux(k,_)) = match k with
| KD_nabbrev(_,id,_,nexp) -> init_env (string_of_id id), fv_of_nexp consider_var mt mt nexp
+let fv_of_abbrev consider_var bound used typq typ_arg =
+ let ts_bound = if consider_var then typq_bindings typq else mt in
+ ts_bound, fv_of_targ consider_var (Nameset.union bound ts_bound) used typ_arg
+
let fv_of_type_def consider_var (TD_aux(t,_)) = match t with
- | TD_abbrev(id,typq,A_aux(A_typ typ, l)) ->
- let typschm = TypSchm_aux (TypSchm_ts (typq,typ), l) in
- init_env (string_of_id id), snd (fv_of_typschm consider_var mt mt typschm)
+ | TD_abbrev(id,typq,typ_arg) ->
+ init_env (string_of_id id), snd (fv_of_abbrev consider_var mt mt typq typ_arg)
| TD_record(id,_,typq,tids,_) ->
let binds = init_env (string_of_id id) in
let bounds = if consider_var then typq_bindings typq else mt in
diff --git a/src/type_check.ml b/src/type_check.ml
index cc0b9843..befc7302 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -82,7 +82,7 @@ let rec indent n = match n with
(* Lazily evaluate debugging message. This can make a big performance
difference; for example, repeated calls to string_of_exp can be costly for
deeply nested expressions, e.g. with long sequences of monadic binds. *)
-let typ_debug m = if !opt_tc_debug > 1 then prerr_endline (indent !depth ^ Lazy.force m) else ()
+let typ_debug ?level:(level=1) m = if !opt_tc_debug > level then prerr_endline (indent !depth ^ Lazy.force m) else ()
let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ Lazy.force m) else ()
@@ -516,6 +516,7 @@ end = struct
else typ_error (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
let rec expand_constraint_synonyms env (NC_aux (aux, l) as nc) =
+ typ_debug ~level:2 (lazy ("Expanding " ^ string_of_n_constraint nc));
match aux with
| NC_or (nc1, nc2) -> NC_aux (NC_or (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l)
| NC_and (nc1, nc2) -> NC_aux (NC_and (expand_constraint_synonyms env nc1, expand_constraint_synonyms env nc2), l)
@@ -523,7 +524,7 @@ end = struct
(try
begin match Bindings.find id env.typ_synonyms env args with
| A_aux (A_bool nc, _) -> expand_constraint_synonyms env nc
- | _ -> typ_error l ("Expected Type when expanding synonym " ^ string_of_id id)
+ | arg -> typ_error l ("Expected Bool when expanding synonym " ^ string_of_id id ^ " got " ^ string_of_typ_arg arg)
end
with Not_found -> NC_aux (NC_app (id, List.map (expand_synonyms_arg env) args), l))
| NC_true | NC_false | NC_equal _ | NC_not_equal _ | NC_bounded_le _ | NC_bounded_ge _ | NC_var _ | NC_set _ -> nc
@@ -602,9 +603,13 @@ end = struct
| A_order _ | A_typ _ | A_bool _ -> arg
| A_nexp n -> A_aux (A_nexp (f n), l)
+ let wf_debug str f x exs =
+ typ_debug ~level:2 (lazy ("wf_" ^ str ^ ": " ^ f x ^ " exs: " ^ Util.string_of_list ", " string_of_kid (KidSet.elements exs)))
+
(* Check if a type, order, n-expression or constraint is
well-formed. Throws a type error if the type is badly formed. *)
let rec wf_typ ?exs:(exs=KidSet.empty) env typ =
+ wf_debug "typ" string_of_typ typ exs;
let (Typ_aux (typ_aux, l)) = expand_synonyms env typ in
match typ_aux with
| Typ_id id when bound_typ_id env id ->
@@ -643,6 +648,7 @@ end = struct
| A_order ord -> wf_order env ord
| A_bool nc -> wf_constraint ~exs:exs env nc
and wf_nexp ?exs:(exs=KidSet.empty) env (Nexp_aux (nexp_aux, l) as nexp) =
+ wf_debug "nexp" string_of_nexp nexp exs;
match nexp_aux with
| Nexp_id _ -> ()
| Nexp_var kid when KidSet.mem kid exs -> ()
@@ -662,7 +668,7 @@ end = struct
| Nexp_minus (nexp1, nexp2) -> wf_nexp ~exs:exs env nexp1; wf_nexp ~exs:exs env nexp2
| Nexp_exp nexp -> wf_nexp ~exs:exs env nexp (* MAYBE: Could put restrictions on what is allowed here *)
| Nexp_neg nexp -> wf_nexp ~exs:exs env nexp
- and wf_order env (Ord_aux (ord_aux, l)) =
+ and wf_order env (Ord_aux (ord_aux, l) as ord) =
match ord_aux with
| Ord_var kid ->
begin
@@ -674,6 +680,7 @@ end = struct
end
| Ord_inc | Ord_dec -> ()
and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc_aux, l) as nc) =
+ wf_debug "constraint" string_of_n_constraint nc exs;
match nc_aux with
| NC_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
| NC_not_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2
@@ -690,6 +697,7 @@ end = struct
| NC_or (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
| NC_and (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2
| NC_app (id, args) -> List.iter (wf_typ_arg ~exs:exs env) args
+ | NC_var kid when KidSet.mem kid exs -> ()
| NC_var kid ->
begin match get_typ_var kid env with
| K_bool -> ()
@@ -1031,8 +1039,9 @@ end = struct
let get_constraints env = env.constraints
- let add_constraint (NC_aux (nc_aux, l) as constr) env =
+ let add_constraint constr env =
wf_constraint env constr;
+ let (NC_aux (nc_aux, l) as constr) = expand_constraint_synonyms env constr in
match nc_aux with
| NC_true -> env
| _ ->
@@ -1261,6 +1270,7 @@ let solve env nexp = failwith "WIP"
let prove env nc =
typ_print (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc));
let (NC_aux (nc_aux, _) as nc) = Env.expand_constraint_synonyms env nc in
+ typ_debug ~level:2 (lazy (Util.("Prove " |> red |> clear) ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env) ^ " |- " ^ string_of_n_constraint nc));
let compare_const f (Nexp_aux (n1, _)) (Nexp_aux (n2, _)) =
match n1, n2 with
| Nexp_constant c1, Nexp_constant c2 when f c1 c2 -> true
@@ -1362,6 +1372,7 @@ let rec nc_identical (NC_aux (nc1, _)) (NC_aux (nc2, _)) =
| NC_false, NC_false -> true
| NC_set (kid1, ints1), NC_set (kid2, ints2) when List.length ints1 = List.length ints2 ->
Kid.compare kid1 kid2 = 0 && List.for_all2 (fun i1 i2 -> i1 = i2) ints1 ints2
+ | NC_var kid1, NC_var kid2 -> Kid.compare kid1 kid2 = 0
| _, _ -> false
let typ_identical env typ1 typ2 =
@@ -1449,8 +1460,15 @@ and unify_typ_arg l env goals (A_aux (aux1, _) as typ_arg1) (A_aux (aux2, _) as
| A_typ typ1, A_typ typ2 -> unify_typ l env goals typ1 typ2
| A_nexp nexp1, A_nexp nexp2 -> unify_nexp l env goals nexp1 nexp2
| A_order ord1, A_order ord2 -> unify_order l goals ord1 ord2
+ | A_bool nc1, A_bool nc2 -> unify_constraint l goals nc1 nc2
| _, _ -> unify_error l ("Could not unify type arguments " ^ string_of_typ_arg typ_arg1 ^ " and " ^ string_of_typ_arg typ_arg2)
+and unify_constraint l goals (NC_aux (aux1, _) as nc1) (NC_aux (aux2, _) as nc2) =
+ typ_debug (lazy (Util.("Unify constraint " |> magenta |> clear) ^ string_of_n_constraint nc1 ^ " and " ^ string_of_n_constraint nc2));
+ match aux1, aux2 with
+ | NC_var v, _ when KidSet.mem v goals -> KBindings.singleton v (arg_bool nc2)
+ | _, _ -> unify_error l ("Could not unify constraints " ^ string_of_n_constraint nc1 ^ " and " ^ string_of_n_constraint nc2)
+
and unify_order l goals (Ord_aux (aux1, _) as ord1) (Ord_aux (aux2, _) as ord2) =
typ_print (lazy (Util.("Unify order " |> magenta |> clear) ^ string_of_order ord1 ^ " and " ^ string_of_order ord2));
match aux1, aux2 with
@@ -1594,6 +1612,7 @@ let rec kid_order_nexp kind_map (Nexp_aux (aux, l) as nexp) =
| Nexp_app (id, nexps) ->
List.fold_left (fun (ord, kids) nexp -> let (ord', kids) = kid_order_nexp kids nexp in (ord @ ord', kids)) ([], kind_map) nexps
+
let rec kid_order kind_map (Typ_aux (aux, l) as typ) =
match aux with
| Typ_var kid when KBindings.mem kid kind_map ->
@@ -1605,11 +1624,18 @@ let rec kid_order kind_map (Typ_aux (aux, l) as typ) =
List.fold_left (fun (ord, kids) arg -> let (ord', kids) = kid_order_arg kids arg in (ord @ ord', kids)) ([], kind_map) args
| Typ_fn _ | Typ_bidir _ | Typ_exist _ -> typ_error l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ)
| Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
-and kid_order_arg kids (A_aux (aux, l) as arg) =
+and kid_order_arg kind_map (A_aux (aux, l) as arg) =
match aux with
- | A_typ typ -> kid_order kids typ
- | A_nexp nexp -> kid_order_nexp kids nexp
- | A_order _ -> ([], kids)
+ | A_typ typ -> kid_order kind_map typ
+ | A_nexp nexp -> kid_order_nexp kind_map nexp
+ | A_bool nc -> kid_order_constraint kind_map nc
+ | 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 ->
+ ([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"
let rec alpha_equivalent env typ1 typ2 =
let counter = ref 0 in
@@ -1742,8 +1768,10 @@ let rec subtyp l env typ1 typ2 =
match typ_aux1, typ_aux2 with
| _, Typ_internal_unknown when Env.allow_unknowns env -> ()
- | Typ_app (id1, _), Typ_id id2 when string_of_id id1 = "atom_bool" && string_of_id id2 = "bool" -> ()
-
+ | Typ_app (id1, _), Typ_id id2 when string_of_id id1 = "atom_bool" && string_of_id id2 = "bool" ->
+ typ_debug (lazy "Boolean subtype");
+ ()
+
| Typ_tup typs1, Typ_tup typs2 when List.length typs1 = List.length typs2 ->
List.iter2 (subtyp l env) typs1 typs2
@@ -1762,7 +1790,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 -> assert false
+ | A_bool nc1, A_bool nc2 when nc_identical nc1 nc2 -> ()
| _, _ -> typ_error l "Mismatched argument types in subtype check"
let typ_equality l env typ1 typ2 =
@@ -1997,6 +2025,7 @@ let rec combine_constraint b f x y = match b, x, y with
| _, _, _ -> None
let rec assert_constraint env b (E_aux (exp_aux, _) as exp) =
+ typ_debug ~level:2 (lazy ("Asserting constraint for " ^ string_of_exp exp ^ " : " ^ string_of_typ (typ_of exp)));
match typ_of exp with
| Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _) ->
Some nc
@@ -2243,14 +2272,11 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
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_sizeof nexp, _)]), _ when Id.compare f (mk_id "__solve") = 0 ->
- Env.wf_nexp env nexp;
- begin match solve env nexp with
- | None -> typ_error l ("Coud not solve " ^ string_of_nexp nexp)
- | Some n ->
- print_endline ("Solved " ^ string_of_nexp nexp ^ " = " ^ Big_int.to_string n);
- annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
- end
+ | E_app (f, [E_aux (E_constraint nc, _)]), _ when Id.compare f (mk_id "_not_prove") = 0 ->
+ 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
(* 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 ->
@@ -2295,10 +2321,19 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
let inferred_exp = infer_funapp l env f xs (Some typ) in
type_coercion env inferred_exp typ
| E_if (cond, then_branch, else_branch), _ ->
- let cond' = crule check_exp env cond (mk_typ (Typ_id (mk_id "bool"))) in
- let then_branch' = crule check_exp (add_opt_constraint (assert_constraint env true cond') env) then_branch typ in
- let else_branch' = crule check_exp (add_opt_constraint (option_map nc_not (assert_constraint env false cond')) env) else_branch typ in
- annot_exp (E_if (cond', then_branch', else_branch')) typ
+ (* let cond' = crule check_exp env cond (mk_typ (Typ_id (mk_id "bool"))) in *)
+ let cond' = irule infer_exp env cond in
+ begin match destruct_exist (typ_of cond') with
+ | Some (kopts, nc, Typ_aux (Typ_app (ab, [A_aux (A_bool flow, _)]), _)) when string_of_id ab = "atom_bool" ->
+ let env = add_existential l kopts nc env in
+ let then_branch' = crule check_exp (Env.add_constraint flow env) then_branch typ in
+ let else_branch' = crule check_exp (Env.add_constraint flow env) else_branch typ in
+ annot_exp (E_if (cond', then_branch', else_branch')) typ
+ | _ ->
+ let then_branch' = crule check_exp (add_opt_constraint (assert_constraint env true cond') env) then_branch typ in
+ let else_branch' = crule check_exp (add_opt_constraint (option_map nc_not (assert_constraint env false cond')) env) else_branch typ in
+ annot_exp (E_if (cond', then_branch', else_branch')) typ
+ end
| E_exit exp, _ ->
let checked_exp = crule check_exp env exp (mk_typ (Typ_id (mk_id "unit"))) in
annot_exp_effect (E_exit checked_exp) typ (mk_effect [BE_escape])
@@ -3251,7 +3286,7 @@ and infer_funapp' l env f (typq, f_typ) xs expected_ret_typ =
let updated_unifiers = KBindings.map (subst_unifiers_typ_arg unifiers) previous_unifiers in
all_unifiers := merge_uvars l updated_unifiers unifiers;
in
-
+
let quants, typ_args, typ_ret, eff =
match Env.expand_synonyms env f_typ with
| Typ_aux (Typ_fn (typ_args, typ_ret, eff), _) -> ref (quant_items typq), typ_args, ref typ_ret, eff
@@ -4271,6 +4306,10 @@ let check_type_union env variant typq (Tu_aux (tu, l)) =
(* FIXME: This code is duplicated with general kind-checking code in environment, can they be merged? *)
let mk_synonym typq typ_arg =
let kopts, ncs = quant_split typq in
+ let kopts = List.map (fun kopt -> kopt, fresh_existential (unaux_kind (kopt_kind kopt))) kopts in
+ let ncs = List.map (fun nc -> List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts) ncs in
+ let typ_arg = List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts in
+ let kopts = List.map snd kopts in
let rec subst_args kopts args =
match kopts, args with
| kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_nat_kopt kopt ->
@@ -4283,7 +4322,7 @@ let mk_synonym typq typ_arg =
| kopt :: kopts, A_aux (A_order arg, _) :: args when is_order_kopt kopt ->
let typ_arg, ncs = subst_args kopts args in
typ_arg_subst (kopt_kid kopt) (arg_order arg) typ_arg, ncs
- | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_order_kopt kopt ->
+ | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt ->
let typ_arg, ncs = subst_args kopts args in
typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs
| [], [] -> typ_arg, ncs
@@ -4310,11 +4349,8 @@ let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
fun env (TD_aux (tdef, (l, _))) ->
let td_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Typedef") in
match tdef with
- | TD_abbrev (id, typq, (A_aux (A_typ _, _) as typ_arg)) ->
- [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ_arg) env
- (* For type synonyms for non-Type kinds we omit them from the AST *)
| TD_abbrev (id, typq, typ_arg) ->
- [], Env.add_typ_synonym id (mk_synonym typq typ_arg) env
+ [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ_arg) env
| TD_record (id, nmscm, typq, fields, _) ->
[DEF_type (TD_aux (tdef, (l, None)))], Env.add_record id typq fields env
| TD_variant (id, nmscm, typq, arms, _) ->
diff --git a/src/type_check.mli b/src/type_check.mli
index 0a0e18f7..04ff48f7 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -84,7 +84,7 @@ type type_error =
exception Type_error of l * type_error;;
-val typ_debug : string Lazy.t -> unit
+val typ_debug : ?level:int -> string Lazy.t -> unit
val typ_print : string Lazy.t -> unit
(** {2 Environments} *)
diff --git a/test/typecheck/future/bool_constraint.sail b/test/typecheck/future/bool_constraint.sail
index 53994630..cce078ef 100644
--- a/test/typecheck/future/bool_constraint.sail
+++ b/test/typecheck/future/bool_constraint.sail
@@ -7,4 +7,39 @@ val foo : forall ('n : Int) ('b : Bool).
function foo(b, n) = {
if b then n else 3
+}
+
+/* We now allow type synonyms for kinds other that Type */
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val my_not = {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> {('q : Bool), 'p <--> 'q. bool('q)}
+
+/* This example mimics 32-bit ARM instructions where a flag in the
+function argument restricts a type variable in a specific branch of
+the code */
+
+val test : forall ('n : Int) ('b : Bool), 0 <= 'n <= 15 & implies('b, 'n <= 14).
+ (bool('b), int('n)) -> unit
+
+function test(cond, n) = {
+ if cond then {
+ _prove(constraint('n <= 14))
+ } else {
+ ()
+ };
+
+ if my_not(cond) then {
+ ()
+ } else {
+ _prove(constraint('n <= 14))
+ }
} \ No newline at end of file
diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect
index e4e4fa55..a647ef00 100644
--- a/test/typecheck/pass/exist_synonym/v3.expect
+++ b/test/typecheck/pass/exist_synonym/v3.expect
@@ -1,3 +1,3 @@
Type error at no location information available
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8)
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8)
diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect
index 622b5fd7..d8bad777 100644
--- a/test/typecheck/pass/exist_synonym/v4.expect
+++ b/test/typecheck/pass/exist_synonym/v4.expect
@@ -1,3 +1,3 @@
Type error at no location information available
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8)
+Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex3#n & 'ex3#n <= 8), (0 <= 'ex2#n & 'ex2#n <= 8)
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
index c7e06dc7..43096686 100644
--- a/test/typecheck/pass/global_type_var/v3.expect
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -2,4 +2,4 @@ Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, ch
val test : forall 'size. atom('size) -> unit
-type variable 'size is already bound
+type variable ('size : Int) is already bound
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index 06df7dc5..95073799 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -4,13 +4,13 @@ Type error at file "if_infer/v1.sail", line 10, character 11 to line 10, charact
No overloadings for vector_access, tried:
bitvector_access:
- Could not resolve quantifiers for bitvector_access (0 <= 'ex41#ex40# & ('ex41#ex40# + 1) <= 3)
+ Could not resolve quantifiers for bitvector_access (0 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 3)
Try adding named type variables for
plain_vector_access:
- Could not resolve quantifiers for plain_vector_access (0 <= 'ex44#ex43# & ('ex44#ex43# + 1) <= 3)
+ Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 3)
Try adding named type variables for
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index 050e90e4..afa04343 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -4,13 +4,13 @@ Type error at file "if_infer/v2.sail", line 10, character 11 to line 10, charact
No overloadings for vector_access, tried:
bitvector_access:
- Could not resolve quantifiers for bitvector_access (0 <= 'ex41#ex40# & ('ex41#ex40# + 1) <= 4)
+ Could not resolve quantifiers for bitvector_access (0 <= 'ex42#ex41# & ('ex42#ex41# + 1) <= 4)
Try adding named type variables for
plain_vector_access:
- Could not resolve quantifiers for plain_vector_access (0 <= 'ex44#ex43# & ('ex44#ex43# + 1) <= 4)
+ Could not resolve quantifiers for plain_vector_access (0 <= 'ex45#ex44# & ('ex45#ex44# + 1) <= 4)
Try adding named type variables for
diff --git a/test/typecheck/pass/tautology.sail b/test/typecheck/pass/tautology.sail
new file mode 100644
index 00000000..f1c8bade
--- /dev/null
+++ b/test/typecheck/pass/tautology.sail
@@ -0,0 +1,65 @@
+
+type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
+
+infixr 1 -->
+
+type operator -->('p: Bool, 'q: Bool) -> Bool = implies('p, 'q)
+
+infix 1 <-->
+
+type operator <-->('p: Bool, 'q: Bool) -> Bool = ('p --> 'q) & ('q --> 'p)
+
+val tautologies : forall ('p : Bool) ('q : Bool) ('r : Bool). (bool('p), bool('q), bool('r)) -> unit effect {escape}
+
+function tautologies(p, q, r) = {
+ _not_prove(constraint('p));
+ _not_prove(constraint('q));
+ _not_prove(constraint('r));
+
+ // implication definition
+ _prove(constraint(not('p) | 'q --> ('p --> 'q)));
+ _prove(constraint(('p --> 'q) --> not('p) | 'q));
+ _prove(constraint(('p --> 'q) <--> not('p) | 'q));
+
+ // implication properties
+ _prove(constraint('p --> 'p));
+ _prove(constraint(('p --> 'q) & ('q --> 'r) --> ('p --> 'r)));
+ _prove(constraint(('p --> 'q) & 'p --> 'q));
+
+ _prove(constraint('p & 'q <--> 'q & 'p));
+ _prove(constraint('p | 'q <--> 'q | 'p));
+ _prove(constraint(('p <--> 'q) <--> ('q <--> 'p)));
+
+ // excluded middle
+ _prove(constraint('p | not('p)));
+
+ // de Morgan
+ _prove(constraint(not('p | 'q) <--> not('p) & not('q)));
+ _prove(constraint(not('p & 'q) <--> not('p) | not('q)));
+
+ // contradiction
+ _prove(constraint('p & not('p) --> false));
+ {
+ assert(constraint('p & not('p)));
+ _prove(constraint(false))
+ };
+ _not_prove(constraint(false));
+
+ _prove(constraint(('p <--> 'q) & ('p | 'q) --> ('p & 'q)));
+ _prove(constraint(('p & 'q --> 'r) <--> ('p --> 'q --> 'r)));
+
+ {
+ assert(constraint('p));
+ _prove(constraint('p))
+ };
+ _not_prove(constraint('p));
+
+ {
+ assert(constraint('p));
+ assert(constraint('p --> 'q));
+ _prove(constraint('q));
+ assert(constraint('q --> 'r));
+ _prove(constraint('r))
+ };
+ _not_prove(constraint('q));
+} \ No newline at end of file
diff --git a/test/typecheck/update_errors.sh b/test/typecheck/update_errors.sh
new file mode 100755
index 00000000..ba436daf
--- /dev/null
+++ b/test/typecheck/update_errors.sh
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+set -e
+
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+SAILDIR="$DIR/../.."
+
+
+for i in `ls $DIR/pass/ | grep sail`;
+do
+ shopt -s nullglob;
+ for file in $DIR/pass/${i%.sail}/*.sail;
+ do
+ pushd $DIR/pass > /dev/null;
+ $SAILDIR/sail ${i%.sail}/$(basename $file) 2> ${file%.sail}.expect || true;
+ popd > /dev/null
+ done
+done
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:36:02 +0000