helm/interface/cic.ml

   1 (******************************************************************************)
   2 (*                                                                            *)
   3 (*                               PROJECT HELM                                 *)
   4 (*                                                                            *)
   5 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
   6 (*                                 14/06/2000                                 *)
   7 (*                                                                            *)
   8 (* This module defines the internal representation of the objects (variables, *)
   9 (* blocks of (co)inductive definitions and constants) and the terms of cic    *)
  10 (*                                                                            *)
  11 (******************************************************************************)
  12
  13 (* STUFF TO MANAGE IDENTIFIERS *)
  14 type id = string  (* the abstract type of the (annotated) node identifiers *)
  15 type anntarget =
  16    Object of annobj
  17  | Term of annterm
  18
  19 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
  20 and sort =
  21    Prop
  22  | Set
  23  | Type
  24 and name =
  25    Name of string
  26  | Anonimous
  27 and term =
  28    Rel of int                                       (* DeBrujin index *)
  29  | Var of UriManager.uri                            (* uri *)
  30  | Meta of int                                      (* numeric id *)
  31  | Sort of sort                                     (* sort *)
  32  | Implicit                                         (* *)
  33  | Cast of term * term                              (* value, type *)
  34  | Prod of name * term * term                       (* binder, source, target *)
  35  | Lambda of name * term * term                     (* binder, source, target *)
  36  | Appl of term list                                (* arguments *)
  37  | Const of UriManager.uri * int                    (* uri, number of cookings*)
  38  | Abst of UriManager.uri                           (* uri *)
  39  | MutInd of UriManager.uri * int * int             (* uri, cookingsno, typeno*)
  40  | MutConstruct of UriManager.uri * int *           (* uri, cookingsno, *)
  41     int * int                                       (*  typeno, consno  *)
  42  (*CSC: serve cookingsno?*)
  43  | MutCase of UriManager.uri * int *                (* ind. uri, cookingsno, *)
  44     int *                                           (*  ind. typeno,         *)
  45     term * term *                                   (*  outtype, ind. term   *)
  46     term list                                       (*  patterns             *)
  47  | Fix of int * inductiveFun list                   (* funno, functions *)
  48  | CoFix of int * coInductiveFun list               (* funno, functions *)
  49 and obj =
  50    Definition of string * term * term *           (* id, value, type,         *)
  51     (int * UriManager.uri list) list              (*  parameters              *)
  52  | Axiom of string * term *
  53     (int * UriManager.uri list) list              (* id, type, parameters     *)
  54  | Variable of string * term                      (* name, type               *)
  55  | CurrentProof of string * (int * term) list *   (* name, conjectures,       *)
  56     term * term                                   (*  value, type             *)
  57  | InductiveDefinition of inductiveType list *    (* inductive types,         *)
  58     (int * UriManager.uri list) list * int        (*  parameters, n ind. pars *)
  59 and inductiveType =
  60  string * bool * term *                       (* typename, inductive, arity *)
  61   constructor list                            (*  constructors              *)
  62 and constructor =
  63  string * term * bool list option ref         (* id, type, really recursive *)
  64 and inductiveFun =
  65  string * int * term * term                   (* name, ind. index, type, body *)
  66 and coInductiveFun =
  67  string * term * term                         (* name, type, body *)
  68
  69 and annterm =
  70    ARel of id * annotation option ref *
  71     int * string option                             (* DeBrujin index, binder *)
  72  | AVar of id * annotation option ref *
  73     UriManager.uri                                  (* uri *)
  74  | AMeta of id * annotation option ref * int        (* numeric id *)
  75  | ASort of id * annotation option ref * sort       (* sort *)
  76  | AImplicit of id * annotation option ref          (* *)
  77  | ACast of id * annotation option ref *
  78     annterm * annterm                               (* value, type *)
  79  | AProd of id * annotation option ref *
  80     name * annterm * annterm                        (* binder, source, target *)
  81  | ALambda of id * annotation option ref *
  82     name * annterm * annterm                        (* binder, source, target *)
  83  | AAppl of id * annotation option ref *
  84     annterm list                                    (* arguments *)
  85  | AConst of id * annotation option ref *
  86     UriManager.uri * int                            (* uri, number of cookings*)
  87  | AAbst of id * annotation option ref *
  88     UriManager.uri                                  (* uri *)
  89  | AMutInd of id * annotation option ref *
  90     UriManager.uri * int * int                      (* uri, cookingsno, typeno*)
  91  | AMutConstruct of id * annotation option ref *
  92     UriManager.uri * int *                          (* uri, cookingsno, *)
  93     int * int                                       (*  typeno, consno  *)
  94  (*CSC: serve cookingsno?*)
  95  | AMutCase of id * annotation option ref *
  96     UriManager.uri * int *                          (* ind. uri, cookingsno  *)
  97     int *                                           (*  ind. typeno,         *)
  98     annterm * annterm *                             (*  outtype, ind. term   *)
  99     annterm list                                    (*  patterns             *)
 100  | AFix of id * annotation option ref *
 101     int * anninductiveFun list                      (* funno, functions *)
 102  | ACoFix of id * annotation option ref *
 103     int * anncoInductiveFun list                    (* funno, functions *)
 104 and annobj =
 105    ADefinition of id * annotation option ref *
 106     string *                                        (* id,           *)
 107     annterm * annterm *                             (*  value, type, *)
 108     (int * UriManager.uri list) list exactness      (*  parameters   *)
 109  | AAxiom of id * annotation option ref *
 110     string * annterm *                              (* id, type    *)
 111     (int * UriManager.uri list) list                (*  parameters *)
 112  | AVariable of id * annotation option ref *
 113     string * annterm                                (* name, type *)
 114  | ACurrentProof of id * annotation option ref *
 115     string * (int * annterm) list *                 (*  name, conjectures, *)
 116     annterm * annterm                               (*  value, type        *)
 117  | AInductiveDefinition of id *
 118     annotation option ref * anninductiveType list * (* inductive types ,      *)
 119     (int * UriManager.uri list) list * int          (*  parameters,n ind. pars*)
 120 and anninductiveType =
 121  string * bool * annterm *                    (* typename, inductive, arity *)
 122   annconstructor list                         (*  constructors              *)
 123 and annconstructor =
 124  string * annterm * bool list option ref      (* id, type, really recursive *)
 125 and anninductiveFun =
 126  string * int * annterm * annterm             (* name, ind. index, type, body *)
 127 and anncoInductiveFun =
 128  string * annterm * annterm                   (* name, type, body *)
 129 and annotation =
 130  string
 131 and 'a exactness =
 132    Possible of 'a                            (* an approximation to something *)
 133  | Actual of 'a                              (* something *)
 134 ;;