X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Finference.ml;h=f040241223bf3996f0972f3df4a4fcc8acbb89be;hb=4ab3123d6a8e5080009d7b471b0cefd05f4817ed;hp=36e9f99a64a710785976c200979d0764620bc849;hpb=1d973a067d441fbae43905abb704e21faa223e2b;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml index 36e9f99a6..f04024122 100644 --- a/helm/software/components/tactics/paramodulation/inference.ml +++ b/helm/software/components/tactics/paramodulation/inference.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -let _profiler = <:profiler<_profiler>>;; +(* let _profiler = <:profiler<_profiler>>;; *) (* $Id$ *) @@ -51,7 +51,7 @@ let rec check_irl start = function let rec is_simple_term = function | Cic.Appl ((Cic.Meta _)::_) -> false | Cic.Appl l -> List.for_all is_simple_term l - | Cic.Meta (i, l) -> check_irl 1 l + | Cic.Meta (i, l) -> let l = [] in check_irl 1 l | Cic.Rel _ -> true | Cic.Const _ -> true | Cic.MutInd (_, _, []) -> true @@ -70,7 +70,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = let lookup = Subst.lookup_subst in let rec occurs_check subst what where = match where with - | t when what = t -> true + | Cic.Meta(i,_) when i = what -> true | C.Appl l -> List.exists (occurs_check subst what) l | C.Meta _ -> let t = lookup where subst in @@ -84,6 +84,9 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = in match s, t with | s, t when s = t -> subst, menv + (* sometimes the same meta has different local contexts; this + could create "cyclic" substitutions *) + | C.Meta (i, _), C.Meta (j, _) when i=j -> subst, menv | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) &&(locked locked_menv j) -> raise @@ -92,7 +95,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = unif subst menv t s | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) -> unif subst menv t s - | C.Meta _, t when occurs_check subst s t -> + | C.Meta (i,_), t when occurs_check subst i t -> raise (U.UnificationFailure (lazy "Inference.unification.unif")) | C.Meta (i, l), t when (locked locked_menv i) -> @@ -140,8 +143,8 @@ let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]" let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph = let metasenv = - HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2)) - (*metasenv1 @ metasenv2*) + HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2)) + (* metasenv1 @ metasenv2 *) in let subst, menv, ug = if not (is_simple_term t1) || not (is_simple_term t2) then ( @@ -211,7 +214,6 @@ let find_equalities context proof = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in - let eq_uri = LibraryObjects.eq_URI () in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let ok_types ty menv = List.for_all (fun (_, _, mt) -> mt = ty) menv @@ -234,20 +236,22 @@ let find_equalities context proof = in ( match head with | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] - when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) -> + when (LibraryObjects.is_eq_URI uri) && + (ok_types ty newmetas) -> debug_print (lazy (Printf.sprintf "OK: %s" (CicPp.ppterm term))); let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in - let w = compute_equality_weight stat in + (* let w = compute_equality_weight stat in *) + let w = 0 in let proof = Equality.Exact p in let e = Equality.mk_equality (w, proof, stat, newmetas) in Some e, (newmeta+1) | _ -> None, newmeta ) | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] - when UriManager.eq uri eq_uri -> + when LibraryObjects.is_eq_URI uri -> let ty = S.lift index ty in let t1 = S.lift index t1 in let t2 = S.lift index t2 in @@ -315,43 +319,65 @@ let equations_blacklist = *) let equations_blacklist = UriManager.UriSet.empty;; +let tty_of_u u = +(* let _ = <:start> in *) + let t = CicUtil.term_of_uri u in + let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in +(* let _ = <:stop> in *) + t, ty +;; + +let utty_of_u u = + let t,ty = tty_of_u u in + u, t, ty +;; -let find_library_equalities dbd context status maxmeta = +let find_library_equalities caso_strano dbd context status maxmeta = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in - let blacklist = - List.fold_left - (fun s u -> UriManager.UriSet.add u s) - equations_blacklist - [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI (); - eq_ind_r_URI ()] +(* let _ = <:start> in *) + let signature = + if caso_strano then + begin + let proof, goalno = status in + let _,metasenv,_,_ = proof in + let metano,context,ty = CicUtil.lookup_meta goalno metasenv in + match ty with + | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] -> + (let mainl, sigl = MetadataConstraints.signature_of l in + let mainr, sigr = MetadataConstraints.signature_of r in + match mainl,mainr with + | Some (uril,tyl), Some (urir, tyr) + when LibraryObjects.is_eq_URI uril && + LibraryObjects.is_eq_URI urir && + tyl = tyr -> + Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr) + | _ -> + let u = (UriManager.uri_of_string + (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in + let main = Some (u, []) in + Some (main,MetadataConstraints.UriManagerSet.union sigl sigr)) + | _ -> assert false + end + else + None in + let eqs = (MetadataQuery.equations_for_goal ~dbd ?signature status) in +(* let _ = <:stop> in *) let candidates = List.fold_left (fun l uri -> - if UriManager.UriSet.mem uri blacklist then + if LibraryObjects.is_eq_refl_URI uri || + LibraryObjects.is_sym_eq_URI uri || + LibraryObjects.is_trans_eq_URI uri || + LibraryObjects.is_eq_ind_URI uri || + LibraryObjects.is_eq_ind_r_URI uri + then l else - let t = CicUtil.term_of_uri uri in - let ty, _ = - CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph - in - (uri, t, ty)::l) - [] - (let t1 = Unix.gettimeofday () in - let eqs = (MetadataQuery.equations_for_goal ~dbd status) in - let t2 = Unix.gettimeofday () in - (debug_print - (lazy - (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n" - (t2 -. t1)))); - eqs) - in - let eq_uri1 = eq_XURI () - and eq_uri2 = LibraryObjects.eq_URI () in - let iseq uri = - (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2) + (utty_of_u uri)::l) + [] eqs in let ok_types ty menv = List.for_all (fun (_, _, mt) -> mt = ty) menv @@ -386,7 +412,9 @@ let find_library_equalities dbd context status maxmeta = in ( match head with | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] - when (iseq uri) && (ok_types ty newmetas) -> + when (LibraryObjects.is_eq_URI uri || + LibraryObjects.is_eq_refl_URI uri) && + (ok_types ty newmetas) -> debug_print (lazy (Printf.sprintf "OK: %s" (CicPp.ppterm term))); @@ -399,7 +427,10 @@ let find_library_equalities dbd context status maxmeta = | _ -> None, newmeta ) | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] - when iseq uri && not (has_vars termty) -> + when + (LibraryObjects.is_eq_URI uri || + LibraryObjects.is_eq_refl_URI uri) && + not (has_vars termty) -> let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in @@ -439,36 +470,33 @@ let find_library_theorems dbd env status equalities_uris = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in - let blacklist = - let refl_equal = - UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in - let s = - UriManager.UriSet.remove refl_equal - (UriManager.UriSet.union equalities_uris equations_blacklist) - in - List.fold_left - (fun s u -> UriManager.UriSet.add u s) - s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI (); - eq_ind_r_URI ()] - in - let metasenv, context, ugraph = env in let candidates = List.fold_left (fun l uri -> - if UriManager.UriSet.mem uri blacklist then l + if LibraryObjects.is_sym_eq_URI uri || + LibraryObjects.is_trans_eq_URI uri || + LibraryObjects.is_eq_ind_URI uri || + LibraryObjects.is_eq_ind_r_URI uri + then l else - let t = CicUtil.term_of_uri uri in - let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in - (t, ty, [])::l) + (let t,ty = tty_of_u uri in t, ty, [] )::l) [] (MetadataQuery.signature_of_goal ~dbd status) in let refl_equal = - let u = eq_XURI () in - let t = CicUtil.term_of_uri u in + let eq = + match LibraryObjects.eq_URI () with + | Some u -> u + | None -> + raise + (ProofEngineTypes.Fail + (lazy "No default eq defined when running find_library_theorems")) + in + let t = CicUtil.term_of_uri (LibraryObjects.eq_refl_URI ~eq) in let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in (t, ty, []) in - refl_equal::candidates + let res = refl_equal::candidates in + res ;; @@ -492,4 +520,4 @@ let find_context_hypotheses env equalities_indexes = res ;; -let get_stats () = <:show> ;; +let get_stats () = "" (*<:show>*) ;;