32 val theorems_of: Proof.context -> thm list NameSpace.table |
32 val theorems_of: Proof.context -> thm list NameSpace.table |
33 val fact_index_of: Proof.context -> FactIndex.T |
33 val fact_index_of: Proof.context -> FactIndex.T |
34 val transfer: theory -> Proof.context -> Proof.context |
34 val transfer: theory -> Proof.context -> Proof.context |
35 val theory: (theory -> theory) -> Proof.context -> Proof.context |
35 val theory: (theory -> theory) -> Proof.context -> Proof.context |
36 val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context |
36 val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context |
37 val pretty_term: Proof.context -> term -> Pretty.T |
37 val pp: Proof.context -> Pretty.pp |
38 val pretty_term_abbrev: Proof.context -> term -> Pretty.T |
38 val pretty_term_abbrev: Proof.context -> term -> Pretty.T |
39 val pretty_typ: Proof.context -> typ -> Pretty.T |
|
40 val pretty_sort: Proof.context -> sort -> Pretty.T |
|
41 val pretty_classrel: Proof.context -> class list -> Pretty.T |
|
42 val pretty_arity: Proof.context -> arity -> Pretty.T |
|
43 val pp: Proof.context -> Pretty.pp |
|
44 val pretty_thm_legacy: thm -> Pretty.T |
39 val pretty_thm_legacy: thm -> Pretty.T |
45 val pretty_thm: Proof.context -> thm -> Pretty.T |
40 val pretty_thm: Proof.context -> thm -> Pretty.T |
46 val pretty_thms: Proof.context -> thm list -> Pretty.T |
41 val pretty_thms: Proof.context -> thm list -> Pretty.T |
47 val pretty_fact: Proof.context -> string * thm list -> Pretty.T |
42 val pretty_fact: Proof.context -> string * thm list -> Pretty.T |
48 val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T |
43 val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T |
49 val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T |
44 val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T |
50 val string_of_typ: Proof.context -> typ -> string |
|
51 val string_of_term: Proof.context -> term -> string |
|
52 val string_of_thm: Proof.context -> thm -> string |
45 val string_of_thm: Proof.context -> thm -> string |
53 val read_typ: Proof.context -> string -> typ |
46 val read_typ: Proof.context -> string -> typ |
54 val read_typ_syntax: Proof.context -> string -> typ |
47 val read_typ_syntax: Proof.context -> string -> typ |
55 val read_typ_abbrev: Proof.context -> string -> typ |
48 val read_typ_abbrev: Proof.context -> string -> typ |
56 val cert_typ: Proof.context -> typ -> typ |
49 val cert_typ: Proof.context -> typ -> typ |
299 |
292 |
300 |
293 |
301 |
294 |
302 (** pretty printing **) |
295 (** pretty printing **) |
303 |
296 |
304 local |
297 (*pp operations -- deferred evaluation*) |
305 |
298 fun pp ctxt = Pretty.pp |
306 fun rewrite_term thy rews t = |
299 (fn x => Syntax.pretty_term ctxt x, |
307 if can Term.type_of t then Pattern.rewrite_term thy rews [] t else t; |
300 fn x => Syntax.pretty_typ ctxt x, |
308 |
301 fn x => Syntax.pretty_sort ctxt x, |
309 fun pretty_term' abbrevs ctxt t = |
302 fn x => Syntax.pretty_classrel ctxt x, |
310 let |
303 fn x => Syntax.pretty_arity ctxt x); |
311 val thy = theory_of ctxt; |
304 |
312 val syntax = syntax_of ctxt; |
305 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt); |
313 val consts = consts_of ctxt; |
|
314 val do_abbrevs = abbrevs andalso not (print_mode_active "no_abbrevs"); |
|
315 val t' = t |
|
316 |> do_abbrevs ? rewrite_term thy (Consts.abbrevs_of consts (print_mode_value () @ [""])) |
|
317 |> do_abbrevs ? rewrite_term thy (Consts.abbrevs_of consts [Syntax.internalM]) |
|
318 |> Sign.extern_term (Consts.extern_early consts) thy |
|
319 |> LocalSyntax.extern_term syntax; |
|
320 in Sign.pretty_term' ctxt (LocalSyntax.syn_of syntax) (Consts.extern consts) t' end; |
|
321 |
|
322 in |
|
323 |
|
324 val pretty_term = pretty_term' true; |
|
325 val pretty_term_abbrev = pretty_term' false; |
|
326 |
|
327 end; |
|
328 |
|
329 fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T; |
|
330 fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S; |
|
331 fun pretty_classrel ctxt cs = Sign.pretty_classrel (theory_of ctxt) cs; |
|
332 fun pretty_arity ctxt ar = Sign.pretty_arity (theory_of ctxt) ar; |
|
333 |
|
334 fun pp ctxt = Pretty.pp (pretty_term ctxt, pretty_typ ctxt, pretty_sort ctxt, |
|
335 pretty_classrel ctxt, pretty_arity ctxt); |
|
336 |
306 |
337 fun pretty_thm_legacy th = |
307 fun pretty_thm_legacy th = |
338 let val thy = Thm.theory_of_thm th |
308 let val thy = Thm.theory_of_thm th |
339 in Display.pretty_thm_aux (pp (init thy)) true false [] th end; |
309 in Display.pretty_thm_aux (pp (init thy)) true false [] th end; |
340 |
310 |
356 (ProofSyntax.term_of_proof prf); |
326 (ProofSyntax.term_of_proof prf); |
357 |
327 |
358 fun pretty_proof_of ctxt full th = |
328 fun pretty_proof_of ctxt full th = |
359 pretty_proof ctxt (ProofSyntax.proof_of full th); |
329 pretty_proof ctxt (ProofSyntax.proof_of full th); |
360 |
330 |
361 val string_of_typ = Pretty.string_of oo pretty_typ; |
|
362 val string_of_term = Pretty.string_of oo pretty_term; |
|
363 val string_of_thm = Pretty.string_of oo pretty_thm; |
331 val string_of_thm = Pretty.string_of oo pretty_thm; |
364 |
332 |
365 |
333 |
366 |
334 |
367 (** prepare types **) |
335 (** prepare types **) |
461 in |
429 in |
462 |
430 |
463 fun expand_abbrevs ctxt = certify_consts ctxt #> expand_binds ctxt; |
431 fun expand_abbrevs ctxt = certify_consts ctxt #> expand_binds ctxt; |
464 |
432 |
465 end; |
433 end; |
|
434 |
|
435 |
|
436 fun contract_abbrevs ctxt t = |
|
437 let |
|
438 val thy = theory_of ctxt; |
|
439 val consts = consts_of ctxt; |
|
440 val Mode {abbrev, ...} = get_mode ctxt; |
|
441 in |
|
442 if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) |
|
443 then t |
|
444 else |
|
445 t |
|
446 |> Pattern.rewrite_term thy (Consts.abbrevs_of consts (print_mode_value () @ [""])) [] |
|
447 |> Pattern.rewrite_term thy (Consts.abbrevs_of consts [Syntax.internalM]) [] |
|
448 end; |
466 |
449 |
467 |
450 |
468 (* patterns *) |
451 (* patterns *) |
469 |
452 |
470 fun prepare_patternT ctxt = |
453 fun prepare_patternT ctxt = |
609 map (prepare_patternT ctxt); |
592 map (prepare_patternT ctxt); |
610 |
593 |
611 fun standard_term_check ctxt = |
594 fun standard_term_check ctxt = |
612 standard_infer_types ctxt #> |
595 standard_infer_types ctxt #> |
613 map (expand_abbrevs ctxt); |
596 map (expand_abbrevs ctxt); |
614 |
597 |
615 fun add_check add f = Context.add_setup |
598 fun standard_term_uncheck ctxt = |
616 (Context.theory_map (add (fn xs => fn ctxt => (f ctxt xs, ctxt)))); |
599 map (contract_abbrevs ctxt); |
|
600 |
|
601 fun add what f = Context.add_setup |
|
602 (Context.theory_map (what (fn xs => fn ctxt => (f ctxt xs, ctxt)))); |
617 |
603 |
618 in |
604 in |
619 |
605 |
620 val _ = add_check (Syntax.add_typ_check 0 "standard") standard_typ_check; |
606 val _ = add (Syntax.add_typ_check 0 "standard") standard_typ_check; |
621 val _ = add_check (Syntax.add_term_check 0 "standard") standard_term_check; |
607 val _ = add (Syntax.add_term_check 0 "standard") standard_term_check; |
622 val _ = add_check (Syntax.add_term_check 100 "fixate") prepare_patterns; |
608 val _ = add (Syntax.add_term_check 100 "fixate") prepare_patterns; |
|
609 |
|
610 val _ = add (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck; |
623 |
611 |
624 end; |
612 end; |
625 |
613 |
626 |
614 |
627 (* inferred types of parameters *) |
615 (* inferred types of parameters *) |
677 val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt; |
665 val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt; |
678 val read = Syntax.standard_parse_term (pp ctxt) check get_sort map_const map_free map_type |
666 val read = Syntax.standard_parse_term (pp ctxt) check get_sort map_const map_free map_type |
679 map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) ((#1 (TypeInfer.paramify_dummies T 0))); |
667 map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) ((#1 (TypeInfer.paramify_dummies T 0))); |
680 in read str end; |
668 in read str end; |
681 |
669 |
|
670 |
|
671 fun unparse_sort ctxt S = |
|
672 Syntax.standard_unparse_sort ctxt (syn_of ctxt) (Sign.extern_sort (theory_of ctxt) S); |
|
673 |
|
674 fun unparse_typ ctxt T = |
|
675 Syntax.standard_unparse_typ ctxt (syn_of ctxt) (Sign.extern_typ (theory_of ctxt) T); |
|
676 |
|
677 fun unparse_term ctxt t = |
|
678 let |
|
679 val thy = theory_of ctxt; |
|
680 val syntax = syntax_of ctxt; |
|
681 val consts = consts_of ctxt; |
|
682 in |
|
683 t |
|
684 |> Sign.extern_term (Consts.extern_early consts) thy |
|
685 |> LocalSyntax.extern_term syntax |
|
686 |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (LocalSyntax.syn_of syntax) |
|
687 (Context.exists_name Context.CPureN thy) |
|
688 end; |
|
689 |
682 in |
690 in |
683 |
691 |
684 val _ = Syntax.install_operations |
692 val _ = Syntax.install_operations |
685 {parse_sort = parse_sort, |
693 {parse_sort = parse_sort, |
686 parse_typ = parse_typ, |
694 parse_typ = parse_typ, |
687 parse_term = parse_term dummyT, |
695 parse_term = parse_term dummyT, |
688 parse_prop = parse_term propT, |
696 parse_prop = parse_term propT, |
689 unparse_sort = undefined, |
697 unparse_sort = unparse_sort, |
690 unparse_typ = undefined, |
698 unparse_typ = unparse_typ, |
691 unparse_term = undefined}; |
699 unparse_term = unparse_term}; |
692 |
700 |
693 end; |
701 end; |
694 |
702 |
695 |
703 |
696 |
704 |
1237 |
1245 |
1238 (* local contexts *) |
1246 (* local contexts *) |
1239 |
1247 |
1240 fun pretty_cases ctxt = |
1248 fun pretty_cases ctxt = |
1241 let |
1249 let |
1242 val prt_term = pretty_term ctxt; |
1250 val prt_term = Syntax.pretty_term ctxt; |
1243 |
1251 |
1244 fun prt_let (xi, t) = Pretty.block |
1252 fun prt_let (xi, t) = Pretty.block |
1245 [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1, |
1253 [Pretty.quote (prt_term (Var (xi, Term.fastype_of t))), Pretty.str " =", Pretty.brk 1, |
1246 Pretty.quote (prt_term t)]; |
1254 Pretty.quote (prt_term t)]; |
1247 |
1255 |
1279 |
1287 |
1280 fun pretty_ctxt ctxt = |
1288 fun pretty_ctxt ctxt = |
1281 if ! prems_limit < 0 andalso not (! debug) then [] |
1289 if ! prems_limit < 0 andalso not (! debug) then [] |
1282 else |
1290 else |
1283 let |
1291 let |
1284 val prt_term = pretty_term ctxt; |
1292 val prt_term = Syntax.pretty_term ctxt; |
1285 |
1293 |
1286 (*structures*) |
1294 (*structures*) |
1287 val structs = LocalSyntax.structs_of (syntax_of ctxt); |
1295 val structs = LocalSyntax.structs_of (syntax_of ctxt); |
1288 val prt_structs = if null structs then [] |
1296 val prt_structs = if null structs then [] |
1289 else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 :: |
1297 else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 :: |
1312 |
1320 |
1313 (* main context *) |
1321 (* main context *) |
1314 |
1322 |
1315 fun pretty_context ctxt = |
1323 fun pretty_context ctxt = |
1316 let |
1324 let |
1317 val prt_term = pretty_term ctxt; |
1325 val prt_term = Syntax.pretty_term ctxt; |
1318 val prt_typ = pretty_typ ctxt; |
1326 val prt_typ = Syntax.pretty_typ ctxt; |
1319 val prt_sort = pretty_sort ctxt; |
1327 val prt_sort = Syntax.pretty_sort ctxt; |
1320 |
1328 |
1321 (*theory*) |
1329 (*theory*) |
1322 val pretty_thy = Pretty.block |
1330 val pretty_thy = Pretty.block |
1323 [Pretty.str "theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)]; |
1331 [Pretty.str "theory:", Pretty.brk 1, Context.pretty_thy (theory_of ctxt)]; |
1324 |
1332 |