Big commit and major code clean-up:

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

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 9a44742b7c5dacebe62d2edd170ccc9020616e61..3a7f6dd32099beff643b6e87d7cd7b8a695f0900 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -27,6 +27,65 @@ 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_uriref (uri,[i]))
+      ::
+      (fst(List.fold_left (
+        fun (acc,j) (name,_) ->
+          (((name,UriManager.string_of_uriref (uri,[i;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 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
+  (* aliases for the constructors and types *)
+  let aliases = env_of_list (extract_alias types uri) status.aliases in
+  (* aliases for the eliminations principles *)
+  let base = String.sub suri 0 (String.length suri - 4)  in
+  let alisases = 
+    env_of_list
+      (List.fold_left (
+        fun acc suffix -> 
+          if List.exists (
+            fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
+          ) status.objects then
+            let u = base ^ suffix in
+            (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
+          else
+            acc
+      ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
+  in
+  {status with aliases = aliases }
+*)
+
+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
@@ -93,60 +152,21 @@ 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