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

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Comorphism)

coding out partiality, lifted to the level of CoCASL
-}

module Comorphisms.CoCASL2CoSubCFOL where

import Logic.Logic
import Logic.Comorphism

-- 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.Fold
import CASL.Simplify
import Comorphisms.CASL2SubCFOL

import qualified Data.Map as Map
import qualified Data.Set as Set
import Common.AS_Annotation
import Common.ProofUtils

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

instance Language CoCASL2CoSubCFOL -- default definition is okay

instance Comorphism CoCASL2CoSubCFOL
               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 :: CoCASL2CoSubCFOL -> CoCASL
sourceLogic CoCASL2CoSubCFOL = CoCASL
CoCASL
    sourceSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics
sourceSublogic CoCASL2CoSubCFOL = CoCASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.caslTop
    targetLogic :: CoCASL2CoSubCFOL -> CoCASL
targetLogic CoCASL2CoSubCFOL = CoCASL
CoCASL
    mapSublogic :: CoCASL2CoSubCFOL -> CoCASL_Sublogics -> Maybe CoCASL_Sublogics
mapSublogic CoCASL2CoSubCFOL 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
$
       if CoCASL_Sublogics -> Bool
forall a. CASL_SL a -> Bool
has_part CoCASL_Sublogics
sl then CoCASL_Sublogics
sl
        { has_part :: Bool
has_part = Bool
False -- partiality is coded out
        , has_pred :: Bool
has_pred = Bool
True
        , which_logic :: CASL_Formulas
which_logic = CASL_Formulas -> CASL_Formulas -> CASL_Formulas
forall a. Ord a => a -> a -> a
max CASL_Formulas
Horn (CASL_Formulas -> CASL_Formulas) -> CASL_Formulas -> CASL_Formulas
forall a b. (a -> b) -> a -> b
$ CoCASL_Sublogics -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic CoCASL_Sublogics
sl
        , has_eq :: Bool
has_eq = Bool
True} else CoCASL_Sublogics
sl
    map_theory :: CoCASL2CoSubCFOL
-> (CSign, [Named CoCASLFORMULA])
-> Result (CSign, [Named CoCASLFORMULA])
map_theory CoCASL2CoSubCFOL (sig :: CSign
sig, sens :: [Named CoCASLFORMULA]
sens) =
        let bsrts :: Set SORT
bsrts = FormulaTreatment -> CSign -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
sortsWithBottom (CASL2SubCFOL -> FormulaTreatment
formulaTreatment CASL2SubCFOL
defaultCASL2SubCFOL)
              CSign
sig (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set SORT] -> Set SORT) -> [Set SORT] -> Set SORT
forall a b. (a -> b) -> a -> b
$ (Named CoCASLFORMULA -> Set SORT)
-> [Named CoCASLFORMULA] -> [Set SORT]
forall a b. (a -> b) -> [a] -> [b]
map (CoCASLFORMULA -> Set SORT
botCoFormulaSorts (CoCASLFORMULA -> Set SORT)
-> (Named CoCASLFORMULA -> CoCASLFORMULA)
-> Named CoCASLFORMULA
-> Set SORT
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named CoCASLFORMULA -> CoCASLFORMULA
forall s a. SenAttr s a -> s
sentence) [Named CoCASLFORMULA]
sens
            e :: CSign
e = Set SORT -> CSign -> CSign
forall f e. Set SORT -> Sign f e -> Sign f e
encodeSig Set SORT
bsrts CSign
sig
            sens1 :: [SenAttr (FORMULA f) String]
sens1 = (Named CoCASLFORMULA -> SenAttr (FORMULA f) String)
-> [Named CoCASLFORMULA] -> [SenAttr (FORMULA f) String]
forall a b. (a -> b) -> [a] -> [b]
map ((CoCASLFORMULA -> FORMULA f)
-> Named CoCASLFORMULA -> SenAttr (FORMULA f) String
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed CoCASLFORMULA -> FORMULA f
forall f1 f. FORMULA f1 -> FORMULA f
mapFORMULA) ([Named CoCASLFORMULA] -> [SenAttr (FORMULA f) String])
-> [Named CoCASLFORMULA] -> [SenAttr (FORMULA f) String]
forall a b. (a -> b) -> a -> b
$ Bool -> Set SORT -> CSign -> [Named CoCASLFORMULA]
forall f e.
(Ord f, TermExtension f) =>
Bool -> Set SORT -> Sign f e -> [Named (FORMULA f)]
generateAxioms
                    (CASL2SubCFOL -> Bool
uniqueBottom CASL2SubCFOL
defaultCASL2SubCFOL) Set SORT
bsrts CSign
sig
            sens2 :: [Named CoCASLFORMULA]
sens2 = (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 ((C_FORMULA -> C_FORMULA) -> CoCASLFORMULA -> CoCASLFORMULA
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula C_FORMULA -> C_FORMULA
simC_FORMULA
                                   (CoCASLFORMULA -> CoCASLFORMULA)
-> (CoCASLFORMULA -> CoCASLFORMULA)
-> CoCASLFORMULA
-> CoCASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SORT -> CoCASLFORMULA -> CoCASLFORMULA
codeCoFormula Set SORT
bsrts)) [Named CoCASLFORMULA]
sens
        in (CSign, [Named CoCASLFORMULA])
-> Result (CSign, [Named CoCASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CSign
e, [Named CoCASLFORMULA] -> [Named CoCASLFORMULA]
forall a. [Named a] -> [Named a]
nameAndDisambiguate ([Named CoCASLFORMULA] -> [Named CoCASLFORMULA])
-> [Named CoCASLFORMULA] -> [Named CoCASLFORMULA]
forall a b. (a -> b) -> a -> b
$ [Named CoCASLFORMULA]
forall f. [SenAttr (FORMULA f) String]
sens1 [Named CoCASLFORMULA]
-> [Named CoCASLFORMULA] -> [Named CoCASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CoCASLFORMULA]
sens2)
    map_morphism :: CoCASL2CoSubCFOL -> CoCASLMor -> Result CoCASLMor
map_morphism CoCASL2CoSubCFOL mor :: CoCASLMor
mor@Morphism {msource :: forall f e m. Morphism f e m -> Sign f e
msource = CSign
src, mtarget :: forall f e m. Morphism f e m -> Sign f e
mtarget = CSign
tar} =
        let mkBSrts :: Sign f e -> Set SORT
mkBSrts s :: Sign f e
s = FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
sortsWithBottom
              (CASL2SubCFOL -> FormulaTreatment
formulaTreatment CASL2SubCFOL
defaultCASL2SubCFOL) Sign f e
s Set SORT
forall a. Set a
Set.empty
        in CoCASLMor -> Result CoCASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return CoCASLMor
mor
            { msource :: CSign
msource = Set SORT -> CSign -> CSign
forall f e. Set SORT -> Sign f e -> Sign f e
encodeSig (CSign -> Set SORT
forall f e. Sign f e -> Set SORT
mkBSrts CSign
src) CSign
src
            , mtarget :: CSign
mtarget = Set SORT -> CSign -> CSign
forall f e. Set SORT -> Sign f e -> Sign f e
encodeSig (CSign -> Set SORT
forall f e. Sign f e -> Set SORT
mkBSrts CSign
tar) CSign
tar
            , op_map :: Op_map
op_map = ((SORT, OpKind) -> (SORT, OpKind)) -> Op_map -> Op_map
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ (i :: SORT
i, _) -> (SORT
i, OpKind
Total)) (Op_map -> Op_map) -> Op_map -> Op_map
forall a b. (a -> b) -> a -> b
$ CoCASLMor -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map CoCASLMor
mor }
    map_sentence :: CoCASL2CoSubCFOL -> CSign -> CoCASLFORMULA -> Result CoCASLFORMULA
map_sentence CoCASL2CoSubCFOL sig :: CSign
sig sen :: CoCASLFORMULA
sen =
        CoCASLFORMULA -> Result CoCASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CoCASLFORMULA -> Result CoCASLFORMULA)
-> CoCASLFORMULA -> Result CoCASLFORMULA
forall a b. (a -> b) -> a -> b
$ (C_FORMULA -> C_FORMULA) -> CoCASLFORMULA -> CoCASLFORMULA
forall f. Ord f => (f -> f) -> FORMULA f -> FORMULA f
simplifyFormula C_FORMULA -> C_FORMULA
simC_FORMULA (CoCASLFORMULA -> CoCASLFORMULA) -> CoCASLFORMULA -> CoCASLFORMULA
forall a b. (a -> b) -> a -> b
$ Set SORT -> CoCASLFORMULA -> CoCASLFORMULA
codeCoFormula
           (FormulaTreatment -> CSign -> Set SORT -> Set SORT
forall f e. FormulaTreatment -> Sign f e -> Set SORT -> Set SORT
sortsWithBottom (CASL2SubCFOL -> FormulaTreatment
formulaTreatment CASL2SubCFOL
defaultCASL2SubCFOL)
            CSign
sig (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ CoCASLFORMULA -> Set SORT
botCoFormulaSorts CoCASLFORMULA
sen) CoCASLFORMULA
sen
    map_symbol :: CoCASL2CoSubCFOL -> CSign -> Symbol -> Set Symbol
map_symbol CoCASL2CoSubCFOL _ s :: Symbol
s =
        Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton Symbol
s {symbType :: SymbType
symbType = SymbType -> SymbType
totalizeSymbType (SymbType -> SymbType) -> SymbType -> SymbType
forall a b. (a -> b) -> a -> b
$ Symbol -> SymbType
symbType Symbol
s}
    has_model_expansion :: CoCASL2CoSubCFOL -> Bool
has_model_expansion CoCASL2CoSubCFOL = Bool
True
    is_weakly_amalgamable :: CoCASL2CoSubCFOL -> Bool
is_weakly_amalgamable CoCASL2CoSubCFOL = Bool
True

codeCoRecord :: Set.Set SORT
             -> Record C_FORMULA (FORMULA C_FORMULA) (TERM C_FORMULA)
codeCoRecord :: Set SORT -> Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA)
codeCoRecord bsrts :: Set SORT
bsrts =
    Bool
-> Set SORT
-> (C_FORMULA -> C_FORMULA)
-> Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA)
forall f.
TermExtension f =>
Bool -> Set SORT -> (f -> f) -> Record f (FORMULA f) (TERM f)
codeRecord (CASL2SubCFOL -> Bool
uniqueBottom CASL2SubCFOL
defaultCASL2SubCFOL) Set SORT
bsrts ((C_FORMULA -> C_FORMULA)
 -> Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA))
-> (C_FORMULA -> C_FORMULA)
-> Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA)
forall a b. (a -> b) -> a -> b
$ Set SORT -> C_FORMULA -> C_FORMULA
codeC_FORMULA Set SORT
bsrts

codeCoFormula :: Set.Set SORT -> FORMULA C_FORMULA -> FORMULA C_FORMULA
codeCoFormula :: Set SORT -> CoCASLFORMULA -> CoCASLFORMULA
codeCoFormula = Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA)
-> CoCASLFORMULA -> CoCASLFORMULA
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA)
 -> CoCASLFORMULA -> CoCASLFORMULA)
-> (Set SORT -> Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA))
-> Set SORT
-> CoCASLFORMULA
-> CoCASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SORT -> Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA)
codeCoRecord

codeC_FORMULA :: Set.Set SORT -> C_FORMULA -> C_FORMULA
codeC_FORMULA :: Set SORT -> C_FORMULA -> C_FORMULA
codeC_FORMULA bsrts :: Set SORT
bsrts = 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 (Set SORT -> Record C_FORMULA CoCASLFORMULA (TERM C_FORMULA)
codeCoRecord Set SORT
bsrts) CoRecord CoCASLFORMULA (TERM C_FORMULA) C_FORMULA MODALITY
mapCoRecord
  {foldCoSort_gen_ax :: C_FORMULA -> [SORT] -> [OP_SYMB] -> Bool -> C_FORMULA
foldCoSort_gen_ax = \ _ s :: [SORT]
s o :: [OP_SYMB]
o b :: Bool
b -> [SORT] -> [OP_SYMB] -> Bool -> C_FORMULA
CoSort_gen_ax [SORT]
s ((OP_SYMB -> OP_SYMB) -> [OP_SYMB] -> [OP_SYMB]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> OP_SYMB
totalizeOpSymb [OP_SYMB]
o) Bool
b}

simC_FORMULA :: C_FORMULA -> C_FORMULA
simC_FORMULA :: C_FORMULA -> C_FORMULA
simC_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. Ord f => (f -> f) -> Record f (FORMULA f) (TERM f)
simplifyRecord C_FORMULA -> C_FORMULA
simC_FORMULA) CoRecord CoCASLFORMULA (TERM C_FORMULA) C_FORMULA MODALITY
mapCoRecord

botCoSorts :: C_FORMULA -> Set.Set SORT
botCoSorts :: C_FORMULA -> Set SORT
botCoSorts =
    Record C_FORMULA (Set SORT) (Set SORT)
-> CoRecord (Set SORT) (Set SORT) (Set SORT) (Set SORT)
-> C_FORMULA
-> Set SORT
forall a b c d.
Record C_FORMULA a b -> CoRecord a b c d -> C_FORMULA -> c
foldC_Formula ((C_FORMULA -> Set SORT) -> Record C_FORMULA (Set SORT) (Set SORT)
forall f. (f -> Set SORT) -> Record f (Set SORT) (Set SORT)
botSorts C_FORMULA -> Set SORT
botCoSorts) (([Set SORT] -> Set SORT)
-> Set SORT -> CoRecord (Set SORT) (Set SORT) (Set SORT) (Set SORT)
forall a. ([a] -> a) -> a -> CoRecord a a a a
constCoRecord [Set SORT] -> Set SORT
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions Set SORT
forall a. Set a
Set.empty)

botCoFormulaSorts :: FORMULA C_FORMULA -> Set.Set SORT
botCoFormulaSorts :: CoCASLFORMULA -> Set SORT
botCoFormulaSorts = Record C_FORMULA (Set SORT) (Set SORT) -> CoCASLFORMULA -> Set SORT
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record C_FORMULA (Set SORT) (Set SORT)
 -> CoCASLFORMULA -> Set SORT)
-> Record C_FORMULA (Set SORT) (Set SORT)
-> CoCASLFORMULA
-> Set SORT
forall a b. (a -> b) -> a -> b
$ (C_FORMULA -> Set SORT) -> Record C_FORMULA (Set SORT) (Set SORT)
forall f. (f -> Set SORT) -> Record f (Set SORT) (Set SORT)
botSorts C_FORMULA -> Set SORT
botCoSorts