Much simpler (and slightly more performant) implementation of the UriManager.

[helm.git] / helm / matita / matitaSync.ml

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 9a44742b7c5dacebe62d2edd170ccc9020616e61..df29edc3b7421049ec63eb5a4616560fbfcb07fd 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -27,6 +27,43 @@ open Printf
 
 open MatitaTypes
 
+(** given a uri and a type list (the contructors types) builds a list of pairs
+ *  (name,uri) that is used to generate authomatic aliases **)
+let extract_alias types uri = 
+  fst(List.fold_left (
+    fun (acc,i) (name, _, _, cl) -> 
+      (name, UriManager.string_of_uri (UriManager.uri_of_uriref uri i None))
+      ::
+      (fst(List.fold_left (
+        fun (acc,j) (name,_) ->
+          (((name,UriManager.string_of_uri (UriManager.uri_of_uriref uri i
+          (Some j))) :: acc) , j+1)
+        ) (acc,1) cl)),i+1
+  ) ([],0) types)
+
+let env_of_list l env =
+ let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri (UriManager.uri_of_string suri)) l in
+  DisambiguateTypes.env_of_list l' env
+
+let add_aliases_for_inductive_def status types suri = 
+  let uri = UriManager.uri_of_string suri in
+  let aliases = env_of_list (extract_alias types uri) status.aliases in
+  {status with aliases = aliases }
+
+let add_alias_for_constant status suri =
+ let uri = UriManager.uri_of_string suri in
+ let name = UriManager.name_of_uri uri in
+ let new_env = env_of_list [(name,suri)] status.aliases in
+ {status with aliases = new_env }
+
+let add_aliases_for_object status suri =
+ function
+    Cic.InductiveDefinition (types,_,_,_) ->
+     add_aliases_for_inductive_def status types suri
+  | Cic.Constant _ -> add_alias_for_constant status suri
+  | Cic.Variable _
+  | Cic.CurrentProof _ -> assert false
+  
 let paths_and_uris_of_obj uri status =
   let basedir = get_string_option status "basedir" in
   let innertypesuri = UriManager.innertypesuri_of_uri uri in
@@ -86,67 +123,25 @@ let save_object_to_disk status uri obj =
          [bodyuri,xmlbodypath]
      | _-> assert false) 
 
-let unregister_if_some = function 
-  | Some u -> Http_getter.unregister' u | None -> ()
-
 let remove_object_from_disk uri path =
   Sys.remove path;
   Http_getter.unregister' uri
 
-let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status =
+let add_obj uri obj status =
   let dbd = MatitaDb.instance () in
   let suri = UriManager.string_of_uri uri in
   if CicEnvironment.in_library uri then
-    command_error (sprintf "%s constant already defined" suri)
+    command_error (sprintf "%s already defined" suri)
   else begin
-    let name = UriManager.name_of_uri uri in
-    let obj = Cic.Constant (name, body, ty, params, attrs) in
-    let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
-    CicEnvironment.add_type_checked_term uri (obj, ugraph);
+    CicTypeChecker.typecheck_obj uri obj;
     MetadataDb.index_obj ~dbd ~uri; (* must be in the env *)
     let new_stuff = save_object_to_disk status uri obj in  
-    MatitaLog.message (sprintf "%s constant defined" suri);
-    { status with objects = new_stuff @ status.objects }
+    MatitaLog.message (sprintf "%s defined" suri);
+    let status = add_aliases_for_object status suri obj in
+    { status with objects = new_stuff @ status.objects;
+                  proof_status = No_proof }
   end
-  
-let split_obj = function
-  | Cic.Constant (name, body, ty, _, attrs)
-  | Cic.Variable (name, body, ty, _, attrs) -> (name, body, ty, attrs)
-  | _ -> assert false
-
-let add_inductive_def
-  ~uri ~types ?(params = []) ?(leftno = 0) ?(attrs = []) ~ugraph status
-=
-  let dbd = MatitaDb.instance () in
-  let suri = UriManager.string_of_uri uri in
-  if CicEnvironment.in_library uri then
-    command_error (sprintf "%s inductive type already defined" suri)
-  else begin
-    let name = UriManager.name_of_uri uri in
-    let obj = Cic.InductiveDefinition (types, params, leftno, attrs) in
-    let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
-    CicEnvironment.put_inductive_definition uri (obj, ugraph);
-    MetadataDb.index_obj ~dbd ~uri; (* must be in the env *)
-    let new_stuff = save_object_to_disk status uri obj in
-    MatitaLog.message (sprintf "%s inductive type defined" suri);
-    let status = { status with objects = new_stuff @ status.objects } in
-    let elim sort status =
-      try
-        let obj = CicElim.elim_of ~sort uri 0 in
-        let (name, body, ty, attrs) = split_obj obj in
-        let suri = MatitaMisc.qualify status name ^ ".con" in
-        let uri = UriManager.uri_of_string suri in
-          (* TODO Zack: make CicElim returns a universe *)
-        let ugraph = CicUniv.empty_ugraph in
-        add_constant ~uri ?body ~ty ~attrs ~ugraph status;
-      with CicElim.Can_t_eliminate -> status
-    in
-    List.fold_left
-      (fun status sort -> elim sort status) 
-      status
-      [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
-  end
-  
+   
 module OrderedUri =
 struct
   type t = UriManager.uri * string