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

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

#load "libsessiontype2"

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 is_point_above_plane         : 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 is_point_above_plane { x, y, z } { a, b, c, d } =
    a *. x +. b *. y +. c *. z +. d >. 0.0

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

open Geometry

(* The protocol *)
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 p     = choose Next oc; send p oc in
  let putCross p₁ p₂ =
    match intersect (p₁, p₂) plane with
    | Some p  → put p
    | None    → () in
  let putVisible p =
    if is_point_above_plane p plane
      then put p
      else ()
  in follow ic;
     match ic with
     | Done ic → finish ()
     | Next ic →
       let p₀ = recv ic in
       let rec loop p =
         putVisible p;
         follow ic;
         match ic with
         | Done ic →
             putCross p p₀;
             finish ()
         | Next ic →
             let p′ = recv ic in
               putCross p p′;
               loop p′
       in loop p₀

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 (plane_of_string s) oc;
                    plane_loop ()
      and point_loop () =
            match getLine () with
            | "" → choose Done oc
            | s  → choose Next oc;
                    send (point_of_string 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 connect plane (ic : point stream channel) =
        let outrv = newRendezvous () in
          Thread.fork (λ_ → clipper plane (ic, accept outrv); ());
          request outrv in
  let rv           = newRendezvous () in
  let _            = Thread.fork (λ_ → parser (accept rv); ()) in
  let (planes, ic) = get_planes [] (request rv) in
  let ic           = foldl connect ic planes
  in
    printer ic

in main ()