content: {- |
  Module      :  ./Isabelle/MarkSimp.hs
  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
  