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

{- |

Module : ./Comorphisms/CASL2PCFOL.hs

Description : coding out subsorting

Copyright : (c) Zicheng Wang, Liam O'Reilly, C. Maeder Uni Bremen 2002-2009

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : non-portable (imports Logic.Logic)

Coding out subsorting (SubPCFOL= -> PCFOL=),

following Chap. III:3.1 of the CASL Reference Manual

-}

module Comorphisms.CASL2PCFOL where

import Logic.Logic

import Logic.Comorphism

import qualified Data.Set as Set

import qualified Common.Lib.Rel as Rel

import Common.AS_Annotation

import Common.Id

import Common.ProofTree

-- CASL

import CASL.Logic_CASL

import CASL.AS_Basic_CASL

import CASL.Sign

import CASL.Morphism

import CASL.Sublogic as Sublogic

import CASL.Inject

import CASL.Project

import CASL.Monoton

-- | The identity of the comorphism

data CASL2PCFOL = CASL2PCFOL deriving Show

instance Language CASL2PCFOL -- default definition is okay

instance Comorphism CASL2PCFOL

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree

CASL CASL_Sublogics

CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

CASLSign

CASLMor

Symbol RawSymbol ProofTree where

sourceLogic CASL2PCFOL = CASL

sourceSublogic CASL2PCFOL = Sublogic.caslTop

targetLogic CASL2PCFOL = CASL

mapSublogic CASL2PCFOL sl = Just $

if has_sub sl then -- subsorting is coded out

sl { sub_features = NoSub

, has_part = True

, which_logic = max Horn

$ which_logic sl

, has_eq = True}

else sl

map_theory CASL2PCFOL = mkTheoryMapping ( \ sig ->

let e = encodeSig sig in

return (e, map (mapNamed $ injFormula id) (monotonicities sig)

++ generateAxioms sig))

(map_sentence CASL2PCFOL)

map_morphism CASL2PCFOL mor = return

(mor { msource = encodeSig $ msource mor,

mtarget = encodeSig $ mtarget mor })

-- other components need not to be adapted!

map_sentence CASL2PCFOL _ = return . f2Formula

map_symbol CASL2PCFOL _ = Set.singleton . id

has_model_expansion CASL2PCFOL = True

is_weakly_amalgamable CASL2PCFOL = True

-- | Add injection, projection and membership symbols to a signature

encodeSig :: Sign f e -> Sign f e

encodeSig sig

= if Rel.noPairs rel then sig else

sig {sortRel = Rel.fromKeysSet $ sortSet sig, opMap = projOpMap}

where

rel = Rel.irreflex $ sortRel sig

relSet = Rel.toSet rel

total (s, s') = mkTotOpType [s] s'

partial (s, s') = (if Rel.member s' s rel then id else mkPartial)

$ total (s', s)

setinjOptype = Set.map total relSet

setprojOptype = Set.map partial relSet

injOpMap = Set.fold (\ t -> addOpTo (uniqueInjName $ toOP_TYPE t) t)

(opMap sig) setinjOptype

projOpMap = Set.fold (\ t -> addOpTo (uniqueProjName $ toOP_TYPE t) t)

injOpMap setprojOptype

-- membership predicates are coded out

-- | Make the name for the embedding or projecton injectivity axiom

mkInjectivityName :: String -> SORT -> SORT -> String

mkInjectivityName = mkAxName . (++ "_injectivity")

-- | Make the name for the embedding injectivity axiom

mkEmbInjName :: SORT -> SORT -> String

mkEmbInjName = mkInjectivityName "embedding"

-- | Make the name for the projection injectivity axiom

mkProjInjName :: SORT -> SORT -> String

mkProjInjName = mkInjectivityName "projection"

-- | create a quantified injectivity implication

mkInjectivity :: (TERM f -> TERM f) -> VAR_DECL -> VAR_DECL -> FORMULA f

mkInjectivity f vx vy =

mkForall [vx, vy] $ mkInjImpl f (toQualVar vx) $ toQualVar vy

-- | create an injectivity implication over x and y

mkInjImpl :: (TERM f -> TERM f) -> TERM f -> TERM f -> FORMULA f

mkInjImpl f x y = mkImpl (mkExEq (f x) (f y)) (mkExEq x y)

-- | apply injection function

injectTo :: TermExtension f => SORT -> TERM f -> TERM f

injectTo s q = injectUnique nullRange q s

-- | apply (a partial) projection function

projectTo :: TermExtension f => SORT -> TERM f -> TERM f

projectTo s q = projectUnique Partial nullRange q s

{- | Make the named sentence for the embedding injectivity axiom from s to s'

i.e., forall x,y:s . inj(x)=e=inj(y) => x=e=y -}

mkEmbInjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f)

mkEmbInjAxiom s s' =

makeNamed (mkEmbInjName s s')

$ mkInjectivity (injectTo s') (mkVarDeclStr "x" s) $ mkVarDeclStr "y" s

{- | Make the named sentence for the projection injectivity axiom from s' to s

i.e., forall x,y:s . pr(x)=e=pr(y) => x=e=y -}

mkProjInjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f)

mkProjInjAxiom s s' =

makeNamed (mkProjInjName s' s)

$ mkInjectivity (projectTo s) (mkVarDeclStr "x" s') $ mkVarDeclStr "y" s'

-- | Make the name for the projection axiom

mkProjName :: SORT -> SORT -> String

mkProjName = mkAxName "projection"

-- | create a quantified existential equation over x of sort s

mkXExEq :: SORT -> (TERM f -> TERM f) -> (TERM f -> TERM f) -> FORMULA f

mkXExEq s fl fr = let

vx = mkVarDeclStr "x" s

qualX = toQualVar vx

in mkForall [vx] $ mkExEq (fl qualX) (fr qualX)

{- | Make the named sentence for the projection axiom from s' to s

i.e., forall x:s . pr(inj(x))=e=x -}

mkProjAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f)

mkProjAxiom s s' = makeNamed (mkProjName s' s)

$ mkXExEq s (projectTo s . injectTo s') id

-- | Make the name for the transitivity axiom from s to s' to s''

mkTransAxiomName :: SORT -> SORT -> SORT -> String

mkTransAxiomName s s' s'' =

mkAxName "transitivity" s s' ++ "_to_" ++ show s''

{- | Make the named sentence for the transitivity axiom from s to s' to s''

i.e., forall x:s . inj(inj(x))=e=inj(x) -}

mkTransAxiom :: TermExtension f => SORT -> SORT -> SORT -> Named (FORMULA f)

mkTransAxiom s s' s'' = makeNamed (mkTransAxiomName s s' s'')

$ mkXExEq s (injectTo s'' . injectTo s') $ injectTo s''

-- | Make the name for the identity axiom from s to s'

mkIdAxiomName :: SORT -> SORT -> String

mkIdAxiomName = mkAxName "identity"

{- | Make the named sentence for the identity axiom from s to s'

i.e., forall x:s . inj(inj(x))=e=x -}

mkIdAxiom :: TermExtension f => SORT -> SORT -> Named (FORMULA f)

mkIdAxiom s s' = makeNamed (mkIdAxiomName s s')

$ mkXExEq s (injectTo s . injectTo s') id

generateAxioms :: TermExtension f => Sign f e -> [Named (FORMULA f)]

generateAxioms sig = concatMap (\ s ->

concatMap (\ s' ->

[mkIdAxiom s s' | Set.member s $ supersortsOf s' sig ]

++ mkEmbInjAxiom s s' : mkProjInjAxiom s s' : mkProjAxiom s s'

: map (mkTransAxiom s s') (filter (/= s) $ realSupers s'))

$ realSupers s) $ Set.toList $ sortSet sig

where

realSupers so = Set.toList $ supersortsOf so sig

f2Formula :: TermExtension f => FORMULA f -> FORMULA f

f2Formula = projFormula Partial id . injFormula id

t2Term :: TermExtension f => TERM f -> TERM f

t2Term = projTerm Partial id . injTerm id