helm/ocaml/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
  31 type equality =
  32     int  *               (* weight *)
  33     proof *
  34     (Cic.term *          (* type *)
  35      Cic.term *          (* left side *)
  36      Cic.term *          (* right side *)
  37      Utils.comparison) * (* ordering *)
  38     Cic.metasenv *       (* environment for metas *)
  39     Cic.term list        (* arguments *)
  40
  41 and proof =
  42   | NoProof
  43   | BasicProof of Cic.term
  44   | ProofBlock of
  45       Cic.substitution * UriManager.uri *
  46         (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
  47   | ProofGoalBlock of proof * proof
  48   | ProofSymBlock of Cic.term list * proof
  49   | SubProof of Cic.term * int * proof
  50 ;;
  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 _ -> "ProofBlock"
  80   | ProofGoalBlock (p1, p2) ->
  81       Printf.sprintf "ProofGoalBlock(%s, %s)"
  82         (string_of_proof p1) (string_of_proof p2)
  83 ;;
  84
  85
  86 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
  87 let build_ens_for_sym_eq sym_eq_URI termlist =
  88   let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
  89   match obj with
  90   | Cic.Constant (_, _, _, uris, _) ->
  91       assert (List.length uris <= List.length termlist);
  92       let rec aux = function
  93         | [], tl -> [], tl
  94         | (uri::uris), (term::tl) ->
  95             let ens, args = aux (uris, tl) in
  96             (uri, term)::ens, args
  97         | _, _ -> assert false
  98       in
  99       aux (uris, termlist)
 100   | _ -> assert false
 101 ;;
 102
 103
 104 let build_proof_term proof =
 105   let rec do_build_proof proof =
 106     match proof with
 107     | NoProof ->
 108         Printf.fprintf stderr "WARNING: no proof!\n";
 109         Cic.Implicit None
 110     | BasicProof term -> term
 111     | ProofGoalBlock (proofbit, proof) ->
 112         print_endline "found ProofGoalBlock, going up...";
 113         do_build_goal_proof proofbit proof
 114     | ProofSymBlock (termlist, proof) ->
 115         let proof = do_build_proof proof in
 116         let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
 117         Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
 118     | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
 119         let t' = Cic.Lambda (name, ty, bo) in
 120         let proof' =
 121           let _, proof', _, _, _ = eq in
 122           do_build_proof proof'
 123         in
 124         let eqproof = do_build_proof eqproof in
 125         let _, _, (ty, what, other, _), menv', args' = eq in
 126         let what, other =
 127           if pos = Utils.Left then what, other else other, what
 128         in
 129         CicMetaSubst.apply_subst subst
 130           (Cic.Appl [Cic.Const (eq_URI, []); ty;
 131                      what; t'; eqproof; other; proof'])
 132     | SubProof (term, meta_index, proof) ->
 133         let proof = do_build_proof proof in
 134         let eq i = function
 135           | Cic.Meta (j, _) -> i = j
 136           | _ -> false
 137         in
 138         ProofEngineReduction.replace
 139           ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
 140
 141   and do_build_goal_proof proofbit proof =
 142     match proof with
 143     | ProofGoalBlock (pb, p) ->
 144         do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
 145     | _ -> do_build_proof (replace_proof proofbit proof)
 146
 147   and replace_proof newproof = function
 148     | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
 149         let eqproof' = replace_proof newproof eqproof in
 150         ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
 151     | ProofGoalBlock (pb, p) ->
 152         let pb' = replace_proof newproof pb in
 153         ProofGoalBlock (pb', p)
 154     | BasicProof _ -> newproof
 155     | SubProof (term, meta_index, p) ->
 156         SubProof (term, meta_index, replace_proof newproof p)
 157     | p -> p
 158   in
 159   do_build_proof proof
 160 ;;
 161
 162
 163 let rec metas_of_term = function
 164   | Cic.Meta (i, c) -> [i]
 165   | Cic.Var (_, ens)
 166   | Cic.Const (_, ens)
 167   | Cic.MutInd (_, _, ens)
 168   | Cic.MutConstruct (_, _, _, ens) ->
 169       List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
 170   | Cic.Cast (s, t)
 171   | Cic.Prod (_, s, t)
 172   | Cic.Lambda (_, s, t)
 173   | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
 174   | Cic.Appl l -> List.flatten (List.map metas_of_term l)
 175   | Cic.MutCase (uri, i, s, t, l) ->
 176       (metas_of_term s) @ (metas_of_term t) @
 177         (List.flatten (List.map metas_of_term l))
 178   | Cic.Fix (i, il) ->
 179       List.flatten
 180         (List.map (fun (s, i, t1, t2) ->
 181                      (metas_of_term t1) @ (metas_of_term t2)) il)
 182   | Cic.CoFix (i, il) ->
 183       List.flatten
 184         (List.map (fun (s, t1, t2) ->
 185                      (metas_of_term t1) @ (metas_of_term t2)) il)
 186   | _ -> []
 187 ;;
 188
 189
 190 exception NotMetaConvertible;;
 191
 192 let meta_convertibility_aux table t1 t2 =
 193   let module C = Cic in
 194   let print_table t =
 195     String.concat ", "
 196       (List.map
 197          (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
 198   in
 199   let rec aux ((table_l, table_r) as table) t1 t2 =
 200     match t1, t2 with
 201     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
 202         let m1_binding, table_l =
 203           try List.assoc m1 table_l, table_l
 204           with Not_found -> m2, (m1, m2)::table_l
 205         and m2_binding, table_r =
 206           try List.assoc m2 table_r, table_r
 207           with Not_found -> m1, (m2, m1)::table_r
 208         in
 209         if (m1_binding <> m2) || (m2_binding <> m1) then
 210           raise NotMetaConvertible
 211         else (
 212           try
 213             List.fold_left2
 214               (fun res t1 t2 ->
 215                  match t1, t2 with
 216                  | None, Some _ | Some _, None -> raise NotMetaConvertible
 217                  | None, None -> res
 218                  | Some t1, Some t2 -> (aux res t1 t2))
 219               (table_l, table_r) tl1 tl2
 220           with Invalid_argument _ ->
 221             raise NotMetaConvertible
 222         )
 223     | C.Var (u1, ens1), C.Var (u2, ens2)
 224     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
 225         aux_ens table ens1 ens2
 226     | C.Cast (s1, t1), C.Cast (s2, t2)
 227     | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
 228     | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
 229     | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
 230         let table = aux table s1 s2 in
 231         aux table t1 t2
 232     | C.Appl l1, C.Appl l2 -> (
 233         try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 234         with Invalid_argument _ -> raise NotMetaConvertible
 235       )
 236     | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
 237         when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
 238     | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
 239         when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
 240         aux_ens table ens1 ens2
 241     | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
 242         when (UriManager.eq u1 u2) && i1 = i2 ->
 243         let table = aux table s1 s2 in
 244         let table = aux table t1 t2 in (
 245           try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 246           with Invalid_argument _ -> raise NotMetaConvertible
 247         )
 248     | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
 249         try
 250           List.fold_left2
 251             (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
 252                if i1 <> i2 then raise NotMetaConvertible
 253                else
 254                  let res = (aux res s1 s2) in aux res t1 t2)
 255             table il1 il2
 256         with Invalid_argument _ -> raise NotMetaConvertible
 257       )
 258     | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
 259         try
 260           List.fold_left2
 261             (fun res (n1, s1, t1) (n2, s2, t2) ->
 262                let res = aux res s1 s2 in aux res t1 t2)
 263             table il1 il2
 264         with Invalid_argument _ -> raise NotMetaConvertible
 265       )
 266     | t1, t2 when t1 = t2 -> table
 267     | _, _ -> raise NotMetaConvertible
 268
 269   and aux_ens table ens1 ens2 =
 270     let cmp (u1, t1) (u2, t2) =
 271       compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
 272     in
 273     let ens1 = List.sort cmp ens1
 274     and ens2 = List.sort cmp ens2 in
 275     try
 276       List.fold_left2
 277         (fun res (u1, t1) (u2, t2) ->
 278            if not (UriManager.eq u1 u2) then raise NotMetaConvertible
 279            else aux res t1 t2)
 280         table ens1 ens2
 281     with Invalid_argument _ -> raise NotMetaConvertible
 282   in
 283   aux table t1 t2
 284 ;;
 285
 286
 287 let meta_convertibility_eq eq1 eq2 =
 288   let _, _, (ty, left, right, _), _, _ = eq1
 289   and _, _, (ty', left', right', _), _, _ = eq2 in
 290   if ty <> ty' then
 291     false
 292   else if (left = left') && (right = right') then
 293     true
 294   else if (left = right') && (right = left') then
 295     true
 296   else
 297     try
 298       let table = meta_convertibility_aux ([], []) left left' in
 299       let _ = meta_convertibility_aux table right right' in
 300       true
 301     with NotMetaConvertible ->
 302       try
 303         let table = meta_convertibility_aux ([], []) left right' in
 304         let _ = meta_convertibility_aux table right left' in
 305         true
 306       with NotMetaConvertible ->
 307         false
 308 ;;
 309
 310
 311 let meta_convertibility t1 t2 =
 312   let f t =
 313     String.concat ", "
 314       (List.map
 315          (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
 316   in
 317   if t1 = t2 then
 318     true
 319   else
 320     try
 321       let l, r = meta_convertibility_aux ([], []) t1 t2 in
 322       true
 323     with NotMetaConvertible ->
 324       false
 325 ;;
 326
 327
 328 let rec check_irl start = function
 329   | [] -> true
 330   | None::tl -> check_irl (start+1) tl
 331   | (Some (Cic.Rel x))::tl ->
 332       if x = start then check_irl (start+1) tl else false
 333   | _ -> false
 334 ;;
 335
 336
 337 let rec is_simple_term = function
 338   | Cic.Appl ((Cic.Meta _)::_) -> false
 339   | Cic.Appl l -> List.for_all is_simple_term l
 340   | Cic.Meta (i, l) -> check_irl 1 l
 341   | Cic.Rel _ -> true
 342   | Cic.Const _ -> true
 343   | Cic.MutInd (_, _, []) -> true
 344   | Cic.MutConstruct (_, _, _, []) -> true
 345   | _ -> false
 346 ;;
 347
 348
 349 let lookup_subst meta subst =
 350   match meta with
 351   | Cic.Meta (i, _) -> (
 352       try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
 353       with Not_found -> meta
 354     )
 355   | _ -> assert false
 356 ;;
 357
 358
 359 let unification_simple metasenv context t1 t2 ugraph =
 360   let module C = Cic in
 361   let module M = CicMetaSubst in
 362   let module U = CicUnification in
 363   let lookup = lookup_subst in
 364   let rec occurs_check subst what where =
 365     match where with
 366     | t when what = t -> true
 367     | C.Appl l -> List.exists (occurs_check subst what) l
 368     | C.Meta _ ->
 369         let t = lookup where subst in
 370         if t <> where then occurs_check subst what t else false
 371     | _ -> false
 372   in
 373   let rec unif subst menv s t =
 374     let s = match s with C.Meta _ -> lookup s subst | _ -> s
 375     and t = match t with C.Meta _ -> lookup t subst | _ -> t
 376     in
 377     match s, t with
 378     | s, t when s = t -> subst, menv
 379     | C.Meta (i, _), C.Meta (j, _) when i > j ->
 380         unif subst menv t s
 381     | C.Meta _, t when occurs_check subst s t ->
 382         raise
 383           (U.UnificationFailure (lazy "Inference.unification.unif"))
 384     | C.Meta (i, l), t -> (
 385         try
 386           let _, _, ty = CicUtil.lookup_meta i menv in
 387           let subst =
 388             if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
 389             else subst
 390           in
 391           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
 392           subst, menv
 393         with CicUtil.Meta_not_found m ->
 394           let names = names_of_context context in
 395           debug_print
 396             (lazy
 397                (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
 398                   (CicPp.pp t1 names) (CicPp.pp t2 names)
 399                   (print_metasenv menv) (print_metasenv metasenv)));
 400           assert false
 401       )
 402     | _, C.Meta _ -> unif subst menv t s
 403     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
 404         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 405     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
 406         try
 407           List.fold_left2
 408             (fun (subst', menv) s t -> unif subst' menv s t)
 409             (subst, menv) tls tlt
 410         with Invalid_argument _ ->
 411           raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 412       )
 413     | _, _ ->
 414         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
 415   in
 416   let subst, menv = unif [] metasenv t1 t2 in
 417   let menv =
 418     List.filter
 419       (fun (m, _, _) ->
 420          try let _ = List.find (fun (i, _) -> m = i) subst in false
 421          with Not_found -> true)
 422       menv
 423   in
 424   List.rev subst, menv, ugraph
 425 ;;
 426
 427
 428 let unification metasenv context t1 t2 ugraph =
 429   let subst, menv, ug =
 430     if not (is_simple_term t1) || not (is_simple_term t2) then (
 431       debug_print
 432         (lazy
 433            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
 434               (CicPp.ppterm t1) (CicPp.ppterm t2)));
 435       CicUnification.fo_unif metasenv context t1 t2 ugraph
 436     ) else
 437       unification_simple metasenv context t1 t2 ugraph
 438   in
 439   let rec fix_term = function
 440     | (Cic.Meta (i, l) as t) ->
 441         let t' = lookup_subst t subst in
 442         if t <> t' then fix_term t' else t
 443     | Cic.Appl l -> Cic.Appl (List.map fix_term l)
 444     | t -> t
 445   in
 446   let rec fix_subst = function
 447     | [] -> []
 448     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
 449   in
 450   fix_subst subst, menv, ug
 451 ;;
 452
 453
 454 let unification = CicUnification.fo_unif;;
 455
 456 exception MatchingFailure;;
 457
 458
 459 (*
 460 let matching_simple metasenv context t1 t2 ugraph =
 461   let module C = Cic in
 462   let module M = CicMetaSubst in
 463   let module U = CicUnification in
 464   let lookup meta subst =
 465     match meta with
 466     | C.Meta (i, _) -> (
 467         try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
 468         with Not_found -> meta
 469       )
 470     | _ -> assert false
 471   in
 472   let rec do_match subst menv s t =
 473     match s, t with
 474     | s, t when s = t -> subst, menv
 475     | s, C.Meta (i, l) ->
 476         let filter_menv i menv =
 477           List.filter (fun (m, _, _) -> i <> m) menv
 478         in
 479         let subst, menv =
 480           let value = lookup t subst in
 481           match value with
 482           | value when value = t ->
 483               let _, _, ty = CicUtil.lookup_meta i menv in
 484               (i, (context, s, ty))::subst, filter_menv i menv
 485           | value when value <> s ->
 486               raise MatchingFailure
 487           | value -> do_match subst menv s value
 488         in
 489         subst, menv
 490     | C.Appl ls, C.Appl lt -> (
 491         try
 492           List.fold_left2
 493             (fun (subst, menv) s t -> do_match subst menv s t)
 494             (subst, menv) ls lt
 495         with Invalid_argument _ ->
 496           raise MatchingFailure
 497       )
 498     | _, _ ->
 499         raise MatchingFailure
 500   in
 501   let subst, menv = do_match [] metasenv t1 t2 in
 502   subst, menv, ugraph
 503 ;;
 504 *)
 505
 506
 507 let matching metasenv context t1 t2 ugraph =
 508     try
 509       let subst, metasenv, ugraph =
 510 try
 511           unification metasenv context t1 t2 ugraph
 512 with CicUtil.Meta_not_found _ as exn ->
 513  Printf.eprintf "t1 = %s\nt2 = %s\nmetasenv = %s\n%!"
 514   (CicPp.ppterm t1) (CicPp.ppterm t2) (CicMetaSubst.ppmetasenv [] metasenv);
 515  raise exn
 516       in
 517       let t' = CicMetaSubst.apply_subst subst t1 in
 518       if not (meta_convertibility t1 t') then
 519         raise MatchingFailure
 520       else
 521         let metas = metas_of_term t1 in
 522         let fix_subst = function
 523           | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
 524               (j, (c, Cic.Meta (i, lc), ty))
 525           | s -> s
 526         in
 527         let subst = List.map fix_subst subst in
 528         subst, metasenv, ugraph
 529     with
 530     | CicUnification.UnificationFailure _
 531     | CicUnification.Uncertain _ ->
 532       raise MatchingFailure
 533 ;;
 534
 535
 536 let find_equalities context proof =
 537   let module C = Cic in
 538   let module S = CicSubstitution in
 539   let module T = CicTypeChecker in
 540   let eq_uri = LibraryObjects.eq_URI () in
 541   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
 542   let ok_types ty menv =
 543     List.for_all (fun (_, _, mt) -> mt = ty) menv
 544   in
 545   let rec aux index newmeta = function
 546     | [] -> [], newmeta
 547     | (Some (_, C.Decl (term)))::tl ->
 548         let do_find context term =
 549           match term with
 550           | C.Prod (name, s, t) ->
 551               let (head, newmetas, args, newmeta) =
 552                 ProofEngineHelpers.saturate_term newmeta []
 553                   context (S.lift index term) 0
 554               in
 555               let p =
 556                 if List.length args = 0 then
 557                   C.Rel index
 558                 else
 559                   C.Appl ((C.Rel index)::args)
 560               in (
 561                 match head with
 562                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 563                     when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
 564                     debug_print
 565                       (lazy
 566                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 567                     let o = !Utils.compare_terms t1 t2 in
 568                     let w = compute_equality_weight ty t1 t2 in
 569                     let proof = BasicProof p in
 570                     let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
 571                     Some e, (newmeta+1)
 572                 | _ -> None, newmeta
 573               )
 574           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 575               when UriManager.eq uri eq_uri ->
 576               let t1 = S.lift index t1
 577               and t2 = S.lift index t2 in
 578               let o = !Utils.compare_terms t1 t2 in
 579               let w = compute_equality_weight ty t1 t2 in
 580               let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
 581               Some e, (newmeta+1)
 582           | _ -> None, newmeta
 583         in (
 584           match do_find context term with
 585           | Some p, newmeta ->
 586               let tl, newmeta' = (aux (index+1) newmeta tl) in
 587               (index, p)::tl, max newmeta newmeta'
 588           | None, _ ->
 589               aux (index+1) newmeta tl
 590         )
 591     | _::tl ->
 592         aux (index+1) newmeta tl
 593   in
 594   let il, maxm = aux 1 newmeta context in
 595   let indexes, equalities = List.split il in
 596   indexes, equalities, maxm
 597 ;;
 598
 599
 600 (*
 601 let equations_blacklist =
 602   List.fold_left
 603     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
 604     UriManager.UriSet.empty [
 605       "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
 606       "cic:/Coq/Init/Logic/trans_eq.con";
 607       "cic:/Coq/Init/Logic/f_equal.con";
 608       "cic:/Coq/Init/Logic/f_equal2.con";
 609       "cic:/Coq/Init/Logic/f_equal3.con";
 610       "cic:/Coq/Init/Logic/f_equal4.con";
 611       "cic:/Coq/Init/Logic/f_equal5.con";
 612       "cic:/Coq/Init/Logic/sym_eq.con";
 613       "cic:/Coq/Init/Logic/eq_ind.con";
 614       "cic:/Coq/Init/Logic/eq_ind_r.con";
 615       "cic:/Coq/Init/Logic/eq_rec.con";
 616       "cic:/Coq/Init/Logic/eq_rec_r.con";
 617       "cic:/Coq/Init/Logic/eq_rect.con";
 618       "cic:/Coq/Init/Logic/eq_rect_r.con";
 619       "cic:/Coq/Logic/Eqdep/UIP.con";
 620       "cic:/Coq/Logic/Eqdep/UIP_refl.con";
 621       "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
 622       "cic:/Coq/ZArith/Zcompare/rename.con";
 623       (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
 624          perche' questo cacchio di teorema rompe le scatole :'( *)
 625       "cic:/Rocq/SUBST/comparith/mult_n_2.con";
 626
 627       "cic:/matita/logic/equality/eq_f.con";
 628       "cic:/matita/logic/equality/eq_f2.con";
 629       "cic:/matita/logic/equality/eq_rec.con";
 630       "cic:/matita/logic/equality/eq_rect.con";
 631     ]
 632 ;;
 633 *)
 634 let equations_blacklist = UriManager.UriSet.empty;;
 635
 636
 637 let find_library_equalities dbd context status maxmeta =
 638   let module C = Cic in
 639   let module S = CicSubstitution in
 640   let module T = CicTypeChecker in
 641   let blacklist =
 642     List.fold_left
 643       (fun s u -> UriManager.UriSet.add u s)
 644       equations_blacklist
 645       [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 646        eq_ind_r_URI ()]
 647   in
 648   let candidates =
 649     List.fold_left
 650       (fun l uri ->
 651         let suri = UriManager.string_of_uri uri in
 652          if UriManager.UriSet.mem uri blacklist then
 653            l
 654          else
 655            let t = CicUtil.term_of_uri uri in
 656            let ty, _ =
 657              CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
 658            in
 659            (uri, t, ty)::l)
 660       []
 661       (let t1 = Unix.gettimeofday () in
 662        let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
 663        let t2 = Unix.gettimeofday () in
 664        (debug_print
 665           (lazy
 666              (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
 667                 (t2 -. t1))));
 668        eqs)
 669   in
 670   let eq_uri1 = eq_XURI ()
 671   and eq_uri2 = LibraryObjects.eq_URI () in
 672   let iseq uri =
 673     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
 674   in
 675   let ok_types ty menv =
 676     List.for_all (fun (_, _, mt) -> mt = ty) menv
 677   in
 678   let rec has_vars = function
 679     | C.Meta _ | C.Rel _ | C.Const _ -> false
 680     | C.Var _ -> true
 681     | C.Appl l -> List.exists has_vars l
 682     | C.Prod (_, s, t) | C.Lambda (_, s, t)
 683     | C.LetIn (_, s, t) | C.Cast (s, t) ->
 684         (has_vars s) || (has_vars t)
 685     | _ -> false
 686   in
 687   let rec aux newmeta = function
 688     | [] -> [], newmeta
 689     | (uri, term, termty)::tl ->
 690         debug_print
 691           (lazy
 692              (Printf.sprintf "Examining: %s (%s)"
 693                 (CicPp.ppterm term) (CicPp.ppterm termty)));
 694         let res, newmeta =
 695           match termty with
 696           | C.Prod (name, s, t) when not (has_vars termty) ->
 697               let head, newmetas, args, newmeta =
 698                 ProofEngineHelpers.saturate_term newmeta [] context termty 0
 699               in
 700               let p =
 701                 if List.length args = 0 then
 702                   term
 703                 else
 704                   C.Appl (term::args)
 705               in (
 706                 match head with
 707                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 708                     when (iseq uri) && (ok_types ty newmetas) ->
 709                     debug_print
 710                       (lazy
 711                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 712                     let o = !Utils.compare_terms t1 t2 in
 713                     let w = compute_equality_weight ty t1 t2 in
 714                     let proof = BasicProof p in
 715                     let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
 716                     Some e, (newmeta+1)
 717                 | _ -> None, newmeta
 718               )
 719           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 720               when iseq uri && not (has_vars termty) ->
 721               let o = !Utils.compare_terms t1 t2 in
 722               let w = compute_equality_weight ty t1 t2 in
 723               let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
 724               Some e, (newmeta+1)
 725           | _ -> None, newmeta
 726         in
 727         match res with
 728         | Some e ->
 729             let tl, newmeta' = aux newmeta tl in
 730             (uri, e)::tl, max newmeta newmeta'
 731         | None ->
 732             aux newmeta tl
 733   in
 734   let found, maxm = aux maxmeta candidates in
 735   let uriset, eqlist =
 736     (List.fold_left
 737        (fun (s, l) (u, e) ->
 738           if List.exists (meta_convertibility_eq e) (List.map snd l) then (
 739             debug_print
 740               (lazy
 741                  (Printf.sprintf "NO!! %s already there!"
 742                     (string_of_equality e)));
 743             (UriManager.UriSet.add u s, l)
 744           ) else (UriManager.UriSet.add u s, (u, e)::l))
 745        (UriManager.UriSet.empty, []) found)
 746   in
 747   uriset, eqlist, maxm
 748 ;;
 749
 750
 751 let find_library_theorems dbd env status equalities_uris =
 752   let module C = Cic in
 753   let module S = CicSubstitution in
 754   let module T = CicTypeChecker in
 755   let blacklist =
 756     let refl_equal =
 757       UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
 758     let s =
 759       UriManager.UriSet.remove refl_equal
 760         (UriManager.UriSet.union equalities_uris equations_blacklist)
 761     in
 762     List.fold_left
 763       (fun s u -> UriManager.UriSet.add u s)
 764       s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 765          eq_ind_r_URI ()]
 766   in
 767   let metasenv, context, ugraph = env in
 768   let candidates =
 769     List.fold_left
 770       (fun l uri ->
 771          if UriManager.UriSet.mem uri blacklist then l
 772          else
 773            let t = CicUtil.term_of_uri uri in
 774            let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
 775            (t, ty, [])::l)
 776       [] (MetadataQuery.signature_of_goal ~dbd status)
 777   in
 778   let refl_equal =
 779     let u = eq_XURI () in
 780     let t = CicUtil.term_of_uri u in
 781     let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
 782     (t, ty, [])
 783   in
 784   refl_equal::candidates
 785 ;;
 786
 787
 788 let find_context_hypotheses env equalities_indexes =
 789   let metasenv, context, ugraph = env in
 790   let _, res =
 791     List.fold_left
 792       (fun (n, l) entry ->
 793          match entry with
 794          | None -> (n+1, l)
 795          | Some _ ->
 796              if List.mem n equalities_indexes then
 797                (n+1, l)
 798              else
 799                let t = Cic.Rel n in
 800                let ty, _ =
 801                  CicTypeChecker.type_of_aux' metasenv context t ugraph in
 802                (n+1, (t, ty, [])::l))
 803       (1, []) context
 804   in
 805   res
 806 ;;
 807
 808
 809 let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
 810   let table = Hashtbl.create (List.length args) in
 811   let newargs, newmeta =
 812     List.fold_right
 813       (fun t (newargs, index) ->
 814          match t with
 815          | Cic.Meta (i, l) ->
 816              if Hashtbl.mem table i then
 817                let idx = Hashtbl.find table i in
 818                ((Cic.Meta (idx, l))::newargs, index+1)
 819              else
 820                let _ = Hashtbl.add table i index in
 821                ((Cic.Meta (index, l))::newargs, index+1)
 822          | _ -> assert false)
 823       args ([], newmeta+1)
 824   in
 825   let repl where =
 826     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
 827       ~where
 828   in
 829   let menv' =
 830     List.fold_right
 831       (fun (i, context, term) menv ->
 832          try
 833            let index = Hashtbl.find table i in
 834            (index, context, term)::menv
 835          with Not_found ->
 836            (i, context, term)::menv)
 837       menv []
 838   in
 839   let ty = repl ty
 840   and left = repl left
 841   and right = repl right in
 842   let metas = (metas_of_term left) @ (metas_of_term right) in
 843   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
 844   let newargs =
 845     List.filter
 846       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
 847   in
 848   let _ =
 849     if List.length metas > 0 then
 850       let first = List.hd metas in
 851       (* this new equality might have less variables than its parents: here
 852          we fill the gap with a dummy arg. Example:
 853          with (f X Y) = X we can simplify
 854          (g X) = (f X Y) in
 855          (g X) = X.
 856          So the new equation has only one variable, but it still has type like
 857          \lambda X,Y:..., so we need to pass a dummy arg for Y
 858          (I hope this makes some sense...)
 859       *)
 860       Hashtbl.iter
 861         (fun k v ->
 862            if not (List.exists
 863                      (function Cic.Meta (i, _) -> i = v | _ -> assert false)
 864                      newargs) then
 865              Hashtbl.replace table k first)
 866         (Hashtbl.copy table)
 867   in
 868   let rec fix_proof = function
 869     | NoProof -> NoProof
 870     | BasicProof term -> BasicProof (repl term)
 871     | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
 872         let subst' =
 873           List.fold_left
 874             (fun s arg ->
 875                match arg with
 876                | Cic.Meta (i, l) -> (
 877                    try
 878                      let j = Hashtbl.find table i in
 879                      if List.mem_assoc i subst then
 880                        s
 881                      else
 882                        let _, context, ty = CicUtil.lookup_meta i menv in
 883                        (i, (context, Cic.Meta (j, l), ty))::s
 884                    with Not_found | CicUtil.Meta_not_found _ ->
 885                      s
 886                  )
 887                | _ -> assert false)
 888             [] args
 889         in
 890         ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
 891     | p -> assert false
 892   in
 893   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
 894   (newmeta + 1, neweq)
 895 ;;
 896
 897
 898 let term_is_equality term =
 899   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
 900   match term with
 901   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
 902   | _ -> false
 903 ;;
 904
 905
 906 exception TermIsNotAnEquality;;
 907
 908 let equality_of_term proof term =
 909   let eq_uri = LibraryObjects.eq_URI () in
 910   let iseq uri = UriManager.eq uri eq_uri in
 911   match term with
 912   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
 913       let o = !Utils.compare_terms t1 t2 in
 914       let w = compute_equality_weight ty t1 t2 in
 915       let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
 916       e
 917   | _ ->
 918       raise TermIsNotAnEquality
 919 ;;
 920
 921
 922 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 923
 924
 925 let is_identity ((metasenv, context, ugraph) as env) = function
 926   | ((_, _, (ty, left, right, _), menv, _) as equality) ->
 927        (left = right ||
 928           (* (meta_convertibility left right) || *)
 929           (fst (CicReduction.are_convertible
 930                   ~metasenv:(metasenv @ menv) context left right ugraph)))
 931 ;;
 932
 933
 934 let term_of_equality equality =
 935   let _, _, (ty, left, right, _), menv, args = equality in
 936   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
 937   let argsno = List.length args in
 938   let t =
 939     CicSubstitution.lift argsno
 940       (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
 941   in
 942   snd (
 943     List.fold_right
 944       (fun a (n, t) ->
 945          match a with
 946          | Cic.Meta (i, _) ->
 947              let name = Cic.Name ("X" ^ (string_of_int n)) in
 948              let _, _, ty = CicUtil.lookup_meta i menv in
 949              let t =
 950                ProofEngineReduction.replace
 951                  ~equality:eq ~what:[i]
 952                  ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
 953              in
 954              (n-1, Cic.Prod (name, ty, t))
 955          | _ -> assert false)
 956       args (argsno, t))
 957 ;;