X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCic.ml;h=97733891e8745b4e3251500878f4804abe1743ef;hb=f4c17198d8afe7c8cd62dbab527d08902d891491;hp=23ba6d084474b3500f051cddba1ddb3adfba039f;hpb=5f926fd66f345c273bc66cc3ab9b1344ad0eac25;p=helm.git diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index 23ba6d084..97733891e 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -1,229 +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/. - *) - -(*****************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 29/11/2000 *) -(* *) -(* This module defines the internal representation of the objects (variables,*) -(* blocks of (co)inductive definitions and constants) and the terms of cic *) -(* *) -(*****************************************************************************) - -(* $Id: cic.ml 7190 2007-01-31 18:36:04Z sacerdot $ *) (* -(* STUFF TO MANAGE IDENTIFIERS *) -type id = string (* the abstract type of the (annotated) node identifiers *) -type 'term explicit_named_substitution = (UriManager.uri * 'term) list + ||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$ *) -(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) +(********************************* TERMS ************************************) -type object_flavour = - [ `Definition - | `MutualDefinition - | `Fact - | `Lemma - | `Remark - | `Theorem - | `Variant - | `Axiom - ] +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 object_class = - [ `Coercion of int - | `Elim of sort (** elimination principle; if sort is Type, the universe is - * not relevant *) - | `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 *) - | `Projection (** record projection *) - | `InversionPrinciple (** inversion principle *) - ] - -type attribute = - [ `Class of object_class - | `Flavour of object_flavour - | `Generated - ] -*) -type sort = - | Prop - | Set - | Type of CicUniv.universe - | CProp - -type implicit_annotation = [ `Closed | `Type | `Hole | `Term ] - -type name = Name of string | Anonymous - -type local_context = int * (term list) option (* shift, subst (None means id) *) +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 *) + | Rel of int (* DeBruijn index, 1 based *) | Meta of int * 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 UriManager.uri (* uri contains indtypeno/constrno *) - | Sort of sort (* sort *) - | Implicit of implicit_annotation (* ... *) - | MutCase of UriManager.uri * (* ind. uri, *) - term * term * (* outtype, ind. term *) - term list (* patterns *) -and obj = - Constant of string * term option * term * (* id, body, type, *) - UriManager.uri list * attribute list (* parameters *) - | Variable of string * term option * term * (* name, body, type *) - UriManager.uri list * attribute list (* parameters *) - | CurrentProof of string * metasenv * term * (* name, conjectures, body, *) - term * UriManager.uri list * attribute list (* type, parameters *) - | InductiveDefinition of inductiveType list * (* inductive types, *) - UriManager.uri list * int * attribute list (* params, left params no *) -and inductiveType = - string * bool * term * (* typename, inductive, arity *) - constructor list (* constructors *) -and constructor = - string * term (* id, type *) -and inductiveFun = - string * int * term * term (* name, ind. index, type, body *) -and coInductiveFun = - string * term * term (* name, type, body *) - -(* a metasenv is a list of declarations of metas in declarations *) -(* order (i.e. [oldest ; ... ; newest]). Older variables can not *) -(* depend on new ones. *) -and conjecture = int * context * term -and metasenv = conjecture list -and substitution = (int * (context * term * term)) list - - - -(* a metasenv is a list of declarations of metas in declarations *) -(* order (i.e. [oldest ; ... ; newest]). Older variables can not *) -(* depend on new ones. *) -and annconjecture = id * int * anncontext * annterm -and annmetasenv = annconjecture list - -and annterm = - ARel of id * id * int * (* idref, DeBrujin index, *) - string (* binder *) - | AVar of id * UriManager.uri * (* uri, *) - annterm explicit_named_substitution (* explicit named subst. *) - | AMeta of id * int * (annterm option) list (* numeric id, *) - (* local context *) - | ASort of id * sort (* sort *) - | AImplicit of id * implicit_annotation option (* *) - | ACast of id * annterm * annterm (* value, type *) - | AProd of id * name * annterm * annterm (* binder, source, target *) - | ALambda of id * name * annterm * annterm (* binder, source, target *) - | ALetIn of id * name * annterm * annterm (* binder, term, target *) - | AAppl of id * annterm list (* arguments *) - | AConst of id * UriManager.uri * (* uri, *) - annterm explicit_named_substitution (* explicit named subst. *) - | AMutInd of id * UriManager.uri * int * (* uri, typeno *) - annterm explicit_named_substitution (* explicit named subst. *) - (* typeno is 0 based *) - | AMutConstruct of id * UriManager.uri * (* uri, *) - int * int * (* typeno, consno *) - annterm explicit_named_substitution (* explicit named subst. *) - (* typeno is 0 based *) - (* consno is 1 based *) - | AMutCase of id * UriManager.uri * (* ind. uri, *) - int * (* ind. typeno, *) - annterm * annterm * (* outtype, ind. term *) - annterm list (* patterns *) - | AFix of id * int * anninductiveFun list (* funno, functions *) - | ACoFix of id * int * anncoInductiveFun list (* funno, functions *) -and annobj = - AConstant of id * id option * string * (* name, *) - annterm option * annterm * (* body, type, *) - UriManager.uri list * attribute list (* parameters *) - | AVariable of id * - string * annterm option * annterm * (* name, body, type *) - UriManager.uri list * attribute list (* parameters *) - | ACurrentProof of id * id * - string * annmetasenv * (* name, conjectures, *) - annterm * annterm * UriManager.uri list * (* body,type,parameters *) - attribute list - | AInductiveDefinition of id * - anninductiveType list * (* inductive types , *) - UriManager.uri list * int * attribute list (* parameters,n ind. pars*) -and anninductiveType = - id * string * bool * annterm * (* typename, inductive, arity *) - annconstructor list (* constructors *) -and annconstructor = - string * annterm (* id, type *) -and anninductiveFun = - id * string * int * annterm * annterm (* name, ind. index, type, body *) -and anncoInductiveFun = - id * string * annterm * annterm (* name, type, body *) -and annotation = - string - -and context_entry = (* A declaration or definition *) - Decl of term - | Def of term * term option (* body, type (if known) *) - -and hypothesis = - (name * context_entry) option (* None means no more accessible *) - -and context = hypothesis list - -and anncontext_entry = (* A declaration or definition *) - ADecl of annterm - | ADef of annterm - -and annhypothesis = - id * (name * anncontext_entry) option (* None means no more accessible *) - -and anncontext = annhypothesis list -;; - -type lazy_term = - context -> metasenv -> CicUniv.universe_graph -> - term * metasenv * CicUniv.universe_graph - -type anntarget = - Object of annobj (* if annobj is a Constant, this is its type *) - | ConstantBody of annobj - | Term of annterm - | Conjecture of annconjecture - | Hypothesis of annhypothesis - -module CicHash = - Hashtbl.Make - (struct - type t = term - let equal = (==) - let hash = Hashtbl.hash_param 100 1000 - end) -;; + | 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