helm/software/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 debug = ref true
  15 let debug_print ?(depth=0) s =
  16   if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
  17 (* let print= debug_print *)
  18  let print ?(depth=0) s =
  19   prerr_endline (String.make depth '\t'^Lazy.force s)
  20
  21 let debug_do f = if !debug then f () else ()
  22
  23 open Continuationals.Stack
  24 open NTacStatus
  25 module Ast = CicNotationPt
  26 let app_counter = ref 0
  27
  28 (* ======================= utility functions ========================= *)
  29 module IntSet = Set.Make(struct type t = int let compare = compare end)
  30
  31 let get_sgoalty status g =
  32  let _,_,metasenv,subst,_ = status#obj in
  33  try
  34    let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
  35    let ty = NCicUntrusted.apply_subst subst ctx ty in
  36    let ctx = NCicUntrusted.apply_subst_context
  37      ~fix_projections:true subst ctx
  38    in
  39      NTacStatus.mk_cic_term ctx ty
  40  with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
  41 ;;
  42
  43 let deps status g =
  44   let gty = get_sgoalty status g in
  45   metas_of_term status gty
  46 ;;
  47
  48 let menv_closure status gl =
  49   let rec closure acc = function
  50     | [] -> acc
  51     | x::l when IntSet.mem x acc -> closure acc l
  52     | x::l -> closure (IntSet.add x acc) (deps status x @ l)
  53   in closure IntSet.empty gl
  54 ;;
  55
  56 (* we call a "fact" an object whose hypothesis occurs in the goal
  57    or in types of goal-variables *)
  58 let is_a_fact status ty =
  59   let status, ty, _ = saturate ~delta:max_int status ty in
  60   let g_metas = metas_of_term status ty in
  61   let clos = menv_closure status g_metas in
  62   let _,_,metasenv,_,_ = status#obj in
  63   let menv =
  64     List.fold_left
  65       (fun acc (i,_) -> IntSet.add i acc)
  66       IntSet.empty metasenv
  67   in IntSet.equal clos menv;;
  68
  69 let is_a_fact_obj s uri =
  70   let obj = NCicEnvironment.get_checked_obj uri in
  71   match obj with
  72     | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
  73         is_a_fact s (mk_cic_term [] ty)
  74 (* aggiungere i costruttori *)
  75     | _ -> false
  76
  77 let current_goal status =
  78   let open_goals = head_goals status#stack in
  79   assert (List.length open_goals  = 1);
  80   let open_goal = List.hd open_goals in
  81   let gty = get_goalty status open_goal in
  82   let ctx = ctx_of gty in
  83     open_goal, ctx, gty
  84
  85
  86
  87 (* =============================== paramod =========================== *)
  88 let auto_paramod ~params:(l,_) status goal =
  89   let gty = get_goalty status goal in
  90   let n,h,metasenv,subst,o = status#obj in
  91   let status,t = term_of_cic_term status gty (ctx_of gty) in
  92   let status, l =
  93     List.fold_left
  94       (fun (status, l) t ->
  95         let status, t = disambiguate status (ctx_of gty) t None in
  96         let status, ty = typeof status (ctx_of t) t in
  97         let status, t =  term_of_cic_term status t (ctx_of gty) in
  98         let status, ty = term_of_cic_term status ty (ctx_of ty) in
  99         (status, (t,ty) :: l))
 100       (status,[]) l
 101   in
 102   match
 103     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
 104   with
 105   | [] -> raise (Error (lazy "no proof found",None))
 106   | (pt, metasenv, subst)::_ ->
 107       let status = status#set_obj (n,h,metasenv,subst,o) in
 108       instantiate status goal (mk_cic_term (ctx_of gty) pt)
 109 ;;
 110
 111 let auto_paramod_tac ~params status =
 112   NTactics.distribute_tac (auto_paramod ~params) status
 113 ;;
 114
 115 let fast_eq_check_all status eq_cache goal =
 116   let gty = get_goalty status goal in
 117   let ctx = ctx_of gty in
 118   let n,h,metasenv,subst,o = status#obj in
 119   let status,t = term_of_cic_term status gty ctx in
 120   let build_status (pt, metasenv, subst) =
 121     let status = status#set_obj (n,h,metasenv,subst,o) in
 122     let gty = get_goalty status goal in
 123     instantiate status goal (mk_cic_term ctx pt)
 124   in
 125     List.map build_status
 126       (NCicParamod.fast_eq_check status metasenv subst ctx
 127          eq_cache (NCic.Rel ~-1,t))
 128 ;;
 129
 130 let fast_eq_check eq_cache status goal =
 131   match fast_eq_check_all status eq_cache goal with
 132   | [] -> raise (Error (lazy "no proof found",None))
 133   | s::_ -> s
 134 ;;
 135
 136 let fast_eq_check_tac ~params s =
 137   NTactics.distribute_tac (fast_eq_check s#eq_cache) s
 138 ;;
 139
 140 let auto_eq_check eq_cache status =
 141   try
 142     let s =
 143       NTactics.distribute_tac (fast_eq_check eq_cache) status in
 144       [s]
 145   with
 146     | Error _ -> []
 147 ;;
 148
 149 (*
 150 let fast_eq_check_tac_all  ~params eq_cache status =
 151   let g,_,_ = current_goal status in
 152   let allstates = fast_eq_check_all status eq_cache g in
 153   let pseudo_low_tac s _ _ = s in
 154   let pseudo_low_tactics =
 155     List.map pseudo_low_tac allstates
 156   in
 157     List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
 158 ;;
 159 *)
 160
 161 (*************** subsumption ****************)
 162
 163 let close_wrt_context =
 164   List.fold_left
 165     (fun ty ctx_entry ->
 166         match ctx_entry with
 167        | name, NCic.Decl t -> NCic.Prod(name,t,ty)
 168        | name, NCic.Def(bo, _) -> NCicSubstitution.subst bo ty)
 169 ;;
 170
 171 let args_for_context ?(k=1) ctx =
 172   let _,args =
 173     List.fold_left
 174       (fun (n,l) ctx_entry ->
 175          match ctx_entry with
 176            | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
 177            | name, NCic.Def(bo, _) -> n+1,l)
 178       (k,[]) ctx in
 179     args
 180
 181 let constant_for_meta ctx ty i =
 182   let name = "cic:/foo"^(string_of_int i)^".con" in
 183   let uri = NUri.uri_of_string name in
 184   let ty = close_wrt_context ty ctx in
 185   (* prerr_endline (NCicPp.ppterm [] [] [] ty); *)
 186   let attr = (`Generated,`Definition,`Local) in
 187   let obj = NCic.Constant([],name,None,ty,attr) in
 188     (* Constant  of relevance * string * term option * term * c_attr *)
 189     (uri,0,[],[],obj)
 190
 191 (* not used *)
 192 let refresh metasenv =
 193   List.fold_left
 194     (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
 195        let ikind = NCicUntrusted.kind_of_meta iattr in
 196        let metasenv,j,instance,ty =
 197          NCicMetaSubst.mk_meta ~attrs:iattr
 198            metasenv ctx ~with_type:ty ikind in
 199        let s_entry = i,(iattr, ctx, instance, ty) in
 200        let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
 201          metasenv,s_entry::subst)
 202       (metasenv,[]) metasenv
 203
 204 (* close metasenv returns a ground instance of all the metas in the
 205 metasenv, insantiatied with axioms, and the list of these axioms *)
 206 let close_metasenv metasenv subst =
 207   (*
 208   let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
 209   *)
 210   let metasenv = NCicUntrusted.sort_metasenv subst metasenv in
 211     List.fold_left
 212       (fun (subst,objs) (i,(iattr,ctx,ty)) ->
 213          let ty = NCicUntrusted.apply_subst subst ctx ty in
 214          let ctx =
 215            NCicUntrusted.apply_subst_context ~fix_projections:true
 216              subst ctx in
 217          let (uri,_,_,_,obj) as okind =
 218            constant_for_meta ctx ty i in
 219          try
 220            NCicEnvironment.check_and_add_obj okind;
 221            let iref = NReference.reference_of_spec uri NReference.Decl in
 222            let iterm =
 223              let args = args_for_context ctx in
 224                if args = [] then NCic.Const iref
 225                else NCic.Appl(NCic.Const iref::args)
 226            in
 227            (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
 228            let s_entry = i, ([], ctx, iterm, ty)
 229            in s_entry::subst,okind::objs
 230          with _ -> assert false)
 231       (subst,[]) metasenv
 232 ;;
 233
 234 let ground_instances status gl =
 235   let _,_,metasenv,subst,_ = status#obj in
 236   let subset = menv_closure status gl in
 237   let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
 238 (*
 239   let submenv = metasenv in
 240 *)
 241   let subst, objs = close_metasenv submenv subst in
 242   try
 243     List.iter
 244       (fun i ->
 245          let (_, ctx, t, _) = List.assoc i subst in
 246            debug_print (lazy (NCicPp.ppterm ctx [] [] t));
 247            List.iter
 248              (fun (uri,_,_,_,_) as obj ->
 249                 NCicEnvironment.invalidate_item (`Obj (uri, obj)))
 250              objs;
 251            ())
 252       gl
 253   with
 254       Not_found -> assert false
 255   (* (ctx,t) *)
 256 ;;
 257
 258 let replace_meta i args target =
 259   let rec aux k = function
 260     (* TODO: local context *)
 261     | NCic.Meta (j,lc) when i = j ->
 262         (match args with
 263            | [] -> NCic.Rel 1
 264            | _ -> let args =
 265                List.map (NCicSubstitution.subst_meta lc) args in
 266                NCic.Appl(NCic.Rel k::args))
 267     | NCic.Meta (j,lc) as m ->
 268         (match lc with
 269            _,NCic.Irl _ -> m
 270          | n,NCic.Ctx l ->
 271             NCic.Meta
 272              (i,(0,NCic.Ctx
 273                  (List.map (fun t ->
 274                    aux k (NCicSubstitution.lift n t)) l))))
 275     | t -> NCicUtils.map (fun _ k -> k+1) k aux t
 276  in
 277    aux 1 target
 278 ;;
 279
 280 let close_wrt_metasenv subst =
 281   List.fold_left
 282     (fun ty (i,(iattr,ctx,mty)) ->
 283        let mty = NCicUntrusted.apply_subst subst ctx mty in
 284        let ctx =
 285          NCicUntrusted.apply_subst_context ~fix_projections:true
 286            subst ctx in
 287        let cty = close_wrt_context mty ctx in
 288        let name = "foo"^(string_of_int i) in
 289        let ty = NCicSubstitution.lift 1 ty in
 290        let args = args_for_context ~k:1 ctx in
 291          (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
 292        let ty = replace_meta i args ty
 293        in
 294        NCic.Prod(name,cty,ty))
 295 ;;
 296
 297 let close status g =
 298   let _,_,metasenv,subst,_ = status#obj in
 299   let subset = menv_closure status [g] in
 300   let subset = IntSet.remove g subset in
 301   let elems = IntSet.elements subset in
 302   let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
 303   let ty = NCicUntrusted.apply_subst subst ctx ty in
 304   debug_print (lazy ("metas in " ^ (NCicPp.ppterm ctx [] metasenv ty)));
 305   debug_print (lazy (String.concat ", " (List.map string_of_int elems)));
 306   let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
 307   let submenv = List.rev (NCicUntrusted.sort_metasenv subst submenv) in
 308 (*
 309     let submenv = metasenv in
 310 *)
 311   let ty = close_wrt_metasenv subst ty submenv in
 312     debug_print (lazy (NCicPp.ppterm ctx [] [] ty));
 313     ctx,ty
 314 ;;
 315
 316
 317
 318 (* =================================== auto =========================== *)
 319 (****************** AUTO ********************
 320
 321 let calculate_timeout flags =
 322     if flags.timeout = 0. then
 323       (debug_print (lazy "AUTO WITH NO TIMEOUT");
 324        {flags with timeout = infinity})
 325     else
 326       flags
 327 ;;
 328 let is_equational_case goalty flags =
 329   let ensure_equational t =
 330     if is_an_equational_goal t then true
 331     else false
 332   in
 333   (flags.use_paramod && is_an_equational_goal goalty) ||
 334   (flags.use_only_paramod && ensure_equational goalty)
 335 ;;
 336
 337 type menv = Cic.metasenv
 338 type subst = Cic.substitution
 339 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
 340 let candidate_no = ref 0;;
 341 type candidate = int * Cic.term Lazy.t
 342 type cache = AutoCache.cache
 343
 344 type fail =
 345   (* the goal (mainly for depth) and key of the goal *)
 346   goal * AutoCache.cache_key
 347 type op =
 348   (* goal has to be proved *)
 349   | D of goal
 350   (* goal has to be cached as a success obtained using candidate as the first
 351    * step *)
 352   | S of goal * AutoCache.cache_key * candidate * int
 353 type elem =
 354   (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
 355   menv * subst * int * op list * op list * fail list
 356 type status =
 357   (* list of computations that may lead to the solution: all op list will
 358    * end with the same (S(g,_)) *)
 359   elem list
 360 type auto_result =
 361   (* menv, subst, alternatives, tables, cache *)
 362   | Proved of menv * subst * elem list * AutomationCache.tables * cache
 363   | Gaveup of AutomationCache.tables * cache
 364
 365
 366 (* the status exported to the external observer *)
 367 type auto_status =
 368   (* context, (goal,candidate) list, and_list, history *)
 369   Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
 370   (int * Cic.term * int) list * Cic.term Lazy.t list
 371
 372 let d_prefix l =
 373   let rec aux acc = function
 374     | (D g)::tl -> aux (acc@[g]) tl
 375     | _ -> acc
 376   in
 377     aux [] l
 378 ;;
 379
 380 let calculate_goal_ty (goalno,_,_) s m =
 381   try
 382     let _,cc,goalty = CicUtil.lookup_meta goalno m in
 383     (* XXX applicare la subst al contesto? *)
 384     Some (cc, CicMetaSubst.apply_subst s goalty)
 385   with CicUtil.Meta_not_found i when i = goalno -> None
 386 ;;
 387
 388 let calculate_closed_goal_ty (goalno,_,_) s =
 389   try
 390     let cc,_,goalty = List.assoc goalno s in
 391     (* XXX applicare la subst al contesto? *)
 392     Some (cc, CicMetaSubst.apply_subst s goalty)
 393   with Not_found ->
 394     None
 395 ;;
 396
 397 let pp_status ctx status =
 398   if debug then
 399   let names = Utils.names_of_context ctx in
 400   let pp x =
 401     let x =
 402       ProofEngineReduction.replace
 403         ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
 404           ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
 405     in
 406     CicPp.pp x names
 407   in
 408   let string_of_do m s (gi,_,_ as g) d =
 409     match calculate_goal_ty g s m with
 410     | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
 411     | None -> Printf.sprintf "D(%d, _, %d)" gi d
 412   in
 413   let string_of_s m su k (ci,ct) gi =
 414     Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
 415   in
 416   let string_of_ol m su l =
 417     String.concat " | "
 418       (List.map
 419         (function
 420           | D (g,d,s) -> string_of_do m su (g,d,s) d
 421           | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
 422         l)
 423   in
 424   let string_of_fl m s fl =
 425     String.concat " | "
 426       (List.map (fun ((i,_,_),ty) ->
 427          Printf.sprintf "(%d, %s)" i (pp ty)) fl)
 428   in
 429   let rec aux = function
 430     | [] -> ()
 431     | (m,s,_,_,ol,fl)::tl ->
 432         Printf.eprintf "< [%s] ;;; [%s]>\n"
 433           (string_of_ol m s ol) (string_of_fl m s fl);
 434         aux tl
 435   in
 436     Printf.eprintf "-------------------------- status -------------------\n";
 437     aux status;
 438     Printf.eprintf "-----------------------------------------------------\n";
 439 ;;
 440
 441 let auto_status = ref [] ;;
 442 let auto_context = ref [];;
 443 let in_pause = ref false;;
 444 let pause b = in_pause := b;;
 445 let cond = Condition.create ();;
 446 let mutex = Mutex.create ();;
 447 let hint = ref None;;
 448 let prune_hint = ref [];;
 449
 450 let step _ = Condition.signal cond;;
 451 let give_hint n = hint := Some n;;
 452 let give_prune_hint hint =
 453   prune_hint := hint :: !prune_hint
 454 ;;
 455
 456 let check_pause _ =
 457   if !in_pause then
 458     begin
 459       Mutex.lock mutex;
 460       Condition.wait cond mutex;
 461       Mutex.unlock mutex
 462     end
 463 ;;
 464
 465 let get_auto_status _ =
 466   let status = !auto_status in
 467   let and_list,elems,last =
 468     match status with
 469     | [] -> [],[],[]
 470     | (m,s,_,don,gl,fail)::tl ->
 471         let and_list =
 472           HExtlib.filter_map
 473             (fun (id,d,_ as g) ->
 474               match calculate_goal_ty g s m with
 475               | Some (_,x) -> Some (id,x,d) | None -> None)
 476             (d_goals gl)
 477         in
 478         let rows =
 479           (* these are the S goalsin the or list *)
 480           let orlist =
 481             List.map
 482               (fun (m,s,_,don,gl,fail) ->
 483                 HExtlib.filter_map
 484                   (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
 485                   (List.rev don @ gl))
 486               status
 487           in
 488           (* this function eats id from a list l::[id,x] returning x, l *)
 489           let eat_tail_if_eq id l =
 490             let rec aux (s, l) = function
 491               | [] -> s, l
 492               | ((id1,_,_),k1,c)::tl when id = id1 ->
 493                   (match s with
 494                   | None -> aux (Some c,l) tl
 495                   | Some _ -> assert false)
 496               | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
 497             in
 498             let c, l = aux (None, []) l in
 499             c, List.rev l
 500           in
 501           let eat_in_parallel id l =
 502             let rec aux (b,eaten, new_l as acc) l =
 503               match l with
 504               | [] -> acc
 505               | l::tl ->
 506                   match eat_tail_if_eq id l with
 507                   | None, l -> aux (b@[false], eaten, new_l@[l]) tl
 508                   | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
 509             in
 510             aux ([],[],[]) l
 511           in
 512           let rec eat_all rows l =
 513             match l with
 514             | [] -> rows
 515             | elem::or_list ->
 516                 match List.rev elem with
 517                 | ((to_eat,depth,_),k,_)::next_lunch ->
 518                     let b, eaten, l = eat_in_parallel to_eat l in
 519                     let eaten = HExtlib.list_uniq eaten in
 520                     let eaten = List.rev eaten in
 521                     let b = true (* List.hd (List.rev b) *) in
 522                     let rows = rows @ [to_eat,k,b,depth,eaten] in
 523                     eat_all rows l
 524                 | [] -> eat_all rows or_list
 525           in
 526           eat_all [] (List.rev orlist)
 527         in
 528         let history =
 529           HExtlib.filter_map
 530             (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
 531             gl
 532         in
 533 (*         let rows = List.filter (fun (_,l) -> l <> []) rows in *)
 534         and_list, rows, history
 535   in
 536   !auto_context, elems, and_list, last
 537 ;;
 538
 539 (* Works if there is no dependency over proofs *)
 540 let is_a_green_cut goalty =
 541   CicUtil.is_meta_closed goalty
 542 ;;
 543 let rec first_s = function
 544   | (D _)::tl -> first_s tl
 545   | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
 546   | [] -> None
 547 ;;
 548 let list_union l1 l2 =
 549   (* TODO ottimizzare compare *)
 550   HExtlib.list_uniq (List.sort compare (l1 @ l1))
 551 ;;
 552 let rec eq_todo l1 l2 =
 553   match l1,l2 with
 554   | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
 555   | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
 556     when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
 557       if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
 558   | [],[] -> true
 559   | _ -> false
 560 ;;
 561 let eat_head todo id fl orlist =
 562   let rec aux acc = function
 563   | [] -> [], acc
 564   | (m, s, _, _, todo1, fl1)::tl as orlist ->
 565       let rec aux1 todo1 =
 566         match first_s todo1 with
 567         | None -> orlist, acc
 568         | Some (((gno,_,_),_,_,_), todo11) ->
 569             (* TODO confronto tra todo da ottimizzare *)
 570             if gno = id && eq_todo todo11 todo then
 571               aux (list_union fl1 acc) tl
 572             else
 573               aux1 todo11
 574       in
 575        aux1 todo1
 576   in
 577     aux fl orlist
 578 ;;
 579 let close_proof p ty menv context =
 580   let metas =
 581     List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
 582   in
 583   let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
 584   naif_closure p menv context
 585 ;;
 586 (* XXX capire bene quando aggiungere alla cache *)
 587 let add_to_cache_and_del_from_orlist_if_green_cut
 588   g s m cache key todo orlist fl ctx size minsize
 589 =
 590   let cache = cache_remove_underinspection cache key in
 591   (* prima per fare la irl usavamo il contesto vero e proprio e non quello
 592    * canonico! XXX *)
 593   match calculate_closed_goal_ty g s with
 594   | None -> assert false
 595   | Some (canonical_ctx , gty) ->
 596       let goalno,depth,sort = g in
 597       let irl = mk_irl canonical_ctx in
 598       let goal = Cic.Meta(goalno, irl) in
 599       let proof = CicMetaSubst.apply_subst s goal in
 600       let green_proof, closed_proof =
 601         let b = is_a_green_cut proof in
 602         if not b then
 603           b, (* close_proof proof gty m ctx *) proof
 604         else
 605           b, proof
 606       in
 607       debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
 608       if is_a_green_cut key then
 609         (* if the initia goal was closed, we cut alternatives *)
 610         let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
 611         let orlist, fl = eat_head todo goalno fl orlist in
 612         let cache =
 613           if size < minsize then
 614             (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
 615           else
 616           (* if the proof is closed we cache it *)
 617           if green_proof then cache_add_success cache key proof
 618           else (* cache_add_success cache key closed_proof *)
 619             (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
 620         in
 621         cache, orlist, fl, true
 622       else
 623         let cache =
 624           debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
 625           if size < minsize then
 626             (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
 627           (* if the substituted goal and the proof are closed we cache it *)
 628           if is_a_green_cut gty then
 629             if green_proof then cache_add_success cache gty proof
 630             else (* cache_add_success cache gty closed_proof *)
 631               (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
 632           else (*
 633             try
 634               let ty, _ =
 635                 CicTypeChecker.type_of_aux' ~subst:s
 636                   m ctx closed_proof CicUniv.oblivion_ugraph
 637               in
 638               if is_a_green_cut ty then
 639                 cache_add_success cache ty closed_proof
 640               else cache
 641             with
 642             | CicTypeChecker.TypeCheckerFailure _ ->*)
 643           (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
 644         in
 645         cache, orlist, fl, false
 646 ;;
 647 let close_failures (fl : fail list) (cache : cache) =
 648   List.fold_left
 649     (fun cache ((gno,depth,_),gty) ->
 650       if CicUtil.is_meta_closed gty then
 651        ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
 652          cache_add_failure cache gty depth)
 653       else
 654          cache)
 655     cache fl
 656 ;;
 657 let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
 658   let entry = goalno, (canonical_ctx, t,ty) in
 659   assert_subst_are_disjoint subst [entry];
 660   let subst = entry :: subst in
 661
 662   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
 663
 664   subst, metasenv
 665 ;;
 666
 667 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
 668   None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
 669 ;;
 670
 671 let equational_case
 672   tables cache depth fake_proof goalno goalty subst context
 673     flags
 674 =
 675   let active,passive,bag = tables in
 676   let ppterm = ppterm context in
 677   let status = (fake_proof,goalno) in
 678     if flags.use_only_paramod then
 679       begin
 680         debug_print (lazy ("PARAMODULATION SU: " ^
 681                          string_of_int goalno ^ " " ^ ppterm goalty ));
 682         let goal_steps, saturation_steps, timeout =
 683           max_int,max_int,flags.timeout
 684         in
 685         match
 686           Saturation.given_clause bag status active passive
 687             goal_steps saturation_steps timeout
 688         with
 689           | None, active, passive, bag ->
 690               [], (active,passive,bag), cache, flags
 691           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
 692             passive,bag ->
 693               assert_subst_are_disjoint subst subst';
 694               let subst = subst@subst' in
 695               let open_goals =
 696                 order_new_goals metasenv subst open_goals ppterm
 697               in
 698               let open_goals =
 699                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 700               in
 701               incr candidate_no;
 702               [(!candidate_no,proof),metasenv,subst,open_goals],
 703                 (active,passive,bag), cache, flags
 704       end
 705     else
 706       begin
 707         debug_print (lazy ("NARROWING DEL GOAL: " ^
 708                          string_of_int goalno ^ " " ^ ppterm goalty ));
 709         let goal_steps, saturation_steps, timeout =
 710           1,0,flags.timeout
 711         in
 712         match
 713           Saturation.solve_narrowing bag status active passive goal_steps
 714         with
 715           | None, active, passive, bag ->
 716               [], (active,passive,bag), cache, flags
 717           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
 718             passive,bag ->
 719               assert_subst_are_disjoint subst subst';
 720               let subst = subst@subst' in
 721               let open_goals =
 722                 order_new_goals metasenv subst open_goals ppterm
 723               in
 724               let open_goals =
 725                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 726               in
 727               incr candidate_no;
 728               [(!candidate_no,proof),metasenv,subst,open_goals],
 729                 (active,passive,bag), cache, flags
 730       end
 731 (*
 732       begin
 733         let params = ([],["use_context","false"]) in
 734         let automation_cache = {
 735               AutomationCache.tables = tables ;
 736               AutomationCache.univ = Universe.empty; }
 737         in
 738         try
 739           let ((_,metasenv,subst,_,_,_),open_goals) =
 740
 741             solve_rewrite ~params ~automation_cache
 742               (fake_proof, goalno)
 743           in
 744           let proof = lazy (Cic.Meta (-1,[])) in
 745           [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
 746         with ProofEngineTypes.Fail _ -> [], tables, cache, flags
 747 (*
 748         let res = Saturation.all_subsumed bag status active passive in
 749         let res' =
 750           List.map
 751             (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
 752                assert_subst_are_disjoint subst subst';
 753                let subst = subst@subst' in
 754                let open_goals =
 755                  order_new_goals metasenv subst open_goals ppterm
 756                in
 757                let open_goals =
 758                  List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 759                in
 760                incr candidate_no;
 761                  (!candidate_no,proof),metasenv,subst,open_goals)
 762             res
 763           in
 764           res', (active,passive,bag), cache, flags
 765 *)
 766       end
 767 *)
 768 ;;
 769
 770 let sort_new_elems =
 771  List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
 772          let p1 = List.length (prop_only l1) in
 773          let p2 = List.length (prop_only l2) in
 774          if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
 775 ;;
 776
 777
 778 let try_candidate dbd
 779   goalty tables subst fake_proof goalno depth context cand
 780 =
 781   let ppterm = ppterm context in
 782   try
 783     let actives, passives, bag = tables in
 784     let (_,metasenv,subst,_,_,_), open_goals =
 785        ProofEngineTypes.apply_tactic
 786         (PrimitiveTactics.apply_tac ~term:cand)
 787         (fake_proof,goalno)
 788     in
 789     let tables = actives, passives,
 790       Equality.push_maxmeta bag
 791         (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
 792     in
 793     debug_print (lazy ("   OK: " ^ ppterm cand));
 794     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
 795     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 796     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 797     incr candidate_no;
 798     Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
 799   with
 800     | ProofEngineTypes.Fail s -> None,tables
 801     | CicUnification.Uncertain s ->  None,tables
 802 ;;
 803
 804 let applicative_case dbd
 805   tables depth subst fake_proof goalno goalty metasenv context
 806   signature universe cache flags
 807 =
 808   (* let goalty_aux =
 809     match goalty with
 810     | Cic.Appl (hd::tl) ->
 811         Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
 812     | _ -> goalty
 813   in *)
 814   let goalty_aux = goalty in
 815   let candidates =
 816     get_candidates flags.skip_trie_filtering universe cache goalty_aux
 817   in
 818   (* if the goal is an equality we skip the congruence theorems
 819   let candidates =
 820     if is_equational_case goalty flags
 821     then List.filter not_default_eq_term candidates
 822     else candidates
 823   in *)
 824   let candidates = List.filter (only signature context metasenv) candidates
 825   in
 826   let tables, elems =
 827     List.fold_left
 828       (fun (tables,elems) cand ->
 829         match
 830           try_candidate dbd goalty
 831             tables subst fake_proof goalno depth context cand
 832         with
 833         | None, tables -> tables, elems
 834         | Some x, tables -> tables, x::elems)
 835       (tables,[]) candidates
 836   in
 837   let elems = sort_new_elems elems in
 838   elems, tables, cache
 839 ;;
 840
 841 let try_smart_candidate dbd
 842   goalty tables subst fake_proof goalno depth context cand
 843 =
 844   let ppterm = ppterm context in
 845   try
 846     let params = ([],[]) in
 847     let automation_cache = {
 848           AutomationCache.tables = tables ;
 849           AutomationCache.univ = Universe.empty; }
 850     in
 851     debug_print (lazy ("candidato per " ^ string_of_int goalno
 852       ^ ": " ^ CicPp.ppterm cand));
 853 (*
 854     let (_,metasenv,subst,_,_,_) = fake_proof in
 855     prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
 856     prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
 857 *)
 858     let ((_,metasenv,subst,_,_,_),open_goals) =
 859       apply_smart ~dbd ~term:cand ~params ~automation_cache
 860         (fake_proof, goalno)
 861     in
 862     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
 863     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 864     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 865     incr candidate_no;
 866     Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
 867   with
 868   | ProofEngineTypes.Fail s -> None,tables
 869   | CicUnification.Uncertain s ->  None,tables
 870 ;;
 871
 872 let smart_applicative_case dbd
 873   tables depth subst fake_proof goalno goalty metasenv context signature
 874   universe cache flags
 875 =
 876   let goalty_aux =
 877     match goalty with
 878     | Cic.Appl (hd::tl) ->
 879         Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
 880     | _ -> goalty
 881   in
 882   let smart_candidates =
 883     get_candidates flags.skip_trie_filtering universe cache goalty_aux
 884   in
 885   let candidates =
 886     get_candidates flags.skip_trie_filtering universe cache goalty
 887   in
 888   let smart_candidates =
 889     List.filter
 890       (fun x -> not(List.mem x candidates)) smart_candidates
 891   in
 892   let debug_msg =
 893     (lazy ("smart_candidates" ^ " = " ^
 894              (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
 895   debug_print debug_msg;
 896   let candidates = List.filter (only signature context metasenv) candidates in
 897   let smart_candidates =
 898     List.filter (only signature context metasenv) smart_candidates
 899   in
 900 (*
 901   let penalty cand depth =
 902     if only signature context metasenv cand then depth else ((prerr_endline (
 903     "penalizzo " ^ CicPp.ppterm cand));depth -1)
 904   in
 905 *)
 906   let tables, elems =
 907     List.fold_left
 908       (fun (tables,elems) cand ->
 909         match
 910           try_candidate dbd goalty
 911             tables subst fake_proof goalno depth context cand
 912         with
 913         | None, tables ->
 914             (* if normal application fails we try to be smart *)
 915             (match try_smart_candidate dbd goalty
 916                tables subst fake_proof goalno depth context cand
 917              with
 918                | None, tables -> tables, elems
 919                | Some x, tables -> tables, x::elems)
 920         | Some x, tables -> tables, x::elems)
 921       (tables,[]) candidates
 922   in
 923   let tables, smart_elems =
 924       List.fold_left
 925         (fun (tables,elems) cand ->
 926           match
 927             try_smart_candidate dbd goalty
 928               tables subst fake_proof goalno depth context cand
 929           with
 930           | None, tables -> tables, elems
 931           | Some x, tables -> tables, x::elems)
 932         (tables,[]) smart_candidates
 933   in
 934   let elems = sort_new_elems (elems @ smart_elems) in
 935   elems, tables, cache
 936 ;;
 937
 938 let equational_and_applicative_case dbd
 939   signature universe flags m s g gty tables cache context
 940 =
 941   let goalno, depth, sort = g in
 942   let fake_proof = mk_fake_proof m s g gty context in
 943   if is_equational_case gty flags then
 944     let elems,tables,cache, flags =
 945       equational_case tables cache
 946         depth fake_proof goalno gty s context flags
 947     in
 948     let more_elems, tables, cache =
 949       if flags.use_only_paramod then
 950         [],tables, cache
 951       else
 952         applicative_case dbd
 953           tables depth s fake_proof goalno
 954             gty m context signature universe cache flags
 955     in
 956       elems@more_elems, tables, cache, flags
 957   else
 958     let elems, tables, cache =
 959       match LibraryObjects.eq_URI () with
 960       | Some _ ->
 961          smart_applicative_case dbd tables depth s fake_proof goalno
 962            gty m context signature universe cache flags
 963       | None ->
 964          applicative_case dbd tables depth s fake_proof goalno
 965            gty m context signature universe cache flags
 966     in
 967       elems, tables, cache, flags
 968 ;;
 969 let rec condition_for_hint i = function
 970   | [] -> false
 971   | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
 972   | _::tl -> condition_for_hint i tl
 973 ;;
 974 let prunable_for_size flags s m todo =
 975   let rec aux b = function
 976     | (S _)::tl -> aux b tl
 977     | (D (_,_,T))::tl -> aux b tl
 978     | (D g)::tl ->
 979         (match calculate_goal_ty g s m with
 980           | None -> aux b tl
 981           | Some (canonical_ctx, gty) ->
 982             let gsize, _ =
 983               Utils.weight_of_term
 984                 ~consider_metas:false ~count_metas_occurrences:true gty in
 985             let newb = b || gsize > flags.maxgoalsizefactor in
 986             aux newb tl)
 987     | [] -> b
 988   in
 989     aux false todo
 990
 991 (*
 992 let prunable ty todo =
 993   let rec aux b = function
 994     | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
 995     | (D (_,_,T))::tl -> aux b tl
 996     | D _::_ -> false
 997     | [] -> b
 998   in
 999     aux false todo
1000 ;;
1001 *)
1002
1003 let prunable menv subst ty todo =
1004   let rec aux = function
1005     | (S(_,k,_,_))::tl ->
1006          (match Equality.meta_convertibility_subst k ty menv with
1007           | None -> aux tl
1008           | Some variant ->
1009                no_progress variant tl (* || aux tl*))
1010     | (D (_,_,T))::tl -> aux tl
1011     | _ -> false
1012   and no_progress variant = function
1013     | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
1014     | D ((n,_,P) as g)::tl ->
1015         (match calculate_goal_ty g subst menv with
1016            | None -> no_progress variant tl
1017            | Some (_, gty) ->
1018                (match calculate_goal_ty g variant menv with
1019                   | None -> assert false
1020                   | Some (_, gty') ->
1021                       if gty = gty' then no_progress variant tl
1022 (*
1023 (prerr_endline (string_of_int n);
1024  prerr_endline (CicPp.ppterm gty);
1025  prerr_endline (CicPp.ppterm gty');
1026  prerr_endline "---------- subst";
1027  prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
1028  prerr_endline "---------- variant";
1029  prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
1030  prerr_endline "---------- menv";
1031  prerr_endline (CicMetaSubst.ppmetasenv [] menv);
1032                          no_progress variant tl) *)
1033                       else false))
1034     | _::tl -> no_progress variant tl
1035   in
1036     aux todo
1037
1038 ;;
1039 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
1040   let s =
1041     HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
1042   in
1043   List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
1044 ;;
1045 let filter_prune_hint c l =
1046   let prune = !prune_hint in
1047   prune_hint := []; (* possible race... *)
1048   if prune = [] then c,l
1049   else
1050     cache_reset_underinspection c,
1051     List.filter (condition_for_prune_hint prune) l
1052 ;;
1053
1054
1055
1056 let
1057   auto_all_solutions dbd tables universe cache context metasenv gl flags
1058 =
1059   let signature =
1060     List.fold_left
1061       (fun set g ->
1062          MetadataConstraints.UriManagerSet.union set
1063              (MetadataQuery.signature_of metasenv g)
1064        )
1065       MetadataConstraints.UriManagerSet.empty gl
1066   in
1067   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1068   let goals =
1069     List.map
1070       (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1071   in
1072   let elems = [metasenv,[],1,[],goals,[]] in
1073   let rec aux tables solutions cache elems flags =
1074     match auto_main dbd tables context flags signature universe cache elems with
1075     | Gaveup (tables,cache) ->
1076         solutions,cache, tables
1077     | Proved (metasenv,subst,others,tables,cache) ->
1078         if Unix.gettimeofday () > flags.timeout then
1079           ((subst,metasenv)::solutions), cache, tables
1080         else
1081           aux tables ((subst,metasenv)::solutions) cache others flags
1082   in
1083   let rc = aux tables [] cache elems flags in
1084     match rc with
1085     | [],cache,tables -> [],cache,tables
1086     | solutions, cache,tables ->
1087         let solutions =
1088           HExtlib.filter_map
1089             (fun (subst,newmetasenv) ->
1090               let opened =
1091                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1092               in
1093               if opened = [] then Some subst else None)
1094             solutions
1095         in
1096          solutions,cache,tables
1097 ;;
1098
1099 (******************* AUTO ***************)
1100
1101
1102 let auto dbd flags metasenv tables universe cache context metasenv gl =
1103   let initial_time = Unix.gettimeofday() in
1104   let signature =
1105     List.fold_left
1106       (fun set g ->
1107          MetadataConstraints.UriManagerSet.union set
1108              (MetadataQuery.signature_of metasenv g)
1109        )
1110       MetadataConstraints.UriManagerSet.empty gl
1111   in
1112   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1113   let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1114   let elems = [metasenv,[],1,[],goals,[]] in
1115   match auto_main dbd tables context flags signature universe cache elems with
1116   | Proved (metasenv,subst,_, tables,cache) ->
1117       debug_print(lazy
1118         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1119       Some (subst,metasenv), cache
1120   | Gaveup (tables,cache) ->
1121       debug_print(lazy
1122         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1123       None,cache
1124 ;;
1125
1126 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
1127   let flags = flags_of_params params () in
1128   let use_library = flags.use_library in
1129   let universe, tables, cache =
1130     init_cache_and_tables
1131      ~dbd ~use_library ~use_context:(not flags.skip_context)
1132      automation_cache univ (proof, goal)
1133   in
1134   let _,metasenv,subst,_,_, _ = proof in
1135   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1136   let signature = MetadataQuery.signature_of metasenv goal in
1137   let signature =
1138     List.fold_left
1139       (fun set t ->
1140          let ty, _ =
1141            CicTypeChecker.type_of_aux' metasenv context t
1142              CicUniv.oblivion_ugraph
1143          in
1144          MetadataConstraints.UriManagerSet.union set
1145            (MetadataConstraints.constants_of ty)
1146        )
1147       signature univ
1148   in
1149   let tables,cache =
1150     if flags.close_more then
1151       close_more
1152         tables context (proof, goal)
1153           (auto_all_solutions dbd) signature universe cache
1154     else tables,cache in
1155   let initial_time = Unix.gettimeofday() in
1156   let (_,oldmetasenv,_,_,_, _) = proof in
1157     hint := None;
1158   let elem =
1159     metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
1160   in
1161   match auto_main dbd tables context flags signature universe cache [elem] with
1162     | Proved (metasenv,subst,_, tables,cache) ->
1163         debug_print (lazy
1164           ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1165         let proof,metasenv =
1166         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1167           proof goal subst metasenv
1168         in
1169         let opened =
1170           ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1171             ~newmetasenv:metasenv
1172         in
1173           proof,opened
1174     | Gaveup (tables,cache) ->
1175         debug_print
1176           (lazy ("TIME:"^
1177             string_of_float(Unix.gettimeofday()-.initial_time)));
1178         raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1179 ;;
1180 *)
1181
1182 (****************** types **************)
1183
1184
1185 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
1186
1187 let keys_of_term status t =
1188   let status, orig_ty = typeof status (ctx_of t) t in
1189   let _, ty, _ = saturate ~delta:max_int status orig_ty in
1190   let keys = [ty] in
1191   let keys =
1192     let _, ty = term_of_cic_term status ty (ctx_of ty) in
1193     match ty with
1194     | NCic.Const (NReference.Ref (_,NReference.Def h))
1195     | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_)
1196        when h > 0 ->
1197          let _,ty,_= saturate status ~delta:(h-1) orig_ty in
1198          ty::keys
1199     | _ -> keys
1200   in
1201   status, keys
1202 ;;
1203
1204 let mk_th_cache status gl =
1205   List.fold_left
1206     (fun (status, acc) g ->
1207        let gty = get_goalty status g in
1208        let ctx = ctx_of gty in
1209        debug_print(lazy("th cache for: "^ppterm status gty));
1210        debug_print(lazy("th cache in: "^ppcontext status ctx));
1211        if List.mem_assq ctx acc then status, acc else
1212          let idx = InvRelDiscriminationTree.empty in
1213          let status,_,idx =
1214            List.fold_left
1215              (fun (status, i, idx) _ ->
1216                 let t = mk_cic_term ctx (NCic.Rel i) in
1217                 debug_print(lazy("indexing: "^ppterm status t));
1218                 let status, keys = keys_of_term status t in
1219                 let idx =
1220                   List.fold_left (fun idx k ->
1221                     InvRelDiscriminationTree.index idx k t) idx keys
1222                 in
1223                 status, i+1, idx)
1224              (status, 1, idx) ctx
1225           in
1226          status, (ctx, idx) :: acc)
1227     (status,[]) gl
1228 ;;
1229
1230 let add_to_th t c ty =
1231   let key_c = ctx_of t in
1232   if not (List.mem_assq key_c c) then
1233       (key_c ,InvRelDiscriminationTree.index
1234                InvRelDiscriminationTree.empty ty t ) :: c
1235   else
1236     let rec replace = function
1237       | [] -> []
1238       | (x, idx) :: tl when x == key_c ->
1239           (x, InvRelDiscriminationTree.index idx ty t) :: tl
1240       | x :: tl -> x :: replace tl
1241     in
1242       replace c
1243 ;;
1244
1245 let pp_idx status idx =
1246    InvRelDiscriminationTree.iter idx
1247       (fun k set ->
1248          debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
1249          Ncic_termSet.iter
1250            (fun t -> debug_print(lazy("\t"^ppterm status t)))
1251            set)
1252 ;;
1253
1254 let pp_th status =
1255   List.iter
1256     (fun ctx, idx ->
1257        debug_print(lazy( "-----------------------------------------------"));
1258        debug_print(lazy( (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx)));
1259        debug_print(lazy( "||====>  "));
1260        pp_idx status idx)
1261 ;;
1262
1263 let search_in_th gty th =
1264   let c = ctx_of gty in
1265   let rec aux acc = function
1266    | [] -> Ncic_termSet.elements acc
1267    | (_::tl) as k ->
1268        try
1269          let idx = List.assq k th in
1270          let acc = Ncic_termSet.union acc
1271            (InvRelDiscriminationTree.retrieve_unifiables idx gty)
1272          in
1273          aux acc tl
1274        with Not_found -> aux acc tl
1275   in
1276     aux Ncic_termSet.empty c
1277 ;;
1278
1279 type flags = {
1280         do_types : bool; (* solve goals in Type *)
1281         maxwidth : int;
1282         maxsize  : int;
1283         maxdepth : int;
1284         timeout  : float;
1285 }
1286
1287 type cache =
1288     {facts : th_cache; (* positive results *)
1289      under_inspection : th_cache; (* to prune looping *)
1290      unit_eq : NCicParamod.state
1291     }
1292
1293 type sort = T | P
1294 type goal = int * sort (* goal, depth, sort *)
1295 type fail = goal * cic_term
1296 type candidate = int * Ast.term (* unique candidate number, candidate *)
1297
1298 exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
1299                                 atoms of the input goals *)
1300 exception Proved of #NTacStatus.tac_status
1301
1302 (* let close_failures _ c = c;; *)
1303 (* let prunable _ _ _ = false;; *)
1304 (* let cache_examine cache gty = `Notfound;; *)
1305 (* let put_in_subst s _ _ _  = s;; *)
1306 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
1307 (* let cache_add_underinspection c _ _ = c;; *)
1308
1309 let init_cache ?(facts=[]) ?(under_inspection=[])
1310     ?(unit_eq=NCicParamod.empty_state) _ =
1311     {facts = facts;
1312      under_inspection = under_inspection;
1313      unit_eq = unit_eq
1314     }
1315
1316 let only _ _ _ = true;;
1317
1318 let candidate_no = ref 0;;
1319
1320 let openg_no status = List.length (head_goals status#stack)
1321
1322 let sort_new_elems l =
1323   List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
1324
1325 let try_candidate flags depth status t =
1326  try
1327    debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
1328    let status = NTactics.apply_tac ("",0,t) status in
1329    let og_no = openg_no status in
1330    if og_no > flags.maxwidth ||
1331       (depth = flags.maxdepth && og_no <> 0) then
1332       (debug_print ~depth (lazy "pruned immediately"); None)
1333    else
1334      (incr candidate_no;
1335       Some ((!candidate_no,t),status))
1336  with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1337 ;;
1338
1339 let get_candidates status cache signature gty =
1340   let universe = status#auto_cache in
1341   let context = ctx_of gty in
1342   let _, raw_gty = term_of_cic_term status gty context in
1343   let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1344         universe raw_gty
1345   in
1346   let cands =
1347     List.filter (only signature context)
1348       (NDiscriminationTree.TermSet.elements cands)
1349   in
1350   List.map (fun t ->
1351      let _status, t = term_of_cic_term status t context in Ast.NCic t)
1352      (search_in_th gty cache)
1353   @
1354   List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
1355 ;;
1356
1357 let applicative_case depth signature status flags gty (cache:cache) =
1358   let tcache = cache.facts in
1359   app_counter:= !app_counter+1;
1360   let candidates = get_candidates status tcache signature gty in
1361   debug_print ~depth
1362     (lazy ("candidates: " ^ string_of_int (List.length candidates)));
1363   let elems =
1364     List.fold_left
1365       (fun elems cand ->
1366         match try_candidate flags depth status cand with
1367         | None -> elems
1368         | Some x -> x::elems)
1369       [] candidates
1370   in
1371   elems
1372 ;;
1373
1374 exception Found
1375 ;;
1376
1377 (* gty is supposed to be meta-closed *)
1378 let is_subsumed depth status gty cache =
1379   if cache=[] then false else (
1380   debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1381   let n,h,metasenv,subst,obj = status#obj in
1382   let ctx = ctx_of gty in
1383   let _ , target = term_of_cic_term status gty ctx in
1384   let target = NCicSubstitution.lift 1 target in
1385   (* candidates must only be searched w.r.t the given context *)
1386   let candidates =
1387     try
1388     let idx = List.assq ctx cache in
1389       Ncic_termSet.elements
1390         (InvRelDiscriminationTree.retrieve_generalizations idx gty)
1391     with Not_found -> []
1392   in
1393   debug_print ~depth
1394     (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1395     try
1396       List.iter
1397         (fun t ->
1398            let _ , source = term_of_cic_term status t ctx in
1399            let implication =
1400              NCic.Prod("foo",source,target) in
1401            let metasenv,j,_,_ =
1402              NCicMetaSubst.mk_meta
1403                metasenv ctx ~with_type:implication `IsType in
1404            let status = status#set_obj (n,h,metasenv,subst,obj) in
1405            let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1406            try
1407              let status = NTactics.intro_tac "foo" status in
1408              let status =
1409                NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1410              in
1411                if (head_goals status#stack = []) then raise Found
1412                else ()
1413            with
1414              | Error _ -> ())
1415         candidates;false
1416     with Found -> debug_print ~depth (lazy "success");true)
1417 ;;
1418
1419 (* warning: ctx is supposed to be already instantiated w.r.t subst *)
1420 let index_local_equations eq_cache status =
1421   let open_goals = head_goals status#stack in
1422   assert (List.length open_goals  = 1);
1423   let open_goal = List.hd open_goals in
1424   let ngty = get_goalty status open_goal in
1425   let ctx = ctx_of ngty in
1426   let c = ref 0 in
1427   List.fold_left
1428     (fun eq_cache _ ->
1429        c:= !c+1;
1430        let t = NCic.Rel !c in
1431          try
1432            let ty = NCicTypeChecker.typeof [] [] ctx t in
1433              prerr_endline ("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty));
1434              NCicParamod.forward_infer_step eq_cache t ty
1435          with
1436            | NCicTypeChecker.TypeCheckerFailure _
1437            | NCicTypeChecker.AssertFailure _ -> eq_cache)
1438     eq_cache ctx
1439 ;;
1440
1441 let rec guess_name name ctx =
1442   if name = "_" then guess_name "auto" ctx else
1443   if not (List.mem_assoc name ctx) then name else
1444   guess_name (name^"'") ctx
1445 ;;
1446
1447 let is_prod status =
1448   let _, ctx, gty = current_goal status in
1449   let _, raw_gty = term_of_cic_term status gty ctx in
1450   match raw_gty with
1451     | NCic.Prod (name,_,_) -> Some (guess_name name ctx)
1452     | _ -> None
1453
1454 let intro ~depth status facts name =
1455   let status = NTactics.intro_tac name status in
1456   let _, ctx, ngty = current_goal status in
1457   let t = mk_cic_term ctx (NCic.Rel 1) in
1458   let status, keys = keys_of_term status t in
1459   let facts = List.fold_left (add_to_th t) facts keys in
1460     debug_print ~depth (lazy ("intro: "^ name));
1461   (* unprovability is not stable w.r.t introduction *)
1462   status, facts
1463 ;;
1464
1465 let rec intros_facts ~depth status facts =
1466   match is_prod status with
1467     | Some(name) ->
1468         let status,facts =
1469           intro ~depth status facts name
1470         in intros_facts ~depth status facts
1471     | _ -> status, facts
1472 ;;
1473
1474 let rec intros ~depth status (cache:cache) =
1475     match is_prod status with
1476       | Some _ ->
1477           prerr_endline "is prod";
1478           let status,facts =
1479             intros_facts ~depth status cache.facts
1480           in
1481             (* we reindex the equation from scratch *)
1482           let unit_eq =
1483             index_local_equations status#eq_cache status in
1484             (* under_inspection must be set to empty *)
1485           status, init_cache ~facts ~unit_eq ()
1486       | _ -> status, cache
1487 ;;
1488
1489 let reduce ~depth status g =
1490   let n,h,metasenv,subst,o = status#obj in
1491   let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1492   let ty = NCicUntrusted.apply_subst subst ctx ty in
1493   let ty' = NCicReduction.whd ~subst ctx ty in
1494   if ty = ty' then []
1495   else
1496     (debug_print ~depth
1497       (lazy ("reduced to: "^ NCicPp.ppterm ctx subst metasenv ty'));
1498     let metasenv =
1499       (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1500     in
1501     let status = status#set_obj (n,h,metasenv,subst,o) in
1502     incr candidate_no;
1503     [(!candidate_no,Ast.Ident("__whd",None)),status])
1504 ;;
1505
1506 let do_something signature flags status g depth gty cache =
1507   (* whd *)
1508   let l = reduce ~depth status g in
1509   (* backward aplications *)
1510   let l1 = applicative_case depth signature status flags gty cache in
1511   (* fast paramodulation *)
1512   let l2 =
1513     List.map
1514       (fun s ->
1515          incr candidate_no;
1516          ((!candidate_no,Ast.Ident("__paramod",None)),s))
1517       (auto_eq_check cache.unit_eq status)
1518   (* states in l2 have have an set of subgoals: no point to sort them *)
1519   in
1520     l2 @ (sort_new_elems (l@l1)), cache
1521 ;;
1522
1523 let pp_goal = function
1524   | (_,Continuationals.Stack.Open i)
1525   | (_,Continuationals.Stack.Closed i) -> string_of_int i
1526 ;;
1527
1528 let pp_goals status l =
1529   String.concat ", "
1530     (List.map
1531        (fun i ->
1532           let gty = get_goalty status i in
1533             NTacStatus.ppterm status gty)
1534        l)
1535 ;;
1536
1537 module M =
1538   struct
1539     type t = int
1540     let compare = Pervasives.compare
1541   end
1542 ;;
1543
1544 module MS = HTopoSort.Make(M)
1545 ;;
1546
1547 let sort_tac status =
1548   let gstatus =
1549     match status#stack with
1550     | [] -> assert false
1551     | (goals, t, k, tag) :: s ->
1552         let g = head_goals status#stack in
1553         let sortedg =
1554           (List.rev (MS.topological_sort g (deps status))) in
1555           debug_print (lazy ("old g = " ^
1556             String.concat "," (List.map string_of_int g)));
1557           debug_print (lazy ("sorted goals = " ^
1558             String.concat "," (List.map string_of_int sortedg)));
1559           let is_it i = function
1560             | (_,Continuationals.Stack.Open j )
1561             | (_,Continuationals.Stack.Closed j ) -> i = j
1562           in
1563           let sorted_goals =
1564             List.map (fun i -> List.find (is_it i) goals) sortedg
1565           in
1566             (sorted_goals, t, k, tag) :: s
1567   in
1568    status#set_stack gstatus
1569 ;;
1570
1571 let clean_up_tac status =
1572   let gstatus =
1573     match status#stack with
1574     | [] -> assert false
1575     | (g, t, k, tag) :: s ->
1576         let is_open = function
1577           | (_,Continuationals.Stack.Open _) -> true
1578           | (_,Continuationals.Stack.Closed _) -> false
1579         in
1580         let g' = List.filter is_open g in
1581           (g', t, k, tag) :: s
1582   in
1583    status#set_stack gstatus
1584 ;;
1585
1586 let focus_tac focus status =
1587   let gstatus =
1588     match status#stack with
1589     | [] -> assert false
1590     | (g, t, k, tag) :: s ->
1591         let in_focus = function
1592           | (_,Continuationals.Stack.Open i)
1593           | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1594         in
1595         let focus,others = List.partition in_focus g
1596         in
1597           (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1598           (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1599   in
1600    status#set_stack gstatus
1601 ;;
1602
1603 let rec auto_clusters
1604     flags signature cache depth status : unit =
1605   debug_print ~depth (lazy "entering auto clusters");
1606   (* ignore(Unix.select [] [] [] 0.01); *)
1607   let status = clean_up_tac status in
1608   let goals = head_goals status#stack in
1609   if goals = [] then raise (Proved status)
1610   else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1611   else if List.length goals < 2 then
1612     auto_main flags signature cache depth status
1613   else
1614     debug_print ~depth (lazy ("goals = " ^
1615       String.concat "," (List.map string_of_int goals)));
1616     let classes = HExtlib.clusters (deps status) goals in
1617       debug_print ~depth
1618         (lazy
1619            (String.concat "\n"
1620            (List.map
1621               (fun l ->
1622                  ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1623            classes)));
1624       let status =
1625         List.fold_left
1626           (fun status gl ->
1627              let status = focus_tac gl status in
1628              try
1629                debug_print ~depth (lazy ("focusing on" ^
1630                               String.concat "," (List.map string_of_int gl)));
1631                auto_main flags signature cache depth status; status
1632              with Proved(status) -> NTactics.merge_tac status)
1633           status classes
1634       in raise (Proved status)
1635
1636 and
1637
1638 (* let rec auto_main flags signature cache status k depth = *)
1639
1640 auto_main flags signature (cache:cache) depth status: unit =
1641   debug_print ~depth (lazy "entering auto main");
1642   (* ignore(Unix.select [] [] [] 0.01); *)
1643   let status = sort_tac (clean_up_tac status) in
1644   let goals = head_goals status#stack in
1645   match goals with
1646     | [] -> raise (Proved status)
1647     | _ ->
1648         let branch = List.length(goals)>1 in
1649         if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1650         else
1651         let status =
1652           if branch then NTactics.branch_tac status
1653           else status in
1654         let status, cache = intros ~depth status cache in
1655         let g,gctx, gty = current_goal status in
1656         let ctx,ty = close status g in
1657         let closegty = mk_cic_term ctx ty in
1658         let status, gty = apply_subst status gctx gty in
1659         debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
1660         if is_subsumed depth status closegty cache.under_inspection then
1661           (debug_print (lazy "SUBSUMED");
1662            raise (Gaveup IntSet.add g IntSet.empty))
1663         else
1664         let alternatives, cache =
1665           do_something signature flags status g depth gty cache in
1666         let loop_cache =
1667           let under_inspection =
1668             add_to_th closegty cache.under_inspection closegty in
1669           {cache with under_inspection = under_inspection} in
1670         let unsat =
1671           List.fold_left
1672             (* the underscore information does not need to be returned
1673                by do_something *)
1674             (fun unsat ((_,t),status) ->
1675                let depth',looping_cache =
1676                  if t=Ast.Ident("__whd",None) then depth,cache
1677                  else depth+1, loop_cache in
1678                debug_print (~depth:depth')
1679                  (lazy ("Case: " ^ CicNotationPp.pp_term t));
1680                try auto_clusters flags signature loop_cache
1681                  depth' status; unsat
1682                with
1683                  | Proved status ->
1684                      debug_print (~depth:depth') (lazy "proved");
1685                      if branch then
1686                        let status = NTactics.merge_tac status
1687                        in
1688                          (* old cache, here *)
1689                          try auto_clusters flags signature cache
1690                            depth status; assert false
1691                          with Gaveup f ->
1692                            debug_print ~depth
1693                              (lazy ("Unsat1 at depth " ^ (string_of_int depth)
1694                                    ^ ": " ^
1695                                    (pp_goals status (IntSet.elements f))));
1696                         (* TODO: cache failures *)
1697                            IntSet.union f unsat
1698                      else raise (Proved status)
1699                  | Gaveup f ->
1700                      debug_print (~depth:depth')
1701                        (lazy ("Unsat2 at depth " ^ (string_of_int depth')
1702                               ^ ": " ^
1703                               (pp_goals status (IntSet.elements f))));
1704                      (* TODO: cache local failures *)
1705                      unsat)
1706             IntSet.empty alternatives
1707         in
1708           raise (Gaveup IntSet.add g unsat)
1709 ;;
1710
1711 let int name l def =
1712   try int_of_string (List.assoc name l)
1713   with Failure _ | Not_found -> def
1714 ;;
1715
1716 let auto_tac ~params:(_univ,flags) status =
1717   let goals = head_goals status#stack in
1718   let status, facts = mk_th_cache status goals in
1719   let unit_eq = index_local_equations status#eq_cache status in
1720   let cache = init_cache ~facts ~unit_eq  () in
1721 (*   pp_th status facts; *)
1722 (*
1723   NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1724     debug_print (lazy(
1725       NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1726       String.concat "\n    " (List.map (
1727       NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[])
1728         (NDiscriminationTree.TermSet.elements t))
1729       )));
1730 *)
1731   let depth = int "depth" flags 3 in
1732   let size  = int "size" flags 10 in
1733   let width = int "width" flags (3+List.length goals) in
1734   (* XXX fix sort *)
1735   let goals = List.map (fun i -> (i,P)) goals in
1736   let signature = () in
1737   let flags = {
1738           maxwidth = width;
1739           maxsize = size;
1740           maxdepth = depth;
1741           timeout = Unix.gettimeofday() +. 3000.;
1742           do_types = false;
1743   } in
1744   let initial_time = Unix.gettimeofday() in
1745   app_counter:= 0;
1746   let rec up_to x y =
1747     if x > y then
1748       (print(lazy
1749         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1750        print(lazy
1751         ("Applicative nodes:"^string_of_int !app_counter));
1752        raise (Error (lazy "auto gave up", None)))
1753     else
1754       let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1755       let flags = { flags with maxdepth = x }
1756       in
1757         try auto_clusters flags signature cache 0 status;assert false
1758         with
1759           | Gaveup _ -> up_to (x+1) y
1760           | Proved s ->
1761               print (lazy ("proved at depth " ^ string_of_int x));
1762               let stack =
1763                 match s#stack with
1764                   | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1765                   | _ -> assert false
1766               in
1767                 s#set_stack stack
1768   in
1769   let s = up_to depth depth in
1770     print(lazy
1771         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1772     print(lazy
1773         ("Applicative nodes:"^string_of_int !app_counter));
1774     s
1775 ;;
1776