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