removed misleading context

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index fbb43cbb0298d3e5c40113b761256a3eeec2c029..37ac72eb987c76ab9e98eef2c135c7ed7273ad86 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -936,7 +936,7 @@ type cache_examination_result =
 type sort = T | P
 type goal = int * int * sort (* goal, depth, sort *)
 type fail = goal * cic_term
-type candidate = int * NCic.term (* unique candidate number, candidate *)
+type candidate = int * Ast.term (* unique candidate number, candidate *)
 
 type op = 
   (* goal has to be proved *)
@@ -969,9 +969,9 @@ let close_failures _ c = c;;
 let prunable _ _ _ = false;;
 let cache_examine cache gty = `Notfound;;
 let put_in_subst s _ _ _  = s;;
-let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ _ = c, o, f, false ;; 
+let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; 
 let cache_add_underinspection c _ _ = c;;
-let equational_case _ _ _ _ _ _ _ = [];;
+let equational_case _ _ _ _ _ _ = [];;
 let sort_new_elems l = l;;
 let only _ _ _ = true;;
 
@@ -979,37 +979,42 @@ let candidate_no = ref 0;;
 
 let try_candidate status t g =
  try
-   debug_print (lazy (" try " ^ 
-     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t
-   ));
-   let ast_for_t = 
-     match t with
-     | NCic.Rel i -> assert false
-     | NCic.Const ref -> Ast.NRef ref
-     | _ -> assert false
-   in
+   debug_print (lazy (" try " ^ CicNotationPp.pp_term t));
    let status = NTactics.focus_tac [g] status in
-   let status = NTactics.apply_tac ("",0,ast_for_t) status in
+   let status = NTactics.apply_tac ("",0,t) status in
    let open_goals = head_goals status#stack in
+   debug_print 
+     (lazy (" success: "^String.concat " "(List.map string_of_int open_goals)));
    incr candidate_no;
    Some ((!candidate_no,t),status,open_goals)
- with Error (msg,exn) -> debug_print msg; None
+ with Error (msg,exn) -> debug_print (lazy " failed"); None
 ;;
 
+let rec mk_irl n = function
+  | [] -> []
+  | _ :: tl -> NCic.Rel n :: mk_irl (n+1) tl
+;;
 
-let get_candidates status context gty =
+let get_candidates status signature gty =
   let universe = status#auto_cache in
-  let _, gty = term_of_cic_term status gty (ctx_of gty) in
+  let context = ctx_of gty in
+  let _, gty = term_of_cic_term status gty context in
   let cands = 
     NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty
   in
-  (* XXX we have to trie for the context *)
-  NDiscriminationTree.TermSet.elements cands
+  let cands = 
+    List.filter (only signature context) 
+      (NDiscriminationTree.TermSet.elements cands)
+  in
+  (* XXX we have to use the trie for the context *)
+  HExtlib.filter_map (fun name,_ -> 
+    if name <> "_" then Some (Ast.Ident (name,None)) else None) context 
+  @ 
+  List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
 ;;
 
-let applicative_case signature status flags g gty cache context = 
-  let candidates = get_candidates status context gty in
-  let candidates = List.filter (only signature context) candidates in
+let applicative_case signature status flags g gty cache = 
+  let candidates = get_candidates status signature gty in
   debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates)));
   let elems = 
     List.fold_left 
@@ -1023,17 +1028,17 @@ let applicative_case signature status flags g gty cache context =
 ;;
 
 let equational_and_applicative_case
-  signature flags status g depth gty cache context
+  signature flags status g depth gty cache 
 =
  let elems = 
   if false (*is_equational_case gty flags*) then
     let elems =
       equational_case
-        signature status flags g gty cache context
+        signature status flags g gty cache 
     in
     let more_elems =
         applicative_case 
-          signature status flags g gty cache context
+          signature status flags g gty cache 
     in
       elems@more_elems
   else
@@ -1044,7 +1049,7 @@ let equational_and_applicative_case
            gty m context signature universe cache flags
       | None -> *)
          applicative_case 
-          signature status flags g gty cache context
+          signature status flags g gty cache 
     in
       elems
  in
@@ -1080,7 +1085,7 @@ let remove_s_from_fl (id,_,_) (fl : fail list) =
     aux fl
 ;;
 
-let auto_main context flags signature elems cache =
+let auto_main flags signature elems cache =
   let rec aux (elems, cache : 'a auto_status) =
 (* processa le hint dell'utente *)
 (*     let cache, elems = filter_prune_hint cache elems in *)
@@ -1108,7 +1113,7 @@ let auto_main context flags signature elems cache =
     | (s, size, don, (S(g, key, c) as op)::todo, fl)::orlist ->
         let cache, orlist, fl, sibling_pruned = 
           add_to_cache_and_del_from_orlist_if_green_cut 
-            g s cache key todo orlist fl context size 
+            g s cache key todo orlist fl size 
         in
         let fl = remove_s_from_fl g fl in
         let don = if sibling_pruned then don else op::don in
@@ -1161,7 +1166,7 @@ let auto_main context flags signature elems cache =
                     (* elems are possible computations for proving gty *)
                     let elems =
                       equational_and_applicative_case 
-                        signature flags s gno depth gty cache context
+                        signature flags s gno depth gty cache 
                     in
                     if elems = [] then
                       (* this goal has failed *)
@@ -1203,18 +1208,18 @@ let auto_main context flags signature elems cache =
 let auto_tac ~params status =
   let cache = Cache.empty in
   let goals = head_goals status#stack in
-  let depth = 3 in (* XXX fix sort *)
+  let depth = 3 in 
+  (* XXX fix sort *)
   let goals = List.map (fun i -> D(i,depth,P)) goals in
   let elems = [status,0,[],goals,[]] in
-  let context = [] (* XXX big problem *) in
   let signature = () in
   let flags = { 
-          maxwidth = 3; 
+          maxwidth = 3 + List.length goals; 
           maxsize = 10; 
           timeout = Unix.gettimeofday() +. 3000.;
           do_types = false; 
   } in
-  match auto_main context flags signature elems cache with
+  match auto_main flags signature elems cache with
   | Gaveup -> raise (Error (lazy "auto gave up", None))
   | Proved (s, (_orlist, _cache)) -> 
       let stack =