added term_of_string function
authorhaftmann
Fri Jul 21 14:49:11 2006 +0200 (2006-07-21)
changeset 2018187b2dfbf31fc
parent 20180 a751bec7cf29
child 20182 79c9ff40d760
added term_of_string function
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Fri Jul 21 14:48:35 2006 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Jul 21 14:49:11 2006 +0200
     1.3 @@ -2637,6 +2637,20 @@
     1.4  
     1.5  fun nibble_of_int i =
     1.6    if i <= 9 then chr (ord "0" + i) else chr (ord "A" + i - 10);
     1.7 +
     1.8 +fun term_of_string s =
     1.9 +  let
    1.10 +    val ty_n = Type ("List.nibble", []);
    1.11 +    val ty_c = Type ("List.char", []);
    1.12 +    val ty_l = Type ("List.list", [ty_c]);
    1.13 +    fun mk_nib n = Const ("List.nibble.Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10)), ty_n);
    1.14 +    fun mk_char c =
    1.15 +      if Symbol.is_ascii c andalso Symbol.is_printable c then
    1.16 +        Const ("List.char.Char", ty_n --> ty_n --> ty_c) $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16)
    1.17 +      else error ("Printable ASCII character expected: " ^ quote c);
    1.18 +    fun mk_string c t = Const ("List.list.Cons", ty_c --> ty_l --> ty_l)
    1.19 +      $ mk_char c $ t;
    1.20 +  in fold_rev mk_string (explode s) (Const ("List.list.Nil", ty_l)) end;
    1.21  *}
    1.22  
    1.23  print_ast_translation {*