* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
+ | Type of CicUniv.universe
| CProp
-and name =
- Name of string
+
+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 *)
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 *)
(* 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 *)
| 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 *)
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 *)
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
+
projects / helm.git / blobdiff