# HG changeset patch
# User haftmann
# Date 1156150959 -7200
# Node ID 0ad2f3bbd4f0383251763e52bc85f9fea911ebcc
# Parent  c4450e8967aab3d434bbd0b7c6d4a437babf939a
added some codegen examples/applications

diff -r c4450e8967aa -r 0ad2f3bbd4f0 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Aug 18 18:51:44 2006 +0200
+++ b/src/HOL/IsaMakefile	Mon Aug 21 11:02:39 2006 +0200
@@ -202,6 +202,7 @@
 $(LOG)/HOL-Library.gz: $(OUT)/HOL \
   Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
   Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
+  Library/MLString.thy \
   Library/FuncSet.thy Library/Library.thy \
   Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
   Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
@@ -638,7 +639,9 @@
 
 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy			\
   ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
-  ex/Chinese.thy ex/Classical.thy ex/Commutative_RingEx.thy			\
+  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy                           \
+  ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy			\
+  ex/Codegenerator.thy ex/Commutative_RingEx.thy               \
   ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy			\
   ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy		\
   ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy			\
diff -r c4450e8967aa -r 0ad2f3bbd4f0 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Aug 18 18:51:44 2006 +0200
+++ b/src/HOL/Library/Library.thy	Mon Aug 21 11:02:39 2006 +0200
@@ -6,6 +6,7 @@
   EfficientNat
   ExecutableSet
   ExecutableRat
+  MLString
   FuncSet
   Multiset
   NatPair
diff -r c4450e8967aa -r 0ad2f3bbd4f0 src/HOL/Library/MLString.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/MLString.thy	Mon Aug 21 11:02:39 2006 +0200
@@ -0,0 +1,88 @@
+(*  ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Monolithic strings for ML  *}
+
+theory MLString
+imports Main
+begin
+
+section {* Monolithic strings for ML *}
+
+subsection {* Motivation *}
+
+text {*
+  Strings are represented in HOL as list of characters.
+  For code generation to Haskell, this is no problem
+  since in Haskell "abc" is equivalent to ['a', 'b', 'c'].
+  On the other hand, in ML all strings have to
+  be represented as list of characters which
+  is awkward to read. This theory provides a distinguished
+  datatype for strings which then by convention
+  are serialized as monolithic ML strings. Note
+  that in Haskell these strings are identified
+  with Haskell strings.
+*}
+
+
+subsection {* Datatype of monolithic strings *}
+
+datatype ml_string = STR string
+
+consts
+  explode :: "ml_string \<Rightarrow> string"
+
+primrec
+  "explode (STR s) = s"
+
+
+subsection {* ML interface *}
+
+ML {*
+structure MLString =
+struct
+
+local
+  val thy = the_context ();
+  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
+end;
+
+end;
+*}
+
+
+subsection {* Code serialization *}
+
+code_typapp ml_string
+  ml (target_atom "string")
+  haskell (target_atom "String")
+
+code_constapp STR
+  haskell ("_")
+
+setup {*
+let
+  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;
+in 
+  CodegenPackage.add_pretty_ml_string "ml" "Nil" "Cons" "STR"
+    print_char print_string "String.implode"
+end
+*}
+
+code_constapp explode
+  ml (target_atom "String.explode")
+  haskell ("_")
+
+end
\ No newline at end of file
diff -r c4450e8967aa -r 0ad2f3bbd4f0 src/HOL/ex/CodeEmbed.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodeEmbed.thy	Mon Aug 21 11:02:39 2006 +0200
@@ -0,0 +1,91 @@
+(*  ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Embedding (a subset of) the Pure term algebra in HOL *}
+
+theory CodeEmbed
+imports Main MLString
+begin
+
+section {* Embedding (a subset of) the Pure term algebra in HOL *}
+
+
+subsection {* Definitions *}
+
+types vname = ml_string;
+types "class" = ml_string;
+types sort = "class list"
+
+datatype "typ" =
+    Type ml_string "typ list" (infix "{\<struct>}" 120)
+  | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
+
+abbreviation
+  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115)
+  "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
+  Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115)
+  "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
+
+datatype "term" =
+    Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112)
+  | Fix   vname "typ" (infix ":\<epsilon>" 112)
+  | App   "term" "term" (infixl "\<bullet>" 110)
+
+abbreviation
+  Apps :: "term \<Rightarrow> term list \<Rightarrow> term"  (infixl "{\<bullet>}" 110)
+  "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
+
+
+subsection {* ML interface *}
+
+ML {*
+structure Embed =
+struct
+
+local
+  val thy = the_context ();
+  val const_Type = Sign.intern_const thy "Type";
+  val const_TFix = Sign.intern_const thy "TFix";
+  val const_Const = Sign.intern_const thy "Const";
+  val const_App = Sign.intern_const thy "App";
+  val const_Fix = Sign.intern_const thy "Fix";
+in
+  val typ_vname = Type (Sign.intern_type thy "vname", []);
+  val typ_class = Type (Sign.intern_type thy "class", []);
+  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;
+  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
+    | term_typ f (TFree v) =
+        f v;
+  fun term_term f g (Const (c, ty)) =
+        Const (const_Const, MLString.typ_ml_string --> typ_typ --> typ_term)
+          $ MLString.term_ml_string c $ g ty
+    | term_term f g (t1 $ t2) =
+        Const (const_App, typ_term --> typ_term --> typ_term)
+          $ term_term f g t1 $ term_term f g t2
+    | term_term f g (Free v) = f v;
+end;
+
+end;
+*}
+
+
+subsection {* Code serialization setup *}
+
+code_typapp
+  "typ"  ml (target_atom "Term.typ")
+  "term" ml (target_atom "Term.term")
+
+code_constapp
+  Type  ml ("Term.Type (_, _)")
+  TFix  ml ("Term.TFree (_, _)")
+  Const ml ("Term.Const (_, _)")
+  App   ml ("Term.$ (_, _)")
+  Fix   ml ("Term.Free (_, _)")
+
+end
\ No newline at end of file
diff -r c4450e8967aa -r 0ad2f3bbd4f0 src/HOL/ex/CodeRandom.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodeRandom.thy	Mon Aug 21 11:02:39 2006 +0200
@@ -0,0 +1,175 @@
+(*  ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* A simple random engine *}
+
+theory CodeRandom
+imports CodeRevappl
+begin
+
+section {* A simple random engine *}
+
+consts
+  pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
+
+primrec
+  "pick (x#xs) n = (let (k, v) = x in
+    if n < k then v else pick xs (n - k))"
+
+lemma pick_def [code, simp]:
+  "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" by simp
+declare pick.simps [simp del, code del]
+
+typedecl randseed
+
+consts
+  random_shift :: "randseed \<Rightarrow> randseed"
+  random_seed :: "randseed \<Rightarrow> nat"
+
+definition
+  random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed"
+  "random n s = (random_seed s mod n, random_shift s)"
+
+lemma random_bound:
+  assumes "0 < n"
+  shows "fst (random n s) < n"
+proof -
+  from prems mod_less_divisor have "!!m .m mod n < n" by auto
+  then show ?thesis unfolding random_def by simp 
+qed
+
+lemma random_random_seed [simp]:
+  "snd (random n s) = random_shift s" unfolding random_def by simp
+
+definition
+  select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
+  [simp]: "select xs s =
+    s
+    \<triangleright> random (length xs)
+    \<turnstile>\<triangleright> (\<lambda>n. Pair (nth xs n))"
+  select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
+  [simp]: "select_weight xs s =
+    s
+    \<triangleright> random (foldl (op +) 0 (map fst xs))
+    \<turnstile>\<triangleright> (\<lambda>n. Pair (pick xs n))"
+
+lemma
+  "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
+proof (induct xs)
+  case Nil show ?case by (simp add: revappl random_def)
+next
+  have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
+  proof -
+    fix xs
+    fix y
+    show "map fst (map (Pair y) xs) = replicate (length xs) y"
+      by (induct xs) simp_all
+  qed
+  have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"
+  proof -
+    fix xs
+    fix n
+    assume "n < length xs"
+    then show "pick (map (Pair 1) xs) n = nth xs n"
+    proof (induct xs fixing: n)
+      case Nil then show ?case by simp
+    next
+      case (Cons x xs) show ?case
+      proof (cases n)
+        case 0 then show ?thesis by simp
+      next
+        case (Suc _)
+    from Cons have "n < length (x # xs)" by auto
+        then have "n < Suc (length xs)" by simp
+        with Suc have "n - 1 < Suc (length xs) - 1" by auto
+        with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n - 1) = xs ! (n - 1)" by auto
+        with Suc show ?thesis by auto
+      qed
+    qed
+  qed
+  have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
+  proof -
+    have replicate_append:
+      "!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"
+      by (simp add: replicate_app_Cons_same)
+    fix xs
+    show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
+    unfolding map_fst_Pair proof (induct xs)
+      case Nil show ?case by simp
+    next
+      case (Cons x xs) then show ?case unfolding replicate_append by simp
+    qed
+  qed
+  have pick_nth_random:
+    "!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"
+  proof -
+    fix s
+    fix x
+    fix xs
+    have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp
+    from pick_nth [OF bound] show
+      "pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
+  qed
+  case (Cons x xs) then show ?case
+    unfolding select_weight_def sum_length revappl_split pick_nth_random
+    by (simp add: revappl_split)
+qed
+
+definition
+  random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed"
+  "random_int k s = (let (l, s') = random (nat k) s in (int l, s'))"
+
+lemma random_nat [code]:
+  "random n s = (let (m, s') = random_int (int n) s in (nat m, s'))"
+unfolding random_int_def Let_def split_def random_def by simp
+
+ML {*
+signature RANDOM =
+sig
+  type seed = IntInf.int;
+  val seed: unit -> seed;
+  val value: IntInf.int -> seed -> IntInf.int * seed;
+end;
+
+structure Random : RANDOM =
+struct
+
+exception RANDOM;
+
+type seed = IntInf.int;
+
+local
+  val a = 16807;
+  val m = 2147483647;
+in
+  fun next s = IntInf.mod (a * s, m)
+end;
+
+local
+  val seed_ref = ref 1;
+in
+  fun seed () =
+    let
+      val r = next (!seed_ref)
+    in
+      (seed_ref := r; r)
+    end;
+end;
+
+fun value h s =
+  if h < 1 then raise RANDOM
+  else (IntInf.mod (s, h - 1), seed ());
+
+end;
+*}
+
+code_typapp randseed
+  ml (target_atom "Random.seed")
+
+code_constapp random_int
+  ml (target_atom "Random.value")
+
+code_serialize ml select select_weight (-)
+
+end
\ No newline at end of file
diff -r c4450e8967aa -r 0ad2f3bbd4f0 src/HOL/ex/CodeRevappl.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodeRevappl.thy	Mon Aug 21 11:02:39 2006 +0200
@@ -0,0 +1,36 @@
+(*  ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* Combinators for structured results *}
+
+theory CodeRevappl
+imports Main
+begin
+
+section {* Combinators for structured results *}
+
+definition
+  revappl :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<triangleright>" 55)
+  revappl_def: "x \<triangleright> f = f x"
+  revappl_snd :: "'c \<times> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<times> 'b" (infixl "|\<triangleright>" 55)
+  revappl_snd_split: "z |\<triangleright> f = (fst z , f (snd z))"
+  revappl_swamp :: "'c \<times> 'a \<Rightarrow> ('a \<Rightarrow> 'd \<times> 'b) \<Rightarrow> ('c \<times> 'd) \<times> 'b" (infixl "|\<triangleright>\<triangleright>" 55)
+  revappl_swamp_split: "z |\<triangleright>\<triangleright> f = ((fst z, fst (f (snd z))), snd (f (snd z)))"
+  revappl_uncurry :: "'c \<times> 'a \<Rightarrow> ('c \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<turnstile>\<triangleright>" 55)
+  revappl_uncurry_split: "z \<turnstile>\<triangleright> f = f (fst z) (snd z)"
+
+lemma revappl_snd_def [code]:
+  "(y, x) |\<triangleright> f = (y, f x)" unfolding revappl_snd_split by simp
+
+lemma revappl_swamp_def [code]:
+  "(y, x) |\<triangleright>\<triangleright> f = (let (z, w) = f x in ((y, z), w))" unfolding Let_def revappl_swamp_split split_def by simp
+
+lemma revappl_uncurry_def [code]:
+  "(y, x) \<turnstile>\<triangleright> f = f y x" unfolding revappl_uncurry_split by simp
+
+lemmas revappl = revappl_def revappl_snd_def revappl_swamp_def revappl_uncurry_def
+
+lemmas revappl_split = revappl_def revappl_snd_split revappl_swamp_split revappl_uncurry_split
+
+end
\ No newline at end of file
diff -r c4450e8967aa -r 0ad2f3bbd4f0 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Aug 18 18:51:44 2006 +0200
+++ b/src/HOL/ex/ROOT.ML	Mon Aug 21 11:02:39 2006 +0200
@@ -6,6 +6,9 @@
 
 no_document time_use_thy "Classpackage";
 no_document time_use_thy "Codegenerator";
+no_document time_use_thy "CodeEmbed";
+no_document time_use_thy "CodeRandom";
+no_document time_use_thy "CodeRevappl";
 
 time_use_thy "Higher_Order_Logic";
 time_use_thy "Abstract_NAT";