Merge pull request #3666 from mtzguido/rename

src: Renaming FStarC.Compiler.* -> FStarC.*
FStarLang · Jan 15, 2025 · b9200e3 · b9200e3
2 parents 8d3b529 + 5a0183a
commit b9200e3
Show file tree

Hide file tree

Showing 346 changed files with 1,221 additions and 1,227 deletions.
diff --git a/mk/fstar-12.mk b/mk/fstar-12.mk
@@ -2,7 +2,7 @@ FSTAR_OPTIONS += --lax
 # HACK ALERT! --MLish passed by generic.mk to FStarC modules
 # only. Passing it here would mean the library is checked with
 # --MLish, which fails.
-FSTAR_OPTIONS += --MLish_effect 'FStarC.Compiler.Effect'
+FSTAR_OPTIONS += --MLish_effect 'FStarC.Effect'
 FSTAR_OPTIONS += --no_default_includes
 FSTAR_OPTIONS += --include "$(FSTAR_ROOT)/ulib"
 

diff --git a/src/FStarCompiler.fst.config.json b/src/FStarCompiler.fst.config.json
@@ -2,7 +2,7 @@
   "fstar_exe": "../stage0/bin/fstar.exe",
   "options": [
     "--MLish",
-    "--MLish_effect", "FStarC.Compiler.Effect",
+    "--MLish_effect", "FStarC.Effect",
     "--lax",
     "--cache_dir", "../stage1/fstarc.checked",
     "--warn_error",

diff --git a/src/README b/src/README
@@ -6,8 +6,8 @@ Some files are written directly in OCaml:
 
  * The lexer: uses the OCaml Sedlexing library
 
- * Some basic system utilities, like FStarC.Compiler.Util only has an
-   interface in F* and is implemented as FStarC_Compiler_Util.ml
+ * Some basic system utilities, like FStarC.Util only has an
+   interface in F* and is implemented as FStarC_Util.ml
 
 --------------------------------------------------------------------------------
 

diff --git a/src/basic/FStarC.Basefiles.fst b/src/basic/FStarC.Basefiles.fst
@@ -1,10 +1,10 @@
 module FStarC.Basefiles
 
 open FStarC
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 module O  = FStarC.Options
-module BU = FStarC.Compiler.Util
+module BU = FStarC.Util
 module E  = FStarC.Errors
 
 let must_find (fn:string) : string =

diff --git a/src/basic/FStarC.Basefiles.fsti b/src/basic/FStarC.Basefiles.fsti
@@ -1,6 +1,6 @@
 module FStarC.Basefiles
 
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 val prims                       : unit    -> string
 val prims_basename              : unit    -> string

diff --git a/src/basic/FStarC.BigInt.fsti b/src/basic/FStarC.BigInt.fsti
@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 module FStarC.BigInt
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 type bigint
 type t = bigint

diff --git a/src/basic/FStarC.Compiler.Bytes.fsti → src/basic/FStarC.Bytes.fsti b/src/basic/FStarC.Compiler.Bytes.fsti → src/basic/FStarC.Bytes.fsti
@@ -13,8 +13,8 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 *)
-module FStarC.Compiler.Bytes
-open FStarC.Compiler.Effect
+module FStarC.Bytes
+open FStarC.Effect
 open FStarC.BaseTypes
 
 type bytes = array byte

diff --git a/src/basic/FStarC.Common.fst b/src/basic/FStarC.Common.fst
@@ -17,9 +17,9 @@
 *)
 
 module FStarC.Common
-open FStarC.Compiler.Effect
-module List = FStarC.Compiler.List
-module BU = FStarC.Compiler.Util
+open FStarC.Effect
+module List = FStarC.List
+module BU = FStarC.Util
 
 let snapshot (push: 'a -> 'b) (stackref: ref (list 'c)) (arg: 'a) : (int & 'b) = BU.atomically (fun () ->
   let len : int = List.length !stackref in

diff --git a/src/basic/FStarC.Common.fsti b/src/basic/FStarC.Common.fsti
@@ -17,9 +17,9 @@
 *)
 
 module FStarC.Common
-open FStarC.Compiler.Effect
-module List = FStarC.Compiler.List
-module BU = FStarC.Compiler.Util
+open FStarC.Effect
+module List = FStarC.List
+module BU = FStarC.Util
 
 val snapshot (push: 'a -> 'b) (stackref: ref (list 'c)) (arg: 'a) : (int & 'b)
 

diff --git a/src/basic/FStarC.Const.fst b/src/basic/FStarC.Const.fst
@@ -14,15 +14,15 @@
    limitations under the License.
 *)
 module FStarC.Const
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 open FStarC.BigInt
 open FStar.Char
 
 let eq_const c1 c2 =
     match c1, c2 with
     | Const_int (s1, o1), Const_int(s2, o2) ->
-      FStarC.Compiler.Util.ensure_decimal s1 = FStarC.Compiler.Util.ensure_decimal s2 &&
+      FStarC.Util.ensure_decimal s1 = FStarC.Util.ensure_decimal s2 &&
       o1=o2
     | Const_string(a, _), Const_string(b, _) -> a=b
     | Const_reflect l1, Const_reflect l2 -> Ident.lid_equals l1 l2
@@ -55,5 +55,5 @@ let bounds signedness width =
 
 let within_bounds repr signedness width =
   let lower, upper = bounds signedness width in
-  let value = big_int_of_string (FStarC.Compiler.Util.ensure_decimal repr) in
+  let value = big_int_of_string (FStarC.Util.ensure_decimal repr) in
   le_big_int lower value && le_big_int value upper
diff --git a/src/basic/FStarC.Const.fsti b/src/basic/FStarC.Const.fsti
@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 module FStarC.Const
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 open FStarC.BigInt
 open FStar.Char
@@ -31,7 +31,7 @@ type width = | Int8 | Int16 | Int32 | Int64 | Sizet
     and
     Const_int("67108863", None)
     which represent the same number
-    You should do an "FStarC.Compiler.Util.ensure_decimal" on the
+    You should do an "FStarC.Util.ensure_decimal" on the
     string representation before comparing integer constants.
 
     eq_const below does that for you
@@ -45,10 +45,10 @@ type sconst =
   | Const_int         of string & option (signedness & width) (* When None, means "mathematical integer", i.e. Prims.int. *)
   | Const_char        of char (* unicode code point: char in F#, int in OCaml *)
   | Const_real        of string
-  | Const_string      of string & FStarC.Compiler.Range.range                (* UTF-8 encoded *)
+  | Const_string      of string & FStarC.Range.range                (* UTF-8 encoded *)
   | Const_range_of                                           (* `range_of` primitive *)
   | Const_set_range_of                                       (* `set_range_of` primitive *)
-  | Const_range       of FStarC.Compiler.Range.range          (* not denotable by the programmer *)
+  | Const_range       of FStarC.Range.range                  (* not denotable by the programmer *)
   | Const_reify       of option Ident.lid                    (* a coercion from a computation to its underlying repr *)
                                                              (* decorated optionally with the computation effect name *)
   | Const_reflect     of Ident.lid                           (* a coercion from a Tot term to an l-computation type *)

diff --git a/src/basic/FStarC.Compiler.Debug.fst → src/basic/FStarC.Debug.fst b/src/basic/FStarC.Compiler.Debug.fst → src/basic/FStarC.Debug.fst
@@ -14,9 +14,9 @@
    limitations under the License.
 *)
 
-module FStarC.Compiler.Debug
+module FStarC.Debug
 
-module BU = FStarC.Compiler.Util
+module BU = FStarC.Util
 
 (* Mutable state *)
 let anyref = BU.mk_ref false

diff --git a/src/basic/FStarC.Compiler.Debug.fsti → src/basic/FStarC.Debug.fsti b/src/basic/FStarC.Compiler.Debug.fsti → src/basic/FStarC.Debug.fsti
@@ -14,11 +14,11 @@
    limitations under the License.
 *)
 
-module FStarC.Compiler.Debug
+module FStarC.Debug
 
 open FStar open FStarC
-open FStarC.Compiler
-open FStarC.Compiler.Effect
+open FStarC
+open FStarC.Effect
 
 (* State handling for this module. Used by FStarC.Options, which
 is the only module that modifies the debug state. *)

diff --git a/src/basic/FStarC.Defensive.fst b/src/basic/FStarC.Defensive.fst
@@ -1,8 +1,8 @@
 module FStarC.Defensive
 
-open FStarC.Compiler
-open FStarC.Compiler.Effect
-open FStarC.Compiler.Util
+open FStarC
+open FStarC.Effect
+open FStarC.Util
 open FStarC.Class.Binders
 open FStarC.Class.Show
 open FStarC.Class.Ord

diff --git a/src/basic/FStarC.Defensive.fsti b/src/basic/FStarC.Defensive.fsti
@@ -15,8 +15,8 @@
 *)
 module FStarC.Defensive
 
-open FStarC.Compiler.Effect
-open FStarC.Compiler.Range
+open FStarC.Effect
+open FStarC.Range
 open FStarC.Class.Binders
 open FStarC.Class.PP
 

diff --git a/src/basic/FStarC.Dyn.fsti b/src/basic/FStarC.Dyn.fsti
@@ -16,7 +16,7 @@
 
 module FStarC.Dyn
 
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 /// Dynamic casts
 

diff --git a/src/basic/FStarC.Compiler.Effect.fsti → src/basic/FStarC.Effect.fsti b/src/basic/FStarC.Compiler.Effect.fsti → src/basic/FStarC.Effect.fsti
@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 
-module FStarC.Compiler.Effect
+module FStarC.Effect
 
 new_effect ALL = ALL_h unit
 

diff --git a/src/basic/FStarC.Errors.Msg.fst b/src/basic/FStarC.Errors.Msg.fst
@@ -1,8 +1,8 @@
 module FStarC.Errors.Msg
 
-open FStarC.Compiler
-open FStarC.Compiler.Effect
-open FStarC.Compiler.Util
+open FStarC
+open FStarC.Effect
+open FStarC.Util
 open FStarC.Pprint
 
 instance is_error_message_string   : is_error_message string = {
@@ -58,6 +58,6 @@ let rendermsg (ds : list document) : string =
   renderdoc (concat (List.map (fun d -> subdoc (group d)) ds))
 
 let json_of_error_message (err_msg: list document): FStarC.Json.json
-  = FStarC.Compiler.List.map
+  = FStarC.List.map
       (fun doc -> FStarC.Json.JsonStr (renderdoc doc)) err_msg
     |> FStarC.Json.JsonList
diff --git a/src/basic/FStarC.Errors.fst b/src/basic/FStarC.Errors.fst
@@ -17,14 +17,14 @@ module FStarC.Errors
 
 open FStar.Pervasives
 open FStar.String
-open FStarC.Compiler
-open FStarC.Compiler.Effect
-open FStarC.Compiler.List
-open FStarC.Compiler.Util
-open FStarC.Compiler.Range
+open FStarC
+open FStarC.Effect
+open FStarC.List
+open FStarC.Util
+open FStarC.Range
 open FStarC.Options
-module List = FStarC.Compiler.List
-module BU = FStarC.Compiler.Util
+module List = FStarC.List
+module BU = FStarC.Util
 module PP = FStarC.Pprint
 
 open FStarC.Class.Monad
@@ -282,7 +282,7 @@ let compare_issues i1 i2 =
     | None, None -> 0
     | None, Some _ -> -1
     | Some _, None -> 1
-    | Some r1, Some r2 -> FStarC.Compiler.Range.compare_use_range r1 r2
+    | Some r1, Some r2 -> FStarC.Range.compare_use_range r1 r2
 
 let dummy_ide_rng : Range.rng =
   mk_rng "<input>" (mk_pos 1 0) (mk_pos 1 0)
@@ -437,7 +437,7 @@ let warn_unsafe_options rng_opt msg =
     add_one (mk_issue EError rng_opt (mkmsg ("Every use of this option triggers an error: " ^ msg)) (Some warn_on_use_errno) [])
   | _ -> ()
 
-let set_option_warning_callback_range (ropt:option FStarC.Compiler.Range.range) =
+let set_option_warning_callback_range (ropt:option FStarC.Range.range) =
     Options.set_option_warning_callback (warn_unsafe_options ropt)
 
 let t_set_parse_warn_error,

diff --git a/src/basic/FStarC.Errors.fsti b/src/basic/FStarC.Errors.fsti
@@ -16,7 +16,7 @@
 
 module FStarC.Errors
 
-module Range = FStarC.Compiler.Range
+module Range = FStarC.Range
 
 include FStarC.Errors.Codes
 include FStarC.Errors.Msg
@@ -27,13 +27,13 @@ open FStarC.Json {json}
 (* This is a fallback to be used if an error is raised/logged
 with a dummy range. It is set by TypeChecker.Tc.process_one_decl to
 the range of the sigelt being checked. *)
-val fallback_range : FStarC.Compiler.Effect.ref (option Range.range)
+val fallback_range : FStarC.Effect.ref (option Range.range)
 
 (* This range, if set, will be used to limit the range of every
 issue that is logged/raised. This is set, e.g. when checking a top-level
 definition, to the range of the definition, so no error can be reported
 outside of it. *)
-val error_range_bound : FStarC.Compiler.Effect.ref (option Range.range)
+val error_range_bound : FStarC.Effect.ref (option Range.range)
 
 val with_error_bound (r:Range.range) (f : unit -> 'a) : 'a
 
@@ -49,7 +49,7 @@ val call_to_erased_errno : int
 val update_flags : list (error_flag & string) -> list error_setting
 
 (* error code, message, source position, and error context *)
-type error = error_code & error_message & FStarC.Compiler.Range.range & list string
+type error = error_code & error_message & FStarC.Range.range & list string
 
 exception Error   of error
 exception Warning of error
@@ -102,7 +102,7 @@ val clear : unit -> unit
 val set_handler : error_handler -> unit
 val get_ctx : unit -> list string
 
-val set_option_warning_callback_range : ropt:option FStarC.Compiler.Range.range -> unit
+val set_option_warning_callback_range : ropt:option FStarC.Range.range -> unit
 val set_parse_warn_error : (string -> list error_setting) -> unit
 
 val lookup : error_code -> error_setting

diff --git a/src/basic/FStarC.Find.fst b/src/basic/FStarC.Find.fst
@@ -17,10 +17,10 @@ module FStarC.Find
 
 open FStar
 open FStarC
-open FStarC.Compiler
-open FStarC.Compiler.Effect
-open FStarC.Compiler.List
-module BU = FStarC.Compiler.Util
+open FStarC
+open FStarC.Effect
+open FStarC.List
+module BU = FStarC.Util
 open FStarC.Class.Show
 
 let fstar_bin_directory : string =

diff --git a/src/basic/FStarC.Find.fsti b/src/basic/FStarC.Find.fsti
@@ -17,7 +17,7 @@ module FStarC.Find
 (* Utilities for finding files in the include path and related
 operations. *)
 
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 (* A bit silly to have this, but this is the directory where the fstar.exe executable is in. *)
 val fstar_bin_directory : string

diff --git a/src/basic/FStarC.GenSym.fst b/src/basic/FStarC.GenSym.fst
@@ -1,6 +1,6 @@
 module FStarC.GenSym
 
-module Util = FStarC.Compiler.Util
+module Util = FStarC.Util
 
 (* private *)
 let gensym_st = Util.mk_ref 0

diff --git a/src/basic/FStarC.GenSym.fsti b/src/basic/FStarC.GenSym.fsti
@@ -18,7 +18,7 @@
 *)
 module FStarC.GenSym
 
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 (** Obtain a fresh ID. *)
 val next_id             : unit -> int

diff --git a/src/basic/FStarC.Getopt.fsti b/src/basic/FStarC.Getopt.fsti
@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 module FStarC.Getopt
-open FStarC.Compiler.Effect
+open FStarC.Effect
 open FStarC.BaseTypes
 
 val noshort : char

diff --git a/src/basic/FStarC.Hash.fsti b/src/basic/FStarC.Hash.fsti
@@ -1,5 +1,5 @@
 module FStarC.Hash
-open FStarC.Compiler.Effect
+open FStarC.Effect
 
 type hash_code
 

diff --git a/src/basic/FStarC.Compiler.Hints.fsti → src/basic/FStarC.Hints.fsti b/src/basic/FStarC.Compiler.Hints.fsti → src/basic/FStarC.Hints.fsti
@@ -1,8 +1,8 @@
-module FStarC.Compiler.Hints
+module FStarC.Hints
 
 open FStarC
-open FStarC.Compiler
-open FStarC.Compiler.Effect
+open FStarC
+open FStarC.Effect
 
 (** Hints. *)
 type hint = {