81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder{-# LANGUAGE ExistentialQuantification #-}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederLicense : GPLv2 or higher, see LICENSE.txt
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederMaintainer : nevrenato@gmail.com
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederStability : experimental
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederPortability : not portable
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederStatic analysis of hybrid logic with an arbitrary logic below.
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroedermodule TopHybrid.StatAna (thAna, anaForm', simSen) where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederimport CASL.Sign -- Symbols, this should be removed...
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederbimap :: (t1 -> t2) -> (s1 -> s2) -> (t1, s1) -> (t2, s2)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederbimap f g (a, b) = (f a, g b)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder-- | Collects the newly declared nomies and modies
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroedercolnomsMods :: [TH_BASIC_ITEM] -> ([MODALITY], [NOMINAL])
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroedercolnomsMods = Data.List.foldr f ([], [])
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder where f (Simple_mod_decl ms) = bimap (++ ms) id
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder f (Simple_nom_decl ns) = bimap id (++ ns)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder{- | Adds the newly declared nomies/modies, and the analysed base
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroedersignature to a new sig
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederchecking for redundancy of modalities and nominals declarations
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederNote : If there are repeated declarations, the size of the sets should
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederbe differnt that the size of the lists -}
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroedertopAna :: (Logic l sub bs sen si smi sign mor symb raw pf) =>
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder [TH_BASIC_ITEM] -> l -> sign -> Result Sgn_Wrap
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedertopAna ds l sig = if not rep then return newSig else mkHint newSig msg
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder x = colnomsMods ds
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder x' = bimap fromList fromList x
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder rep = size (uncurry Data.Set.union x') /=
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder length (uncurry (++) x)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder s = uncurry THybridSign x' sig
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder newSig = Sgn_Wrap l s
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder msg = maybeE 0 Nothing
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder{- Checks if the modalities and nominals referred in a sentence, really exist
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederin the signature -}
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroedernomOrModCheck :: (Pretty f, GetRange f) => Set SIMPLE_ID -> SIMPLE_ID ->
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder TH_FORMULA f -> Result (TH_FORMULA f)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroedernomOrModCheck xs x = if member x xs then return else mkError msg
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder where msg = maybeE 1 Nothing
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder{- | Top Formula analyser
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederThe l argument could be discarded, but then we would need an extra unsafe
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederfunction, to convert the spec type...
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederAs l corresponds to the underlying logic bs should correspond to the
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederunderlying spec, as some formula analysers need the spec associated
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederanaForm :: (Logic l sub bs sen si smi sign mor symb raw pf) =>
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder l -> bs -> Sgn_Wrap -> Frm_Wrap -> Result Frm_Wrap
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederanaForm l bs s (Frm_Wrap _ f) = liftM (Frm_Wrap l) $ unroll l bs s f
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder{- Static analysis of an hybridized sentence, when it's called by an upper
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederlevel logic. (This is only used when we want to analyse 2 or more times
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederhybridized, sentences). Probably this function can be merged smoothly with
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederthe above. I will check this later
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederAn hybridized sentence, with the correpondent sign already built, doesn't
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederneed the top spec, hence we can discard it and just use the underlying (und) -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederanaForm' :: (Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederanaForm' (Spc_Wrap l bs _, s, f) = anaForm l (und bs) s f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- | Unrolling the formula, so that we can analyse it further
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederunroll :: (Show f, GetRange f, ShATermConvertible f,
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder Logic l sub bs sen sy sm si mo sy' rs pf) =>
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder l -> bs -> Sgn_Wrap -> TH_FORMULA f -> Result (TH_FORMULA sen)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederunroll l bs s'@(Sgn_Wrap _ s) f =
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (At n f') -> liftM (At n) $ unroll l bs s' f' >>=
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder nomOrModCheck (nomies s) n
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (Box m f') -> liftM (Box m) $ unroll l bs s' f' >>=
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder nomOrModCheck (modies s) m
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (Dia m f') -> liftM (Dia m) $ unroll l bs s' f' >>=
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder nomOrModCheck (modies s) m
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (Conjunction f' f'') -> liftM2 Conjunction
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (unroll l bs s' f')
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (unroll l bs s' f'')
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (Disjunction f' f'') -> liftM2 Disjunction
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (unroll l bs s' f')
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (unroll l bs s' f'')
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (Implication f' f'') -> liftM2 Implication
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (unroll l bs s' f')
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (unroll l bs s' f'')
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (BiImplication f' f'') -> liftM2 BiImplication
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (unroll l bs s' f')
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (unroll l bs s' f'')
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (Here n) -> nomOrModCheck (nomies s) n $ Here n
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (Neg f') -> liftM Neg (unroll l bs s' f')
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (Uni n f') -> (liftM $ Uni n) (unroll l bs
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (addNomToSig n s') f') >>= checkForRepNom n (nomies s)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (Exist n f') -> (liftM $ Exist n) (unroll l bs
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (addNomToSig n s') f') >>= checkForRepNom n (nomies s)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (UnderLogic f') ->
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder liftM UnderLogic $ undFormAna l (extended s) f' bs
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (Par f') -> liftM Par (unroll l bs s' f')
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder TrueA -> return TrueA
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder FalseA -> return FalseA
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederunroll _ _ EmptySign _ = error "Signature not computable"
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- helper function
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddNomToSig :: NOMINAL -> Sgn_Wrap -> Sgn_Wrap
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederaddNomToSig n (Sgn_Wrap l s) = Sgn_Wrap l s
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder { nomies = Data.Set.insert n $ nomies s}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederaddNomToSig _ EmptySign = error "Signature not computable"
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroedercheckForRepNom :: (Pretty f, GetRange f) =>
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder NOMINAL -> Set NOMINAL -> TH_FORMULA f -> Result (TH_FORMULA f)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroedercheckForRepNom n s = if member n s
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder then mkError "conflict in nominal decl and quantification"
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder{- | Lift of the formula analyser
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederAnalyses each formula and collects the results. Converting also the
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederannotations to the correct format. The function flipM is needed because
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederwe want the annotations independent from the analyser -}
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederanaForms :: (Logic l sub bs sen si smi sign mor symb raw pf) =>
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder l -> bs -> [Annoted Frm_Wrap] -> Sgn_Wrap -> Result [Named Frm_Wrap]
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederanaForms l bs f s = mapM (flipM . makeNamedSen . fmap (anaForm l bs s)) f
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder-- Just flips the monad position with the functor
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederflipM :: (Monad m) => Named (m a) -> m (Named a)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederflipM y = sentence y >>= \ a -> return $ mapNamed (const a) y
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder{- | Examining the list of formulas and collecting results
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederAnalyses first the underlying spec; Then analyses the top spec
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder(without the axioms) and merges the resulting sig with the underlying one.
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederAlso translates the underlying axioms into hybridized ones, so that in the
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederend all axioms are of the same type;
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederNext analyses the hybrid axioms and puts them together with the already
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroedertranslated axioms.
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederFinnaly prepares the tuple format for outputting. -}
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederthAna :: (Spc_Wrap, Sgn_Wrap, GlobalAnnos) ->
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederthAna (Spc_Wrap l sp fs, _, _) = finalRes
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder undA = undAna l $ und sp
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder partMerge = undA >>= \ (x1, x2, x3) -> topAna (bitems sp) l
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder (plainSign x2) >>= \ x -> return (x1, x, formMap x3)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder partMerge' = partMerge >>= \ (x1, x2, x3) ->
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder anaForms l x1 fs x2 >>= \ x -> return (x1, x2, x3 ++ x)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder finalRes = partMerge' >>= \ (x1, x2, x3) ->
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder return (mergSpec x1, mkExtSign x2, x3)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder formMap = Data.List.map $ mapNamed $ Frm_Wrap l . UnderLogic
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder mergSpec e = Spc_Wrap l (Bspec (bitems sp) e) fs
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder-- Analysis of the underlying logic spec
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederundAna :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder l -> bs -> Result (bs, ExtSign sign symb, [Named sen])
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederundAna l b = (maybeE 2 $ basic_analysis l) x
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder where x = (b, empty_signature l, emptyGlobalAnnos)
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederunsafeToForm :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederunsafeToForm _ = unsafeCoerce
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederunsafeToSig :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederunsafeToSig _ = unsafeCoerce
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder{- Analysis of the sentences part the corresponds to the underlying logic. We
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder need to use the unsafe functions here, because the typechecker has no way
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder to check the (simple) relations (l -> sig) and (l -> sen). In other words
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder it can't check that the arguments l and a belong to the Logic class,
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder likewise for l -> b. The unsafe functions will give the "right"
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder type associated with l. -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroederundFormAna :: (StaticAnalysis l bs sen si smi sign mor symb raw) =>
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder l -> a -> b -> bs -> Result sen
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederundFormAna l a b c = (maybeE 4 $ sen_analysis l) (c, a', b')
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder where a' = unsafeToSig l a
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder b' = unsafeToForm l b
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder{- -- Operations on sentences ----
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroederHow can we guarantee that the l in Sgn_Wrap is equal
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederto the l in Frm_Wrap ? -}
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedersimSen :: Sgn_Wrap -> Frm_Wrap -> Frm_Wrap
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von SchroedersimSen (Sgn_Wrap _ s) (Frm_Wrap l f) = Frm_Wrap l $
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder uroll l (unsafeCoerce (extended s)) f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von SchroedersimSen EmptySign _ = error "The signature cannot be empty"
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederuroll :: (Logic l sub bs f s sm sgn mo sy rw pf) =>
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder l -> sgn -> TH_FORMULA f -> TH_FORMULA f
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederuroll l s f = case f of
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder At n f' -> At n $ uroll l s f'
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Box m f' -> Box m $ uroll l s f'
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Dia m f' -> Dia m $ uroll l s f'
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Conjunction f' f'' -> Conjunction (uroll l s f') $ uroll l s f''
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Disjunction f' f'' -> Disjunction (uroll l s f') $ uroll l s f''
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Implication f' f'' -> Implication (uroll l s f') $ uroll l s f''
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder BiImplication f' f'' -> BiImplication (uroll l s f') $
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Here n -> Here n
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Neg f' -> Neg $ uroll l s f'
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder Par f' -> Par $ uroll l s f'
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder UnderLogic f' -> UnderLogic $ simplify_sen l s f'
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder{- These instances should be automatically generated by DriFT, but it cannot
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroedersince they are not declared in a usual format -}
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroederinstance ShATermConvertible Sgn_Wrap where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder toShATermAux att (Sgn_Wrap _ s) = toShATermAux att s
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder toShATermAux _ EmptySign = error "I entered in emptySign"
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder fromShATermAux _ _ = error "I entered here"
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance ShATermConvertible Spc_Wrap where
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder toShATermAux att (Spc_Wrap _ s _) = toShATermAux att s
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder fromShATermAux _ _ = error "I entered here"
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroederinstance ShATermConvertible Frm_Wrap where
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder toShATermAux att (Frm_Wrap _ f) = toShATermAux att f
ffd328462d99eb679e14c0d81e8dde21e046c59fJonathan von Schroeder fromShATermAux _ _ = error "I entered here"