matitaB/components/ng_tactics/nnAuto.ml

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