added records

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

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 9a44742b7c5dacebe62d2edd170ccc9020616e61..850c23ddd119fccd49301a521c4e15515e5aeb77 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -27,6 +27,58 @@ 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)
+
+(** adds a (name,uri) list l to a disambiguation environment e **)
+let env_of_list l e = 
+  let module DT = DisambiguateTypes in
+  let module DTE = DisambiguateTypes.Environment in
+  List.fold_left (
+    fun e (name,uri) -> 
+      DTE.add 
+       (DT.Id name) 
+       (uri,fun _ _ _ -> CicUtil.term_of_uri uri)
+       e
+  ) e l
+
+let add_aliases_for_object 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_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 paths_and_uris_of_obj uri status =
   let basedir = get_string_option status "basedir" in
   let innertypesuri = UriManager.innertypesuri_of_uri uri in
@@ -106,6 +158,7 @@ let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status =
     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);
+    let status = add_aliases_for_object status suri in
     { status with objects = new_stuff @ status.objects }
   end
   
@@ -129,6 +182,7 @@ let add_inductive_def
     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 = add_aliases_for_inductive_def status types suri in
     let status = { status with objects = new_stuff @ status.objects } in
     let elim sort status =
       try
@@ -146,7 +200,43 @@ let add_inductive_def
       status
       [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
   end
-  
+ 
+let add_record_def (suri, params, ty, fields) status =
+  let module CTC = CicTypeChecker in
+  let uri = UriManager.uri_of_string suri in
+  let buri = UriManager.buri_of_uri uri in
+  let record_spec = suri, params, ty, fields in
+  let types, leftno, obj, ugraph = CicRecord.inductive_of_record record_spec in
+  let status = add_inductive_def ~uri ~types ~leftno ~ugraph status in
+  let projections = CicRecord.projections_of record_spec in
+  let status = 
+    List.fold_left (
+      fun status (suri, name, t) -> 
+        try 
+          let ty, ugraph = 
+            CTC.type_of_aux' [] [] t CicUniv.empty_ugraph 
+          in
+          (* THIS MUST BE IN SYNC WITH CicRecord *)
+          let uri = UriManager.uri_of_string suri in
+          let t = Unshare.unshare t in
+          let ty = Unshare.unshare ty in
+          let status = add_constant ~uri ~body:t ~ty ~ugraph status in
+          add_aliases_for_object status suri
+        with
+        | CTC.TypeCheckerFailure s ->
+            MatitaLog.message 
+              ("Unable to create projection " ^ name ^ " cause: " ^ s);
+            status
+        | Http_getter_types.Key_not_found s ->
+            let depend = UriManager.uri_of_string s in
+            let depend = UriManager.name_of_uri depend in
+            MatitaLog.message 
+              ("Unable to create projection " ^ name ^ " cause uses " ^ depend);
+            status
+    ) status projections
+  in
+  status
+   
 module OrderedUri =
 struct
   type t = UriManager.uri * string