# HG changeset patch # User haftmann # Date 1552071408 0 # Node ID 2731278dfff973269f71c6f52f4489b033c55e75 # Parent ccc8e4c995202ffafa9e4eb15bec0ebce5eb356f proper code_simp setup for literals diff -r ccc8e4c99520 -r 2731278dfff9 src/HOL/String.thy --- a/src/HOL/String.thy Fri Mar 08 21:18:58 2019 +0100 +++ b/src/HOL/String.thy Fri Mar 08 18:56:48 2019 +0000 @@ -572,10 +572,28 @@ is "map of_char" . +qualified lemma asciis_of_zero [simp, code]: + "asciis_of_literal 0 = []" + by transfer simp + +qualified lemma asciis_of_Literal [simp, code]: + "asciis_of_literal (String.Literal b0 b1 b2 b3 b4 b5 b6 s) = + of_char (Char b0 b1 b2 b3 b4 b5 b6 False) # asciis_of_literal s " + by transfer simp + qualified lift_definition literal_of_asciis :: "integer list \ String.literal" is "map (String.ascii_of \ char_of)" by auto +qualified lemma literal_of_asciis_Nil [simp, code]: + "literal_of_asciis [] = 0" + by transfer simp + +qualified lemma literal_of_asciis_Cons [simp, code]: + "literal_of_asciis (k # ks) = (case char_of k + of Char b0 b1 b2 b3 b4 b5 b6 b7 \ String.Literal b0 b1 b2 b3 b4 b5 b6 (literal_of_asciis ks))" + by (simp add: char_of_def) (transfer, simp add: char_of_def) + qualified lemma literal_of_asciis_of_literal [simp]: "literal_of_asciis (asciis_of_literal s) = s" proof transfer @@ -593,9 +611,14 @@ "String.implode cs = literal_of_asciis (map of_char cs)" by transfer simp -end +qualified lemma equal_literal [code]: + "HOL.equal (String.Literal b0 b1 b2 b3 b4 b5 b6 s) + (String.Literal a0 a1 a2 a3 a4 a5 a6 r) + \ (b0 \ a0) \ (b1 \ a1) \ (b2 \ a2) \ (b3 \ a3) + \ (b4 \ a4) \ (b5 \ a5) \ (b6 \ a6) \ (s = r)" + by (simp add: equal) -declare [[code drop: String.literal_of_asciis String.asciis_of_literal]] +end subsubsection \Technical code generation setup\ @@ -619,7 +642,7 @@ end -code_reserved SML string Char +code_reserved SML string String Char List code_reserved OCaml string String Char List code_reserved Haskell Prelude code_reserved Scala string @@ -647,7 +670,7 @@ and (Haskell) infixr 5 "++" and (Scala) infixl 7 "+" | constant String.literal_of_asciis \ - (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\"))" + (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\"))" and (OCaml) "!(let xs = _ and chr k = let l = Big'_int.int'_of'_big'_int k @@ -658,7 +681,7 @@ and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)" and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))" | constant String.asciis_of_literal \ - (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)" + (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)" 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 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) [])" and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"