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
 835 let step _ = Condition.signal cond;;
 836 let give_hint n = hint := Some n;;
 837
 838 let check_pause _ =
 839   if !in_pause then
 840     begin
 841       Mutex.lock mutex;
 842       Condition.wait cond mutex;
 843       Mutex.unlock mutex
 844     end
 845 ;;
 846
 847 let get_auto_status _ =
 848   let status = !auto_status in
 849   let and_list,elems,last =
 850     match status with
 851     | [] -> [],[],[]
 852     | (m,s,_,don,gl,fail)::tl ->
 853         let and_list =
 854           HExtlib.filter_map
 855             (fun (id,d,_ as g) ->
 856               match calculate_goal_ty g s m with
 857               | Some (_,x) -> Some (id,x,d) | None -> None)
 858             (d_goals gl)
 859         in
 860         let rows =
 861           (* these are the S goalsin the or list *)
 862           let orlist =
 863             List.map
 864               (fun (m,s,_,don,gl,fail) ->
 865                 HExtlib.filter_map
 866                   (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
 867                   (List.rev don @ gl))
 868               status
 869           in
 870           (* this function eats id from a list l::[id,x] returning x, l *)
 871           let eat_tail_if_eq id l =
 872             let rec aux (s, l) = function
 873               | [] -> s, l
 874               | ((id1,_,_),k1,c)::tl when id = id1 ->
 875                   (match s with
 876                   | None -> aux (Some c,l) tl
 877                   | Some _ -> assert false)
 878               | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
 879             in
 880             let c, l = aux (None, []) l in
 881             c, List.rev l
 882           in
 883           let eat_in_parallel id l =
 884             let rec aux (b,eaten, new_l as acc) l =
 885               match l with
 886               | [] -> acc
 887               | l::tl ->
 888                   match eat_tail_if_eq id l with
 889                   | None, l -> aux (b@[false], eaten, new_l@[l]) tl
 890                   | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
 891             in
 892             aux ([],[],[]) l
 893           in
 894           let rec eat_all rows l =
 895             match l with
 896             | [] -> rows
 897             | elem::or_list ->
 898                 match List.rev elem with
 899                 | ((to_eat,depth,_),k,_)::next_lunch ->
 900                     let b, eaten, l = eat_in_parallel to_eat l in
 901                     let eaten = HExtlib.list_uniq eaten in
 902                     let eaten = List.rev eaten in
 903                     let b = true (* List.hd (List.rev b) *) in
 904                     let rows = rows @ [to_eat,k,b,depth,eaten] in
 905                     eat_all rows l
 906                 | [] -> eat_all rows or_list
 907           in
 908           eat_all [] (List.rev orlist)
 909         in
 910         let history =
 911           HExtlib.filter_map
 912             (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
 913             gl
 914         in
 915 (*         let rows = List.filter (fun (_,l) -> l <> []) rows in *)
 916         and_list, rows, history
 917   in
 918   !auto_context, elems, and_list, last
 919 ;;
 920
 921 (* Works if there is no dependency over proofs *)
 922 let is_a_green_cut goalty =
 923   CicUtil.is_meta_closed goalty
 924 ;;
 925 let rec first_s = function
 926   | (D _)::tl -> first_s tl
 927   | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
 928   | [] -> None
 929 ;;
 930 let list_union l1 l2 =
 931   (* TODO ottimizzare compare *)
 932   HExtlib.list_uniq (List.sort compare (l1 @ l1))
 933 ;;
 934 let eat_head todo id fl orlist =
 935   let rec aux acc = function
 936   | [] -> [], acc
 937   | (m, s, _, _, todo1, fl1)::tl as orlist ->
 938       let rec aux1 todo1 =
 939         match first_s todo1 with
 940         | None -> orlist, acc
 941         | Some (((gno,_,_),_,_,_), todo11) ->
 942             (* TODO confronto tra todo da ottimizzare *)
 943             if gno = id && todo11 = todo then
 944               aux (list_union fl1 acc) tl
 945             else
 946               aux1 todo11
 947       in
 948        aux1 todo1
 949   in
 950     aux fl orlist
 951 ;;
 952 let close_proof p ty menv context =
 953   let metas =
 954     List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
 955   in
 956   let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
 957   naif_closure p menv context
 958 ;;
 959 (* XXX capire bene quando aggiungere alla cache *)
 960 let add_to_cache_and_del_from_orlist_if_green_cut
 961   g s m cache key todo orlist fl ctx size minsize
 962 =
 963   let cache = cache_remove_underinspection cache key in
 964   (* prima per fare la irl usavamo il contesto vero e proprio e non quello
 965    * canonico! XXX *)
 966   match calculate_closed_goal_ty g s with
 967   | None -> assert false
 968   | Some (canonical_ctx , gty) ->
 969       let goalno,depth,sort = g in
 970       assert (sort = P);
 971       let irl = mk_irl canonical_ctx in
 972       let goal = Cic.Meta(goalno, irl) in
 973       let proof = CicMetaSubst.apply_subst s goal in
 974       let green_proof, closed_proof =
 975         let b = is_a_green_cut proof in
 976         if not b then
 977           b, (* close_proof proof gty m ctx *) proof
 978         else
 979           b, proof
 980       in
 981       debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
 982       if is_a_green_cut key then
 983         (* if the initia goal was closed, we cut alternatives *)
 984         let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
 985         let orlist, fl = eat_head todo goalno fl orlist in
 986         let cache =
 987           if size < minsize then
 988             (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
 989           else
 990           (* if the proof is closed we cache it *)
 991           if green_proof then cache_add_success cache key proof
 992           else (* cache_add_success cache key closed_proof *)
 993             (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
 994         in
 995         cache, orlist, fl, true
 996       else
 997         let cache =
 998           debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
 999           if size < minsize then
1000             (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
1001           (* if the substituted goal and the proof are closed we cache it *)
1002           if is_a_green_cut gty then
1003             if green_proof then cache_add_success cache gty proof
1004             else (* cache_add_success cache gty closed_proof *)
1005               (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
1006           else (*
1007             try
1008               let ty, _ =
1009                 CicTypeChecker.type_of_aux' ~subst:s
1010                   m ctx closed_proof CicUniv.oblivion_ugraph
1011               in
1012               if is_a_green_cut ty then
1013                 cache_add_success cache ty closed_proof
1014               else cache
1015             with
1016             | CicTypeChecker.TypeCheckerFailure _ ->*)
1017           (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
1018         in
1019         cache, orlist, fl, false
1020 ;;
1021 let close_failures (fl : fail list) (cache : cache) =
1022   List.fold_left
1023     (fun cache ((gno,depth,_),gty) ->
1024       debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
1025       cache_add_failure cache gty depth)
1026     cache fl
1027 ;;
1028 let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
1029   let entry = goalno, (canonical_ctx, t,ty) in
1030   assert_subst_are_disjoint subst [entry];
1031   let subst = entry :: subst in
1032   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1033   subst, metasenv
1034 ;;
1035 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
1036   None,metasenv,subst ,Cic.Meta(goalno,mk_irl context),goalty, []
1037 ;;
1038 let equational_case
1039   tables maxm cache depth fake_proof goalno goalty subst context
1040     flags
1041 =
1042   let active,passive,bag = tables in
1043   let ppterm = ppterm context in
1044   let status = (fake_proof,goalno) in
1045     if flags.use_only_paramod then
1046       begin
1047         debug_print (lazy ("PARAMODULATION SU: " ^
1048                          string_of_int goalno ^ " " ^ ppterm goalty ));
1049         let goal_steps, saturation_steps, timeout =
1050           max_int,max_int,flags.timeout
1051         in
1052         match
1053           Saturation.given_clause bag maxm status active passive
1054             goal_steps saturation_steps timeout
1055         with
1056           | None, active, passive, maxmeta ->
1057               [], (active,passive,bag), cache, maxmeta, flags
1058           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
1059             passive,maxmeta ->
1060               assert_subst_are_disjoint subst subst';
1061               let subst = subst@subst' in
1062               let open_goals =
1063                 order_new_goals metasenv subst open_goals ppterm
1064               in
1065               let open_goals =
1066                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1067               in
1068               incr candidate_no;
1069                       [(!candidate_no,proof),metasenv,subst,open_goals],
1070                 (active,passive,bag),
1071                 cache, maxmeta, flags
1072       end
1073     else
1074       begin
1075         debug_print
1076           (lazy
1077            ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
1078         let res, maxmeta =
1079           Saturation.all_subsumed bag maxm status active passive
1080         in
1081         assert (maxmeta >= maxm);
1082         let res' =
1083           List.map
1084             (fun subst',(_,metasenv,_subst,proof,_, _),open_goals ->
1085                assert_subst_are_disjoint subst subst';
1086                let subst = subst@subst' in
1087                let open_goals =
1088                  order_new_goals metasenv subst open_goals ppterm
1089                in
1090                let open_goals =
1091                  List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1092                in
1093                incr candidate_no;
1094                  (!candidate_no,proof),metasenv,subst,open_goals)
1095             res
1096           in
1097           res', (active,passive,bag), cache, maxmeta, flags
1098       end
1099 ;;
1100
1101 let try_candidate
1102   goalty tables maxm subst fake_proof goalno depth context cand
1103 =
1104   let ppterm = ppterm context in
1105   try
1106     let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
1107         (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:maxm ~term:cand)
1108         (fake_proof,goalno)
1109     in
1110     debug_print (lazy ("   OK: " ^ ppterm cand));
1111     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
1112     let open_goals = order_new_goals metasenv subst open_goals ppterm in
1113     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
1114     incr candidate_no;
1115     Some ((!candidate_no,cand),metasenv,subst,open_goals), tables , maxmeta
1116   with
1117     | ProofEngineTypes.Fail s -> None,tables, maxm
1118     | CicUnification.Uncertain s ->  None,tables, maxm
1119 ;;
1120
1121 let sort_new_elems =
1122  List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2)
1123 (*  List.sort (fun (_,_,_,l2) (_,_,_,l1) -> List.length l1 - List.length l2)  *)
1124 ;;
1125
1126 let applicative_case
1127   tables maxm depth subst fake_proof goalno goalty metasenv context universe
1128   cache
1129 =
1130   let candidates = get_candidates universe cache goalty in
1131   let tables, elems, maxm =
1132     List.fold_left
1133       (fun (tables,elems,maxm) cand ->
1134         match
1135           try_candidate goalty
1136             tables maxm subst fake_proof goalno depth context cand
1137         with
1138         | None, tables,maxm  -> tables,elems, maxm
1139         | Some x, tables, maxm -> tables,x::elems, maxm)
1140       (tables,[],maxm) candidates
1141   in
1142   let elems = sort_new_elems elems in
1143   elems, tables, cache, maxm
1144 ;;
1145
1146 let equational_and_applicative_case
1147   universe flags m s g gty tables cache maxm context
1148 =
1149   let goalno, depth, sort = g in
1150   let fake_proof = mk_fake_proof m s g gty context in
1151   if is_equational_case gty flags then
1152     let elems,tables,cache,maxm1, flags =
1153       equational_case tables maxm cache
1154         depth fake_proof goalno gty s context flags
1155     in
1156     let maxm = maxm1 in
1157     let more_elems, tables, cache, maxm1 =
1158       if flags.use_only_paramod then
1159         [],tables, cache, maxm
1160       else
1161         applicative_case
1162           tables maxm depth s fake_proof goalno
1163             gty m context universe cache
1164     in
1165     let maxm = maxm1 in
1166       elems@more_elems, tables, cache, maxm, flags
1167   else
1168     let elems, tables, cache, maxm =
1169       applicative_case tables maxm depth s fake_proof goalno
1170         gty m context universe cache
1171     in
1172       elems, tables, cache, maxm, flags
1173 ;;
1174 let rec condition_for_hint i = function
1175   | [] -> false
1176   | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
1177   | _::tl -> condition_for_hint i tl
1178 ;;
1179 let remove_s_from_fl (id,_,_) (fl : fail list) =
1180   let rec aux = function
1181     | [] -> []
1182     | ((id1,_,_),_)::tl when id = id1 -> tl
1183     | hd::tl ->  hd :: aux tl
1184   in
1185     aux fl
1186 ;;
1187
1188 let prunable_for_size flags s m todo =
1189   let rec aux b = function
1190     | (S _)::tl -> aux b tl
1191     | (D (_,_,T))::tl -> aux b tl
1192     | (D g)::tl ->
1193         (match calculate_goal_ty g s m with
1194           | None -> aux b tl
1195           | Some (canonical_ctx, gty) ->
1196             let gsize, _ =
1197               Utils.weight_of_term
1198                 ~consider_metas:false ~count_metas_occurrences:true gty in
1199             let newb = b || gsize > flags.maxgoalsizefactor in
1200             aux newb tl)
1201     | [] -> b
1202   in
1203     aux false todo
1204
1205 (*
1206 let prunable ty todo =
1207   let rec aux b = function
1208     | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
1209     | (D (_,_,T))::tl -> aux b tl
1210     | D _::_ -> false
1211     | [] -> b
1212   in
1213     aux false todo
1214 ;;
1215 *)
1216
1217 let prunable menv subst ty todo =
1218   let rec aux = function
1219     | (S(_,k,_,_))::tl ->
1220          (match Equality.meta_convertibility_subst k ty menv with
1221           | None -> aux tl
1222           | Some variant ->
1223                no_progress variant tl (* || aux tl*))
1224     | (D (_,_,T))::tl -> aux tl
1225     | _ -> false
1226   and no_progress variant = function
1227     | [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true
1228     | D ((n,_,P) as g)::tl ->
1229         (match calculate_goal_ty g subst menv with
1230            | None -> no_progress variant tl
1231            | Some (_, gty) ->
1232                (match calculate_goal_ty g variant menv with
1233                   | None -> assert false
1234                   | Some (_, gty') ->
1235                       if gty = gty' then
1236                          no_progress variant tl
1237                       else false))
1238     | _::tl -> no_progress variant tl
1239   in
1240     aux todo
1241
1242 ;;
1243
1244 let auto_main tables maxm context flags universe cache elems =
1245   auto_context := context;
1246   let rec aux tables maxm flags cache (elems : status) =
1247 (*     pp_status context elems; *)
1248 (* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
1249     auto_status := elems;
1250     check_pause ();
1251 *)
1252     match elems with
1253     | (m, s, size, don, todo, fl)::orlist as status when !hint <> None ->
1254         (match !hint with
1255         | Some i when condition_for_hint i todo ->
1256             aux tables maxm flags cache orlist
1257         | _ ->
1258           hint := None;
1259           aux tables maxm flags cache elems)
1260     | [] ->
1261         (* complete failure *)
1262         Gaveup (tables, cache, maxm)
1263     | (m, s, _, _, [],_)::orlist ->
1264         (* complete success *)
1265         Proved (m, s, orlist, tables, cache, maxm)
1266     | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist ->
1267         (* skip since not Prop, don't even check if closed by side-effect *)
1268         aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1269     | (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
1270         (* partial success, cache g and go on *)
1271         let cache, orlist, fl, sibling_pruned =
1272           add_to_cache_and_del_from_orlist_if_green_cut
1273             g s m cache key todo orlist fl context size minsize
1274         in
1275         debug_print (lazy (AutoCache.cache_print context cache));
1276         let fl = remove_s_from_fl g fl in
1277         let don = if sibling_pruned then don else op::don in
1278         aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
1279     | (m, s, size, don, todo, fl)::orlist
1280       when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1281         debug_print (lazy ("FAIL: WIDTH"));
1282         (* too many goals in and generated by last th *)
1283         let cache = close_failures fl cache in
1284         aux tables maxm flags cache orlist
1285     | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
1286         debug_print
1287           (lazy ("FAIL: SIZE: "^string_of_int size ^
1288             " > " ^ string_of_int flags.maxsize ));
1289         (* we already have a too large proof term *)
1290         let cache = close_failures fl cache in
1291         aux tables maxm flags cache orlist
1292     | _ when Unix.gettimeofday () > flags.timeout ->
1293         (* timeout *)
1294         debug_print (lazy ("FAIL: TIMEOUT"));
1295         Gaveup (tables, cache, maxm)
1296     | (m, s, size, don, (D (gno,depth,P as g))::todo, fl)::orlist as status ->
1297         (* attack g *)
1298         match calculate_goal_ty g s m with
1299         | None ->
1300             (* closed by side effect *)
1301             debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1302             aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist)
1303         | Some (canonical_ctx, gty) ->
1304             let gsize, _ =
1305               Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty
1306             in
1307             if gsize > flags.maxgoalsizefactor then
1308               (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
1309                aux tables maxm flags cache orlist)
1310             else if prunable_for_size flags s m todo then
1311                 (prerr_endline ("POTO at depth: "^(string_of_int depth));
1312                  aux tables maxm flags cache orlist)
1313             else
1314             (* still to be proved *)
1315             (debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
1316             match cache_examine cache gty with
1317             | Failed_in d when d >= depth ->
1318                 (* fail depth *)
1319                 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1320                 let cache = close_failures fl cache in
1321                 aux tables maxm flags cache orlist
1322             | UnderInspection ->
1323                 (* fail loop *)
1324                 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1325                 let cache = close_failures fl cache in
1326                 aux tables maxm flags cache orlist
1327             | Succeded t ->
1328                 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1329                 let s, m = put_in_subst s m g canonical_ctx t gty in
1330                 aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
1331             | Notfound
1332             | Failed_in _ when depth > 0 ->
1333                 ( (* more depth or is the first time we see the goal *)
1334                     if prunable m s gty todo then
1335                       (debug_print (lazy(
1336                          "FAIL: LOOP: one father is equal"));
1337                        aux tables maxm flags cache orlist)
1338                     else
1339                     let cache = cache_add_underinspection cache gty depth in
1340                     auto_status := status;
1341                     check_pause ();
1342                     debug_print
1343                       (lazy ("INSPECTING: " ^
1344                         string_of_int gno ^ "("^ string_of_int size ^ "): "^
1345                         CicPp.ppterm gty));
1346                     (* elems are possible computations for proving gty *)
1347                     let elems, tables, cache, maxm, flags =
1348                       equational_and_applicative_case
1349                         universe flags m s g gty tables cache maxm context
1350                     in
1351                     if elems = [] then
1352                       (* this goal has failed *)
1353                       let cache = close_failures ((g,gty)::fl) cache in
1354                       aux tables maxm flags cache orlist
1355                     else
1356                       (* elems = (cand,m,s,gl) *)
1357                       let size_gl l = List.length
1358                         (List.filter (function (_,_,P) -> true | _ -> false) l)
1359                       in
1360                       let elems =
1361                         let inj_gl gl = List.map (fun g -> D g) gl in
1362                         let rec map = function
1363                           | [] -> assert false
1364                           | (cand,m,s,gl)::[] ->
1365                               (* in the last one we add the failure *)
1366                               let todo =
1367                                 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1368                               in
1369                               (* we are the last in OR, we fail on g and
1370                                * also on all failures implied by g *)
1371                               (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
1372                               :: orlist
1373                           | (cand,m,s,gl)::tl ->
1374                               (* we add the S step after gl and before todo *)
1375                               let todo =
1376                                 inj_gl gl @ (S(g,gty,cand,size+1))::todo
1377                               in
1378                               (* since we are not the last in OR, we do not
1379                                * imply failures *)
1380                               (m,s, size + size_gl gl, don, todo, []) :: map tl
1381                         in
1382                           map elems
1383                       in
1384                         aux tables maxm flags cache elems)
1385             | _ ->
1386                 (* no more depth *)
1387                 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1388                 let cache = close_failures fl cache in
1389                 aux tables maxm flags cache orlist)
1390   in
1391     (aux tables maxm flags cache elems : auto_result)
1392 ;;
1393
1394
1395 let
1396   auto_all_solutions maxm tables universe cache context metasenv gl flags
1397 =
1398   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1399   let goals =
1400     List.map
1401       (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1402   in
1403   let elems = [metasenv,[],1,[],goals,[]] in
1404   let rec aux tables maxm solutions cache elems flags =
1405     match auto_main tables maxm context flags universe cache elems with
1406     | Gaveup (tables,cache,maxm) ->
1407         solutions,cache,maxm
1408     | Proved (metasenv,subst,others,tables,cache,maxm) ->
1409         if Unix.gettimeofday () > flags.timeout then
1410           ((subst,metasenv)::solutions), cache, maxm
1411         else
1412           aux tables maxm ((subst,metasenv)::solutions) cache others flags
1413   in
1414   let rc = aux tables maxm [] cache elems flags in
1415     match rc with
1416     | [],cache,maxm -> [],cache,maxm
1417     | solutions,cache,maxm ->
1418         let solutions =
1419           HExtlib.filter_map
1420             (fun (subst,newmetasenv) ->
1421               let opened =
1422                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1423               in
1424               if opened = [] then Some subst else None)
1425             solutions
1426         in
1427          solutions,cache,maxm
1428 ;;
1429
1430 (* }}} ****************** AUTO ***************)
1431
1432 let auto flags metasenv tables universe cache context metasenv gl =
1433   let initial_time = Unix.gettimeofday() in
1434   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1435   let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1436   let elems = [metasenv,[],1,[],goals,[]] in
1437   match auto_main tables 0 context flags universe cache elems with
1438   | Proved (metasenv,subst,_, tables,cache,_) ->
1439       debug_print(lazy
1440         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1441       Some (subst,metasenv), cache
1442   | Gaveup (tables,cache,maxm) ->
1443       debug_print(lazy
1444         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1445       None,cache
1446 ;;
1447
1448 let bool params name default =
1449     try
1450       let s = List.assoc name params in
1451       if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
1452       else if s = "0" || s = "false" || s = "no" || s= "off" then false
1453       else
1454         let msg = "Unrecognized value for parameter "^name^"\n" in
1455         let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
1456         raise (ProofEngineTypes.Fail (lazy msg))
1457     with Not_found -> default
1458 ;;
1459
1460 let string params name default =
1461     try List.assoc name params with
1462     | Not_found -> default
1463 ;;
1464
1465 let int params name default =
1466     try int_of_string (List.assoc name params) with
1467     | Not_found -> default
1468     | Failure _ ->
1469         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
1470 ;;
1471
1472 let flags_of_params params ?(for_applyS=false) () =
1473  let int = int params in
1474  let bool = bool params in
1475  let close_more = bool "close_more" false in
1476  let use_paramod = bool "use_paramod" true in
1477  let use_only_paramod =
1478   if for_applyS then true else bool "paramodulation" false in
1479  let use_library = bool "library"
1480    ((AutoTypes.default_flags()).AutoTypes.use_library) in
1481  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
1482  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
1483  let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
1484  let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
1485  let timeout = int "timeout" 0 in
1486   { AutoTypes.maxdepth =
1487       if use_only_paramod then 2 else depth;
1488     AutoTypes.maxwidth = width;
1489     AutoTypes.maxsize = size;
1490     AutoTypes.timeout =
1491       if timeout = 0 then
1492        if for_applyS then Unix.gettimeofday () +. 30.0
1493        else
1494          infinity
1495       else
1496        Unix.gettimeofday() +. (float_of_int timeout);
1497     AutoTypes.use_library = use_library;
1498     AutoTypes.use_paramod = use_paramod;
1499     AutoTypes.use_only_paramod = use_only_paramod;
1500     AutoTypes.close_more = close_more;
1501     AutoTypes.dont_cache_failures = false;
1502     AutoTypes.maxgoalsizefactor = gsize;
1503   }
1504
1505 let applyS_tac ~dbd ~term ~params ~universe =
1506  ProofEngineTypes.mk_tactic
1507   (fun status ->
1508     try
1509       let proof, gl,_,_ =
1510        apply_smart ~dbd ~term ~subst:[] ~universe
1511         (flags_of_params params ~for_applyS:true ()) status
1512       in
1513        proof, gl
1514     with
1515     | CicUnification.UnificationFailure msg
1516     | CicTypeChecker.TypeCheckerFailure msg ->
1517         raise (ProofEngineTypes.Fail msg))
1518
1519 (* SUPERPOSITION *)
1520
1521 (* Syntax:
1522  *   auto superposition target = NAME
1523  *     [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
1524  *
1525  *  - if table is omitted no superposition will be performed
1526  *  - if demod_table is omitted no demodulation will be prformed
1527  *  - subterms_only is passed to Indexing.superposition_right
1528  *
1529  *  lists are coded using _ (example: H_H1_H2)
1530  *)
1531
1532 let eq_and_ty_of_goal = function
1533   | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1534       uri,t
1535   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1536 ;;
1537
1538 let rec find_in_ctx i name = function
1539   | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
1540   | Some (Cic.Name name', _)::tl when name = name' -> i
1541   | _::tl -> find_in_ctx (i+1) name tl
1542 ;;
1543
1544 let rec position_of i x = function
1545   | [] -> assert false
1546   | j::tl when j <> x -> position_of (i+1) x tl
1547   | _ -> i
1548 ;;
1549
1550
1551 let superposition_tac ~target ~table ~subterms_only ~demod_table status =
1552   Saturation.reset_refs();
1553   let proof,goalno = status in
1554   let curi,metasenv,_subst,pbo,pty, attrs = proof in
1555   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
1556   let eq_uri,tty = eq_and_ty_of_goal ty in
1557   let env = (metasenv, context, CicUniv.empty_ugraph) in
1558   let names = Utils.names_of_context context in
1559   let bag = Equality.mk_equality_bag () in
1560   let eq_index, equalities, maxm,cache  =
1561     find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
1562   in
1563   let eq_what =
1564     let what = find_in_ctx 1 target context in
1565     List.nth equalities (position_of 0 what eq_index)
1566   in
1567   let eq_other =
1568     if table <> "" then
1569       let other =
1570         let others = Str.split (Str.regexp "_") table in
1571         List.map (fun other -> find_in_ctx 1 other context) others
1572       in
1573       List.map
1574         (fun other -> List.nth equalities (position_of 0 other eq_index))
1575         other
1576     else
1577       []
1578   in
1579   let index = List.fold_left Indexing.index Indexing.empty eq_other in
1580   let maxm, eql =
1581     if table = "" then maxm,[eq_what] else
1582     Indexing.superposition_right bag
1583       ~subterms_only eq_uri maxm env index eq_what
1584   in
1585   debug_print (lazy ("Superposition right:"));
1586   debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env));
1587   debug_print (lazy ("\n table: "));
1588   List.iter
1589     (fun e ->
1590        debug_print (lazy ("  " ^ Equality.string_of_equality e ~env))) eq_other;
1591   debug_print (lazy ("\n result: "));
1592   List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1593   debug_print (lazy ("\n result (cut&paste): "));
1594   List.iter
1595     (fun e ->
1596       let t = Equality.term_of_equality eq_uri e in
1597       debug_print (lazy (CicPp.pp t names)))
1598   eql;
1599   debug_print (lazy ("\n result proofs: "));
1600   List.iter (fun e ->
1601     debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in
1602     let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
1603     Subst.ppsubst s ^ "\n" ^
1604     CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql;
1605   if demod_table <> "" then
1606     begin
1607       let eql =
1608         if eql = [] then [eq_what] else eql
1609       in
1610       let demod =
1611         let demod = Str.split (Str.regexp "_") demod_table in
1612         List.map (fun other -> find_in_ctx 1 other context) demod
1613       in
1614       let eq_demod =
1615         List.map
1616           (fun demod -> List.nth equalities (position_of 0 demod eq_index))
1617           demod
1618       in
1619       let table = List.fold_left Indexing.index Indexing.empty eq_demod in
1620       let maxm,eql =
1621         List.fold_left
1622           (fun (maxm,acc) e ->
1623             let maxm,eq =
1624               Indexing.demodulation_equality bag eq_uri maxm env table e
1625             in
1626             maxm,eq::acc)
1627           (maxm,[]) eql
1628       in
1629       let eql = List.rev eql in
1630       debug_print (lazy ("\n result [demod]: "));
1631       List.iter
1632         (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1633       debug_print (lazy ("\n result [demod] (cut&paste): "));
1634       List.iter
1635         (fun e ->
1636           let t = Equality.term_of_equality eq_uri e in
1637           debug_print (lazy (CicPp.pp t names)))
1638       eql;
1639     end;
1640   proof,[goalno]
1641 ;;
1642
1643 let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) =
1644   (* argument parsing *)
1645   let string = string params in
1646   let bool = bool params in
1647   (* hacks to debug paramod *)
1648   let superposition = bool "superposition" false in
1649   let target = string "target" "" in
1650   let table = string "table" "" in
1651   let subterms_only = bool "subterms_only" false in
1652   let demod_table = string "demod_table" "" in
1653   match superposition with
1654   | true ->
1655       (* this is the ugly hack to debug paramod *)
1656       superposition_tac
1657         ~target ~table ~subterms_only ~demod_table (proof,goal)
1658   | false ->
1659       (* this is the real auto *)
1660       let _,metasenv,_subst,_,_, _ = proof in
1661       let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1662       let flags = flags_of_params params () in
1663       (* just for testing *)
1664       let use_library = flags.use_library in
1665       let tables,cache,newmeta =
1666         init_cache_and_tables dbd use_library flags.use_only_paramod
1667           universe (proof, goal) in
1668       let tables,cache,newmeta =
1669         if flags.close_more then
1670           close_more
1671             tables newmeta context (proof, goal)
1672               auto_all_solutions universe cache
1673         else tables,cache,newmeta in
1674       let initial_time = Unix.gettimeofday() in
1675       let (_,oldmetasenv,_subst,_,_, _) = proof in
1676       hint := None;
1677       let elem =
1678         metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[]
1679       in
1680       match auto_main tables newmeta context flags universe cache [elem] with
1681         | Proved (metasenv,subst,_, tables,cache,_) ->
1682             prerr_endline
1683               ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
1684             let proof,metasenv =
1685             ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1686               proof goal subst metasenv
1687             in
1688             let opened =
1689               ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1690                 ~newmetasenv:metasenv
1691             in
1692               proof,opened
1693         | Gaveup (tables,cache,maxm) ->
1694             debug_print
1695               (lazy ("TIME:"^
1696                 string_of_float(Unix.gettimeofday()-.initial_time)));
1697             raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1698 ;;
1699
1700 let auto_tac ~dbd ~params ~universe =
1701   ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1702
1703 let eq_of_goal = function
1704   | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1705       uri
1706   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1707 ;;
1708
1709 (* DEMODULATE *)
1710 let demodulate_tac ~dbd ~universe (proof,goal)=
1711   let curi,metasenv,_subst,pbo,pty, attrs = proof in
1712   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1713   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1714   let initgoal = [], [], ty in
1715   let eq_uri = eq_of_goal ty in
1716   let (active,passive,bag), cache, maxm =
1717      init_cache_and_tables dbd false true universe (proof,goal) in
1718   let equalities = (Saturation.list_of_passive passive) in
1719   (* we demodulate using both actives passives *)
1720   let table =
1721     List.fold_left
1722       (fun tbl eq -> Indexing.index tbl eq)
1723       (snd active) equalities
1724   in
1725   let changed,(newproof,newmetasenv, newty) =
1726     Indexing.demodulation_goal bag
1727       (metasenv,context,CicUniv.empty_ugraph) table initgoal
1728   in
1729   if changed then
1730     begin
1731       let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1732       let proofterm,_ =
1733         Equality.build_goal_proof bag
1734           eq_uri newproof opengoal ty [] context metasenv
1735       in
1736         let extended_metasenv = (maxm,context,newty)::metasenv in
1737         let extended_status =
1738           (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
1739         let (status,newgoals) =
1740           ProofEngineTypes.apply_tactic
1741             (PrimitiveTactics.apply_tac ~term:proofterm)
1742             extended_status in
1743         (status,maxm::newgoals)
1744     end
1745   else (* if newty = ty then *)
1746     raise (ProofEngineTypes.Fail (lazy "no progress"))
1747   (*else ProofEngineTypes.apply_tactic
1748     (ReductionTactics.simpl_tac
1749       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1750 ;;
1751
1752 let demodulate_tac ~dbd ~universe =
1753   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
1754
1755 let pp_proofterm = Equality.pp_proofterm;;
1756
1757 let revision = "$Revision$";;