# HG changeset patch # User haftmann # Date 1144332560 -7200 # Node ID 094a1c071c8eb7988abbb9ba973517fe2fe0c11d # Parent 3414c04fbc39df35a3e3cdfb2f6d7639276243b9 added functions for definitional code generation diff -r 3414c04fbc39 -r 094a1c071c8e src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Thu Apr 06 16:08:25 2006 +0200 +++ b/src/HOL/Tools/typedef_package.ML Thu Apr 06 16:09:20 2006 +0200 @@ -10,20 +10,21 @@ val quiet_mode: bool ref val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory val add_typedef: bool -> string option -> bstring * string list * mixfix -> - string -> (bstring * bstring) option -> tactic -> theory -> theory * + string -> (bstring * bstring) option -> tactic -> theory -> {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, - Rep_induct: thm, Abs_induct: thm} + Rep_induct: thm, Abs_induct: thm} * theory val add_typedef_i: bool -> string option -> bstring * string list * mixfix -> - term -> (bstring * bstring) option -> tactic -> theory -> theory * + term -> (bstring * bstring) option -> tactic -> theory -> {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, - Rep_induct: thm, Abs_induct: thm} + Rep_induct: thm, Abs_induct: thm} * 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 * (string * string) option -> theory -> Proof.state val setup: theory -> theory + structure TypedefData : THEORY_DATA end; structure TypedefPackage: TYPEDEF_PACKAGE = @@ -74,7 +75,7 @@ structure TypedefData = TheoryDataFun (struct val name = "HOL/typedef"; - type T = (typ * typ * string * string) Symtab.table; + type T = ((typ * typ * string * string) * (thm option * thm * thm)) Symtab.table; val empty = Symtab.empty; val copy = I; val extend = I; @@ -82,8 +83,9 @@ fun print _ _ = (); end); -fun put_typedef newT oldT Abs_name Rep_name = - TypedefData.map (Symtab.update_new (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name))); +fun put_typedef newT oldT Abs_name Rep_name def inject inverse = + TypedefData.map (Symtab.update_new (fst (dest_Type newT), + ((newT, oldT, Abs_name, Rep_name), (def, inject, inverse)))); (* prepare_typedef *) @@ -150,9 +152,8 @@ else (NONE, thy); - fun typedef_result (context, nonempty) = + fun typedef_result nonempty context = Context.the_theory context - |> put_typedef newT oldT (full Abs_name) (full Rep_name) |> add_typedecls [(t, vs, mx)] |> Theory.add_consts_i ((if def then [(name, setT', NoSyn)] else []) @ @@ -165,6 +166,8 @@ |-> (fn (set_def, [type_definition]) => fn theory' => let fun make th = Drule.standard (th OF [type_definition]); + val abs_inject = make Abs_inject; + val abs_inverse = make Abs_inverse; val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, Rep_cases, Abs_cases, Rep_induct, Abs_induct], theory'') = theory' @@ -172,9 +175,9 @@ |> PureThy.add_thms ([((Rep_name, make Rep), []), ((Rep_name ^ "_inverse", make Rep_inverse), []), - ((Abs_name ^ "_inverse", make Abs_inverse), []), + ((Abs_name ^ "_inverse", abs_inverse), []), ((Rep_name ^ "_inject", make Rep_inject), []), - ((Abs_name ^ "_inject", make Abs_inject), []), + ((Abs_name ^ "_inject", abs_inject), []), ((Rep_name ^ "_cases", make Rep_cases), [RuleCases.case_names [Rep_name], InductAttrib.cases_set full_name]), ((Abs_name ^ "_cases", make Abs_cases), @@ -183,12 +186,14 @@ [RuleCases.case_names [Rep_name], InductAttrib.induct_set full_name]), ((Abs_name ^ "_induct", make Abs_induct), [RuleCases.case_names [Abs_name], InductAttrib.induct_type full_tname])]) - ||> Theory.parent_path; + ||> Theory.parent_path + ||> put_typedef newT oldT (full Abs_name) (full Rep_name) + set_def abs_inject abs_inverse val result = {type_definition = type_definition, set_def = set_def, Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; - in ((Context.Theory theory'', type_definition), result) end); + in ((type_definition, result), Context.Theory theory'') end); (* errors *) @@ -216,8 +221,9 @@ (*test theory errors now!*) val test_thy = Theory.copy thy; - val _ = (Context.Theory test_thy, - setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_result; + val _ = + Context.Theory test_thy + |> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal); in (cset, goal, goal_pat, typedef_result) end handle ERROR msg => err_in_typedef msg name; @@ -235,9 +241,12 @@ val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ..."); val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR msg => cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset)); - val (thy', result) = - (Context.Theory thy, non_empty) |> typedef_result |>> (Context.the_theory o fst); - in (thy', result) end; + in + Context.Theory thy + |> typedef_result non_empty + ||> Context.the_theory + |-> (fn (_, result) => pair result) + end; in @@ -255,7 +264,9 @@ let val (_, goal, goal_pat, att_result) = prepare_typedef prep_term def name typ set opt_morphs thy; - val att = #1 o att_result; + fun att (thy, th) = + let val ((th', _), thy') = att_result th thy + in (thy', th') end; in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([goal_pat], [])) thy end; in @@ -283,7 +294,7 @@ fun lookup f T = (case Symtab.lookup (TypedefData.get thy) (get_name T) of NONE => "" - | SOME s => f s); + | SOME (s, _) => f s); in (case strip_comb t of (Const (s, Type ("fun", [T, U])), ts) => @@ -304,7 +315,7 @@ fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) = (case Symtab.lookup (TypedefData.get thy) s of NONE => NONE - | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) => + | SOME ((newT as Type (tname, Us), oldT, Abs_name, Rep_name), _) => if is_some (Codegen.get_assoc_type thy tname) then NONE else let val module' = Codegen.if_library @@ -356,10 +367,47 @@ end) | typedef_tycodegen thy defs gr dep module brack _ = NONE; +fun typedef_type_extr thy tyco = + case Symtab.lookup (TypedefData.get thy) tyco + of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, inject, _)) => + let + val exists_thm = + UNIV_I + |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] [] + |> rewrite_rule [symmetric def]; + in case try (Tactic.rule_by_tactic ((ALLGOALS o resolve_tac) [exists_thm])) inject + of SOME eq_thm => SOME (((Term.typ_tfrees o Type.no_tvars) ty_abs, [(c_abs, [ty_rep])]), + (ALLGOALS o resolve_tac) [eq_reflection] + THEN (ALLGOALS o resolve_tac) [eq_thm]) + | NONE => NONE + end + | _ => NONE; + +fun typedef_fun_extr thy (c, ty) = + case (fst o strip_type) ty + of Type (tyco, _) :: _ => + (case Symtab.lookup (TypedefData.get thy) tyco + of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, _, inverse)) => + if c = c_rep then + let + val exists_thm = + UNIV_I + |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] [] + |> rewrite_rule [symmetric def] + in case try (Tactic.rule_by_tactic ((ALLGOALS o resolve_tac) [exists_thm])) inverse + of SOME eq_thm => SOME [eq_thm] + | NONE => NONE + end + else NONE + | _ => NONE) + | _ => NONE; + val setup = - TypedefData.init #> - Codegen.add_codegen "typedef" typedef_codegen #> - Codegen.add_tycodegen "typedef" typedef_tycodegen; + TypedefData.init + #> Codegen.add_codegen "typedef" typedef_codegen + #> Codegen.add_tycodegen "typedef" typedef_tycodegen + #> CodegenTheorems.add_fun_extr (these oo typedef_fun_extr) + #> CodegenTheorems.add_datatype_extr typedef_type_extr