--- a/doc-src/Classes/Thy/Classes.thy Sun Jul 04 21:01:22 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy Mon Jul 05 10:47:39 2010 +0200
@@ -194,7 +194,7 @@
using our simple algebra:
*}
-instantiation %quote * :: (semigroup, semigroup) semigroup
+instantiation %quote prod :: (semigroup, semigroup) semigroup
begin
definition %quote
@@ -260,7 +260,7 @@
end %quote
-instantiation %quote * :: (monoidl, monoidl) monoidl
+instantiation %quote prod :: (monoidl, monoidl) monoidl
begin
definition %quote
@@ -297,7 +297,7 @@
end %quote
-instantiation %quote * :: (monoid, monoid) monoid
+instantiation %quote prod :: (monoid, monoid) monoid
begin
instance %quote proof
--- a/doc-src/Classes/Thy/document/Classes.tex Sun Jul 04 21:01:22 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Mon Jul 05 10:47:39 2010 +0200
@@ -286,7 +286,7 @@
%
\isatagquote
\isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
@@ -405,7 +405,7 @@
\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{definition}\isamarkupfalse%
@@ -479,7 +479,7 @@
\isanewline
\isanewline
\isacommand{instantiation}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
+\ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline
\isakeyword{begin}\isanewline
\isanewline
\isacommand{instance}\isamarkupfalse%
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Mon Jul 05 10:47:39 2010 +0200
@@ -0,0 +1,25 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* A huge collection of equations to generate code from *}
+
+theory Candidates
+imports
+ Complex_Main
+ Library
+ List_Prefix
+ "~~/src/HOL/Number_Theory/Primes"
+ "~~/src/HOL/ex/Records"
+begin
+
+inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+ empty: "sublist [] xs"
+ | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
+ | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
+
+code_pred sublist .
+
+(*avoid popular infix*)
+code_reserved SML upto
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates_Pretty.thy Mon Jul 05 10:47:39 2010 +0200
@@ -0,0 +1,10 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Generating code using pretty literals and natural number literals *}
+
+theory Candidates_Pretty
+imports Candidates Code_Char Efficient_Nat
+begin
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate.thy Mon Jul 05 10:47:39 2010 +0200
@@ -0,0 +1,15 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator *}
+
+theory Generate
+imports Candidates
+begin
+
+export_code * in SML module_name Code_Test
+ in OCaml module_name Code_Test file -
+ in Haskell file -
+ in Scala file -
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy Mon Jul 05 10:47:39 2010 +0200
@@ -0,0 +1,20 @@
+
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Pervasive test of code generator using pretty literals *}
+
+theory Generate_Pretty
+imports Candidates_Pretty
+begin
+
+lemma [code, code del]: "nat_of_char = nat_of_char" ..
+lemma [code, code del]: "char_of_nat = char_of_nat" ..
+lemma [code, code del]: "(less_eq :: char \<Rightarrow> _) = less_eq" ..
+lemma [code, code del]: "(less :: char \<Rightarrow> _) = less" ..
+
+export_code * in SML module_name Code_Test
+ in OCaml module_name Code_Test file -
+ in Haskell file -
+ in Scala file -
+
+end
--- a/src/HOL/IsaMakefile Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/IsaMakefile Mon Jul 05 10:47:39 2010 +0200
@@ -10,27 +10,28 @@
images: \
HOL \
+ HOL-Library \
HOL-Algebra \
- HOL-Base \
HOL-Boogie \
- HOL-Main \
HOL-Multivariate_Analysis \
HOL-NSA \
HOL-Nominal \
- HOL-Plain \
HOL-Probability \
HOL-Proofs \
HOL-Word \
HOL4 \
- TLA
+ TLA \
+ HOL-Base \
+ HOL-Main \
+ HOL-Plain
-#Note: keep targets sorted (except for HOL-Library and HOL-ex)
+#Note: keep targets sorted (except for HOL-ex)
test: \
- HOL-Library \
HOL-ex \
HOL-Auth \
HOL-Bali \
HOL-Boogie-Examples \
+ HOL-Codegenerator_Test \
HOL-Decision_Procs \
HOL-Hahn_Banach \
HOL-Hoare \
@@ -392,10 +393,11 @@
## HOL-Library
-HOL-Library: HOL $(LOG)/HOL-Library.gz
+HOL-Library: HOL $(OUT)/HOL-Library
-$(LOG)/HOL-Library.gz: $(OUT)/HOL $(SRC)/HOL/Tools/float_arith.ML \
- $(SRC)/Tools/float.ML Library/Abstract_Rat.thy Library/AssocList.thy \
+$(OUT)/HOL-Library: $(OUT)/HOL library.ML \
+ $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \
+ Library/Abstract_Rat.thy Library/AssocList.thy \
Library/BigO.thy Library/Binomial.thy Library/Bit.thy \
Library/Boolean_Algebra.thy Library/Cardinality.thy \
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
@@ -408,7 +410,7 @@
Library/FuncSet.thy Library/Fundamental_Theorem_Algebra.thy \
Library/Glbs.thy Library/Indicator_Function.thy \
Library/Infinite_Set.thy Library/Inner_Product.thy \
- Library/HOL_Library_ROOT.ML Library/Kleene_Algebra.thy \
+ Library/Kleene_Algebra.thy \
Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \
Library/Lattice_Syntax.thy Library/Library.thy \
Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
@@ -432,10 +434,10 @@
Library/Sum_Of_Squares/sum_of_squares.ML \
Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \
Library/While_Combinator.thy Library/Zorn.thy \
- Library/document/root.bib Library/document/root.tex \
Library/positivstellensatz.ML Library/reflection.ML \
- Library/reify_data.ML
- @$(ISABELLE_TOOL) usedir -f HOL_Library_ROOT.ML $(OUT)/HOL Library
+ Library/reify_data.ML \
+ Library/document/root.bib Library/document/root.tex
+ @$(ISABELLE_TOOL) usedir -b -f library.ML $(OUT)/HOL HOL-Library
## HOL-Hahn_Banach
@@ -632,6 +634,18 @@
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel
+## HOL-Codegenerator_Test
+
+HOL-Codegenerator_Test: HOL-Library $(LOG)/HOL-Codegenerator_Test.gz
+
+$(LOG)/HOL-Codegenerator_Test.gz: $(OUT)/HOL-Library \
+ Codegenerator_Test/ROOT.ML Codegenerator_Test/Candidates.thy \
+ Codegenerator_Test/Candidates_Pretty.thy \
+ Codegenerator_Test/Generate.thy \
+ Codegenerator_Test/Generate_Pretty.thy
+ @$(ISABELLE_TOOL) usedir -d false -g false -i false $(OUT)/HOL-Library Codegenerator_Test
+
+
## HOL-Metis_Examples
HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
@@ -976,9 +990,7 @@
ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy \
ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \
- ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy \
- ex/Codegenerator_Pretty.thy ex/Codegenerator_Pretty_Test.thy \
- ex/Codegenerator_Test.thy ex/Coherent.thy ex/Dedekind_Real.thy \
+ ex/CodegenSML_Test.thy ex/Coherent.thy ex/Dedekind_Real.thy \
ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
--- a/src/HOL/Library/Char_nat.thy Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/Library/Char_nat.thy Mon Jul 05 10:47:39 2010 +0200
@@ -53,8 +53,6 @@
"nibble_of_nat (n mod 16) = nibble_of_nat n"
unfolding nibble_of_nat_def mod_mod_trivial ..
-lemmas [code] = nibble_of_nat_norm [symmetric]
-
lemma nibble_of_nat_simps [simp]:
"nibble_of_nat 0 = Nibble0"
"nibble_of_nat 1 = Nibble1"
@@ -74,9 +72,6 @@
"nibble_of_nat 15 = NibbleF"
unfolding nibble_of_nat_def by auto
-lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
- [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc One_nat_def]
-
lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
--- a/src/HOL/Library/Fset.thy Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/Library/Fset.thy Mon Jul 05 10:47:39 2010 +0200
@@ -18,7 +18,7 @@
lemma Fset_member [simp]:
"Fset (member A) = A"
- by (rule member_inverse)
+ by (fact member_inverse)
declare member_inject [simp]
--- a/src/HOL/Library/HOL_Library_ROOT.ML Sun Jul 04 21:01:22 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"];
--- a/src/HOL/Library/Library.thy Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/Library/Library.thy Mon Jul 05 10:47:39 2010 +0200
@@ -8,18 +8,14 @@
Bit
Boolean_Algebra
Char_ord
- Code_Char_chr
- Code_Integer
Continuity
ContNotDenum
Convex
Countable
Diagonalize
Dlist
- Efficient_Nat
Enum
Eval_Witness
- Executable_Set
Float
Formal_Power_Series
Fraction_Field
--- a/src/HOL/Library/Mapping.thy Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/Library/Mapping.thy Mon Jul 05 10:47:39 2010 +0200
@@ -8,19 +8,36 @@
subsection {* Type definition and primitive operations *}
-datatype ('a, 'b) mapping = Mapping "'a \<rightharpoonup> 'b"
+typedef (open) ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
+ morphisms lookup Mapping ..
+
+lemma lookup_Mapping [simp]:
+ "lookup (Mapping f) = f"
+ by (rule Mapping_inverse) rule
+
+lemma Mapping_lookup [simp]:
+ "Mapping (lookup m) = m"
+ by (fact lookup_inverse)
+
+declare lookup_inject [simp]
+
+lemma Mapping_inject [simp]:
+ "Mapping f = Mapping g \<longleftrightarrow> f = g"
+ by (simp add: Mapping_inject)
+
+lemma mapping_eqI:
+ assumes "lookup m = lookup n"
+ shows "m = n"
+ using assms by simp
definition empty :: "('a, 'b) mapping" where
"empty = Mapping (\<lambda>_. None)"
-primrec lookup :: "('a, 'b) mapping \<Rightarrow> 'a \<rightharpoonup> 'b" where
- "lookup (Mapping f) = f"
+definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
+ "update k v m = Mapping ((lookup m)(k \<mapsto> v))"
-primrec update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
- "update k v (Mapping f) = Mapping (f (k \<mapsto> v))"
-
-primrec delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
- "delete k (Mapping f) = Mapping (f (k := None))"
+definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
+ "delete k m = Mapping ((lookup m)(k := None))"
subsection {* Derived operations *}
@@ -59,15 +76,6 @@
subsection {* Properties *}
-lemma lookup_inject [simp]:
- "lookup m = lookup n \<longleftrightarrow> m = n"
- by (cases m, cases n) simp
-
-lemma mapping_eqI:
- assumes "lookup m = lookup n"
- shows "m = n"
- using assms by simp
-
lemma keys_is_none_lookup [code_inline]:
"k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
by (auto simp add: keys_def is_none_def)
@@ -78,11 +86,11 @@
lemma lookup_update [simp]:
"lookup (update k v m) = (lookup m) (k \<mapsto> v)"
- by (cases m) simp
+ by (simp add: update_def)
lemma lookup_delete [simp]:
"lookup (delete k m) = (lookup m) (k := None)"
- by (cases m) simp
+ by (simp add: delete_def)
lemma lookup_map_entry [simp]:
"lookup (map_entry k f m) = (lookup m) (k := Option.map f (lookup m k))"
@@ -150,11 +158,11 @@
lemma is_empty_update [simp]:
"\<not> is_empty (update k v m)"
- by (cases m) (simp add: is_empty_empty)
+ by (simp add: is_empty_empty update_def)
lemma is_empty_delete:
"is_empty (delete k m) \<longleftrightarrow> is_empty m \<or> keys m = {k}"
- by (cases m) (auto simp add: is_empty_empty keys_def dom_eq_empty_conv [symmetric] simp del: dom_eq_empty_conv)
+ by (auto simp add: delete_def is_empty_def keys_def simp del: dom_eq_empty_conv)
lemma is_empty_replace [simp]:
"is_empty (replace k v m) \<longleftrightarrow> is_empty m"
@@ -268,23 +276,20 @@
by (simp add: ordered_keys_def)
-subsection {* Some technical code lemmas *}
+subsection {* Code generator setup *}
-lemma [code]:
- "mapping_case f m = f (Mapping.lookup m)"
- by (cases m) simp
+code_datatype empty update
+
+instantiation mapping :: (type, type) eq
+begin
-lemma [code]:
- "mapping_rec f m = f (Mapping.lookup m)"
- by (cases m) simp
+definition [code del]:
+ "HOL.eq m n \<longleftrightarrow> lookup m = lookup n"
-lemma [code]:
- "Nat.size (m :: (_, _) mapping) = 0"
- by (cases m) simp
+instance proof
+qed (simp add: eq_mapping_def)
-lemma [code]:
- "mapping_size f g m = 0"
- by (cases m) simp
+end
hide_const (open) empty is_empty lookup update delete ordered_keys keys size
--- a/src/HOL/Nitpick.thy Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/Nitpick.thy Mon Jul 05 10:47:39 2010 +0200
@@ -69,9 +69,6 @@
apply (erule_tac x = y in allE)
by (auto simp: mem_def)
-lemma split_def [nitpick_def]: "split f = (\<lambda>p. f (fst p) (snd p))"
-by (simp add: prod_case_unfold split_def)
-
lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
by simp
@@ -252,12 +249,12 @@
less_frac less_eq_frac of_frac
hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
word
-hide_fact (open) If_def Ex1_def split_def rtrancl_def rtranclp_def tranclp_def
- refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
- fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
- list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
- zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
- plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
- inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
+hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
+ wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
+ The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
+ nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
+ num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
+ uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def
+ less_eq_frac_def of_frac_def
end
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Mon Jul 05 10:47:39 2010 +0200
@@ -17,11 +17,11 @@
subsection {* Curry in a Hurry *}
lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
-nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
-nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
+nitpick [card = 1\<midarrow>12, expect = none]
by auto
lemma "split (curry f) = f"
@@ -61,12 +61,12 @@
by auto
lemma "split o curry = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
+nitpick [card = 1\<midarrow>12, expect = none]
apply (rule ext)+
by auto
lemma "curry o split = (\<lambda>x. x)"
-nitpick [card = 1\<midarrow>12, expect = unknown (*none*)]
+nitpick [card = 1\<midarrow>12, expect = none]
apply (rule ext)+
by auto
--- a/src/HOL/Product_Type.thy Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/Product_Type.thy Mon Jul 05 10:47:39 2010 +0200
@@ -158,6 +158,8 @@
by (simp add: Pair_def Abs_prod_inject)
qed
+declare prod.simps(2) [nitpick_simp del]
+
declare weak_case_cong [cong del]
@@ -391,7 +393,7 @@
code_const fst and snd
(Haskell "fst" and "snd")
-lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))"
+lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))"
by (simp add: expand_fun_eq split: prod.split)
lemma fst_eqD: "fst (x, y) = a ==> x = a"
--- a/src/HOL/ROOT.ML Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/ROOT.ML Mon Jul 05 10:47:39 2010 +0200
@@ -1,3 +1,4 @@
-(* Classical Higher-order Logic -- batteries included *)
+
+(* Classical Higher-order Logic *)
use_thys ["Complex_Main"];
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Jul 05 10:47:39 2010 +0200
@@ -876,6 +876,20 @@
"") ^ "."
end
+ val (skipped, the_scopes) =
+ all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
+ bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
+ finitizable_dataTs
+ val _ = if skipped > 0 then
+ print_m (fn () => "Too many scopes. Skipping " ^
+ string_of_int skipped ^ " scope" ^
+ plural_s skipped ^
+ ". (Consider using \"mono\" or \
+ \\"merge_type_vars\" to prevent this.)")
+ else
+ ()
+ val _ = scopes := the_scopes
+
fun run_batches _ _ []
(found_really_genuine, max_potential, max_genuine, donno) =
if donno > 0 andalso max_genuine > 0 then
@@ -888,7 +902,7 @@
" This suggests that the induction hypothesis might be \
\general enough to prove this subgoal."
else
- "")); "none")
+ "")); if skipped > 0 then "unknown" else "none")
else
(print_m (fn () =>
"Nitpick could not find a" ^
@@ -903,20 +917,6 @@
run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
end
- val (skipped, the_scopes) =
- all_scopes hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
- bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
- finitizable_dataTs
- val _ = if skipped > 0 then
- print_m (fn () => "Too many scopes. Skipping " ^
- string_of_int skipped ^ " scope" ^
- plural_s skipped ^
- ". (Consider using \"mono\" or \
- \\"merge_type_vars\" to prevent this.)")
- else
- ()
- val _ = scopes := the_scopes
-
val batches = batch_list batch_size (!scopes)
val outcome_code =
(run_batches 0 (length batches) batches
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Jul 05 10:47:39 2010 +0200
@@ -628,7 +628,9 @@
end
and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
cset)) =
- (case t of
+ (print_g (fn () => " \<Gamma> \<turnstile> " ^
+ Syntax.string_of_term ctxt t ^ " : _?");
+ case t of
Const (x as (s, T)) =>
(case AList.lookup (op =) consts x of
SOME M => (M, accum)
@@ -846,48 +848,54 @@
Plus => do_term t accum
| Minus => consider_general_equals mdata false x t1 t2 accum
in
- case t of
- Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
- do_quantifier x s1 T1 t1
- | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
- | @{const Trueprop} $ t1 =>
- let val (m1, accum) = do_formula sn t1 accum in
- (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
- m1), accum)
- end
- | @{const Not} $ t1 =>
- let val (m1, accum) = do_formula (negate sn) t1 accum in
- (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
- accum)
- end
- | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
- do_quantifier x s1 T1 t1
- | Const (x0 as (s0 as @{const_name Ex}, T0))
- $ (t1 as Abs (s1, T1, t1')) =>
- (case sn of
- Plus => do_quantifier x0 s1 T1 t1'
- | Minus =>
- (* FIXME: Move elsewhere *)
- do_term (@{const Not}
- $ (HOLogic.eq_const (domain_type T0) $ t1
- $ Abs (Name.uu, T1, @{const False}))) accum)
- | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
- do_equals x t1 t2
- | (t0 as Const (s0, _)) $ t1 $ t2 =>
- if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
- s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
- let
- val impl = (s0 = @{const_name "==>"} orelse
- s0 = @{const_name "op -->"})
- val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
- val (m2, accum) = do_formula sn t2 accum
- in
- (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
- accum)
- end
- else
- do_term t accum
- | _ => do_term t accum
+ (print_g (fn () => " \<Gamma> \<turnstile> " ^
+ Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^
+ string_for_sign sn ^ "?");
+ case t of
+ Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
+ do_quantifier x s1 T1 t1
+ | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
+ | @{const Trueprop} $ t1 =>
+ let val (m1, accum) = do_formula sn t1 accum in
+ (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
+ m1), accum)
+ end
+ | @{const Not} $ t1 =>
+ let val (m1, accum) = do_formula (negate sn) t1 accum in
+ (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
+ accum)
+ end
+ | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
+ do_quantifier x s1 T1 t1
+ | Const (x0 as (s0 as @{const_name Ex}, T0))
+ $ (t1 as Abs (s1, T1, t1')) =>
+ (case sn of
+ Plus => do_quantifier x0 s1 T1 t1'
+ | Minus =>
+ (* FIXME: Move elsewhere *)
+ do_term (@{const Not}
+ $ (HOLogic.eq_const (domain_type T0) $ t1
+ $ Abs (Name.uu, T1, @{const False}))) accum)
+ | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ do_equals x t1 t2
+ | Const (@{const_name Let}, _) $ t1 $ t2 =>
+ do_formula sn (betapply (t2, t1)) accum
+ | (t0 as Const (s0, _)) $ t1 $ t2 =>
+ if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
+ s0 = @{const_name "op |"} orelse
+ s0 = @{const_name "op -->"} then
+ let
+ val impl = (s0 = @{const_name "==>"} orelse
+ s0 = @{const_name "op -->"})
+ val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
+ val (m2, accum) = do_formula sn t2 accum
+ in
+ (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
+ accum)
+ end
+ else
+ do_term t accum
+ | _ => do_term t accum)
end
|> tap (fn (m, _) =>
print_g (fn () => "\<Gamma> \<turnstile> " ^
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Jul 05 10:47:39 2010 +0200
@@ -179,7 +179,8 @@
let
val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
- val T = [T1, T2] |> sort Term_Ord.typ_ord |> List.last
+ val T = if def then T1
+ else [T1, T2] |> sort (int_ord o pairself size_of_typ) |> hd
in
list_comb (Const (s0, T --> T --> body_type T0),
map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jul 05 10:47:39 2010 +0200
@@ -12,7 +12,6 @@
type hol_clause = Metis_Clauses.hol_clause
type name_pool = string Symtab.table * string Symtab.table
- val type_wrapper_name : string
val write_tptp_file :
theory -> bool -> bool -> bool -> Path.T
-> hol_clause list * hol_clause list * hol_clause list * hol_clause list
--- a/src/HOL/base.ML Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/base.ML Mon Jul 05 10:47:39 2010 +0200
@@ -1,2 +1,4 @@
-(*side-entry for HOL-Base*)
+
+(* side-entry for HOL-Base *)
+
use_thys ["HOL"];
--- a/src/HOL/ex/Codegenerator_Candidates.thy Sun Jul 04 21:01:22 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* A huge collection of equations to generate code from *}
-
-theory Codegenerator_Candidates
-imports
- Complex_Main
- AssocList
- Binomial
- "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete"
- Dlist
- Fset
- Enum
- List_Prefix
- More_List
- Nat_Infinity
- Nested_Environment
- Option_ord
- Permutation
- "~~/src/HOL/Number_Theory/Primes"
- Product_ord
- "~~/src/HOL/ex/Records"
- RBT
- SetsAndFunctions
- While_Combinator
-begin
-
-inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
- empty: "sublist [] xs"
- | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
- | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
-
-code_pred sublist .
-
-(*avoid popular infix*)
-code_reserved SML upto
-
-end
--- a/src/HOL/ex/Codegenerator_Pretty.thy Sun Jul 04 21:01:22 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Generating code using pretty literals and natural number literals *}
-
-theory Codegenerator_Pretty
-imports "~~/src/HOL/ex/Codegenerator_Candidates" Code_Char Efficient_Nat
-begin
-
-declare isnorm.simps [code del]
-
-end
--- a/src/HOL/ex/Codegenerator_Pretty_Test.thy Sun Jul 04 21:01:22 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Pervasive test of code generator using pretty literals *}
-
-theory Codegenerator_Pretty_Test
-imports Codegenerator_Pretty
-begin
-
-export_code * in SML module_name CodegenTest
- in OCaml module_name CodegenTest file -
- in Haskell file -
- in Scala file -
-
-end
--- a/src/HOL/ex/Codegenerator_Test.thy Sun Jul 04 21:01:22 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Pervasive test of code generator *}
-
-theory Codegenerator_Test
-imports Codegenerator_Candidates
-begin
-
-export_code * in SML module_name CodegenTest
- in OCaml module_name CodegenTest file -
- in Haskell file -
- in Scala file -
-
-end
--- a/src/HOL/ex/ROOT.ML Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/ex/ROOT.ML Mon Jul 05 10:47:39 2010 +0200
@@ -8,8 +8,6 @@
"Efficient_Nat_examples",
"FuncSet",
"Eval_Examples",
- "Codegenerator_Test",
- "Codegenerator_Pretty_Test",
"NormalForm"
];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/library.ML Mon Jul 05 10:47:39 2010 +0200
@@ -0,0 +1,5 @@
+
+(* Classical Higher-order Logic -- batteries included *)
+
+use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
+ "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"];
--- a/src/HOL/main.ML Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/main.ML Mon Jul 05 10:47:39 2010 +0200
@@ -1,2 +1,4 @@
-(*side-entry for HOL-Main*)
+
+(* side-entry for HOL-Main *)
+
use_thys ["Main"];
--- a/src/HOL/plain.ML Sun Jul 04 21:01:22 2010 +0200
+++ b/src/HOL/plain.ML Mon Jul 05 10:47:39 2010 +0200
@@ -1,2 +1,4 @@
-(*side-entry for HOL-Plain*)
+
+(* side-entry for HOL-Plain *)
+
use_thys ["Plain"];
--- a/src/Tools/Code/code_thingol.ML Sun Jul 04 21:01:22 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Mon Jul 05 10:47:39 2010 +0200
@@ -267,10 +267,7 @@
| purify_base "op &" = "and"
| purify_base "op |" = "or"
| purify_base "op -->" = "implies"
- | purify_base "op :" = "member"
| purify_base "op =" = "eq"
- | purify_base "*" = "product"
- | purify_base "+" = "sum"
| purify_base s = Name.desymbolize false s;
fun namify thy get_basename get_thyname name =
let
--- a/src/Tools/Code/etc/settings Sun Jul 04 21:01:22 2010 +0200
+++ b/src/Tools/Code/etc/settings Mon Jul 05 10:47:39 2010 +0200
@@ -1,2 +1,12 @@
ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+
+EXEC_GHC=$(choosefrom \
+ "$ISABELLE_HOME/contrib/ghc" \
+ "$ISABELLE_HOME/../ghc" \
+ $(type -p ghc))
+
+EXEC_OCAML=$(choosefrom \
+ "$ISABELLE_HOME/contrib/ocaml" \
+ "$ISABELLE_HOME/../ocaml" \
+ $(type -p ocaml))