{- |
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 :: Named Sentence -> Named Sentence
markSimp = Bool -> Named Sentence -> Named Sentence
markSimpAux Bool
True

markThSimp :: Named Sentence -> Named Sentence
markThSimp :: Named Sentence -> Named Sentence
markThSimp = Bool -> Named Sentence -> Named Sentence
markSimpAux Bool
False

markSimpAux :: Bool -> Named Sentence -> Named Sentence
markSimpAux :: Bool -> Named Sentence -> Named Sentence
markSimpAux isAx :: Bool
isAx s :: Named Sentence
s = let
  prefixIsin :: [[Char]] -> Bool
prefixIsin = ([Char] -> Bool) -> [[Char]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (([Char] -> [Char] -> Bool) -> [Char] -> [Char] -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf ([Char] -> [Char] -> Bool) -> [Char] -> [Char] -> Bool
forall a b. (a -> b) -> a -> b
$ Named Sentence -> [Char]
forall s a. SenAttr s a -> a
senAttr Named Sentence
s)
  hasSimp :: Bool -> Bool
hasSimp b :: Bool
b = Named Sentence -> Maybe Bool
forall s a. SenAttr s a -> Maybe Bool
simpAnno Named Sentence
s Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b
  in if Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isDef Named Sentence
s Bool -> Bool -> Bool
|| Bool -> Bool
hasSimp Bool
False Bool -> Bool -> Bool
|| [[Char]] -> Bool
prefixIsin [[Char]]
excludePrefixes
    then Named Sentence
s else (Sentence -> Sentence) -> Named Sentence -> Named Sentence
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed ((Sentence -> Bool) -> Sentence -> Sentence
markSimpSen ((Sentence -> Bool) -> Sentence -> Sentence)
-> (Sentence -> Bool) -> Sentence -> Sentence
forall a b. (a -> b) -> a -> b
$ \ ns :: Sentence
ns -> Bool -> Bool
hasSimp Bool
True
      Bool -> Bool -> Bool
|| Bool
isAx Bool -> Bool -> Bool
&& Sentence -> Bool
isSimpRuleSen Sentence
ns Bool -> Bool -> Bool
|| [[Char]] -> Bool
prefixIsin [[Char]]
includePrefixes) Named Sentence
s

excludePrefixes :: [String]
excludePrefixes :: [[Char]]
excludePrefixes = [ "ga_predicate_monotonicity"
                  , "ga_function_monotonicity"
                  , "ga_transitive"]

includePrefixes :: [String]
includePrefixes :: [[Char]]
includePrefixes =
    [ "ga_comm_"
    , "ga_assoc_"
    , "ga_left_comm_"]

markSimpSen :: (Sentence -> Bool) -> Sentence -> Sentence
markSimpSen :: (Sentence -> Bool) -> Sentence -> Sentence
markSimpSen f :: Sentence -> Bool
f s :: Sentence
s = case Sentence
s of
                  Sentence {} -> Sentence
s {isSimp :: Bool
isSimp = Sentence -> Bool
f Sentence
s}
                  _ -> Sentence
s

isSimpRuleSen :: Sentence -> Bool
isSimpRuleSen :: Sentence -> Bool
isSimpRuleSen sen :: Sentence
sen = case Sentence
sen of
    Sentence {metaTerm :: Sentence -> MetaTerm
metaTerm = Term t :: Term
t} -> Term -> Bool
isCondEq Term
t
    _ -> Bool
False

isSimplAppl :: Term -> Bool
isSimplAppl :: Term -> Bool
isSimplAppl trm :: Term
trm = case Term
trm of
    Free {} -> Bool
True
    Const q :: VName
q _ -> [Char] -> [[Char]] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem (VName -> [Char]
new VName
q)
      [[Char]
allS, [Char]
exS, [Char]
ex1S, [Char]
eq, [Char]
impl, [Char]
disj, [Char]
conj, [Char]
cNot]
    App f :: Term
f a :: Term
a _ -> Term -> Bool
isSimplAppl Term
f Bool -> Bool -> Bool
&& Term -> Bool
isSimplAppl Term
a
    Tuplex ts :: [Term]
ts _ -> (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
isSimplAppl [Term]
ts
    _ -> Bool
False

isEqOrSimplAppl :: Term -> Bool
isEqOrSimplAppl :: Term -> Bool
isEqOrSimplAppl trm :: Term
trm = case Term
trm of
    App (App (Const q :: VName
q _) a1 :: Term
a1 _) a2 :: Term
a2 _ | VName -> [Char]
new VName
q [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
eq ->
        Term -> Bool
isSimplAppl Term
a1 Bool -> Bool -> Bool
&& Term -> Bool
isSimplAppl Term
a2 Bool -> Bool -> Bool
&& Term -> Int
sizeOfTerm Term
a1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Term -> Int
sizeOfTerm Term
a2
    _ -> Term -> Bool
isSimplAppl Term
trm

isEqOrNeg :: Term -> Bool
isEqOrNeg :: Term -> Bool
isEqOrNeg trm :: Term
trm = case Term
trm of
    App (Const q :: VName
q _) arg :: Term
arg _ | VName -> [Char]
new VName
q [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
cNot -> Term -> Bool
isEqOrNeg Term
arg
    _ -> Term -> Bool
isEqOrSimplAppl Term
trm

isCondEq :: Term -> Bool
isCondEq :: Term -> Bool
isCondEq trm :: Term
trm = case Term
trm of
    App (Const q :: VName
q _) arg :: Term
arg@Abs {} _ | VName -> [Char]
new VName
q [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
allS -> Term -> Bool
isCondEq (Term -> Term
termId Term
arg)
    App (App (Const q :: VName
q _) a1 :: Term
a1 _) a2 :: Term
a2 _
        | VName -> [Char]
new VName
q [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
impl -> Term -> Bool
isEqOrNeg Term
a1 Bool -> Bool -> Bool
&& Term -> Bool
isCondEq Term
a2
        | VName -> [Char]
new VName
q [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
conj -> Term -> Bool
isCondEq Term
a1 Bool -> Bool -> Bool
&& Term -> Bool
isCondEq Term
a2
    _ -> Term -> Bool
isEqOrNeg Term
trm

sizeOfTerm :: Term -> Int
sizeOfTerm :: Term -> Int
sizeOfTerm trm :: Term
trm = case Term
trm of
    Abs { termId :: Term -> Term
termId = Term
t } -> Term -> Int
sizeOfTerm Term
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
    App { funId :: Term -> Term
funId = Term
t1, argId :: Term -> Term
argId = Term
t2 } -> Term -> Int
sizeOfTerm Term
t1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Term -> Int
sizeOfTerm Term
t2
    If { ifId :: Term -> Term
ifId = Term
t1, thenId :: Term -> Term
thenId = Term
t2, elseId :: Term -> Term
elseId = Term
t3 } ->
        Term -> Int
sizeOfTerm Term
t1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Term -> Int
sizeOfTerm Term
t2) (Term -> Int
sizeOfTerm Term
t3)
    Case { termId :: Term -> Term
termId = Term
t1, caseSubst :: Term -> [(Term, Term)]
caseSubst = [(Term, Term)]
cs } ->
        Term -> Int
sizeOfTerm Term
t1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ((Term, Term) -> Int -> Int) -> Int -> [(Term, Term)] -> Int
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Int -> Int -> Int)
-> ((Term, Term) -> Int) -> (Term, Term) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Int
sizeOfTerm (Term -> Int) -> ((Term, Term) -> Term) -> (Term, Term) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term, Term) -> Term
forall a b. (a, b) -> b
snd) 0 [(Term, Term)]
cs
    Let { letSubst :: Term -> [(Term, Term)]
letSubst = [(Term, Term)]
es, inId :: Term -> Term
inId = Term
t } ->
        Term -> Int
sizeOfTerm Term
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (((Term, Term) -> Int) -> [(Term, Term)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Term -> Int
sizeOfTerm (Term -> Int) -> ((Term, Term) -> Term) -> (Term, Term) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term, Term) -> Term
forall a b. (a, b) -> b
snd) [(Term, Term)]
es)
    IsaEq { firstTerm :: Term -> Term
firstTerm = Term
t1, secondTerm :: Term -> Term
secondTerm = Term
t2 } ->
        Term -> Int
sizeOfTerm Term
t1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Term -> Int
sizeOfTerm Term
t2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
    Tuplex ts :: [Term]
ts _ -> [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Term -> Int) -> [Term] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Int
sizeOfTerm [Term]
ts
    _ -> 1