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