From 53ce2802674bae2ebe5f8fccb446fb9c36f90522 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 13 Feb 2008 12:46:12 +0000 Subject: [PATCH] added leftno to indtypes, better indentation and comments --- helm/software/components/ng_kernel/nCic.ml | 80 ++++++++++------------ 1 file changed, 36 insertions(+), 44 deletions(-) diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 8d974ca10..6691acd47 100644 --- 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,31 @@ type metasenv = conjecture list type substitution = (int * (string option * context * term * term)) list +(******************************** OBJECTS **********************************) +type inductiveFun = string * int * term * term + (* if coinductive, the int has no meaning and must be set to -1 *) -type inductiveFun = - 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 = string * term (* id, type *) type inductiveType = - string * bool * term * (* typename, inductive, arity *) - constructor list (* constructors *) + string * bool * term * int * (* typename, inductive, arity, leftno *) + constructor list (* constructors *) type def_flavour = (* presentational *) - [ `Definition - | `Fact - | `Lemma - | `Remark - | `Theorem - ] + [ `Definition | `Fact | `Lemma | `Remark | `Theorem | `Corollary ] 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 ] 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,6 +96,7 @@ 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 | Fixpoint of NUri.uri * metasenv * substitution * bool * inductiveFun list * f_attr -- 2.39.2