1 (************************************************************************)
2 (* v * The Coq Proof Assistant / The Coq Development Team *)
3 (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
4 (* \VV/ **************************************************************)
5 (* // * This file is distributed under the terms of the *)
6 (* * GNU Lesser General Public License Version 2.1 *)
7 (************************************************************************)
9 (*i $Id: ocaml.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
11 (*s Production of Ocaml syntax. *)
13 open OcamlExtractionTable
20 (*s Some utility functions. *)
24 if String.length s < 2 || s.[1]<>'\''
28 let pp_tuple_light status f = function
30 | [x] -> f status true x
33 prlist_with_sep_status status
34 (fun () -> str "," ++ spc ()) (fun status -> f status false) l in
35 status, pp_par true res
37 let pp_tuple status f = function
42 prlist_with_sep_status status (fun () -> str "," ++ spc ()) f l in
43 status,pp_par true res
45 let pp_boxed_tuple f = function
48 | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
50 let pp_abst = function
53 str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++
57 (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
59 (*s Ocaml renaming issues. *)
62 List.fold_right Idset.add
63 [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
64 "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
65 "for"; "fun"; "function"; "functor"; "if"; "in"; "include";
66 "inherit"; "initializer"; "lazy"; "let"; "match"; "method";
67 "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
68 "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
69 "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
70 "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
74 set_keywords keywords;;
76 let pp_open status filename =
77 let status,res = modname_of_filename status true filename in
78 status, str ("open " ^ res ^ "\n") ++ fnl ()
80 (*s The pretty-printer for Ocaml syntax*)
82 (* Beware of the side-effects of [pp_global] and [pp_modname].
83 They are used to update table of content for modules. Many [let]
84 below should not be altered since they force evaluation order.
87 let str_global status k r =
88 (*CSC: if is_inline_custom r then find_custom r else*) Common.pp_global status k r
90 let pp_global status k r =
91 let status,res = str_global status k r in
95 let pp_modname mp = str (Common.pp_module mp)
99 (let s = find_custom r in
100 let l = String.length s in
101 l >= 2 && s.[0] = '(' && s.[l-1] = ')')
104 let s = find_custom r in
105 String.sub s 1 (String.length s - 2)
108 let pp_one_field status _r _i r = pp_global status Term r
110 let pp_field status r fields i = pp_one_field status r i (List.nth fields i)
112 let pp_fields status r fields =
113 list_map_i_status status (fun status -> pp_one_field status r) 0 fields
115 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
116 are needed or not. *)
118 let rec pp_type status par vl t =
119 let rec pp_rec status par = function
120 | Tmeta _ | Tvar' _ | Taxiom -> assert false
121 | Tvar i -> (try status,pp_tvar (List.nth vl (pred i))
122 with _ -> status,(str "'a" ++ int i))
124 | Tglob (r,[a1;a2]) when is_infix r ->
125 pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
127 | Tglob (r,[]) -> pp_global status Type r
129 | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" ->
130 pp_tuple_light pp_rec l
133 let status,res = pp_tuple_light status pp_rec l in
134 let status,res2 = pp_global status Type r in
135 status,res ++ spc () ++ res2
137 let status,res = pp_rec status true t1 in
138 let status,res2 = pp_rec status false t2 in
139 status,pp_par par (res ++ spc () ++ str "->" ++ spc () ++ res2)
140 | Tdummy _ -> status,str "__"
141 | Tunknown -> status,str "__"
143 let status,res = pp_rec status par t in
146 (*s Pretty-printing of expressions. [par] indicates whether
147 parentheses are needed or not. [env] is the list of names for the
148 de Bruijn variables. [args] is the list of collected arguments
149 (already pretty-printed). *)
151 let is_ifthenelse = function
153 | [|(r1,[],_);(r2,[],_)|] ->
154 (try (find_custom r1 = "true") && (find_custom r2 = "false")
155 with Not_found -> false)*)
158 let expr_needs_par = function
160 | MLcase (_,_,[|_|]) -> false
161 | MLcase (_,_,pv) -> not (is_ifthenelse pv)
164 let rec pp_expr status par env args =
165 let par' = args <> [] || par
166 and apply st = pp_apply st par args in
169 let id = get_db_name n env in status,apply (pr_id id)
171 let status,stl = map_status status (fun status -> pp_expr status true env []) args' in
172 pp_expr status par env (stl @ args) f
174 let fl,a' = collect_lams a in
175 let fl = List.map id_of_mlid fl in
176 let fl,env' = push_vars fl env in
177 let status,res = pp_expr status false env' [] a' in
178 let st = (pp_abst (List.rev fl) ++ res) in
179 status,apply (pp_par par' st)
180 | MLletin (id,a1,a2) ->
181 let i,env' = push_vars [id_of_mlid id] env in
182 let pp_id = pr_id (List.hd i) in
183 let status,pp_a1 = pp_expr status false env [] a1 in
185 pp_expr status (not par && expr_needs_par a2) env' [] a2 in
192 (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++
193 spc () ++ str "in") ++
194 spc () ++ hov 0 pp_a2)))
197 let args = list_skipn (projection_arity status r) args in
198 let record = List.hd args in
199 let status,res = pp_global status Term r in
200 status,pp_apply (record ++ str "." ++ res) par (List.tl args)
202 let status,res = pp_global status Term r in
204 (*CSC: | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c*)
205 | MLcons ({c_kind = Coinductive},r,[]) ->
207 let status,res = pp_global status Cons r in
208 status,pp_par par (str "lazy " ++ res)
209 | MLcons ({c_kind = Coinductive},r,args') ->
212 pp_tuple status (fun status -> pp_expr status true env []) args' in
213 let status,res = pp_global status Cons r in
215 pp_par par (str "lazy (" ++ res ++ spc() ++ tuple ++str ")")
218 pp_global status Cons r
219 | MLcons ({c_kind = Record fields}, r, args') ->
221 let status,res = pp_fields status r fields in
223 map_status status (fun status -> pp_expr status true env []) args' in
224 status,pp_record_pat (res, res2)
225 (*CSC: | MLcons (_,r,[arg1;arg2]) when is_infix r ->
228 ((pp_expr status true env [] arg1) ++ str (get_infix r) ++
229 (pp_expr status true env [] arg2))*)
230 | MLcons (_,r,args') ->
233 pp_tuple status (fun status -> pp_expr status true env []) args' in
234 let status,res = str_global status Cons r in
235 if res = "" (* hack Extract Inductive prod *)
238 let status,res = pp_global status Cons r in
239 status,pp_par par (res ++ spc () ++ tuple)
240 (*CSC: | MLcase (_, t, pv) when is_custom_match pv ->
241 let mkfun (_,ids,e) =
242 if ids <> [] then named_lams (List.rev ids) e
243 else dummy_lams (ast_lift 1 e) 1
248 (str (find_custom_match pv) ++ fnl () ++
249 prvect (fun tr -> pp_expr status true env [] (mkfun tr) ++ fnl ()) pv
250 ++ pp_expr status true env [] t)))*)
251 | MLcase (info, t, pv) ->
252 let status,expr = if info.m_kind = Coinductive then
253 let status,res = pp_expr status true env [] t in
254 status,(str "Lazy.force" ++ spc () ++ res)
256 (pp_expr status false env [] t)
259 (* First, can this match be printed as a mere record projection ? *)
261 match info.m_kind with Record f -> f | _ -> raise Impossible
263 let (r, ids, c) = pv.(0) in
264 let n = List.length ids in
265 let free_of_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
266 let proj_hd status i =
267 let status,res = pp_expr status true env [] t in
268 let status,res2 = pp_field status r fields i in
269 status,res ++ str "." ++ res2
272 | MLrel i when i <= n ->
273 let status,res = proj_hd status (n-i) in
274 status,apply (pp_par par' res)
275 | MLapp (MLrel i, a) when (i <= n) && (free_of_patvar a) ->
276 let _ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
277 let status,res = proj_hd status (n-i) in
279 map_status status (fun status -> pp_expr status true env' []) a
281 status,(pp_apply res par (res2 @ args))
282 | _ -> raise Impossible
284 (* Second, can this match be printed as a let-in ? *)
285 if Array.length pv = 1 then
286 let status,s1,s2 = pp_one_pat status env info pv.(0) in
292 (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr)
293 ++ spc () ++ str "in") ++
294 spc () ++ hov 0 s2)))
297 try status,pp_ifthenelse par' env expr pv
299 let status,res = pp_pat status env info pv in
301 v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++ res)
303 (* Otherwise, standard match *)
305 apply (pp_par par' res))
306 | MLfix (i,ids,defs) ->
307 let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
308 pp_fix status par env' i (Array.of_list (List.rev ids'),defs) args
310 (* An [MLexn] may be applied, but I don't really care. *)
311 status,pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
313 status,str "__" (*An [MLdummy] may be applied, but I don't really care.*)
315 let status,res = pp_expr status true env [] a in
316 status,pp_apply (str "Obj.magic") par (res :: args)
318 status,pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
321 and pp_record_pat (fields, args) =
323 prlist_with_sep (fun () -> str ";" ++ spc ())
324 (fun (f,a) -> f ++ str " =" ++ spc () ++ a)
325 (List.combine fields args) ++
328 and pp_ifthenelse _par _env _expr pv = match pv with
329 (*CSC: | [|(tru,[],the);(fal,[],els)|] when
330 (find_custom tru = "true") && (find_custom fal = "false")
332 hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++
333 hov 2 (str "then " ++
334 hov 2 (pp_expr status (expr_needs_par the) env [] the)) ++ spc () ++
335 hov 2 (str "else " ++
336 hov 2 (pp_expr status (expr_needs_par els) env [] els)))*)
337 | _ -> raise Not_found
339 and pp_one_pat status env info (r,ids,t) =
340 let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
341 let status,expr = pp_expr status (expr_needs_par t) env' [] t in
342 let status,patt = match info.m_kind with
344 let status,res = pp_fields status r fields in
345 status,pp_record_pat (res, List.rev_map pr_id ids)
346 | _ -> match List.rev ids with
347 (*CSC: | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2*)
348 | [] -> pp_global status Cons r
350 (* hack Extract Inductive prod *)
351 let status,res = str_global status Cons r in
353 if res = "" then status,mt()
355 let status,res = pp_global status Cons r in
356 status, res ++ spc () in
357 status,res2 ++ pp_boxed_tuple pr_id ids
361 and pp_pat status env info pv =
362 let factor_br, factor_set = try match info.m_same with
364 let i = Intset.choose ints in
365 branch_as_fun info.m_typs pv.(i), ints
367 let i = Intset.choose ints in
368 ast_pop (branch_as_cst pv.(i)), ints
369 | BranchNone -> MLdummy, Intset.empty
370 with _ -> MLdummy, Intset.empty
372 let last = Array.length pv - 1 in
374 prvecti_status status
375 (fun status i x -> if Intset.mem i factor_set then status,mt () else
376 let status,s1,s2 = pp_one_pat status env info x in
378 hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++
379 if i = last && Intset.is_empty factor_set then mt () else fnl ())
383 if Intset.is_empty factor_set then status,mt () else
384 let par = expr_needs_par factor_br in
385 match info.m_same with
387 let ids, env' = push_vars [anonymous_name] env in
388 let status,res = pp_expr status par env' [] factor_br in
389 status,hv 2 (str "| " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
392 let status,res = pp_expr status par env [] factor_br in
393 status,hv 2 (str "| _ ->" ++ spc () ++ hov 2 res)
394 | BranchNone -> status,mt ()
398 and pp_function status env t =
399 let bl,t' = collect_lams t in
400 let bl,env' = push_vars (List.map id_of_mlid bl) env in
402 | MLcase(i,MLrel 1,pv) when
403 i.m_kind = Standard (*CSC:&& not (is_custom_match pv)*) ->
404 if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
405 let status,res = pp_pat status env' i pv in
406 status,pr_binding (List.rev (List.tl bl)) ++
407 str " = function" ++ fnl () ++ v 0 res
409 let status,res = pp_pat status env' i pv in
411 pr_binding (List.rev bl) ++
412 str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
415 let status,res = pp_expr status false env' [] t' in
417 pr_binding (List.rev bl) ++
418 str " =" ++ fnl () ++ str " " ++
421 (*s names of the functions ([ids]) are already pushed in [env],
422 and passed here just for convenience. *)
424 and pp_fix status par env i (ids,bl) args =
426 prvect_with_sep_status status
427 (fun () -> fnl () ++ str "and ")
428 (fun status (fi,ti) ->
429 let status,res = pp_function status env ti in
430 status, pr_id fi ++ res)
431 (array_map2 (fun id b -> (id,b)) ids bl)
435 (v 0 (str "let rec " ++ res ++ fnl () ++
436 hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
438 let pp_val status e typ =
439 let status,res = pp_type status false [] typ in
441 hov 4 (str "(** val " ++ e ++ str " :" ++ spc ()++res++ str " **)") ++ fnl ()
443 (*s Pretty-printing of [Dfix] *)
445 let pp_Dfix status (rv,c,t) =
446 let status,names = array_map_status status
447 (fun status r -> (*CSC:if is_inline_custom r then mt () else*) pp_global status Term r) rv
449 let rec pp status init i =
450 if i >= Array.length rv then
451 (if init then failwith "empty phrase" else status,mt ())
453 let void = false(*CSC:is_inline_custom rv.(i)*) ||
454 (not false(*CSC:(is_custom rv.(i))*) && c.(i) = MLexn "UNUSED")
456 if void then pp status init (i+1)
459 (*CSC:if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
460 else*) pp_function status (empty_env status) c.(i) in
461 let status,res = pp_val status names.(i) t.(i) in
462 let status,res2 = pp status false (i+1) in
464 (if init then mt () else fnl ()) ++ res ++
465 str (if init then "let rec " else "and ") ++ names.(i) ++ def ++ res2
468 (*s Pretty-printing of inductive types declaration. *)
470 let pp_comment s = str "(* " ++ s ++ str " *)"
472 let pp_one_ind status prefix pl name cnames ctyps =
473 let pl = rename_tvars keywords pl in
474 let pp_constructor status i typs =
476 prlist_with_sep_status status
477 (fun () -> spc () ++ str "* ") (fun status -> pp_type status true pl) typs
480 (if i=0 then mt () else fnl ()) ++
481 hov 3 (str "| " ++ cnames.(i) ++
482 (if typs = [] then mt () else str " of ") ++ res) in
484 if Array.length ctyps = 0 then status,str " unit (* empty inductive *)"
486 let status,res = prvecti_status status pp_constructor ctyps in
487 status, fnl () ++ v 0 res
490 pp_parameters pl ++ str prefix ++ name ++
493 let pp_logical_ind packet =
494 pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
496 pp_comment (str "with constructors : " ++
497 prvect_with_sep spc pr_id packet.ip_consnames) ++
500 let pp_singleton status packet =
501 let status,name = pp_global status Type packet.ip_reference in
502 let l = rename_tvars keywords packet.ip_vars in
503 let status,res = pp_type status false l (List.hd packet.ip_types.(0)) in
505 hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
507 pp_comment (str "singleton inductive, whose constructor was " ++
508 pr_id packet.ip_consnames.(0)))
510 let pp_record status fields packet =
511 let ind = packet.ip_reference in
512 let status,name = pp_global status Type ind in
513 let status,fieldnames = pp_fields status ind fields in
514 let l = List.combine fieldnames packet.ip_types.(0) in
515 let pl = rename_tvars keywords packet.ip_vars in
517 prlist_with_sep_status status (fun () -> str ";" ++ spc ())
519 let status,res = pp_type status true pl t in
520 status, p ++ str " : " ++ res) l in
522 str "type " ++ pp_parameters pl ++ name ++ str " = { "++ hov 0 res ++ str " }"
524 let pp_coind pl name =
525 let pl = rename_tvars keywords pl in
526 pp_parameters pl ++ name ++ str " = " ++
527 pp_parameters pl ++ str "__" ++ name ++ str " Lazy.t" ++
530 let pp_ind status co ind =
531 let prefix = if co then "__" else "" in
532 let some = ref false in
533 let init= ref (str "type ") in
535 array_map_status status
537 if p.ip_logical then status,mt ()
538 else pp_global status Type p.ip_reference)
542 array_map_status status
543 (fun status p -> if p.ip_logical then status,[||] else
544 array_mapi_status status
545 (fun status j _ -> pp_global status Cons p.ip_consreferences.(j))
549 let rec pp status i =
550 if i >= Array.length ind.ind_packets then status,mt ()
552 let p = ind.ind_packets.(i) in
554 let ip = assert false(*CSC: (mind_of_kn kn,i)*) in
555 if is_custom (IndRef ip) then pp (i+1)
559 let status,res = pp status (i+1) in
560 status, pp_logical_ind p ++ res
564 init := (fnl () ++ str "and ");
567 status prefix p.ip_vars names.(i) cnames.(i) p.ip_types in
568 let status,res2 = pp status (i+1) in
571 (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
576 let st = pp status 0 in if !some then st else failwith "empty phrase"
579 (*s Pretty-printing of a declaration. *)
581 let pp_mind status i =
582 match i.ind_kind with
583 | Singleton -> pp_singleton status i.ind_packets.(0)
584 | Coinductive -> pp_ind status true i
585 | Record fields -> pp_record status fields i.ind_packets.(0)
586 | Standard -> pp_ind status false i
588 let pp_decl status = function
589 (*CSC: | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
590 | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase"*)
591 | Dind i -> pp_mind status i
593 let status,name = pp_global status Type r in
594 let l = rename_tvars keywords l in
595 let ids, (status, def) =
597 let ids,s = find_type_custom r in
598 pp_string_parameters ids, str "=" ++ spc () ++ str s
601 if t = Taxiom then status, str "(* AXIOM TO BE REALIZED *)"
603 let status,res = pp_type status false l t in
604 status, str "=" ++ spc () ++ res
606 status, hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
608 let status,name = pp_global status Term r in
610 (*if is_custom r then str (" = " ^ find_custom r)
611 else*) if is_projection status r then
613 (prvect str (Array.make (projection_arity status r) " _")) ++
614 str " x = x." ++ name
616 let status,res = pp_function status (empty_env status) a in
619 let status,res = pp_val status name t in
620 status, res ++ hov 0 (str "let " ++ name ++ def)
621 | Dfix (rv,defs,typs) ->
622 pp_Dfix status (rv,defs,typs)
624 let pp_spec status = function
625 (* | Sval (r,_) when is_inline_custom r -> failwith "empty phrase"
626 | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase"*)
627 | Sind i -> pp_mind status i
629 let status,def = pp_type status false [] t in
630 let status,name = pp_global status Term r in
631 status, hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
633 let status, name = pp_global status Type r in
634 let l = rename_tvars keywords vl in
635 let status, ids, def =
638 let ids, s = find_type_custom r in
639 pp_string_parameters ids, str "= " ++ str s
641 let ids = pp_parameters l in
643 | None -> status, ids, mt ()
644 | Some Taxiom -> status, ids, str "(* AXIOM TO BE REALIZED *)"
646 let status,res = pp_type status false l t in
647 status, ids, str "=" ++ spc () ++ res
649 status, hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
651 let pp_decl status d =
652 try pp_decl status d with Failure "empty phrase" -> status, mt ()