SimplifyTerm.hs revision 16bac70d8cdc9117239d0747640c26bf68fbd500
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherModule : $Header$
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherDescription : simplify terms for prettier printing
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherCopyright : (c) Christian Maeder and Uni Bremen 2005
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherMaintainer : Christian.Maeder@dfki.de
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherStability : provisional
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallagherPortability : portable
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherremove type annotations of unique variables or operations
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagherimport qualified Data.Map as Map
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | simplify terms and patterns (if True)
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo SorcesimplifyRec :: Bool -> Env -> MapRec
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo SorcesimplifyRec b env = mapRec
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce { foldQualVar = \ t (VarDecl v ty _ ps) ->
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher if Map.member v (assumps env) then t else
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher let nv = ResolvedMixTerm v [] [] ps in
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher if b then TypedTerm nv OfType ty ps else nv
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , foldQualOp = \ trm _ (PolyId i _ _) _ tys k ps ->
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher if Map.member i $ localVars env then trm else
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher case Map.lookup i $ assumps env of
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Just s | hasMany s -> trm
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher _ -> ResolvedMixTerm i (if k == Infer then [] else tys) [] ps
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , foldTypedTerm = \ _ nt q ty ps ->
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher let ntyped = TypedTerm nt q ty ps in case q of
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher InType -> ntyped
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher AsType -> ntyped
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov _ -> case nt of
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher QualVar (VarDecl v oty _ qs) | oty == ty ->
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher if Map.member v $ assumps env then nt
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher else TypedTerm (ResolvedMixTerm v [] [] qs) q ty ps
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher QualOp _ (PolyId i _ _) _ tys k qs | q == Inferred ->
e2ac9be4f293b96f3c8992f1171e44bc1da5cfcaMichal Zidek if Map.member i $ localVars env then ntyped
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher else TypedTerm (ResolvedMixTerm i
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher (if k == Infer then [] else tys) [] qs) q ty ps
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher TypedTerm ntt qt tyt _ -> case qt of
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher AsType -> if tyt == ty || q == Inferred then nt else ntyped
e0404de84c31d2387bb244d018a5cac8d01f8b19Simo Sorce OfType -> if tyt == ty || q == Inferred then nt else ntyped
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Inferred -> TypedTerm ntt q ty ps
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , foldQuantifiedTerm = \ (QuantifiedTerm q vs te ps) _ _ _ _ ->
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher let nEnv = execState (mapM_ ( \ vd ->
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher GenVarDecl v -> addLocalVar False v
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher _ -> return ()) vs) env
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher in QuantifiedTerm q vs (simplifyTerm nEnv te) ps
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , foldLambdaTerm = \ (LambdaTerm ls p te qs) _ _ _ _ ->
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov let nEnv = execState (mapM_ (addLocalVar False)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher $ concatMap extractVars ls) env
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher in LambdaTerm (map (simplifyPattern env) ls) p (simplifyTerm nEnv te) qs
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , foldLetTerm = \ (LetTerm br es te ps) _ _ _ _ ->
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov let addEqVars = mapM_ ( \ (ProgEq p _ _) ->
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher mapM_ (addLocalVar False) $ extractVars p)
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher nEnv = execState (addEqVars es) env
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher in LetTerm br (map (simplifyEq nEnv) es) (simplifyTerm nEnv te) ps
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher , foldProgEq = \ (ProgEq p t r) q _ _ ->
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher let nEnv = execState (mapM_ (addLocalVar False) $ extractVars p) env
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher s = simplifyTerm nEnv t
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai Kondrashov in ProgEq q s r }
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher-- | remove qualification of unique identifiers
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghersimplifyTerm :: Env -> Term -> Term
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai KondrashovsimplifyTerm = foldTerm . simplifyRec False
d115f40c7a3999e3cbe705a2ff9cf0fd493f80fbMichal Zidek-- | remove qualification of unique identifiers
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghersimplifyPattern :: Env -> Term -> Term
83bf46f4066e3d5e838a32357c201de9bd6ecdfdNikolai KondrashovsimplifyPattern = foldTerm . simplifyRec True
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghersimplifyEq :: Env -> ProgEq -> ProgEq
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghersimplifyEq = foldEq . simplifyRec False
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghersimplifySentence :: Env -> Sentence -> Sentence
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen GallaghersimplifySentence env s = case s of
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher Formula t -> Formula $ simplifyTerm env t
e134a6af42102c8d865e82bf89e0b8c5a40fb5faStephen Gallagher ProgEqSen i sc eq -> ProgEqSen i sc $ simplifyEq env eq