X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=e7166324de60d735480374a21595b3c9b1af8318;hb=e4158685ac9f6a89c0e208d7c3c0faed84ae45fc;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..e7166324d 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -61,7 +61,7 @@ type retrieval_mode = Matching | Unification;; let string_of_res ?env = function None -> "None" - | Some (t, s, m, u, ((p,e), eq_URI)) -> + | Some (t, s, m, u, (p,e)) -> Printf.sprintf "Some: (%s, %s, %s)" (Utils.string_of_pos p) (Equality.string_of_equality ?env e) @@ -122,7 +122,7 @@ let check_for_duplicates metas msg = let check_res res msg = match res with - Some (t, subst, menv, ug, (eq_found, eq_URI)) -> + Some (t, subst, menv, ug, eq_found) -> let eqs = Equality.string_of_equality (snd eq_found) in check_disjoint_invariant subst menv msg; check_for_duplicates menv (msg ^ "\nchecking " ^ eqs); @@ -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 ;; @@ -243,22 +252,21 @@ let rec find_matches metasenv context ugraph lift_amount term termty = ~metasenv context termty ty ugraph)) then ( find_matches metasenv context ugraph lift_amount term termty tl ) else - let do_match c eq_URI = + let do_match c = let subst', metasenv', ugraph' = Inference.matching metasenv metas context term (S.lift lift_amount c) ugraph in - Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph', - (candidate, eq_URI)) + Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate) in - let c, other, eq_URI = - if pos = Utils.Left then left, right, Utils.eq_ind_URI () - else right, left, Utils.eq_ind_r_URI () + let c, other = + if pos = Utils.Left then left, right + else right, left in if o <> U.Incomparable then let res = try - do_match c eq_URI + do_match c with Inference.MatchingFailure -> find_matches metasenv context ugraph lift_amount term termty tl in @@ -266,7 +274,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = res else let res = - try do_match c eq_URI + try do_match c with Inference.MatchingFailure -> None in if Utils.debug_res then ignore (check_res res "find2"); @@ -307,19 +315,19 @@ let rec find_all_matches ?(unif_fun=Inference.unification) | candidate::tl -> let pos, equality = candidate in let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in - let do_match c eq_URI = + let do_match c = let subst', metasenv', ugraph' = unif_fun metasenv metas context term (S.lift lift_amount c) ugraph in - (C.Rel (1+lift_amount),subst',metasenv',ugraph',(candidate, eq_URI)) + (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate) in - let c, other, eq_URI = - if pos = Utils.Left then left, right, Utils.eq_ind_URI () - else right, left, Utils.eq_ind_r_URI () + let c, other = + if pos = Utils.Left then left, right + else right, left in if o <> U.Incomparable then try - let res = do_match c eq_URI in + let res = do_match c in res::(find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl) with @@ -330,7 +338,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) lift_amount term termty tl else try - let res = do_match c eq_URI in + let res = do_match c in match res with | _, s, _, _, _ -> let c' = apply_subst s c @@ -386,24 +394,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 -> + | (_, 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 +423,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 = @@ -527,7 +536,7 @@ let rec demodulation_aux ?from ?(typecheck=false) exception Foo (** demodulation, when target is an equality *) -let rec demodulation_equality ?from newmeta env table sign target = +let rec demodulation_equality ?from eq_uri newmeta env table sign target = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -549,7 +558,7 @@ let rec demodulation_equality ?from newmeta env table sign target = let metasenv' = (* metasenv @ *) metas in let maxmeta = ref newmeta in - let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) = + let build_newtarget is_left (t, subst, menv, ug, eq_found) = if Utils.debug_metas then begin @@ -573,8 +582,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, []); - S.lift 1 eq_ty; l; r] + C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r] in if sign = Utils.Positive then (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'), @@ -683,7 +691,7 @@ let rec demodulation_equality ?from newmeta env table sign target = (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality ?from newmeta env table sign newtarget + demodulation_equality ?from eq_uri newmeta env table sign newtarget | None -> let res = demodulation_aux metasenv' context ugraph table 0 right in if Utils.debug_res then check_res res "demod result 1"; @@ -694,7 +702,7 @@ let rec demodulation_equality ?from newmeta env table sign target = (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality ?from newmeta env table sign newtarget + demodulation_equality ?from eq_uri newmeta env table sign newtarget | None -> newmeta, target in @@ -718,6 +726,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) -> @@ -789,8 +798,8 @@ let rec betaexpand_term | C.Appl l -> let l', lifted_l = - List.fold_right - (fun arg (res, lifted_tl) -> + List.fold_left + (fun (res, lifted_tl) arg -> let arg_res, lifted_arg = betaexpand_term metasenv context ugraph table lift_amount arg in @@ -806,7 +815,7 @@ let rec betaexpand_term lifted_arg::r, s, m, ug, eq_found) res), lifted_arg::lifted_tl) - ) l ([], []) + ) ([], []) (List.rev l) in (List.map (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l', @@ -840,8 +849,7 @@ let rec betaexpand_term index: its updated value is also returned *) let superposition_right - ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target -= + ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target= let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -872,7 +880,7 @@ let superposition_right in (res left right), (res right left) in - let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) = + let build_new ordering (bo, s, m, ug, eq_found) = if Utils.debug_metas then ignore (check_target context (snd eq_found) "buildnew1" ); @@ -890,8 +898,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, []); - S.lift 1 eq_ty; l; r] + C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r] in bo', Equality.Step @@ -938,7 +945,7 @@ let rec demodulation_theorem newmeta env table theorem = let term, termty, metas = theorem in let metasenv' = metas in - let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) = + let build_newtheorem (t, subst, menv, ug, eq_found) = let pos, equality = eq_found in let (_, proof', (ty, what, other, _), menv',id) = Equality.open_equality equality in @@ -1015,9 +1022,9 @@ 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 (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in let pos, equality = eq_found in let (_, proof', (ty, what, other, _), menv',id) = Equality.open_equality equality in @@ -1029,7 +1036,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 @@ -1043,15 +1050,28 @@ let build_newgoal context goal posu expansion = *) let superposition_left (metasenv, context, ugraph) table goal = let proof,menv,eq,ty,l,r = open_goal goal in - let c = - 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 + let c = !Utils.compare_terms l r in + if c = Utils.Incomparable then + begin + let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in + let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in + (* prerr_endline "incomparable"; + 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 + end + else + let big,small,possmall = + match c with + Utils.Gt -> (* prerr_endline "GT"; *) l,r,Utils.Right + | Utils.Lt -> (* prerr_endline "LT"; *) r,l,Utils.Left + | _ -> assert false + 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 +1083,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 +1095,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