module WS-Annot where
-- in which we describe annotated games, and construct them out of WS
-- formulas

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

-- Our goal is to construct a function:
--   anotate : ∀ {p} (A : Fml p) → Annotation ⟦ A ⟧ (λ _ → PolFml)
-- annotating each game with some formula with a PolFml, i.e. a
-- formula of some polarity.

-- To do this, we first need a notion of semantic-annotated syntax:

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)

-- Annotation functions

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' takes a formula whose semantics is G, and anotates G by
-- (semantic-anotated) formulas. The type had to be this strong for
-- the induction to work.

anotate' :  {p} {G} (A : FML p G)  Annotation G PolFML
anotate' {p} {gam f} A = ν (p ,' A)  i  anotate' {¬ p} $ annot {p} A i)

-- We can now construct the function anotate by an appropriate
-- weakening:

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