From: Andrea Asperti Date: Fri, 3 Feb 2006 15:08:45 +0000 (+0000) Subject: snapshot X-Git-Tag: make_still_working~7655 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=273ad2ca7a9d46e7d4c28fa762f43b1bd9e64b07;p=helm.git snapshot --- diff --git a/helm/ocaml/tactics/paramodulation/indexing.ml b/helm/ocaml/tactics/paramodulation/indexing.ml index 8ffde4bdf..5830b0842 100644 --- a/helm/ocaml/tactics/paramodulation/indexing.ml +++ b/helm/ocaml/tactics/paramodulation/indexing.ml @@ -32,6 +32,25 @@ module Index = Equality_indexing.DT (* path tree based indexing *) let debug_print = Utils.debug_print;; +(* +for debugging +let check_equation env equation msg = + let w, proof, (eq_ty, left, right, order), metas, args = equation in + let metasenv, context, ugraph = env in + let metasenv' = metasenv @ metas in + try + CicTypeChecker.type_of_aux' metasenv' context left ugraph; + CicTypeChecker.type_of_aux' metasenv' context right ugraph; + () + with + CicUtil.Meta_not_found _ as exn -> + begin + prerr_endline msg; + prerr_endline (CicPp.ppterm left); + prerr_endline (CicPp.ppterm right); + raise exn + end +*) type retrieval_mode = Matching | Unification;; @@ -530,7 +549,10 @@ let rec demodulation_equality newmeta env table sign target = Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof)) in let left, right = if is_left then newterm, right else left, newterm in - let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in + let m = + (Inference.metas_of_term left) + @ (Inference.metas_of_term right) + @ (Inference.metas_of_term eq_ty) in (* let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') *) let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metasenv' @ menv') and newargs = args @@ -726,7 +748,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = let module HL = HelmLibraryObjects in let module CR = CicReduction in let module U = Utils in - let weight, proof, (eq_ty, left, right, ordering), _, _ = target in + let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in let expansions, _ = let term = if ordering = U.Gt then left else right in betaexpand_term metasenv context ugraph table 0 term @@ -800,7 +822,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = let res = let w = Utils.compute_equality_weight eq_ty left right in - (w, newproof, (eq_ty, left, right, neworder), [], []) + (w, newproof, (eq_ty, left, right, neworder), menv @ menv', []) in res in diff --git a/helm/ocaml/tactics/paramodulation/indexing.mli b/helm/ocaml/tactics/paramodulation/indexing.mli index d2807447c..8a6f9c2b6 100644 --- a/helm/ocaml/tactics/paramodulation/indexing.mli +++ b/helm/ocaml/tactics/paramodulation/indexing.mli @@ -53,10 +53,10 @@ val superposition_left : Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> 'a * Inference.proof * - (Index.key * Index.key * Index.key * Utils.comparison) * 'b * 'c -> + (Index.key * Index.key * Index.key * Utils.comparison) * Cic.metasenv * 'c -> int * (int * Inference.proof * - (Index.key * Index.key * Index.key * Utils.comparison) * 'd list * + (Index.key * Index.key * Index.key * Utils.comparison) * Cic.metasenv * 'e list) list val superposition_right : diff --git a/helm/ocaml/tactics/paramodulation/inference.ml b/helm/ocaml/tactics/paramodulation/inference.ml index 21dadc868..dfb67583e 100644 --- a/helm/ocaml/tactics/paramodulation/inference.ml +++ b/helm/ocaml/tactics/paramodulation/inference.ml @@ -574,7 +574,9 @@ let find_equalities context proof = match do_find context term with | Some p, newmeta -> let tl, newmeta' = (aux (index+1) newmeta tl) in - (index, p)::tl, max newmeta newmeta' + if newmeta' < newmeta then + prerr_endline "big trouble"; + (index, p)::tl, newmeta' (* max???? *) | None, _ -> aux (index+1) newmeta tl ) @@ -716,7 +718,9 @@ let find_library_equalities dbd context status maxmeta = match res with | Some e -> let tl, newmeta' = aux newmeta tl in - (uri, e)::tl, max newmeta newmeta' + if newmeta' < newmeta then + prerr_endline "big trouble"; + (uri, e)::tl, newmeta' (* max???? *) | None -> aux newmeta tl in @@ -795,8 +799,9 @@ let find_context_hypotheses env equalities_indexes = ;; -let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) = +let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) = let table = Hashtbl.create (List.length args) in + let newargs, newmeta = List.fold_right (fun t (newargs, index) -> @@ -811,6 +816,7 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) = | _ -> assert false) args ([], newmeta+1) in + let repl where = ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs ~where @@ -828,7 +834,7 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) = let ty = repl ty and left = repl left and right = repl right in - let metas = (metas_of_term left) @ (metas_of_term right) in + let metas = (metas_of_term left) @ (metas_of_term right) @ (metas_of_term ty) in let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in let newargs = List.filter @@ -880,10 +886,54 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) = | p -> assert false in let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in - (newmeta + 1, neweq) + (newmeta +1, neweq) ;; +let relocate newmeta menv = + let subst, metasenv, newmeta = + List.fold_right + (fun (i, context, ty) (subst, menv, maxmeta) -> + let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in + let newsubst = (i, (context, (Cic.Meta (maxmeta, irl)), ty)) in + let newmeta = maxmeta, context, ty in + newsubst::subst, newmeta::menv, maxmeta+1) + menv ([], [], newmeta+1) + in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + let subst = + List.map + (fun (i, (context, term, ty)) -> + let context = CicMetaSubst.apply_subst_context subst context in + let term = CicMetaSubst.apply_subst subst term in + let ty = CicMetaSubst.apply_subst subst ty in + (i, (context, term, ty))) subst in + subst, metasenv, newmeta + + +let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) = + (* debug + let _ , eq = + fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in + prerr_endline (string_of_equality eq); *) + let subst, metasenv, newmeta = relocate newmeta menv in + let ty = CicMetaSubst.apply_subst subst ty in + let left = CicMetaSubst.apply_subst subst left in + let right = CicMetaSubst.apply_subst subst right in + let args = List.map (CicMetaSubst.apply_subst subst) args in + let rec fix_proof = function + | NoProof -> NoProof + | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term) + | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) -> + ProofBlock (subst' @ subst, eq_URI, namety, bo, (pos, eq), p) + | p -> assert false + in + let metas = (metas_of_term left)@(metas_of_term right)@(metas_of_term ty) in + let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in + let eq = (w, fix_proof p, (ty, left, right, o), metasenv, args) in + (* debug prerr_endline (string_of_equality eq); *) + newmeta, eq + let term_is_equality term = let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in match term with diff --git a/helm/ocaml/tactics/paramodulation/saturation.ml b/helm/ocaml/tactics/paramodulation/saturation.ml index 9c4dce460..6a700d868 100644 --- a/helm/ocaml/tactics/paramodulation/saturation.ml +++ b/helm/ocaml/tactics/paramodulation/saturation.ml @@ -28,6 +28,25 @@ open Inference;; open Utils;; +(* +for debugging +let check_equation env equation msg = + let w, proof, (eq_ty, left, right, order), metas, args = equation in + let metasenv, context, ugraph = env in + let metasenv' = metasenv @ metas in + try + CicTypeChecker.type_of_aux' metasenv' context left ugraph; + CicTypeChecker.type_of_aux' metasenv' context right ugraph; + () + with + CicUtil.Meta_not_found _ as exn -> + begin + prerr_endline msg; + prerr_endline (CicPp.ppterm left); + prerr_endline (CicPp.ppterm right); + raise exn + end +*) (* set to false to disable paramodulation inside auto_tac *) let connect_to_auto = true;; @@ -483,22 +502,6 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = let demodulate table current = let newmeta, newcurrent = - let _ = - let w, proof, (eq_ty, left, right, order), metas, args = current in - let metasenv, context, ugraph = env in - let metasenv' = metasenv @ metas in - try - CicTypeChecker.type_of_aux' metasenv' context left ugraph; - CicTypeChecker.type_of_aux' metasenv' context right ugraph; - with - CicUtil.Meta_not_found _ as exn -> - begin - prerr_endline "siamo in forward_simplify"; - prerr_endline (CicPp.ppterm left); - prerr_endline (CicPp.ppterm right); - raise exn - end - in Indexing.demodulation_equality !maxmeta env table sign current in maxmeta := newmeta; if is_identity env newcurrent then @@ -584,22 +587,6 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let demodulate sign table target = let newmeta, newtarget = - let _ = - let w, proof, (eq_ty, left, right, order), metas, args = target in - let metasenv, context, ugraph = env in - let metasenv' = metasenv @ metas in - try - CicTypeChecker.type_of_aux' metasenv' context left ugraph; - CicTypeChecker.type_of_aux' metasenv' context right ugraph; - with - CicUtil.Meta_not_found _ as exn -> - begin - prerr_endline "siamo in forward_simplify_new"; - prerr_endline (CicPp.ppterm left); - prerr_endline (CicPp.ppterm right); - raise exn - end - in Indexing.demodulation_equality !maxmeta env table sign target in maxmeta := newmeta; newtarget @@ -609,11 +596,14 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let new_neg, new_pos = let new_neg = List.map (demodulate Negative active_table) new_neg and new_pos = List.map (demodulate Positive active_table) new_pos in + new_neg,new_pos + +(* PROVA match passive_table with | None -> new_neg, new_pos | Some passive_table -> List.map (demodulate Negative passive_table) new_neg, - List.map (demodulate Positive passive_table) new_pos + List.map (demodulate Positive passive_table) new_pos *) in let t2 = Unix.gettimeofday () in @@ -1853,6 +1843,7 @@ let main dbd full term metasenv ugraph = let _, context, goal = CicUtil.lookup_meta goal' metasenv in let eq_indexes, equalities, maxm = find_equalities context proof in let lib_eq_uris, library_equalities, maxm = + find_library_equalities dbd context (proof, goal') (maxm+2) in let library_equalities = List.map snd library_equalities in @@ -2137,7 +2128,18 @@ let saturate raise (ProofEngineTypes.Fail (lazy "Found a proof, but it doesn't typecheck")) in + let tall = fs_time_info.build_all in + let tdemodulate = fs_time_info.demodulate in + let tsubsumption = fs_time_info.subsumption in debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time)); + debug_print (lazy (Printf.sprintf "\ntall: %.9f" tall)); + debug_print (lazy (Printf.sprintf "\ntdemod: %.9f" tdemodulate)); + debug_print (lazy (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption)); + debug_print (lazy (Printf.sprintf "\ninfer_time: %.9f" !infer_time)); + debug_print (lazy (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time)); + debug_print (lazy (Printf.sprintf "\nforward_simpl_new_times: %.9f" !forward_simpl_new_time)); + debug_print (lazy (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time)); + debug_print (lazy (Printf.sprintf "\npassive_maintainance_time: %.9f" !passive_maintainance_time)); newstatus | _ -> raise (ProofEngineTypes.Fail (lazy "NO proof found")) diff --git a/helm/ocaml/tactics/paramodulation/utils.ml b/helm/ocaml/tactics/paramodulation/utils.ml index defd72b16..b212d0fab 100644 --- a/helm/ocaml/tactics/paramodulation/utils.ml +++ b/helm/ocaml/tactics/paramodulation/utils.ml @@ -25,7 +25,7 @@ (* $Id$ *) -let debug = false;; +let debug = true;; let debug_print s = if debug then prerr_endline (Lazy.force s);; @@ -664,20 +664,22 @@ let rec lpo t1 t2 = (* settable by the user... *) -(* let compare_terms = ref nonrec_kbo;; *) +let compare_terms = ref nonrec_kbo;; (* let compare_terms = ref ao;; *) -let compare_terms = ref rpo;; +(* let compare_terms = ref rpo;; *) let guarded_simpl ?(debug=false) context t = - let t' = ProofEngineReduction.simpl context t in - if t = t' then t else - begin - let simpl_order = !compare_terms t t' in - if debug then - prerr_endline ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t')); - if simpl_order = Gt then (if debug then prerr_endline "GT";t') - else (if debug then prerr_endline "NO_GT";t) - end + if !compare_terms == nonrec_kbo then t + else + let t' = ProofEngineReduction.simpl context t in + if t = t' then t else + begin + let simpl_order = !compare_terms t t' in + if debug then + prerr_endline ("comparing "^(CicPp.ppterm t)^(CicPp.ppterm t')); + if simpl_order = Gt then (if debug then prerr_endline "GT";t') + else (if debug then prerr_endline "NO_GT";t) + end ;; type equality_sign = Negative | Positive;;