author  lcp 
Thu, 03 Mar 1994 17:43:14 +0100  
changeset 276  4cf7139e5b7a 
parent 272  0f6270bb9fe9 
child 330  2fda15dd1e0f 
permissions  rwrr 
18  1 
(* Title: Pure/Syntax/sextension.ML 
0  2 
ID: $Id$ 
3 
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen 

4 

165  5 
Syntax extensions (external interface): mixfix declarations, infixes, 
6 
binders, translation rules / functions and the Pure syntax. 

0  7 

8 
TODO: 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

9 
move ast_to_term, pt_to_ast (?) 
0  10 
*) 
11 

12 
infix > < <>; 

13 

14 
signature SEXTENSION0 = 

15 
sig 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

16 
structure Parser: PARSER 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

17 
local open Parser.SynExt.Ast in 
0  18 
datatype mixfix = 
19 
Mixfix of string * string * string * int list * int  

20 
Delimfix of string * string * string  

21 
Infixl of string * string * int  

22 
Infixr of string * string * int  

23 
Binder of string * string * string * int * int  

24 
TInfixl of string * string * int  

25 
TInfixr of string * string * int 

26 
datatype xrule = 

27 
op > of (string * string) * (string * string)  

28 
op < of (string * string) * (string * string)  

29 
op <> of (string * string) * (string * string) 

30 
datatype sext = 

31 
Sext of { 

32 
mixfix: mixfix list, 

33 
parse_translation: (string * (term list > term)) list, 

34 
print_translation: (string * (term list > term)) list}  

35 
NewSext of { 

36 
mixfix: mixfix list, 

37 
xrules: xrule list, 

38 
parse_ast_translation: (string * (ast list > ast)) list, 

39 
parse_translation: (string * (term list > term)) list, 

40 
print_translation: (string * (term list > term)) list, 

41 
print_ast_translation: (string * (ast list > ast)) list} 

42 
val eta_contract: bool ref 

43 
val mk_binder_tr: string * string > string * (term list > term) 

44 
val mk_binder_tr': string * string > string * (term list > term) 

45 
val dependent_tr': string * string > term list > term 

46 
val max_pri: int 

47 
end 

48 
end; 

49 

50 
signature SEXTENSION1 = 

51 
sig 

52 
include SEXTENSION0 

53 
val empty_sext: sext 

54 
val simple_sext: mixfix list > sext 

55 
val constants: sext > (string list * string) list 

56 
val pure_sext: sext 

57 
val syntax_types: string list 

259  58 
val syntax_consts: (string list * string) list 
0  59 
val constrainAbsC: string 
60 
end; 

61 

62 
signature SEXTENSION = 

63 
sig 

64 
include SEXTENSION1 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

65 
local open Parser Parser.SynExt Parser.SynExt.Ast in 
0  66 
val xrules_of: sext > xrule list 
67 
val abs_tr': term > term 

68 
val appl_ast_tr': ast * ast list > ast 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

69 
val syn_ext_of_sext: string list > string list > (string > typ) > sext > syn_ext 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

70 
val pt_to_ast: (string > (ast list > ast) option) > parsetree > ast 
0  71 
val ast_to_term: (string > (term list > term) option) > ast > term 
72 
val apropC: string 

73 
end 

74 
end; 

75 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

76 
functor SExtensionFun(Parser: PARSER): SEXTENSION = 
0  77 
struct 
78 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

79 
structure Parser = Parser; 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

80 
open Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser; 
0  81 

82 

83 
(** datatype sext **) 

84 

85 
datatype mixfix = 

86 
Mixfix of string * string * string * int list * int  

87 
Delimfix of string * string * string  

88 
Infixl of string * string * int  

89 
Infixr of string * string * int  

90 
Binder of string * string * string * int * int  

91 
TInfixl of string * string * int  

92 
TInfixr of string * string * int; 

93 

94 
datatype xrule = 

95 
op > of (string * string) * (string * string)  

96 
op < of (string * string) * (string * string)  

97 
op <> of (string * string) * (string * string); 

98 

99 
datatype sext = 

100 
Sext of { 

101 
mixfix: mixfix list, 

102 
parse_translation: (string * (term list > term)) list, 

103 
print_translation: (string * (term list > term)) list}  

104 
NewSext of { 

105 
mixfix: mixfix list, 

106 
xrules: xrule list, 

107 
parse_ast_translation: (string * (ast list > ast)) list, 

108 
parse_translation: (string * (term list > term)) list, 

109 
print_translation: (string * (term list > term)) list, 

110 
print_ast_translation: (string * (ast list > ast)) list}; 

111 

112 

113 
(* simple_sext *) 

114 

115 
fun simple_sext mixfix = 

116 
Sext {mixfix = mixfix, parse_translation = [], print_translation = []}; 

117 

118 

119 
(* empty_sext *) 

120 

121 
val empty_sext = simple_sext []; 

122 

123 

124 
(* sext_components *) 

125 

126 
fun sext_components (Sext {mixfix, parse_translation, print_translation}) = 

127 
{mixfix = mixfix, 

128 
xrules = [], 

129 
parse_ast_translation = [], 

130 
parse_translation = parse_translation, 

131 
print_translation = print_translation, 

132 
print_ast_translation = []} 

133 
 sext_components (NewSext cmps) = cmps; 

134 

135 

136 
(* mixfix_of *) 

137 

138 
fun mixfix_of (Sext {mixfix, ...}) = mixfix 

139 
 mixfix_of (NewSext {mixfix, ...}) = mixfix; 

140 

141 

142 
(* xrules_of *) 

143 

144 
fun xrules_of (Sext _) = [] 

145 
 xrules_of (NewSext {xrules, ...}) = xrules; 

146 

147 

148 

18  149 
(** parse (ast) translations **) 
0  150 

151 
(* application *) 

152 

153 
fun appl_ast_tr (*"_appl"*) [f, args] = Appl (f :: unfold_ast "_args" args) 

154 
 appl_ast_tr (*"_appl"*) asts = raise_ast "appl_ast_tr" asts; 

155 

156 

157 
(* abstraction *) 

158 

159 
fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty] 

160 
 idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts; 

161 

162 
fun lambda_ast_tr (*"_lambda"*) [idts, body] = 

18  163 
fold_ast_p "_abs" (unfold_ast "_idts" idts, body) 
0  164 
 lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts; 
165 

18  166 
fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body) 
167 
 abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) = 

0  168 
if c = constrainC then 
169 
Const ("_constrainAbs", dummyT) $ absfree (x, T, body) $ tT 

18  170 
else raise_term "abs_tr" ts 
171 
 abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts; 

0  172 

173 

18  174 
(* nondependent abstraction *) 
175 

276  176 
fun k_tr (*"_K"*) [t] = Abs ("uu", dummyT, incr_boundvars 1 t) 
18  177 
 k_tr (*"_K"*) ts = raise_term "k_tr" ts; 
178 

179 

180 
(* binder *) 

0  181 

182 
fun mk_binder_tr (sy, name) = 

183 
let 

184 
val const = Const (name, dummyT); 

185 

186 
fun tr (Free (x, T), t) = const $ absfree (x, T, t) 

187 
 tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t)) 

18  188 
 tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) = 
0  189 
if c = constrainC then 
190 
const $ (Const ("_constrainAbs", dummyT) $ absfree (x, T, t) $ tT) 

18  191 
else raise_term "binder_tr" [t1, t] 
192 
 tr (t1, t2) = raise_term "binder_tr" [t1, t2]; 

0  193 

194 
fun binder_tr (*sy*) [idts, body] = tr (idts, body) 

18  195 
 binder_tr (*sy*) ts = raise_term "binder_tr" ts; 
0  196 
in 
197 
(sy, binder_tr) 

198 
end; 

199 

200 

201 
(* atomic props *) 

202 

18  203 
fun aprop_tr (*"_aprop"*) [t] = 
204 
Const (constrainC, dummyT) $ t $ Free ("prop", dummyT) 

205 
 aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts; 

0  206 

207 

208 
(* meta implication *) 

209 

210 
fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] = 

211 
fold_ast_p "==>" (unfold_ast "_asms" asms, concl) 

212 
 bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts; 

213 

214 

259  215 
(* explode atoms *) 
238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

216 

272  217 
fun explode_tr (*"_explode"*) (ts as [consC, nilC, bit0, bit1, txt]) = 
238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

218 
let 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

219 
fun mk_list [] = nilC 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

220 
 mk_list (t :: ts) = consC $ t $ mk_list ts; 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

221 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

222 
fun encode_bit 0 = bit0 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

223 
 encode_bit 1 = bit1 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

224 
 encode_bit _ = sys_error "encode_bit"; 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

225 

259  226 
fun encode_char c = (* FIXME leading 0s (?) *) 
238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

227 
mk_list (map encode_bit (radixpand (2, (ord c)))); 
272  228 

229 
val str = 

230 
(case txt of 

231 
Free (s, _) => s 

232 
 Const (s, _) => s 

233 
 _ => raise_term "explode_tr" ts); 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

234 
in 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

235 
mk_list (map encode_char (explode str)) 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

236 
end 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

237 
 explode_tr (*"_explode"*) ts = raise_term "explode_tr" ts; 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

238 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

239 

0  240 

18  241 
(** print (ast) translations **) 
0  242 

243 
(* application *) 

244 

245 
fun appl_ast_tr' (f, []) = raise_ast "appl_ast_tr'" [f] 

246 
 appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args]; 

247 

248 

18  249 
(* abstraction *) 
0  250 

251 
fun strip_abss vars_of body_of tm = 

252 
let 

18  253 
fun free (x, _) = Free (x, dummyT); 
254 

0  255 
val vars = vars_of tm; 
256 
val body = body_of tm; 

257 
val rev_new_vars = rename_wrt_term body vars; 

258 
in 

18  259 
(map Free (rev rev_new_vars), subst_bounds (map free rev_new_vars, body)) 
0  260 
end; 
261 

262 
(*do (partial) etacontraction before printing*) 

263 

264 
val eta_contract = ref false; 

265 

266 
fun eta_contr tm = 

267 
let 

268 
fun eta_abs (Abs (a, T, t)) = 

269 
(case eta_abs t of 

18  270 
t' as f $ u => 
0  271 
(case eta_abs u of 
272 
Bound 0 => 

273 
if not (0 mem loose_bnos f) then incr_boundvars ~1 f 

274 
else Abs (a, T, t') 

275 
 _ => Abs (a, T, t')) 

276 
 t' => Abs (a, T, t')) 

277 
 eta_abs t = t; 

278 
in 

279 
if ! eta_contract then eta_abs tm else tm 

280 
end; 

281 

282 

283 
fun abs_tr' tm = 

18  284 
foldr (fn (x, t) => Const ("_abs", dummyT) $ x $ t) 
0  285 
(strip_abss strip_abs_vars strip_abs_body (eta_contr tm)); 
286 

287 

18  288 
fun abs_ast_tr' (*"_abs"*) asts = 
289 
(case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of 

290 
([], _) => raise_ast "abs_ast_tr'" asts 

0  291 
 (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]); 
292 

293 

18  294 
(* binder *) 
0  295 

296 
fun mk_binder_tr' (name, sy) = 

297 
let 

298 
fun mk_idts [] = raise Match (*abort translation*) 

299 
 mk_idts [idt] = idt 

300 
 mk_idts (idt :: idts) = Const ("_idts", dummyT) $ idt $ mk_idts idts; 

301 

302 
fun tr' t = 

303 
let 

304 
val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t; 

305 
in 

306 
Const (sy, dummyT) $ mk_idts xs $ bd 

307 
end; 

308 

309 
fun binder_tr' (*name*) (t :: ts) = 

310 
list_comb (tr' (Const (name, dummyT) $ t), ts) 

311 
 binder_tr' (*name*) [] = raise Match; 

312 
in 

313 
(name, binder_tr') 

314 
end; 

315 

316 

317 
(* idts *) 

318 

319 
fun idts_ast_tr' (*"_idts"*) [Appl [Constant c, x, ty], xs] = 

320 
if c = constrainC then 

321 
Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs] 

322 
else raise Match 

323 
 idts_ast_tr' (*"_idts"*) _ = raise Match; 

324 

325 

326 
(* meta implication *) 

327 

328 
fun impl_ast_tr' (*"==>"*) asts = 

329 
(case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of 

18  330 
(asms as _ :: _ :: _, concl) 
0  331 
=> Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl] 
332 
 _ => raise Match); 

333 

334 

18  335 
(* dependent / nondependent quantifiers *) 
0  336 

18  337 
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = 
0  338 
if 0 mem (loose_bnos B) then 
339 
let val (x', B') = variant_abs (x, dummyT, B); 

18  340 
in list_comb (Const (q, dummyT) $ Free (x', T) $ A $ B', ts) end 
341 
else list_comb (Const (r, dummyT) $ A $ B, ts) 

0  342 
 dependent_tr' _ _ = raise Match; 
343 

344 

259  345 
(* implode atoms *) 
0  346 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

347 
fun implode_ast_tr' (*"_implode"*) (asts as [Constant cons_name, nilC, 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

348 
bit0, bit1, bitss]) = 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

349 
let 
259  350 
fun err () = raise_ast "implode_ast_tr'" asts; 
238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

351 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

352 
fun strip_list lst = 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

353 
let val (xs, y) = unfold_ast_p cons_name lst 
259  354 
in if y = nilC then xs else err () 
238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

355 
end; 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

356 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

357 
fun decode_bit bit = 
259  358 
if bit = bit0 then "0" 
359 
else if bit = bit1 then "1" 

360 
else err (); 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

361 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

362 
fun decode_char bits = 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

363 
chr (#1 (scan_radixint (2, map decode_bit (strip_list bits)))); 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

364 
in 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

365 
Variable (implode (map decode_char (strip_list bitss))) 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

366 
end 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

367 
 implode_ast_tr' (*"_implode"*) asts = raise_ast "implode_ast_tr'" asts; 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

368 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

369 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

370 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

371 
(** syn_ext_of_sext **) 
0  372 

18  373 
fun strip_esc str = 
0  374 
let 
18  375 
fun strip ("'" :: c :: cs) = c :: strip cs 
376 
 strip ["'"] = [] 

377 
 strip (c :: cs) = c :: strip cs 

378 
 strip [] = []; 

0  379 
in 
18  380 
implode (strip (explode str)) 
0  381 
end; 
382 

18  383 
fun infix_name sy = "op " ^ strip_esc sy; 
0  384 

385 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

386 
fun syn_ext_of_sext roots xconsts read_typ sext = 
0  387 
let 
18  388 
val {mixfix, parse_ast_translation, parse_translation, print_translation, 
389 
print_ast_translation, ...} = sext_components sext; 

0  390 

18  391 
val tinfixT = [typeT, typeT] > typeT; 
0  392 

393 
fun binder (Binder (sy, _, name, _, _)) = Some (sy, name) 

394 
 binder _ = None; 

395 

396 
fun binder_typ ty = 

397 
(case read_typ ty of 

398 
Type ("fun", [Type ("fun", [_, T2]), T3]) => 

399 
[Type ("idts", []), T2] > T3 

18  400 
 _ => error ("Illegal binder type " ^ quote ty)); 
0  401 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

402 
fun mk_infix sy ty c p1 p2 p3 = 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

403 
[Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3), 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

404 
Mfix ("op " ^ sy, ty, c, [], max_pri)]; 
18  405 

406 
fun mfix_of (Mixfix (sy, ty, c, ps, p)) = [Mfix (sy, read_typ ty, c, ps, p)] 

0  407 
 mfix_of (Delimfix (sy, ty, c)) = [Mfix (sy, read_typ ty, c, [], max_pri)] 
408 
 mfix_of (Infixl (sy, ty, p)) = 

18  409 
mk_infix sy (read_typ ty) (infix_name sy) p (p + 1) p 
0  410 
 mfix_of (Infixr (sy, ty, p)) = 
18  411 
mk_infix sy (read_typ ty) (infix_name sy) (p + 1) p p 
0  412 
 mfix_of (Binder (sy, ty, _, p, q)) = 
413 
[Mfix ("(3" ^ sy ^ "_./ _)", binder_typ ty, sy, [0, p], q)] 

414 
 mfix_of (TInfixl (s, c, p)) = 

18  415 
[Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p, p + 1], p)] 
0  416 
 mfix_of (TInfixr (s, c, p)) = 
18  417 
[Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p + 1, p], p)]; 
0  418 

419 
val mfix = flat (map mfix_of mixfix); 

18  420 
val binders = mapfilter binder mixfix; 
421 
val bparses = map mk_binder_tr binders; 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

422 
val bprints = map (mk_binder_tr' o swap) binders; 
0  423 
in 
238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

424 
syn_ext roots mfix (distinct (filter is_xid xconsts)) 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

425 
(parse_ast_translation, 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

426 
bparses @ parse_translation, 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

427 
bprints @ print_translation, 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

428 
print_ast_translation) 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

429 
([], []) 
0  430 
end; 
431 

432 

433 

18  434 
(** constants **) 
435 

436 
fun constants sext = 

437 
let 

438 
fun consts (Delimfix (_, ty, c)) = ([c], ty) 

439 
 consts (Mixfix (_, ty, c, _, _)) = ([c], ty) 

440 
 consts (Infixl (c, ty, _)) = ([infix_name c], ty) 

441 
 consts (Infixr (c, ty, _)) = ([infix_name c], ty) 

442 
 consts (Binder (_, ty, c, _, _)) = ([c], ty) 

443 
 consts _ = ([""], ""); (*is filtered out below*) 

444 
in 

445 
distinct (filter_out (fn (l, _) => l = [""]) (map consts (mixfix_of sext))) 

446 
end; 

447 

448 

449 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

450 
(** pt_to_ast **) 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

451 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

452 
fun pt_to_ast trf pt = 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

453 
let 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

454 
fun trans a args = 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

455 
(case trf a of 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

456 
None => mk_appl (Constant a) args 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

457 
 Some f => f args handle exn 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

458 
=> (writeln ("Error in parse ast translation for " ^ quote a); raise exn)); 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

459 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

460 
fun ast_of (Node (a, pts)) = trans a (map ast_of pts) 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

461 
 ast_of (Tip tok) = Variable (str_of_token tok); 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

462 
in 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

463 
ast_of pt 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

464 
end; 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

465 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

466 

6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

467 

0  468 
(** ast_to_term **) 
469 

470 
fun ast_to_term trf ast = 

471 
let 

472 
fun trans a args = 

473 
(case trf a of 

474 
None => list_comb (Const (a, dummyT), args) 

18  475 
 Some f => f args handle exn 
476 
=> (writeln ("Error in parse translation for " ^ quote a); raise exn)); 

0  477 

18  478 
fun term_of (Constant a) = trans a [] 
479 
 term_of (Variable x) = scan_var x 

480 
 term_of (Appl (Constant a :: (asts as _ :: _))) = 

481 
trans a (map term_of asts) 

482 
 term_of (Appl (ast :: (asts as _ :: _))) = 

483 
list_comb (term_of ast, map term_of asts) 

484 
 term_of (ast as Appl _) = raise_ast "ast_to_term: malformed ast" [ast]; 

0  485 
in 
18  486 
term_of ast 
0  487 
end; 
488 

489 

490 

491 
(** the Pure syntax **) 

492 

493 
val pure_sext = 

494 
NewSext { 

495 
mixfix = [ 

496 
Mixfix ("(3%_./ _)", "[idts, 'a] => ('b => 'a)", "_lambda", [0], 0), 

497 
Delimfix ("_", "'a => " ^ args, ""), 

498 
Delimfix ("_,/ _", "['a, " ^ args ^ "] => " ^ args, "_args"), 

499 
Delimfix ("_", "id => idt", ""), 

500 
Mixfix ("_::_", "[id, type] => idt", "_idtyp", [0, 0], 0), 

501 
Delimfix ("'(_')", "idt => idt", ""), 

502 
Delimfix ("_", "idt => idts", ""), 

503 
Mixfix ("_/ _", "[idt, idts] => idts", "_idts", [1, 0], 0), 

504 
Delimfix ("_", "id => aprop", ""), 

505 
Delimfix ("_", "var => aprop", ""), 

272  506 
Mixfix ("(1_/(1'(_')))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], max_pri), 
0  507 
Delimfix ("PROP _", "aprop => prop", "_aprop"), 
508 
Delimfix ("_", "prop => asms", ""), 

509 
Delimfix ("_;/ _", "[prop, asms] => asms", "_asms"), 

510 
Mixfix ("((3[ _ ]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1), 

511 
Mixfix ("(_ ==/ _)", "['a::{}, 'a] => prop", "==", [3, 2], 2), 

512 
Mixfix ("(_ =?=/ _)", "['a::{}, 'a] => prop", "=?=", [3, 2], 2), 

513 
Mixfix ("(_ ==>/ _)", "[prop, prop] => prop", "==>", [2, 1], 1), 

514 
Binder ("!!", "('a::logic => prop) => prop", "all", 0, 0)], 

515 
xrules = [], 

238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

516 
parse_ast_translation = [(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

517 
("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr)], 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

518 
parse_translation = [("_abs", abs_tr), ("_aprop", aprop_tr), ("_K", k_tr), 
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

519 
("_explode", explode_tr)], 
0  520 
print_translation = [], 
18  521 
print_ast_translation = [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), 
238
6af40e3a2bcb
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
165
diff
changeset

522 
("==>", impl_ast_tr'), ("_implode", implode_ast_tr')]}; 
0  523 

259  524 
val syntax_types = terminals @ ["syntax", logic, "type", "types", "sort", 
525 
"classes", args, "idt", "idts", "aprop", "asms"]; 

526 

527 
val syntax_consts = [(["_K", "_explode", "_implode"], "syntax")]; 

0  528 

529 
val constrainAbsC = "_constrainAbs"; 

530 
val apropC = "_aprop"; 

531 

532 

533 
end; 

534 