src/HOL/Tools/typedef_package.ML
changeset 16458 4c6fd0c01d28
parent 16126 3ba9eb7ea366
child 16486 1a12cdb6ee6b
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/Tools/typedef_package.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Markus Wenzel, TU Muenchen
     1.7 +    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     1.8  
     1.9  Gordon/HOL-style type definitions.
    1.10  *)
    1.11 @@ -50,18 +50,16 @@
    1.12  
    1.13  (** theory data **)
    1.14  
    1.15 -structure TypedefArgs =
    1.16 -struct
    1.17 +structure TypedefData = TheoryDataFun
    1.18 +(struct
    1.19    val name = "HOL/typedef";
    1.20    type T = (typ * typ * string * string) Symtab.table;
    1.21    val empty = Symtab.empty;
    1.22    val copy = I;
    1.23 -  val prep_ext = I;
    1.24 -  val merge : T * T -> T = Symtab.merge op =;
    1.25 -  fun print sg _ = ();
    1.26 -end;
    1.27 -
    1.28 -structure TypedefData = TheoryDataFun(TypedefArgs);
    1.29 +  val extend = I;
    1.30 +  fun merge _ (tabs: T * T) = Symtab.merge (op =) tabs;
    1.31 +  fun print _ _ = ();
    1.32 +end);
    1.33  
    1.34  fun put_typedef newT oldT Abs_name Rep_name thy =
    1.35    TypedefData.put (Symtab.update_new
    1.36 @@ -74,16 +72,14 @@
    1.37  
    1.38  fun add_typedecls decls thy =
    1.39    let
    1.40 -    val full = Sign.full_name (Theory.sign_of thy);
    1.41 -
    1.42      fun arity_of (raw_name, args, mx) =
    1.43 -      (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.typeS, HOLogic.typeS);
    1.44 +      (Sign.full_name thy (Syntax.type_name raw_name mx),
    1.45 +        replicate (length args) HOLogic.typeS, HOLogic.typeS);
    1.46    in
    1.47      if can (Theory.assert_super HOL.thy) thy then
    1.48 -      thy
    1.49 -      |> PureThy.add_typedecls decls
    1.50 +      thy |> Theory.add_typedecls decls
    1.51        |> Theory.add_arities_i (map arity_of decls)
    1.52 -    else thy |> PureThy.add_typedecls decls
    1.53 +    else thy |> Theory.add_typedecls decls
    1.54    end;
    1.55  
    1.56  
    1.57 @@ -109,16 +105,17 @@
    1.58        getOpt (witn2_tac, TRY (ALLGOALS (CLASET' blast_tac)));
    1.59    in
    1.60      message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
    1.61 -    Tactic.prove (Theory.sign_of thy) [] [] goal (K tac)
    1.62 -  end handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    1.63 +    Tactic.prove thy [] [] goal (K tac)
    1.64 +  end
    1.65 +  handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    1.66  
    1.67  
    1.68  (* prepare_typedef *)
    1.69  
    1.70 -fun read_term sg used s =
    1.71 -  #1 (Thm.read_def_cterm (sg, K NONE, K NONE) used true (s, HOLogic.typeT));
    1.72 +fun read_term thy used s =
    1.73 +  #1 (Thm.read_def_cterm (thy, K NONE, K NONE) used true (s, HOLogic.typeT));
    1.74  
    1.75 -fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
    1.76 +fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg;
    1.77  
    1.78  fun err_in_typedef name =
    1.79    error ("The error(s) above occurred in typedef " ^ quote name);
    1.80 @@ -126,16 +123,15 @@
    1.81  fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
    1.82    let
    1.83      val _ = Theory.requires thy "Typedef" "typedefs";
    1.84 -    val sign = Theory.sign_of thy;
    1.85 -    val full = Sign.full_name sign;
    1.86 +    val full = Sign.full_name thy;
    1.87  
    1.88      (*rhs*)
    1.89      val full_name = full name;
    1.90 -    val cset = prep_term sign vs raw_set;
    1.91 +    val cset = prep_term thy vs raw_set;
    1.92      val {T = setT, t = set, ...} = Thm.rep_cterm cset;
    1.93      val rhs_tfrees = term_tfrees set;
    1.94      val oldT = HOLogic.dest_setT setT handle TYPE _ =>
    1.95 -      error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT));
    1.96 +      error ("Not a set type: " ^ quote (Sign.string_of_typ thy setT));
    1.97      fun mk_nonempty A =
    1.98        HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
    1.99      val goal = mk_nonempty set;
   1.100 @@ -283,7 +279,7 @@
   1.101          val (gr', _) = Codegen.invoke_tycodegen thy dep false (gr, T);
   1.102          val (gr'', ps) =
   1.103            foldl_map (Codegen.invoke_codegen thy dep true) (gr', ts);
   1.104 -        val id = Codegen.mk_const_id (sign_of thy) s
   1.105 +        val id = Codegen.mk_const_id thy s
   1.106        in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
   1.107      fun get_name (Type (tname, _)) = tname
   1.108        | get_name _ = "";
   1.109 @@ -312,10 +308,9 @@
   1.110         | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
   1.111             if isSome (Codegen.get_assoc_type thy tname) then NONE else
   1.112             let
   1.113 -             val sg = sign_of thy;
   1.114 -             val Abs_id = Codegen.mk_const_id sg Abs_name;
   1.115 -             val Rep_id = Codegen.mk_const_id sg Rep_name;
   1.116 -             val ty_id = Codegen.mk_type_id sg s;
   1.117 +             val Abs_id = Codegen.mk_const_id thy Abs_name;
   1.118 +             val Rep_id = Codegen.mk_const_id thy Rep_name;
   1.119 +             val ty_id = Codegen.mk_type_id thy s;
   1.120               val (gr', qs) = foldl_map
   1.121                 (Codegen.invoke_tycodegen thy dep (length Ts = 1)) (gr, Ts);
   1.122               val gr'' = Graph.add_edge (Abs_id, dep) gr' handle Graph.UNDEF _ =>
   1.123 @@ -334,21 +329,21 @@
   1.124                       Pretty.str "x) = x;"]) ^ "\n\n" ^
   1.125                     (if "term_of" mem !Codegen.mode then
   1.126                        Pretty.string_of (Pretty.block [Pretty.str "fun ",
   1.127 -                        Codegen.mk_term_of sg false newT, Pretty.brk 1,
   1.128 +                        Codegen.mk_term_of thy false newT, Pretty.brk 1,
   1.129                          Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
   1.130                          Pretty.str "x) =", Pretty.brk 1,
   1.131                          Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
   1.132                            Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
   1.133                            Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
   1.134 -                        Codegen.mk_term_of sg false oldT, Pretty.brk 1,
   1.135 +                        Codegen.mk_term_of thy false oldT, Pretty.brk 1,
   1.136                          Pretty.str "x;"]) ^ "\n\n"
   1.137                      else "") ^
   1.138                     (if "test" mem !Codegen.mode then
   1.139                        Pretty.string_of (Pretty.block [Pretty.str "fun ",
   1.140 -                        Codegen.mk_gen sg false [] "" newT, Pretty.brk 1,
   1.141 +                        Codegen.mk_gen thy false [] "" newT, Pretty.brk 1,
   1.142                          Pretty.str "i =", Pretty.brk 1,
   1.143                          Pretty.block [Pretty.str (Abs_id ^ " ("),
   1.144 -                          Codegen.mk_gen sg false [] "" oldT, Pretty.brk 1,
   1.145 +                          Codegen.mk_gen thy false [] "" oldT, Pretty.brk 1,
   1.146                            Pretty.str "i);"]]) ^ "\n\n"
   1.147                      else "")
   1.148                 in Graph.map_node Abs_id (K (NONE, s)) gr'' end