# HG changeset patch # User haftmann # Date 1157529664 -7200 # Node ID 04aa552a83bc2824cf841e34ce847519c77defb9 # Parent 0f6302a48fa66a1e298f743dff3d619b55ed4eee TypedefPackage.add_typedef_* now yields name of introduced type constructor diff -r 0f6302a48fa6 -r 04aa552a83bc src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Tue Sep 05 22:06:18 2006 +0200 +++ b/src/HOL/Import/proof_kernel.ML Wed Sep 06 10:01:04 2006 +0200 @@ -2094,7 +2094,7 @@ val tnames = map fst tfrees val tsyn = mk_syn thy tycname val typ = (tycname,tnames,tsyn) - val (typedef_info, thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy + val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2 val th3 = (#type_definition typedef_info) RS typedef_hol2hol4 @@ -2187,7 +2187,7 @@ val tnames = sort string_ord (map fst tfrees) val tsyn = mk_syn thy tycname val typ = (tycname,tnames,tsyn) - val (typedef_info, thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy + val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2 val fulltyname = Sign.intern_type thy' tycname val aty = Type (fulltyname, map mk_vartype tnames) diff -r 0f6302a48fa6 -r 04aa552a83bc src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Tue Sep 05 22:06:18 2006 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Wed Sep 06 10:01:04 2006 +0200 @@ -548,19 +548,20 @@ (* FIXME: theorems are stored in database for testing only *) val perm_closed_thmss = map mk_perm_closed atoms; - val (_,thy5) = PureThy.add_thmss [(("perm_closed", List.concat perm_closed_thmss), [])] thy4; + val (_, thy5) = PureThy.add_thmss [(("perm_closed", List.concat perm_closed_thmss), [])] thy4; (**** typedef ****) val _ = warning "defining type..."; val (typedefs, thy6) = - fold_map (fn ((((name, mx), tvs), c), name') => fn thy => + thy5 + |> fold_map (fn ((((name, mx), tvs), c), name') => fn thy => setmp TypedefPackage.quiet_mode true (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE (rtac exI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) - (resolve_tac rep_intrs 1))) thy |> (fn (r, thy) => + (resolve_tac rep_intrs 1))) thy |> (fn ((_, r), thy) => let val permT = mk_permT (TFree (Name.variant tvs "'a", HOLogic.typeS)); val pi = Free ("pi", permT); @@ -576,7 +577,7 @@ Free ("x", T))))), [])] thy) end)) (types_syntax ~~ tyvars ~~ - (List.take (ind_consts, length new_type_names)) ~~ new_type_names) thy5; + (List.take (ind_consts, length new_type_names)) ~~ new_type_names); val perm_defs = map snd typedefs; val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs; diff -r 0f6302a48fa6 -r 04aa552a83bc src/HOL/Tools/typecopy_package.ML --- a/src/HOL/Tools/typecopy_package.ML Tue Sep 05 22:06:18 2006 +0200 +++ b/src/HOL/Tools/typecopy_package.ML Wed Sep 06 10:01:04 2006 +0200 @@ -16,7 +16,7 @@ proj_def: thm } val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option - -> theory -> info * theory + -> theory -> (string * info) * theory val get_typecopies: theory -> string list val get_typecopy_info: theory -> string -> info option type hook = string * info -> theory -> theory; @@ -94,16 +94,15 @@ local -fun gen_add_typecopy prep_typ (tyco, raw_vs) raw_ty constr_proj thy = +fun gen_add_typecopy prep_typ (raw_tyco, raw_vs) raw_ty constr_proj thy = let val ty = prep_typ thy raw_ty; val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs; val tac = Tactic.rtac UNIV_witness 1; - fun add_info ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, + fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, Rep_name = c_rep, Abs_inject = inject, Abs_inverse = inverse, ... } : TypedefPackage.info ) thy = let - val Type (tyco', _) = ty_abs; val exists_thm = UNIV_I |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] []; @@ -119,15 +118,16 @@ }; in thy - |> (TypecopyData.map o apfst o Symtab.update_new) (tyco', info) - |> invoke_hooks (tyco', info) - |> pair info + |> (TypecopyData.map o apfst o Symtab.update_new) (tyco, info) + |> invoke_hooks (tyco, info) + |> pair (tyco, info) end in thy - |> TypedefPackage.add_typedef_i false (SOME tyco) (tyco, map fst vs, NoSyn) - (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac - |-> (fn info => add_info info) + |> setmp TypedefPackage.quiet_mode true + (TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn) + (HOLogic.mk_UNIV ty) (Option.map swap constr_proj)) tac + |-> (fn (tyco, info) => add_info tyco info) end; in diff -r 0f6302a48fa6 -r 04aa552a83bc src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Tue Sep 05 22:06:18 2006 +0200 +++ b/src/HOL/Tools/typedef_package.ML Wed Sep 06 10:01:04 2006 +0200 @@ -16,9 +16,9 @@ Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; val get_info: theory -> string -> info option val add_typedef: bool -> string option -> bstring * string list * mixfix -> - string -> (bstring * bstring) option -> tactic -> theory -> info * theory + string -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory val add_typedef_i: bool -> string option -> bstring * string list * mixfix -> - term -> (bstring * bstring) option -> tactic -> theory -> info * theory + term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory val typedef: (bool * string) * (bstring * string list * mixfix) * string * (string * string) option -> theory -> Proof.state val typedef_i: (bool * string) * (bstring * string list * mixfix) * term @@ -197,7 +197,7 @@ Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; val thy3 = thy2 |> put_info full_tname info; - in (info, Context.Theory thy3) end); + in ((full_tname, info), Context.Theory thy3) end); (* errors *) @@ -268,9 +268,12 @@ val (_, goal, goal_pat, typedef_result) = prepare_typedef prep_term def name typ set opt_morphs thy; fun att (thy, th) = - let val ({type_definition, ...}, thy') = typedef_result th thy + let val ((name, {type_definition, ...}), thy') = typedef_result th thy in (thy', type_definition) end; - in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, [goal_pat]) thy end; + in + thy + |> IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, [goal_pat]) + end; in diff -r 0f6302a48fa6 -r 04aa552a83bc src/HOLCF/pcpodef_package.ML --- a/src/HOLCF/pcpodef_package.ML Tue Sep 05 22:06:18 2006 +0200 +++ b/src/HOLCF/pcpodef_package.ML Wed Sep 06 10:01:04 2006 +0200 @@ -101,7 +101,7 @@ ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"]) (ClassPackage.intro_classes_tac []) ||>> PureThy.add_defs_i true [Thm.no_attributes less_def] - |-> (fn ({type_definition, set_def, ...}, [less_definition]) => + |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) => AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"]) (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1) #> rpair (type_definition, less_definition, set_def));