{- |
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 = simplifySen (const return) (const id) . setRevSortRel
simplifyCASLTerm :: (FormExtension f, TermExtension f)
=> Sign f e -> TERM f -> TERM f
simplifyCASLTerm = simplifyTerm (const return) (const 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 minF simpF sign formula =
case formula of
Quantification q vars f pos ->
-- add 'vars' to signature
let sign' = execState (mapM_ addVars vars) sign
in Quantification q vars (simplifySen minF simpF sign' f) pos
Junction j fs pos -> Junction j (map simplifySenCall fs) pos
Relation f1 c f2 pos ->
Relation (simplifySenCall f1) c (simplifySenCall f2) pos
Negation f pos -> Negation (simplifySenCall f) pos
Atom b x -> Atom b x
f@(Predication {}) -> anaFormulaCall f
Definedness t pos -> Definedness (simplifyTermC t) pos
f@(Equation {}) -> anaFormulaCall f
Membership t sort pos -> Membership (simplifyTermC t) sort pos
ExtFORMULA f -> ExtFORMULA $ simpF sign f
QuantOp o ty f ->
let sign' = execState (addOp (emptyAnno ()) (toOpType ty) o) sign
in QuantOp o ty $ simplifySen minF simpF sign' f
QuantPred p ty f ->
let sign' = execState (addPred (emptyAnno ()) (toPredType ty) p) sign
in QuantPred p ty $ simplifySen minF simpF sign' f
f@(Sort_gen_ax _ _) -> f
Mixfix_formula t -> Mixfix_formula (simplifyTermC t)
_ -> formula
where
simplifySenCall = simplifySen minF simpF sign
simplifyTermC = simplifyTerm minF simpF sign
anaFormulaCall = anaFormula minF simpF sign
-- | remove a sort annotation
rmSort :: TERM f -> TERM f
rmSort term = case term of
Sorted_term t _ _ -> t
_ -> 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 minF simpF sign term =
let simTerm = simplifyTerm minF simpF sign term
minTerm = rmSort simTerm
in case maybeResult $ oneExpTerm minF sign minTerm of
Just _ -> minTerm
_ -> 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 minF simpF sign term =
let simplifyTermC = simplifyTerm minF simpF sign
minT = maybeResult . oneExpTerm minF sign
in case term of
Qual_var v _ _ ->
let minTerm = Application (Op_name $ simpleIdToId v) [] nullRange
in case minT minTerm of
Just _ -> minTerm
Nothing -> term
Sorted_term t sort pos ->
simplifyTermWithSort minF simpF sign sort pos t
Conditional term1 formula term2 pos ->
let t1 = simplifyTermC term1
t2 = simplifyTermC term2
f = simplifySen minF simpF sign formula
minCond = Conditional (rmSort t1) f (rmSort t2) pos
in case minT minCond of
Just _ -> minCond
Nothing -> Conditional t1 f t2 pos
Cast t sort pos -> Cast (rmTypesT minF simpF sign t) sort pos
Application opSymb@(Op_name _) ts pos ->
-- assume arguments of unqualified appls are simplified already
let minOp = Application opSymb (map rmSort ts) pos
in case minT minOp of
Just _ -> minOp
Nothing -> term
Application q@(Qual_op_name ide ty ps) tl pos ->
let args = zipWith (\ t s -> simplifyTermWithSort minF simpF sign
s ps t) tl $ args_OP_TYPE ty
opSymb = Op_name ide
minArgs = map rmSort args
minOp = Application opSymb minArgs pos
simT = simplifyTermWithSort minF simpF sign
(res_OP_TYPE ty) ps
$ Application opSymb args pos
in case minT minOp of
Just _ -> minOp
Nothing -> if null args then case minT simT of
Just _ -> simT
_ -> Application q [] pos
else simT
ExtTERM t -> ExtTERM $ simpF sign t
_ -> 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 minF simpF sign gSort poss term =
let simplifyTermCS = simplifyTermWithSort minF simpF sign gSort poss
simplifyTermC = simplifyTerm minF simpF sign
minT = maybeResult . oneExpTerm minF sign
in case term of
Qual_var v _ _ ->
let minTerm = Application (Op_name $ simpleIdToId v) [] nullRange
simT = Sorted_term minTerm gSort poss
in case minT simT of
Just _ -> simT
_ -> term
Sorted_term t sort pos ->
let simT = simplifyTermCS t
in case minT simT of
Just _ -> simT
Nothing -> Sorted_term (rmSort $
simplifyTermWithSort minF simpF sign sort pos t)
sort pos
Conditional term1 formula term2 pos ->
let t1 = simplifyTermCS term1
t2 = simplifyTermCS term2
f = simplifySen minF simpF sign formula
minCond = Conditional (rmSort t1) f (rmSort t2) pos
in case minT minCond of
Just _ -> minCond
Nothing -> Sorted_term minCond gSort poss
Cast t sort pos -> Cast (rmTypesT minF simpF sign t) sort pos
Application opSymb@(Op_name _) ts pos ->
-- assume arguments of unqualified appls are simplified already
let minOp = Application opSymb (map rmSort ts) pos
in case minT minOp of
Just _ -> minOp
Nothing -> case minT term of
Just _ -> term
Nothing -> Sorted_term term gSort poss
Application (Qual_op_name _ ty _) _ _ ->
let simT = simplifyTermC term in
if gSort == res_OP_TYPE ty then
simT else
let minOp = Sorted_term (rmSort simT) gSort poss
in case minT minOp of
Just _ -> minOp
Nothing -> Sorted_term simT gSort poss
ExtTERM t -> ExtTERM $ simpF sign t
_ -> 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 minF simpF sign form1 =
let minForm = maybeResult . minExpFORMULA minF sign
simplifyTermC = simplifyTerm minF simpF sign
simpForm = case form1 of
Equation t1 e t2 pos -> Equation
(simplifyTermC t1) e (simplifyTermC t2) pos
_ -> error "anaFormula1"
rmForm = case simpForm of
Equation t1 e t2 pos -> Equation
(rmSort t1) e (rmSort t2) pos
_ -> error "anaFormula2"
in case form1 of
Predication predSymb@(Pred_name _) tl pos ->
let minPred = Predication predSymb (map rmSort tl) pos
in case minForm minPred of
Just _ -> minPred
Nothing -> form1
Predication (Qual_pred_name pName (Pred_type sl ps) _) tl pos ->
let args = zipWith (\ t s -> simplifyTermWithSort
minF simpF sign s ps t) tl sl
predSymb = Pred_name pName
minPred = Predication predSymb (map rmSort args) pos
in case minForm minPred of
Just _ -> minPred
Nothing -> Predication predSymb args pos
_ -> case minForm rmForm of
Just _ -> rmForm
_ -> simpForm