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