#1087 Allow interleaving of F# and F* sources in a project

[mateuszbujalski]

Preserve the order of files for extraction and F# compilation

[mateuszbujalski]

Note how HyperStack related files come after some F* modules. For F# compilation they come after the extracted modules defined above them. It's actually needed as they depend on FStar.Monotonic.HyperHeap.fst and FStar.Monotonic.HyperStack.fst defined above them (though not enabled yet partially enabled now but there are still issues with extracting of unused parameters).

[mateuszbujalski]

(* FStar.Map.fsti *)
val map_val: #val1:Type -> #val2:Type -> f:(val1 -> val2) -> #key:eqtype -> t key val1 -> Tot (t key val2)

@nikswamy Were you already looking at this particular problem? If not, I suppose it's a good candidate for me to look into next. It seems that all other modules are blocked by the issues around removing of unused parameters across modules which you're looking into (is there anything I can help with there?).

[nikswamy]

Thanks @mateuszbujalski! This looks really great ... very cool that you an add a Compile target with .fst files in an .fsproj. I'm merging this into my working branch on this topic. Not sure I fully understand the issue on FStar.Map issue ... will look into it and reply.

[nikswamy]

Regarding the extraction of non-prefix quantified type variables, as in FStar.Map.map_val:

Yes, you're right. When F* extracts code to OCaml or F#, only prenex quantified type variables are extracted as type variables. The rest (since F# and OCaml do not directly support first-class polymorphism) are erased to unit and trigger the use of Prims.unsafe_coerce of Obj.magic.

For instance, we extract FStar.Map.map_val to

let map_val = (fun ( f  :  'uuuuuu16115  ->  'uuuuuu16116 ) ( key  :  unit ) ( m  :  (obj, 'uuuuuu16115) t ) -> {mappings = (FStar_FunctionalExtensionality.on_domain (fun ( x  :  obj ) -> (f (m.mappings x)))); domain = m.domain})

and a test client

let test (f:int -> nat) (m:t int int) : t int nat = map_val f m

is extracted to

let test : (Prims.int  ->  Prims.nat)  ->  (Prims.int, Prims.int) FStar_Map.t  ->  (Prims.int, Prims.nat) FStar_Map.t = 
  (fun ( uu____245  :  Prims.int  ->  Prims.nat ) 
     ( uu____244  :  (Prims.int, Prims.int) FStar_Map.t ) -> 
     ((fun ( f  :  (Prims.int  ->  Prims.nat) ) ( m  :  (Prims.int, Prims.int) FStar_Map.t ) -> (Prims.unsafe_coerce (FStar_Map.map_val f () (Prims.unsafe_coerce m))))      
       uu____245 uu____244))

Note the addition of the unsafe coerce and the erasure to the type argument to map_val to ().

In OCaml, we get something quite similar

open Prims
let (test :
  (Prims.int -> Prims.nat) ->
    (Prims.int, Prims.int) FStar_Map.t -> (Prims.int, Prims.nat) FStar_Map.t)
  =
  fun uu____245 ->
    fun uu____244 ->
      (fun f -> fun m -> Obj.magic (FStar_Map.map_val f () (Obj.magic m)))
        uu____245 uu____244

At least in OCaml, the use of Obj.magic is safe and justified by the typability of the program in F*, and will not trigger a runtime typechecking failure.

I'm less sure about the semantics of Prims.unsafe_coerce x = unbox (box x) in F#. In this case, it is used to coerce a Map.t<int, int> to a Map.t<obj,unit> and back. This would trigger a runtime failure, I presume? Can you confirm? In points to a difficulty in the F# translation where, unlike OCaml, we do not have a generic way to coerce between types. We discussed this briefly a while back on Zulip. https://fstar.zulipchat.com/#narrow/stream/183594-new-members/topic/Extraction.20to.20F.23/near/192852495

A fix to this particular case for F# could indeed be to move the key:eqtype parameter to the front. But, maybe we should be more defensive in F# extraction and refuse to extract programs that need to use Prims.unsafe_coerce, since these may trigger F# runtime failures?