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