-- ==========================================================
-- BNFC grammar for φ-programs (translated from EO)
-- ==========================================================
--
-- This is a non-ambiguous grammar for φ-programs.

token Bytes ({"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] {"-"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] ({"-"} ["0123456789ABCDEF"] ["0123456789ABCDEF"])+) ;
token Function upper (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;
token LabelId  lower (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;
token AlphaIndex ({"α0"} | {"α"} (digit - ["0"]) (digit)* ) ;
token MetaId {"!"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;

Program. Program ::= "{" [Binding] "}" ;

Formation.      Object ::= "⟦" [Binding] "⟧" ;
Application.    Object ::= Object "(" [Binding] ")" ;
ObjectDispatch. Object ::= Object "." Attribute ;
GlobalDispatch. Object ::= "Φ" "." Attribute ;
ThisDispatch.   Object ::= "ξ" "." Attribute ;
Termination.    Object ::= "⊥" ;
MetaObject.     Object ::= MetaId ;

AlphaBinding.   Binding ::= Attribute "↦" Object ;
EmptyBinding.   Binding ::= Attribute "↦" "∅" ;
DeltaBinding.   Binding ::= "Δ" "⤍" Bytes ;
LambdaBinding.  Binding ::= "λ" "⤍" Function ;
MetaBindings.   Binding ::= MetaId ;
separator Binding "," ;

Phi.    Attribute ::= "φ" ;   -- decoratee object
Rho.    Attribute ::= "ρ" ;   -- parent object
Sigma.  Attribute ::= "σ" ;   -- home object
VTX.    Attribute ::= "ν" ;   -- the vertex identifier (an object that represents the unique identifier of the containing object)
Label.  Attribute ::= LabelId ;
Alpha.  Attribute ::= AlphaIndex ;
MetaAttr. Attribute ::= MetaId ;

-- Additional symbols used as attributes in the rules
ObjectAttr. RuleAttribute ::= Attribute ;
DeltaAttr.  RuleAttribute ::= "Δ" ;
LambdaAttr. RuleAttribute ::= "λ" ;

PeeledObject. PeeledObject ::= ObjectHead [ObjectAction] ;

HeadFormation.    ObjectHead ::= "⟦" [Binding] "⟧" ;
HeadGlobal.       ObjectHead ::= "Φ" ;
HeadThis.         ObjectHead ::= "ξ" ;
HeadTermination.  ObjectHead ::= "⊥" ;

ActionApplication.  ObjectAction ::= "(" [Binding] ")" ;
ActionDispatch.     ObjectAction ::= "." Attribute ;
separator ObjectAction "" ;