1(*---------------------------------------------------------------------------*)
2(* Monadic definitions based on bind and unit operators are higher order     *)
3(* and need congruence rules added for them in order to have correct         *)
4(* termination conditions extracted. The syntax of the desired definition    *)
5(* may need some tweaking in order for our extraction machinery to work      *)
6(* properly. See below. Example, from Ramana Kumar, is to define             *)
7(*                                                                           *)
8(*    foo M =                                                                *)
9(*        STATE_OPTION_BIND (STATE_OPTION_UNIT F)                            *)
10(*         (\b. STATE_OPTION_IGNORE_BIND                                     *)
11(*                (if b then foo M else STATE_OPTION_UNIT ())                *)
12(*                (STATE_OPTION_UNIT ()))                                    *)
13(*                                                                           *)
14(*---------------------------------------------------------------------------*)
15
16set_trace "Unicode" 0;
17set_trace "pp_annotations" 0;
18
19open pairTheory optionTheory relationTheory;
20
21(*---------------------------------------------------------------------------*)
22(* Monad stuff                                                               *)
23(*---------------------------------------------------------------------------*)
24
25val STATE_OPTION_UNIT_def = 
26 Define
27   `STATE_OPTION_UNIT = \a s. SOME(a,s)`;
28
29val STATE_OPTION_BIND_def = 
30 Define
31  `STATE_OPTION_BIND = \m f s. OPTION_BIND (m s) (UNCURRY f)`;
32
33val STATE_OPTION_IGNORE_BIND_def = 
34 Define
35  `STATE_OPTION_IGNORE_BIND = \m1 m2 s. OPTION_BIND (m1 s) (m2 o SND)`;
36
37(*---------------------------------------------------------------------------*)
38(* Expanded out version of example                                           *)
39(*---------------------------------------------------------------------------*)
40
41Hol_defn "foo"
42  `foo M s = 
43     case STATE_OPTION_UNIT F s
44      of NONE -> NONE
45      || SOME (b,s) -> (case ((if b then foo M else STATE_OPTION_UNIT ()) s)
46                         of NONE -> NONE
47                         || SOME(p1,p2) -> STATE_OPTION_UNIT () p2)`;
48
49(*---------------------------------------------------------------------------*)
50(* Add a congruence rule for STATE_OPTION_BIND                               *)
51(*---------------------------------------------------------------------------*)
52
53DefnBase.add_cong 
54 (Q.prove
55   (`!m s m' s' f f'.
56       (m = m') /\ (s=s') /\ 
57       (!x y. (m' s' = SOME(x,y)) ==> (f x y = f' x y))
58        ==> (STATE_OPTION_BIND m f s = STATE_OPTION_BIND m' f' s')`,
59    RW_TAC std_ss [STATE_OPTION_BIND_def] THEN
60      Cases_on `m s` THEN 
61      RW_TAC std_ss [UNCURRY,OPTION_BIND_def]));
62
63(*---------------------------------------------------------------------------*)
64(* Original definition (with a few eta-redexes added in). It's nonsensical;  *)
65(* the only point is to get correct termination conditions extracted. Note   *)
66(* that, for this example, a congruence for STATE_OPTION_IGNORE_BIND isn't   *)
67(* needed.                                                                   *)
68(*---------------------------------------------------------------------------*)
69
70val foo_def = tDefine
71 "foo"
72 `foo M = \s. STATE_OPTION_BIND 
73                (STATE_OPTION_UNIT F)
74                 (\b s. STATE_OPTION_IGNORE_BIND
75                        (if b then foo M else (STATE_OPTION_UNIT ()))
76                        (STATE_OPTION_UNIT())
77                        s)
78                s`
79 (RW_TAC std_ss [STATE_OPTION_UNIT_def] THEN 
80  METIS_TAC [relationTheory.WF_EMPTY_REL]);
81
82(*---------------------------------------------------------------------------*)
83(* Elimination of eta-redexes to obtain                                      *)
84(*                                                                           *)
85(*   val desired_foo_def =                                                   *)
86(*     |- foo M =                                                            *)
87(*        STATE_OPTION_BIND (STATE_OPTION_UNIT F)                            *)
88(*         (\b. STATE_OPTION_IGNORE_BIND                                     *)
89(*                (if b then foo M else STATE_OPTION_UNIT ())                *)
90(*                (STATE_OPTION_UNIT ())) : thm                              *)
91(*---------------------------------------------------------------------------*)
92
93val desired_foo_def = CONV_RULE (DEPTH_CONV ETA_CONV) foo_def;
94
95
96(*---------------------------------------------------------------------------*)
97(* Add a congruence rule for STATE_OPTION_IGNORE_BIND, to check that it      *)
98(* doesn't wreck things.                                                     *)
99(*---------------------------------------------------------------------------*)
100
101DefnBase.add_cong 
102 (Q.prove
103   (`!m1 m2 s m1' m2' s'.
104       (m1 = m1') /\ (s=s') /\ 
105       (!t. (OPTION_MAP SND (m1' s') = SOME t) ==> (m2 t = m2' t))
106        ==> (STATE_OPTION_IGNORE_BIND m1 m2 s = STATE_OPTION_IGNORE_BIND m1' m2' s')`,
107    RW_TAC std_ss [STATE_OPTION_IGNORE_BIND_def] THEN
108      Cases_on `m1 s` THEN 
109      RW_TAC std_ss [UNCURRY,OPTION_BIND_def]));
110
111val foo_def = tDefine
112 "foo"
113 `foo M = \s. STATE_OPTION_BIND 
114                (STATE_OPTION_UNIT F)
115                 (\b s. STATE_OPTION_IGNORE_BIND
116                        (if b then foo M else (STATE_OPTION_UNIT ()))
117                        (STATE_OPTION_UNIT())
118                        s)
119                s`
120 (RW_TAC std_ss [STATE_OPTION_UNIT_def] THEN 
121  METIS_TAC [relationTheory.WF_EMPTY_REL]);
122