src/Pure/ML/ml_syntax.ML
author wenzelm
Fri Nov 19 23:48:07 2010 +0100 (2010-11-19)
changeset 40626 d86540f6ea0d
parent 39514 d9cf3f833318
child 41415 23533273220a
permissions -rw-r--r--
total Symbol.explode (cf. 1050315f6ee2);
wenzelm@24582
     1
(*  Title:      Pure/ML/ml_syntax.ML
wenzelm@24574
     2
    Author:     Makarius
wenzelm@24574
     3
wenzelm@24574
     4
Basic ML syntax operations.
wenzelm@24574
     5
*)
wenzelm@24574
     6
wenzelm@24574
     7
signature ML_SYNTAX =
wenzelm@24574
     8
sig
wenzelm@24574
     9
  val reserved_names: string list
wenzelm@24574
    10
  val reserved: Name.context
wenzelm@24574
    11
  val is_reserved: string -> bool
wenzelm@24574
    12
  val is_identifier: string -> bool
wenzelm@24574
    13
  val atomic: string -> string
wenzelm@24574
    14
  val print_int: int -> string
wenzelm@24574
    15
  val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
wenzelm@24574
    16
  val print_list: ('a -> string) -> 'a list -> string
wenzelm@24574
    17
  val print_option: ('a -> string) -> 'a option -> string
wenzelm@24574
    18
  val print_char: string -> string
wenzelm@24574
    19
  val print_string: string -> string
wenzelm@24574
    20
  val print_strings: string list -> string
wenzelm@30230
    21
  val print_properties: Properties.T -> string
wenzelm@30230
    22
  val print_position: Position.T -> string
wenzelm@30523
    23
  val make_binding: string * Position.T -> string
wenzelm@24574
    24
  val print_indexname: indexname -> string
wenzelm@24574
    25
  val print_class: class -> string
wenzelm@24574
    26
  val print_sort: sort -> string
wenzelm@24574
    27
  val print_typ: typ -> string
wenzelm@24574
    28
  val print_term: term -> string
wenzelm@37535
    29
  val pretty_string: string -> Pretty.T
wenzelm@24574
    30
end;
wenzelm@24574
    31
wenzelm@24574
    32
structure ML_Syntax: ML_SYNTAX =
wenzelm@24574
    33
struct
wenzelm@24574
    34
wenzelm@24574
    35
(* reserved words *)
wenzelm@24574
    36
wenzelm@24582
    37
val reserved_names = filter Syntax.is_ascii_identifier ML_Lex.keywords;
wenzelm@24574
    38
val reserved = Name.make_context reserved_names;
wenzelm@24574
    39
val is_reserved = Name.is_declared reserved;
wenzelm@24574
    40
wenzelm@24574
    41
wenzelm@24574
    42
(* identifiers *)
wenzelm@24574
    43
wenzelm@24574
    44
fun is_identifier name =
wenzelm@24574
    45
  not (is_reserved name) andalso Syntax.is_ascii_identifier name;
wenzelm@24574
    46
wenzelm@24574
    47
wenzelm@24574
    48
(* literal output -- unformatted *)
wenzelm@24574
    49
wenzelm@24574
    50
val atomic = enclose "(" ")";
wenzelm@24574
    51
wenzelm@24574
    52
val print_int = Int.toString;
wenzelm@24574
    53
wenzelm@24574
    54
fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
wenzelm@24574
    55
wenzelm@24574
    56
fun print_list f = enclose "[" "]" o commas o map f;
wenzelm@24574
    57
wenzelm@24574
    58
fun print_option f NONE = "NONE"
wenzelm@24574
    59
  | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
wenzelm@24574
    60
wenzelm@24574
    61
fun print_char s =
wenzelm@31543
    62
  if not (Symbol.is_char s) then s
wenzelm@24574
    63
  else if s = "\"" then "\\\""
wenzelm@24574
    64
  else if s = "\\" then "\\\\"
wenzelm@39514
    65
  else if s = "\t" then "\\t"
wenzelm@39514
    66
  else if s = "\n" then "\\n"
wenzelm@39514
    67
  else if s = "\r" then "\\r"
wenzelm@24574
    68
  else
wenzelm@24574
    69
    let val c = ord s in
wenzelm@24574
    70
      if c < 32 then "\\^" ^ chr (c + ord "@")
wenzelm@24574
    71
      else if c < 127 then s
wenzelm@24574
    72
      else "\\" ^ string_of_int c
wenzelm@24574
    73
    end;
wenzelm@24574
    74
wenzelm@31543
    75
val print_string = quote o implode o map print_char o Symbol.explode;
wenzelm@24574
    76
val print_strings = print_list print_string;
wenzelm@24574
    77
wenzelm@30230
    78
val print_properties = print_list (print_pair print_string print_string);
wenzelm@30230
    79
fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
wenzelm@30523
    80
fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos);
wenzelm@30230
    81
wenzelm@24574
    82
val print_indexname = print_pair print_string print_int;
wenzelm@24574
    83
wenzelm@24574
    84
val print_class = print_string;
wenzelm@24574
    85
val print_sort = print_list print_class;
wenzelm@24574
    86
wenzelm@24574
    87
fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg
wenzelm@24574
    88
  | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg
wenzelm@24574
    89
  | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg;
wenzelm@24574
    90
wenzelm@24574
    91
fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg
wenzelm@24574
    92
  | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg
wenzelm@24574
    93
  | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg
wenzelm@24574
    94
  | print_term (Bound i) = "Bound " ^ print_int i
wenzelm@24574
    95
  | print_term (Abs (s, T, t)) =
wenzelm@24574
    96
      "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
wenzelm@24574
    97
  | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
wenzelm@24574
    98
wenzelm@37535
    99
wenzelm@37535
   100
(* toplevel pretty printing *)
wenzelm@37535
   101
wenzelm@37535
   102
fun pretty_string raw_str =
wenzelm@37535
   103
  let
wenzelm@37535
   104
    val str =
wenzelm@37535
   105
      implode (map (fn XML.Elem _ => "<markup>" | XML.Text s => s) (YXML.parse_body raw_str))
wenzelm@37535
   106
        handle Fail _ => raw_str;
wenzelm@40626
   107
    val syms = Symbol.explode str;
wenzelm@37535
   108
  in Pretty.str (quote (implode (map print_char syms))) end;
wenzelm@37535
   109
wenzelm@24574
   110
end;