Fix(hopefully) extraction for arrays, implementing the proper rules f…

…or pointer decay

examples/steel/arraystructs/ScalarUnion.fst

@@ -3,6 +3,7 @@ module ScalarUnion
 open Steel.C.PCM
 open Steel.C.Opt
 open Steel.C.Connection
+open Steel.C.StructLiteral
 open Steel.C.UnionLiteral
 open Steel.C.Typedef
 open FStar.FunctionalExtensionality
@@ -14,6 +15,7 @@ open Steel.C.Reference
 
 open FStar.FSet
 open Typestring
+open Typenat
 
 module U32 = FStar.UInt32
 module U16 = FStar.UInt16
@@ -65,7 +67,27 @@ let u32_or_u16_pcm = union_pcm u32_or_u16_tag u32_or_u16_fields
 noextract inline_for_extraction
 let c_u32_or_u16: typedef = typedef_union u32_or_u16_tag u32_or_u16_fields
 
-let _ = normalize (mk_c_union u32_or_u16_tag u32_or_u16_fields)
+noextract
+unfold let norm_list =
+  [delta_only
+    [`%mk_c_union;
+     `%mk_c_struct;
+     `%c_fields_t;
+     `%List.Tot.fold_right;
+     `%Typestring.mk_string_t;
+     `%Typestring.string_t_of_chars;
+     `%Typestring.char_t_of_char;
+     `%Mkc_fields?.get_field;
+     `%Mkc_fields?.cfields;
+     `%Mktypedef?.view_type;
+     `%fields_cons;
+     `%fields_nil;
+     `%Typenat.nat_t_of_nat;
+     ];
+   delta_attr [`%c_struct; `%c_typedef];
+   iota; zeta; primops]
+
+let _ = norm norm_list (mk_c_union u32_or_u16_tag u32_or_u16_fields)
 
 #push-options "--fuel 0"
 
@@ -100,7 +122,7 @@ let zero_u32_ref (p:ref 'a U32.t (opt_pcm #U32.t))
   (fun _ -> p `pts_to_view` opt_view _)
   (requires fun _ -> True)
   (ensures fun _ _ _ -> True)
-= opt_write_sel p U32.zero
+= opt_write_sel p 0ul
 
 val zero_u32_of_union (p: ref unit u32_or_u16 u32_or_u16_pcm)
 : Steel unit

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

@@ -28,10 +28,6 @@ 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

@@ -24,6 +24,7 @@ open Steel.Effect.Atomic
 
 open Steel.C.Typedef
 open Steel.C.PCM
+open Steel.C.Fields
 open Typenat
 
 #set-options "--ide_id_info_off"
@@ -43,12 +44,9 @@ let array_view_type (t: Type u#0) (n: size_t)
 /// 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')
+let 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)]
+= array_view_type t 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)
@@ -68,6 +66,7 @@ let length (#base: Type) (#t: Type) (a: array base t) : GTot nat = size_v (len a
 val array_is_unit (t: Type0) (n: size_t) (a: array_pcm_carrier t n)
 : b:bool{b <==> a == one (array_pcm t n)}
 
+[@@c_struct]
 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;

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

@@ -8,6 +8,11 @@ open Steel.C.Opt
 
 module TS = Typestring
 
+irreducible let c_struct = ()
+irreducible let c_union = ()
+irreducible let c_typedef = ()
+
+[@@c_typedef]
 let trivial_typedef: typedef = {
   carrier = option unit;
   pcm = opt_pcm #unit;
@@ -78,10 +83,6 @@ let fields_cons (field: field_t) (td: typedef) (fields: c_fields): c_fields = {
 
 let field_of (fields: c_fields) = field:string{fields.has_field field == true /\ field =!= ""}
 
-irreducible let c_struct = ()
-irreducible let c_union = ()
-irreducible let c_typedef = ()
-
 unfold let unfold_typedefs = [delta_attr [`%c_typedef]]
 
 unfold let simplify_typedefs =

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

@@ -179,6 +179,7 @@ let switch_union_field
   (#tag: Type0) (#fields: c_fields)
   (field: field_of fields) (new_value: (fields.get_field field).view_type)
   (p: ref 'a (union tag fields) (union_pcm tag fields))
+  // TODO match order of c to get p->field = new_value
 : Steel unit
     (p `pts_to_view` union_view tag fields)
     (fun _ -> p `pts_to_view` union_view tag fields)