matitaB/components/ng_tactics/nnAuto.ml

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