components/tactics/paramodulation/inference.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   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.
   6  *
   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.
  11  *
  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.
  16  *
  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,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open Utils;;
  29
  30 let metas_of_proof_time = ref 0.;;
  31 let metas_of_term_time = ref 0.;;
  32
  33 type equality =
  34     int  *               (* weight *)
  35     proof *
  36     (Cic.term *          (* type *)
  37      Cic.term *          (* left side *)
  38      Cic.term *          (* right side *)
  39      Utils.comparison) * (* ordering *)
  40     Cic.metasenv        (* environment for metas *)
  41
  42 and proof =
  43   | NoProof (* term is the goal missing a proof *)
  44   | BasicProof of Cic.term
  45   | ProofBlock of
  46       Cic.substitution * UriManager.uri *
  47         (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
  48   | ProofGoalBlock of proof * proof
  49   | ProofSymBlock of Cic.term list * proof
  50   | SubProof of Cic.term * int * proof
  51 ;;
  52
  53 let string_of_equality ?env =
  54   match env with
  55   | None -> (
  56       function
  57         | w, _, (ty, left, right, o), _ ->
  58             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
  59               (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
  60     )
  61   | Some (_, context, _) -> (
  62       let names = names_of_context context in
  63       function
  64         | w, _, (ty, left, right, o), _ ->
  65             Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
  66               (CicPp.pp left names) (string_of_comparison o)
  67               (CicPp.pp right names)
  68     )
  69 ;;
  70
  71
  72 let rec string_of_proof = function
  73   | NoProof -> "NoProof "
  74   | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
  75   | SubProof (t, i, p) ->
  76       Printf.sprintf "SubProof(%s, %s, %s)"
  77         (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
  78   | ProofSymBlock _ -> "ProofSymBlock"
  79   | ProofBlock (subst, _, _, _ ,_,_) ->
  80       "ProofBlock" ^ (CicMetaSubst.ppsubst subst)
  81   | ProofGoalBlock (p1, p2) ->
  82       Printf.sprintf "ProofGoalBlock(%s, %s)"
  83         (string_of_proof p1) (string_of_proof p2)
  84 ;;
  85
  86
  87 let check_disjoint_invariant subst metasenv msg =
  88   if (List.exists
  89         (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
  90   then
  91     begin
  92       prerr_endline ("not disjoint: " ^ msg);
  93       assert false
  94     end
  95 ;;
  96
  97 (* filter out from metasenv the variables in substs *)
  98 let filter subst metasenv =
  99   List.filter
 100     (fun (m, _, _) ->
 101          try let _ = List.find (fun (i, _) -> m = i) subst in false
 102          with Not_found -> true)
 103     metasenv
 104 ;;
 105
 106 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
 107 let build_ens_for_sym_eq sym_eq_URI termlist =
 108   let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
 109   match obj with
 110   | Cic.Constant (_, _, _, uris, _) ->
 111       assert (List.length uris <= List.length termlist);
 112       let rec aux = function
 113         | [], tl -> [], tl
 114         | (uri::uris), (term::tl) ->
 115             let ens, args = aux (uris, tl) in
 116             (uri, term)::ens, args
 117         | _, _ -> assert false
 118       in
 119       aux (uris, termlist)
 120   | _ -> assert false
 121 ;;
 122
 123
 124 let build_proof_term ?(noproof=Cic.Implicit None) proof =
 125   let rec do_build_proof proof =
 126     match proof with
 127     | NoProof ->
 128         Printf.fprintf stderr "WARNING: no proof!\n";
 129         noproof
 130     | BasicProof term -> term
 131     | ProofGoalBlock (proofbit, proof) ->
 132         print_endline "found ProofGoalBlock, going up...";
 133         do_build_goal_proof proofbit proof
 134     | ProofSymBlock (termlist, proof) ->
 135         let proof = do_build_proof proof in
 136         let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
 137         Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
 138     | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
 139         let t' = Cic.Lambda (name, ty, bo) in
 140         let proof' =
 141           let _, proof', _, _ = eq in
 142           do_build_proof proof'
 143         in
 144         let eqproof = do_build_proof eqproof in
 145         let _, _, (ty, what, other, _), menv' = eq in
 146         let what, other =
 147           if pos = Utils.Left then what, other else other, what
 148         in
 149         CicMetaSubst.apply_subst subst
 150           (Cic.Appl [Cic.Const (eq_URI, []); ty;
 151                      what; t'; eqproof; other; proof'])
 152     | SubProof (term, meta_index, proof) ->
 153         let proof = do_build_proof proof in
 154         let eq i = function
 155           | Cic.Meta (j, _) -> i = j
 156           | _ -> false
 157         in
 158         ProofEngineReduction.replace
 159           ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
 160
 161   and do_build_goal_proof proofbit proof =
 162     match proof with
 163     | ProofGoalBlock (pb, p) ->
 164         do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
 165     | _ -> do_build_proof (replace_proof proofbit proof)
 166
 167   and replace_proof newproof = function
 168     | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
 169         let eqproof' = replace_proof newproof eqproof in
 170         ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
 171     | ProofGoalBlock (pb, p) ->
 172         let pb' = replace_proof newproof pb in
 173         ProofGoalBlock (pb', p)
 174     | BasicProof _ -> newproof
 175     | SubProof (term, meta_index, p) ->
 176         SubProof (term, meta_index, replace_proof newproof p)
 177     | p -> p
 178   in
 179   do_build_proof proof
 180 ;;
 181
 182
 183 let rec metas_of_term = function
 184   | Cic.Meta (i, c) -> [i]
 185   | Cic.Var (_, ens)
 186   | Cic.Const (_, ens)
 187   | Cic.MutInd (_, _, ens)
 188   | Cic.MutConstruct (_, _, _, ens) ->
 189       List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
 190   | Cic.Cast (s, t)
 191   | Cic.Prod (_, s, t)
 192   | Cic.Lambda (_, s, t)
 193   | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
 194   | Cic.Appl l -> List.flatten (List.map metas_of_term l)
 195   | Cic.MutCase (uri, i, s, t, l) ->
 196       (metas_of_term s) @ (metas_of_term t) @
 197         (List.flatten (List.map metas_of_term l))
 198   | Cic.Fix (i, il) ->
 199       List.flatten
 200         (List.map (fun (s, i, t1, t2) ->
 201                      (metas_of_term t1) @ (metas_of_term t2)) il)
 202   | Cic.CoFix (i, il) ->
 203       List.flatten
 204         (List.map (fun (s, t1, t2) ->
 205                      (metas_of_term t1) @ (metas_of_term t2)) il)
 206   | _ -> []
 207 ;;
 208
 209 let rec metas_of_proof p =
 210   if Utils.debug then
 211     let t1 = Unix.gettimeofday () in
 212     let res = metas_of_term (build_proof_term p) in
 213     let t2 = Unix.gettimeofday () in
 214     metas_of_proof_time := !metas_of_proof_time  +. (t2 -. t1);
 215     res
 216   else
 217     metas_of_term (build_proof_term p)
 218 ;;
 219
 220 exception NotMetaConvertible;;
 221
 222 let meta_convertibility_aux table t1 t2 =
 223   let module C = Cic in
 224   let rec aux ((table_l, table_r) as table) t1 t2 =
 225     match t1, t2 with
 226     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
 227         let m1_binding, table_l =
 228           try List.assoc m1 table_l, table_l
 229           with Not_found -> m2, (m1, m2)::table_l
 230         and m2_binding, table_r =
 231           try List.assoc m2 table_r, table_r
 232           with Not_found -> m1, (m2, m1)::table_r
 233         in
 234         if (m1_binding <> m2) || (m2_binding <> m1) then
 235           raise NotMetaConvertible
 236         else (
 237           try
 238             List.fold_left2
 239               (fun res t1 t2 ->
 240                  match t1, t2 with
 241                  | None, Some _ | Some _, None -> raise NotMetaConvertible
 242                  | None, None -> res
 243                  | Some t1, Some t2 -> (aux res t1 t2))
 244               (table_l, table_r) tl1 tl2
 245           with Invalid_argument _ ->
 246             raise NotMetaConvertible
 247         )
 248     | C.Var (u1, ens1), C.Var (u2, ens2)
 249     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
 250         aux_ens table ens1 ens2
 251     | C.Cast (s1, t1), C.Cast (s2, t2)
 252     | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
 253     | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
 254     | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
 255         let table = aux table s1 s2 in
 256         aux table t1 t2
 257     | C.Appl l1, C.Appl l2 -> (
 258         try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 259         with Invalid_argument _ -> raise NotMetaConvertible
 260       )
 261     | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
 262         when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
 263     | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
 264         when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
 265         aux_ens table ens1 ens2
 266     | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
 267         when (UriManager.eq u1 u2) && i1 = i2 ->
 268         let table = aux table s1 s2 in
 269         let table = aux table t1 t2 in (
 270           try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 271           with Invalid_argument _ -> raise NotMetaConvertible
 272         )
 273     | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
 274         try
 275           List.fold_left2
 276             (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
 277                if i1 <> i2 then raise NotMetaConvertible
 278                else
 279                  let res = (aux res s1 s2) in aux res t1 t2)
 280             table il1 il2
 281         with Invalid_argument _ -> raise NotMetaConvertible
 282       )
 283     | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
 284         try
 285           List.fold_left2
 286             (fun res (n1, s1, t1) (n2, s2, t2) ->
 287                let res = aux res s1 s2 in aux res t1 t2)
 288             table il1 il2
 289         with Invalid_argument _ -> raise NotMetaConvertible
 290       )
 291     | t1, t2 when t1 = t2 -> table
 292     | _, _ -> raise NotMetaConvertible
 293
 294   and aux_ens table ens1 ens2 =
 295     let cmp (u1, t1) (u2, t2) =
 296       compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
 297     in
 298     let ens1 = List.sort cmp ens1
 299     and ens2 = List.sort cmp ens2 in
 300     try
 301       List.fold_left2
 302         (fun res (u1, t1) (u2, t2) ->
 303            if not (UriManager.eq u1 u2) then raise NotMetaConvertible
 304            else aux res t1 t2)
 305         table ens1 ens2
 306     with Invalid_argument _ -> raise NotMetaConvertible
 307   in
 308   aux table t1 t2
 309 ;;
 310
 311
 312 let meta_convertibility_eq eq1 eq2 =
 313   let _, _, (ty, left, right, _), _ = eq1
 314   and _, _, (ty', left', right', _), _ = eq2 in
 315   if ty <> ty' then
 316     false
 317   else if (left = left') && (right = right') then
 318     true
 319   else if (left = right') && (right = left') then
 320     true
 321   else
 322     try
 323       let table = meta_convertibility_aux ([], []) left left' in
 324       let _ = meta_convertibility_aux table right right' in
 325       true
 326     with NotMetaConvertible ->
 327       try
 328         let table = meta_convertibility_aux ([], []) left right' in
 329         let _ = meta_convertibility_aux table right left' in
 330         true
 331       with NotMetaConvertible ->
 332         false
 333 ;;
 334
 335
 336 let meta_convertibility t1 t2 =
 337   if t1 = t2 then
 338     true
 339   else
 340     try
 341       ignore(meta_convertibility_aux ([], []) t1 t2);
 342       true
 343     with NotMetaConvertible ->
 344       false
 345 ;;
 346
 347
 348 let rec check_irl start = function
 349   | [] -> true
 350   | None::tl -> check_irl (start+1) tl
 351   | (Some (Cic.Rel x))::tl ->
 352       if x = start then check_irl (start+1) tl else false
 353   | _ -> false
 354 ;;
 355
 356
 357 let rec is_simple_term = function
 358   | Cic.Appl ((Cic.Meta _)::_) -> false
 359   | Cic.Appl l -> List.for_all is_simple_term l
 360   | Cic.Meta (i, l) -> check_irl 1 l
 361   | Cic.Rel _ -> true
 362   | Cic.Const _ -> true
 363   | Cic.MutInd (_, _, []) -> true
 364   | Cic.MutConstruct (_, _, _, []) -> true
 365   | _ -> false
 366 ;;
 367
 368
 369 let rec lookup_subst meta subst =
 370   match meta with
 371   | Cic.Meta (i, _) -> (
 372       try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst
 373       in lookup_subst t subst
 374       with Not_found -> meta
 375     )
 376   | _ -> meta
 377 ;;
 378
 379 let locked menv i =
 380   List.exists (fun (j,_,_) -> i = j) menv
 381 ;;
 382
 383 let unification_simple locked_menv metasenv context t1 t2 ugraph =
 384   let module C = Cic in
 385   let module M = CicMetaSubst in
 386   let module U = CicUnification in
 387   let lookup = lookup_subst in
 388   let rec occurs_check subst what where =
 389     match where with
 390     | t when what = t -> true
 391     | C.Appl l -> List.exists (occurs_check subst what) l
 392     | C.Meta _ ->
 393         let t = lookup where subst in
 394         if t <> where then occurs_check subst what t else false
 395     | _ -> false
 396   in
 397   let rec unif subst menv s t =
 398     let s = match s with C.Meta _ -> lookup s subst | _ -> s
 399     and t = match t with C.Meta _ -> lookup t subst | _ -> t
 400
 401     in
 402     match s, t with
 403     | s, t when s = t -> subst, menv
 404     | C.Meta (i, _), C.Meta (j, _)
 405         when (locked locked_menv i) &&(locked locked_menv j) ->
 406         raise
 407           (U.UnificationFailure (lazy "Inference.unification.unif"))
 408     | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) ->
 409         unif subst menv t s
 410     | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) ->
 411         unif subst menv t s
 412     | C.Meta _, t when occurs_check subst s t ->
 413         raise
 414           (U.UnificationFailure (lazy "Inference.unification.unif"))
 415     | C.Meta (i, l), t when (locked locked_menv i) ->
 416         raise
 417           (U.UnificationFailure (lazy "Inference.unification.unif"))
 418     | C.Meta (i, l), t -> (
 419         try
 420           let _, _, ty = CicUtil.lookup_meta i menv in
 421           assert (not (List.mem_assoc i subst));
 422           let subst = (i, (context, t, ty))::subst in
 423           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
 424           subst, menv
 425         with CicUtil.Meta_not_found m ->
 426           let names = names_of_context context in
 427           debug_print
 428             (lazy
 429                (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
 430                   (CicPp.pp t1 names) (CicPp.pp t2 names)
 431                   (print_metasenv menv) (print_metasenv metasenv)));
 432           assert false
 433       )
 434     | _, C.Meta _ -> unif subst menv t s
 435     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
 436         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 437     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
 438         try
 439           List.fold_left2
 440             (fun (subst', menv) s t -> unif subst' menv s t)
 441             (subst, menv) tls tlt
 442         with Invalid_argument _ ->
 443           raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 444       )
 445     | _, _ ->
 446         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 447   in
 448   let subst, menv = unif [] metasenv t1 t2 in
 449   let menv = filter subst menv in
 450   List.rev subst, menv, ugraph
 451 ;;
 452
 453 let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
 454 let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]"
 455 let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
 456 let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 457
 458 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
 459   let metasenv = metasenv1 @ metasenv2 in
 460   let subst, menv, ug =
 461     if not (is_simple_term t1) || not (is_simple_term t2) then (
 462       debug_print
 463         (lazy
 464            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
 465               (CicPp.ppterm t1) (CicPp.ppterm t2)));
 466       raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif"))
 467     ) else
 468       if b then
 469         (* full unification *)
 470         unification_simple [] metasenv context t1 t2 ugraph
 471       else
 472         (* matching: metasenv1 is locked *)
 473         unification_simple metasenv1 metasenv context t1 t2 ugraph
 474   in
 475   if Utils.debug_res then
 476             ignore(check_disjoint_invariant subst menv "unif");
 477   let flatten subst =
 478     List.map
 479       (fun (i, (context, term, ty)) ->
 480          let context = CicMetaSubst.apply_subst_context subst context in
 481          let term = CicMetaSubst.apply_subst subst term in
 482          let ty = CicMetaSubst.apply_subst subst ty in
 483            (i, (context, term, ty))) subst
 484   in
 485   let flatten_fast subst =
 486     let resolve_meta (i, (context, term, ty)) subst =
 487             let term = CicMetaSubst.apply_subst subst term in
 488             let ty = CicMetaSubst.apply_subst subst ty in
 489              (i, (context, term, ty))
 490     in
 491     let resolve_meta t s = profiler3.HExtlib.profile (resolve_meta t) s in
 492     let filter j (i,_) = i <> j in
 493     let filter a b = profiler4.HExtlib.profile (filter a) b in
 494     List.fold_left
 495       (fun subst (j,(c,t,ty)) as s ->
 496         let s = resolve_meta s subst in
 497         s::(List.filter (filter j) subst))
 498       subst subst
 499   in
 500   (*let flatten subst = profiler.HExtlib.profile flatten subst in*)
 501   let flatten_fast subst = profiler2.HExtlib.profile flatten_fast subst in
 502   (*let subst = flatten subst in*)
 503 (*  let subst = flatten_fast subst in*)
 504     subst, menv, ug
 505 ;;
 506
 507 exception MatchingFailure;;
 508
 509 let matching1 metasenv1 metasenv2 context t1 t2 ugraph =
 510   try
 511     unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
 512   with
 513     CicUnification .UnificationFailure _ ->
 514       raise MatchingFailure
 515 ;;
 516
 517 let unification = unification_aux true
 518 ;;
 519
 520
 521
 522 (*
 523 let unification metasenv1 metasenv2 context t1 t2 ugraph =
 524   let (subst, metasenv, ugraph) =
 525     CicUnification.fo_unif (metasenv1@metasenv2) context t1 t2 ugraph in
 526   if Utils.debug_res then
 527             ignore(check_disjoint_invariant subst metasenv "fo_unif");
 528   (subst, metasenv, ugraph)
 529
 530 ;;
 531 *)
 532
 533
 534 (*
 535 let matching_simple metasenv context t1 t2 ugraph =
 536   let module C = Cic in
 537   let module M = CicMetaSubst in
 538   let module U = CicUnification in
 539   let lookup meta subst =
 540     match meta with
 541     | C.Meta (i, _) -> (
 542         try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
 543         with Not_found -> meta
 544       )
 545     | _ -> assert false
 546   in
 547   let rec do_match subst menv s t =
 548     match s, t with
 549     | s, t when s = t -> subst, menv
 550     | s, C.Meta (i, l) ->
 551         let filter_menv i menv =
 552           List.filter (fun (m, _, _) -> i <> m) menv
 553         in
 554         let subst, menv =
 555           let value = lookup t subst in
 556           match value with
 557           | value when value = t ->
 558               let _, _, ty = CicUtil.lookup_meta i menv in
 559               (i, (context, s, ty))::subst, filter_menv i menv
 560           | value when value <> s ->
 561               raise MatchingFailure
 562           | value -> do_match subst menv s value
 563         in
 564         subst, menv
 565     | C.Appl ls, C.Appl lt -> (
 566         try
 567           List.fold_left2
 568             (fun (subst, menv) s t -> do_match subst menv s t)
 569             (subst, menv) ls lt
 570         with Invalid_argument _ ->
 571           raise MatchingFailure
 572       )
 573     | _, _ ->
 574         raise MatchingFailure
 575   in
 576   let subst, menv = do_match [] metasenv t1 t2 in
 577   subst, menv, ugraph
 578 ;;
 579 *)
 580
 581 (*
 582 let matching metasenv context t1 t2 ugraph =
 583     try
 584       let subst, metasenv, ugraph =
 585         try
 586           unification metasenv context t1 t2 ugraph
 587         with CicUtil.Meta_not_found _ as exn ->
 588           Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
 589             (CicPp.ppterm t1) (CicPp.ppterm t2)
 590             (CicMetaSubst.ppmetasenv [] metasenv);
 591           raise exn
 592       in
 593       if Utils.debug_res then
 594             ignore(check_disjoint_invariant subst metasenv "qua-2");
 595       let t' = CicMetaSubst.apply_subst subst t1 in
 596       if not (meta_convertibility t1 t') then
 597         raise MatchingFailure
 598       else
 599         if Utils.debug_res then
 600             ignore(check_disjoint_invariant subst metasenv "qua-1");
 601         let metas = metas_of_term t1 in
 602         let subst =
 603           List.map
 604             (fun (i, (context, term, ty)) ->
 605                let context = CicMetaSubst.apply_subst_context subst context in
 606                let term = CicMetaSubst.apply_subst subst term in
 607                let ty = CicMetaSubst.apply_subst subst ty in
 608                  (i, (context, term, ty))) subst in
 609           if Utils.debug_res then
 610             ignore(check_disjoint_invariant subst metasenv "qua0");
 611
 612           let subst, metasenv =
 613           List.fold_left
 614             (fun
 615                (subst,metasenv) s ->
 616                  match s with
 617                    | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
 618                        let metasenv' =
 619                          List.filter (fun (x, _, _) -> x<>j) metasenv
 620                        in
 621                          ((j, (c, Cic.Meta (i, lc), ty))::subst,
 622                           (i,c,ty)::metasenv')
 623                    |_ -> s::subst,metasenv) ([],metasenv) subst
 624         in
 625         if Utils.debug_res then
 626           ignore(check_disjoint_invariant subst metasenv "qua1");
 627 (*
 628         let fix_subst = function
 629           | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
 630               (j, (c, Cic.Meta (i, lc), ty))
 631           | s -> s
 632         in
 633         let subst = List.map fix_subst subst in *)
 634         if CicMetaSubst.apply_subst subst t1 = t1 then
 635           subst, metasenv, ugraph
 636         else
 637           (prerr_endline "mah"; raise MatchingFailure)
 638     with
 639     | CicUnification.UnificationFailure _
 640     | CicUnification.Uncertain _ ->
 641       raise MatchingFailure
 642 ;;
 643 *)
 644
 645 (** matching takes in input the _disjoint_ metasenv of t1 and  t2;
 646 it perform unification in the union metasenv, then check that
 647 the first metasenv has not changed *)
 648
 649
 650 let matching2 metasenv1 metasenv2 context t1 t2 ugraph =
 651       let subst, metasenv, ugraph =
 652         try
 653           unification metasenv1 metasenv2 context t1 t2 ugraph
 654         with
 655             CicUtil.Meta_not_found _ as exn ->
 656               Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
 657                 (CicPp.ppterm t1) (CicPp.ppterm t2)
 658                 (CicMetaSubst.ppmetasenv [] (metasenv1@metasenv2));
 659               raise exn
 660           | CicUnification.UnificationFailure _
 661           | CicUnification.Uncertain _ ->
 662               raise MatchingFailure
 663       in
 664       if Utils.debug_res then
 665             ignore(check_disjoint_invariant subst metasenv "qua-2");
 666       (* let us unfold subst *)
 667       if metasenv = metasenv1 then
 668         let subst =
 669           List.map
 670             (fun (i, (context, term, ty)) ->
 671                let context = CicMetaSubst.apply_subst_context subst context in
 672                let term = CicMetaSubst.apply_subst subst term in
 673                let ty = CicMetaSubst.apply_subst subst ty in
 674                  (i, (context, term, ty))) subst in
 675           subst, metasenv, ugraph (* everything is fine *)
 676       else
 677         (* let us unfold subst *)
 678         (*
 679         let subst =
 680           List.map
 681             (fun (i, (context, term, ty)) ->
 682                let context = CicMetaSubst.apply_subst_context subst context in
 683                let term = CicMetaSubst.apply_subst subst term in
 684                let ty = CicMetaSubst.apply_subst subst ty in
 685                  (i, (context, term, ty))) subst in
 686         *)
 687           (* let us revert Meta-Meta in subst privileging metasenv1 *)
 688         let subst, metasenv =
 689           List.fold_left
 690             (fun
 691                (subst,metasenv) s ->
 692                  match s with
 693                    | (i, (c, Cic.Meta (j, lc), ty))
 694                        when (List.exists (fun (x, _, _)  -> x=i) metasenv1) &&
 695                          not (List.exists (fun (x, _)  -> x=j) subst) ->
 696                        let metasenv' =
 697                          List.filter (fun (x, _, _) -> x<>j) metasenv
 698                        in
 699                          ((j, (c, Cic.Meta (i, lc), ty))::subst,
 700                           (i,c,ty)::metasenv')
 701                    |_ -> s::subst,metasenv) ([],metasenv) subst
 702         in
 703         (* finally, let us chek again that metasenv = metasenv1 *)
 704         if metasenv = metasenv1 then
 705           subst, metasenv, ugraph
 706         else raise MatchingFailure
 707 ;;
 708
 709 (* debug
 710 let matching metasenv1 metasenv2 context t1 t2 ugraph =
 711   let rc1 =
 712     try Some (matching1 metasenv1 metasenv2 context t1 t2 ugraph)
 713     with MatchingFailure -> None
 714   in
 715   let rc2 =
 716     try
 717       Some (matching2 metasenv1 metasenv2 context t1 t2 ugraph)
 718     with MatchingFailure -> None
 719   in
 720   match rc1,rc2 with
 721   | Some (s,m,g) , None ->
 722       prerr_endline (CicPp.ppterm t1);
 723       prerr_endline (CicPp.ppterm t2);
 724       prerr_endline "SOLO NOI";
 725       prerr_endline (CicMetaSubst.ppsubst s);
 726       s,m,g
 727   | None , Some _ ->
 728       prerr_endline (CicPp.ppterm t1);
 729       prerr_endline (CicPp.ppterm t2);
 730       prerr_endline "SOLO LUI";
 731       assert false
 732   | None, None -> raise MatchingFailure
 733   | Some (s,m,g), Some (s',m',g') ->
 734       let s = List.sort (fun (i,_) (j,_) -> i - j) s in
 735       let s' = List.sort (fun (i,_) (j,_) -> i - j) s' in
 736       if s <> s' then
 737         begin
 738           prerr_endline (CicMetaSubst.ppsubst s);
 739           prerr_endline (CicMetaSubst.ppsubst s');
 740           prerr_endline (CicPp.ppterm t1);
 741           prerr_endline (CicPp.ppterm t2);
 742                 end;
 743       s,m,g
 744 *)
 745 let matching = matching1;;
 746
 747 let check_eq context msg eq =
 748   let w, proof, (eq_ty, left, right, order), metas = eq in
 749   if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
 750    (fst (CicTypeChecker.type_of_aux' metas context  left CicUniv.empty_ugraph))
 751    CicUniv.empty_ugraph))
 752   then
 753     begin
 754       prerr_endline msg;
 755       assert false;
 756     end
 757   else ()
 758 ;;
 759
 760 let find_equalities context proof =
 761   let module C = Cic in
 762   let module S = CicSubstitution in
 763   let module T = CicTypeChecker in
 764   let eq_uri = LibraryObjects.eq_URI () in
 765   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
 766   let ok_types ty menv =
 767     List.for_all (fun (_, _, mt) -> mt = ty) menv
 768   in
 769   let rec aux index newmeta = function
 770     | [] -> [], newmeta
 771     | (Some (_, C.Decl (term)))::tl ->
 772         let do_find context term =
 773           match term with
 774           | C.Prod (name, s, t) ->
 775               let (head, newmetas, args, newmeta) =
 776                 ProofEngineHelpers.saturate_term newmeta []
 777                   context (S.lift index term) 0
 778               in
 779               let p =
 780                 if List.length args = 0 then
 781                   C.Rel index
 782                 else
 783                   C.Appl ((C.Rel index)::args)
 784               in (
 785                 match head with
 786                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 787                     when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
 788                     debug_print
 789                       (lazy
 790                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 791                     let o = !Utils.compare_terms t1 t2 in
 792                     let stat = (ty,t1,t2,o) in
 793                     let w = compute_equality_weight stat in
 794                     let proof = BasicProof p in
 795                     let e = (w, proof, stat, newmetas) in
 796                     Some e, (newmeta+1)
 797                 | _ -> None, newmeta
 798               )
 799           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 800               when UriManager.eq uri eq_uri ->
 801               let ty = S.lift index ty in
 802               let t1 = S.lift index t1 in
 803               let t2 = S.lift index t2 in
 804               let o = !Utils.compare_terms t1 t2 in
 805               let stat = (ty,t1,t2,o) in
 806               let w = compute_equality_weight stat in
 807               let e = (w, BasicProof (C.Rel index), stat, []) in
 808               Some e, (newmeta+1)
 809           | _ -> None, newmeta
 810         in (
 811           match do_find context term with
 812           | Some p, newmeta ->
 813               let tl, newmeta' = (aux (index+1) newmeta tl) in
 814               if newmeta' < newmeta then
 815                 prerr_endline "big trouble";
 816               (index, p)::tl, newmeta' (* max???? *)
 817           | None, _ ->
 818               aux (index+1) newmeta tl
 819         )
 820     | _::tl ->
 821         aux (index+1) newmeta tl
 822   in
 823   let il, maxm = aux 1 newmeta context in
 824   let indexes, equalities = List.split il in
 825   ignore (List.iter (check_eq context "find") equalities);
 826   indexes, equalities, maxm
 827 ;;
 828
 829
 830 (*
 831 let equations_blacklist =
 832   List.fold_left
 833     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
 834     UriManager.UriSet.empty [
 835       "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
 836       "cic:/Coq/Init/Logic/trans_eq.con";
 837       "cic:/Coq/Init/Logic/f_equal.con";
 838       "cic:/Coq/Init/Logic/f_equal2.con";
 839       "cic:/Coq/Init/Logic/f_equal3.con";
 840       "cic:/Coq/Init/Logic/f_equal4.con";
 841       "cic:/Coq/Init/Logic/f_equal5.con";
 842       "cic:/Coq/Init/Logic/sym_eq.con";
 843       "cic:/Coq/Init/Logic/eq_ind.con";
 844       "cic:/Coq/Init/Logic/eq_ind_r.con";
 845       "cic:/Coq/Init/Logic/eq_rec.con";
 846       "cic:/Coq/Init/Logic/eq_rec_r.con";
 847       "cic:/Coq/Init/Logic/eq_rect.con";
 848       "cic:/Coq/Init/Logic/eq_rect_r.con";
 849       "cic:/Coq/Logic/Eqdep/UIP.con";
 850       "cic:/Coq/Logic/Eqdep/UIP_refl.con";
 851       "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
 852       "cic:/Coq/ZArith/Zcompare/rename.con";
 853       (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
 854          perche' questo cacchio di teorema rompe le scatole :'( *)
 855       "cic:/Rocq/SUBST/comparith/mult_n_2.con";
 856
 857       "cic:/matita/logic/equality/eq_f.con";
 858       "cic:/matita/logic/equality/eq_f2.con";
 859       "cic:/matita/logic/equality/eq_rec.con";
 860       "cic:/matita/logic/equality/eq_rect.con";
 861     ]
 862 ;;
 863 *)
 864 let equations_blacklist = UriManager.UriSet.empty;;
 865
 866
 867 let find_library_equalities dbd context status maxmeta =
 868   let module C = Cic in
 869   let module S = CicSubstitution in
 870   let module T = CicTypeChecker in
 871   let blacklist =
 872     List.fold_left
 873       (fun s u -> UriManager.UriSet.add u s)
 874       equations_blacklist
 875       [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 876        eq_ind_r_URI ()]
 877   in
 878   let candidates =
 879     List.fold_left
 880       (fun l uri ->
 881          if UriManager.UriSet.mem uri blacklist then
 882            l
 883          else
 884            let t = CicUtil.term_of_uri uri in
 885            let ty, _ =
 886              CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
 887            in
 888            (uri, t, ty)::l)
 889       []
 890       (let t1 = Unix.gettimeofday () in
 891        let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
 892        let t2 = Unix.gettimeofday () in
 893        (debug_print
 894           (lazy
 895              (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
 896                 (t2 -. t1))));
 897        eqs)
 898   in
 899   let eq_uri1 = eq_XURI ()
 900   and eq_uri2 = LibraryObjects.eq_URI () in
 901   let iseq uri =
 902     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
 903   in
 904   let ok_types ty menv =
 905     List.for_all (fun (_, _, mt) -> mt = ty) menv
 906   in
 907   let rec has_vars = function
 908     | C.Meta _ | C.Rel _ | C.Const _ -> false
 909     | C.Var _ -> true
 910     | C.Appl l -> List.exists has_vars l
 911     | C.Prod (_, s, t) | C.Lambda (_, s, t)
 912     | C.LetIn (_, s, t) | C.Cast (s, t) ->
 913         (has_vars s) || (has_vars t)
 914     | _ -> false
 915   in
 916   let rec aux newmeta = function
 917     | [] -> [], newmeta
 918     | (uri, term, termty)::tl ->
 919         debug_print
 920           (lazy
 921              (Printf.sprintf "Examining: %s (%s)"
 922                 (CicPp.ppterm term) (CicPp.ppterm termty)));
 923         let res, newmeta =
 924           match termty with
 925           | C.Prod (name, s, t) when not (has_vars termty) ->
 926               let head, newmetas, args, newmeta =
 927                 ProofEngineHelpers.saturate_term newmeta [] context termty 0
 928               in
 929               let p =
 930                 if List.length args = 0 then
 931                   term
 932                 else
 933                   C.Appl (term::args)
 934               in (
 935                 match head with
 936                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 937                     when (iseq uri) && (ok_types ty newmetas) ->
 938                     debug_print
 939                       (lazy
 940                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 941                     let o = !Utils.compare_terms t1 t2 in
 942                     let stat = (ty,t1,t2,o) in
 943                     let w = compute_equality_weight stat in
 944                     let proof = BasicProof p in
 945                     let e = (w, proof, stat, newmetas) in
 946                     Some e, (newmeta+1)
 947                 | _ -> None, newmeta
 948               )
 949           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 950               when iseq uri && not (has_vars termty) ->
 951               let o = !Utils.compare_terms t1 t2 in
 952               let stat = (ty,t1,t2,o) in
 953               let w = compute_equality_weight stat in
 954               let e = (w, BasicProof term, stat, []) in
 955               Some e, (newmeta+1)
 956           | _ -> None, newmeta
 957         in
 958         match res with
 959         | Some e ->
 960             let tl, newmeta' = aux newmeta tl in
 961               if newmeta' < newmeta then
 962                 prerr_endline "big trouble";
 963               (uri, e)::tl, newmeta' (* max???? *)
 964         | None ->
 965             aux newmeta tl
 966   in
 967   let found, maxm = aux maxmeta candidates in
 968   let uriset, eqlist =
 969     (List.fold_left
 970        (fun (s, l) (u, e) ->
 971           if List.exists (meta_convertibility_eq e) (List.map snd l) then (
 972             debug_print
 973               (lazy
 974                  (Printf.sprintf "NO!! %s already there!"
 975                     (string_of_equality e)));
 976             (UriManager.UriSet.add u s, l)
 977           ) else (UriManager.UriSet.add u s, (u, e)::l))
 978        (UriManager.UriSet.empty, []) found)
 979   in
 980   uriset, eqlist, maxm
 981 ;;
 982
 983
 984 let find_library_theorems dbd env status equalities_uris =
 985   let module C = Cic in
 986   let module S = CicSubstitution in
 987   let module T = CicTypeChecker in
 988   let blacklist =
 989     let refl_equal =
 990       UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
 991     let s =
 992       UriManager.UriSet.remove refl_equal
 993         (UriManager.UriSet.union equalities_uris equations_blacklist)
 994     in
 995     List.fold_left
 996       (fun s u -> UriManager.UriSet.add u s)
 997       s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 998          eq_ind_r_URI ()]
 999   in
1000   let metasenv, context, ugraph = env in
1001   let candidates =
1002     List.fold_left
1003       (fun l uri ->
1004          if UriManager.UriSet.mem uri blacklist then l
1005          else
1006            let t = CicUtil.term_of_uri uri in
1007            let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
1008            (t, ty, [])::l)
1009       [] (MetadataQuery.signature_of_goal ~dbd status)
1010   in
1011   let refl_equal =
1012     let u = eq_XURI () in
1013     let t = CicUtil.term_of_uri u in
1014     let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
1015     (t, ty, [])
1016   in
1017   refl_equal::candidates
1018 ;;
1019
1020
1021 let find_context_hypotheses env equalities_indexes =
1022   let metasenv, context, ugraph = env in
1023   let _, res =
1024     List.fold_left
1025       (fun (n, l) entry ->
1026          match entry with
1027          | None -> (n+1, l)
1028          | Some _ ->
1029              if List.mem n equalities_indexes then
1030                (n+1, l)
1031              else
1032                let t = Cic.Rel n in
1033                let ty, _ =
1034                  CicTypeChecker.type_of_aux' metasenv context t ugraph in
1035                (n+1, (t, ty, [])::l))
1036       (1, []) context
1037   in
1038   res
1039 ;;
1040
1041
1042 let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
1043   let table = Hashtbl.create (List.length args) in
1044
1045   let newargs, newmeta =
1046     List.fold_right
1047       (fun t (newargs, index) ->
1048          match t with
1049          | Cic.Meta (i, l) ->
1050              if Hashtbl.mem table i then
1051                let idx = Hashtbl.find table i in
1052                ((Cic.Meta (idx, l))::newargs, index+1)
1053              else
1054                let _ = Hashtbl.add table i index in
1055                ((Cic.Meta (index, l))::newargs, index+1)
1056          | _ -> assert false)
1057       args ([], newmeta+1)
1058   in
1059
1060   let repl where =
1061     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
1062       ~where
1063   in
1064   let menv' =
1065     List.fold_right
1066       (fun (i, context, term) menv ->
1067          try
1068            let index = Hashtbl.find table i in
1069            (index, context, term)::menv
1070          with Not_found ->
1071            (i, context, term)::menv)
1072       menv []
1073   in
1074   let ty = repl ty
1075   and left = repl left
1076   and right = repl right in
1077   let metas =
1078     (metas_of_term left) @
1079       (metas_of_term right) @
1080       (metas_of_term ty) @ (metas_of_proof p) in
1081   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
1082   let newargs =
1083     List.filter
1084       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
1085   in
1086   let _ =
1087     if List.length metas > 0 then
1088       let first = List.hd metas in
1089       (* this new equality might have less variables than its parents: here
1090          we fill the gap with a dummy arg. Example:
1091          with (f X Y) = X we can simplify
1092          (g X) = (f X Y) in
1093          (g X) = X.
1094          So the new equation has only one variable, but it still has type like
1095          \lambda X,Y:..., so we need to pass a dummy arg for Y
1096          (I hope this makes some sense...)
1097       *)
1098       Hashtbl.iter
1099         (fun k v ->
1100            if not (List.exists
1101                      (function Cic.Meta (i, _) -> i = v | _ -> assert false)
1102                      newargs) then
1103              Hashtbl.replace table k first)
1104         (Hashtbl.copy table)
1105   in
1106   let rec fix_proof = function
1107     | NoProof -> NoProof
1108     | BasicProof term -> BasicProof (repl term)
1109     | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
1110         let subst' =
1111           List.fold_left
1112             (fun s arg ->
1113                match arg with
1114                | Cic.Meta (i, l) -> (
1115                    try
1116                      let j = Hashtbl.find table i in
1117                      if List.mem_assoc i subst then
1118                        s
1119                      else
1120                        let _, context, ty = CicUtil.lookup_meta i menv in
1121                        (i, (context, Cic.Meta (j, l), ty))::s
1122                    with Not_found | CicUtil.Meta_not_found _ ->
1123                      s
1124                  )
1125                | _ -> assert false)
1126             [] args
1127         in
1128         ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
1129     | p -> assert false
1130   in
1131   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
1132   (newmeta +1, neweq)
1133 ;;
1134
1135
1136 let relocate newmeta menv =
1137   let subst, metasenv, newmeta =
1138     List.fold_right
1139       (fun (i, context, ty) (subst, menv, maxmeta) ->
1140         let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
1141         let newsubst = (i, (context, (Cic.Meta (maxmeta, irl)), ty)) in
1142         let newmeta = maxmeta, context, ty in
1143         newsubst::subst, newmeta::menv, maxmeta+1)
1144       menv ([], [], newmeta+1)
1145   in
1146   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1147   let subst =
1148     List.map
1149       (fun (i, (context, term, ty)) ->
1150          let context = CicMetaSubst.apply_subst_context subst context in
1151          let term = CicMetaSubst.apply_subst subst term in
1152          let ty = CicMetaSubst.apply_subst subst ty in
1153          (i, (context, term, ty))) subst in
1154   subst, metasenv, newmeta
1155
1156
1157 let fix_metas newmeta (w, p, (ty, left, right, o), menv) =
1158   (*
1159   let metas = (metas_of_term left)@(metas_of_term right)
1160     @(metas_of_term ty)@(metas_of_proof p) in
1161   let menv = List.filter (fun (i, _, _) -> List.mem i metas) menv in
1162   *)
1163   (* debug
1164   let _ , eq =
1165     fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
1166   prerr_endline (string_of_equality eq); *)
1167   let subst, metasenv, newmeta = relocate newmeta menv in
1168   let ty = CicMetaSubst.apply_subst subst ty in
1169   let left = CicMetaSubst.apply_subst subst left in
1170   let right = CicMetaSubst.apply_subst subst right in
1171   let rec fix_proof = function
1172     | NoProof -> NoProof
1173     | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
1174     | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
1175         (*
1176         let newsubst =
1177           List.map
1178             (fun (i, (context, term, ty)) ->
1179                let context = CicMetaSubst.apply_subst_context subst context in
1180                let term = CicMetaSubst.apply_subst subst term in
1181                let ty = CicMetaSubst.apply_subst subst ty in
1182                  (i, (context, term, ty))) subst' in *)
1183           ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
1184     | p -> assert false
1185   in
1186   let p = fix_proof p in
1187   (*
1188   let metas = (metas_of_term left)@(metas_of_term right)
1189     @(metas_of_term ty)@(metas_of_proof p) in
1190   let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
1191   *)
1192   let eq = (w, p, (ty, left, right, o), metasenv) in
1193   (* debug prerr_endline (string_of_equality eq); *)
1194   newmeta+1, eq
1195
1196 let term_is_equality term =
1197   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
1198   match term with
1199   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
1200   | _ -> false
1201 ;;
1202
1203
1204 exception TermIsNotAnEquality;;
1205
1206 let equality_of_term proof term =
1207   let eq_uri = LibraryObjects.eq_URI () in
1208   let iseq uri = UriManager.eq uri eq_uri in
1209   match term with
1210   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1211       let o = !Utils.compare_terms t1 t2 in
1212       let stat = (ty,t1,t2,o) in
1213       let w = compute_equality_weight stat in
1214       let e = (w, BasicProof proof, stat, []) in
1215       e
1216   | _ ->
1217       raise TermIsNotAnEquality
1218 ;;
1219
1220
1221 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1222
1223 let is_weak_identity (metasenv, context, ugraph) = function
1224   | (_, _, (ty, left, right, _), menv) ->
1225        (left = right ||
1226           (meta_convertibility left right))
1227            (* the test below is not a good idea since it stops
1228               demodulation too early *)
1229            (* (fst (CicReduction.are_convertible
1230                   ~metasenv:(metasenv @ menv) context left right ugraph)))*)
1231 ;;
1232
1233 let is_identity (metasenv, context, ugraph) = function
1234   | (_, _, (ty, left, right, _), menv) ->
1235        (left = right ||
1236           (* (meta_convertibility left right)) *)
1237            (fst (CicReduction.are_convertible
1238                   ~metasenv:(metasenv @ menv) context left right ugraph)))
1239 ;;
1240
1241
1242 let term_of_equality equality =
1243   let _, _, (ty, left, right, _), menv = equality in
1244   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
1245   let argsno = List.length menv in
1246   let t =
1247     CicSubstitution.lift argsno
1248       (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
1249   in
1250   snd (
1251     List.fold_right
1252       (fun (i,_,ty) (n, t) ->
1253          let name = Cic.Name ("X" ^ (string_of_int n)) in
1254          let ty = CicSubstitution.lift (n-1) ty in
1255          let t =
1256            ProofEngineReduction.replace
1257              ~equality:eq ~what:[i]
1258              ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
1259          in
1260            (n-1, Cic.Prod (name, ty, t)))
1261       menv (argsno, t))
1262 ;;