rename FStarC.Compiler -> FStarC

FStarLang/FStar#3666
mtzguido · Jan 15, 2025 · 2896013 · 2896013
1 parent a2c0c09
commit 2896013
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 16 deletions.
diff --git a/mk/extraction.mk b/mk/extraction.mk
@@ -6,7 +6,7 @@ TAG=extraction
 ROOTS=$(shell find src/extraction -name '*.fst' -o -name '*.fsti')
 
 FSTAR_OPTIONS += --lax
-FSTAR_OPTIONS += --MLish --MLish_effect "FStarC.Compiler.Effect"
+FSTAR_OPTIONS += --MLish --MLish_effect "FStarC.Effect"
 FSTAR_OPTIONS += --with_fstarc
 FSTAR_OPTIONS += --already_cached 'Prims,FStarC'
 

diff --git a/src/extraction/ExtractSteel.fst b/src/extraction/ExtractSteel.fst
@@ -4,18 +4,17 @@ friend FStarC.Extraction.Krml
 (* IMPORTANT: these `open` directives come from FStarC.Extraction.Krml.
    Without them, spurious dependencies on F* ulib will be introduced *)
 open FStarC
-open FStarC.Compiler.Effect
-open FStarC.Compiler.List
-open FStar
-open FStarC.Compiler
-open FStarC.Compiler.Util
+open FStarC.Effect
+open FStarC.List
+open FStarC
+open FStarC.Util
 open FStarC.Extraction
 open FStarC.Extraction.ML
 open FStarC.Extraction.ML.Syntax
 open FStarC.Const
 open FStarC.BaseTypes
 
-module BU = FStarC.Compiler.Util
+module BU = FStarC.Util
 module FC = FStarC.Const
 
 open FStarC.Extraction.Krml

diff --git a/src/extraction/ExtractSteelC.fst b/src/extraction/ExtractSteelC.fst
@@ -1,19 +1,18 @@
 module ExtractSteelC
 
 friend FStarC.Extraction.Krml
-open FStarC.Compiler.Effect
-open FStarC.Compiler.List
-open FStar
-open FStarC.Compiler
-open FStarC.Compiler.Util
+open FStarC
+open FStarC.Effect
+open FStarC.List
+open FStarC.Util
 open FStarC.Extraction
 open FStarC.Extraction.ML
 open FStarC.Extraction.ML.Syntax
 open FStarC.Const
 open FStarC.BaseTypes
 open FStarC.Extraction.Krml
 module K = FStarC.Extraction.Krml
-module BU = FStarC.Compiler.Util
+module BU = FStarC.Util
 
 (* JL: TODO: in stdlib somewhere? *)
 let opt_bind (m: option 'a) (k: 'a -> option 'b): option 'b =
@@ -26,7 +25,7 @@ let char_of_typechar (t: mlty): option char =
     if p = "Steel.C.Typestring.cdot" then
       Some '.'
     else if BU.starts_with p "Steel.C.Typestring.c" then
-      Some (FStarC.Compiler.String.get p (FStar.String.strlen "Steel.C.Typestring.c"))
+      Some (FStarC.String.get p (FStar.String.strlen "Steel.C.Typestring.c"))
     else
       None
 

diff --git a/src/extraction/Extraction.fst.config.json b/src/extraction/Extraction.fst.config.json
@@ -4,7 +4,7 @@
     "--lax",
     "--MLish",
     "--with_fstarc",
-    "--MLish_effect", "FStarC.Compiler.Effect",
+    "--MLish_effect", "FStarC.Effect",
     "--cache_dir"
   ],
   "include_dirs": [

diff --git a/src/extraction/Makefile b/src/extraction/Makefile
@@ -19,6 +19,6 @@ $(OUTPUT_DIRECTORY)/%.ml: %.fst
 		   --odir "$(OUTPUT_DIRECTORY)" \
 		   --codegen OCaml \
 		   --MLish \
-		   --MLish_effect "FStarC.Compiler.Effect" \
+		   --MLish_effect "FStarC.Effect" \
 		   --extract_module $(basename $(notdir $<))
 	chmod -x $@