# HG changeset patch # User wenzelm # Date 1160177476 -7200 # Node ID 0ddd2f297ae7ac2cf2775d347d84c6c135300c5b # Parent ec9a1bb086daa2a98f4e8130a61bbd89a74c826c turned into abstract wrapper module, cf. theory_target.ML; simplified interfaces; diff -r ec9a1bb086da -r 0ddd2f297ae7 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Sat Oct 07 01:31:15 2006 +0200 +++ b/src/Pure/Isar/local_theory.ML Sat Oct 07 01:31:16 2006 +0200 @@ -2,295 +2,164 @@ ID: $Id$ Author: Makarius -Local theory operations, with optional target locale. +Local theory operations, with abstract target context. *) type local_theory = Proof.context; signature LOCAL_THEORY = sig - val params_of: local_theory -> (string * typ) list - val hyps_of: local_theory -> term list - val standard: local_theory -> thm list -> thm list - val pretty_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> Pretty.T - val quiet_mode: bool ref - val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit + type operations + val target_of: local_theory -> Proof.context + val init: string option -> operations -> Proof.context -> local_theory + val reinit: local_theory -> local_theory val theory: (theory -> theory) -> local_theory -> local_theory val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory - val init: xstring option -> theory -> local_theory - val init_i: string option -> theory -> local_theory - val restore: local_theory -> local_theory - val exit: local_theory -> local_theory * theory - val restore_naming: local_theory -> local_theory - val naming: local_theory -> local_theory - val mapping: xstring option -> (local_theory -> local_theory) -> theory -> local_theory * theory - val term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory - val syntax: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory - val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory -> local_theory - val consts: ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory - val consts_restricted: (string * typ -> bool) -> - ((bstring * typ) * mixfix) list -> local_theory -> term list * local_theory + val target: (Proof.context -> Proof.context) -> local_theory -> local_theory + val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory + val pretty: local_theory -> Pretty.T + val consts: (string * typ -> bool) -> + ((bstring * typ) * mixfix) list -> local_theory -> (term * thm) list * local_theory val axioms: ((bstring * Attrib.src list) * term list) list -> local_theory -> (bstring * thm list) list * local_theory - val axioms_finish: (local_theory -> thm -> thm) -> - ((bstring * Attrib.src list) * term list) list -> local_theory -> - (bstring * thm list) list * local_theory - val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> + val defs: ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list -> + local_theory -> (term * (bstring * thm)) list * local_theory + val notes: ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> local_theory -> (bstring * thm list) list * local_theory - val note: (bstring * Attrib.src list) * thm list -> local_theory -> - (bstring * thm list) * local_theory + val term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory + val declaration: (Context.generic -> Context.generic) -> local_theory -> local_theory val def: (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> local_theory -> (term * (bstring * thm)) * local_theory - val def_finish: (local_theory -> term -> thm -> thm) -> - (bstring * mixfix) * ((bstring * Attrib.src list) * term) -> - local_theory -> (term * (bstring * thm)) * local_theory + val note: (bstring * Attrib.src list) * thm list -> + local_theory -> (bstring * thm list) * Proof.context + val const_syntax: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory + val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory -> local_theory end; structure LocalTheory: LOCAL_THEORY = struct +(** local theory data **) -(** local context data **) +(* type lthy *) + +type operations = + {pretty: local_theory -> Pretty.T, + consts: (string * typ -> bool) -> ((bstring * typ) * mixfix) list -> local_theory -> + (term * thm) list * local_theory, + axioms: ((bstring * Attrib.src list) * term list) list -> local_theory -> + (bstring * thm list) list * local_theory, + defs: ((bstring * mixfix) * ((bstring * Attrib.src list) * term)) list -> local_theory -> + (term * (bstring * thm)) list * local_theory, + notes: ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> local_theory -> + (bstring * thm list) list * local_theory, + term_syntax: (Context.generic -> Context.generic) -> local_theory -> local_theory, + declaration: (Context.generic -> Context.generic) -> local_theory -> local_theory}; + +datatype lthy = LThy of + {theory_prefix: string option, + operations: operations, + target: Proof.context}; + +fun make_lthy (theory_prefix, operations, target) = + LThy {theory_prefix = theory_prefix, operations = operations, target = target}; + + +(* context data *) structure Data = ProofDataFun ( val name = "Pure/local_theory"; - type T = - {locale: (string * Proof.context) option, - params: (string * typ) list, - hyps: term list, - restore_naming: theory -> theory}; - fun init thy = {locale = NONE, params = [], hyps = [], restore_naming = I}; + type T = lthy option; + fun init _ = NONE; fun print _ _ = (); ); val _ = Context.add_setup Data.init; -fun map_locale f = Data.map (fn {locale, params, hyps, restore_naming} => - {locale = Option.map (fn (loc, ctxt) => (loc, f ctxt)) locale, - params = params, hyps = hyps, restore_naming = restore_naming}); - -val locale_of = #locale o Data.get; -val params_of = #params o Data.get; -val hyps_of = #hyps o Data.get; - -fun standard ctxt = - (case #locale (Data.get ctxt) of - NONE => map Drule.standard (* FIXME !? *) - | SOME (_, loc_ctxt) => ProofContext.export_standard ctxt loc_ctxt); - - -(* print consts *) - -val quiet_mode = ref false; +fun get_lthy lthy = + (case Data.get lthy of + NONE => error "No local theory context" + | SOME (LThy data) => data); -local - -fun pretty_var ctxt (x, T) = - Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1, - Pretty.quote (ProofContext.pretty_typ ctxt T)]; - -fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs); - -in +fun map_lthy f lthy = + let val {theory_prefix, operations, target} = get_lthy lthy + in Data.put (SOME (make_lthy (f (theory_prefix, operations, target)))) lthy end; -fun pretty_consts ctxt pred cs = - (case filter pred (params_of ctxt) of - [] => pretty_vars ctxt "constants" cs - | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]); +val target_of = #target o get_lthy; -fun print_consts _ _ [] = () - | print_consts ctxt pred cs = - if ! quiet_mode then () else Pretty.writeln (pretty_consts ctxt pred cs); - -end; +fun map_target f = map_lthy (fn (theory_prefix, operations, target) => + (theory_prefix, operations, f target)); -(* theory/locale substructures *) - -fun theory_result f ctxt = - let val (res, thy') = f (ProofContext.theory_of ctxt) - in (res, ctxt |> map_locale (ProofContext.transfer thy') |> ProofContext.transfer thy') end; - -fun theory f ctxt = #2 (theory_result (f #> pair ()) ctxt); - -fun locale_result f ctxt = - (case locale_of ctxt of - NONE => error "Local theory: no locale context" - | SOME (_, loc_ctxt) => - let - val (res, loc_ctxt') = f loc_ctxt; - val thy' = ProofContext.theory_of loc_ctxt'; - in (res, ctxt |> map_locale (K loc_ctxt') |> ProofContext.transfer thy') end); - -fun locale f ctxt = - if is_none (locale_of ctxt) then ctxt - else #2 (locale_result (f #> pair ()) ctxt); - - -(* init -- restore -- exit *) +(* init *) -fun init_i NONE thy = ProofContext.init thy - | init_i (SOME loc) thy = - thy - |> Locale.init loc - |> ProofContext.inferred_fixes - |> (fn (params, ctxt) => Data.put - {locale = SOME (loc, ctxt), - params = params, - hyps = Assumption.assms_of ctxt, - restore_naming = Sign.restore_naming thy} ctxt); - -fun init loc thy = init_i (Option.map (Locale.intern thy) loc) thy; +fun init theory_prefix operations target = target |> Data.map + (fn NONE => SOME (make_lthy (theory_prefix, operations, target)) + | SOME _ => error "Local theory already initialized"); -fun restore ctxt = - (case locale_of ctxt of - NONE => ctxt - | SOME (_, loc_ctxt) => loc_ctxt |> Data.put (Data.get ctxt)); - -fun exit ctxt = (ctxt, ProofContext.theory_of ctxt); - - -(* local naming *) - -fun naming ctxt = - (case locale_of ctxt of - NONE => ctxt - | SOME (loc, _) => ctxt |> theory (Sign.sticky_prefix (Sign.base_name loc))); - -fun restore_naming ctxt = theory (#restore_naming (Data.get ctxt)) ctxt; - -fun mapping loc f = - init loc #> naming #> f #> restore_naming #> exit; - +fun reinit lthy = + let val {theory_prefix, operations, target} = get_lthy lthy + in init theory_prefix operations target end; -(** local theory **) - -(* term syntax *) - -fun term_syntax f ctxt = ctxt |> - (case locale_of ctxt of - NONE => theory (Context.theory_map f) - | SOME (loc, _) => - locale (Locale.add_term_syntax loc (Context.proof_map f)) #> - Context.proof_map f); +(* substructure mappings *) -fun syntax x y = - term_syntax (Context.mapping (Sign.add_const_syntax x y) (ProofContext.add_const_syntax x y)); +fun theory_result f lthy = + (case #theory_prefix (get_lthy lthy) of + NONE => error "Cannot change background theory" + | SOME prefix => + let + val thy = ProofContext.theory_of lthy; + val (res, thy') = thy + |> Sign.sticky_prefix prefix + |> Sign.qualified_names + |> f + ||> Sign.restore_naming thy; + val lthy' = lthy + |> map_target (ProofContext.transfer thy') + |> ProofContext.transfer thy'; + in (res, lthy') end); -fun abbrevs x y = - term_syntax (Context.mapping (Sign.add_abbrevs x y) (ProofContext.add_abbrevs x y)); - +fun theory f = #2 o theory_result (f #> pair ()); -(* consts *) - -fun consts_restricted pred decls ctxt = +fun target_result f lthy = let - val thy = ProofContext.theory_of ctxt; - val params = filter pred (params_of ctxt); - val ps = map Free params; - val Ps = map #2 params; - val abbrs = decls |> map (fn ((c, T), mx) => - ((c, mx), Term.list_comb (Const (Sign.full_name thy c, Ps ---> T), ps))); - in - ctxt |> - (case locale_of ctxt of - NONE => theory (Sign.add_consts_authentic (map (fn ((c, T), mx) => (c, T, mx)) decls)) - | SOME (loc, _) => - theory (Sign.add_consts_authentic (map (fn ((c, T), _) => (c, Ps ---> T, NoSyn)) decls)) #> - abbrevs Syntax.default_mode abbrs) - |> pair (map #2 abbrs) - end; - -val consts = consts_restricted (K true); + val (res, ctxt') = f (#target (get_lthy lthy)); + val thy' = ProofContext.theory_of ctxt'; + val lthy' = lthy + |> map_target (K ctxt') + |> ProofContext.transfer thy'; + in (res, lthy') end; - -(* fact definitions *) - -fun notes kind facts ctxt = - let - val attrib = Attrib.attribute_i (ProofContext.theory_of ctxt); - val facts' = map (apsnd (map (apfst (standard ctxt)))) facts; (* FIXME burrow standard *) - in - ctxt |> - (case locale_of ctxt of - NONE => theory_result (PureThy.note_thmss_i kind (Attrib.map_facts attrib facts')) - | SOME (loc, _) => - locale_result (apfst #1 o Locale.add_thmss kind loc facts')) - ||> (#2 o ProofContext.note_thmss_i (Attrib.map_facts attrib facts)) - end; - -fun note (a, ths) ctxt = - ctxt |> notes PureThy.theoremK [(a, [(ths, [])])] |>> hd; +fun target f = #2 o target_result (f #> pair ()); -(* axioms *) - -local +(* primitive operations *) -fun add_axiom hyps (name, prop) thy = - let - val name' = if name = "" then "axiom_" ^ serial_string () else name; - val frees = rev ([] |> Term.add_frees prop |> fold Term.add_frees hyps); - val prop' = Term.list_all_free (frees, Logic.list_implies (hyps, prop)); - val thy' = thy |> Theory.add_axioms_i [(name', prop')]; +fun operation f lthy = f (#operations (get_lthy lthy)) lthy; +fun operation1 f x = operation (fn ops => f ops x); +fun operation2 f x y = operation (fn ops => f ops x y); - val cert = Thm.cterm_of thy'; - fun all_polymorphic (x, T) th = - let val var = cert (Var ((x, 0), #1 (Logic.dest_all (Thm.prop_of th)))) - in ((var, cert (Free (x, T))), Thm.forall_elim var th) end; - fun implies_polymorphic hyp th = Thm.assume (cert hyp) COMP th; - val th = - Thm.get_axiom_i thy' (Sign.full_name thy' name') - |> fold_map all_polymorphic frees |-> Drule.cterm_instantiate - |> fold implies_polymorphic hyps - in (th, thy') end; - -in - -fun axioms_finish finish = fold_map (fn ((name, atts), props) => - fold Variable.fix_frees props - #> (fn ctxt => ctxt - |> theory_result (fold_map (add_axiom (hyps_of ctxt)) (PureThy.name_multi name props)) - |-> (fn ths => note ((name, atts), map (finish ctxt) ths)))); - -val axioms = axioms_finish (K I); - -end; +val pretty = operation #pretty; +val consts = operation2 #consts; +val axioms = operation1 #axioms; +val defs = operation1 #defs; +val notes = operation1 #notes; +val term_syntax = operation1 #term_syntax; +val declaration = operation1 #declaration; -(* constant definitions *) - -local +(* derived operations *) -fun add_def (name, prop) = - Theory.add_defs_i false false [(name, prop)] #> (fn thy => - let - val th = Thm.get_axiom_i thy (Sign.full_name thy name); - val cert = Thm.cterm_of thy; - val subst = map2 (fn var => fn free => (cert (Var var), cert (Free free))) - (Term.add_vars (Thm.prop_of th) []) (Term.add_frees prop []); - in (Drule.cterm_instantiate subst th, thy) end); +fun def arg lthy = lthy |> defs [arg] |>> hd; -in +fun note (a, ths) lthy = lthy |> notes [(a, [(ths, [])])] |>> hd; -fun def_finish finish (var, spec) ctxt = - let - val (x, mx) = var; - val ((name, atts), rhs) = spec; - val name' = if name = "" then Thm.def_name x else name; - val rhs_frees = Term.add_frees rhs []; - in - ctxt - |> consts_restricted (member (op =) rhs_frees) [((x, Term.fastype_of rhs), mx)] - |-> (fn [lhs] => - theory_result (add_def (name', Logic.mk_equals (lhs, rhs))) - #-> (fn th => fn ctxt' => note ((name', atts), [finish ctxt' lhs th]) ctxt') - #> apfst (fn (b, [th]) => (lhs, (b, th)))) - end; +fun const_syntax mode args = + term_syntax + (Context.mapping (Sign.add_const_syntax mode args) (ProofContext.add_const_syntax mode args)); -val def = def_finish (K (K I)); +fun abbrevs mode args = + term_syntax (Context.mapping (Sign.add_abbrevs mode args) (ProofContext.add_abbrevs mode args)); end; - -end;