X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=6e200cc310e1559db1e3b1875f6d44a7332294c6;hb=1a40d93d10be4ee71ae9474384af931d70918690;hp=ba51157ff9f4aa24464733c0820f0b518e4d7119;hpb=8f8d3ad5a02faed2ddcaa22f49a9099175445ef4;p=helm.git diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index ba51157ff..6e200cc31 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -53,17 +53,28 @@ type name = | 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 ] @@ -101,7 +112,7 @@ and obj = 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 *) @@ -169,7 +180,7 @@ and annobj = 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 , *) @@ -205,6 +216,10 @@ and annhypothesis = 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 @@ -212,3 +227,12 @@ type anntarget = | Conjecture of annconjecture | Hypothesis of annhypothesis +module CicHash = + Hashtbl.Make + (struct + type t = term + let equal = (==) + let hash = Hashtbl.hash + end) +;; +