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