{- |

Module : $Header$

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