severe bug found in parallel zeta

[helm.git] / matita / components / ng_kernel / nCic.ml

diff --git a/matita/components/ng_kernel/nCic.ml b/matita/components/ng_kernel/nCic.ml
index fa204588dc2dd3e5e08ac4558f1d0a1c5e7b73bf..ebf6f8ef5139779ecc517e0fb9ee83568c14880e 100644 (file)
--- a/matita/components/ng_kernel/nCic.ml
+++ b/matita/components/ng_kernel/nCic.ml
@@ -94,6 +94,7 @@ type def_pragma = (* pragmatic of the object *)
   | `Elim of sort       (* elimination principle; universe is not relevant *)
   | `Projection         (* record projection *)
   | `InversionPrinciple (* inversion principle *)
+  | `DiscriminationPrinciple (* discrimination principle *)
   | `Variant 
   | `Local 
   | `Regular ]            (* Local = hidden technicality *)
@@ -103,11 +104,14 @@ type ind_pragma = (* pragmatic of the object *)
   (* inductive type that encodes a record; the arguments are the record 
    * fields names and if they are coercions and then the coercion arity *)
 
-type generated = [ `Generated | `Provided ]
+type source = [ `Generated (* generated by matita *)
+              | `Provided  (* provided as defined by the user *)
+              | `Implied   (* provided as generated by another ITP *)
+              ]
 
-type c_attr = generated * def_flavour * def_pragma
-type f_attr = generated * def_flavour * def_pragma
-type i_attr = generated * ind_pragma
+type c_attr = source * def_flavour * def_pragma
+type f_attr = source * def_flavour * def_pragma
+type i_attr = source * ind_pragma
 
  (* invariant: metasenv and substitution have disjoint domains *)
 type obj_kind =
@@ -119,3 +123,38 @@ type obj_kind =
 
  (* the int must be 0 if the object has no body *)
 type obj = NUri.uri * int * metasenv * substitution * obj_kind
+
+(* pretty-printing *)
+class virtual status =
+ object
+  method virtual ppterm: context:context -> subst:substitution ->
+   metasenv:metasenv -> ?margin:int -> ?inside_fix:bool -> term -> string
+
+  method virtual ppcontext: ?sep:string -> subst:substitution ->
+   metasenv:metasenv -> context -> string 
+
+  method virtual ppmetasenv: subst:substitution -> metasenv -> string
+
+  method virtual ppsubst: metasenv:metasenv -> ?use_subst:bool -> substitution -> string
+
+  method virtual ppobj: obj -> string
+ end
+
+(* pretty-printing: same as vstatus, but all methods are concrete         *)
+(* used only to declare concrete instances of subclasses of vstatus class *)
+class type cstatus =
+ object
+  inherit status
+
+  method ppterm: context:context -> subst:substitution ->
+   metasenv:metasenv -> ?margin:int -> ?inside_fix:bool -> term -> string
+
+  method ppcontext: ?sep:string -> subst:substitution ->
+   metasenv:metasenv -> context -> string 
+
+  method ppmetasenv: subst:substitution -> metasenv -> string
+
+  method ppsubst: metasenv:metasenv -> ?use_subst:bool -> substitution -> string
+
+  method ppobj: obj -> string
+ end