# HG changeset patch # User haftmann # Date 1223388453 -7200 # Node ID eacb54d9e78d1d5af9dc13c96faf0faa8ddfd26e # Parent 5b426c051e36b5330add704f1ef6c96652b7652b only one theorem table for both code generators diff -r 5b426c051e36 -r eacb54d9e78d NEWS --- a/NEWS Tue Oct 07 16:07:30 2008 +0200 +++ b/NEWS Tue Oct 07 16:07:33 2008 +0200 @@ -91,6 +91,11 @@ *** HOL *** +* Unified theorem tables of both code code generators. Thus [code] +and [code func] behave identically. INCOMPATIBILITY. + +* "undefined" replaces "arbitrary" in most occurences. + * Wrapper script for remote SystemOnTPTP service allows to use sledgehammer without local ATP installation (Vampire etc.). See also ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting diff -r 5b426c051e36 -r eacb54d9e78d src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Tue Oct 07 16:07:30 2008 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Oct 07 16:07:33 2008 +0200 @@ -27,12 +27,12 @@ code_datatype number_nat_inst.number_of_nat -lemma zero_nat_code [code, code unfold]: +lemma zero_nat_code [code, code inline]: "0 = (Numeral0 :: nat)" by simp lemmas [code post] = zero_nat_code [symmetric] -lemma one_nat_code [code, code unfold]: +lemma one_nat_code [code, code inline]: "1 = (Numeral1 :: nat)" by simp lemmas [code post] = one_nat_code [symmetric] @@ -59,9 +59,9 @@ definition divmod_aux :: "nat \ nat \ nat \ nat" where - [code func del]: "divmod_aux = divmod" + [code del]: "divmod_aux = divmod" -lemma [code func]: +lemma [code]: "divmod n m = (if m = 0 then (0, n) else divmod_aux n m)" unfolding divmod_aux_def divmod_div_mod by simp @@ -92,7 +92,7 @@ expression: *} -lemma [code func, code unfold]: +lemma [code, code unfold]: "nat_case = (\f g n. if n = 0 then f else g (n - 1))" by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc) @@ -221,8 +221,7 @@ fun lift f thy eqns1 = let - val eqns2 = ((map o apfst) (AxClass.overload thy) - o burrow_fst Drule.zero_var_indexes_list) eqns1; + val eqns2 = burrow_fst Drule.zero_var_indexes_list eqns1; val thms3 = try (map fst #> map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) #> f thy @@ -232,7 +231,8 @@ in case thms4 of NONE => NONE | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4) - then NONE else SOME (map (Code_Unit.mk_eqn thy) thms4) + then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4) + (*FIXME*) end in @@ -423,7 +423,8 @@ (Haskell infix 4 "<") consts_code - 0 ("0") + "0::nat" ("0") + "1::nat" ("1") Suc ("(_ +/ 1)") "op + \ nat \ nat \ nat" ("(_ +/ _)") "op * \ nat \ nat \ nat" ("(_ */ _)") diff -r 5b426c051e36 -r eacb54d9e78d src/HOL/Library/Executable_Set.thy --- a/src/HOL/Library/Executable_Set.thy Tue Oct 07 16:07:30 2008 +0200 +++ b/src/HOL/Library/Executable_Set.thy Tue Oct 07 16:07:33 2008 +0200 @@ -11,11 +11,22 @@ subsection {* Definitional rewrites *} -lemma [code target: Set]: - "A = B \ A \ B \ B \ A" - by blast +definition subset :: "'a set \ 'a set \ bool" where + "subset = op \" + +declare subset_def [symmetric, code unfold] + +lemma "subset A B \ (\x\A. x \ B)" + unfolding subset_def subset_eq .. -declare subset_eq [code] +definition is_empty :: "'a set \ bool" where + "is_empty A \ A = {}" + +definition eq_set :: "'a set \ 'a set \ bool" where + [code del]: "eq_set = op =" + +lemma [code]: "eq_set A B \ A \ B \ B \ A" + unfolding eq_set_def by auto lemma [code]: "a \ A \ (\x\A. x = a)" @@ -247,6 +258,7 @@ consts_code "{}" ("{*[]*}") insert ("{*insertl*}") + is_empty ("{*null*}") "op \" ("{*unionl*}") "op \" ("{*intersect*}") "op - \ 'a set \ 'a set \ 'a set" ("{* flip subtract *}") diff -r 5b426c051e36 -r eacb54d9e78d src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Tue Oct 07 16:07:30 2008 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Tue Oct 07 16:07:33 2008 +0200 @@ -18,57 +18,73 @@ open Codegen; -structure RecCodegenData = TheoryDataFun +structure ModuleData = TheoryDataFun ( - type T = (thm * string option) list Symtab.table; + type T = string Symtab.table; val empty = Symtab.empty; val copy = I; val extend = I; - fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst); + fun merge _ = Symtab.merge (K true); ); -val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; -val lhs_of = fst o dest_eqn o prop_of; -val const_of = dest_Const o head_of o fst o dest_eqn; - -fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^ - Display.string_of_thm thm); - -fun add_thm opt_module thm = - (if Pattern.pattern (lhs_of thm) then - RecCodegenData.map - (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module))) - else tap (fn _ => warn thm)) - handle TERM _ => tap (fn _ => warn thm); +fun add_thm add NONE thm thy = add thm thy + | add_thm add (SOME module_name) thm thy = + case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm + of SOME (thm', _) => let val c = Code_Unit.const_eqn thm' + in thy + |> ModuleData.map (Symtab.update (c, module_name)) + |> add thm' + end + | NONE => add thm thy; fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping - (add_thm opt_module thm #> Code.add_liberal_eqn thm) I); + (add_thm Code.add_eqn opt_module thm) I); val add_default = Thm.declaration_attribute (fn thm => Context.mapping - (add_thm NONE thm #> Code.add_default_eqn thm) I); + (add_thm Code.add_default_eqn NONE thm) I); + +val del = Thm.declaration_attribute (fn thm => Context.mapping + (Code.del_eqn thm) I); -fun del_thm thm = case try const_of (prop_of thm) - of SOME (s, _) => RecCodegenData.map - (Symtab.map_entry s (remove (Thm.eq_thm o apsnd fst) thm)) - | NONE => tap (fn _ => warn thm); +fun meta_eq_to_obj_eq thy thm = + let + val T = (fastype_of o fst o Logic.dest_equals o Thm.prop_of) thm; + in if Sign.of_sort thy (T, @{sort type}) + then SOME (Conv.fconv_rule Drule.beta_eta_conversion (@{thm meta_eq_to_obj_eq} OF [thm])) + else NONE + end; -val del = Thm.declaration_attribute - (fn thm => Context.mapping (del_thm thm #> Code.del_eqn thm) I) +fun expand_eta thy [] = [] + | expand_eta thy (thms as thm :: _) = + let + val (_, ty) = Code_Unit.const_typ_eqn thm; + in if (null o Term.typ_tvars) ty orelse (null o fst o strip_type) ty + then thms + else map (Code_Unit.expand_eta thy 1) thms + end; -fun del_redundant thy eqs [] = eqs - | del_redundant thy eqs (eq :: eqs') = - let - val matches = curry - (Pattern.matches thy o pairself (lhs_of o fst)) - in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end; +fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else + let + val c' = AxClass.unoverload_const thy (c, T); + val opt_name = Symtab.lookup (ModuleData.get thy) c'; + val thms = Code.these_raw_eqns thy c' + |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) + |> expand_eta thy + |> map (AxClass.overload thy) + |> map_filter (meta_eq_to_obj_eq thy) + |> Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var + |> map (rpair opt_name) + in if null thms then NONE else SOME thms end; + +val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; +val const_of = dest_Const o head_of o fst o dest_eqn; fun get_equations thy defs (s, T) = - (case Symtab.lookup (RecCodegenData.get thy) s of + (case retrieve_equations thy (s, T) of NONE => ([], "") | SOME thms => - let val thms' = del_redundant thy [] - (filter (fn (thm, _) => is_instance T - (snd (const_of (prop_of thm)))) thms) + let val thms' = filter (fn (thm, _) => is_instance T + (snd (const_of (prop_of thm)))) thms in if null thms' then ([], "") else (preprocess thy (map fst thms'), case snd (snd (split_last thms')) of @@ -166,7 +182,6 @@ end) | _ => NONE); - val setup = add_codegen "recfun" recfun_codegen #> Code.add_attribute ("", Args.del |-- Scan.succeed del