From 62806115b67235df92bcd63ed9512e95e430a347 Mon Sep 17 00:00:00 2001
From: Jonas Schneider-Bensch <jonas@cryspen.com>
Date: Tue, 23 Jan 2024 13:49:15 +0100
Subject: [PATCH] Infrastructure for translating known functions

---
 engine/backends/proverif/proverif_backend.ml | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml
index 93f4370db..b241f8fc9 100644
--- a/engine/backends/proverif/proverif_backend.ml
+++ b/engine/backends/proverif/proverif_backend.ml
@@ -110,6 +110,21 @@ module Print = struct
 
   let iblock f = group >> jump 2 0 >> terminate (break 0) >> f >> group
 
+  (* TODO: Give definitions for core / known library functions, cf issues #447, #448 *)
+  let library_functions : (Concrete_ident_generated.name * (AST.expr list -> document)) list =
+    [ (Core__ops__try_trait__Try__branch, fun args -> empty); (* just an example *)
+
+    ]
+
+  let assoc_known_function fname (known_name, _) =
+    Global_ident.eq_name known_name fname
+
+  let translate_known_function fname args =
+    (List.find_exn ~f:(assoc_known_function fname) library_functions |> snd) args
+
+  let is_known_function fname =
+    List.exists ~f:(assoc_known_function fname) library_functions
+
   class print =
     object (print)
       inherit GenericPrint.print as super
@@ -123,6 +138,9 @@ module Print = struct
             >> match ctx with AlreadyPar -> Fn.id | NeedsPar -> iblock braces
           in
           match e with
+          | App { f = { e = GlobalVar n; _ }; args } when is_known_function n ->
+              translate_known_function n args
+          (* Desugared `?` operator *)
           | Match
               {
                 scrutinee =