ProgEq.hs revision 88ece6e49930670e8fd3ee79c89a2e918d2fbd0c
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederMaintainer : maeder@tzi.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : portable
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder convert some formulas to program equations
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maederimport qualified Common.Lib.Set as Set
8197d0be8b81692f311ad5ca34e125e2cf9eecb8Christian MaederisOp :: OpInfo -> Bool
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian MaederisOp o = case opDefn o of
a6f84880cea4485fba85b521d122eba73b0df70bChristian Maeder NoOpDefn _ -> True
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder Definition _ _ -> True
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder SelectData _ _ -> True
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederisOpKind :: (OpInfo -> Bool) -> Env -> Term -> Bool
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian MaederisOpKind f e t = case t of
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder TypedTerm trm q _ _ -> isOfType q && isOpKind f e trm
878ac75d7acbbb06412e82a4c95356ce60f942deChristian Maeder QualOp _ (InstOpId i _ _) sc _ ->
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder if i `elem` map fst bList then False else
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder let mi = findOpId e i sc in case mi of
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Nothing -> False
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Just oi -> f oi
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederisVar, isConstrAppl, isPat, isLHS, isExecutable :: Env -> Term -> Bool
6b1153c560b677f9f5da2a60ee8a10de75ff90c5Christian MaederisOfType :: TypeQual -> Bool
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederisOfType q = case q of
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder OfType -> True
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Inferred -> True
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder AsType -> False
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder InType -> False
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederisVar e t = case t of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder TypedTerm trm q _ _ -> isOfType q && isVar e trm
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder QualVar _ -> True
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederisConstrAppl e t = case t of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder TypedTerm trm q _ _ -> isOfType q && isConstrAppl e trm
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder ApplTerm t1 t2 _ -> isConstrAppl e t1 && isPat e t2
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder _ -> isOpKind isConstructor e t
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederisPat e t = case t of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder TypedTerm trm q _ _ -> isOfType q && isPat e trm
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder TupleTerm ts _ -> all (isPat e) ts
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder AsPattern _ p _ -> isPat e p
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder _ -> isVar e t || isConstrAppl e t
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian MaederisLHS e t = case t of
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder TypedTerm trm q _ _ -> isOfType q && isLHS e trm
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder ApplTerm t1 t2 _ -> isLHS e t1 && isPat e t2
522913d1d69be804c9579bbc77868ec6b501b608Christian Maeder _ -> isOpKind isOp e t
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaederisExecutable e t =
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder QualVar _ -> True
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder QualOp _ _ _ _ -> True
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder QuantifiedTerm _ _ _ _ -> False
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder TypedTerm _ InType _ _ -> False
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder TypedTerm trm _ _ _ -> isExecutable e trm
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder ApplTerm t1 t2 _ -> isExecutable e t1 && isExecutable e t2
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder TupleTerm ts _ -> all (isExecutable e) ts
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder LambdaTerm ps _ trm _ -> all (isPat e) ps && isExecutable e trm
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder CaseTerm trm ps _ -> isExecutable e trm &&
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder all ( \ (ProgEq p c _) -> isPat e p && isExecutable e c) ps
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder LetTerm _ ps trm _ -> all ( \ (ProgEq p c _) ->
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder (isPat e p || isLHS e p) && isExecutable e c) ps
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder && isExecutable e trm
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder _ -> error "isExecutable"
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian MaedermkProgEq, mkCondEq, mkConstTrueEq, mkQuantEq :: Env -> Term -> Maybe ProgEq
b1bd8688a1ce545444792a307412711c2c61df5fChristian MaedermkProgEq e t = case getTupleAp t of
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder Just (i, [a, b]) ->
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder let cond p r =
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder let pvs = map getVar $ extractVars p
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder rvs = map getVar $ extractVars r
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder in isLHS e p && isExecutable e r &&
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder null (checkUniqueness pvs) &&
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Set.fromList rvs `Set.isSubsetOf` Set.fromList pvs
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder in if i `elem` [eqId, exEq, eqvId] then
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder then Just $ ProgEq a b $ get_pos i
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder else if cond a b then Just $ ProgEq a b $ get_pos i
7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder else mkConstTrueEq e t
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder else mkConstTrueEq e t
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder _ -> case getAppl t of
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Just (i, _, [f]) -> if i `elem` [notId, negId] then
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder case mkConstTrueEq e f of
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Just (ProgEq p _ ps) -> Just $ ProgEq p
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder (mkQualOp falseId unitType []) ps
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Nothing -> Nothing
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder else mkConstTrueEq e t
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder _ -> mkConstTrueEq e t
5ba383b1607c20c57e14324e72cee2c789436d5fChristian MaedermkConstTrueEq e t =
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder let vs = map getVar $ extractVars t in
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder if isLHS e t && null (checkUniqueness vs) then
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Just $ ProgEq t (mkQualOp trueId unitType []) $ get_pos t
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maederbottom :: Term
2ac1742771a267119f1d839054b5e45d0a468085Christian Maederbottom = mkQualOp botId botType []
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian MaedermkCondEq e t = case getTupleAp t of
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder Just (i, [p, r]) ->
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder if i == implId then mkCond e p r
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder else if i == infixIf then mkCond e r p
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder else mkProgEq e t
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder _ -> mkProgEq e t
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder mkCond env f p = case mkProgEq env p of
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder Just (ProgEq lhs rhs ps) ->
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder let pvs = map getVar $ extractVars lhs
2118d66b6aa3c90458925019c9b2fb986e2b2aabChristian Maeder fvs = map getVar $ extractVars f
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder in if isExecutable env f &&
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Set.fromList fvs `Set.isSubsetOf` Set.fromList pvs then
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Just (ProgEq lhs
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder (mkTerm whenElse whenType []
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder $ TupleTerm [rhs, f, bottom] []) ps)
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder Nothing -> Nothing
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedermkQuantEq e t = case t of
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder QuantifiedTerm Universal _ trm _ -> mkQuantEq e trm
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder -- ignore quantified variables
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder -- do not allow conditional equations
4805aaef9706fd26f102ffd712b99cb8778ba3c1Christian Maeder _ -> mkCondEq e t
4805aaef9706fd26f102ffd712b99cb8778ba3c1Christian MaedergetTupleAp :: Term -> Maybe (Id, [Term])
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedergetTupleAp t = case getAppl t of
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Just (i, _, [tu]) -> case getTupleArgs tu of
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder Just ts -> Just (i, ts)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder Nothing -> Nothing
cc584a730c98e711c2a244e51b102ba1821e531dChristian MaedergetTupleArgs :: Term -> Maybe [Term]
cc584a730c98e711c2a244e51b102ba1821e531dChristian MaedergetTupleArgs t = case t of
66f4f32855e7e2f0cf79b50ce6bd426598d9b166Christian Maeder TypedTerm trm qt _ _ -> case qt of
66f4f32855e7e2f0cf79b50ce6bd426598d9b166Christian Maeder InType -> Nothing
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder _ -> getTupleArgs trm
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder TupleTerm ts _ -> Just ts
35597678f1c9da703de8d0b6b66ea63247ebe884Christian MaedertranslateSen :: Env -> Sentence -> Sentence
2ac1742771a267119f1d839054b5e45d0a468085Christian MaedertranslateSen env s = case s of
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder Formula t -> case mkQuantEq env t of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Just pe@(ProgEq p _ _) -> case getAppl p of
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder Just (i, sc, _) -> ProgEqSen i sc pe