ProgEq.hs revision 36c6cc568751e4235502cfee00ba7b597dae78dc
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder{- |
e38219f3dd2f5711440478cbffa76ce3db530543cmaederModule : $Header$
e38219f3dd2f5711440478cbffa76ce3db530543cmaederCopyright : (c) Christian Maeder and Uni Bremen 2003
e38219f3dd2f5711440478cbffa76ce3db530543cmaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederMaintainer : maeder@tzi.de
e38219f3dd2f5711440478cbffa76ce3db530543cmaederStability : experimental
e38219f3dd2f5711440478cbffa76ce3db530543cmaederPortability : portable
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederconvert some formulas to program equations
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder-}
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaedermodule HasCASL.ProgEq where
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport Common.Result
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport Common.Id
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport qualified Common.Lib.Set as Set
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport HasCASL.As
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport HasCASL.Le
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport HasCASL.VarDecl
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport HasCASL.Builtin
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport HasCASL.AsUtils
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisOp :: OpInfo -> Bool
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisOp o = case opDefn o of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder NoOpDefn _ -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder Definition _ _ -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder SelectData _ _ -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder _ -> False
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisOpKind :: (OpInfo -> Bool) -> Env -> Term -> Bool
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisOpKind f e t = case t of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder TypedTerm trm q _ _ -> isOfType q && isOpKind f e trm
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder QualOp _ (InstOpId i _ _) sc _ ->
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder if i `elem` map fst bList then False else
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder let mi = findOpId e i sc in case mi of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder Nothing -> False
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder Just oi -> f oi
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder _ -> False
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisVar, isConstrAppl, isPat, isLHS, isExecutable :: Env -> Term -> Bool
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisOfType :: TypeQual -> Bool
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisOfType q = case q of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder OfType -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder Inferred -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder AsType -> False
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder InType -> False
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisVar e t = case t of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder TypedTerm trm q _ _ -> isOfType q && isVar e trm
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder QualVar _ -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder _ -> False
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisConstrAppl e t = case t of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder TypedTerm trm q _ _ -> isOfType q && isConstrAppl e trm
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder ApplTerm t1 t2 _ -> isConstrAppl e t1 && isPat e t2
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder _ -> isOpKind isConstructor e t
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisPat e t = case t of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder TypedTerm trm q _ _ -> isOfType q && isPat e trm
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder TupleTerm ts _ -> all (isPat e) ts
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder AsPattern _ p _ -> isPat e p
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder _ -> isVar e t || isConstrAppl e t
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisLHS e t = case t of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder TypedTerm trm q _ _ -> isOfType q && isLHS e trm
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder ApplTerm t1 t2 _ -> isLHS e t1 && isPat e t2
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder _ -> isOpKind isOp e t
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisExecutable e t =
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder case t of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder QualVar _ -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder QualOp _ _ _ _ -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder QuantifiedTerm _ _ _ _ -> False
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder TypedTerm _ InType _ _ -> False
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder TypedTerm trm _ _ _ -> isExecutable e trm
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder ApplTerm t1 t2 _ -> isExecutable e t1 && isExecutable e t2
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder TupleTerm ts _ -> all (isExecutable e) ts
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder LambdaTerm ps _ trm _ -> all (isPat e) ps && isExecutable e trm
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder CaseTerm trm ps _ -> isExecutable e trm &&
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder all ( \ (ProgEq p c _) -> isPat e p && isExecutable e c) ps
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder LetTerm _ ps trm _ -> all ( \ (ProgEq p c _) ->
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder (isPat e p || isLHS e p) && isExecutable e c) ps
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder && isExecutable e trm
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder _ -> error "isExecutable"
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder
e38219f3dd2f5711440478cbffa76ce3db530543cmaedermkProgEq, mkCondEq, mkConstTrueEq, mkQuantEq :: Env -> Term -> Maybe ProgEq
e38219f3dd2f5711440478cbffa76ce3db530543cmaedermkProgEq e t = case getTupleAp t of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder Just (i, [a, b]) ->
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder let cond p r =
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder let pvs = map getVar $ extractVars p
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder rvs = map getVar $ extractVars r
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder in isLHS e p && isExecutable e r &&
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder null (checkUniqueness pvs) &&
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder Set.fromList rvs `Set.isSubsetOf` Set.fromList pvs
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder in if i `elem` [eqId, exEq, eqvId] then
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder if cond a b
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder then Just $ ProgEq a b $ get_pos i
else if cond a b then Just $ ProgEq a b $ get_pos i
else mkConstTrueEq e t
else mkConstTrueEq e t
_ -> case getAppl t of
Just (i, _, [f]) -> if i `elem` [notId, negId] then
case mkConstTrueEq e f of
Just (ProgEq p _ ps) -> Just $ ProgEq p
(mkQualOp falseId unitTypeScheme []) ps
Nothing -> Nothing
else mkConstTrueEq e t
_ -> mkConstTrueEq e t
mkConstTrueEq e t =
let vs = map getVar $ extractVars t in
if isLHS e t && null (checkUniqueness vs) then
Just $ ProgEq t (mkQualOp trueId unitTypeScheme []) $ get_pos t
else Nothing
bottom :: Term
bottom = mkQualOp botId botType []
mkCondEq e t = case getTupleAp t of
Just (i, [p, r]) ->
if i == implId then mkCond e p r
else if i == infixIf then mkCond e r p
else mkProgEq e t
_ -> mkProgEq e t
where
mkCond env f p = case mkProgEq env p of
Just (ProgEq lhs rhs ps) ->
let pvs = map getVar $ extractVars lhs
fvs = map getVar $ extractVars f
in if isExecutable env f &&
Set.fromList fvs `Set.isSubsetOf` Set.fromList pvs then
Just (ProgEq lhs
(mkTerm whenElse whenType []
$ TupleTerm [rhs, f, bottom] []) ps)
else Nothing
Nothing -> Nothing
mkQuantEq e t = case t of
QuantifiedTerm Universal _ trm _ -> mkQuantEq e trm
-- ignore quantified variables
-- do not allow conditional equations
_ -> mkCondEq e t
getTupleAp :: Term -> Maybe (Id, [Term])
getTupleAp t = case getAppl t of
Just (i, _, [tu]) -> case getTupleArgs tu of
Just ts -> Just (i, ts)
Nothing -> Nothing
_ -> Nothing
getTupleArgs :: Term -> Maybe [Term]
getTupleArgs t = case t of
TypedTerm trm qt _ _ -> case qt of
InType -> Nothing
_ -> getTupleArgs trm
TupleTerm ts _ -> Just ts
_ -> Nothing
translateSen :: Env -> Sentence -> Sentence
translateSen env s = case s of
Formula t -> case mkQuantEq env t of
Nothing -> s
Just pe@(ProgEq p _ _) -> case getAppl p of
Nothing -> s
Just (i, sc, _) -> ProgEqSen i sc pe
_ -> s