Generation of auxiliary lemmas for inductive types and records moved

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

diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml
index d853243ddd06b5a6dc42a423960d8404a546443e..4aa9669472aba78437c4d48852e5e61d831f3402 100644 (file)
--- a/helm/ocaml/library/librarySync.ml
+++ b/helm/ocaml/library/librarySync.ml
@@ -92,7 +92,7 @@ let index_obj =
   fun ~dbd ~uri ->
    profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
 
-let add_obj uri obj ~basedir =
+let add_single_obj uri obj ~basedir =
   let dbd = LibraryDb.instance () in
   if CicEnvironment.in_library uri then
     raise (AlreadyDefined uri)
@@ -119,7 +119,7 @@ let add_obj uri obj ~basedir =
     raise exc
   end
 
-let remove_obj uri =
+let remove_single_obj uri =
   let derived_uris_of_uri uri =
    let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
     innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
@@ -140,3 +140,88 @@ let remove_obj uri =
       CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri);
       CicEnvironment.remove_obj uri)
   to_remove
+
+(*** GENERATION OF AUXILIARY LEMMAS ***)
+
+let generate_elimination_principles ~basedir uri =
+  let uris = ref [] in
+  let elim sort =
+    try
+      let uri,obj = CicElim.elim_of ~sort uri 0 in
+       add_single_obj uri obj ~basedir;
+       uris := uri :: !uris
+    with CicElim.Can_t_eliminate -> ()
+  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 generate_projections ~basedir uri fields =
+ let uris = ref [] in
+ let projections = CicRecord.projections_of uri fields in
+  try
+   List.iter
+    (fun (uri, name, bo) ->
+      try
+       let ty, ugraph =
+         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
+       let attrs = [`Class `Projection; `Generated] in
+       let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+        add_single_obj ~basedir uri obj;
+        uris := uri :: !uris
+      with
+         CicTypeChecker.TypeCheckerFailure s ->
+          HLog.message
+           ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s);
+       | CicEnvironment.Object_not_found uri ->
+          let depend = UriManager.name_of_uri uri in
+           HLog.message
+            ("Unable to create projection " ^ name ^ " because it requires " ^
+               depend)
+    ) projections;
+   !uris
+  with exn ->
+   List.iter remove_single_obj !uris;
+   raise exn
+
+let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
+
+let add_obj uri obj ~basedir =
+ add_single_obj uri obj ~basedir;
+ let uris = ref [] in
+ try
+  begin
+   match obj with
+    | Cic.Constant _ -> ()
+    | Cic.InductiveDefinition (_,_,_,attrs) ->
+        uris := !uris @ generate_elimination_principles ~basedir uri;
+        let rec get_record_attrs =
+          function
+          | [] -> None
+          | (`Class (`Record fields))::_ -> Some fields
+          | _::tl -> get_record_attrs tl
+        in
+         (match get_record_attrs attrs with
+         | None -> () (* not a record *)
+         | Some fields ->
+            uris := !uris @ (generate_projections ~basedir uri fields))
+    | Cic.CurrentProof _
+    | Cic.Variable _ -> assert false
+  end;
+  UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
+  !uris
+ with exn ->
+  List.iter remove_single_obj !uris;
+  raise exn
+
+let remove_obj uri =
+ let uris =
+  try
+   UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri
+  with
+   Not_found -> []
+ in
+  List.iter remove_single_obj (uri::uris)