components/tactics/auto.ml

   1 (* Copyright (C) 2002, 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 AutoTypes;;
  27 open AutoCache;;
  28
  29 let debug = false;;
  30 let debug_print s =
  31   if debug then prerr_endline (Lazy.force s);;
  32
  33 (* functions for retrieving theorems *)
  34
  35 exception FillingFailure of AutoCache.cache * int
  36
  37 let rec unfold context = function
  38   | Cic.Prod(name,s,t) ->
  39       let t' = unfold ((Some (name,Cic.Decl s))::context) t in
  40         Cic.Prod(name,s,t')
  41   | t -> ProofEngineReduction.unfold context t
  42
  43 let find_library_theorems dbd proof goal =
  44   let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
  45   let terms = List.map CicUtil.term_of_uri univ in
  46   List.map
  47     (fun t ->
  48        (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)))
  49     terms
  50
  51 let find_context_theorems context metasenv =
  52   let l,_ =
  53     List.fold_left
  54       (fun (res,i) ctxentry ->
  55          match ctxentry with
  56            | Some (_,Cic.Decl t) ->
  57                (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
  58            | Some (_,Cic.Def (_,Some t)) ->
  59                (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
  60            | Some (_,Cic.Def (_,None)) ->
  61                let t = Cic.Rel i in
  62                let ty,_ =
  63                  CicTypeChecker.type_of_aux'
  64                    metasenv context t CicUniv.empty_ugraph
  65                in
  66                  (t,ty)::res,i+1
  67            |  _ -> res,i+1)
  68       ([],1) context
  69   in l
  70
  71 let rec is_an_equality = function
  72   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _]
  73     when (LibraryObjects.is_eq_URI uri) -> true
  74   | Cic.Prod (_, _, t) -> is_an_equality t
  75   | _ -> false
  76 ;;
  77
  78 let partition_equalities =
  79   List.partition (fun (_,ty) -> is_an_equality ty)
  80
  81
  82 let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;;
  83
  84
  85 let is_unit_equation context metasenv oldnewmeta term =
  86   let head, metasenv, args, newmeta =
  87     TermUtil.saturate_term oldnewmeta metasenv context term 0
  88   in
  89   let propositional_args =
  90     HExtlib.filter_map
  91       (function
  92       | Cic.Meta(i,_) ->
  93           let _,_,mt = CicUtil.lookup_meta i metasenv in
  94           let sort,u =
  95             CicTypeChecker.type_of_aux' metasenv context mt
  96               CicUniv.empty_ugraph
  97           in
  98           let b, _ =
  99             CicReduction.are_convertible ~metasenv context
 100               sort (Cic.Sort Cic.Prop) u
 101           in
 102           if b then Some i else None
 103       | _ -> assert false)
 104     args
 105   in
 106     if propositional_args = [] then
 107       let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
 108         Some (args,metasenv,newmetas,head,newmeta)
 109     else None
 110 ;;
 111
 112 let get_candidates universe cache t =
 113   let candidates=
 114     (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
 115   in
 116   let debug_msg =
 117     (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^
 118              (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
 119   debug_print debug_msg;
 120   candidates
 121 ;;
 122
 123 let only signature context t =
 124   try
 125     let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
 126     let consts = MetadataConstraints.constants_of ty in
 127     let b = MetadataConstraints.UriManagerSet.subset consts signature in
 128     if b then b
 129     else
 130       try
 131         let ty' = unfold context ty in
 132         let consts' = MetadataConstraints.constants_of ty' in
 133         MetadataConstraints.UriManagerSet.subset consts' signature
 134       with _-> false
 135   with _ -> false
 136 ;;
 137
 138 let not_default_eq_term t =
 139   try
 140     let uri = CicUtil.uri_of_term t in
 141       not (LibraryObjects.in_eq_URIs uri)
 142   with Invalid_argument _ -> true
 143
 144 let retrieve_equations signature universe cache context=
 145   match LibraryObjects.eq_URI() with
 146     | None -> []
 147     | Some eq_uri ->
 148         let eq_uri = UriManager.strip_xpointer eq_uri in
 149         let fake= Cic.Meta(-1,[]) in
 150         let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
 151         let candidates = get_candidates universe cache fake_eq in
 152     (* defaults eq uris are built-in in auto *)
 153         let candidates = List.filter not_default_eq_term candidates in
 154         let candidates = List.filter (only signature context) candidates in
 155         List.iter (fun t -> prerr_endline (CicPp.ppterm t)) candidates;
 156         candidates
 157
 158 let build_equality bag head args proof newmetas maxmeta =
 159   match head with
 160   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
 161       let p =
 162         if args = [] then proof else Cic.Appl (proof::args)
 163       in
 164       let o = !Utils.compare_terms t1 t2 in
 165       let stat = (ty,t1,t2,o) in
 166       (* let w = compute_equality_weight stat in *)
 167       let w = 0 in
 168       let proof = Equality.Exact p in
 169       let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
 170       (* to clean the local context of metas *)
 171       Equality.fix_metas bag maxmeta e
 172   | _ -> assert false
 173 ;;
 174
 175 let partition_unit_equalities context metasenv newmeta bag equations =
 176   List.fold_left
 177     (fun (units,other,maxmeta)(t,ty) ->
 178        match is_unit_equation context metasenv maxmeta ty with
 179          | Some (args,metasenv,newmetas,head,newmeta') ->
 180              let maxmeta,equality =
 181                build_equality bag head args t newmetas newmeta' in
 182              equality::units,other,maxmeta
 183          | None ->
 184              units,(t,ty)::other,maxmeta)
 185     ([],[],newmeta) equations
 186
 187 let empty_tables =
 188   (Saturation.make_active [],
 189    Saturation.make_passive [],
 190    Equality.mk_equality_bag)
 191
 192 let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
 193   (* the local cache in initially empty  *)
 194   let cache = AutoCache.cache_empty in
 195   let _, metasenv, _, _, _ = proof in
 196   let signature = MetadataQuery.signature_of metasenv goal in
 197   let newmeta = CicMkImplicit.new_meta metasenv [] in
 198   let _,context,_ = CicUtil.lookup_meta goal metasenv in
 199   let ct = find_context_theorems context metasenv in
 200   prerr_endline
 201     ("ho trovato nel contesto " ^ (string_of_int (List.length ct)));
 202   let lt =
 203     if use_library then
 204        find_library_theorems dbd metasenv goal
 205     else [] in
 206   prerr_endline
 207     ("ho trovato nella libreria " ^ (string_of_int (List.length lt)));
 208   let cache = cache_add_list cache context (ct@lt) in
 209   let equations =
 210     retrieve_equations signature universe cache context in
 211   prerr_endline
 212     ("ho trovato equazioni n. " ^ (string_of_int (List.length equations)));
 213   let eqs_and_types =
 214     HExtlib.filter_map
 215       (fun t ->
 216          let ty,_ =
 217            CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
 218            (* retrieve_equations could also return flexible terms *)
 219            if is_an_equality ty then Some(t,ty)
 220            else
 221              try
 222                let ty' = unfold context ty in
 223                  if is_an_equality ty' then Some(t,ty') else None
 224              with _ -> None) (* catturare l'eccezione giusta di unfold *)
 225       equations in
 226   let bag = Equality.mk_equality_bag () in
 227   let units, other_equalities, newmeta =
 228     partition_unit_equalities context metasenv newmeta bag eqs_and_types in
 229   (* let env = (metasenv, context, CicUniv.empty_ugraph) in
 230     let equalities =
 231     let eq_uri =
 232     match LibraryObjects.eq_URI() with
 233       | None ->assert false
 234       | Some eq_uri -> eq_uri in
 235     Saturation.simplify_equalities bag eq_uri env units in *)
 236   let passive = Saturation.make_passive units in
 237   let no = List.length units in
 238   let active = Saturation.make_active [] in
 239   let active,passive,newmeta =
 240     if paramod then active,passive,newmeta
 241     else
 242       Saturation.pump_actives
 243         context bag newmeta active passive (no+1) infinity
 244   in
 245     (active,passive,bag),cache,newmeta
 246
 247 let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast =
 248   let head, metasenv, args, newmeta =
 249     TermUtil.saturate_term oldnewmeta metasenv context term 0
 250   in
 251   let propositional_args =
 252     HExtlib.filter_map
 253       (function
 254       | Cic.Meta(i,_) ->
 255           let _,_,mt = CicUtil.lookup_meta i metasenv in
 256           let sort,u =
 257             CicTypeChecker.type_of_aux' metasenv context mt
 258               CicUniv.empty_ugraph
 259           in
 260           let b, _ =
 261             CicReduction.are_convertible ~metasenv context
 262               sort (Cic.Sort Cic.Prop) u
 263           in
 264           if b then Some i else None
 265       | _ -> assert false)
 266     args
 267   in
 268   let results,cache,newmeta =
 269     if propositional_args = [] then
 270       let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
 271       [args,metasenv,newmetas,head,newmeta],cache,newmeta
 272     else
 273       (*
 274       let proof =
 275         None,metasenv,term,term (* term non e' significativo *)
 276       in *)
 277       let flags =
 278         if fast then
 279           {AutoTypes.default_flags() with
 280            AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
 281            maxwidth = 2;maxdepth = 2;
 282            use_paramod=true;use_only_paramod=false}
 283         else
 284           {AutoTypes.default_flags() with
 285            AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
 286            maxwidth = 2;maxdepth = 4;
 287            use_paramod=true;use_only_paramod=false}
 288       in
 289       match auto newmeta tables universe cache context metasenv propositional_args flags with
 290       | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
 291       | substs,cache,newmeta ->
 292           List.map
 293             (fun subst ->
 294               let metasenv =
 295                 CicMetaSubst.apply_subst_metasenv subst metasenv
 296               in
 297               let head = CicMetaSubst.apply_subst subst head in
 298               let newmetas =
 299                 List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
 300               in
 301               let args = List.map (CicMetaSubst.apply_subst subst) args in
 302               let newm = CicMkImplicit.new_meta metasenv subst in
 303                 args,metasenv,newmetas,head,max newm newmeta)
 304             substs, cache, newmeta
 305   in
 306   results,cache,newmeta
 307
 308 let build_equalities auto context metasenv tables universe cache newmeta equations =
 309   List.fold_left
 310     (fun (facts,cache,newmeta) (t,ty) ->
 311        (* in any case we add the equation to the cache *)
 312        let cache = AutoCache.cache_add_list cache context [(t,ty)] in
 313        try
 314          let saturated,cache,newmeta =
 315            fill_hypothesis context metasenv newmeta ty tables universe cache auto true
 316          in
 317          let (active,passive,bag) = tables in
 318          let eqs,bag,newmeta =
 319            List.fold_left
 320              (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') ->
 321                 let maxmeta,equality =
 322                   build_equality bag head args t newmetas newmeta'
 323                 in
 324                   equality::acc,bag,maxmeta)
 325              ([],bag,newmeta) saturated
 326          in
 327            (eqs@facts, cache, newmeta)
 328        with FillingFailure (cache,newmeta) ->
 329          (* if filling hypothesis fails we add the equation to
 330             the cache *)
 331          (facts,cache,newmeta)
 332       )
 333     ([],cache,newmeta) equations
 334
 335 let close_more tables maxmeta context status auto universe cache =
 336   let (active,passive,bag) = tables in
 337   let proof, goalno = status in
 338   let _, metasenv,_,_, _ = proof in
 339   let signature = MetadataQuery.signature_of metasenv goalno in
 340   let equations = retrieve_equations signature universe cache context in
 341   let eqs_and_types =
 342     HExtlib.filter_map
 343       (fun t ->
 344          let ty,_ =
 345            CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
 346            (* retrieve_equations could also return flexible terms *)
 347            if is_an_equality ty then Some(t,ty) else None)
 348       equations in
 349   let units, cache, maxm =
 350       build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in
 351   prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
 352     string_of_int maxm);
 353   List.iter
 354     (fun e -> prerr_endline (Equality.string_of_equality e))
 355     units;
 356   prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
 357   let passive = Saturation.add_to_passive units passive in
 358   let no = List.length units in
 359   prerr_endline ("No = " ^ (string_of_int no));
 360   let active,passive,newmeta =
 361     Saturation.pump_actives context bag maxm active passive (no+1) infinity
 362   in
 363     (active,passive,bag),cache,newmeta
 364
 365 let find_context_equalities
 366   maxmeta bag context proof (universe:Universe.universe) cache
 367 =
 368   let module C = Cic in
 369   let module S = CicSubstitution in
 370   let module T = CicTypeChecker in
 371   let _,metasenv,_,_, _ = proof in
 372   let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
 373   (* if use_auto is true, we try to close the hypothesis of equational
 374     statements using auto; a naif, and probably wrong approach *)
 375   let rec aux cache index newmeta = function
 376     | [] -> [], newmeta,cache
 377     | (Some (_, C.Decl (term)))::tl ->
 378         debug_print
 379           (lazy
 380              (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
 381         let do_find context term =
 382           match term with
 383           | C.Prod (name, s, t) when is_an_equality t ->
 384               (try
 385
 386                 let term = S.lift index term in
 387                 let saturated,cache,newmeta =
 388                   fill_hypothesis context metasenv newmeta term
 389                     empty_tables universe cache default_auto false
 390                 in
 391                 let eqs,newmeta =
 392                   List.fold_left
 393                    (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
 394                      let newmeta, equality =
 395                        build_equality
 396                          bag head args (Cic.Rel index) newmetas (max newmeta newmeta')
 397                      in
 398                      equality::acc, newmeta + 1)
 399                    ([],newmeta) saturated
 400                 in
 401                  eqs, newmeta, cache
 402               with FillingFailure (cache,newmeta) ->
 403                 [],newmeta,cache)
 404           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 405               when LibraryObjects.is_eq_URI uri ->
 406               let term = S.lift index term in
 407               let newmeta, e =
 408                 build_equality bag term [] (Cic.Rel index) [] newmeta
 409               in
 410               [e], (newmeta+1),cache
 411           | _ -> [], newmeta, cache
 412         in
 413         let eqs, newmeta, cache = do_find context term in
 414         let rest, newmeta,cache = aux cache (index+1) newmeta tl in
 415         List.map (fun x -> index,x) eqs @ rest, newmeta, cache
 416     | _::tl ->
 417         aux cache (index+1) newmeta tl
 418   in
 419   let il, maxm, cache =
 420     aux cache 1 newmeta context
 421   in
 422   let indexes, equalities = List.split il in
 423   indexes, equalities, maxm, cache
 424 ;;
 425
 426 (***************** applyS *******************)
 427
 428 let new_metasenv_and_unify_and_t
 429  dbd flags universe proof goal ?tables newmeta' metasenv'
 430  context term' ty termty goal_arity
 431 =
 432  let (consthead,newmetasenv,arguments,_) =
 433    TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
 434  let term'' =
 435    match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
 436  in
 437  let proof',oldmetasenv =
 438   let (puri,metasenv,pbo,pty, attrs) = proof in
 439    (puri,newmetasenv,pbo,pty, attrs),metasenv
 440  in
 441  let goal_for_paramod =
 442   match LibraryObjects.eq_URI () with
 443   | Some uri ->
 444       Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
 445   | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
 446  in
 447  let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
 448  let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
 449  let proof'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs in
 450  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
 451  let proof''',goals =
 452   ProofEngineTypes.apply_tactic
 453     (EqualityTactics.rewrite_tac ~direction:`RightToLeft
 454       ~pattern:(ProofEngineTypes.conclusion_pattern None)
 455         (Cic.Meta(newmeta,irl)) [])
 456    (proof'',goal)
 457  in
 458  let goal = match goals with [g] -> g | _ -> assert false in
 459  let subst, (proof'''', _), _ =
 460    PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
 461  in
 462  match
 463    let (active, passive,bag), cache, maxmeta =
 464      init_cache_and_tables dbd flags.use_library true universe (proof'''',newmeta)
 465    in
 466      Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
 467        max_int max_int flags.timeout
 468  with
 469  | None, _,_,_ ->
 470      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
 471  | Some (_,proof''''',_), active,passive,_  ->
 472      subst,proof''''',
 473      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
 474        ~newmetasenv:(let _,m,_,_, _ = proof''''' in m),  active, passive
 475 ;;
 476
 477 let rec count_prods context ty =
 478  match CicReduction.whd context ty with
 479     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
 480   | _ -> 0
 481
 482 let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
 483  let module T = CicTypeChecker in
 484  let module R = CicReduction in
 485  let module C = Cic in
 486   let (_,metasenv,_,_, _) = proof in
 487   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 488   let newmeta = CicMkImplicit.new_meta metasenv subst in
 489    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
 490     match term with
 491        C.Var (uri,exp_named_subst) ->
 492         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 493          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 494           exp_named_subst
 495         in
 496          exp_named_subst_diff,newmeta',newmetasenvfragment,
 497           C.Var (uri,exp_named_subst')
 498      | C.Const (uri,exp_named_subst) ->
 499         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 500          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 501           exp_named_subst
 502         in
 503          exp_named_subst_diff,newmeta',newmetasenvfragment,
 504           C.Const (uri,exp_named_subst')
 505      | C.MutInd (uri,tyno,exp_named_subst) ->
 506         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 507          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 508           exp_named_subst
 509         in
 510          exp_named_subst_diff,newmeta',newmetasenvfragment,
 511           C.MutInd (uri,tyno,exp_named_subst')
 512      | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 513         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 514          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 515           exp_named_subst
 516         in
 517          exp_named_subst_diff,newmeta',newmetasenvfragment,
 518           C.MutConstruct (uri,tyno,consno,exp_named_subst')
 519      | _ -> [],newmeta,[],term
 520    in
 521    let metasenv' = metasenv@newmetasenvfragment in
 522    let termty,_ =
 523      CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
 524    in
 525    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
 526    let goal_arity = count_prods context ty in
 527    let subst, proof, gl, active, passive =
 528     new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
 529      newmeta' metasenv' context term' ty termty goal_arity
 530    in
 531     subst, proof, gl, active, passive
 532 ;;
 533
 534 (****************** AUTO ********************)
 535
 536 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
 537 let ugraph = CicUniv.empty_ugraph;;
 538 let typeof = CicTypeChecker.type_of_aux';;
 539 let ppterm ctx t =
 540   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
 541   CicPp.pp t names
 542 ;;
 543 let is_in_prop context subst metasenv ty =
 544   let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
 545   fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
 546 ;;
 547
 548 let assert_proof_is_valid proof metasenv context goalty =
 549   if debug then
 550     begin
 551       let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
 552       let b,_ = CicReduction.are_convertible context ty goalty u in
 553         if not b then
 554           begin
 555             let names =
 556               List.map (function None -> None | Some (x,_) -> Some x) context
 557             in
 558               prerr_endline ("PROOF:" ^ CicPp.pp proof names);
 559               prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
 560               prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
 561               prerr_endline ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
 562           end;
 563         assert b
 564     end
 565   else ()
 566 ;;
 567
 568 let assert_subst_are_disjoint subst subst' =
 569   if debug then
 570     assert(List.for_all
 571              (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
 572              subst)
 573   else ()
 574 ;;
 575
 576 let sort_new_elems =
 577   List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
 578 ;;
 579
 580 let split_goals_in_prop metasenv subst gl =
 581   List.partition
 582     (fun g ->
 583       let _,context,ty = CicUtil.lookup_meta g metasenv in
 584       try
 585         let sort,u = typeof ~subst metasenv context ty ugraph in
 586         let b,_ =
 587           CicReduction.are_convertible
 588             ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
 589         b
 590       with
 591       | CicTypeChecker.AssertFailure s
 592       | CicTypeChecker.TypeCheckerFailure s ->
 593           debug_print
 594             (lazy (ppterm context (CicMetaSubst.apply_subst subst ty)));
 595           debug_print s;
 596           false)
 597     (* FIXME... they should type! *)
 598     gl
 599 ;;
 600
 601 let split_goals_with_metas metasenv subst gl =
 602   List.partition
 603     (fun g ->
 604       let _,context,ty = CicUtil.lookup_meta g metasenv in
 605       let ty = CicMetaSubst.apply_subst subst ty in
 606       CicUtil.is_meta_closed ty)
 607     gl
 608 ;;
 609
 610 let order_new_goals metasenv subst open_goals ppterm =
 611   let prop,rest = split_goals_in_prop metasenv subst open_goals in
 612   let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
 613   let open_goals =
 614     (List.map (fun x -> x,P) (closed_prop @ open_prop))
 615     @
 616     (List.map (fun x -> x,T) rest)
 617   in
 618   let tys =
 619     List.map
 620       (fun (i,sort) ->
 621         let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
 622   in
 623   debug_print (lazy ("   OPEN: "^
 624     String.concat "\n"
 625       (List.map
 626          (function
 627             | (i,t,P) -> string_of_int i   (* ":"^ppterm t^ "Prop" *)
 628             | (i,t,T) -> string_of_int i ) (* ":"^ppterm t^ "Type")*)
 629          tys)));
 630   open_goals
 631 ;;
 632
 633 let is_an_equational_goal = function
 634   | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
 635   | _ -> false
 636 ;;
 637
 638 let equational_case
 639   tables maxm cache depth fake_proof goalno goalty subst context
 640     flags
 641 =
 642   let active,passive,bag = tables in
 643   let ppterm = ppterm context in
 644   let status = (fake_proof,goalno) in
 645     if flags.use_only_paramod then
 646       begin
 647         prerr_endline ("PARAMODULATION SU: " ^
 648                          string_of_int goalno ^ " " ^ ppterm goalty );
 649         let goal_steps, saturation_steps, timeout = max_int,max_int,flags.timeout in
 650         match
 651           Saturation.given_clause bag maxm status active passive
 652             goal_steps saturation_steps timeout
 653         with
 654           | None, active, passive, maxmeta ->
 655               [], (active,passive,bag), cache, maxmeta, flags
 656           | Some(subst',(_,metasenv,proof,_, _),open_goals),active,passive,maxmeta ->
 657               assert_subst_are_disjoint subst subst';
 658               let subst = subst@subst' in
 659               let open_goals = order_new_goals metasenv subst open_goals ppterm in
 660               let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
 661                 [metasenv,subst,open_goals], (active,passive,bag),
 662               cache, maxmeta, flags
 663       end
 664     else
 665       begin
 666         prerr_endline ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
 667         let res, maxmeta = Saturation.all_subsumed bag maxm status active passive in
 668         assert (maxmeta >= maxm);
 669         let res' =
 670           List.map
 671             (fun subst',(_,metasenv,proof,_, _),open_goals ->
 672                assert_subst_are_disjoint subst subst';
 673                let subst = subst@subst' in
 674                let open_goals = order_new_goals metasenv subst open_goals ppterm in
 675                let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
 676                  metasenv,subst,open_goals)
 677             res in
 678           res', (active,passive,bag), cache, maxmeta, flags
 679       end
 680
 681 (*
 682   let active,passive,bag,cache,maxmeta,flags,goal_steps,saturation_steps,timeout =
 683     given_clause_params
 684       tables maxm auto cache subst flags context status in
 685   match
 686     Saturation.given_clause bag maxmeta status active passive
 687       goal_steps saturation_steps timeout
 688   with
 689   | None, active, passive, maxmeta ->
 690       None, (active,passive,bag), cache, maxmeta, flags
 691   | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta ->
 692       assert_subst_are_disjoint subst subst';
 693       let subst = subst@subst' in
 694       let open_goals = order_new_goals metasenv subst open_goals ppterm in
 695       let open_goals = List.map (fun (x,sort) -> x,depth,sort) open_goals in
 696       Some [metasenv,subst,open_goals], (active,passive,bag), cache, maxmeta, flags
 697 *)
 698 ;;
 699
 700 let try_candidate
 701   goalty tables maxm subst fake_proof goalno depth context cand
 702 =
 703   let ppterm = ppterm context in
 704   try
 705     let subst', ((_,metasenv,_,_, _), open_goals), maxmeta =
 706       PrimitiveTactics.apply_with_subst
 707         ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
 708     in
 709     debug_print (lazy ("   OK: " ^ ppterm cand));
 710     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
 711     assert_subst_are_disjoint subst subst';
 712     let subst = subst@subst' in
 713     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 714     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 715     Some (metasenv,subst,open_goals), tables , maxmeta
 716   with
 717     | ProofEngineTypes.Fail s ->
 718     (*debug_print("   KO: "^Lazy.force s);*)None,tables, maxm
 719     | CicUnification.Uncertain s ->
 720     (*debug_print("   BECCATO: "^Lazy.force s);*)None,tables, maxm
 721 ;;
 722
 723 let applicative_case
 724   tables maxm depth subst fake_proof goalno goalty metasenv context universe
 725   cache
 726 =
 727   let candidates = get_candidates universe cache goalty in
 728   let tables, elems, maxm =
 729     List.fold_left
 730       (fun (tables,elems,maxm) cand ->
 731         match
 732           try_candidate goalty
 733             tables maxm subst fake_proof goalno depth context cand
 734         with
 735         | None, tables,maxm  -> tables,elems, maxm
 736         | Some x, tables, maxm -> tables,x::elems, maxm)
 737       (tables,[],maxm) candidates
 738   in
 739   let elems = sort_new_elems elems in
 740   elems, tables, cache, maxm
 741 ;;
 742
 743 (* Works if there is no dependency over proofs *)
 744 let is_a_green_cut goalty =
 745   CicUtil.is_meta_closed goalty
 746 ;;
 747
 748 let prop = function (_,_,P) -> true | _ -> false;;
 749 let calculate_timeout flags =
 750     if flags.timeout = 0. then
 751       (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
 752     else
 753       flags
 754 ;;
 755 let is_equational_case goalty flags =
 756   let ensure_equational t =
 757     if is_an_equational_goal t then true
 758     else false
 759     (*
 760       let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
 761       raise (ProofEngineTypes.Fail (lazy msg))
 762     *)
 763   in
 764   (flags.use_paramod && is_an_equational_goal goalty) ||
 765   (flags.use_only_paramod && ensure_equational goalty)
 766 ;;
 767 let cache_add_success sort cache k v =
 768   if sort = P then cache_add_success cache k v else cache_remove_underinspection
 769   cache k
 770 ;;
 771
 772 let rec auto_main tables maxm context flags elems universe cache =
 773   let flags = calculate_timeout flags in
 774   let ppterm = ppterm context in
 775   let irl = mk_irl context in
 776   let rec aux flags tables maxm cache = function (* elems in OR *)
 777     | [] -> Fail "no more steps can be done", tables, cache, maxm
 778          (*COMPLETE FAILURE*)
 779     | (metasenv,subst,[])::tl ->
 780         Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
 781     | (metasenv,subst,goals)::tl when
 782       List.length (List.filter prop goals) > flags.maxwidth ->
 783         debug_print
 784           (lazy (" FAILURE(width): " ^ string_of_int (List.length goals)));
 785         aux flags tables maxm cache tl (* FAILURE (width) *)
 786     | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
 787         if Unix.gettimeofday() > flags.timeout then
 788           Fail "timeout",tables,cache,maxm
 789         else
 790         try
 791           let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
 792           debug_print
 793             (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty));
 794           debug_print (lazy (AutoCache.cache_print context cache));
 795           if sort = T && tl <> [] then (* FIXME!!!! *)
 796             (debug_print
 797                (lazy (" FAILURE(not in prop)"));
 798             aux flags tables maxm cache tl (* FAILURE (not in prop) *))
 799           else
 800           match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
 801           | Fail s, tables, cache, maxm' ->
 802               let maxm = maxm' in
 803               debug_print
 804                 (lazy
 805                    (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
 806               let cache =
 807                 if flags.dont_cache_failures then
 808                   cache_remove_underinspection cache goalty
 809                 else cache_add_failure cache goalty depth
 810               in
 811               aux flags tables maxm cache tl
 812           | Success (metasenv,subst,others), tables, cache, maxm' ->
 813               let maxm = maxm' in
 814               (* others are alternatives in OR *)
 815               try
 816                 let goal = Cic.Meta(goalno,irl) in
 817                 let proof = CicMetaSubst.apply_subst subst goal in
 818                 debug_print
 819                   (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
 820                 if is_a_green_cut goalty then
 821                   (assert_proof_is_valid proof metasenv context goalty;
 822                   let cache = cache_add_success sort cache goalty proof in
 823                   aux flags tables maxm cache ((metasenv,subst,gl)::tl))
 824                 else
 825                   (let goalty = CicMetaSubst.apply_subst subst goalty in
 826                   assert_proof_is_valid proof metasenv context goalty;
 827                   let cache =
 828                     if is_a_green_cut goalty then
 829                       cache_add_success sort cache goalty proof
 830                     else
 831                       cache
 832                   in
 833                   let others =
 834                     List.map
 835                       (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
 836                     others
 837                   in
 838                   aux flags tables maxm cache ((metasenv,subst,gl)::others@tl))
 839               with CicUtil.Meta_not_found i when i = goalno ->
 840                 assert false
 841         with CicUtil.Meta_not_found i when i = goalno ->
 842           (* goalno was closed by sideeffect *)
 843           debug_print
 844             (lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
 845           aux flags tables maxm cache ((metasenv,subst,gl)::tl)
 846
 847   and aux_single flags tables maxm universe cache metasenv subst (goalno, depth, _) goalty cc =
 848     let goalty = CicMetaSubst.apply_subst subst goalty in
 849 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
 850       (* FAILURE (euristic cut) *)
 851     match cache_examine cache goalty with
 852     | Failed_in d when d >= depth ->
 853         Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
 854         tables,cache,maxm(*FAILURE(depth)*)
 855     | Succeded t ->
 856         let entry = goalno, (cc, t,goalty) in
 857         assert_subst_are_disjoint subst [entry];
 858         let subst = entry :: subst in
 859         let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
 860         debug_print (lazy ("  CACHE HIT!"));
 861         Success (metasenv, subst, []), tables, cache, maxm
 862     | UnderInspection -> Fail "looping",tables,cache, maxm
 863     | Notfound
 864     | Failed_in _ when depth > 0 -> (* we have more depth now *)
 865         let cache = cache_add_underinspection cache goalty depth in
 866         let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty, [] in (* FG: attrs *)
 867         let elems, tables, cache, maxm, flags =
 868           if is_equational_case goalty flags then
 869             let elems,tables,cache,maxm1, flags =
 870               equational_case tables maxm cache
 871                 depth fake_proof goalno goalty subst context flags in
 872               let maxm = maxm1 in
 873             let more_elems, tables, cache, maxm1 =
 874               if flags.use_only_paramod then
 875                 [],tables, cache, maxm
 876               else
 877                 applicative_case
 878                   tables maxm depth subst fake_proof goalno
 879                   goalty metasenv context universe cache in
 880               let maxm = maxm1 in
 881               elems@more_elems, tables, cache, maxm, flags
 882           else
 883             let elems, tables, cache, maxm =
 884             applicative_case tables maxm depth subst fake_proof goalno
 885               goalty metasenv context universe cache in
 886             elems, tables, cache, maxm, flags
 887         in
 888         aux flags tables maxm cache elems
 889     | _ -> Fail "??",tables,cache,maxm
 890   in
 891     aux flags tables maxm cache elems
 892
 893 and
 894   auto_all_solutions maxm tables universe cache context metasenv gl flags
 895 =
 896   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 897   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 898   let elems = [metasenv,[],goals] in
 899   let rec aux tables maxm solutions cache elems flags =
 900     match auto_main tables maxm context flags elems universe cache with
 901     | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
 902     | Success (metasenv,subst,others),tables,cache,maxm ->
 903         if Unix.gettimeofday () > flags.timeout then
 904           ((subst,metasenv)::solutions), cache, maxm
 905         else
 906           aux tables maxm ((subst,metasenv)::solutions) cache others flags
 907   in
 908   let rc = aux tables maxm [] cache elems flags in
 909     match rc with
 910     | [],cache,maxm -> [],cache,maxm
 911     | solutions,cache,maxm ->
 912         let solutions =
 913           HExtlib.filter_map
 914             (fun (subst,newmetasenv) ->
 915               let opened =
 916                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
 917               in
 918               if opened = [] then Some subst else None)
 919             solutions
 920         in
 921          solutions,cache,maxm
 922 ;;
 923
 924 (* }}} ****************** AUTO ***************)
 925
 926 let auto_all tables universe cache context metasenv gl flags =
 927   let solutions, cache, _ =
 928     auto_all_solutions 0 tables universe cache context metasenv gl flags
 929   in
 930   solutions, cache
 931 ;;
 932
 933 let auto flags metasenv tables universe cache context metasenv gl =
 934   let initial_time = Unix.gettimeofday() in
 935   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 936   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 937   let elems = [metasenv,[],goals] in
 938   match auto_main tables 0 context flags elems universe cache with
 939   | Success (metasenv,subst,_), tables,cache,_ ->
 940       prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
 941       Some (subst,metasenv), cache
 942   | Fail s,tables,cache,maxm -> None,cache
 943 ;;
 944
 945 let bool params name default =
 946     try
 947       let s = List.assoc name params in
 948       if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
 949       else if s = "0" || s = "false" || s = "no" || s= "off" then false
 950       else
 951         let msg = "Unrecognized value for parameter "^name^"\n" in
 952         let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
 953         raise (ProofEngineTypes.Fail (lazy msg))
 954     with Not_found -> default
 955 ;;
 956
 957 let string params name default =
 958     try List.assoc name params with
 959     | Not_found -> default
 960 ;;
 961
 962 let int params name default =
 963     try int_of_string (List.assoc name params) with
 964     | Not_found -> default
 965     | Failure _ ->
 966         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
 967 ;;
 968
 969 let flags_of_params params ?(for_applyS=false) () =
 970  let int = int params in
 971  let bool = bool params in
 972  let close_more = bool "close_more" false in
 973  let use_paramod = bool "use_paramod" true in
 974  let use_only_paramod =
 975   if for_applyS then true else bool "paramodulation" false in
 976  let use_library = bool "library"
 977    ((AutoTypes.default_flags()).AutoTypes.use_library) in
 978  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
 979  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
 980  let timeout = int "timeout" 0 in
 981   { AutoTypes.maxdepth =
 982       if use_only_paramod then 2 else depth;
 983     AutoTypes.maxwidth = width;
 984     AutoTypes.timeout =
 985       if timeout = 0 then
 986        if for_applyS then Unix.gettimeofday () +. 30.0
 987        else
 988          infinity
 989       else
 990        Unix.gettimeofday() +. (float_of_int timeout);
 991     AutoTypes.use_library = use_library;
 992     AutoTypes.use_paramod = use_paramod;
 993     AutoTypes.use_only_paramod = use_only_paramod;
 994     AutoTypes.close_more = close_more;
 995     AutoTypes.dont_cache_failures = false;
 996   }
 997
 998 let applyS_tac ~dbd ~term ~params ~universe =
 999  ProofEngineTypes.mk_tactic
1000   (fun status ->
1001     try
1002       let _, proof, gl,_,_ =
1003        apply_smart ~dbd ~term ~subst:[] ~universe
1004         (flags_of_params params ~for_applyS:true ()) status
1005       in
1006        proof, gl
1007     with
1008     | CicUnification.UnificationFailure msg
1009     | CicTypeChecker.TypeCheckerFailure msg ->
1010         raise (ProofEngineTypes.Fail msg))
1011
1012 (* SUPERPOSITION *)
1013
1014 (* Syntax:
1015  *   auto superposition target = NAME
1016  *     [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
1017  *
1018  *  - if table is omitted no superposition will be performed
1019  *  - if demod_table is omitted no demodulation will be prformed
1020  *  - subterms_only is passed to Indexing.superposition_right
1021  *
1022  *  lists are coded using _ (example: H_H1_H2)
1023  *)
1024
1025 let eq_and_ty_of_goal = function
1026   | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1027       uri,t
1028   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1029 ;;
1030
1031 let rec find_in_ctx i name = function
1032   | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
1033   | Some (Cic.Name name', _)::tl when name = name' -> i
1034   | _::tl -> find_in_ctx (i+1) name tl
1035 ;;
1036
1037 let rec position_of i x = function
1038   | [] -> assert false
1039   | j::tl when j <> x -> position_of (i+1) x tl
1040   | _ -> i
1041 ;;
1042
1043
1044 let superposition_tac ~target ~table ~subterms_only ~demod_table status =
1045   Saturation.reset_refs();
1046   let proof,goalno = status in
1047   let curi,metasenv,pbo,pty, attrs = proof in
1048   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
1049   let eq_uri,tty = eq_and_ty_of_goal ty in
1050   let env = (metasenv, context, CicUniv.empty_ugraph) in
1051   let names = Utils.names_of_context context in
1052   let bag = Equality.mk_equality_bag () in
1053   let eq_index, equalities, maxm,cache  =
1054     find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
1055   in
1056   let eq_what =
1057     let what = find_in_ctx 1 target context in
1058     List.nth equalities (position_of 0 what eq_index)
1059   in
1060   let eq_other =
1061     if table <> "" then
1062       let other =
1063         let others = Str.split (Str.regexp "_") table in
1064         List.map (fun other -> find_in_ctx 1 other context) others
1065       in
1066       List.map
1067         (fun other -> List.nth equalities (position_of 0 other eq_index))
1068         other
1069     else
1070       []
1071   in
1072   let index = List.fold_left Indexing.index Indexing.empty eq_other in
1073   let maxm, eql =
1074     if table = "" then maxm,[eq_what] else
1075     Indexing.superposition_right bag
1076       ~subterms_only eq_uri maxm env index eq_what
1077   in
1078   prerr_endline ("Superposition right:");
1079   prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
1080   prerr_endline ("\n table: ");
1081   List.iter (fun e -> prerr_endline ("  " ^ Equality.string_of_equality e ~env)) eq_other;
1082   prerr_endline ("\n result: ");
1083   List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
1084   prerr_endline ("\n result (cut&paste): ");
1085   List.iter
1086     (fun e ->
1087       let t = Equality.term_of_equality eq_uri e in
1088       prerr_endline (CicPp.pp t names))
1089   eql;
1090   prerr_endline ("\n result proofs: ");
1091   List.iter (fun e ->
1092     prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
1093     let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
1094     Subst.ppsubst s ^ "\n" ^
1095     CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql;
1096   if demod_table <> "" then
1097     begin
1098       let eql =
1099         if eql = [] then [eq_what] else eql
1100       in
1101       let demod =
1102         let demod = Str.split (Str.regexp "_") demod_table in
1103         List.map (fun other -> find_in_ctx 1 other context) demod
1104       in
1105       let eq_demod =
1106         List.map
1107           (fun demod -> List.nth equalities (position_of 0 demod eq_index))
1108           demod
1109       in
1110       let table = List.fold_left Indexing.index Indexing.empty eq_demod in
1111       let maxm,eql =
1112         List.fold_left
1113           (fun (maxm,acc) e ->
1114             let maxm,eq =
1115               Indexing.demodulation_equality bag eq_uri maxm env table e
1116             in
1117             maxm,eq::acc)
1118           (maxm,[]) eql
1119       in
1120       let eql = List.rev eql in
1121       prerr_endline ("\n result [demod]: ");
1122       List.iter
1123         (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
1124       prerr_endline ("\n result [demod] (cut&paste): ");
1125       List.iter
1126         (fun e ->
1127           let t = Equality.term_of_equality eq_uri e in
1128           prerr_endline (CicPp.pp t names))
1129       eql;
1130     end;
1131   proof,[goalno]
1132 ;;
1133
1134 let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
1135   (* argument parsing *)
1136   let string = string params in
1137   let bool = bool params in
1138   (* hacks to debug paramod *)
1139   let superposition = bool "superposition" false in
1140   let target = string "target" "" in
1141   let table = string "table" "" in
1142   let subterms_only = bool "subterms_only" false in
1143   let demod_table = string "demod_table" "" in
1144   match superposition with
1145   | true ->
1146       (* this is the ugly hack to debug paramod *)
1147       superposition_tac
1148         ~target ~table ~subterms_only ~demod_table (proof,goal)
1149   | false ->
1150       (* this is the real auto *)
1151       let _,metasenv,_,_, _ = proof in
1152       let _,context,_ = CicUtil.lookup_meta goal metasenv in
1153       let flags = flags_of_params params () in
1154       (* just for testing *)
1155       let use_library = flags.use_library in
1156       let tables,cache,newmeta =
1157         init_cache_and_tables dbd use_library flags.use_only_paramod
1158           universe (proof, goal) in
1159       let tables,cache,newmeta =
1160         if flags.close_more then
1161           close_more
1162             tables newmeta context (proof, goal) auto_all_solutions universe cache
1163         else tables,cache,newmeta in
1164       let initial_time = Unix.gettimeofday() in
1165       let (_,oldmetasenv,_,_, _) = proof in
1166       let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
1167       match auto_main tables newmeta context flags [elem] universe cache with
1168         | Success (metasenv,subst,_), tables,cache,_ ->
1169             prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
1170             let proof,metasenv =
1171             ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1172               proof goal (CicMetaSubst.apply_subst subst) metasenv
1173             in
1174             let opened =
1175               ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1176                 ~newmetasenv:metasenv
1177             in
1178               proof,opened
1179         | Fail s,tables,cache,maxm ->
1180             raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1181 ;;
1182
1183 let auto_tac ~dbd ~params ~universe =
1184   ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1185
1186 let eq_of_goal = function
1187   | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1188       uri
1189   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1190 ;;
1191
1192 (* DEMODULATE *)
1193 let demodulate_tac ~dbd ~universe (proof,goal)=
1194   let curi,metasenv,pbo,pty, attrs = proof in
1195   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1196   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1197   let initgoal = [], [], ty in
1198   let eq_uri = eq_of_goal ty in
1199   let (active,passive,bag), cache, maxm =
1200      init_cache_and_tables dbd false true universe (proof,goal) in
1201   let equalities = (Saturation.list_of_passive passive) in
1202   (* we demodulate using both actives passives *)
1203   let table =
1204     List.fold_left
1205       (fun tbl eq -> Indexing.index tbl eq)
1206       (snd active) equalities
1207   in
1208   let changed,(newproof,newmetasenv, newty) =
1209     Indexing.demodulation_goal bag
1210       (metasenv,context,CicUniv.empty_ugraph) table initgoal
1211   in
1212   if changed then
1213     begin
1214       let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1215       let proofterm,_ =
1216         Equality.build_goal_proof bag
1217           eq_uri newproof opengoal ty [] context metasenv
1218       in
1219         let extended_metasenv = (maxm,context,newty)::metasenv in
1220         let extended_status =
1221           (curi,extended_metasenv,pbo,pty, attrs),goal in
1222         let (status,newgoals) =
1223           ProofEngineTypes.apply_tactic
1224             (PrimitiveTactics.apply_tac ~term:proofterm)
1225             extended_status in
1226         (status,maxm::newgoals)
1227     end
1228   else (* if newty = ty then *)
1229     raise (ProofEngineTypes.Fail (lazy "no progress"))
1230   (*else ProofEngineTypes.apply_tactic
1231     (ReductionTactics.simpl_tac
1232       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1233 ;;
1234
1235 let demodulate_tac ~dbd ~universe =
1236   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
1237
1238
1239