slightly more standard code setup for String.literal, with explicit special case in predicate compiler
--- a/src/HOL/Code_Evaluation.thy Thu Feb 05 19:44:13 2015 +0100
+++ b/src/HOL/Code_Evaluation.thy Thu Feb 05 19:44:14 2015 +0100
@@ -101,18 +101,6 @@
end
-instantiation String.literal :: term_of
-begin
-
-definition
- "term_of s = App (Const (STR ''STR'')
- (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
- Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
-
-instance ..
-
-end
-
declare [[code drop: rec_term case_term "HOL.equal :: term \<Rightarrow> _"
"term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
"term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
@@ -124,6 +112,12 @@
(Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
by (subst term_of_anything) rule
+lemma term_of_string [code]:
+ "term_of s = App (Const (STR ''STR'')
+ (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
+ Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
+ by (subst term_of_anything) rule
+
code_printing
constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
| constant "term_of \<Colon> String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
--- a/src/HOL/Codegenerator_Test/Candidates.thy Thu Feb 05 19:44:13 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Thu Feb 05 19:44:14 2015 +0100
@@ -12,6 +12,14 @@
"~~/src/HOL/ex/Records"
begin
+setup \<open>
+let
+ val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
+ val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
+ @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
+in fold Code.del_eqns consts end
+\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
+
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
where
empty: "sublist [] xs"
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Thu Feb 05 19:44:13 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Thu Feb 05 19:44:14 2015 +0100
@@ -11,6 +11,14 @@
"~~/src/HOL/Library/RBT_Set"
begin
+setup \<open>
+let
+ val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
+ val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
+ @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
+in fold Code.del_eqns consts end
+\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
+
(*
The following code equations have to be deleted because they use
lists to implement sets in the code generetor.
--- a/src/HOL/Quickcheck_Exhaustive.thy Thu Feb 05 19:44:13 2015 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Thu Feb 05 19:44:14 2015 +0100
@@ -624,6 +624,25 @@
ML_file "Tools/Quickcheck/abstract_generators.ML"
+lemma check_all_char [code]:
+ "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
+ f (char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y), \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
+ (Code_Evaluation.term_of (\<lambda>x y. char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y))) (t1 ())) (t2 ()))))"
+ by (simp add: check_all_char_def)
+
+lemma full_exhaustive_char_code [code]:
+ "full_exhaustive_class.full_exhaustive f i =
+ (if 0 < i then full_exhaustive_class.full_exhaustive
+ (\<lambda>(a, b). full_exhaustive_class.full_exhaustive
+ (\<lambda>(c, d).
+ f (char_of_nat (nat_of_nibble a * 16 + nat_of_nibble c),
+ \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
+ (Code_Evaluation.Const (STR ''String.char.Char'')
+ (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
+ (b ())) (d ()))) (i - 1)) (i - 1)
+ else None)"
+ by (simp add: typerep_fun_def typerep_char_def typerep_nibble_def String.char.full_exhaustive_char.simps)
+
hide_fact (open) orelse_def
no_notation orelse (infixr "orelse" 55)
--- a/src/HOL/String.thy Thu Feb 05 19:44:13 2015 +0100
+++ b/src/HOL/String.thy Thu Feb 05 19:44:14 2015 +0100
@@ -319,6 +319,10 @@
by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
qed
+lemma char_of_nat_nibble_pair [simp]:
+ "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
+ by (simp add: nat_of_char_Char [symmetric])
+
lemma inj_nat_of_char:
"inj nat_of_char"
by (rule inj_on_inverseI) (rule char_of_nat_of_char)
@@ -355,12 +359,16 @@
typedef literal = "UNIV :: string set"
morphisms explode STR ..
-setup_lifting (no_code) type_definition_literal
+setup_lifting type_definition_literal
+
+lemma STR_inject' [simp]:
+ "STR s = STR t \<longleftrightarrow> s = t"
+ by transfer rule
definition implode :: "string \<Rightarrow> String.literal"
where
- "implode = STR"
-
+ [code del]: "implode = STR"
+
instantiation literal :: size
begin
@@ -388,10 +396,6 @@
shows "HOL.equal s s \<longleftrightarrow> True"
by (simp add: equal)
-lemma STR_inject' [simp]:
- "STR xs = STR ys \<longleftrightarrow> xs = ys"
- by (simp add: STR_inject)
-
lifting_update literal.lifting
lifting_forget literal.lifting
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Feb 05 19:44:13 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Feb 05 19:44:14 2015 +0100
@@ -166,6 +166,8 @@
structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
struct
+val no_constr = [@{const_name STR}];
+
(* general functions *)
fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2))
@@ -504,7 +506,8 @@
| _ => false)
in check end
-val is_constr = Code.is_constr o Proof_Context.theory_of
+fun is_constr ctxt c =
+ not (member (op =) no_constr c) andalso Code.is_constr (Proof_Context.theory_of ctxt) c;
fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)