X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=0b0b73e3f27c74ff0d5fefc202d904937726253c;hb=bc76b4d2f3c380894259b45fad52cf85ae6cee18;hp=368a80f5d7f03b8a5242fc828110b85cd2255b3b;hpb=984afddae60275147eac32185e546a7eb943bb6c;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 368a80f5d..0b0b73e3f 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -let _profiler = <:profiler<_profiler>>;; +(* let _profiler = <:profiler<_profiler>>;; *) (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *) @@ -94,7 +94,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 @@ -102,7 +103,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,_,_) = @@ -326,10 +328,9 @@ let canonical t context menv = (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])) -> - - let eq_f_sym = - Cic.Const (UriManager.uri_of_string - "cic:/matita/logic/equality/eq_f1.con",[]) + 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])) @@ -509,9 +510,8 @@ let contextualize uri ty left right t = | t -> (* let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in *) (* let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in *) - let uri_feq = - UriManager.uri_of_string "cic:/matita/logic/equality/eq_f.con" - in + + let uri_feq = LibraryObjects.eq_f_URI ~eq:uri in let pred = (* let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in *) let l = @@ -599,7 +599,7 @@ let parametrize_proof p l r ty = (fun (instance,p,n) m -> (instance@[m], Cic.Lambda - (Cic.Name ("x"^string_of_int n), + (Cic.Name ("X"^string_of_int n), CicSubstitution.lift (lift_no - n - 1) (ty_of_m m), p), n+1)) @@ -636,12 +636,14 @@ let string_of_id names id = | 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)) + "..." +(* (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_of_rule step) id1 id2 (CicPp.pp l names) (CicPp.pp r names) - (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) +(* (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *) + "..." with Not_found -> assert false @@ -1141,7 +1143,7 @@ module IntSet = Set.Make(IntOT);; let n_purged = ref 0;; let collect alive1 alive2 alive3 = - let _ = <:start> in +(* let _ = <:start> in *) let deps_of id = let p,_,_ = proof_of_id id in match p with @@ -1164,14 +1166,87 @@ let collect alive1 alive2 alive3 = in n_purged := !n_purged + List.length to_purge; List.iter (Hashtbl.remove id_to_eq) to_purge; - let _ = <:stop> in () +(* let _ = <:stop> in () *) ;; let id_of e = let _,_,_,_,id = open_equality e in id ;; -let get_stats () = +let get_stats () = "" +(* <:show> ^ "# of purged eq by the collector: " ^ string_of_int !n_purged ^ "\n" +*) +;; + +let rec pp_proofterm name t context = + let rec skip_lambda tys ctx = function + | Cic.Lambda (n,s,t) -> skip_lambda (s::tys) ((Some n)::ctx) t + | t -> ctx,tys,t + in + let rename s name = + match name with + | Cic.Name s1 -> Cic.Name (s ^ s1) + | _ -> assert false + in + let rec skip_letin ctx = function + | Cic.LetIn (n,b,t) -> + pp_proofterm (Some (rename "Lemma " n)) b ctx:: + skip_letin ((Some n)::ctx) t + | t -> + let ppterm t = CicPp.pp t ctx in + let rec pp inner = function + | Cic.Appl [Cic.Const (uri,[]);_;l;m;r;p1;p2] + when Pcre.pmatch ~pat:"trans_eq" (UriManager.string_of_uri uri)-> + if not inner then + (" " ^ ppterm l) :: pp true p1 @ + [ " = " ^ ppterm m ] @ pp true p2 @ + [ " = " ^ ppterm r ] + else + pp true p1 @ + [ " = " ^ ppterm m ] @ pp true p2 + | Cic.Appl [Cic.Const (uri,[]);_;l;m;p] + when Pcre.pmatch ~pat:"sym_eq" (UriManager.string_of_uri uri)-> + pp true p + | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] + when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)-> + pp true p + | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] + when Pcre.pmatch ~pat:"eq_f1" (UriManager.string_of_uri uri)-> + pp true p + | Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p] + when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)-> + [ "witness " ^ ppterm t ] @ pp true p + | Cic.Appl (t::_) ->[ " [by " ^ ppterm t ^ "]"] + | t ->[ " [by " ^ ppterm t ^ "]"] + in + let rec compat = function + | a::b::tl -> (b ^ a) :: compat tl + | h::[] -> [h] + | [] -> [] + in + let compat l = List.hd l :: compat (List.tl l) in + compat (pp false t) @ ["";""] + in + let names, tys, body = skip_lambda [] context t in + let ppname name = (match name with Some (Cic.Name s) -> s | _ -> "") in + ppname name ^ ":\n" ^ + (if context = [] then + let rec pp_l ctx = function + | (t,name)::tl -> + " " ^ ppname name ^ ": " ^ CicPp.pp t ctx ^ "\n" ^ + pp_l (name::ctx) tl + | [] -> "\n\n" + in + pp_l [] (List.rev (List.combine tys names)) + else "") + ^ + String.concat "\n" (skip_letin names body) ;; + +let pp_proofterm t = + "\n\n" ^ + pp_proofterm (Some (Cic.Name "Hypothesis")) t [] +;; +