--- a/src/HOL/Code_Evaluation.thy Tue Dec 08 18:38:08 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy Tue Dec 08 18:40:20 2009 +0100
@@ -279,7 +279,7 @@
val eval_ref = Unsynchronized.ref (NONE : (unit -> term) option);
fun eval_term thy t =
- Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
+ Code_Eval.eval NONE ("Eval.eval_ref", eval_ref) I thy (HOLogic.mk_term_of (fastype_of t) t) [];
end;
*}
--- a/src/HOL/GCD.thy Tue Dec 08 18:38:08 2009 +0100
+++ b/src/HOL/GCD.thy Tue Dec 08 18:40:20 2009 +0100
@@ -25,7 +25,7 @@
*)
-header {* GCD *}
+header {* Greates common divisor and least common multiple *}
theory GCD
imports Fact Parity
@@ -33,7 +33,7 @@
declare One_nat_def [simp del]
-subsection {* gcd *}
+subsection {* GCD and LCM definitions *}
class gcd = zero + one + dvd +
@@ -50,11 +50,7 @@
end
-
-(* definitions for the natural numbers *)
-
instantiation nat :: gcd
-
begin
fun
@@ -72,11 +68,7 @@
end
-
-(* definitions for the integers *)
-
instantiation int :: gcd
-
begin
definition
@@ -94,8 +86,7 @@
end
-subsection {* Set up Transfer *}
-
+subsection {* Transfer setup *}
lemma transfer_nat_int_gcd:
"(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
@@ -125,7 +116,7 @@
transfer_int_nat_gcd transfer_int_nat_gcd_closures]
-subsection {* GCD *}
+subsection {* GCD properties *}
(* was gcd_induct *)
lemma gcd_nat_induct:
@@ -547,6 +538,10 @@
apply simp
done
+lemma gcd_code_int [code]:
+ "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
+ by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
+
subsection {* Coprimality *}
@@ -1225,9 +1220,9 @@
qed
-subsection {* LCM *}
+subsection {* LCM properties *}
-lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
+lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
by (simp add: lcm_int_def lcm_nat_def zdiv_int
zmult_int [symmetric] gcd_int_def)
@@ -1443,6 +1438,7 @@
lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
+
subsubsection {* The complete divisibility lattice *}
--- a/src/HOL/HOL.thy Tue Dec 08 18:38:08 2009 +0100
+++ b/src/HOL/HOL.thy Tue Dec 08 18:40:20 2009 +0100
@@ -1971,7 +1971,7 @@
val t = Thm.term_of ct;
val dummy = @{cprop True};
in case try HOLogic.dest_Trueprop t
- of SOME t' => if Code_ML.eval NONE
+ of SOME t' => if Code_Eval.eval NONE
("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' []
then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
else dummy
--- a/src/HOL/IsaMakefile Tue Dec 08 18:38:08 2009 +0100
+++ b/src/HOL/IsaMakefile Tue Dec 08 18:40:20 2009 +0100
@@ -103,6 +103,7 @@
$(SRC)/Provers/hypsubst.ML \
$(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/splitter.ML \
+ $(SRC)/Tools/Code/code_eval.ML \
$(SRC)/Tools/Code/code_haskell.ML \
$(SRC)/Tools/Code/code_ml.ML \
$(SRC)/Tools/Code/code_preproc.ML \
@@ -369,7 +370,6 @@
Library/Sum_Of_Squares/sos_wrapper.ML \
Library/Sum_Of_Squares/sum_of_squares.ML Library/Fset.thy \
Library/Glbs.thy Library/normarith.ML Library/Executable_Set.thy \
- Library/Crude_Executable_Set.thy \
Library/Infinite_Set.thy Library/FuncSet.thy \
Library/Permutations.thy Library/Bit.thy Library/FrechetDeriv.thy \
Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy \
--- a/src/HOL/Library/Crude_Executable_Set.thy Tue Dec 08 18:38:08 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,259 +0,0 @@
-(* Title: HOL/Library/Crude_Executable_Set.thy
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *}
-
-theory Crude_Executable_Set
-imports List_Set
-begin
-
-declare mem_def [code del]
-declare Collect_def [code del]
-declare insert_code [code del]
-declare vimage_code [code del]
-
-subsection {* Set representation *}
-
-setup {*
- Code.add_type_cmd "set"
-*}
-
-definition Set :: "'a list \<Rightarrow> 'a set" where
- [simp]: "Set = set"
-
-definition Coset :: "'a list \<Rightarrow> 'a set" where
- [simp]: "Coset xs = - set xs"
-
-setup {*
- Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool")
-*}
-
-code_datatype Set Coset
-
-
-subsection {* Basic operations *}
-
-lemma [code]:
- "set xs = Set (remdups xs)"
- by simp
-
-lemma [code]:
- "x \<in> Set xs \<longleftrightarrow> member x xs"
- "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs"
- by (simp_all add: mem_iff)
-
-definition is_empty :: "'a set \<Rightarrow> bool" where
- [simp]: "is_empty A \<longleftrightarrow> A = {}"
-
-lemma [code_inline]:
- "A = {} \<longleftrightarrow> is_empty A"
- by simp
-
-definition empty :: "'a set" where
- [simp]: "empty = {}"
-
-lemma [code_inline]:
- "{} = empty"
- by simp
-
-setup {*
- Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
- #> Code.add_signature_cmd ("empty", "'a set")
- #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
- #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
- #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
- #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
-*}
-
-lemma is_empty_Set [code]:
- "is_empty (Set xs) \<longleftrightarrow> null xs"
- by (simp add: empty_null)
-
-lemma empty_Set [code]:
- "empty = Set []"
- by simp
-
-lemma insert_Set [code]:
- "insert x (Set xs) = Set (List_Set.insert x xs)"
- "insert x (Coset xs) = Coset (remove_all x xs)"
- by (simp_all add: insert_set insert_set_compl)
-
-lemma remove_Set [code]:
- "remove x (Set xs) = Set (remove_all x xs)"
- "remove x (Coset xs) = Coset (List_Set.insert x xs)"
- by (simp_all add:remove_set remove_set_compl)
-
-lemma image_Set [code]:
- "image f (Set xs) = Set (remdups (map f xs))"
- by simp
-
-lemma project_Set [code]:
- "project P (Set xs) = Set (filter P xs)"
- by (simp add: project_set)
-
-lemma Ball_Set [code]:
- "Ball (Set xs) P \<longleftrightarrow> list_all P xs"
- by (simp add: ball_set)
-
-lemma Bex_Set [code]:
- "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
- by (simp add: bex_set)
-
-lemma card_Set [code]:
- "card (Set xs) = length (remdups xs)"
-proof -
- have "card (set (remdups xs)) = length (remdups xs)"
- by (rule distinct_card) simp
- then show ?thesis by simp
-qed
-
-
-subsection {* Derived operations *}
-
-definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- [simp]: "set_eq = op ="
-
-lemma [code_inline]:
- "op = = set_eq"
- by simp
-
-definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- [simp]: "subset_eq = op \<subseteq>"
-
-lemma [code_inline]:
- "op \<subseteq> = subset_eq"
- by simp
-
-definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- [simp]: "subset = op \<subset>"
-
-lemma [code_inline]:
- "op \<subset> = subset"
- by simp
-
-setup {*
- Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
- #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
- #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
-*}
-
-lemma set_eq_subset_eq [code]:
- "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A"
- by auto
-
-lemma subset_eq_forall [code]:
- "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
- by (simp add: subset_eq)
-
-lemma subset_subset_eq [code]:
- "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A"
- by (simp add: subset)
-
-
-subsection {* Functorial operations *}
-
-definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- [simp]: "inter = op \<inter>"
-
-lemma [code_inline]:
- "op \<inter> = inter"
- by simp
-
-definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- [simp]: "subtract A B = B - A"
-
-lemma [code_inline]:
- "B - A = subtract A B"
- by simp
-
-definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- [simp]: "union = op \<union>"
-
-lemma [code_inline]:
- "op \<union> = union"
- by simp
-
-definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
- [simp]: "Inf = Complete_Lattice.Inf"
-
-lemma [code_inline]:
- "Complete_Lattice.Inf = Inf"
- by simp
-
-definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
- [simp]: "Sup = Complete_Lattice.Sup"
-
-lemma [code_inline]:
- "Complete_Lattice.Sup = Sup"
- by simp
-
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
- [simp]: "Inter = Inf"
-
-lemma [code_inline]:
- "Inf = Inter"
- by simp
-
-definition Union :: "'a set set \<Rightarrow> 'a set" where
- [simp]: "Union = Sup"
-
-lemma [code_inline]:
- "Sup = Union"
- by simp
-
-setup {*
- Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a")
- #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a")
- #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set")
- #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set")
-*}
-
-lemma inter_project [code]:
- "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
- "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
- by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set)
-
-lemma subtract_remove [code]:
- "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
- "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
- by (auto simp add: minus_set)
-
-lemma union_insert [code]:
- "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
- "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
- by (auto simp add: union_set)
-
-lemma Inf_inf [code]:
- "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs"
- "Inf (Coset []) = (bot :: 'a::complete_lattice)"
- by (simp_all add: Inf_UNIV Inf_set_fold)
-
-lemma Sup_sup [code]:
- "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs"
- "Sup (Coset []) = (top :: 'a::complete_lattice)"
- by (simp_all add: Sup_UNIV Sup_set_fold)
-
-lemma Inter_inter [code]:
- "Inter (Set xs) = foldl inter (Coset []) xs"
- "Inter (Coset []) = empty"
- unfolding Inter_def Inf_inf by simp_all
-
-lemma Union_union [code]:
- "Union (Set xs) = foldl union empty xs"
- "Union (Coset []) = Coset []"
- unfolding Union_def Sup_sup by simp_all
-
-hide (open) const is_empty empty remove
- set_eq subset_eq subset inter union subtract Inf Sup Inter Union
-
-end
--- a/src/HOL/Library/Eval_Witness.thy Tue Dec 08 18:38:08 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy Tue Dec 08 18:40:20 2009 +0100
@@ -68,7 +68,7 @@
| dest_exs _ _ = sys_error "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
- if Code_ML.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
+ if Code_Eval.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
then Thm.cterm_of thy goal
else @{cprop True} (*dummy*)
end
--- a/src/HOL/Library/Executable_Set.thy Tue Dec 08 18:38:08 2009 +0100
+++ b/src/HOL/Library/Executable_Set.thy Tue Dec 08 18:40:20 2009 +0100
@@ -1,103 +1,271 @@
(* Title: HOL/Library/Executable_Set.thy
Author: Stefan Berghofer, TU Muenchen
+ Author: Florian Haftmann, TU Muenchen
*)
-header {* Implementation of finite sets by lists *}
+header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *}
theory Executable_Set
-imports Main Fset SML_Quickcheck
+imports List_Set
begin
-subsection {* Preprocessor setup *}
+declare mem_def [code del]
+declare Collect_def [code del]
+declare insert_code [code del]
+declare vimage_code [code del]
+
+subsection {* Set representation *}
+
+setup {*
+ Code.add_type_cmd "set"
+*}
+
+definition Set :: "'a list \<Rightarrow> 'a set" where
+ [simp]: "Set = set"
+
+definition Coset :: "'a list \<Rightarrow> 'a set" where
+ [simp]: "Coset xs = - set xs"
+
+setup {*
+ Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool")
+*}
+
+code_datatype Set Coset
-declare member [code]
+consts_code
+ Coset ("\<module>Coset")
+ Set ("\<module>Set")
+attach {*
+ datatype 'a set = Set of 'a list | Coset of 'a list;
+*} -- {* This assumes that there won't be a @{text Coset} without a @{text Set} *}
+
+
+subsection {* Basic operations *}
+
+lemma [code]:
+ "set xs = Set (remdups xs)"
+ by simp
+
+lemma [code]:
+ "x \<in> Set xs \<longleftrightarrow> member x xs"
+ "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs"
+ by (simp_all add: mem_iff)
+
+definition is_empty :: "'a set \<Rightarrow> bool" where
+ [simp]: "is_empty A \<longleftrightarrow> A = {}"
+
+lemma [code_unfold]:
+ "A = {} \<longleftrightarrow> is_empty A"
+ by simp
definition empty :: "'a set" where
- "empty = {}"
+ [simp]: "empty = {}"
+
+lemma [code_unfold]:
+ "{} = empty"
+ by simp
+
+lemma [code_unfold, code_inline del]:
+ "empty = Set []"
+ by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}
+
+setup {*
+ Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("empty", "'a set")
+ #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
+ #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
+*}
+
+lemma is_empty_Set [code]:
+ "is_empty (Set xs) \<longleftrightarrow> null xs"
+ by (simp add: empty_null)
+
+lemma empty_Set [code]:
+ "empty = Set []"
+ by simp
+
+lemma insert_Set [code]:
+ "insert x (Set xs) = Set (List_Set.insert x xs)"
+ "insert x (Coset xs) = Coset (remove_all x xs)"
+ by (simp_all add: insert_set insert_set_compl)
+
+lemma remove_Set [code]:
+ "remove x (Set xs) = Set (remove_all x xs)"
+ "remove x (Coset xs) = Coset (List_Set.insert x xs)"
+ by (simp_all add:remove_set remove_set_compl)
+
+lemma image_Set [code]:
+ "image f (Set xs) = Set (remdups (map f xs))"
+ by simp
+
+lemma project_Set [code]:
+ "project P (Set xs) = Set (filter P xs)"
+ by (simp add: project_set)
+
+lemma Ball_Set [code]:
+ "Ball (Set xs) P \<longleftrightarrow> list_all P xs"
+ by (simp add: ball_set)
-declare empty_def [symmetric, code_unfold]
+lemma Bex_Set [code]:
+ "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
+ by (simp add: bex_set)
+
+lemma card_Set [code]:
+ "card (Set xs) = length (remdups xs)"
+proof -
+ have "card (set (remdups xs)) = length (remdups xs)"
+ by (rule distinct_card) simp
+ then show ?thesis by simp
+qed
+
+
+subsection {* Derived operations *}
+
+definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+ [simp]: "set_eq = op ="
+
+lemma [code_unfold]:
+ "op = = set_eq"
+ by simp
+
+definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+ [simp]: "subset_eq = op \<subseteq>"
+
+lemma [code_unfold]:
+ "op \<subseteq> = subset_eq"
+ by simp
+
+definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+ [simp]: "subset = op \<subset>"
+
+lemma [code_unfold]:
+ "op \<subset> = subset"
+ by simp
+
+setup {*
+ Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
+ #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
+*}
+
+lemma set_eq_subset_eq [code]:
+ "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A"
+ by auto
+
+lemma subset_eq_forall [code]:
+ "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
+ by (simp add: subset_eq)
+
+lemma subset_subset_eq [code]:
+ "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A"
+ by (simp add: subset)
+
+
+subsection {* Functorial operations *}
definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "inter = op \<inter>"
+ [simp]: "inter = op \<inter>"
+
+lemma [code_unfold]:
+ "op \<inter> = inter"
+ by simp
-declare inter_def [symmetric, code_unfold]
+definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+ [simp]: "subtract A B = B - A"
+
+lemma [code_unfold]:
+ "B - A = subtract A B"
+ by simp
definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
- "union = op \<union>"
-
-declare union_def [symmetric, code_unfold]
+ [simp]: "union = op \<union>"
-definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- "subset = op \<le>"
+lemma [code_unfold]:
+ "op \<union> = union"
+ by simp
-declare subset_def [symmetric, code_unfold]
-
-lemma [code]:
- "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
- by (simp add: subset_def subset_eq)
+definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
+ [simp]: "Inf = Complete_Lattice.Inf"
-definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
- [code del]: "eq_set = op ="
-
-(*declare eq_set_def [symmetric, code_unfold]*)
+lemma [code_unfold]:
+ "Complete_Lattice.Inf = Inf"
+ by simp
-lemma [code]:
- "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
- by (simp add: eq_set_def set_eq)
+definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
+ [simp]: "Sup = Complete_Lattice.Sup"
-declare inter [code]
-
-declare List_Set.project_def [symmetric, code_unfold]
+lemma [code_unfold]:
+ "Complete_Lattice.Sup = Sup"
+ by simp
definition Inter :: "'a set set \<Rightarrow> 'a set" where
- "Inter = Complete_Lattice.Inter"
+ [simp]: "Inter = Inf"
-declare Inter_def [symmetric, code_unfold]
+lemma [code_unfold]:
+ "Inf = Inter"
+ by simp
definition Union :: "'a set set \<Rightarrow> 'a set" where
- "Union = Complete_Lattice.Union"
+ [simp]: "Union = Sup"
-declare Union_def [symmetric, code_unfold]
-
+lemma [code_unfold]:
+ "Sup = Union"
+ by simp
-subsection {* Code generator setup *}
-
-ML {*
-nonfix inter;
-nonfix union;
-nonfix subset;
+setup {*
+ Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a")
+ #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a")
+ #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set")
+ #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set")
*}
-definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
- "flip f a b = f b a"
+lemma inter_project [code]:
+ "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
+ "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
+ by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set)
+
+lemma subtract_remove [code]:
+ "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
+ "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
+ by (auto simp add: minus_set)
-types_code
- fset ("(_/ \<module>fset)")
-attach {*
-datatype 'a fset = Set of 'a list | Coset of 'a list;
-*}
+lemma union_insert [code]:
+ "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
+ "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
+ by (auto simp add: union_set)
-consts_code
- Set ("\<module>Set")
- Coset ("\<module>Coset")
+lemma Inf_inf [code]:
+ "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs"
+ "Inf (Coset []) = (bot :: 'a::complete_lattice)"
+ by (simp_all add: Inf_UNIV Inf_set_fold)
-consts_code
- "empty" ("{*Fset.empty*}")
- "List_Set.is_empty" ("{*Fset.is_empty*}")
- "Set.insert" ("{*Fset.insert*}")
- "List_Set.remove" ("{*Fset.remove*}")
- "Set.image" ("{*Fset.map*}")
- "List_Set.project" ("{*Fset.filter*}")
- "Ball" ("{*flip Fset.forall*}")
- "Bex" ("{*flip Fset.exists*}")
- "union" ("{*Fset.union*}")
- "inter" ("{*Fset.inter*}")
- "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
- "Union" ("{*Fset.Union*}")
- "Inter" ("{*Fset.Inter*}")
- card ("{*Fset.card*}")
- fold ("{*foldl o flip*}")
+lemma Sup_sup [code]:
+ "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs"
+ "Sup (Coset []) = (top :: 'a::complete_lattice)"
+ by (simp_all add: Sup_UNIV Sup_set_fold)
+
+lemma Inter_inter [code]:
+ "Inter (Set xs) = foldl inter (Coset []) xs"
+ "Inter (Coset []) = empty"
+ unfolding Inter_def Inf_inf by simp_all
-hide (open) const empty inter union subset eq_set Inter Union flip
+lemma Union_union [code]:
+ "Union (Set xs) = foldl union empty xs"
+ "Union (Coset []) = Coset []"
+ unfolding Union_def Sup_sup by simp_all
-end
\ No newline at end of file
+hide (open) const is_empty empty remove
+ set_eq subset_eq subset inter union subtract Inf Sup Inter Union
+
+end
--- a/src/HOL/Library/Library.thy Tue Dec 08 18:38:08 2009 +0100
+++ b/src/HOL/Library/Library.thy Tue Dec 08 18:40:20 2009 +0100
@@ -14,7 +14,6 @@
Continuity
ContNotDenum
Countable
- Crude_Executable_Set
Diagonalize
Efficient_Nat
Enum
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Dec 08 18:38:08 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Dec 08 18:40:20 2009 +0100
@@ -2586,11 +2586,11 @@
val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
val eval =
if random then
- Code_ML.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
+ Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
(fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' []
|> Random_Engine.run
else
- Code_ML.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []
+ Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref) Predicate.map thy t' []
in (T, eval) end;
fun values ctxt param_user_modes options k t_compr =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Dec 08 18:38:08 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Tue Dec 08 18:40:20 2009 +0100
@@ -106,7 +106,7 @@
mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
val _ = tracing (Syntax.string_of_term ctxt' qc_term)
- val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
+ val compile = Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
(fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc)
thy'' qc_term []
in
--- a/src/HOL/Tools/quickcheck_generators.ML Tue Dec 08 18:38:08 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML Tue Dec 08 18:40:20 2009 +0100
@@ -379,7 +379,7 @@
let
val Ts = (map snd o fst o strip_abs) t;
val t' = mk_generator_expr thy t Ts;
- val compile = Code_ML.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
+ val compile = Code_Eval.eval (SOME target) ("Quickcheck_Generators.eval_ref", eval_ref)
(fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
in compile #> Random_Engine.run end;
@@ -388,7 +388,7 @@
val setup = Typecopy.interpretation ensure_random_typecopy
#> Datatype.interpretation ensure_random_datatype
- #> Code_Target.extend_target (target, (Code_ML.target_Eval, K I))
+ #> Code_Target.extend_target (target, (Code_Eval.target, K I))
#> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of);
end;
--- a/src/Pure/System/isabelle_system.scala Tue Dec 08 18:38:08 2009 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue Dec 08 18:40:20 2009 +0100
@@ -9,6 +9,7 @@
import java.util.regex.Pattern
import java.util.Locale
import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}
+import java.awt.{GraphicsEnvironment, Font}
import scala.io.Source
import scala.util.matching.Regex
@@ -259,7 +260,7 @@
{
getenv_strict("ISABELLE_TOOLS").split(":").find(dir => {
val file = platform_file(dir + "/" + name)
- try { file.isFile && file.canRead } // file.canExecute requires Java 1.6
+ try { file.isFile && file.canRead && file.canExecute }
catch { case _: SecurityException => false }
}) match {
case Some(dir) =>
@@ -331,4 +332,20 @@
val symbols = new Symbol.Interpretation(
read_symbols("$ISABELLE_HOME/etc/symbols") ++
read_symbols("$ISABELLE_HOME_USER/etc/symbols"))
+
+
+ /* fonts */
+
+ val font_family = "IsabelleText"
+
+ private def create_font(name: String) =
+ Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
+
+ def register_fonts(): Boolean =
+ {
+ val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
+ val ok1 = ge.registerFont(create_font("~~/lib/fonts/IsabelleText.ttf"))
+ val ok2 = ge.registerFont(create_font("~~/lib/fonts/IsabelleTextBold.ttf"))
+ ok1 && ok2
+ }
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Code/code_eval.ML Tue Dec 08 18:40:20 2009 +0100
@@ -0,0 +1,153 @@
+(* Title: Tools/code/code_eval.ML_
+ Author: Florian Haftmann, TU Muenchen
+
+Runtime services building on code generation into implementation language SML.
+*)
+
+signature CODE_EVAL =
+sig
+ val target: string
+ val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
+ -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
+ val evaluation_code: theory -> string list -> string list
+ -> string * ((string * string) list * (string * string) list)
+ val setup: theory -> theory
+end;
+
+structure Code_Eval : CODE_EVAL =
+struct
+
+(** generic **)
+
+val target = "Eval";
+
+val eval_struct_name = "Code";
+
+fun evaluation_code thy tycos consts =
+ let
+ val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
+ val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
+ val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
+ eval_struct_name naming program (consts' @ tycos');
+ val (consts'', tycos'') = chop (length consts') target_names;
+ val consts_map = map2 (fn const => fn NONE =>
+ error ("Constant " ^ (quote o Code.string_of_const thy) const
+ ^ "\nhas a user-defined serialization")
+ | SOME const'' => (const, const'')) consts consts''
+ val tycos_map = map2 (fn tyco => fn NONE =>
+ error ("Type " ^ (quote o Sign.extern_type thy) tyco
+ ^ "\nhas a user-defined serialization")
+ | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
+ in (ml_code, (tycos_map, consts_map)) end;
+
+
+(** evaluation **)
+
+fun eval some_target reff postproc thy t args =
+ let
+ val ctxt = ProofContext.init thy;
+ fun evaluator naming program ((_, (_, ty)), t) deps =
+ let
+ val _ = if Code_Thingol.contains_dictvar t then
+ error "Term to be evaluated contains free dictionaries" else ();
+ val value_name = "Value.VALUE.value"
+ val program' = program
+ |> Graph.new_node (value_name,
+ Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
+ |> fold (curry Graph.add_edge value_name) deps;
+ val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
+ (the_default target some_target) "" naming program' [value_name];
+ val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
+ ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
+ in ML_Context.evaluate ctxt false reff sml_code end;
+ in Code_Thingol.eval thy postproc evaluator t end;
+
+
+(** instrumentalization by antiquotation **)
+
+local
+
+structure CodeAntiqData = Proof_Data
+(
+ type T = (string list * string list) * (bool * (string
+ * (string * ((string * string) list * (string * string) list)) lazy));
+ fun init _ = (([], []), (true, ("", Lazy.value ("", ([], [])))));
+);
+
+val is_first_occ = fst o snd o CodeAntiqData.get;
+
+fun register_code new_tycos new_consts ctxt =
+ let
+ val ((tycos, consts), (_, (struct_name, _))) = CodeAntiqData.get ctxt;
+ val tycos' = fold (insert (op =)) new_tycos tycos;
+ val consts' = fold (insert (op =)) new_consts consts;
+ val (struct_name', ctxt') = if struct_name = ""
+ then ML_Antiquote.variant eval_struct_name ctxt
+ else (struct_name, ctxt);
+ val acc_code = Lazy.lazy (fn () => evaluation_code (ProofContext.theory_of ctxt) tycos' consts');
+ in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
+
+fun register_const const = register_code [] [const];
+
+fun register_datatype tyco constrs = register_code [tyco] constrs;
+
+fun print_const const all_struct_name tycos_map consts_map =
+ (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
+
+fun print_datatype tyco constrs all_struct_name tycos_map consts_map =
+ let
+ val upperize = implode o nth_map 0 Symbol.to_ascii_upper o explode;
+ fun check_base name name'' =
+ if upperize (Long_Name.base_name name) = upperize name''
+ then () else error ("Name as printed " ^ quote name''
+ ^ "\ndiffers from logical base name " ^ quote (Long_Name.base_name name) ^ "; sorry.");
+ val tyco'' = (the o AList.lookup (op =) tycos_map) tyco;
+ val constrs'' = map (the o AList.lookup (op =) consts_map) constrs;
+ val _ = check_base tyco tyco'';
+ val _ = map2 check_base constrs constrs'';
+ in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end;
+
+fun print_code struct_name is_first print_it ctxt =
+ let
+ val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
+ val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
+ val ml_code = if is_first then ml_code
+ else "";
+ val all_struct_name = Long_Name.append struct_name struct_code_name;
+ in (ml_code, print_it all_struct_name tycos_map consts_map) end;
+
+in
+
+fun ml_code_antiq raw_const {struct_name, background} =
+ let
+ val const = Code.check_const (ProofContext.theory_of background) raw_const;
+ val is_first = is_first_occ background;
+ val background' = register_const const background;
+ in (print_code struct_name is_first (print_const const), background') end;
+
+fun ml_code_datatype_antiq (raw_tyco, raw_constrs) {struct_name, background} =
+ let
+ val thy = ProofContext.theory_of background;
+ val tyco = Sign.intern_type thy raw_tyco;
+ val constrs = map (Code.check_const thy) raw_constrs;
+ val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
+ val _ = if eq_set (op =) (constrs, constrs') then ()
+ else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
+ val is_first = is_first_occ background;
+ val background' = register_datatype tyco constrs background;
+ in (print_code struct_name is_first (print_datatype tyco constrs), background') end;
+
+end; (*local*)
+
+
+(** Isar setup **)
+
+val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
+val _ = ML_Context.add_antiq "code_datatype" (fn _ =>
+ (Args.tyname --| Scan.lift (Args.$$$ "=")
+ -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
+ >> ml_code_datatype_antiq);
+
+val setup = Code_Target.extend_target (target, (Code_ML.target_SML, K I));
+
+end; (*struct*)
--- a/src/Tools/Code/code_ml.ML Tue Dec 08 18:38:08 2009 +0100
+++ b/src/Tools/Code/code_ml.ML Tue Dec 08 18:40:20 2009 +0100
@@ -6,9 +6,9 @@
signature CODE_ML =
sig
- val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
- -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
- val target_Eval: string
+ val target_SML: string
+ val evaluation_code_of: theory -> string -> string
+ -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
val setup: theory -> theory
end;
@@ -26,7 +26,6 @@
val target_SML = "SML";
val target_OCaml = "OCaml";
-val target_Eval = "Eval";
datatype ml_binding =
ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
@@ -340,7 +339,9 @@
end;
in print_stmt end;
-fun print_sml_module name some_decls body = Pretty.chunks2 (
+fun print_sml_module name some_decls body = if name = ""
+ then Pretty.chunks2 body
+ else Pretty.chunks2 (
Pretty.chunks (
str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
:: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
@@ -664,7 +665,9 @@
end;
in print_stmt end;
-fun print_ocaml_module name some_decls body = Pretty.chunks2 (
+fun print_ocaml_module name some_decls body = if name = ""
+ then Pretty.chunks2 body
+ else Pretty.chunks2 (
Pretty.chunks (
str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
:: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
@@ -937,142 +940,15 @@
end; (*local*)
-(** ML (system language) code for evaluation and instrumentalization **)
-
-val eval_struct_name = "Code"
-
-fun eval_code_of some_target with_struct thy =
- let
- val target = the_default target_Eval some_target;
- val serialize = if with_struct then fn _ => fn [] =>
- serialize_ml target_SML (SOME (K ())) print_sml_module print_sml_stmt (SOME eval_struct_name) true
- else fn _ => fn [] =>
- serialize_ml target_SML (SOME (K ())) ((K o K) Pretty.chunks2) print_sml_stmt (SOME eval_struct_name) true;
- in Code_Target.serialize_custom thy (target, (serialize, literals_sml)) end;
-
-
-(* evaluation *)
-
-fun eval some_target reff postproc thy t args =
- let
- val ctxt = ProofContext.init thy;
- fun evaluator naming program ((_, (_, ty)), t) deps =
- let
- val _ = if Code_Thingol.contains_dictvar t then
- error "Term to be evaluated contains free dictionaries" else ();
- val value_name = "Value.VALUE.value"
- val program' = program
- |> Graph.new_node (value_name,
- Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
- |> fold (curry Graph.add_edge value_name) deps;
- val (value_code, [SOME value_name']) = eval_code_of some_target false thy naming program' [value_name];
- val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
- ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
- in ML_Context.evaluate ctxt false reff sml_code end;
- in Code_Thingol.eval thy postproc evaluator t end;
-
-
-(* instrumentalization by antiquotation *)
-
-local
-
-structure CodeAntiqData = Proof_Data
-(
- type T = (string list * string list) * (bool * (string
- * (string * ((string * string) list * (string * string) list)) lazy));
- fun init _ = (([], []), (true, ("", Lazy.value ("", ([], [])))));
-);
-
-val is_first_occ = fst o snd o CodeAntiqData.get;
+(** for instrumentalization **)
-fun delayed_code thy tycos consts () =
- let
- val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
- val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
- val (ml_code, target_names) = eval_code_of NONE true thy naming program (consts' @ tycos');
- val (consts'', tycos'') = chop (length consts') target_names;
- val consts_map = map2 (fn const => fn NONE =>
- error ("Constant " ^ (quote o Code.string_of_const thy) const
- ^ "\nhas a user-defined serialization")
- | SOME const'' => (const, const'')) consts consts''
- val tycos_map = map2 (fn tyco => fn NONE =>
- error ("Type " ^ (quote o Sign.extern_type thy) tyco
- ^ "\nhas a user-defined serialization")
- | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
- in (ml_code, (tycos_map, consts_map)) end;
-
-fun register_code new_tycos new_consts ctxt =
- let
- val ((tycos, consts), (_, (struct_name, _))) = CodeAntiqData.get ctxt;
- val tycos' = fold (insert (op =)) new_tycos tycos;
- val consts' = fold (insert (op =)) new_consts consts;
- val (struct_name', ctxt') = if struct_name = ""
- then ML_Antiquote.variant eval_struct_name ctxt
- else (struct_name, ctxt);
- val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) tycos' consts');
- in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
-
-fun register_const const = register_code [] [const];
-
-fun register_datatype tyco constrs = register_code [tyco] constrs;
-
-fun print_const const all_struct_name tycos_map consts_map =
- (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
-
-fun print_datatype tyco constrs all_struct_name tycos_map consts_map =
- let
- val upperize = implode o nth_map 0 Symbol.to_ascii_upper o explode;
- fun check_base name name'' =
- if upperize (Long_Name.base_name name) = upperize name''
- then () else error ("Name as printed " ^ quote name''
- ^ "\ndiffers from logical base name " ^ quote (Long_Name.base_name name) ^ "; sorry.");
- val tyco'' = (the o AList.lookup (op =) tycos_map) tyco;
- val constrs'' = map (the o AList.lookup (op =) consts_map) constrs;
- val _ = check_base tyco tyco'';
- val _ = map2 check_base constrs constrs'';
- in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end;
-
-fun print_code struct_name is_first print_it ctxt =
- let
- val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
- val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
- val ml_code = if is_first then ml_code
- else "";
- val all_struct_name = Long_Name.append struct_name struct_code_name;
- in (ml_code, print_it all_struct_name tycos_map consts_map) end;
-
-in
-
-fun ml_code_antiq raw_const {struct_name, background} =
- let
- val const = Code.check_const (ProofContext.theory_of background) raw_const;
- val is_first = is_first_occ background;
- val background' = register_const const background;
- in (print_code struct_name is_first (print_const const), background') end;
-
-fun ml_code_datatype_antiq (raw_tyco, raw_constrs) {struct_name, background} =
- let
- val thy = ProofContext.theory_of background;
- val tyco = Sign.intern_type thy raw_tyco;
- val constrs = map (Code.check_const thy) raw_constrs;
- val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
- val _ = if eq_set (op =) (constrs, constrs') then ()
- else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
- val is_first = is_first_occ background;
- val background' = register_datatype tyco constrs background;
- in (print_code struct_name is_first (print_datatype tyco constrs), background') end;
-
-end; (*local*)
+fun evaluation_code_of thy target struct_name =
+ Code_Target.serialize_custom thy (target, (fn _ => fn [] =>
+ serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
(** Isar setup **)
-val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
-val _ = ML_Context.add_antiq "code_datatype" (fn _ =>
- (Args.tyname --| Scan.lift (Args.$$$ "=")
- -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
- >> ml_code_datatype_antiq);
-
fun isar_seri_sml module_name =
Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
>> (fn with_signatures => serialize_ml target_SML
@@ -1087,7 +963,6 @@
val setup =
Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
#> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
- #> Code_Target.extend_target (target_Eval, (target_SML, K I))
#> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy [
print_typ (INFX (1, X)) ty1,
--- a/src/Tools/Code/code_target.ML Tue Dec 08 18:38:08 2009 +0100
+++ b/src/Tools/Code/code_target.ML Tue Dec 08 18:40:20 2009 +0100
@@ -217,12 +217,164 @@
map_target_data target o apsnd o apsnd o apsnd;
+(** serializer usage **)
+
+(* montage *)
+
+fun the_literals thy =
+ let
+ val (targets, _) = CodeTargetData.get thy;
+ fun literals target = case Symtab.lookup targets target
+ of SOME data => (case the_serializer data
+ of Serializer (_, literals) => literals
+ | Extends (super, _) => literals super)
+ | NONE => error ("Unknown code target language: " ^ quote target);
+ in literals end;
+
+local
+
+fun activate_syntax lookup_name src_tab = Symtab.empty
+ |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
+ of SOME name => (SOME name,
+ Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
+ | NONE => (NONE, tab)) (Symtab.keys src_tab)
+ |>> map_filter I;
+
+fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
+ |> fold_map (fn thing_identifier => fn (tab, naming) =>
+ case Code_Thingol.lookup_const naming thing_identifier
+ of SOME name => let
+ val (syn, naming') = Code_Printer.activate_const_syntax thy
+ literals (the (Symtab.lookup src_tab thing_identifier)) naming
+ in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
+ | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
+ |>> map_filter I;
+
+fun invoke_serializer thy abortable serializer literals reserved abs_includes
+ module_alias class instance tyco const module args naming program2 names1 =
+ let
+ val (names_class, class') =
+ activate_syntax (Code_Thingol.lookup_class naming) class;
+ val names_inst = map_filter (Code_Thingol.lookup_instance naming)
+ (Symreltab.keys instance);
+ val (names_tyco, tyco') =
+ activate_syntax (Code_Thingol.lookup_tyco naming) tyco;
+ val (names_const, (const', _)) =
+ activate_const_syntax thy literals const naming;
+ val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
+ val names2 = subtract (op =) names_hidden names1;
+ val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
+ val names_all = Graph.all_succs program3 names2;
+ val includes = abs_includes names_all;
+ val program4 = Graph.subgraph (member (op =) names_all) program3;
+ val empty_funs = filter_out (member (op =) abortable)
+ (Code_Thingol.empty_funs program3);
+ val _ = if null empty_funs then () else error ("No code equations for "
+ ^ commas (map (Sign.extern_const thy) empty_funs));
+ in
+ serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
+ (Symtab.lookup module_alias) (Symtab.lookup class')
+ (Symtab.lookup tyco') (Symtab.lookup const')
+ program4 names2
+ end;
+
+fun mount_serializer thy alt_serializer target module args naming program names =
+ let
+ val (targets, abortable) = CodeTargetData.get thy;
+ fun collapse_hierarchy target =
+ let
+ val data = case Symtab.lookup targets target
+ of SOME data => data
+ | NONE => error ("Unknown code target language: " ^ quote target);
+ in case the_serializer data
+ of Serializer _ => (I, data)
+ | Extends (super, modify) => let
+ val (modify', data') = collapse_hierarchy super
+ in (modify' #> modify naming, merge_target false target (data', data)) end
+ end;
+ val (modify, data) = collapse_hierarchy target;
+ val (serializer, _) = the_default (case the_serializer data
+ of Serializer seri => seri) alt_serializer;
+ val reserved = the_reserved data;
+ fun select_include names_all (name, (content, cs)) =
+ if null cs then SOME (name, content)
+ else if exists (fn c => case Code_Thingol.lookup_const naming c
+ of SOME name => member (op =) names_all name
+ | NONE => false) cs
+ then SOME (name, content) else NONE;
+ fun includes names_all = map_filter (select_include names_all)
+ ((Symtab.dest o the_includes) data);
+ val module_alias = the_module_alias data;
+ val { class, instance, tyco, const } = the_name_syntax data;
+ val literals = the_literals thy target;
+ in
+ invoke_serializer thy abortable serializer literals reserved
+ includes module_alias class instance tyco const module args naming (modify program) names
+ end;
+
+in
+
+fun serialize thy = mount_serializer thy NONE;
+
+fun serialize_custom thy (target_name, seri) naming program names =
+ mount_serializer thy (SOME seri) target_name NONE [] naming program names (String [])
+ |> the;
+
+end; (* local *)
+
+
+(* code presentation *)
+
+fun code_of thy target module_name cs names_stmt =
+ let
+ val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
+ in
+ string (names_stmt naming) (serialize thy target (SOME module_name) []
+ naming program names_cs)
+ end;
+
+
+(* code generation *)
+
+fun transitivly_non_empty_funs thy naming program =
+ let
+ val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.empty_funs program);
+ val names = map_filter (Code_Thingol.lookup_const naming) cs;
+ in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
+
+fun read_const_exprs thy cs =
+ let
+ val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
+ val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
+ val names4 = transitivly_non_empty_funs thy naming program;
+ val cs5 = map_filter
+ (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
+ in fold (insert (op =)) cs5 cs1 end;
+
+fun cached_program thy =
+ let
+ val (naming, program) = Code_Thingol.cached_program thy;
+ in (transitivly_non_empty_funs thy naming program, (naming, program)) end
+
+fun export_code thy cs seris =
+ let
+ val (cs', (naming, program)) = if null cs then cached_program thy
+ else Code_Thingol.consts_program thy cs;
+ fun mk_seri_dest dest = case dest
+ of NONE => compile
+ | SOME "-" => export
+ | SOME f => file (Path.explode f)
+ val _ = map (fn (((target, module), dest), args) =>
+ (mk_seri_dest dest (serialize thy target module args naming program cs'))) seris;
+ in () end;
+
+fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
+
+
(** serializer configuration **)
(* data access *)
-local
-
fun cert_class thy class =
let
val _ = AxClass.get_info thy class;
@@ -345,6 +497,8 @@
(* concrete syntax *)
+local
+
structure P = OuterParse
and K = OuterKeyword
@@ -369,166 +523,12 @@
val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
val allow_abort_cmd = gen_allow_abort Code.read_const;
-fun the_literals thy =
- let
- val (targets, _) = CodeTargetData.get thy;
- fun literals target = case Symtab.lookup targets target
- of SOME data => (case the_serializer data
- of Serializer (_, literals) => literals
- | Extends (super, _) => literals super)
- | NONE => error ("Unknown code target language: " ^ quote target);
- in literals end;
-
-
-(** serializer usage **)
-
-(* montage *)
-
-local
-
-fun activate_syntax lookup_name src_tab = Symtab.empty
- |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
- of SOME name => (SOME name,
- Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
- | NONE => (NONE, tab)) (Symtab.keys src_tab)
- |>> map_filter I;
-
-fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
- |> fold_map (fn thing_identifier => fn (tab, naming) =>
- case Code_Thingol.lookup_const naming thing_identifier
- of SOME name => let
- val (syn, naming') = Code_Printer.activate_const_syntax thy
- literals (the (Symtab.lookup src_tab thing_identifier)) naming
- in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
- | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
- |>> map_filter I;
-
-fun invoke_serializer thy abortable serializer literals reserved abs_includes
- module_alias class instance tyco const module args naming program2 names1 =
- let
- val (names_class, class') =
- activate_syntax (Code_Thingol.lookup_class naming) class;
- val names_inst = map_filter (Code_Thingol.lookup_instance naming)
- (Symreltab.keys instance);
- val (names_tyco, tyco') =
- activate_syntax (Code_Thingol.lookup_tyco naming) tyco;
- val (names_const, (const', _)) =
- activate_const_syntax thy literals const naming;
- val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
- val names2 = subtract (op =) names_hidden names1;
- val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
- val names_all = Graph.all_succs program3 names2;
- val includes = abs_includes names_all;
- val program4 = Graph.subgraph (member (op =) names_all) program3;
- val empty_funs = filter_out (member (op =) abortable)
- (Code_Thingol.empty_funs program3);
- val _ = if null empty_funs then () else error ("No code equations for "
- ^ commas (map (Sign.extern_const thy) empty_funs));
- in
- serializer module args (Code_Thingol.labelled_name thy program2) reserved includes
- (Symtab.lookup module_alias) (Symtab.lookup class')
- (Symtab.lookup tyco') (Symtab.lookup const')
- program4 names2
- end;
-
-fun mount_serializer thy alt_serializer target module args naming program names =
- let
- val (targets, abortable) = CodeTargetData.get thy;
- fun collapse_hierarchy target =
- let
- val data = case Symtab.lookup targets target
- of SOME data => data
- | NONE => error ("Unknown code target language: " ^ quote target);
- in case the_serializer data
- of Serializer _ => (I, data)
- | Extends (super, modify) => let
- val (modify', data') = collapse_hierarchy super
- in (modify' #> modify naming, merge_target false target (data', data)) end
- end;
- val (modify, data) = collapse_hierarchy target;
- val (serializer, _) = the_default (case the_serializer data
- of Serializer seri => seri) alt_serializer;
- val reserved = the_reserved data;
- fun select_include names_all (name, (content, cs)) =
- if null cs then SOME (name, content)
- else if exists (fn c => case Code_Thingol.lookup_const naming c
- of SOME name => member (op =) names_all name
- | NONE => false) cs
- then SOME (name, content) else NONE;
- fun includes names_all = map_filter (select_include names_all)
- ((Symtab.dest o the_includes) data);
- val module_alias = the_module_alias data;
- val { class, instance, tyco, const } = the_name_syntax data;
- val literals = the_literals thy target;
- in
- invoke_serializer thy abortable serializer literals reserved
- includes module_alias class instance tyco const module args naming (modify program) names
- end;
-
-in
-
-fun serialize thy = mount_serializer thy NONE;
-
-fun serialize_custom thy (target_name, seri) naming program names =
- mount_serializer thy (SOME seri) target_name NONE [] naming program names (String [])
- |> the;
-
-end; (* local *)
-
fun parse_args f args =
case Scan.read OuterLex.stopper f args
of SOME x => x
| NONE => error "Bad serializer arguments";
-(* code presentation *)
-
-fun code_of thy target module_name cs names_stmt =
- let
- val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
- in
- string (names_stmt naming) (serialize thy target (SOME module_name) []
- naming program names_cs)
- end;
-
-
-(* code generation *)
-
-fun transitivly_non_empty_funs thy naming program =
- let
- val cs = subtract (op =) (abort_allowed thy) (Code_Thingol.empty_funs program);
- val names = map_filter (Code_Thingol.lookup_const naming) cs;
- in subtract (op =) (Graph.all_preds program names) (Graph.keys program) end;
-
-fun read_const_exprs thy cs =
- let
- val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
- val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
- val names4 = transitivly_non_empty_funs thy naming program;
- val cs5 = map_filter
- (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
- in fold (insert (op =)) cs5 cs1 end;
-
-fun cached_program thy =
- let
- val (naming, program) = Code_Thingol.cached_program thy;
- in (transitivly_non_empty_funs thy naming program, (naming, program)) end
-
-fun export_code thy cs seris =
- let
- val (cs', (naming, program)) = if null cs then cached_program thy
- else Code_Thingol.consts_program thy cs;
- fun mk_seri_dest dest = case dest
- of NONE => compile
- | SOME "-" => export
- | SOME f => file (Path.explode f)
- val _ = map (fn (((target, module), dest), args) =>
- (mk_seri_dest dest (serialize thy target module args naming program cs'))) seris;
- in () end;
-
-fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
-
-
(** Isar setup **)
val (inK, module_nameK, fileK) = ("in", "module_name", "file");
--- a/src/Tools/Code_Generator.thy Tue Dec 08 18:38:08 2009 +0100
+++ b/src/Tools/Code_Generator.thy Tue Dec 08 18:40:20 2009 +0100
@@ -16,6 +16,7 @@
"~~/src/Tools/Code/code_printer.ML"
"~~/src/Tools/Code/code_target.ML"
"~~/src/Tools/Code/code_ml.ML"
+ "~~/src/Tools/Code/code_eval.ML"
"~~/src/Tools/Code/code_haskell.ML"
"~~/src/Tools/nbe.ML"
begin
@@ -23,6 +24,7 @@
setup {*
Code_Preproc.setup
#> Code_ML.setup
+ #> Code_Eval.setup
#> Code_Haskell.setup
#> Nbe.setup
*}