more basic const report (without completion) for known Const within syntax tree, which usually refers to special syntax (without proper @{const_syntax} markers);
tuned;
1 (* Title: Pure/Syntax/syntax_phases.ML
4 Main phases of inner syntax processing, with standard implementations
5 of parse/unparse operations.
8 signature SYNTAX_PHASES =
10 val decode_sort: term -> sort
11 val decode_typ: term -> typ
12 val decode_term: Proof.context ->
13 Position.report_text list * term Exn.result -> Position.report_text list * term Exn.result
14 val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
15 val term_of_typ: Proof.context -> typ -> term
16 val print_checks: Proof.context -> unit
17 val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
18 Context.generic -> Context.generic
19 val term_check: int -> string -> (Proof.context -> term list -> term list) ->
20 Context.generic -> Context.generic
21 val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) ->
22 Context.generic -> Context.generic
23 val term_uncheck: int -> string -> (Proof.context -> term list -> term list) ->
24 Context.generic -> Context.generic
25 val typ_check': int -> string ->
26 (typ list -> Proof.context -> (typ list * Proof.context) option) ->
27 Context.generic -> Context.generic
28 val term_check': int -> string ->
29 (term list -> Proof.context -> (term list * Proof.context) option) ->
30 Context.generic -> Context.generic
31 val typ_uncheck': int -> string ->
32 (typ list -> Proof.context -> (typ list * Proof.context) option) ->
33 Context.generic -> Context.generic
34 val term_uncheck': int -> string ->
35 (term list -> Proof.context -> (term list * Proof.context) option) ->
36 Context.generic -> Context.generic
39 structure Syntax_Phases: SYNTAX_PHASES =
42 (** markup logical entities **)
44 fun markup_class ctxt c =
45 [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c];
47 fun markup_type ctxt c =
48 [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c];
50 fun markup_const ctxt c =
51 [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c];
53 fun markup_free ctxt x =
54 [if Name.is_skolem x then Markup.skolem else Markup.free] @
55 (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
56 then [Variable.markup_fixed ctxt x]
59 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
61 fun markup_bound def ps (name, id) =
62 let val entity = Markup.entity Markup.boundN name in
64 map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps
67 fun markup_entity ctxt c =
68 (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of
70 | SOME b => markup_entity ctxt b
71 | NONE => c |> Lexicon.unmark
72 {case_class = markup_class ctxt,
73 case_type = markup_type ctxt,
74 case_const = markup_const ctxt,
75 case_fixed = markup_free ctxt,
76 case_default = K []});
80 (** decode parse trees **)
86 fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]);
88 fun class s = Lexicon.unmark_class s handle Fail _ => err ();
90 fun classes (Const (s, _)) = [class s]
91 | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
94 fun sort (Const ("_topsort", _)) = []
95 | sort (Const ("_sort", _) $ cs) = classes cs
96 | sort (Const (s, _)) = [class s]
103 fun decode_pos (Free (s, _)) =
104 if is_some (Term_Position.decode s) then SOME s else NONE
105 | decode_pos _ = NONE;
109 fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]);
113 Const ("_tfree", _) $ t => typ ps sort t
114 | Const ("_tvar", _) $ t => typ ps sort t
115 | Const ("_ofsort", _) $ t $ s =>
116 (case decode_pos s of
117 SOME p => typ (p :: ps) sort t
119 if is_none sort then typ ps (SOME (decode_sort s)) t
121 | Const ("_dummy_ofsort", _) $ s => TFree ("'_dummy_", decode_sort s)
122 | Free (x, _) => TFree (x, ps @ the_default dummyS sort)
123 | Var (xi, _) => TVar (xi, ps @ the_default dummyS sort)
125 if null ps andalso is_none sort then
127 val (head, args) = Term.strip_comb tm;
130 Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
132 in Type (a, map (typ [] NONE) args) end
134 in typ [] NONE tm end;
137 (* parsetree_to_ast *)
139 fun parsetree_to_ast ctxt trf parsetree =
141 val reports = Unsynchronized.ref ([]: Position.report_text list);
142 fun report pos = Position.store_reports reports [pos];
143 val append_reports = Position.append_reports reports;
147 NONE => Ast.mk_appl (Ast.Constant a) args
148 | SOME f => f ctxt args);
150 fun asts_of_token tok =
151 if Lexicon.valued_token tok
152 then [Ast.Variable (Lexicon.str_of_token tok)]
155 fun ast_of_position tok =
156 Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok));
158 fun ast_of_dummy a tok =
159 Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
161 fun asts_of_position c tok =
162 [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
164 and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
166 val pos = Lexicon.pos_of_token tok;
167 val (c, rs) = Proof_Context.check_class ctxt (Lexicon.str_of_token tok, pos);
168 val _ = append_reports rs;
169 in [Ast.Constant (Lexicon.mark_class c)] end
170 | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
172 val pos = Lexicon.pos_of_token tok;
173 val (Type (c, _), rs) =
174 Proof_Context.check_type_name ctxt {proper = true, strict = false}
175 (Lexicon.str_of_token tok, pos);
176 val _ = append_reports rs;
177 in [Ast.Constant (Lexicon.mark_type c)] end
178 | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
179 | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
180 | asts_of (Parser.Node (a as "\\<^const>dummy_pattern", [Parser.Tip tok])) =
182 | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
184 | asts_of (Parser.Node ("_idtypdummy", pts as [Parser.Tip tok, _, _])) =
185 [Ast.Appl (Ast.Constant "_constrain" :: ast_of_dummy "_idtdummy" tok :: maps asts_of pts)]
186 | asts_of (Parser.Node (a, pts)) =
188 val _ = pts |> List.app
189 (fn Parser.Node _ => () | Parser.Tip tok =>
190 if Lexicon.valued_token tok then ()
191 else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a);
192 in [trans a (maps asts_of pts)] end
193 | asts_of (Parser.Tip tok) = asts_of_token tok
198 | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts));
200 val ast = Exn.interruptible_capture ast_of parsetree;
201 in (! reports, ast) end;
206 fun ast_to_term ctxt trf =
210 NONE => Term.list_comb (Syntax.const a, args)
211 | SOME f => f ctxt args);
213 fun term_of (Ast.Constant a) = trans a []
214 | term_of (Ast.Variable x) = Lexicon.read_var x
215 | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
216 trans a (map term_of asts)
217 | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
218 Term.list_comb (term_of ast, map term_of asts)
219 | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
223 (* decode_term -- transform parse tree into raw term *)
225 fun decode_const ctxt (c, ps) =
227 val (Const (c', _), reports) =
228 Proof_Context.check_const ctxt {proper = true, strict = false} (c, ps);
229 in (c', reports) end;
233 fun get_free ctxt x =
235 val fixed = Variable.lookup_fixed ctxt x;
236 val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
237 val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
239 if Variable.is_const ctxt x then NONE
240 else if is_some fixed then fixed
241 else if not is_const orelse is_declared then SOME x
247 fun decode_term _ (result as (_: Position.report_text list, Exn.Exn _)) = result
248 | decode_term ctxt (reports0, Exn.Res tm) =
250 val reports = Unsynchronized.ref reports0;
251 fun report ps = Position.store_reports reports ps;
252 val append_reports = Position.append_reports reports;
254 fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
255 (case Term_Position.decode_position typ of
256 SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
257 | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
258 | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
259 (case Term_Position.decode_position typ of
260 SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t)
261 | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
262 | decode _ qs bs (Abs (x, T, t)) =
265 val _ = report qs (markup_bound true qs) (x, id);
266 in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end
267 | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
268 | decode ps _ _ (Const (a, T)) =
269 (case try Lexicon.unmark_fixed a of
270 SOME x => (report ps (markup_free ctxt) x; Free (x, T))
274 (case try Lexicon.unmark_const a of
276 | NONE => #1 (decode_const ctxt (a, [])));
277 val _ = report ps (markup_const ctxt) c;
279 | decode ps _ _ (Free (a, T)) =
280 ((Name.reject_internal (a, ps) handle ERROR msg =>
281 error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
282 (case get_free ctxt a of
283 SOME x => (report ps (markup_free ctxt) x; Free (x, T))
286 val (c, rs) = decode_const ctxt (a, ps);
287 val _ = append_reports rs;
288 in Const (c, T) end))
289 | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
290 | decode ps _ bs (t as Bound i) =
291 (case try (nth bs) i of
292 SOME (qs, (x, id)) => (report ps (markup_bound false qs) (x, id); t)
295 val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
296 in (! reports, tm') end;
306 fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
307 fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
309 fun report_result ctxt pos ambig_msgs results =
310 (case (proper_results results, failed_results results) of
311 ([], (reports, exn) :: _) => (Context_Position.reports_text ctxt reports; reraise exn)
312 | ([(reports, x)], _) => (Context_Position.reports_text ctxt reports; x)
314 if null ambig_msgs then
315 error ("Parse error: ambiguous syntax" ^ Position.here pos)
316 else error (cat_lines ambig_msgs));
321 fun parse_asts ctxt raw root (syms, pos) =
323 val syn = Proof_Context.syn_of ctxt;
324 val ast_tr = Syntax.parse_ast_translation syn;
326 val toks = Syntax.tokenize syn raw syms;
327 val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
329 val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
331 error (msg ^ Markup.markup_report (implode (map (Lexicon.reported_token_range ctxt) toks)));
332 val len = length pts;
334 val limit = Config.get ctxt Syntax.ambiguity_limit;
339 (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
340 "\nproduces " ^ string_of_int len ^ " parse trees" ^
341 (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
342 map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
345 in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end;
347 fun parse_tree ctxt root input =
349 val syn = Proof_Context.syn_of ctxt;
350 val tr = Syntax.parse_translation syn;
351 val parse_rules = Syntax.parse_rules syn;
352 val (ambig_msgs, asts) = parse_asts ctxt false root input;
354 (map o apsnd o Exn.maps_result)
355 (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts;
356 in (ambig_msgs, results) end;
359 (* parse logical entities *)
361 fun parse_failed ctxt pos msg kind =
362 cat_error msg ("Failed to parse " ^ kind ^
363 Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
365 fun parse_sort ctxt =
366 Syntax.parse_token ctxt Term_XML.Decode.sort Markup.language_sort
368 parse_tree ctxt "sort" (syms, pos)
369 |> uncurry (report_result ctxt pos)
371 |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
372 handle ERROR msg => parse_failed ctxt pos msg "sort");
375 Syntax.parse_token ctxt Term_XML.Decode.typ Markup.language_type
377 parse_tree ctxt "type" (syms, pos)
378 |> uncurry (report_result ctxt pos)
380 handle ERROR msg => parse_failed ctxt pos msg "type");
382 fun parse_term is_prop ctxt =
384 val (markup, kind, root, constrain) =
386 then (Markup.language_prop, "prop", "prop", Type.constraint propT)
387 else (Markup.language_term, "term", Config.get ctxt Syntax.root, I);
388 val decode = constrain o Term_XML.Decode.term;
390 Syntax.parse_token ctxt decode markup
393 val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt);
394 val parsed_len = length (proper_results results);
396 val ambiguity_warning = Config.get ctxt Syntax.ambiguity_warning;
397 val limit = Config.get ctxt Syntax.ambiguity_limit;
399 (*brute-force disambiguation via type-inference*)
400 fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
401 handle exn as ERROR _ => Exn.Exn exn;
404 if parsed_len > 1 then
405 (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_result)
408 val reports' = fst (hd results');
410 val errs = map snd (failed_results results');
411 val checked = map snd (proper_results results');
412 val checked_len = length checked;
414 val pretty_term = Syntax.pretty_term (Config.put Printer.show_brackets true ctxt);
416 if checked_len = 0 then
417 report_result ctxt pos []
418 [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
419 else if checked_len = 1 then
420 (if parsed_len > 1 andalso ambiguity_warning then
421 Context_Position.if_visible ctxt warning
422 (cat_lines (ambig_msgs @
423 ["Fortunately, only one parse tree is type correct" ^
424 Position.here (Position.reset_range pos) ^
425 ",\nbut you may still want to disambiguate your grammar or your input."]))
426 else (); report_result ctxt pos [] results')
428 report_result ctxt pos []
429 [(reports', Exn.Exn (ERROR (cat_lines (ambig_msgs @
430 (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^
431 (if checked_len <= limit then ""
432 else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
433 map (Pretty.string_of o Pretty.item o single o pretty_term)
434 (take limit checked))))))]
435 end handle ERROR msg => parse_failed ctxt pos msg kind)
439 (* parse_ast_pattern *)
441 fun parse_ast_pattern ctxt (root, str) =
443 val syn = Proof_Context.syn_of ctxt;
445 val reports = Unsynchronized.ref ([]: Position.report_text list);
446 fun report ps = Position.store_reports reports ps;
448 fun decode_const ps c = (report ps (markup_entity ctxt) c; Ast.Constant c);
449 fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x);
450 fun decode_appl ps asts = Ast.Appl (map (decode ps) asts)
451 and decode ps (Ast.Constant c) = decode_const ps c
452 | decode ps (Ast.Variable x) =
453 if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
454 then decode_const ps x
456 | decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) =
457 if member (op =) Term_Position.markers c then
458 (case Term_Position.decode x of
459 SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args)
460 | NONE => decode_appl ps asts)
461 else decode_appl ps asts
462 | decode ps (Ast.Appl asts) = decode_appl ps asts;
464 val {text, pos, ...} = Syntax.read_token str;
465 val syms = Symbol_Pos.explode (text, pos);
467 parse_asts ctxt true root (syms, pos)
468 |> uncurry (report_result ctxt pos)
470 val _ = Context_Position.reports_text ctxt (! reports);
475 (** encode parse trees **)
481 val class = Syntax.const o Lexicon.mark_class;
483 fun classes [c] = class c
484 | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
487 [] => Syntax.const "_topsort"
489 | cs => Syntax.const "_sort" $ classes cs)
495 fun term_of_typ ctxt ty =
497 val show_sorts = Config.get ctxt show_sorts orelse Config.get ctxt show_markup;
501 let val S = #2 (Term_Position.decode_positionS raw_S)
502 in if S = dummyS then t else Syntax.const "_ofsort" $ t $ term_of_sort S end
505 fun term_of (Type (a, Ts)) =
506 Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts)
507 | term_of (TFree (x, S)) =
508 if is_some (Term_Position.decode x) then Syntax.free x
509 else ofsort (Syntax.const "_tfree" $ Syntax.free x) S
510 | term_of (TVar (xi, S)) = ofsort (Syntax.const "_tvar" $ Syntax.var xi) S;
516 fun simple_ast_of ctxt =
518 val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
519 fun ast_of (Const (c, _)) = Ast.Constant c
520 | ast_of (Free (x, _)) = Ast.Variable x
521 | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
522 | ast_of (t as _ $ _) =
523 let val (f, args) = strip_comb t
524 in Ast.mk_appl (ast_of f) (map ast_of args) end
525 | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)]
526 | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
530 (* sort_to_ast and typ_to_ast *)
532 fun ast_of_termT ctxt trf tm =
534 val ctxt' = Config.put show_sorts false ctxt;
535 fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
536 | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
537 | ast_of (Const (a, _)) = trans a []
538 | ast_of (t as _ $ _) =
539 (case strip_comb t of
540 (Const (a, _), args) => trans a args
541 | (f, args) => Ast.Appl (map ast_of (f :: args)))
542 | ast_of t = simple_ast_of ctxt t
543 and trans a args = ast_of (trf a ctxt' dummyT args)
544 handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
547 fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
548 fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
557 fun aprop t = Syntax.const "_aprop" $ t;
560 Type_Annotation.clean (Type_Annotation.fastype_of Ts t) = propT
561 handle TERM _ => false;
563 fun is_term (Const ("Pure.term", _) $ _) = true
566 fun mark _ (t as Const _) = t
567 | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t
568 | mark Ts (t as Free _) = if is_prop Ts t then aprop t else t
569 | mark Ts (t as Var _) = if is_prop Ts t then aprop t else t
570 | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
571 | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
572 | mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
573 if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1
574 else mark Ts t1 $ mark Ts t2
575 | mark Ts (t as t1 $ t2) =
576 (if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop)
577 (mark Ts t1 $ mark Ts t2);
580 fun prune_types ctxt tm =
582 fun regard t t' seen =
583 if Type_Annotation.is_omitted (Type_Annotation.fastype_of [] t) then (t, seen)
584 else if member (op aconv) seen t then (t', seen)
587 fun prune (t as Const _, seen) = (t, seen)
588 | prune (t as Free (x, T), seen) = regard t (Free (x, Type_Annotation.ignore_type T)) seen
589 | prune (t as Var (xi, T), seen) = regard t (Var (xi, Type_Annotation.ignore_type T)) seen
590 | prune (t as Bound _, seen) = (t, seen)
591 | prune (Abs (x, T, t), seen) =
592 let val (t', seen') = prune (t, seen);
593 in (Abs (x, T, t'), seen') end
594 | prune (t1 $ t2, seen) =
596 val (t1', seen') = prune (t1, seen);
597 val (t2', seen'') = prune (t2, seen');
598 in (t1' $ t2', seen'') end;
599 in #1 (prune (tm, [])) end;
601 fun mark_atoms {structs, fixes} is_syntax_const ctxt tm =
603 val show_structs = Config.get ctxt show_structs;
605 fun mark ((t as Const (c, _)) $ u) =
606 if member (op =) Pure_Thy.token_markers c
607 then t $ u else mark t $ mark u
608 | mark (t $ u) = mark t $ mark u
609 | mark (Abs (x, T, t)) = Abs (x, T, mark t)
610 | mark (t as Const (c, T)) =
611 if is_syntax_const c then t
612 else Const (Lexicon.mark_const c, T)
613 | mark (t as Free (x, T)) =
614 let val i = find_index (fn s => s = x) structs + 1 in
615 if i = 0 andalso member (op =) fixes x then
616 Const (Lexicon.mark_fixed x, T)
617 else if i = 1 andalso not show_structs then
618 Syntax.const "_struct" $ Syntax.const "_indexdefault"
619 else Syntax.const "_free" $ t
621 | mark (t as Var (xi, T)) =
622 if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
623 else Syntax.const "_var" $ t
629 fun term_to_ast idents is_syntax_const ctxt trf tm =
631 val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
632 val show_markup = Config.get ctxt show_markup;
635 (case strip_comb tm of
636 (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
637 | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
638 Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
639 | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
640 Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
641 | ((c as Const ("_bound", B)), Free (x, T) :: ts) =>
644 if show_markup andalso not show_types orelse B <> dummyT then T
646 in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
647 | (Const ("_idtdummy", T), ts) =>
648 Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
649 | (const as Const (c, T), ts) => trans c (Type_Annotation.smash T) ts
650 | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
652 and trans a T args = ast_of (trf a ctxt T args)
653 handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
658 if show_markup andalso not show_types
659 then Type_Annotation.clean T0
660 else Type_Annotation.smash T0;
662 if (show_types orelse show_markup) andalso T <> dummyT then
663 Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
664 ast_of_termT ctxt trf (term_of_typ ctxt T)]
665 else simple_ast_of ctxt t
670 |> show_types ? prune_types ctxt
671 |> Variable.revert_bounds ctxt
672 |> mark_atoms idents is_syntax_const ctxt
684 fun free_or_skolem ctxt x =
687 if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
688 then Markup.fixed x else Markup.intensify;
691 then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
692 else ([m, Markup.free], x)
695 fun var_or_skolem s =
696 (case Lexicon.read_variable s of
698 (case try Name.dest_skolem x of
699 NONE => (Markup.var, s)
700 | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
701 | NONE => (Markup.var, s));
703 val typing_elem = YXML.output_markup_elem Markup.typing;
704 val sorting_elem = YXML.output_markup_elem Markup.sorting;
706 fun unparse_t t_to_ast prt_t markup ctxt t =
708 val show_markup = Config.get ctxt show_markup;
709 val show_sorts = Config.get ctxt show_sorts;
710 val show_types = Config.get ctxt show_types orelse show_sorts;
712 val syn = Proof_Context.syn_of ctxt;
713 val prtabs = Syntax.prtabs syn;
714 val trf = Syntax.print_ast_translation syn;
716 fun markup_extern c =
717 (case Syntax.lookup_const syn c of
719 | SOME b => markup_extern b
720 | NONE => c |> Lexicon.unmark
721 {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
722 case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
723 case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
724 case_fixed = fn x => free_or_skolem ctxt x,
725 case_default = fn x => ([], x)});
727 fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
728 | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
729 | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
730 | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
731 | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad, x))
732 | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
733 | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
734 | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
735 | token_trans _ _ = NONE;
737 fun markup_trans a [Ast.Variable x] = token_trans a x
738 | markup_trans "_constrain" [t, ty] = constrain_trans t ty
739 | markup_trans "_idtyp" [t, ty] = constrain_trans t ty
740 | markup_trans "_ofsort" [ty, s] = ofsort_trans ty s
741 | markup_trans _ _ = NONE
743 and constrain_trans t ty =
744 if show_markup andalso not show_types then
746 val ((bg1, bg2), en) = typing_elem;
747 val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
748 in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end
751 and ofsort_trans ty s =
752 if show_markup andalso not show_sorts then
754 val ((bg1, bg2), en) = sorting_elem;
755 val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
756 in SOME (Pretty.raw_markup (bg, en) (0, [pretty_typ_ast Markup.empty ty])) end
759 and pretty_typ_ast m ast = ast
760 |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern
763 and pretty_ast m ast = ast
764 |> prt_t ctxt prtabs trf markup_trans markup_extern
767 t_to_ast ctxt (Syntax.print_translation syn) t
768 |> Ast.normalize ctxt (Syntax.print_rules syn)
774 val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast (Markup.language_sort false);
775 val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast (Markup.language_type false);
777 fun unparse_term ctxt =
779 val thy = Proof_Context.theory_of ctxt;
780 val syn = Proof_Context.syn_of ctxt;
781 val idents = Local_Syntax.idents_of (Proof_Context.syntax_of ctxt);
783 unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
784 (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
785 (Markup.language_term false) ctxt
794 (* type propositions *)
796 fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
797 Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
798 | type_prop_tr' ctxt T [t] =
799 Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
800 | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
803 (* type reflection *)
805 fun type_tr' ctxt (Type ("itself", [T])) ts =
806 Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts)
807 | type_tr' _ _ _ = raise Match;
810 (* type constraints *)
812 fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
813 Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts)
814 | type_constraint_tr' _ _ _ = raise Match;
817 (* authentic syntax *)
819 fun const_ast_tr intern ctxt asts =
821 [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
823 val pos = the_default Position.none (Term_Position.decode p);
824 val (c', _) = decode_const ctxt (c, [pos]);
825 val d = if intern then Lexicon.mark_const c' else c;
826 in Ast.Appl [Ast.Constant "_constrain", Ast.Constant d, T] end
827 | _ => raise Ast.AST ("const_ast_tr", asts));
830 (* setup translations *)
833 (Sign.parse_ast_translation
834 [("_context_const", const_ast_tr true),
835 ("_context_xconst", const_ast_tr false)] #>
836 Sign.typed_print_translation
837 [("_type_prop", type_prop_tr'),
838 ("\\<^const>TYPE", type_tr'),
839 ("_type_constraint_", type_constraint_tr')]);
843 (** check/uncheck **)
845 (* context-sensitive (un)checking *)
847 type key = int * bool;
849 structure Checks = Generic_Data
851 type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
853 ((key * ((string * typ check) * stamp) list) list *
854 (key * ((string * term check) * stamp) list) list);
855 val empty = ([], []);
857 fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
858 (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
859 AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
862 fun print_checks ctxt =
864 fun split_checks checks =
865 List.partition (fn ((_, un), _) => not un) checks
866 |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
867 #> sort (int_ord o pairself fst));
868 fun pretty_checks kind checks =
869 checks |> map (fn (i, names) => Pretty.block
870 [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
871 Pretty.brk 1, Pretty.strs names]);
873 val (typs, terms) = Checks.get (Context.Proof ctxt);
874 val (typ_checks, typ_unchecks) = split_checks typs;
875 val (term_checks, term_unchecks) = split_checks terms;
877 pretty_checks "typ_checks" typ_checks @
878 pretty_checks "term_checks" term_checks @
879 pretty_checks "typ_unchecks" typ_unchecks @
880 pretty_checks "term_unchecks" term_unchecks
881 end |> Pretty.chunks |> Pretty.writeln;
886 fun context_check which (key: key) name f =
887 Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
889 fun simple_check eq f xs ctxt =
890 let val xs' = f ctxt xs
891 in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
895 fun typ_check' stage = context_check apfst (stage, false);
896 fun term_check' stage = context_check apsnd (stage, false);
897 fun typ_uncheck' stage = context_check apfst (stage, true);
898 fun term_uncheck' stage = context_check apsnd (stage, true);
900 fun typ_check key name f = typ_check' key name (simple_check (op =) f);
901 fun term_check key name f = term_check' key name (simple_check (op aconv) f);
902 fun typ_uncheck key name f = typ_uncheck' key name (simple_check (op =) f);
903 fun term_uncheck key name f = term_uncheck' key name (simple_check (op aconv) f);
910 fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
911 fun check_all fs = perhaps_apply (map check_stage fs);
913 fun check which uncheck ctxt0 xs0 =
915 val funs = which (Checks.get (Context.Proof ctxt0))
916 |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
917 |> Library.sort (int_ord o pairself fst) |> map snd
918 |> not uncheck ? map rev;
919 in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
921 val apply_typ_check = check fst false;
922 val apply_term_check = check snd false;
923 val apply_typ_uncheck = check fst true;
924 val apply_term_uncheck = check snd true;
928 fun check_typs ctxt raw_tys =
930 val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
931 val _ = Context_Position.if_visible ctxt Output.report sorting_report;
934 |> apply_typ_check ctxt
935 |> Term_Sharing.typs (Proof_Context.theory_of ctxt)
938 fun check_terms ctxt raw_ts =
940 val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts;
941 val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts';
943 val tys = map (Logic.mk_type o snd) ps;
944 val (ts', tys') = ts @ tys
945 |> apply_term_check ctxt
948 fold2 (fn (pos, _) => fn ty =>
949 if Position.is_reported pos then
950 cons (Position.reported_text pos Markup.typing
951 (Syntax.string_of_typ ctxt (Logic.dest_type ty)))
955 val _ = Context_Position.if_visible ctxt Output.report (sorting_report ^ typing_report);
956 in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
958 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
960 val uncheck_typs = apply_typ_uncheck;
961 val uncheck_terms = apply_term_uncheck;
966 (* standard phases *)
969 (typ_check 0 "standard" Proof_Context.standard_typ_check #>
970 term_check 0 "standard"
971 (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
972 term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
973 term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
977 (** install operations **)
979 val _ = Syntax.install_operations
980 {parse_sort = parse_sort,
981 parse_typ = parse_typ,
982 parse_term = parse_term false,
983 parse_prop = parse_term true,
984 unparse_sort = unparse_sort,
985 unparse_typ = unparse_typ,
986 unparse_term = unparse_term,
987 check_typs = check_typs,
988 check_terms = check_terms,
989 check_props = check_props,
990 uncheck_typs = uncheck_typs,
991 uncheck_terms = uncheck_terms};