AS_Annotation.der.hs revision bccea164bdfc2ddc3d1e20749bb5477a46eab3a6
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettDescription : datastructures for annotations of (Het)CASL.
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettCopyright : (c) Klaus Luettich, Christian Maeder, and Uni Bremen 2002-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettMaintainer : Christian.Maeder@dfki.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettDatastructures for annotations of (Het)CASL.
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett There is also a paramterized data type for an 'Annoted' 'item'.
78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maeder See also chapter II.5 of the CASL Reference Manual.
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett-- DrIFT command
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett{-! global: GetRange !-}
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett-- | start of an annote with its WORD or a comment
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettdata Annote_word = Annote_word String | Comment_start deriving (Show, Eq, Ord)
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett-- | line or group for 'Unparsed_anno'
ae930b77ed60580110b52a09456d651f9b841883Andy Gimblettdata Annote_text = Line_anno String | Group_anno [String]
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett deriving (Show, Eq, Ord)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- | formats to be displayed (may be extended in the future).
ae930b77ed60580110b52a09456d651f9b841883Andy Gimblett-- Drop 3 from the show result to get the string for parsing and printing
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblettdata Display_format = DF_HTML | DF_LATEX | DF_RTF deriving (Show, Eq, Ord)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- | swap the entries of a lookup table
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaederswapTable :: [(a, b)] -> [(b, a)]
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettswapTable = map $ \ (a, b) -> (b, a)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-- | drop the first 3 characters from the show result
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian MaedertoTable :: (Show a) => [a] -> [(a, String)]
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy GimbletttoTable = map $ \a -> (a, drop 3 $ show a)
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett-- | a lookup table for the textual representation of display formats
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettdisplay_format_table :: [(Display_format, String)]
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblettdisplay_format_table = toTable [ DF_HTML, DF_LATEX, DF_RTF ]
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett-- | lookup the textual representation of a display format
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett-- in 'display_format_table'
a65b135c4ed7e68b2510bc218018ffa8f9a34fe8Liam O'ReillylookupDisplayFormat :: Display_format -> String
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian MaederlookupDisplayFormat df =
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder maybe (error "lookupDisplayFormat: unknown display format")
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder id $ lookup df display_format_table
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder-- | precedence 'Lower' means less and 'BothDirections' means less and greater.
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder-- 'Higher' means greater but this is syntactically not allowed in 'Prec_anno'.
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder-- 'NoDirection' can also not be specified explicitly,
a65b135c4ed7e68b2510bc218018ffa8f9a34fe8Liam O'Reilly-- but covers those ids that are not mentionend in precedences.
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettdata PrecRel = Higher | Lower | BothDirections | NoDirection
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett deriving (Show, Eq, Ord)
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett-- | either left or right associative
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblettdata AssocEither = ALeft | ARight deriving (Show, Eq, Ord)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | semantic (line) annotations without further information.
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- Use the same drop-3-trick as for the 'Display_format'.
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettdata Semantic_anno = SA_cons | SA_def | SA_implies | SA_mono | SA_implied
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett deriving (Show, Eq, Ord)
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett-- | a lookup table for the textual representation of semantic annos
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettsemantic_anno_table :: [(Semantic_anno, String)]
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettsemantic_anno_table =
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett toTable [SA_cons, SA_def, SA_implies, SA_mono, SA_implied]
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | lookup the textual representation of a semantic anno
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett-- in 'semantic_anno_table'
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettlookupSemanticAnno :: Semantic_anno -> String
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettlookupSemanticAnno sa =
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett maybe (error "lookupSemanticAnno: no semantic anno")
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett id $ lookup sa semantic_anno_table
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett-- | all possible annotations (without comment-outs)
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettdata Annotation = -- | constructor for comments or unparsed annotes
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett Unparsed_anno Annote_word Annote_text Range
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -- | known annotes
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett | Display_anno Id [(Display_format, String)] Range
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -- position of anno start, keywords and anno end
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett | List_anno Id Id Id Range
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett -- position of anno start, commas and anno end
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett | Number_anno Id Range
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett -- position of anno start, commas and anno end
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett | Float_anno Id Id Range
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -- position of anno start, commas and anno end
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett | String_anno Id Id Range
820947bd01ca952c3909eaa0366c6914c87cc1cbTill Mossakowski -- position of anno start, commas and anno end
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett | Prec_anno PrecRel [Id] [Id] Range
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -- ^ positions: "{",commas,"}", RecRel, "{",commas,"}"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -- | Lower = "< " BothDirections = "<>"
fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett | Assoc_anno AssocEither [Id] Range -- position of commas
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett | Label [String] Range
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett -- position of anno start and anno end
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett -- All annotations below are only as annote line allowed
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett | Semantic_anno Semantic_anno Range
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett -- position information for annotations is provided
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett -- by every annotation
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett deriving (Show, Eq, Ord)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- 'isLabel' tests if the given 'Annotation' is a label
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- (a 'Label' typically follows a formula)
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisLabel :: Annotation -> Bool
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisLabel a = case a of
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Label _ _ -> True
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisImplies :: Annotation -> Bool
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisImplies a = case a of
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Semantic_anno SA_implies _ -> True
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachisImplied :: Annotation -> Bool
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettisImplied a = case a of
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett Semantic_anno SA_implied _ -> True
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- 'isSemanticAnno' tests if the given 'Annotation' is a semantic one
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisSemanticAnno :: Annotation -> Bool
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettisSemanticAnno a = case a of
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Semantic_anno _ _ -> True
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett-- 'isComment' tests if the given 'Annotation' is a comment line or a
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- comment group
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettisComment :: Annotation -> Bool
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisComment c = case c of
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett Unparsed_anno Comment_start _ _ -> True
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- 'isAnnote' is the negation of 'isComment'
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettisAnnote :: Annotation -> Bool
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettisAnnote = not . isComment
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett-- | an item wrapped in preceeding (left 'l_annos')
9582375827616730f146b77f9d5a4fd0cc78bc47Andy Gimblett-- and following (right 'r_annos') annotations.
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- 'opt_pos' should carry the position of an optional semicolon
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- following a formula (but is currently unused).
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettdata Annoted a = Annoted
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , opt_pos :: Range
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , l_annos :: [Annotation]
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett , r_annos :: [Annotation] } deriving (Show, Ord, Eq)
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettnotImplied :: Annoted a -> Bool
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettnotImplied = not . any isImplied . r_annos
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett-- | naming or labelling sentences
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettdata SenAttr s a = SenAttr
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett { senAttr :: a
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett , isAxiom :: Bool
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett , isDef :: Bool
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett , wasTheorem :: Bool
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett{- will be set to True when status of isAxiom changes from False to True -}
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett , simpAnno :: Maybe Bool -- for %simp or %nosimp annotations
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett , sentence :: s } deriving (Eq, Ord, Show)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- | equip a sentence with a name
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy GimblettmakeNamed :: a -> s -> SenAttr s a
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy GimblettmakeNamed a s = SenAttr
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett { senAttr = a
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett , isAxiom = True
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett , isDef = False
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett , wasTheorem = False
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett , simpAnno = Nothing
7caf9f99d426a25d56eb7473fea1f55ce4460762Andy Gimblett , sentence = s }
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimbletttype Named s = SenAttr s String
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettreName :: (String -> String) -> Named s -> Named s
e95030058b77cb83593c85aa4c506caf154f63b7Andy GimblettreName f x = x { senAttr = f $ senAttr x }
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett-- | extending sentence maps to maps on labelled sentences
e95030058b77cb83593c85aa4c506caf154f63b7Andy GimblettmapNamed :: (s -> t) -> SenAttr s a -> SenAttr t a
e95030058b77cb83593c85aa4c506caf154f63b7Andy GimblettmapNamed f x = x { sentence = f $ sentence x }
f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett-- | extending sentence maybe-maps to maps on labelled sentences
e95030058b77cb83593c85aa4c506caf154f63b7Andy GimblettmapNamedM :: Monad m => (s -> m t) -> Named s -> m (Named t)
bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettmapNamedM f x = do
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett y <- f $ sentence x
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett return x {sentence = y}
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett-- | process all items and wrap matching annotations around the results
e95030058b77cb83593c85aa4c506caf154f63b7Andy GimblettmapAnM :: (Monad m) => (a -> m b) -> [Annoted a] -> m [Annoted b]
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett do il <- mapM (f . item) al
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett return $ zipWith (flip replaceAnnoted) al il
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- | replace the 'item'
e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettreplaceAnnoted :: b -> Annoted a -> Annoted b
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettreplaceAnnoted x (Annoted _ o l r) = Annoted x o l r
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- | add further following annotations
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettappendAnno :: Annoted a -> [Annotation] -> Annoted a
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettappendAnno (Annoted x p l r) y = Annoted x p l $ r ++ y
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- | put together preceding annotations and an item
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettaddLeftAnno :: [Annotation] -> a -> Annoted a
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettaddLeftAnno l i = Annoted i nullRange l []
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- | decorate with no annotations
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettemptyAnno :: a -> Annoted a
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettemptyAnno = addLeftAnno []
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- | get the label following (or to the right of) an 'item'
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettgetRLabel :: Annoted a -> String
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett case filter isLabel (r_annos a) of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Label l _ : _ -> unwords $ concatMap words l
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- | check for an annotation starting with % and the input str
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- (does not work for known annotation words)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettidentAnno :: String -> Annotation -> Bool
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettidentAnno str an = case an of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett Unparsed_anno (Annote_word wrd) _ _ -> wrd == str
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett-- | test all anntotions for an item
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimbletthasIdentAnno :: String -> Annoted a -> Bool
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimbletthasIdentAnno str a = any (identAnno str) $ l_annos a ++ r_annos a
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettmakeNamedSen :: Annoted a -> Named a
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettmakeNamedSen a = (makeNamed (getRLabel a) $ item a)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett { isAxiom = notImplied a
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett , simpAnno = case (hasIdentAnno "simp" a, hasIdentAnno "nosimp" a) of
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett (True, False) -> Just True
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett (False, True) -> Just False
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett _ -> Nothing }