X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=f34b35748885d8ae4e2ddea34b2c3c8791909dbd;hb=21e21b3b061807035bbd18d29d7a4fd8086ca10d;hp=f840d91f902233642e247cc6fdab1c440c4b0d32;hpb=e14fdca3a845ad0b88a34497f41472c3e7f8473b;p=helm.git diff --git a/matita/components/ng_paramodulation/nCicProof.ml b/matita/components/ng_paramodulation/nCicProof.ml index f840d91f9..f34b35748 100644 --- a/matita/components/ng_paramodulation/nCicProof.ml +++ b/matita/components/ng_paramodulation/nCicProof.ml @@ -19,19 +19,19 @@ let get_sig = fun x -> !eqsig x;; let default_sig = function | Eq -> - let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in + let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in NCic.Const ref | EqInd_l -> - let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_l.con" in + let uri = NUri.uri_of_string "cic:/matita/basics/logic/rewrite_l.con" in let ref = NReference.reference_of_spec uri (NReference.Def(1)) in NCic.Const ref | EqInd_r -> - let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_r.con" in + let uri = NUri.uri_of_string "cic:/matita/basics/logic/rewrite_r.con" in let ref = NReference.reference_of_spec uri (NReference.Def(3)) in NCic.Const ref | Refl -> - let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in + let uri = NUri.uri_of_string "cic:/matita/basics/logic/eq.ind" in let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in NCic.Const ref @@ -48,7 +48,7 @@ let debug c _ = c;; let eq_refl() = debug (!eqsig Refl) "refl";; - let extract lift vl t = + let extract status lift vl t = let rec pos i = function | [] -> raise Not_found | j :: tl when j <> i -> 1+ pos i tl @@ -56,7 +56,7 @@ let debug c _ = c;; in let vl_len = List.length vl in let rec extract = function - | Terms.Leaf x -> NCicSubstitution.lift (vl_len+lift) x + | Terms.Leaf x -> NCicSubstitution.lift status (vl_len+lift) x | Terms.Var j -> (try NCic.Rel (pos j vl) with Not_found -> NCic.Implicit `Term) | Terms.Node l -> NCic.Appl (List.map extract l) @@ -64,8 +64,7 @@ let debug c _ = c;; extract t ;; - - let mk_predicate hole_type amount ft p1 vl = + let mk_predicate status hole_type amount ft p1 vl = let rec aux t p = match p with | [] -> NCic.Rel 1 @@ -79,17 +78,17 @@ let debug c _ = c;; end) in let module Pp = Pp.Pp(NCicBlob) in - prerr_endline ("term: " ^ Pp.pp_foterm ft); - prerr_endline ("path: " ^ String.concat "," + (* prerr_endline ("term: " ^ Pp.pp_foterm ft); + prerr_endline ("path: " ^ String.concat "," (List.map string_of_int p1)); - prerr_endline ("leading to: " ^ Pp.pp_foterm t); + prerr_endline ("leading to: " ^ Pp.pp_foterm t); *) assert false | Terms.Node l -> let l = HExtlib.list_mapi (fun t i -> if i = n then aux t tl - else extract amount (0::vl) t) + else extract status amount (0::vl) t) l in NCic.Appl l @@ -132,7 +131,7 @@ let debug c _ = c;; NCic.Implicit `Term; eq; NCic.Implicit `Term]; ;; - let trans eq p = + let trans eq _p = let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/trans.con" in let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term; @@ -162,7 +161,7 @@ let debug c _ = c;; | _ -> assert false - let mk_morphism eq amount ft pl vl = + let mk_morphism status eq amount ft pl vl = let rec aux t p = match p with | [] -> eq @@ -181,18 +180,18 @@ let debug c _ = c;; List.fold_left (fun (i,acc) t -> i+1, - let f = extract amount vl f in + let _f = extract status amount vl f in if i = n then let imp = NCic.Implicit `Term in NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp:: [aux t tl]) else - NCicUntrusted.mk_appl acc [extract amount vl t] - ) (1,extract amount vl f) l) + NCicUntrusted.mk_appl acc [extract status amount vl t] + ) (1,extract status amount vl f) l) in aux ft (List.rev pl) ;; - let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps = + let mk_proof status ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps= let module NCicBlob = NCicBlob.NCicBlob( struct @@ -202,10 +201,15 @@ let debug c _ = c;; let module Pp = Pp.Pp(NCicBlob) in let module Subst = FoSubst in + (*let compose subst1 subst2 = + let s1 = List.map (fun (x,t) -> (x, Subst.apply_subst subst2 t)) subst1 in + let s2 = List.filter (fun (m,_) -> not (List.mem_assoc m s1)) subst2 + in s1 @ s2 + in*) let position i l = let rec aux = function | [] -> assert false - | (j,_) :: tl when i = j -> 1 + | (j,_) :: _ when i = j -> 1 | _ :: tl -> 1 + aux tl in aux l @@ -236,26 +240,9 @@ let debug c _ = c;; let proof_type = let lit,_,_ = get_literal mp in let lit = Subst.apply_subst subst lit in - extract 0 [] lit in + extract status 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 + let res_subst = subst in let rec aux ongoal seen = function | [] -> NCic.Rel 1 @@ -264,110 +251,76 @@ let debug c _ = c;; let lit,vl,proof = get_literal id in if not ongoal && id = mp then let lit = Subst.apply_subst subst lit in - let eq_ty = extract amount [] lit in + let eq_ty = extract status amount [] lit in let refl = if demod then NCic.Implicit `Term else mk_refl eq_ty in - (* prerr_endline ("Reached m point, id=" ^ (string_of_int id)); + (* 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 + let res = NCicSubstitution.subst status ~avoid_beta_redexes:true ~no_implicit:false refl (aux true ((id,([],lit))::seen) (id::tl)) + in res else match proof with | Terms.Exact _ when tl=[] -> - (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*) + (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id)); *) aux ongoal seen tl | Terms.Step _ when tl=[] -> assert false | Terms.Exact ft -> (* 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), + close_with_forall vl (extract status amount vl lit), + close_with_lambdas vl (extract status amount vl ft), aux ongoal ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) - *) - NCicSubstitution.subst + *) + let res = NCicSubstitution.subst status ~avoid_beta_redexes:true ~no_implicit:false - (close_with_lambdas vl (extract amount vl ft)) + (close_with_lambdas vl (extract status amount vl ft)) (aux ongoal ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) + in res | Terms.Step (_, id1, id2, dir, pos, subst) -> - let id, id1,(lit,vl,proof) = + (* prerr_endline (if ongoal then "on goal" else "not on goal"); + prerr_endline (Pp.pp_substitution subst); *) + (* let subst = if ongoal then res_subst else subst in *) + let id, id1,(lit,vl,_proof) = 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) + 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 *) + (* prerr_endline ("variables = " ^ String.concat "," + (List.map string_of_int vl)); *) 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 - let args = List.map (extract amount vl) args in + let args = List.map (extract status amount vl) args in let rel_for_id = NCic.Rel (List.length vl + position id seen) in if args = [] then rel_for_id else NCic.Appl (rel_for_id::args) in let p_id1 = proof_of_id id1 in let p_id2 = proof_of_id id2 in -(* - let morphism, l, r = - let p = - if (ongoal=true) = (dir=Terms.Left2Right) then - p_id2 - else sym p_id2 in - let id1_ty = ty_of id1 seen in - let id2_ty,l,r = - match ty_of id2 seen with - | Terms.Node [ _; t; l; r ] -> - extract amount vl (Subst.apply_subst subst t), - extract amount vl (Subst.apply_subst subst l), - extract amount vl (Subst.apply_subst subst r) - | _ -> assert false - in - (*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 ("Positions :" ^ - (String.concat ", " - (List.map string_of_int pos)));*) - mk_morphism - p amount (Subst.apply_subst subst id1_ty) pos vl, - l,r - in - let rewrite_step = iff1 morphism p_id1 - in -*) let pred, hole_type, l, r = let id1_ty = ty_of id1 seen in let id2_ty,l,r = match ty_of id2 seen with | Terms.Node [ _; t; l; r ] -> - extract amount vl (Subst.apply_subst subst t), - extract amount vl (Subst.apply_subst subst l), - extract amount vl (Subst.apply_subst subst r) + extract status amount vl (Subst.apply_subst subst t), + extract status amount vl (Subst.apply_subst subst l), + extract status amount vl (Subst.apply_subst subst r) | _ -> assert false in - (* - 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 - ^": " ^ 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)));*) - mk_predicate + (* let _ = prerr_endline ("body = " ^(Pp.pp_foterm id1_ty)) + in *) + mk_predicate status id2_ty amount (Subst.apply_subst subst id1_ty) pos vl, id2_ty, l,r @@ -383,14 +336,15 @@ let debug c _ = c;; let body = aux ongoal ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl in - let occ= NCicUntrusted.count_occurrences [] 1 body in + let occ = + NCicUntrusted.count_occurrences status [] 1 body in if occ <= 1 then - NCicSubstitution.subst + NCicSubstitution.subst status ~avoid_beta_redexes:true ~no_implicit:false (close_with_lambdas vl rewrite_step) body else NCic.LetIn ("clause_" ^ string_of_int id, - close_with_forall vl (extract amount vl lit), + close_with_forall vl (extract status amount vl lit), (* NCic.Implicit `Type, *) close_with_lambdas vl rewrite_step, body) in