- (return_term loc (Ident (id, None)) : 'l2_pattern))]];
- Grammar.Entry.obj (argument : 'argument Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("IDENT", "");
- Gramext.Stoken ("SYMBOL", "."); Gramext.Sself],
- Gramext.action
- (fun (a : 'argument) _ (id : string) _
- (loc : Lexing.position * Lexing.position) ->
- (EtaArg (Some id, a) : 'argument));
- [Gramext.Stoken ("SYMBOL", "η"); Gramext.Stoken ("SYMBOL", ".");
- Gramext.Sself],
- Gramext.action
- (fun (a : 'argument) _ _
- (loc : Lexing.position * Lexing.position) ->
- (EtaArg (None, a) : 'argument));
- [Gramext.Stoken ("IDENT", "")],
- Gramext.action
- (fun (id : string) (loc : Lexing.position * Lexing.position) ->
- (IdentArg id : 'argument))]];
- Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("SYMBOL", "("); Gramext.Slist1 Gramext.Sself;
- Gramext.Stoken ("SYMBOL", ")")],
- Gramext.action
- (fun _ (terms : 'level3_term list) _
- (loc : Lexing.position * Lexing.position) ->
- (match terms with
- [] -> assert false
- | [term] -> term
- | terms -> ApplPattern terms :
- 'level3_term));
- [Gramext.Snterm
- (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e))],
- Gramext.action
- (fun (a : 'argument) (loc : Lexing.position * Lexing.position) ->
- (ArgPattern a : 'level3_term));
- [Gramext.Stoken ("URI", "")],
- Gramext.action
- (fun (u : string) (loc : Lexing.position * Lexing.position) ->
- (UriPattern u : 'level3_term))]];
- Grammar.Entry.obj (associativity : 'associativity Grammar.Entry.e),
- None,
- [None, None,
- [[Gramext.Stoken ("IDENT", "non");
- Gramext.Stoken ("IDENT", "associative")],
- Gramext.action
- (fun _ _ (loc : Lexing.position * Lexing.position) ->
- (Gramext.NonA : 'associativity));
- [Gramext.Stoken ("IDENT", "right");
- Gramext.Stoken ("IDENT", "associative")],
- Gramext.action
- (fun _ _ (loc : Lexing.position * Lexing.position) ->
- (Gramext.RightA : 'associativity));
- [Gramext.Stoken ("IDENT", "left");
- Gramext.Stoken ("IDENT", "associative")],
- Gramext.action
- (fun _ _ (loc : Lexing.position * Lexing.position) ->
- (Gramext.LeftA : 'associativity))]];
- Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("IDENT", "with");
- Gramext.Stoken ("IDENT", "precedence");
- Gramext.Stoken ("NUMBER", "")],
- Gramext.action
- (fun (n : string) _ _ (loc : Lexing.position * Lexing.position) ->
- (int_of_string n : 'precedence))]];
- Grammar.Entry.obj (notation : 'notation Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Stoken ("IDENT", "notation");
- Gramext.Snterm
- (Grammar.Entry.obj
- (level1_pattern : 'level1_pattern Grammar.Entry.e));
- Gramext.Sopt
- (Gramext.Snterm
- (Grammar.Entry.obj
- (associativity : 'associativity Grammar.Entry.e)));
- Gramext.Sopt
- (Gramext.Snterm
- (Grammar.Entry.obj (precedence : 'precedence Grammar.Entry.e)));
- Gramext.Stoken ("IDENT", "for");
- Gramext.Snterm
- (Grammar.Entry.obj
- (level2_pattern : 'level2_pattern Grammar.Entry.e))],
- Gramext.action
- (fun (p2 : 'level2_pattern) _ (prec : 'precedence option)
- (assoc : 'associativity option) (p1 : 'level1_pattern) _
- (loc : Lexing.position * Lexing.position) ->
- (p1, assoc, prec, p2 : 'notation))]];
- Grammar.Entry.obj (interpretation : 'interpretation Grammar.Entry.e),
- None,
- [None, None,
- [[Gramext.Stoken ("IDENT", "interpretation");
- Gramext.Stoken ("SYMBOL", "");
- Gramext.Slist1
- (Gramext.Snterm
- (Grammar.Entry.obj (argument : 'argument Grammar.Entry.e)));
- Gramext.Stoken ("IDENT", "as");
- Gramext.Snterm
- (Grammar.Entry.obj (level3_term : 'level3_term Grammar.Entry.e))],
- Gramext.action
- (fun (t : 'level3_term) _ (args : 'argument list) (s : string) _
- (loc : Lexing.position * Lexing.position) ->
- (() : 'interpretation))]];
- Grammar.Entry.obj (phrase : 'phrase Grammar.Entry.e), None,
- [None, None,
- [[Gramext.Snterm
- (Grammar.Entry.obj (notation : 'notation Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", ".")],
- Gramext.action
- (fun _ (l1, assoc, prec, l2 : 'notation)
- (loc : Lexing.position * Lexing.position) ->
- (Notation (l1, assoc, prec, l2) : 'phrase));
- [Gramext.Stoken ("IDENT", "print");
- Gramext.Snterm
- (Grammar.Entry.obj
- (level2_pattern : 'level2_pattern Grammar.Entry.e));
- Gramext.Stoken ("SYMBOL", ".")],
- Gramext.action
- (fun _ (p2 : 'level2_pattern) _
- (loc : Lexing.position * Lexing.position) ->
- (Print p2 : 'phrase))]]])