Merge pull request #3732 from mtzguido/prelude

Introducing FStar.Prelude, removing special casing for Prims/Pervasives internally

fsharp/base/prims.fs → fsharp/base/Prims.fs

@@ -32,6 +32,7 @@ let ( >= ) (x:int) (y:int)  = x >= y
 let ( < )  (x:int) (y:int) = x < y
 let ( > )  (x:int) (y:int) = x > y
 let (mod) (x:int) (y:int)  = snd (ediv_rem x y)
+let mod_f x y = x mod y
 let ( ~- ) (x:int) = -x
 let abs (x:int) = BigInteger.Abs x
 let of_int (x:FSharp.Core.int) = BigInteger x

fsharp/ulibfs.fsproj

@@ -15,7 +15,7 @@
   </PropertyGroup>
   <ItemGroup>
     <!-- Note, for now we just ignore some modules and or comment out some code in them. -->
-    <Compile Include="base/prims.fs" Link="prims.fs" />
+    <Compile Include="base/Prims.fs" Link="Prims.fs" />
     <Compile Include="base/FStar_Pervasives_Native.fs" Link="FStar_Pervasives_Native.fs" />
     <Compile Include="base/FStar_All.fs" Link="FStar_All.fs" />
     <Compile Include="base/FStar_Char.fs" Link="FStar_Char.fs" />
@@ -51,6 +51,7 @@
     <Compile Include="base/FStar_UInt64.fs" Link="FStar_UInt64.fs" />
     <Compile Include="base/FStar_UInt8.fs" Link="FStar_UInt8.fs" />
 
+    <Compile Link="FStar_NormSteps.fs" Include="extracted\FStar_NormSteps.fs" />
     <Compile Link="FStar_Pervasives.fs" Include="extracted\FStar_Pervasives.fs" />
     <Compile Include="extracted/FStar_Mul.fs" Link="FStar_Mul.fs" />
 

src/basic/FStarC.Array.fsti

@@ -0,0 +1,4 @@
+module FStarC.Array
+
+assume new
+type array : Type -> Type0 

src/basic/FStarC.Bytes.fsti

@@ -17,7 +17,7 @@ module FStarC.Bytes
 open FStarC.Effect
 open FStarC.BaseTypes
 
-type bytes = array byte
+type bytes = FStarC.Array.array byte
 val length : bytes -> int
 val get: bytes -> int -> int
 val zero_create : int -> bytes

src/basic/FStarC.NormSteps.fst

@@ -0,0 +1,86 @@
+module FStarC.NormSteps
+
+(* A mirror of FStar.NormSteps in ulib *)
+
+open Prims
+noeq
+type norm_step =
+  | Simpl // Logical simplification, e.g., [P /\ True ~> P]
+  | Weak // Weak reduction: Do not reduce under binders
+  | HNF // Head normal form
+  | Primops // Reduce primitive operators, e.g., [1 + 1 ~> 2]
+  | Delta // Unfold all non-recursive definitions
+  | Zeta // Unroll recursive calls
+  | ZetaFull // Unroll recursive calls fully
+  | Iota // Reduce case analysis (i.e., match)
+  | NBE // Use normalization-by-evaluation, instead of interpretation (experimental)
+  | Reify // Reify effectful definitions into their representations
+  | NormDebug // Turn on debugging for this call
+  | UnfoldOnly : list string -> norm_step // Unlike Delta, unfold definitions for only the given
+  | UnfoldOnce : list string -> norm_step
+  // names, each string is a fully qualified name
+  // like `A.M.f`
+  // idem
+  | UnfoldFully : list string -> norm_step
+  | UnfoldAttr : list string -> norm_step // Unfold definitions marked with the given attributes
+  | UnfoldQual : list string -> norm_step
+  | UnfoldNamespace : list string -> norm_step
+  | Unmeta : norm_step
+  | Unascribe // Remove type ascriptions [t <: ty ~> t]
+
+irreducible
+let simplify = Simpl
+
+irreducible
+let weak = Weak
+
+irreducible
+let hnf = HNF
+
+irreducible
+let primops = Primops
+
+irreducible
+let delta = Delta
+
+irreducible
+let norm_debug = NormDebug
+
+irreducible
+let zeta = Zeta
+
+irreducible
+let zeta_full = ZetaFull
+
+irreducible
+let iota = Iota
+
+irreducible
+let nbe = NBE
+
+irreducible
+let reify_ = Reify
+
+irreducible
+let delta_only s = UnfoldOnly s
+
+irreducible
+let delta_once s = UnfoldOnce s
+
+irreducible
+let delta_fully s = UnfoldFully s
+
+irreducible
+let delta_attr s = UnfoldAttr s
+
+irreducible
+let delta_qualifier s = UnfoldAttr s
+
+irreducible
+let delta_namespace s = UnfoldNamespace s
+
+irreducible
+let unmeta = Unmeta
+
+irreducible
+let unascribe = Unascribe

src/basic/FStarC.Util.fsti

@@ -18,6 +18,7 @@ module FStarC.Util
 open FStarC.Effect
 open FStarC.Json
 open FStarC.BaseTypes
+open FStarC.Array
 
 exception Impos
 

src/extraction/FStarC.Extraction.ML.Code.fst

@@ -121,6 +121,7 @@ let mlpath_of_mlpath (currentModule : mlsymbol) (x : mlpath) : mlpath =
     match string_of_mlpath x with
     | "Prims.Some" -> ([], "Some")
     | "Prims.None" -> ([], "None")
+    | "Prims.op_Modulus" -> (["Prims"], "mod_f")
     | _ ->
      let ns, x = x in
      (path_of_ns currentModule ns, x)
@@ -158,7 +159,6 @@ let infix_prim_ops = [
     ("op_GreaterThanOrEqual", e_bin_prio_order , ">=");
     ("op_LessThan"          , e_bin_prio_order , "<" );
     ("op_GreaterThan"       , e_bin_prio_order , ">" );
-    ("op_Modulus"           , e_bin_prio_order , "mod" );
 ]
 
 (* -------------------------------------------------------------------- *)
@@ -804,14 +804,6 @@ let doc_of_mllib_r (MLLib mllib) =
         ]
     and for1_mod istop (mod_name, sigmod, MLLib sub) =
         let target_mod_name = Util.flatten_mlpath mod_name in
-        let maybe_open_pervasives =
-            match mod_name with
-            | ["FStar"], "Pervasives" -> []
-            | _ ->
-              let pervasives = Util.flatten_mlpath (["FStar"], "Pervasives") in
-              [hardline;
-               text ("open " ^ pervasives)]
-        in
         let head = reduce1 (if Util.codegen_fsharp()
                             then [text "module";  text target_mod_name]
                             else if not istop
@@ -827,9 +819,6 @@ let doc_of_mllib_r (MLLib mllib) =
         reduce <| (prefix @ [
             head;
             hardline;
-            text "open Prims"] @
-            maybe_open_pervasives @
-            [hardline;
             (match doc with
              | None   -> empty
              | Some s -> cat s hardline);

src/extraction/FStarC.Extraction.ML.Modul.fst

@@ -129,26 +129,26 @@ let rec extract_meta x : option meta =
   match SS.compress x with
   | { n = Tm_fvar fv } ->
       begin match string_of_lid (lid_of_fv fv) with
-      | "FStar.Pervasives.PpxDerivingShow" -> Some PpxDerivingShow
-      | "FStar.Pervasives.PpxDerivingYoJson" -> Some PpxDerivingYoJson
-      | "FStar.Pervasives.CInline" -> Some CInline
-      | "FStar.Pervasives.CNoInline" -> Some CNoInline
-      | "FStar.Pervasives.Substitute" -> Some Substitute
-      | "FStar.Pervasives.Gc" -> Some GCType
-      | "FStar.Pervasives.CAbstractStruct" -> Some CAbstract
-      | "FStar.Pervasives.CIfDef" -> Some CIfDef
-      | "FStar.Pervasives.CMacro" -> Some CMacro
+      | "FStar.Attributes.PpxDerivingShow" -> Some PpxDerivingShow
+      | "FStar.Attributes.PpxDerivingYoJson" -> Some PpxDerivingYoJson
+      | "FStar.Attributes.CInline" -> Some CInline
+      | "FStar.Attributes.CNoInline" -> Some CNoInline
+      | "FStar.Attributes.Substitute" -> Some Substitute
+      | "FStar.Attributes.Gc" -> Some GCType
+      | "FStar.Attributes.CAbstractStruct" -> Some CAbstract
+      | "FStar.Attributes.CIfDef" -> Some CIfDef
+      | "FStar.Attributes.CMacro" -> Some CMacro
       | "Prims.deprecated" -> Some (Deprecated "")
       | _ -> None
       end
   | { n = Tm_app {hd={ n = Tm_fvar fv }; args=[{ n = Tm_constant (Const_string (s, _)) }, _]} } ->
       begin match string_of_lid (lid_of_fv fv) with
-      | "FStar.Pervasives.PpxDerivingShowConstant" -> Some (PpxDerivingShowConstant s)
-      | "FStar.Pervasives.Comment" -> Some (Comment s)
-      | "FStar.Pervasives.CPrologue" -> Some (CPrologue s)
-      | "FStar.Pervasives.CEpilogue" -> Some (CEpilogue s)
-      | "FStar.Pervasives.CConst" -> Some (CConst s)
-      | "FStar.Pervasives.CCConv" -> Some (CCConv s)
+      | "FStar.Attributes.PpxDerivingShowConstant" -> Some (PpxDerivingShowConstant s)
+      | "FStar.Attributes.Comment" -> Some (Comment s)
+      | "FStar.Attributes.CPrologue" -> Some (CPrologue s)
+      | "FStar.Attributes.CEpilogue" -> Some (CEpilogue s)
+      | "FStar.Attributes.CConst" -> Some (CConst s)
+      | "FStar.Attributes.CCConv" -> Some (CCConv s)
       | "Prims.deprecated" -> Some (Deprecated s)
       | _ -> None
       end

src/extraction/FStarC.Extraction.ML.Syntax.fsti

@@ -69,7 +69,7 @@ type mlconstant =
 | MLC_Float  of float
 | MLC_Char   of char
 | MLC_String of string
-| MLC_Bytes  of array byte
+| MLC_Bytes  of FStarC.Array.array byte
 
 type mlpattern =
 | MLP_Wild

src/extraction/FStarC.Extraction.ML.UEnv.fst

@@ -254,6 +254,9 @@ let is_fv_type g fv =
 
 let no_fstar_stubs_ns (ns : list mlsymbol) : list mlsymbol =
   match ns with
+  | "FStar"::"NormSteps"::rest when plug () ->
+    "Fstarcompiler.FStarC"::"NormSteps"::rest
+
   | "FStar"::"Stubs"::rest when plug_no_lib () && Options.Ext.enabled "__guts" -> "FStarC"::rest
 
   (* These 3 modules are special, and are not in the guts. They live in src/ml/full and
@@ -439,29 +442,8 @@ let new_mlpath_of_lident (g:uenv) (x : lident) : mlpath & uenv =
     | "FStar.Pervasives.either"
     | "FStar.Pervasives.Inl"
     | "FStar.Pervasives.Inr"
+      when plug () -> guts mlp
 
-    | "FStar.Pervasives.norm_step"
-    | "FStar.Pervasives.norm_debug"
-    | "FStar.Pervasives.simplify"
-    | "FStar.Pervasives.weak"
-    | "FStar.Pervasives.hnf"
-    | "FStar.Pervasives.primops"
-    | "FStar.Pervasives.delta"
-    | "FStar.Pervasives.norm_debug"
-    | "FStar.Pervasives.zeta"
-    | "FStar.Pervasives.zeta_full"
-    | "FStar.Pervasives.iota"
-    | "FStar.Pervasives.nbe"
-    | "FStar.Pervasives.reify_"
-    | "FStar.Pervasives.delta_only"
-    | "FStar.Pervasives.delta_fully"
-    | "FStar.Pervasives.delta_attr"
-    | "FStar.Pervasives.delta_qualifier"
-    | "FStar.Pervasives.delta_namespace"
-    | "FStar.Pervasives.unmeta"
-    | "FStar.Pervasives.unascribe"
-      when plug ()
-      -> guts mlp
     (* special case to not expose FStarC.Errors *)
     | "FStar.Stubs.Tactics.Common.Stop" ->
       "Fstarcompiler.FStarC"::"Errors"::[], "Stop"

src/fstar/FStarC.Main.fst

@@ -37,6 +37,7 @@ open FStarC.Reflection.V1.Interpreter {}
 open FStarC.Reflection.V2.Interpreter {}
 (* Same, except that it only defines some types for userspace to refer to. *)
 open FStarC.Tactics.Types.Reflection {}
+open FStarC.NormSteps {}
 
 (* process_args:  parses command line arguments, setting FStarC.Options *)
 (*                returns an error status and list of filenames        *)

src/fstar/FStarC.Universal.fst

@@ -95,14 +95,14 @@ let parse (env:uenv) (pre_fn: option string) (fn:string)
     | Some pre_fn ->
         let pre_ast, _ = Parser.Driver.parse_file pre_fn in
         match pre_ast, ast with
-        | Parser.AST.Interface (lid1, decls1, _), Parser.AST.Module (lid2, decls2)
+        | Parser.AST.Interface {mname=lid1; decls=decls1}, Parser.AST.Module {mname=lid2; decls=decls2}
           when Ident.lid_equals lid1 lid2 ->
           let _, env =
             with_dsenv_of_env env (FStarC.ToSyntax.Interleave.initialize_interface lid1 decls1)
           in
           with_dsenv_of_env env (FStarC.ToSyntax.Interleave.interleave_module ast true)
 
-        | Parser.AST.Interface (lid1, _, _), Parser.AST.Module (lid2, _) ->
+        | Parser.AST.Interface {mname=lid1}, Parser.AST.Interface {mname=lid2} ->
           (* Names do not match *)
           Errors.raise_error lid1
             Errors.Fatal_PreModuleMismatch
@@ -181,8 +181,8 @@ let tc_one_fragment curmod (env:TcEnv.env_t) frag =
 
   let range_of_first_mod_decl modul =
     match modul with
-    | Parser.AST.Module (_, { Parser.AST.drange = d } :: _)
-    | Parser.AST.Interface (_, { Parser.AST.drange = d } :: _, _) -> d
+    | Parser.AST.Module {decls = d :: _} -> d.drange
+    | Parser.AST.Interface {decls = d :: _} -> d.drange
     | _ -> Range.dummyRange in
 
   let filter_lang_decls (d:FStarC.Parser.AST.decl) =
@@ -218,8 +218,8 @@ let tc_one_fragment curmod (env:TcEnv.env_t) frag =
         let open FStarC.Parser.AST in
         let decls =
           match ast_modul with
-          | Module (_, decls)
-          | Interface (_, decls, _) -> decls
+          | Module {decls}
+          | Interface {decls} -> decls
         in
         List.filter filter_lang_decls decls
       in
@@ -252,7 +252,14 @@ let tc_one_fragment curmod (env:TcEnv.env_t) frag =
     //We already have a parsed decl, usually from FStarC.Interactive.Incremental
     match d.d with
     | FStarC.Parser.AST.TopLevelModule lid ->
-      check_module_name_declaration (FStarC.Parser.AST.Module(lid, [d]))
+      let no_prelude =
+        d.attrs |> List.existsb (function t ->
+          match t.tm with
+          | Const (FStarC.Const.Const_string ("no_prelude", _)) -> true
+          | _ -> false)
+      in
+      let modul = Parser.AST.Module { mname = lid; decls = [d]; no_prelude } in
+      check_module_name_declaration modul
     | _ -> 
       check_decls [d]
   )
@@ -279,7 +286,7 @@ let tc_one_fragment curmod (env:TcEnv.env_t) frag =
 let load_interface_decls env interface_file_name : TcEnv.env_t =
   let r = Pars.parse None (Pars.Filename interface_file_name) in
   match r with
-  | Pars.ASTFragment (Inl (FStarC.Parser.AST.Interface(l, decls, _)), _) ->
+  | Pars.ASTFragment (Inl (FStarC.Parser.AST.Interface {mname=l; decls}), _) ->
     snd (with_dsenv_of_tcenv env <| FStarC.ToSyntax.Interleave.initialize_interface l decls)
   | Pars.ASTFragment _ ->
     Errors.raise_error0 FStarC.Errors.Fatal_ParseErrors

src/interactive/FStarC.Interactive.Ide.fst

@@ -537,8 +537,8 @@ let run_segment (st: repl_state) (code: string) =
     match Parser.Driver.parse_fragment None frag with
     | Parser.Driver.Empty -> []
     | Parser.Driver.Decls decls
-    | Parser.Driver.Modul (Parser.AST.Module (_, decls))
-    | Parser.Driver.Modul (Parser.AST.Interface (_, decls, _)) -> decls in
+    | Parser.Driver.Modul (Parser.AST.Module {decls})
+    | Parser.Driver.Modul (Parser.AST.Interface {decls}) -> decls in
 
   match with_captured_errors st.repl_env Util.sigint_ignore
             (fun _ -> Some <| collect_decls ()) with

src/interactive/FStarC.Interactive.PushHelper.fst

@@ -364,7 +364,8 @@ let add_module_completions this_fname deps table =
   let loaded_mods_set =
     List.fold_left
       (fun acc dep -> psmap_add acc (Parser.Dep.lowercase_module_name dep) true)
-      (psmap_empty ()) (Basefiles.prims () :: deps) in // Prims is an implicit dependency
+      (psmap_empty ()) deps
+  in
   let loaded modname =
     psmap_find_default loaded_mods_set modname false in
   let this_mod_key =

src/ml/FStarC_Array.ml

@@ -0,0 +1,2 @@
+type 't array' = 't array
+type 't array = 't array'