{- |
Module      :  ./CommonLogic/Tools.hs
Description :  Tools for CommonLogic static analysis
Copyright   :  (c) Eugen Kuksa, Uni Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  eugenk@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

Tools for CommonLogic static analysis
-}

module CommonLogic.Tools
  ( freeName      -- finds a free discourse name
  , indvC_text    -- retrieves all discourse names from a text
  , indvC_sen     -- retrieves all discourse names from a sentence
  , indvC_term    -- retrieves all discourse names from a term
  , prd_text      -- retrieves all predicates from a text
  , setUnion_list -- maps function @f@ to the list @ts@ and unifies the results
  ) where

import Data.Char (intToDigit)
import Data.Set (Set)
import qualified Data.Set as Set
import CommonLogic.AS_CommonLogic
import Common.Id


{- -----------------------------------------------------------------------------
Misc functions                                                            --
----------------------------------------------------------------------------- -}

{- | Finds a free discourse name (appends "_" at the end until free name found)
given the set of all discourse names -}
freeName :: (String, Int) -> Set NAME -> (NAME, Int)
freeName :: (String, Int) -> Set NAME -> (NAME, Int)
freeName (s :: String
s, i :: Int
i) ns :: Set NAME
ns =
    if NAME -> Set NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member NAME
n Set NAME
ns
       then (String, Int) -> Set NAME -> (NAME, Int)
freeName (String
s, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Set NAME
ns
       else (NAME
n, Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
    where n :: NAME
n = String -> NAME
mkSimpleId (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int -> Char
intToDigit Int
i])

{- -----------------------------------------------------------------------------
Functions to compute the set of individual constants (discourse items),   --
these work by recursing into all subelements                              --
----------------------------------------------------------------------------- -}

-- | maps @f@ to @ts@ and unifies the results
setUnion_list :: (Ord b) => (a -> Set b) -> [a] -> Set b
setUnion_list :: (a -> Set b) -> [a] -> Set b
setUnion_list f :: a -> Set b
f = [Set b] -> Set b
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set b] -> Set b) -> ([a] -> [Set b]) -> [a] -> Set b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Set b) -> [a] -> [Set b]
forall a b. (a -> b) -> [a] -> [b]
map a -> Set b
f

-- | retrieves the individual constants from a text
indvC_text :: TEXT -> Set NAME
indvC_text :: TEXT -> Set NAME
indvC_text t :: TEXT
t =
    case TEXT
t of
         Text ps :: [PHRASE]
ps _ -> (PHRASE -> Set NAME) -> [PHRASE] -> Set NAME
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
setUnion_list PHRASE -> Set NAME
indvC_phrase [PHRASE]
ps
         Named_text _ txt :: TEXT
txt _ -> TEXT -> Set NAME
indvC_text TEXT
txt

-- | retrieves the individual constants from a phrase
indvC_phrase :: PHRASE -> Set NAME
indvC_phrase :: PHRASE -> Set NAME
indvC_phrase p :: PHRASE
p =
    case PHRASE
p of
         Module m :: MODULE
m -> MODULE -> Set NAME
indvC_module MODULE
m
         Sentence s :: SENTENCE
s -> SENTENCE -> Set NAME
indvC_sen SENTENCE
s
         Comment_text _ t :: TEXT
t _ -> TEXT -> Set NAME
indvC_text TEXT
t
         _ -> Set NAME
forall a. Set a
Set.empty

-- | retrieves the individual constants from a module
indvC_module :: MODULE -> Set NAME
indvC_module :: MODULE -> Set NAME
indvC_module m :: MODULE
m =
    case MODULE
m of
         Mod _ t :: TEXT
t _ -> TEXT -> Set NAME
indvC_text TEXT
t
         Mod_ex _ _ t :: TEXT
t _ -> TEXT -> Set NAME
indvC_text TEXT
t

-- | retrieves the individual constants from a sentence
indvC_sen :: SENTENCE -> Set NAME
indvC_sen :: SENTENCE -> Set NAME
indvC_sen s :: SENTENCE
s =
    case SENTENCE
s of
         Quant_sent q :: QUANT
q vs :: [NAME_OR_SEQMARK]
vs is :: SENTENCE
is _ -> QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Set NAME
indvC_quantsent QUANT
q [NAME_OR_SEQMARK]
vs SENTENCE
is
         Bool_sent b :: BOOL_SENT
b _ -> BOOL_SENT -> Set NAME
indvC_boolsent BOOL_SENT
b
         Atom_sent a :: ATOM
a _ -> ATOM -> Set NAME
indvC_atomsent ATOM
a
         Comment_sent _ c :: SENTENCE
c _ -> SENTENCE -> Set NAME
indvC_sen SENTENCE
c
         Irregular_sent i :: SENTENCE
i _ -> SENTENCE -> Set NAME
indvC_sen SENTENCE
i

-- | retrieves the individual constants from a quantified sentence
indvC_quantsent :: QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Set NAME
indvC_quantsent :: QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Set NAME
indvC_quantsent _ = [NAME_OR_SEQMARK] -> SENTENCE -> Set NAME
quant
    where quant :: [NAME_OR_SEQMARK] -> SENTENCE -> Set NAME
          quant :: [NAME_OR_SEQMARK] -> SENTENCE -> Set NAME
quant nss :: [NAME_OR_SEQMARK]
nss se :: SENTENCE
se = Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (SENTENCE -> Set NAME
indvC_sen SENTENCE
se)
            (Set NAME -> Set NAME) -> Set NAME -> Set NAME
forall a b. (a -> b) -> a -> b
$ (NAME_OR_SEQMARK -> Set NAME) -> [NAME_OR_SEQMARK] -> Set NAME
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
setUnion_list NAME_OR_SEQMARK -> Set NAME
nameof [NAME_OR_SEQMARK]
nss
          nameof :: NAME_OR_SEQMARK -> Set NAME
          nameof :: NAME_OR_SEQMARK -> Set NAME
nameof nsm :: NAME_OR_SEQMARK
nsm =
              case NAME_OR_SEQMARK
nsm of
                   Name n :: NAME
n -> NAME -> Set NAME
forall a. a -> Set a
Set.singleton NAME
n
                   SeqMark _ -> Set NAME
forall a. Set a
Set.empty -- see indvC_termSeq

-- | retrieves the individual constants from a boolean sentence
indvC_boolsent :: BOOL_SENT -> Set NAME
indvC_boolsent :: BOOL_SENT -> Set NAME
indvC_boolsent b :: BOOL_SENT
b =
    case BOOL_SENT
b of
         Junction _ ss :: [SENTENCE]
ss -> (SENTENCE -> Set NAME) -> [SENTENCE] -> Set NAME
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
setUnion_list SENTENCE -> Set NAME
indvC_sen [SENTENCE]
ss
         Negation s :: SENTENCE
s -> SENTENCE -> Set NAME
indvC_sen SENTENCE
s
         BinOp _ s1 :: SENTENCE
s1 s2 :: SENTENCE
s2 -> (SENTENCE -> Set NAME) -> [SENTENCE] -> Set NAME
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
setUnion_list SENTENCE -> Set NAME
indvC_sen [SENTENCE
s1, SENTENCE
s2]

-- | retrieves the individual constants from an atom
indvC_atomsent :: ATOM -> Set NAME
indvC_atomsent :: ATOM -> Set NAME
indvC_atomsent a :: ATOM
a =
    case ATOM
a of
         Equation t1 :: TERM
t1 t2 :: TERM
t2 -> TERM -> Set NAME
indvC_term TERM
t1 Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` TERM -> Set NAME
indvC_term TERM
t2
         Atom t :: TERM
t ts :: [TERM_SEQ]
ts -> Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TERM -> Set NAME
nonToplevelNames TERM
t)
                    (Set NAME -> Set NAME) -> Set NAME -> Set NAME
forall a b. (a -> b) -> a -> b
$ (TERM_SEQ -> Set NAME) -> [TERM_SEQ] -> Set NAME
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
setUnion_list TERM_SEQ -> Set NAME
indvC_termSeq [TERM_SEQ]
ts -- arguments

-- | omit predicate names
nonToplevelNames :: TERM -> Set NAME
nonToplevelNames :: TERM -> Set NAME
nonToplevelNames trm :: TERM
trm = case TERM
trm of
        Name_term _ -> Set NAME
forall a. Set a
Set.empty
        Comment_term t :: TERM
t _ _ -> TERM -> Set NAME
nonToplevelNames TERM
t
        _ -> TERM -> Set NAME
indvC_term TERM
trm

-- | retrieves the individual constants from a term
indvC_term :: TERM -> Set NAME
indvC_term :: TERM -> Set NAME
indvC_term trm :: TERM
trm =
    case TERM
trm of
        Name_term n :: NAME
n -> NAME -> Set NAME
forall a. a -> Set a
Set.singleton NAME
n
        Funct_term t :: TERM
t ts :: [TERM_SEQ]
ts _ -> Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TERM -> Set NAME
indvC_term TERM
t)
          (Set NAME -> Set NAME) -> Set NAME -> Set NAME
forall a b. (a -> b) -> a -> b
$ (TERM_SEQ -> Set NAME) -> [TERM_SEQ] -> Set NAME
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
setUnion_list TERM_SEQ -> Set NAME
indvC_termSeq [TERM_SEQ]
ts -- arguments
        Comment_term t :: TERM
t _ _ -> TERM -> Set NAME
indvC_term TERM
t
        That_term s :: SENTENCE
s _ -> SENTENCE -> Set NAME
indvC_sen SENTENCE
s

-- | retrieves the individual constant from a single argument
indvC_termSeq :: TERM_SEQ -> Set NAME
indvC_termSeq :: TERM_SEQ -> Set NAME
indvC_termSeq t :: TERM_SEQ
t =
    case TERM_SEQ
t of
        Term_seq txt :: TERM
txt -> TERM -> Set NAME
indvC_term TERM
txt
        Seq_marks _ -> Set NAME
forall a. Set a
Set.empty

{- ----------------------------------------------------------------------------
Functions to compute the set of predicates, these work by recursing      --
into all subelements                                                     --
---------------------------------------------------------------------------- -}

-- | Retrieves all predicates from a text
prd_text :: TEXT -> Set.Set NAME
prd_text :: TEXT -> Set NAME
prd_text t :: TEXT
t =
    case TEXT
t of
         Text ps :: [PHRASE]
ps _ -> [PHRASE] -> Set NAME
prd_phrases [PHRASE]
ps
         Named_text _ nt :: TEXT
nt _ -> TEXT -> Set NAME
prd_text TEXT
nt

prd_phrases :: [PHRASE] -> Set.Set NAME
prd_phrases :: [PHRASE] -> Set NAME
prd_phrases = (PHRASE -> Set NAME) -> [PHRASE] -> Set NAME
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
setUnion_list PHRASE -> Set NAME
prd_phrase

prd_phrase :: PHRASE -> Set.Set NAME
prd_phrase :: PHRASE -> Set NAME
prd_phrase p :: PHRASE
p =
    case PHRASE
p of
         Module m :: MODULE
m -> MODULE -> Set NAME
prd_module MODULE
m
         Sentence s :: SENTENCE
s -> SENTENCE -> Set NAME
prd_sentence SENTENCE
s
         Importation _ -> Set NAME
forall a. Set a
Set.empty
         Comment_text _ t :: TEXT
t _ -> TEXT -> Set NAME
prd_text TEXT
t

prd_module :: MODULE -> Set.Set NAME
prd_module :: MODULE -> Set NAME
prd_module m :: MODULE
m =
    case MODULE
m of
         Mod _ t :: TEXT
t _ -> TEXT -> Set NAME
prd_text TEXT
t
         Mod_ex _ _ t :: TEXT
t _ -> TEXT -> Set NAME
prd_text TEXT
t

prd_sentence :: SENTENCE -> Set.Set NAME
prd_sentence :: SENTENCE -> Set NAME
prd_sentence s :: SENTENCE
s =
    case SENTENCE
s of
         Quant_sent q :: QUANT
q vs :: [NAME_OR_SEQMARK]
vs is :: SENTENCE
is _ -> QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Set NAME
prd_quantSent QUANT
q [NAME_OR_SEQMARK]
vs SENTENCE
is
         Bool_sent b :: BOOL_SENT
b _ -> BOOL_SENT -> Set NAME
prd_boolSent BOOL_SENT
b
         Atom_sent a :: ATOM
a _ -> ATOM -> Set NAME
prd_atomSent ATOM
a
         Comment_sent _ c :: SENTENCE
c _ -> SENTENCE -> Set NAME
prd_sentence SENTENCE
c
         Irregular_sent i :: SENTENCE
i _ -> SENTENCE -> Set NAME
prd_sentence SENTENCE
i

prd_quantSent :: QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Set.Set NAME
prd_quantSent :: QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Set NAME
prd_quantSent _ _ = SENTENCE -> Set NAME
prd_sentence
{- we do not know if variables are predicates, we assume no, and only
check the body -}

prd_boolSent :: BOOL_SENT -> Set.Set NAME
prd_boolSent :: BOOL_SENT -> Set NAME
prd_boolSent b :: BOOL_SENT
b =
    case BOOL_SENT
b of
         Junction _ ss :: [SENTENCE]
ss -> (SENTENCE -> Set NAME) -> [SENTENCE] -> Set NAME
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
setUnion_list SENTENCE -> Set NAME
prd_sentence [SENTENCE]
ss
         Negation s :: SENTENCE
s -> SENTENCE -> Set NAME
prd_sentence SENTENCE
s
         BinOp _ s1 :: SENTENCE
s1 s2 :: SENTENCE
s2 -> (SENTENCE -> Set NAME) -> [SENTENCE] -> Set NAME
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
setUnion_list SENTENCE -> Set NAME
prd_sentence [SENTENCE
s1, SENTENCE
s2]

prd_atomSent :: ATOM -> Set.Set NAME
prd_atomSent :: ATOM -> Set NAME
prd_atomSent a :: ATOM
a =
    case ATOM
a of
         Equation t1 :: TERM
t1 t2 :: TERM
t2 -> (TERM -> Set NAME) -> [TERM] -> Set NAME
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
setUnion_list TERM -> Set NAME
prd_term [TERM
t1, TERM
t2]
         Atom t :: TERM
t tseq :: [TERM_SEQ]
tseq -> -- the predicate name is in t
           [Set NAME] -> Set NAME
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [[TERM_SEQ] -> Set NAME
prd_termSeqs [TERM_SEQ]
tseq, TERM -> Set NAME
prd_term TERM
t, TERM -> Set NAME
prd_add_term TERM
t]

prd_term :: TERM -> Set.Set NAME
prd_term :: TERM -> Set NAME
prd_term t :: TERM
t =
  case TERM
t of
    Name_term _ -> Set NAME
forall a. Set a
Set.empty
    Funct_term ft :: TERM
ft tseqs :: [TERM_SEQ]
tseqs _ -> TERM -> Set NAME
prd_term TERM
ft Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` [TERM_SEQ] -> Set NAME
prd_termSeqs [TERM_SEQ]
tseqs
      -- the function name is not a predicate
    Comment_term ct :: TERM
ct _ _ -> TERM -> Set NAME
prd_term TERM
ct
    That_term s :: SENTENCE
s _ -> SENTENCE -> Set NAME
prd_sentence SENTENCE
s

prd_termSeqs :: [TERM_SEQ] -> Set.Set NAME
prd_termSeqs :: [TERM_SEQ] -> Set NAME
prd_termSeqs = (TERM_SEQ -> Set NAME) -> [TERM_SEQ] -> Set NAME
forall b a. Ord b => (a -> Set b) -> [a] -> Set b
setUnion_list TERM_SEQ -> Set NAME
prd_termSeq

prd_termSeq :: TERM_SEQ -> Set.Set NAME
prd_termSeq :: TERM_SEQ -> Set NAME
prd_termSeq tsec :: TERM_SEQ
tsec =
    case TERM_SEQ
tsec of
         Term_seq t :: TERM
t -> TERM -> Set NAME
prd_term TERM
t
         Seq_marks _ -> Set NAME
forall a. Set a
Set.empty

prd_add_term :: TERM -> Set.Set NAME
prd_add_term :: TERM -> Set NAME
prd_add_term t :: TERM
t =
  case TERM
t of
    Name_term n :: NAME
n -> NAME -> Set NAME
forall a. a -> Set a
Set.singleton NAME
n
    Comment_term ct :: TERM
ct _ _ -> TERM -> Set NAME
prd_add_term TERM
ct
    _ -> Set NAME
forall a. Set a
Set.empty -- from all other terms we do not extract the predicate name