1structure state_transformerSyntax :> state_transformerSyntax =
2struct
3
4open Abbrev HolKernel state_transformerTheory
5
6val ERR = Feedback.mk_HOL_ERR "state_transformerSyntax"
7
8(*---------------------------------------------------------------------------*)
9
10fun syntax n d m =
11   HolKernel.syntax_fns {n = n, dest = d, make = m} "state_transformer"
12
13val s1 = syntax 2 HolKernel.dest_monop HolKernel.mk_monop
14val s2 = syntax 3 HolKernel.dest_binop HolKernel.mk_binop
15
16fun mk_monad_type (ty1, ty2) = ty2 --> pairSyntax.mk_prod (ty1, ty2)
17
18local
19   val err = ERR "dest_monad_type" "not a monad type"
20in
21   fun dest_monad_type ty =
22      let
23         val (ty1, ty2) = Lib.with_exn Type.dom_rng ty err
24         val ty3 as (_, ty4) = Lib.with_exn pairSyntax.dest_prod ty2 err
25         val _ = ty1 = ty4 orelse raise err
26      in
27         ty3
28      end
29end
30
31val state_ty = Type.mk_vartype "'state"
32
33val (unit_tm, mk_unit, dest_unit, is_unit) =
34   syntax 2
35      (fn tm1 => fn e => fn tm2 =>
36          (HolKernel.dest_monop tm1 e tm2,
37           tm2 |> Term.type_of |> Type.dom_rng |> fst))
38      (fn tm1 => fn (tm2, ty) =>
39          Term.mk_comb
40             (Term.inst [Type.alpha |-> ty, Type.beta |-> Term.type_of tm2] tm1,
41              tm2))
42      "UNIT"
43
44val (widen_tm, mk_widen, dest_widen, is_widen) =
45   syntax 2
46      (fn tm1 => fn e => fn tm2 =>
47          (HolKernel.dest_monop tm1 e tm2,
48           fst (pairSyntax.dest_prod
49                   (snd (dest_monad_type (Term.type_of tm2))))))
50      (fn tm1 => fn (tm2, ty) =>
51          let
52             val (ty1, ty2) = dest_monad_type (Term.type_of tm2)
53          in
54             Term.mk_comb
55                (Term.inst [Type.alpha |-> ty1,
56                            Type.beta |-> ty,
57                            state_ty |-> ty2] tm1, tm2)
58          end)
59      "WIDEN"
60
61val (join_tm, mk_join, dest_join, is_join) = s1 "JOIN"
62val (read_tm, mk_read, dest_read, is_read) = s1 "READ"
63val (write_tm, mk_write, dest_write, is_write) = s1 "WRITE"
64val (narrow_tm, mk_narrow, dest_narrow, is_narrow) = s2 "NARROW"
65val (bind_tm, mk_bind, dest_bind, is_bind) = s2 "BIND"
66val (mmap_tm, mk_mmap, dest_mmap, is_mmap) = s2 "MMAP"
67
68val get_state_ty = fst o Type.dom_rng o snd o Type.dom_rng o Term.type_of
69
70val (for_tm, mk_for, dest_for, is_for) =
71   syntax 2
72      (fn tm1 => fn e => fn tm2 =>
73          let
74             val a = HolKernel.dest_monop tm1 e tm2
75          in
76             case pairSyntax.strip_pair a of
77                [i, j, b] => (i, j, b)
78              | _ => raise e
79          end)
80      (fn tm => fn (i, j, b) =>
81         Term.mk_comb (Term.inst [state_ty |-> get_state_ty b] tm,
82                       pairSyntax.list_mk_pair [i, j, b]))
83      "FOR"
84
85val (foreach_tm, mk_foreach, dest_foreach, is_foreach) =
86   syntax 2
87      (fn tm1 => fn e => fn tm2 =>
88          Lib.with_exn pairSyntax.dest_pair (HolKernel.dest_monop tm1 e tm2) e)
89      (fn tm => fn (i, b) =>
90         let
91            val ity = listSyntax.dest_list_type (Term.type_of i)
92            val ty = get_state_ty b
93         in
94            Term.mk_comb (Term.inst [Type.alpha |-> ity, state_ty |-> ty] tm,
95                          pairSyntax.mk_pair (i, b))
96         end)
97      "FOREACH"
98
99end
100