Tracing mechanism for auto. Interface changed to solve an ambiguity between

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 520289aa1f39d1f17886314c901991dc8ad4d843..4d7b8ce4e9d8494da2fcf79cae1f383929beb289 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -530,69 +530,77 @@ let record_index_obj =
    end
 ;;
 
+let compute_keys uri height kind = 
+  let mk_item orig_ty spec =
+    let ty,_,_ = NCicMetaSubst.saturate ~delta:max_int [] [] [] orig_ty 0 in
+    let keys = 
+      match ty with
+       | NCic.Const (NReference.Ref (_,NReference.Def h)) 
+       | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Def h))::_) 
+            when h > 0 ->
+            let ty',_,_= 
+             NCicMetaSubst.saturate ~delta:(h-1) [] [] [] orig_ty 0 in
+              [ty;ty']
+       | _ -> [ty] 
+    in 
+      keys,NCic.Const(NReference.reference_of_spec uri spec) 
+  in
+  let data = 
+    match kind with
+      | NCic.Fixpoint (ind,ifl,_) -> 
+         HExtlib.list_mapi 
+           (fun (_,_,rno,ty,_) i -> 
+               if ind then mk_item ty (NReference.Fix (i,rno,height)) 
+               else mk_item ty (NReference.CoFix height)) ifl
+      | NCic.Inductive (b,lno,itl,_) -> 
+         HExtlib.list_mapi 
+           (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl 
+         @
+           List.map 
+           (fun ((_,_,ty),i,j) -> 
+              mk_item ty (NReference.Con (i,j+1,lno)))
+           (List.flatten 
+              (HExtlib.list_mapi 
+                 (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl)
+                 itl))
+      | NCic.Constant (_,_,Some _, ty, _) -> 
+         [ mk_item ty (NReference.Def height) ]
+      | NCic.Constant (_,_,None, ty, _) ->
+         [ mk_item ty NReference.Decl ]
+  in
+  let data = HExtlib.filter_map
+    (fun (keys, t) ->
+       let keys = List.filter
+        (function 
+            | (NCic.Meta _) 
+            | (NCic.Appl (NCic.Meta _::_)) -> false 
+            | _ -> true) 
+        keys
+       in
+        if keys <> [] then 
+          begin
+             HLog.debug ("Indexing:" ^ 
+               NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+             HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t ->
+               NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
+             Some (keys,t) 
+          end
+        else 
+          begin
+             HLog.debug ("Not indexing:" ^ 
+              NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+             None
+          end)
+    data
+  in data
+;;
+
 let index_obj_for_auto status (uri, height, _, _, kind) = 
  (*prerr_endline (string_of_int height);*)
- let mk_item orig_ty spec =
-   let ty,_,_ = NCicMetaSubst.saturate ~delta:max_int [] [] [] orig_ty 0 in
-   let keys = 
-     match ty with
-     | NCic.Const (NReference.Ref (_,NReference.Def h)) 
-     | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Def h))::_) 
-        when h > 0 ->
-          let ty',_,_= NCicMetaSubst.saturate ~delta:(h-1) [] [] [] orig_ty 0 in
-          [ty;ty']
-     | _ -> [ty]
-   in
-   keys,NCic.Const(NReference.reference_of_spec uri spec)
- in
- let data = 
-  match kind with
-  | NCic.Fixpoint (ind,ifl,_) -> 
-     HExtlib.list_mapi 
-       (fun (_,_,rno,ty,_) i -> 
-          if ind then mk_item ty (NReference.Fix (i,rno,height)) 
-          else mk_item ty (NReference.CoFix height)) ifl
-  | NCic.Inductive (b,lno,itl,_) -> 
-     HExtlib.list_mapi 
-       (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl 
-     @
-     List.map (fun ((_,_,ty),i,j) -> mk_item ty (NReference.Con (i,j+1,lno)))
-       (List.flatten (HExtlib.list_mapi 
-         (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl)
-         itl))
-  | NCic.Constant (_,_,Some _, ty, _) -> 
-     [ mk_item ty (NReference.Def height) ]
-  | NCic.Constant (_,_,None, ty, _) ->
-     [ mk_item ty NReference.Decl ]
- in
- let data = HExtlib.filter_map
-   (fun (keys, t) ->
-     let keys = List.filter
-       (function 
-         | (NCic.Meta _) 
-         | (NCic.Appl (NCic.Meta _::_)) -> false 
-         | _ -> true) 
-       keys
-     in
-     if keys <> [] then 
-      begin
-        HLog.debug ("Indexing:" ^ 
-          NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
-        HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t ->
-          NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
-        Some (keys,t) 
-      end
-     else 
-      begin
-        HLog.debug ("Not indexing:" ^ 
-          NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
-        None
-      end)
-   data
- in
- let status = basic_index_obj data status in
- let dump = record_index_obj data :: status#dump in
- status#set_dump dump
+  let data = compute_keys uri height kind in
+  let status = basic_index_obj data status in
+  let dump = record_index_obj data :: status#dump in   
+  status#set_dump dump
 ;; 
 
 let index_eq uri status =
@@ -776,9 +784,10 @@ let eval_ng_tac tac =
            ) hyps,
           (text,prefix_len,concl))
        ) seqs)
-  | GrafiteAst.NAuto (_loc, (l,a)) ->
+  | GrafiteAst.NAuto (_loc, (None,a)) -> NAuto.auto_tac ~params:(None,a)
+  | GrafiteAst.NAuto (_loc, (Some l,a)) ->
       NAuto.auto_tac
-       ~params:(List.map (fun x -> "",0,x) l,a)
+       ~params:(Some List.map (fun x -> "",0,x) l,a)
   | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
   | GrafiteAst.NCases (_loc, what, where) ->
       NTactics.cases_tac