Skip to content

Commit

Permalink
Revert "Parser.Dep: remove wrong logic for FStar.Stubs"
Browse files Browse the repository at this point in the history
Boy was I wrong. But make it right, these go into FStarC.
  • Loading branch information
mtzguido committed Oct 15, 2024
1 parent 2381f11 commit 74253d9
Showing 1 changed file with 16 additions and 0 deletions.
16 changes: 16 additions & 0 deletions src/parser/FStarC.Parser.Dep.fst
Original file line number Diff line number Diff line change
Expand Up @@ -1759,8 +1759,24 @@ let print_full (outc : out_channel) (deps:deps) : unit =
pr "\n\n"
in
let keys = deps_keys deps.dep_graph in
let no_fstar_stubs_file (s:string) : string =
(* If the original filename begins with FStar.Stubs, then remove that,
consistent with what extraction will actually do.
This is VERY IMPORTANT for krml extraction, since we will generate
the krml file even if we're not extracting these files (they are stubs!)
per se. Make sure to run karamel tests (or a check-world) if you change this. *)
let s1 = "FStar.Stubs." in
let s2 = "FStarC." in
let l1 = String.length s1 in
if String.length s >= l1 && String.substring s 0 l1 = s1 then
s2 ^ String.substring s l1 (String.length s - l1)
else
s
in
let output_file ext fst_file =
let basename = Option.get (check_and_strip_suffix (BU.basename fst_file)) in
let basename = no_fstar_stubs_file basename in
let ml_base_name = replace_chars basename '.' "_" in
Find.prepend_output_dir (ml_base_name ^ ext)
in
Expand Down

0 comments on commit 74253d9

Please sign in to comment.