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