added Local pragma, moved leftno and inductive into obj, added relevance attribute...

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

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index 8d974ca101b4ddcee1969e25edc35d797450b275..43f6c86d9ae03a3b05afc1da41270c2131de281e 100644 (file)
--- a/helm/software/components/ng_kernel/nCic.ml
+++ b/helm/software/components/ng_kernel/nCic.ml
@@ -23,38 +23,37 @@
  * http://cs.unibo.it/helm/.
  *)
 
-type sort =
- | Prop
- | Set
- | Type of int
- | CProp
+(********************************* TERMS ************************************)
+
+type sort = Prop | Set | Type of int | CProp
 
 type implicit_annotation = [ `Closed | `Type | `Hole | `Term ]
 
-type local_context = int * (term list) option         (* shift (0 -> no shift), 
-                                                         subst (None means id) *) 
+type local_context = int * (term list) option    (* shift (0 -> no shift), 
+                                                    subst (None means id) *) 
 and term =
- | Rel      of int                                    (* DeBruijn index, 1 based         *)
+ | Rel      of int                            (* DeBruijn index, 1 based    *)
  | Meta     of int * local_context
- | Appl     of term list                              (* arguments                       *)
- | Prod     of string * term * term                     (* binder, source, target          *)
- | Lambda   of string * term * term                     (* binder, source, target          *)
- | LetIn    of string * term * term * term              (* binder, type, term, body        *)
+ | Appl     of term list                      (* arguments                  *)
+ | Prod     of string * term * term           (* binder, source, target     *)
+ | Lambda   of string * term * term           (* binder, source, target     *)
+ | LetIn    of string * term * term * term    (* binder, type, term, body   *)
 (* Cast \def degenerate LetIn *)
- | Const    of NReference.reference                   (* reference contains indtypeno/constrno *)
- | Sort     of sort                                   (* sort                            *)
- | Implicit of implicit_annotation                    (* ... *)
- | Match    of NReference.reference *                 (* ind. reference,             *)
-    term * term *                                     (*  outtype, ind. term   *)
-    term list                                         (*  patterns             *)
+ | Const    of NReference.reference           (* ref has (indtype|constr)no *)
+ | Sort     of sort                           (* sort                       *)
+ | Implicit of implicit_annotation            (* ...                        *)
+ | Match    of NReference.reference *         (* ind. reference,            *)
+    term * term *                             (*  outtype, ind. term        *)
+    term list                                 (*  patterns                  *)
 
 
+(********************************* TYPING ***********************************)
 
-type context_entry =                            (* A declaration or definition *)
- | Decl of term
- | Def of term * term option                   (* body, type (if known) *)
+type context_entry =                       (* A declaration or definition *)
+ | Decl of term                            (* type *)
+ | Def  of term * term                     (* body, type *)
 
-type hypothesis = string * context_entry               (* None means no more accessible *)
+type hypothesis = string * context_entry   
 
 type context = hypothesis list
 
@@ -65,39 +64,34 @@ type metasenv = conjecture list
 type substitution = (int * (string option * context * term * term)) list
 
 
+(******************************** OBJECTS **********************************)
 
+type relevance = bool list (* relevance of arguments for conversion *)
 
-type inductiveFun =
- string * int * term * term   (* if coinductive, the int has no meaning and must be set to -1 *)
+type inductiveFun = relevance * string * int * term * term 
+  (* if coinductive, the int has no meaning and must be set to -1 *)
 
-type constructor = string * term                                (* id, type *)
+type constructor = relevance * string * term  (* id, type *)
 
 type inductiveType = 
- string * bool * term *       (* typename, inductive, arity *)
- constructor list            (* constructors              *)
+ relevance * string * term * constructor list    
+ (* relevance, typename, arity, constructors *)
 
 type def_flavour = (* presentational *)
-  [ `Definition
-  | `Fact
-  | `Lemma
-  | `Remark
-  | `Theorem
-  ]
+  [ `Definition | `Fact | `Lemma | `Theorem | `Corollary | `Example ]
 
 type def_pragma = (* pragmatic of the object *)
   [ `Coercion of int
-  | `Elim of sort       (** elimination principle; if sort is Type, the universe is not relevant *)
-  | `Projection         (** record projection *)
-  | `InversionPrinciple (** inversion principle *)
-  | `Variant
-  ]
+  | `Elim of sort       (* elimination principle; universe is not relevant *)
+  | `Projection         (* record projection *)
+  | `InversionPrinciple (* inversion principle *)
+  | `Variant 
+  | `Local ] (* Local = hidden technicality *)
  
 type ind_pragma = (* pragmatic of the object *)
-  [ `Record of (string * bool * int) list (** 
-    inductive type that encodes a record; the arguments are
-    the record fields names and if they are coercions and
-    then the coercion arity *)
-  ]
+  [ `Record of (string * bool * int) list ]
+  (* 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 ]
 
@@ -105,8 +99,10 @@ type c_attr = generated * def_flavour * def_pragma
 type f_attr = generated * def_flavour
 type i_attr = generated * ind_pragma
 
+ (* invariant: metasenv and substitution have disjoint domains *)
 type obj =
- | Constant  of NUri.uri * metasenv * substitution * string * term option * term * c_attr
+ | Constant  of NUri.uri * metasenv * substitution * relevance * string * term option * term * c_attr
  | Fixpoint  of NUri.uri * metasenv * substitution * bool * inductiveFun list * f_attr
- | Inductive of NUri.uri * metasenv * substitution * inductiveType list * i_attr
+ | Inductive of NUri.uri * metasenv * substitution * bool * int * inductiveType list * i_attr
+                (* uri, menv, subst, (co)inductive, leftno, types *)