X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic.ml;h=97733891e8745b4e3251500878f4804abe1743ef;hb=c7a74f0ef29118fc97c1a6283f4249a0ed4b0ba1;hp=2ff591ffc3052c4ea73e10ae4fe4a1c45c917b83;hpb=1f46c68d7ad8e10c0321b42f4a653df8fdf3be12;p=helm.git diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 2ff591ffc..97733891e 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -1,63 +1,110 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -type sort = - | Prop - | Set - | Type of int - | CProp - -type implicit_annotation = [ `Closed | `Type | `Hole | `Term ] - -type name = Name of string | Anonymous - -type local_context = int * (term list) option (* shift (0 -> no shift), - subst (None means id) *) +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) +(* $Id$ *) + +(********************************* TERMS ************************************) + +type universe = (bool * NUri.uri) list + (* Max of non-empty list of named universes, or their successor (when true) + * The empty list represents type0 *) + +type sort = Prop | Type of universe + +type implicit_annotation = [ `Closed | `Type | `Hole | `Term | `Typeof of int ] + +type lc_kind = Irl of int | Ctx of term list + +and local_context = int * lc_kind (* shift (0 -> no shift), + subst (Irl n means id of + length n) *) and term = - | Rel of int (* DeBruijn index, 1 based *) - | Meta of int * string option * local_context - | Appl of term list (* arguments *) - | Prod of name * term * term (* binder, source, target *) - | Lambda of name * term * term (* binder, source, target *) - | LetIn of name * term * term * term (* binder, type, term, body *) - | Const of NUriManager.reference (* reference contains indtypeno/constrno *) - | Sort of sort (* sort *) - | Implicit of implicit_annotation (* ... *) - | MutCase of NUriManager.reference * (* ind. reference, *) - term * term * (* outtype, ind. term *) - term list (* patterns *) - -and obj = - | Constant of term option * term - | InductiveDefinition of inductiveType list (* inductive types, *) - -and inductiveType = - string * bool * term * (* typename, inductive, arity *) - constructor list (* constructors *) - -and constructor = - string * term (* id, type *) + | 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 *) +(* Cast \def degenerate LetIn *) + | 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 (* type *) + | Def of term * term (* body, type *) + +type hypothesis = string * context_entry (* name, entry *) + +type context = hypothesis list + +type conjecture = string option * context * term + +type metasenv = (int * conjecture) list + +type subst_entry = string option * context * term * term (* name,ctx,bo,ty *) + +type substitution = (int * subst_entry) list + + +(******************************** OBJECTS **********************************) + +type relevance = bool list (* relevance of arguments for conversion *) + + (* relevance, name, recno, ty, bo *) +type inductiveFun = relevance * string * int * term * term + (* if coinductive, the int has no meaning and must be set to -1 *) + +type constructor = relevance * string * term (* id, type *) + +type inductiveType = + relevance * string * term * constructor list + (* relevance, typename, arity, constructors *) + +type def_flavour = (* presentational *) + [ `Definition | `Fact | `Lemma | `Theorem | `Corollary | `Example ] + +type def_pragma = (* pragmatic of the object *) + [ `Coercion of int + | `Elim of sort (* elimination principle; universe is not relevant *) + | `Projection (* record projection *) + | `InversionPrinciple (* inversion principle *) + | `Variant + | `Local + | `Regular ] (* Local = hidden technicality *) + +type ind_pragma = (* pragmatic of the object *) + [ `Record of (string * bool * int) list | `Regular ] + (* 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 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_kind = + | Constant of relevance * string * term option * term * c_attr + | Fixpoint of bool * inductiveFun list * f_attr + (* true -> fix, funcs, arrts *) + | Inductive of bool * int * inductiveType list * i_attr + (* true -> inductive, leftno, types *) + (* the int must be 0 if the object has no body *) +type obj = NUri.uri * int * metasenv * substitution * obj_kind