{-|
Module: Language.GuardedCommands.Extended
Description: A simple extension to GCL
Copyright: (c) Stijn van Drongelen, 2014
License: MIT
Maintainer: rhymoid@gmail.com
Stability: experimental
Portability: mostly portable (deriving extensions)

A simple extension to 'Language.GuardedCommands.GCL',
including @assume@, @assert@, and declaration and assignment of variables.

-}
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFunctor #-}
module Language.GuardedCommands.Extended
    ( -- * Abstract syntax
      ExtendedGCL (..)
      
      -- * Parsing
    , pExtendedGCL
    ) where

import Control.Applicative
import Data.Data
import Text.Parser.Token

import Language.GuardedCommands

data ExtendedGCL name ty expr
    =  Declare [(name, ty)] (ExtendedGCL name ty expr)
    |  Assign [(name, expr)]
    |  Assume expr
    |  Assert expr
    |  GCL (GCL (ExtendedGCL name ty expr) expr)
    deriving (Eq,Data,Typeable)

pExtendedGCL
    :: (Monad m, TokenParsing m)
    => m name
    -> m ty
    -> m expr
    -> m (ExtendedGCL name ty expr)
pExtendedGCL pName pType pExpr = pSelf
  where
    pSelf = (\_ -> Declare)
        <$> symbol "declare" <*> commaSep1 ((,) <$> pName <* symbol ":" <*> pType)
        <*  symbol "in" <*> pSelf
        <|> (\_ -> Assume) <$> symbol "assume" <*> pExpr
        <|> (\_ -> Assert) <$> symbol "assert" <*> pExpr
        <|> (processAssign =<< ((,) <$> commaSep1 pName <* symbol ":=" <*> commaSep1 pExpr))
        <|> GCL <$> pGCL pSelf pExpr

    processAssign (lvs, rvs)
        | length lvs == length rvs = pure . Assign $ zip lvs rvs
        | True = empty