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

module Funcons.Core.Computations.Threads.Multithreading.Multithreading where

import Funcons.EDSL

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

types :: TypeRelation
types = [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList
    [(Name
"thread-ids",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"thread-ids" [] [Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"thread-id" [Name -> FTerm
TName Name
"atoms"] (forall a. a -> Maybe a
Just [])]),(Name
"threads",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"threads" [] [Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"thread" [Name -> [FTerm] -> FTerm
TApp Name
"thunks" [Name -> FTerm
TName Name
"values"],FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> [FTerm] -> FTerm
TApp Name
"lists" [Name -> FTerm
TName Name
"thread-ids"]) SeqSortOp
QuestionMarkOp] (forall a. a -> Maybe a
Just [])]),(Name
"thread-preemtibilities",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"thread-preemtibilities" [] [Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"thread-preemptible" [] (forall a. a -> Maybe a
Just []),Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"thread-cooperative" [] (forall a. a -> Maybe a
Just [])])]

funcons :: FunconLibrary
funcons = [(Name, EvalFunction)] -> FunconLibrary
libFromList
    [(Name
"thread-id",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_id),(Name
"thread",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread),(Name
"thread-joinable",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_joinable),(Name
"thread-detached",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_detached),(Name
"is-some-thread-active",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepIs_some_thread_active),(Name
"is-some-thread-suspended",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepIs_some_thread_suspended),(Name
"initialise-multithreading",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepInitialise_multithreading),(Name
"initialise-thread-map",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepInitialise_thread_map),(Name
"initialise-active-thread-set",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepInitialise_active_thread_set),(Name
"initialise-thread-stepping",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepInitialise_thread_stepping),(Name
"initialise-terminated-thread-map",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepInitialise_terminated_thread_map),(Name
"initialise-thread-schedule",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepInitialise_thread_schedule),(Name
"multithread",NonStrictFuncon -> EvalFunction
NonStrictFuncon NonStrictFuncon
stepMultithread),(Name
"thread-activate",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_activate),(Name
"thread-detach",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_detach),(Name
"current-thread",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepCurrent_thread),(Name
"thread-step",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepThread_step),(Name
"thread-atomic",NonStrictFuncon -> EvalFunction
NonStrictFuncon NonStrictFuncon
stepThread_atomic),(Name
"thread-yield",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_yield),(Name
"thread-spin",NonStrictFuncon -> EvalFunction
NonStrictFuncon NonStrictFuncon
stepThread_spin),(Name
"thread-suspend",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_suspend),(Name
"thread-resume",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_resume),(Name
"thread-terminate",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_terminate),(Name
"is-thread-terminated",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_thread_terminated),(Name
"thread-value",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_value),(Name
"thread-join",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_join),(Name
"thread-exterminate",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThread_exterminate),(Name
"update-thread-stepping",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepUpdate_thread_stepping),(Name
"update-thread-schedule",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepUpdate_thread_schedule),(Name
"current-thread-schedule",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepCurrent_thread_schedule),(Name
"thread-preemptible",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepThread_preemptible),(Name
"thread-cooperative",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepThread_cooperative),(Name
"is-thread-preemptible",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_thread_preemptible),(Name
"thread-ids",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepThread_ids),(Name
"threads",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepThreads),(Name
"thread-preemtibilities",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepThread_preemtibilities)]

thread_id_ :: [Funcons] -> Funcons
thread_id_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-id" ([Funcons]
fargs)
stepThread_id :: StrictFuncon
stepThread_id [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
116)]),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
114)]),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
97)]),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
45)]),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
100)])])),MetaVar -> FTerm
TVar MetaVar
"_X1"]) Env
env

thread_ :: [Funcons] -> Funcons
thread_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread" ([Funcons]
fargs)
stepThread :: StrictFuncon
stepThread [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",MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"_X2?" SeqSortOp
QuestionMarkOp] 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
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"_X2?") (FTerm -> SeqSortOp -> FTerm
TSortSeq (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp) 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
116)]),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
114)]),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
97)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
100)])])),MetaVar -> FTerm
TVar MetaVar
"_X1",MetaVar -> FTerm
TVar MetaVar
"_X2?"]) Env
env

thread_joinable_ :: [Funcons] -> Funcons
thread_joinable_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-joinable" ([Funcons]
fargs)
stepThread_joinable :: StrictFuncon
stepThread_joinable [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
"TH") (Name -> [FTerm] -> FTerm
TApp Name
"thunks" [Name -> FTerm
TName Name
"values"])] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"thread" [MetaVar -> FTerm
TVar MetaVar
"TH",Name -> [FTerm] -> FTerm
TApp Name
"list" []]) Env
env

thread_detached_ :: [Funcons] -> Funcons
thread_detached_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-detached" ([Funcons]
fargs)
stepThread_detached :: StrictFuncon
stepThread_detached [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
"TH") (Name -> [FTerm] -> FTerm
TApp Name
"thunks" [Name -> FTerm
TName Name
"values"])] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"thread" [MetaVar -> FTerm
TVar MetaVar
"TH"]) Env
env

is_some_thread_active_ :: Funcons
is_some_thread_active_ = Name -> Funcons
FName Name
"is-some-thread-active"
stepIs_some_thread_active :: NullaryFuncon
stepIs_some_thread_active = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] forall {k} {a}. Map k a
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"ATS",[FTerm] -> FTerm
TSet []]]) Env
env

is_some_thread_suspended_ :: Funcons
is_some_thread_suspended_ = Name -> Funcons
FName Name
"is-some-thread-suspended"
stepIs_some_thread_suspended :: NullaryFuncon
stepIs_some_thread_suspended = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"ATS",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"TM"]]]) Env
env

initialise_multithreading_ :: Funcons
initialise_multithreading_ = Name -> Funcons
FName Name
"initialise-multithreading"
stepInitialise_multithreading :: NullaryFuncon
stepInitialise_multithreading = [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
"sequential" [Name -> FTerm
TName Name
"initialise-thread-map",Name -> FTerm
TName Name
"initialise-active-thread-set",Name -> FTerm
TName Name
"initialise-thread-stepping",Name -> FTerm
TName Name
"initialise-terminated-thread-map",Name -> FTerm
TName Name
"initialise-thread-schedule"]) forall {k} {a}. Map k a
env

initialise_thread_map_ :: Funcons
initialise_thread_map_ = Name -> Funcons
FName Name
"initialise-thread-map"
stepInitialise_thread_map :: NullaryFuncon
stepInitialise_thread_map = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-map" (Name -> [FTerm] -> FTerm
TApp Name
"map" []) forall {k} {a}. Map k a
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") forall {k} {a}. Map k a
env

initialise_active_thread_set_ :: Funcons
initialise_active_thread_set_ = Name -> Funcons
FName Name
"initialise-active-thread-set"
stepInitialise_active_thread_set :: NullaryFuncon
stepInitialise_active_thread_set = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" ([FTerm] -> FTerm
TSet []) forall {k} {a}. Map k a
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") forall {k} {a}. Map k a
env

initialise_thread_stepping_ :: Funcons
initialise_thread_stepping_ = Name -> Funcons
FName Name
"initialise-thread-stepping"
stepInitialise_thread_stepping :: NullaryFuncon
stepInitialise_thread_stepping = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" ([FTerm] -> FTerm
TSeq []) forall {k} {a}. Map k a
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") forall {k} {a}. Map k a
env

initialise_terminated_thread_map_ :: Funcons
initialise_terminated_thread_map_ = Name -> Funcons
FName Name
"initialise-terminated-thread-map"
stepInitialise_terminated_thread_map :: NullaryFuncon
stepInitialise_terminated_thread_map = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"terminated-thread-map" (Name -> [FTerm] -> FTerm
TApp Name
"map" []) forall {k} {a}. Map k a
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") forall {k} {a}. Map k a
env

initialise_thread_schedule_ :: Funcons
initialise_thread_schedule_ = Name -> Funcons
FName Name
"initialise-thread-schedule"
stepInitialise_thread_schedule :: NullaryFuncon
stepInitialise_thread_schedule = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-schedule" ([FTerm] -> FTerm
TSet []) forall {k} {a}. Map k a
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") forall {k} {a}. Map k a
env

multithread_ :: [Funcons] -> Funcons
multithread_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"multithread" ([Funcons]
fargs)
stepMultithread :: NonStrictFuncon
stepMultithread [Funcons]
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 <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"X"] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> FTerm
TName Name
"initialise-multithreading",Name -> [FTerm] -> FTerm
TApp Name
"give" [Name -> [FTerm] -> FTerm
TApp Name
"thread-activate" [Name -> [FTerm] -> FTerm
TApp Name
"thread-joinable" [Name -> [FTerm] -> FTerm
TApp Name
"thunk" [Name -> [FTerm] -> FTerm
TApp Name
"closure" [MetaVar -> FTerm
TVar MetaVar
"X"]]]],Name -> [FTerm] -> FTerm
TApp Name
"handle-abrupt" [Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"while-true" [Name -> FTerm
TName Name
"is-some-thread-active",Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> FTerm
TName Name
"update-thread-stepping",Name -> FTerm
TName Name
"thread-step"]],Name -> [FTerm] -> FTerm
TApp Name
"check" [Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> FTerm
TName Name
"is-some-thread-suspended"]],Name -> [FTerm] -> FTerm
TApp Name
"thread-value" [Name -> FTerm
TName Name
"given"]],Name -> FTerm
TName Name
"given"]]]) Env
env

thread_activate_ :: [Funcons] -> Funcons
thread_activate_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-activate" ([Funcons]
fargs)
stepThread_activate :: StrictFuncon
stepThread_activate [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"THR") (Name -> FTerm
TName Name
"threads")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- FTerm -> [FPattern] -> Env -> MSOS Env
premise (Name -> [FTerm] -> FTerm
TApp Name
"thread-id" [Name -> FTerm
TName Name
"fresh-atom"]) [MetaVar -> FPattern
PMetaVar MetaVar
"TI"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-unite" [[FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"TI") (MetaVar -> FTerm
TVar MetaVar
"THR")],MetaVar -> FTerm
TVar MetaVar
"TM"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TM'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"set-unite" [[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI"],MetaVar -> FTerm
TVar MetaVar
"ATS"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-map" (MetaVar -> FTerm
TVar MetaVar
"TM'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (MetaVar -> FTerm
TVar MetaVar
"TI") Env
env

thread_detach_ :: [Funcons] -> Funcons
thread_detach_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-detach" ([Funcons]
fargs)
stepThread_detach :: StrictFuncon
stepThread_detach [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1,MSOS StepRes
step2]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"TM",MetaVar -> FTerm
TVar MetaVar
"TI"]) [Name -> [VPattern] -> VPattern
PADT Name
"thread" [MetaVar -> VPattern
VPMetaVar MetaVar
"TH",VPattern
VPWildCard]]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-override" [[FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"TI") (Name -> [FTerm] -> FTerm
TApp Name
"thread" [MetaVar -> FTerm
TVar MetaVar
"TH"])],MetaVar -> FTerm
TVar MetaVar
"TM"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TM'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-map" (MetaVar -> FTerm
TVar MetaVar
"TM'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step2 :: MSOS StepRes
step2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"terminated-thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TMV"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"TI",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"TMV"]]) (Name -> FTerm
TName Name
"true")) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"TMV",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TMV'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"terminated-thread-map" (MetaVar -> FTerm
TVar MetaVar
"TMV'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env

current_thread_ :: Funcons
current_thread_ = Name -> Funcons
FName Name
"current-thread"
stepCurrent_thread :: NullaryFuncon
stepCurrent_thread = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1,MSOS StepRes
step2]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] forall {k} {a}. Map k a
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (MetaVar -> FTerm
TVar MetaVar
"TI") Env
env
          step2 :: MSOS StepRes
step2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [] forall {k} {a}. Map k a
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"fail") Env
env

thread_step_ :: Funcons
thread_step_ = Name -> Funcons
FName Name
"thread-step"
stepThread_step :: NullaryFuncon
stepThread_step = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1,MSOS StepRes
step2,MSOS StepRes
step3]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"TM",MetaVar -> FTerm
TVar MetaVar
"TI"]) [Name -> [VPattern] -> VPattern
PADT Name
"thread" [Name -> [VPattern] -> VPattern
PADT Name
"thunk" [Name -> [VPattern] -> VPattern
PADT Name
"abstraction" [MetaVar -> VPattern
VPMetaVar MetaVar
"X"]],MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"L?" SeqSortOp
QuestionMarkOp]]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-map" (MetaVar -> FTerm
TVar MetaVar
"TM") Env
env
            Env
env <- FTerm -> [FPattern] -> Env -> MSOS Env
premise (MetaVar -> FTerm
TVar MetaVar
"X") [MetaVar -> FPattern
PMetaVar MetaVar
"X'"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI?" SeqSortOp
QuestionMarkOp] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM'"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"TI",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"TM'"]],Name -> [FTerm] -> FTerm
TApp Name
"map-override" [[FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"TI") (Name -> [FTerm] -> FTerm
TApp Name
"thread" [Name -> [FTerm] -> FTerm
TApp Name
"thunk" [Name -> [FTerm] -> FTerm
TApp Name
"abstraction" [MetaVar -> FTerm
TVar MetaVar
"X'"]],MetaVar -> FTerm
TVar MetaVar
"L?"])],MetaVar -> FTerm
TVar MetaVar
"TM'"],MetaVar -> FTerm
TVar MetaVar
"TM'"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TM''"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI?") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-map" (MetaVar -> FTerm
TVar MetaVar
"TM''") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step2 :: MSOS StepRes
step2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"TM",MetaVar -> FTerm
TVar MetaVar
"TI"]) [Name -> [VPattern] -> VPattern
PADT Name
"thread" [Name -> [VPattern] -> VPattern
PADT Name
"thunk" [Name -> [VPattern] -> VPattern
PADT Name
"abstraction" [MetaVar -> VPattern
VPMetaVar MetaVar
"X"]]]]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (MetaVar -> FTerm
TVar MetaVar
"X") [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"TM",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TM'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"set-difference" [MetaVar -> FTerm
TVar MetaVar
"ATS",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" ([FTerm] -> FTerm
TSeq []) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-map" (MetaVar -> FTerm
TVar MetaVar
"TM'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step3 :: MSOS StepRes
step3 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"terminated-thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TVM"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"TM",MetaVar -> FTerm
TVar MetaVar
"TI"]) [Name -> [VPattern] -> VPattern
PADT Name
"thread" [Name -> [VPattern] -> VPattern
PADT Name
"thunk" [Name -> [VPattern] -> VPattern
PADT Name
"abstraction" [MetaVar -> VPattern
VPMetaVar MetaVar
"X"]],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)])]),MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI*" SeqSortOp
StarOp]]]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (MetaVar -> FTerm
TVar MetaVar
"X") [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"TM",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TM'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"set-unite" [Name -> [FTerm] -> FTerm
TApp Name
"set-difference" [MetaVar -> FTerm
TVar MetaVar
"ATS",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI"]],[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI*"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-unite" [MetaVar -> FTerm
TVar MetaVar
"TVM",[FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"TI") (MetaVar -> FTerm
TVar MetaVar
"V")]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TVM'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" ([FTerm] -> FTerm
TSeq []) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-map" (MetaVar -> FTerm
TVar MetaVar
"TM'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"terminated-thread-map" (MetaVar -> FTerm
TVar MetaVar
"TVM'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env

thread_atomic_ :: [Funcons] -> Funcons
thread_atomic_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-atomic" ([Funcons]
fargs)
stepThread_atomic :: NonStrictFuncon
stepThread_atomic [Funcons]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1,MSOS StepRes
step2,MSOS StepRes
step3,MSOS StepRes
step4,MSOS StepRes
step5,MSOS StepRes
step6]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> MSOS Env
lifted_fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"X"] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"store" [MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] Env
env
            Env
env <- Name -> Maybe VPattern -> Env -> MSOS Env
getControlPatt Name
"abrupted" (forall a. Maybe a
Nothing) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI") Env
env
            (Env
env,[Maybe Values
__varabrupted]) <- forall a. [Name] -> MSOS a -> MSOS (a, [Maybe Values])
receiveSignals [Name
"abrupted"] (forall a. Name -> Maybe FTerm -> Env -> MSOS a -> MSOS a
withControlTerm Name
"abrupted" (forall a. Maybe a
Nothing) Env
env (FTerm -> [FPattern] -> Env -> MSOS Env
premise (MetaVar -> FTerm
TVar MetaVar
"X") [MetaVar -> FPattern
PMetaVar MetaVar
"X'"] Env
env))
            Env
env <- Maybe Values -> Maybe VPattern -> Env -> MSOS Env
receiveSignalPatt Maybe Values
__varabrupted (forall a. Maybe a
Nothing) Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"store" [MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma'"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI'"] Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI'") Env
env
            (Env
env,[Maybe Values
__varabrupted]) <- forall a. [Name] -> MSOS a -> MSOS (a, [Maybe Values])
receiveSignals [Name
"abrupted"] (forall a. Name -> Maybe FTerm -> Env -> MSOS a -> MSOS a
withControlTerm Name
"abrupted" (forall a. Maybe a
Nothing) Env
env (FTerm -> [FPattern] -> Env -> MSOS Env
premise (Name -> [FTerm] -> FTerm
TApp Name
"thread-atomic" [MetaVar -> FTerm
TVar MetaVar
"X'"]) [MetaVar -> FPattern
PMetaVar MetaVar
"V"] Env
env))
            Env
env <- Maybe Values -> Maybe VPattern -> Env -> MSOS Env
receiveSignalPatt Maybe Values
__varabrupted (forall a. Maybe a
Nothing) Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"store" [MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma''"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS''"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI''?" SeqSortOp
QuestionMarkOp] Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma''") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS''") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI''?") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env
          step2 :: MSOS StepRes
step2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> MSOS Env
lifted_fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"X"] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"store" [MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] Env
env
            Env
env <- Name -> Maybe VPattern -> Env -> MSOS Env
getControlPatt Name
"abrupted" (forall a. a -> Maybe a
Just (MetaVar -> VPattern
VPMetaVar MetaVar
"A")) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI") Env
env
            (Env
env,[Maybe Values
__varabrupted]) <- forall a. [Name] -> MSOS a -> MSOS (a, [Maybe Values])
receiveSignals [Name
"abrupted"] (forall a. Name -> Maybe FTerm -> Env -> MSOS a -> MSOS a
withControlTerm Name
"abrupted" (forall a. Maybe a
Nothing) Env
env (FTerm -> [FPattern] -> Env -> MSOS Env
premise (MetaVar -> FTerm
TVar MetaVar
"X") [MetaVar -> FPattern
PMetaVar MetaVar
"X'"] Env
env))
            Env
env <- Maybe Values -> Maybe VPattern -> Env -> MSOS Env
receiveSignalPatt Maybe Values
__varabrupted (forall a. Maybe a
Nothing) Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"store" [MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma'"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI'"] Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI'") Env
env
            (Env
env,[Maybe Values
__varabrupted]) <- forall a. [Name] -> MSOS a -> MSOS (a, [Maybe Values])
receiveSignals [Name
"abrupted"] (forall a. Name -> Maybe FTerm -> Env -> MSOS a -> MSOS a
withControlTerm Name
"abrupted" (forall a. a -> Maybe a
Just (MetaVar -> FTerm
TVar MetaVar
"A")) Env
env (FTerm -> [FPattern] -> Env -> MSOS Env
premise (Name -> [FTerm] -> FTerm
TApp Name
"thread-atomic" [MetaVar -> FTerm
TVar MetaVar
"X'"]) [MetaVar -> FPattern
PMetaVar MetaVar
"V"] Env
env))
            Env
env <- Maybe Values -> Maybe VPattern -> Env -> MSOS Env
receiveSignalPatt Maybe Values
__varabrupted (forall a. a -> Maybe a
Just (MetaVar -> VPattern
VPMetaVar MetaVar
"A")) Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"store" [MetaVar -> VPattern
VPMetaVar MetaVar
"Sigma''"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS''"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI''?" SeqSortOp
QuestionMarkOp] Env
env
            Name -> FTerm -> Env -> MSOS ()
raiseTerm Name
"abrupted" (MetaVar -> FTerm
TVar MetaVar
"A") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"store" (MetaVar -> FTerm
TVar MetaVar
"Sigma''") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS''") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI''?") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env
          step3 :: MSOS StepRes
step3 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> MSOS Env
lifted_fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"X"] forall {k} {a}. Map k a
env
            Env
env <- Name -> Maybe VPattern -> Env -> MSOS Env
getControlPatt Name
"abrupted" (forall a. a -> Maybe a
Just (MetaVar -> VPattern
VPMetaVar MetaVar
"A")) Env
env
            (Env
env,[Maybe Values
__varabrupted]) <- forall a. [Name] -> MSOS a -> MSOS (a, [Maybe Values])
receiveSignals [Name
"abrupted"] (forall a. Name -> Maybe FTerm -> Env -> MSOS a -> MSOS a
withControlTerm Name
"abrupted" (forall a. a -> Maybe a
Just (MetaVar -> FTerm
TVar MetaVar
"A")) Env
env (FTerm -> [FPattern] -> Env -> MSOS Env
premise (MetaVar -> FTerm
TVar MetaVar
"X") [MetaVar -> FPattern
PMetaVar MetaVar
"X'"] Env
env))
            Env
env <- Maybe Values -> Maybe VPattern -> Env -> MSOS Env
receiveSignalPatt Maybe Values
__varabrupted (forall a. a -> Maybe a
Just (MetaVar -> VPattern
VPMetaVar MetaVar
"A")) Env
env
            Name -> FTerm -> Env -> MSOS ()
raiseTerm Name
"abrupted" (MetaVar -> FTerm
TVar MetaVar
"A") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> [FTerm] -> FTerm
TApp Name
"thread-atomic" [MetaVar -> FTerm
TVar MetaVar
"X'"]) Env
env
          step4 :: MSOS StepRes
step4 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> MSOS Env
lifted_fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"X"] forall {k} {a}. Map k a
env
            Env
env <- Name -> Maybe VPattern -> Env -> MSOS Env
getControlPatt Name
"abrupted" (forall a. Maybe a
Nothing) Env
env
            (Env
env,[Maybe Values
__varabrupted]) <- forall a. [Name] -> MSOS a -> MSOS (a, [Maybe Values])
receiveSignals [Name
"abrupted"] (forall a. Name -> Maybe FTerm -> Env -> MSOS a -> MSOS a
withControlTerm Name
"abrupted" (forall a. Maybe a
Nothing) Env
env (FTerm -> [FPattern] -> Env -> MSOS Env
premise (MetaVar -> FTerm
TVar MetaVar
"X") [FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] Env
env))
            Env
env <- Maybe Values -> Maybe VPattern -> Env -> MSOS Env
receiveSignalPatt Maybe Values
__varabrupted (forall a. Maybe a
Nothing) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env
          step5 :: MSOS StepRes
step5 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> MSOS Env
lifted_fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"X"] forall {k} {a}. Map k a
env
            Env
env <- Name -> Maybe VPattern -> Env -> MSOS Env
getControlPatt Name
"abrupted" (forall a. a -> Maybe a
Just (MetaVar -> VPattern
VPMetaVar MetaVar
"A")) Env
env
            (Env
env,[Maybe Values
__varabrupted]) <- forall a. [Name] -> MSOS a -> MSOS (a, [Maybe Values])
receiveSignals [Name
"abrupted"] (forall a. Name -> Maybe FTerm -> Env -> MSOS a -> MSOS a
withControlTerm Name
"abrupted" (forall a. a -> Maybe a
Just (MetaVar -> FTerm
TVar MetaVar
"A")) Env
env (FTerm -> [FPattern] -> Env -> MSOS Env
premise (MetaVar -> FTerm
TVar MetaVar
"X") [FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] Env
env))
            Env
env <- Maybe Values -> Maybe VPattern -> Env -> MSOS Env
receiveSignalPatt Maybe Values
__varabrupted (forall a. a -> Maybe a
Just (MetaVar -> VPattern
VPMetaVar MetaVar
"A")) Env
env
            Name -> FTerm -> Env -> MSOS ()
raiseTerm Name
"abrupted" (MetaVar -> FTerm
TVar MetaVar
"A") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> [FTerm] -> FTerm
TApp Name
"thread-atomic" [MetaVar -> FTerm
TVar MetaVar
"V"]) Env
env
          step6 :: MSOS StepRes
step6 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> MSOS Env
lifted_fsMatch [Funcons]
fargs [FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env

thread_yield_ :: [Funcons] -> Funcons
thread_yield_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-yield" ([Funcons]
fargs)
stepThread_yield :: StrictFuncon
stepThread_yield [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1,MSOS StepRes
step2,MSOS StepRes
step3]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [] forall {k} {a}. Map k a
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" ([FTerm] -> FTerm
TSeq []) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step2 :: MSOS StepRes
step2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"TI",MetaVar -> FTerm
TVar MetaVar
"ATS"]) (Name -> FTerm
TName Name
"true")) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step3 :: MSOS StepRes
step3 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"TI",MetaVar -> FTerm
TVar MetaVar
"ATS"]) (Name -> FTerm
TName Name
"false")) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"fail") Env
env

thread_spin_ :: [Funcons] -> Funcons
thread_spin_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-spin" ([Funcons]
fargs)
stepThread_spin :: NonStrictFuncon
stepThread_spin [Funcons]
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 <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"X"] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"else" [MetaVar -> FTerm
TVar MetaVar
"X",Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"thread-yield" [],Name -> [FTerm] -> FTerm
TApp Name
"thread-spin" [MetaVar -> FTerm
TVar MetaVar
"X"]]]) Env
env

thread_suspend_ :: [Funcons] -> Funcons
thread_suspend_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-suspend" ([Funcons]
fargs)
stepThread_suspend :: StrictFuncon
stepThread_suspend [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1,MSOS StepRes
step2]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI+" SeqSortOp
PlusOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"thread-ids") SeqSortOp
PlusOp)] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"TI",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI+"]]) (Name -> FTerm
TName Name
"false")) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-subset" [[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI+"],MetaVar -> FTerm
TVar MetaVar
"ATS"]) (Name -> FTerm
TName Name
"true")) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"set-difference" [MetaVar -> FTerm
TVar MetaVar
"ATS",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI+"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step2 :: MSOS StepRes
step2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI+" SeqSortOp
PlusOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"thread-ids") SeqSortOp
PlusOp)] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"TI",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI+"]]) (Name -> FTerm
TName Name
"true")) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-subset" [[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI+"],MetaVar -> FTerm
TVar MetaVar
"ATS"]) (Name -> FTerm
TName Name
"true")) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"set-difference" [MetaVar -> FTerm
TVar MetaVar
"ATS",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI+"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" ([FTerm] -> FTerm
TSeq []) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env

thread_resume_ :: [Funcons] -> Funcons
thread_resume_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-resume" ([Funcons]
fargs)
stepThread_resume :: StrictFuncon
stepThread_resume [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"thread-ids") SeqSortOp
StarOp)] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"TI",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI*"]]) (Name -> FTerm
TName Name
"false")) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"set-intersect" [MetaVar -> FTerm
TVar MetaVar
"ATS",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI*"]]) ([FTerm] -> FTerm
TSet [])) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"set-unite" [MetaVar -> FTerm
TVar MetaVar
"ATS",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI*"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env

thread_terminate_ :: [Funcons] -> Funcons
thread_terminate_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-terminate" ([Funcons]
fargs)
stepThread_terminate :: StrictFuncon
stepThread_terminate [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1,MSOS StepRes
step2]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI'") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"TM",MetaVar -> FTerm
TVar MetaVar
"TI'"]) [Name -> [VPattern] -> VPattern
PADT Name
"thread" [Name -> [VPattern] -> VPattern
PADT Name
"thunk" [Name -> [VPattern] -> VPattern
PADT Name
"abstraction" [MetaVar -> VPattern
VPMetaVar MetaVar
"X"]]]]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"TM",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI'"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TM'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"set-difference" [MetaVar -> FTerm
TVar MetaVar
"ATS",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI'"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"when-true" [Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"TI",MetaVar -> FTerm
TVar MetaVar
"TI'"]],MetaVar -> FTerm
TVar MetaVar
"TI"]) [MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI?" SeqSortOp
QuestionMarkOp]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI?") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-map" (MetaVar -> FTerm
TVar MetaVar
"TM'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step2 :: MSOS StepRes
step2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI'") (Name -> FTerm
TName Name
"thread-ids"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"terminated-thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TVM"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"TM",MetaVar -> FTerm
TVar MetaVar
"TI'"]) [Name -> [VPattern] -> VPattern
PADT Name
"thread" [Name -> [VPattern] -> VPattern
PADT Name
"thunk" [Name -> [VPattern] -> VPattern
PADT Name
"abstraction" [MetaVar -> VPattern
VPMetaVar MetaVar
"X"]],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)])]),MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI*" SeqSortOp
StarOp]]]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"TM",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI'"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TM'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"set-unite" [Name -> [FTerm] -> FTerm
TApp Name
"set-difference" [MetaVar -> FTerm
TVar MetaVar
"ATS",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI'"]],[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI*"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-unite" [MetaVar -> FTerm
TVar MetaVar
"TVM",[FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"TI'") (MetaVar -> FTerm
TVar MetaVar
"V")]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TVM'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"when-true" [Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"TI",MetaVar -> FTerm
TVar MetaVar
"TI'"]],MetaVar -> FTerm
TVar MetaVar
"TI"]) [MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI?" SeqSortOp
QuestionMarkOp]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI?") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-map" (MetaVar -> FTerm
TVar MetaVar
"TM'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"terminated-thread-map" (MetaVar -> FTerm
TVar MetaVar
"TVM'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env

is_thread_terminated_ :: [Funcons] -> Funcons
is_thread_terminated_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-thread-terminated" ([Funcons]
fargs)
stepIs_thread_terminated :: StrictFuncon
stepIs_thread_terminated [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"terminated-thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TVM"] Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> [FTerm] -> FTerm
TApp Name
"is-value" [Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"TVM",MetaVar -> FTerm
TVar MetaVar
"TI"]]) Env
env

thread_value_ :: [Funcons] -> Funcons
thread_value_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-value" ([Funcons]
fargs)
stepThread_value :: StrictFuncon
stepThread_value [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"terminated-thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TVM"] Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> [FTerm] -> FTerm
TApp Name
"checked" [Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"TVM",MetaVar -> FTerm
TVar MetaVar
"TI"]]) Env
env

thread_join_ :: [Funcons] -> Funcons
thread_join_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-join" ([Funcons]
fargs)
stepThread_join :: StrictFuncon
stepThread_join [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1,MSOS StepRes
step2,MSOS StepRes
step3,MSOS StepRes
step4]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI'") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"TM",MetaVar -> FTerm
TVar MetaVar
"TI'"]) [Name -> [VPattern] -> VPattern
PADT Name
"thread" [MetaVar -> VPattern
VPMetaVar MetaVar
"TH",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)])]),MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI*" SeqSortOp
StarOp]]]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-override" [[FTerm] -> FTerm
TMap [FTerm -> FTerm -> FTerm
TBinding (MetaVar -> FTerm
TVar MetaVar
"TI'") (Name -> [FTerm] -> FTerm
TApp Name
"thread" [MetaVar -> FTerm
TVar MetaVar
"TH",Name -> [FTerm] -> FTerm
TApp Name
"list" [MetaVar -> FTerm
TVar MetaVar
"TI*",MetaVar -> FTerm
TVar MetaVar
"TI"]])],MetaVar -> FTerm
TVar MetaVar
"TM"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TM'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"set-difference" [MetaVar -> FTerm
TVar MetaVar
"ATS",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-map" (MetaVar -> FTerm
TVar MetaVar
"TM'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" ([FTerm] -> FTerm
TSeq []) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step2 :: MSOS StepRes
step2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI'") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"terminated-thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TVM"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-value" [Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"TVM",MetaVar -> FTerm
TVar MetaVar
"TI'"]]) (Name -> FTerm
TName Name
"true")) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step3 :: MSOS StepRes
step3 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI'") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"TM",MetaVar -> FTerm
TVar MetaVar
"TI'"]) [Name -> [VPattern] -> VPattern
PADT Name
"thread" [MetaVar -> VPattern
VPMetaVar MetaVar
"TH"]]) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"fail") Env
env
          step4 :: MSOS StepRes
step4 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI'") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"terminated-thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TVM"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"TM",MetaVar -> FTerm
TVar MetaVar
"TI'"]) ([FTerm] -> FTerm
TSeq [])) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"lookup" [MetaVar -> FTerm
TVar MetaVar
"TVM",MetaVar -> FTerm
TVar MetaVar
"TI'"]) ([FTerm] -> FTerm
TSeq [])) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"fail") Env
env

thread_exterminate_ :: [Funcons] -> Funcons
thread_exterminate_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"thread-exterminate" ([Funcons]
fargs)
stepThread_exterminate :: StrictFuncon
stepThread_exterminate [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"TI'") (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TM"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"terminated-thread-map" [MetaVar -> VPattern
VPMetaVar MetaVar
"TVM"] Env
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> FTerm -> SideCondition
SCInequality (MetaVar -> FTerm
TVar MetaVar
"TI'") (MetaVar -> FTerm
TVar MetaVar
"TI")) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"TM",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI'"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TM'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"TVM",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI'"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TVM'"]) Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"set-difference" [MetaVar -> FTerm
TVar MetaVar
"ATS",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"TI'"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-map" (MetaVar -> FTerm
TVar MetaVar
"TM'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"terminated-thread-map" (MetaVar -> FTerm
TVar MetaVar
"TVM'") Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"active-thread-set" (MetaVar -> FTerm
TVar MetaVar
"ATS'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env

update_thread_stepping_ :: Funcons
update_thread_stepping_ = Name -> Funcons
FName Name
"update-thread-stepping"
stepUpdate_thread_stepping :: NullaryFuncon
stepUpdate_thread_stepping = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1,MSOS StepRes
step2,MSOS StepRes
step3,MSOS StepRes
step4]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] forall {k} {a}. Map k a
env
            Env
env <- FTerm -> [FPattern] -> Env -> MSOS Env
premise (Name -> [FTerm] -> FTerm
TApp Name
"is-thread-preemptible" [MetaVar -> FTerm
TVar MetaVar
"TI"]) [VPattern -> FPattern
PValue (Name -> [VPattern] -> VPattern
PADT Name
"false" [])] Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step2 :: MSOS StepRes
step2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> VPattern
VPMetaVar MetaVar
"TI"] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- FTerm -> [FPattern] -> Env -> MSOS Env
premise (Name -> [FTerm] -> FTerm
TApp Name
"is-thread-preemptible" [MetaVar -> FTerm
TVar MetaVar
"TI"]) [VPattern -> FPattern
PValue (Name -> [VPattern] -> VPattern
PADT Name
"true" [])] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"some-element" [MetaVar -> FTerm
TVar MetaVar
"ATS"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TI'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step3 :: MSOS StepRes
step3 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [MetaVar -> VPattern
VPMetaVar MetaVar
"ATS"] Env
env
            Env
env <- SideCondition -> Env -> MSOS Env
lifted_sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"some-element" [MetaVar -> FTerm
TVar MetaVar
"ATS"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"TI'"]) Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" (MetaVar -> FTerm
TVar MetaVar
"TI'") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env
          step4 :: MSOS StepRes
step4 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-stepping" [MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"TI?" SeqSortOp
QuestionMarkOp] forall {k} {a}. Map k a
env
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"active-thread-set" [Name -> [VPattern] -> VPattern
PADT Name
"set" []] Env
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-stepping" ([FTerm] -> FTerm
TSeq []) Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env

update_thread_schedule_ :: [Funcons] -> Funcons
update_thread_schedule_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"update-thread-schedule" ([Funcons]
fargs)
stepUpdate_thread_schedule :: StrictFuncon
stepUpdate_thread_schedule [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"VS") (Name -> [FTerm] -> FTerm
TApp Name
"sets" [Name -> FTerm
TName Name
"ground-values"])] forall {k} {a}. Map k a
env
            Name -> FTerm -> Env -> MSOS ()
putMutTerm Name
"thread-schedule" (MetaVar -> FTerm
TVar MetaVar
"VS") Env
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (Name -> FTerm
TName Name
"null-value") Env
env

current_thread_schedule_ :: Funcons
current_thread_schedule_ = Name -> Funcons
FName Name
"current-thread-schedule"
stepCurrent_thread_schedule :: NullaryFuncon
stepCurrent_thread_schedule = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [] [MSOS StepRes
step1]
    where step1 :: MSOS StepRes
step1 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- Name -> [VPattern] -> Env -> MSOS Env
getMutPatt Name
"thread-schedule" [MetaVar -> VPattern
VPMetaVar MetaVar
"VS"] forall {k} {a}. Map k a
env
            FTerm -> Env -> MSOS StepRes
stepTermTo (MetaVar -> FTerm
TVar MetaVar
"VS") Env
env

thread_preemptible_ :: Funcons
thread_preemptible_ = Name -> Funcons
FName Name
"thread-preemptible"
stepThread_preemptible :: NullaryFuncon
stepThread_preemptible = [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
116)]),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
114)]),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
97)]),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
45)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
112)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
114)]),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
101)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
109)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
112)]),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
98)]),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
101)])]))]) forall {k} {a}. Map k a
env

thread_cooperative_ :: Funcons
thread_cooperative_ = Name -> Funcons
FName Name
"thread-cooperative"
stepThread_cooperative :: NullaryFuncon
stepThread_cooperative = [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
116)]),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
114)]),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
97)]),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
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
111)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
112)]),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)]),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
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
118)]),Values -> Funcons
FValue (forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (forall t. Integer -> Values t
Int Integer
101)])]))]) forall {k} {a}. Map k a
env

is_thread_preemptible_ :: [Funcons] -> Funcons
is_thread_preemptible_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-thread-preemptible" ([Funcons]
fargs)
stepIs_thread_preemptible :: StrictFuncon
stepIs_thread_preemptible [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 VPattern
VPWildCard (Name -> FTerm
TName Name
"thread-ids")] forall {k} {a}. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"not" [Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [Name -> FTerm
TName Name
"thread-cooperative",Name -> FTerm
TName Name
"current-thread-schedule"]]) Env
env

thread_ids_ :: Funcons
thread_ids_ = Name -> Funcons
FName Name
"thread-ids"
stepThread_ids :: NullaryFuncon
stepThread_ids = Name -> StrictFuncon
rewriteType Name
"thread-ids" []

threads_ :: Funcons
threads_ = Name -> Funcons
FName Name
"threads"
stepThreads :: NullaryFuncon
stepThreads = Name -> StrictFuncon
rewriteType Name
"threads" []

thread_preemtibilities_ :: Funcons
thread_preemtibilities_ = Name -> Funcons
FName Name
"thread-preemtibilities"
stepThread_preemtibilities :: NullaryFuncon
stepThread_preemtibilities = Name -> StrictFuncon
rewriteType Name
"thread-preemtibilities" []