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