X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=62308896fd02b6b89bb420bd9c2c501c99273e54;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=f5233d03dbab9e907e5c02711729023019b32afa;hpb=2daf59a983cae8151e513196577ae77b1d12e157;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index f5233d03d..62308896f 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -3,20 +3,21 @@ open Utils;; type equality = 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 @@ -1004,18 +996,10 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = match term with | C.Prod (name, s, t) -> (* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *) - let (head, newmetas, args, _) = - PrimitiveTactics.new_metasenv_for_apply newmeta proof + let (head, newmetas, args, newmeta) = + ProofEngineHelpers.saturate_term newmeta [] context (S.lift index term) in - let newmeta = - List.fold_left - (fun maxm arg -> - match arg with - | C.Meta (i, _) -> (max maxm i) - | _ -> assert false) - newmeta args - in let p = if List.length args = 0 then C.Rel index @@ -1027,8 +1011,8 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = Printf.printf "OK: %s\n" (CicPp.ppterm term); let o = !Utils.compare_terms t1 t2 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); + let proof = BasicProof p in + let e = (w, proof, (ty, t1, t2, o), newmetas, args) in Some e, (newmeta+1) | _ -> None, newmeta ) @@ -1037,8 +1021,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = and t2 = S.lift index t2 in let o = !Utils.compare_terms t1 t2 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)); + let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in Some e, (newmeta+1) | _ -> None, newmeta in ( @@ -1056,7 +1039,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = ;; -let fix_metas newmeta ((weight, (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 @@ -1092,7 +1075,7 @@ let fix_metas newmeta ((weight, (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, - (weight, (ty, left, right, o), menv', newargs)) + (w, p, (ty, left, right, o), menv', newargs)) ;; @@ -1102,8 +1085,7 @@ 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 w = compute_equality_weight ty t1 t2 in - let e = (w, (ty, t1, t2, o), [], []) in - store_proof e (BasicProof proof); + let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in e (* (proof, (ty, t1, t2, o), [], []) *) | _ -> @@ -1320,16 +1302,9 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = 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))) ;;