X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=9c471d3b351c6056144b32da87f5a4004745d63c;hb=c3b4dfecb4ead05a2e008dca9abc24a6c7803ddc;hp=ff5bf23cbbaae16548a4dd6a643fa089856ec96c;hpb=bd4a73c6f758bd39254178dd7b313af321a5cd4b;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index ff5bf23cb..9c471d3b3 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -294,6 +294,7 @@ 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 Founif.matching or Inference.unification *) +(* XXX termty unused *) let rec find_all_matches ?(unif_fun=Founif.unification) metasenv context ugraph lift_amount term termty = let module C = Cic in @@ -363,10 +364,12 @@ let find_all_matches (* 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 @@ -404,7 +407,7 @@ let subsumption_aux use_unification env table target = | 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,6 +429,61 @@ let unification x y z = subsumption_aux true x y z ;; +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);*) @@ -529,6 +587,16 @@ exception Foo (** demodulation, when target is an equality *) let rec demodulation_equality bag ?from eq_uri newmeta env table target = + (* + prerr_endline ("demodulation_eq:\n"); + Index.iter table (fun l -> + let l = Index.PosEqSet.elements l in + let l = + List.map (fun (p,e) -> + Utils.string_of_pos p ^ Equality.string_of_equality e) l in + prerr_endline (String.concat "\n" l) + ); + *) let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -566,6 +634,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target = try fst (CicTypeChecker.type_of_aux' metasenv 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 = @@ -600,7 +669,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target = match res with | Some t -> let newmeta, newtarget = build_newtarget true t in - assert (not (Equality.meta_convertibility_eq target newtarget)); + (* assert (not (Equality.meta_convertibility_eq target newtarget)); *) if (Equality.is_weak_identity newtarget) (* || *) (*Equality.meta_convertibility_eq target newtarget*) then newmeta, newtarget @@ -803,6 +872,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' = @@ -843,56 +913,56 @@ let superposition_right 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_weak_identity (*metasenv', context, ugraph*) e) in + let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in (!maxmeta, (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 ;; (*****************************************************************************) @@ -904,7 +974,7 @@ let rec demodulation_theorem bag 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 ;; @@ -948,8 +1018,9 @@ 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 bo' = apply_subst subst 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 @@ -1035,4 +1106,118 @@ let rec demodulation_goal bag env table goal = | None -> do_right () ;; +type next = L | R +type solved = Yes of Equality.goal | No of Equality.goal list + +(* 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 + metasenv context ugraph lift_amount term termty candidates + in + match term with + | C.Appl l -> + let res, _, _ = + List.fold_left + (fun (res,l,r) t -> + res @ + List.map + (fun (rel, s, m, ug, c) -> + (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c)) + (demodulation_all_aux + metasenv context ugraph table lift_amount t), + l@[List.hd r], List.tl r) + (res, [], List.map (S.lift 1) l) l + in + res + | C.Prod (nn, s, t) + | C.Lambda (nn, s, t) -> + let context = (Some (nn, C.Decl s))::context in + let mk s t = + match term with + | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t) + in + res @ + List.map + (fun (rel, subst, m, ug, c) -> + mk (S.lift 1 s) rel, subst, m, ug, c) + (demodulation_all_aux + metasenv context ugraph table (lift_amount+1) t) + (* we could demodulate also in s, but then t may be badly + * typed... *) + | t -> res +;; + +let solve_demodulating bag env table initgoal steps = + let _, context, ugraph = env in + let solved goal res side = + let newg = build_newgoal bag context goal side Equality.Demodulation res in + match newg with + | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right]) + when LibraryObjects.is_eq_URI uri -> + (try + let _ = + Founif.unification m m context left right CicUniv.empty_ugraph + in + Yes newg + with CicUnification.UnificationFailure _ -> No [newg]) + | _ -> No [newg] + in + let solved goal res_list side = + let newg = List.map (fun x -> solved goal x side) res_list in + try + List.find (function Yes _ -> true | _ -> false) newg + with Not_found -> + No (List.flatten (List.map (function No s -> s | _-> assert false) newg)) + in + let rec first f l = + match l with + | [] -> None + | x::tl -> + match f x with + | None -> first f tl + | Some x as ok -> ok + in + let rec aux steps next goal = + if steps = 0 then None else + let goalproof,menv,_,_,left,right = open_goal goal in + let do_step t = + demodulation_all_aux menv context ugraph table 0 t + in + match next with + | L -> + (match do_step left with + | _::_ as res -> + (match solved goal res Utils.Right with + | No newgoals -> + (match first (aux (steps - 1) L) newgoals with + | Some g as success -> success + | None -> aux steps R goal) + | Yes newgoal -> Some newgoal) + | [] -> aux steps R goal) + | R -> + (match do_step right with + | _::_ as res -> + (match solved goal res Utils.Left with + | No newgoals -> + (match first (aux (steps - 1) L) newgoals with + | Some g as success -> success + | None -> None) + | Yes newgoal -> Some newgoal) + | [] -> None) + in + aux steps L initgoal +;; + let get_stats () = "" ;;