FStarLang#1087 Few more modules added to ulib for F#

ulib/fs/FStar_HyperStack_ST.fs

@@ -2,10 +2,9 @@ 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_HyperHeap
+(* TODO: There are issues with removing unused parameters in (Monotonic_)Hyper_Stack modules *)
 //open FStar_Monotonic_HyperStack
 
 //open FStar_HyperStack
@@ -25,10 +24,10 @@ let def_rid = root
 //  let r = FStar_CommonST.alloc contents in
 //  MkRef (root, r)
 
-//let sfree r = ()
+let sfree r = ()
 
-//let new_region = (fun r0 -> def_rid)
-//let new_colored_region = (fun r0 c -> def_rid)
+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
@@ -38,26 +37,26 @@ let def_rid = root
 //  let r = FStar_CommonST.alloc contents in
 //  MkRef (i, r)  
 
-//let rfree 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 read = op_Bang
 
-//let write = op_Colon_Equals
+let write = op_Colon_Equals
 
-//let get () = HS (Prims.parse_int "0", FStar_Map.const FStar_Monotonic_Heap.emp, def_rid)
+//let get () = HS (Prims.parse_int "0", FStar_Map.const1 FStar_Monotonic_Heap.emp, def_rid)
 
-//let recall = (fun r -> ())
+let recall = (fun r -> ())
 
-//let recall_region = (fun r -> ())
-//let witness_region _ = ()
-//let witness_hsref _ = ()
-//type erid = rid
+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
@@ -66,20 +65,20 @@ let def_rid = root
 //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 _ _ = ()
+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 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 _ _ = ()
+let witness_p _ _ = ()
+let recall_p _ _ = ()
 
-//type drgn = rid
-//let new_drgn _ = ()
-//let free_drgn _ = ()
+type drgn = rid
+let new_drgn _ = ()
+let free_drgn _ = ()
 //let ralloc_drgn = ralloc
 //let ralloc_drgn_mm = ralloc_mm

ulib/fs/FStar_Map.fs

@@ -0,0 +1,135 @@
+#light "off"
+module FStar_Map
+open Prims
+open FStar_Pervasives
+(* TODO: The extracted version of this file doesn't include the when 'key : comparison constraint which is required for F# *)
+type t<'key, 'value when 'key : comparison> =
+{mappings : ('key, 'value) FStar_FunctionalExtensionality.restricted_t; domain : 'key FStar_Set.set}
+
+
+let __proj__Mkt__item__mappings = (fun ( projectee  :  ('key, 'value) t ) -> (match (projectee) with
+| {mappings = mappings; domain = domain} -> begin
+mappings
+end))
+
+
+let __proj__Mkt__item__domain = (fun ( projectee  :  ('key, 'value) t ) -> (match (projectee) with
+| {mappings = mappings; domain = domain} -> begin
+domain
+end))
+
+
+let sel = (fun ( m  :  ('key, 'value) t ) ( k  :  'key ) -> (m.mappings k))
+
+
+let upd = (fun ( m  :  ('key, 'value) t ) ( k  :  'key ) ( v  :  'value ) -> {mappings = (FStar_FunctionalExtensionality.on_domain (fun ( x  :  'key ) -> (match ((Prims.op_Equality x k)) with
+| true -> begin
+v
+end
+| uu____5020 -> begin
+(m.mappings x)
+end))); domain = (FStar_Set.union m.domain (FStar_Set.singleton k))})
+
+
+let const1 = (fun ( v  :  'value ) -> {mappings = (FStar_FunctionalExtensionality.on_domain (fun ( uu____5049  :  'key ) -> v)); domain = (FStar_Set.complement (FStar_Set.empty ()))})
+
+
+let domain = (fun ( m  :  ('key, 'value) t ) -> m.domain)
+
+
+let contains = (fun ( m  :  ('key, 'value) t ) ( k  :  'key ) -> (FStar_Set.mem k m.domain))
+
+
+let concat = (fun ( m1  :  ('key, 'value) t ) ( m2  :  ('key, 'value) t ) -> {mappings = (FStar_FunctionalExtensionality.on_domain (fun ( x  :  'key ) -> (match ((FStar_Set.mem x m2.domain)) with
+| true -> begin
+(m2.mappings x)
+end
+| uu____5174 -> begin
+(m1.mappings x)
+end))); domain = (FStar_Set.union m1.domain m2.domain)})
+
+(* TODO: Only implicit arguments at the start of a function are erased, whereas the others are extracted to unit and obj 
+         which makes extracted function unusable. See examples/hello/TestFSharp for a minimal example. 
+
+         Here, key should be a generic argument with a comparison constraint instead of obj/unit. 
+
+         A simple workaround would be to change the declaration of map_val in the FStar.Map.fsti so that 
+         '#key:eqtype' parameter is moved before any non-implicit parameters (i.e. before 'f').
+*)
+let map_val = (fun ( f  :  'uuuuuu5195  ->  'uuuuuu5196 ) ( key  :  'key ) ( m  :  ('key, 'uuuuuu5195) t ) -> {mappings = (FStar_FunctionalExtensionality.on_domain (fun ( x  :  'key ) -> (f (m.mappings x)))); domain = m.domain})
+
+
+let restrict = (fun ( s  :  'key FStar_Set.set ) ( m  :  ('key, 'value) t ) -> {mappings = m.mappings; domain = (FStar_Set.intersect s m.domain)})
+
+
+let const_on = (fun ( dom  :  'key FStar_Set.set ) ( v  :  'value ) -> (restrict dom (const1 v)))
+
+
+type disjoint_dom =
+unit
+
+
+type has_dom =
+unit
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+type equal =
+unit
+
+
+
+
+
+
+
+
+
+
+
+
+

ulib/fs/FStar_Set.fs

@@ -1,7 +1,7 @@
 module FStar_Set
 
 type set<'a when 'a : comparison> = Set<'a>
-let empty = Set.empty
+let empty () = Set.empty
 let singleton = Set.singleton
 let union = Set.union
 let intersect = Set.intersect

ulib/ulibfs.fsproj

@@ -50,15 +50,7 @@
   </PropertyGroup>
   <Import Project="$(FSTAR_HOME)\fsharp.extraction.targets" />
   <ItemGroup>
-    <!-- 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. 
-    -->
+    <!-- Note, for now we just ignore some modules and or comment out some code in them. -->
     <Compile Include="fs\prims.fs" Link="prims.fs" />
     <Compile Include="fs\FStar_All.fs" Link="FStar_All.fs" />
     <!-- <Compile Include="fs\FStar_BaseTypes.fs" Link="FStar_BaseTypes.fs" /> --> <!-- TODO: Depends on UInt.fsti -->
@@ -127,12 +119,16 @@
     <Compile Include="FStar.StrongExcludedMiddle.fst" />
     <Compile Include="FStar.PropositionalExtensionality.fst" />
     <!-- <Compile Include="FStar.PredicateExtensionality.fst" /> -->
+    <Compile Include="fs/FStar_Map.fs" Link="FStar_Map.fs" /> <!-- TODO: Map is 'almost' extracted. 
+                                                                         It lacks only the constraint on the key and there's an issue 
+                                                                         with erasure of 'key:eqtype implicit parameter on map_val 
+                                                              -->
     <!-- <Compile Include="FStar.Map.fst" /> --> <!-- TODO: Doesn't work with current implementation of Set (see TODO note on Set) -->
     <!-- <Compile Include="FStar.Monotonic.Witnessed.fst" /> -->
     <Compile Include="FStar.List.Tot.Properties.fst" />
-    <!-- <Compile Include="FStar.Monotonic.HyperHeap.fst" /> -->
-    <!-- <Compile Include="FStar.Monotonic.HyperStack.fst" /> -->
-    <!-- <Compile Include="FStar.HyperStack.fst" /> -->
+    <Compile Include="FStar.Monotonic.HyperHeap.fst" />
+    <!-- <Compile Include="FStar.Monotonic.HyperStack.fst" /> --> <!-- TODO: Problem with erasing of unused type parameters across modules -->
+    <!-- <Compile Include="FStar.HyperStack.fst" /> --> <!-- TODO: Problem with erasing of unused type parameters across modules -->
     <Compile Include="fs\FStar_HyperStack_All.fs" Link="FStar_HyperStack_All.fs" />
     <Compile Include="fs\FStar_HyperStack_ST.fs" Link="FStar_HyperStack_ST.fs" />
     <Compile Include="fs\FStar_HyperStack_IO.fs" Link="FStar_HyperStack_IO.fs" />
@@ -227,7 +223,7 @@
     <Compile Include="FStar.FunctionalExtensionality.fsti" />
     <!-- <Compile Include="FStar.GSet.fsti" /> -->
     <Compile Include="FStar.Ghost.fsti" />
-    <!-- <Compile Include="FStar.HyperStack.ST.fsti" /> -->
+    <Compile Include="FStar.HyperStack.ST.fsti" />
     <!-- <Compile Include="FStar.IFC.fsti" /> -->
     <!-- <Compile Include="FStar.Int.fsti" /> --> <!-- TODO: Depends on UInt.fsti -->
     <!-- <Compile Include="FStar.Int128.fsti" /> --> <!-- TODO: Depends on UInt.fsti -->
@@ -236,15 +232,15 @@
     <!-- <Compile Include="FStar.Int64.fsti" /> --> <!-- TODO: Depends on UInt.fsti -->
     <!-- <Compile Include="FStar.Int8.fsti" /> --> <!-- TODO: Depends on UInt.fsti -->
     <!-- <Compile Include="FStar.MRef.fsti" /> -->
-    <!-- <Compile Include="FStar.Map.fsti" />  --> <!-- TODO: Doesn't work with current implementation of Set (see TODO note on Set) -->
+    <Compile Include="FStar.Map.fsti" />  <!-- TODO: Doesn't work with current implementation of Set (see TODO note on Set) -->
     <!-- <Compile Include="FStar.Math.Euclid.fsti" /> -->
     <!-- <Compile Include="FStar.Math.Fermat.fsti" /> -->
     <!-- <Compile Include="FStar.Modifies.fsti" /> -->
     <!-- <Compile Include="FStar.ModifiesGen.fsti" /> -->
     <!-- <Compile Include="FStar.Monotonic.DependentMap.fsti" /> -->
     <Compile Include="FStar.Monotonic.Heap.fsti" />
-    <!--  <Compile Include="FStar.Monotonic.HyperHeap.fsti" /> -->
-    <!-- <Compile Include="FStar.Monotonic.HyperStack.fsti" /> -->
+     <Compile Include="FStar.Monotonic.HyperHeap.fsti" />
+    <Compile Include="FStar.Monotonic.HyperStack.fsti" />
     <!-- <Compile Include="FStar.Monotonic.Witnessed.fsti" /> -->
     <Compile Include="FStar.Pervasives.fsti" />
     <Compile Include="FStar.Range.fsti" />