Make it an error to include the vector file before a default order

lib/vector.sail

@@ -68,6 +68,10 @@
 $ifndef _VECTOR
 $define _VECTOR
 
+$ifndef _DEFAULT_ORDER_SET
+$include_error A default order must be set (using `default Order dec` or `default Order inc`) before including this file
+$endif
+
 $include <flow.sail>
 
 type bits('n : Int) = bitvector('n)

src/bin/sail.ml

@@ -303,6 +303,7 @@ let rec options =
       ("-dtc_verbose", Arg.Int Type_check.set_tc_debug, "<verbosity> (debug) verbose typechecker output: 0 is silent");
       ("-dsmt_verbose", Arg.Set Constraint.opt_smt_verbose, " (debug) print SMTLIB constraints sent to SMT solver");
       ("-dmagic_hash", Arg.Set Initial_check.opt_magic_hash, " (debug) allow special character # in identifiers");
+      ("-dno_error_filenames", Arg.Set Error_format.opt_debug_no_filenames, " (debug) do not print filenames in errors");
       ( "-dprofile",
         Arg.Set Profile.opt_profile,
         " (debug) provide basic profiling information for rewriting passes within Sail"

src/lib/error_format.ml

@@ -88,6 +88,10 @@ let rec read_lines in_chan = function
 
 let error_tabwidth = 4
 
+let opt_debug_no_filenames = ref false
+
+let format_filename fname = if !opt_debug_no_filenames then "" else Util.(fname |> cyan |> clear)
+
 let unprintable_notation ?(color = fun x -> x) c =
   let n = Char.code c in
   if n = 9 then Some (String.make error_tabwidth ' ')
@@ -133,7 +137,7 @@ let format_code_single' prefix hint fname in_chan lnum cnum_from cnum_to content
   let line = input_line in_chan in
   let line_prefix = string_of_int lnum ^ Util.(clear (cyan " |")) in
   let blank_prefix = String.make (String.length (string_of_int lnum)) ' ' ^ Util.(clear (ppf.loc_color " |")) in
-  format_endline (Printf.sprintf "%s%s:%d.%d-%d:" prefix Util.(fname |> cyan |> clear) lnum cnum_from cnum_to) ppf;
+  format_endline (Printf.sprintf "%s%s:%d.%d-%d:" prefix (format_filename fname) lnum cnum_from cnum_to) ppf;
   let line, adjust = unprintable_escape ~color:Util.(fun e -> e |> magenta |> clear) line in
   format_endline (line_prefix ^ line) ppf;
   format_endline
@@ -159,7 +163,7 @@ let format_code_double' prefix fname in_chan lnum_from cnum_from lnum_to cnum_to
   let line_from_prefix = string_of_int lnum_from ^ line_from_padding ^ Util.(clear (cyan " |")) in
   let blank_prefix = String.make (String.length (string_of_int lnum_to)) ' ' ^ Util.(clear (ppf.loc_color " |")) in
   format_endline
-    (Printf.sprintf "%s%s:%d.%d-%d.%d:" prefix Util.(fname |> cyan |> clear) lnum_from cnum_from lnum_to cnum_to)
+    (Printf.sprintf "%s%s:%d.%d-%d.%d:" prefix (format_filename fname) lnum_from cnum_from lnum_to cnum_to)
     ppf;
   let cnum_end = String.length line_from in
   let line_from, adjust = unprintable_escape ~color:Util.(fun e -> e |> magenta |> clear) line_from in
@@ -172,7 +176,7 @@ let format_code_double' prefix fname in_chan lnum_from cnum_from lnum_to cnum_to
 
 let format_code_single_fallback prefix fname lnum cnum_from cnum_to contents ppf =
   let blank_prefix = String.make (String.length (string_of_int lnum)) ' ' ^ Util.(clear (ppf.loc_color " |")) in
-  format_endline (Printf.sprintf "%s%s:%d.%d-%d:" prefix Util.(fname |> cyan |> clear) lnum cnum_from cnum_to) ppf;
+  format_endline (Printf.sprintf "%s%s:%d.%d-%d:" prefix (format_filename fname) lnum cnum_from cnum_to) ppf;
   contents { ppf with indent = blank_prefix ^ " " }
 
 let format_code_single prefix hint fname lnum cnum_from cnum_to contents ppf =
@@ -191,7 +195,7 @@ let format_code_single prefix hint fname lnum cnum_from cnum_to contents ppf =
 let format_code_double_fallback prefix fname lnum_from cnum_from lnum_to cnum_to contents ppf =
   let blank_prefix = String.make (String.length (string_of_int lnum_to)) ' ' ^ Util.(clear (ppf.loc_color " |")) in
   format_endline
-    (Printf.sprintf "%s%s:%d.%d-%d.%d:" prefix Util.(fname |> cyan |> clear) lnum_from cnum_from lnum_to cnum_to)
+    (Printf.sprintf "%s%s:%d.%d-%d.%d:" prefix (format_filename fname) lnum_from cnum_from lnum_to cnum_to)
     ppf;
   contents { ppf with indent = blank_prefix ^ " " }
 

src/lib/preprocess.ml

@@ -179,11 +179,25 @@ let wrap_include l file = function
 
 let preprocess dir target opts =
   let module P = Parse_ast in
-  let rec aux acc = function
+  let rec aux includes acc = function
     | [] -> List.rev acc
     | DEF_aux (DEF_pragma ("define", symbol, _), _) :: defs ->
         symbols := StringSet.add symbol !symbols;
-        aux acc defs
+        aux includes acc defs
+    | DEF_aux (DEF_pragma ("include_error", message, _), l) :: defs -> begin
+        match List.rev includes with
+        | [] -> raise (Reporting.err_general (pragma_loc l) message)
+        | (include_root, l) :: ls ->
+            let open Error_format in
+            let b = Buffer.create 20 in
+            let _, message =
+              List.fold_left
+                (fun (includer, msg) (file, l) -> (file, Location ("", Some ("included by " ^ includer), l, msg)))
+                (include_root, Line message) ls
+            in
+            format_message message (buffer_formatter b);
+            raise (Reporting.err_general l (Buffer.contents b))
+      end
     | (DEF_aux (DEF_pragma ("option", command, _), l) as opt_pragma) :: defs ->
         let l = pragma_loc l in
         begin
@@ -202,23 +216,27 @@ let preprocess dir target opts =
           | Arg.Help msg -> raise (Reporting.err_general l "-help flag passed to $option directive")
           | Arg.Bad msg -> raise (Reporting.err_general l ("Invalid flag passed to $option directive" ^ first_line msg))
         end;
-        aux (opt_pragma :: acc) defs
+        aux includes (opt_pragma :: acc) defs
     | DEF_aux (DEF_pragma ("ifndef", symbol, _), l) :: defs ->
         let then_defs, else_defs, defs = cond_pragma l defs in
-        if not (StringSet.mem symbol !symbols) then aux acc (then_defs @ defs) else aux acc (else_defs @ defs)
+        if not (StringSet.mem symbol !symbols) then aux includes acc (then_defs @ defs)
+        else aux includes acc (else_defs @ defs)
     | DEF_aux (DEF_pragma ("ifdef", symbol, _), l) :: defs ->
         let then_defs, else_defs, defs = cond_pragma l defs in
-        if StringSet.mem symbol !symbols then aux acc (then_defs @ defs) else aux acc (else_defs @ defs)
+        if StringSet.mem symbol !symbols then aux includes acc (then_defs @ defs)
+        else aux includes acc (else_defs @ defs)
     | DEF_aux (DEF_pragma ("iftarget", t, _), l) :: defs ->
         let then_defs, else_defs, defs = cond_pragma l defs in
         begin
-          match target with Some t' when t = t' -> aux acc (then_defs @ defs) | _ -> aux acc (else_defs @ defs)
+          match target with
+          | Some t' when t = t' -> aux includes acc (then_defs @ defs)
+          | _ -> aux includes acc (else_defs @ defs)
         end
     | DEF_aux (DEF_pragma ("include", file, _), l) :: defs ->
         let len = String.length file in
         if len = 0 then (
           Reporting.warn "" (pragma_loc l) "Skipping bad $include. No file argument.";
-          aux acc defs
+          aux includes acc defs
         )
         else if file.[0] = '"' && file.[len - 1] = '"' then (
           let relative =
@@ -230,49 +248,56 @@ let preprocess dir target opts =
           in
           let file = String.sub file 1 (len - 2) in
           let include_file = Filename.concat relative file in
-          let include_defs = Initial_check.parse_file ~loc:l (Filename.concat relative file) |> snd |> aux [] in
-          aux (List.rev (wrap_include l include_file include_defs) @ acc) defs
+          let include_defs =
+            Initial_check.parse_file ~loc:l (Filename.concat relative file)
+            |> snd
+            |> aux ((file, pragma_loc l) :: includes) []
+          in
+          aux includes (List.rev (wrap_include l include_file include_defs) @ acc) defs
         )
         else if file.[0] = '<' && file.[len - 1] = '>' then (
-          let file = String.sub file 1 (len - 2) in
+          let lib_file = String.sub file 1 (len - 2) in
           let sail_dir = Reporting.get_sail_dir dir in
-          let file = Filename.concat sail_dir ("lib/" ^ file) in
-          let include_defs = Initial_check.parse_file ~loc:l file |> snd |> aux [] in
-          aux (List.rev (wrap_include l file include_defs) @ acc) defs
+          let file = Filename.concat sail_dir ("lib/" ^ lib_file) in
+          let include_defs =
+            Initial_check.parse_file ~loc:l file |> snd |> aux ((lib_file, pragma_loc l) :: includes) []
+          in
+          aux includes (List.rev (wrap_include l file include_defs) @ acc) defs
         )
         else (
           let help = "Make sure the filename is surrounded by quotes or angle brackets" in
           Reporting.warn "" (pragma_loc l) ("Skipping bad $include " ^ file ^ ". " ^ help);
-          aux acc defs
+          aux includes acc defs
         )
     | DEF_aux (DEF_pragma ("suppress_warnings", _, _), l) :: defs ->
         begin
           match Reporting.simp_loc l with
           | None -> () (* This shouldn't happen, but if it does just continue *)
           | Some (p, _) -> Reporting.suppress_warnings_for_file p.pos_fname
         end;
-        aux acc defs
+        aux includes acc defs
     (* Filter file_start and file_end out of the AST so when we
        round-trip files through the compiler we don't end up with
        incorrect start/end annotations *)
     | (DEF_aux (DEF_pragma ("file_start", _, _), _) | DEF_aux (DEF_pragma ("file_end", _, _), _)) :: defs ->
-        aux acc defs
+        aux includes acc defs
     | (DEF_aux (DEF_pragma (p, _, _), l) as pragma_def) :: defs ->
         if not (StringSet.mem p all_pragmas || String.contains p '#') then
           Reporting.warn "" (pragma_loc l) ("Unrecognised directive: " ^ p);
-        aux (pragma_def :: acc) defs
+        aux includes (pragma_def :: acc) defs
     | DEF_aux (DEF_outcome (outcome_spec, inner_defs), l) :: defs ->
-        aux (DEF_aux (DEF_outcome (outcome_spec, aux [] inner_defs), l) :: acc) defs
+        aux includes (DEF_aux (DEF_outcome (outcome_spec, aux includes [] inner_defs), l) :: acc) defs
     | (DEF_aux (DEF_default (DT_aux (DT_order (_, ATyp_aux (atyp, _)), _)), l) as def) :: defs -> begin
+        symbols := StringSet.add "_DEFAULT_ORDER_SET" !symbols;
         match atyp with
         | Parse_ast.ATyp_inc ->
             symbols := StringSet.add "_DEFAULT_INC" !symbols;
-            aux (def :: acc) defs
+            aux includes (def :: acc) defs
         | Parse_ast.ATyp_dec ->
             symbols := StringSet.add "_DEFAULT_DEC" !symbols;
-            aux (def :: acc) defs
-        | _ -> aux (def :: acc) defs
+            aux includes (def :: acc) defs
+        | _ -> aux includes (def :: acc) defs
       end
-    | def :: defs -> aux (def :: acc) defs
+    | def :: defs -> aux includes (def :: acc) defs
   in
-  aux []
+  aux [] []

test/c/foreach_none.sail

@@ -1,3 +1,5 @@
+default Order dec
+
 $include <prelude.sail>
 
 val main : unit -> unit

test/c/global_let_shadow.sail

@@ -1,3 +1,5 @@
+default Order dec
+
 $include <prelude.sail>
 $include <string.sail>
 

test/c/string_literal_type.sail

@@ -1,3 +1,5 @@
+default Order dec
+
 $include <prelude.sail>
 
 $option -string_literal_type

test/typecheck/fail/prelude_no_order.expect

@@ -0,0 +1,8 @@
+Error:
+:2.0-23:
+2 |$include <prelude.sail>
+  |^---------------------^
+  | :72.0-22:
+  | 72 |$include <vector.sail>
+  |    |^--------------------^ included by prelude.sail
+  |    | A default order must be set (using `default Order dec` or `default Order inc`) before including this file

test/typecheck/fail/prelude_no_order.sail

@@ -0,0 +1,2 @@
+$option -dno_error_filenames
+$include <prelude.sail>

test/typecheck/pass/mutrec.sail

@@ -1,3 +1,5 @@
+default Order dec
+
 $include <prelude.sail>
 
 val f : list(int) -> int

test/typecheck/pass/simple_record_access.sail

@@ -1,3 +1,5 @@
+default Order dec
+
 $include <flow.sail>
 $include <vector_inc.sail>
 

test/typecheck/pass/string_literal_type.sail

@@ -1,3 +1,4 @@
+default Order dec
 $include <prelude.sail>
 
 $option -string_literal_type

test/typecheck/pass/string_literal_type/v1.expect

@@ -1,5 +1,5 @@
 Type error:
-pass/string_literal_type/v1.sail:14.7-23:
-14 |  test(concat_str(x, z))
+pass/string_literal_type/v1.sail:16.7-23:
+16 |  test(concat_str(x, z))
    |       ^--------------^
    | string is not a subtype of string_literal

test/typecheck/pass/string_literal_type/v1.sail

@@ -1,3 +1,5 @@
+default Order dec
+
 $include <prelude.sail>
 
 $option -string_literal_type