X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicRecord.ml;h=e76ca9ca2585c5c442741bb5b2448a0cfaa115e2;hb=762a35d1dcf3ccbcc69701f9d479c450186ecc12;hp=5502f989e9ca0149bdb4d39366cfda61edc95421;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git

diff --git a/helm/software/components/library/cicRecord.ml b/helm/software/components/library/cicRecord.ml
index 5502f989e..e76ca9ca2 100644
--- a/helm/software/components/library/cicRecord.ml
+++ b/helm/software/components/library/cicRecord.ml
@@ -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;;