1 (* Title: Pure/Syntax/syn_ext.ML
3 Author: Markus Wenzel and Carsten Clasohm, TU Muenchen
5 Syntax extension (internal interface).
11 val constrainC: string
22 val typ_to_nonterm: typ -> string
25 Argument of string * int |
27 Bg of int | Brk of int | En
28 datatype xprod = XProd of string * xsymb list * string * int
31 val delims_of: xprod list -> string list list
32 datatype mfix = Mfix of string * typ * string * int list * int
35 logtypes: string list,
39 parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
40 parse_rules: (Ast.ast * Ast.ast) list,
41 parse_translation: (string * (term list -> term)) list,
42 print_translation: (string * (bool -> typ -> term list -> term)) list,
43 print_rules: (Ast.ast * Ast.ast) list,
44 print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
45 token_translation: (string * string * (string -> string * int)) list}
46 val mfix_args: string -> int
47 val mk_syn_ext: bool -> string list -> mfix list ->
48 string list -> (string * (Ast.ast list -> Ast.ast)) list *
49 (string * (term list -> term)) list *
50 (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
51 -> (string * string * (string -> string * int)) list
52 -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
53 val syn_ext: string list -> mfix list -> string list ->
54 (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
55 (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
56 -> (string * string * (string -> string * int)) list
57 -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
58 val syn_ext_logtypes: string list -> syn_ext
59 val syn_ext_const_names: string list -> string list -> syn_ext
60 val syn_ext_rules: string list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
61 val fix_tr': (term list -> term) -> bool -> typ -> term list -> term
62 val syn_ext_trfuns: string list ->
63 (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
64 (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
66 val syn_ext_trfunsT: string list ->
67 (string * (bool -> typ -> term list -> term)) list -> syn_ext
68 val syn_ext_tokentrfuns: string list
69 -> (string * string * (string -> string * int)) list -> syn_ext
73 structure SynExt : SYN_EXT =
79 (** misc definitions **)
81 (* syntactic categories *)
84 val logicT = Type (logic, []);
89 val typeT = Type ("type", []);
92 val spropT = Type (sprop, []);
95 val anyT = Type (any, []);
100 val constrainC = "_constrain";
104 (** datatype xprod **)
106 (*Delim s: delimiter s
107 Argument (s, p): nonterminal s requiring priority >= p, or valued token
108 Space s: some white space for printing
109 Bg, Brk, En: blocks and breaks for pretty printing*)
113 Argument of string * int |
115 Bg of int | Brk of int | En;
118 (*XProd (lhs, syms, c, p):
119 lhs: name of nonterminal on the lhs of the production
120 syms: list of symbols on the rhs of the production
121 c: head of parse tree
122 p: priority of this production*)
124 datatype xprod = XProd of string * xsymb list * string * int;
126 val max_pri = 1000; (*maximum legal priority*)
127 val chain_pri = ~1; (*dummy for chain productions*)
132 fun delims_of xprods =
134 fun del_of (Delim s) = Some s
137 fun dels_of (XProd (_, xsymbs, _, _)) =
138 mapfilter del_of xsymbs;
140 map Symbol.explode (distinct (flat (map dels_of xprods)))
145 (** datatype mfix **)
147 (*Mfix (sy, ty, c, ps, p):
148 sy: rhs of production as symbolic string
149 ty: type description of production
150 c: head of parse tree
151 ps: priorities of arguments in sy
152 p: priority of production*)
154 datatype mfix = Mfix of string * typ * string * int list * int;
159 fun typ_to_nt _ (Type (c, _)) = c
160 | typ_to_nt default _ = default;
162 (*get nonterminal for rhs*)
163 val typ_to_nonterm = typ_to_nt any;
165 (*get nonterminal for lhs*)
166 val typ_to_nonterm1 = typ_to_nt logic;
169 (* read_mixfix, mfix_args *)
172 fun is_meta c = c mem ["(", ")", "/", "_"];
174 val scan_delim_char =
175 $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
176 Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
179 $$ "_" >> K (Argument ("", 0)) ||
180 $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o #1 o Term.read_int) ||
182 $$ "/" -- $$ "/" >> K (Brk ~1) ||
183 $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||
184 Scan.any1 Symbol.is_blank >> (Space o implode) ||
185 Scan.repeat1 scan_delim_char >> (Delim o implode);
189 $$ "'" -- Scan.one Symbol.is_blank >> K None;
191 val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
192 val read_symbs = mapfilter I o #1 o Scan.error (Scan.finite Symbol.eof scan_symbs);
194 val read_mixfix = read_symbs o Symbol.explode;
198 foldl (fn (i, Argument _) => i + 1 | (i, _) => i) (0, read_mixfix sy);
203 fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) =
206 (if msg = "" then () else error_msg msg;
207 error ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const));
210 if p >= 0 andalso p <= max_pri then ()
211 else err ("Precedence out of range: " ^ string_of_int p);
213 fun blocks_ok [] 0 = true
214 | blocks_ok [] _ = false
215 | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
216 | blocks_ok (En :: _) 0 = false
217 | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
218 | blocks_ok (_ :: syms) n = blocks_ok syms n;
220 fun check_blocks syms =
221 if blocks_ok syms 0 then ()
222 else err "Unbalanced block parentheses";
225 val cons_fst = apfst o cons;
227 fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
228 | add_args [] _ _ = err "Too many precedences"
229 | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
230 cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
231 | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
232 cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
233 | add_args (Argument _ :: _) _ _ =
234 err "More arguments than in corresponding type"
235 | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
238 fun is_arg (Argument _) = true
241 fun is_term (Delim _) = true
242 | is_term (Argument (s, _)) = is_terminal s
245 fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
248 fun is_delim (Delim _) = true
249 | is_delim _ = false;
251 fun logify_types copy_prod (a as (Argument (s, p))) =
252 if s mem logtypes then Argument (logic, p) else a
253 | logify_types _ a = a;
256 val raw_symbs = read_mixfix sy handle ERROR => err "";
257 val (symbs, lhs) = add_args raw_symbs typ pris;
259 lhs mem ["prop", "logic"]
261 andalso not (null symbs)
262 andalso not (exists is_delim symbs);
264 if convert andalso not copy_prod then
265 (if lhs mem logtypes then logic
266 else if lhs = "prop" then sprop else lhs)
268 val symbs' = map (logify_types copy_prod) symbs;
269 val xprod = XProd (lhs', symbs', const, pri);
275 if is_terminal lhs' then err ("Illegal lhs: " ^ lhs')
276 else if const <> "" then xprod
277 else if length (filter is_arg symbs') <> 1 then
278 err "Copy production must have exactly one argument"
279 else if exists is_term symbs' then xprod
280 else XProd (lhs', map rem_pri symbs', "", chain_pri)
284 (** datatype syn_ext **)
288 logtypes: string list,
291 prmodes: string list,
292 parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
293 parse_rules: (Ast.ast * Ast.ast) list,
294 parse_translation: (string * (term list -> term)) list,
295 print_translation: (string * (bool -> typ -> term list -> term)) list,
296 print_rules: (Ast.ast * Ast.ast) list,
297 print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
298 token_translation: (string * string * (string -> string * int)) list}
303 fun mk_syn_ext convert logtypes mfixes consts trfuns tokentrfuns rules =
305 val (parse_ast_translation, parse_translation, print_translation,
306 print_ast_translation) = trfuns;
307 val (parse_rules, print_rules) = rules;
308 val logtypes' = logtypes \ "prop";
310 val mfix_consts = distinct (map (fn (Mfix (_, _, c, _, _)) => c) mfixes);
311 val xprods = map (mfix_to_xprod convert logtypes') mfixes;
314 logtypes = logtypes',
316 consts = filter is_xid (consts union mfix_consts),
317 prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
318 parse_ast_translation = parse_ast_translation,
319 parse_rules = parse_rules,
320 parse_translation = parse_translation,
321 print_translation = print_translation,
322 print_rules = print_rules,
323 print_ast_translation = print_ast_translation,
324 token_translation = tokentrfuns}
328 val syn_ext = mk_syn_ext true;
330 fun syn_ext_logtypes logtypes =
331 syn_ext logtypes [] [] ([], [], [], []) [] ([], []);
333 fun syn_ext_const_names logtypes cs =
334 syn_ext logtypes [] cs ([], [], [], []) [] ([], []);
336 fun syn_ext_rules logtypes rules =
337 syn_ext logtypes [] [] ([], [], [], []) [] rules;
339 fun fix_tr' f _ _ ts = f ts;
341 fun syn_ext_trfuns logtypes (atrs, trs, tr's, atr's) =
342 syn_ext logtypes [] [] (atrs, trs, map (apsnd fix_tr') tr's, atr's) [] ([], []);
344 fun syn_ext_trfunsT logtypes tr's =
345 syn_ext logtypes [] [] ([], [], tr's, []) [] ([], []);
347 fun syn_ext_tokentrfuns logtypes tokentrfuns =
348 syn_ext logtypes [] [] ([], [], [], []) tokentrfuns ([], []);
353 val pure_ext = mk_syn_ext false []
354 [Mfix ("_", spropT --> propT, "", [0], 0),
355 Mfix ("_", logicT --> anyT, "", [0], 0),
356 Mfix ("_", spropT --> anyT, "", [0], 0),
357 Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
358 Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
359 Mfix ("_::_", [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
360 Mfix ("_::_", [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]