# HG changeset patch
# User haftmann
# Date 1164187215 -3600
# Node ID b6be1d1b66c5f54b29053c73c73b7a93d55b559f
# Parent  a1937c51ed884889c4ac3d1b32a6813f469e206f
incorporated structure HOList into HOLogic

diff -r a1937c51ed88 -r b6be1d1b66c5 src/HOL/Library/MLString.thy
--- a/src/HOL/Library/MLString.thy	Wed Nov 22 10:20:12 2006 +0100
+++ b/src/HOL/Library/MLString.thy	Wed Nov 22 10:20:15 2006 +0100
@@ -48,8 +48,8 @@
   val const_STR = Sign.intern_const thy "STR";
 in
   val typ_ml_string = Type (Sign.intern_type thy "ml_string", []);
-  fun term_ml_string s = Const (const_STR, HOList.typ_string --> typ_ml_string)
-    $ HOList.term_string s
+  fun term_ml_string s = Const (const_STR, HOLogic.stringT --> typ_ml_string)
+    $ HOLogic.mk_string s
 end;
 
 end;
@@ -67,7 +67,7 @@
 
 setup {*
   CodegenSerializer.add_pretty_ml_string "SML" "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR"
-    HOList.print_char HOList.print_string "String.implode"
+    HOLogic.print_char HOLogic.print_string "String.implode"
 *}
 
 code_const explode
diff -r a1937c51ed88 -r b6be1d1b66c5 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Nov 22 10:20:12 2006 +0100
+++ b/src/HOL/List.thy	Wed Nov 22 10:20:15 2006 +0100
@@ -6,7 +6,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports PreList FunDef
+imports PreList
 begin
 
 datatype 'a list =
@@ -2542,72 +2542,11 @@
   in [("_Char", char_ast_tr), ("_String", string_ast_tr)] end;
 *}
 
-ML {*
-structure HOList =
-struct
-
-local
-  val thy = the_context ();
-in
-  val typ_string = Type (Sign.intern_type thy "string", []);
-  fun typ_list ty = Type (Sign.intern_type thy "list", [ty]);
-  fun term_list ty f [] = Const (Sign.intern_const thy "Nil", typ_list ty)
-    | term_list ty f (x::xs) = Const (Sign.intern_const thy "Cons",
-        ty --> typ_list ty --> typ_list ty) $ f x $ term_list ty f xs;
-end;
-
-fun int_of_nibble h =
-  if "0" <= h andalso h <= "9" then ord h - ord "0"
-  else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10
-  else raise Match;
-
-fun nibble_of_int i =
-  if i <= 9 then chr (ord "0" + i) else chr (ord "A" + i - 10);
-
-fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
-      let
-        fun dest_nibble (Const (s, _)) = (int_of_nibble o unprefix "List.nibble.Nibble") s
-          | dest_nibble _ = raise Match;
-      in
-        (SOME (dest_nibble c1 * 16 + dest_nibble c2)
-        handle Fail _ => NONE | Match => NONE)
-      end
-  | dest_char _ = NONE;
-
-val print_list = Pretty.enum "," "[" "]";
-
-fun print_char c =
-  let
-    val i = ord c
-  in if i < 32
-    then prefix "\\" (string_of_int i)
-    else c
-  end;
-
-val print_string = quote;
-
-fun term_string s =
-  let
-    val ty_n = Type ("List.nibble", []);
-    val ty_c = Type ("List.char", []);
-    val ty_l = Type ("List.list", [ty_c]);
-    fun mk_nib n = Const ("List.nibble.Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10)), ty_n);
-    fun mk_char c =
-      if Symbol.is_ascii c andalso Symbol.is_printable c then
-        Const ("List.char.Char", ty_n --> ty_n --> ty_c) $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16)
-      else error ("Printable ASCII character expected: " ^ quote c);
-    fun mk_string c t = Const ("List.list.Cons", ty_c --> ty_l --> ty_l)
-      $ mk_char c $ t;
-  in fold_rev mk_string (explode s) (Const ("List.list.Nil", ty_l)) end;
-
-end;
-*}
-
 print_ast_translation {*
   let
     fun dest_nib (Syntax.Constant c) =
         (case explode c of
-          ["N", "i", "b", "b", "l", "e", h] => HOList.int_of_nibble h
+          ["N", "i", "b", "b", "l", "e", h] => HOLogic.int_of_nibble h
         | _ => raise Match)
       | dest_nib _ = raise Match;
 
@@ -2646,12 +2585,7 @@
 *}
   "char" ("string")
 attach (term_of) {*
-val nibbleT = Type ("List.nibble", []);
-
-fun term_of_char c =
-  Const ("List.char.Char", nibbleT --> nibbleT --> Type ("List.char", [])) $
-    Const ("List.nibble.Nibble" ^ HOList.nibble_of_int (ord c div 16), nibbleT) $
-    Const ("List.nibble.Nibble" ^ HOList.nibble_of_int (ord c mod 16), nibbleT);
+val term_of_char = HOLogic.mk_char;
 *}
 attach (test) {*
 fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z")));
@@ -2678,10 +2612,10 @@
 code_instance list :: eq and char :: eq
   (Haskell - and -)
 
-code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+code_const "op = \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
-code_const "Code_Generator.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 code_reserved SML
@@ -2699,7 +2633,7 @@
   in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
 
 fun char_codegen thy defs gr dep thyname b t =
-  case (Option.map chr o HOList.dest_char) t 
+  case (Option.map chr o HOLogic.dest_char) t 
    of SOME c =>
         if Symbol.is_printable c
         then SOME (gr, (Pretty.quote o Pretty.str) c)
@@ -2711,11 +2645,11 @@
   Codegen.add_codegen "list_codegen" list_codegen
   #> Codegen.add_codegen "char_codegen" char_codegen
   #> CodegenSerializer.add_pretty_list "SML" "List.list.Nil" "List.list.Cons"
-       HOList.print_list NONE (7, "::")
+       (Pretty.enum "," "[" "]") NONE (7, "::")
   #> CodegenSerializer.add_pretty_list "Haskell" "List.list.Nil" "List.list.Cons"
-       HOList.print_list (SOME (HOList.print_char, HOList.print_string)) (5, ":")
+       (Pretty.enum "," "[" "]") (SOME (HOLogic.print_char, HOLogic.print_string)) (5, ":")
   #> CodegenPackage.add_appconst
-       ("List.char.Char", CodegenPackage.appgen_char HOList.dest_char)
+       ("List.char.Char", CodegenPackage.appgen_char HOLogic.dest_char)
 
 end;
 *}
diff -r a1937c51ed88 -r b6be1d1b66c5 src/HOL/ex/CodeEmbed.thy
--- a/src/HOL/ex/CodeEmbed.thy	Wed Nov 22 10:20:12 2006 +0100
+++ b/src/HOL/ex/CodeEmbed.thy	Wed Nov 22 10:20:15 2006 +0100
@@ -57,10 +57,10 @@
   val typ_sort = Type (Sign.intern_type thy "sort", []);
   val typ_typ = Type (Sign.intern_type thy "typ", []);
   val typ_term = Type (Sign.intern_type thy "term", []);
-  val term_sort = HOList.term_list typ_class MLString.term_ml_string;
+  val term_sort = HOLogic.mk_list MLString.term_ml_string typ_class;
   fun term_typ f (Type (tyco, tys)) =
-        Const (const_Type, MLString.typ_ml_string --> HOList.typ_list typ_typ --> typ_typ)
-          $ MLString.term_ml_string tyco $ HOList.term_list typ_typ (term_typ f) tys
+        Const (const_Type, MLString.typ_ml_string --> HOLogic.listT typ_typ --> typ_typ)
+          $ MLString.term_ml_string tyco $ HOLogic.mk_list (term_typ f) typ_typ tys
     | term_typ f (TFree v) =
         f v;
   fun term_term f g (Const (c, ty)) =
diff -r a1937c51ed88 -r b6be1d1b66c5 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Wed Nov 22 10:20:12 2006 +0100
+++ b/src/HOL/hologic.ML	Wed Nov 22 10:20:15 2006 +0100
@@ -88,6 +88,14 @@
   val listT : typ -> typ
   val mk_list: ('a -> term) -> typ -> 'a list -> term
   val dest_list: term -> term list
+  val charT : typ
+  val int_of_nibble : string -> int
+  val mk_char : string -> term
+  val dest_char : term -> int option
+  val print_char : string -> string
+  val stringT : typ
+  val mk_string : string -> term
+  val print_string : string -> string
 end;
 
 
@@ -343,7 +351,7 @@
 
 (* list *)
 
-fun listT T =  Type ("List.list", [T])
+fun listT T =  Type ("List.list", [T]);
 
 fun mk_list f T [] = Const ("List.list.Nil", listT T)
   | mk_list f T (x :: xs) = Const ("List.list.Cons",
@@ -354,4 +362,62 @@
   | dest_list (Const ("List.list.Cons", _) $ x $ xs) = x :: dest_list xs
   | dest_list t = raise TERM ("dest_list", [t]);
 
+
+(* char *)
+
+val nibbleT = Type ("List.nibble", []);
+val charT = Type ("List.char", []);
+
+fun int_of_nibble h =
+  if "0" <= h andalso h <= "9" then ord h - ord "0"
+  else if "A" <= h andalso h <= "F" then ord h - ord "A" + 10
+  else raise Match;
+
+fun nibble_of_int i =
+  if i <= 9 then chr (ord "0" + i) else chr (ord "A" + i - 10);
+
+fun mk_char c =
+  Const ("List.char.Char", nibbleT --> nibbleT --> charT) $
+    Const ("List.nibble.Nibble" ^ nibble_of_int (ord c div 16), nibbleT) $
+    Const ("List.nibble.Nibble" ^ nibble_of_int (ord c mod 16), nibbleT);
+
+fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
+      let
+        fun dest_nibble (Const (s, _)) = (int_of_nibble o unprefix "List.nibble.Nibble") s
+          | dest_nibble _ = raise Match;
+      in
+        (SOME (dest_nibble c1 * 16 + dest_nibble c2)
+        handle Fail _ => NONE | Match => NONE)
+      end
+  | dest_char _ = NONE;
+
+fun print_char c =
+  let
+    val i = ord c
+  in if i < 32
+    then prefix "\\" (string_of_int i)
+    else c
+  end;
+
+
+(* string *)
+
+val stringT = Type ("List.string", []);
+
+fun mk_string s =
+  let
+    val ty_n = Type ("List.nibble", []);
+    val ty_c = Type ("List.char", []);
+    val ty_l = Type ("List.list", [ty_c]);
+    fun mk_nib n = Const ("List.nibble.Nibble" ^ chr (n + (if n <= 9 then ord "0" else ord "A" - 10)), ty_n);
+    fun mk_char c =
+      if Symbol.is_ascii c andalso Symbol.is_printable c then
+        Const ("List.char.Char", ty_n --> ty_n --> ty_c) $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16)
+      else error ("Printable ASCII character expected: " ^ quote c);
+    fun mk_string c t = Const ("List.list.Cons", ty_c --> ty_l --> ty_l)
+      $ mk_char c $ t;
+  in fold_rev mk_string (explode s) (Const ("List.list.Nil", ty_l)) end;
+
+val print_string = quote;
+
 end;