1+ open import Scope
2+
3+ open import Haskell.Prelude hiding (All; s; t; a)
4+ open import Haskell.Extra.Erase
5+ open import Haskell.Law.Equality renaming (subst to transport)
6+ open import Haskell.Law.Monoid.Def
7+ open import Haskell.Law.List
8+
9+ open import Agda.Core.Name
10+ open import Agda.Core.GlobalScope using (Globals)
11+ open import Agda.Core.Utils
12+ open import Agda.Core.Syntax
13+ open import Agda.Core.Signature
14+ open import Agda.Core.Substitute
15+ open import Agda.Core.Context
16+ open import Agda.Core.ScopeUtils
17+ open import Agda.Core.TCM
18+ open import Agda.Core.TCMInstances
19+ open import Agda.Core.Unification
20+ open UnificationStepAndStop
21+
22+ module Agda.Core.Unifier
23+ {{@0 globals : Globals}}
24+ {{@0 sig : Signature}}
25+ where
26+
27+ private open module @0 G = Globals globals
28+
29+
30+ ---------------------------------------------------------------------------------------------------
31+ {- PART ONE : Context reordering -}
32+ ---------------------------------------------------------------------------------------------------
33+
34+ module Swap where
35+ private variable
36+ @0 x y : Name
37+ @0 α : Scope Name
38+
39+ data SwapError : Set where
40+ CantSwapVarWithItSelf : SwapError
41+ VarInWrongOrder : SwapError
42+
43+ opaque
44+ unfolding Scope
45+ swapTwoLast : Context (x ◃ y ◃ α) → Maybe (Context (y ◃ x ◃ α))
46+ swapTwoLast (CtxExtend (CtxExtend Γ y ay) x ax) = do
47+ ax' ← strengthen (subBindDrop subRefl) ax
48+ let ay' = weaken (subBindDrop subRefl) ay
49+ return ((Γ , x ∶ ax' ) , y ∶ ay')
50+
51+
52+ {- Idea of swapHighest (x, z, Γ) y:
53+ - terminaison condition : you swap x and y or fail
54+ - case 1: if you can swap the two first vars of (x, z, Γ) then
55+ do it and let Γ1Aux be the result of a recursive call on (x, Γ)
56+ return (z, Γ1Aux)
57+ - case 2: if case 1 fails then let Γ' be the result of the
58+ recursive call on (z, Γ) and return swapHighest (x, Γ') y
59+ (recursion terminates because the depth of y in the contexts
60+ used in recursive calls is decreasing.) -}
61+ swapHighest : {{fl : Fuel}} → Context (x ◃ α) → ((⟨ y ⟩ yp) : NameIn α)
62+ → Maybe (Σ0 _ λ α' → Context α' × Renaming (x ◃ α) α')
63+ swapHighest (CtxExtend (CtxExtend Γ0 y ay) x ax) (⟨ y ⟩ (Zero ⟨ IsZero refl ⟩)) = do
64+ Γ' ← swapTwoLast (CtxExtend (CtxExtend Γ0 y ay) x ax)
65+ let σ : Renaming (x ◃ y ◃ α) (y ◃ x ◃ α)
66+ σ = renamingExtend (renamingExtend (renamingWeaken (rezz (_ ∷ _ ∷ [])) id) inHere) (inThere inHere)
67+ return < Γ' , σ >
68+ swapHighest {x = x} {α = Erased z ∷ α} {{More {{fl}}}} (CtxExtend (CtxExtend Γ0 z az) x ax) (⟨ y ⟩ (Suc value ⟨ IsSuc proof ⟩)) =
69+ let Γ : Context (x ◃ z ◃ α)
70+ Γ = (CtxExtend (CtxExtend Γ0 z az) x ax)
71+ yInα : y ∈ α
72+ yInα = value ⟨ proof ⟩ in
73+ let areTheTwoLastVarsSwapable = do
74+ (CtxExtend Γ₁ .z az') ← swapTwoLast Γ
75+ ⟨ α₀' ⟩ (Γ₀' , σ₀ ) ← swapHighest {{fl}} Γ₁ < yInα >
76+ -- σ₀ : Renaming (x ◃ α) α₀'
77+ let σ : Renaming (x ◃ z ◃ α) (z ◃ α₀')
78+ σ = renamingExtend (renamingExtend ((renamingWeakenVar σ₀) ∘ inThere) inHere) (inThere (σ₀ inHere))
79+ az' : Type α₀'
80+ az' = subst (renamingToSubst (rezzScope Γ₁) σ₀) (weaken (subBindDrop subRefl) az)
81+ res1 : Σ0 _ λ α' → Context α' × Renaming (x ◃ z ◃ α) α'
82+ res1 = < CtxExtend Γ₀' z az' , σ >
83+ return res1 in
84+ let otherCase = do
85+ ⟨ γ₀ ⟩ (Δ₀ , τ₀) ← swapHighest {{More {{fl}}}} (CtxExtend Γ0 z az) < yInα >
86+ -- τ₀ : Renaming (z ◃ α) γ₀
87+ let ax' : Type γ₀
88+ ax' = subst (renamingToSubst (rezzScope (CtxExtend Γ0 z az)) τ₀) ax
89+ σ₁ : Renaming (x ◃ z ◃ α) (x ◃ γ₀)
90+ σ₁ = renamingExtend (renamingWeakenVar τ₀) inHere
91+ ⟨ α' ⟩ (Γ' , σ₂) ← swapHighest {{fl}} (CtxExtend Δ₀ x ax') < τ₀ (inThere yInα) >
92+ -- σ₂ : Renaming (x ◃ α₀') α'
93+ let res2 : Σ0 _ λ α' → Context α' × Renaming (x ◃ z ◃ α) α'
94+ res2 = < Γ' , σ₂ ∘ σ₁ >
95+ return res2 in
96+ caseMaybe areTheTwoLastVarsSwapable (λ x → Just x) otherCase
97+ swapHighest {{None}} (CtxExtend (CtxExtend _ _ _) _ _) (⟨ _ ⟩ (Suc _ ⟨ _ ⟩)) = Nothing
98+
99+
100+ swap : Context α → (x y : NameIn α) → Either SwapError (Maybe (Σ0 _ λ α' → Context α' × Renaming α α'))
101+ swap _ (⟨ x ⟩ (Zero ⟨ _ ⟩)) (⟨ y ⟩ (Zero ⟨ _ ⟩)) =
102+ Left CantSwapVarWithItSelf
103+ swap Γ (⟨ x ⟩ (Zero ⟨ IsZero refl ⟩)) (⟨ y ⟩ (Suc value ⟨ IsSuc proof ⟩)) = do
104+ Right (swapHighest {{None}} Γ (⟨ y ⟩ (value ⟨ proof ⟩)))
105+ swap _ (⟨ x ⟩ (Suc vx ⟨ px ⟩)) (⟨ y ⟩ (Zero ⟨ IsZero refl ⟩)) =
106+ Left VarInWrongOrder
107+ swap _ (⟨ x ⟩ (Suc Zero ⟨ _ ⟩)) (⟨ y ⟩ (Suc Zero ⟨ _ ⟩)) =
108+ Left CantSwapVarWithItSelf
109+ swap _ (⟨ x ⟩ (Suc (Suc _) ⟨ _ ⟩)) (⟨ y ⟩ (Suc Zero ⟨ _ ⟩)) =
110+ Left VarInWrongOrder
111+ swap (CtxExtend Γ z az) (⟨ x ⟩ (Suc vx ⟨ IsSuc px ⟩)) (⟨ y ⟩ (Suc (Suc vy) ⟨ IsSuc (IsSuc py) ⟩)) = do
112+ Just (⟨ α₀' ⟩ (Γ0' , σ₀)) ← swap Γ (⟨ x ⟩ (vx ⟨ px ⟩)) (⟨ y ⟩ ((Suc vy) ⟨ IsSuc py ⟩))
113+ where Nothing → Right Nothing
114+ -- σ₀ : Renaming _ α₀'
115+ let τ₀ = renamingToSubst (rezzScope Γ) σ₀
116+ σ : Renaming (z ◃ _) (z ◃ α₀')
117+ σ = renamingExtend (renamingWeakenVar σ₀) inHere
118+ Right (Just < CtxExtend Γ0' z (subst τ₀ az), σ >)
119+ {-
120+ swapVarListFuel2 : (@0 fl : Nat) → Context α → (x : NameIn α) → (l : List (NameIn α)) → @0 {{lengthNat l ≡ fl}} → Maybe (Σ0 _ λ α' → Context α' × Renaming α α')
121+ swapVarListFuel2 (suc fl) Γ (⟨ x ⟩ xp) ((⟨ y ⟩ yp) ∷ l) {{refl}} = do
122+ ⟨ _ ⟩ (Γ0' , σ₀) ← try_swap Γ (⟨ x ⟩ xp) (⟨ y ⟩ yp)
123+ let e : lengthNat (map (λ z → < σ₀ (proj₂ z) >) l) ≡ fl
124+ e = lengthMap ((λ z → < σ₀ (proj₂ z) >)) l
125+ ⟨ _ ⟩ (Γ' , σ) ← swapVarListFuel2 fl Γ0' (⟨ x ⟩ σ₀ xp) (map (λ z → < σ₀ (proj₂ z) >) l) {{e}}
126+ return < Γ' , σ ∘ σ₀ >
127+ where try_swap : Context α → (x y : NameIn α) → Maybe (Σ0 _ λ α' → Context α' × Renaming α α')
128+ try_swap Γ x y with (swap Γ x y)
129+ ... | Left CantSwapVarWithItSelf = Nothing
130+ ... | Left VarInWrongOrder = Just < Γ , id >
131+ ... | Right val = val
132+ swapVarListFuel2 zero Γ x [] {{refl}} = Just < Γ , id > -}
133+
134+ swapVarListFuel : (fl : Nat) → Context α → (x : NameIn α) → (l : List (NameIn α)) → Maybe (Σ0 _ λ α' → Context α' × Renaming α α')
135+ swapVarListFuel (suc fl) Γ (⟨ x ⟩ xp) ((⟨ y ⟩ yp) ∷ l) = do
136+ ⟨ _ ⟩ (Γ0' , σ₀) ← try_swap Γ (⟨ x ⟩ xp) (⟨ y ⟩ yp)
137+ ⟨ _ ⟩ (Γ' , σ) ← swapVarListFuel fl Γ0' (⟨ x ⟩ σ₀ xp) (map (λ z → < σ₀ (proj₂ z) >) l)
138+ return < Γ' , σ ∘ σ₀ >
139+ where try_swap : Context α → (x y : NameIn α) → Maybe (Σ0 _ λ α' → Context α' × Renaming α α')
140+ try_swap Γ x y with (swap Γ x y)
141+ ... | Left CantSwapVarWithItSelf = Nothing
142+ ... | Left VarInWrongOrder = Just < Γ , id >
143+ ... | Right val = val
144+ swapVarListFuel zero Γ x [] = Just < Γ , id >
145+ swapVarListFuel _ _ _ _ = Nothing
146+
147+ swapVarList : Context α → (x : NameIn α) → List (NameIn α) → Maybe (Σ0 _ λ α' → Context α' × Renaming α α')
148+ swapVarList Γ x l = swapVarListFuel (lengthNat l) Γ x l
149+
150+ swapVarTerm : (Γ : Context α) → ((⟨ x ⟩ xp) : NameIn α) → (u : Term α)
151+ → Maybe (Σ0 _ λ α' → Context α' × Renaming α α')
152+ swapVarTerm Γ x u = swapVarList Γ x (varInTerm u)
153+
154+ opaque
155+ swapVarTermStrengthened : (Γ : Context α) → ((⟨ x ⟩ xp) : NameIn α) → (u : Term α)
156+ → Maybe (Σ0 _ λ α' → Context α' × (Σ[ σ ∈ Renaming α α' ]
157+ (Σ[ u₀ ∈ Term (cutDrop (σ xp)) ] Strengthened (subst (renamingToSubst (rezzScope Γ) σ) u) u₀)))
158+ swapVarTermStrengthened Γ (⟨ x ⟩ xp) u =
159+ caseMaybe (swapVarTerm Γ (⟨ x ⟩ xp) u)
160+ (λ (⟨ α' ⟩ (Γ' , σ)) →
161+ let u' : Term α'
162+ u' = subst (renamingToSubst (rezzScope Γ) σ) u in
163+ caseMaybe (strengthen subCutDrop u')
164+ (λ u₀ {{e}} → Just (⟨ α' ⟩ (Γ' , (σ , (u₀ , (subCutDrop ⟨ e ⟩))))))
165+ Nothing)
166+ Nothing
167+
168+ {- End of module Swap -}
169+ open Swap
170+
0 commit comments