let subst' = list (ident & expr)
let subst' =
list (ident & expr)
BitFields.fst.checked
prims.fst.checked Options.fsti.checked Hashtable.fsti.checked FStar.String.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.All.fst.checked Binding.fsti.checked Ast.fst.checked
BitFields.fst
Prims.list FStar.Pervasives.Native.tuple2 Ast.ident Ast.expr
(*
   Copyright 2019 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module BitFields
open FStar.List.Tot
open FStar.Mul
open Ast
open FStar.All
module B = Binding
module H = Hashtable

(* This module implements a pass over the source AST

   coalescing adjacent bit fields and replacing expressions on
   bitfields using offsets into larger fgields

*)

let bitfield_group = int & typ & list atomic_field
let grouped_fields = either field bitfield_group

let group_bit_fields (rewrite_composite_field: field -> ML field)
                     (fields: list field)
  : ML (list grouped_fields)
  = List.fold_right
      (fun field out ->
        match field.v with
        | RecordField _ _
        | SwitchCaseField _ _ ->
          Inl (rewrite_composite_field field) :: out

        | AtomicField af ->
          match af.v.field_bitwidth with
          | None ->
            Inl field :: out

          | Some (Inl _) ->
            failwith "Bit fields should have been elaborated already"

          | Some (Inr bf) ->
            match out with
            | Inr (index, typ, atomic_fields)::tl ->
              if index = bf.v.bitfield_identifier
              then Inr(index, typ, af :: atomic_fields) :: tl //extend this bitfield group
              else Inr(bf.v.bitfield_identifier, bf.v.bitfield_type, [af]) :: out //new bitfield group

            | _ -> Inr (bf.v.bitfield_identifier, bf.v.bitfield_type, [af]) :: out //new bitfield group
        )
       fields
       []
val subst' : Type0
Type0