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 list * term Exn.result -> Position.report 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 can Name.dest_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 list);
142 fun report pos = Position.store_reports reports [pos];
146 NONE => Ast.mk_appl (Ast.Constant a) args
147 | SOME f => f ctxt args);
149 fun asts_of_token tok =
150 if Lexicon.valued_token tok
151 then [Ast.Variable (Lexicon.str_of_token tok)]
154 fun ast_of_position tok =
155 Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok));
157 fun ast_of_dummy a tok =
158 Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
160 fun asts_of_position c tok =
161 [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
163 and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
165 val pos = Lexicon.pos_of_token tok;
166 val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok)
167 handle ERROR msg => error (msg ^ Position.here pos);
168 val _ = report pos (markup_class ctxt) c;
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;
174 Proof_Context.read_type_name_proper ctxt false (Lexicon.str_of_token tok)
175 handle ERROR msg => error (msg ^ Position.here pos);
176 val _ = report pos (markup_type ctxt) c;
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_term _ (result as (_: Position.report list, Exn.Exn _)) = result
226 | decode_term ctxt (reports0, Exn.Res tm) =
229 ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a)))
230 handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a));
231 val get_free = Proof_Context.intern_skolem ctxt;
233 val reports = Unsynchronized.ref reports0;
234 fun report ps = Position.store_reports reports ps;
236 fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
237 (case Term_Position.decode_position typ of
238 SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
239 | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
240 | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
241 (case Term_Position.decode_position typ of
242 SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t)
243 | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
244 | decode _ qs bs (Abs (x, T, t)) =
247 val _ = report qs (markup_bound true qs) (x, id);
248 in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end
249 | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
250 | decode ps _ _ (Const (a, T)) =
251 (case try Lexicon.unmark_fixed a of
252 SOME x => (report ps (markup_free ctxt) x; Free (x, T))
256 (case try Lexicon.unmark_const a of
258 | NONE => snd (get_const a));
259 val _ = report ps (markup_const ctxt) c;
261 | decode ps _ _ (Free (a, T)) =
262 (case (get_free a, get_const a) of
263 (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
264 | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
266 if Long_Name.is_qualified c
267 then (report ps (markup_const ctxt) c; Const (c, T))
268 else (report ps (markup_free ctxt) c; Free (c, T)))
269 | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
270 | decode ps _ bs (t as Bound i) =
271 (case try (nth bs) i of
272 SOME (qs, (x, id)) => (report ps (markup_bound false qs) (x, id); t)
275 val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
276 in (! reports, tm') end;
284 fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
285 fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
287 fun report_result ctxt pos ambig_msgs results =
288 (case (proper_results results, failed_results results) of
289 ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
290 | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
292 if null ambig_msgs then
293 error ("Parse error: ambiguous syntax" ^ Position.here pos)
294 else error (cat_lines ambig_msgs));
299 fun parse_asts ctxt raw root (syms, pos) =
301 val syn = Proof_Context.syn_of ctxt;
302 val ast_tr = Syntax.parse_ast_translation syn;
304 val toks = Syntax.tokenize syn raw syms;
305 val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
307 val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
310 implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
311 val len = length pts;
313 val limit = Config.get ctxt Syntax.ambiguity_limit;
318 (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
319 "\nproduces " ^ string_of_int len ^ " parse trees" ^
320 (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
321 map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))];
323 in (ambig_msgs, map (parsetree_to_ast ctxt ast_tr) pts) end;
325 fun parse_tree ctxt root input =
327 val syn = Proof_Context.syn_of ctxt;
328 val tr = Syntax.parse_translation syn;
329 val parse_rules = Syntax.parse_rules syn;
330 val (ambig_msgs, asts) = parse_asts ctxt false root input;
332 (map o apsnd o Exn.maps_result)
333 (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts;
334 in (ambig_msgs, results) end;
337 (* parse logical entities *)
339 fun parse_failed ctxt pos msg kind =
340 cat_error msg ("Failed to parse " ^ kind ^
341 Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
343 fun parse_sort ctxt =
344 Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
346 parse_tree ctxt "sort" (syms, pos)
347 |> uncurry (report_result ctxt pos)
349 |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
350 handle ERROR msg => parse_failed ctxt pos msg "sort");
353 Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
355 parse_tree ctxt "type" (syms, pos)
356 |> uncurry (report_result ctxt pos)
358 handle ERROR msg => parse_failed ctxt pos msg "type");
360 fun parse_term is_prop ctxt =
362 val (markup, kind, root, constrain) =
364 then (Markup.prop, "proposition", "prop", Type.constraint propT)
365 else (Markup.term, "term", Config.get ctxt Syntax.root, I);
366 val decode = constrain o Term_XML.Decode.term;
368 Syntax.parse_token ctxt decode markup
371 val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt);
372 val parsed_len = length (proper_results results);
374 val ambiguity_warning = Config.get ctxt Syntax.ambiguity_warning;
375 val limit = Config.get ctxt Syntax.ambiguity_limit;
377 (*brute-force disambiguation via type-inference*)
378 fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t)
379 handle exn as ERROR _ => Exn.Exn exn;
382 if parsed_len > 1 then
383 (grouped 10 (Par_List.map_name "Syntax_Phases.parse_term") o apsnd o Exn.maps_result)
386 val reports' = fst (hd results');
388 val errs = map snd (failed_results results');
389 val checked = map snd (proper_results results');
390 val checked_len = length checked;
392 val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
394 if checked_len = 0 then
395 report_result ctxt pos []
396 [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))]
397 else if checked_len = 1 then
398 (if parsed_len > 1 andalso ambiguity_warning then
399 Context_Position.if_visible ctxt warning
400 (cat_lines (ambig_msgs @
401 ["Fortunately, only one parse tree is type correct" ^
402 Position.here (Position.reset_range pos) ^
403 ",\nbut you may still want to disambiguate your grammar or your input."]))
404 else (); report_result ctxt pos [] results')
406 report_result ctxt pos []
407 [(reports', Exn.Exn (ERROR (cat_lines (ambig_msgs @
408 (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^
409 (if checked_len <= limit then ""
410 else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
411 map show_term (take limit checked))))))]
412 end handle ERROR msg => parse_failed ctxt pos msg kind)
416 (* parse_ast_pattern *)
418 fun parse_ast_pattern ctxt (root, str) =
420 val syn = Proof_Context.syn_of ctxt;
422 val reports = Unsynchronized.ref ([]: Position.report list);
423 fun report ps = Position.store_reports reports ps;
425 fun decode_const ps c = (report ps (markup_entity ctxt) c; Ast.Constant c);
426 fun decode_var ps x = (report ps (fn () => [Markup.name x Markup.free]) (); Ast.Variable x);
427 fun decode_appl ps asts = Ast.Appl (map (decode ps) asts)
428 and decode ps (Ast.Constant c) = decode_const ps c
429 | decode ps (Ast.Variable x) =
430 if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
431 then decode_const ps x
433 | decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) =
434 if member (op =) Term_Position.markers c then
435 (case Term_Position.decode x of
436 SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args)
437 | NONE => decode_appl ps asts)
438 else decode_appl ps asts
439 | decode ps (Ast.Appl asts) = decode_appl ps asts;
441 val (syms, pos) = Syntax.read_token str;
443 parse_asts ctxt true root (syms, pos)
444 |> uncurry (report_result ctxt pos)
446 val _ = Context_Position.reports ctxt (! reports);
451 (** encode parse trees **)
457 val class = Syntax.const o Lexicon.mark_class;
459 fun classes [c] = class c
460 | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
463 [] => Syntax.const "_topsort"
465 | cs => Syntax.const "_sort" $ classes cs)
471 fun term_of_typ ctxt ty =
473 val show_sort_constraint = Printer.show_sort_constraint ctxt;
476 if show_sort_constraint then
477 let val S = #2 (Term_Position.decode_positionS raw_S)
478 in if S = dummyS then t else Syntax.const "_ofsort" $ t $ term_of_sort S end
481 fun term_of (Type (a, Ts)) =
482 Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts)
483 | term_of (TFree (x, S)) =
484 if is_some (Term_Position.decode x) then Syntax.free x
485 else ofsort (Syntax.const "_tfree" $ Syntax.free x) S
486 | term_of (TVar (xi, S)) = ofsort (Syntax.const "_tvar" $ Syntax.var xi) S;
492 fun simple_ast_of ctxt =
494 val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
495 fun ast_of (Const (c, _)) = Ast.Constant c
496 | ast_of (Free (x, _)) = Ast.Variable x
497 | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
498 | ast_of (t as _ $ _) =
499 let val (f, args) = strip_comb t
500 in Ast.mk_appl (ast_of f) (map ast_of args) end
501 | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)]
502 | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
506 (* sort_to_ast and typ_to_ast *)
508 fun ast_of_termT ctxt trf tm =
510 val ctxt' = Config.put show_sorts false ctxt;
511 fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
512 | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
513 | ast_of (Const (a, _)) = trans a []
514 | ast_of (t as _ $ _) =
515 (case strip_comb t of
516 (Const (a, _), args) => trans a args
517 | (f, args) => Ast.Appl (map ast_of (f :: args)))
518 | ast_of t = simple_ast_of ctxt t
519 and trans a args = ast_of (trf a ctxt' dummyT args)
520 handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
523 fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S);
524 fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T);
533 fun aprop t = Syntax.const "_aprop" $ t;
536 fastype_of1 (Ts, t) = propT handle TERM _ => false;
538 fun is_term (Const ("Pure.term", _) $ _) = true
541 fun mark _ (t as Const _) = t
542 | mark Ts (t as Const ("_bound", _) $ u) = if is_prop Ts u then aprop t else t
543 | mark _ (t as Free (x, T)) = if T = propT then aprop (Syntax.free x) else t
544 | mark _ (t as Var (xi, T)) = if T = propT then aprop (Syntax.var xi) else t
545 | mark Ts (t as Bound _) = if is_prop Ts t then aprop t else t
546 | mark Ts (Abs (x, T, t)) = Abs (x, T, mark (T :: Ts) t)
547 | mark Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
548 if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ mark Ts t1
549 else mark Ts t1 $ mark Ts t2
550 | mark Ts (t as t1 $ t2) =
551 (if is_Const (Term.head_of t) orelse not (is_prop Ts t) then I else aprop)
552 (mark Ts t1 $ mark Ts t2);
555 fun prune_types ctxt tm =
557 val show_free_types = Config.get ctxt show_free_types;
559 fun prune (t_seen as (Const _, _)) = t_seen
560 | prune (t as Free (x, ty), seen) =
561 if ty = dummyT then (t, seen)
562 else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
564 | prune (t as Var (xi, ty), seen) =
565 if ty = dummyT then (t, seen)
566 else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
568 | prune (t_seen as (Bound _, _)) = t_seen
569 | prune (Abs (x, ty, t), seen) =
570 let val (t', seen') = prune (t, seen);
571 in (Abs (x, ty, t'), seen') end
572 | prune (t1 $ t2, seen) =
574 val (t1', seen') = prune (t1, seen);
575 val (t2', seen'') = prune (t2, seen');
576 in (t1' $ t2', seen'') end;
577 in #1 (prune (tm, [])) end;
579 fun mark_atoms {structs, fixes} is_syntax_const ctxt tm =
581 val show_structs = Config.get ctxt show_structs;
583 fun mark ((t as Const (c, _)) $ u) =
584 if member (op =) Pure_Thy.token_markers c
585 then t $ u else mark t $ mark u
586 | mark (t $ u) = mark t $ mark u
587 | mark (Abs (x, T, t)) = Abs (x, T, mark t)
588 | mark (t as Const (c, T)) =
589 if is_syntax_const c then t
590 else Const (Lexicon.mark_const c, T)
591 | mark (t as Free (x, T)) =
592 let val i = find_index (fn s => s = x) structs + 1 in
593 if i = 0 andalso member (op =) fixes x then
594 Const (Lexicon.mark_fixed x, T)
595 else if i = 1 andalso not show_structs then
596 Syntax.const "_struct" $ Syntax.const "_indexdefault"
597 else Syntax.const "_free" $ t
599 | mark (t as Var (xi, T)) =
600 if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
601 else Syntax.const "_var" $ t
607 fun term_to_ast idents is_syntax_const ctxt trf tm =
609 val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
610 val show_markup = Config.get ctxt show_markup;
613 (case strip_comb tm of
614 (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
615 | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
616 Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
617 | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
618 Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
619 | ((c as Const ("_bound", B)), Free (x, T) :: ts) =>
622 if show_markup andalso not show_types orelse B <> dummyT then T
624 in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
625 | (Const ("_idtdummy", T), ts) =>
626 Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
627 | (const as Const (c, T), ts) => trans c T ts
628 | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
630 and trans a T args = ast_of (trf a ctxt T args)
631 handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
634 if (show_types orelse show_markup) andalso T <> dummyT then
635 Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t,
636 ast_of_termT ctxt trf (term_of_typ ctxt T)]
637 else simple_ast_of ctxt t;
641 |> show_types ? prune_types ctxt
642 |> mark_atoms idents is_syntax_const ctxt
654 fun free_or_skolem ctxt x =
657 if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
658 then Markup.fixed x else Markup.intensify;
660 if can Name.dest_skolem x
661 then ([m, Markup.skolem], Variable.revert_fixed ctxt x)
662 else ([m, Markup.free], x)
665 fun var_or_skolem s =
666 (case Lexicon.read_variable s of
668 (case try Name.dest_skolem x of
669 NONE => (Markup.var, s)
670 | SOME x' => (Markup.skolem, Term.string_of_vname (x', i)))
671 | NONE => (Markup.var, s));
673 val typing_elem = YXML.output_markup_elem Markup.typing;
674 val sorting_elem = YXML.output_markup_elem Markup.sorting;
676 fun unparse_t t_to_ast prt_t markup ctxt t =
678 val show_markup = Config.get ctxt show_markup;
679 val show_sorts = Config.get ctxt show_sorts;
680 val show_types = Config.get ctxt show_types orelse show_sorts;
682 val syn = Proof_Context.syn_of ctxt;
683 val prtabs = Syntax.prtabs syn;
684 val trf = Syntax.print_ast_translation syn;
686 fun markup_extern c =
687 (case Syntax.lookup_const syn c of
689 | SOME b => markup_extern b
690 | NONE => c |> Lexicon.unmark
691 {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
692 case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
693 case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
694 case_fixed = fn x => free_or_skolem ctxt x,
695 case_default = fn x => ([], x)});
697 fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
698 | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
699 | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
700 | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
701 | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad, x))
702 | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
703 | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
704 | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
705 | token_trans _ _ = NONE;
707 fun markup_trans a [Ast.Variable x] = token_trans a x
708 | markup_trans "_constrain" [t, ty] = constrain_trans t ty
709 | markup_trans "_idtyp" [t, ty] = constrain_trans t ty
710 | markup_trans "_ofsort" [ty, s] = ofsort_trans ty s
711 | markup_trans _ _ = NONE
713 and constrain_trans t ty =
714 if show_markup andalso not show_types then
716 val ((bg1, bg2), en) = typing_elem;
717 val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
718 in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end
721 and ofsort_trans ty s =
722 if show_markup andalso not show_sorts then
724 val ((bg1, bg2), en) = sorting_elem;
725 val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
726 in SOME (Pretty.raw_markup (bg, en) (0, [pretty_typ_ast Markup.empty ty])) end
729 and pretty_typ_ast m ast = ast
730 |> Printer.pretty_typ_ast ctxt prtabs trf markup_trans markup_extern
733 and pretty_ast m ast = ast
734 |> prt_t ctxt prtabs trf markup_trans markup_extern
737 t_to_ast ctxt (Syntax.print_translation syn) t
738 |> Ast.normalize ctxt (Syntax.print_rules syn)
744 val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Markup.sort;
745 val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Markup.typ;
747 fun unparse_term ctxt =
749 val thy = Proof_Context.theory_of ctxt;
750 val syn = Proof_Context.syn_of ctxt;
751 val idents = Local_Syntax.idents_of (Proof_Context.syntax_of ctxt);
753 unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
754 (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
764 (* type propositions *)
766 fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
767 Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
768 | type_prop_tr' ctxt T [t] =
769 Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
770 | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts);
773 (* type reflection *)
775 fun type_tr' ctxt (Type ("itself", [T])) ts =
776 Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts)
777 | type_tr' _ _ _ = raise Match;
780 (* type constraints *)
782 fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) =
783 Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts)
784 | type_constraint_tr' _ _ _ = raise Match;
787 (* authentic syntax *)
789 fun const_ast_tr intern ctxt [Ast.Variable c] =
791 val Const (c', _) = Proof_Context.read_const_proper ctxt false c;
792 val d = if intern then Lexicon.mark_const c' else c;
793 in Ast.Constant d end
794 | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] =
795 (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
797 error (msg ^ Position.here (the_default Position.none (Term_Position.decode pos))))
798 | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
801 (* setup translations *)
803 val _ = Context.>> (Context.map_theory
804 (Sign.parse_ast_translation
805 [("_context_const", const_ast_tr true),
806 ("_context_xconst", const_ast_tr false)] #>
807 Sign.typed_print_translation
808 [("_type_prop", type_prop_tr'),
809 ("\\<^const>TYPE", type_tr'),
810 ("_type_constraint_", type_constraint_tr')]));
814 (** check/uncheck **)
816 (* context-sensitive (un)checking *)
818 type key = int * bool;
820 structure Checks = Generic_Data
822 type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
824 ((key * ((string * typ check) * stamp) list) list *
825 (key * ((string * term check) * stamp) list) list);
826 val empty = ([], []);
828 fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
829 (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
830 AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
833 fun print_checks ctxt =
835 fun split_checks checks =
836 List.partition (fn ((_, un), _) => not un) checks
837 |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs))
838 #> sort (int_ord o pairself fst));
839 fun pretty_checks kind checks =
840 checks |> map (fn (i, names) => Pretty.block
841 [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"),
842 Pretty.brk 1, Pretty.strs names]);
844 val (typs, terms) = Checks.get (Context.Proof ctxt);
845 val (typ_checks, typ_unchecks) = split_checks typs;
846 val (term_checks, term_unchecks) = split_checks terms;
848 pretty_checks "typ_checks" typ_checks @
849 pretty_checks "term_checks" term_checks @
850 pretty_checks "typ_unchecks" typ_unchecks @
851 pretty_checks "term_unchecks" term_unchecks
852 end |> Pretty.chunks |> Pretty.writeln;
857 fun context_check which (key: key) name f =
858 Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
860 fun simple_check eq f xs ctxt =
861 let val xs' = f ctxt xs
862 in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
866 fun typ_check' stage = context_check apfst (stage, false);
867 fun term_check' stage = context_check apsnd (stage, false);
868 fun typ_uncheck' stage = context_check apfst (stage, true);
869 fun term_uncheck' stage = context_check apsnd (stage, true);
871 fun typ_check key name f = typ_check' key name (simple_check (op =) f);
872 fun term_check key name f = term_check' key name (simple_check (op aconv) f);
873 fun typ_uncheck key name f = typ_uncheck' key name (simple_check (op =) f);
874 fun term_uncheck key name f = term_uncheck' key name (simple_check (op aconv) f);
881 fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs));
882 fun check_all fs = perhaps_apply (map check_stage fs);
884 fun check which uncheck ctxt0 xs0 =
886 val funs = which (Checks.get (Context.Proof ctxt0))
887 |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE)
888 |> Library.sort (int_ord o pairself fst) |> map snd
889 |> not uncheck ? map rev;
890 in #1 (perhaps (check_all funs) (xs0, ctxt0)) end;
892 val apply_typ_check = check fst false;
893 val apply_term_check = check snd false;
894 val apply_typ_uncheck = check fst true;
895 val apply_term_uncheck = check snd true;
899 fun check_typs ctxt raw_tys =
901 val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
902 val _ = Context_Position.if_visible ctxt Output.report sorting_report;
905 |> apply_typ_check ctxt
906 |> Term_Sharing.typs (Proof_Context.theory_of ctxt)
909 fun check_terms ctxt raw_ts =
911 val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts;
912 val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts';
914 val tys = map (Logic.mk_type o snd) ps;
915 val (ts', tys') = ts @ tys
916 |> apply_term_check ctxt
919 fold2 (fn (pos, _) => fn ty =>
920 if Position.is_reported pos then
921 cons (Position.reported_text pos Markup.typing
922 (Syntax.string_of_typ ctxt (Logic.dest_type ty)))
926 val _ = Context_Position.if_visible ctxt Output.report (sorting_report ^ typing_report);
927 in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
929 fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
931 val uncheck_typs = apply_typ_uncheck;
932 val uncheck_terms = apply_term_uncheck;
937 (* standard phases *)
940 (typ_check 0 "standard" Proof_Context.standard_typ_check #>
941 term_check 0 "standard"
942 (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
943 term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
944 term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
948 (** install operations **)
950 val _ = Syntax.install_operations
951 {parse_sort = parse_sort,
952 parse_typ = parse_typ,
953 parse_term = parse_term false,
954 parse_prop = parse_term true,
955 unparse_sort = unparse_sort,
956 unparse_typ = unparse_typ,
957 unparse_term = unparse_term,
958 check_typs = check_typs,
959 check_terms = check_terms,
960 check_props = check_props,
961 uncheck_typs = uncheck_typs,
962 uncheck_terms = uncheck_terms};