X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=f9e99260d52944640d65ace9d5d9b6909be8cd42;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=2429dcfeddb51b4bc2ec24fb6aa6e52143a0d03e;hpb=e5667db48c0c19867da0326e25af258255e1ef08;p=helm.git diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 2429dcfed..f9e99260d 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -37,8 +37,13 @@ (* 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 ] + type anntarget = - Object of annobj + Object of annobj (* if annobj is a Constant, this is its type *) + | ConstantBody of annobj | Term of annterm | Conjecture of annconjecture | Hypothesis of annhypothesis @@ -47,120 +52,129 @@ type anntarget = and sort = Prop | Set - | Type + | Type of CicUniv.universe + | CProp and name = Name of string - | Anonimous + | Anonymous and term = Rel of int (* DeBrujin index *) - | Var of UriManager.uri (* uri *) + | 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*) - | MutInd of UriManager.uri * int * int (* uri, cookingsno, typeno*) - (* typeno is 0 based *) - | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *) - int * int (* typeno, consno *) - (* consno is 1 based *) - (*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 *) + Constant of string * term option * term * (* id, body, type, *) + UriManager.uri list (* parameters *) + | Variable of string * term option * term * (* name, body, type *) + UriManager.uri list (* parameters *) | CurrentProof of string * metasenv * (* name, conjectures, *) - term * term (* value, type *) + term * term * UriManager.uri list (* value, type, parameters *) | InductiveDefinition of inductiveType list * (* inductive types, *) - (int * UriManager.uri list) list * int (* parameters, n ind. pars *) + UriManager.uri list * int (* parameters, n ind. pars *) 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 *) +(* 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 -(* a metasenv is a list of declarations of metas *) +(* 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 *) + 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*) - | AMutInd of id * UriManager.uri * int * int (* uri, cookingsno, typeno*) + | 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 *) - | AMutConstruct of id * UriManager.uri * int * (* uri, cookingsno, *) - int * int (* typeno, consno *) (* consno is 1 based *) - (*CSC: serve cookingsno?*) - | AMutCase of id * UriManager.uri * int * (* ind. uri, cookingsno *) + | 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 (* parameters *) | AVariable of id * - string * annterm option * annterm (* name, body, type *) - | ACurrentProof of id * - string * annmetasenv * (* name, conjectures, *) - annterm * annterm (* value, type *) + string * annterm option * annterm * (* name, body, type *) + UriManager.uri list (* parameters *) + | ACurrentProof of id * id * + string * annmetasenv * (* name, conjectures, *) + annterm * annterm * UriManager.uri list (* value,type,parameters *) | AInductiveDefinition of id * anninductiveType list * (* inductive types , *) - (int * UriManager.uri list) list * int (* parameters,n ind. pars*) + UriManager.uri list * int (* 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 + | Def of term * term option (* body, type (if known) *) and hypothesis = (name * context_entry) option (* None means no more accessible *) @@ -174,4 +188,5 @@ 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 +;;