{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : $Header$

Description : Inclusion of CASL_DL into CASL

Copyright : (c) Uni Bremen 2007

License : GPLv2 or higher, see LICENSE.txt

Maintainer : luecke@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable (via Logic.Logic)

-}

module Comorphisms.CASL_DL2CASL

(

CASL_DL2CASL (..)

)

where

import Logic.Logic

import Logic.Comorphism

import Common.AS_Annotation

import Common.ProofTree

import Common.Result

import qualified Common.Lib.Rel as Rel

-- CASL_DL = domain

import CASL_DL.PredefinedCASLAxioms

import CASL_DL.Logic_CASL_DL

import CASL_DL.AS_CASL_DL

import CASL_DL.Sign ()

import CASL_DL.StatAna -- DLSign

import CASL_DL.Sublogics

-- CASL = codomain

import CASL.Logic_CASL

import CASL.AS_Basic_CASL

import CASL.Sign

import CASL.Morphism

import CASL.Sublogic as Sublogic

import qualified Data.Set as Set

data CASL_DL2CASL = CASL_DL2CASL deriving Show

instance Language CASL_DL2CASL

instance Comorphism

CASL_DL2CASL -- comorphism

CASL_DL -- lid domain

CASL_DL_SL -- sublogics domain

DL_BASIC_SPEC -- Basic spec domain

DLFORMULA -- sentence domain

SYMB_ITEMS -- symbol items domain

SYMB_MAP_ITEMS -- symbol map items domain

DLSign -- signature domain

DLMor -- morphism domain

Symbol -- symbol domain

RawSymbol -- rawsymbol domain

ProofTree -- proof tree codomain

CASL -- lid codomain

CASL_Sublogics -- sublogics codomain

CASLBasicSpec -- Basic spec codomain

CASLFORMULA -- sentence codomain

SYMB_ITEMS -- symbol items codomain

SYMB_MAP_ITEMS -- symbol map items codomain

CASLSign -- signature codomain

CASLMor -- morphism codomain

Symbol -- symbol codomain

RawSymbol -- rawsymbol codomain

ProofTree -- proof tree domain

where

sourceLogic CASL_DL2CASL = CASL_DL

targetLogic CASL_DL2CASL = CASL

sourceSublogic CASL_DL2CASL = SROIQ

mapSublogic CASL_DL2CASL _ = Just $ Sublogic.caslTop

{ sub_features = LocFilSub

, cons_features = emptyMapConsFeature }

map_symbol CASL_DL2CASL _ = Set.singleton

map_sentence CASL_DL2CASL = trSentence

map_morphism CASL_DL2CASL = mapMor

map_theory CASL_DL2CASL = trTheory

isInclusionComorphism CASL_DL2CASL = True

has_model_expansion CASL_DL2CASL = True

{- | mapping of morphims, we just forget the

additional features -}

mapMor :: DLMor -> Result CASLMor

mapMor inMor =

let

ms = trSign $ msource inMor

mt = trSign $ mtarget inMor

sm = sort_map inMor

fm = op_map inMor

pm = pred_map inMor

in return (embedMorphism () ms mt)

{ sort_map = sm

, op_map = fm

, pred_map = pm }

-- | we forget additional information in the signature

projectToCASL :: DLSign -> CASLSign

projectToCASL dls = dls

{

sentences = []

, extendedInfo = ()

}

{- | Thing is established as the TopSort of all sorts

defined in the CASL_DL spec, a predefined signature

is added -}

trSign :: DLSign -> CASLSign

trSign inSig =

let

inC = projectToCASL inSig `uniteCASLSign` predefSign

inSorts = sortSet inSig

inData = sortSet predefSign

in

inC

{

sortRel = Rel.insertKey thing

$ Rel.insertKey dataS

$ Set.fold (`Rel.insertDiffPair` dataS)

(Set.fold (`Rel.insertDiffPair` thing)

(sortRel inC) inSorts)

$ Set.delete dataS inData

}

-- * translation of the signature predefined axioms are added

-- | Translation of theories

trTheory :: (DLSign, [Named (FORMULA DL_FORMULA)]) ->

Result (CASLSign, [Named (FORMULA ())])

trTheory (inSig, inForms) = do

outForms <- mapR (trNamedSentence inSig) inForms

return (trSign inSig, predefinedAxioms ++ outForms)

-- | translation of named sentences

trNamedSentence :: DLSign -> Named (FORMULA DL_FORMULA) ->

Result (Named (FORMULA ()))

trNamedSentence inSig inForm = do

outSen <- trSentence inSig $ sentence inForm

return $ mapNamed (const outSen) inForm

-- | translation of sentences

trSentence :: DLSign -> FORMULA DL_FORMULA -> Result (FORMULA ())

trSentence inSig inF =

case inF of

Quantification qf vs frm rn ->

do

outF <- trSentence inSig frm

return (Quantification qf vs outF rn)

Junction j fns rn ->

do

outF <- mapR (trSentence inSig) fns

return (Junction j outF rn)

Relation f1 c f2 rn ->

do

out1 <- trSentence inSig f1

out2 <- trSentence inSig f2

return (Relation out1 c out2 rn)

Negation frm rn ->

do

outF <- trSentence inSig frm

return (Negation outF rn)

Atom b rn -> return (Atom b rn)

Predication pr trm rn ->

do

ot <- mapR (trTerm inSig) trm

return (Predication pr ot rn)

Definedness tm rn ->

do

ot <- trTerm inSig tm

return (Definedness ot rn)

Equation t1 e t2 rn ->

do

ot1 <- trTerm inSig t1

ot2 <- trTerm inSig t2

return (Equation ot1 e ot2 rn)

Membership t1 st rn ->

do

ot <- trTerm inSig t1

return (Membership ot st rn)

Mixfix_formula trm ->

do

ot <- trTerm inSig trm

return (Mixfix_formula ot)

Unparsed_formula str rn ->

return (Unparsed_formula str rn)

Sort_gen_ax cstr ft ->

return (Sort_gen_ax cstr ft)

QuantOp {} -> fail "CASL_DL2CASL.QuantOp"

QuantPred {} -> fail "CASL_DL2CASL.QuantPred"

ExtFORMULA form ->

case form of

Cardinality {} ->

fail "Mapping of cardinality not implemented"

-- | translation of terms

trTerm :: DLSign -> TERM DL_FORMULA -> Result (TERM ())

trTerm inSig inF =

case inF of

Qual_var v s rn -> return (Qual_var v s rn)

Application os tms rn ->

do

ot <- mapR (trTerm inSig) tms

return (Application os ot rn)

Sorted_term trm st rn ->

do

ot <- trTerm inSig trm

return (Sorted_term ot st rn)

Cast trm st rn ->

do

ot <- trTerm inSig trm

return (Cast ot st rn)

Conditional t1 frm t2 rn ->

do

ot1 <- trTerm inSig t1

ot2 <- trTerm inSig t2

of1 <- trSentence inSig frm

return (Conditional ot1 of1 ot2 rn)

Unparsed_term str rn -> return (Unparsed_term str rn)

Mixfix_qual_pred ps -> return (Mixfix_qual_pred ps)

Mixfix_term trm ->

do

ot <- mapR (trTerm inSig) trm

return (Mixfix_term ot)

Mixfix_token tok -> return (Mixfix_token tok)

Mixfix_sorted_term st rn -> return (Mixfix_sorted_term st rn)

Mixfix_cast st rn -> return (Mixfix_cast st rn)

Mixfix_parenthesized trm rn ->

do

ot <- mapR (trTerm inSig) trm

return (Mixfix_parenthesized ot rn)

Mixfix_bracketed trm rn ->

do

ot <- mapR (trTerm inSig) trm

return (Mixfix_bracketed ot rn)

Mixfix_braced trm rn ->

do

ot <- mapR (trTerm inSig) trm

return (Mixfix_braced ot rn)

ExtTERM _ -> return $ ExtTERM ()