]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/paramodulation/utils.ml
avoid writing in read only baseuris
[helm.git] / helm / ocaml / paramodulation / utils.ml
1 (* Copyright (C) 2005, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (* $Id$ *)
27
28 let debug = true;;
29
30 let debug_print s = if debug then prerr_endline (Lazy.force s);;
31
32 let print_metasenv metasenv =
33   String.concat "\n--------------------------\n"
34     (List.map (fun (i, context, term) ->
35                  (string_of_int i) ^ " [\n" ^ (CicPp.ppcontext context) ^
36                    "\n] " ^  (CicPp.ppterm term))
37        metasenv)
38 ;;
39
40
41 let print_subst ?(prefix="\n") subst =
42   String.concat prefix
43     (List.map
44        (fun (i, (c, t, ty)) ->
45           Printf.sprintf "?%d -> %s : %s" i
46             (CicPp.ppterm t) (CicPp.ppterm ty))
47        subst)
48 ;;  
49
50 (* (weight of constants, [(meta, weight_of_meta)]) *)
51 type weight = int * (int * int) list;;
52
53 let string_of_weight (cw, mw) =
54   let s =
55     String.concat ", "
56       (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
57   in
58   Printf.sprintf "[%d; %s]" cw s
59
60
61 let weight_of_term ?(consider_metas=true) term =
62   let module C = Cic in
63   let vars_dict = Hashtbl.create 5 in
64   let rec aux = function
65     | C.Meta (metano, _) when consider_metas ->
66         (try
67            let oldw = Hashtbl.find vars_dict metano in
68            Hashtbl.replace vars_dict metano (oldw+1)
69          with Not_found ->
70            Hashtbl.add vars_dict metano 1);
71         0
72     | C.Meta _ -> 0 (* "variables" are lighter than constants and functions...*)
73                   
74     | C.Var (_, ens)
75     | C.Const (_, ens)
76     | C.MutInd (_, _, ens)
77     | C.MutConstruct (_, _, _, ens) ->
78         List.fold_left (fun w (u, t) -> (aux t) + w) 1 ens
79           
80     | C.Cast (t1, t2)
81     | C.Lambda (_, t1, t2)
82     | C.Prod (_, t1, t2)
83     | C.LetIn (_, t1, t2) ->
84         let w1 = aux t1 in
85         let w2 = aux t2 in
86         w1 + w2 + 1
87           
88     | C.Appl l -> List.fold_left (+) 0 (List.map aux l)
89         
90     | C.MutCase (_, _, outt, t, pl) ->
91         let w1 = aux outt in
92         let w2 = aux t in
93         let w3 = List.fold_left (+) 0 (List.map aux pl) in
94         w1 + w2 + w3 + 1
95           
96     | C.Fix (_, fl) ->
97         List.fold_left (fun w (n, i, t1, t2) -> (aux t1) + (aux t2) + w) 1 fl
98           
99     | C.CoFix (_, fl) ->
100         List.fold_left (fun w (n, t1, t2) -> (aux t1) + (aux t2) + w) 1 fl
101           
102     | _ -> 1
103   in
104   let w = aux term in
105   let l =
106     Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict [] in
107   let compare w1 w2 = 
108     match w1, w2 with
109     | (m1, _), (m2, _) -> m2 - m1 
110   in 
111   (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
112 ;;
113
114
115 module OrderedInt = struct
116   type t = int
117
118   let compare = Pervasives.compare
119 end
120
121 module IntSet = Set.Make(OrderedInt)
122
123 let compute_equality_weight ty left right =
124   let metasw = ref 0 in
125   let weight_of t =
126     let w, m = (weight_of_term ~consider_metas:true t) in
127     metasw := !metasw + (2 * (List.length m));
128     w
129   in
130   (* Warning: the following let cannot be expanded since it forces the
131      right evaluation order!!!! *)
132   let w = (weight_of ty) + (weight_of left) + (weight_of right) in
133   w + !metasw
134 ;;
135
136
137 (* returns a "normalized" version of the polynomial weight wl (with type
138  * weight list), i.e. a list sorted ascending by meta number,
139  * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
140  * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
141  *      (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
142 let normalize_weight maxmeta (cw, wl) =
143   let rec aux = function
144     | 0 -> []
145     | m -> (m, 0)::(aux (m-1))
146   in
147   let tmpl = aux maxmeta in
148   let wl =
149     List.sort
150       (fun (m, _) (n, _) -> Pervasives.compare m n)
151       (List.fold_left
152          (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
153   in
154   (cw, wl)
155 ;;
156
157
158 let normalize_weights (cw1, wl1) (cw2, wl2) =
159   let rec aux wl1 wl2 =
160     match wl1, wl2 with
161     | [], [] -> [], []
162     | (m, w)::tl1, (n, w')::tl2 when m = n ->
163         let res1, res2 = aux tl1 tl2 in
164         (m, w)::res1, (n, w')::res2
165     | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
166         let res1, res2 = aux tl1 wl2 in
167         (m, w)::res1, (m, 0)::res2
168     | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
169         let res1, res2 = aux wl1 tl2 in
170         (n, 0)::res1, (n, w')::res2
171     | [], (n, w)::tl2 ->
172         let res1, res2 = aux [] tl2 in
173         (n, 0)::res1, (n, w)::res2
174     | (m, w)::tl1, [] ->
175         let res1, res2 = aux tl1 [] in
176         (m, w)::res1, (m, 0)::res2
177     | _, _ -> assert false
178   in
179   let cmp (m, _) (n, _) = compare m n in
180   let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
181   (cw1, wl1), (cw2, wl2)
182 ;;
183
184         
185 type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;;
186     
187 let string_of_comparison = function
188   | Lt -> "<"
189   | Le -> "<="
190   | Gt -> ">"
191   | Ge -> ">="
192   | Eq -> "="
193   | Incomparable -> "I"
194
195
196 let compare_weights ?(normalize=false)
197     ((h1, w1) as weight1) ((h2, w2) as weight2)=
198   let (h1, w1), (h2, w2) =
199     if normalize then
200       normalize_weights weight1 weight2
201     else
202       (h1, w1), (h2, w2)
203   in
204   let res, diffs =
205     try
206       List.fold_left2
207         (fun ((lt, eq, gt), diffs) w1 w2 ->
208            match w1, w2 with
209            | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
210                let diffs = (w1 - w2) + diffs in 
211                let r = compare w1 w2 in
212                if r < 0 then (lt+1, eq, gt), diffs
213                else if r = 0 then (lt, eq+1, gt), diffs
214                else (lt, eq, gt+1), diffs
215            | (meta1, w1), (meta2, w2) ->
216                debug_print
217                  (lazy
218                     (Printf.sprintf "HMMM!!!! %s, %s\n"
219                        (string_of_weight weight1) (string_of_weight weight2)));
220                assert false)
221         ((0, 0, 0), 0) w1 w2
222     with Invalid_argument _ ->
223       debug_print
224         (lazy
225            (Printf.sprintf "Invalid_argument: %s{%s}, %s{%s}, normalize = %s\n"
226               (string_of_weight (h1, w1)) (string_of_weight weight1)
227               (string_of_weight (h2, w2)) (string_of_weight weight2)
228               (string_of_bool normalize)));
229       assert false
230   in
231   let hdiff = h1 - h2 in
232   match res with
233   | (0, _, 0) ->
234       if hdiff < 0 then Lt
235       else if hdiff > 0 then Gt
236       else Eq (* Incomparable *)
237   | (m, _, 0) ->
238       if diffs < (- hdiff) then Lt
239       else if diffs = (- hdiff) then Le else Incomparable
240 (*
241       if hdiff <= 0 then 
242         if m > 0 || hdiff < 0 then Lt
243         else if diffs >= (- hdiff) then Le else Incomparable
244       else 
245         if diffs >= (- hdiff) then Le else Incomparable *)
246   | (0, _, m) ->
247       if (- hdiff) < diffs then Gt
248       else if (- hdiff) = diffs then Ge else Incomparable
249 (*
250       if hdiff >= 0 then 
251         if m > 0 || hdiff > 0 then Gt
252         else if (- diffs) >= hdiff then Ge else Incomparable
253       else
254         if (- diffs) >= hdiff then Ge else Incomparable *)
255   | (m, _, n) when m > 0 && n > 0 ->
256       Incomparable
257   | _ -> assert false
258 ;;
259
260
261 let rec aux_ordering ?(recursion=true) t1 t2 =
262   let module C = Cic in
263   let compare_uris u1 u2 =
264     let res =
265       compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) in
266     if res < 0 then Lt
267     else if res = 0 then Eq
268     else Gt
269   in
270   match t1, t2 with
271   | C.Meta _, _
272   | _, C.Meta _ -> Incomparable
273
274   | t1, t2 when t1 = t2 -> Eq
275
276   | C.Rel n, C.Rel m -> if n > m then Lt else Gt
277   | C.Rel _, _ -> Lt
278   | _, C.Rel _ -> Gt
279
280   | C.Const (u1, _), C.Const (u2, _) -> compare_uris u1 u2
281   | C.Const _, _ -> Lt
282   | _, C.Const _ -> Gt
283
284   | C.MutInd (u1, _, _), C.MutInd (u2, _, _) -> compare_uris u1 u2
285   | C.MutInd _, _ -> Lt
286   | _, C.MutInd _ -> Gt
287
288   | C.MutConstruct (u1, _, _, _), C.MutConstruct (u2, _, _, _) ->
289       compare_uris u1 u2
290   | C.MutConstruct _, _ -> Lt
291   | _, C.MutConstruct _ -> Gt
292
293   | C.Appl l1, C.Appl l2 when recursion ->
294       let rec cmp t1 t2 =
295         match t1, t2 with
296         | [], [] -> Eq
297         | _, [] -> Gt
298         | [], _ -> Lt
299         | hd1::tl1, hd2::tl2 ->
300             let o = aux_ordering hd1 hd2 in
301             if o = Eq then cmp tl1 tl2
302             else o
303       in
304       cmp l1 l2
305   | C.Appl (h1::t1), C.Appl (h2::t2) when not recursion ->
306       aux_ordering h1 h2
307         
308   | t1, t2 ->
309       debug_print
310         (lazy
311            (Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n"
312               (CicPp.ppterm t1) (CicPp.ppterm t2)));
313       Incomparable
314 ;;
315
316
317 (* w1, w2 are the weights, they should already be normalized... *)
318 let nonrec_kbo_w (t1, w1) (t2, w2) =
319   match compare_weights w1 w2 with
320   | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
321   | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
322   | Eq -> aux_ordering t1 t2
323   | res -> res
324 ;;
325
326     
327 let nonrec_kbo t1 t2 =
328   let w1 = weight_of_term t1 in
329   let w2 = weight_of_term t2 in
330   (* 
331   prerr_endline ("weight1 :"^(string_of_weight w1));
332   prerr_endline ("weight2 :"^(string_of_weight w2)); 
333   *)
334   match compare_weights ~normalize:true w1 w2 with
335   | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
336   | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
337   | Eq -> aux_ordering t1 t2
338   | res -> res
339 ;;
340
341
342 let rec kbo t1 t2 =
343   let aux = aux_ordering ~recursion:false in
344   let w1 = weight_of_term t1
345   and w2 = weight_of_term t2 in
346   let rec cmp t1 t2 =
347     match t1, t2 with
348     | [], [] -> Eq
349     | _, [] -> Gt
350     | [], _ -> Lt
351     | hd1::tl1, hd2::tl2 ->
352         let o =
353           kbo hd1 hd2
354         in
355         if o = Eq then cmp tl1 tl2
356         else o
357   in
358   let comparison = compare_weights ~normalize:true w1 w2 in
359   match comparison with
360   | Le ->
361       let r = aux t1 t2 in
362       if r = Lt then Lt
363       else if r = Eq then (
364         match t1, t2 with
365         | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
366             if cmp tl1 tl2 = Lt then Lt else Incomparable
367         | _, _ ->  Incomparable
368       ) else Incomparable
369   | Ge ->
370       let r = aux t1 t2 in
371       if r = Gt then Gt
372       else if r = Eq then (
373         match t1, t2 with
374         | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
375             if cmp tl1 tl2 = Gt then Gt else Incomparable
376         | _, _ ->  Incomparable
377       ) else Incomparable
378   | Eq ->
379       let r = aux t1 t2 in
380       if r = Eq then (
381         match t1, t2 with
382         | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
383             cmp tl1 tl2
384         | _, _ ->  Incomparable
385       ) else r 
386   | res -> res
387 ;;
388           
389 let rec ao t1 t2 =
390   let get_hd t =
391     match t with
392         Cic.MutConstruct(uri,tyno,cno,_) -> Some(uri,tyno,cno)
393       | Cic.Appl(Cic.MutConstruct(uri,tyno,cno,_)::_) -> 
394           Some(uri,tyno,cno)
395       | _ -> None in
396   let aux = aux_ordering ~recursion:false in
397   let w1 = weight_of_term t1
398   and w2 = weight_of_term t2 in
399   let rec cmp t1 t2 =
400     match t1, t2 with
401     | [], [] -> Eq
402     | _, [] -> Gt
403     | [], _ -> Lt
404     | hd1::tl1, hd2::tl2 ->
405         let o =
406           ao hd1 hd2
407         in
408         if o = Eq then cmp tl1 tl2
409         else o
410   in
411   match get_hd t1, get_hd t2 with
412       Some(_),None -> Lt
413     | None,Some(_) -> Gt
414     | _ ->
415         let comparison = compare_weights ~normalize:true w1 w2 in
416           match comparison with
417             | Le ->
418                 let r = aux t1 t2 in
419                   if r = Lt then Lt
420                   else if r = Eq then (
421                     match t1, t2 with
422                       | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
423                           if cmp tl1 tl2 = Lt then Lt else Incomparable
424                       | _, _ ->  Incomparable
425                   ) else Incomparable
426             | Ge ->
427                 let r = aux t1 t2 in
428                   if r = Gt then Gt
429                   else if r = Eq then (
430                     match t1, t2 with
431                       | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
432                           if cmp tl1 tl2 = Gt then Gt else Incomparable
433                       | _, _ ->  Incomparable
434                   ) else Incomparable
435             | Eq ->
436                 let r = aux t1 t2 in
437                   if r = Eq then (
438                     match t1, t2 with
439                       | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 ->
440                           cmp tl1 tl2
441                       | _, _ ->  Incomparable
442                   ) else r 
443             | res -> res
444 ;;
445
446 let names_of_context context = 
447   List.map
448     (function
449        | None -> None
450        | Some (n, e) -> Some n)
451     context
452 ;;
453
454
455 module OrderedTerm =
456 struct
457   type t = Cic.term
458       
459   let compare = Pervasives.compare
460 end
461
462 module TermSet = Set.Make(OrderedTerm);;
463 module TermMap = Map.Make(OrderedTerm);;
464
465 let symbols_of_term term =
466   let module C = Cic in
467   let rec aux map = function
468     | C.Meta _ -> map
469     | C.Appl l ->
470         List.fold_left (fun res t -> (aux res t)) map l
471     | t ->
472         let map = 
473           try
474             let c = TermMap.find t map in
475             TermMap.add t (c+1) map
476           with Not_found ->
477             TermMap.add t 1 map
478         in
479         map
480   in
481   aux TermMap.empty term
482 ;;
483
484
485 let metas_of_term term =
486   let module C = Cic in
487   let rec aux = function
488     | C.Meta _ as t -> TermSet.singleton t
489     | C.Appl l ->
490         List.fold_left (fun res t -> TermSet.union res (aux t)) TermSet.empty l
491     | t -> TermSet.empty (* TODO: maybe add other cases? *)
492   in
493   aux term
494 ;;
495
496
497 let rec lpo t1 t2 =
498   let module C = Cic in
499   match t1, t2 with
500   | t1, t2 when t1 = t2 -> Eq
501   | t1, (C.Meta _ as m) ->
502       if TermSet.mem m (metas_of_term t1) then Gt else Incomparable
503   | (C.Meta _ as m), t2 ->
504       if TermSet.mem m (metas_of_term t2) then Lt else Incomparable
505   | C.Appl (hd1::tl1), C.Appl (hd2::tl2) -> (
506       let res =
507         let f o r t =
508           if r then true else
509             match lpo t o with
510             | Gt | Eq -> true
511             | _ -> false
512         in
513         let res1 = List.fold_left (f t2) false tl1 in
514         if res1 then Gt
515         else let res2 = List.fold_left (f t1) false tl2 in
516         if res2 then Lt
517         else Incomparable
518       in
519       if res <> Incomparable then
520         res
521       else
522         let f o r t =
523           if not r then false else
524             match lpo o t with
525             | Gt -> true
526             | _ -> false
527         in
528         match aux_ordering hd1 hd2 with
529         | Gt ->
530             let res = List.fold_left (f t1) false tl2 in
531             if res then Gt
532             else Incomparable
533         | Lt ->
534             let res = List.fold_left (f t2) false tl1 in
535             if res then Lt
536             else Incomparable
537         | Eq -> (
538             let lex_res =
539               try
540                 List.fold_left2
541                   (fun r t1 t2 -> if r <> Eq then r else lpo t1 t2)
542                   Eq tl1 tl2
543               with Invalid_argument _ ->
544                 Incomparable
545             in
546             match lex_res with
547             | Gt ->
548                 if List.fold_left (f t1) false tl2 then Gt
549                 else Incomparable
550             | Lt ->
551                 if List.fold_left (f t2) false tl1 then Lt
552                 else Incomparable
553             | _ -> Incomparable
554           )
555         | _ -> Incomparable
556     )
557   | t1, t2 -> aux_ordering t1 t2
558 ;;
559
560
561 (* settable by the user... *)
562 let compare_terms = ref nonrec_kbo;; 
563 (* let compare_terms = ref ao;; *)
564
565 let guarded_simpl context t =
566   let t' = ProofEngineReduction.simpl context t in
567   let simpl_order = !compare_terms t t' in
568   if simpl_order = Gt then 
569     (* prerr_endline ("reduce: "^(CicPp.ppterm t)^(CicPp.ppterm t')); *)
570   t'
571   else t
572 ;;
573
574 type equality_sign = Negative | Positive;;
575
576 let string_of_sign = function
577   | Negative -> "Negative"
578   | Positive -> "Positive"
579 ;;
580
581
582 type pos = Left | Right 
583
584 let string_of_pos = function
585   | Left -> "Left"
586   | Right -> "Right"
587 ;;
588
589
590 let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ())
591 let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ())
592 let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ())
593 let eq_XURI () =
594   let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
595   UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
596 let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())