// The main effects of call/cc are:
// 1. create a "hole" where it was called
// 2. create a function 'k' which fills that hole when applied
// For example, consider the following Scheme expression:
//
// (+ 10 (call/cc (lambda (k) (+ (k 42) 1729))))
//
// To evaluate it, the entire `(call/cc ...)` part is replaced by a hole:
//
// (+ 10 _)
//
// Then, Scheme creates an internal function, `k`, which, when called `(k arg)`,
// will replace the hole `_` by `arg`. That function is sent to the user's
// callback `(lambda (k) ...)`, allowing they to decide when and how to fill
// that hole. In the example above, the user calls `(k 42)`, so the result is:
//
// (+ 10 42)
// 
// And the remaining of the expression, `(+ _ 1729)`, will be garbage collected.
// 
// This ability can be used for various useful purposes, such as exceptions.
// It's impossible to implement this behavior on the pure lambda calculus. On
// interaction combinators, call/cc can be implemented by manipulating some
// edges. For example, consider the graph below:
// 
//   result              garbage   
//      |                  |     
//      +                  @ 
//     / \_____,          / \________,
//    |        |     _____λ          |
//    10       |     |    |       ,--λ <-(very illegal)
//             |     |    +       |  |
//             |     |   / \      |  *
//             |     |  @  1729   |
//             |     |_/ \        |
//             |         42       |
//             |                  |
//             |__________________|
//  
// After some reductions, an intermediate result will be:
//
//          result      garbage
//            |            |
//           [+]          [+]
//           / \         /   \
//         10   42      *    1729
// 
// Here, the user-defined callback `(λ (k) (+ (k 42) 1729))` received a
// continuation `k` and applied it to `42`, "filling" the hole `(+ 10 _)`,
// giving us the correct result. We could implement continuations on the HVM  by
// including a `call/cc` syntax, and then doing the transformation above when
// converting from text to graphs. Meanwhile, it is possible to implement an
// uglier version of it as a library, using scopeless λs. Here is an example:

// Creates a program capable of performing call/cc.
(CC.lang program) =
  let callcc  = λcallback (λ$garbage($hole) (callback λ$hole(0)))
  let result  = (program callcc)
  let garbage = $garbage
  (Seq garbage result)

// Helper function for strictness annotation 
(Seq 0 b) = b
(Seq a b) = b

// Notice the call/cc function receives the user-defined callback. It then gives
// the user an internal function that, when called, will fill the hole, and
// return it on the position where call/cc was called. The value returned by the
// callback itself is then moved to the garbage, which is collected.

// Example usage
Main = (CC.lang λcallcc
  (+ 10 (callcc λk(+ (k 42) 1729))))

// The result is `(Pair (Result 52) (Garbage 1729))`, as expected.
// Reference: http://www.madore.org/~david/computers/callcc.html

// -----------------------------------------------------------------------------

// Note: to be really useful, we must also be able to use a continuation more
// than once. For example, consider the following Scheme program:
// > (define k 0)
// > (+ 10 (call/cc (λ (k_) (set! cont k_))))
// > (k 3)
// > (k 4)
// Its result is to output `13` and `14`, which is the continuation filled with
// `3` and `4`. In theory, we should also be able to achieve that on HVM as:

//Main = (CC.lang λcallcc [
  //(+ 10 (callcc λ$k (3)))
  //($k 3)
  //($k 4)
//])
    
// Notice that, while we're not able to move k_ out of the closure by setting a
// global variable, we can still do it by using scopeless lambdas. Sadly, using
// a global variable like `$k` more than once is not supported by the graph
// builder yet. We can kind of hack our way into having it though:

//Main = (CC.lang λcallcc [
  //(+ 10 (callcc λ$k (λfλa(f a a) λ$k0λ$k1(3) $k)))
  //($k0 3)
  //($k1 4)
//])

// Which correctly computes 13 and 14 by filling the `(+ 10 _)` continuation.
// Note that this is *terribly* ugly as it accumulates results in a list of
// superpositions and the garbage. Of course a proper callcc library would
// support multiple calls, collecting intermediate garbage and results and
// displaying or returning them appropriately. The point of this is to
// illustrate how the ability to "freeze" a "call stack" and instantiate is
// already present on HVM "for free". There is no need to implement anything new
// on the evaluator, and everything can be done as a library with proper syntax.