AS_Annotation.der.hs revision 5446bb8eec1ac2d664fad5298ebb95da76b22a09
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiModule : $Header$
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiCopyright : (c) Klaus L�ttich, Christian Maeder, and Uni Bremen 2002-2005
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiMaintainer : maeder@tzi.de
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiStability : provisional
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiPortability : portable
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiThese datastructures describe the Annotations of (Het)CASL.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski There is also a paramterized data type for an 'Annoted' 'item'.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski See also chapter II.5 of the CASL Reference Manual.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- DrIFT command
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski{-! global: UpPos !-}
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | start of an annote with its WORD or a comment
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Annote_word = Annote_word String | Comment_start deriving (Show, Eq)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | line or group for 'Unparsed_anno'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Annote_text = Line_anno String | Group_anno [String] deriving (Show, Eq)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | formats to be displayed (may be extended in the future).
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- Drop 3 from the show result to get the string for parsing and printing
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Display_format = DF_HTML | DF_LATEX | DF_RTF deriving (Show, Eq, Ord)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | swap the entries of a lookup table
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiswapTable :: [(a, b)] -> [(b, a)]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiswapTable = map $ \ (a, b) -> (b, a)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | drop the first 3 characters from the show result
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskitoTable :: (Show a) => [a] -> [(a, String)]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskitoTable = map $ \a -> (a, drop 3 $ show a)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | a lookup table for the textual representation of display formats
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidisplay_format_table :: [(Display_format, String)]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidisplay_format_table = toTable [ DF_HTML, DF_LATEX, DF_RTF ]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | lookup the textual representation of a display format
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- in 'display_format_table'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskilookupDisplayFormat :: Display_format -> String
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskilookupDisplayFormat df =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski maybe (error "lookupDisplayFormat: unknown display format")
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski id $ lookup df display_format_table
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | precedence 'Lower' means less and 'BothDirections' means less and greater.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- 'Higher' means greater but this is syntactically not allowed in 'Prec_anno'.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- 'NoDirection' can also not be specified explicitly,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- but covers those ids that are not mentionend in precedences.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata PrecRel = Higher | Lower | BothDirections | NoDirection
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski deriving (Show, Eq)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | either left or right associative
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata AssocEither = ALeft | ARight deriving (Show, Eq)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | semantic (line) annotations without further information.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- Use the same drop-3-trick as for the 'Display_format'.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Semantic_anno = SA_cons | SA_def | SA_implies | SA_mono | SA_implied
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski deriving (Show, Eq)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | a lookup table for the textual representation of semantic annos
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskisemantic_anno_table :: [(Semantic_anno, String)]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskisemantic_anno_table = toTable [SA_cons, SA_def,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski SA_implies, SA_mono, SA_implied]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | lookup the textual representation of a semantic anno
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- in 'semantic_anno_table'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskilookupSemanticAnno :: Semantic_anno -> String
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskilookupSemanticAnno sa =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski maybe (error "lookupSemanticAnno: no semantic anno")
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski id $ lookup sa semantic_anno_table
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | all possible annotations (without comment-outs)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Annotation = -- | constructor for comments or unparsed annotes
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Unparsed_anno Annote_word Annote_text Range
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- | known annotes
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | Display_anno Id [(Display_format, String)] Range
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- postion of anno start, keywords and anno end
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | List_anno Id Id Id Range
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- postion of anno start, commas and anno end
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | Number_anno Id Range
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- postion of anno start, commas and anno end
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | Float_anno Id Id Range
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- postion of anno start, commas and anno end
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | String_anno Id Id Range
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- postion of anno start, commas and anno end
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | Prec_anno PrecRel [Id] [Id] Range
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- ^ positions: "{",commas,"}", RecRel, "{",commas,"}"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- | Lower = "< " BothDirections = "<>"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | Assoc_anno AssocEither [Id] Range -- position of commas
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | Label [String] Range
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- postion of anno start and anno end
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- All annotations below are only as annote line allowed
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | Semantic_anno Semantic_anno Range
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- position information for annotations is provided
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- by every annotation
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski deriving (Show, Eq)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- 'isLabel' tests if the given 'Annotation' is a label
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- (a 'Label' typically follows a formula)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisLabel :: Annotation -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisLabel a = case a of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Label _ _ -> True
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisImplies :: Annotation -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisImplies a = case a of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Semantic_anno SA_implies _ -> True
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisImplied :: Annotation -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisImplied a = case a of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Semantic_anno SA_implied _ -> True
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- 'isSemanticAnno' tests if the given 'Annotation' is a semantic one
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisSemanticAnno :: Annotation -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisSemanticAnno a = case a of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Semantic_anno _ _ -> True
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- 'isComment' tests if the given 'Annotation' is a comment line or a
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- comment group
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisComment :: Annotation -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisComment c = case c of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Unparsed_anno Comment_start _ _ -> True
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- 'isAnnote' is the negation of 'isComment'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisAnnote :: Annotation -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiisAnnote = not . isComment
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | an item wrapped in preceeding (left 'l_annos')
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- and following (right 'r_annos') annotations.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- 'opt_pos' should carry the position of an optional semicolon
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- following a formula (but is currently unused).
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Annoted a = Annoted
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , opt_pos :: Range
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , l_annos :: [Annotation]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , r_annos :: [Annotation] } deriving (Show, Eq)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskinotImplied :: Annoted a -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskinotImplied a = not $ any isImplied $ r_annos a
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | naming or labelling sentences
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata Named s = NamedSen
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski { senName :: String
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , isAxiom :: Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , isDef :: Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , sentence :: s } deriving (Eq, Ord, Show)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | equip a sentence with an empty name
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiemptyName :: s -> Named s
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski NamedSen { senName = "", sentence = x, isAxiom = True, isDef = False}
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskireName :: (String -> String) -> Named s -> Named s
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskireName f x = x { senName = f $ senName x }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | extending sentence maps to maps on labelled sentences
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapNamed :: (s -> t) -> Named s -> Named t
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapNamed f x = x { sentence = f $ sentence x }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | extending sentence maybe-maps to maps on labelled sentences
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapNamedM :: Monad m => (s -> m t) -> Named s -> m (Named t)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapNamedM f x = do
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski y <- f $ sentence x
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return x {sentence = y}
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | process all items and wrap matching annotations around the results
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapAnM :: (Monad m) => (a -> m b) -> [Annoted a] -> m [Annoted b]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do il <- mapM (f . item) al
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return $ zipWith (flip replaceAnnoted) al il
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | replace the 'item'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskireplaceAnnoted :: b -> Annoted a -> Annoted b
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskireplaceAnnoted x (Annoted _ o l r) = Annoted x o l r
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | add further following annotations
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiappendAnno :: Annoted a -> [Annotation] -> Annoted a
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiappendAnno (Annoted x p l r) y = Annoted x p l $ r ++ y
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | put together preceding annotations and an item
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiaddLeftAnno :: [Annotation] -> a -> Annoted a
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiaddLeftAnno l i = Annoted i nullRange l []
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | decorate with no annotations
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiemptyAnno :: a -> Annoted a
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiemptyAnno = addLeftAnno []
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | get the label following (or to the right of) an 'item'
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskigetRLabel :: Annoted a -> String
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskigetRLabel a = let ls = filter isLabel (r_annos a) in
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski if null ls then "" else
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let Label l _ = head ls
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in if null l then "" else head l
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- might be a multiline label
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- maybe remove white spaces