packages feed

funcons-tools 0.2.0.13 → 0.2.0.15

raw patch · 61 files changed

+1935/−370 lines, 61 filesdep +randomdep −TypeComposedep −random-stringsdep ~exploring-interpretersdep ~haskelinenew-component:exe:runfctPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: random

Dependencies removed: TypeCompose, random-strings

Dependency ranges changed: exploring-interpreters, haskeline

API changes (from Hackage documentation)

+ Funcons.Core: after_effect_ :: [Funcons] -> Funcons
+ Funcons.Core: allocate_index_ :: [Funcons] -> Funcons
+ Funcons.Core: barrier_create_ :: [Funcons] -> Funcons
+ Funcons.Core: barrier_sync_ :: [Funcons] -> Funcons
+ Funcons.Core: barrier_sync_else_wait_ :: [Funcons] -> Funcons
+ Funcons.Core: condition_create_ :: Funcons
+ Funcons.Core: condition_notify_all_ :: [Funcons] -> Funcons
+ Funcons.Core: condition_notify_first_ :: [Funcons] -> Funcons
+ Funcons.Core: condition_wait_ :: [Funcons] -> Funcons
+ Funcons.Core: condition_wait_with_lock_ :: [Funcons] -> Funcons
+ Funcons.Core: current_thread_ :: Funcons
+ Funcons.Core: current_thread_schedule_ :: Funcons
+ Funcons.Core: exclusive_lock_create_ :: Funcons
+ Funcons.Core: exclusive_lock_release_ :: [Funcons] -> Funcons
+ Funcons.Core: exclusive_lock_sync_ :: [Funcons] -> Funcons
+ Funcons.Core: exclusive_lock_sync_else_wait_ :: [Funcons] -> Funcons
+ Funcons.Core: initialise_active_thread_set_ :: Funcons
+ Funcons.Core: initialise_index_ :: Funcons
+ Funcons.Core: initialise_memo_value_ :: [Funcons] -> Funcons
+ Funcons.Core: initialise_memos_ :: [Funcons] -> Funcons
+ Funcons.Core: initialise_multithreading_ :: Funcons
+ Funcons.Core: initialise_terminated_thread_map_ :: Funcons
+ Funcons.Core: initialise_thread_map_ :: Funcons
+ Funcons.Core: initialise_thread_schedule_ :: Funcons
+ Funcons.Core: initialise_thread_stepping_ :: Funcons
+ Funcons.Core: is_exclusive_lock_holder_ :: [Funcons] -> Funcons
+ Funcons.Core: is_rendezvous_match_ :: [Funcons] -> Funcons
+ Funcons.Core: is_some_thread_active_ :: Funcons
+ Funcons.Core: is_some_thread_suspended_ :: Funcons
+ Funcons.Core: is_sync_feature_ :: [Funcons] -> Funcons
+ Funcons.Core: is_thread_preemptible_ :: [Funcons] -> Funcons
+ Funcons.Core: is_thread_terminated_ :: [Funcons] -> Funcons
+ Funcons.Core: lookup_index_ :: [Funcons] -> Funcons
+ Funcons.Core: memo_value_ :: [Funcons] -> Funcons
+ Funcons.Core: memo_value_recall_ :: [Funcons] -> Funcons
+ Funcons.Core: multithread_ :: [Funcons] -> Funcons
+ Funcons.Core: postpone_ :: [Funcons] -> Funcons
+ Funcons.Core: postpone_after_effect_ :: [Funcons] -> Funcons
+ Funcons.Core: reentrant_lock_create_ :: Funcons
+ Funcons.Core: reentrant_lock_exit_ :: [Funcons] -> Funcons
+ Funcons.Core: reentrant_lock_release_ :: [Funcons] -> Funcons
+ Funcons.Core: reentrant_lock_sync_ :: [Funcons] -> Funcons
+ Funcons.Core: reentrant_lock_sync_else_wait_ :: [Funcons] -> Funcons
+ Funcons.Core: rendezvous_create_ :: [Funcons] -> Funcons
+ Funcons.Core: rendezvous_first_match_drop_ :: [Funcons] -> Funcons
+ Funcons.Core: rendezvous_first_match_thread_ :: [Funcons] -> Funcons
+ Funcons.Core: rendezvous_sync_ :: [Funcons] -> Funcons
+ Funcons.Core: rendezvous_sync_else_wait_ :: [Funcons] -> Funcons
+ Funcons.Core: rendezvous_waits_ :: Funcons
+ Funcons.Core: rw_lock_create_ :: Funcons
+ Funcons.Core: rw_lock_release_exclusive_ :: [Funcons] -> Funcons
+ Funcons.Core: rw_lock_release_shared_ :: [Funcons] -> Funcons
+ Funcons.Core: rw_lock_sync_ :: [Funcons] -> Funcons
+ Funcons.Core: rw_lock_sync_all_shared_ :: [Funcons] -> Funcons
+ Funcons.Core: rw_lock_sync_exclusive_ :: [Funcons] -> Funcons
+ Funcons.Core: rw_lock_sync_exclusive_else_wait_ :: [Funcons] -> Funcons
+ Funcons.Core: rw_lock_sync_shared_ :: [Funcons] -> Funcons
+ Funcons.Core: rw_lock_sync_shared_else_wait_ :: [Funcons] -> Funcons
+ Funcons.Core: semaphore_create_ :: [Funcons] -> Funcons
+ Funcons.Core: semaphore_release_ :: [Funcons] -> Funcons
+ Funcons.Core: semaphore_sync_ :: [Funcons] -> Funcons
+ Funcons.Core: semaphore_sync_else_wait_ :: [Funcons] -> Funcons
+ Funcons.Core: spin_lock_create_ :: Funcons
+ Funcons.Core: spin_lock_release_ :: [Funcons] -> Funcons
+ Funcons.Core: spin_lock_sync_ :: [Funcons] -> Funcons
+ Funcons.Core: stepAfter_effect :: [Funcons] -> Rewrite Rewritten
+ Funcons.Core: stepAllocate_index :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepBarrier_create :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepBarrier_sync :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepBarrier_sync_else_wait :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepCondition_create :: Rewrite Rewritten
+ Funcons.Core: stepCondition_notify_all :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepCondition_notify_first :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepCondition_wait :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepCondition_wait_with_lock :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepCurrent_thread :: Rewrite Rewritten
+ Funcons.Core: stepCurrent_thread_schedule :: Rewrite Rewritten
+ Funcons.Core: stepExclusive_lock_create :: Rewrite Rewritten
+ Funcons.Core: stepExclusive_lock_release :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepExclusive_lock_sync :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepExclusive_lock_sync_else_wait :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepInitialise_active_thread_set :: Rewrite Rewritten
+ Funcons.Core: stepInitialise_index :: Rewrite Rewritten
+ Funcons.Core: stepInitialise_memo_value :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepInitialise_memos :: [Funcons] -> Rewrite Rewritten
+ Funcons.Core: stepInitialise_multithreading :: Rewrite Rewritten
+ Funcons.Core: stepInitialise_terminated_thread_map :: Rewrite Rewritten
+ Funcons.Core: stepInitialise_thread_map :: Rewrite Rewritten
+ Funcons.Core: stepInitialise_thread_schedule :: Rewrite Rewritten
+ Funcons.Core: stepInitialise_thread_stepping :: Rewrite Rewritten
+ Funcons.Core: stepIs_exclusive_lock_holder :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIs_rendezvous_match :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIs_some_thread_active :: Rewrite Rewritten
+ Funcons.Core: stepIs_some_thread_suspended :: Rewrite Rewritten
+ Funcons.Core: stepIs_sync_feature :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIs_thread_preemptible :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIs_thread_terminated :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepLookup_index :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepMemo_value :: [Funcons] -> Rewrite Rewritten
+ Funcons.Core: stepMemo_value_recall :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepMultithread :: [Funcons] -> Rewrite Rewritten
+ Funcons.Core: stepPostpone :: [Funcons] -> Rewrite Rewritten
+ Funcons.Core: stepPostpone_after_effect :: [Funcons] -> Rewrite Rewritten
+ Funcons.Core: stepReentrant_lock_create :: Rewrite Rewritten
+ Funcons.Core: stepReentrant_lock_exit :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepReentrant_lock_release :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepReentrant_lock_sync :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepReentrant_lock_sync_else_wait :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRendezvous_create :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRendezvous_first_match_drop :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRendezvous_first_match_thread :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRendezvous_sync :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRendezvous_sync_else_wait :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRendezvous_waits :: Rewrite Rewritten
+ Funcons.Core: stepRw_lock_create :: Rewrite Rewritten
+ Funcons.Core: stepRw_lock_release_exclusive :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRw_lock_release_shared :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRw_lock_sync :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRw_lock_sync_all_shared :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRw_lock_sync_exclusive :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRw_lock_sync_exclusive_else_wait :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRw_lock_sync_shared :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepRw_lock_sync_shared_else_wait :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSemaphore_create :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSemaphore_release :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSemaphore_sync :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSemaphore_sync_else_wait :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSpin_lock_create :: Rewrite Rewritten
+ Funcons.Core: stepSpin_lock_release :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSpin_lock_sync :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSync :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSync_count :: Rewrite Rewritten
+ Funcons.Core: stepSync_create :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSync_feature :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSync_feature_create :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSync_feature_maps :: Rewrite Rewritten
+ Funcons.Core: stepSync_features :: Rewrite Rewritten
+ Funcons.Core: stepSync_held :: Rewrite Rewritten
+ Funcons.Core: stepSync_holder :: Rewrite Rewritten
+ Funcons.Core: stepSync_waiting_list :: Rewrite Rewritten
+ Funcons.Core: stepSync_waiting_list_add :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSync_waiting_list_head_remove :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepSyncs :: Rewrite Rewritten
+ Funcons.Core: stepThread :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_activate :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_atomic :: [Funcons] -> Rewrite Rewritten
+ Funcons.Core: stepThread_cooperative :: Rewrite Rewritten
+ Funcons.Core: stepThread_detach :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_detached :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_exterminate :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_id :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_ids :: Rewrite Rewritten
+ Funcons.Core: stepThread_join :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_joinable :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_preemptible :: Rewrite Rewritten
+ Funcons.Core: stepThread_preemtibilities :: Rewrite Rewritten
+ Funcons.Core: stepThread_resume :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_spin :: [Funcons] -> Rewrite Rewritten
+ Funcons.Core: stepThread_step :: Rewrite Rewritten
+ Funcons.Core: stepThread_suspend :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_terminate :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_value :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThread_yield :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepThreads :: Rewrite Rewritten
+ Funcons.Core: stepUpdate_thread_schedule :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepUpdate_thread_stepping :: Rewrite Rewritten
+ Funcons.Core: sync_ :: [Funcons] -> Funcons
+ Funcons.Core: sync_count_ :: Funcons
+ Funcons.Core: sync_create_ :: [Funcons] -> Funcons
+ Funcons.Core: sync_feature_ :: [Funcons] -> Funcons
+ Funcons.Core: sync_feature_create_ :: [Funcons] -> Funcons
+ Funcons.Core: sync_feature_maps_ :: Funcons
+ Funcons.Core: sync_features_ :: Funcons
+ Funcons.Core: sync_held_ :: Funcons
+ Funcons.Core: sync_holder_ :: Funcons
+ Funcons.Core: sync_waiting_list_ :: Funcons
+ Funcons.Core: sync_waiting_list_add_ :: [Funcons] -> Funcons
+ Funcons.Core: sync_waiting_list_head_remove_ :: [Funcons] -> Funcons
+ Funcons.Core: syncs_ :: Funcons
+ Funcons.Core: thread_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_activate_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_atomic_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_cooperative_ :: Funcons
+ Funcons.Core: thread_detach_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_detached_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_exterminate_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_id_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_ids_ :: Funcons
+ Funcons.Core: thread_join_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_joinable_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_preemptible_ :: Funcons
+ Funcons.Core: thread_preemtibilities_ :: Funcons
+ Funcons.Core: thread_resume_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_spin_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_step_ :: Funcons
+ Funcons.Core: thread_suspend_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_terminate_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_value_ :: [Funcons] -> Funcons
+ Funcons.Core: thread_yield_ :: [Funcons] -> Funcons
+ Funcons.Core: threads_ :: Funcons
+ Funcons.Core: update_thread_schedule_ :: [Funcons] -> Funcons
+ Funcons.Core: update_thread_stepping_ :: Funcons
+ Funcons.EDSL: VPEmptySet :: VPattern
+ Funcons.EDSL: empty_set__ :: Values
+ Funcons.EDSL: set__ :: [Values] -> Values
+ Funcons.RunOptions: NDInterleaving :: SourceOfND
+ Funcons.RunOptions: NDPatternMatching :: SourceOfND
+ Funcons.RunOptions: NDRuleSelection :: SourceOfND
+ Funcons.RunOptions: NDValueOperations :: SourceOfND
+ Funcons.RunOptions: data SourceOfND
+ Funcons.RunOptions: defaultSources :: [a]
+ Funcons.RunOptions: get_nd_sources :: RunOptions -> [SourceOfND]
+ Funcons.RunOptions: instance GHC.Classes.Eq Funcons.RunOptions.SourceOfND
+ Funcons.RunOptions: instance GHC.Classes.Ord Funcons.RunOptions.SourceOfND
+ Funcons.RunOptions: instance GHC.Enum.Enum Funcons.RunOptions.SourceOfND
+ Funcons.RunOptions: instance GHC.Show.Show Funcons.RunOptions.SourceOfND
+ Funcons.RunOptions: random_seed :: RunOptions -> Int
+ Funcons.RunOptions: turn_off_refocus :: RunOptions -> RunOptions
+ Funcons.RunOptions: turn_on_refocus :: RunOptions -> RunOptions
- Funcons.Core: adtTypeConstruct :: [Values Funcons] -> Rewrite Rewritten
+ Funcons.Core: adtTypeConstruct :: [Values] -> Rewrite Rewritten
- Funcons.Core: ieee_float_remainder_op :: Values Funcons -> Values Funcons -> Values -> Rewrite Rewritten
+ Funcons.Core: ieee_float_remainder_op :: Values Funcons -> Values Funcons -> Values Funcons -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Absolute_Value :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Absolute_Value :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Acos :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Acos :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Asin :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Asin :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Atan :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Atan :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Atan2 :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Atan2 :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Ceiling :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Ceiling :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Cos :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Cos :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Cosh :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Cosh :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Exp :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Exp :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Floor :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Floor :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Log :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Log :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Log10 :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Log10 :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Sin :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Sin :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Sinh :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Sinh :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Sqrt :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Sqrt :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Tan :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Tan :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core: stepIEEE_Float_Tanh :: [Values] -> Rewrite Rewritten
+ Funcons.Core: stepIEEE_Float_Tanh :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: adtTypeConstruct :: [Values Funcons] -> Rewrite Rewritten
+ Funcons.Core.Manual: adtTypeConstruct :: [Values] -> Rewrite Rewritten
- Funcons.Core.Manual: ieee_float_remainder_op :: Values Funcons -> Values Funcons -> Values -> Rewrite Rewritten
+ Funcons.Core.Manual: ieee_float_remainder_op :: Values Funcons -> Values Funcons -> Values Funcons -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Absolute_Value :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Absolute_Value :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Acos :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Acos :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Asin :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Asin :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Atan :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Atan :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Atan2 :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Atan2 :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Ceiling :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Ceiling :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Cos :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Cos :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Cosh :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Cosh :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Exp :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Exp :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Floor :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Floor :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Log :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Log :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Log10 :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Log10 :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Sin :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Sin :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Sinh :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Sinh :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Sqrt :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Sqrt :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Tan :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Tan :: [Values Funcons] -> Rewrite Rewritten
- Funcons.Core.Manual: stepIEEE_Float_Tanh :: [Values] -> Rewrite Rewritten
+ Funcons.Core.Manual: stepIEEE_Float_Tanh :: [Values Funcons] -> Rewrite Rewritten
- Funcons.EDSL: getMut :: Name -> MSOS Values
+ Funcons.EDSL: getMut :: Name -> MSOS [Values]
- Funcons.EDSL: getMutPatt :: Name -> VPattern -> Env -> MSOS Env
+ Funcons.EDSL: getMutPatt :: Name -> [VPattern] -> Env -> MSOS Env
- Funcons.EDSL: putMut :: Name -> Values -> MSOS ()
+ Funcons.EDSL: putMut :: Name -> [Values] -> MSOS ()
- Funcons.EDSL: type Mutable = Map Name Values
+ Funcons.EDSL: type Mutable = Map Name [Values]
- Funcons.MetaProgramming: cmp_MSOSReader :: forall (m :: Type -> Type). Interactive m => Map Name EvalFunction -> Map Name DataTypeMembers -> Funcons -> MSOSReader m
+ Funcons.MetaProgramming: cmp_MSOSReader :: forall {m :: Type -> TYPE LiftedRep}. Interactive m => FunconLibrary -> TypeRelation -> Funcons -> MSOSReader m
- Funcons.MetaProgramming: cmp_MSOSState :: forall (m :: Type -> Type). MSOSState m
+ Funcons.MetaProgramming: cmp_MSOSState :: forall {m :: Type -> Type}. MSOSState m

Files

cbs/Funcons/Core/Computations/Abnormal/Abrupting/Abrupting.hs view
@@ -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
cbs/Funcons/Core/Computations/Abnormal/Breaking/Breaking.hs view
@@ -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
cbs/Funcons/Core/Computations/Abnormal/Continuing/Continuing.hs view
@@ -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
cbs/Funcons/Core/Computations/Abnormal/Controlling/Controlling.hs view
@@ -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
cbs/Funcons/Core/Computations/Abnormal/Failing/Failing.hs view
@@ -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
+ cbs/Funcons/Core/Computations/Abnormal/Postponing/Postponing.hs view
@@ -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
cbs/Funcons/Core/Computations/Abnormal/Returning/Returning.hs view
@@ -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
cbs/Funcons/Core/Computations/Abnormal/Throwing/Throwing.hs view
@@ -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
cbs/Funcons/Core/Computations/Normal/Binding/Binding.hs view
@@ -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
cbs/Funcons/Core/Computations/Normal/Generating/Generating.hs view
@@ -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
cbs/Funcons/Core/Computations/Normal/Giving/Giving.hs view
@@ -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
+ cbs/Funcons/Core/Computations/Normal/Indexing/Indexing.hs view
@@ -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
cbs/Funcons/Core/Computations/Normal/Interacting/Interacting.hs view
@@ -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
cbs/Funcons/Core/Computations/Normal/Linking/Linking.hs view
@@ -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
+ cbs/Funcons/Core/Computations/Normal/Memos/Memos.hs view
@@ -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
cbs/Funcons/Core/Computations/Normal/Storing/Storing.hs view
@@ -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
+ cbs/Funcons/Core/Computations/Threads/Multithreading/Multithreading.hs view
@@ -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" []
+ cbs/Funcons/Core/Computations/Threads/Synchronising/Locks/Locks.hs view
@@ -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
+ cbs/Funcons/Core/Computations/Threads/Synchronising/Notifications/Notifications.hs view
@@ -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
+ cbs/Funcons/Core/Computations/Threads/Synchronising/Synchronising.hs view
@@ -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" []
cbs/Funcons/Core/Library.hs view
@@ -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     ]
cbs/Funcons/Core/Values/Abstraction/Functions/Functions.hs view
@@ -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
cbs/Funcons/Core/Values/Abstraction/Generic/Generic.hs view
@@ -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
cbs/Funcons/Core/Values/Abstraction/Patterns/Patterns.hs view
@@ -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
cbs/Funcons/Core/Values/Abstraction/Thunks/Thunks.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Bits/Bits.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Classes/Classes.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Datatypes/Datatypes.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Graphs/Graphs.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Lists/Lists.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Objects/Objects.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Records/Records.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/References/References.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Sequences/Sequences.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Strings/Strings.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Trees/Trees.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Tuples/Tuples.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Variants/Variants.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Vectors/Vectors.hs view
@@ -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
cbs/Funcons/Core/Values/Primitive/Booleans/Booleans.hs view
@@ -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
cbs/Funcons/Core/Values/Primitive/Characters/Characters.hs view
@@ -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
cbs/Funcons/Core/Values/Primitive/Floats/Floats.hs view
@@ -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
cbs/Funcons/Core/Values/Primitive/Integers/Integers.hs view
@@ -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
cbs/Funcons/Core/Values/Primitive/Null/Null.hs view
@@ -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
cbs/Funcons/Core/Values/ValueTypes/ValueTypes.hs view
@@ -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
funcons-tools.cabal view
@@ -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 (<http://plancomps.org>) 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
manual/Funcons/Core/Computations/Normal/GeneratingBuiltin.hs view
@@ -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 []) 
manual/Funcons/Core/Values/Composite/SetsBuiltin.hs view
@@ -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_)
manual/Funcons/MetaProgramming.hs view
@@ -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 [
src/Funcons/EDSL.hs view
@@ -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
src/Funcons/Entities.hs view
@@ -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)
src/Funcons/Explorer.hs view
@@ -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 <INT>        revert to the state with id <INT>\n\+            \  :debug <FCT>         start step-by-step execution of funcon term <FCT>\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"
src/Funcons/MSOS.hs view
@@ -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 +++                                        zip [i..] ((zip (replicate (length vs) Strict) +                                                          (map FValue vs))) +++                                       map bump (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))) ++ l1 +++                          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
src/Funcons/Patterns.hs view
@@ -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
src/Funcons/Printer.hs view
@@ -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
src/Funcons/RunOptions.hs view
@@ -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 <INT>`)+-- 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
src/Funcons/Tools.hs view
@@ -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 \<natural\>: --          perform a maximum of `n` transitive steps, useful for debugging.+--+--      * --non-deterministic <ND-SOURCES+>: make specific parts of the interpreter non-determinstic (experimental)+--            <ND-SOURCES+> 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 <INT>: 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)): --
src/Funcons/TypeSubstitution.hs view
@@ -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
src/Funcons/Types.hs view
@@ -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
src/Funcons/ValueOperations.hs view
@@ -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 
+ src/Main.hs view
@@ -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++