Update Lesson 1.5 README.

k-distribution/k-tutorial/1_basic/05_modules/README.md

@@ -4,206 +4,241 @@ copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
 # Lesson 1.5: Modules, Imports, and Requires
 
-The purpose of this lesson is to explain how K definitions can be broken into
-separate modules and files and how these distinct components combine into a
-complete K definition.
+In this lesson you will learn how K definitions can be broken into separate 
+modules and files and how these distinct components combine into a complete K 
+definition.
 
 ## K's outer syntax
 
-Recall from [Lesson 1.3](../03_parsing/README.md) that K's grammar is broken
-into two components: the **outer syntax** of K and the **inner syntax** of K.
-Outer syntax, as previously mentioned, consists of **requires**, **modules**,
-**imports**, and **sentences**. A K semantics is expressed by the set of
-sentences contained in the definition. The scope of what is considered
-contained in that definition is determined both by the **main semantics
-module** of a K definition, as well as the **requires** and **imports** present
-in the file that contains that module.
+Recall from [Lesson 1.3](../03_parsing/README.md) that K's grammar is composed
+of two parts: **outer syntax** and **inner syntax**. Outer syntax, as 
+previously mentioned, consists of **requires**, **modules**, **imports**, and 
+**sentences**. A K semantics is expressed by the set of sentences contained in 
+the definition. The scope of what is considered contained in that definition 
+is determined both by the **main semantics module** of a K definition, as well 
+as the **requires** and **imports** present in the file that contains that 
+module.
 
 ## Basic module syntax
 
 The basic unit of grouping sentences in K is the module. A module consists
-of a **module name**, an optional list of **attributes**, a list of
-**imports**, and a list of **sentences**.
+of a **module name**, and optionally, a list of **attributes**, a list of
+**imports**, or a list of **sentences**.
 
 A module name consists of one or more groups of letters, numbers, or
 underscores, separated by a hyphen. Here are some valid module names: `FOO`,
 `FOO-BAR`, `foo0`, `foo0_bar-Baz9`. Here are some invalid module names: `-`,
 `-FOO`, `BAR-`, `FOO--BAR`. Stylistically, modules names are usually all
 uppercase with hyphens separating words, but this is not strictly enforced.
 
-Some example modules include an empty module:
+Some module examples include:
+
+* an empty module:
 
 ```k
 module LESSON-05-A
 
 endmodule
 ```
 
-A module with some attributes:
+* a module with some attributes:
 
 ```k
 module LESSON-05-B [group(attr1,attr2), private]
 
 endmodule
 ```
 
-A module with some sentences:
+* a module with some sentences:
 
 ```k
 module LESSON-05-C
+
   syntax Boolean ::= "true" | "false"
   syntax Boolean ::= "not" Boolean [function]
+
   rule not true => false
   rule not false => true
+
 endmodule
 ```
 
+TODO: We will discuss the new concepts in due time ...
+
 ## Imports
 
-Thus far we have only discussed definitions containing a single module.
-Definitions can also contain multiple modules, in which one module imports
-others.
+Thus far we have only seen definitions containing a single module.
+However, definitions in K can also contain multiple modules, in which one 
+module imports others.
 
-An import in K appears at the top of a module, prior to any sentences. It can
-be specified with the `imports` keyword, followed by a module name.
+An import in K appears after the module name and prior to any sentences. It 
+is specified with the `imports` keyword, followed by a module name.
 
-For example, here is a simple definition with two modules (`lesson-05-d.k`):
+For example, below we have a definition with two modules (`lesson-05-d.k`):
 
 ```k
 module LESSON-05-D-1
+
   syntax Boolean ::= "true" | "false"
   syntax Boolean ::= "not" Boolean [function]
+
 endmodule
 
 module LESSON-05-D
+
   imports LESSON-05-D-1
 
   rule not true => false
   rule not false => true
+
 endmodule
 ```
 
-This K definition is equivalent to the definition expressed by the single module
-`LESSON-05-C`. Essentially, by importing a module, we include all of the
-sentences in the module being imported into the module that we import from.
-There are a few minor differences between importing a module and simply
-including its sentences in another module directly, but we will cover these
-differences later. Essentially, you can think of modules as a way of
-conceptually grouping sentences in a larger K definition.
+Modules can be written in any order, it is not a requirement that the imported 
+modules be specified before other modules importing them. What it is
+required is that the module provided to attribute `--main-module` is not
+imported by any other module.
+
+Let's return to the K definition in `lesson-05-d.k` above. Note that it is
+equivalent to the definition expressed by the single module `LESSON-05-C`.
+Essentially, by importing module `A` into module `B`, we include all sentences
+in module `A` into module `B`. Note that K distinguishes between importing a 
+module and simply including its sentences in another module directly. We 
+will discuss these differences in Lesson [XYZ]().
+For now, you can think of modules as a way of conceptually grouping sentences 
+in a larger K definition.
 
 ### Exercise
 
 Modify `lesson-05-d.k` to include four modules: one containing the syntax, two
 with one rule each that imports the first module, and a final module
 `LESSON-05-D` containing no sentences that imports the second and third module.
-Check to make sure the definition still compiles and that you can still evaluate
-the `not` function.
+Make sure the definition still compiles and that you can still evaluate the 
+`not` function.
 
-## Parsing in the presence of multiple modules
+## Parsing multiple modules
 
-As you may have noticed, each module in a definition can express a distinct set
-of syntax. When parsing the sentences in a module, we use the syntax
-**of that module**, enriched with the basic syntax of K, in order to parse
-rules in that module. For example, the following definition is a parser error
-(`lesson-05-e.k`):
+As you may have noticed, each module in a definition can express a **distinct** 
+set of syntax. When parsing the sentences in a module, we use the syntax
+**of that module**, enriched with the basic syntax of K. For example, the 
+following definition is a parser error (`lesson-05-e.k`):
 
 ```{.k .error}
 module LESSON-05-E-1
+
   rule not true => false
   rule not false => true
+
 endmodule
 
 module LESSON-05-E-2
+
   syntax Boolean ::= "true" | "false"
   syntax Boolean ::= "not" Boolean [function]
+
 endmodule
 ```
 
 This is because the syntax referenced in module `LESSON-05-E-1`, namely, `not`,
 `true`, and `false`, is not imported by that module. You can solve this problem
- by simply importing the modules containing the syntax you want to use in your
+by simply importing the modules containing the syntax you want to use in your
 sentences.
 
 ## Main syntax and semantics modules
 
 When we are compiling a K definition, we need to know where to start. We
 designate two specific **entry point modules**: the **main syntax module**
-and the **main semantics module**. The main syntax module, as well as all the
-modules it imports recursively, are used to create the parser for programs that
-you use to parse programs that you execute with `krun`. The main semantics
-module, as well as all the modules it imports recursively, are used to
-determine the rules that can be applied at runtime in order to execute a
-program. For example, in the above example, if the main semantics module is
-module `LESSON-05-D-1`, then `not` is an uninterpreted function (i.e., has no
-rules associated with it), and the rules in module `LESSON-05-D` are not
-included.
-
-While you can specify the entry point modules explicitly by passing the
-`--main-module` and `--syntax-module` flags to `kompile`, by default, if you
-type `kompile foo.k`, then the main semantics module will be `FOO` and the
-main syntax module will be `FOO-SYNTAX`.
+and the **main semantics module**. The main syntax module, together with all 
+the modules it imports recursively, are used to generate the parser you execute
+with `kast`. The main semantics module, together with all the modules it 
+imports recursively, are used to generate the interpreter you execute with 
+`krun`. Take for example, the definition in `lesson-05-d.k`. If the main 
+semantics module is module `LESSON-05-D-1`, then `not` is an uninterpreted 
+function (i.e., has no rules associated with it) as the rules in module 
+`LESSON-05-D` are not included.
+
+You can specify the entry point modules explicitly by passing the flags
+`--main-module` (for the main semantics module) and `--syntax-module` (for the 
+main syntax module) to `kompile`. However, by default, if you run 
+`kompile foo.k`, then the main semantics module will be `FOO` and the
+main syntax module will be `FOO-SYNTAX`. This is the explanation behind the
+warning you get when running `kompile` with no flags specified.
+
+TODO: Order of imports doesn't matter accross a single-file K definition.
+It is a requirement that the main module is not imported by any other module.
 
 ## Splitting a definition into multiple files
 
-So far, while we have discussed ways to break definitions into separate
-conceptual components (modules), K also provides a mechanism for combining
-multiple files into a single K definition, namely, the **requires** directive.
-
-In K, the `requires` keyword has two meanings. The first, the **requires**
-statement, appears at the top of a K file, prior to any module declarations. It
-consists of the keyword `requires` followed by a double-quoted string. The
-second meaning of the `requires` keyword will be covered in a later lesson,
-but it is distinguished because the second case occurs only inside modules.
-
-The string passed to the **requires** statement contains a filename. When you run
-`kompile` on a file, it will look at all of the `requires` statements in that
-file, look up those files on disk, parse them, and then recursively process all
-the **requires** statements in those files. It then combines all the modules in all
-of those files together, and uses them collectively as the set of modules to
-which `imports` statements can refer.
+So far, we have discussed ways to split definitions into separate conceptual 
+components—modules. However, K also provides a mechanism for combining
+multiple files into a single K definition, namely, through the **requires** 
+directive.
+
+In K, the `requires` keyword has two meanings. The first is represented by the 
+**requires** statement which appears at the top of a K file, prior to any 
+module declarations. It consists of the keyword `requires` followed by a 
+double-quoted string. The second meaning of the `requires` keyword relates to
+side conditioning in rules and you will learn more about it in
+[Lesson 1.7](../07_side_conditions/README.md).
+
+The double quoted string passed to the **requires** statement contains a 
+filename. When you run `kompile` on a file, it will look at all of the 
+`requires` statements in that file, search those files on disk, parse them, 
+and then recursively process all the **requires** statements in those files. 
+It then combines all the modules in all of those files together, and uses 
+them collectively as the set of modules to which `imports` statements can 
+refer.
 
 ## Putting it all together
 
-Putting it all together, here is one possible way in which we could break the
-definition `lesson-02-c.k` from [Lesson 1.2](../02_basics/README.md) into
-multiple files and modules:
+Recall the definition in file `lesson-02-c.k` from 
+[Lesson 1.2](../02_basics/README.md). One way of splitting it into multiple 
+files and modules is the following:
 
-`colors.k`:
+- `colors.k`:
 
 ```k
 module COLORS
+
   syntax Color ::= Yellow()
                  | Blue()
+
 endmodule
 ```
 
-`fruits.k`:
+- `fruits.k`:
 
 ```k
 module FRUITS
+
   syntax Fruit ::= Banana()
                  | Blueberry()
+
 endmodule
 ```
 
-`colorOf.k`:
+- `colorOf.k`:
 
 ```{.k .exclude}
 requires "fruits.k"
 requires "colors.k"
 
 module COLOROF-SYNTAX
+
   imports COLORS
   imports FRUITS
 
   syntax Color ::= colorOf(Fruit) [function]
+
 endmodule
 
 module COLOROF
+
   imports COLOROF-SYNTAX
 
   rule colorOf(Banana()) => Yellow()
   rule colorOf(Blueberry()) => Blue()
+
 endmodule
 ```
 
@@ -214,24 +249,22 @@ same way as the original, single-module definition.
 
 Modify the name of the `COLOROF` module, and then recompile the definition.
 Try to understand why you now get a compiler error. Then, resolve this compiler
-error by passing the `--main-module` and `--syntax-module` flags to kompile.
+error by passing the `--main-module` and `--syntax-module` flags to `kompile`.
 
 ## Include path
 
-One note can be made about how paths are resolved in `requires` statements.
-
-By default, the path you specify is allowed to be an absolute or a relative
-path. If the path is absolute, that exact file is imported. If the path is
-relative, a matching file is looked for within all of the
-**include directories** specified to the compiler. By default, the include
-directories include the current working directory, followed by the
-`include/kframework/builtin` directory within your installation of K. You can
-also pass one or more directories to `kompile` via the `-I` command line flag,
-in which case these directories are prepended to the beginning of the list.
+Paths specified for `requires` statements can be absolute or relative. If the 
+path is absolute, that exact file is imported. If the path is relative, a 
+matching file is searched within all the **include directories** specified to 
+the compiler. By default, the include directories comprise the current working
+directory, followed by the `include/kframework/builtin` directory within your 
+installation of K. You can also pass one or more directories to `kompile` via 
+the `-I` flag, in which case these directories are prepended to the beginning 
+of the list.
 
 ## Exercises
 
-1. Take the solution to Lesson 1.4, Exercise 2 which included the explicit
+1. Take the solution to Exercise 2 in Lesson 1.4 which included the explicit
 priority and associativity declarations, and modify the definition so that
 the syntax of integers and brackets is in one module, the syntax of addition,
 subtraction, and unary negation is in another module, and the syntax of
@@ -244,7 +277,7 @@ separate modules in separate files.
 
 3. Place the file containing the syntax from Exercise 2 in another directory,
 then recompile the definition. Observe why a compilation error occurs. Then
-fix the compiler error by passing `-I` to kompile.
+fix the compiler error by passing `-I` to `kompile`.
 
 ## Next lesson