From: Enrico Tassi Date: Sat, 20 May 2006 10:05:27 +0000 (+0000) Subject: fixed demodulation of goal X-Git-Tag: make_still_working~7350 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=15469f16ff6f86c6cc0107070775b6c03c0ec478;p=helm.git fixed demodulation of goal --- diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 2c560cb55..d69404ed4 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -156,7 +156,7 @@ let check_target context target msg = (* try ignore(CicTypeChecker.type_of_aux' - metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph) + metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph) with e -> prerr_endline msg; prerr_endline (Inference.string_of_proof proof); @@ -242,8 +242,10 @@ let rec find_matches metasenv context ugraph lift_amount term termty = | [] -> None | candidate::tl -> let pos, equality = candidate in - let (_, proof, (ty, left, right, o), metas,_) = - Equality.open_equality equality in + prerr_endline (". " ^ Equality.string_of_equality equality); + let (_, proof, (ty, left, right, o), metas,_) = + Equality.open_equality equality + in if Utils.debug_metas then ignore(check_target context (snd candidate) "find_matches"); if Utils.debug_res then @@ -279,7 +281,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = raise e | CicUtil.Meta_not_found _ as exn -> raise exn in - Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph', + Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph', (candidate, eq_URI)) in let c, other, eq_URI = @@ -333,11 +335,23 @@ 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 (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in let do_match c eq_URI = let subst', metasenv', ugraph' = let t1 = Unix.gettimeofday () in try + let term = + match c,term with + | Cic.Meta _, Cic.Appl[Cic.MutInd(u,0,_);_;l;r] + when LibraryObjects.is_eq_URI u -> l +(* + if Utils.compare_weights (Utils.weight_of_term l) + (Utils.weight_of_term r) = Utils.Gt + then l else r +*) + | _ -> term + in + let r = unif_fun metasenv metas context term (S.lift lift_amount c) ugraph in @@ -473,20 +487,15 @@ let unification = subsumption_aux true;; let rec demodulation_aux ?from ?(typecheck=false) metasenv context ugraph table lift_amount term = - (* Printf.eprintf "term = %s\n" (CicPp.ppterm 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 let candidates = - get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term in - if List.exists (fun (i,_,_) -> i = 2840) metasenv - then - (prerr_endline ("term: " ^(CicPp.ppterm term)); - List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality x)) - candidates; - prerr_endline ("-------"); - prerr_endline ("+++++++")); + get_candidates + ~env:(metasenv,context,ugraph) (* Unification *) Matching table term + in let res = match term with | C.Meta _ -> None @@ -643,7 +652,7 @@ let rec demodulation_equality ?from newmeta env table sign target = else assert false (* - begin + begin prerr_endline "***************************************negative"; let metaproof = incr maxmeta; @@ -673,7 +682,7 @@ let rec demodulation_equality ?from newmeta env table sign target = let target_proof = let pb = Equality.ProofBlock - (subst, eq_URI, (name, ty), bo', + (subst, eq_URI, (name, ty), bo', eq_found, Equality.BasicProof (Equality.empty_subst,metaproof)) in assert false, (* not implemented *) @@ -742,7 +751,7 @@ let rec demodulation_equality ?from newmeta env table sign 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 @@ -905,8 +914,19 @@ let sup_l_counter = ref 1;; 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 fix_expansion (eq,ty,unchanged,posu) (t, subst, menv, ug, eq_f) = + let unchanged = CicSubstitution.lift 1 unchanged in + let ty = CicSubstitution.lift 1 ty in + let pred = + match posu with + | Utils.Left -> Cic.Appl [eq;ty;unchanged;t] + | Utils.Right -> Cic.Appl [eq;ty;t;unchanged] + in + (pred, subst, menv, ug, eq_f) +;; -let build_newgoal context goalproof (t, subst, menv, ug, (eq_found, eq_URI)) = +let build_newgoal context goalproof goal_info expansion = + let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal_info expansion in let pos, equality = eq_found in let (_, proof', (ty, what, other, _), menv',id) = Equality.open_equality equality in @@ -944,23 +964,13 @@ let superposition_left (match c with | Utils.Gt -> l,r,Utils.Right,eq,ty | _ -> r,l,Utils.Left,eq,ty) - | _ -> assert false + | _ -> + let names = Utils.names_of_context context in + prerr_endline ("NON TROVO UN EQ: " ^ CicPp.pp ty names); + assert false in - let small = CicSubstitution.lift 1 small in - let ty = CicSubstitution.lift 1 ty in let expansions, _ = betaexpand_term menv context ugraph table 0 big in - let fix_preds (t, subst, menv, ug, (eq_found, eq_URI)) = - let pred = - match pos with - | Utils.Left -> - Cic.Appl [eq;ty;small;t] - | Utils.Right -> - Cic.Appl [eq;ty;t;small] - in - (pred, subst, menv, ug, (eq_found, eq_URI)) - in - List.map (build_newgoal context proof) - (List.map fix_preds expansions) + List.map (build_newgoal context proof (eq,ty,small,pos)) expansions ;; let sup_r_counter = ref 1;; @@ -995,8 +1005,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = res in match ordering with - | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), [] - | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right) + | U.Gt -> + fst (betaexpand_term metasenv' context ugraph table 0 left), [] + | U.Lt -> + [], fst (betaexpand_term metasenv' context ugraph table 0 right) | _ -> let res l r = List.filter @@ -1017,6 +1029,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = 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 newgoal, newproof = (* qua *) let bo' = @@ -1066,60 +1079,45 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = (List.filter ok (new1 @ new2))) ;; - (** demodulation, when the target is a goal *) -let rec demodulation_goal newmeta env table goal = - let module C = Cic in - let module S = CicSubstitution in - let module M = CicMetaSubst in - let module HL = HelmLibraryObjects in +let goal_metaconvertibility_eq (_,_,g1) (_,_,g2) = + Equality.meta_convertibility g1 g2 +;; + +let rec demodulation_goal env table goal = let metasenv, context, ugraph = env in - let maxmeta = ref newmeta in let goalproof, metas, term = goal in let term = Utils.guarded_simpl (~debug:true) context term in let goal = goalproof, metas, term in let metasenv' = metas in - - let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) = - 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 ty = - try fst (CicTypeChecker.type_of_aux' menv' context what ugraph) - with - | CicUtil.Meta_not_found _ - | Invalid_argument("List.fold_left2") -> ty - in - let newterm, newgoalproof = - 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" in - incr demod_counter; - let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in - bo, (newgoalproofstep::goalproof) - in - let newmetasenv = (* Inference.filter subst *) menv in - !maxmeta, (newgoalproof, newmetasenv, newterm) - in - let res = - demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term + + let left,right,eq,ty = + match term with + | Cic.Appl [eq;ty;l;r] -> l,r,eq,ty + | _ -> assert false in - match res with + let do_right () = + let resright = demodulation_aux metasenv' context ugraph table 0 right in + match resright with + | Some t -> + let newg=build_newgoal context goalproof (eq,ty,left,Utils.Left) t in + if goal_metaconvertibility_eq goal newg then + false, goal + else + true, snd (demodulation_goal env table newg) + | None -> false, goal + in + let resleft = + demodulation_aux (*~typecheck:true*) metasenv' context ugraph table 0 left + in + match resleft with | Some t -> - let newmeta, newgoal = build_newgoal t in - let _, _, newg = newgoal in - if Equality.meta_convertibility term newg then - false, newmeta, newgoal + let newg = build_newgoal context goalproof (eq,ty,right,Utils.Right) t in + if goal_metaconvertibility_eq goal newg then + do_right () else - let changed, newmeta, newgoal = - demodulation_goal newmeta env table newgoal - in - true, newmeta, newgoal - | None -> - false, newmeta, goal + true, snd (demodulation_goal env table newg) + | None -> do_right () ;; (** demodulation, when the target is a theorem *) diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli index f3f23e6f1..27ac1680a 100644 --- a/helm/software/components/tactics/paramodulation/indexing.mli +++ b/helm/software/components/tactics/paramodulation/indexing.mli @@ -75,11 +75,10 @@ val demodulation_equality : Index.t -> Utils.equality_sign -> Equality.equality -> int * Equality.equality val demodulation_goal : - int -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> goal -> - bool * int * goal + bool * goal val demodulation_theorem : 'a -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index cfada5085..6ab9f59e2 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -628,12 +628,7 @@ let rec simplify_goal env goal ?passive (active_list, active_table) = | None -> None | Some ((_, _), pt) -> Some pt in - let demodulate table goal = - let changed, newmeta, newgoal = - Indexing.demodulation_goal !maxmeta env table goal in - maxmeta := newmeta; - changed, newgoal - in + let demodulate table goal = Indexing.demodulation_goal env table goal in let changed, goal = match passive_table with | None -> demodulate active_table goal @@ -1274,8 +1269,8 @@ let simplify_goal_set env goals passive active = in let simplified = List.fold_left - (fun acc g -> - match simplify_goal env g ~passive active with + (fun acc goal -> + match simplify_goal env goal ~passive active with | _, g -> if find g acc then acc else g::acc) [] active_goals in @@ -1314,6 +1309,9 @@ let infer_goal_set env active goals = let selected = hd in let passive_goals = tl in let new' = Indexing.superposition_left env (snd active) selected in + let metasenv, context, ugraph = env in + let names = names_of_context context in + List.iter (fun (_,_,x) -> prerr_endline ("X: " ^ CicPp.pp x names)) new'; selected::active_goals, passive_goals @ new' | _::tl -> aux tl in @@ -2011,7 +2009,7 @@ let main_demod_equalities dbd term metasenv ugraph = *) ;; -let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = +let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = let module I = Inference in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in @@ -2029,11 +2027,11 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = (fun tbl eq -> Indexing.index tbl eq) Indexing.empty equalities in - let _, newmeta,(newproof,newmetasenv, newty) = + let changed,(newproof,newmetasenv, newty) = Indexing.demodulation_goal - maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal + (metasenv,context,CicUniv.empty_ugraph) table initgoal in - if newmeta != maxm then + if changed then begin let opengoal = Cic.Meta(maxm,irl) in let proofterm,_ = @@ -2047,11 +2045,11 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = extended_status in (status,maxm::newgoals) end - else if newty = ty then + else (* if newty = ty then *) raise (ProofEngineTypes.Fail (lazy "no progress")) - else ProofEngineTypes.apply_tactic + (*else ProofEngineTypes.apply_tactic (ReductionTactics.simpl_tac ~pattern) - initialstatus + initialstatus*) ;; let demodulate_tac ~dbd ~pattern =