1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Code_Eval.thy Tue Sep 16 09:21:24 2008 +0200
1.3 @@ -0,0 +1,248 @@
1.4 +(* Title: HOL/Code_Eval.thy
1.5 + ID: $Id$
1.6 + Author: Florian Haftmann, TU Muenchen
1.7 +*)
1.8 +
1.9 +header {* Term evaluation using the generic code generator *}
1.10 +
1.11 +theory Code_Eval
1.12 +imports Plain RType
1.13 +begin
1.14 +
1.15 +subsection {* Term representation *}
1.16 +
1.17 +subsubsection {* Terms and class @{text term_of} *}
1.18 +
1.19 +datatype "term" = dummy_term
1.20 +
1.21 +definition
1.22 + Const :: "message_string \<Rightarrow> rtype \<Rightarrow> term"
1.23 +where
1.24 + "Const _ _ = dummy_term"
1.25 +
1.26 +definition
1.27 + App :: "term \<Rightarrow> term \<Rightarrow> term"
1.28 +where
1.29 + "App _ _ = dummy_term"
1.30 +
1.31 +code_datatype Const App
1.32 +
1.33 +class term_of = rtype +
1.34 + fixes term_of :: "'a \<Rightarrow> term"
1.35 +
1.36 +lemma term_of_anything: "term_of x \<equiv> t"
1.37 + by (rule eq_reflection) (cases "term_of x", cases t, simp)
1.38 +
1.39 +ML {*
1.40 +structure Eval =
1.41 +struct
1.42 +
1.43 +fun mk_term f g (Const (c, ty)) =
1.44 + @{term Const} $ Message_String.mk c $ g ty
1.45 + | mk_term f g (t1 $ t2) =
1.46 + @{term App} $ mk_term f g t1 $ mk_term f g t2
1.47 + | mk_term f g (Free v) = f v
1.48 + | mk_term f g (Bound i) = Bound i
1.49 + | mk_term f g (Abs (v, _, t)) = Abs (v, @{typ term}, mk_term f g t);
1.50 +
1.51 +fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t;
1.52 +
1.53 +end;
1.54 +*}
1.55 +
1.56 +
1.57 +subsubsection {* @{text term_of} instances *}
1.58 +
1.59 +setup {*
1.60 +let
1.61 + fun add_term_of_def ty vs tyco thy =
1.62 + let
1.63 + val lhs = Const (@{const_name term_of}, ty --> @{typ term})
1.64 + $ Free ("x", ty);
1.65 + val rhs = @{term "undefined \<Colon> term"};
1.66 + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
1.67 + in
1.68 + thy
1.69 + |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
1.70 + |> `(fn lthy => Syntax.check_term lthy eq)
1.71 + |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
1.72 + |> snd
1.73 + |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
1.74 + |> LocalTheory.exit
1.75 + |> ProofContext.theory_of
1.76 + end;
1.77 + fun interpretator (tyco, (raw_vs, _)) thy =
1.78 + let
1.79 + val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of};
1.80 + val constrain_sort =
1.81 + curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
1.82 + val vs = (map o apsnd) constrain_sort raw_vs;
1.83 + val ty = Type (tyco, map TFree vs);
1.84 + in
1.85 + thy
1.86 + |> RType.perhaps_add_def tyco
1.87 + |> not has_inst ? add_term_of_def ty vs tyco
1.88 + end;
1.89 +in
1.90 + Code.type_interpretation interpretator
1.91 +end
1.92 +*}
1.93 +
1.94 +setup {*
1.95 +let
1.96 + fun mk_term_of_eq ty vs tyco (c, tys) =
1.97 + let
1.98 + val t = list_comb (Const (c, tys ---> ty),
1.99 + map Free (Name.names Name.context "a" tys));
1.100 + in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term
1.101 + (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty)))
1.102 + (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))) t)
1.103 + end;
1.104 + fun prove_term_of_eq ty eq thy =
1.105 + let
1.106 + val cty = Thm.ctyp_of thy ty;
1.107 + val (arg, rhs) = pairself (Thm.cterm_of thy) eq;
1.108 + val thm = @{thm term_of_anything}
1.109 + |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs]
1.110 + |> Thm.varifyT;
1.111 + in
1.112 + thy
1.113 + |> Code.add_func thm
1.114 + end;
1.115 + fun interpretator (tyco, (raw_vs, raw_cs)) thy =
1.116 + let
1.117 + val constrain_sort =
1.118 + curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
1.119 + val vs = (map o apsnd) constrain_sort raw_vs;
1.120 + val cs = (map o apsnd o map o map_atyps)
1.121 + (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs;
1.122 + val ty = Type (tyco, map TFree vs);
1.123 + val eqs = map (mk_term_of_eq ty vs tyco) cs;
1.124 + val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
1.125 + in
1.126 + thy
1.127 + |> Code.del_funcs const
1.128 + |> fold (prove_term_of_eq ty) eqs
1.129 + end;
1.130 +in
1.131 + Code.type_interpretation interpretator
1.132 +end
1.133 +*}
1.134 +
1.135 +
1.136 +subsubsection {* Code generator setup *}
1.137 +
1.138 +lemmas [code func del] = term.recs term.cases term.size
1.139 +lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
1.140 +
1.141 +lemma [code func, code func del]: "(term_of \<Colon> rtype \<Rightarrow> term) = term_of" ..
1.142 +lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
1.143 +lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
1.144 +
1.145 +code_type "term"
1.146 + (SML "Term.term")
1.147 +
1.148 +code_const Const and App
1.149 + (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)")
1.150 +
1.151 +code_const "term_of \<Colon> message_string \<Rightarrow> term"
1.152 + (SML "Message'_String.mk")
1.153 +
1.154 +
1.155 +subsubsection {* Syntax *}
1.156 +
1.157 +print_translation {*
1.158 +let
1.159 + val term = Const ("<TERM>", dummyT);
1.160 + fun tr1' [_, _] = term;
1.161 + fun tr2' [] = term;
1.162 +in
1.163 + [(@{const_syntax Const}, tr1'),
1.164 + (@{const_syntax App}, tr1'),
1.165 + (@{const_syntax dummy_term}, tr2')]
1.166 +end
1.167 +*}
1.168 +setup {*
1.169 + Sign.declare_const [] ((Name.binding "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
1.170 + #> snd
1.171 +*}
1.172 +
1.173 +notation (output)
1.174 + rterm_of ("\<guillemotleft>_\<guillemotright>")
1.175 +
1.176 +locale rterm_syntax =
1.177 + fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>")
1.178 +
1.179 +parse_translation {*
1.180 +let
1.181 + fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
1.182 + | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
1.183 +in
1.184 + [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)]
1.185 +end
1.186 +*}
1.187 +
1.188 +setup {*
1.189 +let
1.190 + val subst_rterm_of = Eval.mk_term
1.191 + (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v))
1.192 + (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort))));
1.193 + fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t
1.194 + | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) =
1.195 + error ("illegal number of arguments for " ^ quote @{const_name rterm_of})
1.196 + | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts);
1.197 + fun subst_rterm_of'' t =
1.198 + let
1.199 + val t' = subst_rterm_of' (strip_comb t);
1.200 + in if t aconv t'
1.201 + then NONE
1.202 + else SOME t'
1.203 + end;
1.204 + fun check_rterm_of ts ctxt =
1.205 + let
1.206 + val ts' = map subst_rterm_of'' ts;
1.207 + in if exists is_some ts'
1.208 + then SOME (map2 the_default ts ts', ctxt)
1.209 + else NONE
1.210 + end;
1.211 +in
1.212 + Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of)
1.213 +end;
1.214 +*}
1.215 +
1.216 +hide const dummy_term
1.217 +hide (open) const Const App
1.218 +hide (open) const term_of
1.219 +
1.220 +
1.221 +subsection {* Evaluation setup *}
1.222 +
1.223 +ML {*
1.224 +signature EVAL =
1.225 +sig
1.226 + val mk_term: ((string * typ) -> term) -> (typ -> term) -> term -> term
1.227 + val eval_ref: (unit -> term) option ref
1.228 + val eval_term: theory -> term -> term
1.229 +end;
1.230 +
1.231 +structure Eval : EVAL =
1.232 +struct
1.233 +
1.234 +open Eval;
1.235 +
1.236 +val eval_ref = ref (NONE : (unit -> term) option);
1.237 +
1.238 +fun eval_term thy t =
1.239 + t
1.240 + |> Eval.mk_term_of (fastype_of t)
1.241 + |> (fn t => Code_ML.eval_term ("Eval.eval_ref", eval_ref) thy t [])
1.242 + |> Code.postprocess_term thy;
1.243 +
1.244 +end;
1.245 +*}
1.246 +
1.247 +setup {*
1.248 + Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
1.249 +*}
1.250 +
1.251 +end
2.1 --- a/src/HOL/Library/Code_Char.thy Tue Sep 16 09:21:22 2008 +0200
2.2 +++ b/src/HOL/Library/Code_Char.thy Tue Sep 16 09:21:24 2008 +0200
2.3 @@ -6,19 +6,11 @@
2.4 header {* Code generation of pretty characters (and strings) *}
2.5
2.6 theory Code_Char
2.7 -imports Plain "~~/src/HOL/List"
2.8 +imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
2.9 begin
2.10
2.11 declare char.recs [code func del] char.cases [code func del]
2.12
2.13 -lemma [code func]:
2.14 - "size (c\<Colon>char) = 0"
2.15 - by (cases c) simp
2.16 -
2.17 -lemma [code func]:
2.18 - "char_size (c\<Colon>char) = 0"
2.19 - by (cases c) simp
2.20 -
2.21 code_type char
2.22 (SML "char")
2.23 (OCaml "char")
2.24 @@ -43,4 +35,10 @@
2.25 (OCaml "!((_ : char) = _)")
2.26 (Haskell infixl 4 "==")
2.27
2.28 +lemma [code func, code func del]:
2.29 + "(Code_Eval.term_of :: char \<Rightarrow> term) = Code_Eval.term_of" ..
2.30 +
2.31 +code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
2.32 + (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
2.33 +
2.34 end
3.1 --- a/src/HOL/Library/Code_Index.thy Tue Sep 16 09:21:22 2008 +0200
3.2 +++ b/src/HOL/Library/Code_Index.thy Tue Sep 16 09:21:24 2008 +0200
3.3 @@ -5,7 +5,7 @@
3.4 header {* Type of indices *}
3.5
3.6 theory Code_Index
3.7 -imports Plain "~~/src/HOL/Presburger"
3.8 +imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
3.9 begin
3.10
3.11 text {*
3.12 @@ -234,7 +234,8 @@
3.13
3.14 text {* Measure function (for termination proofs) *}
3.15
3.16 -lemma [measure_function]: "is_measure nat_of_index" by (rule is_measure_trivial)
3.17 +lemma [measure_function]:
3.18 + "is_measure nat_of_index" by (rule is_measure_trivial)
3.19
3.20 subsection {* ML interface *}
3.21
3.22 @@ -278,7 +279,7 @@
3.23 unfolding div_mod_index_def by simp
3.24
3.25
3.26 -subsection {* Code serialization *}
3.27 +subsection {* Code generator setup *}
3.28
3.29 text {* Implementation of indices by bounded integers *}
3.30
3.31 @@ -333,4 +334,12 @@
3.32 (OCaml "!((_ : int) < _)")
3.33 (Haskell infix 4 "<")
3.34
3.35 +text {* Evaluation *}
3.36 +
3.37 +lemma [code func, code func del]:
3.38 + "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
3.39 +
3.40 +code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"
3.41 + (SML "HOLogic.mk'_number/ HOLogic.indexT/ (IntInf.fromInt/ _)")
3.42 +
3.43 end
4.1 --- a/src/HOL/Library/Code_Integer.thy Tue Sep 16 09:21:22 2008 +0200
4.2 +++ b/src/HOL/Library/Code_Integer.thy Tue Sep 16 09:21:24 2008 +0200
4.3 @@ -6,7 +6,7 @@
4.4 header {* Pretty integer literals for code generation *}
4.5
4.6 theory Code_Integer
4.7 -imports Plain "~~/src/HOL/Presburger"
4.8 +imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
4.9 begin
4.10
4.11 text {*
4.12 @@ -90,4 +90,12 @@
4.13 code_reserved SML IntInf
4.14 code_reserved OCaml Big_int
4.15
4.16 +text {* Evaluation *}
4.17 +
4.18 +lemma [code func, code func del]:
4.19 + "(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" ..
4.20 +
4.21 +code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"
4.22 + (SML "HOLogic.mk'_number/ HOLogic.intT")
4.23 +
4.24 end
4.25 \ No newline at end of file
5.1 --- a/src/HOL/Library/Efficient_Nat.thy Tue Sep 16 09:21:22 2008 +0200
5.2 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Sep 16 09:21:24 2008 +0200
5.3 @@ -6,7 +6,7 @@
5.4 header {* Implementation of natural numbers by target-language integers *}
5.5
5.6 theory Efficient_Nat
5.7 -imports Plain Code_Integer Code_Index
5.8 +imports Plain Code_Index Code_Integer
5.9 begin
5.10
5.11 text {*
5.12 @@ -424,6 +424,15 @@
5.13 "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" ("(_ </ _)")
5.14
5.15
5.16 +text {* Evaluation *}
5.17 +
5.18 +lemma [code func, code func del]:
5.19 + "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
5.20 +
5.21 +code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
5.22 + (SML "HOLogic.mk'_number/ HOLogic.natT")
5.23 +
5.24 +
5.25 text {* Module names *}
5.26
5.27 code_modulename SML
6.1 --- a/src/HOL/Library/Library.thy Tue Sep 16 09:21:22 2008 +0200
6.2 +++ b/src/HOL/Library/Library.thy Tue Sep 16 09:21:24 2008 +0200
6.3 @@ -19,7 +19,6 @@
6.4 Dense_Linear_Order
6.5 Efficient_Nat
6.6 Enum
6.7 - Eval
6.8 Eval_Witness
6.9 Executable_Set
6.10 "../Real/Float"
7.1 --- a/src/HOL/Library/Nested_Environment.thy Tue Sep 16 09:21:22 2008 +0200
7.2 +++ b/src/HOL/Library/Nested_Environment.thy Tue Sep 16 09:21:24 2008 +0200
7.3 @@ -6,7 +6,7 @@
7.4 header {* Nested environments *}
7.5
7.6 theory Nested_Environment
7.7 -imports Plain "~~/src/HOL/List"
7.8 +imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
7.9 begin
7.10
7.11 text {*
7.12 @@ -523,7 +523,7 @@
7.13 qed
7.14 qed
7.15
7.16 -text {* Equality of environments for code generation *}
7.17 +text {* Environments and code generation *}
7.18
7.19 lemma [code func, code func del]:
7.20 fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
7.21 @@ -567,4 +567,7 @@
7.22 of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
7.23 qed simp_all
7.24
7.25 +lemma [code func, code func del]:
7.26 + "(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Eval.term_of" ..
7.27 +
7.28 end
8.1 --- a/src/HOL/Library/RType.thy Tue Sep 16 09:21:22 2008 +0200
8.2 +++ b/src/HOL/Library/RType.thy Tue Sep 16 09:21:24 2008 +0200
8.3 @@ -6,7 +6,7 @@
8.4 header {* Reflecting Pure types into HOL *}
8.5
8.6 theory RType
8.7 -imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Message" "~~/src/HOL/Code_Index" (* import all 'special code' types *)
8.8 +imports Plain "~~/src/HOL/List" "~~/src/HOL/Library/Code_Message"
8.9 begin
8.10
8.11 datatype "rtype" = RType message_string "rtype list"
9.1 --- a/src/HOL/Main.thy Tue Sep 16 09:21:22 2008 +0200
9.2 +++ b/src/HOL/Main.thy Tue Sep 16 09:21:24 2008 +0200
9.3 @@ -5,7 +5,7 @@
9.4 header {* Main HOL *}
9.5
9.6 theory Main
9.7 -imports Plain Map Nat_Int_Bij Recdef
9.8 +imports Plain Code_Eval Map Nat_Int_Bij Recdef
9.9 begin
9.10
9.11 ML {* val HOL_proofs = ! Proofterm.proofs *}
10.1 --- a/src/HOL/ex/Codegenerator_Pretty.thy Tue Sep 16 09:21:22 2008 +0200
10.2 +++ b/src/HOL/ex/Codegenerator_Pretty.thy Tue Sep 16 09:21:24 2008 +0200
10.3 @@ -9,22 +9,13 @@
10.4 imports ExecutableContent Code_Char Efficient_Nat
10.5 begin
10.6
10.7 -setup {*
10.8 - Code.del_funcs
10.9 - (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "index"}))
10.10 - #> Code.del_funcs
10.11 - (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "char"}))
10.12 - #> Code.del_funcs
10.13 - (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "int"}))
10.14 - #> Code.del_funcs
10.15 - (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "nat"}))
10.16 -*}
10.17 +declare isnorm.simps [code func del]
10.18 +
10.19 +lemma [code func, code func del]:
10.20 + "(Code_Eval.term_of :: char \<Rightarrow> term) = Code_Eval.term_of" ..
10.21
10.22 declare char.recs [code func del]
10.23 char.cases [code func del]
10.24 - char.size [code func del]
10.25 -
10.26 -declare isnorm.simps [code func del]
10.27
10.28 ML {* (*FIXME get rid of this*)
10.29 nonfix union;
11.1 --- a/src/HOL/ex/Quickcheck.thy Tue Sep 16 09:21:22 2008 +0200
11.2 +++ b/src/HOL/ex/Quickcheck.thy Tue Sep 16 09:21:24 2008 +0200
11.3 @@ -5,7 +5,7 @@
11.4 header {* A simple counterexample generator *}
11.5
11.6 theory Quickcheck
11.7 -imports Random Eval
11.8 +imports Random Code_Eval
11.9 begin
11.10
11.11 subsection {* The @{text random} class *}
11.12 @@ -19,7 +19,7 @@
11.13 begin
11.14
11.15 definition
11.16 - "random _ = return (TYPE('a), \<lambda>u. Eval.Const (STR ''TYPE'') RTYPE('a))"
11.17 + "random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') RTYPE('a))"
11.18
11.19 instance ..
11.20
11.21 @@ -173,9 +173,9 @@
11.22 "random n = (do
11.23 (b, _) \<leftarrow> random n;
11.24 (m, t) \<leftarrow> random n;
11.25 - return (if b then (int m, \<lambda>u. Eval.App (Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))
11.26 - else (- int m, \<lambda>u. Eval.App (Eval.Const (STR ''HOL.uminus_class.uminus'') RTYPE(int \<Rightarrow> int))
11.27 - (Eval.App (Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))))
11.28 + return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))
11.29 + else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') RTYPE(int \<Rightarrow> int))
11.30 + (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') RTYPE(nat \<Rightarrow> int)) (t ()))))
11.31 done)"
11.32
11.33 instance ..
11.34 @@ -229,7 +229,7 @@
11.35 begin
11.36
11.37 definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where
11.38 - "random n = random_fun_aux RTYPE('a) RTYPE('b) (op =) Eval.term_of (random n) split_seed"
11.39 + "random n = random_fun_aux RTYPE('a) RTYPE('b) (op =) Code_Eval.term_of (random n) split_seed"
11.40
11.41 instance ..
11.42
12.1 --- a/src/HOL/ex/ROOT.ML Tue Sep 16 09:21:22 2008 +0200
12.2 +++ b/src/HOL/ex/ROOT.ML Tue Sep 16 09:21:24 2008 +0200
12.3 @@ -6,7 +6,7 @@
12.4
12.5 no_document use_thys [
12.6 "Parity",
12.7 - "Eval",
12.8 + "Code_Eval",
12.9 "State_Monad",
12.10 "Efficient_Nat_examples",
12.11 "ExecutableContent",