# HG changeset patch # User wenzelm # Date 878056666 -3600 # Node ID a9dc0484c903800bed2dd864fce1ff88b93385bc # Parent 0770a19c48d379afe2d9418a8aac031bbde07455 restructured -- uses PureThy storage facilities; diff -r 0770a19c48d3 -r a9dc0484c903 src/Pure/Thy/thm_database.ML --- a/src/Pure/Thy/thm_database.ML Tue Oct 28 17:36:16 1997 +0100 +++ b/src/Pure/Thy/thm_database.ML Tue Oct 28 17:37:46 1997 +0100 @@ -1,175 +1,88 @@ (* Title: Pure/Thy/thm_database.ML ID: $Id$ - Author: Carsten Clasohm and Tobias Nipkow - Copyright 1995 TU Muenchen -*) + Author: Carsten Clasohm and Tobias Nipkow and Markus Wenzel, TU Muenchen -datatype thm_db = - ThmDB of {count: int, - thy_idx: (Sign.sg * (string list * int list)) list, - const_idx: ((int * (string * thm)) list) Symtab.table}; - (*count: number of theorems in database (used as unique ID for next thm) - thy_idx: constants and IDs of theorems - indexed by the theory's signature they belong to - const_idx: named theorems tagged by numbers and - indexed by the constants they contain*) +User level interface to thm database (see also Pure/pure_thy.ML). +*) signature THM_DATABASE = - sig - val thm_db: thm_db ref - val store_thm_db: string * thm -> thm - val delete_thm_db: theory -> unit +sig + val store_thm: string * thm -> thm + val qed_thm: thm option ref + val bind_thm: string * thm -> unit + val qed: string -> unit + val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit + val qed_goalw: string -> theory -> thm list -> string -> (thm list -> tactic list) -> unit + (*these peek at the proof state!*) val thms_containing: string list -> (string * thm) list - val findI: int -> (string * thm)list - val findEs: int -> (string * thm)list - val findE: int -> int -> (string * thm)list - - val store_thm : string * thm -> thm - val bind_thm : string * thm -> unit - val qed : string -> unit - val qed_thm : thm ref - val qed_goal : string -> theory -> string - -> (thm list -> tactic list) -> unit - val qed_goalw : string -> theory -> thm list -> string - -> (thm list -> tactic list) -> unit - val get_thm : theory -> string -> thm - val thms_of : theory -> (string * thm) list - val delete_thms : string -> unit - - val print_theory : theory -> unit - end; + val findI: int -> (string * thm) list + val findEs: int -> (string * thm) list + val findE: int -> int -> (string * thm) list +end; structure ThmDatabase: THM_DATABASE = struct -open ThyInfo BrowserInfo; - -(*** ignore and top_const could be turned into functor-parameters, but are -currently identical for all object logics ***) - -(* Constants not to be used for theorem indexing *) -val ignore = ["Trueprop", "all", "==>", "=="]; - -(* top_const: main constant, ignoring Trueprop *) -fun top_const (_ $ t) = (case head_of t of Const(c,_) => Some c - | _ => None) - | top_const _ = None; +(** store theorems **) -(*Symtab which associates a constant with a list of theorems that contain the - constant (theorems are tagged with numbers)*) -val thm_db = ref (ThmDB - {count = 0, thy_idx = []:(Sign.sg * (string list * int list)) list, - const_idx = Symtab.make ([]:(string * ((int * (string * thm)) list)) list)}); - -(*List all relevant constants a term contains*) -fun list_consts t = - let fun consts (Const (c, _)) = if c mem ignore then [] else [c] - | consts (Free _) = [] - | consts (Var _) = [] - | consts (Bound _) = [] - | consts (Abs (_, _, t)) = consts t - | consts (t1$t2) = (consts t1) union (consts t2); - in distinct (consts t) end; - -(*Store a theorem in database*) -fun store_thm_db (named_thm as (name, thm)) = - let val {prop, hyps, sign, ...} = rep_thm thm; - - val consts = distinct (flat (map list_consts (prop :: hyps))); +(* store in theory and generate HTML *) - val ThmDB {count, thy_idx, const_idx} = !thm_db; - - fun update_thys [] = [(sign, (consts, [count]))] - | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) = - if Sign.eq_sg (sign, thy_sign) then - (thy_sign, (thy_consts union consts, count :: thy_nums)) :: ts - else thy :: update_thys ts; - - val tagged_thm = (count, named_thm); - - fun update_db _ [] result = Some result - | update_db checked (c :: cs) result = - let - val old_thms = Symtab.lookup_multi (result, c); - - val duplicate = - if checked then false - else case find_first (fn (_, (n, _)) => n = name) old_thms of - Some (_, (_, t)) => eq_thm (t, thm) - | None => false - in if duplicate then None - else update_db true - cs (Symtab.update ((c, tagged_thm :: old_thms), result)) - end; - - val const_idx' = update_db false consts const_idx; - in if consts = [] then warning ("Theorem " ^ name ^ - " cannot be stored in ThmDB\n\t because it \ - \contains no or only ignored constants.") - else if is_some const_idx' then - thm_db := ThmDB {count = count+1, thy_idx = update_thys thy_idx, - const_idx = the const_idx'} - else (); - thm +fun store_thm (name, thm) = + let val thm' = PureThy.smart_store_thm (name, thm) in + BrowserInfo.thm_to_html thm' name; thm' end; -(*Remove all theorems with given signature from database*) -fun delete_thm_db thy = - let - val sign = sign_of thy; - val ThmDB {count, thy_idx, const_idx} = !thm_db; +(* store on ML toplevel *) + +val qed_thm: thm option ref = ref None; - (*Remove theory from thy_idx and get the data associated with it*) - fun update_thys [] result = (result, [], []) - | update_thys ((thy as (thy_sign, (thy_consts, thy_nums))) :: ts) - result = - if Sign.eq_sg (sign, thy_sign) then - (result @ ts, thy_consts, thy_nums) - else update_thys ts (thy :: result); +val ml_reserved = + ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else", + "end", "exception", "fn", "fun", "handle", "if", "in", "infix", + "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", + "raise", "rec", "then", "type", "val", "with", "withtype", "while", + "eqtype", "functor", "include", "sharing", "sig", "signature", + "struct", "structure", "where"]; - val (thy_idx', thy_consts, thy_nums) = update_thys thy_idx []; +fun is_ml_identifier name = + Syntax.is_identifier name andalso not (name mem ml_reserved); - (*Remove all theorems belonging to a theory*) - fun update_db [] result = result - | update_db (c :: cs) result = - let val thms' = filter_out (fn (num, _) => num mem thy_nums) - (Symtab.lookup_multi (result, c)); - in update_db cs (Symtab.update ((c, thms'), result)) end; - in thm_db := ThmDB {count = count, thy_idx = thy_idx', - const_idx = update_db thy_consts const_idx} +fun ml_store_thm (name, thm) = + let val thm' = store_thm (name, thm) in + if is_ml_identifier name then + (qed_thm := Some thm'; + use_strings ["val " ^ name ^ " = the (! ThmDatabase.qed_thm);"]) + else warning ("Cannot bind thm " ^ quote name ^ " as ML value") end; -(*Intersection of two theorem lists with descending tags*) -infix desc_inter; -fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = [] - | xs desc_inter [] = [] - | (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) = - if xi = yi then x :: (xs desc_inter ys) - else if xi > yi then xs desc_inter yss - else xss desc_inter ys; +fun bind_thm (name, thm) = ml_store_thm (name, standard thm); +fun qed name = ml_store_thm (name, result ()); +fun qed_goal name thy goal tacsf = ml_store_thm (name, prove_goal thy goal tacsf); +fun qed_goalw name thy rews goal tacsf = ml_store_thm (name, prove_goalw thy rews goal tacsf); + + + +(** retrieve theorems **) (*peek at current proof state*) -(*Get all theorems from database that contain a list of constants*) -fun thms_containing constants = - let fun collect [] _ result = map snd result - | collect (c :: cs) first result = - let val ThmDB {const_idx, ...} = !thm_db; +(*get theorems that contain *all* of given constants*) +fun thms_containing raw_consts = + let + val sign = sign_of_thm (topthm ()); + val consts = map (Sign.intern_const sign) raw_consts; + val thy = ThyInfo.theory_of_sign sign; + in + PureThy.thms_containing thy (consts \\ PureThy.ignored_consts) + end; - val new_thms = Symtab.lookup_multi (const_idx, c); - in collect cs false (if first then new_thms - else (result desc_inter new_thms)) - end; - val look_for = constants \\ ignore; - in if null look_for then - error ("No or only ignored constants were specified for theorem \ - \database search:\n " ^ commas (map quote ignore)) - else (); - collect look_for true [] end; +(*top_const: main constant, ignoring Trueprop*) +fun top_const (_ $ t) = (case head_of t of Const (c, _) => Some c | _ => None) + | top_const _ = None; val intro_const = top_const o concl_of; -fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const(p); +fun elim_const thm = case prems_of thm of [] => None | p::_ => top_const p; (* In case faster access is necessary, the thm db should provide special functions @@ -265,130 +178,4 @@ in find_elims sign (nth_elem(j-1, prems_of_goal i)) end; -(*** Store and retrieve theorems ***) - -(** Store theorems **) - -(*Store a theorem in the thy_info of its theory, - and in the theory's HTML file*) -fun store_thm (name, thm) = - let - val (thy_name, {path, children, parents, thy_time, ml_time, - theory, thms, methods, data}) = - thyinfo_of_sign (#sign (rep_thm thm)) - - val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false) - handle Symtab.DUPLICATE s => - (if eq_thm (the (Symtab.lookup (thms, name)), thm) then - (warning ("Theory database already contains copy of\ - \ theorem " ^ quote name); - (thms, true)) - else error ("Duplicate theorem name " ^ quote s - ^ " used in theory database")); - - (*Label this theorem*) - val thm' = Thm.name_thm (name, thm) - in - loaded_thys := Symtab.update - ((thy_name, {path = path, children = children, parents = parents, - thy_time = thy_time, ml_time = ml_time, - theory = theory, thms = thms', - methods = methods, data = data}), - !loaded_thys); - thm_to_html thm name; - if duplicate then thm' else store_thm_db (name, thm') - end; - - -(*Store result of proof in loaded_thys and as ML value*) - -val qed_thm = ref ProtoPure.flexpair_def(*dummy*); - - -fun bind_thm (name, thm) = - (qed_thm := store_thm (name, (standard thm)); - use_strings ["val " ^ name ^ " = !qed_thm;"]); - - -fun qed name = - (qed_thm := store_thm (name, result ()); - use_strings ["val " ^ name ^ " = !qed_thm;"]); - - -fun qed_goal name thy agoal tacsf = - (qed_thm := store_thm (name, prove_goal thy agoal tacsf); - use_strings ["val " ^ name ^ " = !qed_thm;"]); - - -fun qed_goalw name thy rths agoal tacsf = - (qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf); - use_strings ["val " ^ name ^ " = !qed_thm;"]); - - -(** Retrieve theorems **) - -(*Get all theorems belonging to a given theory*) -fun thmtab_of_thy thy = - let val (_, {thms, ...}) = thyinfo_of_sign (sign_of thy); - in thms end; - - -fun thmtab_of_name name = - let val {thms, ...} = the (get_thyinfo name); - in thms end; - - -(*Get a stored theorem specified by theory and name. *) -fun get_thm thy name = - let fun get [] [] searched = - raise THEORY ("get_thm: no theorem " ^ quote name, [thy]) - | get [] ng searched = - get (ng \\ searched) [] searched - | get (t::ts) ng searched = - (case Symtab.lookup (thmtab_of_name t, name) of - Some thm => thm - | None => get ts (ng union (parents_of_name t)) (t::searched)); - - val (tname, _) = thyinfo_of_sign (sign_of thy); - in get [tname] [] [] end; - - -(*Get stored theorems of a theory (original derivations) *) -val thms_of = Symtab.dest o thmtab_of_thy; - - -(*Remove theorems associated with a theory from theory and theorem database*) -fun delete_thms tname = - let - val tinfo = case get_thyinfo tname of - Some ({path, children, parents, thy_time, ml_time, theory, - methods, data, ...}) => - {path = path, children = children, parents = parents, - thy_time = thy_time, ml_time = ml_time, - theory = theory, thms = Symtab.null, - methods = methods, data = data} - | None => error ("Theory " ^ tname ^ " not stored by loader"); - - val {theory, ...} = tinfo; - in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys); - case theory of - Some t => delete_thm_db t - | None => () - end; - - -(*** Print theory ***) - -fun print_thms thy = - let - val thms = thms_of thy; - fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1, - Pretty.quote (pretty_thm th)]; - in - Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms)) - end; - - -fun print_theory thy = (Display.print_theory thy; print_thms thy); - end;