-- ==========================================================
-- 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,.|':;!-?][}{)(⟧⟦"])* ;
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 ;
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 "" ;