slightly more standard code setup for String.literal, with explicit special case in predicate compiler
authorhaftmann
Thu Feb 05 19:44:14 2015 +0100 (2015-02-05)
changeset 59484a130ae7a9398
parent 59483 ddb73392356e
child 59485 792272e6ee6b
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
src/HOL/Code_Evaluation.thy
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/String.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
     1.1 --- a/src/HOL/Code_Evaluation.thy	Thu Feb 05 19:44:13 2015 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Thu Feb 05 19:44:14 2015 +0100
     1.3 @@ -101,18 +101,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instantiation String.literal :: term_of
     1.8 -begin
     1.9 -
    1.10 -definition
    1.11 -  "term_of s = App (Const (STR ''STR'')
    1.12 -    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
    1.13 -      Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
    1.14 -
    1.15 -instance ..
    1.16 -
    1.17 -end
    1.18 -
    1.19  declare [[code drop: rec_term case_term "HOL.equal :: term \<Rightarrow> _"
    1.20    "term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
    1.21    "term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
    1.22 @@ -124,6 +112,12 @@
    1.23        (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
    1.24    by (subst term_of_anything) rule 
    1.25  
    1.26 +lemma term_of_string [code]:
    1.27 +   "term_of s = App (Const (STR ''STR'')
    1.28 +     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
    1.29 +       Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
    1.30 +  by (subst term_of_anything) rule 
    1.31 +  
    1.32  code_printing
    1.33    constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
    1.34  | constant "term_of \<Colon> String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
     2.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Thu Feb 05 19:44:13 2015 +0100
     2.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Thu Feb 05 19:44:14 2015 +0100
     2.3 @@ -12,6 +12,14 @@
     2.4    "~~/src/HOL/ex/Records"
     2.5  begin
     2.6  
     2.7 +setup \<open>
     2.8 +let
     2.9 +  val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
    2.10 +  val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
    2.11 +    @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
    2.12 +in fold Code.del_eqns consts end
    2.13 +\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
    2.14 +
    2.15  inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    2.16  where
    2.17    empty: "sublist [] xs"
     3.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Thu Feb 05 19:44:13 2015 +0100
     3.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Thu Feb 05 19:44:14 2015 +0100
     3.3 @@ -11,6 +11,14 @@
     3.4    "~~/src/HOL/Library/RBT_Set"
     3.5  begin
     3.6  
     3.7 +setup \<open>
     3.8 +let
     3.9 +  val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
    3.10 +  val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
    3.11 +    @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
    3.12 +in fold Code.del_eqns consts end
    3.13 +\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
    3.14 +
    3.15  (* 
    3.16     The following code equations have to be deleted because they use 
    3.17     lists to implement sets in the code generetor. 
     4.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Feb 05 19:44:13 2015 +0100
     4.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Feb 05 19:44:14 2015 +0100
     4.3 @@ -624,6 +624,25 @@
     4.4  
     4.5  ML_file "Tools/Quickcheck/abstract_generators.ML"
     4.6  
     4.7 +lemma check_all_char [code]:
     4.8 +  "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
     4.9 +     f (char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y), \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
    4.10 +       (Code_Evaluation.term_of (\<lambda>x y. char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y))) (t1 ())) (t2 ()))))"
    4.11 +  by (simp add: check_all_char_def)
    4.12 +
    4.13 +lemma full_exhaustive_char_code [code]:
    4.14 +  "full_exhaustive_class.full_exhaustive f i =
    4.15 +     (if 0 < i then full_exhaustive_class.full_exhaustive
    4.16 +       (\<lambda>(a, b). full_exhaustive_class.full_exhaustive
    4.17 +          (\<lambda>(c, d).
    4.18 +            f (char_of_nat (nat_of_nibble a * 16 + nat_of_nibble c),
    4.19 +              \<lambda>_. Code_Evaluation.App (Code_Evaluation.App
    4.20 +                 (Code_Evaluation.Const (STR ''String.char.Char'')
    4.21 +                   (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
    4.22 +                      (b ())) (d ()))) (i - 1)) (i - 1)
    4.23 +    else None)"
    4.24 +  by (simp add: typerep_fun_def typerep_char_def typerep_nibble_def String.char.full_exhaustive_char.simps)
    4.25 +
    4.26  hide_fact (open) orelse_def
    4.27  no_notation orelse (infixr "orelse" 55)
    4.28  
     5.1 --- a/src/HOL/String.thy	Thu Feb 05 19:44:13 2015 +0100
     5.2 +++ b/src/HOL/String.thy	Thu Feb 05 19:44:14 2015 +0100
     5.3 @@ -319,6 +319,10 @@
     5.4      by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
     5.5  qed
     5.6  
     5.7 +lemma char_of_nat_nibble_pair [simp]:
     5.8 +  "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
     5.9 +  by (simp add: nat_of_char_Char [symmetric])
    5.10 +
    5.11  lemma inj_nat_of_char:
    5.12    "inj nat_of_char"
    5.13    by (rule inj_on_inverseI) (rule char_of_nat_of_char)
    5.14 @@ -355,12 +359,16 @@
    5.15  typedef literal = "UNIV :: string set"
    5.16    morphisms explode STR ..
    5.17  
    5.18 -setup_lifting (no_code) type_definition_literal
    5.19 +setup_lifting type_definition_literal
    5.20 +
    5.21 +lemma STR_inject' [simp]:
    5.22 +  "STR s = STR t \<longleftrightarrow> s = t"
    5.23 +  by transfer rule
    5.24  
    5.25  definition implode :: "string \<Rightarrow> String.literal"
    5.26  where
    5.27 -  "implode = STR"
    5.28 -
    5.29 +  [code del]: "implode = STR"
    5.30 +  
    5.31  instantiation literal :: size
    5.32  begin
    5.33  
    5.34 @@ -388,10 +396,6 @@
    5.35    shows "HOL.equal s s \<longleftrightarrow> True"
    5.36    by (simp add: equal)
    5.37  
    5.38 -lemma STR_inject' [simp]:
    5.39 -  "STR xs = STR ys \<longleftrightarrow> xs = ys"
    5.40 -  by (simp add: STR_inject)
    5.41 -
    5.42  lifting_update literal.lifting
    5.43  lifting_forget literal.lifting
    5.44  
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Feb 05 19:44:13 2015 +0100
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Feb 05 19:44:14 2015 +0100
     6.3 @@ -166,6 +166,8 @@
     6.4  structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
     6.5  struct
     6.6  
     6.7 +val no_constr = [@{const_name STR}];
     6.8 +
     6.9  (* general functions *)
    6.10  
    6.11  fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2))
    6.12 @@ -504,7 +506,8 @@
    6.13        | _ => false)
    6.14    in check end
    6.15  
    6.16 -val is_constr = Code.is_constr o Proof_Context.theory_of
    6.17 +fun is_constr ctxt c =
    6.18 +  not (member (op =) no_constr c) andalso Code.is_constr (Proof_Context.theory_of ctxt) c;
    6.19  
    6.20  fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
    6.21