1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae BungiuDescription : datastructures for annotations of (Het)CASL.

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceCopyright : (c) Klaus Luettich, Christian Maeder, and Uni Bremen 2002-2006

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae BungiuLicense : GPLv2 or higher, see LICENSE.txt

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae BungiuMaintainer : Christian.Maeder@dfki.de

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae BungiuStability : provisional

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae BungiuPortability : portable

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae BungiuDatastructures for annotations of (Het)CASL.

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu There is also a paramterized data type for an 'Annoted' 'item'.

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu See also chapter II.5 of the CASL Reference Manual.

ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mance-}

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

386bd8214f3137fe84c392cd58338130d2f80607Felix Gabriel Mancemodule Common.AS_Annotation where

332dadf617c7fdc3353346f6b8e1c4d918214f3cChristian Maederimport Common.Id

332dadf617c7fdc3353346f6b8e1c4d918214f3cChristian Maederimport Common.IRI (IRI)

386bd8214f3137fe84c392cd58338130d2f80607Felix Gabriel Mance

386bd8214f3137fe84c392cd58338130d2f80607Felix Gabriel Manceimport Data.Data

386bd8214f3137fe84c392cd58338130d2f80607Felix Gabriel Manceimport Data.Maybe

386bd8214f3137fe84c392cd58338130d2f80607Felix Gabriel Manceimport qualified Data.Map as Map

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- DrIFT command

1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel Mance{-! global: GetRange !-}

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance-- | start of an annote with its WORD or a comment

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata Annote_word = Annote_word String | Comment_start

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder deriving (Show, Eq, Ord, Typeable, Data)

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | line or group for 'Unparsed_anno'

386bd8214f3137fe84c392cd58338130d2f80607Felix Gabriel Mancedata Annote_text = Line_anno String | Group_anno [String]

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance deriving (Show, Eq, Ord, Typeable, Data)

1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel Mance

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{- | formats to be displayed (may be extended in the future).

332dadf617c7fdc3353346f6b8e1c4d918214f3cChristian MaederDrop 3 from the show result to get the string for parsing and printing -}

332dadf617c7fdc3353346f6b8e1c4d918214f3cChristian Maederdata Display_format = DF_HTML | DF_LATEX | DF_RTF

332dadf617c7fdc3353346f6b8e1c4d918214f3cChristian Maeder deriving (Show, Eq, Ord, Typeable, Data)

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu-- | swap the entries of a lookup table

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae BungiuswapTable :: [(a, b)] -> [(b, a)]

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae BungiuswapTable = map $ \ (a, b) -> (b, a)

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | drop the first 3 characters from the show result

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae BungiutoTable :: (Show a) => [a] -> [(a, String)]

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae BungiutoTable = map $ \ a -> (a, drop 3 $ show a)

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiu-- | a lookup table for the textual representation of display formats

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiudisplay_format_table :: [(Display_format, String)]

5efb71382fdcce83a76a6d40e5f8def0462bf8a8Francisc Nicolae Bungiudisplay_format_table = toTable [ DF_HTML, DF_LATEX, DF_RTF ]

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance{- | lookup the textual representation of a display format

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mancein 'display_format_table' -}

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel MancelookupDisplayFormat :: Display_format -> String

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel MancelookupDisplayFormat df =

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance fromMaybe (error "lookupDisplayFormat: unknown display format")

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance $ lookup df display_format_table

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance{- | precedence 'Lower' means less and 'BothDirections' means less and greater.

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance'Higher' means greater but this is syntactically not allowed in 'Prec_anno'.

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance'NoDirection' can also not be specified explicitly,

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mancebut covers those ids that are not mentionend in precedences. -}

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mancedata PrecRel = Higher | Lower | BothDirections | NoDirection

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance deriving (Show, Eq, Ord, Typeable, Data)

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- | either left or right associative

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mancedata AssocEither = ALeft | ARight deriving (Show, Eq, Ord, Typeable, Data)

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance{- | semantic (line) annotations without further information.

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceUse the same drop-3-trick as for the 'Display_format'. -}

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mancedata Semantic_anno = SA_cons | SA_def | SA_implies | SA_mono | SA_implied

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance | SA_mcons | SA_ccons | SA_wdef

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance deriving (Show, Eq, Ord, Typeable, Data, Enum, Bounded)

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- | a lookup table for the textual representation of semantic annos

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mancesemantic_anno_table :: [(Semantic_anno, String)]

19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel Mancesemantic_anno_table =

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance toTable [minBound .. maxBound]

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance{- | lookup the textual representation of a semantic anno

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mancein 'semantic_anno_table' -}

1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel MancelookupSemanticAnno :: Semantic_anno -> String

332dadf617c7fdc3353346f6b8e1c4d918214f3cChristian MaederlookupSemanticAnno sa =

332dadf617c7fdc3353346f6b8e1c4d918214f3cChristian Maeder fromMaybe (error "lookupSemanticAnno: no semantic anno")

332dadf617c7fdc3353346f6b8e1c4d918214f3cChristian Maeder $ lookup sa semantic_anno_table

332dadf617c7fdc3353346f6b8e1c4d918214f3cChristian Maeder

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- | all possible annotations (without comment-outs)

332dadf617c7fdc3353346f6b8e1c4d918214f3cChristian Maederdata Annotation = -- | constructor for comments or unparsed annotes

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Unparsed_anno Annote_word Annote_text Range

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance -- | known annotes

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | Display_anno Id [(Display_format, String)] Range

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- position of anno start, keywords and anno end

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | List_anno Id Id Id Range

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- position of anno start, commas and anno end

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | Number_anno Id Range

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance -- position of anno start, commas and anno end

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | Float_anno Id Id Range

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance -- position of anno start, commas and anno end

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | String_anno Id Id Range

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- position of anno start, commas and anno end

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | Prec_anno PrecRel [Id] [Id] Range

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance {- positions: "{",commas,"}", RecRel, "{",commas,"}"

332dadf617c7fdc3353346f6b8e1c4d918214f3cChristian Maeder Lower = "< " BothDirections = "<>" -}

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | Assoc_anno AssocEither [Id] Range -- position of commas

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | Label [String] Range

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance -- position of anno start and anno end

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | Prefix_anno [(String, IRI)] Range

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance -- position of anno start and anno end

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance -- All annotations below are only as annote line allowed

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance | Semantic_anno Semantic_anno Range

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance {- position information for annotations is provided

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance by every annotation -}

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance deriving (Show, Eq, Ord, Typeable, Data)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance{- | 'isLabel' tests if the given 'Annotation' is a label

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance(a 'Label' typically follows a formula) -}

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisLabel :: Annotation -> Bool

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel ManceisLabel a = case a of

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Label _ _ -> True

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance _ -> False

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisImplies :: Annotation -> Bool

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisImplies a = case a of

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Semantic_anno SA_implies _ -> True

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance _ -> False

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisImplied :: Annotation -> Bool

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisImplied a = case a of

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Semantic_anno SA_implied _ -> True

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance _ -> False

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- | 'isSemanticAnno' tests if the given 'Annotation' is a semantic one

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisSemanticAnno :: Annotation -> Bool

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisSemanticAnno a = case a of

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Semantic_anno _ _ -> True

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance _ -> False

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance{- | 'isComment' tests if the given 'Annotation' is a comment line or a

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mancecomment group -}

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisComment :: Annotation -> Bool

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisComment c = case c of

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Unparsed_anno Comment_start _ _ -> True

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance _ -> False

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- | 'isAnnote' is the negation of 'isComment'

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisAnnote :: Annotation -> Bool

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel ManceisAnnote = not . isComment

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance-- | separate prefix annotations and put them into a map

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel MancepartPrefixes :: [Annotation] -> (Map.Map String IRI, [Annotation])

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel MancepartPrefixes = foldr (\ a (m, l) -> case a of

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance Prefix_anno p _ -> (Map.union m $ Map.fromList p, l)

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance _ -> (m, a : l)) (Map.empty, [])

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance{- | an item wrapped in preceding (left 'l_annos')

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Manceand following (right 'r_annos') annotations.

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mance'opt_pos' should carry the position of an optional semicolon

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mancefollowing a formula (but is currently unused). -}

e5ea4eeaeefd3521ae3475719e18c96cf91637d5Felix Gabriel Mancedata Annoted a = Annoted

386bd8214f3137fe84c392cd58338130d2f80607Felix Gabriel Mance { item :: a

1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel Mance , opt_pos :: Range

, l_annos :: [Annotation]

, r_annos :: [Annotation] } deriving (Show, Ord, Eq, Typeable, Data)

annoRange :: (a -> [Pos]) -> Annoted a -> [Pos]

annoRange f a =

joinRanges $ map (rangeToList . getRange) (l_annos a) ++ [f $ item a]

++ [rangeToList (opt_pos a)] ++ map (rangeToList . getRange) (r_annos a)

notImplied :: Annoted a -> Bool

notImplied = not . any isImplied . r_annos

-- | naming or labelling sentences

data SenAttr s a = SenAttr

{ senAttr :: a

, isAxiom :: Bool

, isDef :: Bool

, wasTheorem :: Bool

{- will be set to True when status of isAxiom

changes from False to True -}

, simpAnno :: Maybe Bool -- for %simp or %nosimp annotations

, attrOrigin :: Maybe Id

, senMark :: String -- a marker for theoroidal comorphisms

, sentence :: s } deriving (Eq, Ord, Show, Typeable, Data)

-- | equip a sentence with a name

makeNamed :: a -> s -> SenAttr s a

makeNamed a s = SenAttr

{ senAttr = a

, isAxiom = True

, isDef = False

, wasTheorem = False

, simpAnno = Nothing

, attrOrigin = Nothing

, senMark = ""

, sentence = s }

type Named s = SenAttr s String

markSen :: String -> Named s -> Named s

markSen m n = n { senMark = m }

unmark :: Named s -> Named s

unmark = markSen ""

reName :: (a -> b) -> SenAttr s a -> SenAttr s b

reName f x = x { senAttr = f $ senAttr x }

-- | extending sentence maps to maps on labelled sentences

mapNamed :: (s -> t) -> SenAttr s a -> SenAttr t a

mapNamed f x = x { sentence = f $ sentence x }

-- | extending sentence maybe-maps to maps on labelled sentences

mapNamedM :: Monad m => (s -> m t) -> Named s -> m (Named t)

mapNamedM f x = do

y <- f $ sentence x

return x {sentence = y}

-- | process all items and wrap matching annotations around the results

mapAnM :: (Monad m) => (a -> m b) -> [Annoted a] -> m [Annoted b]

mapAnM f al =

do il <- mapM (f . item) al

return $ zipWith (flip replaceAnnoted) al il

instance Functor Annoted where

fmap f (Annoted x o l r) = Annoted (f x) o l r

-- | replace the 'item'

replaceAnnoted :: b -> Annoted a -> Annoted b

replaceAnnoted x (Annoted _ o l r) = Annoted x o l r

{- one could use this fmap variant instead (less efficient)

replaceAnnoted x = fmap (const x)

or even:

replaceAnnoted = (<$) -}

-- | add further following annotations

appendAnno :: Annoted a -> [Annotation] -> Annoted a

appendAnno (Annoted x p l r) = Annoted x p l . (r ++)

-- | put together preceding annotations and an item

addLeftAnno :: [Annotation] -> a -> Annoted a

addLeftAnno l i = Annoted i nullRange l []

-- | decorate with no annotations

emptyAnno :: a -> Annoted a

emptyAnno = addLeftAnno []

-- | get the label following (or to the right of) an 'item'

getRLabel :: Annoted a -> String

getRLabel a =

case filter isLabel (r_annos a) of

Label l _ : _ -> unwords $ concatMap words l

_ -> ""

{- | check for an annotation starting with % and the input str

(does not work for known annotation words) -}

identAnno :: String -> Annotation -> Bool

identAnno str an = case an of

Unparsed_anno (Annote_word wrd) _ _ -> wrd == str

_ -> False

-- | test all anntotions for an item

hasIdentAnno :: String -> Annoted a -> Bool

hasIdentAnno str a = any (identAnno str) $ l_annos a ++ r_annos a

makeNamedSen :: Annoted a -> Named a

makeNamedSen a = (makeNamed (getRLabel a) $ item a)

{ isAxiom = notImplied a

, simpAnno = case (hasIdentAnno "simp" a, hasIdentAnno "nosimp" a) of

(True, False) -> Just True

(False, True) -> Just False

_ -> Nothing }

annoArg :: Annote_text -> String

annoArg txt = case txt of

Line_anno str -> str

Group_anno ls -> unlines ls

newtype Name = Name String deriving Typeable

instance Show Name where

show (Name s) = s

getAnnoName :: Annoted a -> Name

getAnnoName = Name . foldr (\ an -> case an of

Unparsed_anno (Annote_word wrd) txt _ | wrd == "name" ->

(annoArg txt ++)

_ -> id) "" . l_annos