3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl{- |

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristlModule : $Header$

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristlDescription : Inclusion of CASL_DL into CASL

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristlCopyright : (c) Uni Bremen 2007

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristlLicense : GPLv2 or higher

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristlMaintainer : luecke@informatik.uni-bremen.de

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristlStability : provisional

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristlPortability : non-portable (via Logic.Logic)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-}

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlmodule Comorphisms.CASL_DL2CASL

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl (

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl CASL_DL2CASL(..)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl )

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl where

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport Logic.Logic

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport Logic.Comorphism

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport Common.AS_Annotation

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport Common.ProofTree

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport Common.Result

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport qualified Common.Lib.Rel as Rel

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl--CASL_DL = domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL_DL.PredefinedCASLAxioms

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL_DL.Logic_CASL_DL

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL_DL.AS_CASL_DL

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL_DL.Sign()

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL_DL.PredefinedSign

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL_DL.StatAna -- DLSign

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL_DL.Sublogics

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl--CASL = codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL.Logic_CASL

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL.AS_Basic_CASL

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL.Sign

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL.Morphism

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport CASL.Sublogic as Sublogic

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlimport qualified Data.Set as Set

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristldata CASL_DL2CASL = CASL_DL2CASL deriving Show

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlinstance Language CASL_DL2CASL

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristlinstance Comorphism

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl CASL_DL2CASL -- comorphism

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl CASL_DL -- lid domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl CASL_DL_SL -- sublogics domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl DL_BASIC_SPEC -- Basic spec domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl DLFORMULA -- sentence domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl SYMB_ITEMS -- symbol items domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl SYMB_MAP_ITEMS -- symbol map items domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl DLSign -- signature domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl DLMor -- morphism domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Symbol -- symbol domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl RawSymbol -- rawsymbol domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ProofTree -- proof tree codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl CASL -- lid codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl CASL_Sublogics -- sublogics codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl CASLBasicSpec -- Basic spec codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl CASLFORMULA -- sentence codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl SYMB_ITEMS -- symbol items codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl SYMB_MAP_ITEMS -- symbol map items codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl CASLSign -- signature codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl CASLMor -- morphism codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Symbol -- symbol codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl RawSymbol -- rawsymbol codomain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ProofTree -- proof tree domain

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl where

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl sourceLogic CASL_DL2CASL = CASL_DL

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl targetLogic CASL_DL2CASL = CASL

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl sourceSublogic CASL_DL2CASL = SROIQ

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl mapSublogic CASL_DL2CASL _ = Just $ Sublogic.caslTop

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl { sub_features = LocFilSub

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl , cons_features = emptyMapConsFeature }

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl map_symbol CASL_DL2CASL _ = Set.singleton

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl map_sentence CASL_DL2CASL = trSentence

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl map_morphism CASL_DL2CASL = mapMor

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl map_theory CASL_DL2CASL = trTheory

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl isInclusionComorphism CASL_DL2CASL = True

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl has_model_expansion CASL_DL2CASL = True

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- ^ mapping of morphims, we just forget the

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- ^ additional features

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristlmapMor :: DLMor -> Result CASLMor

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristlmapMor inMor =

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl let

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ms = trSign $ msource inMor

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl mt = trSign $ mtarget inMor

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl sm = sort_map inMor

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl fm = op_map inMor

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl pm = pred_map inMor

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl in return (embedMorphism () ms mt)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl { sort_map = sm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl , op_map = fm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl , pred_map = pm }

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- ^ we forget additional information in the signature

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristlprojectToCASL :: DLSign -> CASLSign

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristlprojectToCASL dls = dls

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl {

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl sentences = []

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl , extendedInfo = ()

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl }

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- ^ Thing is established as the TopSort of all sorts

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- ^ defined in the CASL_DL spec, a predefined signature

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- ^ is added

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristltrSign :: DLSign -> CASLSign

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristltrSign inSig =

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl let

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl inC = projectToCASL inSig `uniteCASLSign` predefSign

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl inSorts = sortSet inSig

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl inData = sortSet dataSig_CASL

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl in

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl inC

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl {

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl sortSet = Set.insert topSort $ Set.insert topSortD $ sortSet inC,

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl sortRel =

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Set.fold (\x -> Rel.insert x topSortD)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl (Set.fold (\x -> Rel.insert x topSort)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl (sortRel inC) inSorts) $

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Set.delete topSortD inData

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl }

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- ^ translation of the signature

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- ^ predefined axioms are added

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- Translation of theories

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristltrTheory :: (DLSign, [Named (FORMULA DL_FORMULA)]) ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Result (CASLSign, [Named (FORMULA ())])

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristltrTheory (inSig, inForms) = do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl outForms <- mapR (trNamedSentence inSig) inForms

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (trSign inSig, predefinedAxioms ++ outForms)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- ^ translation of named sentences

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristltrNamedSentence :: DLSign -> Named (FORMULA DL_FORMULA) ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Result (Named (FORMULA ()))

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristltrNamedSentence inSig inForm = do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl outSen <- trSentence inSig $ sentence inForm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return $ mapNamed (const outSen) inForm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- ^ translation of sentences

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristltrSentence :: DLSign -> FORMULA DL_FORMULA -> Result (FORMULA ())

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristltrSentence inSig inF =

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl case inF of

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Quantification qf vs frm rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl outF <- trSentence inSig frm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Quantification qf vs outF rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Conjunction fns rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl outF <- mapR (trSentence inSig) fns

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Conjunction outF rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Disjunction fns rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl outF <- mapR (trSentence inSig) fns

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Disjunction outF rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Implication f1 f2 b rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl out1 <- trSentence inSig f1

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl out2 <- trSentence inSig f2

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Implication out1 out2 b rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Equivalence f1 f2 rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl out1 <- trSentence inSig f1

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl out2 <- trSentence inSig f2

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Equivalence out1 out2 rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Negation frm rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl outF <- trSentence inSig frm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Negation outF rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl True_atom rn -> return (True_atom rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl False_atom rn -> return (False_atom rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Predication pr trm rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot <- mapR (trTerm inSig) trm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Predication pr ot rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Definedness tm rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot <- trTerm inSig tm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Definedness ot rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Existl_equation t1 t2 rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot1 <- trTerm inSig t1

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot2 <- trTerm inSig t2

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Existl_equation ot1 ot2 rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Strong_equation t1 t2 rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot1 <- trTerm inSig t1

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot2 <- trTerm inSig t2

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Strong_equation ot1 ot2 rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Membership t1 st rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot <- trTerm inSig t1

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Membership ot st rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Mixfix_formula trm ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot <- trTerm inSig trm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Mixfix_formula ot)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Unparsed_formula str rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Unparsed_formula str rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Sort_gen_ax cstr ft ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Sort_gen_ax cstr ft)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl QuantOp _ _ _ -> fail "CASL_DL2CASL.QuantOp"

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl QuantPred _ _ _ -> fail "CASL_DL2CASL.QuantPred"

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ExtFORMULA form ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl case form of

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Cardinality _ _ _ _ _ _ ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl fail "Mapping of cardinality not implemented"

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl-- ^ translation of terms

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristltrTerm :: DLSign -> TERM DL_FORMULA -> Result (TERM ())

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias TristltrTerm inSig inF =

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl case inF of

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Qual_var v s rn -> return (Qual_var v s rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Application os tms rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot <- mapR (trTerm inSig) tms

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Application os ot rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Sorted_term trm st rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot <- trTerm inSig trm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Sorted_term ot st rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Cast trm st rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot <- trTerm inSig trm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Cast ot st rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Conditional t1 frm t2 rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot1 <- trTerm inSig t1

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot2 <- trTerm inSig t2

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl of1 <- trSentence inSig frm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Conditional ot1 of1 ot2 rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Unparsed_term str rn -> return (Unparsed_term str rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Mixfix_qual_pred ps -> return (Mixfix_qual_pred ps)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Mixfix_term trm ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot <- mapR (trTerm inSig) trm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Mixfix_term ot)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Mixfix_token tok -> return (Mixfix_token tok)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Mixfix_sorted_term st rn -> return (Mixfix_sorted_term st rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Mixfix_cast st rn -> return (Mixfix_cast st rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Mixfix_parenthesized trm rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot <- mapR (trTerm inSig) trm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Mixfix_parenthesized ot rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Mixfix_bracketed trm rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot <- mapR (trTerm inSig) trm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Mixfix_bracketed ot rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl Mixfix_braced trm rn ->

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl do

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl ot <- mapR (trTerm inSig) trm

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl return (Mixfix_braced ot rn)

3b70a3e7bfc7ae8aa755080c981dfc939e8a259eMatthias Tristl