ExtModal2HasCASL.hs revision 1c3705f7c752c85afabf3e37a93a3ca9bd614df8
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederModule : $Header$
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederCopyright : (c) Christian Maeder, DFKI 2012
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederMaintainer : Christian.Maeder@dfki.de
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederStability : provisional
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederPortability : non-portable (MPTC-FD)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport qualified Common.Lib.Rel as Rel
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport qualified Common.Lib.MapSet as MapSet
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport qualified Data.Set as Set
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder-- ExtModalCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederdata ExtModal2HasCASL = ExtModal2HasCASL deriving (Show)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederinstance Language ExtModal2HasCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederinstance Comorphism ExtModal2HasCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder ExtModal EM.Sublogic EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder BasicSpec Sentence SymbItems SymbMapItems
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Env HC.Morphism HC.Symbol HC.RawSymbol () where
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder sourceLogic ExtModal2HasCASL = ExtModal
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder sourceSublogic ExtModal2HasCASL = maxSublogic
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder targetLogic ExtModal2HasCASL = HasCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder mapSublogic ExtModal2HasCASL _ = Just HC.caslLogic { which_logic = HOL }
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder map_theory ExtModal2HasCASL (sig, sens) = case transSig sig of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder mme -> return (mme, map (mapNamed $ transTop sig mme) sens)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder map_morphism ExtModal2HasCASL = return . mapMor
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder map_sentence ExtModal2HasCASL sig = return . transSen sig
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder map_symbol ExtModal2HasCASL _ = Set.singleton . mapSym
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder has_model_expansion ExtModal2HasCASL = True
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder is_weakly_amalgamable ExtModal2HasCASL = True
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomName :: Id -> Id
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomName t = Id [genToken "N"] [t] $ rangeOfId t
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomOpType :: OpType
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomOpType = mkTotOpType [] world
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder-- | add world arguments to flexible ops and preds; and add relations
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransSig :: ExtModalSign -> CASLSign
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransSig sign = let
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder s1 = embedSign () sign
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder extInf = extendedInfo sign
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder flexibleOps = flexOps extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder flexiblePreds = flexPreds extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder flexOps' = addWorldOp world addPlace flexibleOps
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder flexPreds' = addWorldPred world addPlace flexiblePreds
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder rigOps' = diffOpMapSet (opMap sign) flexibleOps
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder rigPreds' = diffMapSet (predMap sign) flexiblePreds
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder noms = nominals extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder noNomsPreds = Set.fold (`MapSet.delete` nomPType) rigPreds' noms
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder termMs = termMods extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder timeMs = timeMods extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder rels = Set.fold (\ m ->
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder insertModPred world (Set.member m timeMs) (Set.member m termMs) m)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder MapSet.empty $ modalities extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder nomOps = Set.fold (\ n -> addOpTo (nomName n) nomOpType) rigOps' noms
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder { sortRel = Rel.insertKey world $ sortRel sign
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , opMap = addOpMapSet flexOps' nomOps
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , assocOps = diffOpMapSet (assocOps sign) flexibleOps
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , predMap = addMapSet rels $ addMapSet flexPreds' noNomsPreds
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederdata Args = Args
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder { currentW :: TERM ()
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , nextW, freeC :: Int -- world variables
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , boundNoms :: [(Id, TERM ())]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , modSig :: ExtModalSign
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransTop :: ExtModalSign -> CASLSign -> FORMULA EM_FORMULA -> FORMULA ()
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransTop msig csig = let
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder vd = mkVarDecl (genNumVar "w" 1) world
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder vt = toQualVar vd
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder in stripQuant csig . mkForall [vd]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder . transMF (Args vt 1 1 [] msig)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedergetTermOfNom :: Args -> Id -> TERM ()
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedergetTermOfNom as i = fromMaybe (mkNomAppl i) . lookup i $ boundNoms as
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder-- TODO: check that constructors are not flexible!
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedermkNomAppl :: Id -> TERM ()
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedermkNomAppl pn = mkAppl (mkQualOp (nomName pn) $ toOP_TYPE nomOpType) []
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransRecord :: Args -> Record EM_FORMULA (FORMULA ()) (TERM ())
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransRecord as = let
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder extInf = extendedInfo $ modSig as
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder currW = currentW as
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder in (mapRecord $ const ())
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder { foldPredication = \ _ ps args r -> case ps of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Qual_pred_name pn pTy@(Pred_type srts q) p
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder | MapSet.member pn (toPredType pTy) $ flexPreds extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder -> Predication
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder (Qual_pred_name (addPlace pn) (Pred_type (world : srts) q) p)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder (currW : args) r
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder | null srts && Set.member pn (nominals extInf)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder -> mkStEq currW $ getTermOfNom as pn
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder _ -> Predication ps args r
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , foldExtFORMULA = \ _ f -> transEMF as f
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , foldApplication = \ _ os args r -> case os of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Qual_op_name opn oTy@(Op_type ok srts res q) p
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder | MapSet.member opn (toOpType oTy) $ flexOps extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder -> Application
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder (Qual_op_name (addPlace opn) (Op_type ok (world : srts) res q) p)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder (currW : args) r
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder _ -> Application os args r
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransMF :: Args -> FORMULA EM_FORMULA -> FORMULA ()
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransMF = foldFormula . transRecord
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederdisjointVars :: [VAR_DECL] -> [FORMULA ()]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederdisjointVars vs = case vs of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder a : r@(b : _) -> mkNeg (on mkStEq toQualVar a b) : disjointVars r
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransEMF :: Args -> EM_FORMULA -> FORMULA ()
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransEMF as emf = case emf of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder PrefixForm pf f r -> let
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder fW = freeC as
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder in case pf of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder BoxOrDiamond bOp m gEq i -> let
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder ex = bOp == Diamond
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder l = [fW + 1 .. fW + i]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder vds = map (\ n -> mkVarDecl (genNumVar "w" n) world) l
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder nAs = as { freeC = fW + i }
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder tf n = transMF nAs { currentW = mkVarTerm (genNumVar "w" n) world } f
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder tM n = transMod nAs { nextW = n } m
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder conjF = conjunct $ map tM l ++ map tf l ++ disjointVars vds
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder diam = BoxOrDiamond Diamond m True
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder tr b = transEMF as $ PrefixForm (BoxOrDiamond b m gEq i) f r
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder in if gEq && i > 0 && (i == 1 || ex) then case bOp of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Diamond -> mkExist vds conjF
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Box -> mkForall vds conjF
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder EBox -> conjunct [mkExist vds conjF, mkForall vds conjF]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder else if i <= 0 && ex && gEq then trueForm
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder else if bOp == EBox then conjunct $ map tr [Diamond, Box]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder else if ex -- lEq
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder then transMF as . mkNeg . ExtFORMULA $ PrefixForm
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder (diam $ i + 1) f r
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder else if gEq -- Box
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder then transMF as . mkNeg . ExtFORMULA $ PrefixForm
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder (diam i) (mkNeg f) r
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder else transMF as . ExtFORMULA $ PrefixForm
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder (diam $ i + 1) (mkNeg f) r
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Hybrid at i -> let ni = simpleIdToId i in
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder if at then transMF as { currentW = getTermOfNom as ni } f else let
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder vi = mkVarDecl (genNumVar "i" $ fW + 1) world
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder ti = toQualVar vi
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder in mkExist [vi] $ conjunct
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder [ mkStEq ti $ currentW as
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , transMF as { boundNoms = (ni, ti) : boundNoms as
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , currentW = ti
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , freeC = fW + 1 } f ]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder _ -> transMF as f
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder UntilSince _isUntil f1 f2 r -> conjunctRange [transMF as f1, transMF as f2] r
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder ModForm _ -> trueForm
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransMod :: Args -> MODALITY -> FORMULA ()
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransMod as md = let
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder t1 = currentW as
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder t2 = mkVarTerm (genNumVar "w" $ nextW as) world
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder vts = [t1, t2]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder msig = modSig as
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder extInf = extendedInfo msig
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder timeMs = timeMods extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder in case md of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder SimpleMod i -> let ri = simpleIdToId i in mkPredication
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder (mkQualPred (relOfMod (Set.member ri timeMs) False ri)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder . toPRED_TYPE $ modPredType world False ri) vts
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder TermMod t -> case optTermSort t of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Just srt -> case keepMinimals msig id . Set.toList
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder . Set.intersection (termMods extInf) . Set.insert srt
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder $ supersortsOf srt msig of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder [] -> error $ "transMod1: " ++ showDoc t ""
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder st : _ -> mkPredication
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder (mkQualPred (relOfMod (Set.member st timeMs) True st)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder . toPRED_TYPE $ modPredType world True st)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder $ foldTerm (transRecord as) t : vts
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder _ -> error $ "transMod2: " ++ showDoc t ""
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Guard f -> conjunct [mkExEq t1 t2, transMF as f]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder ModOp mOp m1 m2 -> case mOp of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Composition -> let
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder nW = freeC as + 1
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder nAs = as { freeC = nW }
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder vd = mkVarDecl (genNumVar "w" nW) world
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder in mkExist [vd] $ conjunct
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder [ transMod nAs { nextW = nW } m1
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder , transMod nAs { currentW = toQualVar vd } m2 ]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Intersection -> conjunct [transMod as m1, transMod as m2] -- parallel?
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Union -> disjunct [transMod as m1, transMod as m2]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder OrElse -> disjunct . transOrElse [] as $ flatOrElse md
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder TransClos m -> transMod as m -- ignore transitivity for now
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederflatOrElse :: MODALITY -> [MODALITY]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederflatOrElse md = case md of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder ModOp OrElse m1 m2 -> flatOrElse m1 ++ flatOrElse m2
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransOrElse :: [FORMULA EM_FORMULA] -> Args -> [MODALITY] -> [FORMULA ()]
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedertransOrElse nFs as ms = case ms of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder md : r -> case md of
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Guard f -> transMod as (Guard . conjunct $ f : nFs)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder : transOrElse (mkNeg f : nFs) as r
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder _ -> transMod as md : transOrElse nFs as r