helm/software/components/ng_refiner/nRstatus.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
  13
  14 class type ctstatus =
  15  object ('self)
  16   inherit NCicUnifHint.status
  17   inherit NCicCoercion.status
  18   inherit NCicLibrary.status
  19   method set_rstatus : ctstatus -> 'self
  20  end
  21
  22 class status : ctstatus =
  23  object (self)
  24   inherit NCicUnifHint.status
  25   inherit NCicCoercion.status
  26   inherit NCicLibrary.status
  27   method set_rstatus o =
  28    ((self#set_unifhint_status (o :> NCicUnifHint.status))
  29          #set_coercion_status (o :> NCicCoercion.status))
  30          #set_library_status  (o :> NCicLibrary.status)
  31  end
  32
  33 type sstatus = status
  34
  35 module Serializer =
  36  struct
  37   include NCicLibrary.Serializer(struct type status = sstatus end)
  38
  39   let require ~baseuri status =
  40    let rstatus = require ~baseuri (status : #status :> status) in
  41    let status = status#set_uhint_db (rstatus#uhint_db) in
  42    let status = status#set_coerc_db (rstatus#coerc_db) in
  43    let status = status#set_timestamp (rstatus#timestamp) in
  44     status
  45  end
  46
  47 class type ctdumpable_status =
  48  object ('self)
  49   inherit status
  50   method dump: Serializer.obj list
  51   method set_dump: Serializer.obj list -> 'self
  52   method set_dumpable_status: ctdumpable_status -> 'self
  53  end
  54
  55 class dumpable_status : ctdumpable_status =
  56  object
  57   inherit status
  58   val dump = ([] : Serializer.obj list)
  59   method dump = dump
  60   method set_dump v = {< dump = v >}
  61   method set_dumpable_status o =
  62    {< dump = o#dump >}#set_rstatus (o :> status)
  63  end