helm/software/components/tactics/auto.ml

   1 (* Copyright (C) 2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 open AutoTypes;;
  27 open AutoCache;;
  28
  29 let debug = false;;
  30 let debug_print s =
  31   if debug then prerr_endline (Lazy.force s);;
  32
  33 let elems = ref [] ;;
  34
  35 (* closing a term w.r.t. its metavariables
  36    very naif version: it does not take dependencies properly into account *)
  37
  38 let naif_closure ?(prefix_name="xxx_") t metasenv context =
  39   let metasenv = ProofEngineHelpers.sort_metasenv metasenv in
  40   let n = List.length metasenv in
  41   let what = List.map (fun (i,cc,ty) -> Cic.Meta(i,[])) metasenv in
  42   let _,with_what =
  43     List.fold_left
  44       (fun (i,acc) (_,cc,ty) -> (i-1,Cic.Rel i::acc))
  45       (n,[]) metasenv
  46   in
  47   let t = CicSubstitution.lift n t in
  48   let body =
  49     ProofEngineReduction.replace_lifting
  50       ~equality:(fun c t1 t2 ->
  51          match t1,t2 with
  52          | Cic.Meta(i,_),Cic.Meta(j,_) -> i = j
  53          | _ -> false)
  54       ~context ~what ~with_what ~where:t
  55   in
  56   let _, t =
  57     List.fold_left
  58       (fun (n,t) (_,cc,ty) ->
  59         n-1, Cic.Lambda(Cic.Name (prefix_name^string_of_int n),
  60                CicSubstitution.lift n ty,t))
  61       (n-1,body) metasenv
  62   in
  63   t
  64 ;;
  65
  66 let lambda_close ?prefix_name t menv ctx =
  67   let t = naif_closure ?prefix_name t menv ctx in
  68     List.fold_left
  69       (fun (t,i) -> function
  70         | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *)
  71         | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1
  72         | Some (name, Cic.Def (bo, ty)) -> Cic.LetIn (name, bo, ty, t),i+1)
  73       (t,List.length menv) ctx
  74 ;;
  75
  76 (* functions for retrieving theorems *)
  77
  78 exception FillingFailure of AutoCache.cache * int
  79
  80 let rec unfold context = function
  81   | Cic.Prod(name,s,t) ->
  82       let t' = unfold ((Some (name,Cic.Decl s))::context) t in
  83         Cic.Prod(name,s,t')
  84   | t -> ProofEngineReduction.unfold context t
  85
  86 let find_library_theorems dbd proof goal =
  87   let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
  88   let terms = List.map CicUtil.term_of_uri univ in
  89   List.map
  90     (fun t ->
  91        (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)))
  92     terms
  93
  94 let find_context_theorems context metasenv =
  95   let l,_ =
  96     List.fold_left
  97       (fun (res,i) ctxentry ->
  98          match ctxentry with
  99            | Some (_,Cic.Decl t) ->
 100                (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
 101            | Some (_,Cic.Def (_,t)) ->
 102                (Cic.Rel i, CicSubstitution.lift i t)::res,i+1
 103            | None -> res,i+1)
 104       ([],1) context
 105   in l
 106
 107 let rec is_an_equality = function
 108   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _]
 109     when (LibraryObjects.is_eq_URI uri) -> true
 110   | Cic.Prod (_, _, t) -> is_an_equality t
 111   | _ -> false
 112 ;;
 113
 114 let partition_equalities =
 115   List.partition (fun (_,ty) -> is_an_equality ty)
 116
 117
 118 let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;;
 119
 120
 121 let is_unit_equation context metasenv oldnewmeta term =
 122   let head, metasenv, args, newmeta =
 123     TermUtil.saturate_term oldnewmeta metasenv context term 0
 124   in
 125   let propositional_args =
 126     HExtlib.filter_map
 127       (function
 128       | Cic.Meta(i,_) ->
 129           let _,_,mt = CicUtil.lookup_meta i metasenv in
 130           let sort,u =
 131             CicTypeChecker.type_of_aux' metasenv context mt
 132               CicUniv.empty_ugraph
 133           in
 134           let b, _ =
 135             CicReduction.are_convertible ~metasenv context
 136               sort (Cic.Sort Cic.Prop) u
 137           in
 138           if b then Some i else None
 139       | _ -> assert false)
 140     args
 141   in
 142     if propositional_args = [] then
 143       let newmetas =
 144         List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv
 145       in
 146         Some (args,metasenv,newmetas,head,newmeta)
 147     else None
 148 ;;
 149
 150 let get_candidates universe cache t =
 151   let candidates=
 152     (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
 153   in
 154   let debug_msg =
 155     (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^
 156              (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
 157   debug_print debug_msg;
 158   candidates
 159 ;;
 160
 161 let only signature context metasenv t =
 162   try
 163     let ty,_ =
 164       CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph
 165     in
 166     let consts = MetadataConstraints.constants_of ty in
 167     let b = MetadataConstraints.UriManagerSet.subset consts signature in
 168     if b then b
 169     else
 170       let ty' = unfold context ty in
 171       let consts' = MetadataConstraints.constants_of ty' in
 172       MetadataConstraints.UriManagerSet.subset consts' signature
 173   with
 174   | CicTypeChecker.TypeCheckerFailure _ -> assert false
 175   | ProofEngineTypes.Fail _ -> false (* unfold may fail *)
 176 ;;
 177
 178 let not_default_eq_term t =
 179   try
 180     let uri = CicUtil.uri_of_term t in
 181       not (LibraryObjects.in_eq_URIs uri)
 182   with Invalid_argument _ -> true
 183
 184 let retrieve_equations dont_filter signature universe cache context metasenv =
 185   match LibraryObjects.eq_URI() with
 186     | None -> []
 187     | Some eq_uri ->
 188         let eq_uri = UriManager.strip_xpointer eq_uri in
 189         let fake= Cic.Meta(-1,[]) in
 190         let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
 191         let candidates = get_candidates universe cache fake_eq in
 192         if dont_filter then candidates
 193         else
 194           let candidates = List.filter not_default_eq_term candidates in
 195           List.filter (only signature context metasenv) candidates
 196
 197 let build_equality bag head args proof newmetas maxmeta =
 198   match head with
 199   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
 200       let p =
 201         if args = [] then proof else Cic.Appl (proof::args)
 202       in
 203       let o = !Utils.compare_terms t1 t2 in
 204       let stat = (ty,t1,t2,o) in
 205       (* let w = compute_equality_weight stat in *)
 206       let w = 0 in
 207       let proof = Equality.Exact p in
 208       let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
 209       (* to clean the local context of metas *)
 210       Equality.fix_metas bag maxmeta e
 211   | _ -> assert false
 212 ;;
 213
 214 let partition_unit_equalities context metasenv newmeta bag equations =
 215   List.fold_left
 216     (fun (units,other,maxmeta)(t,ty) ->
 217        if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then
 218          let _ =
 219            HLog.warn
 220            ("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context
 221              ^ " since it is not meta closed")
 222          in
 223          units,(t,ty)::other,maxmeta
 224        else
 225        match is_unit_equation context metasenv maxmeta ty with
 226          | Some (args,metasenv,newmetas,head,newmeta') ->
 227              let maxmeta,equality =
 228                build_equality bag head args t newmetas newmeta' in
 229              equality::units,other,maxmeta
 230          | None ->
 231              units,(t,ty)::other,maxmeta)
 232     ([],[],newmeta) equations
 233
 234 let empty_tables =
 235   (Saturation.make_active [],
 236    Saturation.make_passive [],
 237    Equality.mk_equality_bag)
 238
 239 let init_cache_and_tables
 240   ?dbd use_library paramod use_context dont_filter universe (proof, goal)
 241 =
 242   (* the local cache in initially empty  *)
 243   let cache = AutoCache.cache_empty in
 244   let _, metasenv, _subst,_, _, _ = proof in
 245   let signature = MetadataQuery.signature_of metasenv goal in
 246   let newmeta = CicMkImplicit.new_meta metasenv [] in
 247   let _,context,_ = CicUtil.lookup_meta goal metasenv in
 248   let ct = if use_context then find_context_theorems context metasenv else [] in
 249   debug_print
 250     (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct))));
 251   let lt =
 252     match use_library, dbd with
 253     | true, Some dbd -> find_library_theorems dbd metasenv goal
 254     | _ -> []
 255   in
 256   debug_print
 257     (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
 258   let cache = cache_add_list cache context (ct@lt) in
 259   let equations =
 260     retrieve_equations dont_filter signature universe cache context metasenv
 261   in
 262   debug_print
 263     (lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
 264   let eqs_and_types =
 265     HExtlib.filter_map
 266       (fun t ->
 267          let ty,_ =
 268            CicTypeChecker.type_of_aux'
 269              metasenv context t CicUniv.empty_ugraph
 270          in
 271          (* retrieve_equations could also return flexible terms *)
 272          if is_an_equality ty then Some(t,ty)
 273          else
 274            try
 275              let ty' = unfold context ty in
 276              if is_an_equality ty' then Some(t,ty') else None
 277            with ProofEngineTypes.Fail _ -> None)
 278       equations
 279   in
 280   let bag = Equality.mk_equality_bag () in
 281   let units, other_equalities, newmeta =
 282     partition_unit_equalities context metasenv newmeta bag eqs_and_types
 283   in
 284   (* SIMPLIFICATION STEP
 285   let equalities =
 286     let env = (metasenv, context, CicUniv.empty_ugraph) in
 287     let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
 288     Saturation.simplify_equalities bag eq_uri env units
 289   in
 290   *)
 291   let passive = Saturation.make_passive units in
 292   let no = List.length units in
 293   let active = Saturation.make_active [] in
 294   let active,passive,newmeta =
 295     if paramod then active,passive,newmeta
 296     else
 297       Saturation.pump_actives
 298         context bag newmeta active passive (no+1) infinity
 299   in
 300     (active,passive,bag),cache,newmeta
 301
 302 let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast =
 303   let head, metasenv, args, newmeta =
 304     TermUtil.saturate_term oldnewmeta metasenv context term 0
 305   in
 306   let propositional_args =
 307     HExtlib.filter_map
 308       (function
 309       | Cic.Meta(i,_) ->
 310           let _,_,mt = CicUtil.lookup_meta i metasenv in
 311           let sort,u =
 312             CicTypeChecker.type_of_aux' metasenv context mt
 313               CicUniv.empty_ugraph
 314           in
 315           let b, _ =
 316             CicReduction.are_convertible ~metasenv context
 317               sort (Cic.Sort Cic.Prop) u
 318           in
 319           if b then Some i else None
 320       | _ -> assert false)
 321     args
 322   in
 323   let results,cache,newmeta =
 324     if propositional_args = [] then
 325       let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
 326       [args,metasenv,newmetas,head,newmeta],cache,newmeta
 327     else
 328       (*
 329       let proof =
 330         None,metasenv,term,term (* term non e' significativo *)
 331       in *)
 332       let flags =
 333         if fast then
 334           {AutoTypes.default_flags() with
 335            AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
 336            maxwidth = 2;maxdepth = 2;
 337            use_paramod=true;use_only_paramod=false}
 338         else
 339           {AutoTypes.default_flags() with
 340            AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
 341            maxwidth = 2;maxdepth = 4;
 342            use_paramod=true;use_only_paramod=false}
 343       in
 344       match auto newmeta tables universe cache context metasenv propositional_args flags with
 345       | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
 346       | substs,cache,newmeta ->
 347           List.map
 348             (fun subst ->
 349               let metasenv =
 350                 CicMetaSubst.apply_subst_metasenv subst metasenv
 351               in
 352               let head = CicMetaSubst.apply_subst subst head in
 353               let newmetas =
 354                 List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
 355               in
 356               let args = List.map (CicMetaSubst.apply_subst subst) args in
 357               let newm = CicMkImplicit.new_meta metasenv subst in
 358                 args,metasenv,newmetas,head,max newm newmeta)
 359             substs, cache, newmeta
 360   in
 361   results,cache,newmeta
 362
 363 let build_equalities auto context metasenv tables universe cache newmeta equations =
 364   List.fold_left
 365     (fun (facts,cache,newmeta) (t,ty) ->
 366        (* in any case we add the equation to the cache *)
 367        let cache = AutoCache.cache_add_list cache context [(t,ty)] in
 368        try
 369          let saturated,cache,newmeta =
 370            fill_hypothesis context metasenv newmeta ty tables universe cache auto true
 371          in
 372          let (active,passive,bag) = tables in
 373          let eqs,bag,newmeta =
 374            List.fold_left
 375              (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') ->
 376                 let maxmeta,equality =
 377                   build_equality bag head args t newmetas newmeta'
 378                 in
 379                   equality::acc,bag,maxmeta)
 380              ([],bag,newmeta) saturated
 381          in
 382            (eqs@facts, cache, newmeta)
 383        with FillingFailure (cache,newmeta) ->
 384          (* if filling hypothesis fails we add the equation to
 385             the cache *)
 386          (facts,cache,newmeta)
 387       )
 388     ([],cache,newmeta) equations
 389
 390 let close_more tables maxmeta context status auto universe cache =
 391   let (active,passive,bag) = tables in
 392   let proof, goalno = status in
 393   let _, metasenv,_subst,_,_, _ = proof in
 394   let signature = MetadataQuery.signature_of metasenv goalno in
 395   let equations =
 396     retrieve_equations false signature universe cache context metasenv
 397   in
 398   let eqs_and_types =
 399     HExtlib.filter_map
 400       (fun t ->
 401          let ty,_ =
 402            CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
 403            (* retrieve_equations could also return flexible terms *)
 404            if is_an_equality ty then Some(t,ty) else None)
 405       equations in
 406   let units, cache, maxm =
 407       build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in
 408   debug_print (lazy (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
 409     string_of_int maxm));
 410   List.iter
 411     (fun e -> debug_print (lazy (Equality.string_of_equality e)))
 412     units;
 413   debug_print (lazy ">>>>>>>>>>>>>>>>>>>>>>");
 414   let passive = Saturation.add_to_passive units passive in
 415   let no = List.length units in
 416   debug_print (lazy ("No = " ^ (string_of_int no)));
 417   let active,passive,newmeta =
 418     Saturation.pump_actives context bag maxm active passive (no+1) infinity
 419   in
 420     (active,passive,bag),cache,newmeta
 421
 422 let find_context_equalities
 423   maxmeta bag context proof (universe:Universe.universe) cache
 424 =
 425   let module C = Cic in
 426   let module S = CicSubstitution in
 427   let module T = CicTypeChecker in
 428   let _,metasenv,_subst,_,_, _ = proof in
 429   let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
 430   (* if use_auto is true, we try to close the hypothesis of equational
 431     statements using auto; a naif, and probably wrong approach *)
 432   let rec aux cache index newmeta = function
 433     | [] -> [], newmeta,cache
 434     | (Some (_, C.Decl (term)))::tl ->
 435         debug_print
 436           (lazy
 437              (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
 438         let do_find context term =
 439           match term with
 440           | C.Prod (name, s, t) when is_an_equality t ->
 441               (try
 442
 443                 let term = S.lift index term in
 444                 let saturated,cache,newmeta =
 445                   fill_hypothesis context metasenv newmeta term
 446                     empty_tables universe cache default_auto false
 447                 in
 448                 let eqs,newmeta =
 449                   List.fold_left
 450                    (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
 451                      let newmeta, equality =
 452                        build_equality
 453                          bag head args (Cic.Rel index) newmetas (max newmeta newmeta')
 454                      in
 455                      equality::acc, newmeta + 1)
 456                    ([],newmeta) saturated
 457                 in
 458                  eqs, newmeta, cache
 459               with FillingFailure (cache,newmeta) ->
 460                 [],newmeta,cache)
 461           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
 462               when LibraryObjects.is_eq_URI uri ->
 463               let term = S.lift index term in
 464               let newmeta, e =
 465                 build_equality bag term [] (Cic.Rel index) [] newmeta
 466               in
 467               [e], (newmeta+1),cache
 468           | _ -> [], newmeta, cache
 469         in
 470         let eqs, newmeta, cache = do_find context term in
 471         let rest, newmeta,cache = aux cache (index+1) newmeta tl in
 472         List.map (fun x -> index,x) eqs @ rest, newmeta, cache
 473     | _::tl ->
 474         aux cache (index+1) newmeta tl
 475   in
 476   let il, maxm, cache =
 477     aux cache 1 newmeta context
 478   in
 479   let indexes, equalities = List.split il in
 480   indexes, equalities, maxm, cache
 481 ;;
 482
 483 (***************** applyS *******************)
 484
 485 let new_metasenv_and_unify_and_t
 486  dbd flags universe proof goal ?tables newmeta' metasenv'
 487  context term' ty termty goal_arity
 488 =
 489  let (consthead,newmetasenv,arguments,_) =
 490    TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
 491  let term'' =
 492    match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
 493  in
 494  let proof',oldmetasenv =
 495   let (puri,metasenv,_subst,pbo,pty, attrs) = proof in
 496    (puri,newmetasenv,_subst,pbo,pty, attrs),metasenv
 497  in
 498  let goal_for_paramod =
 499   match LibraryObjects.eq_URI () with
 500   | Some uri ->
 501       Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
 502   | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
 503  in
 504  let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
 505  let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
 506  let proof'' =
 507    let uri,_,_subst,p,ty, attrs = proof' in
 508    uri,metasenv_for_paramod,_subst,p,ty, attrs
 509  in
 510  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
 511  let proof''',goals =
 512   ProofEngineTypes.apply_tactic
 513     (EqualityTactics.rewrite_tac ~direction:`RightToLeft
 514       ~pattern:(ProofEngineTypes.conclusion_pattern None)
 515         (Cic.Meta(newmeta,irl)) [])
 516    (proof'',goal)
 517  in
 518  let goal = match goals with [g] -> g | _ -> assert false in
 519  let  proof'''', _  =
 520    ProofEngineTypes.apply_tactic
 521      (PrimitiveTactics.apply_tac term'')
 522      (proof''',goal)
 523  in
 524  match
 525    let (active, passive,bag), cache, maxmeta =
 526      init_cache_and_tables ~dbd flags.use_library true true false universe
 527      (proof'''',newmeta)
 528    in
 529      Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
 530        max_int max_int flags.timeout
 531  with
 532  | None, _,_,_ ->
 533      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
 534  | Some (_,proof''''',_), active,passive,_  ->
 535      proof''''',
 536      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
 537        ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m),  active, passive
 538 ;;
 539
 540 let rec count_prods context ty =
 541  match CicReduction.whd context ty with
 542     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
 543   | _ -> 0
 544
 545 let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
 546  let module T = CicTypeChecker in
 547  let module R = CicReduction in
 548  let module C = Cic in
 549   let (_,metasenv,_subst,_,_, _) = proof in
 550   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 551   let newmeta = CicMkImplicit.new_meta metasenv subst in
 552    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
 553     match term with
 554        C.Var (uri,exp_named_subst) ->
 555         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 556          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 557           exp_named_subst
 558         in
 559          exp_named_subst_diff,newmeta',newmetasenvfragment,
 560           C.Var (uri,exp_named_subst')
 561      | C.Const (uri,exp_named_subst) ->
 562         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 563          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 564           exp_named_subst
 565         in
 566          exp_named_subst_diff,newmeta',newmetasenvfragment,
 567           C.Const (uri,exp_named_subst')
 568      | C.MutInd (uri,tyno,exp_named_subst) ->
 569         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 570          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 571           exp_named_subst
 572         in
 573          exp_named_subst_diff,newmeta',newmetasenvfragment,
 574           C.MutInd (uri,tyno,exp_named_subst')
 575      | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 576         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 577          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 578           exp_named_subst
 579         in
 580          exp_named_subst_diff,newmeta',newmetasenvfragment,
 581           C.MutConstruct (uri,tyno,consno,exp_named_subst')
 582      | _ -> [],newmeta,[],term
 583    in
 584    let metasenv' = metasenv@newmetasenvfragment in
 585    let termty,_ =
 586      CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
 587    in
 588    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
 589    let goal_arity = count_prods context ty in
 590    let proof, gl, active, passive =
 591     new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
 592      newmeta' metasenv' context term' ty termty goal_arity
 593    in
 594     proof, gl, active, passive
 595 ;;
 596
 597 (****************** AUTO ********************)
 598
 599 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
 600 let ugraph = CicUniv.empty_ugraph;;
 601 let typeof = CicTypeChecker.type_of_aux';;
 602 let ppterm ctx t =
 603   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
 604   CicPp.pp t names
 605 ;;
 606 let is_in_prop context subst metasenv ty =
 607   let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
 608   fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
 609 ;;
 610
 611 let assert_proof_is_valid proof metasenv context goalty =
 612   if debug then
 613     begin
 614       let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
 615       let b,_ = CicReduction.are_convertible context ty goalty u in
 616         if not b then
 617           begin
 618             let names =
 619               List.map (function None -> None | Some (x,_) -> Some x) context
 620             in
 621               debug_print (lazy ("PROOF:" ^ CicPp.pp proof names));
 622               debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names));
 623               debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names));
 624               debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv));
 625           end;
 626         assert b
 627     end
 628   else ()
 629 ;;
 630
 631 let assert_subst_are_disjoint subst subst' =
 632   if debug then
 633     assert(List.for_all
 634              (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
 635              subst)
 636   else ()
 637 ;;
 638
 639 let split_goals_in_prop metasenv subst gl =
 640   List.partition
 641     (fun g ->
 642       let _,context,ty = CicUtil.lookup_meta g metasenv in
 643       try
 644         let sort,u = typeof ~subst metasenv context ty ugraph in
 645         let b,_ =
 646           CicReduction.are_convertible
 647             ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
 648         b
 649       with
 650       | CicTypeChecker.AssertFailure s
 651       | CicTypeChecker.TypeCheckerFailure s ->
 652           debug_print
 653             (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty)));
 654           debug_print s;
 655           false)
 656     (* FIXME... they should type! *)
 657     gl
 658 ;;
 659
 660 let split_goals_with_metas metasenv subst gl =
 661   List.partition
 662     (fun g ->
 663       let _,context,ty = CicUtil.lookup_meta g metasenv in
 664       let ty = CicMetaSubst.apply_subst subst ty in
 665       CicUtil.is_meta_closed ty)
 666     gl
 667 ;;
 668
 669 let order_new_goals metasenv subst open_goals ppterm =
 670   let prop,rest = split_goals_in_prop metasenv subst open_goals in
 671   let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
 672   let open_goals =
 673     (List.map (fun x -> x,P) (closed_prop @ open_prop))
 674     @
 675     (List.map (fun x -> x,T) rest)
 676   in
 677   let tys =
 678     List.map
 679       (fun (i,sort) ->
 680         let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
 681   in
 682   debug_print (lazy ("   OPEN: "^
 683     String.concat "\n"
 684       (List.map
 685          (function
 686             | (i,t,P) -> string_of_int i   ^ ":"^ppterm t^ "Prop"
 687             | (i,t,T) -> string_of_int i  ^ ":"^ppterm t^ "Type")
 688          tys)));
 689   open_goals
 690 ;;
 691
 692 let is_an_equational_goal = function
 693   | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
 694   | _ -> false
 695 ;;
 696
 697 (*
 698 let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
 699 *)
 700
 701 let calculate_timeout flags =
 702     if flags.timeout = 0. then
 703       (debug_print (lazy "AUTO WITH NO TIMEOUT");
 704        {flags with timeout = infinity})
 705     else
 706       flags
 707 ;;
 708 let is_equational_case goalty flags =
 709   let ensure_equational t =
 710     if is_an_equational_goal t then true
 711     else false
 712     (*
 713       let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
 714       raise (ProofEngineTypes.Fail (lazy msg))
 715     *)
 716   in
 717   (flags.use_paramod && is_an_equational_goal goalty) ||
 718   (flags.use_only_paramod && ensure_equational goalty)
 719 ;;
 720 (*
 721 let cache_add_success sort cache k v =
 722   if sort = P then cache_add_success cache k v else cache_remove_underinspection
 723   cache k
 724 ;;
 725 *)
 726
 727 type menv = Cic.metasenv
 728 type subst = Cic.substitution
 729 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
 730 let candidate_no = ref 0;;
 731 type candidate = int * Cic.term
 732 type cache = AutoCache.cache
 733 type tables =
 734   Saturation.active_table * Saturation.passive_table * Equality.equality_bag
 735
 736 type fail =
 737   (* the goal (mainly for depth) and key of the goal *)
 738   goal * AutoCache.cache_key
 739 type op =
 740   (* goal has to be proved *)
 741   | D of goal
 742   (* goal has to be cached as a success obtained using candidate as the first
 743    * step *)
 744   | S of goal * AutoCache.cache_key * candidate * int
 745 type elem =
 746   (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
 747   menv * subst * int * op list * op list * fail list
 748 type status =
 749   (* list of computations that may lead to the solution: all op list will
 750    * end with the same (S(g,_)) *)
 751   elem list
 752 type auto_result =
 753   (* menv, subst, alternatives, tables, cache, maxmeta *)
 754   | Proved of menv * subst * elem list * tables * cache * int
 755   | Gaveup of tables * cache * int
 756
 757
 758 (* the status exported to the external observer *)
 759 type auto_status =
 760   (* context, (goal,candidate) list, and_list, history *)
 761   Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list *
 762   (int * Cic.term * int) list * Cic.term list
 763
 764 let d_prefix l =
 765   let rec aux acc = function
 766     | (D g)::tl -> aux (acc@[g]) tl
 767     | _ -> acc
 768   in
 769     aux [] l
 770 ;;
 771 let prop_only l =
 772   List.filter (function (_,_,P) -> true | _ -> false) l
 773 ;;
 774
 775 let d_goals l =
 776   let rec aux acc = function
 777     | (D g)::tl -> aux (acc@[g]) tl
 778     | (S _)::tl -> aux acc tl
 779     | [] -> acc
 780   in
 781     aux [] l
 782 ;;
 783 let calculate_goal_ty (goalno,_,_) s m =
 784   try
 785     let _,cc,goalty = CicUtil.lookup_meta goalno m in
 786     (* XXX applicare la subst al contesto? *)
 787     Some (cc, CicMetaSubst.apply_subst s goalty)
 788   with CicUtil.Meta_not_found i when i = goalno -> None
 789 ;;
 790 let calculate_closed_goal_ty (goalno,_,_) s =
 791   try
 792     let cc,_,goalty = List.assoc goalno s in
 793     (* XXX applicare la subst al contesto? *)
 794     Some (cc, CicMetaSubst.apply_subst s goalty)
 795   with Not_found -> None
 796 ;;
 797 let pp_status ctx status =
 798   if debug then
 799   let names = Utils.names_of_context ctx in
 800   let pp x =
 801     let x =
 802       ProofEngineReduction.replace
 803         ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
 804           ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
 805     in
 806     CicPp.pp x names
 807   in
 808   let string_of_do m s (gi,_,_ as g) d =
 809     match calculate_goal_ty g s m with
 810     | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
 811     | None -> Printf.sprintf "D(%d, _, %d)" gi d
 812   in
 813   let string_of_s m su k (ci,ct) gi =
 814     Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp ct) ci
 815   in
 816   let string_of_ol m su l =
 817     String.concat " | "
 818       (List.map
 819         (function
 820           | D (g,d,s) -> string_of_do m su (g,d,s) d
 821           | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
 822         l)
 823   in
 824   let string_of_fl m s fl =
 825     String.concat " | "
 826       (List.map (fun ((i,_,_),ty) ->
 827          Printf.sprintf "(%d, %s)" i (pp ty)) fl)
 828   in
 829   let rec aux = function
 830     | [] -> ()
 831     | (m,s,_,_,ol,fl)::tl ->
 832         Printf.eprintf "< [%s] ;;; [%s]>\n"
 833           (string_of_ol m s ol) (string_of_fl m s fl);
 834         aux tl
 835   in
 836     Printf.eprintf "-------------------------- status -------------------\n";
 837     aux status;
 838     Printf.eprintf "-----------------------------------------------------\n";
 839 ;;
 840
 841 let auto_status = ref [] ;;
 842 let auto_context = ref [];;
 843 let in_pause = ref false;;
 844 let pause b = in_pause := b;;
 845 let cond = Condition.create ();;
 846 let mutex = Mutex.create ();;
 847 let hint = ref None;;
 848 let prune_hint = ref [];;
 849
 850 let step _ = Condition.signal cond;;
 851 let give_hint n = hint := Some n;;
 852 let give_prune_hint hint =
 853   prune_hint := hint :: !prune_hint
 854 ;;
 855
 856 let check_pause _ =
 857   if !in_pause then
 858     begin
 859       Mutex.lock mutex;
 860       Condition.wait cond mutex;
 861       Mutex.unlock mutex
 862     end
 863 ;;
 864
 865 let get_auto_status _ =
 866   let status = !auto_status in
 867   let and_list,elems,last =
 868     match status with
 869     | [] -> [],[],[]
 870     | (m,s,_,don,gl,fail)::tl ->
 871         let and_list =
 872           HExtlib.filter_map
 873             (fun (id,d,_ as g) ->
 874               match calculate_goal_ty g s m with
 875               | Some (_,x) -> Some (id,x,d) | None -> None)
 876             (d_goals gl)
 877         in
 878         let rows =
 879           (* these are the S goalsin the or list *)
 880           let orlist =
 881             List.map
 882               (fun (m,s,_,don,gl,fail) ->
 883                 HExtlib.filter_map
 884                   (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
 885                   (List.rev don @ gl))
 886               status
 887           in
 888           (* this function eats id from a list l::[id,x] returning x, l *)
 889           let eat_tail_if_eq id l =
 890             let rec aux (s, l) = function
 891               | [] -> s, l
 892               | ((id1,_,_),k1,c)::tl when id = id1 ->
 893                   (match s with
 894                   | None -> aux (Some c,l) tl
 895                   | Some _ -> assert false)
 896               | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
 897             in
 898             let c, l = aux (None, []) l in
 899             c, List.rev l
 900           in
 901           let eat_in_parallel id l =
 902             let rec aux (b,eaten, new_l as acc) l =
 903               match l with
 904               | [] -> acc
 905               | l::tl ->
 906                   match eat_tail_if_eq id l with
 907                   | None, l -> aux (b@[false], eaten, new_l@[l]) tl
 908                   | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
 909             in
 910             aux ([],[],[]) l
 911           in
 912           let rec eat_all rows l =
 913             match l with
 914             | [] -> rows
 915             | elem::or_list ->
 916                 match List.rev elem with
 917                 | ((to_eat,depth,_),k,_)::next_lunch ->
 918                     let b, eaten, l = eat_in_parallel to_eat l in
 919                     let eaten = HExtlib.list_uniq eaten in
 920                     let eaten = List.rev eaten in
 921                     let b = true (* List.hd (List.rev b) *) in
 922                     let rows = rows @ [to_eat,k,b,depth,eaten] in
 923                     eat_all rows l
 924                 | [] -> eat_all rows or_list
 925           in
 926           eat_all [] (List.rev orlist)
 927         in
 928         let history =
 929           HExtlib.filter_map
 930             (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
 931             gl
 932         in
 933 (*         let rows = List.filter (fun (_,l) -> l <> []) rows in *)
 934         and_list, rows, history
 935   in
 936   !auto_context, elems, and_list, last
 937 ;;
 938
 939 (* Works if there is no dependency over proofs *)
 940 let is_a_green_cut goalty =
 941   CicUtil.is_meta_closed goalty
 942 ;;
 943 let rec first_s = function
 944   | (D _)::tl -> first_s tl
 945   | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
 946   | [] -> None
 947 ;;
 948 let list_union l1 l2 =
 949   (* TODO ottimizzare compare *)
 950   HExtlib.list_uniq (List.sort compare (l1 @ l1))
 951 ;;
 952 let eat_head todo id fl orlist =
 953   let rec aux acc = function
 954   | [] -> [], acc
 955   | (m, s, _, _, todo1, fl1)::tl as orlist ->
 956       let rec aux1 todo1 =
 957         match first_s todo1 with
 958         | None -> orlist, acc
 959         | Some (((gno,_,_),_,_,_), todo11) ->
 960             (* TODO confronto tra todo da ottimizzare *)
 961             if gno = id && todo11 = todo then
 962               aux (list_union fl1 acc) tl
 963             else
 964               aux1 todo11
 965       in
 966        aux1 todo1
 967   in
 968     aux fl orlist
 969 ;;
 970 let close_proof p ty menv context =
 971   let metas =
 972     List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
 973   in
 974   let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
 975   naif_closure p menv context
 976 ;;
 977 (* XXX capire bene quando aggiungere alla cache *)
 978 let add_to_cache_and_del_from_orlist_if_green_cut
 979   g s m cache key todo orlist fl ctx size minsize
 980 =
 981   let cache = cache_remove_underinspection cache key in
 982   (* prima per fare la irl usavamo il contesto vero e proprio e non quello
 983    * canonico! XXX *)
 984   match calculate_closed_goal_ty g s with
 985   | None -> assert false
 986   | Some (canonical_ctx , gty) ->
 987       let goalno,depth,sort = g in
 988       let irl = mk_irl canonical_ctx in
 989       let goal = Cic.Meta(goalno, irl) in
 990       let proof = CicMetaSubst.apply_subst s goal in
 991       let green_proof, closed_proof =
 992         let b = is_a_green_cut proof in
 993         if not b then
 994           b, (* close_proof proof gty m ctx *) proof
 995         else
 996           b, proof
 997       in
 998       debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
 999       if is_a_green_cut key then
1000         (* if the initia goal was closed, we cut alternatives *)
1001         let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
1002         let orlist, fl = eat_head todo goalno fl orlist in
1003         let cache =
1004           if size < minsize then
1005             (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
1006           else
1007           (* if the proof is closed we cache it *)
1008           if green_proof then cache_add_success cache key proof
1009           else (* cache_add_success cache key closed_proof *)
1010             (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
1011         in
1012         cache, orlist, fl, true
1013       else
1014         let cache =
1015           debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
1016           if size < minsize then
1017             (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
1018           (* if the substituted goal and the proof are closed we cache it *)
1019           if is_a_green_cut gty then
1020             if green_proof then cache_add_success cache gty proof
1021             else (* cache_add_success cache gty closed_proof *)
1022               (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
1023           else (*
1024             try
1025               let ty, _ =
1026                 CicTypeChecker.type_of_aux' ~subst:s
1027                   m ctx closed_proof CicUniv.oblivion_ugraph
1028               in
1029               if is_a_green_cut ty then
1030                 cache_add_success cache ty closed_proof
1031               else cache
1032             with
1033             | CicTypeChecker.TypeCheckerFailure _ ->*)
1034           (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
1035         in
1036         cache, orlist, fl, false
1037 ;;
1038 let close_failures (fl : fail list) (cache : cache) =
1039   List.fold_left
1040     (fun cache ((gno,depth,_),gty) ->
1041       debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
1042       cache_add_failure cache gty depth)
1043     cache fl
1044 ;;
1045 let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
1046   let entry = goalno, (canonical_ctx, t,ty) in
1047   assert_subst_are_disjoint subst [entry];
1048   let subst = entry :: subst in
1049   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1050   subst, metasenv
1051 ;;
1052 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
1053   None,metasenv,subst ,Cic.Meta(goalno,mk_irl context),goalty, []
1054 ;;
1055 let equational_case
1056   tables maxm cache depth fake_proof goalno goalty subst context
1057     flags
1058 =
1059   let active,passive,bag = tables in
1060   let ppterm = ppterm context in
1061   let status = (fake_proof,goalno) in
1062     if flags.use_only_paramod then
1063       begin
1064         debug_print (lazy ("PARAMODULATION SU: " ^
1065                          string_of_int goalno ^ " " ^ ppterm goalty ));
1066         let goal_steps, saturation_steps, timeout =
1067           max_int,max_int,flags.timeout
1068         in
1069         match
1070           Saturation.given_clause bag maxm status active passive
1071             goal_steps saturation_steps timeout
1072         with
1073           | None, active, passive, maxmeta ->
1074               [], (active,passive,bag), cache, maxmeta, flags
1075           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
1076             passive,maxmeta ->
1077               assert_subst_are_disjoint subst subst';
1078               let subst = subst@subst' in
1079               let open_goals =
1080                 order_new_goals metasenv subst open_goals ppterm
1081               in
1082               let open_goals =
1083                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1084               in
1085               incr candidate_no;
1086                       [(!candidate_no,proof),metasenv,subst,open_goals],
1087                 (active,passive,bag),
1088                 cache, maxmeta, flags
1089       end
1090     else
1091       begin
1092         debug_print
1093           (lazy
1094            ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
1095         let res, maxmeta =
1096           Saturation.all_subsumed bag maxm status active passive
1097         in
1098         assert (maxmeta >= maxm);
1099         let res' =
1100           List.map
1101             (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
1102                assert_subst_are_disjoint subst subst';
1103                let subst = subst@subst' in
1104                let open_goals =
1105                  order_new_goals metasenv subst open_goals ppterm
1106                in
1107                let open_goals =
1108                  List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1109                in
1110                incr candidate_no;
1111                  (!candidate_no,proof),metasenv,subst,open_goals)
1112             res
1113           in
1114           res', (active,passive,bag), cache, maxmeta, flags
1115       end
1116 ;;
1117
1118 let try_candidate
1119   goalty tables maxm subst fake_proof goalno depth context cand
1120 =
1121   let ppterm = ppterm context in
1122   try
1123     let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
1124         (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:maxm ~term:cand)
1125         (fake_proof,goalno)
1126     in
1127     debug_print (lazy ("   OK: " ^ ppterm cand));
1128     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
1129     let open_goals = order_new_goals metasenv subst open_goals ppterm in
1130     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
1131     incr candidate_no;
1132     Some ((!candidate_no,cand),metasenv,subst,open_goals), tables , maxmeta
1133   with
1134     | ProofEngineTypes.Fail s -> None,tables, maxm
1135     | CicUnification.Uncertain s ->  None,tables, maxm
1136 ;;
1137
1138 let sort_new_elems =
1139  List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
1140   List.length (prop_only l1) - List.length (prop_only l2))
1141 ;;
1142
1143 let applicative_case
1144   tables maxm depth subst fake_proof goalno goalty metasenv context universe
1145   cache
1146 =
1147   let candidates = get_candidates universe cache goalty in
1148   let tables, elems, maxm =
1149     List.fold_left
1150       (fun (tables,elems,maxm) cand ->
1151         match
1152           try_candidate goalty
1153             tables maxm subst fake_proof goalno depth context cand
1154         with
1155         | None, tables,maxm  -> tables,elems, maxm
1156         | Some x, tables, maxm -> tables,x::elems, maxm)
1157       (tables,[],maxm) candidates
1158   in
1159   let elems = sort_new_elems elems in
1160   elems, tables, cache, maxm
1161 ;;
1162
1163 let equational_and_applicative_case
1164   universe flags m s g gty tables cache maxm context
1165 =
1166   let goalno, depth, sort = g in
1167   let fake_proof = mk_fake_proof m s g gty context in
1168   if is_equational_case gty flags then
1169     let elems,tables,cache,maxm1, flags =
1170       equational_case tables maxm cache
1171         depth fake_proof goalno gty s context flags
1172     in
1173     let maxm = maxm1 in
1174     let more_elems, tables, cache, maxm1 =
1175       if flags.use_only_paramod then
1176         [],tables, cache, maxm
1177       else
1178         applicative_case
1179           tables maxm depth s fake_proof goalno
1180             gty m context universe cache
1181     in
1182     let maxm = maxm1 in
1183       elems@more_elems, tables, cache, maxm, flags
1184   else
1185     let elems, tables, cache, maxm =
1186       applicative_case tables maxm depth s fake_proof goalno
1187         gty m context universe cache
1188     in
1189       elems, tables, cache, maxm, flags
1190 ;;
1191 let rec condition_for_hint i = function
1192   | [] -> false
1193   | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
1194   | _::tl -> condition_for_hint i tl
1195 ;;
1196 let remove_s_from_fl (id,_,_) (fl : fail list) =
1197   let rec aux = function
1198     | [] -> []
1199     | ((id1,_,_),_)::tl when id = id1 -> tl
1200     | hd::tl ->  hd :: aux tl
1201   in
1202     aux fl
1203 ;;
1204
1205 let prunable_for_size flags s m todo =
1206   let rec aux b = function
1207     | (S _)::tl -> aux b tl
1208     | (D (_,_,T))::tl -> aux b tl
1209     | (D g)::tl ->
1210         (match calculate_goal_ty g s m with
1211           | None -> aux b tl
1212           | Some (canonical_ctx, gty) ->
1213             let gsize, _ =
1214               Utils.weight_of_term
1215                 ~consider_metas:false ~count_metas_occurrences:true gty in
1216             let newb = b || gsize > flags.maxgoalsizefactor in
1217             aux newb tl)
1218     | [] -> b
1219   in
1220     aux false todo
1221
1222 (*
1223 let prunable ty todo =
1224   let rec aux b = function
1225     | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
1226     | (D (_,_,T))::tl -> aux b tl
1227     | D _::_ -> false
1228     | [] -> b
1229   in
1230     aux false todo
1231 ;;
1232 *)
1233
1234 let prunable menv subst ty todo =
1235   let rec aux = function
1236     | (S(_,k,_,_))::tl ->
1237          (match Equality.meta_convertibility_subst k ty menv with
1238           | None -> aux tl
1239           | Some variant ->
1240                no_progress variant tl (* || aux tl*))
1241     | (D (_,_,T))::tl -> aux tl
1242     | _ -> false
1243   and no_progress variant = function
1244     | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
1245     | D ((n,_,P) as g)::tl ->
1246         (match calculate_goal_ty g subst menv with
1247            | None -> no_progress variant tl
1248            | Some (_, gty) ->
1249                (match calculate_goal_ty g variant menv with
1250                   | None -> assert false
1251                   | Some (_, gty') ->
1252                       if gty = gty' then
1253                          no_progress variant tl
1254                       else false))
1255     | _::tl -> no_progress variant tl
1256   in
1257     aux todo
1258
1259 ;;
1260 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
1261   let s =
1262     HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
1263   in
1264   List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
1265 ;;
1266 let filter_prune_hint l =
1267   let prune = !prune_hint in
1268   prune_hint := []; (* possible race... *)
1269   if prune = [] then l
1270   else List.filter (condition_for_prune_hint prune) l
1271 ;;
1272 let auto_main tables maxm context flags universe cache elems =
1273   auto_context := context;
1274   let rec aux tables maxm flags cache (elems : status) =
1275 (*     pp_status context elems; *)
1276 (* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
1277     auto_status := elems;
1278     check_pause ();
1279 *)
1280     let elems = filter_prune_hint elems in
1281     match elems with
1282     | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
1283         (match !hint with
1284         | Some i when condition_for_hint i todo ->
1285             aux tables maxm flags cache orlist
1286         | _ ->
1287           hint := None;
1288           aux tables maxm flags cache elems)
1289     | [] ->
1290         (* complete failure *)
1291         Gaveup (tables, cache, maxm)
1292     | (m, s, _, _, [],_)::orlist ->
1293         (* complete success *)
1294         Proved (m, s, orlist, tables, cache, maxm)
1295     | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist
1296       when not flags.AutoTypes.do_types ->
1297         (* skip since not Prop, don't even check if closed by side-effect *)
1298         aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1299     | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
1300         (* partial success, cache g and go on *)
1301         let cache, orlist, fl, sibling_pruned =
1302           add_to_cache_and_del_from_orlist_if_green_cut
1303             g s m cache key todo orlist fl context size minsize
1304         in
1305         debug_print (lazy (AutoCache.cache_print context cache));
1306         let fl = remove_s_from_fl g fl in
1307         let don = if sibling_pruned then don else op::don in
1308         aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1309     | (m, s, size, don, todo, fl)::orlist
1310       when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1311         debug_print (lazy ("FAIL: WIDTH"));
1312         (* too many goals in and generated by last th *)
1313         let cache = close_failures fl cache in
1314         aux tables maxm flags cache orlist
1315     | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
1316         debug_print
1317           (lazy ("FAIL: SIZE: "^string_of_int size ^
1318             " > " ^ string_of_int flags.maxsize ));
1319         (* we already have a too large proof term *)
1320         let cache = close_failures fl cache in
1321         aux tables maxm flags cache orlist
1322     | _ when Unix.gettimeofday () > flags.timeout ->
1323         (* timeout *)
1324         debug_print (lazy ("FAIL: TIMEOUT"));
1325         Gaveup (tables, cache, maxm)
1326     | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
1327         (* attack g *)
1328         match calculate_goal_ty g s m with
1329         | None ->
1330             (* closed by side effect *)
1331             debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1332             aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist)
1333         | Some (canonical_ctx, gty) ->
1334             let gsize, _ =
1335               Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty
1336             in
1337             if gsize > flags.maxgoalsizefactor then
1338               (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
1339                aux tables maxm flags cache orlist)
1340             else if prunable_for_size flags s m todo then
1341                 (debug_print (lazy ("POTO at depth: "^(string_of_int depth)));
1342                  aux tables maxm flags cache orlist)
1343             else
1344             (* still to be proved *)
1345             (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
1346             match cache_examine cache gty with
1347             | Failed_in d when d >= depth ->
1348                 (* fail depth *)
1349                 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1350                 let cache = close_failures fl cache in
1351                 aux tables maxm flags cache orlist
1352             | UnderInspection ->
1353                 (* fail loop *)
1354                 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1355                 let cache = close_failures fl cache in
1356                 aux tables maxm flags cache orlist
1357             | Succeded t ->
1358                 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1359                 let s, m = put_in_subst s m g canonical_ctx t gty in
1360                 aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
1361             | Notfound
1362             | Failed_in _ when depth > 0 ->
1363                 ( (* more depth or is the first time we see the goal *)
1364                     if prunable m s gty todo then
1365                       (debug_print (lazy(
1366                          "FAIL: LOOP: one father is equal"));
1367                        aux tables maxm flags cache orlist)
1368                     else
1369                     let cache = cache_add_underinspection cache gty depth in
1370                     auto_status := status;
1371                     check_pause ();
1372                     debug_print
1373                       (lazy ("INSPECTING: " ^
1374                         string_of_int gno ^ "("^ string_of_int size ^ "): "^
1375                         CicPp.ppterm gty));
1376                     (* elems are possible computations for proving gty *)
1377                     let elems, tables, cache, maxm, flags =
1378                       equational_and_applicative_case
1379                         universe flags m s g gty tables cache maxm context
1380                     in
1381                     if elems = [] then
1382                       (* this goal has failed *)
1383                       let cache = close_failures ((g,gty)::fl) cache in
1384                       aux tables maxm flags cache orlist
1385                     else
1386                       (* elems = (cand,m,s,gl) *)
1387                       let size_gl l = List.length
1388                         (List.filter (function (_,_,P) -> true | _ -> false) l)
1389                       in
1390                       let elems =
1391                         let inj_gl gl = List.map (fun g -> D g) gl in
1392                         let rec map = function
1393                           | [] -> assert false
1394                           | (cand,m,s,gl)::[] ->
1395                               (* in the last one we add the failure *)
1396                               let todo =
1397                                 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1398                               in
1399                               (* we are the last in OR, we fail on g and
1400                                * also on all failures implied by g *)
1401                               (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
1402                               :: orlist
1403                           | (cand,m,s,gl)::tl ->
1404                               (* we add the S step after gl and before todo *)
1405                               let todo =
1406                                 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1407                               in
1408                               (* since we are not the last in OR, we do not
1409                                * imply failures *)
1410                               (m,s, size + size_gl gl, don, todo, []) :: map tl
1411                         in
1412                           map elems
1413                       in
1414                         aux tables maxm flags cache elems)
1415             | _ ->
1416                 (* no more depth *)
1417                 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1418                 let cache = close_failures fl cache in
1419                 aux tables maxm flags cache orlist)
1420   in
1421     (aux tables maxm flags cache elems : auto_result)
1422 ;;
1423
1424
1425 let
1426   auto_all_solutions maxm tables universe cache context metasenv gl flags
1427 =
1428   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1429   let goals =
1430     List.map
1431       (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1432   in
1433   let elems = [metasenv,[],1,[],goals,[]] in
1434   let rec aux tables maxm solutions cache elems flags =
1435     match auto_main tables maxm context flags universe cache elems with
1436     | Gaveup (tables,cache,maxm) ->
1437         solutions,cache,maxm
1438     | Proved (metasenv,subst,others,tables,cache,maxm) ->
1439         if Unix.gettimeofday () > flags.timeout then
1440           ((subst,metasenv)::solutions), cache, maxm
1441         else
1442           aux tables maxm ((subst,metasenv)::solutions) cache others flags
1443   in
1444   let rc = aux tables maxm [] cache elems flags in
1445     match rc with
1446     | [],cache,maxm -> [],cache,maxm
1447     | solutions,cache,maxm ->
1448         let solutions =
1449           HExtlib.filter_map
1450             (fun (subst,newmetasenv) ->
1451               let opened =
1452                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1453               in
1454               if opened = [] then Some subst else None)
1455             solutions
1456         in
1457          solutions,cache,maxm
1458 ;;
1459
1460 (* }}} ****************** AUTO ***************)
1461
1462 let auto flags metasenv tables universe cache context metasenv gl =
1463   let initial_time = Unix.gettimeofday() in
1464   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1465   let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1466   let elems = [metasenv,[],1,[],goals,[]] in
1467   match auto_main tables 0 context flags universe cache elems with
1468   | Proved (metasenv,subst,_, tables,cache,_) ->
1469       debug_print(lazy
1470         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1471       Some (subst,metasenv), cache
1472   | Gaveup (tables,cache,maxm) ->
1473       debug_print(lazy
1474         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1475       None,cache
1476 ;;
1477
1478 let bool params name default =
1479     try
1480       let s = List.assoc name params in
1481       if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
1482       else if s = "0" || s = "false" || s = "no" || s= "off" then false
1483       else
1484         let msg = "Unrecognized value for parameter "^name^"\n" in
1485         let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
1486         raise (ProofEngineTypes.Fail (lazy msg))
1487     with Not_found -> default
1488 ;;
1489
1490 let string params name default =
1491     try List.assoc name params with
1492     | Not_found -> default
1493 ;;
1494
1495 let int params name default =
1496     try int_of_string (List.assoc name params) with
1497     | Not_found -> default
1498     | Failure _ ->
1499         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
1500 ;;
1501
1502 let flags_of_params params ?(for_applyS=false) () =
1503  let int = int params in
1504  let bool = bool params in
1505  let close_more = bool "close_more" false in
1506  let use_paramod = bool "use_paramod" true in
1507  let use_only_paramod =
1508   if for_applyS then true else bool "paramodulation" false in
1509  let use_library = bool "library"
1510    ((AutoTypes.default_flags()).AutoTypes.use_library) in
1511  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
1512  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
1513  let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
1514  let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
1515  let do_type = bool "type" false in
1516  let timeout = int "timeout" 0 in
1517   { AutoTypes.maxdepth =
1518       if use_only_paramod then 2 else depth;
1519     AutoTypes.maxwidth = width;
1520     AutoTypes.maxsize = size;
1521     AutoTypes.timeout =
1522       if timeout = 0 then
1523        if for_applyS then Unix.gettimeofday () +. 30.0
1524        else
1525          infinity
1526       else
1527        Unix.gettimeofday() +. (float_of_int timeout);
1528     AutoTypes.use_library = use_library;
1529     AutoTypes.use_paramod = use_paramod;
1530     AutoTypes.use_only_paramod = use_only_paramod;
1531     AutoTypes.close_more = close_more;
1532     AutoTypes.dont_cache_failures = false;
1533     AutoTypes.maxgoalsizefactor = gsize;
1534     AutoTypes.do_types = do_type;
1535   }
1536
1537 let applyS_tac ~dbd ~term ~params ~universe =
1538  ProofEngineTypes.mk_tactic
1539   (fun status ->
1540     try
1541       let proof, gl,_,_ =
1542        apply_smart ~dbd ~term ~subst:[] ~universe
1543         (flags_of_params params ~for_applyS:true ()) status
1544       in
1545        proof, gl
1546     with
1547     | CicUnification.UnificationFailure msg
1548     | CicTypeChecker.TypeCheckerFailure msg ->
1549         raise (ProofEngineTypes.Fail msg))
1550
1551 (* SUPERPOSITION *)
1552
1553 (* Syntax:
1554  *   auto superposition target = NAME
1555  *     [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
1556  *
1557  *  - if table is omitted no superposition will be performed
1558  *  - if demod_table is omitted no demodulation will be prformed
1559  *  - subterms_only is passed to Indexing.superposition_right
1560  *
1561  *  lists are coded using _ (example: H_H1_H2)
1562  *)
1563
1564 let eq_and_ty_of_goal = function
1565   | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1566       uri,t
1567   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1568 ;;
1569
1570 let rec find_in_ctx i name = function
1571   | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
1572   | Some (Cic.Name name', _)::tl when name = name' -> i
1573   | _::tl -> find_in_ctx (i+1) name tl
1574 ;;
1575
1576 let rec position_of i x = function
1577   | [] -> assert false
1578   | j::tl when j <> x -> position_of (i+1) x tl
1579   | _ -> i
1580 ;;
1581
1582
1583 let superposition_tac ~target ~table ~subterms_only ~demod_table status =
1584   Saturation.reset_refs();
1585   let proof,goalno = status in
1586   let curi,metasenv,_subst,pbo,pty, attrs = proof in
1587   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
1588   let eq_uri,tty = eq_and_ty_of_goal ty in
1589   let env = (metasenv, context, CicUniv.empty_ugraph) in
1590   let names = Utils.names_of_context context in
1591   let bag = Equality.mk_equality_bag () in
1592   let eq_index, equalities, maxm,cache  =
1593     find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
1594   in
1595   let eq_what =
1596     let what = find_in_ctx 1 target context in
1597     List.nth equalities (position_of 0 what eq_index)
1598   in
1599   let eq_other =
1600     if table <> "" then
1601       let other =
1602         let others = Str.split (Str.regexp "_") table in
1603         List.map (fun other -> find_in_ctx 1 other context) others
1604       in
1605       List.map
1606         (fun other -> List.nth equalities (position_of 0 other eq_index))
1607         other
1608     else
1609       []
1610   in
1611   let index = List.fold_left Indexing.index Indexing.empty eq_other in
1612   let maxm, eql =
1613     if table = "" then maxm,[eq_what] else
1614     Indexing.superposition_right bag
1615       ~subterms_only eq_uri maxm env index eq_what
1616   in
1617   debug_print (lazy ("Superposition right:"));
1618   debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env));
1619   debug_print (lazy ("\n table: "));
1620   List.iter
1621     (fun e ->
1622        debug_print (lazy ("  " ^ Equality.string_of_equality e ~env))) eq_other;
1623   debug_print (lazy ("\n result: "));
1624   List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1625   debug_print (lazy ("\n result (cut&paste): "));
1626   List.iter
1627     (fun e ->
1628       let t = Equality.term_of_equality eq_uri e in
1629       debug_print (lazy (CicPp.pp t names)))
1630   eql;
1631   debug_print (lazy ("\n result proofs: "));
1632   List.iter (fun e ->
1633     debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in
1634     let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
1635     Subst.ppsubst s ^ "\n" ^
1636     CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql;
1637   if demod_table <> "" then
1638     begin
1639       let eql =
1640         if eql = [] then [eq_what] else eql
1641       in
1642       let demod =
1643         let demod = Str.split (Str.regexp "_") demod_table in
1644         List.map (fun other -> find_in_ctx 1 other context) demod
1645       in
1646       let eq_demod =
1647         List.map
1648           (fun demod -> List.nth equalities (position_of 0 demod eq_index))
1649           demod
1650       in
1651       let table = List.fold_left Indexing.index Indexing.empty eq_demod in
1652       let maxm,eql =
1653         List.fold_left
1654           (fun (maxm,acc) e ->
1655             let maxm,eq =
1656               Indexing.demodulation_equality bag eq_uri maxm env table e
1657             in
1658             maxm,eq::acc)
1659           (maxm,[]) eql
1660       in
1661       let eql = List.rev eql in
1662       debug_print (lazy ("\n result [demod]: "));
1663       List.iter
1664         (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1665       debug_print (lazy ("\n result [demod] (cut&paste): "));
1666       List.iter
1667         (fun e ->
1668           let t = Equality.term_of_equality eq_uri e in
1669           debug_print (lazy (CicPp.pp t names)))
1670       eql;
1671     end;
1672   proof,[goalno]
1673 ;;
1674
1675 let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) =
1676   (* argument parsing *)
1677   let string = string params in
1678   let bool = bool params in
1679   (* hacks to debug paramod *)
1680   let superposition = bool "superposition" false in
1681   let target = string "target" "" in
1682   let table = string "table" "" in
1683   let subterms_only = bool "subterms_only" false in
1684   let demod_table = string "demod_table" "" in
1685   match superposition with
1686   | true ->
1687       (* this is the ugly hack to debug paramod *)
1688       superposition_tac
1689         ~target ~table ~subterms_only ~demod_table (proof,goal)
1690   | false ->
1691       (* this is the real auto *)
1692       let _,metasenv,_subst,_,_, _ = proof in
1693       let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1694       let flags = flags_of_params params () in
1695       (* just for testing *)
1696       let use_library = flags.use_library in
1697       let tables,cache,newmeta =
1698         init_cache_and_tables ~dbd use_library flags.use_only_paramod true
1699           false universe (proof, goal) in
1700       let tables,cache,newmeta =
1701         if flags.close_more then
1702           close_more
1703             tables newmeta context (proof, goal)
1704               auto_all_solutions universe cache
1705         else tables,cache,newmeta in
1706       let initial_time = Unix.gettimeofday() in
1707       let (_,oldmetasenv,_subst,_,_, _) = proof in
1708       hint := None;
1709       let elem =
1710         metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[]
1711       in
1712       match auto_main tables newmeta context flags universe cache [elem] with
1713         | Proved (metasenv,subst,_, tables,cache,_) ->
1714             (*prerr_endline
1715               ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));*)
1716             let proof,metasenv =
1717             ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1718               proof goal subst metasenv
1719             in
1720             let opened =
1721               ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1722                 ~newmetasenv:metasenv
1723             in
1724               proof,opened
1725         | Gaveup (tables,cache,maxm) ->
1726             debug_print
1727               (lazy ("TIME:"^
1728                 string_of_float(Unix.gettimeofday()-.initial_time)));
1729             raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1730 ;;
1731
1732 let auto_tac ~dbd ~params ~universe =
1733   ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1734
1735 let eq_of_goal = function
1736   | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1737       uri
1738   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1739 ;;
1740
1741 (* performs steps of rewrite with the universe, obtaining if possible
1742  * a trivial goal *)
1743 let solve_rewrite_tac ~universe ?(steps=1) (proof,goal as status)=
1744   let _,metasenv,_subst,_,_,_ = proof in
1745   let _,context,ty = CicUtil.lookup_meta goal metasenv in
1746   let eq_uri = eq_of_goal ty in
1747   let (active,passive,bag), cache, maxm =
1748      (* we take the whole universe (no signature filtering) *)
1749      init_cache_and_tables false true false true universe (proof,goal)
1750   in
1751   let initgoal = [], metasenv, ty in
1752   let table =
1753     let equalities = (Saturation.list_of_passive passive) in
1754     (* we demodulate using both actives passives *)
1755     List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
1756   in
1757   let env = metasenv,context,CicUniv.empty_ugraph in
1758   match Indexing.solve_demodulating bag env table initgoal steps with
1759   | Some (proof, metasenv, newty) ->
1760       let refl =
1761         match newty with
1762         | Cic.Appl[Cic.MutInd _;eq_ty;left;_] ->
1763             Equality.Exact (Equality.refl_proof eq_uri eq_ty left)
1764         | _ -> assert false
1765       in
1766       let proofterm,_ =
1767         Equality.build_goal_proof
1768           bag eq_uri proof refl newty [] context metasenv
1769       in
1770       ProofEngineTypes.apply_tactic
1771         (PrimitiveTactics.apply_tac ~term:proofterm) status
1772   | None ->
1773       raise
1774         (ProofEngineTypes.Fail (lazy
1775           ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
1776 ;;
1777 let solve_rewrite_tac ~universe ?steps () =
1778   ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ?steps)
1779 ;;
1780
1781 (* DEMODULATE *)
1782 let demodulate_tac ~dbd ~universe (proof,goal)=
1783   let curi,metasenv,_subst,pbo,pty, attrs = proof in
1784   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1785   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1786   let initgoal = [], metasenv, ty in
1787   let eq_uri = eq_of_goal ty in
1788   let (active,passive,bag), cache, maxm =
1789      init_cache_and_tables
1790        ~dbd false true true false universe (proof,goal)
1791   in
1792   let equalities = (Saturation.list_of_passive passive) in
1793   (* we demodulate using both actives passives *)
1794   let table =
1795     List.fold_left
1796       (fun tbl eq -> Indexing.index tbl eq)
1797       (snd active) equalities
1798   in
1799   let changed,(newproof,newmetasenv, newty) =
1800     Indexing.demodulation_goal bag
1801       (metasenv,context,CicUniv.empty_ugraph) table initgoal
1802   in
1803   if changed then
1804     begin
1805       let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1806       let proofterm,_ =
1807         Equality.build_goal_proof bag
1808           eq_uri newproof opengoal ty [] context metasenv
1809       in
1810         let extended_metasenv = (maxm,context,newty)::metasenv in
1811         let extended_status =
1812           (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
1813         let (status,newgoals) =
1814           ProofEngineTypes.apply_tactic
1815             (PrimitiveTactics.apply_tac ~term:proofterm)
1816             extended_status in
1817         (status,maxm::newgoals)
1818     end
1819   else (* if newty = ty then *)
1820     raise (ProofEngineTypes.Fail (lazy "no progress"))
1821   (*else ProofEngineTypes.apply_tactic
1822     (ReductionTactics.simpl_tac
1823       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1824 ;;
1825
1826 let demodulate_tac ~dbd ~universe =
1827   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
1828
1829 let pp_proofterm = Equality.pp_proofterm;;
1830
1831 let revision = "$Revision$";;
1832 let size_and_depth context metasenv t = 100, 100