Matitaweb:

[helm.git] / matitaB / components / ng_tactics / nnAuto.ml

diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml
index a85c18205d7a6aef840fc44eca134b8867d7476c..38e19486b36ead0682dff766b3563c8d2405547d 100644 (file)
--- a/matitaB/components/ng_tactics/nnAuto.ml
+++ b/matitaB/components/ng_tactics/nnAuto.ml
@@ -14,7 +14,7 @@ open Printf
 let print ?(depth=0) s = 
   prerr_endline (String.make (2*depth) ' '^Lazy.force s) 
 let noprint ?(depth=0) _ = () 
-let debug_print = noprint
+let debug_print = print
 
 open Continuationals.Stack
 open NTacStatus
@@ -146,9 +146,11 @@ let is_a_fact_ast status subst metasenv ctx cand =
  let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
    is_a_fact status (mk_cic_term ctx ty)
 
-let current_goal status = 
+let current_goal ?(single_goal=true) status = 
   let open_goals = head_goals status#stack in
-  assert (List.length open_goals  = 1);
+  if single_goal 
+     then assert (List.length open_goals  = 1)
+     else assert (List.length open_goals >= 1);
   let open_goal = List.hd open_goals in
   let gty = get_goalty status open_goal in
   let ctx = ctx_of gty in
@@ -854,7 +856,7 @@ type cache =
 let add_to_trace status ~depth cache t =
   match t with
     | Ast.NRef _ -> 
-       debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
+       print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
        {cache with trace = t::cache.trace}
     | Ast.NCic _  (* local candidate *)
     | _  -> (*not an application *) cache 
@@ -1732,15 +1734,22 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
         (NDiscriminationTree.TermSet.elements t))
       )));
 *)
-  let candidates = 
+  (* To allow using Rels in the user-specified candidates, we need a context
+   * but in the case where multiple goals are open, there is no single context
+   * to type the Rels. At this time, we require that Rels be typed in the
+   * context of the first selected goal *)
+  let _,ctx,_ = current_goal ~single_goal:false status in
+  let status, candidates = 
     match univ with
-      | None -> None 
+      | None -> status, None 
       | Some l -> 
-         let to_Ast t =
-           let status, res = disambiguate status [] t None in 
-           let _,res = term_of_cic_term status res (ctx_of res) 
-           in Ast.NCic res 
-          in Some (List.map to_Ast l) 
+         let to_Ast (st,l) t =
+           let st, res = disambiguate st ctx t None in 
+           let st, res = term_of_cic_term st res (ctx_of res) 
+           in (st, Ast.NCic res::l)
+          in 
+          let status, l' = List.fold_left to_Ast (status,[]) l in
+          status, Some l'
   in 
   let depth = int "depth" flags 3 in 
   let size  = int "size" flags 10 in 
@@ -1779,6 +1788,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
           | Proved (s,trace) -> 
               debug_print (lazy ("proved at depth " ^ string_of_int x));
              List.iter (toref incr_uses statistics) trace;
+             let _ = debug_print (pptrace status trace) in
               let trace = cleanup_trace s trace in
              let _ = debug_print (pptrace status trace) in
               let stack =