X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Futils.ml;h=a558001a5ee0746a0b87e0ddc366bbb696473917;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=f2c475799cf818e2aebec504efd2af369823d53e;hpb=a89f7271e79dc7dc81dc868a75125669c8decc16;p=helm.git diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index f2c475799..a558001a5 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -1,3 +1,33 @@ +(* 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);; + + let print_metasenv metasenv = String.concat "\n--------------------------\n" (List.map (fun (i, context, term) -> @@ -7,8 +37,8 @@ let print_metasenv metasenv = ;; -let print_subst subst = - String.concat "\n" +let print_subst ?(prefix="\n") subst = + String.concat prefix (List.map (fun (i, (c, t, ty)) -> Printf.sprintf "?%d -> %s : %s" i @@ -28,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 @@ -83,14 +111,34 @@ let weight_of_term ?(consider_metas=true) term = ;; +module OrderedInt = struct + type t = int + + let compare = Pervasives.compare +end + +module IntSet = Set.Make(OrderedInt) + +let compute_equality_weight ty left right = + let metasw = ref 0 in + let weight_of t = + let w, m = (weight_of_term ~consider_metas:true t) in + metasw := !metasw + (2 * (List.length 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 +;; + + (* returns a "normalized" version of the polynomial weight wl (with type * weight list), i.e. a list sorted ascending by meta number, * from 0 to maxmeta. wl must be sorted descending by meta number. Example: * 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)) @@ -125,6 +173,7 @@ let normalize_weights (cw1, wl1) (cw2, wl2) = | (m, w)::tl1, [] -> let res1, res2 = aux tl1 [] in (m, w)::res1, (m, 0)::res2 + | _, _ -> assert false in let cmp (m, _) (n, _) = compare m n in let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in @@ -147,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) @@ -173,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 @@ -204,10 +247,11 @@ let compare_weights ?(normalize=false) if (- diffs) >= hdiff then Ge else Incomparable | (m, _, n) when m > 0 && n > 0 -> Incomparable + | _ -> assert false ;; -let rec aux_ordering t1 t2 = +let rec aux_ordering ?(recursion=true) t1 t2 = let module C = Cic in let compare_uris u1 u2 = let res = @@ -239,7 +283,7 @@ let rec aux_ordering t1 t2 = | C.MutConstruct _, _ -> Lt | _, C.MutConstruct _ -> Gt - | C.Appl l1, C.Appl l2 -> + | C.Appl l1, C.Appl l2 when recursion -> let rec cmp t1 t2 = match t1, t2 with | [], [] -> Eq @@ -251,10 +295,14 @@ let rec aux_ordering t1 t2 = else o in cmp l1 l2 + | C.Appl (h1::t1), C.Appl (h2::t2) when not recursion -> + aux_ordering h1 h2 | t1, t2 -> - Printf.printf "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 ;; @@ -280,6 +328,54 @@ let nonrec_kbo t1 t2 = ;; +let rec kbo t1 t2 = + 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 +;; + + let names_of_context context = List.map (function @@ -413,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 ())