val simplify_atomic_field (env: env) (f: atomic_field) : ML atomic_field
let simplify_atomic_field (env:env) (f:atomic_field)
  : ML atomic_field
  = let field = f.v in
    let field = 
      match field.field_type.v with
      | Pointer _ -> failwith "Impossible: field types cannot be pointers"
      | Type_app hd _ args ->
        begin
        match H.try_find env hd.v with
        | None -> //not a singleton record
          field
        | Some (params, inlined_field) ->
          match field.field_array_opt, field.field_bitwidth with
          | FieldArrayQualified _, _
          | FieldString _, _
          | _, Some _ ->  //cannot be inlined
            field
          | _ -> 
            let subst = 
               List.map2 
               (fun (_t, x, _q) e ->
                match e with
                | Inr _ -> failwith "Cannot inline singleton records with output type parameters"
                | Inl e -> (x, e))
               params args
            in
            let subst = (inlined_field.v.field_ident, with_dummy_range (Identifier field.field_ident)) :: subst in
            let inlined_field = subst_atomic_field (mk_subst subst) inlined_field in
            let error msg = 
              let msg = 
                Printf.sprintf "Other types depend on the value of this field, but this field cannot be read because %s"
                               msg
              in
              error msg f.range
            in
            match field, inlined_field.v with
            | { field_action = Some _ }, { field_action = Some _ } ->
              error "it has multiple actions"
  
            | { field_constraint = Some _ }, { field_action = Some _ } ->
              error "reading it would alter the order of evaluation of refinement and action"
  
            | { field_array_opt = FieldArrayQualified _ }, _
            | _, { field_array_opt = FieldArrayQualified _ } ->
              error "it contains an array"
  
            | { field_array_opt = FieldString _ }, _
            | _, { field_array_opt = FieldString _ } ->
              error "it contains a string"

            | { field_bitwidth = Some _ }, _        
            | _, { field_bitwidth = Some _ } ->
              error "it contains a bit field"
          
            | _, _ ->
              let join_constraints c1 c2 =
                match c1, c2 with
                | None, None -> None
                | Some c, None 
                | None, Some c -> Some c
                | Some c1, Some c2 -> Some (with_dummy_range (App And [c1;c2]))
              in
              { field with 
                field_type = inlined_field.v.field_type;
                field_constraint = join_constraints field.field_constraint inlined_field.v.field_constraint;
                field_action = choose_one field.field_action inlined_field.v.field_action }
          end
    in
    { f with v = field }
val simplify_atomic_field (env: env) (f: atomic_field) : ML atomic_field
let simplify_atomic_field (env: env) (f: atomic_field) : ML atomic_field =
let field = f.v in
let field =
  match field.field_type.v with
  | Pointer _ -> failwith "Impossible: field types cannot be pointers"
  | Type_app hd _ args ->
    match H.try_find env hd.v with
    | None -> field
    | Some (params, inlined_field) ->
      match field.field_array_opt, field.field_bitwidth with
      | FieldArrayQualified _, _ | FieldString _, _ | _, Some _ -> field
      | _ ->
        let subst =
          List.map2 (fun (_t, x, _q) e ->
                match e with
                | Inr _ -> failwith "Cannot inline singleton records with output type parameters"
                | Inl e -> (x, e))
            params
            args
        in
        let subst =
          (inlined_field.v.field_ident, with_dummy_range (Identifier field.field_ident)) :: subst
        in
        let inlined_field = subst_atomic_field (mk_subst subst) inlined_field in
        let error msg =
          let msg =
            Printf.sprintf "Other types depend on the value of this field, but this field cannot be read because %s"
              msg
          in
          error msg f.range
        in
        match field, inlined_field.v with
        | { field_action = Some _ }, { field_action = Some _ } -> error "it has multiple actions"
        | { field_constraint = Some _ }, { field_action = Some _ } ->
          error "reading it would alter the order of evaluation of refinement and action"
        | { field_array_opt = FieldArrayQualified _ }, _
        | _, { field_array_opt = FieldArrayQualified _ } -> error "it contains an array"
        | { field_array_opt = FieldString _ }, _
        | _, { field_array_opt = FieldString _ } -> error "it contains a string"
        | { field_bitwidth = Some _ }, _
        | _, { field_bitwidth = Some _ } -> error "it contains a bit field"
        | _, _ ->
          let join_constraints c1 c2 =
            match c1, c2 with
            | None, None -> None
            | Some c, None | None, Some c -> Some c
            | Some c1, Some c2 -> Some (with_dummy_range (App And [c1; c2]))
          in
          {
            field with
            field_type = inlined_field.v.field_type;
            field_constraint
            =
            join_constraints field.field_constraint inlined_field.v.field_constraint;
            field_action = choose_one field.field_action inlined_field.v.field_action
          }
in
{ f with v = field }
InlineSingletonRecords.fst.checked
prims.fst.checked Options.fsti.checked Hashtable.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked FStar.All.fst.checked Ast.fst.checked
InlineSingletonRecords.fst
InlineSingletonRecords.env Ast.atomic_field Ast.Mkwith_meta_t Ast.atomic_field' Ast.__proj__Mkwith_meta_t__item__range Ast.__proj__Mkwith_meta_t__item__comments Ast.__proj__Mkwith_meta_t__item__v Ast.typ' Ast.__proj__Mkatomic_field'__item__field_type Ast.with_meta_t FStar.All.failwith Ast.ident Ast.t_kind Prims.list Ast.either Ast.expr Ast.out_expr Ast.param FStar.Pervasives.Native.Mktuple2 Ast.field_array_t FStar.Pervasives.Native.option Ast.field_bitwidth_t Ast.__proj__Mkatomic_field'__item__field_array_opt Ast.__proj__Mkatomic_field'__item__field_bitwidth FStar.Pervasives.Native.tuple2 Ast.array_qualifier Prims.bool Ast.typ Ast.action Ast.Mkatomic_field' Ast.__proj__Mkatomic_field'__item__field_dependence Ast.__proj__Mkatomic_field'__item__field_ident Ast.__proj__Mkatomic_field'__item__field_constraint InlineSingletonRecords.choose_one Ast.__proj__Mkatomic_field'__item__field_action Ast.expr' FStar.Pervasives.Native.None FStar.Pervasives.Native.Some Ast.with_dummy_range Ast.App Ast.And Prims.Cons Prims.Nil Prims.string Ast.error FStar.Printf.sprintf Ast.subst_atomic_field Ast.subst Ast.mk_subst Ast.Identifier FStar.List.map2 FStar.Pervasives.Native.tuple3 Ast.qualifier InlineSingletonRecords.singleton_record Hashtable.try_find Ast.ident'
(*
   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 InlineSingletonRecords
open Ast
open FStar.All
module H = Hashtable
type singleton_record = list param & atomic_field
let env = H.t ident' singleton_record

(*
  This module implements a pass over the source AST
  
    1. Inlining records that contain only a single field
    2. Inlining enumerated types that have dependences

  Both of these are necessary to avoid double fetches
*)
    
  
let choose_one (a b:option 'a) : ML (option 'a) = 
  match a, b with
  | Some fc, _
  | _, Some fc -> Some fc
  | _ -> None
                 
let simplify_atomic_field (env:env) (f:atomic_field)
val simplify_atomic_field (env: env) (f: atomic_field) : ML atomic_field
env: InlineSingletonRecords.env -> f: Ast.atomic_field -> FStar.All.ML Ast.atomic_field