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 "flatten"
 454
 455 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
 456   let metasenv = metasenv1 @ metasenv2 in
 457   let subst, menv, ug =
 458     if not (is_simple_term t1) || not (is_simple_term t2) then (
 459       debug_print
 460         (lazy
 461            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
 462               (CicPp.ppterm t1) (CicPp.ppterm t2)));
 463       raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif"))
 464     ) else
 465       if b then
 466         (* full unification *)
 467         unification_simple [] metasenv context t1 t2 ugraph
 468       else
 469         (* matching: metasenv1 is locked *)
 470         unification_simple metasenv1 metasenv context t1 t2 ugraph
 471   in
 472   if Utils.debug_res then
 473             ignore(check_disjoint_invariant subst menv "unif");
 474   let flatten subst =
 475     List.map
 476       (fun (i, (context, term, ty)) ->
 477          let context = CicMetaSubst.apply_subst_context subst context in
 478          let term = CicMetaSubst.apply_subst subst term in
 479          let ty = CicMetaSubst.apply_subst subst ty in
 480            (i, (context, term, ty))) subst
 481   in
 482   let flatten subst = profiler.HExtlib.profile flatten subst in
 483   let subst = flatten subst in
 484     subst, menv, ug
 485 ;;
 486
 487 exception MatchingFailure;;
 488
 489 let matching1 metasenv1 metasenv2 context t1 t2 ugraph =
 490   try
 491     unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
 492   with
 493     CicUnification .UnificationFailure _ ->
 494       raise MatchingFailure
 495 ;;
 496
 497 let unification = unification_aux true
 498 ;;
 499
 500
 501
 502 (*
 503 let unification metasenv1 metasenv2 context t1 t2 ugraph =
 504   let (subst, metasenv, ugraph) =
 505     CicUnification.fo_unif (metasenv1@metasenv2) context t1 t2 ugraph in
 506   if Utils.debug_res then
 507             ignore(check_disjoint_invariant subst metasenv "fo_unif");
 508   (subst, metasenv, ugraph)
 509
 510 ;;
 511 *)
 512
 513
 514 (*
 515 let matching_simple metasenv context t1 t2 ugraph =
 516   let module C = Cic in
 517   let module M = CicMetaSubst in
 518   let module U = CicUnification in
 519   let lookup meta subst =
 520     match meta with
 521     | C.Meta (i, _) -> (
 522         try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
 523         with Not_found -> meta
 524       )
 525     | _ -> assert false
 526   in
 527   let rec do_match subst menv s t =
 528     match s, t with
 529     | s, t when s = t -> subst, menv
 530     | s, C.Meta (i, l) ->
 531         let filter_menv i menv =
 532           List.filter (fun (m, _, _) -> i <> m) menv
 533         in
 534         let subst, menv =
 535           let value = lookup t subst in
 536           match value with
 537           | value when value = t ->
 538               let _, _, ty = CicUtil.lookup_meta i menv in
 539               (i, (context, s, ty))::subst, filter_menv i menv
 540           | value when value <> s ->
 541               raise MatchingFailure
 542           | value -> do_match subst menv s value
 543         in
 544         subst, menv
 545     | C.Appl ls, C.Appl lt -> (
 546         try
 547           List.fold_left2
 548             (fun (subst, menv) s t -> do_match subst menv s t)
 549             (subst, menv) ls lt
 550         with Invalid_argument _ ->
 551           raise MatchingFailure
 552       )
 553     | _, _ ->
 554         raise MatchingFailure
 555   in
 556   let subst, menv = do_match [] metasenv t1 t2 in
 557   subst, menv, ugraph
 558 ;;
 559 *)
 560
 561 (*
 562 let matching metasenv context t1 t2 ugraph =
 563     try
 564       let subst, metasenv, ugraph =
 565         try
 566           unification metasenv context t1 t2 ugraph
 567         with CicUtil.Meta_not_found _ as exn ->
 568           Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
 569             (CicPp.ppterm t1) (CicPp.ppterm t2)
 570             (CicMetaSubst.ppmetasenv [] metasenv);
 571           raise exn
 572       in
 573       if Utils.debug_res then
 574             ignore(check_disjoint_invariant subst metasenv "qua-2");
 575       let t' = CicMetaSubst.apply_subst subst t1 in
 576       if not (meta_convertibility t1 t') then
 577         raise MatchingFailure
 578       else
 579         if Utils.debug_res then
 580             ignore(check_disjoint_invariant subst metasenv "qua-1");
 581         let metas = metas_of_term t1 in
 582         let subst =
 583           List.map
 584             (fun (i, (context, term, ty)) ->
 585                let context = CicMetaSubst.apply_subst_context subst context in
 586                let term = CicMetaSubst.apply_subst subst term in
 587                let ty = CicMetaSubst.apply_subst subst ty in
 588                  (i, (context, term, ty))) subst in
 589           if Utils.debug_res then
 590             ignore(check_disjoint_invariant subst metasenv "qua0");
 591
 592           let subst, metasenv =
 593           List.fold_left
 594             (fun
 595                (subst,metasenv) s ->
 596                  match s with
 597                    | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
 598                        let metasenv' =
 599                          List.filter (fun (x, _, _) -> x<>j) metasenv
 600                        in
 601                          ((j, (c, Cic.Meta (i, lc), ty))::subst,
 602                           (i,c,ty)::metasenv')
 603                    |_ -> s::subst,metasenv) ([],metasenv) subst
 604         in
 605         if Utils.debug_res then
 606           ignore(check_disjoint_invariant subst metasenv "qua1");
 607 (*
 608         let fix_subst = function
 609           | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
 610               (j, (c, Cic.Meta (i, lc), ty))
 611           | s -> s
 612         in
 613         let subst = List.map fix_subst subst in *)
 614         if CicMetaSubst.apply_subst subst t1 = t1 then
 615           subst, metasenv, ugraph
 616         else
 617           (prerr_endline "mah"; raise MatchingFailure)
 618     with
 619     | CicUnification.UnificationFailure _
 620     | CicUnification.Uncertain _ ->
 621       raise MatchingFailure
 622 ;;
 623 *)
 624
 625 (** matching takes in input the _disjoint_ metasenv of t1 and  t2;
 626 it perform unification in the union metasenv, then check that
 627 the first metasenv has not changed *)
 628
 629
 630 let matching2 metasenv1 metasenv2 context t1 t2 ugraph =
 631       let subst, metasenv, ugraph =
 632         try
 633           unification metasenv1 metasenv2 context t1 t2 ugraph
 634         with
 635             CicUtil.Meta_not_found _ as exn ->
 636               Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
 637                 (CicPp.ppterm t1) (CicPp.ppterm t2)
 638                 (CicMetaSubst.ppmetasenv [] (metasenv1@metasenv2));
 639               raise exn
 640           | CicUnification.UnificationFailure _
 641           | CicUnification.Uncertain _ ->
 642               raise MatchingFailure
 643       in
 644       if Utils.debug_res then
 645             ignore(check_disjoint_invariant subst metasenv "qua-2");
 646       (* let us unfold subst *)
 647       if metasenv = metasenv1 then
 648         let subst =
 649           List.map
 650             (fun (i, (context, term, ty)) ->
 651                let context = CicMetaSubst.apply_subst_context subst context in
 652                let term = CicMetaSubst.apply_subst subst term in
 653                let ty = CicMetaSubst.apply_subst subst ty in
 654                  (i, (context, term, ty))) subst in
 655           subst, metasenv, ugraph (* everything is fine *)
 656       else
 657         (* let us unfold subst *)
 658         (*
 659         let subst =
 660           List.map
 661             (fun (i, (context, term, ty)) ->
 662                let context = CicMetaSubst.apply_subst_context subst context in
 663                let term = CicMetaSubst.apply_subst subst term in
 664                let ty = CicMetaSubst.apply_subst subst ty in
 665                  (i, (context, term, ty))) subst in
 666         *)
 667           (* let us revert Meta-Meta in subst privileging metasenv1 *)
 668         let subst, metasenv =
 669           List.fold_left
 670             (fun
 671                (subst,metasenv) s ->
 672                  match s with
 673                    | (i, (c, Cic.Meta (j, lc), ty))
 674                        when (List.exists (fun (x, _, _)  -> x=i) metasenv1) &&
 675                          not (List.exists (fun (x, _)  -> x=j) subst) ->
 676                        let metasenv' =
 677                          List.filter (fun (x, _, _) -> x<>j) metasenv
 678                        in
 679                          ((j, (c, Cic.Meta (i, lc), ty))::subst,
 680                           (i,c,ty)::metasenv')
 681                    |_ -> s::subst,metasenv) ([],metasenv) subst
 682         in
 683         (* finally, let us chek again that metasenv = metasenv1 *)
 684         if metasenv = metasenv1 then
 685           subst, metasenv, ugraph
 686         else raise MatchingFailure
 687 ;;
 688
 689 (* debug
 690 let matching metasenv1 metasenv2 context t1 t2 ugraph =
 691   let rc1 =
 692     try Some (matching1 metasenv1 metasenv2 context t1 t2 ugraph)
 693     with MatchingFailure -> None
 694   in
 695   let rc2 =
 696     try
 697       Some (matching2 metasenv1 metasenv2 context t1 t2 ugraph)
 698     with MatchingFailure -> None
 699   in
 700   match rc1,rc2 with
 701   | Some (s,m,g) , None ->
 702       prerr_endline (CicPp.ppterm t1);
 703       prerr_endline (CicPp.ppterm t2);
 704       prerr_endline "SOLO NOI";
 705       prerr_endline (CicMetaSubst.ppsubst s);
 706       s,m,g
 707   | None , Some _ ->
 708       prerr_endline (CicPp.ppterm t1);
 709       prerr_endline (CicPp.ppterm t2);
 710       prerr_endline "SOLO LUI";
 711       assert false
 712   | None, None -> raise MatchingFailure
 713   | Some (s,m,g), Some (s',m',g') ->
 714       let s = List.sort (fun (i,_) (j,_) -> i - j) s in
 715       let s' = List.sort (fun (i,_) (j,_) -> i - j) s' in
 716       if s <> s' then
 717         begin
 718           prerr_endline (CicMetaSubst.ppsubst s);
 719           prerr_endline (CicMetaSubst.ppsubst s');
 720           prerr_endline (CicPp.ppterm t1);
 721           prerr_endline (CicPp.ppterm t2);
 722                 end;
 723       s,m,g
 724 *)
 725 let matching = matching1;;
 726
 727 let check_eq context msg eq =
 728   let w, proof, (eq_ty, left, right, order), metas = eq in
 729   if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
 730    (fst (CicTypeChecker.type_of_aux' metas context  left CicUniv.empty_ugraph))
 731    CicUniv.empty_ugraph))
 732   then
 733     begin
 734       prerr_endline msg;
 735       assert false;
 736     end
 737   else ()
 738 ;;
 739
 740 let find_equalities context proof =
 741   let module C = Cic in
 742   let module S = CicSubstitution in
 743   let module T = CicTypeChecker in
 744   let eq_uri = LibraryObjects.eq_URI () in
 745   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
 746   let ok_types ty menv =
 747     List.for_all (fun (_, _, mt) -> mt = ty) menv
 748   in
 749   let rec aux index newmeta = function
 750     | [] -> [], newmeta
 751     | (Some (_, C.Decl (term)))::tl ->
 752         let do_find context term =
 753           match term with
 754           | C.Prod (name, s, t) ->
 755               let (head, newmetas, args, newmeta) =
 756                 ProofEngineHelpers.saturate_term newmeta []
 757                   context (S.lift index term) 0
 758               in
 759               let p =
 760                 if List.length args = 0 then
 761                   C.Rel index
 762                 else
 763                   C.Appl ((C.Rel index)::args)
 764               in (
 765                 match head with
 766                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 767                     when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
 768                     debug_print
 769                       (lazy
 770                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 771                     let o = !Utils.compare_terms t1 t2 in
 772                     let stat = (ty,t1,t2,o) in
 773                     let w = compute_equality_weight stat in
 774                     let proof = BasicProof p in
 775                     let e = (w, proof, stat, newmetas) in
 776                     Some e, (newmeta+1)
 777                 | _ -> None, newmeta
 778               )
 779           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 780               when UriManager.eq uri eq_uri ->
 781               let ty = S.lift index ty in
 782               let t1 = S.lift index t1 in
 783               let t2 = S.lift index t2 in
 784               let o = !Utils.compare_terms t1 t2 in
 785               let stat = (ty,t1,t2,o) in
 786               let w = compute_equality_weight stat in
 787               let e = (w, BasicProof (C.Rel index), stat, []) in
 788               Some e, (newmeta+1)
 789           | _ -> None, newmeta
 790         in (
 791           match do_find context term with
 792           | Some p, newmeta ->
 793               let tl, newmeta' = (aux (index+1) newmeta tl) in
 794               if newmeta' < newmeta then
 795                 prerr_endline "big trouble";
 796               (index, p)::tl, newmeta' (* max???? *)
 797           | None, _ ->
 798               aux (index+1) newmeta tl
 799         )
 800     | _::tl ->
 801         aux (index+1) newmeta tl
 802   in
 803   let il, maxm = aux 1 newmeta context in
 804   let indexes, equalities = List.split il in
 805   ignore (List.iter (check_eq context "find") equalities);
 806   indexes, equalities, maxm
 807 ;;
 808
 809
 810 (*
 811 let equations_blacklist =
 812   List.fold_left
 813     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
 814     UriManager.UriSet.empty [
 815       "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
 816       "cic:/Coq/Init/Logic/trans_eq.con";
 817       "cic:/Coq/Init/Logic/f_equal.con";
 818       "cic:/Coq/Init/Logic/f_equal2.con";
 819       "cic:/Coq/Init/Logic/f_equal3.con";
 820       "cic:/Coq/Init/Logic/f_equal4.con";
 821       "cic:/Coq/Init/Logic/f_equal5.con";
 822       "cic:/Coq/Init/Logic/sym_eq.con";
 823       "cic:/Coq/Init/Logic/eq_ind.con";
 824       "cic:/Coq/Init/Logic/eq_ind_r.con";
 825       "cic:/Coq/Init/Logic/eq_rec.con";
 826       "cic:/Coq/Init/Logic/eq_rec_r.con";
 827       "cic:/Coq/Init/Logic/eq_rect.con";
 828       "cic:/Coq/Init/Logic/eq_rect_r.con";
 829       "cic:/Coq/Logic/Eqdep/UIP.con";
 830       "cic:/Coq/Logic/Eqdep/UIP_refl.con";
 831       "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
 832       "cic:/Coq/ZArith/Zcompare/rename.con";
 833       (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
 834          perche' questo cacchio di teorema rompe le scatole :'( *)
 835       "cic:/Rocq/SUBST/comparith/mult_n_2.con";
 836
 837       "cic:/matita/logic/equality/eq_f.con";
 838       "cic:/matita/logic/equality/eq_f2.con";
 839       "cic:/matita/logic/equality/eq_rec.con";
 840       "cic:/matita/logic/equality/eq_rect.con";
 841     ]
 842 ;;
 843 *)
 844 let equations_blacklist = UriManager.UriSet.empty;;
 845
 846
 847 let find_library_equalities dbd context status maxmeta =
 848   let module C = Cic in
 849   let module S = CicSubstitution in
 850   let module T = CicTypeChecker in
 851   let blacklist =
 852     List.fold_left
 853       (fun s u -> UriManager.UriSet.add u s)
 854       equations_blacklist
 855       [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 856        eq_ind_r_URI ()]
 857   in
 858   let candidates =
 859     List.fold_left
 860       (fun l uri ->
 861          if UriManager.UriSet.mem uri blacklist then
 862            l
 863          else
 864            let t = CicUtil.term_of_uri uri in
 865            let ty, _ =
 866              CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
 867            in
 868            (uri, t, ty)::l)
 869       []
 870       (let t1 = Unix.gettimeofday () in
 871        let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
 872        let t2 = Unix.gettimeofday () in
 873        (debug_print
 874           (lazy
 875              (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
 876                 (t2 -. t1))));
 877        eqs)
 878   in
 879   let eq_uri1 = eq_XURI ()
 880   and eq_uri2 = LibraryObjects.eq_URI () in
 881   let iseq uri =
 882     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
 883   in
 884   let ok_types ty menv =
 885     List.for_all (fun (_, _, mt) -> mt = ty) menv
 886   in
 887   let rec has_vars = function
 888     | C.Meta _ | C.Rel _ | C.Const _ -> false
 889     | C.Var _ -> true
 890     | C.Appl l -> List.exists has_vars l
 891     | C.Prod (_, s, t) | C.Lambda (_, s, t)
 892     | C.LetIn (_, s, t) | C.Cast (s, t) ->
 893         (has_vars s) || (has_vars t)
 894     | _ -> false
 895   in
 896   let rec aux newmeta = function
 897     | [] -> [], newmeta
 898     | (uri, term, termty)::tl ->
 899         debug_print
 900           (lazy
 901              (Printf.sprintf "Examining: %s (%s)"
 902                 (CicPp.ppterm term) (CicPp.ppterm termty)));
 903         let res, newmeta =
 904           match termty with
 905           | C.Prod (name, s, t) when not (has_vars termty) ->
 906               let head, newmetas, args, newmeta =
 907                 ProofEngineHelpers.saturate_term newmeta [] context termty 0
 908               in
 909               let p =
 910                 if List.length args = 0 then
 911                   term
 912                 else
 913                   C.Appl (term::args)
 914               in (
 915                 match head with
 916                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 917                     when (iseq uri) && (ok_types ty newmetas) ->
 918                     debug_print
 919                       (lazy
 920                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 921                     let o = !Utils.compare_terms t1 t2 in
 922                     let stat = (ty,t1,t2,o) in
 923                     let w = compute_equality_weight stat in
 924                     let proof = BasicProof p in
 925                     let e = (w, proof, stat, newmetas) in
 926                     Some e, (newmeta+1)
 927                 | _ -> None, newmeta
 928               )
 929           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 930               when iseq uri && not (has_vars termty) ->
 931               let o = !Utils.compare_terms t1 t2 in
 932               let stat = (ty,t1,t2,o) in
 933               let w = compute_equality_weight stat in
 934               let e = (w, BasicProof term, stat, []) in
 935               Some e, (newmeta+1)
 936           | _ -> None, newmeta
 937         in
 938         match res with
 939         | Some e ->
 940             let tl, newmeta' = aux newmeta tl in
 941               if newmeta' < newmeta then
 942                 prerr_endline "big trouble";
 943               (uri, e)::tl, newmeta' (* max???? *)
 944         | None ->
 945             aux newmeta tl
 946   in
 947   let found, maxm = aux maxmeta candidates in
 948   let uriset, eqlist =
 949     (List.fold_left
 950        (fun (s, l) (u, e) ->
 951           if List.exists (meta_convertibility_eq e) (List.map snd l) then (
 952             debug_print
 953               (lazy
 954                  (Printf.sprintf "NO!! %s already there!"
 955                     (string_of_equality e)));
 956             (UriManager.UriSet.add u s, l)
 957           ) else (UriManager.UriSet.add u s, (u, e)::l))
 958        (UriManager.UriSet.empty, []) found)
 959   in
 960   uriset, eqlist, maxm
 961 ;;
 962
 963
 964 let find_library_theorems dbd env status equalities_uris =
 965   let module C = Cic in
 966   let module S = CicSubstitution in
 967   let module T = CicTypeChecker in
 968   let blacklist =
 969     let refl_equal =
 970       UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
 971     let s =
 972       UriManager.UriSet.remove refl_equal
 973         (UriManager.UriSet.union equalities_uris equations_blacklist)
 974     in
 975     List.fold_left
 976       (fun s u -> UriManager.UriSet.add u s)
 977       s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 978          eq_ind_r_URI ()]
 979   in
 980   let metasenv, context, ugraph = env in
 981   let candidates =
 982     List.fold_left
 983       (fun l uri ->
 984          if UriManager.UriSet.mem uri blacklist then l
 985          else
 986            let t = CicUtil.term_of_uri uri in
 987            let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
 988            (t, ty, [])::l)
 989       [] (MetadataQuery.signature_of_goal ~dbd status)
 990   in
 991   let refl_equal =
 992     let u = eq_XURI () in
 993     let t = CicUtil.term_of_uri u in
 994     let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
 995     (t, ty, [])
 996   in
 997   refl_equal::candidates
 998 ;;
 999
1000
1001 let find_context_hypotheses env equalities_indexes =
1002   let metasenv, context, ugraph = env in
1003   let _, res =
1004     List.fold_left
1005       (fun (n, l) entry ->
1006          match entry with
1007          | None -> (n+1, l)
1008          | Some _ ->
1009              if List.mem n equalities_indexes then
1010                (n+1, l)
1011              else
1012                let t = Cic.Rel n in
1013                let ty, _ =
1014                  CicTypeChecker.type_of_aux' metasenv context t ugraph in
1015                (n+1, (t, ty, [])::l))
1016       (1, []) context
1017   in
1018   res
1019 ;;
1020
1021
1022 let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
1023   let table = Hashtbl.create (List.length args) in
1024
1025   let newargs, newmeta =
1026     List.fold_right
1027       (fun t (newargs, index) ->
1028          match t with
1029          | Cic.Meta (i, l) ->
1030              if Hashtbl.mem table i then
1031                let idx = Hashtbl.find table i in
1032                ((Cic.Meta (idx, l))::newargs, index+1)
1033              else
1034                let _ = Hashtbl.add table i index in
1035                ((Cic.Meta (index, l))::newargs, index+1)
1036          | _ -> assert false)
1037       args ([], newmeta+1)
1038   in
1039
1040   let repl where =
1041     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
1042       ~where
1043   in
1044   let menv' =
1045     List.fold_right
1046       (fun (i, context, term) menv ->
1047          try
1048            let index = Hashtbl.find table i in
1049            (index, context, term)::menv
1050          with Not_found ->
1051            (i, context, term)::menv)
1052       menv []
1053   in
1054   let ty = repl ty
1055   and left = repl left
1056   and right = repl right in
1057   let metas =
1058     (metas_of_term left) @
1059       (metas_of_term right) @
1060       (metas_of_term ty) @ (metas_of_proof p) in
1061   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
1062   let newargs =
1063     List.filter
1064       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
1065   in
1066   let _ =
1067     if List.length metas > 0 then
1068       let first = List.hd metas in
1069       (* this new equality might have less variables than its parents: here
1070          we fill the gap with a dummy arg. Example:
1071          with (f X Y) = X we can simplify
1072          (g X) = (f X Y) in
1073          (g X) = X.
1074          So the new equation has only one variable, but it still has type like
1075          \lambda X,Y:..., so we need to pass a dummy arg for Y
1076          (I hope this makes some sense...)
1077       *)
1078       Hashtbl.iter
1079         (fun k v ->
1080            if not (List.exists
1081                      (function Cic.Meta (i, _) -> i = v | _ -> assert false)
1082                      newargs) then
1083              Hashtbl.replace table k first)
1084         (Hashtbl.copy table)
1085   in
1086   let rec fix_proof = function
1087     | NoProof -> NoProof
1088     | BasicProof term -> BasicProof (repl term)
1089     | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
1090         let subst' =
1091           List.fold_left
1092             (fun s arg ->
1093                match arg with
1094                | Cic.Meta (i, l) -> (
1095                    try
1096                      let j = Hashtbl.find table i in
1097                      if List.mem_assoc i subst then
1098                        s
1099                      else
1100                        let _, context, ty = CicUtil.lookup_meta i menv in
1101                        (i, (context, Cic.Meta (j, l), ty))::s
1102                    with Not_found | CicUtil.Meta_not_found _ ->
1103                      s
1104                  )
1105                | _ -> assert false)
1106             [] args
1107         in
1108         ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
1109     | p -> assert false
1110   in
1111   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
1112   (newmeta +1, neweq)
1113 ;;
1114
1115
1116 let relocate newmeta menv =
1117   let subst, metasenv, newmeta =
1118     List.fold_right
1119       (fun (i, context, ty) (subst, menv, maxmeta) ->
1120         let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
1121         let newsubst = (i, (context, (Cic.Meta (maxmeta, irl)), ty)) in
1122         let newmeta = maxmeta, context, ty in
1123         newsubst::subst, newmeta::menv, maxmeta+1)
1124       menv ([], [], newmeta+1)
1125   in
1126   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1127   let subst =
1128     List.map
1129       (fun (i, (context, term, ty)) ->
1130          let context = CicMetaSubst.apply_subst_context subst context in
1131          let term = CicMetaSubst.apply_subst subst term in
1132          let ty = CicMetaSubst.apply_subst subst ty in
1133          (i, (context, term, ty))) subst in
1134   subst, metasenv, newmeta
1135
1136
1137 let fix_metas newmeta (w, p, (ty, left, right, o), menv) =
1138   (*
1139   let metas = (metas_of_term left)@(metas_of_term right)
1140     @(metas_of_term ty)@(metas_of_proof p) in
1141   let menv = List.filter (fun (i, _, _) -> List.mem i metas) menv in
1142   *)
1143   (* debug
1144   let _ , eq =
1145     fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
1146   prerr_endline (string_of_equality eq); *)
1147   let subst, metasenv, newmeta = relocate newmeta menv in
1148   let ty = CicMetaSubst.apply_subst subst ty in
1149   let left = CicMetaSubst.apply_subst subst left in
1150   let right = CicMetaSubst.apply_subst subst right in
1151   let rec fix_proof = function
1152     | NoProof -> NoProof
1153     | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
1154     | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
1155         (*
1156         let newsubst =
1157           List.map
1158             (fun (i, (context, term, ty)) ->
1159                let context = CicMetaSubst.apply_subst_context subst context in
1160                let term = CicMetaSubst.apply_subst subst term in
1161                let ty = CicMetaSubst.apply_subst subst ty in
1162                  (i, (context, term, ty))) subst' in *)
1163           ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
1164     | p -> assert false
1165   in
1166   let p = fix_proof p in
1167   (*
1168   let metas = (metas_of_term left)@(metas_of_term right)
1169     @(metas_of_term ty)@(metas_of_proof p) in
1170   let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
1171   *)
1172   let eq = (w, p, (ty, left, right, o), metasenv) in
1173   (* debug prerr_endline (string_of_equality eq); *)
1174   newmeta+1, eq
1175
1176 let term_is_equality term =
1177   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
1178   match term with
1179   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
1180   | _ -> false
1181 ;;
1182
1183
1184 exception TermIsNotAnEquality;;
1185
1186 let equality_of_term proof term =
1187   let eq_uri = LibraryObjects.eq_URI () in
1188   let iseq uri = UriManager.eq uri eq_uri in
1189   match term with
1190   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
1191       let o = !Utils.compare_terms t1 t2 in
1192       let stat = (ty,t1,t2,o) in
1193       let w = compute_equality_weight stat in
1194       let e = (w, BasicProof proof, stat, []) in
1195       e
1196   | _ ->
1197       raise TermIsNotAnEquality
1198 ;;
1199
1200
1201 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1202
1203 let is_weak_identity (metasenv, context, ugraph) = function
1204   | (_, _, (ty, left, right, _), menv) ->
1205        (left = right ||
1206           (meta_convertibility left right))
1207            (* the test below is not a good idea since it stops
1208               demodulation too early *)
1209            (* (fst (CicReduction.are_convertible
1210                   ~metasenv:(metasenv @ menv) context left right ugraph)))*)
1211 ;;
1212
1213 let is_identity (metasenv, context, ugraph) = function
1214   | (_, _, (ty, left, right, _), menv) ->
1215        (left = right ||
1216           (* (meta_convertibility left right)) *)
1217            (fst (CicReduction.are_convertible
1218                   ~metasenv:(metasenv @ menv) context left right ugraph)))
1219 ;;
1220
1221
1222 let term_of_equality equality =
1223   let _, _, (ty, left, right, _), menv = equality in
1224   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
1225   let argsno = List.length menv in
1226   let t =
1227     CicSubstitution.lift argsno
1228       (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
1229   in
1230   snd (
1231     List.fold_right
1232       (fun (i,_,ty) (n, t) ->
1233          let name = Cic.Name ("X" ^ (string_of_int n)) in
1234          let ty = CicSubstitution.lift (n-1) ty in
1235          let t =
1236            ProofEngineReduction.replace
1237              ~equality:eq ~what:[i]
1238              ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
1239          in
1240            (n-1, Cic.Prod (name, ty, t)))
1241       menv (argsno, t))
1242 ;;