# HG changeset patch # User huffman # Date 1267569676 28800 # Node ID 0e2ef13796a475188f64a6072c9f8166c9edf7a9 # Parent 59550ec4921d21f65add0ec449904596c1cd5eb2 add_axioms no longer needs a definitional mode diff -r 59550ec4921d -r 0e2ef13796a4 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 14:35:09 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Mar 02 14:41:16 2010 -0800 @@ -10,12 +10,10 @@ string Symtab.table -> (int -> term) -> Datatype.dtyp -> term val calc_axioms : - bool -> Domain_Library.eq list -> int -> Domain_Library.eq -> string * (string * term) list val add_axioms : - bool -> ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list -> Domain_Library.eq list -> theory -> theory @@ -49,15 +47,11 @@ | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); fun calc_axioms - (definitional : bool) (eqs : eq list) (n : int) (eqn as ((dname,_),cons) : eq) : string * (string * term) list = let - -(* ----- axioms and definitions concerning the isomorphism ------------------ *) - val dc_abs = %%:(dname^"_abs"); val dc_rep = %%:(dname^"_rep"); val x_name'= "x"; @@ -66,10 +60,9 @@ val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); - in - (dnam, if definitional then [] else [abs_iso_ax, rep_iso_ax]) - end; (* let (calc_axioms) *) + (dnam, [abs_iso_ax, rep_iso_ax]) + end; (* legacy type inference *) @@ -85,7 +78,7 @@ fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x); fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; -fun add_axioms definitional eqs' (eqs : eq list) thy' = +fun add_axioms eqs' (eqs : eq list) thy' = let val dnames = map (fst o fst) eqs; val x_name = idx_name dnames "x"; @@ -95,7 +88,7 @@ #> add_axioms_infer axs #> Sign.parent_path; - val axs = mapn (calc_axioms definitional eqs) 0 eqs; + val axs = mapn (calc_axioms eqs) 0 eqs; val thy = thy' |> fold add_one axs; fun get_iso_info ((dname, tyvars), cons') = @@ -121,10 +114,9 @@ } end; val dom_binds = map (Binding.name o Long_Name.base_name) dnames; - val thy = - if definitional then thy - else snd (Domain_Take_Proofs.define_take_functions - (dom_binds ~~ map get_iso_info eqs') thy); + val (take_info, thy) = + Domain_Take_Proofs.define_take_functions + (dom_binds ~~ map get_iso_info eqs') thy; (* declare lub_take axioms *) local @@ -141,9 +133,7 @@ add_one (dnam, [("lub_take", ax)]) end in - val thy = - if definitional then thy - else fold ax_lub_take dnames thy + val thy = fold ax_lub_take dnames thy end; in thy diff -r 59550ec4921d -r 0e2ef13796a4 src/HOLCF/Tools/Domain/domain_extender.ML --- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 14:35:09 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Mar 02 14:41:16 2010 -0800 @@ -164,7 +164,7 @@ ) : cons; val eqs : eq list = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; - val thy = thy |> Domain_Axioms.add_axioms false eqs' eqs; + val thy = Domain_Axioms.add_axioms eqs' eqs thy; val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn (eq, (x,cs)) => @@ -237,7 +237,6 @@ ) : cons; val eqs : eq list = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs'; - val thy = thy |> Domain_Axioms.add_axioms true eqs' eqs; val ((rewss, take_rews), theorems_thy) = thy |> fold_map (fn (eq, (x,cs)) =>