why3pp.ml 15.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2019   --   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.                           *)
(*                                                                  *)
(********************************************************************)

BECKER Benedikt's avatar
BECKER Benedikt committed
12 13 14 15 16 17 18 19
module LatexInd (Conf: sig val prefix: string val flatten_applies : bool val comment_macros : bool end) = struct

  open Format
  open Why3
  open Ptree
  open Ident

  open Conf
BECKER Benedikt's avatar
BECKER Benedikt committed
20 21 22

  let sanitize =
    let my_char_to_alpha = function
BECKER Benedikt's avatar
BECKER Benedikt committed
23
      | '_' -> ""
24
      | c -> char_to_alpha c
BECKER Benedikt's avatar
BECKER Benedikt committed
25
    in
26 27
    sanitizer my_char_to_alpha my_char_to_alpha

28 29 30 31 32 33
  let sanitize_op = function
    | "<>" -> "\\neq"
    | "^" -> "\\string^"
    | "++" -> "\\mathbin{+\\mkern-10mu+}"
    | s -> s

34
  (** Optionally extract trailing numbers and quotes, after an optional single or double
BECKER Benedikt's avatar
BECKER Benedikt committed
35
      underscore *)
36
  let split_base_suffixes str =
BECKER Benedikt's avatar
BECKER Benedikt committed
37 38 39 40
    try
      let re = Str.regexp "_?_?\\([0-9]*\\)\\('*\\)$" in
      let n = Str.search_forward re str 0 in
      let base = String.sub str 0 n in
41 42 43 44 45 46 47 48 49 50 51
      let numbers =
        match Str.matched_group 1 str with
        | "" -> None
        | s -> Some s
      in
      let quotes =
        match Str.matched_group 2 str with
        | "" -> None
        | s -> Some s
      in
      Some (base, numbers, quotes)
BECKER Benedikt's avatar
BECKER Benedikt committed
52
    with Not_found ->
BECKER Benedikt's avatar
BECKER Benedikt committed
53
      None
BECKER Benedikt's avatar
BECKER Benedikt committed
54 55 56

  (** Requirements *)

57
  type command_shape = {name: string; name': string; arity: int}
BECKER Benedikt's avatar
BECKER Benedikt committed
58 59 60 61 62

  module Requirements = Set.Make (struct type t = command_shape let compare = compare end)

  let requirements = ref Requirements.empty

63 64
  let record_command_shape name name' arity =
    requirements := Requirements.add {name; name'; arity} !requirements
BECKER Benedikt's avatar
BECKER Benedikt committed
65 66

  (** {2 Printers} *)
67 68
  let pp_command' ~suffix fmt base =
    fprintf fmt "\\%s%s%s" prefix (sanitize base) suffix
BECKER Benedikt's avatar
BECKER Benedikt committed
69 70

  (** Print a string as a LaTeX command *)
71
  let pp_command ~arity ~is_field fmt name =
72 73 74 75
    if match sn_decode name with | SNword _ -> false | _ -> true then
      failwith ("pp_command: argument not word: "^name);
    let name, name', suffix =
      if arity = 0 then
76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
        if is_field then
          name^"field", name, ""
        else
          match split_base_suffixes name with
          | Some (base, numbers, quotes) ->
              let numbers =
                match numbers with
                | Some s -> sprintf "_{%s}" s
                | None -> "" in
              let quotes =
                match quotes with
                | Some s -> s
                | None -> "" in
              base, base, numbers^quotes
          | _ -> name, name, ""
91
      else
92 93
        (assert (not is_field);
         name^string_of_int arity, name, "") in
94 95 96
    record_command_shape name name' arity;
    pp_command' ~suffix fmt name

97 98
  let pp_var' ~arity fmt s =
    pp_command ~arity ~is_field:false fmt s
BECKER Benedikt's avatar
BECKER Benedikt committed
99

100 101 102 103 104 105 106 107
  let pp_var ~arity fmt id =
    pp_var' ~arity fmt id.id_str

  let pp_field fmt id =
    pp_command ~arity:0 ~is_field:true fmt id.id_str

  let pp_str str fmt () =
    fprintf fmt str
BECKER Benedikt's avatar
BECKER Benedikt committed
108

109
  let pp_command_shape ~comment_macros fmt {name; name'; arity} =
BECKER Benedikt's avatar
BECKER Benedikt committed
110 111 112 113 114 115
    let rec mk_args acc = function
      | 0 -> acc
      | n -> mk_args (sprintf "#%d" n::acc) (pred n) in
    let pp_args fmt n =
      if n = 0 then
        ()
116
      else
BECKER Benedikt's avatar
BECKER Benedikt committed
117 118
        let args = mk_args [] n in
        fprintf fmt "(%a)" (pp_print_list ~pp_sep:(pp_str ", ") pp_print_string) args in
119 120
    fprintf fmt "%s\\newcommand{%a}[%d]{\\mathsf{%s}%a}@."
      (if comment_macros then "% " else "")
BECKER Benedikt's avatar
BECKER Benedikt committed
121
      (pp_command' ~suffix:"") name arity (sanitize name') pp_args arity
BECKER Benedikt's avatar
BECKER Benedikt committed
122 123 124 125 126 127 128 129 130 131

  (** {2 Pretty-print inductive definition to latex }*)

  let latex_rule_name fmt s =
    let f = function
      | '_' -> pp_print_char fmt '-'
      | c -> pp_print_char fmt c
    in
    String.iter f s

132 133 134 135
  let id_of_qualid = function
    | Qident id
    | Qdot (_, id) -> id

BECKER Benedikt's avatar
BECKER Benedikt committed
136 137 138 139 140 141 142 143
  let rec str_of_qualid = function
    | Qident id -> id.id_str
    | Qdot (qid, id) -> str_of_qualid qid^"."^id.id_str

  let pp_arg pp fmt =
    fprintf fmt "{%a}" pp

  let pp_field pp fmt (qid, x) =
144
    fprintf fmt "%a\\texttt{=}%a"
145 146
      pp_field (id_of_qualid qid)
      pp x
BECKER Benedikt's avatar
BECKER Benedikt committed
147 148 149

  let rec pp_type fmt = function
    | PTtyvar id ->
150
        pp_var ~arity:0 fmt id
BECKER Benedikt's avatar
BECKER Benedikt committed
151 152
    | PTtyapp (qid, ts) ->
        let arity = List.length ts in
153
        fprintf fmt "%a%a" (pp_var ~arity) (id_of_qualid qid)
BECKER Benedikt's avatar
BECKER Benedikt committed
154 155 156 157 158 159 160
          (pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_type)) ts
    | PTtuple ts ->
        fprintf fmt "(%a)"
          (pp_print_list ~pp_sep:(pp_str "") pp_type) ts
    | PTarrow (ty1, ty2) ->
        fprintf fmt "%a \\rightarrow %a"
          pp_type ty1 pp_type ty2
161 162
    | PTscope (_, ty) ->
        pp_type fmt ty
BECKER Benedikt's avatar
BECKER Benedikt committed
163 164 165 166 167 168 169 170 171 172 173
    | PTparen ty ->
        fprintf fmt "(%a)" pp_type ty
    | PTpure ty ->
        fprintf fmt "\\texttt{\\{}%a\\texttt{\\}}" pp_type ty
    | PTref _ -> failwith "pp_type: ref"

  let rec pp_pattern fmt p =
    match p.pat_desc with
    | Pwild ->
        fprintf fmt "\\texttt{anything}"
    | Pvar id ->
174
        fprintf fmt "%a" (pp_var ~arity:0) id
BECKER Benedikt's avatar
BECKER Benedikt committed
175 176
    | Papp (qid, ps) ->
        let arity = List.length ps in
177
        fprintf fmt "%a%a" (pp_var ~arity) (id_of_qualid qid)
BECKER Benedikt's avatar
BECKER Benedikt committed
178 179
          (pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_pattern)) ps
    | Prec fs ->
BECKER Benedikt's avatar
BECKER Benedikt committed
180
        fprintf fmt "\\texttt{\\{}%a\\texttt{\\}}"
BECKER Benedikt's avatar
BECKER Benedikt committed
181 182 183 184
          (pp_print_list ~pp_sep:(pp_str "\\texttt{;} ") (pp_field pp_pattern)) fs
    | Ptuple ps ->
        fprintf fmt "(%a)" (pp_print_list ~pp_sep:(pp_str ", ") pp_pattern) ps
    | Pas (p, id, _) ->
185
        fprintf fmt "%a \\texttt{as} %a" pp_pattern p (pp_var ~arity:0) id
BECKER Benedikt's avatar
BECKER Benedikt committed
186
    | Por (p1, p2) ->
BECKER Benedikt's avatar
BECKER Benedikt committed
187
        fprintf fmt "%a \\texttt{|} %a" pp_pattern p1 pp_pattern p2
BECKER Benedikt's avatar
BECKER Benedikt committed
188 189
    | Pcast (p, ty) ->
        fprintf fmt "%a : %a" pp_pattern p pp_type ty
BECKER Benedikt's avatar
BECKER Benedikt committed
190
    | Pscope (_, p) ->
191
        pp_pattern fmt p
BECKER Benedikt's avatar
BECKER Benedikt committed
192 193 194 195 196
    | Pparen p ->
        fprintf fmt "(%a)" pp_pattern p
    | Pghost p ->
        pp_pattern fmt p

197 198 199 200 201 202 203 204 205
  let rec flatten_apply t =
    match t.term_desc with
    | Tapply ({term_desc=Tident qid}, t) -> Some (qid, [t])
    | Tapply (t1, t2) ->
        (match flatten_apply t1 with
         | Some (qid, ts) -> Some (qid, ts@[t2])
         | None -> None)
    | _ -> None

BECKER Benedikt's avatar
BECKER Benedikt committed
206 207 208 209 210 211 212 213 214
  let rec pp_term fmt t =
    match t.term_desc with
    | Ttrue ->
        fprintf fmt "\\top"
    | Tfalse ->
        fprintf fmt "\\bot"
    | Tconst n ->
        Number.print_constant fmt n
    | Tident qid ->
215 216
        let id = id_of_qualid qid in
        (match sn_decode id.id_str with
217
         | SNword _ -> pp_var ~arity:0 fmt id
218
         | _ -> fprintf fmt "(%s)" id.id_str)
BECKER Benedikt's avatar
BECKER Benedikt committed
219 220
    | Tinnfix (t1, id, t2)
    | Tinfix (t1, id, t2) ->
221 222
        let op =
          match sn_decode id.id_str with
223
          | SNinfix s -> sanitize_op s
224 225
          | _ -> failwith ("pp_term: op not infix: |"^id.id_str^"|") in
        fprintf fmt "%a %s %a" pp_term t1 op pp_term t2
BECKER Benedikt's avatar
BECKER Benedikt committed
226 227 228 229 230 231 232 233 234 235 236 237 238 239
    | Tbinop (t1, op, t2)
    | Tbinnop (t1, op, t2) ->
        let str =
          let open Dterm in
          match op with
          | DTimplies -> "\\rightarrow"
          | DTiff -> "\\leftrightarrow"
          | DTand -> "\\wedge"
          | DTand_asym -> "\\bar\\wedge"
          | DTor -> "\\vee"
          | DTor_asym -> "\\bar\\vee"
          | DTby -> "\\texttt{by}"
          | DTso -> "\\texttt{so}" in
        fprintf fmt "%a %s %a" pp_term t1 str pp_term t2
240 241 242 243 244 245
    | Tidapp (qid, ts) ->
        let id = id_of_qualid qid in
        (match sn_decode id.id_str, ts with
         | SNword s, ts ->
             let arity = List.length ts in
             let pp_args = pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_term) in
246
             fprintf fmt "%a%a" (pp_var' ~arity) s pp_args ts
247
         | SNinfix s, [t1; t2] ->
248
             fprintf fmt "%a %s %a" pp_term t1 (sanitize_op s) pp_term t2
249 250 251 252
         | SNprefix s, [t]
         | SNtight s, [t] ->
             fprintf fmt "%s %a" s pp_term t
         | SNget s, [t1; t2] ->
BECKER Benedikt's avatar
BECKER Benedikt committed
253
             fprintf fmt "%a[%a]%s" pp_term t1 pp_term t2 s
254 255 256 257 258 259 260 261 262 263
         | SNset s, [t1; t2; t3] ->
             fprintf fmt "%a[%a]%s \\leftarrow %a" pp_term t1 pp_term t2 s pp_term t3
         | SNupdate s, [t1; t2; t3] ->
             fprintf fmt "%a[%a \\leftarrow %a]%s" pp_term t1 pp_term t2 pp_term t3 s
         | SNcut s, [t] ->
             fprintf fmt "%a[\\ldots]%s" pp_term t s
         | SNlcut s, [t1; t2] ->
             fprintf fmt "%a[\\ldots %a]%s" pp_term t1 pp_term t2 s
         | SNrcut s, [t1; t2] ->
             fprintf fmt "%a[%a \\ldots]%s" pp_term t1 pp_term t2 s
264
         | _ -> failwith (sprintf "pp_term Tidapp %s %d" id.id_str (List.length ts)))
265 266 267 268 269 270 271 272
    | Tapply (t1, t2) ->
        (match
           if flatten_applies
           then flatten_apply t
           else None
         with
         | Some (qid, ts) ->
             let arity = List.length ts in
273
             fprintf fmt "%a%a" (pp_var ~arity) (id_of_qualid qid)
274 275 276
               (pp_print_list ~pp_sep:(pp_str "") (pp_arg pp_term)) ts
         | None ->
             fprintf fmt "%a %a" pp_term t1 pp_term t2)
BECKER Benedikt's avatar
BECKER Benedikt committed
277
    | Tnot {term_desc=Tinfix (t1, op, t2)} when
278
        sn_decode op.id_str = SNinfix "=" ->
BECKER Benedikt's avatar
BECKER Benedikt committed
279 280 281 282 283 284 285
        fprintf fmt "%a \\neq %a" pp_term t1 pp_term t2
    | Tnot t ->
        fprintf fmt "\\neg %a" pp_term t
    | Tif (t1, t2, t3) ->
        fprintf fmt "\\texttt{if}~%a~\\texttt{then}~%a~\\texttt{else}~%a"
          pp_term t1 pp_term t2 pp_term t3
    | Tlet (id, t1, t2) ->
286
        fprintf fmt "\\textbf{let}~%a = %a~\\textbf{in}~%a" (pp_var ~arity:0) id
BECKER Benedikt's avatar
BECKER Benedikt committed
287 288 289 290 291 292 293 294 295
          pp_term t1 pp_term t2
    | Tquant (_, _, _, t) ->
        pp_term fmt t
    | Tcase (t, bs) ->
        let pp_sep = pp_str " \\texttt{|} " in
        let pp_branch fmt (p, t') = fprintf fmt "%a \\rightarrow %a" pp_pattern p pp_term t' in
        fprintf fmt "\\texttt{match}~%a~\\texttt{with}~%a" pp_term t
          (pp_print_list ~pp_sep pp_branch) bs
    | Tcast (t, ty) ->
BECKER Benedikt's avatar
BECKER Benedikt committed
296
        fprintf fmt "%a \\texttt{:} %a" pp_term t pp_type ty
BECKER Benedikt's avatar
BECKER Benedikt committed
297 298 299 300 301 302 303
    | Ttuple ts ->
        fprintf fmt "(%a)" (pp_print_list ~pp_sep:(pp_str ", ") pp_term) ts
    | Trecord fs ->
        let pp = pp_print_list ~pp_sep:(pp_str "\\texttt{;} ") (pp_field pp_term) in
        fprintf fmt "\\{%a\\}" pp fs
    | Tupdate (t, fs) ->
        let pp_fs = pp_print_list ~pp_sep:(pp_str "\\texttt{;} ") (pp_field pp_term) in
304
        fprintf fmt "\\{%a~\\texttt{with}~%a\\}" pp_term t pp_fs fs
BECKER Benedikt's avatar
BECKER Benedikt committed
305
    | Tscope (_, t) ->
306
        pp_term fmt t
BECKER Benedikt's avatar
BECKER Benedikt committed
307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325
    | Tattr _ -> failwith "pp_term: attr"
    | Tat _ -> failwith "pp_term: at"
    | Tasref _ -> failwith "pp_term: asref"

  let pp_rule fmt (id, terms) : unit =
    match List.rev terms with
    | [] -> invalid_arg "latex_rule: empty rule"
    | concl :: precs ->
        fprintf fmt "  \\inferrule[%a]@.    {%s%a}@.    {%a} \\\\@."
          latex_rule_name id.id_str
          (if precs = [] then "~" else "")
          (pp_print_list ~pp_sep:(pp_str "@ \\\\@ ") pp_term) (List.rev precs)
          pp_term concl

  let pp_rules fmt path defs =
    fprintf fmt "\\begin{mathparpagebreakable} %% %s@." (String.concat "." path);
    List.iter (pp_rule fmt) defs;
    fprintf fmt "\\end{mathparpagebreakable}@."

BECKER Benedikt's avatar
BECKER Benedikt committed
326 327
  exception Found of ind_decl

BECKER Benedikt's avatar
BECKER Benedikt committed
328 329 330 331 332 333
  (** Search an inductive type in mlw file by path (module.Theory.type or module.type) *)
  let search_inductive (path: string list) (mlw_file: mlw_file) : ind_decl =
    let name, decls =
      match path, mlw_file with
      | [name], Decls decls -> name, decls
      | [module_name; name], Modules modules ->
BECKER Benedikt's avatar
BECKER Benedikt committed
334
          let aux (id, _) = String.compare id.id_str module_name = 0 in
BECKER Benedikt's avatar
BECKER Benedikt committed
335 336 337 338 339 340
          name, snd (List.find aux modules)
      | _ -> raise Not_found in
    try
      let aux = function
        | Dind (Decl.Ind, ind_decls) ->
            let aux decl =
BECKER Benedikt's avatar
BECKER Benedikt committed
341
              if String.compare decl.in_ident.id_str name = 0 then
BECKER Benedikt's avatar
BECKER Benedikt committed
342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358
                raise (Found decl) in
            List.iter aux ind_decls
        | _ -> () in
      List.iter aux decls;
      raise Not_found
    with Found decl -> decl

  (** Flatten toplevel implies, let bindings, and universal quantifications *)
  let rec flatten_implies (t: term) : term list =
    match t.term_desc with
    | Tbinop (t1, Dterm.DTimplies, t2) ->
        t1 :: flatten_implies t2
    | Tquant (Dterm.DTforall, _, _, t) ->
        flatten_implies t
    | Tlet (id, t1, t2) ->
        let equality = (* id = t2 *)
          let id_term = {term_loc=Loc.dummy_position; term_desc=Tident (Qident id)} in
359
          let op = {Ptree.id_str=op_infix "="; Ptree.id_loc=Loc.dummy_position; id_ats=[]} in
BECKER Benedikt's avatar
BECKER Benedikt committed
360 361 362 363 364 365
          Tinfix (id_term, op, t1) in
        {term_loc=Loc.dummy_position; term_desc=equality} ::
        flatten_implies t2
    | _ -> [t]

  let main fmt mlw_file paths =
BECKER Benedikt's avatar
BECKER Benedikt committed
366 367 368 369 370 371 372 373 374 375 376 377
    let buf = Buffer.create 42 in
    let fmt' = formatter_of_buffer buf in
    let for_path path =
      try
        let decl = search_inductive path mlw_file in
        let defs = List.map (fun (_, id, t) -> id, flatten_implies t) decl.in_def in
        pp_rules fmt' path defs
      with Not_found ->
        eprintf "Could not find %s" (Strings.join "." path) in
    List.iter for_path paths;
    Requirements.iter (pp_command_shape ~comment_macros fmt) !requirements;
    pp_print_string fmt (Buffer.contents buf)
BECKER Benedikt's avatar
BECKER Benedikt committed
378
end
379 380 381

(** {2 Command line interface} *)

BECKER Benedikt's avatar
BECKER Benedikt committed
382
open Format
383
open Why3
BECKER Benedikt's avatar
BECKER Benedikt committed
384

385 386 387 388 389 390 391 392 393 394 395 396
let filename = ref None

let paths = Queue.create ()

let add_filename_then_path p =
  if !filename = None then
    filename := Some p
  else
    Queue.add (Strings.split '.' p) paths

type kind = Inductive

BECKER Benedikt's avatar
BECKER Benedikt committed
397
let kind = ref None
398 399

let set_kind = function
BECKER Benedikt's avatar
BECKER Benedikt committed
400
  | "inductive" -> kind := Some Inductive
401 402
  | str -> ksprintf invalid_arg "kind: %s" str

BECKER Benedikt's avatar
BECKER Benedikt committed
403
type output = Latex | Mlw | Ast
404

BECKER Benedikt's avatar
BECKER Benedikt committed
405
let output = ref None
406 407

let set_output = function
BECKER Benedikt's avatar
BECKER Benedikt committed
408
  | "latex" -> output := Some Latex
BECKER Benedikt's avatar
BECKER Benedikt committed
409 410 411
  | "mlw" -> output := Some Mlw
  | "ast" -> output := Some Ast
  | str -> ksprintf invalid_arg "output: --%s--" str
412

BECKER Benedikt's avatar
BECKER Benedikt committed
413 414
let prefix = ref "IND"

415 416
let usage =
  "Pretty print Why3 declarations (currently only inductive types in LaTeX using mathpartir).\n\
417
   why3 pp [--output=latex|mlw|ast] [--kind=inductive] [--prefix <prefix>] <filename> [<Module>.]<type> ..."
418 419

let options = [
420 421 422 423
  "--output", Arg.String set_output,                "<output> Output format";
  "--kind",   Arg.String set_kind,                  "<category> Syntactic category to be printed (--kind=inductive only possible value for --output=latex)";
  "--prefix", Arg.String ((:=) prefix),             "<prefix> Prefix for LaTeX commands (default for output latex: IND)";
  "-",        Arg.Unit (fun () -> filename := Some "-"), " Read from stdin";
424 425 426
]

let parse_mlw_file filename =
427
  let c = if filename = "-" then stdin else open_in filename in
428
  let lexbuf = Lexing.from_channel c in
429
  let mlw_file = Lexer.parse_mlw_file lexbuf in
430 431
  if filename <> "-" then
    close_in c;
432 433 434 435 436 437 438 439
  mlw_file

let () =
  Arg.parse options add_filename_then_path usage;
  try
    match !filename with
    | Some filename ->
        let mlw_file = parse_mlw_file filename in
BECKER Benedikt's avatar
BECKER Benedikt committed
440 441
        (match !output, !kind, Queue.length paths with
         | Some Latex, Some Inductive, _ ->
442
             let paths = List.rev (Queue.fold (fun l x -> x :: l) [] paths) in
443
             let module Conf = struct let prefix = !prefix let flatten_applies = true let comment_macros = true end in
444
             let module M = LatexInd(Conf) in
BECKER Benedikt's avatar
BECKER Benedikt committed
445
             M.main std_formatter mlw_file paths
BECKER Benedikt's avatar
BECKER Benedikt committed
446 447 448
         | Some Mlw, None, 0 ->
             Mlw_printer.pp_mlw_file std_formatter mlw_file
         (* | Some Ast, None, 0 ->
449
          *     Ptree.pp_mlw_file std_formatter mlw_file *)
BECKER Benedikt's avatar
BECKER Benedikt committed
450
         | _, _, _ ->
451
             failwith "command line arguments"
452
        )
453 454 455 456
    | None -> invalid_arg "no filename given"
  with Invalid_argument msg ->
    eprintf "Error: %s@." msg;
    exit 1