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 ppsubst = ppsubst ~names:[]
360 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
361 let build_ens uri termlist =
362 let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
364 | Cic.Constant (_, _, _, uris, _) ->
365 assert (List.length uris <= List.length termlist);
366 let rec aux = function
368 | (uri::uris), (term::tl) ->
369 let ens, args = aux (uris, tl) in
370 (uri, term)::ens, args
371 | _, _ -> assert false
377 let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
378 let rec do_build_proof proof =
381 Printf.fprintf stderr "WARNING: no proof!\n";
383 | BasicProof (s,term) -> apply_subst s term
384 | ProofGoalBlock (proofbit, proof) ->
385 print_endline "found ProofGoalBlock, going up...";
386 do_build_goal_proof proofbit proof
387 | ProofSymBlock (termlist, proof) ->
388 let proof = do_build_proof proof in
389 let ens, args = build_ens (Utils.sym_eq_URI ()) termlist in
390 Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
391 | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
392 let t' = Cic.Lambda (name, ty, bo) in
393 let _, (_,proof), (ty, what, other, _), menv',_ = open_equality eq in
394 let proof' = do_build_proof proof in
395 let eqproof = do_build_proof eqproof in
397 if pos = Utils.Left then what, other else other, what
400 (Cic.Appl [Cic.Const (eq_URI, []); ty;
401 what; t'; eqproof; other; proof'])
402 | SubProof (term, meta_index, proof) ->
403 let proof = do_build_proof proof in
405 | Cic.Meta (j, _) -> i = j
408 ProofEngineReduction.replace
409 ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
411 and do_build_goal_proof proofbit proof =
413 | ProofGoalBlock (pb, p) ->
414 do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
415 | _ -> do_build_proof (replace_proof proofbit proof)
417 and replace_proof newproof = function
418 | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
419 let eqproof' = replace_proof newproof eqproof in
420 ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
421 | ProofGoalBlock (pb, p) ->
422 let pb' = replace_proof newproof pb in
423 ProofGoalBlock (pb', p)
424 | BasicProof _ -> newproof
425 | SubProof (term, meta_index, p) ->
426 SubProof (term, meta_index, replace_proof newproof p)
432 let mk_sym uri ty t1 t2 p =
433 let ens, args = build_ens uri [ty;t1;t2;p] in
434 Cic.Appl (Cic.Const(uri, ens) :: args)
437 let mk_trans uri ty t1 t2 t3 p12 p23 =
438 let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in
439 Cic.Appl (Cic.Const (uri, ens) :: args)
442 let mk_eq_ind uri ty what pred p1 other p2 =
443 Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
446 let p_of_sym ens tl =
447 let args = List.map snd ens @ tl in
453 let open_trans ens tl =
454 let args = List.map snd ens @ tl in
456 | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2
461 let rec remove_refl t =
463 | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
464 when LibraryObjects.is_trans_eq_URI uri_trans ->
465 let ty,l,m,r,p1,p2 = open_trans ens tl in
467 | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 ->
469 | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] ->
471 | _ -> Cic.Appl (List.map remove_refl args))
472 | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
475 let rec canonical t =
477 | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
478 when LibraryObjects.is_sym_eq_URI uri_sym ->
479 (match p_of_sym ens tl with
480 | Cic.Appl ((Cic.Const(uri,ens))::tl)
481 when LibraryObjects.is_sym_eq_URI uri ->
482 canonical (p_of_sym ens tl)
483 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
484 when LibraryObjects.is_trans_eq_URI uri_trans ->
485 let ty,l,m,r,p1,p2 = open_trans ens tl in
486 mk_trans uri_trans ty r m l
487 (canonical (mk_sym uri_sym ty m r p2))
488 (canonical (mk_sym uri_sym ty l m p1))
489 | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl)
490 when LibraryObjects.is_eq_ind_URI uri_ind ||
491 LibraryObjects.is_eq_ind_r_URI uri_ind ->
492 let ty, what, pred, p1, other, p2 =
494 | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
499 | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
500 when LibraryObjects.is_eq_URI uri ->
502 (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
504 prerr_endline (CicPp.ppterm pred);
507 let l = CicSubstitution.subst what l in
508 let r = CicSubstitution.subst what r in
511 canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
512 | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
513 when LibraryObjects.is_eq_URI uri -> t
514 | _ -> Cic.Appl (List.map canonical args))
515 | Cic.Appl l -> Cic.Appl (List.map canonical l)
518 remove_refl (canonical t)
521 let build_proof_step subst p1 p2 pos l r pred =
522 let p1 = apply_subst subst p1 in
523 let p2 = apply_subst subst p2 in
524 let l = apply_subst subst l in
525 let r = apply_subst subst r in
526 let pred = apply_subst subst pred in
527 let ty,body = (* Cic.Implicit None *)
529 | Cic.Lambda (_,ty,body) -> ty,body
532 let what, other = (* Cic.Implicit None, Cic.Implicit None *)
533 if pos = Utils.Left then l,r else r,l
536 CicSubstitution.subst (Cic.Implicit None) t <>
537 CicSubstitution.subst (Cic.Rel 1) t
540 |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
541 let third = CicSubstitution.subst (Cic.Implicit None) third in
542 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
543 let uri_sym = LibraryObjects.sym_eq_URI ~eq in
544 mk_trans uri_trans ty other what third
545 (mk_sym uri_sym ty what other p2) p1
546 |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right ->
547 let third = CicSubstitution.subst (Cic.Implicit None) third in
548 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
549 mk_trans uri_trans ty other what third p2 p1
550 |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left ->
551 let third = CicSubstitution.subst (Cic.Implicit None) third in
552 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
553 mk_trans uri_trans ty third what other p1 p2
554 |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right ->
555 let third = CicSubstitution.subst (Cic.Implicit None) third in
556 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
557 let uri_sym = LibraryObjects.sym_eq_URI ~eq in
558 mk_trans uri_trans ty third what other p1
559 (mk_sym uri_sym ty other what p2)
560 | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs
562 let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
563 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
564 let pred_of t = CicSubstitution.subst t lhs in
565 let pred_of_what = pred_of what in
566 let pred_of_other = pred_of other in
568 * ====================================
569 * inject p2: P(what) = P(other)
571 let rec inject ty lhs what other p2 =
573 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
574 when LibraryObjects.is_trans_eq_URI uri_trans ->
575 let ty,l,m,r,plm,pmr = open_trans ens tl in
576 mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
577 (inject ty lhs m r pmr) (inject ty lhs l m plm)
579 let liftedty = CicSubstitution.lift 1 ty in
580 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
582 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
584 (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
585 (Cic.Lambda (Cic.Name "foo",ty,
587 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
588 refl_eq_part what p2)
590 mk_trans uri_trans ty pred_of_other pred_of_what rhs
591 (inject ty lhs what other p2) p1
592 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
594 let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
595 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
596 let pred_of t = CicSubstitution.subst t lhs in
597 let pred_of_what = pred_of what in
598 let pred_of_other = pred_of other in
600 * ====================================
601 * inject p2: P(what) = P(other)
603 let rec inject ty lhs what other p2 =
605 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
606 when LibraryObjects.is_trans_eq_URI uri_trans ->
607 let ty,l,m,r,plm,pmr = open_trans ens tl in
608 mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
609 (inject ty lhs m l plm)
610 (inject ty lhs r m pmr)
612 let liftedty = CicSubstitution.lift 1 ty in
613 let lifted_pred_of_other =
614 CicSubstitution.lift 1 (pred_of other) in
616 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
618 mk_eq_ind (Utils.eq_ind_URI ()) ty other
619 (Cic.Lambda (Cic.Name "foo",ty,
621 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
624 mk_trans uri_trans ty pred_of_other pred_of_what rhs
625 (inject ty lhs what other p2) p1
626 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
628 let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
629 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
630 let pred_of t = CicSubstitution.subst t rhs in
631 let pred_of_what = pred_of what in
632 let pred_of_other = pred_of other in
634 * ====================================
635 * inject p2: P(what) = P(other)
637 let rec inject ty lhs what other p2 =
639 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
640 when LibraryObjects.is_trans_eq_URI uri_trans ->
641 let ty,l,m,r,plm,pmr = open_trans ens tl in
642 mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
643 (inject ty lhs m r pmr)
644 (inject ty lhs l m plm)
646 let liftedty = CicSubstitution.lift 1 ty in
647 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
649 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
651 (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
652 (Cic.Lambda (Cic.Name "foo",ty,
654 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
655 refl_eq_part what p2)
657 mk_trans uri_trans ty lhs pred_of_what pred_of_other
658 p1 (inject ty rhs other what p2)
659 | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
661 let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
662 let uri_trans = LibraryObjects.trans_eq_URI ~eq in
663 let pred_of t = CicSubstitution.subst t rhs in
664 let pred_of_what = pred_of what in
665 let pred_of_other = pred_of other in
667 * ====================================
668 * inject p2: P(what) = P(other)
670 let rec inject ty lhs what other p2 =
672 | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
673 when LibraryObjects.is_trans_eq_URI uri_trans ->
674 let ty,l,m,r,plm,pmr = open_trans ens tl in
675 (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
676 (inject ty lhs m l plm)
677 (inject ty lhs r m pmr))
679 let liftedty = CicSubstitution.lift 1 ty in
680 let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
682 Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
684 mk_eq_ind (Utils.eq_ind_URI ()) ty other
685 (Cic.Lambda (Cic.Name "foo",ty,
687 [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
690 mk_trans uri_trans ty lhs pred_of_what pred_of_other
691 p1 (inject ty rhs other what p2)
693 mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
695 mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
698 let build_proof_term_new proof =
699 let rec aux = function
701 | Step (subst,(_, id1, (pos,id2), pred)) ->
702 let p,_,_ = proof_of_id id1 in
704 let p,l,r = proof_of_id id2 in
706 build_proof_step subst p1 p2 pos l r pred
713 let p,_,_ = proof_of_id id in
715 | Exact _ -> if (List.mem id acc) then acc else id :: acc
716 | Step (_,(_,id1, (_,id2), _)) ->
717 let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
718 let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
721 List.fold_left (fun acc (_,id,_,_) -> aux acc id) [] goalproof
724 let string_of_id names id =
726 let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
729 Printf.sprintf "%d = %s: %s = %s" id
730 (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
731 | Step (_,(step,id1, (_,id2), _) ) ->
732 Printf.sprintf "%6d: %s %6d %6d %s = %s" id
733 (if step = SuperpositionRight then "SupR" else "Demo")
734 id1 id2 (CicPp.pp l names) (CicPp.pp r names)
736 Not_found -> assert false
738 let pp_proof names goalproof =
739 String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) ^
740 "\ngoal is demodulated with " ^
742 ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
745 let build_goal_proof l initial =
748 (fun current_proof (pos,id,subst,pred) ->
749 let p,l,r = proof_of_id id in
750 let p = build_proof_term_new p in
751 let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
752 build_proof_step subst current_proof p pos l r pred)
758 let refl_proof ty term =
761 (LibraryObjects.eq_URI (), 0, 1, []);
765 let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
767 let relocate newmeta menv =
768 let subst, metasenv, newmeta =
770 (fun (i, context, ty) (subst, menv, maxmeta) ->
772 CicMkImplicit.identity_relocation_list_for_metavariable context *)
774 let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
775 let newmeta = maxmeta, context, ty in
776 newsubst, newmeta::menv, maxmeta+1)
777 menv ([], [], newmeta+1)
779 let metasenv = apply_subst_metasenv subst metasenv in
780 let subst = flatten_subst subst in
781 subst, metasenv, newmeta
784 let fix_metas newmeta eq =
785 let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in
788 fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
789 prerr_endline (string_of_equality eq); *)
790 let subst, metasenv, newmeta = relocate newmeta menv in
791 let ty = apply_subst subst ty in
792 let left = apply_subst subst left in
793 let right = apply_subst subst right in
794 let fix_proof = function
796 | BasicProof (subst',term) -> BasicProof (subst@subst',term)
797 | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
801 (fun (i, (context, term, ty)) ->
802 let context = apply_subst_context subst context in
803 let term = apply_subst subst term in
804 let ty = apply_subst subst ty in
805 (i, (context, term, ty))) subst' in *)
806 ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
809 let fix_new_proof = function
810 | Exact p -> Exact (apply_subst subst p)
811 | Step (s,(r,id1,(pos,id2),pred)) ->
812 Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
814 let new_p = fix_new_proof p1 in
815 let old_p = fix_proof p2 in
816 let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in
817 (* debug prerr_endline (string_of_equality eq); *)
820 exception NotMetaConvertible;;
822 let meta_convertibility_aux table t1 t2 =
823 let module C = Cic in
824 let rec aux ((table_l, table_r) as table) t1 t2 =
826 | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
827 let m1_binding, table_l =
828 try List.assoc m1 table_l, table_l
829 with Not_found -> m2, (m1, m2)::table_l
830 and m2_binding, table_r =
831 try List.assoc m2 table_r, table_r
832 with Not_found -> m1, (m2, m1)::table_r
834 if (m1_binding <> m2) || (m2_binding <> m1) then
835 raise NotMetaConvertible
841 | None, Some _ | Some _, None -> raise NotMetaConvertible
843 | Some t1, Some t2 -> (aux res t1 t2))
844 (table_l, table_r) tl1 tl2
845 with Invalid_argument _ ->
846 raise NotMetaConvertible
848 | C.Var (u1, ens1), C.Var (u2, ens2)
849 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
850 aux_ens table ens1 ens2
851 | C.Cast (s1, t1), C.Cast (s2, t2)
852 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
853 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
854 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
855 let table = aux table s1 s2 in
857 | C.Appl l1, C.Appl l2 -> (
858 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
859 with Invalid_argument _ -> raise NotMetaConvertible
861 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
862 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
863 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
864 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
865 aux_ens table ens1 ens2
866 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
867 when (UriManager.eq u1 u2) && i1 = i2 ->
868 let table = aux table s1 s2 in
869 let table = aux table t1 t2 in (
870 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
871 with Invalid_argument _ -> raise NotMetaConvertible
873 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
876 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
877 if i1 <> i2 then raise NotMetaConvertible
879 let res = (aux res s1 s2) in aux res t1 t2)
881 with Invalid_argument _ -> raise NotMetaConvertible
883 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
886 (fun res (n1, s1, t1) (n2, s2, t2) ->
887 let res = aux res s1 s2 in aux res t1 t2)
889 with Invalid_argument _ -> raise NotMetaConvertible
891 | t1, t2 when t1 = t2 -> table
892 | _, _ -> raise NotMetaConvertible
894 and aux_ens table ens1 ens2 =
895 let cmp (u1, t1) (u2, t2) =
896 Pervasives.compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
898 let ens1 = List.sort cmp ens1
899 and ens2 = List.sort cmp ens2 in
902 (fun res (u1, t1) (u2, t2) ->
903 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
906 with Invalid_argument _ -> raise NotMetaConvertible
912 let meta_convertibility_eq eq1 eq2 =
913 let _, _, (ty, left, right, _), _,_ = open_equality eq1 in
914 let _, _, (ty', left', right', _), _,_ = open_equality eq2 in
917 else if (left = left') && (right = right') then
919 else if (left = right') && (right = left') then
923 let table = meta_convertibility_aux ([], []) left left' in
924 let _ = meta_convertibility_aux table right right' in
926 with NotMetaConvertible ->
928 let table = meta_convertibility_aux ([], []) left right' in
929 let _ = meta_convertibility_aux table right left' in
931 with NotMetaConvertible ->
936 let meta_convertibility t1 t2 =
941 ignore(meta_convertibility_aux ([], []) t1 t2);
943 with NotMetaConvertible ->
947 exception TermIsNotAnEquality;;
949 let term_is_equality term =
950 let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
952 | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
956 let equality_of_term proof term =
957 let eq_uri = LibraryObjects.eq_URI () in
958 let iseq uri = UriManager.eq uri eq_uri in
960 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
961 let o = !Utils.compare_terms t1 t2 in
962 let stat = (ty,t1,t2,o) in
963 let w = Utils.compute_equality_weight stat in
964 let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in
967 raise TermIsNotAnEquality
970 let is_weak_identity eq =
971 let _,_,(_,left, right,_),_,_ = open_equality eq in
972 left = right || meta_convertibility left right
975 let is_identity (_, context, ugraph) eq =
976 let _,_,(ty,left,right,_),menv,_ = open_equality eq in
978 (* (meta_convertibility left right)) *)
979 fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
983 let term_of_equality equality =
984 let _, _, (ty, left, right, _), menv, _= open_equality equality in
985 let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
986 let argsno = List.length menv in
988 CicSubstitution.lift argsno
989 (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
993 (fun (i,_,ty) (n, t) ->
994 let name = Cic.Name ("X" ^ (string_of_int n)) in
995 let ty = CicSubstitution.lift (n-1) ty in
997 ProofEngineReduction.replace
998 ~equality:eq ~what:[i]
999 ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
1001 (n-1, Cic.Prod (name, ty, t)))