2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 (* (weight of constants, [(meta, weight_of_meta)]) *)
15 type weight = int * (int * int) list;;
17 let string_of_weight (cw, mw) =
20 (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
22 Printf.sprintf "[%d; %s]" cw s
25 let weight_of_term term =
26 let vars_dict = Hashtbl.create 5 in
27 let rec aux = function
30 let oldw = Hashtbl.find vars_dict i in
31 Hashtbl.replace vars_dict i (oldw+1)
33 Hashtbl.add vars_dict i 1);
36 | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
40 Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict []
44 | (m1, _), (m2, _) -> m2 - m1
46 (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
49 let compute_clause_weight = assert false (*
53 let w, m = (weight_of_term
54 ~consider_metas:true ~count_metas_occurrences:false right) in
55 w + (factor * (List.length m)) ;
58 let w, m = (weight_of_term
59 ~consider_metas:true ~count_metas_occurrences:false left) in
60 w + (factor * (List.length m)) ;
64 let w1, m1 = (weight_of_term
65 ~consider_metas:true ~count_metas_occurrences:false right) in
66 let w2, m2 = (weight_of_term
67 ~consider_metas:true ~count_metas_occurrences:false left) in
68 w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
72 (* returns a "normalized" version of the polynomial weight wl (with type
73 * weight list), i.e. a list sorted ascending by meta number,
74 * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
75 * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
76 * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
77 let normalize_weight maxmeta (cw, wl) =
78 let rec aux = function
80 | m -> (m, 0)::(aux (m-1))
82 let tmpl = aux maxmeta in
85 (fun (m, _) (n, _) -> Pervasives.compare m n)
87 (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
93 let normalize_weights (cw1, wl1) (cw2, wl2) =
97 | (m, w)::tl1, (n, w')::tl2 when m = n ->
98 let res1, res2 = aux tl1 tl2 in
99 (m, w)::res1, (n, w')::res2
100 | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
101 let res1, res2 = aux tl1 wl2 in
102 (m, w)::res1, (m, 0)::res2
103 | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
104 let res1, res2 = aux wl1 tl2 in
105 (n, 0)::res1, (n, w')::res2
107 let res1, res2 = aux [] tl2 in
108 (n, 0)::res1, (n, w)::res2
110 let res1, res2 = aux tl1 [] in
111 (m, w)::res1, (m, 0)::res2
112 | _, _ -> assert false
114 let cmp (m, _) (n, _) = compare m n in
115 let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
116 (cw1, wl1), (cw2, wl2)
119 (* Riazanov: 3.1.5 pag 38 *)
120 let compare_weights ((h1, w1) as weight1) ((h2, w2) as weight2)=
124 (fun ((lt, eq, gt), diffs) w1 w2 ->
126 | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
127 let diffs = (w1 - w2) + diffs in
128 let r = compare w1 w2 in
129 if r < 0 then (lt+1, eq, gt), diffs
130 else if r = 0 then (lt, eq+1, gt), diffs
131 else (lt, eq, gt+1), diffs
134 with Invalid_argument _ -> assert false
136 let hdiff = h1 - h2 in
140 else if hdiff > 0 then Gt
143 if hdiff <= 0 then Lt
144 else if (- diffs) >= hdiff then Le else Incomparable
146 if hdiff >= 0 then Gt
147 else if diffs >= (- hdiff) then Ge else Incomparable
148 | (m, _, n) when m > 0 && n > 0 ->
154 let rec aux_ordering ?(recursion=true) t1 t2 =
155 let module C = Cic in
156 let compare_uris u1 u2 =
158 compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) in
160 else if res = 0 then Eq
165 | _, C.Meta _ -> Incomparable
167 | t1, t2 when t1 = t2 -> Eq
169 | C.Rel n, C.Rel m -> if n > m then Lt else Gt
173 | C.Const (u1, _), C.Const (u2, _) -> compare_uris u1 u2
177 | C.MutInd (u1, tno1, _), C.MutInd (u2, tno2, _) ->
178 let res = compare_uris u1 u2 in
179 if res <> Eq then res
181 let res = compare tno1 tno2 in
182 if res = 0 then Eq else if res < 0 then Lt else Gt
183 | C.MutInd _, _ -> Lt
184 | _, C.MutInd _ -> Gt
186 | C.MutConstruct (u1, tno1, cno1, _), C.MutConstruct (u2, tno2, cno2, _) ->
187 let res = compare_uris u1 u2 in
188 if res <> Eq then res
190 let res = compare (tno1,cno1) (tno2,cno2) in
191 if res = 0 then Eq else if res < 0 then Lt else Gt
192 | C.MutConstruct _, _ -> Lt
193 | _, C.MutConstruct _ -> Gt
195 | C.Appl l1, C.Appl l2 when recursion ->
201 | hd1::tl1, hd2::tl2 ->
202 let o = aux_ordering hd1 hd2 in
203 if o = Eq then cmp tl1 tl2
207 | C.Appl (h1::t1), C.Appl (h2::t2) when not recursion ->
213 (Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
214 (CicPp.ppterm t1) (CicPp.ppterm t2)));
218 let nonrec_kbo t1 t2 =
219 let w1 = weight_of_term t1 in
220 let w2 = weight_of_term t2 in
221 match compare_weights ~normalize:true w1 w2 with
222 | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
223 | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
224 | Eq -> aux_ordering t1 t2
229 let aux = aux_ordering ~recursion:false in
230 let w1 = weight_of_term t1
231 and w2 = weight_of_term t2 in
237 | hd1::tl1, hd2::tl2 ->
241 if o = Eq then cmp tl1 tl2
244 let comparison = compare_weights ~normalize:true w1 w2 in
245 match comparison with
249 else if r = Eq then (
251 | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
252 if cmp tl1 tl2 = Lt then Lt else Incomparable
253 | _, _ -> Incomparable
258 else if r = Eq then (
260 | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
261 if cmp tl1 tl2 = Gt then Gt else Incomparable
262 | _, _ -> Incomparable
268 | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
270 | _, _ -> Incomparable
275 let compare_terms = nonrec_kbo;;