X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=4b85d61bc7960aac8f20e10953f9e3cef67a1815;hb=79fdc0d44a2c8a3b1d2649b25fd7181c2ef49209;hp=9b08ba6dc5a662dcc0f6dd2865f686ad7374a4f9;hpb=81cb773cbc402fc74752fb69a436b25be49489ee;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 9b08ba6dc..4b85d61bc 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/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
@@ -71,7 +75,9 @@ let save_object_to_disk uri obj ugraph univlist =
   in
   (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
   let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
-   if Helm_registry.get_bool "matita.system" then
+   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
@@ -153,13 +159,20 @@ let add_single_obj uri obj refinement_toolkit =
       (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" 
       (univ_time *. 100. /. total_time) (total_time) (univ_time)
       (UriManager.name_of_uri uri));*)
-    let _, ugraph, univlist = 
-      CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
+    let obj, ugraph, univlist = 
+      try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri 
+      with CicEnvironment.Object_not_found _ -> assert false
+    in
     try 
       index_obj ~dbd ~uri; (* 2 must be in the env *)
       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"^
+          Printexc.to_string exc));
         try 
          HLog.message
           (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
@@ -217,7 +230,7 @@ let generate_elimination_principles uri refinement_toolkit =
 	List.iter remove_single_obj !uris;
 	raise exn 
   in
-  let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+  let obj, _ = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in
     match obj with
       | Cic.InductiveDefinition (indTypes, _, _, _) ->
 	  let counter = ref 0 in
@@ -233,12 +246,35 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,_,_) -> true)
 
+let stack = ref [];;
+
+let h2l h =
+  UriManager.UriHashtbl.fold 
+  (fun k v acc -> (k,v) :: acc) h []
+;;
+
+let push () =
+  stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack;
+  remove_all_coercions ()
+;;
+
+let pop () =
+  match !stack with
+  | [] -> raise (Failure "Unable to POP from librarySync.ml")
+  | (db,h) :: tl -> 
+      stack := tl;
+      remove_all_coercions ();
+      CoercDb.restore db;
+      List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v)
+      h
+;;
+
 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 
+    CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph 
   in
   (* we have to get the source and the tgt type uri
    * in Coq syntax we have already their names, but
@@ -308,7 +344,9 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
       (CoercDb.to_list ())
   in
   if not add_composites then
-    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
+    UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
+    [])
   else
     let new_coercions = 
       CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
@@ -327,14 +365,11 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
     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,saturations,obj,arity) -> 
             add_single_obj uri obj refinement_toolkit;
              (uri,arity,saturations)::acc) 
           [] new_coercions
-      else
-        []
     in
     (* store that composite_uris are related to uri. the first component is
      * the stuff in the DB while the second is stuff for remove_obj *)
@@ -344,8 +379,8 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
        List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
         composite_uris; 
     *)
-    UriManager.UriHashtbl.add coercion_hashtbl uri 
-      (composite_uris,if add_composites then composite_uris else []);
+    UriManager.UriHashtbl.add 
+      coercion_hashtbl uri (composite_uris,composite_uris);
     (*
     prerr_endline ("lemmas:");
       List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
@@ -363,7 +398,8 @@ 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))
@@ -371,7 +407,7 @@ let remove_coercion uri =
     (* remove composites from the lib *)
     List.iter remove_single_obj composites_in_lib
   with
-    Not_found -> () (* mhh..... *)
+    Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *)
     
 
 let generate_projections refinement_toolkit uri fields =
@@ -385,8 +421,8 @@ let generate_projections refinement_toolkit uri fields =
     (fun (uri, name, bo) (_name, coercion, arity) ->
       let saturations = 0 in
       try
-       let ty, ugraph =
-         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
+       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
         add_single_obj uri obj refinement_toolkit;
@@ -444,31 +480,31 @@ let
       List.fold_right
        (fun (name,idx,ty,bo) (n,uris) ->
          if name = name_to_avoid then
-          (n+1,uris)
+          (n-1,uris)
          else
           let uri =
            UriManager.uri_of_string
             (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
-          let bo = Cic.Fix (n,funs) in 
+	  let bo = Cic.Fix (n-1,funs) in 
           let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
-           add_single_obj uri obj refinement_toolkit;
-           (n+1,uri::uris)
-       ) funs (1,[]))
+           (add_single_obj uri obj refinement_toolkit;
+           (n-1,uri::uris)))
+       funs (List.length funs,[]))
   | Cic.CoFix (_,funs) ->
      snd (
       List.fold_right
        (fun (name,ty,bo) (n,uris) ->
          if name = name_to_avoid then
-          (n+1,uris)
+          (n-1,uris)
          else
           let uri =
            UriManager.uri_of_string
             (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
-          let bo = Cic.CoFix (n,funs) in 
+          let bo = Cic.CoFix (n-1,funs) in 
           let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
            add_single_obj uri obj refinement_toolkit;
-           (n+1,uri::uris)
-       ) funs (1,[]))
+           (n-1,uri::uris)
+       ) funs (List.length funs,[]))
   | _ -> assert false
 
 let add_obj refinement_toolkit uri obj =
@@ -485,21 +521,25 @@ let add_obj refinement_toolkit uri obj =
            generate_sibling_mutual_definitions refinement_toolkit uri attrs
             name bo
     | Cic.Constant _ -> ()
-    | Cic.InductiveDefinition (_,_,_,attrs) ->
-        uris := !uris @ 
-          generate_elimination_principles uri refinement_toolkit;
-        uris := !uris @ generate_inversion refinement_toolkit uri obj;
-        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 refinement_toolkit uri fields))
+    | Cic.InductiveDefinition (inductivefuns,_,_,attrs) ->
+       let _,inductive,_,_ = List.hd inductivefuns in
+       if inductive then
+        begin
+         uris := !uris @ 
+           generate_elimination_principles uri refinement_toolkit;
+         uris := !uris @ generate_inversion refinement_toolkit uri obj;
+        end ;
+       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 refinement_toolkit uri fields))
     | Cic.CurrentProof _
     | Cic.Variable _ -> assert false
   end;