# HG changeset patch # User wenzelm # Date 1124192563 -7200 # Node ID 501c28052aea0834f776baab5533e1619e3528af # Parent f753d6dd9bd0e538928033afa3e0a38c08eacac8 added transfer; adapt local syntax to potential changes of theory syntax; added pretty_proof(_of); diff -r f753d6dd9bd0 -r 501c28052aea src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Aug 16 13:42:42 2005 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Aug 16 13:42:43 2005 +0200 @@ -21,6 +21,7 @@ val prems_of: context -> thm list val fact_index_of: context -> FactIndex.T val init: theory -> context + val transfer: theory -> context -> context val pretty_term: context -> term -> Pretty.T val pretty_typ: context -> typ -> Pretty.T val pretty_sort: context -> sort -> Pretty.T @@ -28,6 +29,8 @@ val pretty_thm: context -> thm -> Pretty.T val pretty_thms: context -> thm list -> Pretty.T val pretty_fact: context -> string * thm list -> Pretty.T + val pretty_proof: context -> Proofterm.proof -> Pretty.T + val pretty_proof_of: context -> bool -> thm -> Pretty.T val string_of_term: context -> term -> string val default_type: context -> string -> typ option val used_types: context -> string list @@ -155,7 +158,7 @@ (** generic proof contexts **) type context = Context.proof; -exception CONTEXT of string * context; +exception CONTEXT = Context.PROOF; val theory_of = Context.theory_of_proof; val sign_of = theory_of; @@ -170,20 +173,21 @@ datatype ctxt = Ctxt of - {syntax: Syntax.syntax * string list * string list, (*syntax with structs and mixfixed*) + {syntax: (Syntax.syntax * Syntax.syntax * (Syntax.syntax -> Syntax.syntax)) * + string list * string list, (*global/local syntax with structs and mixfixed*) asms: - ((cterm list * exporter) list * (*assumes: A ==> _*) - (string * thm list) list) * (*prems: A |- A *) - (string * string) list, (*fixes: !!x. _*) - binds: (term * typ) Vartab.table, (*term bindings*) - thms: NameSpace.naming * (*local thms*) + ((cterm list * exporter) list * (*assumes: A ==> _*) + (string * thm list) list) * (*prems: A |- A *) + (string * string) list, (*fixes: !!x. _*) + binds: (term * typ) Vartab.table, (*term bindings*) + thms: NameSpace.naming * (*local thms*) thm list NameSpace.table * FactIndex.T, - cases: (string * RuleCases.T) list, (*local contexts*) + cases: (string * RuleCases.T) list, (*local contexts*) defs: - typ Vartab.table * (*type constraints*) - sort Vartab.table * (*default sorts*) - string list * (*used type variables*) - term list Symtab.table}; (*type variable occurrences*) + typ Vartab.table * (*type constraints*) + sort Vartab.table * (*default sorts*) + string list * (*used type variables*) + term list Symtab.table}; (*type variable occurrences*) fun make_ctxt (syntax, asms, binds, thms, cases, defs) = Ctxt {syntax = syntax, asms = asms, binds = binds, thms = thms, cases = cases, defs = defs}; @@ -193,8 +197,8 @@ val name = "Isar/context"; type T = ctxt; fun init thy = - make_ctxt ((Sign.syn_of thy, [], []), (([], []), []), Vartab.empty, - (NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [], + make_ctxt (((Sign.syn_of thy, Sign.syn_of thy, I), [], []), (([], []), []), + Vartab.empty, (NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [], (Vartab.empty, Vartab.empty, [], Symtab.empty)); fun print _ _ = (); end); @@ -276,35 +280,55 @@ fun mk trs = map Syntax.mk_trfun trs; +fun extend_syntax thy extend (global_syn, syn, mk_syn) = + let + val thy_syn = Sign.syn_of thy; + val mk_syn' = extend o mk_syn; + val (global_syn', syn') = + if Syntax.eq_syntax (global_syn, thy_syn) + then (global_syn, extend syn) + else (thy_syn, mk_syn' thy_syn); (*potentially expensive*) + in (global_syn', syn', mk_syn') end; + in -fun add_syntax decls ctxt = ctxt |> - map_context (fn ((syn, structs, mixfixed), asms, binds, thms, cases, defs) => - let - val is_logtype = Sign.is_logtype (theory_of ctxt); - val structs' = structs @ List.mapPartial prep_struct decls; - val mxs = List.mapPartial prep_mixfix decls; - val (fixed, mxs_output) = Library.split_list (List.mapPartial prep_mixfix' decls); - val trs = map fixed_tr fixed; - val syn' = syn - |> Syntax.extend_const_gram is_logtype ("", false) mxs_output - |> Syntax.extend_const_gram is_logtype ("", true) mxs - |> Syntax.extend_trfuns ([], mk trs, [], []); - in ((syn', structs', fixed @ mixfixed), asms, binds, thms, cases, defs) end); +fun add_syntax decls ctxt = ctxt |> map_context (fn (syntax, asms, binds, thms, cases, defs) => + let + val (syns, structs, mixfixed) = syntax; + val thy = theory_of ctxt; + + val is_logtype = Sign.is_logtype thy; + val structs' = structs @ List.mapPartial prep_struct decls; + val mxs = List.mapPartial prep_mixfix decls; + val (fixed, mxs_output) = Library.split_list (List.mapPartial prep_mixfix' decls); + val trs = map fixed_tr fixed; -fun syn_of ctxt = + val extend = + Syntax.extend_const_gram is_logtype ("", false) mxs_output + #> Syntax.extend_const_gram is_logtype ("", true) mxs + #> Syntax.extend_trfuns ([], mk trs, [], []); + val syns' = extend_syntax thy extend syns; + in ((syns', structs', fixed @ mixfixed), asms, binds, thms, cases, defs) end); + +fun syn_of' thy ctxt = let - val (syn, structs, _) = syntax_of ctxt; + val (syns, structs, _) = syntax_of ctxt; val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs; - in syn |> Syntax.extend_trfuns (mk atrs, mk trs, mk trs', mk atrs') end; + val extend = Syntax.extend_trfuns (mk atrs, mk trs, mk trs', mk atrs'); + in #2 (extend_syntax thy extend syns) end; + +fun syn_of ctxt = syn_of' (theory_of ctxt) ctxt; end; +fun transfer thy = add_syntax [] o Context.transfer_proof thy; + (** pretty printing **) -fun pretty_term ctxt t = Sign.pretty_term' (syn_of ctxt) (theory_of ctxt) (context_tr' ctxt t); +fun pretty_term' thy ctxt t = Sign.pretty_term' (syn_of' thy ctxt) thy (context_tr' ctxt t); +fun pretty_term ctxt t = pretty_term' (theory_of ctxt) ctxt (context_tr' ctxt t); fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T; fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S; fun pretty_classrel ctxt cs = Sign.pretty_classrel (theory_of ctxt) cs; @@ -329,6 +353,13 @@ | pretty_fact ctxt (a, ths) = Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths)); +fun pretty_proof ctxt prf = + pretty_term' (ProofSyntax.proof_syntax prf (theory_of ctxt)) ctxt + (ProofSyntax.term_of_proof prf); + +fun pretty_proof_of ctxt full th = + pretty_proof ctxt (ProofSyntax.proof_of full th); + (** default sorts and types **) @@ -969,7 +1000,7 @@ (* reset_thms *) -fun reset_thms name = (* FIXME NameSpace.hide!? *) +fun reset_thms name = map_context (fn (syntax, asms, binds, (q, (space, tab), index), cases, defs) => (syntax, asms, binds, (q, (space, Symtab.delete_safe name tab), index), cases, defs));