Doc: Add translation

Author: uncomputable

doc/translation.md

@@ -0,0 +1,105 @@
+# Translation
+
+We write ⟦`e`⟧Ξ to denote the translation of Simphony expression `e` using environment Ξ from A.
+
+The translation produces a Simplicity expression with source type A.
+
+The target type depends on the Simphony expression `e`.
+
+## Unit literal
+
+⟦`()`⟧Ξ = unit: A → 𝟙
+
+## Product constructor
+
+If Ctx(Ξ) ⊩ `b`: B
+
+If Ctx(Ξ) ⊩ `c`: C
+
+Then ⟦`(b, c)`⟧Ξ = pair ⟦`b`⟧Ξ ⟦`c`⟧Ξ: A → B × C
+
+## Left constructor
+
+If Ctx(Ξ) ⊩ `b`: B
+
+Then ⟦`Left(b)`⟧Ξ = injl ⟦`b`⟧Ξ: A → B + C
+
+For any C
+
+## Right constructor
+
+If Ctx(Ξ) ⊩ `c`: C
+
+Then ⟦`Right(c)`⟧Ξ = injr ⟦`c`⟧Ξ: A → B + C
+
+For any B
+
+## Bit string literal
+
+If `s` is a bit string of 2^n bits
+
+Then ⟦`0bs`⟧Ξ = const 0bs: A → 𝟚^(2^n)
+
+## Byte string literal
+
+If `s` is a hex string of 2^n digits
+
+Then ⟦`0xs`⟧Ξ = const 0xs: A → 𝟚^(4 * 2^n)
+
+## Variable
+
+If Ctx(Ξ)(`v`) = B
+
+Then ⟦`v`⟧Ξ = Ξ(`v`): A → B
+
+## Witness value
+
+Ctx(Ξ) ⊩ `witness(name)`: B
+
+Then ⟦`witness(name)`⟧Ξ = witness: A → B
+
+## Jet
+
+If `j` is the name of a jet of type B → C
+
+If Ctx(Ξ) ⊩ `b`: B
+
+Then ⟦`jet_j b`⟧Ξ = comp ⟦`b`⟧Ξ jet_j: A → C
+
+## Chaining
+
+If Ctx(Ξ) ⊩ `b`: 𝟙
+
+If Ctx(Ξ) ⊩ `c`: C
+
+Then ⟦`b; c`⟧Ξ = comp (pair ⟦`b`⟧Ξ ⟦`c`⟧Ξ) (drop iden): A → C
+
+## Let statement
+
+If Ctx(Ξ) ⊩ `b`: B
+
+If Product(PEnv(B, `p`), Ξ) ⊩ c: C
+
+Then ⟦`let p: B = b; c`⟧Ξ = comp (pair ⟦`b`⟧Ξ iden) ⟦`c`⟧Product(PEnv(B, `p`), Ξ): A → C
+
+## Match statement
+
+If Ctx(Ξ) ⊩ `a`: B + C
+
+If Product(PEnv(B, `x`), Ξ) ⊩ `b`: D
+
+If Product(PEnv(C, `y`), Ξ) ⊩ `c`: D
+
+Then ⟦`match a { Left(x) => a, Right(y) => b, }`⟧Ξ = comp (pair ⟦a⟧Ξ iden) (case ⟦b⟧Product(PEnv(B, `x`), Ξ) ⟦c⟧Product(PEnv(C, `y`), Ξ)): A → D
+
+## Left unwrap
+
+If Ctx(Ξ) ⊩ `b`: B + C
+
+Then ⟦`b.unwrap_left()`⟧Ξ = comp (pair ⟦`b`⟧Ξ unit) (assertl iden #{fail 0}): A → B
+
+## Right unwrap
+
+If Ctx(Ξ) ⊩ `c`: B + C
+
+Then ⟦`c.unwrap_right()`⟧Ξ = comp (pair ⟦`c`⟧Ξ unit) (assertr #{fail 0} iden): A → C