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