isOpKind :: (OpInfo -> Bool) -> Env -> Term -> Bool
isOpKind f e t = case t of
TypedTerm trm q _ _ -> isOfType q && isOpKind f e trm
QualOp _ (InstOpId i _ _) sc _ ->
if i `elem` map fst bList then False else
let mi = findOpId e i sc in case mi of
isVar, isConstrAppl, isPat, isLHS, isExecutable :: Env -> Term -> Bool
isOfType :: TypeQual -> Bool
TypedTerm trm q _ _ -> isOfType q && isVar e trm
isConstrAppl e t = case t of
TypedTerm trm q _ _ -> isOfType q && isConstrAppl e trm
ApplTerm t1 t2 _ -> isConstrAppl e t1 && isPat e t2
_ -> isOpKind isConstructor e t
TypedTerm trm q _ _ -> isOfType q && isPat e trm
TupleTerm ts _ -> all (isPat e) ts
AsPattern _ p _ -> isPat e p
_ -> isVar e t || isConstrAppl e t
TypedTerm trm q _ _ -> isOfType q && isLHS e trm
ApplTerm t1 t2 _ -> isLHS e t1 && isPat e t2
QuantifiedTerm _ _ _ _ -> False
TypedTerm _ InType _ _ -> False
TypedTerm trm _ _ _ -> isExecutable e trm
ApplTerm t1 t2 _ -> isExecutable e t1 && isExecutable e t2
TupleTerm ts _ -> all (isExecutable e) ts
LambdaTerm ps _ trm _ -> all (isPat e) ps && isExecutable e trm
CaseTerm trm ps _ -> isExecutable e trm &&
all ( \ (ProgEq p c _) -> isPat e p && isExecutable e c) ps
LetTerm _ ps trm _ -> all ( \ (ProgEq p c _) ->
(isPat e p || isLHS e p) && isExecutable e c) ps
_ -> error "isExecutable"
mkProgEq, mkCondEq, mkConstTrueEq, mkQuantEq :: Env -> Term -> Maybe ProgEq
mkProgEq e t = case getTupleAp t of
let pvs = map getVar $ extractVars p
rvs = map getVar $ extractVars r
in isLHS e p && isExecutable e r &&
null (checkUniqueness pvs) &&
in if i `elem` [eqId, exEq, eqvId] then
then Just $ ProgEq a b $ posOfId i
else if cond a b then Just $ ProgEq a b $ posOfId i
Just (i, _, [f]) -> if i `elem` [notId, negId] then
case mkConstTrueEq e f of
Just (ProgEq p _ ps) -> Just $ ProgEq p
(mkQualOp falseId unitType []) ps
let vs = map getVar $ extractVars t in
if isLHS e t && null (checkUniqueness vs) then
Just $ ProgEq t (mkQualOp trueId unitType []) $ posOfTerm t
bottom = mkQualOp botId botType []
mkCondEq e t = case getTupleAp t of
if i == implId then mkCond e p r
else if i == infixIf then mkCond e r p
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 &&
(mkTerm whenElse whenType []
$ TupleTerm [rhs, f, bottom] []) ps)
mkQuantEq e t = case t of
QuantifiedTerm Universal _ trm _ -> mkQuantEq e trm
-- ignore quantified variables
-- do not allow conditional equations
getTupleAp :: Term -> Maybe (Id, [Term])
getTupleAp t = case getAppl t of
Just (i, _, [tu]) -> case getTupleArgs tu of
getTupleArgs :: Term -> Maybe [Term]
getTupleArgs t = case t of
TypedTerm trm qt _ _ -> case qt of
TupleTerm ts _ -> Just ts
translateSen :: Env -> Sentence -> Sentence
translateSen env s = case s of
Formula t -> case mkQuantEq env t of
Just pe@(ProgEq p _ _) -> case getAppl p of
Just (i, sc, _) -> ProgEqSen i sc pe