{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module : ./OMDoc/DataTypes.hs
Description : The OMDoc Data Types
Copyright : (c) Ewaryst Schulz, DFKI 2008
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Ewaryst.Schulz@dfki.de
Stability : provisional
Portability : portable
Datatypes for an intermediate OMDoc representation.
-}
module OMDoc.DataTypes where
import Common.Utils
import Common.Doc
import Common.DocUtils
import Common.Amalgamate (readShow)
import Common.Id
import Common.Lexer
import Common.AnnoParser
import Common.Percent (encodeBut)
import Data.List
import Data.Typeable
import qualified Data.Map as Map
{-
OMDoc represented in 3 layers:
1. toplevel (theory, view)
2. theory constitutive (axiom, symbol)
3. subelements (insort, ...) and OpenMath
-}
-- -------------------- Datatypes for Representation ----------------------
-- | OMDoc root element with libname and a list of toplevel elements
data OMDoc = OMDoc String [TLElement] deriving (Show, Read, Eq, Ord)
{- | Toplevel elements for OMDoc, theory with name, meta and content,
view with from, to and morphism -}
data TLElement = TLTheory String (Maybe OMCD) [TCElement]
| TLView String OMCD OMCD TCMorphism
deriving (Show, Read, Eq, Ord)
{-
NOTATIONS
OMDoc currently supports two kinds of notations: smart and flexible.
a) The smart ones look like this:
<notation for="??+" role="application" fixity="f" precedence="p" implicit="i"/>
Here f \in {in, pre, post}, p is an integer (higher precedence =
higher binding), and i is the number of implicit arguments (0 by
default).
In this case, you would additionally give
<notation for="??+" role="constant"><text value="+"/></notation>
This notation is called to render operation itself, i.e.,
produces the operator symbol.
b) The flexible ones look like this
<notation for="??something" role="application" precedence="P">
<component index="1" precedence="p1"/>
<text value="["/>
<component index="2" precedence="p2"/>
<text value="/"/>
<component index="3" precedence="p3"/>
<text value="]"/>
</notation>
Here <component index="i"/> recurses into argument number i.
P is the output precedence, p1,p2,p3 are the input precedences.
You can also use <component index="0"/>. That renders the operator
symbol by calling the notation
<notation for="??+" role="constant">...</notation>
2) The smart ones have two major advantages:
- They can be read back easily.
- They are independent of the output format.
In 1b) above, we would need one notation for Hets-syntax, one for MathML etc
-}
-- | Theory constitutive elements for OMDoc
data TCElement =
-- | Symbol to represent sorts, constants, predicate symbols, etc.
TCSymbol String OMElement SymbolRole (Maybe OMElement)
-- | A notation for the given symbol with an optional style
| TCNotation OMQualName String (Maybe String)
{- | A smart notation for the given symbol with fixity, associativity,
precedence and the number of implicit arguments -}
| TCSmartNotation OMQualName Fixity Assoc Int Int
{- | A smart notation for the given symbol, the argument- and
text-components have to alternate in the component list -}
| TCFlexibleNotation OMQualName Int [NotationComponent]
-- | Algebraic Data Type represents free/generated types
| TCADT [OmdADT]
-- | Import statements for referencing other theories
| TCImport String OMCD TCMorphism
-- | A comment, only for development purposes
| TCComment String
deriving (Show, Read, Eq, Ord)
-- | return type for sentence translation (ADT or formula)
type TCorOMElement = Either TCElement OMElement
-- | Morphisms to specify signature mappings
type TCMorphism = [(OMName, OMImage)]
{- | The target type of a mapping is just an alias or an assignment to
a symbol -}
type OMImage = Either String OMElement
-- | The flattened structure of an Algebraic Data Type
data OmdADT =
-- | A single sort given by name, type and a list of constructors
ADTSortDef String ADTType [OmdADT]
-- | A constructor given by its name and a list of arguments
| ADTConstr String [OmdADT]
-- | An argument with type and evtually a selector
| ADTArg OMElement (Maybe OmdADT)
-- | The selector has a name and is total (Yes) or partial (No)
| ADTSelector String Totality
-- | Insort elements point to other sortdefs and inherit their structure
| ADTInsort OMQualName
deriving (Show, Read, Eq, Ord)
-- | Roles of the declared symbols can be object or type
data SymbolRole = Obj | Typ | Axiom | Theorem deriving (Eq, Ord)
-- | Fixity of notation patterns
data Fixity = Infix | Prefix | Postfix deriving (Eq, Ord)
-- | Associativity of notation patterns
data Assoc = LeftAssoc | RightAssoc | NoneAssoc deriving (Eq, Ord)
-- | Type of the algebraic data type
data ADTType = Free | Generated deriving (Eq, Ord)
-- | Totality for selectors of an adt
data Totality = Yes | No deriving (Eq, Ord)
{- | A component can be a text-component, e.g., <text value="["/>, or an
argument-component such as <component index="1" precedence="p1"/> -}
data NotationComponent = TextComp String | ArgComp Int Int
deriving (Show, Read, Eq, Ord)
instance Show SymbolRole where
show Obj = "object"
show Typ = "type"
show Axiom = "axiom"
show Theorem = "theorem"
instance Show ADTType where
show Free = "free"
show Generated = "generated"
instance Show Totality where
show Yes = "yes"
show No = "no"
instance Show Fixity where
show Infix = "in"
show Prefix = "pre"
show Postfix = "post"
instance Show Assoc where
show LeftAssoc = "left"
show RightAssoc = "right"
show NoneAssoc = "none"
instance Read SymbolRole where
readsPrec _ = readShow [Obj, Typ, Axiom, Theorem]
instance Read ADTType where
readsPrec _ = readShow [Free, Generated]
instance Read Totality where
readsPrec _ = readShow [Yes, No]
instance Read Fixity where
readsPrec _ = readShow [Infix, Prefix, Postfix]
instance Read Assoc where
readsPrec _ = readShow [LeftAssoc, RightAssoc, NoneAssoc]
-- | Names used for OpenMath variables and symbols
data OMName = OMName { name :: String, path :: [String] }
deriving (Show, Read, Eq, Ord, Typeable)
{- | Attribute-name/attribute-value pair used to represent the type
of a type-annotated term -}
data OMAttribute = OMAttr OMElement OMElement
deriving (Show, Read, Eq, Ord)
{- | CD contains the reference to the content dictionary
and eventually the cdbase entry -}
data OMCD = CD [String] deriving (Show, Read, Eq, Ord)
type OMQualName = (OMCD, OMName)
-- | Elements for Open Math
data OMElement =
-- | Symbol
OMS OMQualName
-- | Simple variable
| OMV OMName
-- | Attributed element needed for type annotations of elements
| OMATTT OMElement OMAttribute
{- | Application to a list of arguments,
first argument is usually the functionhead -}
| OMA [OMElement]
-- | Bindersymbol, bound vars, body
| OMBIND OMElement [OMElement] OMElement
deriving (Show, Read, Eq, Ord)
-- * Hets Utils
nameToId :: String -> Id
nameToId = parseString parseAnnoId
nameToToken :: String -> Token
nameToToken = mkSimpleId
-- * Utils for Translation
type UniqName = (String, Int)
type NameMap a = Map.Map a UniqName
-- | Mapping of symbols and sentence names to unique ids (used in export)
data SigMap a = SigMap (NameMap a) (NameMap String)
{- | Mapping of OMDoc names to hets strings, for signature creation,
and strings to symbols, for lookup in terms (used in import) -}
data SigMapI a = SigMapI { sigMapISymbs :: Map.Map OMName a
, sigMapINotations :: Map.Map OMName String }
sigMapSymbs :: SigMap a -> NameMap a
sigMapSymbs (SigMap sm _) = sm
cdFromList :: [String] -> OMCD
cdFromList ["", ""] = CD []
cdFromList ["", cd] = CD [cd]
cdFromList [base, cd] = CD [cd, base]
cdFromList _ = error "cdFromList: Malformed list. I need exactly 2 elements!"
cdIsEmpty :: OMCD -> Bool
cdIsEmpty cd = ["", ""] == cdToList cd
-- | The result list has always two elements: [base, modul]
cdToList :: OMCD -> [String]
cdToList (CD [cd, base]) = [base, cd]
cdToList (CD [cd]) = ["", cd]
cdToList _ = ["", ""]
cdToMaybeList :: OMCD -> [Maybe String]
cdToMaybeList (CD [cd, base]) = [Just base, Just cd]
cdToMaybeList (CD [cd]) = [Nothing, Just cd]
cdToMaybeList _ = [Nothing, Nothing]
-- * Name handling: encoding, decoding, unique names
{- | The closing paren + percent can be used neither in ordinary Hets-names
nor in sentence names hence it is used here for encodings. -}
uniqPrefix :: String
uniqPrefix = "%()%"
{- | Special name encoding in order to be able to recognize these names
while reading. -}
nameEncode :: String -- ^ the kind of the encoding, may not contain colons
-> [String] -- ^ the values to encode
-> String
nameEncode s l = concat [uniqPrefix, s, ":", intercalate uniqPrefix l]
{- | This invariant should hold:
@(x, l) = fromJust $ nameDecode $ nameEncode x l@ -}
nameDecode :: String -> Maybe (String, [String])
nameDecode s =
case stripPrefix uniqPrefix s of
Nothing -> Nothing
Just s' ->
let (kind, r) = break (== ':') s'
in if null r
then error $ "nameDecode: missing colon in " ++ s
else Just (kind, splitByList uniqPrefix $ tail r)
nameToString :: UniqName -> String
nameToString (s, i) =
let s' = encodeBut (`notElem` "/?%#") s
in if i > 0 then nameEncode ("over_" ++ show i) [s'] else s'
-- * Constructing/Extracting Values
{- | name of the theory constitutive element, error if not TCSymbol, TCNotation,
or TCImport -}
tcName :: TCElement -> OMName
tcName tc = case tc of
TCSymbol s _ _ _ -> mkSimpleName s
TCNotation qn _ _ -> unqualName qn
TCImport s _ _ -> mkSimpleName s
_ -> error "tcName: No name for this value."
unqualName :: OMQualName -> OMName
unqualName = snd
emptyCD :: OMCD
emptyCD = CD []
omName :: UniqName -> OMName
omName = mkSimpleName . nameToString
mkSimpleName :: String -> OMName
mkSimpleName s = OMName s []
mkSimpleQualName :: UniqName -> OMQualName
mkSimpleQualName un = (CD [], omName un)
simpleOMS :: UniqName -> OMElement
simpleOMS = OMS . mkSimpleQualName
-- * Lookup utils for Import and Export
lookupNotation :: SigMapI a -> OMName -> String
lookupNotation smi = lookupNotationInMap $ sigMapINotations smi
lookupNotationInMap :: Map.Map OMName String -> OMName -> String
lookupNotationInMap m n = Map.findWithDefault (name n) n m
-- * Pretty instances
instance Pretty OMName where
pretty = text . show