]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic/cic.ml
added generation of LaTeX documentation
[helm.git] / helm / ocaml / 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 (* 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  | Conjecture of annconjecture
44  | Hypothesis of annhypothesis
45
46 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
47 and sort =
48    Prop
49  | Set
50  | Type
51 and name =
52    Name of string
53  | Anonimous
54 and term =
55    Rel of int                                       (* DeBrujin index *)
56  | Var of UriManager.uri                            (* uri *)
57  | Meta of int * (term option) list                 (* numeric id,    *)
58                                                     (*  local context *)
59  | Sort of sort                                     (* sort *)
60  | Implicit                                         (* *)
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                                                     (* typeno is 0 based *)
69  | MutConstruct of UriManager.uri * int *           (* uri, cookingsno, *)
70     int * int                                       (*  typeno, consno  *)
71                                                     (* consno is 1 based *)
72  (*CSC: serve cookingsno?*)
73  | MutCase of UriManager.uri * int *                (* ind. uri, cookingsno, *)
74     int *                                           (*  ind. typeno,         *)
75     term * term *                                   (*  outtype, ind. term   *)
76     term list                                       (*  patterns             *)
77  | Fix of int * inductiveFun list                   (* funno, functions *)
78  | CoFix of int * coInductiveFun list               (* funno, functions *)
79 and obj =
80    Definition of string * term * term *           (* id, value, type,         *)
81     (int * UriManager.uri list) list              (*  parameters              *)
82  | Axiom of string * term *
83     (int * UriManager.uri list) list              (* id, type, parameters     *)
84  | Variable of string * term option * term        (* name, body, type         *)
85  | CurrentProof of string * metasenv *            (* name, conjectures,       *)
86     term * term                                   (*  value, type             *)
87  | InductiveDefinition of inductiveType list *    (* inductive types,         *)
88     (int * UriManager.uri list) list * int        (*  parameters, n ind. pars *)
89 and inductiveType = 
90  string * bool * term *                       (* typename, inductive, arity *)
91   constructor list                            (*  constructors              *)
92 and constructor =
93  string * term * bool list option ref         (* id, type, really recursive *)
94 and inductiveFun =
95  string * int * term * term                   (* name, ind. index, type, body *)
96 and coInductiveFun =
97  string * term * term                         (* name, type, body *)
98
99 (* a metasenv is a list of declarations of metas *)
100 and conjecture = int * context * term
101 and metasenv = conjecture list
102
103 (* a metasenv is a list of declarations of metas *)
104 and annconjecture = id * int * anncontext * annterm
105 and annmetasenv = annconjecture list
106
107 and annterm =
108    ARel of id * int * string                        (* DeBrujin index, binder *)
109  | AVar of id * UriManager.uri                      (* uri *)
110  | AMeta of id * int * (annterm option) list        (* numeric id,    *)
111                                                     (*  local context *)
112  | ASort of id * sort                               (* sort *)
113  | AImplicit of id                                  (* *)
114  | ACast of id * annterm * annterm                  (* value, type *)
115  | AProd of id * name * annterm * annterm           (* binder, source, target *)
116  | ALambda of id * name * annterm * annterm         (* binder, source, target *)
117  | ALetIn of id * name * annterm * annterm          (* binder, term, target *)
118  | AAppl of id * annterm list                       (* arguments *)
119  | AConst of id * UriManager.uri * int              (* uri, number of cookings*)
120  | AMutInd of id * UriManager.uri * int * int       (* uri, cookingsno, typeno*)
121                                                     (* typeno is 0 based *)
122  | AMutConstruct of id * UriManager.uri * int *     (* uri, cookingsno, *)
123     int * int                                       (*  typeno, consno  *)
124                                                     (* consno is 1 based *)
125  (*CSC: serve cookingsno?*)
126  | AMutCase of id * UriManager.uri * int *          (* ind. uri, cookingsno  *)
127     int *                                           (*  ind. typeno,         *)
128     annterm * annterm *                             (*  outtype, ind. term   *)
129     annterm list                                    (*  patterns             *)
130  | AFix of id * int * anninductiveFun list          (* funno, functions *)
131  | ACoFix of id * int * anncoInductiveFun list      (* funno, functions *)
132 and annobj =
133    ADefinition of id * string *                     (* id,           *)
134     annterm * annterm *                             (*  value, type, *)
135     (int * UriManager.uri list) list exactness      (*  parameters   *)
136  | AAxiom of id * string * annterm *                (* id, type    *)
137     (int * UriManager.uri list) list                (*  parameters *)
138  | AVariable of id *
139     string * annterm option * annterm               (* name, body, type *)
140  | ACurrentProof of id *
141     string * annmetasenv *                          (*  name, conjectures, *)
142     annterm * annterm                               (*  value, type        *)
143  | AInductiveDefinition of id *
144     anninductiveType list *                         (* inductive types ,      *)
145     (int * UriManager.uri list) list * int          (*  parameters,n ind. pars*)
146 and anninductiveType = 
147  string * bool * annterm *                    (* typename, inductive, arity *)
148   annconstructor list                         (*  constructors              *)
149 and annconstructor =
150  string * annterm * bool list option ref      (* id, type, really recursive *)
151 and anninductiveFun =
152  string * int * annterm * annterm             (* name, ind. index, type, body *)
153 and anncoInductiveFun =
154  string * annterm * annterm                   (* name, type, body *)
155 and annotation =
156  string
157 and 'a exactness =
158    Possible of 'a                            (* an approximation to something *)
159  | Actual of 'a                              (* something *)
160
161 and context_entry =                            (* A declaration or definition *)
162    Decl of term
163  | Def of term
164
165 and hypothesis =
166  (name * context_entry) option               (* None means no more accessible *)
167
168 and context = hypothesis list
169
170 and anncontext_entry =                         (* A declaration or definition *)
171    ADecl of annterm
172  | ADef of annterm
173
174 and annhypothesis =
175  id * (name * anncontext_entry) option       (* None means no more accessible *)
176
177 and anncontext = annhypothesis list;;