src/HOL/Codegenerator_Test/Generate_Target_String_Literals.thy

systematic checks for bit operations and more rules on symbolic terms

(* Author: Florian Haftmann, TU Muenchen *)

section \<open>Test of target-language string literal operations\<close>

theory Generate_Target_String_Literals
imports
  "HOL-Library.Code_Test"
begin

definition computations where
  \<open>computations = (
    STR ''abc'' + STR 0x20 + STR ''def'',
    String.implode ''abc'',
    String.explode STR ''abc'',
    String.literal_of_asciis [10, 20, 30, 40, 1111, 2222, 3333],
    size (STR ''abc''),
    STR ''def'' \<le> STR ''abc'',
    STR ''abc'' < STR ''def''
  )\<close>

definition results where
  \<open>results = (
    STR ''abc def'',
    STR ''abc'',
    ''abc'',
    STR ''\<newline>'' + STR 0x14 + STR 0x1E + STR ''(W.'' + STR 0x05,
    3,
    False,
    True
  )\<close>

definition check where
  \<open>check \<longleftrightarrow> computations = results\<close>

lemma check
  by code_simp

lemma check
  by normalization

lemma check
  by eval

test_code check in OCaml
test_code check in GHC
test_code check in Scala

end