{- |
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