]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic/cic.ml
added testlibrary.opt and some cm****
[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 'term explicit_named_substitution = (UriManager.uri * 'term) list
41
42 type anntarget =
43    Object of annobj         (* if annobj is a Constant, this is its type *)
44  | ConstantBody of annobj
45  | Term of annterm
46  | Conjecture of annconjecture
47  | Hypothesis of annhypothesis
48
49 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
50 and sort =
51    Prop
52  | Set
53  | Type
54  | CProp
55 and name =
56    Name of string
57  | Anonymous
58 and term =
59    Rel of int                                       (* DeBrujin index *)
60  | Var of UriManager.uri *                          (* uri,                   *)
61      term explicit_named_substitution               (*  explicit named subst. *)
62  | Meta of int * (term option) list                 (* numeric id,    *)
63                                                     (*  local context *)
64  | Sort of sort                                     (* sort *)
65  | Implicit                                         (* *)
66  | Cast of term * term                              (* value, type *)
67  | Prod of name * term * term                       (* binder, source, target *)
68  | Lambda of name * term * term                     (* binder, source, target *)
69  | LetIn of name * term * term                      (* binder, term, target *)
70  | Appl of term list                                (* arguments *)
71  | Const of UriManager.uri *                        (* uri,                   *)
72      term explicit_named_substitution               (*  explicit named subst. *)
73  | MutInd of UriManager.uri * int *                 (* uri, typeno, *)
74      term explicit_named_substitution               (*  explicit named subst. *)
75                                                     (* typeno is 0 based      *)
76  | MutConstruct of UriManager.uri *                 (* uri,                   *)
77     int * int *                                     (*  typeno, consno        *)
78      term explicit_named_substitution               (*  explicit named subst. *)
79                                                     (* typeno is 0 based      *)
80                                                     (* consno is 1 based      *)
81  | MutCase of UriManager.uri *                      (* ind. uri,             *)
82     int *                                           (*  ind. typeno,         *)
83     term * term *                                   (*  outtype, ind. term   *)
84     term list                                       (*  patterns             *)
85  | Fix of int * inductiveFun list                   (* funno (0 based), funs *)
86  | CoFix of int * coInductiveFun list               (* funno (0 based), funs *)
87 and obj =
88    Constant of string * term option * term *      (* id, body, type,          *)
89     UriManager.uri list                           (*  parameters              *)
90  | Variable of string * term option * term *      (* name, body, type         *)
91     UriManager.uri list                           (* parameters               *)
92  | CurrentProof of string * metasenv *            (* name, conjectures,       *)
93     term * term * UriManager.uri list             (*  value, type, parameters *)
94  | InductiveDefinition of inductiveType list *    (* inductive types,         *)
95     UriManager.uri list * int                     (*  parameters, n ind. pars *)
96 and inductiveType = 
97  string * bool * term *                       (* typename, inductive, arity *)
98   constructor list                            (*  constructors              *)
99 and constructor =
100  string * term                                (* id, type *)
101 and inductiveFun =
102  string * int * term * term                   (* name, ind. index, type, body *)
103 and coInductiveFun =
104  string * term * term                         (* name, type, body *)
105
106 (* a metasenv is a list of declarations of metas in declarations *)
107 (* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
108 (* depend on new ones.                                           *)
109 and conjecture = int * context * term
110 and metasenv = conjecture list
111
112 (* a metasenv is a list of declarations of metas in declarations *)
113 (* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
114 (* depend on new ones.                                           *)
115 and annconjecture = id * int * anncontext * annterm
116 and annmetasenv = annconjecture list
117
118 and annterm =
119    ARel of id * id * int *                          (* idref, DeBrujin index, *)
120     string                                          (*  binder                *)
121  | AVar of id * UriManager.uri *                    (* uri,                   *)
122     annterm explicit_named_substitution             (*  explicit named subst. *)
123  | AMeta of id * int * (annterm option) list        (* numeric id,    *)
124                                                     (*  local context *)
125  | ASort of id * sort                               (* sort *)
126  | AImplicit of id                                  (* *)
127  | ACast of id * annterm * annterm                  (* value, type *)
128  | AProd of id * name * annterm * annterm           (* binder, source, target *)
129  | ALambda of id * name * annterm * annterm         (* binder, source, target *)
130  | ALetIn of id * name * annterm * annterm          (* binder, term, target *)
131  | AAppl of id * annterm list                       (* arguments *)
132  | AConst of id * UriManager.uri *                  (* uri,                   *)
133     annterm explicit_named_substitution             (*  explicit named subst. *)
134  | AMutInd of id * UriManager.uri * int *           (* uri, typeno            *)
135     annterm explicit_named_substitution             (*  explicit named subst. *)
136                                                     (* typeno is 0 based *)
137  | AMutConstruct of id * UriManager.uri *           (* uri,                   *)
138     int * int *                                     (*  typeno, consno        *)
139     annterm explicit_named_substitution             (*  explicit named subst. *)
140                                                     (* typeno is 0 based *)
141                                                     (* consno is 1 based *)
142  | AMutCase of id * UriManager.uri *                (* ind. uri,             *)
143     int *                                           (*  ind. typeno,         *)
144     annterm * annterm *                             (*  outtype, ind. term   *)
145     annterm list                                    (*  patterns             *)
146  | AFix of id * int * anninductiveFun list          (* funno, functions *)
147  | ACoFix of id * int * anncoInductiveFun list      (* funno, functions *)
148 and annobj =
149    AConstant of id * id option * string *           (* name,         *)
150     annterm option * annterm *                      (*  body, type,  *)
151     UriManager.uri list                             (*  parameters   *)
152  | AVariable of id *
153     string * annterm option * annterm *             (* name, body, type *)
154     UriManager.uri list                             (*  parameters      *)
155  | ACurrentProof of id * id *
156     string * annmetasenv *                          (*  name, conjectures,    *)
157     annterm * annterm * UriManager.uri list         (*  value,type,parameters *)
158  | AInductiveDefinition of id *
159     anninductiveType list *                         (* inductive types ,      *)
160     UriManager.uri list * int                       (*  parameters,n ind. pars*)
161 and anninductiveType = 
162  id * string * bool * annterm *               (* typename, inductive, arity *)
163   annconstructor list                         (*  constructors              *)
164 and annconstructor =
165  string * annterm                             (* id, type *)
166 and anninductiveFun =
167  id * string * int * annterm * annterm        (* name, ind. index, type, body *)
168 and anncoInductiveFun =
169  id * string * annterm * annterm              (* name, type, body *)
170 and annotation =
171  string
172
173 and context_entry =                            (* A declaration or definition *)
174    Decl of term
175  | Def of term * term option                   (* body, type (if known) *)
176
177 and hypothesis =
178  (name * context_entry) option               (* None means no more accessible *)
179
180 and context = hypothesis list
181
182 and anncontext_entry =                         (* A declaration or definition *)
183    ADecl of annterm
184  | ADef of annterm
185
186 and annhypothesis =
187  id * (name * anncontext_entry) option       (* None means no more accessible *)
188
189 and anncontext = annhypothesis list
190 ;;