src/Pure/ML/ml_syntax.ML
author wenzelm
Fri, 14 Sep 2007 17:02:34 +0200
changeset 24574 e840872e9c7c
child 24582 57599da58045
permissions -rw-r--r--
moved ML_XXX.ML files to Pure/ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24574
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/ml_syntax.ML
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     4
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     5
Basic ML syntax operations.
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
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     8
signature ML_SYNTAX =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
     9
sig
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    10
  val reserved_names: string list
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    11
  val reserved: Name.context
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    12
  val is_reserved: string -> bool
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    13
  val is_identifier: string -> bool
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    14
  val atomic: string -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    15
  val print_int: int -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    16
  val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    17
  val print_list: ('a -> string) -> 'a list -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    18
  val print_option: ('a -> string) -> 'a option -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    19
  val print_char: string -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    20
  val print_string: string -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    21
  val print_strings: string list -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    22
  val print_indexname: indexname -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    23
  val print_class: class -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    24
  val print_sort: sort -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    25
  val print_typ: typ -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    26
  val print_term: term -> string
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    27
end;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    28
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    29
structure ML_Syntax: ML_SYNTAX =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    30
struct
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    31
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    32
(* reserved words *)
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    33
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    34
val reserved_names =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    35
 ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    36
  "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    37
  "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    38
  "raise", "rec", "then", "type", "val", "with", "withtype", "while",
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    39
  "eqtype", "functor", "include", "sharing", "sig", "signature",
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    40
  "struct", "structure", "where"];
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
val reserved = Name.make_context reserved_names;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    43
val is_reserved = Name.is_declared reserved;
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
(* identifiers *)
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
fun is_identifier name =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    49
  not (is_reserved name) andalso Syntax.is_ascii_identifier name;
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
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    52
(* literal output -- unformatted *)
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
val atomic = enclose "(" ")";
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
val print_int = Int.toString;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    57
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    58
fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    59
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    60
fun print_list f = enclose "[" "]" o commas o map f;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    61
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    62
fun print_option f NONE = "NONE"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    63
  | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    64
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    65
fun print_char s =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    66
  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
    67
  else if s = "\"" then "\\\""
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    68
  else if s = "\\" then "\\\\"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    69
  else
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    70
    let val c = ord s in
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    71
      if c < 32 then "\\^" ^ chr (c + ord "@")
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    72
      else if c < 127 then s
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    73
      else "\\" ^ string_of_int c
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    74
    end;
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
val print_string = quote o translate_string print_char;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    77
val print_strings = print_list print_string;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    78
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    79
val print_indexname = print_pair print_string print_int;
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
val print_class = print_string;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    82
val print_sort = print_list print_class;
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    83
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    84
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
    85
  | 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
    86
  | 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
    87
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    88
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
    89
  | 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
    90
  | 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
    91
  | print_term (Bound i) = "Bound " ^ print_int i
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    92
  | print_term (Abs (s, T, t)) =
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    93
      "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    94
  | 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
    95
e840872e9c7c moved ML_XXX.ML files to Pure/ML;
wenzelm
parents:
diff changeset
    96
end;