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