{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Fpl/As.der.hs
Description :  abstract syntax for FPL
Copyright   :  (c) Christian Maeder, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

abstract syntax for FPL, logic for functional programs
as CASL extension
-}

module Fpl.As where

-- DrIFT command
{-! global: GetRange !-}

import Common.AS_Annotation
import Common.AnnoState
import Common.Doc as Doc
import Common.DocUtils
import Common.Id
import Common.Keywords
import Common.Lexer
import Common.Parsec
import Common.Token hiding (innerList)

import Text.ParserCombinators.Parsec

import CASL.AS_Basic_CASL
import CASL.Formula
import CASL.SortItem
import CASL.OpItem
import CASL.ToDoc

import Data.Data
import Data.List (delete)
import Data.Maybe (isNothing)

type FplBasicSpec = BASIC_SPEC FplExt () TermExt

type FplTerm = TERM TermExt
type FplForm = FORMULA TermExt

data FplExt =
    FplSortItems [Annoted FplSortItem] Range
  | FplOpItems [Annoted FplOpItem] Range
  deriving (Int -> FplExt -> ShowS
[FplExt] -> ShowS
FplExt -> String
(Int -> FplExt -> ShowS)
-> (FplExt -> String) -> ([FplExt] -> ShowS) -> Show FplExt
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FplExt] -> ShowS
$cshowList :: [FplExt] -> ShowS
show :: FplExt -> String
$cshow :: FplExt -> String
showsPrec :: Int -> FplExt -> ShowS
$cshowsPrec :: Int -> FplExt -> ShowS
Show, Typeable, Typeable FplExt
Constr
DataType
Typeable FplExt =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> FplExt -> c FplExt)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c FplExt)
-> (FplExt -> Constr)
-> (FplExt -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c FplExt))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FplExt))
-> ((forall b. Data b => b -> b) -> FplExt -> FplExt)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FplExt -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FplExt -> r)
-> (forall u. (forall d. Data d => d -> u) -> FplExt -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> FplExt -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FplExt -> m FplExt)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FplExt -> m FplExt)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FplExt -> m FplExt)
-> Data FplExt
FplExt -> Constr
FplExt -> DataType
(forall b. Data b => b -> b) -> FplExt -> FplExt
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplExt -> c FplExt
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplExt
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> FplExt -> u
forall u. (forall d. Data d => d -> u) -> FplExt -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FplExt -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FplExt -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FplExt -> m FplExt
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FplExt -> m FplExt
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplExt
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplExt -> c FplExt
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FplExt)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FplExt)
$cFplOpItems :: Constr
$cFplSortItems :: Constr
$tFplExt :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> FplExt -> m FplExt
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FplExt -> m FplExt
gmapMp :: (forall d. Data d => d -> m d) -> FplExt -> m FplExt
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FplExt -> m FplExt
gmapM :: (forall d. Data d => d -> m d) -> FplExt -> m FplExt
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FplExt -> m FplExt
gmapQi :: Int -> (forall d. Data d => d -> u) -> FplExt -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FplExt -> u
gmapQ :: (forall d. Data d => d -> u) -> FplExt -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FplExt -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FplExt -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FplExt -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FplExt -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FplExt -> r
gmapT :: (forall b. Data b => b -> b) -> FplExt -> FplExt
$cgmapT :: (forall b. Data b => b -> b) -> FplExt -> FplExt
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FplExt)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FplExt)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c FplExt)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FplExt)
dataTypeOf :: FplExt -> DataType
$cdataTypeOf :: FplExt -> DataType
toConstr :: FplExt -> Constr
$ctoConstr :: FplExt -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplExt
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplExt
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplExt -> c FplExt
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplExt -> c FplExt
$cp1Data :: Typeable FplExt
Data)

data FplSortItem =
    FreeType DATATYPE_DECL
  | CaslSortItem (SORT_ITEM TermExt)
  deriving (Int -> FplSortItem -> ShowS
[FplSortItem] -> ShowS
FplSortItem -> String
(Int -> FplSortItem -> ShowS)
-> (FplSortItem -> String)
-> ([FplSortItem] -> ShowS)
-> Show FplSortItem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FplSortItem] -> ShowS
$cshowList :: [FplSortItem] -> ShowS
show :: FplSortItem -> String
$cshow :: FplSortItem -> String
showsPrec :: Int -> FplSortItem -> ShowS
$cshowsPrec :: Int -> FplSortItem -> ShowS
Show, Typeable, Typeable FplSortItem
Constr
DataType
Typeable FplSortItem =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> FplSortItem -> c FplSortItem)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c FplSortItem)
-> (FplSortItem -> Constr)
-> (FplSortItem -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c FplSortItem))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c FplSortItem))
-> ((forall b. Data b => b -> b) -> FplSortItem -> FplSortItem)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FplSortItem -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FplSortItem -> r)
-> (forall u. (forall d. Data d => d -> u) -> FplSortItem -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> FplSortItem -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FplSortItem -> m FplSortItem)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FplSortItem -> m FplSortItem)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FplSortItem -> m FplSortItem)
-> Data FplSortItem
FplSortItem -> Constr
FplSortItem -> DataType
(forall b. Data b => b -> b) -> FplSortItem -> FplSortItem
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplSortItem -> c FplSortItem
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplSortItem
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> FplSortItem -> u
forall u. (forall d. Data d => d -> u) -> FplSortItem -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FplSortItem -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FplSortItem -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FplSortItem -> m FplSortItem
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FplSortItem -> m FplSortItem
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplSortItem
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplSortItem -> c FplSortItem
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FplSortItem)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c FplSortItem)
$cCaslSortItem :: Constr
$cFreeType :: Constr
$tFplSortItem :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> FplSortItem -> m FplSortItem
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FplSortItem -> m FplSortItem
gmapMp :: (forall d. Data d => d -> m d) -> FplSortItem -> m FplSortItem
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FplSortItem -> m FplSortItem
gmapM :: (forall d. Data d => d -> m d) -> FplSortItem -> m FplSortItem
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FplSortItem -> m FplSortItem
gmapQi :: Int -> (forall d. Data d => d -> u) -> FplSortItem -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FplSortItem -> u
gmapQ :: (forall d. Data d => d -> u) -> FplSortItem -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FplSortItem -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FplSortItem -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FplSortItem -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FplSortItem -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FplSortItem -> r
gmapT :: (forall b. Data b => b -> b) -> FplSortItem -> FplSortItem
$cgmapT :: (forall b. Data b => b -> b) -> FplSortItem -> FplSortItem
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c FplSortItem)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c FplSortItem)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c FplSortItem)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FplSortItem)
dataTypeOf :: FplSortItem -> DataType
$cdataTypeOf :: FplSortItem -> DataType
toConstr :: FplSortItem -> Constr
$ctoConstr :: FplSortItem -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplSortItem
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplSortItem
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplSortItem -> c FplSortItem
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplSortItem -> c FplSortItem
$cp1Data :: Typeable FplSortItem
Data)

data FplOpItem =
    FunOp FunDef
  | CaslOpItem (OP_ITEM TermExt)
  deriving (Int -> FplOpItem -> ShowS
[FplOpItem] -> ShowS
FplOpItem -> String
(Int -> FplOpItem -> ShowS)
-> (FplOpItem -> String)
-> ([FplOpItem] -> ShowS)
-> Show FplOpItem
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FplOpItem] -> ShowS
$cshowList :: [FplOpItem] -> ShowS
show :: FplOpItem -> String
$cshow :: FplOpItem -> String
showsPrec :: Int -> FplOpItem -> ShowS
$cshowsPrec :: Int -> FplOpItem -> ShowS
Show, Typeable, Typeable FplOpItem
Constr
DataType
Typeable FplOpItem =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> FplOpItem -> c FplOpItem)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c FplOpItem)
-> (FplOpItem -> Constr)
-> (FplOpItem -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c FplOpItem))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FplOpItem))
-> ((forall b. Data b => b -> b) -> FplOpItem -> FplOpItem)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FplOpItem -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FplOpItem -> r)
-> (forall u. (forall d. Data d => d -> u) -> FplOpItem -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> FplOpItem -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FplOpItem -> m FplOpItem)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FplOpItem -> m FplOpItem)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FplOpItem -> m FplOpItem)
-> Data FplOpItem
FplOpItem -> Constr
FplOpItem -> DataType
(forall b. Data b => b -> b) -> FplOpItem -> FplOpItem
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplOpItem -> c FplOpItem
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplOpItem
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> FplOpItem -> u
forall u. (forall d. Data d => d -> u) -> FplOpItem -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FplOpItem -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FplOpItem -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FplOpItem -> m FplOpItem
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FplOpItem -> m FplOpItem
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplOpItem
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplOpItem -> c FplOpItem
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FplOpItem)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FplOpItem)
$cCaslOpItem :: Constr
$cFunOp :: Constr
$tFplOpItem :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> FplOpItem -> m FplOpItem
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FplOpItem -> m FplOpItem
gmapMp :: (forall d. Data d => d -> m d) -> FplOpItem -> m FplOpItem
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FplOpItem -> m FplOpItem
gmapM :: (forall d. Data d => d -> m d) -> FplOpItem -> m FplOpItem
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FplOpItem -> m FplOpItem
gmapQi :: Int -> (forall d. Data d => d -> u) -> FplOpItem -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FplOpItem -> u
gmapQ :: (forall d. Data d => d -> u) -> FplOpItem -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FplOpItem -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FplOpItem -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FplOpItem -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FplOpItem -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FplOpItem -> r
gmapT :: (forall b. Data b => b -> b) -> FplOpItem -> FplOpItem
$cgmapT :: (forall b. Data b => b -> b) -> FplOpItem -> FplOpItem
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FplOpItem)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FplOpItem)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c FplOpItem)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FplOpItem)
dataTypeOf :: FplOpItem -> DataType
$cdataTypeOf :: FplOpItem -> DataType
toConstr :: FplOpItem -> Constr
$ctoConstr :: FplOpItem -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplOpItem
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FplOpItem
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplOpItem -> c FplOpItem
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FplOpItem -> c FplOpItem
$cp1Data :: Typeable FplOpItem
Data)

prepPunctBar :: [Doc] -> [Doc]
prepPunctBar :: [Doc] -> [Doc]
prepPunctBar = Doc -> [Doc] -> [Doc]
punctuate (Doc
Doc.space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
bar)

printDD :: DATATYPE_DECL -> Doc
printDD :: DATATYPE_DECL -> Doc
printDD (Datatype_decl s :: SORT
s as :: [Annoted ALTERNATIVE]
as _) =
    [Doc] -> Doc
sep [SORT -> Doc
forall a. Pretty a => a -> Doc
pretty SORT
s Doc -> Doc -> Doc
<+> String -> Doc
keyword String
freeS Doc -> Doc -> Doc
<+> String -> Doc
keyword String
withS
        , [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc]
prepPunctBar
          ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Annoted ALTERNATIVE -> Doc) -> [Annoted ALTERNATIVE] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((ALTERNATIVE -> Doc) -> Annoted ALTERNATIVE -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted ALTERNATIVE -> Doc
printALTERNATIVE) [Annoted ALTERNATIVE]
as ]

instance ListCheck FplOpItem where
  innerList :: FplOpItem -> [()]
innerList i :: FplOpItem
i = case FplOpItem
i of
    FunOp _ -> [()]
    CaslOpItem oi :: OP_ITEM TermExt
oi -> OP_ITEM TermExt -> [()]
forall a. ListCheck a => a -> [()]
innerList OP_ITEM TermExt
oi

instance ListCheck FplSortItem where
  innerList :: FplSortItem -> [()]
innerList i :: FplSortItem
i = case FplSortItem
i of
    FreeType _ -> [()]
    CaslSortItem si :: SORT_ITEM TermExt
si -> SORT_ITEM TermExt -> [()]
forall a. ListCheck a => a -> [()]
innerList SORT_ITEM TermExt
si

instance Pretty FplExt where
  pretty :: FplExt -> Doc
pretty e :: FplExt
e = case FplExt
e of
    FplSortItems ds :: [Annoted FplSortItem]
ds _ ->
        String -> Doc
topSigKey (String
sortS String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Annoted FplSortItem] -> String
forall a. ListCheck a => a -> String
pluralS [Annoted FplSortItem]
ds) Doc -> Doc -> Doc
<+> (FplSortItem -> Doc) -> [Annoted FplSortItem] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos FplSortItem -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted FplSortItem]
ds
    FplOpItems ds :: [Annoted FplOpItem]
ds _ -> String -> Doc
topSigKey (String
opS String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Annoted FplOpItem] -> String
forall a. ListCheck a => a -> String
pluralS [Annoted FplOpItem]
ds) Doc -> Doc -> Doc
<+> (FplOpItem -> Doc) -> [Annoted FplOpItem] -> Doc
forall a. (a -> Doc) -> [Annoted a] -> Doc
semiAnnos FplOpItem -> Doc
forall a. Pretty a => a -> Doc
pretty [Annoted FplOpItem]
ds

instance Pretty FplSortItem where
  pretty :: FplSortItem -> Doc
pretty e :: FplSortItem
e = case FplSortItem
e of
    FreeType d :: DATATYPE_DECL
d -> DATATYPE_DECL -> Doc
printDD DATATYPE_DECL
d
    CaslSortItem s :: SORT_ITEM TermExt
s -> SORT_ITEM TermExt -> Doc
forall f. FormExtension f => SORT_ITEM f -> Doc
printSortItem SORT_ITEM TermExt
s

instance Pretty FplOpItem where
  pretty :: FplOpItem -> Doc
pretty e :: FplOpItem
e = case FplOpItem
e of
    FunOp o :: FunDef
o -> FunDef -> Doc
forall a. Pretty a => a -> Doc
pretty FunDef
o
    CaslOpItem s :: OP_ITEM TermExt
s -> OP_ITEM TermExt -> Doc
forall f. FormExtension f => OP_ITEM f -> Doc
printOpItem OP_ITEM TermExt
s

data FunDef = FunDef OP_NAME OP_HEAD (Annoted FplTerm) Range
  deriving (Int -> FunDef -> ShowS
[FunDef] -> ShowS
FunDef -> String
(Int -> FunDef -> ShowS)
-> (FunDef -> String) -> ([FunDef] -> ShowS) -> Show FunDef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FunDef] -> ShowS
$cshowList :: [FunDef] -> ShowS
show :: FunDef -> String
$cshow :: FunDef -> String
showsPrec :: Int -> FunDef -> ShowS
$cshowsPrec :: Int -> FunDef -> ShowS
Show, FunDef -> FunDef -> Bool
(FunDef -> FunDef -> Bool)
-> (FunDef -> FunDef -> Bool) -> Eq FunDef
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FunDef -> FunDef -> Bool
$c/= :: FunDef -> FunDef -> Bool
== :: FunDef -> FunDef -> Bool
$c== :: FunDef -> FunDef -> Bool
Eq, Eq FunDef
Eq FunDef =>
(FunDef -> FunDef -> Ordering)
-> (FunDef -> FunDef -> Bool)
-> (FunDef -> FunDef -> Bool)
-> (FunDef -> FunDef -> Bool)
-> (FunDef -> FunDef -> Bool)
-> (FunDef -> FunDef -> FunDef)
-> (FunDef -> FunDef -> FunDef)
-> Ord FunDef
FunDef -> FunDef -> Bool
FunDef -> FunDef -> Ordering
FunDef -> FunDef -> FunDef
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FunDef -> FunDef -> FunDef
$cmin :: FunDef -> FunDef -> FunDef
max :: FunDef -> FunDef -> FunDef
$cmax :: FunDef -> FunDef -> FunDef
>= :: FunDef -> FunDef -> Bool
$c>= :: FunDef -> FunDef -> Bool
> :: FunDef -> FunDef -> Bool
$c> :: FunDef -> FunDef -> Bool
<= :: FunDef -> FunDef -> Bool
$c<= :: FunDef -> FunDef -> Bool
< :: FunDef -> FunDef -> Bool
$c< :: FunDef -> FunDef -> Bool
compare :: FunDef -> FunDef -> Ordering
$ccompare :: FunDef -> FunDef -> Ordering
$cp1Ord :: Eq FunDef
Ord, Typeable, Typeable FunDef
Constr
DataType
Typeable FunDef =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> FunDef -> c FunDef)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c FunDef)
-> (FunDef -> Constr)
-> (FunDef -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c FunDef))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDef))
-> ((forall b. Data b => b -> b) -> FunDef -> FunDef)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FunDef -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FunDef -> r)
-> (forall u. (forall d. Data d => d -> u) -> FunDef -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> FunDef -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FunDef -> m FunDef)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FunDef -> m FunDef)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FunDef -> m FunDef)
-> Data FunDef
FunDef -> Constr
FunDef -> DataType
(forall b. Data b => b -> b) -> FunDef -> FunDef
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunDef -> c FunDef
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunDef
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> FunDef -> u
forall u. (forall d. Data d => d -> u) -> FunDef -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunDef -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunDef -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunDef -> m FunDef
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDef -> m FunDef
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunDef
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunDef -> c FunDef
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunDef)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDef)
$cFunDef :: Constr
$tFunDef :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> FunDef -> m FunDef
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDef -> m FunDef
gmapMp :: (forall d. Data d => d -> m d) -> FunDef -> m FunDef
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FunDef -> m FunDef
gmapM :: (forall d. Data d => d -> m d) -> FunDef -> m FunDef
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FunDef -> m FunDef
gmapQi :: Int -> (forall d. Data d => d -> u) -> FunDef -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FunDef -> u
gmapQ :: (forall d. Data d => d -> u) -> FunDef -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> FunDef -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunDef -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunDef -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunDef -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunDef -> r
gmapT :: (forall b. Data b => b -> b) -> FunDef -> FunDef
$cgmapT :: (forall b. Data b => b -> b) -> FunDef -> FunDef
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDef)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunDef)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c FunDef)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c FunDef)
dataTypeOf :: FunDef -> DataType
$cdataTypeOf :: FunDef -> DataType
toConstr :: FunDef -> Constr
$ctoConstr :: FunDef -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunDef
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c FunDef
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunDef -> c FunDef
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FunDef -> c FunDef
$cp1Data :: Typeable FunDef
Data)

kindHead :: OpKind -> OP_HEAD -> OP_HEAD
kindHead :: OpKind -> OP_HEAD -> OP_HEAD
kindHead k :: OpKind
k (Op_head _ args :: [VAR_DECL]
args r :: Maybe SORT
r ps :: Range
ps) = OpKind -> [VAR_DECL] -> Maybe SORT -> Range -> OP_HEAD
Op_head OpKind
k [VAR_DECL]
args Maybe SORT
r Range
ps

instance Pretty FunDef where
  pretty :: FunDef -> Doc
pretty (FunDef i :: SORT
i h :: OP_HEAD
h@(Op_head _ l :: [VAR_DECL]
l ms :: Maybe SORT
ms _) t :: Annoted FplTerm
t _) =
    let di :: Doc
di = SORT -> Doc
idLabelDoc SORT
i
        et :: Doc
et = Doc
equals Doc -> Doc -> Doc
<+> (FplTerm -> Doc) -> Annoted FplTerm -> Doc
forall a. (a -> Doc) -> Annoted a -> Doc
printAnnoted FplTerm -> Doc
forall a. Pretty a => a -> Doc
pretty Annoted FplTerm
t
    in [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ if Maybe SORT -> Bool
forall a. Maybe a -> Bool
isNothing Maybe SORT
ms Bool -> Bool -> Bool
&& [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
l then [Doc
di, Doc
et] else
      [String -> Doc
keyword String
functS,
      [Doc] -> Doc
sep [(if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
l then [Doc] -> Doc
sep else [Doc] -> Doc
cat) [Doc
di, OP_HEAD -> Doc
forall a. Pretty a => a -> Doc
pretty (OP_HEAD -> Doc) -> OP_HEAD -> Doc
forall a b. (a -> b) -> a -> b
$ OpKind -> OP_HEAD -> OP_HEAD
kindHead OpKind
Total OP_HEAD
h], Doc
et]]

{- | extra terms of FPL. if-then-else must use a term as guard with result
sort @Bool@. To allow @true@, @false@ and an equality test an extra term
parser is needed that must not be used when parsing formulas. -}
data TermExt =
    FixDef FunDef -- ^ formula
  | Case FplTerm [(FplTerm, FplTerm)] Range
  | Let FunDef FplTerm Range
  | IfThenElse FplTerm FplTerm FplTerm Range
  | EqTerm FplTerm FplTerm Range
  | BoolTerm FplTerm
  deriving (Int -> TermExt -> ShowS
[TermExt] -> ShowS
TermExt -> String
(Int -> TermExt -> ShowS)
-> (TermExt -> String) -> ([TermExt] -> ShowS) -> Show TermExt
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TermExt] -> ShowS
$cshowList :: [TermExt] -> ShowS
show :: TermExt -> String
$cshow :: TermExt -> String
showsPrec :: Int -> TermExt -> ShowS
$cshowsPrec :: Int -> TermExt -> ShowS
Show, TermExt -> TermExt -> Bool
(TermExt -> TermExt -> Bool)
-> (TermExt -> TermExt -> Bool) -> Eq TermExt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TermExt -> TermExt -> Bool
$c/= :: TermExt -> TermExt -> Bool
== :: TermExt -> TermExt -> Bool
$c== :: TermExt -> TermExt -> Bool
Eq, Eq TermExt
Eq TermExt =>
(TermExt -> TermExt -> Ordering)
-> (TermExt -> TermExt -> Bool)
-> (TermExt -> TermExt -> Bool)
-> (TermExt -> TermExt -> Bool)
-> (TermExt -> TermExt -> Bool)
-> (TermExt -> TermExt -> TermExt)
-> (TermExt -> TermExt -> TermExt)
-> Ord TermExt
TermExt -> TermExt -> Bool
TermExt -> TermExt -> Ordering
TermExt -> TermExt -> TermExt
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TermExt -> TermExt -> TermExt
$cmin :: TermExt -> TermExt -> TermExt
max :: TermExt -> TermExt -> TermExt
$cmax :: TermExt -> TermExt -> TermExt
>= :: TermExt -> TermExt -> Bool
$c>= :: TermExt -> TermExt -> Bool
> :: TermExt -> TermExt -> Bool
$c> :: TermExt -> TermExt -> Bool
<= :: TermExt -> TermExt -> Bool
$c<= :: TermExt -> TermExt -> Bool
< :: TermExt -> TermExt -> Bool
$c< :: TermExt -> TermExt -> Bool
compare :: TermExt -> TermExt -> Ordering
$ccompare :: TermExt -> TermExt -> Ordering
$cp1Ord :: Eq TermExt
Ord, Typeable, Typeable TermExt
Constr
DataType
Typeable TermExt =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> TermExt -> c TermExt)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TermExt)
-> (TermExt -> Constr)
-> (TermExt -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c TermExt))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TermExt))
-> ((forall b. Data b => b -> b) -> TermExt -> TermExt)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> TermExt -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> TermExt -> r)
-> (forall u. (forall d. Data d => d -> u) -> TermExt -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TermExt -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> TermExt -> m TermExt)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TermExt -> m TermExt)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TermExt -> m TermExt)
-> Data TermExt
TermExt -> Constr
TermExt -> DataType
(forall b. Data b => b -> b) -> TermExt -> TermExt
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TermExt -> c TermExt
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TermExt
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TermExt -> u
forall u. (forall d. Data d => d -> u) -> TermExt -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TermExt -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TermExt -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TermExt -> m TermExt
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TermExt -> m TermExt
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TermExt
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TermExt -> c TermExt
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TermExt)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TermExt)
$cBoolTerm :: Constr
$cEqTerm :: Constr
$cIfThenElse :: Constr
$cLet :: Constr
$cCase :: Constr
$cFixDef :: Constr
$tTermExt :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TermExt -> m TermExt
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TermExt -> m TermExt
gmapMp :: (forall d. Data d => d -> m d) -> TermExt -> m TermExt
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TermExt -> m TermExt
gmapM :: (forall d. Data d => d -> m d) -> TermExt -> m TermExt
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TermExt -> m TermExt
gmapQi :: Int -> (forall d. Data d => d -> u) -> TermExt -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TermExt -> u
gmapQ :: (forall d. Data d => d -> u) -> TermExt -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TermExt -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TermExt -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> TermExt -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TermExt -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> TermExt -> r
gmapT :: (forall b. Data b => b -> b) -> TermExt -> TermExt
$cgmapT :: (forall b. Data b => b -> b) -> TermExt -> TermExt
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TermExt)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TermExt)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TermExt)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TermExt)
dataTypeOf :: TermExt -> DataType
$cdataTypeOf :: TermExt -> DataType
toConstr :: TermExt -> Constr
$ctoConstr :: TermExt -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TermExt
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TermExt
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TermExt -> c TermExt
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TermExt -> c TermExt
$cp1Data :: Typeable TermExt
Data)

instance FormExtension TermExt

instance Pretty TermExt where
  pretty :: TermExt -> Doc
pretty t :: TermExt
t = case TermExt
t of
    FixDef fd :: FunDef
fd -> FunDef -> Doc
forall a. Pretty a => a -> Doc
pretty FunDef
fd
    Case c :: FplTerm
c l :: [(FplTerm, FplTerm)]
l _ ->
      [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (String -> Doc
keyword String
caseS Doc -> Doc -> Doc
<+> FplTerm -> Doc
forall a. Pretty a => a -> Doc
pretty FplTerm
c Doc -> Doc -> Doc
<+> String -> Doc
keyword String
ofS)
          Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc] -> [Doc]
prepPunctBar
            (((FplTerm, FplTerm) -> Doc) -> [(FplTerm, FplTerm)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: FplTerm
p, e :: FplTerm
e) -> [Doc] -> Doc
fsep [FplTerm -> Doc
forall a. Pretty a => a -> Doc
pretty FplTerm
p, Doc
implies, FplTerm -> Doc
forall a. Pretty a => a -> Doc
pretty FplTerm
e]) [(FplTerm, FplTerm)]
l)
    Let fd :: FunDef
fd i :: FplTerm
i _ -> [Doc] -> Doc
sep [String -> Doc
keyword String
letS Doc -> Doc -> Doc
<+> FunDef -> Doc
forall a. Pretty a => a -> Doc
pretty FunDef
fd, String -> Doc
keyword String
inS Doc -> Doc -> Doc
<+> FplTerm -> Doc
forall a. Pretty a => a -> Doc
pretty FplTerm
i]
    IfThenElse i :: FplTerm
i d :: FplTerm
d e :: FplTerm
e _ ->
        [Doc] -> Doc
fsep [ String -> Doc
keyword String
ifS Doc -> Doc -> Doc
<+> FplTerm -> Doc
forall a. Pretty a => a -> Doc
pretty FplTerm
i
             , String -> Doc
keyword String
thenS Doc -> Doc -> Doc
<+> FplTerm -> Doc
forall a. Pretty a => a -> Doc
pretty FplTerm
d
             , String -> Doc
keyword String
elseS Doc -> Doc -> Doc
<+> FplTerm -> Doc
forall a. Pretty a => a -> Doc
pretty FplTerm
e ]
    EqTerm t1 :: FplTerm
t1 t2 :: FplTerm
t2 r :: Range
r -> FORMULA TermExt -> Doc
forall a. Pretty a => a -> Doc
pretty (FORMULA TermExt -> Doc) -> FORMULA TermExt -> Doc
forall a b. (a -> b) -> a -> b
$ FplTerm -> Equality -> FplTerm -> Range -> FORMULA TermExt
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation FplTerm
t1 Equality
Strong FplTerm
t2 Range
r
    BoolTerm f :: FplTerm
f -> FplTerm -> Doc
forall a. Pretty a => a -> Doc
pretty FplTerm
f

fplReservedWords :: [String]
fplReservedWords :: [String]
fplReservedWords = [String
barS, String
functS, String
caseS, String
ofS, String
letS]

funDef :: [String] -> AParser st FunDef
funDef :: [String] -> AParser st FunDef
funDef ks :: [String]
ks = do
  Token
q <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
functS
  SORT
o <- [String] -> GenParser Char (AnnoState st) SORT
forall st. [String] -> GenParser Char st SORT
parseId [String]
ks
  OP_HEAD
h <- [String] -> AParser st OP_HEAD
forall st. [String] -> AParser st OP_HEAD
opHead [String]
ks
  Token
e <- AParser st Token
forall st. AParser st Token
equalT
  [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
  FplTerm
t <- [String] -> AParser st FplTerm
forall st. [String] -> AParser st FplTerm
eqTerm [String]
ks
  FunDef -> AParser st FunDef
forall (m :: * -> *) a. Monad m => a -> m a
return (FunDef -> AParser st FunDef) -> FunDef -> AParser st FunDef
forall a b. (a -> b) -> a -> b
$ SORT -> OP_HEAD -> Annoted FplTerm -> Range -> FunDef
FunDef SORT
o (OpKind -> OP_HEAD -> OP_HEAD
kindHead OpKind
Partial OP_HEAD
h)
    (FplTerm -> Range -> [Annotation] -> [Annotation] -> Annoted FplTerm
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted FplTerm
t Range
nullRange [Annotation]
a []) (Range -> FunDef) -> Range -> FunDef
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
q [] Token
e

optVarDecls :: [String] -> AParser st ([VAR_DECL], [Token])
optVarDecls :: [String] -> AParser st ([VAR_DECL], [Token])
optVarDecls ks :: [String]
ks =
    (CharParser (AnnoState st) Token
forall st. CharParser st Token
oParenT CharParser (AnnoState st) Token
-> AParser st ([VAR_DECL], [Token])
-> AParser st ([VAR_DECL], [Token])
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GenParser Char (AnnoState st) VAR_DECL
-> CharParser (AnnoState st) Token
-> AParser st ([VAR_DECL], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy ([String] -> GenParser Char (AnnoState st) VAR_DECL
forall st. [String] -> AParser st VAR_DECL
varDecl [String]
ks) CharParser (AnnoState st) Token
forall st. AParser st Token
anSemi AParser st ([VAR_DECL], [Token])
-> CharParser (AnnoState st) Token
-> AParser st ([VAR_DECL], [Token])
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< CharParser (AnnoState st) Token
forall st. CharParser st Token
cParenT)
    AParser st ([VAR_DECL], [Token])
-> AParser st ([VAR_DECL], [Token])
-> AParser st ([VAR_DECL], [Token])
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([VAR_DECL], [Token]) -> AParser st ([VAR_DECL], [Token])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])

constBool :: AParser st FplTerm
constBool :: AParser st FplTerm
constBool = (Token -> FplTerm)
-> ParsecT String (AnnoState st) Identity Token
-> AParser st FplTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Token -> FplTerm
forall f. Token -> TERM f
Mixfix_token (String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
trueS ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> ParsecT String (AnnoState st) Identity Token
forall st. String -> AParser st Token
asKey String
falseS)

boolTerm :: [String] -> AParser st FplTerm
boolTerm :: [String] -> AParser st FplTerm
boolTerm ks :: [String]
ks = AParser st FplTerm
forall st. AParser st FplTerm
constBool AParser st FplTerm -> AParser st FplTerm -> AParser st FplTerm
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st FplTerm
forall f st. TermParser f => [String] -> AParser st (TERM f)
mixTerm [String]
ks

eqTerm :: [String] -> AParser st FplTerm
eqTerm :: [String] -> AParser st FplTerm
eqTerm ks :: [String]
ks = do
  FplTerm
b <- [String] -> AParser st FplTerm
forall st. [String] -> AParser st FplTerm
boolTerm [String]
ks
  FplTerm -> AParser st FplTerm -> AParser st FplTerm
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option FplTerm
b (AParser st FplTerm -> AParser st FplTerm)
-> AParser st FplTerm -> AParser st FplTerm
forall a b. (a -> b) -> a -> b
$ do
    Token
e <- AParser st Token
forall st. AParser st Token
equalT
    FplTerm
b2 <- [String] -> AParser st FplTerm
forall st. [String] -> AParser st FplTerm
boolTerm [String]
ks
    FplTerm -> AParser st FplTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FplTerm -> AParser st FplTerm) -> FplTerm -> AParser st FplTerm
forall a b. (a -> b) -> a -> b
$ TermExt -> FplTerm
forall f. f -> TERM f
ExtTERM (TermExt -> FplTerm) -> TermExt -> FplTerm
forall a b. (a -> b) -> a -> b
$ FplTerm -> FplTerm -> Range -> TermExt
EqTerm FplTerm
b FplTerm
b2 (Range -> TermExt) -> Range -> TermExt
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
e

{- | extra formulas to compare bool terms with true or false.
Interpreting boolean valued terms as formulas is still missing. -}
eqForm :: [String] -> AParser st TermExt
eqForm :: [String] -> AParser st TermExt
eqForm ks :: [String]
ks = do
    (c :: FplTerm
c, t :: Token
t) <- GenParser Char (AnnoState st) (FplTerm, Token)
-> GenParser Char (AnnoState st) (FplTerm, Token)
forall tok st a. GenParser tok st a -> GenParser tok st a
try (GenParser Char (AnnoState st) (FplTerm, Token)
 -> GenParser Char (AnnoState st) (FplTerm, Token))
-> GenParser Char (AnnoState st) (FplTerm, Token)
-> GenParser Char (AnnoState st) (FplTerm, Token)
forall a b. (a -> b) -> a -> b
$ ParsecT String (AnnoState st) Identity FplTerm
-> ParsecT String (AnnoState st) Identity Token
-> GenParser Char (AnnoState st) (FplTerm, Token)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair ParsecT String (AnnoState st) Identity FplTerm
forall st. AParser st FplTerm
constBool ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
equalT
    FplTerm
e <- [String] -> ParsecT String (AnnoState st) Identity FplTerm
forall f st. TermParser f => [String] -> AParser st (TERM f)
mixTerm [String]
ks
    TermExt -> AParser st TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> AParser st TermExt) -> TermExt -> AParser st TermExt
forall a b. (a -> b) -> a -> b
$ FplTerm -> FplTerm -> Range -> TermExt
EqTerm FplTerm
c FplTerm
e (Range -> TermExt) -> Range -> TermExt
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
t
  AParser st TermExt -> AParser st TermExt -> AParser st TermExt
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ((FplTerm, (Token, FplTerm)) -> TermExt)
-> ParsecT
     String (AnnoState st) Identity (FplTerm, (Token, FplTerm))
-> AParser st TermExt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (e :: FplTerm
e, (t :: Token
t, c :: FplTerm
c)) -> FplTerm -> FplTerm -> Range -> TermExt
EqTerm FplTerm
e FplTerm
c (Range -> TermExt) -> Range -> TermExt
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
t)
    (ParsecT String (AnnoState st) Identity (FplTerm, (Token, FplTerm))
-> ParsecT
     String (AnnoState st) Identity (FplTerm, (Token, FplTerm))
forall tok st a. GenParser tok st a -> GenParser tok st a
try (ParsecT String (AnnoState st) Identity (FplTerm, (Token, FplTerm))
 -> ParsecT
      String (AnnoState st) Identity (FplTerm, (Token, FplTerm)))
-> ParsecT
     String (AnnoState st) Identity (FplTerm, (Token, FplTerm))
-> ParsecT
     String (AnnoState st) Identity (FplTerm, (Token, FplTerm))
forall a b. (a -> b) -> a -> b
$ ParsecT String (AnnoState st) Identity FplTerm
-> ParsecT String (AnnoState st) Identity (Token, FplTerm)
-> ParsecT
     String (AnnoState st) Identity (FplTerm, (Token, FplTerm))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair ([String] -> ParsecT String (AnnoState st) Identity FplTerm
forall f st. TermParser f => [String] -> AParser st (TERM f)
mixTerm [String]
ks) (ParsecT String (AnnoState st) Identity (Token, FplTerm)
 -> ParsecT
      String (AnnoState st) Identity (FplTerm, (Token, FplTerm)))
-> ParsecT String (AnnoState st) Identity (Token, FplTerm)
-> ParsecT
     String (AnnoState st) Identity (FplTerm, (Token, FplTerm))
forall a b. (a -> b) -> a -> b
$ ParsecT String (AnnoState st) Identity Token
-> ParsecT String (AnnoState st) Identity FplTerm
-> ParsecT String (AnnoState st) Identity (Token, FplTerm)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair ParsecT String (AnnoState st) Identity Token
forall st. AParser st Token
equalT ParsecT String (AnnoState st) Identity FplTerm
forall st. AParser st FplTerm
constBool)

fplTerm :: [String] -> AParser st TermExt
fplTerm :: [String] -> AParser st TermExt
fplTerm ks :: [String]
ks = [String] -> AParser st TermExt
forall st. [String] -> AParser st TermExt
caseTerm [String]
ks AParser st TermExt -> AParser st TermExt -> AParser st TermExt
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st TermExt
forall st. [String] -> AParser st TermExt
letTerm [String]
ks AParser st TermExt -> AParser st TermExt -> AParser st TermExt
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st TermExt
forall st. [String] -> AParser st TermExt
ifThenElse [String]
ks

caseTerm :: [String] -> AParser st TermExt
caseTerm :: [String] -> AParser st TermExt
caseTerm ks :: [String]
ks = do
  Token
c <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
caseS
  FplTerm
t <- [String] -> AParser st FplTerm
forall st. [String] -> AParser st FplTerm
eqTerm [String]
ks
  Token
o <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
ofS
  (cs :: [(FplTerm, FplTerm)]
cs, qs :: [Token]
qs) <- GenParser Char (AnnoState st) (FplTerm, FplTerm)
-> AParser st Token
-> GenParser Char (AnnoState st) ([(FplTerm, FplTerm)], [Token])
forall tok st a b.
GenParser tok st a
-> GenParser tok st b -> GenParser tok st ([a], [b])
separatedBy ([String] -> GenParser Char (AnnoState st) (FplTerm, FplTerm)
forall st. [String] -> AParser st (FplTerm, FplTerm)
patTermPair [String]
ks) AParser st Token
forall st. AParser st Token
barT
  TermExt -> AParser st TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> AParser st TermExt) -> TermExt -> AParser st TermExt
forall a b. (a -> b) -> a -> b
$ FplTerm -> [(FplTerm, FplTerm)] -> Range -> TermExt
Case FplTerm
t [(FplTerm, FplTerm)]
cs (Range -> TermExt) -> Range -> TermExt
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
c [Token]
qs Token
o

patTermPair :: [String] -> AParser st (FplTerm, FplTerm)
patTermPair :: [String] -> AParser st (FplTerm, FplTerm)
patTermPair ks :: [String]
ks = do
  FplTerm
p <- [String] -> AParser st FplTerm
forall st. [String] -> AParser st FplTerm
eqTerm [String]
ks
  AParser st Token
forall st. AParser st Token
implKey
  FplTerm
t <- [String] -> AParser st FplTerm
forall st. [String] -> AParser st FplTerm
eqTerm [String]
ks
  (FplTerm, FplTerm) -> AParser st (FplTerm, FplTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (FplTerm
p, FplTerm
t)

letVar :: [String] -> AParser st FunDef
letVar :: [String] -> AParser st FunDef
letVar ks :: [String]
ks = do
  Token
v <- [String] -> GenParser Char (AnnoState st) Token
forall st. [String] -> GenParser Char st Token
varId [String]
ks
  Token
e <- GenParser Char (AnnoState st) Token
forall st. AParser st Token
equalT
  [Annotation]
a <- AParser st [Annotation]
forall st. AParser st [Annotation]
annos
  FplTerm
t <- [String] -> AParser st FplTerm
forall st. [String] -> AParser st FplTerm
eqTerm [String]
ks
  FunDef -> AParser st FunDef
forall (m :: * -> *) a. Monad m => a -> m a
return (FunDef -> AParser st FunDef) -> FunDef -> AParser st FunDef
forall a b. (a -> b) -> a -> b
$ SORT -> OP_HEAD -> Annoted FplTerm -> Range -> FunDef
FunDef (Token -> SORT
simpleIdToId Token
v) (OpKind -> [VAR_DECL] -> Maybe SORT -> Range -> OP_HEAD
Op_head OpKind
Partial [] Maybe SORT
forall a. Maybe a
Nothing Range
nullRange)
    (FplTerm -> Range -> [Annotation] -> [Annotation] -> Annoted FplTerm
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted FplTerm
t Range
nullRange [Annotation]
a []) (Range -> FunDef) -> Range -> FunDef
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
e

letTerm :: [String] -> AParser st TermExt
letTerm :: [String] -> AParser st TermExt
letTerm ks :: [String]
ks = do
  Token
l <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
letS
  FunDef
d <- [String] -> AParser st FunDef
forall st. [String] -> AParser st FunDef
funDef [String]
ks AParser st FunDef -> AParser st FunDef -> AParser st FunDef
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st FunDef
forall st. [String] -> AParser st FunDef
letVar [String]
ks
  Token
i <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
inS
  FplTerm
t <- [String] -> AParser st FplTerm
forall f st. TermParser f => [String] -> AParser st (TERM f)
term [String]
ks
  TermExt -> AParser st TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> AParser st TermExt) -> TermExt -> AParser st TermExt
forall a b. (a -> b) -> a -> b
$ FunDef -> FplTerm -> Range -> TermExt
Let FunDef
d FplTerm
t (Range -> TermExt) -> Range -> TermExt
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
l [] Token
i

ifThenElse :: [String] -> AParser st TermExt
ifThenElse :: [String] -> AParser st TermExt
ifThenElse ks :: [String]
ks = do
  Token
i <- AParser st Token
forall st. AParser st Token
ifKey
  FplTerm
f <- [String] -> AParser st FplTerm
forall st. [String] -> AParser st FplTerm
eqTerm [String]
ks
  Token
t <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
thenS
  FplTerm
a <- [String] -> AParser st FplTerm
forall st. [String] -> AParser st FplTerm
eqTerm [String]
ks
  Token
e <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
elseS
  FplTerm
b <- [String] -> AParser st FplTerm
forall st. [String] -> AParser st FplTerm
eqTerm [String]
ks
  TermExt -> AParser st TermExt
forall (m :: * -> *) a. Monad m => a -> m a
return (TermExt -> AParser st TermExt) -> TermExt -> AParser st TermExt
forall a b. (a -> b) -> a -> b
$ FplTerm -> FplTerm -> FplTerm -> Range -> TermExt
IfThenElse FplTerm
f FplTerm
a FplTerm
b (Range -> TermExt) -> Range -> TermExt
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> Token -> Range
toRange Token
i [Token
t] Token
e

instance TermParser TermExt where
  termParser :: Bool -> AParser st TermExt
termParser b :: Bool
b = if Bool
b then [String] -> AParser st TermExt
forall st. [String] -> AParser st TermExt
fplTerm [String]
fplReservedWords else
    (FunDef -> TermExt)
-> ParsecT String (AnnoState st) Identity FunDef
-> AParser st TermExt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FunDef -> TermExt
FixDef ([String] -> ParsecT String (AnnoState st) Identity FunDef
forall st. [String] -> AParser st FunDef
funDef [String]
fplReservedWords) AParser st TermExt -> AParser st TermExt -> AParser st TermExt
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String] -> AParser st TermExt
forall st. [String] -> AParser st TermExt
eqForm [String]
fplReservedWords

fplExt :: [String] -> AParser st FplExt
fplExt :: [String] -> AParser st FplExt
fplExt ks :: [String]
ks = [String]
-> String
-> ([String] -> AParser st FplSortItem)
-> ([Annoted FplSortItem] -> Range -> FplExt)
-> AParser st FplExt
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList [String]
ks String
sortS [String] -> AParser st FplSortItem
forall st. [String] -> AParser st FplSortItem
fplSortItem [Annoted FplSortItem] -> Range -> FplExt
FplSortItems
  AParser st FplExt -> AParser st FplExt -> AParser st FplExt
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String]
-> String
-> ([String] -> AParser st FplOpItem)
-> ([Annoted FplOpItem] -> Range -> FplExt)
-> AParser st FplExt
forall st b a.
[String]
-> String
-> ([String] -> AParser st b)
-> ([Annoted b] -> Range -> a)
-> AParser st a
itemList (String -> [String] -> [String]
forall a. Eq a => a -> [a] -> [a]
delete String
functS [String]
ks) String
opS [String] -> AParser st FplOpItem
forall st. [String] -> AParser st FplOpItem
fplOpItem [Annoted FplOpItem] -> Range -> FplExt
FplOpItems
  AParser st FplExt -> AParser st FplExt -> AParser st FplExt
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ((String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
etypeS CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
typeS CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
predS
      CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> CharParser (AnnoState st) Token
forall st. String -> CharParser st Token
pluralKeyword String
esortS CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> CharParser (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
generatedS CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
-> CharParser (AnnoState st) Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> CharParser (AnnoState st) Token
forall st. String -> AParser st Token
asKey String
freeS)
       CharParser (AnnoState st) Token
-> (Token -> AParser st FplExt) -> AParser st FplExt
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ k :: Token
k -> String -> AParser st FplExt
forall s (m :: * -> *) t u a.
Stream s m t =>
String -> ParsecT s u m a
unexpected (String -> AParser st FplExt) -> String -> AParser st FplExt
forall a b. (a -> b) -> a -> b
$ "CASL keyword '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Token -> ShowS
forall a. Show a => a -> ShowS
shows Token
k "'")

fplSortItem :: [String] -> AParser st FplSortItem
fplSortItem :: [String] -> AParser st FplSortItem
fplSortItem ks :: [String]
ks = do
    SORT
s <- [String] -> GenParser Char (AnnoState st) SORT
forall st. [String] -> GenParser Char st SORT
sortId [String]
ks
    [String] -> SORT -> AParser st FplSortItem
forall st. [String] -> SORT -> AParser st FplSortItem
freeType [String]
ks SORT
s AParser st FplSortItem
-> AParser st FplSortItem -> AParser st FplSortItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
      (SORT_ITEM TermExt -> FplSortItem)
-> ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
-> AParser st FplSortItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SORT_ITEM TermExt -> FplSortItem
CaslSortItem ([String]
-> ([SORT], Range)
-> ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
forall st f.
[String] -> ([SORT], Range) -> AParser st (SORT_ITEM f)
subSortDecl [String]
ks ([SORT
s], Range
nullRange) ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
-> ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
-> ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String]
-> SORT
-> ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
forall st f. [String] -> SORT -> AParser st (SORT_ITEM f)
commaSortDecl [String]
ks SORT
s
          ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
-> ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
-> ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [String]
-> SORT
-> ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
forall f st.
TermParser f =>
[String] -> SORT -> AParser st (SORT_ITEM f)
isoDecl [String]
ks SORT
s ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
-> ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
-> ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> SORT_ITEM TermExt
-> ParsecT String (AnnoState st) Identity (SORT_ITEM TermExt)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SORT] -> Range -> SORT_ITEM TermExt
forall f. [SORT] -> Range -> SORT_ITEM f
Sort_decl [SORT
s] Range
nullRange))

freeType :: [String] -> SORT -> AParser st FplSortItem
freeType :: [String] -> SORT -> AParser st FplSortItem
freeType ks :: [String]
ks s :: SORT
s = do
  Token
f <- String -> AParser st Token
forall st. String -> AParser st Token
asKey String
freeS
  String -> AParser st Token
forall st. String -> AParser st Token
asKey String
withS
  (DATATYPE_DECL -> FplSortItem)
-> ParsecT String (AnnoState st) Identity DATATYPE_DECL
-> AParser st FplSortItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DATATYPE_DECL -> FplSortItem
FreeType (ParsecT String (AnnoState st) Identity DATATYPE_DECL
 -> AParser st FplSortItem)
-> ParsecT String (AnnoState st) Identity DATATYPE_DECL
-> AParser st FplSortItem
forall a b. (a -> b) -> a -> b
$ [String]
-> SORT
-> Token
-> ParsecT String (AnnoState st) Identity DATATYPE_DECL
forall st. [String] -> SORT -> Token -> AParser st DATATYPE_DECL
parseDatatype [String]
ks SORT
s Token
f

fplOpItem :: [String] -> AParser st FplOpItem
fplOpItem :: [String] -> AParser st FplOpItem
fplOpItem ks :: [String]
ks = (FunDef -> FplOpItem)
-> ParsecT String (AnnoState st) Identity FunDef
-> AParser st FplOpItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FunDef -> FplOpItem
FunOp ([String] -> ParsecT String (AnnoState st) Identity FunDef
forall st. [String] -> AParser st FunDef
funDef [String]
ks) AParser st FplOpItem
-> AParser st FplOpItem -> AParser st FplOpItem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (OP_ITEM TermExt -> FplOpItem)
-> ParsecT String (AnnoState st) Identity (OP_ITEM TermExt)
-> AParser st FplOpItem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap OP_ITEM TermExt -> FplOpItem
CaslOpItem ([String]
-> ParsecT String (AnnoState st) Identity (OP_ITEM TermExt)
forall f st. TermParser f => [String] -> AParser st (OP_ITEM f)
opItem [String]
ks)

instance AParsable FplExt where
  aparser :: AParser st FplExt
aparser = [String] -> AParser st FplExt
forall st. [String] -> AParser st FplExt
fplExt [String]
fplReservedWords

-- Generated by DrIFT, look but don't touch!

instance GetRange FplExt where
  getRange :: FplExt -> Range
getRange x :: FplExt
x = case FplExt
x of
    FplSortItems _ p :: Range
p -> Range
p
    FplOpItems _ p :: Range
p -> Range
p
  rangeSpan :: FplExt -> [Pos]
rangeSpan x :: FplExt
x = case FplExt
x of
    FplSortItems a :: [Annoted FplSortItem]
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [[Annoted FplSortItem] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted FplSortItem]
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]
    FplOpItems a :: [Annoted FplOpItem]
a b :: Range
b -> [[Pos]] -> [Pos]
joinRanges [[Annoted FplOpItem] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [Annoted FplOpItem]
a, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
b]

instance GetRange FplSortItem where
  getRange :: FplSortItem -> Range
getRange = Range -> FplSortItem -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: FplSortItem -> [Pos]
rangeSpan x :: FplSortItem
x = case FplSortItem
x of
    FreeType a :: DATATYPE_DECL
a -> [[Pos]] -> [Pos]
joinRanges [DATATYPE_DECL -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan DATATYPE_DECL
a]
    CaslSortItem a :: SORT_ITEM TermExt
a -> [[Pos]] -> [Pos]
joinRanges [SORT_ITEM TermExt -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT_ITEM TermExt
a]

instance GetRange FplOpItem where
  getRange :: FplOpItem -> Range
getRange = Range -> FplOpItem -> Range
forall a b. a -> b -> a
const Range
nullRange
  rangeSpan :: FplOpItem -> [Pos]
rangeSpan x :: FplOpItem
x = case FplOpItem
x of
    FunOp a :: FunDef
a -> [[Pos]] -> [Pos]
joinRanges [FunDef -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FunDef
a]
    CaslOpItem a :: OP_ITEM TermExt
a -> [[Pos]] -> [Pos]
joinRanges [OP_ITEM TermExt -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan OP_ITEM TermExt
a]

instance GetRange FunDef where
  getRange :: FunDef -> Range
getRange x :: FunDef
x = case FunDef
x of
    FunDef _ _ _ p :: Range
p -> Range
p
  rangeSpan :: FunDef -> [Pos]
rangeSpan x :: FunDef
x = case FunDef
x of
    FunDef a :: SORT
a b :: OP_HEAD
b c :: Annoted FplTerm
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [SORT -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan SORT
a, OP_HEAD -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan OP_HEAD
b,
                                  Annoted FplTerm -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Annoted FplTerm
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]

instance GetRange TermExt where
  getRange :: TermExt -> Range
getRange x :: TermExt
x = case TermExt
x of
    FixDef _ -> Range
nullRange
    Case _ _ p :: Range
p -> Range
p
    Let _ _ p :: Range
p -> Range
p
    IfThenElse _ _ _ p :: Range
p -> Range
p
    EqTerm _ _ p :: Range
p -> Range
p
    BoolTerm _ -> Range
nullRange
  rangeSpan :: TermExt -> [Pos]
rangeSpan x :: TermExt
x = case TermExt
x of
    FixDef a :: FunDef
a -> [[Pos]] -> [Pos]
joinRanges [FunDef -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FunDef
a]
    Case a :: FplTerm
a b :: [(FplTerm, FplTerm)]
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [FplTerm -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FplTerm
a, [(FplTerm, FplTerm)] -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan [(FplTerm, FplTerm)]
b, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    Let a :: FunDef
a b :: FplTerm
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [FunDef -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FunDef
a, FplTerm -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FplTerm
b, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    IfThenElse a :: FplTerm
a b :: FplTerm
b c :: FplTerm
c d :: Range
d -> [[Pos]] -> [Pos]
joinRanges [FplTerm -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FplTerm
a, FplTerm -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FplTerm
b,
                                      FplTerm -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FplTerm
c, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
d]
    EqTerm a :: FplTerm
a b :: FplTerm
b c :: Range
c -> [[Pos]] -> [Pos]
joinRanges [FplTerm -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FplTerm
a, FplTerm -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FplTerm
b, Range -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan Range
c]
    BoolTerm a :: FplTerm
a -> [[Pos]] -> [Pos]
joinRanges [FplTerm -> [Pos]
forall a. GetRange a => a -> [Pos]
rangeSpan FplTerm
a]