{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/Adl2CASL.hs
Description :  Coding a description language into CASL
Copyright   :  (c)  Stef Joosten, Christian Maeder DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

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

The translating comorphism from Adl to CASL.
-}

module Comorphisms.Adl2CASL
    ( Adl2CASL (..)
    ) where

import Logic.Logic
import Logic.Comorphism

-- Adl
import Adl.Logic_Adl as A
import Adl.As as A
import Adl.Sign as A

-- CASL
import CASL.Logic_CASL
import CASL.AS_Basic_CASL as C
import CASL.Sublogic
import CASL.Sign as C
import CASL.Morphism as C
import CASL.Fold
import CASL.Overload

import Common.AS_Annotation
import Common.DefaultMorphism
import Common.DocUtils
import Common.Id
import Common.ProofTree
import Common.Result
import Common.Token
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet
import Common.Lib.State

import qualified Data.Set as Set

-- | lid of the morphism
data Adl2CASL = Adl2CASL deriving Int -> Adl2CASL -> ShowS
[Adl2CASL] -> ShowS
Adl2CASL -> String
(Int -> Adl2CASL -> ShowS)
-> (Adl2CASL -> String) -> ([Adl2CASL] -> ShowS) -> Show Adl2CASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Adl2CASL] -> ShowS
$cshowList :: [Adl2CASL] -> ShowS
show :: Adl2CASL -> String
$cshow :: Adl2CASL -> String
showsPrec :: Int -> Adl2CASL -> ShowS
$cshowsPrec :: Int -> Adl2CASL -> ShowS
Show

instance Language Adl2CASL -- default is ok

instance Comorphism Adl2CASL
    Adl
    ()
    Context
    Sen
    ()
    ()
    A.Sign
    A.Morphism
    A.Symbol
    A.RawSymbol
    ProofTree
    CASL
    CASL_Sublogics
    CASLBasicSpec
    CASLFORMULA
    SYMB_ITEMS
    SYMB_MAP_ITEMS
    CASLSign
    CASLMor
    C.Symbol
    C.RawSymbol
    ProofTree
    where
      sourceLogic :: Adl2CASL -> Adl
sourceLogic Adl2CASL = Adl
Adl
      sourceSublogic :: Adl2CASL -> ()
sourceSublogic Adl2CASL = ()
      targetLogic :: Adl2CASL -> CASL
targetLogic Adl2CASL = CASL
CASL
      mapSublogic :: Adl2CASL -> () -> Maybe CASL_Sublogics
mapSublogic Adl2CASL _ = 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
$ CASL_Sublogics
forall a. Lattice a => CASL_SL a
caslTop
        { has_part :: Bool
has_part = Bool
False
        , sub_features :: SubsortingFeatures
sub_features = SubsortingFeatures
LocFilSub
        , cons_features :: SortGenerationFeatures
cons_features = SortGenerationFeatures
NoSortGen }
      map_theory :: Adl2CASL
-> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
map_theory Adl2CASL = (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory
      map_sentence :: Adl2CASL -> Sign -> Sen -> Result CASLFORMULA
map_sentence Adl2CASL s :: Sign
s = CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> (Sen -> CASLFORMULA) -> Sen -> Result CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLSign -> Sen -> CASLFORMULA
mapSen (Sign -> CASLSign
mapSign Sign
s)
      map_morphism :: Adl2CASL -> Morphism -> Result CASLMor
map_morphism Adl2CASL = Morphism -> Result CASLMor
mapMor
      map_symbol :: Adl2CASL -> Sign -> Symbol -> Set Symbol
map_symbol Adl2CASL _ = 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
mapSym
      is_model_transportable :: Adl2CASL -> Bool
is_model_transportable Adl2CASL = Bool
True
      has_model_expansion :: Adl2CASL -> Bool
has_model_expansion Adl2CASL = Bool
True
      is_weakly_amalgamable :: Adl2CASL -> Bool
is_weakly_amalgamable Adl2CASL = Bool
True
      isInclusionComorphism :: Adl2CASL -> Bool
isInclusionComorphism Adl2CASL = Bool
True

mapTheory :: (A.Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory :: (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory (s :: Sign
s, ns :: [Named Sen]
ns) = let cs :: CASLSign
cs = Sign -> CASLSign
mapSign Sign
s in
  (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign
cs, (Named Sen -> Named CASLFORMULA)
-> [Named Sen] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((Sen -> CASLFORMULA) -> Named Sen -> Named CASLFORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((Sen -> CASLFORMULA) -> Named Sen -> Named CASLFORMULA)
-> (Sen -> CASLFORMULA) -> Named Sen -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLSign -> Sen -> CASLFORMULA
mapSen CASLSign
cs) [Named Sen]
ns)

relTypeToPred :: RelType -> PredType
relTypeToPred :: RelType -> PredType
relTypeToPred (RelType c1 :: Concept
c1 c2 :: Concept
c2) = [SORT] -> PredType
PredType [Concept -> SORT
conceptToId Concept
c1, Concept -> SORT
conceptToId Concept
c2]

mapSign :: A.Sign -> CASLSign
mapSign :: Sign -> CASLSign
mapSign s :: Sign
s = (() -> CASLSign
forall e f. e -> Sign f e
C.emptySign ())
  { sortRel :: Rel SORT
sortRel = Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Rel SORT -> Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union
       (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
$ (Symbol -> Set SORT -> Set SORT)
-> Set SORT -> Set Symbol -> Set SORT
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ sy :: Symbol
sy -> case Symbol
sy of
                 A.Con (C i :: Token
i) -> SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert (SORT -> Set SORT -> Set SORT) -> SORT -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Token -> SORT
simpleIdToId Token
i
                 _ -> Set SORT -> Set SORT
forall a. a -> a
id) Set SORT
forall a. Set a
Set.empty (Set Symbol -> Set SORT) -> Set Symbol -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign -> Set Symbol
A.symOf Sign
s)
       (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ (Concept -> SORT) -> Rel Concept -> Rel SORT
forall a b. (Ord a, Ord b) => (a -> b) -> Rel a -> Rel b
Rel.map Concept -> SORT
conceptToId (Rel Concept -> Rel SORT) -> Rel Concept -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Sign -> Rel Concept
isas Sign
s
  , predMap :: PredMap
predMap = [(SORT, [PredType])] -> PredMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList
      ([(SORT, [PredType])] -> PredMap)
-> (Map SORT (Set RelType) -> [(SORT, [PredType])])
-> Map SORT (Set RelType)
-> PredMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SORT, [PredType]) -> (SORT, [PredType]))
-> [(SORT, [PredType])] -> [(SORT, [PredType])]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: SORT
i, l :: [PredType]
l) -> (Token -> SORT
transRelId (Token -> SORT) -> Token -> SORT
forall a b. (a -> b) -> a -> b
$ SORT -> Token
idToSimpleId SORT
i, [PredType]
l))
      ([(SORT, [PredType])] -> [(SORT, [PredType])])
-> (Map SORT (Set RelType) -> [(SORT, [PredType])])
-> Map SORT (Set RelType)
-> [(SORT, [PredType])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredMap -> [(SORT, [PredType])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList (PredMap -> [(SORT, [PredType])])
-> (Map SORT (Set RelType) -> PredMap)
-> Map SORT (Set RelType)
-> [(SORT, [PredType])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RelType -> PredType) -> MapSet SORT RelType -> PredMap
forall b c a.
(Ord b, Ord c) =>
(b -> c) -> MapSet a b -> MapSet a c
MapSet.map RelType -> PredType
relTypeToPred (MapSet SORT RelType -> PredMap)
-> (Map SORT (Set RelType) -> MapSet SORT RelType)
-> Map SORT (Set RelType)
-> PredMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SORT (Set RelType) -> MapSet SORT RelType
forall a b. Ord a => Map a (Set b) -> MapSet a b
MapSet.fromMap (Map SORT (Set RelType) -> PredMap)
-> Map SORT (Set RelType) -> PredMap
forall a b. (a -> b) -> a -> b
$ Sign -> Map SORT (Set RelType)
rels Sign
s
  }

transRelId :: Token -> Id
transRelId :: Token -> SORT
transRelId t :: Token
t@(Token s :: String
s p :: Range
p) = Token -> SORT
simpleIdToId (Token -> SORT) -> Token -> SORT
forall a b. (a -> b) -> a -> b
$
   if String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
s [String]
casl_reserved_fwords then String -> Range -> Token
Token ("P_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
p else Token
t

mapSen :: CASLSign -> Sen -> CASLFORMULA
mapSen :: CASLSign -> Sen -> CASLFORMULA
mapSen sig :: CASLSign
sig s :: Sen
s = case Sen
s of
  DeclProp r :: Relation
r p :: RangedProp
p -> CASLSign -> Relation -> RangedProp -> CASLFORMULA
getRelProp CASLSign
sig Relation
r RangedProp
p
  Assertion _ r :: Rule
r ->
    let ((v1 :: Token
v1, s1 :: SORT
s1), (v2 :: Token
v2, s2 :: SORT
s2), f :: CASLFORMULA
f) = State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
-> Int -> ((Token, SORT), (Token, SORT), CASLFORMULA)
forall s a. State s a -> s -> a
evalState (CASLSign
-> Rule -> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
transRule CASLSign
sig Rule
r) 1 in
    [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [Token -> SORT -> VAR_DECL
mkVarDecl Token
v1 SORT
s1, Token -> SORT -> VAR_DECL
mkVarDecl Token
v2 SORT
s2] CASLFORMULA
f

-- | Translation of morphisms
mapMor :: A.Morphism -> Result CASLMor
mapMor :: Morphism -> Result CASLMor
mapMor mor :: Morphism
mor = CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLMor -> Result CASLMor) -> CASLMor -> Result CASLMor
forall a b. (a -> b) -> a -> b
$ () -> CASLSign -> CASLSign -> CASLMor
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism ()
    (Sign -> CASLSign
mapSign (Sign -> CASLSign) -> Sign -> CASLSign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
forall sign. DefaultMorphism sign -> sign
domOfDefaultMorphism Morphism
mor) (CASLSign -> CASLMor) -> CASLSign -> CASLMor
forall a b. (a -> b) -> a -> b
$ Sign -> CASLSign
mapSign (Sign -> CASLSign) -> Sign -> CASLSign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
forall sign. DefaultMorphism sign -> sign
codOfDefaultMorphism Morphism
mor

mapSym :: A.Symbol -> C.Symbol
mapSym :: Symbol -> Symbol
mapSym s :: Symbol
s = case Symbol
s of
  A.Con c :: Concept
c -> SORT -> Symbol
idToSortSymbol (SORT -> Symbol) -> SORT -> Symbol
forall a b. (a -> b) -> a -> b
$ Concept -> SORT
conceptToId Concept
c
  Rel (Sgn n :: Token
n t :: RelType
t) -> SORT -> PredType -> Symbol
idToPredSymbol (Token -> SORT
transRelId Token
n) (PredType -> Symbol) -> PredType -> Symbol
forall a b. (a -> b) -> a -> b
$ RelType -> PredType
relTypeToPred RelType
t

next :: State Int Int
next :: State Int Int
next = do
  Int
i <- State Int Int
forall s. State s s
get
  Int -> State Int ()
forall s. s -> State s ()
put (Int -> State Int ()) -> Int -> State Int ()
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
  Int -> State Int Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i

getRelPred :: CASLSign -> A.Relation -> PRED_SYMB
getRelPred :: CASLSign -> Relation -> PRED_SYMB
getRelPred sig :: CASLSign
sig m :: Relation
m@(Sgn t :: Token
t (RelType c1 :: Concept
c1 c2 :: Concept
c2)) = let
  ty1 :: SORT
ty1 = Concept -> SORT
conceptToId Concept
c1
  ty2 :: SORT
ty2 = Concept -> SORT
conceptToId Concept
c2
  i :: SORT
i = Token -> SORT
transRelId Token
t
  cs :: [PredType]
cs = (PredType -> Bool) -> [PredType] -> [PredType]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ pt :: PredType
pt -> case PredType -> [SORT]
predArgs PredType
pt of
                  [fr :: SORT
fr, to :: SORT
to] -> CASLSign -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
leqSort CASLSign
sig SORT
ty1 SORT
fr Bool -> Bool -> Bool
&& CASLSign -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
leqSort CASLSign
sig SORT
ty2 SORT
to
                  _ -> Bool
False)
               ([PredType] -> [PredType]) -> [PredType] -> [PredType]
forall a b. (a -> b) -> a -> b
$ Set PredType -> [PredType]
forall a. Set a -> [a]
Set.toList (Set PredType -> [PredType]) -> Set PredType -> [PredType]
forall a b. (a -> b) -> a -> b
$ SORT -> PredMap -> Set PredType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
i (PredMap -> Set PredType) -> PredMap -> Set PredType
forall a b. (a -> b) -> a -> b
$ CASLSign -> PredMap
forall f e. Sign f e -> PredMap
predMap CASLSign
sig
  in case [PredType]
cs of
       ty :: PredType
ty : _ ->
           SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
i (PredType -> PRED_TYPE
toPRED_TYPE PredType
ty) (Range -> PRED_SYMB) -> Range -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
t
       _ -> String -> PRED_SYMB
forall a. HasCallStack => String -> a
error (String -> PRED_SYMB) -> String -> PRED_SYMB
forall a b. (a -> b) -> a -> b
$ "getRelPred " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Relation -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Relation
m ""

getRelProp :: CASLSign -> A.Relation -> RangedProp -> CASLFORMULA
getRelProp :: CASLSign -> Relation -> RangedProp -> CASLFORMULA
getRelProp sig :: CASLSign
sig r :: Relation
r p :: RangedProp
p =
  let qp :: PRED_SYMB
qp@(Qual_pred_name _ (Pred_type [fr :: SORT
fr, to :: SORT
to] _) _) = CASLSign -> Relation -> PRED_SYMB
getRelPred CASLSign
sig Relation
r
      q :: Range
q = RangedProp -> Range
propRange RangedProp
p
      q1 :: VAR_DECL
q1 = [Token] -> SORT -> Range -> VAR_DECL
Var_decl [String -> Token
mkSimpleId "a"] SORT
fr Range
q
      q2 :: VAR_DECL
q2 = [Token] -> SORT -> Range -> VAR_DECL
Var_decl [String -> Token
mkSimpleId "b"] SORT
to Range
q
      q3 :: VAR_DECL
q3 = [Token] -> SORT -> Range -> VAR_DECL
Var_decl [String -> Token
mkSimpleId "c"] SORT
fr Range
q
      t1 :: TERM f
t1 = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
q1
      t2 :: TERM f
t2 = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
q2
      t3 :: TERM f
t3 = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
q3
      pAppl :: FORMULA f
pAppl = PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
qp [TERM f
forall f. TERM f
t1, TERM f
forall f. TERM f
t2] Range
q
      eqs :: Bool
eqs = SORT
fr SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
to
  in case RangedProp -> Prop
propProp RangedProp
p of
       Uni -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL
q1, VAR_DECL
q2, VAR_DECL
q3]
            (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation
             ([CASLFORMULA] -> Range -> CASLFORMULA
forall f. [FORMULA f] -> Range -> FORMULA f
conjunctRange
              [CASLFORMULA
forall f. FORMULA f
pAppl, PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
qp [TERM ()
forall f. TERM f
t3, TERM ()
forall f. TERM f
t2] Range
q] Range
q)
             Relation
Implication (TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM ()
forall f. TERM f
t1 Equality
Strong TERM ()
forall f. TERM f
t3 Range
q)
             Range
q) Range
q
       Tot -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL
q1] (QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Existential [VAR_DECL
q2] CASLFORMULA
forall f. FORMULA f
pAppl Range
q) Range
q
       Sur -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL
q2] (QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Existential [VAR_DECL
q1] CASLFORMULA
forall f. FORMULA f
pAppl Range
q) Range
q
       Inj -> let
         q4 :: VAR_DECL
q4 = [Token] -> SORT -> Range -> VAR_DECL
Var_decl [String -> Token
mkSimpleId "c"] SORT
to Range
q
         t4 :: TERM f
t4 = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
q4
         in [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL
q1, VAR_DECL
q2, VAR_DECL
q4]
            (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation
             ([CASLFORMULA] -> Range -> CASLFORMULA
forall f. [FORMULA f] -> Range -> FORMULA f
conjunctRange
              [CASLFORMULA
forall f. FORMULA f
pAppl, PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
qp [TERM ()
forall f. TERM f
t1, TERM ()
forall f. TERM f
t4] Range
q] Range
q)
             Relation
Implication (TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM ()
forall f. TERM f
t2 Equality
Strong TERM ()
forall f. TERM f
t4 Range
q)
             Range
q) Range
q
       Sym | Bool
eqs -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL
q1, VAR_DECL
q2]
         (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
forall f. FORMULA f
pAppl Relation
Equivalence (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
qp [TERM ()
forall f. TERM f
t2, TERM ()
forall f. TERM f
t1] Range
q) Range
q) Range
q
       Asy | Bool
eqs -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL
q1, VAR_DECL
q2]
         (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
forall f. FORMULA f
pAppl Relation
Implication
          (CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
qp [TERM ()
forall f. TERM f
t2, TERM ()
forall f. TERM f
t1] Range
q) Range
q) Range
q) Range
q
       Trn | Bool
eqs -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL
q1, VAR_DECL
q2, VAR_DECL
q3]
          (CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation
           ([CASLFORMULA] -> Range -> CASLFORMULA
forall f. [FORMULA f] -> Range -> FORMULA f
conjunctRange [CASLFORMULA
forall f. FORMULA f
pAppl, PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
qp [TERM ()
forall f. TERM f
t2, TERM ()
forall f. TERM f
t3] Range
q] Range
q)
             Relation
Implication (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
qp [TERM ()
forall f. TERM f
t1, TERM ()
forall f. TERM f
t3] Range
q)
             Range
q) Range
q
       Rfx | Bool
eqs -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange [VAR_DECL
q1] (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
qp [TERM ()
forall f. TERM f
t1, TERM ()
forall f. TERM f
t1] Range
q) Range
q
       pr :: Prop
pr -> String -> CASLFORMULA
forall a. HasCallStack => String -> a
error (String -> CASLFORMULA) -> String -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ "getRelProp " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Prop -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Prop
pr ""

transRule :: CASLSign -> Rule
          -> State Int ((VAR, SORT), (VAR, SORT), CASLFORMULA)
transRule :: CASLSign
-> Rule -> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
transRule sig :: CASLSign
sig rule :: Rule
rule =
  let myMin :: (a, SORT) -> (a, SORT) -> (a, SORT)
myMin v :: (a, SORT)
v@(ta :: a
ta, sa :: SORT
sa) (_, sb :: SORT
sb)
        | CASLSign -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
leqSort CASLSign
sig SORT
sa SORT
sb = (a, SORT)
v
        | CASLSign -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
leqSort CASLSign
sig SORT
sb SORT
sa = (a
ta, SORT
sb)
        | Bool
otherwise = String -> (a, SORT)
forall a. HasCallStack => String -> a
error (String -> (a, SORT)) -> String -> (a, SORT)
forall a b. (a -> b) -> a -> b
$
            "transRule.myMin " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (SORT, SORT) -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (SORT
sa, SORT
sb) "\n " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rule -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Rule
rule ""
      myVarDecl :: (Token, SORT) -> VAR_DECL
myVarDecl = (Token -> SORT -> VAR_DECL) -> (Token, SORT) -> VAR_DECL
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Token -> SORT -> VAR_DECL
mkVarDecl
  in case Rule
rule of
  Tm m :: Relation
m@(Sgn (Token s :: String
s p :: Range
p) (RelType c1 :: Concept
c1 c2 :: Concept
c2)) -> do
      Int
i <- State Int Int
next
      Int
j <- State Int Int
next
      let v1 :: Token
v1 = String -> Int -> Token
mkNumVar "a" Int
i
          v2 :: Token
v2 = String -> Int -> Token
mkNumVar "b" Int
j
          isI :: Bool
isI = String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "I"
          ty1' :: SORT
ty1' = Concept -> SORT
conceptToId Concept
c1
          ty2' :: SORT
ty2' = Concept -> SORT
conceptToId Concept
c2
          ty1 :: SORT
ty1 = if Bool
isI Bool -> Bool -> Bool
&& CASLSign -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
leqSort CASLSign
sig SORT
ty2 SORT
ty1 then SORT
ty2' else SORT
ty1'
          ty2 :: SORT
ty2 = if Bool
isI Bool -> Bool -> Bool
&& CASLSign -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
leqSort CASLSign
sig SORT
ty1 SORT
ty2 then SORT
ty1' else SORT
ty2'
          q1 :: TERM f
q1 = Token -> SORT -> Range -> TERM f
forall f. Token -> SORT -> Range -> TERM f
Qual_var Token
v1 SORT
ty1 Range
p
          q2 :: TERM f
q2 = Token -> SORT -> Range -> TERM f
forall f. Token -> SORT -> Range -> TERM f
Qual_var Token
v2 SORT
ty2 Range
p
      ((Token, SORT), (Token, SORT), CASLFORMULA)
-> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Token
v1, SORT
ty1), (Token
v2, SORT
ty2),
        if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "V" then Bool -> Range -> CASLFORMULA
forall f. Bool -> Range -> FORMULA f
Atom Bool
True Range
p else
        if Bool
isI then
            if SORT
ty1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
ty2 then TERM () -> Equality -> TERM () -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation TERM ()
forall f. TERM f
q1 Equality
Strong TERM ()
forall f. TERM f
q2 Range
p else
                String -> CASLFORMULA
forall a. HasCallStack => String -> a
error (String -> CASLFORMULA) -> String -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ "transRule.I " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Rule -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Rule
rule ""
        else
          let qp :: PRED_SYMB
qp@(Qual_pred_name _ (Pred_type [fr :: SORT
fr, to :: SORT
to] _) _) = CASLSign -> Relation -> PRED_SYMB
getRelPred CASLSign
sig Relation
m
          in PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
qp
            [ if SORT
ty1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
fr then TERM ()
forall f. TERM f
q1 else TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM ()
forall f. TERM f
q1 SORT
fr Range
p
            , if SORT
ty2 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
to then TERM ()
forall f. TERM f
q2 else TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM ()
forall f. TERM f
q2 SORT
to Range
p] Range
p)
  UnExp o :: UnOp
o e :: Rule
e -> do
    (v1 :: (Token, SORT)
v1, v2 :: (Token, SORT)
v2@(t2 :: Token
t2, _), f :: CASLFORMULA
f) <- CASLSign
-> Rule -> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
transRule CASLSign
sig Rule
e
    case UnOp
o of
      Co -> ((Token, SORT), (Token, SORT), CASLFORMULA)
-> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Token, SORT)
v2, (Token, SORT)
v1, CASLFORMULA
f)
      Cp -> ((Token, SORT), (Token, SORT), CASLFORMULA)
-> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Token, SORT)
v1, (Token, SORT)
v2, CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
negateForm CASLFORMULA
f Range
nullRange)
      _ -> do
        Int
k <- State Int Int
next
        let v :: (Token, SORT)
v@(_, s :: SORT
s) = (Token, SORT) -> (Token, SORT) -> (Token, SORT)
forall a a. (a, SORT) -> (a, SORT) -> (a, SORT)
myMin (Token, SORT)
v1 (Token, SORT)
v2
            w :: (Token, SORT)
w = (Token
t2, SORT
s)
            nf :: CASLFORMULA
nf = CASLSign
-> (Token, SORT) -> (Token, SORT) -> CASLFORMULA -> CASLFORMULA
renameVar CASLSign
sig (Token, SORT)
v1 (Token, SORT)
v (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLSign
-> (Token, SORT) -> (Token, SORT) -> CASLFORMULA -> CASLFORMULA
renameVar CASLSign
sig (Token, SORT)
v2 (Token, SORT)
w CASLFORMULA
f
            z :: (Token, SORT)
z = (String -> Int -> Token
mkNumVar "c" Int
k, SORT
s)
            cf :: CASLFORMULA
cf = [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [(Token, SORT) -> VAR_DECL
myVarDecl (Token, SORT)
z]
                 (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLSign
-> (Token, SORT) -> (Token, SORT) -> CASLFORMULA -> CASLFORMULA
renameVar CASLSign
sig (Token, SORT)
v (Token, SORT)
z CASLFORMULA
nf, CASLSign
-> (Token, SORT) -> (Token, SORT) -> CASLFORMULA -> CASLFORMULA
renameVar CASLSign
sig (Token, SORT)
w (Token, SORT)
z CASLFORMULA
nf]
        -- this is (and always will be) incomplete wrt to compositions
        ((Token, SORT), (Token, SORT), CASLFORMULA)
-> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Token, SORT)
v, (Token, SORT)
w, [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct
           ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [ TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar (VAR_DECL -> TERM ()) -> VAR_DECL -> TERM ()
forall a b. (a -> b) -> a -> b
$ (Token, SORT) -> VAR_DECL
myVarDecl (Token, SORT)
v) (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> TERM ()
forall f. VAR_DECL -> TERM f
toQualVar (VAR_DECL -> TERM ()) -> VAR_DECL -> TERM ()
forall a b. (a -> b) -> a -> b
$ (Token, SORT) -> VAR_DECL
myVarDecl (Token, SORT)
w
             | UnOp
o UnOp -> UnOp -> Bool
forall a. Eq a => a -> a -> Bool
== UnOp
K0] [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA
nf, CASLFORMULA
cf])
  MulExp o :: MulOp
o es :: [Rule]
es -> case [Rule]
es of
    [] -> String -> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
forall a. HasCallStack => String -> a
error "transRule2"
    r :: Rule
r : t :: [Rule]
t -> if [Rule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Rule]
t then CASLSign
-> Rule -> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
transRule CASLSign
sig Rule
r else do
       (v1 :: (Token, SORT)
v1, v2 :: (Token, SORT)
v2, f1 :: CASLFORMULA
f1) <- CASLSign
-> Rule -> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
transRule CASLSign
sig Rule
r
       (v3 :: (Token, SORT)
v3, v4 :: (Token, SORT)
v4, f2 :: CASLFORMULA
f2) <- CASLSign
-> Rule -> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
transRule CASLSign
sig (Rule -> State Int ((Token, SORT), (Token, SORT), CASLFORMULA))
-> Rule -> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ MulOp -> [Rule] -> Rule
MulExp MulOp
o [Rule]
t
       if MulOp -> [MulOp] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem MulOp
o [MulOp
Fc, MulOp
Fd] then ((Token, SORT), (Token, SORT), CASLFORMULA)
-> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Token, SORT)
v1, (Token, SORT)
v4,
         let v23 :: (Token, SORT)
v23 = (Token, SORT) -> (Token, SORT) -> (Token, SORT)
forall a a. (a, SORT) -> (a, SORT) -> (a, SORT)
myMin (Token, SORT)
v2 (Token, SORT)
v3
             f3 :: CASLFORMULA
f3 = CASLSign
-> (Token, SORT) -> (Token, SORT) -> CASLFORMULA -> CASLFORMULA
renameVar CASLSign
sig (Token, SORT)
v2 (Token, SORT)
v23 CASLFORMULA
f1
             f4 :: CASLFORMULA
f4 = CASLSign
-> (Token, SORT) -> (Token, SORT) -> CASLFORMULA -> CASLFORMULA
renameVar CASLSign
sig (Token, SORT)
v3 (Token, SORT)
v23 CASLFORMULA
f2
             vs :: [VAR_DECL]
vs = [(Token, SORT) -> VAR_DECL
myVarDecl (Token, SORT)
v23]
             cs :: [CASLFORMULA]
cs = [CASLFORMULA
f3, CASLFORMULA
f4]
         in if MulOp
o MulOp -> MulOp -> Bool
forall a. Eq a => a -> a -> Bool
== MulOp
Fc then [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkExist [VAR_DECL]
vs (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
cs
              else [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
vs (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct [CASLFORMULA]
cs)
         else do
           let v13 :: (Token, SORT)
v13 = (Token, SORT) -> (Token, SORT) -> (Token, SORT)
forall a a. (a, SORT) -> (a, SORT) -> (a, SORT)
myMin (Token, SORT)
v1 (Token, SORT)
v3
               v24 :: (Token, SORT)
v24 = (Token, SORT) -> (Token, SORT) -> (Token, SORT)
forall a a. (a, SORT) -> (a, SORT) -> (a, SORT)
myMin (Token, SORT)
v2 (Token, SORT)
v4
               f3 :: CASLFORMULA
f3 = CASLSign
-> (Token, SORT) -> (Token, SORT) -> CASLFORMULA -> CASLFORMULA
renameVar CASLSign
sig (Token, SORT)
v1 (Token, SORT)
v13 (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLSign
-> (Token, SORT) -> (Token, SORT) -> CASLFORMULA -> CASLFORMULA
renameVar CASLSign
sig (Token, SORT)
v2 (Token, SORT)
v24 CASLFORMULA
f1
               f4 :: CASLFORMULA
f4 = CASLSign
-> (Token, SORT) -> (Token, SORT) -> CASLFORMULA -> CASLFORMULA
renameVar CASLSign
sig (Token, SORT)
v3 (Token, SORT)
v13 (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLSign
-> (Token, SORT) -> (Token, SORT) -> CASLFORMULA -> CASLFORMULA
renameVar CASLSign
sig (Token, SORT)
v4 (Token, SORT)
v24 CASLFORMULA
f2
           ((Token, SORT), (Token, SORT), CASLFORMULA)
-> State Int ((Token, SORT), (Token, SORT), CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Token, SORT)
v13, (Token, SORT)
v24, case MulOp
o of
             Fi -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA
f3, CASLFORMULA
f4]
             Fu -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
disjunct [CASLFORMULA
f3, CASLFORMULA
f4]
             Ri -> CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl CASLFORMULA
f3 CASLFORMULA
f4
             Rr -> CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
f4 Relation
RevImpl CASLFORMULA
f3 Range
nullRange
             Re -> CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv CASLFORMULA
f3 CASLFORMULA
f4
             _ -> String -> CASLFORMULA
forall a. HasCallStack => String -> a
error "transRule,MulExp")

renameVarRecord :: CASLSign -> (VAR, SORT) -> (VAR, SORT)
                -> Record () CASLFORMULA (TERM ())
renameVarRecord :: CASLSign
-> (Token, SORT)
-> (Token, SORT)
-> Record () CASLFORMULA (TERM ())
renameVarRecord sig :: CASLSign
sig from :: (Token, SORT)
from to :: (Token, SORT)
to = ((() -> ()) -> Record () CASLFORMULA (TERM ())
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord () -> ()
forall a. a -> a
id)
  { foldQual_var :: TERM () -> Token -> SORT -> Range -> TERM ()
foldQual_var = \ _ v :: Token
v ty :: SORT
ty p :: Range
p ->
      let (nv :: Token
nv, nty :: SORT
nty) = if (Token
v, SORT
ty) (Token, SORT) -> (Token, SORT) -> Bool
forall a. Eq a => a -> a -> Bool
== (Token, SORT)
from then (Token, SORT)
to else (Token
v, SORT
ty)
          qv :: TERM f
qv = Token -> SORT -> Range -> TERM f
forall f. Token -> SORT -> Range -> TERM f
Qual_var Token
nv SORT
nty Range
p
      in if SORT
nty SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
ty then TERM ()
forall f. TERM f
qv else
         if CASLSign -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
leqSort CASLSign
sig SORT
nty SORT
ty then TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM ()
forall f. TERM f
qv SORT
ty Range
p else
             String -> TERM ()
forall a. HasCallStack => String -> a
error "renameVar"
  }

renameVar :: CASLSign -> (VAR, SORT) -> (VAR, SORT) -> CASLFORMULA
          -> CASLFORMULA
renameVar :: CASLSign
-> (Token, SORT) -> (Token, SORT) -> CASLFORMULA -> CASLFORMULA
renameVar sig :: CASLSign
sig v :: (Token, SORT)
v = Record () CASLFORMULA (TERM ()) -> CASLFORMULA -> CASLFORMULA
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record () CASLFORMULA (TERM ()) -> CASLFORMULA -> CASLFORMULA)
-> ((Token, SORT) -> Record () CASLFORMULA (TERM ()))
-> (Token, SORT)
-> CASLFORMULA
-> CASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLSign
-> (Token, SORT)
-> (Token, SORT)
-> Record () CASLFORMULA (TERM ())
renameVarRecord CASLSign
sig (Token, SORT)
v