1 (* cOpyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
29 (******* CIC substitution ***************************************************)
31 type cic_substitution = Cic.substitution
32 let cic_apply_subst = CicMetaSubst.apply_subst
33 let cic_apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
34 let cic_ppsubst = CicMetaSubst.ppsubst
35 let cic_buildsubst n context t ty tail = (n,(context,t,ty)) :: tail
36 let cic_flatten_subst subst =
38 (fun (i, (context, term, ty)) ->
39 let context = (* cic_apply_subst_context subst*) context in
40 let term = cic_apply_subst subst term in
41 let ty = cic_apply_subst subst ty in
42 (i, (context, term, ty))) subst
43 let rec cic_lookup_subst meta subst =
45 | Cic.Meta (i, _) -> (
46 try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst
47 in cic_lookup_subst t subst
48 with Not_found -> meta
53 let cic_merge_subst_if_possible s1 s2 =
54 let already_in = Hashtbl.create 13 in
55 let rec aux acc = function
56 | ((i,_,x) as s)::tl ->
58 let x' = Hashtbl.find already_in i in
59 if x = x' then aux acc tl else None
62 Hashtbl.add already_in i x;
69 (******** NAIF substitution **************************************************)
71 * naif version of apply subst; the local context of metas is ignored;
72 * we assume the substituted term must be lifted according to the nesting
74 * Alternatively, we could used implicit instead of metas
77 type naif_substitution = (int * Cic.term) list
79 let naif_apply_subst subst term =
83 | Cic.Var (uri,exp_named_subst) ->
84 let exp_named_subst' =
85 List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
87 Cic.Var (uri, exp_named_subst')
90 aux k (CicSubstitution.lift k (List.assoc i subst))
94 | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
95 | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
96 | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
97 | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
98 | Cic.Appl [] -> assert false
99 | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
100 | Cic.Const (uri,exp_named_subst) ->
101 let exp_named_subst' =
102 List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
104 if exp_named_subst' != exp_named_subst then
105 Cic.Const (uri, exp_named_subst')
107 t (* TODO: provare a mantenere il piu' possibile sharing *)
108 | Cic.MutInd (uri,typeno,exp_named_subst) ->
109 let exp_named_subst' =
110 List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
112 Cic.MutInd (uri,typeno,exp_named_subst')
113 | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
114 let exp_named_subst' =
115 List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
117 Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
118 | Cic.MutCase (sp,i,outty,t,pl) ->
119 let pl' = List.map (aux k) pl in
120 Cic.MutCase (sp, i, aux k outty, aux k t, pl')
122 let len = List.length fl in
125 (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
128 | Cic.CoFix (i, fl) ->
129 let len = List.length fl in
131 List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
138 (* naif version of apply_subst_metasenv: we do not apply the
139 substitution to the context *)
141 let naif_apply_subst_metasenv subst metasenv =
143 (fun (n, context, ty) ->
144 (n, context, naif_apply_subst subst ty))
146 (fun (i, _, _) -> not (List.mem_assoc i subst))
149 let naif_ppsubst names subst =
150 "{" ^ String.concat "; "
153 Printf.sprintf "%d:= %s" idx (CicPp.pp t names))
157 let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
159 let naif_flatten_subst subst =
160 List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
163 let rec naif_lookup_subst meta subst =
167 naif_lookup_subst (List.assoc i subst) subst
173 let naif_merge_subst_if_possible s1 s2 =
174 let already_in = Hashtbl.create 13 in
175 let rec aux acc = function
176 | ((i,x) as s)::tl ->
178 let x' = Hashtbl.find already_in i in
179 if x = x' then aux acc tl else None
182 Hashtbl.add already_in i x;
189 (********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
191 type substitution = naif_substitution
192 let apply_subst = naif_apply_subst
193 let apply_subst_metasenv = naif_apply_subst_metasenv
194 let ppsubst ~names l = naif_ppsubst (names:(Cic.name option)list) l
195 let buildsubst = naif_buildsubst
196 let flatten_subst = naif_flatten_subst
197 let lookup_subst = naif_lookup_subst
199 (* filter out from metasenv the variables in substs *)
200 let filter subst metasenv =
203 try let _ = List.find (fun (i, _) -> m = i) subst in false
204 with Not_found -> true)
208 let is_in_subst i subst = List.mem_assoc i subst;;
210 let merge_subst_if_possible = naif_merge_subst_if_possible;;
212 let empty_subst = [];;
214 (********* EQUALITY **********************************************************)
216 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
217 type uncomparable = int -> int
219 uncomparable * (* trick to break structural equality *)
222 (Cic.term * (* type *)
223 Cic.term * (* left side *)
224 Cic.term * (* right side *)
225 Utils.comparison) * (* ordering *)
226 Cic.metasenv * (* environment for metas *)
228 and proof = new_proof * old_proof
232 | Step of substitution * (rule * int*(Utils.pos*int)* Cic.term) (* eq1, eq2,predicate *)
234 | NoProof (* term is the goal missing a proof *)
235 | BasicProof of substitution * Cic.term
237 substitution * UriManager.uri *
238 (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * old_proof
239 | ProofGoalBlock of old_proof * old_proof
240 | ProofSymBlock of Cic.term list * old_proof
241 | SubProof of Cic.term * int * old_proof
242 and goal_proof = (Utils.pos * int * substitution * Cic.term) list
247 let id_to_eq = Hashtbl.create 1024;;
255 Hashtbl.clear id_to_eq
258 let uncomparable = fun _ -> 0
260 let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
261 let id = freshid () in
262 let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in
263 Hashtbl.add id_to_eq id eq;
267 let mk_tmp_equality (weight,(ty,l,r,o),m) =
269 uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id
273 let open_equality (_,weight,proof,(ty,l,r,o),m,id) =
274 (weight,proof,(ty,l,r,o),m,id)
276 let string_of_equality ?env eq =
279 let w, _, (ty, left, right, o), _ , id = open_equality eq in
280 Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
281 id w (CicPp.ppterm ty)
283 (Utils.string_of_comparison o) (CicPp.ppterm right)
284 | Some (_, context, _) ->
285 let names = Utils.names_of_context context in
286 let w, _, (ty, left, right, o), _ , id = open_equality eq in
287 Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
288 id w (CicPp.pp ty names)
289 (CicPp.pp left names) (Utils.string_of_comparison o)
290 (CicPp.pp right names)
293 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
294 Pervasives.compare s1 s2
297 let rec string_of_proof_old ?(names=[]) = function
298 | NoProof -> "NoProof "
299 | BasicProof (s, t) -> "BasicProof(" ^
300 ppsubst ~names s ^ ", " ^ (CicPp.pp t names) ^ ")"
301 | SubProof (t, i, p) ->
302 Printf.sprintf "SubProof(%s, %s, %s)"
303 (CicPp.pp t names) (string_of_int i) (string_of_proof_old p)
304 | ProofSymBlock (_,p) ->
305 Printf.sprintf "ProofSymBlock(%s)" (string_of_proof_old p)
306 | ProofBlock (subst, _, _, _ ,(_,eq),old) ->
307 let _,(_,p),_,_,_ = open_equality eq in
308 "ProofBlock(" ^ (ppsubst ~names subst) ^ "," ^ (string_of_proof_old old) ^ "," ^
309 string_of_proof_old p ^ ")"
310 | ProofGoalBlock (p1, p2) ->
311 Printf.sprintf "ProofGoalBlock(%s, %s)"
312 (string_of_proof_old p1) (string_of_proof_old p2)
318 let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
321 Not_found -> assert false
324 let string_of_proof_new ?(names=[]) p gp =
325 let str_of_rule = function
326 | SuperpositionRight -> "SupR"
327 | SuperpositionLeft -> "SupL"
328 | Demodulation -> "Demod"
330 let str_of_pos = function
331 | Utils.Left -> "left"
332 | Utils.Right -> "right"
334 let fst3 (x,_,_) = x in
335 let rec aux margin name =
336 let prefix = String.make margin ' ' ^ name ^ ": " in function
338 Printf.sprintf "%sExact (%s)\n"
339 prefix (CicPp.pp t names)
340 | Step (subst,(rule,eq1,(pos,eq2),pred)) ->
341 Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
342 prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos)
343 (CicPp.pp pred names)^
344 aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^
345 aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2))
352 "GOAL: %s %d %s %s\n"
353 (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^
354 aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
358 let rec depend eq id =
359 let (_,(p,_),(_,_,_,_),_,ideq) = open_equality eq in
360 if id = ideq then true else
363 | Step (_,(_,id1,(_,id2),_)) ->
364 let eq1 = Hashtbl.find id_to_eq id1 in
365 let eq2 = Hashtbl.find id_to_eq id2 in
366 depend eq1 id || depend eq1 id2
369 let ppsubst = ppsubst ~names:[]
371 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
372 let build_ens uri termlist =
373 let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
375 | Cic.Constant (_, _, _, uris, _) ->
376 assert (List.length uris <= List.length termlist);
377 let rec aux = function
379 | (uri::uris), (term::tl) ->
380 let ens, args = aux (uris, tl) in
381 (uri, term)::ens, args
382 | _, _ -> assert false
388 let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
389 let rec do_build_proof proof =
392 Printf.fprintf stderr "WARNING: no proof!\n";
394 | BasicProof (s,term) -> apply_subst s term
395 | ProofGoalBlock (proofbit, proof) ->
396 print_endline "found ProofGoalBlock, going up...";
397 do_build_goal_proof proofbit proof
398 | ProofSymBlock (termlist, proof) ->
399 let proof = do_build_proof proof in
400 let ens, args = build_ens (Utils.sym_eq_URI ()) termlist in
401 Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
402 | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
403 let t' = Cic.Lambda (name, ty, bo) in
404 let _, (_,proof), (ty, what, other, _), menv',_ = open_equality eq in
405 let proof' = do_build_proof proof in
406 let eqproof = do_build_proof eqproof in
408 if pos = Utils.Left then what, other else other, what
411 (Cic.Appl [Cic.Const (eq_URI, []); ty;
412 what; t'; eqproof; other; proof'])
413 | SubProof (term, meta_index, proof) ->
414 let proof = do_build_proof proof in
416 | Cic.Meta (j, _) -> i = j
419 ProofEngineReduction.replace
420 ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
422 and do_build_goal_proof proofbit proof =
424 | ProofGoalBlock (pb, p) ->
425 do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
426 | _ -> do_build_proof (replace_proof proofbit proof)
428 and replace_proof newproof = function
429 | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
430 let eqproof' = replace_proof newproof eqproof in
431 ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
432 | ProofGoalBlock (pb, p) ->
433 let pb' = replace_proof newproof pb in
434 ProofGoalBlock (pb', p)
435 | BasicProof _ -> newproof
436 | SubProof (term, meta_index, p) ->
437 SubProof (term, meta_index, replace_proof newproof p)
443 let mk_sym uri ty t1 t2 p =
444 let ens, args = build_ens uri [ty;t1;t2;p] in
445 Cic.Appl (Cic.Const(uri, ens) :: args)
448 let mk_trans uri ty t1 t2 t3 p12 p23 =
449 let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in
450 Cic.Appl (Cic.Const (uri, ens) :: args)
453 let mk_eq_ind uri ty what pred p1 other p2 =
454 Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
457 let p_of_sym ens tl =
458 let args = List.map snd ens @ tl in
464 let open_trans ens tl =
465 let args = List.map snd ens @ tl in
467 | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2
472 let rec remove_refl t =
474 | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
475 when LibraryObjects.is_trans_eq_URI uri_trans ->
476 let ty,l,m,r,p1,p2 = open_trans ens tl in
478 | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 ->
480 | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] ->
482 | _ -> Cic.Appl (List.map remove_refl args))
483 | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
486 let rec canonical t =
488 | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
489 when LibraryObjects.is_sym_eq_URI uri_sym ->
490 (match p_of_sym ens tl with
491 | Cic.Appl ((Cic.Const(uri,ens))::tl)
492 when LibraryObjects.is_sym_eq_URI uri ->
493 canonical (p_of_sym ens tl)
494 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
495 when LibraryObjects.is_trans_eq_URI uri_trans ->
496 let ty,l,m,r,p1,p2 = open_trans ens tl in
497 mk_trans uri_trans ty r m l
498 (canonical (mk_sym uri_sym ty m r p2))
499 (canonical (mk_sym uri_sym ty l m p1))
500 | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl)
501 when LibraryObjects.is_eq_ind_URI uri_ind ||
502 LibraryObjects.is_eq_ind_r_URI uri_ind ->
503 let ty, what, pred, p1, other, p2 =
505 | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
510 | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
511 when LibraryObjects.is_eq_URI uri ->
513 (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
515 prerr_endline (CicPp.ppterm pred);
518 let l = CicSubstitution.subst what l in
519 let r = CicSubstitution.subst what r in
522 canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
523 | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
524 when LibraryObjects.is_eq_URI uri -> t
525 | _ -> Cic.Appl (List.map canonical args))
526 | Cic.Appl l -> Cic.Appl (List.map canonical l)
529 remove_refl (canonical t)
532 let build_proof_step subst p1 p2 pos l r pred =
533 let p1 = apply_subst subst p1 in
534 let p2 = apply_subst subst p2 in
535 let l = apply_subst subst l in
536 let r = apply_subst subst r in
537 let pred = apply_subst subst pred in
538 let ty,body = (* Cic.Implicit None *)
540 | Cic.Lambda (_,ty,body) -> ty,body
543 let what, other = (* Cic.Implicit None, Cic.Implicit None *)
544 if pos = Utils.Left then l,r else r,l
547 CicSubstitution.subst (Cic.Implicit None) t <>
548 CicSubstitution.subst (Cic.Rel 1) t
552 |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
553 let third = CicSubstitution.subst (Cic.Implicit None) third in
554 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
555 let uri_sym = LibraryObjects.sym_eq_URI ~eq in
556 mk_trans uri_trans ty other what third
557 (mk_sym uri_sym ty what other p2) p1
558 |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right ->
559 let third = CicSubstitution.subst (Cic.Implicit None) third in
560 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
561 mk_trans uri_trans ty other what third p2 p1
562 |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left ->
563 let third = CicSubstitution.subst (Cic.Implicit None) third in
564 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
565 mk_trans uri_trans ty third what other p1 p2
566 |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right ->
567 let third = CicSubstitution.subst (Cic.Implicit None) third in
568 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
569 let uri_sym = LibraryObjects.sym_eq_URI ~eq in
570 mk_trans uri_trans ty third what other p1
571 (mk_sym uri_sym ty other what p2)
572 | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs
574 let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
575 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
576 let pred_of t = CicSubstitution.subst t lhs in
577 let pred_of_what = pred_of what in
578 let pred_of_other = pred_of other in
580 * ====================================
581 * inject p2: P(what) = P(other)
583 let rec inject ty lhs what other p2 =
585 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
586 when LibraryObjects.is_trans_eq_URI uri_trans ->
587 let ty,l,m,r,plm,pmr = open_trans ens tl in
588 mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
589 (inject ty lhs m r pmr) (inject ty lhs l m plm)
591 let liftedty = CicSubstitution.lift 1 ty in
592 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
594 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
596 (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
597 (Cic.Lambda (Cic.Name "foo",ty,
599 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
600 refl_eq_part what p2)
602 mk_trans uri_trans ty pred_of_other pred_of_what rhs
603 (inject ty lhs what other p2) p1
604 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
606 let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
607 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
608 let pred_of t = CicSubstitution.subst t lhs in
609 let pred_of_what = pred_of what in
610 let pred_of_other = pred_of other in
612 * ====================================
613 * inject p2: P(what) = P(other)
615 let rec inject ty lhs what other p2 =
617 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
618 when LibraryObjects.is_trans_eq_URI uri_trans ->
619 let ty,l,m,r,plm,pmr = open_trans ens tl in
620 mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
621 (inject ty lhs m l plm)
622 (inject ty lhs r m pmr)
624 let liftedty = CicSubstitution.lift 1 ty in
625 let lifted_pred_of_other =
626 CicSubstitution.lift 1 (pred_of other) in
628 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
630 mk_eq_ind (Utils.eq_ind_URI ()) ty other
631 (Cic.Lambda (Cic.Name "foo",ty,
633 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
636 mk_trans uri_trans ty pred_of_other pred_of_what rhs
637 (inject ty lhs what other p2) p1
638 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
640 let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
641 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
642 let pred_of t = CicSubstitution.subst t rhs in
643 let pred_of_what = pred_of what in
644 let pred_of_other = pred_of other in
646 * ====================================
647 * inject p2: P(what) = P(other)
649 let rec inject ty lhs what other p2 =
651 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
652 when LibraryObjects.is_trans_eq_URI uri_trans ->
653 let ty,l,m,r,plm,pmr = open_trans ens tl in
654 mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
655 (inject ty lhs m r pmr)
656 (inject ty lhs l m plm)
658 let liftedty = CicSubstitution.lift 1 ty in
659 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
661 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
663 (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
664 (Cic.Lambda (Cic.Name "foo",ty,
666 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
667 refl_eq_part what p2)
669 mk_trans uri_trans ty lhs pred_of_what pred_of_other
670 p1 (inject ty rhs other what p2)
671 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
673 let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
674 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
675 let pred_of t = CicSubstitution.subst t rhs in
676 let pred_of_what = pred_of what in
677 let pred_of_other = pred_of other in
679 * ====================================
680 * inject p2: P(what) = P(other)
682 let rec inject ty lhs what other p2 =
684 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
685 when LibraryObjects.is_trans_eq_URI uri_trans ->
686 let ty,l,m,r,plm,pmr = open_trans ens tl in
687 (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
688 (inject ty lhs m l plm)
689 (inject ty lhs r m pmr))
691 let liftedty = CicSubstitution.lift 1 ty in
692 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
694 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
696 mk_eq_ind (Utils.eq_ind_URI ()) ty other
697 (Cic.Lambda (Cic.Name "foo",ty,
699 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
702 mk_trans uri_trans ty lhs pred_of_what pred_of_other
703 p1 (inject ty rhs other what p2)
706 mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
708 mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
711 let build_proof_term_new proof =
712 let rec aux = function
714 | Step (subst,(_, id1, (pos,id2), pred)) ->
715 let p,_,_ = proof_of_id id1 in
717 let p,l,r = proof_of_id id2 in
719 build_proof_step subst p1 p2 pos l r pred
724 let wfo goalproof proof =
726 let p,_,_ = proof_of_id id in
728 | Exact _ -> if (List.mem id acc) then acc else id :: acc
729 | Step (_,(_,id1, (_,id2), _)) ->
730 let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
731 let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
737 | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2
739 List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof
742 let string_of_id names id =
744 let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
747 Printf.sprintf "%d = %s: %s = %s" id
748 (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
749 | Step (_,(step,id1, (_,id2), _) ) ->
750 Printf.sprintf "%6d: %s %6d %6d %s = %s" id
751 (if step = SuperpositionRight then "SupR" else "Demo")
752 id1 id2 (CicPp.pp l names) (CicPp.pp r names)
754 Not_found -> assert false
756 let pp_proof names goalproof proof =
757 String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^
758 "\ngoal is demodulated with " ^
760 ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
763 let build_goal_proof l initial =
766 (fun current_proof (pos,id,subst,pred) ->
767 let p,l,r = proof_of_id id in
768 let p = build_proof_term_new p in
769 let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
770 build_proof_step subst current_proof p pos l r pred)
776 let refl_proof ty term =
779 (LibraryObjects.eq_URI (), 0, 1, []);
783 let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
785 let relocate newmeta menv =
786 let subst, metasenv, newmeta =
788 (fun (i, context, ty) (subst, menv, maxmeta) ->
790 CicMkImplicit.identity_relocation_list_for_metavariable context *)
792 let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
793 let newmeta = maxmeta, context, ty in
794 newsubst, newmeta::menv, maxmeta+1)
795 menv ([], [], newmeta+1)
797 let metasenv = apply_subst_metasenv subst metasenv in
798 let subst = flatten_subst subst in
799 subst, metasenv, newmeta
802 let fix_metas newmeta eq =
803 let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in
806 fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
807 prerr_endline (string_of_equality eq); *)
808 let subst, metasenv, newmeta = relocate newmeta menv in
809 let ty = apply_subst subst ty in
810 let left = apply_subst subst left in
811 let right = apply_subst subst right in
812 let fix_proof = function
814 | BasicProof (subst',term) -> BasicProof (subst@subst',term)
815 | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
819 (fun (i, (context, term, ty)) ->
820 let context = apply_subst_context subst context in
821 let term = apply_subst subst term in
822 let ty = apply_subst subst ty in
823 (i, (context, term, ty))) subst' in *)
824 ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
827 let fix_new_proof = function
828 | Exact p -> Exact (apply_subst subst p)
829 | Step (s,(r,id1,(pos,id2),pred)) ->
830 Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
832 let new_p = fix_new_proof p1 in
833 let old_p = fix_proof p2 in
834 let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in
835 (* debug prerr_endline (string_of_equality eq); *)
838 exception NotMetaConvertible;;
840 let meta_convertibility_aux table t1 t2 =
841 let module C = Cic in
842 let rec aux ((table_l, table_r) as table) t1 t2 =
844 | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
845 let m1_binding, table_l =
846 try List.assoc m1 table_l, table_l
847 with Not_found -> m2, (m1, m2)::table_l
848 and m2_binding, table_r =
849 try List.assoc m2 table_r, table_r
850 with Not_found -> m1, (m2, m1)::table_r
852 if (m1_binding <> m2) || (m2_binding <> m1) then
853 raise NotMetaConvertible
859 | None, Some _ | Some _, None -> raise NotMetaConvertible
861 | Some t1, Some t2 -> (aux res t1 t2))
862 (table_l, table_r) tl1 tl2
863 with Invalid_argument _ ->
864 raise NotMetaConvertible
866 | C.Var (u1, ens1), C.Var (u2, ens2)
867 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
868 aux_ens table ens1 ens2
869 | C.Cast (s1, t1), C.Cast (s2, t2)
870 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
871 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
872 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
873 let table = aux table s1 s2 in
875 | C.Appl l1, C.Appl l2 -> (
876 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
877 with Invalid_argument _ -> raise NotMetaConvertible
879 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
880 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
881 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
882 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
883 aux_ens table ens1 ens2
884 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
885 when (UriManager.eq u1 u2) && i1 = i2 ->
886 let table = aux table s1 s2 in
887 let table = aux table t1 t2 in (
888 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
889 with Invalid_argument _ -> raise NotMetaConvertible
891 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
894 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
895 if i1 <> i2 then raise NotMetaConvertible
897 let res = (aux res s1 s2) in aux res t1 t2)
899 with Invalid_argument _ -> raise NotMetaConvertible
901 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
904 (fun res (n1, s1, t1) (n2, s2, t2) ->
905 let res = aux res s1 s2 in aux res t1 t2)
907 with Invalid_argument _ -> raise NotMetaConvertible
909 | t1, t2 when t1 = t2 -> table
910 | _, _ -> raise NotMetaConvertible
912 and aux_ens table ens1 ens2 =
913 let cmp (u1, t1) (u2, t2) =
914 Pervasives.compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
916 let ens1 = List.sort cmp ens1
917 and ens2 = List.sort cmp ens2 in
920 (fun res (u1, t1) (u2, t2) ->
921 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
924 with Invalid_argument _ -> raise NotMetaConvertible
930 let meta_convertibility_eq eq1 eq2 =
931 let _, _, (ty, left, right, _), _,_ = open_equality eq1 in
932 let _, _, (ty', left', right', _), _,_ = open_equality eq2 in
935 else if (left = left') && (right = right') then
937 else if (left = right') && (right = left') then
941 let table = meta_convertibility_aux ([], []) left left' in
942 let _ = meta_convertibility_aux table right right' in
944 with NotMetaConvertible ->
946 let table = meta_convertibility_aux ([], []) left right' in
947 let _ = meta_convertibility_aux table right left' in
949 with NotMetaConvertible ->
954 let meta_convertibility t1 t2 =
959 ignore(meta_convertibility_aux ([], []) t1 t2);
961 with NotMetaConvertible ->
965 exception TermIsNotAnEquality;;
967 let term_is_equality term =
968 let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
970 | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
974 let equality_of_term proof term =
975 let eq_uri = LibraryObjects.eq_URI () in
976 let iseq uri = UriManager.eq uri eq_uri in
978 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
979 let o = !Utils.compare_terms t1 t2 in
980 let stat = (ty,t1,t2,o) in
981 let w = Utils.compute_equality_weight stat in
982 let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in
985 raise TermIsNotAnEquality
988 let is_weak_identity eq =
989 let _,_,(_,left, right,_),_,_ = open_equality eq in
990 left = right || meta_convertibility left right
993 let is_identity (_, context, ugraph) eq =
994 let _,_,(ty,left,right,_),menv,_ = open_equality eq in
996 (* (meta_convertibility left right)) *)
997 fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
1001 let term_of_equality equality =
1002 let _, _, (ty, left, right, _), menv, _= open_equality equality in
1003 let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
1004 let argsno = List.length menv in
1006 CicSubstitution.lift argsno
1007 (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
1011 (fun (i,_,ty) (n, t) ->
1012 let name = Cic.Name ("X" ^ (string_of_int n)) in
1013 let ty = CicSubstitution.lift (n-1) ty in
1015 ProofEngineReduction.replace
1016 ~equality:eq ~what:[i]
1017 ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
1019 (n-1, Cic.Prod (name, ty, t)))