← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to plugins/extraction/ocaml.ml

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
plugins/extraction/ocaml.ml
1
1
(************************************************************************)
2
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
3
 
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 
3
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
4
4
(*   \VV/  **************************************************************)
5
5
(*    //   *      This file is distributed under the terms of the       *)
6
6
(*         *       GNU Lesser General Public License Version 2.1        *)
7
7
(************************************************************************)
8
8
 
9
 
(*i $Id: ocaml.ml 14010 2011-04-15 16:05:07Z letouzey $ i*)
 
9
(*i $Id: ocaml.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
10
10
 
11
11
(*s Production of Ocaml syntax. *)
12
12
 
113
113
  let s = find_custom r in
114
114
  String.sub s 1 (String.length s - 2)
115
115
 
116
 
exception NoRecord
117
 
 
118
 
let find_projections = function Record l -> l | _ -> raise NoRecord
 
116
let get_ind = function
 
117
  | IndRef _ as r -> r
 
118
  | ConstructRef (ind,_) -> IndRef ind
 
119
  | _ -> assert false
 
120
 
 
121
let pp_one_field r i = function
 
122
  | Some r -> pp_global Term r
 
123
  | None -> pp_global Type (get_ind r) ++ str "__" ++ int i
 
124
 
 
125
let pp_field r fields i = pp_one_field r i (List.nth fields i)
 
126
 
 
127
let pp_fields r fields = list_map_i (pp_one_field r) 0 fields
119
128
 
120
129
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
121
130
    are needed or not. *)
202
211
    | MLcons (_,r,[]) ->
203
212
        assert (args=[]);
204
213
        pp_global Cons r
205
 
    | MLcons ({c_kind = Record projs}, r, args') ->
 
214
    | MLcons ({c_kind = Record fields}, r, args') ->
206
215
        assert (args=[]);
207
 
        pp_record_pat (projs, List.map (pp_expr true env []) args')
 
216
        pp_record_pat (pp_fields r fields, List.map (pp_expr true env []) args')
208
217
    | MLcons (_,r,[arg1;arg2]) when is_infix r ->
209
218
        assert (args=[]);
210
219
        pp_par par
234
243
          (pp_expr false env [] t)
235
244
        in
236
245
        (try
237
 
           let projs = find_projections info.m_kind in
238
 
           let (_, ids, c) = pv.(0) in
 
246
           (* First, can this match be printed as a mere record projection ? *)
 
247
           let fields =
 
248
             match info.m_kind with Record f -> f | _ -> raise Impossible
 
249
           in
 
250
           let (r, ids, c) = pv.(0) in
239
251
           let n = List.length ids in
 
252
           let free_of_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
 
253
           let proj_hd i =
 
254
             pp_expr true env [] t ++ str "." ++ pp_field r fields i
 
255
           in
240
256
           match c with
241
 
             | MLrel i when i <= n ->
242
 
                 apply (pp_par par' (pp_expr true env [] t ++ str "." ++
243
 
                                     pp_global Term (List.nth projs (n-i))))
244
 
             | MLapp (MLrel i, a) when i <= n ->
245
 
                 if List.exists (ast_occurs_itvl 1 n) a
246
 
                 then raise NoRecord
247
 
                 else
248
 
                   let ids,env' = push_vars (List.rev_map id_of_mlid ids) env
249
 
                   in
250
 
                   (pp_apply
251
 
                      (pp_expr true env [] t ++ str "." ++
252
 
                       pp_global Term (List.nth projs (n-i)))
253
 
                      par ((List.map (pp_expr true env' []) a) @ args))
254
 
             | _ -> raise NoRecord
255
 
         with NoRecord ->
 
257
             | MLrel i when i <= n -> apply (pp_par par' (proj_hd (n-i)))
 
258
             | MLapp (MLrel i, a) when (i <= n) && (free_of_patvar a) ->
 
259
               let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
 
260
               (pp_apply (proj_hd (n-i))
 
261
                  par ((List.map (pp_expr true env' []) a) @ args))
 
262
             | _ -> raise Impossible
 
263
         with Impossible ->
 
264
           (* Second, can this match be printed as a let-in ? *)
256
265
           if Array.length pv = 1 then
257
266
             let s1,s2 = pp_one_pat env info pv.(0) in
258
267
             apply
263
272
                         ++ spc () ++ str "in") ++
264
273
                      spc () ++ hov 0 s2)))
265
274
           else
 
275
             (* Otherwise, standard match *)
266
276
             apply
267
277
               (pp_par par'
268
278
                  (try pp_ifthenelse par' env expr pv
283
293
        pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
284
294
 
285
295
 
286
 
and pp_record_pat (projs, args) =
 
296
and pp_record_pat (fields, args) =
287
297
   str "{ " ++
288
298
   prlist_with_sep (fun () -> str ";" ++ spc ())
289
 
     (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a)
290
 
     (List.combine projs args) ++
 
299
     (fun (f,a) -> f ++ str " =" ++ spc () ++ a)
 
300
     (List.combine fields args) ++
291
301
   str " }"
292
302
 
293
303
and pp_ifthenelse par env expr pv = match pv with
304
314
and pp_one_pat env info (r,ids,t) =
305
315
  let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
306
316
  let expr = pp_expr (expr_needs_par t) env' [] t in
307
 
  try
308
 
    let projs = find_projections info.m_kind in
309
 
    pp_record_pat (projs, List.rev_map pr_id ids), expr
310
 
  with NoRecord ->
311
 
    (match List.rev ids with
312
 
      | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2
313
 
      | [] -> pp_global Cons r
314
 
      | ids ->
 
317
  let patt = match info.m_kind with
 
318
    | Record fields ->
 
319
      pp_record_pat (pp_fields r fields, List.rev_map pr_id ids)
 
320
    | _ -> match List.rev ids with
 
321
        | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2
 
322
        | [] -> pp_global Cons r
 
323
        | ids ->
315
324
          (* hack Extract Inductive prod *)
316
325
          (if str_global Cons r = "" then mt () else pp_global Cons r ++ spc ())
317
 
           ++ pp_boxed_tuple pr_id ids),
318
 
    expr
 
326
          ++ pp_boxed_tuple pr_id ids
 
327
  in
 
328
  patt, expr
319
329
 
320
330
and pp_pat env info pv =
321
331
  let factor_br, factor_set = try match info.m_same with
448
458
         pp_comment (str "singleton inductive, whose constructor was " ++
449
459
                     pr_id packet.ip_consnames.(0)))
450
460
 
451
 
let pp_record kn projs ip_equiv packet =
452
 
  let name = pp_global Type (IndRef (mind_of_kn kn,0)) in
453
 
  let projnames = List.map (pp_global Term) projs in
454
 
  let l = List.combine projnames packet.ip_types.(0) in
 
461
let pp_record kn fields ip_equiv packet =
 
462
  let ind = IndRef (mind_of_kn kn,0) in
 
463
  let name = pp_global Type ind in
 
464
  let fieldnames = pp_fields ind fields in
 
465
  let l = List.combine fieldnames packet.ip_types.(0) in
455
466
  let pl = rename_tvars keywords packet.ip_vars in
456
467
  str "type " ++ pp_parameters pl ++ name ++
457
468
  pp_equiv pl name ip_equiv ++ str " = { "++
512
523
  match i.ind_kind with
513
524
    | Singleton -> pp_singleton kn i.ind_packets.(0)
514
525
    | Coinductive -> pp_ind true kn i
515
 
    | Record projs ->
516
 
        pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0)
 
526
    | Record fields -> pp_record kn fields (i.ind_equiv,0) i.ind_packets.(0)
517
527
    | Standard -> pp_ind false kn i
518
528
 
519
529
let pp_decl = function