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 *)
40 type 'term explicit_named_substitution = (UriManager.uri * 'term) list
43 Object of annobj (* if annobj is a Constant, this is its type *)
44 | ConstantBody of annobj
46 | Conjecture of annconjecture
47 | Hypothesis of annhypothesis
49 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
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, *)
63 | Sort of sort (* sort *)
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 *)
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 *)
96 string * bool * term * (* typename, inductive, arity *)
97 constructor list (* constructors *)
99 string * term (* id, type *)
101 string * int * term * term (* name, ind. index, type, body *)
103 string * term * term (* name, type, body *)
105 (* a metasenv is a list of declarations of metas in declarations *)
106 (* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
107 (* depend on new ones. *)
108 and conjecture = int * context * term
109 and metasenv = conjecture list
111 (* a metasenv is a list of declarations of metas in declarations *)
112 (* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
113 (* depend on new ones. *)
114 and annconjecture = id * int * anncontext * annterm
115 and annmetasenv = annconjecture list
118 ARel of id * id * int * (* idref, DeBrujin index, *)
120 | AVar of id * UriManager.uri * (* uri, *)
121 annterm explicit_named_substitution (* explicit named subst. *)
122 | AMeta of id * int * (annterm option) list (* numeric id, *)
124 | ASort of id * sort (* sort *)
125 | AImplicit of id (* *)
126 | ACast of id * annterm * annterm (* value, type *)
127 | AProd of id * name * annterm * annterm (* binder, source, target *)
128 | ALambda of id * name * annterm * annterm (* binder, source, target *)
129 | ALetIn of id * name * annterm * annterm (* binder, term, target *)
130 | AAppl of id * annterm list (* arguments *)
131 | AConst of id * UriManager.uri * (* uri, *)
132 annterm explicit_named_substitution (* explicit named subst. *)
133 | AMutInd of id * UriManager.uri * int * (* uri, typeno *)
134 annterm explicit_named_substitution (* explicit named subst. *)
135 (* typeno is 0 based *)
136 | AMutConstruct of id * UriManager.uri * (* uri, *)
137 int * int * (* typeno, consno *)
138 annterm explicit_named_substitution (* explicit named subst. *)
139 (* typeno is 0 based *)
140 (* consno is 1 based *)
141 | AMutCase of id * UriManager.uri * (* ind. uri, *)
142 int * (* ind. typeno, *)
143 annterm * annterm * (* outtype, ind. term *)
144 annterm list (* patterns *)
145 | AFix of id * int * anninductiveFun list (* funno, functions *)
146 | ACoFix of id * int * anncoInductiveFun list (* funno, functions *)
148 AConstant of id * id option * string * (* name, *)
149 annterm option * annterm * (* body, type, *)
150 UriManager.uri list (* parameters *)
152 string * annterm option * annterm * (* name, body, type *)
153 UriManager.uri list (* parameters *)
154 | ACurrentProof of id * id *
155 string * annmetasenv * (* name, conjectures, *)
156 annterm * annterm * UriManager.uri list (* value,type,parameters *)
157 | AInductiveDefinition of id *
158 anninductiveType list * (* inductive types , *)
159 UriManager.uri list * int (* parameters,n ind. pars*)
160 and anninductiveType =
161 id * string * bool * annterm * (* typename, inductive, arity *)
162 annconstructor list (* constructors *)
164 string * annterm (* id, type *)
165 and anninductiveFun =
166 id * string * int * annterm * annterm (* name, ind. index, type, body *)
167 and anncoInductiveFun =
168 id * string * annterm * annterm (* name, type, body *)
172 and context_entry = (* A declaration or definition *)
174 | Def of term * term option (* body, type (if known) *)
177 (name * context_entry) option (* None means no more accessible *)
179 and context = hypothesis list
181 and anncontext_entry = (* A declaration or definition *)
186 id * (name * anncontext_entry) option (* None means no more accessible *)
188 and anncontext = annhypothesis list