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 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   (* some flexibility *)
 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     let gl1,gl2 = List.partition test global_cands in
1102     let ll1,ll2 = List.partition test local_cands in
1103     (* if the goal is an equation we avoid to apply unit equalities,
1104      since superposition should take care of them; refl is an
1105      exception since it prompts for convertibility *)
1106     let l1 = if is_eq then [Ast.Ident("refl",`Ambiguous)] else gl1@ll1 in
1107     let l2 =
1108       (* if smart given candidates are applied in smart mode *)
1109       if by && smart then ll2
1110       else if by then given_candidates@ll2
1111       else gl2@ll2
1112     in l1,l2
1113   in
1114   (* we now compute candidates to be applied in smart mode, splitted in
1115      facts and not facts *)
1116   let smart_candidates_facts, smart_candidates_other =
1117     if is_prod || not(smart) then [],[]
1118     else
1119     let sgl1,sgl2 = List.partition test smart_global_cands in
1120     let sll1,sll2 = List.partition test smart_local_cands in
1121     let l1 = if is_eq then [] else sgl1@sll1 in
1122     let l2 =
1123       if by && smart then given_candidates@sll2
1124       else if by then sll2
1125       else sgl2@sll2
1126     in l1,l2
1127   in
1128   candidates_facts,
1129   smart_candidates_facts,
1130   sort_candidates status context (candidates_other),
1131   sort_candidates status context (smart_candidates_other)
1132 ;;
1133
1134 let applicative_case depth signature status flags gty cache =
1135   app_counter:= !app_counter+1;
1136   let _,_,metasenv,subst,_ = status#obj in
1137   let context = ctx_of gty in
1138   let tcache = cache.facts in
1139   let is_prod, is_eq =
1140     let status, t = term_of_cic_term status gty context  in
1141     let t = NCicReduction.whd status subst context t in
1142       match t with
1143         | NCic.Prod _ -> true, false
1144         | _ -> false, NCicParamod.is_equation status metasenv subst context t
1145   in
1146   debug_print ~depth (lazy (string_of_bool is_eq));
1147   (* new *)
1148   let candidates_facts, smart_candidates_facts,
1149       candidates_other, smart_candidates_other =
1150     get_candidates ~smart:true depth
1151       flags status tcache signature gty
1152   in
1153   let sm = if is_eq || is_prod then 0 else 2 in
1154   let sm1 = if flags.last then 2 else 0 in
1155   let maxd = (depth + 1 = flags.maxdepth) in
1156   let try_candidates only_one sm acc candidates =
1157     List.fold_left
1158       (fun elems cand ->
1159          if (only_one && (elems <> [])) then elems
1160          else
1161            match try_candidate (~smart:sm)
1162              flags depth status cache.unit_eq context cand with
1163                | None -> elems
1164                | Some x -> x::elems)
1165       acc candidates
1166   in
1167   (* if the goal is the last one we stop at the first fact *)
1168   let elems = try_candidates flags.last sm [] candidates_facts in
1169   (* now we add smart_facts *)
1170   let elems = try_candidates flags.last sm elems smart_candidates_facts in
1171   (* if we are at maxdepth and the goal is not a product we are done
1172      similarly, if the goal is the last one and we already found a
1173      solution *)
1174   if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1175   else
1176     let elems = try_candidates false 2 elems candidates_other in
1177     debug_print ~depth (lazy ("not facts: try smart application"));
1178     try_candidates false 2 elems smart_candidates_other
1179 ;;
1180
1181 exception Found
1182 ;;
1183
1184 (* gty is supposed to be meta-closed *)
1185 let is_subsumed depth filter_depth status gty cache =
1186   if cache=[] then false else (
1187   debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1188   let n,h,metasenv,subst,obj = status#obj in
1189   let ctx = ctx_of gty in
1190   let _ , raw_gty = term_of_cic_term status gty ctx in
1191   let target = NCicSubstitution.lift status 1 raw_gty in
1192   (* we compute candidates using the perforated type *)
1193   let weak_gty  =
1194     match target with
1195       | NCic.Appl _
1196       | NCic.Const _
1197       | NCic.Rel _ ->
1198           let raw_weak =
1199             perforate_small status subst metasenv ctx raw_gty in
1200           let weak = mk_cic_term ctx raw_weak in
1201           debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1202           Some (weak)
1203       | _ -> None
1204   in
1205   (* candidates must only be searched w.r.t the given context *)
1206   let candidates =
1207     try
1208     let idx = List.assq ctx cache in
1209     match weak_gty with
1210       | Some weak ->
1211           Ncic_termSet.elements
1212             (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1213       |None -> []
1214     with Not_found -> []
1215   in
1216   (* this is a dirty trick: the first argument of an application is used
1217      to remember at which depth a goal failed *)
1218   let filter t =
1219     let ctx = ctx_of t in
1220     let _, src = term_of_cic_term status t ctx in
1221     match src with
1222      | NCic.Appl [NCic.Implicit (`Typeof d); t]
1223        when d <= depth -> Some (mk_cic_term ctx t)
1224      | _ -> None in
1225   let candidates =
1226     if filter_depth then HExtlib.filter_map filter candidates else candidates in
1227   debug_print ~depth
1228     (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1229     try
1230       List.iter
1231         (fun t ->
1232            let _ , source = term_of_cic_term status t ctx in
1233            let implication =
1234              NCic.Prod("foo",source,target) in
1235            let metasenv,j,_,_ =
1236              NCicMetaSubst.mk_meta
1237                metasenv ctx ~with_type:implication `IsType in
1238            let status = status#set_obj (n,h,metasenv,subst,obj) in
1239            let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1240            try
1241              let status = NTactics.intro_tac "foo" status in
1242              let status =
1243                NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1244              in
1245                if (head_goals status#stack = []) then raise Found
1246                else ()
1247            with
1248              | Error _ -> ())
1249         candidates;false
1250     with Found -> debug_print ~depth (lazy "success");true)
1251 ;;
1252
1253 let rec guess_name name ctx =
1254   if name = "_" then guess_name "auto" ctx else
1255   if not (List.mem_assoc name ctx) then name else
1256   guess_name (name^"'") ctx
1257 ;;
1258
1259 let is_prod status =
1260   let _, ctx, gty = current_goal status in
1261   let status, gty = apply_subst status ctx gty in
1262   let _, raw_gty = term_of_cic_term status gty ctx in
1263   match raw_gty with
1264     | NCic.Prod (name,src,_) ->
1265         let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1266         (match snd (term_of_cic_term status src ctx) with
1267         | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1268         | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1269             let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1270             (match itys with
1271             (* | [_,_,_,[_;_]]  con nat va, ovviamente, in loop *)
1272             | [_,_,_,[_]]
1273             | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1274             | _ -> `Some (guess_name name ctx))
1275         | _ -> `Some (guess_name name ctx))
1276     | _ -> `None
1277
1278 let intro ~depth status facts name =
1279   let status = NTactics.intro_tac name status in
1280   let _, ctx, ngty = current_goal status in
1281   let t = mk_cic_term ctx (NCic.Rel 1) in
1282   let status, keys = keys_of_term status t in
1283   let facts = List.fold_left (add_to_th t) facts keys in
1284     debug_print ~depth (lazy ("intro: "^ name));
1285   (* unprovability is not stable w.r.t introduction *)
1286   status, facts
1287 ;;
1288
1289 let rec intros_facts ~depth status facts =
1290   if List.length (head_goals status#stack) <> 1 then status, facts else
1291   match is_prod status with
1292     | `Inductive name
1293     | `Some(name) ->
1294         let status,facts =
1295           intro ~depth status facts name
1296         in intros_facts ~depth status facts
1297 (*    | `Inductive name ->
1298           let status = NTactics.case1_tac name status in
1299           intros_facts ~depth status facts *)
1300     | _ -> status, facts
1301 ;;
1302
1303 let intros ~depth status cache =
1304     match is_prod status with
1305       | `Inductive _
1306       | `Some _ ->
1307           let trace = cache.trace in
1308           let status,facts =
1309             intros_facts ~depth status cache.facts
1310           in
1311           if head_goals status#stack = [] then
1312             let status = NTactics.merge_tac status in
1313             [(0,Ast.Ident("__intros",`Ambiguous)),status], cache
1314           else
1315             (* we reindex the equation from scratch *)
1316             let unit_eq = index_local_equations status#eq_cache status in
1317             let status = NTactics.merge_tac status in
1318             [(0,Ast.Ident("__intros",`Ambiguous)),status],
1319             init_cache ~facts ~unit_eq () ~trace
1320       | _ -> [],cache
1321 ;;
1322
1323 let reduce ~whd ~depth status g =
1324   let n,h,metasenv,subst,o = status#obj in
1325   let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1326   let ty = NCicUntrusted.apply_subst status subst ctx ty in
1327   let ty' =
1328    (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1329   in
1330   if ty = ty' then []
1331   else
1332     (debug_print ~depth
1333       (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1334     let metasenv =
1335       (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1336     in
1337     let status = status#set_obj (n,h,metasenv,subst,o) in
1338     (* we merge to gain a depth level; the previous goal level should
1339        be empty *)
1340     let status = NTactics.merge_tac status in
1341     incr candidate_no;
1342     [(!candidate_no,Ast.Ident("__whd",`Ambiguous)),status])
1343 ;;
1344
1345 let do_something signature flags status g depth gty cache =
1346   let l0, cache = intros ~depth status cache in
1347   if l0 <> [] then l0, cache
1348   else
1349   (* whd *)
1350   let l = reduce ~whd:true ~depth status g in
1351   (* if l <> [] then l,cache else *)
1352   (* backward aplications *)
1353   let l1 =
1354     List.map
1355       (fun s ->
1356          incr candidate_no;
1357          ((!candidate_no,Ast.Ident("__paramod",`Ambiguous)),s))
1358       (auto_eq_check cache.unit_eq status)
1359   in
1360   let l2 =
1361     if ((l1 <> []) && flags.last) then [] else
1362     applicative_case depth signature status flags gty cache
1363   in
1364   (* statistics *)
1365   List.iter
1366     (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1367   (* states in l1 have have an empty set of subgoals: no point to sort them *)
1368   debug_print ~depth
1369     (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1370     (* we order alternatives w.r.t the number of subgoals they open *)
1371     l1 @ (sort_new_elems l2) @ l, cache
1372 ;;
1373
1374 let pp_goal = function
1375   | (_,Continuationals.Stack.Open i)
1376   | (_,Continuationals.Stack.Closed i) -> string_of_int i
1377 ;;
1378
1379 let pp_goals status l =
1380   String.concat ", "
1381     (List.map
1382        (fun i ->
1383           let gty = get_goalty status i in
1384             NTacStatus.ppterm status gty)
1385        l)
1386 ;;
1387
1388 module M =
1389   struct
1390     type t = int
1391     let compare = Pervasives.compare
1392   end
1393 ;;
1394
1395 module MS = HTopoSort.Make(M)
1396 ;;
1397
1398 let sort_tac status =
1399   let gstatus =
1400     match status#stack with
1401     | [] -> assert false
1402     | (goals, t, k, tag) :: s ->
1403         let g = head_goals status#stack in
1404         let sortedg =
1405           (List.rev (MS.topological_sort g (deps status))) in
1406           noprint (lazy ("old g = " ^
1407             String.concat "," (List.map string_of_int g)));
1408           noprint (lazy ("sorted goals = " ^
1409             String.concat "," (List.map string_of_int sortedg)));
1410           let is_it i = function
1411             | (_,Continuationals.Stack.Open j )
1412             | (_,Continuationals.Stack.Closed j ) -> i = j
1413           in
1414           let sorted_goals =
1415             List.map (fun i -> List.find (is_it i) goals) sortedg
1416           in
1417             (sorted_goals, t, k, tag) :: s
1418   in
1419    status#set_stack gstatus
1420 ;;
1421
1422 let clean_up_tac status =
1423   let gstatus =
1424     match status#stack with
1425     | [] -> assert false
1426     | (g, t, k, tag) :: s ->
1427         let is_open = function
1428           | (_,Continuationals.Stack.Open _) -> true
1429           | (_,Continuationals.Stack.Closed _) -> false
1430         in
1431         let g' = List.filter is_open g in
1432           (g', t, k, tag) :: s
1433   in
1434    status#set_stack gstatus
1435 ;;
1436
1437 let focus_tac focus status =
1438   let gstatus =
1439     match status#stack with
1440     | [] -> assert false
1441     | (g, t, k, tag) :: s ->
1442         let in_focus = function
1443           | (_,Continuationals.Stack.Open i)
1444           | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1445         in
1446         let focus,others = List.partition in_focus g
1447         in
1448           (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1449           (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1450   in
1451    status#set_stack gstatus
1452 ;;
1453
1454 let deep_focus_tac level focus status =
1455   let in_focus = function
1456     | (_,Continuationals.Stack.Open i)
1457     | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1458   in
1459   let rec slice level gs =
1460     if level = 0 then [],[],gs else
1461       match gs with
1462         | [] -> assert false
1463         | (g, t, k, tag) :: s ->
1464             let f,o,gs = slice (level-1) s in
1465             let f1,o1 = List.partition in_focus g
1466             in
1467             (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1468   in
1469   let gstatus =
1470     let f,o,s = slice level status#stack in f@o@s
1471   in
1472    status#set_stack gstatus
1473 ;;
1474
1475 let move_to_side level status =
1476 match status#stack with
1477   | [] -> assert false
1478   | (g,_,_,_)::tl ->
1479       let is_open = function
1480           | (_,Continuationals.Stack.Open i) -> Some i
1481           | (_,Continuationals.Stack.Closed _) -> None
1482         in
1483       let others = menv_closure status (stack_goals (level-1) tl) in
1484       List.for_all (fun i -> IntSet.mem i others)
1485         (HExtlib.filter_map is_open g)
1486
1487 let top_cache ~depth top status cache =
1488   if top then
1489     let unit_eq = index_local_equations status#eq_cache status in
1490     {cache with unit_eq = unit_eq}
1491   else cache
1492
1493 let rec auto_clusters ?(top=false)
1494     flags signature cache depth status : unit =
1495   debug_print ~depth (lazy ("entering auto clusters at depth " ^
1496                            (string_of_int depth)));
1497   debug_print ~depth (pptrace status cache.trace);
1498   (* ignore(Unix.select [] [] [] 0.01); *)
1499   let status = clean_up_tac status in
1500   let goals = head_goals status#stack in
1501   if goals = [] then
1502     if depth = 0 then raise (Proved (status, cache.trace))
1503     else
1504       let status = NTactics.merge_tac status in
1505         let cache =
1506         let l,tree = cache.under_inspection in
1507           match l with
1508             | [] -> cache (* possible because of intros that cleans the cache *)
1509             | a::tl -> let tree = rm_from_th a tree a in
1510               {cache with under_inspection = tl,tree}
1511         in
1512          auto_clusters flags signature cache (depth-1) status
1513   else if List.length goals < 2 then
1514     let cache = top_cache ~depth top status cache in
1515     auto_main flags signature cache depth status
1516   else
1517     let all_goals = open_goals (depth+1) status in
1518     debug_print ~depth (lazy ("goals = " ^
1519       String.concat "," (List.map string_of_int all_goals)));
1520     let classes = HExtlib.clusters (deps status) all_goals in
1521     (* if any of the classes exceed maxwidth we fail *)
1522     List.iter
1523       (fun gl ->
1524          if List.length gl > flags.maxwidth then
1525            begin
1526              debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1527              HLog.warn (sprintf "global width (%u) exceeded: %u"
1528                flags.maxwidth (List.length gl));
1529              raise (Gaveup cache.failures)
1530            end else ()) classes;
1531     if List.length classes = 1 then
1532       let flags =
1533         {flags with last = (List.length all_goals = 1)} in
1534         (* no need to cluster *)
1535       let cache = top_cache ~depth top status cache in
1536         auto_main flags signature cache depth status
1537     else
1538       let classes = if top then List.rev classes else classes in
1539       debug_print ~depth
1540         (lazy
1541            (String.concat "\n"
1542            (List.map
1543              (fun l ->
1544                ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1545            classes)));
1546       (* we now process each cluster *)
1547       let status,cache,b =
1548         List.fold_left
1549           (fun (status,cache,b) gl ->
1550              let flags =
1551                {flags with last = (List.length gl = 1)} in
1552              let lold = List.length status#stack in
1553               debug_print ~depth (lazy ("stack length = " ^
1554                         (string_of_int lold)));
1555              let fstatus = deep_focus_tac (depth+1) gl status in
1556              let cache = top_cache ~depth top fstatus cache in
1557              try
1558                debug_print ~depth (lazy ("focusing on" ^
1559                               String.concat "," (List.map string_of_int gl)));
1560                auto_main flags signature cache depth fstatus; assert false
1561              with
1562                | Proved(status,trace) ->
1563                    let status = NTactics.merge_tac status in
1564                    let cache = {cache with trace = trace} in
1565                    let lnew = List.length status#stack in
1566                      assert (lold = lnew);
1567                    (status,cache,true)
1568                | Gaveup failures when top ->
1569                    let cache = {cache with failures = failures} in
1570                    (status,cache,b)
1571           )
1572           (status,cache,false) classes
1573       in
1574       let rec final_merge n s =
1575         if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1576       in let status = final_merge depth status
1577       in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1578
1579 and
1580
1581 (* BRAND NEW VERSION *)
1582 auto_main flags signature cache depth status: unit =
1583   debug_print ~depth (lazy "entering auto main");
1584   debug_print ~depth (pptrace status cache.trace);
1585   debug_print ~depth (lazy ("stack length = " ^
1586                         (string_of_int (List.length status#stack))));
1587   (* ignore(Unix.select [] [] [] 0.01); *)
1588   let status = sort_tac (clean_up_tac status) in
1589   let goals = head_goals status#stack in
1590   match goals with
1591     | [] when depth = 0 -> raise (Proved (status,cache.trace))
1592     | []  ->
1593         let status = NTactics.merge_tac status in
1594         let cache =
1595           let l,tree = cache.under_inspection in
1596             match l with
1597               | [] -> cache (* possible because of intros that cleans the cache *)
1598               | a::tl -> let tree = rm_from_th a tree a in
1599                   {cache with under_inspection = tl,tree}
1600         in
1601           auto_clusters flags signature cache (depth-1) status
1602     | orig::_ ->
1603         if depth > 0 && move_to_side depth status
1604         then
1605           let status = NTactics.merge_tac status in
1606           let cache =
1607             let l,tree = cache.under_inspection in
1608               match l with
1609                 | [] -> cache (* possible because of intros that cleans the cache*)
1610                 | a::tl -> let tree = rm_from_th a tree a in
1611                     {cache with under_inspection = tl,tree}
1612           in
1613             auto_clusters flags signature cache (depth-1) status
1614         else
1615         let ng = List.length goals in
1616         (* moved inside auto_clusters *)
1617         if ng > flags.maxwidth then begin
1618           debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1619           HLog.warn (sprintf "local width (%u) exceeded: %u"
1620              flags.maxwidth ng);
1621           raise (Gaveup cache.failures)
1622         end else if depth = flags.maxdepth then
1623           raise (Gaveup cache.failures)
1624         else
1625         let status = NTactics.branch_tac ~force:true status in
1626         let g,gctx, gty = current_goal status in
1627         let ctx,ty = close status g in
1628         let closegty = mk_cic_term ctx ty in
1629         let status, gty = apply_subst status gctx gty in
1630         debug_print ~depth (lazy("Attacking goal " ^
1631           string_of_int g ^ " : "^ppterm status gty));
1632         debug_print ~depth (lazy ("current failures: " ^
1633           string_of_int (List.length (all_elements ctx cache.failures))));
1634         let is_eq =
1635            let _,_,metasenv,subst,_ = status#obj in
1636            NCicParamod.is_equation status metasenv subst ctx ty in
1637         (* if the goal is an equality we artificially raise its depth up to
1638            flags.maxdepth - 1 *)
1639         if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then
1640         (* for efficiency reasons, in this case we severely cripple the
1641            search depth *)
1642           (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1643            auto_main flags signature cache (depth+1) status)
1644         (* check for loops *)
1645         else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1646           (debug_print ~depth (lazy "SUBSUMED");
1647            raise (Gaveup cache.failures))
1648         (* check for failures *)
1649         else if is_subsumed depth true status closegty cache.failures then
1650           (debug_print ~depth (lazy "ALREADY MET");
1651            raise (Gaveup cache.failures))
1652         else
1653         let new_sig = height_of_goal g status in
1654         if new_sig < signature then
1655           (debug_print  ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1656            debug_print  ~depth (lazy ("olds = " ^ (string_of_int signature))));
1657         let alternatives, cache =
1658           do_something signature flags status g depth gty cache in
1659         let loop_cache =
1660           if flags.last then
1661             let l,tree = cache.under_inspection in
1662             let l,tree = closegty::l, add_to_th closegty tree closegty in
1663             {cache with under_inspection = l,tree}
1664           else cache in
1665         let failures =
1666           List.fold_left
1667           (fun allfailures ((_,t),status) ->
1668              debug_print ~depth
1669                (lazy ("(re)considering goal " ^
1670                        (string_of_int g) ^" : "^ppterm status gty));
1671              debug_print (~depth:depth)
1672                (lazy ("Case: " ^ NotationPp.pp_term status t));
1673              let depth,cache =
1674                if t=Ast.Ident("__whd",`Ambiguous) ||
1675                   t=Ast.Ident("__intros",`Ambiguous)
1676                then depth, cache
1677                else depth+1,loop_cache in
1678              let cache = add_to_trace status ~depth cache t in
1679              let cache = {cache with failures = allfailures} in
1680              try
1681                auto_clusters flags signature cache depth status;
1682                assert false;
1683              with Gaveup fail ->
1684                debug_print ~depth (lazy "Failed");
1685                fail)
1686           cache.failures alternatives in
1687         let failures =
1688           if flags.last then
1689             let newfail =
1690               let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1691               mk_cic_term ctx dty
1692             in
1693             prerr_endline ("FAILURE : " ^ ppterm status gty);
1694             add_to_th newfail failures closegty
1695           else failures in
1696         debug_print ~depth (lazy "no more candidates");
1697         raise (Gaveup failures)
1698 ;;
1699
1700 let int name l def =
1701   try int_of_string (List.assoc name l)
1702   with Failure _ | Not_found -> def
1703 ;;
1704
1705 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1706
1707 let cleanup_trace s trace =
1708   (* removing duplicates *)
1709   let trace_set =
1710     List.fold_left
1711       (fun acc t -> AstSet.add t acc)
1712       AstSet.empty trace in
1713   let trace = AstSet.elements trace_set
1714     (* filtering facts *)
1715   in List.filter
1716        (fun t ->
1717           match t with
1718             | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1719             | _ -> false) trace
1720 ;;
1721
1722 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1723   let oldstatus = status in
1724   let status = (status:> NTacStatus.tac_status) in
1725   let goals = head_goals status#stack in
1726   let status, facts = mk_th_cache status goals in
1727 (* let unit_eq = index_local_equations status#eq_cache status in *)
1728   let cache = init_cache ~facts () in
1729 (*   pp_th status facts; *)
1730 (*
1731   NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1732     debug_print (lazy(
1733       NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1734       String.concat "\n    " (List.map (
1735       status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1736         (NDiscriminationTree.TermSet.elements t))
1737       )));
1738 *)
1739   (* To allow using Rels in the user-specified candidates, we need a context
1740    * but in the case where multiple goals are open, there is no single context
1741    * to type the Rels. At this time, we require that Rels be typed in the
1742    * context of the first selected goal *)
1743   let _,ctx,_ = current_goal ~single_goal:false status in
1744   let status, candidates =
1745     match univ with
1746       | None -> status, None
1747       | Some l ->
1748           let to_Ast (st,l) t =
1749             let st, res = disambiguate st ctx t None in
1750             let st, res = term_of_cic_term st res (ctx_of res)
1751             in (st, Ast.NCic res::l)
1752           in
1753           let status, l' = List.fold_left to_Ast (status,[]) l in
1754           status, Some l'
1755   in
1756   let depth = int "depth" flags 3 in
1757   let size  = int "size" flags 10 in
1758   let width = int "width" flags 4 (* (3+List.length goals)*) in
1759   (* XXX fix sort *)
1760 (*   let goals = List.map (fun i -> (i,P)) goals in *)
1761   let signature = height_of_goals status in
1762   let flags = {
1763           last = true;
1764           candidates = candidates;
1765           maxwidth = width;
1766           maxsize = size;
1767           maxdepth = depth;
1768           timeout = Unix.gettimeofday() +. 3000.;
1769           do_types = false;
1770   } in
1771   let initial_time = Unix.gettimeofday() in
1772   app_counter:= 0;
1773   let rec up_to x y =
1774     if x > y then
1775       (debug_print(lazy
1776         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1777        debug_print(lazy
1778         ("Applicative nodes:"^string_of_int !app_counter));
1779        raise (Error (lazy "auto gave up", None)))
1780     else
1781       let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1782       let flags = { flags with maxdepth = x }
1783       in
1784         try auto_clusters (~top:true) flags signature cache 0 status;assert false
1785 (*
1786         try auto_main flags signature cache 0 status;assert false
1787 *)
1788         with
1789           | Gaveup _ -> up_to (x+1) y
1790           | Proved (s,trace) ->
1791               debug_print (lazy ("proved at depth " ^ string_of_int x));
1792               List.iter (toref incr_uses statistics) trace;
1793               let _ = debug_print (pptrace status trace) in
1794               let trace = cleanup_trace s trace in
1795               let _ = debug_print (pptrace status trace) in
1796               let stack =
1797                 match s#stack with
1798                   | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1799                   | _ -> assert false
1800               in
1801               let s = s#set_stack stack in
1802                 trace_ref := trace;
1803                 oldstatus#set_status s
1804   in
1805   let s = up_to depth depth in
1806     debug_print (print_stat status statistics);
1807     debug_print(lazy
1808         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1809     debug_print(lazy
1810         ("Applicative nodes:"^string_of_int !app_counter));
1811     s
1812 ;;
1813
1814 let auto_tac ~params:(_,flags as params) ?trace_ref =
1815   if List.mem_assoc "demod" flags then
1816     demod_tac ~params
1817   else if List.mem_assoc "paramod" flags then
1818     paramod_tac ~params
1819   else if List.mem_assoc "fast_paramod" flags then
1820     fast_eq_check_tac ~params
1821   else auto_tac ~params ?trace_ref
1822 ;;
1823
1824
1825
1826
1827
1828
1829
1830
1831
1832
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842