components/tactics/auto.ml

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