author  clasohm 
Wed, 29 Jun 1994 12:01:17 +0200  
changeset 441  2b97bd6415b7 
parent 373  68400ea32f7b 
child 555  a7f397a14b16 
permissions  rwrr 
240  1 
(* Title: Pure/Syntax/syn_ext.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Syntax extension (internal interface). 

6 
*) 

7 

8 
signature SYN_EXT0 = 

9 
sig 

10 
val typeT: typ 

11 
val constrainC: string 

12 
end; 

13 

14 
signature SYN_EXT = 

15 
sig 

16 
include SYN_EXT0 

17 
structure Ast: AST 

18 
local open Ast in 

19 
val logic: string 

20 
val args: string 

21 
val idT: typ 

22 
val varT: typ 

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

23 
val tidT: typ 
240  24 
val tvarT: typ 
25 
val applC: string 

26 
val typ_to_nonterm: typ > string 

27 
datatype xsymb = 

28 
Delim of string  

29 
Argument of string * int  

30 
Space of string  

31 
Bg of int  Brk of int  En 

32 
datatype xprod = XProd of string * xsymb list * string * int 

33 
val max_pri: int 

34 
val chain_pri: int 

35 
val delims_of: xprod list > string list 

36 
datatype mfix = Mfix of string * typ * string * int list * int 

37 
datatype syn_ext = 

38 
SynExt of { 

39 
roots: string list, 

40 
xprods: xprod list, 

41 
consts: string list, 

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

43 
parse_rules: (ast * ast) list, 

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

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

46 
print_rules: (ast * ast) list, 

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

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

48 
val syn_ext: string list > string list > mfix list > string list > 
240  49 
(string * (ast list > ast)) list * (string * (term list > term)) list * 
50 
(string * (term list > term)) list * (string * (ast list > ast)) list 

51 
> (ast * ast) list * (ast * ast) list > syn_ext 

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

52 
val syn_ext_rules: string list > (ast * ast) list * (ast * ast) list > syn_ext 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

53 
val syn_ext_roots: string list > string list > syn_ext 
240  54 
end 
55 
end; 

56 

57 
functor SynExtFun(structure Lexicon: LEXICON and Ast: AST): SYN_EXT = 

58 
struct 

59 

60 
structure Ast = Ast; 

61 
open Lexicon Ast; 

62 

63 

64 
(** misc definitions **) 

65 

66 
(* syntactic categories *) 

67 

68 
val logic = "logic"; 

69 
val logicT = Type (logic, []); 

70 

71 
val logic1 = "logic1"; 

72 
val logic1T = Type (logic1, []); 

73 

74 
val args = "args"; 

75 
val argsT = Type (args, []); 

76 

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

77 
val typeT = Type ("type", []); 
240  78 

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

79 
val funT = Type ("fun", []); 
240  80 

81 

82 
(* terminals *) 

83 

84 
val idT = Type (id, []); 

85 
val varT = Type (var, []); 

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

86 
val tidT = Type (tid, []); 
240  87 
val tvarT = Type (tvar, []); 
88 

89 

90 
(* constants *) 

91 

92 
val applC = "_appl"; 

93 
val constrainC = "_constrain"; 

94 

95 

96 

97 
(** datatype xprod **) 

98 

99 
(*Delim s: delimiter s 

100 
Argument (s, p): nonterminal s requiring priority >= p, or valued token 

101 
Space s: some white space for printing 

102 
Bg, Brk, En: blocks and breaks for pretty printing*) 

103 

104 
datatype xsymb = 

105 
Delim of string  

106 
Argument of string * int  

107 
Space of string  

108 
Bg of int  Brk of int  En; 

109 

110 

111 
(*XProd (lhs, syms, c, p): 

112 
lhs: name of nonterminal on the lhs of the production 

113 
syms: list of symbols on the rhs of the production 

114 
c: head of parse tree 

115 
p: priority of this production*) 

116 

117 
datatype xprod = XProd of string * xsymb list * string * int; 

118 

119 
val max_pri = 1000; (*maximum legal priority*) 

120 
val chain_pri = ~1; (*dummy for chain productions*) 

121 

122 

123 
(* delims_of *) 

124 

125 
fun delims_of xprods = 

126 
let 

127 
fun del_of (Delim s) = Some s 

128 
 del_of _ = None; 

129 

130 
fun dels_of (XProd (_, xsymbs, _, _)) = 

131 
mapfilter del_of xsymbs; 

132 
in 

133 
distinct (flat (map dels_of xprods)) 

134 
end; 

135 

136 

137 

138 
(** datatype mfix **) 

139 

140 
(*Mfix (sy, ty, c, ps, p): 

141 
sy: rhs of production as symbolic string 

142 
ty: type description of production 

143 
c: head of parse tree 

144 
ps: priorities of arguments in sy 

145 
p: priority of production*) 

146 

147 
datatype mfix = Mfix of string * typ * string * int list * int; 

148 

149 

150 
(* typ_to_nonterm *) 

151 

152 
fun typ_to_nonterm (Type (c, _)) = c 

153 
 typ_to_nonterm _ = logic; 

154 

155 
fun typ_to_nonterm1 (Type (c, _)) = c 

156 
 typ_to_nonterm1 _ = logic1; 

157 

158 

159 
(* mfix_to_xprod *) 

160 

161 
fun mfix_to_xprod (Mfix (sy, typ, const, pris, pri)) = 

162 
let 

163 
fun err msg = 

164 
(writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const); 

165 
error msg); 

166 

167 
fun check_pri p = 

168 
if p >= 0 andalso p <= max_pri then () 

169 
else err ("precedence out of range: " ^ string_of_int p); 

170 

171 
fun blocks_ok [] 0 = true 

172 
 blocks_ok [] _ = false 

173 
 blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1) 

174 
 blocks_ok (En :: _) 0 = false 

175 
 blocks_ok (En :: syms) n = blocks_ok syms (n  1) 

176 
 blocks_ok (_ :: syms) n = blocks_ok syms n; 

177 

178 
fun check_blocks syms = 

179 
if blocks_ok syms 0 then () 

180 
else err "unbalanced block parentheses"; 

181 

182 

183 
fun is_meta c = c mem ["(", ")", "/", "_"]; 

184 

185 
fun scan_delim_char ("'" :: c :: cs) = 

186 
if is_blank c then err "illegal spaces in delimiter" else (c, cs) 

187 
 scan_delim_char ["'"] = err "trailing escape character" 

188 
 scan_delim_char (chs as c :: cs) = 

189 
if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs) 

190 
 scan_delim_char [] = raise LEXICAL_ERROR; 

191 

192 
val scan_symb = 

193 
$$ "_" >> K (Argument ("", 0))  

194 
$$ "("  scan_int >> (Bg o #2)  

195 
$$ ")" >> K En  

196 
$$ "/"  $$ "/" >> K (Brk ~1)  

197 
$$ "/"  scan_any is_blank >> (Brk o length o #2)  

198 
scan_any1 is_blank >> (Space o implode)  

199 
repeat1 scan_delim_char >> (Delim o implode); 

200 

201 

202 
val cons_fst = apfst o cons; 

203 

204 
fun add_args [] ty [] = ([], typ_to_nonterm1 ty) 

205 
 add_args [] _ _ = err "too many precedences" 

206 
 add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] = 

207 
cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys []) 

208 
 add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) = 

209 
cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps) 

210 
 add_args (Argument _ :: _) _ _ = 

211 
err "more arguments than in corresponding type" 

212 
 add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps); 

213 

214 

215 
fun is_arg (Argument _) = true 

216 
 is_arg _ = false; 

217 

218 
fun is_term (Delim _) = true 

219 
 is_term (Argument (s, _)) = is_terminal s 

220 
 is_term _ = false; 

221 

222 
fun rem_pri (Argument (s, _)) = Argument (s, chain_pri) 

223 
 rem_pri sym = sym; 

224 

225 

226 
val (raw_symbs, _) = repeat scan_symb (explode sy); 

227 
val (symbs, lhs) = add_args raw_symbs typ pris; 

228 
val xprod = XProd (lhs, symbs, const, pri); 

229 
in 

230 
seq check_pri pris; 

231 
check_pri pri; 

232 
check_blocks symbs; 

233 

234 
if is_terminal lhs then err ("illegal lhs: " ^ lhs) 

235 
else if const <> "" then xprod 

236 
else if length (filter is_arg symbs) <> 1 then 

237 
err "copy production must have exactly one argument" 

238 
else if exists is_term symbs then xprod 

239 
else XProd (lhs, map rem_pri symbs, "", chain_pri) 

240 
end; 

241 

242 

243 
(** datatype syn_ext **) 

244 

245 
datatype syn_ext = 

246 
SynExt of { 

247 
roots: string list, 

248 
xprods: xprod list, 

249 
consts: string list, 

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

251 
parse_rules: (ast * ast) list, 

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

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

254 
print_rules: (ast * ast) list, 

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

256 

257 

258 
(* syn_ext *) 

259 

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

260 
fun syn_ext all_roots new_roots mfixes consts trfuns rules = 
240  261 
let 
262 
val (parse_ast_translation, parse_translation, print_translation, 

263 
print_ast_translation) = trfuns; 

264 
val (parse_rules, print_rules) = rules; 

265 

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

266 
val Troots = map (apr (Type, [])) new_roots; 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

267 
val Troots' = Troots \\ [typeT, propT]; 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

268 

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

269 
fun change_name T ext = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

270 
let val Type (name, ts) = T 
373
68400ea32f7b
fixed a bug in syntax_error, added "Building new grammar" message;
clasohm
parents:
369
diff
changeset

271 
in Type ("@" ^ name ^ ext, ts) end; 
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

272 

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

273 
(* Append "_H" to lhs if production is not a copy or chain production *) 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

274 
fun hide_xprod roots (XProd (lhs, symbs, const, pri)) = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

275 
let fun is_delim (Delim _) = true 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

276 
 is_delim _ = false 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

277 
in if const <> "" andalso lhs mem roots andalso exists is_delim symbs then 
373
68400ea32f7b
fixed a bug in syntax_error, added "Building new grammar" message;
clasohm
parents:
369
diff
changeset

278 
XProd ("@" ^ lhs ^ "_H", symbs, const, pri) 
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

279 
else XProd (lhs, symbs, const, pri) 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

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

281 

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

282 
(* Make descend production and append "_H" to rhs nonterminal *) 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

283 
fun descend_right (from, to) = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

284 
Mfix ("_", change_name to "_H" > from, "", [0], 0); 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

285 

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

286 
(* Make descend production and append "_H" to lhs *) 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

287 
fun descend_left (from, to) = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

288 
Mfix ("_", to > change_name from "_H", "", [0], 0); 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

289 

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

290 
(* Make descend production and append "_A" to lhs *) 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

291 
fun descend1 (from, to) = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

292 
Mfix ("_", to > change_name from "_A", "", [0], 0); 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

293 

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

294 
(* Make parentheses production for 'hidden' and 'automatic' nonterminal *) 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

295 
fun parents T = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

296 
if T = typeT then 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

297 
[Mfix ("'(_')", T > T, "", [0], max_pri)] 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

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

299 
[Mfix ("'(_')", change_name T "_H" > change_name T "_H", "", [0], max_pri), 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

300 
Mfix ("'(_')", change_name T "_A" > change_name T "_A", "", [0], max_pri)]; 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

301 

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

302 
fun mkappl T = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

303 
Mfix ("(1_/(1'(_')))", [funT, argsT] > change_name T "_A", applC, 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

304 
[max_pri, 0], max_pri); 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

305 

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

306 
fun mkid T = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

307 
Mfix ("_", idT > change_name T "_A", "", [], max_pri); 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

308 

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

309 
fun mkvar T = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

310 
Mfix ("_", varT > change_name T "_A", "", [], max_pri); 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

311 

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

312 
fun constrain T = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

313 
Mfix ("_::_", [T, typeT] > change_name T "_A", constrainC, 
441  314 
[4, 0], 3) 
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

315 

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

316 
fun unhide T = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

317 
if T <> logicT then 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

318 
[Mfix ("_", change_name T "_H" > T, "", [0], 0), 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

319 
Mfix ("_", change_name T "_A" > T, "", [0], 0)] 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

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

321 
[Mfix ("_", change_name T "_A" > T, "", [0], 0)]; 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

322 

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

323 
val mfixes' = flat (map parents Troots) @ map mkappl Troots' @ 
240  324 
map mkid Troots' @ map mkvar Troots' @ map constrain Troots' @ 
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

325 
map (apl (logicT, descend_right)) (Troots \\ [logicT, typeT]) @ 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

326 
map (apr (descend1, logic1T)) (Troots') @ 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

327 
flat (map unhide (Troots \\ [typeT])); 
240  328 
val mfix_consts = 
368  329 
distinct (map (fn (Mfix (_, _, c, _, _)) => c) (mfixes @ mfixes')); 
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

330 
val xprods = map mfix_to_xprod mfixes; 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

331 
val xprods' = map mfix_to_xprod mfixes'; 
240  332 
in 
333 
SynExt { 

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

334 
roots = new_roots, 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

335 
xprods = (map (hide_xprod (all_roots \\ ["logic", "type"])) xprods) 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

336 
@ xprods', (* hide only productions that weren't created 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

337 
automatically *) 
368  338 
consts = filter is_xid (consts union mfix_consts), 
240  339 
parse_ast_translation = parse_ast_translation, 
340 
parse_rules = parse_rules, 

341 
parse_translation = parse_translation, 

342 
print_translation = print_translation, 

343 
print_rules = print_rules, 

344 
print_ast_translation = print_ast_translation} 

345 
end; 

346 

347 

348 
(* syn_ext_rules, syn_ext_roots *) 

349 

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

350 
fun syn_ext_rules roots rules = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

351 
syn_ext roots [] [] [] ([], [], [], []) rules; 
240  352 

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

353 
fun syn_ext_roots all_roots new_roots = 
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

354 
syn_ext all_roots new_roots [] [] ([], [], [], []) ([], []); 
240  355 

356 

357 
end; 

358 