Merge pull request #390 from hacspec/fstar-add-fsti

feat(fstar): add `interfaces` flag

cli/options/src/lib.rs

@@ -121,9 +121,25 @@ pub struct FStarOptions {
     /// Number of unrolling of recursive functions to try
     #[arg(long, default_value = "0")]
     fuel: u32,
-    ///  Number of unrolling of inductive datatypes to try
+    /// Number of unrolling of inductive datatypes to try
     #[arg(long, default_value = "1")]
     ifuel: u32,
+    /// Modules for which Hax should extract interfaces (`*.fsti`
+    /// files). By default we extract no interface. This flag expects
+    /// a space-separated list of inclusion clauses. An inclusion
+    /// clause is a Rust path prefixed with `+` or `-`. `-` excludes
+    /// any matched item, `+` includes any matched item. By default,
+    /// every item is included. Rust path chunks can be either a
+    /// concrete string, or a glob (just like bash globs, but with
+    /// Rust paths).
+    #[arg(
+        long,
+        value_parser = parse_inclusion_clause,
+        value_delimiter = ' ',
+        allow_hyphen_values(true)
+    )]
+    // TODO: InclusionKind is a bit too expressive here, see https://github.com/hacspec/hax/issues/397
+    interfaces: Vec<InclusionClause>,
 }
 
 #[derive(JsonSchema, Subcommand, Debug, Clone, Serialize, Deserialize)]

engine/backends/fstar/fstar_ast.ml

@@ -21,10 +21,13 @@ let lid_of_id id = Ident.lid_of_ids [ id ]
 let term (tm : AST.term') = AST.{ tm; range = dummyRange; level = Expr }
 let generate_fresh_ident () = Ident.gen dummyRange
 
-let decl ?(quals = []) ?(attrs = []) (d : AST.decl') =
-  `Item AST.{ d; drange = dummyRange; quals; attrs }
+let decl ?(fsti = true) ?(quals = []) ?(attrs = []) (d : AST.decl') =
+  let decl = AST.{ d; drange = dummyRange; quals; attrs } in
+  if fsti then `Intf decl else `Impl decl
+
+let decls ?(fsti = true) ?(quals = []) ?(attrs = []) x =
+  [ decl ~fsti ~quals ~attrs x ]
 
-let decls ?(quals = []) ?(attrs = []) x = [ decl ~quals ~attrs x ]
 let pat (pat : AST.pattern') = AST.{ pat; prange = dummyRange }
 
 module Attrs = struct
@@ -92,7 +95,7 @@ let term_of_string s =
 
 let decls_of_string s =
   match parse_string (fun x -> Toplevel x) s with
-  | ASTFragment (Inr l, _) -> List.map ~f:(fun i -> `Item i) l
+  | ASTFragment (Inr l, _) -> List.map ~f:(fun i -> `Impl i) l
   | _ -> failwith "parse failed"
 
 let decl_of_string s =