X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=cabca8259aefc524e89ed5b0e8e74f27049df70e;hb=f1c3f85a4e5acf2b6ee52b16103cbb95322016ac;hp=c5290694bfd96a4c5179b70eaeb665d8a742d3d7;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/components/ng_paramodulation/nCicProof.ml b/matita/components/ng_paramodulation/nCicProof.ml index c5290694b..cabca8259 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 @@ -39,32 +39,6 @@ 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 debug c r = prerr_endline r; c *) let debug c _ = c;; @@ -74,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 @@ -82,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) @@ -91,7 +65,7 @@ let debug c _ = c;; ;; - 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 @@ -115,7 +89,7 @@ let debug c _ = c;; 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 @@ -188,7 +162,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 @@ -207,18 +181,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 @@ -262,7 +236,7 @@ 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 = @@ -290,14 +264,14 @@ 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)); (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl, aux true ((id,([],lit))::seen) (id::tl))) *) - NCicSubstitution.subst + NCicSubstitution.subst status ~avoid_beta_redexes:true ~no_implicit:false refl (aux true ((id,([],lit))::seen) (id::tl)) else @@ -310,14 +284,14 @@ let debug c _ = c;; (* 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 + 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) | Terms.Step (_, id1, id2, dir, pos, subst) -> @@ -333,7 +307,7 @@ let debug c _ = c;; 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) @@ -350,9 +324,9 @@ let debug c _ = c;; 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 :"; @@ -376,9 +350,9 @@ let debug c _ = c;; 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 (* @@ -393,7 +367,7 @@ let debug c _ = c;; prerr_endline ("Positions :" ^ (String.concat ", " (List.map string_of_int pos)));*) - mk_predicate + mk_predicate status id2_ty amount (Subst.apply_subst subst id1_ty) pos vl, id2_ty, l,r @@ -409,14 +383,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