datatype thmref = Name ... | NameSelection ...;
authorwenzelm
Mon Jun 20 22:14:07 2005 +0200 (2005-06-20)
changeset 16493d0f6c33b2300
parent 16492 fbfd15412f05
child 16494 6961e8ab33e1
datatype thmref = Name ... | NameSelection ...;
added print_theorems_diff;
tuned;
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Mon Jun 20 22:14:06 2005 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Mon Jun 20 22:14:07 2005 +0200
     1.3 @@ -7,7 +7,8 @@
     1.4  
     1.5  signature BASIC_PURE_THY =
     1.6  sig
     1.7 -  type thmref
     1.8 +  datatype interval = FromTo of int * int | From of int | Single of int
     1.9 +  datatype thmref = Name of string | NameSelection of string * interval list
    1.10    val print_theorems: theory -> unit
    1.11    val print_theory: theory -> unit
    1.12    val get_thm: theory -> thmref -> thm
    1.13 @@ -23,12 +24,14 @@
    1.14  signature PURE_THY =
    1.15  sig
    1.16    include BASIC_PURE_THY
    1.17 -  datatype interval = FromTo of int * int | From of int | Single of int
    1.18    val string_of_thmref: thmref -> string
    1.19    val theorem_space: theory -> NameSpace.T
    1.20 +  val print_theorems_diff: theory -> theory -> unit
    1.21    val get_thm_closure: theory -> thmref -> thm
    1.22    val get_thms_closure: theory -> thmref -> thm list
    1.23    val single_thm: string -> thm list -> thm
    1.24 +  val name_of_thmref: thmref -> string
    1.25 +  val map_name_of_thmref: (string -> string) -> thmref -> thmref
    1.26    val select_thm: thmref -> thm list -> thm list
    1.27    val selections: string * thm list -> (thmref * thm) list
    1.28    val fact_index_of: theory -> FactIndex.T
    1.29 @@ -78,15 +81,20 @@
    1.30  
    1.31  (** dataype theorems **)
    1.32  
    1.33 -fun pretty_theorems thy theorems =
    1.34 +fun pretty_theorems_diff thy prev_thms (space, thms) =
    1.35    let
    1.36      val prt_thm = Display.pretty_thm_sg thy;
    1.37      fun prt_thms (name, [th]) =
    1.38            Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
    1.39        | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
    1.40 -    val thmss = NameSpace.extern_table theorems;
    1.41 +
    1.42 +    val diff_thmss = Symtab.fold (fn fact =>
    1.43 +      if not (Symtab.member eq_thms prev_thms fact) then cons fact else I) thms [];
    1.44 +    val thmss = diff_thmss |> map (apfst (NameSpace.extern space)) |> Library.sort_wrt #1;
    1.45    in Pretty.big_list "theorems:" (map prt_thms thmss) end;
    1.46  
    1.47 +fun pretty_theorems thy = pretty_theorems_diff thy Symtab.empty;
    1.48 +
    1.49  structure TheoremsData = TheoryDataFun
    1.50  (struct
    1.51    val name = "Pure/theorems";
    1.52 @@ -104,18 +112,23 @@
    1.53    fun print thy (ref {theorems, index}) = Pretty.writeln (pretty_theorems thy theorems);
    1.54  end);
    1.55  
    1.56 -val get_theorems = TheoremsData.get;
    1.57 -val theorem_space = #1 o #theorems o ! o get_theorems;
    1.58 -val fact_index_of = #index o ! o get_theorems;
    1.59 +val get_theorems_ref = TheoremsData.get;
    1.60 +val get_theorems = ! o get_theorems_ref;
    1.61 +val theorem_space = #1 o #theorems o get_theorems;
    1.62 +val fact_index_of = #index o get_theorems;
    1.63  
    1.64  
    1.65  (* print theory *)
    1.66  
    1.67  val print_theorems = TheoremsData.print;
    1.68  
    1.69 +fun print_theorems_diff prev_thy thy =
    1.70 +  Pretty.writeln (pretty_theorems_diff thy
    1.71 +    (#2 (#theorems (get_theorems prev_thy))) (#theorems (get_theorems thy)));
    1.72 +
    1.73  fun print_theory thy =
    1.74    Display.pretty_full_theory thy @
    1.75 -    [pretty_theorems thy (#theorems (! (get_theorems thy)))]
    1.76 +    [pretty_theorems thy (#theorems (get_theorems thy))]
    1.77    |> Pretty.chunks |> Pretty.writeln;
    1.78  
    1.79  
    1.80 @@ -145,19 +158,27 @@
    1.81    | string_of_interval (Single i) = string_of_int i;
    1.82  
    1.83  
    1.84 -(* type thmref *)
    1.85 +(* datatype thmref *)
    1.86 +
    1.87 +datatype thmref =
    1.88 +  Name of string |
    1.89 +  NameSelection of string * interval list;
    1.90  
    1.91 -type thmref = xstring * interval list option;
    1.92 +fun name_of_thmref (Name name) = name
    1.93 +  | name_of_thmref (NameSelection (name, _)) = name;
    1.94  
    1.95 -fun string_of_thmref (name, NONE) = name
    1.96 -  | string_of_thmref (name, SOME is) =
    1.97 +fun map_name_of_thmref f (Name name) = Name (f name)
    1.98 +  | map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is);
    1.99 +
   1.100 +fun string_of_thmref (Name name) = name
   1.101 +  | string_of_thmref (NameSelection (name, is)) =
   1.102        name ^ enclose "(" ")" (commas (map string_of_interval is));
   1.103  
   1.104  
   1.105  (* select_thm *)
   1.106  
   1.107 -fun select_thm (_, NONE) thms = thms
   1.108 -  | select_thm (name, SOME is) thms =
   1.109 +fun select_thm (Name _) thms = thms
   1.110 +  | select_thm (NameSelection (name, is)) thms =
   1.111        let
   1.112          val n = length thms;
   1.113          fun select i =
   1.114 @@ -170,9 +191,9 @@
   1.115  
   1.116  (* selections *)
   1.117  
   1.118 -fun selections (name, [thm]) = [((name, NONE), thm)]
   1.119 +fun selections (name, [thm]) = [(Name name, thm)]
   1.120    | selections (name, thms) = (1 upto length thms, thms) |> ListPair.map (fn (i, thm) =>
   1.121 -      ((name, SOME [Single i]), thm));
   1.122 +      (NameSelection (name, [Single i]), thm));
   1.123  
   1.124  
   1.125  (* get_thm(s)_closure -- statically scoped versions *)
   1.126 @@ -182,7 +203,7 @@
   1.127  fun lookup_thms thy =
   1.128    let
   1.129      val thy_ref = Theory.self_ref thy;
   1.130 -    val ref {theorems = (space, thms), ...} = get_theorems thy;
   1.131 +    val (space, thms) = #theorems (get_theorems thy);
   1.132    in
   1.133      fn name =>
   1.134        Option.map (map (Thm.transfer (Theory.deref thy_ref)))    (*dynamic identity*)
   1.135 @@ -191,22 +212,26 @@
   1.136  
   1.137  fun get_thms_closure thy =
   1.138    let val closures = map lookup_thms (thy :: Theory.ancestors_of thy) in
   1.139 -    fn (name, i) => select_thm (name, i) (the_thms name (get_first (fn f => f name) closures))
   1.140 +    fn thmref =>
   1.141 +      let val name = name_of_thmref thmref
   1.142 +      in select_thm thmref (the_thms name (get_first (fn f => f name) closures)) end
   1.143    end;
   1.144  
   1.145  fun get_thm_closure thy =
   1.146    let val get = get_thms_closure thy
   1.147 -  in fn (name, i) => single_thm name (get (name, i)) end;
   1.148 +  in fn thmref => single_thm (name_of_thmref thmref) (get thmref) end;
   1.149  
   1.150  
   1.151  (* get_thms etc. *)
   1.152  
   1.153 -fun get_thms theory (name, i) =
   1.154 -  get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory)
   1.155 -  |> the_thms name |> select_thm (name, i) |> map (Thm.transfer theory);
   1.156 +fun get_thms theory thmref =
   1.157 +  let val name = name_of_thmref thmref in
   1.158 +    get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory)
   1.159 +    |> the_thms name |> select_thm thmref |> map (Thm.transfer theory)
   1.160 +  end;
   1.161  
   1.162 -fun get_thmss thy names = List.concat (map (get_thms thy) names);
   1.163 -fun get_thm thy (name, i) = single_thm name (get_thms thy (name, i));
   1.164 +fun get_thmss thy thmrefs = List.concat (map (get_thms thy) thmrefs);
   1.165 +fun get_thm thy thmref = single_thm (name_of_thmref thmref) (get_thms thy thmref);
   1.166  
   1.167  
   1.168  (* thms_containing etc. *)
   1.169 @@ -220,7 +245,7 @@
   1.170    (theory :: Theory.ancestors_of theory)
   1.171    |> map (fn thy =>
   1.172        FactIndex.find (fact_index_of thy) spec
   1.173 -      |> List.filter (fn (name, ths) => valid_thms theory ((name, NONE), ths))
   1.174 +      |> List.filter (fn (name, ths) => valid_thms theory (Name name, ths))
   1.175        |> gen_distinct eq_fst)
   1.176    |> List.concat;
   1.177  
   1.178 @@ -232,7 +257,7 @@
   1.179  (* thms_of etc. *)
   1.180  
   1.181  fun thms_of thy =
   1.182 -  let val ref {theorems = (_, thms), ...} = get_theorems thy in
   1.183 +  let val (_, thms) = #theorems (get_theorems thy) in
   1.184      map (fn th => (Thm.name_of_thm th, th)) (List.concat (map snd (Symtab.dest thms)))
   1.185    end;
   1.186  
   1.187 @@ -246,7 +271,7 @@
   1.188  
   1.189  fun hide_thms fully names thy =
   1.190    let
   1.191 -    val r as ref {theorems = (space, thms), index} = get_theorems thy;
   1.192 +    val r as ref {theorems = (space, thms), index} = get_theorems_ref thy;
   1.193      val space' = fold (NameSpace.hide fully) names space;
   1.194    in r := {theorems = (space', thms), index = index}; thy end;
   1.195  
   1.196 @@ -280,7 +305,7 @@
   1.197    | enter_thms pre_name post_name app_att (bname, thms) thy =
   1.198        let
   1.199          val name = Sign.full_name thy bname;
   1.200 -        val r as ref {theorems = (space, theorems), index} = get_theorems thy;
   1.201 +        val r as ref {theorems = (space, theorems), index} = get_theorems_ref thy;
   1.202          val space' = Sign.declare_name thy name space;
   1.203          val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
   1.204          val theorems' = Symtab.update ((name, thms'), theorems);
   1.205 @@ -423,7 +448,7 @@
   1.206  val A = Free ("A", propT);
   1.207  
   1.208  val proto_pure =
   1.209 -  Context.pre_pure
   1.210 +  Context.pre_pure_thy
   1.211    |> Sign.init
   1.212    |> Theory.init
   1.213    |> Proofterm.init
   1.214 @@ -461,7 +486,7 @@
   1.215     [("Goal_def", Logic.mk_equals (Logic.mk_goal A, A))]
   1.216    |> (#1 o add_thmss [(("nothing", []), [])])
   1.217    |> Theory.add_axioms_i Proofterm.equality_axms
   1.218 -  |> Context.end_theory;
   1.219 +  |> Theory.end_theory;
   1.220  
   1.221  structure ProtoPure =
   1.222  struct