{- |
Module      :  ./CASL/OMDoc.hs
Description :  CASL specific OMDoc constants
Copyright   :  (c) Ewaryst Schulz, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  ewaryst.schulz@dfki.de
Stability   :  provisional
Portability :  portable

Library of CASL specific OMDoc constants
-}

module CASL.OMDoc where

import OMDoc.DataTypes

-- * Meta theory

-- | CASL meta theory content dictionary
caslMetaTheory :: OMCD
caslMetaTheory :: OMCD
caslMetaTheory = [String] -> OMCD
CD ["casl", "http://cds.omdoc.org/logics/casl/casl.omdoc"]


-- * Terms

-- cdbase entries missing for predefined content dictionaries

const_casl :: String -> OMElement
const_casl :: String -> OMElement
const_casl n :: String
n = OMQualName -> OMElement
OMS (OMCD
caslMetaTheory, String -> OMName
mkSimpleName String
n)

const_true, const_false, const_sort, const_funtype, const_partialfuntype
 , const_and, const_or, const_implies, const_implied, const_equivalent
 , const_forall, const_exists, const_eq, const_eeq, const_existsunique
 , const_def, const_in, const_if, const_cast, const_type, const_not
 , const_predtype, const_subsortof :: OMElement

const_true :: OMElement
const_true = String -> OMElement
const_casl "true"
const_false :: OMElement
const_false = String -> OMElement
const_casl "false"

const_funtype :: OMElement
const_funtype = String -> OMElement
const_casl "funtype"
const_partialfuntype :: OMElement
const_partialfuntype = String -> OMElement
const_casl "partialfuntype"
const_predtype :: OMElement
const_predtype = String -> OMElement
const_casl "predtype"
const_type :: OMElement
const_type = String -> OMElement
const_casl "type"
const_subsortof :: OMElement
const_subsortof = String -> OMElement
const_casl "subsortof"

const_not :: OMElement
const_not = String -> OMElement
const_casl "not"
const_and :: OMElement
const_and = String -> OMElement
const_casl "and"
const_or :: OMElement
const_or = String -> OMElement
const_casl "or"
const_implies :: OMElement
const_implies = String -> OMElement
const_casl "implies"
const_implied :: OMElement
const_implied = String -> OMElement
const_casl "implied"
const_equivalent :: OMElement
const_equivalent = String -> OMElement
const_casl "equivalent"

const_forall :: OMElement
const_forall = String -> OMElement
const_casl "forall"
const_exists :: OMElement
const_exists = String -> OMElement
const_casl "exists"

const_eq :: OMElement
const_eq = String -> OMElement
const_casl "eq"
const_eeq :: OMElement
const_eeq = String -> OMElement
const_casl "eeq"
const_existsunique :: OMElement
const_existsunique = String -> OMElement
const_casl "existsunique"
const_def :: OMElement
const_def = String -> OMElement
const_casl "def"
const_in :: OMElement
const_in = String -> OMElement
const_casl "in"
const_if :: OMElement
const_if = String -> OMElement
const_casl "if"
const_cast :: OMElement
const_cast = String -> OMElement
const_casl "cast"
const_sort :: OMElement
const_sort = String -> OMElement
const_casl "sort"