* http://cs.unibo.it/helm/.
*)
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
(* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
let id = freshid () in
let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
Hashtbl.add id_to_eq id eq;
+
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
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,_,_) =
Pervasives.compare s1 s2
;;
+let rec max_weight_in_proof current =
+ function
+ | Exact _ -> current
+ | Step (_, (_,id1,(_,id2),_)) ->
+ let eq1 = Hashtbl.find id_to_eq id1 in
+ let eq2 = Hashtbl.find id_to_eq id2 in
+ let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in
+ let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in
+ let current = max current w1 in
+ let current = max_weight_in_proof current p1 in
+ let current = max current w2 in
+ max_weight_in_proof current p2
+
+let max_weight_in_goal_proof =
+ List.fold_left
+ (fun current (_,_,id,_,_) ->
+ let eq = Hashtbl.find id_to_eq id in
+ let (w,p,(_,_,_,_),_,_) = open_equality eq in
+ let current = max current w in
+ max_weight_in_proof current p)
+
+let max_weight goal_proof proof =
+ let current = max_weight_in_proof 0 proof in
+ max_weight_in_goal_proof current goal_proof
+
let proof_of_id id =
try
let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
(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]))
Cic.Appl [Cic.Const(uri_feq,[]);ty;ty1;pred;left;right;t]
;;
+let rec look_ahead aux = function
+ | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) as t
+ when LibraryObjects.is_eq_ind_URI uri_ind ||
+ LibraryObjects.is_eq_ind_r_URI uri_ind ->
+ let ty1,what,pred,p1,other,p2 = open_eq_ind tl in
+ let ty2,eq,lp,rp = open_pred pred in
+ let hole = Cic.Implicit (Some `Hole) in
+ let ty2 = CicSubstitution.subst hole ty2 in
+ aux ty1 (CicSubstitution.subst other lp) (CicSubstitution.subst other rp) hole ty2 t
+ | Cic.Lambda (n,s,t) -> Cic.Lambda (n,s,look_ahead aux t)
+ | t -> t
+;;
+
let contextualize uri ty left right t =
let hole = Cic.Implicit (Some `Hole) in
- (* aux [uri] [ty] [left] [right] [ctx] [t]
+ (* aux [uri] [ty] [left] [right] [ctx] [ctx_ty] [t]
*
* the parameters validate this invariant
* t: eq(uri) ty left right
* that is used only by the base case
*
* ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
- * ty_ctx is the type of ctx_d
+ * ctx_ty is the type of ctx
*)
let rec aux uri ty left right ctx_d ctx_ty = function
| Cic.Appl ((Cic.Const(uri_sym,ens))::tl)
let ty,l,r,p = open_sym ens tl in
mk_sym uri_sym ty l r (aux uri ty l r ctx_d ctx_ty p)
| Cic.LetIn (name,body,rest) ->
- (* we should go in body *)
- Cic.LetIn (name,body,aux uri ty left right ctx_d ctx_ty rest)
+ Cic.LetIn (name,look_ahead (aux uri) body, aux uri ty left right ctx_d ctx_ty 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 ->
| 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 =
let parametrize_proof p l r ty =
let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in
let mot = CicUtil.metas_of_term_set in
- let parameters = uniq (mot p @ mot l @ mot r) in
+ let parameters = uniq ((*mot p @*) mot l @ mot r) in
(* ?if they are under a lambda? *)
let parameters =
HExtlib.list_uniq (List.sort Pervasives.compare parameters)
(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