AS_BASIC_CSL.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
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