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