Skip to content

Commit

Permalink
Feature: add support for configuration files to control how declarati…
Browse files Browse the repository at this point in the history
…ons are grouped within various C files
  • Loading branch information
msprotz committed Feb 14, 2024
1 parent 818bcab commit 8efa0f7
Show file tree
Hide file tree
Showing 5 changed files with 24 additions and 12 deletions.
30 changes: 20 additions & 10 deletions bin/main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ Supported options:|}
"--log", Arg.Set_string O.log_level, " log level, use * for everything";
"--debug", Arg.String debug, " debug options, to be passed to krml";
"--output", Arg.Set_string Krml.Options.tmpdir, " output directory in which to write files";
"--config", Arg.Set_string O.config, " YAML configuration file";
] in
let spec = Arg.align spec in
let files = ref [] in
Expand Down Expand Up @@ -87,15 +88,16 @@ Supported options:|}

Printf.printf "2️⃣ Cleanup\n";
let files =
(* Custom bundling, for now -- since our bundling operates based on
declaration lids, not their original file. *)
let prefix, (f, decls) = Krml.KList.split_at_last files in
let core, decls = List.fold_left (fun (core, decls) decl ->
match Krml.Ast.lid_of_decl decl with
| "core" :: _, _ -> Krml.Bundles.mark_private decl :: core, decls
| _ -> core, decl :: decls
) ([], []) decls in
prefix @ [ "core", List.rev core; f, List.rev decls ]
if !O.config = "" then
files
else
let config = Eurydice.Bundles.load_config !O.config in
let config = Eurydice.Bundles.parse_config config in
let files = Eurydice.Bundles.bundle files config in
let files = Krml.Bundles.topological_sort files in
Krml.KPrint.bprintf "File order after topological sort: %s\n"
(String.concat ", " (List.map fst files));
files
in
let files = Eurydice.Cleanup1.cleanup files in

Expand Down Expand Up @@ -154,10 +156,18 @@ Supported options:|}
let c_name_map = Simplify.allocate_c_names files in
let deps = Bundles.direct_dependencies_with_internal files file_of_map in
let files = List.map (fun (f, ds) ->
let is_fine = function
| ["LowStar"; "Ignore"], "ignore"
| "Eurydice" :: _, _ ->
(* | "core" :: _, _ -> *)
true
| _ ->
false
in
f, List.filter_map (fun d ->
match d with
| Krml.Ast.DExternal (_, _, _, _, lid, t, _) when Krml.Monomorphization.(
has_variables [ t ] || has_cg_array [ t ]
(has_variables [ t ] || has_cg_array [ t ]) && not (is_fine lid)
) ->
KPrint.bprintf "Warning: %a is a type/const-polymorphic assumed function, \
must be implemented with a macro, dropping it\n" Krml.PrintAst.Ops.plid lid;
Expand Down
2 changes: 1 addition & 1 deletion dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,6 @@
(synopsis "A Rust to C translator")
(description "Eurydice builds upon Charon to take existing Rust code and
translate it to C")
(depends ocaml dune terminal))
(depends ocaml dune terminal yaml))

(using menhir 2.1)
1 change: 1 addition & 0 deletions eurydice.opam
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ depends: [
"ocaml"
"dune" {>= "3.7"}
"terminal"
"yaml"
"odoc" {with-doc}
]
build: [
Expand Down
1 change: 1 addition & 0 deletions lib/Options.ml
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
let log_level = ref ""
let config = ref ""
2 changes: 1 addition & 1 deletion lib/dune
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
(library
(name eurydice)
(libraries charon krml))
(libraries charon krml yaml))

0 comments on commit 8efa0f7

Please sign in to comment.