diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,373 @@ +Mozilla Public License Version 2.0 +================================== + +1. Definitions +-------------- + +1.1. "Contributor" + means each individual or legal entity that creates, contributes to + the creation of, or owns Covered Software. + +1.2. "Contributor Version" + means the combination of the Contributions of others (if any) used + by a Contributor and that particular Contributor's Contribution. + +1.3. "Contribution" + means Covered Software of a particular Contributor. + +1.4. "Covered Software" + means Source Code Form to which the initial Contributor has attached + the notice in Exhibit A, the Executable Form of such Source Code + Form, and Modifications of such Source Code Form, in each case + including portions thereof. + +1.5. "Incompatible With Secondary Licenses" + means + + (a) that the initial Contributor has attached the notice described + in Exhibit B to the Covered Software; or + + (b) that the Covered Software was made available under the terms of + version 1.1 or earlier of the License, but not also under the + terms of a Secondary License. + +1.6. "Executable Form" + means any form of the work other than Source Code Form. + +1.7. "Larger Work" + means a work that combines Covered Software with other material, in + a separate file or files, that is not Covered Software. + +1.8. "License" + means this document. + +1.9. "Licensable" + means having the right to grant, to the maximum extent possible, + whether at the time of the initial grant or subsequently, any and + all of the rights conveyed by this License. + +1.10. "Modifications" + means any of the following: + + (a) any file in Source Code Form that results from an addition to, + deletion from, or modification of the contents of Covered + Software; or + + (b) any new file in Source Code Form that contains any Covered + Software. + +1.11. "Patent Claims" of a Contributor + means any patent claim(s), including without limitation, method, + process, and apparatus claims, in any patent Licensable by such + Contributor that would be infringed, but for the grant of the + License, by the making, using, selling, offering for sale, having + made, import, or transfer of either its Contributions or its + Contributor Version. + +1.12. "Secondary License" + means either the GNU General Public License, Version 2.0, the GNU + Lesser General Public License, Version 2.1, the GNU Affero General + Public License, Version 3.0, or any later versions of those + licenses. + +1.13. "Source Code Form" + means the form of the work preferred for making modifications. + +1.14. "You" (or "Your") + means an individual or a legal entity exercising rights under this + License. For legal entities, "You" includes any entity that + controls, is controlled by, or is under common control with You. For + purposes of this definition, "control" means (a) the power, direct + or indirect, to cause the direction or management of such entity, + whether by contract or otherwise, or (b) ownership of more than + fifty percent (50%) of the outstanding shares or beneficial + ownership of such entity. + +2. License Grants and Conditions +-------------------------------- + +2.1. Grants + +Each Contributor hereby grants You a world-wide, royalty-free, +non-exclusive license: + +(a) under intellectual property rights (other than patent or trademark) + Licensable by such Contributor to use, reproduce, make available, + modify, display, perform, distribute, and otherwise exploit its + Contributions, either on an unmodified basis, with Modifications, or + as part of a Larger Work; and + +(b) under Patent Claims of such Contributor to make, use, sell, offer + for sale, have made, import, and otherwise transfer either its + Contributions or its Contributor Version. + +2.2. Effective Date + +The licenses granted in Section 2.1 with respect to any Contribution +become effective for each Contribution on the date the Contributor first +distributes such Contribution. + +2.3. Limitations on Grant Scope + +The licenses granted in this Section 2 are the only rights granted under +this License. No additional rights or licenses will be implied from the +distribution or licensing of Covered Software under this License. +Notwithstanding Section 2.1(b) above, no patent license is granted by a +Contributor: + +(a) for any code that a Contributor has removed from Covered Software; + or + +(b) for infringements caused by: (i) Your and any other third party's + modifications of Covered Software, or (ii) the combination of its + Contributions with other software (except as part of its Contributor + Version); or + +(c) under Patent Claims infringed by Covered Software in the absence of + its Contributions. + +This License does not grant any rights in the trademarks, service marks, +or logos of any Contributor (except as may be necessary to comply with +the notice requirements in Section 3.4). + +2.4. Subsequent Licenses + +No Contributor makes additional grants as a result of Your choice to +distribute the Covered Software under a subsequent version of this +License (see Section 10.2) or under the terms of a Secondary License (if +permitted under the terms of Section 3.3). + +2.5. Representation + +Each Contributor represents that the Contributor believes its +Contributions are its original creation(s) or it has sufficient rights +to grant the rights to its Contributions conveyed by this License. + +2.6. Fair Use + +This License is not intended to limit any rights You have under +applicable copyright doctrines of fair use, fair dealing, or other +equivalents. + +2.7. Conditions + +Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted +in Section 2.1. + +3. Responsibilities +------------------- + +3.1. Distribution of Source Form + +All distribution of Covered Software in Source Code Form, including any +Modifications that You create or to which You contribute, must be under +the terms of this License. You must inform recipients that the Source +Code Form of the Covered Software is governed by the terms of this +License, and how they can obtain a copy of this License. You may not +attempt to alter or restrict the recipients' rights in the Source Code +Form. + +3.2. Distribution of Executable Form + +If You distribute Covered Software in Executable Form then: + +(a) such Covered Software must also be made available in Source Code + Form, as described in Section 3.1, and You must inform recipients of + the Executable Form how they can obtain a copy of such Source Code + Form by reasonable means in a timely manner, at a charge no more + than the cost of distribution to the recipient; and + +(b) You may distribute such Executable Form under the terms of this + License, or sublicense it under different terms, provided that the + license for the Executable Form does not attempt to limit or alter + the recipients' rights in the Source Code Form under this License. + +3.3. Distribution of a Larger Work + +You may create and distribute a Larger Work under terms of Your choice, +provided that You also comply with the requirements of this License for +the Covered Software. If the Larger Work is a combination of Covered +Software with a work governed by one or more Secondary Licenses, and the +Covered Software is not Incompatible With Secondary Licenses, this +License permits You to additionally distribute such Covered Software +under the terms of such Secondary License(s), so that the recipient of +the Larger Work may, at their option, further distribute the Covered +Software under the terms of either this License or such Secondary +License(s). + +3.4. Notices + +You may not remove or alter the substance of any license notices +(including copyright notices, patent notices, disclaimers of warranty, +or limitations of liability) contained within the Source Code Form of +the Covered Software, except that You may alter any license notices to +the extent required to remedy known factual inaccuracies. + +3.5. Application of Additional Terms + +You may choose to offer, and to charge a fee for, warranty, support, +indemnity or liability obligations to one or more recipients of Covered +Software. However, You may do so only on Your own behalf, and not on +behalf of any Contributor. You must make it absolutely clear that any +such warranty, support, indemnity, or liability obligation is offered by +You alone, and You hereby agree to indemnify every Contributor for any +liability incurred by such Contributor as a result of warranty, support, +indemnity or liability terms You offer. You may include additional +disclaimers of warranty and limitations of liability specific to any +jurisdiction. + +4. Inability to Comply Due to Statute or Regulation +--------------------------------------------------- + +If it is impossible for You to comply with any of the terms of this +License with respect to some or all of the Covered Software due to +statute, judicial order, or regulation then You must: (a) comply with +the terms of this License to the maximum extent possible; and (b) +describe the limitations and the code they affect. Such description must +be placed in a text file included with all distributions of the Covered +Software under this License. Except to the extent prohibited by statute +or regulation, such description must be sufficiently detailed for a +recipient of ordinary skill to be able to understand it. + +5. Termination +-------------- + +5.1. The rights granted under this License will terminate automatically +if You fail to comply with any of its terms. However, if You become +compliant, then the rights granted under this License from a particular +Contributor are reinstated (a) provisionally, unless and until such +Contributor explicitly and finally terminates Your grants, and (b) on an +ongoing basis, if such Contributor fails to notify You of the +non-compliance by some reasonable means prior to 60 days after You have +come back into compliance. Moreover, Your grants from a particular +Contributor are reinstated on an ongoing basis if such Contributor +notifies You of the non-compliance by some reasonable means, this is the +first time You have received notice of non-compliance with this License +from such Contributor, and You become compliant prior to 30 days after +Your receipt of the notice. + +5.2. If You initiate litigation against any entity by asserting a patent +infringement claim (excluding declaratory judgment actions, +counter-claims, and cross-claims) alleging that a Contributor Version +directly or indirectly infringes any patent, then the rights granted to +You by any and all Contributors for the Covered Software under Section +2.1 of this License shall terminate. + +5.3. In the event of termination under Sections 5.1 or 5.2 above, all +end user license agreements (excluding distributors and resellers) which +have been validly granted by You or Your distributors under this License +prior to termination shall survive termination. + +************************************************************************ +* * +* 6. Disclaimer of Warranty * +* ------------------------- * +* * +* Covered Software is provided under this License on an "as is" * +* basis, without warranty of any kind, either expressed, implied, or * +* statutory, including, without limitation, warranties that the * +* Covered Software is free of defects, merchantable, fit for a * +* particular purpose or non-infringing. The entire risk as to the * +* quality and performance of the Covered Software is with You. * +* Should any Covered Software prove defective in any respect, You * +* (not any Contributor) assume the cost of any necessary servicing, * +* repair, or correction. This disclaimer of warranty constitutes an * +* essential part of this License. No use of any Covered Software is * +* authorized under this License except under this disclaimer. * +* * +************************************************************************ + +************************************************************************ +* * +* 7. Limitation of Liability * +* -------------------------- * +* * +* Under no circumstances and under no legal theory, whether tort * +* (including negligence), contract, or otherwise, shall any * +* Contributor, or anyone who distributes Covered Software as * +* permitted above, be liable to You for any direct, indirect, * +* special, incidental, or consequential damages of any character * +* including, without limitation, damages for lost profits, loss of * +* goodwill, work stoppage, computer failure or malfunction, or any * +* and all other commercial damages or losses, even if such party * +* shall have been informed of the possibility of such damages. This * +* limitation of liability shall not apply to liability for death or * +* personal injury resulting from such party's negligence to the * +* extent applicable law prohibits such limitation. Some * +* jurisdictions do not allow the exclusion or limitation of * +* incidental or consequential damages, so this exclusion and * +* limitation may not apply to You. * +* * +************************************************************************ + +8. Litigation +------------- + +Any litigation relating to this License may be brought only in the +courts of a jurisdiction where the defendant maintains its principal +place of business and such litigation shall be governed by laws of that +jurisdiction, without reference to its conflict-of-law provisions. +Nothing in this Section shall prevent a party's ability to bring +cross-claims or counter-claims. + +9. Miscellaneous +---------------- + +This License represents the complete agreement concerning the subject +matter hereof. If any provision of this License is held to be +unenforceable, such provision shall be reformed only to the extent +necessary to make it enforceable. Any law or regulation which provides +that the language of a contract shall be construed against the drafter +shall not be used to construe this License against a Contributor. + +10. Versions of the License +--------------------------- + +10.1. New Versions + +Mozilla Foundation is the license steward. Except as provided in Section +10.3, no one other than the license steward has the right to modify or +publish new versions of this License. Each version will be given a +distinguishing version number. + +10.2. Effect of New Versions + +You may distribute the Covered Software under the terms of the version +of the License under which You originally received the Covered Software, +or under the terms of any subsequent version published by the license +steward. + +10.3. Modified Versions + +If you create software not governed by this License, and you want to +create a new license for such software, you may create and use a +modified version of this License if you rename the license and remove +any references to the name of the license steward (except to note that +such modified license differs from this License). + +10.4. Distributing Source Code Form that is Incompatible With Secondary +Licenses + +If You choose to distribute Source Code Form that is Incompatible With +Secondary Licenses under the terms of this version of the License, the +notice described in Exhibit B of this License must be attached. + +Exhibit A - Source Code Form License Notice +------------------------------------------- + + This Source Code Form is subject to the terms of the Mozilla Public + License, v. 2.0. If a copy of the MPL was not distributed with this + file, You can obtain one at http://mozilla.org/MPL/2.0/. + +If it is not possible or desirable to put the notice in a particular +file, then You may include the notice in a location (such as a LICENSE +file in a relevant directory) where a recipient would be likely to look +for such a notice. + +You may add additional accurate notices of copyright ownership. + +Exhibit B - "Incompatible With Secondary Licenses" Notice +--------------------------------------------------------- + + This Source Code Form is "Incompatible With Secondary Licenses", as + defined by the Mozilla Public License, v. 2.0. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,19 @@ +# Motor: Type-safe effectful state machines in Haskell + +*Motor* is an experimental Haskell library for building finite-state +machines with type-safe transitions and effects. It draws inspiration +from the Idris +[ST](http:/*docs.idris-lang.org*en*latest*st/state.html) library. + +## Usage + +See the [Motor module documentation on +Hackage](http://hackage.haskell.org/package/motor) for detailed usage. + +## Examples + +* [Door](examples/Door.hs) + +## License + +[Mozilla Public License Version 2.0](LICENSE) diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/motor.cabal b/motor.cabal new file mode 100644 --- /dev/null +++ b/motor.cabal @@ -0,0 +1,60 @@ +name: motor +version: 0.1.0.0 +synopsis: + Type-safe effectful state machines in Haskell +description: + /Motor/ is an experimental Haskell library for building finite-state + machines with type-safe transitions and effects. It draws inspiration + from the Idris [ST + ](http://docs.idris-lang.org/en/latest/st/state.html) library. See the + "Motor.FSM" module for documentation. +license: MPL-2.0 +license-file: LICENSE +author: Oskar Wickström +maintainer: oskar.wickstrom@gmail.com +copyright: Oskar Wickström +category: Control +build-type: Simple +extra-source-files: + CHANGELOG.md + README.md +cabal-version: >=1.10 + +source-repository head + type: git + location: https://github.com/owickstrom/motor + +library + exposed-modules: Motor.FSM + , Motor.FSM.Class + , Motor.FSM.Sugar + , Motor.FSM.Logging + -- other-modules: + -- other-extensions: + build-depends: base >=4.9 && <4.10 + , indexed + , indexed-extras + , CTRex + , reflection + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -Wall + -fno-warn-unticked-promoted-constructors + +test-suite spec + type: exitcode-stdio-1.0 + other-modules: Motor.FSMSpec + , Motor.FSMSpec.Game + hs-source-dirs: test + main-is: Main.hs + build-depends: base + , indexed + , indexed-extras + , CTRex + , motor + ghc-options: -Wall + -fno-warn-orphans + -fno-warn-missing-signatures + -fno-warn-unticked-promoted-constructors + -fno-warn-name-shadowing + default-language: Haskell2010 diff --git a/src/Motor/FSM.hs b/src/Motor/FSM.hs new file mode 100644 --- /dev/null +++ b/src/Motor/FSM.hs @@ -0,0 +1,302 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{- | /Motor/ is an experimental Haskell library for building + finite-state machines with type-safe transitions and effects. It + draws inspiration from the Idris + [ST](http://docs.idris-lang.org/en/latest/st/state.html) library. +-} +module Motor.FSM ( + + -- * Usage + -- $usage + + -- ** Indexed Monads + -- $indexed-monads + + -- ** State Actions + -- $state-actions + + -- ** Infix Operators + -- $infix + + -- ** Row Polymorphism + -- $row-polymorphism + + -- * Examples + -- $examples + + -- * API + + -- ** MonadFSM Class + MonadFSM (..) + + -- ** Resource Names + , Name (..) + + -- ** State Actions + , (:->) + , To, Add, Delete + , FromActions, NoActions, Actions , OnlyActions + + -- ** Aliases + , type (!-->) + , type (!+) + , type (!-) + + -- ** FSM + , FSM, runFSM + ) where + +import Control.Monad.IO.Class +import Control.Monad.Indexed +import Control.Monad.Indexed.State +import Control.Monad.Indexed.Trans +import Data.OpenRecords + +import Motor.FSM.Class +import Motor.FSM.Sugar + + +-- | IxStateT-based implementation of 'MonadFSM'. +newtype FSM m (i :: Row *) (o :: Row *) a = + FSM (IxStateT m (Rec i) (Rec o) a) + +instance Monad m => IxFunctor (FSM m) where + imap f (FSM ma) = FSM (imap f ma) + +instance Monad m => IxPointed (FSM m) where + ireturn a = FSM (ireturn a) + +instance Monad m => IxApplicative (FSM m) where + iap (FSM f) (FSM a) = FSM (iap f a) + +instance Monad m => IxMonad (FSM m) where + ibind f (FSM ma) = + FSM + (ibind + (\a -> + let FSM b = f a + in b) + ma) + +instance Monad m => Functor (FSM m i i) where + fmap = imap + +instance Monad m => Applicative (FSM m i i) where + pure = ireturn + (<*>) = iap + +instance Monad m => Monad (FSM m i i) where + return = ireturn + m >>= k = ibind k m + +instance IxMonadTrans FSM where + ilift = FSM . ilift + +instance MonadIO m => MonadIO (FSM m i i) where + liftIO = ilift . liftIO + +-- | Run an 'FSM' state machine and retrieve its return value. Note +-- that all resources added in the 'FSM' computation must be deleted +-- eventually, as the output row is 'Empty'. +runFSM :: Monad m => FSM m Empty Empty a -> m a +runFSM (FSM f) = fst <$> runIxStateT f empty + +instance Monad m => MonadFSM (FSM m) where + new (Name :: Name n) x = FSM (imodify ((lbl := x) .|)) + where + lbl = Label :: Label n + delete (Name :: Name n) = FSM (imodify (.- lbl)) + where + lbl = Label :: Label n + enter (Name :: Name n) x = FSM (imodify $ \s -> lbl := x .| (s .- lbl)) + where + lbl = Label :: Label n + +{- $usage +The central finite-state machine abstraction in Motor is the 'MonadFSM' type class. +'MonadFSM' is an /indexed monad/ type class, meaning that it has not one, +but /three/ type parameters: + + 1. A 'Row' of input resource states + 2. A 'Row' of output resource state + 3. A return type (just as in 'Monad') + +The 'MonadFSM' parameter kinds might look a bit scary, but they state +the same: + +@ +class IxMonad m => MonadFSM (m :: (Row *) -> (Row *) -> * -> *) where + ... +@ + +The rows describe how the FSM computation will affect the state of its +resources when evaluated. A row is essentially a type-level map, from +resource names to state types, and the FSM computation's rows describe +the resource states /before/ and /after/ the computation. + +An FSM computation @newConn@ that adds a resource named @"connection"@ +with state @Idle@ could have the following type: + +>>> :t newConn +newConn :: MonadFSM m => m r ("connection" ::= Idle :| r) () + +A computation @spawnTwoPlayers@ that adds two resources could have +this type: + +>>> :t spawnTwoPlayers +spawnTwoPlayers :: + :: MonadFSM m => + m r ("hero2" ::= Standing :| "hero1" ::= Standing :| r) () + +Motor uses the extensible records in "Data.OpenRecords", provided by +the [CTRex](https://wiki.haskell.org/CTRex) library, for row kinds. +Have a look at it's documentation to learn more about the type-level +operators available for rows. + + +-} + +{- $indexed-monads + +As mentioned above, 'MonadFSM' is an indexed monad. It uses the +definition from "Control.Monad.Indexed", in the +[indexed](https://hackage.haskell.org/package/indexed-0.1.3) +package. This means that you can use 'ibind' and friends to compose +FSM computations. + +@ +c1 >>>= \\_ -> c2 +@ + +You can combine this with the @RebindableSyntax@ language extension to +get do-syntax for FSM programs: + +@ +test :: MonadFSM m => m Empty Empty () +test = do + c1 + c2 + r <- c3 + c4 r + where + (>>) a = (>>>=) a . const + (>>=) = (>>>=) +@ + +See [24 Days of GHC Extensions: Rebindable + Syntax](https://ocharles.org.uk/blog/guest-posts/2014-12-06-rebindable-syntax.html) + for some more information on how to use @RebindableSyntax@. + +-} + +{- $state-actions +To make it easier to read and write FSM computation types, there is +some syntax sugar available. + +/State actions/ allow you two describe state changes of named +resources with a /single/ list, as opposed two writing two rows. They +also take care of matching the CTRex row combinators with the +expectations of Motor, which can be tricky to do by hand. + +There are three state actions: + +* 'Add' adds a new resource. +* 'To' transitions the state of a resource. +* 'Delete' deletes an existing resource. + +A mapping between a resource name is written using the `:->` type operator, +with a `Symbol` on the left, and a state action type on the right. Here are +some examples: + +@ +"container" :-> Add Empty + +"list" :-> To Empty NonEmpty + +"game" :-> Delete GameEnded +@ + +So, the list of mappings from resource names to state actions describe +what happens to each resource. Together with an initial row of +resources 'r', and a return value 'a', we can declare the type of an +FSM computation using the 'Actions' type: + +@ +MonadFSM m => Actions m '[ n1 :-> a1, n2 :-> a2, ... ] r a +@ + +A computation that adds two resources could have the following type: + +@ +addingTwoThings :: + MonadFSM m => + Actions m '[ "container" :-> Add Empty, "game" :-> Add Started ] r () +@ +-} + +{- $infix As an alternative to the 'Add', 'To', and 'Delete' types, +Motor offers infix operator aliases. These start with @!@ to indicate +that they can be effectful. + +The '!-->' operator is an infix alias for `To`: + +@ +useStateMachines :: + MonadFSM m => + Actions m '[ "program" :-> NotCool !--> Cool ] r () +@ + +The `!+` and `!-` are infix aliases for mappings from resource names to `Add` +and `Delete` state actions, respectively: + +@ +startNewGame :: + MonadFSM m => + Actions m '[ "game" !+ Started ] r () + +endGameWhenWon :: + MonadFSM m => + Actions m '[ "game" !- Won ] r () +@ +-} + +{- $row-polymorphism + +Because of how CTRex works, FSM computations that have a free variable as +their input row of resources, i.e. that are polymorphic in the sense of +other resource states, must list /all their actions in reverse order/. + +@ +doFourThings :: + Game m + => Actions m '[ "hero2" !- Standing + , "hero1" !- Standing + , "hero2" !+ Standing + , "hero1" !+ Standing + ] r () +doFourThings = + spawn hero1 + >>>= \_ -> spawn hero2 + >>>= \_ -> perish hero1 + >>>= \_ -> perish hero2 +@ + +This is obviously quite clumsy. If anyone has ideas on how to fix or +work around it, /please get in touch/. + +Had the @r@ been replaced by @Empty@ in the type signature above, it could +have had type @NoActions m Empty ()@ instead. +-} + + +{- $examples + +The [GitHub repository](https://github.com/owickstrom/motor) includes +some examples, check that out. +-} diff --git a/src/Motor/FSM/Class.hs b/src/Motor/FSM/Class.hs new file mode 100644 --- /dev/null +++ b/src/Motor/FSM/Class.hs @@ -0,0 +1,39 @@ +-- | The 'MonadFSM' class is the indexed monad for finite-state +-- machines. +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RebindableSyntax #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +module Motor.FSM.Class + ( MonadFSM(..) + , Name (..) + ) where + +import Control.Monad.Indexed +import Data.OpenRecords +import GHC.TypeLits (Symbol) + +-- * FSM monad + +-- | An indexed monad for finite-state machines, managing the state +-- of named resources. +class IxMonad m => MonadFSM (m :: (Row *) -> (Row *) -> * -> *) where + -- | Creates a new resource and returns its 'Name'. + new :: Name n -> a -> m r (Extend n a r) () + -- | Deletes an existing resource named by its 'Name'. + delete :: Name n -> m r (r :- n) () + -- | Replaces the state of an existing resource named by its 'Name'. + enter :: Name n -> b -> m r (n ::= b :| (r :- n)) () + +-- | A name of a resource, represented using a 'Symbol'. +data Name (n :: Symbol) where + Name :: KnownSymbol n => Name n diff --git a/src/Motor/FSM/Logging.hs b/src/Motor/FSM/Logging.hs new file mode 100644 --- /dev/null +++ b/src/Motor/FSM/Logging.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- | Simple MonadIO-based logging for 'MonadFSM' programs. +module Motor.FSM.Logging where + +import Control.Monad.IO.Class +import Data.OpenRecords +import Data.Proxy +import Data.Reflection + +import Motor.FSM + +log :: + (MonadIO (m i i), KnownSymbol n, Reifies n String) + => Name n + -> String + -> m (i :: Row *) (i :: Row *) () +log (_ :: Name n) s = liftIO (putStrLn (prefix ++ ": " ++ s)) + where prefix = reflect (Proxy :: Proxy n) diff --git a/src/Motor/FSM/Sugar.hs b/src/Motor/FSM/Sugar.hs new file mode 100644 --- /dev/null +++ b/src/Motor/FSM/Sugar.hs @@ -0,0 +1,72 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +-- | Syntactic sugar for 'MonadFSM' types. +module Motor.FSM.Sugar + ( Add(..) + , Delete(..) + , To(..) + , (:->) + , FromActions + , NoActions + , Actions + , OnlyActions + , type (!-->) + , type (!+) + , type (!-) + ) where + +import Data.OpenRecords +import GHC.TypeLits (Symbol) + +-- | Action that adds a new resource in state 's'. +newtype Add s = Add s + +-- | Action that deletes an existing resource in state 's'. +newtype Delete s = Delete s + +-- | Action that transitions the state of an existing resource from +-- state 'a' to 'b'. +data To a b = Transition a b + +-- | Mapping from 'Symbol' to some action 'k'. +data (:->) (n :: Symbol) (a :: k) + +infixr 5 :-> + +-- | Translates a list of 'Action's to a 'Row'. +type family FromActions (as :: [*]) (rs :: Row *) :: (Row *) where + FromActions '[] rs = rs + FromActions ((n :-> Add a) ': ts) r = Extend n a (FromActions ts r) + FromActions ((n :-> Delete a) ': ts) r = FromActions ts r :- n + FromActions ((n :-> To a b) ': ts) r = Extend n b (FromActions ts r :- n) + +-- | Alias for 'MonadFSM' that includes no actions. +type NoActions m (r :: Row *) a = m r r a + +-- | Alias for 'MonadFSM' that uses 'FromActions' to construct rows. +type Actions m as (r :: Row *) a = m r (FromActions as r) a + +-- | Alias for 'MonadFSM' that uses 'FromActions' to construct rows, +-- starting from an 'Empty' row, i.e. allowing no /other/ resources. +type OnlyActions m as a = Actions m as Empty a + +-- | Infix version of 'To'. +type (!-->) i o = To i o + +infixl 6 !--> + +-- | Add a named resource. Alias of 'Add'. +type (!+) (n :: Symbol) s = n :-> Add s + +infix 6 !+ + +-- | Delete a named resource. Alias of 'Delete'. +type (!-) (n :: Symbol) s = n :-> Delete s + +infix 6 !- diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,9 @@ +module Main where + +import Motor.FSMSpec () +import Motor.FSMSpec.Game () + +main :: IO () +main = do + putStrLn "\nIt compiles. Ship it!\n" + putStrLn "... OK then, it should have some tests." diff --git a/test/Motor/FSMSpec.hs b/test/Motor/FSMSpec.hs new file mode 100644 --- /dev/null +++ b/test/Motor/FSMSpec.hs @@ -0,0 +1,46 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RebindableSyntax #-} +{-# LANGUAGE TypeOperators #-} +module Motor.FSMSpec where + +import Prelude hiding ((>>), (>>=)) + +import Control.Monad.Indexed +import Data.OpenRecords + +import Motor.FSM + +data S1 = S1 +data S2 = S2 + +n1 :: Name "n1" +n1 = Name + +n2 :: Name "n2" +n2 = Name + +s1s2 :: MonadFSM m => Name n -> m r (n ::= S2 :| (r :- n)) () +s1s2 s = enter s S2 + +s2s1 :: MonadFSM m => Name n -> m r (n ::= S1 :| (r :- n)) () +s2s1 s = enter s S1 + + +dropS1 :: MonadFSM m => Name n -> m r (r :- n) () +dropS1 = delete + +test :: MonadFSM m => m Empty Empty () +test = do + new n1 S1 + s1s2 n1 + s2s1 n1 + + new n2 S2 + s1s2 n2 + s2s1 n2 + + dropS1 n1 + dropS1 n2 + where + (>>) a = (>>>=) a . const diff --git a/test/Motor/FSMSpec/Game.hs b/test/Motor/FSMSpec/Game.hs new file mode 100644 --- /dev/null +++ b/test/Motor/FSMSpec/Game.hs @@ -0,0 +1,115 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RebindableSyntax #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +module Motor.FSMSpec.Game where + +import Prelude hiding (log) + +import Control.Monad.Indexed +import Control.Monad.IO.Class +import Data.OpenRecords + +import Motor.FSM +import Motor.FSM.Logging + +-- * Game Protocol/Machine + +data Standing +data Jumping + +class MonadFSM m => Game (m :: Row * -> Row * -> * -> *) where + type State m :: * -> * + spawn :: KnownSymbol n => Name n -> m r (n ::= State m Standing :| r) () + jump :: KnownSymbol n => Name n -> m r (n ::= State m Jumping :| (r :- n)) () + land :: KnownSymbol n => Name n -> m r (n ::= State m Standing :| (r :- n)) () + perish :: KnownSymbol n => Name n -> m r (r :- n) () + +-- * Game Implemention + +newtype GameImpl m (i :: Row *) (o :: Row *) a = + GameImpl { runGameImpl :: FSM m i o a } + deriving (IxFunctor, IxPointed, IxApplicative, IxMonad, MonadFSM) + +deriving instance Monad m => Functor (GameImpl m i i) + +deriving instance Monad m => Applicative (GameImpl m i i) + +deriving instance Monad m => Monad (GameImpl m i i) + +instance (MonadIO m) => MonadIO (GameImpl m i i) where + liftIO = GameImpl . liftIO + +data GameState s where + Standing :: GameState Standing + Jumping :: GameState Jumping + +instance (MonadIO m, Monad m) => Game (GameImpl m) where + type State (GameImpl m) = GameState + spawn n = + log n "Spawning player." + >>>= const (new n Standing) + jump n = + log n "Huuuhhh!" + >>>= const (enter n Jumping) + land n = + log n "Back on safe ground." + >>>= const (enter n Standing) + perish n = + log n "Aaaaarhhh..." + >>>= const (delete n) + +hero1 :: Name "hero1" +hero1 = Name + +hero2 :: Name "hero2" +hero2 = Name + +testTwoAdds :: + Game m + => Actions m '[ "hero2" !+ State m Standing + , "hero1" !+ State m Standing + ] r () +testTwoAdds = + spawn hero1 >>>= \_ -> spawn hero2 + +testTwoDeletes :: + Game m + => Actions m '[ "hero2" !- State m Standing, "hero1" !- State m Standing] r () +testTwoDeletes = + perish hero1 >>>= \_ -> perish hero2 + +testTwoAddDeletes :: + Game m + => Actions m '[ "hero2" !- State m Standing + , "hero1" !- State m Standing + , "hero2" !+ State m Standing + , "hero1" !+ State m Standing + ] r () +testTwoAddDeletes = do + spawn hero1 + spawn hero2 + perish hero1 + perish hero2 + where + (>>) a = (>>>=) a . const + +testGame :: Game m => OnlyActions m '[] () +testGame = testTwoAdds >> testTwoDeletes + where + (>>) a = (>>>=) a . const + + +run :: Monad m => GameImpl m Empty Empty () -> m () +run g = runFSM (runGameImpl g) + +runIO :: IO () +runIO = do + run testGame + putStrLn "Game over."