SimplifyTerm.hs revision 09249711700a6acbc40a2e337688b434d7aafa28
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederModule : $Header$
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederDescription : simplify terms for prettier printing
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2005
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederMaintainer : Christian.Maeder@dfki.de
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederStability : provisional
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaederPortability : portable
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederremove type annotations of unique variables or operations
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maederimport qualified Data.Map as Map
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaedersimplifyRec :: Env -> MapRec
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaedersimplifyRec env = mapRec
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder { foldQualVar = \ t (VarDecl v _ _ ps) ->
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder if Map.member v $ assumps env then t else ResolvedMixTerm v [] [] ps
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder , foldQualOp = \ trm _ (InstOpId i _ _) _ ps ->
8191ab400cc9ebb5a3f6c6f18104a208aae187e8Christian Maeder if Map.member i $ localVars env then trm else
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder case Map.lookup i $ assumps env of
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder Just (OpInfos (_ : _ : _)) -> trm
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder _ -> ResolvedMixTerm i [] [] ps
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder , foldTypedTerm = \ _ nt q ty ps ->
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder let ntyped = TypedTerm nt q ty ps in case q of
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder InType -> ntyped
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder AsType -> ntyped
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder _ -> case nt of
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder QualVar (VarDecl v oty _ qs) | oty == ty ->
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder if Map.member v $ assumps env then ntyped
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder else TypedTerm (ResolvedMixTerm v [] [] qs) OfType ty ps
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder QualOp _ (InstOpId i _ _) _ qs | q == Inferred ->
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder if Map.member i $ localVars env then ntyped
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder else TypedTerm (ResolvedMixTerm i [] [] qs) OfType ty ps
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder , foldQuantifiedTerm = \ (QuantifiedTerm q vs te ps) _ _ _ _ ->
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder let nEnv = execState (mapM_ ( \ vd ->
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder GenVarDecl v -> addLocalVar False v
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder _ -> return ()) vs) env
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder in QuantifiedTerm q vs (simplifyTerm nEnv te) ps
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder , foldLambdaTerm = \ (LambdaTerm ls p te qs) ps _ _ _ ->
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder let nEnv = execState (mapM_ (addLocalVar False)
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder $ concatMap extractVars ls) env
186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder in LambdaTerm ps p (simplifyTerm nEnv te) qs
186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder , foldLetTerm = \ (LetTerm b es te ps) _ _ _ _ ->
186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder let addEqVars = mapM_ ( \ (ProgEq p _ _) ->
186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder mapM_ (addLocalVar False) $ extractVars p)
186de7a36bdf5910e0616c3a0447603e98217dc7Christian Maeder nEnv = execState (addEqVars es) env
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder in LetTerm b (map (simplifyEq nEnv) es) (simplifyTerm nEnv te) ps
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder , foldProgEq = \ (ProgEq p t r) q _ _ ->
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder let nEnv = execState (mapM_ (addLocalVar False) $ extractVars p) env
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder s = simplifyTerm nEnv t
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder in ProgEq q s r
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder-- | remove qualification of unique identifiers
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaedersimplifyTerm :: Env -> Term -> Term
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaedersimplifyTerm = foldTerm . simplifyRec
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaedersimplifyEq :: Env -> ProgEq -> ProgEq
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaedersimplifyEq = foldEq . simplifyRec
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaedersimplifySentence :: Env -> Sentence -> Sentence
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian MaedersimplifySentence env s = case s of
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder Formula t -> Formula $ simplifyTerm env t
52dc3a3b27f1bdd5128c89f96e1a5444a96474d8Christian Maeder ProgEqSen i sc eq -> ProgEqSen i sc $ simplifyEq env eq