summaryrefslogtreecommitdiff
path: root/plugins/extraction/ocaml.ml
blob: 36ca37131d6b5434fa1de2b38f0598587b1c6c9c (plain)
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
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: ocaml.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)

(*s Production of Ocaml syntax. *)

open Pp
open Util
open Names
open Nameops
open Libnames
open Table
open Miniml
open Mlutil
open Modutil
open Common
open Declarations


(*s Some utility functions. *)

let pp_tvar id =
  let s = string_of_id id in
  if String.length s < 2 || s.[1]<>'\''
  then str ("'"^s)
  else str ("' "^s)

let pp_tuple_light f = function
  | [] -> mt ()
  | [x] -> f true x
  | l ->
      pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l)

let pp_tuple f = function
  | [] -> mt ()
  | [x] -> f x
  | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l)

let pp_boxed_tuple f = function
  | [] -> mt ()
  | [x] -> f x
  | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))

let pp_abst = function
  | [] -> mt ()
  | l  ->
      str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++
      str " ->" ++ spc ()

let pp_parameters l =
  (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))

let pp_string_parameters l =
  (pp_boxed_tuple str l ++ space_if (l<>[]))

(*s Ocaml renaming issues. *)

let keywords =
  List.fold_right (fun s -> Idset.add (id_of_string s))
  [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
    "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
    "for"; "fun"; "function"; "functor"; "if"; "in"; "include";
    "inherit"; "initializer"; "lazy"; "let"; "match"; "method";
    "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
    "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
    "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
  Idset.empty

let pp_open mp = str ("open "^ string_of_modfile mp ^"\n")

let preamble _ used_modules usf =
  prlist pp_open used_modules ++
  (if used_modules = [] then mt () else fnl ()) ++
  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++
  (if usf.mldummy then
     str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n"
   else mt ()) ++
  (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ())

let sig_preamble _ used_modules usf =
  prlist pp_open used_modules ++
  (if used_modules = [] then mt () else fnl ()) ++
  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt())

(*s The pretty-printer for Ocaml syntax*)

(* Beware of the side-effects of [pp_global] and [pp_modname].
   They are used to update table of content for modules. Many [let]
   below should not be altered since they force evaluation order.
*)

let str_global k r =
  if is_inline_custom r then find_custom r else Common.pp_global k r

let pp_global k r = str (str_global k r)

let pp_modname mp = str (Common.pp_module mp)

let is_infix r =
  is_inline_custom r &&
  (let s = find_custom r in
   let l = String.length s in
   l >= 2 && s.[0] = '(' && s.[l-1] = ')')

let get_infix r =
  let s = find_custom r in
  String.sub s 1 (String.length s - 2)

exception NoRecord

let find_projections = function Record l -> l | _ -> raise NoRecord

(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
    are needed or not. *)

let mk_ind path s =
  make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)

let rec pp_type par vl t =
  let rec pp_rec par = function
    | Tmeta _ | Tvar' _ | Taxiom -> assert false
    | Tvar i -> (try pp_tvar (List.nth vl (pred i))
		 with _ -> (str "'a" ++ int i))
    | Tglob (r,[a1;a2]) when is_infix r ->
	pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
    | Tglob (r,[]) -> pp_global Type r
    | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" ->
	pp_tuple_light pp_rec l
    | Tglob (r,l) ->
	pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
    | Tarr (t1,t2) ->
	pp_par par
	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
    | Tdummy _ -> str "__"
    | Tunknown -> str "__"
  in
  hov 0 (pp_rec par t)

(*s Pretty-printing of expressions. [par] indicates whether
    parentheses are needed or not. [env] is the list of names for the
    de Bruijn variables. [args] is the list of collected arguments
    (already pretty-printed). *)

let is_ifthenelse = function
  | [|(r1,[],_);(r2,[],_)|] ->
      (try (find_custom r1 = "true") && (find_custom r2 = "false")
       with Not_found -> false)
  | _ -> false

let expr_needs_par = function
  | MLlam _  -> true
  | MLcase (_,_,[|_|]) -> false
  | MLcase (_,_,pv) -> not (is_ifthenelse pv)
  | _        -> false


(** Special hack for constants of type Ascii.ascii : if an
    [Extract Inductive ascii => char] has been declared, then
    the constants are directly turned into chars *)

let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"

let check_extract_ascii () =
  try find_custom (IndRef (ind_ascii,0)) = "char" with Not_found -> false

let is_list_cons l =
 List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l

let pp_char l =
  let rec cumul = function
    | [] -> 0
    | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
    | _ -> assert false
  in str ("'"^Char.escaped (Char.chr (cumul l))^"'")

let rec pp_expr par env args =
  let par' = args <> [] || par
  and apply st = pp_apply st par args in
  function
    | MLrel n ->
	let id = get_db_name n env in apply (pr_id id)
    | MLapp (f,args') ->
	let stl = List.map (pp_expr true env []) args' in
        pp_expr par env (stl @ args) f
    | MLlam _ as a ->
      	let fl,a' = collect_lams a in
	let fl = List.map id_of_mlid fl in
	let fl,env' = push_vars fl env in
	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
	apply (pp_par par' st)
    | MLletin (id,a1,a2) ->
	let i,env' = push_vars [id_of_mlid id] env in
	let pp_id = pr_id (List.hd i)
	and pp_a1 = pp_expr false env [] a1
	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
	hv 0
	  (apply
	     (pp_par par'
		(hv 0
		   (hov 2
		      (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++
		    spc () ++ str "in") ++
		 spc () ++ hov 0 pp_a2)))
    | MLglob r ->
	(try
	   let args = list_skipn (projection_arity r) args in
	   let record = List.hd args in
	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
	 with _ -> apply (pp_global Term r))
    | MLcons(_,ConstructRef ((kn,0),1),l)
        when kn = ind_ascii && check_extract_ascii () & is_list_cons l ->
	assert (args=[]);
	pp_char l
    | MLcons (Coinductive,r,[]) ->
	assert (args=[]);
	pp_par par (str "lazy " ++ pp_global Cons r)
    | MLcons (Coinductive,r,args') ->
	assert (args=[]);
	let tuple = pp_tuple (pp_expr true env []) args' in
	pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")")
    | MLcons (_,r,[]) ->
	assert (args=[]);
	pp_global Cons r
    | MLcons (Record projs, r, args') ->
	assert (args=[]);
	pp_record_pat (projs, List.map (pp_expr true env []) args')
    | MLcons (_,r,[arg1;arg2]) when is_infix r ->
	assert (args=[]);
	pp_par par
	  ((pp_expr true env [] arg1) ++ str (get_infix r) ++
	   (pp_expr true env [] arg2))
    | MLcons (_,r,args') ->
	assert (args=[]);
	let tuple = pp_tuple (pp_expr true env []) args' in
	if str_global Cons r = "" (* hack Extract Inductive prod *)
	then tuple
	else pp_par par (pp_global Cons r ++ spc () ++ tuple)
    | MLcase (_, t, pv) when is_custom_match pv ->
	let mkfun (_,ids,e) =
	  if ids <> [] then named_lams (List.rev ids) e
	  else dummy_lams (ast_lift 1 e) 1
	in
	hov 2 (str (find_custom_match pv) ++ fnl () ++
		 prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
	       ++ pp_expr true env [] t)
    | MLcase ((i,factors), t, pv) ->
	let expr = if i = Coinductive then
	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
	else
	  (pp_expr false env [] t)
	in
	(try
	   let projs = find_projections i in
	   let (_, ids, c) = pv.(0) in
	   let n = List.length ids in
	   match c with
	     | MLrel i when i <= n ->
		 apply (pp_par par' (pp_expr true env [] t ++ str "." ++
				     pp_global Term (List.nth projs (n-i))))
	     | MLapp (MLrel i, a) when i <= n ->
		 if List.exists (ast_occurs_itvl 1 n) a
		 then raise NoRecord
		 else
		   let ids,env' = push_vars (List.rev_map id_of_mlid ids) env
		   in
		   (pp_apply
		      (pp_expr true env [] t ++ str "." ++
		       pp_global Term (List.nth projs (n-i)))
		      par ((List.map (pp_expr true env' []) a) @ args))
	     | _ -> raise NoRecord
	 with NoRecord ->
	   if Array.length pv = 1 then
	     let s1,s2 = pp_one_pat env i pv.(0) in
	     apply
	       (hv 0
		  (pp_par par'
		     (hv 0
			(hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr)
			 ++ spc () ++ str "in") ++
		      spc () ++ hov 0 s2)))
	   else
 	     apply
      	       (pp_par par'
		  (try pp_ifthenelse par' env expr pv
		   with Not_found ->
		     v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++
			  str "  | " ++ pp_pat env (i,factors) pv))))
    | MLfix (i,ids,defs) ->
	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
      	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
    | MLexn s ->
	(* An [MLexn] may be applied, but I don't really care. *)
	pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
    | MLdummy ->
	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
    | MLmagic a ->
	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
    | MLaxiom ->
	pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")


and pp_record_pat (projs, args) =
   str "{ " ++
   prlist_with_sep (fun () -> str ";" ++ spc ())
     (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a)
     (List.combine projs args) ++
   str " }"

and pp_ifthenelse par env expr pv = match pv with
  | [|(tru,[],the);(fal,[],els)|] when
      (find_custom tru = "true") && (find_custom fal = "false")
      ->
      hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++
            hov 2 (str "then " ++
		   hov 2 (pp_expr (expr_needs_par the) env [] the)) ++ spc () ++
	    hov 2 (str "else " ++
	           hov 2 (pp_expr (expr_needs_par els) env [] els)))
  | _ -> raise Not_found

and pp_one_pat env i (r,ids,t) =
  let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
  let expr = pp_expr (expr_needs_par t) env' [] t in
  try
    let projs = find_projections i in
    pp_record_pat (projs, List.rev_map pr_id ids), expr
  with NoRecord ->
    (match List.rev ids with
      | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2
      | [] -> pp_global Cons r
      | ids ->
	  (* hack Extract Inductive prod *)
	  (if str_global Cons r = "" then mt () else pp_global Cons r ++ spc ())
	   ++ pp_boxed_tuple pr_id ids),
    expr

and pp_pat env (info,factors) pv =
  let factor_br, factor_l = try match factors with
    | BranchFun (i::_ as l) -> check_function_branch pv.(i), l
    | BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l
    | _ -> MLdummy, []
  with Impossible -> MLdummy, []
  in
  let par = expr_needs_par factor_br in
  let last = Array.length pv - 1 in
  prvecti
    (fun i x -> if List.mem i factor_l then mt () else
       let s1,s2 = pp_one_pat env info x in
       hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++
       if i = last && factor_l = [] then mt () else
       fnl () ++ str "  | ") pv
  ++
  if factor_l = [] then mt () else match factors with
    | BranchFun _ ->
	let ids, env' = push_vars [anonymous_name] env in
	hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++
	       pp_expr par env' [] factor_br)
    | BranchCst _ ->
	hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br)
    | BranchNone -> mt ()

and pp_function env t =
  let bl,t' = collect_lams t in
  let bl,env' = push_vars (List.map id_of_mlid bl) env in
  match t' with
    | MLcase(i,MLrel 1,pv) when fst i=Standard && not (is_custom_match pv) ->
	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
	  pr_binding (List.rev (List.tl bl)) ++
       	  str " = function" ++ fnl () ++
	  v 0 (str "  | " ++ pp_pat env' i pv)
	else
          pr_binding (List.rev bl) ++
          str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
	  v 0 (str "  | " ++ pp_pat env' i pv)
    | _ ->
          pr_binding (List.rev bl) ++
	  str " =" ++ fnl () ++ str "  " ++
	  hov 2 (pp_expr false env' [] t')

(*s names of the functions ([ids]) are already pushed in [env],
    and passed here just for convenience. *)

and pp_fix par env i (ids,bl) args =
  pp_par par
    (v 0 (str "let rec " ++
	  prvect_with_sep
      	    (fun () -> fnl () ++ str "and ")
	    (fun (fi,ti) -> pr_id fi ++ pp_function env ti)
	    (array_map2 (fun id b -> (id,b)) ids bl) ++
	  fnl () ++
	  hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))

let pp_val e typ =
  hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++
  str " **)")  ++ fnl2 ()

(*s Pretty-printing of [Dfix] *)

let pp_Dfix (rv,c,t) =
  let names = Array.map
    (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
  in
  let rec pp sep letand i =
    if i >= Array.length rv then mt ()
    else if is_inline_custom rv.(i) then pp sep letand (i+1)
    else
      let def =
	if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
	else pp_function (empty_env ()) c.(i)
      in
      sep () ++ pp_val names.(i) t.(i) ++
      str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1)
  in pp mt "let rec " 0

(*s Pretty-printing of inductive types declaration. *)

let pp_equiv param_list name = function
  | NoEquiv, _ -> mt ()
  | Equiv kn, i ->
      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (mind_of_kn kn,i))
  | RenEquiv ren, _  ->
      str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name

let pp_comment s = str "(* " ++ s ++ str " *)"

let pp_one_ind prefix ip_equiv pl name cnames ctyps =
  let pl = rename_tvars keywords pl in
  let pp_constructor i typs =
    (if i=0 then mt () else fnl ()) ++
    hov 5 (str "  | " ++ cnames.(i) ++
	   (if typs = [] then mt () else str " of ") ++
	   prlist_with_sep
	    (fun () -> spc () ++ str "* ") (pp_type true pl) typs)
  in
  pp_parameters pl ++ str prefix ++ name ++
  pp_equiv pl name ip_equiv ++ str " =" ++
  if Array.length ctyps = 0 then str " unit (* empty inductive *)"
  else fnl () ++ v 0 (prvecti pp_constructor ctyps)

let pp_logical_ind packet =
  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
  fnl () ++
  pp_comment (str "with constructors : " ++
	      prvect_with_sep spc pr_id packet.ip_consnames) ++
  fnl ()

let pp_singleton kn packet =
  let name = pp_global Type (IndRef (mind_of_kn kn,0)) in
  let l = rename_tvars keywords packet.ip_vars in
  hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
	 pp_comment (str "singleton inductive, whose constructor was " ++
		     pr_id packet.ip_consnames.(0)))

let pp_record kn projs ip_equiv packet =
  let name = pp_global Type (IndRef (mind_of_kn kn,0)) in
  let projnames = List.map (pp_global Term) projs in
  let l = List.combine projnames packet.ip_types.(0) in
  let pl = rename_tvars keywords packet.ip_vars in
  str "type " ++ pp_parameters pl ++ name ++
  pp_equiv pl name ip_equiv ++ str " = { "++
  hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ())
	   (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l)
  ++ str " }"

let pp_coind pl name =
  let pl = rename_tvars keywords pl in
  pp_parameters pl ++ name ++ str " = " ++
  pp_parameters pl ++ str "__" ++ name ++ str " Lazy.t" ++
  fnl() ++ str "and "

let pp_ind co kn ind =
  let prefix = if co then "__" else "" in
  let some = ref false in
  let init= ref (str "type ") in
  let names =
    Array.mapi (fun i p -> if p.ip_logical then mt () else
		  pp_global Type (IndRef (mind_of_kn kn,i)))
      ind.ind_packets
  in
  let cnames =
    Array.mapi
      (fun i p -> if p.ip_logical then [||] else
	 Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((mind_of_kn kn,i),j+1)))
	   p.ip_types)
      ind.ind_packets
  in
  let rec pp i =
    if i >= Array.length ind.ind_packets then mt ()
    else
      let ip = (mind_of_kn kn,i) in
      let ip_equiv = ind.ind_equiv, i in
      let p = ind.ind_packets.(i) in
      if is_custom (IndRef ip) then pp (i+1)
      else begin
	some := true;
	if p.ip_logical then pp_logical_ind p ++ pp (i+1)
	else
	  let s = !init in
	  begin
	    init := (fnl () ++ str "and ");
	    s ++
	    (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
	    pp_one_ind
	      prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++
	    pp (i+1)
	  end
      end
  in
  let st = pp 0 in if !some then st else failwith "empty phrase"


(*s Pretty-printing of a declaration. *)

let pp_mind kn i =
  match i.ind_info with
    | Singleton -> pp_singleton kn i.ind_packets.(0)
    | Coinductive -> pp_ind true kn i
    | Record projs ->
	pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0)
    | Standard -> pp_ind false kn i

let pp_decl = function
    | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
    | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase"
    | Dind (kn,i) -> pp_mind kn i
    | Dtype (r, l, t) ->
        let name = pp_global Type r in
	let l = rename_tvars keywords l in
        let ids, def =
	  try
	    let ids,s = find_type_custom r in
	    pp_string_parameters ids, str "=" ++ spc () ++ str s
	  with Not_found ->
	    pp_parameters l,
	    if t = Taxiom then str "(* AXIOM TO BE REALIZED *)"
	    else str "=" ++ spc () ++ pp_type false l t
	in
	hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
    | Dterm (r, a, t) ->
	let def =
	  if is_custom r then str (" = " ^ find_custom r)
	  else if is_projection r then
	    (prvect str (Array.make (projection_arity r) " _")) ++
	    str " x = x."
	  else pp_function (empty_env ()) a
	in
	let name = pp_global Term r in
	let postdef = if is_projection r then name else mt () in
	pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef)
    | Dfix (rv,defs,typs) ->
	pp_Dfix (rv,defs,typs)

let pp_alias_decl ren = function
  | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
  | Dtype (r, l, _) ->
      let name = pp_global Type r in
      let l = rename_tvars keywords l in
      let ids = pp_parameters l in
      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
	     str (ren^".") ++ name)
  | Dterm (r, a, t) ->
      let name = pp_global Term r in
      hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name)
  | Dfix (rv, _, _) ->
      prvecti (fun i r -> if is_inline_custom r then mt () else
		 let name = pp_global Term r in
		 hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++
		 fnl ())
	rv

let pp_spec = function
  | Sval (r,_) when is_inline_custom r -> failwith "empty phrase"
  | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
  | Sind (kn,i) -> pp_mind kn i
  | Sval (r,t) ->
      let def = pp_type false [] t in
      let name = pp_global Term r in
      hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
  | Stype (r,vl,ot) ->
      let name = pp_global Type r in
      let l = rename_tvars keywords vl in
      let ids, def =
	try
	  let ids, s = find_type_custom r in
	  pp_string_parameters ids,  str "= " ++ str s
	with Not_found ->
	  let ids = pp_parameters l in
	  match ot with
	    | None -> ids, mt ()
	    | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)"
	    | Some t -> ids, str "=" ++ spc () ++ pp_type false l t
      in
      hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)

let pp_alias_spec ren = function
  | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
  | Stype (r,l,_) ->
      let name = pp_global Type r in
      let l = rename_tvars keywords l in
      let ids = pp_parameters l in
      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
	     str (ren^".") ++ name)
  | Sval _ -> assert false

let rec pp_specif = function
  | (_,Spec (Sval _ as s)) -> pp_spec s
  | (l,Spec s) ->
      (try
	 let ren = Common.check_duplicate (top_visible_mp ()) l in
	 hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++
	 fnl () ++ str "end" ++ fnl () ++
	 pp_alias_spec ren s
       with Not_found -> pp_spec s)
  | (l,Smodule mt) ->
      let def = pp_module_type [] mt in
      let def' = pp_module_type [] mt in
      let name = pp_modname (MPdot (top_visible_mp (), l)) in
      hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++
      (try
	 let ren = Common.check_duplicate (top_visible_mp ()) l in
	 fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def')
       with Not_found -> Pp.mt ())
  | (l,Smodtype mt) ->
      let def = pp_module_type [] mt in
      let name = pp_modname (MPdot (top_visible_mp (), l)) in
      hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
      (try
	 let ren = Common.check_duplicate (top_visible_mp ()) l in
	 fnl () ++ str ("module type "^ren^" = ") ++ name
       with Not_found -> Pp.mt ())

and pp_module_type params = function
  | MTident kn ->
      pp_modname kn
  | MTfunsig (mbid, mt, mt') ->
      let typ = pp_module_type [] mt in
      let name = pp_modname (MPbound mbid) in
      let def = pp_module_type (MPbound mbid :: params) mt' in
      str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
  | MTsig (mp, sign) ->
      push_visible mp params;
      let l = map_succeed pp_specif sign in
      pop_visible ();
      str "sig " ++ fnl () ++
      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
	fnl () ++ str "end"
  | MTwith(mt,ML_With_type(idl,vl,typ)) ->
      let ids = pp_parameters (rename_tvars keywords vl) in
      let mp_mt = msid_of_mt mt in
      let l,idl' = list_sep_last idl in
      let mp_w =
	List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
      in
      let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l)) in
      push_visible mp_mt [];
      let pp_w = str " with type " ++ ids ++ pp_global Type r in
      pop_visible();
      pp_module_type [] mt ++ pp_w ++ str " = " ++ pp_type false vl typ
  | MTwith(mt,ML_With_module(idl,mp)) ->
      let mp_mt = msid_of_mt mt in
      let mp_w =
	List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl
      in
      push_visible mp_mt [];
      let pp_w = str " with module " ++ pp_modname mp_w in
      pop_visible ();
      pp_module_type [] mt ++ pp_w ++ str " = " ++ pp_modname mp

let is_short = function MEident _ | MEapply _ -> true | _ -> false

let rec pp_structure_elem = function
  | (l,SEdecl d) ->
       (try
	 let ren = Common.check_duplicate (top_visible_mp ()) l in
	 hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++
	 fnl () ++ str "end" ++ fnl () ++
	 pp_alias_decl ren d
	with Not_found -> pp_decl d)
  | (l,SEmodule m) ->
      let typ =
        (* virtual printing of the type, in order to have a correct mli later*)
	if Common.get_phase () = Pre then
	  str ": " ++ pp_module_type [] m.ml_mod_type
	else mt ()
      in
      let def = pp_module_expr [] m.ml_mod_expr in
      let name = pp_modname (MPdot (top_visible_mp (), l)) in
      hov 1
	(str "module " ++ name ++ typ ++ str " = " ++
	 (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++
      (try
	 let ren = Common.check_duplicate (top_visible_mp ()) l in
	 fnl () ++ str ("module "^ren^" = ") ++ name
       with Not_found -> mt ())
  | (l,SEmodtype m) ->
      let def = pp_module_type [] m in
      let name = pp_modname (MPdot (top_visible_mp (), l)) in
      hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
      (try
	 let ren = Common.check_duplicate (top_visible_mp ()) l in
         fnl () ++ str ("module type "^ren^" = ") ++ name
       with Not_found -> mt ())

and pp_module_expr params = function
  | MEident mp -> pp_modname mp
  | MEapply (me, me') ->
      pp_module_expr [] me ++ str "(" ++ pp_module_expr [] me' ++ str ")"
  | MEfunctor (mbid, mt, me) ->
      let name = pp_modname (MPbound mbid) in
      let typ = pp_module_type [] mt in
      let def = pp_module_expr (MPbound mbid :: params) me in
      str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
  | MEstruct (mp, sel) ->
      push_visible mp params;
      let l = map_succeed pp_structure_elem sel in
      pop_visible ();
      str "struct " ++ fnl () ++
      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
      fnl () ++ str "end"

let do_struct f s =
  let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt ()
  in
  let ppl (mp,sel) =
    push_visible mp [];
    let p = prlist_strict pp sel in
    (* for monolithic extraction, we try to simulate the unavailability
       of [MPfile] in names by artificially nesting these [MPfile] *)
    (if modular () then pop_visible ()); p
  in
  let p = prlist_strict ppl s in
  (if not (modular ()) then repeat (List.length s) pop_visible ());
  p

let pp_struct s = do_struct pp_structure_elem s

let pp_signature s = do_struct pp_specif s

let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt ()

let ocaml_descr = {
  keywords = keywords;
  file_suffix = ".ml";
  preamble = preamble;
  pp_struct = pp_struct;
  sig_suffix = Some ".mli";
  sig_preamble = sig_preamble;
  pp_sig = pp_signature;
  pp_decl = pp_decl;
}