1.1 --- a/src/Pure/pure_thy.ML Wed Mar 19 18:15:25 2008 +0100
1.2 +++ b/src/Pure/pure_thy.ML Wed Mar 19 22:27:57 2008 +0100
1.3 @@ -7,14 +7,8 @@
1.4
1.5 signature BASIC_PURE_THY =
1.6 sig
1.7 - datatype interval = FromTo of int * int | From of int | Single of int
1.8 - datatype thmref =
1.9 - Name of string |
1.10 - NameSelection of string * interval list |
1.11 - Fact of string
1.12 - val get_thm: theory -> thmref -> thm
1.13 - val get_thms: theory -> thmref -> thm list
1.14 - val get_thmss: theory -> thmref list -> thm list
1.15 + val get_thm: theory -> Facts.ref -> thm
1.16 + val get_thms: theory -> Facts.ref -> thm list
1.17 structure ProtoPure:
1.18 sig
1.19 val thy: theory
1.20 @@ -44,13 +38,7 @@
1.21 val kind_internal: attribute
1.22 val has_internal: Markup.property list -> bool
1.23 val is_internal: thm -> bool
1.24 - val string_of_thmref: thmref -> string
1.25 - val single_thm: string -> thm list -> thm
1.26 - val name_of_thmref: thmref -> string
1.27 - val map_name_of_thmref: (string -> string) -> thmref -> thmref
1.28 - val select_thm: thmref -> thm list -> thm list
1.29 - val selections: string * thm list -> (thmref * thm) list
1.30 - val get_thms_silent: theory -> thmref -> thm list
1.31 + val get_thms_silent: theory -> Facts.ref -> thm list
1.32 val theorems_of: theory -> thm list NameSpace.table
1.33 val all_facts_of: theory -> Facts.T
1.34 val thms_of: theory -> (string * thm) list
1.35 @@ -73,7 +61,7 @@
1.36 val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
1.37 val note: string -> string * thm -> theory -> thm * theory
1.38 val note_thmss: string -> ((bstring * attribute list) *
1.39 - (thmref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
1.40 + (Facts.ref * attribute list) list) list -> theory -> (bstring * thm list) list * theory
1.41 val note_thmss_i: string -> ((bstring * attribute list) *
1.42 (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory
1.43 val note_thmss_grouped: string -> string -> ((bstring * attribute list) *
1.44 @@ -182,75 +170,6 @@
1.45 fun the_thms _ (SOME thms) = thms
1.46 | the_thms name NONE = error ("Unknown theorem(s) " ^ quote name);
1.47
1.48 -fun single_thm _ [thm] = thm
1.49 - | single_thm name _ = error ("Single theorem expected " ^ quote name);
1.50 -
1.51 -
1.52 -(* datatype interval *)
1.53 -
1.54 -datatype interval =
1.55 - FromTo of int * int |
1.56 - From of int |
1.57 - Single of int;
1.58 -
1.59 -fun string_of_interval (FromTo (i, j)) = string_of_int i ^ "-" ^ string_of_int j
1.60 - | string_of_interval (From i) = string_of_int i ^ "-"
1.61 - | string_of_interval (Single i) = string_of_int i;
1.62 -
1.63 -fun interval n iv =
1.64 - let fun err () = raise Fail ("Bad interval specification " ^ string_of_interval iv) in
1.65 - (case iv of
1.66 - FromTo (i, j) => if i <= j then i upto j else err ()
1.67 - | From i => if i <= n then i upto n else err ()
1.68 - | Single i => [i])
1.69 - end;
1.70 -
1.71 -
1.72 -(* datatype thmref *)
1.73 -
1.74 -datatype thmref =
1.75 - Name of string |
1.76 - NameSelection of string * interval list |
1.77 - Fact of string;
1.78 -
1.79 -fun name_of_thmref (Name name) = name
1.80 - | name_of_thmref (NameSelection (name, _)) = name
1.81 - | name_of_thmref (Fact _) = error "Illegal literal fact";
1.82 -
1.83 -fun map_name_of_thmref f (Name name) = Name (f name)
1.84 - | map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is)
1.85 - | map_name_of_thmref _ thmref = thmref;
1.86 -
1.87 -fun string_of_thmref (Name name) = name
1.88 - | string_of_thmref (NameSelection (name, is)) =
1.89 - name ^ enclose "(" ")" (commas (map string_of_interval is))
1.90 - | string_of_thmref (Fact _) = error "Illegal literal fact";
1.91 -
1.92 -
1.93 -(* select_thm *)
1.94 -
1.95 -fun select_thm (Name _) thms = thms
1.96 - | select_thm (Fact _) thms = thms
1.97 - | select_thm (NameSelection (name, ivs)) thms =
1.98 - let
1.99 - val n = length thms;
1.100 - fun err msg = error (msg ^ " for " ^ quote name ^ " (length " ^ string_of_int n ^ ")");
1.101 - fun select i =
1.102 - if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
1.103 - else nth thms (i - 1);
1.104 - val is = maps (interval n) ivs handle Fail msg => err msg;
1.105 - in map select is end;
1.106 -
1.107 -
1.108 -(* selections *)
1.109 -
1.110 -fun selections (name, [thm]) = [(Name name, thm)]
1.111 - | selections (name, thms) = (1 upto length thms, thms) |> ListPair.map (fn (i, thm) =>
1.112 - (NameSelection (name, [Single i]), thm));
1.113 -
1.114 -
1.115 -(* lookup/get thms *)
1.116 -
1.117 local
1.118
1.119 fun lookup_thms thy xname =
1.120 @@ -270,7 +189,7 @@
1.121
1.122 fun get_fact silent theory thmref =
1.123 let
1.124 - val name = name_of_thmref thmref;
1.125 + val name = Facts.name_of_ref thmref;
1.126 val new_res = lookup_fact theory name;
1.127 val old_res = get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory);
1.128 val is_same =
1.129 @@ -283,14 +202,13 @@
1.130 else legacy_feature ("Fact lookup differs from old-style thm database:\n" ^
1.131 show_result new_res ^ " vs " ^ show_result old_res ^
1.132 Position.str_of (Position.thread_data ()));
1.133 - in Option.map #2 old_res |> the_thms name |> select_thm thmref |> map (Thm.transfer theory) end;
1.134 + in Option.map #2 old_res |> the_thms name |> Facts.select thmref |> map (Thm.transfer theory) end;
1.135
1.136 in
1.137
1.138 val get_thms_silent = get_fact true;
1.139 val get_thms = get_fact false;
1.140 -fun get_thmss thy thmrefs = maps (get_thms thy) thmrefs;
1.141 -fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref);
1.142 +fun get_thm thy thmref = Facts.the_single (Facts.name_of_ref thmref) (get_thms thy thmref);
1.143
1.144 end;
1.145