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