Further module improvements

src/bin/sail.ml

@@ -68,14 +68,14 @@
 open Libsail
 
 let opt_new_cli = ref false
-let opt_file_arguments : string list ref = ref []
+let opt_free_arguments : string list ref = ref []
 let opt_file_out : string option ref = ref None
 let opt_just_check : bool ref = ref false
 let opt_auto_interpreter_rewrites : bool ref = ref false
 let opt_interactive_script : string option ref = ref None
 let opt_splice : string list ref = ref []
 let opt_print_version = ref false
-let opt_memo_z3 = ref false
+let opt_memo_z3 = ref true
 let opt_have_feature = ref None
 let opt_show_sail_dir = ref false
 let opt_project_file : string option ref = ref None
@@ -356,25 +356,45 @@ let file_to_string filename =
 
 let run_sail (config : Yojson.Basic.t option) tgt =
   Target.run_pre_parse_hook tgt ();
+
+  let rigging_files, frees = List.partition (fun free -> Filename.check_suffix free ".rigging") !opt_free_arguments in
+
   let ast, env, effect_info =
-    match !opt_project_file with
-    | Some file ->
+    match rigging_files with
+    | [] ->
+        (* If there are no provided rigging files, we concatenate all
+           the free file arguments into one big blob like before *)
+        Frontend.load_files ~target:tgt Manifest.dir !options Type_check.initial_env frees
+    | _ ->
         let t = Profile.start () in
-        let root_directory = Filename.dirname file in
-        let defs = Initial_check.parse_project ~filename:file ~contents:(file_to_string file) in
-        let proj = Project.initialize_project_structure ~root_directory defs in
+        let defs =
+          List.map
+            (fun rigging_file ->
+              let root_directory = Filename.dirname rigging_file in
+              let contents = file_to_string rigging_file in
+              Project.mk_root root_directory :: Initial_check.parse_project ~filename:rigging_file ~contents ()
+            )
+            rigging_files
+          |> List.concat
+        in
+        let proj = Project.initialize_project_structure defs in
+        if !opt_list_files then (
+          let files = Project.all_files proj in
+          print_endline (Util.string_of_list " " fst files);
+          exit 0
+        );
         let mod_ids =
           List.map
             (fun mod_name ->
               match Project.get_module_id proj mod_name with
               | Some id -> id
               | None -> raise (Reporting.err_general Parse_ast.Unknown ("Unknown module " ^ mod_name))
             )
-            !opt_file_arguments
+            frees
         in
         Profile.finish "parsing project" t;
-        Frontend.load_modules ~target:tgt Manifest.dir !options Type_check.initial_env proj mod_ids
-    | None -> Frontend.load_files ~target:tgt Manifest.dir !options Type_check.initial_env !opt_file_arguments
+        let env = Type_check.initial_env_with_modules proj in
+        Frontend.load_modules ~target:tgt Manifest.dir !options env proj mod_ids
   in
   let ast, env = Frontend.initial_rewrite effect_info env ast in
   let ast, env = List.fold_right (fun file (ast, _) -> Splice.splice ast file) !opt_splice (ast, env) in
@@ -402,7 +422,7 @@ let run_sail_format (config : Yojson.Basic.t option) =
       | None -> Format_sail.default_config
   end in
   let module Formatter = Format_sail.Make (Config) in
-  let parsed_files = List.map (fun f -> (f, Initial_check.parse_file f)) !opt_file_arguments in
+  let parsed_files = List.map (fun f -> (f, Initial_check.parse_file f)) !opt_free_arguments in
   List.iter
     (fun (f, (comments, parse_ast)) ->
       let source = file_to_string f in
@@ -485,7 +505,7 @@ let main () =
       )
   end;
 
-  Arg.parse_dynamic options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) usage_msg;
+  Arg.parse_dynamic options (fun s -> opt_free_arguments := !opt_free_arguments @ [s]) usage_msg;
 
   let config = Option.bind (get_config_file ()) parse_config_file in
 

src/lib/chunk_ast.ml

@@ -1277,7 +1277,7 @@ let chunk_def source last_line_span comments chunks (DEF_aux (def, l)) =
   begin
     match def with
     | DEF_fundef fdef -> chunk_fundef comments chunks fdef
-    | DEF_pragma (pragma, arg) ->
+    | DEF_pragma (pragma, arg, _) ->
         Queue.add (Pragma (pragma, arg)) chunks;
         pragma_span := true
     | DEF_default dts -> chunk_default_typing_spec comments chunks dts

src/lib/frontend.ml

@@ -93,17 +93,10 @@ let wrap_module proj parsed_module =
   let module P = Parse_ast in
   let open Project in
   let name, l = module_name proj parsed_module.id in
-  let bracket_pragma p = P.DEF_aux (P.DEF_pragma (p, Printf.sprintf "%d %s" parsed_module.id name), to_loc l) in
-  let require_pragma =
-    let reqs = module_requires proj parsed_module.id in
-    if Util.list_empty reqs then []
-    else [P.DEF_aux (P.DEF_pragma ("require#", Util.string_of_list " " string_of_int reqs), to_loc l)]
-  in
+  let bracket_pragma p = P.DEF_aux (P.DEF_pragma (p, name, 1), to_loc l) in
   parsed_module.files
-  |> Util.update_first (fun (f, (comments, defs)) ->
-         (f, (comments, (bracket_pragma "module_start#" :: require_pragma) @ defs))
-     )
-  |> Util.update_last (fun (f, (comments, defs)) -> (f, (comments, defs @ [bracket_pragma "module_end#"])))
+  |> Util.update_first (fun (f, (comments, defs)) -> (f, (comments, bracket_pragma "start_module#" :: defs)))
+  |> Util.update_last (fun (f, (comments, defs)) -> (f, (comments, defs @ [bracket_pragma "end_module#"])))
 
 let process_ast target type_envs ast =
   if !opt_ddump_initial_ast then Pretty_print_sail.pp_ast stdout ast;

src/lib/initial_check.ml

@@ -1248,6 +1248,17 @@ let check_annotation (DEF_aux (aux, def_annot)) =
     | _ -> ()
   )
 
+let pragma_arg_loc pragma arg_left_trim l =
+  let open Lexing in
+  Reporting.map_loc_range
+    (fun p1 p2 ->
+      let left_trim = String.length pragma + arg_left_trim + 1 in
+      let p1 = { p1 with pos_cnum = p1.pos_cnum + left_trim } in
+      let p2 = { p2 with pos_cnum = p2.pos_cnum - 1; pos_bol = p1.pos_bol; pos_lnum = p1.pos_lnum } in
+      (p1, p2)
+    )
+    l
+
 let rec to_ast_def doc attrs ctx (P.DEF_aux (def, l)) : uannot def list ctx_out =
   let annot = mk_def_annot ?doc ~attrs l in
   match def with
@@ -1305,25 +1316,30 @@ let rec to_ast_def doc attrs ctx (P.DEF_aux (def, l)) : uannot def list ctx_out
   | P.DEF_register dec ->
       let d = to_ast_dec ctx dec in
       ([DEF_aux (DEF_register d, annot)], ctx)
-  | P.DEF_pragma ("sail_internal", arg) -> begin
-      match Reporting.loc_file l with
-      | Some file ->
-          ( [DEF_aux (DEF_pragma ("sail_internal", arg, l), annot)],
-            { ctx with internal_files = StringSet.add file ctx.internal_files }
-          )
-      | None -> ([DEF_aux (DEF_pragma ("sail_internal", arg, l), annot)], ctx)
-    end
-  | P.DEF_pragma ("target_set", arg) ->
-      let args = String.split_on_char ' ' arg |> List.filter (fun s -> String.length s > 0) in
+  | P.DEF_pragma (pragma, arg, ltrim) ->
+      let l = pragma_arg_loc pragma ltrim l in
       begin
-        match args with
-        | set :: targets ->
-            ( [DEF_aux (DEF_pragma ("target_set", arg, l), annot)],
-              { ctx with target_sets = StringMap.add set targets ctx.target_sets }
-            )
-        | [] -> raise (Reporting.err_general l "No arguments provided to target set directive")
+        match pragma with
+        | "sail_internal" -> begin
+            match Reporting.loc_file l with
+            | Some file ->
+                ( [DEF_aux (DEF_pragma ("sail_internal", arg, l), annot)],
+                  { ctx with internal_files = StringSet.add file ctx.internal_files }
+                )
+            | None -> ([DEF_aux (DEF_pragma ("sail_internal", arg, l), annot)], ctx)
+          end
+        | "target_set" ->
+            let args = String.split_on_char ' ' arg |> List.filter (fun s -> String.length s > 0) in
+            begin
+              match args with
+              | set :: targets ->
+                  ( [DEF_aux (DEF_pragma ("target_set", arg, l), annot)],
+                    { ctx with target_sets = StringMap.add set targets ctx.target_sets }
+                  )
+              | [] -> raise (Reporting.err_general l "No arguments provided to target set directive")
+            end
+        | _ -> ([DEF_aux (DEF_pragma (pragma, arg, l), annot)], ctx)
       end
-  | P.DEF_pragma (pragma, arg) -> ([DEF_aux (DEF_pragma (pragma, arg, l), annot)], ctx)
   | P.DEF_internal_mutrec _ ->
       (* Should never occur because of remove_mutrec *)
       raise (Reporting.err_unreachable l __POS__ "Internal mutual block found when processing scattered defs")
@@ -1773,11 +1789,20 @@ let parse_file_from_string ~filename:f ~contents:s =
     let tok = Lexing.lexeme lexbuf in
     raise (Reporting.err_syntax pos ("current token: " ^ tok))
 
-let parse_project ~filename:f ~contents:s =
+let parse_project ?inline ?filename:f ~contents:s () =
   let open Project in
   let open Lexing in
   let lexbuf = from_string s in
-  lexbuf.lex_curr_p <- { pos_fname = f; pos_lnum = 1; pos_bol = 0; pos_cnum = 0 };
+
+  (* Note that OCaml >= 4.11 has a much less hacky way of doing this *)
+  begin
+    match inline with
+    | Some p ->
+        lexbuf.lex_curr_p <- p;
+        lexbuf.lex_abs_pos <- p.pos_cnum
+    | None -> lexbuf.lex_curr_p <- { pos_fname = Option.get f; pos_lnum = 1; pos_bol = 0; pos_cnum = 0 }
+  end;
+
   try Project_parser.file Project_lexer.token lexbuf
   with Project_parser.Error ->
     let pos = Lexing.lexeme_start_p lexbuf in

src/lib/initial_check.mli

@@ -139,4 +139,5 @@ val parse_file : ?loc:Parse_ast.l -> string -> Lexer.comment list * Parse_ast.de
 
 val parse_file_from_string : filename:string -> contents:string -> Lexer.comment list * Parse_ast.def list
 
-val parse_project : filename:string -> contents:string -> Project.def Project.spanned list
+val parse_project :
+  ?inline:Lexing.position -> ?filename:string -> contents:string -> unit -> Project.def Project.spanned list

src/lib/lexer.mll

@@ -224,7 +224,10 @@ rule token = parse
   | "$[" (ident+ as i)
     { let attr = attribute 0 (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf in Attribute(i, String.trim attr) }
   | "$" (ident+ as i)
-    { let p = pragma (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) false lexbuf in Pragma(i, String.trim p) }
+    { let startpos = Lexing.lexeme_start_p lexbuf in
+      let arg = pragma (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) false lexbuf in
+      lexbuf.lex_start_p <- startpos;
+      Pragma (i, arg) }
   | "infix" ws (digit as p) ws (operator as op)
     { Fixity (Infix, Big_int.of_string (Char.escaped p), op) }
   | "infixl" ws (digit as p) ws (operator as op)

src/lib/parse_ast.ml

@@ -439,7 +439,7 @@ type def_aux =
   | DEF_measure of id * pat * exp (* separate termination measure declaration *)
   | DEF_loop_measures of id * loop_measure list (* separate termination measure declaration *)
   | DEF_register of dec_spec (* register declaration *)
-  | DEF_pragma of string * string
+  | DEF_pragma of string * string * int
   | DEF_attribute of string * string * def
   | DEF_doc of string * def
   | DEF_internal_mutrec of fundef list

src/lib/parser.mly

@@ -233,6 +233,20 @@ let fix_extern typschm = function
 let funcl_annot fs fcl =
   List.fold_right (fun f fcl -> f fcl) fs fcl
 
+let pragma_left_spaces pragma p s =
+  let n = ref 0 in
+  while !n < String.length s && (s.[!n] = ' ' || s.[!n] = '\t') do
+    if s.[!n] = '\t' then (
+      (* If find a tab we won't be able to correctly format errors
+         found in the directive argument. It would be very weird for a
+         tab to show up here, so just bail. *)
+      let p = { p with Lexing.pos_cnum = p.Lexing.pos_cnum + String.length pragma + 1 + !n } in
+      raise (Reporting.err_lex p "Tab character (\\t) found between directive and argument. Please use spaces.")
+    );
+    incr n
+  done;
+  !n
+
 let effect_deprecated l =
   Reporting.warn ~once_from:__POS__ "Deprecated" l "Explicit effect annotations are deprecated. They are no longer used and can be removed."
 
@@ -1319,7 +1333,9 @@ def_aux:
   | Mutual Lcurly fun_def_list Rcurly
     { DEF_internal_mutrec $3 }
   | Pragma
-    { DEF_pragma (fst $1, snd $1) }
+    { let (pragma, arg) = $1 in
+      let ltrim = pragma_left_spaces pragma $startpos arg in
+      DEF_pragma (pragma, String.trim arg, ltrim) }
   | TerminationMeasure id pat Eq exp
     { DEF_measure ($2, $3, $5) }
   | TerminationMeasure id loop_measures