Remove implicit casts from source

These have been deprecated for a long time, so finally remove the code for them

language/sail.ott

@@ -670,27 +670,21 @@ val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::=
    {{ lem VS_aux of val_spec_aux * annot 'a }}
   | val_spec_aux ::  :: aux
 
-cast_opt :: 'Cast_' ::=
-   {{ com option cast annotation for val specs }}
-   {{ ocaml bool }} {{ lem bool }} {{ isa bool }}
-   |       :: S :: no_cast {{ ocaml false }} {{ lem false }} {{ isa false }}
-   | cast  :: S :: cast {{ ocaml true }} {{ lem true }} {{ isa true }}
-
 val_spec_aux :: 'VS_' ::=
   {{ com value type specification }}
-  {{ ocaml  VS_val_spec of typschm * id * (string * string) list * bool }}
-  {{ lem VS_val_spec of typschm * id * maybe extern * bool }}
-  {{ isa  typschm * id  * (string => string option) * bool }}  
-  | val cast_opt id : typschm                           :: S :: val_spec
+  {{ ocaml  VS_val_spec of typschm * id * extern option }}
+  {{ lem VS_val_spec of typschm * id * maybe extern }}
+  {{ isa  typschm * id  * (string => string option) }}  
+  | val id : typschm                           :: S :: val_spec
     {{ com specify the type of an upcoming definition }}
-    {{ ocaml (VS_val_spec [[typschm]] [[id]] [] [[cast_opt]]) }} {{ lem }} {{ isa }}
-  | val cast_opt string : typschm       :: S :: extern_no_rename
+    {{ ocaml (VS_val_spec [[typschm]] [[id]] []) }} {{ lem }} {{ isa }}
+  | val string : typschm       :: S :: extern_no_rename
     {{ com specify the type of an external function }}
-    {{ ocaml  (VS_val_spec [[typschm]] [[string]] [ ( "_" , [[string]] ) ] [[cast_opt]] ) }} {{ lem }} {{ isa }}
-  | val cast_opt id = string : typschm      :: S :: extern_rename_all
+    {{ ocaml  (VS_val_spec [[typschm]] [[string]] [ ( "_" , [[string]] ) ]) }} {{ lem }} {{ isa }}
+  | val id = string : typschm      :: S :: extern_rename_all
     {{ com specify the type of an external function }}
-    {{ ocaml  (VS_val_spec [[typschm]] [[id]] [ ( "_" , [[string]] ) ] [[cast_opt]] ) }} {{ lem }} {{ isa }}
-  | val cast_opt id = { string1 = string'1 , ... , stringn = string'n } : typschm :: S :: extern_rename_some
+    {{ ocaml  (VS_val_spec [[typschm]] [[id]] [ ( "_" , [[string]] ) ]) }} {{ lem }} {{ isa }}
+  | val id = { string1 = string'1 , ... , stringn = string'n } : typschm :: S :: extern_rename_some
     {{ ichlo }}
 
 

src/bin/repl.ml

@@ -197,7 +197,7 @@ let setup_sail_scripting istate =
       (fun (cmd, (_, action)) ->
         let name = sail_command_name cmd in
         let typschm = mk_typschm (mk_typquant []) (Interactive.reflect_typ action) in
-        mk_val_spec (VS_val_spec (typschm, mk_id name, Some { pure = false; bindings = [("_", name)] }, false))
+        mk_val_spec (VS_val_spec (typschm, mk_id name, Some { pure = false; bindings = [("_", name)] }))
       )
       cmds
   in

src/bin/sail.ml

@@ -175,10 +175,8 @@ let rec options =
         Arg.Set State.opt_type_grouped_regstate,
         " group registers with same type together in generated register state record"
       );
-      ( "-enum_casts",
-        Arg.Set Initial_check.opt_enum_casts,
-        " allow enumerations to be automatically casted to numeric range types"
-      );
+      (* Casts have been removed, preserved for backwards compatibility *)
+      ("-enum_casts", Arg.Unit (fun () -> ()), "");
       ("-non_lexical_flow", Arg.Set Nl_flow.opt_nl_flow, " allow non-lexical flow typing");
       ( "-no_lexp_bounds_check",
         Arg.Set Type_check.opt_no_lexp_bounds_check,
@@ -234,15 +232,9 @@ let rec options =
         Arg.Set Profile.opt_profile,
         " (debug) provide basic profiling information for rewriting passes within Sail"
       );
-      ("-dno_cast", Arg.Set Frontend.opt_dno_cast, " (debug) typecheck without any implicit casting");
-      ( "-dallow_cast",
-        Arg.Tuple
-          [
-            Arg.Unit (fun () -> Reporting.simple_warn "-dallow_cast option is deprecated");
-            Arg.Clear Frontend.opt_dno_cast;
-          ],
-        " (debug) typecheck allowing implicit casting (deprecated)"
-      );
+      ("-dno_cast", Arg.Unit (fun () -> ()), "");
+      (* No longer does anything, preserved for backwards compatibility only *)
+      ("-dallow_cast", Arg.Unit (fun () -> ()), "");
       ( "-ddump_rewrite_ast",
         Arg.String
           (fun l ->

src/lib/ast_util.ml

@@ -1128,7 +1128,7 @@ let id_of_type_def_aux = function
       id
 let id_of_type_def (TD_aux (td_aux, _)) = id_of_type_def_aux td_aux
 
-let id_of_val_spec (VS_aux (VS_val_spec (_, id, _, _), _)) = id
+let id_of_val_spec (VS_aux (VS_val_spec (_, id, _), _)) = id
 
 let id_of_dec_spec (DEC_aux (DEC_reg (_, id, _), _)) = id
 
@@ -1160,7 +1160,7 @@ let ids_of_defs defs = List.fold_left IdSet.union IdSet.empty (List.map ids_of_d
 let ids_of_ast ast = ids_of_defs ast.defs
 
 let val_spec_ids defs =
-  let val_spec_id (VS_aux (vs_aux, _)) = match vs_aux with VS_val_spec (_, id, _, _) -> id in
+  let val_spec_id (VS_aux (vs_aux, _)) = match vs_aux with VS_val_spec (_, id, _) -> id in
   let rec vs_ids = function
     | DEF_aux (DEF_val vs, _) :: defs -> val_spec_id vs :: vs_ids defs
     | _ :: defs -> vs_ids defs
@@ -1548,7 +1548,7 @@ let construct_mpexp (mpat, guard, ann) =
   match guard with None -> MPat_aux (MPat_pat mpat, ann) | Some guard -> MPat_aux (MPat_when (mpat, guard), ann)
 
 let is_valspec id = function
-  | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id', _, _), _)), _) when Id.compare id id' = 0 -> true
+  | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id', _), _)), _) when Id.compare id id' = 0 -> true
   | _ -> false
 
 let is_fundef id = function
@@ -1557,8 +1557,8 @@ let is_fundef id = function
       true
   | _ -> false
 
-let rename_valspec id (VS_aux (VS_val_spec (typschm, _, externs, is_cast), annot)) =
-  VS_aux (VS_val_spec (typschm, id, externs, is_cast), annot)
+let rename_valspec id (VS_aux (VS_val_spec (typschm, _, externs), annot)) =
+  VS_aux (VS_val_spec (typschm, id, externs), annot)
 
 let rename_funcl id (FCL_aux (FCL_funcl (_, pexp), annot)) = FCL_aux (FCL_funcl (id, pexp), annot)
 

src/lib/bitfield.ml

@@ -95,7 +95,7 @@ let range_width r = List.map slice_width (indices_of_range r) |> List.fold_left
 (* Generate a constructor function for a bitfield type *)
 let constructor name order size =
   let typschm = fun_typschm [bitvec_typ size order] (mk_id_typ name) in
-  let constructor_val = mk_val_spec (VS_val_spec (typschm, prepend_id "Mk_" name, None, false)) in
+  let constructor_val = mk_val_spec (VS_val_spec (typschm, prepend_id "Mk_" name, None)) in
   let constructor_fun = Printf.sprintf "function Mk_%s v = struct { bits = v }" (string_of_id name) in
   constructor_val :: defs_of_string __POS__ constructor_fun
 
@@ -160,7 +160,7 @@ let field_getter typ_name field order range =
   let size = range_width range in
   let typschm = fun_typschm [mk_id_typ typ_name] (bitvec_typ size order) in
   let fun_id = (field_accessor_ids typ_name field).get in
-  let spec = mk_val_spec (VS_val_spec (typschm, fun_id, None, false)) in
+  let spec = mk_val_spec (VS_val_spec (typschm, fun_id, None)) in
   let body = get_field_exp range (get_bits_field (mk_exp (E_id (mk_id "v")))) in
   let funcl = mk_funcl fun_id (mk_pat (P_id (mk_id "v"))) body in
   [spec; mk_fundef [funcl]]
@@ -170,7 +170,7 @@ let field_updater typ_name field order range =
   let typ = mk_id_typ typ_name in
   let typschm = fun_typschm [typ; bitvec_typ size order] typ in
   let fun_id = (field_accessor_ids typ_name field).update in
-  let spec = mk_val_spec (VS_val_spec (typschm, fun_id, None, false)) in
+  let spec = mk_val_spec (VS_val_spec (typschm, fun_id, None)) in
   let orig_var = mk_id "v" in
   let new_val_var = mk_id "x" in
   let bits_exp = get_bits_field (mk_id_exp orig_var) in

src/lib/callgraph.ml

@@ -288,7 +288,7 @@ let add_def_to_graph graph (DEF_aux (def, _)) =
 
   let scan_outcome_def l outcome (DEF_aux (aux, _)) =
     match aux with
-    | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), _, _, _), _)) ->
+    | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), _, _), _)) ->
         graph := G.add_edges outcome [] !graph;
         scan_typquant outcome typq;
         IdSet.iter (fun typ_id -> graph := G.add_edge outcome (Type typ_id) !graph) (typ_ids typ)
@@ -306,7 +306,7 @@ let add_def_to_graph graph (DEF_aux (def, _)) =
 
   begin
     match def with
-    | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, (Typ_aux (Typ_bidir _, _) as typ)), _), id, _, _), _))
+    | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, (Typ_aux (Typ_bidir _, _) as typ)), _), id, _), _))
       ->
         graph := G.add_edges (Mapping id) [] !graph;
         List.iter
@@ -319,7 +319,7 @@ let add_def_to_graph graph (DEF_aux (def, _)) =
           ];
         scan_typquant (Mapping id) typq;
         IdSet.iter (fun typ_id -> graph := G.add_edge (Mapping id) (Type typ_id) !graph) (typ_ids typ)
-    | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), id, _, _), _)) ->
+    | DEF_val (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), _), id, _), _)) ->
         graph := G.add_edges (Function id) [] !graph;
         scan_typquant (Function id) typq;
         IdSet.iter (fun typ_id -> graph := G.add_edge (Function id) (Type typ_id) !graph) (typ_ids typ)

src/lib/chunk_ast.ml

@@ -108,7 +108,7 @@ type chunk =
       return_typ_opt : chunks option;
       funcls : pexp_chunks list;
     }
-  | Val of { is_cast : bool; id : id; extern_opt : extern option; typq_opt : chunks option; typ : chunks }
+  | Val of { id : id; extern_opt : extern option; typq_opt : chunks option; typ : chunks }
   | Enum of { id : id; enum_functions : chunks list option; members : chunks list }
   | Function_typ of { mapping : bool; lhs : chunks; rhs : chunks }
   | Exists of { vars : chunks; constr : chunks; typ : chunks }
@@ -223,9 +223,7 @@ let rec prerr_chunk indent = function
           Queue.iter (prerr_chunk (indent ^ "    ")) funcl.body
         )
         fn.funcls
-  | Val vs ->
-      Printf.eprintf "%sVal:%s is_cast=%b has_extern=%b\n" indent (string_of_id vs.id) vs.is_cast
-        (Option.is_some vs.extern_opt)
+  | Val vs -> Printf.eprintf "%sVal:%s has_extern=%b\n" indent (string_of_id vs.id) (Option.is_some vs.extern_opt)
   | Enum e ->
       Printf.eprintf "%sEnum:%s\n" indent (string_of_id e.id);
       begin
@@ -1083,7 +1081,7 @@ let chunk_fundef comments chunks (FD_aux (FD_function (rec_opt, tannot_opt, _, f
   let funcls = List.map (chunk_funcl comments) funcls in
   Function { id = fn_id; clause = false; rec_opt = None; typq_opt; return_typ_opt; funcls } |> add_chunk chunks
 
-let chunk_val_spec comments chunks (VS_aux (VS_val_spec (typschm, id, extern_opt, is_cast), l)) =
+let chunk_val_spec comments chunks (VS_aux (VS_val_spec (typschm, id, extern_opt), l)) =
   pop_comments comments chunks l;
   let typq_chunks_opt, typ =
     match typschm with
@@ -1095,7 +1093,7 @@ let chunk_val_spec comments chunks (VS_aux (VS_val_spec (typschm, id, extern_opt
   in
   let typ_chunks = Queue.create () in
   chunk_atyp comments typ_chunks typ;
-  add_chunk chunks (Val { is_cast; id; extern_opt; typq_opt = typq_chunks_opt; typ = typ_chunks });
+  add_chunk chunks (Val { id; extern_opt; typq_opt = typq_chunks_opt; typ = typ_chunks });
   if not (pop_trailing_comment ~space:1 comments chunks (ending_line_num l)) then Queue.push (Spacer (true, 1)) chunks
 
 let chunk_register comments chunks (DEC_aux (DEC_reg ((ATyp_aux (_, typ_l) as typ), id, opt_exp), l)) =

src/lib/chunk_ast.mli

@@ -95,13 +95,7 @@ type chunk =
       return_typ_opt : chunks option;
       funcls : pexp_chunks list;
     }
-  | Val of {
-      is_cast : bool;
-      id : Parse_ast.id;
-      extern_opt : Parse_ast.extern option;
-      typq_opt : chunks option;
-      typ : chunks;
-    }
+  | Val of { id : Parse_ast.id; extern_opt : Parse_ast.extern option; typq_opt : chunks option; typ : chunks }
   | Enum of { id : Parse_ast.id; enum_functions : chunks list option; members : chunks list }
   | Function_typ of { mapping : bool; lhs : chunks; rhs : chunks }
   | Exists of { vars : chunks; constr : chunks; typ : chunks }

src/lib/constant_propagation_mutrec.ml

@@ -154,7 +154,7 @@ let generate_val_spec env id args l annot =
       in
       let quant_items' = List.map mk_qi_kopt (KOptSet.elements kopts') @ List.map mk_qi_nc constraints' in
       let typschm = mk_typschm (mk_typquant quant_items') typ' in
-      (mk_val_spec (VS_val_spec (typschm, generate_fun_id id args, None, false)), ksubsts)
+      (mk_val_spec (VS_val_spec (typschm, generate_fun_id id args, None)), ksubsts)
   | _, Typ_aux (_, l) -> raise (Reporting.err_unreachable l __POS__ "Function val spec is not a function type")
 
 let const_prop target defs substs ksubsts exp =

src/lib/effects.ml

@@ -209,7 +209,7 @@ let infer_def_direct_effects asserts_termination def =
 
   begin
     match def with
-    | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, Some { pure = false; _ }, _), _)), _) ->
+    | DEF_aux (DEF_val (VS_aux (VS_val_spec (_, id, Some { pure = false; _ }), _)), _) ->
         effects := EffectSet.add External !effects
     | DEF_aux (DEF_fundef (FD_aux (FD_function (_, _, funcls), (l, _))), def_annot) -> begin
         match funcls_info funcls with

src/lib/format_sail.ml

@@ -529,9 +529,7 @@ module Make (Config : CONFIG) = struct
         let doc_binding (target, name) =
           string target ^^ char ':' ^^ space ^^ char '"' ^^ utf8string name ^^ char '"'
         in
-        string "val" ^^ space
-        ^^ (if vs.is_cast then string "cast" ^^ space else empty)
-        ^^ doc_id vs.id
+        string "val" ^^ space ^^ doc_id vs.id
         ^^ group
              ( match vs.extern_opt with
              | Some extern ->

src/lib/frontend.ml

@@ -72,12 +72,10 @@ module StringMap = Map.Make (String)
 
 let opt_ddump_initial_ast = ref false
 let opt_ddump_tc_ast = ref false
-let opt_dno_cast = ref true
 let opt_reformat : string option ref = ref None
 
 let check_ast (asserts_termination : bool) (env : Type_check.Env.t) (ast : uannot ast) :
     Type_check.tannot ast * Type_check.Env.t * Effects.side_effect_info =
-  let env = if !opt_dno_cast then Type_check.Env.no_casts env else env in
   let ast, env = Type_error.check env ast in
   let ast = Scattered.descatter ast in
   let side_effects = Effects.infer_side_effects asserts_termination ast in

src/lib/frontend.mli

@@ -67,7 +67,6 @@
 
 val opt_ddump_initial_ast : bool ref
 val opt_ddump_tc_ast : bool ref
-val opt_dno_cast : bool ref
 val opt_reformat : string option ref
 
 open Ast_defs

src/lib/initial_check.ml

@@ -78,7 +78,6 @@ module P = Parse_ast
 let opt_undefined_gen = ref false
 let opt_fast_undefined = ref false
 let opt_magic_hash = ref false
-let opt_enum_casts = ref false
 
 type ctx = {
   kinds : kind_aux KBindings.t;
@@ -631,10 +630,10 @@ let to_ast_spec ctx (vs : P.val_spec) : uannot val_spec ctx_out =
   match vs with
   | P.VS_aux (vs, l) -> (
       match vs with
-      | P.VS_val_spec (ts, id, ext, is_cast) ->
+      | P.VS_val_spec (ts, id, ext) ->
           let typschm, _ = to_ast_typschm ctx ts in
           let ext = Option.map to_ast_extern ext in
-          (VS_aux (VS_val_spec (typschm, to_ast_id ctx id, ext, is_cast), (l, empty_uannot)), ctx)
+          (VS_aux (VS_val_spec (typschm, to_ast_id ctx id, ext), (l, empty_uannot)), ctx)
     )
 
 let to_ast_outcome ctx (ev : P.outcome_spec) : outcome_spec ctx_out =
@@ -757,7 +756,7 @@ let generate_enum_functions l ctx enum_id fns exps =
                  )
               );
           ];
-        mk_val_spec (VS_val_spec (mk_typschm (mk_typquant []) (function_typ [mk_id_typ enum_id] typ), name, None, false));
+        mk_val_spec (VS_val_spec (mk_typschm (mk_typquant []) (function_typ [mk_id_typ enum_id] typ), name, None));
       ]
     )
     fns
@@ -1157,9 +1156,9 @@ let constraint_of_string str =
   with Parser.Error -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Failed to parse " ^ str)
 
 let extern_of_string ?(pure = false) id str =
-  VS_val_spec (typschm_of_string str, id, Some { pure; bindings = [("_", string_of_id id)] }, false) |> mk_val_spec
+  VS_val_spec (typschm_of_string str, id, Some { pure; bindings = [("_", string_of_id id)] }) |> mk_val_spec
 
-let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, None, false))
+let val_spec_of_string id str = mk_val_spec (VS_val_spec (typschm_of_string str, id, None))
 
 let quant_item_param = function
   | QI_aux (QI_id kopt, _) when is_int_kopt kopt -> [prepend_id "atom_" (id_of_kid (kopt_kid kopt))]
@@ -1269,15 +1268,15 @@ let generate_undefineds vs_ids defs =
           letbinds
       )
     in
-    ( mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false)),
+    ( mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None)),
       mk_fundef [mk_funcl (prepend_id "undefined_" id) pat body]
     )
   in
   let undefined_td = function
     | TD_enum (id, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
         let typschm = typschm_of_string ("unit -> " ^ string_of_id id) in
         [
-          mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, None, false));
+          mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, None));
           mk_fundef
             [
               mk_funcl (prepend_id "undefined_" id)
@@ -1293,7 +1292,7 @@ let generate_undefineds vs_ids defs =
           p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))
         in
         [
-          mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false));
+          mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None));
           mk_fundef
             [
               mk_funcl (prepend_id "undefined_" id) pat
@@ -1358,7 +1357,7 @@ let generate_enum_functions vs_ids defs =
         | Some _ -> gen_enums (enum :: acc) defs
         | None ->
             let enum_val_spec name quants typ =
-              mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, None, !opt_enum_casts))
+              mk_val_spec (VS_val_spec (mk_typschm (mk_typquant quants) typ, name, None))
             in
             let range_constraint kid =
               nc_and (nc_lteq (nint 0) (nvar kid)) (nc_lteq (nvar kid) (nint (List.length elems - 1)))

src/lib/initial_check.mli

@@ -91,11 +91,6 @@ val opt_fast_undefined : bool ref
    name *)
 val opt_magic_hash : bool ref
 
-(** When true enums can be automatically casted to range types and
-   back.  Otherwise generated T_of_num and num_of_T functions must be
-   manually used for each enum T *)
-val opt_enum_casts : bool ref
-
 (** This is a bit of a hack right now - it ensures that the undefiend
    builtins (undefined_vector etc), only get added to the AST
    once. The original assumption in sail is that the whole AST gets

src/lib/jib_compile.ml

@@ -1539,7 +1539,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp =
         let instrs = setup @ [call (CL_id (global id, ctyp_of_typ ctx typ))] @ cleanup in
         let instrs = unique_names instrs in
         ([CDEF_register (id, ctyp_of_typ ctx typ, instrs)], ctx)
-    | DEF_val (VS_aux (VS_val_spec (_, id, ext, _), _)) ->
+    | DEF_val (VS_aux (VS_val_spec (_, id, ext), _)) ->
         let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
         let extern = if Env.is_extern id ctx.tc_env "c" then Some (Env.get_extern id ctx.tc_env "c") else None in
         let arg_typs, ret_typ =