matita/components/ng_tactics/nnAuto.ml

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