Merge pull request #180 from mtzguido/fstarc

Moving FStar->FStarC
FStarLang · Oct 11, 2024 · 0f3e79a · 0f3e79a
2 parents 90d7ce2 + 017f13e
commit 0f3e79a
Show file tree

Hide file tree

Showing 12 changed files with 2,106 additions and 2,095 deletions.
diff --git a/lib/steel/Steel.ST.Array.fst b/lib/steel/Steel.ST.Array.fst
@@ -19,7 +19,7 @@ module Steel.ST.Array
 module US = FStar.SizeT
 
 /// Lifting a value of universe 0 to universe 1. We use
-/// FStar.Universe, since FStar.Extraction.Krml is set to extract
+/// FStar.Universe, since FStarC.Extraction.Krml is set to extract
 /// those functions to identity.
 
 inline_for_extraction

diff --git a/src/Makefile b/src/Makefile
@@ -38,7 +38,7 @@ boot:
 .PHONY: clean-snapshot
 clean-snapshot:
 	rm -rf ocaml/*/generated ../include/steel/Steel_SpinLock.h
-	rm -f ocaml/plugin/FStar_Parser_Parse.mly
+	rm -f ocaml/plugin/FStarC_Parser_Parse.mly
 
 .PHONY: full-boot
 full-boot:

diff --git a/src/extraction/ExtractSteel.fst b/src/extraction/ExtractSteel.fst
@@ -1,23 +1,24 @@
 module ExtractSteel
-friend FStar.Extraction.Krml
+friend FStarC.Extraction.Krml
 
-(* IMPORTANT: these `open` directives come from FStar.Extraction.Krml.
+(* IMPORTANT: these `open` directives come from FStarC.Extraction.Krml.
    Without them, spurious dependencies on F* ulib will be introduced *)
-open FStar.Compiler.Effect
-open FStar.Compiler.List
+open FStarC
+open FStarC.Compiler.Effect
+open FStarC.Compiler.List
 open FStar
-open FStar.Compiler
-open FStar.Compiler.Util
-open FStar.Extraction
-open FStar.Extraction.ML
-open FStar.Extraction.ML.Syntax
-open FStar.Const
-open FStar.BaseTypes
-
-module BU = FStar.Compiler.Util
-module FC = FStar.Const
-
-open FStar.Extraction.Krml
+open FStarC.Compiler
+open FStarC.Compiler.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 FC = FStarC.Const
+
+open FStarC.Extraction.Krml
 
 let steel_translate_type_without_decay : translate_type_without_decay_t = fun env t ->
   match t with

diff --git a/src/extraction/ExtractSteel.fsti b/src/extraction/ExtractSteel.fsti
@@ -1,3 +1,3 @@
 module ExtractSteel
 
-// this fsti is necessary because we are `friend`ing FStar.Extraction.Krml
+// this fsti is necessary because we are `friend`ing FStarC.Extraction.Krml
diff --git a/src/extraction/ExtractSteelC.fst b/src/extraction/ExtractSteelC.fst
@@ -1,19 +1,19 @@
 module ExtractSteelC
 
-friend FStar.Extraction.Krml
-open FStar.Compiler.Effect
-open FStar.Compiler.List
+friend FStarC.Extraction.Krml
+open FStarC.Compiler.Effect
+open FStarC.Compiler.List
 open FStar
-open FStar.Compiler
-open FStar.Compiler.Util
-open FStar.Extraction
-open FStar.Extraction.ML
-open FStar.Extraction.ML.Syntax
-open FStar.Const
-open FStar.BaseTypes
-open FStar.Extraction.Krml
-module K = FStar.Extraction.Krml
-module BU = FStar.Compiler.Util
+open FStarC.Compiler
+open FStarC.Compiler.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
 
 (* JL: TODO: in stdlib somewhere? *)
 let opt_bind (m: option 'a) (k: 'a -> option 'b): option 'b =
@@ -26,7 +26,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 (FStar.Compiler.String.get p (FStar.String.strlen "Steel.C.Typestring.c"))
+      Some (FStarC.Compiler.String.get p (FStar.String.strlen "Steel.C.Typestring.c"))
     else
       None
 
@@ -330,7 +330,7 @@ let parse_steel_c_fields env (fields: mlty): option (list _) =
       match go fields with
       | None ->
         BU.print1 "Failed to parse fields from %s.\n"
-          (FStar.Extraction.ML.Code.string_of_mlty ([], "") fields);
+          (FStarC.Extraction.ML.Code.string_of_mlty ([], "") fields);
         None
 
       | Some fields ->
@@ -339,14 +339,14 @@ let parse_steel_c_fields env (fields: mlty): option (list _) =
             (fun () (field, ty) ->
                BU.print2 "  %s : %s\n"
                  field
-                 (FStar.Extraction.ML.Code.string_of_mlty ([], "") ty))
+                 (FStarC.Extraction.ML.Code.string_of_mlty ([], "") ty))
             ()
             fields;
           Some (
             List.map
               (fun (field, ty) ->
                  BU.print1 "Translating %s.\n"
-                   (FStar.Extraction.ML.Code.string_of_mlty ([], "") ty);
+                   (FStarC.Extraction.ML.Code.string_of_mlty ([], "") ty);
                  (field, translate_type_without_decay env ty))
               fields)
 
@@ -366,7 +366,7 @@ let define_struct
   match lident_of_typestring tag with
   | None ->
     BU.print1 "Failed to parse struct tag from %s.\n"
-      (FStar.Extraction.ML.Code.string_of_mlty ([], "") tag);
+      (FStarC.Extraction.ML.Code.string_of_mlty ([], "") tag);
     None
   | Some p ->
     define_struct_gen env p [] fields
@@ -386,7 +386,7 @@ let define_union
   match lident_of_typestring tag with
   | None ->
     BU.print1 "Failed to parse union tag from %s.\n"
-      (FStar.Extraction.ML.Code.string_of_mlty ([], "") tag);
+      (FStarC.Extraction.ML.Code.string_of_mlty ([], "") tag);
     None
   | Some p ->
     define_union_gen env p [] fields

diff --git a/src/extraction/ExtractSteelC.fsti b/src/extraction/ExtractSteelC.fsti
@@ -1,2 +1,2 @@
 module ExtractSteelC
-(* this interface is necessary because ExtractSteelC `friend`s FStar.Extraction.Krml *)
+(* this interface is necessary because ExtractSteelC `friend`s FStarC.Extraction.Krml *)
diff --git a/src/extraction/Makefile b/src/extraction/Makefile
@@ -24,5 +24,6 @@ $(OUTPUT_DIRECTORY)/%.ml: %.fst
 		   --odir "$(OUTPUT_DIRECTORY)" \
                    --codegen OCaml \
 		   --MLish \
+		   --MLish_effect "FStarC.Compiler.Effect" \
                    --extract_module $(basename $(notdir $<))
 	chmod -x $@