mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-04-20 03:03:25 -04:00
Documentation.
This commit is contained in:
@@ -11,6 +11,7 @@
|
||||
- [CLI](./cli/README.md)
|
||||
- [asm](./asm/README.md)
|
||||
- [Modules](./asm/modules.md)
|
||||
- [Declarations](./asm/declarations.md)
|
||||
- [Machines](./asm/machines.md)
|
||||
- [Registers](./asm/registers.md)
|
||||
- [Functions](./asm/functions.md)
|
||||
|
||||
13
book/src/asm/declarations.md
Normal file
13
book/src/asm/declarations.md
Normal file
@@ -0,0 +1,13 @@
|
||||
# Declarations
|
||||
|
||||
Symbols can be defined via ``let <name> = <value>;``. The value is a generic [PIL-expression](../pil/expressions.md)
|
||||
and its type is unconstrained (it can be a value, a function or even a higher-order function).
|
||||
|
||||
Other symbols available in the current module can be accessed by name, but it is also possible to specify
|
||||
full relative paths in the form of e.g. ``super::super::module_name::symbol``.
|
||||
|
||||
Here are some examples of how to define and use symbols:
|
||||
|
||||
```
|
||||
{{#include ../../../test_data/asm/book/declarations.asm}}
|
||||
```
|
||||
31
test_data/asm/book/declarations.asm
Normal file
31
test_data/asm/book/declarations.asm
Normal file
@@ -0,0 +1,31 @@
|
||||
mod utils {
|
||||
// This defines a function by means of a lambda expression that
|
||||
// computes the sum of an array of values.
|
||||
let sum = |len, arr| match len { 0 => 0, _ => arr[len - 1] + sum(len - 1, arr) };
|
||||
// A simple function that returns the input incremented by one.
|
||||
let incremented = |x| x + 1;
|
||||
// This is a function that takes an expression as input and returns
|
||||
// a constraint enforcing this expression increments by a certain value
|
||||
// between rows.
|
||||
let constrain_incremented_by = |x, inc| x' == x + inc;
|
||||
}
|
||||
|
||||
machine Main {
|
||||
// Machines create local scopes in the way functions create local scopes:
|
||||
// - all symbols in the machine's module are available without prefix,
|
||||
// - new symbols can be defined but are only available inside the machine.
|
||||
reg A;
|
||||
reg pc[@pc];
|
||||
|
||||
// This defines a witness column,
|
||||
let x;
|
||||
// and now we force it to stay unchanged.
|
||||
utils::constrain_incremented_by(x, 0);
|
||||
|
||||
// We define an instruction that uses a complicated way to increment a register.
|
||||
instr incr_a { A = utils::incremented(A) }
|
||||
|
||||
function main {
|
||||
return;
|
||||
}
|
||||
}
|
||||
@@ -9,6 +9,17 @@ mod submodule_in_folder;
|
||||
use submodule::Other as SubmoduleOther;
|
||||
use submodule_in_folder::Other as FolderSubmoduleOther;
|
||||
|
||||
let zero = 0;
|
||||
|
||||
// we can also define modules inline
|
||||
mod utils {
|
||||
// Each module has a fresh symbol list. Every external symbol needs to be imported,
|
||||
// even from the parent module.
|
||||
use super::zero;
|
||||
|
||||
let one = zero + 1;
|
||||
}
|
||||
|
||||
machine Main {
|
||||
// use a machine from another module by relative path
|
||||
my_module::Other a;
|
||||
|
||||
Reference in New Issue
Block a user