X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=fd8d776c180749023a85e4c87a4d266113482aa0;hb=f8d45b2e4fa7817d7ef8312b3bb8a7439bd7fb8c;hp=71ac2939a7c8d6a7ab94c17a584871c19ec6eabc;hpb=46b29739a529f639c3f34b038a6070a3a573db41;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 71ac2939a..fd8d776c1 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
@@ -819,11 +868,18 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
             List.fold_left
              (fun (status,uris) boxml ->
                try
-                let status,nuris =
+                let nstatus,nuris =
                  eval_ncommand opts status
                   ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
                 in
-                status, concat_nuris uris nuris
+                if nstatus#ng_mode <> `CommandMode then
+                  begin
+                    HLog.error "error in generating projection/eliminator";
+                    prerr_endline (NCicPp.ppobj nstatus#obj);
+                    nstatus, uris
+                  end
+                else
+                  nstatus, concat_nuris uris nuris
                with
                | MultiPassDisambiguator.DisambiguationError _ 
                | NCicTypeChecker.TypeCheckerFailure _ ->
@@ -845,6 +901,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                        fst (match menv with
                              [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
                            | _ -> status,`New []))
+                       (* XXX *)
                       with _ -> HLog.warn "error in generating inversion principle"; 
                                 let status = status#set_ng_mode `CommandMode in status)
                   status