val simplify_out_expr_node (env: T.env_t) (oe: with_meta_t out_expr') : ML (with_meta_t out_expr')
let rec simplify_typ_param (env:T.env_t) (p:typ_param) : ML typ_param =
  match p with
  | Inl e -> simplify_expr env e |> Inl
  | Inr oe -> simplify_out_expr env oe |> Inr

and simplify_typ (env:T.env_t) (t:typ)
  : ML typ
  = match t.v with
    | Pointer t -> {t with v=Pointer (simplify_typ env t)}
    | Type_app s b ps ->
      let ps = List.map (simplify_typ_param env) ps in
      let s = B.resolve_record_case_output_extern_type_name (fst env) s in
      let t = { t with v = Type_app s b ps } in
      B.unfold_typ_abbrev_only (fst env) t

and simplify_out_expr_node (env:T.env_t) (oe:with_meta_t out_expr')
  : ML (with_meta_t out_expr')
  = oe

and simplify_out_expr_meta (env:T.env_t) (mopt:option out_expr_meta_t)
  : ML (option out_expr_meta_t)
  = match mopt with
    | None -> None
    | Some ({ out_expr_base_t = bt;
              out_expr_t = t;
              out_expr_bit_width = n }) ->
      Some ({ out_expr_base_t = simplify_typ env bt;
              out_expr_t = simplify_typ env t;
              out_expr_bit_width = n })

and simplify_out_expr (env:T.env_t) (oe:out_expr) : ML out_expr =
  {oe with
   out_expr_node = simplify_out_expr_node env oe.out_expr_node;
   out_expr_meta = simplify_out_expr_meta env oe.out_expr_meta}
val simplify_out_expr_node (env: T.env_t) (oe: with_meta_t out_expr') : ML (with_meta_t out_expr')
let rec simplify_out_expr_node (env: T.env_t) (oe: with_meta_t out_expr')
    : ML (with_meta_t out_expr') =
oe
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.with_meta_t Ast.out_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)
  : 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

(*
 * Simplify output expressions, mainly their metadata to resolve
 *   abbrevs in the types that appear in the metadata
 *)
let rec simplify_typ_param (env:T.env_t) (p:typ_param) : ML typ_param =
  match p with
  | Inl e -> simplify_expr env e |> Inl
  | Inr oe -> simplify_out_expr env oe |> Inr

and simplify_typ (env:T.env_t) (t:typ)
  : ML typ
  = match t.v with
    | Pointer t -> {t with v=Pointer (simplify_typ env t)}
    | Type_app s b ps ->
      let ps = List.map (simplify_typ_param env) ps in
      let s = B.resolve_record_case_output_extern_type_name (fst env) s in
      let t = { t with v = Type_app s b ps } in
      B.unfold_typ_abbrev_only (fst env) t

and simplify_out_expr_node (env:T.env_t) (oe:with_meta_t out_expr')
val simplify_out_expr_node (env: T.env_t) (oe: with_meta_t out_expr') : ML (with_meta_t out_expr')
env: TypeSizes.env_t -> oe: Ast.with_meta_t Ast.out_expr'
  -> FStar.All.ML (Ast.with_meta_t Ast.out_expr')