X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic.ml;h=32b79f02a2f898a2dadd8472b7aef08a38adca36;hb=da5dd88bbcc43d9f4342e47c922b820abf91c92f;hp=8d974ca101b4ddcee1969e25edc35d797450b275;hpb=d8f3098a13d52841ad0022617e7f7ce3c7848670;p=helm.git diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 8d974ca10..32b79f02a 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -1,112 +1,116 @@ -(* 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 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 univ_algebra = [ `Type | `Succ | `CProp ] + +type universe = (univ_algebra * 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 | `Tagged of string | `Term | `Typeof of int | `Vector ] + + +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 *) + | 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 (* name, entry *) type context = hypothesis list -type conjecture = int * string option * context * term +type meta_attrs = [`Name of string | `IsSort | `InScope | `OutScope of int] list + +type conjecture = meta_attrs * context * term + +type metasenv = (int * conjecture) list -type metasenv = conjecture list +type subst_entry = meta_attrs * context * term * term (* name,ctx,bo,ty *) -type substitution = (int * (string option * context * term * term)) list +type substitution = (int * subst_entry) 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 *) + (* 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 = 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 + | `Regular ] (* 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 | `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 f_attr = generated * def_flavour * def_pragma type i_attr = generated * ind_pragma -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 - | Inductive of NUri.uri * metasenv * substitution * inductiveType list * i_attr + (* 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