FStarLang#1087 Add note on Map/Set extraction issues + few more F# mo…

…dules

ulib/fs/FStar_CommonST.fs

@@ -0,0 +1,26 @@
+module FStar_CommonST
+
+open FStar_Monotonic_Heap
+
+let read x = x.contents
+
+let op_Bang x = read x
+
+let write x y = x.contents <- y
+
+let op_Colon_Equals x y = write x y
+
+let uid = ref 0
+
+let alloc contents =
+  let id = incr uid; !uid in
+  let r = { id = id; contents = contents } in
+  r
+
+let recall = (fun r -> ())
+let get () = ()
+
+type 'a witnessed = | C
+
+let gst_witness = (fun r -> ())
+let gst_recall = (fun r -> ())

ulib/fs/FStar_HyperStack_All.fs

@@ -0,0 +1,8 @@
+module FStar_HyperStack_All
+
+let failwith x = failwith x
+let exit i = exit (Microsoft.FSharp.Core.Operators.int i)
+let pipe_right a f = f a
+let pipe_left f a = f a
+let try_with f1 f2 = try f1 () with | e -> f2 e
+

ulib/fs/FStar_HyperStack_IO.fs

@@ -0,0 +1,6 @@
+module FStar_HyperStack_IO
+
+open Prims
+
+let print_string : Prims.string -> Prims.unit =
+  FStar_IO.print_string

ulib/fs/FStar_HyperStack_ST.fs

@@ -0,0 +1,85 @@
+module FStar_HyperStack_ST
+
+open FStar_CommonST
+
+// TODO: Need to fix the order of compilation for extracted modules. 
+//       This realised module depends on some of the extracted modules.
+
+//open FStar_Monotonic_HyperHeap
+//open FStar_Monotonic_HyperStack
+
+//open FStar_HyperStack
+
+let push_frame () = ()
+let pop_frame () = ()
+
+let root = ()
+
+let def_rid = root
+
+//let salloc (contents:'a) :('a reference) =
+//  let r = FStar_CommonST.alloc contents in
+//  MkRef (root, r)
+
+//let salloc_mm (contents:'a) :('a reference) =
+//  let r = FStar_CommonST.alloc contents in
+//  MkRef (root, r)
+
+//let sfree r = ()
+
+//let new_region = (fun r0 -> def_rid)
+//let new_colored_region = (fun r0 c -> def_rid)
+
+//let ralloc i (contents:'a) :('a reference) =
+//  let r = FStar_CommonST.alloc contents in
+//  MkRef (i, r)  
+
+//let ralloc_mm i (contents:'a) :('a reference) =
+//  let r = FStar_CommonST.alloc contents in
+//  MkRef (i, r)  
+
+//let rfree r = ()
+
+//let op_Colon_Equals r v = match r with
+//  | MkRef (_, r) -> op_Colon_Equals r v
+
+//let op_Bang r = match r with
+//  | MkRef (_, r) -> op_Bang r
+
+//let read = op_Bang
+
+//let write = op_Colon_Equals
+
+//let get () = HS (Prims.parse_int "0", FStar_Map.const FStar_Monotonic_Heap.emp, def_rid)
+
+//let recall = (fun r -> ())
+
+//let recall_region = (fun r -> ())
+//let witness_region _ = ()
+//let witness_hsref _ = ()
+//type erid = rid
+
+//type 'a ref = 'a FStar_HyperStack.reference
+//type ('a, 'b) mreference = 'a ref
+//type 'a reference = 'a ref
+//let alloc = salloc
+//type ('a, 'b) mref = 'a ref
+//type ('a, 'b, 'c) m_rref = 'b ref
+//type ('a, 'b, 'c, 'd, 'e) stable_on_t = unit
+//let mr_witness _ _ _ _ _ = ()
+//let testify _ = ()
+//let testify_forall _ = ()
+//let testify_forall_region_contains_pred _ _ = ()
+
+//type ex_rid = erid
+//type 'a witnessed = 'a FStar_CommonST.witnessed
+//type ('a, 'b, 'c, 'd) stable_on = unit
+//type ('a, 'b, 'c, 'd) token = unit
+//let witness_p _ _ = ()
+//let recall_p _ _ = ()
+
+//type drgn = rid
+//let new_drgn _ = ()
+//let free_drgn _ = ()
+//let ralloc_drgn = ralloc
+//let ralloc_drgn_mm = ralloc_mm

ulib/fs/FStar_Monotonic_Heap.fs

@@ -3,7 +3,9 @@ module Obj = FSharp.Compatibility.OCaml.Obj
 
 type heap = unit
 
-(* https://www.lexifi.com/blog/references-physical-equality *)
+(* Following OCaml implementation we want reference (physical) equality for ref.  
+   https://www.lexifi.com/blog/references-physical-equality *)
+[<ReferenceEquality>]
 type 'a ref = {
   mutable contents: 'a;
   id: int

ulib/fs/FStar_ST.fs

@@ -1,10 +1,23 @@
 #light "off"
 module FStar_ST
-  type 'a __ref = 'a ref
-  type 'a ref = 'a __ref
-  let read x = !x
-  let op_Colon_Equals x y = x := y
-  let alloc x = ref x
-
-  let recall = (fun r -> ())
-  let write x y = x.contents <- y
+
+open FStar_CommonST
+
+type 'a mref = 'a FStar_Monotonic_Heap.mref
+type 'a ref = 'a FStar_Monotonic_Heap.ref
+
+let read = read
+let op_Bang = op_Bang
+
+let write = write
+let op_Colon_Equals = op_Colon_Equals
+
+let alloc x = alloc
+
+let recall = recall
+let get = get
+
+type 'a witnessed = 'a FStar_CommonST.witnessed
+
+let gst_Witness = gst_witness
+let gst_recall = gst_recall

ulib/ulibfs.fsproj

@@ -52,29 +52,28 @@
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\fsharp.extraction.targets" />
   <ItemGroup>
-    <!-- NOTE: Those realized files do not rely on extracted files from ulib library, so
-               it doesn't matter if we include them before or after the generated files. 
-               Currently, they will be added at the beginning of the list.
-               
-               However, we might need to reconsider this in case we run into a realized file
-               that has a dependency on extracted file. Then we should make sure that realized files
-               are added at the end. -->
+    <!-- TODO: Currently, realised modules will be added at the beginning of the @Compile list.
+               However, some of the realised modules (namely FStar_HyperStack_ST) have a 
+               dependency on extracted modules. 
+
+               We need to change how the @Compile list is ordered by using dependency analysis 
+               available in F*. 
+
+               Note, for now we just ignore some modules and or comment out some code in them. 
+    -->
     <Compile Include="fs\prims.fs" />
     <Compile Include="fs\FStar_All.fs" />
     <!-- <Compile Include="fs\FStar_BaseTypes.fs" /> --> <!-- TODO: Depends on UInt.fsti -->
     <!-- <Compile Include="fs\FStar_Buffer.fs" /> --> <!-- TODO: Depends on UInt.fsti -->
     <!-- <Compile Include="fs\FStar_Bytes.fs" /> --> <!-- TODO: Depends on UInt.fsti -->
     <Compile Include="fs\FStar_Char.fs" />
-    <!-- <Compile Include="fs\FStar_CommonST.fs" /> --> <!-- TODO: Not sure if this is needed -->
     <!-- <Compile Include="fs\FStar_Constructive.fs" /> --> <!-- NOTE: Legacy -->
     <Compile Include="fs\FStar_Dyn.fs" /> 
     <Compile Include="fs\FStar_Float.fs" />
     <Compile Include="fs\FStar_Ghost.fs" />
     <Compile Include="fs\FStar_Monotonic_Heap.fs" />
+    <Compile Include="fs\FStar_CommonST.fs" />
     <Compile Include="fs\FStar_Heap.fs" />
-    <!-- <Compile Include="fs\FStar_HyperStack_All.fs" /> -->
-    <!-- <Compile Include="fs\FStar_HyperStack_ST.fs" /> -->
-    <!-- <Compile Include="fs\FStar_HyperStack_IO.fs" /> -->
     <!-- <Compile Include="fs\FStar_Int16.fs" /> --> <!-- TODO: Depends on UInt.fsti -->
     <!-- <Compile Include="fs\FStar_Int32.fs" /> --> <!-- TODO: Depends on UInt.fsti -->
     <!-- <Compile Include="fs\FStar_Int64.fs" /> --> <!-- TODO: Depends on UInt.fsti -->
@@ -85,10 +84,22 @@
     <Compile Include="fs\FStar_Mul.fs" />
     <Compile Include="fs\FStar_Option.fs" />
     <Compile Include="fs\FStar_Pervasives_Native.fs" />
-    <Compile Include="fs\FStar_Set.fs" />
+    <!-- TODO: Set is implemented with extra 'comparison' constraint on key. 
+               Extracted modules that depend on Set (e.g. Map) don't respect this (i.e. constraint is not emitted). 
+               Moreover, both Set and Map modules restrict key with 'eqtype' which only gives decidable equality, 
+               but we should require ordering. 
+               
+               So there are two points to address:
+               1. Emitting constraints for type parameters when extracting F# code (e.g. for eqtype or 'ordered')
+               2. Add 'type ordered = Type{hasOrder 'a}' or similar and use it instead of 'eqtype' in Set/Map interface.
+    -->
+    <Compile Include="fs\FStar_Set.fs" /> 
     <Compile Include="fs\FStar_ST.fs" />
     <Compile Include="fs\FStar_Exn.fs" />
     <Compile Include="fs\FStar_String.fs" />
+    <Compile Include="fs\FStar_HyperStack_All.fs" />
+    <Compile Include="fs\FStar_HyperStack_ST.fs" />
+    <Compile Include="fs\FStar_HyperStack_IO.fs" />
     <!-- <Compile Include="fs\FStar_UInt16.fs" /> --> <!-- TODO: Depends on UInt.fsti -->
     <!-- <Compile Include="fs\FStar_UInt32.fs" /> --> <!-- TODO: Depends on UInt.fsti -->
     <!-- <Compile Include="fs\FStar_UInt64.fs" /> --> <!-- TODO: Depends on UInt.fsti -->
@@ -121,7 +132,7 @@
     <FStarSourceFile Include="FStar.StrongExcludedMiddle.fst" />
     <FStarSourceFile Include="FStar.PropositionalExtensionality.fst" />
     <!-- <FStarSourceFile Include="FStar.PredicateExtensionality.fst" /> -->
-    <!-- <FStarSourceFile Include="FStar.Map.fst" /> -->
+    <!-- <FStarSourceFile Include="FStar.Map.fst" /> --> <!-- TODO: Doesn't work with current implementation of Set (see TODO note on Set) -->
     <!-- <FStarSourceFile Include="FStar.Monotonic.Witnessed.fst" /> -->
     <FStarSourceFile Include="FStar.List.Tot.Properties.fst" />
     <!-- <FStarSourceFile Include="FStar.Monotonic.HyperHeap.fst" /> -->
@@ -227,7 +238,7 @@
     <!-- <FStarInterfaceFile Include="FStar.Int64.fsti" /> --> <!-- TODO: Depends on UInt.fsti -->
     <!-- <FStarInterfaceFile Include="FStar.Int8.fsti" /> --> <!-- TODO: Depends on UInt.fsti -->
     <!-- <FStarInterfaceFile Include="FStar.MRef.fsti" /> -->
-    <!-- <FStarInterfaceFile Include="FStar.Map.fsti" /> -->
+    <!-- <FStarInterfaceFile Include="FStar.Map.fsti" />  --> <!-- TODO: Doesn't work with current implementation of Set (see TODO note on Set) -->
     <!-- <FStarInterfaceFile Include="FStar.Math.Euclid.fsti" /> -->
     <!-- <FStarInterfaceFile Include="FStar.Math.Fermat.fsti" /> -->
     <!-- <FStarInterfaceFile Include="FStar.Modifies.fsti" /> -->