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 uri_sym = LibraryObjects.sym_eq_URI ~eq in
559 let pred_of t = CicSubstitution.subst t lhs in
560 let pred_of_what = pred_of what in
561 let pred_of_other = pred_of other in
563 * ====================================
564 * inject p2: P(what) = P(other)
566 let inject ty lhs what other p2 =
567 let liftedty = CicSubstitution.lift 1 ty in
568 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
570 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
572 mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
573 (Cic.Lambda (Cic.Name "foo",ty,
575 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
578 mk_trans uri_trans ty pred_of_other pred_of_what rhs
579 (mk_sym uri_sym ty pred_of_what pred_of_other
580 (inject ty lhs what other p2)
582 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
584 let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
585 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
586 let uri_sym = LibraryObjects.sym_eq_URI ~eq in
587 let pred_of t = CicSubstitution.subst t lhs in
588 let pred_of_what = pred_of what in
589 let pred_of_other = pred_of other in
591 * ====================================
592 * inject p2: P(what) = P(other)
594 let inject ty lhs what other p2 =
595 let liftedty = CicSubstitution.lift 1 ty in
596 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
598 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
600 mk_eq_ind (Utils.eq_ind_URI ()) ty other
601 (Cic.Lambda (Cic.Name "foo",ty,
603 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
606 mk_trans uri_trans ty pred_of_other pred_of_what rhs
607 (mk_sym uri_sym ty pred_of_other pred_of_what
608 (inject ty lhs what other p2)
610 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
612 let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
613 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
614 let uri_sym = LibraryObjects.sym_eq_URI ~eq in
615 let pred_of t = CicSubstitution.subst t rhs in
616 let pred_of_what = pred_of what in
617 let pred_of_other = pred_of other in
619 * ====================================
620 * inject p2: P(what) = P(other)
622 let inject ty lhs what other p2 =
623 let liftedty = CicSubstitution.lift 1 ty in
624 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
626 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
628 mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
629 (Cic.Lambda (Cic.Name "foo",ty,
631 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
634 mk_trans uri_trans ty lhs pred_of_what pred_of_other p1
635 (mk_sym uri_sym ty pred_of_what pred_of_other
636 (inject ty rhs other what p2))
637 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
639 let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
640 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
641 let uri_sym = LibraryObjects.sym_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 inject ty lhs what other p2 =
650 let liftedty = CicSubstitution.lift 1 ty in
651 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
653 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
655 mk_eq_ind (Utils.eq_ind_URI ()) ty other
656 (Cic.Lambda (Cic.Name "foo",ty,
658 [Cic.MutInd(eq,0,[]);liftedty;lhs;lifted_pred_of_other])))
661 mk_trans uri_trans ty lhs pred_of_what pred_of_other p1
662 (mk_sym uri_sym ty pred_of_other pred_of_what
663 (inject ty rhs other what p2))
665 mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
667 mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
670 let build_proof_term_new proof =
671 let rec aux = function
673 | Step (subst,(_, id1, (pos,id2), pred)) ->
674 let p,_,_ = proof_of_id id1 in
676 let p,l,r = proof_of_id id2 in
678 build_proof_step subst p1 p2 pos l r pred
682 let build_goal_proof l initial =
685 (fun current_proof (pos,id,subst,pred) ->
686 let p,l,r = proof_of_id id in
687 let p = build_proof_term_new p in
688 let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
689 build_proof_step subst current_proof p pos l r pred)
695 let refl_proof ty term =
698 (LibraryObjects.eq_URI (), 0, 1, []);
702 let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
704 let relocate newmeta menv =
705 let subst, metasenv, newmeta =
707 (fun (i, context, ty) (subst, menv, maxmeta) ->
709 CicMkImplicit.identity_relocation_list_for_metavariable context *)
711 let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
712 let newmeta = maxmeta, context, ty in
713 newsubst, newmeta::menv, maxmeta+1)
714 menv ([], [], newmeta+1)
716 let metasenv = apply_subst_metasenv subst metasenv in
717 let subst = flatten_subst subst in
718 subst, metasenv, newmeta
721 let fix_metas newmeta eq =
722 let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in
725 fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
726 prerr_endline (string_of_equality eq); *)
727 let subst, metasenv, newmeta = relocate newmeta menv in
728 let ty = apply_subst subst ty in
729 let left = apply_subst subst left in
730 let right = apply_subst subst right in
731 let fix_proof = function
733 | BasicProof (subst',term) -> BasicProof (subst@subst',term)
734 | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
738 (fun (i, (context, term, ty)) ->
739 let context = apply_subst_context subst context in
740 let term = apply_subst subst term in
741 let ty = apply_subst subst ty in
742 (i, (context, term, ty))) subst' in *)
743 ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
746 let fix_new_proof = function
747 | Exact p -> Exact (apply_subst subst p)
748 | Step (s,(r,id1,(pos,id2),pred)) ->
749 Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
751 let new_p = fix_new_proof p1 in
752 let old_p = fix_proof p2 in
753 let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in
754 (* debug prerr_endline (string_of_equality eq); *)
757 exception NotMetaConvertible;;
759 let meta_convertibility_aux table t1 t2 =
760 let module C = Cic in
761 let rec aux ((table_l, table_r) as table) t1 t2 =
763 | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
764 let m1_binding, table_l =
765 try List.assoc m1 table_l, table_l
766 with Not_found -> m2, (m1, m2)::table_l
767 and m2_binding, table_r =
768 try List.assoc m2 table_r, table_r
769 with Not_found -> m1, (m2, m1)::table_r
771 if (m1_binding <> m2) || (m2_binding <> m1) then
772 raise NotMetaConvertible
778 | None, Some _ | Some _, None -> raise NotMetaConvertible
780 | Some t1, Some t2 -> (aux res t1 t2))
781 (table_l, table_r) tl1 tl2
782 with Invalid_argument _ ->
783 raise NotMetaConvertible
785 | C.Var (u1, ens1), C.Var (u2, ens2)
786 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
787 aux_ens table ens1 ens2
788 | C.Cast (s1, t1), C.Cast (s2, t2)
789 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
790 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
791 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
792 let table = aux table s1 s2 in
794 | C.Appl l1, C.Appl l2 -> (
795 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
796 with Invalid_argument _ -> raise NotMetaConvertible
798 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
799 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
800 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
801 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
802 aux_ens table ens1 ens2
803 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
804 when (UriManager.eq u1 u2) && i1 = i2 ->
805 let table = aux table s1 s2 in
806 let table = aux table t1 t2 in (
807 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
808 with Invalid_argument _ -> raise NotMetaConvertible
810 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
813 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
814 if i1 <> i2 then raise NotMetaConvertible
816 let res = (aux res s1 s2) in aux res t1 t2)
818 with Invalid_argument _ -> raise NotMetaConvertible
820 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
823 (fun res (n1, s1, t1) (n2, s2, t2) ->
824 let res = aux res s1 s2 in aux res t1 t2)
826 with Invalid_argument _ -> raise NotMetaConvertible
828 | t1, t2 when t1 = t2 -> table
829 | _, _ -> raise NotMetaConvertible
831 and aux_ens table ens1 ens2 =
832 let cmp (u1, t1) (u2, t2) =
833 Pervasives.compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
835 let ens1 = List.sort cmp ens1
836 and ens2 = List.sort cmp ens2 in
839 (fun res (u1, t1) (u2, t2) ->
840 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
843 with Invalid_argument _ -> raise NotMetaConvertible
849 let meta_convertibility_eq eq1 eq2 =
850 let _, _, (ty, left, right, _), _,_ = open_equality eq1 in
851 let _, _, (ty', left', right', _), _,_ = open_equality eq2 in
854 else if (left = left') && (right = right') then
856 else if (left = right') && (right = left') then
860 let table = meta_convertibility_aux ([], []) left left' in
861 let _ = meta_convertibility_aux table right right' in
863 with NotMetaConvertible ->
865 let table = meta_convertibility_aux ([], []) left right' in
866 let _ = meta_convertibility_aux table right left' in
868 with NotMetaConvertible ->
873 let meta_convertibility t1 t2 =
878 ignore(meta_convertibility_aux ([], []) t1 t2);
880 with NotMetaConvertible ->
884 exception TermIsNotAnEquality;;
886 let term_is_equality term =
887 let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
889 | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
893 let equality_of_term proof term =
894 let eq_uri = LibraryObjects.eq_URI () in
895 let iseq uri = UriManager.eq uri eq_uri in
897 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
898 let o = !Utils.compare_terms t1 t2 in
899 let stat = (ty,t1,t2,o) in
900 let w = Utils.compute_equality_weight stat in
901 let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in
904 raise TermIsNotAnEquality
907 let is_weak_identity eq =
908 let _,_,(_,left, right,_),_,_ = open_equality eq in
909 left = right || meta_convertibility left right
912 let is_identity (_, context, ugraph) eq =
913 let _,_,(ty,left,right,_),menv,_ = open_equality eq in
915 (* (meta_convertibility left right)) *)
916 fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
920 let term_of_equality equality =
921 let _, _, (ty, left, right, _), menv, _= open_equality equality in
922 let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
923 let argsno = List.length menv in
925 CicSubstitution.lift argsno
926 (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
930 (fun (i,_,ty) (n, t) ->
931 let name = Cic.Name ("X" ^ (string_of_int n)) in
932 let ty = CicSubstitution.lift (n-1) ty in
934 ProofEngineReduction.replace
935 ~equality:eq ~what:[i]
936 ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
938 (n-1, Cic.Prod (name, ty, t)))