* http://cs.unibo.it/helm/.
*)
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
(* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
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
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,_,_) =
(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]))
| 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 =
(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))
| 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
let n_purged = ref 0;;
let collect alive1 alive2 alive3 =
- let _ = <:start<collect>> in
+(* let _ = <:start<collect>> in *)
let deps_of id =
let p,_,_ = proof_of_id id in
match p with
in
n_purged := !n_purged + List.length to_purge;
List.iter (Hashtbl.remove id_to_eq) to_purge;
- let _ = <:stop<collect>> in ()
+(* let _ = <:stop<collect>> in () *)
;;
let id_of e =
let _,_,_,_,id = open_equality e in id
;;
-let get_stats () =
+let get_stats () = ""
+(*
<:show<Equality.>> ^
"# 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 []
+;;
+
projects / helm.git / blobdiff