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

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

import Funcons.EDSL

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

types :: TypeRelation
types = [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList
    [(Name
"syncs",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"syncs" [] [Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"sync" [Name -> FTerm
TName Name
"sync-feature-maps"] (forall a. a -> Maybe a
Just [])]),(Name
"sync-features",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"sync-features" [] [Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"sync-waiting-list" [] (forall a. a -> Maybe a
Just []),Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"sync-held" [] (forall a. a -> Maybe a
Just []),Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"sync-holder" [] (forall a. a -> Maybe a
Just []),Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"sync-count" [] (forall a. a -> Maybe a
Just [])])]

funcons :: FunconLibrary
funcons = [(Name, EvalFunction)] -> FunconLibrary
libFromList
    [(Name
"sync",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSync),(Name
"sync-create",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSync_create),(Name
"sync-feature",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSync_feature),(Name
"is-sync-feature",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_sync_feature),(Name
"sync-waiting-list",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepSync_waiting_list),(Name
"sync-held",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepSync_held),(Name
"sync-holder",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepSync_holder),(Name
"sync-count",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepSync_count),(Name
"sync-feature-maps",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepSync_feature_maps),(Name
"sync-feature-create",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSync_feature_create),(Name
"sync-waiting-list-add",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSync_waiting_list_add),(Name
"sync-waiting-list-head-remove",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSync_waiting_list_head_remove),(Name
"syncs",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepSyncs),(Name
"sync-features",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepSync_features)]

sync_ :: [Funcons] -> Funcons
sync_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"sync" ([Funcons]
fargs)
stepSync :: StrictFuncon
stepSync [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 [MetaVar -> VPattern
VPMetaVar MetaVar
"_X1"] forall {k} {a}. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"_X1") (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp)) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"datatype-value" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (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
115)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
121)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
110)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
99)])])),MetaVar -> FTerm
TVar MetaVar
"_X1"]) Env
env

sync_create_ :: [Funcons] -> Funcons
sync_create_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"sync-create" ([Funcons]
fargs)
stepSync_create :: StrictFuncon
stepSync_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 -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"M+" SeqSortOp
PlusOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"sync-feature-maps") SeqSortOp
PlusOp)] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"sync" [Name -> [FTerm] -> FTerm
TApp Name
"checked" [Name -> [FTerm] -> FTerm
TApp Name
"map-unite" [MetaVar -> FTerm
TVar MetaVar
"M+"]]]) Env
env

sync_feature_ :: [Funcons] -> Funcons
sync_feature_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"sync-feature" ([Funcons]
fargs)
stepSync_feature :: StrictFuncon
stepSync_feature [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 [Name -> [VPattern] -> VPattern
PADT Name
"sync" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SFM") (Name -> FTerm
TName Name
"sync-feature-maps")],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SF") (Name -> FTerm
TName Name
"sync-features")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"checked" [Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"SFM",MetaVar -> FTerm
TVar MetaVar
"SF"]]) Env
env

is_sync_feature_ :: [Funcons] -> Funcons
is_sync_feature_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-sync-feature" ([Funcons]
fargs)
stepIs_sync_feature :: StrictFuncon
stepIs_sync_feature [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 [Name -> [VPattern] -> VPattern
PADT Name
"sync" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SFM") (Name -> FTerm
TName Name
"sync-feature-maps")],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"SF") (Name -> FTerm
TName Name
"sync-features")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"SF",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"SFM"]]) Env
env

sync_waiting_list_ :: Funcons
sync_waiting_list_ = Name -> Funcons
FName Name
"sync-waiting-list"
stepSync_waiting_list :: NullaryFuncon
stepSync_waiting_list = [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
"datatype-value" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (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
115)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
121)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
110)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
99)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
45)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
119)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
97)]),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
116)]),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
110)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
103)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
45)]),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)])]))]) forall {k} {a}. Map k a
env

sync_held_ :: Funcons
sync_held_ = Name -> Funcons
FName Name
"sync-held"
stepSync_held :: NullaryFuncon
stepSync_held = [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
"datatype-value" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (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
115)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
121)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
110)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
99)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
45)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
104)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
101)]),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
100)])]))]) forall {k} {a}. Map k a
env

sync_holder_ :: Funcons
sync_holder_ = Name -> Funcons
FName Name
"sync-holder"
stepSync_holder :: NullaryFuncon
stepSync_holder = [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
"datatype-value" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (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
115)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
121)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
110)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
99)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
45)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
104)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
111)]),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
100)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
101)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
114)])]))]) forall {k} {a}. Map k a
env

sync_count_ :: Funcons
sync_count_ = Name -> Funcons
FName Name
"sync-count"
stepSync_count :: NullaryFuncon
stepSync_count = [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
"datatype-value" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (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
115)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
121)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
110)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
99)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
45)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
99)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
111)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
117)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
110)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
116)])]))]) forall {k} {a}. Map k a
env

sync_feature_maps_ :: Funcons
sync_feature_maps_ = Name -> Funcons
FName Name
"sync-feature-maps"
stepSync_feature_maps :: NullaryFuncon
stepSync_feature_maps = [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
"maps" [Name -> FTerm
TName Name
"sync-features",Name -> FTerm
TName Name
"values"]) forall {k} {a}. Map k a
env

sync_feature_create_ :: [Funcons] -> Funcons
sync_feature_create_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"sync-feature-create" ([Funcons]
fargs)
stepSync_feature_create :: StrictFuncon
stepSync_feature_create [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2,NullaryFuncon
rewrite3,NullaryFuncon
rewrite4] []
    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
"sync-waiting-list" []] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo ([FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (Name -> FTerm
TName Name
"sync-waiting-list") (Name -> [FTerm] -> FTerm
TApp Name
"allocate-initialised-variable" [Name -> [FTerm] -> FTerm
TApp Name
"lists" [Name -> FTerm
TName Name
"values"],Name -> [FTerm] -> FTerm
TApp Name
"list" []])]) 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
"sync-held" []] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo ([FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (Name -> FTerm
TName Name
"sync-held") (Name -> [FTerm] -> FTerm
TApp Name
"allocate-initialised-variable" [Name -> FTerm
TName Name
"booleans",Name -> FTerm
TName Name
"false"])]) Env
env
          rewrite3 :: NullaryFuncon
rewrite3 = 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
"sync-holder" []] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo ([FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (Name -> FTerm
TName Name
"sync-holder") (Name -> [FTerm] -> FTerm
TApp Name
"allocate-variable" [Name -> FTerm
TName Name
"thread-ids"])]) Env
env
          rewrite4 :: NullaryFuncon
rewrite4 = 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
"sync-count" []] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo ([FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (Name -> FTerm
TName Name
"sync-count") (Name -> [FTerm] -> FTerm
TApp Name
"allocate-initialised-variable" [Name -> FTerm
TName Name
"nats",Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (forall t. Integer -> Values t
Nat Integer
0))])]) Env
env

sync_waiting_list_add_ :: [Funcons] -> Funcons
sync_waiting_list_add_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"sync-waiting-list-add" ([Funcons]
fargs)
stepSync_waiting_list_add :: StrictFuncon
stepSync_waiting_list_add [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
"values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (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-append" [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
"list" [MetaVar -> FTerm
TVar MetaVar
"V"]]]) Env
env

sync_waiting_list_head_remove_ :: [Funcons] -> Funcons
sync_waiting_list_head_remove_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"sync-waiting-list-head-remove" ([Funcons]
fargs)
stepSync_waiting_list_head_remove :: StrictFuncon
stepSync_waiting_list_head_remove [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
"give" [Name -> [FTerm] -> FTerm
TApp Name
"checked" [Name -> [FTerm] -> FTerm
TApp Name
"list-head" [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
"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
"checked" [Name -> [FTerm] -> FTerm
TApp Name
"list-tail" [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
TName Name
"given"]]) Env
env

syncs_ :: Funcons
syncs_ = Name -> Funcons
FName Name
"syncs"
stepSyncs :: NullaryFuncon
stepSyncs = Name -> StrictFuncon
rewriteType Name
"syncs" []

sync_features_ :: Funcons
sync_features_ = Name -> Funcons
FName Name
"sync-features"
stepSync_features :: NullaryFuncon
stepSync_features = Name -> StrictFuncon
rewriteType Name
"sync-features" []