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 (* $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         unification metasenv context t1 t2 ugraph
 511       in
 512       let t' = CicMetaSubst.apply_subst subst t1 in
 513       if not (meta_convertibility t1 t') then
 514         raise MatchingFailure
 515       else
 516         let metas = metas_of_term t1 in
 517         let fix_subst = function
 518           | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
 519               (j, (c, Cic.Meta (i, lc), ty))
 520           | s -> s
 521         in
 522         let subst = List.map fix_subst subst in
 523         subst, metasenv, ugraph
 524     with
 525     | CicUnification.UnificationFailure _
 526     | CicUnification.Uncertain _ ->
 527       raise MatchingFailure
 528 ;;
 529
 530
 531 let find_equalities context proof =
 532   let module C = Cic in
 533   let module S = CicSubstitution in
 534   let module T = CicTypeChecker in
 535   let eq_uri = LibraryObjects.eq_URI () in
 536   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
 537   let ok_types ty menv =
 538     List.for_all (fun (_, _, mt) -> mt = ty) menv
 539   in
 540   let rec aux index newmeta = function
 541     | [] -> [], newmeta
 542     | (Some (_, C.Decl (term)))::tl ->
 543         let do_find context term =
 544           match term with
 545           | C.Prod (name, s, t) ->
 546               let (head, newmetas, args, newmeta) =
 547                 ProofEngineHelpers.saturate_term newmeta []
 548                   context (S.lift index term) 0
 549               in
 550               let p =
 551                 if List.length args = 0 then
 552                   C.Rel index
 553                 else
 554                   C.Appl ((C.Rel index)::args)
 555               in (
 556                 match head with
 557                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 558                     when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
 559                     debug_print
 560                       (lazy
 561                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 562                     let o = !Utils.compare_terms t1 t2 in
 563                     let w = compute_equality_weight ty t1 t2 in
 564                     let proof = BasicProof p in
 565                     let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
 566                     Some e, (newmeta+1)
 567                 | _ -> None, newmeta
 568               )
 569           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 570               when UriManager.eq uri eq_uri ->
 571               let t1 = S.lift index t1
 572               and t2 = S.lift index t2 in
 573               let o = !Utils.compare_terms t1 t2 in
 574               let w = compute_equality_weight ty t1 t2 in
 575               let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
 576               Some e, (newmeta+1)
 577           | _ -> None, newmeta
 578         in (
 579           match do_find context term with
 580           | Some p, newmeta ->
 581               let tl, newmeta' = (aux (index+1) newmeta tl) in
 582               (index, p)::tl, max newmeta newmeta'
 583           | None, _ ->
 584               aux (index+1) newmeta tl
 585         )
 586     | _::tl ->
 587         aux (index+1) newmeta tl
 588   in
 589   let il, maxm = aux 1 newmeta context in
 590   let indexes, equalities = List.split il in
 591   indexes, equalities, maxm
 592 ;;
 593
 594
 595 (*
 596 let equations_blacklist =
 597   List.fold_left
 598     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
 599     UriManager.UriSet.empty [
 600       "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
 601       "cic:/Coq/Init/Logic/trans_eq.con";
 602       "cic:/Coq/Init/Logic/f_equal.con";
 603       "cic:/Coq/Init/Logic/f_equal2.con";
 604       "cic:/Coq/Init/Logic/f_equal3.con";
 605       "cic:/Coq/Init/Logic/f_equal4.con";
 606       "cic:/Coq/Init/Logic/f_equal5.con";
 607       "cic:/Coq/Init/Logic/sym_eq.con";
 608       "cic:/Coq/Init/Logic/eq_ind.con";
 609       "cic:/Coq/Init/Logic/eq_ind_r.con";
 610       "cic:/Coq/Init/Logic/eq_rec.con";
 611       "cic:/Coq/Init/Logic/eq_rec_r.con";
 612       "cic:/Coq/Init/Logic/eq_rect.con";
 613       "cic:/Coq/Init/Logic/eq_rect_r.con";
 614       "cic:/Coq/Logic/Eqdep/UIP.con";
 615       "cic:/Coq/Logic/Eqdep/UIP_refl.con";
 616       "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
 617       "cic:/Coq/ZArith/Zcompare/rename.con";
 618       (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
 619          perche' questo cacchio di teorema rompe le scatole :'( *)
 620       "cic:/Rocq/SUBST/comparith/mult_n_2.con";
 621
 622       "cic:/matita/logic/equality/eq_f.con";
 623       "cic:/matita/logic/equality/eq_f2.con";
 624       "cic:/matita/logic/equality/eq_rec.con";
 625       "cic:/matita/logic/equality/eq_rect.con";
 626     ]
 627 ;;
 628 *)
 629 let equations_blacklist = UriManager.UriSet.empty;;
 630
 631
 632 let find_library_equalities dbd context status maxmeta =
 633   let module C = Cic in
 634   let module S = CicSubstitution in
 635   let module T = CicTypeChecker in
 636   let blacklist =
 637     List.fold_left
 638       (fun s u -> UriManager.UriSet.add u s)
 639       equations_blacklist
 640       [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 641        eq_ind_r_URI ()]
 642   in
 643   let candidates =
 644     List.fold_left
 645       (fun l uri ->
 646         let suri = UriManager.string_of_uri uri in
 647          if UriManager.UriSet.mem uri blacklist then
 648            l
 649          else
 650            let t = CicUtil.term_of_uri uri in
 651            let ty, _ =
 652              CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
 653            in
 654            (uri, t, ty)::l)
 655       []
 656       (let t1 = Unix.gettimeofday () in
 657        let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
 658        let t2 = Unix.gettimeofday () in
 659        (debug_print
 660           (lazy
 661              (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
 662                 (t2 -. t1))));
 663        eqs)
 664   in
 665   let eq_uri1 = eq_XURI ()
 666   and eq_uri2 = LibraryObjects.eq_URI () in
 667   let iseq uri =
 668     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
 669   in
 670   let ok_types ty menv =
 671     List.for_all (fun (_, _, mt) -> mt = ty) menv
 672   in
 673   let rec has_vars = function
 674     | C.Meta _ | C.Rel _ | C.Const _ -> false
 675     | C.Var _ -> true
 676     | C.Appl l -> List.exists has_vars l
 677     | C.Prod (_, s, t) | C.Lambda (_, s, t)
 678     | C.LetIn (_, s, t) | C.Cast (s, t) ->
 679         (has_vars s) || (has_vars t)
 680     | _ -> false
 681   in
 682   let rec aux newmeta = function
 683     | [] -> [], newmeta
 684     | (uri, term, termty)::tl ->
 685         debug_print
 686           (lazy
 687              (Printf.sprintf "Examining: %s (%s)"
 688                 (CicPp.ppterm term) (CicPp.ppterm termty)));
 689         let res, newmeta =
 690           match termty with
 691           | C.Prod (name, s, t) when not (has_vars termty) ->
 692               let head, newmetas, args, newmeta =
 693                 ProofEngineHelpers.saturate_term newmeta [] context termty 0
 694               in
 695               let p =
 696                 if List.length args = 0 then
 697                   term
 698                 else
 699                   C.Appl (term::args)
 700               in (
 701                 match head with
 702                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 703                     when (iseq uri) && (ok_types ty newmetas) ->
 704                     debug_print
 705                       (lazy
 706                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 707                     let o = !Utils.compare_terms t1 t2 in
 708                     let w = compute_equality_weight ty t1 t2 in
 709                     let proof = BasicProof p in
 710                     let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
 711                     Some e, (newmeta+1)
 712                 | _ -> None, newmeta
 713               )
 714           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 715               when iseq uri && not (has_vars termty) ->
 716               let o = !Utils.compare_terms t1 t2 in
 717               let w = compute_equality_weight ty t1 t2 in
 718               let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
 719               Some e, (newmeta+1)
 720           | _ -> None, newmeta
 721         in
 722         match res with
 723         | Some e ->
 724             let tl, newmeta' = aux newmeta tl in
 725             (uri, e)::tl, max newmeta newmeta'
 726         | None ->
 727             aux newmeta tl
 728   in
 729   let found, maxm = aux maxmeta candidates in
 730   let uriset, eqlist =
 731     (List.fold_left
 732        (fun (s, l) (u, e) ->
 733           if List.exists (meta_convertibility_eq e) (List.map snd l) then (
 734             debug_print
 735               (lazy
 736                  (Printf.sprintf "NO!! %s already there!"
 737                     (string_of_equality e)));
 738             (UriManager.UriSet.add u s, l)
 739           ) else (UriManager.UriSet.add u s, (u, e)::l))
 740        (UriManager.UriSet.empty, []) found)
 741   in
 742   uriset, eqlist, maxm
 743 ;;
 744
 745
 746 let find_library_theorems dbd env status equalities_uris =
 747   let module C = Cic in
 748   let module S = CicSubstitution in
 749   let module T = CicTypeChecker in
 750   let blacklist =
 751     let refl_equal =
 752       UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
 753     let s =
 754       UriManager.UriSet.remove refl_equal
 755         (UriManager.UriSet.union equalities_uris equations_blacklist)
 756     in
 757     List.fold_left
 758       (fun s u -> UriManager.UriSet.add u s)
 759       s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 760          eq_ind_r_URI ()]
 761   in
 762   let metasenv, context, ugraph = env in
 763   let candidates =
 764     List.fold_left
 765       (fun l uri ->
 766          if UriManager.UriSet.mem uri blacklist then l
 767          else
 768            let t = CicUtil.term_of_uri uri in
 769            let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
 770            (t, ty, [])::l)
 771       [] (MetadataQuery.signature_of_goal ~dbd status)
 772   in
 773   let refl_equal =
 774     let u = eq_XURI () in
 775     let t = CicUtil.term_of_uri u in
 776     let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
 777     (t, ty, [])
 778   in
 779   refl_equal::candidates
 780 ;;
 781
 782
 783 let find_context_hypotheses env equalities_indexes =
 784   let metasenv, context, ugraph = env in
 785   let _, res =
 786     List.fold_left
 787       (fun (n, l) entry ->
 788          match entry with
 789          | None -> (n+1, l)
 790          | Some _ ->
 791              if List.mem n equalities_indexes then
 792                (n+1, l)
 793              else
 794                let t = Cic.Rel n in
 795                let ty, _ =
 796                  CicTypeChecker.type_of_aux' metasenv context t ugraph in
 797                (n+1, (t, ty, [])::l))
 798       (1, []) context
 799   in
 800   res
 801 ;;
 802
 803
 804 let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
 805   let table = Hashtbl.create (List.length args) in
 806   let newargs, newmeta =
 807     List.fold_right
 808       (fun t (newargs, index) ->
 809          match t with
 810          | Cic.Meta (i, l) ->
 811              if Hashtbl.mem table i then
 812                let idx = Hashtbl.find table i in
 813                ((Cic.Meta (idx, l))::newargs, index+1)
 814              else
 815                let _ = Hashtbl.add table i index in
 816                ((Cic.Meta (index, l))::newargs, index+1)
 817          | _ -> assert false)
 818       args ([], newmeta+1)
 819   in
 820   let repl where =
 821     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
 822       ~where
 823   in
 824   let menv' =
 825     List.fold_right
 826       (fun (i, context, term) menv ->
 827          try
 828            let index = Hashtbl.find table i in
 829            (index, context, term)::menv
 830          with Not_found ->
 831            (i, context, term)::menv)
 832       menv []
 833   in
 834   let ty = repl ty
 835   and left = repl left
 836   and right = repl right in
 837   let metas = (metas_of_term left) @ (metas_of_term right) in
 838   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
 839   let newargs =
 840     List.filter
 841       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
 842   in
 843   let _ =
 844     if List.length metas > 0 then
 845       let first = List.hd metas in
 846       (* this new equality might have less variables than its parents: here
 847          we fill the gap with a dummy arg. Example:
 848          with (f X Y) = X we can simplify
 849          (g X) = (f X Y) in
 850          (g X) = X.
 851          So the new equation has only one variable, but it still has type like
 852          \lambda X,Y:..., so we need to pass a dummy arg for Y
 853          (I hope this makes some sense...)
 854       *)
 855       Hashtbl.iter
 856         (fun k v ->
 857            if not (List.exists
 858                      (function Cic.Meta (i, _) -> i = v | _ -> assert false)
 859                      newargs) then
 860              Hashtbl.replace table k first)
 861         (Hashtbl.copy table)
 862   in
 863   let rec fix_proof = function
 864     | NoProof -> NoProof
 865     | BasicProof term -> BasicProof (repl term)
 866     | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
 867         let subst' =
 868           List.fold_left
 869             (fun s arg ->
 870                match arg with
 871                | Cic.Meta (i, l) -> (
 872                    try
 873                      let j = Hashtbl.find table i in
 874                      if List.mem_assoc i subst then
 875                        s
 876                      else
 877                        let _, context, ty = CicUtil.lookup_meta i menv in
 878                        (i, (context, Cic.Meta (j, l), ty))::s
 879                    with Not_found | CicUtil.Meta_not_found _ ->
 880                      s
 881                  )
 882                | _ -> assert false)
 883             [] args
 884         in
 885         ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
 886     | p -> assert false
 887   in
 888   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
 889   (newmeta + 1, neweq)
 890 ;;
 891
 892
 893 let term_is_equality term =
 894   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
 895   match term with
 896   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
 897   | _ -> false
 898 ;;
 899
 900
 901 exception TermIsNotAnEquality;;
 902
 903 let equality_of_term proof term =
 904   let eq_uri = LibraryObjects.eq_URI () in
 905   let iseq uri = UriManager.eq uri eq_uri in
 906   match term with
 907   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
 908       let o = !Utils.compare_terms t1 t2 in
 909       let w = compute_equality_weight ty t1 t2 in
 910       let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
 911       e
 912   | _ ->
 913       raise TermIsNotAnEquality
 914 ;;
 915
 916
 917 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 918
 919
 920 let is_identity ((metasenv, context, ugraph) as env) = function
 921   | ((_, _, (ty, left, right, _), menv, _) as equality) ->
 922        (left = right ||
 923           (* (meta_convertibility left right) || *)
 924           (fst (CicReduction.are_convertible
 925                   ~metasenv:(metasenv @ menv) context left right ugraph)))
 926 ;;
 927
 928
 929 let term_of_equality equality =
 930   let _, _, (ty, left, right, _), menv, args = equality in
 931   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
 932   let argsno = List.length args in
 933   let t =
 934     CicSubstitution.lift argsno
 935       (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
 936   in
 937   snd (
 938     List.fold_right
 939       (fun a (n, t) ->
 940          match a with
 941          | Cic.Meta (i, _) ->
 942              let name = Cic.Name ("X" ^ (string_of_int n)) in
 943              let _, _, ty = CicUtil.lookup_meta i menv in
 944              let t =
 945                ProofEngineReduction.replace
 946                  ~equality:eq ~what:[i]
 947                  ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
 948              in
 949              (n-1, Cic.Prod (name, ty, t))
 950          | _ -> assert false)
 951       args (argsno, t))
 952 ;;