{- |
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 :: Int
truePrec = 1

falsePrec :: Int
falsePrec :: Int
falsePrec = 1

predPrec :: Int
predPrec :: Int
predPrec = 1

equalPrec :: Int
equalPrec :: Int
equalPrec = 1

negPrec :: Int
negPrec :: Int
negPrec = 2

conjPrec :: Int
conjPrec :: Int
conjPrec = 3

disjPrec :: Int
disjPrec :: Int
disjPrec = 3

implPrec :: Int
implPrec :: Int
implPrec = 4

equivPrec :: Int
equivPrec :: Int
equivPrec = 4

forallPrec :: Int
forallPrec :: Int
forallPrec = 5

existsPrec :: Int
existsPrec :: Int
existsPrec = 5

sortPrec :: Int
sortPrec :: Int
sortPrec = 1

formPrec :: Int
formPrec :: Int
formPrec = 1

univPrec :: Int
univPrec :: Int
univPrec = 1

funcPrec :: Int
funcPrec :: Int
funcPrec = 2

piPrec :: Int
piPrec :: Int
piPrec = 3

-- datatype for items annotated with diagnostic messages
data DIAGN a = Diagn
    { DIAGN a -> [Diagnosis]
diags :: [Result.Diagnosis]
    , DIAGN a -> a
item :: a
    } deriving (Int -> DIAGN a -> ShowS
[DIAGN a] -> ShowS
DIAGN a -> String
(Int -> DIAGN a -> ShowS)
-> (DIAGN a -> String) -> ([DIAGN a] -> ShowS) -> Show (DIAGN a)
forall a. Show a => Int -> DIAGN a -> ShowS
forall a. Show a => [DIAGN a] -> ShowS
forall a. Show a => DIAGN a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DIAGN a] -> ShowS
$cshowList :: forall a. Show a => [DIAGN a] -> ShowS
show :: DIAGN a -> String
$cshow :: forall a. Show a => DIAGN a -> String
showsPrec :: Int -> DIAGN a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> DIAGN a -> ShowS
Show, DIAGN a -> DIAGN a -> Bool
(DIAGN a -> DIAGN a -> Bool)
-> (DIAGN a -> DIAGN a -> Bool) -> Eq (DIAGN a)
forall a. Eq a => DIAGN a -> DIAGN a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DIAGN a -> DIAGN a -> Bool
$c/= :: forall a. Eq a => DIAGN a -> DIAGN a -> Bool
== :: DIAGN a -> DIAGN a -> Bool
$c== :: forall a. Eq a => DIAGN a -> DIAGN a -> Bool
Eq)

-- conjunction for a list of truth values with diagnostic messages
andD :: [DIAGN Bool] -> DIAGN Bool
andD :: [DIAGN Bool] -> DIAGN Bool
andD xs :: [DIAGN Bool]
xs = [Diagnosis] -> Bool -> DIAGN Bool
forall a. [Diagnosis] -> a -> DIAGN a
Diagn [Diagnosis]
diag Bool
result
          where result :: Bool
result = (DIAGN Bool -> Bool) -> [DIAGN Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all DIAGN Bool -> Bool
forall a. DIAGN a -> a
item [DIAGN Bool]
xs
                diag :: [Diagnosis]
diag = (DIAGN Bool -> [Diagnosis]) -> [DIAGN Bool] -> [Diagnosis]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DIAGN Bool -> [Diagnosis]
forall a. DIAGN a -> [Diagnosis]
diags [DIAGN Bool]
xs