X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=aacaabda95490e4f9e1cfc9df946f6be70e08c8c;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=64b7f857cce087cc7f5925654939c2a613768434;hpb=ae326f646ef4c01b43d6da04201b427d1e175400;p=helm.git diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 64b7f857c..aacaabda9 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -23,124 +23,202 @@ * 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 anntarget = - Object of annobj - | Term of annterm +type 'term explicit_named_substitution = (UriManager.uri * 'term) list + +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 - | Anonimous -and term = - Rel of int (* DeBrujin index *) - | Var of UriManager.uri (* uri *) - | Meta of int (* numeric id *) + | Type of CicUniv.universe + | CProp + +type name = + | Name of string + | Anonymous + +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 *) | LetIn of name * term * term (* binder, term, target *) | Appl of term list (* arguments *) - | Const of UriManager.uri * int (* uri, number of cookings*) - | Abst of UriManager.uri (* uri *) - | MutInd of UriManager.uri * int * int (* uri, cookingsno, typeno*) - | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *) - int * int (* typeno, consno *) - (*CSC: serve cookingsno?*) - | MutCase of UriManager.uri * int * (* ind. uri, cookingsno, *) + | Const of UriManager.uri * (* uri, *) + term explicit_named_substitution (* explicit named subst. *) + | MutInd of UriManager.uri * int * (* uri, typeno, *) + term explicit_named_substitution (* explicit named subst. *) + (* typeno is 0 based *) + | MutConstruct of UriManager.uri * (* uri, *) + int * int * (* typeno, consno *) + term explicit_named_substitution (* explicit named subst. *) + (* typeno is 0 based *) + (* consno is 1 based *) + | MutCase of UriManager.uri * (* ind. uri, *) 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 = - Definition of string * term * term * (* id, value, type, *) - (int * UriManager.uri list) list (* parameters *) - | Axiom of string * term * - (int * UriManager.uri list) list (* id, type, parameters *) - | Variable of string * term option * term (* name, body, type *) - | CurrentProof of string * (int * term) list * (* name, conjectures, *) - term * term (* value, type *) + 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, *) - (int * UriManager.uri list) 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 *) and constructor = - string * term * bool list option ref (* id, type, really recursive *) + 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 * int * string (* DeBrujin index, binder *) - | AVar of id * UriManager.uri (* uri *) - | AMeta of id * int (* numeric id *) + 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 (* *) + | 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 * int (* uri, number of cookings*) - | AAbst of id * UriManager.uri (* uri *) - | AMutInd of id * UriManager.uri * int * int (* uri, cookingsno, typeno*) - | AMutConstruct of id * UriManager.uri * int * (* uri, cookingsno, *) - int * int (* typeno, consno *) - (*CSC: serve cookingsno?*) - | AMutCase of id * UriManager.uri * int * (* ind. uri, cookingsno *) + | 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 = - ADefinition of id * string * (* id, *) - annterm * annterm * (* value, type, *) - (int * UriManager.uri list) list exactness (* parameters *) - | AAxiom of id * string * annterm * (* id, type *) - (int * UriManager.uri list) list (* parameters *) + 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 *) - | ACurrentProof of id * - string * (int * annterm) list * (* name, conjectures, *) - annterm * annterm (* value, type *) + 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 , *) - (int * UriManager.uri list) list * int (* parameters,n ind. pars*) + UriManager.uri list * int * attribute list (* parameters,n ind. pars*) and anninductiveType = - string * bool * annterm * (* typename, inductive, arity *) + id * string * bool * annterm * (* typename, inductive, arity *) annconstructor list (* constructors *) and annconstructor = - string * annterm * bool list option ref (* id, type, really recursive *) + string * annterm (* id, type *) and anninductiveFun = - string * int * annterm * annterm (* name, ind. index, type, body *) + id * string * int * annterm * annterm (* name, ind. index, type, body *) and anncoInductiveFun = - string * annterm * annterm (* name, type, body *) + id * string * annterm * annterm (* name, type, body *) and annotation = string -and 'a exactness = - Possible of 'a (* an approximation to something *) - | Actual of 'a (* something *) + +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 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 +