NetKAT_Syntax_GADT.ml

(* Run this with utop *)
#require "core";;

(* NetKAT syntax using GADTs *)

open Core.Std

type switchId = Int64.t

type portId = Int32.t

type location =
  | PhysicalPort of portId
  | Pipe of string
  | Query of string

type _ header =
  | Switch : switchId header
  | Location : location header
  | IP4Src : Int32.t header
  | IP4Dst : Int32.t header

type pred =
  | True
  | False
  | Test : 'a header * 'a -> pred
  | And of pred * pred
  | Or of pred * pred
  | Neg of pred

type pol =
  | Filter of pred
  | Mod : 'a header * 'a -> pol
  | Union of pol * pol
  | Seq of pol * pol
  | Star of pol
  | Link of switchId * portId * switchId * portId

(* This actually sucks. *)

type box = Box : 'a header -> box

let rec pol_fields (pol : pol) : box Set.Poly.t = match pol with
  | Filter a -> Set.Poly.empty
  | Mod (hdr, _) -> Set.Poly.singleton (Box hdr)
  | Union (p, q) -> Set.Poly.union (pol_fields p) (pol_fields q)
  | Seq (p, q) -> Set.Poly.union (pol_fields p) (pol_fields q)
  | Star p -> pol_fields p
  | Link _ -> Set.Poly.of_list [Box Switch; Box Location]

and pred_fields (pred : pred) : box Set.Poly.t = match pred with
  | True -> Set.Poly.empty
  | False -> Set.Poly.empty
  | Test (hdr, _) -> Set.Poly.singleton (Box hdr)
  | And (a, b) -> Set.Poly.union (pol_fields a) (pol_fields b)
  | Or (a, b) -> Set.Poly.union (pol_fields a) (pol_fields b)
  | Neg a -> pol_fields a