content: {- |
  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
  