------------------------------------------------------------------------
-- Fixity and associativity
------------------------------------------------------------------------

module Mixfix.Fixity where

open import Data.Fin using (Fin; zero; suc; #_)
open import Data.Fin.Props using (eq?)
open import Function.LeftInverse
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq

data Associativity : Set where
  left  : Associativity
  right : Associativity
  non   : Associativity

-- A combination of fixity and associativity. Only infix operators
-- have associativity.

-- Note that infix is a reserved word.

data Fixity : Set where
  prefx  : Fixity
  infx   : (assoc : Associativity) → Fixity
  postfx : Fixity
  closed : Fixity

Fixity-is-finite : LeftInverse (Eq.setoid Fixity) (Eq.setoid (Fin 6))
Fixity-is-finite = record
  { from            = Eq.→-to-⟶ from
  ; to              = Eq.→-to-⟶ to
  ; left-inverse-of = left-inverse-of
  }
  where
  to : Fixity → Fin 6
  to prefx        = # 0
  to (infx left)  = # 1
  to (infx right) = # 2
  to (infx non)   = # 3
  to postfx       = # 4
  to closed       = # 5

  from : Fin 6 → Fixity
  from zero                                   = prefx
  from (suc zero)                             = infx left
  from (suc (suc zero))                       = infx right
  from (suc (suc (suc zero)))                 = infx non
  from (suc (suc (suc (suc zero))))           = postfx
  from (suc (suc (suc (suc (suc zero)))))     = closed
  from (suc (suc (suc (suc (suc (suc ()))))))

  left-inverse-of : Eq.→-to-⟶ from LeftInverseOf Eq.→-to-⟶ to
  left-inverse-of prefx        = refl
  left-inverse-of (infx left)  = refl
  left-inverse-of (infx right) = refl
  left-inverse-of (infx non)   = refl
  left-inverse-of postfx       = refl
  left-inverse-of closed       = refl

_≟_ : Decidable (_≡_ {A = Fixity})
_≟_ = eq? injection
  where open LeftInverse Fixity-is-finite