X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=f5233d03dbab9e907e5c02711729023019b32afa;hb=ba9a57375b50e0527bf0d48f189f7e3129bbe99f;hp=d8ff4a7d9d116537f963b222f92da5da379c62d0;hpb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index d8ff4a7d9..f5233d03d 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1,6 +1,26 @@ open Utils;; +type equality = + int * (* weight *) + (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 = + | BasicProof of Cic.term + | ProofBlock of + Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) * + equality + | NoProof +;; + + let string_of_equality ?env = match env with | None -> ( @@ -20,6 +40,45 @@ let string_of_equality ?env = ;; +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 + match proof with + | NoProof -> + Printf.fprintf stderr "WARNING: no proof for %s\n" + (string_of_equality equality); + Cic.Implicit None + | BasicProof term -> term + | ProofBlock (subst, eq_URI, t', (pos, eq), eq') -> +(* 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 what, other = if pos = Utils.Left then what, other else other, what in + CicMetaSubst.apply_subst subst + (Cic.Appl [Cic.Const (eq_URI, []); ty; + what; t'; eqproof; other; proof']) +;; + + let rec metas_of_term = function | Cic.Meta (i, c) -> [i] | Cic.Var (_, ens) @@ -933,17 +992,6 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) ;; -type equality = - Cic.term * (* proof *) - (Cic.term * (* type *) - Cic.term * (* left side *) - Cic.term * (* right side *) - Utils.comparison) * (* ordering *) - Cic.metasenv * (* environment for metas *) - Cic.term list (* arguments *) -;; - - let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = let module C = Cic in let module S = CicSubstitution in @@ -978,14 +1026,20 @@ 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 - Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1) + 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 ) | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> let t1 = S.lift index t1 and t2 = S.lift index t2 in let o = !Utils.compare_terms t1 t2 in - Some (C.Rel index, (ty, t1, t2, o), [], []), (newmeta+1) + 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 in ( match do_find context term with @@ -1002,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 @@ -1038,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)) ;; @@ -1047,7 +1101,11 @@ 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 - (proof, (ty, t1, t2, o), [], []) + 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), [], []) *) | _ -> raise TermIsNotAnEquality ;; @@ -1056,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 @@ -1257,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 @@ -1273,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 @@ -1470,6 +1531,7 @@ let subsumption env target source = ); res ;; +*) let extract_differing_subterms t1 t2 =