components/tactics/paramodulation/equality_retrieval.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 open Utils;;
  27
  28 let debug_print s = ();;(*prerr_endline (Lazy.force s);;*)
  29
  30 type auto_type =
  31   int ->
  32   AutoTypes.flags ->
  33   ProofEngineTypes.proof ->
  34   Cic.context ->
  35   AutoCache.cache ->
  36   ProofEngineTypes.goal list ->
  37     Cic.substitution list * AutoCache.cache * int
  38
  39 let is_var_free (_,term,_ty) =
  40   let rec is_var_free = function
  41     | Cic.Var _ -> false
  42     | Cic.Appl l -> List.for_all is_var_free l
  43     | Cic.Prod (_, s, t)
  44     | Cic.Lambda (_, s, t)
  45     | Cic.LetIn (_, s, t)
  46     | Cic.Cast (s, t) -> (is_var_free s) && (is_var_free t)
  47     | _ -> true
  48  in
  49  is_var_free term
  50 ;;
  51
  52 let rec is_an_equality = function
  53   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2]
  54     when (LibraryObjects.is_eq_URI uri) -> true
  55   | Cic.Prod (name, s, t) -> is_an_equality t
  56   | _ -> false
  57 ;;
  58
  59 let build_equality_of_hypothesis bag index head args newmetas maxmeta =
  60   match head with
  61   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
  62       let p =
  63         if args = [] then Cic.Rel index else Cic.Appl ((Cic.Rel index)::args)
  64       in
  65       debug_print
  66         (lazy
  67            (Printf.sprintf "OK: %s" (CicPp.ppterm p)));
  68       let o = !Utils.compare_terms t1 t2 in
  69       let stat = (ty,t1,t2,o) in
  70       (* let w = compute_equality_weight stat in *)
  71       let w = 0 in
  72       let proof = Equality.Exact p in
  73       let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
  74       (* to clean the local context of metas *)
  75       Equality.fix_metas bag maxmeta e
  76   | _ -> assert false
  77 ;;
  78
  79 let build_equality bag ty t1 t2 proof menv maxmeta =
  80   let o = !Utils.compare_terms t1 t2 in
  81   let stat = (ty,t1,t2,o) in
  82   let w = compute_equality_weight stat in
  83   let proof = Equality.Exact proof in
  84   let e = Equality.mk_equality bag (w, proof, stat, menv) in
  85   (* to clean the local context of metas *)
  86   Equality.fix_metas bag maxmeta e
  87 ;;
  88
  89 let tty_of_u u =
  90   let t = CicUtil.term_of_uri u in
  91   let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
  92   t, ty
  93 ;;
  94
  95 let utty_of_u u =
  96   let t,ty = tty_of_u u in
  97   u, t, ty
  98 ;;
  99
 100 let is_monomorphic_eq (_,term,termty) =
 101   let rec last = function
 102     | Cic.Prod(_,_,t) -> last t
 103     | t -> t
 104   in
 105   match last termty with
 106   | Cic.Appl [Cic.MutInd (_, _, []); Cic.Rel _; _; _] -> false
 107   | Cic.Appl [Cic.MutInd (_, _, []); _; _; _] -> true
 108   | _ -> false
 109 ;;
 110
 111 (*
 112 let equations_blacklist =
 113  let blacklist = [
 114   "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
 115   "cic:/Coq/Init/Logic/trans_eq.con"; "cic:/Coq/Init/Logic/f_equal.con";
 116   "cic:/Coq/Init/Logic/f_equal2.con"; "cic:/Coq/Init/Logic/f_equal3.con";
 117   "cic:/Coq/Init/Logic/f_equal4.con"; "cic:/Coq/Init/Logic/f_equal5.con";
 118   "cic:/Coq/Init/Logic/sym_eq.con"; "cic:/Coq/Init/Logic/eq_ind.con";
 119   "cic:/Coq/Init/Logic/eq_ind_r.con"; "cic:/Coq/Init/Logic/eq_rec.con";
 120   "cic:/Coq/Init/Logic/eq_rec_r.con"; "cic:/Coq/Init/Logic/eq_rect.con";
 121   "cic:/Coq/Init/Logic/eq_rect_r.con"; "cic:/Coq/Logic/Eqdep/UIP.con";
 122   "cic:/Coq/Logic/Eqdep/UIP_refl.con";"cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
 123   "cic:/Coq/ZArith/Zcompare/rename.con";
 124   "cic:/Rocq/SUBST/comparith/mult_n_2.con";
 125   "cic:/matita/logic/equality/eq_f.con";"cic:/matita/logic/equality/eq_f2.con";
 126   "cic:/matita/logic/equality/eq_rec.con";
 127   "cic:/matita/logic/equality/eq_rect.con"; ]
 128  in
 129   List.fold_left
 130     (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
 131     UriManager.UriSet.empty blacklist
 132 ;;
 133 *)
 134 let equations_blacklist = UriManager.UriSet.empty;;
 135
 136 (* {{{ ****************** SATURATION STUFF ***************************)
 137 exception UnableToSaturate of AutoCache.cache * int
 138
 139 let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;;
 140
 141 let saturate_term context metasenv oldnewmeta term cache auto fast =
 142   let head, metasenv, args, newmeta =
 143     ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
 144   in
 145   let args_for_auto =
 146     HExtlib.filter_map
 147       (function
 148       | Cic.Meta(i,_) ->
 149           let _,_,mt = CicUtil.lookup_meta i metasenv in
 150           let sort,u =
 151             CicTypeChecker.type_of_aux' metasenv context mt
 152               CicUniv.empty_ugraph
 153           in
 154           let b, _ =
 155             CicReduction.are_convertible ~metasenv context
 156               sort (Cic.Sort Cic.Prop) u
 157           in
 158           if b then Some i else None
 159           (* maybe unif or conv should be used instead of = *)
 160       | _ -> assert false)
 161     args
 162   in
 163   let results,cache,newmeta =
 164     if args_for_auto = [] then
 165       let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
 166       [args,metasenv,newmetas,head,newmeta],cache,newmeta
 167     else
 168       let proof =
 169         None,metasenv,term,term (* term non e' significativo *)
 170       in
 171       let flags =
 172         if fast then
 173           {AutoTypes.default_flags() with
 174            AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
 175            maxwidth = 2;maxdepth = 2;
 176            use_paramod=true;use_only_paramod=false}
 177         else
 178           {AutoTypes.default_flags() with
 179            AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
 180            maxwidth = 2;maxdepth = 4;
 181            use_paramod=true;use_only_paramod=false}
 182       in
 183       match auto newmeta flags proof context cache args_for_auto with
 184       | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta))
 185       | substs,cache,newmeta ->
 186           List.map
 187             (fun subst ->
 188               let metasenv =
 189                 CicMetaSubst.apply_subst_metasenv subst metasenv
 190               in
 191               let head = CicMetaSubst.apply_subst subst head in
 192               let newmetas =
 193                 List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
 194               in
 195               let args = List.map (CicMetaSubst.apply_subst subst) args in
 196               let newm = CicMkImplicit.new_meta metasenv subst in
 197               args,metasenv,newmetas,head,max newm newmeta)
 198             substs, cache, newmeta
 199   in
 200   results,cache,newmeta
 201 ;;
 202 (* }}} ***************************************************************)
 203
 204 let find_context_equalities
 205   maxmeta bag ?(auto = default_auto) context proof cache
 206 =
 207   prerr_endline "find_equalities";
 208   let module C = Cic in
 209   let module S = CicSubstitution in
 210   let module T = CicTypeChecker in
 211   let _,metasenv,_,_ = proof in
 212   let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
 213   let rec aux cache index newmeta = function
 214     | [] -> [], newmeta,cache
 215     | (Some (_, C.Decl (term)))::tl ->
 216         debug_print
 217           (lazy
 218              (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
 219         let do_find context term =
 220           match term with
 221           | C.Prod (name, s, t) when is_an_equality t ->
 222               (try
 223                 let term = S.lift index term in
 224                 let saturated,cache,newmeta =
 225                   saturate_term context metasenv newmeta term
 226                     cache auto false
 227                 in
 228                 let eqs,newmeta =
 229                   List.fold_left
 230                    (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
 231                      let newmeta, equality =
 232                        build_equality_of_hypothesis
 233                          bag index head args newmetas (max newmeta newmeta')
 234                      in
 235                      equality::acc, newmeta + 1)
 236                    ([],newmeta) saturated
 237                 in
 238                  eqs, newmeta, cache
 239               with UnableToSaturate (cache,newmeta) ->
 240                 [],newmeta,cache)
 241           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 242               when LibraryObjects.is_eq_URI uri ->
 243               let term = S.lift index term in
 244               let newmeta, e =
 245                 build_equality_of_hypothesis bag index term [] [] newmeta
 246               in
 247               [e], (newmeta+1),cache
 248           | _ -> [], newmeta, cache
 249         in
 250         let eqs, newmeta, cache = do_find context term in
 251         let rest, newmeta,cache = aux cache (index+1) newmeta tl in
 252         List.map (fun x -> index,x) eqs @ rest, newmeta, cache
 253     | _::tl ->
 254         aux cache (index+1) newmeta tl
 255   in
 256   let il, maxm, cache =
 257     aux cache 1 newmeta context
 258   in
 259   let indexes, equalities = List.split il in
 260   indexes, equalities, maxm, cache
 261 ;;
 262
 263 let find_library_equalities bag
 264   ?(auto = default_auto) caso_strano dbd context status maxmeta cache
 265 =
 266   let module C = Cic in
 267   let module S = CicSubstitution in
 268   let module T = CicTypeChecker in
 269   let proof, goalno = status in
 270   let _,metasenv,_,_ = proof in
 271   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
 272   let signature =
 273     if caso_strano then
 274       begin
 275         match ty with
 276         | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] ->
 277             (let mainl, sigl = MetadataConstraints.signature_of l in
 278             let mainr, sigr = MetadataConstraints.signature_of r in
 279             match mainl,mainr with
 280             | Some (uril,tyl), Some (urir, tyr)
 281                 when LibraryObjects.is_eq_URI uril &&
 282                      LibraryObjects.is_eq_URI urir &&
 283                      tyl = tyr ->
 284                   Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr)
 285             | _ ->
 286                 let u = (UriManager.uri_of_string
 287                   (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in
 288                 let main = Some (u, []) in
 289                 Some (main,MetadataConstraints.UriManagerSet.union sigl sigr))
 290         | _ -> assert false
 291       end
 292     else
 293       None
 294  in
 295  let eqs = MetadataQuery.equations_for_goal ~dbd ?signature status in
 296  let candidates = List.map utty_of_u eqs in
 297  let candidates = List.filter is_monomorphic_eq candidates in
 298  let candidates = List.filter is_var_free candidates in
 299  let rec aux cache newmeta = function
 300     | [] -> [], newmeta, cache
 301     | (uri, term, termty)::tl ->
 302         debug_print
 303           (lazy
 304              (Printf.sprintf "Examining: %s (%s)"
 305                 (CicPp.ppterm term) (CicPp.ppterm termty)));
 306         let res, newmeta, cache =
 307           match termty with
 308           | C.Prod (name, s, t) ->
 309               (try
 310                 let saturated,cache,newmeta =
 311                   saturate_term context metasenv newmeta termty
 312                     cache auto true
 313                 in
 314                 let eqs,newmeta =
 315                   List.fold_left
 316                    (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
 317                      match head with
 318                      | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 319                        when LibraryObjects.is_eq_URI uri ->
 320                          let proof = C.Appl (term::args) in
 321                          let maxmeta, equality =
 322                            build_equality bag ty t1 t2 proof newmetas
 323                              (max newmeta newmeta')
 324                          in
 325                          equality::acc,maxmeta + 1
 326                      | _ -> assert false)
 327                    ([],newmeta) saturated
 328                 in
 329                  eqs, newmeta , cache
 330               with UnableToSaturate (cache,newmeta) ->
 331                 [], newmeta , cache)
 332           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] ->
 333               let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
 334               [e], newmeta+1, cache
 335           | _ -> assert false
 336         in
 337         let res = List.map (fun e -> uri, e) res in
 338         let tl, newmeta, cache = aux cache newmeta tl in
 339         res @ tl, newmeta, cache
 340   in
 341   let found, maxm, cache =
 342     aux cache maxmeta candidates
 343   in
 344   let uriset, eqlist =
 345     let mceq = Equality.meta_convertibility_eq in
 346     (List.fold_left
 347        (fun (s, l) (u, e) ->
 348           if List.exists (mceq e) (List.map snd l) then (
 349             debug_print
 350               (lazy
 351                  (Printf.sprintf "NO!! %s already there!"
 352                     (Equality.string_of_equality e)));
 353             (UriManager.UriSet.add u s, l)
 354           ) else (UriManager.UriSet.add u s, (u, e)::l))
 355        (UriManager.UriSet.empty, []) found)
 356   in
 357   uriset, eqlist, maxm, cache
 358 ;;
 359