--- a/src/HOL/Code_Generator.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Code_Generator.thy Fri Apr 20 11:21:42 2007 +0200
@@ -219,7 +219,7 @@
definition
if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
- "if_delayed b f g = (if b then f True else g False)"
+ [code nofunc]: "if_delayed b f g = (if b then f True else g False)"
lemma [code func]:
shows "if_delayed True f g = f True"
@@ -230,7 +230,6 @@
"(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
unfolding if_delayed_def ..
-
hide (open) const if_delayed
end
--- a/src/HOL/Datatype.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Datatype.thy Fri Apr 20 11:21:42 2007 +0200
@@ -102,7 +102,7 @@
(** apfst -- can be used in similar type definitions **)
-lemma apfst_conv [simp]: "apfst f (a,b) = (f(a),b)"
+lemma apfst_conv [simp, code func]: "apfst f (a, b) = (f a, b)"
by (simp add: apfst_def)
@@ -697,10 +697,10 @@
option_map :: "('a => 'b) => ('a option => 'b option)"
"option_map == %f y. case y of None => None | Some x => Some (f x)"
-lemma option_map_None [simp]: "option_map f None = None"
+lemma option_map_None [simp, code func]: "option_map f None = None"
by (simp add: option_map_def)
-lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
+lemma option_map_Some [simp, code func]: "option_map f (Some x) = Some (f x)"
by (simp add: option_map_def)
lemma option_map_is_None [iff]:
--- a/src/HOL/Divides.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Divides.thy Fri Apr 20 11:21:42 2007 +0200
@@ -871,9 +871,9 @@
done
-subsection {* Code generation for div and mod *}
+subsection {* Code generation for div, mod and dvd on nat *}
-definition
+definition [code nofunc]:
"divmod (m\<Colon>nat) n = (m div n, m mod n)"
lemma divmod_zero [code]: "divmod m 0 = (0, m)"
@@ -893,13 +893,22 @@
lemma mod_divmod [code]: "m mod n = snd (divmod m n)"
unfolding divmod_def by simp
+definition
+ dvd_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
+where
+ "dvd_nat m n \<longleftrightarrow> n mod m = (0 \<Colon> nat)"
+
+lemma [code inline]:
+ "op dvd = dvd_nat"
+ by (auto simp add: dvd_nat_def dvd_eq_mod_eq_0 expand_fun_eq)
+
code_modulename SML
Divides Integer
code_modulename OCaml
Divides Integer
-hide (open) const divmod
+hide (open) const divmod dvd_nat
subsection {* Legacy bindings *}
--- a/src/HOL/FixedPoint.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/FixedPoint.thy Fri Apr 20 11:21:42 2007 +0200
@@ -198,6 +198,8 @@
apply (iprover elim: le_funE)
done
+lemmas [code nofunc] = Inf_fun_def
+
theorem Sup_fun_eq: "Sup A = (\<lambda>x. Sup {y. \<exists>f\<in>A. y = f x})"
apply (rule order_antisym)
apply (rule Sup_least)
@@ -219,6 +221,8 @@
Inf_set_def: "Inf S \<equiv> \<Inter>S"
by intro_classes (auto simp add: Inf_set_def)
+lemmas [code nofunc] = Inf_set_def
+
theorem Sup_set_eq: "Sup S = \<Union>S"
apply (rule subset_antisym)
apply (rule Sup_least)
--- a/src/HOL/Fun.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Fun.thy Fri Apr 20 11:21:42 2007 +0200
@@ -12,7 +12,7 @@
constdefs
fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
- "fun_upd f a b == % x. if x=a then b else f x"
+ [code func]: "fun_upd f a b == % x. if x=a then b else f x"
nonterminals
updbinds updbind
@@ -34,15 +34,20 @@
"fun_sum" == sum_case
*)
-constdefs
- override_on :: "('a => 'b) => ('a => 'b) => 'a set => ('a => 'b)"
- "override_on f g A == %a. if a : A then g a else f a"
+definition
+ override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+ "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
- id :: "'a => 'a"
- "id == %x. x"
+definition
+ id :: "'a \<Rightarrow> 'a"
+where
+ "id = (\<lambda>x. x)"
- comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "o" 55)
- "f o g == %x. f(g(x))"
+definition
+ comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55)
+where
+ "f o g = (\<lambda>x. f (g x))"
notation (xsymbols)
comp (infixl "\<circ>" 55)
@@ -404,9 +409,10 @@
subsection{* swap *}
-constdefs
- swap :: "['a, 'a, 'a => 'b] => ('a => 'b)"
- "swap a b f == f(a := f b, b:= f a)"
+definition
+ swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
+where
+ "swap a b f = f (a := f b, b:= f a)"
lemma swap_self: "swap a a f = f"
by (simp add: swap_def)
@@ -418,7 +424,7 @@
by (rule ext, simp add: fun_upd_def swap_def)
lemma inj_on_imp_inj_on_swap:
- "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
+ "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
by (simp add: inj_on_def swap_def, blast)
lemma inj_on_swap_iff [simp]:
@@ -460,6 +466,8 @@
le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
+lemmas [code nofunc] = le_fun_def less_fun_def
+
instance "fun" :: (type, preorder) preorder
by default (auto simp add: le_fun_def less_fun_def intro: order_trans)
@@ -528,6 +536,8 @@
apply (auto dest: le_funD)
done
+lemmas [code nofunc] = inf_fun_eq sup_fun_eq
+
instance "fun" :: (type, distrib_lattice) distrib_lattice
by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
--- a/src/HOL/HOL.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/HOL.thy Fri Apr 20 11:21:42 2007 +0200
@@ -165,7 +165,7 @@
True_or_False: "(P=True) | (P=False)"
defs
- Let_def: "Let s f == f(s)"
+ Let_def [code func]: "Let s f == f(s)"
if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
finalconsts
@@ -177,7 +177,7 @@
axiomatization
undefined :: 'a
-axioms
+axiomatization where
undefined_fun: "undefined x = undefined"
@@ -912,8 +912,8 @@
structure Blast = BlastFun(
struct
type claset = Classical.claset
- val equality_name = "op ="
- val not_name = "Not"
+ val equality_name = @{const_name "op ="}
+ val not_name = @{const_name "Not"}
val notE = @{thm HOL.notE}
val ccontr = @{thm HOL.ccontr}
val contr_tac = Classical.contr_tac
--- a/src/HOL/Integ/IntDef.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Integ/IntDef.thy Fri Apr 20 11:21:42 2007 +0200
@@ -517,15 +517,16 @@
subsection{*The Constants @{term neg} and @{term iszero}*}
-constdefs
-
- neg :: "'a::ordered_idom => bool"
- "neg(Z) == Z < 0"
+definition
+ neg :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
+where
+ "neg Z \<longleftrightarrow> Z < 0"
+definition
(*For simplifying equalities*)
- iszero :: "'a::comm_semiring_1_cancel => bool"
- "iszero z == z = (0)"
-
+ iszero :: "'a\<Colon>comm_semiring_1_cancel \<Rightarrow> bool"
+where
+ "iszero z \<longleftrightarrow> z = 0"
lemma not_neg_int [simp]: "~ neg(int n)"
by (simp add: neg_def)
--- a/src/HOL/Integ/IntDiv.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Integ/IntDiv.thy Fri Apr 20 11:21:42 2007 +0200
@@ -18,13 +18,13 @@
constdefs
quorem :: "(int*int) * (int*int) => bool"
--{*definition of quotient and remainder*}
- "quorem == %((a,b), (q,r)).
+ [code func]: "quorem == %((a,b), (q,r)).
a = b*q + r &
(if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
adjust :: "[int, int*int] => int*int"
--{*for the division algorithm*}
- "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
+ [code func]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
else (2*q, r)"
text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
@@ -44,13 +44,13 @@
text{*algorithm for the general case @{term "b\<noteq>0"}*}
constdefs
negateSnd :: "int*int => int*int"
- "negateSnd == %(q,r). (q,-r)"
+ [code func]: "negateSnd == %(q,r). (q,-r)"
divAlg :: "int*int => int*int"
--{*The full division algorithm considers all possible signs for a, b
including the special case @{text "a=0, b<0"} because
@{term negDivAlg} requires @{term "a<0"}.*}
- "divAlg ==
+ [code func]: "divAlg ==
%(a,b). if 0\<le>a then
if 0\<le>b then posDivAlg (a,b)
else if a=0 then (0,0)
@@ -65,8 +65,8 @@
text{*The operators are defined with reference to the algorithm, which is
proved to satisfy the specification.*}
defs
- div_def: "a div b == fst (divAlg (a,b))"
- mod_def: "a mod b == snd (divAlg (a,b))"
+ div_def [code func]: "a div b == fst (divAlg (a,b))"
+ mod_def [code func]: "a mod b == snd (divAlg (a,b))"
text{*
--- a/src/HOL/Integ/Numeral.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Integ/Numeral.thy Fri Apr 20 11:21:42 2007 +0200
@@ -32,15 +32,15 @@
definition
Pls :: int where
- "Pls = 0"
+ [code nofunc]:"Pls = 0"
definition
Min :: int where
- "Min = - 1"
+ [code nofunc]:"Min = - 1"
definition
Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
- "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+ [code nofunc]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
class number = type + -- {* for numeric types: nat, int, real, \dots *}
fixes number_of :: "int \<Rightarrow> 'a"
@@ -68,11 +68,11 @@
definition
succ :: "int \<Rightarrow> int" where
- "succ k = k + 1"
+ [code nofunc]: "succ k = k + 1"
definition
pred :: "int \<Rightarrow> int" where
- "pred k = k - 1"
+ [code nofunc]: "pred k = k - 1"
declare
max_def[of "number_of u" "number_of v", standard, simp]
--- a/src/HOL/Integ/Presburger.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Integ/Presburger.thy Fri Apr 20 11:21:42 2007 +0200
@@ -1069,11 +1069,12 @@
lemma eq_number_of [code func]:
"((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
unfolding number_of_is_id ..
+
lemma eq_Pls_Pls:
- "Numeral.Pls = Numeral.Pls" ..
+ "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
lemma eq_Pls_Min:
- "Numeral.Pls \<noteq> Numeral.Min"
+ "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
unfolding Pls_def Min_def by auto
lemma eq_Pls_Bit0:
@@ -1081,18 +1082,18 @@
unfolding Pls_def Bit_def bit.cases by auto
lemma eq_Pls_Bit1:
- "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
+ "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
unfolding Pls_def Bit_def bit.cases by arith
lemma eq_Min_Pls:
- "Numeral.Min \<noteq> Numeral.Pls"
+ "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
unfolding Pls_def Min_def by auto
lemma eq_Min_Min:
- "Numeral.Min = Numeral.Min" ..
+ "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
lemma eq_Min_Bit0:
- "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
+ "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
unfolding Min_def Bit_def bit.cases by arith
lemma eq_Min_Bit1:
@@ -1104,11 +1105,11 @@
unfolding Pls_def Bit_def bit.cases by auto
lemma eq_Bit1_Pls:
- "Numeral.Bit k bit.B1 \<noteq> Numeral.Pls"
+ "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
unfolding Pls_def Bit_def bit.cases by arith
lemma eq_Bit0_Min:
- "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
+ "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
unfolding Min_def Bit_def bit.cases by arith
lemma eq_Bit1_Min:
@@ -1140,10 +1141,10 @@
unfolding number_of_is_id ..
lemma less_eq_Pls_Pls:
- "Numeral.Pls \<le> Numeral.Pls" ..
+ "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
lemma less_eq_Pls_Min:
- "\<not> (Numeral.Pls \<le> Numeral.Min)"
+ "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
unfolding Pls_def Min_def by auto
lemma less_eq_Pls_Bit:
@@ -1151,11 +1152,11 @@
unfolding Pls_def Bit_def by (cases v) auto
lemma less_eq_Min_Pls:
- "Numeral.Min \<le> Numeral.Pls"
+ "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
unfolding Pls_def Min_def by auto
lemma less_eq_Min_Min:
- "Numeral.Min \<le> Numeral.Min" ..
+ "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
lemma less_eq_Min_Bit0:
"Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
@@ -1198,10 +1199,10 @@
unfolding number_of_is_id ..
lemma less_Pls_Pls:
- "\<not> (Numeral.Pls < Numeral.Pls)" by auto
+ "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
lemma less_Pls_Min:
- "\<not> (Numeral.Pls < Numeral.Min)"
+ "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
unfolding Pls_def Min_def by auto
lemma less_Pls_Bit0:
@@ -1213,11 +1214,11 @@
unfolding Pls_def Bit_def by auto
lemma less_Min_Pls:
- "Numeral.Min < Numeral.Pls"
+ "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
unfolding Pls_def Min_def by auto
lemma less_Min_Min:
- "\<not> (Numeral.Min < Numeral.Min)" by auto
+ "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
lemma less_Min_Bit:
"Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
--- a/src/HOL/Library/ExecutableSet.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/ExecutableSet.thy Fri Apr 20 11:21:42 2007 +0200
@@ -287,6 +287,12 @@
"image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
lemma [code func]:
+ "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
+
+lemma [code func]:
+ "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
+
+lemma [code func]:
"UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
lemma [code func]:
@@ -301,6 +307,7 @@
lemma [code func]:
"filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
+
code_abstype "'a set" "'a list" where
"{}" \<equiv> empty_list
insert \<equiv> insertl
--- a/src/HOL/Library/Graphs.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/Graphs.thy Fri Apr 20 11:21:42 2007 +0200
@@ -73,13 +73,14 @@
by auto
qed
+lemmas [code nofunc] = graph_plus_def
instance graph :: (type, type) "{distrib_lattice, complete_lattice}"
graph_leq_def: "G \<le> H \<equiv> dest_graph G \<subseteq> dest_graph H"
graph_less_def: "G < H \<equiv> dest_graph G \<subset> dest_graph H"
"inf G H \<equiv> Graph (dest_graph G \<inter> dest_graph H)"
"sup G H \<equiv> G + H"
- Inf_graph_def: "Inf == \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
+ Inf_graph_def: "Inf \<equiv> \<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs))"
proof
fix x y z :: "('a,'b) graph"
fix A :: "('a, 'b) graph set"
@@ -122,6 +123,9 @@
unfolding Inf_graph_def graph_leq_def by auto }
qed
+lemmas [code nofunc] = graph_leq_def graph_less_def
+ inf_graph_def sup_graph_def Inf_graph_def
+
lemma in_grplus:
"has_edge (G + H) p b q = (has_edge G p b q \<or> has_edge H p b q)"
by (cases G, cases H, auto simp:has_edge_def graph_plus_def)
@@ -146,6 +150,8 @@
by (cases a) (simp add:grcomp.simps)
qed
+lemmas [code nofunc] = graph_mult_def
+
instance graph :: (type, one) one
graph_one_def: "1 == Graph { (x, 1, x) |x. True}" ..
--- a/src/HOL/Library/List_lexord.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/List_lexord.thy Fri Apr 20 11:21:42 2007 +0200
@@ -13,7 +13,7 @@
list_le_def: "(xs::('a::ord) list) \<le> ys \<equiv> (xs < ys \<or> xs = ys)"
list_less_def: "(xs::('a::ord) list) < ys \<equiv> (xs, ys) \<in> lexord {(u,v). u < v}" ..
-lemmas list_ord_defs = list_less_def list_le_def
+lemmas list_ord_defs [code nofunc] = list_less_def list_le_def
instance list :: (order) order
apply (intro_classes, unfold list_ord_defs)
@@ -40,6 +40,8 @@
by intro_classes
(auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
+lemmas [code nofunc] = inf_list_def sup_list_def
+
lemma not_less_Nil [simp]: "\<not> (x < [])"
by (unfold list_less_def) simp
--- a/src/HOL/Library/Product_ord.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/Product_ord.thy Fri Apr 20 11:21:42 2007 +0200
@@ -13,7 +13,7 @@
prod_le_def: "(x \<le> y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x \<le> snd y)"
prod_less_def: "(x < y) \<equiv> (fst x < fst y) \<or> (fst x = fst y \<and> snd x < snd y)" ..
-lemmas prod_ord_defs = prod_less_def prod_le_def
+lemmas prod_ord_defs [code nofunc] = prod_less_def prod_le_def
lemma [code func]:
"(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
--- a/src/HOL/Library/SCT_Definition.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/SCT_Definition.thy Fri Apr 20 11:21:42 2007 +0200
@@ -15,12 +15,11 @@
LESS ("\<down>")
| LEQ ("\<Down>")
-instance sedge :: times ..
-instance sedge :: one ..
+instance sedge :: one
+ one_sedge_def: "1 \<equiv> \<Down>" ..
-defs (overloaded)
- one_sedge_def: "1 == \<Down>"
- mult_sedge_def:" a * b == (if a = \<down> then \<down> else b)"
+instance sedge :: times
+ mult_sedge_def:" a * b \<equiv> if a = \<down> then \<down> else b" ..
instance sedge :: comm_monoid_mult
proof
@@ -31,14 +30,18 @@
by (cases a, simp) (cases b, auto)
qed
+lemma sedge_UNIV:
+ "UNIV = { LESS, LEQ }"
+ by auto (case_tac x, auto) (*FIXME*)
+
instance sedge :: finite
proof
- have a: "UNIV = { LESS, LEQ }"
- by auto (case_tac x, auto) (* FIXME *)
show "finite (UNIV::sedge set)"
- by (simp add:a)
+ by (simp add: sedge_UNIV)
qed
+lemmas [code func] = sedge_UNIV
+
types scg = "(nat, sedge) graph"
types acg = "(nat, scg) graph"
--- a/src/HOL/Library/SCT_Implementation.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Library/SCT_Implementation.thy Fri Apr 20 11:21:42 2007 +0200
@@ -19,11 +19,10 @@
where
"connect_edges ((n,e,m), (n', e', m')) = (n, e * e', m')"
-lemma grcomp_code[code]:
+lemma grcomp_code [code]:
"grcomp (Graph G) (Graph H) = Graph (connect_edges ` { x \<in> G\<times>H. edges_match x })"
by (rule graph_ext) (auto simp:graph_mult_def has_edge_def image_def)
-
definition test_SCT :: "acg \<Rightarrow> bool"
where
"test_SCT \<A> =
@@ -119,6 +118,6 @@
Kleene_Algebras SCT
SCT_Implementation SCT
-code_gen test_SCT (SML -)
+code_gen test_SCT (SML #)
end
--- a/src/HOL/Map.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Map.thy Fri Apr 20 11:21:42 2007 +0200
@@ -84,7 +84,7 @@
"map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
defs
- map_upds_def: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
+ map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
subsection {* @{term [source] empty} *}
--- a/src/HOL/Nat.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Nat.thy Fri Apr 20 11:21:42 2007 +0200
@@ -62,7 +62,9 @@
Zero_nat_def: "0 == Abs_Nat Zero_Rep"
One_nat_def [simp]: "1 == Suc 0"
less_def: "m < n == (m, n) : pred_nat^+"
- le_def: "m \<le> (n::nat) == ~ (n < m)" ..
+ le_def: "m \<le> (n::nat) == ~ (n < m)" ..
+
+lemmas [code nofunc] = less_def le_def
text {* Induction *}
--- a/src/HOL/Presburger.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Presburger.thy Fri Apr 20 11:21:42 2007 +0200
@@ -1069,11 +1069,12 @@
lemma eq_number_of [code func]:
"((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
unfolding number_of_is_id ..
+
lemma eq_Pls_Pls:
- "Numeral.Pls = Numeral.Pls" ..
+ "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
lemma eq_Pls_Min:
- "Numeral.Pls \<noteq> Numeral.Min"
+ "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
unfolding Pls_def Min_def by auto
lemma eq_Pls_Bit0:
@@ -1081,18 +1082,18 @@
unfolding Pls_def Bit_def bit.cases by auto
lemma eq_Pls_Bit1:
- "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
+ "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
unfolding Pls_def Bit_def bit.cases by arith
lemma eq_Min_Pls:
- "Numeral.Min \<noteq> Numeral.Pls"
+ "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
unfolding Pls_def Min_def by auto
lemma eq_Min_Min:
- "Numeral.Min = Numeral.Min" ..
+ "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
lemma eq_Min_Bit0:
- "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
+ "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
unfolding Min_def Bit_def bit.cases by arith
lemma eq_Min_Bit1:
@@ -1104,11 +1105,11 @@
unfolding Pls_def Bit_def bit.cases by auto
lemma eq_Bit1_Pls:
- "Numeral.Bit k bit.B1 \<noteq> Numeral.Pls"
+ "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
unfolding Pls_def Bit_def bit.cases by arith
lemma eq_Bit0_Min:
- "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
+ "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
unfolding Min_def Bit_def bit.cases by arith
lemma eq_Bit1_Min:
@@ -1140,10 +1141,10 @@
unfolding number_of_is_id ..
lemma less_eq_Pls_Pls:
- "Numeral.Pls \<le> Numeral.Pls" ..
+ "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
lemma less_eq_Pls_Min:
- "\<not> (Numeral.Pls \<le> Numeral.Min)"
+ "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
unfolding Pls_def Min_def by auto
lemma less_eq_Pls_Bit:
@@ -1151,11 +1152,11 @@
unfolding Pls_def Bit_def by (cases v) auto
lemma less_eq_Min_Pls:
- "Numeral.Min \<le> Numeral.Pls"
+ "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
unfolding Pls_def Min_def by auto
lemma less_eq_Min_Min:
- "Numeral.Min \<le> Numeral.Min" ..
+ "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
lemma less_eq_Min_Bit0:
"Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
@@ -1198,10 +1199,10 @@
unfolding number_of_is_id ..
lemma less_Pls_Pls:
- "\<not> (Numeral.Pls < Numeral.Pls)" by auto
+ "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
lemma less_Pls_Min:
- "\<not> (Numeral.Pls < Numeral.Min)"
+ "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
unfolding Pls_def Min_def by auto
lemma less_Pls_Bit0:
@@ -1213,11 +1214,11 @@
unfolding Pls_def Bit_def by auto
lemma less_Min_Pls:
- "Numeral.Min < Numeral.Pls"
+ "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
unfolding Pls_def Min_def by auto
lemma less_Min_Min:
- "\<not> (Numeral.Min < Numeral.Min)" by auto
+ "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
lemma less_Min_Bit:
"Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
--- a/src/HOL/Product_Type.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Product_Type.thy Fri Apr 20 11:21:42 2007 +0200
@@ -104,10 +104,10 @@
Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)"
fst_def: "fst p == THE a. EX b. p = Pair a b"
snd_def: "snd p == THE b. EX a. p = Pair a b"
- split_def: "split == (%c p. c (fst p) (snd p))"
- curry_def: "curry == (%c x y. c (Pair x y))"
- prod_fun_def: "prod_fun f g == split (%x y. Pair (f x) (g y))"
- Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
+ split_def [code func]: "split == (%c p. c (fst p) (snd p))"
+ curry_def [code func]: "curry == (%c x y. c (Pair x y))"
+ prod_fun_def [code func]: "prod_fun f g == split (%x y. Pair (f x) (g y))"
+ Sigma_def [code func]: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
abbreviation
Times :: "['a set, 'b set] => ('a * 'b) set"
@@ -599,17 +599,22 @@
done
-constdefs
- upd_fst :: "('a => 'c) => 'a * 'b => 'c * 'b"
- "upd_fst f == prod_fun f id"
+definition
+ upd_fst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
+where
+ "upd_fst f = prod_fun f id"
- upd_snd :: "('b => 'c) => 'a * 'b => 'a * 'c"
- "upd_snd f == prod_fun id f"
+definition
+ upd_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
+where
+ "upd_snd f = prod_fun id f"
-lemma upd_fst_conv [simp]: "upd_fst f (x,y) = (f x,y)"
+lemma upd_fst_conv [simp, code func]:
+ "upd_fst f (x, y) = (f x, y)"
by (simp add: upd_fst_def)
-lemma upd_snd_conv [simp]: "upd_snd f (x,y) = (x,f y)"
+lemma upd_snd_conv [simp, code func]:
+ "upd_snd f (x, y) = (x, f y)"
by (simp add: upd_snd_def)
text {*
--- a/src/HOL/Record.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Record.thy Fri Apr 20 11:21:42 2007 +0200
@@ -17,11 +17,10 @@
lemma rec_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
by simp
-constdefs K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
-"K_record c x \<equiv> c"
-
-lemma K_record_apply [simp]: "K_record c x = c"
- by (simp add: K_record_def)
+definition
+ K_record:: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
+where
+ K_record_apply [simp]: "K_record c x = c"
lemma K_record_comp [simp]: "(K_record c \<circ> f) = K_record c"
by (rule ext) (simp add: K_record_apply comp_def)
--- a/src/HOL/Set.thy Fri Apr 20 11:21:41 2007 +0200
+++ b/src/HOL/Set.thy Fri Apr 20 11:21:42 2007 +0200
@@ -145,8 +145,10 @@
subscripts in Proof General. *}
instance set :: (type) ord
- subset_def: "A <= B == \<forall>x\<in>A. x \<in> B"
- psubset_def: "A < B == (A::'a set) <= B & ~ A=B" ..
+ subset_def: "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
+ psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
+
+lemmas [code nofunc] = subset_def psubset_def
abbreviation
subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
@@ -344,6 +346,8 @@
Compl_def: "- A == {x. ~x:A}"
set_diff_def: "A - B == {x. x:A & ~x:B}" ..
+lemmas [code nofunc] = Compl_def set_diff_def
+
defs
Un_def: "A Un B == {x. x:A | x:B}"
Int_def: "A Int B == {x. x:A & x:B}"
@@ -2126,6 +2130,8 @@
sup_set_eq: "sup A B \<equiv> A \<union> B"
by intro_classes (auto simp add: inf_set_eq sup_set_eq)
+lemmas [code nofunc] = inf_set_eq sup_set_eq
+
subsection {* Basic ML bindings *}
--- a/src/Pure/Isar/ROOT.ML Fri Apr 20 11:21:41 2007 +0200
+++ b/src/Pure/Isar/ROOT.ML Fri Apr 20 11:21:42 2007 +0200
@@ -11,6 +11,7 @@
use "auto_bind.ML";
use "local_syntax.ML";
use "proof_context.ML";
+use "../axclass.ML";
use "local_defs.ML";
(*outer syntax*)
@@ -41,13 +42,17 @@
use "net_rules.ML";
use "induct_attrib.ML";
+(*code generator base*)
+use "../Tools/codegen_consts.ML";
+use "../Tools/codegen_func.ML";
+use "../Tools/codegen_data.ML";
+
(*derived theory and proof elements*)
use "local_theory.ML";
use "calculation.ML";
use "obtain.ML";
use "locale.ML";
use "spec_parse.ML";
-use "../axclass.ML";
use "../Tools/class_package.ML";
use "theory_target.ML";
use "specification.ML";
--- a/src/Pure/Isar/isar_syn.ML Fri Apr 20 11:21:41 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Apr 20 11:21:42 2007 +0200
@@ -89,7 +89,7 @@
(P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
P.!!! (P.list1 P.xname)) []
-- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
- >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
+ >> (fn (x, y) => Toplevel.theory (snd o ClassPackage.axclass_cmd x y)));
(* types *)
@@ -432,11 +432,6 @@
>> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
) >> (Toplevel.print oo Toplevel.theory_to_proof));
-val print_classesP =
- OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
- o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
-
end;
@@ -710,6 +705,16 @@
+(** code generation **)
+
+val code_datatypeP =
+ OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl (
+ Scan.repeat1 P.term
+ >> (Toplevel.theory o CodegenData.add_datatype_consts_cmd)
+ );
+
+
+
(** diagnostic commands (for interactive mode only) **)
val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
@@ -752,6 +757,11 @@
OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
+val print_classesP =
+ OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
+ o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
+
val print_localeP =
OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
(opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
@@ -860,6 +870,11 @@
OuterSyntax.improper_command "typ" "read and print type" K.diag
(opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
+val print_codesetupP =
+ OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag
+ (Scan.succeed
+ (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
+ (CodegenData.print_codesetup o Toplevel.theory_of)));
(** system commands (for interactive mode only) **)
@@ -994,6 +1009,8 @@
apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
interpretP,
+ (*code generation*)
+ code_datatypeP,
(*diagnostic commands*)
pretty_setmarginP, helpP, print_classesP, print_commandsP, print_contextP,
print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
@@ -1003,7 +1020,7 @@
print_methodsP, print_antiquotationsP, thy_depsP, class_depsP, thm_depsP,
find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
print_thmsP, print_prfsP, print_full_prfsP, print_propP,
- print_termP, print_typeP,
+ print_termP, print_typeP, print_codesetupP,
(*system commands*)
cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
--- a/src/Pure/Isar/specification.ML Fri Apr 20 11:21:41 2007 +0200
+++ b/src/Pure/Isar/specification.ML Fri Apr 20 11:21:42 2007 +0200
@@ -130,7 +130,8 @@
(* |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs)); FIXME *)
|> LocalTheory.def Thm.definitionK ((x, mx), ((name, []), rhs));
val ((b, [th']), lthy3) = lthy2
- |> LocalTheory.note Thm.definitionK ((name, atts), [prove lthy2 th]);
+ |> LocalTheory.note Thm.definitionK
+ ((name, CodegenData.add_func_attr false :: atts), [prove lthy2 th]);
val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
--- a/src/Pure/Tools/ROOT.ML Fri Apr 20 11:21:41 2007 +0200
+++ b/src/Pure/Tools/ROOT.ML Fri Apr 20 11:21:42 2007 +0200
@@ -15,9 +15,6 @@
use "../codegen.ML";
(*code generator, 2nd generation*)
-use "codegen_consts.ML";
-use "codegen_func.ML";
-use "codegen_data.ML";
use "codegen_names.ML";
use "codegen_funcgr.ML";
use "codegen_thingol.ML";
--- a/src/Pure/Tools/codegen_data.ML Fri Apr 20 11:21:41 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML Fri Apr 20 11:21:42 2007 +0200
@@ -14,6 +14,7 @@
val add_func: bool -> thm -> theory -> theory
val del_func: thm -> theory -> theory
val add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory
+ val add_func_attr: bool -> Attrib.src
val add_inline: thm -> theory -> theory
val del_inline: thm -> theory -> theory
val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory
@@ -23,6 +24,7 @@
val add_datatype: string * ((string * sort) list * (string * typ list) list)
-> theory -> theory
val add_datatype_consts: CodegenConsts.const list -> theory -> theory
+ val add_datatype_consts_cmd: string list -> theory -> theory
val coregular_algebra: theory -> Sorts.algebra
val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
@@ -33,6 +35,8 @@
val preprocess_cterm: cterm -> thm
+ val print_codesetup: theory -> unit
+
val trace: bool ref
end;
@@ -91,7 +95,7 @@
then (false, xs)
else (true, AList.merge eq_key eq xys);
-val merge_thms = merge' Thm.eq_thm;
+val merge_thms = merge' Thm.eq_thm_prop;
fun merge_lthms (r1, r2) =
if Susp.same (r1, r2)
@@ -122,7 +126,7 @@
fun drop thm' = not (matches args (args_of thm'))
orelse (warning ("Dropping redundant defining equation\n" ^ string_of_thm thm'); false);
val (keeps, drops) = List.partition drop sels;
- in (thm :: keeps, dels |> fold (insert Thm.eq_thm) drops |> remove Thm.eq_thm thm) end;
+ in (thm :: keeps, dels |> fold (insert Thm.eq_thm_prop) drops |> remove Thm.eq_thm_prop thm) end;
fun add_thm thm (sels, dels) =
apfst Susp.value (add_drop_redundant thm (Susp.force sels, dels));
@@ -135,7 +139,7 @@
fold add_thm (Susp.force lthms) (sels, dels);
fun del_thm thm (sels, dels) =
- (Susp.value (remove Thm.eq_thm thm (Susp.force sels)), thm :: dels);
+ (Susp.value (remove Thm.eq_thm_prop thm (Susp.force sels)), thm :: dels);
fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels;
@@ -144,8 +148,8 @@
val (dels_t, dels) = merge_thms (dels1, dels2);
in if dels_t
then let
- val (_, sels) = merge_thms (Susp.force sels1, subtract Thm.eq_thm dels1 (Susp.force sels2))
- val (_, dels) = merge_thms (dels1, subtract Thm.eq_thm (Susp.force sels1) dels2)
+ val (_, sels) = merge_thms (Susp.force sels1, subtract Thm.eq_thm_prop dels1 (Susp.force sels2))
+ val (_, dels) = merge_thms (dels1, subtract Thm.eq_thm_prop (Susp.force sels1) dels2)
in (true, ((lazy_thms o K) sels, dels)) end
else let
val (sels_t, sels) = merge_lthms (sels1, sels2)
@@ -377,6 +381,8 @@
end;
end);
+val print_codesetup = CodeData.print;
+
fun init k = CodeData.map
(fn (exec, data) => (exec, ref (Datatab.update (k, invoke_empty k) (! data))));
@@ -402,16 +408,16 @@
fun common_typ_funcs [] = []
| common_typ_funcs [thm] = [thm]
- | common_typ_funcs thms =
+ | common_typ_funcs (thms as thm :: _) =
let
- val thy = Thm.theory_of_thm (hd thms)
+ val thy = Thm.theory_of_thm thm;
fun incr_thm thm max =
let
val thm' = incr_indexes max thm;
val max' = Thm.maxidx_of thm' + 1;
in (thm', max') end;
val (thms', maxidx) = fold_map incr_thm thms 0;
- val (ty1::tys) = map CodegenFunc.typ_func thms';
+ val ty1 :: tys = map (snd o CodegenFunc.head_func) thms';
fun unify ty env = Sign.typ_unify thy (ty1, ty) env
handle Type.TUNIFY =>
error ("Type unificaton failed, while unifying defining equations\n"
@@ -423,12 +429,12 @@
cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
in map (Thm.instantiate (instT, [])) thms' end;
-fun certify_const thy c c_thms =
+fun certify_const thy const thms =
let
- fun cert (c', thm) = if CodegenConsts.eq_const (c, c')
+ fun cert thm = if CodegenConsts.eq_const (const, fst (CodegenFunc.head_func thm))
then thm else error ("Wrong head of defining equation,\nexpected constant "
- ^ CodegenConsts.string_of_const thy c ^ "\n" ^ string_of_thm thm)
- in map cert c_thms end;
+ ^ CodegenConsts.string_of_const thy const ^ "\n" ^ string_of_thm thm)
+ in map cert thms end;
@@ -459,7 +465,7 @@
|> maps these
|> map (Thm.transfer thy);
val sorts = map (map (snd o dest_TVar) o snd o dest_Type o the_single
- o Sign.const_typargs thy o fst o CodegenFunc.dest_func) funcs;
+ o Sign.const_typargs thy o (fn ((c, _), ty) => (c, ty)) o CodegenFunc.head_func) funcs;
in sorts end;
fun weakest_constraints thy (class, tyco) =
@@ -512,51 +518,49 @@
val classop_weakest_typ = gen_classop_typ weakest_constraints;
val classop_strongest_typ = gen_classop_typ strongest_constraints;
-fun gen_mk_func_typ strict thm =
+fun assert_func_typ thm =
let
val thy = Thm.theory_of_thm thm;
- val raw_funcs = CodegenFunc.mk_func strict thm;
- val error_warning = if strict then error else warning #> K NONE;
fun check_typ_classop class (const as (c, SOME tyco), thm) =
let
- val ((_, ty), _) = CodegenFunc.dest_func thm;
+ val (_, ty) = CodegenFunc.head_func thm;
val ty_decl = classop_weakest_typ thy class (c, tyco);
val ty_strongest = classop_strongest_typ thy class (c, tyco);
fun constrain thm =
let
val max = Thm.maxidx_of thm + 1;
val ty_decl' = Logic.incr_tvar max ty_decl;
- val ((_, ty'), _) = CodegenFunc.dest_func thm;
+ val (_, ty') = CodegenFunc.head_func thm;
val (env, _) = Sign.typ_unify thy (ty_decl', ty') (Vartab.empty, max);
val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
in Thm.instantiate (instT, []) thm end;
in if Sign.typ_instance thy (ty_strongest, ty)
then if Sign.typ_instance thy (ty, ty_decl)
- then SOME (const, thm)
+ then thm
else (warning ("Constraining type\n" ^ CodegenConsts.string_of_typ thy ty
^ "\nof defining equation\n"
^ string_of_thm thm
^ "\nto permitted most general type\n"
^ CodegenConsts.string_of_typ thy ty_decl);
- SOME (const, constrain thm))
- else error_warning ("Type\n" ^ CodegenConsts.string_of_typ thy ty
+ constrain thm)
+ else CodegenFunc.bad_thm ("Type\n" ^ CodegenConsts.string_of_typ thy ty
^ "\nof defining equation\n"
^ string_of_thm thm
^ "\nis incompatible with permitted least general type\n"
^ CodegenConsts.string_of_typ thy ty_strongest)
end
| check_typ_classop class ((c, NONE), thm) =
- error_warning ("Illegal type for class operation " ^ quote c
+ CodegenFunc.bad_thm ("Illegal type for class operation " ^ quote c
^ "\nin defining equation\n"
^ string_of_thm thm);
fun check_typ_fun (const as (c, _), thm) =
let
- val ((_, ty), _) = CodegenFunc.dest_func thm;
+ val (_, ty) = CodegenFunc.head_func thm;
val ty_decl = Sign.the_const_type thy c;
in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
- then SOME (const, thm)
- else error_warning ("Type\n" ^ CodegenConsts.string_of_typ thy ty
+ then thm
+ else CodegenFunc.bad_thm ("Type\n" ^ CodegenConsts.string_of_typ thy ty
^ "\nof defining equation\n"
^ string_of_thm thm
^ "\nis incompatible declared function type\n"
@@ -566,23 +570,34 @@
case AxClass.class_of_param thy c
of SOME class => check_typ_classop class (const, thm)
| NONE => check_typ_fun (const, thm);
- val funcs = map_filter check_typ raw_funcs;
- in funcs end;
+ in check_typ (fst (CodegenFunc.head_func thm), thm) end;
+
+val mk_func = CodegenFunc.error_thm
+ (assert_func_typ o CodegenFunc.mk_func);
+val mk_func_liberal = CodegenFunc.warning_thm
+ (assert_func_typ o CodegenFunc.mk_func);
end;
-
(** interfaces **)
-fun add_func strict thm thy =
- let
- val funcs = gen_mk_func_typ strict thm;
- val cs = map fst funcs;
- in
- map_exec_purge (SOME cs) (map_funcs
- (fold (fn (c, thm) => Consttab.map_default
- (c, (Susp.value [], [])) (add_thm thm)) funcs)) thy
- end;
+fun add_func true thm thy =
+ let
+ val func = mk_func thm;
+ val (const, _) = CodegenFunc.head_func func;
+ in map_exec_purge (SOME [const]) (map_funcs
+ (Consttab.map_default
+ (const, (Susp.value [], [])) (add_thm func))) thy
+ end
+ | add_func false thm thy =
+ case mk_func_liberal thm
+ of SOME func => let
+ val (const, _) = CodegenFunc.head_func func
+ in map_exec_purge (SOME [const]) (map_funcs
+ (Consttab.map_default
+ (const, (Susp.value [], [])) (add_thm func))) thy
+ end
+ | NONE => thy;
fun delete_force msg key xs =
if AList.defined (op =) xs key then AList.delete (op =) key xs
@@ -590,23 +605,26 @@
fun del_func thm thy =
let
- val funcs = gen_mk_func_typ false thm;
- val cs = map fst funcs;
- in
- map_exec_purge (SOME cs) (map_funcs
- (fold (fn (c, thm) => Consttab.map_entry c
- (del_thm thm)) funcs)) thy
+ val func = mk_func thm;
+ val (const, _) = CodegenFunc.head_func func;
+ in map_exec_purge (SOME [const]) (map_funcs
+ (Consttab.map_entry
+ const (del_thm func))) thy
end;
fun add_funcl (const, lthms) thy =
let
- val lthms' = certificate thy (fn thy => certify_const thy const
- o maps (CodegenFunc.mk_func true)) lthms;
+ val lthms' = certificate thy (fn thy => certify_const thy const) lthms;
+ (*FIXME must check compatibility with sort algebra;
+ alas, naive checking results in non-termination!*)
in
map_exec_purge (SOME [const]) (map_funcs (Consttab.map_default (const, (Susp.value [], []))
(add_lthms lthms'))) thy
end;
+fun add_func_attr strict = Attrib.internal (fn _ => Thm.declaration_attribute
+ (fn thm => Context.mapping (add_func strict thm) I));
+
local
fun del_datatype tyco thy =
@@ -637,12 +655,12 @@
fun add_inline thm thy =
(map_exec_purge NONE o map_preproc o apfst o apfst)
- (fold (insert Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
+ (insert Thm.eq_thm_prop (CodegenFunc.mk_rew thm)) thy;
(*fully applied in order to get right context for mk_rew!*)
fun del_inline thm thy =
(map_exec_purge NONE o map_preproc o apfst o apfst)
- (fold (remove Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
+ (remove Thm.eq_thm_prop (CodegenFunc.mk_rew thm)) thy;
(*fully applied in order to get right context for mk_rew!*)
fun add_inline_proc (name, f) =
@@ -680,12 +698,9 @@
fun apply_preproc thy f [] = []
| apply_preproc thy f (thms as (thm :: _)) =
let
+ val (const, _) = CodegenFunc.head_func thm;
val thms' = f thy thms;
- val thms'' as ((const, _) :: _) = map CodegenFunc.mk_head thms'
- in (certify_const thy const o map CodegenFunc.mk_head) thms' end;
-
-fun cmp_thms thy =
- make_ord (fn (thm1, thm2) => not (Sign.typ_instance thy (CodegenFunc.typ_func thm1, CodegenFunc.typ_func thm2)));
+ in certify_const thy const thms' end;
fun rhs_conv conv thm =
let
@@ -700,7 +715,6 @@
|> map (CodegenFunc.rewrite_func ((#inlines o the_preproc o get_exec) thy))
|> fold (fn (_, (_, f)) => apply_inline_proc thy f) ((#inline_procs o the_preproc o get_exec) thy)
(*FIXME - must check: rewrite rule, defining equation, proper constant |> map (snd o check_func false thy) *)
- |> sort (cmp_thms thy)
|> common_typ_funcs;
fun preprocess_cterm ct =
@@ -757,38 +771,14 @@
|> these
|> map (Thm.transfer thy);
-fun find_def thy (const as (c, _)) =
- let
- val specs = Defs.specifications_of (Theory.defs_of thy) c;
- val ty = case try (default_typ_proto thy) const
- of NONE => NONE
- | SOME ty => ty;
- val tys = Sign.const_typargs thy (c, ty |> the_default (Sign.the_const_type thy c));
- fun get_def (_, { is_def, name, lhs, rhs, thyname }) =
- if is_def andalso forall (Sign.typ_instance thy) (tys ~~ lhs) then
- try (Thm.get_axiom_i thy) name
- else NONE
- in get_first get_def specs end;
-
in
fun these_funcs thy const =
let
- fun get_prim_def_funcs (const as (c, tys)) =
- case find_def thy const
- of SOME thm =>
- thm
- |> Thm.transfer thy
- |> gen_mk_func_typ false
- |> map (CodegenFunc.expand_eta ~1 o snd)
- | NONE => []
fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals
o ObjectLogic.drop_judgment thy o Thm.plain_prop_of);
- val funcs = case get_funcs thy const
- of [] => get_prim_def_funcs const
- | funcs => funcs
in
- funcs
+ get_funcs thy const
|> preprocess thy
|> drop_refl thy
end;
@@ -796,61 +786,14 @@
fun default_typ thy (const as (c, _)) = case default_typ_proto thy const
of SOME ty => ty
| NONE => (case get_funcs thy const
- of thm :: _ => CodegenFunc.typ_func thm
+ of thm :: _ => snd (CodegenFunc.head_func thm)
| [] => Sign.the_const_type thy c);
end; (*local*)
-
-(** code attributes **)
-
-local
- fun add_simple_attribute (name, f) =
- (Codegen.add_attribute name o (Scan.succeed o Thm.declaration_attribute))
- (fn th => Context.mapping (f th) I);
-in
- val _ = map (Context.add_setup o add_simple_attribute) [
- ("func", add_func true),
- ("nofunc", del_func),
- ("unfold", (fn thm => Codegen.add_unfold thm #> add_inline thm)),
- ("inline", add_inline),
- ("noinline", del_inline)
- ]
-end; (*local*)
-
-
-(** Isar setup **)
-
-local
-
-structure P = OuterParse
-and K = OuterKeyword
-
-val print_codesetupK = "print_codesetup";
-val code_datatypeK = "code_datatype";
-
-in
-
-val print_codesetupP =
- OuterSyntax.improper_command print_codesetupK "print code generator setup of this theory" K.diag
- (Scan.succeed
- (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep (CodeData.print o Toplevel.theory_of)));
-
-val code_datatypeP =
- OuterSyntax.command code_datatypeK "define set of code datatype constructors" K.thy_decl (
- Scan.repeat1 P.term
- >> (Toplevel.theory o add_datatype_consts_cmd)
- );
-
-
-val _ = OuterSyntax.add_parsers [print_codesetupP, code_datatypeP];
-
-end; (*local*)
-
end; (*struct*)
-
(** type-safe interfaces for data depedent on executable content **)
signature CODE_DATA_ARGS =