accomodate change of TheoryDataFun;
authorwenzelm
Fri Jun 17 18:33:15 2005 +0200 (2005-06-17)
changeset 16430bc07926e4f03
parent 16429 e871f4b1a4f0
child 16431 90c9b8bb3b66
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
Sign.the_const_type;
Context.exists_name;
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jun 17 18:33:14 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Jun 17 18:33:15 2005 +0200
     1.3 @@ -63,17 +63,12 @@
     1.4         size : thm list,
     1.5         simps : thm list}
     1.6    val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
     1.7 -  val get_datatypes_sg : Sign.sg -> DatatypeAux.datatype_info Symtab.table
     1.8    val print_datatypes : theory -> unit
     1.9 -  val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info option
    1.10    val datatype_info : theory -> string -> DatatypeAux.datatype_info option
    1.11 -  val datatype_info_sg_err : Sign.sg -> string -> DatatypeAux.datatype_info
    1.12    val datatype_info_err : theory -> string -> DatatypeAux.datatype_info
    1.13    val constrs_of : theory -> string -> term list option
    1.14 -  val constrs_of_sg : Sign.sg -> string -> term list option
    1.15    val case_const_of : theory -> string -> term option
    1.16    val weak_case_congs_of : theory -> thm list
    1.17 -  val weak_case_congs_of_sg : Sign.sg -> thm list
    1.18    val setup: (theory -> theory) list
    1.19  end;
    1.20  
    1.21 @@ -87,23 +82,21 @@
    1.22  
    1.23  (* data kind 'HOL/datatypes' *)
    1.24  
    1.25 -structure DatatypesArgs =
    1.26 -struct
    1.27 +structure DatatypesData = TheoryDataFun
    1.28 +(struct
    1.29    val name = "HOL/datatypes";
    1.30    type T = datatype_info Symtab.table;
    1.31  
    1.32    val empty = Symtab.empty;
    1.33    val copy = I;
    1.34 -  val prep_ext = I;
    1.35 -  val merge: T * T -> T = Symtab.merge (K true);
    1.36 +  val extend = I;
    1.37 +  fun merge _ tabs : T = Symtab.merge (K true) tabs;
    1.38  
    1.39    fun print sg tab =
    1.40      Pretty.writeln (Pretty.strs ("datatypes:" ::
    1.41        map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
    1.42 -end;
    1.43 +end);
    1.44  
    1.45 -structure DatatypesData = TheoryDataFun(DatatypesArgs);
    1.46 -val get_datatypes_sg = DatatypesData.get_sg;
    1.47  val get_datatypes = DatatypesData.get;
    1.48  val put_datatypes = DatatypesData.put;
    1.49  val print_datatypes = DatatypesData.print;
    1.50 @@ -111,34 +104,24 @@
    1.51  
    1.52  (** theory information about datatypes **)
    1.53  
    1.54 -fun datatype_info_sg sg name = Symtab.lookup (get_datatypes_sg sg, name);
    1.55 -
    1.56 -fun datatype_info_sg_err sg name = (case datatype_info_sg sg name of
    1.57 -      SOME info => info
    1.58 -    | NONE => error ("Unknown datatype " ^ quote name));
    1.59 -
    1.60 -val datatype_info = datatype_info_sg o Theory.sign_of;
    1.61 +fun datatype_info thy name = Symtab.lookup (get_datatypes thy, name);
    1.62  
    1.63  fun datatype_info_err thy name = (case datatype_info thy name of
    1.64        SOME info => info
    1.65      | NONE => error ("Unknown datatype " ^ quote name));
    1.66  
    1.67 -fun constrs_of_sg sg tname = (case datatype_info_sg sg tname of
    1.68 +fun constrs_of thy tname = (case datatype_info thy tname of
    1.69     SOME {index, descr, ...} =>
    1.70       let val (_, _, constrs) = valOf (assoc (descr, index))
    1.71 -     in SOME (map (fn (cname, _) => Const (cname, valOf (Sign.const_type sg cname))) constrs)
    1.72 +     in SOME (map (fn (cname, _) => Const (cname, Sign.the_const_type thy cname)) constrs)
    1.73       end
    1.74   | _ => NONE);
    1.75  
    1.76 -val constrs_of = constrs_of_sg o Theory.sign_of;
    1.77 -
    1.78  fun case_const_of thy tname = (case datatype_info thy tname of
    1.79 -   SOME {case_name, ...} => SOME (Const (case_name, valOf (Sign.const_type
    1.80 -     (Theory.sign_of thy) case_name)))
    1.81 +   SOME {case_name, ...} => SOME (Const (case_name, Sign.the_const_type thy case_name))
    1.82   | _ => NONE);
    1.83  
    1.84 -val weak_case_congs_of_sg = map (#weak_case_cong o #2) o Symtab.dest o get_datatypes_sg;
    1.85 -val weak_case_congs_of = weak_case_congs_of_sg o Theory.sign_of;
    1.86 +val weak_case_congs_of = map (#weak_case_cong o #2) o Symtab.dest o get_datatypes;
    1.87  
    1.88  fun find_tname var Bi =
    1.89    let val frees = map dest_Free (term_frees Bi)
    1.90 @@ -197,7 +180,7 @@
    1.91          SOME r => (r, "Induction rule")
    1.92        | NONE =>
    1.93            let val tn = find_tname (hd (List.mapPartial I (List.concat varss))) Bi
    1.94 -          in (#induction (datatype_info_sg_err sign tn), "Induction rule for type " ^ tn) end);
    1.95 +          in (#induction (datatype_info_err sign tn), "Induction rule for type " ^ tn) end);
    1.96  
    1.97      val concls = HOLogic.dest_concls (Thm.concl_of rule);
    1.98      val insts = List.concat (map prep_inst (concls ~~ varss)) handle UnequalLengths =>
    1.99 @@ -229,7 +212,7 @@
   1.100        let val tn = infer_tname state i t in
   1.101          if tn = HOLogic.boolN then inst_tac [(("P", 0), t)] case_split_thm i state
   1.102          else case_inst_tac inst_tac t
   1.103 -               (#exhaustion (datatype_info_sg_err (Thm.sign_of_thm state) tn))
   1.104 +               (#exhaustion (datatype_info_err (Thm.sign_of_thm state) tn))
   1.105                 i state
   1.106        end handle THM _ => Seq.empty;
   1.107  
   1.108 @@ -349,7 +332,7 @@
   1.109           (case (stripT (0, T1), stripT (0, T2)) of
   1.110              ((i', Type (tname1, _)), (j', Type (tname2, _))) =>
   1.111                  if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
   1.112 -                   (case (constrs_of_sg sg tname1) of
   1.113 +                   (case (constrs_of sg tname1) of
   1.114                        SOME constrs => let val cnames = map (fst o dest_Const) constrs
   1.115                          in if cname1 mem cnames andalso cname2 mem cnames then
   1.116                               let val eq_t = Logic.mk_equals (t, Const ("False", HOLogic.boolT));
   1.117 @@ -358,7 +341,7 @@
   1.118                                   val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
   1.119                                     map (get_thm Datatype_thy o rpair NONE)
   1.120                                       ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]
   1.121 -                             in (case (#distinct (datatype_info_sg_err sg tname1)) of
   1.122 +                             in (case (#distinct (datatype_info_err sg tname1)) of
   1.123                                   QuickAndDirty => SOME (Thm.invoke_oracle
   1.124                                     Datatype_thy distinctN (sg, ConstrDistinct eq_t))
   1.125                                 | FewConstrs thms => SOME (Tactic.prove sg [] [] eq_t (K
   1.126 @@ -380,7 +363,7 @@
   1.127    | distinct_proc sg _ _ = NONE;
   1.128  
   1.129  val distinct_simproc =
   1.130 -  Simplifier.simproc (Theory.sign_of HOL.thy) distinctN ["s = t"] distinct_proc;
   1.131 +  Simplifier.simproc HOL.thy distinctN ["s = t"] distinct_proc;
   1.132  
   1.133  val dist_ss = HOL_ss addsimprocs [distinct_simproc];
   1.134  
   1.135 @@ -403,7 +386,7 @@
   1.136        fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
   1.137          | dest_case2 t = [t];
   1.138        val cases as ((cname, _), _) :: _ = map dest_case1 (dest_case2 u);
   1.139 -      val tab = Symtab.dest (get_datatypes_sg sg);
   1.140 +      val tab = Symtab.dest (get_datatypes sg);
   1.141        val (cases', default) = (case split_last cases of
   1.142            (cases', (("dummy_pattern", []), t)) => (cases', SOME t)
   1.143          | _ => (cases, NONE))
   1.144 @@ -623,8 +606,8 @@
   1.145          (name, Ts @ [T] ---> freeT, NoSyn))
   1.146            (case_names ~~ newTs ~~ case_fn_Ts));
   1.147  
   1.148 -    val reccomb_names' = map (Sign.intern_const (Theory.sign_of thy2')) reccomb_names;
   1.149 -    val case_names' = map (Sign.intern_const (Theory.sign_of thy2')) case_names;
   1.150 +    val reccomb_names' = map (Sign.intern_const thy2') reccomb_names;
   1.151 +    val case_names' = map (Sign.intern_const thy2') case_names;
   1.152  
   1.153      val thy2 = thy2' |>
   1.154  
   1.155 @@ -840,7 +823,7 @@
   1.156      val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   1.157        [descr] sorts thy7;
   1.158      val (thy9, size_thms) =
   1.159 -      if Sign.exists_stamp "NatArith" (Theory.sign_of thy8) then
   1.160 +      if Context.exists_name "NatArith" thy8 then
   1.161          DatatypeAbsProofs.prove_size_thms false new_type_names
   1.162            [descr] sorts reccomb_names rec_thms thy8
   1.163        else (thy8, []);