From 7aafcce5268d75a57e69b4085436850567a6c869 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 14 Sep 2009 14:09:21 +0000 Subject: [PATCH] Simplest typing for status records. --- .../components/grafite_parser/nEstatus.ml | 13 +++++----- .../components/grafite_parser/nEstatus.mli | 14 +++++----- .../components/lexicon/lexiconEngine.ml | 7 ++++- .../components/lexicon/lexiconEngine.mli | 9 +++++-- .../components/ng_kernel/nCicLibrary.ml | 6 ++++- .../components/ng_kernel/nCicLibrary.mli | 9 +++++-- .../components/ng_refiner/nCicCoercion.ml | 11 +++++--- .../components/ng_refiner/nCicCoercion.mli | 10 +++++-- .../components/ng_refiner/nCicUnifHint.ml | 7 ++++- .../components/ng_refiner/nCicUnifHint.mli | 9 +++++-- .../components/ng_refiner/nRstatus.ml | 26 +++++++++++-------- .../components/ng_refiner/nRstatus.mli | 26 ++++++++++++------- 12 files changed, 100 insertions(+), 47 deletions(-) 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: -> '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: - -> '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 -- 2.39.2