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