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