{- |
Module      :  ./CASL/SimplifySen.hs
Description : simplification of formulas and terms for output after analysis
Copyright   :  (c) Heng Jiang, C. Maeder, Uni Bremen 2004-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Simplification of formulas and terms for output after analysis

-}

module CASL.SimplifySen
  ( simplifyCASLSen
  , simplifyCASLTerm
  , simplifySen
  , simplifyTerm
  , rmTypesT
  ) where

import Common.AS_Annotation
import Common.Id
import Common.Result
import Common.Lib.State

import CASL.Sign
import CASL.AS_Basic_CASL
import CASL.Overload
import CASL.StaticAna
import CASL.ToDoc

{- | simplifies formula\/term informations for 'show theory' of
   HETS-graph representation. -}
simplifyCASLSen :: (FormExtension f, TermExtension f)
  => Sign f e -> FORMULA f -> FORMULA f
simplifyCASLSen :: Sign f e -> FORMULA f -> FORMULA f
simplifyCASLSen = Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen ((f -> Result f) -> Min f e
forall a b. a -> b -> a
const f -> Result f
forall (m :: * -> *) a. Monad m => a -> m a
return) ((f -> f) -> Sign f e -> f -> f
forall a b. a -> b -> a
const f -> f
forall a. a -> a
id) (Sign f e -> FORMULA f -> FORMULA f)
-> (Sign f e -> Sign f e) -> Sign f e -> FORMULA f -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> Sign f e
forall f e. Sign f e -> Sign f e
setRevSortRel

simplifyCASLTerm :: (FormExtension f, TermExtension f)
  => Sign f e -> TERM f -> TERM f
simplifyCASLTerm :: Sign f e -> TERM f -> TERM f
simplifyCASLTerm = Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
simplifyTerm ((f -> Result f) -> Min f e
forall a b. a -> b -> a
const f -> Result f
forall (m :: * -> *) a. Monad m => a -> m a
return) ((f -> f) -> Sign f e -> f -> f
forall a b. a -> b -> a
const f -> f
forall a. a -> a
id)

simplifySen :: (FormExtension f, TermExtension f)
  => Min f e -- ^ extension type analysis
    -> (Sign f e -> f -> f) -- ^ simplifySen for ExtFORMULA
    -> Sign f e -> FORMULA f -> FORMULA f
simplifySen :: Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen minF :: Min f e
minF simpF :: Sign f e -> f -> f
simpF sign :: Sign f e
sign formula :: FORMULA f
formula =
    case FORMULA f
formula of
    Quantification q :: QUANTIFIER
q vars :: [VAR_DECL]
vars f :: FORMULA f
f pos :: Range
pos ->
            -- add 'vars' to signature
           let sign' :: Sign f e
sign' = State (Sign f e) () -> Sign f e -> Sign f e
forall s a. State s a -> s -> s
execState ((VAR_DECL -> State (Sign f e) ())
-> [VAR_DECL] -> State (Sign f e) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State (Sign f e) ()
forall f e. VAR_DECL -> State (Sign f e) ()
addVars [VAR_DECL]
vars) Sign f e
sign
           in QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vars (Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign' FORMULA f
f) Range
pos
    Junction j :: Junctor
j fs :: [FORMULA f]
fs pos :: Range
pos -> Junctor -> [FORMULA f] -> Range -> FORMULA f
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j ((FORMULA f -> FORMULA f) -> [FORMULA f] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA f -> FORMULA f
simplifySenCall [FORMULA f]
fs) Range
pos
    Relation f1 :: FORMULA f
f1 c :: Relation
c f2 :: FORMULA f
f2 pos :: Range
pos ->
        FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation (FORMULA f -> FORMULA f
simplifySenCall FORMULA f
f1) Relation
c (FORMULA f -> FORMULA f
simplifySenCall FORMULA f
f2) Range
pos
    Negation f :: FORMULA f
f pos :: Range
pos -> FORMULA f -> Range -> FORMULA f
forall f. FORMULA f -> Range -> FORMULA f
Negation (FORMULA f -> FORMULA f
simplifySenCall FORMULA f
f) Range
pos
    Atom b :: Bool
b x :: Range
x -> Bool -> Range -> FORMULA f
forall f. Bool -> Range -> FORMULA f
Atom Bool
b Range
x
    f :: FORMULA f
f@(Predication {}) -> FORMULA f -> FORMULA f
anaFormulaCall FORMULA f
f
    Definedness t :: TERM f
t pos :: Range
pos -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Range -> FORMULA f
Definedness (TERM f -> TERM f
simplifyTermC TERM f
t) Range
pos
    f :: FORMULA f
f@(Equation {}) -> FORMULA f -> FORMULA f
anaFormulaCall FORMULA f
f
    Membership t :: TERM f
t sort :: SORT
sort pos :: Range
pos -> TERM f -> SORT -> Range -> FORMULA f
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership (TERM f -> TERM f
simplifyTermC TERM f
t) SORT
sort Range
pos
    ExtFORMULA f :: f
f -> f -> FORMULA f
forall f. f -> FORMULA f
ExtFORMULA (f -> FORMULA f) -> f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Sign f e -> f -> f
simpF Sign f e
sign f
f
    QuantOp o :: SORT
o ty :: OP_TYPE
ty f :: FORMULA f
f ->
        let sign' :: Sign f e
sign' = State (Sign f e) () -> Sign f e -> Sign f e
forall s a. State s a -> s -> s
execState (Annoted () -> OpType -> SORT -> State (Sign f e) ()
forall a f e. Annoted a -> OpType -> SORT -> State (Sign f e) ()
addOp (() -> Annoted ()
forall a. a -> Annoted a
emptyAnno ()) (OP_TYPE -> OpType
toOpType OP_TYPE
ty) SORT
o) Sign f e
sign
        in SORT -> OP_TYPE -> FORMULA f -> FORMULA f
forall f. SORT -> OP_TYPE -> FORMULA f -> FORMULA f
QuantOp SORT
o OP_TYPE
ty (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign' FORMULA f
f
    QuantPred p :: SORT
p ty :: PRED_TYPE
ty f :: FORMULA f
f ->
        let sign' :: Sign f e
sign' = State (Sign f e) () -> Sign f e -> Sign f e
forall s a. State s a -> s -> s
execState (Annoted () -> PredType -> SORT -> State (Sign f e) ()
forall a f e. Annoted a -> PredType -> SORT -> State (Sign f e) ()
addPred (() -> Annoted ()
forall a. a -> Annoted a
emptyAnno ()) (PRED_TYPE -> PredType
toPredType PRED_TYPE
ty) SORT
p) Sign f e
sign
        in SORT -> PRED_TYPE -> FORMULA f -> FORMULA f
forall f. SORT -> PRED_TYPE -> FORMULA f -> FORMULA f
QuantPred SORT
p PRED_TYPE
ty (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign' FORMULA f
f
    f :: FORMULA f
f@(Sort_gen_ax _ _) -> FORMULA f
f
    Mixfix_formula t :: TERM f
t -> TERM f -> FORMULA f
forall f. TERM f -> FORMULA f
Mixfix_formula (TERM f -> TERM f
simplifyTermC TERM f
t)
    _ -> FORMULA f
formula
    where
        simplifySenCall :: FORMULA f -> FORMULA f
simplifySenCall = Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign
        simplifyTermC :: TERM f -> TERM f
simplifyTermC = Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
simplifyTerm Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign
        anaFormulaCall :: FORMULA f -> FORMULA f
anaFormulaCall = Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
anaFormula Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign

-- | remove a sort annotation
rmSort :: TERM f -> TERM f
rmSort :: TERM f -> TERM f
rmSort term :: TERM f
term = case TERM f
term of
         Sorted_term t :: TERM f
t _ _ -> TERM f
t
         _ -> TERM f
term

{- |
   simplifies the term and removes its type-information as far as the signature
   allows
-}
rmTypesT :: (FormExtension f, TermExtension f)
  => Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
rmTypesT :: Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
rmTypesT minF :: Min f e
minF simpF :: Sign f e -> f -> f
simpF sign :: Sign f e
sign term :: TERM f
term =
    let simTerm :: TERM f
simTerm = Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
simplifyTerm Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign TERM f
term
        minTerm :: TERM f
minTerm = TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort TERM f
simTerm
    in case Result (TERM f) -> Maybe (TERM f)
forall a. Result a -> Maybe a
maybeResult (Result (TERM f) -> Maybe (TERM f))
-> Result (TERM f) -> Maybe (TERM f)
forall a b. (a -> b) -> a -> b
$ Min f e -> Sign f e -> TERM f -> Result (TERM f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min f e
minF Sign f e
sign TERM f
minTerm of
       Just _ -> TERM f
minTerm
       _ -> TERM f
simTerm

{- |
   simplify the TERM and keep its typing information if it had one
-}
simplifyTerm :: (FormExtension f, TermExtension f)
  => Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
simplifyTerm :: Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
simplifyTerm minF :: Min f e
minF simpF :: Sign f e -> f -> f
simpF sign :: Sign f e
sign term :: TERM f
term =
    let simplifyTermC :: TERM f -> TERM f
simplifyTermC = Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
simplifyTerm Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign
        minT :: TERM f -> Maybe (TERM f)
minT = Result (TERM f) -> Maybe (TERM f)
forall a. Result a -> Maybe a
maybeResult (Result (TERM f) -> Maybe (TERM f))
-> (TERM f -> Result (TERM f)) -> TERM f -> Maybe (TERM f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Min f e -> Sign f e -> TERM f -> Result (TERM f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min f e
minF Sign f e
sign
    in case TERM f
term of
       Qual_var v :: VAR
v _ _ ->
           let minTerm :: TERM f
minTerm = OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_SYMB
Op_name (SORT -> OP_SYMB) -> SORT -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ VAR -> SORT
simpleIdToId VAR
v) [] Range
nullRange
           in case TERM f -> Maybe (TERM f)
minT TERM f
forall f. TERM f
minTerm of
              Just _ -> TERM f
forall f. TERM f
minTerm
              Nothing -> TERM f
term
       Sorted_term t :: TERM f
t sort :: SORT
sort pos :: Range
pos ->
           Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
simplifyTermWithSort Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign SORT
sort Range
pos TERM f
t
       Conditional term1 :: TERM f
term1 formula :: FORMULA f
formula term2 :: TERM f
term2 pos :: Range
pos ->
           let t1 :: TERM f
t1 = TERM f -> TERM f
simplifyTermC TERM f
term1
               t2 :: TERM f
t2 = TERM f -> TERM f
simplifyTermC TERM f
term2
               f :: FORMULA f
f = Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign FORMULA f
formula
               minCond :: TERM f
minCond = TERM f -> FORMULA f -> TERM f -> Range -> TERM f
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional (TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort TERM f
t1) FORMULA f
f (TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort TERM f
t2) Range
pos
           in case TERM f -> Maybe (TERM f)
minT TERM f
minCond of
              Just _ -> TERM f
minCond
              Nothing -> TERM f -> FORMULA f -> TERM f -> Range -> TERM f
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional TERM f
t1 FORMULA f
f TERM f
t2 Range
pos
       Cast t :: TERM f
t sort :: SORT
sort pos :: Range
pos -> TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Cast (Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
rmTypesT Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign TERM f
t) SORT
sort Range
pos
       Application opSymb :: OP_SYMB
opSymb@(Op_name _) ts :: [TERM f]
ts pos :: Range
pos ->
           -- assume arguments of unqualified appls are simplified already
           let minOp :: TERM f
minOp = OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
opSymb ((TERM f -> TERM f) -> [TERM f] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort [TERM f]
ts) Range
pos
           in case TERM f -> Maybe (TERM f)
minT TERM f
minOp of
              Just _ -> TERM f
minOp
              Nothing -> TERM f
term
       Application q :: OP_SYMB
q@(Qual_op_name ide :: SORT
ide ty :: OP_TYPE
ty ps :: Range
ps) tl :: [TERM f]
tl pos :: Range
pos ->
           let args :: [TERM f]
args = (TERM f -> SORT -> TERM f) -> [TERM f] -> [SORT] -> [TERM f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ t :: TERM f
t s :: SORT
s -> Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
simplifyTermWithSort Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign
                               SORT
s Range
ps TERM f
t) [TERM f]
tl ([SORT] -> [TERM f]) -> [SORT] -> [TERM f]
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> [SORT]
args_OP_TYPE OP_TYPE
ty
               opSymb :: OP_SYMB
opSymb = SORT -> OP_SYMB
Op_name SORT
ide
               minArgs :: [TERM f]
minArgs = (TERM f -> TERM f) -> [TERM f] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort [TERM f]
args
               minOp :: TERM f
minOp = OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
opSymb [TERM f]
minArgs Range
pos
               simT :: TERM f
simT = Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
simplifyTermWithSort Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign
                         (OP_TYPE -> SORT
res_OP_TYPE OP_TYPE
ty) Range
ps
                         (TERM f -> TERM f) -> TERM f -> TERM f
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
opSymb [TERM f]
args Range
pos
           in case TERM f -> Maybe (TERM f)
minT TERM f
minOp of
              Just _ -> TERM f
minOp
              Nothing -> if [TERM f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM f]
args then case TERM f -> Maybe (TERM f)
minT TERM f
simT of
                 Just _ -> TERM f
simT
                 _ -> OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
q [] Range
pos
                 else TERM f
simT
       ExtTERM t :: f
t -> f -> TERM f
forall f. f -> TERM f
ExtTERM (f -> TERM f) -> f -> TERM f
forall a b. (a -> b) -> a -> b
$ Sign f e -> f -> f
simpF Sign f e
sign f
t
       _ -> TERM f
term

{- |
   simplify the TERM with given sort and attach sort if necessary
-}
simplifyTermWithSort :: (FormExtension f, TermExtension f)
  => Min f e -> (Sign f e -> f -> f) -> Sign f e -> SORT -> Range -> TERM f
    -> TERM f
simplifyTermWithSort :: Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
simplifyTermWithSort minF :: Min f e
minF simpF :: Sign f e -> f -> f
simpF sign :: Sign f e
sign gSort :: SORT
gSort poss :: Range
poss term :: TERM f
term =
    let simplifyTermCS :: TERM f -> TERM f
simplifyTermCS = Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
simplifyTermWithSort Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign SORT
gSort Range
poss
        simplifyTermC :: TERM f -> TERM f
simplifyTermC = Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
simplifyTerm Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign
        minT :: TERM f -> Maybe (TERM f)
minT = Result (TERM f) -> Maybe (TERM f)
forall a. Result a -> Maybe a
maybeResult (Result (TERM f) -> Maybe (TERM f))
-> (TERM f -> Result (TERM f)) -> TERM f -> Maybe (TERM f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Min f e -> Sign f e -> TERM f -> Result (TERM f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min f e
minF Sign f e
sign
    in case TERM f
term of
       Qual_var v :: VAR
v _ _ ->
           let minTerm :: TERM f
minTerm = OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (SORT -> OP_SYMB
Op_name (SORT -> OP_SYMB) -> SORT -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ VAR -> SORT
simpleIdToId VAR
v) [] Range
nullRange
               simT :: TERM f
simT = TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM f
forall f. TERM f
minTerm SORT
gSort Range
poss
           in case TERM f -> Maybe (TERM f)
minT TERM f
forall f. TERM f
simT of
                  Just _ -> TERM f
forall f. TERM f
simT
                  _ -> TERM f
term
       Sorted_term t :: TERM f
t sort :: SORT
sort pos :: Range
pos ->
           let simT :: TERM f
simT = TERM f -> TERM f
simplifyTermCS TERM f
t
           in case TERM f -> Maybe (TERM f)
minT TERM f
simT of
                   Just _ -> TERM f
simT
                   Nothing -> TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term (TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort (TERM f -> TERM f) -> TERM f -> TERM f
forall a b. (a -> b) -> a -> b
$
                               Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
simplifyTermWithSort Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign SORT
sort Range
pos TERM f
t)
                              SORT
sort Range
pos
       Conditional term1 :: TERM f
term1 formula :: FORMULA f
formula term2 :: TERM f
term2 pos :: Range
pos ->
           let t1 :: TERM f
t1 = TERM f -> TERM f
simplifyTermCS TERM f
term1
               t2 :: TERM f
t2 = TERM f -> TERM f
simplifyTermCS TERM f
term2
               f :: FORMULA f
f = Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign FORMULA f
formula
               minCond :: TERM f
minCond = TERM f -> FORMULA f -> TERM f -> Range -> TERM f
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional (TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort TERM f
t1) FORMULA f
f (TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort TERM f
t2) Range
pos
           in case TERM f -> Maybe (TERM f)
minT TERM f
minCond of
              Just _ -> TERM f
minCond
              Nothing -> TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM f
minCond SORT
gSort Range
poss
       Cast t :: TERM f
t sort :: SORT
sort pos :: Range
pos -> TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Cast (Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
rmTypesT Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign TERM f
t) SORT
sort Range
pos
       Application opSymb :: OP_SYMB
opSymb@(Op_name _) ts :: [TERM f]
ts pos :: Range
pos ->
           -- assume arguments of unqualified appls are simplified already
           let minOp :: TERM f
minOp = OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
opSymb ((TERM f -> TERM f) -> [TERM f] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort [TERM f]
ts) Range
pos
           in case TERM f -> Maybe (TERM f)
minT TERM f
minOp of
              Just _ -> TERM f
minOp
              Nothing -> case TERM f -> Maybe (TERM f)
minT TERM f
term of
                  Just _ -> TERM f
term
                  Nothing -> TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM f
term SORT
gSort Range
poss
       Application (Qual_op_name _ ty :: OP_TYPE
ty _) _ _ ->
           let simT :: TERM f
simT = TERM f -> TERM f
simplifyTermC TERM f
term in
           if SORT
gSort SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== OP_TYPE -> SORT
res_OP_TYPE OP_TYPE
ty then
              TERM f
simT else
           let minOp :: TERM f
minOp = TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term (TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort TERM f
simT) SORT
gSort Range
poss
           in case TERM f -> Maybe (TERM f)
minT TERM f
minOp of
              Just _ -> TERM f
minOp
              Nothing -> TERM f -> SORT -> Range -> TERM f
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM f
simT SORT
gSort Range
poss
       ExtTERM t :: f
t -> f -> TERM f
forall f. f -> TERM f
ExtTERM (f -> TERM f) -> f -> TERM f
forall a b. (a -> b) -> a -> b
$ Sign f e -> f -> f
simpF Sign f e
sign f
t
       _ -> TERM f
term

{- |
    analyzes the formula if it is the minimal expansions.
-}
anaFormula :: (FormExtension f, TermExtension f)
  => Min f e -> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
anaFormula :: Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
anaFormula minF :: Min f e
minF simpF :: Sign f e -> f -> f
simpF sign :: Sign f e
sign form1 :: FORMULA f
form1 =
    let minForm :: FORMULA f -> Maybe (FORMULA f)
minForm = Result (FORMULA f) -> Maybe (FORMULA f)
forall a. Result a -> Maybe a
maybeResult (Result (FORMULA f) -> Maybe (FORMULA f))
-> (FORMULA f -> Result (FORMULA f))
-> FORMULA f
-> Maybe (FORMULA f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> FORMULA f -> Result (FORMULA f)
minExpFORMULA Min f e
minF Sign f e
sign
        simplifyTermC :: TERM f -> TERM f
simplifyTermC = Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
simplifyTerm Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign
        simpForm :: FORMULA f
simpForm = case FORMULA f
form1 of
            Equation t1 :: TERM f
t1 e :: Equality
e t2 :: TERM f
t2 pos :: Range
pos -> TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
              (TERM f -> TERM f
simplifyTermC TERM f
t1) Equality
e (TERM f -> TERM f
simplifyTermC TERM f
t2) Range
pos
            _ -> [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "anaFormula1"
        rmForm :: FORMULA f
rmForm = case FORMULA f
simpForm of
            Equation t1 :: TERM f
t1 e :: Equality
e t2 :: TERM f
t2 pos :: Range
pos -> TERM f -> Equality -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
              (TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort TERM f
t1) Equality
e (TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort TERM f
t2) Range
pos
            _ -> [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "anaFormula2"
     in case FORMULA f
form1 of
        Predication predSymb :: PRED_SYMB
predSymb@(Pred_name _) tl :: [TERM f]
tl pos :: Range
pos ->
           let minPred :: FORMULA f
minPred = PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
predSymb ((TERM f -> TERM f) -> [TERM f] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort [TERM f]
tl) Range
pos
           in case FORMULA f -> Maybe (FORMULA f)
minForm FORMULA f
minPred of
              Just _ -> FORMULA f
minPred
              Nothing -> FORMULA f
form1
        Predication (Qual_pred_name pName :: SORT
pName (Pred_type sl :: [SORT]
sl ps :: Range
ps) _) tl :: [TERM f]
tl pos :: Range
pos ->
           let args :: [TERM f]
args = (TERM f -> SORT -> TERM f) -> [TERM f] -> [SORT] -> [TERM f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ t :: TERM f
t s :: SORT
s -> Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f)
-> Sign f e
-> SORT
-> Range
-> TERM f
-> TERM f
simplifyTermWithSort
                               Min f e
minF Sign f e -> f -> f
simpF Sign f e
sign SORT
s Range
ps TERM f
t) [TERM f]
tl [SORT]
sl
               predSymb :: PRED_SYMB
predSymb = SORT -> PRED_SYMB
Pred_name SORT
pName
               minPred :: FORMULA f
minPred = PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
predSymb ((TERM f -> TERM f) -> [TERM f] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map TERM f -> TERM f
forall f. TERM f -> TERM f
rmSort [TERM f]
args) Range
pos
           in case FORMULA f -> Maybe (FORMULA f)
minForm FORMULA f
minPred of
              Just _ -> FORMULA f
minPred
              Nothing -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
predSymb [TERM f]
args Range
pos
        _ -> case FORMULA f -> Maybe (FORMULA f)
minForm FORMULA f
rmForm of
             Just _ -> FORMULA f
rmForm
             _ -> FORMULA f
simpForm