MarkSimp.hs revision 3d3889e0cefcdce9b3f43c53aaa201943ac2e895
{- |
Module : $Header$
Description : mark certain Isabelle sentenes for the simplifier
Copyright : (c) University of Cambridge, Cambridge, England
adaption (c) Till Mossakowski, Uni Bremen 2002-2005
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
try to recognize formulas for the simplifier
-}
module Isabelle.MarkSimp (markSimp, markThSimp) where
import Isabelle.IsaSign
import Isabelle.IsaConsts
import Common.AS_Annotation
import Data.List (isPrefixOf)
markSimp :: Named Sentence -> Named Sentence
markSimp = markSimpAux True
markThSimp :: Named Sentence -> Named Sentence
markThSimp = markSimpAux False
markSimpAux :: Bool -> Named Sentence -> Named Sentence
markSimpAux isAx s = let
prefixIsin = any (flip isPrefixOf $ senAttr s)
hasSimp b = simpAnno s == Just b
in if isDef s || hasSimp False || prefixIsin excludePrefixes
then s else mapNamed (markSimpSen $ \ ns -> hasSimp True
|| isAx && isSimpRuleSen ns || prefixIsin includePrefixes) s
excludePrefixes :: [String]
excludePrefixes = [ "ga_predicate_monotonicity"
, "ga_function_monotonicity"
, "ga_transitive"]
includePrefixes :: [String]
includePrefixes =
[ "ga_comm_"
, "ga_assoc_"
, "ga_left_comm_"]
markSimpSen :: (Sentence -> Bool) -> Sentence -> Sentence
markSimpSen f s = case s of
Sentence {} -> s {isSimp = f s}
_ -> s
isSimpRuleSen :: Sentence -> Bool
isSimpRuleSen sen = case sen of
Sentence {metaTerm = Term t} -> isCondEq t
_ -> False
isSimplAppl :: Term -> Bool
isSimplAppl trm = case trm of
Free {} -> True
Const q _ -> notElem (new q)
[allS, exS, ex1S, eq, impl, disj, conj, cNot]
App f a _ -> isSimplAppl f && isSimplAppl a
Tuplex ts _ -> all isSimplAppl ts
_ -> False
isEqOrSimplAppl :: Term -> Bool
isEqOrSimplAppl trm = case trm of
App (App (Const q _) a1 _) a2 _ | new q == eq ->
isSimplAppl a1 && isSimplAppl a2 && sizeOfTerm a1 > sizeOfTerm a2
_ -> isSimplAppl trm
isEqOrNeg :: Term -> Bool
isEqOrNeg trm = case trm of
App (Const q _) arg _ | new q == cNot -> isEqOrNeg arg
_ -> isEqOrSimplAppl trm
isCondEq :: Term -> Bool
isCondEq trm = case trm of
App (Const q _) arg@Abs {} _ | new q == allS -> isCondEq (termId arg)
App (App (Const q _) a1 _) a2 _
| new q == impl -> isEqOrNeg a1 && isCondEq a2
| new q == conj -> isCondEq a1 && isCondEq a2
_ -> isEqOrNeg trm
sizeOfTerm :: Term -> Int
sizeOfTerm trm = case trm of
Abs { termId = t } -> sizeOfTerm t + 1
App { funId = t1, argId = t2 } -> sizeOfTerm t1 + sizeOfTerm t2
If { ifId = t1, thenId = t2, elseId = t3 } ->
sizeOfTerm t1 + max (sizeOfTerm t2) (sizeOfTerm t3)
Case { termId = t1, caseSubst = cs } ->
sizeOfTerm t1 + foldr (max . sizeOfTerm . snd) 0 cs
Let { letSubst = es, inId = t } ->
sizeOfTerm t + sum (map (sizeOfTerm . snd) es)
IsaEq { firstTerm = t1, secondTerm = t2 } ->
sizeOfTerm t1 + sizeOfTerm t2 + 1
Tuplex ts _ -> sum $ map sizeOfTerm ts
_ -> 1