{- |
Module      :  ./HasCASL/ProgEq.hs
Description :  convert some formulas to program equations
Copyright   :  (c) Christian Maeder and Uni Bremen 2003
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

convert some formulas to program equations
-}

module HasCASL.ProgEq where

import Common.Result
import Common.Id
import qualified Data.Map as Map
import qualified Data.Set as Set

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Le
import HasCASL.Builtin
import HasCASL.Unify (getTypeOf)
import HasCASL.MinType (haveCommonSupertype)

isOp :: OpInfo -> Bool
isOp :: OpInfo -> Bool
isOp o :: OpInfo
o = case OpInfo -> OpDefn
opDefn OpInfo
o of
    NoOpDefn _ -> Bool
True
    Definition _ _ -> Bool
True
    SelectData _ _ -> Bool
True
    _ -> Bool
False

isOpKind :: (OpInfo -> Bool) -> Env -> Term -> Bool
isOpKind :: (OpInfo -> Bool) -> Env -> Term -> Bool
isOpKind f :: OpInfo -> Bool
f e :: Env
e t :: Term
t = case Term
t of
    TypedTerm trm :: Term
trm q :: TypeQual
q _ _ -> TypeQual -> Bool
isOfType TypeQual
q Bool -> Bool -> Bool
&& (OpInfo -> Bool) -> Env -> Term -> Bool
isOpKind OpInfo -> Bool
f Env
e Term
trm
    QualOp _ (PolyId i :: Id
i _ _) sc :: TypeScheme
sc _ _ _ ->
        (Id
i Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((Id, TypeScheme) -> Id) -> [(Id, TypeScheme)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Id, TypeScheme) -> Id
forall a b. (a, b) -> a
fst [(Id, TypeScheme)]
bList) Bool -> Bool -> Bool
&&
        (OpInfo -> Bool) -> [OpInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ oi :: OpInfo
oi -> OpInfo -> Bool
f OpInfo
oi Bool -> Bool -> Bool
&& let sc2 :: TypeScheme
sc2 = OpInfo -> TypeScheme
opType OpInfo
oi in
             TypeScheme
sc TypeScheme -> TypeScheme -> Bool
forall a. Eq a => a -> a -> Bool
== TypeScheme
sc2 Bool -> Bool -> Bool
|| Env -> TypeScheme -> TypeScheme -> Bool
haveCommonSupertype Env
e TypeScheme
sc TypeScheme
sc2)
         (Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList (Set OpInfo -> [OpInfo]) -> Set OpInfo -> [OpInfo]
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> Id -> Map Id (Set OpInfo) -> Set OpInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set OpInfo
forall a. Set a
Set.empty Id
i (Map Id (Set OpInfo) -> Set OpInfo)
-> Map Id (Set OpInfo) -> Set OpInfo
forall a b. (a -> b) -> a -> b
$ Env -> Map Id (Set OpInfo)
assumps Env
e)
    _ -> Bool
False

isOfType :: TypeQual -> Bool
isOfType :: TypeQual -> Bool
isOfType q :: TypeQual
q = case TypeQual
q of
    OfType -> Bool
True
    Inferred -> Bool
True
    AsType -> Bool
False
    InType -> Bool
False

isVar :: Env -> Term -> Bool
isVar :: Env -> Term -> Bool
isVar e :: Env
e t :: Term
t = case Term
t of
    TypedTerm trm :: Term
trm q :: TypeQual
q _ _ -> TypeQual -> Bool
isOfType TypeQual
q Bool -> Bool -> Bool
&& Env -> Term -> Bool
isVar Env
e Term
trm
    QualVar _ -> Bool
True
    _ -> Bool
False

isConstrAppl :: Env -> Term -> Bool
isConstrAppl :: Env -> Term -> Bool
isConstrAppl e :: Env
e t :: Term
t = case Term
t of
    TypedTerm trm :: Term
trm q :: TypeQual
q _ _ -> TypeQual -> Bool
isOfType TypeQual
q Bool -> Bool -> Bool
&& Env -> Term -> Bool
isConstrAppl Env
e Term
trm
    ApplTerm t1 :: Term
t1 t2 :: Term
t2 _ -> Env -> Term -> Bool
isConstrAppl Env
e Term
t1 Bool -> Bool -> Bool
&& Env -> Term -> Bool
isPat Env
e Term
t2
    _ -> (OpInfo -> Bool) -> Env -> Term -> Bool
isOpKind OpInfo -> Bool
isConstructor Env
e Term
t

isPat :: Env -> Term -> Bool
isPat :: Env -> Term -> Bool
isPat e :: Env
e t :: Term
t = case Term
t of
    TypedTerm trm :: Term
trm q :: TypeQual
q _ _ -> TypeQual -> Bool
isOfType TypeQual
q Bool -> Bool -> Bool
&& Env -> Term -> Bool
isPat Env
e Term
trm
    TupleTerm ts :: [Term]
ts _ -> (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Env -> Term -> Bool
isPat Env
e) [Term]
ts
    AsPattern _ p :: Term
p _ -> Env -> Term -> Bool
isPat Env
e Term
p
    _ -> Env -> Term -> Bool
isVar Env
e Term
t Bool -> Bool -> Bool
|| Env -> Term -> Bool
isConstrAppl Env
e Term
t

isLHS :: Env -> Term -> Bool
isLHS :: Env -> Term -> Bool
isLHS e :: Env
e t :: Term
t = case Term
t of
    TypedTerm trm :: Term
trm q :: TypeQual
q _ _ -> TypeQual -> Bool
isOfType TypeQual
q Bool -> Bool -> Bool
&& Env -> Term -> Bool
isLHS Env
e Term
trm
    ApplTerm t1 :: Term
t1 t2 :: Term
t2 _ -> Env -> Term -> Bool
isLHS Env
e Term
t1 Bool -> Bool -> Bool
&& Env -> Term -> Bool
isPat Env
e Term
t2
    _ -> (OpInfo -> Bool) -> Env -> Term -> Bool
isOpKind OpInfo -> Bool
isOp Env
e Term
t

isExecutable :: Env -> Term -> Bool
isExecutable :: Env -> Term -> Bool
isExecutable e :: Env
e t :: Term
t = case Term
t of
    QualVar _ -> Bool
True
    QualOp {} -> Bool
True
    QuantifiedTerm {} -> Bool
False
    TypedTerm _ InType _ _ -> Bool
False
    TypedTerm trm :: Term
trm _ _ _ -> Env -> Term -> Bool
isExecutable Env
e Term
trm
    ApplTerm t1 :: Term
t1 t2 :: Term
t2 _ -> Env -> Term -> Bool
isExecutable Env
e Term
t1 Bool -> Bool -> Bool
&& Env -> Term -> Bool
isExecutable Env
e Term
t2
    TupleTerm ts :: [Term]
ts _ -> (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Env -> Term -> Bool
isExecutable Env
e) [Term]
ts
    LambdaTerm ps :: [Term]
ps _ trm :: Term
trm _ -> (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Env -> Term -> Bool
isPat Env
e) [Term]
ps Bool -> Bool -> Bool
&& Env -> Term -> Bool
isExecutable Env
e Term
trm
    CaseTerm trm :: Term
trm ps :: [ProgEq]
ps _ -> Env -> Term -> Bool
isExecutable Env
e Term
trm Bool -> Bool -> Bool
&&
       (ProgEq -> Bool) -> [ProgEq] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ( \ (ProgEq p :: Term
p c :: Term
c _) -> Env -> Term -> Bool
isPat Env
e Term
p Bool -> Bool -> Bool
&& Env -> Term -> Bool
isExecutable Env
e Term
c) [ProgEq]
ps
    LetTerm _ ps :: [ProgEq]
ps trm :: Term
trm _ -> (ProgEq -> Bool) -> [ProgEq] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ( \ (ProgEq p :: Term
p c :: Term
c _) ->
           (Env -> Term -> Bool
isPat Env
e Term
p Bool -> Bool -> Bool
|| Env -> Term -> Bool
isLHS Env
e Term
p) Bool -> Bool -> Bool
&& Env -> Term -> Bool
isExecutable Env
e Term
c) [ProgEq]
ps
           Bool -> Bool -> Bool
&& Env -> Term -> Bool
isExecutable Env
e Term
trm
    _ -> [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error "isExecutable"

mkProgEq :: Env -> Term -> Maybe ProgEq
mkProgEq :: Env -> Term -> Maybe ProgEq
mkProgEq e :: Env
e t :: Term
t = case Term -> Maybe (Id, [Term])
getTupleAp Term
t of
    Just (i :: Id
i, [a :: Term
a, b :: Term
b]) ->
       let cond :: Term -> Term -> Bool
cond p :: Term
p r :: Term
r =
             let pvs :: [Id]
pvs = (VarDecl -> Id) -> [VarDecl] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Id
getVar ([VarDecl] -> [Id]) -> [VarDecl] -> [Id]
forall a b. (a -> b) -> a -> b
$ Term -> [VarDecl]
extractVars Term
p
                 rvs :: [Id]
rvs = (VarDecl -> Id) -> [VarDecl] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Id
getVar ([VarDecl] -> [Id]) -> [VarDecl] -> [Id]
forall a b. (a -> b) -> a -> b
$ Term -> [VarDecl]
extractVars Term
r
             in Env -> Term -> Bool
isLHS Env
e Term
p Bool -> Bool -> Bool
&& Env -> Term -> Bool
isExecutable Env
e Term
r Bool -> Bool -> Bool
&&
                 [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Id] -> [Diagnosis]
forall a. (Pretty a, GetRange a, Ord a) => [a] -> [Diagnosis]
checkUniqueness [Id]
pvs) Bool -> Bool -> Bool
&&
                      [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [Id]
rvs Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [Id]
pvs
       in if Id
i Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Id
eqId, Id
exEq, Id
eqvId] then
              if Term -> Term -> Bool
cond Term
a Term
b
                 then ProgEq -> Maybe ProgEq
forall a. a -> Maybe a
Just (ProgEq -> Maybe ProgEq) -> ProgEq -> Maybe ProgEq
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Range -> ProgEq
ProgEq Term
a Term
b (Range -> ProgEq) -> Range -> ProgEq
forall a b. (a -> b) -> a -> b
$ Id -> Range
forall a. GetRange a => a -> Range
getRange Id
i
                 else if Term -> Term -> Bool
cond Term
b Term
a then ProgEq -> Maybe ProgEq
forall a. a -> Maybe a
Just (ProgEq -> Maybe ProgEq) -> ProgEq -> Maybe ProgEq
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Range -> ProgEq
ProgEq Term
b Term
a (Range -> ProgEq) -> Range -> ProgEq
forall a b. (a -> b) -> a -> b
$ Id -> Range
forall a. GetRange a => a -> Range
getRange Id
i
                      else Env -> Term -> Maybe ProgEq
mkConstTrueEq Env
e Term
t
          else Env -> Term -> Maybe ProgEq
mkConstTrueEq Env
e Term
t
    _ -> case Term -> Maybe (Id, TypeScheme, [Term])
getAppl Term
t of
        Just (i :: Id
i, _, [f :: Term
f]) -> if Id
i Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Id
notId, Id
negId] then
            case Env -> Term -> Maybe ProgEq
mkConstTrueEq Env
e Term
f of
            Just (ProgEq p :: Term
p _ ps :: Range
ps) -> ProgEq -> Maybe ProgEq
forall a. a -> Maybe a
Just (ProgEq -> Maybe ProgEq) -> ProgEq -> Maybe ProgEq
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Range -> ProgEq
ProgEq Term
p
                (Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOp Id
falseId TypeScheme
unitTypeScheme [] Range
nullRange) Range
ps
            Nothing -> Maybe ProgEq
forall a. Maybe a
Nothing
            else Env -> Term -> Maybe ProgEq
mkConstTrueEq Env
e Term
t
        _ -> Env -> Term -> Maybe ProgEq
mkConstTrueEq Env
e Term
t

mkConstTrueEq :: Env -> Term -> Maybe ProgEq
mkConstTrueEq :: Env -> Term -> Maybe ProgEq
mkConstTrueEq e :: Env
e t :: Term
t =
    let vs :: [Id]
vs = (VarDecl -> Id) -> [VarDecl] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Id
getVar ([VarDecl] -> [Id]) -> [VarDecl] -> [Id]
forall a b. (a -> b) -> a -> b
$ Term -> [VarDecl]
extractVars Term
t in
        if Env -> Term -> Bool
isLHS Env
e Term
t Bool -> Bool -> Bool
&& [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Id] -> [Diagnosis]
forall a. (Pretty a, GetRange a, Ord a) => [a] -> [Diagnosis]
checkUniqueness [Id]
vs) then
           ProgEq -> Maybe ProgEq
forall a. a -> Maybe a
Just (ProgEq -> Maybe ProgEq) -> ProgEq -> Maybe ProgEq
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Range -> ProgEq
ProgEq Term
t (Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOp Id
trueId TypeScheme
unitTypeScheme [] Range
nullRange)
                    (Range -> ProgEq) -> Range -> ProgEq
forall a b. (a -> b) -> a -> b
$ Term -> Range
forall a. GetRange a => a -> Range
getRange Term
t
           else Maybe ProgEq
forall a. Maybe a
Nothing

bottom :: Type -> Term
bottom :: Type -> Term
bottom ty :: Type
ty = Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOp Id
botId TypeScheme
botType [Type
ty] Range
nullRange

mkCondEq :: Env -> Term -> Maybe ProgEq
mkCondEq :: Env -> Term -> Maybe ProgEq
mkCondEq e :: Env
e t :: Term
t = case Term -> Maybe (Id, [Term])
getTupleAp Term
t of
    Just (i :: Id
i, [p :: Term
p, r :: Term
r])
     | Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
implId -> Env -> Term -> Term -> Maybe ProgEq
mkCond Env
e Term
p Term
r
     | Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
infixIf -> Env -> Term -> Term -> Maybe ProgEq
mkCond Env
e Term
r Term
p
     | Bool
otherwise -> Env -> Term -> Maybe ProgEq
mkProgEq Env
e Term
t
    _ -> Env -> Term -> Maybe ProgEq
mkProgEq Env
e Term
t
    where
    mkCond :: Env -> Term -> Term -> Maybe ProgEq
mkCond env :: Env
env f :: Term
f p :: Term
p = case Env -> Term -> Maybe ProgEq
mkProgEq Env
env Term
p of
      Just (ProgEq lhs :: Term
lhs rhs :: Term
rhs ps :: Range
ps) ->
          let pvs :: [Id]
pvs = (VarDecl -> Id) -> [VarDecl] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Id
getVar ([VarDecl] -> [Id]) -> [VarDecl] -> [Id]
forall a b. (a -> b) -> a -> b
$ Term -> [VarDecl]
extractVars Term
lhs
              fvs :: [Id]
fvs = (VarDecl -> Id) -> [VarDecl] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl -> Id
getVar ([VarDecl] -> [Id]) -> [VarDecl] -> [Id]
forall a b. (a -> b) -> a -> b
$ Term -> [VarDecl]
extractVars Term
f
          in case Term -> Maybe Type
forall (m :: * -> *). MonadFail m => Term -> m Type
getTypeOf Term
rhs of
          Nothing -> Maybe ProgEq
forall a. Maybe a
Nothing
          Just ty :: Type
ty -> if Env -> Term -> Bool
isExecutable Env
env Term
f Bool -> Bool -> Bool
&&
             [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [Id]
fvs Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [Id]
pvs then
             ProgEq -> Maybe ProgEq
forall a. a -> Maybe a
Just (Term -> Term -> Range -> ProgEq
ProgEq Term
lhs
                   (Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm Id
whenElse TypeScheme
whenType [Type
ty] Range
nullRange
                    (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Range -> Term
TupleTerm [Term
rhs, Term
f, Type -> Term
bottom Type
ty] Range
nullRange) Range
ps)
             else Maybe ProgEq
forall a. Maybe a
Nothing
      Nothing -> Maybe ProgEq
forall a. Maybe a
Nothing

mkQuantEq :: Env -> Term -> Maybe ProgEq
mkQuantEq :: Env -> Term -> Maybe ProgEq
mkQuantEq e :: Env
e t :: Term
t = case Term
t of
    QuantifiedTerm Universal _ trm :: Term
trm _ -> Env -> Term -> Maybe ProgEq
mkQuantEq Env
e Term
trm
    {- ignore quantified variables
    do not allow conditional equations -}
    _ -> Env -> Term -> Maybe ProgEq
mkCondEq Env
e Term
t

getTupleAp :: Term -> Maybe (Id, [Term])
getTupleAp :: Term -> Maybe (Id, [Term])
getTupleAp t :: Term
t = case Term -> Maybe (Id, TypeScheme, [Term])
getAppl Term
t of
   Just (i :: Id
i, _, [tu :: Term
tu]) -> case Term -> Maybe [Term]
getTupleArgs Term
tu of
       Just ts :: [Term]
ts -> (Id, [Term]) -> Maybe (Id, [Term])
forall a. a -> Maybe a
Just (Id
i, [Term]
ts)
       Nothing -> Maybe (Id, [Term])
forall a. Maybe a
Nothing
   _ -> Maybe (Id, [Term])
forall a. Maybe a
Nothing

translateSen :: Env -> Sentence -> Sentence
translateSen :: Env -> Sentence -> Sentence
translateSen env :: Env
env s :: Sentence
s = case Sentence
s of
        Formula t :: Term
t -> case Env -> Term -> Maybe ProgEq
mkQuantEq Env
env Term
t of
                 Nothing -> Sentence
s
                 Just pe :: ProgEq
pe@(ProgEq p :: Term
p _ _) -> case Term -> Maybe (Id, TypeScheme, [Term])
getAppl Term
p of
                     Nothing -> Sentence
s
                     Just (i :: Id
i, sc :: TypeScheme
sc, _) -> Id -> TypeScheme -> ProgEq -> Sentence
ProgEqSen Id
i TypeScheme
sc ProgEq
pe
        _ -> Sentence
s