X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=b10dc818e80af3921c0385e4fac8ea38cef5cd20;hb=f340ae8d0be1c480c6a496a11157a6ccfb367c13;hp=b6c3dc66a6625ec2e2ba92043e5108d6375f501d;hpb=2d242b51687938075e568d360b93f83a4b0a1ce9;p=helm.git diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index b6c3dc66a..b10dc818e 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -41,7 +41,7 @@ and proof = | Exact of Cic.term | Step of Subst.substitution * (rule * int*(Utils.pos*int)* Cic.term) (* subst, (rule,eq1, eq2,predicate) *) -and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list +and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list ;; (* globals *) @@ -75,21 +75,29 @@ let mk_tmp_equality (weight,(ty,l,r,o),m) = let open_equality (_,weight,proof,(ty,l,r,o),m,id) = (weight,proof,(ty,l,r,o),m,id) +let string_of_rule = function + | SuperpositionRight -> "SupR" + | SuperpositionLeft -> "SupL" + | Demodulation -> "Demod" +;; + let string_of_equality ?env eq = match env with | None -> - let w, _, (ty, left, right, o), _ , id = open_equality eq in - Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" + let w, _, (ty, left, right, o), m , id = open_equality eq in + Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]" id w (CicPp.ppterm ty) (CicPp.ppterm left) (Utils.string_of_comparison o) (CicPp.ppterm right) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) | Some (_, context, _) -> let names = Utils.names_of_context context in - let w, _, (ty, left, right, o), _ , id = open_equality eq in - Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" + let w, _, (ty, left, right, o), m , id = open_equality eq in + Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]" id w (CicPp.pp ty names) (CicPp.pp left names) (Utils.string_of_comparison o) (CicPp.pp right names) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) ;; let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) = @@ -105,11 +113,6 @@ let proof_of_id id = let string_of_proof ?(names=[]) p gp = - let str_of_rule = function - | SuperpositionRight -> "SupR" - | SuperpositionLeft -> "SupL" - | Demodulation -> "Demod" - in let str_of_pos = function | Utils.Left -> "left" | Utils.Right -> "right" @@ -122,7 +125,7 @@ let string_of_proof ?(names=[]) p gp = prefix (CicPp.pp t names) | Step (subst,(rule,eq1,(pos,eq2),pred)) -> Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n" - prefix (str_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) + prefix (string_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) (CicPp.pp pred names)^ aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) @@ -130,9 +133,9 @@ let string_of_proof ?(names=[]) p gp = aux 0 "" p ^ String.concat "\n" (List.map - (fun (pos,i,s,t) -> + (fun (r,pos,i,s,t) -> (Printf.sprintf - "GOAL: %s %d %s %s\n" + "GOAL: %s %s %d %s %s\n" (string_of_rule r) (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^ aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i))) gp) @@ -228,10 +231,13 @@ let canonical t = remove_refl p1 | _ -> Cic.Appl (List.map remove_refl args)) | Cic.Appl l -> Cic.Appl (List.map remove_refl l) + | Cic.LetIn (name,bo,rest) -> + Cic.LetIn (name,remove_refl bo,remove_refl rest) | _ -> t in let rec canonical t = match t with + | Cic.LetIn(name,bo,rest) -> Cic.LetIn(name,canonical bo,canonical rest) | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args) when LibraryObjects.is_sym_eq_URI uri_sym -> (match p_of_sym ens tl with @@ -315,6 +321,9 @@ let contextualize uri ty left right t = * ctx is a term with an open (Rel 1). (Rel 1) is the empty context *) let rec aux uri ty left right ctx_d = function + | Cic.LetIn (name,body,rest) -> + (* we should go in body *) + Cic.LetIn (name,body,aux uri ty left right ctx_d rest) | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) when LibraryObjects.is_eq_ind_URI uri_ind || LibraryObjects.is_eq_ind_r_URI uri_ind -> @@ -392,12 +401,15 @@ let contextualize_rewrites t ty = contextualize eq ty l r t ;; -let build_proof_step subst p1 p2 pos l r pred = - let p1 = Subst.apply_subst subst p1 in - let p2 = Subst.apply_subst subst p2 in - let l = Subst.apply_subst subst l in - let r = Subst.apply_subst subst r in - let pred = Subst.apply_subst subst pred in +let build_proof_step ?(sym=false) lift subst p1 p2 pos l r pred = + let p1 = Subst.apply_subst_lift lift subst p1 in + let p2 = Subst.apply_subst_lift lift subst p2 in + let l = CicSubstitution.lift lift l in + let l = Subst.apply_subst_lift lift subst l in + let r = CicSubstitution.lift lift r in + let r = Subst.apply_subst_lift lift subst r in + let pred = CicSubstitution.lift lift pred in + let pred = Subst.apply_subst_lift lift subst pred in let ty,body = match pred with | Cic.Lambda (_,ty,body) -> ty,body @@ -406,27 +418,65 @@ let build_proof_step subst p1 p2 pos l r pred = let what, other = if pos = Utils.Left then l,r else r,l in + let p = match pos with | Utils.Left -> mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2 | Utils.Right -> mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2 + in + if sym then + let uri,pl,pr = + let eq,_,pl,pr = open_eq body in + LibraryObjects.sym_eq_URI ~eq, pl, pr + in + let l = CicSubstitution.subst other pl in + let r = CicSubstitution.subst other pr in + mk_sym uri ty l r p + else + p ;; -let build_proof_term proof = - let rec aux = function - | Exact term -> term - | Step (subst,(_, id1, (pos,id2), pred)) -> - let p,_,_ = proof_of_id id1 in - let p1 = aux p in - let p,l,r = proof_of_id id2 in - let p2 = aux p in - build_proof_step subst p1 p2 pos l r pred +let parametrize_proof p l r ty = + let parameters = CicUtil.metas_of_term p +@ CicUtil.metas_of_term l +@ CicUtil.metas_of_term r +in (* ?if they are under a lambda? *) + let parameters = + HExtlib.list_uniq (List.sort Pervasives.compare parameters) in - aux proof + let what = List.map (fun (i,l) -> Cic.Meta (i,l)) parameters in + let with_what, lift_no = + List.fold_right (fun _ (acc,n) -> ((Cic.Rel n)::acc),n+1) what ([],1) + in + let p = CicSubstitution.lift (lift_no-1) p in + let p = + ProofEngineReduction.replace_lifting + ~equality:(fun t1 t2 -> + match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) + ~what ~with_what ~where:p + in + let ty_of_m _ = ty (*function + | Cic.Meta (i,_) -> List.assoc i menv + | _ -> assert false *) + in + let args, proof,_ = + List.fold_left + (fun (instance,p,n) m -> + (instance@[m], + Cic.Lambda + (Cic.Name ("x"^string_of_int n), + CicSubstitution.lift (lift_no - n - 1) (ty_of_m m), + p), + n+1)) + ([Cic.Rel 1],p,1) + what + in + let instance = match args with | [x] -> x | _ -> Cic.Appl args in + proof, instance ;; -let wfo goalproof proof = +let wfo goalproof proof id = let rec aux acc id = let p,_,_ = proof_of_id id in match p with @@ -438,45 +488,167 @@ let wfo goalproof proof = in let acc = match proof with - | Exact _ -> [] - | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2 + | Exact _ -> [id] + | Step (_,(_,id1, (_,id2), _)) -> aux (aux [id] id1) id2 in - List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof + List.fold_left (fun acc (_,_,id,_,_) -> aux acc id) acc goalproof ;; let string_of_id names id = + if id = 0 then "" else try - let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in match p with | Exact t -> - Printf.sprintf "%d = %s: %s = %s" id + Printf.sprintf "%d = %s: %s = %s [%s]" id (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) | Step (_,(step,id1, (_,id2), _) ) -> - Printf.sprintf "%6d: %s %6d %6d %s = %s" id - (if step = SuperpositionRight then "SupR" else "Demo") + Printf.sprintf "%6d: %s %6d %6d %s = %s [%s]" id + (string_of_rule step) id1 id2 (CicPp.pp l names) (CicPp.pp r names) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) with Not_found -> assert false -let pp_proof names goalproof proof = - String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^ - "\ngoal is demodulated with " ^ - (String.concat " " - ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof))) -;; - -let build_goal_proof l initial ty = - let proof = - List.fold_left - (fun current_proof (pos,id,subst,pred) -> - let p,l,r = proof_of_id id in - let p = build_proof_term p in - let pos = if pos = Utils.Left then Utils.Right else Utils.Left in - build_proof_step subst current_proof p pos l r pred) - initial l +let pp_proof names goalproof proof subst id initial_goal = + prerr_endline ("AAAAA" ^ string_of_int id); + prerr_endline (String.concat "+" (List.map string_of_int (wfo goalproof proof + id))); + String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof id)) ^ + "\ngoal:\n " ^ + (String.concat "\n " + (fst (List.fold_right + (fun (r,pos,i,s,pred) (acc,g) -> + let _,_,left,right = open_eq g in + let ty = + match pos with + | Utils.Left -> CicReduction.head_beta_reduce (Cic.Appl[pred;right]) + | Utils.Right -> CicReduction.head_beta_reduce (Cic.Appl[pred;left]) + in + let ty = Subst.apply_subst s ty in + ("("^ string_of_rule r ^ " " ^ string_of_int i^") -> " + ^ CicPp.pp ty names) :: acc,ty) goalproof ([],initial_goal)))) ^ + "\nand then subsumed by " ^ string_of_int id ^ " when " ^ Subst.ppsubst subst +;; + +(* returns the list of ids that should be factorized *) +let get_duplicate_step_in_wfo l p = + let ol = List.rev l in + let h = Hashtbl.create 13 in + (* NOTE: here the n parameter is an approximation of the dependency + between equations. To do things seriously we should maintain a + dependency graph. This approximation is not perfect. *) + let add i n = + let p,_,_ = proof_of_id i in + match p with + | Exact _ -> true + | _ -> + try let (pos,no) = Hashtbl.find h i in Hashtbl.replace h i (pos,no+1);false + with Not_found -> Hashtbl.add h i (n,1);true + in + let rec aux n = function + | Exact _ -> n + | Step (_,(_,i1,(_,i2),_)) -> + let go_on_1 = add i1 n in + let go_on_2 = add i2 n in + max + (if go_on_1 then aux (n+1) (let p,_,_ = proof_of_id i1 in p) else n+1) + (if go_on_2 then aux (n+1) (let p,_,_ = proof_of_id i2 in p) else n+1) + in + let i = aux 0 p in + let _ = + List.fold_left + (fun acc (_,_,id,_,_) -> aux acc (let p,_,_ = proof_of_id id in p)) + i ol + in + (* now h is complete *) + let proofs = Hashtbl.fold (fun k (pos,count) acc->(k,pos,count)::acc) h [] in + let proofs = List.filter (fun (_,_,c) -> c > 1) proofs in + let proofs = + List.sort (fun (_,c1,_) (_,c2,_) -> Pervasives.compare c2 c1) proofs + in + List.map (fun (i,_,_) -> i) proofs +;; + +let build_proof_term h lift proof = + let proof_of_id aux id = + let p,l,r = proof_of_id id in + try List.assoc id h,l,r with Not_found -> aux p, l, r + in + let rec aux = function + | Exact term -> CicSubstitution.lift lift term + | Step (subst,(_, id1, (pos,id2), pred)) -> + let p1,_,_ = proof_of_id aux id1 in + let p2,l,r = proof_of_id aux id2 in + let p = build_proof_step lift subst p1 p2 pos l r pred in +(* let cond = (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in + if not cond then + prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2); + assert cond;*) + p in - proof - (*canonical (contextualize_rewrites proof ty)*) + aux proof +;; + +let build_goal_proof l initial ty se = + let se = List.map (fun i -> Cic.Meta (i,[])) se in + let lets = get_duplicate_step_in_wfo l initial in + let letsno = List.length lets in + let _,mty,_,_ = open_eq ty in + let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l + in + let lets,_,h = + List.fold_left + (fun (acc,n,h) id -> + let p,l,r = proof_of_id id in + let cic = build_proof_term h n p in + let real_cic,instance = + parametrize_proof cic l r (CicSubstitution.lift n mty) + in + let h = (id, instance)::lift_list h in + acc@[id,real_cic],n+1,h) + ([],0,[]) lets + in + let proof,se = + let rec aux se current_proof = function + | [] -> current_proof,se + | (rule,pos,id,subst,pred)::tl -> + let p,l,r = proof_of_id id in + let p = build_proof_term h letsno p in + let pos = if pos = Utils.Left then Utils.Right else Utils.Left in + let sym,pred = + match rule with + | SuperpositionLeft when pos = Utils.Left -> + let pred = + match pred with + | Cic.Lambda (name,ty,Cic.Appl[eq;ty1;l;r]) -> + Cic.Lambda (name,ty,Cic.Appl[eq;ty1;r;l]) + | _ -> assert false + in + true, pred + | _ -> false,pred + in + let proof = + build_proof_step ~sym letsno subst current_proof p pos l r pred + in + let proof,se = aux se proof tl in + Subst.apply_subst_lift letsno subst proof, + List.map (fun x -> Subst.apply_subst_lift letsno subst x) se + in + aux se (build_proof_term h letsno initial) l + in + let n,proof = + let initial = proof in + List.fold_right + (fun (id,cic) (n,p) -> + n-1, + Cic.LetIn ( + Cic.Name ("H"^string_of_int id), + cic, p)) + lets (letsno-1,initial) + in + (*canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty))*)proof, se ;; let refl_proof ty term = @@ -486,46 +658,45 @@ let refl_proof ty term = ty; term] ;; -let metas_of_proof p = - Utils.metas_of_term (build_proof_term p) +let metas_of_proof p = + let p = build_proof_term [] 0 p in + Utils.metas_of_term p ;; -let relocate newmeta menv = - let subst, metasenv, newmeta = +let relocate newmeta menv to_be_relocated = + let subst, newmetasenv, newmeta = List.fold_right - (fun (i, context, ty) (subst, menv, maxmeta) -> - let irl = [] (* - CicMkImplicit.identity_relocation_list_for_metavariable context *) - in - let newsubst = Subst.buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in - let newmeta = maxmeta, context, ty in - newsubst, newmeta::menv, maxmeta+1) - menv (Subst.empty_subst, [], newmeta+1) + (fun i (subst, metasenv, maxmeta) -> + let _,context,ty = CicUtil.lookup_meta i menv in + let irl = [] in + let newmeta = Cic.Meta(maxmeta,irl) in + let newsubst = Subst.buildsubst i context newmeta ty subst in + newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1) + to_be_relocated (Subst.empty_subst, [], newmeta+1) in - let metasenv = Subst.apply_subst_metasenv subst metasenv in - let subst = Subst.flatten_subst subst in - subst, metasenv, newmeta + let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in + subst, menv, newmeta let fix_metas newmeta eq = let w, p, (ty, left, right, o), menv,_ = open_equality eq in - (* debug - let _ , eq = - fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in - prerr_endline (string_of_equality eq); *) - let subst, metasenv, newmeta = relocate newmeta menv in + let to_be_relocated = + HExtlib.list_uniq + (List.sort Pervasives.compare + (Utils.metas_of_term left @ Utils.metas_of_term right)) + in + let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in let ty = Subst.apply_subst subst ty in let left = Subst.apply_subst subst left in let right = Subst.apply_subst subst right in let fix_proof = function | Exact p -> Exact (Subst.apply_subst subst p) | Step (s,(r,id1,(pos,id2),pred)) -> - Step (Subst.concat_substs s subst,(r,id1,(pos,id2), pred)) + Step (Subst.concat s subst,(r,id1,(pos,id2), pred)) in let p = fix_proof p in - let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in - (* debug prerr_endline (string_of_equality eq); *) - newmeta+1, eq + let eq' = mk_equality (w, p, (ty, left, right, o), metasenv) in + newmeta+1, eq' exception NotMetaConvertible;;