Theory Step_External

theory Step_External
imports LLVM_Step
begin

context small_step
begin

inductive assign_unknown_value for n s' where
  "assign_unknown_value n s'"
if "s' = update_frames_stack n (Inr c)"

definition call_external_function :: "name ⇒ operand list ⇒ name ⇒ llvm_state error ⇒ bool" where
  "call_external_function fn os n s' =
    (case (map_of_funs fn) of
      Some (ExternalFunction _ fn ps) ⇒
        (case (zip_parameters os ps) of Inr _ ⇒ assign_unknown_value n s'
                                      | Inl es ⇒ (s' = Inl es))
     | _ ⇒ s' = call_function fn os)"

end (* context small_step *)

end