X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=0bc4dc2c2dff39664b93537df7fbf0ed8d0018dd;hb=e22808c929a9cebf5e4e2b7428ff0cbf89e1f92a;hp=9a7285062a393e196d4dfb1ef0ab0413194d9e5d;hpb=7288b45eacf9f7dcd118b3b89b81ff19ae9d6ce5;p=helm.git diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index 9a7285062..0bc4dc2c2 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -11,45 +11,68 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) -let reference_of_oxuri = ref (fun _ -> assert false);; -let set_reference_of_oxuri f = reference_of_oxuri := f;; +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 eqP () = - let r = - !reference_of_oxuri - (UriManager.uri_of_string - "cic:/matita/logic/equality/eq.ind#xpointer(1/1)") - 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 () = - let r = - !reference_of_oxuri - (UriManager.uri_of_string - "cic:/matita/logic/equality/eq_ind.con") - in - NCic.Const r - ;; +let set_default_sig () = + (*prerr_endline "setting default sig";*) + eqsig := default_sig - 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 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 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 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 @@ -99,7 +122,31 @@ let set_reference_of_oxuri f = reference_of_oxuri := f;; NCic.Lambda("x", hole_type, aux ft (List.rev p1)) ;; - let mk_proof (bag : NCic.term Terms.bag) mp steps = +(* + let mk_morphism eq amount ft p1 vl = + let rec aux t p = + match p with + | [] -> eq + | n::tl -> + 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) + in aux ft (List.rev pl) + ;; +*) + + let mk_proof (bag : NCic.term Terms.bag) mp subst steps = let module Subst = FoSubst in let position i l = let rec aux = function @@ -132,17 +179,30 @@ let set_reference_of_oxuri f = reference_of_oxuri := f;; in 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 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 - ((*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 = 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=[] -> @@ -151,11 +211,18 @@ let set_reference_of_oxuri f = reference_of_oxuri := f;; | 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), 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 @@ -202,14 +269,23 @@ let set_reference_of_oxuri f = reference_of_oxuri := f;; else l,r,eq_ind () in - NCic.LetIn ("clause_" ^ string_of_int id, - close_with_forall vl (extract amount vl lit), + 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 + 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 ]), - aux ongoal - ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) + close_with_lambdas vl (NCic.Appl + [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]), + body) in - aux false [] steps + aux false [] steps, proof_type ;;