From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 16 Oct 2009 12:40:36 +0000 (+0000)
Subject: better indexing for auto
X-Git-Tag: make_still_working~3287
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a63a5994b882fc391f6ec9b67a83e9777157b1ff;p=helm.git

better indexing for auto
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 71ac2939a..aea900cdf 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -507,8 +507,10 @@ let eval_unification_hint status t n =
 let basic_index_obj l status =
   status#set_auto_cache 
     (List.fold_left
-      (fun t (k,v) -> 
-         NDiscriminationTree.DiscriminationTree.index t k v) 
+      (fun t (ks,v) -> 
+         List.fold_left (fun t k ->
+           NDiscriminationTree.DiscriminationTree.index t k v)
+          t ks) 
     status#auto_cache l) 
 ;;     
 
@@ -519,7 +521,7 @@ let record_index_obj =
  =
     basic_index_obj
       (List.map 
-        (fun k,v -> refresh_uri_in_term k, refresh_uri_in_term v) 
+        (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v) 
       l)
  in
   NCicLibrary.Serializer.register#run "index_obj"
@@ -529,16 +531,63 @@ let record_index_obj =
 ;;
 
 let index_obj_for_auto status (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 _ -> []
-  | NCic.Inductive _ -> []
-  | NCic.Constant (_,_,Some _, ty, _) ->
-     let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in
-      [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Def height))]
+  | 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, _) ->
-     let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in
-      [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Decl))]
+     [ 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