|
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 |
|
10 val reserved_names: string list |
|
11 val reserved: Name.context |
|
12 val is_reserved: string -> bool |
|
13 val is_identifier: string -> bool |
|
14 val atomic: string -> string |
|
15 val print_int: int -> string |
|
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 |
|
21 val print_strings: string list -> string |
|
22 val print_indexname: indexname -> string |
|
23 val print_class: class -> string |
|
24 val print_sort: sort -> string |
|
25 val print_typ: typ -> string |
|
26 val print_term: term -> string |
|
27 end; |
|
28 |
|
29 structure ML_Syntax: ML_SYNTAX = |
|
30 struct |
|
31 |
|
32 (* reserved words *) |
|
33 |
|
34 val reserved_names = |
|
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 |
|
42 val reserved = Name.make_context reserved_names; |
|
43 val is_reserved = Name.is_declared reserved; |
|
44 |
|
45 |
|
46 (* identifiers *) |
|
47 |
|
48 fun is_identifier name = |
|
49 not (is_reserved name) andalso Syntax.is_ascii_identifier name; |
|
50 |
|
51 |
|
52 (* literal output -- unformatted *) |
|
53 |
|
54 val atomic = enclose "(" ")"; |
|
55 |
|
56 val print_int = Int.toString; |
|
57 |
|
58 fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")"; |
|
59 |
|
60 fun print_list f = enclose "[" "]" o commas o map f; |
|
61 |
|
62 fun print_option f NONE = "NONE" |
|
63 | print_option f (SOME x) = "SOME (" ^ f x ^ ")"; |
|
64 |
|
65 fun print_char s = |
|
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; |
|
75 |
|
76 val print_string = quote o translate_string print_char; |
|
77 val print_strings = print_list print_string; |
|
78 |
|
79 val print_indexname = print_pair print_string print_int; |
|
80 |
|
81 val print_class = print_string; |
|
82 val print_sort = print_list print_class; |
|
83 |
|
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 |
|
86 | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg; |
|
87 |
|
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 |
|
90 | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg |
|
91 | print_term (Bound i) = "Bound " ^ print_int i |
|
92 | print_term (Abs (s, T, t)) = |
|
93 "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")" |
|
94 | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2); |
|
95 |
|
96 end; |