{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/DFOL2CASL.hs
Description :  Translation of first-order logic with dependent types (DFOL) to
               CASL
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable

Ref: K. Sojakova and F. Rabe. Translating a Dependently-Typed Logic to
     First-Order Logic. LNCS 2009, pages 326-341.
-}

module Comorphisms.DFOL2CASL where

import Logic.Logic
import Logic.Comorphism

import Common.ProofTree

import DFOL.Logic_DFOL
import DFOL.AS_DFOL
import DFOL.Sign
import DFOL.Morphism
import DFOL.Symbol
import DFOL.Comorphism

import qualified CASL.Logic_CASL as CASL_Logic
import qualified CASL.Sublogic as CSL
import qualified CASL.AS_Basic_CASL as CASL_AS
import qualified CASL.Sign as CASL_Sign
import qualified CASL.Morphism as CASL_Morphism

-- cid for the comorphism
data DFOL2CASL = DFOL2CASL deriving Int -> DFOL2CASL -> ShowS
[DFOL2CASL] -> ShowS
DFOL2CASL -> String
(Int -> DFOL2CASL -> ShowS)
-> (DFOL2CASL -> String)
-> ([DFOL2CASL] -> ShowS)
-> Show DFOL2CASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DFOL2CASL] -> ShowS
$cshowList :: [DFOL2CASL] -> ShowS
show :: DFOL2CASL -> String
$cshow :: DFOL2CASL -> String
showsPrec :: Int -> DFOL2CASL -> ShowS
$cshowsPrec :: Int -> DFOL2CASL -> ShowS
Show

instance Language DFOL2CASL where
   language_name :: DFOL2CASL -> String
language_name DFOL2CASL = "DFOL2CASL"

instance Comorphism DFOL2CASL
   DFOL () BASIC_SPEC FORMULA SYMB_ITEMS SYMB_MAP_ITEMS
        Sign Morphism Symbol Symbol ()
   CASL_Logic.CASL CSL.CASL_Sublogics CASL_Logic.CASLBasicSpec
        CASL_AS.CASLFORMULA CASL_AS.SYMB_ITEMS CASL_AS.SYMB_MAP_ITEMS
        CASL_Sign.CASLSign CASL_Morphism.CASLMor CASL_Sign.Symbol
        CASL_Morphism.RawSymbol ProofTree
   where
   sourceLogic :: DFOL2CASL -> DFOL
sourceLogic DFOL2CASL = DFOL
DFOL
   sourceSublogic :: DFOL2CASL -> ()
sourceSublogic DFOL2CASL = ()
   targetLogic :: DFOL2CASL -> CASL
targetLogic DFOL2CASL = CASL
CASL_Logic.CASL
   mapSublogic :: DFOL2CASL -> () -> Maybe CASL_Sublogics
mapSublogic DFOL2CASL () = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just CASL_Sublogics
forall a. Lattice a => CASL_SL a
CSL.bottom
                      { has_eq :: Bool
CSL.has_eq = Bool
True
                      , has_pred :: Bool
CSL.has_pred = Bool
True
                      , which_logic :: CASL_Formulas
CSL.which_logic = CASL_Formulas
CSL.FOL
                      }
   map_theory :: DFOL2CASL
-> (Sign, [Named FORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory DFOL2CASL = (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall a. a -> Result a
wrapInResult ((CASLSign, [Named CASLFORMULA])
 -> Result (CASLSign, [Named CASLFORMULA]))
-> ((Sign, [Named FORMULA]) -> (CASLSign, [Named CASLFORMULA]))
-> (Sign, [Named FORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sign, [Named FORMULA]) -> (CASLSign, [Named CASLFORMULA])
theoryTransl
   map_symbol :: DFOL2CASL -> Sign -> Symbol -> Set Symbol
map_symbol DFOL2CASL = Sign -> Symbol -> Set Symbol
symbolTransl
   map_sentence :: DFOL2CASL -> Sign -> FORMULA -> Result CASLFORMULA
map_sentence DFOL2CASL sig :: Sign
sig = CASLFORMULA -> Result CASLFORMULA
forall a. a -> Result a
wrapInResult (CASLFORMULA -> Result CASLFORMULA)
-> (FORMULA -> CASLFORMULA) -> FORMULA -> Result CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> FORMULA -> CASLFORMULA
senTransl Sign
sig
   map_morphism :: DFOL2CASL -> Morphism -> Result CASLMor
map_morphism DFOL2CASL = CASLMor -> Result CASLMor
forall a. a -> Result a
wrapInResult (CASLMor -> Result CASLMor)
-> (Morphism -> CASLMor) -> Morphism -> Result CASLMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> CASLMor
morphTransl
   has_model_expansion :: DFOL2CASL -> Bool
has_model_expansion DFOL2CASL = Bool
True