89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./DFOL/Utils.hs

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaDescription : Utilities for first-order logic with dependent types (DFOL)

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaCopyright : (c) Kristina Sojakova, DFKI Bremen 2009

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaMaintainer : k.sojakova@jacobs-university.de

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaStability : experimental

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaPortability : portable

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova-}

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakovamodule DFOL.Utils where

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovaimport qualified Common.Result as Result

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova-- logical operators precedences

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovatruePrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovatruePrec = 1

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovafalsePrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovafalsePrec = 1

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovapredPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovapredPrec = 1

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaequalPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaequalPrec = 1

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovanegPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovanegPrec = 2

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaconjPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaconjPrec = 3

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovadisjPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovadisjPrec = 3

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaimplPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaimplPrec = 4

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaequivPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaequivPrec = 4

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaforallPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaforallPrec = 5

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaexistsPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaexistsPrec = 5

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovasortPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovasortPrec = 1

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaformPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaformPrec = 1

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaunivPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovaunivPrec = 1

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovafuncPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovafuncPrec = 2

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovapiPrec :: Int

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovapiPrec = 3

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- datatype for items annotated with diagnostic messages

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakovadata DIAGN a = Diagn

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova { diags :: [Result.Diagnosis]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , item :: a

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova } deriving (Show, Eq)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova-- conjunction for a list of truth values with diagnostic messages

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaandD :: [DIAGN Bool] -> DIAGN Bool

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina SojakovaandD xs = Diagn diag result

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder where result = all item xs

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder diag = concatMap diags xs