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

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index a09baafe1..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
@@ -59,35 +63,65 @@ let paths_and_uris_of_obj uri =
   xmlunivgraphpath, univgraphuri
 
 let save_object_to_disk uri obj ugraph univlist =
+  let write f x =
+    if not (Helm_registry.get_opt_default 
+              Helm_registry.bool "matita.nodisk" ~default:false) 
+    then      
+      f x
+  in
   let ensure_path_exists path =
     let dir = Filename.dirname path in
     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 
   in
-  List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
+  write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]);
   (* now write to disk *)
-  ensure_path_exists xmlpath;
-  Xml.pp ~gzip:true xml (Some xmlpath);
-  CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
+  write ensure_path_exists xmlpath;
+  write (Xml.pp ~gzip:true xml) (Some xmlpath);
+  write (CicUniv.write_xml_of_ugraph xmlunivgraphpath 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,_ -> []
      | Some bodyxml,Some bodyuri->
-         ensure_path_exists xmlbodypath;
-         Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
+         write ensure_path_exists xmlbodypath;
+         write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath);
          [bodyuri, xmlbodypath]
      | _-> assert false) 
 
@@ -105,7 +139,7 @@ let add_single_obj uri obj refinement_toolkit =
   let module RT = RefinementTool in
   let obj = 
     if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
-       not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
+       not (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
     then
       refinement_toolkit.RT.pack_coercion_obj obj
     else
@@ -132,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))
@@ -143,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 =
@@ -151,48 +189,63 @@ let remove_single_obj uri =
    let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
     innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
   in
-  let to_remove =
-    uri :: 
-    (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @
-    derived_uris_of_uri uri
-  in   
+  let uris_to_remove =
+   if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri]
+  in
+  let files_to_remove = uri :: derived_uris_of_uri uri in   
   List.iter 
-    (fun uri -> 
-      (try
-        let file = Http_getter.resolve' ~writable:true uri in
-         HExtlib.safe_remove file;
-         HExtlib.rmdir_descend (Filename.dirname file)
-      with Http_getter_types.Key_not_found _ -> ());
-      ignore (LibraryDb.remove_uri uri);
-      (*CoercGraph.remove_coercion uri;*)
-      CicEnvironment.remove_obj uri)
-  to_remove
+   (fun uri -> 
+     (try
+       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 _ -> ());
+   ) files_to_remove ;
+  List.iter 
+   (fun uri -> 
+     ignore (LibraryDb.remove_uri uri);
+     (*CoercGraph.remove_coercion uri;*)
+   ) uris_to_remove ;
+  CicEnvironment.remove_obj uri
 
 (*** GENERATION OF AUXILIARY LEMMAS ***)
 
 let generate_elimination_principles uri refinement_toolkit =
   let uris = ref [] in
-  let elim sort =
-    try
-      let uri,obj = CicElim.elim_of ~sort uri 0 in
-       add_single_obj uri obj refinement_toolkit;
-       uris := uri :: !uris
-    with CicElim.Can_t_eliminate -> ()
+  let elim i =
+    let elim sort =
+      try
+	let uri,obj = CicElim.elim_of ~sort uri i in
+	  add_single_obj uri obj refinement_toolkit;
+	  uris := uri :: !uris
+      with CicElim.Can_t_eliminate -> ()
+    in
+      try
+	List.iter 
+	  elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
+      with exn ->
+	List.iter remove_single_obj !uris;
+	raise exn 
   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 (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+    match obj with
+      | Cic.InductiveDefinition (indTypes, _, _, _) ->
+	  let counter = ref 0 in
+	    List.iter (fun _ -> elim !counter; counter := !counter+1) indTypes;
+	    !uris
+      | _  -> 
+	  failwith (Printf.sprintf "not an inductive definition (%s)"
+		      (UriManager.string_of_uri uri))
 
 (* COERCIONS ***********************************************************)
   
 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 =
+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 
@@ -208,74 +261,122 @@ let add_coercion ~add_composites refinement_toolkit uri =
    * should we saturate it with metas in case we insert it?
    * 
    *)
-  let extract_last_two_p ty =
+  let spine2list ty =
     let rec aux = function
-      | Cic.Prod( _, _, ((Cic.Prod _) as t)) -> 
-          aux t
-      | Cic.Prod( _, src, tgt) -> src, tgt
-      | _ -> assert false
+      | Cic.Prod( _, src, tgt) -> src::aux tgt
+      | t -> [t]
     in
     aux ty
   in
-  let ty_src, ty_tgt = extract_last_two_p coer_ty in
-  let src_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
-  let tgt_carr = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
-  let new_coercions = 
-    CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 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)) 
-      new_coercions;
-  if 
-    List.exists 
-      (fun (s,t,_) -> CoercDb.eq_carr s src_carr && CoercDb.eq_carr t tgt_carr)
+  let src_carr, tgt_carr = 
+    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 (arity,saturations,None,List.rev l)
+    in
+    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,_ -> 
+           let bo = 
+            match obj with 
+            | Cic.Constant (_, Some bo, _, _, _) -> bo
+            | _ -> assert false
+           in
+           CoercDb.eq_carr s src_carr && 
+           CoercDb.eq_carr t tgt_carr &&
+           if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
+           CicUniv.oblivion_ugraph)
+           then true else
+            (HLog.warn
+              ("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 unification can fail randomly.");
+             false))
+         ul)
       (CoercDb.to_list ())
-  then
-    begin
-      assert (new_coercions = []);
-      []
-    end
+  in
+  if not add_composites then
+    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);[])
   else
-    begin
-      CoercDb.add_coercion (src_carr, tgt_carr, uri);
-      (* add the composites obj and they eventual lemmas *)
-      let lemmas = 
-        if add_composites then
-          List.fold_left
-            (fun acc (_,_,uri,obj) -> 
-              add_single_obj uri obj refinement_toolkit;
-              uri::acc) 
-            composite_uris 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 *)
-      (* 
-         prerr_endline ("adding: " ^ 
-           string_of_bool add_composites ^ UriManager.string_of_uri uri);
-         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 []);
-      lemmas
-    end
+    let new_coercions = 
+      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))
+      new_coercions 
+    in
+    let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
+    (* update the DB *)
+    List.iter 
+      (fun (src,tgt,uri,saturations,_,_) ->
+        CoercDb.add_coercion (src,tgt,uri,saturations)) 
+      new_coercions;
+    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 *)
+    (* 
+       prerr_endline ("adding: " ^ 
+         string_of_bool add_composites ^ UriManager.string_of_uri uri);
+       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 []);
+    (*
+    prerr_endline ("lemmas:");
+      List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+      lemmas;
+    prerr_endline ("lemmas END");*)
+    lemmas
+;;
 
 let remove_coercion uri =
   try
     let (composites_in_db, composites_in_lib) = 
       UriManager.UriHashtbl.find coercion_hashtbl uri 
     in
-    prerr_endline ("removing: " ^UriManager.string_of_uri uri);
+    (*prerr_endline ("removing: " ^UriManager.string_of_uri uri);
     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
-      composites_in_db;
+      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
@@ -285,10 +386,14 @@ let remove_coercion uri =
 
 let generate_projections refinement_toolkit uri fields =
  let uris = ref [] in
- let projections = CicRecord.projections_of uri (List.map fst fields) in
+ let projections = 
+   CicRecord.projections_of uri 
+     (List.map (fun (x,_,_) -> x) fields) 
+ in
   try
    List.iter2 
-    (fun (uri, name, bo) (_name, coercion) ->
+    (fun (uri, name, bo) (_name, coercion, arity) ->
+      let saturations = 0 in
       try
        let ty, ugraph =
          CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
@@ -297,7 +402,22 @@ let generate_projections refinement_toolkit uri fields =
         add_single_obj uri obj refinement_toolkit;
         let composites = 
          if coercion then
-            add_coercion ~add_composites:true refinement_toolkit uri
+            begin
+(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
+              (*CSC: I think there is a bug here. The composite coercions
+                are not remembered in the .moo file. Thus they are re-generated
+                every time. Right? *)
+              let x = 
+                add_coercion ~add_composites:true refinement_toolkit uri arity
+                 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 (fun u,_,_ -> u) x
+            end
           else  
             []
         in
@@ -320,23 +440,65 @@ let generate_projections refinement_toolkit uri fields =
 let build_inversion_principle = ref (fun a b -> assert false);;
 
 let generate_inversion refinement_toolkit uri obj =
- match !build_inversion_principle uri obj with
-    None -> []
-  | Some (ind_uri,ind_obj) ->
-     add_single_obj ind_uri ind_obj refinement_toolkit;
-     [ind_uri]
+  List.map 
+    (fun (ind_uri,ind_obj) -> 
+       add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
+    (!build_inversion_principle uri obj)
+
+let
+ generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
+=
+ function
+    Cic.Fix (_,funs) ->
+     snd (
+      List.fold_right
+       (fun (name,idx,ty,bo) (n,uris) ->
+         if name = name_to_avoid then
+          (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 obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+           add_single_obj uri obj refinement_toolkit;
+           (n+1,uri::uris)
+       ) funs (1,[]))
+  | Cic.CoFix (_,funs) ->
+     snd (
+      List.fold_right
+       (fun (name,ty,bo) (n,uris) ->
+         if name = name_to_avoid then
+          (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 obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+           add_single_obj uri obj refinement_toolkit;
+           (n+1,uri::uris)
+       ) funs (1,[]))
+  | _ -> assert false
 
 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
+    | Cic.Constant (name,Some bo,_,_,attrs) when
+       List.mem (`Flavour `MutualDefinition) attrs ->
+        uris :=
+         !uris @
+           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; *)
+        uris := !uris @ generate_inversion refinement_toolkit uri obj;
         let rec get_record_attrs =
           function
           | [] -> None
@@ -353,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 =