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

module Funcons.Core.Computations.Threads.Synchronising.Locks.Locks 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
"is-exclusive-lock-holder",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_exclusive_lock_holder),(Name
"spin-lock-create",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepSpin_lock_create),(Name
"spin-lock-sync",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSpin_lock_sync),(Name
"spin-lock-release",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSpin_lock_release),(Name
"exclusive-lock-create",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepExclusive_lock_create),(Name
"exclusive-lock-sync",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepExclusive_lock_sync),(Name
"exclusive-lock-sync-else-wait",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepExclusive_lock_sync_else_wait),(Name
"exclusive-lock-release",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepExclusive_lock_release),(Name
"reentrant-lock-create",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepReentrant_lock_create),(Name
"reentrant-lock-sync",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepReentrant_lock_sync),(Name
"reentrant-lock-sync-else-wait",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepReentrant_lock_sync_else_wait),(Name
"reentrant-lock-release",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepReentrant_lock_release),(Name
"reentrant-lock-exit",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepReentrant_lock_exit),(Name
"semaphore-create",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSemaphore_create),(Name
"semaphore-sync",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSemaphore_sync),(Name
"semaphore-sync-else-wait",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSemaphore_sync_else_wait),(Name
"semaphore-release",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSemaphore_release),(Name
"rw-lock-create",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepRw_lock_create),(Name
"rw-lock-sync-exclusive",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRw_lock_sync_exclusive),(Name
"rw-lock-sync-shared",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRw_lock_sync_shared),(Name
"rw-lock-sync-exclusive-else-wait",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRw_lock_sync_exclusive_else_wait),(Name
"rw-lock-sync-shared-else-wait",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRw_lock_sync_shared_else_wait),(Name
"rw-lock-release-exclusive",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRw_lock_release_exclusive),(Name
"rw-lock-release-shared",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRw_lock_release_shared),(Name
"rw-lock-sync",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRw_lock_sync),(Name
"rw-lock-sync-all-shared",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepRw_lock_sync_all_shared)]

is_exclusive_lock_holder_ :: [Funcons] -> Funcons
is_exclusive_lock_holder_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-exclusive-lock-holder" ([Funcons]
fargs)
stepIs_exclusive_lock_holder :: StrictFuncon
stepIs_exclusive_lock_holder [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
"is-equal" [Name -> FTerm
TName Name
"current-thread",Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-holder"]]]) Env
env

spin_lock_create_ :: Funcons
spin_lock_create_ = Name -> Funcons
FName Name
"spin-lock-create"
stepSpin_lock_create :: NullaryFuncon
stepSpin_lock_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-held"],Name -> [FTerm] -> FTerm
TApp Name
"sync-feature-create" [Name -> FTerm
TName Name
"sync-holder"]]) forall {k} {a}. Map k a
env

spin_lock_sync_ :: [Funcons] -> Funcons
spin_lock_sync_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"spin-lock-sync" ([Funcons]
fargs)
stepSpin_lock_sync :: StrictFuncon
stepSpin_lock_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
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"]]]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"],Name -> FTerm
TName Name
"true"],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-holder"],Name -> FTerm
TName Name
"current-thread"]]]) Env
env

spin_lock_release_ :: [Funcons] -> Funcons
spin_lock_release_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"spin-lock-release" ([Funcons]
fargs)
stepSpin_lock_release :: StrictFuncon
stepSpin_lock_release [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
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-exclusive-lock-holder" [MetaVar -> FTerm
TVar MetaVar
"SY"]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"],Name -> FTerm
TName Name
"false"],Name -> [FTerm] -> FTerm
TApp Name
"un-assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-holder"]]]]) Env
env

exclusive_lock_create_ :: Funcons
exclusive_lock_create_ = Name -> Funcons
FName Name
"exclusive-lock-create"
stepExclusive_lock_create :: NullaryFuncon
stepExclusive_lock_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"],Name -> [FTerm] -> FTerm
TApp Name
"sync-feature-create" [Name -> FTerm
TName Name
"sync-held"],Name -> [FTerm] -> FTerm
TApp Name
"sync-feature-create" [Name -> FTerm
TName Name
"sync-holder"]]) forall {k} {a}. Map k a
env

exclusive_lock_sync_ :: [Funcons] -> Funcons
exclusive_lock_sync_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"exclusive-lock-sync" ([Funcons]
fargs)
stepExclusive_lock_sync :: StrictFuncon
stepExclusive_lock_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
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"]]]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"],Name -> FTerm
TName Name
"true"],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-holder"],Name -> FTerm
TName Name
"current-thread"]]]) Env
env

exclusive_lock_sync_else_wait_ :: [Funcons] -> Funcons
exclusive_lock_sync_else_wait_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"exclusive-lock-sync-else-wait" ([Funcons]
fargs)
stepExclusive_lock_sync_else_wait :: StrictFuncon
stepExclusive_lock_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
"exclusive-lock-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
"thread-suspend" [Name -> FTerm
TName Name
"current-thread"]]]]) Env
env

exclusive_lock_release_ :: [Funcons] -> Funcons
exclusive_lock_release_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"exclusive-lock-release" ([Funcons]
fargs)
stepExclusive_lock_release :: StrictFuncon
stepExclusive_lock_release [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
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-exclusive-lock-holder" [MetaVar -> FTerm
TVar MetaVar
"SY"]],Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [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" []],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-held"],Name -> FTerm
TName Name
"false"],Name -> [FTerm] -> FTerm
TApp Name
"un-assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-holder"]]],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
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-holder"],Name -> FTerm
TName Name
"given"],Name -> [FTerm] -> FTerm
TApp Name
"thread-resume" [Name -> FTerm
TName Name
"given"]]]]]]) Env
env

reentrant_lock_create_ :: Funcons
reentrant_lock_create_ = Name -> Funcons
FName Name
"reentrant-lock-create"
stepReentrant_lock_create :: NullaryFuncon
stepReentrant_lock_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"],Name -> [FTerm] -> FTerm
TApp Name
"sync-feature-create" [Name -> FTerm
TName Name
"sync-held"],Name -> [FTerm] -> FTerm
TApp Name
"sync-feature-create" [Name -> FTerm
TName Name
"sync-holder"],Name -> [FTerm] -> FTerm
TApp Name
"sync-feature-create" [Name -> FTerm
TName Name
"sync-count"]]) forall {k} {a}. Map k a
env

reentrant_lock_sync_ :: [Funcons] -> Funcons
reentrant_lock_sync_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"reentrant-lock-sync" ([Funcons]
fargs)
stepReentrant_lock_sync :: StrictFuncon
stepReentrant_lock_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
"else" [Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"]]]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"],Name -> FTerm
TName Name
"true"],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-holder"],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"],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
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"]]],Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-exclusive-lock-holder" [MetaVar -> FTerm
TVar MetaVar
"SY"]],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
"nat-succ" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-count"]]]]]]]) Env
env

reentrant_lock_sync_else_wait_ :: [Funcons] -> Funcons
reentrant_lock_sync_else_wait_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"reentrant-lock-sync-else-wait" ([Funcons]
fargs)
stepReentrant_lock_sync_else_wait :: StrictFuncon
stepReentrant_lock_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
"reentrant-lock-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
"thread-suspend" [Name -> FTerm
TName Name
"current-thread"]]]]) Env
env

reentrant_lock_release_ :: [Funcons] -> Funcons
reentrant_lock_release_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"reentrant-lock-release" ([Funcons]
fargs)
stepReentrant_lock_release :: StrictFuncon
stepReentrant_lock_release [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
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-exclusive-lock-holder" [MetaVar -> FTerm
TVar MetaVar
"SY"]],Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [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" []],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-held"],Name -> FTerm
TName Name
"false"],Name -> [FTerm] -> FTerm
TApp Name
"un-assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-holder"]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-count"],Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (forall t. Integer -> Values t
Nat Integer
0))]],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
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-holder"],Name -> FTerm
TName Name
"given"],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-count"],Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (forall t. Integer -> Values t
Nat Integer
0))],Name -> [FTerm] -> FTerm
TApp Name
"thread-resume" [Name -> FTerm
TName Name
"given"]]]]]]) Env
env

reentrant_lock_exit_ :: [Funcons] -> Funcons
reentrant_lock_exit_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"reentrant-lock-exit" ([Funcons]
fargs)
stepReentrant_lock_exit :: StrictFuncon
stepReentrant_lock_exit [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
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-exclusive-lock-holder" [MetaVar -> FTerm
TVar MetaVar
"SY"]],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
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-greater" [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
"assign" [Name -> FTerm
TName Name
"given",Name -> [FTerm] -> FTerm
TApp Name
"checked" [Name -> [FTerm] -> FTerm
TApp Name
"nat-pred" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> FTerm
TName Name
"given"]]]],Name -> [FTerm] -> FTerm
TApp Name
"reentrant-lock-release" [MetaVar -> FTerm
TVar MetaVar
"SY"]]]]]) Env
env

semaphore_create_ :: [Funcons] -> Funcons
semaphore_create_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"semaphore-create" ([Funcons]
fargs)
stepSemaphore_create :: StrictFuncon
stepSemaphore_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

semaphore_sync_ :: [Funcons] -> Funcons
semaphore_sync_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"semaphore-sync" ([Funcons]
fargs)
stepSemaphore_sync :: StrictFuncon
stepSemaphore_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
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-greater" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-count"]],Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (forall t. Integer -> Values t
Nat Integer
0))]],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"]]]]]]]) Env
env

semaphore_sync_else_wait_ :: [Funcons] -> Funcons
semaphore_sync_else_wait_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"semaphore-sync-else-wait" ([Funcons]
fargs)
stepSemaphore_sync_else_wait :: StrictFuncon
stepSemaphore_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
"semaphore-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
"thread-suspend" [Name -> FTerm
TName Name
"current-thread"]]]]) Env
env

semaphore_release_ :: [Funcons] -> Funcons
semaphore_release_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"semaphore-release" ([Funcons]
fargs)
stepSemaphore_release :: StrictFuncon
stepSemaphore_release [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
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [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" []],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
"nat-succ" [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
"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

rw_lock_create_ :: Funcons
rw_lock_create_ = Name -> Funcons
FName Name
"rw-lock-create"
stepRw_lock_create :: NullaryFuncon
stepRw_lock_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
"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-held"],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"],Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (forall t. Integer -> Values t
Nat Integer
0))],Name -> FTerm
TName Name
"given"]]) forall {k} {a}. Map k a
env

rw_lock_sync_exclusive_ :: [Funcons] -> Funcons
rw_lock_sync_exclusive_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rw-lock-sync-exclusive" ([Funcons]
fargs)
stepRw_lock_sync_exclusive :: StrictFuncon
stepRw_lock_sync_exclusive [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
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"and" [Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"]]],Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-count"]],Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (forall t. Integer -> Values t
Nat Integer
0))]]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"],Name -> FTerm
TName Name
"true"]]]) Env
env

rw_lock_sync_shared_ :: [Funcons] -> Funcons
rw_lock_sync_shared_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rw-lock-sync-shared" ([Funcons]
fargs)
stepRw_lock_sync_shared :: StrictFuncon
stepRw_lock_sync_shared [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
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"]]]],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
"nat-succ" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-count"]]]]]]) Env
env

rw_lock_sync_exclusive_else_wait_ :: [Funcons] -> Funcons
rw_lock_sync_exclusive_else_wait_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rw-lock-sync-exclusive-else-wait" ([Funcons]
fargs)
stepRw_lock_sync_exclusive_else_wait :: StrictFuncon
stepRw_lock_sync_exclusive_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
"rw-lock-sync-exclusive" [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] -> FTerm
TApp Name
"tuple" [Name -> FTerm
TName Name
"current-thread",Name -> FTerm
TName Name
"false"]],Name -> [FTerm] -> FTerm
TApp Name
"thread-suspend" [Name -> FTerm
TName Name
"current-thread"]]]]) Env
env

rw_lock_sync_shared_else_wait_ :: [Funcons] -> Funcons
rw_lock_sync_shared_else_wait_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rw-lock-sync-shared-else-wait" ([Funcons]
fargs)
stepRw_lock_sync_shared_else_wait :: StrictFuncon
stepRw_lock_sync_shared_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
"rw-lock-sync-shared" [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] -> FTerm
TApp Name
"tuple" [Name -> FTerm
TName Name
"current-thread",Name -> FTerm
TName Name
"true"]],Name -> [FTerm] -> FTerm
TApp Name
"thread-suspend" [Name -> FTerm
TName Name
"current-thread"]]]]) Env
env

rw_lock_release_exclusive_ :: [Funcons] -> Funcons
rw_lock_release_exclusive_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rw-lock-release-exclusive" ([Funcons]
fargs)
stepRw_lock_release_exclusive :: StrictFuncon
stepRw_lock_release_exclusive [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
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"assigned" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"]]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"],Name -> FTerm
TName Name
"false"],Name -> [FTerm] -> FTerm
TApp Name
"rw-lock-sync" [MetaVar -> FTerm
TVar MetaVar
"SY"]]]) Env
env

rw_lock_release_shared_ :: [Funcons] -> Funcons
rw_lock_release_shared_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rw-lock-release-shared" ([Funcons]
fargs)
stepRw_lock_release_shared :: StrictFuncon
stepRw_lock_release_shared [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
"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
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (forall t. Integer -> Values t
Nat Integer
0)),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
"rw-lock-sync" [MetaVar -> FTerm
TVar MetaVar
"SY"],Name -> FTerm
TName Name
"null-value"]]]) Env
env

rw_lock_sync_ :: [Funcons] -> Funcons
rw_lock_sync_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rw-lock-sync" ([Funcons]
fargs)
stepRw_lock_sync :: StrictFuncon
stepRw_lock_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
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [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" []],Name -> FTerm
TName Name
"null-value",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
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"thread-resume" [Name -> [FTerm] -> FTerm
TApp Name
"first" [Name -> [FTerm] -> FTerm
TApp Name
"tuple-elements" [Name -> FTerm
TName Name
"given"]]],Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"second" [Name -> [FTerm] -> FTerm
TApp Name
"tuple-elements" [Name -> FTerm
TName Name
"given"]],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-count"],Name -> [FTerm] -> FTerm
TApp Name
"nat-succ" [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
"rw-lock-sync-all-shared" [MetaVar -> FTerm
TVar MetaVar
"SY"]],Name -> [FTerm] -> FTerm
TApp Name
"assign" [Name -> [FTerm] -> FTerm
TApp Name
"sync-feature" [MetaVar -> FTerm
TVar MetaVar
"SY",Name -> FTerm
TName Name
"sync-held"],Name -> FTerm
TName Name
"true"]]]]]) Env
env

rw_lock_sync_all_shared_ :: [Funcons] -> Funcons
rw_lock_sync_all_shared_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"rw-lock-sync-all-shared" ([Funcons]
fargs)
stepRw_lock_sync_all_shared :: StrictFuncon
stepRw_lock_sync_all_shared [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
"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" [Name -> [FTerm] -> FTerm
TApp Name
"left-to-right-filter" [Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"second" [Name -> [FTerm] -> FTerm
TApp Name
"tuple-elements" [Name -> FTerm
TName Name
"given"]],Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"thread-resume" [Name -> [FTerm] -> FTerm
TApp Name
"first" [Name -> [FTerm] -> FTerm
TApp Name
"tuple-elements" [Name -> FTerm
TName Name
"given"]]],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
"nat-succ" [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
TName Name
"false"],Name -> FTerm
TName Name
"true"],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"]]]]]]) Env
env