1structure state_monadLib :> state_monadLib = 2struct 3 4open HolKernel Parse boolLib numLib simpLib 5open state_transformerTheory 6 7structure Parse = struct 8 open Parse 9 val (Type, Term) = 10 parse_from_grammars state_transformerTheory.state_transformer_grammars 11end 12open Parse 13 14val add_state_monad_compset = 15 let 16 val cnv = 17 SIMP_CONV std_ss 18 [Once state_transformerTheory.FOR_def, 19 Once state_transformerTheory.MWHILE_DEF, 20 state_transformerTheory.MMAP_DEF, 21 state_transformerTheory.MCOMP_DEF, 22 state_transformerTheory.JOIN_DEF, 23 state_transformerTheory.FOREACH_def, 24 state_transformerTheory.READ_def, 25 state_transformerTheory.WRITE_def, 26 state_transformerTheory.NARROW_def, 27 state_transformerTheory.WIDEN_def, 28 state_transformerTheory.UNIT_DEF, 29 state_transformerTheory.BIND_DEF, 30 state_transformerTheory.EXT_DEF, 31 state_transformerTheory.IGNORE_BIND_DEF, 32 state_transformerTheory.sequence_def, 33 state_transformerTheory.mapM_def, 34 boolTheory.LET_DEF, boolTheory.COND_RATOR, pairTheory.UNCURRY_DEF, 35 combinTheory.o_DEF, 36 combinTheory.I_THM 37 |> Q.SPEC `x` 38 |> Conv.CONV_RULE (Conv.RAND_CONV (Conv.UNBETA_CONV ``x:'a``)) 39 |> Drule.GEN_ALL 40 |> Drule.EXT] o 41 Feedback.trace ("notify type variable guesses", 0) Parse.Term 42 in 43 computeLib.add_thms 44 (pairTheory.UNCURRY_DEF :: 45 List.map cnv 46 [ 47 `UNIT v s`, 48 `BIND f g s`, 49 `EXT f g s`, 50 `mapM f s`, 51 `MMAP f g s`, 52 `MCOMP f g s x`, 53 `JOIN f s`, 54 `FOREACH ([], f) s`, 55 `FOREACH (h :: t, f) s`, 56 `FOR (i, j, f) s`, 57 `READ f s`, 58 `WRITE f s`, 59 `NARROW v f s`, 60 `WIDEN f (s1, s2)`, 61 `MWHILE f g s`, 62 `IGNORE_BIND f g s`, 63 `sequence l s` 64 ] 65 ) 66 end 67 68end 69