Modules: Change naming

Less nautical theme

doc/asciidoc/Makefile

@@ -11,13 +11,13 @@ SAIL_DOCS += sail_doc/tuples.json
 SAIL_DOCS += sail_doc/string.json
 SAIL_DOCS += module_sail_doc/simple_mod.json
 SAIL_DOCS += module_sail_doc/simple_mod_err.error
-SAIL_DOCS += module_sail_doc/cond.rigging
+SAIL_DOCS += module_sail_doc/cond.sail_project
 SAIL_DOCS += sail_doc/cannot_wildcard.json
 SAIL_DOCS += lib_sail_doc/concurrency_interface/read_write.json
 
 TIKZ_FIGURES = ordering-tikz.png
 
-INCS = module_sail_doc/simple_mod.rigging
+INCS = module_sail_doc/simple_mod.sail_project
 
 all: manual.html manual.pdf
 
@@ -32,15 +32,15 @@ lib_sail_doc/%.json: ../../lib/%.sail
 
 .SECONDEXPANSION:
 
-module_sail_doc/%.json: ../examples/%.rigging $$(shell sail ../examples/%.rigging -list_files)
+module_sail_doc/%.json: ../examples/%.sail_project $$(shell sail ../examples/%.sail_project -list_files)
 	mkdir -p module_sail_doc
 	sail -doc $(addprefix -doc_file ,$(shell sail $< -list_files)) -doc_embed plain -doc_bundle $(notdir $@) -o module_sail_doc $<
 
-module_sail_doc/%.error: ../examples/%.rigging $$(shell sail ../examples/%.rigging -list_files)
+module_sail_doc/%.error: ../examples/%.sail_project $$(shell sail ../examples/%.sail_project -list_files)
 	mkdir -p module_sail_doc
 	-sail -no_color $< 2> $@
 
-module_sail_doc/%.rigging: ../examples/%.rigging
+module_sail_doc/%.sail_project: ../examples/%.sail_project
 	mkdir -p module_sail_doc
 	sail $< -list_files 1>/dev/null
 	cp $< $@

doc/asciidoc/modules.adoc

@@ -6,10 +6,8 @@ _modules_. Modules provide an access control mechanism, meaning a Sail
 definition in one module cannot access or use definitions provided by
 another module unless it explicitly _requires_ the other module.
 
-The module structure of a Sail specification is specified in a
-separate `.rigging` file (so named because
-https://en.wikipedia.org/wiki/Rigging[rigging] is what supports and
-organizes the sails on a ship).
+The module structure of a Sail project/specification is specified in a
+separate `.sail_project` file.
 
 For a simple example, let's assume we have two Sail files `amod.sail` and
 `bmod.sail`:
@@ -25,12 +23,12 @@ include::sail:ALFA[from=simplemod,type=span]
 ----
 include::sail:BRAVO[from=simplemod,type=span]
 ----
-We can use the following rigging file:
+We can use the following `.sail_project` file:
 
-.`simple_mod.rigging`
+.`simple_mod.sail_project`
 [source]
 ----
-include::module_sail_doc/simple_mod.rigging[]
+include::module_sail_doc/simple_mod.sail_project[]
 ----
 This file defines two modules `A` and `B`, with module `A` containing
 the file `amod.sail` and module B containing the file `bmod.sail`.
@@ -48,24 +46,25 @@ exists as it has already checked module `A`, so it points us at the
 definition and suggests how we could resolve the error by adding the
 requires line we just removed.
 
-When using a rigging file we do not have to pass all the files on the
-command line, so we can invoke Sail simply as
+When using a `.sail_project` file we do not have to pass all the files
+on the command line, so we can invoke Sail simply as
 
 [source,shell]
 ----
-sail simple_mod.rigging
+sail simple_mod.sail_project
 ----
 
 and it will know where to find `amod.sail` and `bmod.sail` relative to
-the location of the rigging file.
+the location of the project file.
 
 A module can have more than one Sail file. These files are processed
 sequentially in the order they are listed. This is exactly like what
 happens when we pass multiple Sail files on the command line without a
-rigging file to define the module structure. A module can therefore be
-thought of as a sequence of Sail files that is treated as a single
-logical unit. As an example, we could add a third module to our above
-file, which is comprised of three Sail files and depends on A and B.
+`.sail_project` file to define the module structure. A module can
+therefore be thought of as a sequence of Sail files that is treated as
+a single logical unit. As an example, we could add a third module to
+our above file, which is comprised of three Sail files and depends on
+A and B.
 
 [source]
 ----
@@ -96,56 +95,56 @@ C {
 ----
 
 If we wanted to we could define `C` in a separate file, rather than
-adding it to our previous file, and pass multiple rigging files to
+adding it to our previous file, and pass multiple project files to
 Sail like so:
 
 [source,shell]
 ----
-sail simple_mod.rigging new_file_with_C.rigging
+sail simple_mod.sail_project new_file_with_C.sail_project
 ----
 
-These will be treated together as a single large rigging file. A use
+These will be treated together as a single large project file. A use
 case might be if you were defining an out-of-tree extension `Xfoo` for
 sail-riscv, you could do something like:
 
 [source,shell]
 ----
-sail sail-riscv/riscv.rigging src/Xfoo.rigging
+sail sail-riscv/riscv.sail_project src/Xfoo.sail_project
 ----
 
-and the modules you define in `Xfoo.rigging` can require modules from
-`riscv.rigging` (and technically also vice-versa, although it makes
-less sense in this example).
+and the modules you define in `Xfoo.sail_project` can require modules
+from `riscv.sail_project`, and also vice-versa, although it makes less
+sense in this example.
 
 === Working with Makefiles
 
 The `-list_files` option can be used to list all the files within a
-rigging file, which allows them to be used in a Makefile prerequisite.
+project file, which allows them to be used in a Makefile prerequisite.
 As an example, to build the module examples in this very manual, we
 use the rule below to generate documentation indexes (which our
-Asciidoctor plugin consumes) for every `.sail` file within a rigging
+Asciidoctor plugin consumes) for every `.sail` file within a project
 file.
 
 [%nowrap,make]
 ----
 .SECONDEXPANSION:
 
-module_sail_doc/%.json: ../examples/%.rigging $$(shell sail ../examples/%.rigging -list_files)
+module_sail_doc/%.json: ../examples/%.sail_project $$(shell sail ../examples/%.sail_project -list_files)
 	mkdir -p module_sail_doc
 	sail -doc $(addprefix -doc_file ,$(shell sail $< -list_files)) -doc_embed plain -doc_bundle $(notdir $@) -o module_sail_doc $<
 ----
 
 === Conditional compilation within modules
 
-We can use _variables_ in our rigging files to control either file
+We can use _variables_ in our project files to control either file
 inclusion within a module or to control whether a module requires
 another or not. A variable can even contain a sequence of modules,
 that can then be used in a require statement, as shown in the
 following example:
 
 [source]
 ----
-include::module_sail_doc/cond.rigging[]
+include::module_sail_doc/cond.sail_project[]
 ----
 
 === Optional and default modules

src/bin/sail.ml

@@ -78,7 +78,7 @@ let opt_print_version = ref false
 let opt_memo_z3 = ref true
 let opt_have_feature = ref None
 let opt_show_sail_dir = ref false
-let opt_rigging_files : string list ref = ref []
+let opt_project_files : string list ref = ref []
 let opt_list_files = ref false
 let opt_variable_assignments : string list ref = ref []
 let opt_config_file : string option ref = ref None
@@ -198,15 +198,15 @@ let rec options =
         " drop to an interactive session after running Sail. Differs from -i in that it does not set up the \
          interpreter in the interactive shell."
       );
-      ( "-rigging",
-        Arg.String (fun file -> opt_rigging_files := !opt_rigging_files @ [file]),
-        "<file> module rigging file"
+      ( "-project",
+        Arg.String (fun file -> opt_project_files := !opt_project_files @ [file]),
+        "<file> sail project file defining module structure"
       );
       ( "-variable",
         Arg.String (fun assignment -> opt_variable_assignments := assignment :: !opt_variable_assignments),
         "<variable=value> assign a module variable to a value"
       );
-      ("-list_files", Arg.Set opt_list_files, " list files used in all module rigging files");
+      ("-list_files", Arg.Set opt_list_files, " list files used in all project files");
       ("-config", Arg.String (fun file -> opt_config_file := Some file), "<file> configuration file");
       ("-fmt", Arg.Set opt_format, " format input source code");
       ( "-fmt_backup",
@@ -365,24 +365,29 @@ 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 project_files, frees =
+    List.partition (fun free -> Filename.check_suffix free ".sail_project") !opt_free_arguments
+  in
 
   let ast, env, effect_info =
-    match (rigging_files, !opt_rigging_files) with
+    match (project_files, !opt_project_files) with
     | [], [] ->
-        (* If there are no provided rigging files, we concatenate all
+        (* If there are no provided project 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
-    | rigging_files, [] | [], rigging_files ->
+    (* Allows project files from either free arguments via suffix, or
+       from -project, but not both as the ordering between them would
+       be unclear. *)
+    | project_files, [] | [], project_files ->
         let t = Profile.start () 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 ()
+            (fun project_file ->
+              let root_directory = Filename.dirname project_file in
+              let contents = file_to_string project_file in
+              Project.mk_root root_directory :: Initial_check.parse_project ~filename:project_file ~contents ()
             )
-            rigging_files
+            project_files
           |> List.concat
         in
         let variables = ref Util.StringMap.empty in
@@ -413,8 +418,8 @@ let run_sail (config : Yojson.Basic.t option) tgt =
     | _, _ ->
         raise
           (Reporting.err_general Parse_ast.Unknown
-             "Module rigging files should either be specified with the appropriate option, or as free arguments with \
-              the appropriate extension, but not both!"
+             "Module files (.sail_project) should either be specified with the appropriate option, or as free \
+              arguments with the appropriate extension, but not both!"
           )
   in
   let ast, env = Frontend.initial_rewrite effect_info env ast in

src/lib/type_check.ml

@@ -4522,7 +4522,7 @@ and check_def : Env.t -> uannot def -> tannot def list * Env.t =
         ],
         env
       )
-  | DEF_pragma ("rigging#", arg, l) ->
+  | DEF_pragma ("project#", arg, l) ->
       let start_p = match Reporting.simp_loc l with Some (p, _) -> Some p | None -> None in
       let proj_defs = Initial_check.parse_project ?inline:start_p ~contents:arg () in
       let proj = Project.initialize_project_structure ~variables:(ref Util.StringMap.empty) proj_defs in

test/typecheck/fail/cond_mod.expect

@@ -9,5 +9,5 @@
    | 7 |let x : int = 3
    |   |    ^ definition here in A
    | fail/cond_mod.sail:3.34-35:
-   | 3 |$rigging# variable b = false A {} B { requires if $b then A else [] }
+   | 3 |$project# variable b = false A {} B { requires if $b then A else [] }
    |   |                                  ^ add 'requires A' within B here

test/typecheck/fail/cond_mod.sail

@@ -1,6 +1,6 @@
 $option -dmagic_hash
 
-$rigging# variable b = false A {} B { requires if $b then A else [] }
+$project# variable b = false A {} B { requires if $b then A else [] }
 
 $start_module# A
 

test/typecheck/fail/duplicate_toplevel_let_mod.sail

@@ -1,6 +1,6 @@
 $option -dmagic_hash
 
-$rigging# A {} B {}
+$project# A {} B {}
 
 $start_module# A
 

test/typecheck/fail/overload_member_scope.sail

@@ -8,7 +8,7 @@ $option -dmagic_hash
 // that allows us to cleanly remove optional modules if they overload
 // identifiers.
 
-$rigging# A { } B { requires A } C { requires B }
+$project# A { } B { requires A } C { requires B }
 
 $start_module# A
 

test/typecheck/fail/unscope_enum.sail

@@ -1,6 +1,6 @@
 $option -dmagic_hash
 
-$rigging# A {}
+$project# A {}
 
 default Order dec
 

test/typecheck/fail/unscope_let.sail

@@ -1,6 +1,6 @@
 $option -dmagic_hash
 
-$rigging# A {}
+$project# A {}
 
 default Order dec
 

test/typecheck/fail/unscope_register.sail

@@ -1,6 +1,6 @@
 $option -dmagic_hash
 
-$rigging# A {}
+$project# A {}
 
 default Order dec
 

test/typecheck/fail/unscope_type.sail

@@ -1,6 +1,6 @@
 $option -dmagic_hash
 
-$rigging# A {}
+$project# A {}
 
 default Order dec
 

test/typecheck/fail/unscope_val.sail

@@ -1,6 +1,6 @@
 $option -dmagic_hash
 
-$rigging# A {}
+$project# A {}
 
 default Order dec
 

test/typecheck/pass/extension_constructor.sail

@@ -1,6 +1,6 @@
 $option -dmagic_hash
 
-$rigging# A { } B { requires A } C { requires A }
+$project# A { } B { requires A } C { requires A }
 
 // Module A
 $start_module# A

test/typecheck/pass/extension_constructor/v1.expect

@@ -9,5 +9,5 @@
    | 10 |  $[extension B] Baz : unit,
    |    |                 ^-^ definition here in B
    | pass/extension_constructor/v1.sail:3.33-34:
-   | 3 |$rigging# A { } B { requires A } C { requires A }
+   | 3 |$project# A { } B { requires A } C { requires A }
    |   |                                 ^ add 'requires B' within C here

test/typecheck/pass/extension_constructor/v1.sail

@@ -1,6 +1,6 @@
 $option -dmagic_hash
 
-$rigging# A { } B { requires A } C { requires A }
+$project# A { } B { requires A } C { requires A }
 
 // Module A
 $start_module# A

test/typecheck/pass/extension_constructor/v2.expect

@@ -14,5 +14,5 @@
    |    | 8 |union Foo = {
    |    |   |      ^-^ definition here in A
    |    | pass/extension_constructor/v2.sail:3.33-34:
-   |    | 3 |$rigging# A { } B { requires A } C { }
+   |    | 3 |$project# A { } B { requires A } C { }
    |    |   |                                 ^ add 'requires A' within C here

test/typecheck/pass/extension_constructor/v2.sail

@@ -1,6 +1,6 @@
 $option -dmagic_hash
 
-$rigging# A { } B { requires A } C { }
+$project# A { } B { requires A } C { }
 
 // Module A
 $start_module# A

test/typecheck/pass/mod_var.sail

@@ -1,6 +1,6 @@
 $option -dmagic_hash
 
-$rigging# variable mods = [A] A {} B { requires $mods }
+$project# variable mods = [A] A {} B { requires $mods }
 
 $start_module# A