X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=c6682bd9100df786a88c71425230f8a219de07ed;hb=84e4ed5e9a09589ac149c6d0d135c226d5b7a5f9;hp=086893a974985e614026bfaebd29b89e5f4de912;hpb=e134b6f156268364d3027e73910c19e9c7e09838;p=helm.git

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 086893a97..c6682bd91 100644
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -25,6 +25,10 @@
 
 (* $Id$ *)
 
+let object_declaration_hook = ref (fun _ _ -> ());;
+let set_object_declaration_hook f =
+ object_declaration_hook := f
+
 exception AlreadyDefined of UriManager.uri
 
 let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
@@ -44,7 +48,7 @@ let uris_of_obj uri =
   innertypesuri,bodyuri,univgraphuri
 
 let paths_and_uris_of_obj uri =
-  let resolved = Http_getter.filename' ~writable:true uri in
+  let resolved = Http_getter.filename' ~local:true ~writable:true uri in
   let basepath = Filename.dirname resolved in
   let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
   let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
@@ -70,12 +74,28 @@ let save_object_to_disk uri obj ugraph univlist =
     HExtlib.mkdir dir
   in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
-  let annobj = Cic2acic.plain_acic_object_of_cic_object obj in 
+  let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
+   if Helm_registry.get_bool "matita.system" &&
+      not (Helm_registry.get_bool "matita.noinnertypes")
+   then
+    let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
+     Cic2acic.acic_object_of_cic_object obj 
+    in
+    let innertypesxml = 
+     Cic2Xml.print_inner_types
+      uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false
+    in
+    annobj, Some innertypesxml, Some ids_to_inner_sorts, false
+   else 
+    let annobj = Cic2acic.plain_acic_object_of_cic_object obj in  
+    annobj, None, None, true 
+  in 
   (* prepare XML *)
   let xml, bodyxml =
    Cic2Xml.print_object
-    uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj 
-  in
+    uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false 
+    ~generate_attributes annobj 
+  in    
   let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
       xmlunivgraphpath, univgraphuri = 
     paths_and_uris_of_obj uri 
@@ -88,6 +108,14 @@ let save_object_to_disk uri obj ugraph univlist =
   (* we return a list of uri,path we registered/created *)
   (uri,xmlpath) ::
   (univgraphuri,xmlunivgraphpath) ::
+    (* now the optional inner types, both write and register *)
+    (match innertypes with 
+     | None -> []
+     | Some innertypesxml ->
+         write ensure_path_exists innertypespath;
+         write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath);
+         [innertypesuri, innertypespath]
+    ) @
     (* now the optional body, both write and register *)
     (match bodyxml,bodyuri with
        None,_ -> []
@@ -138,6 +166,10 @@ let add_single_obj uri obj refinement_toolkit =
       try
         (*3*)
         let new_stuff = save_object_to_disk uri obj ugraph univlist in
+        (* EXPERIMENTAL: pretty print the object in natural language *)
+	(try !object_declaration_hook uri obj
+	 with exc ->
+	  prerr_endline "Error: object_declaration_hook failed");
         try 
          HLog.message
           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
@@ -149,7 +181,7 @@ let add_single_obj uri obj refinement_toolkit =
         raise exc
     with exc ->
       CicEnvironment.remove_obj uri; (* -1 *)
-    raise exc
+      raise exc
   end
 
 let remove_single_obj uri =
@@ -164,7 +196,7 @@ let remove_single_obj uri =
   List.iter 
    (fun uri -> 
      (try
-       let file = Http_getter.resolve' ~writable:true uri in
+       let file = Http_getter.resolve' ~local:true ~writable:true uri in
         HExtlib.safe_remove file;
         HExtlib.rmdir_descend (Filename.dirname file)
      with Http_getter_types.Key_not_found _ -> ());
@@ -209,9 +241,11 @@ let generate_elimination_principles uri refinement_toolkit =
   
 let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
-  CoercDb.remove_coercion (fun (_,_,u1) -> true)
+  CoercDb.remove_coercion (fun (_,_,_,_) -> true)
 
-let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
+let add_coercion ~add_composites refinement_toolkit uri arity saturations
+ baseuri
+=
   let coer_ty,_ =
     let coer = CicUtil.term_of_uri uri in
     CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
@@ -227,7 +261,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
    * should we saturate it with metas in case we insert it?
    * 
    *)
-  let spline2list ty =
+  let spine2list ty =
     let rec aux = function
       | Cic.Prod( _, src, tgt) -> src::aux tgt
       | t -> [t]
@@ -235,30 +269,35 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
     aux ty
   in
   let src_carr, tgt_carr = 
-    let list_remove_from_tail n l = 
-      let rec aux n = function
-        | hd::tl when n > 0 -> aux (n-1) tl
-        | l when n = 0 -> l
-        | _ -> assert false
+    let get_classes arity saturations l = 
+      (* this is the ackerman's function revisited *)
+      let rec aux = function
+         0,0,None,tgt::src::_ -> src,Some (`Class tgt)
+       | 0,0,target,src::_ -> src,target
+       | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl)
+       | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl)
+       | arity,saturations,None,_::tl -> 
+            aux (arity, saturations, Some `Funclass, tl)
+       | arity,saturations,target,_::tl -> 
+            aux (arity - 1, saturations, target, tl)
+       | _ -> assert false
       in
-      aux n (List.rev l)
+       aux (arity,saturations,None,List.rev l)
     in
-    let types = spline2list coer_ty in
-    match arity, list_remove_from_tail arity types with
-    | 0,tgt::src::_ -> 
-        (* if ~delta is true, it is impossible to define an identity coercion *)
-        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
-        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
-    | n,_::src::_ -> 
-        CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
-        CoercDb.Fun arity
-    | _ -> assert false    
+    let types = spine2list coer_ty in
+    let src,tgt = get_classes arity saturations types in
+     CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
+     match tgt with
+        None -> assert false
+      | Some `Funclass -> CoercDb.Fun arity
+      | Some (`Class tgt) ->
+         CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
   in
   let already_in_obj src_carr tgt_carr uri obj = 
      List.exists 
       (fun (s,t,ul) -> 
         List.exists 
-         (fun u -> 
+         (fun u,_ -> 
            let bo = 
             match obj with 
             | Cic.Constant (_, Some bo, _, _, _) -> bo
@@ -273,36 +312,36 @@ let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
               ("Coercions " ^ 
                 UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
                 uri^" are not convertible, but are between the same nodes.\n"^
-                "From now on nification can fail randomly.");
+                "From now on unification can fail randomly.");
              false))
          ul)
       (CoercDb.to_list ())
   in
   if not add_composites then
-    (CoercDb.add_coercion (src_carr, tgt_carr, uri);[])
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
   else
     let new_coercions = 
-      CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 
+      CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
        baseuri
     in
     let new_coercions = 
-      List.filter (fun (s,t,u,obj) -> not(already_in_obj s t u obj))
+      List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
       new_coercions 
     in
-    let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
+    let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
     (* update the DB *)
     List.iter 
-      (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
+      (fun (src,tgt,uri,saturations,_,_) ->
+        CoercDb.add_coercion (src,tgt,uri,saturations)) 
       new_coercions;
-    CoercDb.add_coercion (src_carr, tgt_carr, uri);
+    CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
     (* add the composites obj and they eventual lemmas *)
     let lemmas = 
       if add_composites then
         List.fold_left
-          (fun acc (_,tgt,uri,obj) -> 
+          (fun acc (_,tgt,uri,saturations,obj,arity) -> 
             add_single_obj uri obj refinement_toolkit;
-            let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
-             (uri,arity)::acc) 
+             (uri,arity,saturations)::acc) 
           [] new_coercions
       else
         []
@@ -334,10 +373,10 @@ let remove_coercion uri =
     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
       composites_in_db;*)
     UriManager.UriHashtbl.remove coercion_hashtbl uri;
-    CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
+    CoercDb.remove_coercion (fun (_,_,u,_) -> UriManager.eq uri u);
     (* remove from the DB *) 
     List.iter 
-      (fun u -> CoercDb.remove_coercion (fun (_,_,u1) -> UriManager.eq u u1))
+      (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
       composites_in_db;
     (* remove composites from the lib *)
     List.iter remove_single_obj composites_in_lib
@@ -354,6 +393,7 @@ let generate_projections refinement_toolkit uri fields =
   try
    List.iter2 
     (fun (uri, name, bo) (_name, coercion, arity) ->
+      let saturations = 0 in
       try
        let ty, ugraph =
          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
@@ -369,14 +409,14 @@ let generate_projections refinement_toolkit uri fields =
                 every time. Right? *)
               let x = 
                 add_coercion ~add_composites:true refinement_toolkit uri arity
-		 (UriManager.buri_of_uri uri)
+                 saturations (UriManager.buri_of_uri uri)
               in
 (*prerr_endline ("are: ");
   List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
   prerr_endline "---";
 *)
               (*CSC: I throw the arity away. See comment above *)
-              List.map fst x
+              List.map (fun u,_,_ -> u) x
             end
           else  
             []
@@ -444,6 +484,7 @@ let
 let add_obj refinement_toolkit uri obj =
  add_single_obj uri obj refinement_toolkit;
  let uris = ref [] in
+ let not_debug = not (Helm_registry.get_bool "matita.debug") in
  try
   begin
    match obj with
@@ -474,9 +515,10 @@ let add_obj refinement_toolkit uri obj =
   end;
   UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
   !uris
- with exn ->
-  List.iter remove_single_obj !uris;
-  raise exn
+ with 
+ | exn when not_debug ->
+    List.iter remove_single_obj !uris;
+    raise exn
 
 let remove_obj uri =
  let uris =