src/Pure/ML/ml_syntax.ML
author wenzelm
Wed, 21 Jan 2009 23:21:44 +0100
changeset 29606 fedb8be05f24
parent 26373 b615c10404bf
child 30230 a2094a8c1672
permissions -rw-r--r--
removed Ids;
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
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    21
  val print_indexname: indexname -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    22
  val print_class: class -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    23
  val print_sort: sort -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    24
  val print_typ: typ -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    25
  val print_term: term -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    26
end;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    27
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    28
structure ML_Syntax: ML_SYNTAX =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    29
struct
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    30
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    31
(* reserved words *)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    32
24582
57599da58045 ML_Lex.keywords;
wenzelm
parents: 24574
diff changeset
    33
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
    34
val reserved = Name.make_context reserved_names;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    35
val is_reserved = Name.is_declared reserved;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    36
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    37
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    38
(* identifiers *)
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
fun is_identifier name =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    41
  not (is_reserved name) andalso Syntax.is_ascii_identifier name;
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
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    44
(* literal output -- unformatted *)
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
val atomic = enclose "(" ")";
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 print_int = Int.toString;
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
fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
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_list f = enclose "[" "]" o commas o map f;
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_option f NONE = "NONE"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    55
  | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
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_char s =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    58
  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
    59
  else if s = "\"" then "\\\""
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    60
  else if s = "\\" then "\\\\"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    61
  else
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    62
    let val c = ord s in
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    63
      if c < 32 then "\\^" ^ chr (c + ord "@")
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    64
      else if c < 127 then s
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    65
      else "\\" ^ string_of_int c
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    66
    end;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    67
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    68
val print_string = quote o translate_string print_char;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    69
val print_strings = print_list print_string;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    70
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    71
val print_indexname = print_pair print_string print_int;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    72
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    73
val print_class = print_string;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    74
val print_sort = print_list print_class;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    75
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    76
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
    77
  | 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
    78
  | 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
    79
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    80
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
    81
  | 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
    82
  | 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
    83
  | print_term (Bound i) = "Bound " ^ print_int i
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    84
  | print_term (Abs (s, T, t)) =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    85
      "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    86
  | 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
    87
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    88
end;