X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=2429dcfeddb51b4bc2ec24fb6aa6e52143a0d03e;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=5c42f9e76c9efeb0af3dd3c6fbe87bd6e1afc24a;hpb=298fa826610192b1a173c81b4ebf961c1c7e6609;p=helm.git diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 5c42f9e76..2429dcfed 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -40,6 +40,8 @@ type id = string (* the abstract type of the (annotated) node identifiers *) type anntarget = Object of annobj | Term of annterm + | Conjecture of annconjecture + | Hypothesis of annhypothesis (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) and sort = @@ -52,7 +54,8 @@ and name = and term = Rel of int (* DeBrujin index *) | Var of UriManager.uri (* uri *) - | Meta of int (* numeric id *) + | Meta of int * (term option) list (* numeric id, *) + (* local context *) | Sort of sort (* sort *) | Implicit (* *) | Cast of term * term (* value, type *) @@ -61,10 +64,11 @@ and term = | 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*) + (* 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, *) int * (* ind. typeno, *) @@ -78,7 +82,7 @@ and obj = | 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, *) + | CurrentProof of string * metasenv * (* name, conjectures, *) term * term (* value, type *) | InductiveDefinition of inductiveType list * (* inductive types, *) (int * UriManager.uri list) list * int (* parameters, n ind. pars *) @@ -92,58 +96,52 @@ and inductiveFun = and coInductiveFun = string * term * term (* name, type, body *) +(* a metasenv is a list of declarations of metas *) +and conjecture = int * context * term +and metasenv = conjecture list + +(* a metasenv is a list of declarations of metas *) +and annconjecture = id * int * anncontext * annterm +and annmetasenv = annconjecture list + and annterm = - ARel of id * annotation option ref * - int * string option (* DeBrujin index, binder *) - | AVar of id * annotation option ref * - UriManager.uri (* uri *) - | AMeta of id * annotation option ref * int (* numeric id *) - | ASort of id * annotation option ref * sort (* sort *) - | AImplicit of id * annotation option ref (* *) - | ACast of id * annotation option ref * - annterm * annterm (* value, type *) - | AProd of id * annotation option ref * - name * annterm * annterm (* binder, source, target *) - | ALambda of id * annotation option ref * - name * annterm * annterm (* binder, source, target *) - | ALetIn of id * annotation option ref * - name * annterm * annterm (* binder, term, target *) - | AAppl of id * annotation option ref * - annterm list (* arguments *) - | AConst of id * annotation option ref * - UriManager.uri * int (* uri, number of cookings*) - | AAbst of id * annotation option ref * - UriManager.uri (* uri *) - | AMutInd of id * annotation option ref * - UriManager.uri * int * int (* uri, cookingsno, typeno*) - | AMutConstruct of id * annotation option ref * - UriManager.uri * int * (* uri, cookingsno, *) + ARel of id * int * string (* DeBrujin index, binder *) + | AVar of id * UriManager.uri (* uri *) + | AMeta of id * int * (annterm option) list (* numeric id, *) + (* local context *) + | ASort of id * sort (* sort *) + | AImplicit of id (* *) + | 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*) + (* 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 * annotation option ref * - UriManager.uri * int * (* ind. uri, cookingsno *) + | AMutCase of id * UriManager.uri * int * (* ind. uri, cookingsno *) int * (* ind. typeno, *) annterm * annterm * (* outtype, ind. term *) annterm list (* patterns *) - | AFix of id * annotation option ref * - int * anninductiveFun list (* funno, functions *) - | ACoFix of id * annotation option ref * - int * anncoInductiveFun list (* funno, functions *) + | AFix of id * int * anninductiveFun list (* funno, functions *) + | ACoFix of id * int * anncoInductiveFun list (* funno, functions *) and annobj = - ADefinition of id * annotation option ref * - string * (* id, *) + ADefinition of id * string * (* id, *) annterm * annterm * (* value, type, *) (int * UriManager.uri list) list exactness (* parameters *) - | AAxiom of id * annotation option ref * - string * annterm * (* id, type *) + | AAxiom of id * string * annterm * (* id, type *) (int * UriManager.uri list) list (* parameters *) - | AVariable of id * annotation option ref * + | AVariable of id * string * annterm option * annterm (* name, body, type *) - | ACurrentProof of id * annotation option ref * - string * (int * annterm) list * (* name, conjectures, *) + | ACurrentProof of id * + string * annmetasenv * (* name, conjectures, *) annterm * annterm (* value, type *) | AInductiveDefinition of id * - annotation option ref * anninductiveType list * (* inductive types , *) + anninductiveType list * (* inductive types , *) (int * UriManager.uri list) list * int (* parameters,n ind. pars*) and anninductiveType = string * bool * annterm * (* typename, inductive, arity *) @@ -159,4 +157,21 @@ and annotation = 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 + +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;;