Adding Let in Contexts

src/Agda/Core/Context.agda

@@ -4,14 +4,15 @@ open import Utils.Either
 open import Utils.Tactics using (auto)
 open import Haskell.Extra.Dec
 open import Haskell.Extra.Erase
-open import Haskell.Law.Equality
+open import Haskell.Law.Equality hiding (subst)
 open import Haskell.Law.Monoid
 open import Haskell.Prelude hiding (All; s; t)
 
 open import Agda.Core.Name
+open import Agda.Core.Utils
 open import Agda.Core.GlobalScope using (Globals)
 open import Agda.Core.Syntax
-open import Agda.Core.Signature
+open import Agda.Core.Substitute
 
 module Agda.Core.Context
   {{@0 globals : Globals}}
@@ -26,32 +27,36 @@ private variable
 data Context : @0 Scope Name → Set where
   CtxEmpty  : Context mempty
   CtxExtend : Context α → (@0 x : Name) → Type α → Context  (α ▸ x)
-
+  CtxExtendLet : Context α → (@0 x : Name) → Term α → Type α → Context  (α ▸ x)
 {-# COMPILE AGDA2HS Context #-}
 
-_,_∶_ : Context α → (@0 x : Name) → Type α → Context  (α ▸ x)
-_,_∶_ = CtxExtend
-
-infix 4 _,_∶_
+pattern ⌈⌉ = CtxEmpty
+pattern _,_∶_ g x ty = CtxExtend g x ty
+pattern _,_≔_∶_ g x u ty = CtxExtendLet g x u ty
 
-{-# COMPILE AGDA2HS _,_∶_ inline #-}
+infixl 4 _,_∶_
+infixl 4 _,_≔_∶_
 
 private variable
   @0 Γ : Context α
 
 lookupVar : (Γ : Context α) (x : NameIn α) → Type α
-lookupVar CtxEmpty x = nameInEmptyCase x
-lookupVar (CtxExtend g y s) x = raiseType (rezz _) (nameInBindCase x
+lookupVar ⌈⌉ x = nameInEmptyCase x
+lookupVar (g , y ∶ s) x = raiseType (rezz _) (nameInBindCase x
+  (λ q → lookupVar g (⟨ _ ⟩ q))
+  (λ _ → s))
+lookupVar (g , y ≔ u ∶ s) x = raiseType (rezz _) (nameInBindCase x
   (λ q → lookupVar g (⟨ _ ⟩ q))
   (λ _ → s))
 
 {-# COMPILE AGDA2HS lookupVar #-}
 
 rezzScope : (Γ : Context α) → Rezz α
-rezzScope CtxEmpty = rezz _
-rezzScope (CtxExtend g x _) =
+rezzScope ⌈⌉ = rezz _
+rezzScope (g , x ∶ _) =
+  rezzCong (λ t → t <> (singleton x)) (rezzScope g)
+rezzScope (g , x ≔ _ ∶ _) =
   rezzCong (λ t → t <> (singleton x)) (rezzScope g)
-
 {-# COMPILE AGDA2HS rezzScope #-}
 
 addContextTel : Context α → Telescope α rβ  → Context (extScope α rβ)
@@ -60,3 +65,85 @@ addContextTel {α} c ⌈⌉ =
 addContextTel {α} c (ExtendTel {rβ = rβ} x ty telt) =
   subst0 Context (sym extScopeBind) (addContextTel (c , x ∶ ty) telt)
 {-# COMPILE AGDA2HS addContextTel #-}
+
+opaque
+  MaybeLet : @0 Scope Name → Set
+  MaybeLet α = (Maybe (Term α)) × Type α
+  {-# COMPILE AGDA2HS MaybeLet #-}
+
+  weakenMaybeLet : α ⊆ β → MaybeLet α → MaybeLet β
+  weakenMaybeLet s (Nothing , ty) = (Nothing , weaken s ty)
+  weakenMaybeLet s (Just u , ty) = (Just (weaken s u) , weaken s ty)
+  {-# COMPILE AGDA2HS weakenMaybeLet #-}
+
+  instance
+    iWeakenMaybeLet : Weaken MaybeLet
+    iWeakenMaybeLet .weaken = weakenMaybeLet
+    {-# COMPILE AGDA2HS iWeakenMaybeLet #-}
+
+  strengthenMaybeLet : α ⊆ β → MaybeLet β → Maybe (MaybeLet α)
+  strengthenMaybeLet s (Nothing , ty) = do
+    ty' ← strengthenType s ty
+    return (Nothing , ty')
+  strengthenMaybeLet s (Just u , ty) = do
+    u' ← strengthen s u
+    ty' ← strengthen s ty
+    return (Just u' , ty')
+  {-# COMPILE AGDA2HS strengthenMaybeLet #-}
+
+  instance
+    iStrengthenMaybeLet : Strengthen MaybeLet
+    iStrengthenMaybeLet .strengthen = strengthenMaybeLet
+    {-# COMPILE AGDA2HS iStrengthenMaybeLet #-}
+
+  substMaybeLet : α ⇒ β → MaybeLet α → MaybeLet β
+  substMaybeLet s (Nothing , ty) = (Nothing , subst s ty)
+  substMaybeLet s (Just u , ty) = (Just (subst s u) , subst s ty)
+  {-# COMPILE AGDA2HS substMaybeLet #-}
+
+  instance
+    iSubstMaybeLet : Substitute MaybeLet
+    iSubstMaybeLet .subst = substMaybeLet
+    {-# COMPILE AGDA2HS iSubstMaybeLet #-}
+
+
+data CtxView : @0 Scope Name → Set where
+  CtxViewEmpty : CtxView mempty
+  CtxViewExtend : CtxView α → (@0 x : Name) → MaybeLet α → CtxView (α ▸ x)
+{-# COMPILE AGDA2HS CtxView #-}
+
+private opaque
+  unfolding MaybeLet
+  contextToCtxView : Context α → CtxView α
+  contextToCtxView ⌈⌉ = CtxViewEmpty
+  contextToCtxView (g , x ∶ ty) = CtxViewExtend (contextToCtxView g) x (Nothing , ty)
+  contextToCtxView (g , x ≔ u ∶ ty) = CtxViewExtend (contextToCtxView g) x (Just u , ty)
+  {-# COMPILE AGDA2HS contextToCtxView #-}
+
+
+  ctxViewToContext : CtxView α → Context α
+  ctxViewToContext CtxViewEmpty = ⌈⌉
+  ctxViewToContext (CtxViewExtend g x (Nothing , ty)) = ctxViewToContext g , x ∶ ty
+  ctxViewToContext (CtxViewExtend g x (Just u , ty)) = ctxViewToContext g , x ≔ u ∶ ty
+  {-# COMPILE AGDA2HS ctxViewToContext #-}
+
+  equivLeft : (g : Context α) → ctxViewToContext (contextToCtxView g) ≡ g
+  equivLeft ⌈⌉ = refl
+  equivLeft (g , x ∶ ty) = cong (λ g₀ → g₀ , x ∶ ty) (equivLeft g)
+  equivLeft (g , x ≔ u ∶ ty) = cong (λ g₀ → g₀ , x ≔ u ∶ ty) (equivLeft g)
+
+  equivRight : (g : CtxView α) → contextToCtxView (ctxViewToContext g) ≡ g
+  equivRight CtxViewEmpty = refl
+  equivRight (CtxViewExtend g x (Nothing , ty)) = cong (λ g₀ → CtxViewExtend g₀ x (Nothing , ty)) (equivRight g)
+  equivRight (CtxViewExtend g x (Just u , ty)) = cong (λ g₀ → CtxViewExtend g₀ x (Just u , ty)) (equivRight g)
+
+opaque
+  unfolding contextToCtxView
+  equivalenceContext : Equivalence (Context α) (CtxView α)
+  equivalenceContext = Equiv contextToCtxView ctxViewToContext equivLeft equivRight
+  {-# COMPILE AGDA2HS equivalenceContext #-}
+
+rezzScope' : (g : CtxView α) → Rezz α
+rezzScope' CtxViewEmpty = rezz _
+rezzScope' (CtxViewExtend g x _) = rezzCong (λ t → t <> (singleton x)) (rezzScope' g)
+{-# COMPILE AGDA2HS rezzScope' #-}

src/Agda/Core/Name.agda

@@ -97,8 +97,8 @@ instance
     }
 
 -------------------------------------------------------------------------------
-pattern Vsuc n p = ⟨ _ ⟩ (Suc n ⟨ IsSuc p ⟩)
-pattern V2suc n p = ⟨ _ ⟩ (Suc (Suc n) ⟨ IsSuc (IsSuc p) ⟩)
-pattern Vzero = ⟨ _ ⟩ Zero ⟨ IsZero refl ⟩
-pattern Vone = ⟨ _ ⟩ (Suc Zero) ⟨ IsSuc (IsZero refl) ⟩
+pattern Vsuc x n p = ⟨ x ⟩ (Suc n ⟨ IsSuc p ⟩)
+pattern V2suc x n p = ⟨ x ⟩ (Suc (Suc n) ⟨ IsSuc (IsSuc p) ⟩)
+pattern Vzero x = ⟨ x ⟩ Zero ⟨ IsZero refl ⟩
+pattern Vone x = ⟨ x ⟩ (Suc Zero) ⟨ IsSuc (IsZero refl) ⟩
 -------------------------------------------------------------------------------

src/Agda/Core/Tests.agda

@@ -182,12 +182,12 @@ module TestUnifierSwap where
 
   givenfuel = Suc (Suc (Suc (Suc Zero)))
   opaque
-    unfolding ScopeThings swapHighest vec
+    unfolding ScopeThings swapHighest swapTwoLast vec equivalenceContext
 
     @0 testSwapHighestBaseCaseProp : Set
     testSwapHighestBaseCase : testSwapHighestBaseCaseProp
 
-    testSwapHighestBaseCaseProp = (swapHighest {{fl = Zero}} Context-w' w ≡ Just _ )
+    testSwapHighestBaseCaseProp = (swapHighest {{fl = Zero}} Context-w' w ≡ Just (⟨ Scope-v' ▸ "w'" ▸ "w" ⟩ (Context-v' , "w'" ∶ _ , "w" ∶ _ , _)) )
     testSwapHighestBaseCase = refl
 
     @0 testSwapHighest1Prop : Set

src/Agda/Core/Typechecker.agda

@@ -261,7 +261,7 @@ checkLet : ∀ Γ (@0 x : Name)
            → TCM (Γ ⊢ TLet x u v ∶ ty)
 checkLet ctx x u v ty = do
   tu , dtu  ← inferType ctx u
-  dtv       ← checkType (ctx , x ∶ tu) v (weaken (subBindDrop subRefl) ty)
+  dtv       ← checkType (ctx , x ≔ u ∶ tu) v (weaken (subBindDrop subRefl) ty)
   return $ TyLet dtu dtv
 {-# COMPILE AGDA2HS checkLet #-}
 

src/Agda/Core/Typing.agda

@@ -166,7 +166,7 @@ data TyTerm {α} Γ where
 
   TyLet :
     Γ ⊢ u ∶ a
-    → Γ , x ∶ a ⊢ v ∶ weakenType (subBindDrop subRefl) b
+    → Γ , x ≔ u ∶ a ⊢ v ∶ weakenType (subBindDrop subRefl) b
     ----------------------------------------------
     → Γ ⊢ TLet x u v ∶ b
 

src/Agda/Core/Unification.agda

@@ -60,10 +60,13 @@ module Shrinking where
   opaque
     unfolding Scope
     shrinkContext : Context α → ShrinkSubst α β → Context β
-    shrinkContext CtxEmpty RNil = CtxEmpty
-    shrinkContext (CtxExtend Γ x a) (RKeep σ) =
-      CtxExtend (shrinkContext Γ σ) x (subst (ShrinkSubstToSubst σ) a)
-    shrinkContext (CtxExtend Γ x a) (RCons u σ) = shrinkContext Γ σ
+    shrinkContext ⌈⌉ RNil = ⌈⌉
+    shrinkContext (Γ , x ∶ a) (RKeep σ) =
+      shrinkContext Γ σ , x ∶ subst (ShrinkSubstToSubst σ) a
+    shrinkContext (Γ , x ≔ u ∶ a) (RKeep σ) =
+      shrinkContext Γ σ , x ≔ subst (ShrinkSubstToSubst σ) u ∶ subst (ShrinkSubstToSubst σ) a
+    shrinkContext (Γ , _ ∶ _) (RCons u σ) = shrinkContext Γ σ
+    shrinkContext (Γ , _ ≔ _ ∶ _) (RCons u σ) = shrinkContext Γ σ
 
   opaque
     unfolding cut

src/Agda/Core/Unifier.agda

@@ -64,12 +64,16 @@ module Swap where
 
   opaque
     unfolding Scope
-    swapTwoLast : Context (α ▸ x ▸ y) → Maybe (Context (α ▸ y ▸ x))
-    swapTwoLast (CtxExtend (CtxExtend Γ y ay) x ax) = do
-      ax' ← strengthen (subBindDrop subRefl) ax
-      let ay' = weaken (subBindDrop subRefl) ay
-      return ((Γ , x ∶ ax' ) , y ∶ ay')
+    swapTwoLast' : CtxView (α ▸ x ▸ y) → Maybe (CtxView (α ▸ y ▸ x))
+    swapTwoLast' (CtxViewExtend (CtxViewExtend Γ x a) y b) = do
+      b' ← strengthenMaybeLet (subBindDrop subRefl) b
+      let a' = weaken (subBindDrop subRefl) a
+      return (CtxViewExtend (CtxViewExtend Γ y b') x a')
 
+    swapTwoLast : Context (α ▸ x ▸ y) → Maybe (Context (α ▸ y ▸ x))
+    swapTwoLast Γ = do
+      res ← swapTwoLast' (σ equivalenceContext Γ)
+      return (τ equivalenceContext res)
 
     {- Idea of swapHighest (x, z, Γ) y:
         - terminaison condition : you swap x and y or fail
@@ -80,73 +84,72 @@ module Swap where
           recursive call on (z, Γ) and return swapHighest (x, Γ') y
       (recursion terminates because the depth of y in the contexts
       used in recursive calls is decreasing.) -}
-    swapHighest : {{fl : Index}} → Context  (α ▸ x) → ((⟨ y ⟩ yp) : NameIn α)
-      → Maybe (Σ0 _ λ α' → Context α' × Renaming  (α ▸ x) α')
-    swapHighest (CtxExtend (CtxExtend Γ0 y ay) x ax) (⟨ y ⟩ (Zero ⟨ IsZero refl ⟩)) = do
-      Γ' ← swapTwoLast (CtxExtend (CtxExtend Γ0 y ay) x ax)
+    swapHighest' : {{fl : Index}} → CtxView  (α ▸ x) → ((⟨ y ⟩ yp) : NameIn α)
+      → Maybe (Σ0 _ λ α' → CtxView α' × Renaming  (α ▸ x) α')
+    swapHighest' {α = Erased y ∷ α} {x = x} Γ (Vzero y) = do
+      Γ' ← swapTwoLast' Γ
       let σ : Renaming (α ▸ y ▸ x) (α ▸ x ▸ y)
-          σ = renamingExtend (renamingExtend (renamingWeaken (rezz (_ ∷ _ ∷ [])) id) inHere) (inThere inHere)
+          σ = renamingExtend (renamingExtend (renamingWeaken (rezz ([] ▸ x ▸ y)) id) inHere) (inThere inHere)
       return < Γ' , σ >
-    swapHighest {α = Erased z ∷ α}  {x = x} {{Suc fl}} (CtxExtend (CtxExtend Γ0 z az) x ax) (⟨ y ⟩ (Suc value ⟨ IsSuc proof ⟩)) =
-      let Γ : Context (α ▸ z ▸ x)
-          Γ = (CtxExtend (CtxExtend Γ0 z az) x ax)
-          yInα : y ∈ α
+    swapHighest' {α = Erased z ∷ α}  {x = x} {{Suc fl}} Γ@(CtxViewExtend (CtxViewExtend Γ0 z az) x ax) (Vsuc y value proof) =
+      let yInα : y ∈ α
           yInα = value ⟨ proof ⟩ in
       let areTheTwoLastVarsSwapable = do
-        (CtxExtend Γ₁ .z az') ← swapTwoLast Γ
-        ⟨ α₀' ⟩ (Γ₀' , σ₀ ) ← swapHighest {{fl}} Γ₁  < yInα >
+        (CtxViewExtend Γ₁ .z az') ← swapTwoLast' Γ
+        ⟨ α₀' ⟩ (Γ₀' , σ₀ ) ← swapHighest' {{fl}} Γ₁  < yInα >
         -- σ₀ : Renaming  (α ▸ x) α₀'
         let σ : Renaming (α ▸ z ▸ x) (α₀' ▸ z)
             σ = renamingExtend (renamingExtend ((renamingWeakenVar σ₀) ∘ inThere) inHere) (inThere (σ₀ inHere))
-            az' : Type α₀'
-            az' = subst (renamingToSubst (rezzScope Γ₁) σ₀) (weaken (subBindDrop subRefl) az)
-            res1 : Σ0 _ λ α' → Context α' × Renaming (α ▸ z ▸ x) α'
-            res1 = < CtxExtend Γ₀' z az' , σ >
+            az' : MaybeLet α₀'
+            az' = subst (renamingToSubst (rezzScope' Γ₁) σ₀) (weaken (subBindDrop subRefl) az)
+            res1 : Σ0 _ λ α' → CtxView α' × Renaming (α ▸ z ▸ x) α'
+            res1 = < CtxViewExtend Γ₀' z az' , σ >
         return res1 in
       let otherCase = do
-        ⟨ γ₀ ⟩ (Δ₀ , τ₀) ← swapHighest {{fl}} (CtxExtend Γ0 z az) < yInα >
+        ⟨ γ₀ ⟩ (Δ₀ , τ₀) ← swapHighest' {{fl}} (CtxViewExtend Γ0 z az) < yInα >
         -- τ₀ : Renaming (z ◃ α) γ₀
-        let ax' : Type γ₀
-            ax' = subst (renamingToSubst (rezzScope (CtxExtend Γ0 z az)) τ₀) ax
+        let ax' : MaybeLet γ₀
+            ax' = subst (renamingToSubst (rezzScope' (CtxViewExtend Γ0 z az)) τ₀) ax
             σ₁ : Renaming (α ▸ z ▸ x) (γ₀ ▸ x)
             σ₁ = renamingExtend (renamingWeakenVar τ₀) inHere
-        ⟨ α' ⟩ (Γ' , σ₂) ← swapHighest {{fl}} (CtxExtend Δ₀ x ax') < τ₀ (inThere yInα) >
+        ⟨ α' ⟩ (Γ' , σ₂) ← swapHighest' {{fl}} (CtxViewExtend Δ₀ x ax') < τ₀ (inThere yInα) >
         -- σ₂ : Renaming (x ◃ α₀') α'
-        let res2 : Σ0 _ λ α' → Context α' × Renaming (α ▸ z ▸ x) α'
+        let res2 : Σ0 _ λ α' → CtxView α' × Renaming (α ▸ z ▸ x) α'
             res2 = < Γ' , σ₂ ∘ σ₁ >
         return res2 in
       caseMaybe areTheTwoLastVarsSwapable (λ x → Just x) otherCase
-    swapHighest {{Zero}} (CtxExtend (CtxExtend _ _ _) _ _) (⟨ _ ⟩ (Suc _ ⟨ _ ⟩))  = Nothing -- this shouldn't happens as at all times fl ≥ position of y in the scope
+    swapHighest' {{Zero}} (CtxViewExtend (CtxViewExtend _ _ _) _ _) (⟨ _ ⟩ (Suc _ ⟨ _ ⟩))  = Nothing -- this shouldn't happens as at all times fl ≥ position of y in the scope
+
+
+    swapHighest : {{fl : Index}} → Context  (α ▸ x) → ((⟨ y ⟩ yp) : NameIn α)
+      → Maybe (Σ0 _ λ α' → Context α' × Renaming  (α ▸ x) α')
+    swapHighest {{fl = fl}} Γ v = do
+      ⟨ α' ⟩ (res , σ) ← swapHighest' {{ fl = fl }} (σ equivalenceContext Γ) v
+      return (⟨ α' ⟩ (τ equivalenceContext res , σ))
 
     swap : Context α → (x y : NameIn α) → Either SwapError (Maybe (Σ0 _ λ α' → Context α' × Renaming α α'))
-    swap _ Vzero Vzero = Left CantSwapVarWithItSelf
-    swap Γ Vzero (Vsuc value proof) = do
+    swap _ (Vzero _) (Vzero _) = Left CantSwapVarWithItSelf
+    swap Γ (Vzero _) (Vsuc _ value proof) = do
       Right (swapHighest {{value}} Γ < (value ⟨ proof ⟩) >)
-    swap _ (Vsuc _ _) Vzero = Left VarInWrongOrder
-    swap _ Vone Vone = Left CantSwapVarWithItSelf
-    swap _ (V2suc _ _) Vone = Left VarInWrongOrder
-    swap (CtxExtend Γ z az) (Vsuc vx px) (V2suc vy py) = do
-      Just (⟨ α₀' ⟩ (Γ0' , σ₀)) ← swap Γ (⟨ _ ⟩ (vx ⟨ px ⟩)) (⟨ _ ⟩ ((Suc vy) ⟨ IsSuc py ⟩))
+    swap _ (Vsuc _ _ _) (Vzero _) = Left VarInWrongOrder
+    swap _ (Vone _) (Vone _) = Left CantSwapVarWithItSelf
+    swap _ (V2suc _ _ _) (Vone _) = Left VarInWrongOrder
+    swap (Γ , z ∶ az) (Vsuc x vx px) (V2suc y vy py) = do
+      Just (⟨ α₀' ⟩ (Γ0' , σ₀)) ← swap Γ (⟨ x ⟩ (vx ⟨ px ⟩)) (⟨ y ⟩ ((Suc vy) ⟨ IsSuc py ⟩))
+        where Nothing → Right Nothing
+      -- σ₀ : Renaming _ α₀'
+      let τ₀ = renamingToSubst (rezzScope Γ) σ₀
+          σ : Renaming (_ ▸ z) (α₀' ▸ z)
+          σ = renamingExtend (renamingWeakenVar σ₀) inHere
+      Right (Just < Γ0' , z ∶ (subst τ₀ az), σ >)
+    swap (Γ , z ≔ u ∶ az) (Vsuc x vx px) (V2suc y vy py) = do
+      Just (⟨ α₀' ⟩ (Γ0' , σ₀)) ← swap Γ (⟨ x ⟩ (vx ⟨ px ⟩)) (⟨ y ⟩ ((Suc vy) ⟨ IsSuc py ⟩))
         where Nothing → Right Nothing
       -- σ₀ : Renaming _ α₀'
       let τ₀ = renamingToSubst (rezzScope Γ) σ₀
           σ : Renaming (_ ▸ z) (α₀' ▸ z)
           σ = renamingExtend (renamingWeakenVar σ₀) inHere
-      Right (Just < CtxExtend Γ0' z (subst τ₀ az), σ >)
-  {-
-  swapVarListFuel2 : Context α → (x : NameIn α) → (l : List (NameIn α)) → (fl : Nat) → @0 {{lengthNat l ≡ fl}} → Maybe (Σ0 _ λ α' → Context α' × Renaming α α')
-  swapVarListFuel2 Γ (⟨ x ⟩ xp) ((⟨ y ⟩ yp) ∷ l) (suc fl) {{e}} = {!   !} --  do
-    -- ⟨ _ ⟩ (Γ0' , σ₀) ← try_swap Γ (⟨ x ⟩ xp) (⟨ y ⟩ yp)
-    -- let e : lengthNat (map (λ z → < σ₀ (proj₂ z) >) l) ≡ fl
-    --     e = lengthMap ((λ z → < σ₀ (proj₂ z) >)) l
-    -- ⟨ _ ⟩ (Γ' , σ) ← swapVarListFuel2 fl Γ0' (⟨ x ⟩ σ₀ xp) (map (λ z → < σ₀ (proj₂ z) >) l) {{e}}
-    -- return < Γ' , σ ∘ σ₀ >
-    -- where try_swap : Context α → (x y : NameIn α) → Maybe (Σ0 _ λ α' → Context α' × Renaming α α')
-    --       try_swap Γ x y with (swap Γ x y)
-    --       ... | Left CantSwapVarWithItSelf = Nothing
-    --       ... | Left VarInWrongOrder = Just < Γ , id >
-    --       ... | Right val = val
-  swapVarListFuel2 Γ x [] zero = Just < Γ , id > -}
+      Right (Just < Γ0' , z ≔ (subst τ₀ u) ∶ (subst τ₀ az), σ >)
 
   swapVarListFuel : (fl : Nat) → Context α → (x : NameIn α) → (l : List (NameIn α)) → Maybe (Σ0 _ λ α' → Context α' × Renaming α α')
   swapVarListFuel (suc fl) Γ (⟨ x ⟩ xp) ((⟨ y ⟩ yp) ∷ l) = do