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=9fa8dbb000a30e17e20b5f221b142b5cf77db098;hpb=ec07ff398325533d848da92e9dc69852d24b78a5;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 9fa8dbb00..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,13 +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 (_,_,_, ty, _) ->
-      [ 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, _) ->
+     [ 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
@@ -692,7 +744,7 @@ let eval_ng_tac tac =
           (text,prefix_len,concl))
        ) seqs)
   | GrafiteAst.NAuto (_loc, (l,a)) ->
-      NTactics.auto_tac
+      NAuto.auto_tac
 	~params:(List.map (fun x -> "",0,x) l,a)
   | GrafiteAst.NBranch _ -> NTactics.branch_tac 
   | GrafiteAst.NCases (_loc, what, where) ->
@@ -816,17 +868,47 @@ 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 _ ->
                   HLog.warn "error in generating projection/eliminator";
                   status,uris
-             ) (status,`New [] (* uris *)) boxml in
+             ) (status,`New [] (* uris *)) boxml in             
+           let _,_,_,_,nobj = obj in 
+           let status = match nobj with
+               NCic.Inductive (true,leftno,[it],_) ->
+                 let _,ind_name,ty,cl = it in
+                 List.fold_left 
+                   (fun status outsort ->
+                      let status = status#set_ng_mode `ProofMode in
+                      try
+                       (let status,invobj = NInversion.mk_inverter 
+                                      (ind_name ^ "_inv_" ^ (snd (NCicElim.ast_of_sort outsort))) 
+                                      it leftno outsort status status#baseuri in
+                       let _,_,menv,_,_ = invobj in
+                       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
+                  (NCic.Prop::
+                    List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
+              | _ -> status
+           in
            let coercions =
             match obj with
               _,_,_,_,NCic.Inductive