hets/CommonLogic/Tools.hs

{- |
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 (s, i) ns =
    if Set.member n ns
       then freeName (s, i + 1) ns
       else (n, i + 1)
    where n = mkSimpleId (s ++ "_" ++ [intToDigit 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 f = Set.unions . map f

-- | retrieves the individual constants from a text
indvC_text :: TEXT -> Set NAME
indvC_text t =
    case t of
         Text ps _ -> setUnion_list indvC_phrase ps
         Named_text _ txt _ -> indvC_text txt

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

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

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

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

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

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

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

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

-- | retrieves the individual constant from a single argument
indvC_termSeq :: TERM_SEQ -> Set NAME
indvC_termSeq t =
    case t of
        Term_seq txt -> indvC_term txt
        Seq_marks _ -> 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 t =
    case t of
         Text ps _ -> prd_phrases ps
         Named_text _ nt _ -> prd_text nt

prd_phrases :: [PHRASE] -> Set.Set NAME
prd_phrases = setUnion_list prd_phrase

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

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

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

prd_quantSent :: QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Set.Set NAME
prd_quantSent _ _ = 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 b =
    case b of
         Junction _ ss -> setUnion_list prd_sentence ss
         Negation s -> prd_sentence s
         BinOp _ s1 s2 -> setUnion_list prd_sentence [s1, s2]

prd_atomSent :: ATOM -> Set.Set NAME
prd_atomSent a =
    case a of
         Equation t1 t2 -> setUnion_list prd_term [t1, t2]
         Atom t tseq -> -- the predicate name is in t
           Set.unions [prd_termSeqs tseq, prd_term t, prd_add_term t]

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

prd_termSeqs :: [TERM_SEQ] -> Set.Set NAME
prd_termSeqs = setUnion_list prd_termSeq

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

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