only one theorem table for both code generators
authorhaftmann
Tue Oct 07 16:07:33 2008 +0200 (2008-10-07)
changeset 28522eacb54d9e78d
parent 28521 5b426c051e36
child 28523 5818d9cfb2e7
only one theorem table for both code generators
NEWS
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Tools/recfun_codegen.ML
     1.1 --- a/NEWS	Tue Oct 07 16:07:30 2008 +0200
     1.2 +++ b/NEWS	Tue Oct 07 16:07:33 2008 +0200
     1.3 @@ -91,6 +91,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Unified theorem tables of both code code generators.  Thus [code]
     1.8 +and [code func] behave identically.  INCOMPATIBILITY.
     1.9 +
    1.10 +* "undefined" replaces "arbitrary" in most occurences.
    1.11 +
    1.12  * Wrapper script for remote SystemOnTPTP service allows to use
    1.13  sledgehammer without local ATP installation (Vampire etc.).  See also
    1.14  ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
     2.1 --- a/src/HOL/Library/Efficient_Nat.thy	Tue Oct 07 16:07:30 2008 +0200
     2.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Oct 07 16:07:33 2008 +0200
     2.3 @@ -27,12 +27,12 @@
     2.4  
     2.5  code_datatype number_nat_inst.number_of_nat
     2.6  
     2.7 -lemma zero_nat_code [code, code unfold]:
     2.8 +lemma zero_nat_code [code, code inline]:
     2.9    "0 = (Numeral0 :: nat)"
    2.10    by simp
    2.11  lemmas [code post] = zero_nat_code [symmetric]
    2.12  
    2.13 -lemma one_nat_code [code, code unfold]:
    2.14 +lemma one_nat_code [code, code inline]:
    2.15    "1 = (Numeral1 :: nat)"
    2.16    by simp
    2.17  lemmas [code post] = one_nat_code [symmetric]
    2.18 @@ -59,9 +59,9 @@
    2.19  definition
    2.20    divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
    2.21  where
    2.22 -  [code func del]: "divmod_aux = divmod"
    2.23 +  [code del]: "divmod_aux = divmod"
    2.24  
    2.25 -lemma [code func]:
    2.26 +lemma [code]:
    2.27    "divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
    2.28    unfolding divmod_aux_def divmod_div_mod by simp
    2.29  
    2.30 @@ -92,7 +92,7 @@
    2.31    expression:
    2.32  *}
    2.33  
    2.34 -lemma [code func, code unfold]:
    2.35 +lemma [code, code unfold]:
    2.36    "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
    2.37    by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
    2.38  
    2.39 @@ -221,8 +221,7 @@
    2.40  
    2.41  fun lift f thy eqns1 =
    2.42    let
    2.43 -    val eqns2 = ((map o apfst) (AxClass.overload thy)
    2.44 -      o burrow_fst Drule.zero_var_indexes_list) eqns1;
    2.45 +    val eqns2 = burrow_fst Drule.zero_var_indexes_list eqns1;
    2.46      val thms3 = try (map fst
    2.47        #> map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
    2.48        #> f thy
    2.49 @@ -232,7 +231,8 @@
    2.50    in case thms4
    2.51     of NONE => NONE
    2.52      | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
    2.53 -        then NONE else SOME (map (Code_Unit.mk_eqn thy) thms4)
    2.54 +        then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
    2.55 +          (*FIXME*)
    2.56    end
    2.57  
    2.58  in
    2.59 @@ -423,7 +423,8 @@
    2.60    (Haskell infix 4 "<")
    2.61  
    2.62  consts_code
    2.63 -  0                            ("0")
    2.64 +  "0::nat"                     ("0")
    2.65 +  "1::nat"                     ("1")
    2.66    Suc                          ("(_ +/ 1)")
    2.67    "op + \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ +/ _)")
    2.68    "op * \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ */ _)")
     3.1 --- a/src/HOL/Library/Executable_Set.thy	Tue Oct 07 16:07:30 2008 +0200
     3.2 +++ b/src/HOL/Library/Executable_Set.thy	Tue Oct 07 16:07:33 2008 +0200
     3.3 @@ -11,11 +11,22 @@
     3.4  
     3.5  subsection {* Definitional rewrites *}
     3.6  
     3.7 -lemma [code target: Set]:
     3.8 -  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
     3.9 -  by blast
    3.10 +definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    3.11 +  "subset = op \<le>"
    3.12 +
    3.13 +declare subset_def [symmetric, code unfold]
    3.14 +
    3.15 +lemma "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    3.16 +  unfolding subset_def subset_eq ..
    3.17  
    3.18 -declare subset_eq [code]
    3.19 +definition is_empty :: "'a set \<Rightarrow> bool" where
    3.20 +  "is_empty A \<longleftrightarrow> A = {}"
    3.21 +
    3.22 +definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    3.23 +  [code del]: "eq_set = op ="
    3.24 +
    3.25 +lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    3.26 +  unfolding eq_set_def by auto
    3.27  
    3.28  lemma [code]:
    3.29    "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
    3.30 @@ -247,6 +258,7 @@
    3.31  consts_code
    3.32    "{}" ("{*[]*}")
    3.33    insert ("{*insertl*}")
    3.34 +  is_empty ("{*null*}")
    3.35    "op \<union>" ("{*unionl*}")
    3.36    "op \<inter>" ("{*intersect*}")
    3.37    "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
     4.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Oct 07 16:07:30 2008 +0200
     4.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Oct 07 16:07:33 2008 +0200
     4.3 @@ -18,57 +18,73 @@
     4.4  
     4.5  open Codegen;
     4.6  
     4.7 -structure RecCodegenData = TheoryDataFun
     4.8 +structure ModuleData = TheoryDataFun
     4.9  (
    4.10 -  type T = (thm * string option) list Symtab.table;
    4.11 +  type T = string Symtab.table;
    4.12    val empty = Symtab.empty;
    4.13    val copy = I;
    4.14    val extend = I;
    4.15 -  fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst);
    4.16 +  fun merge _ = Symtab.merge (K true);
    4.17  );
    4.18  
    4.19 -val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
    4.20 -val lhs_of = fst o dest_eqn o prop_of;
    4.21 -val const_of = dest_Const o head_of o fst o dest_eqn;
    4.22 -
    4.23 -fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
    4.24 -  Display.string_of_thm thm);
    4.25 -
    4.26 -fun add_thm opt_module thm =
    4.27 -  (if Pattern.pattern (lhs_of thm) then
    4.28 -    RecCodegenData.map
    4.29 -      (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module)))
    4.30 -  else tap (fn _ => warn thm))
    4.31 -  handle TERM _ => tap (fn _ => warn thm);
    4.32 +fun add_thm add NONE thm thy = add thm thy
    4.33 +  | add_thm add (SOME module_name) thm thy =
    4.34 +      case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm
    4.35 +       of SOME (thm', _) => let val c = Code_Unit.const_eqn thm'
    4.36 +            in thy
    4.37 +              |> ModuleData.map (Symtab.update (c, module_name))
    4.38 +              |> add thm'
    4.39 +            end
    4.40 +        | NONE => add thm thy;
    4.41  
    4.42  fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
    4.43 -  (add_thm opt_module thm #> Code.add_liberal_eqn thm) I);
    4.44 +  (add_thm Code.add_eqn opt_module thm) I);
    4.45  
    4.46  val add_default = Thm.declaration_attribute (fn thm => Context.mapping
    4.47 -  (add_thm NONE thm #> Code.add_default_eqn thm) I);
    4.48 +  (add_thm Code.add_default_eqn NONE thm) I);
    4.49 +
    4.50 +val del = Thm.declaration_attribute (fn thm => Context.mapping
    4.51 +  (Code.del_eqn thm) I);
    4.52  
    4.53 -fun del_thm thm = case try const_of (prop_of thm)
    4.54 - of SOME (s, _) => RecCodegenData.map
    4.55 -      (Symtab.map_entry s (remove (Thm.eq_thm o apsnd fst) thm))
    4.56 -  | NONE => tap (fn _ => warn thm);
    4.57 +fun meta_eq_to_obj_eq thy thm =
    4.58 +  let
    4.59 +    val T = (fastype_of o fst o Logic.dest_equals o Thm.prop_of) thm;
    4.60 +  in if Sign.of_sort thy (T, @{sort type})
    4.61 +    then SOME (Conv.fconv_rule Drule.beta_eta_conversion (@{thm meta_eq_to_obj_eq} OF [thm]))
    4.62 +    else NONE
    4.63 +  end;
    4.64  
    4.65 -val del = Thm.declaration_attribute
    4.66 -  (fn thm => Context.mapping (del_thm thm #> Code.del_eqn thm) I)
    4.67 +fun expand_eta thy [] = []
    4.68 +  | expand_eta thy (thms as thm :: _) =
    4.69 +      let
    4.70 +        val (_, ty) = Code_Unit.const_typ_eqn thm;
    4.71 +      in if (null o Term.typ_tvars) ty orelse (null o fst o strip_type) ty
    4.72 +        then thms
    4.73 +        else map (Code_Unit.expand_eta thy 1) thms
    4.74 +      end;
    4.75  
    4.76 -fun del_redundant thy eqs [] = eqs
    4.77 -  | del_redundant thy eqs (eq :: eqs') =
    4.78 -    let
    4.79 -      val matches = curry
    4.80 -        (Pattern.matches thy o pairself (lhs_of o fst))
    4.81 -    in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
    4.82 +fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else
    4.83 +  let
    4.84 +    val c' = AxClass.unoverload_const thy (c, T);
    4.85 +    val opt_name = Symtab.lookup (ModuleData.get thy) c';
    4.86 +    val thms = Code.these_raw_eqns thy c'
    4.87 +      |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    4.88 +      |> expand_eta thy
    4.89 +      |> map (AxClass.overload thy)
    4.90 +      |> map_filter (meta_eq_to_obj_eq thy)
    4.91 +      |> Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var
    4.92 +      |> map (rpair opt_name)
    4.93 +  in if null thms then NONE else SOME thms end;
    4.94 +
    4.95 +val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
    4.96 +val const_of = dest_Const o head_of o fst o dest_eqn;
    4.97  
    4.98  fun get_equations thy defs (s, T) =
    4.99 -  (case Symtab.lookup (RecCodegenData.get thy) s of
   4.100 +  (case retrieve_equations thy (s, T) of
   4.101       NONE => ([], "")
   4.102     | SOME thms => 
   4.103 -       let val thms' = del_redundant thy []
   4.104 -         (filter (fn (thm, _) => is_instance T
   4.105 -           (snd (const_of (prop_of thm)))) thms)
   4.106 +       let val thms' = filter (fn (thm, _) => is_instance T
   4.107 +           (snd (const_of (prop_of thm)))) thms
   4.108         in if null thms' then ([], "")
   4.109           else (preprocess thy (map fst thms'),
   4.110             case snd (snd (split_last thms')) of
   4.111 @@ -166,7 +182,6 @@
   4.112          end)
   4.113    | _ => NONE);
   4.114  
   4.115 -
   4.116  val setup =
   4.117    add_codegen "recfun" recfun_codegen
   4.118    #> Code.add_attribute ("", Args.del |-- Scan.succeed del