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, _, _, _ = 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,_,_, _ = 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,_,_, _ = 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,pbo,pty, attrs) = proof in
 472    (puri,newmetasenv,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'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs in
 483  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
 484  let proof''',goals =
 485   ProofEngineTypes.apply_tactic
 486     (EqualityTactics.rewrite_tac ~direction:`RightToLeft
 487       ~pattern:(ProofEngineTypes.conclusion_pattern None)
 488         (Cic.Meta(newmeta,irl)) [])
 489    (proof'',goal)
 490  in
 491  let goal = match goals with [g] -> g | _ -> assert false in
 492  let subst, (proof'''', _), _ =
 493    PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
 494  in
 495  match
 496    let (active, passive,bag), cache, maxmeta =
 497      init_cache_and_tables dbd flags.use_library true universe (proof'''',newmeta)
 498    in
 499      Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
 500        max_int max_int flags.timeout
 501  with
 502  | None, _,_,_ ->
 503      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
 504  | Some (_,proof''''',_), active,passive,_  ->
 505      subst,proof''''',
 506      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
 507        ~newmetasenv:(let _,m,_,_, _ = proof''''' in m),  active, passive
 508 ;;
 509
 510 let rec count_prods context ty =
 511  match CicReduction.whd context ty with
 512     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
 513   | _ -> 0
 514
 515 let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
 516  let module T = CicTypeChecker in
 517  let module R = CicReduction in
 518  let module C = Cic in
 519   let (_,metasenv,_,_, _) = proof in
 520   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 521   let newmeta = CicMkImplicit.new_meta metasenv subst in
 522    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
 523     match term with
 524        C.Var (uri,exp_named_subst) ->
 525         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 526          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 527           exp_named_subst
 528         in
 529          exp_named_subst_diff,newmeta',newmetasenvfragment,
 530           C.Var (uri,exp_named_subst')
 531      | C.Const (uri,exp_named_subst) ->
 532         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 533          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 534           exp_named_subst
 535         in
 536          exp_named_subst_diff,newmeta',newmetasenvfragment,
 537           C.Const (uri,exp_named_subst')
 538      | C.MutInd (uri,tyno,exp_named_subst) ->
 539         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 540          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 541           exp_named_subst
 542         in
 543          exp_named_subst_diff,newmeta',newmetasenvfragment,
 544           C.MutInd (uri,tyno,exp_named_subst')
 545      | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 546         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 547          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 548           exp_named_subst
 549         in
 550          exp_named_subst_diff,newmeta',newmetasenvfragment,
 551           C.MutConstruct (uri,tyno,consno,exp_named_subst')
 552      | _ -> [],newmeta,[],term
 553    in
 554    let metasenv' = metasenv@newmetasenvfragment in
 555    let termty,_ =
 556      CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
 557    in
 558    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
 559    let goal_arity = count_prods context ty in
 560    let subst, proof, gl, active, passive =
 561     new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
 562      newmeta' metasenv' context term' ty termty goal_arity
 563    in
 564     subst, proof, gl, active, passive
 565 ;;
 566
 567 (****************** AUTO ********************)
 568
 569 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
 570 let ugraph = CicUniv.empty_ugraph;;
 571 let typeof = CicTypeChecker.type_of_aux';;
 572 let ppterm ctx t =
 573   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
 574   CicPp.pp t names
 575 ;;
 576 let is_in_prop context subst metasenv ty =
 577   let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
 578   fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
 579 ;;
 580
 581 let assert_proof_is_valid proof metasenv context goalty =
 582   if debug then
 583     begin
 584       let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
 585       let b,_ = CicReduction.are_convertible context ty goalty u in
 586         if not b then
 587           begin
 588             let names =
 589               List.map (function None -> None | Some (x,_) -> Some x) context
 590             in
 591               debug_print (lazy ("PROOF:" ^ CicPp.pp proof names));
 592               debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names));
 593               debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names));
 594               debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv));
 595           end;
 596         assert b
 597     end
 598   else ()
 599 ;;
 600
 601 let assert_subst_are_disjoint subst subst' =
 602   if debug then
 603     assert(List.for_all
 604              (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
 605              subst)
 606   else ()
 607 ;;
 608
 609 let split_goals_in_prop metasenv subst gl =
 610   List.partition
 611     (fun g ->
 612       let _,context,ty = CicUtil.lookup_meta g metasenv in
 613       try
 614         let sort,u = typeof ~subst metasenv context ty ugraph in
 615         let b,_ =
 616           CicReduction.are_convertible
 617             ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
 618         b
 619       with
 620       | CicTypeChecker.AssertFailure s
 621       | CicTypeChecker.TypeCheckerFailure s ->
 622           debug_print
 623             (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty)));
 624           debug_print s;
 625           false)
 626     (* FIXME... they should type! *)
 627     gl
 628 ;;
 629
 630 let split_goals_with_metas metasenv subst gl =
 631   List.partition
 632     (fun g ->
 633       let _,context,ty = CicUtil.lookup_meta g metasenv in
 634       let ty = CicMetaSubst.apply_subst subst ty in
 635       CicUtil.is_meta_closed ty)
 636     gl
 637 ;;
 638
 639 let order_new_goals metasenv subst open_goals ppterm =
 640   let prop,rest = split_goals_in_prop metasenv subst open_goals in
 641   let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
 642   let open_goals =
 643     (List.map (fun x -> x,P) (closed_prop @ open_prop))
 644     @
 645     (List.map (fun x -> x,T) rest)
 646   in
 647   let tys =
 648     List.map
 649       (fun (i,sort) ->
 650         let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
 651   in
 652   debug_print (lazy ("   OPEN: "^
 653     String.concat "\n"
 654       (List.map
 655          (function
 656             | (i,t,P) -> string_of_int i   ^ ":"^ppterm t^ "Prop"
 657             | (i,t,T) -> string_of_int i  ^ ":"^ppterm t^ "Type")
 658          tys)));
 659   open_goals
 660 ;;
 661
 662 let is_an_equational_goal = function
 663   | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
 664   | _ -> false
 665 ;;
 666
 667 (*
 668 let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
 669 *)
 670
 671 let calculate_timeout flags =
 672     if flags.timeout = 0. then
 673       (debug_print (lazy "AUTO WITH NO TIMEOUT");
 674        {flags with timeout = infinity})
 675     else
 676       flags
 677 ;;
 678 let is_equational_case goalty flags =
 679   let ensure_equational t =
 680     if is_an_equational_goal t then true
 681     else false
 682     (*
 683       let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
 684       raise (ProofEngineTypes.Fail (lazy msg))
 685     *)
 686   in
 687   (flags.use_paramod && is_an_equational_goal goalty) ||
 688   (flags.use_only_paramod && ensure_equational goalty)
 689 ;;
 690 (*
 691 let cache_add_success sort cache k v =
 692   if sort = P then cache_add_success cache k v else cache_remove_underinspection
 693   cache k
 694 ;;
 695 *)
 696
 697 type menv = Cic.metasenv
 698 type subst = Cic.substitution
 699 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
 700 let candidate_no = ref 0;;
 701 type candidate = int * Cic.term
 702 type cache = AutoCache.cache
 703 type tables =
 704   Saturation.active_table * Saturation.passive_table * Equality.equality_bag
 705
 706 type fail =
 707   (* the goal (mainly for depth) and key of the goal *)
 708   goal * AutoCache.cache_key
 709 type op =
 710   (* goal has to be proved *)
 711   | D of goal
 712   (* goal has to be cached as a success obtained using candidate as the first
 713    * step *)
 714   | S of goal * AutoCache.cache_key * candidate * int
 715 type elem =
 716   (* menv, subst, size, operations to do, failures to cache if any op fails *)
 717   menv * subst * int * op list * fail list
 718 type status =
 719   (* list of computations that may lead to the solution: all op list will
 720    * end with the same (S(g,_)) *)
 721   elem list
 722 type auto_result =
 723   (* menv, subst, alternatives, tables, cache, maxmeta *)
 724   | Proved of menv * subst * elem list * tables * cache * int
 725   | Gaveup of tables * cache * int
 726
 727
 728 (* the status exported to the external observer *)
 729 type auto_status =
 730   (* context, (goal,candidate) list, and_list, history *)
 731   Cic.context * (Cic.term * (int * Cic.term) list) list *
 732   Cic.term list * Cic.term list
 733
 734 let d_prefix l =
 735   let rec aux acc = function
 736     | (D g)::tl -> aux (acc@[g]) tl
 737     | _ -> acc
 738   in
 739     aux [] l
 740 ;;
 741 let prop_only l =
 742   List.filter (function (_,_,P) -> true | _ -> false) l
 743 ;;
 744
 745 let d_goals l =
 746   let rec aux acc = function
 747     | (D g)::tl -> aux (acc@[g]) tl
 748     | (S _)::tl -> aux acc tl
 749     | [] -> acc
 750   in
 751     aux [] l
 752 ;;
 753 let calculate_goal_ty (goalno,_,_) s m =
 754   try
 755     let _,cc,goalty = CicUtil.lookup_meta goalno m in
 756     (* XXX applicare la subst al contesto? *)
 757     Some (cc, CicMetaSubst.apply_subst s goalty)
 758   with CicUtil.Meta_not_found i when i = goalno -> None
 759 ;;
 760 let calculate_closed_goal_ty (goalno,_,_) s =
 761   try
 762     let cc,_,goalty = List.assoc goalno s in
 763     (* XXX applicare la subst al contesto? *)
 764     Some (cc, CicMetaSubst.apply_subst s goalty)
 765   with Not_found -> None
 766 ;;
 767 let pp_status ctx status =
 768   if debug then
 769   let names = Utils.names_of_context ctx in
 770   let pp x =
 771     let x =
 772       ProofEngineReduction.replace
 773         ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
 774           ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
 775     in
 776     CicPp.pp x names
 777   in
 778   let string_of_do m s (gi,_,_ as g) d =
 779     match calculate_goal_ty g s m with
 780     | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
 781     | None -> Printf.sprintf "D(%d, _, %d)" gi d
 782   in
 783   let string_of_s m su k (ci,ct) gi =
 784     Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp ct) ci
 785   in
 786   let string_of_ol m su l =
 787     String.concat " | "
 788       (List.map
 789         (function
 790           | D (g,d,s) -> string_of_do m su (g,d,s) d
 791           | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
 792         l)
 793   in
 794   let string_of_fl m s fl =
 795     String.concat " | "
 796       (List.map (fun ((i,_,_),ty) ->
 797          Printf.sprintf "(%d, %s)" i (pp ty)) fl)
 798   in
 799   let rec aux = function
 800     | [] -> ()
 801     | (m,s,ol,fl)::tl ->
 802         Printf.eprintf "< [%s] ;;; [%s]>\n"
 803           (string_of_ol m s ol) (string_of_fl m s fl);
 804         aux tl
 805   in
 806     Printf.eprintf "-------------------------- status -------------------\n";
 807     aux status;
 808     Printf.eprintf "-----------------------------------------------------\n";
 809 ;;
 810
 811 let auto_status = ref [] ;;
 812 let auto_context = ref [];;
 813 let in_pause = ref false;;
 814 let pause b = in_pause := b;;
 815 let cond = Condition.create ();;
 816 let mutex = Mutex.create ();;
 817 let hint = ref None;;
 818
 819 let step _ = Condition.signal cond;;
 820 let give_hint n = hint := Some n;;
 821
 822 let check_pause _ =
 823   if !in_pause then
 824     begin
 825       Mutex.lock mutex;
 826       Condition.wait cond mutex;
 827       Mutex.unlock mutex
 828     end
 829 ;;
 830
 831 let get_auto_status _ =
 832   let status = !auto_status in
 833 (*
 834   debug_print "status:";
 835   List.iter (fun ((cand,ty),_,_,gl) ->
 836     Printf.eprintf "cand: %s; ty: %s; gl: %d\n"
 837       (CicPp.ppterm cand) (CicPp.ppterm ty) (List.length gl)) status;
 838 *)
 839   let and_list,elems,last =
 840     match status with
 841     | [] -> [],[],[]
 842     | (m,s,_,gl,fail)::tl ->
 843         let and_list =
 844           List.map snd
 845             (HExtlib.filter_map
 846               (fun g -> calculate_goal_ty g s m) (d_goals gl))
 847         in
 848         let rows =
 849           (* these are the S goalsin the or list *)
 850           let orlist =
 851             List.map
 852               (fun (m,s,_,gl,fail) ->
 853                 HExtlib.filter_map
 854                   (function S (g,k,c,_) -> Some (g,k,c) | _ -> None) gl)
 855               status
 856           in
 857           (* this function eats id from a list l::[id,x] returning x, l *)
 858           let eat_tail_if_eq id l =
 859             match (List.rev l) with
 860             | ((id1,_,_),k1,c)::tl when id = id1 -> Some c, List.rev tl
 861             | _ -> None, l
 862           in
 863           let eat_in_parallel id l =
 864             let rec aux (eaten, new_l as acc) l =
 865               match l with
 866               | [] -> acc
 867               | l::tl ->
 868                   match eat_tail_if_eq id l with
 869                   | None, l -> aux (eaten, new_l@[l]) tl
 870                   | Some t,l -> aux (eaten@[t], new_l@[l]) tl
 871             in
 872             aux ([],[]) l
 873           in
 874           let rec eat_all rows l =
 875             match l with
 876             | [] -> rows
 877             | elem::or_list ->
 878                 match List.rev elem with
 879                 | ((to_eat,_,_),k,_)::next_lunch ->
 880                     let eaten, l = eat_in_parallel to_eat l in
 881                     let eaten = HExtlib.list_uniq eaten in
 882                     let rows = rows @ [k,eaten] in
 883                     eat_all rows l
 884                 | [] -> eat_all rows or_list
 885           in
 886           eat_all [] orlist
 887         in
 888         let history =
 889           HExtlib.filter_map
 890             (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
 891             gl
 892         in
 893 (*         let rows = List.filter (fun (_,l) -> l <> []) rows in *)
 894         and_list, rows, history
 895   in
 896   !auto_context, elems, and_list, last
 897 ;;
 898
 899 (* Works if there is no dependency over proofs *)
 900 let is_a_green_cut goalty =
 901   CicUtil.is_meta_closed goalty
 902 ;;
 903 let rec first_s = function
 904   | (D _)::tl -> first_s tl
 905   | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
 906   | [] -> None
 907 ;;
 908 let list_union l1 l2 =
 909   (* TODO ottimizzare compare *)
 910   HExtlib.list_uniq (List.sort compare (l1 @ l1))
 911 ;;
 912 let eat_head todo id fl orlist =
 913   let rec aux acc = function
 914   | [] -> [], acc
 915   | (m, s, _, todo1, fl1)::tl as orlist ->
 916       let rec aux1 todo1 =
 917         match first_s todo1 with
 918         | None -> orlist, acc
 919         | Some (((gno,_,_),_,_,_), todo11) ->
 920             (* TODO confronto tra todo da ottimizzare *)
 921             if gno = id && todo11 = todo then
 922               aux (list_union fl1 acc) tl
 923             else
 924               aux1 todo11
 925       in
 926        aux1 todo1
 927   in
 928     aux fl orlist
 929 ;;
 930 let close_proof p ty menv context =
 931   let metas =
 932     List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
 933   in
 934   let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
 935   naif_closure p menv context
 936 ;;
 937 (* XXX capire bene quando aggiungere alla cache *)
 938 let add_to_cache_and_del_from_orlist_if_green_cut
 939   g s m cache key todo orlist fl ctx size minsize
 940 =
 941   let cache = cache_remove_underinspection cache key in
 942   (* prima per fare la irl usavamo il contesto vero e proprio e non quello
 943    * canonico! XXX *)
 944   match calculate_closed_goal_ty g s with
 945   | None -> assert false
 946   | Some (canonical_ctx , gty) ->
 947       let goalno,depth,sort = g in
 948       assert (sort = P);
 949       let irl = mk_irl canonical_ctx in
 950       let goal = Cic.Meta(goalno, irl) in
 951       let proof = CicMetaSubst.apply_subst s goal in
 952       let green_proof, closed_proof =
 953         let b = is_a_green_cut proof in
 954         if not b then
 955           b, (* close_proof proof gty m ctx *) proof
 956         else
 957           b, proof
 958       in
 959       debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
 960       if is_a_green_cut key then
 961         (* if the initia goal was closed, we cut alternatives *)
 962         let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
 963         let orlist, fl = eat_head todo goalno fl orlist in
 964         let cache =
 965           if size < minsize then
 966             (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
 967           else
 968           (* if the proof is closed we cache it *)
 969           if green_proof then cache_add_success cache key proof
 970           else (* cache_add_success cache key closed_proof *)
 971             (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
 972         in
 973         cache, orlist, fl
 974       else
 975         let cache =
 976           debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
 977           if size < minsize then
 978             (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
 979           (* if the substituted goal and the proof are closed we cache it *)
 980           if is_a_green_cut gty then
 981             if green_proof then cache_add_success cache gty proof
 982             else (* cache_add_success cache gty closed_proof *)
 983               (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
 984           else (*
 985             try
 986               let ty, _ =
 987                 CicTypeChecker.type_of_aux' ~subst:s
 988                   m ctx closed_proof CicUniv.oblivion_ugraph
 989               in
 990               if is_a_green_cut ty then
 991                 cache_add_success cache ty closed_proof
 992               else cache
 993             with
 994             | CicTypeChecker.TypeCheckerFailure _ ->*)
 995           (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
 996         in
 997         cache, orlist, fl
 998 ;;
 999 let close_failures (fl : fail list) (cache : cache) =
1000   List.fold_left
1001     (fun cache ((gno,depth,_),gty) ->
1002       debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
1003       cache_add_failure cache gty depth)
1004     cache fl
1005 ;;
1006 let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
1007   let entry = goalno, (canonical_ctx, t,ty) in
1008   assert_subst_are_disjoint subst [entry];
1009   let subst = entry :: subst in
1010   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1011   subst, metasenv
1012 ;;
1013 let mk_fake_proof metasenv (goalno,_,_) goalty context =
1014   None,metasenv,Cic.Meta(goalno,mk_irl context),goalty, []
1015 ;;
1016 let equational_case
1017   tables maxm cache depth fake_proof goalno goalty subst context
1018     flags
1019 =
1020   let active,passive,bag = tables in
1021   let ppterm = ppterm context in
1022   let status = (fake_proof,goalno) in
1023     if flags.use_only_paramod then
1024       begin
1025         debug_print (lazy ("PARAMODULATION SU: " ^
1026                          string_of_int goalno ^ " " ^ ppterm goalty ));
1027         let goal_steps, saturation_steps, timeout =
1028           max_int,max_int,flags.timeout
1029         in
1030         match
1031           Saturation.given_clause bag maxm status active passive
1032             goal_steps saturation_steps timeout
1033         with
1034           | None, active, passive, maxmeta ->
1035               [], (active,passive,bag), cache, maxmeta, flags
1036           | Some(subst',(_,metasenv,proof,_, _),open_goals),active,
1037             passive,maxmeta ->
1038               assert_subst_are_disjoint subst subst';
1039               let subst = subst@subst' in
1040               let open_goals =
1041                 order_new_goals metasenv subst open_goals ppterm
1042               in
1043               let open_goals =
1044                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1045               in
1046               incr candidate_no;
1047                       [(!candidate_no,proof),metasenv,subst,open_goals],
1048                 (active,passive,bag),
1049                 cache, maxmeta, flags
1050       end
1051     else
1052       begin
1053         debug_print
1054           (lazy
1055            ("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
1056         let res, maxmeta =
1057           Saturation.all_subsumed bag maxm status active passive
1058         in
1059         assert (maxmeta >= maxm);
1060         let res' =
1061           List.map
1062             (fun subst',(_,metasenv,proof,_, _),open_goals ->
1063                assert_subst_are_disjoint subst subst';
1064                let subst = subst@subst' in
1065                let open_goals =
1066                  order_new_goals metasenv subst open_goals ppterm
1067                in
1068                let open_goals =
1069                  List.map (fun (x,sort) -> x,depth-1,sort) open_goals
1070                in
1071                incr candidate_no;
1072                  (!candidate_no,proof),metasenv,subst,open_goals)
1073             res
1074           in
1075           res', (active,passive,bag), cache, maxmeta, flags
1076       end
1077 ;;
1078
1079 let try_candidate
1080   goalty tables maxm subst fake_proof goalno depth context cand
1081 =
1082   let ppterm = ppterm context in
1083   try
1084     let subst', ((_,metasenv,_,_, _), open_goals), maxmeta =
1085       PrimitiveTactics.apply_with_subst
1086         ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
1087     in
1088     debug_print (lazy ("   OK: " ^ ppterm cand));
1089     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
1090     let subst = subst' in
1091     let open_goals = order_new_goals metasenv subst open_goals ppterm in
1092     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
1093     incr candidate_no;
1094     Some ((!candidate_no,cand),metasenv,subst,open_goals), tables , maxmeta
1095   with
1096     | ProofEngineTypes.Fail s -> None,tables, maxm
1097     | CicUnification.Uncertain s ->  None,tables, maxm
1098 ;;
1099
1100 let sort_new_elems =
1101   List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2)
1102 ;;
1103
1104 let applicative_case
1105   tables maxm depth subst fake_proof goalno goalty metasenv context universe
1106   cache
1107 =
1108   let candidates = get_candidates universe cache goalty in
1109   let tables, elems, maxm =
1110     List.fold_left
1111       (fun (tables,elems,maxm) cand ->
1112         match
1113           try_candidate goalty
1114             tables maxm subst fake_proof goalno depth context cand
1115         with
1116         | None, tables,maxm  -> tables,elems, maxm
1117         | Some x, tables, maxm -> tables,x::elems, maxm)
1118       (tables,[],maxm) candidates
1119   in
1120   let elems = sort_new_elems elems in
1121   elems, tables, cache, maxm
1122 ;;
1123
1124 let equational_and_applicative_case
1125   universe flags m s g gty tables cache maxm context
1126 =
1127   let goalno, depth, sort = g in
1128   let fake_proof = mk_fake_proof m g gty context in
1129   if is_equational_case gty flags then
1130     let elems,tables,cache,maxm1, flags =
1131       equational_case tables maxm cache
1132         depth fake_proof goalno gty s context flags
1133     in
1134     let maxm = maxm1 in
1135     let more_elems, tables, cache, maxm1 =
1136       if flags.use_only_paramod then
1137         [],tables, cache, maxm
1138       else
1139         applicative_case
1140           tables maxm depth s fake_proof goalno
1141             gty m context universe cache
1142     in
1143     let maxm = maxm1 in
1144       elems@more_elems, tables, cache, maxm, flags
1145   else
1146     let elems, tables, cache, maxm =
1147       applicative_case tables maxm depth s fake_proof goalno
1148         gty m context universe cache
1149     in
1150       elems, tables, cache, maxm, flags
1151 ;;
1152 let rec first_s_cand = function
1153   | [] -> 0
1154   | S (_,_,(i,_),_):: _ -> i
1155   | _::tl -> first_s_cand tl
1156 ;;
1157 let remove_s_from_fl (id,_,_) (fl : fail list) =
1158   let rec aux = function
1159     | [] -> []
1160     | ((id1,_,_),_)::tl when id = id1 -> tl
1161     | hd::tl ->  hd :: aux tl
1162   in
1163     aux fl
1164 ;;
1165 let auto_main tables maxm context flags universe cache elems =
1166   auto_context := context;
1167   let rec aux tables maxm flags cache (elems : status) =
1168 (*     pp_status context elems;  *)
1169     match elems with
1170     | [] ->
1171         (* complete failure *)
1172         Gaveup (tables, cache, maxm)
1173     | (m, s, _, [],_)::orlist ->
1174         (* complete success *)
1175         Proved (m, s, orlist, tables, cache, maxm)
1176     | (m, s, size, (D (_,_,T))::todo, fl)::orlist ->
1177         (* skip since not Prop, don't even check if closed by side-effect *)
1178         aux tables maxm flags cache ((m, s, size, todo, fl)::orlist)
1179     | (m, s, size, (S(g, key, c,minsize))::todo, fl)::orlist ->
1180         (* partial success, cache g and go on *)
1181         let cache, orlist, fl =
1182           add_to_cache_and_del_from_orlist_if_green_cut
1183             g s m cache key todo orlist fl context size minsize
1184         in
1185         debug_print (lazy (AutoCache.cache_print context cache));
1186         let fl = remove_s_from_fl g fl in
1187         aux tables maxm flags cache ((m, s, size, todo, fl)::orlist)
1188     | (m, s, size, todo, fl)::orlist
1189       when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1190         debug_print (lazy ("FAIL: WIDTH"));
1191         (* too many goals in and generated by last th *)
1192         let cache = close_failures fl cache in
1193         aux tables maxm flags cache orlist
1194     | (m, s, size, todo, fl)::orlist
1195       when size > flags.maxsize ->
1196         debug_print (lazy ("FAIL: SIZE"));
1197         (* we already have a too large proof term *)
1198         let cache = close_failures fl cache in
1199         aux tables maxm flags cache orlist
1200     | _ when Unix.gettimeofday () > flags.timeout ->
1201         (* timeout *)
1202         debug_print (lazy ("FAIL: SIZE"));
1203         Gaveup (tables, cache, maxm)
1204     | (m, s, size, (D (gno,depth,P as g))::todo, fl)::orlist as status ->
1205         (* attack g *)
1206         match calculate_goal_ty g s m with
1207         | None ->
1208             (* closed by side effect *)
1209             debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1210             aux tables maxm flags cache ((m,s,size,todo, fl)::orlist)
1211         | Some (canonical_ctx, gty) ->
1212             (* still to be proved *)
1213             debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
1214             debug_print (lazy (AutoCache.cache_print context cache));
1215             match cache_examine cache gty with
1216             | Failed_in d when d >= depth ->
1217                 (* fail depth *)
1218                 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1219                 let cache = close_failures fl cache in
1220                 aux tables maxm flags cache orlist
1221             | UnderInspection ->
1222                 (* fail loop *)
1223                 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1224                 let cache = close_failures fl cache in
1225                 aux tables maxm flags cache orlist
1226             | Succeded t ->
1227                 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1228                 let s, m = put_in_subst s m g canonical_ctx t gty in
1229                 aux tables maxm flags cache ((m, s, size, todo, fl)::orlist)
1230             | Notfound
1231             | Failed_in _ when depth > 0 ->
1232                 (match !hint with
1233                 | Some i when first_s_cand todo <> i ->
1234                     aux tables maxm flags cache orlist
1235                 | _ -> hint := None;
1236                     (* more depth or is the first time we see the goal *)
1237                     let cache = cache_add_underinspection cache gty depth in
1238                     auto_status := status;
1239                     check_pause ();
1240                     debug_print
1241                       (lazy ("INSPECTING: " ^
1242                         string_of_int gno ^ "("^ string_of_int size ^ "): "^CicPp.ppterm gty));
1243                     (* elems are possible computations for proving gty *)
1244                     let elems, tables, cache, maxm, flags =
1245                       equational_and_applicative_case
1246                         universe flags m s g gty tables cache maxm context
1247                     in
1248                     if elems = [] then
1249                       (* this goal has failed *)
1250                       let cache = close_failures ((g,gty)::fl) cache in
1251                       aux tables maxm flags cache orlist
1252                     else
1253                       (* elems = (cand,m,s,gl) *)
1254                       let size_gl l = List.length
1255                         (List.filter (function (_,_,P) -> true | _ -> false) l)
1256                       in
1257                       let elems =
1258                         let inj_gl gl = List.map (fun g -> D g) gl in
1259                         let rec map = function
1260                           | [] -> assert false
1261                           | (cand,m,s,gl)::[] ->
1262                               (* in the last one we add the failure *)
1263                               let todo = inj_gl gl @ (S(g,gty,cand,size+1))::todo in
1264                               (* we are the last in OR, we fail on g and
1265                                * also on all failures implied by g *)
1266                               (m,s, size + size_gl gl, todo, (g,gty)::fl) :: orlist
1267                           | (cand,m,s,gl)::tl ->
1268                               (* we add the S step after gl and before todo *)
1269                               let todo = inj_gl gl @ (S(g,gty,cand,size+1))::todo in
1270                               (* since we are not the last in OR, we do not
1271                                * imply failures *)
1272                               (m,s, size + size_gl gl, todo, []) :: map tl
1273                         in
1274                           map elems
1275                       in
1276                         aux tables maxm flags cache elems)
1277             | _ ->
1278                 (* no more depth *)
1279                 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1280                 let cache = close_failures fl cache in
1281                 aux tables maxm flags cache orlist
1282   in
1283     (aux tables maxm flags cache elems : auto_result)
1284 ;;
1285
1286 (*
1287 let rec auto_main tables maxm context flags elems universe cache =
1288   auto_context := context;
1289   let flags = calculate_timeout flags in
1290   let ppterm = ppterm context in
1291   let irl = mk_irl context in
1292   let rec aux flags tables maxm cache elems status =
1293     match elems with (* elems in OR *)
1294     | [] -> Fail "no more steps can be done", tables, cache, maxm
1295          (*COMPLETE FAILURE*)
1296     | (p ,metasenv,subst,[])::tl ->
1297         Success (p,metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
1298     | (_,metasenv,subst,goals)::tl when
1299       List.length (List.filter prop goals) > flags.maxwidth ->
1300         debug_print
1301           (lazy (" FAILURE(width): " ^ string_of_int (List.length goals)));
1302         aux flags tables maxm cache tl (List.tl status) (* FAILURE (width) *)
1303     | (p,metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
1304         let (_,_,_,_::gl_status)::tl_status = status in
1305         if Unix.gettimeofday() > flags.timeout then
1306           Fail "timeout",tables,cache,maxm
1307         else
1308         try
1309           let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
1310           let id,_,_ = p in
1311           debug_print
1312             (lazy ("INSPECTING " ^ string_of_int goalno^
1313             ":"^"(id="^string_of_int id^")"^ppterm goalty ^
1314                    "with depth"^string_of_int depth));
1315           debug_print (lazy (AutoCache.cache_print context cache));
1316           if sort = T (* && tl <> []*)  then
1317             (debug_print
1318                (lazy (" FAILURE(not in prop)"));
1319             aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
1320             ((p,metasenv,subst,gl)::tl_status))
1321           else
1322           match aux_single flags tables maxm universe cache metasenv subst elem
1323           goalty cc gl_status tl_status p with
1324           | Fail s, tables, cache, maxm' ->
1325               let maxm = maxm' in
1326               debug_print
1327                 (lazy
1328                    (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
1329               let cache =
1330                 if flags.dont_cache_failures or s = "hint" then
1331                   cache_remove_underinspection cache goalty
1332                 else
1333                   cache_add_failure cache goalty depth
1334               in
1335               aux flags tables maxm cache tl tl_status
1336           | Success (p1,metasenv,subst,others), tables, cache, maxm' ->
1337               let maxm = maxm' in
1338               (* others are alternatives in OR *)
1339               try
1340                 let goal = Cic.Meta(goalno,irl) in
1341                 let proof = CicMetaSubst.apply_subst subst goal in
1342                 debug_print
1343                   (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
1344                 if is_a_green_cut goalty then
1345                   (* assert_proof_is_valid proof metasenv context goalty; *)
1346                   let cache = cache_add_success sort cache goalty proof in
1347                   aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
1348                     ((p,metasenv,subst,gl)::tl_status)
1349
1350                 else
1351                   (let goalty = CicMetaSubst.apply_subst subst goalty in
1352                  (* assert_proof_is_valid proof metasenv context goalty; *)
1353                   let cache =
1354                     if is_a_green_cut goalty then
1355                       cache_add_success sort cache goalty proof
1356                     else
1357                       cache
1358                   in
1359                   let others =
1360                     List.map
1361                       (fun (p,metasenv,subst,goals) ->
1362                         (p,metasenv,subst,goals@gl))
1363                     others
1364                   in
1365                   aux flags tables maxm cache
1366                     ((p,metasenv,subst,gl)::others@tl)
1367                     ((p,metasenv,subst,gl)::others@tl_status)
1368
1369                     )
1370
1371               with CicUtil.Meta_not_found i when i = goalno ->
1372                 assert false
1373         with CicUtil.Meta_not_found i when i = goalno ->
1374           (* goalno was closed by sideeffect *)
1375           debug_print
1376             (lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
1377           aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
1378             ((p,metasenv,subst,gl)::tl_status)
1379
1380   and aux_single flags tables maxm universe cache metasenv subst (goalno, depth,
1381   _) goalty cc e l (id,_,_) =
1382     match !hint with
1383     | Some id' when id <> id' -> Fail "hint", tables,cache,maxm
1384     | _ ->
1385         hint := None;
1386     (* let flags = if depth < 10 then {flags with maxwidth=3} else flags in *)
1387     let goalty = CicMetaSubst.apply_subst subst goalty in
1388 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
1389       (* FAILURE (euristic cut) *)
1390     match cache_examine cache goalty with
1391     | Failed_in d when d >= depth ->
1392         Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
1393         tables,cache,maxm(*FAILURE(depth)*)
1394     | Succeded t ->
1395         let entry = goalno, (cc, t,goalty) in
1396         assert_subst_are_disjoint subst [entry];
1397         let subst = entry :: subst in
1398         let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1399         debug_print (lazy ("  CACHE HIT!"));
1400         incr candidate_no;
1401         Success ((!candidate_no,t,goalty),metasenv, subst, []), tables, cache, maxm
1402     | UnderInspection ->
1403         (* assert (not (is_a_green_cut goalty)); *)
1404         Fail "looping",tables,cache, maxm
1405     | Notfound
1406     | Failed_in _ when depth > 0 -> (* we have more depth now *)
1407         let cache = cache_add_underinspection cache goalty depth in
1408         let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty, [] in (* FG: attrs *)
1409         let elems, tables, cache, maxm, flags =
1410           if is_equational_case goalty flags then
1411             let elems,tables,cache,maxm1, flags =
1412               equational_case tables maxm cache
1413                 depth fake_proof goalno goalty subst context flags in
1414               let maxm = maxm1 in
1415             let more_elems, tables, cache, maxm1 =
1416               if flags.use_only_paramod then
1417                 [],tables, cache, maxm
1418               else
1419                 applicative_case
1420                   tables maxm depth subst fake_proof goalno
1421                   goalty metasenv context universe cache in
1422               let maxm = maxm1 in
1423               elems@more_elems, tables, cache, maxm, flags
1424           else
1425             let elems, tables, cache, maxm =
1426             applicative_case tables maxm depth subst fake_proof goalno
1427               goalty metasenv context universe cache in
1428             elems, tables, cache, maxm, flags
1429         in
1430         let status =
1431           List.map (fun (p,m,s,l) -> p,m,s,l@e) elems @ l
1432         in
1433     auto_status := status;
1434     check_pause ();
1435         let rc = aux flags tables maxm cache elems status in
1436         debug_print "BACK!";
1437         rc
1438     | _ -> Fail "depth = 0",tables,cache,maxm
1439   in
1440   aux flags tables maxm cache elems elems
1441
1442 and
1443 *)
1444
1445 (*
1446 let
1447   auto_all_solutions maxm tables universe cache context metasenv gl flags
1448 =
1449   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1450   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
1451   let elems = [(0,Cic.Implicit None,Cic.Implicit None), metasenv,[],goals] in
1452   let rec aux tables maxm solutions cache elems flags =
1453     match auto_main tables maxm context flags elems universe cache with
1454     | Fail s,tables,cache,maxm ->debug_print s; solutions,cache,maxm
1455     | Success (_,metasenv,subst,others),tables,cache,maxm ->
1456         if Unix.gettimeofday () > flags.timeout then
1457           ((subst,metasenv)::solutions), cache, maxm
1458         else
1459           aux tables maxm ((subst,metasenv)::solutions) cache others flags
1460   in
1461   let rc = aux tables maxm [] cache elems flags in
1462     match rc with
1463     | [],cache,maxm -> [],cache,maxm
1464     | solutions,cache,maxm ->
1465         let solutions =
1466           HExtlib.filter_map
1467             (fun (subst,newmetasenv) ->
1468               let opened =
1469                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1470               in
1471               if opened = [] then Some subst else None)
1472             solutions
1473         in
1474          solutions,cache,maxm
1475 ;;
1476 *)
1477 let
1478   auto_all_solutions maxm tables universe cache context metasenv gl flags
1479 =
1480   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1481   let goals =
1482     List.map
1483       (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1484   in
1485   let elems = [metasenv,[],1,goals,[]] in
1486   let rec aux tables maxm solutions cache elems flags =
1487     match auto_main tables maxm context flags universe cache elems with
1488     | Gaveup (tables,cache,maxm) ->
1489         solutions,cache,maxm
1490     | Proved (metasenv,subst,others,tables,cache,maxm) ->
1491         if Unix.gettimeofday () > flags.timeout then
1492           ((subst,metasenv)::solutions), cache, maxm
1493         else
1494           aux tables maxm ((subst,metasenv)::solutions) cache others flags
1495   in
1496   let rc = aux tables maxm [] cache elems flags in
1497     match rc with
1498     | [],cache,maxm -> [],cache,maxm
1499     | solutions,cache,maxm ->
1500         let solutions =
1501           HExtlib.filter_map
1502             (fun (subst,newmetasenv) ->
1503               let opened =
1504                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1505               in
1506               if opened = [] then Some subst else None)
1507             solutions
1508         in
1509          solutions,cache,maxm
1510 ;;
1511
1512 (* }}} ****************** AUTO ***************)
1513
1514 (* script generation for applicative proofs
1515 let cic2grafite context menv t =
1516   let module PT = CicNotationPt in
1517   let module GA = GrafiteAst in
1518   let pp_t context t =
1519     let names = Utils.names_of_context context in
1520     CicPp.pp t names
1521   in
1522   let sort_of context t =
1523     let ty,_ =
1524       CicTypeChecker.type_of_aux' menv context t
1525         CicUniv.oblivion_ugraph
1526     in
1527     let sort,_ = CicTypeChecker.type_of_aux' menv context ty
1528         CicUniv.oblivion_ugraph
1529     in
1530     match sort with
1531     | Cic.Sort Cic.Prop -> P
1532     | _ -> T
1533   in
1534   let floc = HExtlib.dummy_floc in
1535   let rec print_term c = function
1536     | Cic.Rel _
1537     | Cic.MutConstruct _
1538     | Cic.MutInd _
1539     | Cic.Const _ as t ->
1540         PT.Ident (pp_t c t, None)
1541     | Cic.Appl l -> PT.Appl (List.map (print_term c) l)
1542     | Cic.Implicit _ -> PT.Implicit
1543     | Cic.Lambda (Cic.Name n, s, t) ->
1544         PT.Binder (`Lambda, (PT.Ident (n,None), Some (print_term c s)),
1545           print_term (Some (Cic.Name n, Cic.Decl s)::c) t)
1546     | Cic.Prod (Cic.Name n, s, t) ->
1547         PT.Binder (`Forall, (PT.Ident (n,None), Some (print_term c s)),
1548           print_term (Some (Cic.Name n, Cic.Decl s)::c) t)
1549     | Cic.LetIn (Cic.Name n, s, t) ->
1550         PT.Binder (`Lambda, (PT.Ident (n,None), Some (print_term c s)),
1551           print_term (Some (Cic.Name n, Cic.Def (s,None))::c) t)
1552     | Cic.Meta _ -> PT.Implicit
1553     | _ as t ->
1554         PT.Ident ("ERROR"^CicPp.ppterm t, None)
1555     (*
1556         debug_print (lazy (CicPp.ppterm t));
1557         assert false
1558         *)
1559   in
1560   let rec print_proof context = function
1561     | Cic.Rel _
1562     | Cic.Const _ as t ->
1563         [GA.Executable (floc,
1564           GA.Tactic (floc,
1565           Some (GA.Apply (floc, print_term context t)), GA.Dot floc))]
1566     | Cic.Appl (he::tl) ->
1567         let tl = List.map (fun t -> t, sort_of context t) tl in
1568         let subgoals =
1569           HExtlib.filter_map (function (t,P) -> Some t | _ -> None) tl
1570         in
1571         let args =
1572             List.map
1573               (function
1574                 | (t,P) -> Cic.Implicit None
1575                 | (t,_) -> t)
1576               tl
1577         in
1578         if List.length subgoals > 1 then
1579           (* branch *)
1580           [GA.Executable (floc,
1581             GA.Tactic (floc,
1582               Some (GA.Apply (floc, print_term context (Cic.Appl (he::args)))),
1583               GA.Semicolon floc))] @
1584           [GA.Executable (floc, GA.Tactic (floc, None, GA.Branch floc))] @
1585           (HExtlib.list_concat
1586           ~sep:[GA.Executable (floc, GA.Tactic (floc, None,GA.Shift floc))]
1587             (List.map (print_proof context) subgoals)) @
1588           [GA.Executable (floc, GA.Tactic (floc, None,GA.Merge floc))]
1589         else
1590           (* simple apply *)
1591           [GA.Executable (floc,
1592             GA.Tactic (floc,
1593             Some (GA.Apply
1594               (floc, print_term context (Cic.Appl (he::args)) )), GA.Dot floc))]
1595           @
1596           (match subgoals with
1597           | [] -> []
1598           | [x] -> print_proof context x
1599           | _ -> assert false)
1600     | _ -> []
1601     (*
1602         debug_print (lazy (CicPp.ppterm t));
1603         assert false
1604         *)
1605   in
1606   let ast = print_proof context t in
1607   let pp t =
1608     (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
1609      * which will show up using the following command line:
1610      * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
1611     let width = max_int in
1612     let term_pp content_term =
1613       let pres_term = TermContentPres.pp_ast content_term in
1614       let dummy_tbl = Hashtbl.create 1 in
1615       let markup = CicNotationPres.render dummy_tbl pres_term in
1616       let s = "(" ^ BoxPp.render_to_string List.hd width markup ^ ")" in
1617       Pcre.substitute
1618         ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
1619     in
1620     CicNotationPp.set_pp_term term_pp;
1621     let lazy_term_pp = fun x -> assert false in
1622     let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
1623     GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t
1624   in
1625   String.concat "\n" (List.map pp ast)
1626 ;;
1627 let auto_all tables universe cache context metasenv gl flags =
1628   let solutions, cache, _ =
1629     auto_all_solutions 0 tables universe cache context metasenv gl flags
1630   in
1631   solutions, cache
1632 ;;
1633 *)
1634
1635 let auto flags metasenv tables universe cache context metasenv gl =
1636   let initial_time = Unix.gettimeofday() in
1637   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1638   let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1639   let elems = [metasenv,[],1,goals,[]] in
1640   match auto_main tables 0 context flags universe cache elems with
1641   | Proved (metasenv,subst,_, tables,cache,_) ->
1642       debug_print(lazy
1643         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1644       Some (subst,metasenv), cache
1645   | Gaveup (tables,cache,maxm) ->
1646       debug_print(lazy
1647         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1648       None,cache
1649 ;;
1650
1651 let bool params name default =
1652     try
1653       let s = List.assoc name params in
1654       if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
1655       else if s = "0" || s = "false" || s = "no" || s= "off" then false
1656       else
1657         let msg = "Unrecognized value for parameter "^name^"\n" in
1658         let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
1659         raise (ProofEngineTypes.Fail (lazy msg))
1660     with Not_found -> default
1661 ;;
1662
1663 let string params name default =
1664     try List.assoc name params with
1665     | Not_found -> default
1666 ;;
1667
1668 let int params name default =
1669     try int_of_string (List.assoc name params) with
1670     | Not_found -> default
1671     | Failure _ ->
1672         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
1673 ;;
1674
1675 let flags_of_params params ?(for_applyS=false) () =
1676  let int = int params in
1677  let bool = bool params in
1678  let close_more = bool "close_more" false in
1679  let use_paramod = bool "use_paramod" true in
1680  let use_only_paramod =
1681   if for_applyS then true else bool "paramodulation" false in
1682  let use_library = bool "library"
1683    ((AutoTypes.default_flags()).AutoTypes.use_library) in
1684  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
1685  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
1686  let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
1687  let timeout = int "timeout" 0 in
1688   { AutoTypes.maxdepth =
1689       if use_only_paramod then 2 else depth;
1690     AutoTypes.maxwidth = width;
1691     AutoTypes.maxsize = size;
1692     AutoTypes.timeout =
1693       if timeout = 0 then
1694        if for_applyS then Unix.gettimeofday () +. 30.0
1695        else
1696          infinity
1697       else
1698        Unix.gettimeofday() +. (float_of_int timeout);
1699     AutoTypes.use_library = use_library;
1700     AutoTypes.use_paramod = use_paramod;
1701     AutoTypes.use_only_paramod = use_only_paramod;
1702     AutoTypes.close_more = close_more;
1703     AutoTypes.dont_cache_failures = false;
1704   }
1705
1706 let applyS_tac ~dbd ~term ~params ~universe =
1707  ProofEngineTypes.mk_tactic
1708   (fun status ->
1709     try
1710       let _, proof, gl,_,_ =
1711        apply_smart ~dbd ~term ~subst:[] ~universe
1712         (flags_of_params params ~for_applyS:true ()) status
1713       in
1714        proof, gl
1715     with
1716     | CicUnification.UnificationFailure msg
1717     | CicTypeChecker.TypeCheckerFailure msg ->
1718         raise (ProofEngineTypes.Fail msg))
1719
1720 (* SUPERPOSITION *)
1721
1722 (* Syntax:
1723  *   auto superposition target = NAME
1724  *     [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
1725  *
1726  *  - if table is omitted no superposition will be performed
1727  *  - if demod_table is omitted no demodulation will be prformed
1728  *  - subterms_only is passed to Indexing.superposition_right
1729  *
1730  *  lists are coded using _ (example: H_H1_H2)
1731  *)
1732
1733 let eq_and_ty_of_goal = function
1734   | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1735       uri,t
1736   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1737 ;;
1738
1739 let rec find_in_ctx i name = function
1740   | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
1741   | Some (Cic.Name name', _)::tl when name = name' -> i
1742   | _::tl -> find_in_ctx (i+1) name tl
1743 ;;
1744
1745 let rec position_of i x = function
1746   | [] -> assert false
1747   | j::tl when j <> x -> position_of (i+1) x tl
1748   | _ -> i
1749 ;;
1750
1751
1752 let superposition_tac ~target ~table ~subterms_only ~demod_table status =
1753   Saturation.reset_refs();
1754   let proof,goalno = status in
1755   let curi,metasenv,pbo,pty, attrs = proof in
1756   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
1757   let eq_uri,tty = eq_and_ty_of_goal ty in
1758   let env = (metasenv, context, CicUniv.empty_ugraph) in
1759   let names = Utils.names_of_context context in
1760   let bag = Equality.mk_equality_bag () in
1761   let eq_index, equalities, maxm,cache  =
1762     find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
1763   in
1764   let eq_what =
1765     let what = find_in_ctx 1 target context in
1766     List.nth equalities (position_of 0 what eq_index)
1767   in
1768   let eq_other =
1769     if table <> "" then
1770       let other =
1771         let others = Str.split (Str.regexp "_") table in
1772         List.map (fun other -> find_in_ctx 1 other context) others
1773       in
1774       List.map
1775         (fun other -> List.nth equalities (position_of 0 other eq_index))
1776         other
1777     else
1778       []
1779   in
1780   let index = List.fold_left Indexing.index Indexing.empty eq_other in
1781   let maxm, eql =
1782     if table = "" then maxm,[eq_what] else
1783     Indexing.superposition_right bag
1784       ~subterms_only eq_uri maxm env index eq_what
1785   in
1786   debug_print (lazy ("Superposition right:"));
1787   debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env));
1788   debug_print (lazy ("\n table: "));
1789   List.iter
1790     (fun e ->
1791        debug_print (lazy ("  " ^ Equality.string_of_equality e ~env))) eq_other;
1792   debug_print (lazy ("\n result: "));
1793   List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1794   debug_print (lazy ("\n result (cut&paste): "));
1795   List.iter
1796     (fun e ->
1797       let t = Equality.term_of_equality eq_uri e in
1798       debug_print (lazy (CicPp.pp t names)))
1799   eql;
1800   debug_print (lazy ("\n result proofs: "));
1801   List.iter (fun e ->
1802     debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in
1803     let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
1804     Subst.ppsubst s ^ "\n" ^
1805     CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql;
1806   if demod_table <> "" then
1807     begin
1808       let eql =
1809         if eql = [] then [eq_what] else eql
1810       in
1811       let demod =
1812         let demod = Str.split (Str.regexp "_") demod_table in
1813         List.map (fun other -> find_in_ctx 1 other context) demod
1814       in
1815       let eq_demod =
1816         List.map
1817           (fun demod -> List.nth equalities (position_of 0 demod eq_index))
1818           demod
1819       in
1820       let table = List.fold_left Indexing.index Indexing.empty eq_demod in
1821       let maxm,eql =
1822         List.fold_left
1823           (fun (maxm,acc) e ->
1824             let maxm,eq =
1825               Indexing.demodulation_equality bag eq_uri maxm env table e
1826             in
1827             maxm,eq::acc)
1828           (maxm,[]) eql
1829       in
1830       let eql = List.rev eql in
1831       debug_print (lazy ("\n result [demod]: "));
1832       List.iter
1833         (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
1834       debug_print (lazy ("\n result [demod] (cut&paste): "));
1835       List.iter
1836         (fun e ->
1837           let t = Equality.term_of_equality eq_uri e in
1838           debug_print (lazy (CicPp.pp t names)))
1839       eql;
1840     end;
1841   proof,[goalno]
1842 ;;
1843
1844 let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
1845   (* argument parsing *)
1846   let string = string params in
1847   let bool = bool params in
1848   (* hacks to debug paramod *)
1849   let superposition = bool "superposition" false in
1850   let target = string "target" "" in
1851   let table = string "table" "" in
1852   let subterms_only = bool "subterms_only" false in
1853   let demod_table = string "demod_table" "" in
1854   match superposition with
1855   | true ->
1856       (* this is the ugly hack to debug paramod *)
1857       superposition_tac
1858         ~target ~table ~subterms_only ~demod_table (proof,goal)
1859   | false ->
1860       (* this is the real auto *)
1861       let _,metasenv,_,_, _ = proof in
1862       let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1863       let flags = flags_of_params params () in
1864       (* just for testing *)
1865       let use_library = flags.use_library in
1866       let tables,cache,newmeta =
1867         init_cache_and_tables dbd use_library flags.use_only_paramod
1868           universe (proof, goal) in
1869       let tables,cache,newmeta =
1870         if flags.close_more then
1871           close_more
1872             tables newmeta context (proof, goal)
1873               auto_all_solutions universe cache
1874         else tables,cache,newmeta in
1875       let initial_time = Unix.gettimeofday() in
1876       let (_,oldmetasenv,_,_, _) = proof in
1877       hint := None;
1878       let elem =
1879         metasenv,[],1,[D (goal,flags.maxdepth,P)],[]
1880       in
1881       match auto_main tables newmeta context flags universe cache [elem] with
1882         | Proved (metasenv,subst,_, tables,cache,_) ->
1883             prerr_endline
1884               ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
1885             (* script generation
1886             let irl = mk_irl context in
1887             let goal_term = Cic.Meta(goal, irl) in
1888             let proof_term = CicMetaSubst.apply_subst subst goal_term in
1889             HLog.debug (cic2grafite context metasenv proof_term);
1890             *)
1891             let proof,metasenv =
1892             ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1893               proof goal (CicMetaSubst.apply_subst subst) metasenv
1894             in
1895             let opened =
1896               ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1897                 ~newmetasenv:metasenv
1898             in
1899               proof,opened
1900         | Gaveup (tables,cache,maxm) ->
1901             debug_print
1902               (lazy ("TIME:"^
1903                 string_of_float(Unix.gettimeofday()-.initial_time)));
1904             raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1905 ;;
1906
1907 let auto_tac ~dbd ~params ~universe =
1908   ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
1909
1910 let eq_of_goal = function
1911   | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1912       uri
1913   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1914 ;;
1915
1916 (* DEMODULATE *)
1917 let demodulate_tac ~dbd ~universe (proof,goal)=
1918   let curi,metasenv,pbo,pty, attrs = proof in
1919   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1920   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1921   let initgoal = [], [], ty in
1922   let eq_uri = eq_of_goal ty in
1923   let (active,passive,bag), cache, maxm =
1924      init_cache_and_tables dbd false true universe (proof,goal) in
1925   let equalities = (Saturation.list_of_passive passive) in
1926   (* we demodulate using both actives passives *)
1927   let table =
1928     List.fold_left
1929       (fun tbl eq -> Indexing.index tbl eq)
1930       (snd active) equalities
1931   in
1932   let changed,(newproof,newmetasenv, newty) =
1933     Indexing.demodulation_goal bag
1934       (metasenv,context,CicUniv.empty_ugraph) table initgoal
1935   in
1936   if changed then
1937     begin
1938       let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
1939       let proofterm,_ =
1940         Equality.build_goal_proof bag
1941           eq_uri newproof opengoal ty [] context metasenv
1942       in
1943         let extended_metasenv = (maxm,context,newty)::metasenv in
1944         let extended_status =
1945           (curi,extended_metasenv,pbo,pty, attrs),goal in
1946         let (status,newgoals) =
1947           ProofEngineTypes.apply_tactic
1948             (PrimitiveTactics.apply_tac ~term:proofterm)
1949             extended_status in
1950         (status,maxm::newgoals)
1951     end
1952   else (* if newty = ty then *)
1953     raise (ProofEngineTypes.Fail (lazy "no progress"))
1954   (*else ProofEngineTypes.apply_tactic
1955     (ReductionTactics.simpl_tac
1956       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
1957 ;;
1958
1959 let demodulate_tac ~dbd ~universe =
1960   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
1961