1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
|
open Sign;;
open Classops;;
open Names;;
open Nameops
open Term;;
open Impargs;;
open Reduction;;
open Libnames;;
open Libobject;;
open Environ;;
open Declarations;;
open Prettyp;;
open Inductive;;
open Util;;
open Pp;;
open Declare;;
open Nametab
open Vernacexpr;;
open Decl_kinds;;
open Constrextern;;
open Topconstr;;
(* This function converts the parameter binders of an inductive definition,
in particular you have to be careful to handle each element in the
context containing all previously defined variables. This squeleton
of this procedure is taken from the function print_env in pretty.ml *)
let convert_env =
let convert_binder env (na, b, c) =
match b with
| Some b -> LocalRawDef ((dummy_loc,na), extern_constr true env b)
| None -> LocalRawAssum ([dummy_loc,na], default_binder_kind, extern_constr true env c) in
let rec cvrec env = function
[] -> []
| b::rest -> (convert_binder env b)::(cvrec (push_rel b env) rest) in
cvrec (Global.env());;
(* let mib string =
let sp = Nametab.sp_of_id CCI (id_of_string string) in
let lobj = Lib.map_leaf (objsp_of sp) in
let (cmap, _) = outMutualInductive lobj in
Listmap.map cmap CCI;; *)
(* This function is directly inspired by print_impl_args in pretty.ml *)
let impl_args_to_string_by_pos = function
[] -> None
| [i] -> Some(" position " ^ (string_of_int i) ^ " is implicit.")
| l -> Some (" positions " ^
(List.fold_right (fun i s -> (string_of_int i) ^ " " ^ s)
l
" are implicit."));;
(* This function is directly inspired by implicit_args_id in pretty.ml *)
let impl_args_to_string l =
impl_args_to_string_by_pos (positions_of_implicits l)
let implicit_args_id_to_ast_list id l ast_list =
(match impl_args_to_string l with
None -> ast_list
| Some(s) -> CommentString s::
CommentString ("For " ^ (string_of_id id))::
ast_list);;
(* This function construct an ast to enumerate the implicit positions for an
inductive type and its constructors. It is obtained directly from
implicit_args_msg in pretty.ml. *)
let implicit_args_to_ast_list sp mipv =
let implicit_args_descriptions =
let ast_list = ref [] in
(Array.iteri
(fun i mip ->
let imps = implicits_of_global (IndRef (sp, i)) in
(ast_list :=
implicit_args_id_to_ast_list mip.mind_typename imps !ast_list;
Array.iteri
(fun j idc ->
let impls = implicits_of_global
(ConstructRef ((sp,i),j+1)) in
ast_list :=
implicit_args_id_to_ast_list idc impls !ast_list)
mip.mind_consnames))
mipv;
!ast_list) in
match implicit_args_descriptions with
[] -> []
| _ -> [VernacComments (List.rev implicit_args_descriptions)];;
(* This function converts constructors for an inductive definition to a
Coqast.t. It is obtained directly from print_constructors in pretty.ml *)
let convert_constructors envpar names types =
let array_idC =
array_map2
(fun n t ->
let coercion_flag = false (* arbitrary *) in
(coercion_flag, ((dummy_loc,n), extern_constr true envpar t)))
names types in
Array.to_list array_idC;;
(* this function converts one inductive type in a possibly multiple inductive
definition *)
let convert_one_inductive sp tyi =
let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
let env = Global.env () in
let envpar = push_rel_context params env in
let sp = sp_of_global (IndRef (sp, tyi)) in
(((dummy_loc,basename sp),
convert_env(List.rev params),
(extern_constr true envpar arity),
convert_constructors envpar cstrnames cstrtypes), None);;
(* This function converts a Mutual inductive definition to a Coqast.t.
It is obtained directly from print_mutual in pretty.ml. However, all
references to kinds have been removed and it treats only CCI stuff. *)
let mutual_to_ast_list sp mib =
let mipv = (Global.lookup_mind sp).mind_packets in
let _, l =
Array.fold_right
(fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
VernacInductive (mib.mind_finite, l)
:: (implicit_args_to_ast_list sp mipv);;
let constr_to_ast v =
extern_constr true (Global.env()) v;;
let implicits_to_ast_list implicits =
match (impl_args_to_string implicits) with
| None -> []
| Some s -> [VernacComments [CommentString s]];;
let make_variable_ast name typ implicits =
(VernacAssumption
((Local,Definitional),false,(*inline flag*)
[false,([dummy_loc,name], constr_to_ast typ)]))
::(implicits_to_ast_list implicits);;
let make_definition_ast name c typ implicits =
VernacDefinition ((Global,false,Definition), (dummy_loc,name),
DefineBody ([], None, constr_to_ast c, Some (constr_to_ast typ)),
(fun _ _ -> ()))
::(implicits_to_ast_list implicits);;
(* This function is inspired by print_constant *)
let constant_to_ast_list kn =
let cb = Global.lookup_constant kn in
let c = cb.const_body in
let typ = Typeops.type_of_constant_type (Global.env()) cb.const_type in
let l = implicits_of_global (ConstRef kn) in
(match c with
None ->
make_variable_ast (id_of_label (con_label kn)) typ l
| Some c1 ->
make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l)
let variable_to_ast_list sp =
let (id, c, v) = Global.lookup_named sp in
let l = implicits_of_global (VarRef sp) in
(match c with
None ->
make_variable_ast id v l
| Some c1 ->
make_definition_ast id c1 v l);;
(* this function is taken from print_inductive in file pretty.ml *)
let inductive_to_ast_list sp =
let mib = Global.lookup_mind sp in
mutual_to_ast_list sp mib
(* this function is inspired by print_leaf_entry from pretty.ml *)
let leaf_entry_to_ast_list ((sp,kn),lobj) =
let tag = object_tag lobj in
match tag with
| "VARIABLE" -> variable_to_ast_list (basename sp)
| "CONSTANT" -> constant_to_ast_list (constant_of_kn kn)
| "INDUCTIVE" -> inductive_to_ast_list kn
| s ->
errorlabstrm
"print" (str ("printing of unrecognized object " ^
s ^ " has been required"));;
(* this function is inspired by print_name *)
let name_to_ast ref =
let (loc,qid) = qualid_of_reference ref in
let l =
try
let sp = Nametab.locate_obj qid in
let (sp,lobj) =
let (sp,entry) =
List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None)
in
match entry with
| Lib.Leaf obj -> (sp,obj)
| _ -> raise Not_found
in
leaf_entry_to_ast_list (sp,lobj)
with Not_found ->
try
match Nametab.locate qid with
| ConstRef sp -> constant_to_ast_list sp
| IndRef (sp,_) -> inductive_to_ast_list sp
| ConstructRef ((sp,_),_) -> inductive_to_ast_list sp
| VarRef sp -> variable_to_ast_list sp
with Not_found ->
try (* Var locale de but, pas var de section... donc pas d'implicits *)
let dir,name = repr_qualid qid in
if (repr_dirpath dir) <> [] then raise Not_found;
let (_,c,typ) = Global.lookup_named name in
(match c with
None -> make_variable_ast name typ []
| Some c1 -> make_definition_ast name c1 typ [])
with Not_found ->
try
let _sp = Nametab.locate_syntactic_definition qid in
errorlabstrm "print"
(str "printing of syntax definitions not implemented")
with Not_found ->
errorlabstrm "print"
(pr_qualid qid ++
spc () ++ str "not a defined object")
in
VernacList (List.map (fun x -> (dummy_loc,x)) l)
|
