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

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.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 ->
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.
(a -> m b) -> t a -> m ()
mapM_ VAR_DECL -> State (Sign f e) ()
forall f e. VAR_DECL -> State (Sign f e) ()
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) ()
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) ()
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
```