X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=b10dc818e80af3921c0385e4fac8ea38cef5cd20;hb=f340ae8d0be1c480c6a496a11157a6ccfb367c13;hp=c31538bda7595dd0b223311d8ee2bc7049dfd262;hpb=356f9fafa095801f1be70ff495f0977ce96ed6bc;p=helm.git diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index c31538bda..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) @@ -398,7 +401,7 @@ let contextualize_rewrites t ty = contextualize eq ty l r t ;; -let build_proof_step lift subst p1 p2 pos l r pred = +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 @@ -415,15 +418,30 @@ let build_proof_step lift 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 parametrize_proof p ty = - let parameters = CicUtil.metas_of_term p in (* ?if they are under a lambda? *) +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 @@ -434,7 +452,9 @@ let parametrize_proof p ty = let p = CicSubstitution.lift (lift_no-1) p in let p = ProofEngineReduction.replace_lifting - ~equality:(=) ~what ~with_what ~where:p + ~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 @@ -456,7 +476,7 @@ let parametrize_proof p ty = 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 @@ -468,56 +488,78 @@ 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 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 _ -> () + | Exact _ -> true | _ -> - try let (pos,no) = Hashtbl.find h i in Hashtbl.replace h i (pos,no+1) - with Not_found -> Hashtbl.add h i (n,1) + 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),_)) -> - add i1 n;add i2 n; - max (aux (n+1) (let p,_,_ = proof_of_id i1 in p)) - (aux (n+1) (let p,_,_ = proof_of_id i2 in p)) + 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)) + (fun acc (_,_,id,_,_) -> aux acc (let p,_,_ = proof_of_id id in p)) i ol in (* now h is complete *) @@ -537,12 +579,14 @@ let build_proof_term h lift proof = let rec aux = function | Exact term -> CicSubstitution.lift lift term | Step (subst,(_, id1, (pos,id2), pred)) -> - if Subst.is_in_subst 9 subst then - prerr_endline (Printf.sprintf "ID %d-%d has: %s\n" id1 id2 (Subst.ppsubst - subst)); let p1,_,_ = proof_of_id aux id1 in let p2,l,r = proof_of_id aux id2 in - build_proof_step lift subst p1 p2 pos l r pred + 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 aux proof ;; @@ -557,10 +601,10 @@ let build_goal_proof l initial ty se = let lets,_,h = List.fold_left (fun (acc,n,h) id -> - let p,_,_ = proof_of_id id in + 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 (CicSubstitution.lift n mty) + 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) @@ -569,12 +613,24 @@ let build_goal_proof l initial ty se = let proof,se = let rec aux se current_proof = function | [] -> current_proof,se - | (pos,id,subst,pred)::tl -> - let p,l,r = proof_of_id id in + | (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 letsno subst current_proof p pos l r pred + 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, @@ -592,7 +648,7 @@ let build_goal_proof l initial ty se = cic, p)) lets (letsno-1,initial) in - canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), se + (*canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty))*)proof, se ;; let refl_proof ty term = @@ -607,26 +663,29 @@ let metas_of_proof p = 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 - 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 @@ -636,8 +695,8 @@ let fix_metas newmeta eq = 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 - newmeta+1, eq + let eq' = mk_equality (w, p, (ty, left, right, o), metasenv) in + newmeta+1, eq' exception NotMetaConvertible;;