alms-0.6.5: examples/session-types-polygons.alms

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

#load "libthread"
#load "libsessiontype"

open SessionType

(*
We first build a tiny 3-D geometry library
*)
module type GEOMETRY = sig
  (* Points, planes, and line segments in R³ *)
  type point   = { x, y, z : float }
  type plane   = { a, b, c, d : float }
  type segment = point × point

  (*
    The plane { a, b, c, d } represents the open half-space
    { (x, y, z) | ax + by + cz + d > 0 }
  *)

  val string_of_point : point → string
  val string_of_plane : plane → string

  val point_of_string : string → point
  val plane_of_string : string → plane

  (* Is the point above the plane?  (i.e., in the semi-space) *)
  val isPointAbovePlane         : point → plane → bool

  (* Does the line segment between the two points intersect the plane,
     and if so, where? *)
  val intersect       : segment → plane → point option
end

module Geometry : GEOMETRY = struct
  type point   = { x, y, z : float }
  type plane   = { a, b, c, d : float }
  type segment = point × point

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

  let string_of_plane {a, b, c, d} =
      string_of a ^ "x + " ^ string_of b ^ "y + " ^
      string_of c ^ "z + " ^ string_of d ^ " > 0"

  (* Some of this should be in the library! *)
  let splitWhile pred =
    let rec loop acc xs =
              match xs with
              | []      → (rev acc, [])
              | x ∷ xs' → if pred x
                            then loop (x ∷ acc) xs'
                            else (rev acc, xs)
     in loop []

  let notp = compose not

  let isSpace = function
    | ' '  → true
    | '\t' → true
    | '\n' → true
    | '\r' → true
    | _    → false

  let dropSpace = compose snd (splitWhile isSpace)

  let point_of_string s =
    let foil = compose float_of_string implode 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
        { x = foil x, y = foil y, z = foil z }

  let plane_of_string s =
    let foil = compose float_of_string implode 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
        { a = foil a, b = foil b, c = foil c, d = foil d }

  let isPointAbovePlane { x, y, z } { a, b, c, d } =
    a *. x +. b *. y +. c *. z +. d >. 0.0

  let intersect (p1, p2) ({ a, b, c, d } as plane) =
   if isPointAbovePlane p1 plane == isPointAbovePlane p2 plane
     then None
     else let t = (a *. p1.x +. b *. p1.y +. c *. p1.z +. d) /.
                  (a *. (p1.x -. p2.x) +.
                   b *. (p1.y -. p2.y) +.
                   c *. (p1.z -. p2.z)) in
          let x = p1.x +. (p2.x -. p1.x) *. t in
          let y = p1.y +. (p2.y -. p1.y) *. t in
          let z = p1.z +. (p2.z -. p1.z) *. t in
            Some { x, y, z }
end

open Geometry

(*
Our protocol is to send an unbounded sequence of points:
*)
type `a stream = mu 's. 1 |&| ?`a; 's

(*
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: plane)
            (ic: point stream channel)
            (oc: point stream dual channel) =
       let finish (oc: point stream dual channel) =
             sel1 oc; () in
       let put pt (oc: point stream dual channel) =
             send pt (sel2 oc) in
       let putCross p1 p2 (oc: point stream dual channel) =
             match intersect (p1, p2) plane with
             | Some pt → put pt oc
             | None    → oc in
       let putVisible pt (oc: point stream dual channel) =
             if isPointAbovePlane pt plane
               then put pt oc
               else oc in
         match follow ic with
         | Left _   → finish oc
         | Right ic →
             let (pt0, ic) = recv ic in
             let rec loop pt
                          (ic: point stream channel)
                          (oc: point stream dual channel) =
                       let oc = putVisible pt oc in
                         match follow ic with
                         | Left _   → let oc = putCross pt pt0 oc in
                                         finish oc
                         | Right ic → let (pt', ic) = recv ic in
                                       let oc = putCross pt pt' oc in
                                         loop pt' ic oc
               in loop pt0 ic oc

let rec printer ic =
  match follow ic with
  | Left _   → ()
  | Right ic → let (pt, ic) = recv ic in
      putStrLn (string_of_point pt);
      printer ic

-- The main protocol for the program, which lets us split our parser
-- from our main loop.
type main_prot = mu 's. point stream |&| ?plane; 's

let parser =
  let rec plane_loop (oc: main_prot dual channel) =
            match getLine () with
            | "" → point_loop (sel1 oc)
            | s  → let plane = plane_of_string s in
                    let oc    = send plane (sel2 oc) in
                      plane_loop oc
      and point_loop (oc: point stream dual channel) =
            match getLine () with
            | "" → sel1 oc; ()
            | s  → let point = point_of_string s in
                    let oc    = send point (sel2 oc) in
                      point_loop oc
   in plane_loop

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

in
  main ()