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 (* STUFF TO MANAGE IDENTIFIERS *)
39 type id = string (* the abstract type of the (annotated) node identifiers *)
43 | Conjecture of annconjecture
44 | Hypothesis of annhypothesis
46 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
55 Rel of int (* DeBrujin index *)
56 | Var of UriManager.uri (* uri *)
57 | Meta of int * (term option) list (* numeric id, *)
59 | Sort of sort (* sort *)
61 | Cast of term * term (* value, type *)
62 | Prod of name * term * term (* binder, source, target *)
63 | Lambda of name * term * term (* binder, source, target *)
64 | LetIn of name * term * term (* binder, term, target *)
65 | Appl of term list (* arguments *)
66 | Const of UriManager.uri * int (* uri, number of cookings*)
67 | MutInd of UriManager.uri * int * int (* uri, cookingsno, typeno*)
68 | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *)
69 int * int (* typeno, consno *)
70 (*CSC: serve cookingsno?*)
71 | MutCase of UriManager.uri * int * (* ind. uri, cookingsno, *)
72 int * (* ind. typeno, *)
73 term * term * (* outtype, ind. term *)
74 term list (* patterns *)
75 | Fix of int * inductiveFun list (* funno, functions *)
76 | CoFix of int * coInductiveFun list (* funno, functions *)
78 Definition of string * term * term * (* id, value, type, *)
79 (int * UriManager.uri list) list (* parameters *)
80 | Axiom of string * term *
81 (int * UriManager.uri list) list (* id, type, parameters *)
82 | Variable of string * term option * term (* name, body, type *)
83 | CurrentProof of string * metasenv * (* name, conjectures, *)
84 term * term (* value, type *)
85 | InductiveDefinition of inductiveType list * (* inductive types, *)
86 (int * UriManager.uri list) list * int (* parameters, n ind. pars *)
88 string * bool * term * (* typename, inductive, arity *)
89 constructor list (* constructors *)
91 string * term * bool list option ref (* id, type, really recursive *)
93 string * int * term * term (* name, ind. index, type, body *)
95 string * term * term (* name, type, body *)
97 (* a metasenv is a list of declarations of metas *)
98 and conjecture = int * context * term
99 and metasenv = conjecture list
101 (* a metasenv is a list of declarations of metas *)
102 and annconjecture = id * int * anncontext * annterm
103 and annmetasenv = annconjecture list
106 ARel of id * int * string (* DeBrujin index, binder *)
107 | AVar of id * UriManager.uri (* uri *)
108 | AMeta of id * int * (annterm option) list (* numeric id, *)
110 | ASort of id * sort (* sort *)
111 | AImplicit of id (* *)
112 | ACast of id * annterm * annterm (* value, type *)
113 | AProd of id * name * annterm * annterm (* binder, source, target *)
114 | ALambda of id * name * annterm * annterm (* binder, source, target *)
115 | ALetIn of id * name * annterm * annterm (* binder, term, target *)
116 | AAppl of id * annterm list (* arguments *)
117 | AConst of id * UriManager.uri * int (* uri, number of cookings*)
118 | AMutInd of id * UriManager.uri * int * int (* uri, cookingsno, typeno*)
119 | AMutConstruct of id * UriManager.uri * int * (* uri, cookingsno, *)
120 int * int (* typeno, consno *)
121 (*CSC: serve cookingsno?*)
122 | AMutCase of id * UriManager.uri * int * (* ind. uri, cookingsno *)
123 int * (* ind. typeno, *)
124 annterm * annterm * (* outtype, ind. term *)
125 annterm list (* patterns *)
126 | AFix of id * int * anninductiveFun list (* funno, functions *)
127 | ACoFix of id * int * anncoInductiveFun list (* funno, functions *)
129 ADefinition of id * string * (* id, *)
130 annterm * annterm * (* value, type, *)
131 (int * UriManager.uri list) list exactness (* parameters *)
132 | AAxiom of id * string * annterm * (* id, type *)
133 (int * UriManager.uri list) list (* parameters *)
135 string * annterm option * annterm (* name, body, type *)
136 | ACurrentProof of id *
137 string * annmetasenv * (* name, conjectures, *)
138 annterm * annterm (* value, type *)
139 | AInductiveDefinition of id *
140 anninductiveType list * (* inductive types , *)
141 (int * UriManager.uri list) list * int (* parameters,n ind. pars*)
142 and anninductiveType =
143 string * bool * annterm * (* typename, inductive, arity *)
144 annconstructor list (* constructors *)
146 string * annterm * bool list option ref (* id, type, really recursive *)
147 and anninductiveFun =
148 string * int * annterm * annterm (* name, ind. index, type, body *)
149 and anncoInductiveFun =
150 string * annterm * annterm (* name, type, body *)
154 Possible of 'a (* an approximation to something *)
155 | Actual of 'a (* something *)
157 and context_entry = (* A declaration or definition *)
162 (name * context_entry) option (* None means no more accessible *)
164 and context = hypothesis list
166 and anncontext_entry = (* A declaration or definition *)
171 id * (name * anncontext_entry) option (* None means no more accessible *)
173 and anncontext = annhypothesis list;;