author  wenzelm 
Mon, 09 Nov 1998 15:42:08 +0100  
changeset 5840  e2d2b896c717 
parent 473  fdacecc688a1 
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 

382  53 
local open Parser.SynExt.Ast in 
54 
val empty_sext: sext 

55 
val simple_sext: mixfix list > sext 

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

57 
val pure_sext: sext 

58 
val syntax_types: string list 

59 
val syntax_consts: (string list * string) list 

60 
val constrainAbsC: string 

61 
val pure_trfuns: 

62 
(string * (ast list > ast)) list * 

63 
(string * (term list > term)) list * 

64 
(string * (term list > term)) list * 

65 
(string * (ast list > ast)) list 

66 
end 

0  67 
end; 
68 

69 
signature SEXTENSION = 

70 
sig 

71 
include SEXTENSION1 

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

72 
local open Parser Parser.SynExt Parser.SynExt.Ast in 
0  73 
val xrules_of: sext > xrule list 
74 
val abs_tr': term > term 

382  75 
val prop_tr': bool > term > term 
0  76 
val appl_ast_tr': ast * ast list > ast 
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
276
diff
changeset

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

78 
val pt_to_ast: (string > (ast list > ast) option) > parsetree > ast 
0  79 
val ast_to_term: (string > (term list > term) option) > ast > term 
80 
end 

81 
end; 

82 

382  83 
functor SExtensionFun(structure TypeExt: TYPE_EXT and Parser: PARSER 
84 
sharing TypeExt.SynExt = Parser.SynExt): SEXTENSION = 

0  85 
struct 
86 

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

87 
structure Parser = Parser; 
382  88 
open TypeExt Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser; 
0  89 

90 

382  91 
(** datatype sext **) (* FIXME remove *) 
0  92 

93 
datatype mixfix = 

94 
Mixfix of string * string * string * int list * int  

95 
Delimfix of string * string * string  

96 
Infixl of string * string * int  

97 
Infixr of string * string * int  

98 
Binder of string * string * string * int * int  

99 
TInfixl of string * string * int  

100 
TInfixr of string * string * int; 

101 

382  102 

103 
(* FIXME > syntax.ML, BASIC_SYNTAX, SYNTAX *) 

0  104 
datatype xrule = 
105 
op > of (string * string) * (string * string)  

106 
op < of (string * string) * (string * string)  

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

108 

109 
datatype sext = 

110 
Sext of { 

111 
mixfix: mixfix list, 

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

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

114 
NewSext of { 

115 
mixfix: mixfix list, 

116 
xrules: xrule list, 

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

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

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

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

121 

122 

123 
(* simple_sext *) 

124 

125 
fun simple_sext mixfix = 

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

127 

128 

129 
(* empty_sext *) 

130 

131 
val empty_sext = simple_sext []; 

132 

133 

134 
(* sext_components *) 

135 

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

137 
{mixfix = mixfix, 

138 
xrules = [], 

139 
parse_ast_translation = [], 

140 
parse_translation = parse_translation, 

141 
print_translation = print_translation, 

142 
print_ast_translation = []} 

143 
 sext_components (NewSext cmps) = cmps; 

144 

145 

146 
(* mixfix_of *) 

147 

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

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

150 

151 

152 
(* xrules_of *) 

153 

154 
fun xrules_of (Sext _) = [] 

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

156 

157 

158 

382  159 
(*** translation functions ***) (* FIXME > trans.ML *) 
160 

161 
fun const c = Const (c, dummyT); 

162 

163 

18  164 
(** parse (ast) translations **) 
0  165 

166 
(* application *) 

167 

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

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

170 

171 

172 
(* abstraction *) 

173 

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

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

176 

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

18  178 
fold_ast_p "_abs" (unfold_ast "_idts" idts, body) 
0  179 
 lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts; 
180 

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

0  183 
if c = constrainC then 
382  184 
const "_constrainAbs" $ absfree (x, T, body) $ tT 
18  185 
else raise_term "abs_tr" ts 
186 
 abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts; 

0  187 

188 

18  189 
(* nondependent abstraction *) 
190 

276  191 
fun k_tr (*"_K"*) [t] = Abs ("uu", dummyT, incr_boundvars 1 t) 
18  192 
 k_tr (*"_K"*) ts = raise_term "k_tr" ts; 
193 

194 

195 
(* binder *) 

0  196 

197 
fun mk_binder_tr (sy, name) = 

198 
let 

382  199 
fun tr (Free (x, T), t) = const name $ absfree (x, T, t) 
0  200 
 tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t)) 
18  201 
 tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) = 
0  202 
if c = constrainC then 
382  203 
const name $ (const "_constrainAbs" $ absfree (x, T, t) $ tT) 
18  204 
else raise_term "binder_tr" [t1, t] 
205 
 tr (t1, t2) = raise_term "binder_tr" [t1, t2]; 

0  206 

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

18  208 
 binder_tr (*sy*) ts = raise_term "binder_tr" ts; 
0  209 
in 
210 
(sy, binder_tr) 

211 
end; 

212 

213 

382  214 
(* meta propositions *) 
0  215 

382  216 
fun aprop_tr (*"_aprop"*) [t] = const constrainC $ t $ const "prop" 
18  217 
 aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts; 
0  218 

473  219 
fun ofclass_tr (*"_ofclass"*) [ty, cls] = 
220 
cls $ (const constrainC $ const "TYPE" $ (const "itself" $ ty)) 

221 
 ofclass_tr (*"_ofclass"*) ts = raise_term "ofclass_tr" ts; 

382  222 

0  223 

224 
(* meta implication *) 

225 

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

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

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

229 

230 

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

232 

272  233 
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

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

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

236 
 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

237 

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

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

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

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

241 

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

243 
mk_list (map encode_bit (radixpand (2, (ord c)))); 
272  244 

245 
val str = 

246 
(case txt of 

247 
Free (s, _) => s 

248 
 Const (s, _) => s 

249 
 _ => raise_term "explode_tr" ts); 

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

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

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

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

253 
 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

254 

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

255 

0  256 

18  257 
(** print (ast) translations **) 
0  258 

259 
(* application *) 

260 

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

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

263 

264 

18  265 
(* abstraction *) 
0  266 

267 
fun strip_abss vars_of body_of tm = 

268 
let 

18  269 
fun free (x, _) = Free (x, dummyT); 
270 

0  271 
val vars = vars_of tm; 
272 
val body = body_of tm; 

273 
val rev_new_vars = rename_wrt_term body vars; 

274 
in 

18  275 
(map Free (rev rev_new_vars), subst_bounds (map free rev_new_vars, body)) 
0  276 
end; 
277 

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

279 

280 
val eta_contract = ref false; 

281 

282 
fun eta_contr tm = 

283 
let 

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

285 
(case eta_abs t of 

18  286 
t' as f $ u => 
0  287 
(case eta_abs u of 
288 
Bound 0 => 

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

290 
else Abs (a, T, t') 

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

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

293 
 eta_abs t = t; 

294 
in 

295 
if ! eta_contract then eta_abs tm else tm 

296 
end; 

297 

298 

299 
fun abs_tr' tm = 

382  300 
foldr (fn (x, t) => const "_abs" $ x $ t) 
0  301 
(strip_abss strip_abs_vars strip_abs_body (eta_contr tm)); 
302 

303 

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

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

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

309 

18  310 
(* binder *) 
0  311 

312 
fun mk_binder_tr' (name, sy) = 

313 
let 

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

315 
 mk_idts [idt] = idt 

382  316 
 mk_idts (idt :: idts) = const "_idts" $ idt $ mk_idts idts; 
0  317 

318 
fun tr' t = 

319 
let 

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

321 
in 

382  322 
const sy $ mk_idts xs $ bd 
0  323 
end; 
324 

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

382  326 
list_comb (tr' (const name $ t), ts) 
0  327 
 binder_tr' (*name*) [] = raise Match; 
328 
in 

329 
(name, binder_tr') 

330 
end; 

331 

332 

333 
(* idts *) 

334 

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

336 
if c = constrainC then 

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

338 
else raise Match 

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

340 

341 

382  342 
(* meta propositions *) 
343 

344 
fun prop_tr' show_sorts tm = 

345 
let 

346 
fun aprop t = const "_aprop" $ t; 

347 

348 
fun is_prop tys t = 

349 
fastype_of1 (tys, t) = propT handle TERM _ => false; 

350 

351 
fun tr' _ (t as Const _) = t 

352 
 tr' _ (t as Free (x, ty)) = 

353 
if ty = propT then aprop (Free (x, dummyT)) else t 

354 
 tr' _ (t as Var (xi, ty)) = 

355 
if ty = propT then aprop (Var (xi, dummyT)) else t 

356 
 tr' tys (t as Bound _) = 

357 
if is_prop tys t then aprop t else t 

358 
 tr' tys (Abs (x, ty, t)) = Abs (x, ty, tr' (ty :: tys) t) 

359 
 tr' tys (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [ty])))) = 

360 
if is_prop tys t then 

473  361 
const "_ofclass" $ term_of_typ show_sorts ty $ tr' tys t1 
382  362 
else tr' tys t1 $ tr' tys t2 
363 
 tr' tys (t as t1 $ t2) = 

364 
(if is_Const (head_of t) orelse not (is_prop tys t) 

365 
then I else aprop) (tr' tys t1 $ tr' tys t2); 

366 
in 

367 
tr' [] tm 

368 
end; 

369 

370 

0  371 
(* meta implication *) 
372 

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

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

18  375 
(asms as _ :: _ :: _, concl) 
0  376 
=> Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl] 
377 
 _ => raise Match); 

378 

379 

18  380 
(* dependent / nondependent quantifiers *) 
0  381 

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

382  385 
in list_comb (const q $ Free (x', T) $ A $ B', ts) end 
386 
else list_comb (const r $ A $ B, ts) 

0  387 
 dependent_tr' _ _ = raise Match; 
388 

389 

259  390 
(* implode atoms *) 
0  391 

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

392 
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

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

394 
let 
259  395 
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

396 

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

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

398 
let val (xs, y) = unfold_ast_p cons_name lst 
259  399 
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

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

401 

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

402 
fun decode_bit bit = 
259  403 
if bit = bit0 then "0" 
404 
else if bit = bit1 then "1" 

405 
else err (); 

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

406 

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

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

408 
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

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

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

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

412 
 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

413 

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

414 

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

415 

382  416 

417 
(** syn_ext_of_sext **) (* FIXME remove *) 

0  418 

18  419 
fun strip_esc str = 
0  420 
let 
18  421 
fun strip ("'" :: c :: cs) = c :: strip cs 
422 
 strip ["'"] = [] 

423 
 strip (c :: cs) = c :: strip cs 

424 
 strip [] = []; 

0  425 
in 
18  426 
implode (strip (explode str)) 
0  427 
end; 
428 

18  429 
fun infix_name sy = "op " ^ strip_esc sy; 
0  430 

431 

330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
276
diff
changeset

432 
fun syn_ext_of_sext all_roots new_roots xconsts read_typ sext = 
0  433 
let 
18  434 
val {mixfix, parse_ast_translation, parse_translation, print_translation, 
435 
print_ast_translation, ...} = sext_components sext; 

0  436 

18  437 
val tinfixT = [typeT, typeT] > typeT; 
0  438 

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

440 
 binder _ = None; 

441 

442 
fun binder_typ ty = 

443 
(case read_typ ty of 

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

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

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

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

448 
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

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

450 
Mfix ("op " ^ sy, ty, c, [], max_pri)]; 
18  451 

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

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

18  455 
mk_infix sy (read_typ ty) (infix_name sy) p (p + 1) p 
0  456 
 mfix_of (Infixr (sy, ty, p)) = 
18  457 
mk_infix sy (read_typ ty) (infix_name sy) (p + 1) p p 
0  458 
 mfix_of (Binder (sy, ty, _, p, q)) = 
459 
[Mfix ("(3" ^ sy ^ "_./ _)", binder_typ ty, sy, [0, p], q)] 

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

18  461 
[Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p, p + 1], p)] 
0  462 
 mfix_of (TInfixr (s, c, p)) = 
18  463 
[Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p + 1, p], p)]; 
0  464 

465 
val mfix = flat (map mfix_of mixfix); 

18  466 
val binders = mapfilter binder mixfix; 
467 
val bparses = map mk_binder_tr binders; 

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

468 
val bprints = map (mk_binder_tr' o swap) binders; 
0  469 
in 
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
276
diff
changeset

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

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

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

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

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

475 
([], []) 
0  476 
end; 
477 

478 

479 

382  480 
(** constants **) (* FIXME remove *) 
18  481 

482 
fun constants sext = 

483 
let 

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

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

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

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

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

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

490 
in 

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

492 
end; 

493 

494 

495 

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

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

497 

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

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

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

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

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

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

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

504 
=> (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

505 

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

506 
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

507 
 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

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

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

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

511 

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

512 

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

513 

0  514 
(** ast_to_term **) 
515 

516 
fun ast_to_term trf ast = 

517 
let 

518 
fun trans a args = 

519 
(case trf a of 

382  520 
None => list_comb (const a, args) 
18  521 
 Some f => f args handle exn 
522 
=> (writeln ("Error in parse translation for " ^ quote a); raise exn)); 

0  523 

18  524 
fun term_of (Constant a) = trans a [] 
525 
 term_of (Variable x) = scan_var x 

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

527 
trans a (map term_of asts) 

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

529 
list_comb (term_of ast, map term_of asts) 

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

0  531 
in 
18  532 
term_of ast 
0  533 
end; 
534 

535 

536 

382  537 
(** pure_trfuns **) 
538 

539 
val pure_trfuns = 

540 
([(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), 

541 
("_bigimpl", bigimpl_ast_tr)], 

473  542 
[("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), 
543 
("_K", k_tr), ("_explode", explode_tr)], 

382  544 
[], 
545 
[("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr'), 

546 
("_implode", implode_ast_tr')]); 

547 

548 
val constrainAbsC = "_constrainAbs"; 

549 

550 

551 
(** the Pure syntax **) (* FIXME remove *) 

0  552 

553 
val pure_sext = 

554 
NewSext { 

555 
mixfix = [ 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

575 
xrules = [], 

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

576 
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

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

578 
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

579 
("_explode", explode_tr)], 
0  580 
print_translation = [], 
18  581 
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

582 
("==>", impl_ast_tr'), ("_implode", implode_ast_tr')]}; 
0  583 

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

586 

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

0  588 

589 

590 
end; 

591 