module WS-Annot where
open import Data.Sum
open import Data.Unit
open import Data.Empty
open import Data.Product renaming (_,_ to _,'_)
open import Relation.Binary.PropositionalEquality
open import Data.String
open import Function
open import Game renaming (_⊗_ to _⊗'_ ; _⊘_ to _⊘'_ )
open import WS-Syn
open import WS-Sem-Fsc
data FML : Pol → Game → Set where
F0 : FML + I
F1 : FML - I
F⊤ : FML + o
F⊥ : FML - o
_⊗_ : ∀ {G H} (M : FML - G)(N : FML - H) → FML - (G ⊗' H)
_⅋_ : ∀ {G H} (P : FML + G)(Q : FML + H) → FML + (G ⊗' H)
_&_ : ∀ {G H} (M : FML - G)(N : FML - H) → FML - (G ×' H)
_⊕_ : ∀ {G H} (P : FML + G)(Q : FML + H) → FML + (G ×' H)
ω& : ∀ {G} (M : FML - G) → FML - (ω× G)
ω⊕ : ∀ {G} (P : FML + G) → FML + (ω× G)
_-⊘_ : ∀ {G H} (M : FML - G)(N : FML - H) → FML - (G ⊘' H)
_+◁_ : ∀ {G H} (P : FML + G)(Q : FML + H) → FML + (G ⊘' H)
_+⊘_ : ∀ {G H} (P : FML + G)(N : FML - H) → FML + (H ⊸ G)
_-◁_ : ∀ {G H} (M : FML - G)(P : FML + H) → FML - (H ⊸ G)
toFml : ∀ {pol}{G}(A : FML pol G) → Fml pol
toFml F0 = F0
toFml F1 = F1
toFml F⊤ = F⊤
toFml F⊥ = F⊥
toFml (M ⊗ N) = (toFml M) ⊗ (toFml N)
toFml (P ⅋ Q) = (toFml P) ⅋ (toFml Q)
toFml (M & N) = (toFml M) & (toFml N)
toFml (P ⊕ Q) = (toFml P) ⊕ (toFml Q)
toFml (M -⊘ N) = (toFml M) ⊘ (toFml N)
toFml (P +◁ Q) = (toFml P) ◁ (toFml Q)
toFml (P +⊘ N) = (toFml P) ⊘ (toFml N)
toFml (M -◁ P) = (toFml M) ◁ (toFml P)
toFml (ω& M) = ω& (toFml M)
toFml (ω⊕ P) = ω⊕ (toFml P)
toFML : ∀ {pol}(A : Fml pol) → FML pol ⟦ A ⟧
toFML F0 = F0
toFML F1 = F1
toFML F⊥ = F⊥
toFML F⊤ = F⊤
toFML (M ⊗ N) = (toFML M) ⊗ (toFML N)
toFML (P ⅋ Q) = (toFML P) ⅋ (toFML Q)
toFML (P ⊕ Q) = (toFML P) ⊕ (toFML Q)
toFML (M & N) = (toFML M) & (toFML N)
toFML (ω& N) = ω& (toFML N)
toFML (ω⊕ P) = ω⊕ (toFML P)
toFML (_⊘_ { + } A M) = (toFML A) +⊘ (toFML M)
toFML (_⊘_ { - } A M) = (toFML A) -⊘ (toFML M)
toFML (_◁_ { + } A M) = (toFML A) +◁ (toFML M)
toFML (_◁_ { - } A M) = (toFML A) -◁ (toFML M)
mutual
annot+ : ∀ {G} (P : FML + G)(i : Mov G) → FML - (G ▸ i)
annot+ F0 ()
annot+ F⊤ tt = F1
annot+ (_⅋_ {gam _} {gam _} P Q) (inj₁ i) = annot+ P i -◁ Q
annot+ (_⅋_ {gam _} {gam _} P Q) (inj₂ j) = annot+ Q j -◁ P
annot+ (_⊕_ {gam _} {gam _} P Q) (inj₁ i) = annot+ P i
annot+ (_⊕_ {gam _} {gam _} P Q) (inj₂ j) = annot+ Q j
annot+ (ω⊕ {gam _} P) m = annot+ P (proj₂ m)
annot+ (_+◁_ {gam _} {gam _} P Q) i = annot+ P i -◁ Q
annot+ (_+⊘_ {gam _} {gam _} P N) i = annot+ P i ⊗ N
annot- : ∀ {G} (M : FML - G)(i : Mov G) → FML + (G ▸ i)
annot- F1 ()
annot- F⊥ tt = F0
annot- (_⊗_ {gam _} {gam _} M N) (inj₁ i) = annot- M i +⊘ N
annot- (_⊗_ {gam _} {gam _} M N) (inj₂ j) = annot- N j +⊘ M
annot- (_&_ {gam _} {gam _} M N) (inj₁ i) = annot- M i
annot- (ω& {gam _} M) m = annot- M (proj₂ m)
annot- (_&_ {gam _} {gam _} M N) (inj₂ j) = annot- N j
annot- (_-⊘_ {gam _} {gam _} M N) i = annot- M i +⊘ N
annot- (_-◁_ {gam _} {gam _} M P) i = annot- M i ⅋ P
annot : ∀ {pol G}(A : FML pol G)(i : Mov G) → FML (¬ pol) (G ▸ i)
annot { + } = annot+
annot { - } = annot-
PolFML : Game → Set
PolFML G = Σ Pol (λ p → FML p G)
anotate' : ∀ {p} {G} (A : FML p G) → Annotation G PolFML
anotate' {p} {gam f} A = ν (p ,' A) (λ i → anotate' {¬ p} $ annot {p} A i)
forget : ∀ {G} → Annotation G PolFML → Annotation G (λ _ → PolFml)
forget {gam g} (ν (p ,' A) f) = ν (p ,' toFml A) (λ i → forget (f i))
anotate : ∀ {p} (A : Fml p) → Annotation ⟦ A ⟧ (λ _ → PolFml)
anotate = forget ∘ anotate' ∘ toFML