]> matita.cs.unibo.it Git - helm.git/blob - helm/interface/cic.ml
First very partial implementation of LetIn and bodyed Variables
[helm.git] / helm / interface / cic.ml
1 (******************************************************************************)
2 (*                                                                            *)
3 (*                               PROJECT HELM                                 *)
4 (*                                                                            *)
5 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
6 (*                                 14/06/2000                                 *)
7 (*                                                                            *)
8 (* This module defines the internal representation of the objects (variables, *)
9 (* blocks of (co)inductive definitions and constants) and the terms of cic    *)
10 (*                                                                            *)
11 (******************************************************************************)
12
13 (* STUFF TO MANAGE IDENTIFIERS *)
14 type id = string  (* the abstract type of the (annotated) node identifiers *)
15 type anntarget =
16    Object of annobj
17  | Term of annterm
18
19 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
20 and sort =
21    Prop
22  | Set
23  | Type
24 and name =
25    Name of string
26  | Anonimous
27 and term =
28    Rel of int                                       (* DeBrujin index *)
29  | Var of UriManager.uri                            (* uri *)
30  | Meta of int                                      (* numeric id *)
31  | Sort of sort                                     (* sort *)
32  | Implicit                                         (* *)
33  | Cast of term * term                              (* value, type *)
34  | Prod of name * term * term                       (* binder, source, target *)
35  | Lambda of name * term * term                     (* binder, source, target *)
36  | LetIn of name * term * term                      (* binder, term, target *)
37  | Appl of term list                                (* arguments *)
38  | Const of UriManager.uri * int                    (* uri, number of cookings*)
39  | Abst of UriManager.uri                           (* uri *)
40  | MutInd of UriManager.uri * int * int             (* uri, cookingsno, typeno*)
41  | MutConstruct of UriManager.uri * int *           (* uri, cookingsno, *)
42     int * int                                       (*  typeno, consno  *)
43  (*CSC: serve cookingsno?*)
44  | MutCase of UriManager.uri * int *                (* ind. uri, cookingsno, *)
45     int *                                           (*  ind. typeno,         *)
46     term * term *                                   (*  outtype, ind. term   *)
47     term list                                       (*  patterns             *)
48  | Fix of int * inductiveFun list                   (* funno, functions *)
49  | CoFix of int * coInductiveFun list               (* funno, functions *)
50 and obj =
51    Definition of string * term * term *           (* id, value, type,         *)
52     (int * UriManager.uri list) list              (*  parameters              *)
53  | Axiom of string * term *
54     (int * UriManager.uri list) list              (* id, type, parameters     *)
55  | Variable of string * term option * term        (* name, body, type         *)
56  | CurrentProof of string * (int * term) list *   (* name, conjectures,       *)
57     term * term                                   (*  value, type             *)
58  | InductiveDefinition of inductiveType list *    (* inductive types,         *)
59     (int * UriManager.uri list) list * int        (*  parameters, n ind. pars *)
60 and inductiveType = 
61  string * bool * term *                       (* typename, inductive, arity *)
62   constructor list                            (*  constructors              *)
63 and constructor =
64  string * term * bool list option ref         (* id, type, really recursive *)
65 and inductiveFun =
66  string * int * term * term                   (* name, ind. index, type, body *)
67 and coInductiveFun =
68  string * term * term                         (* name, type, body *)
69
70 and annterm =
71    ARel of id * annotation option ref *
72     int * string option                             (* DeBrujin index, binder *)
73  | AVar of id * annotation option ref *             
74     UriManager.uri                                  (* uri *)
75  | AMeta of id * annotation option ref * int        (* numeric id *)
76  | ASort of id * annotation option ref * sort       (* sort *)
77  | AImplicit of id * annotation option ref          (* *)
78  | ACast of id * annotation option ref *
79     annterm * annterm                               (* value, type *)
80  | AProd of id * annotation option ref *
81     name * annterm * annterm                        (* binder, source, target *)
82  | ALambda of id * annotation option ref *
83     name * annterm * annterm                        (* binder, source, target *)
84  | ALetIn of id * annotation option ref *
85     name * annterm * annterm                        (* binder, term, target *)
86  | AAppl of id * annotation option ref *
87     annterm list                                    (* arguments *)
88  | AConst of id * annotation option ref *
89     UriManager.uri * int                            (* uri, number of cookings*)
90  | AAbst of id * annotation option ref *
91     UriManager.uri                                  (* uri *)
92  | AMutInd of id * annotation option ref *
93     UriManager.uri * int * int                      (* uri, cookingsno, typeno*)
94  | AMutConstruct of id * annotation option ref *
95     UriManager.uri * int *                          (* uri, cookingsno, *)
96     int * int                                       (*  typeno, consno  *)
97  (*CSC: serve cookingsno?*)
98  | AMutCase of id * annotation option ref *
99     UriManager.uri * int *                          (* ind. uri, cookingsno  *)
100     int *                                           (*  ind. typeno,         *)
101     annterm * annterm *                             (*  outtype, ind. term   *)
102     annterm list                                    (*  patterns             *)
103  | AFix of id * annotation option ref *
104     int * anninductiveFun list                      (* funno, functions *)
105  | ACoFix of id * annotation option ref *
106     int * anncoInductiveFun list                    (* funno, functions *)
107 and annobj =
108    ADefinition of id * annotation option ref *
109     string *                                        (* id,           *)
110     annterm * annterm *                             (*  value, type, *)
111     (int * UriManager.uri list) list exactness      (*  parameters   *)
112  | AAxiom of id * annotation option ref *
113     string * annterm *                              (* id, type    *)
114     (int * UriManager.uri list) list                (*  parameters *)
115  | AVariable of id * annotation option ref *
116     string * annterm option * annterm               (* name, body, type *)
117  | ACurrentProof of id * annotation option ref *
118     string * (int * annterm) list *                 (*  name, conjectures, *)
119     annterm * annterm                               (*  value, type        *)
120  | AInductiveDefinition of id *
121     annotation option ref * anninductiveType list * (* inductive types ,      *)
122     (int * UriManager.uri list) list * int          (*  parameters,n ind. pars*)
123 and anninductiveType = 
124  string * bool * annterm *                    (* typename, inductive, arity *)
125   annconstructor list                         (*  constructors              *)
126 and annconstructor =
127  string * annterm * bool list option ref      (* id, type, really recursive *)
128 and anninductiveFun =
129  string * int * annterm * annterm             (* name, ind. index, type, body *)
130 and anncoInductiveFun =
131  string * annterm * annterm                   (* name, type, body *)
132 and annotation =
133  string
134 and 'a exactness =
135    Possible of 'a                            (* an approximation to something *)
136  | Actual of 'a                              (* something *)
137 ;;