Merge pull request #455 from hacspec/jonas/generic-printer-aux

Extend generic printer API with auxiliary information

engine/backends/proverif/proverif_backend.ml

@@ -128,7 +128,7 @@ module Print = struct
   let is_known_function fname =
     List.exists ~f:(assoc_known_function fname) library_functions
 
-  class print =
+  class print aux =
     object (print)
       inherit GenericPrint.print as super
       method ty_bool = string "bool"
@@ -314,8 +314,12 @@ module Print = struct
                 }
     end
 
+  type proverif_aux_info = AstItems of AST.item list | NoAuxInfo
+
   include Api (struct
-    let new_print () = (new print :> print_object)
+    type aux_info = proverif_aux_info
+
+    let new_print aux = (new print aux :> print_object)
   end)
 end
 
@@ -368,7 +372,7 @@ module DataTypes = MkSubprinter (struct
     List.filter ~f:(fun item -> [%matches? Type _] item.v) items
 
   let contents items =
-    let contents, _ = Print.items (filter_data_types items) in
+    let contents, _ = Print.items NoAuxInfo (filter_data_types items) in
     contents
 end)
 
@@ -380,8 +384,8 @@ module Letfuns = MkSubprinter (struct
     let process_letfuns, pure_letfuns =
       List.partition_tf ~f:is_process (filter_crate_functions items)
     in
-    let pure_letfuns_print, _ = Print.items pure_letfuns in
-    let process_letfuns_print, _ = Print.items process_letfuns in
+    let pure_letfuns_print, _ = Print.items NoAuxInfo pure_letfuns in
+    let process_letfuns_print, _ = Print.items NoAuxInfo process_letfuns in
     pure_letfuns_print ^ process_letfuns_print
 end)
 
@@ -391,7 +395,9 @@ module Processes = MkSubprinter (struct
   let process_filter item = [%matches? Fn _] item.v && is_process item
 
   let contents items =
-    let contents, _ = Print.items (List.filter ~f:process_filter items) in
+    let contents, _ =
+      Print.items NoAuxInfo (List.filter ~f:process_filter items)
+    in
     contents
 end)
 

engine/bin/dune

@@ -2,7 +2,14 @@
  (name lib)
  (modules lib)
  (wrapped false)
- (libraries hax_engine fstar_backend coq_backend easycrypt_backend proverif_backend logs core)
+ (libraries
+  hax_engine
+  fstar_backend
+  coq_backend
+  easycrypt_backend
+  proverif_backend
+  logs
+  core)
  (preprocess
   (pps
    ppx_yojson_conv

engine/doc/dune

@@ -1,3 +1,3 @@
 (documentation
-  (package hax-engine)
-  (mld_files index))
+ (package hax-engine)
+ (mld_files index))

engine/lib/generic_printer/generic_printer.ml

@@ -429,6 +429,8 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
   include Class
 
   include Api (struct
+    type aux_info = unit
+
     let new_print () = (new Class.print :> print_object)
   end)
 end

engine/lib/generic_printer/generic_printer_base.ml

@@ -346,30 +346,37 @@ module Make (F : Features.T) = struct
     end
 
   module type API = sig
-    val items : item list -> annot_str
-    val item : item -> annot_str
-    val expr : expr -> annot_str
-    val pat : pat -> annot_str
-    val ty : ty -> annot_str
+    type aux_info
+
+    val items : aux_info -> item list -> annot_str
+    val item : aux_info -> item -> annot_str
+    val expr : aux_info -> expr -> annot_str
+    val pat : aux_info -> pat -> annot_str
+    val ty : aux_info -> ty -> annot_str
   end
 
   module Api (NewPrint : sig
-    val new_print : unit -> print_object
+    type aux_info
+
+    val new_print : aux_info -> print_object
   end) =
   struct
     open NewPrint
 
-    let mk (f : print_object -> 'a -> PPrint.document) (x : 'a) : annot_str =
-      let printer = new_print () in
+    let mk (f : print_object -> 'a -> PPrint.document) (aux : aux_info) (x : 'a)
+        : annot_str =
+      let printer = new_print aux in
       let doc = f printer x in
       let buf = Buffer.create 0 in
       PPrint.ToBuffer.pretty 1.0 80 buf doc;
       (Buffer.contents buf, printer#get_span_data ())
 
-    let items : item list -> annot_str = mk (fun p -> p#items)
-    let item : item -> annot_str = mk (fun p -> p#item)
-    let expr : expr -> annot_str = mk (fun p -> p#expr AlreadyPar)
-    let pat : pat -> annot_str = mk (fun p -> p#pat AlreadyPar)
-    let ty : ty -> annot_str = mk (fun p -> p#ty AlreadyPar)
+    type aux_info = NewPrint.aux_info
+
+    let items : aux_info -> item list -> annot_str = mk (fun p -> p#items)
+    let item : aux_info -> item -> annot_str = mk (fun p -> p#item)
+    let expr : aux_info -> expr -> annot_str = mk (fun p -> p#expr AlreadyPar)
+    let pat : aux_info -> pat -> annot_str = mk (fun p -> p#pat AlreadyPar)
+    let ty : aux_info -> ty -> annot_str = mk (fun p -> p#ty AlreadyPar)
   end
 end