X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=c5290694bfd96a4c5179b70eaeb665d8a742d3d7;hb=12d58352dbd62df65d44becc0f69fc5a7b370866;hp=b80ac7e9ce7007aa8c83c1da55c8d4a477b9021a;hpb=12f96bd48b460d06f9858a334ee7c52d6831712f;p=helm.git diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index b80ac7e9c..c5290694b 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;; @@ -207,7 +207,7 @@ let debug c _ = c;; List.fold_left (fun (i,acc) t -> i+1, - let f = extract amount vl f in + let f = extract amount vl f in if i = n then let imp = NCic.Implicit `Term in NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp:: @@ -218,7 +218,15 @@ let debug c _ = c;; in aux ft (List.rev pl) ;; - let mk_proof (bag : NCic.term Terms.bag) mp subst steps = + let mk_proof ?(demod=false) (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 @@ -245,7 +253,7 @@ let debug c _ = c;; let get_literal id = let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in let lit =match lit with - | Terms.Predicate t -> assert false + | Terms.Predicate t -> t (* assert false *) | Terms.Equation (l,r,ty,_) -> Terms.Node [ Terms.Leaf eqP(); ty; l; r] in @@ -255,17 +263,39 @@ let debug c _ = c;; let lit,_,_ = get_literal mp in let lit = Subst.apply_subst subst lit in extract 0 [] lit in + (* composition of all subst acting on goal *) + let res_subst = + let rec rsaux ongoal acc = + function + | [] -> acc (* is the final subst for refl *) + | id::tl when ongoal -> + let lit,vl,proof = get_literal id in + (match proof with + | Terms.Exact _ -> rsaux ongoal acc tl + | Terms.Step (_, _, _, _, _, s) -> + rsaux ongoal (s@acc) tl) + | id::tl -> + (* subst is the the substitution for refl *) + rsaux (id=mp) subst tl + in + let r = rsaux false [] steps in + (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r); + prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *) + r + in let rec aux ongoal seen = function | [] -> NCic.Rel 1 | id :: tl -> 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, + let refl = + if demod then NCic.Implicit `Term + else 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, aux true ((id,([],lit))::seen) (id::tl))) *) NCicSubstitution.subst ~avoid_beta_redexes:true ~no_implicit:false refl @@ -277,8 +307,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 +322,14 @@ 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 res_subst lit, + Subst.filter res_subst vl, proof) + else id,id1,(lit,vl,proof) in + (* free variables remaining in the goal should not + be abstracted: we do not want to prove a generalization *) + 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 +381,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)));*) @@ -372,7 +409,8 @@ let debug c _ = c;; let body = aux ongoal ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl in - if NCicUntrusted.count_occurrences [] 0 body <= 1 then + let occ= NCicUntrusted.count_occurrences [] 1 body in + if occ <= 1 then NCicSubstitution.subst ~avoid_beta_redexes:true ~no_implicit:false (close_with_lambdas vl rewrite_step) body