src/HOL/Library/Code_Char.thy
author haftmann
Fri, 02 Jul 2010 14:23:17 +0200
changeset 37692 7b072f0c8bde
parent 37459 7a3610dca96b
child 38857 97775f3e8722
permissions -rw-r--r--
drop unconvenient code declarations
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")
37222
4d984bc33c66 added Scala code setup
haftmann
parents: 33234
diff changeset
    15
  (Scala "Char")
24999
haftmann
parents:
diff changeset
    16
haftmann
parents:
diff changeset
    17
setup {*
37222
4d984bc33c66 added Scala code setup
haftmann
parents: 33234
diff changeset
    18
  fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 
31053
b7e1c065b6e4 confine term setup to Eval serialiser
haftmann
parents: 31046
diff changeset
    19
  #> String_Code.add_literal_list_string "Haskell"
24999
haftmann
parents:
diff changeset
    20
*}
haftmann
parents:
diff changeset
    21
haftmann
parents:
diff changeset
    22
code_instance char :: eq
haftmann
parents:
diff changeset
    23
  (Haskell -)
haftmann
parents:
diff changeset
    24
haftmann
parents:
diff changeset
    25
code_reserved SML
haftmann
parents:
diff changeset
    26
  char
haftmann
parents:
diff changeset
    27
haftmann
parents:
diff changeset
    28
code_reserved OCaml
haftmann
parents:
diff changeset
    29
  char
haftmann
parents:
diff changeset
    30
37222
4d984bc33c66 added Scala code setup
haftmann
parents: 33234
diff changeset
    31
code_reserved Scala
4d984bc33c66 added Scala code setup
haftmann
parents: 33234
diff changeset
    32
  char
4d984bc33c66 added Scala code setup
haftmann
parents: 33234
diff changeset
    33
28346
b8390cd56b8f discontinued special treatment of op = vs. eq_class.eq
haftmann
parents: 28244
diff changeset
    34
code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
24999
haftmann
parents:
diff changeset
    35
  (SML "!((_ : char) = _)")
haftmann
parents:
diff changeset
    36
  (OCaml "!((_ : char) = _)")
haftmann
parents:
diff changeset
    37
  (Haskell infixl 4 "==")
37222
4d984bc33c66 added Scala code setup
haftmann
parents: 33234
diff changeset
    38
  (Scala infixl 5 "==")
24999
haftmann
parents:
diff changeset
    39
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 31053
diff changeset
    40
code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
31046
c1969f609bf7 confine term setup to Eval serialiser
haftmann
parents: 30663
diff changeset
    41
  (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
28228
7ebe8dc06cbb evaluation using code generator
haftmann
parents: 28090
diff changeset
    42
33234
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    43
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    44
definition implode :: "string \<Rightarrow> String.literal" where
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    45
  "implode = STR"
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    46
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    47
primrec explode :: "String.literal \<Rightarrow> string" where
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    48
  "explode (STR s) = s"
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    49
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    50
lemma [code]:
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    51
  "literal_case f s = f (explode s)"
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    52
  "literal_rec f s = f (explode s)"
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    53
  by (cases s, simp)+
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    54
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    55
code_reserved SML String
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    56
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    57
code_const implode
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    58
  (SML "String.implode")
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    59
  (OCaml "failwith/ \"implode\"")
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    60
  (Haskell "_")
37459
7a3610dca96b avoid Scala legacy operations
haftmann
parents: 37222
diff changeset
    61
  (Scala "!(\"\" ++/ _)")
33234
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    62
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    63
code_const explode
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    64
  (SML "String.explode")
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    65
  (OCaml "failwith/ \"explode\"")
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    66
  (Haskell "_")
37459
7a3610dca96b avoid Scala legacy operations
haftmann
parents: 37222
diff changeset
    67
  (Scala "!(_.toList)")
33234
a5eba0447559 added implode and explode
haftmann
parents: 32657
diff changeset
    68
24999
haftmann
parents:
diff changeset
    69
end