Notes on porting TCP1_netTypes and TCP1_preHostTypes:

TCP1_netTypes:

OVERLOAD_ON OTHER SQ_OTHER is not ported to LEM

not handled:
val _ = overload_on("NET",     ``RD_NET``);
val _ = overload_on("HOST",    ``RD_HOST``);
val _ = overload_on("TOSNET",  ``RD_TOSNET``);
val _ = overload_on("TOSHOST", ``RD_TOSHOST``);
val _ = overload_on("OTHER",   ``RD_OTHER``);

FIXME
val _ = Parse.add_record_field("is1",``msg_is1``);  (* overload x.is1 *)
val _ = Parse.add_record_field("is2",``msg_is2``);  (* overload x.is2 *)

many records with same field names; changed e.g as follows
type
  (*: UDP datagram type :*)
udpDatagram
  = <| udp_is1 : option ip;      (* source IP *)
       udp_is2 : option ip;      (* destination IP *)
       udp_ps1 : option port;     (* source port *)
       udp_ps2 : option port;     (* destination port *)
       udp_data : list byte
    |>

--

TCP1_preHostTypes:

'a list -> list 'a
'a option -> option 'a
etc

in following, slow of bool => rule_status changed to pair
type
  rule_cat  = fast    of rule_status
            | block
            | slow    of bool  * rule_status

does LEM have curried constructors? yes, this is the syntax for
curried constructors; to make non-curried have to write eg |slow of
(bool * rule_status); this is similar to OCaml (?); in my opinion,
this is a confusion between constructors, and functions

bounded existential ? x :: xs. replaced with logical equivalent (does
LEM have bounded existentials?)

x ' y is FAPPLY x y

(* FIXME
val _ = overload_on ("<", ``fdlt``);
val _ = overload_on ("<=", ``fdle``);
*)

NOTIN no longer infix

>=, < etc on ints are int_geq etc