From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 7 Nov 2011 09:09:24 +0000 (+0000)
Subject: Removed some dead code.
X-Git-Tag: make_still_working~2132
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e7d3d4fe448f615e0ff4202331382fc45bb4e1ca;p=helm.git

Removed some dead code.
---

diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml
index 201f522d0..a85c18205 100644
--- a/matitaB/components/ng_tactics/nnAuto.ml
+++ b/matitaB/components/ng_tactics/nnAuto.ml
@@ -1174,130 +1174,9 @@ let applicative_case depth signature status flags gty cache =
     try_candidates false 2 elems smart_candidates_other
 ;;
 
-
-(*
-let get_candidates ?(smart=true) depth flags status cache signature gty =
-  let maxd = ((depth + 1) = flags.maxdepth) in 
-  let universe = status#auto_cache in
-  let _,_,metasenv,subst,_ = status#obj in
-  let context = ctx_of gty in
-  let _, raw_gty = term_of_cic_term status gty context in
-  debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
-  let raw_weak_gty, weak_gty  =
-    if smart then
-      match raw_gty with
-	| NCic.Appl _ 
-	| NCic.Const _ 
-	| NCic.Rel _ -> 
-            let raw_weak = 
-              perforate_small status subst metasenv context raw_gty in
-            let weak = mk_cic_term context raw_weak in
-            debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
-              Some raw_weak, Some (weak)
-	| _ -> None,None
-    else None,None
-  in
-  let global_cands, smart_global_cands =
-    match flags.candidates with
-      | Some l when (not maxd) -> l,[]
-      | Some _ 
-      | None -> 
-	  let mapf s = 
-	    let to_ast = function 
-	      | NCic.Const r when true (*is_relevant statistics r*) -> Some (Ast.NRef r)
-	(*       | NCic.Const _ -> None  *)
-	      | _ -> assert false in
-	      HExtlib.filter_map 
-		to_ast (NDiscriminationTree.TermSet.elements s) in
-	  let g,l = 
-	    get_cands
-	      (NDiscriminationTree.DiscriminationTree.retrieve_unifiables 
-		 universe)
-	      NDiscriminationTree.TermSet.diff 
-	      NDiscriminationTree.TermSet.empty
-	      raw_gty raw_weak_gty in
-	    mapf g, mapf l in
-  let local_cands,smart_local_cands = 
-    let mapf s = 
-      let to_ast t =
-	let _status, t = term_of_cic_term status t context 
-	in Ast.NCic t in
-	List.map to_ast (Ncic_termSet.elements s) in
-    let g,l = 
-      get_cands
-	(fun ty -> search_in_th ty cache)
-	Ncic_termSet.diff  Ncic_termSet.empty gty weak_gty in
-      mapf g, mapf l in
-    sort_candidates status context (global_cands@local_cands),
-    sort_candidates status context (smart_global_cands@smart_local_cands)
-;; 
-
-let applicative_case depth signature status flags gty cache =
-  app_counter:= !app_counter+1; 
-  let _,_,metasenv,subst,_ = status#obj in
-  let context = ctx_of gty in
-  let tcache = cache.facts in
-  let is_prod, is_eq =   
-    let status, t = term_of_cic_term status gty context  in 
-    let t = NCicReduction.whd status subst context t in
-      match t with
-	| NCic.Prod _ -> true, false
-	| _ -> false, NCicParamod.is_equation status metasenv subst context t 
-  in
-  debug_print ~depth (lazy (string_of_bool is_eq)); 
-  (* new *)
-  let candidates, smart_candidates = 
-    get_candidates ~smart:true depth 
-      flags status tcache signature gty in 
-  let test = is_a_fact_ast status subst metasenv context in
-  let candidates_facts,candidates_other =
-    (* if the goal is an equation we avoid to apply unit equalities,
-     since superposition should take care of them; refl is an
-     exception since it prompts for convertibility *)
-    let l1,l2 = List.partition test candidates in
-    (* put the right uri *)
-    if is_eq then [Ast.Ident("refl",`Ambiguous)],l2 else l1,l2
-  in
-  let smart_candidates_facts, smart_candidates_other =
-    match flags.candidates with
-    | Some l -> [],l
-    | None ->
-        let l1,l2 = List.partition test smart_candidates in
-        if is_eq then [],l2 else l1,l2
-  in
-  let sm = if is_eq then 0 else 2 in
-  let sm1 = if flags.last then 2 else 0 in
-  let maxd = (depth + 1 = flags.maxdepth) in 
-  let try_candidates only_one sm acc candidates =
-    List.fold_left 
-      (fun elems cand ->
-         if (only_one && (elems <> [])) then elems 
-         else
-           match try_candidate (~smart:sm) 
-             flags depth status cache.unit_eq context cand with
-               | None -> elems
-               | Some x -> x::elems)
-      acc candidates
-  in 
-  (* if the goal is the last one we stop at the first fact *)
-  let elems = try_candidates flags.last sm [] candidates_facts in
-  (* now we add smart_facts *)
-  let elems = try_candidates flags.last sm elems smart_candidates_facts in
-  (* if we are at maxdepth and the goal is not a product we are done 
-     similarly, if the goal is the last one and we already found a
-     solution *)
-  if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
-  else
-    let elems = try_candidates false 2 elems candidates_other in
-    debug_print ~depth (lazy ("not facts: try smart application"));
-    try_candidates false 2 elems smart_candidates_other
-;; *)
-
 exception Found
 ;; 
 
-
-
 (* gty is supposed to be meta-closed *)
 let is_subsumed depth filter_depth status gty cache =
   if cache=[] then false else (