components/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 (* $Id$ *)
  39
  40 (* STUFF TO MANAGE IDENTIFIERS *)
  41 type id = string  (* the abstract type of the (annotated) node identifiers *)
  42 type 'term explicit_named_substitution = (UriManager.uri * 'term) list
  43
  44 type implicit_annotation = [ `Closed | `Type | `Hole ]
  45
  46 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
  47
  48 type sort =
  49    Prop
  50  | Set
  51  | Type of CicUniv.universe
  52  | CProp
  53
  54 type name =
  55  | Name of string
  56  | Anonymous
  57
  58 type object_flavour =
  59   [ `Definition
  60   | `MutualDefinition
  61   | `Fact
  62   | `Lemma
  63   | `Remark
  64   | `Theorem
  65   | `Variant
  66   | `Axiom
  67   ]
  68
  69 type object_class =
  70   [ `Coercion of int
  71   | `Elim of sort   (** elimination principle; if sort is Type, the universe is
  72                       * not relevant *)
  73   | `Record of (string * bool * int) list (**
  74                         inductive type that encodes a record; the arguments are
  75                         the record fields names and if they are coercions and
  76                         then the coercion arity *)
  77   | `Projection     (** record projection *)
  78   | `InversionPrinciple (** inversion principle *)
  79   ]
  80
  81 type attribute =
  82   [ `Class of object_class
  83   | `Flavour of object_flavour
  84   | `Generated
  85   ]
  86
  87 type term =
  88    Rel of int                                       (* DeBrujin index, 1 based*)
  89  | Var of UriManager.uri *                          (* uri,                   *)
  90      term explicit_named_substitution               (*  explicit named subst. *)
  91  | Meta of int * (term option) list                 (* numeric id,    *)
  92                                                     (*  local context *)
  93  | Sort of sort                                     (* sort *)
  94  | Implicit of implicit_annotation option           (* *)
  95  | Cast of term * term                              (* value, type *)
  96  | Prod of name * term * term                       (* binder, source, target *)
  97  | Lambda of name * term * term                     (* binder, source, target *)
  98  | LetIn of name * term * term * term               (* binder, term, type, target *)
  99  | Appl of term list                                (* arguments *)
 100  | Const of UriManager.uri *                        (* uri,                   *)
 101      term explicit_named_substitution               (*  explicit named subst. *)
 102  | MutInd of UriManager.uri * int *                 (* uri, typeno, *)
 103      term explicit_named_substitution               (*  explicit named subst. *)
 104                                                     (* typeno is 0 based      *)
 105  | MutConstruct of UriManager.uri *                 (* uri,                   *)
 106     int * int *                                     (*  typeno, consno        *)
 107      term explicit_named_substitution               (*  explicit named subst. *)
 108                                                     (* typeno is 0 based      *)
 109                                                     (* consno is 1 based      *)
 110  | MutCase of UriManager.uri *                      (* ind. uri,             *)
 111     int *                                           (*  ind. typeno,         *)
 112     term * term *                                   (*  outtype, ind. term   *)
 113     term list                                       (*  patterns             *)
 114  | Fix of int * inductiveFun list                   (* funno (0 based), funs *)
 115  | CoFix of int * coInductiveFun list               (* funno (0 based), funs *)
 116 and obj =
 117    Constant of string * term option * term *      (* id, body, type,          *)
 118     UriManager.uri list * attribute list          (*  parameters              *)
 119  | Variable of string * term option * term *      (* name, body, type         *)
 120     UriManager.uri list * attribute list          (* parameters               *)
 121  | CurrentProof of string * metasenv * term *     (* name, conjectures, body, *)
 122     term * UriManager.uri list * attribute list   (*  type, parameters        *)
 123  | InductiveDefinition of inductiveType list *    (* inductive types,         *)
 124     UriManager.uri list * int * attribute list    (*  params, left params no  *)
 125 and inductiveType =
 126  string * bool * term *                       (* typename, inductive, arity *)
 127   constructor list                            (*  constructors              *)
 128 and constructor =
 129  string * term                                (* id, type *)
 130 and inductiveFun =
 131  string * int * term * term                   (* name, ind. index, type, body *)
 132 and coInductiveFun =
 133  string * term * term                         (* name, type, body *)
 134
 135 (* a metasenv is a list of declarations of metas in declarations *)
 136 (* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
 137 (* depend on new ones.                                           *)
 138 and conjecture = int * context * term
 139 and metasenv = conjecture list
 140 and substitution = (int * (context * term * term)) list
 141
 142
 143
 144 (* a metasenv is a list of declarations of metas in declarations *)
 145 (* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
 146 (* depend on new ones.                                           *)
 147 and annconjecture = id * int * anncontext * annterm
 148 and annmetasenv = annconjecture list
 149
 150 and annterm =
 151    ARel of id * id * int *                          (* idref, DeBrujin index, *)
 152     string                                          (*  binder                *)
 153  | AVar of id * UriManager.uri *                    (* uri,                   *)
 154     annterm explicit_named_substitution             (*  explicit named subst. *)
 155  | AMeta of id * int * (annterm option) list        (* numeric id,    *)
 156                                                     (*  local context *)
 157  | ASort of id * sort                               (* sort *)
 158  | AImplicit of id * implicit_annotation option     (* *)
 159  | ACast of id * annterm * annterm                  (* value, type *)
 160  | AProd of id * name * annterm * annterm           (* binder, source, target *)
 161  | ALambda of id * name * annterm * annterm         (* binder, source, target *)
 162  | ALetIn of id * name * annterm * annterm *  annterm (* binder, term, type, target *)
 163  | AAppl of id * annterm list                       (* arguments *)
 164  | AConst of id * UriManager.uri *                  (* uri,                   *)
 165     annterm explicit_named_substitution             (*  explicit named subst. *)
 166  | AMutInd of id * UriManager.uri * int *           (* uri, typeno            *)
 167     annterm explicit_named_substitution             (*  explicit named subst. *)
 168                                                     (* typeno is 0 based *)
 169  | AMutConstruct of id * UriManager.uri *           (* uri,                   *)
 170     int * int *                                     (*  typeno, consno        *)
 171     annterm explicit_named_substitution             (*  explicit named subst. *)
 172                                                     (* typeno is 0 based *)
 173                                                     (* consno is 1 based *)
 174  | AMutCase of id * UriManager.uri *                (* ind. uri,             *)
 175     int *                                           (*  ind. typeno,         *)
 176     annterm * annterm *                             (*  outtype, ind. term   *)
 177     annterm list                                    (*  patterns             *)
 178  | AFix of id * int * anninductiveFun list          (* funno, functions *)
 179  | ACoFix of id * int * anncoInductiveFun list      (* funno, functions *)
 180 and annobj =
 181    AConstant of id * id option * string *           (* name,         *)
 182     annterm option * annterm *                      (*  body, type,  *)
 183     UriManager.uri list * attribute list            (*  parameters   *)
 184  | AVariable of id *
 185     string * annterm option * annterm *             (* name, body, type *)
 186     UriManager.uri list * attribute list            (*  parameters      *)
 187  | ACurrentProof of id * id *
 188     string * annmetasenv *                          (*  name, conjectures,    *)
 189     annterm * annterm * UriManager.uri list *       (*  body,type,parameters  *)
 190     attribute list
 191  | AInductiveDefinition of id *
 192     anninductiveType list *                         (* inductive types ,      *)
 193     UriManager.uri list * int * attribute list      (*  parameters,n ind. pars*)
 194 and anninductiveType =
 195  id * string * bool * annterm *               (* typename, inductive, arity *)
 196   annconstructor list                         (*  constructors              *)
 197 and annconstructor =
 198  string * annterm                             (* id, type *)
 199 and anninductiveFun =
 200  id * string * int * annterm * annterm        (* name, ind. index, type, body *)
 201 and anncoInductiveFun =
 202  id * string * annterm * annterm              (* name, type, body *)
 203 and annotation =
 204  string
 205
 206 and context_entry =                            (* A declaration or definition *)
 207    Decl of term
 208  | Def of term * term                          (* body, type *)
 209
 210 and hypothesis =
 211  (name * context_entry) option               (* None means no more accessible *)
 212
 213 and context = hypothesis list
 214
 215 and anncontext_entry =                         (* A declaration or definition *)
 216    ADecl of annterm
 217  | ADef of annterm * annterm
 218
 219 and annhypothesis =
 220  id * (name * anncontext_entry) option       (* None means no more accessible *)
 221
 222 and anncontext = annhypothesis list
 223 ;;
 224
 225 type lazy_term =
 226  context -> metasenv -> CicUniv.universe_graph ->
 227   term * metasenv * CicUniv.universe_graph
 228
 229 type anntarget =
 230    Object of annobj         (* if annobj is a Constant, this is its type *)
 231  | ConstantBody of annobj
 232  | Term of annterm
 233  | Conjecture of annconjecture
 234  | Hypothesis of annhypothesis
 235
 236 module CicHash =
 237  Hashtbl.Make
 238   (struct
 239     type t = term
 240     let equal = (==)
 241     let hash = Hashtbl.hash_param 100 1000
 242    end)
 243 ;;
 244