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