{-# 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 Int -> CASL2PCFOL -> ShowS
[CASL2PCFOL] -> ShowS
CASL2PCFOL -> String
(Int -> CASL2PCFOL -> ShowS)
-> (CASL2PCFOL -> String)
-> ([CASL2PCFOL] -> ShowS)
-> Show CASL2PCFOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2PCFOL] -> ShowS
$cshowList :: [CASL2PCFOL] -> ShowS
show :: CASL2PCFOL -> String
$cshow :: CASL2PCFOL -> String
showsPrec :: Int -> CASL2PCFOL -> ShowS
$cshowsPrec :: Int -> CASL2PCFOL -> ShowS
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
sourceLogic CASL2PCFOL = CASL
CASL
    sourceSublogic :: CASL2PCFOL -> CASL_Sublogics
sourceSublogic CASL2PCFOL = CASL_Sublogics
forall a. Lattice a => CASL_SL a
Sublogic.caslTop
    targetLogic :: CASL2PCFOL -> CASL
targetLogic CASL2PCFOL = CASL
CASL
    mapSublogic :: CASL2PCFOL -> CASL_Sublogics -> Maybe CASL_Sublogics
mapSublogic CASL2PCFOL sl :: CASL_Sublogics
sl = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just (CASL_Sublogics -> Maybe CASL_Sublogics)
-> CASL_Sublogics -> Maybe CASL_Sublogics
forall a b. (a -> b) -> a -> b
$
                                if CASL_Sublogics -> Bool
forall a. CASL_SL a -> Bool
has_sub CASL_Sublogics
sl then -- subsorting is coded out
                                      CASL_Sublogics
sl { sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
NoSub
                                         , has_part :: Bool
has_part = 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
$ CASL_Sublogics -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
which_logic CASL_Sublogics
sl
                                         , has_eq :: Bool
has_eq = Bool
True}
                                  else CASL_Sublogics
sl
    map_theory :: CASL2PCFOL
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory CASL2PCFOL = (CASLSign -> Result (CASLSign, [Named CASLFORMULA]))
-> (CASLSign -> CASLFORMULA -> Result CASLFORMULA)
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
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 :: CASLSign
sig ->
      let e :: CASLSign
e = CASLSign -> CASLSign
forall f e. Sign f e -> Sign f e
encodeSig CASLSign
sig in
      (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign
e, (Named CASLFORMULA -> Named CASLFORMULA)
-> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((CASLFORMULA -> CASLFORMULA)
-> Named CASLFORMULA -> Named CASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((CASLFORMULA -> CASLFORMULA)
 -> Named CASLFORMULA -> Named CASLFORMULA)
-> (CASLFORMULA -> CASLFORMULA)
-> Named CASLFORMULA
-> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (() -> ()) -> CASLFORMULA -> CASLFORMULA
forall f. TermExtension f => (f -> f) -> FORMULA f -> FORMULA f
injFormula () -> ()
forall a. a -> a
id) (CASLSign -> [Named CASLFORMULA]
forall f e. Sign f e -> [Named (FORMULA f)]
monotonicities CASLSign
sig)
                 [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ CASLSign -> [Named CASLFORMULA]
forall f e. TermExtension f => Sign f e -> [Named (FORMULA f)]
generateAxioms CASLSign
sig))
      (CASL2PCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA
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 CASL2PCFOL
CASL2PCFOL)
    map_morphism :: CASL2PCFOL -> CASLMor -> Result CASLMor
map_morphism CASL2PCFOL mor :: CASLMor
mor = CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return
      (CASLMor
mor { msource :: CASLSign
msource = CASLSign -> CASLSign
forall f e. Sign f e -> Sign f e
encodeSig (CASLSign -> CASLSign) -> CASLSign -> CASLSign
forall a b. (a -> b) -> a -> b
$ CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
msource CASLMor
mor,
              mtarget :: CASLSign
mtarget = CASLSign -> CASLSign
forall f e. Sign f e -> Sign f e
encodeSig (CASLSign -> CASLSign) -> CASLSign -> CASLSign
forall a b. (a -> b) -> a -> b
$ CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
mtarget CASLMor
mor })
      -- other components need not to be adapted!
    map_sentence :: CASL2PCFOL -> CASLSign -> CASLFORMULA -> Result CASLFORMULA
map_sentence CASL2PCFOL _ = CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> (CASLFORMULA -> CASLFORMULA)
-> CASLFORMULA
-> Result CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> CASLFORMULA
forall f. TermExtension f => FORMULA f -> FORMULA f
f2Formula
    map_symbol :: CASL2PCFOL -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2PCFOL _ = 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 :: CASL2PCFOL -> Bool
has_model_expansion CASL2PCFOL = Bool
True
    is_weakly_amalgamable :: CASL2PCFOL -> Bool
is_weakly_amalgamable CASL2PCFOL = Bool
True

-- | Add injection, projection and membership symbols to a signature
encodeSig :: Sign f e -> Sign f e
encodeSig :: Sign f e -> Sign f e
encodeSig sig :: Sign f e
sig
  = if Rel SORT -> Bool
forall a. Ord a => Rel a -> Bool
Rel.noPairs Rel SORT
rel then Sign f e
sig else
      Sign f e
sig {sortRel :: Rel SORT
sortRel = Set SORT -> Rel SORT
forall a. Ord a => Set a -> Rel a
Rel.fromKeysSet (Set SORT -> Rel SORT) -> Set SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
sig, opMap :: OpMap
opMap = OpMap
projOpMap}
  where
        rel :: Rel SORT
rel = Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.irreflex (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sig
        relSet :: Set (SORT, SORT)
relSet = Rel SORT -> Set (SORT, SORT)
forall a. Ord a => Rel a -> Set (a, a)
Rel.toSet Rel SORT
rel
        total :: (SORT, SORT) -> OpType
total (s :: SORT
s, s' :: SORT
s') = [SORT] -> SORT -> OpType
mkTotOpType [SORT
s] SORT
s'
        partial :: (SORT, SORT) -> OpType
partial (s :: SORT
s, s' :: SORT
s') = (if SORT -> SORT -> Rel SORT -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.member SORT
s' SORT
s Rel SORT
rel then OpType -> OpType
forall a. a -> a
id else OpType -> OpType
mkPartial)
          (OpType -> OpType) -> OpType -> OpType
forall a b. (a -> b) -> a -> b
$ (SORT, SORT) -> OpType
total (SORT
s', SORT
s)
        setinjOptype :: Set OpType
setinjOptype = ((SORT, SORT) -> OpType) -> Set (SORT, SORT) -> Set OpType
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (SORT, SORT) -> OpType
total Set (SORT, SORT)
relSet
        setprojOptype :: Set OpType
setprojOptype = ((SORT, SORT) -> OpType) -> Set (SORT, SORT) -> Set OpType
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (SORT, SORT) -> OpType
partial Set (SORT, SORT)
relSet
        injOpMap :: OpMap
injOpMap = (OpType -> OpMap -> OpMap) -> OpMap -> Set OpType -> OpMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ t :: OpType
t -> SORT -> OpType -> OpMap -> OpMap
addOpTo (OP_TYPE -> SORT
uniqueInjName (OP_TYPE -> SORT) -> OP_TYPE -> SORT
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
t) OpType
t)
          (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
sig) Set OpType
setinjOptype
        projOpMap :: OpMap
projOpMap = (OpType -> OpMap -> OpMap) -> OpMap -> Set OpType -> OpMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ t :: OpType
t -> SORT -> OpType -> OpMap -> OpMap
addOpTo (OP_TYPE -> SORT
uniqueProjName (OP_TYPE -> SORT) -> OP_TYPE -> SORT
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
t) OpType
t)
          OpMap
injOpMap Set OpType
setprojOptype
    -- membership predicates are coded out

-- | Make the name for the embedding or projecton injectivity axiom
mkInjectivityName :: String -> SORT -> SORT -> String
mkInjectivityName :: String -> SORT -> SORT -> String
mkInjectivityName = String -> SORT -> SORT -> String
mkAxName (String -> SORT -> SORT -> String)
-> ShowS -> String -> SORT -> SORT -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_injectivity")

-- | Make the name for the embedding injectivity axiom
mkEmbInjName :: SORT -> SORT -> String
mkEmbInjName :: SORT -> SORT -> String
mkEmbInjName = String -> SORT -> SORT -> String
mkInjectivityName "embedding"

-- | Make the name for the projection injectivity axiom
mkProjInjName :: SORT -> SORT -> String
mkProjInjName :: SORT -> SORT -> String
mkProjInjName = String -> SORT -> SORT -> String
mkInjectivityName "projection"

-- | create a quantified injectivity implication
mkInjectivity :: (TERM f -> TERM f) -> VAR_DECL -> VAR_DECL -> FORMULA f
mkInjectivity :: (TERM f -> TERM f) -> VAR_DECL -> VAR_DECL -> FORMULA f
mkInjectivity f :: TERM f -> TERM f
f vx :: VAR_DECL
vx vy :: VAR_DECL
vy =
  [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
vx, VAR_DECL
vy] (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ (TERM f -> TERM f) -> TERM f -> TERM f -> FORMULA f
forall f. (TERM f -> TERM f) -> TERM f -> TERM f -> FORMULA f
mkInjImpl TERM f -> TERM f
f (VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vx) (TERM f -> FORMULA f) -> TERM f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vy

-- | create an injectivity implication over x and y
mkInjImpl :: (TERM f -> TERM f) -> TERM f -> TERM f -> FORMULA f
mkInjImpl :: (TERM f -> TERM f) -> TERM f -> TERM f -> FORMULA f
mkInjImpl f :: TERM f -> TERM f
f x :: TERM f
x y :: TERM f
y = FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl (TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkExEq (TERM f -> TERM f
f TERM f
x) (TERM f -> TERM f
f TERM f
y)) (TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkExEq TERM f
x TERM f
y)

-- | apply injection function
injectTo :: TermExtension f => SORT -> TERM f -> TERM f
injectTo :: SORT -> TERM f -> TERM f
injectTo s :: SORT
s q :: TERM f
q = Range -> TERM f -> SORT -> TERM f
forall f. TermExtension f => Range -> TERM f -> SORT -> TERM f
injectUnique Range
nullRange TERM f
q SORT
s

-- | apply (a partial) projection function
projectTo :: TermExtension f => SORT -> TERM f -> TERM f
projectTo :: SORT -> TERM f -> TERM f
projectTo s :: SORT
s q :: TERM f
q = OpKind -> Range -> TERM f -> SORT -> TERM f
forall f.
TermExtension f =>
OpKind -> Range -> TERM f -> SORT -> TERM f
projectUnique OpKind
Partial Range
nullRange TERM f
q SORT
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 :: SORT -> SORT -> Named (FORMULA f)
mkEmbInjAxiom s :: SORT
s s' :: SORT
s' =
    String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed (SORT -> SORT -> String
mkEmbInjName SORT
s SORT
s')
      (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ (TERM f -> TERM f) -> VAR_DECL -> VAR_DECL -> FORMULA f
forall f. (TERM f -> TERM f) -> VAR_DECL -> VAR_DECL -> FORMULA f
mkInjectivity (SORT -> TERM f -> TERM f
forall f. TermExtension f => SORT -> TERM f -> TERM f
injectTo SORT
s') (String -> SORT -> VAR_DECL
mkVarDeclStr "x" SORT
s) (VAR_DECL -> FORMULA f) -> VAR_DECL -> FORMULA f
forall a b. (a -> b) -> a -> b
$ String -> SORT -> VAR_DECL
mkVarDeclStr "y" SORT
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 :: SORT -> SORT -> Named (FORMULA f)
mkProjInjAxiom s :: SORT
s s' :: SORT
s' =
    String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed (SORT -> SORT -> String
mkProjInjName SORT
s' SORT
s)
      (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ (TERM f -> TERM f) -> VAR_DECL -> VAR_DECL -> FORMULA f
forall f. (TERM f -> TERM f) -> VAR_DECL -> VAR_DECL -> FORMULA f
mkInjectivity (SORT -> TERM f -> TERM f
forall f. TermExtension f => SORT -> TERM f -> TERM f
projectTo SORT
s) (String -> SORT -> VAR_DECL
mkVarDeclStr "x" SORT
s') (VAR_DECL -> FORMULA f) -> VAR_DECL -> FORMULA f
forall a b. (a -> b) -> a -> b
$ String -> SORT -> VAR_DECL
mkVarDeclStr "y" SORT
s'

-- | Make the name for the projection axiom
mkProjName :: SORT -> SORT -> String
mkProjName :: SORT -> SORT -> String
mkProjName = String -> SORT -> SORT -> String
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 :: SORT -> (TERM f -> TERM f) -> (TERM f -> TERM f) -> FORMULA f
mkXExEq s :: SORT
s fl :: TERM f -> TERM f
fl fr :: TERM f -> TERM f
fr = let
  vx :: VAR_DECL
vx = String -> SORT -> VAR_DECL
mkVarDeclStr "x" SORT
s
  qualX :: TERM f
qualX = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
vx
  in [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
vx] (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkExEq (TERM f -> TERM f
fl TERM f
forall f. TERM f
qualX) (TERM f -> TERM f
fr TERM f
forall f. TERM f
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 :: SORT -> SORT -> Named (FORMULA f)
mkProjAxiom s :: SORT
s s' :: SORT
s' = String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed (SORT -> SORT -> String
mkProjName SORT
s' SORT
s)
    (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ SORT -> (TERM f -> TERM f) -> (TERM f -> TERM f) -> FORMULA f
forall f.
SORT -> (TERM f -> TERM f) -> (TERM f -> TERM f) -> FORMULA f
mkXExEq SORT
s (SORT -> TERM f -> TERM f
forall f. TermExtension f => SORT -> TERM f -> TERM f
projectTo SORT
s (TERM f -> TERM f) -> (TERM f -> TERM f) -> TERM f -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> TERM f -> TERM f
forall f. TermExtension f => SORT -> TERM f -> TERM f
injectTo SORT
s') TERM f -> TERM f
forall a. a -> a
id

-- | Make the name for the transitivity axiom from s to s' to s''
mkTransAxiomName :: SORT -> SORT -> SORT -> String
mkTransAxiomName :: SORT -> SORT -> SORT -> String
mkTransAxiomName s :: SORT
s s' :: SORT
s' s'' :: SORT
s'' =
  String -> SORT -> SORT -> String
mkAxName "transitivity" SORT
s SORT
s' String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_to_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SORT -> String
forall a. Show a => a -> String
show SORT
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 :: SORT -> SORT -> SORT -> Named (FORMULA f)
mkTransAxiom s :: SORT
s s' :: SORT
s' s'' :: SORT
s'' = String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed (SORT -> SORT -> SORT -> String
mkTransAxiomName SORT
s SORT
s' SORT
s'')
    (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ SORT -> (TERM f -> TERM f) -> (TERM f -> TERM f) -> FORMULA f
forall f.
SORT -> (TERM f -> TERM f) -> (TERM f -> TERM f) -> FORMULA f
mkXExEq SORT
s (SORT -> TERM f -> TERM f
forall f. TermExtension f => SORT -> TERM f -> TERM f
injectTo SORT
s'' (TERM f -> TERM f) -> (TERM f -> TERM f) -> TERM f -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> TERM f -> TERM f
forall f. TermExtension f => SORT -> TERM f -> TERM f
injectTo SORT
s') ((TERM f -> TERM f) -> FORMULA f)
-> (TERM f -> TERM f) -> FORMULA f
forall a b. (a -> b) -> a -> b
$ SORT -> TERM f -> TERM f
forall f. TermExtension f => SORT -> TERM f -> TERM f
injectTo SORT
s''

-- | Make the name for the identity axiom from s to s'
mkIdAxiomName :: SORT -> SORT -> String
mkIdAxiomName :: SORT -> SORT -> String
mkIdAxiomName = String -> SORT -> SORT -> String
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 :: SORT -> SORT -> Named (FORMULA f)
mkIdAxiom s :: SORT
s s' :: SORT
s' = String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed (SORT -> SORT -> String
mkIdAxiomName SORT
s SORT
s')
    (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ SORT -> (TERM f -> TERM f) -> (TERM f -> TERM f) -> FORMULA f
forall f.
SORT -> (TERM f -> TERM f) -> (TERM f -> TERM f) -> FORMULA f
mkXExEq SORT
s (SORT -> TERM f -> TERM f
forall f. TermExtension f => SORT -> TERM f -> TERM f
injectTo SORT
s (TERM f -> TERM f) -> (TERM f -> TERM f) -> TERM f -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> TERM f -> TERM f
forall f. TermExtension f => SORT -> TERM f -> TERM f
injectTo SORT
s') TERM f -> TERM f
forall a. a -> a
id

generateAxioms :: TermExtension f => Sign f e -> [Named (FORMULA f)]
generateAxioms :: Sign f e -> [Named (FORMULA f)]
generateAxioms sig :: Sign f e
sig = (SORT -> [Named (FORMULA f)]) -> [SORT] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ s :: SORT
s ->
    (SORT -> [Named (FORMULA f)]) -> [SORT] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ s' :: SORT
s' ->
      [SORT -> SORT -> Named (FORMULA f)
forall f. TermExtension f => SORT -> SORT -> Named (FORMULA f)
mkIdAxiom SORT
s SORT
s' | SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
s (Set SORT -> Bool) -> Set SORT -> Bool
forall a b. (a -> b) -> a -> b
$ SORT -> Sign f e -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
s' Sign f e
sig ]
      [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ SORT -> SORT -> Named (FORMULA f)
forall f. TermExtension f => SORT -> SORT -> Named (FORMULA f)
mkEmbInjAxiom SORT
s SORT
s' Named (FORMULA f) -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. a -> [a] -> [a]
: SORT -> SORT -> Named (FORMULA f)
forall f. TermExtension f => SORT -> SORT -> Named (FORMULA f)
mkProjInjAxiom SORT
s SORT
s' Named (FORMULA f) -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. a -> [a] -> [a]
: SORT -> SORT -> Named (FORMULA f)
forall f. TermExtension f => SORT -> SORT -> Named (FORMULA f)
mkProjAxiom SORT
s SORT
s'
      Named (FORMULA f) -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. a -> [a] -> [a]
: (SORT -> Named (FORMULA f)) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (SORT -> SORT -> SORT -> Named (FORMULA f)
forall f.
TermExtension f =>
SORT -> SORT -> SORT -> Named (FORMULA f)
mkTransAxiom SORT
s SORT
s') ((SORT -> Bool) -> [SORT] -> [SORT]
forall a. (a -> Bool) -> [a] -> [a]
filter (SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
/= SORT
s) ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ SORT -> [SORT]
realSupers SORT
s'))
    ([SORT] -> [Named (FORMULA f)]) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> a -> b
$ SORT -> [SORT]
realSupers SORT
s) ([SORT] -> [Named (FORMULA f)]) -> [SORT] -> [Named (FORMULA f)]
forall a b. (a -> b) -> a -> b
$ Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
sig
    where
        realSupers :: SORT -> [SORT]
realSupers so :: SORT
so = Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ SORT -> Sign f e -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
so Sign f e
sig

f2Formula :: TermExtension f => FORMULA f -> FORMULA f
f2Formula :: FORMULA f -> FORMULA f
f2Formula = OpKind -> (f -> f) -> FORMULA f -> FORMULA f
forall f.
TermExtension f =>
OpKind -> (f -> f) -> FORMULA f -> FORMULA f
projFormula OpKind
Partial f -> f
forall a. a -> a
id (FORMULA f -> FORMULA f)
-> (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> f) -> FORMULA f -> FORMULA f
forall f. TermExtension f => (f -> f) -> FORMULA f -> FORMULA f
injFormula f -> f
forall a. a -> a
id

t2Term :: TermExtension f => TERM f -> TERM f
t2Term :: TERM f -> TERM f
t2Term = OpKind -> (f -> f) -> TERM f -> TERM f
forall f. TermExtension f => OpKind -> (f -> f) -> TERM f -> TERM f
projTerm OpKind
Partial f -> f
forall a. a -> a
id (TERM f -> TERM f) -> (TERM f -> TERM f) -> TERM f -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> f) -> TERM f -> TERM f
forall f. TermExtension f => (f -> f) -> TERM f -> TERM f
injTerm f -> f
forall a. a -> a
id