val apply_function_to_operands
      (operands: list object_value_t)
      (return_type: Type0)
      (operand_types: list Type0)
      (fn: build_function_type return_type operand_types)
    : GTot (conditional_computation_t return_type)
val apply_function_to_operands
      (operands: list object_value_t)
      (return_type: Type0)
      (operand_types: list Type0)
      (fn: build_function_type return_type operand_types)
    : GTot (conditional_computation_t return_type)
let rec apply_function_to_operands
  (operands: list object_value_t)
  (return_type: Type0)
  (operand_types: list Type0)
  (fn: build_function_type return_type operand_types)
  : GTot (conditional_computation_t return_type) =
  match operands, operand_types with
  | [], [] -> fn
  | first_operand :: remaining_operands, first_operand_type :: remaining_operand_types ->
      (match first_operand with
       | ObjectValueAbstract ty value ->
           if eqb first_operand_type ty then
             let fn_cast: first_operand_type -> GTot (build_function_type return_type remaining_operand_types) = fn in
             apply_function_to_operands remaining_operands return_type remaining_operand_types (fn_cast value)
           else
             ComputationUndefined
       | _ -> ComputationUndefined)
  | _ -> ComputationImpossible
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

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)

let rec types_to_tds (tys: list Type0) : (list object_td_t) =
  match tys with
  | [] -> []
  | first_ty :: remaining_tys -> (ObjectTDAbstract first_ty) :: (types_to_tds remaining_tys)

let rec expression_valid (exp: expression_t) : GTot bool =
  match exp with
  | ExpressionConstant value -> object_value_valid value
  | ExpressionGlobalVariable td _ -> true
  | ExpressionLocalVariable td _ -> true
  | ExpressionUnaryOperator operand_td result_td operator operand ->
         expression_valid operand
      && eqb (expression_to_td operand) operand_td
  | ExpressionBinaryOperator operand_td1 operand_td2 result_td operator operand1 operand2 ->
         expression_valid operand1
      && expression_valid operand2
      && eqb (expression_to_td operand1) operand_td1
      && eqb (expression_to_td operand2) operand_td2
  | ExpressionIf td cond operand_then operand_else ->
         expression_valid cond
      && expression_valid operand_then
      && expression_valid operand_else
      && eqb (expression_to_td cond) (ObjectTDPrimitive PrimitiveTDBool)
      && eqb (expression_to_td operand_then) td
      && eqb (expression_to_td operand_else) td
  | ExpressionDereference td ptr ->
         expression_valid ptr
      && eqb (expression_to_td ptr) (ObjectTDPrimitive PrimitiveTDPointer)
  | ExpressionAddressOf obj -> expression_valid obj
  | ExpressionPointerOffset ptr offset ->
         expression_valid ptr
      && expression_valid offset
      && eqb (expression_to_td ptr) (ObjectTDPrimitive PrimitiveTDPointer)
      && eqb (expression_to_td offset) (ObjectTDAbstract int)
  | ExpressionFieldOf td obj field_id ->
         expression_valid obj
      && ObjectTDStruct? (expression_to_td obj)
      && 0 <= field_id
      && field_id < length (ObjectTDStruct?.field_tds (expression_to_td obj))
      && eqb td ((ObjectTDStruct?.field_tds (expression_to_td obj)) `index` field_id)
  | ExpressionAllocated ptr ->
         expression_valid ptr
      && eqb (expression_to_td ptr) (ObjectTDPrimitive PrimitiveTDPointer)
  | ExpressionApplyFunction td operands return_type operand_types _ ->
         eqb td (ObjectTDAbstract return_type)
      && eqb (expressions_to_tds operands) (types_to_tds operand_types)
  | ExpressionIfUndefined td potentially_unsafe safe_substitution ->
         eqb td (expression_to_td potentially_unsafe)
      && eqb td (expression_to_td safe_substitution)
  | ExpressionInitialTid -> true
  | ExpressionUniqsUsed -> true
  | ExpressionStopReason -> true

type valid_expression_t = value: expression_t{expression_valid value}
/
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

    operands: Prims.list Armada.Type.object_value_t ->
    return_type: Type0 ->
    operand_types: Prims.list Type0 ->
    fn: Armada.Expression.build_function_type return_type operand_types
  -> Prims.GTot (Armada.Computation.conditional_computation_t return_type)
Prims.list Armada.Type.object_value_t Armada.Expression.build_function_type FStar.Pervasives.Native.Mktuple2 Spec.Ubool.eqb Armada.Expression.apply_function_to_operands Prims.bool Armada.Computation.ComputationUndefined Armada.Computation.conditional_computation_t FStar.Pervasives.Native.tuple2 Armada.Computation.ComputationImpossible
let rec apply_function_to_operands
      (operands: list object_value_t)
      (return_type: Type0)
      (operand_types: list Type0)
      (fn: build_function_type return_type operand_types)
    : GTot (conditional_computation_t return_type) =
  
match operands, operand_types with
| [], [] -> fn
| first_operand :: remaining_operands, first_operand_type :: remaining_operand_types ->
  (match first_operand with
    | ObjectValueAbstract ty value ->
      if eqb first_operand_type ty
      then
        let fn_cast: first_operand_type
          -> GTot (build_function_type return_type remaining_operand_types) =
          fn
        in
        apply_function_to_operands remaining_operands
          return_type
          remaining_operand_types
          (fn_cast value)
      else ComputationUndefined
    | _ -> ComputationUndefined)
| _ -> ComputationImpossible