src/HOL/Library/Code_Char.thy
author haftmann
Tue, 27 Oct 2009 15:32:20 +0100
changeset 33234 a5eba0447559
parent 32657 5f13912245ff
child 37222 4d984bc33c66
permissions -rw-r--r--
added implode and explode
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24999
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Library/Code_Char.thy
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann
haftmann
parents:
diff changeset
     3
*)
haftmann
parents:
diff changeset
     4
haftmann
parents:
diff changeset
     5
header {* Code generation of pretty characters (and strings) *}
haftmann
parents:
diff changeset
     6
haftmann
parents:
diff changeset
     7
theory Code_Char
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 31053
diff changeset
     8
imports List Code_Evaluation Main
24999
haftmann
parents:
diff changeset
     9
begin
haftmann
parents:
diff changeset
    10
haftmann
parents:
diff changeset
    11
code_type char
haftmann
parents:
diff changeset
    12
  (SML "char")
haftmann
parents:
diff changeset
    13
  (OCaml "char")
haftmann
parents:
diff changeset
    14
  (Haskell "Char")
haftmann
parents:
diff changeset
    15
haftmann
parents:
diff changeset
    16
setup {*
31053
b7e1c065b6e4 confine term setup to Eval serialiser
haftmann
parents: 31046
diff changeset
    17
  fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"] 
b7e1c065b6e4 confine term setup to Eval serialiser
haftmann
parents: 31046
diff changeset
    18
  #> String_Code.add_literal_list_string "Haskell"
24999
haftmann
parents:
diff changeset
    19
*}
haftmann
parents:
diff changeset
    20
haftmann
parents:
diff changeset
    21
code_instance char :: eq
haftmann
parents:
diff changeset
    22
  (Haskell -)
haftmann
parents:
diff changeset
    23
haftmann
parents:
diff changeset
    24
code_reserved SML
haftmann
parents:
diff changeset
    25
  char
haftmann
parents:
diff changeset
    26
haftmann
parents:
diff changeset
    27
code_reserved OCaml
haftmann
parents:
diff changeset
    28
  char
haftmann
parents:
diff changeset
    29
28346
b8390cd56b8f discontinued special treatment of op = vs. eq_class.eq
haftmann
parents: 28244
diff changeset
    30
code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
24999
haftmann
parents:
diff changeset
    31
  (SML "!((_ : char) = _)")
haftmann
parents:
diff changeset
    32
  (OCaml "!((_ : char) = _)")
haftmann
parents:
diff changeset
    33
  (Haskell infixl 4 "==")
haftmann
parents:
diff changeset
    34
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 31053
diff changeset
    35
code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
31046
c1969f609bf7 confine term setup to Eval serialiser
haftmann
parents: 30663
diff changeset
    36
  (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 28090
diff changeset
    37
33234
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    38
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    39
definition implode :: "string \<Rightarrow> String.literal" where
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    40
  "implode = STR"
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    41
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    42
primrec explode :: "String.literal \<Rightarrow> string" where
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    43
  "explode (STR s) = s"
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    44
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    45
lemma [code]:
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    46
  "literal_case f s = f (explode s)"
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    47
  "literal_rec f s = f (explode s)"
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    48
  by (cases s, simp)+
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    49
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    50
code_reserved SML String
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    51
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    52
code_const implode
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    53
  (SML "String.implode")
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    54
  (OCaml "failwith/ \"implode\"")
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    55
  (Haskell "_")
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    56
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    57
code_const explode
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    58
  (SML "String.explode")
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    59
  (OCaml "failwith/ \"explode\"")
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    60
  (Haskell "_")
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    61
24999
haftmann
parents:
diff changeset
    62
end