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