X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2Fcic.ml;h=aacaabda95490e4f9e1cfc9df946f6be70e08c8c;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=f9e99260d52944640d65ace9d5d9b6909be8cd42;hpb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;p=helm.git

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index f9e99260d..aacaabda9 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -23,42 +23,62 @@
  * 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 implicit_annotation = [ `Closed | `Type ]
-
-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 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,    *)
@@ -88,13 +108,13 @@ and term =
  | 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              *)
@@ -110,6 +130,9 @@ and coInductiveFun =
 (* 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 *)
@@ -150,16 +173,17 @@ and annterm =
 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              *)
@@ -190,3 +214,11 @@ and annhypothesis =
 
 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
+