{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CoCASL2CoPCFOL.hs
Description :  Extension of CASL2PCFOL to CoCASL
Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Coding out subsorting, lifted tot eh level of CoCASL
-}

module Comorphisms.CoCASL2CoPCFOL where

import Logic.Logic
import Logic.Comorphism
import qualified Data.Set as Set
import Common.AS_Annotation

-- CoCASL
import CoCASL.Logic_CoCASL
import CoCASL.AS_CoCASL
import CoCASL.StatAna
import CoCASL.Sublogic
import CASL.Sublogic as SL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Inject
import CASL.Project
import CASL.Monoton
import Comorphisms.CASL2PCFOL

-- | The identity of the comorphism
data CoCASL2CoPCFOL = CoCASL2CoPCFOL deriving Int -> CoCASL2CoPCFOL -> ShowS
[CoCASL2CoPCFOL] -> ShowS
CoCASL2CoPCFOL -> String
(Int -> CoCASL2CoPCFOL -> ShowS)
-> (CoCASL2CoPCFOL -> String)
-> ([CoCASL2CoPCFOL] -> ShowS)
-> Show CoCASL2CoPCFOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CoCASL2CoPCFOL] -> ShowS
$cshowList :: [CoCASL2CoPCFOL] -> ShowS
show :: CoCASL2CoPCFOL -> String
$cshow :: CoCASL2CoPCFOL -> String
showsPrec :: Int -> CoCASL2CoPCFOL -> ShowS
$cshowsPrec :: Int -> CoCASL2CoPCFOL -> ShowS
Show

instance Language CoCASL2CoPCFOL -- default definition is okay

instance Comorphism CoCASL2CoPCFOL
               CoCASL CoCASL_Sublogics
               C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CSign
               CoCASLMor
               Symbol RawSymbol ()
               CoCASL CoCASL_Sublogics
               C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CSign
               CoCASLMor
               Symbol RawSymbol () where
    sourceLogic :: CoCASL2CoPCFOL -> CoCASL
sourceLogic CoCASL2CoPCFOL = CoCASL
CoCASL
    sourceSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics
sourceSublogic CoCASL2CoPCFOL = CoCASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.caslTop
    targetLogic :: CoCASL2CoPCFOL -> CoCASL
targetLogic CoCASL2CoPCFOL = CoCASL
CoCASL
    mapSublogic :: CoCASL2CoPCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics
mapSublogic CoCASL2CoPCFOL sl :: CoCASL_Sublogics
sl = CoCASL_Sublogics -> Maybe CoCASL_Sublogics
forall a. a -> Maybe a
Just (CoCASL_Sublogics -> Maybe CoCASL_Sublogics)
-> CoCASL_Sublogics -> Maybe CoCASL_Sublogics
forall a b. (a -> b) -> a -> b
$
          CoCASL_Sublogics -> CoCASL_Sublogics -> CoCASL_Sublogics
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max CoCASL_Sublogics
forall a. Lattice a => CASL_SL a
need_horn CoCASL_Sublogics
sl
            { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
NoSub  -- subsorting is coded out
            , has_part :: Bool
has_part = Bool
True
            , has_eq :: Bool
has_eq = Bool
True
            }
    map_theory :: CoCASL2CoPCFOL
-> (CSign, [Named CoCASLFORMULA])
-> Result (CSign, [Named CoCASLFORMULA])
map_theory CoCASL2CoPCFOL = (CSign -> Result (CSign, [Named CoCASLFORMULA]))
-> (CSign -> CoCASLFORMULA -> Result CoCASLFORMULA)
-> (CSign, [Named CoCASLFORMULA])
-> Result (CSign, [Named CoCASLFORMULA])
forall (m :: * -> *) sign1 sign2 sentence2 sentence1.
Monad m =>
(sign1 -> m (sign2, [Named sentence2]))
-> (sign1 -> sentence1 -> m sentence2)
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
mkTheoryMapping ( \ sig :: CSign
sig ->
      let e :: CSign
e = CSign -> CSign
forall f e. Sign f e -> Sign f e
encodeSig CSign
sig in (CSign, [Named CoCASLFORMULA])
-> Result (CSign, [Named CoCASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return
      (CSign
e, (Named CoCASLFORMULA -> Named CoCASLFORMULA)
-> [Named CoCASLFORMULA] -> [Named CoCASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((CoCASLFORMULA -> CoCASLFORMULA)
-> Named CoCASLFORMULA -> Named CoCASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((CoCASLFORMULA -> CoCASLFORMULA)
 -> Named CoCASLFORMULA -> Named CoCASLFORMULA)
-> (CoCASLFORMULA -> CoCASLFORMULA)
-> Named CoCASLFORMULA
-> Named CoCASLFORMULA
forall a b. (a -> b) -> a -> b
$ (C_FORMULA -> C_FORMULA) -> CoCASLFORMULA -> CoCASLFORMULA
forall f. TermExtension f => (f -> f) -> FORMULA f -> FORMULA f
injFormula C_FORMULA -> C_FORMULA
injC_Formula) (CSign -> [Named CoCASLFORMULA]
forall f e. Sign f e -> [Named (FORMULA f)]
monotonicities CSign
sig)
          [Named CoCASLFORMULA]
-> [Named CoCASLFORMULA] -> [Named CoCASLFORMULA]
forall a. [a] -> [a] -> [a]
++ (Named CoCASLFORMULA -> Named CoCASLFORMULA)
-> [Named CoCASLFORMULA] -> [Named CoCASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((CoCASLFORMULA -> CoCASLFORMULA)
-> Named CoCASLFORMULA -> Named CoCASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed CoCASLFORMULA -> CoCASLFORMULA
forall f1 f. FORMULA f1 -> FORMULA f
mapFORMULA) (CSign -> [Named CoCASLFORMULA]
forall f e. TermExtension f => Sign f e -> [Named (FORMULA f)]
generateAxioms CSign
sig)))
      (CoCASL2CoPCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> sentence1 -> Result sentence2
map_sentence CoCASL2CoPCFOL
CoCASL2CoPCFOL)
    map_morphism :: CoCASL2CoPCFOL -> CoCASLMor -> Result CoCASLMor
map_morphism CoCASL2CoPCFOL mor :: CoCASLMor
mor = CoCASLMor -> Result CoCASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return
      (CoCASLMor
mor { msource :: CSign
msource = CSign -> CSign
forall f e. Sign f e -> Sign f e
encodeSig (CSign -> CSign) -> CSign -> CSign
forall a b. (a -> b) -> a -> b
$ CoCASLMor -> CSign
forall f e m. Morphism f e m -> Sign f e
msource CoCASLMor
mor
           , mtarget :: CSign
mtarget = CSign -> CSign
forall f e. Sign f e -> Sign f e
encodeSig (CSign -> CSign) -> CSign -> CSign
forall a b. (a -> b) -> a -> b
$ CoCASLMor -> CSign
forall f e m. Morphism f e m -> Sign f e
mtarget CoCASLMor
mor })
      -- other components need not to be adapted!
    map_sentence :: CoCASL2CoPCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA
map_sentence CoCASL2CoPCFOL _ = CoCASLFORMULA -> Result CoCASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CoCASLFORMULA -> Result CoCASLFORMULA)
-> (CoCASLFORMULA -> CoCASLFORMULA)
-> CoCASLFORMULA
-> Result CoCASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoCASLFORMULA -> CoCASLFORMULA
cf2CFormula
    map_symbol :: CoCASL2CoPCFOL -> CSign -> Symbol -> Set Symbol
map_symbol CoCASL2CoPCFOL _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (Symbol -> Symbol) -> Symbol -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
forall a. a -> a
id
    has_model_expansion :: CoCASL2CoPCFOL -> Bool
has_model_expansion CoCASL2CoPCFOL = Bool
True
    is_weakly_amalgamable :: CoCASL2CoPCFOL -> Bool
is_weakly_amalgamable CoCASL2CoPCFOL = Bool
True

cf2CFormula :: FORMULA C_FORMULA -> FORMULA C_FORMULA
cf2CFormula :: CoCASLFORMULA -> CoCASLFORMULA
cf2CFormula = OpKind
-> (C_FORMULA -> C_FORMULA) -> CoCASLFORMULA -> CoCASLFORMULA
forall f.
TermExtension f =>
OpKind -> (f -> f) -> FORMULA f -> FORMULA f
projFormula OpKind
Partial C_FORMULA -> C_FORMULA
projC_Formula (CoCASLFORMULA -> CoCASLFORMULA)
-> (CoCASLFORMULA -> CoCASLFORMULA)
-> CoCASLFORMULA
-> CoCASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (C_FORMULA -> C_FORMULA) -> CoCASLFORMULA -> CoCASLFORMULA
forall f. TermExtension f => (f -> f) -> FORMULA f -> FORMULA f
injFormula C_FORMULA -> C_FORMULA
injC_Formula

projC_Formula :: C_FORMULA -> C_FORMULA
projC_Formula :: C_FORMULA -> C_FORMULA
projC_Formula = Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA)
-> CoRecord CoCASLFORMULA (TERM C_FORMULA) C_FORMULA MODALITY
-> C_FORMULA
-> C_FORMULA
forall a b c d.
Record C_FORMULA a b -> CoRecord a b c d -> C_FORMULA -> c
foldC_Formula (OpKind
-> (C_FORMULA -> C_FORMULA)
-> Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA)
forall f.
TermExtension f =>
OpKind -> (f -> f) -> Record f (FORMULA f) (TERM f)
projRecord OpKind
Partial C_FORMULA -> C_FORMULA
projC_Formula) CoRecord CoCASLFORMULA (TERM C_FORMULA) C_FORMULA MODALITY
mapCoRecord

injC_Formula :: C_FORMULA -> C_FORMULA
injC_Formula :: C_FORMULA -> C_FORMULA
injC_Formula = Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA)
-> CoRecord CoCASLFORMULA (TERM C_FORMULA) C_FORMULA MODALITY
-> C_FORMULA
-> C_FORMULA
forall a b c d.
Record C_FORMULA a b -> CoRecord a b c d -> C_FORMULA -> c
foldC_Formula ((C_FORMULA -> C_FORMULA)
-> Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA)
forall f.
TermExtension f =>
(f -> f) -> Record f (FORMULA f) (TERM f)
injRecord C_FORMULA -> C_FORMULA
injC_Formula) CoRecord CoCASLFORMULA (TERM C_FORMULA) C_FORMULA MODALITY
mapCoRecord