Hets - the Heterogeneous Tool Set

Copyright(c) Ewaryst Schulz, DFKI Bremen 2009
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerewaryst.schulz@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

CASL.OMDocImport

Description

CASL implementation of the interface functions omdocToSym, omdocToSen , addOMadtToTheory, addOmdocToTheory from class Logic. The actual instantiation can be found in module CASL.Logic_CASL.

Synopsis

Documentation

omdocToSym :: Env -> TCElement -> String -> Result Symbol

A TCSymbols is transformed to a CASL symbol with given name.

addOMadtToTheory :: Env -> (Sign f e, [Named (FORMULA f)]) -> [[OmdADT]] -> Result (Sign f e, [Named (FORMULA f)])

Sort generation constraints are added as named formulas.

addOmdocToTheory :: Env -> (Sign f e, [Named (FORMULA f)]) -> [TCElement] -> Result (Sign f e, [Named (FORMULA f)])

The subsort relation is recovered from exported sentences.