src/Pure/ML/ml_syntax.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24582 57599da58045
child 26362 d9ce159a41d1
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      Pure/ML/ml_syntax.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Basic ML syntax operations.
     6 *)
     7 
     8 signature ML_SYNTAX =
     9 sig
    10   val reserved_names: string list
    11   val reserved: Name.context
    12   val is_reserved: string -> bool
    13   val is_identifier: string -> bool
    14   val atomic: string -> string
    15   val print_int: int -> string
    16   val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
    17   val print_list: ('a -> string) -> 'a list -> string
    18   val print_option: ('a -> string) -> 'a option -> string
    19   val print_char: string -> string
    20   val print_string: string -> string
    21   val print_strings: string list -> string
    22   val print_indexname: indexname -> string
    23   val print_class: class -> string
    24   val print_sort: sort -> string
    25   val print_typ: typ -> string
    26   val print_term: term -> string
    27 end;
    28 
    29 structure ML_Syntax: ML_SYNTAX =
    30 struct
    31 
    32 (* reserved words *)
    33 
    34 val reserved_names = filter Syntax.is_ascii_identifier ML_Lex.keywords;
    35 val reserved = Name.make_context reserved_names;
    36 val is_reserved = Name.is_declared reserved;
    37 
    38 
    39 (* identifiers *)
    40 
    41 fun is_identifier name =
    42   not (is_reserved name) andalso Syntax.is_ascii_identifier name;
    43 
    44 
    45 (* literal output -- unformatted *)
    46 
    47 val atomic = enclose "(" ")";
    48 
    49 val print_int = Int.toString;
    50 
    51 fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
    52 
    53 fun print_list f = enclose "[" "]" o commas o map f;
    54 
    55 fun print_option f NONE = "NONE"
    56   | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
    57 
    58 fun print_char s =
    59   if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s)
    60   else if s = "\"" then "\\\""
    61   else if s = "\\" then "\\\\"
    62   else
    63     let val c = ord s in
    64       if c < 32 then "\\^" ^ chr (c + ord "@")
    65       else if c < 127 then s
    66       else "\\" ^ string_of_int c
    67     end;
    68 
    69 val print_string = quote o translate_string print_char;
    70 val print_strings = print_list print_string;
    71 
    72 val print_indexname = print_pair print_string print_int;
    73 
    74 val print_class = print_string;
    75 val print_sort = print_list print_class;
    76 
    77 fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg
    78   | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg
    79   | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg;
    80 
    81 fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg
    82   | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg
    83   | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg
    84   | print_term (Bound i) = "Bound " ^ print_int i
    85   | print_term (Abs (s, T, t)) =
    86       "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
    87   | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
    88 
    89 end;