- inversion principles are now generated also for co-inductive types

[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 4d7b8ce4e9d8494da2fcf79cae1f383929beb289..89673e7d75dae131b867114380e98b37fec483f6 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -531,68 +531,54 @@ let record_index_obj =
 ;;
 
 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 mk_item orig_ty spec =
+  let keys = NnAuto.keys_of_cic_term [] [] [] orig_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
+  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
 ;;
 
 let index_obj_for_auto status (uri, height, _, _, kind) = 
@@ -954,15 +940,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)
@@ -1099,7 +1087,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