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