module CoercionExpr.Precision 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 hiding ([_])
open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_)
open import Data.Maybe
open import Relation.Nullary using (Β¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≑_; refl)
open import Function using (case_of_)

open import Common.Utils
open import Common.SecurityLabels
open import Common.BlameLabels
open import CoercionExpr.CoercionExpr


infix 4 ⊒_βŠ‘_
infix 4 ⊒l_βŠ‘_
infix 4 ⊒r_βŠ‘_

data ⊒_βŠ‘_ : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€²} (cΜ… : CExpr g₁ β‡’ gβ‚‚) (cΜ…β€² : CExpr g₁′ β‡’ gβ‚‚β€²) β†’ Set where

  βŠ‘-id : βˆ€ {g gβ€²}
    β†’ (gβŠ‘gβ€² : g βŠ‘β‚— gβ€²)
      ---------------------------------
    β†’ ⊒ id g βŠ‘ id gβ€²

  βŠ‘-cast : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€² g₃ g₃′}
             {cΜ… : CExpr g₁ β‡’ gβ‚‚} {cΜ…β€² : CExpr g₁′ β‡’ gβ‚‚β€²}
             {c : ⊒ gβ‚‚ β‡’ g₃} {cβ€² : ⊒ gβ‚‚β€² β‡’ g₃′}
    β†’ ⊒ cΜ… βŠ‘ cΜ…β€²
    β†’ gβ‚‚ βŠ‘β‚— gβ‚‚β€² β†’ g₃ βŠ‘β‚— g₃′ {- c βŠ‘ cβ€² -}
      -------------------------------------------
    β†’ ⊒ cΜ… β¨Ύ c βŠ‘ cΜ…β€² β¨Ύ cβ€²

  βŠ‘-castl : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€² g₃}
              {cΜ… : CExpr g₁ β‡’ gβ‚‚} {cΜ…β€² : CExpr g₁′ β‡’ gβ‚‚β€²}
              {c : ⊒ gβ‚‚ β‡’ g₃}
    β†’ ⊒ cΜ… βŠ‘ cΜ…β€²
    β†’ gβ‚‚ βŠ‘β‚— gβ‚‚β€² β†’ g₃ βŠ‘β‚— gβ‚‚β€²  {- c βŠ‘ gβ‚‚β€² -}
      -------------------------------------------
    β†’ ⊒ cΜ… β¨Ύ c βŠ‘ cΜ…β€²

  βŠ‘-castr : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€² g₃′}
              {cΜ… : CExpr g₁ β‡’ gβ‚‚} {cΜ…β€² : CExpr g₁′ β‡’ gβ‚‚β€²}
              {cβ€² : ⊒ gβ‚‚β€² β‡’ g₃′}
    β†’ ⊒ cΜ… βŠ‘ cΜ…β€²
    β†’ gβ‚‚ βŠ‘β‚— gβ‚‚β€² β†’ gβ‚‚ βŠ‘β‚— g₃′  {- gβ‚‚ βŠ‘ cβ€² -}
      -------------------------------------------
    β†’ ⊒ cΜ… βŠ‘ cΜ…β€² β¨Ύ cβ€²

  βŠ‘-βŠ₯ : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€²} {cΜ… : CExpr g₁ β‡’ gβ‚‚} {p}
    β†’ g₁ βŠ‘β‚— g₁′
    β†’ gβ‚‚ βŠ‘β‚— gβ‚‚β€²
      ---------------------------------
    β†’ ⊒ cΜ… βŠ‘ βŠ₯ g₁′ gβ‚‚β€² p


data ⊒l_βŠ‘_ : βˆ€ {g₁ gβ‚‚} (cΜ… : CExpr g₁ β‡’ gβ‚‚) (g : Label) β†’ Set where

  βŠ‘-id : βˆ€ {g gβ€²}
    β†’ (gβŠ‘gβ€² : g βŠ‘β‚— gβ€²)
      ---------------------------------
    β†’ ⊒l id g βŠ‘ gβ€²

  βŠ‘-cast : βˆ€ {g₁ gβ‚‚ g₃ gβ€²}
             {cΜ… : CExpr g₁ β‡’ gβ‚‚}
             {c : ⊒ gβ‚‚ β‡’ g₃}
    β†’ ⊒l cΜ… βŠ‘ gβ€²
    β†’ gβ‚‚ βŠ‘β‚— gβ€² β†’ g₃ βŠ‘β‚— gβ€² {- c βŠ‘ gβ€² -}
      -------------------------------------------
    β†’ ⊒l cΜ… β¨Ύ c βŠ‘ gβ€²


data ⊒r_βŠ‘_ : βˆ€ {g₁′ gβ‚‚β€²} (g : Label) (cΜ…β€² : CExpr g₁′ β‡’ gβ‚‚β€²) β†’ Set where

  βŠ‘-id : βˆ€ {g gβ€²}
    β†’ (gβŠ‘gβ€² : g βŠ‘β‚— gβ€²)
      ---------------------------------
    β†’ ⊒r g βŠ‘ id gβ€²

  βŠ‘-cast : βˆ€ {g g₁′ gβ‚‚β€² g₃′}
             {cΜ…β€² : CExpr g₁′ β‡’ gβ‚‚β€²}
             {cβ€² : ⊒ gβ‚‚β€² β‡’ g₃′}
    β†’ ⊒r g βŠ‘ cΜ…β€²
    β†’ g βŠ‘β‚— gβ‚‚β€² β†’ g βŠ‘β‚— g₃′ {- g βŠ‘ cβ€² -}
      -------------------------------------------
    β†’ ⊒r g βŠ‘ cΜ…β€² β¨Ύ cβ€²

  βŠ‘-βŠ₯ : βˆ€ {g g₁′ gβ‚‚β€²} {p}
    β†’ g βŠ‘β‚— g₁′
    β†’ g βŠ‘β‚— gβ‚‚β€²
      ---------------------------------
    β†’ ⊒r g βŠ‘ βŠ₯ g₁′ gβ‚‚β€² p


prec-refl : βˆ€ {g₁ gβ‚‚} (cΜ… : CExpr g₁ β‡’ gβ‚‚) β†’ ⊒ cΜ… βŠ‘ cΜ…
prec-refl (id _) = βŠ‘-id βŠ‘β‚—-refl
prec-refl (cΜ… β¨Ύ c) = βŠ‘-cast (prec-refl cΜ…) βŠ‘β‚—-refl βŠ‘β‚—-refl
prec-refl (βŠ₯ _ _ p) = βŠ‘-βŠ₯ βŠ‘β‚—-refl βŠ‘β‚—-refl


precβ†’βŠ‘ : βˆ€ {g₁ g₁′ gβ‚‚ gβ‚‚β€²} (cΜ… : CExpr g₁ β‡’ gβ‚‚) (cΜ…β€² : CExpr g₁′ β‡’ gβ‚‚β€²)
  β†’ ⊒ cΜ… βŠ‘ cΜ…β€²
  β†’ (g₁ βŠ‘β‚— g₁′) Γ— (gβ‚‚ βŠ‘β‚— gβ‚‚β€²)
precβ†’βŠ‘ (id g) (id gβ€²) (βŠ‘-id gβŠ‘gβ€²) = ⟨ gβŠ‘gβ€² , gβŠ‘gβ€² ⟩
precβ†’βŠ‘ (cΜ… β¨Ύ c) (cΜ…β€² β¨Ύ cβ€²) (βŠ‘-cast cΜ…βŠ‘cΜ…β€² _ gβ‚‚βŠ‘gβ‚‚β€²) =
  case precβ†’βŠ‘ cΜ… cΜ…β€² cΜ…βŠ‘cΜ…β€² of Ξ» where
  ⟨ gβ‚βŠ‘g₁′ , _ ⟩ β†’ ⟨ gβ‚βŠ‘g₁′ , gβ‚‚βŠ‘gβ‚‚β€² ⟩
precβ†’βŠ‘ (cΜ… β¨Ύ c) cΜ…β€² (βŠ‘-castl cΜ…βŠ‘cΜ…β€² gβ‚‚βŠ‘gβ‚‚β€² gβ‚ƒβŠ‘gβ‚‚β€²) =
  case precβ†’βŠ‘ cΜ… cΜ…β€² cΜ…βŠ‘cΜ…β€² of Ξ» where
  ⟨ gβ‚βŠ‘g₁′ , _ ⟩ β†’ ⟨ gβ‚βŠ‘g₁′ , gβ‚ƒβŠ‘gβ‚‚β€² ⟩
precβ†’βŠ‘ cΜ… (cΜ…β€² β¨Ύ cβ€²) (βŠ‘-castr cΜ…βŠ‘cΜ…β€² gβ‚‚βŠ‘gβ‚‚β€² gβ‚‚βŠ‘g₃′) =
  case precβ†’βŠ‘ cΜ… cΜ…β€² cΜ…βŠ‘cΜ…β€² of Ξ» where
  ⟨ gβ‚βŠ‘g₁′ , _ ⟩ β†’ ⟨ gβ‚βŠ‘g₁′ , gβ‚‚βŠ‘g₃′ ⟩
precβ†’βŠ‘ cΜ… (βŠ₯ _ _ _) (βŠ‘-βŠ₯ gβ‚βŠ‘g₁′ gβ‚‚βŠ‘gβ‚‚β€²) = ⟨ gβ‚βŠ‘g₁′ , gβ‚‚βŠ‘gβ‚‚β€² ⟩


prec-leftβ†’βŠ‘ : βˆ€ {g₁ gβ‚‚ gβ€²} (cΜ… : CExpr g₁ β‡’ gβ‚‚)
  β†’ ⊒l cΜ… βŠ‘ gβ€²
  β†’ (g₁ βŠ‘β‚— gβ€²) Γ— (gβ‚‚ βŠ‘β‚— gβ€²)
prec-leftβ†’βŠ‘ (id g) (βŠ‘-id gβŠ‘gβ€²) = ⟨ gβŠ‘gβ€² , gβŠ‘gβ€² ⟩
prec-leftβ†’βŠ‘ (cΜ… β¨Ύ c) (βŠ‘-cast cΜ…βŠ‘gβ€² gβ‚βŠ‘gβ€² gβ‚‚βŠ‘gβ€²) =
  ⟨ proj₁ (prec-leftβ†’βŠ‘ cΜ… cΜ…βŠ‘gβ€²) , gβ‚‚βŠ‘gβ€² ⟩

prec-rightβ†’βŠ‘ : βˆ€ {g g₁′ gβ‚‚β€²} (cΜ…β€² : CExpr g₁′ β‡’ gβ‚‚β€²)
  β†’ ⊒r g βŠ‘ cΜ…β€²
  β†’ (g βŠ‘β‚— g₁′) Γ— (g βŠ‘β‚— gβ‚‚β€²)
prec-rightβ†’βŠ‘ (id _) (βŠ‘-id gβŠ‘gβ€²) = ⟨ gβŠ‘gβ€² , gβŠ‘gβ€² ⟩
prec-rightβ†’βŠ‘ (_ β¨Ύ _) (βŠ‘-cast gβŠ‘cΜ…β€² x y) = ⟨ proj₁ (prec-rightβ†’βŠ‘ _ gβŠ‘cΜ…β€²) , y ⟩
prec-rightβ†’βŠ‘ (βŠ₯ _ _ _) (βŠ‘-βŠ₯ x y) = ⟨ x , y ⟩

βŠ‘-left-expand : βˆ€ {g₁ gβ‚‚ gβ€²} {cΜ… : CExpr g₁ β‡’ gβ‚‚}
  β†’ ⊒l cΜ… βŠ‘ gβ€²
  β†’ ⊒  cΜ… βŠ‘ id gβ€²
βŠ‘-left-expand (βŠ‘-id gβŠ‘gβ€²) = βŠ‘-id gβŠ‘gβ€²
βŠ‘-left-expand (βŠ‘-cast cΜ…βŠ‘gβ€² gβ‚βŠ‘gβ€² gβ‚‚βŠ‘gβ€²) = βŠ‘-castl (βŠ‘-left-expand cΜ…βŠ‘gβ€²) gβ‚βŠ‘gβ€² gβ‚‚βŠ‘gβ€²

βŠ‘-left-contract : βˆ€ {g₁ gβ‚‚ gβ€²} {cΜ… : CExpr g₁ β‡’ gβ‚‚}
  β†’ ⊒  cΜ… βŠ‘ id gβ€²
  β†’ ⊒l cΜ… βŠ‘ gβ€²
βŠ‘-left-contract (βŠ‘-id gβŠ‘gβ€²) = βŠ‘-id gβŠ‘gβ€²
βŠ‘-left-contract (βŠ‘-castl cΜ…βŠ‘id gβ‚βŠ‘gβ€² gβ‚‚βŠ‘gβ€²) = βŠ‘-cast (βŠ‘-left-contract cΜ…βŠ‘id) gβ‚βŠ‘gβ€² gβ‚‚βŠ‘gβ€²

βŠ‘-right-expand : βˆ€ {g g₁′ gβ‚‚β€²} {cΜ…β€² : CExpr g₁′ β‡’ gβ‚‚β€²}
  β†’ ⊒r g βŠ‘ cΜ…β€²
  β†’ ⊒  id g βŠ‘ cΜ…β€²
βŠ‘-right-expand (βŠ‘-id gβŠ‘gβ€²) = βŠ‘-id gβŠ‘gβ€²
βŠ‘-right-expand (βŠ‘-cast gβŠ‘cΜ…β€² gβŠ‘g₁′ gβŠ‘gβ‚‚β€²) = βŠ‘-castr (βŠ‘-right-expand gβŠ‘cΜ…β€²) gβŠ‘g₁′ gβŠ‘gβ‚‚β€²
βŠ‘-right-expand (βŠ‘-βŠ₯ gβŠ‘g₁′ gβŠ‘gβ‚‚β€²) = βŠ‘-βŠ₯ gβŠ‘g₁′ gβŠ‘gβ‚‚β€²

βŠ‘-right-contract : βˆ€ {g g₁′ gβ‚‚β€²} {cΜ…β€² : CExpr g₁′ β‡’ gβ‚‚β€²}
  β†’ ⊒ id g βŠ‘ cΜ…β€²
  β†’ ⊒r   g βŠ‘ cΜ…β€²
βŠ‘-right-contract (βŠ‘-id gβŠ‘gβ€²) = βŠ‘-id gβŠ‘gβ€²
βŠ‘-right-contract (βŠ‘-castr idβŠ‘cΜ…β€² gβŠ‘g₁′ gβŠ‘gβ‚‚β€²) = βŠ‘-cast (βŠ‘-right-contract idβŠ‘cΜ…β€²) gβŠ‘g₁′ gβŠ‘gβ‚‚β€²
βŠ‘-right-contract (βŠ‘-βŠ₯ gβŠ‘g₁′ gβŠ‘gβ‚‚β€²) = βŠ‘-βŠ₯ gβŠ‘g₁′ gβŠ‘gβ‚‚β€²


pres-prec-left : βˆ€ {g₁ gβ‚‚ gβ€²} {c̅₁ cΜ…β‚‚ : CExpr g₁ β‡’ gβ‚‚}
  β†’ ⊒l c̅₁ βŠ‘ gβ€²
  β†’ c̅₁ β€”β†’ cΜ…β‚‚
  β†’ ⊒l cΜ…β‚‚ βŠ‘ gβ€²
pres-prec-left (βŠ‘-cast prec gβ‚βŠ‘gβ€² gβ‚‚βŠ‘gβ€²) (ΞΎ r) =
  βŠ‘-cast (pres-prec-left prec r) gβ‚βŠ‘gβ€² gβ‚‚βŠ‘gβ€²
pres-prec-left (βŠ‘-cast () x x₁) ΞΎ-βŠ₯
pres-prec-left (βŠ‘-cast prec _ _) (id x) = prec
pres-prec-left (βŠ‘-cast (βŠ‘-cast prec lβŠ‘l β‹†βŠ‘) β‹†βŠ‘ lβŠ‘l) (?-id x) = prec
pres-prec-left (βŠ‘-cast (βŠ‘-cast _ lβŠ‘l β‹†βŠ‘) β‹†βŠ‘ ()) (?-↑ x)
pres-prec-left (βŠ‘-cast (βŠ‘-cast prec lβŠ‘l β‹†βŠ‘) β‹†βŠ‘ ()) (?-βŠ₯ x)

pres-prec-left-mult : βˆ€ {g₁ gβ‚‚ gβ€²} {c̅₁ cΜ…β‚‚ : CExpr g₁ β‡’ gβ‚‚}
  β†’ ⊒l c̅₁ βŠ‘ gβ€²
  β†’ c̅₁ β€”β†  cΜ…β‚‚
  β†’ ⊒l cΜ…β‚‚ βŠ‘ gβ€²
pres-prec-left-mult prec (_ ∎) = prec
pres-prec-left-mult prec (_ β€”β†’βŸ¨ r ⟩ r*) = pres-prec-left-mult (pres-prec-left prec r) r*

pres-prec-right : βˆ€ {g g₁ gβ‚‚} {c̅₁ cΜ…β‚‚ : CExpr g₁ β‡’ gβ‚‚}
  β†’ ⊒r g βŠ‘ c̅₁
  β†’ c̅₁ β€”β†’ cΜ…β‚‚
  β†’ ⊒r g βŠ‘ cΜ…β‚‚
pres-prec-right (βŠ‘-cast prec gβŠ‘g₃ gβŠ‘gβ‚‚) (ΞΎ r) = βŠ‘-cast (pres-prec-right prec r) gβŠ‘g₃ gβŠ‘gβ‚‚
pres-prec-right (βŠ‘-cast (βŠ‘-βŠ₯ gβŠ‘g₁ _) _ gβŠ‘gβ‚‚) ΞΎ-βŠ₯ = βŠ‘-βŠ₯ gβŠ‘g₁ gβŠ‘gβ‚‚
pres-prec-right (βŠ‘-cast prec _ _) (id _) = prec
pres-prec-right (βŠ‘-cast (βŠ‘-cast prec _ _) β‹†βŠ‘ _) (?-id _) = prec
pres-prec-right (βŠ‘-cast (βŠ‘-cast prec _ _) β‹†βŠ‘ _) (?-↑ _) = βŠ‘-cast prec β‹†βŠ‘ β‹†βŠ‘
pres-prec-right (βŠ‘-cast (βŠ‘-cast prec _ _) _ gβŠ‘low) (?-βŠ₯ _) = βŠ‘-βŠ₯ (proj₁ (prec-rightβ†’βŠ‘ _ prec)) gβŠ‘low

pres-prec-right-mult : βˆ€ {g g₁ gβ‚‚} {c̅₁ cΜ…β‚‚ : CExpr g₁ β‡’ gβ‚‚}
  β†’ ⊒r g βŠ‘ c̅₁
  β†’ c̅₁ β€”β†  cΜ…β‚‚
  β†’ ⊒r g βŠ‘ cΜ…β‚‚
pres-prec-right-mult prec (_ ∎) = prec
pres-prec-right-mult prec (_ β€”β†’βŸ¨ r ⟩ r*) = pres-prec-right-mult (pres-prec-right prec r) r*


prec-inj-left : βˆ€ {g gβ€² β„“}
  (cΜ…β‚™ : CExpr g β‡’ ⋆) (cΜ…β‚™β€² : CExpr gβ€² β‡’ l β„“)
  β†’ CVal cΜ…β‚™ β†’ CVal cΜ…β‚™β€²
  β†’ ⊒ cΜ…β‚™ βŠ‘ cΜ…β‚™β€² β¨Ύ β„“ !
  β†’ ⊒ cΜ…β‚™ βŠ‘ cΜ…β‚™β€²
prec-inj-left (cΜ…β‚™ β¨Ύ c) cΜ…β‚™β€² v vβ€² (βŠ‘-cast cΜ…β‚™βŠ‘cΜ…β‚™β€² gβ‚βŠ‘β„“ β‹†βŠ‘) = βŠ‘-castl cΜ…β‚™βŠ‘cΜ…β‚™β€² gβ‚βŠ‘β„“ β‹†βŠ‘
prec-inj-left (cΜ…β‚™ β¨Ύ id .⋆) cΜ…β‚™β€² () vβ€² (βŠ‘-castl cΜ…β‚™βŠ‘cΜ…β‚™β€²β¨Ύ! β‹†βŠ‘ β‹†βŠ‘)
prec-inj-left cΜ…β‚™ cΜ…β‚™β€² v vβ€² (βŠ‘-castr cΜ…β‚™βŠ‘cΜ…β‚™β€²β¨Ύ! β‹†βŠ‘ β‹†βŠ‘) = cΜ…β‚™βŠ‘cΜ…β‚™β€²β¨Ύ!


prec-left-safe : βˆ€ {β„“ g gβ€² p} {cΜ… : CExpr l β„“ β‡’ g}
  β†’ ⊒l cΜ… βŠ‘ gβ€²
  β†’ Β¬ (cΜ… β€”β†  βŠ₯ (l β„“) g p)
prec-left-safe (βŠ‘-id gβŠ‘gβ€²) (.(id (l _)) β€”β†’βŸ¨ () ⟩ _)
prec-left-safe (βŠ‘-cast prec x y) (_ β€”β†’βŸ¨ ΞΎ r ⟩ r*) =
  prec-left-safe (βŠ‘-cast (pres-prec-left prec r) x y) r*
prec-left-safe (βŠ‘-cast () _ _) (_ β€”β†’βŸ¨ ΞΎ-βŠ₯ ⟩ _ ∎)
prec-left-safe (βŠ‘-cast prec _ _) (_ β€”β†’βŸ¨ id _ ⟩ r*) =
  prec-left-safe prec r*
prec-left-safe (βŠ‘-cast (βŠ‘-cast prec _ _) _ _) (_ β€”β†’βŸ¨ ?-id _ ⟩ r*) =
  prec-left-safe prec r*
prec-left-safe (βŠ‘-cast (βŠ‘-cast _ lβŠ‘l _) _ ()) (_ β€”β†’βŸ¨ ?-↑ _ ⟩ _)
prec-left-safe (βŠ‘-cast (βŠ‘-cast _ lβŠ‘l _) _ ()) (_ β€”β†’βŸ¨ ?-βŠ₯ _ ⟩ _ ∎)


-- shorthands
!βŠ‘β†‘ : ⊒ id (l low) β¨Ύ (low !) βŠ‘ id (l low) β¨Ύ ↑
!βŠ‘β†‘ = βŠ‘-cast (βŠ‘-id lβŠ‘l) lβŠ‘l β‹†βŠ‘

!βŠ‘β†‘! : ⊒ id (l low) β¨Ύ (low !) βŠ‘ id (l low) β¨Ύ ↑ β¨Ύ (high !)
!βŠ‘β†‘! = βŠ‘-castr (βŠ‘-cast (βŠ‘-id lβŠ‘l) lβŠ‘l β‹†βŠ‘) β‹†βŠ‘ β‹†βŠ‘

↑!βŠ‘β†‘ : ⊒ id (l low) β¨Ύ ↑ β¨Ύ (high !) βŠ‘ id (l low) β¨Ύ ↑
↑!βŠ‘β†‘ = βŠ‘-castl (prec-refl _) lβŠ‘l β‹†βŠ‘