1open HolKernel Parse boolLib bossLib;
2
3open monadsyntax
4
5(*
6
7   Inspired by usual Haskell definition of the Cont type/monad. We
8   don't need to hide the function under a constructor, but this does
9   have the advantage of making the type more explicit.
10
11   What in Haskell is Cont r a here becomes ('a,'r) Cont, where 'r is
12   the final result type, and doesn't vary as monadic values are composed.
13   Though this is a switch, I like that the eventual result type gets to be
14   the last parameter.
15
16*)
17
18val _ = new_theory "contMonad";
19
20val _ = temp_add_monadsyntax()
21
22val _ = Datatype`Cont = Cont ((�� -> ��) -> ��)`
23
24val runCont_def = Define`runCont (Cont f) = f`
25
26val CONT_UNIT_def = Define`
27  CONT_UNIT (a:��) : (��,��)Cont = Cont (��f. f a)
28`;
29
30val CONT_BIND_def = Define`
31  CONT_BIND (m : (��,��) Cont) (f : �� -> (��,��) Cont) : (��,��) Cont =
32    Cont (��(k:��->��). runCont m (��a:��. runCont (f a) (��b:��. k b)))
33`;
34
35val _ = overload_on ("return", ``CONT_UNIT``)
36val _ = overload_on ("monad_bind", ``CONT_BIND``)
37val _ = overload_on ("monad_unitbind", ``��m1 m2. CONT_BIND m1 (K m2)``)
38
39val t6 = Q.store_thm(
40  "t6",
41  `runCont (do x <- return 2; y <- return 3; return (2 + 3) od) SUC = 6`,
42  CONV_TAC EVAL)
43
44val throw_def = Define`
45  throw (v:��) : (��,��) Cont = Cont (��k. v)
46`;
47
48val eek_example = ``
49  do
50    x <- return 2;
51    y <- throw [1;2;3];
52    z <- return 3;
53    return (x + y + z)
54  od
55``;
56
57val eek_result = save_thm(
58  "eek_result",
59  EVAL ``runCont ^eek_example (��a. [a])``);
60
61val callCC_def = Define`
62  callCC f =
63   Cont (��k. runCont (f (��a. Cont (��x. k a))) k)
64`;
65
66val runC_def = Define`
67  runC m = runCont m I
68`;
69
70val reset_def = Define`
71  (reset : (��,��)Cont -> (��,'r)Cont) = return o runC
72`;
73
74val shift_def = Define`
75  shift f = Cont (runC o f)
76`;
77
78
79val okmij1 =
80   EVAL ``do
81    (a,b) <- reset (do x <- shift (��k. return (3,4));
82                       return (x,x)
83                    od);
84    return (a + b)
85   od``
86
87(* from http://okmij.org/ftp/continuations/ContExample.hs
88
89   The k is the continuation that doubles the value, the +1 is not part
90   of the continuation because it's outside the reset, and so the result
91   below is 41
92
93*)
94val okmij_ex1 = save_thm(
95  "okmij_ex1",
96  EVAL ``runC do
97                 n <- reset (do x <- shift (��k. return (k (k 10))) ;
98                                return (2 * x)
99                             od);
100                 return (n + 1)
101              od``)
102
103val boringCC = save_thm(
104  "boringCC",
105  EVAL ``runC do x <- callCC (��k. k 11);
106     n <- return (x * 2);
107     return (n + 1)
108  od``);
109
110val doubleCC = save_thm(
111  "doubleCC",
112  EVAL ``runC do x <- callCC (��k. return (runC (k 11) + runC (k 10)));
113            n <- return (x * 2);
114            return (n + 1)
115         od``)
116
117
118
119val _ = export_theory();
120