src/Pure/pure_thy.ML
changeset 4922 03b81b6e1baa
parent 4853 67bcbb03c235
child 4933 c85b339accfe
     1.1 --- a/src/Pure/pure_thy.ML	Wed May 13 12:21:45 1998 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Wed May 13 12:23:28 1998 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4  signature PURE_THY =
     1.5  sig
     1.6    include BASIC_PURE_THY
     1.7 +  val thms_closure: theory -> xstring -> tthm list option
     1.8    val get_tthm: theory -> xstring -> tthm
     1.9    val get_tthms: theory -> xstring -> tthm list
    1.10    val thms_containing: theory -> string list -> (string * thm) list
    1.11 @@ -29,6 +30,7 @@
    1.12    val add_defs_i: ((bstring * term) * theory attribute list) list -> theory -> theory
    1.13    val add_defss: ((bstring * string list) * theory attribute list) list -> theory -> theory
    1.14    val add_defss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory
    1.15 +  val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
    1.16    val proto_pure: theory
    1.17    val pure: theory
    1.18    val cpure: theory
    1.19 @@ -38,9 +40,9 @@
    1.20  struct
    1.21  
    1.22  
    1.23 -(*** init theorems data ***)
    1.24 +(*** theorem database ***)
    1.25  
    1.26 -(** data kind 'theorems' **)
    1.27 +(** data kind 'Pure/theorems' **)
    1.28  
    1.29  val theoremsK = "Pure/theorems";
    1.30  
    1.31 @@ -89,23 +91,26 @@
    1.32  
    1.33  (** retrieve theorems **)
    1.34  
    1.35 -fun local_thms thy name =
    1.36 -  let
    1.37 -    val ref {space, thms_tab, ...} = get_theorems thy;
    1.38 -    val full_name = NameSpace.intern space name;
    1.39 -  in Symtab.lookup (thms_tab, full_name) end;
    1.40 +(* thms_closure *)
    1.41 +
    1.42 +(*note: we avoid life references to the theory, so users may safely
    1.43 +  keep thms_closure without too much space consumption*)
    1.44  
    1.45 -fun all_local_thms [] _ = None
    1.46 -  | all_local_thms (thy :: thys) name =
    1.47 -      (case local_thms thy name of
    1.48 -        None => all_local_thms thys name
    1.49 -      | some => some);
    1.50 +fun thms_closure_aux thy =
    1.51 +  let val ref {space, thms_tab, ...} = get_theorems thy
    1.52 +  in fn name => Symtab.lookup (thms_tab, NameSpace.intern space name) end;
    1.53 +
    1.54 +fun thms_closure thy =
    1.55 +  let val closures = map thms_closure_aux (thy :: Theory.ancestors_of thy)
    1.56 +  in fn name => get_first (fn f => f name) closures end;
    1.57  
    1.58  
    1.59  (* get_thms etc. *)
    1.60  
    1.61 +fun lookup_thms name thy = thms_closure_aux thy name;
    1.62 +
    1.63  fun get_tthms thy name =
    1.64 -  (case all_local_thms (thy :: Theory.ancestors_of thy) name of
    1.65 +  (case get_first (lookup_thms name) (thy :: Theory.ancestors_of thy) of
    1.66      None => raise THEORY ("Unknown theorem(s) " ^ quote name, [thy])
    1.67    | Some thms => thms);
    1.68  
    1.69 @@ -266,22 +271,46 @@
    1.70  
    1.71  
    1.72  
    1.73 -(** the Pure theories **)
    1.74 +(*** add logical types ***)
    1.75 +
    1.76 +fun add_typedecls decls thy =
    1.77 +  let
    1.78 +    val full = Sign.full_name (Theory.sign_of thy);
    1.79 +
    1.80 +    fun type_of (raw_name, vs, mx) =
    1.81 +      if null (duplicates vs) then (raw_name, length vs, mx)
    1.82 +      else error ("Duplicate parameters in type declaration: " ^ quote raw_name);
    1.83 +
    1.84 +    fun arity_of (raw_name, len, mx) =
    1.85 +      (full (Syntax.type_name raw_name mx), replicate len logicS, logicS);
    1.86 +
    1.87 +    val types = map type_of decls;
    1.88 +    val arities = map arity_of types;
    1.89 +  in
    1.90 +    thy
    1.91 +    |> Theory.add_types types
    1.92 +    |> Theory.add_arities_i arities
    1.93 +  end;
    1.94 +
    1.95 +
    1.96 +
    1.97 +(*** the Pure theories ***)
    1.98  
    1.99  val proto_pure =
   1.100    Theory.pre_pure
   1.101    |> Theory.apply [Attribute.setup, theorems_setup]
   1.102    |> Theory.add_types
   1.103 -   (("fun", 2, NoSyn) ::
   1.104 -    ("prop", 0, NoSyn) ::
   1.105 -    ("itself", 1, NoSyn) ::
   1.106 -    Syntax.pure_types)
   1.107 +   [("fun", 2, NoSyn),
   1.108 +    ("prop", 0, NoSyn),
   1.109 +    ("itself", 1, NoSyn),
   1.110 +    ("dummy", 0, NoSyn)]
   1.111    |> Theory.add_classes_i [(logicC, [])]
   1.112    |> Theory.add_defsort_i logicS
   1.113    |> Theory.add_arities_i
   1.114     [("fun", [logicS, logicS], logicS),
   1.115      ("prop", [], logicS),
   1.116      ("itself", [logicS], logicS)]
   1.117 +  |> Theory.add_nonterminals Syntax.pure_nonterms
   1.118    |> Theory.add_syntax Syntax.pure_syntax
   1.119    |> Theory.add_modesyntax ("symbols", true) Syntax.pure_sym_syntax
   1.120    |> Theory.add_trfuns Syntax.pure_trfuns
   1.121 @@ -303,14 +332,14 @@
   1.122  
   1.123  val pure =
   1.124    Theory.prep_ext_merge [proto_pure]
   1.125 +  |> Theory.add_path "Pure"
   1.126    |> Theory.add_syntax Syntax.pure_appl_syntax
   1.127 -  |> Theory.add_path "Pure"
   1.128    |> Theory.add_name "Pure";
   1.129  
   1.130  val cpure =
   1.131    Theory.prep_ext_merge [proto_pure]
   1.132 +  |> Theory.add_path "CPure"
   1.133    |> Theory.add_syntax Syntax.pure_applC_syntax
   1.134 -  |> Theory.add_path "CPure"
   1.135    |> Theory.add_name "CPure";
   1.136  
   1.137