hets/DFOL/Utils.hs

{- |
Module      :  ./DFOL/Utils.hs
Description :  Utilities for first-order logic with dependent types (DFOL)
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}

module DFOL.Utils where

import qualified Common.Result as Result

-- logical operators precedences
truePrec :: Int
truePrec = 1

falsePrec :: Int
falsePrec = 1

predPrec :: Int
predPrec = 1

equalPrec :: Int
equalPrec = 1

negPrec :: Int
negPrec = 2

conjPrec :: Int
conjPrec = 3

disjPrec :: Int
disjPrec = 3

implPrec :: Int
implPrec = 4

equivPrec :: Int
equivPrec = 4

forallPrec :: Int
forallPrec = 5

existsPrec :: Int
existsPrec = 5

sortPrec :: Int
sortPrec = 1

formPrec :: Int
formPrec = 1

univPrec :: Int
univPrec = 1

funcPrec :: Int
funcPrec = 2

piPrec :: Int
piPrec = 3

-- datatype for items annotated with diagnostic messages
data DIAGN a = Diagn
    { diags :: [Result.Diagnosis]
    , item :: a
    } deriving (Show, Eq)

-- conjunction for a list of truth values with diagnostic messages
andD :: [DIAGN Bool] -> DIAGN Bool
andD xs = Diagn diag result
          where result = all item xs
                diag = concatMap diags xs