open HolKernel Parse boolLib
infix THEN

open bossLib

local open TNet_oksTheory TNet_LIBinterfaceTheory TNet_auxfnsTheory in end;

open TNet_typesTheory;  (* needed for ^duration_ty ... why? *)

val _ = new_theory "TNet_host0";

val OP_def =
  Define`OP fd opn =
           (?is ps. opn = bind(fd, is, ps)) \/
           (?i ps. opn = connect(fd, i, ps)) \/
           (opn = disconnect fd) \/
           (opn = getsockname fd) \/
           (opn = getpeername fd) \/
           (opn = geterr fd) \/
           (?opt. opn = getsockopt(fd, opt)) \/
           (?opt b. opn = setsockopt(fd, opt, b)) \/
           (?v data nb. opn = sendto(fd, v, data, nb)) \/
           (?nb. opn = recvfrom(fd, nb)) \/
           (opn = close fd)`;

val OP2_def =
  Define`OP2 fd ts =
           (?junk. ts = Sendto2(fd, junk)) \/
           (ts = Recvfrom2 fd)`;

val _ =
    Hol_datatype
      `Lhost0 = Lh_call of tid # LIB_interface
              | Lh_return of tid # TLang
              | Lh_sendmsg of msg
              | Lh_recvmsg of msg
              | Lh_console of string
              | Lh_tau
              | Lh_epsilon of ^duration_ty
              | Lh_exit                     `;

(* -------------------------------------------------- *)
(* this definition really should be built in... *)

val real_of_int_def =
  Define`real_of_int (i:int) = if i < 0 then ~(real_of_num (Num ~i))
                               else real_of_num (Num i)`;

(* -------------------------------------------------- *)

val _ =
    Hol_datatype
      `rule_ids = socket_1 | socket_2 |
                  bind_1 | bind_2 | bind_3 | bind_4 | bind_5 | bind_6 |
                    bind_7 | bind_8 | bind_9 |
                  connect_1 | connect_2 | connect_3 |
                  disconnect_1 | disconnect_2 | disconnect_3 |
                  getsockname_1 | getpeername_1 |
                  geterr_1 | getsockopt_1 | setsockopt_1 |
                  sendto_1 | sendto_2 | sendto_3 | sendto_4 | sendto_5 |
                    sendto_6 | sendto_7 | sendto_8 | sendto_9 |
                    sendto_10 |
                  recvfrom_1 | recvfrom_2 | recvfrom_3 | recvfrom_4 |
                    recvfrom_5 | recvfrom_6 | recvfrom_7 |
                  close_1 |
                  select_1 | select_2 | select_3 | select_4 |
                  delay_1 | delay_2 | delay_3 |
                  getifaddrs_1 |
                  console_print_1 | console_print_2 |
                  convert_port_1 | convert_port_2 |
                  convert_ip_1 | convert_ip_2 |
                  notsockfd_1 | notsockfd_2 |
                  intr_1 |
                  badmem_1 | badmem_2 | badmem_3 | badmem_4 |
                  exit_1 |  exit_2 |
                  ret_1 |
                  create_1 | create_2 |
                  delivery_out_1 | delivery_out_martian |
                  delivery_in_udp_1 | delivery_in_udp_2 |
                    delivery_in_martian_3 |
                  delivery_in_icmp_1 | delivery_in_icmp_2 |
                  delivery_loopback_udp_1 | delivery_loopback_udp_2 |
                  delivery_loopback_icmp_1 | delivery_loopback_icmp_2 |
                  epsilon_1`;

val _ =
    Hol_datatype
      `rule_cats = succeed     | fail     | badfail     |
                   slowsucceed | slowfail |
                   exit        | enter2   | misc`;


val _ = export_theory();