]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_library/nCicLibrary.mli
Big change:
[helm.git] / matita / components / ng_library / nCicLibrary.mli
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$ *)
13
14 exception LibraryOutOfSync of string Lazy.t
15 exception IncludedFileNotCompiled of string * string 
16
17 type timestamp
18
19 class status :
20  object ('self)
21   method timestamp: timestamp
22   method set_timestamp: timestamp -> 'self
23  end
24
25 (* it also checks it and add it to the environment *)
26 val add_obj: #status as 'status -> NCic.obj -> 'status
27 val add_constraint: 
28   #status as 'status -> NCic.universe -> NCic.universe -> 'status
29 val aliases_of: NUri.uri -> NReference.reference list
30 val resolve: string -> NReference.reference list
31 (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *)
32 val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *)
33
34 val clear_cache : unit -> unit
35
36 val time_travel: #status -> unit
37 val decompile: baseuri:NUri.uri -> unit
38
39 val init: unit -> unit
40
41 type obj
42
43 module type SerializerType =
44  sig
45   type dumpable_status
46
47   type 'a register_type =
48    'a ->
49     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
50     refresh_uri_in_term:(NCic.term -> NCic.term) ->
51     refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
52     alias_only:bool ->
53      dumpable_status -> dumpable_status
54
55   val register: < run: 'a.  string -> 'a register_type -> ('a -> obj) >
56   val serialize: baseuri:NUri.uri -> dependencies:string list -> obj list ->
57        unit
58    (* the obj is the "include" command to be added to the dump list *)
59   val require: baseuri:
60    NUri.uri -> alias_only:bool -> dumpable_status -> dumpable_status * obj
61   val dependencies_of: baseuri:NUri.uri -> string list
62  end
63
64 module Serializer(D: sig type dumpable_status end) :
65   SerializerType with type dumpable_status = D.dumpable_status
66
67 class dumpable_status :
68  object ('self)
69   method dump: obj list
70   method set_dump: obj list -> 'self
71  end
72
73 val refresh_uri: NUri.uri -> NUri.uri
74
75 val ng_path_of_baseuri: ?no_suffix:bool -> NUri.uri -> string
76
77 (* IMPERATIVE STUFF, TO BE PUT IN THE STATUS *)
78 val get_already_included: unit -> NUri.uri list
79
80 (* EOF *)