[Pyrat] printer that is able to print the simple example

caisar.opam

@@ -20,7 +20,7 @@ depends: [
   "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst"] {dev}
+  ["dune" "subst" "--root" "."] {dev}
   [
     "dune"
     "build"
@@ -28,7 +28,8 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files=false"
+    "--promote-install-files"
+    "false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}

config/drivers/pyrat.drv

@@ -6,7 +6,7 @@ prelude "(* this is the prelude for PyRAT *)"
 valid "^Inconsistent assumption$"
 
 
-printer "why3"
+printer "pyrat"
 filename "%f-%t-%g.why"
 
 valid "^File \".*\", line [0-9]+, characters [0-9]+-[0-9]+:Valid"
@@ -144,6 +144,22 @@ theory real.Real
 
 end
 
+theory ieee_float.Float64
+
+  syntax function (.+)  "(%1 + %2)"
+  syntax function (.-)  "(%1 - %2)"
+  syntax function (.*)  "(%1 * %2)"
+  syntax function (./)  "(%1 / %2)"
+  syntax function (.-_) "(-%1)"
+
+  syntax predicate le "(%1 <= %2)"
+  syntax predicate lt  "(%1 <  %2)"
+  syntax predicate ge "(%1 >= %2)"
+  syntax predicate gt  "(%1 >  %2)"
+
+
+end
+
 theory real.RealInfix
 
   syntax function (+.)  "(%1 + %2)"

nnet.opam

@@ -9,7 +9,7 @@ depends: [
   "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst"] {dev}
+  ["dune" "subst" "--root" "."] {dev}
   [
     "dune"
     "build"
@@ -17,7 +17,8 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files=false"
+    "--promote-install-files"
+    "false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}

src/main.ml

@@ -10,6 +10,8 @@ open Cmdliner
 let caisar = "caisar"
 
 let () = Transformations.init ()
+
+let () = Pyrat.init ()
 (* -- Logs. *)
 
 let pp_header =

src/printer/pyrat.ml

@@ -4,10 +4,103 @@
 (*                                                                        *)
 (**************************************************************************)
 
-let print_task args ?old:_ fmt _task =
+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 =
+  match t.Why3.Term.t_node with
+  | Tconst c -> Why3.Constant.(print number_format unsupported_escape) fmt c
+  | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _ | Teps _ ->
+    Why3.Printer.unsupportedTerm t "Pyrat"
+  | Tapp (ls, l) -> (
+    match Why3.Printer.query_syntax info.info_syn ls.ls_name with
+    | Some s -> Why3.Printer.syntax_arguments s (print_term info) fmt l
+    | None -> (
+      match (Why3.Term.Hls.find_opt info.variables ls, l) with
+      | Some s, [] -> Fmt.string fmt s
+      | _ -> Why3.Printer.unsupportedTerm t "Unknown variables"))
+  | Tbinop ((Timplies | Tiff), _, _) | Tnot _ | Ttrue | Tfalse ->
+    Why3.Printer.unsupportedTerm t "Pyrat: Iff, Implies, not"
+  | Tbinop (Tand, _, _) -> Why3.Printer.unsupportedTerm t "Pyrat: Deep and"
+  | Tbinop (Tor, t1, t2) ->
+    Fmt.pf fmt "%a or %a" (print_term info) t1 (print_term info) t2
+
+let print_top_term info fmt t =
+  let print_term info fmt t =
+    (** don't print things we don't know *)
+    if Why3.Term.t_s_all (fun _ -> true)
+        (fun ls -> Why3.Ident.Mid.mem ls.ls_name info.info_syn ||
+                   Why3.Term.Hls.mem info.variables ls)
+        t then
+      print_term info fmt t
+  in
+  match t.Why3.Term.t_node with
+  | Tquant _ -> ()
+  | Tbinop (Tand, t1, t2) ->
+    Fmt.pf fmt "%a@.%a" (print_term info) t1 (print_term info) t2
+  | _ ->  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_term info fmt f
+  | Dprop (Decl.Pgoal, _, f) -> print_top_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
+    | Decl d -> print_decl info fmt d
+    | 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 (_, _) -> ())
+
+let print_task args ?old:_ fmt task =
   let open Why3 in
-  Printer.print_prelude fmt args.Printer.prelude
+  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 () =
+let init () =
   Why3.Printer.register_printer ~desc:"Printer for the PyRAT prover." "pyrat"
     print_task

src/transformations.mli

@@ -6,3 +6,9 @@
 
 val init : unit -> unit
 (** Register the transformations. *)
+
+val meta_input : Why3.Theory.meta
+(** Indicates the position of the input *)
+
+val meta_output : Why3.Theory.meta
+(** Indicates the position of the output *)