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