X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcic%2Fcic.ml;h=8b1d379b7883bd10dca65c4aeec199b0eeff2d89;hb=cb11de1c61f0b61935b1c6c1832deacb49f7b5bd;hp=012f52eeac47ab02b2afc6d297f3fa258c19f414;hpb=d284dd23d0e12a62a001d3473eadf4942d12ffaa;p=helm.git diff --git a/matita/components/cic/cic.ml b/matita/components/cic/cic.ml index 012f52eea..8b1d379b7 100644 --- a/matita/components/cic/cic.ml +++ b/matita/components/cic/cic.ml @@ -37,17 +37,7 @@ (* $Id$ *) -(* 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 implicit_annotation = [ `Closed | `Type | `Hole ] - -(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) - -type sort = - Prop - | Set type name = | Name of string @@ -63,175 +53,3 @@ type object_flavour = | `Variant | `Axiom ] - -type object_class = - [ `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 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 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 * term (* binder, term, type, target *) - | Appl of term list (* arguments *) - | 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 (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 * 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 * annterm (* binder, term, type, 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 (* body, type *) - -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 * 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 - -module CicHash = - Hashtbl.Make - (struct - type t = term - let equal = (==) - let hash = Hashtbl.hash_param 100 1000 - end) -;; -