added structure HOList
authorhaftmann
Sun Jul 23 07:20:26 2006 +0200 (2006-07-23)
changeset 2018473b5efaf2aef
parent 20183 fd546b0c8a7c
child 20185 183f08468e19
added structure HOList
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Sun Jul 23 07:19:36 2006 +0200
     1.2 +++ b/src/HOL/List.thy	Sun Jul 23 07:20:26 2006 +0200
     1.3 @@ -2630,6 +2630,19 @@
     1.4  *}
     1.5  
     1.6  ML {*
     1.7 +structure HOList =
     1.8 +struct
     1.9 +
    1.10 +local
    1.11 +  val thy = the_context ();
    1.12 +in
    1.13 +  val typ_string = Type (Sign.intern_type thy "string", []);
    1.14 +  fun typ_list ty = Type (Sign.intern_type thy "list", [ty]);
    1.15 +  fun term_list ty f [] = Const (Sign.intern_const thy "Nil", typ_list ty)
    1.16 +    | term_list ty f (x::xs) = Const (Sign.intern_const thy "Cons",
    1.17 +        ty --> typ_list ty --> typ_list ty) $ f x $ term_list ty f xs;
    1.18 +end;
    1.19 +
    1.20  fun int_of_nibble h =
    1.21    if "0" <= h andalso h <= "9" then ord h - ord "0"
    1.22    else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10
    1.23 @@ -2638,7 +2651,7 @@
    1.24  fun nibble_of_int i =
    1.25    if i <= 9 then chr (ord "0" + i) else chr (ord "A" + i - 10);
    1.26  
    1.27 -fun term_of_string s =
    1.28 +fun term_string s =
    1.29    let
    1.30      val ty_n = Type ("List.nibble", []);
    1.31      val ty_c = Type ("List.char", []);
    1.32 @@ -2651,13 +2664,15 @@
    1.33      fun mk_string c t = Const ("List.list.Cons", ty_c --> ty_l --> ty_l)
    1.34        $ mk_char c $ t;
    1.35    in fold_rev mk_string (explode s) (Const ("List.list.Nil", ty_l)) end;
    1.36 +
    1.37 +end;
    1.38  *}
    1.39  
    1.40  print_ast_translation {*
    1.41    let
    1.42      fun dest_nib (Syntax.Constant c) =
    1.43          (case explode c of
    1.44 -          ["N", "i", "b", "b", "l", "e", h] => int_of_nibble h
    1.45 +          ["N", "i", "b", "b", "l", "e", h] => HOList.int_of_nibble h
    1.46          | _ => raise Match)
    1.47        | dest_nib _ = raise Match;
    1.48  
    1.49 @@ -2691,7 +2706,7 @@
    1.50  
    1.51  fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
    1.52        let
    1.53 -        fun dest_nibble (Const (s, _)) = (int_of_nibble o unprefix "List.nibble.Nibble") s
    1.54 +        fun dest_nibble (Const (s, _)) = (HOList.int_of_nibble o unprefix "List.nibble.Nibble") s
    1.55            | dest_nibble _ = raise Match;
    1.56        in
    1.57          (SOME (dest_nibble c1 * 16 + dest_nibble c2)
    1.58 @@ -2739,8 +2754,8 @@
    1.59  
    1.60  fun term_of_char c =
    1.61    Const ("List.char.Char", nibbleT --> nibbleT --> Type ("List.char", [])) $
    1.62 -    Const ("List.nibble.Nibble" ^ nibble_of_int (ord c div 16), nibbleT) $
    1.63 -    Const ("List.nibble.Nibble" ^ nibble_of_int (ord c mod 16), nibbleT);
    1.64 +    Const ("List.nibble.Nibble" ^ HOList.nibble_of_int (ord c div 16), nibbleT) $
    1.65 +    Const ("List.nibble.Nibble" ^ HOList.nibble_of_int (ord c mod 16), nibbleT);
    1.66  *}
    1.67  attach (test) {*
    1.68  fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z")));