{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances
  , FlexibleInstances #-}
{- |
Module      :  ./CASL/Logic_CASL.hs
Description :  Instance of class Logic for the CASL logic
Copyright   :  (c) Klaus Luettich, Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

Instance of class Logic for the CASL logic
   Also the instances for Syntax and Category.
-}

module CASL.Logic_CASL where

import ATC.ProofTree ()

import CASL.AS_Basic_CASL
import CASL.Parse_AS_Basic
import CASL.Kif
import CASL.Kif2CASL
import CASL.Fold
import CASL.ToDoc
import CASL.ToItem (bsToItem)
import CASL.SymbolParser
import CASL.MapSentence
import CASL.Amalgamability
import CASL.ATC_CASL ()
import CASL.Sublogic as SL
import CASL.Sign
import CASL.StaticAna
import CASL.ColimSign
import CASL.Morphism
import CASL.SymbolMapAnalysis
import CASL.Taxonomy
import CASL.Simplify
import CASL.SimplifySen
import CASL.CCC.FreeTypes
import CASL.CCC.OnePoint () -- currently unused
import CASL.Qualify
import CASL.Quantification
import qualified CASL.OMDocImport as OMI
import CASL.OMDocExport
import CASL.Freeness

-- test
import CASL.Formula (formula)

#ifdef UNI_PACKAGE
import CASL.QuickCheck
import CASL.Zipperposition
#endif

import Common.ProofTree
import Common.Consistency
import Common.DocUtils

import Data.Monoid ()
import qualified Data.Set as Set

import Logic.Logic

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

instance Language CASL where
 description :: CASL -> String
description _ = [String] -> String
unlines
  [ "CASL - the Common algebraic specification language"
  , "This logic is subsorted partial first-order logic"
  , "  with sort generation constraints"
  , "See the CASL User Manual, LNCS 2900, Springer Verlag"
  , "and the CASL Reference Manual, LNCS 2960, Springer Verlag"
  , "See also http://www.cofi.info/CASL.html"
  , ""
  , "Abbreviations of sublogic names indicate the following feature:"
  , "  Sub    -> with subsorting"
  , "  Sul    -> with a locally filtered subsort relation"
  , "  P      -> with partial functions"
  , "  C      -> with sort generation constraints"
  , "  tC     -> C without partial constructors"
  , "  fC     -> C without non-free constraints (implies tC)"
  , "  eC     -> C without renamings"
  , "  sC     -> C with injective constructors"
  , "  seC    -> sC and eC"
  , "  FOL    -> first order logic"
  , "  FOAlg  -> FOL without predicates"
  , "  Horn   -> positive conditional logic"
  , "  GHorn  -> generalized Horn"
  , "  GCond  -> GHorn without predicates"
  , "  Cond   -> Horn without predicates"
  , "  Atom   -> atomic logic"
  , "  Eq     -> Atom without predicates"
  , "  =      -> with equality"
  , ""
  , "Examples:"
  , "  SubPCFOL=   -> the CASL logic itself"
  , "  FOAlg=      -> first order algebra (without predicates)"
  , "  SubPHorn=   -> the positive conditional fragement of CASL"
  , "  SubPAtom    -> the atomic subset of CASL"
  , "  SubPCAtom   -> SubPAtom with sort generation constraints"
  , "  Eq=         -> classical equational logic" ]

type CASLBasicSpec = BASIC_SPEC () () ()

trueC :: a -> b -> Bool
trueC :: a -> b -> Bool
trueC _ _ = Bool
True

instance (Ord f, Ord e, Ord m, MorphismExtension e m) =>
    Category (Sign f e) (Morphism f e m) where
    ide :: Sign f e -> Morphism f e m
ide sig :: Sign f e
sig = m -> Sign f e -> Morphism f e m
forall m f e. m -> Sign f e -> Morphism f e m
idMor (e -> m
forall e m. MorphismExtension e m => e -> m
ideMorphismExtension (e -> m) -> e -> m
forall a b. (a -> b) -> a -> b
$ Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
sig) Sign f e
sig
    inverse :: Morphism f e m -> Result (Morphism f e m)
inverse = (Morphism f e m -> Result m)
-> Morphism f e m -> Result (Morphism f e m)
forall f e m.
(Morphism f e m -> Result m)
-> Morphism f e m -> Result (Morphism f e m)
inverseMorphism Morphism f e m -> Result m
forall e m f. MorphismExtension e m => Morphism f e m -> Result m
inverseMorphismExtension
    composeMorphisms :: Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
composeMorphisms = (Morphism f e m -> Morphism f e m -> Result m)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
forall e f m.
Eq e =>
(Morphism f e m -> Morphism f e m -> Result m)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
composeM Morphism f e m -> Morphism f e m -> Result m
forall e m f.
MorphismExtension e m =>
Morphism f e m -> Morphism f e m -> Result m
composeMorphismExtension
    dom :: Morphism f e m -> Sign f e
dom = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource
    cod :: Morphism f e m -> Sign f e
cod = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget
    isInclusion :: Morphism f e m -> Bool
isInclusion = (m -> Bool) -> Morphism f e m -> Bool
forall m f e. (m -> Bool) -> Morphism f e m -> Bool
isInclusionMorphism m -> Bool
forall e m. MorphismExtension e m => m -> Bool
isInclusionMorphismExtension
    legal_mor :: Morphism f e m -> Result ()
legal_mor = Morphism f e m -> Result ()
forall e m f. MorphismExtension e m => Morphism f e m -> Result ()
legalMor

instance Semigroup (BASIC_SPEC b s f) where
    (Basic_spec l1 :: [Annoted (BASIC_ITEMS b s f)]
l1) <> :: BASIC_SPEC b s f -> BASIC_SPEC b s f -> BASIC_SPEC b s f
<> (Basic_spec l2 :: [Annoted (BASIC_ITEMS b s f)]
l2) = [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
forall b s f. [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
Basic_spec ([Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f)
-> [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
forall a b. (a -> b) -> a -> b
$ [Annoted (BASIC_ITEMS b s f)]
l1 [Annoted (BASIC_ITEMS b s f)]
-> [Annoted (BASIC_ITEMS b s f)] -> [Annoted (BASIC_ITEMS b s f)]
forall a. [a] -> [a] -> [a]
++ [Annoted (BASIC_ITEMS b s f)]
l2
instance Monoid (BASIC_SPEC b s f) where
    mempty :: BASIC_SPEC b s f
mempty = [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
forall b s f. [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
Basic_spec []

-- abstract syntax, parsing (and printing)

instance Syntax CASL CASLBasicSpec
                Symbol SYMB_ITEMS SYMB_MAP_ITEMS
      where
         parsersAndPrinters :: CASL
-> Map
     String
     (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc)
parsersAndPrinters CASL = String
-> (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc)
-> Map
     String
     (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc)
-> Map
     String
     (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc)
forall b. String -> b -> Map String b -> Map String b
addSyntax "KIF"
           (AParser st CASLBasicSpec -> PrefixMap -> AParser st CASLBasicSpec
forall a b. a -> b -> a
const (AParser st CASLBasicSpec -> PrefixMap -> AParser st CASLBasicSpec)
-> AParser st CASLBasicSpec
-> PrefixMap
-> AParser st CASLBasicSpec
forall a b. (a -> b) -> a -> b
$ ([RangedLL] -> CASLBasicSpec)
-> ParsecT String (AnnoState st) Identity [RangedLL]
-> AParser st CASLBasicSpec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [RangedLL] -> CASLBasicSpec
kif2CASL ParsecT String (AnnoState st) Identity [RangedLL]
forall st. CharParser st [RangedLL]
kifBasic, CASLBasicSpec -> Doc
forall a. Pretty a => a -> Doc
pretty)
           (Map
   String
   (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc)
 -> Map
      String
      (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc))
-> Map
     String
     (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc)
-> Map
     String
     (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc)
forall a b. (a -> b) -> a -> b
$ (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc)
-> Map
     String
     (PrefixMap -> AParser st CASLBasicSpec, CASLBasicSpec -> Doc)
forall b. b -> Map String b
makeDefault ([String] -> PrefixMap -> AParser st CASLBasicSpec
forall f s b st.
(TermParser f, AParsable s, AParsable b) =>
[String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec [], CASLBasicSpec -> Doc
forall a. Pretty a => a -> Doc
pretty)
         parseSingleSymbItem :: CASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parseSingleSymbItem CASL = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_ITEMS
forall st. [String] -> AParser st SYMB_ITEMS
symbItem []
         parse_symb_items :: CASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items CASL = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_ITEMS
forall st. [String] -> AParser st SYMB_ITEMS
symbItems []
         parse_symb_map_items :: CASL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items CASL = (PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_MAP_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> (AParser st SYMB_MAP_ITEMS
    -> PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_MAP_ITEMS -> PrefixMap -> AParser st SYMB_MAP_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_MAP_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_MAP_ITEMS
forall st. [String] -> AParser st SYMB_MAP_ITEMS
symbMapItems []
         toItem :: CASL -> CASLBasicSpec -> Item
toItem CASL = CASLBasicSpec -> Item
forall b s f.
(Pretty b, Pretty s, GetRange b, GetRange s, FormExtension f) =>
BASIC_SPEC b s f -> Item
bsToItem
         symb_items_name :: CASL -> SYMB_ITEMS -> [String]
symb_items_name CASL = SYMB_ITEMS -> [String]
symbItemsName

-- lattices (for sublogics)

instance Lattice a => SemiLatticeWithTop (CASL_SL a) where
    lub :: CASL_SL a -> CASL_SL a -> CASL_SL a
lub = CASL_SL a -> CASL_SL a -> CASL_SL a
forall a. Lattice a => CASL_SL a -> CASL_SL a -> CASL_SL a
sublogics_max
    top :: CASL_SL a
top = CASL_SL a
forall a. Lattice a => CASL_SL a
SL.top

class Lattice a => MinSL a f where
    minSL :: f -> CASL_SL a

instance MinSL () () where
    minSL :: () -> CASL_SL ()
minSL () = CASL_SL ()
forall a. Lattice a => CASL_SL a
bottom

class NameSL a where
    nameSL :: a -> String

instance NameSL () where
    nameSL :: () -> String
nameSL _ = ""

class Lattice a => ProjForm a f where
    projForm :: CASL_SL a -> f -> Maybe (FORMULA f)

instance Lattice a => ProjForm a () where
    projForm :: CASL_SL a -> () -> Maybe (FORMULA ())
projForm _ = FORMULA () -> Maybe (FORMULA ())
forall a. a -> Maybe a
Just (FORMULA () -> Maybe (FORMULA ()))
-> (() -> FORMULA ()) -> () -> Maybe (FORMULA ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> FORMULA ()
forall f. f -> FORMULA f
ExtFORMULA

class (Lattice a, ProjForm a f) => ProjSigItem a s f where
    projSigItems :: CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])

instance (Lattice a, ProjForm a f) => ProjSigItem a () f where
    projSigItems :: CASL_SL a -> () -> (Maybe (SIG_ITEMS () f), [SORT])
projSigItems _ s :: ()
s = (SIG_ITEMS () f -> Maybe (SIG_ITEMS () f)
forall a. a -> Maybe a
Just (SIG_ITEMS () f -> Maybe (SIG_ITEMS () f))
-> SIG_ITEMS () f -> Maybe (SIG_ITEMS () f)
forall a b. (a -> b) -> a -> b
$ () -> SIG_ITEMS () f
forall s f. s -> SIG_ITEMS s f
Ext_SIG_ITEMS ()
s, [])

class (Lattice a, ProjForm a f) => ProjBasic a b s f where
    projBasicItems :: CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])

instance (Lattice a, ProjForm a f, ProjSigItem a s f)
    => ProjBasic a () s f where
    projBasicItems :: CASL_SL a -> () -> (Maybe (BASIC_ITEMS () s f), [SORT])
projBasicItems _ b :: ()
b = (BASIC_ITEMS () s f -> Maybe (BASIC_ITEMS () s f)
forall a. a -> Maybe a
Just (BASIC_ITEMS () s f -> Maybe (BASIC_ITEMS () s f))
-> BASIC_ITEMS () s f -> Maybe (BASIC_ITEMS () s f)
forall a b. (a -> b) -> a -> b
$ () -> BASIC_ITEMS () s f
forall b s f. b -> BASIC_ITEMS b s f
Ext_BASIC_ITEMS ()
b, [])

instance (NameSL a) => SublogicName (CASL_SL a) where
    sublogicName :: CASL_SL a -> String
sublogicName = (a -> String) -> CASL_SL a -> String
forall a. (a -> String) -> CASL_SL a -> String
sublogics_name a -> String
forall a. NameSL a => a -> String
nameSL

instance (MinSL a f, MinSL a s, MinSL a b) =>
    MinSublogic (CASL_SL a) (BASIC_SPEC b s f) where
    minSublogic :: BASIC_SPEC b s f -> CASL_SL a
minSublogic = (b -> CASL_SL a)
-> (s -> CASL_SL a)
-> (f -> CASL_SL a)
-> BASIC_SPEC b s f
-> CASL_SL a
forall a b s f.
Lattice a =>
(b -> CASL_SL a)
-> (s -> CASL_SL a)
-> (f -> CASL_SL a)
-> BASIC_SPEC b s f
-> CASL_SL a
sl_basic_spec b -> CASL_SL a
forall a f. MinSL a f => f -> CASL_SL a
minSL s -> CASL_SL a
forall a f. MinSL a f => f -> CASL_SL a
minSL f -> CASL_SL a
forall a f. MinSL a f => f -> CASL_SL a
minSL

instance MinSL a f => MinSublogic (CASL_SL a) (FORMULA f) where
    minSublogic :: FORMULA f -> CASL_SL a
minSublogic = (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
forall a f. Lattice a => (f -> CASL_SL a) -> FORMULA f -> CASL_SL a
sl_sentence f -> CASL_SL a
forall a f. MinSL a f => f -> CASL_SL a
minSL

instance Lattice a => MinSublogic (CASL_SL a) SYMB_ITEMS where
    minSublogic :: SYMB_ITEMS -> CASL_SL a
minSublogic = SYMB_ITEMS -> CASL_SL a
forall a. Lattice a => SYMB_ITEMS -> CASL_SL a
sl_symb_items

instance Lattice a => MinSublogic (CASL_SL a) SYMB_MAP_ITEMS where
    minSublogic :: SYMB_MAP_ITEMS -> CASL_SL a
minSublogic = SYMB_MAP_ITEMS -> CASL_SL a
forall a. Lattice a => SYMB_MAP_ITEMS -> CASL_SL a
sl_symb_map_items

instance MinSL a e => MinSublogic (CASL_SL a) (Sign f e) where
    minSublogic :: Sign f e -> CASL_SL a
minSublogic = (e -> CASL_SL a) -> Sign f e -> CASL_SL a
forall a e f.
Lattice a =>
(e -> CASL_SL a) -> Sign f e -> CASL_SL a
sl_sign e -> CASL_SL a
forall a f. MinSL a f => f -> CASL_SL a
minSL

instance MinSL a e => MinSublogic (CASL_SL a) (Morphism f e m) where
    minSublogic :: Morphism f e m -> CASL_SL a
minSublogic = (e -> CASL_SL a) -> Morphism f e m -> CASL_SL a
forall a e f m.
Lattice a =>
(e -> CASL_SL a) -> Morphism f e m -> CASL_SL a
sl_morphism e -> CASL_SL a
forall a f. MinSL a f => f -> CASL_SL a
minSL

instance Lattice a => MinSublogic (CASL_SL a) Symbol where
    minSublogic :: Symbol -> CASL_SL a
minSublogic = Symbol -> CASL_SL a
forall a. Lattice a => Symbol -> CASL_SL a
sl_symbol

instance (MinSL a f, MinSL a s, MinSL a b, ProjForm a f,
          ProjSigItem a s f, ProjBasic a b s f) =>
    ProjectSublogic (CASL_SL a) (BASIC_SPEC b s f) where
    projectSublogic :: CASL_SL a -> BASIC_SPEC b s f -> BASIC_SPEC b s f
projectSublogic = (CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT]))
-> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a
-> BASIC_SPEC b s f
-> BASIC_SPEC b s f
forall a b s f.
Lattice a =>
(CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT]))
-> (CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT]))
-> (CASL_SL a -> f -> Maybe (FORMULA f))
-> CASL_SL a
-> BASIC_SPEC b s f
-> BASIC_SPEC b s f
pr_basic_spec CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])
forall a b s f.
ProjBasic a b s f =>
CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])
projBasicItems CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])
forall a s f.
ProjSigItem a s f =>
CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])
projSigItems CASL_SL a -> f -> Maybe (FORMULA f)
forall a f. ProjForm a f => CASL_SL a -> f -> Maybe (FORMULA f)
projForm

instance Lattice a => ProjectSublogicM (CASL_SL a) SYMB_ITEMS where
    projectSublogicM :: CASL_SL a -> SYMB_ITEMS -> Maybe SYMB_ITEMS
projectSublogicM = CASL_SL a -> SYMB_ITEMS -> Maybe SYMB_ITEMS
forall a. Lattice a => CASL_SL a -> SYMB_ITEMS -> Maybe SYMB_ITEMS
pr_symb_items

instance Lattice a => ProjectSublogicM (CASL_SL a) SYMB_MAP_ITEMS where
    projectSublogicM :: CASL_SL a -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
projectSublogicM = CASL_SL a -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
forall a.
Lattice a =>
CASL_SL a -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
pr_symb_map_items

instance MinSL a e => ProjectSublogic (CASL_SL a) (Sign f e) where
    projectSublogic :: CASL_SL a -> Sign f e -> Sign f e
projectSublogic = CASL_SL a -> Sign f e -> Sign f e
forall a f e. CASL_SL a -> Sign f e -> Sign f e
pr_sign

instance MinSL a e => ProjectSublogic (CASL_SL a) (Morphism f e m) where
    projectSublogic :: CASL_SL a -> Morphism f e m -> Morphism f e m
projectSublogic = CASL_SL a -> Morphism f e m -> Morphism f e m
forall a f e m.
Lattice a =>
CASL_SL a -> Morphism f e m -> Morphism f e m
pr_morphism

instance Lattice a => ProjectSublogicM (CASL_SL a) Symbol where
    projectSublogicM :: CASL_SL a -> Symbol -> Maybe Symbol
projectSublogicM = CASL_SL a -> Symbol -> Maybe Symbol
forall a. Lattice a => CASL_SL a -> Symbol -> Maybe Symbol
pr_symbol

-- CASL logic

instance Sentences CASL CASLFORMULA CASLSign CASLMor Symbol where
      map_sen :: CASL -> CASLMor -> FORMULA () -> Result (FORMULA ())
map_sen CASL m :: CASLMor
m = FORMULA () -> Result (FORMULA ())
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA () -> Result (FORMULA ()))
-> (FORMULA () -> FORMULA ()) -> FORMULA () -> Result (FORMULA ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen () () () -> CASLMor -> FORMULA () -> FORMULA ()
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen ((() -> ()) -> MapSen () () ()
forall a b. a -> b -> a
const () -> ()
forall a. a -> a
id) CASLMor
m
      negation :: CASL -> FORMULA () -> Maybe (FORMULA ())
negation CASL = FORMULA () -> Maybe (FORMULA ())
forall f. FORMULA f -> Maybe (FORMULA f)
negateFormula
      sym_of :: CASL -> CASLSign -> [Set Symbol]
sym_of CASL = CASLSign -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf
      mostSymsOf :: CASL -> CASLSign -> [Symbol]
mostSymsOf CASL = CASLSign -> [Symbol]
forall f e. Sign f e -> [Symbol]
sigSymsOf
      symmap_of :: CASL -> CASLMor -> EndoMap Symbol
symmap_of CASL = CASLMor -> EndoMap Symbol
forall f e m. Morphism f e m -> EndoMap Symbol
morphismToSymbMap
      sym_name :: CASL -> Symbol -> SORT
sym_name CASL = Symbol -> SORT
symName
      symKind :: CASL -> Symbol -> String
symKind CASL = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Symbol -> Doc) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SYMB_KIND -> Doc
forall a. Pretty a => a -> Doc
pretty (SYMB_KIND -> Doc) -> (Symbol -> SYMB_KIND) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbType -> SYMB_KIND
symbolKind (SymbType -> SYMB_KIND)
-> (Symbol -> SymbType) -> Symbol -> SYMB_KIND
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SymbType
symbType
      symsOfSen :: CASL -> CASLSign -> FORMULA () -> [Symbol]
symsOfSen CASL _ = Set Symbol -> [Symbol]
forall a. Set a -> [a]
Set.toList
        (Set Symbol -> [Symbol])
-> (FORMULA () -> Set Symbol) -> FORMULA () -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Record () (Set Symbol) (Set Symbol) -> FORMULA () -> Set Symbol
forall f a b. Record f a b -> FORMULA f -> a
foldFormula ((() -> Set Symbol) -> Record () (Set Symbol) (Set Symbol)
forall f. (f -> Set Symbol) -> Record f (Set Symbol) (Set Symbol)
symbolsRecord ((() -> Set Symbol) -> Record () (Set Symbol) (Set Symbol))
-> (() -> Set Symbol) -> Record () (Set Symbol) (Set Symbol)
forall a b. (a -> b) -> a -> b
$ Set Symbol -> () -> Set Symbol
forall a b. a -> b -> a
const Set Symbol
forall a. Set a
Set.empty)
      simplify_sen :: CASL -> CASLSign -> FORMULA () -> FORMULA ()
simplify_sen CASL = CASLSign -> FORMULA () -> FORMULA ()
forall f e.
(FormExtension f, TermExtension f) =>
Sign f e -> FORMULA f -> FORMULA f
simplifyCASLSen
      print_named :: CASL -> Named (FORMULA ()) -> Doc
print_named CASL = Named (FORMULA ()) -> Doc
forall f. FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula

instance StaticAnalysis CASL CASLBasicSpec CASLFORMULA
               SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol where
         basic_analysis :: CASL
-> Maybe
     ((CASLBasicSpec, CASLSign, GlobalAnnos)
      -> Result
           (CASLBasicSpec, ExtSign CASLSign Symbol, [Named (FORMULA ())]))
basic_analysis CASL = ((CASLBasicSpec, CASLSign, GlobalAnnos)
 -> Result
      (CASLBasicSpec, ExtSign CASLSign Symbol, [Named (FORMULA ())]))
-> Maybe
     ((CASLBasicSpec, CASLSign, GlobalAnnos)
      -> Result
           (CASLBasicSpec, ExtSign CASLSign Symbol, [Named (FORMULA ())]))
forall a. a -> Maybe a
Just (CASLBasicSpec, CASLSign, GlobalAnnos)
-> Result
     (CASLBasicSpec, ExtSign CASLSign Symbol, [Named (FORMULA ())])
basicCASLAnalysis
         sen_analysis :: CASL
-> Maybe
     ((CASLBasicSpec, CASLSign, FORMULA ()) -> Result (FORMULA ()))
sen_analysis CASL = ((CASLBasicSpec, CASLSign, FORMULA ()) -> Result (FORMULA ()))
-> Maybe
     ((CASLBasicSpec, CASLSign, FORMULA ()) -> Result (FORMULA ()))
forall a. a -> Maybe a
Just (CASLBasicSpec, CASLSign, FORMULA ()) -> Result (FORMULA ())
cASLsen_analysis
         stat_symb_map_items :: CASL
-> CASLSign
-> Maybe CASLSign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
stat_symb_map_items CASL = CASLSign
-> Maybe CASLSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol)
forall f e.
Sign f e
-> Maybe (Sign f e)
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
statSymbMapItems
         stat_symb_items :: CASL -> CASLSign -> [SYMB_ITEMS] -> Result [RawSymbol]
stat_symb_items CASL = CASLSign -> [SYMB_ITEMS] -> Result [RawSymbol]
forall f e. Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems
         signature_colimit :: CASL
-> Gr CASLSign (Int, CASLMor) -> Result (CASLSign, Map Int CASLMor)
signature_colimit CASL diag :: Gr CASLSign (Int, CASLMor)
diag = (CASLSign, Map Int CASLMor) -> Result (CASLSign, Map Int CASLMor)
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLSign, Map Int CASLMor) -> Result (CASLSign, Map Int CASLMor))
-> (CASLSign, Map Int CASLMor)
-> Result (CASLSign, Map Int CASLMor)
forall a b. (a -> b) -> a -> b
$ Gr CASLSign (Int, CASLMor)
-> (Gr () (Int, ()) -> Map Int CASLMor -> ((), Map Int ()))
-> (CASLSign, Map Int CASLMor)
forall f e m.
Category (Sign f e) (Morphism f e m) =>
Gr (Sign f e) (Int, Morphism f e m)
-> (Gr e (Int, m) -> Map Int (Morphism f e m) -> (e, Map Int m))
-> (Sign f e, Map Int (Morphism f e m))
signColimit Gr CASLSign (Int, CASLMor)
diag Gr () (Int, ()) -> Map Int CASLMor -> ((), Map Int ())
extCASLColimit
         quotient_term_algebra :: CASL
-> CASLMor
-> [Named (FORMULA ())]
-> Result (CASLSign, [Named (FORMULA ())])
quotient_term_algebra CASL = CASLMor
-> [Named (FORMULA ())] -> Result (CASLSign, [Named (FORMULA ())])
quotientTermAlgebra
         ensures_amalgamability :: CASL
-> ([CASLAmalgOpt], Gr CASLSign (Int, CASLMor), [(Int, CASLMor)],
    Gr String String)
-> Result Amalgamates
ensures_amalgamability CASL (opts :: [CASLAmalgOpt]
opts, diag :: Gr CASLSign (Int, CASLMor)
diag, sink :: [(Int, CASLMor)]
sink, desc :: Gr String String
desc) =
             [CASLAmalgOpt]
-> Gr CASLSign (Int, CASLMor)
-> [(Int, CASLMor)]
-> Gr String String
-> Result Amalgamates
ensuresAmalgamability [CASLAmalgOpt]
opts Gr CASLSign (Int, CASLMor)
diag [(Int, CASLMor)]
sink Gr String String
desc

         qualify :: CASL
-> SIMPLE_ID
-> LibName
-> CASLMor
-> CASLSign
-> Result (CASLMor, [Named (FORMULA ())])
qualify CASL = SIMPLE_ID
-> LibName
-> CASLMor
-> CASLSign
-> Result (CASLMor, [Named (FORMULA ())])
forall f e.
SIMPLE_ID
-> LibName
-> Morphism f e ()
-> Sign f e
-> Result (Morphism f e (), [Named (FORMULA f)])
qualifySig
         symbol_to_raw :: CASL -> Symbol -> RawSymbol
symbol_to_raw CASL = Symbol -> RawSymbol
symbolToRaw
         id_to_raw :: CASL -> SORT -> RawSymbol
id_to_raw CASL = SORT -> RawSymbol
idToRaw
         matches :: CASL -> Symbol -> RawSymbol -> Bool
matches CASL = Symbol -> RawSymbol -> Bool
CASL.Morphism.matches
         is_transportable :: CASL -> CASLMor -> Bool
is_transportable CASL = CASLMor -> Bool
forall f e m. Morphism f e m -> Bool
isSortInjective
         is_injective :: CASL -> CASLMor -> Bool
is_injective CASL = CASLMor -> Bool
forall f e m. Morphism f e m -> Bool
isInjective

         empty_signature :: CASL -> CASLSign
empty_signature CASL = () -> CASLSign
forall e f. e -> Sign f e
emptySign ()
         add_symb_to_sign :: CASL -> CASLSign -> Symbol -> Result CASLSign
add_symb_to_sign CASL = CASLSign -> Symbol -> Result CASLSign
forall e f. Sign e f -> Symbol -> Result (Sign e f)
addSymbToSign

         signature_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign
signature_union CASL s :: CASLSign
s = CASLSign -> Result CASLSign
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign -> Result CASLSign)
-> (CASLSign -> CASLSign) -> CASLSign -> Result CASLSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() -> () -> ()) -> CASLSign -> CASLSign -> CASLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig () -> () -> ()
forall a b. a -> b -> a
const CASLSign
s
         signatureDiff :: CASL -> CASLSign -> CASLSign -> Result CASLSign
signatureDiff CASL s :: CASLSign
s = CASLSign -> Result CASLSign
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign -> Result CASLSign)
-> (CASLSign -> CASLSign) -> CASLSign -> Result CASLSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() -> () -> ()) -> CASLSign -> CASLSign -> CASLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig () -> () -> ()
forall a b. a -> b -> a
const CASLSign
s
         intersection :: CASL -> CASLSign -> CASLSign -> Result CASLSign
intersection CASL s :: CASLSign
s = CASLSign -> Result CASLSign
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign -> Result CASLSign)
-> (CASLSign -> CASLSign) -> CASLSign -> Result CASLSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() -> () -> ()) -> CASLSign -> CASLSign -> CASLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
interSig () -> () -> ()
forall a b. a -> b -> a
const CASLSign
s
         morphism_union :: CASL -> CASLMor -> CASLMor -> Result CASLMor
morphism_union CASL = (() -> () -> ()) -> CASLMor -> CASLMor -> Result CASLMor
forall e f m.
(e -> e -> e)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
plainMorphismUnion () -> () -> ()
forall a b. a -> b -> a
const
         final_union :: CASL -> CASLSign -> CASLSign -> Result CASLSign
final_union CASL = (() -> () -> ()) -> CASLSign -> CASLSign -> Result CASLSign
forall e f.
(e -> e -> e) -> Sign f e -> Sign f e -> Result (Sign f e)
finalUnion () -> () -> ()
forall a b. a -> b -> a
const
         is_subsig :: CASL -> CASLSign -> CASLSign -> Bool
is_subsig CASL = (() -> () -> Bool) -> CASLSign -> CASLSign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig () -> () -> Bool
forall a b. a -> b -> Bool
trueC
         subsig_inclusion :: CASL -> CASLSign -> CASLSign -> Result CASLMor
subsig_inclusion CASL = () -> CASLSign -> CASLSign -> Result CASLMor
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion ()
         cogenerated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor
cogenerated_sign CASL = () -> Set Symbol -> CASLSign -> Result CASLMor
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
cogeneratedSign ()
         generated_sign :: CASL -> Set Symbol -> CASLSign -> Result CASLMor
generated_sign CASL = () -> Set Symbol -> CASLSign -> Result CASLMor
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign ()
         induced_from_morphism :: CASL -> EndoMap RawSymbol -> CASLSign -> Result CASLMor
induced_from_morphism CASL = () -> EndoMap RawSymbol -> CASLSign -> Result CASLMor
forall e f m.
(Pretty e, Show f) =>
m -> EndoMap RawSymbol -> Sign f e -> Result (Morphism f e m)
inducedFromMorphism ()
         induced_from_to_morphism :: CASL
-> EndoMap RawSymbol
-> ExtSign CASLSign Symbol
-> ExtSign CASLSign Symbol
-> Result CASLMor
induced_from_to_morphism CASL = ()
-> (() -> () -> Bool)
-> (() -> () -> ())
-> EndoMap RawSymbol
-> ExtSign CASLSign Symbol
-> ExtSign CASLSign Symbol
-> Result CASLMor
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
m
-> (e -> e -> Bool)
-> (e -> e -> e)
-> EndoMap RawSymbol
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphism () () -> () -> Bool
forall a b. a -> b -> Bool
trueC () -> () -> ()
forall a b. a -> b -> a
const
         theory_to_taxonomy :: CASL
-> TaxoGraphKind
-> MMiSSOntology
-> CASLSign
-> [Named (FORMULA ())]
-> Result MMiSSOntology
theory_to_taxonomy CASL = TaxoGraphKind
-> MMiSSOntology
-> CASLSign
-> [Named (FORMULA ())]
-> Result MMiSSOntology
forall f e.
TaxoGraphKind
-> MMiSSOntology
-> Sign f e
-> [Named (FORMULA f)]
-> Result MMiSSOntology
convTaxo

instance Logic CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree where
         stability :: CASL -> Stability
stability CASL = Stability
Stable
         -- for Hybridization
         parse_basic_sen :: CASL -> Maybe (CASLBasicSpec -> AParser st (FORMULA ()))
parse_basic_sen CASL = (CASLBasicSpec -> AParser st (FORMULA ()))
-> Maybe (CASLBasicSpec -> AParser st (FORMULA ()))
forall a. a -> Maybe a
Just ((CASLBasicSpec -> AParser st (FORMULA ()))
 -> Maybe (CASLBasicSpec -> AParser st (FORMULA ())))
-> (CASLBasicSpec -> AParser st (FORMULA ()))
-> Maybe (CASLBasicSpec -> AParser st (FORMULA ()))
forall a b. (a -> b) -> a -> b
$ \ _ -> [String] -> AParser st (FORMULA ())
forall f st. TermParser f => [String] -> AParser st (FORMULA f)
formula []

         proj_sublogic_epsilon :: CASL -> CASL_SL () -> CASLSign -> CASLMor
proj_sublogic_epsilon CASL = () -> CASL_SL () -> CASLSign -> CASLMor
forall m a f e. m -> CASL_SL a -> Sign f e -> Morphism f e m
pr_epsilon ()
         all_sublogics :: CASL -> [CASL_SL ()]
all_sublogics CASL = [()] -> [CASL_SL ()]
forall a. Lattice a => [a] -> [CASL_SL a]
sublogics_all []
         sublogicDimensions :: CASL -> [[CASL_SL ()]]
sublogicDimensions CASL = [[()]] -> [[CASL_SL ()]]
forall a. Lattice a => [[a]] -> [[CASL_SL a]]
sDims []
         parseSublogic :: CASL -> String -> Maybe (CASL_SL ())
parseSublogic CASL = (String -> Maybe ((), String)) -> String -> Maybe (CASL_SL ())
forall a.
(String -> Maybe (a, String)) -> String -> Maybe (CASL_SL a)
parseSL (\ s :: String
s -> ((), String) -> Maybe ((), String)
forall a. a -> Maybe a
Just ((), String
s))
         conservativityCheck :: CASL -> [ConservativityChecker CASLSign (FORMULA ()) CASLMor]
conservativityCheck CASL =
             [String
-> IO (Maybe String)
-> ((CASLSign, [Named (FORMULA ())])
    -> CASLMor
    -> [Named (FORMULA ())]
    -> IO (Result (Conservativity, [FORMULA ()])))
-> ConservativityChecker CASLSign (FORMULA ()) CASLMor
forall sign sentence morphism.
String
-> IO (Maybe String)
-> ((sign, [Named sentence])
    -> morphism
    -> [Named sentence]
    -> IO (Result (Conservativity, [sentence])))
-> ConservativityChecker sign sentence morphism
ConservativityChecker "CCC" (Maybe String -> IO (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing) (CASLSign, [Named (FORMULA ())])
-> CASLMor
-> [Named (FORMULA ())]
-> IO (Result (Conservativity, [FORMULA ()]))
forall f e m.
(FormExtension f, TermExtension f, Ord f) =>
(Sign f e, [Named (FORMULA f)])
-> Morphism f e m
-> [Named (FORMULA f)]
-> IO (Result (Conservativity, [FORMULA f]))
checkFreeType]
         empty_proof_tree :: CASL -> ProofTree
empty_proof_tree CASL = ProofTree
emptyProofTree
         omdoc_metatheory :: CASL -> Maybe OMCD
omdoc_metatheory CASL = OMCD -> Maybe OMCD
forall a. a -> Maybe a
Just OMCD
caslMetaTheory
         export_senToOmdoc :: CASL -> NameMap Symbol -> FORMULA () -> Result TCorOMElement
export_senToOmdoc CASL = NameMap Symbol -> FORMULA () -> Result TCorOMElement
forall f.
(GetRange f, Pretty f) =>
NameMap Symbol -> FORMULA f -> Result TCorOMElement
exportSenToOmdoc
         export_symToOmdoc :: CASL -> NameMap Symbol -> Symbol -> String -> Result TCElement
export_symToOmdoc CASL = NameMap Symbol -> Symbol -> String -> Result TCElement
exportSymToOmdoc
         export_theoryToOmdoc :: CASL
-> SigMap Symbol
-> CASLSign
-> [Named (FORMULA ())]
-> Result [TCElement]
export_theoryToOmdoc CASL = SigMap Symbol
-> CASLSign -> [Named (FORMULA ())] -> Result [TCElement]
forall f e.
(Show f, Pretty e) =>
SigMap Symbol
-> Sign f e -> [Named (FORMULA f)] -> Result [TCElement]
exportTheoryToOmdoc
         omdocToSen :: CASL
-> SigMapI Symbol
-> TCElement
-> String
-> Result (Maybe (Named (FORMULA ())))
omdocToSen CASL = SigMapI Symbol
-> TCElement -> String -> Result (Maybe (Named (FORMULA ())))
forall f.
SigMapI Symbol
-> TCElement -> String -> Result (Maybe (Named (FORMULA f)))
OMI.omdocToSen
         omdocToSym :: CASL -> SigMapI Symbol -> TCElement -> String -> Result Symbol
omdocToSym CASL = SigMapI Symbol -> TCElement -> String -> Result Symbol
OMI.omdocToSym
         addOMadtToTheory :: CASL
-> SigMapI Symbol
-> (CASLSign, [Named (FORMULA ())])
-> [[OmdADT]]
-> Result (CASLSign, [Named (FORMULA ())])
addOMadtToTheory CASL = SigMapI Symbol
-> (CASLSign, [Named (FORMULA ())])
-> [[OmdADT]]
-> Result (CASLSign, [Named (FORMULA ())])
forall f e.
SigMapI Symbol
-> (Sign f e, [Named (FORMULA f)])
-> [[OmdADT]]
-> Result (Sign f e, [Named (FORMULA f)])
OMI.addOMadtToTheory
         addOmdocToTheory :: CASL
-> SigMapI Symbol
-> (CASLSign, [Named (FORMULA ())])
-> [TCElement]
-> Result (CASLSign, [Named (FORMULA ())])
addOmdocToTheory CASL = SigMapI Symbol
-> (CASLSign, [Named (FORMULA ())])
-> [TCElement]
-> Result (CASLSign, [Named (FORMULA ())])
forall f e.
SigMapI Symbol
-> (Sign f e, [Named (FORMULA f)])
-> [TCElement]
-> Result (Sign f e, [Named (FORMULA f)])
OMI.addOmdocToTheory
         syntaxTable :: CASL -> CASLSign -> Maybe SyntaxTable
syntaxTable CASL = SyntaxTable -> Maybe SyntaxTable
forall a. a -> Maybe a
Just (SyntaxTable -> Maybe SyntaxTable)
-> (CASLSign -> SyntaxTable) -> CASLSign -> Maybe SyntaxTable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLSign -> SyntaxTable
forall f e. Sign f e -> SyntaxTable
getSyntaxTable
#ifdef UNI_PACKAGE
         provers :: CASL
-> [Prover CASLSign (FORMULA ()) CASLMor (CASL_SL ()) ProofTree]
provers CASL =
           [ Prover CASLSign (FORMULA ()) CASLMor (CASL_SL ()) ProofTree
quickCheckProver
           , Prover CASLSign (FORMULA ()) CASLMor (CASL_SL ()) ProofTree
zipperpositionFreeFolProver
           , Prover CASLSign (FORMULA ()) CASLMor (CASL_SL ()) ProofTree
zipperpositionCFolProver
           ]
#endif