{- |

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