001002

witness{
 📎 1.2 Notational Conventions and Terminology
 lbl{"1.2 Notational Conventions and Terminology" } 

    --------------------------------------------------------------------------------
001 1.
002 The key words MUST, MUST NOT, REQUIRED, SHALL, SHALL NOT, SHOULD, SHOULD NOT, 
003 RECOMMENDED, MAY, and OPTIONAL, when they appear EMPHASIZED in this document, 
004 are to be interpreted as described in RFC 2119. Other terminology used to 
005 describe the EXI format is defined in the body of this specification.
006 The term event and stream is used throughout this document to denote EXI event 
007 and EXI stream respectively unless the words are qualified differently to mean 
008 otherwise.
009 This document specifies an abstract grammar for EXI. In grammar notation, all 
010 terminal symbols are represented in plain text and all non-terminal symbols are 
011 represented in italics. Grammar productions are represented as follows:
012 
013 LeftHandSide: Terminal NonTerminal
014 
015 A set of one or more grammar productions that share the same left-hand side 
016 non-terminal symbol are often presented together annotated with event codes that 
017 specify how events matching the terminal symbols of the associated productions 
018 are represented in the EXI stream as follows:
019 
020 LeftHandSide:
021  Terminal_1 NonTerminal_1    EventCode_1
022  Terminal_2 NonTerminal_2    EventCode_2
023  Terminal_3 NonTerminal_3    EventCode_3
024 
025  ...
026 
027  Terminal_n NonTerminal_n    EventCode_n 
028 
029 Section 8.1 Grammar Notation introduces additional notations for describing 
030 productions and event codes in grammars. Those additional notations facilitate 
031 concise representation of the EXI grammar system.
032 
033 [Definition:] In this document, the term qname is used to denote a QName. 
034 QName values are composed of an uri, a local-name and an optional prefix. Two 
035 qnames are considered equal if they have the same uri and local-name, 
036 regardless of their prefix values. In cases where prefixes are not relevant, 
037 such as in the grammar notation, they are not specified by this document.
038 
039 Terminal symbols that are qualified with a qname permit the use of a wildcard 
040 symbol (*) in place of or as part of a qname. The forms of terminal symbols 
041 involving qname wildcards used in grammars and their definitions are described 
042 in the table below.
043 Wildcard               Definition
044 
045 
046 SE(*)                  The terminal symbol that matches a start element (SE)
047                        event with any qname.
048 SE(uri: *)             The terminal symbol that matches a start element (SE)
049                        event with any local-name in namespace uri.
050 AT(*)                  The terminal symbol that matches an attribute (AT)
051                        event with any qname
052 AT (uri:*)             The terminal symbol that matches an attribute (AT)
053                        event with any local-name in namespace uri.
054 
055 Several prefixes are used throughout this document to designate certain 
056 namespaces.
057 The bindings shown below are assumed, however, any prefixes can be used in 
058 practice if they are properly bound to the namespaces.
059 
060 Prefix                      Namespace Name
061 exi                         http://www.w3.org/2009/exi
062 xsd                         http://www.w3.org/2001/XMLSchema
063 xsi                         http://www.w3.org/2001/XMLSchema-instance
064 
065 In describing the layout of an EXI format construct, a pair of square 
066 brackets [] are used to surround the name of a field to denote that the 
067 occurrence of the field is optional in the structure of the part or component 
068 that contains the field.
069 In arithmetic expressions, the notation |^x^| where x represents a real 
070 number denotes the ceiling of x, that is, the smallest integer greater than 
071 or equal to x.
072 When it is stated that strings are sorted in lexicographical order, it is done 
073 so character by character, and the order among characters is determines by 
074 comparing their Unicode code points.
075 
076 Unless stated otherwise, when this specification indicates one type is derived 
077 form another type, it means the type is derived by extension or restriction, not
078 by union or list. Similarly, when this specification uses the term type 
079 hierarchy, it is referring to the hierarchy of types derived from another by 
080 extension or restriction.

 refs{  ref{   id{BasicFormOfTerminals   }   
   section{    loc{     from{39     }     
     to{53     }     
    }    
   }   
  }  
 } 
}

Macro equality_test:
 (((symbolic_equality(as_nodeset((arglist.at(0))),as_nodeset((arglist.at(1)))).diff).equal).content()) 
 exegesis{
  📎 __1__2__ex_1
  witness_ref{id(__1__2)
lines((72 .. 74))
  }  
For UTF-8 this means the 'usual' ordering, i.e. the lexicographic order as induced by the '<'-relation on bytes. 
    No locale aware collation (see https://unicode.org/reports/tr10/).
 }
 exegesis{
  📎 __1__2__ex_2
  witness_ref{id(__1__2)
lines((33 .. 37))
  }  
 }
 
 Macro  qnames_equivalent:
  equality_test{
   a{((((arglist.qname).at(0)).content()).uri)((((arglist.qname).at(0)).content()).local_name)   }   a{((((arglist.qname).at(1)).content()).uri)((((arglist.qname).at(1)).content()).local_name)   }  }
  
  fact{
1  }
  fact{
1  }
  non_fact{
0  }
  example{
   📎 EXI knows Right Regular grammars only
   Grammar{    lhs{NonTerminal_1    }    
    rhs{Terminal_1
NonTerminal_1
EventCode(1)
    }    
    rhs{Terminal_2
NonTerminal_2
EventCode(2)
    }    
    rhs{Terminal_3
NonTerminal_3
EventCode(3)
    }    
    rhs{Terminal_n
NonTerminal_n
EventCode(n)
    }    
   }   
  }
  📎 Concept: Grammar_EachLHSContainsExactlyOneNonTerminal
  
  witness_ref{
id(__1__2)
line(13)
  }
  
  Macro   CheckEXIConcept_Grammar_EachLHSContainsExactlyOneNonTerminal:
   violation := 0
   for each e in ((arglist.Grammar).rhs)
    if (((e.contains_symbol("GrammarNonterminal")).size()) == 0):
     violation
← 1
     
    !violation    
    📎 Example 1 (Grammar_EachLHSContainsExactlyOneNonTerminal)
    
Example of a grammar not satisfying EXIConcept_Grammar_EachLHSContainsExactlyOneNonTerminal.    
    Grammar{
     lhs{LeftHandSide     }     
     rhs{Terminal_1     }     
    }
0    
    tests{
    }