X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fng_kernel%2FnCicEnvironment.mli;h=790d72abe096b1d3884c73f6f77df313142b3174;hb=b98ec1a1a37602eca524dc5487c357a200bbb5b6;hp=80fcd2b68e4f993c3e49adfe2fe6c7c115df7399;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/ng_kernel/nCicEnvironment.mli b/matitaB/components/ng_kernel/nCicEnvironment.mli
index 80fcd2b68..790d72abe 100644
--- a/matitaB/components/ng_kernel/nCicEnvironment.mli
+++ b/matitaB/components/ng_kernel/nCicEnvironment.mli
@@ -16,41 +16,66 @@ exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t * exn;;
 exception AlreadyDefined of string Lazy.t;;
 
-val set_get_obj: (NCic.status -> NUri.uri -> NCic.obj) -> unit
+type item = 
+  [ `Obj of NUri.uri * NCic.obj 
+  | `Constr of NCic.universe * NCic.universe ]
+;;
 
-val get_checked_obj: #NCic.status -> NUri.uri -> NCic.obj
+type obj_exn =
+  [ `WellTyped of NCic.obj
+  | `Exn of exn ]
+;;
 
-val check_and_add_obj: #NCic.status -> NCic.obj -> unit
+type db
 
-val get_relevance: #NCic.status -> NReference.reference -> bool list
+class type g_status = 
+  object
+    method env_db : db
+  end
+
+class virtual status : string option ->
+ object('self)
+  inherit NCic.status
+  inherit g_status
+  method set_env_db : db -> 'self
+  method set_env_status : #g_status -> 'self
+ end
+
+val set_get_obj : (status -> NUri.uri -> NCic.obj) -> unit
+val set_typecheck_obj : (status -> NCic.obj -> unit) -> unit
+
+val get_checked_obj: #status -> NUri.uri -> NCic.obj
+
+val check_and_add_obj: #status -> NCic.obj -> unit
+
+val get_relevance: #status -> NReference.reference -> bool list
 
 val get_checked_def:
-  #NCic.status -> NReference.reference -> 
+    #status -> NReference.reference -> 
     NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int
 
 (* the last integer is the index of the inductive type in the reference *)
 val get_checked_indtys:
-  #NCic.status -> NReference.reference -> 
+    #status -> NReference.reference -> 
     bool * int * NCic.inductiveType list * NCic.i_attr * int
 
 val get_checked_fixes_or_cofixes:
-  #NCic.status -> NReference.reference -> 
+   #status -> NReference.reference -> 
    NCic.inductiveFun list * NCic.f_attr * int
 
-val invalidate_item: 
+val invalidate_item:
+      #status -> 
       [ `Obj of NUri.uri * NCic.obj 
       | `Constr of NCic.universe * NCic.universe ] -> unit
 
-val invalidate: unit -> unit
-
-val set_typecheck_obj: (NCic.status -> NCic.obj -> unit) -> unit
+val invalidate: #status -> unit
 
 (* =========== universes ============= *)
 
 (* utils *)
 val ppsort : Format.formatter -> NCic.sort -> unit
-val pp_constraints: unit -> string
-val get_universes: unit -> NCic.universe list
+val pp_constraints: #status -> string
+val get_universes: #status -> NCic.universe list
 
 (* use to type products *)
 val max: NCic.universe -> NCic.universe -> NCic.universe
@@ -58,13 +83,13 @@ val max: NCic.universe -> NCic.universe -> NCic.universe
 (* raise BadConstraints if the second arg. is an inferred universe or
  * if the added constraint gives circularity *)
 exception BadConstraint of string Lazy.t;;
-val add_lt_constraint: NCic.universe -> NCic.universe -> unit
+val add_lt_constraint: #status -> NCic.universe -> NCic.universe -> unit
 val universe_eq: NCic.universe -> NCic.universe -> bool
-val universe_leq: NCic.universe -> NCic.universe -> bool
-val universe_lt: NCic.universe -> NCic.universe -> bool
+val universe_leq: #status -> NCic.universe -> NCic.universe -> bool
+val universe_lt: #status -> NCic.universe -> NCic.universe -> bool
 
 (* checks if s1 <= s2 *)
-val are_sorts_convertible: test_eq_only:bool -> NCic.sort -> NCic.sort -> bool
+val are_sorts_convertible: #status -> test_eq_only:bool -> NCic.sort -> NCic.sort -> bool
 
 (* to type a Match *)
 val allowed_sort_elimination: NCic.sort -> NCic.sort -> [ `Yes | `UnitOnly ]
@@ -72,11 +97,11 @@ val allowed_sort_elimination: NCic.sort -> NCic.sort -> [ `Yes | `UnitOnly ]
 (* algebraic successor function *)
 exception UntypableSort of string Lazy.t
 exception AssertFailure of string Lazy.t
-val typeof_sort: NCic.sort -> NCic.sort
+val typeof_sort: #status -> NCic.sort -> NCic.sort
 
 (* looks for a declared universe that is the least one above the input *)
-val sup : NCic.universe -> NCic.universe option
-val inf : strict:bool -> NCic.universe -> NCic.universe option
+val sup : #status -> NCic.universe -> NCic.universe option
+val inf : #status -> strict:bool -> NCic.universe -> NCic.universe option
 val family_of : NCic.universe -> [ `CProp | `Type ]
 
 (* =========== /universes ============= *)