ProgEq.hs revision 36c6cc568751e4235502cfee00ba7b597dae78dc
e38219f3dd2f5711440478cbffa76ce3db530543cmaederModule : $Header$
e38219f3dd2f5711440478cbffa76ce3db530543cmaederCopyright : (c) Christian Maeder and Uni Bremen 2003
e38219f3dd2f5711440478cbffa76ce3db530543cmaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
e38219f3dd2f5711440478cbffa76ce3db530543cmaederMaintainer : maeder@tzi.de
e38219f3dd2f5711440478cbffa76ce3db530543cmaederStability : experimental
e38219f3dd2f5711440478cbffa76ce3db530543cmaederPortability : portable
e38219f3dd2f5711440478cbffa76ce3db530543cmaederconvert some formulas to program equations
e38219f3dd2f5711440478cbffa76ce3db530543cmaederimport qualified Common.Lib.Set as Set
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisOp :: OpInfo -> Bool
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisOp o = case opDefn o of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder NoOpDefn _ -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder Definition _ _ -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder SelectData _ _ -> True
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
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisVar, isConstrAppl, isPat, isLHS, isExecutable :: Env -> Term -> Bool
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisOfType :: TypeQual -> Bool
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisOfType q = case q of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder OfType -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder Inferred -> True
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder AsType -> False
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder InType -> False
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisVar e t = case t of
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder TypedTerm trm q _ _ -> isOfType q && isVar e trm
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder QualVar _ -> True
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
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
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
e38219f3dd2f5711440478cbffa76ce3db530543cmaederisExecutable e t =
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"
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 in if i `elem` [eqId, exEq, eqvId] then
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder if cond a b
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder then Just $ ProgEq a b $ get_pos i