From 3df775cea96aae2d25dd9b47f9491711abc1c8fb Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 15 Jun 2006 09:37:49 +0000 Subject: [PATCH] some fixed done in Orsay: - supL is called on both sides if the equation is not oriented - contextualize_rewrites fixed if multiple equalities are used (equalities on different types) --- .../tactics/paramodulation/equality.ml | 49 ++++++++++--------- .../tactics/paramodulation/indexing.ml | 23 +++++++-- .../tactics/paramodulation/inference.ml | 2 +- .../tactics/paramodulation/saturation.ml | 41 ++++++++++++++-- 4 files changed, 83 insertions(+), 32 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 3bff5b574..2be5da062 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -223,7 +223,7 @@ let open_eq_ind args = let open_pred pred = match pred with - | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r])) + | Cic.Lambda (_,_,(Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r])) when LibraryObjects.is_eq_URI uri -> ty,uri,l,r | _ -> prerr_endline (CicPp.ppterm pred); assert false ;; @@ -336,15 +336,16 @@ let contextualize uri ty left right t = * that is used only by the base case * * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context + * ty_ctx is the type of ctx_d *) - let rec aux uri ty left right ctx_d = function + let rec aux uri ty left right ctx_d ctx_ty = function | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) when LibraryObjects.is_sym_eq_URI uri_sym -> let ty,l,r,p = open_sym ens tl in - mk_sym uri_sym ty l r (aux uri ty l r ctx_d p) + mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p) | Cic.LetIn (name,body,rest) -> (* we should go in body *) - Cic.LetIn (name,body,aux uri ty left right ctx_d rest) + Cic.LetIn (name,body,aux uri ty left right ctx_d ctx_ty rest) | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) when LibraryObjects.is_eq_ind_URI uri_ind || LibraryObjects.is_eq_ind_r_URI uri_ind -> @@ -355,12 +356,13 @@ let contextualize uri ty left right t = let is_not_fixed_lp = is_not_fixed lp in let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in (* extract the context and the fixed term from the predicate *) - let m, ctx_c = + let m, ctx_c, ty2 = let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in (* they were under a lambda *) - let m = CicSubstitution.subst (Cic.Implicit None) m in + let m = CicSubstitution.subst hole m in let ctx_c = CicSubstitution.subst hole ctx_c in - m, ctx_c + let ty2 = CicSubstitution.subst hole ty2 in + m, ctx_c, ty2 in (* create the compound context and put the terms under it *) let ctx_dc = compose_contexts ctx_d ctx_c in @@ -373,17 +375,17 @@ let contextualize uri ty left right t = (* now put the proofs in the compound context *) let p1 = (* p1: dc_what = d_m *) if is_not_fixed_lp then - aux uri ty1 c_what m ctx_d p1 + aux uri ty2 c_what m ctx_d ctx_ty p1 else - mk_sym uri_sym ty d_m dc_what - (aux uri ty1 m c_what ctx_d p1) + mk_sym uri_sym ctx_ty d_m dc_what + (aux uri ty2 m c_what ctx_d ctx_ty p1) in let p2 = (* p2: dc_other = dc_what *) if avoid_eq_ind then - mk_sym uri_sym ty dc_what dc_other - (aux uri ty1 what other ctx_dc p2) + mk_sym uri_sym ctx_ty dc_what dc_other + (aux uri ty1 what other ctx_dc ctx_ty p2) else - aux uri ty1 other what ctx_dc p2 + aux uri ty1 other what ctx_dc ctx_ty p2 in (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *) @@ -392,10 +394,11 @@ let contextualize uri ty left right t = dc_other,dc_what,d_m,p2,p1 else d_m,dc_what,dc_other, - (mk_sym uri_sym ty dc_what d_m p1), - (mk_sym uri_sym ty dc_other dc_what p2) + (mk_sym uri_sym ctx_ty dc_what d_m p1), + (mk_sym uri_sym ctx_ty dc_other dc_what p2) in - mk_trans uri_trans ty a b c paeqb pbeqc + mk_trans uri_trans ctx_ty a b c paeqb pbeqc + | t when ctx_d = hole -> t | t -> let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in @@ -406,16 +409,16 @@ let contextualize uri ty left right t = let ctx_d = CicSubstitution.lift 1 ctx_d in put_in_ctx ctx_d (Cic.Rel 1) in - let lty = CicSubstitution.lift 1 ty in + let lty = CicSubstitution.lift 1 ctx_ty in Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r)) in let d_left = put_in_ctx ctx_d left in let d_right = put_in_ctx ctx_d right in - let refl_eq = mk_refl uri ty d_left in - mk_sym uri_sym ty d_right d_left + let refl_eq = mk_refl uri ctx_ty d_left in + mk_sym uri_sym ctx_ty d_right d_left (mk_eq_ind uri_ind ty left pred refl_eq right t) in - aux uri ty left right hole t + aux uri ty left right hole ty t ;; let contextualize_rewrites t ty = @@ -729,9 +732,8 @@ let build_goal_proof l initial ty se = cic, p)) lets (letsno-1,initial) in - (proof,se) - (* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), - se *) + canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), + se ;; let refl_proof ty term = @@ -789,6 +791,7 @@ let meta_convertibility_aux table t1 t2 = let rec aux ((table_l, table_r) as table) t1 t2 = match t1, t2 with | C.Meta (m1, tl1), C.Meta (m2, tl2) -> + let tl1, tl2 = [],[] in let m1_binding, table_l = try List.assoc m1 table_l, table_l with Not_found -> m2, (m1, m2)::table_l diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index e72ed64da..925aab6e0 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -728,6 +728,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) -> @@ -1057,11 +1058,23 @@ let superposition_left (metasenv, context, ugraph) table goal = 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 Equality.SuperpositionLeft) expansions + + if c = Utils.Incomparable then + let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in + let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in + prerr_endline "ZZZ"; + 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 + + else + 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 Equality.SuperpositionLeft) expansions ;; (** demodulation, when the target is a goal *) diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml index 91fcee8a2..6004de44c 100644 --- a/helm/software/components/tactics/paramodulation/inference.ml +++ b/helm/software/components/tactics/paramodulation/inference.ml @@ -51,7 +51,7 @@ let rec check_irl start = function let rec is_simple_term = function | Cic.Appl ((Cic.Meta _)::_) -> false | Cic.Appl l -> List.for_all is_simple_term l - | Cic.Meta (i, l) -> check_irl 1 l + | Cic.Meta (i, l) -> let l = [] in check_irl 1 l | Cic.Rel _ -> true | Cic.Const _ -> true | Cic.MutInd (_, _, []) -> true diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 1282ed27f..fe63c7d66 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -708,7 +708,6 @@ let backward_simplify env new' ?passive active = active, passive, newa, newp *) ;; - let close env new' given = let new_pos, new_table, min_weight = List.fold_left @@ -1202,6 +1201,17 @@ let check_if_goal_is_identity env = function when left = right && iseq uri -> let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in Some (goalproof, reflproof, 0, Subst.empty_subst,m) + | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]) + when iseq uri -> + (let _,context,_ = env in + try + let s,m,_ = + Inference.unification m m context left right CicUniv.empty_ugraph + in + let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in + let m = Subst.apply_subst_metasenv s m in + Some (goalproof, reflproof, 0, s,m) + with _ -> None) | _ -> None ;; @@ -1270,10 +1280,16 @@ let infer_goal_set env active goals = let infer_goal_set_with_current env current goals = let active_goals, passive_goals = goals in let _,table,_ = build_table [current] in + let _,_,_,_,id = Equality.open_equality current in active_goals, List.fold_left (fun acc g -> let new' = Indexing.superposition_left env table g in + if id = 2 then + begin + prerr_endline "XXXXXXX"; + List.iter (fun _,_,e -> prerr_endline (CicPp.ppterm e)) new' ; + end; acc @ new') passive_goals active_goals ;; @@ -1288,6 +1304,7 @@ let size_of_goal_set_p (_,l) = List.length l;; let given_clause ((_,context,_) as env) goals theorems passive active max_iterations max_time = + let names = names_of_context context in let initial_time = Unix.gettimeofday () in let iterations_left iterno = let now = Unix.gettimeofday () in @@ -1339,13 +1356,18 @@ let given_clause ParamodulationFailure "No more passive"(*maybe this is a success! *) else begin + let goals = infer_goal_set env active goals in + let goals = infer_goal_set env active goals in let goals = infer_goal_set env active goals in let current, passive = select env goals passive in + let _,_,goaltype = List.hd (fst goals) in + prerr_endline (Printf.sprintf "Current goal = %s\n" + (CicPp.pp goaltype names)); prerr_endline (Printf.sprintf "Selected = %s\n" (Equality.string_of_equality ~env current)); (* SIMPLIFICATION OF CURRENT *) let res = - forward_simplify env (Positive, current) ~passive active + forward_simplify env (Positive, current) (*~passive*) active in match res with | None -> step goals theorems passive active (iterno+1) @@ -1376,6 +1398,14 @@ let given_clause | Some p, Some rp -> simplify (new' @ p @ rp) active passive in let active, passive, new' = simplify new' active passive in + if iterno = 36 || iterno = 654 then + begin + prerr_endline "..................."; + List.iter + (fun x -> prerr_endline (Equality.string_of_equality +~env:env x)) new'; + prerr_endline "FINE..................."; + end; prerr_endline "simpl goal with new"; let goals = let a,b,_ = build_table new' in @@ -1732,6 +1762,8 @@ let saturate let initial = Equality.add_subst subsumption_subst newproof in Equality.build_goal_proof goalproof initial type_of_goal side_effects in + let goal_proof = Subst.apply_subst subsumption_subst goal_proof in + let metas_still_open_in_proof = Utils.metas_of_term goal_proof in (*prerr_endline (CicPp.pp goal_proof names);*) (* ?? *) let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in @@ -1750,7 +1782,10 @@ let saturate | None -> [i,context,ty], (Cic.Meta(i,[]))::acc2, (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) - ([],[],[],None) proof_menv + ([],[],[],None) + (List.filter + (fun (i,_,_) -> List.mem i metas_still_open_in_proof) + proof_menv) in let replace where = (* we need this fake equality since the metas of the hypothesis may be -- 2.39.2