(* *)
(*****************************************************************************)
+(* $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
| 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 *)
+ | `Record of (string * bool) list (**
+ inductive type that encodes a record; the arguments are
+ the record fields names and if they are coercions *)
| `Projection (** record projection *)
]
type attribute =
[ `Class of object_class
+ | `Flavour of object_flavour
| `Generated
]
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, value,*)
+ | 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 *)
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 , *)
and anncontext = annhypothesis list
;;
+type lazy_term =
+ context -> metasenv -> CicUniv.universe_graph ->
+ term * metasenv * CicUniv.universe_graph
+
type anntarget =
Object of annobj (* if annobj is a Constant, this is its type *)
| ConstantBody of annobj
| Conjecture of annconjecture
| Hypothesis of annhypothesis
+module CicHash =
+ Hashtbl.Make
+ (struct
+ type t = term
+ let equal = (==)
+ let hash = Hashtbl.hash
+ end)
+;;
+