alms-0.6.0: examples/session-types-polygons2.alms

-- Sutherland-Hodgman (1974) re-entrant polygon clipping

#load "libthread"
#load "libsessiontype2"

open SessionType

--
-- We first build a 3-D geometry library in sublanguage C:
--

-- Points and planes in R^3.
type point = Point of float * float * float
type plane = Plane of float * float * float * float

-- We use the plane Plane(a, b, c, d) to represent the open half-space
-- { Point(x, y, z) | ax + by + cz + d > 0 }

let string_of_point (Point(x, y, z)) =
    "(" ^ string_of x ^ ", " ^ string_of y ^ ", " ^ string_of z ^ ")"

let string_of_plane (Plane(a, b, c, d)) =
    string_of a ^ "x + " ^ string_of b ^ "y + " ^
    string_of c ^ "z + " ^ string_of d ^ " > 0"

let splitWhile : ('a -> bool) -> 'a list -> 'a list * 'a list
  = fun pred ->
      let rec loop (acc: 'a list) (xs: 'a list) : 'a list * 'a list =
                match xs with
                | []     -> (rev acc, [])
                | x ∷ xs' -> if pred x
                               then loop (x ∷ acc) xs'
                               else (rev acc, xs)
       in loop []

let notp (pred: 'a -> bool) (x: 'a) = not (pred x)

let isSpace c =
  match c with
  | ' '  -> true
  | '\t' -> true
  | '\n' -> true
  | '\r' -> true
  | _    -> false

let dropSpace cs = snd (splitWhile isSpace cs)

let parsePoint (s : string) : point =
  let foil (x: char list) = float_of_string (implode x) in
    let cs = explode s in
    let '(' ∷ cs = dropSpace cs in
    let (x, _ ∷ cs) = splitWhile (notp ((==) ',')) (dropSpace cs) in
    let (y, _ ∷ cs) = splitWhile (notp ((==) ',')) (dropSpace cs) in
    let (z, _ ∷ cs) = splitWhile (notp ((==) ')')) (dropSpace cs) in
      Point (foil x, foil y, foil z)

let parsePlane (s: string) : plane =
  let foil (x: char list) = float_of_string (implode x) in
    let cs = explode s in
    let (a, _ ∷ cs) = splitWhile (notp ((==) 'x')) (dropSpace cs) in
    let '+' ∷ cs    = dropSpace cs in
    let (b, _ ∷ cs) = splitWhile (notp ((==) 'y')) (dropSpace cs) in
    let '+' ∷ cs    = dropSpace cs in
    let (c, _ ∷ cs) = splitWhile (notp ((==) 'z')) (dropSpace cs) in
    let '+' ∷ cs    = dropSpace cs in
    let (d, _ ∷ cs) = splitWhile (notp ((==) '>')) (dropSpace cs) in
    let '0' ∷ cs    = dropSpace cs in
      Plane (foil a, foil b, foil c, foil d)

-- Is the point above the plane?  (i.e., in the semi-space)
let isPointAbovePlane (Point(x, y, z): point)
                         (Plane(a, b, c, d): plane): bool =
  a *. x +. b *. y +. c *. z +. d >. 0.0

-- Does the line segment between the two points intersect the plane,
-- and if so, where?
let intersect (Point(x1, y1, z1) as p1 : point)
              (Point(x2, y2, z2) as p2 : point)
              (Plane(a, b, c, d) as plane : plane): point option =
 if isPointAbovePlane p1 plane == isPointAbovePlane p2 plane
   then None
   else let t = (a *. x1 +. b *. y1 +. c *. z1 +. d) /.
                (a *. (x1 -. x2) +.
                 b *. (y1 -. y2) +.
                 c *. (z1 -. z2)) in
        let x = x1 +. (x2 -. x1) *. t in
        let y = y1 +. (y2 -. y1) *. t in
        let z = z1 +. (z2 -. z1) *. t in
          Some (Point (x, y, z))

--
-- In sublanguage A, our protocol is to send an unbounded
-- sequence of points:
--

type 'a stream = ?->('a step)
 and 'a step   = Done of 1 channel
               | Next of (?'a; 'a stream) channel

--
-- Each transducer takes a plane to clip by, and two rendezvous objects,
-- the first on which it expects to receive points, and the second on
-- which it will send points.
--

let clipper plane
            !(ic: point stream channel, oc: point stream dual channel) =
  let finish () =
    choose Done oc in
  let put pt =
    choose Next oc;
    send pt oc in
  let putCross p1 p2 =
    match intersect p1 p2 plane with
    | Some pt -> put pt
    | None    -> () in
  let putVisible pt =
    if isPointAbovePlane pt plane
      then put pt
      else ()
   in follow ic;
      match ic with
      | Done ic -> finish ()
      | Next ic ->
        let pt0 = recv ic in
        let rec loop pt =
          putVisible pt;
          follow ic;
          match ic with
          | Done ic -> putCross pt pt0;
                       finish ()
          | Next ic -> let pt' = recv ic in
                       putCross pt pt';
                       loop pt'
         in loop pt0

let rec printer !(ic: point stream channel) =
  follow ic;
  match ic with
  | Done ic -> ()
  | Next ic -> putStrLn (string_of_point (recv ic));
               printer ic

-- The main protocol for the program, which lets us split our parser
-- from our main loop.
type main_prot = ?->main2
    and main2     = Planes of (?plane; main_prot) channel
                  | Points of point stream channel

let parser (!oc: main_prot dual channel) =
  let rec plane_loop () =
            match getLine () with
            | "" -> choose Points oc;
                    point_loop ()
            | s  -> choose Planes oc;
                    send (parsePlane s) oc;
                    plane_loop ()
      and point_loop () =
            match getLine () with
            | "" -> choose Done oc
            | s  -> choose Next oc;
                    send (parsePoint s) oc;
                    point_loop ()
   in plane_loop ()

let main =
  let rec get_planes (acc: plane list) !(ic: main_prot channel) =
            follow ic;
            match ic with
            | Points ic -> rev acc
            | Planes ic -> get_planes (recv ic ∷ acc) ic in
  let rec connect (planes: plane list)
                  (ic: point stream channel)
                  : point stream channel =
            match planes with
            | []              -> ic
            | plane ∷ rest ->
                let outrv = newRendezvous () in
                  AThread.fork
                    (fun () -> clipper plane (ic, accept outrv); ());
                  connect rest (request outrv) in
  fun () ->
    let rv           = newRendezvous () in
    let _            = AThread.fork (fun () -> parser (accept rv); ()) in
    let (planes, ic) = get_planes [] (request rv) in
    let ic           = connect planes ic in
      printer ic

in
  main ()