matita/components/ng_tactics/nnAuto.ml

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