author  clasohm 
Mon, 12 Jun 1995 15:01:03 +0200  
changeset 1145  d25b863ab2ac 
parent 922  196ca0973a6d 
child 1178  b28c6ecc3e6d 
permissions  rwrr 
240  1 
(* Title: Pure/Syntax/syn_ext.ML 
2 
ID: $Id$ 

911
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

3 
Author: Markus Wenzel and Carsten Clasohm, TU Muenchen 
240  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 

780  21 
val any: string 
22 
val sprop: string 

240  23 
val typ_to_nonterm: typ > string 
24 
datatype xsymb = 

25 
Delim of string  

26 
Argument of string * int  

27 
Space of string  

28 
Bg of int  Brk of int  En 

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

30 
val max_pri: int 

31 
val chain_pri: int 

32 
val delims_of: xprod list > string list 

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

34 
datatype syn_ext = 

35 
SynExt of { 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

36 
logtypes: string list, 
240  37 
xprods: xprod list, 
38 
consts: string list, 

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

40 
parse_rules: (ast * ast) list, 

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

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

43 
print_rules: (ast * ast) list, 

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

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

45 
val mk_syn_ext: bool > string list > mfix list > 
780  46 
string list > (string * (ast list > ast)) list * 
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

47 
(string * (term list > term)) list * 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

48 
(string * (term list > term)) list * (string * (ast list > ast)) list 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

49 
> (ast * ast) list * (ast * ast) list > syn_ext 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

50 
val syn_ext: string list > mfix list > string list > 
240  51 
(string * (ast list > ast)) list * (string * (term list > term)) list * 
52 
(string * (term list > term)) list * (string * (ast list > ast)) list 

53 
> (ast * ast) list * (ast * ast) list > syn_ext 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

54 
val syn_ext_logtypes: string list > syn_ext 
555
a7f397a14b16
removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents:
441
diff
changeset

55 
val syn_ext_const_names: string list > string list > syn_ext 
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
240
diff
changeset

56 
val syn_ext_rules: string list > (ast * ast) list * (ast * ast) list > syn_ext 
555
a7f397a14b16
removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents:
441
diff
changeset

57 
val syn_ext_trfuns: string list > 
a7f397a14b16
removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents:
441
diff
changeset

58 
(string * (ast list > ast)) list * (string * (term list > term)) list * 
a7f397a14b16
removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents:
441
diff
changeset

59 
(string * (term list > term)) list * (string * (ast list > ast)) list 
a7f397a14b16
removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents:
441
diff
changeset

60 
> syn_ext 
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

61 
val pure_ext: syn_ext 
240  62 
end 
63 
end; 

64 

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

66 
struct 

67 

68 
structure Ast = Ast; 

69 
open Lexicon Ast; 

70 

71 

72 
(** misc definitions **) 

73 

74 
(* syntactic categories *) 

75 

76 
val logic = "logic"; 

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

78 

79 
val args = "args"; 

80 

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

81 
val typeT = Type ("type", []); 
240  82 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

83 
val sprop = "#prop"; 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

84 
val spropT = Type (sprop, []); 
240  85 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

86 
val any = "any"; 
624  87 
val anyT = Type (any, []); 
88 

780  89 

240  90 
(* constants *) 
91 

92 
val constrainC = "_constrain"; 

93 

94 

95 

96 
(** datatype xprod **) 

97 

98 
(*Delim s: delimiter s 

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

100 
Space s: some white space for printing 

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

102 

103 
datatype xsymb = 

104 
Delim of string  

105 
Argument of string * int  

106 
Space of string  

107 
Bg of int  Brk of int  En; 

108 

109 

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

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

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

113 
c: head of parse tree 

114 
p: priority of this production*) 

115 

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

117 

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

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

120 

121 

122 
(* delims_of *) 

123 

124 
fun delims_of xprods = 

125 
let 

126 
fun del_of (Delim s) = Some s 

127 
 del_of _ = None; 

128 

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

130 
mapfilter del_of xsymbs; 

131 
in 

132 
distinct (flat (map dels_of xprods)) 

133 
end; 

134 

135 

136 

137 
(** datatype mfix **) 

138 

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

140 
sy: rhs of production as symbolic string 

141 
ty: type description of production 

142 
c: head of parse tree 

143 
ps: priorities of arguments in sy 

144 
p: priority of production*) 

145 

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

147 

148 

149 
(* typ_to_nonterm *) 

150 

865  151 
fun typ_to_nt _ (Type (c, _)) = c 
152 
 typ_to_nt default _ = default; 

153 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

154 
(*get nonterminal for rhs*) 
865  155 
val typ_to_nonterm = typ_to_nt any; 
240  156 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

157 
(*get nonterminal for lhs*) 
865  158 
val typ_to_nonterm1 = typ_to_nt logic; 
240  159 

160 

161 
(* mfix_to_xprod *) 

162 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

163 
fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) = 
240  164 
let 
165 
fun err msg = 

780  166 
(writeln ("Error in mixfix annotation " ^ quote sy ^ " for " 
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

167 
^ quote const); 
240  168 
error msg); 
169 

170 
fun check_pri p = 

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

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

173 

174 
fun blocks_ok [] 0 = true 

175 
 blocks_ok [] _ = false 

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

177 
 blocks_ok (En :: _) 0 = false 

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

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

180 

181 
fun check_blocks syms = 

182 
if blocks_ok syms 0 then () 

183 
else err "unbalanced block parentheses"; 

184 

185 

911
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

186 
local 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

187 
fun is_meta c = c mem ["(", ")", "/", "_"]; 
240  188 

911
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

189 
fun scan_delim_char ("'" :: c :: cs) = 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

190 
if is_blank c then raise LEXICAL_ERROR else (c, cs) 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

191 
 scan_delim_char ["'"] = err "trailing escape character" 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

192 
 scan_delim_char (chs as c :: cs) = 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

193 
if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs) 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

194 
 scan_delim_char [] = raise LEXICAL_ERROR; 
240  195 

911
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

196 
val scan_sym = 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

197 
$$ "_" >> K (Argument ("", 0))  
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

198 
$$ "("  scan_int >> (Bg o #2)  
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

199 
$$ ")" >> K En  
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

200 
$$ "/"  $$ "/" >> K (Brk ~1)  
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

201 
$$ "/"  scan_any is_blank >> (Brk o length o #2)  
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

202 
scan_any1 is_blank >> (Space o implode)  
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

203 
repeat1 scan_delim_char >> (Delim o implode); 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

204 

55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

205 
val scan_symb = 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

206 
scan_sym >> Some  
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

207 
$$ "'"  scan_one is_blank >> K None; 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

208 
in 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

209 
val scan_symbs = mapfilter I o #1 o repeat scan_symb; 
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

210 
end; 
240  211 

212 

213 
val cons_fst = apfst o cons; 

214 

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

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

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

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

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

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

221 
 add_args (Argument _ :: _) _ _ = 

222 
err "more arguments than in corresponding type" 

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

224 

225 

226 
fun is_arg (Argument _) = true 

227 
 is_arg _ = false; 

228 

229 
fun is_term (Delim _) = true 

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

231 
 is_term _ = false; 

232 

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

234 
 rem_pri sym = sym; 

235 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

236 
fun is_delim (Delim _) = true 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

237 
 is_delim _ = false; 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

238 

b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

239 
(*replace logical types on rhs by "logic"*) 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

240 
fun unify_logtypes copy_prod (a as (Argument (s, p))) = 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

241 
if s mem logtypes then Argument (logic, p) 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

242 
else a 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

243 
 unify_logtypes _ a = a; 
240  244 

911
55754d6d399c
new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents:
865
diff
changeset

245 
val raw_symbs = scan_symbs (explode sy); 
240  246 
val (symbs, lhs) = add_args raw_symbs typ pris; 
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

247 
val copy_prod = lhs mem ["prop", "logic"] 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

248 
andalso const <> "" 
1145
d25b863ab2ac
fixed bug in mfix_to_xprod: lambda productions' lhs shouldn't be modified
clasohm
parents:
922
diff
changeset

249 
andalso not (null symbs) 
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

250 
andalso not (exists is_delim symbs); 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

251 
val lhs' = if convert andalso not copy_prod then 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

252 
(if lhs mem logtypes then logic 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

253 
else if lhs = "prop" then sprop else lhs) 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

254 
else lhs; 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

255 
val symbs' = map (unify_logtypes copy_prod) symbs; 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

256 
val xprod = XProd (lhs', symbs', const, pri); 
240  257 
in 
258 
seq check_pri pris; 

259 
check_pri pri; 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

260 
check_blocks symbs'; 
240  261 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

262 
if is_terminal lhs' then err ("illegal lhs: " ^ lhs') 
240  263 
else if const <> "" then xprod 
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

264 
else if length (filter is_arg symbs') <> 1 then 
240  265 
err "copy production must have exactly one argument" 
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

266 
else if exists is_term symbs' then xprod 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

267 
else XProd (lhs', map rem_pri symbs', "", chain_pri) 
240  268 
end; 
269 

270 

271 
(** datatype syn_ext **) 

272 

273 
datatype syn_ext = 

274 
SynExt of { 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

275 
logtypes: string list, 
240  276 
xprods: xprod list, 
277 
consts: string list, 

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

279 
parse_rules: (ast * ast) list, 

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

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

282 
print_rules: (ast * ast) list, 

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

284 

285 

286 
(* syn_ext *) 

287 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

288 
fun mk_syn_ext convert logtypes mfixes consts trfuns rules = 
240  289 
let 
290 
val (parse_ast_translation, parse_translation, print_translation, 

291 
print_ast_translation) = trfuns; 

292 
val (parse_rules, print_rules) = rules; 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

293 
val logtypes' = logtypes \ "prop"; 
240  294 

624  295 
val mfix_consts = distinct (map (fn (Mfix (_, _, c, _, _)) => c) mfixes); 
764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

296 
val xprods = map (mfix_to_xprod convert logtypes') mfixes; 
240  297 
in 
298 
SynExt { 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

299 
logtypes = logtypes', 
624  300 
xprods = xprods, 
368  301 
consts = filter is_xid (consts union mfix_consts), 
240  302 
parse_ast_translation = parse_ast_translation, 
303 
parse_rules = parse_rules, 

304 
parse_translation = parse_translation, 

305 
print_translation = print_translation, 

306 
print_rules = print_rules, 

307 
print_ast_translation = print_ast_translation} 

308 
end; 

309 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

310 
val syn_ext = mk_syn_ext true; 
240  311 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

312 
fun syn_ext_logtypes logtypes = 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

313 
syn_ext logtypes [] [] ([], [], [], []) ([], []); 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

314 

b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

315 
fun syn_ext_const_names logtypes cs = 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

316 
syn_ext logtypes [] cs ([], [], [], []) ([], []); 
555
a7f397a14b16
removed idT, varT, tidT, tvarT (now in lexicon.ML);
wenzelm
parents:
441
diff
changeset

317 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

318 
fun syn_ext_rules logtypes rules = 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

319 
syn_ext logtypes [] [] ([], [], [], []) rules; 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

320 

b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

321 
fun syn_ext_trfuns logtypes trfuns = 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

322 
syn_ext logtypes [] [] trfuns ([], []); 
240  323 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

324 
(* pure_ext *) 
240  325 

764
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

326 
val pure_ext = mk_syn_ext false [] 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

327 
[Mfix ("_", spropT > propT, "", [0], 0), 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

328 
Mfix ("_", logicT > anyT, "", [0], 0), 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

329 
Mfix ("_", spropT > anyT, "", [0], 0), 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

330 
Mfix ("'(_')", logicT > logicT, "", [0], max_pri), 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

331 
Mfix ("'(_')", spropT > spropT, "", [0], max_pri), 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

332 
Mfix ("_::_", [logicT, typeT] > logicT, "_constrain", [4, 0], 3), 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

333 
Mfix ("_::_", [spropT, typeT] > spropT, "_constrain", [4, 0], 3)] 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

334 
[] 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

335 
([], [], [], []) 
b60e77395d1a
changed Pure's grammar and the way types are converted to nonterminals
clasohm
parents:
624
diff
changeset

336 
([], []); 
240  337 

338 
end; 