src/Pure/ML/ml_syntax.ML
author wenzelm
Fri, 18 Mar 2016 16:26:35 +0100
changeset 62663 bea354f6ff21
parent 62528 c8c532b22947
child 62819 d3ff367a16a0
permissions -rw-r--r--
clarified modules; tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24582
57599da58045 ML_Lex.keywords;
wenzelm
parents: 24574
diff changeset
     1
(*  Title:      Pure/ML/ml_syntax.ML
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     3
62528
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
     4
Concrete ML syntax for basic values.
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     5
*)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     6
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     7
signature ML_SYNTAX =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     8
sig
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     9
  val reserved_names: string list
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    10
  val reserved: Name.context
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    11
  val is_reserved: string -> bool
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    12
  val is_identifier: string -> bool
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    13
  val atomic: string -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    14
  val print_int: int -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    15
  val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    16
  val print_list: ('a -> string) -> 'a list -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    17
  val print_option: ('a -> string) -> 'a option -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    18
  val print_char: string -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    19
  val print_string: string -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    20
  val print_strings: string list -> string
30230
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    21
  val print_properties: Properties.T -> string
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    22
  val print_position: Position.T -> string
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 56184
diff changeset
    23
  val print_range: Position.range -> string
30523
4007ea1ddac2 added make_binding;
wenzelm
parents: 30230
diff changeset
    24
  val make_binding: string * Position.T -> string
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    25
  val print_indexname: indexname -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    26
  val print_class: class -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    27
  val print_sort: sort -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    28
  val print_typ: typ -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    29
  val print_term: term -> string
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
    30
  val pretty_string: int -> string -> Pretty.T
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    31
end;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    32
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    33
structure ML_Syntax: ML_SYNTAX =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    34
struct
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    35
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    36
(* reserved words *)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    37
50238
98d35a7368bd more uniform Symbol.is_ascii_identifier in ML/Scala;
wenzelm
parents: 43845
diff changeset
    38
val reserved_names = filter Symbol.is_ascii_identifier ML_Lex.keywords;
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    39
val reserved = Name.make_context reserved_names;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    40
val is_reserved = Name.is_declared reserved;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    41
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    42
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    43
(* identifiers *)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    44
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    45
fun is_identifier name =
50238
98d35a7368bd more uniform Symbol.is_ascii_identifier in ML/Scala;
wenzelm
parents: 43845
diff changeset
    46
  not (is_reserved name) andalso Symbol.is_ascii_identifier name;
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    47
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    48
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    49
(* literal output -- unformatted *)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    50
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    51
val atomic = enclose "(" ")";
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    52
41491
a2ad5b824051 eliminated Int.toString;
wenzelm
parents: 41415
diff changeset
    53
val print_int = string_of_int;
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    54
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    55
fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    56
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    57
fun print_list f = enclose "[" "]" o commas o map f;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    58
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    59
fun print_option f NONE = "NONE"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    60
  | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    61
62528
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    62
fun print_chr s =
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    63
  if Symbol.is_char s then
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    64
    (case ord s of
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    65
      34 => "\\\""
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    66
    | 92 => "\\\\"
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    67
    | 9 => "\\t"
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    68
    | 10 => "\\n"
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    69
    | 11 => "\\f"
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    70
    | 13 => "\\r"
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    71
    | c =>
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    72
        if c < 32 then "\\^" ^ chr (c + 64)
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    73
        else if c < 127 then s
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    74
        else "\\" ^ string_of_int c)
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    75
  else error ("Bad character: " ^ quote s);
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    76
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    77
fun print_char s =
62528
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    78
  if Symbol.is_char s then print_chr s
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    79
  else if Symbol.is_utf8 s then translate_string print_chr s
c8c532b22947 clarified ML syntax for strings concerning UTF8;
wenzelm
parents: 58978
diff changeset
    80
  else s;
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    81
31543
5bef6c7cc819 allow Isabelle symbols within low-level ML source;
wenzelm
parents: 30523
diff changeset
    82
val print_string = quote o implode o map print_char o Symbol.explode;
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    83
val print_strings = print_list print_string;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    84
30230
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    85
val print_properties = print_list (print_pair print_string print_string);
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 56184
diff changeset
    86
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 56184
diff changeset
    87
fun print_position pos =
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 56184
diff changeset
    88
  "Position.of_properties " ^ print_properties (Position.properties_of pos);
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 56184
diff changeset
    89
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 56184
diff changeset
    90
fun print_range range =
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 56184
diff changeset
    91
  "Position.range_of_properties " ^ print_properties (Position.properties_of_range range);
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 56184
diff changeset
    92
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 56184
diff changeset
    93
fun make_binding (name, pos) =
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 56184
diff changeset
    94
  "Binding.make " ^ print_pair print_string print_position (name, pos);
30230
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    95
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    96
val print_indexname = print_pair print_string print_int;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    97
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    98
val print_class = print_string;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    99
val print_sort = print_list print_class;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
   100
56184
a2bd40830593 more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents: 50238
diff changeset
   101
fun print_typ (Type arg) = "Term.Type " ^ print_pair print_string (print_list print_typ) arg
a2bd40830593 more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents: 50238
diff changeset
   102
  | print_typ (TFree arg) = "Term.TFree " ^ print_pair print_string print_sort arg
a2bd40830593 more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents: 50238
diff changeset
   103
  | print_typ (TVar arg) = "Term.TVar " ^ print_pair print_indexname print_sort arg;
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
   104
56184
a2bd40830593 more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents: 50238
diff changeset
   105
fun print_term (Const arg) = "Term.Const " ^ print_pair print_string print_typ arg
a2bd40830593 more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents: 50238
diff changeset
   106
  | print_term (Free arg) = "Term.Free " ^ print_pair print_string print_typ arg
a2bd40830593 more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents: 50238
diff changeset
   107
  | print_term (Var arg) = "Term.Var " ^ print_pair print_indexname print_typ arg
a2bd40830593 more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents: 50238
diff changeset
   108
  | print_term (Bound i) = "Term.Bound " ^ print_int i
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
   109
  | print_term (Abs (s, T, t)) =
56184
a2bd40830593 more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents: 50238
diff changeset
   110
      "Term.Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
a2bd40830593 more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
wenzelm
parents: 50238
diff changeset
   111
  | print_term (t1 $ t2) = "Term.$ " ^ print_pair print_term print_term (t1, t2);
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
   112
37535
75de61a479e3 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents: 31543
diff changeset
   113
75de61a479e3 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents: 31543
diff changeset
   114
(* toplevel pretty printing *)
75de61a479e3 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents: 31543
diff changeset
   115
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   116
fun pretty_string max_len str =
37535
75de61a479e3 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents: 31543
diff changeset
   117
  let
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   118
    val body =
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   119
      maps (fn XML.Elem _ => ["<markup>"] | XML.Text s => Symbol.explode s) (YXML.parse_body str)
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   120
        handle Fail _ => Symbol.explode str;
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   121
    val body' =
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   122
      if length body <= max_len then body
42047
a7a4e04b5386 pretty_string: proper handling of negative max_len;
wenzelm
parents: 41491
diff changeset
   123
      else take (Int.max (max_len, 0)) body @ ["..."];
41415
23533273220a tuned ML toplevel pp for type string: observe depth limit;
wenzelm
parents: 40626
diff changeset
   124
  in Pretty.str (quote (implode (map print_char body'))) end;
37535
75de61a479e3 ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
wenzelm
parents: 31543
diff changeset
   125
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62528
diff changeset
   126
val _ =
bea354f6ff21 clarified modules;
wenzelm
parents: 62528
diff changeset
   127
  PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
bea354f6ff21 clarified modules;
wenzelm
parents: 62528
diff changeset
   128
    Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
bea354f6ff21 clarified modules;
wenzelm
parents: 62528
diff changeset
   129
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
   130
end;