src: Renaming FStarC.Compiler.* -> FStarC.*

Author: mtzguido

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"
 

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",

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
 
 --------------------------------------------------------------------------------
 

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 =

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

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

src/basic/FStarC.Compiler.Bytes.fsti src/basic/FStarC.Bytes.fstisrc/basic/FStarC.Compiler.Bytes.fsti renamed to 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

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

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)
 

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