X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=b80ac7e9ce7007aa8c83c1da55c8d4a477b9021a;hb=12f96bd48b460d06f9858a334ee7c52d6831712f;hp=0bc4dc2c2dff39664b93537df7fbf0ed8d0018dd;hpb=cf89508024f0a19023bb1bac343012d54e860d9d;p=helm.git diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index 0bc4dc2c2..b80ac7e9c 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -21,19 +21,19 @@ 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 + 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 + 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 + 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 + NCic.Const ref let set_default_sig () = (*prerr_endline "setting default sig";*) @@ -43,25 +43,25 @@ 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)")) + 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")) + 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")) + 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)")) + NCic.Const + (reference_of_oxuri + (UriManager.uri_of_string + "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")) in eqsig:= nsig ;; @@ -90,6 +90,7 @@ let debug c _ = c;; extract t ;; + let mk_predicate hole_type amount ft p1 vl = let rec aux t p = match p with @@ -98,16 +99,16 @@ let debug c _ = c;; match t with | Terms.Leaf _ | Terms.Var _ -> - let module Pp = - Pp.Pp(NCicBlob.NCicBlob( - struct - let metasenv = [] let subst = [] let context = [] - end)) - in + 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); + prerr_endline ("leading to: " ^ Pp.pp_foterm t); assert false | Terms.Node l -> let l = @@ -122,29 +123,100 @@ 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_morphism eq amount ft p1 vl = + 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 l -> - let dag,arity = ____ in - let l = - HExtlib.list_rev_mapi_filter - (fun t i -> - if i < arity then None - else if i = n then Some (aux t tl) - else Some (NCic.Appl [refl ...])) - l - in - NCic.Appl (dag::l) + | 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 (bag : NCic.term Terms.bag) mp subst steps = let module Subst = FoSubst in @@ -177,68 +249,94 @@ let debug c _ = c;; | Terms.Equation (l,r,ty,_) -> Terms.Node [ Terms.Leaf eqP(); ty; l; r] in - lit, vl, proof + lit, vl, proof in - let mk_refl = function - | NCic.Appl [_; ty; l; _] - -> NCic.Appl [eq_refl();ty;l] - | _ -> assert false - in let proof_type = let lit,_,_ = get_literal mp in let lit = Subst.apply_subst subst lit in - extract 0 [] lit in + extract 0 [] lit 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 + 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, + (* (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 + 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)) + ~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 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 = @@ -249,42 +347,40 @@ 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); - 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); + 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 l, r, eq_ind = - if (ongoal=true) = (dir=Terms.Left2Right) then - r,l,eq_ind_r () - else - l,r,eq_ind () - in - 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 - NCicSubstitution.subst - ~avoid_beta_redexes:true ~no_implicit:false - (close_with_lambdas vl (NCic.Appl - [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ])) - body + 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.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 ]), - body) + 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 + if NCicUntrusted.count_occurrences [] 0 body <= 1 then + NCicSubstitution.subst + ~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), + (* NCic.Implicit `Type, *) + close_with_lambdas vl rewrite_step, body) in aux false [] steps, proof_type ;;