isabelle.ml 17.3 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
(********************************************************************)

MARCHE Claude's avatar
MARCHE Claude committed
12 13
(** Isabelle printer
    main author: Stefan Berghofer <stefan.berghofer@secunet.com>
MARCHE Claude's avatar
MARCHE Claude committed
14
*)
15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47

open Format
open Pp
open Ident
open Ty
open Term
open Decl
open Printer

(** Utilities *)

let attrib s pr fmt v = fprintf fmt " %s=\"%a\"" s pr v

let attribs s pr pr' fmt (att, r) = fprintf fmt "%a%a" (attrib s pr) att pr' r

let empty_elem s pr fmt att = fprintf fmt "<%s%a/>" s pr att

let elem s pr pr' fmt (att, x) = fprintf fmt "<%s%a>%a</%s>" s pr att pr' x s

let elem' s pr fmt x = elem s nothing pr fmt ((), x)

let elems s pr pr' fmt ((att, xs) as p) = match xs with
  | [] -> empty_elem s pr fmt att
  | _ -> elem s pr (print_list nothing pr') fmt p

let elems' s pr fmt xs = elems s nothing pr fmt ((), xs)

let pair pr pr' fmt (x, y) = fprintf fmt "%a%a" pr x pr' y

let opt_string_of_bool b = if b then Some "true" else None

(* identifiers *)

48 49 50
let black_list =
  ["o"; "O"]

51 52
let isanitize = sanitizer' char_to_alpha char_to_alnumus char_to_alnum

53
let fresh_printer () =
54
  create_ident_printer black_list ~sanitizer:isanitize
55 56 57

let iprinter = fresh_printer ()

58
let forget_ids () = forget_all iprinter
59

60
let string_of_id id = isanitize id.id_string
61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85

(* type variables *)

let tvprinter = fresh_printer ()

let forget_tvs () = forget_all tvprinter

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

(* 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

(* info *)

type info = {
  info_syn : syntax_map;
  symbol_printers : (string * ident_printer) Mid.t;
  realization : bool;
86
  theories : string Mid.t;
87 88 89 90
}

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

91
let print_altname_path info fmt id =
92
  attribs "altname" html_string
93 94 95 96 97 98 99 100 101 102 103 104 105
    (print_option (attrib "path" string))
    fmt (id.id_string, Mid.find_opt id info.theories)

let print_id_attr info fmt id =
  attribs "name" print_id (print_altname_path info)
    fmt (id, id)

let print_ts info fmt ts = print_id_attr info fmt ts.ts_name

let print_ls info fmt ls = print_id_attr info fmt ls.ls_name

let print_pr info fmt pr = print_id_attr info fmt pr.pr_name

106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
let print_id_real info fmt id =
  try
    let path, ipr = Mid.find id info.symbol_printers in
    attribs "name" string (attrib "path" string) fmt (id_unique ipr id, path)
  with Not_found ->
    attribs "name" print_id (attrib "local" string) fmt (id, "true")

let print_ts_real info fmt ts = print_id_real info fmt ts.ts_name

(** Types *)

let rec print_ty info fmt ty = match ty.ty_node with
  | Tyvar v -> empty_elem "tvar" (attrib "name" print_tv) fmt v
  | Tyapp (ts, tl) when is_ts_tuple ts ->
      elems' "prodt" (print_ty info) fmt tl
  | Tyapp (ts, tl) ->
      begin match query_syntax info.info_syn ts.ts_name with
        | Some s -> syntax_arguments s (print_ty info) fmt tl
        | None -> elems "type" (print_ts_real info) (print_ty info) fmt (ts, tl)
      end

let print_fun_type info fmt (tys, opty) = match opty with
  | None -> elems' "pred" (print_ty info) fmt tys
  | Some ty -> (match tys with
    | [] -> print_ty info fmt ty
    | _ -> elems' "fun" (print_ty info) fmt (tys @ [ty]))

(** Patterns, terms, and formulas *)

let print_ls_type info fmt ls =
  print_fun_type info fmt (ls.ls_args, ls.ls_value)

let print_ls_real info defs fmt (ls, ty) =
  if Sls.mem ls defs
  then elem "var" (attrib "name" print_id)
    (print_fun_type info) fmt (ls.ls_name, ty)
  else elem "const" (print_id_real info)
    (print_fun_type info) fmt (ls.ls_name, ty)

let print_app pr pr' fmt ((h, xs) as p) = match xs with
  | [] -> pr fmt h
  | _ -> elem' "app" (pair pr (print_list nothing pr')) fmt p

let print_var info fmt v =
  elem "var" (attrib "name" print_vs) (print_ty info) fmt (v, v.vs_ty)

let print_const = empty_elem "const" (attrib "name" string)

let print_abs info pr fmt (v, t) =
  elem "abs" (attrib "name" print_vs) (pair (print_ty info) pr) fmt
    (v, (v.vs_ty, t));
  forget_var v

let p_type p = p.pat_ty

161 162 163 164 165 166 167 168 169 170 171 172
let rec split_por p = match p.pat_node with
  | Pwild -> [pat_wild p.pat_ty]
  | Pvar v -> [pat_var v]
  | Pas _ -> assert false
  | Por (p1, p2) -> split_por p1 @ split_por p2
  | Papp (cs, pl) ->
      List.map (fun zs -> pat_app cs zs p.pat_ty)
        (List.fold_right
           (fun xs xss -> List.concat
              (List.map (fun x -> List.map (fun ys -> x :: ys) xss) xs))
           (List.map split_por pl) [[]])

173
let rec print_pat info fmt p = match p.pat_node with
Stefan Berghofer's avatar
Stefan Berghofer committed
174
  | Pwild -> print_const fmt "Pure.dummy_pattern"
175
  | Pvar v -> print_var info fmt v
176
  | Pas _ ->
177
      assert false
178
  | Por _ ->
179 180 181 182 183
      assert false
  | Papp (cs, pl) when is_fs_tuple cs ->
      elems' "prod" (print_pat info) fmt pl
  | Papp (cs, pl) ->
      begin match query_syntax info.info_syn cs.ls_name with
184 185
        | Some s -> gen_syntax_arguments_typed_prec p_type (fun _ -> [||])
            s (fun _ fmt p -> print_pat info fmt p) (print_ty info) p [] fmt pl
186 187 188 189 190 191 192 193 194 195
        | _ -> print_app (print_ls_real info Sls.empty) (print_pat info)
            fmt ((cs, (List.map p_type pl, Some (p.pat_ty))), pl)
      end

let binop_name = function
  | Tand -> "HOL.conj"
  | Tor -> "HOL.disj"
  | Timplies -> "HOL.implies"
  | Tiff -> "HOL.eq"

196 197 198 199 200 201 202 203 204 205 206 207 208 209
let number_format = {
    Number.long_int_support = `Default;
    Number.negative_int_support = `Custom (fun _ _ -> assert false);
    Number.dec_int_support = `Default;
    Number.hex_int_support = `Unsupported;
    Number.oct_int_support = `Unsupported;
    Number.bin_int_support = `Unsupported;
    Number.negative_real_support = `Custom (fun _ _ -> assert false);
    Number.dec_real_support = `Unsupported;
    Number.hex_real_support = `Unsupported;
    Number.frac_real_support =
      `Custom
        ((fun fmt i -> fprintf fmt "<num val=\"%s\"><type name=\"Real.real\"/></num>" i),
         (fun fmt i n -> fprintf fmt
210 211 212 213
                "<app>\
                   <const name=\"Groups.times_class.times\"/>\
                   <num val=\"%s\"><type name=\"Real.real\"/></num>\
                   <num val=\"%s\"/>\
214 215
                 </app>" i n),
         (fun fmt i n -> fprintf fmt
216
                "<app>\
Stefan Berghofer's avatar
Stefan Berghofer committed
217
                   <const name=\"Why3_Real.why3_divide\"/>\
218 219
                   <num val=\"%s\"><type name=\"Real.real\"/></num>\
                   <num val=\"%s\"/>\
220 221 222 223 224 225 226
                 </app>" i n));
  }

let rec print_term info defs fmt t = match t.t_node with
  | Tvar v ->
      print_var info fmt v
  | Tconst c ->
227 228 229 230 231 232
      begin match c with
        | Number.ConstInt _ ->
            fprintf fmt "<num val=\"%a\">%a</num>"
              (Number.print number_format) c (print_ty info) (t_type t)
        | _ -> Number.print number_format fmt c
      end
233 234 235 236 237 238 239 240 241 242 243 244 245
  | Tif (f, t1, t2) ->
      print_app print_const (print_term info defs) fmt ("HOL.If", [f; t1; t2])
  | Tlet (t1, tb) ->
      elem' "app"
        (pair print_const (pair (print_term info defs)
           (print_abs info (print_term info defs))))
        fmt ("HOL.Let", (t1, t_open_bound tb))
  | Tcase (t, bl) ->
      elem' "case"
        (pair (print_term info defs)
           (print_list nothing (print_branch info defs)))
        fmt (t, bl)
  | Teps fb ->
Stefan Berghofer's avatar
Stefan Berghofer committed
246 247 248 249
      elem' "app"
        (pair print_const
           (print_abs info (print_term info defs)))
        fmt ("Hilbert_Choice.Eps", t_open_bound fb)
250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278
  | Tapp (fs, pl) when is_fs_tuple fs ->
      elems' "prod" (print_term info defs) fmt pl
  | Tapp (fs, tl) ->
      begin match query_syntax info.info_syn fs.ls_name with
        | Some s -> syntax_arguments_typed s
            (print_term info defs) (print_ty info) t fmt tl
        | _ -> print_app (print_ls_real info defs) (print_term info defs)
            fmt ((fs, (List.map t_type tl, t.t_ty)), tl)
      end
  | Tquant (q, fq) ->
      let vl, _tl, f = t_open_quant fq in
      print_quant info defs
        (match q with Tforall -> "HOL.All" | Texists -> "HOL.Ex")
        fmt (vl, f)
  | Ttrue ->
      print_const fmt "HOL.True"
  | Tfalse ->
      print_const fmt "HOL.False"
  | Tbinop (b, f1, f2) ->
      print_app print_const (print_term info defs) fmt (binop_name b, [f1; f2])
  | Tnot f ->
      print_app print_const (print_term info defs) fmt ("HOL.Not", [f])

and print_quant info defs s fmt (vl, f) = match vl with
  | [] -> print_term info defs fmt f
  | v :: vl' -> elem' "app" (pair print_const
      (print_abs info (print_quant info defs s))) fmt (s, (v, (vl', f)))

and print_branch info defs fmt br =
279 280 281
  let p, t = t_open_branch br in
  print_list nothing (elem' "pat" (pair (print_pat info) (print_term info defs)))
    fmt (List.map (fun q -> (q, t)) (split_por p));
282 283
  Svs.iter forget_var p.pat_vars

284 285 286 287
let rec dest_conj t = match t.t_node with
  | Tbinop (Tand, f1, f2) -> dest_conj f1 @ dest_conj f2
  | _ -> [t]

288 289 290 291 292
let rec dest_rule vl fl t = match t.t_node with
  | Tquant (Tforall, fq) ->
      let vl', _tl, f = t_open_quant fq in
      dest_rule (vl @ vl') fl f
  | Tbinop (Timplies, f1, f2) ->
293 294
      dest_rule vl (fl @ dest_conj f1) f2
  | _ -> (vl, fl, t)
295 296 297 298 299 300 301 302 303

let rec dest_forall vl t = match t.t_node with
  | Tquant (Tforall, fq) ->
      let vl', _tl, f = t_open_quant fq in
      dest_forall (vl @ vl') f
  | _ -> (vl, t)

(** Declarations *)

304 305 306 307
let print_constr info fmt (cs, pjl) =
  elems "constr" (print_ls info)
    (elem "carg" (print_option (print_ls info)) (print_ty info)) fmt
    (cs, List.combine pjl cs.ls_args)
308 309 310 311

let print_tparams = elems' "params" (empty_elem "param" (attrib "name" print_tv))

let print_data_decl info fmt (ts, csl) =
312
  elem "datatype" (print_ts info)
313 314 315 316 317 318 319 320 321 322 323 324 325
    (pair print_tparams (elems' "constrs" (print_constr info)))
    fmt (ts, (ts.ts_args, csl));
  forget_tvs ()

let print_data_decls info fmt tl =
  let tl = List.filter (fun (ts, _) ->
    not (is_ts_tuple ts || Mid.mem ts.ts_name info.info_syn)) tl in
  if tl <> [] then begin
    elems' "datatypes" (print_data_decl info) fmt tl
  end

let print_statement s pr id info fmt f =
  let vl, prems, concl = dest_rule [] [] f in
326
  elem s pr
327 328 329 330 331 332 333 334 335 336
    (pair
       (elems' "prems" (print_term info Sls.empty))
       (elems' "concls" (print_term info Sls.empty)))
    fmt (id, (prems, dest_conj concl));
  List.iter forget_var vl;
  forget_tvs ()

let print_equivalence_lemma info fmt (ls, ld) =
  let name = Ident.string_unique iprinter
    ((id_unique iprinter ls.ls_name) ^ "_def") in
337
  print_statement "lemma" (attrib "name" string) name info fmt (ls_defn_axiom ld)
338

339
let print_fun_eqn s info defs fmt (ls, ld) =
340
  let vl, t = dest_forall [] (ls_defn_axiom ld) in
341
  elem s (print_altname_path info) (print_term info defs) fmt (ls.ls_name, t);
342 343 344 345 346 347 348
  List.iter forget_var vl

let print_logic_decl info fmt ((ls, _) as d) =
  print_fun_eqn "definition" info (Sls.add ls Sls.empty) fmt d;
  forget_tvs ()

let print_logic_decl info fmt d =
349 350 351
  (* During realization the definition of a "builtin" symbol is
     printed and an equivalence lemma with associated Isabelle function is
     requested *)
352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370
  if not (Mid.mem (fst d).ls_name info.info_syn) then
    print_logic_decl info fmt d
  else if info.realization then
    print_equivalence_lemma info fmt d

let print_recursive_decl info fmt dl =
  let dl_syn, dl_no_syn =
    List.partition (fun (ls, _) ->
      info.realization && (Mid.mem ls.ls_name info.info_syn)) dl in
  let defs = List.fold_left (fun acc (ls, _) ->
    Sls.add ls acc) Sls.empty dl_no_syn in
  if dl_no_syn <> [] then begin
    elems' "function" (print_fun_eqn "eqn" info defs) fmt dl_no_syn;
    forget_tvs ()
  end;
  List.iter (print_equivalence_lemma info fmt) dl_syn

let print_ind info defs fmt (pr, f) =
  let vl, fl, g = dest_rule [] [] f in
371
  elem "rule" (print_pr info)
372 373 374 375 376
    (pair (elems' "prems" (print_term info defs)) (print_term info defs))
    fmt (pr, (fl, g));
  List.iter forget_var vl

let print_ind_decl info defs fmt (ps, bl) =
377
  elem "pred" (print_ls info)
378 379 380 381 382 383 384 385
    (pair (print_ls_type info) (print_list nothing (print_ind info defs)))
    fmt (ps, (ps, bl))

let print_coind fmt s = match s with
  | Ind -> ()
  | Coind -> attrib "coind" string fmt "true"

let print_ind_decls info s fmt tl =
386 387
  let tl_syn, tl_no_syn = List.partition (fun (ps, _) ->
    info.realization && (Mid.mem ps.ls_name info.info_syn)) tl in
388
  let defs = List.fold_left (fun acc (ps, _) ->
389 390 391
    Sls.add ps acc) Sls.empty tl_no_syn in
  if tl_no_syn <> [] then begin
    elems "inductive" print_coind (print_ind_decl info defs) fmt (s, tl_no_syn);
392
    forget_tvs ()
393 394 395 396
  end;
  List.iter (fun (_, rls) ->
    List.iter (fun (pr, f) ->
      print_statement "lemma" (print_pr info) pr info fmt f) rls) tl_syn
397 398 399

let print_type_decl info fmt ts =
  if not (Mid.mem ts.ts_name info.info_syn || is_ts_tuple ts) then
Clément Fumex's avatar
Clément Fumex committed
400
  let def = match ts.ts_def with Alias ty -> Some ty | _ -> None in
401 402
    (elem "typedecl" (print_ts info)
       (pair print_tparams (print_option (print_ty info)))
Clément Fumex's avatar
Clément Fumex committed
403
       fmt (ts, (ts.ts_args, def));
404 405 406 407
     forget_tvs ())

let print_param_decl info fmt ls =
  if not (Mid.mem ls.ls_name info.info_syn) then
408
    (elem "param" (print_ls info) (print_ls_type info) fmt (ls, ls);
409 410 411 412 413 414 415 416 417
     forget_tvs ())

let print_prop_decl info fmt (k, pr, f) =
  let stt = match k with
    | Paxiom when info.realization -> "lemma"
    | Paxiom -> "axiom"
    | Plemma -> "lemma"
    | Pgoal -> "lemma"
  in
418
  print_statement stt (print_pr info) pr info fmt f
419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440

let print_decl info fmt d =
  match d.d_node with
  | Dtype ts ->
      print_type_decl info fmt ts
  | Ddata tl -> print_data_decls info fmt tl
  | Dparam ls ->
      print_param_decl info fmt ls
  | Dlogic [s,_ as ld] when not (Sid.mem s.ls_name d.d_syms) ->
      print_logic_decl info fmt ld
  | Dlogic ll ->
      print_recursive_decl info fmt ll
  | Dind (s, il) ->
      print_ind_decls info s fmt il
  | Dprop (_, pr, _) when not info.realization && Mid.mem pr.pr_name info.info_syn ->
      ()
  | Dprop pr ->
      print_prop_decl info fmt pr

let print_decls info fmt dl =
  print_list nothing (print_decl info) fmt dl

441
let make_thname th = String.concat "." (th.Theory.th_path @
442
  [string_of_id th.Theory.th_name])
443

444
let print_task printer_args realize fmt task =
445 446 447 448 449
  forget_ids ();
  (* find theories that are both used and realized from metas *)
  let realized_theories =
    Task.on_meta meta_realized_theory (fun mid args ->
      match args with
450
      | [Theory.MAstr s1; Theory.MAstr _] ->
451
        let f,id =
452
          let l = Strings.rev_split '.' s1 in
453
          List.rev (List.tl l), List.hd l in
454
        let th = Env.read_theory printer_args.env f id in
455 456 457
        Mid.add th.Theory.th_name (th, s1) mid
      | _ -> assert false
    ) Mid.empty task in
458
  (* two cases: task is use T or task is a real goal *)
459 460 461
  let rec upd_realized_theories = function
    | Some { Task.task_decl = { Theory.td_node =
               Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, pr, _) }}} ->
462
        string_of_id pr.pr_name, realized_theories
463
    | Some { Task.task_decl = { Theory.td_node = Theory.Use th }} ->
464 465
        Sid.iter (fun id -> ignore (id_unique iprinter id)) th.Theory.th_local;
        let id = th.Theory.th_name in
466
        String.concat "." (th.Theory.th_path @ [string_of_id id]),
467
        Mid.remove id realized_theories
468 469 470 471 472
    | Some { Task.task_decl = { Theory.td_node = Theory.Meta _ };
             Task.task_prev = task } ->
        upd_realized_theories task
    | _ -> assert false in
  let thname, realized_theories = upd_realized_theories task in
473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491
  (* make names as stable as possible by first printing all identifiers *)
  let realized_theories' = Mid.map fst realized_theories in
  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;
        pr)
        realized_theories' in
    Mid.map (fun th ->
        (snd (Mid.find th.Theory.th_name realized_theories),
         Mid.find th.Theory.th_name printers))
      realized_symbols in
  let info = {
    info_syn = get_syntax_map task;
    symbol_printers = symbol_printers;
    realization = realize;
492 493
    theories = Mid.map make_thname
      (Task.used_symbols (Task.used_theories task));
494 495 496
  }
  in
  elem "theory"
497
    (attribs "name" string (print_option (attrib "realize" string)))
498 499 500
    (pair
       (elems' "realized" (empty_elem "require"
          (attrib "name" (fun fmt (th, _) ->
501
             string fmt (make_thname th)))))
502 503 504 505 506
       (print_decls info))
    fmt
    ((thname, opt_string_of_bool realize),
     (Mid.values realized_theories, local_decls))

MARCHE Claude's avatar
MARCHE Claude committed
507
let print_task_full args ?old:_ fmt task =
508
  print_task args false fmt task
509

MARCHE Claude's avatar
MARCHE Claude committed
510
let print_task_real args ?old:_ fmt task =
511
  print_task args true fmt task
512 513 514 515 516 517 518 519

let () = register_printer "isabelle" print_task_full
  ~desc:"Printer@ for@ the@ Isabelle@ proof@ assistant@ \
         (without@ realization@ capabilities)."

let () = register_printer "isabelle-realize" print_task_real
  ~desc:"Printer@ for@ the@ Isabelle@ proof@ assistant@ \
         (with@ realization@ capabilities)."