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 9fun udie () = die "FAILED!" 10 11val _ = tprint "Testing parsing of parmonadsyntax" 12val bind_t = prim_mk_const{Thy = "state_transformer", Name = "BIND"} 13val _ = overload_on ("monad_bind", bind_t) 14val _ = set_trace "notify type variable guesses" 0 15val t = Term`do x <- f y ; g x od` 16val _ = if same_const bind_t (#1 (strip_comb t)) then OK() 17 else udie() 18 19val _ = tprint "Testing Q.parsing of parmonadsyntax" 20val t = Parse.parse_in_context [] `do x <- f y; g x od` 21val _ = if same_const bind_t (#1 (strip_comb t)) then OK() 22 else udie() 23 24val _ = tprint "Testing Q-parsing of parmonadsyntax (TYPED-con)" 25val t = Parse.parse_in_context [] `do x <- f y; g x od : 'a -> bool # 'a` 26val _ = if same_const bind_t (#1 (strip_comb t)) then OK() 27 else udie() 28 29val _ = Parse.current_backend := PPBackEnd.vt100_terminal 30fun tpp' (s,expected) = 31 testutils.tpp_expected { 32 input = s, output = expected, 33 testf = fn s => "Testing (coloured-)printing of `"^s^"`" 34 } 35 36fun bound s = "\^[[0;32m" ^ s ^ "\^[[0m" 37fun free s = "\^[[0;1;34m" ^ s ^ "\^[[0m" 38val concat = String.concat 39 40val bx = bound "x" 41val fy = free "y" 42val fp = free "p" 43val fx = free "x" 44 45val monadtpp_test1 = 46 ("do x <- f y; g x od", 47 concat ["do ", bx, " <- ", free "f", " ", fy, "; ", free "g", " ", 48 bx, " od"]) 49val monadtpp_test2 = 50 ("do m1; m2 od", 51 concat ["do ", free "m1", "; ", free "m2", " od"]) 52 53val monadtpp_test3 = 54 ("do x <- m1; y <- m2; \ 55 \if my_very_long_guard then m3 else do a <- very_long_monad1; \ 56 \b <- very_long_monad2; superLongFinalMonad long_arg od od", 57 String.concat [ 58 "do\n ", 59 bx, " <- ", free "m1", ";\n ", 60 bound "y", " <- ", free "m2", ";\n ", 61 "if ", free "my_very_long_guard", " then ", free "m3", "\n ", (* 2 *) 62 "else\n ", 63 "do\n ", (* 6 *) 64 bound "a", " <- ", free "very_long_monad1", ";\n ", (* 6 *) 65 bound "b", " <- ", free "very_long_monad2", ";\n ", (* 6 *) 66 free "superLongFinalMonad", " ", free "long_arg", "\n ", (* 4 *) 67 "od\n", (* 0 *) 68 "od"]) 69 70val _ = app tpp' [monadtpp_test1, monadtpp_test2, monadtpp_test3] 71 72val _ = clear_overloads_on "monad_bind" 73 74val _ = temp_remove_absyn_postprocessor "parmonadsyntax.transform_absyn" 75val _ = temp_remove_user_printer "parmonadsyntax.print_monads" 76 77val _ = temp_add_user_printer ("monadsyntax.print_monads", genvar alpha, 78 monadsyntax.print_monads) 79val _ = temp_add_absyn_postprocessor ("monadsyntax.transform_absyn", 80 monadsyntax.transform_absyn) 81 82val _ = monadsyntax.enable_monad "option" 83 84val _ = unicode_off (raw_backend (trace ("types", 1) testutils.tpp)) 85 "do (x :num) <- (s :num option); SOME (x + (1 :num)) od" 86 87val _ = tprint "Testing monadsyntax parse of OPTION_BIND" 88val t = ``do x <- opt ; SOME (x + 1) od`` 89val (f, args) = strip_comb t 90val _ = same_const f ``option$OPTION_BIND`` andalso 91 hd args = mk_var("opt", ``:num option``) andalso 92 hd (tl args) = ``\x:num. SOME (x + 1)`` andalso 93 (OK(); true) orelse udie () 94 95val _ = tprint "Testing monadsyntax parse of OPTION_IGNORE_BIND" 96val t = ``do SOME 3 ; SOME 4 od`` 97val (f, args) = strip_comb t 98val _ = same_const f ``option$OPTION_IGNORE_BIND`` andalso 99 hd args = ``SOME 3`` andalso 100 hd (tl args) = ``SOME 4`` andalso 101 (OK(); true) orelse udie() 102 103val _ = disable_monad "option" 104val _ = declare_monad ("option", 105 {bind = ``OPTION_BIND``, ignorebind = NONE, 106 unit = ``SOME``, fail = SOME ``NONE``, 107 choice = SOME ``OPTION_CHOICE``, 108 guard = SOME ``OPTION_GUARD``}) 109val _ = enable_monad "option" 110 111val _ = tprint "Testing monadsyntax parse of OPTION_BIND (ignoring)" 112val t = ``do SOME 3 ; SOME 4 od`` 113val (f, args) = strip_comb t 114val _ = same_const f ``option$OPTION_BIND`` andalso 115 hd args = ``SOME 3`` andalso 116 hd (tl args) = ``K (SOME 4) : num -> num option`` andalso 117 (OK(); true) orelse udie() 118 119val _ = app tpp' [monadtpp_test1, monadtpp_test2, monadtpp_test3] 120 121val _ = disable_monad "option" 122val _ = enable_monad "errorState" 123 124val _ = print "Testing with error state monad\n" 125 126val _ = app tpp' [monadtpp_test1, monadtpp_test2, monadtpp_test3] 127 128val _ = current_backend := PPBackEnd.raw_terminal 129val _ = testutils.tpp "do x <- f y; g x od arg" 130 131val _ = Process.exit Process.success 132