From f4c17198d8afe7c8cd62dbab527d08902d891491 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 19 Jun 2009 07:21:49 +0000 Subject: [PATCH] Good: 1) all set_* methods are now polymorphic 2) no more :> coercions 3) no more technical class types Bad: 1) some polymorphic set_* methods have explicit row types that are problematic when extending another class in another file. The row types should just be #classname, but ocaml rejects them that way. --- .../components/grafite_parser/nEstatus.ml | 20 +++++----- .../components/grafite_parser/nEstatus.mli | 7 +++- .../components/lexicon/lexiconEngine.ml | 4 +- .../components/lexicon/lexiconEngine.mli | 2 +- .../components/ng_kernel/nCicLibrary.ml | 4 +- .../components/ng_kernel/nCicLibrary.mli | 2 +- .../components/ng_refiner/nCicCoercion.ml | 4 +- .../components/ng_refiner/nCicCoercion.mli | 2 +- .../components/ng_refiner/nCicUnifHint.ml | 4 +- .../components/ng_refiner/nCicUnifHint.mli | 2 +- .../components/ng_refiner/nRstatus.ml | 40 ++++++++----------- .../components/ng_refiner/nRstatus.mli | 11 ++++- .../components/ng_tactics/nTactics.ml | 13 +++--- 13 files changed, 62 insertions(+), 53 deletions(-) diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml index d7737cde9..0c6e91095 100644 --- a/helm/software/components/grafite_parser/nEstatus.ml +++ b/helm/software/components/grafite_parser/nEstatus.ml @@ -11,18 +11,16 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -class type ctstatus = - object ('self) - inherit LexiconEngine.status - inherit NRstatus.dumpable_status - method set_estatus: ctstatus -> 'self - end - -class status : ctstatus = +class status = object (self) inherit LexiconEngine.status inherit NRstatus.dumpable_status - method set_estatus o = - (self#set_lexicon_engine_status (o :> LexiconEngine.status)) - #set_dumpable_status (o :> 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 + = 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 e77f4e566..dec3aca01 100644 --- a/helm/software/components/grafite_parser/nEstatus.mli +++ b/helm/software/components/grafite_parser/nEstatus.mli @@ -15,5 +15,10 @@ class status : object ('self) inherit LexiconEngine.status inherit NRstatus.dumpable_status - method set_estatus: status -> 'self + method set_estatus: + < coerc_db : NCicCoercion.db; + uhint_db : NCicUnifHint.db; + timestamp: NCicLibrary.timestamp; + dump: NRstatus.Serializer.obj list; + lstatus: LexiconEngine.lexicon_status; .. > -> 'self end diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index 4662ca6bd..12200193e 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -52,7 +52,9 @@ class status = val lstatus = initial_status method lstatus = lstatus method set_lstatus v = {< lstatus = v >} - method set_lexicon_engine_status (o : status) = {< lstatus = o#lstatus >} + method set_lexicon_engine_status + : 'status. < lstatus: lexicon_status; .. > as 'status -> 'self + = fun o -> {< lstatus = o#lstatus >} end let dump_aliases out msg status = diff --git a/helm/software/components/lexicon/lexiconEngine.mli b/helm/software/components/lexicon/lexiconEngine.mli index 4e404024d..c526741b2 100644 --- a/helm/software/components/lexicon/lexiconEngine.mli +++ b/helm/software/components/lexicon/lexiconEngine.mli @@ -36,7 +36,7 @@ class status : object ('self) method lstatus: lexicon_status method set_lstatus: lexicon_status -> 'self - method set_lexicon_engine_status: status -> 'self + method set_lexicon_engine_status: < lstatus: lexicon_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 d54002d60..47c8d67c6 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -28,7 +28,9 @@ class status = val timestamp = (time0 : timestamp) method timestamp = timestamp method set_timestamp v = {< timestamp = v >} - method set_library_status (o : status) = {< timestamp = o#timestamp >} + method set_library_status + : 'status. < timestamp : timestamp; .. > as 'status -> 'self + = fun o -> {< timestamp = o#timestamp >} end let time_travel status = diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index 50ebf8f10..a8b546d2e 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -19,7 +19,7 @@ class status : object ('self) method timestamp: timestamp method set_timestamp: timestamp -> 'self - method set_library_status: status -> 'self + method set_library_status: -> 'self end val add_obj: #status as 'status -> NUri.uri -> NCic.obj -> 'status diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index d7fef8d8f..29fe0fd54 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -31,7 +31,9 @@ class status = val db = empty_db method coerc_db = db method set_coerc_db v = {< db = v >} - method set_coercion_status (o : status) = {< db = o#coerc_db >} + method set_coercion_status + : 'status. < coerc_db : db; .. > as 'status -> 'self + = fun o -> {< db = o#coerc_db >} end let index_coercion status c src tgt arity arg = diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli index 0d96a7407..1d31d469f 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.mli +++ b/helm/software/components/ng_refiner/nCicCoercion.mli @@ -17,7 +17,7 @@ class status : object ('self) method coerc_db: db method set_coerc_db: db -> 'self - method set_coercion_status: status -> 'self + method set_coercion_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 6d80fe6ca..d166b1936 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -29,7 +29,9 @@ class status = val db = DB.empty method uhint_db = db method set_uhint_db v = {< db = v >} - method set_unifhint_status (o : status) = {< db = o#uhint_db >} + method set_unifhint_status + : 'status. < uhint_db : db; .. > as 'status -> 'self + = fun o -> {< db = o#uhint_db >} end let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");; diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli index fa65d5277..7b8536ba7 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.mli +++ b/helm/software/components/ng_refiner/nCicUnifHint.mli @@ -17,7 +17,7 @@ class status : object ('self) method uhint_db: db method set_uhint_db: db -> 'self - method set_unifhint_status: status -> 'self + method set_unifhint_status: < uhint_db : db; .. > -> 'self end val index_hint: diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml index 5ef83ec3c..bb2d357d7 100644 --- a/helm/software/components/ng_refiner/nRstatus.ml +++ b/helm/software/components/ng_refiner/nRstatus.ml @@ -11,23 +11,18 @@ (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) -class type ctstatus = - object ('self) - inherit NCicUnifHint.status - inherit NCicCoercion.status - inherit NCicLibrary.status - method set_rstatus : ctstatus -> 'self - end - -class status : ctstatus = +class status = object (self) inherit NCicUnifHint.status inherit NCicCoercion.status inherit NCicLibrary.status - method set_rstatus o = - ((self#set_unifhint_status (o :> NCicUnifHint.status)) - #set_coercion_status (o :> NCicCoercion.status)) - #set_library_status (o :> NCicLibrary.status) + method set_rstatus + : 'status. + < coerc_db : NCicCoercion.db; + uhint_db : NCicUnifHint.db; + timestamp: NCicLibrary.timestamp; .. > as 'status -> 'self + = fun o -> + ((self#set_unifhint_status o)#set_coercion_status o)#set_library_status o end type sstatus = status @@ -44,20 +39,17 @@ module Serializer = status end -class type ctdumpable_status = - object ('self) - inherit status - method dump: Serializer.obj list - method set_dump: Serializer.obj list -> 'self - method set_dumpable_status: ctdumpable_status -> 'self - end - -class dumpable_status : ctdumpable_status = +class dumpable_status = object inherit status val dump = ([] : Serializer.obj list) method dump = dump method set_dump v = {< dump = v >} - method set_dumpable_status o = - {< dump = o#dump >}#set_rstatus (o :> status) + method set_dumpable_status + : 'status. + < coerc_db : NCicCoercion.db; + uhint_db : NCicUnifHint.db; + timestamp: NCicLibrary.timestamp; + dump: Serializer.obj list; .. > 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 7fde1b747..89f62ce1d 100644 --- a/helm/software/components/ng_refiner/nRstatus.mli +++ b/helm/software/components/ng_refiner/nRstatus.mli @@ -16,7 +16,10 @@ class status : inherit NCicUnifHint.status inherit NCicCoercion.status inherit NCicLibrary.status - method set_rstatus: status -> 'self + method set_rstatus: + < coerc_db : NCicCoercion.db; + uhint_db : NCicUnifHint.db; + timestamp: NCicLibrary.timestamp; .. > -> 'self end module Serializer: @@ -30,5 +33,9 @@ class dumpable_status : inherit status method dump: Serializer.obj list method set_dump: Serializer.obj list -> 'self - method set_dumpable_status: dumpable_status -> 'self + method set_dumpable_status: + < coerc_db : NCicCoercion.db; + uhint_db : NCicUnifHint.db; + timestamp: NCicLibrary.timestamp; + dump: Serializer.obj list; .. > -> 'self end diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index dab608e8a..fc0a8013c 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -179,17 +179,16 @@ let compare_statuses ~past ~present = (e.g. the tactic could perform a global analysis of the set of goals) *) -let exec tac low_status g = +let exec tac (low_status : #lowtac_status) g = let stack = [ [0,Open g], [], [], `NoTag ] in let status = - (new NTacStatus.status low_status#obj stack)#set_estatus - (low_status :> NEstatus.status) + (new NTacStatus.status low_status#obj stack)#set_estatus low_status in let status = tac status in - (low_status#set_estatus (status :> NEstatus.status))#set_obj status#obj + (low_status#set_estatus status)#set_obj status#obj ;; -let distribute_tac tac status = +let distribute_tac tac (status : #tac_status) = match status#stack with | [] -> assert false | (g, t, k, tag) :: s -> @@ -226,7 +225,7 @@ let distribute_tac tac status = let stack = (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s in - ((status#set_stack stack)#set_obj (sn :> lowtac_status)#obj)#set_estatus (sn :> NEstatus.status) + ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn ;; let atomic_tac htac = distribute_tac (exec htac) ;; @@ -248,7 +247,7 @@ let first_tac tacl status = | Some x -> x ;; -let exact_tac t = distribute_tac (fun status goal -> +let exact_tac t : 's tactic = distribute_tac (fun status goal -> let goalty = get_goalty status goal in let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in instantiate status goal t) -- 2.39.2