src/Pure/ML/ml_syntax.ML
author wenzelm
Tue, 03 Mar 2009 21:48:40 +0100
changeset 30230 a2094a8c1672
parent 29606 fedb8be05f24
child 30523 4007ea1ddac2
permissions -rw-r--r--
added print_properties, print_position (again);
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
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     4
Basic ML syntax operations.
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
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    23
  val print_indexname: indexname -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    24
  val print_class: class -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    25
  val print_sort: sort -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    26
  val print_typ: typ -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    27
  val print_term: term -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    28
end;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    29
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    30
structure ML_Syntax: ML_SYNTAX =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    31
struct
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
(* reserved words *)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    34
24582
57599da58045 ML_Lex.keywords;
wenzelm
parents: 24574
diff changeset
    35
val reserved_names = filter Syntax.is_ascii_identifier ML_Lex.keywords;
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    36
val reserved = Name.make_context reserved_names;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    37
val is_reserved = Name.is_declared reserved;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    38
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    39
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    40
(* identifiers *)
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
fun is_identifier name =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    43
  not (is_reserved name) andalso Syntax.is_ascii_identifier name;
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
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    46
(* literal output -- unformatted *)
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
val atomic = enclose "(" ")";
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    49
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    50
val print_int = Int.toString;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    51
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    52
fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    53
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    54
fun print_list f = enclose "[" "]" o commas o map f;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    55
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    56
fun print_option f NONE = "NONE"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    57
  | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
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_char s =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    60
  if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    61
  else if s = "\"" then "\\\""
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    62
  else if s = "\\" then "\\\\"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    63
  else
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    64
    let val c = ord s in
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    65
      if c < 32 then "\\^" ^ chr (c + ord "@")
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    66
      else if c < 127 then s
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    67
      else "\\" ^ string_of_int c
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    68
    end;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    69
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    70
val print_string = quote o translate_string print_char;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    71
val print_strings = print_list print_string;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    72
30230
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    73
val print_properties = print_list (print_pair print_string print_string);
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    74
fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
a2094a8c1672 added print_properties, print_position (again);
wenzelm
parents: 29606
diff changeset
    75
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    76
val print_indexname = print_pair print_string print_int;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    77
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    78
val print_class = print_string;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    79
val print_sort = print_list print_class;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    80
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    81
fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    82
  | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    83
  | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    84
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    85
fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    86
  | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    87
  | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    88
  | print_term (Bound i) = "Bound " ^ print_int i
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    89
  | print_term (Abs (s, T, t)) =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    90
      "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    91
  | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    92
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    93
end;