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 (_,depth,P) -> depth < 9 | _ -> false;;
 749
 750 let calculate_timeout flags =
 751     if flags.timeout = 0. then
 752       (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
 753     else
 754       flags
 755 ;;
 756 let is_equational_case goalty flags =
 757   let ensure_equational t =
 758     if is_an_equational_goal t then true
 759     else false
 760     (*
 761       let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
 762       raise (ProofEngineTypes.Fail (lazy msg))
 763     *)
 764   in
 765   (flags.use_paramod && is_an_equational_goal goalty) ||
 766   (flags.use_only_paramod && ensure_equational goalty)
 767 ;;
 768 let cache_add_success sort cache k v =
 769   if sort = P then cache_add_success cache k v else cache_remove_underinspection
 770   cache k
 771 ;;
 772
 773 let rec auto_main tables maxm context flags elems universe cache =
 774   let flags = calculate_timeout flags in
 775   let ppterm = ppterm context in
 776   let irl = mk_irl context in
 777   let rec aux flags tables maxm cache = function (* elems in OR *)
 778     | [] -> Fail "no more steps can be done", tables, cache, maxm
 779          (*COMPLETE FAILURE*)
 780     | (metasenv,subst,[])::tl ->
 781         Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
 782     | (metasenv,subst,goals)::tl when
 783       List.length (List.filter prop goals) > flags.maxwidth ->
 784         debug_print
 785           (lazy (" FAILURE(width): " ^ string_of_int (List.length goals)));
 786         aux flags tables maxm cache tl (* FAILURE (width) *)
 787     | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
 788         if Unix.gettimeofday() > flags.timeout then
 789           Fail "timeout",tables,cache,maxm
 790         else
 791         try
 792           let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
 793           debug_print
 794             (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty ^
 795                    "with depth"^string_of_int depth));
 796           debug_print (lazy (AutoCache.cache_print context cache));
 797           if sort = T (* && tl <> []*)  then
 798           aux flags tables maxm cache ((metasenv,subst,gl)::tl)
 799           (* Success (metasenv,subst,tl), tables, cache,maxm *)
 800           (*
 801             (debug_print
 802                (lazy (" FAILURE(not in prop)"));
 803             aux flags tables maxm cache tl (* FAILURE (not in prop) *)) *)
 804           else
 805           match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
 806           | Fail s, tables, cache, maxm' ->
 807               let maxm = maxm' in
 808               debug_print
 809                 (lazy
 810                    (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
 811               let cache =
 812                 if flags.dont_cache_failures then
 813                   cache_remove_underinspection cache goalty
 814                 else cache_add_failure cache goalty depth
 815               in
 816               aux flags tables maxm cache tl
 817           | Success (metasenv,subst,others), tables, cache, maxm' ->
 818               let maxm = maxm' in
 819               (* others are alternatives in OR *)
 820               try
 821                 let goal = Cic.Meta(goalno,irl) in
 822                 let proof = CicMetaSubst.apply_subst subst goal in
 823                 debug_print
 824                   (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
 825                 if is_a_green_cut goalty then
 826                   (* assert_proof_is_valid proof metasenv context goalty; *)
 827                   let cache = cache_add_success sort cache goalty proof in
 828                   aux flags tables maxm cache ((metasenv,subst,gl)::tl)
 829                 else
 830                   (let goalty = CicMetaSubst.apply_subst subst goalty in
 831                  (* assert_proof_is_valid proof metasenv context goalty; *)
 832                   let cache =
 833                     if is_a_green_cut goalty then
 834                       cache_add_success sort cache goalty proof
 835                     else
 836                       cache
 837                   in
 838                   let others =
 839                     List.map
 840                       (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
 841                     others
 842                   in
 843                   aux flags tables maxm cache ((metasenv,subst,gl)::others@tl))
 844               with CicUtil.Meta_not_found i when i = goalno ->
 845                 assert false
 846         with CicUtil.Meta_not_found i when i = goalno ->
 847           (* goalno was closed by sideeffect *)
 848           debug_print
 849             (lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
 850           aux flags tables maxm cache ((metasenv,subst,gl)::tl)
 851
 852   and aux_single flags tables maxm universe cache metasenv subst (goalno, depth, _) goalty cc =
 853     (* let flags = if depth < 10 then {flags with maxwidth=3} else flags in *)
 854     let goalty = CicMetaSubst.apply_subst subst goalty in
 855 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
 856       (* FAILURE (euristic cut) *)
 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 ->
 869         (* assert (not (is_a_green_cut goalty)); *)
 870         Fail "looping",tables,cache, maxm
 871     | Notfound
 872     | Failed_in _ when depth > 0 -> (* we have more depth now *)
 873         let cache = cache_add_underinspection cache goalty depth in
 874         let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty, [] in (* FG: attrs *)
 875         let elems, tables, cache, maxm, flags =
 876           if is_equational_case goalty flags then
 877             let elems,tables,cache,maxm1, flags =
 878               equational_case tables maxm cache
 879                 depth fake_proof goalno goalty subst context flags in
 880               let maxm = maxm1 in
 881             let more_elems, tables, cache, maxm1 =
 882               if flags.use_only_paramod then
 883                 [],tables, cache, maxm
 884               else
 885                 applicative_case
 886                   tables maxm depth subst fake_proof goalno
 887                   goalty metasenv context universe cache in
 888               let maxm = maxm1 in
 889               elems@more_elems, tables, cache, maxm, flags
 890           else
 891             let elems, tables, cache, maxm =
 892             applicative_case tables maxm depth subst fake_proof goalno
 893               goalty metasenv context universe cache in
 894             elems, tables, cache, maxm, flags
 895         in
 896         aux flags tables maxm cache elems
 897     | _ -> Fail "depth = 0",tables,cache,maxm
 898   in
 899     aux flags tables maxm cache elems
 900
 901 and
 902   auto_all_solutions maxm tables universe cache context metasenv gl flags
 903 =
 904   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 905   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 906   let elems = [metasenv,[],goals] in
 907   let rec aux tables maxm solutions cache elems flags =
 908     match auto_main tables maxm context flags elems universe cache with
 909     | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
 910     | Success (metasenv,subst,others),tables,cache,maxm ->
 911         if Unix.gettimeofday () > flags.timeout then
 912           ((subst,metasenv)::solutions), cache, maxm
 913         else
 914           aux tables maxm ((subst,metasenv)::solutions) cache others flags
 915   in
 916   let rc = aux tables maxm [] cache elems flags in
 917     match rc with
 918     | [],cache,maxm -> [],cache,maxm
 919     | solutions,cache,maxm ->
 920         let solutions =
 921           HExtlib.filter_map
 922             (fun (subst,newmetasenv) ->
 923               let opened =
 924                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
 925               in
 926               if opened = [] then Some subst else None)
 927             solutions
 928         in
 929          solutions,cache,maxm
 930 ;;
 931
 932 (* }}} ****************** AUTO ***************)
 933
 934 let auto_all tables universe cache context metasenv gl flags =
 935   let solutions, cache, _ =
 936     auto_all_solutions 0 tables universe cache context metasenv gl flags
 937   in
 938   solutions, cache
 939 ;;
 940
 941 let auto flags metasenv tables universe cache context metasenv gl =
 942   let initial_time = Unix.gettimeofday() in
 943   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 944   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 945   let elems = [metasenv,[],goals] in
 946   match auto_main tables 0 context flags elems universe cache with
 947   | Success (metasenv,subst,_), tables,cache,_ ->
 948       prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
 949       Some (subst,metasenv), cache
 950   | Fail s,tables,cache,maxm -> None,cache
 951 ;;
 952
 953 let bool params name default =
 954     try
 955       let s = List.assoc name params in
 956       if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
 957       else if s = "0" || s = "false" || s = "no" || s= "off" then false
 958       else
 959         let msg = "Unrecognized value for parameter "^name^"\n" in
 960         let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
 961         raise (ProofEngineTypes.Fail (lazy msg))
 962     with Not_found -> default
 963 ;;
 964
 965 let string params name default =
 966     try List.assoc name params with
 967     | Not_found -> default
 968 ;;
 969
 970 let int params name default =
 971     try int_of_string (List.assoc name params) with
 972     | Not_found -> default
 973     | Failure _ ->
 974         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
 975 ;;
 976
 977 let flags_of_params params ?(for_applyS=false) () =
 978  let int = int params in
 979  let bool = bool params in
 980  let close_more = bool "close_more" false in
 981  let use_paramod = bool "use_paramod" true in
 982  let use_only_paramod =
 983   if for_applyS then true else bool "paramodulation" false in
 984  let use_library = bool "library"
 985    ((AutoTypes.default_flags()).AutoTypes.use_library) in
 986  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
 987  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
 988  let timeout = int "timeout" 0 in
 989   { AutoTypes.maxdepth =
 990       if use_only_paramod then 2 else depth;
 991     AutoTypes.maxwidth = width;
 992     AutoTypes.timeout =
 993       if timeout = 0 then
 994        if for_applyS then Unix.gettimeofday () +. 30.0
 995        else
 996          infinity
 997       else
 998        Unix.gettimeofday() +. (float_of_int timeout);
 999     AutoTypes.use_library = use_library;
1000     AutoTypes.use_paramod = use_paramod;
1001     AutoTypes.use_only_paramod = use_only_paramod;
1002     AutoTypes.close_more = close_more;
1003     AutoTypes.dont_cache_failures = false;
1004   }
1005
1006 let applyS_tac ~dbd ~term ~params ~universe =
1007  ProofEngineTypes.mk_tactic
1008   (fun status ->
1009     try
1010       let _, proof, gl,_,_ =
1011        apply_smart ~dbd ~term ~subst:[] ~universe
1012         (flags_of_params params ~for_applyS:true ()) status
1013       in
1014        proof, gl
1015     with
1016     | CicUnification.UnificationFailure msg
1017     | CicTypeChecker.TypeCheckerFailure msg ->
1018         raise (ProofEngineTypes.Fail msg))
1019
1020 (* SUPERPOSITION *)
1021
1022 (* Syntax:
1023  *   auto superposition target = NAME
1024  *     [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
1025  *
1026  *  - if table is omitted no superposition will be performed
1027  *  - if demod_table is omitted no demodulation will be prformed
1028  *  - subterms_only is passed to Indexing.superposition_right
1029  *
1030  *  lists are coded using _ (example: H_H1_H2)
1031  *)
1032
1033 let eq_and_ty_of_goal = function
1034   | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1035       uri,t
1036   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1037 ;;
1038
1039 let rec find_in_ctx i name = function
1040   | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
1041   | Some (Cic.Name name', _)::tl when name = name' -> i
1042   | _::tl -> find_in_ctx (i+1) name tl
1043 ;;
1044
1045 let rec position_of i x = function
1046   | [] -> assert false
1047   | j::tl when j <> x -> position_of (i+1) x tl
1048   | _ -> i
1049 ;;
1050
1051
1052 let superposition_tac ~target ~table ~subterms_only ~demod_table status =
1053   Saturation.reset_refs();
1054   let proof,goalno = status in
1055   let curi,metasenv,pbo,pty, attrs = proof in
1056   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
1057   let eq_uri,tty = eq_and_ty_of_goal ty in
1058   let env = (metasenv, context, CicUniv.empty_ugraph) in
1059   let names = Utils.names_of_context context in
1060   let bag = Equality.mk_equality_bag () in
1061   let eq_index, equalities, maxm,cache  =
1062     find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
1063   in
1064   let eq_what =
1065     let what = find_in_ctx 1 target context in
1066     List.nth equalities (position_of 0 what eq_index)
1067   in
1068   let eq_other =
1069     if table <> "" then
1070       let other =
1071         let others = Str.split (Str.regexp "_") table in
1072         List.map (fun other -> find_in_ctx 1 other context) others
1073       in
1074       List.map
1075         (fun other -> List.nth equalities (position_of 0 other eq_index))
1076         other
1077     else
1078       []
1079   in
1080   let index = List.fold_left Indexing.index Indexing.empty eq_other in
1081   let maxm, eql =
1082     if table = "" then maxm,[eq_what] else
1083     Indexing.superposition_right bag
1084       ~subterms_only eq_uri maxm env index eq_what
1085   in
1086   prerr_endline ("Superposition right:");
1087   prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
1088   prerr_endline ("\n table: ");
1089   List.iter (fun e -> prerr_endline ("  " ^ Equality.string_of_equality e ~env)) eq_other;
1090   prerr_endline ("\n result: ");
1091   List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
1092   prerr_endline ("\n result (cut&paste): ");
1093   List.iter
1094     (fun e ->
1095       let t = Equality.term_of_equality eq_uri e in
1096       prerr_endline (CicPp.pp t names))
1097   eql;
1098   prerr_endline ("\n result proofs: ");
1099   List.iter (fun e ->
1100     prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
1101     let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
1102     Subst.ppsubst s ^ "\n" ^
1103     CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql;
1104   if demod_table <> "" then
1105     begin
1106       let eql =
1107         if eql = [] then [eq_what] else eql
1108       in
1109       let demod =
1110         let demod = Str.split (Str.regexp "_") demod_table in
1111         List.map (fun other -> find_in_ctx 1 other context) demod
1112       in
1113       let eq_demod =
1114         List.map
1115           (fun demod -> List.nth equalities (position_of 0 demod eq_index))
1116           demod
1117       in
1118       let table = List.fold_left Indexing.index Indexing.empty eq_demod in
1119       let maxm,eql =
1120         List.fold_left
1121           (fun (maxm,acc) e ->
1122             let maxm,eq =
1123               Indexing.demodulation_equality bag eq_uri maxm env table e
1124             in
1125             maxm,eq::acc)
1126           (maxm,[]) eql
1127       in
1128       let eql = List.rev eql in
1129       prerr_endline ("\n result [demod]: ");
1130       List.iter
1131         (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
1132       prerr_endline ("\n result [demod] (cut&paste): ");
1133       List.iter
1134         (fun e ->
1135           let t = Equality.term_of_equality eq_uri e in
1136           prerr_endline (CicPp.pp t names))
1137       eql;
1138     end;
1139   proof,[goalno]
1140 ;;
1141
1142 let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
1143   (* argument parsing *)
1144   let string = string params in
1145   let bool = bool params in
1146   (* hacks to debug paramod *)
1147   let superposition = bool "superposition" false in
1148   let target = string "target" "" in
1149   let table = string "table" "" in
1150   let subterms_only = bool "subterms_only" false in
1151   let demod_table = string "demod_table" "" in
1152   match superposition with
1153   | true ->
1154       (* this is the ugly hack to debug paramod *)
1155       superposition_tac
1156         ~target ~table ~subterms_only ~demod_table (proof,goal)
1157   | false ->
1158       (* this is the real auto *)
1159       let _,metasenv,_,_, _ = proof in
1160       let _,context,_ = CicUtil.lookup_meta goal metasenv in
1161       let flags = flags_of_params params () in
1162       (* just for testing *)
1163       let use_library = flags.use_library in
1164       let tables,cache,newmeta =
1165         init_cache_and_tables dbd use_library flags.use_only_paramod
1166           universe (proof, goal) in
1167       let tables,cache,newmeta =
1168         if flags.close_more then
1169           close_more
1170             tables newmeta context (proof, goal) auto_all_solutions universe cache
1171         else tables,cache,newmeta in
1172       let initial_time = Unix.gettimeofday() in
1173       let (_,oldmetasenv,_,_, _) = proof in
1174       let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
1175       match auto_main tables newmeta context flags [elem] universe cache with
1176         | Success (metasenv,subst,_), tables,cache,_ ->
1177             prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
1178             let proof,metasenv =
1179             ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1180               proof goal (CicMetaSubst.apply_subst subst) metasenv
1181             in
1182             let opened =
1183               ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1184                 ~newmetasenv:metasenv
1185             in
1186               proof,opened
1187         | Fail s,tables,cache,maxm ->
1188             raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1189 ;;
1190
1191 let auto_tac ~dbd ~params ~universe =
1192   ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1193
1194 let eq_of_goal = function
1195   | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1196       uri
1197   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1198 ;;
1199
1200 (* DEMODULATE *)
1201 let demodulate_tac ~dbd ~universe (proof,goal)=
1202   let curi,metasenv,pbo,pty, attrs = proof in
1203   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1204   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1205   let initgoal = [], [], ty in
1206   let eq_uri = eq_of_goal ty in
1207   let (active,passive,bag), cache, maxm =
1208      init_cache_and_tables dbd false true universe (proof,goal) in
1209   let equalities = (Saturation.list_of_passive passive) in
1210   (* we demodulate using both actives passives *)
1211   let table =
1212     List.fold_left
1213       (fun tbl eq -> Indexing.index tbl eq)
1214       (snd active) equalities
1215   in
1216   let changed,(newproof,newmetasenv, newty) =
1217     Indexing.demodulation_goal bag
1218       (metasenv,context,CicUniv.empty_ugraph) table initgoal
1219   in
1220   if changed then
1221     begin
1222       let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1223       let proofterm,_ =
1224         Equality.build_goal_proof bag
1225           eq_uri newproof opengoal ty [] context metasenv
1226       in
1227         let extended_metasenv = (maxm,context,newty)::metasenv in
1228         let extended_status =
1229           (curi,extended_metasenv,pbo,pty, attrs),goal in
1230         let (status,newgoals) =
1231           ProofEngineTypes.apply_tactic
1232             (PrimitiveTactics.apply_tac ~term:proofterm)
1233             extended_status in
1234         (status,maxm::newgoals)
1235     end
1236   else (* if newty = ty then *)
1237     raise (ProofEngineTypes.Fail (lazy "no progress"))
1238   (*else ProofEngineTypes.apply_tactic
1239     (ReductionTactics.simpl_tac
1240       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1241 ;;
1242
1243 let demodulate_tac ~dbd ~universe =
1244   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
1245
1246
1247