{-# 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 (Int -> OMDoc -> ShowS
[OMDoc] -> ShowS
OMDoc -> String
(Int -> OMDoc -> ShowS)
-> (OMDoc -> String) -> ([OMDoc] -> ShowS) -> Show OMDoc
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OMDoc] -> ShowS
$cshowList :: [OMDoc] -> ShowS
show :: OMDoc -> String
$cshow :: OMDoc -> String
showsPrec :: Int -> OMDoc -> ShowS
$cshowsPrec :: Int -> OMDoc -> ShowS
Show, ReadPrec [OMDoc]
ReadPrec OMDoc
Int -> ReadS OMDoc
ReadS [OMDoc]
(Int -> ReadS OMDoc)
-> ReadS [OMDoc]
-> ReadPrec OMDoc
-> ReadPrec [OMDoc]
-> Read OMDoc
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [OMDoc]
$creadListPrec :: ReadPrec [OMDoc]
readPrec :: ReadPrec OMDoc
$creadPrec :: ReadPrec OMDoc
readList :: ReadS [OMDoc]
$creadList :: ReadS [OMDoc]
readsPrec :: Int -> ReadS OMDoc
$creadsPrec :: Int -> ReadS OMDoc
Read, OMDoc -> OMDoc -> Bool
(OMDoc -> OMDoc -> Bool) -> (OMDoc -> OMDoc -> Bool) -> Eq OMDoc
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OMDoc -> OMDoc -> Bool
$c/= :: OMDoc -> OMDoc -> Bool
== :: OMDoc -> OMDoc -> Bool
$c== :: OMDoc -> OMDoc -> Bool
Eq, Eq OMDoc
Eq OMDoc =>
(OMDoc -> OMDoc -> Ordering)
-> (OMDoc -> OMDoc -> Bool)
-> (OMDoc -> OMDoc -> Bool)
-> (OMDoc -> OMDoc -> Bool)
-> (OMDoc -> OMDoc -> Bool)
-> (OMDoc -> OMDoc -> OMDoc)
-> (OMDoc -> OMDoc -> OMDoc)
-> Ord OMDoc
OMDoc -> OMDoc -> Bool
OMDoc -> OMDoc -> Ordering
OMDoc -> OMDoc -> OMDoc
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OMDoc -> OMDoc -> OMDoc
$cmin :: OMDoc -> OMDoc -> OMDoc
max :: OMDoc -> OMDoc -> OMDoc
$cmax :: OMDoc -> OMDoc -> OMDoc
>= :: OMDoc -> OMDoc -> Bool
$c>= :: OMDoc -> OMDoc -> Bool
> :: OMDoc -> OMDoc -> Bool
$c> :: OMDoc -> OMDoc -> Bool
<= :: OMDoc -> OMDoc -> Bool
$c<= :: OMDoc -> OMDoc -> Bool
< :: OMDoc -> OMDoc -> Bool
$c< :: OMDoc -> OMDoc -> Bool
compare :: OMDoc -> OMDoc -> Ordering
$ccompare :: OMDoc -> OMDoc -> Ordering
$cp1Ord :: Eq OMDoc
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 (Int -> TLElement -> ShowS
[TLElement] -> ShowS
TLElement -> String
(Int -> TLElement -> ShowS)
-> (TLElement -> String)
-> ([TLElement] -> ShowS)
-> Show TLElement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TLElement] -> ShowS
$cshowList :: [TLElement] -> ShowS
show :: TLElement -> String
$cshow :: TLElement -> String
showsPrec :: Int -> TLElement -> ShowS
$cshowsPrec :: Int -> TLElement -> ShowS
Show, ReadPrec [TLElement]
ReadPrec TLElement
Int -> ReadS TLElement
ReadS [TLElement]
(Int -> ReadS TLElement)
-> ReadS [TLElement]
-> ReadPrec TLElement
-> ReadPrec [TLElement]
-> Read TLElement
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [TLElement]
$creadListPrec :: ReadPrec [TLElement]
readPrec :: ReadPrec TLElement
$creadPrec :: ReadPrec TLElement
readList :: ReadS [TLElement]
$creadList :: ReadS [TLElement]
readsPrec :: Int -> ReadS TLElement
$creadsPrec :: Int -> ReadS TLElement
Read, TLElement -> TLElement -> Bool
(TLElement -> TLElement -> Bool)
-> (TLElement -> TLElement -> Bool) -> Eq TLElement
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TLElement -> TLElement -> Bool
$c/= :: TLElement -> TLElement -> Bool
== :: TLElement -> TLElement -> Bool
$c== :: TLElement -> TLElement -> Bool
Eq, Eq TLElement
Eq TLElement =>
(TLElement -> TLElement -> Ordering)
-> (TLElement -> TLElement -> Bool)
-> (TLElement -> TLElement -> Bool)
-> (TLElement -> TLElement -> Bool)
-> (TLElement -> TLElement -> Bool)
-> (TLElement -> TLElement -> TLElement)
-> (TLElement -> TLElement -> TLElement)
-> Ord TLElement
TLElement -> TLElement -> Bool
TLElement -> TLElement -> Ordering
TLElement -> TLElement -> TLElement
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TLElement -> TLElement -> TLElement
$cmin :: TLElement -> TLElement -> TLElement
max :: TLElement -> TLElement -> TLElement
$cmax :: TLElement -> TLElement -> TLElement
>= :: TLElement -> TLElement -> Bool
$c>= :: TLElement -> TLElement -> Bool
> :: TLElement -> TLElement -> Bool
$c> :: TLElement -> TLElement -> Bool
<= :: TLElement -> TLElement -> Bool
$c<= :: TLElement -> TLElement -> Bool
< :: TLElement -> TLElement -> Bool
$c< :: TLElement -> TLElement -> Bool
compare :: TLElement -> TLElement -> Ordering
$ccompare :: TLElement -> TLElement -> Ordering
$cp1Ord :: Eq TLElement
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 (Int -> TCElement -> ShowS
[TCElement] -> ShowS
TCElement -> String
(Int -> TCElement -> ShowS)
-> (TCElement -> String)
-> ([TCElement] -> ShowS)
-> Show TCElement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TCElement] -> ShowS
$cshowList :: [TCElement] -> ShowS
show :: TCElement -> String
$cshow :: TCElement -> String
showsPrec :: Int -> TCElement -> ShowS
$cshowsPrec :: Int -> TCElement -> ShowS
Show, ReadPrec [TCElement]
ReadPrec TCElement
Int -> ReadS TCElement
ReadS [TCElement]
(Int -> ReadS TCElement)
-> ReadS [TCElement]
-> ReadPrec TCElement
-> ReadPrec [TCElement]
-> Read TCElement
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [TCElement]
$creadListPrec :: ReadPrec [TCElement]
readPrec :: ReadPrec TCElement
$creadPrec :: ReadPrec TCElement
readList :: ReadS [TCElement]
$creadList :: ReadS [TCElement]
readsPrec :: Int -> ReadS TCElement
$creadsPrec :: Int -> ReadS TCElement
Read, TCElement -> TCElement -> Bool
(TCElement -> TCElement -> Bool)
-> (TCElement -> TCElement -> Bool) -> Eq TCElement
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TCElement -> TCElement -> Bool
$c/= :: TCElement -> TCElement -> Bool
== :: TCElement -> TCElement -> Bool
$c== :: TCElement -> TCElement -> Bool
Eq, Eq TCElement
Eq TCElement =>
(TCElement -> TCElement -> Ordering)
-> (TCElement -> TCElement -> Bool)
-> (TCElement -> TCElement -> Bool)
-> (TCElement -> TCElement -> Bool)
-> (TCElement -> TCElement -> Bool)
-> (TCElement -> TCElement -> TCElement)
-> (TCElement -> TCElement -> TCElement)
-> Ord TCElement
TCElement -> TCElement -> Bool
TCElement -> TCElement -> Ordering
TCElement -> TCElement -> TCElement
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TCElement -> TCElement -> TCElement
$cmin :: TCElement -> TCElement -> TCElement
max :: TCElement -> TCElement -> TCElement
$cmax :: TCElement -> TCElement -> TCElement
>= :: TCElement -> TCElement -> Bool
$c>= :: TCElement -> TCElement -> Bool
> :: TCElement -> TCElement -> Bool
$c> :: TCElement -> TCElement -> Bool
<= :: TCElement -> TCElement -> Bool
$c<= :: TCElement -> TCElement -> Bool
< :: TCElement -> TCElement -> Bool
$c< :: TCElement -> TCElement -> Bool
compare :: TCElement -> TCElement -> Ordering
$ccompare :: TCElement -> TCElement -> Ordering
$cp1Ord :: Eq TCElement
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 (Int -> OmdADT -> ShowS
[OmdADT] -> ShowS
OmdADT -> String
(Int -> OmdADT -> ShowS)
-> (OmdADT -> String) -> ([OmdADT] -> ShowS) -> Show OmdADT
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OmdADT] -> ShowS
$cshowList :: [OmdADT] -> ShowS
show :: OmdADT -> String
$cshow :: OmdADT -> String
showsPrec :: Int -> OmdADT -> ShowS
$cshowsPrec :: Int -> OmdADT -> ShowS
Show, ReadPrec [OmdADT]
ReadPrec OmdADT
Int -> ReadS OmdADT
ReadS [OmdADT]
(Int -> ReadS OmdADT)
-> ReadS [OmdADT]
-> ReadPrec OmdADT
-> ReadPrec [OmdADT]
-> Read OmdADT
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [OmdADT]
$creadListPrec :: ReadPrec [OmdADT]
readPrec :: ReadPrec OmdADT
$creadPrec :: ReadPrec OmdADT
readList :: ReadS [OmdADT]
$creadList :: ReadS [OmdADT]
readsPrec :: Int -> ReadS OmdADT
$creadsPrec :: Int -> ReadS OmdADT
Read, OmdADT -> OmdADT -> Bool
(OmdADT -> OmdADT -> Bool)
-> (OmdADT -> OmdADT -> Bool) -> Eq OmdADT
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OmdADT -> OmdADT -> Bool
$c/= :: OmdADT -> OmdADT -> Bool
== :: OmdADT -> OmdADT -> Bool
$c== :: OmdADT -> OmdADT -> Bool
Eq, Eq OmdADT
Eq OmdADT =>
(OmdADT -> OmdADT -> Ordering)
-> (OmdADT -> OmdADT -> Bool)
-> (OmdADT -> OmdADT -> Bool)
-> (OmdADT -> OmdADT -> Bool)
-> (OmdADT -> OmdADT -> Bool)
-> (OmdADT -> OmdADT -> OmdADT)
-> (OmdADT -> OmdADT -> OmdADT)
-> Ord OmdADT
OmdADT -> OmdADT -> Bool
OmdADT -> OmdADT -> Ordering
OmdADT -> OmdADT -> OmdADT
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OmdADT -> OmdADT -> OmdADT
$cmin :: OmdADT -> OmdADT -> OmdADT
max :: OmdADT -> OmdADT -> OmdADT
$cmax :: OmdADT -> OmdADT -> OmdADT
>= :: OmdADT -> OmdADT -> Bool
$c>= :: OmdADT -> OmdADT -> Bool
> :: OmdADT -> OmdADT -> Bool
$c> :: OmdADT -> OmdADT -> Bool
<= :: OmdADT -> OmdADT -> Bool
$c<= :: OmdADT -> OmdADT -> Bool
< :: OmdADT -> OmdADT -> Bool
$c< :: OmdADT -> OmdADT -> Bool
compare :: OmdADT -> OmdADT -> Ordering
$ccompare :: OmdADT -> OmdADT -> Ordering
$cp1Ord :: Eq OmdADT
Ord)

-- | Roles of the declared symbols can be object or type
data SymbolRole = Obj | Typ | Axiom | Theorem deriving (SymbolRole -> SymbolRole -> Bool
(SymbolRole -> SymbolRole -> Bool)
-> (SymbolRole -> SymbolRole -> Bool) -> Eq SymbolRole
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SymbolRole -> SymbolRole -> Bool
$c/= :: SymbolRole -> SymbolRole -> Bool
== :: SymbolRole -> SymbolRole -> Bool
$c== :: SymbolRole -> SymbolRole -> Bool
Eq, Eq SymbolRole
Eq SymbolRole =>
(SymbolRole -> SymbolRole -> Ordering)
-> (SymbolRole -> SymbolRole -> Bool)
-> (SymbolRole -> SymbolRole -> Bool)
-> (SymbolRole -> SymbolRole -> Bool)
-> (SymbolRole -> SymbolRole -> Bool)
-> (SymbolRole -> SymbolRole -> SymbolRole)
-> (SymbolRole -> SymbolRole -> SymbolRole)
-> Ord SymbolRole
SymbolRole -> SymbolRole -> Bool
SymbolRole -> SymbolRole -> Ordering
SymbolRole -> SymbolRole -> SymbolRole
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SymbolRole -> SymbolRole -> SymbolRole
$cmin :: SymbolRole -> SymbolRole -> SymbolRole
max :: SymbolRole -> SymbolRole -> SymbolRole
$cmax :: SymbolRole -> SymbolRole -> SymbolRole
>= :: SymbolRole -> SymbolRole -> Bool
$c>= :: SymbolRole -> SymbolRole -> Bool
> :: SymbolRole -> SymbolRole -> Bool
$c> :: SymbolRole -> SymbolRole -> Bool
<= :: SymbolRole -> SymbolRole -> Bool
$c<= :: SymbolRole -> SymbolRole -> Bool
< :: SymbolRole -> SymbolRole -> Bool
$c< :: SymbolRole -> SymbolRole -> Bool
compare :: SymbolRole -> SymbolRole -> Ordering
$ccompare :: SymbolRole -> SymbolRole -> Ordering
$cp1Ord :: Eq SymbolRole
Ord)

-- | Fixity of notation patterns
data Fixity = Infix | Prefix | Postfix deriving (Fixity -> Fixity -> Bool
(Fixity -> Fixity -> Bool)
-> (Fixity -> Fixity -> Bool) -> Eq Fixity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Fixity -> Fixity -> Bool
$c/= :: Fixity -> Fixity -> Bool
== :: Fixity -> Fixity -> Bool
$c== :: Fixity -> Fixity -> Bool
Eq, Eq Fixity
Eq Fixity =>
(Fixity -> Fixity -> Ordering)
-> (Fixity -> Fixity -> Bool)
-> (Fixity -> Fixity -> Bool)
-> (Fixity -> Fixity -> Bool)
-> (Fixity -> Fixity -> Bool)
-> (Fixity -> Fixity -> Fixity)
-> (Fixity -> Fixity -> Fixity)
-> Ord Fixity
Fixity -> Fixity -> Bool
Fixity -> Fixity -> Ordering
Fixity -> Fixity -> Fixity
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Fixity -> Fixity -> Fixity
$cmin :: Fixity -> Fixity -> Fixity
max :: Fixity -> Fixity -> Fixity
$cmax :: Fixity -> Fixity -> Fixity
>= :: Fixity -> Fixity -> Bool
$c>= :: Fixity -> Fixity -> Bool
> :: Fixity -> Fixity -> Bool
$c> :: Fixity -> Fixity -> Bool
<= :: Fixity -> Fixity -> Bool
$c<= :: Fixity -> Fixity -> Bool
< :: Fixity -> Fixity -> Bool
$c< :: Fixity -> Fixity -> Bool
compare :: Fixity -> Fixity -> Ordering
$ccompare :: Fixity -> Fixity -> Ordering
$cp1Ord :: Eq Fixity
Ord)

-- | Associativity of notation patterns
data Assoc = LeftAssoc | RightAssoc | NoneAssoc deriving (Assoc -> Assoc -> Bool
(Assoc -> Assoc -> Bool) -> (Assoc -> Assoc -> Bool) -> Eq Assoc
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Assoc -> Assoc -> Bool
$c/= :: Assoc -> Assoc -> Bool
== :: Assoc -> Assoc -> Bool
$c== :: Assoc -> Assoc -> Bool
Eq, Eq Assoc
Eq Assoc =>
(Assoc -> Assoc -> Ordering)
-> (Assoc -> Assoc -> Bool)
-> (Assoc -> Assoc -> Bool)
-> (Assoc -> Assoc -> Bool)
-> (Assoc -> Assoc -> Bool)
-> (Assoc -> Assoc -> Assoc)
-> (Assoc -> Assoc -> Assoc)
-> Ord Assoc
Assoc -> Assoc -> Bool
Assoc -> Assoc -> Ordering
Assoc -> Assoc -> Assoc
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Assoc -> Assoc -> Assoc
$cmin :: Assoc -> Assoc -> Assoc
max :: Assoc -> Assoc -> Assoc
$cmax :: Assoc -> Assoc -> Assoc
>= :: Assoc -> Assoc -> Bool
$c>= :: Assoc -> Assoc -> Bool
> :: Assoc -> Assoc -> Bool
$c> :: Assoc -> Assoc -> Bool
<= :: Assoc -> Assoc -> Bool
$c<= :: Assoc -> Assoc -> Bool
< :: Assoc -> Assoc -> Bool
$c< :: Assoc -> Assoc -> Bool
compare :: Assoc -> Assoc -> Ordering
$ccompare :: Assoc -> Assoc -> Ordering
$cp1Ord :: Eq Assoc
Ord)

-- | Type of the algebraic data type
data ADTType = Free | Generated deriving (ADTType -> ADTType -> Bool
(ADTType -> ADTType -> Bool)
-> (ADTType -> ADTType -> Bool) -> Eq ADTType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ADTType -> ADTType -> Bool
$c/= :: ADTType -> ADTType -> Bool
== :: ADTType -> ADTType -> Bool
$c== :: ADTType -> ADTType -> Bool
Eq, Eq ADTType
Eq ADTType =>
(ADTType -> ADTType -> Ordering)
-> (ADTType -> ADTType -> Bool)
-> (ADTType -> ADTType -> Bool)
-> (ADTType -> ADTType -> Bool)
-> (ADTType -> ADTType -> Bool)
-> (ADTType -> ADTType -> ADTType)
-> (ADTType -> ADTType -> ADTType)
-> Ord ADTType
ADTType -> ADTType -> Bool
ADTType -> ADTType -> Ordering
ADTType -> ADTType -> ADTType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ADTType -> ADTType -> ADTType
$cmin :: ADTType -> ADTType -> ADTType
max :: ADTType -> ADTType -> ADTType
$cmax :: ADTType -> ADTType -> ADTType
>= :: ADTType -> ADTType -> Bool
$c>= :: ADTType -> ADTType -> Bool
> :: ADTType -> ADTType -> Bool
$c> :: ADTType -> ADTType -> Bool
<= :: ADTType -> ADTType -> Bool
$c<= :: ADTType -> ADTType -> Bool
< :: ADTType -> ADTType -> Bool
$c< :: ADTType -> ADTType -> Bool
compare :: ADTType -> ADTType -> Ordering
$ccompare :: ADTType -> ADTType -> Ordering
$cp1Ord :: Eq ADTType
Ord)

-- | Totality for selectors of an adt
data Totality = Yes | No deriving (Totality -> Totality -> Bool
(Totality -> Totality -> Bool)
-> (Totality -> Totality -> Bool) -> Eq Totality
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Totality -> Totality -> Bool
$c/= :: Totality -> Totality -> Bool
== :: Totality -> Totality -> Bool
$c== :: Totality -> Totality -> Bool
Eq, Eq Totality
Eq Totality =>
(Totality -> Totality -> Ordering)
-> (Totality -> Totality -> Bool)
-> (Totality -> Totality -> Bool)
-> (Totality -> Totality -> Bool)
-> (Totality -> Totality -> Bool)
-> (Totality -> Totality -> Totality)
-> (Totality -> Totality -> Totality)
-> Ord Totality
Totality -> Totality -> Bool
Totality -> Totality -> Ordering
Totality -> Totality -> Totality
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Totality -> Totality -> Totality
$cmin :: Totality -> Totality -> Totality
max :: Totality -> Totality -> Totality
$cmax :: Totality -> Totality -> Totality
>= :: Totality -> Totality -> Bool
$c>= :: Totality -> Totality -> Bool
> :: Totality -> Totality -> Bool
$c> :: Totality -> Totality -> Bool
<= :: Totality -> Totality -> Bool
$c<= :: Totality -> Totality -> Bool
< :: Totality -> Totality -> Bool
$c< :: Totality -> Totality -> Bool
compare :: Totality -> Totality -> Ordering
$ccompare :: Totality -> Totality -> Ordering
$cp1Ord :: Eq Totality
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 (Int -> NotationComponent -> ShowS
[NotationComponent] -> ShowS
NotationComponent -> String
(Int -> NotationComponent -> ShowS)
-> (NotationComponent -> String)
-> ([NotationComponent] -> ShowS)
-> Show NotationComponent
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NotationComponent] -> ShowS
$cshowList :: [NotationComponent] -> ShowS
show :: NotationComponent -> String
$cshow :: NotationComponent -> String
showsPrec :: Int -> NotationComponent -> ShowS
$cshowsPrec :: Int -> NotationComponent -> ShowS
Show, ReadPrec [NotationComponent]
ReadPrec NotationComponent
Int -> ReadS NotationComponent
ReadS [NotationComponent]
(Int -> ReadS NotationComponent)
-> ReadS [NotationComponent]
-> ReadPrec NotationComponent
-> ReadPrec [NotationComponent]
-> Read NotationComponent
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [NotationComponent]
$creadListPrec :: ReadPrec [NotationComponent]
readPrec :: ReadPrec NotationComponent
$creadPrec :: ReadPrec NotationComponent
readList :: ReadS [NotationComponent]
$creadList :: ReadS [NotationComponent]
readsPrec :: Int -> ReadS NotationComponent
$creadsPrec :: Int -> ReadS NotationComponent
Read, NotationComponent -> NotationComponent -> Bool
(NotationComponent -> NotationComponent -> Bool)
-> (NotationComponent -> NotationComponent -> Bool)
-> Eq NotationComponent
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NotationComponent -> NotationComponent -> Bool
$c/= :: NotationComponent -> NotationComponent -> Bool
== :: NotationComponent -> NotationComponent -> Bool
$c== :: NotationComponent -> NotationComponent -> Bool
Eq, Eq NotationComponent
Eq NotationComponent =>
(NotationComponent -> NotationComponent -> Ordering)
-> (NotationComponent -> NotationComponent -> Bool)
-> (NotationComponent -> NotationComponent -> Bool)
-> (NotationComponent -> NotationComponent -> Bool)
-> (NotationComponent -> NotationComponent -> Bool)
-> (NotationComponent -> NotationComponent -> NotationComponent)
-> (NotationComponent -> NotationComponent -> NotationComponent)
-> Ord NotationComponent
NotationComponent -> NotationComponent -> Bool
NotationComponent -> NotationComponent -> Ordering
NotationComponent -> NotationComponent -> NotationComponent
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: NotationComponent -> NotationComponent -> NotationComponent
$cmin :: NotationComponent -> NotationComponent -> NotationComponent
max :: NotationComponent -> NotationComponent -> NotationComponent
$cmax :: NotationComponent -> NotationComponent -> NotationComponent
>= :: NotationComponent -> NotationComponent -> Bool
$c>= :: NotationComponent -> NotationComponent -> Bool
> :: NotationComponent -> NotationComponent -> Bool
$c> :: NotationComponent -> NotationComponent -> Bool
<= :: NotationComponent -> NotationComponent -> Bool
$c<= :: NotationComponent -> NotationComponent -> Bool
< :: NotationComponent -> NotationComponent -> Bool
$c< :: NotationComponent -> NotationComponent -> Bool
compare :: NotationComponent -> NotationComponent -> Ordering
$ccompare :: NotationComponent -> NotationComponent -> Ordering
$cp1Ord :: Eq NotationComponent
Ord)


instance Show SymbolRole where
    show :: SymbolRole -> String
show Obj = "object"
    show Typ = "type"
    show Axiom = "axiom"
    show Theorem = "theorem"

instance Show ADTType where
    show :: ADTType -> String
show Free = "free"
    show Generated = "generated"

instance Show Totality where
    show :: Totality -> String
show Yes = "yes"
    show No = "no"

instance Show Fixity where
    show :: Fixity -> String
show Infix = "in"
    show Prefix = "pre"
    show Postfix = "post"

instance Show Assoc where
    show :: Assoc -> String
show LeftAssoc = "left"
    show RightAssoc = "right"
    show NoneAssoc = "none"

instance Read SymbolRole where
    readsPrec :: Int -> ReadS SymbolRole
readsPrec _ = [SymbolRole] -> ReadS SymbolRole
forall a. Show a => [a] -> ReadS a
readShow [SymbolRole
Obj, SymbolRole
Typ, SymbolRole
Axiom, SymbolRole
Theorem]

instance Read ADTType where
    readsPrec :: Int -> ReadS ADTType
readsPrec _ = [ADTType] -> ReadS ADTType
forall a. Show a => [a] -> ReadS a
readShow [ADTType
Free, ADTType
Generated]

instance Read Totality where
    readsPrec :: Int -> ReadS Totality
readsPrec _ = [Totality] -> ReadS Totality
forall a. Show a => [a] -> ReadS a
readShow [Totality
Yes, Totality
No]

instance Read Fixity where
    readsPrec :: Int -> ReadS Fixity
readsPrec _ = [Fixity] -> ReadS Fixity
forall a. Show a => [a] -> ReadS a
readShow [Fixity
Infix, Fixity
Prefix, Fixity
Postfix]

instance Read Assoc where
    readsPrec :: Int -> ReadS Assoc
readsPrec _ = [Assoc] -> ReadS Assoc
forall a. Show a => [a] -> ReadS a
readShow [Assoc
LeftAssoc, Assoc
RightAssoc, Assoc
NoneAssoc]

-- | Names used for OpenMath variables and symbols
data OMName = OMName { OMName -> String
name :: String, OMName -> [String]
path :: [String] }
              deriving (Int -> OMName -> ShowS
[OMName] -> ShowS
OMName -> String
(Int -> OMName -> ShowS)
-> (OMName -> String) -> ([OMName] -> ShowS) -> Show OMName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OMName] -> ShowS
$cshowList :: [OMName] -> ShowS
show :: OMName -> String
$cshow :: OMName -> String
showsPrec :: Int -> OMName -> ShowS
$cshowsPrec :: Int -> OMName -> ShowS
Show, ReadPrec [OMName]
ReadPrec OMName
Int -> ReadS OMName
ReadS [OMName]
(Int -> ReadS OMName)
-> ReadS [OMName]
-> ReadPrec OMName
-> ReadPrec [OMName]
-> Read OMName
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [OMName]
$creadListPrec :: ReadPrec [OMName]
readPrec :: ReadPrec OMName
$creadPrec :: ReadPrec OMName
readList :: ReadS [OMName]
$creadList :: ReadS [OMName]
readsPrec :: Int -> ReadS OMName
$creadsPrec :: Int -> ReadS OMName
Read, OMName -> OMName -> Bool
(OMName -> OMName -> Bool)
-> (OMName -> OMName -> Bool) -> Eq OMName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OMName -> OMName -> Bool
$c/= :: OMName -> OMName -> Bool
== :: OMName -> OMName -> Bool
$c== :: OMName -> OMName -> Bool
Eq, Eq OMName
Eq OMName =>
(OMName -> OMName -> Ordering)
-> (OMName -> OMName -> Bool)
-> (OMName -> OMName -> Bool)
-> (OMName -> OMName -> Bool)
-> (OMName -> OMName -> Bool)
-> (OMName -> OMName -> OMName)
-> (OMName -> OMName -> OMName)
-> Ord OMName
OMName -> OMName -> Bool
OMName -> OMName -> Ordering
OMName -> OMName -> OMName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OMName -> OMName -> OMName
$cmin :: OMName -> OMName -> OMName
max :: OMName -> OMName -> OMName
$cmax :: OMName -> OMName -> OMName
>= :: OMName -> OMName -> Bool
$c>= :: OMName -> OMName -> Bool
> :: OMName -> OMName -> Bool
$c> :: OMName -> OMName -> Bool
<= :: OMName -> OMName -> Bool
$c<= :: OMName -> OMName -> Bool
< :: OMName -> OMName -> Bool
$c< :: OMName -> OMName -> Bool
compare :: OMName -> OMName -> Ordering
$ccompare :: OMName -> OMName -> Ordering
$cp1Ord :: Eq OMName
Ord, Typeable)

{- | Attribute-name/attribute-value pair used to represent the type
of a type-annotated term -}
data OMAttribute = OMAttr OMElement OMElement
                      deriving (Int -> OMAttribute -> ShowS
[OMAttribute] -> ShowS
OMAttribute -> String
(Int -> OMAttribute -> ShowS)
-> (OMAttribute -> String)
-> ([OMAttribute] -> ShowS)
-> Show OMAttribute
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OMAttribute] -> ShowS
$cshowList :: [OMAttribute] -> ShowS
show :: OMAttribute -> String
$cshow :: OMAttribute -> String
showsPrec :: Int -> OMAttribute -> ShowS
$cshowsPrec :: Int -> OMAttribute -> ShowS
Show, ReadPrec [OMAttribute]
ReadPrec OMAttribute
Int -> ReadS OMAttribute
ReadS [OMAttribute]
(Int -> ReadS OMAttribute)
-> ReadS [OMAttribute]
-> ReadPrec OMAttribute
-> ReadPrec [OMAttribute]
-> Read OMAttribute
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [OMAttribute]
$creadListPrec :: ReadPrec [OMAttribute]
readPrec :: ReadPrec OMAttribute
$creadPrec :: ReadPrec OMAttribute
readList :: ReadS [OMAttribute]
$creadList :: ReadS [OMAttribute]
readsPrec :: Int -> ReadS OMAttribute
$creadsPrec :: Int -> ReadS OMAttribute
Read, OMAttribute -> OMAttribute -> Bool
(OMAttribute -> OMAttribute -> Bool)
-> (OMAttribute -> OMAttribute -> Bool) -> Eq OMAttribute
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OMAttribute -> OMAttribute -> Bool
$c/= :: OMAttribute -> OMAttribute -> Bool
== :: OMAttribute -> OMAttribute -> Bool
$c== :: OMAttribute -> OMAttribute -> Bool
Eq, Eq OMAttribute
Eq OMAttribute =>
(OMAttribute -> OMAttribute -> Ordering)
-> (OMAttribute -> OMAttribute -> Bool)
-> (OMAttribute -> OMAttribute -> Bool)
-> (OMAttribute -> OMAttribute -> Bool)
-> (OMAttribute -> OMAttribute -> Bool)
-> (OMAttribute -> OMAttribute -> OMAttribute)
-> (OMAttribute -> OMAttribute -> OMAttribute)
-> Ord OMAttribute
OMAttribute -> OMAttribute -> Bool
OMAttribute -> OMAttribute -> Ordering
OMAttribute -> OMAttribute -> OMAttribute
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OMAttribute -> OMAttribute -> OMAttribute
$cmin :: OMAttribute -> OMAttribute -> OMAttribute
max :: OMAttribute -> OMAttribute -> OMAttribute
$cmax :: OMAttribute -> OMAttribute -> OMAttribute
>= :: OMAttribute -> OMAttribute -> Bool
$c>= :: OMAttribute -> OMAttribute -> Bool
> :: OMAttribute -> OMAttribute -> Bool
$c> :: OMAttribute -> OMAttribute -> Bool
<= :: OMAttribute -> OMAttribute -> Bool
$c<= :: OMAttribute -> OMAttribute -> Bool
< :: OMAttribute -> OMAttribute -> Bool
$c< :: OMAttribute -> OMAttribute -> Bool
compare :: OMAttribute -> OMAttribute -> Ordering
$ccompare :: OMAttribute -> OMAttribute -> Ordering
$cp1Ord :: Eq OMAttribute
Ord)

{- | CD contains the reference to the content dictionary
and eventually the cdbase entry -}
data OMCD = CD [String] deriving (Int -> OMCD -> ShowS
[OMCD] -> ShowS
OMCD -> String
(Int -> OMCD -> ShowS)
-> (OMCD -> String) -> ([OMCD] -> ShowS) -> Show OMCD
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OMCD] -> ShowS
$cshowList :: [OMCD] -> ShowS
show :: OMCD -> String
$cshow :: OMCD -> String
showsPrec :: Int -> OMCD -> ShowS
$cshowsPrec :: Int -> OMCD -> ShowS
Show, ReadPrec [OMCD]
ReadPrec OMCD
Int -> ReadS OMCD
ReadS [OMCD]
(Int -> ReadS OMCD)
-> ReadS [OMCD] -> ReadPrec OMCD -> ReadPrec [OMCD] -> Read OMCD
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [OMCD]
$creadListPrec :: ReadPrec [OMCD]
readPrec :: ReadPrec OMCD
$creadPrec :: ReadPrec OMCD
readList :: ReadS [OMCD]
$creadList :: ReadS [OMCD]
readsPrec :: Int -> ReadS OMCD
$creadsPrec :: Int -> ReadS OMCD
Read, OMCD -> OMCD -> Bool
(OMCD -> OMCD -> Bool) -> (OMCD -> OMCD -> Bool) -> Eq OMCD
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OMCD -> OMCD -> Bool
$c/= :: OMCD -> OMCD -> Bool
== :: OMCD -> OMCD -> Bool
$c== :: OMCD -> OMCD -> Bool
Eq, Eq OMCD
Eq OMCD =>
(OMCD -> OMCD -> Ordering)
-> (OMCD -> OMCD -> Bool)
-> (OMCD -> OMCD -> Bool)
-> (OMCD -> OMCD -> Bool)
-> (OMCD -> OMCD -> Bool)
-> (OMCD -> OMCD -> OMCD)
-> (OMCD -> OMCD -> OMCD)
-> Ord OMCD
OMCD -> OMCD -> Bool
OMCD -> OMCD -> Ordering
OMCD -> OMCD -> OMCD
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OMCD -> OMCD -> OMCD
$cmin :: OMCD -> OMCD -> OMCD
max :: OMCD -> OMCD -> OMCD
$cmax :: OMCD -> OMCD -> OMCD
>= :: OMCD -> OMCD -> Bool
$c>= :: OMCD -> OMCD -> Bool
> :: OMCD -> OMCD -> Bool
$c> :: OMCD -> OMCD -> Bool
<= :: OMCD -> OMCD -> Bool
$c<= :: OMCD -> OMCD -> Bool
< :: OMCD -> OMCD -> Bool
$c< :: OMCD -> OMCD -> Bool
compare :: OMCD -> OMCD -> Ordering
$ccompare :: OMCD -> OMCD -> Ordering
$cp1Ord :: Eq OMCD
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 (Int -> OMElement -> ShowS
[OMElement] -> ShowS
OMElement -> String
(Int -> OMElement -> ShowS)
-> (OMElement -> String)
-> ([OMElement] -> ShowS)
-> Show OMElement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OMElement] -> ShowS
$cshowList :: [OMElement] -> ShowS
show :: OMElement -> String
$cshow :: OMElement -> String
showsPrec :: Int -> OMElement -> ShowS
$cshowsPrec :: Int -> OMElement -> ShowS
Show, ReadPrec [OMElement]
ReadPrec OMElement
Int -> ReadS OMElement
ReadS [OMElement]
(Int -> ReadS OMElement)
-> ReadS [OMElement]
-> ReadPrec OMElement
-> ReadPrec [OMElement]
-> Read OMElement
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [OMElement]
$creadListPrec :: ReadPrec [OMElement]
readPrec :: ReadPrec OMElement
$creadPrec :: ReadPrec OMElement
readList :: ReadS [OMElement]
$creadList :: ReadS [OMElement]
readsPrec :: Int -> ReadS OMElement
$creadsPrec :: Int -> ReadS OMElement
Read, OMElement -> OMElement -> Bool
(OMElement -> OMElement -> Bool)
-> (OMElement -> OMElement -> Bool) -> Eq OMElement
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OMElement -> OMElement -> Bool
$c/= :: OMElement -> OMElement -> Bool
== :: OMElement -> OMElement -> Bool
$c== :: OMElement -> OMElement -> Bool
Eq, Eq OMElement
Eq OMElement =>
(OMElement -> OMElement -> Ordering)
-> (OMElement -> OMElement -> Bool)
-> (OMElement -> OMElement -> Bool)
-> (OMElement -> OMElement -> Bool)
-> (OMElement -> OMElement -> Bool)
-> (OMElement -> OMElement -> OMElement)
-> (OMElement -> OMElement -> OMElement)
-> Ord OMElement
OMElement -> OMElement -> Bool
OMElement -> OMElement -> Ordering
OMElement -> OMElement -> OMElement
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OMElement -> OMElement -> OMElement
$cmin :: OMElement -> OMElement -> OMElement
max :: OMElement -> OMElement -> OMElement
$cmax :: OMElement -> OMElement -> OMElement
>= :: OMElement -> OMElement -> Bool
$c>= :: OMElement -> OMElement -> Bool
> :: OMElement -> OMElement -> Bool
$c> :: OMElement -> OMElement -> Bool
<= :: OMElement -> OMElement -> Bool
$c<= :: OMElement -> OMElement -> Bool
< :: OMElement -> OMElement -> Bool
$c< :: OMElement -> OMElement -> Bool
compare :: OMElement -> OMElement -> Ordering
$ccompare :: OMElement -> OMElement -> Ordering
$cp1Ord :: Eq OMElement
Ord)


-- * Hets Utils

nameToId :: String -> Id
nameToId :: String -> Id
nameToId = CharParser () Id -> String -> Id
forall a. CharParser () a -> String -> a
parseString CharParser () Id
forall st. GenParser Char st Id
parseAnnoId

nameToToken :: String -> Token
nameToToken :: String -> Token
nameToToken = String -> Token
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 { SigMapI a -> Map OMName a
sigMapISymbs :: Map.Map OMName a
                         , SigMapI a -> Map OMName String
sigMapINotations :: Map.Map OMName String }

sigMapSymbs :: SigMap a -> NameMap a
sigMapSymbs :: SigMap a -> NameMap a
sigMapSymbs (SigMap sm :: NameMap a
sm _) = NameMap a
sm

cdFromList :: [String] -> OMCD
cdFromList :: [String] -> OMCD
cdFromList ["", ""] = [String] -> OMCD
CD []
cdFromList ["", cd :: String
cd] = [String] -> OMCD
CD [String
cd]
cdFromList [base :: String
base, cd :: String
cd] = [String] -> OMCD
CD [String
cd, String
base]
cdFromList _ = String -> OMCD
forall a. HasCallStack => String -> a
error "cdFromList: Malformed list. I need exactly 2 elements!"

cdIsEmpty :: OMCD -> Bool
cdIsEmpty :: OMCD -> Bool
cdIsEmpty cd :: OMCD
cd = ["", ""] [String] -> [String] -> Bool
forall a. Eq a => a -> a -> Bool
== OMCD -> [String]
cdToList OMCD
cd

-- | The result list has always two elements: [base, modul]
cdToList :: OMCD -> [String]
cdToList :: OMCD -> [String]
cdToList (CD [cd :: String
cd, base :: String
base]) = [String
base, String
cd]
cdToList (CD [cd :: String
cd]) = ["", String
cd]
cdToList _ = ["", ""]

cdToMaybeList :: OMCD -> [Maybe String]
cdToMaybeList :: OMCD -> [Maybe String]
cdToMaybeList (CD [cd :: String
cd, base :: String
base]) = [String -> Maybe String
forall a. a -> Maybe a
Just String
base, String -> Maybe String
forall a. a -> Maybe a
Just String
cd]
cdToMaybeList (CD [cd :: String
cd]) = [Maybe String
forall a. Maybe a
Nothing, String -> Maybe String
forall a. a -> Maybe a
Just String
cd]
cdToMaybeList _ = [Maybe String
forall a. Maybe a
Nothing, Maybe String
forall a. Maybe a
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 :: 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 :: String -> [String] -> String
nameEncode s :: String
s l :: [String]
l = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
uniqPrefix, String
s, ":", String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
uniqPrefix [String]
l]

{- | This invariant should hold:
@(x, l) = fromJust $ nameDecode $ nameEncode x l@ -}
nameDecode :: String -> Maybe (String, [String])
nameDecode :: String -> Maybe (String, [String])
nameDecode s :: String
s =
    case String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
uniqPrefix String
s of
      Nothing -> Maybe (String, [String])
forall a. Maybe a
Nothing
      Just s' :: String
s' ->
          let (kind :: String
kind, r :: String
r) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ':') String
s'
          in if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
r
             then String -> Maybe (String, [String])
forall a. HasCallStack => String -> a
error (String -> Maybe (String, [String]))
-> String -> Maybe (String, [String])
forall a b. (a -> b) -> a -> b
$ "nameDecode: missing colon in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
             else (String, [String]) -> Maybe (String, [String])
forall a. a -> Maybe a
Just (String
kind, String -> String -> [String]
forall a. Eq a => [a] -> [a] -> [[a]]
splitByList String
uniqPrefix (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. [a] -> [a]
tail String
r)

nameToString :: UniqName -> String
nameToString :: UniqName -> String
nameToString (s :: String
s, i :: Int
i) =
    let s' :: String
s' = (Char -> Bool) -> ShowS
encodeBut (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` "/?%#") String
s
    in if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then String -> [String] -> String
nameEncode ("over_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) [String
s'] else String
s'

-- * Constructing/Extracting Values

{- | name of the theory constitutive element, error if not TCSymbol, TCNotation,
or TCImport -}
tcName :: TCElement -> OMName
tcName :: TCElement -> OMName
tcName tc :: TCElement
tc = case TCElement
tc of
              TCSymbol s :: String
s _ _ _ -> String -> OMName
mkSimpleName String
s
              TCNotation qn :: OMQualName
qn _ _ -> OMQualName -> OMName
unqualName OMQualName
qn
              TCImport s :: String
s _ _ -> String -> OMName
mkSimpleName String
s
              _ -> String -> OMName
forall a. HasCallStack => String -> a
error "tcName: No name for this value."

unqualName :: OMQualName -> OMName
unqualName :: OMQualName -> OMName
unqualName = OMQualName -> OMName
forall a b. (a, b) -> b
snd


emptyCD :: OMCD
emptyCD :: OMCD
emptyCD = [String] -> OMCD
CD []

omName :: UniqName -> OMName
omName :: UniqName -> OMName
omName = String -> OMName
mkSimpleName (String -> OMName) -> (UniqName -> String) -> UniqName -> OMName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqName -> String
nameToString

mkSimpleName :: String -> OMName
mkSimpleName :: String -> OMName
mkSimpleName s :: String
s = String -> [String] -> OMName
OMName String
s []

mkSimpleQualName :: UniqName -> OMQualName
mkSimpleQualName :: UniqName -> OMQualName
mkSimpleQualName un :: UniqName
un = ([String] -> OMCD
CD [], UniqName -> OMName
omName UniqName
un)

simpleOMS :: UniqName -> OMElement
simpleOMS :: UniqName -> OMElement
simpleOMS = OMQualName -> OMElement
OMS (OMQualName -> OMElement)
-> (UniqName -> OMQualName) -> UniqName -> OMElement
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqName -> OMQualName
mkSimpleQualName

-- * Lookup utils for Import and Export

lookupNotation :: SigMapI a -> OMName -> String
lookupNotation :: SigMapI a -> OMName -> String
lookupNotation smi :: SigMapI a
smi = Map OMName String -> OMName -> String
lookupNotationInMap (Map OMName String -> OMName -> String)
-> Map OMName String -> OMName -> String
forall a b. (a -> b) -> a -> b
$ SigMapI a -> Map OMName String
forall a. SigMapI a -> Map OMName String
sigMapINotations SigMapI a
smi

lookupNotationInMap :: Map.Map OMName String -> OMName -> String
lookupNotationInMap :: Map OMName String -> OMName -> String
lookupNotationInMap m :: Map OMName String
m n :: OMName
n = String -> OMName -> Map OMName String -> String
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (OMName -> String
name OMName
n) OMName
n Map OMName String
m

-- * Pretty instances

instance Pretty OMName where
    pretty :: OMName -> Doc
pretty = String -> Doc
text (String -> Doc) -> (OMName -> String) -> OMName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OMName -> String
forall a. Show a => a -> String
show