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