{- |

Module : ./HasCASL/SimplifyTerm.hs

Description : simplify terms for prettier printing

Copyright : (c) Christian Maeder and Uni Bremen 2005

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

remove type annotations of unique variables or operations

-}

module HasCASL.SimplifyTerm where

import HasCASL.As

import HasCASL.AsUtils

import HasCASL.VarDecl

import HasCASL.Le

import HasCASL.FoldTerm

import HasCASL.TypeAna

import Common.Lib.State

import qualified Data.Map as Map

-- | simplify terms and patterns (if True)

simplifyRec :: Bool -> Env -> MapRec

simplifyRec b env = mapRec

{ foldQualVar = \ t (VarDecl v ty _ ps) ->

if Map.member v (assumps env) then t else

let nv = ResolvedMixTerm v [] [] ps in

if b then TypedTerm nv OfType ty ps else nv

, foldQualOp = \ trm _ (PolyId i _ _) _ tys k ps ->

if Map.member i $ localVars env then trm else

case getMinAssumps env i of

_ : _ : _ -> trm

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

, foldTypedTerm = \ _ nt q ty ps ->

let ntyped = TypedTerm nt q ty ps in case q of

InType -> ntyped

AsType -> ntyped

_ -> case nt of

QualVar (VarDecl v oty _ qs) | oty == ty ->

if Map.member v $ assumps env then nt

else TypedTerm (ResolvedMixTerm v [] [] qs) q ty ps

QualOp _ (PolyId i _ _) _ tys k qs | q == Inferred ->

if Map.member i $ localVars env then ntyped

else case getMinAssumps env i of

_ : _ : _ -> ntyped

_ -> TypedTerm (ResolvedMixTerm i

(if k == Infer then [] else tys) [] qs) q ty ps

TypedTerm ntt qt tyt _ -> case qt of

InType -> nt

AsType -> if tyt == ty || q == Inferred then nt else ntyped

OfType -> if tyt == ty || q == Inferred then nt else ntyped

Inferred -> TypedTerm ntt q ty ps

_ -> ntyped

, foldQuantifiedTerm = \ ot _ _ _ _ ->

let QuantifiedTerm q vs te ps = ot

nEnv = execState (mapM_ ( \ vd ->

case vd of

GenVarDecl v -> addLocalVar False v

_ -> return ()) vs) env

in QuantifiedTerm q vs (simplifyTerm nEnv te) ps

, foldLambdaTerm = \ ot _ _ _ _ ->

let LambdaTerm ls p te qs = ot

nEnv = execState (mapM_ (addLocalVar False)

$ concatMap extractVars ls) env

in LambdaTerm (map (simplifyPattern env) ls) p (simplifyTerm nEnv te) qs

, foldLetTerm = \ ot _ _ _ _ ->

let LetTerm br es te ps = ot

addEqVars = mapM_ ( \ (ProgEq p _ _) ->

mapM_ (addLocalVar False) $ extractVars p)

nEnv = execState (addEqVars es) env

in LetTerm br (map (simplifyEq nEnv) es) (simplifyTerm nEnv te) ps

, foldProgEq = \ ot q _ _ ->

let ProgEq p t r = ot

nEnv = execState (mapM_ (addLocalVar False) $ extractVars p) env

s = simplifyTerm nEnv t

in ProgEq q s r }

-- | remove qualification of unique identifiers

simplifyTerm :: Env -> Term -> Term

simplifyTerm = foldTerm . simplifyRec False

-- | remove qualification of unique identifiers

simplifyPattern :: Env -> Term -> Term

simplifyPattern = foldTerm . simplifyRec True

simplifyEq :: Env -> ProgEq -> ProgEq

simplifyEq = foldEq . simplifyRec False

simplifySentence :: Env -> Sentence -> Sentence

simplifySentence env s = case s of

Formula t -> Formula $ simplifyTerm env t

ProgEqSen i sc eq -> ProgEqSen i sc $ simplifyEq env eq

_ -> s