X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=fe2da884d4c1f02c2c808e97b2c40fe9fa522a88;hb=2589e631ad9c04a89cb7730d6bca913aed016f98;hp=520289aa1f39d1f17886314c901991dc8ad4d843;hpb=f54d5fd0caa8c15b6f12d7c91b0ee1bfa5a1b16e;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 520289aa1..fe2da884d 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -530,18 +530,15 @@ let record_index_obj =
    end
 ;;
 
-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]
+let compute_keys status uri height kind = 
+ let mk_item ty spec =
+   let orig_ty = NTacStatus.mk_cic_term [] ty in
+   let status,keys = NnAuto.keys_of_type status orig_ty in
+   let keys =  
+     List.map 
+       (fun t -> 
+	  snd (NTacStatus.term_of_cic_term status t (NTacStatus.ctx_of t)))
+       keys
    in
    keys,NCic.Const(NReference.reference_of_spec uri spec)
  in
@@ -565,7 +562,7 @@ let index_obj_for_auto status (uri, height, _, _, kind) =
   | NCic.Constant (_,_,None, ty, _) ->
      [ mk_item ty NReference.Decl ]
  in
- let data = HExtlib.filter_map
+  HExtlib.filter_map
    (fun (keys, t) ->
      let keys = List.filter
        (function 
@@ -588,11 +585,15 @@ let index_obj_for_auto status (uri, height, _, _, kind) =
           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
+    data
+;;
+
+let index_obj_for_auto status (uri, height, _, _, kind) = 
+ (*prerr_endline (string_of_int height);*)
+  let data = compute_keys status 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 +777,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 
@@ -945,15 +947,17 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
              ) (status,`New [] (* uris *)) boxml in             
            let _,_,_,_,nobj = obj in 
            let status = match nobj with
-               NCic.Inductive (true,leftno,[it],_) ->
+               NCic.Inductive (is_ind,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 status,invobj =
+                         NInversion.mk_inverter 
+                          (ind_name ^ "_inv_" ^
+                            (snd (NCicElim.ast_of_sort outsort)))
+                          is_ind 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)
@@ -1090,7 +1094,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
             indtyno, NCicEnvironment.get_checked_indtys r
         | _ -> prerr_endline ("engine: indty ="  ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] indty) ; assert false in
       let it = List.nth tys indtyno in
-     let status,obj = NInversion.mk_inverter name it leftno ?selection sort 
+     let status,obj = NInversion.mk_inverter name true it leftno ?selection sort 
                         status status#baseuri in
      let _,_,menv,_,_ = obj in
      (match menv with