diff --git a/docs/SUMMARY.md b/docs/SUMMARY.md index 3cd8e535c..f425c6b9a 100644 --- a/docs/SUMMARY.md +++ b/docs/SUMMARY.md @@ -30,9 +30,12 @@ - [Standard library](./reference/stdlib.md) - [Language reference](./reference/language/README.md) + - [Project](./reference/language/project.md) - [Functions](./reference/language/functions.md) + - [Infix operators](./reference/language/infix.md) - [Data types](./reference/language/datatypes.md) - [Modules](./reference/language/modules.md) + - [Statements](./reference/language/statement.md) - [Local definitions](./reference/language/let.md) - [Control structures](./reference/language/control.md) - [Comments](./reference/language/comments.md) diff --git a/docs/reference/language/infix.md b/docs/reference/language/infix.md new file mode 100644 index 000000000..0d93696db --- /dev/null +++ b/docs/reference/language/infix.md @@ -0,0 +1,3 @@ +# Infix operators + +TODO diff --git a/docs/reference/language/modules.md b/docs/reference/language/modules.md index a0a45b73c..6c81f3404 100644 --- a/docs/reference/language/modules.md +++ b/docs/reference/language/modules.md @@ -1,189 +1,140 @@ # Module system -## Defining a module +Modules are the way in which we split our programs in separate files. Juvix also +supports local modules, which provide a way to better organize different scopes +within a file. -The `module` keyword stars the declaration of a module followed by its -name and body. The module declaration ends with the `end` keyword. +We call top modules those who are defined at the top of a file. +We call local modules those who are defined inside another module. + +## Top modules + +A module has a name and a body, which comprises a sequence of +[statements](statement.md). + +In order to define a module named `Data.List` we will use the following syntax: ```juvix --- ModuleName.juvix -module ModuleName; +module Data.List; -end; + ``` -A Juvix project is a collection of Juvix modules inside one main -project folder containing a metadata file named `juvix.yaml`. Each Juvix -file has to define a module of the same name. The name of the -module must coincide with the path of its file relative to its -project's root directory. For example, if the file is -`root/Data/List.juvix` then the module must be called `Data.List`, -assuming `root` is the project's folder. +### Top module naming convention -To check that Juvix is correctly detecting your project's root, one can -run the command `juvix dev root File.juvix`. +Top modules that belong to a [project](project.md) must follow a naming +convention. That is, if `dir` is the root of a project, then the module in +`dir/Data/List.juvix` must be named `Data.List`. -## Importing modules +## _Import_ and _open_ statements -To bring into the current scope all module definitions from other -external modules, one can use the `import` keyword along with the -corresponding module name. This way, one gets all the imported names -qualified. +In order to access the definitions from another modules we use an +_import_ statement. To import some module named `Data.List` we will write ```juvix --- A.juvix -module A; - axiom - Nat : Type; - - axiom - zero : Nat; -end; - --- B.juvix -module B; - import A; - x : A.Nat; - x := A.zero; +import Data.List; ``` -Additionally, one can open an imported module making available -all its names by their unqualified name. +Now, we can access the definitions in the imported module using _qualified +names_. E.g., `Data.List.sort`. + +It is possible to import modules and give them a more convinent way thus: ```juvix --- A.juvix -module A; - axiom - Nat : Type; - - axiom - zero : Nat; -end; - --- B.juvix -module B; - import A; - open A; - x : Nat; - x := zero; -end; +import Data.List as List; ``` -However, opening modules may create name collisions if you already have -the imported names as definitions in the current module. In this case, -Juvix will complain with an error, letting you know which symbols are -ambiguous. For example, in module `B` below, the name `a` is ambiguous. +If we want to access the contents of a module without the need to qualify the +names, we use an _open statement_. The syntax is as follows: ```juvix --- A.juvix -module A; -axiom -A : Type; - -axiom -a : A; -end; - --- B.juvix -module B; - -import A; -open A; - -axiom -a : A; - -x := a; -end; +open Data.List; ``` -One alternative here is hiding the name `a` as follows. +Now we can simply write `sort`. It is important to remember that when we open a +module, that module must be in scope, i.e., it must either be imported +or defined as a local module + +Since importing and opening a module is done often, there is special syntax for +that. The following statement: ```juvix --- B.juvix -module B; -import A; -open A hiding {a}; - -axiom -a : A; - - -x := a; - -end; +open import Data.List; ``` -Now, we can use the `open import` syntax to simplify the `import-open` -statements. - -Instead of having: +Is equivalent to this: ```juvix -import Prelude; -open Prelude; +import Data.List; +open Data.List; ``` -We simplify it by the expression: +When opening a module, if we want to open an explicit subset of its definitions, +we must use the `using` keyword thus: ```juvix +open Data.List using {List; sort; reverse} +``` + +If we want to open all definitions of a module minus a subset, we +must use the `hiding` keyword thus: + +```juvix +open Data.List hiding {head; tail} +``` + +All opened definitions are available under the current module, but +they are not exported by default. Meaning that if another module imports the current +module, it will only be able to access the definitions defined there but not +those which have been opened. If we want opened definitions to be exported, we +must use the `public` keyword thus: + +``` +module Prelude; + +open import Data.List public; +``` + +Now, from another module we can access definitions in `Data.List` through the +`Prelude` module. + +``` +module MyModule; + open import Prelude; + +-- List, sort, reverse, etc. are now in scope ``` -The `hiding` keyword can be used within an `open-import` statement. +## Local modules -```juvix --- B.juvix -module A; -open import A hiding {a}; +Juvix modules have a hierarchical structure. So far we have discussed top level +modules, which have a one-to-one correspondence with files in the filesystem. On +the other hand, local modules are defined within another module. They can be +useful to group definitions within a file. -axiom -a : A; +The syntax for local modules is as follows: -x := a; +``` +module Path.To.TopModule; + +module Loc; + end; ``` -## Exporting symbols +After the definition of a local module, we can access its definitions by using +qualified names. Local modules can be opened by open statements in the same way +as top modules. -The module `C` below does not typecheck. Both symbols, originally -defined in module `A`, are not visible in module `C` after importing -`B`. The symbols `A` and `a` are not exported by the module `B`. To -export symbols from an imported module, one can use the `public` keyword -at the end of the corresponding `open` statement. For example, the -module `C` typechecks after marking the import of `A` as `public` in -module `B`. +Local modules inherit the scope of the parent module. Some shadowing rules +apply, and they probably follow your intuition: -```juvix --- A.juvix -module A; -axiom -A : Type; +1. Opening or defining a symbol shadows inherited instances of that symbol. +2. Opening a symbol does _not_ shadow a defined instanance of that symbol in the + current module. +3. Conversely, defining a symbol in the current module does _not_ shadow an + opened instance of that symbol. -axiom -a : A; - -end; - --- B.juvix -module B; -open import A; -end; - --- C.juvix -module C; -open import B; - -x : A; -x := a; -end; -``` - -Fix: - -```juvix --- B.juvix -module B; -open import A public; -end; -``` +As a consequence of 2 and 3, using a symbol that is both defined and opened +locally will result in an ambiguity error. diff --git a/docs/reference/language/modules_old.md b/docs/reference/language/modules_old.md new file mode 100644 index 000000000..28a2ced79 --- /dev/null +++ b/docs/reference/language/modules_old.md @@ -0,0 +1,166 @@ +# Module system + +## Defining a module + +The `module` keyword starts the declaration of a module followed by its +name and body. The module declaration ends with the `end` keyword. + +```juvix +-- ModuleName.juvix +module ModuleName; + +end; +``` + +A Juvix project is a collection of Juvix modules inside one main +project folder containing a metadata file named `juvix.yaml`. Each Juvix +file has to define a module of the same name. The name of the +module must coincide with the path of the its file relative to its +project's root directory. For example, if the file is +`root/Data/List.juvix` then the module must be called `Data.List`, +assuming `root` is the project's folder. + +To check that Juvix is correctly detecting your project's root, one can +run the command `juvix dev root File.juvix`. + +## Importing modules + +To bring into the current scope all module definitions from other +external modules, one can use the `import` keyword along with the +corresponding module name. This way, one gets all the imported names +qualified. + +```juvix +-- A.juvix +module A; + axiom Nat : Type; + axiom zero : Nat; +end; + +-- B.juvix +module B; + import A; + x : A.Nat; + x := A.zero; +``` + +Additionally, one can open an imported module making available +all its names by their unqualified name. + +```juvix +-- A.juvix +module A; + axiom Nat : Type; + axiom zero : Nat; +end; + +-- B.juvix +module B; + import A; + open A; + x : Nat; + x := zero; +``` + +However, opening modules may create name collisions if you already have +the imported names as definitions in the current module. In this case, +Juvix will complain with an error, letting you know which symbols are +ambiguous. For example, in module `B` below, the name `a` is ambiguous. + +```juvix +-- A.juvix +module A; +axiom A : Type; +axiom a : A; +end; + +-- B.juvix +module B; +import A; +open A; +axiom a : A; + +x := a; +end; +``` + +One alternative here is hiding the name `a` as follows. + +```juvix +-- B.juvix +module B; +import A; +open A hiding {a}; + +axiom a : A; +x := a; + +end; +``` + +Now, we can use the `open import` syntax to simplify the `import-open` +statements. + +Instead of having: + +```juvix +import Prelude; +open Prelude; +``` + +We simplify it by the expression: + +```juvix +open import Prelude; +``` + +The `hiding` keyword can be used within an `open-import` statement. + +```juvix +-- B.juvix +module A; +open import A hiding {a}; +axiom a : A; +x := a; +end; +``` + +## Exporting symbols + +The module `C` below does not typecheck. Both symbols, originally +defined in module `A`, are not visible in module `C` after importing +`B`. The symbols `A` and `a` are not exported by the module `B`. To +export symbols from an imported module, one can use the `public` keyword +at the end of the corresponding `open` statement. For example, the +module `C` typechecks after marking the import of `A` as `public` in +module `B`. + +```juvix +-- A.juvix +module A; +axiom A : Type; +axiom a : A; +end; + +-- B.juvix +module B; +open import A; +end; + +-- C.juvix +module C; +open import B; + +x : A; +x := a; +end; +``` + +Fix: + +```juvix +-- B.juvix +module B; +open import A public; +end; +``` diff --git a/docs/reference/language/project.md b/docs/reference/language/project.md new file mode 100644 index 000000000..50d11b81b --- /dev/null +++ b/docs/reference/language/project.md @@ -0,0 +1,37 @@ +# Juvix project + +A _juvix project_ is a collection of juvix modules plus some extra metadata +gathered in a `juvix.yaml` file. The most convenient way to create a juvix +project is to run the command `juvix init`. + +A project is rooted in a directory. The root is set by creating a `juvix.yaml`, +which contains the following fields: + +1. **name**: The name of the project. The name must not be empty and cannot + exceed 100 characters. Lower case letters, digits and hyphen `-` are + acceptable characters. The first letter must not be a hyphen. Summarizing, it + must match the following regexp: `[a-z0-9][a-z0-9-]{0,99}`. +2. **version** (_optional_): The version of the project. It must follow the + [SemVer](https://semver.org/) specification. If ommited the version will be + assumed to be _0.0.0_. +3. **dependencies** (_optional_): The dependencies of the project given as a + list. Each dependency is given as relative (or absolute) path to the root of + another juvix project. If the field is ommited, it will be assumed to contain + the juvix standard library as a dependency. + +As intuition would tell, a juvix module belongs to a juvix project if it is +placed in the subtree hanging from the root directory. This rule has two +exceptions: + +1. Modules in a hidden (or hanging from a hidden) directory are not part of the + project. E.g., if the root of a project is `dir`, then the module + `dir/.d/Lib.juvix` does not belong to the project rooted in `dir`. +1. A `juvix.yaml` file shadows other `juvix.yaml` files in parent + directories. E.g. if the root of a project is `dir` and the files + `dir/juvix.yaml` and `dir/nested/juvix.yaml` exist, then the module + `dir/nested/Lib.juvix` would belong to the project in `dir/nested`. + +## Module naming convention + +Modules that belong to a project must follow a naming convention. +See the documentation for [modules](modules.md). diff --git a/docs/reference/language/statement.md b/docs/reference/language/statement.md new file mode 100644 index 000000000..31ca5b024 --- /dev/null +++ b/docs/reference/language/statement.md @@ -0,0 +1,13 @@ +# Statement + +A juvix statement is each of the components of a module. +All statements are listed below: + +1. [type definition](datatypes.md). +2. [function definition](functions.md). +3. [axiom definition](axioms.md). +4. [fixity declaration](infix.md). +5. [function definition](functions.md). +6. [open](modules.md). +7. [import](modules.md). +8. [local module](modules.md).