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