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