content: {- |
  Module      :  ./HasCASL/MinType.hs
  Description :  choose a minimal type for overloaded terms
  Copyright   :  (c) Christian Maeder and Uni Bremen 2003
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  choose a minimal type
  -}
  
  module HasCASL.MinType
    ( q2p
    , typeNub
    , haveCommonSupertype
    , getCommonSupertype
    ) where
  
  import HasCASL.As
  import HasCASL.FoldType
  import HasCASL.Le
  import HasCASL.AsUtils
  import HasCASL.TypeAna
  import HasCASL.Unify
  import HasCASL.Constrain
  
  import qualified Data.Set as Set
  import qualified Data.Map as Map
  import qualified Common.Lib.Rel as Rel
  import Common.DocUtils
  import Common.Id
  import Common.Result
  import Common.Lib.State
  import Common.Utils
  
  import Data.List as List
  import Data.Maybe
  
  q2p :: (a, b, c, d) -> (c, d)
  q2p (_, _, c, d) = (c, d)
  
  typeNub :: Env -> (a -> (Type, Term)) -> [a] -> [a]
  typeNub e f = let
      comp (ty1, t1) (ty2, t2) = eqTerm e t1 t2 &&
                                 lesserType e ty1 ty2
      lt a b = comp (f a) (f b)
      in keepMins lt
  
  eqTerm :: Env -> Term -> Term -> Bool
  eqTerm e t1 t2 = case (t1, t2) of
       (TypedTerm t _ _ _, _) -> eqTerm e t t2
       (_, TypedTerm t _ _ _) -> eqTerm e t1 t
       (QualVar (VarDecl v1 _s1 _ _), QualVar (VarDecl v2 _s2 _ _)) ->
           v1 == v2
       (QualOp _ i1 s1 _ _ _, QualOp _ i2 s2 _ _ _) -> i1 == i2
           && haveCommonSupertype e s1 s2
       (ApplTerm tf1 ta1 _, ApplTerm tf2 ta2 _) ->
           eqTerm e tf1 tf2 && eqTerm e ta1 ta2
       (TupleTerm ts1 _, TupleTerm ts2 _) ->
           length ts1 == length ts2 && and (zipWith (eqTerm e) ts1 ts2)
       (QuantifiedTerm q1 vs1 f1 _, QuantifiedTerm q2 vs2 f2 _) ->
           (q1, vs1) == (q2, vs2) && eqTerm e f1 f2
       (LambdaTerm ps1 p1 f1 _, LambdaTerm ps2 p2 f2 _) ->
            and (zipWith (eqTerm e) ps1 ps2) && p1 == p2 && eqTerm e f1 f2
            && length ps1 == length ps2
       (CaseTerm f1 e1 _, CaseTerm f2 e2 _) ->
           eqTerm e f1 f2 && length e1 == length e2
           && and (zipWith (eqProgEq e) e1 e2)
       (LetTerm _ e1 f1 _, LetTerm _ e2 f2 _) ->
           eqTerm e f1 f2 && length e1 == length e2
           && and (zipWith (eqProgEq e) e1 e2)
       _ -> False
  
  eqProgEq :: Env -> ProgEq -> ProgEq -> Bool
  eqProgEq e (ProgEq p1 t1 _) (ProgEq p2 t2 _) = eqTerm e p1 p2 && eqTerm e t1 t2
  
  addToEnv :: (Type, VarKind) -> Env -> Env
  addToEnv (ty, vk) e = case ty of
      TypeName i rk c | c > 0 ->
          execState (addLocalTypeVar False (TypeVarDefn NonVar vk rk c) i) e
      _ -> e
  
  haveCommonSupertype :: Env -> TypeScheme -> TypeScheme -> Bool
  haveCommonSupertype e s = isJust . getCommonSupertype e s
  
  getCommonSupertype :: Env -> TypeScheme -> TypeScheme -> Maybe TypeTriple
  getCommonSupertype e s1 s2 =
      evalState (toEnvState $ haveCommonSupertypeE e s1 s2) e
  
  type TypeTriple = (Type, [Type], Type, [Type], [TypeArg], Type)
  
  haveCommonSupertypeE :: Env -> TypeScheme -> TypeScheme
    -> State Int (Maybe TypeTriple)
  haveCommonSupertypeE eIn s1 s2 = do
      (t1, l1) <- freshInst s1
      (t2, l2) <- freshInst s2
      cst <- mkSingleSubst (genName "commonSupertype", rStar)
      let cs = Set.fromList [Subtyping t1 cst, Subtyping t2 cst]
          e = foldr addToEnv eIn $ (cst, VarKind universe) : l1 ++ l2
      Result _ mr <- shapeRelAndSimplify False e cs (Just cst)
      return $ case mr of
        Nothing -> Nothing
        Just (sbst, rcs) -> let (qs, subC) = partitionC rcs
          in case reduceCommonSubtypes
                 (Rel.transClosure $ fromTypeMap $ typeMap e)
                 (toListC subC) of
               Just msb | Set.null qs -> let
                 doSubst = subst $ compSubst sbst msb
                 [ty, ty1, ty2] = map doSubst [cst, t1, t2]
                 fvs = foldr1 List.union $ map freeTVars [ty1, ty2, ty]
                 svs = sortBy comp fvs
                 comp a b = compare (fst a) $ fst b
                 tvs = localTypeVars e
                 newArgs = map ( \ (_, (i, _)) -> case Map.lookup i tvs of
                    Nothing -> error $ "generalizeS " ++ show (i, ty)
                        ++ "\n" ++ showDoc (s1, s2) ""
                    Just (TypeVarDefn v vk rk c) ->
                        TypeArg i v vk rk c Other nullRange) svs
                 genArgs = generalize newArgs
                 [gty, gty1, gty2] = map genArgs [ty, ty1, ty2]
                 gl1 = map (genArgs . doSubst . fst) l1
                 gl2 = map (genArgs . doSubst . fst) l2
                 in Just (gty1, gl1, gty2, gl2, genTypeArgs newArgs, gty)
               _ -> Nothing
  
  reduceCommonSubtypes :: Rel.Rel Type -> [(Type, Type)] -> Maybe Subst
  reduceCommonSubtypes e l = let
      mygroup = groupBy ( \ (a, b) (c, d) -> case (a, b, d) of
                    (TypeName _ _ n, TypeName _ _ 0, TypeName _ _ 0)
                        -> n > 0 && a == c
                    _ -> False)
      mypart = partition ( \ s -> case s of
                           [] -> error "reduceCommonSubtypes1"
                           [_] -> False
                           _ -> True)
      (csubts, rest) = mypart $ mygroup l
      swap = map $ \ (a, b) -> (b, a)
      (csuperts, rest2) = mypart $ mygroup $ sort $ swap (concat rest)
      mkPair s = case s of
            (a, _) : _ -> (a, map snd s)
            _ -> error "reduceCommonSubtypes2"
      subM = mapM (commonSubtype e True . mkPair) csubts
      superM = mapM (commonSubtype e False . mkPair) csuperts
      in case (concat rest2, subM, superM) of
        ([], Just l1, Just l2) -> Just $ Map.fromList $ l1 ++ l2
        _ -> Nothing
  
  commonSubtype :: Rel.Rel Type -> Bool -> (Type, [Type]) -> Maybe (Int, Type)
  commonSubtype trel b (ty, l) =
    let tySet = foldl1 Set.intersection
           $ map (if b then Rel.predecessors trel else Rel.succs trel) l
    in case ty of
      TypeName _ _ n | not (Set.null tySet) && n > 0
        -> Just (n, Set.findMin tySet)
      _ -> Nothing
  