# HG changeset patch # User haftmann # Date 1423161854 -3600 # Node ID a130ae7a93988345ac9f37f2b53acf2c92f0fc27 # Parent ddb73392356ef1356ade7e491ef8bcff7cc0ceb5 slightly more standard code setup for String.literal, with explicit special case in predicate compiler diff -r ddb73392356e -r a130ae7a9398 src/HOL/Code_Evaluation.thy --- 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 \ _" "term_of :: typerep \ _" "term_of :: term \ _" "term_of :: String.literal \ _" "term_of :: _ Predicate.pred \ term" "term_of :: _ Predicate.seq \ 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 \ integer \ term" \ (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT" | constant "term_of \ String.literal \ term" \ (Eval) "HOLogic.mk'_literal" diff -r ddb73392356e -r a130ae7a9398 src/HOL/Codegenerator_Test/Candidates.thy --- 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 \ +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 +\ -- \drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\ + inductive sublist :: "'a list \ 'a list \ bool" where empty: "sublist [] xs" diff -r ddb73392356e -r a130ae7a9398 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy --- 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 \ +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 +\ -- \drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\ + (* The following code equations have to be deleted because they use lists to implement sets in the code generetor. diff -r ddb73392356e -r a130ae7a9398 src/HOL/Quickcheck_Exhaustive.thy --- 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 (\(x, t1). check_all (\(y, t2). + f (char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y), \_. Code_Evaluation.App (Code_Evaluation.App + (Code_Evaluation.term_of (\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 + (\(a, b). full_exhaustive_class.full_exhaustive + (\(c, d). + f (char_of_nat (nat_of_nibble a * 16 + nat_of_nibble c), + \_. Code_Evaluation.App (Code_Evaluation.App + (Code_Evaluation.Const (STR ''String.char.Char'') + (TYPEREP(nibble \ nibble \ 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) diff -r ddb73392356e -r a130ae7a9398 src/HOL/String.thy --- 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 \ s = t" + by transfer rule definition implode :: "string \ String.literal" where - "implode = STR" - + [code del]: "implode = STR" + instantiation literal :: size begin @@ -388,10 +396,6 @@ shows "HOL.equal s s \ True" by (simp add: equal) -lemma STR_inject' [simp]: - "STR xs = STR ys \ xs = ys" - by (simp add: STR_inject) - lifting_update literal.lifting lifting_forget literal.lifting diff -r ddb73392356e -r a130ae7a9398 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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)