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

comment "//" ;
comment "/*" "*/" ;

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,.|':;!-?][}{)(⟧⟦"])* ;
token MetaFunctionName {"@"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ;

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

Formation.      Object ::= "⟦" [Binding] "⟧" ;
Application.    Object ::= Object "(" [Binding] ")" ;
ObjectDispatch. Object ::= Object "." Attribute ;
GlobalObject.   Object ::= "Φ";
ThisObject.     Object ::= "ξ";
Termination.    Object ::= "⊥" ;
MetaObject.     Object ::= MetaId ;
MetaFunction.   Object ::= MetaFunctionName "(" Object ")" ;

AlphaBinding.       Binding ::= Attribute "↦" Object ;
EmptyBinding.       Binding ::= Attribute "↦" "∅" ;
DeltaBinding.       Binding ::= "Δ" "⤍" Bytes ;
DeltaEmptyBinding.  Binding ::= "Δ" "⤍" "∅" ;
LambdaBinding.      Binding ::= "λ" "⤍" Function ;
MetaBindings.       Binding ::= MetaId ;
MetaDeltaBinding.   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 "" ;