diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. 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/language-gcl.cabal b/language-gcl.cabal new file mode 100644 --- /dev/null +++ b/language-gcl.cabal @@ -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 diff --git a/src/Language/GuardedCommands.hs b/src/Language/GuardedCommands.hs new file mode 100644 --- /dev/null +++ b/src/Language/GuardedCommands.hs @@ -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. + + +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