X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Futils.ml;h=a558001a5ee0746a0b87e0ddc366bbb696473917;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=681a371e1a6f71c60e90d7021aa1a8aa121c0688;hpb=cfda0acfce3f5e0b843bfe2b7ba7c371e5690db0;p=helm.git diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 681a371e1..a558001a5 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + let debug = true;; let debug_print s = if debug then prerr_endline (Lazy.force s);; @@ -33,8 +58,6 @@ let string_of_weight (cw, mw) = let weight_of_term ?(consider_metas=true) term = - (* ALB: what to consider as a variable? I think "variables" in our case are - Metas and maybe Rels... *) let module C = Cic in let vars_dict = Hashtbl.create 5 in let rec aux = function @@ -97,21 +120,16 @@ end module IntSet = Set.Make(OrderedInt) let compute_equality_weight ty left right = -(* let metasw = ref IntSet.empty in *) let metasw = ref 0 in let weight_of t = - let w, m = (weight_of_term ~consider_metas:true(* false *) t) in -(* let mw = List.fold_left (fun mw (_, c) -> mw + 2 * c) 0 m in *) -(* metasw := !metasw + mw; *) + let w, m = (weight_of_term ~consider_metas:true t) in metasw := !metasw + (2 * (List.length m)); -(* metasw := List.fold_left (fun s (i, _) -> IntSet.add i s) !metasw m; *) w in (* Warning: the following let cannot be expanded since it forces the right evaluation order!!!! *) let w = (weight_of ty) + (weight_of left) + (weight_of right) in w + !metasw -(* (4 * IntSet.cardinal !metasw) *) ;; @@ -121,8 +139,6 @@ let compute_equality_weight ty left right = * normalize_weight 5 (3, [(3, 2); (1, 1)]) -> * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *) let normalize_weight maxmeta (cw, wl) = -(* Printf.printf "normalize_weight: %d, %s\n" maxmeta *) -(* (string_of_weight (cw, wl)); *) let rec aux = function | 0 -> [] | m -> (m, 0)::(aux (m-1)) @@ -180,16 +196,6 @@ let compare_weights ?(normalize=false) ((h1, w1) as weight1) ((h2, w2) as weight2)= let (h1, w1), (h2, w2) = if normalize then -(* let maxmeta = *) -(* let maxmeta l = *) -(* try *) -(* match List.hd l with *) -(* | (m, _) -> m *) -(* with Failure _ -> 0 *) -(* in *) -(* max (maxmeta w1) (maxmeta w2) *) -(* in *) -(* (normalize_weight maxmeta (h1, w1)), (normalize_weight maxmeta (h2, w2)) *) normalize_weights weight1 weight2 else (h1, w1), (h2, w2) @@ -206,15 +212,19 @@ let compare_weights ?(normalize=false) else if r = 0 then (lt, eq+1, gt), diffs else (lt, eq, gt+1), diffs | (meta1, w1), (meta2, w2) -> - Printf.printf "HMMM!!!! %s, %s\n" - (string_of_weight weight1) (string_of_weight weight2); + debug_print + (lazy + (Printf.sprintf "HMMM!!!! %s, %s\n" + (string_of_weight weight1) (string_of_weight weight2))); assert false) ((0, 0, 0), 0) w1 w2 with Invalid_argument _ -> - Printf.printf "Invalid_argument: %s{%s}, %s{%s}, normalize = %s\n" - (string_of_weight (h1, w1)) (string_of_weight weight1) - (string_of_weight (h2, w2)) (string_of_weight weight2) - (string_of_bool normalize); + debug_print + (lazy + (Printf.sprintf "Invalid_argument: %s{%s}, %s{%s}, normalize = %s\n" + (string_of_weight (h1, w1)) (string_of_weight weight1) + (string_of_weight (h2, w2)) (string_of_weight weight2) + (string_of_bool normalize))); assert false in let hdiff = h1 - h2 in @@ -289,9 +299,10 @@ let rec aux_ordering ?(recursion=true) t1 t2 = aux_ordering h1 h2 | t1, t2 -> - debug_print (lazy ( - Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n" - (CicPp.ppterm t1) (CicPp.ppterm t2))); + debug_print + (lazy + (Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n" + (CicPp.ppterm t1) (CicPp.ppterm t2))); Incomparable ;; @@ -318,64 +329,50 @@ let nonrec_kbo t1 t2 = let rec kbo t1 t2 = -(* debug_print (lazy ( *) -(* Printf.sprintf "kbo %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2))); *) -(* if t1 = t2 then *) -(* Eq *) -(* else *) - let aux = aux_ordering ~recursion:false in - let w1 = weight_of_term t1 - and w2 = weight_of_term t2 in - let rec cmp t1 t2 = - match t1, t2 with - | [], [] -> Eq - | _, [] -> Gt - | [], _ -> Lt - | hd1::tl1, hd2::tl2 -> - let o = -(* debug_print (lazy ( *) -(* Printf.sprintf "recursion kbo on %s %s" *) -(* (CicPp.ppterm hd1) (CicPp.ppterm hd2))); *) - kbo hd1 hd2 - in - if o = Eq then cmp tl1 tl2 - else o - in - let comparison = compare_weights ~normalize:true w1 w2 in -(* debug_print (lazy ( *) -(* Printf.sprintf "Weights are: %s %s: %s" *) -(* (string_of_weight w1) (string_of_weight w2) *) -(* (string_of_comparison comparison))); *) - match comparison with - | Le -> - let r = aux t1 t2 in -(* debug_print (lazy ("HERE! " ^ (string_of_comparison r))); *) - if r = Lt then Lt - else if r = Eq then ( - match t1, t2 with - | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> - if cmp tl1 tl2 = Lt then Lt else Incomparable - | _, _ -> Incomparable - ) else Incomparable - | Ge -> - let r = aux t1 t2 in - if r = Gt then Gt - else if r = Eq then ( - match t1, t2 with - | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> - if cmp tl1 tl2 = Gt then Gt else Incomparable - | _, _ -> Incomparable - ) else Incomparable - | Eq -> - let r = aux t1 t2 in - if r = Eq then ( - match t1, t2 with - | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> -(* if cmp tl1 tl2 = Gt then Gt else Incomparable *) - cmp tl1 tl2 - | _, _ -> Incomparable - ) else r - | res -> res + let aux = aux_ordering ~recursion:false in + let w1 = weight_of_term t1 + and w2 = weight_of_term t2 in + let rec cmp t1 t2 = + match t1, t2 with + | [], [] -> Eq + | _, [] -> Gt + | [], _ -> Lt + | hd1::tl1, hd2::tl2 -> + let o = + kbo hd1 hd2 + in + if o = Eq then cmp tl1 tl2 + else o + in + let comparison = compare_weights ~normalize:true w1 w2 in + match comparison with + | Le -> + let r = aux t1 t2 in + if r = Lt then Lt + else if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + if cmp tl1 tl2 = Lt then Lt else Incomparable + | _, _ -> Incomparable + ) else Incomparable + | Ge -> + let r = aux t1 t2 in + if r = Gt then Gt + else if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + if cmp tl1 tl2 = Gt then Gt else Incomparable + | _, _ -> Incomparable + ) else Incomparable + | Eq -> + let r = aux t1 t2 in + if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + cmp tl1 tl2 + | _, _ -> Incomparable + ) else r + | res -> res ;; @@ -512,3 +509,12 @@ let string_of_pos = function | Left -> "Left" | Right -> "Right" ;; + + +let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ()) +let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ()) +let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ()) +let eq_XURI () = + let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in + UriManager.uri_of_string (s ^ "#xpointer(1/1/1)") +let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())