X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;fp=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=e30d4403490cd01fce5fe4050141656bef3a48f4;hb=c3af85c9492385a7a0de0f5aa57df241ee0bd553;hp=ed22ef4721745369614be57fc2b65274bea0027f;hpb=28ac70d3f475442cda4ef30e0e9c0e6d012b2527;p=helm.git diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index ed22ef472..e30d44034 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -90,12 +90,10 @@ let indexing_retrieval_time = ref 0.;; let apply_subst = CicMetaSubst.apply_subst -(* Profiling code -let apply_subst = - let profile = CicUtil.profile "apply_subst" in - (fun s a -> profile.profile (apply_subst s) a) -;; -*) +(* let apply_subst = *) +(* let profile = CicUtil.profile "apply_subst" in *) +(* (fun s a -> profile (apply_subst s) a) *) +(* ;; *) (* @@ -249,6 +247,15 @@ let rec find_matches metasenv context ugraph lift_amount term termty = and other' = (* M. *)apply_subst s other in let order = cmp c' other' in let names = U.names_of_context context in +(* let _ = *) +(* debug_print *) +(* (Printf.sprintf "OK matching: %s and %s, order: %s" *) +(* (CicPp.ppterm c') *) +(* (CicPp.ppterm other') *) +(* (Utils.string_of_comparison order)); *) +(* debug_print *) +(* (Printf.sprintf "subst:\n%s\n" (Utils.print_subst s)) *) +(* in *) if order = U.Gt then res else @@ -373,29 +380,34 @@ let subsumption env table target = find_all_matches ~unif_fun:Inference.matching metasenv context ugraph 0 left ty leftc in - let ok what (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _)) = - try - let other = if pos = Utils.Left then r else l in - let subst', menv', ug' = - let t1 = Unix.gettimeofday () in + let rec ok what = function + | [] -> false, [] + | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _))::tl -> try - let r = - Inference.matching metasenv context what other ugraph in - let t2 = Unix.gettimeofday () in - match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); - r - with Inference.MatchingFailure as e -> - let t2 = Unix.gettimeofday () in - match_unif_time_no := !match_unif_time_no +. (t2 -. t1); - raise e - in - samesubst subst subst' - with Inference.MatchingFailure -> - false + let other = if pos = Utils.Left then r else l in + let subst', menv', ug' = + let t1 = Unix.gettimeofday () in + try + let r = + Inference.matching metasenv context what other ugraph in + let t2 = Unix.gettimeofday () in + match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1); + r + with Inference.MatchingFailure as e -> + let t2 = Unix.gettimeofday () in + match_unif_time_no := !match_unif_time_no +. (t2 -. t1); + raise e + in + if samesubst subst subst' then + true, subst + else + ok what tl + with Inference.MatchingFailure -> + ok what tl in - let r = List.exists (ok right) leftr in + let r, subst = ok right leftr in if r then - true + true, subst else let rightr = match right with @@ -405,11 +417,11 @@ let subsumption env table target = find_all_matches ~unif_fun:Inference.matching metasenv context ugraph 0 right ty rightc in - List.exists (ok left) rightr + ok left rightr ;; -let rec demodulate_term metasenv context ugraph table lift_amount term = +let rec demodulation_aux metasenv context ugraph table lift_amount term = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -437,7 +449,7 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = (res, tl @ [S.lift 1 t]) else let r = - demodulate_term metasenv context ugraph table + demodulation_aux metasenv context ugraph table lift_amount t in match r with @@ -452,11 +464,11 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = ) | C.Prod (nn, s, t) -> let r1 = - demodulate_term metasenv context ugraph table lift_amount s in ( + demodulation_aux metasenv context ugraph table lift_amount s in ( match r1 with | None -> let r2 = - demodulate_term metasenv + demodulation_aux metasenv ((Some (nn, C.Decl s))::context) ugraph table (lift_amount+1) t in ( @@ -472,11 +484,11 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = ) | C.Lambda (nn, s, t) -> let r1 = - demodulate_term metasenv context ugraph table lift_amount s in ( + demodulation_aux metasenv context ugraph table lift_amount s in ( match r1 with | None -> let r2 = - demodulate_term metasenv + demodulation_aux metasenv ((Some (nn, C.Decl s))::context) ugraph table (lift_amount+1) t in ( @@ -510,7 +522,7 @@ let build_newtarget_time = ref 0.;; let demod_counter = ref 1;; -let rec demodulation newmeta env table sign target = +let rec demodulation_equality newmeta env table sign target = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -629,7 +641,7 @@ let rec demodulation newmeta env table sign target = in !maxmeta, res in - let res = demodulate_term metasenv' context ugraph table 0 left in + let res = demodulation_aux metasenv' context ugraph table 0 left in match res with | Some t -> let newmeta, newtarget = build_newtarget true t in @@ -640,9 +652,9 @@ let rec demodulation newmeta env table sign target = (* if subsumption env table newtarget then *) (* newmeta, build_identity newtarget *) (* else *) - demodulation newmeta env table sign newtarget + demodulation_equality newmeta env table sign newtarget | None -> - let res = demodulate_term metasenv' context ugraph table 0 right in + let res = demodulation_aux metasenv' context ugraph table 0 right in match res with | Some t -> let newmeta, newtarget = build_newtarget false t in @@ -653,7 +665,7 @@ let rec demodulation newmeta env table sign target = (* if subsumption env table newtarget then *) (* newmeta, build_identity newtarget *) (* else *) - demodulation newmeta env table sign newtarget + demodulation_equality newmeta env table sign newtarget | None -> newmeta, target ;; @@ -998,8 +1010,13 @@ let rec demodulation_goal newmeta env table goal = let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) = let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in let what, other = if pos = Utils.Left then what, other else other, what in + let ty = + try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) + with CicUtil.Meta_not_found _ -> ty + in let newterm, newproof = let bo = (* M. *)apply_subst subst (S.subst other t) in + let bo' = apply_subst subst t in let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in incr demod_counter; let metaproof = @@ -1025,29 +1042,35 @@ let rec demodulation_goal newmeta env table goal = in let goal_proof = let pb = - Inference.ProofBlock (subst, eq_URI, (name, ty), bo, + Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, Inference.BasicProof metaproof) in - match proof with - | Inference.NoProof -> - debug_print (lazy "replacing a NoProof"); - pb - | Inference.BasicProof _ -> - debug_print (lazy "replacing a BasicProof"); - pb - | Inference.ProofGoalBlock (_, parent_proof) -> - debug_print (lazy "replacing another ProofGoalBlock"); - Inference.ProofGoalBlock (pb, parent_proof) - | _ -> assert false + let rec repl = function + | Inference.NoProof -> + debug_print (lazy "replacing a NoProof"); + pb + | Inference.BasicProof _ -> + debug_print (lazy "replacing a BasicProof"); + pb + | Inference.ProofGoalBlock (_, parent_proof) -> + debug_print (lazy "replacing another ProofGoalBlock"); + Inference.ProofGoalBlock (pb, parent_proof) + | (Inference.SubProof (term, meta_index, p) as subproof) -> + debug_print + (lazy + (Printf.sprintf "replacing %s" + (Inference.string_of_proof subproof))); + Inference.SubProof (term, meta_index, repl p) + | _ -> assert false + in repl proof in bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof) in let m = Inference.metas_of_term newterm in let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in !maxmeta, (newproof, newmetasenv, newterm) - in - - let res = demodulate_term metasenv' context ugraph table 0 term in + in + let res = demodulation_aux metasenv' context ugraph table 0 term in match res with | Some t -> let newmeta, newgoal = build_newgoal t in @@ -1059,3 +1082,46 @@ let rec demodulation_goal newmeta env table goal = | None -> newmeta, goal ;; + + +let rec demodulation_theorem newmeta env table theorem = + let module C = Cic in + let module S = CicSubstitution in + let module M = CicMetaSubst in + let module HL = HelmLibraryObjects in + let metasenv, context, ugraph = env in + let maxmeta = ref newmeta in + let proof, metas, term = theorem in + let term, termty, metas = theorem in + let metasenv' = metasenv @ metas in + + let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) = + let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in + let what, other = if pos = Utils.Left then what, other else other, what in + let newterm, newty = + let bo = apply_subst subst (S.subst other t) in + let bo' = apply_subst subst t in + let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in + incr demod_counter; + let newproof = + Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, + Inference.BasicProof term) + in + (Inference.build_proof_term newproof, bo) + in + let m = Inference.metas_of_term newterm in + let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in + !maxmeta, (newterm, newty, newmetasenv) + in + let res = demodulation_aux metasenv' context ugraph table 0 termty in + match res with + | Some t -> + let newmeta, newthm = build_newtheorem t in + let newt, newty, _ = newthm in + if Inference.meta_convertibility termty newty then + newmeta, newthm + else + demodulation_theorem newmeta env table newthm + | None -> + newmeta, theorem +;;