{- |

Module : $Header$

Description : Hets-to-OMDoc conversion

Copyright : (c) Ewaryst Schulz, DFKI Bremen 2009

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : ewaryst.schulz@dfki.de

Stability : provisional

Portability : non-portable(Logic)

CASL implementation of the interface functions export_signToOmdoc,

export_morphismToOmdoc, export_senToOmdoc from class Logic. The actual

instantiation can be found in module CASL.Logic_CASL.

-}

module CASL.OMDoc

( exportSignToOmdoc

, exportMorphismToOmdoc

, exportSenToOmdoc

, omdocMetaTheory

) where

import OMDoc.DataTypes

import Common.AS_Annotation

import Common.Id

import Common.LibName

import Common.Result

import qualified Common.Lib.Rel as Rel

import Common.DocUtils

import CASL.AS_Basic_CASL

import CASL.ATC_CASL ()

import CASL.Sign

import CASL.Morphism

import CASL.Fold

import CASL.Quantification

import Data.Map as Map

import Data.Set as Set

import Data.Maybe

-- | the identifier of a specification, combining the specid and the libid

data SPEC_ID = SPEC_ID Id Id | NOSPEC deriving Show

omdocMetaTheory :: Maybe OMCD

omdocMetaTheory = Just $ CD "casl" $ Just "http://cds.omdoc.org/logics/casl.omdoc"

exportSignToOmdoc :: (Show f, Pretty e) => SIMPLE_ID -> LibId -> Sign f e ->

[TCElement]

exportSignToOmdoc sid lid sign =

catMaybes

$ Set.toList (Set.map (sortSignToOmdoc spid sign) (sortSet sign))

++ Prelude.map (exportSubsortToOmdoc spid) (Rel.toList $ sortRel sign)

++ Map.elems (mapWithKey (funSignToOmdoc spid sign) (opMap sign))

++ Map.elems (mapWithKey (predSignToOmdoc spid sign) (predMap sign))

where spid = (SPEC_ID (simpleIdToId sid) (libIdToId lid))

exportMorphismToOmdoc :: (Pretty e, Show f, Pretty m) => Morphism f e m -> TCElement

--exportMorphismToOmdoc morphism = []

--exportMorphismToOmdoc _ = error "not implemented yet"

exportMorphismToOmdoc (Morphism _ _ sortmap opmap predmap _) =

{- TCComment $ "morphism"

++ " sourcesign: " ++ (show $ pretty s)

++ " sortmaplength=" ++ (show $ Map.size sortmap)

++ " opmaplength=" ++ (show $ Map.size opmap)

++ " predmaplength=" ++ (show $ Map.size predmap)

-}

TCMorphism $ Map.elems (mapWithKey (makeSortMapEntry NOSPEC) sortmap)

++ Map.elems (mapWithKey (makeOpMapEntry NOSPEC) opmap)

++ Map.elems (mapWithKey (makePredMapEntry NOSPEC) predmap)

exportSubsortToOmdoc :: SPEC_ID -> (SORT, SORT) -> Maybe TCElement

exportSubsortToOmdoc spid (s1, s2) = Just $ TCAxiomOrTheorem Nothing

-- the name of the axiom is generated by (name of s1)<(name of s2)

(idToName spid s1 ++ "<" ++ idToName spid s2)

$ OMA [const_subsortof, sortToOmdoc spid s1, sortToOmdoc spid s2]

exportSenToOmdoc :: (GetRange f, Pretty f) => SIMPLE_ID -> LibId -> Sign f e

-> Named(FORMULA f) -> TCElement

exportSenToOmdoc sid lid sign f =

let spid = (SPEC_ID (simpleIdToId sid) (libIdToId lid))

sname = (senAttr f)

sen = sentence f

in

case sen of

Sort_gen_ax cs b -> makeADTsFromConstraints spid sign cs b

_ -> TCAxiomOrTheorem

(if isAxiom f then Nothing else Just const_unproven)

sname $ foldFormula

(omdocRec spid

sign (\_ -> error "CASL extension not supported."))

sen

sfail :: String -> Range -> a

sfail s r = error $ show (Diag Error ("unexpected " ++ s) r)

-------------------------- ADT --------------------------

makeADTsFromConstraints :: SPEC_ID -> Sign f e -> [Constraint] -> Bool

-> TCElement

makeADTsFromConstraints spid _ cs b =

TCADT $ Prelude.map (makeADTSortDef spid b) cs

makeADTSortDef :: SPEC_ID -> Bool -> Constraint -> OmdADT

makeADTSortDef spid b (Constraint s l _) =

ADTSortDef (idToName spid s) b $

Prelude.map (makeADTConstructor spid . fst) l

makeADTConstructor :: SPEC_ID -> OP_SYMB -> OmdADT

makeADTConstructor spid (Qual_op_name n (Op_type _ args _ _) _) =

ADTConstr (idToName spid n) $ Prelude.map (makeADTArgument spid) args

makeADTConstructor _ (Op_name (Id _ _ r)) = sfail "No_qual_op" r

-- No support for selectors

makeADTArgument :: SPEC_ID -> SORT -> OmdADT

makeADTArgument spid s = ADTArg (sortToOmdoc spid s) Nothing

-------------------------- Theory constitutive --------------------------

sortSignToOmdoc :: SPEC_ID -> Sign a e -> SORT -> Maybe TCElement

sortSignToOmdoc spid _ s

| isLocalId spid s = Just $ TCSymbol (idToName spid s) const_sort Typ

-- | otherwise = Just $ TCComment $ "nonlocal symbol: " ++ (show s)

| otherwise = Nothing

-- assuming here the the set of pred types contains only one Element!

predSignToOmdoc :: SPEC_ID -> Sign a e -> Id -> (Set.Set PredType) ->

Maybe TCElement

predSignToOmdoc spid _ p ptypes

| isLocalId spid p =

Just $ TCSymbol (idToName spid p)

(makePredType spid $ Set.findMin ptypes) Obj

-- | otherwise = Just $ TCComment $ "nonlocal predicate: " ++ (show p)

| otherwise = Nothing

-- assuming here the the set of op types contains only one Element!

funSignToOmdoc :: SPEC_ID -> Sign a e -> Id -> (Set.Set OpType) ->

Maybe TCElement

funSignToOmdoc spid _ f ftypes

| isLocalId spid f =

Just $ TCSymbol (idToName spid f)

(makeObjectType spid $ Set.findMin ftypes)

Obj

-- | otherwise = Just $ TCComment $ "nonlocal function: " ++ (show f)

| otherwise = Nothing

-------------------------- types --------------------------

-- | Given an operator or predicate signature we construct the according type

makeType :: SPEC_ID -> OpKind -> [SORT] -> Maybe SORT -> OMElement

makeType spid _ [] (Just r) = (sortToOmdoc spid r)

makeType spid total domain range =

(OMA $ funtypeconstr : (Prelude.map (sortToOmdoc spid) args))

where

funtypeconstr = case total of

Total -> case range of

Nothing -> const_predtype

_ -> const_funtype

Partial -> const_partialfuntype

args = case range of Nothing -> domain

Just r -> domain ++ [r]

makePredType :: SPEC_ID -> PredType -> OMElement

makePredType spid (PredType predargs) =

makeType spid Total predargs Nothing

makeObjectType :: SPEC_ID -> OpType -> OMElement

makeObjectType spid (OpType opkind opargs oprange) =

makeType spid opkind opargs (Just oprange)

-------------------------- Names --------------------------

-- | the qualified name of an identifier consisting of

-- the name, the spec and the lib

data NameTriple = NameTriple { getName :: String

, getSpecName :: String

, getLibName :: String } deriving Show

idToName :: SPEC_ID -> Id -> String

idToName spid = getName . (idToNameTriple spid)

idToNameTriple :: SPEC_ID -> Id -> NameTriple

-- spid-structure

idToNameTriple spid s

| isQualName s = NameTriple { getName = show $ unQualName s

, getSpecName = show $ getNodeId s

, getLibName = show $ libIdOfQualName s }

| otherwise = case spid of

(SPEC_ID sid lid) -> NameTriple { getName = show s

, getSpecName = show sid

, getLibName = show lid }

NOSPEC -> error $ "unqualified morphism entry " ++ show s

isLocalId :: SPEC_ID -> Id -> Bool

-- spid-structure

isLocalId (SPEC_ID s l) i@(Id _ [_, s1, l1] _)

| isQualName i = (s == s1) && (l == l1)

| otherwise = True

isLocalId _ _ = True

-------------------------- OpenMath --------------------------

-- | probably outsource this to a generic module

makeOMS :: NameTriple -> OMElement

makeOMS (NameTriple { getName = i, getSpecName = s, getLibName = l }) =

-- special handling for library entries !??

OMS (CD s $ if l == "library" || l == "" then Nothing else Just l)

$ mkSimpleName i

idToOmdoc :: SPEC_ID -> Id -> OMElement

idToOmdoc spid s = makeOMS $ idToNameTriple spid s

sortToOmdoc :: SPEC_ID -> Id -> OMElement

sortToOmdoc = idToOmdoc

funToOmdoc :: SPEC_ID -> OP_SYMB -> OMElement

funToOmdoc spid (Qual_op_name i _ _) = idToOmdoc spid i

funToOmdoc spid (Op_name i) = idToOmdoc spid i

predToOmdoc :: SPEC_ID -> PRED_SYMB -> OMElement

predToOmdoc spid (Qual_pred_name i _ _) = idToOmdoc spid i

predToOmdoc spid (Pred_name i) = idToOmdoc spid i

-- | the object e1 and its type e2

makeAttribution :: OMElement -> OMElement -> OMElement

makeAttribution e1 e2 = OMATTT e1 $ OMAttr const_type e2

varToOmdoc :: Token -> OMElement

varToOmdoc v = OMV $ mkSimpleName $ tokStr v

-- | typed vars can only be typed by a single sort (first order)

varDeclToOMDoc :: SPEC_ID -> (VAR, SORT) -> OMElement

varDeclToOMDoc spid (v, s) = makeAttribution (varToOmdoc v) $

sortToOmdoc spid s

-- cdbase entries missing for predefined content dictionaries

const_casl :: String -> OMElement

const_casl n = OMS (CD "casl" Nothing) $ mkSimpleName 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_unproven, const_subsortof :: OMElement

const_true = const_casl "true"

const_false = const_casl "false"

const_funtype = const_casl "funtype"

const_partialfuntype = const_casl "partialfuntype"

const_predtype = const_casl "predtype"

const_type = const_casl "type"

const_subsortof = const_casl "subsortof"

const_not = const_casl "not"

const_and = const_casl "and"

const_or = const_casl "or"

const_implies = const_casl "implies"

const_implied = const_casl "implied"

const_equivalent = const_casl "equivalent"

const_forall = const_casl "forall"

const_exists = const_casl "exists"

const_eq = const_casl "eq"

const_eeq = const_casl "eeq"

const_existsunique = const_casl "existsunique"

const_def = const_casl "def"

const_in = const_casl "in"

const_if = const_casl "if"

const_cast = const_casl "cast"

const_sort = const_casl "sort"

const_unproven = const_casl "unproven"

omdocRec :: GetRange f => SPEC_ID -> Sign f e -> (f -> OMElement)

-> Record f OMElement OMElement

omdocRec spid _ mf = Record

{ foldQuantification = \ _ q vs f _ ->

let s = case q of

Universal -> const_forall

Existential -> const_exists

Unique_existential -> const_existsunique

vl = Prelude.map (varDeclToOMDoc spid) $ flatVAR_DECLs vs

in OMBIND s vl f

, foldConjunction = \ _ fs _ -> OMA $ const_and : fs

, foldDisjunction = \ _ fs _ -> OMA $ const_or : fs

, foldImplication = \ _ f1 f2 b _ ->

if b then (OMA [const_implies , f1, f2])

else (OMA [const_implied , f1, f2])

, foldEquivalence = \ _ f1 f2 _ ->

(OMA [const_equivalent , f1, f2])

, foldNegation = \ _ f _ -> (OMA [const_not , f])

, foldTrue_atom = \ _ _ -> const_true

, foldFalse_atom = \ _ _ -> const_false

, foldPredication = \ _ p ts _ -> OMA $ (predToOmdoc spid p) : ts

, foldDefinedness = \ _ t _ -> OMA [const_def, t]

, foldExistl_equation = \ _ t1 t2 _ -> (OMA [const_eeq , t1, t2])

, foldStrong_equation = \ _ t1 t2 _ -> (OMA [const_eq , t1, t2])

, foldMembership = \ _ t s _ ->

(OMA [const_in , t, sortToOmdoc spid s])

, foldMixfix_formula = \ t _ -> sfail "Mixfix_formula" $ getRange t

, foldQuantOp = \ _ o _ _ -> sfail ("QuantOp " ++ show o) $ getRange o

, foldQuantPred = \ _ p _ _ -> sfail ("QuantPred " ++ show p) $ getRange p

, foldSort_gen_ax = \ t _ _ -> sfail

"Sort generating axioms should be filtered out before!"

$ getRange t

, foldExtFORMULA = \ _ f -> mf f

, foldQual_var = \ _ v _ _ -> varToOmdoc v

, foldApplication = \ _ o ts _ -> OMA $ (funToOmdoc spid o) : ts

, foldSorted_term = \ _ r _ _ -> r

, foldCast = \ _ t s _ ->

(OMA [const_cast , t, sortToOmdoc spid s])

, foldConditional = \ _ e f t _ -> (OMA [const_if , e , t, f])

, foldMixfix_qual_pred = \ _ p -> sfail "Mixfix_qual_pred" $ getRange p

, foldMixfix_term = \ (Mixfix_term ts) _ ->

sfail "Mixfix_term" $ getRange ts

, foldMixfix_token = \ _ t -> sfail "Mixfix_token" $ tokPos t

, foldMixfix_sorted_term = \ _ _ r -> sfail "Mixfix_sorted_term" r

, foldMixfix_cast = \ _ _ r -> sfail "Mixfix_cast" r

, foldMixfix_parenthesized = \ _ _ r -> sfail "Mixfix_parenthesized" r

, foldMixfix_bracketed = \ _ _ r -> sfail "Mixfix_bracketed" r

, foldMixfix_braced = \ _ _ r -> sfail "Mixfix_braced" r }

-------------------------- Morphisms --------------------------

makeSortMapEntry :: SPEC_ID -> SORT -> SORT -> (OMName, OMElement)

makeSortMapEntry spid s1 s2 = (mkSimpleName $ idToName spid s1, sortToOmdoc spid s2)

makeOpMapEntry :: SPEC_ID -> (Id, OpType) -> (Id, OpKind) ->

(OMName, OMElement)

makeOpMapEntry spid (o1, _) (o2, _) =

(mkSimpleName $ idToName spid o1, idToOmdoc spid o2)

makePredMapEntry :: SPEC_ID -> (Id, PredType) -> Id -> (OMName, OMElement)

makePredMapEntry spid (p1, _) p2 =

(mkSimpleName $ idToName spid p1, idToOmdoc spid p2)

--------------------------------------------------------------------