content: {- |
  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 o = case opDefn o of
      NoOpDefn _ -> True
      Definition _ _ -> True
      SelectData _ _ -> True
      _ -> False
  
  isOpKind :: (OpInfo -> Bool) -> Env -> Term -> Bool
  isOpKind f e t = case t of
      TypedTerm trm q _ _ -> isOfType q && isOpKind f e trm
      QualOp _ (PolyId i _ _) sc _ _ _ ->
          (i `notElem` map fst bList) &&
          any (\ oi -> f oi && let sc2 = opType oi in
               sc == sc2 || haveCommonSupertype e sc sc2)
           (Set.toList $ Map.findWithDefault Set.empty i $ assumps e)
      _ -> False
  
  isOfType :: TypeQual -> Bool
  isOfType q = case q of
      OfType -> True
      Inferred -> True
      AsType -> False
      InType -> False
  
  isVar :: Env -> Term -> Bool
  isVar e t = case t of
      TypedTerm trm q _ _ -> isOfType q && isVar e trm
      QualVar _ -> True
      _ -> False
  
  isConstrAppl :: Env -> Term -> Bool
  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
  
  isPat :: Env -> Term -> Bool
  isPat e t = case t of
      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
  
  isLHS :: Env -> Term -> Bool
  isLHS e t = case t of
      TypedTerm trm q _ _ -> isOfType q && isLHS e trm
      ApplTerm t1 t2 _ -> isLHS e t1 && isPat e t2
      _ -> isOpKind isOp e t
  
  isExecutable :: Env -> Term -> Bool
  isExecutable e t = case t of
      QualVar _ -> True
      QualOp {} -> True
      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
             && isExecutable e trm
      _ -> error "isExecutable"
  
  mkProgEq :: Env -> Term -> Maybe ProgEq
  mkProgEq e t = case getTupleAp t of
      Just (i, [a, b]) ->
         let cond p r =
               let pvs = map getVar $ extractVars p
                   rvs = map getVar $ extractVars r
               in isLHS e p && isExecutable e r &&
                   null (checkUniqueness pvs) &&
                        Set.fromList rvs `Set.isSubsetOf` Set.fromList pvs
         in if i `elem` [eqId, exEq, eqvId] then
                if cond a b
                   then Just $ ProgEq a b $ getRange i
                   else if cond b a then Just $ ProgEq b a $ getRange 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 [] nullRange) ps
              Nothing -> Nothing
              else mkConstTrueEq e t
          _ -> mkConstTrueEq e t
  
  mkConstTrueEq :: Env -> Term -> Maybe ProgEq
  mkConstTrueEq e t =
      let vs = map getVar $ extractVars t in
          if isLHS e t && null (checkUniqueness vs) then
             Just $ ProgEq t (mkQualOp trueId unitTypeScheme [] nullRange)
                      $ getRange t
             else Nothing
  
  bottom :: Type -> Term
  bottom ty = mkQualOp botId botType [ty] nullRange
  
  mkCondEq :: Env -> Term -> Maybe ProgEq
  mkCondEq e t = case getTupleAp t of
      Just (i, [p, r])
       | i == implId -> mkCond e p r
       | i == infixIf -> mkCond e r p
       | otherwise -> 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 case getTypeOf rhs of
            Nothing -> Nothing
            Just ty -> if isExecutable env f &&
               Set.fromList fvs `Set.isSubsetOf` Set.fromList pvs then
               Just (ProgEq lhs
                     (mkTerm whenElse whenType [ty] nullRange
                      $ TupleTerm [rhs, f, bottom ty] nullRange) ps)
               else Nothing
        Nothing -> Nothing
  
  mkQuantEq :: Env -> Term -> Maybe ProgEq
  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
  
  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
  