language-gcl (empty) → 0.1

raw patch · 4 files changed

+184/−0 lines, 4 filesdep +basedep +bifunctorsdep +parserssetup-changed

Dependencies added: base, bifunctors, parsers

Files

LICENSE +19/−0
Setup.hs +2/−0
language-gcl.cabal +26/−0
src/Language/GuardedCommands.hs +137/−0

+ LICENSE view

@@ -0,0 +1,19 @@+Copyright (c) 2014 Stijn van Drongelen++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in+all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN+THE SOFTWARE.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ language-gcl.cabal view

@@ -0,0 +1,26 @@+name:               language-gcl+version:            0.1+synopsis:           Something similar to Dijkstra's guarded command language+description:+    language-gcl provides the abstract syntax and parsers for+    basic building blocks for programming languages,+    based on Edsger W. Dijkstra's guarded command language.+license:            MIT+license-file:       LICENSE+author:             Stijn van Drongelen+maintainer:         rhymoid@gmail.com+category:           Language+build-type:         Simple+cabal-version:      >=1.10+tested-with:        GHC==7.6.3++library+    exposed-modules:+        Language.GuardedCommands+    build-depends:+        base        >=4 && <5,+        parsers            <1,+        bifunctors         <5+    hs-source-dirs:     src+    default-language:   Haskell2010+    ghc-options:        -Wall

+ src/Language/GuardedCommands.hs view

@@ -0,0 +1,137 @@+{-|+Module: Language.GuardedCommands+Description: A language similar to Dijkstra's guarded command language+Copyright: (c) Stijn van Drongelen, 2014+License: MIT+Maintainer: rhymoid@gmail.com+Stability: experimental+Portability: mostly portable (deriving extensions)++A language with guarded commands, heavily based on:++* Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs.+  /Commun. ACM 18/, 8 (August 1975), 453–457.+  <http://doi.acm.org/10.1145/360933.360975 DOI=10.1145/360933.360975>++With regards to the above source, the following assumptions were made:++* Guarded command sets may be empty, and __skip__ and __abort__ are keywords.++* The __while__ /guard/ __do__ /stmts.../ __od__ notation used on page 457+  is allowed and is syntactic sugar for __do__ /guard/ __→__ /stmts.../ __od__.++Furthermore, the language is extended so that the blocks denoted+by __do__ /.../ __od__ may be preceded by zero or more loop invariants+(written: __invariant__ /guard/).++-}+{-# LANGUAGE Haskell2010 #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+module Language.GuardedCommands+    ( -- * Abstract syntax+      GCL (..)+    , GC (..)+    +      -- * Parsing+      -- | Parsers based on the 'Text.Parser.Combinators.TokenParsing' class.+      --+      --   By overriding 'Text.Parser.Combinators.TokenParsing.token' appropriately,+      --   the keywords (@words \"□ → if fi do od abort skip invariant while  \"@)+      --   may take on different forms or even be forbidden.+    , pGCL+    , pGuardedCommandSet+    , pGuardedCommand+    , pGuardedList+    ) where++import Control.Applicative+import Data.Bifunctor+import Data.Data (Data, Typeable)+import Data.Foldable (Foldable)+import Data.Traversable (Traversable)+import Text.Parser.Combinators+import Text.Parser.Token++-- | Guarded statements+data GCL stmt guard+    = -- | Alternative statement.+      -- If none of the guards is true, the command diverges;+      -- otherwise, an arbitrary guarded list with a true guard is executed.+       Alternative           [GC stmt guard]+      -- | Repetitive statement.+      -- If none of the guards is true, the command terminates;+      -- otherwise, an arbitrary guarded list with a true guard is executed (the \'iteration\'),+      -- after which the entire repetitive statement is executed again.+      -- Before and after every iteration, all loop invariants must hold.+    |  Repetitive   [guard]  [GC stmt guard]+      -- | Some user-defined statement.+    |  Statement   stmt+    deriving (Eq,Foldable,Functor,Data,Traversable,Typeable)++instance Bifunctor GCL where+    bimap f g (Alternative gss) = Alternative (map (bimap f g) gss)+    bimap f g (Repetitive invs gss) = Repetitive (map g invs) (map (bimap f g) gss)+    bimap f _ (Statement stmt) = Statement (f stmt)++-- | Guarded commands+data GC stmt guard = GC guard [GCL stmt guard]+    deriving (Eq,Foldable,Functor,Data,Traversable,Typeable)++instance Bifunctor GC where+    bimap f g (GC gd gl) = GC (g gd) (map (bimap f g) gl)++-- | Parse a guarded statement, given parsers for user-defined statments and for guards.+pGCL+    :: TokenParsing m+    => m stmt+    -> m guard+    -> m (GCL stmt guard)+pGCL pStmt pGuard = pSelf+  where+    pGcsBlock bra ket+        = between (symbol bra) (symbol ket)+        $ pGuardedCommandSet pGuard pSelf++    pLoopInvs = many (symbol "invariant" *> pGuard)++    pSelf = Alternative <$> pGcsBlock "if" "fi"+        <|> procWhile <$> symbol "while" <*> pGuard <*> pLoopInvs+        <*> between (symbol "do") (symbol "od") (pGuardedList pSelf)+        <|> Repetitive <$> pLoopInvs <*> pGcsBlock "do" "od"+        <|> Alternative [] <$ symbol "abort"+        <|> Repetitive [] [] <$ symbol "skip"+        <|> Statement <$> pStmt++    procWhile _ g invs stmts = Repetitive invs [GC g stmts]++-- | Parse a guarded command set, given parsers for guards and guarded statements.+--+--   The guarded commands are separated by a 'white box' (U+25A1) symbol,+--   although one might argue that Dijkstra used a 'white vertical rectangle' (U+25AF).+pGuardedCommandSet+    :: TokenParsing m+    => m guard -> m (GCL stmt guard) -> m [GC stmt guard]+pGuardedCommandSet pGuard pTheGCL+    = pGuardedCommand pGuard pTheGCL `sepBy` symbol "□"+    -- There are a few alternatives (U+25AF, U+25 or the string @"[]"@)++-- | Parse a guarded command, given parsers for guards and guarded statements.+--+--   The guard and the guarded list are separated by a 'rightwards arrow' (U+2192) symbol.+pGuardedCommand+    :: TokenParsing m+    => m guard -> m (GCL stmt guard) -> m (GC stmt guard)+pGuardedCommand pGuard pTheGCL+    = GC <$> pGuard <* symbol "→" <*> pGuardedList pTheGCL++-- | Parse a guarded list, given a parser for guarded statements.+--+--   The guarded statements are separated by a semicolon.+--   This function is equal to a type-restricted 'Text.Parser.Combinators.TokenParsing.semiSep1'.+pGuardedList+    :: TokenParsing m+    => m (GCL stmt guard) -> m [GCL stmt guard]+pGuardedList = semiSep1