summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.ml7
-rw-r--r--src/ast_util.mli2
-rw-r--r--src/c_backend.ml31
-rw-r--r--src/initial_check.ml13
-rw-r--r--src/interpreter.ml4
-rw-r--r--src/monomorphise.ml23
-rw-r--r--src/ocaml_backend.ml14
-rw-r--r--src/parse_ast.ml3
-rw-r--r--src/parser.mly6
-rw-r--r--src/pattern_completeness.ml2
-rw-r--r--src/pretty_print_lem.ml65
-rw-r--r--src/pretty_print_lem_ast.ml8
-rw-r--r--src/pretty_print_sail.ml4
-rw-r--r--src/rewrites.ml6
-rw-r--r--src/spec_analysis.ml4
-rw-r--r--src/state.ml4
-rw-r--r--src/type_check.ml60
-rw-r--r--src/value.ml1
18 files changed, 79 insertions, 178 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 1c74381f..591e8df2 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -54,7 +54,7 @@ module Big_int = Nat_big_num
type mut = Immutable | Mutable
-type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound
+type lvar = Register of typ | Enum of typ | Local of mut * typ | Unbound
let no_annot = (Parse_ast.Unknown, ())
@@ -1009,10 +1009,7 @@ let split_defs f (Defs defs) =
let append_ast (Defs ast1) (Defs ast2) = Defs (ast1 @ ast2)
let concat_ast asts = List.fold_right append_ast asts (Defs [])
-let type_union_id (Tu_aux (aux, _)) = match aux with
- | Tu_id id -> id
- | Tu_ty_id (_, id) -> id
-
+let type_union_id (Tu_aux (Tu_ty_id (_, id), _)) = id
let rec subst id value (E_aux (e_aux, annot) as exp) =
let wrap e_aux = E_aux (e_aux, annot) in
diff --git a/src/ast_util.mli b/src/ast_util.mli
index d1827685..de925fc3 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -58,7 +58,7 @@ type mut = Immutable | Mutable
(** [lvar] is the type of variables - they can either be registers,
local mutable or immutable variables, nullary union constructors
(i.e. None in option), or unbound identifiers *)
-type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typquant * typ | Unbound
+type lvar = Register of typ | Enum of typ | Local of mut * typ | Unbound
val no_annot : unit annot
val gen_loc : Parse_ast.l -> Parse_ast.l
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 33f6f127..2542dd42 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -80,7 +80,6 @@ let lvar_typ = function
| Local (_, typ) -> typ
| Register typ -> typ
| Enum typ -> typ
- (* | Union (_, typ) -> typ *)
| _ -> assert false
let string_of_value = function
@@ -348,8 +347,6 @@ let pp_lvar lvar doc =
string "[I/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
| Enum typ ->
string "[E/" ^^ string (string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
- | Union (typq, typ) ->
- string "[U/" ^^ string (string_of_typquant typq ^ "/" ^ string_of_typ typ |> Util.yellow |> Util.clear) ^^ string "]" ^^ doc
| Unbound -> string "[?]" ^^ doc
let pp_annot typ doc =
@@ -627,7 +624,6 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) =
| E_id id ->
let lvar = Env.lookup_id id (env_of exp) in
begin match lvar with
- | Union (_, typ) -> AE_app (id, [AV_lit (mk_lit L_unit, unit_typ)], typ)
| _ -> AE_val (AV_id (id, lvar))
end
@@ -1123,16 +1119,7 @@ let cdef_ctyps ctx = function
| CDEF_reg_dec (_, ctyp) -> [ctyp]
| CDEF_spec (_, ctyps, ctyp) -> ctyp :: ctyps
| CDEF_fundef (id, _, _, instrs) ->
- (* TODO: Move this code to DEF_fundef -> CDEF_fundef translation, and modify bytecode.ott *)
- let _, Typ_aux (fn_typ, _) =
- try Env.get_val_spec id ctx.tc_env with
- | Type_error _ ->
- (* If we can't find the function type, then it must be a nullary union constructor. *)
- begin match Env.lookup_id id ctx.tc_env with
- | Union (typq, typ) -> typq, function_typ unit_typ typ no_effect
- | _ -> failwith ("Got function identifier " ^ string_of_id id ^ " which is neither a function nor a constructor.")
- end
- in
+ let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
let arg_typs, ret_typ = match fn_typ with
| Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
| Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
@@ -1455,15 +1442,7 @@ let compile_funcall ctx id args typ =
let setup = ref [] in
let cleanup = ref [] in
- let _, Typ_aux (fn_typ, _) =
- try Env.get_val_spec id ctx.tc_env with
- | Type_error _ ->
- (* If we can't find the function type, then it must be a nullary union constructor. *)
- begin match Env.lookup_id id ctx.tc_env with
- | Union (typq, typ) -> typq, function_typ unit_typ typ no_effect
- | _ -> failwith ("Got function identifier " ^ string_of_id id ^ " which is neither a function nor a constructor.")
- end
- in
+ let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
let arg_typs, ret_typ = match fn_typ with
| Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
| Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
@@ -1892,11 +1871,7 @@ let compile_type_def ctx (TD_aux (type_def, _)) =
{ ctx with records = Bindings.add id ctors ctx.records }
| TD_variant (id, _, _, tus, _) ->
- let compile_tu (Tu_aux (tu_aux, _)) =
- match tu_aux with
- | Tu_id id -> CT_unit, id
- | Tu_ty_id (typ, id) -> ctyp_of_typ ctx typ, id
- in
+ let compile_tu (Tu_aux (Tu_ty_id (typ, id), _)) = ctyp_of_typ ctx typ, id in
let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in
CTD_variant (id, Bindings.bindings ctus),
{ ctx with variants = Bindings.add id ctus ctx.variants }
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 9da200d9..0019f18f 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -648,15 +648,9 @@ let rec to_ast_range (Parse_ast.BF_aux(r,l)) = (* TODO add check that ranges are
| Parse_ast.BF_concat(ir1,ir2) -> BF_concat( to_ast_range ir1, to_ast_range ir2)),
l)
-let to_ast_type_union k_env default_order (Parse_ast.Tu_aux(tu,l)) =
- match tu with
- | Parse_ast.Tu_ty_id(atyp,id) ->
- let typ = to_ast_typ k_env default_order atyp in
- (match typ with
- | Typ_aux(Typ_id (Id_aux (Id "unit",_)),_) ->
- Tu_aux(Tu_id(to_ast_id id),l)
- | _ -> Tu_aux(Tu_ty_id(typ, to_ast_id id), l))
- | Parse_ast.Tu_id id -> (Tu_aux(Tu_id(to_ast_id id),l))
+let to_ast_type_union k_env default_order (Parse_ast.Tu_aux (Parse_ast.Tu_ty_id (atyp, id), l)) =
+ let typ = to_ast_typ k_env default_order atyp in
+ Tu_aux (Tu_ty_id (typ, to_ast_id id), l)
let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (unit type_def) envs_out =
match td with
@@ -1042,7 +1036,6 @@ let generate_undefineds vs_ids (Defs defs) =
end
in
let undefined_tu = function
- | Tu_aux (Tu_id id, _) -> mk_exp (E_id id)
| Tu_aux (Tu_ty_id (Typ_aux (Typ_tup typs, _), id), _) ->
mk_exp (E_app (id, List.map (fun _ -> mk_lit_exp L_undef) typs))
| Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef]))
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 55dcbed0..2b24d66c 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -415,7 +415,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
| Local (Immutable, _) ->
let chain = build_letchain id gstate.letbinds orig_exp in
return chain
- | Enum _ | Union _ ->
+ | Enum _ ->
return (exp_of_value (V_ctor (string_of_id id, [])))
| _ -> failwith ("id " ^ string_of_id id)
end
@@ -568,7 +568,7 @@ and pattern_match env (P_aux (p_aux, _) as pat) value =
let open Type_check in
begin
match Env.lookup_id id env with
- | Enum _ | Union _ ->
+ | Enum _ ->
if is_ctor value && string_of_id id = fst (coerce_ctor value)
then true, Bindings.empty
else false, Bindings.empty
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 45541585..0d63a9c3 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -165,9 +165,7 @@ let pat_id_is_variable env id =
| Local _
| Register _
-> true
- | Enum _
- | Union _
- -> false
+ | Enum _ -> false
let rec is_value (E_aux (e,(l,annot))) =
let is_constructor id =
@@ -179,7 +177,7 @@ let rec is_value (E_aux (e,(l,annot))) =
| Some (env,_,_) ->
Env.is_union_constructor id env ||
(match Env.lookup_id id env with
- | Enum _ | Union _ -> true
+ | Enum _ -> true
| Unbound | Local _ | Register _ -> false)
in
match e with
@@ -1118,15 +1116,12 @@ let is_env_inconsistent env ksubsts =
let split_defs all_errors splits defs =
let no_errors_happened = ref true in
let split_constructors (Defs defs) =
- let sc_type_union q (Tu_aux (tu,l) as tua) =
- match tu with
- | Tu_id id -> [],[tua]
- | Tu_ty_id (ty,id) ->
- (match split_src_type id ty q with
- | None -> ([],[Tu_aux (Tu_ty_id (ty,id),l)])
- | Some variants ->
- ([(id,variants)],
- List.map (fun (insts, id', ty) -> Tu_aux (Tu_ty_id (ty,id'),Generated l)) variants))
+ let sc_type_union q (Tu_aux (Tu_ty_id (ty, id), l) as tua) =
+ match split_src_type id ty q with
+ | None -> ([],[Tu_aux (Tu_ty_id (ty,id),l)])
+ | Some variants ->
+ ([(id,variants)],
+ List.map (fun (insts, id', ty) -> Tu_aux (Tu_ty_id (ty,id'),Generated l)) variants)
in
let sc_type_def ((TD_aux (tda,annot)) as td) =
match tda with
@@ -2799,7 +2794,7 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
| args -> (args,assigns,empty)
| exception Not_found ->
match Env.lookup_id id (Type_check.env_of_annot (l,annot)) with
- | Enum _ | Union _ -> dempty,assigns,empty
+ | Enum _ -> dempty,assigns,empty
| Register _ -> Unknown (l, string_of_id id ^ " is a register"),assigns,empty
| _ ->
Unknown (l, string_of_id id ^ " is not in the environment"),assigns,empty
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 795b6300..c580b9fa 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -177,7 +177,6 @@ let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
match Env.lookup_id id (pat_env_of pat) with
| Local (Immutable, _) | Unbound -> zencode ctx id
| Enum _ -> zencode_upper ctx id
- | Union _ -> zencode_upper ctx id
| _ -> failwith ("Ocaml: Cannot pattern match on mutable variable or register:" ^ string_of_pat pat)
end
| P_lit lit -> ocaml_lit lit
@@ -315,7 +314,7 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
begin
match Env.lookup_id id (env_of exp) with
| Local (Immutable, _) | Unbound -> zencode ctx id
- | Enum _ | Union _ -> zencode_upper ctx id
+ | Enum _ -> zencode_upper ctx id
| Register _ when is_passed_by_name (typ_of exp) -> zencode ctx id
| Register typ ->
if !opt_trace_ocaml then
@@ -515,9 +514,8 @@ let rec ocaml_fields ctx =
| [] -> empty
let rec ocaml_cases ctx =
- let ocaml_case = function
- | Tu_aux (Tu_id id, _) -> separate space [bar; zencode_upper ctx id]
- | Tu_aux (Tu_ty_id (typ, id), _) -> separate space [bar; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
+ let ocaml_case (Tu_aux (Tu_ty_id (typ, id), _)) =
+ separate space [bar; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
in
function
| [tu] -> ocaml_case tu
@@ -525,10 +523,8 @@ let rec ocaml_cases ctx =
| [] -> empty
let rec ocaml_exceptions ctx =
- let ocaml_exception = function
- | Tu_aux (Tu_id id, _) -> separate space [string "exception"; zencode_upper ctx id]
- | Tu_aux (Tu_ty_id (typ, id), _) ->
- separate space [string "exception"; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
+ let ocaml_exception (Tu_aux (Tu_ty_id (typ, id), _)) =
+ separate space [string "exception"; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
in
function
| [tu] -> ocaml_exception tu
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index ba948040..635aa46e 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -361,8 +361,7 @@ funcl_aux = (* Function clause *)
type
type_union_aux = (* Type union constructors *)
- Tu_id of id
- | Tu_ty_id of atyp * id
+ Tu_ty_id of atyp * id
type
diff --git a/src/parser.mly b/src/parser.mly
index c8cc49a3..7e4874f8 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -677,6 +677,8 @@ atomic_pat:
| kid
{ mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos,
mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos }
+ | id Unit
+ { mk_pat (P_app ($1, [mk_pat P_wild $startpos $endpos])) $startpos $endpos }
| id Lparen pat_list Rparen
{ mk_pat (P_app ($1, $3)) $startpos $endpos }
| atomic_pat Colon typ
@@ -999,6 +1001,8 @@ atomic_exp:
{ mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
| id Lparen exp_list Rparen
{ mk_exp (E_app ($1, $3)) $startpos $endpos }
+ | Exit Unit
+ { mk_exp (E_exit (mk_lit_exp L_unit $startpos $endpos)) $startpos $endpos }
| Exit Lparen exp Rparen
{ mk_exp (E_exit $3) $startpos $endpos }
| Sizeof Lparen typ Rparen
@@ -1155,8 +1159,6 @@ struct_fields:
type_union:
| id Colon typ
{ Tu_aux (Tu_ty_id ($3, $1), loc $startpos $endpos) }
- | id
- { Tu_aux (Tu_id $1, loc $startpos $endpos) }
type_unions:
| type_union
diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index 94623e6f..c13452ff 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -97,7 +97,7 @@ let rec generalize ctx (P_aux (p_aux, _) as pat) =
| Unbound -> GP_wild
| Local (Immutable, _) -> GP_wild
| Register _ | Local (Mutable, _) -> Util.warn "Matching on register or mutable variable"; GP_wild
- | Enum _ | Union _ -> GP_app (Bindings.singleton id GP_wild)
+ | Enum _ -> GP_app (Bindings.singleton id GP_wild)
end
| P_var (pat, _) -> generalize ctx pat
| P_vector pats ->
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index a0390a94..f2136f07 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -445,24 +445,22 @@ let doc_typschm_lem quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
else pt
let is_ctor env id = match Env.lookup_id id env with
-| Enum _ | Union _ -> true
+| Enum _ -> true
| _ -> false
(*Note: vector concatenation, literal vectors, indexed vectors, and record should
be removed prior to pp. The latter two have never yet been seen
*)
let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
+ | P_app(id, _) when string_of_id id = "None" -> string "Nothing"
| P_app(id, ((_ :: _) as pats)) ->
let ppp = doc_unop (doc_id_lem_ctor id)
(parens (separate_map comma (doc_pat_lem ctxt true) pats)) in
if apat_needed then parens ppp else ppp
- | P_app(id,[]) -> doc_id_lem_ctor id
+ | P_app(id, []) -> doc_id_lem_ctor id
| P_lit lit -> doc_lit_lem lit
| P_wild -> underscore
- | P_id id ->
- begin match id with
- | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
- | _ -> doc_id_lem id end
+ | P_id id -> doc_id_lem id
| P_var(p,_) -> doc_pat_lem ctxt true p
| P_as(p,id) -> parens (separate space [doc_pat_lem ctxt true p; string "as"; doc_id_lem id])
| P_typ(Typ_aux (Typ_tup typs, _), P_aux (P_tup pats, _)) ->
@@ -614,6 +612,7 @@ let doc_exp_lem, doc_let_lem =
| E_app(f,args) ->
begin match f with
(* temporary hack to make the loop body a function of the temporary variables *)
+ | Id_aux (Id "None", _) as none -> doc_id_lem_ctor none
| Id_aux (Id "foreach", _) ->
begin
match args with
@@ -681,7 +680,7 @@ let doc_exp_lem, doc_let_lem =
end
| _ ->
begin match annot with
- | Some (env, _, _) when (is_ctor env f) ->
+ | Some (env, _, _) when Env.is_union_constructor f env ->
let epp =
match args with
| [] -> doc_id_lem_ctor f
@@ -899,10 +898,9 @@ let doc_exp_lem, doc_let_lem =
in top_exp, let_exp
(*TODO Upcase and downcase type and constructors as needed*)
-let doc_type_union_lem (Tu_aux(typ_u,_)) = match typ_u with
- | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor id; string "of";
- parens (doc_typ_lem typ)]
- | Tu_id id -> separate space [pipe; doc_id_lem_ctor id]
+let doc_type_union_lem (Tu_aux(Tu_ty_id(typ,id),_)) =
+ separate space [pipe; doc_id_lem_ctor id; string "of";
+ parens (doc_typ_lem typ)]
let rec doc_range_lem (BF_aux(r,_)) = match r with
| BF_single i -> parens (doc_op comma (doc_int i) (doc_int i))
@@ -995,19 +993,12 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
(separate space [string "let rec";fromInterpValueF;string "v";equals;string "match v with"])
(
((separate_map (break 1))
- (fun (Tu_aux (tu,_)) ->
- match tu with
- | Tu_ty_id (ty,cid) ->
- (separate space)
- [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
- arrow;
- doc_id_lem_ctor cid;
- parens (string "fromInterpValue v")]
- | Tu_id cid ->
- (separate space)
- [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
- arrow;
- doc_id_lem_ctor cid])
+ (fun (Tu_aux (Tu_ty_id (ty,cid),_)) ->
+ (separate space)
+ [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+ arrow;
+ doc_id_lem_ctor cid;
+ parens (string "fromInterpValue v")])
ar) ^/^
((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^
@@ -1024,24 +1015,14 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
(separate space [string "let";toInterpValueF;equals;string "function"])
(
((separate_map (break 1))
- (fun (Tu_aux (tu,_)) ->
- match tu with
- | Tu_ty_id (ty,cid) ->
- (separate space)
- [pipe;doc_id_lem_ctor cid;string "v";arrow;
- string "SI.V_ctor";
- parens (make_id false cid);
- parens (string "SIA.T_id " ^^ string_lit (doc_id id));
- string "SI.C_Union";
- parens (string "toInterpValue v")]
- | Tu_id cid ->
- (separate space)
- [pipe;doc_id_lem_ctor cid;arrow;
- string "SI.V_ctor";
- parens (make_id false cid);
- parens (string "SIA.T_id " ^^ string_lit (doc_id id));
- string "SI.C_Union";
- parens (string "toInterpValue ()")])
+ (fun (Tu_aux (Tu_ty_id (ty,cid),_)) ->
+ (separate space)
+ [pipe;doc_id_lem_ctor cid;string "v";arrow;
+ string "SI.V_ctor";
+ parens (make_id false cid);
+ parens (string "SIA.T_id " ^^ string_lit (doc_id id));
+ string "SI.C_Union";
+ parens (string "toInterpValue v")])
ar) ^/^
string "end") in
let fromToInterpValuePP =
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 63661bb9..559c1116 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -517,11 +517,9 @@ let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
| TD_variant(id,nm,typq,ar,_) ->
- let a_pp ppf (Tu_aux(typ_u,l)) =
- match typ_u with
- | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]"
- pp_lem_typ typ pp_lem_id id pp_lem_l l
- | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l
+ let a_pp ppf (Tu_aux(Tu_ty_id(typ,id),l)) =
+ fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]"
+ pp_lem_typ typ pp_lem_id id pp_lem_l l
in
fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 7620ca50..29284262 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -456,9 +456,7 @@ let doc_dec (DEC_aux (reg,_)) =
let doc_field (typ, id) =
separate space [doc_id id; colon; doc_typ typ]
-let doc_union (Tu_aux (tu, l)) = match tu with
- | Tu_id id -> doc_id id
- | Tu_ty_id (typ, id) -> separate space [doc_id id; colon; doc_typ typ]
+let doc_union (Tu_aux (Tu_ty_id (typ, id), l)) = separate space [doc_id id; colon; doc_typ typ]
let doc_typdef (TD_aux(td,_)) = match td with
| TD_abbrev (id, _, typschm) ->
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 50a8ae68..0b4a864c 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1952,10 +1952,8 @@ let rewrite_constraint =
rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_e_constraint) }
-let rewrite_type_union_typs rw_typ (Tu_aux (tu, annot)) =
- match tu with
- | Tu_id id -> Tu_aux (Tu_id id, annot)
- | Tu_ty_id (typ, id) -> Tu_aux (Tu_ty_id (rw_typ typ, id), annot)
+let rewrite_type_union_typs rw_typ (Tu_aux (Tu_ty_id (typ, id), annot)) =
+ Tu_aux (Tu_ty_id (rw_typ typ, id), annot)
let rewrite_type_def_typs rw_typ rw_typquant rw_typschm (TD_aux (td, annot)) =
match td with
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 371acfdc..74312d9b 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -289,9 +289,7 @@ let init_env s = Nameset.singleton s
let typ_variants consider_var bound tunions =
List.fold_right
- (fun (Tu_aux(t,_)) (b,n) -> match t with
- | Tu_id id -> Nameset.add (string_of_id id) b,n
- | Tu_ty_id(t,id) -> Nameset.add (string_of_id id) b, fv_of_typ consider_var b n t)
+ (fun (Tu_aux(Tu_ty_id(t,id),_)) (b,n) -> Nameset.add (string_of_id id) b, fv_of_typ consider_var b n t)
tunions
(bound,mt)
diff --git a/src/state.ml b/src/state.ml
index 690c7948..8e024179 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -144,7 +144,7 @@ let add_regval_conv id typ defs =
let from_val = Printf.sprintf "val %s : register_value -> option(%s)" from_name typ_str in
let from_function = String.concat "\n" [
Printf.sprintf "function %s Regval_%s(v) = Some(v)" from_name id;
- Printf.sprintf "and %s _ = None" from_name
+ Printf.sprintf "and %s _ = None()" from_name
] in
let from_defs = if is_defined from_name then [] else [from_val; from_function] in
(* Create a function that converts from target type to regval. *)
@@ -316,7 +316,7 @@ let generate_regstate_defs mwords defs =
let regtyps = register_base_types mwords (List.map fst registers) in
let option_typ =
if has_def "option" then [] else
- ["union option ('a : Type) = {None, Some : 'a}"]
+ ["union option ('a : Type) = {None : unit, Some : 'a}"]
in
let regval_typ = if has_def "register_value" then [] else generate_regval_typ regtyps in
let regstate_typ = if has_def "regstate" then [] else generate_regstate registers in
diff --git a/src/type_check.ml b/src/type_check.ml
index 16e5bed2..ff4240aa 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -674,7 +674,6 @@ end = struct
let is_union_constructor id env =
let is_ctor id (Tu_aux (tu, _)) = match tu with
- | Tu_id ctor_id when Id.compare id ctor_id = 0 -> true
| Tu_ty_id (_, ctor_id) when Id.compare id ctor_id = 0 -> true
| _ -> false
in
@@ -835,14 +834,7 @@ end = struct
let (enum, _) = List.find (fun (enum, ctors) -> IdSet.mem id ctors) (Bindings.bindings env.enums) in
Enum (mk_typ (Typ_id enum))
with
- | Not_found ->
- begin
- try
- let (typq, typ) = freshen_bind env (Bindings.find id env.union_ids) in
- Union (typq, typ)
- with
- | Not_found -> Unbound
- end
+ | Not_found -> Unbound
end
end
@@ -2024,11 +2016,6 @@ let rec filter_casts env from_typ to_typ casts =
end
| [] -> []
-let is_union_id id env =
- match Env.lookup_id id env with
- | Union (_, _) -> true
- | _ -> false
-
let crule r env exp typ =
incr depth;
typ_print ("Check " ^ string_of_exp exp ^ " <= " ^ string_of_typ typ);
@@ -2246,14 +2233,6 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
if is_typ_monomorphic typ || Env.polymorphic_undefineds env
then annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef])
else typ_error l ("Type " ^ string_of_typ typ ^ " failed undefined monomorphism restriction")
- | E_id id, _ when is_union_id id env ->
- begin
- match Env.lookup_id id env with
- | Union (typq, ctor_typ) ->
- let inferred_exp = fst (infer_funapp' l env id (typq, mk_typ (Typ_fn (unit_typ, ctor_typ, no_effect))) [mk_lit_exp L_unit] (Some typ)) in
- annot_exp (E_id id) (typ_of inferred_exp)
- | _ -> assert false (* Unreachble due to guard *)
- end
| _, _ ->
let inferred_exp = irule infer_exp env exp in
type_coercion env inferred_exp typ
@@ -2381,19 +2360,18 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
match pat_aux with
| P_id v ->
begin
+ (* If the identifier we're matching on is also a constructor of
+ a union, that's probably a mistake, so warn about it. *)
+ if Env.is_union_constructor v env then
+ Util.warn (Printf.sprintf "Identifier %s found in pattern is also a union constructor at %s\n"
+ (string_of_id v)
+ (Reporting_basic.loc_to_string l))
+ else ();
match Env.lookup_id v env with
| Local (Immutable, _) | Unbound -> annot_pat (P_id v) typ, Env.add_local v (Immutable, typ) env, []
| Local (Mutable, _) | Register _ ->
typ_error l ("Cannot shadow mutable local or register in switch statement pattern " ^ string_of_pat pat)
| Enum enum -> subtyp l env enum typ; annot_pat (P_id v) typ, env, []
- | Union (typq, ctor_typ) ->
- begin
- try
- let _ = unify l env ctor_typ typ in
- annot_pat (P_id v) typ, env, []
- with
- | Unification_error (l, m) -> typ_error l ("Unification error when pattern matching against union constructor: " ^ m)
- end
end
| P_var (pat, typ_pat) ->
let typ = Env.expand_synonyms env typ in
@@ -2523,7 +2501,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) =
| P_id v ->
begin
match Env.lookup_id v env with
- | Local (Immutable, _) | Unbound | Union _ ->
+ | Local (Immutable, _) | Unbound ->
typ_error l ("Cannot infer identifier in pattern " ^ string_of_pat pat ^ " - try adding a type annotation")
| Local (Mutable, _) | Register _ ->
typ_error l ("Cannot shadow mutable local or register in switch statement pattern " ^ string_of_pat pat)
@@ -2617,7 +2595,6 @@ and bind_assignment env (LEXP_aux (lexp_aux, _) as lexp) (E_aux (_, (l, ())) as
let is_immutable, vtyp, is_register = match Env.lookup_id v env with
| Unbound -> typ_error l "Cannot assign to element of unbound vector"
| Enum _ -> typ_error l "Cannot vector assign to enumeration element"
- | Union _ -> typ_error l "Cannot vector assign to union element"
| Local (Immutable, vtyp) -> true, vtyp, false
| Local (Mutable, vtyp) -> false, vtyp, false
| Register vtyp -> false, vtyp, true
@@ -2678,8 +2655,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
end
| LEXP_id v ->
begin match Env.lookup_id v env with
- | Local (Immutable, _) | Enum _ | Union _ ->
- typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v)
+ | Local (Immutable, _) | Enum _ ->
+ typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
| Local (Mutable, vtyp) -> subtyp l env typ vtyp; annot_lexp (LEXP_id v) typ, env
| Register vtyp -> subtyp l env typ vtyp; annot_lexp_effect (LEXP_id v) typ (mk_effect [BE_wreg]), env
| Unbound -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
@@ -2687,8 +2664,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
| LEXP_cast (typ_annot, v) ->
begin
match Env.lookup_id v env with
- | Local (Immutable, _) | Enum _ | Union _ ->
- typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v)
+ | Local (Immutable, _) | Enum _ ->
+ typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
| Local (Mutable, vtyp) ->
begin
subtyp l env typ typ_annot;
@@ -2732,8 +2709,8 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
| LEXP_aux (LEXP_id v, _) ->
begin
match Env.lookup_id v env with
- | Local (Immutable, _) | Enum _ | Union _ ->
- typ_error l ("Cannot modify let-bound constant, union or enumeration constructor " ^ string_of_id v)
+ | Local (Immutable, _) | Enum _ ->
+ typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
| Unbound ->
typ_error l "Unbound variable in vector tuple assignment"
| Local (Mutable, vtyp) | Register vtyp ->
@@ -2773,7 +2750,6 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
let is_immutable, is_register, vtyp = match Env.lookup_id v env with
| Unbound -> typ_error l "Cannot assign to element of unbound vector"
| Enum _ -> typ_error l "Cannot vector assign to enumeration element"
- | Union _ -> typ_error l "Cannot vector assign to union element"
| Local (Immutable, vtyp) -> true, false, vtyp
| Local (Mutable, vtyp) -> false, false, vtyp
| Register vtyp -> false, true, vtyp
@@ -2798,7 +2774,6 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
let is_immutable, is_register, vtyp = match Env.lookup_id v env with
| Unbound -> typ_error l "Cannot assign to element of unbound vector"
| Enum _ -> typ_error l "Cannot vector assign to enumeration element"
- | Union _ -> typ_error l "Cannot vector assign to union element"
| Local (Immutable, vtyp) -> true, false, vtyp
| Local (Mutable, vtyp) -> false, false, vtyp
| Register vtyp -> false, true, vtyp
@@ -2840,10 +2815,6 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
| Local (_, typ) | Enum typ -> annot_exp (E_id v) typ
| Register typ -> annot_exp_effect (E_id v) typ (mk_effect [BE_rreg])
| Unbound -> typ_error l ("Identifier " ^ string_of_id v ^ " is unbound")
- | Union (typq, typ) ->
- if quant_items typq = []
- then annot_exp (E_id v) typ
- else typ_error l ("Cannot infer the type of polymorphic union indentifier " ^ string_of_id v)
end
| E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit)
| E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)])))
@@ -3610,7 +3581,6 @@ let fold_union_quant quants (QI_aux (qi, l)) =
let check_type_union env variant typq (Tu_aux (tu, l)) =
let ret_typ = app_typ variant (List.fold_left fold_union_quant [] (quant_items typq)) in
match tu with
- | Tu_id v -> Env.add_union_id v (typq, ret_typ) env
| Tu_ty_id (typ, v) ->
let typ' = mk_typ (Typ_fn (typ, ret_typ, no_effect)) in
env
diff --git a/src/value.ml b/src/value.ml
index 077ad883..f865fea1 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -434,6 +434,7 @@ let primops =
("sub_vec", value_sub_vec);
("read_ram", value_read_ram);
("write_ram", value_write_ram);
+ ("undefined_unit", fun _ -> V_unit);
("undefined_bit", fun _ -> V_bit Sail_lib.B0);
("undefined_int", fun _ -> V_int Big_int.zero);
("undefined_bool", fun _ -> V_bool false);
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 13:27:41 +0000