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