From c471db7f3e949af87d9206861d9b36a13dfce45a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 4 Mar 2010 07:52:45 +0000 Subject: [PATCH] Corrected a bug relative to the application of substs in the "on goal" case. --- .../components/ng_paramodulation/nCicProof.ml | 39 ++++++++++++------- 1 file changed, 26 insertions(+), 13 deletions(-) diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index b80ac7e9c..b5f4af9d6 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -12,7 +12,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl - + let eqsig = ref (fun _ -> assert false);; let set_sig f = eqsig:= f;; let get_sig = fun x -> !eqsig x;; @@ -219,6 +219,14 @@ let debug c _ = c;; ;; let mk_proof (bag : NCic.term Terms.bag) mp subst steps = + let module NCicBlob = + NCicBlob.NCicBlob( + struct + let metasenv = [] let subst = [] let context = [] + end) + in + let module Pp = Pp.Pp(NCicBlob) + in let module Subst = FoSubst in let position i l = let rec aux = function @@ -261,11 +269,11 @@ let debug c _ = c;; let amount = List.length seen in let lit,vl,proof = get_literal id in if not ongoal && id = mp then - let lit = Subst.apply_subst subst lit in + let lit = Subst.apply_subst subst lit in let eq_ty = extract amount [] lit in let refl = mk_refl eq_ty in - (*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*) - (* (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl, + (* prerr_endline ("Reached m point, id=" ^ (string_of_int id)); + (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl, aux true ((id,([],lit))::seen) (id::tl))) *) NCicSubstitution.subst ~avoid_beta_redexes:true ~no_implicit:false refl @@ -277,8 +285,8 @@ let debug c _ = c;; aux ongoal seen tl | Terms.Step _ when tl=[] -> assert false | Terms.Exact ft -> - (* prerr_endline ("Exact for " ^ (string_of_int id));*) - (* + (* + prerr_endline ("Exact for " ^ (string_of_int id)); NCic.LetIn ("clause_" ^ string_of_int id, close_with_forall vl (extract amount vl lit), close_with_lambdas vl (extract amount vl ft), @@ -292,10 +300,12 @@ let debug c _ = c;; ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) | Terms.Step (_, id1, id2, dir, pos, subst) -> let id, id1,(lit,vl,proof) = - if ongoal then id1,id,get_literal id1 - else id,id1,(lit,vl,proof) - in - let vl = if ongoal then [](*Subst.filter subst vl*) else vl in + if ongoal then + let lit,vl,proof = get_literal id1 in + id1,id,(Subst.apply_subst subst lit, + Subst.filter subst vl, proof) + else id,id1,(lit,vl,proof) in + let vl = if ongoal then [] else vl in let proof_of_id id = let vars = List.rev (vars_of id seen) in let args = List.map (Subst.apply_subst subst) vars in @@ -347,12 +357,15 @@ let debug c _ = c;; extract amount vl (Subst.apply_subst subst r) | _ -> assert false in - (*prerr_endline "mk_predicate :"; + (* + prerr_endline "mk_predicate :"; if ongoal then prerr_endline "ongoal=true" else prerr_endline "ongoal=false"; prerr_endline ("id=" ^ string_of_int id); - prerr_endline ("id1=" ^ string_of_int id1); - prerr_endline ("id2=" ^ string_of_int id2); + prerr_endline ("id1=" ^ string_of_int id1 + ^": " ^ Pp.pp_foterm id1_ty); + prerr_endline ("id2=" ^ string_of_int id2 + ^ ": " ^ NCicPp.ppterm [][][] id2_ty); prerr_endline ("Positions :" ^ (String.concat ", " (List.map string_of_int pos)));*) -- 2.39.2