X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=c5290694bfd96a4c5179b70eaeb665d8a742d3d7;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=1e50999e9e14243fd6dc976f7c4eb0372c2ccaf2;hpb=2c2b31c242aa81dc6f3c73e7e2a3ec0789a21edd;p=helm.git diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index 1e50999e9..c5290694b 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -11,42 +11,69 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) - let eqP () = - let r = - OCic2NCic.reference_of_oxuri - (UriManager.uri_of_string - "cic:/matita/logic/equality/eq.ind#xpointer(1/1)") - in - NCic.Const r - ;; +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;; - let eq_ind () = - let r = - OCic2NCic.reference_of_oxuri - (UriManager.uri_of_string - "cic:/matita/logic/equality/eq_ind.con") - in - NCic.Const r - ;; +let default_sig = function + | Eq -> + let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/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 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 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 ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in + NCic.Const ref - let eq_ind_r () = - let r = - OCic2NCic.reference_of_oxuri - (UriManager.uri_of_string - "cic:/matita/logic/equality/eq_elim_r.con") - in - NCic.Const r - ;; +let set_default_sig () = + (*prerr_endline "setting default sig";*) + eqsig := default_sig - let eq_refl () = - let r = - OCic2NCic.reference_of_oxuri - (UriManager.uri_of_string - "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)") - in - NCic.Const r +let set_reference_of_oxuri reference_of_oxuri = + prerr_endline "setting oxuri in nCicProof"; + let nsig = function + | Eq -> + NCic.Const + (reference_of_oxuri + (UriManager.uri_of_string + "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")) + | EqInd_l -> + NCic.Const + (reference_of_oxuri + (UriManager.uri_of_string + "cic:/matita/logic/equality/eq_ind.con")) + | EqInd_r -> + NCic.Const + (reference_of_oxuri + (UriManager.uri_of_string + "cic:/matita/logic/equality/eq_elim_r.con")) + | Refl -> + NCic.Const + (reference_of_oxuri + (UriManager.uri_of_string + "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")) + in eqsig:= nsig ;; +(* let debug c r = prerr_endline r; c *) +let debug c _ = c;; + + let eqP() = debug (!eqsig Eq) "eq" ;; + let eq_ind() = debug (!eqsig EqInd_l) "eq_ind" ;; + let eq_ind_r() = debug (!eqsig EqInd_r) "eq_ind_r";; + let eq_refl() = debug (!eqsig Refl) "refl";; + + let extract lift vl t = let rec pos i = function | [] -> raise Not_found @@ -63,6 +90,7 @@ extract t ;; + let mk_predicate hole_type amount ft p1 vl = let rec aux t p = match p with @@ -71,9 +99,16 @@ match t with | Terms.Leaf _ | Terms.Var _ -> -(* prerr_endline ("term: " ^ ppfot ft); *) + let module NCicBlob = NCicBlob.NCicBlob( + struct + let metasenv = [] let subst = [] let context = [] + end) + in + let module Pp = Pp.Pp(NCicBlob) in + 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); assert false | Terms.Node l -> let l = @@ -88,7 +123,110 @@ NCic.Lambda("x", hole_type, aux ft (List.rev p1)) ;; - let mk_proof (bag : NCic.term Terms.bag) mp steps = + let dag = + let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/prop1.con" in + let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,4)) in + NCic.Const ref + ;; + + (* + let eq_setoid = + let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq.con" in + let ref = NReference.reference_of_spec uri (NReference.Fix(0,0,2)) in + NCic.Const ref + ;; + *) + + let sym eq = + let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/sym.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; + NCic.Implicit `Term; NCic.Implicit `Term; eq]; + ;; + + let eq_morphism1 eq = + let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism1.con" in + let u = NReference.reference_of_spec u (NReference.Def 4) in + NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term; + NCic.Implicit `Term; NCic.Implicit `Term; eq]; + ;; + + let eq_morphism2 eq = + let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism2.con" in + let u = NReference.reference_of_spec u (NReference.Def 4) in + NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term; + NCic.Implicit `Term; eq; NCic.Implicit `Term]; + ;; + + 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; + NCic.Implicit `Term; NCic.Implicit `Term; NCic.Implicit `Term; eq] + ;; + + let iff1 eq p = + let uri = NUri.uri_of_string "cic:/matita/ng/logic/connectives/if.con" in + let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,1)) in + NCic.Appl[NCic.Const ref; NCic.Implicit `Type; NCic.Implicit `Type; + eq; p]; + ;; + +(* + let mk_refl = function + | NCic.Appl [_; _; x; _] -> + let uri= NUri.uri_of_string "cic:/matita/ng/properties/relations/refl.con" in + let ref = NReference.reference_of_spec uri (NReference.Fix(0,1,3)) in + NCic.Appl[NCic.Const ref; NCic.Implicit `Type; NCic.Implicit `Term; + NCic.Implicit `Term(*x*)] + | _ -> assert false +*) + + let mk_refl = function + | NCic.Appl [_; ty; l; _] + -> NCic.Appl [eq_refl();ty;l] + | _ -> assert false + + + let mk_morphism eq amount ft pl vl = + let rec aux t p = + match p with + | [] -> eq + | n::tl -> + prerr_endline (string_of_int n); + match t with + | Terms.Leaf _ + | Terms.Var _ -> assert false + | Terms.Node [] -> assert false + | Terms.Node [ Terms.Leaf eqt ; _; l; r ] + when (eqP ()) = eqt -> + if n=2 then eq_morphism1 (aux l tl) + else eq_morphism2 (aux r tl) + | Terms.Node (f::l) -> + snd ( + List.fold_left + (fun (i,acc) t -> + i+1, + 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:: + [aux t tl]) + else + NCicUntrusted.mk_appl acc [extract amount vl t] + ) (1,extract amount vl f) l) + in aux ft (List.rev pl) + ;; + + 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 @@ -113,13 +251,37 @@ t vl in let get_literal id = - let (_, lit, vl, proof),_ = Terms.M.find id bag in + 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 - lit, vl, proof + lit, vl, proof + in + let proof_type = + 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 @@ -127,40 +289,88 @@ let amount = List.length seen in let lit,vl,proof = get_literal id in if not ongoal && id = mp then - ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*) - NCic.LetIn ("clause_" ^ string_of_int id, - extract amount [] lit, - (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]), - aux true ((id,([],lit))::seen) (id::tl))) + let lit = Subst.apply_subst subst lit in + let eq_ty = extract 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)); + (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 + (aux true ((id,([],lit))::seen) (id::tl)) else match proof with | Terms.Exact _ when tl=[] -> - (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*) - aux ongoal seen tl + (* 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));*) + (* + 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), aux ongoal ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) + *) + NCicSubstitution.subst + ~avoid_beta_redexes:true ~no_implicit:false + (close_with_lambdas vl (extract amount vl ft)) + (aux ongoal + ((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 let args = List.map (extract amount vl) args in - let rel_for_id = NCic.Rel (List.length vl + position id seen) in - if args = [] then rel_for_id + 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 = @@ -171,34 +381,45 @@ 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)));*) + (* + 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 id2_ty amount (Subst.apply_subst subst id1_ty) pos vl, id2_ty, l,r in - let l, r, eq_ind = - if (ongoal=true) = (dir=Terms.Left2Right) then - r,l,eq_ind_r () + let rewrite_step = + if (ongoal=true) = (dir=Terms.Left2Right) then + NCic.Appl + [eq_ind_r(); hole_type; r; pred; p_id1; l; p_id2] + else + NCic.Appl + [ eq_ind(); hole_type; l; pred; p_id1; r; p_id2] + in + 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 + if occ <= 1 then + NCicSubstitution.subst + ~avoid_beta_redexes:true ~no_implicit:false + (close_with_lambdas vl rewrite_step) body else - l,r,eq_ind () - in - NCic.LetIn ("clause_" ^ string_of_int id, - close_with_forall vl (extract amount vl lit), - (* NCic.Implicit `Type, *) - close_with_lambdas vl - (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]), - aux ongoal - ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) + NCic.LetIn ("clause_" ^ string_of_int id, + close_with_forall vl (extract amount vl lit), + (* NCic.Implicit `Type, *) + close_with_lambdas vl rewrite_step, body) in - aux false [] steps + aux false [] steps, proof_type ;;