Skip to content

Commit

Permalink
some examples
Browse files Browse the repository at this point in the history
  • Loading branch information
oflatt committed Feb 2, 2024
1 parent 4839676 commit 7a70012
Showing 1 changed file with 79 additions and 2 deletions.
81 changes: 79 additions & 2 deletions tree_inputs/semantics.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@

In previous schemas, we might write
shared computation like this:
```
```scheme
(Let id1 some_impure_computation
(Add (Get (Arg id1) 0) (Get (Arg id1) 1)))
```
Expand All @@ -16,7 +16,7 @@ the argument is equal to `some_impure_computation`.
`Input`s allow us to avoid this id by
allowing us to refer to the impure computation directly:

```
```scheme
(Let
(Add (Get (Input some_impure_computation) 0) (Get (Input some_impure_computation) 1)))
```
Expand All @@ -26,3 +26,80 @@ Each `Let` can only have one `Input`.

Now, no ids are necessary because the
context is baked into the `Input` itself.


## Regions

`Function`, `Loop`, and `Let` all
create regions.
`Function` and `Loop` only refer to `Arg` and sub-regions.
`Let` only refers to `Input` and
sub-regions.


For a valid program, there is a 1 to 1 correspondance between a `Let`
and its `Input`.


Here are some examples.
First lets define a couple constants:
```
(let zero (Const (Global) (Int 0)))
(let one (Const (Global) (Int 1)))
```


This program is valid. The outer `Let` has `(Input one)` and
the inner `Let` has `(Input zero)`:
```scheme
(Let
(Add (Let (Neg (Input zero)))
(Input one)))
```

This program is invalid, since
the `Let` has two unique `Input`s:
```
(Let
(Add (Input zero)
(Input one)))
```

An `Input` can also have sub-regions.
The following valid program reads from address 0, doubles it, and negates the result twice:
```
(Let
(Neg
(Input
(Neg
(Let
(Add (Input (Read zero (IntT)))
(Input (Read zero (IntT)))))))))
```


A `Let` evaluates its input only once.
This program prints zero twice:
```
(Let
(All (Sequential)
(Cons
(Print zero)
(Cons
(Input (Print zero))
(Input (Print zero))))))
```


Inputs are evaluated before anything else.
This program prints zero, then one:
```
(Let
(All (Sequential)
(Cons
(Print one)
(Cons
(Input (Print zero))
(Input (Print zero))))))
```

0 comments on commit 7a70012

Please sign in to comment.