X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Finference.ml;h=e2f85fa2b4acce69dfa6604b1c92799234771bf1;hb=50844b0116c863862434c7c673c5caaf6ff78cdf;hp=6004de44ceb29ef815daf390b824678aa8863ef3;hpb=5f53c5415d0bde33509eb53db7ef230819266420;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml index 6004de44c..e2f85fa2b 100644 --- a/helm/software/components/tactics/paramodulation/inference.ml +++ b/helm/software/components/tactics/paramodulation/inference.ml @@ -211,7 +211,6 @@ let find_equalities context proof = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in - let eq_uri = Utils.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,7 +233,8 @@ 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))); @@ -247,7 +247,7 @@ let find_equalities context proof = | _ -> 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 +315,39 @@ 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 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 ()] - in + let _ = <:start> in + let eqs = (MetadataQuery.equations_for_goal ~dbd 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 = Utils.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 +382,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 +397,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 +440,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 ;;