helm/interface/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 (*                                 14/06/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 anntarget =
  41    Object of annobj
  42  | Term of annterm
  43
  44 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
  45 and sort =
  46    Prop
  47  | Set
  48  | Type
  49 and name =
  50    Name of string
  51  | Anonimous
  52 and term =
  53    Rel of int                                       (* DeBrujin index *)
  54  | Var of UriManager.uri                            (* uri *)
  55  | Meta of int                                      (* numeric id *)
  56  | Sort of sort                                     (* sort *)
  57  | Implicit                                         (* *)
  58  | Cast of term * term                              (* value, type *)
  59  | Prod of name * term * term                       (* binder, source, target *)
  60  | Lambda of name * term * term                     (* binder, source, target *)
  61  | LetIn of name * term * term                      (* binder, term, target *)
  62  | Appl of term list                                (* arguments *)
  63  | Const of UriManager.uri * int                    (* uri, number of cookings*)
  64  | Abst of UriManager.uri                           (* uri *)
  65  | MutInd of UriManager.uri * int * int             (* uri, cookingsno, typeno*)
  66  | MutConstruct of UriManager.uri * int *           (* uri, cookingsno, *)
  67     int * int                                       (*  typeno, consno  *)
  68  (*CSC: serve cookingsno?*)
  69  | MutCase of UriManager.uri * int *                (* ind. uri, cookingsno, *)
  70     int *                                           (*  ind. typeno,         *)
  71     term * term *                                   (*  outtype, ind. term   *)
  72     term list                                       (*  patterns             *)
  73  | Fix of int * inductiveFun list                   (* funno, functions *)
  74  | CoFix of int * coInductiveFun list               (* funno, functions *)
  75 and obj =
  76    Definition of string * term * term *           (* id, value, type,         *)
  77     (int * UriManager.uri list) list              (*  parameters              *)
  78  | Axiom of string * term *
  79     (int * UriManager.uri list) list              (* id, type, parameters     *)
  80  | Variable of string * term option * term        (* name, body, type         *)
  81  | CurrentProof of string * (int * term) list *   (* name, conjectures,       *)
  82     term * term                                   (*  value, type             *)
  83  | InductiveDefinition of inductiveType list *    (* inductive types,         *)
  84     (int * UriManager.uri list) list * int        (*  parameters, n ind. pars *)
  85 and inductiveType =
  86  string * bool * term *                       (* typename, inductive, arity *)
  87   constructor list                            (*  constructors              *)
  88 and constructor =
  89  string * term * bool list option ref         (* id, type, really recursive *)
  90 and inductiveFun =
  91  string * int * term * term                   (* name, ind. index, type, body *)
  92 and coInductiveFun =
  93  string * term * term                         (* name, type, body *)
  94
  95 and annterm =
  96    ARel of id * annotation option ref *
  97     int * string option                             (* DeBrujin index, binder *)
  98  | AVar of id * annotation option ref *
  99     UriManager.uri                                  (* uri *)
 100  | AMeta of id * annotation option ref * int        (* numeric id *)
 101  | ASort of id * annotation option ref * sort       (* sort *)
 102  | AImplicit of id * annotation option ref          (* *)
 103  | ACast of id * annotation option ref *
 104     annterm * annterm                               (* value, type *)
 105  | AProd of id * annotation option ref *
 106     name * annterm * annterm                        (* binder, source, target *)
 107  | ALambda of id * annotation option ref *
 108     name * annterm * annterm                        (* binder, source, target *)
 109  | ALetIn of id * annotation option ref *
 110     name * annterm * annterm                        (* binder, term, target *)
 111  | AAppl of id * annotation option ref *
 112     annterm list                                    (* arguments *)
 113  | AConst of id * annotation option ref *
 114     UriManager.uri * int                            (* uri, number of cookings*)
 115  | AAbst of id * annotation option ref *
 116     UriManager.uri                                  (* uri *)
 117  | AMutInd of id * annotation option ref *
 118     UriManager.uri * int * int                      (* uri, cookingsno, typeno*)
 119  | AMutConstruct of id * annotation option ref *
 120     UriManager.uri * int *                          (* uri, cookingsno, *)
 121     int * int                                       (*  typeno, consno  *)
 122  (*CSC: serve cookingsno?*)
 123  | AMutCase of id * annotation option ref *
 124     UriManager.uri * int *                          (* ind. uri, cookingsno  *)
 125     int *                                           (*  ind. typeno,         *)
 126     annterm * annterm *                             (*  outtype, ind. term   *)
 127     annterm list                                    (*  patterns             *)
 128  | AFix of id * annotation option ref *
 129     int * anninductiveFun list                      (* funno, functions *)
 130  | ACoFix of id * annotation option ref *
 131     int * anncoInductiveFun list                    (* funno, functions *)
 132 and annobj =
 133    ADefinition of id * annotation option ref *
 134     string *                                        (* id,           *)
 135     annterm * annterm *                             (*  value, type, *)
 136     (int * UriManager.uri list) list exactness      (*  parameters   *)
 137  | AAxiom of id * annotation option ref *
 138     string * annterm *                              (* id, type    *)
 139     (int * UriManager.uri list) list                (*  parameters *)
 140  | AVariable of id * annotation option ref *
 141     string * annterm option * annterm               (* name, body, type *)
 142  | ACurrentProof of id * annotation option ref *
 143     string * (int * annterm) list *                 (*  name, conjectures, *)
 144     annterm * annterm                               (*  value, type        *)
 145  | AInductiveDefinition of id *
 146     annotation option ref * anninductiveType list * (* inductive types ,      *)
 147     (int * UriManager.uri list) list * int          (*  parameters,n ind. pars*)
 148 and anninductiveType =
 149  string * bool * annterm *                    (* typename, inductive, arity *)
 150   annconstructor list                         (*  constructors              *)
 151 and annconstructor =
 152  string * annterm * bool list option ref      (* id, type, really recursive *)
 153 and anninductiveFun =
 154  string * int * annterm * annterm             (* name, ind. index, type, body *)
 155 and anncoInductiveFun =
 156  string * annterm * annterm                   (* name, type, body *)
 157 and annotation =
 158  string
 159 and 'a exactness =
 160    Possible of 'a                            (* an approximation to something *)
 161  | Actual of 'a                              (* something *)
 162 ;;