449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings{- |

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterModule : $Header$

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterDescription : datastructures for annotations of (Het)CASL.

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterCopyright : (c) Klaus Luettich, Christian Maeder, and Uni Bremen 2002-2006

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterLicense : GPLv2 or higher, see LICENSE.txt

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterMaintainer : Christian.Maeder@dfki.de

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterStability : provisional

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterPortability : portable

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterDatastructures for annotations of (Het)CASL.

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster There is also a paramterized data type for an 'Annoted' 'item'.

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster See also chapter II.5 of the CASL Reference Manual.

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-}

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fostermodule Common.AS_Annotation where

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport Common.Id

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport Common.IRI (IRI)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport Data.Maybe

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterimport qualified Data.Map as Map

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- DrIFT command

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster{-! global: GetRange !-}

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- | start of an annote with its WORD or a comment

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbingsdata Annote_word = Annote_word String | Comment_start deriving (Show, Eq, Ord)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- | line or group for 'Unparsed_anno'

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterdata Annote_text = Line_anno String | Group_anno [String]

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings deriving (Show, Eq, Ord)

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster{- | formats to be displayed (may be extended in the future).

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterDrop 3 from the show result to get the string for parsing and printing -}

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterdata Display_format = DF_HTML | DF_LATEX | DF_RTF deriving (Show, Eq, Ord)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- | swap the entries of a lookup table

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterswapTable :: [(a, b)] -> [(b, a)]

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterswapTable = map $ \ (a, b) -> (b, a)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- | drop the first 3 characters from the show result

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostertoTable :: (Show a) => [a] -> [(a, String)]

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FostertoTable = map $ \ a -> (a, drop 3 $ show a)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- | a lookup table for the textual representation of display formats

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterdisplay_format_table :: [(Display_format, String)]

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterdisplay_format_table = toTable [ DF_HTML, DF_LATEX, DF_RTF ]

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster{- | lookup the textual representation of a display format

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterin 'display_format_table' -}

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterlookupDisplayFormat :: Display_format -> String

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterlookupDisplayFormat df =

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster fromMaybe (error "lookupDisplayFormat: unknown display format")

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster $ lookup df display_format_table

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster{- | precedence 'Lower' means less and 'BothDirections' means less and greater.

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings'Higher' means greater but this is syntactically not allowed in 'Prec_anno'.

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster'NoDirection' can also not be specified explicitly,

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterbut covers those ids that are not mentionend in precedences. -}

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterdata PrecRel = Higher | Lower | BothDirections | NoDirection

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster deriving (Show, Eq, Ord)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- | either left or right associative

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterdata AssocEither = ALeft | ARight deriving (Show, Eq, Ord)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster{- | semantic (line) annotations without further information.

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterUse the same drop-3-trick as for the 'Display_format'. -}

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterdata Semantic_anno = SA_cons | SA_def | SA_implies | SA_mono | SA_implied

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | SA_mcons | SA_ccons

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster deriving (Show, Eq, Ord)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- | a lookup table for the textual representation of semantic annos

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fostersemantic_anno_table :: [(Semantic_anno, String)]

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fostersemantic_anno_table =

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster toTable [SA_cons, SA_def, SA_implies, SA_mono, SA_implied, SA_mcons, SA_ccons]

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster{- | lookup the textual representation of a semantic anno

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterin 'semantic_anno_table' -}

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterlookupSemanticAnno :: Semantic_anno -> String

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterlookupSemanticAnno sa =

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster fromMaybe (error "lookupSemanticAnno: no semantic anno")

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster $ lookup sa semantic_anno_table

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster-- | all possible annotations (without comment-outs)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Fosterdata Annotation = -- | constructor for comments or unparsed annotes

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Unparsed_anno Annote_word Annote_text Range

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- | known annotes

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | Display_anno Id [(Display_format, String)] Range

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- position of anno start, keywords and anno end

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | List_anno Id Id Id Range

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- position of anno start, commas and anno end

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | Number_anno Id Range

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- position of anno start, commas and anno end

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | Float_anno Id Id Range

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- position of anno start, commas and anno end

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | String_anno Id Id Range

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- position of anno start, commas and anno end

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | Prec_anno PrecRel [Id] [Id] Range

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster {- positions: "{",commas,"}", RecRel, "{",commas,"}"

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Lower = "< " BothDirections = "<>" -}

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | Assoc_anno AssocEither [Id] Range -- position of commas

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | Label [String] Range

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- position of anno start and anno end

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | Prefix_anno [(String, IRI)] Range

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- position of anno start and anno end

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster -- All annotations below are only as annote line allowed

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster | Semantic_anno Semantic_anno Range

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster {- position information for annotations is provided

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster by every annotation -}

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster deriving (Show, Eq, Ord)

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster{- | 'isLabel' tests if the given 'Annotation' is a label

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster(a 'Label' typically follows a formula) -}

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterisLabel :: Annotation -> Bool

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterisLabel a = case a of

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster Label _ _ -> True

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster _ -> False

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan Foster

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken StubbingsisImplies :: Annotation -> Bool

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken StubbingsisImplies a = case a of

449854c2a07b50ea64d9d6a8b03d18d4afeeee43Ken Stubbings Semantic_anno SA_implies _ -> True

5bdd6bf9211505ff52afc7e32bdc49cdfacf4879Charles Sparey _ -> False

5bdd6bf9211505ff52afc7e32bdc49cdfacf4879Charles Sparey

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterisImplied :: Annotation -> Bool

a688bcbb4bcff5398fdd29b86f83450257dc0df4Allan FosterisImplied a = case a of

Semantic_anno SA_implied _ -> True

_ -> False

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

isSemanticAnno :: Annotation -> Bool

isSemanticAnno a = case a of

Semantic_anno _ _ -> True

_ -> False

{- | 'isComment' tests if the given 'Annotation' is a comment line or a

comment group -}

isComment :: Annotation -> Bool

isComment c = case c of

Unparsed_anno Comment_start _ _ -> True

_ -> False

-- | 'isAnnote' is the negation of 'isComment'

isAnnote :: Annotation -> Bool

isAnnote = not . isComment

-- | separate prefix annotations and put them into a map

partPrefixes :: [Annotation] -> (Map.Map String IRI, [Annotation])

partPrefixes = foldr (\ a (m, l) -> case a of

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

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

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

and following (right 'r_annos') annotations.

'opt_pos' should carry the position of an optional semicolon

following a formula (but is currently unused). -}

data Annoted a = Annoted

{ item :: a

, opt_pos :: Range

, l_annos :: [Annotation]

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

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)

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

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