-- GeNeRaTeD fOr: /home/thomas/repos/plancomps/CBS-beta/Unstable-Funcons-beta/Computations/Threads/Synchronising/Notifications/Notifications.cbs
{-# LANGUAGE OverloadedStrings #-}

module Funcons.Core.Computations.Threads.Synchronising.Notifications.Notifications where

import Funcons.EDSL

import Funcons.Operations hiding (Values,libFromList)
entities :: [a]
entities = []

types :: TypeRelation
types = [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList
    []

funcons :: FunconLibrary
funcons = [(Name, EvalFunction)] -> FunconLibrary
libFromList
    [(Name
"barrier-create",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBarrier_create),(Name
"barrier-sync",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBarrier_sync),(Name
"barrier-sync-else-wait",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBarrier_sync_else_wait),(Name
"condition-create",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepCondition_create),(Name
"condition-wait",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepCondition_wait),(Name
"condition-wait-with-lock",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepCondition_wait_with_lock),(Name
"condition-notify-all",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepCondition_notify_all),(Name
"condition-notify-first",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepCondition_notify_first),(Name
"rendezvous-create",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRendezvous_create),(Name
"rendezvous-sync",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRendezvous_sync),(Name
"rendezvous-sync-else-wait",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRendezvous_sync_else_wait),(Name
"rendezvous-waits",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepRendezvous_waits),(Name
"is-rendezvous-match",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_rendezvous_match),(Name
"rendezvous-first-match-thread",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRendezvous_first_match_thread),(Name
"rendezvous-first-match-drop",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRendezvous_first_match_drop)]

barrier_create_ :: [Funcons] -> Funcons
barrier_create_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"barrier-create" ([Funcons]
fargs)
stepBarrier_create :: StrictFuncon
stepBarrier_create [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"pos-ints")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"give" [Name -> [FTerm] -> FTerm
TApp Name
"sync-create" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature-create" [Name -> FTerm
TName Name
"sync-waiting-list"],Name -> [FTerm] -> FTerm
TApp Name
"sync-feature-create" [Name -> FTerm
TName Name
"sync-count"]],Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [Name -> FTerm
TName Name
"given",Name -> FTerm
TName Name
"sync-count"],MetaVar -> FTerm
TVar MetaVar
"N"],Name -> FTerm
TName Name
"given"]]) Env
env

barrier_sync_ :: [Funcons] -> Funcons
barrier_sync_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"barrier-sync" ([Funcons]
fargs)
stepBarrier_sync :: StrictFuncon
stepBarrier_sync [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SY") (Name -> FTerm
TName Name
"syncs")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"thread-atomic" [Name -> [FTerm] -> FTerm
TApp Name
"give" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-count"],Name -> [FTerm] -> FTerm
TApp Name
"else" [Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> FTerm
TName Name
"given"],Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (forall t. Integer -> Values t
Nat Integer
0))]],Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> FTerm
TName Name
"given"],Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (forall t. Integer -> Values t
Nat Integer
1))]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> FTerm
TName Name
"given",Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (forall t. Integer -> Values t
Nat Integer
0))],Name -> [FTerm] -> FTerm
TApp Name
"thread-resume" [Name -> [FTerm] -> FTerm
TApp Name
"list-elements" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-waiting-list"]]]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-waiting-list"],Name -> [FTerm] -> FTerm
TApp Name
"list" []]]]]]) Env
env

barrier_sync_else_wait_ :: [Funcons] -> Funcons
barrier_sync_else_wait_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"barrier-sync-else-wait" ([Funcons]
fargs)
stepBarrier_sync_else_wait :: StrictFuncon
stepBarrier_sync_else_wait [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SY") (Name -> FTerm
TName Name
"syncs")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"thread-atomic" [Name -> [FTerm] -> FTerm
TApp Name
"else" [Name -> [FTerm] -> FTerm
TApp Name
"barrier-sync" [MetaVar -> FTerm
TVar MetaVar
"SY"],Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"sync-waiting-list-add" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"current-thread"],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-count"],Name -> [FTerm] -> FTerm
TApp Name
"checked" [Name -> [FTerm] -> FTerm
TApp Name
"nat-pred" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-count"]]]]],Name -> [FTerm] -> FTerm
TApp Name
"thread-suspend" [Name -> FTerm
TName Name
"current-thread"]]]]) Env
env

condition_create_ :: Funcons
condition_create_ = Name -> Funcons
FName Name
"condition-create"
stepCondition_create :: NullaryFuncon
stepCondition_create = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"sync-create" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature-create" [Name -> FTerm
TName Name
"sync-waiting-list"]]) forall {k} {a}. Map k a
env

condition_wait_ :: [Funcons] -> Funcons
condition_wait_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"condition-wait" ([Funcons]
fargs)
stepCondition_wait :: StrictFuncon
stepCondition_wait [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SY") (Name -> FTerm
TName Name
"syncs")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"thread-atomic" [Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"sync-waiting-list-add" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"current-thread"],Name -> [FTerm] -> FTerm
TApp Name
"thread-suspend" [Name -> FTerm
TName Name
"current-thread"]]]) Env
env

condition_wait_with_lock_ :: [Funcons] -> Funcons
condition_wait_with_lock_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"condition-wait-with-lock" ([Funcons]
fargs)
stepCondition_wait_with_lock :: StrictFuncon
stepCondition_wait_with_lock [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SY") (Name -> FTerm
TName Name
"syncs"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"L") (Name -> FTerm
TName Name
"syncs")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"thread-atomic" [Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"exclusive-lock-release" [MetaVar -> FTerm
TVar MetaVar
"L"],Name -> [FTerm] -> FTerm
TApp Name
"sync-waiting-list-add" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"current-thread"],Name -> [FTerm] -> FTerm
TApp Name
"thread-suspend" [Name -> FTerm
TName Name
"current-thread"]]],Name -> [FTerm] -> FTerm
TApp Name
"exclusive-lock-sync-else-wait" [MetaVar -> FTerm
TVar MetaVar
"L"]]) Env
env

condition_notify_all_ :: [Funcons] -> Funcons
condition_notify_all_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"condition-notify-all" ([Funcons]
fargs)
stepCondition_notify_all :: StrictFuncon
stepCondition_notify_all [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SY") (Name -> FTerm
TName Name
"syncs")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"thread-atomic" [Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"thread-resume" [Name -> [FTerm] -> FTerm
TApp Name
"list-elements" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-waiting-list"]]]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-waiting-list"],Name -> [FTerm] -> FTerm
TApp Name
"list" []]]]) Env
env

condition_notify_first_ :: [Funcons] -> Funcons
condition_notify_first_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"condition-notify-first" ([Funcons]
fargs)
stepCondition_notify_first :: StrictFuncon
stepCondition_notify_first [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SY") (Name -> FTerm
TName Name
"syncs")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"thread-atomic" [Name -> [FTerm] -> FTerm
TApp Name
"give" [Name -> [FTerm] -> FTerm
TApp Name
"sync-waiting-list-head-remove" [MetaVar -> FTerm
TVar MetaVar
"SY"],Name -> [FTerm] -> FTerm
TApp Name
"thread-resume" [Name -> FTerm
TName Name
"given"]]]) Env
env

rendezvous_create_ :: [Funcons] -> Funcons
rendezvous_create_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rendezvous-create" ([Funcons]
fargs)
stepRendezvous_create :: StrictFuncon
stepRendezvous_create [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"pos-ints")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"give" [Name -> [FTerm] -> FTerm
TApp Name
"sync-create" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature-create" [Name -> FTerm
TName Name
"sync-waiting-list"],Name -> [FTerm] -> FTerm
TApp Name
"sync-feature-create" [Name -> FTerm
TName Name
"sync-count"]],Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [Name -> FTerm
TName Name
"given",Name -> FTerm
TName Name
"sync-count"],MetaVar -> FTerm
TVar MetaVar
"N"],Name -> FTerm
TName Name
"given"]]) Env
env

rendezvous_sync_ :: [Funcons] -> Funcons
rendezvous_sync_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rendezvous-sync" ([Funcons]
fargs)
stepRendezvous_sync :: StrictFuncon
stepRendezvous_sync [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SY") (Name -> FTerm
TName Name
"syncs"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"ground-values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"give" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-waiting-list"]],Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-rendezvous-match" [Name -> FTerm
TName Name
"given",MetaVar -> FTerm
TVar MetaVar
"V"]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-waiting-list"],Name -> [FTerm] -> FTerm
TApp Name
"rendezvous-first-match-drop" [Name -> FTerm
TName Name
"given",MetaVar -> FTerm
TVar MetaVar
"V"]],Name -> [FTerm] -> FTerm
TApp Name
"thread-resume" [Name -> [FTerm] -> FTerm
TApp Name
"rendezvous-first-match-thread" [Name -> FTerm
TName Name
"given",MetaVar -> FTerm
TVar MetaVar
"V"]]]]) Env
env

rendezvous_sync_else_wait_ :: [Funcons] -> Funcons
rendezvous_sync_else_wait_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rendezvous-sync-else-wait" ([Funcons]
fargs)
stepRendezvous_sync_else_wait :: StrictFuncon
stepRendezvous_sync_else_wait [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SY") (Name -> FTerm
TName Name
"syncs"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"ground-values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"thread-atomic" [Name -> [FTerm] -> FTerm
TApp Name
"else" [Name -> [FTerm] -> FTerm
TApp Name
"rendezvous-sync" [MetaVar -> FTerm
TVar MetaVar
"SY",MetaVar -> FTerm
TVar MetaVar
"V"],Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"sync-waiting-list-add" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> [FTerm] -> FTerm
TApp Name
"tuple" [MetaVar -> FTerm
TVar MetaVar
"V",Name -> FTerm
TName Name
"current-thread"]],Name -> [FTerm] -> FTerm
TApp Name
"thread-suspend" [Name -> FTerm
TName Name
"current-thread"]]]]) Env
env

rendezvous_waits_ :: Funcons
rendezvous_waits_ = Name -> Funcons
FName Name
"rendezvous-waits"
stepRendezvous_waits :: NullaryFuncon
stepRendezvous_waits = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"tuples" [Name -> FTerm
TName Name
"ground-values",Name -> FTerm
TName Name
"thread-ids"]) forall {k} {a}. Map k a
env

is_rendezvous_match_ :: [Funcons] -> Funcons
is_rendezvous_match_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-rendezvous-match" ([Funcons]
fargs)
stepIs_rendezvous_match :: StrictFuncon
stepIs_rendezvous_match [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [Values -> VPattern
VPLit (forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
108)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
105)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
115)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
116)])]),Name -> [VPattern] -> VPattern
PADT Name
"tuple" [MetaVar -> VPattern
VPMetaVar MetaVar
"V'",MetaVar -> VPattern
VPMetaVar MetaVar
"TI"],MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"P*" SeqSortOp
StarOp],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"V'",MetaVar -> FTerm
TVar MetaVar
"V"],Name -> FTerm
TName Name
"true",Name -> [FTerm] -> FTerm
TApp Name
"is-rendezvous-match" [Name -> [FTerm] -> FTerm
TApp Name
"list" [MetaVar -> FTerm
TVar MetaVar
"P*"],MetaVar -> FTerm
TVar MetaVar
"V"]]) Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [Values -> VPattern
VPLit (forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
108)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
105)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
115)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
116)])])],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env

rendezvous_first_match_thread_ :: [Funcons] -> Funcons
rendezvous_first_match_thread_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rendezvous-first-match-thread" ([Funcons]
fargs)
stepRendezvous_first_match_thread :: StrictFuncon
stepRendezvous_first_match_thread [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [Values -> VPattern
VPLit (forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
108)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
105)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
115)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
116)])]),Name -> [VPattern] -> VPattern
PADT Name
"tuple" [MetaVar -> VPattern
VPMetaVar MetaVar
"V'",MetaVar -> VPattern
VPMetaVar MetaVar
"TI"],MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"P*" SeqSortOp
StarOp],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"V'",MetaVar -> FTerm
TVar MetaVar
"V"],MetaVar -> FTerm
TVar MetaVar
"TI",Name -> [FTerm] -> FTerm
TApp Name
"rendezvous-first-match-thread" [Name -> [FTerm] -> FTerm
TApp Name
"list" [MetaVar -> FTerm
TVar MetaVar
"P*"],MetaVar -> FTerm
TVar MetaVar
"V"]]) Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [Values -> VPattern
VPLit (forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
108)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
105)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
115)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
116)])])],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"fail") Env
env

rendezvous_first_match_drop_ :: [Funcons] -> Funcons
rendezvous_first_match_drop_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rendezvous-first-match-drop" ([Funcons]
fargs)
stepRendezvous_first_match_drop :: StrictFuncon
stepRendezvous_first_match_drop [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [Values -> VPattern
VPLit (forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
108)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
105)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
115)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
116)])]),Name -> [VPattern] -> VPattern
PADT Name
"tuple" [MetaVar -> VPattern
VPMetaVar MetaVar
"V'",MetaVar -> VPattern
VPMetaVar MetaVar
"TI"],MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"P*" SeqSortOp
StarOp],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"V'",MetaVar -> FTerm
TVar MetaVar
"V"],Name -> [FTerm] -> FTerm
TApp Name
"list" [MetaVar -> FTerm
TVar MetaVar
"P*"],Name -> [FTerm] -> FTerm
TApp Name
"cons" [Name -> [FTerm] -> FTerm
TApp Name
"tuple" [MetaVar -> FTerm
TVar MetaVar
"V'",MetaVar -> FTerm
TVar MetaVar
"TI"],Name -> [FTerm] -> FTerm
TApp Name
"rendezvous-first-match-drop" [Name -> [FTerm] -> FTerm
TApp Name
"list" [MetaVar -> FTerm
TVar MetaVar
"P*"],MetaVar -> FTerm
TVar MetaVar
"V"]]]) Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [Values -> VPattern
VPLit (forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
108)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
105)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
115)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
116)])])],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"fail") Env
env