Merge pull request #847 from jmchapman/master

all `plc example` evaluation tests passing
IntersectMBO · Apr 25, 2019 · dfcaeb4 · dfcaeb4
2 parents bac510d + a64d5ce
commit dfcaeb4
Show file tree

Hide file tree

Showing 14 changed files with 532 additions and 155 deletions.
diff --git a/metatheory/Algorithmic/Main.lagda b/metatheory/Algorithmic/Main.lagda
@@ -50,20 +50,26 @@ lemma1 = primTrustMe
 lemma2 : length str2 ≡ 7
 lemma2 = primTrustMe
 
+{-
 constr1 : ∀{Γ} → Γ ⊢ con bytestring (size⋆ 16)
 constr1 = con (bytestring 16 str1 (subst (λ x → x Data.Nat.≤ 16) (sym lemma1) (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))))
+-}
 
+{-
 constr2 : ∀{Γ} → Γ ⊢ con bytestring (size⋆ 16)
 constr2 = con (bytestring 16 str2 (subst (λ x → x Data.Nat.≤ 16) (sym lemma2) (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))))
+-}
 
+{-
 append12 : ∀{Γ} → Γ ⊢ con bytestring (size⋆ 16)
 append12 = builtin concatenate (λ { Z → size⋆ 16 ; (S ())}) (constr1 ,, constr2 ,, tt)
+-}
 
 con1 : ∀{Γ} → Γ ⊢ con integer (size⋆ 8)
-con1 = con (integer 8 (pos 1) (-≤+ ,, (+≤+ (s≤s (s≤s z≤n)))))
+con1 = con (integer 8 (pos 1) _) -- (-≤+ ,, (+≤+ (s≤s (s≤s z≤n)))))
 
 con2 : ∀{Γ} → Γ ⊢ con integer (size⋆ 8)
-con2 = con (integer 8 (pos 2) (-≤+ ,, (+≤+ (s≤s (s≤s (s≤s z≤n))))))
+con2 = con (integer 8 (pos 2) _) -- (-≤+ ,, (+≤+ (s≤s (s≤s (s≤s z≤n))))))
 
 builtin2plus2 : ∅ ⊢ con integer (size⋆ 8)
 builtin2plus2 = builtin

diff --git a/metatheory/Algorithmic/Reduction.lagda b/metatheory/Algorithmic/Reduction.lagda
@@ -59,12 +59,38 @@ data Value :  ∀ {J Γ} {A : ∥ Γ ∥ ⊢Nf⋆ J} → Γ ⊢ A → Set where
 \end{code}
 
 \begin{code}
+VTel : ∀ Γ Δ → (∀ {K} → Δ ∋⋆ K → ∥ Γ ∥ ⊢Nf⋆ K) → List (Δ ⊢Nf⋆ *) → Set
+
 data Error :  ∀ {Γ} {A : ∥ Γ ∥ ⊢Nf⋆ *} → Γ ⊢ A → Set where
+  -- a genuine runtime error returned from a builtin
   E-error : ∀{Γ}{A : ∥ Γ ∥ ⊢Nf⋆ *} → Error (error {Γ} A)
+
+  -- error inside somewhere
+  E-·₁ : ∀{Γ}{A B : ∥ Γ ∥ ⊢Nf⋆ *} {L : Γ ⊢ A ⇒ B}{M : Γ ⊢ A}
+    → Error L → Error (L · M)
+  E-·₂ : ∀{Γ}{A B : ∥ Γ ∥ ⊢Nf⋆ *} {L : Γ ⊢ A ⇒ B}{M : Γ ⊢ A}
+    → Error M → Error (L · M)
+  E-·⋆ : ∀{Γ K}{B : ∥ Γ ∥ ,⋆ K ⊢Nf⋆ *}{L : Γ ⊢ Π B}{A : ∥ Γ ∥ ⊢Nf⋆ K}
+    → Error L → Error (L ·⋆ A)
+  E-unwrap : ∀{Γ K}
+    → {pat : ∥ Γ ∥ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *}
+    → {arg : ∥ Γ ∥ ⊢Nf⋆ K}
+    → {L : Γ ⊢ ne (μ1 · pat · arg)} → Error L → Error (unwrap1 L)
+  E-builtin : ∀{Γ}  → (bn : Builtin)
+    → let Δ ,, As ,, C = SIG bn in
+      (σ : ∀ {K} → Δ ∋⋆ K → ∥ Γ ∥ ⊢Nf⋆ K)
+    → (tel : Tel Γ Δ σ As)
+    → ∀ Bs Ds
+    → (vtel : VTel Γ Δ σ Bs)
+    → ∀{C}{t : Γ ⊢ substNf σ C}
+    → Error t
+    → (p : Bs ++ (C ∷ Ds) ≡ As)
+    → (tel' : Tel Γ Δ σ Ds)
+    → Error (builtin bn σ tel)
+
 \end{code}
 
 \begin{code}
-VTel : ∀ Γ Δ → (∀ {K} → Δ ∋⋆ K → ∥ Γ ∥ ⊢Nf⋆ K) → List (Δ ⊢Nf⋆ *) → Set
 VTel Γ Δ σ [] = ⊤
 VTel Γ Δ σ (A ∷ As) = Σ (Γ ⊢ substNf σ A) λ t → Value t × VTel Γ Δ σ As
 
@@ -332,6 +358,7 @@ data _—→_ : ∀ {J Γ} {A : ∥ Γ ∥ ⊢Nf⋆ J} → (Γ ⊢ A) → (Γ
       --------------
     → V · M —→ V · M′
 
+{-
   E-·₁ : ∀ {Γ A B} {L : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
     → Error L
       -----------------
@@ -341,17 +368,17 @@ data _—→_ : ∀ {J Γ} {A : ∥ Γ ∥ ⊢Nf⋆ J} → (Γ ⊢ A) → (Γ
     → Error M
       -----------------
     → L · M —→ error _
-
+-}
   ξ-·⋆ : ∀ {Γ K}{B : ∥ Γ ∥ ,⋆ K ⊢Nf⋆ *}{L L′ : Γ ⊢ Π B}{A}
     → L —→ L′
       -----------------
     → L ·⋆ A —→ L′ ·⋆ A
-
+{-
   E-·⋆ : ∀ {Γ K}{B : ∥ Γ ∥ ,⋆ K ⊢Nf⋆ *}{L : Γ ⊢ Π B}{A}
     → Error L
       -----------------
     → L ·⋆ A —→ error _
-
+-}
   β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
     → Value W
       -------------------
@@ -373,14 +400,14 @@ data _—→_ : ∀ {J Γ} {A : ∥ Γ ∥ ⊢Nf⋆ J} → (Γ ⊢ A) → (Γ
     → {M M' : Γ ⊢ ne (μ1 · pat · arg)}
     → M —→ M'
     → unwrap1 M —→ unwrap1 M'
-
+{-
   E-unwrap1 : ∀{Γ K}
     → {pat : ∥ Γ ∥ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *}
     → {arg : ∥ Γ ∥ ⊢Nf⋆ K}
     → {M : Γ ⊢ ne (μ1 · pat · arg)}
     → Error M
     → unwrap1 M —→ error _
-
+-}
 
   β-builtin : ∀{Γ}
     → (bn : Builtin)
@@ -405,6 +432,7 @@ data _—→_ : ∀ {J Γ} {A : ∥ Γ ∥ ⊢Nf⋆ J} → (Γ ⊢ A) → (Γ
       —→
       builtin bn σ (reconstTel Bs Ds σ vtel t' p tel')
 
+{-
   E-builtin : ∀{Γ}  → (bn : Builtin)
     → let Δ ,, As ,, C = SIG bn in
       (σ : ∀ {K} → Δ ∋⋆ K → ∥ Γ ∥ ⊢Nf⋆ K)
@@ -418,7 +446,7 @@ data _—→_ : ∀ {J Γ} {A : ∥ Γ ∥ ⊢Nf⋆ J} → (Γ ⊢ A) → (Γ
     → builtin bn σ tel
       —→
       error _
-
+-}
 
 \end{code}
 
@@ -504,20 +532,20 @@ progressTel {As = A ∷ As} (t ,, tel) | done vt | error Bs Ds vtel E q tel' = e
 progress (` ())
 progress (ƛ M) = done V-ƛ
 progress (M · N) with progress M
-...                   | error EM  = step (E-·₁ EM)
+...                   | error EM  = error (E-·₁ EM)
 progress (M · N)      | step p = step (ξ-·₁ p)
 progress (.(ƛ _) · N) | done V-ƛ with progress N
-...                              | error EN  = step (E-·₂ EN)
+...                              | error EN  = error (E-·₂ EN)
 progress (.(ƛ _) · N) | done V-ƛ | step p  = step (ξ-·₂ V-ƛ p)
 progress (.(ƛ _) · N) | done V-ƛ | done VN = step (β-ƛ VN)
 progress (Λ M) = done V-Λ_
 progress (M ·⋆ A) with progress M
-...               | error EM  = step (E-·⋆ EM)
+...               | error EM = error (E-·⋆ EM)
 progress (M ·⋆ A) | step p = step (ξ-·⋆ p)
 progress (.(Λ _) ·⋆ A) | done V-Λ_ = step β-Λ
 progress (wrap1 pat arg term) = done V-wrap1
-progress (unwrap1 M)       with progress M
-...                  | error EM  = step (E-unwrap1 EM)
+progress (unwrap1 M) with progress M
+...                  | error EM  = error (E-unwrap EM)
 progress (unwrap1 M) | step p = step (ξ-unwrap1 p)
 progress (unwrap1 .(wrap1 _ _ _)) | done V-wrap1 = step β-wrap1
 progress (con (integer s i x))    = done (V-con _)
@@ -528,5 +556,5 @@ progress (builtin bn σ X) | done VX = step (β-builtin bn σ X VX)
 progress (builtin bn σ X) | step Bs Ds vtel p q tel' =
   step (ξ-builtin bn σ X Bs Ds vtel p q tel')
 progress (builtin bn σ X) | error Bs Ds vtel p q tel' =
-  step (E-builtin bn σ X Bs Ds vtel p q tel')
+  error (E-builtin bn σ X Bs Ds vtel p q tel')
 progress (error A)        = error E-error
diff --git a/metatheory/Algorithmic/Soundness.lagda b/metatheory/Algorithmic/Soundness.lagda
@@ -3,32 +3,33 @@ module Algorithmic.Soundness where
 
 open import Type
 open import Type.RenamingSubstitution
-import Declarative as Syn
-import Algorithmic as Norm
+import Declarative as Dec
+import Algorithmic as Alg
 open import Type.BetaNormal
 open import Type.Equality
 open import Type.BetaNBE
 open import Type.BetaNBE.Completeness
 open import Type.BetaNBE.Soundness
 open import Type.BetaNBE.Stability
 open import Type.BetaNBE.RenamingSubstitution
-open import Relation.Binary.PropositionalEquality renaming (subst to substEq) hiding ([_])
+open import Relation.Binary.PropositionalEquality
+  renaming (subst to substEq) hiding ([_])
 open import Algorithmic.Completeness
 
 open import Function
 \end{code}
 
 \begin{code}
-embCtx : Norm.Ctx → Syn.Ctx
-embCtx∥ : ∀ Γ → Norm.∥ Γ ∥ ≡ Syn.∥ embCtx Γ ∥
+embCtx : Alg.Ctx → Dec.Ctx
+embCtx∥ : ∀ Γ → Alg.∥ Γ ∥ ≡ Dec.∥ embCtx Γ ∥
 
-embCtx Norm.∅       = Syn.∅
-embCtx (Γ Norm.,⋆ K) = embCtx Γ Syn.,⋆ K
-embCtx (Γ Norm., A)  = embCtx Γ Syn., substEq (_⊢⋆ _) (embCtx∥ Γ) (embNf A)
+embCtx Alg.∅       = Dec.∅
+embCtx (Γ Alg.,⋆ K) = embCtx Γ Dec.,⋆ K
+embCtx (Γ Alg., A)  = embCtx Γ Dec., substEq (_⊢⋆ _) (embCtx∥ Γ) (embNf A)
 
-embCtx∥ Norm.∅       = refl
-embCtx∥ (Γ Norm.,⋆ K) = cong (_,⋆ K) (embCtx∥ Γ)
-embCtx∥ (Γ Norm., A)  = embCtx∥ Γ
+embCtx∥ Alg.∅       = refl
+embCtx∥ (Γ Alg.,⋆ K) = cong (_,⋆ K) (embCtx∥ Γ)
+embCtx∥ (Γ Alg., A)  = embCtx∥ Γ
 \end{code}
 
 
@@ -43,30 +44,30 @@ lemT' A refl refl = sym (rename-embNf S A)
 \end{code}
 
 \begin{code}
-subst∋' : ∀ {Γ Γ' K}{A : Syn.∥ Γ ∥ ⊢⋆ K}{A' : Syn.∥ Γ' ∥ ⊢⋆ K}
+subst∋' : ∀ {Γ Γ' K}{A : Dec.∥ Γ ∥ ⊢⋆ K}{A' : Dec.∥ Γ' ∥ ⊢⋆ K}
  → (p : Γ ≡ Γ')
- → substEq (_⊢⋆ K) (cong Syn.∥_∥ p) A ≡ A' →
- (Γ Syn.∋ A) → Γ' Syn.∋ A'
+ → substEq (_⊢⋆ K) (cong Dec.∥_∥ p) A ≡ A' →
+ (Γ Dec.∋ A) → Γ' Dec.∋ A'
 subst∋' refl refl α = α
 \end{code}
 
 \begin{code}
-embTyVar : ∀{Γ K}{A : Norm.∥ Γ ∥ ⊢Nf⋆ K}
-  → Γ Norm.∋ A
-  → embCtx Γ Syn.∋ substEq (_⊢⋆ K) (embCtx∥ Γ) (embNf A)
-embTyVar Norm.Z     = Syn.Z
-embTyVar (Norm.S α) = Syn.S (embTyVar α)
-embTyVar {Γ Norm.,⋆ K} (Norm.T {A = A} α) = subst∋'
+embVar : ∀{Γ K}{A : Alg.∥ Γ ∥ ⊢Nf⋆ K}
+  → Γ Alg.∋ A
+  → embCtx Γ Dec.∋ substEq (_⊢⋆ K) (embCtx∥ Γ) (embNf A)
+embVar Alg.Z     = Dec.Z
+embVar (Alg.S α) = Dec.S (embVar α)
+embVar {Γ Alg.,⋆ K} (Alg.T {A = A} α) = subst∋'
   refl
-  (lemT' A (embCtx∥ Γ) (embCtx∥ (Γ Norm.,⋆ K)))
-  (Syn.T (embTyVar α))
+  (lemT' A (embCtx∥ Γ) (embCtx∥ (Γ Alg.,⋆ K)))
+  (Dec.T (embVar α))
 \end{code}
 
 \begin{code}
-subst⊢' : ∀ {Γ Γ' K}{A : Syn.∥ Γ ∥ ⊢⋆ K}{A' : Syn.∥ Γ' ∥ ⊢⋆ K}
+subst⊢' : ∀ {Γ Γ' K}{A : Dec.∥ Γ ∥ ⊢⋆ K}{A' : Dec.∥ Γ' ∥ ⊢⋆ K}
  → (p : Γ ≡ Γ')
- → substEq (_⊢⋆ K) (cong Syn.∥_∥ p) A ≡ A' →
- (Γ Syn.⊢ A) → Γ' Syn.⊢ A'
+ → substEq (_⊢⋆ K) (cong Dec.∥_∥ p) A ≡ A' →
+ (Γ Dec.⊢ A) → Γ' Dec.⊢ A'
 subst⊢' refl refl α = α
 \end{code}
 
@@ -165,12 +166,12 @@ substTC' : ∀{Γ Γ'}(p : Γ ≡ Γ')(s : Γ ⊢⋆ #)(tcn : TyCon)
   → STermCon.TermCon (con tcn (substEq (_⊢⋆ #) p s))
 substTC' refl s tcn t = t
 
-embTypeTC : ∀{φ}{A : φ ⊢Nf⋆ *}
+embTC : ∀{φ}{A : φ ⊢Nf⋆ *}
   → NTermCon.TermCon A
   → STermCon.TermCon (embNf A)
-embTypeTC (NTermCon.integer s i p)    = STermCon.integer s i p
-embTypeTC (NTermCon.bytestring s b p) = STermCon.bytestring s b p 
-embTypeTC (NTermCon.size s)           = STermCon.size s
+embTC (NTermCon.integer s i p)    = STermCon.integer s i p
+embTC (NTermCon.bytestring s b p) = STermCon.bytestring s b p 
+embTC (NTermCon.size s)           = STermCon.size s
 \end{code}
 \begin{code}
 open import Data.Product renaming (_,_ to _,,_)
@@ -262,69 +263,69 @@ embTel : ∀{Γ Δ Δ'}(q : Δ' ≡ Δ)
   → (As  : List (Δ ⊢Nf⋆ *))
   → (As' : List (Δ' ⊢⋆ *))
   → embList As ≡βL substEq (λ Δ → List (Δ ⊢⋆ *)) q As'
-  → (σ : {J : Kind} → Δ ∋⋆ J → Norm.∥ Γ ∥ ⊢Nf⋆ J)
-  → Norm.Tel Γ Δ σ As
-  → Syn.Tel (embCtx Γ) Δ'
+  → (σ : {J : Kind} → Δ ∋⋆ J → Alg.∥ Γ ∥ ⊢Nf⋆ J)
+  → Alg.Tel Γ Δ σ As
+  → Dec.Tel (embCtx Γ) Δ'
       (λ {J} α →
          substEq (_⊢⋆ J) (embCtx∥ Γ)
          (embNf (σ (substEq (_∋⋆ J) q α))))
       As'
 
-embTy : ∀{Γ K}{A : Norm.∥ Γ ∥ ⊢Nf⋆ K}
-  → Γ Norm.⊢ A
-  → embCtx Γ Syn.⊢ substEq (_⊢⋆ K) (embCtx∥ Γ) (embNf A)
+emb : ∀{Γ K}{A : Alg.∥ Γ ∥ ⊢Nf⋆ K}
+  → Γ Alg.⊢ A
+  → embCtx Γ Dec.⊢ substEq (_⊢⋆ K) (embCtx∥ Γ) (embNf A)
 
 embTel refl [] [] p σ x = tt
 embTel refl [] (A' ∷ As') () σ x
 embTel refl (A ∷ As) [] () σ x
 embTel {Γ} refl (A ∷ As) (A' ∷ As') (p ,, p') σ (t ,, tel) =
-  Syn.conv (lemsub A A' (embCtx∥ Γ)  σ p) (embTy t)
+  Dec.conv (lemsub A A' (embCtx∥ Γ)  σ p) (emb t)
   ,,
   embTel refl As As' p' σ tel
 
-embTy (Norm.` α) = Syn.` (embTyVar α)
-embTy {Γ} (Norm.ƛ {A = A}{B} t) =
-  subst⊢' refl (sym (lemƛ' A B (embCtx∥ Γ)) ) (Syn.ƛ (embTy t))
-embTy {Γ} (Norm._·_ {A = A}{B} t u) =
-  subst⊢' refl (lemƛ' A B (embCtx∥ Γ)) (embTy t) Syn.· embTy u
-embTy {Γ} (Norm.Λ {B = B} t) =
-  subst⊢' refl (lemΠ' (embCtx∥ Γ) (embCtx∥ (Γ Norm.,⋆ _)) B) (Syn.Λ (embTy t))
-embTy {Γ}(Norm._·⋆_ {K = K}{B = B} t A) = Syn.conv
-  (lem[]'' (embCtx∥ Γ) (embCtx∥ (Γ Norm.,⋆ K)) A B)
-  (Syn._·⋆_
-    (subst⊢' refl (sym (lemΠ' (embCtx∥ Γ) (embCtx∥ (Γ Norm.,⋆ K)) B)) (embTy t))
+emb (Alg.` α) = Dec.` (embVar α)
+emb {Γ} (Alg.ƛ {A = A}{B} t) =
+  subst⊢' refl (sym (lemƛ' A B (embCtx∥ Γ)) ) (Dec.ƛ (emb t))
+emb {Γ} (Alg._·_ {A = A}{B} t u) =
+  subst⊢' refl (lemƛ' A B (embCtx∥ Γ)) (emb t) Dec.· emb u
+emb {Γ} (Alg.Λ {B = B} t) =
+  subst⊢' refl (lemΠ' (embCtx∥ Γ) (embCtx∥ (Γ Alg.,⋆ _)) B) (Dec.Λ (emb t))
+emb {Γ}(Alg._·⋆_ {K = K}{B = B} t A) = Dec.conv
+  (lem[]'' (embCtx∥ Γ) (embCtx∥ (Γ Alg.,⋆ K)) A B)
+  (Dec._·⋆_
+    (subst⊢' refl (sym (lemΠ' (embCtx∥ Γ) (embCtx∥ (Γ Alg.,⋆ K)) B)) (emb t))
     (substEq (_⊢⋆ K) (embCtx∥ Γ) (embNf A)))
-embTy {Γ} (Norm.wrap1 pat arg t) = subst⊢'
+emb {Γ} (Alg.wrap1 pat arg t) = subst⊢'
   refl
   (sym (lemμ'' (embCtx∥ Γ) pat arg))
-  (Syn.wrap1
+  (Dec.wrap1
     (substEq (_⊢⋆ _) (embCtx∥ Γ) (embNf pat))
     (substEq (_⊢⋆ _) (embCtx∥ Γ) (embNf arg))
-    (Syn.conv (sym≡β (lemμ''' (embCtx∥ Γ) pat arg)) (embTy t)))
-embTy {Γ} (Norm.unwrap1 {pat = pat}{arg} t) = Syn.conv
+    (Dec.conv (sym≡β (lemμ''' (embCtx∥ Γ) pat arg)) (emb t)))
+emb {Γ} (Alg.unwrap1 {pat = pat}{arg} t) = Dec.conv
   (lemμ'''
     (embCtx∥ Γ) pat arg)
-    (Syn.unwrap1 (subst⊢' refl (lemμ'' (embCtx∥ Γ) pat arg) (embTy t)))
-embTy {Γ} (Norm.con  {s = s}{tcn = tcn} t ) = subst⊢'
+    (Dec.unwrap1 (subst⊢' refl (lemμ'' (embCtx∥ Γ) pat arg) (emb t)))
+emb {Γ} (Alg.con  {s = s}{tcn = tcn} t ) = subst⊢'
   refl
   (lemcon' (embCtx∥ Γ) tcn s)
-  (Syn.con (substTC' (embCtx∥ Γ) (embNf s) tcn (embTypeTC t)))
-embTy {Γ} (Norm.builtin bn σ tel) = let
+  (Dec.con (substTC' (embCtx∥ Γ) (embNf s) tcn (embTC t)))
+emb {Γ} (Alg.builtin bn σ tel) = let
   Δ  ,, As  ,, C  = SSig.SIG bn
   Δ' ,, As' ,, C' = NSig.SIG bn
-  in Syn.conv
+  in Dec.conv
     (lemσ' bn (embCtx∥ Γ) C C' (nfTypeSIG≡₁ bn) σ (nfTypeSIG≡₂ bn))
-    (Syn.builtin
+    (Dec.builtin
       bn
       (λ {J} α → substEq
         (_⊢⋆ J)
         (embCtx∥ Γ)
         (embNf (σ (substEq (_∋⋆ J) (nfTypeSIG≡₁ bn) α))))
       (embTel (nfTypeSIG≡₁ bn) As' As (lemList' bn) σ tel))
-embTy {Γ} (Norm.error A) = Syn.error (substEq (_⊢⋆ _) (embCtx∥ Γ) (embNf A) )
+emb {Γ} (Alg.error A) = Dec.error (substEq (_⊢⋆ _) (embCtx∥ Γ) (embNf A) )
 
-soundnessT : ∀{Γ K}{A : Norm.∥ Γ ∥ ⊢Nf⋆ K}
-  → Γ Norm.⊢ A
-  → embCtx Γ Syn.⊢ substEq (_⊢⋆ K) (embCtx∥ Γ) (embNf A)
-soundnessT = embTy
+soundnessT : ∀{Γ K}{A : Alg.∥ Γ ∥ ⊢Nf⋆ K}
+  → Γ Alg.⊢ A
+  → embCtx Γ Dec.⊢ substEq (_⊢⋆ K) (embCtx∥ Γ) (embNf A)
+soundnessT = emb
 \end{code}