- | Notation of loc * direction option * Ast.term * Gramext.g_assoc *
- int * Ast.term
- (* direction, l1 pattern, associativity, precedence, l2 pattern *)
- | Interpretation of loc *
- string * (string * Ast.argument_pattern list) *
- Ast.cic_appl_pattern
- (* description (i.e. id), symbol, arg pattern, appl pattern *)
-
- | Metadata of loc * metadata
-
- (* DEBUGGING *)
- | Dump of loc (* dump grammar on stdout *)
- (* DEBUGGING *)
- | Render of loc * UriManager.uri (* render library object *)
-
-(* composed magic: term + command magics. No need to change this value *)
-let magic = magic + 10000 * CicNotationPt.magic
-
-let reash_cmd_uris =
- let reash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
- function
- | Default (loc, name, uris) ->
- let uris = List.map reash_uri uris in
- Default (loc, name, uris)
- | Interpretation (loc, dsc, args, cic_appl_pattern) ->
- let rec aux =
- function
- | CicNotationPt.UriPattern uri ->
- CicNotationPt.UriPattern (reash_uri uri)
- | CicNotationPt.ApplPattern args ->
- CicNotationPt.ApplPattern (List.map aux args)
- | CicNotationPt.VarPattern _
- | CicNotationPt.ImplicitPattern as pat -> pat
- in
- let appl_pattern = aux cic_appl_pattern in
- Interpretation (loc, dsc, args, appl_pattern)
- | cmd -> cmd