X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=aacaabda95490e4f9e1cfc9df946f6be70e08c8c;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=fd46c22b4820e74232d3e18e2e8a2eb46b073041;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index fd46c22b4..aacaabda9 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -23,45 +23,68 @@ * 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 *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* 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 *) +(* *) +(*****************************************************************************) (* STUFF TO MANAGE IDENTIFIERS *) type id = string (* the abstract type of the (annotated) node identifiers *) type 'term explicit_named_substitution = (UriManager.uri * 'term) list -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 +type implicit_annotation = [ `Closed | `Type | `Hole ] (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) -and sort = + +type sort = Prop | Set - | Type -and name = - Name of string + | Type of CicUniv.universe + | CProp + +type name = + | Name of string | Anonymous -and term = - Rel of int (* DeBrujin index *) + +type object_flavour = + [ `Definition + | `Fact + | `Lemma + | `Remark + | `Theorem + | `Variant + ] + +type object_class = + [ `Coercion + | `Elim of sort (** elimination principle; if sort is Type, the universe is + * not relevant *) + | `Record of string list (** inductive type that encodes a record; + the arguments are the record fields *) + | `Projection (** record projection *) + ] + +type attribute = + [ `Class of object_class + | `Flavour of object_flavour + | `Generated + ] + +type term = + Rel of int (* DeBrujin index, 1 based*) | Var of UriManager.uri * (* uri, *) term explicit_named_substitution (* explicit named subst. *) | Meta of int * (term option) list (* numeric id, *) (* local context *) | Sort of sort (* sort *) - | Implicit (* *) + | Implicit of implicit_annotation option (* *) | Cast of term * term (* value, type *) | Prod of name * term * term (* binder, source, target *) | Lambda of name * term * term (* binder, source, target *) @@ -81,17 +104,17 @@ and term = int * (* ind. typeno, *) term * term * (* outtype, ind. term *) term list (* patterns *) - | Fix of int * inductiveFun list (* funno, functions *) - | CoFix of int * coInductiveFun list (* funno, functions *) + | Fix of int * inductiveFun list (* funno (0 based), funs *) + | CoFix of int * coInductiveFun list (* funno (0 based), funs *) and obj = Constant of string * term option * term * (* id, body, type, *) - UriManager.uri list (* parameters *) + UriManager.uri list * attribute list (* parameters *) | Variable of string * term option * term * (* name, body, type *) - UriManager.uri list (* parameters *) - | CurrentProof of string * metasenv * (* name, conjectures, *) - term * term * UriManager.uri list (* value, type, parameters *) + 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 (* parameters, n ind. pars *) + UriManager.uri list * int * attribute list (* params, left params no *) and inductiveType = string * bool * term * (* typename, inductive, arity *) constructor list (* constructors *) @@ -107,6 +130,9 @@ and coInductiveFun = (* 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 *) @@ -122,7 +148,7 @@ and annterm = | AMeta of id * int * (annterm option) list (* numeric id, *) (* local context *) | ASort of id * sort (* sort *) - | AImplicit of id (* *) + | 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 *) @@ -147,16 +173,17 @@ and annterm = and annobj = AConstant of id * id option * string * (* name, *) annterm option * annterm * (* body, type, *) - UriManager.uri list (* parameters *) + UriManager.uri list * attribute list (* parameters *) | AVariable of id * string * annterm option * annterm * (* name, body, type *) - UriManager.uri list (* parameters *) + UriManager.uri list * attribute list (* parameters *) | ACurrentProof of id * id * string * annmetasenv * (* name, conjectures, *) - annterm * annterm * UriManager.uri list (* value,type,parameters *) + annterm * annterm * UriManager.uri list * (* body,type,parameters *) + attribute list | AInductiveDefinition of id * anninductiveType list * (* inductive types , *) - UriManager.uri list * int (* parameters,n ind. pars*) + UriManager.uri list * int * attribute list (* parameters,n ind. pars*) and anninductiveType = id * string * bool * annterm * (* typename, inductive, arity *) annconstructor list (* constructors *) @@ -171,7 +198,7 @@ and annotation = and context_entry = (* A declaration or definition *) Decl of term - | Def of term + | Def of term * term option (* body, type (if known) *) and hypothesis = (name * context_entry) option (* None means no more accessible *) @@ -185,4 +212,13 @@ and anncontext_entry = (* A declaration or definition *) and annhypothesis = id * (name * anncontext_entry) option (* None means no more accessible *) -and anncontext = annhypothesis list;; +and anncontext = annhypothesis list +;; + +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 +