1 (******************************************************************************)
5 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
8 (* This module defines the internal representation of the objects (variables, *)
9 (* blocks of (co)inductive definitions and constants) and the terms of cic *)
11 (******************************************************************************)
13 (* STUFF TO MANAGE IDENTIFIERS *)
14 type id = string (* the abstract type of the (annotated) node identifiers *)
19 (* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
28 Rel of int (* DeBrujin index *)
29 | Var of UriManager.uri (* uri *)
30 | Meta of int (* numeric id *)
31 | Sort of sort (* sort *)
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 | Appl of term list (* arguments *)
37 | Const of UriManager.uri * int (* uri, number of cookings*)
38 | Abst of UriManager.uri (* uri *)
39 | MutInd of UriManager.uri * int * int (* uri, cookingsno, typeno*)
40 | MutConstruct of UriManager.uri * int * (* uri, cookingsno, *)
41 int * int (* typeno, consno *)
42 (*CSC: serve cookingsno?*)
43 | MutCase of UriManager.uri * int * (* ind. uri, cookingsno, *)
44 int * (* ind. typeno, *)
45 term * term * (* outtype, ind. term *)
46 term list (* patterns *)
47 | Fix of int * inductiveFun list (* funno, functions *)
48 | CoFix of int * coInductiveFun list (* funno, functions *)
50 Definition of string * term * term * (* id, value, type, *)
51 (int * UriManager.uri list) list (* parameters *)
52 | Axiom of string * term *
53 (int * UriManager.uri list) list (* id, type, parameters *)
54 | Variable of string * term (* name, type *)
55 | CurrentProof of string * (int * term) list * (* name, conjectures, *)
56 term * term (* value, type *)
57 | InductiveDefinition of inductiveType list * (* inductive types, *)
58 (int * UriManager.uri list) list * int (* parameters, n ind. pars *)
60 string * bool * term * (* typename, inductive, arity *)
61 constructor list (* constructors *)
63 string * term * bool list option ref (* id, type, really recursive *)
65 string * int * term * term (* name, ind. index, type, body *)
67 string * term * term (* name, type, body *)
70 ARel of id * annotation option ref *
71 int * string option (* DeBrujin index, binder *)
72 | AVar of id * annotation option ref *
73 UriManager.uri (* uri *)
74 | AMeta of id * annotation option ref * int (* numeric id *)
75 | ASort of id * annotation option ref * sort (* sort *)
76 | AImplicit of id * annotation option ref (* *)
77 | ACast of id * annotation option ref *
78 annterm * annterm (* value, type *)
79 | AProd of id * annotation option ref *
80 name * annterm * annterm (* binder, source, target *)
81 | ALambda of id * annotation option ref *
82 name * annterm * annterm (* binder, source, target *)
83 | AAppl of id * annotation option ref *
84 annterm list (* arguments *)
85 | AConst of id * annotation option ref *
86 UriManager.uri * int (* uri, number of cookings*)
87 | AAbst of id * annotation option ref *
88 UriManager.uri (* uri *)
89 | AMutInd of id * annotation option ref *
90 UriManager.uri * int * int (* uri, cookingsno, typeno*)
91 | AMutConstruct of id * annotation option ref *
92 UriManager.uri * int * (* uri, cookingsno, *)
93 int * int (* typeno, consno *)
94 (*CSC: serve cookingsno?*)
95 | AMutCase of id * annotation option ref *
96 UriManager.uri * int * (* ind. uri, cookingsno *)
97 int * (* ind. typeno, *)
98 annterm * annterm * (* outtype, ind. term *)
99 annterm list (* patterns *)
100 | AFix of id * annotation option ref *
101 int * anninductiveFun list (* funno, functions *)
102 | ACoFix of id * annotation option ref *
103 int * anncoInductiveFun list (* funno, functions *)
105 ADefinition of id * annotation option ref *
107 annterm * annterm * (* value, type, *)
108 (int * UriManager.uri list) list exactness (* parameters *)
109 | AAxiom of id * annotation option ref *
110 string * annterm * (* id, type *)
111 (int * UriManager.uri list) list (* parameters *)
112 | AVariable of id * annotation option ref *
113 string * annterm (* name, type *)
114 | ACurrentProof of id * annotation option ref *
115 string * (int * annterm) list * (* name, conjectures, *)
116 annterm * annterm (* value, type *)
117 | AInductiveDefinition of id *
118 annotation option ref * anninductiveType list * (* inductive types , *)
119 (int * UriManager.uri list) list * int (* parameters,n ind. pars*)
120 and anninductiveType =
121 string * bool * annterm * (* typename, inductive, arity *)
122 annconstructor list (* constructors *)
124 string * annterm * bool list option ref (* id, type, really recursive *)
125 and anninductiveFun =
126 string * int * annterm * annterm (* name, ind. index, type, body *)
127 and anncoInductiveFun =
128 string * annterm * annterm (* name, type, body *)
132 Possible of 'a (* an approximation to something *)
133 | Actual of 'a (* something *)