From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 14 Sep 2009 14:09:21 +0000 (+0000)
Subject: Simplest typing for status records.
X-Git-Tag: make_still_working~3468
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7aafcce5268d75a57e69b4085436850567a6c869;p=helm.git

Simplest typing for status records.
---

diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml
index 0c6e91095..5cd454fb3 100644
--- 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 dec3aca01..8e361407f 100644
--- 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 54c5985f3..0bf40e234 100644
--- 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 c526741b2..f08891b5a 100644
--- 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 c75de5265..fb733cdfc 100644
--- 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 2911204ae..d89db9d71 100644
--- 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 7d5d0101a..fd697265a 100644
--- 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 dd5820eb9..0f514eef6 100644
--- 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 9f349ba6b..ce8808552 100644
--- 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 87519352c..862c9808e 100644
--- 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 26482e61b..dc7a6cf4a 100644
--- 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 10a4a8a62..40974aac2 100644
--- 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