Generation of inductive and inversion principles for mutual

[helm.git] / components / library / librarySync.ml

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index e1b73821bc6176014ca5c55bb30474858b126f30..1db8f0cfc2c7b8374b79ae334ef068da0cab6c83 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -178,19 +178,30 @@ let remove_single_obj uri =
 
 let generate_elimination_principles uri refinement_toolkit =
   let uris = ref [] in
-  let elim sort =
-    try
-      let uri,obj = CicElim.elim_of ~sort uri 0 in
-       add_single_obj uri obj refinement_toolkit;
-       uris := uri :: !uris
-    with CicElim.Can_t_eliminate -> ()
+  let elim i =
+    let elim sort =
+      try
+       let uri,obj = CicElim.elim_of ~sort uri i in
+         add_single_obj uri obj refinement_toolkit;
+         uris := uri :: !uris
+      with CicElim.Can_t_eliminate -> ()
+    in
+      try
+       List.iter 
+         elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
+      with exn ->
+       List.iter remove_single_obj !uris;
+       raise exn 
   in
-  try
-    List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
-    !uris
-  with exn ->
-   List.iter remove_single_obj !uris;
-   raise exn
+  let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+    match obj with
+      | Cic.InductiveDefinition (indTypes, _, _, _) ->
+         let counter = ref 0 in
+           List.iter (fun _ -> elim !counter; counter := !counter+1) indTypes;
+           !uris
+      | _  -> 
+         failwith (Printf.sprintf "not an inductive definition (%s)"
+                     (UriManager.string_of_uri uri))
 
 (* COERCIONS ***********************************************************)
   
@@ -350,11 +361,10 @@ let generate_projections refinement_toolkit uri fields =
 let build_inversion_principle = ref (fun a b -> assert false);;
 
 let generate_inversion refinement_toolkit uri obj =
- match !build_inversion_principle uri obj with
-    None -> []
-  | Some (ind_uri,ind_obj) ->
-     add_single_obj ind_uri ind_obj refinement_toolkit;
-     [ind_uri]
+  List.map 
+    (fun (ind_uri,ind_obj) -> 
+       add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
+    (!build_inversion_principle uri obj)
 
 let add_obj refinement_toolkit uri obj =
  add_single_obj uri obj refinement_toolkit;