25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, DeriveDataTypeable #-}

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis{- |

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisModule : ./CSL/AS_BASIC_CSL.hs

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisDescription : Abstract syntax for EnCL

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisCopyright : (c) Dominik Dietrich, Ewaryst Schulz, DFKI Bremen 2010

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisLicense : GPLv2 or higher, see LICENSE.txt

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisMaintainer : Ewaryst.Schulz@dfki.de

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisStability : experimental

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisPortability : portable

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisThis module contains the abstract syntax types for EnCL as well as the

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtispredefined operator configuration.

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis-}

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtismodule CSL.AS_BASIC_CSL

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis ( EXPRESSION (..) {- datatype for numerical expressions

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis (e.g. polynomials) -}

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , EXTPARAM (..) -- datatype for extended parameters (e.g. [I=0])

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , BASIC_ITEM (..) -- Items of a Basic Spec

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , BASIC_SPEC (..) -- Basic Spec

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , SYMB_ITEMS (..) -- List of symbols

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , SYMB (..) -- Symbols

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , SYMB_MAP_ITEMS (..) -- Symbol map

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , SYMB_OR_MAP (..) -- Symbol or symbol map

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , OPNAME (..) -- predefined operator names

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , OPID (..) -- identifier for operators

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , ConstantName (..) -- names of user-defined constants

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , OP_ITEM (..) -- operator declaration

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , VAR_ITEM (..) -- variable declaration

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , VarDecl (..) -- variable declaration in assignment

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , OpDecl (..) -- operator declaration in assignment

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , EPDecl (..) -- extparam declaration

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , EPVal (..) -- extparam values

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , getEPVarRef

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , Domain -- domains for variable declarations

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , EPDomain -- domains for extended parameter declarations

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , GroundConstant (..) -- constants for domain formation

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , cmpFloatToInt -- comparer for APFloat with APInt

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , AssDefinition (..) -- A function or constant definition

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , InstantiatedConstant (..) {- for function constants we need to store the

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis instantiation -}

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , CMD (..) -- Command datatype

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , OperatorState (..) -- Class providing operator lookup

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , OpInfo (..) -- Type for Operator information

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , BindInfo (..) -- Type for Binder information

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , operatorInfo {- Operator information for pretty printing

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis and static analysis -}

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , operatorInfoMap -- allows efficient lookup of ops by printname

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , operatorInfoNameMap -- allows efficient lookup of ops by opname

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , operatorBindInfoMap

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , mergeOpArityMap -- for combining two operator arity maps

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , getOpInfoMap

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , getOpInfoNameMap

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , getBindInfoMap

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , lookupOpInfo

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , lookupOpInfoForParsing

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , lookupBindInfo

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , APInt, APFloat -- arbitrary precision numbers

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , toFraction, fromFraction

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , OpInfoMap

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , OpInfoNameMap

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , BindInfoMap

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , showOPNAME

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , maxPrecedence

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis ) where

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisimport Common.Id as Id

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisimport Common.AS_Annotation as AS_Anno

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisimport Data.Data

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisimport qualified Data.Map as Map

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisimport Data.Ratio

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisimport CSL.TreePO

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis{- ---------------------------------------------------------------------------

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisEnCL Basic Data Structures and utils

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis--------------------------------------------------------------------------- -}

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis-- Arbitrary precision numbers

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtistype APInt = Integer

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtistype APFloat = Rational

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtiscmpFloatToInt :: APFloat -> APInt -> Ordering

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtiscmpFloatToInt a b = compare a $ fromFraction b 1

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisfromFraction :: Integer -> Integer -> APFloat

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisfromFraction = (%)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtistoFraction :: APFloat -> (Integer, Integer)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtistoFraction r = (numerator r, denominator r)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis-- | operator symbol declaration

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisdata OP_ITEM = Op_item [Id.Token] Id.Range

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis deriving (Show, Typeable, Data)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis-- | variable symbol declaration

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisdata VAR_ITEM = Var_item [Id.Token] Domain Id.Range

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis deriving (Show, Typeable, Data)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisnewtype BASIC_SPEC = Basic_spec [AS_Anno.Annoted BASIC_ITEM]

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis deriving (Show, Typeable, Data)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisdata GroundConstant = GCI APInt | GCR APFloat deriving (Show, Typeable, Data)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtiscmpGCs :: GroundConstant -> GroundConstant -> Ordering

ddc0e0b53c661f6e439e3b7072b3ef353eadb4afRichard LowecmpGCs (GCI a) (GCI b) = compare a b

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtiscmpGCs (GCR a) (GCR b) = compare a b

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtiscmpGCs (GCI a) (GCR b) = swapCompare $ cmpFloatToInt b a

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtiscmpGCs (GCR a) (GCI b) = cmpFloatToInt a b

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisinstance Eq GroundConstant where

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis a == b = cmpGCs a b == EQ

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisinstance Ord GroundConstant where

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis compare = cmpGCs

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisinstance Continuous GroundConstant

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtistype Domain = SetOrInterval GroundConstant

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtistype EPDomain = ClosedInterval EPVal

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis-- | A constant or function definition

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisdata AssDefinition = ConstDef EXPRESSION | FunDef [String] EXPRESSION

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis deriving (Eq, Ord, Show, Typeable, Data)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisdata InstantiatedConstant = InstantiatedConstant

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis { constName :: ConstantName

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis , instantiation :: [EXPRESSION] } deriving (Show, Eq, Ord, Typeable, Data)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis{- | basic items: an operator, extended parameter or variable

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis declaration or an axiom -}

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisdata BASIC_ITEM =

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis Op_decl OP_ITEM

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | EP_decl [(Id.Token, EPDomain)]

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | EP_domdecl [(Id.Token, APInt)]

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | EP_defval [(Id.Token, APInt)]

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | Var_decls [VAR_ITEM]

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | Axiom_item (AS_Anno.Annoted CMD)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis deriving (Show, Typeable, Data)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis-- | Extended Parameter Datatype

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisdata EXTPARAM = EP Id.Token String APInt

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis deriving (Eq, Ord, Show, Typeable, Data)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisdata EPDecl = EPDecl Id.Token -- name

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis EPDomain -- a domain over which the ep ranges

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis (Maybe APInt) -- evtl. a default value

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis deriving (Eq, Ord, Show, Typeable, Data)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis{- | Extended Parameter value may be an integer or a reference to an 'EPDomVal'.

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisThis type is used for the domain specification of EPs (see 'EPDomain'). -}

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisdata EPVal = EPVal APInt | EPConstRef Id.Token

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis deriving (Eq, Ord, Show, Typeable, Data)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisgetEPVarRef :: EPVal -> Maybe Id.Token

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisgetEPVarRef (EPConstRef tok) = Just tok

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisgetEPVarRef _ = Nothing

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisdata OPNAME =

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis -- arithmetic operators

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_mult | OP_div | OP_plus | OP_minus | OP_neg | OP_pow

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis -- roots, trigonometric and other operators

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_fthrt | OP_sqrt | OP_abs | OP_max | OP_min | OP_sign

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_cos | OP_sin | OP_tan | OP_cot | OP_Pi

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_reldist

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis -- special CAS operators

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_minimize | OP_minloc | OP_maximize | OP_maxloc | OP_factor | OP_approx

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_divide | OP_factorize | OP_int | OP_rlqe | OP_simplify | OP_solve

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis -- comparison predicates

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_neq | OP_lt | OP_leq | OP_eq | OP_gt | OP_geq | OP_convergence

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_reldistLe

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis -- containment predicate

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_in

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis -- special CAS constants

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_undef | OP_failure

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis -- boolean constants and connectives

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_false | OP_true | OP_not | OP_and | OP_or | OP_impl

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis -- quantifiers

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_ex | OP_all

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis -- types

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis | OP_hastype | OP_real

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis deriving (Eq, Ord, Typeable, Data)

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtisinstance Show OPNAME where

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis show = showOPNAME

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisshowOPNAME :: OPNAME -> String

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr JasiukajtisshowOPNAME x =

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis case x of

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_neq -> "!="

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_mult -> "*"

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_plus -> "+"

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_minus -> "-"

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_neg -> "-"

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_div -> "/"

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_lt -> "<"

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_leq -> "<="

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_eq -> "="

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_gt -> ">"

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_geq -> ">="

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_Pi -> "Pi"

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_pow -> "^"

25c28e83beb90e7c80452a7c818c5e6f73a07dc8Piotr Jasiukajtis OP_abs -> "abs"

OP_sign -> "sign"

OP_all -> "all"

OP_and -> "and"

OP_convergence -> "convergence"

OP_cos -> "cos"

OP_divide -> "divide"

OP_ex -> "ex"

OP_factor -> "factor"

OP_factorize -> "factorize"

OP_fthrt -> "fthrt"

OP_impl -> "impl"

OP_int -> "int"

OP_max -> "max"

OP_maximize -> "maximize"

OP_maxloc -> "maxloc"

OP_min -> "min"

OP_minimize -> "minimize"

OP_minloc -> "minloc"

OP_not -> "not"

OP_or -> "or"

OP_reldist -> "reldist"

OP_reldistLe -> "reldistLe"

OP_rlqe -> "rlqe"

OP_simplify -> "simplify"

OP_sin -> "sin"

OP_solve -> "solve"

OP_sqrt -> "sqrt"

OP_tan -> "tan"

OP_cot -> "cot"

OP_false -> "false"

OP_true -> "true"

OP_in -> "in"

OP_approx -> "approx"

OP_undef -> "undef"

OP_failure -> "fail"

OP_hastype -> "::"

OP_real -> "real"

data OPID = OpId OPNAME | OpUser ConstantName

deriving (Eq, Ord, Show, Typeable, Data)

{- | We differentiate between simple constant names and indexed constant names

resulting from the extended parameter elimination. -}

data ConstantName = SimpleConstant String | ElimConstant String Int

deriving (Eq, Ord, Show, Typeable, Data)

{-

instance Show OPID where

show (OpId n) = show n

show (OpUser s) = show s

instance Show ConstantName where

show (SimpleConstant s) = s

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

-}

-- | Datatype for expressions

data EXPRESSION =

Var Id.Token

| Op OPID [EXTPARAM] [EXPRESSION] Id.Range

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

| List [EXPRESSION] Id.Range

| Interval Double Double Id.Range

| Int APInt Id.Range

| Rat APFloat Id.Range

deriving (Eq, Ord, Show, Typeable, Data)

data VarDecl = VarDecl Id.Token (Maybe Domain)

deriving (Show, Eq, Ord, Typeable, Data)

data OpDecl = OpDecl ConstantName [EXTPARAM] [VarDecl] Id.Range

deriving (Show, Eq, Ord, Typeable, Data)

-- TODO: add Range-support to this type

data CMD = Ass OpDecl EXPRESSION

| Cmd String [EXPRESSION]

| Sequence [CMD] -- program sequence

| Cond [(EXPRESSION, [CMD])]

| Repeat EXPRESSION [CMD] -- constraint, statements

deriving (Show, Eq, Ord, Typeable, Data)

-- | symbol lists for hiding

data SYMB_ITEMS = Symb_items [SYMB] Id.Range

-- pos: SYMB_KIND, commas

deriving (Show, Eq, Typeable, Data)

-- | symbol for identifiers

newtype SYMB = Symb_id Id.Token

-- pos: colon

deriving (Show, Eq, Typeable, Data)

-- | symbol maps for renamings

data SYMB_MAP_ITEMS = Symb_map_items [SYMB_OR_MAP] Id.Range

-- pos: SYMB_KIND, commas

deriving (Show, Eq, Typeable, Data)

-- | 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, Typeable, Data)

{- ---------------------------------------------------------------------------

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, Typeable, Data)

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, Typeable, Data)

type ArityMap = Map.Map Int OpInfo

type OpInfoArityMap a = Map.Map a ArityMap

type OpInfoMap = OpInfoArityMap String

type OpInfoNameMap = OpInfoArityMap OPNAME

type BindInfoMap = Map.Map String OpInfo

{- | 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 = foldl f Map.empty

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 = foldl f Map.empty

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

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

{- | a special map for binders which have to be unique for each name

(no different arities). -}

getBindInfoMap :: [OpInfo] -> BindInfoMap

getBindInfoMap = foldl f Map.empty

where f m oi@(OpInfo {bind = Just _}) =

Map.insertWith cf (show $ opname oi) oi m

f m _ = m

cf a _ = error $ "operatorBindInfoMap: duplicate entry for "

++ show (opname a)

-- | opInfoMap for the predefined 'operatorInfo'

operatorInfoMap :: OpInfoMap

operatorInfoMap = getOpInfoMap (show . opname) operatorInfo

-- | opInfoNameMap for the predefined 'operatorInfo'

operatorInfoNameMap :: OpInfoNameMap

operatorInfoNameMap = getOpInfoNameMap operatorInfo

operatorBindInfoMap :: BindInfoMap

operatorBindInfoMap = getBindInfoMap 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, OP_real ]

++ map (aX 1)

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

, OP_abs, OP_sign, OP_simplify, OP_rlqe, OP_factor

, OP_factorize ]

++ map (a2i 5) [ OP_hastype ]

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

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

++ map (a2i 40) [ OP_and ]

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

++ map (a2i 60) [ OP_plus ]

++ map (a2i 70) [ OP_minus ]

++ map (a2i 80) [OP_mult]

++ map (a2i 90) [OP_div]

++ map (a2i 100) [OP_pow]

++ map (aX 2)

[ OP_int, OP_divide, OP_solve, OP_convergence, OP_reldist

, OP_approx]

++ 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 = 120

{- ---------------------------------------------------------------------------

OpInfo lookup utils

--------------------------------------------------------------------------- -}

class OperatorState a where

addVar :: a -> String -> a

addVar = const

isVar :: a -> String -> Bool

isVar _ _ = False

lookupOperator :: a

-> String -- ^ operator name

-> Int -- ^ operator arity

-> Either Bool OpInfo

lookupBinder :: a

-> String -- ^ binder name

-> Maybe OpInfo

instance OperatorState () where

lookupOperator _ = lookupOpInfoForParsing operatorInfoMap

lookupBinder _ = flip Map.lookup operatorBindInfoMap

instance OperatorState (OpInfoMap, BindInfoMap) where

lookupOperator = lookupOpInfoForParsing . fst

lookupBinder = flip Map.lookup . snd

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