ocaml_printer.ml 8.41 KB
Newer Older
Mário Pereira's avatar
Mário Pereira committed
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
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

(** Printer for extracted OCaml code *)

open Compile
open Format
open Pmodule
open Theory
open Ident
open Pp

module Print = struct

  open ML

  let ocaml_keywords =
    ["and"; "as"; "assert"; "asr"; "begin";
     "class"; "constraint"; "do"; "done"; "downto"; "else"; "end";
     "exception"; "external"; "false"; "for"; "fun"; "function";
     "functor"; "if"; "in"; "include"; "inherit"; "initializer";
     "land"; "lazy"; "let"; "lor"; "lsl"; "lsr"; "lxor"; "match";
     "method"; "mod"; "module"; "mutable"; "new"; "object"; "of";
     "open"; "or"; "private"; "rec"; "sig"; "struct"; "then"; "to";
     "true"; "try"; "type"; "val"; "virtual"; "when"; "while"; "with";
     "raise";]

Mário Pereira's avatar
Mário Pereira committed
36
  let iprinter, aprinter =
Mário Pereira's avatar
Mário Pereira committed
37
    let isanitize = sanitizer char_to_alpha char_to_alnumus in
Mário Pereira's avatar
Mário Pereira committed
38
39
40
    let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
    create_ident_printer ocaml_keywords ~sanitizer:isanitize,
    create_ident_printer ocaml_keywords ~sanitizer:lsanitize
Mário Pereira's avatar
Mário Pereira committed
41
42
43
44
45

  let print_ident fmt id =
    let s = id_unique iprinter id in
    fprintf fmt "%s" s

Mário Pereira's avatar
Mário Pereira committed
46
47
48
49
50
51
  (* let print_lident = print_qident ~sanitizer:Strings.uncapitalize *)
  (* let print_uident = print_qident ~sanitizer:Strings.capitalize *)

  let print_tv fmt tv =
    fprintf fmt "'%s" (id_unique aprinter tv)

52
53
54
  let protect_on b s =
    if b then "(" ^^ s ^^ ")" else s

Mário Pereira's avatar
Mário Pereira committed
55
56
  let star fmt () = fprintf fmt " *@ "

57
58
  (** Types *)

59
  let rec print_ty ?(paren=false) fmt = function
Mário Pereira's avatar
Mário Pereira committed
60
61
62
63
64
    | Tvar id ->
       print_tv fmt id
    | Ttuple [] ->
       fprintf fmt "unit"
    | Ttuple tl ->
65
66
       fprintf fmt (protect_on paren "@[%a@]")
               (print_list star (print_ty ~paren:false)) tl
Mário Pereira's avatar
Mário Pereira committed
67
68
69
    | Tapp (ts, []) ->
       print_ident fmt ts
    | Tapp (ts, [ty]) ->
70
71
       fprintf fmt (protect_on paren "%a@ %a")
               (print_ty ~paren:true) ty print_ident ts
Mário Pereira's avatar
Mário Pereira committed
72
    | Tapp (ts, tl) ->
73
74
       fprintf fmt (protect_on paren "(%a)@ %a")
               (print_list comma (print_ty ~paren:false)) tl
Mário Pereira's avatar
Mário Pereira committed
75
76
77
               print_ident ts

  let print_vsty fmt (v, ty) =
78
79
80
81
82
83
84
    fprintf fmt "%a:@ %a" print_ident v (print_ty ~paren:false) ty

  let print_tv_arg = print_tv
  let print_tv_args fmt = function
    | []   -> ()
    | [tv] -> fprintf fmt "%a@ " print_tv_arg tv
    | tvl  -> fprintf fmt "(%a)@ " (print_list comma print_tv_arg) tvl
Mário Pereira's avatar
Mário Pereira committed
85
86
87
88

  let print_vs_arg fmt vs =
    fprintf fmt "@[(%a)@]" print_vsty vs

Mário Pereira's avatar
Mário Pereira committed
89
90
91
92
93
94
95
96
97
98
99
100
101
  let print_path =
    print_list dot pp_print_string (* point-free *)

  let print_path_id fmt = function
    | [], id -> print_ident fmt id
    | p, id  -> fprintf fmt "%a.%a" print_path p print_ident id

  let print_theory_name fmt th =
    print_path_id fmt (th.th_path, th.th_name)

  let print_module_name fmt m =
    print_theory_name fmt m.mod_theory

102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
  let rec print_pat fmt = function
    | Pwild ->
       fprintf fmt "_"
    | Pident id ->
       print_ident fmt id
    | Pas (p, id) ->
       fprintf fmt "%a as %a" print_pat p print_ident id
    | Por (p1, p2) ->
       fprintf fmt "%a | %a" print_pat p1 print_pat p2
    | Ptuple pl ->
       fprintf fmt "(%a)" (print_list comma print_pat) pl
    | Papp (id, []) ->
       print_ident fmt id
    | Papp (id, [p]) ->
       fprintf fmt "%a %a" print_ident id print_pat p
    | Papp (id, pl) ->
       fprintf fmt "%a (%a)" print_ident id (print_list comma print_pat) pl
    | Precord fl ->
       let print_field fmt (id, p) =
         fprintf fmt "%a = %a" print_ident id print_pat p
       in
       fprintf fmt "{ %a }" (print_list semi print_field) fl

125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
  let print_const fmt c =
    let n = Number.compute_int c in
    let m = BigInt.to_int n in
    fprintf fmt "%d" m

  (** Expressions *)

  let extract_op {id_string = s} =
    try Some (Strings.remove_prefix "infix " s) with Not_found ->
    try Some (Strings.remove_prefix "prefix " s) with Not_found ->
    None

  let print_apply fmt s vl =
    match extract_op s, vl with
    | Some o, [t1; t2] ->
       fprintf fmt "@[<hov 1>%a %s %a@]"
         print_ident t1 o print_ident t2
142
143
    | _, [] ->
      print_ident fmt s
144
145
146
147
    | _, tl ->
       fprintf fmt "@[<hov 2>%a %a@]"
         print_ident s (print_list space print_ident) tl

Mário Pereira's avatar
Mário Pereira committed
148
  let rec print_enode fmt = function
149
150
    | Econst c ->
       fprintf fmt "%a" print_const c
Mário Pereira's avatar
Mário Pereira committed
151
152
    | Eident id ->
       print_ident fmt id
Mário Pereira's avatar
Mário Pereira committed
153
154
    | Elet (id, e1, e2) ->
       fprintf fmt "@[<hov 2>let @[%a@] =@ @[%a@]@] in@ %a"
155
156
157
         print_ident id print_expr e1 print_expr e2
    | Eabsurd ->
       fprintf fmt "assert false (* absurd *)"
158
159
    | Eapp (s, vl) ->
       print_apply fmt s vl
160
161
162
    | Ematch (e, pl) ->
       fprintf fmt "@[begin match @[%a@] with@\n@[<hov>%a@] end@]"
         print_expr e (print_list newline print_branch) pl
163
164
    | Eblock [] ->
       fprintf fmt "()"
165
    | _ -> (* TODO *) assert false
Mário Pereira's avatar
Mário Pereira committed
166

167
168
169
  and print_branch fmt (p, e) =
    fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_expr e

Mário Pereira's avatar
Mário Pereira committed
170
  and print_expr fmt e =
Mário Pereira's avatar
Mário Pereira committed
171
172
    print_enode fmt e.e_node

173
  let print_type_decl fmt (id, args, tydef) =
174
175
    let print_constr fmt (id, cs_args) =
      match cs_args with
176
177
178
179
180
181
182
      | [] ->
         fprintf fmt "@[<hov 4>| %a@]"
                 print_ident id (* FIXME: first letter must be uppercase
                                       -> print_uident *)
      | l ->
         fprintf fmt "@[<hov 4>| %a of %a@]"
                 print_ident id (* FIXME: print_uident *)
183
                 (print_list star (print_ty ~paren:false)) l in
184
185
186
187
188
189
    let print_field fmt (is_mutable, id, ty) =
      fprintf fmt "%s%a: %a;"
              (if is_mutable then "mutable " else "")
              print_ident id
              (print_ty ~paren:false) ty
    in
190
191
192
193
194
    let print_def fmt = function
      | Dabstract ->
         ()
      | Ddata csl ->
         fprintf fmt " =@\n%a" (print_list newline print_constr) csl
195
196
      | Drecord fl ->
         fprintf fmt " = {@\n%a@\n}" (print_list newline print_field) fl
197
      | Dalias ty ->
198
         fprintf fmt " =@ %a" (print_ty ~paren:false) ty in
199
200
201
202
203
204
205
    fprintf fmt "@[<hov 2>%s %a%a%a@]"
            (if true then "type" else "and") (* FIXME: mutual recursive types *)
            print_tv_args args
            print_ident id  (* FIXME: first letter must be lowercase
                                   -> print_lident *)
            print_def tydef

Mário Pereira's avatar
Mário Pereira committed
206
  let print_decl fmt = function
Mário Pereira's avatar
Mário Pereira committed
207
208
    | Dlet (isrec, [id, vl, e]) ->
       fprintf fmt "@[<hov 2>%s %a@ %a =@ %a@]"
Mário Pereira's avatar
Mário Pereira committed
209
210
               (if isrec then "let rec" else "let")
               print_ident id
Mário Pereira's avatar
Mário Pereira committed
211
               (print_list space print_vs_arg) vl
Mário Pereira's avatar
Mário Pereira committed
212
213
               print_expr e;
       fprintf fmt "@\n@\n"
214
215
216
    | Dtype dl ->
       print_list newline print_type_decl fmt dl;
       fprintf fmt "@\n@\n"
217
218
219
220
221
    | Dexn (id, None) ->
       fprintf fmt "exception %a@\n@\n" print_ident id
    | Dexn (id, Some t) ->
       fprintf fmt "@[<hov 2>exception %a of %a@]@\n@\n"
               print_ident id (print_ty ~paren:true) t
222
    | _ -> (* TODO *) assert false
Mário Pereira's avatar
Mário Pereira committed
223
224
225

end

226
227
228
229
230
231
232
233
234
235
236
237
238
let extract_module pargs ?old fmt ({mod_theory = th} as m) =
  ignore (pargs);
  ignore (old);
  ignore (m);
  let info = {
    info_syn          = pargs.Pdriver.syntax;
    info_convert      = pargs.Pdriver.converter;
    info_current_th   = th;
    info_current_mo   = Some m;
    info_th_known_map = th.th_known;
    info_mo_known_map = m.mod_known;
    info_fname        = None; (* TODO *)
  } in
Mário Pereira's avatar
Mário Pereira committed
239
240
241
  fprintf fmt
    "(* This file has been generated from Why3 module %a *)@\n@\n"
    Print.print_module_name m;
242
  let mdecls = Translate.module_ info m in
Mário Pereira's avatar
Mário Pereira committed
243
244
  print_list nothing Print.print_decl fmt mdecls;
  fprintf fmt "@."
245

246
247
248
249
250
251
252
253
let fg ?fname m =
  let mod_name = m.Pmodule.mod_theory.Theory.th_name.id_string in
  match fname with
  | None   -> mod_name ^ ".ml"
  | Some f -> (Filename.remove_extension f) ^ "__" ^ mod_name ^ ".ml"

let () = Pdriver.register_printer "ocaml" ~desc:"printer for OCaml code" fg extract_module

254
255
(*
 * Local Variables:
256
 * compile-command: "make -C ../.. -j3 bin/why3extract.opt"
257
258
 * End:
 *)