hets/OMDoc/DataTypes.hs

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