X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=b535119ed2df5702e9c8a3f2f0a99ce4d0bd7b80;hb=b4da5c84ca7fa4c028ef70875aa79cc7bc279ee9;hp=f3af1b482e8afb2eece8d1ce79d3e10af7812ec7;hpb=bc76b4d2f3c380894259b45fad52cf85ae6cee18;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index f3af1b482..b535119ed 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -127,14 +127,14 @@ let check_res res msg = | None -> () ;; -let check_target context target msg = +let check_target bag context target msg = let w, proof, (eq_ty, left, right, order), metas,_ = Equality.open_equality target in (* check that metas does not contains duplicates *) let eqs = Equality.string_of_equality target in let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right) - @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in + @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof) in let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in let _ = if menv <> metas then begin @@ -151,11 +151,11 @@ let check_target context target msg = (* try ignore(CicTypeChecker.type_of_aux' - metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph) + metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph) with e -> prerr_endline msg; - prerr_endline (Inference.string_of_proof proof); - prerr_endline (CicPp.ppterm (Inference.build_proof_term proof)); + prerr_endline (Founif.string_of_proof proof); + prerr_endline (CicPp.ppterm (Founif.build_proof_term proof)); prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left)); prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right)); raise e @@ -210,7 +210,7 @@ let get_candidates ?env mode tree term = the build_newtarget functions] )) *) -let rec find_matches metasenv context ugraph lift_amount term termty = +let rec find_matches bag metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in let module S = CicSubstitution in @@ -226,7 +226,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = Equality.open_equality equality in if Utils.debug_metas then - ignore(check_target context (snd candidate) "find_matches"); + ignore(check_target bag context (snd candidate) "find_matches"); if Utils.debug_res then begin let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in @@ -242,11 +242,11 @@ let rec find_matches metasenv context ugraph lift_amount term termty = end; if check && not (fst (CicReduction.are_convertible ~metasenv context termty ty ugraph)) then ( - find_matches metasenv context ugraph lift_amount term termty tl + find_matches bag metasenv context ugraph lift_amount term termty tl ) else let do_match c = let subst', metasenv', ugraph' = - Inference.matching + Founif.matching metasenv metas context term (S.lift lift_amount c) ugraph in Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate) @@ -259,15 +259,15 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let res = try do_match c - with Inference.MatchingFailure -> - find_matches metasenv context ugraph lift_amount term termty tl + with Founif.MatchingFailure -> + find_matches bag metasenv context ugraph lift_amount term termty tl in if Utils.debug_res then ignore (check_res res "find1"); res else let res = try do_match c - with Inference.MatchingFailure -> None + with Founif.MatchingFailure -> None in if Utils.debug_res then ignore (check_res res "find2"); match res with @@ -280,10 +280,10 @@ let rec find_matches metasenv context ugraph lift_amount term termty = if order = U.Gt then res else - find_matches + find_matches bag metasenv context ugraph lift_amount term termty tl | None -> - find_matches metasenv context ugraph lift_amount term termty tl + find_matches bag metasenv context ugraph lift_amount term termty tl ;; let find_matches metasenv context ugraph lift_amount term termty = @@ -292,9 +292,9 @@ let find_matches metasenv context ugraph lift_amount term termty = (* as above, but finds all the matching equalities, and the matching condition - can be either Inference.matching or Inference.unification + can be either Founif.matching or Inference.unification *) -let rec find_all_matches ?(unif_fun=Inference.unification) +let rec find_all_matches ?(unif_fun=Founif.unification) metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in @@ -323,7 +323,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) res::(find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl) with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph @@ -343,7 +343,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph @@ -356,7 +356,7 @@ let find_all_matches find_all_matches ?unif_fun metasenv context ugraph lift_amount term termty l (*prerr_endline "CANDIDATES:"; - List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l; + List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l; prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int (List.length rc));*) ;; @@ -370,13 +370,13 @@ let print_res l = let subsumption_aux use_unification env table target = let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in - let metasenv, context, ugraph = env in + let _, context, ugraph = env in let metasenv = tmetas in let predicate, unif_fun = if use_unification then - Unification, Inference.unification + Unification, Founif.unification else - Matching, Inference.matching + Matching, Founif.matching in let leftr = match left with @@ -401,10 +401,10 @@ let subsumption_aux use_unification env table target = | None -> ok what leftorright tl | Some s -> Some (s, equation, leftorright <> pos )) with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ -> ok what leftorright tl in - match ok right Utils.Left leftr with + match ok right Utils.Left leftr with | Some _ as res -> res | None -> let rightr = @@ -426,7 +426,62 @@ let unification x y z = subsumption_aux true x y z ;; -let rec demodulation_aux ?from ?(typecheck=false) +let subsumption_aux_all use_unification env table target = + let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in + let _, context, ugraph = env in + let metasenv = tmetas in + let predicate, unif_fun = + if use_unification then + Unification, Founif.unification + else + Matching, Founif.matching + in + let leftr = + match left with + | Cic.Meta _ when not use_unification -> [] + | _ -> + let leftc = get_candidates predicate table left in + find_all_matches ~unif_fun + metasenv context ugraph 0 left ty leftc + in + let rightr = + match right with + | Cic.Meta _ when not use_unification -> [] + | _ -> + let rightc = get_candidates predicate table right in + find_all_matches ~unif_fun + metasenv context ugraph 0 right ty rightc + in + let rec ok_all what leftorright = function + | [] -> [] + | (_, 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 + in + (match Subst.merge_subst_if_possible subst subst' with + | None -> ok_all what leftorright tl + | Some s -> + (s, equation, leftorright <> pos )::(ok_all what leftorright tl)) + with + | Founif.MatchingFailure + | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl) + in + (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr ) +;; + +let subsumption_all x y z = + subsumption_aux_all false x y z +;; + +let unification_all x y z = + subsumption_aux_all true x y z +;; +let rec demodulation_aux bag ?from ?(typecheck=false) metasenv context ugraph table lift_amount term = (* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*) let module C = Cic in @@ -448,7 +503,7 @@ let rec demodulation_aux ?from ?(typecheck=false) C.Implicit None, ugraph in let res = - find_matches metasenv context ugraph lift_amount term termty candidates + find_matches bag metasenv context ugraph lift_amount term termty candidates in if Utils.debug_res then ignore(check_res res "demod1"); if res <> None then @@ -463,7 +518,7 @@ let rec demodulation_aux ?from ?(typecheck=false) (res, tl @ [S.lift 1 t]) else let r = - demodulation_aux ~from:"1" metasenv context ugraph table + demodulation_aux bag ~from:"1" metasenv context ugraph table lift_amount t in match r with @@ -478,12 +533,12 @@ let rec demodulation_aux ?from ?(typecheck=false) ) | C.Prod (nn, s, t) -> let r1 = - demodulation_aux ~from:"2" + demodulation_aux bag ~from:"2" metasenv context ugraph table lift_amount s in ( match r1 with | None -> let r2 = - demodulation_aux metasenv + demodulation_aux bag metasenv ((Some (nn, C.Decl s))::context) ugraph table (lift_amount+1) t in ( @@ -499,12 +554,12 @@ let rec demodulation_aux ?from ?(typecheck=false) ) | C.Lambda (nn, s, t) -> let r1 = - demodulation_aux + demodulation_aux bag metasenv context ugraph table lift_amount s in ( match r1 with | None -> let r2 = - demodulation_aux metasenv + demodulation_aux bag metasenv ((Some (nn, C.Decl s))::context) ugraph table (lift_amount+1) t in ( @@ -528,7 +583,7 @@ let rec demodulation_aux ?from ?(typecheck=false) exception Foo (** demodulation, when target is an equality *) -let rec demodulation_equality ?from eq_uri newmeta env table target = +let rec demodulation_equality bag ?from eq_uri newmeta env table target = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -546,7 +601,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table target = (* let w = Utils.compute_equality_weight stat in*) (* let target = Equality.mk_equality (w, proof, stat, metas) in *) if Utils.debug_metas then - ignore(check_target context target "demod equalities input"); + ignore(check_target bag context target "demod equalities input"); let metasenv' = (* metasenv @ *) metas in let maxmeta = ref newmeta in @@ -557,7 +612,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table target = ignore(check_for_duplicates menv "input1"); ignore(check_disjoint_invariant subst menv "input2"); let substs = Subst.ppsubst subst in - ignore(check_target context (snd eq_found) ("input3" ^ substs)) + ignore(check_target bag context (snd eq_found) ("input3" ^ substs)) end; let pos, equality = eq_found in let (_, proof', @@ -585,27 +640,29 @@ let rec demodulation_equality ?from eq_uri newmeta env table target = let stat = (eq_ty, left, right, ordering) in let res = let w = Utils.compute_equality_weight stat in - (Equality.mk_equality (w, newproof, stat,newmenv)) + (Equality.mk_equality bag (w, newproof, stat,newmenv)) in if Utils.debug_metas then - ignore(check_target context res "buildnew_target output"); + ignore(check_target bag context res "buildnew_target output"); !maxmeta, res in - let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in + let res = + demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left + in if Utils.debug_res then check_res res "demod result"; let newmeta, newtarget = match res with | Some t -> let newmeta, newtarget = build_newtarget true t in - assert (not (Equality.meta_convertibility_eq target newtarget)); - if (Equality.is_weak_identity newtarget) || - (Equality.meta_convertibility_eq target newtarget) then + (* assert (not (Equality.meta_convertibility_eq target newtarget)); *) + if (Equality.is_weak_identity newtarget) (* || *) + (*Equality.meta_convertibility_eq target newtarget*) then newmeta, newtarget else - demodulation_equality ?from eq_uri newmeta env table newtarget + demodulation_equality bag ?from eq_uri newmeta env table newtarget | None -> - let res = demodulation_aux metasenv' context ugraph table 0 right in + let res = demodulation_aux bag metasenv' context ugraph table 0 right in if Utils.debug_res then check_res res "demod result 1"; match res with | Some t -> @@ -614,7 +671,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table target = (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality ?from eq_uri newmeta env table newtarget + demodulation_equality bag ?from eq_uri newmeta env table newtarget | None -> newmeta, target in @@ -760,7 +817,7 @@ let rec betaexpand_term the first free meta index, i.e. the first number above the highest meta index: its updated value is also returned *) -let superposition_right +let superposition_right bag ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target= let module C = Cic in let module S = CicSubstitution in @@ -772,7 +829,7 @@ let superposition_right Equality.open_equality target in if Utils.debug_metas then - ignore (check_target context target "superpositionright"); + ignore (check_target bag context target "superpositionright"); let metasenv' = newmetas in let maxmeta = ref newmeta in let res1, res2 = @@ -794,7 +851,7 @@ let superposition_right in let build_new ordering (bo, s, m, ug, eq_found) = if Utils.debug_metas then - ignore (check_target context (snd eq_found) "buildnew1" ); + ignore (check_target bag context (snd eq_found) "buildnew1" ); let pos, equality = eq_found in let (_, proof', (ty, what, other, _), menv',id') = @@ -822,21 +879,21 @@ let superposition_right if ordering = U.Gt then newgoal, apply_subst s right else apply_subst s left, newgoal in let neworder = !Utils.compare_terms left right in - let newmenv = (* Inference.filter s *) m in + let newmenv = (* Founif.filter s *) m in let stat = (eq_ty, left, right, neworder) in let eq' = let w = Utils.compute_equality_weight stat in - Equality.mk_equality (w, newproof, stat, newmenv) in + Equality.mk_equality bag (w, newproof, stat, newmenv) in if Utils.debug_metas then - ignore (check_target context eq' "buildnew3"); - let newm, eq' = Equality.fix_metas !maxmeta eq' in + ignore (check_target bag context eq' "buildnew3"); + let newm, eq' = Equality.fix_metas bag !maxmeta eq' in if Utils.debug_metas then - ignore (check_target context eq' "buildnew4"); + ignore (check_target bag context eq' "buildnew4"); newm, eq' in maxmeta := newmeta; if Utils.debug_metas then - ignore(check_target context newequality "buildnew2"); + ignore(check_target bag context newequality "buildnew2"); newequality in let new1 = List.map (build_new U.Gt) res1 @@ -847,7 +904,7 @@ let superposition_right ;; (** demodulation, when the target is a theorem *) -let rec demodulation_theorem newmeta env table theorem = +let rec demodulation_theorem bag newmeta env table theorem = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -879,7 +936,7 @@ let rec demodulation_theorem newmeta env table theorem = !maxmeta, (newterm, newty, menv) in let res = - demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty + demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty in match res with | Some t -> @@ -888,7 +945,7 @@ let rec demodulation_theorem newmeta env table theorem = if Equality.meta_convertibility termty newty then newmeta, newthm else - demodulation_theorem newmeta env table newthm + demodulation_theorem bag newmeta env table newthm | None -> newmeta, theorem ;; @@ -902,7 +959,7 @@ let rec demodulation_theorem newmeta env table theorem = let open_goal g = match g with | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) -> - assert (LibraryObjects.is_eq_URI uri); + (* assert (LibraryObjects.is_eq_URI uri); *) proof,menv,eq,ty,l,r | _ -> assert false ;; @@ -934,7 +991,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 rule expansion = +let build_newgoal bag context goal posu rule expansion = let goalproof,_,_,_,_,_ = open_goal goal in let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in let pos, equality = eq_found in @@ -946,12 +1003,15 @@ let build_newgoal context goal posu rule expansion = Utils.guarded_simpl context (apply_subst subst (CicSubstitution.subst other t)) in - let bo' = (*apply_subst subst*) t in - let name = Cic.Name "x" in + let bo' = (*apply_subst subst*) t in + (* patch?? + let bo' = t in + let ty = apply_subst subst ty in *) + let name = Cic.Name "x" in let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in bo, (newgoalproofstep::goalproof) in - let newmetasenv = (* Inference.filter subst *) menv in + let newmetasenv = (* Founif.filter subst *) menv in (newgoalproof, newmetasenv, newterm) ;; @@ -960,7 +1020,7 @@ let build_newgoal context goal posu rule expansion = returns a list of new clauses inferred with a left superposition step the negative equation "target" and one of the positive equations in "table" *) -let superposition_left (metasenv, context, ugraph) table goal maxmeta = +let superposition_left bag (metasenv, context, ugraph) table goal maxmeta = let names = Utils.names_of_context context in let proof,menv,eq,ty,l,r = open_goal goal in let c = !Utils.compare_terms l r in @@ -973,9 +1033,9 @@ let superposition_left (metasenv, context, ugraph) table goal maxmeta = 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 bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl @ - List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr + List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr end else match c with @@ -983,13 +1043,13 @@ let superposition_left (metasenv, context, ugraph) table goal maxmeta = let big,small,possmall = l,r,Utils.Right in let expansions, _ = betaexpand_term menv context ugraph table 0 big in List.map - (build_newgoal context goal possmall Equality.SuperpositionLeft) + (build_newgoal bag context goal possmall Equality.SuperpositionLeft) expansions | Utils.Lt -> (* prerr_endline "LT"; *) let big,small,possmall = 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) + (build_newgoal bag context goal possmall Equality.SuperpositionLeft) expansions | Utils.Eq -> [] | _ -> @@ -1005,31 +1065,31 @@ let superposition_left (metasenv, context, ugraph) table goal maxmeta = ;; (** demodulation, when the target is a goal *) -let rec demodulation_goal env table goal = +let rec demodulation_goal bag env table goal = let goalproof,menv,_,_,left,right = open_goal goal in let _, context, ugraph = env in (* let term = Utils.guarded_simpl (~debug:true) context term in*) let do_right () = - let resright = demodulation_aux menv context ugraph table 0 right in + let resright = demodulation_aux bag menv context ugraph table 0 right in match resright with | Some t -> let newg = - build_newgoal context goal Utils.Left Equality.Demodulation t + build_newgoal bag context goal Utils.Left Equality.Demodulation t in if goal_metaconvertibility_eq goal newg then false, goal else - true, snd (demodulation_goal env table newg) + true, snd (demodulation_goal bag env table newg) | None -> false, goal in - let resleft = demodulation_aux menv context ugraph table 0 left in + let resleft = demodulation_aux bag menv context ugraph table 0 left in match resleft with | Some t -> - let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in + let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in if goal_metaconvertibility_eq goal newg then do_right () else - true, snd (demodulation_goal env table newg) + true, snd (demodulation_goal bag env table newg) | None -> do_right () ;;