b897c52f865b2fc4e220e2110b874e59c716456bBob Halley{- |

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyModule : $Header$

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyDescription : datastructures for annotations of (Het)CASL.

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyCopyright : (c) Klaus L�ttich, Christian Maeder, and Uni Bremen 2002-2006

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyMaintainer : Christian.Maeder@dfki.de

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyStability : provisional

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyPortability : portable

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob HalleyDatastructures for annotations of (Het)CASL.

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley There is also a paramterized data type for an 'Annoted' 'item'.

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley See also chapter II.5 of the CASL Reference Manual.

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley-}

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halleymodule Common.AS_Annotation where

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleyimport Common.Id

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- DrIFT command

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley{-! global: UpPos !-}

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- | start of an annote with its WORD or a comment

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleydata Annote_word = Annote_word String | Comment_start deriving (Show, Eq, Ord)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- | line or group for 'Unparsed_anno'

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleydata Annote_text = Line_anno String | Group_anno [String]

efd6c944a4ebd3fb65dc39f9172d322198b2b1d3Bob Halley deriving (Show, Eq, Ord)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- | formats to be displayed (may be extended in the future).

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- Drop 3 from the show result to get the string for parsing and printing

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleydata Display_format = DF_HTML | DF_LATEX | DF_RTF deriving (Show, Eq, Ord)

5fbced719b71e659322b4ce3e4a39c9b039674c7Bob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- | swap the entries of a lookup table

efd6c944a4ebd3fb65dc39f9172d322198b2b1d3Bob HalleyswapTable :: [(a, b)] -> [(b, a)]

e6d6ce00e2bf0f6a755f8229212e35706e4035aeMichael GraffswapTable = map $ \ (a, b) -> (b, a)

e6d6ce00e2bf0f6a755f8229212e35706e4035aeMichael Graff

e6d6ce00e2bf0f6a755f8229212e35706e4035aeMichael Graff-- | drop the first 3 characters from the show result

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleytoTable :: (Show a) => [a] -> [(a, String)]

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleytoTable = map $ \a -> (a, drop 3 $ show a)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley-- | a lookup table for the textual representation of display formats

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halleydisplay_format_table :: [(Display_format, String)]

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halleydisplay_format_table = toTable [ DF_HTML, DF_LATEX, DF_RTF ]

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley-- | lookup the textual representation of a display format

efd6c944a4ebd3fb65dc39f9172d322198b2b1d3Bob Halley-- in 'display_format_table'

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleylookupDisplayFormat :: Display_format -> String

178f6ad061e54bc5babfca3577f72058fa0797c1Bob HalleylookupDisplayFormat df =

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley maybe (error "lookupDisplayFormat: unknown display format")

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley id $ lookup df display_format_table

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley-- | precedence 'Lower' means less and 'BothDirections' means less and greater.

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley-- 'Higher' means greater but this is syntactically not allowed in 'Prec_anno'.

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley-- 'NoDirection' can also not be specified explicitly,

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- but covers those ids that are not mentionend in precedences.

efd6c944a4ebd3fb65dc39f9172d322198b2b1d3Bob Halleydata PrecRel = Higher | Lower | BothDirections | NoDirection

efd6c944a4ebd3fb65dc39f9172d322198b2b1d3Bob Halley deriving (Show, Eq, Ord)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- | either left or right associative

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleydata AssocEither = ALeft | ARight deriving (Show, Eq, Ord)

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- | semantic (line) annotations without further information.

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- Use the same drop-3-trick as for the 'Display_format'.

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleydata Semantic_anno = SA_cons | SA_def | SA_implies | SA_mono | SA_implied

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley deriving (Show, Eq, Ord)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- | a lookup table for the textual representation of semantic annos

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleysemantic_anno_table :: [(Semantic_anno, String)]

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleysemantic_anno_table = toTable [SA_cons, SA_def,

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley SA_implies, SA_mono, SA_implied]

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- | lookup the textual representation of a semantic anno

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- in 'semantic_anno_table'

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleylookupSemanticAnno :: Semantic_anno -> String

178f6ad061e54bc5babfca3577f72058fa0797c1Bob HalleylookupSemanticAnno sa =

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley maybe (error "lookupSemanticAnno: no semantic anno")

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley id $ lookup sa semantic_anno_table

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley-- | all possible annotations (without comment-outs)

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halleydata Annotation = -- | constructor for comments or unparsed annotes

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley Unparsed_anno Annote_word Annote_text Range

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- | known annotes

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley | Display_anno Id [(Display_format, String)] Range

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- position of anno start, keywords and anno end

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley | List_anno Id Id Id Range

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- position of anno start, commas and anno end

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley | Number_anno Id Range

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- position of anno start, commas and anno end

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley | Float_anno Id Id Range

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- position of anno start, commas and anno end

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley | String_anno Id Id Range

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- position of anno start, commas and anno end

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley | Prec_anno PrecRel [Id] [Id] Range

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- ^ positions: "{",commas,"}", RecRel, "{",commas,"}"

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley -- | Lower = "< " BothDirections = "<>"

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley | Assoc_anno AssocEither [Id] Range -- position of commas

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley | Label [String] Range

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley -- position of anno start and anno end

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley -- All annotations below are only as annote line allowed

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley | Semantic_anno Semantic_anno Range

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley -- position information for annotations is provided

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley -- by every annotation

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley deriving (Show, Eq, Ord)

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley-- |

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley-- 'isLabel' tests if the given 'Annotation' is a label

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob Halley-- (a 'Label' typically follows a formula)

19ba7857f6bf38619eda1f1dae0eb05a6cdd2b77Bob HalleyisLabel :: Annotation -> Bool

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleyisLabel a = case a of

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley Label _ _ -> True

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley _ -> False

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

178f6ad061e54bc5babfca3577f72058fa0797c1Bob HalleyisImplies :: Annotation -> Bool

178f6ad061e54bc5babfca3577f72058fa0797c1Bob HalleyisImplies a = case a of

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley Semantic_anno SA_implies _ -> True

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley _ -> False

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleyisImplied :: Annotation -> Bool

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleyisImplied a = case a of

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley Semantic_anno SA_implied _ -> True

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley _ -> False

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- |

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- 'isSemanticAnno' tests if the given 'Annotation' is a semantic one

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleyisSemanticAnno :: Annotation -> Bool

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleyisSemanticAnno a = case a of

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley Semantic_anno _ _ -> True

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley _ -> False

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- |

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- 'isComment' tests if the given 'Annotation' is a comment line or a

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- comment group

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleyisComment :: Annotation -> Bool

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleyisComment c = case c of

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley Unparsed_anno Comment_start _ _ -> True

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley _ -> False

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley-- |

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- 'isAnnote' is the negation of 'isComment'

178f6ad061e54bc5babfca3577f72058fa0797c1Bob HalleyisAnnote :: Annotation -> Bool

178f6ad061e54bc5babfca3577f72058fa0797c1Bob HalleyisAnnote = not . isComment

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley-- | an item wrapped in preceeding (left 'l_annos')

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley-- and following (right 'r_annos') annotations.

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley-- 'opt_pos' should carry the position of an optional semicolon

178f6ad061e54bc5babfca3577f72058fa0797c1Bob Halley-- following a formula (but is currently unused).

b897c52f865b2fc4e220e2110b874e59c716456bBob Halleydata Annoted a = Annoted

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley { item :: a

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley , opt_pos :: Range

59a6d9cbcdbec6960d47e5871fb7e7c0253e1fb2Mark Andrews , l_annos :: [Annotation]

59a6d9cbcdbec6960d47e5871fb7e7c0253e1fb2Mark Andrews , r_annos :: [Annotation] } deriving (Show, Eq)

b897c52f865b2fc4e220e2110b874e59c716456bBob Halley

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleynotImplied :: Annoted a -> Bool

b897c52f865b2fc4e220e2110b874e59c716456bBob HalleynotImplied a = not $ any isImplied $ r_annos a

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

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

-- | equip a sentence with an empty name

type Named s = SenAttr s String

senName :: Named s -> String

senName = senAttr

makeNamed :: String -> s -> Named s

makeNamed str x = SenAttr

{ senAttr = str

, isAxiom = True

, isDef = False

, wasTheorem = False

, sentence = x }

reName :: (String -> String) -> Named s -> Named s

reName f x = x { senAttr = f $ senName 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

-- | replace the 'item'

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

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

-- | add further following annotations

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

appendAnno (Annoted x p l r) y = Annoted x p l $ r ++ y

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

_ -> ""