1structure wfrecUtils :> wfrecUtils = 2struct 3 4open HolKernel boolSyntax pairSyntax Abbrev; 5 6val ERR = mk_HOL_ERR "wfrecUtils"; 7 8fun zip3 [][][] = [] 9 | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3 10 | zip3 _ _ _ = raise ERR "zip3" "different lengths"; 11 12 13fun unzip3 [] = ([],[],[]) 14 | unzip3 ((x,y,z)::rst) = 15 let val (l1,l2,l3) = unzip3 rst 16 in (x::l1, y::l2, z::l3) 17 end; 18 19fun gtake f = 20 let fun grab(0,rst) = ([],rst) 21 | grab(n, x::rst) = 22 let val (taken,left) = grab(n-1,rst) 23 in (f x::taken, left) end 24 | grab _ = raise ERR "gtake" "grab.empty list" 25 in grab 26 end; 27 28 29fun list_to_string f delim = 30 let fun stringulate [] = [] 31 | stringulate [x] = [f x] 32 | stringulate (h::t) = f h::delim::stringulate t 33 in 34 fn l => String.concat (stringulate l) 35 end; 36 37 38fun mk_sum_type ty1 ty2 = mk_type("sum", [ty1,ty2]) 39val mk_prod_type = curry mk_prod; 40 41val list_mk_fun_type = end_itlist (curry(op -->)); 42val list_mk_prod_type = list_mk_prod; 43 44val strip_fun_type = HolKernel.strip_fun; 45val strip_prod_type = pairSyntax.spine_prod; 46 47fun atom_name tm = fst(dest_var tm handle HOL_ERR _ => dest_const tm); 48 49fun strip_imp tm = 50 if is_neg tm then ([],tm) else 51 if is_imp tm then 52 let val (ant,conseq) = dest_imp_only tm 53 val (imps,rst) = strip_imp conseq 54 in (ant::imps, rst) 55 end 56 else ([],tm); 57 58fun gen_all tm = itlist (curry mk_forall) (free_vars_lr tm) tm; 59 60 61local fun break [] = raise ERR "mk_vstruct" "unable" 62 | break (h::t) = (h,t) 63in 64fun mk_vstruct ty V = 65 if is_vartype ty then break V 66 else case dest_thy_type ty 67 of {Tyop="prod", Thy="pair", Args=[ty1,ty2]} => 68 let val (ltm,vs1) = mk_vstruct ty1 V 69 val (rtm,vs2) = mk_vstruct ty2 vs1 70 in 71 (mk_pair(ltm, rtm), vs2) 72 end 73 | _ => break V 74end; 75 76fun func_of_cond_eqn tm = 77 #1(strip_comb(lhs(#2 (strip_forall(#2(strip_imp (#2 (strip_forall tm)))))))) 78 79fun dest_relation tm = 80 if type_of tm = Type.bool 81 then let val (Rator,r) = dest_comb tm 82 val (Rator,d) = dest_comb Rator 83 in (Rator,d,r) 84 end 85 handle HOL_ERR _ => raise ERR "dest_relation" "term structure" 86 else raise ERR "dest_relation" "not a boolean term"; 87 88 89fun is_WFR tm = 90 case total dest_thy_const (rator tm) 91 of SOME{Name="WF", Thy="relation", ...} => true 92 | otherwise => false; 93 94 95(*--------------------------------------------------------------------------- 96 * "vary" makes variables that are guaranteed not to be in vlist and 97 * furthermore, are guaranteed not to be equal to each other. The names of 98 * the variables will start with "v" and end in a number. 99 *---------------------------------------------------------------------------*) 100 101local val counter = ref 0 102in 103fun vary vlist = 104 let val slist = ref (map (fst o dest_var) vlist) 105 val _ = counter := 0 106 fun pass str = 107 if Lib.mem str (!slist) 108 then (counter := !counter + 1; pass ("v"^int_to_string(!counter))) 109 else (slist := str :: !slist; str) 110 in 111 fn ty => mk_var(pass "v", ty) 112 end 113end; 114 115fun match_term thry tm1 tm2 = Term.match_term tm1 tm2; 116fun match_type thry ty1 ty2 = Type.match_type ty1 ty2; 117 118end; 119