src/Pure/Syntax/syntax.ML
changeset 4618 731bed12f762
parent 4496 16187138463d
child 4703 a50ab39756db
equal deleted inserted replaced
4617:cea2a5b5ee10 4618:731bed12f762
    38     (string * (ast list -> ast)) list -> syntax
    38     (string * (ast list -> ast)) list -> syntax
    39   val extend_trfunsT: syntax -> (string * (bool -> typ -> term list -> term)) list -> syntax
    39   val extend_trfunsT: syntax -> (string * (bool -> typ -> term list -> term)) list -> syntax
    40   val extend_tokentrfuns: syntax -> (string * string * (string -> string * int)) list -> syntax
    40   val extend_tokentrfuns: syntax -> (string * string * (string -> string * int)) list -> syntax
    41   val extend_trrules: syntax -> (string * string) trrule list -> syntax
    41   val extend_trrules: syntax -> (string * string) trrule list -> syntax
    42   val extend_trrules_i: syntax -> ast trrule list -> syntax
    42   val extend_trrules_i: syntax -> ast trrule list -> syntax
       
    43   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
    43   val merge_syntaxes: syntax -> syntax -> syntax
    44   val merge_syntaxes: syntax -> syntax -> syntax
    44   val type_syn: syntax
    45   val type_syn: syntax
    45   val pure_syn: syntax
    46   val pure_syn: syntax
    46   val print_gram: syntax -> unit
    47   val print_gram: syntax -> unit
    47   val print_trans: syntax -> unit
    48   val print_trans: syntax -> unit
   395 datatype 'a trrule =
   396 datatype 'a trrule =
   396   ParseRule of 'a * 'a |
   397   ParseRule of 'a * 'a |
   397   PrintRule of 'a * 'a |
   398   PrintRule of 'a * 'a |
   398   ParsePrintRule of 'a * 'a;
   399   ParsePrintRule of 'a * 'a;
   399 
   400 
   400 fun map_rule f (ParseRule (x, y)) = ParseRule (f x, f y)
   401 fun map_trrule f (ParseRule (x, y)) = ParseRule (f x, f y)
   401   | map_rule f (PrintRule (x, y)) = PrintRule (f x, f y)
   402   | map_trrule f (PrintRule (x, y)) = PrintRule (f x, f y)
   402   | map_rule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
   403   | map_trrule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
   403 
   404 
   404 fun parse_rule (ParseRule pats) = Some pats
   405 fun parse_rule (ParseRule pats) = Some pats
   405   | parse_rule (PrintRule _) = None
   406   | parse_rule (PrintRule _) = None
   406   | parse_rule (ParsePrintRule pats) = Some pats;
   407   | parse_rule (ParsePrintRule pats) = Some pats;
   407 
   408 
   435     error ("The error(s) above occurred in translation pattern " ^
   436     error ("The error(s) above occurred in translation pattern " ^
   436       quote str);
   437       quote str);
   437 
   438 
   438 
   439 
   439 fun prep_rules rd_pat raw_rules =
   440 fun prep_rules rd_pat raw_rules =
   440   let val rules = map (map_rule rd_pat) raw_rules in
   441   let val rules = map (map_trrule rd_pat) raw_rules in
   441     (map check_rule (mapfilter parse_rule rules),
   442     (map check_rule (mapfilter parse_rule rules),
   442       map check_rule (mapfilter print_rule rules))
   443       map check_rule (mapfilter print_rule rules))
   443   end
   444   end
   444 
   445 
   445 
   446