Adl2CASL.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiDescription : Coding a description language into CASL
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Stef Joosten, Christian Maeder DFKI GmbH 2010
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : Christian.Maeder@dfki.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : experimental
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (imports Logic.Logic)
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiThe translating comorphism from Adl to CASL.
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski ( Adl2CASL (..)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport qualified Common.Lib.Rel as Rel
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport qualified Data.Set as Set
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport qualified Data.Map as Map
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- | lid of the morphism
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata Adl2CASL = Adl2CASL deriving Show
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance Language Adl2CASL -- default is ok
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Comorphism Adl2CASL
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder CASL_Sublogics
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder CASLBasicSpec
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder SYMB_MAP_ITEMS
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maeder sourceLogic Adl2CASL = Adl
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maeder sourceSublogic Adl2CASL = ()
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maeder targetLogic Adl2CASL = CASL
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder mapSublogic Adl2CASL _ = Just $ caslTop
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder { has_part = False
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , sub_features = LocFilSub
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , cons_features = NoSortGen }
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder map_theory Adl2CASL = mapTheory
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder map_sentence Adl2CASL s = return . mapSen (mapSign s)
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder map_morphism Adl2CASL = mapMor
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder map_symbol Adl2CASL _ = Set.singleton . mapSym
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder is_model_transportable Adl2CASL = True
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder has_model_expansion Adl2CASL = True
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski is_weakly_amalgamable Adl2CASL = True
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski isInclusionComorphism Adl2CASL = True
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapTheory :: (A.Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapTheory (s, ns) = let cs = mapSign s in
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder return (cs, map (mapNamed $ mapSen cs) ns)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederrelTypeToPred :: RelType -> PredType
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederrelTypeToPred (RelType c1 c2) = PredType [conceptToId c1, conceptToId c2]
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedermapSign :: A.Sign -> CASLSign
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedermapSign s = (C.emptySign ())
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder { sortSet = Set.fold (\ sy -> case sy of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Con (C i) -> Set.insert $ simpleIdToId i
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , sortRel = Rel.map conceptToId $ isas s
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , predMap = Map.fromList . map (\ (i, l) -> (transRelId $ idToSimpleId i, l))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski . Map.toList . Map.map (Set.map relTypeToPred) $ rels s
4fc727afa544a757d1959ce77c02208f8bf330dcChristian MaedertransRelId :: Token -> Id
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedertransRelId t@(Token s p) = simpleIdToId $
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder if elem s casl_reserved_fwords then Token ("P_" ++ s) p else t
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedermapSen :: CASLSign -> Sen -> CASLFORMULA
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedermapSen sig s = case s of
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder DeclProp r p -> getRelProp sig r p
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Assertion _ r ->
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder let ((v1, s1), (v2, s2), f) = evalState (transRule sig r) 1 in
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder mkForall [mkVarDecl v1 s1, mkVarDecl v2 s2] f nullRange
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- | Translation of morphisms
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermapMor :: A.Morphism -> Result CASLMor
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedermapMor mor = return $ embedMorphism ()
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (mapSign $ domOfDefaultMorphism mor) $ mapSign $ codOfDefaultMorphism mor
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermapSym s = case s of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Con c -> idToSortSymbol $ conceptToId c
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Rel (Sgn n t) -> idToPredSymbol (transRelId n) $ relTypeToPred t
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedernext :: State Int Int
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedergetRelPred :: CASLSign -> Relation -> PRED_SYMB
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedergetRelPred sig m@(Sgn t (RelType c1 c2)) = let
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ty1 = conceptToId c1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ty2 = conceptToId c2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder i = transRelId t
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder cs = filter (\ pt -> case predArgs pt of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder [fr, to] -> leqSort sig ty1 fr && leqSort sig ty2 to
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $ Set.toList $ Map.findWithDefault Set.empty i
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder $ predMap sig
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in case cs of
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Qual_pred_name i (toPRED_TYPE ty) $ tokPos t
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski _ -> error $ "getRelPred " ++ showDoc m ""
612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaedergetRelProp :: CASLSign -> Relation -> RangedProp -> CASLFORMULA
5e46b572ed576c0494768998b043d9d340594122Till MossakowskigetRelProp sig r p =
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder let qp@(Qual_pred_name _ (Pred_type [fr, to] _) _) = getRelPred sig r
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder q = propRange p
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder q1 = Var_decl [mkSimpleId "a"] fr q
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder q2 = Var_decl [mkSimpleId "b"] to q
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder q3 = Var_decl [mkSimpleId "c"] fr q
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder t1 = toQualVar q1
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder t2 = toQualVar q2
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder t3 = toQualVar q3
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder pAppl = Predication qp [t1, t2] q
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder eqs = fr == to
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder in case propProp p of
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Uni -> mkForall [q1, q2, q3]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski [pAppl, Predication qp [t3, t2] q] q)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Strong_equation t1 t3 q)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Tot -> mkForall [q1] (Quantification Existential [q2] pAppl q) q
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Sur -> mkForall [q2] (Quantification Existential [q1] pAppl q) q
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski q4 = Var_decl [mkSimpleId "c"] to q
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski t4 = toQualVar q4
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in mkForall [q1, q2, q4]
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski [pAppl, Predication qp [t1, t4] q] q)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Strong_equation t2 t4 q)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mkForall [q1, q2] (Equivalence pAppl (Predication qp [t2, t1] q) q) q
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Asy | eqs -> mkForall [q1, q2]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Implication pAppl (Negation (Predication qp [t2, t1] q) q) True q) q
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Trn | eqs -> mkForall [q1, q2, q3]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Conjunction [pAppl, Predication qp [t2, t3] q] q)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (Predication qp [t1, t3] q)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Rfx | eqs -> mkForall [q1] (Predication qp [t1, t1] q) q
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder pr -> error $ "getRelProp " ++ showDoc pr ""
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitransRule :: CASLSign -> Rule
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> State Int ((VAR, SORT), (VAR, SORT), CASLFORMULA)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitransRule sig rule =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let myMin v@(ta, sa) (_, sb) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if leqSort sig sa sb then v else
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if leqSort sig sb sa then (ta, sb) else
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder error $ "transRule.myMin " ++ showDoc (sa, sb) "\n "
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ++ showDoc rule ""
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder myVarDecl = uncurry mkVarDecl
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder disjunct fs = Disjunction fs nullRange
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder mkExist vs f = Quantification Existential vs f nullRange
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder in case rule of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Tm m@(Sgn (Token s p) (RelType c1 c2)) -> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let v1 = mkNumVar "a" i
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder v2 = mkNumVar "b" j
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder isI = s == "I"
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski ty1' = conceptToId c1
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ty2' = conceptToId c2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ty1 = if isI && leqSort sig ty2 ty1 then ty2' else ty1'
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ty2 = if isI && leqSort sig ty1 ty2 then ty1' else ty2'
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder q1 = Qual_var v1 ty1 p
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder q2 = Qual_var v2 ty2 p
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return ((v1, ty1), (v2, ty2),
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder if s == "V" then True_atom p else
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder if ty1 == ty2 then Strong_equation q1 q2 p else
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder error $ "transRule.I " ++ showDoc rule ""
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let qp@(Qual_pred_name _ (Pred_type [fr, to] _) _) = getRelPred sig m
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder in Predication qp
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder [ if ty1 == fr then q1 else Sorted_term q1 fr p
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , if ty2 == to then q2 else Sorted_term q2 to p] p)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder UnExp o e -> do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (v1, v2@(t2, _), f) <- transRule sig e
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Co -> return (v2, v1, f)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Cp -> return (v1, v2, negateForm f nullRange)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder let v@(_, s) = myMin v1 v2
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder nf = renameVar sig v1 v $ renameVar sig v2 w f
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder z = (mkNumVar "c" k, s)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder cf = mkExist [myVarDecl z]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder $ conjunct [renameVar sig v z nf, renameVar sig w z nf]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder -- this is (and always will be) incomplete wrt to compositions
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder return (v, w, disjunct
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder $ [ mkStEq (toQualVar $ myVarDecl v) $ toQualVar $ myVarDecl w
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder | o == K0] ++ [nf, cf])
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder MulExp o es -> case es of
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder [] -> error "transRule2"
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder r : t -> if null t then transRule sig r else do
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (v1, v2, f1) <- transRule sig r
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (v3, v4, f2) <- transRule sig $ MulExp o t
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder if elem o [Fc, Fd] then return (v1, v4,
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder let v23 = myMin v2 v3
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder f3 = renameVar sig v2 v23 f1
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder f4 = renameVar sig v3 v23 f2
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder vs = [myVarDecl v23]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder cs = [f3, f4]
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder in if o == Fc then mkExist vs $ conjunct cs
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder else mkForall vs (disjunct cs) nullRange)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder let v13 = myMin v1 v3
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder v24 = myMin v2 v4
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder f3 = renameVar sig v1 v13 $ renameVar sig v2 v24 f1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski f4 = renameVar sig v3 v13 $ renameVar sig v4 v24 f2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (v13, v24, case o of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Fi -> conjunct [f3, f4]
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Fu -> disjunct [f3, f4]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Ri -> mkImpl f3 f4
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Rr -> Implication f4 f3 False nullRange
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder Re -> mkEqv f3 f4
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder _ -> error "transRule,MulExp")
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederrenameVarRecord :: CASLSign -> (VAR, SORT) -> (VAR, SORT)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder -> Record () CASLFORMULA (TERM ())
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederrenameVarRecord sig from to = (mapRecord id)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder { foldQual_var = \ _ v ty p ->
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let (nv, nty) = if (v, ty) == from then to else (v, ty)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder qv = Qual_var nv nty p
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder in if nty == ty then qv else
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder if leqSort sig nty ty then Sorted_term qv ty p else
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder error "renameVar"
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederrenameVar :: CASLSign -> (VAR, SORT) -> (VAR, SORT) -> CASLFORMULA
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder -> CASLFORMULA
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederrenameVar sig v = foldFormula . renameVarRecord sig v