4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |

5ba323da9f037264b4a356085e844889aedeac23Christian MaederModule : $Header$

c58a94c44b76b072ace930f2126c889c0b64cb2aChristian MaederDescription : Abstract syntax for CSL

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Dominik Dietrich, Ewaryst Schulz, DFKI Bremen 2010

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederMaintainer : Ewaryst.Schulz@dfki.de

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederStability : experimental

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : portable

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederThis file contains the abstract syntax for CSL as well as pretty printer for it.

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-}

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule CSL.AS_BASIC_CSL

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ( EXPRESSION (..) -- datatype for numerical expressions (e.g. polynomials)

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , EXTPARAM (..) -- datatype for extended parameters (e.g. [I=0])

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder , BASIC_ITEM (..) -- Items of a Basic Spec

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder , BASIC_SPEC (..) -- Basic Spec

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , SYMB_ITEMS (..) -- List of symbols

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maeder , SYMB (..) -- Symbols

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , SYMB_MAP_ITEMS (..) -- Symbol map

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder , SYMB_OR_MAP (..) -- Symbol or symbol map

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , OPNAME (..) -- predefined operator names

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , OPID (..) -- identifier for operators

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder , ConstantName (..) -- names of user-defined constants

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder , OP_ITEM (..) -- operator declaration

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , VAR_ITEM (..) -- variable declaration

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , Domain (..) -- domains for variable declarations

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , GroundConstant (..) -- constants for domain formation

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , AssDefinition (..) -- A function or constant definition

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , getDefiniens -- accessor function for AssDefinition

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder , getArguments -- accessor function for AssDefinition

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , isFunDef -- predicate for AssDefinition

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , isInterval -- predicate for EXPRESSION

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , mkDefinition -- constructor for AssDefinition

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder , updateDefinition -- updates the definiens

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder , InstantiatedConstant(..) -- for function constants we need to store the

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder -- instantiation

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , CMD (..) -- Command datatype

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder , OperatorState (..) -- Class providing operator lookup

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , mapExpr -- maps function over EXPRESSION arguments

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , mkVar -- Variable constructor

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , mkOp -- Simple Operator constructor

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , mkPredefOp -- Simple Operator constructor for predefined ops

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , mkAndAnalyzeOp

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder , toElimConst -- Constant naming for elim constants, see Analysis.hs

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder , OpInfo (..) -- Type for Operator information

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , BindInfo (..) -- Type for Binder information

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , operatorInfo -- Operator information for pretty printing

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder -- and static analysis

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder , operatorInfoMap -- allows efficient lookup of ops by printname

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , operatorInfoNameMap -- allows efficient lookup of ops by opname

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , mergeOpArityMap -- for combining two operator arity maps

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , getOpInfoMap

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder , getOpInfoNameMap

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , lookupOpInfoForParsing

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder , lookupBindInfo

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , APInt, APFloat -- arbitrary precision numbers

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder -- Printer

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder , printExpression

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , printCMD

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , printAssDefinition

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , printConstantName

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , ExpressionPrinter (..)

27912d626bf179b82fcb337077e5cd9653bb71cfChristian Maeder , toArgList

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , simpleName

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder , showOPNAME

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder , OpInfoMap

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , OpInfoNameMap

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ) where

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederimport Common.Id as Id

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederimport Common.Doc

5ba323da9f037264b4a356085e844889aedeac23Christian Maederimport Common.DocUtils

5ba323da9f037264b4a356085e844889aedeac23Christian Maederimport Common.AS_Annotation as AS_Anno

5ba323da9f037264b4a356085e844889aedeac23Christian Maederimport qualified Data.Map as Map

5ba323da9f037264b4a356085e844889aedeac23Christian Maederimport Control.Monad

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederimport Control.Monad.Reader

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maederimport Data.Maybe

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-- Arbitrary precision numbers

975642b989852fc24119c59cf40bc1af653608ffChristian Maedertype APInt = Integer

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder-- TODO: use an arbitrary precision float here:

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- The use of Other floats (such as Double) requires an instance for

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- ShATermConvertible in Common.ATerm.ConvInstances

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maedertype APFloat = Double

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | A simple operator constructor from given operator name and arguments

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedermkOp :: String -> [EXPRESSION] -> EXPRESSION

9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaedermkOp s el = Op (OpUser $ SimpleConstant s) [] el nullRange

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | A variable constructor

9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaedermkVar :: String -> EXPRESSION

9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaedermkVar = Var . mkSimpleId

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- | A simple operator constructor from given operator id and arguments

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedermkPredefOp :: OPNAME -> [EXPRESSION] -> EXPRESSION

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedermkPredefOp n el = Op (OpId n) [] el nullRange

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | Lookup the string in the given 'OperatorState'

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaedermkAndAnalyzeOp :: OperatorState st => st -> String -> [EXTPARAM] -> [EXPRESSION]

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder -> Range -> EXPRESSION

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedermkAndAnalyzeOp st s eps exps rg =

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder let err msg = "mkAndAnalyzeOp: At operator " ++ s ++ "\n" ++ msg

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder -- an error-message producing function

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder g msg | not $ null eps = Just $ err msg

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ++ "* No extended parameters allowed\n"

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder | null msg = Nothing

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | otherwise = Just $ err msg

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder opOrErr mOp x = case x of

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Just msg -> error msg

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder _ -> let oi = fromJust mOp

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder in (foldNAry oi, OpId $ opname oi)

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder (fnary, op) =

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder case lookupOperator st s (length exps) of

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder Left False -> (False, OpUser $ SimpleConstant s)

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder -- if registered it must be registered with the given arity or

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder -- as flex-op, otherwise we don't accept it

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Left True -> opOrErr Nothing $ g "* Wrong arity\n"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Right opinfo -> opOrErr (Just opinfo) $ g ""

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder e | fnary && length exps > 2 =

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder if null eps

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder then foldl f (f (exps!!0) (exps!!1)) $ drop 2 exps

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder else error $ "mkAndAnalyzeOp: cannot fold application with "

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder ++ "extended parameters "

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder ++ show (pretty $ Op op eps exps rg)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder | otherwise = Op op eps exps rg

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder f e' e'' = Op op [] [e', e''] rg

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder in e

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedermapExpr :: (EXPRESSION -> EXPRESSION) -> EXPRESSION -> EXPRESSION

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedermapExpr f e =

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder case e of

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Op oi epl args rg -> Op oi epl (map f args) rg

5ba323da9f037264b4a356085e844889aedeac23Christian Maeder List exps rg -> List (map f exps) rg

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder _ -> e

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- * CSL Basic Data Structures

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | operator symbol declaration

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederdata OP_ITEM = Op_item [Id.Token] Id.Range

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder deriving Show

5ba323da9f037264b4a356085e844889aedeac23Christian Maeder

5ba323da9f037264b4a356085e844889aedeac23Christian Maeder-- | variable symbol declaration

5ba323da9f037264b4a356085e844889aedeac23Christian Maederdata VAR_ITEM = Var_item [Id.Token] Domain Id.Range

5ba323da9f037264b4a356085e844889aedeac23Christian Maeder deriving Show

5ba323da9f037264b4a356085e844889aedeac23Christian Maeder

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maedernewtype BASIC_SPEC = Basic_spec [AS_Anno.Annoted (BASIC_ITEM)]

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder deriving Show

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederdata GroundConstant = GCI APInt | GCR APFloat deriving (Eq, Ord, Show)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

c9892acbf03a509d874ac6d79b9a2cb09042e0dcChristian Maeder-- | A finite set or an interval. True = closed, False = opened

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederdata Domain = Set [GroundConstant]

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | IntVal (GroundConstant, Bool) (GroundConstant, Bool)

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder deriving (Eq, Ord, Show)

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | A constant or function definition

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata AssDefinition = ConstDef EXPRESSION | FunDef [String] EXPRESSION

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder deriving (Eq, Ord, Show)

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederupdateDefinition :: EXPRESSION -> AssDefinition -> AssDefinition

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederupdateDefinition e' (ConstDef _) = ConstDef e'

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederupdateDefinition e' (FunDef l _) = FunDef l e'

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

b49276c9f50038e0bd499ad49f7bd6444566a834Christian MaedermkDefinition :: [String] -> EXPRESSION -> AssDefinition

9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaedermkDefinition l e = if null l then ConstDef e else FunDef l e

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedergetDefiniens :: AssDefinition -> EXPRESSION

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedergetDefiniens (ConstDef e) = e

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedergetDefiniens (FunDef _ e) = e

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedergetArguments :: AssDefinition -> [String]

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedergetArguments (FunDef l _) = l

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedergetArguments _ = []

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederisFunDef :: AssDefinition -> Bool

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederisFunDef (FunDef _ _) = True

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaederisFunDef _ = False

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederisInterval :: EXPRESSION -> Bool

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederisInterval (Interval _ _ _) = True

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederisInterval _ = False

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata InstantiatedConstant = InstantiatedConstant

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder { constName :: ConstantName

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder , instantiation :: [EXPRESSION] } deriving (Show, Eq, Ord)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederinstance Pretty InstantiatedConstant where

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder pretty (InstantiatedConstant { constName = cn, instantiation = el }) =

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder if null el then pretty cn

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder else pretty cn <> (parens $ sepByCommas $ map pretty el)

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | basic items: an operator or variable declaration or an axiom

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederdata BASIC_ITEM =

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder Op_decl OP_ITEM

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder | Var_decls [VAR_ITEM]

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder | Axiom_item (AS_Anno.Annoted CMD)

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder deriving Show

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- | Extended Parameter Datatype

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maederdata EXTPARAM = EP Id.Token String APInt deriving (Eq, Ord, Show)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederdata OPNAME =

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder -- arithmetic operators

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder OP_mult | OP_div | OP_plus | OP_minus | OP_neg | OP_pow

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder -- roots, trigonometric and other operators

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder | OP_fthrt | OP_sqrt | OP_abs | OP_max | OP_min | OP_sign

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder | OP_cos | OP_sin | OP_tan | OP_Pi

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder | OP_reldist

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder -- special CAS operators

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder | OP_minimize | OP_minloc | OP_maximize | OP_maxloc | OP_factor

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder | OP_divide | OP_factorize | OP_int | OP_rlqe | OP_simplify | OP_solve

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder -- comparison predicates

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder | OP_neq | OP_lt | OP_leq | OP_eq | OP_gt | OP_geq | OP_convergence

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder | OP_reldistLe

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder -- containment predicate

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder | OP_in

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder -- special CAS constants

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder | OP_undef | OP_failure

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder -- boolean constants and connectives

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder | OP_false | OP_true | OP_not | OP_and | OP_or | OP_impl

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder -- quantifiers

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder | OP_ex | OP_all

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder deriving (Eq, Ord)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederinstance Show OPNAME where

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder show = showOPNAME

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedershowOPNAME :: OPNAME -> String

f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedershowOPNAME x =

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder case x of

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder OP_neq -> "!="

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder OP_mult -> "*"

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder OP_plus -> "+"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_minus -> "-"

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder OP_neg -> "-"

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder OP_div -> "/"

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder OP_lt -> "<"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_leq -> "<="

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_eq -> "="

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_gt -> ">"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_geq -> ">="

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_Pi -> "Pi"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_pow -> "^"

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder OP_abs -> "abs"

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder OP_sign -> "sign"

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder OP_all -> "all"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_and -> "and"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_convergence -> "convergence"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_cos -> "cos"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_divide -> "divide"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_ex -> "ex"

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder OP_factor -> "factor"

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder OP_factorize -> "factorize"

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder OP_fthrt -> "fthrt"

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder OP_impl -> "impl"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_int -> "int"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_max -> "max"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_maximize -> "maximize"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_maxloc -> "maxloc"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_min -> "min"

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder OP_minimize -> "minimize"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_minloc -> "minloc"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_not -> "not"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_or -> "or"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_reldist -> "reldist"

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder OP_reldistLe -> "reldistLe"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder OP_rlqe -> "rlqe"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_simplify -> "simplify"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder OP_sin -> "sin"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder OP_solve -> "solve"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_sqrt -> "sqrt"

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder OP_tan -> "tan"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_false -> "false"

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder OP_true -> "true"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder OP_in -> "in"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder OP_undef -> "undef"

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder OP_failure -> "fail"

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederdata OPID = OpId OPNAME | OpUser ConstantName deriving (Eq, Ord, Show)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-- | We differentiate between simple constant names and indexed constant names

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- resulting from the extended parameter elimination.

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maederdata ConstantName = SimpleConstant String | ElimConstant String Int

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder deriving (Eq, Ord, Show)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedersimpleName :: OPID -> String

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedersimpleName (OpId n) = showOPNAME n

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedersimpleName (OpUser (SimpleConstant s)) = s

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedersimpleName (OpUser x) = error "simpleName: ElimConstant not supported: " ++ show x

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder{-

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederinstance Show OPID where

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder show (OpId n) = show n

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder show (OpUser s) = show s

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederinstance Show ConstantName where

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder show (SimpleConstant s) = s

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder show (ElimConstant s i) = if i > 0 then s ++ "__" ++ show i else s

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-}

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedertoElimConst :: ConstantName -> Int -> ConstantName

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedertoElimConst (SimpleConstant s) i = ElimConstant s i

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedertoElimConst ec _ = error $ "toElimConst: already an elim const " ++ show ec

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | Datatype for expressions

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederdata EXPRESSION =

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder Var Id.Token

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | Op OPID [EXTPARAM] [EXPRESSION] Id.Range

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder -- TODO: don't need lists anymore, they should be removed soon

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | List [EXPRESSION] Id.Range

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | Interval APFloat APFloat Id.Range

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder | Int APInt Id.Range

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | Double APFloat Id.Range

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder deriving (Eq, Ord, Show)

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | If the expression list is a variable list the list of the variable names

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- is returned.

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedertoArgList :: [EXPRESSION] -> [String]

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedertoArgList [] = []

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian MaedertoArgList (Var tok:l) = tokStr tok : toArgList l

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedertoArgList (x:_) = error $ "toArgList: unsupported as argument " ++ show (pretty x)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-- TODO: add Range-support to this type

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata CMD = Ass EXPRESSION EXPRESSION

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder | Cmd String [EXPRESSION]

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | Sequence [CMD] -- program sequence

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | Cond [(EXPRESSION, [CMD])]

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder | Repeat EXPRESSION [CMD] -- constraint, statements

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder deriving (Show, Eq, Ord)

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maeder-- | symbol lists for hiding

0be2d0cfd911d313e7e941edbc77f95052c8c19bChristian Maederdata SYMB_ITEMS = Symb_items [SYMB] Id.Range

-- pos: SYMB_KIND, commas

deriving (Show, Eq)

-- | symbol for identifiers

newtype SYMB = Symb_id Id.Token

-- pos: colon

deriving (Show, Eq)

-- | symbol maps for renamings

data SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP] Id.Range

-- pos: SYMB_KIND, commas

deriving (Show, Eq)

-- | symbol map or renaming (renaming then denotes the identity renaming)

data SYMB_OR_MAP = Symb SYMB

| Symb_map SYMB SYMB Id.Range

-- pos: "|->"

deriving (Show, Eq)

-- * Predefined Operators: info for parsing/printing and static analysis

data BindInfo = BindInfo { bindingVarPos :: [Int] -- ^ argument positions of

-- binding variables

, boundBodyPos :: [Int] -- ^ argument positions of

-- bound terms

} deriving (Eq, Ord, Show)

data OpInfo = OpInfo { prec :: Int -- ^ precedence between 0 and maxPrecedence

, infx :: Bool -- ^ True = infix

, arity :: Int -- ^ the operator arity

, foldNAry :: Bool -- ^ True = fold nary-applications

-- during construction into binary ones

, opname :: OPNAME -- ^ The actual operator name

, bind :: Maybe BindInfo -- ^ More info for binders

} deriving (Eq, Ord, Show)

type ArityMap = Map.Map Int OpInfo

type OpInfoArityMap a = Map.Map a ArityMap

type OpInfoMap = OpInfoArityMap String

type OpInfoNameMap = OpInfoArityMap OPNAME

-- | Merges two OpInfoArityMaps together with the first map as default map

-- and the second overwriting the default values

mergeOpArityMap :: Ord a => OpInfoArityMap a -> OpInfoArityMap a

-> OpInfoArityMap a

mergeOpArityMap = flip $ Map.unionWith Map.union

-- | Mapping of operator names to arity-'OpInfo'-maps (an operator may

-- behave differently for different arities).

getOpInfoMap :: (OpInfo -> String) -> [OpInfo] -> OpInfoMap

getOpInfoMap pf oinfo = foldl f Map.empty oinfo

where f m oi = Map.insertWith Map.union (pf oi)

(Map.fromList [(arity oi, oi)]) m

-- | Same as operatorInfoMap but with keys of type OPNAME instead of String

getOpInfoNameMap :: [OpInfo] -> OpInfoNameMap

getOpInfoNameMap oinfo = foldl f Map.empty oinfo

where f m oi = Map.insertWith Map.union (opname oi)

(Map.fromList [(arity oi, oi)]) m

-- | opInfoMap for the predefined 'operatorInfo'

operatorInfoMap :: OpInfoMap

operatorInfoMap = getOpInfoMap (show . opname) operatorInfo

-- | opInfoNameMap for the predefined 'operatorInfo'

operatorInfoNameMap :: OpInfoNameMap

operatorInfoNameMap = getOpInfoNameMap operatorInfo

-- | Mapping of operator names to arity-'OpInfo'-maps (an operator may

-- behave differently for different arities).

operatorInfo :: [OpInfo]

operatorInfo =

let -- arity (-1 means flex), precedence, infix

toSgl n i p = OpInfo { prec = if p == 0 then maxPrecedence else p

, infx = p > 0

, arity = i

, opname = n

, foldNAry = False

, bind = Nothing

}

toSglBind n i bv bb =

OpInfo { prec = maxPrecedence

, infx = False

, arity = i

, opname = n

, foldNAry = False

, bind = Just $ BindInfo [bv] [bb]

}

-- arityX simple ops

aX i s = toSgl s i 0

-- arityflex simple ops

aflex = aX (-1)

-- arity2 binder

a2bind bv bb s = toSglBind s 2 bv bb

-- arity4 binder

a4bind bv bb s = toSglBind s 4 bv bb

-- arity2 infix with precedence

a2i p s = toSgl s 2 p

in map (aX 0) [ OP_failure, OP_undef, OP_Pi, OP_true, OP_false ]

++ map (aX 1)

[ OP_neg, OP_cos, OP_sin, OP_tan, OP_sqrt, OP_fthrt, OP_abs

, OP_sign, OP_simplify, OP_rlqe, OP_factor, OP_factorize ]

++ map (a2bind 0 1) [ OP_ex, OP_all ]

++ map (a2i 3) [ OP_or, OP_impl ]

++ map (a2i 4) [ OP_and ]

++ map (a2i 5) [ OP_eq, OP_gt, OP_leq, OP_geq, OP_neq, OP_lt, OP_in]

++ map (a2i 6) [ OP_plus ]

++ map (a2i 7) [ OP_minus ]

++ map (a2i 8) [OP_mult]

++ map (a2i 9) [OP_div]

++ map (a2i 10) [OP_pow]

++ map (aX 2)

[OP_int, OP_divide, OP_solve, OP_convergence, OP_reldist]

++ map (aX 3) [OP_reldistLe]

++ map aflex [ OP_min, OP_max ]

++ map (a2bind 1 0) [ OP_maximize, OP_minimize ]

++ map (a4bind 1 0) [ OP_maxloc, OP_minloc ]

maxPrecedence :: Int

maxPrecedence = 100

-- ---------------------------------------------------------------------------

-- * OpInfo lookup utils

-- ---------------------------------------------------------------------------

class OperatorState a where

lookupOperator :: a

-> String -- ^ operator name

-> Int -- ^ operator arity

-> Either Bool OpInfo

instance OperatorState () where

lookupOperator _ = lookupOpInfoForParsing operatorInfoMap

instance OperatorState OpInfoMap where

lookupOperator = lookupOpInfoForParsing

-- | For the given name and arity we lookup an 'OpInfo', where arity=-1

-- means flexible arity. If an operator is registered for the given

-- string but not for the arity we return: Left True.

-- This function is designed for the lookup of operators in not statically

-- analyzed terms. For statically analyzed terms use lookupOpInfo.

lookupOpInfoForParsing :: OpInfoMap -- ^ map to be used for lookup

-> String -- ^ operator name

-> Int -- ^ operator arity

-> Either Bool OpInfo

lookupOpInfoForParsing oiMap op arit =

case Map.lookup op oiMap of

Just oim ->

case Map.lookup arit oim of

Just x -> Right x

Nothing ->

case Map.lookup (-1) oim of

Just x -> Right x

_ -> Left True

_ -> Left False

-- | For the given name and arity we lookup an 'OpInfo', where arity=-1

-- means flexible arity. If an operator is registered for the given

-- string but not for the arity we return: Left True.

lookupOpInfo :: OpInfoNameMap -> OPID -- ^ operator id

-> Int -- ^ operator arity

-> Either Bool OpInfo

lookupOpInfo oinm (OpId op) arit =

case Map.lookup op oinm of

Just oim ->

case Map.lookup arit oim of

Just x -> Right x

Nothing ->

case Map.lookup (-1) oim of

Just x -> Right x

_ -> Left True

_ -> error $ "lookupOpInfo: no opinfo for " ++ show op

lookupOpInfo _ (OpUser _) _ = Left False

-- | For the given name and arity we lookup an 'BindInfo', where arity=-1

-- means flexible arity.

lookupBindInfo :: OpInfoNameMap -> OPID -- ^ operator name

-> Int -- ^ operator arity

-> Maybe BindInfo

lookupBindInfo oinm (OpId op) arit =

case Map.lookup op oinm of

Just oim ->

case Map.lookup arit oim of

Just x -> bind x

_ -> Nothing

_ -> error $ "lookupBindInfo: no opinfo for " ++ show op

lookupBindInfo _ (OpUser _) _ = Nothing

-- * Pretty Printing

instance Pretty Domain where

pretty = printDomain

instance Pretty OP_ITEM where

pretty = printOpItem

instance Pretty VAR_ITEM where

pretty = printVarItem

instance Pretty BASIC_SPEC where

pretty = printBasicSpec

instance Pretty BASIC_ITEM where

pretty = printBasicItems

instance Pretty EXTPARAM where

pretty = printExtparam

instance Pretty EXPRESSION where

pretty = head . printExpression

instance Pretty SYMB_ITEMS where

pretty = printSymbItems

instance Pretty SYMB where

pretty = printSymbol

instance Pretty SYMB_MAP_ITEMS where

pretty = printSymbMapItems

instance Pretty SYMB_OR_MAP where

pretty = printSymbOrMap

instance Pretty CMD where

pretty = head . printCMD

instance Pretty ConstantName where

pretty = printConstantName

instance Pretty AssDefinition where

pretty = head . printAssDefinition

instance Pretty OPID where

pretty = head . printOPID

-- | A monad for printing of constants. This turns the pretty printing facility

-- more flexible w.r.t. the output of 'ConstantName'.

class Monad m => ExpressionPrinter m where

getOINM :: m OpInfoNameMap

getOINM = return operatorInfoNameMap

printConstant :: ConstantName -> m Doc

printConstant = return . printConstantName

printOpname :: OPNAME -> m Doc

printOpname = return . text . showOPNAME

prefixMode :: m Bool

prefixMode = return False

printArgs :: [Doc] -> m Doc

printArgs = return . parens . sepByCommas

printVarDecl :: String -> m Doc

printVarDecl = return . text

printInterval :: APFloat -> APFloat -> m Doc

printInterval l r =

return $ brackets $ sepByCommas $ map (text . show) [l, r]

-- | The default ConstantName printer

printConstantName :: ConstantName -> Doc

printConstantName (SimpleConstant s) = text s

printConstantName (ElimConstant s i) =

text $ if i > 0 then s ++ "__" ++ show i else s

printAssDefinition :: ExpressionPrinter m => AssDefinition -> m Doc

printAssDefinition (ConstDef e) = printExpression e >>= return . (text "=" <+>)

printAssDefinition (FunDef l e) = do

ed <- printExpression e

l' <- mapM printVarDecl l

args <- printArgs l'

return $ args <+> text "=" <+> ed

printOPID :: ExpressionPrinter m => OPID -> m Doc

printOPID (OpUser c) = printConstant c

printOPID (OpId oi) = printOpname oi

-- a dummy instance, we take the simplest monad

instance ExpressionPrinter []

-- | An 'OpInfoNameMap' can be interpreted as an 'ExpressionPrinter'

instance ExpressionPrinter (Reader OpInfoNameMap) where

getOINM = ask

printCMD :: ExpressionPrinter m => CMD -> m Doc

printCMD (Ass c def) = do

[c', def'] <- mapM printExpression [c, def]

return $ c' <+> text ":=" <+> def'

printCMD c@(Cmd s exps) -- TODO: remove the case := later

| s == ":=" = error $ "printCMD: use Ass for assignment representation! "

++ show c

| s == "constraint" = printExpression (exps !! 0)

| otherwise = let f l = text s <> parens (sepByCommas l)

in liftM f $ mapM printExpression exps

printCMD (Repeat e stms) = do

e' <- printExpression e

let f l = text "re" <>

(text "peat" $+$ vcat (map (text "." <+>) l))

$+$ text "until" <+> e'

liftM f $ mapM printCMD stms

printCMD (Sequence stms) =

let f l = text "se" <> (text "quence" $+$ vcat (map (text "." <+>) l))

$+$ text "end"

in liftM f $ mapM printCMD stms

printCMD (Cond l) = let f l' = vcat l' $+$ text "end"

in liftM f $ mapM (uncurry printCase) l

printCase :: ExpressionPrinter m => EXPRESSION -> [CMD] -> m Doc

printCase e l = do

e' <- printExpression e

let f l' = text "ca" <> (text "se" <+> e' <> text ":"

$+$ vcat (map (text "." <+>) l'))

liftM f $ mapM printCMD l

getPrec :: OpInfoNameMap -> EXPRESSION -> Int

getPrec oinm (Op s _ exps _)

| length exps == 0 = maxPrecedence + 1

| otherwise =

case lookupOpInfo oinm s $ length exps of

Right oi -> prec oi

Left True -> error $

concat [ "getPrec: registered operator ", show s, " used "

, "with non-registered arity ", show $ length exps ]

_ -> maxPrecedence -- this is probably a userdefine prefix function

-- , binds strongly

getPrec _ _ = maxPrecedence

getOp :: EXPRESSION -> Maybe OPID

getOp (Op s _ _ _) = Just s

getOp _ = Nothing

printExtparam :: EXTPARAM -> Doc

printExtparam (EP p op i) =

pretty p <> text op <> (text $ if op == "-|" then "" else show i)

printExtparams :: [EXTPARAM] -> Doc

printExtparams [] = empty

printExtparams l = brackets $ sepByCommas $ map printExtparam l

printInfix :: ExpressionPrinter m => EXPRESSION -> m Doc

printInfix e@(Op s _ exps@[e1, e2] _) = do

-- we mustn't omit the space between the operator and its arguments for text-

-- operators such as "and", "or", but it would be good to omit it for "+-*/"

oi <- printOPID s

oinm <- getOINM

let outerprec = getPrec oinm e

f cmp e' ed = if cmp outerprec $ getPrec oinm e' then ed else parens ed

g [ed1, ed2] = let cmp = case getOp e1 of

Just op1 | op1 == s -> (<=)

| otherwise -> (<)

_ -> (<)

in f cmp e1 ed1 <+> oi <+> f (<) e2 ed2

g _ = error "printInfix: Inner impossible case"

liftM g $ mapM printExpression exps

printInfix _ = error "printInfix: Impossible case"

printExpression :: ExpressionPrinter m => EXPRESSION -> m Doc

printExpression (Var token) = return $ text $ tokStr token

printExpression e@(Op s epl exps _)

| length exps == 0 = liftM (<> printExtparams epl) $ printOPID s

| otherwise = do

let asPrfx pexps = do

oid <- printOPID s

args <- printArgs pexps

return $ oid <> printExtparams epl <> args

asPrfx' = mapM printExpression exps >>= asPrfx

oinm <- getOINM

pfxMode <- prefixMode

if pfxMode then asPrfx' else

case lookupOpInfo oinm s $ length exps of

Right oi

| infx oi -> printInfix e

| otherwise -> asPrfx'

_ -> asPrfx'

printExpression (List exps _) = liftM sepByCommas (mapM printExpression exps)

printExpression (Int i _) = return $ text (show i)

printExpression (Double d _) = return $ text (show d)

printExpression (Interval l r _) = printInterval l r

printOpItem :: OP_ITEM -> Doc

printOpItem (Op_item tokens _) =

text "operator" <+> sepByCommas (map pretty tokens)

printVarItem :: VAR_ITEM -> Doc

printVarItem (Var_item vars dom _) =

hsep [sepByCommas $ map pretty vars, text "in", pretty dom]

printDomain :: Domain -> Doc

printDomain (Set l) = braces $ sepByCommas $ map printGC l

printDomain (IntVal (c1, b1) (c2, b2)) =

hcat [ getIBorder True b1, sepByCommas $ map printGC [c1, c2]

, getIBorder False b2]

getIBorder :: Bool -> Bool -> Doc

getIBorder False False = lbrack

getIBorder True True = lbrack

getIBorder _ _ = rbrack

printGC :: GroundConstant -> Doc

printGC (GCI i) = text (show i)

printGC (GCR d) = text (show d)

printBasicSpec :: BASIC_SPEC -> Doc

printBasicSpec (Basic_spec xs) = vcat $ map pretty xs

printBasicItems :: BASIC_ITEM -> Doc

printBasicItems (Axiom_item x) = pretty x

printBasicItems (Op_decl x) = pretty x

printBasicItems (Var_decls x) = text "vars" <+> (sepBySemis $ map pretty x)

printSymbol :: SYMB -> Doc

printSymbol (Symb_id sym) = pretty sym

printSymbItems :: SYMB_ITEMS -> Doc

printSymbItems (Symb_items xs _) = fsep $ map pretty xs

printSymbOrMap :: SYMB_OR_MAP -> Doc

printSymbOrMap (Symb sym) = pretty sym

printSymbOrMap (Symb_map source dest _) =

pretty source <+> mapsto <+> pretty dest

printSymbMapItems :: SYMB_MAP_ITEMS -> Doc

printSymbMapItems (Symb_map_items xs _) = fsep $ map pretty xs

-- Instances for GetRange

instance GetRange OP_ITEM where

getRange = Range . rangeSpan

rangeSpan x = case x of

Op_item a b -> joinRanges [rangeSpan a, rangeSpan b]

instance GetRange VAR_ITEM where

getRange = Range . rangeSpan

rangeSpan x = case x of

Var_item a _ b -> joinRanges [rangeSpan a, rangeSpan b]

instance GetRange BASIC_SPEC where

getRange = Range . rangeSpan

rangeSpan x = case x of

Basic_spec a -> joinRanges [rangeSpan a]

instance GetRange BASIC_ITEM where

getRange = Range . rangeSpan

rangeSpan x = case x of

Op_decl a -> joinRanges [rangeSpan a]

Var_decls a -> joinRanges [rangeSpan a]

Axiom_item a -> joinRanges [rangeSpan a]

instance GetRange CMD where

getRange = Range . rangeSpan

rangeSpan (Ass c def) = joinRanges (map rangeSpan [c, def])

rangeSpan (Cmd _ exps) = joinRanges (map rangeSpan exps)

-- parsing guruantees l <> null

rangeSpan (Repeat c l) = joinRanges [rangeSpan c, rangeSpan $ head l]

-- parsing guruantees l <> null

rangeSpan (Sequence l) = rangeSpan $ head l

rangeSpan (Cond l) = rangeSpan $ head l

instance GetRange SYMB_ITEMS where

getRange = Range . rangeSpan

rangeSpan (Symb_items a b) = joinRanges [rangeSpan a, rangeSpan b]

instance GetRange SYMB where

getRange = Range . rangeSpan

rangeSpan (Symb_id a) = joinRanges [rangeSpan a]

instance GetRange SYMB_MAP_ITEMS where

getRange = Range . rangeSpan

rangeSpan (Symb_map_items a b) = joinRanges [rangeSpan a, rangeSpan b]

instance GetRange SYMB_OR_MAP where

getRange = Range . rangeSpan

rangeSpan x = case x of

Symb a -> joinRanges [rangeSpan a]

Symb_map a b c -> joinRanges [rangeSpan a, rangeSpan b, rangeSpan c]

instance GetRange EXPRESSION where

getRange = Range . rangeSpan

rangeSpan x = case x of

Var token -> joinRanges [rangeSpan token]

Op _ _ exps a -> joinRanges $ [rangeSpan a] ++ (map rangeSpan exps)

List exps a -> joinRanges $ [rangeSpan a] ++ (map rangeSpan exps)

Int _ a -> joinRanges [rangeSpan a]

Double _ a -> joinRanges [rangeSpan a]

Interval _ _ a -> joinRanges [rangeSpan a]