From 7a70012791b347069dbfa82791cb0a41840af040 Mon Sep 17 00:00:00 2001
From: oflatt <oflatt@gmail.com>
Date: Fri, 2 Feb 2024 07:53:00 -0800
Subject: [PATCH] some examples

---
 tree_inputs/semantics.md | 81 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 79 insertions(+), 2 deletions(-)

diff --git a/tree_inputs/semantics.md b/tree_inputs/semantics.md
index 0661b8db5..3bd8d484e 100644
--- a/tree_inputs/semantics.md
+++ b/tree_inputs/semantics.md
@@ -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)))
 ```
@@ -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)))
 ```
@@ -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))))))
+```
+