Translation

We write ⟦e⟧Ξ to denote the translation of SimplicityHL expression e using environment Ξ from A.

The translation produces a Simplicity expression with source type A.

The target type depends on the SimplicityHL 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⟧Ξ = comp unit const 0bs: A → 𝟚^(2^n)

Byte string literal

If s is a hex string of 2^n digits

Then ⟦0xs⟧Ξ = comp unit 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⟧Ξ 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) => b, Right(y) => c, }⟧Ξ = 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