more explicit notion of ord value for HOL characters
authorhaftmann
Sat Sep 08 08:09:07 2018 +0000 (9 months ago)
changeset 68939bcce5967e10e
parent 68938 a0b19a163f5e
child 68940 25b431feb2e9
more explicit notion of ord value for HOL characters
src/HOL/Tools/string_syntax.ML
     1.1 --- a/src/HOL/Tools/string_syntax.ML	Sat Sep 08 08:08:28 2018 +0000
     1.2 +++ b/src/HOL/Tools/string_syntax.ML	Sat Sep 08 08:09:07 2018 +0000
     1.3 @@ -8,6 +8,7 @@
     1.4    val hex: int -> string
     1.5    val mk_bits_syntax: int -> int -> term list
     1.6    val dest_bits_syntax: term list -> int
     1.7 +  val ascii_ord_of: string -> int
     1.8    val plain_strings_of: string -> string list
     1.9    datatype character = Char of string | Ord of int
    1.10    val classify_character: int -> character
    1.11 @@ -47,14 +48,14 @@
    1.12  
    1.13  (* char *)
    1.14  
    1.15 +fun ascii_ord_of c =
    1.16 +  if Symbol.is_ascii c then ord c
    1.17 +  else if c = "\<newline>" then 10
    1.18 +  else error ("Bad character: " ^ quote c);
    1.19 +
    1.20  fun mk_char_syntax i =
    1.21    list_comb (Syntax.const @{const_syntax Char}, mk_bits_syntax 8 i);
    1.22  
    1.23 -fun mk_char_syntax' c =
    1.24 -  if Symbol.is_ascii c then mk_char_syntax (ord c)
    1.25 -  else if c = "\<newline>" then mk_char_syntax 10
    1.26 -  else error ("Bad character: " ^ quote c);
    1.27 -
    1.28  fun plain_strings_of str =
    1.29    map fst (Lexicon.explode_str (str, Position.none));
    1.30  
    1.31 @@ -84,7 +85,7 @@
    1.32        c $ char_tr [t] $ u
    1.33    | char_tr [Free (str, _)] =
    1.34        (case plain_strings_of str of
    1.35 -        [c] => mk_char_syntax' c
    1.36 +        [c] => mk_char_syntax (ascii_ord_of c)
    1.37        | _ => error ("Single character expected: " ^ str))
    1.38    | char_tr ts = raise TERM ("char_tr", ts);
    1.39  
    1.40 @@ -107,7 +108,8 @@
    1.41  
    1.42  fun mk_string_syntax [] = Syntax.const @{const_syntax Nil}
    1.43    | mk_string_syntax (c :: cs) =
    1.44 -      Syntax.const @{const_syntax Cons} $ mk_char_syntax' c $ mk_string_syntax cs;
    1.45 +      Syntax.const @{const_syntax Cons} $ mk_char_syntax (ascii_ord_of c)
    1.46 +        $ mk_string_syntax cs;
    1.47  
    1.48  fun mk_string_ast ss =
    1.49    Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},