------------------------------------------------------------------------ -- 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