matitaB/components/ng_tactics/nnAuto.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 open Printf
  13
  14 let print ?(depth=0) s =
  15   prerr_endline (String.make (2*depth) ' '^Lazy.force s)
  16 let noprint ?(depth=0) _ = ()
  17 let debug_print = noprint
  18
  19 open Continuationals.Stack
  20 open NTacStatus
  21 module Ast = NotationPt
  22
  23 (* ======================= statistics  ========================= *)
  24
  25 let app_counter = ref 0
  26
  27 module RHT = struct
  28   type t = NReference.reference
  29   let equal = (==)
  30   let compare = Pervasives.compare
  31   let hash = Hashtbl.hash
  32 end;;
  33
  34 module RefHash = Hashtbl.Make(RHT);;
  35
  36 type info = {
  37   nominations : int ref;
  38   uses: int ref;
  39 }
  40
  41 let statistics: info RefHash.t = RefHash.create 503
  42
  43 let incr_nominations tbl item =
  44   try
  45     let v = RefHash.find tbl item in incr v.nominations
  46   with Not_found ->
  47     RefHash.add tbl item {nominations = ref 1; uses = ref 0}
  48
  49 let incr_uses tbl item =
  50   try
  51     let v = RefHash.find tbl item in incr v.uses
  52   with Not_found -> assert false
  53
  54 let toref f tbl t =
  55   match t with
  56     | Ast.NRef n ->
  57         f tbl n
  58     | Ast.NCic _  (* local candidate *)
  59     | _  ->  ()
  60
  61 let is_relevant tbl item =
  62   try
  63     let v = RefHash.find tbl item in
  64       if !(v.nominations) < 60 then true (* not enough info *)
  65       else if !(v.uses) = 0 then false
  66       else true
  67   with Not_found -> true
  68
  69 let print_stat status tbl =
  70   let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
  71   let relevance v = float !(v.uses) /. float !(v.nominations) in
  72   let vcompare (_,v1) (_,v2) =
  73     Pervasives.compare (relevance v1) (relevance v2) in
  74   let l = List.sort vcompare l in
  75   let short_name r =
  76     Filename.chop_extension
  77       (Filename.basename (NReference.string_of_reference r))
  78   in
  79   let vstring (a,v)=
  80       short_name a ^ ": rel = " ^
  81       (string_of_float (relevance v)) ^
  82       "; uses = " ^ (string_of_int !(v.uses)) ^
  83       "; nom = " ^ (string_of_int !(v.nominations)) in
  84   lazy ("\n\nSTATISTICS:\n" ^
  85           String.concat "\n" (List.map vstring l))
  86
  87 (* ======================= utility functions ========================= *)
  88 module IntSet = Set.Make(struct type t = int let compare = compare end)
  89
  90 let get_sgoalty status g =
  91  let _,_,metasenv,subst,_ = status#obj in
  92  try
  93    let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
  94    let ty = NCicUntrusted.apply_subst status subst ctx ty in
  95    let ctx = NCicUntrusted.apply_subst_context status
  96      ~fix_projections:true subst ctx
  97    in
  98      NTacStatus.mk_cic_term ctx ty
  99  with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
 100 ;;
 101
 102 let deps status g =
 103   let gty = get_sgoalty status g in
 104   metas_of_term status gty
 105 ;;
 106
 107 let menv_closure status gl =
 108   let rec closure acc = function
 109     | [] -> acc
 110     | x::l when IntSet.mem x acc -> closure acc l
 111     | x::l -> closure (IntSet.add x acc) (deps status x @ l)
 112   in closure IntSet.empty gl
 113 ;;
 114
 115 (* we call a "fact" an object whose hypothesis occur in the goal
 116    or in types of goal-variables *)
 117 let branch status ty =
 118   let status, ty, metas = saturate ~delta:0 status ty in
 119   noprint (lazy ("saturated ty :" ^ (ppterm status ty)));
 120   let g_metas = metas_of_term status ty in
 121   let clos = menv_closure status g_metas in
 122   (* let _,_,metasenv,_,_ = status#obj in *)
 123   let menv =
 124     List.fold_left
 125       (fun acc m ->
 126          let _, m = term_of_cic_term status m (ctx_of m) in
 127          match m with
 128          | NCic.Meta(i,_) -> IntSet.add i acc
 129          | _ -> assert false)
 130       IntSet.empty metas
 131   in
 132   (* IntSet.subset menv clos *)
 133   IntSet.cardinal(IntSet.diff menv clos)
 134
 135 let is_a_fact status ty = branch status ty = 0
 136
 137 let is_a_fact_obj s uri =
 138   let obj = NCicEnvironment.get_checked_obj s uri in
 139   match obj with
 140     | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) ->
 141         is_a_fact s (mk_cic_term [] ty)
 142 (* aggiungere i costruttori *)
 143     | _ -> false
 144
 145 let is_a_fact_ast status subst metasenv ctx cand =
 146  debug_print ~depth:0
 147    (lazy ("------- checking " ^ NotationPp.pp_term status cand));
 148  let status, t = disambiguate status ctx ("",0,cand) None in
 149  let status,t = term_of_cic_term status t ctx in
 150  let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
 151    is_a_fact status (mk_cic_term ctx ty)
 152
 153 let current_goal ?(single_goal=true) status =
 154   let open_goals = head_goals status#stack in
 155   if single_goal
 156      then assert (List.length open_goals  = 1)
 157      else assert (List.length open_goals >= 1);
 158   let open_goal = List.hd open_goals in
 159   let gty = get_goalty status open_goal in
 160   let ctx = ctx_of gty in
 161     open_goal, ctx, gty
 162
 163 let height_of_ref status (NReference.Ref (uri, x)) =
 164   match x with
 165   | NReference.Decl
 166   | NReference.Ind _
 167   | NReference.Con _
 168   | NReference.CoFix _ ->
 169       let _,height,_,_,_ = NCicEnvironment.get_checked_obj status uri in
 170       height
 171   | NReference.Def h -> h
 172   | NReference.Fix (_,_,h) -> h
 173 ;;
 174
 175 (*************************** height functions ********************************)
 176 let fast_height_of_term status t =
 177  let h = ref 0 in
 178  let rec aux =
 179   function
 180      NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
 181    | NCic.Meta _ -> ()
 182    | NCic.Rel _
 183    | NCic.Sort _ -> ()
 184    | NCic.Implicit _ -> assert false
 185    | NCic.Const nref ->
 186 (*
 187                    prerr_endline (status#ppterm ~metasenv:[] ~subst:[]
 188                    ~context:[] t ^ ":" ^ string_of_int (height_of_ref status nref));
 189 *)
 190        h := max !h (height_of_ref status nref)
 191    | NCic.Prod (_,t1,t2)
 192    | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
 193    | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
 194    | NCic.Appl l -> List.iter aux l
 195    | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
 196  in
 197   aux t; !h
 198 ;;
 199
 200 let height_of_goal g status =
 201   let ty = get_goalty status g in
 202   let context = ctx_of ty in
 203   let _, ty = term_of_cic_term status ty (ctx_of ty) in
 204   let h = ref (fast_height_of_term status ty) in
 205   List.iter
 206     (function
 207        | _, NCic.Decl ty -> h := max !h (fast_height_of_term status ty)
 208        | _, NCic.Def (bo,ty) ->
 209            h := max !h (fast_height_of_term status ty);
 210            h := max !h (fast_height_of_term status bo);
 211     )
 212     context;
 213   !h
 214 ;;
 215
 216 let height_of_goals status =
 217   let open_goals = head_goals status#stack in
 218   assert (List.length open_goals > 0);
 219   let h = ref 1 in
 220   List.iter
 221     (fun open_goal ->
 222        h := max !h (height_of_goal open_goal status))
 223      open_goals;
 224   noprint (lazy ("altezza sequente: " ^ string_of_int !h));
 225   !h
 226 ;;
 227
 228 (* =============================== paramod =========================== *)
 229 let solve f status eq_cache goal =
 230 (*
 231   let f =
 232     if fast then NCicParamod.fast_eq_check
 233     else NCicParamod.paramod in
 234 *)
 235   let n,h,metasenv,subst,o = status#obj in
 236   let gname, ctx, gty = List.assoc goal metasenv in
 237   let gty = NCicUntrusted.apply_subst status subst ctx gty in
 238   let build_status (pt, _, metasenv, subst) =
 239     try
 240       noprint (lazy ("refining: "^(status#ppterm ctx subst metasenv pt)));
 241       let stamp = Unix.gettimeofday () in
 242       let metasenv, subst, pt, pty =
 243         (* NCicRefiner.typeof status
 244           (* (status#set_coerc_db NCicCoercion.empty_db) *)
 245           metasenv subst ctx pt None in
 246           debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt)));
 247           noprint (lazy ("synt: "^(status#ppterm ctx subst metasenv pty)));
 248           let metasenv, subst =
 249             NCicUnification.unify status metasenv subst ctx gty pty *)
 250         NCicRefiner.typeof
 251           (status#set_coerc_db NCicCoercion.empty_db)
 252           metasenv subst ctx pt (Some gty)
 253         in
 254           noprint (lazy (Printf.sprintf "Refined in %fs"
 255                      (Unix.gettimeofday() -. stamp)));
 256           let status = status#set_obj (n,h,metasenv,subst,o) in
 257           let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
 258           let subst = (goal,(gname,ctx,pt,pty)) :: subst in
 259             Some (status#set_obj (n,h,metasenv,subst,o))
 260     with
 261         NCicRefiner.RefineFailure msg
 262       | NCicRefiner.Uncertain msg ->
 263           debug_print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
 264                         snd (Lazy.force msg) ^
 265                         "\n in the environment\n" ^
 266                         status#ppmetasenv subst metasenv)); None
 267       | NCicRefiner.AssertFailure msg ->
 268           debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
 269                         Lazy.force msg ^
 270                         "\n in the environment\n" ^
 271                         status#ppmetasenv subst metasenv)); None
 272       | _ -> None
 273     in
 274     HExtlib.filter_map build_status
 275       (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
 276 ;;
 277
 278 let fast_eq_check eq_cache status (goal:int) =
 279   match solve NCicParamod.fast_eq_check status eq_cache goal with
 280   | [] -> raise (Error (lazy "no proof found",None))
 281   | s::_ -> s
 282 ;;
 283
 284 let dist_fast_eq_check eq_cache s =
 285   NTactics.distribute_tac (fast_eq_check eq_cache) s
 286 ;;
 287
 288 let auto_eq_check eq_cache status =
 289   try
 290     let s = dist_fast_eq_check eq_cache status in
 291       [s]
 292   with
 293     | Error _ -> debug_print (lazy ("no paramod proof found"));[]
 294 ;;
 295
 296 let index_local_equations eq_cache status =
 297   noprint (lazy "indexing equations");
 298   let open_goals = head_goals status#stack in
 299   let open_goal = List.hd open_goals in
 300   let ngty = get_goalty status open_goal in
 301   let _,_,metasenv,subst,_ = status#obj in
 302   let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
 303   let c = ref 0 in
 304   List.fold_left
 305     (fun eq_cache _ ->
 306        c:= !c+1;
 307        let t = NCic.Rel !c in
 308          try
 309            let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
 310            if is_a_fact status (mk_cic_term ctx ty) then
 311              (noprint(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
 312               NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
 313            else
 314              (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
 315               eq_cache)
 316          with
 317            | NCicTypeChecker.TypeCheckerFailure _
 318            | NCicTypeChecker.AssertFailure _ -> eq_cache)
 319     eq_cache ctx
 320 ;;
 321
 322 let fast_eq_check_tac ~params s =
 323   let unit_eq = index_local_equations s#eq_cache s in
 324   dist_fast_eq_check unit_eq s
 325 ;;
 326
 327 let paramod eq_cache status goal =
 328   match solve NCicParamod.paramod status eq_cache goal with
 329   | [] -> raise (Error (lazy "no proof found",None))
 330   | s::_ -> s
 331 ;;
 332
 333 let paramod_tac ~params s =
 334   let unit_eq = index_local_equations s#eq_cache s in
 335   NTactics.distribute_tac (paramod unit_eq) s
 336 ;;
 337
 338 let demod eq_cache status goal =
 339   match solve NCicParamod.demod status eq_cache goal with
 340   | [] -> raise (Error (lazy "no progress",None))
 341   | s::_ -> s
 342 ;;
 343
 344 let demod_tac ~params s =
 345   let unit_eq = index_local_equations s#eq_cache s in
 346   NTactics.distribute_tac (demod unit_eq) s
 347 ;;
 348
 349 (*
 350 let fast_eq_check_tac_all  ~params eq_cache status =
 351   let g,_,_ = current_goal status in
 352   let allstates = fast_eq_check_all status eq_cache g in
 353   let pseudo_low_tac s _ _ = s in
 354   let pseudo_low_tactics =
 355     List.map pseudo_low_tac allstates
 356   in
 357     List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
 358 ;;
 359 *)
 360
 361 (*
 362 let demod status eq_cache goal =
 363   let n,h,metasenv,subst,o = status#obj in
 364   let gname, ctx, gty = List.assoc goal metasenv in
 365   let gty = NCicUntrusted.apply_subst subst ctx gty in
 366
 367 let demod_tac ~params s =
 368   let unit_eq = index_local_equations s#eq_cache s in
 369   dist_fast_eq_check unit_eq s
 370 *)
 371
 372 (*************** subsumption ****************)
 373
 374 let close_wrt_context status =
 375   List.fold_left
 376     (fun ty ctx_entry ->
 377         match ctx_entry with
 378        | name, NCic.Decl t -> NCic.Prod(name,t,ty)
 379        | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
 380 ;;
 381
 382 let args_for_context ?(k=1) ctx =
 383   let _,args =
 384     List.fold_left
 385       (fun (n,l) ctx_entry ->
 386          match ctx_entry with
 387            | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
 388            | name, NCic.Def(bo, _) -> n+1,l)
 389       (k,[]) ctx in
 390     args
 391
 392 let constant_for_meta status ctx ty i =
 393   let name = "cic:/foo"^(string_of_int i)^".con" in
 394   let uri = NUri.uri_of_string name in
 395   let ty = close_wrt_context status ty ctx in
 396   (* prerr_endline (status#ppterm [] [] [] ty); *)
 397   let attr = (`Generated,`Definition,`Local) in
 398   let obj = NCic.Constant([],name,None,ty,attr) in
 399     (* Constant  of relevance * string * term option * term * c_attr *)
 400     (uri,0,[],[],obj)
 401
 402 (* not used *)
 403 let refresh metasenv =
 404   List.fold_left
 405     (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
 406        let ikind = NCicUntrusted.kind_of_meta iattr in
 407        let metasenv,j,instance,ty =
 408          NCicMetaSubst.mk_meta ~attrs:iattr
 409            metasenv ctx ~with_type:ty ikind in
 410        let s_entry = i,(iattr, ctx, instance, ty) in
 411        let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
 412          metasenv,s_entry::subst)
 413       (metasenv,[]) metasenv
 414
 415 (* close metasenv returns a ground instance of all the metas in the
 416 metasenv, insantiatied with axioms, and the list of these axioms *)
 417 let close_metasenv status metasenv subst =
 418   (*
 419   let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
 420   *)
 421   let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in
 422     List.fold_left
 423       (fun (subst,objs) (i,(iattr,ctx,ty)) ->
 424          let ty = NCicUntrusted.apply_subst status subst ctx ty in
 425          let ctx =
 426            NCicUntrusted.apply_subst_context status ~fix_projections:true
 427              subst ctx in
 428          let (uri,_,_,_,obj) as okind =
 429            constant_for_meta status ctx ty i in
 430          try
 431            NCicEnvironment.check_and_add_obj status okind;
 432            let iref = NReference.reference_of_spec uri NReference.Decl in
 433            let iterm =
 434              let args = args_for_context ctx in
 435                if args = [] then NCic.Const iref
 436                else NCic.Appl(NCic.Const iref::args)
 437            in
 438            (* prerr_endline (status#ppterm ctx [] [] iterm); *)
 439            let s_entry = i, ([], ctx, iterm, ty)
 440            in s_entry::subst,okind::objs
 441          with _ -> assert false)
 442       (subst,[]) metasenv
 443 ;;
 444
 445 let ground_instances status gl =
 446   let _,_,metasenv,subst,_ = status#obj in
 447   let subset = menv_closure status gl in
 448   let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
 449 (*
 450   let submenv = metasenv in
 451 *)
 452   let subst, objs = close_metasenv status submenv subst in
 453   try
 454     List.iter
 455       (fun i ->
 456          let (_, ctx, t, _) = List.assoc i subst in
 457            noprint (lazy (status#ppterm ctx [] [] t));
 458            List.iter
 459              (fun (uri,_,_,_,_) as obj ->
 460                 NCicEnvironment.invalidate_item status (`Obj (uri, obj)))
 461              objs;
 462            ())
 463       gl
 464   with
 465       Not_found -> assert false
 466   (* (ctx,t) *)
 467 ;;
 468
 469 let replace_meta status i args target =
 470   let rec aux k = function
 471     (* TODO: local context *)
 472     | NCic.Meta (j,lc) when i = j ->
 473         (match args with
 474            | [] -> NCic.Rel 1
 475            | _ -> let args =
 476                List.map (NCicSubstitution.subst_meta status lc) args in
 477                NCic.Appl(NCic.Rel k::args))
 478     | NCic.Meta (j,lc) as m ->
 479         (match lc with
 480            _,NCic.Irl _ -> m
 481          | n,NCic.Ctx l ->
 482             NCic.Meta
 483              (i,(0,NCic.Ctx
 484                  (List.map (fun t ->
 485                    aux k (NCicSubstitution.lift status n t)) l))))
 486     | t -> NCicUtils.map status (fun _ k -> k+1) k aux t
 487  in
 488    aux 1 target
 489 ;;
 490
 491 let close_wrt_metasenv status subst =
 492   List.fold_left
 493     (fun ty (i,(iattr,ctx,mty)) ->
 494        let mty = NCicUntrusted.apply_subst status subst ctx mty in
 495        let ctx =
 496          NCicUntrusted.apply_subst_context status ~fix_projections:true
 497            subst ctx in
 498        let cty = close_wrt_context status mty ctx in
 499        let name = "foo"^(string_of_int i) in
 500        let ty = NCicSubstitution.lift status 1 ty in
 501        let args = args_for_context ~k:1 ctx in
 502          (* prerr_endline (status#ppterm ctx [] [] iterm); *)
 503        let ty = replace_meta status i args ty
 504        in
 505        NCic.Prod(name,cty,ty))
 506 ;;
 507
 508 let close status g =
 509   let _,_,metasenv,subst,_ = status#obj in
 510   let subset = menv_closure status [g] in
 511   let subset = IntSet.remove g subset in
 512   let elems = IntSet.elements subset in
 513   let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
 514   let ty = NCicUntrusted.apply_subst status subst ctx ty in
 515   noprint (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty)));
 516   noprint (lazy (String.concat ", " (List.map string_of_int elems)));
 517   let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
 518   let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in
 519 (*
 520     let submenv = metasenv in
 521 *)
 522   let ty = close_wrt_metasenv status subst ty submenv in
 523     noprint (lazy (status#ppterm ctx [] [] ty));
 524     ctx,ty
 525 ;;
 526
 527 (****************** smart application ********************)
 528
 529 let saturate_to_ref status metasenv subst ctx nref ty =
 530   let height = height_of_ref status nref in
 531   let rec aux metasenv ty args =
 532     let ty,metasenv,moreargs =
 533       NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in
 534     match ty with
 535       | NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
 536           when nre<>nref ->
 537           let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
 538             aux metasenv bo (args@moreargs)
 539       | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
 540           when nre<>nref ->
 541           let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
 542             aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
 543     | _ -> ty,metasenv,(args@moreargs)
 544   in
 545     aux metasenv ty []
 546
 547 let smart_apply t unit_eq status g =
 548   let n,h,metasenv,subst,o = status#obj in
 549   let gname, ctx, gty = List.assoc g metasenv in
 550   (* let ggty = mk_cic_term context gty in *)
 551   let status, t = disambiguate status ctx t None in
 552   let status,t = term_of_cic_term status t ctx in
 553   let _,_,metasenv,subst,_ = status#obj in
 554   let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
 555   let ty,metasenv,args =
 556     match gty with
 557       | NCic.Const(nref)
 558       | NCic.Appl(NCic.Const(nref)::_) ->
 559           saturate_to_ref status metasenv subst ctx nref ty
 560       | _ ->
 561           NCicMetaSubst.saturate status metasenv subst ctx ty 0 in
 562   let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
 563   let status = status#set_obj (n,h,metasenv,subst,o) in
 564   let pterm = if args=[] then t else
 565     match t with
 566       | NCic.Appl l -> NCic.Appl(l@args)
 567       | _ -> NCic.Appl(t::args)
 568   in
 569   noprint(lazy("pterm " ^ (status#ppterm ctx [] [] pterm)));
 570   noprint(lazy("pty " ^ (status#ppterm ctx [] [] ty)));
 571   let eq_coerc =
 572     let uri =
 573       NUri.uri_of_string "cic:/matita/basics/logic/eq_coerc.con" in
 574     let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
 575       NCic.Const ref
 576   in
 577   let smart =
 578     NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
 579   let smart = mk_cic_term ctx smart in
 580     try
 581       let status = instantiate status g smart in
 582       let _,_,metasenv,subst,_ = status#obj in
 583       let _,ctx,jty = List.assoc j metasenv in
 584       let jty = NCicUntrusted.apply_subst status subst ctx jty in
 585         noprint(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
 586         fast_eq_check unit_eq status j
 587     with
 588       | NCicEnvironment.ObjectNotFound s as e ->
 589           raise (Error (lazy "eq_coerc non yet defined",Some e))
 590       | Error _ as e -> debug_print (lazy "error"); raise e
 591
 592 let compare_statuses ~past ~present =
 593  let _,_,past,_,_ = past#obj in
 594  let _,_,present,_,_ = present#obj in
 595  List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
 596  List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
 597 ;;
 598
 599 (* paramodulation has only an implicit knowledge of the symmetry of equality;
 600    hence it is in trouble in proving (a = b) = (b = a) *)
 601 let try_sym tac status g =
 602   (* put the right uri *)
 603   let sym_eq = Ast.Appl [Ast.Ident("sym_eq",`Ambiguous); Ast.Implicit `Vector] in
 604   let _,_,metasenv,subst,_ = status#obj in
 605   let _, context, gty = List.assoc g metasenv in
 606   let is_eq =
 607     NCicParamod.is_equation status metasenv subst context gty
 608   in
 609   if is_eq then
 610     try tac status g
 611     with Error _ ->
 612       let new_status = instantiate_with_ast status g ("",0,sym_eq) in
 613       let go, _ = compare_statuses ~past:status ~present:new_status in
 614       assert (List.length go  = 1);
 615       let ng = List.hd go in
 616       tac new_status ng
 617    else tac status g
 618 ;;
 619
 620 let smart_apply_tac t s =
 621   let unit_eq = index_local_equations s#eq_cache s in
 622   NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s
 623   (* NTactics.distribute_tac (smart_apply t unit_eq) s *)
 624
 625 let smart_apply_auto t eq_cache =
 626   NTactics.distribute_tac (try_sym (smart_apply t eq_cache))
 627   (* NTactics.distribute_tac (smart_apply t eq_cache) *)
 628
 629
 630 (****************** types **************)
 631
 632
 633 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
 634
 635 (* cartesian: term set list -> term list set *)
 636 let rec cartesian =
 637  function
 638     [] -> NDiscriminationTree.TermListSet.empty
 639   | [l] ->
 640      NDiscriminationTree.TermSet.fold
 641       (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
 642   | he::tl ->
 643      let rest = cartesian tl in
 644       NDiscriminationTree.TermSet.fold
 645        (fun x acc ->
 646          NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
 647        ) he NDiscriminationTree.TermListSet.empty
 648 ;;
 649
 650 (* all_keys_of_cic_type: term -> term set *)
 651 let all_keys_of_cic_type status metasenv subst context ty =
 652  let saturate ty =
 653   (* Here we are dropping the metasenv, but this should not raise any
 654      exception (hopefully...) *)
 655   let ty,_,hyps =
 656    NCicMetaSubst.saturate status ~delta:max_int metasenv subst context ty 0
 657   in
 658    ty,List.length hyps
 659  in
 660  let rec aux ty =
 661   match ty with
 662      NCic.Appl (he::tl) ->
 663       let tl' =
 664        List.map (fun ty ->
 665         let wty = NCicReduction.whd status ~delta:0 ~subst context ty in
 666          if ty = wty then
 667           NDiscriminationTree.TermSet.add ty (aux ty)
 668          else
 669           NDiscriminationTree.TermSet.union
 670            (NDiscriminationTree.TermSet.add  ty (aux  ty))
 671            (NDiscriminationTree.TermSet.add wty (aux wty))
 672         ) tl
 673       in
 674        NDiscriminationTree.TermListSet.fold
 675         (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
 676         (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
 677         NDiscriminationTree.TermSet.empty
 678    | _ -> NDiscriminationTree.TermSet.empty
 679  in
 680   let ty,ity = saturate ty in
 681   let wty,iwty = saturate (NCicReduction.whd status ~delta:0 ~subst context ty) in
 682    if ty = wty then
 683     [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
 684    else
 685     [ity,  NDiscriminationTree.TermSet.add  ty (aux  ty) ;
 686      iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
 687 ;;
 688
 689 let all_keys_of_type status t =
 690  let _,_,metasenv,subst,_ = status#obj in
 691  let context = ctx_of t in
 692  let status, t = apply_subst status context t in
 693  let keys =
 694   all_keys_of_cic_type status metasenv subst context
 695    (snd (term_of_cic_term status t context))
 696  in
 697   status,
 698    List.map
 699     (fun (intros,keys) ->
 700       intros,
 701        NDiscriminationTree.TermSet.fold
 702         (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
 703         keys Ncic_termSet.empty
 704     ) keys
 705 ;;
 706
 707
 708 let keys_of_type status orig_ty =
 709   (* Here we are dropping the metasenv (in the status), but this should not
 710      raise any exception (hopefully...) *)
 711   let _, ty, _ = saturate ~delta:max_int status orig_ty in
 712   let _, ty = apply_subst status (ctx_of ty) ty in
 713   let keys =
 714 (*
 715     let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
 716     if orig_ty' <> orig_ty then
 717      let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
 718       [ty;ty']
 719     else
 720      [ty]
 721 *)
 722    [ty] in
 723 (*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
 724   let keys =
 725     let _, ty = term_of_cic_term status ty (ctx_of ty) in
 726     match ty with
 727     | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
 728     | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
 729        when h > 0 ->
 730          let _,ty,_= saturate status ~delta:(h-1) orig_ty in
 731          ty::keys
 732     | _ -> keys
 733   in
 734   status, keys
 735 ;;
 736
 737 let all_keys_of_term status t =
 738  let status, orig_ty = typeof status (ctx_of t) t in
 739   all_keys_of_type status orig_ty
 740 ;;
 741
 742 let keys_of_term status t =
 743   let status, orig_ty = typeof status (ctx_of t) t in
 744     keys_of_type status orig_ty
 745 ;;
 746
 747 let mk_th_cache status gl =
 748   List.fold_left
 749     (fun (status, acc) g ->
 750        let gty = get_goalty status g in
 751        let ctx = ctx_of gty in
 752        noprint(lazy("th cache for: "^ppterm status gty));
 753        noprint(lazy("th cache in: "^ppcontext status ctx));
 754        if List.mem_assq ctx acc then status, acc else
 755          let idx = InvRelDiscriminationTree.empty in
 756          let status,_,idx =
 757            List.fold_left
 758              (fun (status, i, idx) _ ->
 759                 let t = mk_cic_term ctx (NCic.Rel i) in
 760                 let status, keys = keys_of_term status t in
 761                 noprint(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
 762                 let idx =
 763                   List.fold_left (fun idx k ->
 764                     InvRelDiscriminationTree.index idx k t) idx keys
 765                 in
 766                 status, i+1, idx)
 767              (status, 1, idx) ctx
 768           in
 769          status, (ctx, idx) :: acc)
 770     (status,[]) gl
 771 ;;
 772
 773 let all_elements ctx cache =
 774   let dummy = mk_cic_term ctx (NCic.Meta (0,(0, (NCic.Irl 0)))) in
 775     try
 776       let idx = List.assq ctx cache in
 777       Ncic_termSet.elements
 778         (InvRelDiscriminationTree.retrieve_unifiables idx dummy)
 779     with Not_found -> []
 780
 781 let add_to_th t c ty =
 782   let key_c = ctx_of t in
 783   if not (List.mem_assq key_c c) then
 784       (key_c ,InvRelDiscriminationTree.index
 785                InvRelDiscriminationTree.empty ty t ) :: c
 786   else
 787     let rec replace = function
 788       | [] -> []
 789       | (x, idx) :: tl when x == key_c ->
 790           (x, InvRelDiscriminationTree.index idx ty t) :: tl
 791       | x :: tl -> x :: replace tl
 792     in
 793       replace c
 794 ;;
 795
 796 let rm_from_th t c ty =
 797   let key_c = ctx_of t in
 798   if not (List.mem_assq key_c c) then assert false
 799   else
 800     let rec replace = function
 801       | [] -> []
 802       | (x, idx) :: tl when x == key_c ->
 803           (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
 804       | x :: tl -> x :: replace tl
 805     in
 806       replace c
 807 ;;
 808
 809 let pp_idx status idx =
 810    InvRelDiscriminationTree.iter idx
 811       (fun k set ->
 812          noprint(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
 813          Ncic_termSet.iter
 814            (fun t -> debug_print(lazy("\t"^ppterm status t)))
 815            set)
 816 ;;
 817
 818 let pp_th (status: #NTacStatus.pstatus) =
 819   List.iter
 820     (fun ctx, idx ->
 821        noprint(lazy( "-----------------------------------------------"));
 822        noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx)));
 823        noprint(lazy( "||====>  "));
 824        pp_idx status idx)
 825 ;;
 826
 827 let search_in_th gty th =
 828   let c = ctx_of gty in
 829   let rec aux acc = function
 830    | [] -> (* Ncic_termSet.elements *) acc
 831    | (_::tl) as k ->
 832        try
 833          let idx = List.assoc(*q*) k th in
 834          let acc = Ncic_termSet.union acc
 835            (InvRelDiscriminationTree.retrieve_unifiables idx gty)
 836          in
 837          aux acc tl
 838        with Not_found -> aux acc tl
 839   in
 840     aux Ncic_termSet.empty c
 841 ;;
 842
 843 type flags = {
 844         do_types : bool; (* solve goals in Type *)
 845         last : bool; (* last goal: take first solution only  *)
 846         candidates: Ast.term list option;
 847         maxwidth : int;
 848         maxsize  : int;
 849         maxdepth : int;
 850         timeout  : float;
 851 }
 852
 853 type cache =
 854     {facts : th_cache; (* positive results *)
 855      under_inspection : cic_term list * th_cache; (* to prune looping *)
 856      failures : th_cache; (* to avoid repetitions *)
 857      unit_eq : NCicParamod.state;
 858      trace: Ast.term list
 859     }
 860
 861 let add_to_trace status ~depth cache t =
 862   match t with
 863     | Ast.NRef _ ->
 864         print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
 865         {cache with trace = t::cache.trace}
 866     | Ast.NCic _  (* local candidate *)
 867     | _  -> (*not an application *) cache
 868
 869 let pptrace status tr =
 870   (lazy ("Proof Trace: " ^ (String.concat ";"
 871                               (List.map (NotationPp.pp_term status) tr))))
 872 (* not used
 873 let remove_from_trace cache t =
 874   match t with
 875     | Ast.NRef _ ->
 876         (match cache.trace with
 877            |  _::tl -> {cache with trace = tl}
 878            | _ -> assert false)
 879     | Ast.NCic _  (* local candidate *)
 880     |  _  -> (*not an application *) cache *)
 881
 882 type sort = T | P
 883 type goal = int * sort (* goal, depth, sort *)
 884 type fail = goal * cic_term
 885 type candidate = int * Ast.term (* unique candidate number, candidate *)
 886
 887 exception Gaveup of th_cache (* failure cache *)
 888 exception Proved of NTacStatus.tac_status * Ast.term list
 889
 890 (* let close_failures _ c = c;; *)
 891 (* let prunable _ _ _ = false;; *)
 892 (* let cache_examine cache gty = `Notfound;; *)
 893 (* let put_in_subst s _ _ _  = s;; *)
 894 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
 895 (* let cache_add_underinspection c _ _ = c;; *)
 896
 897 let init_cache ?(facts=[]) ?(under_inspection=[],[])
 898     ?(failures=[])
 899     ?(unit_eq=NCicParamod.empty_state)
 900     ?(trace=[])
 901     _ =
 902     {facts = facts;
 903      failures = failures;
 904      under_inspection = under_inspection;
 905      unit_eq = unit_eq;
 906      trace = trace}
 907
 908 let only signature _context candidate = true
 909 (*
 910         (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
 911   let candidate_ty =
 912    NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
 913   in
 914   let height = fast_height_of_term status candidate_ty in
 915   let rc = signature >= height in
 916   if rc = false then
 917     noprint (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[]
 918           ~metasenv:[] candidate ^ ": " ^ string_of_int height))
 919   else
 920     noprint (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[]
 921           ~metasenv:[] candidate ^ ": " ^ string_of_int height));
 922
 923   rc *)
 924 ;;
 925
 926 let candidate_no = ref 0;;
 927
 928 let openg_no status = List.length (head_goals status#stack)
 929
 930 let sort_candidates status ctx candidates =
 931  let _,_,metasenv,subst,_ = status#obj in
 932   let branch cand =
 933     let status,ct = disambiguate status ctx ("",0,cand) None in
 934     let status,t = term_of_cic_term status ct ctx in
 935     let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
 936     let res = branch status (mk_cic_term ctx ty) in
 937     noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
 938                       ^ (string_of_int res)));
 939       res
 940   in
 941   let candidates = List.map (fun t -> branch t,t) candidates in
 942   let candidates =
 943      List.sort (fun (a,_) (b,_) -> a - b) candidates in
 944   let candidates = List.map snd candidates in
 945     noprint (lazy ("candidates =\n" ^ (String.concat "\n"
 946         (List.map (NotationPp.pp_term status) candidates))));
 947     candidates
 948
 949 let sort_new_elems l =
 950   List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
 951
 952 let rec stack_goals level gs =
 953   if level = 0 then []
 954   else match gs with
 955     | [] -> assert false
 956     | (g,_,_,_)::s ->
 957         let is_open = function
 958           | (_,Continuationals.Stack.Open i) -> Some i
 959           | (_,Continuationals.Stack.Closed _) -> None
 960         in
 961           HExtlib.filter_map is_open g @ stack_goals (level-1) s
 962 ;;
 963
 964 let open_goals level status = stack_goals level status#stack
 965 ;;
 966
 967 let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
 968  try
 969   let old_og_no = List.length (open_goals (depth+1) status) in
 970   debug_print ~depth (lazy ("try " ^ (NotationPp.pp_term status) t));
 971   let status =
 972     if smart= 0 then NTactics.apply_tac ("",0,t) status
 973     else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
 974     else (* smart = 2: both *)
 975       try NTactics.apply_tac ("",0,t) status
 976       with Error _ ->
 977         smart_apply_auto ("",0,t) eq_cache status
 978   in
 979     (* we compare the expected branching with the actual one and
 980        prune the candidate when the latter is larger. The optimization
 981        is meant to rule out stange applications of flexible terms,
 982        such as the application of eq_f that always succeeds.
 983        There is some gain but less than expected *)
 984   let og_no = List.length (open_goals (depth+1) status) in
 985   let status, cict = disambiguate status ctx ("",0,t) None in
 986   let status,ct = term_of_cic_term status cict ctx in
 987   let _,_,metasenv,subst,_ = status#obj in
 988   let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
 989   let res = branch status (mk_cic_term ctx ty) in
 990   let diff = og_no - old_og_no in
 991   debug_print (lazy ("expected branching: " ^ (string_of_int res)));
 992   debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
 993   (* some flexibility *)
 994   if diff > res  && res > 0 (* facts are never pruned *) then
 995     (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
 996                     ^ (string_of_int res) ^ " vs. " ^ (string_of_int diff)));
 997      debug_print ~depth (lazy "strange application"); None)
 998   else
 999     (incr candidate_no; Some ((!candidate_no,t),status))
1000  with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1001 ;;
1002
1003 let sort_of status subst metasenv ctx t =
1004   let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
1005   let metasenv',ty = NCicUnification.fix_sorts status metasenv subst ty in
1006    assert (metasenv = metasenv');
1007    NCicTypeChecker.typeof status subst metasenv ctx ty
1008 ;;
1009
1010 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
1011 ;;
1012
1013 let perforate_small status subst metasenv context t =
1014   let rec aux = function
1015     | NCic.Appl (hd::tl) ->
1016         let map t =
1017           let s = sort_of status subst metasenv context t in
1018             match s with
1019               | NCic.Sort(NCic.Type [`Type,u])
1020                   when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
1021               | _ -> aux t
1022         in
1023           NCic.Appl (hd::List.map map tl)
1024     | t -> t
1025   in
1026     aux t
1027 ;;
1028
1029 let get_cands retrieve_for diff empty gty weak_gty =
1030   let cands = retrieve_for gty in
1031     match weak_gty with
1032       | None -> cands, empty
1033       | Some weak_gty ->
1034           let more_cands =  retrieve_for weak_gty in
1035             cands, diff more_cands cands
1036 ;;
1037
1038 let get_candidates ?(smart=true) depth flags status cache signature gty =
1039   let universe = status#auto_cache in
1040   let _,_,metasenv,subst,_ = status#obj in
1041   let context = ctx_of gty in
1042   let _, raw_gty = term_of_cic_term status gty context in
1043   let is_prod, is_eq =
1044   let status, t = term_of_cic_term status gty context  in
1045   let t = NCicReduction.whd status subst context t in
1046     match t with
1047       | NCic.Prod _ -> true, false
1048       | _ -> false, NCicParamod.is_equation status metasenv subst context t
1049   in
1050   debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1051   let is_eq =
1052     NCicParamod.is_equation status metasenv subst context raw_gty
1053   in
1054   let raw_weak_gty, weak_gty  =
1055     if smart then
1056       match raw_gty with
1057         | NCic.Appl _
1058         | NCic.Const _
1059         | NCic.Rel _ ->
1060             let raw_weak =
1061               perforate_small status subst metasenv context raw_gty in
1062             let weak = mk_cic_term context raw_weak in
1063             debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1064               Some raw_weak, Some (weak)
1065         | _ -> None,None
1066     else None,None
1067   in
1068   (* we now compute global candidates *)
1069   let global_cands, smart_global_cands =
1070     let mapf s =
1071       let to_ast = function
1072         | NCic.Const r when true
1073              (*is_relevant statistics r*) -> Some (Ast.NRef r)
1074      (* | NCic.Const _ -> None  *)
1075         | _ -> assert false in
1076           HExtlib.filter_map
1077             to_ast (NDiscriminationTree.TermSet.elements s) in
1078       let g,l =
1079         get_cands
1080           (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
1081           NDiscriminationTree.TermSet.diff
1082           NDiscriminationTree.TermSet.empty
1083           raw_gty raw_weak_gty in
1084       mapf g, mapf l in
1085   (* we now compute local candidates *)
1086   let local_cands,smart_local_cands =
1087     let mapf s =
1088       let to_ast t =
1089         let _status, t = term_of_cic_term status t context
1090         in Ast.NCic t in
1091         List.map to_ast (Ncic_termSet.elements s) in
1092     let g,l =
1093       get_cands
1094         (fun ty -> search_in_th ty cache)
1095         Ncic_termSet.diff  Ncic_termSet.empty gty weak_gty in
1096       mapf g, mapf l in
1097   (* we now splits candidates in facts or not facts *)
1098   let test = is_a_fact_ast status subst metasenv context in
1099   let by,given_candidates =
1100     match flags.candidates with
1101     | Some l -> true, l
1102     | None -> false, [] in
1103   (* we compute candidates to be applied in normal mode, splitted in
1104      facts and not facts *)
1105   let candidates_facts,candidates_other =
1106     let gl1,gl2 = List.partition test global_cands in
1107     let ll1,ll2 = List.partition test local_cands in
1108     (* if the goal is an equation we avoid to apply unit equalities,
1109      since superposition should take care of them; refl is an
1110      exception since it prompts for convertibility *)
1111     let l1 = if is_eq then [Ast.Ident("refl",`Ambiguous)] else gl1@ll1 in
1112     let l2 =
1113       (* if smart given candidates are applied in smart mode *)
1114       if by && smart then ll2
1115       else if by then given_candidates@ll2
1116       else gl2@ll2
1117     in l1,l2
1118   in
1119   (* we now compute candidates to be applied in smart mode, splitted in
1120      facts and not facts *)
1121   let smart_candidates_facts, smart_candidates_other =
1122     if is_prod || not(smart) then [],[]
1123     else
1124     let sgl1,sgl2 = List.partition test smart_global_cands in
1125     let sll1,sll2 = List.partition test smart_local_cands in
1126     let l1 = if is_eq then [] else sgl1@sll1 in
1127     let l2 =
1128       if by && smart then given_candidates@sll2
1129       else if by then sll2
1130       else sgl2@sll2
1131     in l1,l2
1132   in
1133   candidates_facts,
1134   smart_candidates_facts,
1135   sort_candidates status context (candidates_other),
1136   sort_candidates status context (smart_candidates_other)
1137 ;;
1138
1139 let applicative_case depth signature status flags gty cache =
1140   app_counter:= !app_counter+1;
1141   let _,_,metasenv,subst,_ = status#obj in
1142   let context = ctx_of gty in
1143   let tcache = cache.facts in
1144   let is_prod, is_eq =
1145     let status, t = term_of_cic_term status gty context  in
1146     let t = NCicReduction.whd status subst context t in
1147       match t with
1148         | NCic.Prod _ -> true, false
1149         | _ -> false, NCicParamod.is_equation status metasenv subst context t
1150   in
1151   debug_print ~depth (lazy (string_of_bool is_eq));
1152   (* new *)
1153   let candidates_facts, smart_candidates_facts,
1154       candidates_other, smart_candidates_other =
1155     get_candidates ~smart:true depth
1156       flags status tcache signature gty
1157   in
1158   let sm = if is_eq || is_prod then 0 else 2 in
1159   let sm1 = if flags.last then 2 else 0 in
1160   let maxd = (depth + 1 = flags.maxdepth) in
1161   let try_candidates only_one sm acc candidates =
1162     List.fold_left
1163       (fun elems cand ->
1164          if (only_one && (elems <> [])) then elems
1165          else
1166            match try_candidate (~smart:sm)
1167              flags depth status cache.unit_eq context cand with
1168                | None -> elems
1169                | Some x -> x::elems)
1170       acc candidates
1171   in
1172   (* if the goal is the last one we stop at the first fact *)
1173   let elems = try_candidates flags.last sm [] candidates_facts in
1174   (* now we add smart_facts *)
1175   let elems = try_candidates flags.last sm elems smart_candidates_facts in
1176   (* if we are at maxdepth and the goal is not a product we are done
1177      similarly, if the goal is the last one and we already found a
1178      solution *)
1179   if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1180   else
1181     let elems = try_candidates false 2 elems candidates_other in
1182     debug_print ~depth (lazy ("not facts: try smart application"));
1183     try_candidates false 2 elems smart_candidates_other
1184 ;;
1185
1186 exception Found
1187 ;;
1188
1189 (* gty is supposed to be meta-closed *)
1190 let is_subsumed depth filter_depth status gty cache =
1191   if cache=[] then false else (
1192   debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1193   let n,h,metasenv,subst,obj = status#obj in
1194   let ctx = ctx_of gty in
1195   let _ , raw_gty = term_of_cic_term status gty ctx in
1196   let target = NCicSubstitution.lift status 1 raw_gty in
1197   (* we compute candidates using the perforated type *)
1198   let weak_gty  =
1199     match target with
1200       | NCic.Appl _
1201       | NCic.Const _
1202       | NCic.Rel _ ->
1203           let raw_weak =
1204             perforate_small status subst metasenv ctx raw_gty in
1205           let weak = mk_cic_term ctx raw_weak in
1206           debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1207           Some (weak)
1208       | _ -> None
1209   in
1210   (* candidates must only be searched w.r.t the given context *)
1211   let candidates =
1212     try
1213     let idx = List.assq ctx cache in
1214     match weak_gty with
1215       | Some weak ->
1216           Ncic_termSet.elements
1217             (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1218       |None -> []
1219     with Not_found -> []
1220   in
1221   (* this is a dirty trick: the first argument of an application is used
1222      to remember at which depth a goal failed *)
1223   let filter t =
1224     let ctx = ctx_of t in
1225     let _, src = term_of_cic_term status t ctx in
1226     match src with
1227      | NCic.Appl [NCic.Implicit (`Typeof d); t]
1228        when d <= depth -> Some (mk_cic_term ctx t)
1229      | _ -> None in
1230   let candidates =
1231     if filter_depth then HExtlib.filter_map filter candidates else candidates in
1232   debug_print ~depth
1233     (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1234     try
1235       List.iter
1236         (fun t ->
1237            let _ , source = term_of_cic_term status t ctx in
1238            let implication =
1239              NCic.Prod("foo",source,target) in
1240            let metasenv,j,_,_ =
1241              NCicMetaSubst.mk_meta
1242                metasenv ctx ~with_type:implication `IsType in
1243            let status = status#set_obj (n,h,metasenv,subst,obj) in
1244            let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1245            try
1246              let status = NTactics.intro_tac "foo" status in
1247              let status =
1248                NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1249              in
1250                if (head_goals status#stack = []) then raise Found
1251                else ()
1252            with
1253              | Error _ -> ())
1254         candidates;false
1255     with Found -> debug_print ~depth (lazy "success");true)
1256 ;;
1257
1258 let rec guess_name name ctx =
1259   if name = "_" then guess_name "auto" ctx else
1260   if not (List.mem_assoc name ctx) then name else
1261   guess_name (name^"'") ctx
1262 ;;
1263
1264 let is_prod status =
1265   let _, ctx, gty = current_goal status in
1266   let status, gty = apply_subst status ctx gty in
1267   let _, raw_gty = term_of_cic_term status gty ctx in
1268   match raw_gty with
1269     | NCic.Prod (name,src,_) ->
1270         let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1271         (match snd (term_of_cic_term status src ctx) with
1272         | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1273         | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1274             let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1275             (match itys with
1276             (* | [_,_,_,[_;_]]  con nat va, ovviamente, in loop *)
1277             | [_,_,_,[_]]
1278             | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1279             | _ -> `Some (guess_name name ctx))
1280         | _ -> `Some (guess_name name ctx))
1281     | _ -> `None
1282
1283 let intro ~depth status facts name =
1284   let status = NTactics.intro_tac name status in
1285   let _, ctx, ngty = current_goal status in
1286   let t = mk_cic_term ctx (NCic.Rel 1) in
1287   let status, keys = keys_of_term status t in
1288   let facts = List.fold_left (add_to_th t) facts keys in
1289     debug_print ~depth (lazy ("intro: "^ name));
1290   (* unprovability is not stable w.r.t introduction *)
1291   status, facts
1292 ;;
1293
1294 let rec intros_facts ~depth status facts =
1295   if List.length (head_goals status#stack) <> 1 then status, facts else
1296   match is_prod status with
1297     | `Inductive name
1298     | `Some(name) ->
1299         let status,facts =
1300           intro ~depth status facts name
1301         in intros_facts ~depth status facts
1302 (*    | `Inductive name ->
1303           let status = NTactics.case1_tac name status in
1304           intros_facts ~depth status facts *)
1305     | _ -> status, facts
1306 ;;
1307
1308 let intros ~depth status cache =
1309     match is_prod status with
1310       | `Inductive _
1311       | `Some _ ->
1312           let trace = cache.trace in
1313           let status,facts =
1314             intros_facts ~depth status cache.facts
1315           in
1316           if head_goals status#stack = [] then
1317             let status = NTactics.merge_tac status in
1318             [(0,Ast.Ident("__intros",`Ambiguous)),status], cache
1319           else
1320             (* we reindex the equation from scratch *)
1321             let unit_eq = index_local_equations status#eq_cache status in
1322             let status = NTactics.merge_tac status in
1323             [(0,Ast.Ident("__intros",`Ambiguous)),status],
1324             init_cache ~facts ~unit_eq () ~trace
1325       | _ -> [],cache
1326 ;;
1327
1328 let reduce ~whd ~depth status g =
1329   let n,h,metasenv,subst,o = status#obj in
1330   let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1331   let ty = NCicUntrusted.apply_subst status subst ctx ty in
1332   let ty' =
1333    (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1334   in
1335   if ty = ty' then []
1336   else
1337     (debug_print ~depth
1338       (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1339     let metasenv =
1340       (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1341     in
1342     let status = status#set_obj (n,h,metasenv,subst,o) in
1343     (* we merge to gain a depth level; the previous goal level should
1344        be empty *)
1345     let status = NTactics.merge_tac status in
1346     incr candidate_no;
1347     [(!candidate_no,Ast.Ident("__whd",`Ambiguous)),status])
1348 ;;
1349
1350 let do_something signature flags status g depth gty cache =
1351   let l0, cache = intros ~depth status cache in
1352   if l0 <> [] then l0, cache
1353   else
1354   (* whd *)
1355   let l = reduce ~whd:true ~depth status g in
1356   (* if l <> [] then l,cache else *)
1357   (* backward aplications *)
1358   let l1 =
1359     List.map
1360       (fun s ->
1361          incr candidate_no;
1362          ((!candidate_no,Ast.Ident("__paramod",`Ambiguous)),s))
1363       (auto_eq_check cache.unit_eq status)
1364   in
1365   let l2 =
1366     if ((l1 <> []) && flags.last) then [] else
1367     applicative_case depth signature status flags gty cache
1368   in
1369   (* statistics *)
1370   List.iter
1371     (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1372   (* states in l1 have have an empty set of subgoals: no point to sort them *)
1373   debug_print ~depth
1374     (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1375     (* we order alternatives w.r.t the number of subgoals they open *)
1376     l1 @ (sort_new_elems l2) @ l, cache
1377 ;;
1378
1379 let pp_goal = function
1380   | (_,Continuationals.Stack.Open i)
1381   | (_,Continuationals.Stack.Closed i) -> string_of_int i
1382 ;;
1383
1384 let pp_goals status l =
1385   String.concat ", "
1386     (List.map
1387        (fun i ->
1388           let gty = get_goalty status i in
1389             NTacStatus.ppterm status gty)
1390        l)
1391 ;;
1392
1393 module M =
1394   struct
1395     type t = int
1396     let compare = Pervasives.compare
1397   end
1398 ;;
1399
1400 module MS = HTopoSort.Make(M)
1401 ;;
1402
1403 let sort_tac status =
1404   let gstatus =
1405     match status#stack with
1406     | [] -> assert false
1407     | (goals, t, k, tag) :: s ->
1408         let g = head_goals status#stack in
1409         let sortedg =
1410           (List.rev (MS.topological_sort g (deps status))) in
1411           noprint (lazy ("old g = " ^
1412             String.concat "," (List.map string_of_int g)));
1413           noprint (lazy ("sorted goals = " ^
1414             String.concat "," (List.map string_of_int sortedg)));
1415           let is_it i = function
1416             | (_,Continuationals.Stack.Open j )
1417             | (_,Continuationals.Stack.Closed j ) -> i = j
1418           in
1419           let sorted_goals =
1420             List.map (fun i -> List.find (is_it i) goals) sortedg
1421           in
1422             (sorted_goals, t, k, tag) :: s
1423   in
1424    status#set_stack gstatus
1425 ;;
1426
1427 let clean_up_tac status =
1428   let gstatus =
1429     match status#stack with
1430     | [] -> assert false
1431     | (g, t, k, tag) :: s ->
1432         let is_open = function
1433           | (_,Continuationals.Stack.Open _) -> true
1434           | (_,Continuationals.Stack.Closed _) -> false
1435         in
1436         let g' = List.filter is_open g in
1437           (g', t, k, tag) :: s
1438   in
1439    status#set_stack gstatus
1440 ;;
1441
1442 let focus_tac focus status =
1443   let gstatus =
1444     match status#stack with
1445     | [] -> assert false
1446     | (g, t, k, tag) :: s ->
1447         let in_focus = function
1448           | (_,Continuationals.Stack.Open i)
1449           | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1450         in
1451         let focus,others = List.partition in_focus g
1452         in
1453           (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1454           (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1455   in
1456    status#set_stack gstatus
1457 ;;
1458
1459 let deep_focus_tac level focus status =
1460   let in_focus = function
1461     | (_,Continuationals.Stack.Open i)
1462     | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1463   in
1464   let rec slice level gs =
1465     if level = 0 then [],[],gs else
1466       match gs with
1467         | [] -> assert false
1468         | (g, t, k, tag) :: s ->
1469             let f,o,gs = slice (level-1) s in
1470             let f1,o1 = List.partition in_focus g
1471             in
1472             (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1473   in
1474   let gstatus =
1475     let f,o,s = slice level status#stack in f@o@s
1476   in
1477    status#set_stack gstatus
1478 ;;
1479
1480 let move_to_side level status =
1481 match status#stack with
1482   | [] -> assert false
1483   | (g,_,_,_)::tl ->
1484       let is_open = function
1485           | (_,Continuationals.Stack.Open i) -> Some i
1486           | (_,Continuationals.Stack.Closed _) -> None
1487         in
1488       let others = menv_closure status (stack_goals (level-1) tl) in
1489       List.for_all (fun i -> IntSet.mem i others)
1490         (HExtlib.filter_map is_open g)
1491
1492 let top_cache ~depth top status cache =
1493   if top then
1494     let unit_eq = index_local_equations status#eq_cache status in
1495     {cache with unit_eq = unit_eq}
1496   else cache
1497
1498 let rec auto_clusters ?(top=false)
1499     flags signature cache depth status : unit =
1500   debug_print ~depth (lazy ("entering auto clusters at depth " ^
1501                            (string_of_int depth)));
1502   debug_print ~depth (pptrace status cache.trace);
1503   (* ignore(Unix.select [] [] [] 0.01); *)
1504   let status = clean_up_tac status in
1505   let goals = head_goals status#stack in
1506   if goals = [] then
1507     if depth = 0 then raise (Proved (status, cache.trace))
1508     else
1509       let status = NTactics.merge_tac status in
1510         let cache =
1511         let l,tree = cache.under_inspection in
1512           match l with
1513             | [] -> cache (* possible because of intros that cleans the cache *)
1514             | a::tl -> let tree = rm_from_th a tree a in
1515               {cache with under_inspection = tl,tree}
1516         in
1517          auto_clusters flags signature cache (depth-1) status
1518   else if List.length goals < 2 then
1519     let cache = top_cache ~depth top status cache in
1520     auto_main flags signature cache depth status
1521   else
1522     let all_goals = open_goals (depth+1) status in
1523     debug_print ~depth (lazy ("goals = " ^
1524       String.concat "," (List.map string_of_int all_goals)));
1525     let classes = HExtlib.clusters (deps status) all_goals in
1526     (* if any of the classes exceed maxwidth we fail *)
1527     List.iter
1528       (fun gl ->
1529          if List.length gl > flags.maxwidth then
1530            begin
1531              debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1532              HLog.warn (sprintf "global width (%u) exceeded: %u"
1533                flags.maxwidth (List.length gl));
1534              raise (Gaveup cache.failures)
1535            end else ()) classes;
1536     if List.length classes = 1 then
1537       let flags =
1538         {flags with last = (List.length all_goals = 1)} in
1539         (* no need to cluster *)
1540       let cache = top_cache ~depth top status cache in
1541         auto_main flags signature cache depth status
1542     else
1543       let classes = if top then List.rev classes else classes in
1544       debug_print ~depth
1545         (lazy
1546            (String.concat "\n"
1547            (List.map
1548              (fun l ->
1549                ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1550            classes)));
1551       (* we now process each cluster *)
1552       let status,cache,b =
1553         List.fold_left
1554           (fun (status,cache,b) gl ->
1555              let flags =
1556                {flags with last = (List.length gl = 1)} in
1557              let lold = List.length status#stack in
1558               debug_print ~depth (lazy ("stack length = " ^
1559                         (string_of_int lold)));
1560              let fstatus = deep_focus_tac (depth+1) gl status in
1561              let cache = top_cache ~depth top fstatus cache in
1562              try
1563                debug_print ~depth (lazy ("focusing on" ^
1564                               String.concat "," (List.map string_of_int gl)));
1565                auto_main flags signature cache depth fstatus; assert false
1566              with
1567                | Proved(status,trace) ->
1568                    let status = NTactics.merge_tac status in
1569                    let cache = {cache with trace = trace} in
1570                    let lnew = List.length status#stack in
1571                      assert (lold = lnew);
1572                    (status,cache,true)
1573                | Gaveup failures when top ->
1574                    let cache = {cache with failures = failures} in
1575                    (status,cache,b)
1576           )
1577           (status,cache,false) classes
1578       in
1579       let rec final_merge n s =
1580         if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1581       in let status = final_merge depth status
1582       in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1583
1584 and
1585
1586 (* BRAND NEW VERSION *)
1587 auto_main flags signature cache depth status: unit =
1588   debug_print ~depth (lazy "entering auto main");
1589   debug_print ~depth (pptrace status cache.trace);
1590   debug_print ~depth (lazy ("stack length = " ^
1591                         (string_of_int (List.length status#stack))));
1592   (* ignore(Unix.select [] [] [] 0.01); *)
1593   let status = sort_tac (clean_up_tac status) in
1594   let goals = head_goals status#stack in
1595   match goals with
1596     | [] when depth = 0 -> raise (Proved (status,cache.trace))
1597     | []  ->
1598         let status = NTactics.merge_tac status in
1599         let cache =
1600           let l,tree = cache.under_inspection in
1601             match l with
1602               | [] -> cache (* possible because of intros that cleans the cache *)
1603               | a::tl -> let tree = rm_from_th a tree a in
1604                   {cache with under_inspection = tl,tree}
1605         in
1606           auto_clusters flags signature cache (depth-1) status
1607     | orig::_ ->
1608         if depth > 0 && move_to_side depth status
1609         then
1610           let status = NTactics.merge_tac status in
1611           let cache =
1612             let l,tree = cache.under_inspection in
1613               match l with
1614                 | [] -> cache (* possible because of intros that cleans the cache*)
1615                 | a::tl -> let tree = rm_from_th a tree a in
1616                     {cache with under_inspection = tl,tree}
1617           in
1618             auto_clusters flags signature cache (depth-1) status
1619         else
1620         let ng = List.length goals in
1621         (* moved inside auto_clusters *)
1622         if ng > flags.maxwidth then begin
1623           debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1624           HLog.warn (sprintf "local width (%u) exceeded: %u"
1625              flags.maxwidth ng);
1626           raise (Gaveup cache.failures)
1627         end else if depth = flags.maxdepth then
1628           raise (Gaveup cache.failures)
1629         else
1630         let status = NTactics.branch_tac ~force:true status in
1631         let g,gctx, gty = current_goal status in
1632         let ctx,ty = close status g in
1633         let closegty = mk_cic_term ctx ty in
1634         let status, gty = apply_subst status gctx gty in
1635         debug_print ~depth (lazy("Attacking goal " ^
1636           string_of_int g ^ " : "^ppterm status gty));
1637         debug_print ~depth (lazy ("current failures: " ^
1638           string_of_int (List.length (all_elements ctx cache.failures))));
1639         let is_eq =
1640            let _,_,metasenv,subst,_ = status#obj in
1641            NCicParamod.is_equation status metasenv subst ctx ty in
1642         (* if the goal is an equality we artificially raise its depth up to
1643            flags.maxdepth - 1 *)
1644         if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then
1645         (* for efficiency reasons, in this case we severely cripple the
1646            search depth *)
1647           (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1648            auto_main flags signature cache (depth+1) status)
1649         (* check for loops *)
1650         else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1651           (debug_print ~depth (lazy "SUBSUMED");
1652            raise (Gaveup cache.failures))
1653         (* check for failures *)
1654         else if is_subsumed depth true status closegty cache.failures then
1655           (debug_print ~depth (lazy "ALREADY MET");
1656            raise (Gaveup cache.failures))
1657         else
1658         let new_sig = height_of_goal g status in
1659         if new_sig < signature then
1660           (debug_print  ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1661            debug_print  ~depth (lazy ("olds = " ^ (string_of_int signature))));
1662         let alternatives, cache =
1663           do_something signature flags status g depth gty cache in
1664         let loop_cache =
1665           if flags.last then
1666             let l,tree = cache.under_inspection in
1667             let l,tree = closegty::l, add_to_th closegty tree closegty in
1668             {cache with under_inspection = l,tree}
1669           else cache in
1670         let failures =
1671           List.fold_left
1672           (fun allfailures ((_,t),status) ->
1673              debug_print ~depth
1674                (lazy ("(re)considering goal " ^
1675                        (string_of_int g) ^" : "^ppterm status gty));
1676              debug_print (~depth:depth)
1677                (lazy ("Case: " ^ NotationPp.pp_term status t));
1678              let depth,cache =
1679                if t=Ast.Ident("__whd",`Ambiguous) ||
1680                   t=Ast.Ident("__intros",`Ambiguous)
1681                then depth, cache
1682                else depth+1,loop_cache in
1683              let cache = add_to_trace status ~depth cache t in
1684              let cache = {cache with failures = allfailures} in
1685              try
1686                auto_clusters flags signature cache depth status;
1687                assert false;
1688              with Gaveup fail ->
1689                debug_print ~depth (lazy "Failed");
1690                fail)
1691           cache.failures alternatives in
1692         let failures =
1693           if flags.last then
1694             let newfail =
1695               let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1696               mk_cic_term ctx dty
1697             in
1698             prerr_endline ("FAILURE : " ^ ppterm status gty);
1699             add_to_th newfail failures closegty
1700           else failures in
1701         debug_print ~depth (lazy "no more candidates");
1702         raise (Gaveup failures)
1703 ;;
1704
1705 let int name l def =
1706   try int_of_string (List.assoc name l)
1707   with Failure _ | Not_found -> def
1708 ;;
1709
1710 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1711
1712 let cleanup_trace s trace =
1713   (* removing duplicates *)
1714   let trace_set =
1715     List.fold_left
1716       (fun acc t -> AstSet.add t acc)
1717       AstSet.empty trace in
1718   let trace = AstSet.elements trace_set
1719     (* filtering facts *)
1720   in List.filter
1721        (fun t ->
1722           match t with
1723             | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1724             | _ -> false) trace
1725 ;;
1726
1727 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1728   let oldstatus = status in
1729   let status = (status:> NTacStatus.tac_status) in
1730   let goals = head_goals status#stack in
1731   let status, facts = mk_th_cache status goals in
1732 (* let unit_eq = index_local_equations status#eq_cache status in *)
1733   let cache = init_cache ~facts () in
1734 (*   pp_th status facts; *)
1735 (*
1736   NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1737     (*debug_*)print (lazy(
1738       NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1739       String.concat "\n    " (List.map (
1740       status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1741         (NDiscriminationTree.TermSet.elements t))
1742       )));
1743 *)
1744   (* To allow using Rels in the user-specified candidates, we need a context
1745    * but in the case where multiple goals are open, there is no single context
1746    * to type the Rels. At this time, we require that Rels be typed in the
1747    * context of the first selected goal *)
1748   let _,ctx,_ = current_goal ~single_goal:false status in
1749   let status, candidates =
1750     match univ with
1751       | None -> status, None
1752       | Some l ->
1753           let to_Ast (st,l) t =
1754             let st, res = disambiguate st ctx t None in
1755             let st, res = term_of_cic_term st res (ctx_of res)
1756             in (st, Ast.NCic res::l)
1757           in
1758           let status, l' = List.fold_left to_Ast (status,[]) l in
1759           status, Some l'
1760   in
1761   let depth = int "depth" flags 3 in
1762   let size  = int "size" flags 10 in
1763   let width = int "width" flags 4 (* (3+List.length goals)*) in
1764   (* XXX fix sort *)
1765 (*   let goals = List.map (fun i -> (i,P)) goals in *)
1766   let signature = height_of_goals status in
1767   let flags = {
1768           last = true;
1769           candidates = candidates;
1770           maxwidth = width;
1771           maxsize = size;
1772           maxdepth = depth;
1773           timeout = Unix.gettimeofday() +. 3000.;
1774           do_types = false;
1775   } in
1776   let initial_time = Unix.gettimeofday() in
1777   app_counter:= 0;
1778   let rec up_to x y =
1779     if x > y then
1780       (debug_print(lazy
1781         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1782        debug_print(lazy
1783         ("Applicative nodes:"^string_of_int !app_counter));
1784        raise (Error (lazy "auto gave up", None)))
1785     else
1786       let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1787       let flags = { flags with maxdepth = x }
1788       in
1789         try auto_clusters (~top:true) flags signature cache 0 status;assert false
1790 (*
1791         try auto_main flags signature cache 0 status;assert false
1792 *)
1793         with
1794           | Gaveup _ -> up_to (x+1) y
1795           | Proved (s,trace) ->
1796               debug_print (lazy ("proved at depth " ^ string_of_int x));
1797               List.iter (toref incr_uses statistics) trace;
1798               let _ = debug_print (pptrace status trace) in
1799               let trace = cleanup_trace s trace in
1800               let _ = debug_print (pptrace status trace) in
1801               let stack =
1802                 match s#stack with
1803                   | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1804                   | _ -> assert false
1805               in
1806               let s = s#set_stack stack in
1807                 trace_ref := trace;
1808                 oldstatus#set_status s
1809   in
1810   let s = up_to depth depth in
1811     debug_print (print_stat status statistics);
1812     debug_print(lazy
1813         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1814     debug_print(lazy
1815         ("Applicative nodes:"^string_of_int !app_counter));
1816     s
1817 ;;
1818
1819 let auto_tac ~params:(_,flags as params) ?trace_ref =
1820   if List.mem_assoc "demod" flags then
1821     demod_tac ~params
1822   else if List.mem_assoc "paramod" flags then
1823     paramod_tac ~params
1824   else if List.mem_assoc "fast_paramod" flags then
1825     fast_eq_check_tac ~params
1826   else auto_tac ~params ?trace_ref
1827 ;;
1828
1829
1830
1831
1832
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847