pyrat.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(**************************************************************************)

type info = {
  info_syn : Why3.Printer.syntax_map;
  variables : string Why3.Term.Hls.t;
}

let number_format =
  {
    Why3.Number.long_int_support = `Default;
    Why3.Number.negative_int_support = `Default;
    Why3.Number.dec_int_support = `Default;
    Why3.Number.hex_int_support = `Unsupported;
    Why3.Number.oct_int_support = `Unsupported;
    Why3.Number.bin_int_support = `Unsupported;
    Why3.Number.negative_real_support = `Default;
    Why3.Number.dec_real_support = `Default;
    Why3.Number.hex_real_support = `Unsupported;
    Why3.Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
  }

let rec print_term info fmt t =
  let open Why3 in
  match t.Term.t_node with
  | Tbinop ((Timplies | Tiff), _, _)
  | Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
  | Teps _ ->
    Printer.unsupportedTerm t "Not supported by PyRAT"
  | Tbinop (Tand, _, _) -> assert false (* Should appear only at top-level. *)
  | Tconst c -> Constant.(print number_format unsupported_escape) fmt c
  | Tapp (ls, l) -> (
    match Printer.query_syntax info.info_syn ls.ls_name with
    | Some s -> Printer.syntax_arguments s (print_term info) fmt l
    | None -> (
      match (Term.Hls.find_opt info.variables ls, l) with
      | Some s, [] -> Fmt.string fmt s
      | _ -> Printer.unsupportedTerm t "Unknown variable(s)"))
  | Tbinop (Tor, t1, t2) ->
    Fmt.pf fmt "%a or %a" (print_term info) t1 (print_term info) t2

let rec print_top_level_term info fmt t =
  let open Why3 in
  (* Don't print things we don't know. *)
  let t_is_known =
    Term.t_s_all
      (fun _ -> true)
      (fun ls ->
        Ident.Mid.mem ls.ls_name info.info_syn || Term.Hls.mem info.variables ls)
  in
  match t.Term.t_node with
  | Tquant _ -> ()
  | Tbinop (Tand, t1, t2) ->
    if t_is_known t1 && t_is_known t2
    then
      Fmt.pf fmt "%a%a"
        (print_top_level_term info)
        t1
        (print_top_level_term info)
        t2
  | _ -> if t_is_known t then Fmt.pf fmt "%a@." (print_term info) t

let print_decl info fmt d =
  let open Why3 in
  match d.Decl.d_node with
  | Dtype _ -> ()
  | Ddata _ -> ()
  | Dparam _ -> ()
  | Dlogic _ -> ()
  | Dind _ -> ()
  | Dprop (Decl.Plemma, _, _) -> assert false
  | Dprop (Decl.Paxiom, _, f) -> print_top_level_term info fmt f
  | Dprop (Decl.Pgoal, _, f) -> print_top_level_term info fmt f

let rec print_tdecl info fmt task =
  let open Why3 in
  match task with
  | None -> ()
  | Some { Task.task_prev; task_decl; _ } -> (
    print_tdecl info fmt task_prev;
    match task_decl.Theory.td_node with
    | Use _ | Clone _ -> ()
    | Meta (meta, l) when Theory.meta_equal meta Transformations.meta_input -> (
      match l with
      | [ MAls ls; MAint i ] ->
        Why3.Term.Hls.add info.variables ls (Fmt.str "x%i" i)
      | _ -> assert false)
    | Meta (meta, l) when Theory.meta_equal meta Transformations.meta_output
      -> (
      match l with
      | [ MAls ls; MAint i ] ->
        Why3.Term.Hls.add info.variables ls (Fmt.str "y%i" i)
      | _ -> assert false)
    | Meta (_, _) -> ()
    | Decl d -> print_decl info fmt d)

let print_task args ?old:_ fmt task =
  let open Why3 in
  let info =
    {
      info_syn = Discriminate.get_syntax_map task;
      variables = Why3.Term.Hls.create 10;
    }
  in
  Printer.print_prelude fmt args.Printer.prelude;
  print_tdecl info fmt task

let init () =
  Why3.Printer.register_printer ~desc:"Printer for the PyRAT prover." "pyrat"
    print_task