helm/software/components/ng_tactics/nAuto.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 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 open Printf
  15
  16 let debug = true
  17 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
  18
  19 open Continuationals.Stack
  20 open NTacStatus
  21 module Ast = CicNotationPt
  22
  23 (* =================================== paramod =========================== *)
  24 let auto_paramod ~params:(l,_) status goal =
  25   let gty = get_goalty status goal in
  26   let n,h,metasenv,subst,o = status#obj in
  27   let status,t = term_of_cic_term status gty (ctx_of gty) in
  28   let status, l =
  29     List.fold_left
  30       (fun (status, l) t ->
  31         let status, t = disambiguate status t None (ctx_of gty) in
  32         let status, ty = typeof status (ctx_of t) t in
  33         let status, t =  term_of_cic_term status t (ctx_of gty) in
  34         let status, ty = term_of_cic_term status ty (ctx_of ty) in
  35         (status, (t,ty) :: l))
  36       (status,[]) l
  37   in
  38   match
  39     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
  40   with
  41   | [] -> raise (Error (lazy "no proof found",None))
  42   | (pt, metasenv, subst)::_ ->
  43       let status = status#set_obj (n,h,metasenv,subst,o) in
  44       instantiate status goal (mk_cic_term (ctx_of gty) pt)
  45 ;;
  46
  47 let auto_paramod_tac ~params status =
  48   NTactics.distribute_tac (auto_paramod ~params) status
  49 ;;
  50
  51 (* =================================== auto =========================== *)
  52 (****************** AUTO ********************
  53
  54 let calculate_timeout flags =
  55     if flags.timeout = 0. then
  56       (debug_print (lazy "AUTO WITH NO TIMEOUT");
  57        {flags with timeout = infinity})
  58     else
  59       flags
  60 ;;
  61 let is_equational_case goalty flags =
  62   let ensure_equational t =
  63     if is_an_equational_goal t then true
  64     else false
  65   in
  66   (flags.use_paramod && is_an_equational_goal goalty) ||
  67   (flags.use_only_paramod && ensure_equational goalty)
  68 ;;
  69
  70 type menv = Cic.metasenv
  71 type subst = Cic.substitution
  72 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
  73 let candidate_no = ref 0;;
  74 type candidate = int * Cic.term Lazy.t
  75 type cache = AutoCache.cache
  76
  77 type fail =
  78   (* the goal (mainly for depth) and key of the goal *)
  79   goal * AutoCache.cache_key
  80 type op =
  81   (* goal has to be proved *)
  82   | D of goal
  83   (* goal has to be cached as a success obtained using candidate as the first
  84    * step *)
  85   | S of goal * AutoCache.cache_key * candidate * int
  86 type elem =
  87   (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
  88   menv * subst * int * op list * op list * fail list
  89 type status =
  90   (* list of computations that may lead to the solution: all op list will
  91    * end with the same (S(g,_)) *)
  92   elem list
  93 type auto_result =
  94   (* menv, subst, alternatives, tables, cache *)
  95   | Proved of menv * subst * elem list * AutomationCache.tables * cache
  96   | Gaveup of AutomationCache.tables * cache
  97
  98
  99 (* the status exported to the external observer *)
 100 type auto_status =
 101   (* context, (goal,candidate) list, and_list, history *)
 102   Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
 103   (int * Cic.term * int) list * Cic.term Lazy.t list
 104
 105 let d_prefix l =
 106   let rec aux acc = function
 107     | (D g)::tl -> aux (acc@[g]) tl
 108     | _ -> acc
 109   in
 110     aux [] l
 111 ;;
 112
 113 let calculate_goal_ty (goalno,_,_) s m =
 114   try
 115     let _,cc,goalty = CicUtil.lookup_meta goalno m in
 116     (* XXX applicare la subst al contesto? *)
 117     Some (cc, CicMetaSubst.apply_subst s goalty)
 118   with CicUtil.Meta_not_found i when i = goalno -> None
 119 ;;
 120
 121 let calculate_closed_goal_ty (goalno,_,_) s =
 122   try
 123     let cc,_,goalty = List.assoc goalno s in
 124     (* XXX applicare la subst al contesto? *)
 125     Some (cc, CicMetaSubst.apply_subst s goalty)
 126   with Not_found ->
 127     None
 128 ;;
 129
 130 let pp_status ctx status =
 131   if debug then
 132   let names = Utils.names_of_context ctx in
 133   let pp x =
 134     let x =
 135       ProofEngineReduction.replace
 136         ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
 137           ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
 138     in
 139     CicPp.pp x names
 140   in
 141   let string_of_do m s (gi,_,_ as g) d =
 142     match calculate_goal_ty g s m with
 143     | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
 144     | None -> Printf.sprintf "D(%d, _, %d)" gi d
 145   in
 146   let string_of_s m su k (ci,ct) gi =
 147     Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
 148   in
 149   let string_of_ol m su l =
 150     String.concat " | "
 151       (List.map
 152         (function
 153           | D (g,d,s) -> string_of_do m su (g,d,s) d
 154           | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
 155         l)
 156   in
 157   let string_of_fl m s fl =
 158     String.concat " | "
 159       (List.map (fun ((i,_,_),ty) ->
 160          Printf.sprintf "(%d, %s)" i (pp ty)) fl)
 161   in
 162   let rec aux = function
 163     | [] -> ()
 164     | (m,s,_,_,ol,fl)::tl ->
 165         Printf.eprintf "< [%s] ;;; [%s]>\n"
 166           (string_of_ol m s ol) (string_of_fl m s fl);
 167         aux tl
 168   in
 169     Printf.eprintf "-------------------------- status -------------------\n";
 170     aux status;
 171     Printf.eprintf "-----------------------------------------------------\n";
 172 ;;
 173
 174 let auto_status = ref [] ;;
 175 let auto_context = ref [];;
 176 let in_pause = ref false;;
 177 let pause b = in_pause := b;;
 178 let cond = Condition.create ();;
 179 let mutex = Mutex.create ();;
 180 let hint = ref None;;
 181 let prune_hint = ref [];;
 182
 183 let step _ = Condition.signal cond;;
 184 let give_hint n = hint := Some n;;
 185 let give_prune_hint hint =
 186   prune_hint := hint :: !prune_hint
 187 ;;
 188
 189 let check_pause _ =
 190   if !in_pause then
 191     begin
 192       Mutex.lock mutex;
 193       Condition.wait cond mutex;
 194       Mutex.unlock mutex
 195     end
 196 ;;
 197
 198 let get_auto_status _ =
 199   let status = !auto_status in
 200   let and_list,elems,last =
 201     match status with
 202     | [] -> [],[],[]
 203     | (m,s,_,don,gl,fail)::tl ->
 204         let and_list =
 205           HExtlib.filter_map
 206             (fun (id,d,_ as g) ->
 207               match calculate_goal_ty g s m with
 208               | Some (_,x) -> Some (id,x,d) | None -> None)
 209             (d_goals gl)
 210         in
 211         let rows =
 212           (* these are the S goalsin the or list *)
 213           let orlist =
 214             List.map
 215               (fun (m,s,_,don,gl,fail) ->
 216                 HExtlib.filter_map
 217                   (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
 218                   (List.rev don @ gl))
 219               status
 220           in
 221           (* this function eats id from a list l::[id,x] returning x, l *)
 222           let eat_tail_if_eq id l =
 223             let rec aux (s, l) = function
 224               | [] -> s, l
 225               | ((id1,_,_),k1,c)::tl when id = id1 ->
 226                   (match s with
 227                   | None -> aux (Some c,l) tl
 228                   | Some _ -> assert false)
 229               | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
 230             in
 231             let c, l = aux (None, []) l in
 232             c, List.rev l
 233           in
 234           let eat_in_parallel id l =
 235             let rec aux (b,eaten, new_l as acc) l =
 236               match l with
 237               | [] -> acc
 238               | l::tl ->
 239                   match eat_tail_if_eq id l with
 240                   | None, l -> aux (b@[false], eaten, new_l@[l]) tl
 241                   | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
 242             in
 243             aux ([],[],[]) l
 244           in
 245           let rec eat_all rows l =
 246             match l with
 247             | [] -> rows
 248             | elem::or_list ->
 249                 match List.rev elem with
 250                 | ((to_eat,depth,_),k,_)::next_lunch ->
 251                     let b, eaten, l = eat_in_parallel to_eat l in
 252                     let eaten = HExtlib.list_uniq eaten in
 253                     let eaten = List.rev eaten in
 254                     let b = true (* List.hd (List.rev b) *) in
 255                     let rows = rows @ [to_eat,k,b,depth,eaten] in
 256                     eat_all rows l
 257                 | [] -> eat_all rows or_list
 258           in
 259           eat_all [] (List.rev orlist)
 260         in
 261         let history =
 262           HExtlib.filter_map
 263             (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
 264             gl
 265         in
 266 (*         let rows = List.filter (fun (_,l) -> l <> []) rows in *)
 267         and_list, rows, history
 268   in
 269   !auto_context, elems, and_list, last
 270 ;;
 271
 272 (* Works if there is no dependency over proofs *)
 273 let is_a_green_cut goalty =
 274   CicUtil.is_meta_closed goalty
 275 ;;
 276 let rec first_s = function
 277   | (D _)::tl -> first_s tl
 278   | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
 279   | [] -> None
 280 ;;
 281 let list_union l1 l2 =
 282   (* TODO ottimizzare compare *)
 283   HExtlib.list_uniq (List.sort compare (l1 @ l1))
 284 ;;
 285 let rec eq_todo l1 l2 =
 286   match l1,l2 with
 287   | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
 288   | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
 289     when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
 290       if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
 291   | [],[] -> true
 292   | _ -> false
 293 ;;
 294 let eat_head todo id fl orlist =
 295   let rec aux acc = function
 296   | [] -> [], acc
 297   | (m, s, _, _, todo1, fl1)::tl as orlist ->
 298       let rec aux1 todo1 =
 299         match first_s todo1 with
 300         | None -> orlist, acc
 301         | Some (((gno,_,_),_,_,_), todo11) ->
 302             (* TODO confronto tra todo da ottimizzare *)
 303             if gno = id && eq_todo todo11 todo then
 304               aux (list_union fl1 acc) tl
 305             else
 306               aux1 todo11
 307       in
 308        aux1 todo1
 309   in
 310     aux fl orlist
 311 ;;
 312 let close_proof p ty menv context =
 313   let metas =
 314     List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
 315   in
 316   let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
 317   naif_closure p menv context
 318 ;;
 319 (* XXX capire bene quando aggiungere alla cache *)
 320 let add_to_cache_and_del_from_orlist_if_green_cut
 321   g s m cache key todo orlist fl ctx size minsize
 322 =
 323   let cache = cache_remove_underinspection cache key in
 324   (* prima per fare la irl usavamo il contesto vero e proprio e non quello
 325    * canonico! XXX *)
 326   match calculate_closed_goal_ty g s with
 327   | None -> assert false
 328   | Some (canonical_ctx , gty) ->
 329       let goalno,depth,sort = g in
 330       let irl = mk_irl canonical_ctx in
 331       let goal = Cic.Meta(goalno, irl) in
 332       let proof = CicMetaSubst.apply_subst s goal in
 333       let green_proof, closed_proof =
 334         let b = is_a_green_cut proof in
 335         if not b then
 336           b, (* close_proof proof gty m ctx *) proof
 337         else
 338           b, proof
 339       in
 340       debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
 341       if is_a_green_cut key then
 342         (* if the initia goal was closed, we cut alternatives *)
 343         let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
 344         let orlist, fl = eat_head todo goalno fl orlist in
 345         let cache =
 346           if size < minsize then
 347             (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
 348           else
 349           (* if the proof is closed we cache it *)
 350           if green_proof then cache_add_success cache key proof
 351           else (* cache_add_success cache key closed_proof *)
 352             (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
 353         in
 354         cache, orlist, fl, true
 355       else
 356         let cache =
 357           debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
 358           if size < minsize then
 359             (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
 360           (* if the substituted goal and the proof are closed we cache it *)
 361           if is_a_green_cut gty then
 362             if green_proof then cache_add_success cache gty proof
 363             else (* cache_add_success cache gty closed_proof *)
 364               (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
 365           else (*
 366             try
 367               let ty, _ =
 368                 CicTypeChecker.type_of_aux' ~subst:s
 369                   m ctx closed_proof CicUniv.oblivion_ugraph
 370               in
 371               if is_a_green_cut ty then
 372                 cache_add_success cache ty closed_proof
 373               else cache
 374             with
 375             | CicTypeChecker.TypeCheckerFailure _ ->*)
 376           (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
 377         in
 378         cache, orlist, fl, false
 379 ;;
 380 let close_failures (fl : fail list) (cache : cache) =
 381   List.fold_left
 382     (fun cache ((gno,depth,_),gty) ->
 383       if CicUtil.is_meta_closed gty then
 384        ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
 385          cache_add_failure cache gty depth)
 386       else
 387          cache)
 388     cache fl
 389 ;;
 390 let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
 391   let entry = goalno, (canonical_ctx, t,ty) in
 392   assert_subst_are_disjoint subst [entry];
 393   let subst = entry :: subst in
 394
 395   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
 396
 397   subst, metasenv
 398 ;;
 399
 400 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
 401   None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
 402 ;;
 403
 404 let equational_case
 405   tables cache depth fake_proof goalno goalty subst context
 406     flags
 407 =
 408   let active,passive,bag = tables in
 409   let ppterm = ppterm context in
 410   let status = (fake_proof,goalno) in
 411     if flags.use_only_paramod then
 412       begin
 413         debug_print (lazy ("PARAMODULATION SU: " ^
 414                          string_of_int goalno ^ " " ^ ppterm goalty ));
 415         let goal_steps, saturation_steps, timeout =
 416           max_int,max_int,flags.timeout
 417         in
 418         match
 419           Saturation.given_clause bag status active passive
 420             goal_steps saturation_steps timeout
 421         with
 422           | None, active, passive, bag ->
 423               [], (active,passive,bag), cache, flags
 424           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
 425             passive,bag ->
 426               assert_subst_are_disjoint subst subst';
 427               let subst = subst@subst' in
 428               let open_goals =
 429                 order_new_goals metasenv subst open_goals ppterm
 430               in
 431               let open_goals =
 432                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 433               in
 434               incr candidate_no;
 435               [(!candidate_no,proof),metasenv,subst,open_goals],
 436                 (active,passive,bag), cache, flags
 437       end
 438     else
 439       begin
 440         debug_print (lazy ("NARROWING DEL GOAL: " ^
 441                          string_of_int goalno ^ " " ^ ppterm goalty ));
 442         let goal_steps, saturation_steps, timeout =
 443           1,0,flags.timeout
 444         in
 445         match
 446           Saturation.solve_narrowing bag status active passive goal_steps
 447         with
 448           | None, active, passive, bag ->
 449               [], (active,passive,bag), cache, flags
 450           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
 451             passive,bag ->
 452               assert_subst_are_disjoint subst subst';
 453               let subst = subst@subst' in
 454               let open_goals =
 455                 order_new_goals metasenv subst open_goals ppterm
 456               in
 457               let open_goals =
 458                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 459               in
 460               incr candidate_no;
 461               [(!candidate_no,proof),metasenv,subst,open_goals],
 462                 (active,passive,bag), cache, flags
 463       end
 464 (*
 465       begin
 466         let params = ([],["use_context","false"]) in
 467         let automation_cache = {
 468               AutomationCache.tables = tables ;
 469               AutomationCache.univ = Universe.empty; }
 470         in
 471         try
 472           let ((_,metasenv,subst,_,_,_),open_goals) =
 473
 474             solve_rewrite ~params ~automation_cache
 475               (fake_proof, goalno)
 476           in
 477           let proof = lazy (Cic.Meta (-1,[])) in
 478           [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
 479         with ProofEngineTypes.Fail _ -> [], tables, cache, flags
 480 (*
 481         let res = Saturation.all_subsumed bag status active passive in
 482         let res' =
 483           List.map
 484             (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
 485                assert_subst_are_disjoint subst subst';
 486                let subst = subst@subst' in
 487                let open_goals =
 488                  order_new_goals metasenv subst open_goals ppterm
 489                in
 490                let open_goals =
 491                  List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 492                in
 493                incr candidate_no;
 494                  (!candidate_no,proof),metasenv,subst,open_goals)
 495             res
 496           in
 497           res', (active,passive,bag), cache, flags
 498 *)
 499       end
 500 *)
 501 ;;
 502
 503 let sort_new_elems =
 504  List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
 505          let p1 = List.length (prop_only l1) in
 506          let p2 = List.length (prop_only l2) in
 507          if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
 508 ;;
 509
 510
 511 let try_candidate dbd
 512   goalty tables subst fake_proof goalno depth context cand
 513 =
 514   let ppterm = ppterm context in
 515   try
 516     let actives, passives, bag = tables in
 517     let (_,metasenv,subst,_,_,_), open_goals =
 518        ProofEngineTypes.apply_tactic
 519         (PrimitiveTactics.apply_tac ~term:cand)
 520         (fake_proof,goalno)
 521     in
 522     let tables = actives, passives,
 523       Equality.push_maxmeta bag
 524         (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
 525     in
 526     debug_print (lazy ("   OK: " ^ ppterm cand));
 527     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
 528     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 529     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 530     incr candidate_no;
 531     Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
 532   with
 533     | ProofEngineTypes.Fail s -> None,tables
 534     | CicUnification.Uncertain s ->  None,tables
 535 ;;
 536
 537 let applicative_case dbd
 538   tables depth subst fake_proof goalno goalty metasenv context
 539   signature universe cache flags
 540 =
 541   (* let goalty_aux =
 542     match goalty with
 543     | Cic.Appl (hd::tl) ->
 544         Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
 545     | _ -> goalty
 546   in *)
 547   let goalty_aux = goalty in
 548   let candidates =
 549     get_candidates flags.skip_trie_filtering universe cache goalty_aux
 550   in
 551   (* if the goal is an equality we skip the congruence theorems
 552   let candidates =
 553     if is_equational_case goalty flags
 554     then List.filter not_default_eq_term candidates
 555     else candidates
 556   in *)
 557   let candidates = List.filter (only signature context metasenv) candidates
 558   in
 559   let tables, elems =
 560     List.fold_left
 561       (fun (tables,elems) cand ->
 562         match
 563           try_candidate dbd goalty
 564             tables subst fake_proof goalno depth context cand
 565         with
 566         | None, tables -> tables, elems
 567         | Some x, tables -> tables, x::elems)
 568       (tables,[]) candidates
 569   in
 570   let elems = sort_new_elems elems in
 571   elems, tables, cache
 572 ;;
 573
 574 let try_smart_candidate dbd
 575   goalty tables subst fake_proof goalno depth context cand
 576 =
 577   let ppterm = ppterm context in
 578   try
 579     let params = ([],[]) in
 580     let automation_cache = {
 581           AutomationCache.tables = tables ;
 582           AutomationCache.univ = Universe.empty; }
 583     in
 584     debug_print (lazy ("candidato per " ^ string_of_int goalno
 585       ^ ": " ^ CicPp.ppterm cand));
 586 (*
 587     let (_,metasenv,subst,_,_,_) = fake_proof in
 588     prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
 589     prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
 590 *)
 591     let ((_,metasenv,subst,_,_,_),open_goals) =
 592       apply_smart ~dbd ~term:cand ~params ~automation_cache
 593         (fake_proof, goalno)
 594     in
 595     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
 596     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 597     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 598     incr candidate_no;
 599     Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
 600   with
 601   | ProofEngineTypes.Fail s -> None,tables
 602   | CicUnification.Uncertain s ->  None,tables
 603 ;;
 604
 605 let smart_applicative_case dbd
 606   tables depth subst fake_proof goalno goalty metasenv context signature
 607   universe cache flags
 608 =
 609   let goalty_aux =
 610     match goalty with
 611     | Cic.Appl (hd::tl) ->
 612         Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
 613     | _ -> goalty
 614   in
 615   let smart_candidates =
 616     get_candidates flags.skip_trie_filtering universe cache goalty_aux
 617   in
 618   let candidates =
 619     get_candidates flags.skip_trie_filtering universe cache goalty
 620   in
 621   let smart_candidates =
 622     List.filter
 623       (fun x -> not(List.mem x candidates)) smart_candidates
 624   in
 625   let debug_msg =
 626     (lazy ("smart_candidates" ^ " = " ^
 627              (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
 628   debug_print debug_msg;
 629   let candidates = List.filter (only signature context metasenv) candidates in
 630   let smart_candidates =
 631     List.filter (only signature context metasenv) smart_candidates
 632   in
 633 (*
 634   let penalty cand depth =
 635     if only signature context metasenv cand then depth else ((prerr_endline (
 636     "penalizzo " ^ CicPp.ppterm cand));depth -1)
 637   in
 638 *)
 639   let tables, elems =
 640     List.fold_left
 641       (fun (tables,elems) cand ->
 642         match
 643           try_candidate dbd goalty
 644             tables subst fake_proof goalno depth context cand
 645         with
 646         | None, tables ->
 647             (* if normal application fails we try to be smart *)
 648             (match try_smart_candidate dbd goalty
 649                tables subst fake_proof goalno depth context cand
 650              with
 651                | None, tables -> tables, elems
 652                | Some x, tables -> tables, x::elems)
 653         | Some x, tables -> tables, x::elems)
 654       (tables,[]) candidates
 655   in
 656   let tables, smart_elems =
 657       List.fold_left
 658         (fun (tables,elems) cand ->
 659           match
 660             try_smart_candidate dbd goalty
 661               tables subst fake_proof goalno depth context cand
 662           with
 663           | None, tables -> tables, elems
 664           | Some x, tables -> tables, x::elems)
 665         (tables,[]) smart_candidates
 666   in
 667   let elems = sort_new_elems (elems @ smart_elems) in
 668   elems, tables, cache
 669 ;;
 670
 671 let equational_and_applicative_case dbd
 672   signature universe flags m s g gty tables cache context
 673 =
 674   let goalno, depth, sort = g in
 675   let fake_proof = mk_fake_proof m s g gty context in
 676   if is_equational_case gty flags then
 677     let elems,tables,cache, flags =
 678       equational_case tables cache
 679         depth fake_proof goalno gty s context flags
 680     in
 681     let more_elems, tables, cache =
 682       if flags.use_only_paramod then
 683         [],tables, cache
 684       else
 685         applicative_case dbd
 686           tables depth s fake_proof goalno
 687             gty m context signature universe cache flags
 688     in
 689       elems@more_elems, tables, cache, flags
 690   else
 691     let elems, tables, cache =
 692       match LibraryObjects.eq_URI () with
 693       | Some _ ->
 694          smart_applicative_case dbd tables depth s fake_proof goalno
 695            gty m context signature universe cache flags
 696       | None ->
 697          applicative_case dbd tables depth s fake_proof goalno
 698            gty m context signature universe cache flags
 699     in
 700       elems, tables, cache, flags
 701 ;;
 702 let rec condition_for_hint i = function
 703   | [] -> false
 704   | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
 705   | _::tl -> condition_for_hint i tl
 706 ;;
 707 let prunable_for_size flags s m todo =
 708   let rec aux b = function
 709     | (S _)::tl -> aux b tl
 710     | (D (_,_,T))::tl -> aux b tl
 711     | (D g)::tl ->
 712         (match calculate_goal_ty g s m with
 713           | None -> aux b tl
 714           | Some (canonical_ctx, gty) ->
 715             let gsize, _ =
 716               Utils.weight_of_term
 717                 ~consider_metas:false ~count_metas_occurrences:true gty in
 718             let newb = b || gsize > flags.maxgoalsizefactor in
 719             aux newb tl)
 720     | [] -> b
 721   in
 722     aux false todo
 723
 724 (*
 725 let prunable ty todo =
 726   let rec aux b = function
 727     | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
 728     | (D (_,_,T))::tl -> aux b tl
 729     | D _::_ -> false
 730     | [] -> b
 731   in
 732     aux false todo
 733 ;;
 734 *)
 735
 736 let prunable menv subst ty todo =
 737   let rec aux = function
 738     | (S(_,k,_,_))::tl ->
 739          (match Equality.meta_convertibility_subst k ty menv with
 740           | None -> aux tl
 741           | Some variant ->
 742                no_progress variant tl (* || aux tl*))
 743     | (D (_,_,T))::tl -> aux tl
 744     | _ -> false
 745   and no_progress variant = function
 746     | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
 747     | D ((n,_,P) as g)::tl ->
 748         (match calculate_goal_ty g subst menv with
 749            | None -> no_progress variant tl
 750            | Some (_, gty) ->
 751                (match calculate_goal_ty g variant menv with
 752                   | None -> assert false
 753                   | Some (_, gty') ->
 754                       if gty = gty' then no_progress variant tl
 755 (*
 756 (prerr_endline (string_of_int n);
 757  prerr_endline (CicPp.ppterm gty);
 758  prerr_endline (CicPp.ppterm gty');
 759  prerr_endline "---------- subst";
 760  prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
 761  prerr_endline "---------- variant";
 762  prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
 763  prerr_endline "---------- menv";
 764  prerr_endline (CicMetaSubst.ppmetasenv [] menv);
 765                          no_progress variant tl) *)
 766                       else false))
 767     | _::tl -> no_progress variant tl
 768   in
 769     aux todo
 770
 771 ;;
 772 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
 773   let s =
 774     HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
 775   in
 776   List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
 777 ;;
 778 let filter_prune_hint c l =
 779   let prune = !prune_hint in
 780   prune_hint := []; (* possible race... *)
 781   if prune = [] then c,l
 782   else
 783     cache_reset_underinspection c,
 784     List.filter (condition_for_prune_hint prune) l
 785 ;;
 786
 787
 788
 789 let
 790   auto_all_solutions dbd tables universe cache context metasenv gl flags
 791 =
 792   let signature =
 793     List.fold_left
 794       (fun set g ->
 795          MetadataConstraints.UriManagerSet.union set
 796              (MetadataQuery.signature_of metasenv g)
 797        )
 798       MetadataConstraints.UriManagerSet.empty gl
 799   in
 800   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 801   let goals =
 802     List.map
 803       (fun (x,s) -> D (x,flags.maxdepth,s)) goals
 804   in
 805   let elems = [metasenv,[],1,[],goals,[]] in
 806   let rec aux tables solutions cache elems flags =
 807     match auto_main dbd tables context flags signature universe cache elems with
 808     | Gaveup (tables,cache) ->
 809         solutions,cache, tables
 810     | Proved (metasenv,subst,others,tables,cache) ->
 811         if Unix.gettimeofday () > flags.timeout then
 812           ((subst,metasenv)::solutions), cache, tables
 813         else
 814           aux tables ((subst,metasenv)::solutions) cache others flags
 815   in
 816   let rc = aux tables [] cache elems flags in
 817     match rc with
 818     | [],cache,tables -> [],cache,tables
 819     | solutions, cache,tables ->
 820         let solutions =
 821           HExtlib.filter_map
 822             (fun (subst,newmetasenv) ->
 823               let opened =
 824                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
 825               in
 826               if opened = [] then Some subst else None)
 827             solutions
 828         in
 829          solutions,cache,tables
 830 ;;
 831
 832 (******************* AUTO ***************)
 833
 834
 835 let auto dbd flags metasenv tables universe cache context metasenv gl =
 836   let initial_time = Unix.gettimeofday() in
 837   let signature =
 838     List.fold_left
 839       (fun set g ->
 840          MetadataConstraints.UriManagerSet.union set
 841              (MetadataQuery.signature_of metasenv g)
 842        )
 843       MetadataConstraints.UriManagerSet.empty gl
 844   in
 845   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 846   let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
 847   let elems = [metasenv,[],1,[],goals,[]] in
 848   match auto_main dbd tables context flags signature universe cache elems with
 849   | Proved (metasenv,subst,_, tables,cache) ->
 850       debug_print(lazy
 851         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
 852       Some (subst,metasenv), cache
 853   | Gaveup (tables,cache) ->
 854       debug_print(lazy
 855         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
 856       None,cache
 857 ;;
 858
 859 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
 860   let flags = flags_of_params params () in
 861   let use_library = flags.use_library in
 862   let universe, tables, cache =
 863     init_cache_and_tables
 864      ~dbd ~use_library ~use_context:(not flags.skip_context)
 865      automation_cache univ (proof, goal)
 866   in
 867   let _,metasenv,subst,_,_, _ = proof in
 868   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
 869   let signature = MetadataQuery.signature_of metasenv goal in
 870   let signature =
 871     List.fold_left
 872       (fun set t ->
 873          let ty, _ =
 874            CicTypeChecker.type_of_aux' metasenv context t
 875              CicUniv.oblivion_ugraph
 876          in
 877          MetadataConstraints.UriManagerSet.union set
 878            (MetadataConstraints.constants_of ty)
 879        )
 880       signature univ
 881   in
 882   let tables,cache =
 883     if flags.close_more then
 884       close_more
 885         tables context (proof, goal)
 886           (auto_all_solutions dbd) signature universe cache
 887     else tables,cache in
 888   let initial_time = Unix.gettimeofday() in
 889   let (_,oldmetasenv,_,_,_, _) = proof in
 890     hint := None;
 891   let elem =
 892     metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
 893   in
 894   match auto_main dbd tables context flags signature universe cache [elem] with
 895     | Proved (metasenv,subst,_, tables,cache) ->
 896         debug_print (lazy
 897           ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
 898         let proof,metasenv =
 899         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
 900           proof goal subst metasenv
 901         in
 902         let opened =
 903           ProofEngineHelpers.compare_metasenvs ~oldmetasenv
 904             ~newmetasenv:metasenv
 905         in
 906           proof,opened
 907     | Gaveup (tables,cache) ->
 908         debug_print
 909           (lazy ("TIME:"^
 910             string_of_float(Unix.gettimeofday()-.initial_time)));
 911         raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
 912 ;;
 913 *)
 914
 915 module CacheElem : Set.OrderedType =
 916  struct
 917   type t =
 918    | Failed_in of int * NCic.term     (* depth, goal type *)
 919    | Succeded of Cic.term * Cic.term  (* proof, proof type *)
 920    | UnderInspection of Cic.term      (* avoid looping *)
 921
 922   let compare = Pervasives.compare
 923  end
 924
 925 module CacheSet = Set.Make(CacheElem)
 926 module Cache =
 927   Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CacheSet)
 928
 929 type cache_examination_result =
 930   [ `Failed_in of int
 931   | `UnderInspection
 932   | `Succeded of NCic.term
 933   | `NotFound
 934   ]
 935
 936 type sort = T | P
 937 type goal = int * int * sort (* goal, depth, sort *)
 938 type fail = goal * cic_term
 939 type candidate = int * NCic.term (* unique candidate number, candidate *)
 940
 941 type op =
 942   (* goal has to be proved *)
 943   | D of goal
 944   (* goal has to be cached as a success obtained using candidate as the first
 945    * step *)
 946   | S of goal * cic_term * candidate (* int was minsize *)
 947 type 'a elem =
 948   (* menv, subst, size, operations done (only S), operations to do,
 949    * failures to cache if any op fails *)
 950   (#tac_status as 'a) * int * op list * op list * fail list
 951
 952 type 'a auto_status =
 953   (* list of computations that may lead to the solution: all op list will
 954    * end with the same (S(g,_)) *)
 955   'a elem list * Cache.t
 956
 957 type 'a auto_result =
 958   | Gaveup
 959   | Proved of (#tac_status as 'a) * 'a auto_status (* alt. proofs *)
 960
 961 type flags = {
 962         do_types : bool; (* solve goals in Type *)
 963         maxwidth : int;
 964         maxsize  : int;
 965         timeout  : float;
 966 }
 967
 968 let close_failures _ c = c;;
 969 let prunable _ _ _ = false;;
 970 let cache_examine cache gty = `Notfound;;
 971 let put_in_subst s _ _ _  = s;;
 972 let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ _ = c, o, f, false ;;
 973 let cache_add_underinspection c _ _ = c;;
 974 let equational_case _ _ _ _ _ _ _ = [];;
 975 let sort_new_elems l = l;;
 976 let only _ _ _ = true;;
 977
 978 let candidate_no = ref 0;;
 979
 980 let try_candidate status t g =
 981  try
 982    debug_print (lazy (" try " ^
 983      NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t
 984    ));
 985    let ast_for_t =
 986      match t with
 987      | NCic.Rel i -> assert false
 988      | NCic.Const ref -> Ast.NRef ref
 989      | _ -> assert false
 990    in
 991    let status = NTactics.focus_tac [g] status in
 992    let status = NTactics.apply_tac ("",0,ast_for_t) status in
 993    let open_goals = head_goals status#stack in
 994    incr candidate_no;
 995    Some ((!candidate_no,t),status,open_goals)
 996  with Error (msg,exn) -> debug_print msg; None
 997 ;;
 998
 999
1000 let get_candidates status context gty =
1001   let universe = status#auto_cache in
1002   let _, gty = term_of_cic_term status gty (ctx_of gty) in
1003   let cands =
1004     NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty
1005   in
1006   (* XXX we have to trie for the context *)
1007   let cands = NDiscriminationTree.TermSet.elements cands in
1008   List.iter (fun x ->
1009     debug_print (lazy (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)))
1010     cands;
1011   cands
1012 ;;
1013
1014 let applicative_case signature status flags g gty cache context =
1015   let candidates = get_candidates status context gty in
1016   let candidates = List.filter (only signature context) candidates in
1017   debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates)));
1018   let elems =
1019     List.fold_left
1020       (fun elems cand ->
1021         match try_candidate status cand g with
1022         | None -> elems
1023         | Some x -> x::elems)
1024       [] candidates
1025   in
1026   elems
1027 ;;
1028
1029 let equational_and_applicative_case
1030   signature flags status g depth gty cache context
1031 =
1032  let elems =
1033   if false (*is_equational_case gty flags*) then
1034     let elems =
1035       equational_case
1036         signature status flags g gty cache context
1037     in
1038     let more_elems =
1039         applicative_case
1040           signature status flags g gty cache context
1041     in
1042       elems@more_elems
1043   else
1044     let elems =
1045       (*match LibraryObjects.eq_URI () with
1046       | Some _ ->
1047          smart_applicative_case dbd tables depth s fake_proof goalno
1048            gty m context signature universe cache flags
1049       | None -> *)
1050          applicative_case
1051           signature status flags g gty cache context
1052     in
1053       elems
1054  in
1055  let elems =
1056     (* XXX calculate the sort *)
1057    List.map (fun c,s,gl -> c,s,List.map (fun i -> i,depth-1,P) gl) elems
1058  in
1059  let elems = sort_new_elems elems in
1060  elems
1061 ;;
1062
1063 let calculate_goal_ty (goalno,_,_) status =
1064   try Some (get_goalty status goalno)
1065   with Error _ -> None
1066 ;;
1067 let d_goals l =
1068   let rec aux acc = function
1069     | (D g)::tl -> aux (acc@[g]) tl
1070     | (S _)::tl -> aux acc tl
1071     | [] -> acc
1072   in
1073     aux [] l
1074 ;;
1075 let prop_only l =
1076   List.filter (function (_,_,P) -> true | _ -> false) l
1077 ;;
1078 let remove_s_from_fl (id,_,_) (fl : fail list) =
1079   let rec aux = function
1080     | [] -> []
1081     | ((id1,_,_),_)::tl when id = id1 -> tl
1082     | hd::tl ->  hd :: aux tl
1083   in
1084     aux fl
1085 ;;
1086
1087 let auto_main context flags signature elems cache =
1088   let rec aux (elems, cache : 'a auto_status) =
1089 (* processa le hint dell'utente *)
1090 (*     let cache, elems = filter_prune_hint cache elems in *)
1091     match elems with
1092 (* USER HINT
1093     | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
1094         debug_print (lazy "skip");
1095         (match !hint with
1096         | Some i when condition_for_hint i todo ->
1097             aux tables flags cache orlist
1098         | _ ->
1099           hint := None;
1100           aux tables flags cache elems)
1101 *)
1102     | [] ->
1103         debug_print (lazy "gave up");
1104         Gaveup
1105     | (s, _, _, [],_)::orlist ->
1106         debug_print (lazy "success");
1107         Proved (s, (orlist, cache))
1108     | (s, size, don, (D (_,_,T))::todo, fl)::orlist
1109       when not flags.do_types ->
1110         debug_print (lazy "skip goal in Type");
1111         aux ((s, size, don, todo, fl)::orlist, cache)
1112     | (s, size, don, (S(g, key, c) as op)::todo, fl)::orlist ->
1113         let cache, orlist, fl, sibling_pruned =
1114           add_to_cache_and_del_from_orlist_if_green_cut
1115             g s cache key todo orlist fl context size
1116         in
1117         let fl = remove_s_from_fl g fl in
1118         let don = if sibling_pruned then don else op::don in
1119         let s = NTactics.unfocus_tac s in
1120         aux ((s, size, don, todo, fl)::orlist, cache)
1121     | (s, size, don, todo, fl)::orlist
1122       when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1123         debug_print (lazy ("FAIL: WIDTH"));
1124         aux (orlist, cache)
1125     | (s, size, don, todo, fl)::orlist when size > flags.maxsize ->
1126         debug_print (lazy ("FAIL: SIZE: "^string_of_int size ^
1127             " > " ^ string_of_int flags.maxsize ));
1128         aux (orlist, cache)
1129     | _ when Unix.gettimeofday () > flags.timeout ->
1130         debug_print (lazy ("FAIL: TIMEOUT"));
1131         Gaveup
1132     | (s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist ->
1133         debug_print (lazy "attack goal");
1134         match calculate_goal_ty g s with
1135         | None ->
1136             debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1137             aux ((s,size,don,todo, fl)::orlist, cache)
1138         | Some gty ->
1139             debug_print (lazy ("EXAMINE: "^ ppterm s gty));
1140             match cache_examine cache gty with
1141             | `Failed_in d when d >= depth ->
1142                 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1143                 let cache = close_failures fl cache in
1144                 aux (orlist, cache)
1145             | `UnderInspection ->
1146                 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1147                 let cache = close_failures fl cache in
1148                 aux (orlist,cache)
1149             | `Succeded t ->
1150                 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1151                 let s = put_in_subst s g t gty in
1152                 aux ((s, size, don,todo, fl)::orlist, cache)
1153             | `Notfound
1154             | `Failed_in _ when depth > 0 ->
1155                 ( (* more depth or is the first time we see the goal *)
1156                     if prunable s gty todo then
1157                       (debug_print (lazy( "FAIL: LOOP: one father is equal"));
1158                        let cache = close_failures fl cache in
1159                        aux (orlist,cache))
1160                     else
1161                     let cache = cache_add_underinspection cache gty depth in
1162                     debug_print (lazy ("INSPECTING: " ^
1163                         string_of_int gno ^ "("^ string_of_int size ^ "): "^
1164                         ppterm s gty));
1165                     (* elems are possible computations for proving gty *)
1166                     let elems =
1167                       equational_and_applicative_case
1168                         signature flags s gno depth gty cache context
1169                     in
1170                     if elems = [] then
1171                       (* this goal has failed *)
1172                       let cache = close_failures ((g,gty)::fl) cache in
1173                       aux (orlist, cache)
1174                     else
1175                       let size_gl l = List.length
1176                         (List.filter (function (_,_,P) -> true | _ -> false) l)
1177                       in
1178                       let elems =
1179                         let inj_gl gl = List.map (fun g -> D g) gl in
1180                         let rec map = function
1181                           | [] -> assert false
1182                           | (cand,s,gl)::[] ->
1183                               let todo =
1184                                 inj_gl gl @ (S(g,gty,cand))::todo
1185                               in
1186                               (* we are the last in OR, we fail on g and
1187                                * also on all failures implied by g *)
1188                               (s, size + size_gl gl, don, todo, (g,gty)::fl)
1189                               :: orlist
1190                           | (cand,s,gl)::tl ->
1191                               let todo =
1192                                 inj_gl gl @ (S(g,gty,cand))::todo
1193                               in
1194                               (s, size + size_gl gl, don, todo, []) :: map tl
1195                         in
1196                           map elems
1197                       in
1198                         aux (elems, cache))
1199             | _ ->
1200                 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1201                 let cache = close_failures fl cache in
1202                 aux (orlist, cache)
1203   in
1204     (aux (elems, cache) : 'a auto_result)
1205 ;;
1206
1207 let auto_tac ~params status =
1208   let cache = Cache.empty in
1209   let goals = head_goals status#stack in
1210   let depth = 3 in (* XXX fix sort *)
1211   let goals = List.map (fun i -> D(i,depth,P)) goals in
1212   let elems = [status,0,[],goals,[]] in
1213   let context = [] (* XXX big problem *) in
1214   let signature = () in
1215   let flags = {
1216           maxwidth = 3;
1217           maxsize = 10;
1218           timeout = Unix.gettimeofday() +. 3000.;
1219           do_types = false;
1220   } in
1221   match auto_main context flags signature elems cache with
1222   | Gaveup -> raise (Error (lazy "auto gave up", None))
1223   | Proved (s, (_orlist, _cache)) ->
1224       let stack =
1225         match s#stack with
1226         | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1227         | _ -> assert false
1228       in
1229       s#set_stack stack
1230 ;;
1231
1232
1233 (* ========================= dispatching of auto/auto_paramod ============ *)
1234 let auto_tac ~params:(_,flags as params) =
1235   if List.mem_assoc "paramodulation" flags then
1236     auto_paramod_tac ~params
1237   else
1238     auto_tac ~params
1239 ;;
1240
1241 (* EOF *)