# HG changeset patch # User wenzelm # Date 878056576 -3600 # Node ID 0770a19c48d379afe2d9418a8aac031bbde07455 # Parent 4e2994bae718f5e38351a3af339537a18520fd73 added ignored_consts, thms_containing, add_store_axioms(_i), add_store_defs(_i), thms_of; tuned pure thys; diff -r 4e2994bae718 -r 0770a19c48d3 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Oct 28 17:34:12 1997 +0100 +++ b/src/Pure/pure_thy.ML Tue Oct 28 17:36:16 1997 +0100 @@ -5,13 +5,25 @@ Init 'theorems' data. The Pure theories. *) +signature BASIC_PURE_THY = +sig + val get_thm: theory -> xstring -> thm + val get_thms: theory -> xstring -> thm list + val thms_of: theory -> (string * thm) list +end + signature PURE_THY = sig - val store_thms: (bstring * thm) list -> theory -> theory (*DESTRUCTIVE*) - val store_thmss: (bstring * thm list) list -> theory -> theory (*DESTRUCTIVE*) - val smart_store_thm: (bstring * thm) -> thm (*DESTRUCTIVE*) - val get_thm: theory -> xstring -> thm - val get_thms: theory -> xstring -> thm list + include BASIC_PURE_THY + val ignored_consts: string list + val thms_containing: theory -> string list -> (string * thm) list + val store_thms: (bstring * thm) list -> theory -> theory + val store_thmss: (bstring * thm list) list -> theory -> theory + val smart_store_thm: (bstring * thm) -> thm + val add_store_axioms: (bstring * string) list -> theory -> theory + val add_store_axioms_i: (bstring * term) list -> theory -> theory + val add_store_defs: (bstring * string) list -> theory -> theory + val add_store_defs_i: (bstring * term) list -> theory -> theory val proto_pure: theory val pure: theory val cpure: theory @@ -21,30 +33,27 @@ struct -(** init theorems data **) +(*** init theorems data ***) -(* data kind theorems *) +(** data kind theorems **) val theorems = "theorems"; exception Theorems of - {space: NameSpace.T, thms_tab: thm list Symtab.table} ref; + {space: NameSpace.T, + thms_tab: thm list Symtab.table, + const_idx: int * (int * thm) list Symtab.table} ref; (* methods *) local -val empty = - Theorems (ref {space = NameSpace.empty, thms_tab = Symtab.null}); +fun mk_empty _ = + Theorems (ref {space = NameSpace.empty, + thms_tab = Symtab.null, const_idx = (0, Symtab.null)}); -fun ext (Theorems (ref {space, ...})) = - Theorems (ref {space = space, thms_tab = Symtab.null}); - -fun merge (Theorems (ref {space = space1, ...}), Theorems (ref {space = space2, ...})) = - Theorems (ref {space = NameSpace.merge (space1, space2), thms_tab = Symtab.null}); - -fun print (Theorems (ref {space, thms_tab})) = +fun print (Theorems (ref {space, thms_tab, const_idx = _})) = let val prt_thm = Pretty.quote o pretty_thm; fun prt_thms (name, [th]) = @@ -61,50 +70,110 @@ in -val theorems_methods = (empty, ext, merge, print); +val theorems_methods = (mk_empty (), mk_empty, mk_empty, print); end; (* get data record *) -fun get_theorems sg = +fun get_theorems_sg sg = (case Sign.get_data sg theorems of Theorems r => r - | _ => sys_error "get_theorems"); + | _ => sys_error "get_theorems_sg"); + +val get_theorems = get_theorems_sg o sign_of; + -(* retrieve theorems *) +(** retrieve theorems **) -fun lookup_thms theory full_name = +(* get_thm(s) *) + +fun local_thms thy name = let - val tab_of = #thms_tab o ! o get_theorems o sign_of; - fun lookup [] = raise Match - | lookup (thy :: thys) = - (case Symtab.lookup (tab_of thy, full_name) of - Some thms => thms - | None => lookup (Theory.parents_of thy) handle Match => lookup thys) - in - lookup [theory] handle Match - => raise THEORY ("No theorems " ^ quote full_name ^ " stored in theory", [theory]) - end; + val ref {space, thms_tab, ...} = get_theorems thy; + val full_name = NameSpace.intern space name; + in Symtab.lookup (thms_tab, full_name) end; + +fun all_local_thms [] _ = None + | all_local_thms (thy :: thys) name = + (case local_thms thy name of + None => all_local_thms thys name + | some => some); + fun get_thms thy name = - let - val ref {space, ...} = get_theorems (sign_of thy); - val full_name = NameSpace.intern space name; - in lookup_thms thy full_name end; + (case all_local_thms (thy :: Theory.ancestors_of thy) name of + None => raise THEORY ("Theorems " ^ quote name ^ " not stored in theory", [thy]) + | Some thms => thms); fun get_thm thy name = (case get_thms thy name of [thm] => thm - | _ => raise THEORY ("Singleton theorem list expected " ^ quote name, [thy])); + | _ => raise THEORY ("Singleton list of theorems expected " ^ quote name, [thy])); + + +(* thms_of *) + +fun attach_name thm = (Thm.name_of_thm thm, thm); + +fun thms_of thy = + let val ref {thms_tab, ...} = get_theorems thy in + map attach_name (flat (map snd (Symtab.dest thms_tab))) + end; + -(* store theorems *) (*DESTRUCTIVE*) +(** theorems indexed by constants **) + +(* make index *) + +val ignored_consts = ["Trueprop", "all", "==>", "=="]; + +fun add_const_idx ((next, table), thm) = + let + val {hyps, prop, ...} = Thm.rep_thm thm; + val consts = + foldr add_term_consts (hyps, add_term_consts (prop, [])) \\ ignored_consts; + + fun add (tab, c) = + Symtab.update ((c, (next, thm) :: Symtab.lookup_multi (tab, c)), tab); + in (next + 1, foldl add (table, consts)) end; + +fun make_const_idx thm_tab = + foldl (foldl add_const_idx) ((0, Symtab.null), map snd (Symtab.dest thm_tab)); + + +(* lookup index *) -fun err_dup name = - error ("Duplicate theorems " ^ quote name); +(*search locally*) +fun containing [] thy = thms_of thy + | containing consts thy = + let + fun intr ([], _) = [] + | intr (_, []) = [] + | intr (xxs as ((x as (i:int, _)) :: xs), yys as ((y as (j, _)) :: ys)) = + if i = j then x :: intr (xs, ys) + else if i > j then intr (xs, yys) + else intr (xxs, ys); + + fun intrs [xs] = xs + | intrs xss = if exists null xss then [] else foldl intr (hd xss, tl xss); + + val ref {const_idx = (_, ctab), ...} = get_theorems thy; + val ithmss = map (fn c => Symtab.lookup_multi (ctab, c)) consts; + in + map (attach_name o snd) (intrs ithmss) + end; + +(*search globally*) +fun thms_containing thy consts = + flat (map (containing consts) (thy :: Theory.ancestors_of thy)); + + + +(** store theorems **) (*DESTRUCTIVE*) fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name); @@ -123,20 +192,24 @@ val named_thms = ListPair.map Thm.name_thm (names, thms); val eq_thms = ListPair.all Thm.eq_thm; - val r as ref {space, thms_tab = tab} = get_theorems sg; + + val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg; + + val overwrite = + (case Symtab.lookup (thms_tab, name) of + None => false + | Some thms' => + if length thms' = len andalso eq_thms (thms', named_thms) then + (warn_same name; false) + else (warn_overwrite name; true)); + + val space' = NameSpace.extend ([name], space); + val thms_tab' = Symtab.update ((name, named_thms), thms_tab); + val const_idx' = + if overwrite then make_const_idx thms_tab' + else foldl add_const_idx (const_idx, named_thms); in - (case Symtab.lookup (tab, name) of - None => - if NameSpace.declared space name then err_dup name else () - | Some thms' => - if length thms' = len andalso eq_thms (thms', named_thms) then - warn_same name - else warn_overwrite name); - - r := - {space = NameSpace.extend ([name], space), - thms_tab = Symtab.update ((name, named_thms), tab)}; - + r := {space = space', thms_tab = thms_tab', const_idx = const_idx'}; named_thms end; @@ -155,6 +228,20 @@ in named_thm end; +(* store axioms as theorems *) + +fun add_store add named_axs thy = + let + val thy' = add named_axs thy; + val named_thms = map (fn name => (name, get_axiom thy' name)) (map fst named_axs); + in store_thms named_thms thy' end; + +val add_store_axioms = add_store Theory.add_axioms; +val add_store_axioms_i = add_store Theory.add_axioms_i; +val add_store_defs = add_store Theory.add_defs; +val add_store_defs_i = add_store Theory.add_defs_i; + + (** the Pure theories **) @@ -184,21 +271,30 @@ ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)), ("all", "('a => prop) => prop", Binder ("!!", 0, 0)), ("TYPE", "'a itself", NoSyn)] - |> Theory.add_defs [("flexpair_def", "(t =?= u) == (t == u::'a::{})")] + |> Theory.add_path "ProtoPure" + |> add_store_defs [("flexpair_def", "(t =?= u) == (t == u::'a::{})")] |> Theory.add_name "ProtoPure"; -val pure = proto_pure +val pure = + Theory.prep_ext_merge [proto_pure] |> Theory.add_syntax Syntax.pure_appl_syntax + |> Theory.add_path "Pure" |> Theory.add_name "Pure"; -val cpure = proto_pure +val cpure = + Theory.prep_ext_merge [proto_pure] |> Theory.add_syntax Syntax.pure_applC_syntax + |> Theory.add_path "CPure" |> Theory.add_name "CPure"; end; +structure BasicPureThy: BASIC_PURE_THY = PureThy; +open BasicPureThy; + + (** theory structures **)