Simplest typing for status records.

diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml
index 0c6e91095d4502bd0052afe6c89aa0d1b952ab44..5cd454fb3a4b9b429769968eb550e0131f842327 100644 (file)
--- a/helm/software/components/grafite_parser/nEstatus.ml
+++ b/helm/software/components/grafite_parser/nEstatus.ml
@@ -11,16 +11,17 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+class type g_status =
+ object
+  inherit LexiconEngine.g_status
+  inherit NRstatus.g_dumpable_status
+ end
+
 class status =
  object (self)
   inherit LexiconEngine.status
   inherit NRstatus.dumpable_status
   method set_estatus
-   : 'status.
-      < coerc_db : NCicCoercion.db;
-        uhint_db : NCicUnifHint.db;
-        timestamp: NCicLibrary.timestamp;
-        dump: NRstatus.Serializer.obj list;
-        lstatus: LexiconEngine.lexicon_status; .. > as 'status -> 'self
+   : 'status. #g_status as 'status -> 'self
    = fun o -> (self#set_lexicon_engine_status o)#set_dumpable_status o
  end

diff --git a/helm/software/components/grafite_parser/nEstatus.mli b/helm/software/components/grafite_parser/nEstatus.mli
index dec3aca01280fe3e4ebb21b4c4f4a37cd54c299c..8e361407fa6621bff099577c50e8b29d3557b67c 100644 (file)
--- a/helm/software/components/grafite_parser/nEstatus.mli
+++ b/helm/software/components/grafite_parser/nEstatus.mli
@@ -11,14 +11,16 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+class type g_status =
+ object
+  inherit LexiconEngine.g_status
+  inherit NRstatus.g_dumpable_status
+ end
+
 class status :
  object ('self)
   inherit LexiconEngine.status
   inherit NRstatus.dumpable_status
-  method set_estatus:
-   < coerc_db : NCicCoercion.db;
-     uhint_db : NCicUnifHint.db;
-     timestamp: NCicLibrary.timestamp;
-     dump: NRstatus.Serializer.obj list;
-     lstatus: LexiconEngine.lexicon_status; .. > -> 'self
+  inherit g_status
+  method set_estatus: #g_status -> 'self
  end

diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml
index 54c5985f3cda38c02fca901ea5b41909840fdcfc..0bf40e234f68ee2fc54fd1b2956fb952c74f6a88 100644 (file)
--- a/helm/software/components/lexicon/lexiconEngine.ml
+++ b/helm/software/components/lexicon/lexiconEngine.ml
@@ -47,13 +47,18 @@ let initial_status = {
   notation_ids = [];
 }
 
+class type g_status =
+ object
+  method lstatus: lexicon_status
+ end
+
 class status =
  object
   val lstatus = initial_status
   method lstatus = lstatus
   method set_lstatus v = {< lstatus = v >}
   method set_lexicon_engine_status
-   : 'status. < lstatus: lexicon_status; .. > as 'status -> 'self
+   : 'status. #g_status as 'status -> 'self
    = fun o -> {< lstatus = o#lstatus >}
  end
 

diff --git a/helm/software/components/lexicon/lexiconEngine.mli b/helm/software/components/lexicon/lexiconEngine.mli
index c526741b2a1eb69a4cc06cb449b8a0e3cda49aec..f08891b5a974c6010840897a98beafe978235e78 100644 (file)
--- a/helm/software/components/lexicon/lexiconEngine.mli
+++ b/helm/software/components/lexicon/lexiconEngine.mli
@@ -32,11 +32,16 @@ type lexicon_status = {
   notation_ids: CicNotation.notation_id list;      (** in-scope notation ids *)
 }
 
+class type g_status =
+ object
+  method lstatus: lexicon_status
+ end
+
 class status :
  object ('self)
-  method lstatus: lexicon_status
+  inherit g_status
   method set_lstatus: lexicon_status -> 'self
-  method set_lexicon_engine_status: < lstatus: lexicon_status ; .. > -> 'self
+  method set_lexicon_engine_status: #g_status -> 'self
  end
 
 val eval_command : #status as 'status -> LexiconAst.command -> 'status

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index c75de5265b603d67808c7ff55582960f792779c0..fb733cdfcb877366658881b96c2365f06b37352a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -143,6 +143,10 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
 
 let init = load_db;;
 
+class type g_status =
+ object
+  method timestamp: timestamp
+ end
 
 class status =
  object
@@ -150,7 +154,7 @@ class status =
   method timestamp = timestamp
   method set_timestamp v = {< timestamp = v >}
   method set_library_status
-   : 'status. < timestamp : timestamp; .. > as 'status -> 'self
+   : 'status. #g_status as 'status -> 'self
    = fun o -> {< timestamp = o#timestamp >}
  end
 

diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli
index 2911204ae50d0370375b56f4ac772e370a0952fb..d89db9d7114ed5022c9aa87b852f7100300a56c1 100644 (file)
--- a/helm/software/components/ng_kernel/nCicLibrary.mli
+++ b/helm/software/components/ng_kernel/nCicLibrary.mli
@@ -15,11 +15,16 @@ exception LibraryOutOfSync of string Lazy.t
 
 type timestamp
 
+class type g_status =
+ object
+  method timestamp: timestamp
+ end
+
 class status :
  object ('self)
-  method timestamp: timestamp
+  inherit g_status
   method set_timestamp: timestamp -> 'self
-  method set_library_status: <timestamp: timestamp; ..> -> 'self
+  method set_library_status: #g_status -> 'self
  end
 
 (* it also checks it and add it to the environment *)

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 7d5d0101ad3de62287ad4197d6465a0efee51540..fd697265a2464e4c9255eb6f844fd796b2fe6bac 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -31,6 +31,12 @@ type db = DB.t * DB.t
 
 let empty_db = DB.empty,DB.empty
 
+class type g_status =
+ object
+  inherit NCicUnifHint.g_status
+  method coerc_db: db
+ end
+
 class status =
  object
   inherit NCicUnifHint.status
@@ -38,9 +44,8 @@ class status =
   method coerc_db = db
   method set_coerc_db v = {< db = v >}
   method set_coercion_status
-  : 'status. < coerc_db : db; uhint_db: NCicUnifHint.db; .. > as 'status -> 
-          'self
-          = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
+   : 'status. #g_status as 'status -> 'self
+   = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
  end
 
 let index_coercion status name c src tgt arity arg =

diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli
index dd5820eb92d8064b8f00ab3419a8ecbb9a0e0015..0f514eef69ba86ed9dd33c245852f9c37f0b6780 100644 (file)
--- a/helm/software/components/ng_refiner/nCicCoercion.mli
+++ b/helm/software/components/ng_refiner/nCicCoercion.mli
@@ -13,13 +13,19 @@
 
 type db
 
+class type g_status =
+ object
+  inherit NCicUnifHint.g_status
+  method coerc_db: db
+ end
+
 class status :
  object ('self)
   inherit NCicUnifHint.status
+  inherit g_status
   method coerc_db: db
   method set_coerc_db: db -> 'self
-  method set_coercion_status: <coerc_db: db; uhint_db: NCicUnifHint.db; ..> 
-    -> 'self
+  method set_coercion_status: #g_status -> 'self
  end
 
 val empty_db: db

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index 9f349ba6bbbfce24ede8364ea1ab1045f313eb2d..ce88085521c2ddabda8d96069f9fba79bb90a876 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -36,13 +36,18 @@ exception HintNotValid
 
 let skel_dummy = NCic.Implicit `Type;;
 
+class type g_status =
+ object
+  method uhint_db: db
+ end
+
 class status =
  object
   val db = HDB.empty, EQDB.empty
   method uhint_db = db
   method set_uhint_db v = {< db = v >}
   method set_unifhint_status
-   : 'status. < uhint_db : db; .. > as 'status -> 'self
+   : 'status. #g_status as 'status -> 'self
    = fun o -> {< db = o#uhint_db >}
  end
 

diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli
index 87519352c4b783b0ba4955cb300517b34cc95bb3..862c9808efc0193b00d78257cfd1f48f5ecbd2b7 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnifHint.mli
+++ b/helm/software/components/ng_refiner/nCicUnifHint.mli
@@ -15,11 +15,16 @@ type db
 
 exception HintNotValid
 
+class type g_status =
+ object
+  method uhint_db: db
+ end
+
 class status :
  object ('self)
-  method uhint_db: db
+  inherit g_status
   method set_uhint_db: db -> 'self
-  method set_unifhint_status: < uhint_db : db; .. > -> 'self
+  method set_unifhint_status: #g_status -> 'self
  end
 
 val index_hint: 

diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml
index 26482e61b4138deec35cae8c12a0bb5774f24f16..dc7a6cf4a6df00fbad5997308c58e4ac04cd43c1 100644 (file)
--- a/helm/software/components/ng_refiner/nRstatus.ml
+++ b/helm/software/components/ng_refiner/nRstatus.ml
@@ -11,17 +11,19 @@
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
+class type g_status =
+ object
+  inherit NCicCoercion.g_status
+  inherit NCicLibrary.g_status
+ end
+
 class status =
  object (self)
   inherit NCicCoercion.status
   inherit NCicLibrary.status
   method set_rstatus
-   : 'status.
-       < coerc_db : NCicCoercion.db;
-         uhint_db : NCicUnifHint.db;
-         timestamp: NCicLibrary.timestamp; .. > as 'status -> 'self
-   = fun o ->
-      (self#set_coercion_status o)#set_library_status o
+   : 'status. #g_status as 'status -> 'self
+   = fun o -> (self#set_coercion_status o)#set_library_status o
  end
 
 type sstatus = status
@@ -38,6 +40,12 @@ module Serializer =
     status 
  end
 
+class type g_dumpable_status =
+ object
+  inherit g_status
+  method dump: Serializer.obj list
+ end
+
 class dumpable_status =
  object
   inherit status
@@ -45,10 +53,6 @@ class dumpable_status =
   method dump = dump
   method set_dump v = {< dump = v >}
   method set_dumpable_status
-   : 'status.
-       < coerc_db : NCicCoercion.db;
-         uhint_db : NCicUnifHint.db;
-         timestamp: NCicLibrary.timestamp;
-         dump: Serializer.obj list; .. > as 'status -> 'self
+   : 'status. #g_dumpable_status as 'status -> 'self
    = fun o -> {< dump = o#dump >}#set_rstatus o
  end

diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli
index 10a4a8a622a5203f7dce1be998b7c373a64f2571..40974aac21c08b68c9d614de44edaae8fa24a349 100644 (file)
--- a/helm/software/components/ng_refiner/nRstatus.mli
+++ b/helm/software/components/ng_refiner/nRstatus.mli
@@ -11,14 +11,18 @@
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
+class type g_status =
+ object
+  inherit NCicCoercion.g_status
+  inherit NCicLibrary.g_status
+ end
+
 class status :
  object ('self)
   inherit NCicCoercion.status
   inherit NCicLibrary.status
-  method set_rstatus: 
-   < coerc_db : NCicCoercion.db;
-     uhint_db : NCicUnifHint.db;
-     timestamp: NCicLibrary.timestamp; .. > -> 'self
+  inherit g_status
+  method set_rstatus: #g_status -> 'self
  end
 
 module Serializer:
@@ -27,14 +31,16 @@ module Serializer:
   val require: baseuri:NUri.uri -> (#status as 'status) -> 'status
  end
 
+class type g_dumpable_status =
+ object
+  inherit g_status
+  method dump: Serializer.obj list
+ end
+
 class dumpable_status :
  object ('self)
   inherit status
-  method dump: Serializer.obj list
+  inherit g_dumpable_status
   method set_dump: Serializer.obj list -> 'self
-  method set_dumpable_status:
-   < coerc_db : NCicCoercion.db;
-     uhint_db : NCicUnifHint.db;
-     timestamp: NCicLibrary.timestamp;
-     dump: Serializer.obj list; .. > -> 'self
+  method set_dumpable_status: #g_dumpable_status -> 'self
  end