matita/components/ng_tactics/nnAuto.ml

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