val value_of_const_expr (env:env_t) (e:expr)
  : ML (option (either bool (integer_type & int)))
let rec value_of_const_expr (env:env_t) (e:expr)
  : ML (option (either bool (integer_type & int)))
  =
  match e.v with
  | Constant (Int t n) -> Some (Inr (t, n))
  | Constant (Bool b) -> Some (Inl b)
  | App op [e1; e2] ->
    let v1 = value_of_const_expr env e1 in
    let v2 = value_of_const_expr env e2 in
    begin
    match op, v1, v2 with
    | Plus _,  Some (Inr (t1, n1)), Some (Inr (t2, n2)) -> Some (Inr (integer_type_lub t1 t2, n1 + n2))
    | Minus _, Some (Inr (t1, n1)), Some (Inr (t2, n2)) -> Some (Inr (integer_type_lub t1 t2, n1 - n2))
    | Mul _,   Some (Inr (t1, n1)), Some (Inr (t2, n2)) -> Some (Inr (integer_type_lub t1 t2, n1 * n2))
    | Division _, Some (Inr (t1, n1)), Some (Inr (t2, n2)) ->
      if n2 = 0
      then error ("Division by zero in constant expression") e2.range
      else Some (Inr (integer_type_lub t1 t2, n1 / n2))
    | GT _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 > n2))
    | LT _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 < n2))
    | GE _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 >= n2))
    | LE _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 <= n2))
    | And, Some (Inl b1), Some (Inl b2) -> Some (Inl (b1 && b2))
    | Or, Some (Inl b1), Some (Inl b2) -> Some (Inl (b1 || b2))
    | _ -> None
    end
  | App Not [e] ->
    let v = value_of_const_expr env e in
    begin
    match v with
    | Some (Inl b) -> Some (Inl (not b))
    | _ -> None
    end
  | App SizeOf [{v=Identifier t}] ->
    begin
    try
      match size_of_typ env (with_range (Type_app t KindSpec []) t.range) with
      | Fixed n
      | WithVariableSuffix n -> Some (Inr (UInt32, n))
      | _ -> None
    with
      | _ -> None
    end
  | App (Cast _ t) [e] ->
    let v = value_of_const_expr env e in
    begin
    match v with
    | Some (Inr (_, n)) ->
      Some (Inr (t, n))
    | _ -> None
    end
  | Identifier i ->
    begin
    match B.lookup_macro_definition (fst env) i with
    | Some e ->
      value_of_const_expr env e
    | _ -> None
    end
  | _ -> None
val value_of_const_expr (env:env_t) (e:expr)
  : ML (option (either bool (integer_type & int)))
let rec value_of_const_expr (env: env_t) (e: expr) : ML (option (either bool (integer_type & int))) =
match e.v with
| Constant (Int t n) -> Some (Inr (t, n))
| Constant (Bool b) -> Some (Inl b)
| App op [e1 ; e2] ->
  let v1 = value_of_const_expr env e1 in
  let v2 = value_of_const_expr env e2 in
  (match op, v1, v2 with
    | Plus _, Some (Inr (t1, n1)), Some (Inr (t2, n2)) ->
      Some (Inr (integer_type_lub t1 t2, n1 + n2))
    | Minus _, Some (Inr (t1, n1)), Some (Inr (t2, n2)) ->
      Some (Inr (integer_type_lub t1 t2, n1 - n2))
    | Mul _, Some (Inr (t1, n1)), Some (Inr (t2, n2)) ->
      Some (Inr (integer_type_lub t1 t2, n1 * n2))
    | Division _, Some (Inr (t1, n1)), Some (Inr (t2, n2)) ->
      if n2 = 0
      then error ("Division by zero in constant expression") e2.range
      else Some (Inr (integer_type_lub t1 t2, n1 / n2))
    | GT _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 > n2))
    | LT _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 < n2))
    | GE _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 >= n2))
    | LE _, Some (Inr (_, n1)), Some (Inr (_, n2)) -> Some (Inl (n1 <= n2))
    | And, Some (Inl b1), Some (Inl b2) -> Some (Inl (b1 && b2))
    | Or, Some (Inl b1), Some (Inl b2) -> Some (Inl (b1 || b2))
    | _ -> None)
| App Not [e] ->
  let v = value_of_const_expr env e in
  (match v with
    | Some (Inl b) -> Some (Inl (not b))
    | _ -> None)
| App SizeOf [{ v = Identifier t }] ->
  (try
      match size_of_typ env (with_range (Type_app t KindSpec []) t.range) with
      | Fixed n | WithVariableSuffix n -> Some (Inr (UInt32, n))
      | _ -> None
    with
    | _ -> None)
| App (Cast _ t) [e] ->
  let v = value_of_const_expr env e in
  (match v with
    | Some (Inr (_, n)) -> Some (Inr (t, n))
    | _ -> None)
| Identifier i ->
  (match B.lookup_macro_definition (fst env) i with
    | Some e -> value_of_const_expr env e
    | _ -> None)
| _ -> None
TypeSizes.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.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.IO.fst.checked FStar.All.fst.checked Binding.fsti.checked Ast.fst.checked
TypeSizes.fst
TypeSizes.env_t Ast.expr Ast.__proj__Mkwith_meta_t__item__v Ast.expr' Ast.integer_type Prims.int FStar.Pervasives.Native.Some Ast.either Prims.bool FStar.Pervasives.Native.tuple2 Ast.Inr FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option Ast.Inl Ast.op Ast.with_meta_t FStar.Pervasives.Native.Mktuple3 Ast.integer_type_lub Prims.op_Addition Prims.op_Subtraction FStar.Mul.op_Star Prims.op_Equality Ast.error Ast.__proj__Mkwith_meta_t__item__range Prims.op_Division Prims.op_GreaterThan Prims.op_LessThan Prims.op_GreaterThanOrEqual Prims.op_LessThanOrEqual Prims.op_AmpAmp Prims.op_BarBar FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.None TypeSizes.value_of_const_expr Prims.op_Negation Ast.ident Ast.range Ast.comments FStar.All.try_with Prims.unit Ast.UInt32 TypeSizes.size TypeSizes.size_of_typ Ast.with_range Ast.typ' Ast.Type_app Ast.KindSpec Prims.Nil Ast.out_expr Ast.ident' Prims.exn Binding.lookup_macro_definition FStar.Pervasives.Native.fst Binding.env TypeSizes.size_env
(*
   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 as 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 TypeSizes
open FStar.All
open Ast
open FStar.Mul
module H = Hashtable
module B = Binding

let product_size (base:size) (n:int) =
  match base with
  | Variable
  | WithVariableSuffix _ ->
    Variable
  | Fixed k ->
    Fixed (k * n)

let typename = ident'

let alignment = option (x:int{x == 1 \/ x == 2 \/ x == 4 \/ x == 8})

type size_env = H.t typename (size & alignment)

//TODO: size of pointer is platform-dependent
let pointer_alignment : alignment = Some 8

let initial_senv () =
  let i = [
       ("unit",     (Fixed 0,  None));
       ("Bool",     (Fixed 1,  Some 1));
       ("UINT8",    (Fixed 1,  Some 1));
       ("UINT16",   (Fixed 2,  Some 2));
       ("UINT32",   (Fixed 4,  Some 4));
       ("UINT64",   (Fixed 8,  Some 8));
       ("UINT8BE",   (Fixed 1,  Some 1));
       ("UINT16BE",   (Fixed 2,  Some 2));
       ("UINT32BE",   (Fixed 4,  Some 4));
       ("UINT64BE",   (Fixed 8,  Some 8));
       ("field_id", (Fixed 4,  Some 4));
       ("all_bytes", (Variable, None));
       ("all_zeros", (Variable, None));
       ("PUINT8",   (Variable, pointer_alignment))
  ]
  in
  let senv = H.create 17 in
  List.iter (fun (i, k) -> H.insert senv (to_ident' i) k) i;
  senv

let size_and_alignment_of_typename (env:env_t) (i:ident)
  : ML (size & alignment)
  = match H.try_find (snd env) i.v with
    | Some s -> s
    | None ->
      failwith (Printf.sprintf "size_of_typename: Identifier %s not found" (ident_to_string i))

let size_of_typename (env:env_t) (i:ident)
  : ML size
  = fst (size_and_alignment_of_typename env i)

let print_size =
  function
  | Fixed n -> Printf.sprintf "(Fixed %d)" n
  | WithVariableSuffix n -> Printf.sprintf "(WithVariableSuffix %d)" n
  | Variable -> "Variable"

let extend_with_size_of_ident (env:env_t) (i:ident) (n:size) (a:alignment)
  : ML unit
  = Options.debug_print_string
     (Printf.sprintf "***** Size of %s = %s\n"
                     (ident_to_string i) (print_size n));
    H.insert (snd env) i.v (n, a)

let extend_with_size_of_typedef_names (env:env_t) (names:typedef_names) (size:size) (a:alignment)
  : ML unit
  = extend_with_size_of_ident env names.typedef_name size a;
    extend_with_size_of_ident env names.typedef_abbrev size a;
    extend_with_size_of_ident env names.typedef_ptr_abbrev Variable a

let size_and_alignment_of_typ (env:env_t) (t:typ)
  : ML (size & alignment)
  = match t.v with
    | Type_app i _ _ -> size_and_alignment_of_typename env i
    | Pointer _ -> Variable, Some 8

let size_of_typ (env:env_t) (t:typ)
  : ML size
  = fst (size_and_alignment_of_typ env t)

let rec value_of_const_expr (env:env_t) (e:expr)
  : ML (option (either bool (integer_type & int)))
val value_of_const_expr (env:env_t) (e:expr)
  : ML (option (either bool (integer_type & int)))
env: TypeSizes.env_t -> e: Ast.expr
  -> FStar.All.ML
    (FStar.Pervasives.Native.option (Ast.either Prims.bool (Ast.integer_type * Prims.int)))