mirror of
https://github.com/anoma/juvix.git
synced 2024-12-13 19:49:20 +03:00
Documentation for projects and modules (#1962)
This commit is contained in:
janmasrovira
GitHub
parent
46360a753c
commit
96822c0383
@ -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)
|
||||
|
||||
3
docs/reference/language/infix.md
Normal file
3
docs/reference/language/infix.md
Normal file
@ -0,0 +1,3 @@
|
||||
# Infix operators
|
||||
|
||||
TODO
|
||||
@ -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;
|
||||
<body>
|
||||
```
|
||||
|
||||
A <u>Juvix project</u> 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 <u>module</u> 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 <u>open</u> 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;
|
||||
<body>
|
||||
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.
|
||||
|
||||
166
docs/reference/language/modules_old.md
Normal file
166
docs/reference/language/modules_old.md
Normal file
@ -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 <u>Juvix project</u> 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 <u>module</u> 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 <u>open</u> 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;
|
||||
```
|
||||
37
docs/reference/language/project.md
Normal file
37
docs/reference/language/project.md
Normal file
@ -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).
|
||||
13
docs/reference/language/statement.md
Normal file
13
docs/reference/language/statement.md
Normal file
@ -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).
|
||||
Loading…
Reference in New Issue
Block a user