src/HOL/Library/MLString.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 22849 3c41e8492ba6
permissions -rw-r--r--
tuned Proof
haftmann@20400
     1
(*  ID:         $Id$
haftmann@20400
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@20400
     3
*)
haftmann@20400
     4
wenzelm@22665
     5
header {* Monolithic strings for ML *}
haftmann@20400
     6
haftmann@20400
     7
theory MLString
haftmann@20453
     8
imports List
haftmann@20400
     9
begin
haftmann@20400
    10
haftmann@20400
    11
subsection {* Motivation *}
haftmann@20400
    12
haftmann@20400
    13
text {*
haftmann@20400
    14
  Strings are represented in HOL as list of characters.
haftmann@20400
    15
  For code generation to Haskell, this is no problem
haftmann@20400
    16
  since in Haskell "abc" is equivalent to ['a', 'b', 'c'].
haftmann@20400
    17
  On the other hand, in ML all strings have to
haftmann@20400
    18
  be represented as list of characters which
haftmann@20400
    19
  is awkward to read. This theory provides a distinguished
haftmann@20400
    20
  datatype for strings which then by convention
haftmann@22799
    21
  are serialized as monolithic ML strings.
haftmann@20400
    22
*}
haftmann@20400
    23
haftmann@20400
    24
haftmann@20400
    25
subsection {* Datatype of monolithic strings *}
haftmann@20400
    26
haftmann@20400
    27
datatype ml_string = STR string
haftmann@20400
    28
haftmann@22849
    29
lemmas [code func del] = ml_string.recs ml_string.cases
haftmann@20400
    30
haftmann@22799
    31
lemma [code func]: "size (s\<Colon>ml_string) = 0"
haftmann@22799
    32
  by (cases s) simp_all
haftmann@20400
    33
haftmann@20400
    34
subsection {* ML interface *}
haftmann@20400
    35
haftmann@20400
    36
ML {*
haftmann@20400
    37
structure MLString =
haftmann@20400
    38
struct
haftmann@20400
    39
haftmann@22520
    40
fun mk s = @{term STR} $ HOLogic.mk_string s;
haftmann@20400
    41
haftmann@20400
    42
end;
haftmann@20400
    43
*}
haftmann@20400
    44
haftmann@20400
    45
haftmann@20400
    46
subsection {* Code serialization *}
haftmann@20400
    47
haftmann@20453
    48
code_type ml_string
haftmann@21113
    49
  (SML "string")
haftmann@20400
    50
haftmann@20400
    51
setup {*
haftmann@22799
    52
let
haftmann@22799
    53
  val charr = @{const_name Char}
haftmann@22799
    54
  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
haftmann@22799
    55
    @{const_name Nibble2}, @{const_name Nibble3},
haftmann@22799
    56
    @{const_name Nibble4}, @{const_name Nibble5},
haftmann@22799
    57
    @{const_name Nibble6}, @{const_name Nibble7},
haftmann@22799
    58
    @{const_name Nibble8}, @{const_name Nibble9},
haftmann@22799
    59
    @{const_name NibbleA}, @{const_name NibbleB},
haftmann@22799
    60
    @{const_name NibbleC}, @{const_name NibbleD},
haftmann@22799
    61
    @{const_name NibbleE}, @{const_name NibbleF}];
haftmann@22799
    62
in
wenzelm@21756
    63
  CodegenSerializer.add_pretty_ml_string "SML"
haftmann@22799
    64
    charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
haftmann@22799
    65
end
haftmann@20400
    66
*}
haftmann@20400
    67
haftmann@22799
    68
code_reserved SML string
haftmann@21079
    69
haftmann@22552
    70
code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
haftmann@22552
    71
  (SML "!((_ : string) = _)")
haftmann@22016
    72
haftmann@20453
    73
end