]> matita.cs.unibo.it Git - helm.git/commitdiff
nAuto W.I.P.
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 6 Oct 2009 11:48:02 +0000 (11:48 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 6 Oct 2009 11:48:02 +0000 (11:48 +0000)
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/ng_tactics/nAuto.ml

index 871ec01b8dde9a5c3e019488999049af1ebcf4f7..1b6878aba1414bb619b525c40a28155402ab6a7e 100644 (file)
@@ -534,8 +534,8 @@ let index_obj_for_auto status (uri, height, _, _, kind) =
   | NCic.Fixpoint _ -> []
   | NCic.Inductive _ -> []
   | NCic.Constant (_,_,_, ty, _) ->
-      [ ty, NCic.Const(NReference.reference_of_spec 
-              uri (NReference.Def height)) ]
+      let ty = (* saturare *) ty in
+      [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Def height))]
  in
  let status = basic_index_obj data status in
  let dump = record_index_obj data :: status#dump in
index 60587e1e34ec3277dee4a6c0c42cbd8424f6707d..bdcb98969d546a78703029b5e8f184f10f130079 100644 (file)
@@ -49,6 +49,1077 @@ let auto_paramod_tac ~params status =
 ;;
 
 (* =================================== auto =========================== *)
+(****************** AUTO ********************
+
+let calculate_timeout flags = 
+    if flags.timeout = 0. then 
+      (debug_print (lazy "AUTO WITH NO TIMEOUT");
+       {flags with timeout = infinity})
+    else 
+      flags 
+;;
+let is_equational_case goalty flags =
+  let ensure_equational t = 
+    if is_an_equational_goal t then true 
+    else false
+  in
+  (flags.use_paramod && is_an_equational_goal goalty) || 
+  (flags.use_only_paramod && ensure_equational goalty)
+;;
+
+type menv = Cic.metasenv
+type subst = Cic.substitution
+type goal = ProofEngineTypes.goal * int * AutoTypes.sort
+let candidate_no = ref 0;;
+type candidate = int * Cic.term Lazy.t
+type cache = AutoCache.cache
+
+type fail = 
+  (* the goal (mainly for depth) and key of the goal *)
+  goal * AutoCache.cache_key
+type op = 
+  (* goal has to be proved *)
+  | D of goal 
+  (* goal has to be cached as a success obtained using candidate as the first
+   * step *)
+  | S of goal * AutoCache.cache_key * candidate * int 
+type elem = 
+  (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
+  menv * subst * int * op list * op list * fail list 
+type status = 
+  (* list of computations that may lead to the solution: all op list will
+   * end with the same (S(g,_)) *)
+  elem list
+type auto_result = 
+  (* menv, subst, alternatives, tables, cache *)
+  | Proved of menv * subst * elem list * AutomationCache.tables * cache 
+  | Gaveup of AutomationCache.tables * cache 
+
+
+(* the status exported to the external observer *)  
+type auto_status = 
+  (* context, (goal,candidate) list, and_list, history *)
+  Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * 
+  (int * Cic.term * int) list * Cic.term Lazy.t list
+
+let d_prefix l =
+  let rec aux acc = function
+    | (D g)::tl -> aux (acc@[g]) tl
+    | _ -> acc
+  in
+    aux [] l
+;;
+
+let calculate_goal_ty (goalno,_,_) s m = 
+  try
+    let _,cc,goalty = CicUtil.lookup_meta goalno m in
+    (* XXX applicare la subst al contesto? *)
+    Some (cc, CicMetaSubst.apply_subst s goalty)
+  with CicUtil.Meta_not_found i when i = goalno -> None
+;;
+
+let calculate_closed_goal_ty (goalno,_,_) s = 
+  try
+    let cc,_,goalty = List.assoc goalno s in
+    (* XXX applicare la subst al contesto? *)
+    Some (cc, CicMetaSubst.apply_subst s goalty)
+  with Not_found -> 
+    None
+;;
+
+let pp_status ctx status = 
+  if debug then 
+  let names = Utils.names_of_context ctx in
+  let pp x = 
+    let x = 
+      ProofEngineReduction.replace 
+        ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false) 
+          ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
+    in
+    CicPp.pp x names
+  in
+  let string_of_do m s (gi,_,_ as g) d =
+    match calculate_goal_ty g s m with
+    | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
+    | None -> Printf.sprintf "D(%d, _, %d)" gi d
+  in
+  let string_of_s m su k (ci,ct) gi =
+    Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
+  in
+  let string_of_ol m su l =
+    String.concat " | " 
+      (List.map 
+        (function 
+          | D (g,d,s) -> string_of_do m su (g,d,s) d 
+          | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi) 
+        l)
+  in
+  let string_of_fl m s fl = 
+    String.concat " | " 
+      (List.map (fun ((i,_,_),ty) -> 
+         Printf.sprintf "(%d, %s)" i (pp ty)) fl)
+  in
+  let rec aux = function
+    | [] -> ()
+    | (m,s,_,_,ol,fl)::tl ->
+        Printf.eprintf "< [%s] ;;; [%s]>\n" 
+          (string_of_ol m s ol) (string_of_fl m s fl);
+        aux tl
+  in
+    Printf.eprintf "-------------------------- status -------------------\n";
+    aux status;
+    Printf.eprintf "-----------------------------------------------------\n";
+;;
+  
+let auto_status = ref [] ;;
+let auto_context = ref [];;
+let in_pause = ref false;;
+let pause b = in_pause := b;;
+let cond = Condition.create ();;
+let mutex = Mutex.create ();;
+let hint = ref None;;
+let prune_hint = ref [];;
+
+let step _ = Condition.signal cond;;
+let give_hint n = hint := Some n;;
+let give_prune_hint hint =
+  prune_hint := hint :: !prune_hint
+;;
+
+let check_pause _ =
+  if !in_pause then
+    begin
+      Mutex.lock mutex;
+      Condition.wait cond mutex;
+      Mutex.unlock mutex
+    end
+;;
+
+let get_auto_status _ = 
+  let status = !auto_status in
+  let and_list,elems,last = 
+    match status with
+    | [] -> [],[],[]
+    | (m,s,_,don,gl,fail)::tl ->
+        let and_list = 
+          HExtlib.filter_map 
+            (fun (id,d,_ as g) -> 
+              match calculate_goal_ty g s m with
+              | Some (_,x) -> Some (id,x,d) | None -> None)
+            (d_goals gl)
+        in
+        let rows = 
+          (* these are the S goalsin the or list *)
+          let orlist = 
+            List.map
+              (fun (m,s,_,don,gl,fail) -> 
+                HExtlib.filter_map
+                  (function S (g,k,c,_) -> Some (g,k,c) | _ -> None) 
+                  (List.rev don @ gl))
+              status
+          in
+          (* this function eats id from a list l::[id,x] returning x, l *)
+          let eat_tail_if_eq id l = 
+            let rec aux (s, l) = function
+              | [] -> s, l
+              | ((id1,_,_),k1,c)::tl when id = id1 ->
+                  (match s with
+                  | None -> aux (Some c,l) tl
+                  | Some _ -> assert false)
+              | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
+            in
+            let c, l = aux (None, []) l in
+            c, List.rev l
+          in
+          let eat_in_parallel id l =
+            let rec aux (b,eaten, new_l as acc) l =
+              match l with
+              | [] -> acc
+              | l::tl ->
+                  match eat_tail_if_eq id l with
+                  | None, l -> aux (b@[false], eaten, new_l@[l]) tl
+                  | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
+            in
+            aux ([],[],[]) l
+          in
+          let rec eat_all rows l =
+            match l with
+            | [] -> rows
+            | elem::or_list ->
+                match List.rev elem with
+                | ((to_eat,depth,_),k,_)::next_lunch ->
+                    let b, eaten, l = eat_in_parallel to_eat l in
+                    let eaten = HExtlib.list_uniq eaten in
+                    let eaten = List.rev eaten in
+                    let b = true (* List.hd (List.rev b) *) in
+                    let rows = rows @ [to_eat,k,b,depth,eaten] in
+                    eat_all rows l
+                | [] -> eat_all rows or_list
+          in
+          eat_all [] (List.rev orlist)
+        in
+        let history = 
+          HExtlib.filter_map
+            (function (S (_,_,(_,c),_)) -> Some c | _ -> None) 
+            gl 
+        in
+(*         let rows = List.filter (fun (_,l) -> l <> []) rows in *)
+        and_list, rows, history
+  in
+  !auto_context, elems, and_list, last
+;;
+
+(* Works if there is no dependency over proofs *)
+let is_a_green_cut goalty =
+  CicUtil.is_meta_closed goalty
+;;
+let rec first_s = function
+  | (D _)::tl -> first_s tl
+  | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
+  | [] -> None
+;;
+let list_union l1 l2 =
+  (* TODO ottimizzare compare *)
+  HExtlib.list_uniq (List.sort compare (l1 @ l1))
+;;
+let rec eq_todo l1 l2 =
+  match l1,l2 with
+  | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
+  | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
+    when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
+      if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
+  | [],[] -> true
+  | _ -> false
+;;
+let eat_head todo id fl orlist = 
+  let rec aux acc = function
+  | [] -> [], acc
+  | (m, s, _, _, todo1, fl1)::tl as orlist -> 
+      let rec aux1 todo1 =
+        match first_s todo1 with
+        | None -> orlist, acc
+        | Some (((gno,_,_),_,_,_), todo11) ->
+            (* TODO confronto tra todo da ottimizzare *)
+            if gno = id && eq_todo todo11 todo then 
+              aux (list_union fl1 acc) tl
+            else 
+              aux1 todo11
+      in
+       aux1 todo1
+  in 
+    aux fl orlist
+;;
+let close_proof p ty menv context = 
+  let metas =
+    List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
+  in
+  let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
+  naif_closure p menv context
+;;
+(* XXX capire bene quando aggiungere alla cache *)
+let add_to_cache_and_del_from_orlist_if_green_cut
+  g s m cache key todo orlist fl ctx size minsize
+= 
+  let cache = cache_remove_underinspection cache key in
+  (* prima per fare la irl usavamo il contesto vero e proprio e non quello 
+   * canonico! XXX *)
+  match calculate_closed_goal_ty g s with
+  | None -> assert false
+  | Some (canonical_ctx , gty) ->
+      let goalno,depth,sort = g in
+      let irl = mk_irl canonical_ctx in
+      let goal = Cic.Meta(goalno, irl) in
+      let proof = CicMetaSubst.apply_subst s goal in
+      let green_proof, closed_proof = 
+        let b = is_a_green_cut proof in
+        if not b then
+          b, (* close_proof proof gty m ctx *) proof 
+        else
+          b, proof
+      in
+      debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
+      if is_a_green_cut key then
+        (* if the initia goal was closed, we cut alternatives *)
+        let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
+        let orlist, fl = eat_head todo goalno fl orlist in
+        let cache = 
+          if size < minsize then 
+            (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
+          else 
+          (* if the proof is closed we cache it *)
+          if green_proof then cache_add_success cache key proof
+          else (* cache_add_success cache key closed_proof *) 
+            (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
+        in
+        cache, orlist, fl, true
+      else
+        let cache = 
+          debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
+          if size < minsize then 
+            (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
+          (* if the substituted goal and the proof are closed we cache it *)
+          if is_a_green_cut gty then
+            if green_proof then cache_add_success cache gty proof
+            else (* cache_add_success cache gty closed_proof *) 
+              (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
+          else (*
+            try
+              let ty, _ =
+                CicTypeChecker.type_of_aux' ~subst:s 
+                  m ctx closed_proof CicUniv.oblivion_ugraph
+              in
+              if is_a_green_cut ty then 
+                cache_add_success cache ty closed_proof
+              else cache
+            with
+            | CicTypeChecker.TypeCheckerFailure _ ->*) 
+          (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
+        in
+        cache, orlist, fl, false
+;;
+let close_failures (fl : fail list) (cache : cache) = 
+  List.fold_left 
+    (fun cache ((gno,depth,_),gty) -> 
+      if CicUtil.is_meta_closed gty then
+       ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
+         cache_add_failure cache gty depth) 
+      else
+         cache)
+    cache fl
+;;
+let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
+  let entry = goalno, (canonical_ctx, t,ty) in
+  assert_subst_are_disjoint subst [entry];
+  let subst = entry :: subst in
+  
+  let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+
+  subst, metasenv
+;;
+
+let mk_fake_proof metasenv subst (goalno,_,_) goalty context = 
+  None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, [] 
+;;
+
+let equational_case 
+  tables cache depth fake_proof goalno goalty subst context 
+    flags
+=
+  let active,passive,bag = tables in
+  let ppterm = ppterm context in
+  let status = (fake_proof,goalno) in
+    if flags.use_only_paramod then
+      begin
+        debug_print (lazy ("PARAMODULATION SU: " ^ 
+                         string_of_int goalno ^ " " ^ ppterm goalty ));
+        let goal_steps, saturation_steps, timeout =
+          max_int,max_int,flags.timeout 
+        in
+        match
+          Saturation.given_clause bag status active passive 
+            goal_steps saturation_steps timeout
+        with 
+          | None, active, passive, bag -> 
+              [], (active,passive,bag), cache, flags
+          | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
+            passive,bag ->
+              assert_subst_are_disjoint subst subst';
+              let subst = subst@subst' in
+              let open_goals = 
+                order_new_goals metasenv subst open_goals ppterm 
+              in
+              let open_goals = 
+                List.map (fun (x,sort) -> x,depth-1,sort) open_goals 
+              in
+              incr candidate_no;
+              [(!candidate_no,proof),metasenv,subst,open_goals], 
+                (active,passive,bag), cache, flags
+      end
+    else
+      begin
+        debug_print (lazy ("NARROWING DEL GOAL: " ^ 
+                         string_of_int goalno ^ " " ^ ppterm goalty ));
+        let goal_steps, saturation_steps, timeout =
+          1,0,flags.timeout 
+        in
+        match
+          Saturation.solve_narrowing bag status active passive goal_steps 
+        with 
+          | None, active, passive, bag -> 
+              [], (active,passive,bag), cache, flags
+          | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
+            passive,bag ->
+              assert_subst_are_disjoint subst subst';
+              let subst = subst@subst' in
+              let open_goals = 
+                order_new_goals metasenv subst open_goals ppterm 
+              in
+              let open_goals = 
+                List.map (fun (x,sort) -> x,depth-1,sort) open_goals 
+              in
+              incr candidate_no;
+              [(!candidate_no,proof),metasenv,subst,open_goals], 
+                (active,passive,bag), cache, flags
+      end
+(*
+      begin
+        let params = ([],["use_context","false"]) in
+        let automation_cache = { 
+              AutomationCache.tables = tables ;
+              AutomationCache.univ = Universe.empty; }
+        in
+        try 
+          let ((_,metasenv,subst,_,_,_),open_goals) =
+
+            solve_rewrite ~params ~automation_cache
+              (fake_proof, goalno)
+          in
+          let proof = lazy (Cic.Meta (-1,[])) in
+          [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
+        with ProofEngineTypes.Fail _ -> [], tables, cache, flags
+(*
+        let res = Saturation.all_subsumed bag status active passive in
+        let res' =
+          List.map 
+            (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
+               assert_subst_are_disjoint subst subst';
+               let subst = subst@subst' in
+               let open_goals = 
+                 order_new_goals metasenv subst open_goals ppterm 
+               in
+               let open_goals = 
+                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals 
+               in
+               incr candidate_no;
+                 (!candidate_no,proof),metasenv,subst,open_goals)
+            res 
+          in
+          res', (active,passive,bag), cache, flags 
+*)
+      end
+*)
+;;
+
+let sort_new_elems = 
+ List.sort (fun (_,_,_,l1) (_,_,_,l2) -> 
+         let p1 = List.length (prop_only l1) in 
+         let p2 = List.length (prop_only l2) in
+         if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
+;;
+
+
+let try_candidate dbd
+  goalty tables subst fake_proof goalno depth context cand 
+=
+  let ppterm = ppterm context in
+  try 
+    let actives, passives, bag = tables in 
+    let (_,metasenv,subst,_,_,_), open_goals =
+       ProofEngineTypes.apply_tactic
+        (PrimitiveTactics.apply_tac ~term:cand)
+        (fake_proof,goalno) 
+    in
+    let tables = actives, passives, 
+      Equality.push_maxmeta bag 
+        (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst)) 
+    in
+    debug_print (lazy ("   OK: " ^ ppterm cand));
+    let metasenv = CicRefine.pack_coercion_metasenv metasenv in
+    let open_goals = order_new_goals metasenv subst open_goals ppterm in
+    let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
+    incr candidate_no;
+    Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables 
+  with 
+    | ProofEngineTypes.Fail s -> None,tables
+    | CicUnification.Uncertain s ->  None,tables
+;;
+
+let applicative_case dbd
+  tables depth subst fake_proof goalno goalty metasenv context 
+  signature universe cache flags
+= 
+  (* let goalty_aux = 
+    match goalty with
+    | Cic.Appl (hd::tl) -> 
+        Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
+    | _ -> goalty
+  in *)
+  let goalty_aux = goalty in
+  let candidates = 
+    get_candidates flags.skip_trie_filtering universe cache goalty_aux
+  in
+  (* if the goal is an equality we skip the congruence theorems 
+  let candidates =
+    if is_equational_case goalty flags 
+    then List.filter not_default_eq_term candidates 
+    else candidates 
+  in *)
+  let candidates = List.filter (only signature context metasenv) candidates 
+  in
+  let tables, elems = 
+    List.fold_left 
+      (fun (tables,elems) cand ->
+        match 
+          try_candidate dbd goalty
+            tables subst fake_proof goalno depth context cand
+        with
+        | None, tables -> tables, elems
+        | Some x, tables -> tables, x::elems)
+      (tables,[]) candidates
+  in
+  let elems = sort_new_elems elems in
+  elems, tables, cache
+;;
+
+let try_smart_candidate dbd
+  goalty tables subst fake_proof goalno depth context cand 
+=
+  let ppterm = ppterm context in
+  try
+    let params = ([],[]) in
+    let automation_cache = { 
+          AutomationCache.tables = tables ;
+          AutomationCache.univ = Universe.empty; }
+    in
+    debug_print (lazy ("candidato per " ^ string_of_int goalno 
+      ^ ": " ^ CicPp.ppterm cand));
+(*
+    let (_,metasenv,subst,_,_,_) = fake_proof in
+    prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
+    prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
+*)
+    let ((_,metasenv,subst,_,_,_),open_goals) =
+      apply_smart ~dbd ~term:cand ~params ~automation_cache
+        (fake_proof, goalno)
+    in
+    let metasenv = CicRefine.pack_coercion_metasenv metasenv in
+    let open_goals = order_new_goals metasenv subst open_goals ppterm in
+    let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
+    incr candidate_no;
+    Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables 
+  with 
+  | ProofEngineTypes.Fail s -> None,tables
+  | CicUnification.Uncertain s ->  None,tables
+;;
+
+let smart_applicative_case dbd
+  tables depth subst fake_proof goalno goalty metasenv context signature
+  universe cache flags
+= 
+  let goalty_aux = 
+    match goalty with
+    | Cic.Appl (hd::tl) -> 
+        Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
+    | _ -> goalty
+  in
+  let smart_candidates = 
+    get_candidates flags.skip_trie_filtering universe cache goalty_aux
+  in
+  let candidates = 
+    get_candidates flags.skip_trie_filtering universe cache goalty
+  in
+  let smart_candidates = 
+    List.filter
+      (fun x -> not(List.mem x candidates)) smart_candidates
+  in 
+  let debug_msg =
+    (lazy ("smart_candidates" ^ " = " ^ 
+             (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
+  debug_print debug_msg;
+  let candidates = List.filter (only signature context metasenv) candidates in
+  let smart_candidates = 
+    List.filter (only signature context metasenv) smart_candidates 
+  in
+(*
+  let penalty cand depth = 
+    if only signature context metasenv cand then depth else ((prerr_endline (
+    "penalizzo " ^ CicPp.ppterm cand));depth -1)
+  in
+*)
+  let tables, elems = 
+    List.fold_left 
+      (fun (tables,elems) cand ->
+        match 
+          try_candidate dbd goalty
+            tables subst fake_proof goalno depth context cand
+        with
+        | None, tables ->
+            (* if normal application fails we try to be smart *)
+           (match try_smart_candidate dbd goalty
+               tables subst fake_proof goalno depth context cand
+            with
+              | None, tables -> tables, elems
+               | Some x, tables -> tables, x::elems)
+        | Some x, tables -> tables, x::elems)
+      (tables,[]) candidates
+  in
+  let tables, smart_elems = 
+      List.fold_left 
+        (fun (tables,elems) cand ->
+          match 
+            try_smart_candidate dbd goalty
+              tables subst fake_proof goalno depth context cand
+          with
+          | None, tables -> tables, elems
+          | Some x, tables -> tables, x::elems)
+        (tables,[]) smart_candidates
+  in
+  let elems = sort_new_elems (elems @ smart_elems) in
+  elems, tables, cache
+;;
+
+let equational_and_applicative_case dbd
+  signature universe flags m s g gty tables cache context 
+=
+  let goalno, depth, sort = g in
+  let fake_proof = mk_fake_proof m s g gty context in
+  if is_equational_case gty flags then
+    let elems,tables,cache, flags =
+      equational_case tables cache
+        depth fake_proof goalno gty s context flags 
+    in
+    let more_elems, tables, cache =
+      if flags.use_only_paramod then
+        [],tables, cache
+      else
+        applicative_case dbd
+          tables depth s fake_proof goalno 
+            gty m context signature universe cache flags
+    in
+      elems@more_elems, tables, cache, flags            
+  else
+    let elems, tables, cache =
+      match LibraryObjects.eq_URI () with
+      | Some _ ->
+         smart_applicative_case dbd tables depth s fake_proof goalno 
+           gty m context signature universe cache flags
+      | None -> 
+         applicative_case dbd tables depth s fake_proof goalno 
+           gty m context signature universe cache flags
+    in
+      elems, tables, cache, flags  
+;;
+let rec condition_for_hint i = function
+  | [] -> false
+  | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
+  | _::tl -> condition_for_hint i tl
+;;
+let prunable_for_size flags s m todo =
+  let rec aux b = function
+    | (S _)::tl -> aux b tl
+    | (D (_,_,T))::tl -> aux b tl
+    | (D g)::tl -> 
+       (match calculate_goal_ty g s m with
+          | None -> aux b tl
+         | Some (canonical_ctx, gty) -> 
+            let gsize, _ = 
+              Utils.weight_of_term 
+               ~consider_metas:false ~count_metas_occurrences:true gty in
+           let newb = b || gsize > flags.maxgoalsizefactor in
+           aux newb tl)
+    | [] -> b
+  in
+    aux false todo
+
+(*
+let prunable ty todo =
+  let rec aux b = function
+    | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
+    | (D (_,_,T))::tl -> aux b tl
+    | D _::_ -> false
+    | [] -> b
+  in
+    aux false todo
+;;
+*)
+
+let prunable menv subst ty todo =
+  let rec aux = function
+    | (S(_,k,_,_))::tl ->
+        (match Equality.meta_convertibility_subst k ty menv with
+         | None -> aux tl
+         | Some variant -> 
+              no_progress variant tl (* || aux tl*))
+    | (D (_,_,T))::tl -> aux tl
+    | _ -> false
+  and no_progress variant = function
+    | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
+    | D ((n,_,P) as g)::tl -> 
+       (match calculate_goal_ty g subst menv with
+           | None -> no_progress variant tl
+           | Some (_, gty) -> 
+              (match calculate_goal_ty g variant menv with
+                 | None -> assert false
+                 | Some (_, gty') ->
+                     if gty = gty' then no_progress variant tl
+(* 
+(prerr_endline (string_of_int n);
+ prerr_endline (CicPp.ppterm gty);
+ prerr_endline (CicPp.ppterm gty');
+ prerr_endline "---------- subst";
+ prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
+ prerr_endline "---------- variant";
+ prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
+ prerr_endline "---------- menv";
+ prerr_endline (CicMetaSubst.ppmetasenv [] menv); 
+                        no_progress variant tl) *)
+                     else false))
+    | _::tl -> no_progress variant tl
+  in
+    aux todo
+
+;;
+let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
+  let s = 
+    HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo 
+  in
+  List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
+;;
+let filter_prune_hint c l =
+  let prune = !prune_hint in
+  prune_hint := []; (* possible race... *)
+  if prune = [] then c,l
+  else 
+    cache_reset_underinspection c,      
+    List.filter (condition_for_prune_hint prune) l
+;;
+
+    
+
+let
+  auto_all_solutions dbd tables universe cache context metasenv gl flags 
+=
+  let signature =
+    List.fold_left 
+      (fun set g ->
+        MetadataConstraints.UriManagerSet.union set 
+            (MetadataQuery.signature_of metasenv g)
+       )
+      MetadataConstraints.UriManagerSet.empty gl 
+  in
+  let goals = order_new_goals metasenv [] gl CicPp.ppterm in
+  let goals = 
+    List.map 
+      (fun (x,s) -> D (x,flags.maxdepth,s)) goals 
+  in
+  let elems = [metasenv,[],1,[],goals,[]] in
+  let rec aux tables solutions cache elems flags =
+    match auto_main dbd tables context flags signature universe cache elems with
+    | Gaveup (tables,cache) ->
+        solutions,cache, tables
+    | Proved (metasenv,subst,others,tables,cache) -> 
+        if Unix.gettimeofday () > flags.timeout then
+          ((subst,metasenv)::solutions), cache, tables
+        else
+          aux tables ((subst,metasenv)::solutions) cache others flags
+  in
+  let rc = aux tables [] cache elems flags in
+    match rc with
+    | [],cache,tables -> [],cache,tables
+    | solutions, cache,tables -> 
+        let solutions = 
+          HExtlib.filter_map
+            (fun (subst,newmetasenv) ->
+              let opened = 
+                ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
+              in
+              if opened = [] then Some subst else None)
+            solutions
+        in
+         solutions,cache,tables
+;;
+
+(******************* AUTO ***************)
+
+
+let auto dbd flags metasenv tables universe cache context metasenv gl =
+  let initial_time = Unix.gettimeofday() in  
+  let signature =
+    List.fold_left 
+      (fun set g ->
+        MetadataConstraints.UriManagerSet.union set 
+            (MetadataQuery.signature_of metasenv g)
+       )
+      MetadataConstraints.UriManagerSet.empty gl 
+  in
+  let goals = order_new_goals metasenv [] gl CicPp.ppterm in
+  let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
+  let elems = [metasenv,[],1,[],goals,[]] in
+  match auto_main dbd tables context flags signature universe cache elems with
+  | Proved (metasenv,subst,_, tables,cache) -> 
+      debug_print(lazy
+        ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
+      Some (subst,metasenv), cache
+  | Gaveup (tables,cache) -> 
+      debug_print(lazy
+        ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
+      None,cache
+;;
+
+let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
+  let flags = flags_of_params params () in
+  let use_library = flags.use_library in
+  let universe, tables, cache =
+    init_cache_and_tables 
+     ~dbd ~use_library ~use_context:(not flags.skip_context)
+     automation_cache univ (proof, goal) 
+  in
+  let _,metasenv,subst,_,_, _ = proof in
+  let _,context,goalty = CicUtil.lookup_meta goal metasenv in
+  let signature = MetadataQuery.signature_of metasenv goal in
+  let signature = 
+    List.fold_left 
+      (fun set t ->
+         let ty, _ = 
+          CicTypeChecker.type_of_aux' metasenv context t 
+            CicUniv.oblivion_ugraph
+        in
+        MetadataConstraints.UriManagerSet.union set 
+          (MetadataConstraints.constants_of ty)
+       )
+      signature univ
+  in
+  let tables,cache =
+    if flags.close_more then
+      close_more 
+        tables context (proof, goal) 
+          (auto_all_solutions dbd) signature universe cache 
+    else tables,cache in
+  let initial_time = Unix.gettimeofday() in
+  let (_,oldmetasenv,_,_,_, _) = proof in
+    hint := None;
+  let elem = 
+    metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
+  in
+  match auto_main dbd tables context flags signature universe cache [elem] with
+    | Proved (metasenv,subst,_, tables,cache) -> 
+        debug_print (lazy 
+          ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
+        let proof,metasenv =
+        ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+          proof goal subst metasenv
+        in
+        let opened = 
+          ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+            ~newmetasenv:metasenv
+        in
+          proof,opened
+    | Gaveup (tables,cache) -> 
+        debug_print
+          (lazy ("TIME:"^
+            string_of_float(Unix.gettimeofday()-.initial_time)));
+        raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+;;
+*)
+
+module CacheElem : Set.OrderedType =
+ struct
+  type t = 
+   | Failed_in of int * NCic.term     (* depth, goal type *)
+   | Succeded of Cic.term * Cic.term  (* proof, proof type *)
+   | UnderInspection of Cic.term      (* avoid looping *)
+
+  let compare = Pervasives.compare
+ end
+
+module CacheSet = Set.Make(CacheElem)
+module Cache = 
+  Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CacheSet)
+
+type cache_examination_result =
+  [ `Failed_in of int
+  | `UnderInspection 
+  | `Succeded of NCic.term
+  | `NotFound
+  ]
+
+type sort = T | P
+type goal = int * int * sort
+type fail = goal * NCic.term
+type candidate = NCic.term
+type menv = NCic.metasenv
+type subst = NCic.substitution
+
+type op = 
+  (* goal has to be proved *)
+  | D of goal 
+  (* goal has to be cached as a success obtained using candidate as the first
+   * step *)
+  | S of goal * Cache.input * candidate (* int was minsize *)
+type elem = 
+  (* menv, subst, size, operations done (only S), operations to do, 
+   * failures to cache if any op fails *)
+  menv * subst * int * op list * op list * fail list 
+
+type auto_status = 
+  (* list of computations that may lead to the solution: all op list will
+   * end with the same (S(g,_)) *)
+  elem list * Cache.t
+
+type auto_result = 
+  | Gaveup 
+  | Proved of menv * subst * auto_status (* the alternative proofs *)
+
+type flags = {
+        do_types : bool; (* solve goals in Type *)
+        maxwidth : int;
+        maxsize  : int;
+        timeout  : float;
+}
+
+let close_failures = assert false;;
+let equational_and_applicative_case = assert false;;
+let prunable = assert false;;
+let cache_examine = assert false;;
+let put_in_subst = assert false;;
+let calculate_goal_ty = assert false;;
+let add_to_cache_and_del_from_orlist_if_green_cut = assert false;;
+let cache_add_underinspection = assert false;;
+
+let d_goals l =
+  let rec aux acc = function
+    | (D g)::tl -> aux (acc@[g]) tl
+    | (S _)::tl -> aux acc tl
+    | [] -> acc
+  in
+    aux [] l
+;;
+let prop_only l =
+  List.filter (function (_,_,P) -> true | _ -> false) l
+;;
+let remove_s_from_fl (id,_,_) (fl : fail list) =
+  let rec aux = function
+    | [] -> []
+    | ((id1,_,_),_)::tl when id = id1 -> tl
+    | hd::tl ->  hd :: aux tl
+  in 
+    aux fl
+;;
+
+let auto_main status context flags signature elems cache =
+  let rec aux (elems, cache : auto_status) =
+(* processa le hint dell'utente *)
+(*     let cache, elems = filter_prune_hint cache elems in *)
+    match elems with
+(* USER HINT
+    | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
+       debug_print (lazy "skip");
+        (match !hint with
+        | Some i when condition_for_hint i todo ->
+            aux tables flags cache orlist
+        | _ ->
+          hint := None;
+          aux tables flags cache elems)
+*)
+    | [] ->
+        (* complete failure *)
+        debug_print (lazy "gave up");
+        Gaveup
+    | (m, s, _, _, [],_)::orlist ->
+        (* complete success *)
+        debug_print (lazy "success");
+        Proved (m, s, (orlist, cache))
+    | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist 
+      when not flags.do_types ->
+        (* skip since not Prop, don't even check if closed by side-effect *)
+        debug_print (lazy "skip goal in Type");
+        aux ((m, s, size, don, todo, fl)::orlist, cache)
+    | (m, s, size, don, (S(g, key, c) as op)::todo, fl)::orlist ->
+        (* partial success, cache g and go on *)
+        let cache, orlist, fl, sibling_pruned = 
+          add_to_cache_and_del_from_orlist_if_green_cut 
+            g s m cache key todo orlist fl context size 
+        in
+        let fl = remove_s_from_fl g fl in
+        let don = if sibling_pruned then don else op::don in
+        aux ((m, s, size, don, todo, fl)::orlist, cache)
+    | (m, s, size, don, todo, fl)::orlist 
+      when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
+        debug_print (lazy ("FAIL: WIDTH"));
+        aux (orlist, cache)
+    | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
+        debug_print (lazy ("FAIL: SIZE: "^string_of_int size ^ 
+            " > " ^ string_of_int flags.maxsize ));
+        aux (orlist, cache)
+    | _ when Unix.gettimeofday () > flags.timeout ->
+        debug_print (lazy ("FAIL: TIMEOUT"));
+        Gaveup 
+    | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
+        debug_print (lazy "attack goal");
+        match calculate_goal_ty g s m with
+        | None -> 
+            debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
+            aux ((m,s,size,don,todo, fl)::orlist, cache)
+        | Some (canonical_ctx, gty) ->
+            debug_print (lazy ("EXAMINE: "^
+              NCicPp.ppterm ~metasenv:m ~subst:s ~context gty));
+            match cache_examine cache gty with
+            | `Failed_in d when d >= depth -> 
+                debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
+                let cache = close_failures fl cache in
+                aux (orlist, cache)
+            | `UnderInspection -> 
+                debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
+                let cache = close_failures fl cache in
+                aux (orlist,cache)
+            | `Succeded t -> 
+                debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
+                let s, m = put_in_subst s m g canonical_ctx t gty in
+                aux ((m, s, size, don,todo, fl)::orlist, cache)
+            | `Notfound 
+            | `Failed_in _ when depth > 0 -> 
+                ( (* more depth or is the first time we see the goal *)
+                    if prunable m s gty todo then
+                      (debug_print (lazy( "FAIL: LOOP: one father is equal"));
+                       let cache = close_failures fl cache in
+                       aux (orlist,cache))
+                    else
+                    let cache = cache_add_underinspection cache gty depth in
+                    debug_print (lazy ("INSPECTING: " ^ 
+                        string_of_int gno ^ "("^ string_of_int size ^ "): "^
+                        NCicPp.ppterm ~metasenv:m ~subst:s ~context gty));
+                    (* elems are possible computations for proving gty *)
+                    let elems =
+                      equational_and_applicative_case 
+                        signature status flags m s g gty cache context
+                    in
+                    if elems = [] then
+                      (* this goal has failed *)
+                      let cache = close_failures ((g,gty)::fl) cache in
+                      aux (orlist, cache)
+                    else
+                      let size_gl l = List.length 
+                        (List.filter (function (_,_,P) -> true | _ -> false) l) 
+                      in
+                      let elems = 
+                        let inj_gl gl = List.map (fun g -> D g) gl in
+                        let rec map = function
+                          | [] -> assert false
+                          | (cand,m,s,gl)::[] ->
+                              let todo = 
+                                inj_gl gl @ (S(g,gty,cand))::todo 
+                              in
+                              (* we are the last in OR, we fail on g and 
+                               * also on all failures implied by g *)
+                              (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
+                              :: orlist
+                          | (cand,m,s,gl)::tl -> 
+                              let todo = 
+                                inj_gl gl @ (S(g,gty,cand))::todo 
+                              in
+                              (m,s, size + size_gl gl, don, todo, []) :: map tl
+                        in
+                          map elems
+                      in
+                        aux (elems, cache))
+            | _ -> 
+                debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
+                let cache = close_failures fl cache in
+                aux (orlist, cache)
+  in
+    (aux (elems, cache) : auto_result)
+;;
+
 let auto_tac ~params status =
   prerr_endline "I teoremi noti sono";
   NDiscriminationTree.DiscriminationTree.iter status#auto_cache
@@ -60,6 +1131,7 @@ let auto_tac ~params status =
   status
 ;;
 
+
 (* ========================= dispatching of auto/auto_paramod ============ *)
 let auto_tac ~params:(_,flags as params) =
   if List.mem_assoc "paramodulation" flags then