# HG changeset patch # User wenzelm # Date 895055008 -7200 # Node ID 03b81b6e1baa8185bf3cfd4b5b40035679fad297 # Parent 74bc10921f7debc4d6876850de8c0d2528b65c45 added thms_closure: theory -> xstring -> tthm list option; added add_typedecls: (bstring * string list * mixfix) list -> theory -> theory; |> Theory.add_nonterminals Syntax.pure_nonterms; diff -r 74bc10921f7d -r 03b81b6e1baa src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed May 13 12:21:45 1998 +0200 +++ b/src/Pure/pure_thy.ML Wed May 13 12:23:28 1998 +0200 @@ -15,6 +15,7 @@ signature PURE_THY = sig include BASIC_PURE_THY + val thms_closure: theory -> xstring -> tthm list option val get_tthm: theory -> xstring -> tthm val get_tthms: theory -> xstring -> tthm list val thms_containing: theory -> string list -> (string * thm) list @@ -29,6 +30,7 @@ val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory val add_defss: ((bstring * string list) * theory attribute list) list -> theory -> theory val add_defss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory + val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory val proto_pure: theory val pure: theory val cpure: theory @@ -38,9 +40,9 @@ struct -(*** init theorems data ***) +(*** theorem database ***) -(** data kind 'theorems' **) +(** data kind 'Pure/theorems' **) val theoremsK = "Pure/theorems"; @@ -89,23 +91,26 @@ (** retrieve theorems **) -fun local_thms thy name = - let - val ref {space, thms_tab, ...} = get_theorems thy; - val full_name = NameSpace.intern space name; - in Symtab.lookup (thms_tab, full_name) end; +(* thms_closure *) + +(*note: we avoid life references to the theory, so users may safely + keep thms_closure without too much space consumption*) -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 thms_closure_aux thy = + let val ref {space, thms_tab, ...} = get_theorems thy + in fn name => Symtab.lookup (thms_tab, NameSpace.intern space name) end; + +fun thms_closure thy = + let val closures = map thms_closure_aux (thy :: Theory.ancestors_of thy) + in fn name => get_first (fn f => f name) closures end; (* get_thms etc. *) +fun lookup_thms name thy = thms_closure_aux thy name; + fun get_tthms thy name = - (case all_local_thms (thy :: Theory.ancestors_of thy) name of + (case get_first (lookup_thms name) (thy :: Theory.ancestors_of thy) of None => raise THEORY ("Unknown theorem(s) " ^ quote name, [thy]) | Some thms => thms); @@ -266,22 +271,46 @@ -(** the Pure theories **) +(*** add logical types ***) + +fun add_typedecls decls thy = + let + val full = Sign.full_name (Theory.sign_of thy); + + fun type_of (raw_name, vs, mx) = + if null (duplicates vs) then (raw_name, length vs, mx) + else error ("Duplicate parameters in type declaration: " ^ quote raw_name); + + fun arity_of (raw_name, len, mx) = + (full (Syntax.type_name raw_name mx), replicate len logicS, logicS); + + val types = map type_of decls; + val arities = map arity_of types; + in + thy + |> Theory.add_types types + |> Theory.add_arities_i arities + end; + + + +(*** the Pure theories ***) val proto_pure = Theory.pre_pure |> Theory.apply [Attribute.setup, theorems_setup] |> Theory.add_types - (("fun", 2, NoSyn) :: - ("prop", 0, NoSyn) :: - ("itself", 1, NoSyn) :: - Syntax.pure_types) + [("fun", 2, NoSyn), + ("prop", 0, NoSyn), + ("itself", 1, NoSyn), + ("dummy", 0, NoSyn)] |> Theory.add_classes_i [(logicC, [])] |> Theory.add_defsort_i logicS |> Theory.add_arities_i [("fun", [logicS, logicS], logicS), ("prop", [], logicS), ("itself", [logicS], logicS)] + |> Theory.add_nonterminals Syntax.pure_nonterms |> Theory.add_syntax Syntax.pure_syntax |> Theory.add_modesyntax ("symbols", true) Syntax.pure_sym_syntax |> Theory.add_trfuns Syntax.pure_trfuns @@ -303,14 +332,14 @@ val pure = Theory.prep_ext_merge [proto_pure] + |> Theory.add_path "Pure" |> Theory.add_syntax Syntax.pure_appl_syntax - |> Theory.add_path "Pure" |> Theory.add_name "Pure"; val cpure = Theory.prep_ext_merge [proto_pure] + |> Theory.add_path "CPure" |> Theory.add_syntax Syntax.pure_applC_syntax - |> Theory.add_path "CPure" |> Theory.add_name "CPure";