{-|
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