helm/ocaml/cic/cic.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 29/11/2000                                 *)
  32 (*                                                                            *)
  33 (* This module defines the internal representation of the objects (variables, *)
  34 (* blocks of (co)inductive definitions and constants) and the terms of cic    *)
  35 (*                                                                            *)
  36 (******************************************************************************)
  37
  38 (* STUFF TO MANAGE IDENTIFIERS *)
  39 type id = string  (* the abstract type of the (annotated) node identifiers *)
  40 type 'term explicit_named_substitution = (UriManager.uri * 'term) list
  41
  42 type anntarget =
  43    Object of annobj         (* if annobj is a Constant, this is its type *)
  44  | ConstantBody of annobj
  45  | Term of annterm
  46  | Conjecture of annconjecture
  47  | Hypothesis of annhypothesis
  48
  49 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
  50 and sort =
  51    Prop
  52  | Set
  53  | Type
  54 and name =
  55    Name of string
  56  | Anonymous
  57 and term =
  58    Rel of int                                       (* DeBrujin index *)
  59  | Var of UriManager.uri *                          (* uri,                   *)
  60      term explicit_named_substitution               (*  explicit named subst. *)
  61  | Meta of int * (term option) list                 (* numeric id,    *)
  62                                                     (*  local context *)
  63  | Sort of sort                                     (* sort *)
  64  | Implicit                                         (* *)
  65  | Cast of term * term                              (* value, type *)
  66  | Prod of name * term * term                       (* binder, source, target *)
  67  | Lambda of name * term * term                     (* binder, source, target *)
  68  | LetIn of name * term * term                      (* binder, term, target *)
  69  | Appl of term list                                (* arguments *)
  70  | Const of UriManager.uri *                        (* uri,                   *)
  71      term explicit_named_substitution               (*  explicit named subst. *)
  72  | MutInd of UriManager.uri * int *                 (* uri, typeno, *)
  73      term explicit_named_substitution               (*  explicit named subst. *)
  74                                                     (* typeno is 0 based      *)
  75  | MutConstruct of UriManager.uri *                 (* uri,                   *)
  76     int * int *                                     (*  typeno, consno        *)
  77      term explicit_named_substitution               (*  explicit named subst. *)
  78                                                     (* typeno is 0 based      *)
  79                                                     (* consno is 1 based      *)
  80  | MutCase of UriManager.uri *                      (* ind. uri,             *)
  81     int *                                           (*  ind. typeno,         *)
  82     term * term *                                   (*  outtype, ind. term   *)
  83     term list                                       (*  patterns             *)
  84  | Fix of int * inductiveFun list                   (* funno, functions *)
  85  | CoFix of int * coInductiveFun list               (* funno, functions *)
  86 and obj =
  87    Constant of string * term option * term *      (* id, body, type,          *)
  88     UriManager.uri list                           (*  parameters              *)
  89  | Variable of string * term option * term *      (* name, body, type         *)
  90     UriManager.uri list                           (* parameters               *)
  91  | CurrentProof of string * metasenv *            (* name, conjectures,       *)
  92     term * term * UriManager.uri list             (*  value, type, parameters *)
  93  | InductiveDefinition of inductiveType list *    (* inductive types,         *)
  94     UriManager.uri list * int                     (*  parameters, n ind. pars *)
  95 and inductiveType =
  96  string * bool * term *                       (* typename, inductive, arity *)
  97   constructor list                            (*  constructors              *)
  98 and constructor =
  99  string * term                                (* id, type *)
 100 and inductiveFun =
 101  string * int * term * term                   (* name, ind. index, type, body *)
 102 and coInductiveFun =
 103  string * term * term                         (* name, type, body *)
 104
 105 (* a metasenv is a list of declarations of metas *)
 106 and conjecture = int * context * term
 107 and metasenv = conjecture list
 108
 109 (* a metasenv is a list of declarations of metas *)
 110 and annconjecture = id * int * anncontext * annterm
 111 and annmetasenv = annconjecture list
 112
 113 and annterm =
 114    ARel of id * id * int *                          (* idref, DeBrujin index, *)
 115     string                                          (*  binder                *)
 116  | AVar of id * UriManager.uri *                    (* uri,                   *)
 117     annterm explicit_named_substitution             (*  explicit named subst. *)
 118  | AMeta of id * int * (annterm option) list        (* numeric id,    *)
 119                                                     (*  local context *)
 120  | ASort of id * sort                               (* sort *)
 121  | AImplicit of id                                  (* *)
 122  | ACast of id * annterm * annterm                  (* value, type *)
 123  | AProd of id * name * annterm * annterm           (* binder, source, target *)
 124  | ALambda of id * name * annterm * annterm         (* binder, source, target *)
 125  | ALetIn of id * name * annterm * annterm          (* binder, term, target *)
 126  | AAppl of id * annterm list                       (* arguments *)
 127  | AConst of id * UriManager.uri *                  (* uri,                   *)
 128     annterm explicit_named_substitution             (*  explicit named subst. *)
 129  | AMutInd of id * UriManager.uri * int *           (* uri, typeno            *)
 130     annterm explicit_named_substitution             (*  explicit named subst. *)
 131                                                     (* typeno is 0 based *)
 132  | AMutConstruct of id * UriManager.uri *           (* uri,                   *)
 133     int * int *                                     (*  typeno, consno        *)
 134     annterm explicit_named_substitution             (*  explicit named subst. *)
 135                                                     (* typeno is 0 based *)
 136                                                     (* consno is 1 based *)
 137  | AMutCase of id * UriManager.uri *                (* ind. uri,             *)
 138     int *                                           (*  ind. typeno,         *)
 139     annterm * annterm *                             (*  outtype, ind. term   *)
 140     annterm list                                    (*  patterns             *)
 141  | AFix of id * int * anninductiveFun list          (* funno, functions *)
 142  | ACoFix of id * int * anncoInductiveFun list      (* funno, functions *)
 143 and annobj =
 144    AConstant of id * id option * string *           (* name,         *)
 145     annterm option * annterm *                      (*  body, type,  *)
 146     UriManager.uri list                             (*  parameters   *)
 147  | AVariable of id *
 148     string * annterm option * annterm *             (* name, body, type *)
 149     UriManager.uri list                             (*  parameters      *)
 150  | ACurrentProof of id * id *
 151     string * annmetasenv *                          (*  name, conjectures,    *)
 152     annterm * annterm * UriManager.uri list         (*  value,type,parameters *)
 153  | AInductiveDefinition of id *
 154     anninductiveType list *                         (* inductive types ,      *)
 155     UriManager.uri list * int                       (*  parameters,n ind. pars*)
 156 and anninductiveType =
 157  string * bool * annterm *                    (* typename, inductive, arity *)
 158   annconstructor list                         (*  constructors              *)
 159 and annconstructor =
 160  string * annterm                             (* id, type *)
 161 and anninductiveFun =
 162  id * string * int * annterm * annterm        (* name, ind. index, type, body *)
 163 and anncoInductiveFun =
 164  id * string * annterm * annterm              (* name, type, body *)
 165 and annotation =
 166  string
 167
 168 and context_entry =                            (* A declaration or definition *)
 169    Decl of term
 170  | Def of term
 171
 172 and hypothesis =
 173  (name * context_entry) option               (* None means no more accessible *)
 174
 175 and context = hypothesis list
 176
 177 and anncontext_entry =                         (* A declaration or definition *)
 178    ADecl of annterm
 179  | ADef of annterm
 180
 181 and annhypothesis =
 182  id * (name * anncontext_entry) option       (* None means no more accessible *)
 183
 184 and anncontext = annhypothesis list;;