Merge pull request #301 from mtzguido/rename

renaming FStarC.Compiler.* -> FStarC.*
FStarLang · Jan 15, 2025 · 7406025 · 7406025
2 parents 1f7f57c + 217bc83
commit 7406025
Show file tree

Hide file tree

Showing 35 changed files with 142 additions and 150 deletions.
diff --git a/mk/boot.mk b/mk/boot.mk
@@ -53,6 +53,7 @@ FSTAR = $(FSTAR_EXE) $(SIL) $(FSTAR_OPTIONS)
 %$(EXTENSION):
 	$(call msg, $(MSG), $(FF))
 	$(FSTAR) --already_cached ',*' $<
+	touch -c $@
 
 %.ml: FF=$(notdir $(subst $(EXTENSION),,$<))
 %.ml: MM=$(basename $(FF))

diff --git a/mk/extraction.mk b/mk/extraction.mk
@@ -9,7 +9,7 @@ CODEGEN := PluginNoLib
 ROOTS := $(shell find $(SRC) -name '*.fst' -o -name '*.fsti')
 FSTAR_OPTIONS += --with_fstarc
 EXTRACT += --extract '-*,+ExtractPulse,+ExtractPulseC,+ExtractPulseOCaml'
-FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Compiler.Effect
+FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Effect
 
 DEPFLAGS += --already_cached 'Prims,FStarC'
 

diff --git a/mk/syntax_extension.mk b/mk/syntax_extension.mk
@@ -9,7 +9,7 @@ CODEGEN := PluginNoLib
 ROOTS := $(shell find $(SRC) -name '*.fst' -o -name '*.fsti')
 FSTAR_OPTIONS += --with_fstarc
 EXTRACT += --extract '-*,+PulseSyntaxExtension'
-FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Compiler.Effect
+FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Effect
 
 DEPFLAGS += --already_cached 'Prims,FStarC'
 

diff --git a/pulse2rust/src/Makefile b/pulse2rust/src/Makefile
@@ -9,7 +9,7 @@ CODEGEN := PluginNoLib
 ROOTS := $(shell find $(SRC) -name '*.fst' -o -name '*.fsti')
 FSTAR_OPTIONS += --with_fstarc
 EXTRACT += --extract '-*,+Pulse2Rust'
-FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Compiler.Effect
+FSTAR_OPTIONS += --lax --MLish --MLish_effect FStarC.Effect
 
 DEPFLAGS += --already_cached 'FStarC'
 

diff --git a/pulse2rust/src/Pulse2Rust.Deps.fst b/pulse2rust/src/Pulse2Rust.Deps.fst
@@ -17,10 +17,9 @@
 module Pulse2Rust.Deps
 
 open FStarC
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 open Pulse2Rust.Env

diff --git a/pulse2rust/src/Pulse2Rust.Deps.fsti b/pulse2rust/src/Pulse2Rust.Deps.fsti
@@ -16,10 +16,9 @@
 
 module Pulse2Rust.Deps
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 open Pulse2Rust.Env

diff --git a/pulse2rust/src/Pulse2Rust.Env.fst b/pulse2rust/src/Pulse2Rust.Env.fst
@@ -16,10 +16,9 @@
 
 module Pulse2Rust.Env
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open FStarC.Class.Setlike
 

diff --git a/pulse2rust/src/Pulse2Rust.Env.fsti b/pulse2rust/src/Pulse2Rust.Env.fsti
@@ -16,10 +16,10 @@
 
 module Pulse2Rust.Env
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 

diff --git a/pulse2rust/src/Pulse2Rust.Extract.fst b/pulse2rust/src/Pulse2Rust.Extract.fst
@@ -16,10 +16,10 @@
 
 module Pulse2Rust.Extract
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 open Pulse2Rust.Env
@@ -73,7 +73,7 @@ let lookup_datacon (g:env) (s:S.mlident) : option (list string & S.mlsymbol) =
     let ropt = find_map decls (lookup_datacon_in_module1 s) in
     match ropt with
     | None -> None
-    | Some tname -> Some (FStarC.Compiler.Util.split k ".", tname)
+    | Some tname -> Some (FStarC.Util.split k ".", tname)
   )
 
 //
@@ -887,7 +887,7 @@ let extract_generic_type_param_trait_bounds (attrs:list S.mlexpr) : list (list s
                       match e.expr with
                       | MLE_Const (MLC_String s) -> s
                       | _ -> failwith "unexpected generic type param bounds")
-         |> List.map (fun bound -> FStarC.Compiler.Util.split bound "::"))
+         |> List.map (fun bound -> FStarC.Util.split bound "::"))
   |> dflt []
 
 let extract_generic_type_params (tyvars:list S.ty_param)

diff --git a/pulse2rust/src/Pulse2Rust.Extract.fsti b/pulse2rust/src/Pulse2Rust.Extract.fsti
@@ -16,10 +16,9 @@
 
 module Pulse2Rust.Extract
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 open Pulse2Rust.Env

diff --git a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fst
@@ -16,9 +16,9 @@
 
 module Pulse2Rust.Rust.Syntax
 
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
-module L = FStarC.Compiler.List
+module L = FStarC.List
 
 let vec_new_fn = "vec_new"
 let panic_fn = "panic"

diff --git a/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti b/pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti
@@ -16,7 +16,7 @@
 
 module Pulse2Rust.Rust.Syntax
 
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 type lit_int_width =
   | I8

diff --git a/pulse2rust/src/Pulse2Rust.fst b/pulse2rust/src/Pulse2Rust.fst
@@ -16,10 +16,10 @@
 
 module Pulse2Rust
 
-open FStarC.Compiler
-open FStarC.Compiler.Util
-open FStarC.Compiler.List
-open FStarC.Compiler.Effect
+open FStarC
+open FStarC.Util
+open FStarC.List
+open FStarC.Effect
 
 open Pulse2Rust.Deps
 open Pulse2Rust.Rust.Syntax
@@ -182,7 +182,7 @@ let extract (files:list string) (odir:string) (libs:string) : unit =
   let root_module = file_to_module_name (let root_file::_ = files in root_file) in
   // print1 "root_module: %s\n" root_module;
   let reachable_defs = collect_reachable_defs d root_module in
-  let external_libs = FStarC.Compiler.Util.split libs "," |> List.map trim_string in
+  let external_libs = FStarC.Util.split libs "," |> List.map trim_string in
   let g = empty_env external_libs d all_modules reachable_defs in
   let _, all_rust_files = List.fold_left (fun (g, all_rust_files) f ->
     // print1 "Extracting file: %s\n" f;

diff --git a/pulse2rust/src/Pulse2Rust.fst.config.json b/pulse2rust/src/Pulse2Rust.fst.config.json
@@ -4,7 +4,7 @@
     "--query_cache",
     "--lax",
     "--MLish",
-    "--MLish_effect", "FStarC.Compiler.Effect",
+    "--MLish_effect", "FStarC.Effect",
     "--with_fstarc",
     "--z3version",
     "4.13.3",

diff --git a/pulse2rust/src/RustBindings.fsti b/pulse2rust/src/RustBindings.fsti
@@ -16,7 +16,7 @@
 
 module RustBindings
 
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 open Pulse2Rust.Rust.Syntax
 

diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst
@@ -1,20 +1,17 @@
 module ExtractPulse
 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.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
 
-module BU = FStarC.Compiler.Util
+module BU = FStarC.Util
 module FC = FStarC.Const
 
 open FStarC.Class.Show

diff --git a/src/extraction/ExtractPulseC.fst b/src/extraction/ExtractPulseC.fst
@@ -1,19 +1,18 @@
 module ExtractPulseC
 
 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 = "Pulse.C.Typestring.cdot" then
       Some '.'
     else if BU.starts_with p "Pulse.C.Typestring.c" then
-      Some (FStarC.Compiler.String.get p (FStar.String.strlen "Pulse.C.Typestring.c"))
+      Some (FStarC.String.get p (FStar.String.strlen "Pulse.C.Typestring.c"))
     else
       None
 

diff --git a/src/extraction/ExtractPulseOCaml.fst b/src/extraction/ExtractPulseOCaml.fst
@@ -7,18 +7,17 @@ extract Quicksort.Task simply, without needing to build fstar.lib in
 OCaml 5. (We could.. but the compiled fstar.lib that F* comes with
 is in OCaml 4.X, so we'd need more build logic.) *)
 
-open FStarC.Compiler.Effect
-open FStarC.Compiler.List
+open FStarC.Effect
+open FStarC.List
 open FStarC
-open FStarC.Compiler
-open FStarC.Compiler.Util
+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.Class.Show

diff --git a/src/extraction/Extraction.fst.config.json b/src/extraction/Extraction.fst.config.json
@@ -4,7 +4,7 @@
     "--query_cache",
     "--lax",
     "--MLish",
-    "--MLish_effect", "FStarC.Compiler.Effect",
+    "--MLish_effect", "FStarC.Effect",
     "--with_fstarc",
     "--z3version",
     "4.13.3",

diff --git a/src/ml/FStarC_Parser_Parse.mly b/src/ml/FStarC_Parser_Parse.mly
@@ -36,9 +36,9 @@ open Fstarcompiler
 open Prims
 open FStar_Pervasives
 open FStarC_Errors
-open FStarC_Compiler_List
-open FStarC_Compiler_Util
-open FStarC_Compiler_Range
+open FStarC_List
+open FStarC_Util
+open FStarC_Range
 
 (* TODO : these files should be deprecated and removed *)
 open FStarC_Parser_Const

diff --git a/src/ml/PulseSyntaxExtension_Parser.ml b/src/ml/PulseSyntaxExtension_Parser.ml
@@ -2,7 +2,7 @@ open Fstarcompiler
 open Lexing
 open FStar_Pervasives_Native
 open FStar_Pervasives
-open FStarC_Compiler_Range
+open FStarC_Range
 open FStarC_Parser_ParseIt
 module FP = FStarC_Parser_Parse
 module PP = Pulse_FStar_Parser
@@ -226,7 +226,7 @@ let parse_decl (s:string) (r:range) =
   with
   | e ->
     let pos = FStarC_Parser_Util.pos_of_lexpos (lexbuf.cur_p) in
-    let r = FStarC_Compiler_Range.mk_range fn pos pos in
+    let r = FStarC_Range.mk_range fn pos pos in
     Inr (Some ("Syntax error", r))
 
 
@@ -240,10 +240,10 @@ let parse_peek_id (s:string) (r:range) : (string, string * range) either =
   with
   | e ->
     let pos = FStarC_Parser_Util.pos_of_lexpos (lexbuf.cur_p) in
-    let r = FStarC_Compiler_Range.mk_range fn pos pos in
-    let msg = FStarC_Compiler_Util.format3 
+    let r = FStarC_Range.mk_range fn pos pos in
+    let msg = FStarC_Util.format3 
          "Failed to peek id, Syntax error @ %s\n%s\n%s\n"
-          (FStarC_Compiler_Range.string_of_range r)
+          (FStarC_Range.string_of_range r)
           (Printexc.to_string e)
           (Printexc.get_backtrace()) in
     Inr (msg, r)
@@ -263,5 +263,5 @@ let parse_lang (s:string) (r:range) =
   with
   | e ->
     let pos = FStarC_Parser_Util.pos_of_lexpos (lexbuf.cur_p) in
-    let r = FStarC_Compiler_Range.mk_range fn pos pos in
+    let r = FStarC_Range.mk_range fn pos pos in
     Inr (Some ("#lang-pulse: Syntax error", r))
diff --git a/src/ml/PulseSyntaxExtension_SyntaxWrapper.ml b/src/ml/PulseSyntaxExtension_SyntaxWrapper.ml
@@ -5,7 +5,7 @@ open Pulse_Syntax_Base
 module U = Pulse_Syntax_Pure
 module S = FStarC_Syntax_Syntax
 type universe = Pulse_Syntax_Base.universe
-type range = FStarC_Compiler_Range.range
+type range = FStarC_Range.range
 let u_zero : universe = U.u_zero
 let u_succ (u:universe) : universe = U.u_succ u
 let u_var (s:string) : universe = U.u_var s
@@ -64,7 +64,7 @@ let tm_arrow (b:binder) (q:S.aqual) (body:comp) : term =
   U.tm_arrow b (map_aqual q) body
 let tm_expr (t:S.term) r : term = Pulse_Syntax_Pure.wr t r
 let tm_unknown r : term = wr r Tm_Unknown
-let tm_emp_inames :term = wr FStarC_Compiler_Range.dummyRange Tm_EmpInames
+let tm_emp_inames :term = wr FStarC_Range.dummyRange Tm_EmpInames
 let tm_add_inv (names:term) (n:term) r : term =
   Pulse_RuntimeUtils.set_range (Pulse_Syntax_Pure.tm_add_inv names n) r
 
@@ -231,7 +231,7 @@ let binder_to_string (env:Env.env) (b:binder)
   = tac_to_string env (Pulse_Syntax_Printer.binder_to_string b)
 let bv_to_string (x:bv) : string =
     x.bv_ppname.name ^ "@" ^
-     (FStarC_Compiler_Util.string_of_int x.bv_index)
+     (FStarC_Util.string_of_int x.bv_index)
 let term_to_string (env:Env.env) (t:term)
   : string
   = tac_to_string env (Pulse_Syntax_Printer.term_to_string t)