val simplify_expr (env: T.env_t) (e: expr) : ML expr
let rec simplify_expr (env:T.env_t) (e:expr)
  : ML expr
  = match e.v with
    | This -> failwith "Impossible: should have been eliminated already"
    | App SizeOf _ ->
      begin
      match T.value_of_const_expr env e with
      | Some (Inr (t, n)) -> with_range (Constant (Int t n)) e.range
      | _ -> error (Printf.sprintf "Could not evaluate %s to a compile-time constant" (print_expr e)) e.range
      end
    | App op es ->
      let es = List.map (simplify_expr env) es in
      { e with v = App op es }

    | _ -> e
val simplify_expr (env: T.env_t) (e: expr) : ML expr
let rec simplify_expr (env: T.env_t) (e: expr) : ML expr =
match e.v with
| This -> failwith "Impossible: should have been eliminated already"
| App SizeOf _ ->
  (match T.value_of_const_expr env e with
    | Some (Inr (t, n)) -> with_range (Constant (Int t n)) e.range
    | _ ->
      error (Printf.sprintf "Could not evaluate %s to a compile-time constant" (print_expr e))
        e.range)
| App op es ->
  let es = List.map (simplify_expr env) es in
  { e with v = App op es }
| _ -> e
Simplify.fst.checked
TypeSizes.fsti.checked prims.fst.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked FStar.All.fst.checked Binding.fsti.checked Ast.fst.checked
Simplify.fst
TypeSizes.env_t Ast.expr Ast.__proj__Mkwith_meta_t__item__v Ast.expr' FStar.All.failwith Prims.list Ast.with_meta_t Ast.integer_type Prims.int Ast.with_range Ast.Constant Ast.Int Ast.__proj__Mkwith_meta_t__item__range FStar.Pervasives.Native.option Ast.either Prims.bool FStar.Pervasives.Native.tuple2 Ast.error FStar.Printf.sprintf Ast.print_expr TypeSizes.value_of_const_expr Ast.op Ast.Mkwith_meta_t Ast.App Ast.__proj__Mkwith_meta_t__item__comments FStar.List.map Simplify.simplify_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 Simplify
open Ast
open FStar.All
module B = Binding
module T = TypeSizes

(*
  This module implements a pass over the source AST
  
    1. Simplifying refinement expressions, in particular reducing
       sizeof expressions to constants

    2. Reducing typedef abbreviations
*)

let rec simplify_expr (env:T.env_t) (e:expr)
val simplify_expr (env: T.env_t) (e: expr) : ML expr
env: TypeSizes.env_t -> e: Ast.expr -> FStar.All.ML Ast.expr