X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=7ff0dfd2cc6560dd0b7cfefbb8d088122875283c;hb=ba5f2cc720dd8fbb74214cfd99d63fb7330ffce3;hp=34c601b3558ee15ba9d1bbe90038e7d4d2b4879d;hpb=7fa3bd6487683920f34871688b357f08f67ebb3d;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 34c601b35..7ff0dfd2c 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -109,19 +109,73 @@ let check_disjoint_invariant subst metasenv msg = ;; let check_for_duplicates metas msg = - if List.length metas <> - List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then - begin + let rec aux = function + | [] -> true + | (m,_,_)::tl -> not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in + let b = aux metas in + if not b then + begin prerr_endline ("DUPLICATI " ^ msg); prerr_endline (CicMetaSubst.ppmetasenv [] metas); assert false - end + end + else () +;; + +let check_metasenv msg menv = + List.iter + (fun (i,ctx,ty) -> + try ignore(CicTypeChecker.type_of_aux' menv ctx ty + CicUniv.empty_ugraph) + with + | CicUtil.Meta_not_found _ -> + prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv); + assert false + | _ -> () + ) menv +;; + +(* the metasenv returned by res must included in the original one, +due to matching. If it fails, it is probably because we are not +demodulating with a unit equality *) + +let not_unit_eq ctx eq = + let (_,_,(ty,left,right,o),metas,_) = Equality.open_equality eq in + let b = + List.exists + (fun (_,_,ty) -> + try + let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.oblivion_ugraph + in s = Cic.Sort(Cic.Prop) + with _ -> + prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas + in b +(* +if b then prerr_endline ("not a unit equality: " ^ Equality.string_of_equality eq); b *) +;; + +let check_demod_res res metasenv msg = + match res with + | Some (_, _, menv, _, _) -> + let b = + List.for_all + (fun (i,_,_) -> + (List.exists (fun (j,_,_) -> i=j) metasenv)) menv + in + if (not b) then + begin + debug_print (lazy ("extended context " ^ msg)); + debug_print (lazy (CicMetaSubst.ppmetasenv [] menv)); + end; + b + | None -> false ;; let check_res res msg = match res with - Some (t, subst, menv, ug, eq_found) -> + | Some (t, subst, menv, ug, eq_found) -> let eqs = Equality.string_of_equality (snd eq_found) in + check_metasenv msg menv; check_disjoint_invariant subst menv msg; check_for_duplicates menv (msg ^ "\nchecking " ^ eqs); | None -> () @@ -151,11 +205,11 @@ let check_target bag 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 @@ -222,6 +276,11 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = | [] -> None | candidate::tl -> let pos, equality = candidate in + (* if not_unit_eq context equality then + begin + prerr_endline "not a unit"; + prerr_endline (Equality.string_of_equality equality) + end; *) let (_, proof, (ty, left, right, o), metas,_) = Equality.open_equality equality in @@ -232,13 +291,18 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in let t="t = " ^ (CicPp.ppterm term) ^ "\n" in let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in -(* + let ms="metasenv =" ^ (CicMetaSubst.ppmetasenv [] metasenv) ^ "\n" in + let eq_uri = + match LibraryObjects.eq_URI () with + | Some (uri) -> uri + | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in let p="proof = "^ - (CicPp.ppterm(Equality.build_proof_term proof))^"\n" + (CicPp.ppterm(Equality.build_proof_term bag eq_uri [] 0 proof))^"\n" in -*) + check_for_duplicates metas "gia nella metas"; - check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*)) + check_for_duplicates metasenv "gia nel metasenv"; + check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^ms^p) end; if check && not (fst (CicReduction.are_convertible ~metasenv context termty ty ugraph)) then ( @@ -246,9 +310,11 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = ) else let do_match c = let subst', metasenv', ugraph' = - Inference.matching + Founif.matching metasenv metas context term (S.lift lift_amount c) ugraph in + if Utils.debug_metas then + check_metasenv "founif :" metasenv'; Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate) in let c, other = @@ -259,7 +325,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = let res = try do_match c - with Inference.MatchingFailure -> + 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"); @@ -267,9 +333,9 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = 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"); + if Utils.debug_res then ignore (check_res res "find2"); match res with | Some (_, s, _, _, _) -> let c' = apply_subst s c in @@ -292,27 +358,44 @@ 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) +(* XXX termty unused *) +let rec find_all_matches ?(unif_fun=Founif.unification) ?(demod=false) metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in - let cmp = !Utils.compare_terms in + (* prerr_endline ("matching " ^ CicPp.ppterm term); *) + let cmp x y = + let r = !Utils.compare_terms x y in +(* + prerr_endline ( + CicPp.ppterm x ^ " " ^ + Utils.string_of_comparison r ^ " " ^ + CicPp.ppterm y ); +*) + r + in + let check = match termty with C.Implicit None -> false | _ -> true in function | [] -> [] | candidate::tl -> let pos, equality = candidate in - let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in + let (_,_,(ty,left,right,o),metas,_)= Equality.open_equality equality in + if check && not (fst (CicReduction.are_convertible + ~metasenv context termty ty ugraph)) then ( + find_all_matches metasenv context ugraph lift_amount term termty tl + ) else 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) in + let c, other = if pos = Utils.Left then left, right else right, left @@ -323,7 +406,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 @@ -336,14 +419,16 @@ let rec find_all_matches ?(unif_fun=Inference.unification) let c' = apply_subst s c and other' = apply_subst s other in let order = cmp c' other' in - if order <> U.Lt && order <> U.Le then + if (demod && order = U.Gt) || + (not demod && (order <> U.Lt && order <> U.Le)) + then res::(find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl) else find_all_matches ~unif_fun metasenv context ugraph - lift_amount term termty tl + lift_amount term termty tl with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph @@ -351,22 +436,24 @@ let rec find_all_matches ?(unif_fun=Inference.unification) ;; let find_all_matches - ?unif_fun metasenv context ugraph lift_amount term termty l + ?unif_fun ?demod metasenv context ugraph lift_amount term termty l = find_all_matches - ?unif_fun metasenv context ugraph lift_amount term termty l + ?unif_fun ?demod 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));*) ;; (* returns true if target is subsumed by some equality in table *) +(* let print_res l = prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug, ((pos,equation),_)) -> Equality.string_of_equality equation)l)) ;; +*) let subsumption_aux use_unification env table target = let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in @@ -374,9 +461,9 @@ let subsumption_aux use_unification env table target = 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 +488,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,32 +513,104 @@ let unification x y z = subsumption_aux true x y z ;; +(* the target must be disjoint from the equations in the table *) +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 + if Utils.debug_metas then + check_for_duplicates metasenv "subsumption_aux_all"; + 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 [] menv 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 let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in + if Utils.debug_metas then + check_for_duplicates metasenv "in input a demodulation aux"; let candidates = get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term - in + in +(* let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates in *) let res = match term with | C.Meta _ -> None | term -> - let termty, ugraph = - if typecheck then - CicTypeChecker.type_of_aux' metasenv context term ugraph - else - C.Implicit None, ugraph + let res = + try + let termty, ugraph = + if typecheck then + CicTypeChecker.type_of_aux' metasenv context term ugraph + else + C.Implicit None, ugraph + in + find_matches bag metasenv context ugraph + lift_amount term termty candidates + with _ -> + prerr_endline "type checking error"; + prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv); + prerr_endline ("term: " ^ (CicPp.ppterm term)); + assert false; + (* None *) in - let res = - 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 + let res = + (if Utils.debug_res then + ignore(check_res res "demod1"); + if check_demod_res res metasenv "demod" then res else None) in + if res <> None then res else match term with @@ -463,7 +622,7 @@ let rec demodulation_aux bag ?from ?(typecheck=false) (res, tl @ [S.lift 1 t]) else let r = - demodulation_aux bag ~from:"1" metasenv context ugraph table + demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck lift_amount t in match r with @@ -476,6 +635,7 @@ let rec demodulation_aux bag ?from ?(typecheck=false) | Some (_, subst, menv, ug, eq_found) -> Some (C.Appl ll, subst, menv, ug, eq_found) ) +(* | C.Prod (nn, s, t) -> let r1 = demodulation_aux bag ~from:"2" @@ -498,6 +658,7 @@ let rec demodulation_aux bag ?from ?(typecheck=false) subst, menv, ug, eq_found) ) | C.Lambda (nn, s, t) -> + prerr_endline "siam qui"; let r1 = demodulation_aux bag metasenv context ugraph table lift_amount s in ( @@ -518,6 +679,7 @@ let rec demodulation_aux bag ?from ?(typecheck=false) Some (C.Lambda (nn, s', (S.lift 1 t)), subst, menv, ug, eq_found) ) +*) | t -> None in @@ -528,7 +690,7 @@ let rec demodulation_aux bag ?from ?(typecheck=false) exception Foo (** demodulation, when target is an equality *) -let rec demodulation_equality bag ?from eq_uri newmeta env table target = +let rec demodulation_equality bag ?from eq_uri env table target = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -548,9 +710,8 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target = if Utils.debug_metas then ignore(check_target bag context target "demod equalities input"); let metasenv' = (* metasenv @ *) metas in - let maxmeta = ref newmeta in - let build_newtarget is_left (t, subst, menv, ug, eq_found) = + let build_newtarget bag is_left (t, subst, menv, ug, eq_found) = if Utils.debug_metas then begin @@ -562,10 +723,12 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target = let pos, equality = eq_found in let (_, proof', (ty, what, other, _), menv',id') = Equality.open_equality equality in + (* let ty = - try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) - with CicUtil.Meta_not_found _ -> ty - in + try fst (CicTypeChecker.type_of_aux' menv' context what ugraph) + with CicUtil.Meta_not_found _ -> ty + in *) + let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newproof = let bo = @@ -583,45 +746,44 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target = let left, right = if is_left then newterm, right else left, newterm in let ordering = !Utils.compare_terms left right in let stat = (eq_ty, left, right, ordering) in - let res = + let bag, res = let w = Utils.compute_equality_weight stat in - (Equality.mk_equality bag (w, newproof, stat,newmenv)) + Equality.mk_equality bag (w, newproof, stat,newmenv) in if Utils.debug_metas then ignore(check_target bag context res "buildnew_target output"); - !maxmeta, res + bag, res in - let res = - demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left + demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left in if Utils.debug_res then check_res res "demod result"; - let newmeta, newtarget = + let bag, 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 - newmeta, newtarget + let bag, newtarget = build_newtarget bag true t in + (* assert (not (Equality.meta_convertibility_eq target newtarget)); *) + if (Equality.is_weak_identity newtarget) (* || *) + (*Equality.meta_convertibility_eq target newtarget*) then + bag, newtarget else - demodulation_equality bag ?from eq_uri newmeta env table newtarget + demodulation_equality bag ?from eq_uri env table newtarget | None -> 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 -> - let newmeta, newtarget = build_newtarget false t in + let bag, newtarget = build_newtarget bag false t in if (Equality.is_weak_identity newtarget) || (Equality.meta_convertibility_eq target newtarget) then - newmeta, newtarget + bag, newtarget else - demodulation_equality bag ?from eq_uri newmeta env table newtarget + demodulation_equality bag ?from eq_uri env table newtarget | None -> - newmeta, target + bag, target in (* newmeta, newtarget *) - newmeta,newtarget + bag, newtarget ;; (** @@ -741,10 +903,11 @@ let rec betaexpand_term | C.Meta (i, l) -> res, lifted_term | term -> let termty, ugraph = - C.Implicit None, ugraph -(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) + C.Implicit None, ugraph +(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) in let candidates = get_candidates Unification table term in + (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *) let r = if subterms_only then [] @@ -763,7 +926,7 @@ let rec betaexpand_term index: its updated value is also returned *) let superposition_right bag - ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target= + ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target= let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -776,7 +939,6 @@ let superposition_right bag if Utils.debug_metas then ignore (check_target bag context target "superpositionright"); let metasenv' = newmetas in - let maxmeta = ref newmeta in let res1, res2 = match ordering with | U.Gt -> @@ -794,7 +956,7 @@ let superposition_right bag in (res left right), (res right left) in - let build_new ordering (bo, s, m, ug, eq_found) = + let build_new bag ordering (bo, s, m, ug, eq_found) = if Utils.debug_metas then ignore (check_target bag context (snd eq_found) "buildnew1" ); @@ -803,6 +965,7 @@ let superposition_right bag Equality.open_equality equality in let what, other = if pos = Utils.Left then what, other else other, what in + let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in let newgoal, newproof = (* qua *) let bo' = @@ -819,80 +982,88 @@ let superposition_right bag (s,(Equality.SuperpositionRight, id,(pos,id'),(Cic.Lambda(name,ty,bo'')))) in - let newmeta, newequality = + let bag, newequality = let left, 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 bag, eq' = let w = Utils.compute_equality_weight stat in Equality.mk_equality bag (w, newproof, stat, newmenv) in if Utils.debug_metas then ignore (check_target bag context eq' "buildnew3"); - let newm, eq' = Equality.fix_metas bag !maxmeta eq' in + let bag, eq' = Equality.fix_metas bag eq' in if Utils.debug_metas then ignore (check_target bag context eq' "buildnew4"); - newm, eq' + bag, eq' in - maxmeta := newmeta; if Utils.debug_metas then ignore(check_target bag context newequality "buildnew2"); - newequality + bag, newequality + in + let bag, new1 = + List.fold_right + (fun x (bag,acc) -> + let bag, e = build_new bag U.Gt x in + bag, e::acc) res1 (bag,[]) + in + let bag, new2 = + List.fold_right + (fun x (bag,acc) -> + let bag, e = build_new bag U.Lt x in + bag, e::acc) res2 (bag,[]) in - let new1 = List.map (build_new U.Gt) res1 - and new2 = List.map (build_new U.Lt) res2 in let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in - (!maxmeta, - (List.filter ok (new1 @ new2))) + bag, List.filter ok (new1 @ new2) ;; (** demodulation, when the target is a theorem *) -let rec demodulation_theorem bag newmeta env table theorem = +let rec demodulation_theorem bag env table theorem = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in + let eq_uri = + match LibraryObjects.eq_URI() with + | Some u -> u + | None -> assert false in let metasenv, context, ugraph = env in - let maxmeta = ref newmeta in - let term, termty, metas = theorem in - let metasenv' = metas in - + let proof, theo, metas = theorem in 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 - let what, other = if pos = Utils.Left then what, other else other, what in - let newterm, newty = - let bo = Utils.guarded_simpl context (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*) -(* - let newproofold = - Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, - Equality.BasicProof (Equality.empty_subst,term)) - in - (Equality.build_proof_term_old newproofold, bo) -*) - (* TODO, not ported to the new proofs *) - if true then assert false; term, bo - in - !maxmeta, (newterm, newty, menv) - in - let res = - demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty + let peq = + match proof' with + | Equality.Exact p -> p + | _ -> assert false in + let what, other = + if pos = Utils.Left then what, other else other, what in + let newtheo = apply_subst subst (S.subst other t) in + let name = C.Name "x" in + let body = apply_subst subst t in + let pred = C.Lambda(name,ty,body) in + let newproof = + match pos with + | Utils.Left -> + Equality.mk_eq_ind eq_uri ty what pred proof other peq + | Utils.Right -> + Equality.mk_eq_ind eq_uri ty what pred proof other peq + in + newproof,newtheo in + let res = demodulation_aux bag metas context ugraph table 0 theo in match res with | Some t -> - let newmeta, newthm = build_newtheorem t in - let newt, newty, _ = newthm in - if Equality.meta_convertibility termty newty then - newmeta, newthm + let newproof, newtheo = build_newtheorem t in + if Equality.meta_convertibility theo newtheo then + newproof, newtheo else - demodulation_theorem bag newmeta env table newthm + demodulation_theorem bag env table (newproof,newtheo,[]) | None -> - newmeta, theorem + proof,theo ;; (*****************************************************************************) @@ -901,13 +1072,52 @@ let rec demodulation_theorem bag newmeta env table theorem = (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **) (*****************************************************************************) +(* new: demodulation of non_equality terms *) +let build_newg bag context goal rule expansion = + let goalproof,_,_ = goal in + let (t,subst,menv,ug,eq_found) = expansion in + let pos, equality = eq_found in + let (_, proof', (ty, what, other, _), menv',id) = + Equality.open_equality equality in + let what, other = if pos = Utils.Left then what, other else other, what in + let newterm, newgoalproof = + let bo = + Utils.guarded_simpl context + (apply_subst subst (CicSubstitution.subst other t)) + in + let name = Cic.Name "x" in + let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in + let newgoalproofstep = (rule,pos,id,subst,pred) in + bo, (newgoalproofstep::goalproof) + in + let newmetasenv = (* Founif.filter subst *) menv in + (newgoalproof, newmetasenv, newterm) +;; + +let rec demod bag env table goal = + let _,menv,t = goal in + let _, context, ugraph = env in + let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:false)in + match res with + | Some newt -> + let newg = + build_newg bag context goal Equality.Demodulation newt + in + let _,_,newt = newg in + if Equality.meta_convertibility t newt then + false, goal + else + true, snd (demod bag env table newg) + | None -> + false, goal +;; + 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 -;; let ty_of_goal (_,_,ty) = ty ;; @@ -921,6 +1131,7 @@ let goal_metaconvertibility_eq g1 g2 = * C[x] ---> (eq ty unchanged C[x]) * [posu] is the side of the [unchanged] term in the original goal *) + let fix_expansion goal posu (t, subst, menv, ug, eq_f) = let _,_,eq,ty,l,r = open_goal goal in let unchanged = if posu = Utils.Left then l else r in @@ -948,12 +1159,12 @@ let build_newgoal bag 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 newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in + let name = Cic.Name "x" in + let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in + let newgoalproofstep = (rule,pos,id,subst,pred) in bo, (newgoalproofstep::goalproof) in - let newmetasenv = (* Inference.filter subst *) menv in + let newmetasenv = (* Founif.filter subst *) menv in (newgoalproof, newmetasenv, newterm) ;; @@ -962,7 +1173,7 @@ let build_newgoal bag 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 bag (metasenv, context, ugraph) table goal maxmeta = +let superposition_left bag (metasenv, context, ugraph) table goal = 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 @@ -981,7 +1192,7 @@ let superposition_left bag (metasenv, context, ugraph) table goal maxmeta = end else match c with - | Utils.Gt -> (* prerr_endline "GT"; *) + | Utils.Gt -> let big,small,possmall = l,r,Utils.Right in let expansions, _ = betaexpand_term menv context ugraph table 0 big in List.map @@ -1001,9 +1212,10 @@ let superposition_left bag (metasenv, context, ugraph) table goal maxmeta = in (* rinfresco le meta *) List.fold_right - (fun g (max,acc) -> - let max,g = Equality.fix_metas_goal max g in max,g::acc) - newgoals (maxmeta,[]) + (fun g (b,acc) -> + let b,g = Equality.fix_metas_goal b g in + b,g::acc) + newgoals (bag,[]) ;; (** demodulation, when the target is a goal *) @@ -1035,4 +1247,194 @@ let rec demodulation_goal bag env table goal = | None -> do_right () ;; -let get_stats () = "" ;; +(* returns all the 1 step demodulations *) +module C = Cic;; +module S = CicSubstitution;; + +let rec demodulation_all_aux + metasenv context ugraph table lift_amount term += + let candidates = + get_candidates ~env:(metasenv,context,ugraph) Matching table term + in + match term with + | C.Meta _ -> [] + | _ -> + let termty, ugraph = C.Implicit None, ugraph in + let res = + find_all_matches + ~unif_fun:Founif.matching ~demod:true + metasenv context ugraph lift_amount term termty candidates + in + match term with + | C.Appl l -> + let res, _, _, _ = + List.fold_left + (fun (res,b,l,r) t -> + if not b then res,b,l,r + else + let demods_for_t = + demodulation_all_aux + metasenv context ugraph table lift_amount t + in + let b = demods_for_t = [] in + res @ + List.map + (fun (rel, s, m, ug, c) -> + (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c)) + demods_for_t, b, l@[List.hd r], List.tl r) + (res, true, [], List.map (S.lift 1) l) l + in + res + | t -> res +;; + +let demod_all steps bag env table goal = + let _, context, ugraph = env in + let is_visited l (_,_,t) = + List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l + in + let rec aux steps visited nf bag = function + | _ when steps = 0 -> visited, bag, nf + | [] -> visited, bag, nf + | goal :: rest when is_visited visited goal-> aux steps visited nf bag rest + | goal :: rest -> + let visited = goal :: visited in + let _,menv,t = goal in + let res = demodulation_all_aux menv context ugraph table 0 t in + let steps = if res = [] then steps-1 else steps in + let new_goals = + List.map (build_newg bag context goal Equality.Demodulation) res + in + let nf = if new_goals = [] then goal :: nf else nf in + aux steps visited nf bag (new_goals @ rest) + in + aux steps [] [] bag [goal] +;; + +let combine_demodulation_proofs bag env goal (pl,ml,l) (pr,mr,r) = + let proof,m,eq,ty,left,right = open_goal goal in + let pl = + List.map + (fun (rule,pos,id,subst,pred) -> + let pred = + match pred with + | Cic.Lambda (name,src,tgt) -> + Cic.Lambda (name,src, + Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right]) + | _ -> assert false + in + rule,pos,id,subst,pred) + pl + in + let pr = + List.map + (fun (rule,pos,id,subst,pred) -> + let pred = + match pred with + | Cic.Lambda (name,src,tgt) -> + Cic.Lambda (name,src, + Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt]) + | _ -> assert false + in + rule,pos,id,subst,pred) + pr + in + (pr@pl@proof, m, Cic.Appl [eq;ty;l;r]) +;; + +let demodulation_all_goal bag env table goal maxnf = + let proof,menv,eq,ty,left,right = open_goal goal in + let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in + let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in + let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in + let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in + List.fold_left + (fun acc (_,_,l as ld) -> + List.fold_left + (fun acc (_,_,r as rd) -> + combine_demodulation_proofs bag env goal ld rd :: acc) + acc r_demod) + [] l_demod +;; + +let solve_demodulating bag env table initgoal steps = + let proof,menv,eq,ty,left,right = open_goal initgoal in + let uri = + match eq with + | Cic.MutInd (u,_,_) -> u + | _ -> assert false + in + let _, context, ugraph = env in + let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in + let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in + let is_solved left right ml mr = + let m = ml @ (List.filter + (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr) + in + try + let s,_,_ = + Founif.unification [] m context left right CicUniv.empty_ugraph in + Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left)) + with CicUnification.UnificationFailure _ -> + let solutions = + unification_all env table (Equality.mk_tmp_equality + (0,(Cic.Implicit None,left,right,Utils.Incomparable),m)) + in + if solutions = [] then None + else + let s, e, swapped = List.hd solutions in + let _,p,(ty,l,r,_),me,id = Equality.open_equality e in + let bag, p = + if swapped then Equality.symmetric bag ty l id uri me else bag, p + in + Some (bag, m,s, p) + in + let newgoal = + HExtlib.list_findopt + (fun (pr,mr,r) _ -> + try + let pl,ml,l,bag,m,s,p = + match + HExtlib.list_findopt (fun (pl,ml,l) _ -> + match is_solved l r ml mr with + | None -> None + | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p) + ) l_demod + with Some x -> x | _ -> raise Not_found + in + let pl = + List.map + (fun (rule,pos,id,subst,pred) -> + let pred = + match pred with + | Cic.Lambda (name,src,tgt) -> + Cic.Lambda (name,src, + Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right]) + | _ -> assert false + in + rule,pos,id,subst,pred) + pl + in + let pr = + List.map + (fun (rule,pos,id,subst,pred) -> + let pred = + match pred with + | Cic.Lambda (name,src,tgt) -> + Cic.Lambda (name,src, + Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt]) + | _ -> assert false + in + rule,pos,id,subst,pred) + pr + in + Some (bag,pr@pl@proof,m,s,p) + with Not_found -> None) + r_demod + in + newgoal +;; + + +