X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=9a7285062a393e196d4dfb1ef0ab0413194d9e5d;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=c5290694bfd96a4c5179b70eaeb665d8a742d3d7;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index c5290694b..9a7285062 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -11,68 +11,45 @@ (* $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;; +let reference_of_oxuri = ref (fun _ -> assert false);; +let set_reference_of_oxuri f = reference_of_oxuri := f;; -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 set_default_sig () = - (*prerr_endline "setting default sig";*) - eqsig := default_sig - -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 eqP () = + let r = + !reference_of_oxuri + (UriManager.uri_of_string + "cic:/matita/logic/equality/eq.ind#xpointer(1/1)") + in + NCic.Const r ;; -(* let debug c r = prerr_endline r; c *) -let debug c _ = c;; + let eq_ind () = + let r = + !reference_of_oxuri + (UriManager.uri_of_string + "cic:/matita/logic/equality/eq_ind.con") + in + NCic.Const r + ;; - 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 eq_ind_r () = + let r = + !reference_of_oxuri + (UriManager.uri_of_string + "cic:/matita/logic/equality/eq_elim_r.con") + in + NCic.Const r + ;; + let eq_refl () = + let r = + !reference_of_oxuri + (UriManager.uri_of_string + "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)") + in + NCic.Const r + ;; let extract lift vl t = let rec pos i = function @@ -90,7 +67,6 @@ let debug c _ = c;; extract t ;; - let mk_predicate hole_type amount ft p1 vl = let rec aux t p = match p with @@ -99,16 +75,16 @@ let debug c _ = c;; match t with | Terms.Leaf _ | Terms.Var _ -> - let module NCicBlob = NCicBlob.NCicBlob( - struct - let metasenv = [] let subst = [] let context = [] - end) - in - let module Pp = Pp.Pp(NCicBlob) in + let module Pp = + Pp.Pp(NCicBlob.NCicBlob( + struct + let metasenv = [] let subst = [] let context = [] + end)) + 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); + prerr_endline ("leading to: " ^ Pp.pp_foterm t); assert false | Terms.Node l -> let l = @@ -123,110 +99,7 @@ let debug c _ = c;; NCic.Lambda("x", hole_type, aux ft (List.rev p1)) ;; - 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 mk_proof (bag : NCic.term Terms.bag) mp steps = let module Subst = FoSubst in let position i l = let rec aux = function @@ -253,35 +126,11 @@ 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 -> t (* assert false *) + | Terms.Predicate t -> assert false | Terms.Equation (l,r,ty,_) -> Terms.Node [ Terms.Leaf eqP(); ty; l; r] in - 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 + lit, vl, proof in let rec aux ongoal seen = function | [] -> NCic.Rel 1 @@ -289,88 +138,40 @@ 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 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)) + ((*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))) 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 - 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 + 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 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 = @@ -381,45 +182,34 @@ let debug c _ = c;; 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 - ^": " ^ 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)));*) + (*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_predicate id2_ty amount (Subst.apply_subst subst id1_ty) pos vl, id2_ty, l,r in - 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 + let l, r, eq_ind = + if (ongoal=true) = (dir=Terms.Left2Right) then + r,l,eq_ind_r () else - 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) + 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) in - aux false [] steps, proof_type + aux false [] steps ;;