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