Hets - the Heterogeneous Tool Set

Copyright(c) Ewaryst Schulz DFKI 2008
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerEwaryst.Schulz@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

OMDoc.DataTypes

Contents

Description

Datatypes for an intermediate OMDoc representation.

Synopsis

Documentation

data OMDoc Source #

OMDoc root element with libname and a list of toplevel elements

Constructors

OMDoc String [TLElement] 

Instances

Eq OMDoc Source # 

Methods

(==) :: OMDoc -> OMDoc -> Bool

(/=) :: OMDoc -> OMDoc -> Bool

Ord OMDoc Source # 

Methods

compare :: OMDoc -> OMDoc -> Ordering

(<) :: OMDoc -> OMDoc -> Bool

(<=) :: OMDoc -> OMDoc -> Bool

(>) :: OMDoc -> OMDoc -> Bool

(>=) :: OMDoc -> OMDoc -> Bool

max :: OMDoc -> OMDoc -> OMDoc

min :: OMDoc -> OMDoc -> OMDoc

Read OMDoc Source # 

Methods

readsPrec :: Int -> ReadS OMDoc

readList :: ReadS [OMDoc]

readPrec :: ReadPrec OMDoc

readListPrec :: ReadPrec [OMDoc]

Show OMDoc Source # 

Methods

showsPrec :: Int -> OMDoc -> ShowS

show :: OMDoc -> String

showList :: [OMDoc] -> ShowS

XmlRepresentable OMDoc Source #

The root instance for representing OMDoc in XML

Methods

toXml :: OMDoc -> Content Source #

fromXml :: Element -> Result (Maybe OMDoc) Source #

data TLElement Source #

Toplevel elements for OMDoc, theory with name, meta and content, view with from, to and morphism

Constructors

TLTheory String (Maybe OMCD) [TCElement] 
TLView String OMCD OMCD TCMorphism 

Instances

Eq TLElement Source # 

Methods

(==) :: TLElement -> TLElement -> Bool

(/=) :: TLElement -> TLElement -> Bool

Ord TLElement Source # 

Methods

compare :: TLElement -> TLElement -> Ordering

(<) :: TLElement -> TLElement -> Bool

(<=) :: TLElement -> TLElement -> Bool

(>) :: TLElement -> TLElement -> Bool

(>=) :: TLElement -> TLElement -> Bool

max :: TLElement -> TLElement -> TLElement

min :: TLElement -> TLElement -> TLElement

Read TLElement Source # 

Methods

readsPrec :: Int -> ReadS TLElement

readList :: ReadS [TLElement]

readPrec :: ReadPrec TLElement

readListPrec :: ReadPrec [TLElement]

Show TLElement Source # 

Methods

showsPrec :: Int -> TLElement -> ShowS

show :: TLElement -> String

showList :: [TLElement] -> ShowS

XmlRepresentable TLElement Source #

toplevel OMDoc elements to XML and back

Methods

toXml :: TLElement -> Content Source #

fromXml :: Element -> Result (Maybe TLElement) Source #

data TCElement Source #

Theory constitutive elements for OMDoc

Constructors

TCSymbol String OMElement SymbolRole (Maybe OMElement)

Symbol to represent sorts, constants, predicate symbols, etc.

TCNotation OMQualName String (Maybe String)

A notation for the given symbol with an optional style

TCSmartNotation OMQualName Fixity Assoc Int Int

A smart notation for the given symbol with fixity, associativity, precedence and the number of implicit arguments

TCFlexibleNotation OMQualName Int [NotationComponent]

A smart notation for the given symbol, the argument- and text-components have to alternate in the component list

TCADT [OmdADT]

Algebraic Data Type represents free/generated types

TCImport String OMCD TCMorphism

Import statements for referencing other theories

TCComment String

A comment, only for development purposes

Instances

Eq TCElement Source # 

Methods

(==) :: TCElement -> TCElement -> Bool

(/=) :: TCElement -> TCElement -> Bool

Ord TCElement Source # 

Methods

compare :: TCElement -> TCElement -> Ordering

(<) :: TCElement -> TCElement -> Bool

(<=) :: TCElement -> TCElement -> Bool

(>) :: TCElement -> TCElement -> Bool

(>=) :: TCElement -> TCElement -> Bool

max :: TCElement -> TCElement -> TCElement

min :: TCElement -> TCElement -> TCElement

Read TCElement Source # 

Methods

readsPrec :: Int -> ReadS TCElement

readList :: ReadS [TCElement]

readPrec :: ReadPrec TCElement

readListPrec :: ReadPrec [TCElement]

Show TCElement Source # 

Methods

showsPrec :: Int -> TCElement -> ShowS

show :: TCElement -> String

showList :: [TCElement] -> ShowS

XmlRepresentable TCElement Source #

theory constitutive OMDoc elements to XML and back

Methods

toXml :: TCElement -> Content Source #

fromXml :: Element -> Result (Maybe TCElement) Source #

type TCorOMElement = Either TCElement OMElement Source #

return type for sentence translation (ADT or formula)

type TCMorphism = [(OMName, OMImage)] Source #

Morphisms to specify signature mappings

type OMImage = Either String OMElement Source #

The target type of a mapping is just an alias or an assignment to a symbol

data OmdADT Source #

The flattened structure of an Algebraic Data Type

Constructors

ADTSortDef String ADTType [OmdADT]

A single sort given by name, type and a list of constructors

ADTConstr String [OmdADT]

A constructor given by its name and a list of arguments

ADTArg OMElement (Maybe OmdADT)

An argument with type and evtually a selector

ADTSelector String Totality

The selector has a name and is total (Yes) or partial (No)

ADTInsort OMQualName

Insort elements point to other sortdefs and inherit their structure

Instances

Eq OmdADT Source # 

Methods

(==) :: OmdADT -> OmdADT -> Bool

(/=) :: OmdADT -> OmdADT -> Bool

Ord OmdADT Source # 

Methods

compare :: OmdADT -> OmdADT -> Ordering

(<) :: OmdADT -> OmdADT -> Bool

(<=) :: OmdADT -> OmdADT -> Bool

(>) :: OmdADT -> OmdADT -> Bool

(>=) :: OmdADT -> OmdADT -> Bool

max :: OmdADT -> OmdADT -> OmdADT

min :: OmdADT -> OmdADT -> OmdADT

Read OmdADT Source # 

Methods

readsPrec :: Int -> ReadS OmdADT

readList :: ReadS [OmdADT]

readPrec :: ReadPrec OmdADT

readListPrec :: ReadPrec [OmdADT]

Show OmdADT Source # 

Methods

showsPrec :: Int -> OmdADT -> ShowS

show :: OmdADT -> String

showList :: [OmdADT] -> ShowS

XmlRepresentable OmdADT Source #

OMDoc - Algebraic Data Types

Methods

toXml :: OmdADT -> Content Source #

fromXml :: Element -> Result (Maybe OmdADT) Source #

data SymbolRole Source #

Roles of the declared symbols can be object or type

Constructors

Obj 
Typ 
Axiom 
Theorem 

Instances

Eq SymbolRole Source # 

Methods

(==) :: SymbolRole -> SymbolRole -> Bool

(/=) :: SymbolRole -> SymbolRole -> Bool

Ord SymbolRole Source # 
Read SymbolRole Source # 

Methods

readsPrec :: Int -> ReadS SymbolRole

readList :: ReadS [SymbolRole]

readPrec :: ReadPrec SymbolRole

readListPrec :: ReadPrec [SymbolRole]

Show SymbolRole Source # 

Methods

showsPrec :: Int -> SymbolRole -> ShowS

show :: SymbolRole -> String

showList :: [SymbolRole] -> ShowS

data Fixity Source #

Fixity of notation patterns

Constructors

Infix 
Prefix 
Postfix 

Instances

Eq Fixity Source # 

Methods

(==) :: Fixity -> Fixity -> Bool

(/=) :: Fixity -> Fixity -> Bool

Ord Fixity Source # 

Methods

compare :: Fixity -> Fixity -> Ordering

(<) :: Fixity -> Fixity -> Bool

(<=) :: Fixity -> Fixity -> Bool

(>) :: Fixity -> Fixity -> Bool

(>=) :: Fixity -> Fixity -> Bool

max :: Fixity -> Fixity -> Fixity

min :: Fixity -> Fixity -> Fixity

Read Fixity Source # 

Methods

readsPrec :: Int -> ReadS Fixity

readList :: ReadS [Fixity]

readPrec :: ReadPrec Fixity

readListPrec :: ReadPrec [Fixity]

Show Fixity Source # 

Methods

showsPrec :: Int -> Fixity -> ShowS

show :: Fixity -> String

showList :: [Fixity] -> ShowS

data Assoc Source #

Associativity of notation patterns

Instances

Eq Assoc Source # 

Methods

(==) :: Assoc -> Assoc -> Bool

(/=) :: Assoc -> Assoc -> Bool

Ord Assoc Source # 

Methods

compare :: Assoc -> Assoc -> Ordering

(<) :: Assoc -> Assoc -> Bool

(<=) :: Assoc -> Assoc -> Bool

(>) :: Assoc -> Assoc -> Bool

(>=) :: Assoc -> Assoc -> Bool

max :: Assoc -> Assoc -> Assoc

min :: Assoc -> Assoc -> Assoc

Read Assoc Source # 

Methods

readsPrec :: Int -> ReadS Assoc

readList :: ReadS [Assoc]

readPrec :: ReadPrec Assoc

readListPrec :: ReadPrec [Assoc]

Show Assoc Source # 

Methods

showsPrec :: Int -> Assoc -> ShowS

show :: Assoc -> String

showList :: [Assoc] -> ShowS

data ADTType Source #

Type of the algebraic data type

Constructors

Free 
Generated 

Instances

Eq ADTType Source # 

Methods

(==) :: ADTType -> ADTType -> Bool

(/=) :: ADTType -> ADTType -> Bool

Ord ADTType Source # 

Methods

compare :: ADTType -> ADTType -> Ordering

(<) :: ADTType -> ADTType -> Bool

(<=) :: ADTType -> ADTType -> Bool

(>) :: ADTType -> ADTType -> Bool

(>=) :: ADTType -> ADTType -> Bool

max :: ADTType -> ADTType -> ADTType

min :: ADTType -> ADTType -> ADTType

Read ADTType Source # 

Methods

readsPrec :: Int -> ReadS ADTType

readList :: ReadS [ADTType]

readPrec :: ReadPrec ADTType

readListPrec :: ReadPrec [ADTType]

Show ADTType Source # 

Methods

showsPrec :: Int -> ADTType -> ShowS

show :: ADTType -> String

showList :: [ADTType] -> ShowS

data Totality Source #

Totality for selectors of an adt

Constructors

Yes 
No 

Instances

Eq Totality Source # 

Methods

(==) :: Totality -> Totality -> Bool

(/=) :: Totality -> Totality -> Bool

Ord Totality Source # 

Methods

compare :: Totality -> Totality -> Ordering

(<) :: Totality -> Totality -> Bool

(<=) :: Totality -> Totality -> Bool

(>) :: Totality -> Totality -> Bool

(>=) :: Totality -> Totality -> Bool

max :: Totality -> Totality -> Totality

min :: Totality -> Totality -> Totality

Read Totality Source # 

Methods

readsPrec :: Int -> ReadS Totality

readList :: ReadS [Totality]

readPrec :: ReadPrec Totality

readListPrec :: ReadPrec [Totality]

Show Totality Source # 

Methods

showsPrec :: Int -> Totality -> ShowS

show :: Totality -> String

showList :: [Totality] -> ShowS

data OMName Source #

Names used for OpenMath variables and symbols

Constructors

OMName 

Fields

Instances

Eq OMName Source # 

Methods

(==) :: OMName -> OMName -> Bool

(/=) :: OMName -> OMName -> Bool

Ord OMName Source # 

Methods

compare :: OMName -> OMName -> Ordering

(<) :: OMName -> OMName -> Bool

(<=) :: OMName -> OMName -> Bool

(>) :: OMName -> OMName -> Bool

(>=) :: OMName -> OMName -> Bool

max :: OMName -> OMName -> OMName

min :: OMName -> OMName -> OMName

Read OMName Source # 

Methods

readsPrec :: Int -> ReadS OMName

readList :: ReadS [OMName]

readPrec :: ReadPrec OMName

readListPrec :: ReadPrec [OMName]

Show OMName Source # 

Methods

showsPrec :: Int -> OMName -> ShowS

show :: OMName -> String

showList :: [OMName] -> ShowS

Pretty OMName Source # 

data OMAttribute Source #

Attribute-name/attribute-value pair used to represent the type of a type-annotated term

Constructors

OMAttr OMElement OMElement 

Instances

Eq OMAttribute Source # 

Methods

(==) :: OMAttribute -> OMAttribute -> Bool

(/=) :: OMAttribute -> OMAttribute -> Bool

Ord OMAttribute Source # 
Read OMAttribute Source # 

Methods

readsPrec :: Int -> ReadS OMAttribute

readList :: ReadS [OMAttribute]

readPrec :: ReadPrec OMAttribute

readListPrec :: ReadPrec [OMAttribute]

Show OMAttribute Source # 

Methods

showsPrec :: Int -> OMAttribute -> ShowS

show :: OMAttribute -> String

showList :: [OMAttribute] -> ShowS

XmlRepresentable OMAttribute Source #

Helper instance for OpenMath attributes

Methods

toXml :: OMAttribute -> Content Source #

fromXml :: Element -> Result (Maybe OMAttribute) Source #

data OMCD Source #

CD contains the reference to the content dictionary and eventually the cdbase entry

Constructors

CD [String] 

Instances

Eq OMCD Source # 

Methods

(==) :: OMCD -> OMCD -> Bool

(/=) :: OMCD -> OMCD -> Bool

Ord OMCD Source # 

Methods

compare :: OMCD -> OMCD -> Ordering

(<) :: OMCD -> OMCD -> Bool

(<=) :: OMCD -> OMCD -> Bool

(>) :: OMCD -> OMCD -> Bool

(>=) :: OMCD -> OMCD -> Bool

max :: OMCD -> OMCD -> OMCD

min :: OMCD -> OMCD -> OMCD

Read OMCD Source # 

Methods

readsPrec :: Int -> ReadS OMCD

readList :: ReadS [OMCD]

readPrec :: ReadPrec OMCD

readListPrec :: ReadPrec [OMCD]

Show OMCD Source # 

Methods

showsPrec :: Int -> OMCD -> ShowS

show :: OMCD -> String

showList :: [OMCD] -> ShowS

data OMElement Source #

Elements for Open Math

Constructors

OMS OMQualName

Symbol

OMV OMName

Simple variable

OMATTT OMElement OMAttribute

Attributed element needed for type annotations of elements

OMA [OMElement]

Application to a list of arguments, first argument is usually the functionhead

OMBIND OMElement [OMElement] OMElement

Bindersymbol, bound vars, body

Instances

Eq OMElement Source # 

Methods

(==) :: OMElement -> OMElement -> Bool

(/=) :: OMElement -> OMElement -> Bool

Ord OMElement Source # 

Methods

compare :: OMElement -> OMElement -> Ordering

(<) :: OMElement -> OMElement -> Bool

(<=) :: OMElement -> OMElement -> Bool

(>) :: OMElement -> OMElement -> Bool

(>=) :: OMElement -> OMElement -> Bool

max :: OMElement -> OMElement -> OMElement

min :: OMElement -> OMElement -> OMElement

Read OMElement Source # 

Methods

readsPrec :: Int -> ReadS OMElement

readList :: ReadS [OMElement]

readPrec :: ReadPrec OMElement

readListPrec :: ReadPrec [OMElement]

Show OMElement Source # 

Methods

showsPrec :: Int -> OMElement -> ShowS

show :: OMElement -> String

showList :: [OMElement] -> ShowS

XmlRepresentable OMElement Source #

OpenMath elements to XML and back

Methods

toXml :: OMElement -> Content Source #

fromXml :: Element -> Result (Maybe OMElement) Source #

Hets Utils

nameToId :: String -> Id Source #

nameToToken :: String -> Token Source #

Utils for Translation

type UniqName = (String, Int) Source #

type NameMap a = Map a UniqName Source #

data SigMap a Source #

Mapping of symbols and sentence names to unique ids (used in export)

Constructors

SigMap (NameMap a) (NameMap String) 

data SigMapI a Source #

Mapping of OMDoc names to hets strings, for signature creation, and strings to symbols, for lookup in terms (used in import)

Constructors

SigMapI 

Fields

cdFromList :: [String] -> OMCD Source #

cdIsEmpty :: OMCD -> Bool Source #

cdToList :: OMCD -> [String] Source #

The result list has always two elements: [base, modul]

cdToMaybeList :: OMCD -> [Maybe String] Source #

Name handling: encoding, decoding, unique names

uniqPrefix :: String Source #

The closing paren + percent can be used neither in ordinary Hets-names nor in sentence names hence it is used here for encodings.

nameEncode Source #

Arguments

:: String

the kind of the encoding, may not contain colons

-> [String]

the values to encode

-> String 

Special name encoding in order to be able to recognize these names while reading.

nameDecode :: String -> Maybe (String, [String]) Source #

This invariant should hold: (x, l) = fromJust $ nameDecode $ nameEncode x l

Constructing/Extracting Values

tcName :: TCElement -> OMName Source #

name of the theory constitutive element, error if not TCSymbol, TCNotation, or TCImport

Lookup utils for Import and Export

lookupNotationInMap :: Map OMName String -> OMName -> String Source #

Pretty instances