X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=fad86a854aeec9f7db327e70ba0dfec5cee78de8;hb=22964c949671af4b5e739b06b915a81a4fc2c5b5;hp=163fabddbac6ebf6e04eaac05363615b9839ac02;hpb=c9d7e6a946744890def5b5471c93b4dbd78c4ac9;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 163fabddb..fad86a854 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -2,21 +2,22 @@ open Utils;; type equality = - Cic.term * (* proof *) + int * (* weight *) + proof * (Cic.term * (* type *) Cic.term * (* left side *) Cic.term * (* right side *) Utils.comparison) * (* ordering *) Cic.metasenv * (* environment for metas *) Cic.term list (* arguments *) -;; - -type proof = +and proof = | BasicProof of Cic.term | ProofBlock of - Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) * - equality + Cic.substitution * UriManager.uri * + (* name, ty, eq_ty, left, right *) + (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * + (Utils.pos * equality) * equality | NoProof ;; @@ -25,40 +26,25 @@ let string_of_equality ?env = match env with | None -> ( function - | _, (ty, left, right, o), _, _ -> - Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty) + | w, _, (ty, left, right, o), _, _ -> + Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty) (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right) ) | Some (_, context, _) -> ( let names = names_of_context context in function - | _, (ty, left, right, o), _, _ -> - Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names) + | w, _, (ty, left, right, o), _, _ -> + Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names) (CicPp.pp left names) (string_of_comparison o) (CicPp.pp right names) ) ;; -let prooftable = Hashtbl.create 2001;; - -let store_proof equality proof = - if not (Hashtbl.mem prooftable equality) then - Hashtbl.add prooftable equality proof -;; - - -let delete_proof equality = -(* Printf.printf "| Removing proof of %s" (string_of_equality equality); *) -(* print_newline (); *) - Hashtbl.remove prooftable equality -;; - - let rec build_term_proof equality = (* Printf.printf "build_term_proof %s" (string_of_equality equality); *) (* print_newline (); *) - let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in + let _, proof, _, _, _ = equality in match proof with | NoProof -> Printf.fprintf stderr "WARNING: no proof for %s\n" @@ -66,12 +52,18 @@ let rec build_term_proof equality = Cic.Implicit None | BasicProof term -> term | ProofBlock (subst, eq_URI, t', (pos, eq), eq') -> + let name, ty, eq_ty, left, right = t' in + let bo = + Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); + eq_ty; left; right] + in + let t' = Cic.Lambda (name, ty, CicSubstitution.lift 1 bo) in (* Printf.printf " ProofBlock: eq = %s, eq' = %s" *) (* (string_of_equality eq) (string_of_equality eq'); *) (* print_newline (); *) let proof' = build_term_proof eq in let eqproof = build_term_proof eq' in - let _, (ty, what, other, _), menv', args' = eq in + let _, _, (ty, what, other, _), menv', args' = eq in let what, other = if pos = Utils.Left then what, other else other, what in CicMetaSubst.apply_subst subst (Cic.Appl [Cic.Const (eq_URI, []); ty; @@ -220,8 +212,8 @@ let meta_convertibility_aux table t1 t2 = let meta_convertibility_eq eq1 eq2 = - let _, (ty, left, right, _), _, _ = eq1 - and _, (ty', left', right', _), _, _ = eq2 in + let _, _, (ty, left, right, _), _, _ = eq1 + and _, _, (ty', left', right', _), _, _ = eq2 in if ty <> ty' then false else if (left = left') && (right = right') then @@ -1026,8 +1018,9 @@ 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 - store_proof e (BasicProof p); + let w = compute_equality_weight ty t1 t2 in + let proof = BasicProof p in + let e = (w, proof, (ty, t1, t2, o), newmetas, args) in Some e, (newmeta+1) | _ -> None, newmeta ) @@ -1035,8 +1028,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 - store_proof e (BasicProof (C.Rel index)); + let w = compute_equality_weight ty t1 t2 in + let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in Some e, (newmeta+1) | _ -> None, newmeta in ( @@ -1054,7 +1047,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 ((w, p, (ty, left, right, o), menv, args) as equality) = let table = Hashtbl.create (List.length args) in let newargs, _ = List.fold_right @@ -1090,7 +1083,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)) + (w, p, (ty, left, right, o), menv', newargs)) ;; @@ -1099,8 +1092,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 - store_proof e (BasicProof proof); + let w = compute_equality_weight ty t1 t2 in + let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in e (* (proof, (ty, t1, t2, o), [], []) *) | _ -> @@ -1111,6 +1104,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,22 +1306,17 @@ 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 - | ((_, (ty, left, right, _), _, _) as equality) -> - let res = - (left = right || - (fst (CicReduction.are_convertible context left right ugraph))) - in -(* if res then ( *) -(* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *) -(* print_newline (); *) -(* ); *) - res + | ((_, _, (ty, left, right, _), _, _) as equality) -> + (left = right || + (fst (CicReduction.are_convertible context left right ugraph))) ;; +(* let demodulation newmeta (metasenv, context, ugraph) target source = let module C = Cic in let module S = CicSubstitution in @@ -1525,6 +1514,7 @@ let subsumption env target source = ); res ;; +*) let extract_differing_subterms t1 t2 =