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 open_equality (_,weight,proof,(ty,l,r,o),m,id) =
268 (weight,proof,(ty,l,r,o),m,id)
270 let string_of_equality ?env eq =
273 let w, _, (ty, left, right, o), _ , id = open_equality eq in
274 Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
275 id w (CicPp.ppterm ty)
277 (Utils.string_of_comparison o) (CicPp.ppterm right)
278 | Some (_, context, _) ->
279 let names = Utils.names_of_context context in
280 let w, _, (ty, left, right, o), _ , id = open_equality eq in
281 Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
282 id w (CicPp.pp ty names)
283 (CicPp.pp left names) (Utils.string_of_comparison o)
284 (CicPp.pp right names)
287 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
288 Pervasives.compare s1 s2
291 let rec string_of_proof_old ?(names=[]) = function
292 | NoProof -> "NoProof "
293 | BasicProof (s, t) -> "BasicProof(" ^
294 ppsubst ~names s ^ ", " ^ (CicPp.pp t names) ^ ")"
295 | SubProof (t, i, p) ->
296 Printf.sprintf "SubProof(%s, %s, %s)"
297 (CicPp.pp t names) (string_of_int i) (string_of_proof_old p)
298 | ProofSymBlock (_,p) ->
299 Printf.sprintf "ProofSymBlock(%s)" (string_of_proof_old p)
300 | ProofBlock (subst, _, _, _ ,(_,eq),old) ->
301 let _,(_,p),_,_,_ = open_equality eq in
302 "ProofBlock(" ^ (ppsubst ~names subst) ^ "," ^ (string_of_proof_old old) ^ "," ^
303 string_of_proof_old p ^ ")"
304 | ProofGoalBlock (p1, p2) ->
305 Printf.sprintf "ProofGoalBlock(%s, %s)"
306 (string_of_proof_old p1) (string_of_proof_old p2)
312 let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
315 Not_found -> assert false
318 let string_of_proof_new ?(names=[]) p gp =
319 let str_of_rule = function
320 | SuperpositionRight -> "SupR"
321 | SuperpositionLeft -> "SupL"
322 | Demodulation -> "Demod"
324 let str_of_pos = function
325 | Utils.Left -> "left"
326 | Utils.Right -> "right"
328 let fst3 (x,_,_) = x in
329 let rec aux margin name =
330 let prefix = String.make margin ' ' ^ name ^ ": " in function
332 Printf.sprintf "%sExact (%s)\n"
333 prefix (CicPp.pp t names)
334 | Step (subst,(rule,eq1,(pos,eq2),pred)) ->
335 Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
336 prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos)
337 (CicPp.pp pred names)^
338 aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^
339 aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2))
346 "GOAL: %s %d %s %s\n"
347 (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^
348 aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
352 let ppsubst = ppsubst ~names:[]
354 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
355 let build_ens uri termlist =
356 let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
358 | Cic.Constant (_, _, _, uris, _) ->
359 assert (List.length uris <= List.length termlist);
360 let rec aux = function
362 | (uri::uris), (term::tl) ->
363 let ens, args = aux (uris, tl) in
364 (uri, term)::ens, args
365 | _, _ -> assert false
371 let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
372 let rec do_build_proof proof =
375 Printf.fprintf stderr "WARNING: no proof!\n";
377 | BasicProof (s,term) -> apply_subst s term
378 | ProofGoalBlock (proofbit, proof) ->
379 print_endline "found ProofGoalBlock, going up...";
380 do_build_goal_proof proofbit proof
381 | ProofSymBlock (termlist, proof) ->
382 let proof = do_build_proof proof in
383 let ens, args = build_ens (Utils.sym_eq_URI ()) termlist in
384 Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
385 | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
386 let t' = Cic.Lambda (name, ty, bo) in
387 let _, (_,proof), (ty, what, other, _), menv',_ = open_equality eq in
388 let proof' = do_build_proof proof in
389 let eqproof = do_build_proof eqproof in
391 if pos = Utils.Left then what, other else other, what
394 (Cic.Appl [Cic.Const (eq_URI, []); ty;
395 what; t'; eqproof; other; proof'])
396 | SubProof (term, meta_index, proof) ->
397 let proof = do_build_proof proof in
399 | Cic.Meta (j, _) -> i = j
402 ProofEngineReduction.replace
403 ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
405 and do_build_goal_proof proofbit proof =
407 | ProofGoalBlock (pb, p) ->
408 do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
409 | _ -> do_build_proof (replace_proof proofbit proof)
411 and replace_proof newproof = function
412 | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
413 let eqproof' = replace_proof newproof eqproof in
414 ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
415 | ProofGoalBlock (pb, p) ->
416 let pb' = replace_proof newproof pb in
417 ProofGoalBlock (pb', p)
418 | BasicProof _ -> newproof
419 | SubProof (term, meta_index, p) ->
420 SubProof (term, meta_index, replace_proof newproof p)
426 let mk_sym uri ty t1 t2 p =
427 let ens, args = build_ens uri [ty;t1;t2;p] in
428 Cic.Appl (Cic.Const(uri, ens) :: args)
431 let mk_trans uri ty t1 t2 t3 p12 p23 =
432 let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in
433 Cic.Appl (Cic.Const (uri, ens) :: args)
436 let mk_eq_ind uri ty what pred p1 other p2 =
437 Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
440 let p_of_sym ens tl =
441 let args = List.map snd ens @ tl in
447 let open_trans ens tl =
448 let args = List.map snd ens @ tl in
450 | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2
455 let rec remove_refl t =
457 | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
458 when LibraryObjects.is_trans_eq_URI uri_trans ->
459 let ty,l,m,r,p1,p2 = open_trans ens tl in
461 | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 ->
463 | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] ->
465 | _ -> Cic.Appl (List.map remove_refl args))
466 | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
469 let rec canonical t =
471 | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
472 when LibraryObjects.is_sym_eq_URI uri_sym ->
473 (match p_of_sym ens tl with
474 | Cic.Appl ((Cic.Const(uri,ens))::tl)
475 when LibraryObjects.is_sym_eq_URI uri ->
476 canonical (p_of_sym ens tl)
477 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
478 when LibraryObjects.is_trans_eq_URI uri_trans ->
479 let ty,l,m,r,p1,p2 = open_trans ens tl in
480 mk_trans uri_trans ty r m l
481 (canonical (mk_sym uri_sym ty m r p2))
482 (canonical (mk_sym uri_sym ty l m p1))
483 | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl)
484 when LibraryObjects.is_eq_ind_URI uri_ind ||
485 LibraryObjects.is_eq_ind_r_URI uri_ind ->
486 let ty, what, pred, p1, other, p2 =
488 | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
493 | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
494 when LibraryObjects.is_eq_URI uri ->
496 (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
498 prerr_endline (CicPp.ppterm pred);
501 let l = CicSubstitution.subst what l in
502 let r = CicSubstitution.subst what r in
505 canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
506 | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
507 when LibraryObjects.is_eq_URI uri -> t
508 | _ -> Cic.Appl (List.map canonical args))
509 | Cic.Appl l -> Cic.Appl (List.map canonical l)
512 remove_refl (canonical t)
515 let build_proof_step subst p1 p2 pos l r pred =
516 let p1 = apply_subst subst p1 in
517 let p2 = apply_subst subst p2 in
518 let l = apply_subst subst l in
519 let r = apply_subst subst r in
520 let pred = apply_subst subst pred in
521 let ty,body = (* Cic.Implicit None *)
523 | Cic.Lambda (_,ty,body) -> ty,body
526 let what, other = (* Cic.Implicit None, Cic.Implicit None *)
527 if pos = Utils.Left then l,r else r,l
530 CicSubstitution.subst (Cic.Implicit None) t <>
531 CicSubstitution.subst (Cic.Rel 1) t
534 |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
535 let third = CicSubstitution.subst (Cic.Implicit None) third in
536 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
537 let uri_sym = LibraryObjects.sym_eq_URI ~eq in
538 mk_trans uri_trans ty other what third
539 (mk_sym uri_sym ty what other p2) p1
540 |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right ->
541 let third = CicSubstitution.subst (Cic.Implicit None) third in
542 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
543 mk_trans uri_trans ty other what third p2 p1
544 |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left ->
545 let third = CicSubstitution.subst (Cic.Implicit None) third in
546 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
547 mk_trans uri_trans ty third what other p1 p2
548 |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right ->
549 let third = CicSubstitution.subst (Cic.Implicit None) third in
550 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
551 let uri_sym = LibraryObjects.sym_eq_URI ~eq in
552 mk_trans uri_trans ty third what other p1
553 (mk_sym uri_sym ty other what p2)
554 | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs
556 let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
557 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
558 let pred_of t = CicSubstitution.subst t lhs in
559 let pred_of_what = pred_of what in
560 let pred_of_other = pred_of other in
562 * ====================================
563 * inject p2: P(what) = P(other)
565 let rec inject ty lhs what other p2 =
567 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
568 when LibraryObjects.is_trans_eq_URI uri_trans ->
569 let ty,l,m,r,plm,pmr = open_trans ens tl in
570 mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
571 (inject ty lhs m r pmr) (inject ty lhs l m plm)
573 let liftedty = CicSubstitution.lift 1 ty in
574 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
576 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
578 (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
579 (Cic.Lambda (Cic.Name "foo",ty,
581 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
582 refl_eq_part what p2)
584 mk_trans uri_trans ty pred_of_other pred_of_what rhs
585 (inject ty lhs what other p2) p1
586 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
588 let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
589 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
590 let pred_of t = CicSubstitution.subst t lhs in
591 let pred_of_what = pred_of what in
592 let pred_of_other = pred_of other in
594 * ====================================
595 * inject p2: P(what) = P(other)
597 let rec inject ty lhs what other p2 =
599 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
600 when LibraryObjects.is_trans_eq_URI uri_trans ->
601 let ty,l,m,r,plm,pmr = open_trans ens tl in
602 mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
603 (inject ty lhs m l plm)
604 (inject ty lhs r m pmr)
606 let liftedty = CicSubstitution.lift 1 ty in
607 let lifted_pred_of_other =
608 CicSubstitution.lift 1 (pred_of other) in
610 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
612 mk_eq_ind (Utils.eq_ind_URI ()) ty other
613 (Cic.Lambda (Cic.Name "foo",ty,
615 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
618 mk_trans uri_trans ty pred_of_other pred_of_what rhs
619 (inject ty lhs what other p2) p1
620 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
622 let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
623 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
624 let pred_of t = CicSubstitution.subst t rhs in
625 let pred_of_what = pred_of what in
626 let pred_of_other = pred_of other in
628 * ====================================
629 * inject p2: P(what) = P(other)
631 let rec inject ty lhs what other p2 =
633 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
634 when LibraryObjects.is_trans_eq_URI uri_trans ->
635 let ty,l,m,r,plm,pmr = open_trans ens tl in
636 mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
637 (inject ty lhs m r pmr)
638 (inject ty lhs l m plm)
640 let liftedty = CicSubstitution.lift 1 ty in
641 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
643 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
645 (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
646 (Cic.Lambda (Cic.Name "foo",ty,
648 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
649 refl_eq_part what p2)
651 mk_trans uri_trans ty lhs pred_of_what pred_of_other
652 p1 (inject ty rhs other what p2)
653 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
655 let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
656 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
657 let pred_of t = CicSubstitution.subst t rhs in
658 let pred_of_what = pred_of what in
659 let pred_of_other = pred_of other in
661 * ====================================
662 * inject p2: P(what) = P(other)
664 let rec inject ty lhs what other p2 =
666 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
667 when LibraryObjects.is_trans_eq_URI uri_trans ->
668 let ty,l,m,r,plm,pmr = open_trans ens tl in
669 (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
670 (inject ty lhs m l plm)
671 (inject ty lhs r m pmr))
673 let liftedty = CicSubstitution.lift 1 ty in
674 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
676 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
678 mk_eq_ind (Utils.eq_ind_URI ()) ty other
679 (Cic.Lambda (Cic.Name "foo",ty,
681 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
684 mk_trans uri_trans ty lhs pred_of_what pred_of_other
685 p1 (inject ty rhs other what p2)
687 mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
689 mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
692 let build_proof_term_new proof =
693 let rec aux = function
695 | Step (subst,(_, id1, (pos,id2), pred)) ->
696 let p,_,_ = proof_of_id id1 in
698 let p,l,r = proof_of_id id2 in
700 build_proof_step subst p1 p2 pos l r pred
707 let p,_,_ = proof_of_id id in
709 | Exact _ -> id :: acc
710 | Step (_,(_,id1, (_,id2), _)) ->
711 let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
712 let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
715 List.fold_left (fun acc (_,id,_,_) -> aux acc id) [] goalproof
718 let string_of_id names id =
720 let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
723 Printf.sprintf "%d = %s: %s = %s" id
724 (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
725 | Step (_,(step,id1, (_,id2), _) ) ->
726 Printf.sprintf "%5d: %s %4d %4d %s = %s" id
727 (if step = SuperpositionRight then "SupR" else "Demo")
728 id1 id2 (CicPp.pp l names) (CicPp.pp r names)
730 Not_found -> assert false
732 let pp_proof names goalproof =
733 String.concat "\n" (List.map (string_of_id names) (wfo goalproof))
735 let build_goal_proof l initial =
738 (fun current_proof (pos,id,subst,pred) ->
739 let p,l,r = proof_of_id id in
740 let p = build_proof_term_new p in
741 let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
742 build_proof_step subst current_proof p pos l r pred)
748 let refl_proof ty term =
751 (LibraryObjects.eq_URI (), 0, 1, []);
755 let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
757 let relocate newmeta menv =
758 let subst, metasenv, newmeta =
760 (fun (i, context, ty) (subst, menv, maxmeta) ->
762 CicMkImplicit.identity_relocation_list_for_metavariable context *)
764 let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
765 let newmeta = maxmeta, context, ty in
766 newsubst, newmeta::menv, maxmeta+1)
767 menv ([], [], newmeta+1)
769 let metasenv = apply_subst_metasenv subst metasenv in
770 let subst = flatten_subst subst in
771 subst, metasenv, newmeta
774 let fix_metas newmeta eq =
775 let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in
778 fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
779 prerr_endline (string_of_equality eq); *)
780 let subst, metasenv, newmeta = relocate newmeta menv in
781 let ty = apply_subst subst ty in
782 let left = apply_subst subst left in
783 let right = apply_subst subst right in
784 let fix_proof = function
786 | BasicProof (subst',term) -> BasicProof (subst@subst',term)
787 | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
791 (fun (i, (context, term, ty)) ->
792 let context = apply_subst_context subst context in
793 let term = apply_subst subst term in
794 let ty = apply_subst subst ty in
795 (i, (context, term, ty))) subst' in *)
796 ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
799 let fix_new_proof = function
800 | Exact p -> Exact (apply_subst subst p)
801 | Step (s,(r,id1,(pos,id2),pred)) ->
802 Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
804 let new_p = fix_new_proof p1 in
805 let old_p = fix_proof p2 in
806 let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in
807 (* debug prerr_endline (string_of_equality eq); *)
810 exception NotMetaConvertible;;
812 let meta_convertibility_aux table t1 t2 =
813 let module C = Cic in
814 let rec aux ((table_l, table_r) as table) t1 t2 =
816 | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
817 let m1_binding, table_l =
818 try List.assoc m1 table_l, table_l
819 with Not_found -> m2, (m1, m2)::table_l
820 and m2_binding, table_r =
821 try List.assoc m2 table_r, table_r
822 with Not_found -> m1, (m2, m1)::table_r
824 if (m1_binding <> m2) || (m2_binding <> m1) then
825 raise NotMetaConvertible
831 | None, Some _ | Some _, None -> raise NotMetaConvertible
833 | Some t1, Some t2 -> (aux res t1 t2))
834 (table_l, table_r) tl1 tl2
835 with Invalid_argument _ ->
836 raise NotMetaConvertible
838 | C.Var (u1, ens1), C.Var (u2, ens2)
839 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
840 aux_ens table ens1 ens2
841 | C.Cast (s1, t1), C.Cast (s2, t2)
842 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
843 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
844 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
845 let table = aux table s1 s2 in
847 | C.Appl l1, C.Appl l2 -> (
848 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
849 with Invalid_argument _ -> raise NotMetaConvertible
851 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
852 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
853 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
854 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
855 aux_ens table ens1 ens2
856 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
857 when (UriManager.eq u1 u2) && i1 = i2 ->
858 let table = aux table s1 s2 in
859 let table = aux table t1 t2 in (
860 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
861 with Invalid_argument _ -> raise NotMetaConvertible
863 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
866 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
867 if i1 <> i2 then raise NotMetaConvertible
869 let res = (aux res s1 s2) in aux res t1 t2)
871 with Invalid_argument _ -> raise NotMetaConvertible
873 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
876 (fun res (n1, s1, t1) (n2, s2, t2) ->
877 let res = aux res s1 s2 in aux res t1 t2)
879 with Invalid_argument _ -> raise NotMetaConvertible
881 | t1, t2 when t1 = t2 -> table
882 | _, _ -> raise NotMetaConvertible
884 and aux_ens table ens1 ens2 =
885 let cmp (u1, t1) (u2, t2) =
886 Pervasives.compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
888 let ens1 = List.sort cmp ens1
889 and ens2 = List.sort cmp ens2 in
892 (fun res (u1, t1) (u2, t2) ->
893 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
896 with Invalid_argument _ -> raise NotMetaConvertible
902 let meta_convertibility_eq eq1 eq2 =
903 let _, _, (ty, left, right, _), _,_ = open_equality eq1 in
904 let _, _, (ty', left', right', _), _,_ = open_equality eq2 in
907 else if (left = left') && (right = right') then
909 else if (left = right') && (right = left') then
913 let table = meta_convertibility_aux ([], []) left left' in
914 let _ = meta_convertibility_aux table right right' in
916 with NotMetaConvertible ->
918 let table = meta_convertibility_aux ([], []) left right' in
919 let _ = meta_convertibility_aux table right left' in
921 with NotMetaConvertible ->
926 let meta_convertibility t1 t2 =
931 ignore(meta_convertibility_aux ([], []) t1 t2);
933 with NotMetaConvertible ->
937 exception TermIsNotAnEquality;;
939 let term_is_equality term =
940 let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
942 | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
946 let equality_of_term proof term =
947 let eq_uri = LibraryObjects.eq_URI () in
948 let iseq uri = UriManager.eq uri eq_uri in
950 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
951 let o = !Utils.compare_terms t1 t2 in
952 let stat = (ty,t1,t2,o) in
953 let w = Utils.compute_equality_weight stat in
954 let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in
957 raise TermIsNotAnEquality
960 let is_weak_identity eq =
961 let _,_,(_,left, right,_),_,_ = open_equality eq in
962 left = right || meta_convertibility left right
965 let is_identity (_, context, ugraph) eq =
966 let _,_,(ty,left,right,_),menv,_ = open_equality eq in
968 (* (meta_convertibility left right)) *)
969 fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
973 let term_of_equality equality =
974 let _, _, (ty, left, right, _), menv, _= open_equality equality in
975 let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
976 let argsno = List.length menv in
978 CicSubstitution.lift argsno
979 (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
983 (fun (i,_,ty) (n, t) ->
984 let name = Cic.Name ("X" ^ (string_of_int n)) in
985 let ty = CicSubstitution.lift (n-1) ty in
987 ProofEngineReduction.replace
988 ~equality:eq ~what:[i]
989 ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
991 (n-1, Cic.Prod (name, ty, t)))