{- |
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 :: Bool -> Env -> MapRec
simplifyRec b :: Bool
b env :: Env
env = MapRec
mapRec
    { foldQualVar :: Term -> VarDecl -> Term
foldQualVar = \ t :: Term
t (VarDecl v :: Id
v ty :: Type
ty _ ps :: Range
ps) ->
      if Id -> Map Id (Set OpInfo) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
v (Env -> Map Id (Set OpInfo)
assumps Env
env) then Term
t else
          let nv :: Term
nv = Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm Id
v [] [] Range
ps in
          if Bool
b then Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
nv TypeQual
OfType Type
ty Range
ps else Term
nv
    , foldQualOp :: Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> Term
foldQualOp = \ trm :: Term
trm _ (PolyId i :: Id
i _ _) _ tys :: [Type]
tys k :: InstKind
k ps :: Range
ps ->
      if Id -> Map Id VarDefn -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
i (Map Id VarDefn -> Bool) -> Map Id VarDefn -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Map Id VarDefn
localVars Env
env then Term
trm else
          case Env -> Id -> [OpInfo]
getMinAssumps Env
env Id
i of
          _ : _ : _ -> Term
trm
          _ -> Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm Id
i (if InstKind
k InstKind -> InstKind -> Bool
forall a. Eq a => a -> a -> Bool
== InstKind
Infer then [] else [Type]
tys) [] Range
ps
    , foldTypedTerm :: Term -> Term -> TypeQual -> Type -> Range -> Term
foldTypedTerm = \ _ nt :: Term
nt q :: TypeQual
q ty :: Type
ty ps :: Range
ps ->
        let ntyped :: Term
ntyped = Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
nt TypeQual
q Type
ty Range
ps in case TypeQual
q of
        InType -> Term
ntyped
        AsType -> Term
ntyped
        _ -> case Term
nt of
           QualVar (VarDecl v :: Id
v oty :: Type
oty _ qs :: Range
qs) | Type
oty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ty ->
              if Id -> Map Id (Set OpInfo) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
v (Map Id (Set OpInfo) -> Bool) -> Map Id (Set OpInfo) -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Map Id (Set OpInfo)
assumps Env
env then Term
nt
              else Term -> TypeQual -> Type -> Range -> Term
TypedTerm (Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm Id
v [] [] Range
qs) TypeQual
q Type
ty Range
ps
           QualOp _ (PolyId i :: Id
i _ _) _ tys :: [Type]
tys k :: InstKind
k qs :: Range
qs | TypeQual
q TypeQual -> TypeQual -> Bool
forall a. Eq a => a -> a -> Bool
== TypeQual
Inferred ->
              if Id -> Map Id VarDefn -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Id
i (Map Id VarDefn -> Bool) -> Map Id VarDefn -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Map Id VarDefn
localVars Env
env then Term
ntyped
              else case Env -> Id -> [OpInfo]
getMinAssumps Env
env Id
i of
                _ : _ : _ -> Term
ntyped
                _ -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm (Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm Id
i
                     (if InstKind
k InstKind -> InstKind -> Bool
forall a. Eq a => a -> a -> Bool
== InstKind
Infer then [] else [Type]
tys) [] Range
qs) TypeQual
q Type
ty Range
ps
           TypedTerm ntt :: Term
ntt qt :: TypeQual
qt tyt :: Type
tyt _ -> case TypeQual
qt of
               InType -> Term
nt
               AsType -> if Type
tyt Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ty Bool -> Bool -> Bool
|| TypeQual
q TypeQual -> TypeQual -> Bool
forall a. Eq a => a -> a -> Bool
== TypeQual
Inferred then Term
nt else Term
ntyped
               OfType -> if Type
tyt Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ty Bool -> Bool -> Bool
|| TypeQual
q TypeQual -> TypeQual -> Bool
forall a. Eq a => a -> a -> Bool
== TypeQual
Inferred then Term
nt else Term
ntyped
               Inferred -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
ntt TypeQual
q Type
ty Range
ps
           _ -> Term
ntyped
    , foldQuantifiedTerm :: Term -> Quantifier -> [GenVarDecl] -> Term -> Range -> Term
foldQuantifiedTerm = \ ot :: Term
ot _ _ _ _ ->
       let QuantifiedTerm q :: Quantifier
q vs :: [GenVarDecl]
vs te :: Term
te ps :: Range
ps = Term
ot
           nEnv :: Env
nEnv = State Env () -> Env -> Env
forall s a. State s a -> s -> s
execState ((GenVarDecl -> State Env ()) -> [GenVarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ vd :: GenVarDecl
vd ->
              case GenVarDecl
vd of
              GenVarDecl v :: VarDecl
v -> Bool -> VarDecl -> State Env ()
addLocalVar Bool
False VarDecl
v
              _ -> () -> State Env ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) [GenVarDecl]
vs) Env
env
       in Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
q [GenVarDecl]
vs (Env -> Term -> Term
simplifyTerm Env
nEnv Term
te) Range
ps
    , foldLambdaTerm :: Term -> [Term] -> Partiality -> Term -> Range -> Term
foldLambdaTerm = \ ot :: Term
ot _ _ _ _ ->
       let LambdaTerm ls :: [Term]
ls p :: Partiality
p te :: Term
te qs :: Range
qs = Term
ot
           nEnv :: Env
nEnv = State Env () -> Env -> Env
forall s a. State s a -> s -> s
execState ((VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> VarDecl -> State Env ()
addLocalVar Bool
False)
                     ([VarDecl] -> State Env ()) -> [VarDecl] -> State Env ()
forall a b. (a -> b) -> a -> b
$ (Term -> [VarDecl]) -> [Term] -> [VarDecl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term -> [VarDecl]
extractVars [Term]
ls) Env
env
       in [Term] -> Partiality -> Term -> Range -> Term
LambdaTerm ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Term -> Term
simplifyPattern Env
env) [Term]
ls) Partiality
p (Env -> Term -> Term
simplifyTerm Env
nEnv Term
te) Range
qs
    , foldLetTerm :: Term -> LetBrand -> [ProgEq] -> Term -> Range -> Term
foldLetTerm = \ ot :: Term
ot _ _ _ _ ->
       let LetTerm br :: LetBrand
br es :: [ProgEq]
es te :: Term
te ps :: Range
ps = Term
ot
           addEqVars :: [ProgEq] -> State Env ()
addEqVars = (ProgEq -> State Env ()) -> [ProgEq] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ (ProgEq p :: Term
p _ _) ->
                       (VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> VarDecl -> State Env ()
addLocalVar Bool
False) ([VarDecl] -> State Env ()) -> [VarDecl] -> State Env ()
forall a b. (a -> b) -> a -> b
$ Term -> [VarDecl]
extractVars Term
p)
           nEnv :: Env
nEnv = State Env () -> Env -> Env
forall s a. State s a -> s -> s
execState ([ProgEq] -> State Env ()
addEqVars [ProgEq]
es) Env
env
       in LetBrand -> [ProgEq] -> Term -> Range -> Term
LetTerm LetBrand
br ((ProgEq -> ProgEq) -> [ProgEq] -> [ProgEq]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> ProgEq -> ProgEq
simplifyEq Env
nEnv) [ProgEq]
es) (Env -> Term -> Term
simplifyTerm Env
nEnv Term
te) Range
ps
    , foldProgEq :: ProgEq -> Term -> Term -> Range -> ProgEq
foldProgEq = \ ot :: ProgEq
ot q :: Term
q _ _ ->
        let ProgEq p :: Term
p t :: Term
t r :: Range
r = ProgEq
ot
            nEnv :: Env
nEnv = State Env () -> Env -> Env
forall s a. State s a -> s -> s
execState ((VarDecl -> State Env ()) -> [VarDecl] -> State Env ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> VarDecl -> State Env ()
addLocalVar Bool
False) ([VarDecl] -> State Env ()) -> [VarDecl] -> State Env ()
forall a b. (a -> b) -> a -> b
$ Term -> [VarDecl]
extractVars Term
p) Env
env
            s :: Term
s = Env -> Term -> Term
simplifyTerm Env
nEnv Term
t
        in Term -> Term -> Range -> ProgEq
ProgEq Term
q Term
s Range
r }

-- | remove qualification of unique identifiers
simplifyTerm :: Env -> Term -> Term
simplifyTerm :: Env -> Term -> Term
simplifyTerm = MapRec -> Term -> Term
forall a b. FoldRec a b -> Term -> a
foldTerm (MapRec -> Term -> Term) -> (Env -> MapRec) -> Env -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Env -> MapRec
simplifyRec Bool
False

-- | remove qualification of unique identifiers
simplifyPattern :: Env -> Term -> Term
simplifyPattern :: Env -> Term -> Term
simplifyPattern = MapRec -> Term -> Term
forall a b. FoldRec a b -> Term -> a
foldTerm (MapRec -> Term -> Term) -> (Env -> MapRec) -> Env -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Env -> MapRec
simplifyRec Bool
True

simplifyEq :: Env -> ProgEq -> ProgEq
simplifyEq :: Env -> ProgEq -> ProgEq
simplifyEq = MapRec -> ProgEq -> ProgEq
forall a b. FoldRec a b -> ProgEq -> b
foldEq (MapRec -> ProgEq -> ProgEq)
-> (Env -> MapRec) -> Env -> ProgEq -> ProgEq
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Env -> MapRec
simplifyRec Bool
False

simplifySentence :: Env -> Sentence -> Sentence
simplifySentence :: Env -> Sentence -> Sentence
simplifySentence env :: Env
env s :: Sentence
s = case Sentence
s of
    Formula t :: Term
t -> Term -> Sentence
Formula (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ Env -> Term -> Term
simplifyTerm Env
env Term
t
    ProgEqSen i :: Id
i sc :: TypeScheme
sc eq :: ProgEq
eq -> Id -> TypeScheme -> ProgEq -> Sentence
ProgEqSen Id
i TypeScheme
sc (ProgEq -> Sentence) -> ProgEq -> Sentence
forall a b. (a -> b) -> a -> b
$ Env -> ProgEq -> ProgEq
simplifyEq Env
env ProgEq
eq
    _ -> Sentence
s