open import Common.Types
module Common.CoercionPrecision where
open import Data.Nat
open import Data.Unit using (⊤; tt)
open import Data.Bool using (true; false) renaming (Bool to 𝔹)
open import Data.List
open import Data.Product using (_×_; ∃-syntax; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Maybe
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; subst; subst₂; sym)
open import Function using (case_of_)
open import Syntax hiding (_⨟_; ↑)
open import Common.Utils
open import Common.Coercions
open import CoercionExpr.CoercionExpr
open import CoercionExpr.Stamping
open import CoercionExpr.Precision
renaming (prec→⊑ to cexpr-prec→⊑; ⊢l_⊑_ to ⊢ₗ_⊑_; ⊢r_⊑_ to ⊢ᵣ_⊑_)
open import CoercionExpr.SyntacComp renaming (_⨟_ to _⊹⊹_)
infix 4 ⟨_⟩⊑⟨_⟩
infix 4 ⟨_⟩⊑_
infix 4 _⊑⟨_⟩
data ⟨_⟩⊑⟨_⟩ : ∀ {A A′ B B′} → Cast A ⇒ B → Cast A′ ⇒ B′ → Set where
⊑-base : ∀ {ι g₁ g₁′ g₂ g₂′} {c̅ : CExpr g₁ ⇒ g₂} {c̅′ : CExpr g₁′ ⇒ g₂′}
→ ⊢ c̅ ⊑ c̅′
→ ⟨ cast (Castᵣ_⇒_.id ι) c̅ ⟩⊑⟨ cast (Castᵣ_⇒_.id ι) c̅′ ⟩
⊑-ref : ∀ {A A′ B B′ g₁ g₁′ g₂ g₂′} {c : Cast B ⇒ A} {c′ : Cast B′ ⇒ A′}
{d : Cast A ⇒ B} {d′ : Cast A′ ⇒ B′}
{c̅ : CExpr g₁ ⇒ g₂} {c̅′ : CExpr g₁′ ⇒ g₂′}
→ ⟨ c ⟩⊑⟨ c′ ⟩
→ ⟨ d ⟩⊑⟨ d′ ⟩
→ ⊢ c̅ ⊑ c̅′
→ ⟨ cast (ref c d) c̅ ⟩⊑⟨ cast (ref c′ d′) c̅′ ⟩
⊑-fun : ∀ {A A′ B B′ C C′ D D′ gc₁ gc₁′ gc₂ gc₂′ g₁ g₁′ g₂ g₂′}
{c : Cast C ⇒ A} {c′ : Cast C′ ⇒ A′}
{d : Cast B ⇒ D} {d′ : Cast B′ ⇒ D′}
{d̅ : CExpr gc₂ ⇒ gc₁} {d̅′ : CExpr gc₂′ ⇒ gc₁′}
{c̅ : CExpr g₁ ⇒ g₂} {c̅′ : CExpr g₁′ ⇒ g₂′}
→ ⊢ d̅ ⊑ d̅′
→ ⟨ c ⟩⊑⟨ c′ ⟩
→ ⟨ d ⟩⊑⟨ d′ ⟩
→ ⊢ c̅ ⊑ c̅′
→ ⟨ cast (fun d̅ c d) c̅ ⟩⊑⟨ cast (fun d̅′ c′ d′) c̅′ ⟩
data ⟨_⟩⊑_ : ∀ {A B} → Cast A ⇒ B → (A′ : Type) → Set where
⊑-base : ∀ {ι g₁ g₂ g′} {c̅ : CExpr g₁ ⇒ g₂}
→ ⊢ₗ c̅ ⊑ g′
→ ⟨ cast (Castᵣ_⇒_.id ι) c̅ ⟩⊑ ` ι of g′
⊑-ref : ∀ {A A′ B g₁ g₂ g′} {c : Cast B ⇒ A} {d : Cast A ⇒ B}
{c̅ : CExpr g₁ ⇒ g₂}
→ ⟨ c ⟩⊑ A′
→ ⟨ d ⟩⊑ A′
→ ⊢ₗ c̅ ⊑ g′
→ ⟨ cast (ref c d) c̅ ⟩⊑ Ref A′ of g′
⊑-fun : ∀ {A A′ B B′ C D gc₁ gc₂ gc′ g₁ g₂ g′}
{c : Cast C ⇒ A} {d : Cast B ⇒ D}
{d̅ : CExpr gc₂ ⇒ gc₁} {c̅ : CExpr g₁ ⇒ g₂}
→ ⊢ₗ d̅ ⊑ gc′
→ ⟨ c ⟩⊑ A′
→ ⟨ d ⟩⊑ B′
→ ⊢ₗ c̅ ⊑ g′
→ ⟨ cast (fun d̅ c d) c̅ ⟩⊑ ⟦ gc′ ⟧ A′ ⇒ B′ of g′
data _⊑⟨_⟩ : ∀ {A′ B′} → (A : Type) → Cast A′ ⇒ B′ → Set where
⊑-base : ∀ {ι g g₁′ g₂′} {c̅′ : CExpr g₁′ ⇒ g₂′}
→ ⊢ᵣ g ⊑ c̅′
→ ` ι of g ⊑⟨ cast (Castᵣ_⇒_.id ι) c̅′ ⟩
⊑-ref : ∀ {A A′ B′ g g₁′ g₂′} {c′ : Cast B′ ⇒ A′} {d′ : Cast A′ ⇒ B′}
{c̅′ : CExpr g₁′ ⇒ g₂′}
→ A ⊑⟨ c′ ⟩
→ A ⊑⟨ d′ ⟩
→ ⊢ᵣ g ⊑ c̅′
→ Ref A of g ⊑⟨ cast (ref c′ d′) c̅′ ⟩
⊑-fun : ∀ {A A′ B B′ C′ D′ gc gc₁′ gc₂′ g g₁′ g₂′}
{c′ : Cast C′ ⇒ A′} {d′ : Cast B′ ⇒ D′}
{d̅′ : CExpr gc₂′ ⇒ gc₁′} {c̅′ : CExpr g₁′ ⇒ g₂′}
→ ⊢ᵣ gc ⊑ d̅′
→ A ⊑⟨ c′ ⟩
→ B ⊑⟨ d′ ⟩
→ ⊢ᵣ g ⊑ c̅′
→ ⟦ gc ⟧ A ⇒ B of g ⊑⟨ cast (fun d̅′ c′ d′) c̅′ ⟩
coercion-prec→⊑ : ∀ {A A′ B B′} {c : Cast A ⇒ B} {d : Cast A′ ⇒ B′}
→ ⟨ c ⟩⊑⟨ d ⟩
→ A ⊑ A′ × B ⊑ B′
coercion-prec→⊑ (⊑-base c̅⊑c̅′) =
let ⟨ g₁⊑g₁′ , g₂⊑g₂′ ⟩ = cexpr-prec→⊑ _ _ c̅⊑c̅′ in
⟨ ⊑-ty g₁⊑g₁′ ⊑-ι , ⊑-ty g₂⊑g₂′ ⊑-ι ⟩
coercion-prec→⊑ (⊑-ref c⊑c′ d⊑d′ c̅⊑c̅′) =
let ⟨ g₁⊑g₁′ , g₂⊑g₂′ ⟩ = cexpr-prec→⊑ _ _ c̅⊑c̅′ in
let ⟨ B⊑B′ , A⊑A′ ⟩ = coercion-prec→⊑ c⊑c′ in
⟨ ⊑-ty g₁⊑g₁′ (⊑-ref A⊑A′) , ⊑-ty g₂⊑g₂′ (⊑-ref B⊑B′) ⟩
coercion-prec→⊑ (⊑-fun d̅⊑d̅′ c⊑c′ d⊑d′ c̅⊑c̅′) =
let ⟨ g₁⊑g₁′ , g₂⊑g₂′ ⟩ = cexpr-prec→⊑ _ _ c̅⊑c̅′ in
let ⟨ gc₂⊑gc₂′ , gc₁⊑gc₁′ ⟩ = cexpr-prec→⊑ _ _ d̅⊑d̅′ in
let ⟨ C⊑C′ , A⊑A′ ⟩ = coercion-prec→⊑ c⊑c′ in
let ⟨ B⊑B′ , D⊑D′ ⟩ = coercion-prec→⊑ d⊑d′ in
⟨ ⊑-ty g₁⊑g₁′ (⊑-fun gc₁⊑gc₁′ A⊑A′ B⊑B′) , ⊑-ty g₂⊑g₂′ (⊑-fun gc₂⊑gc₂′ C⊑C′ D⊑D′) ⟩
coercion-prec-left→⊑ : ∀ {A A′ B} {c : Cast A ⇒ B}
→ ⟨ c ⟩⊑ A′
→ A ⊑ A′ × B ⊑ A′
coercion-prec-left→⊑ (⊑-base c̅⊑g′) =
let ⟨ g₁⊑g′ , g₂⊑g′ ⟩ = prec-left→⊑ _ c̅⊑g′ in
⟨ ⊑-ty g₁⊑g′ ⊑-ι , ⊑-ty g₂⊑g′ ⊑-ι ⟩
coercion-prec-left→⊑ (⊑-ref c⊑A′ d⊑A′ c̅⊑g′) =
let ⟨ g₁⊑g′ , g₂⊑g′ ⟩ = prec-left→⊑ _ c̅⊑g′ in
let ⟨ B⊑A′ , A⊑A′ ⟩ = coercion-prec-left→⊑ c⊑A′ in
⟨ ⊑-ty g₁⊑g′ (⊑-ref A⊑A′) , ⊑-ty g₂⊑g′ (⊑-ref B⊑A′) ⟩
coercion-prec-left→⊑ (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ c̅⊑g′) =
let ⟨ g₁⊑g′ , g₂⊑g′ ⟩ = prec-left→⊑ _ c̅⊑g′ in
let ⟨ gc₂⊑gc′ , gc₁⊑gc′ ⟩ = prec-left→⊑ _ d̅⊑gc′ in
let ⟨ C⊑A′ , A⊑A′ ⟩ = coercion-prec-left→⊑ c⊑A′ in
let ⟨ B⊑B′ , D⊑B′ ⟩ = coercion-prec-left→⊑ d⊑B′ in
⟨ ⊑-ty g₁⊑g′ (⊑-fun gc₁⊑gc′ A⊑A′ B⊑B′) , ⊑-ty g₂⊑g′ (⊑-fun gc₂⊑gc′ C⊑A′ D⊑B′) ⟩
coercion-prec-right→⊑ : ∀ {A A′ B′} {c : Cast A′ ⇒ B′}
→ A ⊑⟨ c ⟩
→ A ⊑ A′ × A ⊑ B′
coercion-prec-right→⊑ (⊑-base g⊑c̅′) =
let ⟨ g⊑g₁′ , g⊑g₂′ ⟩ = prec-right→⊑ _ g⊑c̅′ in
⟨ ⊑-ty g⊑g₁′ ⊑-ι , ⊑-ty g⊑g₂′ ⊑-ι ⟩
coercion-prec-right→⊑ (⊑-ref A⊑c′ A⊑d′ g⊑c̅′) =
let ⟨ g⊑g₁′ , g⊑g₂′ ⟩ = prec-right→⊑ _ g⊑c̅′ in
let ⟨ A⊑B′ , A⊑A′ ⟩ = coercion-prec-right→⊑ A⊑c′ in
⟨ ⊑-ty g⊑g₁′ (⊑-ref A⊑A′) , ⊑-ty g⊑g₂′ (⊑-ref A⊑B′) ⟩
coercion-prec-right→⊑ (⊑-fun gc⊑d̅′ A⊑c′ B⊑d′ g⊑c̅′) =
let ⟨ g⊑g₁′ , g⊑g₂′ ⟩ = prec-right→⊑ _ g⊑c̅′ in
let ⟨ gc⊑gc₂′ , gc⊑gc₁′ ⟩ = prec-right→⊑ _ gc⊑d̅′ in
let ⟨ A⊑C′ , A⊑A′ ⟩ = coercion-prec-right→⊑ A⊑c′ in
let ⟨ B⊑B′ , B⊑D′ ⟩ = coercion-prec-right→⊑ B⊑d′ in
⟨ ⊑-ty g⊑g₁′ (⊑-fun gc⊑gc₁′ A⊑A′ B⊑B′) , ⊑-ty g⊑g₂′ (⊑-fun gc⊑gc₂′ A⊑C′ B⊑D′) ⟩
comp-pres-prec : ∀ {A A′ B B′ C C′} {c : Cast A ⇒ B} {d : Cast B ⇒ C}
{c′ : Cast A′ ⇒ B′} {d′ : Cast B′ ⇒ C′}
→ ⟨ c ⟩⊑⟨ c′ ⟩
→ ⟨ d ⟩⊑⟨ d′ ⟩
→ ⟨ c ⨟ d ⟩⊑⟨ c′ ⨟ d′ ⟩
comp-pres-prec (⊑-base c̅⊑c̅′) (⊑-base d̅⊑d̅′) = ⊑-base (comp-pres-⊑ c̅⊑c̅′ d̅⊑d̅′)
comp-pres-prec (⊑-ref c⊑c′ d⊑d′ c̅⊑c̅′) (⊑-ref c⊑A′ d⊑A′ c̅⊑g′) =
⊑-ref (comp-pres-prec c⊑A′ c⊑c′) (comp-pres-prec d⊑d′ d⊑A′)
(comp-pres-⊑ c̅⊑c̅′ c̅⊑g′)
comp-pres-prec (⊑-fun d̅⊑d̅′ c⊑c′ d⊑d′ c̅⊑c̅′) (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ c̅⊑g′) =
⊑-fun (comp-pres-⊑ d̅⊑gc′ d̅⊑d̅′) (comp-pres-prec c⊑A′ c⊑c′)
(comp-pres-prec d⊑d′ d⊑B′) (comp-pres-⊑ c̅⊑c̅′ c̅⊑g′)
comp-pres-prec-ll : ∀ {A A′ B C} {c : Cast A ⇒ B} {d : Cast B ⇒ C}
→ ⟨ c ⟩⊑ A′
→ ⟨ d ⟩⊑ A′
→ ⟨ c ⨟ d ⟩⊑ A′
comp-pres-prec-ll (⊑-base c̅⊑g′) (⊑-base d̅⊑g′) = ⊑-base (comp-pres-⊑-ll c̅⊑g′ d̅⊑g′)
comp-pres-prec-ll (⊑-ref c₁⊑A′ d₁⊑A′ c̅⊑g′) (⊑-ref c₂⊑A′ d₂⊑A′ d̅⊑g′) =
⊑-ref (comp-pres-prec-ll c₂⊑A′ c₁⊑A′) (comp-pres-prec-ll d₁⊑A′ d₂⊑A′)
(comp-pres-⊑-ll c̅⊑g′ d̅⊑g′)
comp-pres-prec-ll (⊑-fun d̅₁⊑gc′ c₁⊑A′ d₁⊑B′ c̅₁⊑g′) (⊑-fun d̅₂⊑gc′ c₂⊑A′ d₂⊑B′ c̅₂⊑g′) =
⊑-fun (comp-pres-⊑-ll d̅₂⊑gc′ d̅₁⊑gc′) (comp-pres-prec-ll c₂⊑A′ c₁⊑A′)
(comp-pres-prec-ll d₁⊑B′ d₂⊑B′) (comp-pres-⊑-ll c̅₁⊑g′ c̅₂⊑g′)
comp-pres-prec-rr : ∀ {A A′ B′ C′} {c : Cast A′ ⇒ B′} {d : Cast B′ ⇒ C′}
→ A ⊑⟨ c ⟩
→ A ⊑⟨ d ⟩
→ A ⊑⟨ c ⨟ d ⟩
comp-pres-prec-rr (⊑-base c̅⊑g′) (⊑-base d̅⊑g′) = ⊑-base (comp-pres-⊑-rr c̅⊑g′ d̅⊑g′)
comp-pres-prec-rr (⊑-ref c₁⊑A′ d₁⊑A′ c̅⊑g′) (⊑-ref c₂⊑A′ d₂⊑A′ d̅⊑g′) =
⊑-ref (comp-pres-prec-rr c₂⊑A′ c₁⊑A′) (comp-pres-prec-rr d₁⊑A′ d₂⊑A′)
(comp-pres-⊑-rr c̅⊑g′ d̅⊑g′)
comp-pres-prec-rr (⊑-fun d̅₁⊑gc′ c₁⊑A′ d₁⊑B′ c̅₁⊑g′) (⊑-fun d̅₂⊑gc′ c₂⊑A′ d₂⊑B′ c̅₂⊑g′) =
⊑-fun (comp-pres-⊑-rr d̅₂⊑gc′ d̅₁⊑gc′) (comp-pres-prec-rr c₂⊑A′ c₁⊑A′)
(comp-pres-prec-rr d₁⊑B′ d₂⊑B′) (comp-pres-⊑-rr c̅₁⊑g′ c̅₂⊑g′)
comp-pres-prec-bl : ∀ {A A′ B B′ C} {c : Cast A ⇒ B} {d : Cast B ⇒ C}
{c′ : Cast A′ ⇒ B′}
→ ⟨ c ⟩⊑⟨ c′ ⟩
→ ⟨ d ⟩⊑ B′
→ ⟨ c ⨟ d ⟩⊑⟨ c′ ⟩
comp-pres-prec-lb : ∀ {A A′ B B′ C} {c : Cast A ⇒ B} {d : Cast B ⇒ C}
{c′ : Cast A′ ⇒ B′}
→ ⟨ c ⟩⊑ A′
→ ⟨ d ⟩⊑⟨ c′ ⟩
→ ⟨ c ⨟ d ⟩⊑⟨ c′ ⟩
comp-pres-prec-bl (⊑-base c̅⊑c̅′) (⊑-base d̅⊑g′) = ⊑-base (comp-pres-⊑-bl c̅⊑c̅′ d̅⊑g′)
comp-pres-prec-bl (⊑-ref c⊑c′ d⊑d′ c̅⊑c̅′) (⊑-ref c⊑A′ d⊑A′ c̅⊑g′) =
⊑-ref (comp-pres-prec-lb c⊑A′ c⊑c′) (comp-pres-prec-bl d⊑d′ d⊑A′)
(comp-pres-⊑-bl c̅⊑c̅′ c̅⊑g′)
comp-pres-prec-bl (⊑-fun d̅⊑d̅′ c⊑c′ d⊑d′ c̅⊑c̅′) (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ c̅⊑g′) =
⊑-fun (comp-pres-⊑-lb d̅⊑gc′ d̅⊑d̅′) (comp-pres-prec-lb c⊑A′ c⊑c′)
(comp-pres-prec-bl d⊑d′ d⊑B′) (comp-pres-⊑-bl c̅⊑c̅′ c̅⊑g′)
comp-pres-prec-lb (⊑-base d̅⊑g′) (⊑-base c̅⊑c̅′) = ⊑-base (comp-pres-⊑-lb d̅⊑g′ c̅⊑c̅′)
comp-pres-prec-lb (⊑-ref c⊑A′ d⊑A′ c̅⊑g′) (⊑-ref c⊑c′ d⊑d′ c̅⊑c̅′) =
⊑-ref (comp-pres-prec-bl c⊑c′ c⊑A′) (comp-pres-prec-lb d⊑A′ d⊑d′)
(comp-pres-⊑-lb c̅⊑g′ c̅⊑c̅′)
comp-pres-prec-lb (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ c̅⊑g′) (⊑-fun d̅⊑d̅′ c⊑c′ d⊑d′ c̅⊑c̅′) =
⊑-fun (comp-pres-⊑-bl d̅⊑d̅′ d̅⊑gc′) (comp-pres-prec-bl c⊑c′ c⊑A′)
(comp-pres-prec-lb d⊑B′ d⊑d′) (comp-pres-⊑-lb c̅⊑g′ c̅⊑c̅′)
comp-pres-prec-br : ∀ {A A′ B B′ C′} {c : Cast A ⇒ B}
{c′ : Cast A′ ⇒ B′} {d′ : Cast B′ ⇒ C′}
→ ⟨ c ⟩⊑⟨ c′ ⟩
→ B ⊑⟨ d′ ⟩
→ ⟨ c ⟩⊑⟨ c′ ⨟ d′ ⟩
comp-pres-prec-rb : ∀ {A A′ B B′ C′} {c : Cast A ⇒ B}
{c′ : Cast A′ ⇒ B′} {d′ : Cast B′ ⇒ C′}
→ A ⊑⟨ c′ ⟩
→ ⟨ c ⟩⊑⟨ d′ ⟩
→ ⟨ c ⟩⊑⟨ c′ ⨟ d′ ⟩
comp-pres-prec-br (⊑-base x) (⊑-base x′) = ⊑-base (comp-pres-⊑-br x x′)
comp-pres-prec-br (⊑-ref x y z) (⊑-ref x′ y′ z′) =
⊑-ref (comp-pres-prec-rb x′ x) (comp-pres-prec-br y y′)
(comp-pres-⊑-br z z′)
comp-pres-prec-br (⊑-fun x y z w) (⊑-fun x′ y′ z′ w′) =
⊑-fun (comp-pres-⊑-rb x′ x) (comp-pres-prec-rb y′ y)
(comp-pres-prec-br z z′) (comp-pres-⊑-br w w′)
comp-pres-prec-rb (⊑-base x) (⊑-base x′) = ⊑-base (comp-pres-⊑-rb x x′)
comp-pres-prec-rb (⊑-ref x y z) (⊑-ref x′ y′ z′) =
⊑-ref (comp-pres-prec-br x′ x) (comp-pres-prec-rb y y′)
(comp-pres-⊑-rb z z′)
comp-pres-prec-rb (⊑-fun x y z w) (⊑-fun x′ y′ z′ w′) =
⊑-fun (comp-pres-⊑-br x′ x) (comp-pres-prec-br y′ y)
(comp-pres-prec-rb z z′) (comp-pres-⊑-rb w w′)
comp-pres-prec-rl : ∀ {A A′ B B′} {c : Cast A ⇒ B} {c′ : Cast A′ ⇒ B′}
→ A ⊑⟨ c′ ⟩
→ ⟨ c ⟩⊑ B′
→ ⟨ c ⟩⊑⟨ c′ ⟩
comp-pres-prec-lr : ∀ {A A′ B B′} {c : Cast A ⇒ B} {c′ : Cast A′ ⇒ B′}
→ ⟨ c ⟩⊑ A′
→ B ⊑⟨ c′ ⟩
→ ⟨ c ⟩⊑⟨ c′ ⟩
comp-pres-prec-rl (⊑-base g⊑c̅′) (⊑-base c̅⊑g′) = ⊑-base (comp-pres-⊑-rl g⊑c̅′ c̅⊑g′)
comp-pres-prec-rl (⊑-ref A⊑c′ A⊑d′ g⊑c̅′) (⊑-ref c⊑A′ d⊑A′ c̅⊑g′) =
⊑-ref (comp-pres-prec-lr c⊑A′ A⊑c′) (comp-pres-prec-rl A⊑d′ d⊑A′)
(comp-pres-⊑-rl g⊑c̅′ c̅⊑g′)
comp-pres-prec-rl (⊑-fun gc⊑d̅′ A⊑c′ B⊑d′ g⊑c̅′) (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ c̅⊑g′) =
⊑-fun (comp-pres-⊑-lr d̅⊑gc′ gc⊑d̅′) (comp-pres-prec-lr c⊑A′ A⊑c′)
(comp-pres-prec-rl B⊑d′ d⊑B′) (comp-pres-⊑-rl g⊑c̅′ c̅⊑g′)
comp-pres-prec-lr (⊑-base c̅⊑g′) (⊑-base g⊑c̅′) = ⊑-base (comp-pres-⊑-lr c̅⊑g′ g⊑c̅′)
comp-pres-prec-lr (⊑-ref c⊑A′ d⊑A′ c̅⊑g′) (⊑-ref A⊑c′ A⊑d′ g⊑c̅′) =
⊑-ref (comp-pres-prec-rl A⊑c′ c⊑A′) (comp-pres-prec-lr d⊑A′ A⊑d′)
(comp-pres-⊑-lr c̅⊑g′ g⊑c̅′)
comp-pres-prec-lr (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ c̅⊑g′) (⊑-fun gc⊑d̅′ A⊑c′ B⊑d′ g⊑c̅′) =
⊑-fun (comp-pres-⊑-rl gc⊑d̅′ d̅⊑gc′) (comp-pres-prec-rl A⊑c′ c⊑A′)
(comp-pres-prec-lr d⊑B′ B⊑d′) (comp-pres-⊑-lr c̅⊑g′ g⊑c̅′)
prec-coerce-id : ∀ {A A′}
→ A ⊑ A′
→ ⟨ coerce-id A ⟩⊑⟨ coerce-id A′ ⟩
prec-coerce-id (⊑-ty g₁⊑g₂ ⊑-ι) = ⊑-base (⊑-id g₁⊑g₂)
prec-coerce-id (⊑-ty g₁⊑g₂ (⊑-ref A⊑B)) =
⊑-ref (prec-coerce-id A⊑B) (prec-coerce-id A⊑B) (⊑-id g₁⊑g₂)
prec-coerce-id (⊑-ty x (⊑-fun x₁ x₂ x₃)) =
⊑-fun (⊑-id x₁) (prec-coerce-id x₂) (prec-coerce-id x₃) (⊑-id x)
prec-coerce-id-left : ∀ {A A′}
→ A ⊑ A′
→ ⟨ coerce-id A ⟩⊑ A′
prec-coerce-id-left (⊑-ty g₁⊑g₂ ⊑-ι) = ⊑-base (⊑-id g₁⊑g₂)
prec-coerce-id-left (⊑-ty g₁⊑g₂ (⊑-ref A⊑B)) =
⊑-ref (prec-coerce-id-left A⊑B) (prec-coerce-id-left A⊑B) (⊑-id g₁⊑g₂)
prec-coerce-id-left (⊑-ty x (⊑-fun x₁ x₂ x₃)) =
⊑-fun (⊑-id x₁) (prec-coerce-id-left x₂) (prec-coerce-id-left x₃) (⊑-id x)
prec-left-coerce-id : ∀ {A A′ B} {c : Cast A ⇒ B}
→ ⟨ c ⟩⊑ A′
→ ⟨ c ⟩⊑⟨ coerce-id A′ ⟩
prec-left-coerce-id (⊑-base c̅⊑g′) = ⊑-base (⊑-left-expand c̅⊑g′)
prec-left-coerce-id (⊑-ref c⊑A′ d⊑A′ c̅⊑g′) =
⊑-ref (prec-left-coerce-id c⊑A′) (prec-left-coerce-id d⊑A′) (⊑-left-expand c̅⊑g′)
prec-left-coerce-id (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ c̅⊑g′) =
⊑-fun (⊑-left-expand d̅⊑gc′) (prec-left-coerce-id c⊑A′) (prec-left-coerce-id d⊑B′) (⊑-left-expand c̅⊑g′)
prec-right-coerce-id : ∀ {A A′ B′} {c′ : Cast A′ ⇒ B′}
→ A ⊑⟨ c′ ⟩
→ ⟨ coerce-id A ⟩⊑⟨ c′ ⟩
prec-right-coerce-id (⊑-base c̅⊑g′) = ⊑-base (⊑-right-expand c̅⊑g′)
prec-right-coerce-id (⊑-ref c⊑A′ d⊑A′ c̅⊑g′) =
⊑-ref (prec-right-coerce-id c⊑A′) (prec-right-coerce-id d⊑A′) (⊑-right-expand c̅⊑g′)
prec-right-coerce-id (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ c̅⊑g′) =
⊑-fun (⊑-right-expand d̅⊑gc′) (prec-right-coerce-id c⊑A′) (prec-right-coerce-id d⊑B′) (⊑-right-expand c̅⊑g′)
stamp-ir-prec : ∀ {A A′ B B′} {c : Cast A ⇒ B} {c′ : Cast A′ ⇒ B′} {ℓ}
→ ⟨ c ⟩⊑⟨ c′ ⟩
→ (i : Irreducible c )
→ (i′ : Irreducible c′)
→ ⟨ stamp-ir c i ℓ ⟩⊑⟨ stamp-ir c′ i′ ℓ ⟩
stamp-ir-prec (⊑-base c̅⊑c̅′) (ir-base 𝓋 x) (ir-base 𝓋′ x′) =
case cexpr-prec→⊑ _ _ c̅⊑c̅′ of λ where
⟨ l⊑l , _ ⟩ → ⊑-base (stampₗ-prec 𝓋 𝓋′ c̅⊑c̅′)
stamp-ir-prec (⊑-ref c⊑c′ d⊑d′ c̅⊑c̅′) (ir-ref 𝓋) (ir-ref 𝓋′) =
case cexpr-prec→⊑ _ _ c̅⊑c̅′ of λ where
⟨ l⊑l , _ ⟩ → ⊑-ref c⊑c′ d⊑d′ (stampₗ-prec _ _ c̅⊑c̅′)
stamp-ir-prec (⊑-fun d̅⊑d̅′ c⊑c′ d⊑d′ c̅⊑c̅′) (ir-fun 𝓋) (ir-fun 𝓋′) =
case cexpr-prec→⊑ _ _ c̅⊑c̅′ of λ where
⟨ l⊑l , _ ⟩ → ⊑-fun d̅⊑d̅′ c⊑c′ d⊑d′ (stampₗ-prec _ _ c̅⊑c̅′)
stamp-ir!-prec : ∀ {A A′ T T′} {c : Cast A ⇒ T of ⋆} {c′ : Cast A′ ⇒ T′ of ⋆} {ℓ ℓ′}
→ ⟨ c ⟩⊑⟨ c′ ⟩
→ (i : Irreducible c )
→ (i′ : Irreducible c′)
→ ℓ ≼ ℓ′
→ ⟨ stamp-ir c i ℓ ⟩⊑⟨ stamp-ir c′ i′ ℓ′ ⟩
stamp-ir!-prec (⊑-base c̅⊑c̅′) (ir-base {g = g} 𝓋 x) (ir-base {g = g′} 𝓋′ x′) ℓ≼ℓ′
rewrite g⋎̃⋆≡⋆ {g} | g⋎̃⋆≡⋆ {g′} =
case cexpr-prec→⊑ _ _ c̅⊑c̅′ of λ where
⟨ l⊑l , _ ⟩ → ⊑-base (stamp⋆ₗ-prec 𝓋 𝓋′ c̅⊑c̅′ ℓ≼ℓ′)
stamp-ir!-prec (⊑-ref c⊑c′ d⊑d′ c̅⊑c̅′) (ir-ref {g = g} 𝓋) (ir-ref {g = g′} 𝓋′) ℓ≼ℓ′
rewrite g⋎̃⋆≡⋆ {g} | g⋎̃⋆≡⋆ {g′} =
case cexpr-prec→⊑ _ _ c̅⊑c̅′ of λ where
⟨ l⊑l , _ ⟩ → ⊑-ref c⊑c′ d⊑d′ (stamp⋆ₗ-prec _ _ c̅⊑c̅′ ℓ≼ℓ′)
stamp-ir!-prec (⊑-fun d̅⊑d̅′ c⊑c′ d⊑d′ c̅⊑c̅′) (ir-fun {g = g} 𝓋) (ir-fun {g = g′} 𝓋′) ℓ≼ℓ′
rewrite g⋎̃⋆≡⋆ {g} | g⋎̃⋆≡⋆ {g′} =
case cexpr-prec→⊑ _ _ c̅⊑c̅′ of λ where
⟨ l⊑l , _ ⟩ → ⊑-fun d̅⊑d̅′ c⊑c′ d⊑d′ (stamp⋆ₗ-prec _ _ c̅⊑c̅′ ℓ≼ℓ′)
stamp-ir-high-on-high-right : ∀ {T A B} {c′ : Cast A ⇒ B}
→ T of l high ⊑⟨ c′ ⟩
→ (i′ : Irreducible c′)
→ T of l high ⊑⟨ stamp-ir c′ i′ high ⟩
stamp-ir-high-on-high-right (⊑-base (⊑-id l⊑l)) (ir-base CVal.id high≢high) = contradiction refl high≢high
stamp-ir-high-on-high-right (⊑-base (⊑-cast _ l⊑l ())) (ir-base (inj CVal.id) _)
stamp-ir-high-on-high-right (⊑-base (⊑-cast _ _ ())) (ir-base (inj (up CVal.id)) _)
stamp-ir-high-on-high-right (⊑-base (⊑-⊥ _ _)) (ir-base () _)
stamp-ir-high-on-high-right (⊑-ref A⊑c′ A⊑d′ (⊑-id l⊑l)) (ir-ref CVal.id) = ⊑-ref A⊑c′ A⊑d′ (⊑-id l⊑l)
stamp-ir-high-on-high-right (⊑-ref A⊑c′ A⊑d′ (⊑-cast _ _ ())) (ir-ref (inj CVal.id))
stamp-ir-high-on-high-right (⊑-ref A⊑c′ A⊑d′ (⊑-cast _ _ ())) (ir-ref (inj (up CVal.id)))
stamp-ir-high-on-high-right (⊑-ref A⊑c′ A⊑d′ (⊑-cast _ () _)) (ir-ref (up CVal.id))
stamp-ir-high-on-high-right (⊑-ref _ _ (⊑-⊥ _ _)) (ir-ref ())
stamp-ir-high-on-high-right (⊑-fun gc⊑d̅′ A⊑c′ B⊑d′ (⊑-id l⊑l)) (ir-fun CVal.id) = (⊑-fun gc⊑d̅′ A⊑c′ B⊑d′ (⊑-id l⊑l))
stamp-ir-high-on-high-right (⊑-fun _ _ _ (⊑-cast _ _ ())) (ir-fun (inj CVal.id))
stamp-ir-high-on-high-right (⊑-fun _ _ _ (⊑-cast _ _ ())) (ir-fun (inj (up CVal.id)))
stamp-ir-high-on-high-right (⊑-fun _ _ _ (⊑-cast _ () _)) (ir-fun (up CVal.id))
stamp-ir-high-on-high-right (⊑-fun _ _ _ (⊑-⊥ _ _)) (ir-fun ())
stamp-ir-high-on-high-left : ∀ {T′ A B} {c : Cast A ⇒ B}
→ ⟨ c ⟩⊑ T′ of l high
→ (i : Irreducible c)
→ ⟨ stamp-ir c i high ⟩⊑ T′ of l high
stamp-ir-high-on-high-left (⊑-base (⊑-id l⊑l)) (ir-base CVal.id high≢high) = contradiction refl high≢high
stamp-ir-high-on-high-left (⊑-base (⊑-cast (⊑-id l⊑l) y ⋆⊑)) (ir-base (inj CVal.id) _) = ⊑-base (⊑-cast (⊑-id l⊑l) l⊑l ⋆⊑)
stamp-ir-high-on-high-left (⊑-base (⊑-cast (⊑-cast (⊑-id ()) _ _) _ ⋆⊑)) (ir-base (inj (up CVal.id)) _)
stamp-ir-high-on-high-left (⊑-ref c⊑A′ d⊑A′ (⊑-id l⊑l)) (ir-ref CVal.id) = ⊑-ref c⊑A′ d⊑A′ (⊑-id l⊑l)
stamp-ir-high-on-high-left (⊑-ref c⊑A′ d⊑A′ (⊑-cast (⊑-id l⊑l) l⊑l ⋆⊑)) (ir-ref (inj CVal.id)) =
⊑-ref c⊑A′ d⊑A′ (⊑-cast (⊑-id l⊑l) l⊑l ⋆⊑)
stamp-ir-high-on-high-left (⊑-ref c⊑A′ d⊑A′ (⊑-cast (⊑-cast (⊑-id ()) _ _) y ⋆⊑)) (ir-ref (inj (up CVal.id)))
stamp-ir-high-on-high-left (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ (⊑-id l⊑l)) (ir-fun CVal.id) = (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ (⊑-id l⊑l))
stamp-ir-high-on-high-left (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ (⊑-cast (⊑-id l⊑l) l⊑l ⋆⊑)) (ir-fun (inj CVal.id)) =
⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ (⊑-cast (⊑-id l⊑l) l⊑l ⋆⊑)
stamp-ir-high-on-high-left (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ (⊑-cast (⊑-cast _ () _) _ ⋆⊑)) (ir-fun (inj (up CVal.id)))
stamp-ir-high-on-low-right : ∀ {T A B} {c′ : Cast A ⇒ B}
→ T of l low ⊑⟨ c′ ⟩
→ (i′ : Irreducible c′)
→ ⟨ cast (coerceᵣ-id T) (CExpr_⇒_.id (l low) ⨾ ↑) ⟩⊑⟨ stamp-ir c′ i′ high ⟩
stamp-ir-high-on-low-right _ (ir-base CVal.id ℓ≢ℓ) = contradiction refl ℓ≢ℓ
stamp-ir-high-on-low-right (⊑-base (⊑-cast (⊑-id l⊑l) x₂ ())) (ir-base (inj CVal.id) _)
stamp-ir-high-on-low-right (⊑-base (⊑-cast _ _ ())) (ir-base (inj (up CVal.id)) _)
stamp-ir-high-on-low-right (⊑-base (⊑-cast _ _ ())) (ir-base (up CVal.id) _)
stamp-ir-high-on-low-right (⊑-ref A⊑c′ A⊑d′ (⊑-id l⊑l)) (ir-ref CVal.id) =
⊑-ref (prec-right-coerce-id A⊑c′) (prec-right-coerce-id A⊑d′) (prec-refl _)
stamp-ir-high-on-low-right (⊑-ref A⊑c′ A⊑d′ (⊑-cast _ _ ())) (ir-ref (inj CVal.id))
stamp-ir-high-on-low-right (⊑-ref A⊑c′ A⊑d′ (⊑-cast _ _ ())) (ir-ref (inj (up CVal.id)))
stamp-ir-high-on-low-right (⊑-ref A⊑c′ A⊑d′ (⊑-cast _ l⊑l _)) (ir-ref (up CVal.id)) =
⊑-ref (prec-right-coerce-id A⊑c′) (prec-right-coerce-id A⊑d′) (prec-refl _)
stamp-ir-high-on-low-right (⊑-ref _ _ (⊑-⊥ _ _)) (ir-ref ())
stamp-ir-high-on-low-right (⊑-fun gc⊑d̅′ A⊑c′ B⊑d′ (⊑-id l⊑l)) (ir-fun CVal.id) =
⊑-fun (⊑-right-expand gc⊑d̅′) (prec-right-coerce-id A⊑c′) (prec-right-coerce-id B⊑d′) (prec-refl _)
stamp-ir-high-on-low-right (⊑-fun _ _ _ (⊑-cast _ _ ())) (ir-fun (inj CVal.id))
stamp-ir-high-on-low-right (⊑-fun _ _ _ (⊑-cast _ _ ())) (ir-fun (inj (up CVal.id)))
stamp-ir-high-on-low-right (⊑-fun gc⊑d̅′ A⊑c′ B⊑d′ (⊑-cast _ l⊑l _)) (ir-fun (up CVal.id)) =
⊑-fun (⊑-right-expand gc⊑d̅′) (prec-right-coerce-id A⊑c′) (prec-right-coerce-id B⊑d′) (prec-refl _)
stamp-ir-high-on-low-right (⊑-fun _ _ _ (⊑-⊥ _ _)) (ir-fun ())
stamp-ir-high-on-low-left : ∀ {T′ A B} {c : Cast A ⇒ B}
→ ⟨ c ⟩⊑ T′ of l low
→ (i : Irreducible c)
→ ⟨ stamp-ir c i high ⟩⊑⟨ cast (coerceᵣ-id T′) (CExpr_⇒_.id (l low) ⨾ ↑) ⟩
stamp-ir-high-on-low-left (⊑-base (⊑-id l⊑l)) (ir-base CVal.id high≢high) = contradiction refl high≢high
stamp-ir-high-on-low-left (⊑-base (⊑-cast (⊑-id l⊑l) y ⋆⊑)) (ir-base (inj CVal.id) _) = ⊑-base ↑!⊑↑
stamp-ir-high-on-low-left (⊑-base (⊑-cast (⊑-cast (⊑-id l⊑l) _ _) _ ⋆⊑)) (ir-base (inj (up CVal.id)) _) =
⊑-base ↑!⊑↑
stamp-ir-high-on-low-left (⊑-ref c⊑A′ d⊑A′ (⊑-id l⊑l)) (ir-ref CVal.id) =
⊑-ref (prec-left-coerce-id c⊑A′) (prec-left-coerce-id d⊑A′) (prec-refl _)
stamp-ir-high-on-low-left (⊑-ref c⊑A′ d⊑A′ (⊑-cast (⊑-id l⊑l) l⊑l ⋆⊑)) (ir-ref (inj CVal.id)) =
⊑-ref (prec-left-coerce-id c⊑A′) (prec-left-coerce-id d⊑A′) ↑!⊑↑
stamp-ir-high-on-low-left (⊑-ref c⊑A′ d⊑A′ (⊑-cast (⊑-cast (⊑-id l⊑l) _ _) y ⋆⊑)) (ir-ref (inj (up CVal.id))) =
⊑-ref (prec-left-coerce-id c⊑A′) (prec-left-coerce-id d⊑A′) ↑!⊑↑
stamp-ir-high-on-low-left (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ (⊑-id l⊑l)) (ir-fun CVal.id) =
⊑-fun (⊑-left-expand d̅⊑gc′) (prec-left-coerce-id c⊑A′) (prec-left-coerce-id d⊑B′) (prec-refl _)
stamp-ir-high-on-low-left (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ (⊑-cast (⊑-id l⊑l) l⊑l ⋆⊑)) (ir-fun (inj CVal.id)) =
⊑-fun (⊑-left-expand d̅⊑gc′) (prec-left-coerce-id c⊑A′) (prec-left-coerce-id d⊑B′) ↑!⊑↑
stamp-ir-high-on-low-left (⊑-fun d̅⊑gc′ c⊑A′ d⊑B′ (⊑-cast (⊑-cast _ l⊑l _) _ ⋆⊑)) (ir-fun (inj (up CVal.id))) =
⊑-fun (⊑-left-expand d̅⊑gc′) (prec-left-coerce-id c⊑A′) (prec-left-coerce-id d⊑B′) ↑!⊑↑