proper code_simp setup for literals
authorhaftmann
Fri Mar 08 18:56:48 2019 +0000 (3 months ago ago)
changeset 700602731278dfff9
parent 70059 ccc8e4c99520
child 70062 6a6cdf34e980
child 70063 a9e574e2cba5
proper code_simp setup for literals
src/HOL/String.thy
     1.1 --- a/src/HOL/String.thy	Fri Mar 08 21:18:58 2019 +0100
     1.2 +++ b/src/HOL/String.thy	Fri Mar 08 18:56:48 2019 +0000
     1.3 @@ -572,10 +572,28 @@
     1.4    is "map of_char"
     1.5    .
     1.6  
     1.7 +qualified lemma asciis_of_zero [simp, code]:
     1.8 +  "asciis_of_literal 0 = []"
     1.9 +  by transfer simp
    1.10 +
    1.11 +qualified lemma asciis_of_Literal [simp, code]:
    1.12 +  "asciis_of_literal (String.Literal b0 b1 b2 b3 b4 b5 b6 s) =
    1.13 +    of_char (Char b0 b1 b2 b3 b4 b5 b6 False) # asciis_of_literal s "
    1.14 +  by transfer simp
    1.15 +
    1.16  qualified lift_definition literal_of_asciis :: "integer list \<Rightarrow> String.literal"
    1.17    is "map (String.ascii_of \<circ> char_of)"
    1.18    by auto
    1.19  
    1.20 +qualified lemma literal_of_asciis_Nil [simp, code]:
    1.21 +  "literal_of_asciis [] = 0"
    1.22 +  by transfer simp
    1.23 +
    1.24 +qualified lemma literal_of_asciis_Cons [simp, code]:
    1.25 +  "literal_of_asciis (k # ks) = (case char_of k
    1.26 +    of Char b0 b1 b2 b3 b4 b5 b6 b7 \<Rightarrow> String.Literal b0 b1 b2 b3 b4 b5 b6 (literal_of_asciis ks))"
    1.27 +  by (simp add: char_of_def) (transfer, simp add: char_of_def)
    1.28 +
    1.29  qualified lemma literal_of_asciis_of_literal [simp]:
    1.30    "literal_of_asciis (asciis_of_literal s) = s"
    1.31  proof transfer
    1.32 @@ -593,9 +611,14 @@
    1.33    "String.implode cs = literal_of_asciis (map of_char cs)"
    1.34    by transfer simp
    1.35  
    1.36 -end
    1.37 +qualified lemma equal_literal [code]:
    1.38 +  "HOL.equal (String.Literal b0 b1 b2 b3 b4 b5 b6 s)
    1.39 +    (String.Literal a0 a1 a2 a3 a4 a5 a6 r)
    1.40 +    \<longleftrightarrow> (b0 \<longleftrightarrow> a0) \<and> (b1 \<longleftrightarrow> a1) \<and> (b2 \<longleftrightarrow> a2) \<and> (b3 \<longleftrightarrow> a3)
    1.41 +      \<and> (b4 \<longleftrightarrow> a4) \<and> (b5 \<longleftrightarrow> a5) \<and> (b6 \<longleftrightarrow> a6) \<and> (s = r)"
    1.42 +  by (simp add: equal)
    1.43  
    1.44 -declare [[code drop: String.literal_of_asciis String.asciis_of_literal]]
    1.45 +end
    1.46  
    1.47  
    1.48  subsubsection \<open>Technical code generation setup\<close>
    1.49 @@ -619,7 +642,7 @@
    1.50  
    1.51  end
    1.52  
    1.53 -code_reserved SML string Char
    1.54 +code_reserved SML string String Char List
    1.55  code_reserved OCaml string String Char List
    1.56  code_reserved Haskell Prelude
    1.57  code_reserved Scala string
    1.58 @@ -647,7 +670,7 @@
    1.59      and (Haskell) infixr 5 "++"
    1.60      and (Scala) infixl 7 "+"
    1.61  | constant String.literal_of_asciis \<rightharpoonup>
    1.62 -    (SML) "!(String.implode/ o map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))"
    1.63 +    (SML) "!(String.implode/ o List.map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))"
    1.64      and (OCaml) "!(let xs = _
    1.65        and chr k =
    1.66          let l = Big'_int.int'_of'_big'_int k
    1.67 @@ -658,7 +681,7 @@
    1.68      and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
    1.69      and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))"
    1.70  | constant String.asciis_of_literal \<rightharpoonup>
    1.71 -    (SML) "!(map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)"
    1.72 +    (SML) "!(List.map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)"
    1.73      and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (String.get s i) in
    1.74        if k < 128 then Big'_int.big'_int'_of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])"
    1.75      and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"