1structure combinSyntax :> combinSyntax =
2struct
3
4open HolKernel Parse boolLib;  local open combinTheory in end;
5
6val ERR = mk_HOL_ERR "combinSyntax"
7
8val K_tm = prim_mk_const{Name="K", Thy="combin"}
9val S_tm = prim_mk_const{Name="S", Thy="combin"}
10val I_tm = prim_mk_const{Name="I", Thy="combin"}
11val C_tm = prim_mk_const{Name="C", Thy="combin"}
12val W_tm = prim_mk_const{Name="W", Thy="combin"}
13val o_tm = prim_mk_const{Name="o", Thy="combin"};
14
15val update_tm = prim_mk_const{Name="UPDATE", Thy="combin"};
16
17fun mk_K(x,y) =
18   list_mk_comb(inst[alpha |-> type_of x,
19                     beta |-> type_of y]K_tm, [x,y]);
20
21fun mk_K_1 (tm,ty) = mk_comb(inst [alpha |-> type_of tm,
22                                   beta  |-> ty] K_tm,tm)
23
24fun mk_S(f,g,x) =
25 let val (fdom,frng) = dom_rng(type_of f)
26     val (ty1,ty2) = dom_rng frng
27 in list_mk_comb(inst[alpha |-> fdom,
28                      beta |-> ty1, gamma |-> ty2]S_tm, [f,g,x])
29 end
30
31fun mk_I x = mk_comb(inst[alpha |-> type_of x]I_tm, x)
32
33fun mk_C(f,x,y) =
34 let val (fdom,frng) = dom_rng(type_of f)
35     val (ty1,ty2) = dom_rng frng
36 in list_mk_comb(inst[alpha |-> fdom,
37                      beta  |-> ty1,
38                      gamma |-> ty2]C_tm, [f,x,y])
39 end
40
41fun mk_W(f,x) =
42  let val (ty1,rng) = dom_rng (type_of f)
43      val (_,ty2) = dom_rng rng
44  in list_mk_comb(inst[alpha |-> ty1, beta |-> ty2]W_tm, [f,x])
45 end
46
47fun mk_o(f,g) =
48 let val (fdom,frng) = dom_rng(type_of f)
49     val (gdom,_)    = dom_rng(type_of g)
50 in list_mk_comb
51      (inst [alpha |-> gdom, beta |-> frng, gamma |-> fdom] o_tm, [f,g])
52 end;
53
54fun mk_update(f,g) =
55 list_mk_comb
56    (inst [alpha |-> type_of f, beta |-> type_of g] update_tm, [f,g])
57 handle HOL_ERR _ => raise ERR "mk_update" "";
58
59val dest_K   = dest_binop K_tm (ERR "dest_K"   "not K")
60val dest_K_1 = dest_monop K_tm (ERR "dest_K_1" "not K")
61val dest_S   = dest_triop S_tm (ERR "dest_S"   "not S")
62val dest_I   = dest_monop I_tm (ERR "dest_I"   "not I")
63val dest_C   = dest_triop C_tm (ERR "dest_C"   "not C")
64val dest_W   = dest_binop W_tm (ERR "dest_W"   "not W")
65val dest_o   = dest_binop o_tm (ERR "dest_o"   "not o")
66
67val dest_update = dest_binop update_tm (ERR "dest_update"   "not =+")
68val dest_update_comb = (dest_update ## I) o Term.dest_comb
69val is_update_comb   = can dest_update_comb
70
71fun strip_update tm =
72let
73  fun recurse t a =
74        if not (is_update_comb t) then
75          (List.rev a, t)
76        else let val (u,t') = dest_update_comb t in
77          recurse t' (u::a)
78        end
79in
80  recurse tm []
81end
82
83val is_K   = can dest_K
84val is_K_1 = can dest_K_1
85val is_S   = can dest_S
86val is_I   = can dest_I
87val is_C   = can dest_C
88val is_W   = can dest_W
89val is_o   = can dest_o
90
91val is_update = can dest_update
92
93val fail_tm = prim_mk_const{Name="FAIL", Thy="combin"};
94
95fun mk_fail (f,s,args) =
96   list_mk_comb(inst[alpha |-> type_of f,
97                     beta |-> bool]fail_tm,
98                 f::mk_var(s,bool)::args);
99fun dest_fail M =
100  case strip_comb M
101   of (c,f::s::args) =>
102        if same_const c fail_tm then
103          if is_var s then (f,fst(dest_var s),args)
104          else raise ERR "dest_fail" "need a variable"
105        else raise ERR "dest_fail" "not a FAIL term"
106    | otherwise => raise ERR "dest_fail" "too few args";
107
108val is_fail = can dest_fail;
109
110end
111