21477
|
1 |
(* Title: Pure/General/ml_syntax.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
|
|
5 |
Basic ML syntax operations.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature ML_SYNTAX =
|
|
9 |
sig
|
21723
|
10 |
val reserved_names: string list
|
|
11 |
val reserved: Name.context
|
21477
|
12 |
val is_reserved: string -> bool
|
|
13 |
val is_identifier: string -> bool
|
22154
|
14 |
val atomic: string -> string
|
|
15 |
val print_int: int -> string
|
21758
|
16 |
val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
|
|
17 |
val print_list: ('a -> string) -> 'a list -> string
|
|
18 |
val print_option: ('a -> string) -> 'a option -> string
|
|
19 |
val print_char: string -> string
|
|
20 |
val print_string: string -> string
|
22238
|
21 |
val print_strings: string list -> string
|
22716
|
22 |
val print_indexname: indexname -> string
|
22030
|
23 |
val print_class: class -> string
|
|
24 |
val print_sort: sort -> string
|
|
25 |
val print_typ: typ -> string
|
|
26 |
val print_term: term -> string
|
21477
|
27 |
end;
|
|
28 |
|
|
29 |
structure ML_Syntax: ML_SYNTAX =
|
|
30 |
struct
|
|
31 |
|
|
32 |
(* reserved words *)
|
|
33 |
|
21723
|
34 |
val reserved_names =
|
21477
|
35 |
["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
|
|
36 |
"end", "exception", "fn", "fun", "handle", "if", "in", "infix",
|
|
37 |
"infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
|
|
38 |
"raise", "rec", "then", "type", "val", "with", "withtype", "while",
|
|
39 |
"eqtype", "functor", "include", "sharing", "sig", "signature",
|
|
40 |
"struct", "structure", "where"];
|
|
41 |
|
21723
|
42 |
val reserved = Name.make_context reserved_names;
|
|
43 |
val is_reserved = Name.is_declared reserved;
|
21477
|
44 |
|
|
45 |
|
|
46 |
(* identifiers *)
|
|
47 |
|
|
48 |
fun is_identifier name =
|
|
49 |
not (is_reserved name) andalso Syntax.is_ascii_identifier name;
|
|
50 |
|
|
51 |
|
22133
|
52 |
(* literal output -- unformatted *)
|
21477
|
53 |
|
22154
|
54 |
val atomic = enclose "(" ")";
|
|
55 |
|
|
56 |
val print_int = Int.toString;
|
|
57 |
|
21758
|
58 |
fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
|
21477
|
59 |
|
21758
|
60 |
fun print_list f = enclose "[" "]" o commas o map f;
|
21477
|
61 |
|
21758
|
62 |
fun print_option f NONE = "NONE"
|
|
63 |
| print_option f (SOME x) = "SOME (" ^ f x ^ ")";
|
21477
|
64 |
|
21758
|
65 |
fun print_char s =
|
21494
|
66 |
if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s)
|
|
67 |
else if s = "\"" then "\\\""
|
|
68 |
else if s = "\\" then "\\\\"
|
|
69 |
else
|
|
70 |
let val c = ord s in
|
|
71 |
if c < 32 then "\\^" ^ chr (c + ord "@")
|
|
72 |
else if c < 127 then s
|
|
73 |
else "\\" ^ string_of_int c
|
|
74 |
end;
|
21477
|
75 |
|
21758
|
76 |
val print_string = quote o translate_string print_char;
|
22238
|
77 |
val print_strings = print_list print_string;
|
21477
|
78 |
|
22716
|
79 |
val print_indexname = print_pair print_string print_int;
|
|
80 |
|
22029
|
81 |
val print_class = print_string;
|
|
82 |
val print_sort = print_list print_class;
|
|
83 |
|
22154
|
84 |
fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg
|
|
85 |
| print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg
|
22716
|
86 |
| print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg;
|
22029
|
87 |
|
22154
|
88 |
fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg
|
|
89 |
| print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg
|
22716
|
90 |
| print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg
|
22154
|
91 |
| print_term (Bound i) = "Bound " ^ print_int i
|
22029
|
92 |
| print_term (Abs (s, T, t)) =
|
22030
|
93 |
"Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
|
22716
|
94 |
| print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
|
22029
|
95 |
|
21477
|
96 |
end;
|