let id = freshid () in
let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
Hashtbl.add id_to_eq id eq;
+
eq
;;
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
CicSubstitution.subst (Cic.Rel 1) t
;;
+let head_of_apply = function | Cic.Appl (hd::_) -> hd | t -> t;;
+let tail_of_apply = function | Cic.Appl (_::tl) -> tl | t -> [];;
+let count_args t = List.length (tail_of_apply t);;
+let rec build_nat =
+ let u = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
+ function
+ | 0 -> Cic.MutConstruct(u,0,1,[])
+ | n ->
+ Cic.Appl [Cic.MutConstruct(u,0,2,[]);build_nat (n-1)]
+;;
+let tyof context menv t =
+ try
+ fst(CicTypeChecker.type_of_aux' menv context t CicUniv.empty_ugraph)
+ with
+ | CicTypeChecker.TypeCheckerFailure _
+ | CicTypeChecker.AssertFailure _ -> assert false
+;;
+let rec lambdaof left context = function
+ | Cic.Prod (n,s,t) ->
+ Cic.Lambda (n,s,lambdaof left context t)
+ | Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r]
+ when LibraryObjects.is_eq_URI uri -> if left then l else r
+ | t ->
+ let names = Utils.names_of_context context in
+ prerr_endline ("lambdaof: " ^ (CicPp.pp t names));
+ assert false
+;;
-let canonical t =
+let canonical t context menv =
let rec remove_refl t =
match t with
| Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
Cic.LetIn (name,remove_refl bo,remove_refl rest)
| _ -> t
in
- let rec canonical t =
+ let rec canonical context t =
match t with
- | Cic.LetIn(name,bo,rest) -> Cic.LetIn(name,canonical bo,canonical rest)
+ | Cic.LetIn(name,bo,rest) ->
+ let context' = (Some (name,Cic.Def (bo,None)))::context in
+ Cic.LetIn(name,canonical context 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
| Cic.Appl ((Cic.Const(uri,ens))::tl)
when LibraryObjects.is_sym_eq_URI uri ->
- canonical (p_of_sym ens tl)
+ canonical context (p_of_sym ens tl)
| 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
mk_trans uri_trans ty r m l
- (canonical (mk_sym uri_sym ty m r p2))
- (canonical (mk_sym uri_sym ty l m p1))
+ (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",[])
+ in
+ Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p]))
+
+(*
+ let sym_eq = Cic.Const(uri_sym,ens) in
+ let eq_f = Cic.Const(uri_feq,[]) in
+ let b = Cic.MutConstruct (UriManager.uri_of_string
+ "cic:/matita/datatypes/bool/bool.ind",0,1,[])
+ in
+ let u = ty1 in
+ let ctx = f in
+ let n = build_nat (count_args p) in
+ let h = head_of_apply p in
+ let predl = lambdaof true context (tyof context menv h) in
+ let predr = lambdaof false context (tyof context menv h) in
+ let args = tail_of_apply p in
+ let appl =
+ Cic.Appl
+ ([Cic.Const(UriManager.uri_of_string
+ "cic:/matita/paramodulation/rewrite.con",[]);
+ eq; sym_eq; eq_f; b; u; ctx; n; predl; predr; h] @
+ args)
+ in
+ appl
+*)
+(*
| Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl)
when LibraryObjects.is_eq_ind_URI uri_ind ||
LibraryObjects.is_eq_ind_r_URI uri_ind ->
Cic.Appl
[he;ty;what;pred;
canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
+*)
| Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
when LibraryObjects.is_eq_URI uri -> t
- | _ -> Cic.Appl (List.map canonical args))
- | Cic.Appl l -> Cic.Appl (List.map canonical l)
+ | _ -> Cic.Appl (List.map (canonical context) args))
+ | Cic.Appl l -> Cic.Appl (List.map (canonical context) l)
| _ -> t
in
- remove_refl (canonical t)
+ remove_refl (canonical context t)
;;
let ty_of_lambda = function
| _ -> assert false
;;
+let mk_feq uri_feq ty ty1 left pred right t =
+ Cic.Appl [Cic.Const(uri_feq,[]);ty;ty1;pred;left;right;t]
+;;
+
let contextualize uri ty left right t =
let hole = Cic.Implicit (Some `Hole) in
(* aux [uri] [ty] [left] [right] [ctx] [t]
mk_trans uri_trans ctx_ty a b c paeqb pbeqc
| t when ctx_d = hole -> t
| t ->
- let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
- let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
+(* 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 pred =
- (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
- let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in
+(* let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in *)
let l =
let ctx_d = CicSubstitution.lift 1 ctx_d in
put_in_ctx ctx_d (Cic.Rel 1)
in
- let lty = CicSubstitution.lift 1 ctx_ty in
- Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
+(* let lty = CicSubstitution.lift 1 ctx_ty in *)
+(* Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r)) *)
+ Cic.Lambda (Cic.Name "foo",ty,l)
in
- let d_left = put_in_ctx ctx_d left in
- let d_right = put_in_ctx ctx_d right in
- let refl_eq = mk_refl uri ctx_ty d_left in
- mk_sym uri_sym ctx_ty d_right d_left
- (mk_eq_ind uri_ind ty left pred refl_eq right t)
+(* let d_left = put_in_ctx ctx_d left in *)
+(* let d_right = put_in_ctx ctx_d right in *)
+(* let refl_eq = mk_refl uri ctx_ty d_left in *)
+(* mk_sym uri_sym ctx_ty d_right d_left *)
+(* (mk_eq_ind uri_ind ty left pred refl_eq right t) *)
+ (mk_feq uri_feq ty ctx_ty left pred right t)
in
aux uri ty left right hole ty t
;;
aux proof
;;
-let build_goal_proof eq l initial ty se =
+let build_goal_proof 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 l initial in
let letsno = List.length lets in
cic, p))
lets (letsno-1,initial)
in
-(* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
- * *)
-proof,
+ canonical
+ (contextualize_rewrites proof (CicSubstitution.lift letsno ty))
+ context menv,
se
;;
projects / helm.git / blobdiff