From: Alberto Griggio Date: Fri, 1 Jul 2005 14:28:02 +0000 (+0000) Subject: removed first Cic.term from type equality, added an int (weight of the equality) X-Git-Tag: PRE_GETTER_STORAGE~62 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2daf59a983cae8151e513196577ae77b1d12e157;p=helm.git removed first Cic.term from type equality, added an int (weight of the equality) --- diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 6425e3c82..c50d809ac 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -419,7 +419,8 @@ let rec demodulation newmeta env table target = build_newtarget_time := !build_newtarget_time +. (time2 -. time1); let res = - (C.Implicit None, (eq_ty, left, right, ordering), newmetasenv, newargs) + let w = Utils.compute_equality_weight eq_ty left right in + (w, (eq_ty, left, right, ordering), newmetasenv, newargs) in Inference.store_proof res newproof; newmeta, res @@ -602,7 +603,10 @@ let superposition_left (metasenv, context, ugraph) table target = let time2 = Unix.gettimeofday () in build_newtarget_time := !build_newtarget_time +. (time2 -. time1); - let res = (C.Implicit None, (eq_ty, left, right, neworder), [], []) in + let res = + let w = Utils.compute_equality_weight eq_ty left right in + (w, (eq_ty, left, right, neworder), [], []) + in Inference.store_proof res newproof; res in @@ -668,7 +672,8 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = and newmenv = newmetas @ menv' and newargs = args @ args' in let eq' = - (C.Implicit None, (eq_ty, left, right, neworder), newmenv, newargs) + let w = Utils.compute_equality_weight eq_ty left right in + (w, (eq_ty, left, right, neworder), newmenv, newargs) and env = (metasenv, context, ugraph) in let newm, eq' = Inference.fix_metas !maxmeta eq' in newm, eq' diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 163fabddb..f5233d03d 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -2,7 +2,7 @@ open Utils;; type equality = - Cic.term * (* proof *) + int * (* weight *) (Cic.term * (* type *) Cic.term * (* left side *) Cic.term * (* right side *) @@ -1026,7 +1026,8 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> Printf.printf "OK: %s\n" (CicPp.ppterm term); let o = !Utils.compare_terms t1 t2 in - let e = (p, (ty, t1, t2, o), newmetas, args) in + let w = compute_equality_weight ty t1 t2 in + let e = (w, (ty, t1, t2, o), newmetas, args) in store_proof e (BasicProof p); Some e, (newmeta+1) | _ -> None, newmeta @@ -1035,7 +1036,8 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = let t1 = S.lift index t1 and t2 = S.lift index t2 in let o = !Utils.compare_terms t1 t2 in - let e = (C.Rel index, (ty, t1, t2, o), [], []) in + let w = compute_equality_weight ty t1 t2 in + let e = (w, (ty, t1, t2, o), [], []) in store_proof e (BasicProof (C.Rel index)); Some e, (newmeta+1) | _ -> None, newmeta @@ -1054,7 +1056,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = ;; -let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) = +let fix_metas newmeta ((weight, (ty, left, right, o), menv, args) as equality) = let table = Hashtbl.create (List.length args) in let newargs, _ = List.fold_right @@ -1090,7 +1092,7 @@ let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) = (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs in (newmeta + (List.length newargs) + 1, - (repl proof, (ty, left, right, o), menv', newargs)) + (weight, (ty, left, right, o), menv', newargs)) ;; @@ -1099,7 +1101,8 @@ exception TermIsNotAnEquality;; let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> let o = !Utils.compare_terms t1 t2 in - let e = (proof, (ty, t1, t2, o), [], []) in + let w = compute_equality_weight ty t1 t2 in + let e = (w, (ty, t1, t2, o), [], []) in store_proof e (BasicProof proof); e (* (proof, (ty, t1, t2, o), [], []) *) @@ -1111,6 +1114,7 @@ let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; +(* let superposition_left (metasenv, context, ugraph) target source = let module C = Cic in let module S = CicSubstitution in @@ -1312,6 +1316,7 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = (!maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))) ;; +*) let is_identity ((_, context, ugraph) as env) = function @@ -1328,6 +1333,7 @@ let is_identity ((_, context, ugraph) as env) = function ;; +(* let demodulation newmeta (metasenv, context, ugraph) target source = let module C = Cic in let module S = CicSubstitution in @@ -1525,6 +1531,7 @@ let subsumption env target source = ); res ;; +*) let extract_differing_subterms t1 t2 = diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 74194e84a..aa2b9231d 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -1,5 +1,5 @@ type equality = - Cic.term * (* proof *) + int * (* weight *) (Cic.term * (* type *) Cic.term * (* left side *) Cic.term * (* right side *) @@ -66,7 +66,7 @@ val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term -> returns a list of new clauses inferred with a left superposition step the negative equation "target" and the positive equation "source" *) -val superposition_left: environment -> equality -> equality -> equality list +(* val superposition_left: environment -> equality -> equality -> equality list *) (** superposition_right newmeta env target source @@ -75,10 +75,10 @@ val superposition_left: environment -> equality -> equality -> equality list "newmeta" is the first free meta index, i.e. the first number above the highest meta index: its updated value is also returned *) -val superposition_right: - int -> environment -> equality -> equality -> int * equality list +(* val superposition_right: *) +(* int -> environment -> equality -> equality -> int * equality list *) -val demodulation: int -> environment -> equality -> equality -> int * equality +(* val demodulation: int -> environment -> equality -> equality -> int * equality *) val meta_convertibility_eq: equality -> equality -> bool @@ -86,7 +86,7 @@ val is_identity: environment -> equality -> bool val string_of_equality: ?env:environment -> equality -> string -val subsumption: environment -> equality -> equality -> bool +(* val subsumption: environment -> equality -> equality -> bool *) val metas_of_term: Cic.term -> int list diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 793e48423..877e5929a 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -64,17 +64,6 @@ let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) = ;; -let weight_of_equality (_, (ty, left, right, _), _, _) = - let meta_number = ref 0 in - let weight_of t = - let weight, ml = weight_of_term t in - meta_number := !meta_number + (List.fold_left (fun r (_, n) -> r+n) 0 ml); - weight - in - (weight_of ty) + (weight_of left) + (weight_of right), meta_number -;; - - module OrderedEquality = struct type t = Inference.equality @@ -82,17 +71,25 @@ module OrderedEquality = struct match meta_convertibility_eq eq1 eq2 with | true -> 0 | false -> - let _, (ty, left, right, _), _, _ = eq1 - and _, (ty', left', right', _), _, _ = eq2 in -(* let w1, m1 = weight_of_equality eq1 *) -(* and w2, m2 = weight_of_equality eq2 in *) - let weight_of t = fst (weight_of_term ~consider_metas:false t) in - let w1 = (weight_of ty) + (weight_of left) + (weight_of right) - and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in + let w1, (ty, left, right, _), _, a = eq1 + and w2, (ty', left', right', _), _, a' = eq2 in +(* let weight_of t = fst (weight_of_term ~consider_metas:false t) in *) +(* let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *) +(* and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *) match Pervasives.compare w1 w2 with - | 0 -> Pervasives.compare eq1 eq2 -(* let res = Pervasives.compare m1 m2 in *) -(* if res = 0 then Pervasives.compare eq1 eq2 else res *) + | 0 -> + let res = (List.length a) - (List.length a') in + if res <> 0 then res else ( + try + let res = Pervasives.compare (List.hd a) (List.hd a') in + if res <> 0 then res else Pervasives.compare eq1 eq2 + with _ -> Pervasives.compare eq1 eq2 +(* match a, a' with *) +(* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *) +(* let res = Pervasives.compare i j in *) +(* if res <> 0 then res else Pervasives.compare eq1 eq2 *) +(* | _, _ -> Pervasives.compare eq1 eq2 *) + ) | res -> res end diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 52d99327e..42703045d 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -83,6 +83,12 @@ let weight_of_term ?(consider_metas=true) term = ;; +let compute_equality_weight ty left right = + let weight_of t = fst (weight_of_term ~consider_metas:false t) in + (weight_of ty) + (weight_of left) + (weight_of right) +;; + + (* 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: diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index 612f07cf0..e69caed4d 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -39,3 +39,5 @@ val string_of_sign: equality_sign -> string type pos = Left | Right val string_of_pos: pos -> string + +val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int