Utils.hs revision 0095c7efbddd0ffeed6aaf8ec015346be161d819
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian MaederCopyright : (c) Klaus L�ttich and Uni Bremen 2002-2004
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian MaederMaintainer : luettich@tzi.de
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian MaederStability : provisional
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian MaederPortability : portable
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian MaederDescription : module to store utilities for CASL and its comorphisms
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian Maederimport qualified Common.Lib.Set as Set
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian Maederimport qualified Common.Lib.Map as Map
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder-- replacePropPredication replaces a propositional predication of a
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder-- given symbol with an also given formula. Optionally a given variable
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder-- is replaced in the predication of another predicate symbol with a
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder-- given term, the variable must occur in the first argument position
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder-- of the predication.
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian MaederreplacePropPredication :: Maybe (PRED_NAME,VAR,TERM f)
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian Maeder -- ^ Just (pSymb,x,t) replace x
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu -- with t in Predication of pSymb
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -> PRED_NAME -- ^ propositional symbol to replace
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -> FORMULA f -- ^ Formula to insert
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu -> FORMULA f -- ^ Formula with placeholder
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai CodescureplacePropPredication mTerm pSymb frmIns =
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu foldFormula (mapRecord $ const $ error
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder "replacePropPredication: unexpected extended formula")
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu { foldPredication = \ (Predication qpn ts ps) _ _ _ ->
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu let (pSymbT,var,term) = fromJust mTerm in case qpn of
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu Qual_pred_name symb (Pred_type s _) _
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu | symb == pSymb && null ts && null s -> frmIns
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu | isJust mTerm && symb == pSymbT -> case ts of
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu Sorted_term (Qual_var v1 _ _) _ _ : args
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu | v1 == var -> Predication qpn (term:args) ps
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu _ -> error "replacePropPredication: unknown term to replace"
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu _ -> error "replacePropPredication: unknown formula to replace"
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian Maeder , foldConditional = \ t _ _ _ _ -> t }
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian Maeder-- noMixfixF checks a 'FORMULA' f for Mixfix_*.
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder-- A logic specific helper has to be provided for checking the f.
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaedernoMixfixF :: (f -> Bool) -> FORMULA f -> Bool
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian MaedernoMixfixF = foldFormula . noMixfixRecord
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder-- noMixfixT checks a 'TERM' f for Mixfix_*.
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu-- A logic specific helper has to be provided for checking the f.
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian MaedernoMixfixT :: (f -> Bool) -> TERM f -> Bool
62d5dbbceb675837039e6bad0971c324cce96a21Mihai CodescunoMixfixT = foldTerm . noMixfixRecord
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maedertype FreshVARMap f = Map.Map VAR (TERM f)
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder-- | build_vMap constructs a mapping between a list of old variables and
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu-- corresponding fresh variables based on two lists of VAR_DECL
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maederbuild_vMap :: [VAR_DECL] -> [VAR_DECL] -> FreshVARMap f
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescubuild_vMap vDecls f_vDecls =
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu Map.fromList (concat (zipWith toTups vDecls f_vDecls))
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder where toTups (Var_decl vars1 sor1 _) (Var_decl vars2 sor2 _) =
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu assert (sor1 == sor2)
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu (zipWith (toTup sor1) vars1 vars2)
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu toTup s v1 v2 = (v1,toVarTerm v2 s)
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu-- | specialised lookup in FreshVARMap that ensures that the VAR with
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu-- the correct type (SORT) is replaced
ab2ff2c8e08cd0f13064b87348f78a00775c54e5Mihai Codesculookup_vMap :: VAR -> SORT -> FreshVARMap f -> Maybe (TERM f)
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codesculookup_vMap v s m =
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu maybe Nothing
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder (\ t@(Qual_var _ s' _) -> if s==s' then Just t else Nothing)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder-- | specialized delete that deletes all shadowed variables
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederdelete_vMap :: [VAR_DECL] -> FreshVARMap f -> FreshVARMap f
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescudelete_vMap vDecls m = foldr Map.delete m vars
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder where vars = concatMap (\ (Var_decl vs _ _) -> vs) vDecls
62d5dbbceb675837039e6bad0971c324cce96a21Mihai CodescureplaceVarsRec :: FreshVARMap f -> (f -> f) -> Record f (FORMULA f) (TERM f)
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederreplaceVarsRec m mf = (mapRecord mf)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder { foldQual_var = \ qv v s _ ->
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu maybe qv id (lookup_vMap v s m)
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian Maeder , foldQuantification = \ (Quantification q vs f ps) _ _ _ _ ->
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu let nm = delete_vMap vs m
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu in Quantification q vs (replace_varsF nm mf f) ps
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder-- | replace_vars replaces all Qual_var occurences that are supposed
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu-- to be replaced according to the FreshVARMap
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescureplace_varsF :: FreshVARMap f
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu -- ^ this function replaces Qual_var in ExtFORMULA
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder -> FORMULA f -> FORMULA f
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescureplace_varsF m mf phi = foldFormula (replaceVarsRec m mf) phi
62d5dbbceb675837039e6bad0971c324cce96a21Mihai CodescucodeOutUniqueRecord :: (f -> f) -> (f -> f) -> Record f (FORMULA f) (TERM f)
62d5dbbceb675837039e6bad0971c324cce96a21Mihai CodescucodeOutUniqueRecord rf mf = (mapRecord mf)
ab2ff2c8e08cd0f13064b87348f78a00775c54e5Mihai Codescu { foldQuantification = \ _ q vDecl f' ps ->
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu Unique_existential -> let
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder eqForms (Var_decl vars1 sor1 _) (Var_decl vars2 sor2 _) =
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu assert (sor1 == sor2)
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu (zipWith (eqFor sor1) vars1 vars2)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder eqFor s v1 v2 = Strong_equation (toSortTerm (toVarTerm v1 s))
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (toSortTerm (toVarTerm v2 s))
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder -- fresh_vars produces new variables based on a list
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian Maeder -- of defined variables
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu -- args: (1) set of already used variable names
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder -- (2) list of variables
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder fresh_vars = mapAccumL fresh_var
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu fresh_var accSet (Var_decl vars sor _) =
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu let accSet' = Set.union (Set.fromList vars) accSet
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu (accSet'',vars') = mapAccumL nVar accSet' vars
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian Maeder in (accSet'',Var_decl vars' sor nullRange)
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian Maeder genVar t i = mkSimpleId $ tokStr t ++ '_' : show i
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder nVar aSet v =
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu let v' = fromJust (find (not . flip Set.member aSet)
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu ([genVar v (i :: Int) | i<-[1..]]))
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu in (Set.insert v' aSet,v')
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu (vSet', vDecl') = fresh_vars Set.empty vDecl
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu (_vSet'', vDecl'') = fresh_vars vSet' vDecl
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu f'_rep_x = replace_varsF (build_vMap vDecl vDecl') rf f'
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu f'_rep_y = replace_varsF (build_vMap vDecl vDecl'') rf f'
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu allForm = Quantification Universal (vDecl'++vDecl'')
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (Conjunction [f'_rep_x,f'_rep_y] nullRange)
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu implForm True ps) nullRange
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu implForm = assert (not (null vDecl))
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu (let fs = concat (zipWith eqForms vDecl' vDecl'')
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu in (if length fs == 1
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu else Conjunction fs nullRange))
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder in Conjunction
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [Quantification Existential vDecl f' ps,
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu _ -> Quantification q vDecl f' ps
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder-- | codeOutUniqueExtF compiles every unique_existential quantification
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu-- to simple quantifications. It works recursively through the whole
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder-- formula and only touches Unique_existential quantifications
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder-- exists! x . phi(x) ==>
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu-- (exists x. phi(x)) /\ (forall x,y . phi(x) /\ phi(y) => x=y)
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai CodescucodeOutUniqueExtF :: (f -> f)
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian Maeder -- ^ this function replaces Qual_var in ExtFORMULA
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu -- ^ codes out Unique_existential in ExtFORMULA
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu -> FORMULA f -> FORMULA f
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai CodescucodeOutUniqueExtF rf mf phi = if noMixfixF (const True) phi
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu then foldFormula (codeOutUniqueRecord rf mf) phi
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai CodescucodeOutCondRecord :: (Eq f) => (f -> f)
62d5dbbceb675837039e6bad0971c324cce96a21Mihai Codescu -> Record f (FORMULA f) (TERM f)
de2f13b8310de00ca228385b1530660e036054c2Christian MaedercodeOutCondRecord fun =
6519f127467b96775226c98f6086fccd5b6723aaChristian Maeder (mapRecord fun)
d58b2e1dc7d2254fa2e10d8c0b5a498ac207d6eaChristian Maeder { foldPredication =
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian Maeder \ phi _ _ _ ->
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder either (codeOutConditionalF fun) id
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder (codeOutCondPredication phi)
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder , foldExistl_equation =
21489db35f79507a68ee6e6926e01b8e8ea60c6bChristian Maeder \ (Existl_equation t1 t2 ps) _ _ _ ->
21489db35f79507a68ee6e6926e01b8e8ea60c6bChristian Maeder either (codeOutConditionalF fun) id
07d65f8d6e942389273f18950619d314c48e182bChristian Maeder (mkEquationAtom Existl_equation t1 t2 ps)
21489db35f79507a68ee6e6926e01b8e8ea60c6bChristian Maeder , foldStrong_equation =
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder \ (Strong_equation t1 t2 ps) _ _ _ ->
21489db35f79507a68ee6e6926e01b8e8ea60c6bChristian Maeder either (codeOutConditionalF fun) id
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder (mkEquationAtom Strong_equation t1 t2 ps)
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder , foldMembership =
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder \ (Membership t s ps) _ _ _ ->
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder either (codeOutConditionalF fun) id
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder (mkSingleTermF (\ x y -> Membership x s y) t ps)
d4aed7a2eea6b546c0d9520d85038addb7beb12fChristian Maeder , foldDefinedness =
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder \ (Definedness t ps) _ _ ->
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian Maeder either (codeOutConditionalF fun) id
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder (mkSingleTermF Definedness t ps)
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian MaedercodeOutCondPredication :: (Eq f) => FORMULA f
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder -> Either (FORMULA f) (FORMULA f)
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian Maeder -- ^ Left means check again for Conditional,
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian Maeder -- Right means no Conditional left
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian MaedercodeOutCondPredication phi@(Predication _ ts _) =
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian Maeder maybe (Right phi) (Left . constructExpansion phi)
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder (listToMaybe (catMaybes (map findConditionalT ts)))
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian MaedercodeOutCondPredication _ = error "CASL.Utils: Predication expected"
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian MaederconstructExpansion :: (Eq f) => FORMULA f
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederconstructExpansion atom c@(Conditional t1 phi t2 ps) =
b79567bdb08bc2c2dfff8d89cd79023fc139b5d3Mihai Codescu Conjunction [ Implication phi (substConditionalF c t1 atom) False ps
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder , Implication (Negation phi ps)
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder (substConditionalF c t2 atom) False ps] ps
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian MaederconstructExpansion _ _ = error "CASL.Utils: Conditional expected"
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian MaedermkEquationAtom :: (Eq f) => (TERM f -> TERM f -> Range -> FORMULA f)
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder -- ^ equational constructor
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder -> TERM f -> TERM f -> Range
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder -> Either (FORMULA f) (FORMULA f)
a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian Maeder -- ^ Left means check again for Conditional,
38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder -- Right means no Conditional left
38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian MaedermkEquationAtom cons t1 t2 ps =
38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder maybe (Right phi) (Left . constructExpansion phi)
38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder (listToMaybe (catMaybes (map findConditionalT [t1,t2])))
38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder where phi = cons t1 t2 ps
ebbe7382423f69d67ffa140163054bc2f8dcd810Christian MaedermkSingleTermF :: (Eq f) => (TERM f -> Range -> FORMULA f)
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder -- ^ single term atom constructor
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder -> TERM f -> Range
bb2c1beb7ab66a49627a2a34df80864a3c65cc83Christian Maeder -> Either (FORMULA f) (FORMULA f)
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder -- ^ Left means check again for Conditional,
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder -- Right means no Conditional left
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian MaedermkSingleTermF cons t ps =
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder maybe (Right phi) (Left . constructExpansion phi)
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder (findConditionalT t)
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder where phi = cons t ps
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder'codeOutConditionalF' implemented via 'CASL.Fold.foldFormula'
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maederat each atom with a term find first (most left,no recursion into
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder terms within it) Conditional term and report it (findConditionalT)
f99c9fca932e8e6e8111049fd93164ed81e1b0abChristian Maedersubstitute the original atom with the conjunction of the already
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder encoded atoms and already encoded formula
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maederencoded atoms are the result of the substition (substConditionalF)
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder of the Conditional term with each result term of the Conditional
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder term plus recusion of codingOutConditionalF
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maederencoded formulas are the result of codingOutConditionalF
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maederexpansion of conditionals according to CASL-Ref-Manual:
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian Maeder\'@A[T1 when F else T2]@\' expands to
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder\'@(A[T1] if F) \/\\ (A[T2] if not F)@\'
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian MaedercodeOutConditionalF :: (Eq f) =>
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder -> FORMULA f -> FORMULA f
36a493b7eec0f9d719674296c26afe7fd9bfe327Christian MaedercodeOutConditionalF fun = foldFormula (codeOutCondRecord fun)
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian MaederfindConditionalRecord :: Record f (Maybe (TERM f)) (Maybe (TERM f))
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian MaederfindConditionalRecord =
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder (constRecord (error "findConditionalRecord")
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder (listToMaybe . catMaybes) Nothing)
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder { foldConditional = \ cond _ _ _ _ -> Just cond }
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian MaederfindConditionalT :: TERM f -> Maybe (TERM f)
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian MaederfindConditionalT t = if noMixfixT (error "findConditionalT.ExtFormula") t
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder then foldOnlyTerm (error "findConditionalT") findConditionalRecord t
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian MaedersubstConditionalRecord :: (Eq f)
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder => TERM f -- ^ Conditional to search for
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder -> TERM f -- ^ newly inserted term
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder -> Record f (FORMULA f) (TERM f)
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian MaedersubstConditionalRecord c t =
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder mapOnlyTermRecord
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder { foldConditional = \ c1 _ _ _ _ ->
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder -- FIXME: correct implementation would use an equality
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder -- which checks for correct positions also!
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder if c1 == c then t else c1
38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian MaedersubstConditionalF :: (Eq f)
38f35f2c4a3b6a778f4f68e7af047a174e93abbeChristian Maeder => TERM f -- ^ Conditional to search for
c43270ad64272b1509c4c29645136c269dae7c9eChristian Maeder -> TERM f -- ^ newly inserted term
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder -> FORMULA f -> FORMULA f
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian MaedersubstConditionalF c t f =
720eeee7c9d8442093c8d05bed743193eee906e0Christian Maeder if noMixfixF (error "substConditionalF.ExtFormula") f
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder then foldFormula (substConditionalRecord c t) f
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder Subsitute predications with strong equation if it is equivalent to.
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian MaedereqSubstRecord :: Set.Set PRED_SYMB -- ^ equivalent predicates
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder -> (f->f) -> Record f (FORMULA f) (TERM f)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedereqSubstRecord eqPredSet extFun =
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder (mapRecord extFun) {foldPredication = foldPred}
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder where foldPred _ psymb tList rng =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder if Set.member psymb eqPredSet
248ab4f138caa9a594cd3fe0815e7fd4150701efChristian Maeder then Strong_equation (head tList) (tList !! 1) rng
substEqPreds :: Set.Set PRED_SYMB -> (f -> f) -> FORMULA f -> FORMULA f
toSortTerm _ = error "CASL2TopSort.toSortTerm: can only handle Qual_var"