4751N/A{- |

4751N/AModule : ./HasCASL/SimplifyTerm.hs

4751N/ADescription : simplify terms for prettier printing

4751N/ACopyright : (c) Christian Maeder and Uni Bremen 2005

4751N/ALicense : GPLv2 or higher, see LICENSE.txt

4751N/A

4751N/AMaintainer : Christian.Maeder@dfki.de

4751N/AStability : provisional

4751N/APortability : portable

4751N/A

4751N/Aremove type annotations of unique variables or operations

4751N/A

4751N/A-}

4751N/A

4751N/Amodule HasCASL.SimplifyTerm where

4751N/A

4751N/Aimport HasCASL.As

4751N/Aimport HasCASL.AsUtils

4751N/Aimport HasCASL.VarDecl

4751N/Aimport HasCASL.Le

4751N/Aimport HasCASL.FoldTerm

4751N/Aimport HasCASL.TypeAna

4751N/A

4751N/Aimport Common.Lib.State

4751N/A

5061N/Aimport qualified Data.Map as Map

5821N/A

4751N/A-- | simplify terms and patterns (if True)

4751N/AsimplifyRec :: Bool -> Env -> MapRec

4751N/AsimplifyRec b env = mapRec

4751N/A { foldQualVar = \ t (VarDecl v ty _ ps) ->

4751N/A if Map.member v (assumps env) then t else

4751N/A let nv = ResolvedMixTerm v [] [] ps in

4751N/A if b then TypedTerm nv OfType ty ps else nv

4751N/A , foldQualOp = \ trm _ (PolyId i _ _) _ tys k ps ->

4751N/A if Map.member i $ localVars env then trm else

4751N/A case getMinAssumps env i of

4751N/A _ : _ : _ -> trm

4751N/A _ -> ResolvedMixTerm i (if k == Infer then [] else tys) [] ps

4751N/A , foldTypedTerm = \ _ nt q ty ps ->

4751N/A let ntyped = TypedTerm nt q ty ps in case q of

4751N/A InType -> ntyped

4751N/A AsType -> ntyped

4751N/A _ -> case nt of

4751N/A QualVar (VarDecl v oty _ qs) | oty == ty ->

4751N/A if Map.member v $ assumps env then nt

4751N/A else TypedTerm (ResolvedMixTerm v [] [] qs) q ty ps

4751N/A QualOp _ (PolyId i _ _) _ tys k qs | q == Inferred ->

4751N/A if Map.member i $ localVars env then ntyped

4751N/A else case getMinAssumps env i of

4751N/A _ : _ : _ -> ntyped

4751N/A _ -> TypedTerm (ResolvedMixTerm i

4751N/A (if k == Infer then [] else tys) [] qs) q ty ps

4751N/A TypedTerm ntt qt tyt _ -> case qt of

4751N/A InType -> nt

4751N/A AsType -> if tyt == ty || q == Inferred then nt else ntyped

4751N/A OfType -> if tyt == ty || q == Inferred then nt else ntyped

4751N/A Inferred -> TypedTerm ntt q ty ps

4751N/A _ -> ntyped

4751N/A , foldQuantifiedTerm = \ ot _ _ _ _ ->

4751N/A let QuantifiedTerm q vs te ps = ot

4751N/A nEnv = execState (mapM_ ( \ vd ->

4751N/A case vd of

4751N/A GenVarDecl v -> addLocalVar False v

4751N/A _ -> return ()) vs) env

4751N/A in QuantifiedTerm q vs (simplifyTerm nEnv te) ps

4751N/A , foldLambdaTerm = \ ot _ _ _ _ ->

4751N/A let LambdaTerm ls p te qs = ot

4751N/A nEnv = execState (mapM_ (addLocalVar False)

4751N/A $ concatMap extractVars ls) env

4751N/A in LambdaTerm (map (simplifyPattern env) ls) p (simplifyTerm nEnv te) qs

4751N/A , foldLetTerm = \ ot _ _ _ _ ->

4751N/A let LetTerm br es te ps = ot

4751N/A addEqVars = mapM_ ( \ (ProgEq p _ _) ->

4751N/A mapM_ (addLocalVar False) $ extractVars p)

4751N/A nEnv = execState (addEqVars es) env

4751N/A in LetTerm br (map (simplifyEq nEnv) es) (simplifyTerm nEnv te) ps

4751N/A , foldProgEq = \ ot q _ _ ->

4751N/A let ProgEq p t r = ot

4751N/A nEnv = execState (mapM_ (addLocalVar False) $ extractVars p) env

4751N/A s = simplifyTerm nEnv t

4751N/A in ProgEq q s r }

4751N/A

4751N/A-- | remove qualification of unique identifiers

4751N/AsimplifyTerm :: Env -> Term -> Term

4751N/AsimplifyTerm = foldTerm . simplifyRec False

4751N/A

4751N/A-- | remove qualification of unique identifiers

4751N/AsimplifyPattern :: Env -> Term -> Term

4751N/AsimplifyPattern = foldTerm . simplifyRec True

4751N/A

4751N/AsimplifyEq :: Env -> ProgEq -> ProgEq

4751N/AsimplifyEq = foldEq . simplifyRec False

4751N/A

4751N/AsimplifySentence :: Env -> Sentence -> Sentence

4751N/AsimplifySentence env s = case s of

4751N/A Formula t -> Formula $ simplifyTerm env t

5061N/A ProgEqSen i sc eq -> ProgEqSen i sc $ simplifyEq env eq

4751N/A _ -> s

4751N/A