384
|
1 |
(* Title: Pure/Syntax/mixfix.ML
|
|
2 |
ID: $Id$
|
551
|
3 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
|
384
|
4 |
|
|
5 |
Mixfix declarations, infixes, binders. Part of the Pure syntax.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature MIXFIX0 =
|
|
9 |
sig
|
|
10 |
datatype mixfix =
|
|
11 |
NoSyn |
|
|
12 |
Mixfix of string * int list * int |
|
|
13 |
Delimfix of string |
|
|
14 |
Infixl of int |
|
|
15 |
Infixr of int |
|
|
16 |
Binder of string * int
|
|
17 |
val max_pri: int
|
|
18 |
end;
|
|
19 |
|
|
20 |
signature MIXFIX1 =
|
|
21 |
sig
|
|
22 |
include MIXFIX0
|
|
23 |
val type_name: string -> mixfix -> string
|
|
24 |
val const_name: string -> mixfix -> string
|
|
25 |
val pure_types: (string * int * mixfix) list
|
|
26 |
val pure_syntax: (string * string * mixfix) list
|
|
27 |
end;
|
|
28 |
|
|
29 |
signature MIXFIX =
|
|
30 |
sig
|
|
31 |
include MIXFIX1
|
|
32 |
structure SynExt: SYN_EXT
|
|
33 |
local open SynExt in
|
|
34 |
val syn_ext_types: string list -> (string * int * mixfix) list -> syn_ext
|
|
35 |
val syn_ext_consts: string list -> (string * typ * mixfix) list -> syn_ext
|
|
36 |
end
|
|
37 |
end;
|
|
38 |
|
|
39 |
functor MixfixFun(structure Lexicon: LEXICON and SynExt: SYN_EXT
|
551
|
40 |
and SynTrans: SYN_TRANS): MIXFIX =
|
384
|
41 |
struct
|
|
42 |
|
|
43 |
structure SynExt = SynExt;
|
551
|
44 |
open Lexicon SynExt SynExt.Ast SynTrans;
|
384
|
45 |
|
|
46 |
|
|
47 |
(** mixfix declarations **)
|
|
48 |
|
|
49 |
datatype mixfix =
|
|
50 |
NoSyn |
|
|
51 |
Mixfix of string * int list * int |
|
|
52 |
Delimfix of string |
|
|
53 |
Infixl of int |
|
|
54 |
Infixr of int |
|
|
55 |
Binder of string * int;
|
|
56 |
|
|
57 |
|
|
58 |
(* type / const names *)
|
|
59 |
|
|
60 |
fun strip ("'" :: c :: cs) = c :: strip cs
|
|
61 |
| strip ["'"] = []
|
|
62 |
| strip (c :: cs) = c :: strip cs
|
|
63 |
| strip [] = [];
|
|
64 |
|
|
65 |
val strip_esc = implode o strip o explode;
|
|
66 |
|
|
67 |
|
|
68 |
fun type_name t (Infixl _) = strip_esc t
|
|
69 |
| type_name t (Infixr _) = strip_esc t
|
|
70 |
| type_name t _ = t;
|
|
71 |
|
|
72 |
fun infix_name c = "op " ^ strip_esc c;
|
|
73 |
|
|
74 |
fun const_name c (Infixl _) = infix_name c
|
|
75 |
| const_name c (Infixr _) = infix_name c
|
|
76 |
| const_name c _ = c;
|
|
77 |
|
|
78 |
|
|
79 |
(* syn_ext_types *)
|
|
80 |
|
|
81 |
fun syn_ext_types all_roots type_decls =
|
|
82 |
let
|
|
83 |
fun name_of (t, _, mx) = type_name t mx;
|
|
84 |
|
|
85 |
fun mk_infix t p1 p2 p3 =
|
|
86 |
Mfix ("(_ " ^ t ^ "/ _)", [typeT, typeT] ---> typeT,
|
|
87 |
strip_esc t, [p1, p2], p3);
|
|
88 |
|
|
89 |
fun mfix_of (_, _, NoSyn) = None
|
|
90 |
| mfix_of (t, 2, Infixl p) = Some (mk_infix t p (p + 1) p)
|
|
91 |
| mfix_of (t, 2, Infixr p) = Some (mk_infix t (p + 1) p p)
|
|
92 |
| mfix_of decl = error ("Bad mixfix declaration for type " ^
|
|
93 |
quote (name_of decl));
|
|
94 |
|
|
95 |
val mfix = mapfilter mfix_of type_decls;
|
|
96 |
val xconsts = map name_of type_decls;
|
|
97 |
in
|
|
98 |
syn_ext all_roots [] mfix xconsts ([], [], [], []) ([], [])
|
|
99 |
end;
|
|
100 |
|
|
101 |
|
|
102 |
(* syn_ext_consts *)
|
|
103 |
|
|
104 |
fun syn_ext_consts all_roots const_decls =
|
|
105 |
let
|
|
106 |
fun name_of (c, _, mx) = const_name c mx;
|
|
107 |
|
|
108 |
fun mk_infix sy ty c p1 p2 p3 =
|
|
109 |
[Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3),
|
|
110 |
Mfix ("op " ^ sy, ty, c, [], max_pri)];
|
|
111 |
|
|
112 |
fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
|
|
113 |
[Type ("idts", []), ty2] ---> ty3
|
|
114 |
| binder_typ c _ = error ("Bad type of binder " ^ quote c);
|
|
115 |
|
|
116 |
fun mfix_of (_, _, NoSyn) = []
|
|
117 |
| mfix_of (c, ty, Mixfix (sy, ps, p)) = [Mfix (sy, ty, c, ps, p)]
|
|
118 |
| mfix_of (c, ty, Delimfix sy) = [Mfix (sy, ty, c, [], max_pri)]
|
|
119 |
| mfix_of (sy, ty, Infixl p) = mk_infix sy ty (infix_name sy) p (p + 1) p
|
|
120 |
| mfix_of (sy, ty, Infixr p) = mk_infix sy ty (infix_name sy) (p + 1) p p
|
|
121 |
| mfix_of (c, ty, Binder (sy, p)) =
|
|
122 |
[Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [], p)];
|
|
123 |
|
|
124 |
fun binder (c, _, Binder (sy, _)) = Some (sy, c)
|
|
125 |
| binder _ = None;
|
|
126 |
|
|
127 |
val mfix = flat (map mfix_of const_decls);
|
|
128 |
val xconsts = map name_of const_decls;
|
|
129 |
val binders = mapfilter binder const_decls;
|
|
130 |
val binder_trs = map mk_binder_tr binders;
|
|
131 |
val binder_trs' = map (mk_binder_tr' o swap) binders;
|
|
132 |
in
|
|
133 |
syn_ext all_roots [] mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
|
|
134 |
end;
|
|
135 |
|
|
136 |
|
|
137 |
|
|
138 |
(** Pure syntax **)
|
|
139 |
|
|
140 |
val pure_types =
|
|
141 |
map (fn t => (t, 0, NoSyn))
|
|
142 |
(terminals @ [logic, "type", "types", "sort", "classes", args, "idt",
|
624
|
143 |
"idts", "aprop", "asms", "any"]);
|
384
|
144 |
|
|
145 |
val pure_syntax =
|
|
146 |
[("_lambda", "[idts, 'a] => ('b => 'a)", Mixfix ("(3%_./ _)", [], 0)),
|
|
147 |
("", "'a => " ^ args, Delimfix "_"),
|
|
148 |
("_args", "['a, " ^ args ^ "] => " ^ args, Delimfix "_,/ _"),
|
|
149 |
("", "id => idt", Delimfix "_"),
|
|
150 |
("_idtyp", "[id, type] => idt", Mixfix ("_::_", [], 0)),
|
|
151 |
("", "idt => idt", Delimfix "'(_')"),
|
|
152 |
("", "idt => idts", Delimfix "_"),
|
|
153 |
("_idts", "[idt, idts] => idts", Mixfix ("_/ _", [1, 0], 0)),
|
|
154 |
("", "id => aprop", Delimfix "_"),
|
|
155 |
("", "var => aprop", Delimfix "_"),
|
|
156 |
(applC, "[('b => 'a), " ^ args ^ "] => aprop",
|
|
157 |
Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)),
|
|
158 |
("_aprop", "aprop => prop", Delimfix "PROP _"),
|
|
159 |
("", "prop => asms", Delimfix "_"),
|
|
160 |
("_asms", "[prop, asms] => asms", Delimfix "_;/ _"),
|
|
161 |
("_bigimpl", "[asms, prop] => prop", Mixfix ("((3[| _ |]) ==>/ _)", [0, 1], 1)),
|
472
|
162 |
("_ofclass", "[type, 'a] => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"),
|
384
|
163 |
("_K", "'a", NoSyn),
|
|
164 |
("_explode", "'a", NoSyn),
|
624
|
165 |
("_implode", "'a", NoSyn),
|
|
166 |
("", "id => logic", Delimfix "_"),
|
|
167 |
("", "var => logic", Delimfix "_"),
|
|
168 |
("_appl", "[logic, args] => logic", Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)),
|
|
169 |
("_constrain", "[logic, type] => logic", Mixfix ("_::_", [max_pri, 0], 999))]
|
384
|
170 |
|
|
171 |
end;
|