Source file ocaml.ml
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
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
open Pp
open CErrors
open Util
open Names
open ModPath
open Table
open Miniml
open Mlutil
open Modutil
open Common
let pp_tvar id = str ("'" ^ Id.to_string id)
let pp_abst = function
| [] -> mt ()
| l ->
str "fun " ++ prlist_with_sep (fun () -> str " ") Id.print l ++
str " ->" ++ spc ()
let pp_parameters l =
(pp_boxed_tuple pp_tvar l ++ space_if (not (List.is_empty l)))
let pp_string_parameters l =
(pp_boxed_tuple str l ++ space_if (not (List.is_empty l)))
let pp_letin pat def body =
let fstline = str "let " ++ pat ++ str " =" ++ spc () ++ def in
hv 0 (hv 0 (hov 2 fstline ++ spc () ++ str "in") ++ spc () ++ hov 0 body)
let keywords =
List.fold_right (fun s -> Id.Set.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"; "nonrec"; "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" ; "_" ; "__" ]
Id.Set.empty
let pp_open table mp = str ("open "^ string_of_modfile (State.get_table table) mp) ++ fnl ()
let s = str "(* " ++ hov 0 s ++ str " *)"
let = function
| None -> mt ()
| Some com -> pp_comment com ++ fnl2 ()
let then_nl pp = if Pp.ismt pp then mt () else pp ++ fnl ()
let pp_tdummy usf =
if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt ()
let pp_mldummy usf =
if usf.mldummy then
str "let __ = let rec f _ = Obj.repr f in Obj.repr f" ++ fnl ()
else mt ()
let preamble table _ used_modules usf =
pp_header_comment comment ++
then_nl (prlist (fun o -> pp_open table o) used_modules) ++
then_nl (pp_tdummy usf ++ pp_mldummy usf)
let sig_preamble table _ used_modules usf =
pp_header_comment comment ++
then_nl (prlist (fun o -> pp_open table o) used_modules) ++
then_nl (pp_tdummy usf)
let str_global_with_key table k key r =
if is_inline_custom r then find_custom r else Common.pp_global_with_key table k key r
let str_global table k r = str_global_with_key table k (repr_of_r r) r
let pp_global_with_key table k key r = str (str_global_with_key table k key r)
let pp_global table k r = str (str_global table k r)
let pp_global_name table k r = str (Common.pp_global table k r)
let pp_modname table mp = str (Common.pp_module table mp)
let infix_symbols =
['=' ; '<' ; '>' ; '@' ; '^' ; ';' ; '&' ; '+' ; '-' ; '*' ; '/' ; '$' ; '%' ]
let operator_chars =
[ '!' ; '$' ; '%' ; '&' ; '*' ; '+' ; '-' ; '.' ; '/' ; ':' ; '<' ; '=' ; '>' ; '?' ; '@' ; '^' ; '|' ; '~' ]
let builtin_infixes =
[ "::" ; "," ]
let substring_all_opchars s start stop =
let rec check_char i =
if i >= stop then true
else
List.mem s.[i] operator_chars && check_char (i+1)
in
check_char start
let is_infix r =
is_inline_custom r &&
(let s = find_custom r in
let len = String.length s in
len >= 3 &&
(s.[0] == '(' && s.[len-1] == ')' &&
let inparens = String.trim (String.sub s 1 (len - 2)) in
let inparens_len = String.length inparens in
(List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) ||
(inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len) ||
(List.mem inparens builtin_infixes)))
let get_infix r =
let s = find_custom r in
String.sub s 1 (String.length s - 2)
let get_ind r = let open GlobRef in match r.glob with
| IndRef _ -> r
| ConstructRef (ind,_) -> { glob = IndRef ind; inst = r.inst }
| _ -> assert false
let kn_of_ind r = let open GlobRef in match r.glob with
| IndRef (kn,_) -> MutInd.user kn
| _ -> assert false
let pp_one_field table r i = function
| Some r' -> pp_global_with_key table Term (kn_of_ind (get_ind r)) r'
| None -> pp_global table Type (get_ind r) ++ str "__" ++ int i
let pp_field table r fields i = pp_one_field table r i (List.nth fields i)
let pp_fields table r fields = List.map_i (pp_one_field table r) 0 fields
let pp_type table 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 Failure _ -> (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 table Type r
| Tglob (gr,l)
when not (keep_singleton ()) && Rocqlib.check_ref sig_type_name gr.glob ->
pp_tuple_light pp_rec l
| Tglob (r,l) ->
pp_tuple_light pp_rec l ++ spc () ++ pp_global table 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)
let is_bool_patt p s =
try
let r = match p with
| Pusual r -> r
| Pcons (r,[]) -> r
| _ -> raise Not_found
in
String.equal (find_custom r) s
with Not_found -> false
let is_ifthenelse = function
| [|([],p1,_);([],p2,_)|] -> is_bool_patt p1 "true" && is_bool_patt p2 "false"
| _ -> false
let expr_needs_par = function
| MLlam _ -> true
| MLcase (_,_,[|_|]) -> false
| MLcase (_,_,pv) -> not (is_ifthenelse pv)
| _ -> false
let rec pp_expr table par env args =
let apply st = pp_apply st par args
and apply2 st = pp_apply2 st par args in
function
| MLrel n ->
let id = get_db_name n env in
let id = if Id.equal id dummy_name then Id.of_string "__" else id in
apply (Id.print id)
| MLapp (f,args') ->
let stl = List.map (pp_expr table true env []) args' in
pp_expr table 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 table false env' [] a' in
apply2 st
| MLletin (id,a1,a2) ->
let i,env' = push_vars [id_of_mlid id] env in
let pp_id = Id.print (List.hd i)
and pp_a1 = pp_expr table false env [] a1
and pp_a2 = pp_expr table (not par && expr_needs_par a2) env' [] a2 in
hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
| MLglob r -> apply (pp_global table Term r)
| MLfix (i,ids,defs) ->
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
pp_fix table par env' i (Array.of_list (List.rev ids'),defs) args
| MLexn s ->
pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
| MLdummy k ->
(match msg_of_implicit k with
| "" -> str "__"
| s -> str "__" ++ spc () ++ str ("(* "^s^" *)"))
| MLmagic a ->
pp_apply (str "Obj.magic") par (pp_expr table true env [] a :: args)
| MLaxiom s ->
pp_par par (str "failwith \"AXIOM TO BE REALIZED (" ++ str s ++ str ")\"")
| MLcons (_,r,a) as c ->
assert (List.is_empty args);
begin match a with
| _ when is_native_char c -> pp_native_char c
| _ when is_native_string c -> pp_native_string c
| [a1;a2] when is_infix r ->
let pp = pp_expr table true env [] in
pp_par par (pp a1 ++ str (get_infix r) ++ pp a2)
| _ when is_coinductive (State.get_table table) r ->
let ne = not (List.is_empty a) in
let tuple = space_if ne ++ pp_tuple (pp_expr table true env []) a in
pp_par par (str "lazy " ++ pp_par ne (pp_global table Cons r ++ tuple))
| [] -> pp_global table Cons r
| _ ->
let fds = get_record_fields (State.get_table table) r in
if not (List.is_empty fds) then
pp_record_pat (pp_fields table r fds, List.map (pp_expr table true env []) a)
else
let tuple = pp_tuple (pp_expr table true env []) a in
if String.is_empty (str_global table Cons r)
then tuple
else pp_par par (pp_global table Cons r ++ spc () ++ tuple)
end
| MLtuple l ->
assert (List.is_empty args);
pp_boxed_tuple (pp_expr table true env []) l
| MLcase (_, t, pv) when is_custom_match pv ->
if not (is_regular_match pv) then
user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
let mkfun (ids,_,e) =
if not (List.is_empty ids) then named_lams (List.rev ids) e
else dummy_lams (ast_lift 1 e) 1
in
let pp_branch tr = pp_expr table true env [] (mkfun tr) ++ fnl () in
let inner =
str (find_custom_match pv) ++ fnl () ++
prvect pp_branch pv ++
pp_expr table true env [] t
in
apply2 (hov 2 inner)
| MLcase (typ, t, pv) ->
let head =
if not (is_coinductive_type (State.get_table table) typ) then pp_expr table false env [] t
else (str "Lazy.force" ++ spc () ++ pp_expr table true env [] t)
in
(try pp_record_proj table par env typ t pv args
with Impossible ->
if Int.equal (Array.length pv) 1 then
let s1,s2 = pp_one_pat table env pv.(0) in
hv 0 (apply2 (pp_letin s1 head s2))
else
(try apply2 (pp_ifthenelse table env head pv)
with Not_found ->
apply2
(v 0 (str "match " ++ head ++ str " with" ++ fnl () ++
pp_pat table env pv))))
| MLuint i ->
assert (args=[]);
str "(" ++ str (Uint63.compile i) ++ str ")"
| MLfloat f ->
assert (args=[]);
str "(" ++ str (Float64.compile f) ++ str ")"
| MLstring s ->
assert (args=[]);
str "(" ++ str (Pstring.compile s) ++ str ")"
| MLparray(t,def) ->
assert (args=[]);
let tuple = pp_array (pp_expr table true env []) (Array.to_list t) in
let def = pp_expr table true env [] def in
str "(ExtrNative.of_array [|" ++ tuple ++ str "|]" ++ spc () ++ def ++ str")"
and pp_record_proj table par env typ t pv args =
let fields = record_fields_of_type (State.get_table table) typ in
if List.is_empty fields then raise Impossible;
if not (Int.equal (Array.length pv) 1) then raise Impossible;
if has_deep_pattern pv then raise Impossible;
let (ids,pat,body) = pv.(0) in
let n = List.length ids in
let no_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
let rel_i,a = match body with
| MLrel i | MLmagic(MLrel i) when i <= n -> i,[]
| MLapp(MLrel i, a) | MLmagic(MLapp(MLrel i, a))
| MLapp(MLmagic(MLrel i), a) when i<=n && no_patvar a -> i,a
| _ -> raise Impossible
in
let magic =
match body with MLmagic _ | MLapp(MLmagic _, _) -> true | _ -> false
in
let rec lookup_rel i idx = function
| Prel j :: l -> if Int.equal i j then idx else lookup_rel i (idx+1) l
| Pwild :: l -> lookup_rel i (idx+1) l
| _ -> raise Impossible
in
let r,idx = match pat with
| Pusual r -> r, n-rel_i
| Pcons (r,l) -> r, lookup_rel rel_i 0 l
| _ -> raise Impossible
in
if is_infix r then raise Impossible;
let env' = snd (push_vars (List.rev_map id_of_mlid ids) env) in
let pp_args = (List.map (pp_expr table true env' []) a) @ args in
let pp_head = pp_expr table true env [] t ++ str "." ++ pp_field table r fields idx
in
if magic then
pp_apply (str "Obj.magic") par (pp_head :: pp_args)
else
pp_apply pp_head par pp_args
and pp_record_pat (fields, args) =
str "{ " ++
prlist_with_sep (fun () -> str ";" ++ spc ())
(fun (f,a) -> f ++ str " =" ++ spc () ++ a)
(List.combine fields args) ++
str " }"
and pp_cons_pat table r ppl =
if is_infix r && Int.equal (List.length ppl) 2 then
List.hd ppl ++ str (get_infix r) ++ List.hd (List.tl ppl)
else
let fields = get_record_fields (State.get_table table) r in
if not (List.is_empty fields) then pp_record_pat (pp_fields table r fields, ppl)
else if String.is_empty (str_global table Cons r) then
pp_boxed_tuple identity ppl
else
pp_global table Cons r ++ space_if (not (List.is_empty ppl)) ++ pp_boxed_tuple identity ppl
and pp_gen_pat table ids env = function
| Pcons (r, l) -> pp_cons_pat table r (List.map (pp_gen_pat table ids env) l)
| Pusual r -> pp_cons_pat table r (List.map Id.print ids)
| Ptuple l -> pp_boxed_tuple (pp_gen_pat table ids env) l
| Pwild -> str "_"
| Prel n -> Id.print (get_db_name n env)
and pp_ifthenelse table env expr pv = match pv with
| [|([],tru,the);([],fal,els)|] when
(is_bool_patt tru "true") && (is_bool_patt fal "false")
->
hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++
hov 2 (str "then " ++
hov 2 (pp_expr table (expr_needs_par the) env [] the)) ++ spc () ++
hov 2 (str "else " ++
hov 2 (pp_expr table (expr_needs_par els) env [] els)))
| _ -> raise Not_found
and pp_one_pat table env (ids,p,t) =
let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in
pp_gen_pat table (List.rev ids') env' p,
pp_expr table (expr_needs_par t) env' [] t
and pp_pat table env pv =
prvecti
(fun i x ->
let s1,s2 = pp_one_pat table env x in
hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++
if Int.equal i (Array.length pv - 1) then mt () else fnl ())
pv
and pp_function table 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(Tglob(r,_),MLrel 1,pv) when
not (is_coinductive (State.get_table table) r) && List.is_empty (get_record_fields (State.get_table table) r) &&
not (is_custom_match pv) ->
if not (ast_occurs 1 (MLcase(Tunknown,MLaxiom "",pv))) then
pr_binding (List.rev (List.tl bl)) ++
str " = function" ++ fnl () ++
v 0 (pp_pat table env' pv)
else
pr_binding (List.rev bl) ++
str " = match " ++ Id.print (List.hd bl) ++ str " with" ++ fnl () ++
v 0 (pp_pat table env' pv)
| _ ->
pr_binding (List.rev bl) ++
str " =" ++ fnl () ++ str " " ++
hov 2 (pp_expr table false env' [] t')
and pp_fix table par env i (ids,bl) args =
pp_par par
(v 0 (str "let rec " ++
prvect_with_sep
(fun () -> fnl () ++ str "and ")
(fun (fi,ti) -> Id.print fi ++ pp_function table env ti)
(Array.map2 (fun id b -> (id,b)) ids bl) ++
fnl () ++
hov 2 (str "in " ++ pp_apply (Id.print ids.(i)) false args)))
let cut2 () = brk (0,-100000) ++ brk (0,0)
let pp_val table e typ =
hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type table false [] typ ++
str " **)") ++ cut2 ()
let pp_Dfix table (rv,c,t) =
let names = Array.map
(fun r -> if is_inline_custom r then mt () else pp_global_name table Term r) rv
in
let rec pp init i =
if i >= Array.length rv then mt ()
else
let void = is_inline_custom rv.(i) ||
(not (is_custom rv.(i)) &&
match c.(i) with MLexn "UNUSED" -> true | _ -> false)
in
if void then pp init (i+1)
else
let def =
if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
else pp_function table (empty_env table ()) c.(i)
in
(if init then mt () else cut2 ()) ++
pp_val table names.(i) t.(i) ++
str (if init then "let rec " else "and ") ++ names.(i) ++ def ++
pp false (i+1)
in pp true 0
let pp_equiv table param_list name inst = function
| NoEquiv, _ -> mt ()
| Equiv kn, i ->
let r = { glob = GlobRef.IndRef (MutInd.make1 kn, i); inst } in
str " = " ++ pp_parameters param_list ++ pp_global table Type r
| RenEquiv ren, _ ->
str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
let pp_one_ind table prefix inst ip_equiv pl name cnames ctyps =
let pl = rename_tvars keywords pl in
let pp_constructor i typs =
(if Int.equal i 0 then mt () else fnl ()) ++
hov 3 (str "| " ++ cnames.(i) ++
(if List.is_empty typs then mt () else str " of ") ++
prlist_with_sep
(fun () -> spc () ++ str "* ") (pp_type table true pl) typs)
in
pp_parameters pl ++ str prefix ++ name ++
pp_equiv table pl name inst ip_equiv ++ str " =" ++
if Int.equal (Array.length ctyps) 0 then str " |"
else fnl () ++ v 0 (prvecti pp_constructor ctyps)
let pp_logical_ind packet =
pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++
fnl () ++
pp_comment (str "with constructors : " ++
prvect_with_sep spc Id.print packet.ip_consnames) ++
fnl ()
let pp_singleton table packet =
let name = pp_global_name table Type packet.ip_typename_ref in
let l = rename_tvars keywords packet.ip_vars in
hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
pp_type table false l (List.hd packet.ip_types.(0)) ++ fnl () ++
pp_comment (str "singleton inductive, whose constructor was " ++
Id.print packet.ip_consnames.(0)))
let pp_record table fields ip_equiv packet =
let ind = packet.ip_typename_ref in
let name = pp_global_name table Type ind in
let fieldnames = pp_fields table ind fields in
let l = List.combine fieldnames packet.ip_types.(0) in
let pl = rename_tvars keywords packet.ip_vars in
str "type " ++ pp_parameters pl ++ name ++
pp_equiv table pl name ind.inst ip_equiv ++ str " = { "++
hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ())
(fun (p,t) -> p ++ str " : " ++ pp_type table 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 table co ind =
let prefix = if co then "__" else "" in
let initkwd = str "type " in
let nextkwd = fnl () ++ str "and " in
let names =
Array.mapi (fun i p -> if p.ip_logical then mt () else
pp_global_name table Type p.ip_typename_ref)
ind.ind_packets
in
let cnames =
Array.mapi
(fun i p -> if p.ip_logical then [||] else
Array.mapi (fun j _ -> pp_global table Cons p.ip_consnames_ref.(j))
p.ip_types)
ind.ind_packets
in
let rec pp i kwd =
if i >= Array.length ind.ind_packets then mt ()
else
let ip = ind.ind_packets.(i).ip_typename_ref in
let ip_equiv = ind.ind_equiv, i in
let p = ind.ind_packets.(i) in
if is_custom ip then pp (i+1) kwd
else if p.ip_logical then pp_logical_ind p ++ pp (i+1) kwd
else
let inst = p.ip_typename_ref.inst in
kwd ++ (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
pp_one_ind table prefix inst ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++
pp (i+1) nextkwd
in
pp 0 initkwd
let pp_mind table i =
match i.ind_kind with
| Singleton -> pp_singleton table i.ind_packets.(0)
| Coinductive -> pp_ind table true i
| Record fields -> pp_record table fields (i.ind_equiv,0) i.ind_packets.(0)
| Standard -> pp_ind table false i
let pp_decl table = function
| Dtype (r,_,_) when is_inline_custom r -> mt ()
| Dterm (r,_,_) when is_inline_custom r -> mt ()
| Dind i -> pp_mind table i
| Dtype (r, l, t) ->
let name = pp_global_name table 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 table false l t
in
hov 2 (str "type " ++ ids ++ name ++ def)
| Dterm (r, a, t) ->
let def =
if is_foreign_custom r then str ": " ++ pp_type table false [] t ++ str " = \"" ++ str (find_custom r) ++ str "\""
else if is_custom r then str (" = " ^ find_custom r)
else pp_function table (empty_env table ()) a
in
let name = pp_global_name table Term r in
let expr_begin = if is_foreign_custom r then str "external " else str "let " in
let callback_def =
try
let alias =
match find_callback r with
| Some s -> str s
| None -> name
in
cut2 () ++ hov 0 ((str "let () = Stdlib.Callback.register \"") ++ alias ++ (str "\" ") ++ name)
with Not_found ->
mt()
in pp_val table name t ++ hov 0 (expr_begin ++ name ++ def ++ mt ()) ++ callback_def;
| Dfix (rv,defs,typs) ->
pp_Dfix table (rv,defs,typs)
let pp_spec table = function
| Sval (r,_) when is_inline_custom r -> mt ()
| Stype (r,_,_) when is_inline_custom r -> mt ()
| Sind i -> pp_mind table i
| Sval (r,t) ->
let def = pp_type table false [] t in
let name = pp_global_name table Term r in
hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
| Stype (r,vl,ot) ->
let name = pp_global_name table 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 " =" ++ spc () ++ 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 table false l t
in
hov 2 (str "type " ++ ids ++ name ++ def)
let rec pp_specif table = function
| (_,Spec (Sval _ as s)) -> pp_spec table s
| (l,Spec s) ->
(match Common.State.get_duplicate table (State.get_top_visible_mp table) l with
| None -> pp_spec table s
| Some ren ->
hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec table s) ++
fnl () ++ str "end" ++ fnl () ++
str ("include module type of struct include "^ren^" end"))
| (l,Smodule mt) ->
let def = pp_module_type table [] mt in
let name = pp_modname table (MPdot (State.get_top_visible_mp table, l)) in
hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++
(match Common.State.get_duplicate table (State.get_top_visible_mp table) l with
| None -> Pp.mt ()
| Some ren ->
fnl () ++
hov 1 (str ("module "^ren^" :") ++ spc () ++
str "module type of struct include " ++ name ++ str " end"))
| (l,Smodtype mt) ->
let def = pp_module_type table [] mt in
let name = pp_modname table (MPdot (State.get_top_visible_mp table, l)) in
hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
(match Common.State.get_duplicate table (State.get_top_visible_mp table) l with
| None -> Pp.mt ()
| Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
and pp_module_type table params = function
| MTident kn ->
pp_modname table kn
| MTfunsig (mbid, mt, mt') ->
let typ = pp_module_type table [] mt in
let name = pp_modname table (MPbound mbid) in
let def = pp_module_type table (MPbound mbid :: params) mt' in
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MTsig (mp, sign) ->
let l = State.with_visibility table mp params begin fun table ->
let try_pp_specif l x =
let px = pp_specif table x in
if Pp.ismt px then l else px::l
in
let l = List.fold_left try_pp_specif [] sign in
List.rev l
end in
str "sig" ++ fnl () ++
(if List.is_empty l then mt ()
else
v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
++ str "end"
| MTwith(mt,ML_With_type (rlv, 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 = { glob = GlobRef.ConstRef (Constant.make2 mp_w (Label.of_id l)); inst = rlv } in
let pp_w = State.with_visibility table mp_mt [] begin fun table ->
str " with type " ++ ids ++ pp_global table Type r
end in
pp_module_type table [] mt ++ pp_w ++ str " = " ++ pp_type table 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
let pp_w = State.with_visibility table mp_mt [] begin fun table ->
str " with module " ++ pp_modname table mp_w
end in
pp_module_type table [] mt ++ pp_w ++ str " = " ++ pp_modname table mp
let is_short = function MEident _ | MEapply _ -> true | _ -> false
let rec pp_structure_elem table = function
| (l,SEdecl d) ->
(match Common.State.get_duplicate table (State.get_top_visible_mp table) l with
| None -> pp_decl table d
| Some ren ->
v 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl table d) ++
fnl () ++ str "end" ++ fnl () ++ str ("include "^ren))
| (l,SEmodule m) ->
let typ =
if Common.State.get_phase table == Pre then
str ": " ++ pp_module_type table [] m.ml_mod_type
else mt ()
in
let def = pp_module_expr table [] m.ml_mod_expr in
let name = pp_modname table (MPdot (State.get_top_visible_mp table, l)) in
hov 1
(str "module " ++ name ++ typ ++ str " =" ++
(if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++
(match Common.State.get_duplicate table (State.get_top_visible_mp table) l with
| Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name
| None -> mt ())
| (l,SEmodtype m) ->
let def = pp_module_type table [] m in
let name = pp_modname table (MPdot (State.get_top_visible_mp table, l)) in
hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
(match Common.State.get_duplicate table (State.get_top_visible_mp table) l with
| None -> mt ()
| Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
and pp_module_expr table params = function
| MEident mp -> pp_modname table mp
| MEapply (me, me') ->
pp_module_expr table [] me ++ str "(" ++ pp_module_expr table [] me' ++ str ")"
| MEfunctor (mbid, mt, me) ->
let name = pp_modname table (MPbound mbid) in
let typ = pp_module_type table [] mt in
let def = pp_module_expr table (MPbound mbid :: params) me in
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MEstruct (mp, sel) ->
let l = State.with_visibility table mp params begin fun table ->
let try_pp_structure_elem l x =
let px = pp_structure_elem table x in
if Pp.ismt px then l else px::l
in
let l = List.fold_left try_pp_structure_elem [] sel in
List.rev l
end in
str "struct" ++ fnl () ++
(if List.is_empty l then mt ()
else
v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
++ str "end"
let rec prlist_sep_nonempty sep f = function
| [] -> mt ()
| [h] -> f h
| h::t ->
let e = f h in
let r = prlist_sep_nonempty sep f t in
if Pp.ismt e then r
else e ++ sep () ++ r
let do_struct table f s =
let modular = State.get_modular table in
let p =
if modular then
let ppl (mp, sel) = State.with_visibility table mp [] begin fun table ->
prlist_sep_nonempty cut2 (fun s -> f table s) sel
end in
List.map_left ppl s
else
let rec eval table = function
| [] -> []
| (mp, sel) :: l ->
State.with_visibility table mp [] begin fun table ->
let h = prlist_sep_nonempty cut2 (fun s -> f table s) sel in
h :: eval table l
end
in
eval table s
in
let p = prlist_sep_nonempty cut2 (fun x -> x) p in
v 0 p ++ fnl ()
let pp_struct table s = do_struct table (fun table e -> pp_structure_elem table e) s
let pp_signature table s = do_struct table (fun table e -> pp_specif table e) s
let file_naming state mp = file_of_modfile (State.get_table state) mp
let ocaml_descr = {
keywords = keywords;
file_suffix = ".ml";
file_naming = file_naming;
preamble = preamble;
pp_struct = pp_struct;
sig_suffix = Some ".mli";
sig_preamble = sig_preamble;
pp_sig = pp_signature;
pp_decl = pp_decl;
}