Initial revision

[helm.git] / helm / ocaml / cic / cic.ml

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index 550d4a8f6d306f14dd1caba58b7a183503784a8b..2429dcfeddb51b4bc2ec24fb6aa6e52143a0d03e 100644 (file)
--- 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 =
@@ -62,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,         *)
@@ -93,9 +96,13 @@ and inductiveFun =
 and coInductiveFun =
  string * term * term                         (* name, type, body *)
 
-and metasenv = (int * context * term) list (* a metasenv is a list of declarations of metas *)
+(* a metasenv is a list of declarations of metas *)
+and conjecture = int * context * term
+and metasenv = conjecture list
 
-and annmetasenv = (int * anncontext * annterm) list (* a metasenv is a list of declarations of metas *)
+(* a metasenv is a list of declarations of metas *)
+and annconjecture = id * int * anncontext * annterm
+and annmetasenv = annconjecture list
 
 and annterm =
    ARel of id * int * string                        (* DeBrujin index, binder *)
@@ -110,10 +117,11 @@ and annterm =
  | 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*)
- | AAbst of id * UriManager.uri                     (* uri *)
  | 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 * UriManager.uri * int *          (* ind. uri, cookingsno  *)
     int *                                           (*  ind. typeno,         *)
@@ -150,14 +158,20 @@ and 'a exactness =
    Possible of 'a                            (* an approximation to something *)
  | Actual of 'a                              (* something *)
 
-and context_entry =                    (* Contexts are lists of context_entry *)
+and context_entry =                            (* A declaration or definition *)
    Decl of term
  | Def of term
 
-and context = ((name * context_entry) option) list
+and hypothesis =
+ (name * context_entry) option               (* None means no more accessible *)
 
-and anncontext_entry =                 (* Contexts are lists of context_entry *)
+and context = hypothesis list
+
+and anncontext_entry =                         (* A declaration or definition *)
    ADecl of annterm
  | ADef of annterm
 
-and anncontext = ((name * anncontext_entry) option) list;;
+and annhypothesis =
+ id * (name * anncontext_entry) option       (* None means no more accessible *)
+
+and anncontext = annhypothesis list;;