val expressions_to_tds (exps: list expression_t) : GTot (list object_td_t)
val expressions_to_tds (exps: list expression_t) : GTot (list object_td_t)
let rec expressions_to_tds (exps: list expression_t) : GTot (list object_td_t) =
  match exps with
  | [] -> []
  | first_exp :: remaining_exps -> (expression_to_td first_exp) :: (expressions_to_tds remaining_exps)
module Armada.Expression

open Armada.Base
open Armada.BinaryOp
open Armada.BoundedInt
open Armada.Computation
open Armada.Memory
open Armada.Pointer
open Armada.State
open Armada.Thread
open Armada.Type
open Armada.UnaryOp
open FStar.Sequence.Base
open Spec.List
open Spec.Ubool
open Util.List

let rec build_function_type (return_type: Type0) (operand_types: list Type0) : Type =
  match operand_types with
  | [] -> conditional_computation_t return_type
  | first_type :: remaining_types -> (first_type -> GTot (build_function_type return_type remaining_types))

noeq type expression_t =
  | ExpressionConstant: (value: object_value_t) -> expression_t
  | ExpressionGlobalVariable: (td: object_td_t) -> (var_id: var_id_t) -> expression_t
  | ExpressionLocalVariable: (td: object_td_t) -> (var_id: var_id_t) -> expression_t
  | ExpressionUnaryOperator:
      (operand_td: object_td_t) -> (result_td: object_td_t) ->
      (operator: unary_op_t operand_td result_td) -> (operand: expression_t) -> expression_t
  | ExpressionBinaryOperator:
      (operand_td1: object_td_t) -> (operand_td2: object_td_t) -> (result_td: object_td_t) ->
      (operator: binary_op_t operand_td1 operand_td2 result_td) ->
      (operand1: expression_t) -> (operand2: expression_t) -> expression_t
  | ExpressionIf: (td: object_td_t) -> (cond: expression_t) -> (operand_then: expression_t) ->
      (operand_else: expression_t) -> expression_t
  | ExpressionDereference: (td: object_td_t) -> (ptr: expression_t) -> expression_t
  | ExpressionAddressOf: (obj: expression_t) -> expression_t
  | ExpressionPointerOffset: (ptr: expression_t) -> (offset: expression_t) -> expression_t
  | ExpressionFieldOf: (td: object_td_t) -> (obj: expression_t) -> (field_id: nat) -> expression_t
  | ExpressionAllocated: (ptr: expression_t) -> expression_t
  | ExpressionApplyFunction:
      (td: object_td_t) -> (operands: list expression_t) -> (return_type: Type0) -> (operand_types: list Type0) ->
      (fn: build_function_type return_type operand_types) -> expression_t
  | ExpressionIfUndefined:
      (td: object_td_t) -> (potentially_unsafe: expression_t) -> (safe_substitution: expression_t) -> expression_t
  | ExpressionInitialTid: expression_t
  | ExpressionUniqsUsed: expression_t
  | ExpressionStopReason: expression_t

let expression_to_td (exp: expression_t) : GTot object_td_t =
  match exp with
  | ExpressionConstant value -> object_value_to_td value
  | ExpressionGlobalVariable td _ -> td
  | ExpressionLocalVariable td _ -> td
  | ExpressionUnaryOperator _ result_td _ _ -> result_td
  | ExpressionBinaryOperator _ _ result_td _ _ _ -> result_td
  | ExpressionIf td _ _ _ -> td
  | ExpressionDereference td _ -> td
  | ExpressionAddressOf obj -> ObjectTDPrimitive PrimitiveTDPointer
  | ExpressionPointerOffset _ _ -> ObjectTDPrimitive PrimitiveTDPointer
  | ExpressionFieldOf td _ _ -> td
  | ExpressionAllocated _ -> ObjectTDPrimitive PrimitiveTDBool
  | ExpressionApplyFunction td _ _ _ _ -> td
  | ExpressionIfUndefined td _ _ -> td
  | ExpressionInitialTid -> ObjectTDAbstract tid_t
  | ExpressionUniqsUsed -> ObjectTDAbstract (list root_id_uniquifier_t)
  | ExpressionStopReason -> ObjectTDAbstract stop_reason_t
/
Util.List.fst.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.UnaryOp.fst.checked Armada.Type.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.State.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Computation.fst.checked Armada.BoundedInt.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked
Armada.Expression.fst
exps: Prims.list Armada.Expression.expression_t -> Prims.GTot (Prims.list Armada.Type.object_td_t)
Prims.list Armada.Expression.expression_t Prims.Nil Armada.Type.object_td_t Prims.Cons Armada.Expression.expression_to_td Armada.Expression.expressions_to_tds
let rec expressions_to_tds (exps: list expression_t) : GTot (list object_td_t) =
  
match exps with
| [] -> []
| first_exp :: remaining_exps -> (expression_to_td first_exp) :: (expressions_to_tds remaining_exps)