X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=925aab6e05d3663ba3d01eabca3cf11e43b16ac8;hb=e8f64678cc425f19336ff4f905f9b2f00acd6627;hp=dd2d0a422e1fee06df487e362a3966e9b4f57c19;hpb=1d973a067d441fbae43905abb704e21faa223e2b;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index dd2d0a422..925aab6e0 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -181,8 +181,17 @@ let check_target context target msg = let get_candidates ?env mode tree term = let s = match mode with - | Matching -> Index.retrieve_generalizations tree term - | Unification -> Index.retrieve_unifiables tree term + | Matching -> + let _ = <:start> in + <:stop> + | Unification -> + let _ = <:start> in + <:stop> + in Index.PosEqSet.elements s ;; @@ -386,24 +395,25 @@ let subsumption_aux use_unification env table target = find_all_matches ~unif_fun metasenv context ugraph 0 left ty leftc in - let rec ok what = function + let rec ok what leftorright = function | [] -> None | (_, subst, menv, ug, ((pos,equation),_))::tl -> let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in try let other = if pos = Utils.Left then r else l in let what' = Subst.apply_subst subst what in + let other' = Subst.apply_subst subst other in let subst', menv', ug' = - unif_fun metasenv m context what' other ugraph + unif_fun metasenv m context what' other' ugraph in (match Subst.merge_subst_if_possible subst subst' with - | None -> ok what tl - | Some s -> Some (s, equation)) + | None -> ok what leftorright tl + | Some s -> Some (s, equation, leftorright <> pos )) with | Inference.MatchingFailure - | CicUnification.UnificationFailure _ -> ok what tl + | CicUnification.UnificationFailure _ -> ok what leftorright tl in - match ok right leftr with + match ok right Utils.Left leftr with | Some _ as res -> res | None -> let rightr = @@ -414,7 +424,7 @@ let subsumption_aux use_unification env table target = find_all_matches ~unif_fun metasenv context ugraph 0 right ty rightc in - ok left rightr + ok left Utils.Right rightr ;; let subsumption x y z = @@ -573,7 +583,7 @@ let rec demodulation_equality ?from newmeta env table sign target = let name = C.Name "x" in let bo' = let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in - C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); + C.Appl [C.MutInd (Utils.eq_URI (), 0, []); S.lift 1 eq_ty; l; r] in if sign = Utils.Positive then @@ -718,6 +728,7 @@ let rec betaexpand_term let res, lifted_term = match term with | C.Meta (i, l) -> + let l = [] in let l', lifted_l = List.fold_right (fun arg (res, lifted_tl) -> @@ -890,7 +901,7 @@ let superposition_right let bo'' = let l, r = if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in - C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); + C.Appl [C.MutInd (Utils.eq_URI (), 0, []); S.lift 1 eq_ty; l; r] in bo', @@ -1015,7 +1026,7 @@ let fix_expansion goal posu (t, subst, menv, ug, eq_f) = (* ginve the old [goal], the side that has not changed [posu] and the * expansion builds a new goal *) -let build_newgoal context goal posu expansion = +let build_newgoal context goal posu rule expansion = let goalproof,_,_,_,_,_ = open_goal goal in let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in let pos, equality = eq_found in @@ -1029,7 +1040,7 @@ let build_newgoal context goal posu expansion = in let bo' = (*apply_subst subst*) t in let name = Cic.Name "x" in - let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in + let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in bo, (newgoalproofstep::goalproof) in let newmetasenv = (* Inference.filter subst *) menv in @@ -1047,11 +1058,23 @@ let superposition_left (metasenv, context, ugraph) table goal = Utils.compare_weights ~normalize:true (Utils.weight_of_term l) (Utils.weight_of_term r) in - let big,small,possmall = - match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left - in - let expansions, _ = betaexpand_term menv context ugraph table 0 big in - List.map (build_newgoal context goal possmall) expansions + + if c = Utils.Incomparable then + let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in + let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in + prerr_endline "ZZZ"; + prerr_endline (string_of_int (List.length expansionsl)); + prerr_endline (string_of_int (List.length expansionsr)); + List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl + @ + List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr + + else + let big,small,possmall = + match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left + in + let expansions, _ = betaexpand_term menv context ugraph table 0 big in + List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions ;; (** demodulation, when the target is a goal *) @@ -1063,7 +1086,9 @@ let rec demodulation_goal env table goal = let resright = demodulation_aux menv context ugraph table 0 right in match resright with | Some t -> - let newg = build_newgoal context goal Utils.Left t in + let newg = + build_newgoal context goal Utils.Left Equality.Demodulation t + in if goal_metaconvertibility_eq goal newg then false, goal else @@ -1073,7 +1098,7 @@ let rec demodulation_goal env table goal = let resleft = demodulation_aux menv context ugraph table 0 left in match resleft with | Some t -> - let newg = build_newgoal context goal Utils.Right t in + let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in if goal_metaconvertibility_eq goal newg then do_right () else