Extraction for Steel.C.Array

examples/steel/arraystructs/Steel.C.Array.fst

@@ -28,6 +28,10 @@ let array_elements_pcm
 
 let array_pcm t n = S.prod_pcm (array_elements_pcm t n)
 
+let array_view_type_sized t n' n = array_view_type t n
+
+let unfold_array_view_type_sized t n' n = ()
+
 [@"opaque_to_smt"]
 let rec raise_list_array_domain
   (t: Type u#0)

examples/steel/arraystructs/Steel.C.Array.fsti

@@ -22,6 +22,10 @@ open Steel.Effect
 open FStar.Ghost
 open Steel.Effect.Atomic
 
+open Steel.C.Typedef
+open Steel.C.PCM
+open Typenat
+
 #set-options "--ide_id_info_off"
 
 /// A library for arrays in Steel
@@ -32,9 +36,20 @@ val array_pcm_carrier (t: Type u#0) (n: Ghost.erased size_t) : Type u#0
 val array_pcm (t: Type u#0) (n: Ghost.erased size_t) : Tot (Steel.C.PCM.pcm (array_pcm_carrier t n))
 
 // FIXME: how to produce array type t[n] as the type of some struct field?
-let array_view_type (t: Type u#0) (n: size_t) : Type u#0 =
+let array_view_type (t: Type u#0) (n: size_t)
+: Type u#0 =
   Seq.lseq t (size_v n)
 
+/// A variant of array_view_type, which records the length of the
+/// array in Type as a Typenat, for extraction
+let size_t_of (n': Type u#0) = n:size_t{n' == nat_t_of_nat (size_v n)}
+val array_view_type_sized (t: Type u#0) (n': Type u#0) (n: size_t_of n')
+: Type u#0
+val unfold_array_view_type_sized
+ (t: Type u#0) (n': Type u#0) (n: size_t_of n')
+: Lemma (array_view_type_sized t n' n == array_view_type t n)
+  [SMTPat (array_view_type_sized t n' n)]
+
 val array_view (t: Type u#0) (n: size_t)
   : Pure (Steel.C.Ref.sel_view (array_pcm t n) (array_view_type t n) false)
     (requires (size_v n > 0))
@@ -49,6 +64,18 @@ val array (base: Type u#0) (t:Type u#0) : Type u#0
 val len (#base: Type) (#t: Type) (a: array base t) : GTot size_t
 let length (#base: Type) (#t: Type) (a: array base t) : GTot nat = size_v (len a)
 
+// TODO 
+val array_is_unit (t: Type0) (n: size_t) (a: array_pcm_carrier t n)
+: b:bool{b <==> a == one (array_pcm t n)}
+
+let array_typedef_sized (t: Type0) (n': Type0) (n: size_t_of n'{size_v n > 0}): typedef = {
+  carrier = array_pcm_carrier t n;
+  pcm = array_pcm t n;
+  view_type = array_view_type_sized t n' n;
+  view = array_view t n;
+  is_unit = array_is_unit t n;
+}
+
 /// Combining the elements above to create an array vprop
 /// TODO: generalize to any view
 

src/extraction/FStar.Extraction.Kremlin.fs

@@ -190,6 +190,7 @@ and typ =
   | TApp of lident * list<typ>
   | TTuple of list<typ>
   | TConstBuf of typ
+  | TArray of typ * constant
 
 (** Versioned binary writing/reading of ASTs *)
 
@@ -598,6 +599,17 @@ and translate_type_decl env ty: option<decl> =
 
       | Some fields ->
           print_endline "Got fields:";
+          // Unlike in arguments, fixed-size arrays in structs do not decay to pointers
+          let rec translate_field_type env ty =
+            match ty with
+            | MLTY_Named ([t; n; _], p)
+              when Syntax.string_of_mlpath p = "Steel.C.Array.array_view_type_sized"
+              // TODO add support for fixed-size arrays to Steel.C.Array.fsti
+              ->
+                let int_of_typenat s = failwith "unimplemented" in // TODO
+                TArray (translate_field_type env t, (UInt32, int_of_typenat n))
+            | t -> translate_type env t
+          in
           List.fold_left
             (fun () (field, ty) ->
                BU.print2 "  %s : %s\n"
@@ -610,7 +622,7 @@ and translate_type_decl env ty: option<decl> =
               (fun (field, ty) ->
                  BU.print1 "Translating %s.\n"
                    (FStar.Extraction.ML.Code.string_of_mlty ([], "") ty);
-                 (field, translate_type env ty))
+                 (field, translate_field_type env ty))
               fields)
     in
     match ty with
@@ -730,6 +742,19 @@ and translate_type env t: typ =
 
   | MLTY_Named ([_; arg; _; _], p) when
     Syntax.string_of_mlpath p = "Steel.C.Reference.ref"
+    ->
+      let rec skip_array_view_types ty =
+        match ty with
+        | MLTY_Named ([ty; _; _], p) when
+          Syntax.string_of_mlpath p = "Steel.C.Array.array_view_type_sized"
+          ->
+            skip_array_view_types ty
+        | _ -> ty
+      in
+      TBuf (translate_type env (skip_array_view_types arg))
+
+  | MLTY_Named ([_; arg], p) when
+    Syntax.string_of_mlpath p = "Steel.C.Array.array"
     ->
       TBuf (translate_type env arg)
 
@@ -1212,6 +1237,26 @@ and translate_expr env e: expr =
         EBufRead (translate_expr env r, EConstant (UInt32, "0")),
         translate_expr env x)
 
+  | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, [_; _])}, [r])
+    when string_of_mlpath p = "Steel.C.Array.ref_of_array" ->
+      translate_expr env r
+
+  | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, [_; _])}, [r])
+    when string_of_mlpath p = "Steel.C.Array.mk_array_of_ref" ->
+      translate_expr env r
+
+  | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, [_; _])}, [_; r])
+    when string_of_mlpath p = "Steel.C.Array.intro_varray" ->
+      translate_expr env r
+
+  | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, [_; _])}, [r; i])
+    when string_of_mlpath p = "Steel.C.Array.index" ->
+      EBufRead (translate_expr env r, translate_expr env i)
+
+  | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, [_; _])}, [r; i; x])
+    when string_of_mlpath p = "Steel.C.Array.upd" ->
+      EBufWrite (translate_expr env r, translate_expr env i, translate_expr env x)
+
   | MLE_App (head, args) ->
       EApp (translate_expr env head, List.map (translate_expr env) args)