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               if newmeta' < newmeta then
 578                 prerr_endline "big trouble";
 579               (index, p)::tl, newmeta' (* max???? *)
 580           | None, _ ->
 581               aux (index+1) newmeta tl
 582         )
 583     | _::tl ->
 584         aux (index+1) newmeta tl
 585   in
 586   let il, maxm = aux 1 newmeta context in
 587   let indexes, equalities = List.split il in
 588   indexes, equalities, maxm
 589 ;;
 590
 591
 592 (*
 593 let equations_blacklist =
 594   List.fold_left
 595     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
 596     UriManager.UriSet.empty [
 597       "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
 598       "cic:/Coq/Init/Logic/trans_eq.con";
 599       "cic:/Coq/Init/Logic/f_equal.con";
 600       "cic:/Coq/Init/Logic/f_equal2.con";
 601       "cic:/Coq/Init/Logic/f_equal3.con";
 602       "cic:/Coq/Init/Logic/f_equal4.con";
 603       "cic:/Coq/Init/Logic/f_equal5.con";
 604       "cic:/Coq/Init/Logic/sym_eq.con";
 605       "cic:/Coq/Init/Logic/eq_ind.con";
 606       "cic:/Coq/Init/Logic/eq_ind_r.con";
 607       "cic:/Coq/Init/Logic/eq_rec.con";
 608       "cic:/Coq/Init/Logic/eq_rec_r.con";
 609       "cic:/Coq/Init/Logic/eq_rect.con";
 610       "cic:/Coq/Init/Logic/eq_rect_r.con";
 611       "cic:/Coq/Logic/Eqdep/UIP.con";
 612       "cic:/Coq/Logic/Eqdep/UIP_refl.con";
 613       "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
 614       "cic:/Coq/ZArith/Zcompare/rename.con";
 615       (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
 616          perche' questo cacchio di teorema rompe le scatole :'( *)
 617       "cic:/Rocq/SUBST/comparith/mult_n_2.con";
 618
 619       "cic:/matita/logic/equality/eq_f.con";
 620       "cic:/matita/logic/equality/eq_f2.con";
 621       "cic:/matita/logic/equality/eq_rec.con";
 622       "cic:/matita/logic/equality/eq_rect.con";
 623     ]
 624 ;;
 625 *)
 626 let equations_blacklist = UriManager.UriSet.empty;;
 627
 628
 629 let find_library_equalities dbd context status maxmeta =
 630   let module C = Cic in
 631   let module S = CicSubstitution in
 632   let module T = CicTypeChecker in
 633   let blacklist =
 634     List.fold_left
 635       (fun s u -> UriManager.UriSet.add u s)
 636       equations_blacklist
 637       [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
 638        eq_ind_r_URI ()]
 639   in
 640   let candidates =
 641     List.fold_left
 642       (fun l uri ->
 643          if UriManager.UriSet.mem uri blacklist then
 644            l
 645          else
 646            let t = CicUtil.term_of_uri uri in
 647            let ty, _ =
 648              CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
 649            in
 650            (uri, t, ty)::l)
 651       []
 652       (let t1 = Unix.gettimeofday () in
 653        let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
 654        let t2 = Unix.gettimeofday () in
 655        (debug_print
 656           (lazy
 657              (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
 658                 (t2 -. t1))));
 659        eqs)
 660   in
 661   let eq_uri1 = eq_XURI ()
 662   and eq_uri2 = LibraryObjects.eq_URI () in
 663   let iseq uri =
 664     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
 665   in
 666   let ok_types ty menv =
 667     List.for_all (fun (_, _, mt) -> mt = ty) menv
 668   in
 669   let rec has_vars = function
 670     | C.Meta _ | C.Rel _ | C.Const _ -> false
 671     | C.Var _ -> true
 672     | C.Appl l -> List.exists has_vars l
 673     | C.Prod (_, s, t) | C.Lambda (_, s, t)
 674     | C.LetIn (_, s, t) | C.Cast (s, t) ->
 675         (has_vars s) || (has_vars t)
 676     | _ -> false
 677   in
 678   let rec aux newmeta = function
 679     | [] -> [], newmeta
 680     | (uri, term, termty)::tl ->
 681         debug_print
 682           (lazy
 683              (Printf.sprintf "Examining: %s (%s)"
 684                 (CicPp.ppterm term) (CicPp.ppterm termty)));
 685         let res, newmeta =
 686           match termty with
 687           | C.Prod (name, s, t) when not (has_vars termty) ->
 688               let head, newmetas, args, newmeta =
 689                 ProofEngineHelpers.saturate_term newmeta [] context termty 0
 690               in
 691               let p =
 692                 if List.length args = 0 then
 693                   term
 694                 else
 695                   C.Appl (term::args)
 696               in (
 697                 match head with
 698                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 699                     when (iseq uri) && (ok_types ty newmetas) ->
 700                     debug_print
 701                       (lazy
 702                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
 703                     let o = !Utils.compare_terms t1 t2 in
 704                     let w = compute_equality_weight ty t1 t2 in
 705                     let proof = BasicProof p in
 706                     let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
 707                     Some e, (newmeta+1)
 708                 | _ -> None, newmeta
 709               )
 710           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 711               when iseq uri && not (has_vars termty) ->
 712               let o = !Utils.compare_terms t1 t2 in
 713               let w = compute_equality_weight ty t1 t2 in
 714               let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
 715               Some e, (newmeta+1)
 716           | _ -> None, newmeta
 717         in
 718         match res with
 719         | Some e ->
 720             let tl, newmeta' = aux newmeta tl in
 721               if newmeta' < newmeta then
 722                 prerr_endline "big trouble";
 723               (uri, e)::tl, newmeta' (* max???? *)
 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_old newmeta (w, p, (ty, left, right, o), menv, args) =
 803   let table = Hashtbl.create (List.length args) in
 804
 805   let newargs, newmeta =
 806     List.fold_right
 807       (fun t (newargs, index) ->
 808          match t with
 809          | Cic.Meta (i, l) ->
 810              if Hashtbl.mem table i then
 811                let idx = Hashtbl.find table i in
 812                ((Cic.Meta (idx, l))::newargs, index+1)
 813              else
 814                let _ = Hashtbl.add table i index in
 815                ((Cic.Meta (index, l))::newargs, index+1)
 816          | _ -> assert false)
 817       args ([], newmeta+1)
 818   in
 819
 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) @ (metas_of_term ty) 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 relocate newmeta menv =
 894   let subst, metasenv, newmeta =
 895     List.fold_right
 896       (fun (i, context, ty) (subst, menv, maxmeta) ->
 897         let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
 898         let newsubst = (i, (context, (Cic.Meta (maxmeta, irl)), ty)) in
 899         let newmeta = maxmeta, context, ty in
 900         newsubst::subst, newmeta::menv, maxmeta+1)
 901       menv ([], [], newmeta+1)
 902   in
 903   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
 904   let subst =
 905     List.map
 906       (fun (i, (context, term, ty)) ->
 907          let context = CicMetaSubst.apply_subst_context subst context in
 908          let term = CicMetaSubst.apply_subst subst term in
 909          let ty = CicMetaSubst.apply_subst subst ty in
 910          (i, (context, term, ty))) subst in
 911   subst, metasenv, newmeta
 912
 913
 914 let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
 915   (* debug
 916   let _ , eq =
 917     fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
 918   prerr_endline (string_of_equality eq); *)
 919   let subst, metasenv, newmeta = relocate newmeta menv in
 920   let ty = CicMetaSubst.apply_subst subst ty in
 921   let left = CicMetaSubst.apply_subst subst left in
 922   let right = CicMetaSubst.apply_subst subst right in
 923   let args = List.map (CicMetaSubst.apply_subst subst) args in
 924   let rec fix_proof = function
 925     | NoProof -> NoProof
 926     | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
 927     | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
 928         ProofBlock (subst' @ subst, eq_URI, namety, bo, (pos, eq), p)
 929     | p -> assert false
 930   in
 931   let metas = (metas_of_term left)@(metas_of_term right)@(metas_of_term ty) in
 932   let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
 933   let eq = (w, fix_proof p, (ty, left, right, o), metasenv, args) in
 934   (* debug prerr_endline (string_of_equality eq); *)
 935   newmeta, eq
 936
 937 let term_is_equality term =
 938   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
 939   match term with
 940   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
 941   | _ -> false
 942 ;;
 943
 944
 945 exception TermIsNotAnEquality;;
 946
 947 let equality_of_term proof term =
 948   let eq_uri = LibraryObjects.eq_URI () in
 949   let iseq uri = UriManager.eq uri eq_uri in
 950   match term with
 951   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
 952       let o = !Utils.compare_terms t1 t2 in
 953       let w = compute_equality_weight ty t1 t2 in
 954       let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
 955       e
 956   | _ ->
 957       raise TermIsNotAnEquality
 958 ;;
 959
 960
 961 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 962
 963 let is_weak_identity (metasenv, context, ugraph) = function
 964   | (_, _, (ty, left, right, _), menv, _) ->
 965        (left = right ||
 966           (meta_convertibility left right))
 967            (* the test below is not a good idea since it stops
 968               demodulation too early *)
 969            (* (fst (CicReduction.are_convertible
 970                   ~metasenv:(metasenv @ menv) context left right ugraph)))*)
 971 ;;
 972
 973 let is_identity (metasenv, context, ugraph) = function
 974   | (_, _, (ty, left, right, _), menv, _) ->
 975        (left = right ||
 976           (* (meta_convertibility left right)) *)
 977            (fst (CicReduction.are_convertible
 978                   ~metasenv:(metasenv @ menv) context left right ugraph)))
 979 ;;
 980
 981
 982 let term_of_equality equality =
 983   let _, _, (ty, left, right, _), menv, args = equality in
 984   let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
 985   let argsno = List.length args in
 986   let t =
 987     CicSubstitution.lift argsno
 988       (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
 989   in
 990   snd (
 991     List.fold_right
 992       (fun a (n, t) ->
 993          match a with
 994          | Cic.Meta (i, _) ->
 995              let name = Cic.Name ("X" ^ (string_of_int n)) in
 996              let _, _, ty = CicUtil.lookup_meta i menv in
 997              let t =
 998                ProofEngineReduction.replace
 999                  ~equality:eq ~what:[i]
1000                  ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
1001              in
1002              (n-1, Cic.Prod (name, ty, t))
1003          | _ -> assert false)
1004       args (argsno, t))
1005 ;;