MarkSimp.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian MaederModule : $Header$
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian MaederDescription : mark certain Isabelle sentenes for the simplifier
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian MaederCopyright : (c) University of Cambridge, Cambridge, England
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian Maeder adaption (c) Till Mossakowski, Uni Bremen 2002-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian MaederMaintainer : Christian.Maeder@dfki.de
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian MaederStability : provisional
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian MaederPortability : portable
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian Maedertry to recognize formulas for the simplifier
b205bc86685958085af2b816c277faef3ebed52aChristian Maedermodule Isabelle.MarkSimp (markSimp, markThSimp) where
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maederimport Data.List (isPrefixOf)
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian MaedermarkSimp :: Named Sentence -> Named Sentence
b205bc86685958085af2b816c277faef3ebed52aChristian MaedermarkSimp = markSimpAux True
b205bc86685958085af2b816c277faef3ebed52aChristian MaedermarkThSimp :: Named Sentence -> Named Sentence
b205bc86685958085af2b816c277faef3ebed52aChristian MaedermarkThSimp = markSimpAux False
b205bc86685958085af2b816c277faef3ebed52aChristian MaedermarkSimpAux :: Bool -> Named Sentence -> Named Sentence
b205bc86685958085af2b816c277faef3ebed52aChristian MaedermarkSimpAux isAx s = let
021d7137df04ec1834911d99d90243a092841cedChristian Maeder prefixIsin = any (flip isPrefixOf $ senAttr s)
021d7137df04ec1834911d99d90243a092841cedChristian Maeder hasSimp b = simpAnno s == Just b
021d7137df04ec1834911d99d90243a092841cedChristian Maeder in if isDef s || hasSimp False || prefixIsin excludePrefixes
021d7137df04ec1834911d99d90243a092841cedChristian Maeder then s else mapNamed (markSimpSen $ \ ns -> hasSimp True
b205bc86685958085af2b816c277faef3ebed52aChristian Maeder || isAx && isSimpRuleSen ns || prefixIsin includePrefixes) s
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian MaederexcludePrefixes :: [String]
003db5288a0289b5d652ad12bc4a09af1824bf79Till MossakowskiexcludePrefixes = [ "ga_predicate_monotonicity"
003db5288a0289b5d652ad12bc4a09af1824bf79Till Mossakowski , "ga_function_monotonicity"
003db5288a0289b5d652ad12bc4a09af1824bf79Till Mossakowski ,"ga_transitive"]
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian MaederincludePrefixes :: [String]
23f25b487695c18b40461b44f89946f3a76b5796Christian MaederincludePrefixes =
23f25b487695c18b40461b44f89946f3a76b5796Christian Maeder , "ga_assoc_"
23f25b487695c18b40461b44f89946f3a76b5796Christian Maeder , "ga_left_comm_"]
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian MaedermarkSimpSen :: (Sentence -> Bool) -> Sentence -> Sentence
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian MaedermarkSimpSen f s = case s of
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian Maeder Sentence {} -> s {isSimp = f s}
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian MaederisSimpRuleSen :: Sentence -> Bool
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian MaederisSimpRuleSen sen = case sen of
794ea8703e849ef00e0487fb79552e81b557eafbChristian Maeder Sentence {metaTerm = Term t} -> isCondEq t
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian MaederisSimplAppl :: Term -> Bool
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian MaederisSimplAppl trm = case trm of
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder Free {} -> True
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder Const q _ -> not $ elem (new q)
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder [allS, exS, ex1S, eq, impl, disj, conj, cNot]
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder App f a _ -> isSimplAppl f && isSimplAppl a
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder Tuplex ts _ -> all isSimplAppl ts
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian MaederisEqOrSimplAppl :: Term -> Bool
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian MaederisEqOrSimplAppl trm = case trm of
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder App (App (Const q _) a1 _) a2 _ | new q == eq ->
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder isSimplAppl a1 && isSimplAppl a2 && sizeOfTerm a1 > sizeOfTerm a2
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder _ -> isSimplAppl trm
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian MaederisEqOrNeg :: Term -> Bool
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian MaederisEqOrNeg trm = case trm of
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder App (Const q _) arg _ | new q == cNot -> isEqOrNeg arg
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder _ -> isEqOrSimplAppl trm
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian MaederisCondEq :: Term -> Bool
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian MaederisCondEq trm = case trm of
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder App (Const q _) arg@Abs{} _ | new q == allS -> isCondEq (termId arg)
a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian Maeder App (App (Const q _) a1 _) a2 _
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder | new q == impl -> isEqOrNeg a1 && isCondEq a2
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder | new q == conj -> isCondEq a1 && isCondEq a2
4a647326d6083cd2e4a88f2c9f2be639e14530dcChristian Maeder _ -> isEqOrNeg trm
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian MaedersizeOfTerm :: Term -> Int
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian MaedersizeOfTerm trm = case trm of
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder Abs { termId = t } -> sizeOfTerm t + 1
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder App { funId = t1, argId = t2 } -> sizeOfTerm t1 + sizeOfTerm t2
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder If { ifId = t1, thenId = t2, elseId = t3 } ->
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder sizeOfTerm t1 + max (sizeOfTerm t2) (sizeOfTerm t3)
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder Case { termId = t1, caseSubst = cs } ->
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder sizeOfTerm t1 + foldr max 0 (map (sizeOfTerm . snd) cs)
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder Let { letSubst = es, inId = t } ->
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder sizeOfTerm t + sum (map (sizeOfTerm . snd) es)
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder IsaEq { firstTerm = t1, secondTerm = t2 } ->
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder sizeOfTerm t1 + sizeOfTerm t2 + 1
2fc44bccbdb9dd30d3aa1b49fff1f3e3c3e64d0aChristian Maeder Tuplex ts _ -> sum $ map sizeOfTerm ts