-
Notifications
You must be signed in to change notification settings - Fork 9
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
a0379a8 feat: Add Simfony book (Christian Lewe) 74df9c3 chore: Add GitHub action to deploy book (Christian Lewe) 4250b4d chore: Add mdbook to nix flake (Christian Lewe) Pull request description: Write the first draft of the Simfony book. The book will be updated in following PRs. Add a GitHub action to deploy the book in GitHub pages. ACKs for top commit: apoelstra: ACK a0379a8; successfully ran local tests; much better! Tree-SHA512: db61450ab7dfe4f07d7f95a73ac5a67b7b355d2018a5411c2c86f561bc5414698481e46fd78e2073587a815aa720f0317fc092a416fddc4ae7faada8abfab890
- Loading branch information
Showing
13 changed files
with
669 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
name: Deploy Book on GitHub Pages | ||
on: | ||
push: | ||
branches: | ||
- master | ||
permissions: | ||
contents: write | ||
jobs: | ||
deploy: | ||
name: Deploy Book on GitHub Pages | ||
runs-on: ubuntu-latest | ||
|
||
steps: | ||
- name: Checkout | ||
uses: actions/checkout@v3 | ||
|
||
- name: Install nix | ||
uses: cachix/install-nix-action@v24 | ||
with: | ||
github_access_token: ${{ secrets.GITHUB_TOKEN }} | ||
|
||
- name: Build website | ||
run: | | ||
nix develop .#book --command bash -c "mdbook build" | ||
- name: Deploy to GitHub pages | ||
uses: JamesIves/github-pages-deploy-action@v4 | ||
with: | ||
branch: pages # The branch the action should deploy to. | ||
folder: book/book # The folder the action should deploy. | ||
clean: true # Automatically remove deleted files from the deployment branch. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -15,3 +15,6 @@ target/ | |
|
||
# Vscode project files | ||
.vscode | ||
|
||
# mdbook HTML output dir | ||
book/book/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
[book] | ||
authors = ["Christian Lewe"] | ||
language = "en" | ||
multilingual = false | ||
src = "src" | ||
title = "The Simfony Programming Language" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
# Summary | ||
|
||
[Introduction](./introduction.md) | ||
|
||
# Types and Values | ||
- [Types and Values](./type.md) | ||
- [Type Aliases](./type_alias.md) | ||
- [Type Casting](./type_casting.md) | ||
|
||
# Writing a Program | ||
- [Let Statements](./let_statement.md) | ||
- [Match Expression](./match_expression.md) | ||
- [Functions](./function.md) | ||
- [Programs](./program.md) | ||
|
||
# Locking and Unlocking UTXOs |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,105 @@ | ||
# Functions | ||
|
||
Functions are defined and called [just like in Rust](https://doc.rust-lang.org/std/keyword.fn.html). | ||
|
||
```rust | ||
fn add(x: u32, y: u32) -> u32 { | ||
let (carry, sum): (bool, u32) = jet::add_32(x, y); | ||
match carry { | ||
true => panic!(), // overflow | ||
false => {}, // ok | ||
}; | ||
sum | ||
} | ||
``` | ||
|
||
The above example defines a function called `add` that takes two parameters: variable `x` of type `u32` and variable `y` of type `u32`. The function returns a value of type `u32`. | ||
|
||
The body of the function is a block expression `{ ... }` that is executed from top to bottom. | ||
The function returns on the final line _(note the missing semicolon `;`)_. | ||
In the above example, `x` and `y` are added via the `add_32` jet. | ||
The function then checks if the carry is true, signaling an overflow, in which case it panics. | ||
On the last line, the value of `sum` is returned. | ||
|
||
The above function is called by writing its name `add` followed by a list of arguments `(40, 2)`. | ||
Each parameter needs an argument, so the list of arguments is as long as the list of arguments. | ||
Here, `x` is assigned the value `40` and `y` is assigned the value `2`. | ||
|
||
```rust | ||
let z: u32 = add(40, 2); | ||
``` | ||
|
||
## No early returns | ||
|
||
Simfony has no support for an early return via a "return" keyword. | ||
The only branching that is available is via [match expressions](./match_expression.md). | ||
|
||
## No recursion | ||
|
||
Simfony has no support for recursive function calls. | ||
A function can be called inside a function body if it has been defined before. | ||
This means that a function cannot call itself. | ||
Loops, where `f` calls `g` and `g` calls `f`, are also impossible. | ||
|
||
What _is_ possible are stratified function definitions, where level-0 functions depend on nothing, level-1 functions depend on level-0 functions, and so on. | ||
|
||
```rust | ||
fn level_0() -> u32 { | ||
0 | ||
} | ||
|
||
fn level_1() -> u32 { | ||
let (_, next) = jet::increment_32(level_0()); | ||
next | ||
} | ||
|
||
fn level_2() -> u32 { | ||
let (_, next) = jet::increment_32(level_1)); | ||
next | ||
} | ||
``` | ||
|
||
## Order matters | ||
|
||
If function `g` calls function `f`, then `f` **must** be defined before `g`. | ||
|
||
```rust | ||
fn f() -> u32 { | ||
42 | ||
} | ||
|
||
fn g() -> u32 { | ||
f() | ||
} | ||
``` | ||
|
||
## Main function | ||
|
||
The `main` function is the entry point of each Simfony program. | ||
Running a program means running its `main` function. | ||
Other functions are called from the `main` function. | ||
|
||
```rust | ||
fn main() { | ||
// ... | ||
} | ||
``` | ||
|
||
The `main` function is a reserved name and must exist in every program. | ||
Simfony programs are always "binaries". | ||
There is no support for "libraries". | ||
|
||
## Jets | ||
|
||
Jets are predefined and optimized functions for common usecases. | ||
|
||
```rust | ||
jet::add_32(40, 2) | ||
``` | ||
|
||
Jets live inside the namespace `jet`, which is why they are prefixed with `jet::`. | ||
They can be called without defining them manually. | ||
|
||
It is usually more efficient to call a jet than to manually compute a value. | ||
|
||
[The jet documentation](https://docs.rs/simfony-as-rust/latest/simfony_as_rust/jet/index.html) lists each jet and explains what it does. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
# Introduction | ||
|
||
Simfony is a high-level language for writing Bitcoin smart contracts. | ||
In other words, Simfony is a language for expressing spending conditions of UTXOs on the Bitcoin blockchain. | ||
|
||
Simfony looks and feels like [Rust](https://www.rust-lang.org/). | ||
Developers write Simfony, Bitcoin full nodes run Simplicity. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,68 @@ | ||
# Let Statement | ||
|
||
Variables are defined in let statements, [just like in Rust](https://doc.rust-lang.org/std/keyword.let.html). | ||
|
||
```rust | ||
let x: u32 = 1; | ||
``` | ||
|
||
The above let statement defines a variable called `x`. | ||
The variable is of type `u32` and it is assigned the value `1`. | ||
|
||
```rust | ||
let x: u32 = f(1337); | ||
``` | ||
|
||
Variables can be assigned to the output value of any expression, such as function calls. | ||
|
||
## Explicit typing | ||
|
||
In Simfony, the type of a defined variable **always** has to be written. | ||
This is different from Rust, which has better type inference. | ||
|
||
## Immutability | ||
|
||
Simfony variables are **always** immutable. | ||
There are no mutable variables. | ||
|
||
## Redefinition and scoping | ||
|
||
The same variable can be defined twice in the same scope. | ||
The later definition overrides the earlier definition. | ||
|
||
```rust | ||
let x: u32 = 1; | ||
let x: u32 = 2; | ||
assert!(jet::eq_32(x, 2)); // x == 2 | ||
``` | ||
|
||
Normal scoping rules apply: | ||
Variables from outer scopes are available inside inner scopes. | ||
A variable defined in an inner scope shadows a variable of the same name from an outer scope. | ||
|
||
```rust | ||
let x: u32 = 1; | ||
let y: u32 = 2; | ||
let z: u32 = { | ||
let x: u32 = 3; | ||
assert!(jet::eq_32(y, 2)); // y == 2 | ||
x | ||
}; | ||
assert!(jet::eq_32(x, 3)); // z == 3 | ||
``` | ||
|
||
## Pattern matching | ||
|
||
There is limited pattern matching support inside let statements. | ||
|
||
```rust | ||
let (x, y, _): (u8, u16, u32) = (1, 2, 3); | ||
let [x, _, z]: [u32; 3] = [1, 2, 3]; | ||
``` | ||
|
||
In the first line, the tuple `(1, 2, 3)` is deconstructed into the values `1`, `2` and `3`. | ||
These values are assigned to the variable names `x`, `y` and `_`. | ||
The variable name `_` is a special name that ignores its value. | ||
In the end, two variables are created: `x: u32 = 1` and `y: u16 = 2`. | ||
|
||
Similarly, arrays can be deconstructed element by element and assigned to a variable each. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,95 @@ | ||
# Match Expression | ||
|
||
A match expression conditionally executes code branches. | ||
Which branch is executed depends on the input to the match expression. | ||
|
||
```rust | ||
let result: u32 = match f(42) { | ||
Left(x: u32) => x, | ||
Right(x: u16) => jet::left_pad_low_16_32(x), | ||
}; | ||
``` | ||
|
||
In the above example, the output of the function call `f(42)` is matched. | ||
`f` returns an output of type `Either<u32, u16>`. | ||
If `f(42)` returns a value that matches the pattern `Left(x: u32)`, then the first match arm is executed. | ||
This arm simply returns the value `x`. | ||
Alternatively, if `f(42)` returns a value that matches the pattern `Right(x: u16)`, then the second match arm is executed. | ||
This arm extends the 16-bit number `x` to a 32-bit number by padding its left with zeroes. | ||
Because of type constraints, the output of `f` must match one of these two patterns. | ||
The whole match expression returns a value of type `u32`, from one of the two arms. | ||
|
||
## Explicit typing | ||
|
||
In Simfony, the type of variables inside match arms must **always** be written. | ||
This is different from Rust, which has better type inference. | ||
|
||
## Pattern matching | ||
|
||
There is limited support for pattern matching inside match expressions. | ||
|
||
Boolean values can be matched. | ||
The Boolean match expression is the replacement for an "if-then-else" in Simfony. | ||
|
||
```rust | ||
let bit_flip: bool = match false { | ||
false => true, | ||
true => false, | ||
}; | ||
``` | ||
|
||
Optional values can be matched. | ||
The `Some` arm introduces a variable which must be explicitly typed. | ||
|
||
```rust | ||
let unwrap_or_default: u32 = match Some(42) { | ||
None => 0, | ||
Some(x: u32) => x, | ||
}; | ||
``` | ||
|
||
Finally, `Either` values can be matched. | ||
Again, variables that are introduced in match arms must be explicitly typed. | ||
|
||
```rust | ||
let map_either: u32 = match Left(1337) { | ||
Left(x: u32) => f(x), | ||
Right(y: u32) => f(y), | ||
}; | ||
``` | ||
|
||
Match expressions don't support further pattern matching, in contrast to Rust. | ||
|
||
```rust | ||
let unwrap_or_default: u32 = match Some((4, 2)) { | ||
None => 0, | ||
// this doesn't compile | ||
Some((y, z): (u16, u16)) => <(u16, u16)>::into((y, z)), | ||
}; | ||
``` | ||
|
||
However, the match arm can contain code that performs the deconstruction. | ||
For example, the tuple `x` of type `(u16, u16)` can be deconstructed into two integers `y` and `z` of type `u16`. | ||
|
||
```rust | ||
let unwrap_or_default: u32 = match Some((4, 2)) { | ||
None => 0, | ||
Some(x: (u16, u16)) => { | ||
let (y, z): (u16, u16) = x; | ||
<(u16, u16)>::into((y, z)) | ||
} | ||
}; | ||
``` | ||
|
||
The match arm can also contain match expressions for further deconstruction. | ||
For example, the sum value `x` of type `Either<u32, u32>` can be matched as either `Left(y: u32)` or `Right(z: u32)`. | ||
|
||
```rust | ||
let unwrap_or_default: u32 = match Some(Left(42)) { | ||
None => 0, | ||
Some(x: Either<u32, u32>) => match x { | ||
Left(y: u32) => y, | ||
Right(z: u32) => z, | ||
}, | ||
}; | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
# Programs | ||
|
||
A Simfony program consists of a `main` [function](./function.md). | ||
|
||
A program may also have [type aliases](./type_alias.md) or custom [function definitions](./function.md). | ||
The `main` function comes last in the program, because everything it calls must be defined before it. | ||
|
||
```rust | ||
type Furlong = u32; | ||
type Mile = u32; | ||
|
||
fn to_miles(distance: Either<Furlong, Mile>) -> Mile { | ||
match distance { | ||
Left(furlongs: Furlong) => jet::divide_32(furlongs, 8), | ||
Right(miles: Mile) => miles, | ||
} | ||
} | ||
|
||
fn main() { | ||
let eight_furlongs: Either<Furlong, Mile> = Left(8); | ||
let one_mile: Either<Furlong, Mile> = Right(1); | ||
assert!(jet::eq_32(1, to_miles(eight_furlongs))); | ||
assert!(jet::eq_32(1, to_miles(one_mile))); | ||
} | ||
``` |
Oops, something went wrong.