added some codegen examples/applications
authorhaftmann
Mon Aug 21 11:02:39 2006 +0200 (2006-08-21)
changeset 204000ad2f3bbd4f0
parent 20399 c4450e8967aa
child 20401 f01ae74f29f2
added some codegen examples/applications
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/MLString.thy
src/HOL/ex/CodeEmbed.thy
src/HOL/ex/CodeRandom.thy
src/HOL/ex/CodeRevappl.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Aug 18 18:51:44 2006 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Aug 21 11:02:39 2006 +0200
     1.3 @@ -202,6 +202,7 @@
     1.4  $(LOG)/HOL-Library.gz: $(OUT)/HOL \
     1.5    Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
     1.6    Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \
     1.7 +  Library/MLString.thy \
     1.8    Library/FuncSet.thy Library/Library.thy \
     1.9    Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \
    1.10    Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
    1.11 @@ -638,7 +639,9 @@
    1.12  
    1.13  $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy			\
    1.14    ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy			\
    1.15 -  ex/Chinese.thy ex/Classical.thy ex/Commutative_RingEx.thy			\
    1.16 +  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy                           \
    1.17 +  ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy			\
    1.18 +  ex/Codegenerator.thy ex/Commutative_RingEx.thy               \
    1.19    ex/Commutative_Ring_Complete.thy ex/Guess.thy ex/Hebrew.thy			\
    1.20    ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy		\
    1.21    ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy			\
     2.1 --- a/src/HOL/Library/Library.thy	Fri Aug 18 18:51:44 2006 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Mon Aug 21 11:02:39 2006 +0200
     2.3 @@ -6,6 +6,7 @@
     2.4    EfficientNat
     2.5    ExecutableSet
     2.6    ExecutableRat
     2.7 +  MLString
     2.8    FuncSet
     2.9    Multiset
    2.10    NatPair
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/MLString.thy	Mon Aug 21 11:02:39 2006 +0200
     3.3 @@ -0,0 +1,88 @@
     3.4 +(*  ID:         $Id$
     3.5 +    Author:     Florian Haftmann, TU Muenchen
     3.6 +*)
     3.7 +
     3.8 +header {* Monolithic strings for ML  *}
     3.9 +
    3.10 +theory MLString
    3.11 +imports Main
    3.12 +begin
    3.13 +
    3.14 +section {* Monolithic strings for ML *}
    3.15 +
    3.16 +subsection {* Motivation *}
    3.17 +
    3.18 +text {*
    3.19 +  Strings are represented in HOL as list of characters.
    3.20 +  For code generation to Haskell, this is no problem
    3.21 +  since in Haskell "abc" is equivalent to ['a', 'b', 'c'].
    3.22 +  On the other hand, in ML all strings have to
    3.23 +  be represented as list of characters which
    3.24 +  is awkward to read. This theory provides a distinguished
    3.25 +  datatype for strings which then by convention
    3.26 +  are serialized as monolithic ML strings. Note
    3.27 +  that in Haskell these strings are identified
    3.28 +  with Haskell strings.
    3.29 +*}
    3.30 +
    3.31 +
    3.32 +subsection {* Datatype of monolithic strings *}
    3.33 +
    3.34 +datatype ml_string = STR string
    3.35 +
    3.36 +consts
    3.37 +  explode :: "ml_string \<Rightarrow> string"
    3.38 +
    3.39 +primrec
    3.40 +  "explode (STR s) = s"
    3.41 +
    3.42 +
    3.43 +subsection {* ML interface *}
    3.44 +
    3.45 +ML {*
    3.46 +structure MLString =
    3.47 +struct
    3.48 +
    3.49 +local
    3.50 +  val thy = the_context ();
    3.51 +  val const_STR = Sign.intern_const thy "STR";
    3.52 +in
    3.53 +  val typ_ml_string = Type (Sign.intern_type thy "ml_string", []);
    3.54 +  fun term_ml_string s = Const (const_STR, HOList.typ_string --> typ_ml_string)
    3.55 +    $ HOList.term_string s
    3.56 +end;
    3.57 +
    3.58 +end;
    3.59 +*}
    3.60 +
    3.61 +
    3.62 +subsection {* Code serialization *}
    3.63 +
    3.64 +code_typapp ml_string
    3.65 +  ml (target_atom "string")
    3.66 +  haskell (target_atom "String")
    3.67 +
    3.68 +code_constapp STR
    3.69 +  haskell ("_")
    3.70 +
    3.71 +setup {*
    3.72 +let
    3.73 +  fun print_char c =
    3.74 +    let
    3.75 +      val i = ord c
    3.76 +    in if i < 32
    3.77 +      then prefix "\\" (string_of_int i)
    3.78 +      else c
    3.79 +    end;
    3.80 +  val print_string = quote;
    3.81 +in 
    3.82 +  CodegenPackage.add_pretty_ml_string "ml" "Nil" "Cons" "STR"
    3.83 +    print_char print_string "String.implode"
    3.84 +end
    3.85 +*}
    3.86 +
    3.87 +code_constapp explode
    3.88 +  ml (target_atom "String.explode")
    3.89 +  haskell ("_")
    3.90 +
    3.91 +end
    3.92 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/ex/CodeEmbed.thy	Mon Aug 21 11:02:39 2006 +0200
     4.3 @@ -0,0 +1,91 @@
     4.4 +(*  ID:         $Id$
     4.5 +    Author:     Florian Haftmann, TU Muenchen
     4.6 +*)
     4.7 +
     4.8 +header {* Embedding (a subset of) the Pure term algebra in HOL *}
     4.9 +
    4.10 +theory CodeEmbed
    4.11 +imports Main MLString
    4.12 +begin
    4.13 +
    4.14 +section {* Embedding (a subset of) the Pure term algebra in HOL *}
    4.15 +
    4.16 +
    4.17 +subsection {* Definitions *}
    4.18 +
    4.19 +types vname = ml_string;
    4.20 +types "class" = ml_string;
    4.21 +types sort = "class list"
    4.22 +
    4.23 +datatype "typ" =
    4.24 +    Type ml_string "typ list" (infix "{\<struct>}" 120)
    4.25 +  | TFix vname sort (infix "\<Colon>\<epsilon>" 117)
    4.26 +
    4.27 +abbreviation
    4.28 +  Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115)
    4.29 +  "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]"
    4.30 +  Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115)
    4.31 +  "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty"
    4.32 +
    4.33 +datatype "term" =
    4.34 +    Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112)
    4.35 +  | Fix   vname "typ" (infix ":\<epsilon>" 112)
    4.36 +  | App   "term" "term" (infixl "\<bullet>" 110)
    4.37 +
    4.38 +abbreviation
    4.39 +  Apps :: "term \<Rightarrow> term list \<Rightarrow> term"  (infixl "{\<bullet>}" 110)
    4.40 +  "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts"
    4.41 +
    4.42 +
    4.43 +subsection {* ML interface *}
    4.44 +
    4.45 +ML {*
    4.46 +structure Embed =
    4.47 +struct
    4.48 +
    4.49 +local
    4.50 +  val thy = the_context ();
    4.51 +  val const_Type = Sign.intern_const thy "Type";
    4.52 +  val const_TFix = Sign.intern_const thy "TFix";
    4.53 +  val const_Const = Sign.intern_const thy "Const";
    4.54 +  val const_App = Sign.intern_const thy "App";
    4.55 +  val const_Fix = Sign.intern_const thy "Fix";
    4.56 +in
    4.57 +  val typ_vname = Type (Sign.intern_type thy "vname", []);
    4.58 +  val typ_class = Type (Sign.intern_type thy "class", []);
    4.59 +  val typ_sort = Type (Sign.intern_type thy "sort", []);
    4.60 +  val typ_typ = Type (Sign.intern_type thy "typ", []);
    4.61 +  val typ_term = Type (Sign.intern_type thy "term", []);
    4.62 +  val term_sort = HOList.term_list typ_class MLString.term_ml_string;
    4.63 +  fun term_typ f (Type (tyco, tys)) =
    4.64 +        Const (const_Type, MLString.typ_ml_string --> HOList.typ_list typ_typ --> typ_typ)
    4.65 +          $ MLString.term_ml_string tyco $ HOList.term_list typ_typ (term_typ f) tys
    4.66 +    | term_typ f (TFree v) =
    4.67 +        f v;
    4.68 +  fun term_term f g (Const (c, ty)) =
    4.69 +        Const (const_Const, MLString.typ_ml_string --> typ_typ --> typ_term)
    4.70 +          $ MLString.term_ml_string c $ g ty
    4.71 +    | term_term f g (t1 $ t2) =
    4.72 +        Const (const_App, typ_term --> typ_term --> typ_term)
    4.73 +          $ term_term f g t1 $ term_term f g t2
    4.74 +    | term_term f g (Free v) = f v;
    4.75 +end;
    4.76 +
    4.77 +end;
    4.78 +*}
    4.79 +
    4.80 +
    4.81 +subsection {* Code serialization setup *}
    4.82 +
    4.83 +code_typapp
    4.84 +  "typ"  ml (target_atom "Term.typ")
    4.85 +  "term" ml (target_atom "Term.term")
    4.86 +
    4.87 +code_constapp
    4.88 +  Type  ml ("Term.Type (_, _)")
    4.89 +  TFix  ml ("Term.TFree (_, _)")
    4.90 +  Const ml ("Term.Const (_, _)")
    4.91 +  App   ml ("Term.$ (_, _)")
    4.92 +  Fix   ml ("Term.Free (_, _)")
    4.93 +
    4.94 +end
    4.95 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/ex/CodeRandom.thy	Mon Aug 21 11:02:39 2006 +0200
     5.3 @@ -0,0 +1,175 @@
     5.4 +(*  ID:         $Id$
     5.5 +    Author:     Florian Haftmann, TU Muenchen
     5.6 +*)
     5.7 +
     5.8 +header {* A simple random engine *}
     5.9 +
    5.10 +theory CodeRandom
    5.11 +imports CodeRevappl
    5.12 +begin
    5.13 +
    5.14 +section {* A simple random engine *}
    5.15 +
    5.16 +consts
    5.17 +  pick :: "(nat \<times> 'a) list \<Rightarrow> nat \<Rightarrow> 'a"
    5.18 +
    5.19 +primrec
    5.20 +  "pick (x#xs) n = (let (k, v) = x in
    5.21 +    if n < k then v else pick xs (n - k))"
    5.22 +
    5.23 +lemma pick_def [code, simp]:
    5.24 +  "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))" by simp
    5.25 +declare pick.simps [simp del, code del]
    5.26 +
    5.27 +typedecl randseed
    5.28 +
    5.29 +consts
    5.30 +  random_shift :: "randseed \<Rightarrow> randseed"
    5.31 +  random_seed :: "randseed \<Rightarrow> nat"
    5.32 +
    5.33 +definition
    5.34 +  random :: "nat \<Rightarrow> randseed \<Rightarrow> nat \<times> randseed"
    5.35 +  "random n s = (random_seed s mod n, random_shift s)"
    5.36 +
    5.37 +lemma random_bound:
    5.38 +  assumes "0 < n"
    5.39 +  shows "fst (random n s) < n"
    5.40 +proof -
    5.41 +  from prems mod_less_divisor have "!!m .m mod n < n" by auto
    5.42 +  then show ?thesis unfolding random_def by simp 
    5.43 +qed
    5.44 +
    5.45 +lemma random_random_seed [simp]:
    5.46 +  "snd (random n s) = random_shift s" unfolding random_def by simp
    5.47 +
    5.48 +definition
    5.49 +  select :: "'a list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
    5.50 +  [simp]: "select xs s =
    5.51 +    s
    5.52 +    \<triangleright> random (length xs)
    5.53 +    \<turnstile>\<triangleright> (\<lambda>n. Pair (nth xs n))"
    5.54 +  select_weight :: "(nat \<times> 'a) list \<Rightarrow> randseed \<Rightarrow> 'a \<times> randseed"
    5.55 +  [simp]: "select_weight xs s =
    5.56 +    s
    5.57 +    \<triangleright> random (foldl (op +) 0 (map fst xs))
    5.58 +    \<turnstile>\<triangleright> (\<lambda>n. Pair (pick xs n))"
    5.59 +
    5.60 +lemma
    5.61 +  "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
    5.62 +proof (induct xs)
    5.63 +  case Nil show ?case by (simp add: revappl random_def)
    5.64 +next
    5.65 +  have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
    5.66 +  proof -
    5.67 +    fix xs
    5.68 +    fix y
    5.69 +    show "map fst (map (Pair y) xs) = replicate (length xs) y"
    5.70 +      by (induct xs) simp_all
    5.71 +  qed
    5.72 +  have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"
    5.73 +  proof -
    5.74 +    fix xs
    5.75 +    fix n
    5.76 +    assume "n < length xs"
    5.77 +    then show "pick (map (Pair 1) xs) n = nth xs n"
    5.78 +    proof (induct xs fixing: n)
    5.79 +      case Nil then show ?case by simp
    5.80 +    next
    5.81 +      case (Cons x xs) show ?case
    5.82 +      proof (cases n)
    5.83 +        case 0 then show ?thesis by simp
    5.84 +      next
    5.85 +        case (Suc _)
    5.86 +    from Cons have "n < length (x # xs)" by auto
    5.87 +        then have "n < Suc (length xs)" by simp
    5.88 +        with Suc have "n - 1 < Suc (length xs) - 1" by auto
    5.89 +        with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n - 1) = xs ! (n - 1)" by auto
    5.90 +        with Suc show ?thesis by auto
    5.91 +      qed
    5.92 +    qed
    5.93 +  qed
    5.94 +  have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
    5.95 +  proof -
    5.96 +    have replicate_append:
    5.97 +      "!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"
    5.98 +      by (simp add: replicate_app_Cons_same)
    5.99 +    fix xs
   5.100 +    show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
   5.101 +    unfolding map_fst_Pair proof (induct xs)
   5.102 +      case Nil show ?case by simp
   5.103 +    next
   5.104 +      case (Cons x xs) then show ?case unfolding replicate_append by simp
   5.105 +    qed
   5.106 +  qed
   5.107 +  have pick_nth_random:
   5.108 +    "!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"
   5.109 +  proof -
   5.110 +    fix s
   5.111 +    fix x
   5.112 +    fix xs
   5.113 +    have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp
   5.114 +    from pick_nth [OF bound] show
   5.115 +      "pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
   5.116 +  qed
   5.117 +  case (Cons x xs) then show ?case
   5.118 +    unfolding select_weight_def sum_length revappl_split pick_nth_random
   5.119 +    by (simp add: revappl_split)
   5.120 +qed
   5.121 +
   5.122 +definition
   5.123 +  random_int :: "int \<Rightarrow> randseed \<Rightarrow> int * randseed"
   5.124 +  "random_int k s = (let (l, s') = random (nat k) s in (int l, s'))"
   5.125 +
   5.126 +lemma random_nat [code]:
   5.127 +  "random n s = (let (m, s') = random_int (int n) s in (nat m, s'))"
   5.128 +unfolding random_int_def Let_def split_def random_def by simp
   5.129 +
   5.130 +ML {*
   5.131 +signature RANDOM =
   5.132 +sig
   5.133 +  type seed = IntInf.int;
   5.134 +  val seed: unit -> seed;
   5.135 +  val value: IntInf.int -> seed -> IntInf.int * seed;
   5.136 +end;
   5.137 +
   5.138 +structure Random : RANDOM =
   5.139 +struct
   5.140 +
   5.141 +exception RANDOM;
   5.142 +
   5.143 +type seed = IntInf.int;
   5.144 +
   5.145 +local
   5.146 +  val a = 16807;
   5.147 +  val m = 2147483647;
   5.148 +in
   5.149 +  fun next s = IntInf.mod (a * s, m)
   5.150 +end;
   5.151 +
   5.152 +local
   5.153 +  val seed_ref = ref 1;
   5.154 +in
   5.155 +  fun seed () =
   5.156 +    let
   5.157 +      val r = next (!seed_ref)
   5.158 +    in
   5.159 +      (seed_ref := r; r)
   5.160 +    end;
   5.161 +end;
   5.162 +
   5.163 +fun value h s =
   5.164 +  if h < 1 then raise RANDOM
   5.165 +  else (IntInf.mod (s, h - 1), seed ());
   5.166 +
   5.167 +end;
   5.168 +*}
   5.169 +
   5.170 +code_typapp randseed
   5.171 +  ml (target_atom "Random.seed")
   5.172 +
   5.173 +code_constapp random_int
   5.174 +  ml (target_atom "Random.value")
   5.175 +
   5.176 +code_serialize ml select select_weight (-)
   5.177 +
   5.178 +end
   5.179 \ No newline at end of file
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/ex/CodeRevappl.thy	Mon Aug 21 11:02:39 2006 +0200
     6.3 @@ -0,0 +1,36 @@
     6.4 +(*  ID:         $Id$
     6.5 +    Author:     Florian Haftmann, TU Muenchen
     6.6 +*)
     6.7 +
     6.8 +header {* Combinators for structured results *}
     6.9 +
    6.10 +theory CodeRevappl
    6.11 +imports Main
    6.12 +begin
    6.13 +
    6.14 +section {* Combinators for structured results *}
    6.15 +
    6.16 +definition
    6.17 +  revappl :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<triangleright>" 55)
    6.18 +  revappl_def: "x \<triangleright> f = f x"
    6.19 +  revappl_snd :: "'c \<times> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<times> 'b" (infixl "|\<triangleright>" 55)
    6.20 +  revappl_snd_split: "z |\<triangleright> f = (fst z , f (snd z))"
    6.21 +  revappl_swamp :: "'c \<times> 'a \<Rightarrow> ('a \<Rightarrow> 'd \<times> 'b) \<Rightarrow> ('c \<times> 'd) \<times> 'b" (infixl "|\<triangleright>\<triangleright>" 55)
    6.22 +  revappl_swamp_split: "z |\<triangleright>\<triangleright> f = ((fst z, fst (f (snd z))), snd (f (snd z)))"
    6.23 +  revappl_uncurry :: "'c \<times> 'a \<Rightarrow> ('c \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b" (infixl "\<turnstile>\<triangleright>" 55)
    6.24 +  revappl_uncurry_split: "z \<turnstile>\<triangleright> f = f (fst z) (snd z)"
    6.25 +
    6.26 +lemma revappl_snd_def [code]:
    6.27 +  "(y, x) |\<triangleright> f = (y, f x)" unfolding revappl_snd_split by simp
    6.28 +
    6.29 +lemma revappl_swamp_def [code]:
    6.30 +  "(y, x) |\<triangleright>\<triangleright> f = (let (z, w) = f x in ((y, z), w))" unfolding Let_def revappl_swamp_split split_def by simp
    6.31 +
    6.32 +lemma revappl_uncurry_def [code]:
    6.33 +  "(y, x) \<turnstile>\<triangleright> f = f y x" unfolding revappl_uncurry_split by simp
    6.34 +
    6.35 +lemmas revappl = revappl_def revappl_snd_def revappl_swamp_def revappl_uncurry_def
    6.36 +
    6.37 +lemmas revappl_split = revappl_def revappl_snd_split revappl_swamp_split revappl_uncurry_split
    6.38 +
    6.39 +end
    6.40 \ No newline at end of file
     7.1 --- a/src/HOL/ex/ROOT.ML	Fri Aug 18 18:51:44 2006 +0200
     7.2 +++ b/src/HOL/ex/ROOT.ML	Mon Aug 21 11:02:39 2006 +0200
     7.3 @@ -6,6 +6,9 @@
     7.4  
     7.5  no_document time_use_thy "Classpackage";
     7.6  no_document time_use_thy "Codegenerator";
     7.7 +no_document time_use_thy "CodeEmbed";
     7.8 +no_document time_use_thy "CodeRandom";
     7.9 +no_document time_use_thy "CodeRevappl";
    7.10  
    7.11  time_use_thy "Higher_Order_Logic";
    7.12  time_use_thy "Abstract_NAT";