99 |
99 |
100 open Code_Thingol; |
100 open Code_Thingol; |
101 |
101 |
102 (** generic nonsense *) |
102 (** generic nonsense *) |
103 |
103 |
104 fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm) |
104 fun eqn_error (SOME thm) s = |
|
105 error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm) |
105 | eqn_error NONE s = error s; |
106 | eqn_error NONE s = error s; |
106 |
107 |
107 val code_presentationN = "code_presentation"; |
108 val code_presentationN = "code_presentation"; |
108 val stmt_nameN = "stmt_name"; |
109 val stmt_nameN = "stmt_name"; |
109 val _ = Markup.add_mode code_presentationN YXML.output_markup; |
110 val _ = Markup.add_mode code_presentationN YXML.output_markup; |
130 fun markup_stmt name = Print_Mode.setmp [code_presentationN] |
131 fun markup_stmt name = Print_Mode.setmp [code_presentationN] |
131 (Pretty.mark (code_presentationN, [(stmt_nameN, name)])); |
132 (Pretty.mark (code_presentationN, [(stmt_nameN, name)])); |
132 |
133 |
133 fun filter_presentation [] tree = |
134 fun filter_presentation [] tree = |
134 Buffer.empty |
135 Buffer.empty |
135 |> fold XML.add_content tree |
136 |> fold XML.add_content tree |
136 | filter_presentation presentation_names tree = |
137 | filter_presentation presentation_names tree = |
137 let |
138 let |
138 fun is_selected (name, attrs) = |
139 fun is_selected (name, attrs) = |
139 name = code_presentationN |
140 name = code_presentationN |
140 andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN)); |
141 andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN)); |
141 fun add_content_with_space tree (is_first, buf) = |
142 fun add_content_with_space tree (is_first, buf) = |
142 buf |
143 buf |
143 |> not is_first ? Buffer.add "\n\n" |
144 |> not is_first ? Buffer.add "\n\n" |
167 let |
168 let |
168 val (names', namectxt') = fold_map Name.variant names namectxt; |
169 val (names', namectxt') = fold_map Name.variant names namectxt; |
169 val namemap' = fold2 (curry Symtab.update) names names' namemap; |
170 val namemap' = fold2 (curry Symtab.update) names names' namemap; |
170 in (namemap', namectxt') end; |
171 in (namemap', namectxt') end; |
171 |
172 |
172 fun lookup_var (namemap, _) name = case Symtab.lookup namemap name |
173 fun lookup_var (namemap, _) name = |
173 of SOME name' => name' |
174 case Symtab.lookup namemap name of |
|
175 SOME name' => name' |
174 | NONE => error ("Invalid name in context: " ^ quote name); |
176 | NONE => error ("Invalid name in context: " ^ quote name); |
175 |
177 |
176 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode; |
178 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode; |
177 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode; |
179 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode; |
178 |
180 |
188 val fished2 = map_index (fillup_param x) fished1; |
190 val fished2 = map_index (fillup_param x) fished1; |
189 val (fished3, _) = fold_map Name.variant fished2 Name.context; |
191 val (fished3, _) = fold_map Name.variant fished2 Name.context; |
190 val vars' = intro_vars fished3 vars; |
192 val vars' = intro_vars fished3 vars; |
191 in map (lookup_var vars') fished3 end; |
193 in map (lookup_var vars') fished3 end; |
192 |
194 |
193 fun intro_base_names no_syntax deresolve names = names |
195 fun intro_base_names no_syntax deresolve names = names |
194 |> map_filter (fn name => if no_syntax name then |
196 |> map_filter (fn name => if no_syntax name then |
195 let val name' = deresolve name in |
197 let val name' = deresolve name in |
196 if Long_Name.is_qualified name' then NONE else SOME name' |
198 if Long_Name.is_qualified name' then NONE else SOME name' |
197 end else NONE) |
199 end else NONE) |
198 |> intro_vars; |
200 |> intro_vars; |
295 |
297 |
296 fun requires_args (plain_const_syntax _) = 0 |
298 fun requires_args (plain_const_syntax _) = 0 |
297 | requires_args (complex_const_syntax (k, _)) = k; |
299 | requires_args (complex_const_syntax (k, _)) = k; |
298 |
300 |
299 fun simple_const_syntax syn = |
301 fun simple_const_syntax syn = |
300 complex_const_syntax (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn); |
302 complex_const_syntax |
|
303 (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn); |
301 |
304 |
302 type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T) |
305 type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T) |
303 -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T) |
306 -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T) |
304 |
307 |
305 datatype activated_const_syntax = Plain_const_syntax of int * string |
308 datatype activated_const_syntax = Plain_const_syntax of int * string |
309 (Plain_const_syntax (Code.args_number thy c, s), naming) |
312 (Plain_const_syntax (Code.args_number thy c, s), naming) |
310 | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming = |
313 | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming = |
311 fold_map (Code_Thingol.ensure_declared_const thy) cs naming |
314 fold_map (Code_Thingol.ensure_declared_const thy) cs naming |
312 |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs'))); |
315 |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs'))); |
313 |
316 |
314 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy (app as ((c, (_, function_typs)), ts)) = |
317 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy |
315 case const_syntax c |
318 (app as ((c, (_, function_typs)), ts)) = |
316 of NONE => brackify fxy (print_app_expr some_thm vars app) |
319 case const_syntax c of |
317 | SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts) |
320 NONE => brackify fxy (print_app_expr some_thm vars app) |
318 | SOME (Complex_const_syntax (k, print)) => |
321 | SOME (Plain_const_syntax (_, s)) => |
319 let |
322 brackify fxy (str s :: map (print_term some_thm vars BR) ts) |
320 fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs); |
323 | SOME (Complex_const_syntax (k, print)) => |
321 in if k = length ts |
324 let |
322 then print' fxy ts |
325 fun print' fxy ts = |
|
326 print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs); |
|
327 in |
|
328 if k = length ts |
|
329 then print' fxy ts |
323 else if k < length ts |
330 else if k < length ts |
324 then case chop k ts of (ts1, ts2) => |
331 then case chop k ts of (ts1, ts2) => |
325 brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2) |
332 brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2) |
326 else print_term some_thm vars fxy (Code_Thingol.eta_expand k app) |
333 else print_term some_thm vars fxy (Code_Thingol.eta_expand k app) |
327 end; |
334 end; |
328 |
335 |
329 fun gen_print_bind print_term thm (fxy : fixity) pat vars = |
336 fun gen_print_bind print_term thm (fxy : fixity) pat vars = |
330 let |
337 let |
331 val vs = Code_Thingol.fold_varnames (insert (op =)) pat []; |
338 val vs = Code_Thingol.fold_varnames (insert (op =)) pat []; |
332 val vars' = intro_vars vs vars; |
339 val vars' = intro_vars vs vars; |
375 || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break)) |
382 || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break)) |
376 || (Scan.repeat1 |
383 || (Scan.repeat1 |
377 ( $$ "'" |-- sym_any |
384 ( $$ "'" |-- sym_any |
378 || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")") |
385 || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")") |
379 sym_any) >> (String o implode))); |
386 sym_any) >> (String o implode))); |
380 in case Scan.finite Symbol.stopper parse (Symbol.explode s) |
387 fun err s (_, NONE) = (fn () => "malformed mixfix annotation: " ^ quote s) |
381 of ((false, [String s]), []) => mk_plain s |
388 | err _ (_, SOME msg) = msg; |
|
389 in |
|
390 case Scan.finite Symbol.stopper parse (Symbol.explode s) of |
|
391 ((false, [String s]), []) => mk_plain s |
382 | ((_, p as [_]), []) => mk_complex (mk_mixfix prep_arg (NOBR, p)) |
392 | ((_, p as [_]), []) => mk_complex (mk_mixfix prep_arg (NOBR, p)) |
383 | ((b, p as _ :: _ :: _), []) => mk_complex (mk_mixfix prep_arg (if b then NOBR else BR, p)) |
393 | ((b, p as _ :: _ :: _), []) => mk_complex (mk_mixfix prep_arg (if b then NOBR else BR, p)) |
384 | _ => Scan.!! |
394 | _ => Scan.!! (err s) Scan.fail () |
385 (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail () |
|
386 end; |
395 end; |
387 |
396 |
388 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr"); |
397 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr"); |
389 |
398 |
390 fun parse_syntax mk_plain mk_complex prep_arg = |
399 fun parse_syntax mk_plain mk_complex prep_arg = |