-- GeNeRaTeD fOr: ../../CBS/Funcons/Computations/Control flow/Abnormal/Continuations/call-cc.aterm
{-# LANGUAGE OverloadedStrings #-}

module Funcons.Core.Computations.ControlFlow.Abnormal.Continuations.CallCc where

import Funcons.EDSL

entities = []

types = typeEnvFromList
    []

funcons = libFromList
    [("call-cc",StrictFuncon stepCall_cc)]

-- |
-- /call-cc(F)/ emits a /control-signal/ that, when handled by an enclosing
--   /prompt/ , applies /F/ to the current continuation.  If that current
--   continuation argument is invoked, then the current computation will terminate
--   up to the enclosing /prompt/ when that continuation terminates.
call_cc_ fargs = FApp "call-cc" (FTuple fargs)
stepCall_cc fargs =
    evalRules [] [step1]
    where step1 = do
            let env = emptyEnv
            env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "F") (TName "values")] env
            env <- premise (TName "fresh-binder") (PMetaVar "K") env
            stepTermTo (TApp "control" (TTuple [TApp "binding-lambda" (TTuple [TVar "K",TApp "apply" (TTuple [TApp "bound" (TTuple [TVar "K"]),TApp "apply" (TTuple [TVar "F",TApp "lambda" (TTuple [TApp "abort" (TTuple [TApp "apply" (TTuple [TApp "bound" (TTuple [TVar "K"]),TName "given"])])])])])])])) env