pvs.ml 30.8 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
10
(********************************************************************)
11 12 13

(** PVS printer *)

14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
(*
QUESTIONS FOR THE PVS TEAM
--------------------------
  * tuples (there are native tuples in Why3)

    - in Why3, we have 0-tuples as well, i.e. a type "()" with a single
      value also written "()"

      currently, I'm using

         tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0

    - it looks like PVS does not allow me to perform pattern-matching (CASES)
      on tuples i.e something like

        CASES x1 OF
         (x2, x3): ...
        ENDCASES

      so I'm doing that instead:

        LET x2 = x1`1, x3 = x1`2 IN ...

Jean-Christophe's avatar
Jean-Christophe committed
37
      better: LET (x2, x3) = x1 IN ...
38 39 40

TODO
----
41 42
  * driver
    - maps: const
43

Jean-Christophe's avatar
Jean-Christophe committed
44 45
  * use proveit (same path as PVS) to replay a proof

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
open Format
open Pp
open Ident
open Ty
open Term
open Decl
open Printer

let black_list =
  [ "and"; "conjecture"; "fact"; "let"; "table";
    "andthen"; "containing"; "false"; "library"; "then";
    "array"; "conversion"; "forall"; "macro"; "theorem";
    "assuming"; "conversion+"; "formula"; "measure"; "theory";
    "assumption"; "conversion-"; "from"; "nonempty"; "type"; "true";
    "auto"; "rewrite"; "corollary"; "function"; "not"; "type";
    "auto"; "rewrite+";" datatype"; "has"; "type"; "o"; "type+";
    "auto"; "rewrite-"; "else"; "if"; "obligation"; "var";
    "axiom"; "elsif"; "iff"; "of"; "when";
    "begin"; "end"; "implies"; "or"; "where";
    "but"; "endassuming"; "importing"; "orelse"; "with";
    "by"; "endcases"; "in"; "postulate"; "xor";
    "cases"; "endcond"; "inductive"; "proposition";
    "challenge"; "endif"; "judgement"; "recursive";
    "claim"; "endtable"; "lambda"; "sublemma";
    "closure"; "exists"; "law"; "subtypes";
73
    "cond"; "exporting"; "lemma"; "subtype"; "of";
74
    (* PVS prelude *)
75 76
    "boolean"; "bool";
    "pred"; "setof"; "exists1";
77
    "list"; "length"; "member"; "nth"; "append"; "reverse";
78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
    "domain"; "range"; "graph"; "preserves"; "inverts"; "transpose";
    "restrict"; "extend"; "identity"; "eq";
    "epsilon";
    "set"; "member"; "emptyset"; "nonempty_set"; "fullset";
    "union"; "intersection"; "complement"; "difference";
    "symmetric_difference"; "every"; "some"; "singleton"; "add"; "remove";
    "choose"; "the"; "singleton_elt"; "rest"; "setofsets"; "powerset";
    "rinverse"; "rcomplement"; "runion"; "rintersection"; "image";
    "preimage"; "postcondition"; "converse";
    "number"; "number_field"; "numfield"; "nonzero_number"; "nznum";
    "real"; "nonzero_real"; "nzreal";
    "nonneg_real"; "nonpos_real"; "posreal"; "negreal"; "nnreal"; "npreal";
    "rational"; "rat"; "nonzero_rational"; "nzrat";
    "nonneg_rat"; "nonpos_rat"; "posrat"; "negrat"; "nnrat"; "nprat";
    "integer"; "int"; "nonzero_integer"; "nzint";
    "nonneg_int"; "nonpos_int"; "posint"; "negint"; "nnint"; "npint";
    "subrange"; "even_int"; "odd_int";
    "naturalnumber"; "nat"; "upto"; "below"; "succ"; "pred";
    "min"; "max"; "sgn"; "abs";
    "mod"; "divides"; "rem"; "ndiv";
    "upfrom"; "above";
99
    "even";
100
    ]
101

102
let fresh_printer () =
103
  let isanitize = sanitizer char_to_lalpha char_to_lalnumus in
104 105
  create_ident_printer black_list ~sanitizer:isanitize

106 107 108 109 110 111 112 113
let iprinter =
  let isanitize = sanitizer char_to_lalpha char_to_lalnumus in
  create_ident_printer black_list ~sanitizer:isanitize

let forget_all () = forget_all iprinter

let tv_set = ref Sid.empty

114 115 116 117
let thprinter =
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  create_ident_printer black_list ~sanitizer:isanitize

118 119 120 121 122 123 124 125 126
(* type variables *)

let print_tv fmt tv =
  let n = id_unique iprinter tv.tv_name in
  fprintf fmt "%s" n

let print_tv_binder fmt tv =
  tv_set := Sid.add tv.tv_name !tv_set;
  let n = id_unique iprinter tv.tv_name in
127
  fprintf fmt "%s:TYPE+" n
128

129 130 131
let print_params_list fmt = function
  | [] -> ()
  | tvl -> fprintf fmt "[%a]" (print_list comma print_tv_binder) tvl
132 133

let print_params fmt stv =
134
  print_params_list fmt (Stv.elements stv)
135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155

let forget_tvs () =
  Sid.iter (forget_id iprinter) !tv_set;
  tv_set := Sid.empty

(* logic variables *)
let print_vs fmt vs =
  let n = id_unique iprinter vs.vs_name in
  fprintf fmt "%s" n

let forget_var vs = forget_id iprinter vs.vs_name

let print_ts fmt ts =
  fprintf fmt "%s" (id_unique iprinter ts.ts_name)

let print_ls fmt ls =
  fprintf fmt "%s" (id_unique iprinter ls.ls_name)

let print_pr fmt pr =
  fprintf fmt "%s" (id_unique iprinter pr.pr_name)

156 157 158
let print_name fmt id =
  fprintf fmt "%% Why3 %s@\n" (id_unique iprinter id)

159 160 161 162 163
let get_th_name id =
  let s = id_unique thprinter id in
  Ident.forget_all thprinter;
  s

164 165 166 167
(* info *)

type info = {
  info_syn : syntax_map;
168
  symbol_printers : (string * Theory.theory * ident_printer) Mid.t;
169 170 171 172 173 174 175 176
  realization : bool;
}

let print_path = print_list (constant_string ".") string

let print_id fmt id = string fmt (id_unique iprinter id)

let print_id_real info fmt id =
177 178
  try
    let path, th, ipr = Mid.find id info.symbol_printers in
179
    let th = get_th_name th.Theory.th_name in
180 181 182 183 184
    let id = id_unique ipr id in
    if path = "" then fprintf fmt "%s.%s" th id
    else fprintf fmt "%s@@%s.%s" path th id
  with Not_found ->
    print_id fmt id
185 186 187 188 189 190 191 192 193 194

let print_ls_real info fmt ls = print_id_real info fmt ls.ls_name
let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name
let print_pr_real info fmt pr = print_id_real info fmt pr.pr_name

(** Types *)

let rec print_ty info fmt ty = match ty.ty_node with
  | Tyvar v -> print_tv fmt v
  | Tyapp (ts, tl) when is_ts_tuple ts ->
195
      begin match tl with
196
        | []  -> fprintf fmt "[]"
197 198
        | [ty] -> print_ty info fmt ty
        | _   -> fprintf fmt "[%a]" (print_list comma (print_ty info)) tl
199 200 201 202
      end
  | Tyapp (ts, tl) ->
      begin match query_syntax info.info_syn ts.ts_name with
        | Some s -> syntax_arguments s (print_ty info) fmt tl
203 204 205 206 207 208
        | None -> begin
          match tl with
            | []  -> (print_ts_real info) fmt ts
            | l   -> fprintf fmt "%a[%a]" (print_ts_real info) ts
                       (print_list comma (print_ty info)) l
        end
209 210 211 212 213 214 215 216 217 218 219 220 221
      end

(* can the type of a value be derived from the type of the arguments? *)
let unambig_fs fs =
  let rec lookup v ty = match ty.ty_node with
    | Tyvar u when tv_equal u v -> true
    | _ -> ty_any (lookup v) ty
  in
  let lookup v = List.exists (lookup v) fs.ls_args in
  let rec inspect ty = match ty.ty_node with
    | Tyvar u when not (lookup u) -> false
    | _ -> ty_all inspect ty
  in
222
  inspect (Opt.get fs.ls_value)
223 224 225 226 227

(** Patterns, terms, and formulas *)

let lparen_l fmt () = fprintf fmt "@ ("
let lparen_r fmt () = fprintf fmt "(@,"
228 229 230 231
let print_paren_l fmt x =
  print_list_delim ~start:lparen_l ~stop:rparen ~sep:comma fmt x
let print_paren_r fmt x =
  print_list_delim ~start:lparen_r ~stop:rparen ~sep:comma fmt x
232 233 234 235 236

let arrow fmt () = fprintf fmt "@ -> "
let print_arrow_list fmt x = print_list arrow fmt x
let print_space_list fmt x = print_list space fmt x
let print_comma_list fmt x = print_list comma fmt x
237 238
let print_or_list fmt x = print_list (fun fmt () -> fprintf fmt " OR@\n") fmt x
let comma_newline fmt () = fprintf fmt ",@\n"
239 240

let rec print_pat info fmt p = match p.pat_node with
241 242 243 244 245
  | Pvar v ->
      print_vs fmt v
  | Papp (cs, _) when is_fs_tuple cs ->
      assert false (* is handled earlier in print_term/fmla *)
  | Papp (cs, pl) ->
246 247 248
      begin match query_syntax info.info_syn cs.ls_name with
        | Some s -> syntax_arguments s (print_pat info) fmt pl
        | _ when pl = [] -> (print_ls_real info) fmt cs
249 250
        | _ -> fprintf fmt "%a(%a)"
          (print_ls_real info) cs (print_list comma (print_pat info)) pl
251
      end
252 253 254 255
  | Pas _ | Por _ ->
      assert false (* compile_match must have taken care of that *)
  | Pwild ->
      assert false (* is handled in print_branches *)
256 257 258 259 260 261 262

let print_vsty_nopar info fmt v =
  fprintf fmt "%a:%a" print_vs v (print_ty info) v.vs_ty

let print_vsty info fmt v =
  fprintf fmt "(%a)" (print_vsty_nopar info) v

263 264 265 266 267 268 269 270
let is_tuple0_ty = function
  | Some { ty_node = Tyapp (ts, _) } -> ts_equal ts (ts_tuple 0)
  | Some _ | None -> false

let is_tuple_ty = function
  | Some { ty_node = Tyapp (ts, _) } -> is_ts_tuple ts
  | Some _ | None -> false

271 272 273 274 275 276 277 278
let print_binop fmt = function
  | Tand -> fprintf fmt "AND"
  | Tor -> fprintf fmt "OR"
  | Timplies -> fprintf fmt "=>"
  | Tiff -> fprintf fmt "<=>"

(* TODO: labels are lost, but we could print them as "% label \n",
   it would result in an ugly output, though *)
Andrei Paskevich's avatar
Andrei Paskevich committed
279
let print_attr _fmt (_l,_) = () (*fprintf fmt "(*%s*)" l*)
280 281 282

let protect_on x s = if x then "(" ^^ s ^^ ")" else s

283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
let number_format = {
    Number.long_int_support = `Default;
    Number.negative_int_support = `Default;
    Number.dec_int_support = `Default;
    Number.hex_int_support = `Unsupported;
    Number.oct_int_support = `Unsupported;
    Number.bin_int_support = `Unsupported;
    Number.negative_real_support = `Default;
    Number.dec_real_support = `Unsupported;
    Number.hex_real_support = `Unsupported;
    Number.frac_real_support =
      `Custom
        ((fun fmt i -> pp_print_string fmt i),
         (fun fmt i n -> fprintf fmt "(%s * %s)" i n),
         (fun fmt i n -> fprintf fmt "(%s / %s)" i n));
  }

300 301 302 303 304 305 306
let rec print_term info fmt t = print_lrterm false false info fmt t
and     print_fmla info fmt f = print_lrfmla false false info fmt f
and print_opl_term info fmt t = print_lrterm true  false info fmt t
and print_opl_fmla info fmt f = print_lrfmla true  false info fmt f
and print_opr_term info fmt t = print_lrterm false true  info fmt t
and print_opr_fmla info fmt f = print_lrfmla false true  info fmt f

Andrei Paskevich's avatar
Andrei Paskevich committed
307
and print_lrterm opl opr info fmt t = match t.t_attrs with
308 309
  | _ -> print_tnode opl opr info fmt t

Andrei Paskevich's avatar
Andrei Paskevich committed
310
and print_lrfmla opl opr info fmt f = match f.t_attrs with
311 312 313 314 315 316
  | _ -> print_fnode opl opr info fmt f

and print_tnode opl opr info fmt t = match t.t_node with
  | Tvar v ->
      print_vs fmt v
  | Tconst c ->
317
      Number.print number_format fmt c
318
  | Tif (f, t1, t2) ->
319
      fprintf fmt "IF %a@ THEN %a@ ELSE %a ENDIF"
320 321 322 323 324 325
        (print_fmla info) f (print_term info) t1 (print_opl_term info) t2
  | Tlet (t1, tb) ->
      let v,t2 = t_open_bound tb in
      fprintf fmt (protect_on opr "LET %a =@ %a IN@ %a")
        print_vs v (print_opl_term info) t1 (print_opl_term info) t2;
      forget_var v
326 327 328 329 330 331 332 333 334
  | Tcase (t, [b]) when is_tuple0_ty t.t_ty ->
      let _,t = t_open_branch b in
      print_term info fmt t
  | Tcase (t, [b]) when is_tuple_ty t.t_ty ->
      let p,t1 = t_open_branch b in
      fprintf fmt "@[<hov 4>LET %a IN@ %a@]"
        (print_tuple_pat info t) p (print_term info) t1;
      Svs.iter forget_var p.pat_vars
  | Tcase (t, bl) ->
335
      fprintf fmt "CASES %a OF@\n@[<hov>%a@]@\nENDCASES"
336
        (print_term info) t (print_branches print_term info) bl
337 338
  | Teps fb ->
      let v,f = t_open_bound fb in
339 340
      fprintf fmt (protect_on opr "epsilon(LAMBDA (%a):@ %a)")
        (print_vsty_nopar info) v (print_opl_fmla info) f;
341 342
      forget_var v
  | Tapp (fs, []) when is_fs_tuple fs ->
343
      fprintf fmt "()"
344 345 346 347 348
  | Tapp (fs, pl) when is_fs_tuple fs ->
      fprintf fmt "%a" (print_paren_r (print_term info)) pl
  | Tapp (fs, tl) ->
    begin match query_syntax info.info_syn fs.ls_name with
      | Some s ->
349
          syntax_arguments_typed s (print_term info) (print_ty info) t fmt tl
350
      | _ ->
351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366
          let no_cast = unambig_fs fs in
          begin match tl with
            | [] when no_cast ->
              fprintf fmt "%a" (print_ls_real info) fs
            | [] ->
              fprintf fmt "(%a :: %a)"
                (print_ls_real info) fs (print_ty info) (t_type t)
            | _ when no_cast ->
              fprintf fmt "%a(%a)" (print_ls_real info) fs
                (print_comma_list (print_term info)) tl
            |_ ->
              fprintf fmt (protect_on opl "(%a(%a) :: %a)")
                (print_ls_real info) fs
                (print_comma_list (print_term info)) tl
                (print_ty info) (t_type t)
          end
367
    end
368 369
  | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse ->
      raise (TermExpected t)
370 371 372 373

and print_fnode opl opr info fmt f = match f.t_node with
  | Tquant (Tforall, fq) ->
      let vl,_tl,f = t_open_quant fq in
374 375
      fprintf fmt (protect_on opr "FORALL (%a):@ %a")
        (print_comma_list (print_vsty_nopar info)) vl
376 377 378 379 380 381 382 383
        (* (print_tl info) tl *) (print_fmla info) f;
      List.iter forget_var vl
  | Tquant (Texists,fq) ->
      let vl,_tl,f = t_open_quant fq in
      let rec aux fmt vl = match vl with
        | [] ->
          print_fmla info fmt f
        | v :: vr ->
384
          fprintf fmt (protect_on opr "EXISTS (%a):@ %a")
385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402
            (print_vsty_nopar info) v aux vr
      in
      aux fmt vl;
      List.iter forget_var vl
  | Ttrue ->
      fprintf fmt "TRUE"
  | Tfalse ->
      fprintf fmt "FALSE"
  | Tbinop (b, f1, f2) ->
      fprintf fmt (protect_on (opl || opr) "%a %a@ %a")
        (print_opr_fmla info) f1 print_binop b (print_opl_fmla info) f2
  | Tnot f ->
      fprintf fmt (protect_on opr "NOT %a") (print_opl_fmla info) f
  | Tlet (t, f) ->
      let v,f = t_open_bound f in
      fprintf fmt (protect_on opr "LET %a =@ %a IN@ %a")
        print_vs v (print_opl_term info) t (print_opl_fmla info) f;
      forget_var v
403 404 405 406 407 408 409 410
  | Tcase (t, [b]) when is_tuple0_ty t.t_ty ->
      let _,f = t_open_branch b in
      print_fmla info fmt f
  | Tcase (t, [b]) when is_tuple_ty t.t_ty ->
      let p,f = t_open_branch b in
      fprintf fmt "@[<hov 4>LET %a IN@ %a@]"
        (print_tuple_pat info t) p (print_fmla info) f;
      Svs.iter forget_var p.pat_vars
411 412
  | Tcase (t, bl) ->
      fprintf fmt "CASES %a OF@\n@[<hov>%a@]@\nENDCASES"
413
        (print_term info) t (print_branches print_fmla info) bl
414
  | Tif (f1, f2, f3) ->
415
      fprintf fmt (protect_on opr "IF %a@ THEN %a@ ELSE %a ENDIF")
416 417 418 419 420
        (print_fmla info) f1 (print_fmla info) f2 (print_opl_fmla info) f3
  | Tapp (ps, tl) ->
    begin match query_syntax info.info_syn ps.ls_name with
      | Some s ->
          syntax_arguments s (print_term info) fmt tl
421 422 423
      | None when tl = [] ->
          fprintf fmt "%a" (print_ls_real info) ps
      | None ->
424
          fprintf fmt "%a(%a)" (print_ls_real info) ps
425
            (print_comma_list (print_term info)) tl
426 427 428 429
    end
  | Tvar _ | Tconst _ | Teps _ ->
      raise (FmlaExpected f)

430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445
and print_tuple_pat info t fmt p =
  let unvar p = match p.pat_node with
    | Pvar vs -> vs
    | _ -> assert false (*TODO?*)
  in
  let l = match p.pat_node with
    | Papp (_, pl) -> List.map unvar pl | _ -> assert false
  in
  let i = ref 0 in
  let print fmt vs =
    incr i;
    fprintf fmt "%a = %a`%d"
      (print_vsty_nopar info) vs (print_term info) t !i
  in
  print_comma_list print fmt l

446
and print_branch print info fmt br =
447
  let p,t = t_open_branch br in
448
  fprintf fmt "@[<hov 4> %a:@ %a@]"
449
    (print_pat info) p (print info) t;
450 451
  Svs.iter forget_var p.pat_vars

452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468
and print_branches ?(first=true) print info fmt = function
  | [] ->
      ()
  | br :: bl ->
      let p, t = t_open_branch br in
      begin match p.pat_node with
        | Pwild ->
            assert (bl = []);
            if not first then fprintf fmt "@\n";
            fprintf fmt "@[<hov 4>ELSE@ %a@]" (print info) t
        | _ ->
            if not first then fprintf fmt ",@\n";
            fprintf fmt "@[<hov 4> %a:@ %a@]"
              (print_pat info) p (print info) t;
            Svs.iter forget_var p.pat_vars;
            print_branches ~first:false print info fmt bl
      end
469 470 471 472 473 474

let print_expr info fmt =
  TermTF.t_select (print_term info fmt) (print_fmla info fmt)

(** Declarations *)

475
let print_constr info _ts fmt (cs,_) =
476 477 478 479
  match cs.ls_args with
    | [] ->
        fprintf fmt "@[<hov 4>%a: %a?@]" print_ls cs print_ls cs
    | l ->
480 481 482 483 484 485
        let sid = ref Sid.empty in
        let print fmt ty =
	  let n = id_register (id_fresh "x") in
	  sid := Sid.add n !sid;
	  fprintf fmt "%s:%a" (id_unique iprinter n) (print_ty info) ty
	in
486
        fprintf fmt "@[<hov 4>%a(%a): %a?@]" print_ls cs
487 488
          (print_comma_list print) l print_ls cs;
        Sid.iter (forget_id iprinter) !sid
489 490 491

let ls_ty_vars ls =
  let ty_vars_args = List.fold_left Ty.ty_freevars Stv.empty ls.ls_args in
492
  let ty_vars_value = Opt.fold Ty.ty_freevars Stv.empty ls.ls_value in
493 494 495 496 497 498 499 500
  (ty_vars_args, ty_vars_value, Stv.union ty_vars_args ty_vars_value)

(*

  copy of old user scripts

*)

501 502 503 504
let clean_line s =
  let n = String.length s in
  if n >= 2 && s.[0] = ' ' && s.[1] = ' ' then String.sub s 2 (n - 2) else s

505
type contents = string list
506 507

type chunk =
508 509
  | Edition of string * contents (* name contents *)
  | Other of contents            (* contents *)
510

Jean-Christophe's avatar
Jean-Christophe committed
511
let re_blank = Str.regexp "[ ]*$"
512 513
let re_why3 = Str.regexp "% Why3 \\([^ ]+\\)"

514 515 516 517
(* Reads an old version of the file, as a list of chunks.
   Each chunk is either identified as a Why3 symbol (Edition)
   or as something else (Other).
   Note: the very last chunk is purposely ignored, as it is "END th" *)
518 519
let read_old_script ch =
  let chunks = ref [] in
520
  let contents = ref [] in
521
  let read_line () =
522
    let s = input_line ch in
Jean-Christophe's avatar
Jean-Christophe committed
523
    clean_line s
524
  in
Jean-Christophe's avatar
Jean-Christophe committed
525 526 527 528 529
  (* skip first lines, until we find a blank line *)
  begin try while true do
    let s = read_line () in if Str.string_match re_blank s 0 then raise Exit
  done with End_of_file | Exit -> () end;
  (* then read chunks *)
530 531 532 533 534 535 536 537 538
  let rec read ?name () =
    let s = read_line () in
    if s = "" then begin
      new_chunk ?name (); read ()
    end else if Str.string_match re_why3 s 0 then begin
      new_chunk ?name ();
      let name = Str.matched_group 1 s in
      read ~name ()
    end else begin
539
      contents := s :: !contents;
540 541 542
      read ?name ()
    end
  and new_chunk ?name () =
543 544
    let s = List.rev !contents in
    contents := [];
545
    match s, name with
546
      | ([] | [""]), _ -> ()
547 548 549 550
      | _, None -> chunks := Other s :: !chunks
      | _, Some n -> chunks := Edition (n, s) :: !chunks
  in
  try read () with End_of_file -> List.rev !chunks
551 552 553 554 555 556 557 558 559 560 561 562 563 564

(* DEBUG
let read_old_script ch =
  let cl = read_old_script ch in
  let dump = function
    | Edition (n, s) ->
        eprintf "/edited %s = @[%a@]" n (print_list newline pp_print_string) s
    | Other _s -> eprintf "/other"
  in
  List.iter dump cl; eprintf "@.";
  cl
*)

let print_contents fmt c = print_list newline pp_print_string fmt c
565 566 567

(* Output all the Other entries of the script that occur before the
   location of name. Modify the script by removing the name entry and all
568
   these outputs. Return the user content, if any. *)
569 570 571 572
let output_till_statement fmt script name =
  let print i =
    let rec aux acc = function
      | h :: l when h == i ->
573
          let l = match l with Other [""] :: l -> l | _ -> l in
574
          script := List.rev_append acc l
575
      | Other o :: l -> fprintf fmt "%a@\n@\n" print_contents o; aux acc l
576 577 578 579 580 581 582 583 584 585 586
      | h :: l -> aux (h :: acc) l
      | [] -> assert false
    in
    aux [] !script
  in
  let rec find = function
    | Edition (n,_) as o :: _ when n = name -> print o; Some o
    | [] -> None
    | _ :: t -> find t
  in
  find !script
587

588 589 590 591
let print_contents_in_comment fmt c =
  let print fmt s =
    if s = "" || s.[0] <> '%' then fprintf fmt "%% "; fprintf fmt "%s" s in
  print_list newline print fmt c
592

593
let output_remaining fmt cl =
594
  let print fmt = function
595
    | Edition (n, c) ->
596
        fprintf fmt "%% Obsolete chunk %s@\n%a@\n" n print_contents_in_comment c
597
    | Other c ->
598 599 600 601 602 603 604 605 606 607 608 609
        fprintf fmt "%a@\n" print_contents_in_comment c
  in
  print_list newline print fmt cl

(* Extracts and prints a definition from a user-edited chunk, if any;
   otherwise, prints nothing *)
let print_user_def fmt c =
  let rec scan_string _stack i s =
    let n = String.length s in
    if i = n then None else match s.[i] with
      | '=' -> Some (String.sub s i (n - i))
      | _ -> scan_string _stack (i+1) s
610
  in
611 612 613 614 615 616 617 618 619 620 621 622 623
  let rec scan_chunck _stack = function
    | [] -> ()
    | s :: c ->
        begin match scan_string _stack 0 s with
          | Some s -> fprintf fmt " %s" s; print_contents fmt c
          | None -> scan_chunck _stack c
        end
  in
  scan_chunck [] c

let realization fmt info = function
  | Some (Edition (_, c)) when info.realization -> print_user_def fmt c
  | _ -> ()
624

625 626 627 628
let print_type_decl ~prev info fmt ts = ignore (prev);
  if not (is_ts_tuple ts) then begin
    print_name fmt ts.ts_name;
    match ts.ts_def with
Clément Fumex's avatar
Clément Fumex committed
629
    | NoDef | Range _ | Float _ ->
Jean-Christophe's avatar
Jean-Christophe committed
630
        fprintf fmt "@[<hov 2>%a%a: TYPE+"
631 632 633
          print_ts ts print_params_list ts.ts_args;
        realization fmt info prev;
        fprintf fmt "@]@\n@\n"
Clément Fumex's avatar
Clément Fumex committed
634
    | Alias ty ->
635
        fprintf fmt "@[<hov 2>%a%a: TYPE+ =@ %a@]@\n@\n"
636
          print_ts ts print_params_list ts.ts_args
637
          (print_ty info) ty
638
  end
639

640 641 642 643 644
let print_type_decl ~prev info fmt ts =
  if not (Mid.mem ts.ts_name info.info_syn) then begin
    print_type_decl ~prev info fmt ts;
    forget_tvs ()
  end
645 646

let print_data_decl info fmt (ts,csl) =
647 648 649 650 651 652 653
  if not (is_ts_tuple ts) then begin
    print_name fmt ts.ts_name;
    fprintf fmt
      "@[<hov 1>%a%a: DATATYPE@\n@[<hov 1>BEGIN@\n%a@]@\nEND %a@]@\n@\n"
      print_ts ts print_params_list ts.ts_args
      (print_list newline (print_constr info ts)) csl print_ts ts
  end
654

655
let print_data_decl info fmt d =
656 657 658
  if not (Mid.mem (fst d).ts_name info.info_syn) then begin
    print_data_decl info fmt d;
    forget_tvs ()
659
  end
660

661 662 663 664
let print_ls_type info fmt = function
  | None -> fprintf fmt "bool"
  | Some ty -> print_ty info fmt ty

665 666 667 668 669 670
let create_argument ty = create_vsymbol (id_fresh "x") ty

let print_arguments info fmt = function
  | [] -> ()
  | vl -> fprintf fmt "(%a)" (print_comma_list (print_vsty_nopar info)) vl

671 672 673 674 675 676 677 678
let re_macro = Str.regexp "\\bMACRO\\b"
let has_macro s =
  try let _ = Str.search_forward re_macro s 0 in true with Not_found -> false
let is_macro info fmt = function
  | Some (Edition (_, c)) when info.realization && List.exists has_macro c ->
      fprintf fmt "MACRO "
  | _ -> ()

679 680
let print_param_decl ~prev info fmt ls =
  ignore prev;
681 682
  let _, _, all_ty_params = ls_ty_vars ls in
  let vl = List.map create_argument ls.ls_args in
683
  print_name fmt ls.ls_name;
684 685 686
  fprintf fmt "@[<hov 2>%a%a%a: %a%a"
    print_ls ls print_params all_ty_params (print_arguments info) vl
    (is_macro info) prev (print_ls_type info) ls.ls_value;
687 688 689
  realization fmt info prev;
  List.iter forget_var vl;
  fprintf fmt "@]@\n@\n"
690

691
let print_param_decl ~prev info fmt ls =
692 693 694 695
  if not (Mid.mem ls.ls_name info.info_syn) then begin
    print_param_decl ~prev info fmt ls;
    forget_tvs ()
  end
696

697 698
let print_logic_decl ~prev info fmt (ls,ld) =
  ignore prev;
699
  let _, _, all_ty_params = ls_ty_vars ls in
700
  let vl,e = open_ls_defn ld in
701
  print_name fmt ls.ls_name;
702
  fprintf fmt "@[<hov 2>%a%a%a: %a =@ %a@]@\n@\n"
703
    print_ls ls print_params all_ty_params
704
    (print_arguments info) vl (print_ls_type info) ls.ls_value
705 706
    (print_expr info) e;
  List.iter forget_var vl
707

708
let print_logic_decl ~prev info fmt d =
709 710 711 712
  if not (Mid.mem (fst d).ls_name info.info_syn) then begin
    print_logic_decl ~prev info fmt d;
    forget_tvs ()
  end
713

714
let print_recursive_decl info fmt (ls,ld) =
715
  let _, _, all_ty_params = ls_ty_vars ls in
716 717
  let i = match Decl.ls_defn_decrease ld with
    | [i] -> i | _ -> assert false in
718
  let vl,e = open_ls_defn ld in
719
  print_name fmt ls.ls_name;
720 721
  fprintf fmt "@[<hov 2>%a%a%a: RECURSIVE %a =@ %a@\n"
    print_ls ls print_params all_ty_params (print_arguments info) vl
722 723
    (print_ls_type info) ls.ls_value
    (print_expr info) e;
724
  fprintf fmt "MEASURE %a BY <<@\n@]@\n"
725
    print_vs (List.nth vl i);
726 727 728 729 730 731 732
  List.iter forget_var vl

let print_recursive_decl info fmt d =
  if not (Mid.mem (fst d).ls_name info.info_syn) then begin
    print_recursive_decl info fmt d;
    forget_tvs ()
  end
733 734

let print_ind info fmt (pr,f) =
735
  fprintf fmt "@[%% %a:@\n(%a)@]" print_pr pr (print_fmla info) f
736

737
let print_ind_decl info fmt (ps,al) =
738
  let _, _, all_ty_params = ls_ty_vars ps in
739 740
  let vl = List.map (create_vsymbol (id_fresh "z")) ps.ls_args in
  let tl = List.map t_var vl in
741
  let dj = Lists.map_join_left (Eliminate_inductive.exi tl) t_or al in
742
  print_name fmt ps.ls_name;
743 744
  fprintf fmt "@[<hov 2>%a%a%a: INDUCTIVE bool =@ @[<hov>%a@]@]@\n"
    print_ls ps print_params all_ty_params (print_arguments info) vl
745
    (print_fmla info) dj;
746 747 748
  fprintf fmt "@\n"

let print_ind_decl info fmt d =
749 750 751 752
  if not (Mid.mem (fst d).ls_name info.info_syn) then begin
    print_ind_decl info fmt d;
    forget_tvs ()
  end
753

754 755 756 757 758 759 760 761 762 763 764
let re_lemma = Str.regexp "\\(\\bLEMMA\\b\\|\\bTHEOREM\\b\\)"
let rec find_lemma = function
  | [] -> "AXIOM"
  | s :: sl ->
      (try let _ = Str.search_forward re_lemma s 0 in Str.matched_group 1 s
       with Not_found -> find_lemma sl)
let axiom_or_lemma = function
  | Some (Edition (_, c)) -> find_lemma c
  | _ -> "AXIOM"

let print_prop_decl ~prev info fmt (k,pr,f) =
765
  ignore (prev);
766
  let params = t_ty_freevars Stv.empty f in
767
  let kind = match k with
Jean-Christophe's avatar
Jean-Christophe committed
768
    | Paxiom when info.realization -> "LEMMA" (* axiom_or_lemma prev *)
769
    | Paxiom -> "AXIOM"
770
    | Plemma -> "LEMMA"
771
    | Pgoal -> "THEOREM" in
772
  print_name fmt pr.pr_name;
773 774
  fprintf fmt "@[<hov 2>%a%a: %s %a@]@\n@\n"
    print_pr pr print_params params kind (print_fmla info) f;
775 776 777 778 779 780 781 782 783 784 785 786 787 788 789
  forget_tvs ()

let print_decl ~old info fmt d =
  let name = match d.d_node with
    | Dtype ts
    | Ddata ((ts, _) :: _) -> id_unique iprinter ts.ts_name
    | Dparam ls
    | Dlogic ((ls, _) :: _)
    | Dind (_, (ls,_) :: _) -> id_unique iprinter ls.ls_name
    | Dprop (_, pr, _) -> id_unique iprinter pr.pr_name
    | Ddata []
    | Dlogic []
    | Dind (_, []) -> assert false in
  let prev = output_till_statement fmt old name in
  match d.d_node with
790
  | Dtype ts ->
791
      print_type_decl ~prev info fmt ts
792 793 794
  | Ddata tl ->
      print_list nothing (print_data_decl info) fmt tl
  | Dparam ls ->
795
      print_param_decl ~prev info fmt ls
796
  | Dlogic [s, _ as ld] when not (Sid.mem s.ls_name d.d_syms) ->
797
      print_logic_decl ~prev info fmt ld
798 799 800
  | Dlogic [d] ->
      print_recursive_decl info fmt d
  | Dlogic _ ->
801
      unsupportedDecl d "PVS does not support mutually recursive definitions"
802
  | Dind (Ind, il) ->
803
      print_list nothing (print_ind_decl info) fmt il
804
  | Dind (Coind, _) ->
805
      unsupportedDecl d "PVS: coinductive definitions are not supported"
806 807
  | Dprop (_, pr, _) when Mid.mem pr.pr_name info.info_syn ->
      ()
808
  | Dprop pr ->
809
      print_prop_decl ~prev info fmt pr
810 811

let print_decls ~old info fmt dl =
812
  fprintf fmt "@[<hov>%a@]" (print_list nothing (print_decl ~old info)) dl
813 814 815 816 817 818 819

let init_printer th =
  let isanitize = sanitizer char_to_alpha char_to_alnumus in
  let pr = create_ident_printer black_list ~sanitizer:isanitize in
  Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
  pr

820
let print_task printer_args realize ?old fmt task =
821
  forget_all ();
822 823
  print_prelude fmt printer_args.prelude;
  print_th_prelude task fmt printer_args.th_prelude;
824 825
  (* find theories that are both used and realized from metas *)
  let realized_theories =
Andrei Paskevich's avatar
Andrei Paskevich committed
826
    Task.on_meta meta_realized_theory (fun mid args ->
827 828 829
      match args with
      | [Theory.MAstr s1; Theory.MAstr s2] ->
        let f,id =
830
          let l = Strings.rev_split '.' s1 in
831
          List.rev (List.tl l), List.hd l in
832
        let th = Env.read_theory printer_args.env f id in
833 834
        Mid.add th.Theory.th_name
          (th, (f, if s2 = "" then String.concat "." f else s2)) mid
835 836
      | _ -> assert false
    ) Mid.empty task in
837
  (* two cases: task is use T or task is a real goal *)
838 839 840
    let rec upd_realized_theories = function
    | Some { Task.task_decl = { Theory.td_node =
               Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, pr, _) }}} ->
841
        get_th_name pr.pr_name, [], realized_theories
842
    | Some { Task.task_decl = { Theory.td_node = Theory.Use th }} ->
843
        Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
844
       let id = th.Theory.th_name in
845
       get_th_name id,
846 847 848 849 850 851 852
       th.Theory.th_path,
       Mid.remove id realized_theories
    | Some { Task.task_decl = { Theory.td_node = Theory.Meta _ };
             Task.task_prev = task } ->
        upd_realized_theories task
    | _ -> assert false in
  let thname, thpath, realized_theories = upd_realized_theories task in
Jean-Christophe's avatar
Jean-Christophe committed
853 854
  (* make names as stable as possible by first printing all identifiers *)
  let realized_theories' = Mid.map fst realized_theories in
855 856 857 858 859 860 861
  let realized_symbols = Task.used_symbols realized_theories' in
  let local_decls = Task.local_decls task realized_symbols in
  let symbol_printers =
    let printers =
      Mid.map (fun th ->
        let pr = fresh_printer () in
        Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
Jean-Christophe's avatar
Jean-Christophe committed
862 863
        pr)
        realized_theories' in
864
    Mid.map (fun th ->
865 866
               let _, (p, s) = Mid.find th.Theory.th_name realized_theories in
               let s = if p = thpath then "" else s in
Jean-Christophe's avatar
Jean-Christophe committed
867 868
               (s, th, Mid.find th.Theory.th_name printers))
      realized_symbols in
869 870 871 872 873 874
  let info = {
    info_syn = get_syntax_map task;
    symbol_printers = symbol_printers;
    realization = realize;
  }
  in
Jean-Christophe's avatar
Jean-Christophe committed
875 876 877 878 879 880 881 882 883 884 885 886 887
  (* (\* build IMPORTING declarations *\) *)
  (* let libraries = Hashtbl.create 17 in (\* path -> library name *\) *)
  (* let importing = Hashtbl.create 17 in (\* library name -> theory name *\) *)
  (* let add _ (th, (path, _)) = *)
  (*   if not (Hashtbl.mem libraries path) then begin *)
  (*     let libname = String.concat "_" ("why3" :: path) in *)
  (*     Hashtbl.add libraries path libname *)
  (*   end; *)
  (*   let libname = Hashtbl.find libraries path in *)
  (*   Hashtbl.add importing libname th.Theory.th_name.id_string *)
  (* in *)
  (* Mid.iter add realized_theories; *)
  (* finally, read the old file, if any, and generate the new one *)
888 889 890
  let old = ref (match old with
    | None -> []
    | Some ch -> read_old_script ch)
891
  in
Jean-Christophe's avatar
Jean-Christophe committed
892 893 894 895
  fprintf fmt "@[<hov 1>%s: THEORY@\n@[<hov 1>BEGIN@\n" thname;
  Mid.iter
    (fun _ (th, (path, _)) ->
       let lib = if path = thpath then "" else String.concat "." path ^ "@" in
896
       fprintf fmt "IMPORTING %s%s@\n" lib (get_th_name th.Theory.th_name))
Jean-Christophe's avatar
Jean-Christophe committed
897
    realized_theories;
898 899 900
  fprintf fmt "%% do not edit above this line@\n";
  fprintf fmt
    "%% surround new declarations you insert below with blank lines@\n@\n";
901 902
  print_decls ~old info fmt local_decls;
  output_remaining fmt !old;
903
  fprintf fmt "@]@\nEND %s@\n@]" thname
904

905 906
let print_task_full args ?old fmt task =
  print_task args false ?old fmt task
907

908 909
let print_task_real args ?old fmt task =
  print_task args true  ?old fmt task
910 911

let () = register_printer "pvs" print_task_full
912 913 914
  ~desc:"Printer@ for@ the@ PVS@ proof@ assistant@ \
         (without@ realization@ capabilities)."

915
let () = register_printer "pvs-realize" print_task_real
916 917 918
  ~desc:"Printer@ for@ the@ PVS@ proof@ assistant@ \
         (with@ realization@ capabilities)."

919 920 921 922 923 924

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. "
End:
*)