1open HolKernel Parse boolTheory boolLib testutils 2open monadsyntax parmonadsyntax state_transformerTheory errorStateMonadTheory 3 4val _ = temp_remove_absyn_postprocessor "monadsyntax.transform_absyn" 5val _ = temp_remove_user_printer "monadsyntax.print_monads" 6 7val _ = set_trace "Unicode" 0 8(* interactive only: 9val _ = diemode := FailException 10*) 11 12fun udie () = die "FAILED!" 13 14val _ = tprint "Testing parsing of parmonadsyntax" 15val bind_t = prim_mk_const{Thy = "state_transformer", Name = "BIND"} 16val _ = overload_on ("monad_bind", bind_t) 17val _ = set_trace "notify type variable guesses" 0 18val t = Term`do x <- f y ; g x od` 19val _ = if same_const bind_t (#1 (strip_comb t)) then OK() 20 else udie() 21 22val _ = tprint "Testing Q.parsing of parmonadsyntax" 23val t = Parse.parse_in_context [] `do x <- f y; g x od` 24val _ = if same_const bind_t (#1 (strip_comb t)) then OK() 25 else udie() 26 27val _ = tprint "Testing Q-parsing of parmonadsyntax (TYPED-con)" 28val t = Parse.parse_in_context [] `do x <- f y; g x od : 'a -> bool # 'a` 29val _ = if same_const bind_t (#1 (strip_comb t)) then OK() 30 else udie() 31 32val _ = Parse.current_backend := PPBackEnd.vt100_terminal 33fun tpp' (s,expected) = 34 testutils.tpp_expected { 35 input = s, output = expected, 36 testf = fn s => "Testing (coloured-)printing of `"^s^"`" 37 } 38 39fun bound s = "\^[[0;32m" ^ s ^ "\^[[0m" 40fun free s = "\^[[0;1;34m" ^ s ^ "\^[[0m" 41val concat = String.concat 42 43val bx = bound "x" 44val fy = free "y" 45val fp = free "p" 46val fx = free "x" 47 48val monadtpp_test1 = 49 ("do x <- f y; g x od", 50 concat ["do ", bx, " <- ", free "f", " ", fy, "; ", free "g", " ", 51 bx, " od"]) 52val monadtpp_test2 = 53 ("do m1; m2 od", 54 concat ["do ", free "m1", "; ", free "m2", " od"]) 55 56val monadtpp_test3 = 57 ("do x <- m1; y <- m2; \ 58 \if my_very_long_guard then m3 else do a <- very_long_monad1; \ 59 \b <- very_long_monad2; superLongFinalMonad long_arg od od", 60 String.concat [ 61 "do\n ", 62 bx, " <- ", free "m1", ";\n ", 63 bound "y", " <- ", free "m2", ";\n ", 64 "if ", free "my_very_long_guard", " then ", free "m3", "\n ", (* 2 *) 65 "else\n ", 66 "do\n ", (* 6 *) 67 bound "a", " <- ", free "very_long_monad1", ";\n ", (* 6 *) 68 bound "b", " <- ", free "very_long_monad2", ";\n ", (* 6 *) 69 free "superLongFinalMonad", " ", free "long_arg", "\n ", (* 4 *) 70 "od\n", (* 0 *) 71 "od"]) 72 73val monadtpp_test4 = 74 ("do (x:��) <- f (x:��); g x; od", 75 String.concat [ 76 "do ", bx, " <- ", free "f", " ", free "x", "; ", 77 free "g", " ", bx, " od" 78 ]) 79 80val _ = app tpp' [monadtpp_test1, monadtpp_test2, monadtpp_test3, 81 monadtpp_test4] 82 83val _ = clear_overloads_on "monad_bind" 84 85val _ = temp_remove_absyn_postprocessor "parmonadsyntax.transform_absyn" 86val _ = temp_remove_user_printer "parmonadsyntax.print_monads" 87 88val _ = temp_add_user_printer ("monadsyntax.print_monads", genvar alpha, 89 monadsyntax.print_monads) 90val _ = temp_add_absyn_postprocessor ("monadsyntax.transform_absyn", 91 monadsyntax.transform_absyn) 92 93val _ = monadsyntax.enable_monad "option" 94 95val _ = unicode_off (raw_backend (trace ("types", 1) testutils.tpp)) 96 "do (x :num) <- (s :num option); SOME (x + (1 :num)) od" 97 98val _ = tprint "Testing monadsyntax parse of OPTION_BIND" 99val t = ``do x <- opt ; SOME (x + 1) od`` 100val (f, args) = strip_comb t 101val _ = if same_const f ``option$OPTION_BIND`` andalso 102 hd args ~~ mk_var("opt", ``:num option``) andalso 103 hd (tl args) ~~ ``\x:num. SOME (x + 1)`` 104 then OK() else udie () 105 106val _ = tprint "Testing monadsyntax parse of OPTION_IGNORE_BIND" 107val t = ``do SOME 3 ; SOME 4 od`` 108val (f, args) = strip_comb t 109val _ = if same_const f ``option$OPTION_IGNORE_BIND`` andalso 110 hd args ~~ ``SOME 3`` andalso 111 hd (tl args) ~~ ``SOME 4`` 112 then OK() else udie() 113 114val _ = tprint "Testing parse of mlet in option monad" 115val t = ``do mlet x <- y; SOME (x + 1) od`` 116val (f, args) = strip_comb t 117val _ = if same_const f boolSyntax.let_tm andalso 118 hd args ~~ ``\x. SOME (x + 1)`` andalso 119 hd (tl args) ~~ ``y : num`` 120 then OK() else udie() 121 122val _ = tprint "Testing parse of mlet in option monad (after bind)" 123val t = ``do y <- z; mlet x <- y; SOME (x + 1) od`` 124val (f, args) = strip_comb t 125val _ = if same_const f ``option$OPTION_BIND`` andalso 126 hd args ~~ ``z : num option`` andalso 127 hd (tl args) ~~ ``\y. let x = y in SOME (x + 1)`` 128 then OK() else udie() 129 130val _ = tprint "Testing parse of mlet arrow in option monad" 131val t = ``do x <<- y; SOME (x + 1) od`` 132val (f, args) = strip_comb t 133val _ = if same_const f boolSyntax.let_tm andalso 134 hd args ~~ ``\x. SOME (x + 1)`` andalso 135 hd (tl args) ~~ ``y : num`` 136 then OK() else udie() 137 138val _ = tprint "Testing parse of mlet arrow in option monad (after bind)" 139val t = ``do y <- z; x <<- y; SOME (x + 1) od`` 140val (f, args) = strip_comb t 141val _ = if same_const f ``option$OPTION_BIND`` andalso 142 hd args ~~ ``z : num option`` andalso 143 hd (tl args) ~~ ``\y. let x = y in SOME (x + 1)`` 144 then OK() else udie() 145 146val mlettpp_test1 = 147 ("do mlet (x:��) <- f (x:��); g x; od", 148 String.concat [ 149 "let ", bx, " = ", free "f", " ", free "x", " in ", 150 free "g", " ", bx 151 ]) 152 153val mlettpp_test2 = 154 ("do (x:��) <<- f (x:��); g x; od", 155 String.concat [ 156 "let ", bx, " = ", free "f", " ", free "x", " in ", 157 free "g", " ", bx 158 ]) 159 160val mlettpp_test3 = 161 ("do a <- b; (x:��) <<- f (x:��); g x; od", 162 String.concat [ 163 "do ", bound "a", " <- ", free "b", "; ", 164 bound "x", " <<- ", free "f", " ", free "x", "; ", 165 free "g", " ", bx, " od" 166 ]) 167 168val mlettpp_test4 = 169 ("do a <- b; let x = f x in g x; od", 170 String.concat [ 171 "do ", bound "a", " <- ", free "b", "; ", 172 bound "x", " <<- ", free "f", " ", free "x", "; ", 173 free "g", " ", bx, " od" 174 ]) 175 176val _ = app tpp' [mlettpp_test1, mlettpp_test2, mlettpp_test3, mlettpp_test4] 177 178val _ = monadsyntax.print_explicit_monadic_lets true; 179 180val mlettpp_test5 = 181 ("do a <- b; (x:��) <<- f (x:��); g x; od", 182 String.concat [ 183 "do ", bound "a", " <- ", free "b", "; ", 184 "mlet ", bound "x", " <- ", free "f", " ", free "x", "; ", 185 free "g", " ", bx, " od" 186 ]) 187 188val mlettpp_test6 = 189 ("do a <- b; let x = f x in g x; od", 190 String.concat [ 191 "do ", bound "a", " <- ", free "b", "; ", 192 "mlet ", bound "x", " <- ", free "f", " ", free "x", "; ", 193 free "g", " ", bx, " od" 194 ]) 195 196val _ = app tpp' [mlettpp_test5, mlettpp_test6]; 197 198val _ = disable_monad "option" 199val _ = declare_monad ("option", 200 {bind = ``OPTION_BIND``, ignorebind = NONE, 201 unit = ``SOME``, fail = SOME ``NONE``, 202 choice = SOME ``OPTION_CHOICE``, 203 guard = SOME ``OPTION_GUARD``}) 204val _ = enable_monad "option" 205 206val _ = tprint "Testing monadsyntax parse of OPTION_BIND (ignoring)" 207val t = ``do SOME 3 ; SOME 4 od`` 208val (f, args) = strip_comb t 209val _ = if same_const f ``option$OPTION_BIND`` andalso 210 hd args ~~ ``SOME 3`` andalso 211 hd (tl args) ~~ ``K (SOME 4) : num -> num option`` then 212 OK() else udie() 213 214val _ = app tpp' [monadtpp_test1, monadtpp_test2, monadtpp_test3, 215 monadtpp_test4] 216 217val _ = disable_monad "option" 218val _ = enable_monad "errorState" 219 220val _ = print "Testing with error state monad\n" 221 222val _ = app tpp' [monadtpp_test1, monadtpp_test2, monadtpp_test3] 223 224val _ = current_backend := PPBackEnd.raw_terminal 225val _ = testutils.tpp "do x <- f y; g x od arg" 226 227val _ = Process.exit Process.success 228