src/Pure/ML/ml_syntax.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 65933 f3e4f9e6c485
child 69207 ae2074acbaa8
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Pure/ML/ml_syntax.ML
     2     Author:     Makarius
     3 
     4 Concrete ML syntax for basic values.
     5 *)
     6 
     7 signature ML_SYNTAX =
     8 sig
     9   val reserved_names: string list
    10   val reserved: Name.context
    11   val is_reserved: string -> bool
    12   val is_identifier: string -> bool
    13   val atomic: string -> string
    14   val print_int: int -> string
    15   val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
    16   val print_list: ('a -> string) -> 'a list -> string
    17   val print_option: ('a -> string) -> 'a option -> string
    18   val print_char: string -> string
    19   val print_string: string -> string
    20   val print_strings: string list -> string
    21   val print_properties: Properties.T -> string
    22   val print_position: Position.T -> string
    23   val print_range: Position.range -> string
    24   val make_binding: string * Position.T -> string
    25   val print_indexname: indexname -> string
    26   val print_class: class -> string
    27   val print_sort: sort -> string
    28   val print_typ: typ -> string
    29   val print_term: term -> string
    30   val pretty_string: int -> string -> Pretty.T
    31 end;
    32 
    33 structure ML_Syntax: ML_SYNTAX =
    34 struct
    35 
    36 (* reserved words *)
    37 
    38 val reserved_names = filter Symbol.is_ascii_identifier ML_Lex.keywords;
    39 val reserved = Name.make_context reserved_names;
    40 val is_reserved = Name.is_declared reserved;
    41 
    42 
    43 (* identifiers *)
    44 
    45 fun is_identifier name =
    46   not (is_reserved name) andalso Symbol.is_ascii_identifier name;
    47 
    48 
    49 (* literal output -- unformatted *)
    50 
    51 val atomic = enclose "(" ")";
    52 
    53 val print_int = string_of_int;
    54 
    55 fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
    56 
    57 fun print_list f = enclose "[" "]" o commas o map f;
    58 
    59 fun print_option f NONE = "NONE"
    60   | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
    61 
    62 fun print_chr s =
    63   if Symbol.is_char s then
    64     (case ord s of
    65       34 => "\\\""
    66     | 92 => "\\\\"
    67     | 7 => "\\a"
    68     | 8 => "\\b"
    69     | 9 => "\\t"
    70     | 10 => "\\n"
    71     | 11 => "\\v"
    72     | 12 => "\\f"
    73     | 13 => "\\r"
    74     | c =>
    75         if c < 32 then "\\^" ^ chr (c + 64)
    76         else if c < 127 then s
    77         else "\\" ^ string_of_int c)
    78   else error ("Bad character: " ^ quote s);
    79 
    80 fun print_char s =
    81   if Symbol.is_char s then print_chr s
    82   else if Symbol.is_utf8 s then translate_string print_chr s
    83   else s;
    84 
    85 val print_string = quote o implode o map print_char o Symbol.explode;
    86 val print_strings = print_list print_string;
    87 
    88 val print_properties = print_list (print_pair print_string print_string);
    89 
    90 fun print_position pos =
    91   "Position.of_properties " ^ print_properties (Position.properties_of pos);
    92 
    93 fun print_range range =
    94   "Position.range_of_properties " ^ print_properties (Position.properties_of_range range);
    95 
    96 fun make_binding (name, pos) =
    97   "Binding.make " ^ print_pair print_string print_position (name, pos);
    98 
    99 val print_indexname = print_pair print_string print_int;
   100 
   101 val print_class = print_string;
   102 val print_sort = print_list print_class;
   103 
   104 fun print_typ (Type arg) = "Term.Type " ^ print_pair print_string (print_list print_typ) arg
   105   | print_typ (TFree arg) = "Term.TFree " ^ print_pair print_string print_sort arg
   106   | print_typ (TVar arg) = "Term.TVar " ^ print_pair print_indexname print_sort arg;
   107 
   108 fun print_term (Const arg) = "Term.Const " ^ print_pair print_string print_typ arg
   109   | print_term (Free arg) = "Term.Free " ^ print_pair print_string print_typ arg
   110   | print_term (Var arg) = "Term.Var " ^ print_pair print_indexname print_typ arg
   111   | print_term (Bound i) = "Term.Bound " ^ print_int i
   112   | print_term (Abs (s, T, t)) =
   113       "Term.Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
   114   | print_term (t1 $ t2) = "Term.$ " ^ print_pair print_term print_term (t1, t2);
   115 
   116 
   117 (* toplevel pretty printing *)
   118 
   119 fun pretty_string max_len str =
   120   let
   121     val body =
   122       maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str)
   123         handle Fail _ => Symbol.explode str;
   124     val body' =
   125       if length body <= max_len then body
   126       else take (Int.max (max_len, 0)) body @ ["..."];
   127   in Pretty.str (quote (implode (map print_char body'))) end;
   128 
   129 val _ =
   130   ML_system_pp (fn depth => fn _ => fn str =>
   131     Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
   132 
   133 end;