dependences update

[helm.git] / helm / software / components / library / cicRecord.ml

diff --git a/helm/software/components/library/cicRecord.ml b/helm/software/components/library/cicRecord.ml
index 775292ccbb4c959892707be7eaa33a5e8df68236..e76ca9ca2585c5c442741bb5b2448a0cfaa115e2 100644 (file)
--- a/helm/software/components/library/cicRecord.ml
+++ b/helm/software/components/library/cicRecord.ml
@@ -43,7 +43,7 @@ let generate_one_proj uri params paramsno fields t i =
 
 let projections_of uri field_names =
  let buri = UriManager.buri_of_uri uri in
- let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
+ let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in
   match obj with
      Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) ->
       assert (params = []); (* general case not implemented *)
@@ -86,3 +86,50 @@ let projections_of uri field_names =
        in
         aux (List.length fields) (CicSubstitution.lift 2 ty,field_names)
    | _ -> assert false
+;;
+
+let generate_projections ~add_obj ~add_coercion (uri as orig_uri) obj =
+ match obj with
+  | Cic.InductiveDefinition (inductivefuns,_,_,attrs) ->
+     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 -> []
+      | Some fields ->
+         let uris = ref [] in
+         let projections = 
+           projections_of uri (List.map (fun (x,_,_) -> x) fields) 
+         in
+          List.iter2 
+            (fun (uri, name, bo) (_name, coercion, arity) ->
+             try
+              let ty, _ =
+                CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in
+              let attrs = [`Class `Projection; `Generated] in
+              let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+              let lemmas = add_obj uri obj in
+              let lemmas1 = 
+                if not coercion then [] else 
+                 add_coercion uri arity 0 (UriManager.buri_of_uri orig_uri)
+              in
+               uris := lemmas1 @ lemmas @ 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 fields;
+          !uris)
+  | _ -> []
+;;
+
+
+let init () = 
+  LibrarySync.add_object_declaration_hook generate_projections;;