diff --git a/cbs/Funcons/Core/Computations/Abnormal/Abrupting/Abrupting.hs b/cbs/Funcons/Core/Computations/Abnormal/Abrupting/Abrupting.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Abrupting/Abrupting.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Abrupting/Abrupting.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Abnormal/Abrupting/Abrupting.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Abnormal/Abrupting/Abrupting.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Abnormal.Abrupting.Abrupting where diff --git a/cbs/Funcons/Core/Computations/Abnormal/Breaking/Breaking.hs b/cbs/Funcons/Core/Computations/Abnormal/Breaking/Breaking.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Breaking/Breaking.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Breaking/Breaking.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Abnormal/Breaking/Breaking.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Abnormal/Breaking/Breaking.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Abnormal.Breaking.Breaking where diff --git a/cbs/Funcons/Core/Computations/Abnormal/Continuing/Continuing.hs b/cbs/Funcons/Core/Computations/Abnormal/Continuing/Continuing.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Continuing/Continuing.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Continuing/Continuing.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Abnormal/Continuing/Continuing.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Abnormal/Continuing/Continuing.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Abnormal.Continuing.Continuing where diff --git a/cbs/Funcons/Core/Computations/Abnormal/Controlling/Controlling.hs b/cbs/Funcons/Core/Computations/Abnormal/Controlling/Controlling.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Controlling/Controlling.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Controlling/Controlling.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Abnormal/Controlling/Controlling.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Abnormal/Controlling/Controlling.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Abnormal.Controlling.Controlling where diff --git a/cbs/Funcons/Core/Computations/Abnormal/Failing/Failing.hs b/cbs/Funcons/Core/Computations/Abnormal/Failing/Failing.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Failing/Failing.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Failing/Failing.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Abnormal/Failing/Failing.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Abnormal/Failing/Failing.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Abnormal.Failing.Failing where diff --git a/cbs/Funcons/Core/Computations/Abnormal/Postponing/Postponing.hs b/cbs/Funcons/Core/Computations/Abnormal/Postponing/Postponing.hs new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Computations/Abnormal/Postponing/Postponing.hs @@ -0,0 +1,68 @@ +-- GeNeRaTeD fOr: /home/thomas/repos/plancomps/CBS-beta/Unstable-Funcons-beta/Computations/Abnormal/Postponing/Postponing.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Computations.Abnormal.Postponing.Postponing where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) +entities = [] + +types = typeEnvFromList + [] + +funcons = libFromList + [("postpone",NonStrictFuncon stepPostpone),("postpone-after-effect",NonStrictFuncon stepPostpone_after_effect),("after-effect",NonStrictFuncon stepAfter_effect)] + +postpone_ fargs = FApp "postpone" (fargs) +stepPostpone fargs = + evalRules [] [step1,step2] + where step1 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getInhPatt "given-value" [VPMetaVar "V"] env + env <- getControlPatt "postponing" (Just (VPMetaVar "A")) env + (env,[__varpostponing]) <- receiveSignals ["postponing"] (withControlTerm "postponing" (Nothing) env (withInhTerm "given-value" (TVar "V") env (premise (TApp "closure" [TApp "give" [TVar "V",TVar "X"]]) [PMetaVar "A"] env))) + env <- receiveSignalPatt __varpostponing (Nothing) env + raiseTerm "postponing" (TVar "A") env + stepTermTo (TName "null-value") env + step2 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getInhPatt "given-value" [] env + env <- getControlPatt "postponing" (Just (VPMetaVar "A")) env + (env,[__varpostponing]) <- receiveSignals ["postponing"] (withControlTerm "postponing" (Nothing) env (withInhTerm "given-value" (TSeq []) env (premise (TApp "closure" [TApp "no-given" [TVar "X"]]) [PMetaVar "A"] env))) + env <- receiveSignalPatt __varpostponing (Nothing) env + raiseTerm "postponing" (TVar "A") env + stepTermTo (TName "null-value") env + +postpone_after_effect_ fargs = FApp "postpone-after-effect" (fargs) +stepPostpone_after_effect fargs = + evalRules [rewrite1] [step1,step2] + where rewrite1 = do + let env = emptyEnv + env <- fsMatch fargs [PAnnotated (PMetaVar "V") (TName "values")] env + rewriteTermTo (TVar "V") env + step1 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getControlPatt "postponing" (Nothing) env + (env,[__varpostponing]) <- receiveSignals ["postponing"] (withControlTerm "postponing" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) + env <- receiveSignalPatt __varpostponing (Nothing) env + stepTermTo (TApp "postpone-after-effect" [TVar "X'"]) env + step2 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getControlPatt "postponing" (Nothing) env + (env,[__varpostponing]) <- receiveSignals ["postponing"] (withControlTerm "postponing" (Just (TVar "A")) env (premise (TVar "X") [PMetaVar "X'"] env)) + env <- receiveSignalPatt __varpostponing (Just (VPMetaVar "A")) env + env <- lifted_sideCondition (SCPatternMatch (TVar "A") [PADT "abstraction" [VPMetaVar "Y"]]) env + stepTermTo (TApp "postpone-after-effect" [TApp "after-effect" [TVar "X'",TVar "Y"]]) env + +after_effect_ fargs = FApp "after-effect" (fargs) +stepAfter_effect fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- fsMatch fargs [PMetaVar "X",PMetaVar "Y"] env + rewriteTermTo (TApp "give" [TVar "X",TApp "sequential" [TVar "Y",TName "given"]]) env diff --git a/cbs/Funcons/Core/Computations/Abnormal/Returning/Returning.hs b/cbs/Funcons/Core/Computations/Abnormal/Returning/Returning.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Returning/Returning.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Returning/Returning.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Abnormal/Returning/Returning.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Abnormal/Returning/Returning.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Abnormal.Returning.Returning where diff --git a/cbs/Funcons/Core/Computations/Abnormal/Throwing/Throwing.hs b/cbs/Funcons/Core/Computations/Abnormal/Throwing/Throwing.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Throwing/Throwing.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Throwing/Throwing.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Abnormal/Throwing/Throwing.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Abnormal/Throwing/Throwing.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Abnormal.Throwing.Throwing where diff --git a/cbs/Funcons/Core/Computations/Normal/Binding/Binding.hs b/cbs/Funcons/Core/Computations/Normal/Binding/Binding.hs --- a/cbs/Funcons/Core/Computations/Normal/Binding/Binding.hs +++ b/cbs/Funcons/Core/Computations/Normal/Binding/Binding.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Normal/Binding/Binding.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Normal/Binding/Binding.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Normal.Binding.Binding where diff --git a/cbs/Funcons/Core/Computations/Normal/Generating/Generating.hs b/cbs/Funcons/Core/Computations/Normal/Generating/Generating.hs --- a/cbs/Funcons/Core/Computations/Normal/Generating/Generating.hs +++ b/cbs/Funcons/Core/Computations/Normal/Generating/Generating.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Normal/Generating/Generating.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Normal/Generating/Generating.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Normal.Generating.Generating where @@ -18,7 +18,7 @@ stepFresh_atom = evalRules [] [step1] where step1 = do let env = emptyEnv - env <- getMutPatt "used-atom-set" (VPMetaVar "SA") env + env <- getMutPatt "used-atom-set" [VPMetaVar "SA"] env env <- lifted_sideCondition (SCPatternMatch (TApp "element-not-in" [TName "atoms",TVar "SA"]) [VPMetaVar "A"]) env putMutTerm "used-atom-set" (TApp "set-insert" [TVar "A",TVar "SA"]) env stepTermTo (TVar "A") env @@ -29,7 +29,7 @@ where step1 = do let env = emptyEnv env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "SA") (TApp "sets" [TName "atoms"])] env - env <- getMutPatt "used-atom-set" (VPMetaVar "SA'") env + env <- getMutPatt "used-atom-set" [VPMetaVar "SA'"] env env <- lifted_sideCondition (SCPatternMatch (TApp "element-not-in" [TName "atoms",TVar "SA"]) [VPMetaVar "A"]) env putMutTerm "used-atom-set" (TApp "set-insert" [TVar "A",TVar "SA'"]) env stepTermTo (TVar "A") env diff --git a/cbs/Funcons/Core/Computations/Normal/Giving/Giving.hs b/cbs/Funcons/Core/Computations/Normal/Giving/Giving.hs --- a/cbs/Funcons/Core/Computations/Normal/Giving/Giving.hs +++ b/cbs/Funcons/Core/Computations/Normal/Giving/Giving.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Normal/Giving/Giving.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Normal/Giving/Giving.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Normal.Giving.Giving where diff --git a/cbs/Funcons/Core/Computations/Normal/Indexing/Indexing.hs b/cbs/Funcons/Core/Computations/Normal/Indexing/Indexing.hs new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Computations/Normal/Indexing/Indexing.hs @@ -0,0 +1,43 @@ +-- GeNeRaTeD fOr: /home/thomas/repos/plancomps/CBS-beta/Unstable-Funcons-beta/Computations/Normal/Indexing/Indexing.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Computations.Normal.Indexing.Indexing where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) +entities = [] + +types = typeEnvFromList + [] + +funcons = libFromList + [("initialise-index",NullaryFuncon stepInitialise_index),("allocate-index",StrictFuncon stepAllocate_index),("lookup-index",StrictFuncon stepLookup_index)] + +initialise_index_ = FName "initialise-index" +stepInitialise_index = evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- getMutPatt "value-index" [VPWildCard] env + putMutTerm "value-index" (TSeq []) env + stepTermTo (TName "null-value") env + +allocate_index_ fargs = FApp "allocate-index" (fargs) +stepAllocate_index fargs = + evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "ground-values")] env + env <- getMutPatt "value-index" [VPSeqVar "V*" StarOp] env + putMutTerm "value-index" (TSeq [TVar "V*",TVar "V"]) env + stepTermTo (TApp "length" [TVar "V*",TVar "V"]) env + +lookup_index_ fargs = FApp "lookup-index" (fargs) +stepLookup_index fargs = + evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "natural-numbers")] env + env <- getMutPatt "value-index" [VPSeqVar "V*" StarOp] env + putMutTerm "value-index" (TVar "V*") env + stepTermTo (TApp "index" [TVar "N",TVar "V*"]) env diff --git a/cbs/Funcons/Core/Computations/Normal/Interacting/Interacting.hs b/cbs/Funcons/Core/Computations/Normal/Interacting/Interacting.hs --- a/cbs/Funcons/Core/Computations/Normal/Interacting/Interacting.hs +++ b/cbs/Funcons/Core/Computations/Normal/Interacting/Interacting.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Normal/Interacting/Interacting.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Normal/Interacting/Interacting.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Normal.Interacting.Interacting where diff --git a/cbs/Funcons/Core/Computations/Normal/Linking/Linking.hs b/cbs/Funcons/Core/Computations/Normal/Linking/Linking.hs --- a/cbs/Funcons/Core/Computations/Normal/Linking/Linking.hs +++ b/cbs/Funcons/Core/Computations/Normal/Linking/Linking.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Normal/Linking/Linking.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Normal/Linking/Linking.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Normal.Linking.Linking where diff --git a/cbs/Funcons/Core/Computations/Normal/Memos/Memos.hs b/cbs/Funcons/Core/Computations/Normal/Memos/Memos.hs new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Computations/Normal/Memos/Memos.hs @@ -0,0 +1,69 @@ +-- GeNeRaTeD fOr: /home/thomas/repos/plancomps/CBS-beta/Unstable-Funcons-beta/Computations/Normal/Memos/Memos.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Computations.Normal.Memos.Memos where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) +entities = [] + +types = typeEnvFromList + [] + +funcons = libFromList + [("initialise-memos",NonStrictFuncon stepInitialise_memos),("memo-value",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepMemo_value),("initialise-memo-value",StrictFuncon stepInitialise_memo_value),("memo-value-recall",StrictFuncon stepMemo_value_recall)] + +initialise_memos_ fargs = FApp "initialise-memos" (fargs) +stepInitialise_memos fargs = + evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getMutPatt "memo-map" [VPWildCard] env + putMutTerm "memo-map" (TApp "map" []) env + stepTermTo (TVar "X") env + +memo_value_ fargs = FApp "memo-value" (fargs) +stepMemo_value fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- fsMatch fargs [PAnnotated (PMetaVar "K") (TName "ground-values"),PMetaVar "X"] env + rewriteTermTo (TApp "else" [TApp "memo-value-recall" [TVar "K"],TApp "give" [TVar "X",TApp "sequential" [TApp "else" [TApp "initialise-memo-value" [TVar "K",TName "given"],TName "null-value"],TApp "memo-value-recall" [TVar "K"]]]]) env + +initialise_memo_value_ fargs = FApp "initialise-memo-value" (fargs) +stepInitialise_memo_value fargs = + evalRules [] [step1,step2] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "K") (TName "ground-values"),VPAnnotated (VPMetaVar "V") (TName "values")] env + env <- getMutPatt "memo-map" [VPMetaVar "M"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-unite" [TVar "M",TMap [TBinding (TVar "K") (TVar "V")]]) [VPMetaVar "M'"]) env + putMutTerm "memo-map" (TVar "M'") env + stepTermTo (TName "null-value") env + step2 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "K") (TName "ground-values"),VPAnnotated (VPMetaVar "V") (TName "values")] env + env <- getMutPatt "memo-map" [VPMetaVar "M"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-unite" [TVar "M",TMap [TBinding (TVar "K") (TVar "V")]]) []) env + putMutTerm "memo-map" (TVar "M") env + stepTermTo (TName "fail") env + +memo_value_recall_ fargs = FApp "memo-value-recall" (fargs) +stepMemo_value_recall fargs = + evalRules [] [step1,step2] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "K") (TName "ground-values")] env + env <- getMutPatt "memo-map" [VPMetaVar "M"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "M",TVar "K"]) [VPMetaVar "V"]) env + putMutTerm "memo-map" (TVar "M") env + stepTermTo (TVar "V") env + step2 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "K") (TName "ground-values")] env + env <- getMutPatt "memo-map" [VPMetaVar "M"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "M",TVar "K"]) []) env + putMutTerm "memo-map" (TVar "M") env + stepTermTo (TName "fail") env diff --git a/cbs/Funcons/Core/Computations/Normal/Storing/Storing.hs b/cbs/Funcons/Core/Computations/Normal/Storing/Storing.hs --- a/cbs/Funcons/Core/Computations/Normal/Storing/Storing.hs +++ b/cbs/Funcons/Core/Computations/Normal/Storing/Storing.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Normal/Storing/Storing.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Computations/Normal/Storing/Storing.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Computations.Normal.Storing.Storing where @@ -31,7 +31,7 @@ stepStore_clear = evalRules [] [step1] where step1 = do let env = emptyEnv - env <- getMutPatt "store" (VPWildCard) env + env <- getMutPatt "store" [VPWildCard] env putMutTerm "store" (TApp "map" []) env stepTermTo (TName "null-value") env @@ -62,10 +62,10 @@ where step1 = do let env = emptyEnv env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "T") (TName "types")] env - env <- getMutPatt "store" (VPMetaVar "Sigma") env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env putMutTerm "store" (TVar "Sigma") env env <- premise (TApp "use-atom-not-in" [TApp "dom" [TVar "Sigma"]]) [PMetaVar "L"] env - env <- getMutPatt "store" (VPMetaVar "Sigma'") env + env <- getMutPatt "store" [VPMetaVar "Sigma'"] env env <- lifted_sideCondition (SCPatternMatch (TApp "map-override" [TMap [TBinding (TVar "L") (TSeq [])],TVar "Sigma'"]) [VPMetaVar "Sigma''"]) env putMutTerm "store" (TVar "Sigma''") env stepTermTo (TApp "variable" [TVar "L",TVar "T"]) env @@ -81,14 +81,14 @@ step1 = do let env = emptyEnv env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env - env <- getMutPatt "store" (VPMetaVar "Sigma") env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "true")) env putMutTerm "store" (TApp "map-delete" [TVar "Sigma",TSet [TVar "L"]]) env stepTermTo (TName "null-value") env step2 = do let env = emptyEnv env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env - env <- getMutPatt "store" (VPMetaVar "Sigma") env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "false")) env putMutTerm "store" (TVar "Sigma") env stepTermTo (TName "fail") env @@ -100,14 +100,14 @@ where step1 = do let env = emptyEnv env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "values")] env - env <- getMutPatt "store" (VPMetaVar "Sigma") env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "not" [TApp "is-value" [TApp "map-lookup" [TVar "Sigma",TVar "L"]]],TApp "is-in-type" [TVar "Val",TVar "T"]]) (TName "true")) env putMutTerm "store" (TApp "map-override" [TMap [TBinding (TVar "L") (TVar "Val")],TVar "Sigma"]) env stepTermTo (TName "null-value") env step2 = do let env = emptyEnv env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "values")] env - env <- getMutPatt "store" (VPMetaVar "Sigma") env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "not" [TApp "is-value" [TApp "map-lookup" [TVar "Sigma",TVar "L"]]],TApp "is-in-type" [TVar "Val",TVar "T"]]) (TName "false")) env putMutTerm "store" (TVar "Sigma") env stepTermTo (TName "fail") env @@ -127,14 +127,14 @@ where step1 = do let env = emptyEnv env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "values")] env - env <- getMutPatt "store" (VPMetaVar "Sigma") env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "is-in-type" [TVar "Val",TVar "T"]]) (TName "true")) env putMutTerm "store" (TApp "map-override" [TMap [TBinding (TVar "L") (TVar "Val")],TVar "Sigma"]) env stepTermTo (TName "null-value") env step2 = do let env = emptyEnv env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "values")] env - env <- getMutPatt "store" (VPMetaVar "Sigma") env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "is-in-type" [TVar "Val",TVar "T"]]) (TName "false")) env putMutTerm "store" (TVar "Sigma") env stepTermTo (TName "fail") env @@ -145,14 +145,14 @@ where step1 = do let env = emptyEnv env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env - env <- getMutPatt "store" (VPMetaVar "Sigma") env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env env <- lifted_sideCondition (SCPatternMatch (TApp "map-lookup" [TVar "Sigma",TVar "L"]) [VPAnnotated (VPMetaVar "Val") (TName "values")]) env putMutTerm "store" (TVar "Sigma") env stepTermTo (TVar "Val") env step2 = do let env = emptyEnv env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env - env <- getMutPatt "store" (VPMetaVar "Sigma") env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env env <- lifted_sideCondition (SCEquality (TApp "map-lookup" [TVar "Sigma",TVar "L"]) (TSeq [])) env putMutTerm "store" (TVar "Sigma") env stepTermTo (TName "fail") env @@ -175,14 +175,14 @@ where step1 = do let env = emptyEnv env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env - env <- getMutPatt "store" (VPMetaVar "Sigma") env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "true")) env putMutTerm "store" (TApp "map-override" [TMap [TBinding (TVar "L") (TSeq [])],TVar "Sigma"]) env stepTermTo (TName "null-value") env step2 = do let env = emptyEnv env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env - env <- getMutPatt "store" (VPMetaVar "Sigma") env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "false")) env putMutTerm "store" (TVar "Sigma") env stepTermTo (TName "fail") env diff --git a/cbs/Funcons/Core/Computations/Threads/Multithreading/Multithreading.hs b/cbs/Funcons/Core/Computations/Threads/Multithreading/Multithreading.hs new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Computations/Threads/Multithreading/Multithreading.hs @@ -0,0 +1,547 @@ +-- 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 = [] + +types = typeEnvFromList + [("thread-ids",DataTypeMemberss "thread-ids" [] [DataTypeMemberConstructor "thread-id" [TName "atoms"] (Just [])]),("threads",DataTypeMemberss "threads" [] [DataTypeMemberConstructor "thread" [TApp "thunks" [TName "values"],TSortSeq (TApp "lists" [TName "thread-ids"]) QuestionMarkOp] (Just [])]),("thread-preemtibilities",DataTypeMemberss "thread-preemtibilities" [] [DataTypeMemberConstructor "thread-preemptible" [] (Just []),DataTypeMemberConstructor "thread-cooperative" [] (Just [])])] + +funcons = libFromList + [("thread-id",StrictFuncon stepThread_id),("thread",StrictFuncon stepThread),("thread-joinable",StrictFuncon stepThread_joinable),("thread-detached",StrictFuncon stepThread_detached),("is-some-thread-active",NullaryFuncon stepIs_some_thread_active),("is-some-thread-suspended",NullaryFuncon stepIs_some_thread_suspended),("initialise-multithreading",NullaryFuncon stepInitialise_multithreading),("initialise-thread-map",NullaryFuncon stepInitialise_thread_map),("initialise-active-thread-set",NullaryFuncon stepInitialise_active_thread_set),("initialise-thread-stepping",NullaryFuncon stepInitialise_thread_stepping),("initialise-terminated-thread-map",NullaryFuncon stepInitialise_terminated_thread_map),("initialise-thread-schedule",NullaryFuncon stepInitialise_thread_schedule),("multithread",NonStrictFuncon stepMultithread),("thread-activate",StrictFuncon stepThread_activate),("thread-detach",StrictFuncon stepThread_detach),("current-thread",NullaryFuncon stepCurrent_thread),("thread-step",NullaryFuncon stepThread_step),("thread-atomic",NonStrictFuncon stepThread_atomic),("thread-yield",StrictFuncon stepThread_yield),("thread-spin",NonStrictFuncon stepThread_spin),("thread-suspend",StrictFuncon stepThread_suspend),("thread-resume",StrictFuncon stepThread_resume),("thread-terminate",StrictFuncon stepThread_terminate),("is-thread-terminated",StrictFuncon stepIs_thread_terminated),("thread-value",StrictFuncon stepThread_value),("thread-join",StrictFuncon stepThread_join),("thread-exterminate",StrictFuncon stepThread_exterminate),("update-thread-stepping",NullaryFuncon stepUpdate_thread_stepping),("update-thread-schedule",StrictFuncon stepUpdate_thread_schedule),("current-thread-schedule",NullaryFuncon stepCurrent_thread_schedule),("thread-preemptible",NullaryFuncon stepThread_preemptible),("thread-cooperative",NullaryFuncon stepThread_cooperative),("is-thread-preemptible",StrictFuncon stepIs_thread_preemptible),("thread-ids",NullaryFuncon stepThread_ids),("threads",NullaryFuncon stepThreads),("thread-preemtibilities",NullaryFuncon stepThread_preemtibilities)] + +thread_id_ fargs = FApp "thread-id" (fargs) +stepThread_id fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPMetaVar "_X1"] env + env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 104)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 100)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 100)])])),TVar "_X1"]) env + +thread_ fargs = FApp "thread" (fargs) +stepThread fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPMetaVar "_X1",VPSeqVar "_X2?" QuestionMarkOp] env + env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env + env <- sideCondition (SCIsInSort (TVar "_X2?") (TSortSeq (TSortSeq (TName "values") QuestionMarkOp) QuestionMarkOp)) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 104)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 100)])])),TVar "_X1",TVar "_X2?"]) env + +thread_joinable_ fargs = FApp "thread-joinable" (fargs) +stepThread_joinable fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "TH") (TApp "thunks" [TName "values"])] env + rewriteTermTo (TApp "thread" [TVar "TH",TApp "list" []]) env + +thread_detached_ fargs = FApp "thread-detached" (fargs) +stepThread_detached fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "TH") (TApp "thunks" [TName "values"])] env + rewriteTermTo (TApp "thread" [TVar "TH"]) env + +is_some_thread_active_ = FName "is-some-thread-active" +stepIs_some_thread_active = evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + stepTermTo (TApp "not" [TApp "is-equal" [TVar "ATS",TSet []]]) env + +is_some_thread_suspended_ = FName "is-some-thread-suspended" +stepIs_some_thread_suspended = evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + stepTermTo (TApp "not" [TApp "is-equal" [TVar "ATS",TApp "dom" [TVar "TM"]]]) env + +initialise_multithreading_ = FName "initialise-multithreading" +stepInitialise_multithreading = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "sequential" [TName "initialise-thread-map",TName "initialise-active-thread-set",TName "initialise-thread-stepping",TName "initialise-terminated-thread-map",TName "initialise-thread-schedule"]) env + +initialise_thread_map_ = FName "initialise-thread-map" +stepInitialise_thread_map = evalRules [] [step1] + where step1 = do + let env = emptyEnv + putMutTerm "thread-map" (TApp "map" []) env + stepTermTo (TName "null-value") env + +initialise_active_thread_set_ = FName "initialise-active-thread-set" +stepInitialise_active_thread_set = evalRules [] [step1] + where step1 = do + let env = emptyEnv + putMutTerm "active-thread-set" (TSet []) env + stepTermTo (TName "null-value") env + +initialise_thread_stepping_ = FName "initialise-thread-stepping" +stepInitialise_thread_stepping = evalRules [] [step1] + where step1 = do + let env = emptyEnv + putMutTerm "thread-stepping" (TSeq []) env + stepTermTo (TName "null-value") env + +initialise_terminated_thread_map_ = FName "initialise-terminated-thread-map" +stepInitialise_terminated_thread_map = evalRules [] [step1] + where step1 = do + let env = emptyEnv + putMutTerm "terminated-thread-map" (TApp "map" []) env + stepTermTo (TName "null-value") env + +initialise_thread_schedule_ = FName "initialise-thread-schedule" +stepInitialise_thread_schedule = evalRules [] [step1] + where step1 = do + let env = emptyEnv + putMutTerm "thread-schedule" (TSet []) env + stepTermTo (TName "null-value") env + +multithread_ fargs = FApp "multithread" (fargs) +stepMultithread fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- fsMatch fargs [PMetaVar "X"] env + rewriteTermTo (TApp "sequential" [TName "initialise-multithreading",TApp "give" [TApp "thread-activate" [TApp "thread-joinable" [TApp "thunk" [TApp "closure" [TVar "X"]]]],TApp "handle-abrupt" [TApp "sequential" [TApp "while-true" [TName "is-some-thread-active",TApp "sequential" [TName "update-thread-stepping",TName "thread-step"]],TApp "check" [TApp "not" [TName "is-some-thread-suspended"]],TApp "thread-value" [TName "given"]],TName "given"]]]) env + +thread_activate_ fargs = FApp "thread-activate" (fargs) +stepThread_activate fargs = + evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "THR") (TName "threads")] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- premise (TApp "thread-id" [TName "fresh-atom"]) [PMetaVar "TI"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-unite" [TMap [TBinding (TVar "TI") (TVar "THR")],TVar "TM"]) [VPMetaVar "TM'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "set-unite" [TSet [TVar "TI"],TVar "ATS"]) [VPMetaVar "ATS'"]) env + putMutTerm "thread-map" (TVar "TM'") env + putMutTerm "active-thread-set" (TVar "ATS'") env + stepTermTo (TVar "TI") env + +thread_detach_ fargs = FApp "thread-detach" (fargs) +stepThread_detach fargs = + evalRules [] [step1,step2] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI") (TName "thread-ids")] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-lookup" [TVar "TM",TVar "TI"]) [PADT "thread" [VPMetaVar "TH",VPWildCard]]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-override" [TMap [TBinding (TVar "TI") (TApp "thread" [TVar "TH"])],TVar "TM"]) [VPMetaVar "TM'"]) env + putMutTerm "thread-map" (TVar "TM'") env + stepTermTo (TName "null-value") env + step2 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI") (TName "thread-ids")] env + env <- getMutPatt "terminated-thread-map" [VPMetaVar "TMV"] env + env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "TI",TApp "dom" [TVar "TMV"]]) (TName "true")) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-delete" [TVar "TMV",TSet [TVar "TI"]]) [VPMetaVar "TMV'"]) env + putMutTerm "terminated-thread-map" (TVar "TMV'") env + stepTermTo (TName "null-value") env + +current_thread_ = FName "current-thread" +stepCurrent_thread = evalRules [] [step1,step2] + where step1 = do + let env = emptyEnv + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + stepTermTo (TVar "TI") env + step2 = do + let env = emptyEnv + env <- getMutPatt "thread-stepping" [] env + stepTermTo (TName "fail") env + +thread_step_ = FName "thread-step" +stepThread_step = evalRules [] [step1,step2,step3] + where step1 = do + let env = emptyEnv + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "TM",TVar "TI"]) [PADT "thread" [PADT "thunk" [PADT "abstraction" [VPMetaVar "X"]],VPSeqVar "L?" QuestionMarkOp]]) env + putMutTerm "thread-stepping" (TVar "TI") env + putMutTerm "thread-map" (TVar "TM") env + env <- premise (TVar "X") [PMetaVar "X'"] env + env <- getMutPatt "thread-stepping" [VPSeqVar "TI?" QuestionMarkOp] env + env <- getMutPatt "thread-map" [VPMetaVar "TM'"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "if-true-else" [TApp "is-in-set" [TVar "TI",TApp "dom" [TVar "TM'"]],TApp "map-override" [TMap [TBinding (TVar "TI") (TApp "thread" [TApp "thunk" [TApp "abstraction" [TVar "X'"]],TVar "L?"])],TVar "TM'"],TVar "TM'"]) [VPMetaVar "TM''"]) env + putMutTerm "thread-stepping" (TVar "TI?") env + putMutTerm "thread-map" (TVar "TM''") env + stepTermTo (TName "null-value") env + step2 = do + let env = emptyEnv + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "TM",TVar "TI"]) [PADT "thread" [PADT "thunk" [PADT "abstraction" [VPMetaVar "X"]]]]) env + env <- lifted_sideCondition (SCPatternMatch (TVar "X") [VPAnnotated (VPMetaVar "V") (TName "values")]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-delete" [TVar "TM",TSet [TVar "TI"]]) [VPMetaVar "TM'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "set-difference" [TVar "ATS",TSet [TVar "TI"]]) [VPMetaVar "ATS'"]) env + putMutTerm "active-thread-set" (TVar "ATS'") env + putMutTerm "thread-stepping" (TSeq []) env + putMutTerm "thread-map" (TVar "TM'") env + stepTermTo (TName "null-value") env + step3 = do + let env = emptyEnv + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + env <- getMutPatt "terminated-thread-map" [VPMetaVar "TVM"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "TM",TVar "TI"]) [PADT "thread" [PADT "thunk" [PADT "abstraction" [VPMetaVar "X"]],PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),VPSeqVar "TI*" StarOp]]]) env + env <- lifted_sideCondition (SCPatternMatch (TVar "X") [VPAnnotated (VPMetaVar "V") (TName "values")]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-delete" [TVar "TM",TSet [TVar "TI"]]) [VPMetaVar "TM'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "set-unite" [TApp "set-difference" [TVar "ATS",TSet [TVar "TI"]],TSet [TVar "TI*"]]) [VPMetaVar "ATS'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-unite" [TVar "TVM",TMap [TBinding (TVar "TI") (TVar "V")]]) [VPMetaVar "TVM'"]) env + putMutTerm "active-thread-set" (TVar "ATS'") env + putMutTerm "thread-stepping" (TSeq []) env + putMutTerm "thread-map" (TVar "TM'") env + putMutTerm "terminated-thread-map" (TVar "TVM'") env + stepTermTo (TName "null-value") env + +thread_atomic_ fargs = FApp "thread-atomic" (fargs) +stepThread_atomic fargs = + evalRules [] [step1,step2,step3,step4,step5,step6] + where step1 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getControlPatt "abrupted" (Nothing) env + putMutTerm "store" (TVar "Sigma") env + putMutTerm "active-thread-set" (TVar "ATS") env + putMutTerm "thread-stepping" (TVar "TI") env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) + env <- receiveSignalPatt __varabrupted (Nothing) env + env <- getMutPatt "store" [VPMetaVar "Sigma'"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS'"] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI'"] env + putMutTerm "store" (TVar "Sigma'") env + putMutTerm "active-thread-set" (TVar "ATS'") env + putMutTerm "thread-stepping" (TVar "TI'") env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TApp "thread-atomic" [TVar "X'"]) [PMetaVar "V"] env)) + env <- receiveSignalPatt __varabrupted (Nothing) env + env <- getMutPatt "store" [VPMetaVar "Sigma''"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS''"] env + env <- getMutPatt "thread-stepping" [VPSeqVar "TI''?" QuestionMarkOp] env + putMutTerm "store" (TVar "Sigma''") env + putMutTerm "active-thread-set" (TVar "ATS''") env + putMutTerm "thread-stepping" (TVar "TI''?") env + stepTermTo (TVar "V") env + step2 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getMutPatt "store" [VPMetaVar "Sigma"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getControlPatt "abrupted" (Just (VPMetaVar "A")) env + putMutTerm "store" (TVar "Sigma") env + putMutTerm "active-thread-set" (TVar "ATS") env + putMutTerm "thread-stepping" (TVar "TI") env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) + env <- receiveSignalPatt __varabrupted (Nothing) env + env <- getMutPatt "store" [VPMetaVar "Sigma'"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS'"] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI'"] env + putMutTerm "store" (TVar "Sigma'") env + putMutTerm "active-thread-set" (TVar "ATS'") env + putMutTerm "thread-stepping" (TVar "TI'") env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "A")) env (premise (TApp "thread-atomic" [TVar "X'"]) [PMetaVar "V"] env)) + env <- receiveSignalPatt __varabrupted (Just (VPMetaVar "A")) env + env <- getMutPatt "store" [VPMetaVar "Sigma''"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS''"] env + env <- getMutPatt "thread-stepping" [VPSeqVar "TI''?" QuestionMarkOp] env + raiseTerm "abrupted" (TVar "A") env + putMutTerm "store" (TVar "Sigma''") env + putMutTerm "active-thread-set" (TVar "ATS''") env + putMutTerm "thread-stepping" (TVar "TI''?") env + stepTermTo (TVar "V") env + step3 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getControlPatt "abrupted" (Just (VPMetaVar "A")) env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "A")) env (premise (TVar "X") [PMetaVar "X'"] env)) + env <- receiveSignalPatt __varabrupted (Just (VPMetaVar "A")) env + raiseTerm "abrupted" (TVar "A") env + stepTermTo (TApp "thread-atomic" [TVar "X'"]) env + step4 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getControlPatt "abrupted" (Nothing) env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PAnnotated (PMetaVar "V") (TName "values")] env)) + env <- receiveSignalPatt __varabrupted (Nothing) env + stepTermTo (TVar "V") env + step5 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getControlPatt "abrupted" (Just (VPMetaVar "A")) env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "A")) env (premise (TVar "X") [PAnnotated (PMetaVar "V") (TName "values")] env)) + env <- receiveSignalPatt __varabrupted (Just (VPMetaVar "A")) env + raiseTerm "abrupted" (TVar "A") env + stepTermTo (TApp "thread-atomic" [TVar "V"]) env + step6 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PAnnotated (PMetaVar "V") (TName "values")] env + stepTermTo (TVar "V") env + +thread_yield_ fargs = FApp "thread-yield" (fargs) +stepThread_yield fargs = + evalRules [] [step1,step2,step3] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [] env + putMutTerm "thread-stepping" (TSeq []) env + stepTermTo (TName "null-value") env + step2 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI") (TName "thread-ids")] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "TI",TVar "ATS"]) (TName "true")) env + putMutTerm "thread-stepping" (TVar "TI") env + stepTermTo (TName "null-value") env + step3 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI") (TName "thread-ids")] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "TI",TVar "ATS"]) (TName "false")) env + stepTermTo (TName "fail") env + +thread_spin_ fargs = FApp "thread-spin" (fargs) +stepThread_spin fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- fsMatch fargs [PMetaVar "X"] env + rewriteTermTo (TApp "else" [TVar "X",TApp "sequential" [TApp "thread-yield" [],TApp "thread-spin" [TVar "X"]]]) env + +thread_suspend_ fargs = FApp "thread-suspend" (fargs) +stepThread_suspend fargs = + evalRules [] [step1,step2] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPSeqVar "TI+" PlusOp) (TSortSeq (TName "thread-ids") PlusOp)] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "TI",TSet [TVar "TI+"]]) (TName "false")) env + env <- lifted_sideCondition (SCEquality (TApp "is-subset" [TSet [TVar "TI+"],TVar "ATS"]) (TName "true")) env + env <- lifted_sideCondition (SCPatternMatch (TApp "set-difference" [TVar "ATS",TSet [TVar "TI+"]]) [VPMetaVar "ATS'"]) env + putMutTerm "thread-stepping" (TVar "TI") env + putMutTerm "active-thread-set" (TVar "ATS'") env + stepTermTo (TName "null-value") env + step2 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPSeqVar "TI+" PlusOp) (TSortSeq (TName "thread-ids") PlusOp)] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "TI",TSet [TVar "TI+"]]) (TName "true")) env + env <- lifted_sideCondition (SCEquality (TApp "is-subset" [TSet [TVar "TI+"],TVar "ATS"]) (TName "true")) env + env <- lifted_sideCondition (SCPatternMatch (TApp "set-difference" [TVar "ATS",TSet [TVar "TI+"]]) [VPMetaVar "ATS'"]) env + putMutTerm "thread-stepping" (TSeq []) env + putMutTerm "active-thread-set" (TVar "ATS'") env + stepTermTo (TName "null-value") env + +thread_resume_ fargs = FApp "thread-resume" (fargs) +stepThread_resume fargs = + evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPSeqVar "TI*" StarOp) (TSortSeq (TName "thread-ids") StarOp)] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "TI",TSet [TVar "TI*"]]) (TName "false")) env + env <- lifted_sideCondition (SCEquality (TApp "set-intersect" [TVar "ATS",TSet [TVar "TI*"]]) (TSet [])) env + env <- lifted_sideCondition (SCPatternMatch (TApp "set-unite" [TVar "ATS",TSet [TVar "TI*"]]) [VPMetaVar "ATS'"]) env + putMutTerm "thread-stepping" (TVar "TI") env + putMutTerm "active-thread-set" (TVar "ATS'") env + stepTermTo (TName "null-value") env + +thread_terminate_ fargs = FApp "thread-terminate" (fargs) +stepThread_terminate fargs = + evalRules [] [step1,step2] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI'") (TName "thread-ids")] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "TM",TVar "TI'"]) [PADT "thread" [PADT "thunk" [PADT "abstraction" [VPMetaVar "X"]]]]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-delete" [TVar "TM",TSet [TVar "TI'"]]) [VPMetaVar "TM'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "set-difference" [TVar "ATS",TSet [TVar "TI'"]]) [VPMetaVar "ATS'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "when-true" [TApp "not" [TApp "is-equal" [TVar "TI",TVar "TI'"]],TVar "TI"]) [VPSeqVar "TI?" QuestionMarkOp]) env + putMutTerm "thread-stepping" (TVar "TI?") env + putMutTerm "thread-map" (TVar "TM'") env + putMutTerm "active-thread-set" (TVar "ATS'") env + stepTermTo (TName "null-value") env + step2 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI'") (TName "thread-ids"),VPAnnotated (VPMetaVar "V") (TName "values")] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + env <- getMutPatt "terminated-thread-map" [VPMetaVar "TVM"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "TM",TVar "TI'"]) [PADT "thread" [PADT "thunk" [PADT "abstraction" [VPMetaVar "X"]],PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),VPSeqVar "TI*" StarOp]]]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-delete" [TVar "TM",TSet [TVar "TI'"]]) [VPMetaVar "TM'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "set-unite" [TApp "set-difference" [TVar "ATS",TSet [TVar "TI'"]],TSet [TVar "TI*"]]) [VPMetaVar "ATS'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-unite" [TVar "TVM",TMap [TBinding (TVar "TI'") (TVar "V")]]) [VPMetaVar "TVM'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "when-true" [TApp "not" [TApp "is-equal" [TVar "TI",TVar "TI'"]],TVar "TI"]) [VPSeqVar "TI?" QuestionMarkOp]) env + putMutTerm "thread-stepping" (TVar "TI?") env + putMutTerm "thread-map" (TVar "TM'") env + putMutTerm "terminated-thread-map" (TVar "TVM'") env + putMutTerm "active-thread-set" (TVar "ATS'") env + stepTermTo (TName "null-value") env + +is_thread_terminated_ fargs = FApp "is-thread-terminated" (fargs) +stepIs_thread_terminated fargs = + evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI") (TName "thread-ids")] env + env <- getMutPatt "terminated-thread-map" [VPMetaVar "TVM"] env + stepTermTo (TApp "is-value" [TApp "map-lookup" [TVar "TVM",TVar "TI"]]) env + +thread_value_ fargs = FApp "thread-value" (fargs) +stepThread_value fargs = + evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI") (TName "thread-ids")] env + env <- getMutPatt "terminated-thread-map" [VPMetaVar "TVM"] env + stepTermTo (TApp "checked" [TApp "map-lookup" [TVar "TVM",TVar "TI"]]) env + +thread_join_ fargs = FApp "thread-join" (fargs) +stepThread_join fargs = + evalRules [] [step1,step2,step3,step4] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI'") (TName "thread-ids")] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "TM",TVar "TI'"]) [PADT "thread" [VPMetaVar "TH",PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),VPSeqVar "TI*" StarOp]]]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-override" [TMap [TBinding (TVar "TI'") (TApp "thread" [TVar "TH",TApp "list" [TVar "TI*",TVar "TI"]])],TVar "TM"]) [VPMetaVar "TM'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "set-difference" [TVar "ATS",TSet [TVar "TI"]]) [VPMetaVar "ATS'"]) env + putMutTerm "thread-map" (TVar "TM'") env + putMutTerm "thread-stepping" (TSeq []) env + putMutTerm "active-thread-set" (TVar "ATS'") env + stepTermTo (TName "null-value") env + step2 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI'") (TName "thread-ids")] env + env <- getMutPatt "terminated-thread-map" [VPMetaVar "TVM"] env + env <- lifted_sideCondition (SCEquality (TApp "is-value" [TApp "lookup" [TVar "TVM",TVar "TI'"]]) (TName "true")) env + stepTermTo (TName "null-value") env + step3 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI'") (TName "thread-ids")] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "TM",TVar "TI'"]) [PADT "thread" [VPMetaVar "TH"]]) env + stepTermTo (TName "fail") env + step4 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI'") (TName "thread-ids")] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + env <- getMutPatt "terminated-thread-map" [VPMetaVar "TVM"] env + env <- lifted_sideCondition (SCEquality (TApp "lookup" [TVar "TM",TVar "TI'"]) (TSeq [])) env + env <- lifted_sideCondition (SCEquality (TApp "lookup" [TVar "TVM",TVar "TI'"]) (TSeq [])) env + stepTermTo (TName "fail") env + +thread_exterminate_ fargs = FApp "thread-exterminate" (fargs) +stepThread_exterminate fargs = + evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "TI'") (TName "thread-ids")] env + env <- getMutPatt "thread-map" [VPMetaVar "TM"] env + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getMutPatt "terminated-thread-map" [VPMetaVar "TVM"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- lifted_sideCondition (SCInequality (TVar "TI'") (TVar "TI")) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-delete" [TVar "TM",TSet [TVar "TI'"]]) [VPMetaVar "TM'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-delete" [TVar "TVM",TSet [TVar "TI'"]]) [VPMetaVar "TVM'"]) env + env <- lifted_sideCondition (SCPatternMatch (TApp "set-difference" [TVar "ATS",TSet [TVar "TI'"]]) [VPMetaVar "ATS'"]) env + putMutTerm "thread-map" (TVar "TM'") env + putMutTerm "thread-stepping" (TVar "TI") env + putMutTerm "terminated-thread-map" (TVar "TVM'") env + putMutTerm "active-thread-set" (TVar "ATS'") env + stepTermTo (TName "null-value") env + +update_thread_stepping_ = FName "update-thread-stepping" +stepUpdate_thread_stepping = evalRules [] [step1,step2,step3,step4] + where step1 = do + let env = emptyEnv + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- premise (TApp "is-thread-preemptible" [TVar "TI"]) [PValue (PADT "false" [])] env + stepTermTo (TName "null-value") env + step2 = do + let env = emptyEnv + env <- getMutPatt "thread-stepping" [VPMetaVar "TI"] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- premise (TApp "is-thread-preemptible" [TVar "TI"]) [PValue (PADT "true" [])] env + env <- lifted_sideCondition (SCPatternMatch (TApp "some-element" [TVar "ATS"]) [VPMetaVar "TI'"]) env + putMutTerm "thread-stepping" (TVar "TI'") env + stepTermTo (TName "null-value") env + step3 = do + let env = emptyEnv + env <- getMutPatt "thread-stepping" [] env + env <- getMutPatt "active-thread-set" [VPMetaVar "ATS"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "some-element" [TVar "ATS"]) [VPMetaVar "TI'"]) env + putMutTerm "thread-stepping" (TVar "TI'") env + stepTermTo (TName "null-value") env + step4 = do + let env = emptyEnv + env <- getMutPatt "thread-stepping" [VPSeqVar "TI?" QuestionMarkOp] env + env <- getMutPatt "active-thread-set" [PADT "set" []] env + putMutTerm "thread-stepping" (TSeq []) env + stepTermTo (TName "null-value") env + +update_thread_schedule_ fargs = FApp "update-thread-schedule" (fargs) +stepUpdate_thread_schedule fargs = + evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "VS") (TApp "sets" [TName "ground-values"])] env + putMutTerm "thread-schedule" (TVar "VS") env + stepTermTo (TName "null-value") env + +current_thread_schedule_ = FName "current-thread-schedule" +stepCurrent_thread_schedule = evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- getMutPatt "thread-schedule" [VPMetaVar "VS"] env + stepTermTo (TVar "VS") env + +thread_preemptible_ = FName "thread-preemptible" +stepThread_preemptible = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 104)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 100)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 112)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 109)]),FValue (ADTVal "unicode-character" [FValue (Int 112)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 98)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 101)])]))]) env + +thread_cooperative_ = FName "thread-cooperative" +stepThread_cooperative = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 104)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 100)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 112)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 118)]),FValue (ADTVal "unicode-character" [FValue (Int 101)])]))]) env + +is_thread_preemptible_ fargs = FApp "is-thread-preemptible" (fargs) +stepIs_thread_preemptible fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated VPWildCard (TName "thread-ids")] env + rewriteTermTo (TApp "not" [TApp "is-in-set" [TName "thread-cooperative",TName "current-thread-schedule"]]) env + +thread_ids_ = FName "thread-ids" +stepThread_ids = rewriteType "thread-ids" [] + +threads_ = FName "threads" +stepThreads = rewriteType "threads" [] + +thread_preemtibilities_ = FName "thread-preemtibilities" +stepThread_preemtibilities = rewriteType "thread-preemtibilities" [] diff --git a/cbs/Funcons/Core/Computations/Threads/Synchronising/Locks/Locks.hs b/cbs/Funcons/Core/Computations/Threads/Synchronising/Locks/Locks.hs new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Computations/Threads/Synchronising/Locks/Locks.hs @@ -0,0 +1,215 @@ +-- GeNeRaTeD fOr: /home/thomas/repos/plancomps/CBS-beta/Unstable-Funcons-beta/Computations/Threads/Synchronising/Locks/Locks.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Computations.Threads.Synchronising.Locks.Locks where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) +entities = [] + +types = typeEnvFromList + [] + +funcons = libFromList + [("is-exclusive-lock-holder",StrictFuncon stepIs_exclusive_lock_holder),("spin-lock-create",NullaryFuncon stepSpin_lock_create),("spin-lock-sync",StrictFuncon stepSpin_lock_sync),("spin-lock-release",StrictFuncon stepSpin_lock_release),("exclusive-lock-create",NullaryFuncon stepExclusive_lock_create),("exclusive-lock-sync",StrictFuncon stepExclusive_lock_sync),("exclusive-lock-sync-else-wait",StrictFuncon stepExclusive_lock_sync_else_wait),("exclusive-lock-release",StrictFuncon stepExclusive_lock_release),("reentrant-lock-create",NullaryFuncon stepReentrant_lock_create),("reentrant-lock-sync",StrictFuncon stepReentrant_lock_sync),("reentrant-lock-sync-else-wait",StrictFuncon stepReentrant_lock_sync_else_wait),("reentrant-lock-release",StrictFuncon stepReentrant_lock_release),("reentrant-lock-exit",StrictFuncon stepReentrant_lock_exit),("semaphore-create",StrictFuncon stepSemaphore_create),("semaphore-sync",StrictFuncon stepSemaphore_sync),("semaphore-sync-else-wait",StrictFuncon stepSemaphore_sync_else_wait),("semaphore-release",StrictFuncon stepSemaphore_release),("rw-lock-create",NullaryFuncon stepRw_lock_create),("rw-lock-sync-exclusive",StrictFuncon stepRw_lock_sync_exclusive),("rw-lock-sync-shared",StrictFuncon stepRw_lock_sync_shared),("rw-lock-sync-exclusive-else-wait",StrictFuncon stepRw_lock_sync_exclusive_else_wait),("rw-lock-sync-shared-else-wait",StrictFuncon stepRw_lock_sync_shared_else_wait),("rw-lock-release-exclusive",StrictFuncon stepRw_lock_release_exclusive),("rw-lock-release-shared",StrictFuncon stepRw_lock_release_shared),("rw-lock-sync",StrictFuncon stepRw_lock_sync),("rw-lock-sync-all-shared",StrictFuncon stepRw_lock_sync_all_shared)] + +is_exclusive_lock_holder_ fargs = FApp "is-exclusive-lock-holder" (fargs) +stepIs_exclusive_lock_holder fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "is-equal" [TName "current-thread",TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-holder"]]]) env + +spin_lock_create_ = FName "spin-lock-create" +stepSpin_lock_create = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "sync-create" [TApp "sync-feature-create" [TName "sync-held"],TApp "sync-feature-create" [TName "sync-holder"]]) env + +spin_lock_sync_ fargs = FApp "spin-lock-sync" (fargs) +stepSpin_lock_sync fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "check-true" [TApp "not" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-held"]]]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-held"],TName "true"],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-holder"],TName "current-thread"]]]) env + +spin_lock_release_ fargs = FApp "spin-lock-release" (fargs) +stepSpin_lock_release fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "check-true" [TApp "is-exclusive-lock-holder" [TVar "SY"]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-held"],TName "false"],TApp "un-assign" [TApp "sync-feature" [TVar "SY",TName "sync-holder"]]]]) env + +exclusive_lock_create_ = FName "exclusive-lock-create" +stepExclusive_lock_create = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "sync-create" [TApp "sync-feature-create" [TName "sync-waiting-list"],TApp "sync-feature-create" [TName "sync-held"],TApp "sync-feature-create" [TName "sync-holder"]]) env + +exclusive_lock_sync_ fargs = FApp "exclusive-lock-sync" (fargs) +stepExclusive_lock_sync fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "check-true" [TApp "not" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-held"]]]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-held"],TName "true"],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-holder"],TName "current-thread"]]]) env + +exclusive_lock_sync_else_wait_ fargs = FApp "exclusive-lock-sync-else-wait" (fargs) +stepExclusive_lock_sync_else_wait fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "else" [TApp "exclusive-lock-sync" [TVar "SY"],TApp "sequential" [TApp "sync-waiting-list-add" [TVar "SY",TName "current-thread"],TApp "thread-suspend" [TName "current-thread"]]]]) env + +exclusive_lock_release_ fargs = FApp "exclusive-lock-release" (fargs) +stepExclusive_lock_release fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "check-true" [TApp "is-exclusive-lock-holder" [TVar "SY"]],TApp "if-true-else" [TApp "is-equal" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"]],TApp "list" []],TApp "sequential" [TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-held"],TName "false"],TApp "un-assign" [TApp "sync-feature" [TVar "SY",TName "sync-holder"]]],TApp "give" [TApp "sync-waiting-list-head-remove" [TVar "SY"],TApp "sequential" [TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-holder"],TName "given"],TApp "thread-resume" [TName "given"]]]]]]) env + +reentrant_lock_create_ = FName "reentrant-lock-create" +stepReentrant_lock_create = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "sync-create" [TApp "sync-feature-create" [TName "sync-waiting-list"],TApp "sync-feature-create" [TName "sync-held"],TApp "sync-feature-create" [TName "sync-holder"],TApp "sync-feature-create" [TName "sync-count"]]) env + +reentrant_lock_sync_ fargs = FApp "reentrant-lock-sync" (fargs) +stepReentrant_lock_sync fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "else" [TApp "sequential" [TApp "check-true" [TApp "not" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-held"]]]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-held"],TName "true"],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-holder"],TName "current-thread"],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TFuncon (FValue (Nat 0))]],TApp "sequential" [TApp "check-true" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-held"]]],TApp "check-true" [TApp "is-exclusive-lock-holder" [TVar "SY"]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TApp "nat-succ" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-count"]]]]]]]) env + +reentrant_lock_sync_else_wait_ fargs = FApp "reentrant-lock-sync-else-wait" (fargs) +stepReentrant_lock_sync_else_wait fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "else" [TApp "reentrant-lock-sync" [TVar "SY"],TApp "sequential" [TApp "sync-waiting-list-add" [TVar "SY",TName "current-thread"],TApp "thread-suspend" [TName "current-thread"]]]]) env + +reentrant_lock_release_ fargs = FApp "reentrant-lock-release" (fargs) +stepReentrant_lock_release fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "check-true" [TApp "is-exclusive-lock-holder" [TVar "SY"]],TApp "if-true-else" [TApp "is-equal" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"]],TApp "list" []],TApp "sequential" [TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-held"],TName "false"],TApp "un-assign" [TApp "sync-feature" [TVar "SY",TName "sync-holder"]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TFuncon (FValue (Nat 0))]],TApp "give" [TApp "sync-waiting-list-head-remove" [TVar "SY"],TApp "sequential" [TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-holder"],TName "given"],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TFuncon (FValue (Nat 0))],TApp "thread-resume" [TName "given"]]]]]]) env + +reentrant_lock_exit_ fargs = FApp "reentrant-lock-exit" (fargs) +stepReentrant_lock_exit fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "check-true" [TApp "is-exclusive-lock-holder" [TVar "SY"]],TApp "give" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TApp "if-true-else" [TApp "is-greater" [TApp "assigned" [TName "given"],TFuncon (FValue (Nat 0))],TApp "assign" [TName "given",TApp "checked" [TApp "nat-pred" [TApp "assigned" [TName "given"]]]],TApp "reentrant-lock-release" [TVar "SY"]]]]]) env + +semaphore_create_ fargs = FApp "semaphore-create" (fargs) +stepSemaphore_create fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints")] env + rewriteTermTo (TApp "give" [TApp "sync-create" [TApp "sync-feature-create" [TName "sync-waiting-list"],TApp "sync-feature-create" [TName "sync-count"]],TApp "sequential" [TApp "assign" [TApp "sync-feature" [TName "given",TName "sync-count"],TVar "N"],TName "given"]]) env + +semaphore_sync_ fargs = FApp "semaphore-sync" (fargs) +stepSemaphore_sync fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "check-true" [TApp "is-greater" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-count"]],TFuncon (FValue (Nat 0))]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TApp "checked" [TApp "nat-pred" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-count"]]]]]]]) env + +semaphore_sync_else_wait_ fargs = FApp "semaphore-sync-else-wait" (fargs) +stepSemaphore_sync_else_wait fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "else" [TApp "semaphore-sync" [TVar "SY"],TApp "sequential" [TApp "sync-waiting-list-add" [TVar "SY",TName "current-thread"],TApp "thread-suspend" [TName "current-thread"]]]]) env + +semaphore_release_ fargs = FApp "semaphore-release" (fargs) +stepSemaphore_release fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "if-true-else" [TApp "is-equal" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"]],TApp "list" []],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TApp "nat-succ" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-count"]]]],TApp "give" [TApp "sync-waiting-list-head-remove" [TVar "SY"],TApp "thread-resume" [TName "given"]]]]) env + +rw_lock_create_ = FName "rw-lock-create" +stepRw_lock_create = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "give" [TApp "sync-create" [TApp "sync-feature-create" [TName "sync-waiting-list"],TApp "sync-feature-create" [TName "sync-held"],TApp "sync-feature-create" [TName "sync-count"]],TApp "sequential" [TApp "assign" [TApp "sync-feature" [TName "given",TName "sync-count"],TFuncon (FValue (Nat 0))],TName "given"]]) env + +rw_lock_sync_exclusive_ fargs = FApp "rw-lock-sync-exclusive" (fargs) +stepRw_lock_sync_exclusive fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "check-true" [TApp "and" [TApp "not" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-held"]]],TApp "is-equal" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-count"]],TFuncon (FValue (Nat 0))]]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-held"],TName "true"]]]) env + +rw_lock_sync_shared_ fargs = FApp "rw-lock-sync-shared" (fargs) +stepRw_lock_sync_shared fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "check-true" [TApp "not" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-held"]]]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TApp "nat-succ" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-count"]]]]]]) env + +rw_lock_sync_exclusive_else_wait_ fargs = FApp "rw-lock-sync-exclusive-else-wait" (fargs) +stepRw_lock_sync_exclusive_else_wait fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "else" [TApp "rw-lock-sync-exclusive" [TVar "SY"],TApp "sequential" [TApp "sync-waiting-list-add" [TVar "SY",TApp "tuple" [TName "current-thread",TName "false"]],TApp "thread-suspend" [TName "current-thread"]]]]) env + +rw_lock_sync_shared_else_wait_ fargs = FApp "rw-lock-sync-shared-else-wait" (fargs) +stepRw_lock_sync_shared_else_wait fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "else" [TApp "rw-lock-sync-shared" [TVar "SY"],TApp "sequential" [TApp "sync-waiting-list-add" [TVar "SY",TApp "tuple" [TName "current-thread",TName "true"]],TApp "thread-suspend" [TName "current-thread"]]]]) env + +rw_lock_release_exclusive_ fargs = FApp "rw-lock-release-exclusive" (fargs) +stepRw_lock_release_exclusive fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "check-true" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-held"]]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-held"],TName "false"],TApp "rw-lock-sync" [TVar "SY"]]]) env + +rw_lock_release_shared_ fargs = FApp "rw-lock-release-shared" (fargs) +stepRw_lock_release_shared fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TApp "checked" [TApp "nat-pred" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-count"]]]]],TApp "if-true-else" [TApp "is-equal" [TFuncon (FValue (Nat 0)),TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-count"]]],TApp "rw-lock-sync" [TVar "SY"],TName "null-value"]]]) env + +rw_lock_sync_ fargs = FApp "rw-lock-sync" (fargs) +stepRw_lock_sync fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "if-true-else" [TApp "is-equal" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"]],TApp "list" []],TName "null-value",TApp "give" [TApp "sync-waiting-list-head-remove" [TVar "SY"],TApp "sequential" [TApp "thread-resume" [TApp "first" [TApp "tuple-elements" [TName "given"]]],TApp "if-true-else" [TApp "second" [TApp "tuple-elements" [TName "given"]],TApp "sequential" [TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TApp "nat-succ" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-count"]]]],TApp "rw-lock-sync-all-shared" [TVar "SY"]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-held"],TName "true"]]]]]) env + +rw_lock_sync_all_shared_ fargs = FApp "rw-lock-sync-all-shared" (fargs) +stepRw_lock_sync_all_shared fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"],TApp "list" [TApp "left-to-right-filter" [TApp "if-true-else" [TApp "second" [TApp "tuple-elements" [TName "given"]],TApp "sequential" [TApp "thread-resume" [TApp "first" [TApp "tuple-elements" [TName "given"]]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TApp "nat-succ" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-count"]]]],TName "false"],TName "true"],TApp "list-elements" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"]]]]]]) env diff --git a/cbs/Funcons/Core/Computations/Threads/Synchronising/Notifications/Notifications.hs b/cbs/Funcons/Core/Computations/Threads/Synchronising/Notifications/Notifications.hs new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Computations/Threads/Synchronising/Notifications/Notifications.hs @@ -0,0 +1,143 @@ +-- GeNeRaTeD fOr: /home/thomas/repos/plancomps/CBS-beta/Unstable-Funcons-beta/Computations/Threads/Synchronising/Notifications/Notifications.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Computations.Threads.Synchronising.Notifications.Notifications where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) +entities = [] + +types = typeEnvFromList + [] + +funcons = libFromList + [("barrier-create",StrictFuncon stepBarrier_create),("barrier-sync",StrictFuncon stepBarrier_sync),("barrier-sync-else-wait",StrictFuncon stepBarrier_sync_else_wait),("condition-create",NullaryFuncon stepCondition_create),("condition-wait",StrictFuncon stepCondition_wait),("condition-wait-with-lock",StrictFuncon stepCondition_wait_with_lock),("condition-notify-all",StrictFuncon stepCondition_notify_all),("condition-notify-first",StrictFuncon stepCondition_notify_first),("rendezvous-create",StrictFuncon stepRendezvous_create),("rendezvous-sync",StrictFuncon stepRendezvous_sync),("rendezvous-sync-else-wait",StrictFuncon stepRendezvous_sync_else_wait),("rendezvous-waits",NullaryFuncon stepRendezvous_waits),("is-rendezvous-match",StrictFuncon stepIs_rendezvous_match),("rendezvous-first-match-thread",StrictFuncon stepRendezvous_first_match_thread),("rendezvous-first-match-drop",StrictFuncon stepRendezvous_first_match_drop)] + +barrier_create_ fargs = FApp "barrier-create" (fargs) +stepBarrier_create fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints")] env + rewriteTermTo (TApp "give" [TApp "sync-create" [TApp "sync-feature-create" [TName "sync-waiting-list"],TApp "sync-feature-create" [TName "sync-count"]],TApp "sequential" [TApp "assign" [TApp "sync-feature" [TName "given",TName "sync-count"],TVar "N"],TName "given"]]) env + +barrier_sync_ fargs = FApp "barrier-sync" (fargs) +stepBarrier_sync fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "give" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TApp "else" [TApp "check-true" [TApp "is-equal" [TApp "assigned" [TName "given"],TFuncon (FValue (Nat 0))]],TApp "sequential" [TApp "check-true" [TApp "is-equal" [TApp "assigned" [TName "given"],TFuncon (FValue (Nat 1))]],TApp "assign" [TName "given",TFuncon (FValue (Nat 0))],TApp "thread-resume" [TApp "list-elements" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"]]]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"],TApp "list" []]]]]]) env + +barrier_sync_else_wait_ fargs = FApp "barrier-sync-else-wait" (fargs) +stepBarrier_sync_else_wait fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "else" [TApp "barrier-sync" [TVar "SY"],TApp "sequential" [TApp "sync-waiting-list-add" [TVar "SY",TName "current-thread"],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-count"],TApp "checked" [TApp "nat-pred" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-count"]]]]],TApp "thread-suspend" [TName "current-thread"]]]]) env + +condition_create_ = FName "condition-create" +stepCondition_create = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "sync-create" [TApp "sync-feature-create" [TName "sync-waiting-list"]]) env + +condition_wait_ fargs = FApp "condition-wait" (fargs) +stepCondition_wait fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "sync-waiting-list-add" [TVar "SY",TName "current-thread"],TApp "thread-suspend" [TName "current-thread"]]]) env + +condition_wait_with_lock_ fargs = FApp "condition-wait-with-lock" (fargs) +stepCondition_wait_with_lock fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs"),VPAnnotated (VPMetaVar "L") (TName "syncs")] env + rewriteTermTo (TApp "sequential" [TApp "thread-atomic" [TApp "sequential" [TApp "exclusive-lock-release" [TVar "L"],TApp "sync-waiting-list-add" [TVar "SY",TName "current-thread"],TApp "thread-suspend" [TName "current-thread"]]],TApp "exclusive-lock-sync-else-wait" [TVar "L"]]) env + +condition_notify_all_ fargs = FApp "condition-notify-all" (fargs) +stepCondition_notify_all fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "sequential" [TApp "thread-resume" [TApp "list-elements" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"]]]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"],TApp "list" []]]]) env + +condition_notify_first_ fargs = FApp "condition-notify-first" (fargs) +stepCondition_notify_first fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "thread-atomic" [TApp "give" [TApp "sync-waiting-list-head-remove" [TVar "SY"],TApp "thread-resume" [TName "given"]]]) env + +rendezvous_create_ fargs = FApp "rendezvous-create" (fargs) +stepRendezvous_create fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints")] env + rewriteTermTo (TApp "give" [TApp "sync-create" [TApp "sync-feature-create" [TName "sync-waiting-list"],TApp "sync-feature-create" [TName "sync-count"]],TApp "sequential" [TApp "assign" [TApp "sync-feature" [TName "given",TName "sync-count"],TVar "N"],TName "given"]]) env + +rendezvous_sync_ fargs = FApp "rendezvous-sync" (fargs) +stepRendezvous_sync fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs"),VPAnnotated (VPMetaVar "V") (TName "ground-values")] env + rewriteTermTo (TApp "give" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"]],TApp "sequential" [TApp "check-true" [TApp "is-rendezvous-match" [TName "given",TVar "V"]],TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"],TApp "rendezvous-first-match-drop" [TName "given",TVar "V"]],TApp "thread-resume" [TApp "rendezvous-first-match-thread" [TName "given",TVar "V"]]]]) env + +rendezvous_sync_else_wait_ fargs = FApp "rendezvous-sync-else-wait" (fargs) +stepRendezvous_sync_else_wait fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs"),VPAnnotated (VPMetaVar "V") (TName "ground-values")] env + rewriteTermTo (TApp "thread-atomic" [TApp "else" [TApp "rendezvous-sync" [TVar "SY",TVar "V"],TApp "sequential" [TApp "sync-waiting-list-add" [TVar "SY",TApp "tuple" [TVar "V",TName "current-thread"]],TApp "thread-suspend" [TName "current-thread"]]]]) env + +rendezvous_waits_ = FName "rendezvous-waits" +stepRendezvous_waits = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "tuples" [TName "ground-values",TName "thread-ids"]) env + +is_rendezvous_match_ fargs = FApp "is-rendezvous-match" (fargs) +stepIs_rendezvous_match fargs = + evalRules [rewrite1,rewrite2] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),PADT "tuple" [VPMetaVar "V'",VPMetaVar "TI"],VPSeqVar "P*" StarOp],VPAnnotated (VPMetaVar "V") (TName "values")] env + rewriteTermTo (TApp "if-true-else" [TApp "is-equal" [TVar "V'",TVar "V"],TName "true",TApp "is-rendezvous-match" [TApp "list" [TVar "P*"],TVar "V"]]) env + rewrite2 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])])],VPAnnotated (VPMetaVar "V") (TName "values")] env + rewriteTermTo (TName "false") env + +rendezvous_first_match_thread_ fargs = FApp "rendezvous-first-match-thread" (fargs) +stepRendezvous_first_match_thread fargs = + evalRules [rewrite1,rewrite2] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),PADT "tuple" [VPMetaVar "V'",VPMetaVar "TI"],VPSeqVar "P*" StarOp],VPAnnotated (VPMetaVar "V") (TName "values")] env + rewriteTermTo (TApp "if-true-else" [TApp "is-equal" [TVar "V'",TVar "V"],TVar "TI",TApp "rendezvous-first-match-thread" [TApp "list" [TVar "P*"],TVar "V"]]) env + rewrite2 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])])],VPAnnotated (VPMetaVar "V") (TName "values")] env + rewriteTermTo (TName "fail") env + +rendezvous_first_match_drop_ fargs = FApp "rendezvous-first-match-drop" (fargs) +stepRendezvous_first_match_drop fargs = + evalRules [rewrite1,rewrite2] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),PADT "tuple" [VPMetaVar "V'",VPMetaVar "TI"],VPSeqVar "P*" StarOp],VPAnnotated (VPMetaVar "V") (TName "values")] env + rewriteTermTo (TApp "if-true-else" [TApp "is-equal" [TVar "V'",TVar "V"],TApp "list" [TVar "P*"],TApp "cons" [TApp "tuple" [TVar "V'",TVar "TI"],TApp "rendezvous-first-match-drop" [TApp "list" [TVar "P*"],TVar "V"]]]) env + rewrite2 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])])],VPAnnotated (VPMetaVar "V") (TName "values")] env + rewriteTermTo (TName "fail") env diff --git a/cbs/Funcons/Core/Computations/Threads/Synchronising/Synchronising.hs b/cbs/Funcons/Core/Computations/Threads/Synchronising/Synchronising.hs new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Computations/Threads/Synchronising/Synchronising.hs @@ -0,0 +1,120 @@ +-- GeNeRaTeD fOr: /home/thomas/repos/plancomps/CBS-beta/Unstable-Funcons-beta/Computations/Threads/Synchronising/Synchronising.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Computations.Threads.Synchronising.Synchronising where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) +entities = [] + +types = typeEnvFromList + [("syncs",DataTypeMemberss "syncs" [] [DataTypeMemberConstructor "sync" [TName "sync-feature-maps"] (Just [])]),("sync-features",DataTypeMemberss "sync-features" [] [DataTypeMemberConstructor "sync-waiting-list" [] (Just []),DataTypeMemberConstructor "sync-held" [] (Just []),DataTypeMemberConstructor "sync-holder" [] (Just []),DataTypeMemberConstructor "sync-count" [] (Just [])])] + +funcons = libFromList + [("sync",StrictFuncon stepSync),("sync-create",StrictFuncon stepSync_create),("sync-feature",StrictFuncon stepSync_feature),("is-sync-feature",StrictFuncon stepIs_sync_feature),("sync-waiting-list",NullaryFuncon stepSync_waiting_list),("sync-held",NullaryFuncon stepSync_held),("sync-holder",NullaryFuncon stepSync_holder),("sync-count",NullaryFuncon stepSync_count),("sync-feature-maps",NullaryFuncon stepSync_feature_maps),("sync-feature-create",StrictFuncon stepSync_feature_create),("sync-waiting-list-add",StrictFuncon stepSync_waiting_list_add),("sync-waiting-list-head-remove",StrictFuncon stepSync_waiting_list_head_remove),("syncs",NullaryFuncon stepSyncs),("sync-features",NullaryFuncon stepSync_features)] + +sync_ fargs = FApp "sync" (fargs) +stepSync fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPMetaVar "_X1"] env + env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 121)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 99)])])),TVar "_X1"]) env + +sync_create_ fargs = FApp "sync-create" (fargs) +stepSync_create fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPSeqVar "M+" PlusOp) (TSortSeq (TName "sync-feature-maps") PlusOp)] env + rewriteTermTo (TApp "sync" [TApp "checked" [TApp "map-unite" [TVar "M+"]]]) env + +sync_feature_ fargs = FApp "sync-feature" (fargs) +stepSync_feature fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "sync" [VPAnnotated (VPMetaVar "SFM") (TName "sync-feature-maps")],VPAnnotated (VPMetaVar "SF") (TName "sync-features")] env + rewriteTermTo (TApp "checked" [TApp "map-lookup" [TVar "SFM",TVar "SF"]]) env + +is_sync_feature_ fargs = FApp "is-sync-feature" (fargs) +stepIs_sync_feature fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "sync" [VPAnnotated (VPMetaVar "SFM") (TName "sync-feature-maps")],VPAnnotated (VPMetaVar "SF") (TName "sync-features")] env + rewriteTermTo (TApp "is-in-set" [TVar "SF",TApp "dom" [TVar "SFM"]]) env + +sync_waiting_list_ = FName "sync-waiting-list" +stepSync_waiting_list = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 121)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 119)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 103)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]))]) env + +sync_held_ = FName "sync-held" +stepSync_held = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 121)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 104)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 100)])]))]) env + +sync_holder_ = FName "sync-holder" +stepSync_holder = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 121)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 104)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 100)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 114)])]))]) env + +sync_count_ = FName "sync-count" +stepSync_count = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 121)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]))]) env + +sync_feature_maps_ = FName "sync-feature-maps" +stepSync_feature_maps = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "maps" [TName "sync-features",TName "values"]) env + +sync_feature_create_ fargs = FApp "sync-feature-create" (fargs) +stepSync_feature_create fargs = + evalRules [rewrite1,rewrite2,rewrite3,rewrite4] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "sync-waiting-list" []] env + rewriteTermTo (TMap [TBinding (TName "sync-waiting-list") (TApp "allocate-initialised-variable" [TApp "lists" [TName "values"],TApp "list" []])]) env + rewrite2 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "sync-held" []] env + rewriteTermTo (TMap [TBinding (TName "sync-held") (TApp "allocate-initialised-variable" [TName "booleans",TName "false"])]) env + rewrite3 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "sync-holder" []] env + rewriteTermTo (TMap [TBinding (TName "sync-holder") (TApp "allocate-variable" [TName "thread-ids"])]) env + rewrite4 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "sync-count" []] env + rewriteTermTo (TMap [TBinding (TName "sync-count") (TApp "allocate-initialised-variable" [TName "nats",TFuncon (FValue (Nat 0))])]) env + +sync_waiting_list_add_ fargs = FApp "sync-waiting-list-add" (fargs) +stepSync_waiting_list_add fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs"),VPAnnotated (VPMetaVar "V") (TName "values")] env + rewriteTermTo (TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"],TApp "list-append" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"]],TApp "list" [TVar "V"]]]) env + +sync_waiting_list_head_remove_ fargs = FApp "sync-waiting-list-head-remove" (fargs) +stepSync_waiting_list_head_remove fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "SY") (TName "syncs")] env + rewriteTermTo (TApp "give" [TApp "checked" [TApp "list-head" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"]]]],TApp "sequential" [TApp "assign" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"],TApp "checked" [TApp "list-tail" [TApp "assigned" [TApp "sync-feature" [TVar "SY",TName "sync-waiting-list"]]]]],TName "given"]]) env + +syncs_ = FName "syncs" +stepSyncs = rewriteType "syncs" [] + +sync_features_ = FName "sync-features" +stepSync_features = rewriteType "sync-features" [] diff --git a/cbs/Funcons/Core/Library.hs b/cbs/Funcons/Core/Library.hs --- a/cbs/Funcons/Core/Library.hs +++ b/cbs/Funcons/Core/Library.hs @@ -1,253 +1,295 @@ module Funcons.Core.Library ( funcons, entities, types, - module Funcons.Core.Computations.Normal.Interacting.Interacting, - module Funcons.Core.Computations.Normal.Flowing.Flowing, - module Funcons.Core.Computations.Normal.Storing.Storing, - module Funcons.Core.Computations.Normal.Linking.Linking, - module Funcons.Core.Computations.Normal.Giving.Giving, - module Funcons.Core.Computations.Normal.Generating.Generating, - module Funcons.Core.Computations.Normal.Binding.Binding, + module Funcons.Core.Computations.Threads.Synchronising.Locks.Locks, + module Funcons.Core.Computations.Threads.Synchronising.Synchronising, + module Funcons.Core.Computations.Threads.Synchronising.Notifications.Notifications, + module Funcons.Core.Computations.Threads.Multithreading.Multithreading, + module Funcons.Core.Computations.Abnormal.Failing.Failing, + module Funcons.Core.Computations.Abnormal.Postponing.Postponing, + module Funcons.Core.Computations.Abnormal.Continuing.Continuing, module Funcons.Core.Computations.Abnormal.Abrupting.Abrupting, module Funcons.Core.Computations.Abnormal.Returning.Returning, - module Funcons.Core.Computations.Abnormal.Controlling.Controlling, - module Funcons.Core.Computations.Abnormal.Throwing.Throwing, - module Funcons.Core.Computations.Abnormal.Failing.Failing, module Funcons.Core.Computations.Abnormal.Sticking, + module Funcons.Core.Computations.Abnormal.Throwing.Throwing, + module Funcons.Core.Computations.Abnormal.Controlling.Controlling, module Funcons.Core.Computations.Abnormal.Breaking.Breaking, - module Funcons.Core.Computations.Abnormal.Continuing.Continuing, - module Funcons.Core.Values.Composite.ASTs.ASTs, - module Funcons.Core.Values.Composite.Records.Records, - module Funcons.Core.Values.Composite.Strings.Strings, + module Funcons.Core.Computations.Normal.Linking.Linking, + module Funcons.Core.Computations.Normal.Binding.Binding, + module Funcons.Core.Computations.Normal.Giving.Giving, + module Funcons.Core.Computations.Normal.Indexing.Indexing, + module Funcons.Core.Computations.Normal.Flowing.Flowing, + module Funcons.Core.Computations.Normal.Generating.Generating, + module Funcons.Core.Computations.Normal.Memos.Memos, + module Funcons.Core.Computations.Normal.Interacting.Interacting, + module Funcons.Core.Computations.Normal.Storing.Storing, + module Funcons.Core.Values.Primitive.Characters.Characters, + module Funcons.Core.Values.Primitive.Booleans.Booleans, + module Funcons.Core.Values.Primitive.Null.Null, + module Funcons.Core.Values.Primitive.Integers.Integers, + module Funcons.Core.Values.Primitive.Floats.Floats, + module Funcons.Core.Values.Abstraction.Functions.Functions, + module Funcons.Core.Values.Abstraction.Thunks.Thunks, + module Funcons.Core.Values.Abstraction.Generic.Generic, + module Funcons.Core.Values.Abstraction.Patterns.Patterns, + module Funcons.Core.Values.ValueTypes.ValueTypes, + module Funcons.Core.Values.Composite.Bits.Bits, + module Funcons.Core.Values.Composite.Objects.Objects, module Funcons.Core.Values.Composite.References.References, + module Funcons.Core.Values.Composite.Datatypes.Datatypes, + module Funcons.Core.Values.Composite.Records.Records, module Funcons.Core.Values.Composite.Graphs.Graphs, + module Funcons.Core.Values.Composite.Sequences.Sequences, module Funcons.Core.Values.Composite.Vectors.Vectors, - module Funcons.Core.Values.Composite.Variants.Variants, module Funcons.Core.Values.Composite.Trees.Trees, - module Funcons.Core.Values.Composite.Sequences.Sequences, module Funcons.Core.Values.Composite.Lists.Lists, - module Funcons.Core.Values.Composite.Classes.Classes, - module Funcons.Core.Values.Composite.Objects.Objects, - module Funcons.Core.Values.Composite.Datatypes.Datatypes, module Funcons.Core.Values.Composite.Tuples.Tuples, - module Funcons.Core.Values.Composite.Bits.Bits, - module Funcons.Core.Values.Primitive.Floats.Floats, - module Funcons.Core.Values.Primitive.Booleans.Booleans, - module Funcons.Core.Values.Primitive.Null.Null, - module Funcons.Core.Values.Primitive.Characters.Characters, - module Funcons.Core.Values.Primitive.Integers.Integers, - module Funcons.Core.Values.ValueTypes.ValueTypes, - module Funcons.Core.Values.Abstraction.Thunks.Thunks, - module Funcons.Core.Values.Abstraction.Patterns.Patterns, - module Funcons.Core.Values.Abstraction.Functions.Functions, - module Funcons.Core.Values.Abstraction.Generic.Generic, + module Funcons.Core.Values.Composite.Variants.Variants, + module Funcons.Core.Values.Composite.Strings.Strings, + module Funcons.Core.Values.Composite.Classes.Classes, + module Funcons.Core.Values.Composite.ASTs.ASTs, ) where import Funcons.EDSL -import Funcons.Core.Computations.Normal.Interacting.Interacting hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Normal.Interacting.Interacting -import Funcons.Core.Computations.Normal.Flowing.Flowing hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Normal.Flowing.Flowing -import Funcons.Core.Computations.Normal.Storing.Storing hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Normal.Storing.Storing -import Funcons.Core.Computations.Normal.Linking.Linking hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Normal.Linking.Linking -import Funcons.Core.Computations.Normal.Giving.Giving hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Normal.Giving.Giving -import Funcons.Core.Computations.Normal.Generating.Generating hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Normal.Generating.Generating -import Funcons.Core.Computations.Normal.Binding.Binding hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Normal.Binding.Binding +import Funcons.Core.Computations.Threads.Synchronising.Locks.Locks hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Threads.Synchronising.Locks.Locks +import Funcons.Core.Computations.Threads.Synchronising.Synchronising hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Threads.Synchronising.Synchronising +import Funcons.Core.Computations.Threads.Synchronising.Notifications.Notifications hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Threads.Synchronising.Notifications.Notifications +import Funcons.Core.Computations.Threads.Multithreading.Multithreading hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Threads.Multithreading.Multithreading +import Funcons.Core.Computations.Abnormal.Failing.Failing hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Abnormal.Failing.Failing +import Funcons.Core.Computations.Abnormal.Postponing.Postponing hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Abnormal.Postponing.Postponing +import Funcons.Core.Computations.Abnormal.Continuing.Continuing hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Abnormal.Continuing.Continuing import Funcons.Core.Computations.Abnormal.Abrupting.Abrupting hiding (funcons,types,entities) import qualified Funcons.Core.Computations.Abnormal.Abrupting.Abrupting import Funcons.Core.Computations.Abnormal.Returning.Returning hiding (funcons,types,entities) import qualified Funcons.Core.Computations.Abnormal.Returning.Returning -import Funcons.Core.Computations.Abnormal.Controlling.Controlling hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Abnormal.Controlling.Controlling -import Funcons.Core.Computations.Abnormal.Throwing.Throwing hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Abnormal.Throwing.Throwing -import Funcons.Core.Computations.Abnormal.Failing.Failing hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Abnormal.Failing.Failing import Funcons.Core.Computations.Abnormal.Sticking hiding (funcons,types,entities) import qualified Funcons.Core.Computations.Abnormal.Sticking +import Funcons.Core.Computations.Abnormal.Throwing.Throwing hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Abnormal.Throwing.Throwing +import Funcons.Core.Computations.Abnormal.Controlling.Controlling hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Abnormal.Controlling.Controlling import Funcons.Core.Computations.Abnormal.Breaking.Breaking hiding (funcons,types,entities) import qualified Funcons.Core.Computations.Abnormal.Breaking.Breaking -import Funcons.Core.Computations.Abnormal.Continuing.Continuing hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Abnormal.Continuing.Continuing -import Funcons.Core.Values.Composite.ASTs.ASTs hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.ASTs.ASTs -import Funcons.Core.Values.Composite.Records.Records hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Records.Records -import Funcons.Core.Values.Composite.Strings.Strings hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Strings.Strings +import Funcons.Core.Computations.Normal.Linking.Linking hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Normal.Linking.Linking +import Funcons.Core.Computations.Normal.Binding.Binding hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Normal.Binding.Binding +import Funcons.Core.Computations.Normal.Giving.Giving hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Normal.Giving.Giving +import Funcons.Core.Computations.Normal.Indexing.Indexing hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Normal.Indexing.Indexing +import Funcons.Core.Computations.Normal.Flowing.Flowing hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Normal.Flowing.Flowing +import Funcons.Core.Computations.Normal.Generating.Generating hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Normal.Generating.Generating +import Funcons.Core.Computations.Normal.Memos.Memos hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Normal.Memos.Memos +import Funcons.Core.Computations.Normal.Interacting.Interacting hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Normal.Interacting.Interacting +import Funcons.Core.Computations.Normal.Storing.Storing hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Normal.Storing.Storing +import Funcons.Core.Values.Primitive.Characters.Characters hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Primitive.Characters.Characters +import Funcons.Core.Values.Primitive.Booleans.Booleans hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Primitive.Booleans.Booleans +import Funcons.Core.Values.Primitive.Null.Null hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Primitive.Null.Null +import Funcons.Core.Values.Primitive.Integers.Integers hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Primitive.Integers.Integers +import Funcons.Core.Values.Primitive.Floats.Floats hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Primitive.Floats.Floats +import Funcons.Core.Values.Abstraction.Functions.Functions hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Abstraction.Functions.Functions +import Funcons.Core.Values.Abstraction.Thunks.Thunks hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Abstraction.Thunks.Thunks +import Funcons.Core.Values.Abstraction.Generic.Generic hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Abstraction.Generic.Generic +import Funcons.Core.Values.Abstraction.Patterns.Patterns hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Abstraction.Patterns.Patterns +import Funcons.Core.Values.ValueTypes.ValueTypes hiding (funcons,types,entities) +import qualified Funcons.Core.Values.ValueTypes.ValueTypes +import Funcons.Core.Values.Composite.Bits.Bits hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Bits.Bits +import Funcons.Core.Values.Composite.Objects.Objects hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Objects.Objects import Funcons.Core.Values.Composite.References.References hiding (funcons,types,entities) import qualified Funcons.Core.Values.Composite.References.References +import Funcons.Core.Values.Composite.Datatypes.Datatypes hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Datatypes.Datatypes +import Funcons.Core.Values.Composite.Records.Records hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Records.Records import Funcons.Core.Values.Composite.Graphs.Graphs hiding (funcons,types,entities) import qualified Funcons.Core.Values.Composite.Graphs.Graphs +import Funcons.Core.Values.Composite.Sequences.Sequences hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Sequences.Sequences import Funcons.Core.Values.Composite.Vectors.Vectors hiding (funcons,types,entities) import qualified Funcons.Core.Values.Composite.Vectors.Vectors -import Funcons.Core.Values.Composite.Variants.Variants hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Variants.Variants import Funcons.Core.Values.Composite.Trees.Trees hiding (funcons,types,entities) import qualified Funcons.Core.Values.Composite.Trees.Trees -import Funcons.Core.Values.Composite.Sequences.Sequences hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Sequences.Sequences import Funcons.Core.Values.Composite.Lists.Lists hiding (funcons,types,entities) import qualified Funcons.Core.Values.Composite.Lists.Lists -import Funcons.Core.Values.Composite.Classes.Classes hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Classes.Classes -import Funcons.Core.Values.Composite.Objects.Objects hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Objects.Objects -import Funcons.Core.Values.Composite.Datatypes.Datatypes hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Datatypes.Datatypes import Funcons.Core.Values.Composite.Tuples.Tuples hiding (funcons,types,entities) import qualified Funcons.Core.Values.Composite.Tuples.Tuples -import Funcons.Core.Values.Composite.Bits.Bits hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Bits.Bits -import Funcons.Core.Values.Primitive.Floats.Floats hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Primitive.Floats.Floats -import Funcons.Core.Values.Primitive.Booleans.Booleans hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Primitive.Booleans.Booleans -import Funcons.Core.Values.Primitive.Null.Null hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Primitive.Null.Null -import Funcons.Core.Values.Primitive.Characters.Characters hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Primitive.Characters.Characters -import Funcons.Core.Values.Primitive.Integers.Integers hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Primitive.Integers.Integers -import Funcons.Core.Values.ValueTypes.ValueTypes hiding (funcons,types,entities) -import qualified Funcons.Core.Values.ValueTypes.ValueTypes -import Funcons.Core.Values.Abstraction.Thunks.Thunks hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Abstraction.Thunks.Thunks -import Funcons.Core.Values.Abstraction.Patterns.Patterns hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Abstraction.Patterns.Patterns -import Funcons.Core.Values.Abstraction.Functions.Functions hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Abstraction.Functions.Functions -import Funcons.Core.Values.Abstraction.Generic.Generic hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Abstraction.Generic.Generic +import Funcons.Core.Values.Composite.Variants.Variants hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Variants.Variants +import Funcons.Core.Values.Composite.Strings.Strings hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Strings.Strings +import Funcons.Core.Values.Composite.Classes.Classes hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Classes.Classes +import Funcons.Core.Values.Composite.ASTs.ASTs hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.ASTs.ASTs funcons = libUnions [ - Funcons.Core.Computations.Normal.Interacting.Interacting.funcons - , Funcons.Core.Computations.Normal.Flowing.Flowing.funcons - , Funcons.Core.Computations.Normal.Storing.Storing.funcons - , Funcons.Core.Computations.Normal.Linking.Linking.funcons - , Funcons.Core.Computations.Normal.Giving.Giving.funcons - , Funcons.Core.Computations.Normal.Generating.Generating.funcons - , Funcons.Core.Computations.Normal.Binding.Binding.funcons + Funcons.Core.Computations.Threads.Synchronising.Locks.Locks.funcons + , Funcons.Core.Computations.Threads.Synchronising.Synchronising.funcons + , Funcons.Core.Computations.Threads.Synchronising.Notifications.Notifications.funcons + , Funcons.Core.Computations.Threads.Multithreading.Multithreading.funcons + , Funcons.Core.Computations.Abnormal.Failing.Failing.funcons + , Funcons.Core.Computations.Abnormal.Postponing.Postponing.funcons + , Funcons.Core.Computations.Abnormal.Continuing.Continuing.funcons , Funcons.Core.Computations.Abnormal.Abrupting.Abrupting.funcons , Funcons.Core.Computations.Abnormal.Returning.Returning.funcons - , Funcons.Core.Computations.Abnormal.Controlling.Controlling.funcons - , Funcons.Core.Computations.Abnormal.Throwing.Throwing.funcons - , Funcons.Core.Computations.Abnormal.Failing.Failing.funcons , Funcons.Core.Computations.Abnormal.Sticking.funcons + , Funcons.Core.Computations.Abnormal.Throwing.Throwing.funcons + , Funcons.Core.Computations.Abnormal.Controlling.Controlling.funcons , Funcons.Core.Computations.Abnormal.Breaking.Breaking.funcons - , Funcons.Core.Computations.Abnormal.Continuing.Continuing.funcons - , Funcons.Core.Values.Composite.ASTs.ASTs.funcons - , Funcons.Core.Values.Composite.Records.Records.funcons - , Funcons.Core.Values.Composite.Strings.Strings.funcons + , Funcons.Core.Computations.Normal.Linking.Linking.funcons + , Funcons.Core.Computations.Normal.Binding.Binding.funcons + , Funcons.Core.Computations.Normal.Giving.Giving.funcons + , Funcons.Core.Computations.Normal.Indexing.Indexing.funcons + , Funcons.Core.Computations.Normal.Flowing.Flowing.funcons + , Funcons.Core.Computations.Normal.Generating.Generating.funcons + , Funcons.Core.Computations.Normal.Memos.Memos.funcons + , Funcons.Core.Computations.Normal.Interacting.Interacting.funcons + , Funcons.Core.Computations.Normal.Storing.Storing.funcons + , Funcons.Core.Values.Primitive.Characters.Characters.funcons + , Funcons.Core.Values.Primitive.Booleans.Booleans.funcons + , Funcons.Core.Values.Primitive.Null.Null.funcons + , Funcons.Core.Values.Primitive.Integers.Integers.funcons + , Funcons.Core.Values.Primitive.Floats.Floats.funcons + , Funcons.Core.Values.Abstraction.Functions.Functions.funcons + , Funcons.Core.Values.Abstraction.Thunks.Thunks.funcons + , Funcons.Core.Values.Abstraction.Generic.Generic.funcons + , Funcons.Core.Values.Abstraction.Patterns.Patterns.funcons + , Funcons.Core.Values.ValueTypes.ValueTypes.funcons + , Funcons.Core.Values.Composite.Bits.Bits.funcons + , Funcons.Core.Values.Composite.Objects.Objects.funcons , Funcons.Core.Values.Composite.References.References.funcons + , Funcons.Core.Values.Composite.Datatypes.Datatypes.funcons + , Funcons.Core.Values.Composite.Records.Records.funcons , Funcons.Core.Values.Composite.Graphs.Graphs.funcons + , Funcons.Core.Values.Composite.Sequences.Sequences.funcons , Funcons.Core.Values.Composite.Vectors.Vectors.funcons - , Funcons.Core.Values.Composite.Variants.Variants.funcons , Funcons.Core.Values.Composite.Trees.Trees.funcons - , Funcons.Core.Values.Composite.Sequences.Sequences.funcons , Funcons.Core.Values.Composite.Lists.Lists.funcons - , Funcons.Core.Values.Composite.Classes.Classes.funcons - , Funcons.Core.Values.Composite.Objects.Objects.funcons - , Funcons.Core.Values.Composite.Datatypes.Datatypes.funcons , Funcons.Core.Values.Composite.Tuples.Tuples.funcons - , Funcons.Core.Values.Composite.Bits.Bits.funcons - , Funcons.Core.Values.Primitive.Floats.Floats.funcons - , Funcons.Core.Values.Primitive.Booleans.Booleans.funcons - , Funcons.Core.Values.Primitive.Null.Null.funcons - , Funcons.Core.Values.Primitive.Characters.Characters.funcons - , Funcons.Core.Values.Primitive.Integers.Integers.funcons - , Funcons.Core.Values.ValueTypes.ValueTypes.funcons - , Funcons.Core.Values.Abstraction.Thunks.Thunks.funcons - , Funcons.Core.Values.Abstraction.Patterns.Patterns.funcons - , Funcons.Core.Values.Abstraction.Functions.Functions.funcons - , Funcons.Core.Values.Abstraction.Generic.Generic.funcons + , Funcons.Core.Values.Composite.Variants.Variants.funcons + , Funcons.Core.Values.Composite.Strings.Strings.funcons + , Funcons.Core.Values.Composite.Classes.Classes.funcons + , Funcons.Core.Values.Composite.ASTs.ASTs.funcons ] entities = concat [ - Funcons.Core.Computations.Normal.Interacting.Interacting.entities - , Funcons.Core.Computations.Normal.Flowing.Flowing.entities - , Funcons.Core.Computations.Normal.Storing.Storing.entities - , Funcons.Core.Computations.Normal.Linking.Linking.entities - , Funcons.Core.Computations.Normal.Giving.Giving.entities - , Funcons.Core.Computations.Normal.Generating.Generating.entities - , Funcons.Core.Computations.Normal.Binding.Binding.entities + Funcons.Core.Computations.Threads.Synchronising.Locks.Locks.entities + , Funcons.Core.Computations.Threads.Synchronising.Synchronising.entities + , Funcons.Core.Computations.Threads.Synchronising.Notifications.Notifications.entities + , Funcons.Core.Computations.Threads.Multithreading.Multithreading.entities + , Funcons.Core.Computations.Abnormal.Failing.Failing.entities + , Funcons.Core.Computations.Abnormal.Postponing.Postponing.entities + , Funcons.Core.Computations.Abnormal.Continuing.Continuing.entities , Funcons.Core.Computations.Abnormal.Abrupting.Abrupting.entities , Funcons.Core.Computations.Abnormal.Returning.Returning.entities - , Funcons.Core.Computations.Abnormal.Controlling.Controlling.entities - , Funcons.Core.Computations.Abnormal.Throwing.Throwing.entities - , Funcons.Core.Computations.Abnormal.Failing.Failing.entities , Funcons.Core.Computations.Abnormal.Sticking.entities + , Funcons.Core.Computations.Abnormal.Throwing.Throwing.entities + , Funcons.Core.Computations.Abnormal.Controlling.Controlling.entities , Funcons.Core.Computations.Abnormal.Breaking.Breaking.entities - , Funcons.Core.Computations.Abnormal.Continuing.Continuing.entities - , Funcons.Core.Values.Composite.ASTs.ASTs.entities - , Funcons.Core.Values.Composite.Records.Records.entities - , Funcons.Core.Values.Composite.Strings.Strings.entities + , Funcons.Core.Computations.Normal.Linking.Linking.entities + , Funcons.Core.Computations.Normal.Binding.Binding.entities + , Funcons.Core.Computations.Normal.Giving.Giving.entities + , Funcons.Core.Computations.Normal.Indexing.Indexing.entities + , Funcons.Core.Computations.Normal.Flowing.Flowing.entities + , Funcons.Core.Computations.Normal.Generating.Generating.entities + , Funcons.Core.Computations.Normal.Memos.Memos.entities + , Funcons.Core.Computations.Normal.Interacting.Interacting.entities + , Funcons.Core.Computations.Normal.Storing.Storing.entities + , Funcons.Core.Values.Primitive.Characters.Characters.entities + , Funcons.Core.Values.Primitive.Booleans.Booleans.entities + , Funcons.Core.Values.Primitive.Null.Null.entities + , Funcons.Core.Values.Primitive.Integers.Integers.entities + , Funcons.Core.Values.Primitive.Floats.Floats.entities + , Funcons.Core.Values.Abstraction.Functions.Functions.entities + , Funcons.Core.Values.Abstraction.Thunks.Thunks.entities + , Funcons.Core.Values.Abstraction.Generic.Generic.entities + , Funcons.Core.Values.Abstraction.Patterns.Patterns.entities + , Funcons.Core.Values.ValueTypes.ValueTypes.entities + , Funcons.Core.Values.Composite.Bits.Bits.entities + , Funcons.Core.Values.Composite.Objects.Objects.entities , Funcons.Core.Values.Composite.References.References.entities + , Funcons.Core.Values.Composite.Datatypes.Datatypes.entities + , Funcons.Core.Values.Composite.Records.Records.entities , Funcons.Core.Values.Composite.Graphs.Graphs.entities + , Funcons.Core.Values.Composite.Sequences.Sequences.entities , Funcons.Core.Values.Composite.Vectors.Vectors.entities - , Funcons.Core.Values.Composite.Variants.Variants.entities , Funcons.Core.Values.Composite.Trees.Trees.entities - , Funcons.Core.Values.Composite.Sequences.Sequences.entities , Funcons.Core.Values.Composite.Lists.Lists.entities - , Funcons.Core.Values.Composite.Classes.Classes.entities - , Funcons.Core.Values.Composite.Objects.Objects.entities - , Funcons.Core.Values.Composite.Datatypes.Datatypes.entities , Funcons.Core.Values.Composite.Tuples.Tuples.entities - , Funcons.Core.Values.Composite.Bits.Bits.entities - , Funcons.Core.Values.Primitive.Floats.Floats.entities - , Funcons.Core.Values.Primitive.Booleans.Booleans.entities - , Funcons.Core.Values.Primitive.Null.Null.entities - , Funcons.Core.Values.Primitive.Characters.Characters.entities - , Funcons.Core.Values.Primitive.Integers.Integers.entities - , Funcons.Core.Values.ValueTypes.ValueTypes.entities - , Funcons.Core.Values.Abstraction.Thunks.Thunks.entities - , Funcons.Core.Values.Abstraction.Patterns.Patterns.entities - , Funcons.Core.Values.Abstraction.Functions.Functions.entities - , Funcons.Core.Values.Abstraction.Generic.Generic.entities + , Funcons.Core.Values.Composite.Variants.Variants.entities + , Funcons.Core.Values.Composite.Strings.Strings.entities + , Funcons.Core.Values.Composite.Classes.Classes.entities + , Funcons.Core.Values.Composite.ASTs.ASTs.entities ] types = typeEnvUnions [ - Funcons.Core.Computations.Normal.Interacting.Interacting.types - , Funcons.Core.Computations.Normal.Flowing.Flowing.types - , Funcons.Core.Computations.Normal.Storing.Storing.types - , Funcons.Core.Computations.Normal.Linking.Linking.types - , Funcons.Core.Computations.Normal.Giving.Giving.types - , Funcons.Core.Computations.Normal.Generating.Generating.types - , Funcons.Core.Computations.Normal.Binding.Binding.types + Funcons.Core.Computations.Threads.Synchronising.Locks.Locks.types + , Funcons.Core.Computations.Threads.Synchronising.Synchronising.types + , Funcons.Core.Computations.Threads.Synchronising.Notifications.Notifications.types + , Funcons.Core.Computations.Threads.Multithreading.Multithreading.types + , Funcons.Core.Computations.Abnormal.Failing.Failing.types + , Funcons.Core.Computations.Abnormal.Postponing.Postponing.types + , Funcons.Core.Computations.Abnormal.Continuing.Continuing.types , Funcons.Core.Computations.Abnormal.Abrupting.Abrupting.types , Funcons.Core.Computations.Abnormal.Returning.Returning.types - , Funcons.Core.Computations.Abnormal.Controlling.Controlling.types - , Funcons.Core.Computations.Abnormal.Throwing.Throwing.types - , Funcons.Core.Computations.Abnormal.Failing.Failing.types , Funcons.Core.Computations.Abnormal.Sticking.types + , Funcons.Core.Computations.Abnormal.Throwing.Throwing.types + , Funcons.Core.Computations.Abnormal.Controlling.Controlling.types , Funcons.Core.Computations.Abnormal.Breaking.Breaking.types - , Funcons.Core.Computations.Abnormal.Continuing.Continuing.types - , Funcons.Core.Values.Composite.ASTs.ASTs.types - , Funcons.Core.Values.Composite.Records.Records.types - , Funcons.Core.Values.Composite.Strings.Strings.types + , Funcons.Core.Computations.Normal.Linking.Linking.types + , Funcons.Core.Computations.Normal.Binding.Binding.types + , Funcons.Core.Computations.Normal.Giving.Giving.types + , Funcons.Core.Computations.Normal.Indexing.Indexing.types + , Funcons.Core.Computations.Normal.Flowing.Flowing.types + , Funcons.Core.Computations.Normal.Generating.Generating.types + , Funcons.Core.Computations.Normal.Memos.Memos.types + , Funcons.Core.Computations.Normal.Interacting.Interacting.types + , Funcons.Core.Computations.Normal.Storing.Storing.types + , Funcons.Core.Values.Primitive.Characters.Characters.types + , Funcons.Core.Values.Primitive.Booleans.Booleans.types + , Funcons.Core.Values.Primitive.Null.Null.types + , Funcons.Core.Values.Primitive.Integers.Integers.types + , Funcons.Core.Values.Primitive.Floats.Floats.types + , Funcons.Core.Values.Abstraction.Functions.Functions.types + , Funcons.Core.Values.Abstraction.Thunks.Thunks.types + , Funcons.Core.Values.Abstraction.Generic.Generic.types + , Funcons.Core.Values.Abstraction.Patterns.Patterns.types + , Funcons.Core.Values.ValueTypes.ValueTypes.types + , Funcons.Core.Values.Composite.Bits.Bits.types + , Funcons.Core.Values.Composite.Objects.Objects.types , Funcons.Core.Values.Composite.References.References.types + , Funcons.Core.Values.Composite.Datatypes.Datatypes.types + , Funcons.Core.Values.Composite.Records.Records.types , Funcons.Core.Values.Composite.Graphs.Graphs.types + , Funcons.Core.Values.Composite.Sequences.Sequences.types , Funcons.Core.Values.Composite.Vectors.Vectors.types - , Funcons.Core.Values.Composite.Variants.Variants.types , Funcons.Core.Values.Composite.Trees.Trees.types - , Funcons.Core.Values.Composite.Sequences.Sequences.types , Funcons.Core.Values.Composite.Lists.Lists.types - , Funcons.Core.Values.Composite.Classes.Classes.types - , Funcons.Core.Values.Composite.Objects.Objects.types - , Funcons.Core.Values.Composite.Datatypes.Datatypes.types , Funcons.Core.Values.Composite.Tuples.Tuples.types - , Funcons.Core.Values.Composite.Bits.Bits.types - , Funcons.Core.Values.Primitive.Floats.Floats.types - , Funcons.Core.Values.Primitive.Booleans.Booleans.types - , Funcons.Core.Values.Primitive.Null.Null.types - , Funcons.Core.Values.Primitive.Characters.Characters.types - , Funcons.Core.Values.Primitive.Integers.Integers.types - , Funcons.Core.Values.ValueTypes.ValueTypes.types - , Funcons.Core.Values.Abstraction.Thunks.Thunks.types - , Funcons.Core.Values.Abstraction.Patterns.Patterns.types - , Funcons.Core.Values.Abstraction.Functions.Functions.types - , Funcons.Core.Values.Abstraction.Generic.Generic.types + , Funcons.Core.Values.Composite.Variants.Variants.types + , Funcons.Core.Values.Composite.Strings.Strings.types + , Funcons.Core.Values.Composite.Classes.Classes.types + , Funcons.Core.Values.Composite.ASTs.ASTs.types ] diff --git a/cbs/Funcons/Core/Values/Abstraction/Functions/Functions.hs b/cbs/Funcons/Core/Values/Abstraction/Functions/Functions.hs --- a/cbs/Funcons/Core/Values/Abstraction/Functions/Functions.hs +++ b/cbs/Funcons/Core/Values/Abstraction/Functions/Functions.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Abstraction/Functions/Functions.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Abstraction/Functions/Functions.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Abstraction.Functions.Functions where diff --git a/cbs/Funcons/Core/Values/Abstraction/Generic/Generic.hs b/cbs/Funcons/Core/Values/Abstraction/Generic/Generic.hs --- a/cbs/Funcons/Core/Values/Abstraction/Generic/Generic.hs +++ b/cbs/Funcons/Core/Values/Abstraction/Generic/Generic.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Abstraction/Generic/Generic.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Abstraction/Generic/Generic.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Abstraction.Generic.Generic where diff --git a/cbs/Funcons/Core/Values/Abstraction/Patterns/Patterns.hs b/cbs/Funcons/Core/Values/Abstraction/Patterns/Patterns.hs --- a/cbs/Funcons/Core/Values/Abstraction/Patterns/Patterns.hs +++ b/cbs/Funcons/Core/Values/Abstraction/Patterns/Patterns.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Abstraction/Patterns/Patterns.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Abstraction/Patterns/Patterns.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Abstraction.Patterns.Patterns where diff --git a/cbs/Funcons/Core/Values/Abstraction/Thunks/Thunks.hs b/cbs/Funcons/Core/Values/Abstraction/Thunks/Thunks.hs --- a/cbs/Funcons/Core/Values/Abstraction/Thunks/Thunks.hs +++ b/cbs/Funcons/Core/Values/Abstraction/Thunks/Thunks.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Abstraction/Thunks/Thunks.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Abstraction/Thunks/Thunks.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Abstraction.Thunks.Thunks where diff --git a/cbs/Funcons/Core/Values/Composite/Bits/Bits.hs b/cbs/Funcons/Core/Values/Composite/Bits/Bits.hs --- a/cbs/Funcons/Core/Values/Composite/Bits/Bits.hs +++ b/cbs/Funcons/Core/Values/Composite/Bits/Bits.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Bits/Bits.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Bits/Bits.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Bits.Bits where diff --git a/cbs/Funcons/Core/Values/Composite/Classes/Classes.hs b/cbs/Funcons/Core/Values/Composite/Classes/Classes.hs --- a/cbs/Funcons/Core/Values/Composite/Classes/Classes.hs +++ b/cbs/Funcons/Core/Values/Composite/Classes/Classes.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Classes/Classes.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Classes/Classes.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Classes.Classes where diff --git a/cbs/Funcons/Core/Values/Composite/Datatypes/Datatypes.hs b/cbs/Funcons/Core/Values/Composite/Datatypes/Datatypes.hs --- a/cbs/Funcons/Core/Values/Composite/Datatypes/Datatypes.hs +++ b/cbs/Funcons/Core/Values/Composite/Datatypes/Datatypes.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Datatypes/Datatypes.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Datatypes/Datatypes.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Datatypes.Datatypes where diff --git a/cbs/Funcons/Core/Values/Composite/Graphs/Graphs.hs b/cbs/Funcons/Core/Values/Composite/Graphs/Graphs.hs --- a/cbs/Funcons/Core/Values/Composite/Graphs/Graphs.hs +++ b/cbs/Funcons/Core/Values/Composite/Graphs/Graphs.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Graphs/Graphs.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Graphs/Graphs.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Graphs.Graphs where diff --git a/cbs/Funcons/Core/Values/Composite/Lists/Lists.hs b/cbs/Funcons/Core/Values/Composite/Lists/Lists.hs --- a/cbs/Funcons/Core/Values/Composite/Lists/Lists.hs +++ b/cbs/Funcons/Core/Values/Composite/Lists/Lists.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Lists/Lists.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Lists/Lists.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Lists.Lists where diff --git a/cbs/Funcons/Core/Values/Composite/Objects/Objects.hs b/cbs/Funcons/Core/Values/Composite/Objects/Objects.hs --- a/cbs/Funcons/Core/Values/Composite/Objects/Objects.hs +++ b/cbs/Funcons/Core/Values/Composite/Objects/Objects.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Objects/Objects.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Objects/Objects.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Objects.Objects where diff --git a/cbs/Funcons/Core/Values/Composite/Records/Records.hs b/cbs/Funcons/Core/Values/Composite/Records/Records.hs --- a/cbs/Funcons/Core/Values/Composite/Records/Records.hs +++ b/cbs/Funcons/Core/Values/Composite/Records/Records.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Records/Records.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Records/Records.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Records.Records where diff --git a/cbs/Funcons/Core/Values/Composite/References/References.hs b/cbs/Funcons/Core/Values/Composite/References/References.hs --- a/cbs/Funcons/Core/Values/Composite/References/References.hs +++ b/cbs/Funcons/Core/Values/Composite/References/References.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/References/References.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/References/References.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.References.References where diff --git a/cbs/Funcons/Core/Values/Composite/Sequences/Sequences.hs b/cbs/Funcons/Core/Values/Composite/Sequences/Sequences.hs --- a/cbs/Funcons/Core/Values/Composite/Sequences/Sequences.hs +++ b/cbs/Funcons/Core/Values/Composite/Sequences/Sequences.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Sequences/Sequences.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Sequences/Sequences.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Sequences.Sequences where diff --git a/cbs/Funcons/Core/Values/Composite/Strings/Strings.hs b/cbs/Funcons/Core/Values/Composite/Strings/Strings.hs --- a/cbs/Funcons/Core/Values/Composite/Strings/Strings.hs +++ b/cbs/Funcons/Core/Values/Composite/Strings/Strings.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Strings/Strings.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Strings/Strings.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Strings.Strings where diff --git a/cbs/Funcons/Core/Values/Composite/Trees/Trees.hs b/cbs/Funcons/Core/Values/Composite/Trees/Trees.hs --- a/cbs/Funcons/Core/Values/Composite/Trees/Trees.hs +++ b/cbs/Funcons/Core/Values/Composite/Trees/Trees.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Trees/Trees.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Trees/Trees.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Trees.Trees where diff --git a/cbs/Funcons/Core/Values/Composite/Tuples/Tuples.hs b/cbs/Funcons/Core/Values/Composite/Tuples/Tuples.hs --- a/cbs/Funcons/Core/Values/Composite/Tuples/Tuples.hs +++ b/cbs/Funcons/Core/Values/Composite/Tuples/Tuples.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Tuples/Tuples.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Tuples/Tuples.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Tuples.Tuples where diff --git a/cbs/Funcons/Core/Values/Composite/Variants/Variants.hs b/cbs/Funcons/Core/Values/Composite/Variants/Variants.hs --- a/cbs/Funcons/Core/Values/Composite/Variants/Variants.hs +++ b/cbs/Funcons/Core/Values/Composite/Variants/Variants.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Variants/Variants.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Variants/Variants.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Variants.Variants where diff --git a/cbs/Funcons/Core/Values/Composite/Vectors/Vectors.hs b/cbs/Funcons/Core/Values/Composite/Vectors/Vectors.hs --- a/cbs/Funcons/Core/Values/Composite/Vectors/Vectors.hs +++ b/cbs/Funcons/Core/Values/Composite/Vectors/Vectors.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Vectors/Vectors.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Composite/Vectors/Vectors.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Composite.Vectors.Vectors where diff --git a/cbs/Funcons/Core/Values/Primitive/Booleans/Booleans.hs b/cbs/Funcons/Core/Values/Primitive/Booleans/Booleans.hs --- a/cbs/Funcons/Core/Values/Primitive/Booleans/Booleans.hs +++ b/cbs/Funcons/Core/Values/Primitive/Booleans/Booleans.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Primitive/Booleans/Booleans.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Primitive/Booleans/Booleans.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Primitive.Booleans.Booleans where diff --git a/cbs/Funcons/Core/Values/Primitive/Characters/Characters.hs b/cbs/Funcons/Core/Values/Primitive/Characters/Characters.hs --- a/cbs/Funcons/Core/Values/Primitive/Characters/Characters.hs +++ b/cbs/Funcons/Core/Values/Primitive/Characters/Characters.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Primitive/Characters/Characters.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Primitive/Characters/Characters.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Primitive.Characters.Characters where diff --git a/cbs/Funcons/Core/Values/Primitive/Floats/Floats.hs b/cbs/Funcons/Core/Values/Primitive/Floats/Floats.hs --- a/cbs/Funcons/Core/Values/Primitive/Floats/Floats.hs +++ b/cbs/Funcons/Core/Values/Primitive/Floats/Floats.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Primitive/Floats/Floats.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Primitive/Floats/Floats.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Primitive.Floats.Floats where diff --git a/cbs/Funcons/Core/Values/Primitive/Integers/Integers.hs b/cbs/Funcons/Core/Values/Primitive/Integers/Integers.hs --- a/cbs/Funcons/Core/Values/Primitive/Integers/Integers.hs +++ b/cbs/Funcons/Core/Values/Primitive/Integers/Integers.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Primitive/Integers/Integers.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Primitive/Integers/Integers.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Primitive.Integers.Integers where diff --git a/cbs/Funcons/Core/Values/Primitive/Null/Null.hs b/cbs/Funcons/Core/Values/Primitive/Null/Null.hs --- a/cbs/Funcons/Core/Values/Primitive/Null/Null.hs +++ b/cbs/Funcons/Core/Values/Primitive/Null/Null.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Primitive/Null/Null.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Primitive/Null/Null.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.Primitive.Null.Null where diff --git a/cbs/Funcons/Core/Values/ValueTypes/ValueTypes.hs b/cbs/Funcons/Core/Values/ValueTypes/ValueTypes.hs --- a/cbs/Funcons/Core/Values/ValueTypes/ValueTypes.hs +++ b/cbs/Funcons/Core/Values/ValueTypes/ValueTypes.hs @@ -1,4 +1,4 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Value-Types/Value-Types.cbs +-- GeNeRaTeD fOr: ../CBS-beta/Funcons-beta/Values/Value-Types/Value-Types.cbs {-# LANGUAGE OverloadedStrings #-} module Funcons.Core.Values.ValueTypes.ValueTypes where diff --git a/funcons-tools.cabal b/funcons-tools.cabal --- a/funcons-tools.cabal +++ b/funcons-tools.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: funcons-tools -version: 0.2.0.13 +version: 0.2.0.15 synopsis: A modular interpreter for executing funcons description: The PLanCompS project () has developed a component-based approach to formal semantics. @@ -53,10 +53,9 @@ ,directory ,mtl >= 2.2.1 ,gll >= 0.4.0.9 - ,TypeCompose>=0.9.10 ,regex-applicative - ,random-strings ,funcons-values >= 0.1.0.9 + ,random >= 1.1 ,haskeline >= 0.8.1.2 hs-source-dirs: src, cbs, manual default-language: Haskell2010 @@ -115,7 +114,15 @@ Funcons.Core.Values.Abstraction.Functions.Functions, Funcons.Core.Values.Abstraction.Patterns.Patterns, Funcons.Core.Values.Abstraction.Generic.Generic, - Funcons.Core.Values.Abstraction.Thunks.Thunks + Funcons.Core.Values.Abstraction.Thunks.Thunks, +-- unstable + Funcons.Core.Computations.Abnormal.Postponing.Postponing, + Funcons.Core.Computations.Normal.Indexing.Indexing, + Funcons.Core.Computations.Normal.Memos.Memos, + Funcons.Core.Computations.Threads.Multithreading.Multithreading, + Funcons.Core.Computations.Threads.Synchronising.Locks.Locks, + Funcons.Core.Computations.Threads.Synchronising.Notifications.Notifications, + Funcons.Core.Computations.Threads.Synchronising.Synchronising -- manual , Funcons.Core.Computations.Normal.GeneratingBuiltin , Funcons.Core.Computations.AbnormalBuiltin @@ -150,11 +157,10 @@ ,directory ,mtl >= 2.2.1 ,gll >= 0.4.0.9 - ,TypeCompose>=0.9.10 ,regex-applicative - ,random-strings ,funcons-values >= 0.1.0.9 - ,exploring-interpreters >= 0.3.0.0 + ,exploring-interpreters >= 1.3.0.0 + ,random >= 1.1 ,haskeline >= 0.8.1 ,transformers >= 0.5.6 hs-source-dirs: src, manual, cbs @@ -178,7 +184,121 @@ Funcons.Core.Computations.Normal.Interacting.Interacting Funcons.Core.Computations.Normal.Linking.Linking Funcons.Core.Computations.Normal.Storing.Storing - Funcons.Core.Computations.TypesBuiltin + Funcons.Core.Computations.TypesBuiltin, + -- unstable + Funcons.Core.Computations.Abnormal.Postponing.Postponing, + Funcons.Core.Computations.Normal.Indexing.Indexing, + Funcons.Core.Computations.Normal.Memos.Memos, + Funcons.Core.Computations.Threads.Multithreading.Multithreading, + Funcons.Core.Computations.Threads.Synchronising.Locks.Locks, + Funcons.Core.Computations.Threads.Synchronising.Notifications.Notifications, + Funcons.Core.Computations.Threads.Synchronising.Synchronising + Funcons.Core + Funcons.Core.Library + Funcons.Core.Manual + Funcons.Core.Values.Abstraction.Functions.Functions + Funcons.Core.Values.Abstraction.Generic.Generic + Funcons.Core.Values.Abstraction.Patterns.Patterns + Funcons.Core.Values.Abstraction.Thunks.Thunks + Funcons.Core.Values.Composite.ASTs.ASTs + Funcons.Core.Values.Composite.Bits.Bits + Funcons.Core.Values.Composite.Classes.Classes + Funcons.Core.Values.Composite.Datatypes.Datatypes + Funcons.Core.Values.Composite.DatatypesBuiltin + Funcons.Core.Values.Composite.Graphs.Graphs + Funcons.Core.Values.Composite.GraphsBuiltin + Funcons.Core.Values.Composite.Lists.Lists + Funcons.Core.Values.Composite.MapsBuiltin + Funcons.Core.Values.Composite.MultisetsBuiltin + Funcons.Core.Values.Composite.Objects.Objects + Funcons.Core.Values.Composite.Records.Records + Funcons.Core.Values.Composite.References.References + Funcons.Core.Values.Composite.Sequences.Sequences + Funcons.Core.Values.Composite.SetsBuiltin + Funcons.Core.Values.Composite.Strings.Strings + Funcons.Core.Values.Composite.Trees.Trees + Funcons.Core.Values.Composite.Tuples.Tuples + Funcons.Core.Values.Composite.Variants.Variants + Funcons.Core.Values.Composite.Vectors.Vectors + Funcons.Core.Values.Primitive.Atoms + Funcons.Core.Values.Primitive.BitsBuiltin + Funcons.Core.Values.Primitive.BoolBuiltin + Funcons.Core.Values.Primitive.Booleans.Booleans + Funcons.Core.Values.Primitive.Characters.Characters + Funcons.Core.Values.Primitive.CharactersBuiltin + Funcons.Core.Values.Primitive.Floats.Floats + Funcons.Core.Values.Primitive.FloatsBuiltin + Funcons.Core.Values.Primitive.Integers.Integers + Funcons.Core.Values.Primitive.IntegersBuiltin + Funcons.Core.Values.Primitive.Null.Null + Funcons.Core.Values.Primitive.StringsBuiltin + Funcons.Core.Values.TypesBuiltin + Funcons.Core.Values.ValueTypes.ValueTypes + Funcons.EDSL + Funcons.Entities + Funcons.Exceptions + Funcons.GLLParser + Funcons.MSOS + Funcons.Parser + Funcons.Patterns + Funcons.Printer + Funcons.RunOptions + Funcons.Simulation + Funcons.Substitution + Funcons.Tools + Funcons.TypeSubstitution + Funcons.Types + Funcons.Explorer + +executable runfct + main-is: Main.hs + other-extensions: OverloadedStrings + build-depends: base >=4.8 && <= 5 + ,text >= 1.2 + ,containers >= 0.5 && < 0.7 + ,vector>=0.12 + ,bv >= 0.5 + ,multiset >= 0.3 + ,split + ,directory + ,mtl >= 2.2.1 + ,gll >= 0.4.0.9 + ,regex-applicative + ,funcons-values >= 0.1.0.9 + ,exploring-interpreters >= 1.3.0.0 + ,random >= 1.1 + ,haskeline >= 0.8.1 + ,transformers >= 0.5.6 + hs-source-dirs: src, manual, cbs + default-language: Haskell2010 + -- ghc-options: -rtsopts + other-modules: + Funcons.Core.Computations.Abnormal.Abrupting.Abrupting + Funcons.Core.Computations.Abnormal.Breaking.Breaking + Funcons.Core.Computations.Abnormal.Continuing.Continuing + Funcons.Core.Computations.Abnormal.Controlling.Controlling + Funcons.Core.Computations.Abnormal.Failing.Failing + Funcons.Core.Computations.Abnormal.Returning.Returning + Funcons.Core.Computations.Abnormal.Sticking + Funcons.Core.Computations.Abnormal.Throwing.Throwing + Funcons.Core.Computations.AbnormalBuiltin + Funcons.Core.Computations.Normal.Binding.Binding + Funcons.Core.Computations.Normal.Flowing.Flowing + Funcons.Core.Computations.Normal.Generating.Generating + Funcons.Core.Computations.Normal.GeneratingBuiltin + Funcons.Core.Computations.Normal.Giving.Giving + Funcons.Core.Computations.Normal.Interacting.Interacting + Funcons.Core.Computations.Normal.Linking.Linking + Funcons.Core.Computations.Normal.Storing.Storing + Funcons.Core.Computations.TypesBuiltin, + -- unstable + Funcons.Core.Computations.Abnormal.Postponing.Postponing, + Funcons.Core.Computations.Normal.Indexing.Indexing, + Funcons.Core.Computations.Normal.Memos.Memos, + Funcons.Core.Computations.Threads.Multithreading.Multithreading, + Funcons.Core.Computations.Threads.Synchronising.Locks.Locks, + Funcons.Core.Computations.Threads.Synchronising.Notifications.Notifications, + Funcons.Core.Computations.Threads.Synchronising.Synchronising Funcons.Core Funcons.Core.Library Funcons.Core.Manual diff --git a/manual/Funcons/Core/Computations/Normal/GeneratingBuiltin.hs b/manual/Funcons/Core/Computations/Normal/GeneratingBuiltin.hs --- a/manual/Funcons/Core/Computations/Normal/GeneratingBuiltin.hs +++ b/manual/Funcons/Core/Computations/Normal/GeneratingBuiltin.hs @@ -17,8 +17,8 @@ where step1 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "P"] env - env <- getMutPatt "used-atom-set" (VPWildCard) env - putMut "used-atom-set" reserved_atoms + env <- getMutPatt "used-atom-set" [VPWildCard] env + putMut "used-atom-set" [reserved_atoms] stepTermTo (TVar "P") env reserved_atoms = Set (fromList []) diff --git a/manual/Funcons/Core/Values/Composite/SetsBuiltin.hs b/manual/Funcons/Core/Values/Composite/SetsBuiltin.hs --- a/manual/Funcons/Core/Values/Composite/SetsBuiltin.hs +++ b/manual/Funcons/Core/Values/Composite/SetsBuiltin.hs @@ -7,9 +7,6 @@ import qualified Data.Set as S -import Test.RandomStrings (randomString', randomASCII) -import System.IO.Unsafe (unsafePerformIO) - library = libFromList [ ("set", fromValOp set_ VAL.set_) , ("set-empty", fromNullaryValOp set_empty_ VAL.set_empty_) diff --git a/manual/Funcons/MetaProgramming.hs b/manual/Funcons/MetaProgramming.hs --- a/manual/Funcons/MetaProgramming.hs +++ b/manual/Funcons/MetaProgramming.hs @@ -90,8 +90,8 @@ ((Right f, _, _), _) -> f where process = do env <- evalRel fenv - putMut atom_gen_entity (Set S.empty) - putMut store_entity (Map M.empty) + putMut atom_gen_entity [Set S.empty] + putMut store_entity [Map M.empty] withInh env_entity [env] (ctRel f) env_entity = "environment" @@ -105,7 +105,7 @@ cmp_MSOSReader lib env f = MSOSReader cmp_RewriteReader M.empty M.empty (fread True) where cmp_RewriteReader = RewriteReader lib env defaultRunOptions f f --cmp_MSOSWriter = MSOSWriter mempty mempty mempty -cmp_MSOSState = MSOSState M.empty M.empty (RewriteState) +cmp_MSOSState = MSOSState M.empty M.empty emptyRewriteState library :: FunconLibrary library = libFromList [ diff --git a/src/Funcons/EDSL.hs b/src/Funcons/EDSL.hs --- a/src/Funcons/EDSL.hs +++ b/src/Funcons/EDSL.hs @@ -13,7 +13,7 @@ -- *** Funcon terms set_, vec_, env_fromlist_, null__, -- *** Values - int_, bool_, bool__, list__, vector__, tuple__, char_, char__, nat_, float_, ieee_float_32_, ieee_float_64_, string_, string__, atom_, + int_, bool_, bool__, list__, set__, empty_set__, vector__, tuple__, char_, char__, nat_, float_, ieee_float_32_, ieee_float_64_, string_, string__, atom_, -- *** Types values_, integers_, vectors_, type_, ty_star, ty_plus, ty_opt, ty_union, ty_neg, ty_inter, ty_power, -- ** Pretty-print funcon terms diff --git a/src/Funcons/Entities.hs b/src/Funcons/Entities.hs --- a/src/Funcons/Entities.hs +++ b/src/Funcons/Entities.hs @@ -47,8 +47,7 @@ setEntityDefaults [] msos = msos setEntityDefaults ((DefMutable nm f):rest) msos = liftRewrite (rewriteFuncons f) >>= \case - ValTerm [v] -> putMut nm v >> setEntityDefaults rest msos - ValTerm vs -> liftRewrite $ exception f "default value evaluates to a sequence" + ValTerm vs -> putMut nm vs >> setEntityDefaults rest msos _ -> liftRewrite $ exception f "default value requires steps to evaluate" setEntityDefaults ((DefInherited nm f):rest) msos = liftRewrite (rewriteFuncons f) >>= \case @@ -70,32 +69,29 @@ giveMUT = MSOS $ \ctxt mut -> return (Right (mut_entities mut), mut, mempty) -- | Get the value of some mutable entity. -getMut :: Name -> MSOS Values -getMut key = do rw <- giveMUT - case M.lookup key rw of - Nothing -> return null__ - Just v -> return v +getMut :: Name -> MSOS [Values] +getMut key = maybe [null__] id . M.lookup key <$> giveMUT -- | Variant of 'getMut' that performs pattern-matching. -getMutPatt :: Name -> VPattern -> Env -> MSOS Env -getMutPatt nm pat env = do - val <- getMut nm - liftRewrite (vMatch val pat env) +getMutPatt :: Name -> [VPattern] -> Env -> MSOS Env +getMutPatt nm pats env = do + vals <- getMut nm + liftRewrite (vsMatch vals pats env) -modifyMUT :: Name -> (Values -> Values) -> MSOS () +modifyMUT :: Name -> ([Values] -> [Values]) -> MSOS () modifyMUT key f = do rw <- giveMUT newMUT (M.alter up key rw) - where up Nothing = Just (f null__) - up (Just x) = Just (f x) + where up Nothing = Just (f [null__]) + up (Just xs) = Just (f xs) -- | Set the value of some mutable entity. -putMut :: Name -> Values -> MSOS () +putMut :: Name -> [Values] -> MSOS () putMut key v = do rw <- giveMUT newMUT (M.insert key v rw) -- | Variant of 'putMut' that applies substitution. putMutTerm :: Name -> FTerm -> Env -> MSOS () -putMutTerm nm term env = liftRewrite (subsAndRewritesToValue term env) >>= putMut nm +putMutTerm nm term env = liftRewrite (subsAndRewritesToValues term env) >>= putMut nm newMUT :: Mutable -> MSOS () newMUT rw = MSOS $ \ctxt mut-> return (Right(), mut {mut_entities = rw}, mempty) diff --git a/src/Funcons/Explorer.hs b/src/Funcons/Explorer.hs --- a/src/Funcons/Explorer.hs +++ b/src/Funcons/Explorer.hs @@ -30,13 +30,22 @@ import System.Environment import System.IO +data Phrase = FTerm Funcons + | Debug Funcons + | Step + | SmallStep + | PrettyBigStep + | Finish + deriving (Show, Eq) + data Config = Config { reader :: MSOSReader IO - , state :: MSOSState IO + , state :: MSOSState IO + , progress:: StepRes } deriving (Eq) -type Explorer = EI.Explorer Funcons IO Config () +type Explorer = EI.Explorer Phrase IO Config () handle_revert :: EI.Ref -> Explorer -> IO Explorer handle_revert r exp = @@ -68,9 +77,16 @@ (":revert", mint) | Just ref_id' <- readMaybe (dropWhile isSpace mint) -> lift (handle_revert ref_id' exp) >>= repl' | otherwise -> outputStrLn "Revert requires an integer argument" >> repl' exp + (":debug", mfct) -> case fct_parse_either (dropWhile isSpace mfct) of + Left err -> outputStrLn err >> repl' exp + Right fct -> lift (EI.execute (Debug fct) exp) >>= (repl' . fst) + (":step", _) -> lift (EI.execute Step exp) >>= (repl' . fst) + (":small-step", _)-> lift (EI.execute SmallStep exp) >>= (repl' . fst) + (":pretty-big-step", _) -> lift (EI.execute PrettyBigStep exp) >>= (repl' . fst) + (":finish", _) -> lift (EI.execute Finish exp) >>= (repl' . fst) _ -> case fct_parse_either input of Left err -> outputStrLn err >> repl' exp - Right fct -> lift (EI.execute fct exp) >>= (repl' . fst) + Right fct -> lift (EI.execute (FTerm fct) exp) >>= (repl' . fst) mk_explorer :: [String] -> IO Explorer @@ -80,7 +96,7 @@ putStrLn ("unknown option: " ++ arg) opts_ref <- newIORef opts cfg <- mk_initial_config library entities typeenv opts - return $ EI.mkExplorerTree (\f c -> (\c -> (c, ())) <$> def_interpreter opts_ref f c) cfg + return $ EI.mkExplorer False (const . const $ False) (\f c -> (\c -> (c, ())) <$> def_interpreter opts_ref f c) cfg where library = libUnions [ Funcons.Core.Library.funcons, Funcons.EDSL.library, Funcons.Core.Manual.library ] entities = Funcons.Core.Library.entities @@ -90,36 +106,74 @@ mk_initial_config lib defaults tyenv opts = do let msos_ctxt = MSOSReader (RewriteReader lib tyenv opts f0 f0) emptyINH emptyDCTRL (fread (string_inputs opts)) ((e_exc_f, mut, wr), rem_ins) <- - fexec (runMSOS (setEntityDefaults defaults (stepTrans opts 0 (toStepRes f0))) - msos_ctxt (emptyMSOSState {inp_es = M.empty})) (inputValues opts) - return $ Config { reader = init msos_ctxt, state = mut } + fexec (runMSOS (setEntityDefaults defaults (loop opts f0)) + msos_ctxt ((emptyMSOSState (random_seed opts)) {inp_es = M.empty})) (inputValues opts) + return $ Config { reader = init msos_ctxt, state = mut, progress = done } where f0 = initialise_binding_ [initialise_storing_ [map_empty_ []]] init msos_reader = msos_reader {inh_entities = M.insert "environment" [Map M.empty] (inh_entities msos_reader) } -def_interpreter :: IORef RunOptions -> Funcons -> Config -> IO (Maybe Config) -def_interpreter opts_ref f0' cfg = do - let f0 = give_ [f0', - give_ [if_else_ [is_ [given_, environments_], given_ - ,if_else_ [is_ [given_, null_type_], given_ - ,bind_ [Funcons.EDSL.string_ "it", given_]]] - ,if_else_ [is_ [given_, null_type_], given_ - ,sequential_ [print_ [given_,Funcons.EDSL.string_ "\n"], given_]]]] - opts <- readIORef opts_ref - let msos_ctxt = (reader cfg) { ereader = (ereader (reader cfg)) { local_fct = f0, global_fct = f0 } } - (e_exc_f, mut, wr) <- runMSOS (stepTrans opts 0 (toStepRes f0)) msos_ctxt (state cfg) - case e_exc_f of - Left ie -> putStrLn (showIException ie) >> return Nothing - Right (Left fct) -> return $ Just $ cfg { state = mut } -- did not yield an environment - Right (Right efvs) -> case filter isMap efvs of - [] -> return $ Just $ cfg { state = mut } - [env] -> return $ Just $ cfg { reader = accumulate (reader cfg) env, state = mut } - _ -> putStrLn ("multiple environments computed") >> return Nothing - where accumulate msos_reader env = msos_reader { inh_entities = M.update override "environment" (inh_entities msos_reader) } - where override [old_env] = case (env, old_env) of - (Map m1, Map m2) -> Just [Map (M.union m1 m2)] - _ -> Nothing - override _ = Nothing +def_interpreter :: IORef RunOptions -> Phrase -> Config -> IO (Maybe Config) +def_interpreter opts_ref phrase cfg = do + opts <- readIORef opts_ref + case phrase of FTerm f0' -> let f0 = prep_term f0' + in fmap (setProgress done) <$> exec (loop opts) f0 (prep_ctxt f0 opts) + Debug f0' -> let f0 = prep_term f0' + in putStrLn ("\nremaining funcon term:\n" ++ ppFuncons opts f0) + >> return (Just (cfg { progress = Left f0 })) + Step -> case progress cfg of + Left fct -> mk_step opts fct + Right vs -> putStrLn "already done.." >> return (Just cfg) + SmallStep -> case progress cfg of + Left fct -> mk_step (turn_off_refocus opts) fct + Right vs -> putStrLn "already done.." >> return (Just cfg) + PrettyBigStep -> case progress cfg of + Left fct -> mk_step (turn_on_refocus opts) fct + Right vs -> putStrLn "already done.." >> return (Just cfg) + Finish -> case progress cfg of + Left fct -> fmap (setProgress done) <$> exec (loop opts) fct (prep_ctxt fct opts) + Right vs -> putStrLn "already done.." >> return (Just cfg) + where prep_term f0' = + give_ [f0', + give_ [if_else_ [is_ [given_, environments_], given_ + ,if_else_ [is_ [given_, null_type_], given_ + ,bind_ [Funcons.EDSL.string_ "it", given_]]] + ,if_else_ [is_ [given_, null_type_], given_ + ,sequential_ [print_ [given_,Funcons.EDSL.string_ "\n"], given_]]]] + prep_ctxt f0 opts = (reader cfg) { ereader = (ereader (reader cfg)) { local_fct = f0, global_fct = f0, run_opts = opts } } + mk_step opts f0 = do im <- exec step f0 (prep_ctxt f0 opts) + case im of Just cfg -> case progress cfg of + Left fct -> putStrLn ("\nremaining funcon term:\n" ++ ppFuncons opts fct) + _ -> return () + Nothing -> return () + return im + exec stepper f0 msos_ctxt = do + (e_exc_f, mut, wr) <- runMSOS (stepper f0) msos_ctxt (state cfg) + case e_exc_f of + Left ie -> putStrLn (showIException ie) >> return Nothing + Right (Left fct) -> return $ Just $ cfg { state = mut, progress = Left fct} -- did not yield an environment + Right (Right efvs) -> case filter isMap efvs of + [] -> return $ Just $ cfg { state = mut, progress = Right efvs } + [env] -> return $ Just $ cfg { reader = accumulate (reader cfg) env, state = mut, progress = Right efvs } + _ -> putStrLn ("multiple environments computed") >> return Nothing + where accumulate msos_reader env = msos_reader { inh_entities = M.update override "environment" (inh_entities msos_reader) } + where override [old_env] = case (env, old_env) of + (Map m1, Map m2) -> Just [Map (M.union m1 m2)] + _ -> Nothing + override _ = Nothing + +loop :: RunOptions -> Funcons -> MSOS StepRes +loop opts = stepTrans opts 0 . toStepRes + +step :: Funcons -> MSOS StepRes +step = stepAndOutput + +done :: StepRes +done = Right [] + +setProgress :: StepRes -> Config -> Config +setProgress res cfg = cfg { progress = res } + -- assumes all components of RewriteReader do not change per session instance Eq (MSOSReader IO) where r1 == r2 = inh_entities r1 == inh_entities r2 @@ -137,7 +191,7 @@ display_mut_entity cfg ent = case M.lookup (pack ent) (mut_entities (state cfg)) of Nothing -> putStrLn ("unknown mutable entity: " ++ ent) - Just v -> putStrLn $ showValues v + Just v -> putStrLn $ showL (map showValues v) display_help :: IO () display_help = @@ -148,6 +202,11 @@ \ :session displays the explored traces in the form of a tree\n\ \ with nodes labelled by state identifiers\n\ \ :revert revert to the state with id \n\ + \ :debug start step-by-step execution of funcon term \n\ + \ :step perform the next step in a step-by-step execution (without changing the refocusing setting)\n\ + \ :pretty-big-step perform the next step in a step-by-step execution with refocusing\n\ + \ :small-step perform the next step in a step-by-step execution without refocusing\n\ + \ :finish perform all remaining steps of a step-by-step execution\n\ \ :help :h show these commands\n\ \ :quit :q end the exploration\n\ \ or just type a funcon term" diff --git a/src/Funcons/MSOS.hs b/src/Funcons/MSOS.hs --- a/src/Funcons/MSOS.hs +++ b/src/Funcons/MSOS.hs @@ -24,10 +24,11 @@ rewriteRules, stepRules, evalRules, MSOSState(..), emptyMSOSState, emptyRewriteState, MSOSReader(..),RewriteReader(..),showIException, MSOSWriter(..), RewriteWriterr(..), -- * Evaluation funcons TODO internal usage only (by Funcons.Tools) Rewritten(..), rewriteFuncons, rewriteFunconsWcount, evalFuncons - , stepTrans, rewritesToValue, rewritesToValues, rewritesToType + , stepTrans, stepAndOutput, rewritesToValue, rewritesToValues, rewritesToType , emptyDCTRL, emptyINH, Interactive(..), SimIO(..) , rewriteToValErr, count_delegation, optRefocus - , evalStrictSequence, rewriteStrictSequence, evalSequence, + , evalStrictSequence, rewriteStrictSequence, evalSequence + , maybe_randomSelect, maybe_randomRemove, -- * Values showTypes, showSorts, showValues, showValuesSeq, showFuncons, showFunconsSeq,traceLib, -- * Funcon libraries @@ -49,14 +50,17 @@ import Control.Arrow ((***)) import Control.Monad.Writer hiding ((<>)) import Control.Monad.Fail +import Data.Function (on) import Data.Maybe (isJust, isNothing, fromJust) -import Data.List (foldl', intercalate) +import Data.List (foldl', intercalate, partition, sortBy) import Data.Text (unpack) import Data.Semigroup import qualified Data.Map as M +import System.Random import System.IO.Unsafe + --trace p b = unsafePerformIO (putStrLn p >> return b) trace p b = b traceLib :: FunconLibrary -> FunconLibrary @@ -78,21 +82,29 @@ fromNullaryValOp cons mkExpr = NullaryFuncon op where op = report (cons []) False (VAL.eval (mkExpr [])) +report :: Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten report f seqRes res = case res of - Error _ (VAL.SortErr str) -> sortErr f str - Error _ (DomErr str) -> rewrittens [] - Error _ (ArityErr str) -> sortErr f str - Error _ (ProjErr str) -> sortErr f str - Error _ (Normal (FValue v)) -> rewritten' v - Error _ (Normal t) -> rewriteFuncons t + Error _ dres -> reportResult dres Success (FValue (ADTVal "null" _)) -> rewrittens [] Success (FValue v) -> rewritten' v Success t -> rewriteFuncons t + EvalResults ress -> maybe_randomSelect NDValueOperations ress >>= + report f seqRes where rewritten' v | seqRes, ValSeq fs <- v, let mvs = map project fs, all isJust mvs = rewrittens (map fromJust mvs) | otherwise = rewritten v - + reportResult dres = case dres of + (VAL.SortErr str) -> sortErr f str + (DomErr str) -> rewrittens [] + (ArityErr str) -> sortErr f str + (ProjErr str) -> sortErr f str + (Normal (FValue v)) -> rewritten' v + (Normal t) -> rewriteFuncons t + (Nondeterministic ress) -> case ress of + [] -> sortErr f "nondeterminism: empty" + _ -> randomSelect ress >>= reportResult + -- | -- Evaluation functions capture the operational behaviour of a funcon. -- Evaluation functions come in multiple flavours, each with a different @@ -182,8 +194,8 @@ { funconlib :: FunconLibrary , ty_env :: TypeRelation, run_opts :: RunOptions , global_fct :: Funcons, local_fct :: Funcons } -data RewriteState = RewriteState { } -emptyRewriteState = RewriteState +data RewriteState = RewriteState { random_gen :: StdGen } +emptyRewriteState = RewriteState (mkStdGen 0) data RewriteWriterr = RewriteWriterr { counters :: Counters } -- | Monadic type for the implicit propagation of meta-information on @@ -271,8 +283,9 @@ , ewriter :: RewriteWriterr } data MSOSState m = MSOSState { inp_es :: Input m, mut_entities :: Mutable , estate :: RewriteState } -emptyMSOSState :: MSOSState m -emptyMSOSState = MSOSState M.empty M.empty emptyRewriteState +emptyMSOSState :: Int -> MSOSState m +emptyMSOSState seed = + MSOSState M.empty M.empty (emptyRewriteState { random_gen = mkStdGen seed }) -- | Monadic type for the propagation of semantic entities and meta-information -- on the evaluation of funcons. The meta-information includes a library @@ -332,13 +345,15 @@ MSOSWriter (x1 `unionCTRL` y1) (x2 `unionOUT` y2) (x3 `mappend` y3) -- | A map storing the values of /mutable/ entities. -type Mutable = M.Map Name Values +type Mutable = M.Map Name [Values] stepRules = stepARules NoMoreBranches count_backtrack_in stepARules :: ([IException] -> IE) -> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes stepARules fexc _ errs [] = msos_throw (fexc errs) -stepARules fexc counter errs (t1:ts) = MSOS $ \ctxt mut -> do +stepARules fexc counter errs ts = + liftRewrite (maybe_randomRemove NDRuleSelection ts) >>= + \(t1,ts) -> MSOS $ \ctxt mut -> do (e_ie_a, mut', wr) <- runMSOS t1 ctxt mut case e_ie_a of Left ie | failsRule ie -> -- resets input & read/write entities @@ -368,7 +383,9 @@ evalRules = evalRules' [] evalRules' :: [IException] -> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten evalRules' errs [] msoss = buildStep (stepARules NoRule count_backtrack_out errs msoss) -evalRules' errs ((Rewrite rw_rules):rest) msoss = Rewrite $ \ctxt st -> +evalRules' errs rules msoss = + maybe_randomRemove NDRuleSelection rules >>= \((Rewrite rw_rules),rest) -> + Rewrite $ \ctxt st -> let (rw_res, st', wo) = rw_rules ctxt st in case rw_res of Left ie | failsRule ie -> --resets counters and state @@ -382,10 +399,10 @@ msos_throw = liftRewrite . rewrite_throw --- -giveOpts :: MSOS RunOptions -giveOpts = MSOS $ \ctxt mut -> - return (Right (run_opts (ereader ctxt)), mut, mempty) +giveOpts :: Rewrite RunOptions +giveOpts = Rewrite $ \ctxt mut -> (Right (run_opts ctxt), mut, mempty) + giveINH :: MSOS Inherited giveINH = MSOS $ \ctxt mut -> return (Right (inh_entities ctxt), mut, mempty) @@ -402,6 +419,43 @@ modifyRewriteReader :: (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a modifyRewriteReader mod (MSOS f) = MSOS (f . mod') where mod' ctxt = ctxt { ereader = mod (ereader ctxt) } + +maybe_randomRemove :: SourceOfND -> [a] -> Rewrite (a, [a]) +maybe_randomRemove _ [] = randomRemove [] +maybe_randomRemove src xs@(x:xs') = do + opts <- giveOpts + if src `elem` get_nd_sources opts then randomRemove xs + else return (x, xs') + +-- | Uses the random number generator of Rewrite to randomly select +-- an element of a given list. The element is returned, together +-- with the list from which the element has been removed +-- Raises an internal exception if given an empty list +randomRemove :: [a] -> Rewrite (a, [a]) +randomRemove [] = internal "randomRemove: empty list" +randomRemove [x]= return (x, []) +randomRemove xs = Rewrite $ \_ mut -> + let gen = random_gen mut + (i, gen') = next gen + index = i `mod` (length xs) + elem = xs !! index + rest = take index xs ++ drop (index + 1) xs + in (Right (elem, rest), mut {random_gen = gen'}, mempty ) + +maybe_randomSelect src xs = fst <$> maybe_randomRemove src xs +randomSelect xs = fst <$> randomRemove xs + +{- +randomSelect :: [a] -> Rewrite a +randomSelect xs = Rewrite $ \_ mut -> + let gen = random_gen mut + (_, top) = genRange gen + unit = fromIntegral top / fromIntegral (length xs) + (i, gen') = next gen + index = round (fromIntegral i / unit) + in (Right (xs !! index), mut {random_gen = gen'}, mempty ) +-} + ----------------- -- | a map storing the values of /inherited/ entities. type Inherited = M.Map Name [Values] @@ -808,22 +862,36 @@ evalSequence :: [Strictness] -> [Funcons] -> ([Funcons] -> Rewrite Rewritten) -> ([Funcons] -> Funcons) -> Rewrite Rewritten -evalSequence strns args cont cons = - uncurry evalSeqAux $ map snd *** id $ span isDone (zip strns args) - where unmatched = drop (length strns) args - evalSeqAux :: [Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten - evalSeqAux vs [] = cont vs - evalSeqAux vs ((_,f):fs) = premiseEval valueCont funconCont f - where valueCont vs' = do - count_rewrite - evalSeqAux (vs++(map FValue vs' ++ map snd othervs)) otherfs - where (othervs, otherfs) = span isDone fs - funconCont stepf = stepf >>= \case - Left f' -> stepTo (cons (vs++[f']++map snd fs)) - Right vs' -> stepTo (cons (vs++(map FValue vs')++map snd fs)) +evalSequence strns args cont cons = do + let args_map = zip [1..] (zip strns args) + + let evalSeqAux args_done args_undone + | null args_undone = cont (map (snd . snd) (sorter args_done)) + | otherwise = do + ((i,(_,f)), args_undone') <- + maybe_randomRemove NDInterleaving args_undone + let valueCont vs = do + count_rewrite + evalSeqAux args_done' (map bump args_undone') + where args_done' = filter ((i) . fst) args_done) + bump (k,v) | k > i = (k + length vs - 1, v) + | otherwise = (k,v) + let funconCont stepf = stepf >>= \case + Left f' -> stepTo (cons (remakeArgs args_done [f'] args_undone')) + Right vs' -> stepTo (cons (remakeArgs args_done (map FValue vs') args_undone')) + where remakeArgs m1 l1 m2 = + map (snd . snd) (sorter (filter ((i) . fst) (m1++m2))) + + premiseEval valueCont funconCont f + uncurry evalSeqAux (partition (isDone . snd) args_map) + where isDone (NonStrict, _) = True isDone (Strict, FValue _) = True - isDone (NonStrict, _) = True - isDone _ = False + isDone (Strict,_) = False + sorter = sortBy (compare `on` fst) -- | Yield an 'MSOS' computation as a fully rewritten term. -- This function must be used in order to access entities in the definition @@ -841,18 +909,19 @@ | otherwise -> if_abruptly_terminates (do_abrupt_terminate opts) (stepAndOutput f) return continue where continue res = count_restart >> stepTrans opts (i+1) res - stepAndOutput :: Funcons -> MSOS StepRes - stepAndOutput f = MSOS $ \ctxt mut -> - let MSOS stepper' = evalFuncons f - stepper ctxt mut = stepper' (setGlobal ctxt) mut - setGlobal ctxt = ctxt - { ereader = (ereader ctxt) {global_fct = f }} - in do (eres,mut',wr') <- stepper ctxt mut - mapM_ (uncurry fprint) - [ (entity,val) - | (entity, vals) <- M.assocs (out_entities wr') - , val <- vals ] - return (eres, mut', wr') + +stepAndOutput :: Funcons -> MSOS StepRes +stepAndOutput f = MSOS $ \ctxt mut -> + let MSOS stepper' = evalFuncons f + stepper ctxt mut = stepper' (setGlobal ctxt) mut + setGlobal ctxt = ctxt + { ereader = (ereader ctxt) {global_fct = f }} + in do (eres,mut',wr') <- stepper ctxt mut + mapM_ (uncurry fprint) + [ (entity,val) + | (entity, vals) <- M.assocs (out_entities wr') + , val <- vals ] + return (eres, mut', wr') toStepRes :: Funcons -> StepRes diff --git a/src/Funcons/Patterns.hs b/src/Funcons/Patterns.hs --- a/src/Funcons/Patterns.hs +++ b/src/Funcons/Patterns.hs @@ -10,6 +10,7 @@ import Funcons.Substitution import Funcons.Exceptions import Funcons.Operations (isGround) +import Funcons.RunOptions (SourceOfND(..)) import Control.Applicative import Control.Monad (foldM, forM) @@ -61,10 +62,10 @@ Nothing -> compare -- no annotation => shortest match Just _ -> flip compare -- annoration => longest match -matching :: (a -> String) -> [a] -> [Matcher a] -> Env -> Rewrite Env -matching show str ps env = do +matching :: String -> (a -> String) -> [a] -> [Matcher a] -> Env -> Rewrite Env +matching pats show str ps env = do matches <- foldr seqWith lastMatcher ps str 0 env - let rule_fail = PatternMismatch ("Pattern match failed: " ++ intercalate "," (map show str)) + let rule_fail = PatternMismatch ("Pattern match failed: " ++ intercalate "," (map show str) ++ " does not match " ++ pats) case matches of [] -> rewrite_throw rule_fail [(_,env')] -> return env' @@ -76,10 +77,14 @@ | otherwise = return [] seqWith :: Matcher a -> Matcher a -> Matcher a - seqWith p q str k env = p str k env >>= foldM acceptFirst [] - where acceptFirst acc (r, env) - | null acc = q str r env - | otherwise = return acc + seqWith p q str k env = p str k env >>= acceptFirst + where acceptFirst [] = return [] + acceptFirst xs@((r,env):rest) = do +-- requires backtracking between premises and pattern matching to avoid unnecessary failure + ((r, env),rest) <- maybe_randomRemove NDPatternMatching xs + res <- q str r env + case res of [] -> acceptFirst rest + _ -> return res ordered_subsequences :: [a] -> [[a]] ordered_subsequences xs = ordered_subsequences' xs [] @@ -110,6 +115,7 @@ | VPAnnotated VPattern FTerm | VPSeqVar MetaVar SeqSortOp | VPLit Values + | VPEmptySet | VPType TPattern deriving (Show, Eq, Ord, Read) @@ -120,7 +126,8 @@ v2tPattern (PADT cons pats) = TPADT cons <$> mapM v2tPattern pats v2tPattern (VPLit lit) = Just $ TPLit (TFuncon (FValue lit)) v2tPattern VPWildCard = Just TPWildCard ---v2tPattern (PList _) = Nothing +--v2tPattern (PList _) = Nothing +v2tPattern VPEmptySet = Nothing v2tPattern (VPAnnotated fp t) = Nothing -- required for "matching" lazy arguments (fields) of adt constructors @@ -135,6 +142,7 @@ substitute_patt_signal vpat env = case vpat of PADT name vpats -> PADT name <$> subs_flatten vpats env VPWildCard -> return VPWildCard + VPEmptySet -> return VPEmptySet -- PList pats -> PList <$> subs_flatten pats env VPMetaVar var -> case M.lookup var env of Nothing -> return (VPMetaVar var) @@ -181,7 +189,7 @@ | all isSort_ str , Just tpats <- sequence (map v2tPattern pats) = tsMatch (map (downcastSort . FValue) str) tpats env - | otherwise = matching showValues str matchers env + | otherwise = matching (show pats) showValues str matchers env where matchers = map toMatcher pats toMatcher pat = case vpSeqVarInfo pat of Just info -> seqMatcher isInMaybeTermTypePreserve ValuesTerm info @@ -208,7 +216,7 @@ | not strict && all (not.hasStep) str = let downValues vs = map downcastValue vs in vsMatch (downValues str) (map f2vPattern pats) env - | otherwise = matching showFuncons str matchers env + | otherwise = matching (show pats) showFuncons str matchers env where matchers = map toMatcher pats toMatcher pat = case fpSeqVarInfo pat of Just info -> seqMatcher rewritesToAnnotatedType FunconsTerm info @@ -250,6 +258,8 @@ vMatch (ADTVal str vs) (PADT "datatype-value" pats) env = adtMatch "" "" (string_ (unpack str):vs) pats env vMatch _ (VPWildCard) env = return env +vMatch (Set s) VPEmptySet env | null s = return env +vMatch (Map m) VPEmptySet env | null m = return env vMatch VAny _ env = return env vMatch v (VPMetaVar var) env = return (envInsert var (ValueTerm v) env) vMatch (ADTVal str vs) (PADT con pats) env = adtMatch str con vs pats env @@ -273,7 +283,7 @@ tsMatch = strict_tsMatch strict_tsMatch :: [ComputationTypes] -> [TPattern] -> Env -> Rewrite Env -strict_tsMatch str pats env = matching showSorts str matchers env +strict_tsMatch str pats env = matching (show pats) showSorts str matchers env where matchers = map toMatcher pats toMatcher pat = case tpSeqVarInfo pat of Nothing -> singleMatcher tMatch pat @@ -527,6 +537,7 @@ PADT cons pats -> case pats of [] -> TName cons _ -> TApp cons (map vpat2term pats) VPLit lit -> TFuncon $ (FValue lit) + VPEmptySet -> TFuncon $ (FValue (set__ [])) VPWildCard -> TAny -- PList pats -> TList (map vpat2term pats) VPMetaVar var -> TVar var diff --git a/src/Funcons/Printer.hs b/src/Funcons/Printer.hs --- a/src/Funcons/Printer.hs +++ b/src/Funcons/Printer.hs @@ -2,7 +2,7 @@ module Funcons.Printer ( ppFuncons, ppValues, ppTypes, ppTerms, - showValues, showFuncons, showTypes, showSorts, showTerms, showOp, + showValues, showFuncons, showTypes, showSorts, showTerms, showOp, showL, showValuesSeq, ppValuesSeq, showFunconsSeq, ppFunconsSeq, ) where @@ -11,6 +11,9 @@ import Data.List (intercalate) import Data.Text (unpack) + +showL :: [String] -> String +showL elems = "[" ++ intercalate "," elems ++ "]" -- | Pretty-print a 'Values'. showValues :: Values -> String diff --git a/src/Funcons/RunOptions.hs b/src/Funcons/RunOptions.hs --- a/src/Funcons/RunOptions.hs +++ b/src/Funcons/RunOptions.hs @@ -10,7 +10,7 @@ import qualified Data.Map as M import Control.Monad (when) -import Control.Compose (OO(..)) +import GLL.Types.TypeCompose (OO(..)) import Data.Text (pack) import Data.List (isSuffixOf, isPrefixOf) import Data.List.Split (splitOn) @@ -30,6 +30,24 @@ , given_inputs :: InputValues } +-- | Several sources of nondeterminism exists, i.e. locations where a choice between a sequence of valid alternatives are made. +-- These options turn on pseudo-random selection of an alternative, based on a seed provide (configuration option `--seed `) +-- If random selection is not turned on for a particular location, the first alternative in the sequence is chosen +data SourceOfND = + NDRuleSelection -- | Several rules of a funcon may "overlap" + | NDPatternMatching -- | ambiguity when multiple sequence variables occur in a pattern + | NDInterleaving -- | strict parameters in a funcon signature induce congruence rules that can be considered in different orders + | NDValueOperations -- | value operations may produce several valid results + deriving (Enum, Ord, Eq) + +defaultSources = [] + +instance Show SourceOfND where + show NDPatternMatching = "pattern-matching" + show NDInterleaving = "interleaving-of-args" + show NDValueOperations = "value-operations" + show NDRuleSelection = "rules" + defaultRunOptions :: RunOptions defaultRunOptions = RunOptions Nothing M.empty M.empty M.empty M.empty @@ -57,9 +75,18 @@ do_refocus :: RunOptions -> Bool do_refocus opts = bool_opt_default True "refocus" (general_opts opts) +turn_off_refocus :: RunOptions -> RunOptions +turn_off_refocus opts = opts { general_opts = M.insert "refocus" "false" (general_opts opts) } + +turn_on_refocus :: RunOptions -> RunOptions +turn_on_refocus opts = opts { general_opts = M.insert "refocus" "true" (general_opts opts) } + max_restarts :: RunOptions -> Maybe Int max_restarts = fmap read . M.lookup "max-restarts" . general_opts +random_seed :: RunOptions -> Int +random_seed = maybe 0 read . M.lookup "seed" . general_opts + do_abrupt_terminate :: RunOptions -> Bool do_abrupt_terminate = not . bool_opt "no-abrupt-termination" . general_opts @@ -76,6 +103,15 @@ then not (interactive_mode opts) else False +get_nd_sources :: RunOptions -> [SourceOfND] +get_nd_sources = maybe defaultSources (readSources . splitOn ",") . + M.lookup "non-deterministic" . general_opts + where readSources opts = [ source + | o <- opts + , source <- [NDRuleSelection ..] + , o == show source ] + + show_mutable :: RunOptions -> [Name] show_mutable = maybe [] (map pack . splitOn ",") . M.lookup "display-mutable-entity" . general_opts @@ -130,7 +166,8 @@ booleanOptions_ = map ("--" ++) booleanOptions stringOptions = ["display-mutable-entity", "hide-output-entity" - , "hide-control-entity", "hide-input-entity", "max-restarts"] + , "hide-control-entity", "hide-input-entity", "max-restarts" + , "seed", "non-deterministic"] stringOptions_ = map ("--" ++) stringOptions allOptions = "funcon-term" : booleanOptions ++ stringOptions @@ -232,7 +269,7 @@ pBool = "BOOL-VALUE" <:=> id_lit -- everything except `false` is considered `true` pStringValue :: Parser String -pStringValue = "STRING-VALUE" <:=> id_lit <||> string_lit +pStringValue = "STRING-VALUE" <:=> id_lit <||> string_lit <||> (show <$$> int_lit) pFunconName :: Parser String pFunconName = "FUNCON-NAME" <:=> id_lit diff --git a/src/Funcons/Tools.hs b/src/Funcons/Tools.hs --- a/src/Funcons/Tools.hs +++ b/src/Funcons/Tools.hs @@ -150,7 +150,7 @@ -- and all the desired output will already have been printed to the screen ((e_exc_f, mut, wr), rem_ins) <- fexec (runMSOS (setEntityDefaults defaults (stepTrans opts 0 (toStepRes f0))) - msos_ctxt (emptyMSOSState {inp_es = inputs})) (inputValues opts) + msos_ctxt ((emptyMSOSState (random_seed opts)){inp_es = inputs})) (inputValues opts) -- if not in --interactive-mode then print additional information based on flags unless (interactive_mode opts) (withResults defaults msos_ctxt e_exc_f mut wr rem_ins) @@ -193,7 +193,7 @@ display name = case M.lookup name muts of Nothing -> return () Just v -> putStrLn ("Mutable Entity: " ++ unpack name) >> - putStrLn (displayValue v) >> putStrLn "" + putStrLn (displayValues v) >> putStrLn "" printControl = forM_ (M.keys ctrl \\ toHide) display where ctrl = ctrl_entities wr @@ -283,11 +283,11 @@ _ -> return () printMutable = forM_ (M.assocs muts) (uncurry display) - where display name val = case M.lookup name opts of + where display name vals = case M.lookup name opts of Nothing -> return () Just expected -> unless - (map (localEval name) expected == [val]) - (reportError name (showL $ map showFuncons expected) (showValues val)) + (map (localEval name) expected == vals) + (reportError name (showL $ map showFuncons expected) (showL $ map showValues vals)) -- set default values of output and control entities ctrl :: M.Map Name (Maybe Values) @@ -331,10 +331,7 @@ val -> error ("non-list given as expected output entity ("++ unpack name ++ "): " ++ showL (map showValues val)) -showL :: [String] -> String -showL elems = "[" ++ intercalate "," elems ++ "]" - -- $moduledoc -- This module exports functions for creating executables for funcon interpeters. -- The executables accepts a number of command line and configuration options that @@ -379,6 +376,16 @@ -- this option is used to hide one or more input entities. -- * --max-restarts \: -- perform a maximum of `n` transitive steps, useful for debugging. +-- +-- * --non-deterministic : make specific parts of the interpreter non-determinstic (experimental) +-- is a comma-separated list (of length at least one) containing one or more of: +-- rules: when several rules of a funcon "overlap" +-- pattern-matching: when multiple sequence variables occur in a pattern +-- interleaving-of-args: strict parameters in a funcon signature induce congruence rules that can be considered in different orders +-- value-operations: value operations may produce several valid results (e.g. `some-element`) +-- +-- *seed : set a seed for the source of randomness, ineffective if --non-deterministic is not set +-- -- -- (4) __Boolean options__ (/true/, /false/ or no argument (/true/ by default)): -- diff --git a/src/Funcons/TypeSubstitution.hs b/src/Funcons/TypeSubstitution.hs --- a/src/Funcons/TypeSubstitution.hs +++ b/src/Funcons/TypeSubstitution.hs @@ -69,7 +69,8 @@ VPSeqVar var op -> VPSeqVar var op VPLit v -> VPLit v VPWildCard -> VPWildCard - VPType pat -> VPType pat + VPType pat -> VPType pat + VPEmptySet -> VPEmptySet instance HasTypeVar FPattern where subsTypeVarWildcard mt env pat = case pat of diff --git a/src/Funcons/Types.hs b/src/Funcons/Types.hs --- a/src/Funcons/Types.hs +++ b/src/Funcons/Types.hs @@ -184,6 +184,9 @@ list__ :: [Values] -> Values list__ = VAL.list +set__ :: [Values] -> Values +set__ = VAL.set + vector__ :: [Values] -> Values vector__ = VAL.vector @@ -206,7 +209,10 @@ -- | The empty set as a 'Funcons'. empty_set_ :: Funcons -empty_set_ = FValue (Set S.empty) +empty_set_ = FValue empty_set__ + +empty_set__ :: Values +empty_set__ = Set S.empty -- | Creates a tuple of funcon terms. --tuple_ :: [Funcons] -> Funcons diff --git a/src/Funcons/ValueOperations.hs b/src/Funcons/ValueOperations.hs --- a/src/Funcons/ValueOperations.hs +++ b/src/Funcons/ValueOperations.hs @@ -24,9 +24,8 @@ Left (_, _, exc) -> Left exc Right r -> Right r where - (e_exc_rewritten, _, _) = runRewrite rew reader state + (e_exc_rewritten, _, _) = runRewrite rew reader emptyRewriteState reader = RewriteReader (libUnions [Funcons.EDSL.library ,Funcons.Core.Manual.library]) emptyTypeRelation defaultRunOptions undefined undefined - state = RewriteState diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,13 @@ + +module Main where + +import Funcons.EDSL +import Funcons.Tools +import Funcons.Core.Manual as Manual + +import qualified Data.Map as M + +main :: IO () +main = mkMain + +