From: Enrico Tassi Date: Tue, 16 Jun 2009 23:07:35 +0000 (+0000) Subject: first proof reconstruction attempt, still bugged since it X-Git-Tag: make_still_working~3858 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8de1a75899a83dd31e856804bd448c1bd87d9ab3;p=helm.git first proof reconstruction attempt, still bugged since it does all steps in a forward fashion --- diff --git a/helm/software/components/ng_paramodulation/cicBlob.ml b/helm/software/components/ng_paramodulation/cicBlob.ml index 88ec26c2e..888e6c001 100644 --- a/helm/software/components/ng_paramodulation/cicBlob.ml +++ b/helm/software/components/ng_paramodulation/cicBlob.ml @@ -37,5 +37,7 @@ module CicBlob(C : CicContext) : Terms.Blob with type t = Cic.term = struct let eqP = assert false;; let saturate = assert false;; + + let mk_proof = assert false;; end diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml index 9053ec223..6154306b5 100644 --- a/helm/software/components/ng_paramodulation/foSubst.ml +++ b/helm/software/components/ng_paramodulation/foSubst.ml @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module Subst (B : Terms.Blob) = struct +(* module Subst (B : Terms.Blob) = struct *) let id_subst = [];; @@ -48,4 +48,4 @@ module Subst (B : Terms.Blob) = struct let concat x y = x @ y;; -end +(* end *) diff --git a/helm/software/components/ng_paramodulation/foSubst.mli b/helm/software/components/ng_paramodulation/foSubst.mli index 74845d28a..441e35581 100644 --- a/helm/software/components/ng_paramodulation/foSubst.mli +++ b/helm/software/components/ng_paramodulation/foSubst.mli @@ -11,18 +11,20 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) +(* module Subst (B : Terms.Blob) : sig - val id_subst : B.t Terms.substitution +*) + val id_subst : 'a Terms.substitution val build_subst : - int -> B.t Terms.foterm -> B.t Terms.substitution -> - B.t Terms.substitution + int -> 'a Terms.foterm -> 'a Terms.substitution -> + 'a Terms.substitution val lookup_subst : - int -> B.t Terms.substitution -> B.t Terms.foterm - val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist + int -> 'a Terms.substitution -> 'a Terms.foterm + val filter : 'a Terms.substitution -> Terms.varlist -> Terms.varlist val apply_subst : - B.t Terms.substitution -> B.t Terms.foterm -> B.t Terms.foterm + 'a Terms.substitution -> 'a Terms.foterm -> 'a Terms.foterm val concat: - B.t Terms.substitution -> B.t Terms.substitution -> - B.t Terms.substitution - end + 'a Terms.substitution -> 'a Terms.substitution -> + 'a Terms.substitution +(* end *) diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml index fae6e0840..6eb014062 100644 --- a/helm/software/components/ng_paramodulation/foUnif.ml +++ b/helm/software/components/ng_paramodulation/foUnif.ml @@ -14,7 +14,7 @@ exception UnificationFailure of string Lazy.t;; module Founif (B : Terms.Blob) = struct - module Subst = FoSubst.Subst(B) + module Subst = FoSubst (*.Subst(B)*) module U = FoUtils.Utils(B) let unification vars locked_vars t1 t2 = diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index ec76511d9..f56cccd89 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -27,7 +27,7 @@ let mk_id = ;; module Utils (B : Terms.Blob) = struct - module Subst = FoSubst.Subst(B) ;; + module Subst = FoSubst;; (*.Subst(B) ;;*) module Order = Orderings.Orderings(B) ;; let rec eq_foterm x y = diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index 09399b326..5aded5329 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -84,5 +84,129 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct NCic.Const r ;; + let eq_ind = + let r = + OCic2NCic.reference_of_oxuri + (UriManager.uri_of_string + "cic:/matita/logic/equality/eq_ind.con") + in + NCic.Const r + ;; + + let eq_ind_r = + let r = + OCic2NCic.reference_of_oxuri + (UriManager.uri_of_string + "cic:/matita/logic/equality/eq_elim_r.con") + in + NCic.Const r + ;; + + let extract lift vl t = + let rec pos i = function + | [] -> raise Not_found + | j :: tl when j <> i -> 1+ pos i tl + | _ -> 1 + in + let vl_len = List.length vl in + let rec extract = function + | Terms.Leaf x -> NCicSubstitution.lift (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) + in + extract t + ;; + + let rec ppfot = function + | Terms.Leaf _ -> "." + | Terms.Var i -> "?" ^ string_of_int i + | Terms.Node l -> "(" ^ String.concat " " (List.map ppfot l) ^ ")" + ;; + + let mk_predicate amount ft p vl = + let rec aux t p = + match p with + | [] -> NCic.Rel 1 + | n::tl -> + match t with + | Terms.Leaf _ + | Terms.Var _ -> + prerr_endline ("term: " ^ ppfot ft); + prerr_endline ("path: " ^ String.concat "," + (List.map string_of_int p)); + assert false + | Terms.Node l -> + let l = + HExtlib.list_mapi + (fun t i -> + if i = n then aux t tl + else extract amount (0::vl) t) + l + in + NCic.Appl l + in + NCic.Lambda("x", NCic.Implicit `Type, aux ft (List.rev p)) + ;; + + let mk_proof (bag : NCic.term Terms.bag) steps = + let module Subst = FoSubst in + let position i l = + let rec aux = function + | [] -> assert false + | (j,_) :: tl when i = j -> 1 + | _ :: tl -> 1 + aux tl + in + aux l + in + let vars_of i l = fst (List.assoc i l) in + let ty_of i l = snd (List.assoc i l) in + let close_with_lambdas vl t = + List.fold_left + (fun t i -> + NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t)) + t vl + in + let rec aux 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 = + match lit with + | Terms.Predicate t -> assert false + | Terms.Equation (l,r,ty,_) -> + Terms.Node [ Terms.Leaf eqP; ty; l; r] + in +(* prerr_endline ("X" ^ ppfot lit); *) + match proof with + | Terms.Exact ft -> + NCic.LetIn ("clause_" ^ string_of_int id, NCic.Implicit `Type, + close_with_lambdas vl (extract amount vl ft), + aux ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) + | Terms.Step (_, id1, id2, dir, pos, subst) -> + let proof_of_id id = + let vars = 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 id1_ty = ty_of id1 seen in + mk_predicate amount (Subst.apply_subst subst id1_ty) pos vl + 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, + 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) + in + aux [] steps + ;; end diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index b301e8005..36adca454 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -2,7 +2,7 @@ let debug s = () (* prerr_endline s *) ;; -let nparamod metasenv subst context t table = +let nparamod rdb metasenv subst context t table = let nb_iter = ref 100 in prerr_endline "========================================"; let module C = struct @@ -148,9 +148,37 @@ let nparamod metasenv subst context t table = in let actives = [], IDX.DT.empty in try given_clause bag maxvar actives passives g_actives g_passives - with Sup.Success (bag, _, mp) -> - prerr_endline "YES!"; - prerr_endline "Meeting point :"; prerr_endline (Pp.pp_unit_clause mp) - (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag) *) - | Failure _ -> prerr_endline "FAILURE" + with + | Sup.Success (bag, _, (i,_,_,_)) -> + let l = + let module S = + HTopoSort.Make(struct type t=int let compare=Pervasives.compare end) + in + let module C : Set.S with type elt = int = + Set.Make(struct type t=int let compare=Pervasives.compare end) + in + let all id = + let rec traverse acc i = + match Terms.M.find i bag with + | (_,_,_,Terms.Exact _) -> acc + | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) -> + traverse (traverse (C.add i1 (C.add i2 acc)) i1) i2 + in + C.elements (traverse C.empty id) + in + S.topological_sort (all i) all + 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 + 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 + () + | Failure _ -> prerr_endline "FAILURE"; ;; diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index 5ba90f943..dd866f8db 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -1,4 +1,5 @@ val nparamod : + NRstatus.refiner_status -> NCic.metasenv -> NCic.substitution -> NCic.context -> (NCic.term * NCic.term) -> (NCic.term * NCic.term) list -> unit diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index b90c08d38..29f257697 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -86,18 +86,18 @@ let string_of_comparison = function let pp_unit_clause ~formatter:f c = let (id, l, vars, proof) = c in - Format.fprintf f "Id : %d, " id ; + Format.fprintf f "Id : %3d, " id ; match l with | Terms.Predicate t -> pp_foterm f t | Terms.Equation (lhs, rhs, ty, comp) -> - Format.fprintf f "{"; + Format.fprintf f "@[{"; pp_foterm f ty; - Format.fprintf f "}: "; + Format.fprintf f "}:@;@["; pp_foterm f lhs; - Format.fprintf f " %s " (string_of_comparison comp); + Format.fprintf f "@;%s@;" (string_of_comparison comp); pp_foterm f rhs; - Format.fprintf f " [%s] by %s" + Format.fprintf f "@]@;[%s] by %s@]" (String.concat ", " (List.map string_of_int vars)) (match proof with | Terms.Exact _ -> "axiom" diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 046799a77..2198ec8bd 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -15,7 +15,7 @@ module Superposition (B : Terms.Blob) = struct module IDX = Index.Index(B) module Unif = FoUnif.Founif(B) - module Subst = FoSubst.Subst(B) + module Subst = FoSubst (*.Subst(B)*) module Order = Orderings.Orderings(B) module Utils = FoUtils.Utils(B) module Pp = Pp.Pp(B) diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index bcc3bcf7b..46f83544f 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -67,5 +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 end diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index 7b3cb1750..bab1a78d0 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -74,5 +74,8 @@ module type Blob = val embed : t -> t foterm (* saturate [proof] [type] -> [proof] * [type] *) val saturate : t -> t -> t foterm * t foterm + + val mk_proof : t bag -> int list -> t + end diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 147df78f8..b6b933211 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -568,7 +568,8 @@ let auto ~params:(l,_) status goal = (status, (t,ty) :: l)) (status,[]) l in - Paramod.nparamod metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l; + let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in + Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l; status ;;