Merge pull request #615 from hacspec/inline-backend-macro-items

Proc-macro for backend prelude/epilogue to Rust items

cli/options/src/lib.rs

@@ -259,10 +259,11 @@ pub struct TranslationOptions {
     /// prefixed by modifiers are processed from left to right,
     /// excluding or including items. Each pattern selects a number of
     /// item. The modifiers are:
-    ///
-    ///  - `+`: includes the selected items with their dependencies,
-    /// transitively (e.g. if function `f` calls `g` which in turn
-    /// calls `h`, then `+k::f` includes `f`, `g` and `h`)
+
+    /// {n}{n} - `+`: includes the selected items with their
+    /// dependencies, transitively (e.g. if function `f` calls `g`
+    /// which in turn calls `h`, then `+k::f` includes `f`, `g` and
+    /// `h`)
 
     /// {n} - `+~`: includes the selected items with their direct
     /// dependencies only (following the previous example, `+~k::f`
@@ -299,15 +300,15 @@ pub struct BackendOptions {
     /// Enable engine debugging: dumps the AST at each phase.
     ///
     /// The value of `<DEBUG_ENGINE>` can be either:
-    ///
-    ///  - `interactive` (or `i`): enables debugging of the engine,
+
+    /// {n}{n} - `interactive` (or `i`): enables debugging of the engine,
     /// and visualize interactively in a webapp how a crate was
     /// transformed by each phase, both in Rust-like syntax and
     /// browsing directly the internal AST. By default, the webapp is
     /// hosted on `http://localhost:8000`, the port can be override by
     /// setting the `HAX_DEBUGGER_PORT` environment variable.
-    ///
-    /// - `<FILE>` or `file:<FILE>`: outputs the different AST as JSON
+
+    /// {n} - `<FILE>` or `file:<FILE>`: outputs the different AST as JSON
     /// to `<FILE>`. `<FILE>` can be either [-] or a path.
     #[arg(short, long = "debug-engine")]
     pub debug_engine: Option<DebugEngineMode>,

engine/backends/fstar/fstar_backend.ml

@@ -573,16 +573,20 @@ struct
              kind = UnsupportedMacro { id = [%show: global_ident] macro };
              span = e.span;
            }
-    | Quote { contents; _ } ->
-        List.map
-          ~f:(function
-            | `Verbatim code -> code
-            | `Expr e -> pexpr e |> term_to_string
-            | `Pat p -> ppat p |> pat_to_string)
-          contents
-        |> String.concat |> F.term_of_string
+    | Quote quote -> pquote e.span quote |> F.term_of_string
     | _ -> .
 
+  (** Prints a `quote` to a string *)
+  and pquote span { contents; _ } =
+    List.map
+      ~f:(function
+        | `Verbatim code -> code
+        | `Expr e -> pexpr e |> term_to_string
+        | `Pat p -> ppat p |> pat_to_string
+        | `Typ p -> pty span p |> term_to_string)
+      contents
+    |> String.concat
+
   and parm { arm = { arm_pat; body } } = (ppat arm_pat, None, pexpr body)
 
   module FStarBinder = struct
@@ -793,7 +797,12 @@ struct
         F.mk_e_app effect (if is_lemma then args else typ :: args)
 
   let rec pitem (e : item) :
-      [> `Impl of F.AST.decl | `Intf of F.AST.decl | `Comment of string ] list =
+      [> `Impl of F.AST.decl
+      | `Intf of F.AST.decl
+      | `VerbatimImpl of string
+      | `VerbatimIntf of string
+      | `Comment of string ]
+      list =
     try pitem_unwrapped e
     with Diagnostics.SpanFreeError.Exn error ->
       let error = Diagnostics.SpanFreeError.payload error in
@@ -805,7 +814,12 @@ struct
       ]
 
   and pitem_unwrapped (e : item) :
-      [> `Impl of F.AST.decl | `Intf of F.AST.decl | `Comment of string ] list =
+      [> `Impl of F.AST.decl
+      | `Intf of F.AST.decl
+      | `VerbatimImpl of string
+      | `VerbatimIntf of string
+      | `Comment of string ]
+      list =
     match e.v with
     | Alias { name; item } ->
         let pat =
@@ -1248,6 +1262,20 @@ struct
         let tcinst = F.term @@ F.AST.Var FStar_Parser_Const.tcinstance_lid in
         F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ]
         @@ F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ])
+    | Quote quote ->
+        let fstar_opts =
+          Attrs.find_unique_attr e.attrs ~f:(function
+            | ItemQuote q -> Some q.fstar_options
+            | _ -> None)
+          |> Option.value_or_thunk ~default:(fun _ ->
+                 Error.assertion_failure e.span
+                   "Malformed `Quote` item: could not find a ItemQuote payload")
+          |> Option.value ~default:Types.{ intf = true; impl = false }
+        in
+        (if fstar_opts.intf then [ `VerbatimIntf (pquote e.span quote) ]
+        else [])
+        @
+        if fstar_opts.impl then [ `VerbatimImpl (pquote e.span quote) ] else []
     | HaxError details ->
         [
           `Comment
@@ -1261,7 +1289,12 @@ end
 module type S = sig
   val pitem :
     item ->
-    [> `Impl of F.AST.decl | `Intf of F.AST.decl | `Comment of string ] list
+    [> `Impl of F.AST.decl
+    | `Intf of F.AST.decl
+    | `VerbatimImpl of string
+    | `VerbatimIntf of string
+    | `Comment of string ]
+    list
 end
 
 let make (module M : Attrs.WITH_ITEMS) ctx =
@@ -1311,6 +1344,8 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
   |> List.concat_map ~f:(function
        | `Impl i -> [ mk_impl (decl_to_string i) ]
        | `Intf i -> [ mk_intf (decl_to_string i) ]
+       | `VerbatimIntf s -> if interface_mode then [ `Intf s ] else [ `Impl s ]
+       | `VerbatimImpl s -> if interface_mode then [ `Impl s ] else [ `Impl s ]
        | `Comment s ->
            let s = "(* " ^ s ^ " *)" in
            if interface_mode then [ `Impl s; `Intf s ] else [ `Impl s ])

engine/backends/proverif/proverif_backend.ml

@@ -624,6 +624,7 @@ module Make (Options : OPTS) : MAKE = struct
                 ^^ separate_map hardline
                      (fun variant -> fun_and_reduc name variant)
                      variants
+          | Quote quote -> print#quote quote
           | _ -> empty
 
         method! expr_let : lhs:pat -> rhs:expr -> expr fn =

engine/bin/lib.ml

@@ -126,7 +126,15 @@ let run (options : Types.engine_options) : Types.output =
 let main (options : Types.engine_options) =
   Printexc.record_backtrace true;
   let result =
-    try Ok (run options) with e -> Error (e, Printexc.get_raw_backtrace ())
+    try Ok (run options) with
+    | Hax_engine.Diagnostics.SpanFreeError.Exn exn ->
+        Error
+          ( Failure
+              ("Uncatched hax exception (please report, this should not \
+                appear): "
+              ^ [%show: Hax_engine.Diagnostics.SpanFreeError.t] exn),
+            Printexc.get_raw_backtrace () )
+    | e -> Error (e, Printexc.get_raw_backtrace ())
   in
   match result with
   | Ok results ->

engine/lib/ast.ml

@@ -258,15 +258,18 @@ functor
         }
       | Closure of { params : pat list; body : expr; captures : expr list }
       | EffectAction of { action : F.monadic_action; argument : expr }
-      | Quote of {
-          contents : [ `Verbatim of string | `Expr of expr | `Pat of pat ] list;
-          witness : F.quote;
-        }
+      | Quote of quote
           (** A quotation is an inlined piece of backend code
               interleaved with Rust code *)
 
     and expr = { e : expr'; span : span; typ : ty }
 
+    and quote = {
+      contents :
+        [ `Verbatim of string | `Expr of expr | `Pat of pat | `Typ of ty ] list;
+      witness : F.quote;
+    }
+
     and supported_monads =
       | MException of ty
           (** a exception monad, which we use to handle early returns *)
@@ -388,6 +391,7 @@ functor
           is_external : bool;
           rename : string option;
         }
+      | Quote of quote
       | HaxError of string
       | NotImplementedYet
 

engine/lib/ast_visitors.ml

@@ -434,17 +434,7 @@ functor
               in
               let argument = self#visit_expr env record_payload.argument in
               EffectAction { action; argument }
-          | Quote { contents; witness } ->
-              let contents =
-                self#visit_list
-                  (fun env -> function
-                    | `Verbatim code -> `Verbatim code
-                    | `Expr e -> `Expr (self#visit_expr env e)
-                    | `Pat p -> `Pat (self#visit_pat env p))
-                  env contents
-              in
-              let witness = self#visit_feature_quote env witness in
-              Quote { contents; witness }
+          | Quote quote -> Quote (self#visit_quote env quote)
 
         method visit_expr (env : 'env) (this : expr) : expr =
           let e = self#visit_expr' env this.e in
@@ -453,6 +443,20 @@ functor
           let out : expr = { e; span; typ } in
           out
 
+        method visit_quote (env : 'env) ({ contents; witness } : quote) : quote
+            =
+          let contents =
+            self#visit_list
+              (fun env -> function
+                | `Verbatim code -> `Verbatim code
+                | `Expr e -> `Expr (self#visit_expr env e)
+                | `Pat p -> `Pat (self#visit_pat env p)
+                | `Typ t -> `Typ (self#visit_ty env t))
+              env contents
+          in
+          let witness = self#visit_feature_quote env witness in
+          { contents; witness }
+
         method visit_supported_monads (env : 'env) (this : supported_monads)
             : supported_monads =
           match this with
@@ -678,6 +682,7 @@ functor
                 self#visit_option self#visit_string env record_payload.rename
               in
               Use { path; is_external; rename }
+          | Quote quote -> Quote (self#visit_quote env quote)
           | HaxError x0 ->
               let x0 = self#visit_string env x0 in
               HaxError x0
@@ -1461,22 +1466,9 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               (EffectAction { action; argument }, reduce_acc)
-          | Quote { contents; witness } ->
-              let list, reduce_acc =
-                self#visit_list
-                  (fun env -> function
-                    | `Verbatim code -> (`Verbatim code, self#zero)
-                    | `Expr e ->
-                        let e, acc = self#visit_expr env e in
-                        (`Expr e, acc)
-                    | `Pat p ->
-                        let p, acc = self#visit_pat env p in
-                        (`Pat p, acc))
-                  env contents
-              in
-              let witness, reduce_acc' = self#visit_feature_quote env witness in
-              let reduce_acc = self#plus reduce_acc reduce_acc' in
-              (Quote { contents; witness }, reduce_acc)
+          | Quote quote ->
+              let quote, acc = self#visit_quote env quote in
+              (Quote quote, acc)
 
         method visit_expr (env : 'env) (this : expr) : expr * 'acc =
           let e, reduce_acc = self#visit_expr' env this.e in
@@ -1487,6 +1479,27 @@ functor
           let out : expr = { e; span; typ } in
           (out, reduce_acc)
 
+        method visit_quote (env : 'env) ({ contents; witness } : quote)
+            : quote * 'acc =
+          let list, reduce_acc =
+            self#visit_list
+              (fun env -> function
+                | `Verbatim code -> (`Verbatim code, self#zero)
+                | `Expr e ->
+                    let e, acc = self#visit_expr env e in
+                    (`Expr e, acc)
+                | `Pat p ->
+                    let p, acc = self#visit_pat env p in
+                    (`Pat p, acc)
+                | `Typ t ->
+                    let t, acc = self#visit_ty env t in
+                    (`Typ t, acc))
+              env contents
+          in
+          let witness, reduce_acc' = self#visit_feature_quote env witness in
+          let reduce_acc = self#plus reduce_acc reduce_acc' in
+          ({ contents; witness }, reduce_acc)
+
         method visit_supported_monads (env : 'env) (this : supported_monads)
             : supported_monads * 'acc =
           match this with
@@ -1817,6 +1830,9 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               (Use { path; is_external; rename }, reduce_acc)
+          | Quote quote ->
+              let quote, acc = self#visit_quote env quote in
+              (Quote quote, acc)
           | HaxError x0 ->
               let x0, reduce_acc = self#visit_string env x0 in
               (HaxError x0, reduce_acc)
@@ -2602,18 +2618,7 @@ functor
               let reduce_acc' = self#visit_expr env record_payload.argument in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               reduce_acc
-          | Quote { contents; witness } ->
-              let reduce_acc =
-                self#visit_list
-                  (fun env -> function
-                    | `Verbatim code -> self#zero
-                    | `Expr e -> self#visit_expr env e
-                    | `Pat p -> self#visit_pat env p)
-                  env contents
-              in
-              let reduce_acc' = self#visit_feature_quote env witness in
-              let reduce_acc = self#plus reduce_acc reduce_acc' in
-              reduce_acc
+          | Quote quote -> self#visit_quote env quote
 
         method visit_expr (env : 'env) (this : expr) : 'acc =
           let reduce_acc = self#visit_expr' env this.e in
@@ -2623,6 +2628,20 @@ functor
           let reduce_acc = self#plus reduce_acc reduce_acc' in
           reduce_acc
 
+        method visit_quote (env : 'env) ({ contents; witness } : quote) : 'acc =
+          let reduce_acc =
+            self#visit_list
+              (fun env -> function
+                | `Verbatim code -> self#zero
+                | `Expr e -> self#visit_expr env e
+                | `Pat p -> self#visit_pat env p
+                | `Typ t -> self#visit_ty env t)
+              env contents
+          in
+          let reduce_acc' = self#visit_feature_quote env witness in
+          let reduce_acc = self#plus reduce_acc reduce_acc' in
+          reduce_acc
+
         method visit_supported_monads (env : 'env) (this : supported_monads)
             : 'acc =
           match this with
@@ -2918,6 +2937,7 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               reduce_acc
+          | Quote quote -> self#visit_quote env quote
           | HaxError x0 ->
               let reduce_acc = self#visit_string env x0 in
               reduce_acc