AS_Annotation.der.hs revision 2021aab879998f80e04855eb20812415b1aa8926
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{-# LANGUAGE DeriveDataTypeable #-}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiModule : $Header$
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiDescription : datastructures for annotations of (Het)CASL.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiCopyright : (c) Klaus Luettich, Christian Maeder, and Uni Bremen 2002-2006
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiLicense : GPLv2 or higher, see LICENSE.txt
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiMaintainer : Christian.Maeder@dfki.de
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiStability : provisional
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiPortability : portable
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiDatastructures for annotations of (Het)CASL.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski There is also a paramterized data type for an 'Annoted' 'item'.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski See also chapter II.5 of the CASL Reference Manual.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskiimport qualified Data.Map as Map
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- DrIFT command
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{-! global: GetRange !-}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | start of an annote with its WORD or a comment
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidata Annote_word = Annote_word String | Comment_start
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski deriving (Show, Eq, Ord, Typeable, Data)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | line or group for 'Unparsed_anno'
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidata Annote_text = Line_anno String | Group_anno [String]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski deriving (Show, Eq, Ord, Typeable, Data)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{- | formats to be displayed (may be extended in the future).
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiDrop 3 from the show result to get the string for parsing and printing -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidata Display_format = DF_HTML | DF_LATEX | DF_RTF
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski deriving (Show, Eq, Ord, Typeable, Data)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | swap the entries of a lookup table
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiswapTable :: [(a, b)] -> [(b, a)]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiswapTable = map $ \ (a, b) -> (b, a)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | drop the first 3 characters from the show result
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskitoTable :: (Show a) => [a] -> [(a, String)]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskitoTable = map $ \ a -> (a, drop 3 $ show a)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | a lookup table for the textual representation of display formats
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidisplay_format_table :: [(Display_format, String)]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidisplay_format_table = toTable [ DF_HTML, DF_LATEX, DF_RTF ]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{- | lookup the textual representation of a display format
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskiin 'display_format_table' -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskilookupDisplayFormat :: Display_format -> String
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskilookupDisplayFormat df =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski fromMaybe (error "lookupDisplayFormat: unknown display format")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski $ lookup df display_format_table
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{- | precedence 'Lower' means less and 'BothDirections' means less and greater.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski'Higher' means greater but this is syntactically not allowed in 'Prec_anno'.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski'NoDirection' can also not be specified explicitly,
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskibut covers those ids that are not mentionend in precedences. -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidata PrecRel = Higher | Lower | BothDirections | NoDirection
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski deriving (Show, Eq, Ord, Typeable, Data)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | either left or right associative
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidata AssocEither = ALeft | ARight deriving (Show, Eq, Ord, Typeable, Data)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{- | semantic (line) annotations without further information.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiUse the same drop-3-trick as for the 'Display_format'. -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidata Semantic_anno = SA_cons | SA_def | SA_implies | SA_mono | SA_implied
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski | SA_mcons | SA_ccons | SA_wdef
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski deriving (Show, Eq, Ord, Typeable, Data, Enum, Bounded)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | a lookup table for the textual representation of semantic annos
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskisemantic_anno_table :: [(Semantic_anno, String)]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskisemantic_anno_table =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski toTable [minBound .. maxBound]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{- | lookup the textual representation of a semantic anno
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskiin 'semantic_anno_table' -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskilookupSemanticAnno :: Semantic_anno -> String
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskilookupSemanticAnno sa =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski fromMaybe (error "lookupSemanticAnno: no semantic anno")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski $ lookup sa semantic_anno_table
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | all possible annotations (without comment-outs)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidata Annotation = -- | constructor for comments or unparsed annotes
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Unparsed_anno Annote_word Annote_text Range
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -- | known annotes
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski | Display_anno Id [(Display_format, String)] Range
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -- position of anno start, keywords and anno end
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski | List_anno Id Id Id Range
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -- position of anno start, commas and anno end
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski | Number_anno Id Range
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -- position of anno start, commas and anno end
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski | Float_anno Id Id Range
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -- position of anno start, commas and anno end
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski | String_anno Id Id Range
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -- position of anno start, commas and anno end
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski | Prec_anno PrecRel [Id] [Id] Range
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski {- positions: "{",commas,"}", RecRel, "{",commas,"}"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Lower = "< " BothDirections = "<>" -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski | Assoc_anno AssocEither [Id] Range -- position of commas
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski | Label [String] Range
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -- position of anno start and anno end
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski | Prefix_anno [(String, IRI)] Range
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -- position of anno start and anno end
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski -- All annotations below are only as annote line allowed
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski | Semantic_anno Semantic_anno Range
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski {- position information for annotations is provided
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski by every annotation -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski deriving (Show, Eq, Ord, Typeable, Data)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{- | 'isLabel' tests if the given 'Annotation' is a label
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(a 'Label' typically follows a formula) -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisLabel :: Annotation -> Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisLabel a = case a of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Label _ _ -> True
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisImplies :: Annotation -> Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisImplies a = case a of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Semantic_anno SA_implies _ -> True
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisImplied :: Annotation -> Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisImplied a = case a of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Semantic_anno SA_implied _ -> True
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | 'isSemanticAnno' tests if the given 'Annotation' is a semantic one
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisSemanticAnno :: Annotation -> Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisSemanticAnno a = case a of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Semantic_anno _ _ -> True
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{- | 'isComment' tests if the given 'Annotation' is a comment line or a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskicomment group -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisComment :: Annotation -> Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisComment c = case c of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Unparsed_anno Comment_start _ _ -> True
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | 'isAnnote' is the negation of 'isComment'
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisAnnote :: Annotation -> Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiisAnnote = not . isComment
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | separate prefix annotations and put them into a map
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskipartPrefixes :: [Annotation] -> (Map.Map String IRI, [Annotation])
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskipartPrefixes = foldr (\ a (m, l) -> case a of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Prefix_anno p _ -> (Map.union m $ Map.fromList p, l)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski _ -> (m, a : l)) (Map.empty, [])
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{- | an item wrapped in preceding (left 'l_annos')
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskiand following (right 'r_annos') annotations.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski'opt_pos' should carry the position of an optional semicolon
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskifollowing a formula (but is currently unused). -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidata Annoted a = Annoted
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , opt_pos :: Range
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , l_annos :: [Annotation]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , r_annos :: [Annotation] } deriving (Show, Ord, Eq, Typeable, Data)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiannoRange :: (a -> [Pos]) -> Annoted a -> [Pos]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiannoRange f a =
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski joinRanges $ map (rangeToList . getRange) (l_annos a) ++ [f $ item a]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ++ [rangeToList (opt_pos a)] ++ map (rangeToList . getRange) (r_annos a)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskinotImplied :: Annoted a -> Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskinotImplied = not . any isImplied . r_annos
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | naming or labelling sentences
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskidata SenAttr s a = SenAttr
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski { senAttr :: a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , priority :: Maybe String
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , isAxiom :: Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , isDef :: Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , wasTheorem :: Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski {- will be set to True when status of isAxiom
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski changes from False to True -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , simpAnno :: Maybe Bool -- for %simp or %nosimp annotations
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , attrOrigin :: Maybe Id
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , senMark :: String -- a marker for theoroidal comorphisms
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , sentence :: s } deriving (Eq, Ord, Show, Typeable, Data)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | equip a sentence with a name
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeNamed :: a -> s -> SenAttr s a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeNamed a s = SenAttr
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski { senAttr = a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , priority = Nothing
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , isAxiom = True
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , isDef = False
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , wasTheorem = False
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , simpAnno = Nothing
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , attrOrigin = Nothing
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , senMark = ""
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , sentence = s }
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskitype Named s = SenAttr s String
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimarkSen :: String -> Named s -> Named s
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimarkSen m n = n { senMark = m }
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskiunmark :: Named s -> Named s
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskiunmark = markSen ""
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskireName :: (a -> b) -> SenAttr s a -> SenAttr s b
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskireName f x = x { senAttr = f $ senAttr x }
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | extending sentence maps to maps on labelled sentences
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimapNamed :: (s -> t) -> SenAttr s a -> SenAttr t a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimapNamed f x = x { sentence = f $ sentence x }
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | extending sentence maybe-maps to maps on labelled sentences
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimapNamedM :: Monad m => (s -> m t) -> Named s -> m (Named t)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimapNamedM f x = do
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski y <- f $ sentence x
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski return x {sentence = y}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | process all items and wrap matching annotations around the results
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimapAnM :: (Monad m) => (a -> m b) -> [Annoted a] -> m [Annoted b]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski do il <- mapM (f . item) al
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski return $ zipWith (flip replaceAnnoted) al il
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskiinstance Functor Annoted where
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski fmap f (Annoted x o l r) = Annoted (f x) o l r
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | replace the 'item'
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskireplaceAnnoted :: b -> Annoted a -> Annoted b
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskireplaceAnnoted x (Annoted _ o l r) = Annoted x o l r
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{- one could use this fmap variant instead (less efficient)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskireplaceAnnoted x = fmap (const x)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskireplaceAnnoted = (<$) -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | add further following annotations
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiappendAnno :: Annoted a -> [Annotation] -> Annoted a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiappendAnno (Annoted x p l r) = Annoted x p l . (r ++)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | put together preceding annotations and an item
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiaddLeftAnno :: [Annotation] -> a -> Annoted a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiaddLeftAnno l i = Annoted i nullRange l []
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | decorate with no annotations
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiemptyAnno :: a -> Annoted a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiemptyAnno = addLeftAnno []
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | get the label following (or to the right of) an 'item'
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskigetRLabel :: Annoted a -> String
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski case filter isLabel (r_annos a) of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Label l _ : _ -> unwords $ concatMap words l
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski{- | check for an annotation starting with % and the input str
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(does not work for known annotation words) -}
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiidentAnno :: String -> Annotation -> Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiidentAnno str an = case an of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Unparsed_anno (Annote_word wrd) _ _ -> wrd == str
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski-- | test all anntotions for an item
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskihasIdentAnno :: String -> Annoted a -> Bool
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskihasIdentAnno str a = any (identAnno str) $ l_annos a ++ r_annos a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskigetPriority :: [Annotation] -> Maybe String
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskigetPriority = foldl
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (\ mId anno -> case anno of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Unparsed_anno (Annote_word "priority") (Group_anno (x : _)) _ -> Just x
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeNamedSen :: Annoted a -> Named a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskimakeNamedSen a = (makeNamed (getRLabel a) $ item a)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski { isAxiom = notImplied a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , priority = getPriority $ r_annos a
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski , simpAnno = case (hasIdentAnno "simp" a, hasIdentAnno "nosimp" a) of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (True, False) -> Just True
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (False, True) -> Just False
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski _ -> Nothing }
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskiannoArg :: Annote_text -> String
453058446f4b25ac85504960f6aaf8d9e4bc1a9bTill MossakowskiannoArg txt = case txt of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Line_anno str -> str
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Group_anno ls -> unlines ls
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskinewtype Name = Name String deriving Typeable
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowskiinstance Show Name where
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski show (Name s) = s
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskigetAnnoName :: Annoted a -> Name
f93990c928a2b0b8f970b86d0fbd18d604147af6Till MossakowskigetAnnoName = Name . foldr (\ an -> case an of
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski Unparsed_anno (Annote_word wrd) txt _ | wrd == "name" ->
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (annoArg txt ++)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski _ -> id) "" . l_annos