X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=1bc87f8c54fd6e235b903a405e6422b7486ba62e;hb=b36c499a9234a3dc0abd5fb8d418975966f179e7;hp=65593985108f1e42d177074fb2c70957fe9cf6f1;hpb=59895ae358dff2a57a9fd1ea6924690a0862e036;p=helm.git diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 655939851..1bc87f8c5 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -96,8 +96,8 @@ let string_of_equality ?env eq = 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)) *) - "..." + (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), m , id = open_equality eq in @@ -105,8 +105,8 @@ let string_of_equality ?env eq = 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)) *) - "..." + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) +(* "..." *) ;; let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) = @@ -202,7 +202,7 @@ let build_ens uri termlist = let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match obj with | Cic.Constant (_, _, _, uris, _) -> - assert (List.length uris <= List.length termlist); + (* assert (List.length uris <= List.length termlist); *) let rec aux = function | [], tl -> [], tl | (uri::uris), (term::tl) -> @@ -269,6 +269,48 @@ let is_not_fixed t = ;; let canonical t context menv = + let remove_cycles t = + let is_transitive = + function + Cic.Appl (Cic.Const (uri_trans,_)::_) + when LibraryObjects.is_trans_eq_URI uri_trans -> + true + | _ -> false in + let rec collect = + function + Cic.Appl (Cic.Const (uri_trans,ens)::tl) + when LibraryObjects.is_trans_eq_URI uri_trans -> + let ty,l,m,r,p1,p2 = open_trans ens tl in + (if is_transitive p1 then fst (collect p1) else [l,p1]) @ + (if is_transitive p2 then fst (collect p2) else [m,p2]), + (r, uri_trans, ty) + | t -> assert false in + let rec cut_to_last_duplicate l acc = + function + [] -> List.rev acc + | (l',p)::tl when l=l' -> +if acc <> [] then +prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI"); + cut_to_last_duplicate l [l',p] tl + | (l',p)::tl -> + cut_to_last_duplicate l ((l',p)::acc) tl + in + let rec rebuild = + function + (l,_)::_::_ as steps, ((r,uri_trans,ty) as last) -> + (match cut_to_last_duplicate l [] steps with + (l,p1)::((m,_)::_::_ as tl) -> + mk_trans uri_trans ty l m r p1 (rebuild (tl,last)) + | [l,p1 ; m,p2] -> mk_trans uri_trans ty l m r p1 p2 + | [l,p1] -> p1 + | [] -> assert false) + | _ -> assert false + in + if is_transitive t then + rebuild (collect t) + else + t + in let rec remove_refl t = match t with | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args) @@ -285,11 +327,18 @@ let canonical t context menv = Cic.LetIn (name,remove_refl bo,remove_refl rest) | _ -> t in - let rec canonical context t = + let rec canonical_trough_lambda context = function + | Cic.Lambda(name,ty,bo) -> + let context' = (Some (name,Cic.Decl ty))::context in + Cic.Lambda(name,ty,canonical_trough_lambda context' bo) + | t -> canonical context t + + and canonical context t = match t with | Cic.LetIn(name,bo,rest) -> + let bo = canonical_trough_lambda context bo in let context' = (Some (name,Cic.Def (bo,None)))::context in - Cic.LetIn(name,canonical context bo,canonical context' rest) + Cic.LetIn(name,bo,canonical context' 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 @@ -302,19 +351,22 @@ let canonical t context menv = mk_trans uri_trans ty r m l (canonical context (mk_sym uri_sym ty m r p2)) (canonical context (mk_sym uri_sym ty l m p1)) - | Cic.Appl (([Cic.Const(uri_feq,ens);ty1;ty2;f;x;y;p])) -> + | Cic.Appl (([Cic.Const(uri_feq,ens);ty1;ty2;f;x;y;p])) + when LibraryObjects.is_eq_f_URI uri_feq -> let eq = LibraryObjects.eq_URI_of_eq_f_URI uri_feq in let eq_f_sym = Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, []) in - Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p])) + let rc = Cic.Appl [eq_f_sym;ty1;ty2;f;x;y;p] in + prerr_endline ("CANONICAL " ^ CicPp.ppterm rc); + rc | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t when LibraryObjects.is_eq_URI uri -> t | _ -> Cic.Appl (List.map (canonical context) args)) | Cic.Appl l -> Cic.Appl (List.map (canonical context) l) | _ -> t in - remove_refl (canonical context t) + remove_cycles (remove_refl (canonical context t)) ;; let compose_contexts ctx1 ctx2 = @@ -372,7 +424,8 @@ let contextualize uri ty left right t = * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context * ctx_ty is the type of ctx *) - let rec aux uri ty left right ctx_d ctx_ty = function + let rec aux uri ty left right ctx_d ctx_ty t = + match t with | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) when LibraryObjects.is_sym_eq_URI uri_sym -> let ty,l,r,p = open_sym ens tl in @@ -407,8 +460,8 @@ let contextualize uri ty left right t = let c_what = put_in_ctx ctx_c what in (* now put the proofs in the compound context *) let p1 = (* p1: dc_what = d_m *) - if is_not_fixed_lp then - aux uri ty2 c_what m ctx_d ctx_ty p1 + if is_not_fixed_lp then + aux uri ty2 c_what m ctx_d ctx_ty p1 else mk_sym uri_sym ctx_ty d_m dc_what (aux uri ty2 m c_what ctx_d ctx_ty p1) @@ -417,7 +470,7 @@ let contextualize uri ty left right t = if avoid_eq_ind then mk_sym uri_sym ctx_ty dc_what dc_other (aux uri ty1 what other ctx_dc ctx_ty p2) - else + else aux uri ty1 other what ctx_dc ctx_ty p2 in (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m @@ -496,8 +549,8 @@ let build_proof_step eq lift subst p1 p2 pos l r pred = p ;; -let parametrize_proof p l r ty = - let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in +let parametrize_proof p l r = + let uniq l = HExtlib.list_uniq (List.sort (fun (i,_) (j,_) -> Pervasives.compare i j) l) in let mot = CicUtil.metas_of_term_set in let parameters = uniq (mot p @ mot l @ mot r) in (* ?if they are under a lambda? *) @@ -506,6 +559,21 @@ let parametrize_proof p l r ty = HExtlib.list_uniq (List.sort Pervasives.compare parameters) in *) + (* resorts l such that *hopefully* dependencies can be inferred *) + let guess_dependency p l = + match p with + | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) + when LibraryObjects.is_eq_ind_URI uri_ind || + LibraryObjects.is_eq_ind_r_URI uri_ind -> + let ty,_,_,_,_,_ = open_eq_ind tl in + let metas = CicUtil.metas_of_term ty in + let nondep, dep = + List.partition (fun (i,_) -> List.exists (fun (j,_) -> j=i) metas) l + in + nondep@dep + | _ -> l + in + let parameters = guess_dependency p parameters in 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) @@ -517,10 +585,7 @@ let parametrize_proof p l r ty = 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 ty_of_m _ = Cic.Implicit (Some `Type) in let args, proof,_ = List.fold_left (fun (instance,p,n) m -> @@ -558,19 +623,19 @@ let wfo bag goalproof proof id = let string_of_id (id_to_eq,_) names id = if id = 0 then "" else try - let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in + let (_,p,(t,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in match p with | Exact t -> 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 [%s]" id +(* "..." *) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) + | Step (_,(step,id1, (dir,id2), p) ) -> + Printf.sprintf "%6d: %s %6d %6d %s =(%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)) *) - "..." + id1 id2 (CicPp.pp l names) (CicPp.pp t names) (CicPp.pp r names) + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) + (*"..."*) with Not_found -> assert false @@ -721,7 +786,6 @@ let build_goal_proof bag eq l initial ty se context menv = let se = List.map (fun i -> Cic.Meta (i,[])) se in let lets = get_duplicate_step_in_wfo bag 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 @@ -729,7 +793,7 @@ let build_goal_proof bag eq l initial ty se context menv = let p,l,r = proof_of_id bag id in let cic = build_proof_term bag eq h n p in let real_cic,instance = - parametrize_proof cic l r (CicSubstitution.lift n mty) + parametrize_proof cic l r in let h = (id, instance)::lift_list h in acc@[id,real_cic],n+1,h) @@ -839,7 +903,8 @@ let fix_metas bag newmeta eq = (* List.map (fun i ,_,_ -> i) menv *) HExtlib.list_uniq (List.sort Pervasives.compare - (Utils.metas_of_term left @ Utils.metas_of_term right)) + (Utils.metas_of_term left @ Utils.metas_of_term right @ + Utils.metas_of_term ty)) in let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in let ty = Subst.apply_subst subst ty in @@ -1003,7 +1068,9 @@ let is_weak_identity eq = let is_identity (_, context, ugraph) eq = let _,_,(ty,left,right,_),menv,_ = open_equality eq in (* doing metaconv here is meaningless *) - fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph) + left = right +(* fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph) + * *) ;;