1 (* Copyright (C) 2000, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (*****************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
33 (* This module defines the internal representation of the objects (variables,*)
34 (* blocks of (co)inductive definitions and constants) and the terms of cic *)
36 (*****************************************************************************)
38 (* $Id: cic.ml 7190 2007-01-31 18:36:04Z sacerdot $ *)
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
45 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
60 | `Elim of sort (** elimination principle; if sort is Type, the universe is
62 | `Record of (string * bool * int) list (**
63 inductive type that encodes a record; the arguments are
64 the record fields names and if they are coercions and
65 then the coercion arity *)
66 | `Projection (** record projection *)
67 | `InversionPrinciple (** inversion principle *)
71 [ `Class of object_class
72 | `Flavour of object_flavour
79 | Type of CicUniv.universe
82 type implicit_annotation = [ `Closed | `Type | `Hole | `Term ]
84 type name = Name of string | Anonymous
86 type local_context = int * (term list) option (* shift, subst (None means id) *)
89 | Rel of int (* DeBruijn index, 1 based *)
90 | Meta of int * local_context
91 | Appl of term list (* arguments *)
92 | Prod of name * term * term (* binder, source, target *)
93 | Lambda of name * term * term (* binder, source, target *)
94 | LetIn of name * term * term * term (* binder, type, term, body *)
95 | Const of UriManager.uri (* uri contains indtypeno/constrno *)
96 | Sort of sort (* sort *)
97 | Implicit of implicit_annotation (* ... *)
98 | MutCase of UriManager.uri * (* ind. uri, *)
99 term * term * (* outtype, ind. term *)
100 term list (* patterns *)
102 Constant of string * term option * term * (* id, body, type, *)
103 UriManager.uri list * attribute list (* parameters *)
104 | Variable of string * term option * term * (* name, body, type *)
105 UriManager.uri list * attribute list (* parameters *)
106 | CurrentProof of string * metasenv * term * (* name, conjectures, body, *)
107 term * UriManager.uri list * attribute list (* type, parameters *)
108 | InductiveDefinition of inductiveType list * (* inductive types, *)
109 UriManager.uri list * int * attribute list (* params, left params no *)
111 string * bool * term * (* typename, inductive, arity *)
112 constructor list (* constructors *)
114 string * term (* id, type *)
116 string * int * term * term (* name, ind. index, type, body *)
118 string * term * term (* name, type, body *)
120 (* a metasenv is a list of declarations of metas in declarations *)
121 (* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
122 (* depend on new ones. *)
123 and conjecture = int * context * term
124 and metasenv = conjecture list
125 and substitution = (int * (context * term * term)) list
129 (* a metasenv is a list of declarations of metas in declarations *)
130 (* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
131 (* depend on new ones. *)
132 and annconjecture = id * int * anncontext * annterm
133 and annmetasenv = annconjecture list
136 ARel of id * id * int * (* idref, DeBrujin index, *)
138 | AVar of id * UriManager.uri * (* uri, *)
139 annterm explicit_named_substitution (* explicit named subst. *)
140 | AMeta of id * int * (annterm option) list (* numeric id, *)
142 | ASort of id * sort (* sort *)
143 | AImplicit of id * implicit_annotation option (* *)
144 | ACast of id * annterm * annterm (* value, type *)
145 | AProd of id * name * annterm * annterm (* binder, source, target *)
146 | ALambda of id * name * annterm * annterm (* binder, source, target *)
147 | ALetIn of id * name * annterm * annterm (* binder, term, target *)
148 | AAppl of id * annterm list (* arguments *)
149 | AConst of id * UriManager.uri * (* uri, *)
150 annterm explicit_named_substitution (* explicit named subst. *)
151 | AMutInd of id * UriManager.uri * int * (* uri, typeno *)
152 annterm explicit_named_substitution (* explicit named subst. *)
153 (* typeno is 0 based *)
154 | AMutConstruct of id * UriManager.uri * (* uri, *)
155 int * int * (* typeno, consno *)
156 annterm explicit_named_substitution (* explicit named subst. *)
157 (* typeno is 0 based *)
158 (* consno is 1 based *)
159 | AMutCase of id * UriManager.uri * (* ind. uri, *)
160 int * (* ind. typeno, *)
161 annterm * annterm * (* outtype, ind. term *)
162 annterm list (* patterns *)
163 | AFix of id * int * anninductiveFun list (* funno, functions *)
164 | ACoFix of id * int * anncoInductiveFun list (* funno, functions *)
166 AConstant of id * id option * string * (* name, *)
167 annterm option * annterm * (* body, type, *)
168 UriManager.uri list * attribute list (* parameters *)
170 string * annterm option * annterm * (* name, body, type *)
171 UriManager.uri list * attribute list (* parameters *)
172 | ACurrentProof of id * id *
173 string * annmetasenv * (* name, conjectures, *)
174 annterm * annterm * UriManager.uri list * (* body,type,parameters *)
176 | AInductiveDefinition of id *
177 anninductiveType list * (* inductive types , *)
178 UriManager.uri list * int * attribute list (* parameters,n ind. pars*)
179 and anninductiveType =
180 id * string * bool * annterm * (* typename, inductive, arity *)
181 annconstructor list (* constructors *)
183 string * annterm (* id, type *)
184 and anninductiveFun =
185 id * string * int * annterm * annterm (* name, ind. index, type, body *)
186 and anncoInductiveFun =
187 id * string * annterm * annterm (* name, type, body *)
191 and context_entry = (* A declaration or definition *)
193 | Def of term * term option (* body, type (if known) *)
196 (name * context_entry) option (* None means no more accessible *)
198 and context = hypothesis list
200 and anncontext_entry = (* A declaration or definition *)
205 id * (name * anncontext_entry) option (* None means no more accessible *)
207 and anncontext = annhypothesis list
211 context -> metasenv -> CicUniv.universe_graph ->
212 term * metasenv * CicUniv.universe_graph
215 Object of annobj (* if annobj is a Constant, this is its type *)
216 | ConstantBody of annobj
218 | Conjecture of annconjecture
219 | Hypothesis of annhypothesis
226 let hash = Hashtbl.hash_param 100 1000