From: Enrico Tassi Date: Wed, 17 Jun 2009 13:35:12 +0000 (+0000) Subject: proof reconstruction almost OK X-Git-Tag: make_still_working~3855 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a9e037fe189335607ab5d10523c836d8c7717245;p=helm.git proof reconstruction almost OK --- diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index 5aded5329..621b22559 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -102,6 +102,15 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct NCic.Const r ;; + 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 extract lift vl t = let rec pos i = function | [] -> raise Not_found @@ -124,7 +133,7 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct | Terms.Node l -> "(" ^ String.concat " " (List.map ppfot l) ^ ")" ;; - let mk_predicate amount ft p vl = + let mk_predicate hole_type amount ft p vl = let rec aux t p = match p with | [] -> NCic.Rel 1 @@ -146,10 +155,10 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct in NCic.Appl l in - NCic.Lambda("x", NCic.Implicit `Type, aux ft (List.rev p)) + NCic.Lambda("x", hole_type, aux ft (List.rev p)) ;; - let mk_proof (bag : NCic.term Terms.bag) steps = + let mk_proof (bag : NCic.term Terms.bag) mp steps = let module Subst = FoSubst in let position i l = let rec aux = function @@ -167,10 +176,15 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t)) t vl in - let rec aux seen = function + let close_with_forall vl t = + List.fold_left + (fun t i -> + NCic.Prod ("x"^string_of_int i, NCic.Implicit `Type, t)) + t vl + in + let rec aux ongoal seen = function | [] -> NCic.Rel 1 | id :: tl -> -(* prerr_endline ("Let4 : " ^string_of_int id); *) let amount = List.length seen in let _, lit, vl, proof = Terms.M.find id bag in let lit = @@ -179,34 +193,61 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct | Terms.Equation (l,r,ty,_) -> Terms.Node [ Terms.Leaf eqP; ty; l; r] in -(* prerr_endline ("X" ^ ppfot lit); *) + if not ongoal && id = mp then + (assert (vl = []); + NCic.LetIn ("clause_" ^ string_of_int id, + extract amount vl 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=[] -> aux ongoal seen tl + | Terms.Step _ when tl=[] -> assert false | Terms.Exact ft -> - NCic.LetIn ("clause_" ^ string_of_int id, NCic.Implicit `Type, + NCic.LetIn ("clause_" ^ string_of_int id, + close_with_forall vl (extract amount vl lit), close_with_lambdas vl (extract amount vl ft), - aux ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) + aux ongoal + ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) | Terms.Step (_, id1, id2, dir, pos, subst) -> + let id, id1 = if ongoal then id1,id else id,id1 in let proof_of_id id = - let vars = vars_of id seen in + 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 NCic.Appl (NCic.Rel (List.length vl + position id seen) :: args) in let p_id1 = proof_of_id id1 in let p_id2 = proof_of_id id2 in - let pred = + let pred, hole_type, l, r = let id1_ty = ty_of id1 seen in - mk_predicate amount (Subst.apply_subst subst id1_ty) pos vl + 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 + 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 eq_ind = if dir=Terms.Left2Right then eq_ind else eq_ind_r in - NCic.LetIn ("clause_" ^ string_of_int id, NCic.Implicit `Type, + NCic.LetIn ("clause_" ^ string_of_int id, + close_with_forall vl (extract amount vl lit), close_with_lambdas vl - (NCic.Appl [ eq_ind ; NCic.Implicit `Type; - pred; NCic.Implicit `Term; p_id1; - NCic.Implicit `Term; p_id2 ]), - aux ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) + (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 [] steps + aux false [] steps ;; end diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 8903ec02f..f0cd03758 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -165,27 +165,42 @@ let nparamod rdb metasenv subst context t table = Set.Make(struct type t=int let compare=Pervasives.compare end) in let all id = - let rec traverse acc i = + let rec traverse ongoal (accg,acce) i = match Terms.M.find i bag with - | (_,_,_,Terms.Exact _) -> acc + | (_,_,_,Terms.Exact _) -> accg, acce | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) -> - traverse (traverse (C.add i1 (C.add i2 acc)) i1) i2 + let accg, acce = + if ongoal then C.add i1 accg, acce + else accg, C.add i1 acce + in + let acce = C.add i2 acce in + traverse false (traverse ongoal (accg,acce) i1) i2 in - C.elements (traverse C.empty id) + traverse true (C.empty,C.empty) id in - S.topological_sort (all i) all + let esteps = + S.topological_sort (C.elements (snd (all i))) + (fun i -> C.elements (snd (all i))) + in + let gsteps = + S.topological_sort (C.elements (fst (all i))) + (fun i -> C.elements (fst (all i))) + in + let gsteps = List.rev gsteps in + esteps@gsteps in prerr_endline "YES!"; prerr_endline "Proof:"; List.iter (fun x -> prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l; - let proofterm = B.mk_proof bag l in + let proofterm = B.mk_proof bag i l in prerr_endline (NCicPp.ppterm ~metasenv:C.metasenv ~subst:C.subst ~context:C.context proofterm); let _metasenv, _subst, _proofterm, _prooftype = NCicRefiner.typeof rdb C.metasenv C.subst C.context proofterm None in + prerr_endline "REFINED!"; () | Failure _ -> prerr_endline "FAILURE"; ;; diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index 46f83544f..0118df7c1 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -67,6 +67,6 @@ module type Blob = val pp : t -> string val embed : t -> t foterm val saturate : t -> t -> t foterm * t foterm - val mk_proof : t bag -> int list -> t + val mk_proof : t bag -> int -> int list -> t end diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index bab1a78d0..f1eacb734 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -75,7 +75,7 @@ module type Blob = (* saturate [proof] [type] -> [proof] * [type] *) val saturate : t -> t -> t foterm * t foterm - val mk_proof : t bag -> int list -> t + val mk_proof : t bag -> int -> int list -> t end