TypeDecl.hs

{- |
Module      :  ./HasCASL/TypeDecl.hs
Description :  analyse type declarations
Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

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

analyse type declarations
-}

module HasCASL.TypeDecl
    ( anaFormula
    , mapAnMaybe
    , anaTypeItems
    , dataPatToType
    , ana1Datatype
    , anaDatatype
    , addDataSen
    ) where

import Common.Id
import Common.AS_Annotation
import Common.Lib.State
import qualified Data.Map as Map
import qualified Data.Set as Set
import Common.Result

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Builtin
import HasCASL.Le
import HasCASL.ClassAna
import HasCASL.TypeAna
import HasCASL.ConvertTypePattern
import HasCASL.DataAna
import HasCASL.Unify
import HasCASL.VarDecl
import HasCASL.SubtypeDecl
import HasCASL.MixAna
import HasCASL.TypeCheck

import Control.Monad

import Data.Maybe
import Data.List (group)

-- | resolve and type check a formula
anaFormula :: Annoted Term -> State Env (Maybe (Annoted Term, Annoted Term))
anaFormula at = do
    rt <- resolve $ item at
    case rt of
      Nothing -> return Nothing
      Just t -> do
          mt <- typeCheck (mkLazyType unitType) t
          return $ case mt of
              Nothing -> Nothing
              Just e -> Just (at { item = t }, at { item = e })

anaVars :: Env -> Vars -> Type -> Result Term
anaVars te vv t = case vv of
    Var v -> return $ QualVar $ VarDecl v t Other $ posOfId v
    VarTuple vs ps -> let
        (topTy, ts) = getTypeAppl t
        n = length ts in
        if n > 1 && lesserType te topTy (toProdType n nullRange) then
               if n == length vs then
                  let lrs = zipWith (anaVars te) vs ts
                      lms = map maybeResult lrs in
                      if all isJust lms then
                         return $ TupleTerm (map fromJust lms) ps
                         else Result (concatMap diags lrs) Nothing
               else mkError "wrong arity" topTy
        else mkError "product type expected" topTy

-- | lift a analysis function to annotated items
mapAnMaybe :: (Monad m) => (Annoted a -> m (Maybe b)) -> [Annoted a]
           -> m [Annoted b]
mapAnMaybe f al = do
    il <- mapM f al
    return $ map ( \ (i, a) -> replaceAnnoted (fromJust i) a) $
           filter (isJust . fst) $ zip il al

-- | analyse annotated type items
anaTypeItems :: GenKind -> [Annoted TypeItem] -> State Env [Annoted TypeItem]
anaTypeItems gk l = do
    ul <- mapAnMaybe ana1TypeItem l
    tys <- fmap reverse $ foldM ( \ r i -> case item i of
      Datatype d -> fmap (: r) $ dataPatToType d
      _ -> return r) [] ul
    rl <- mapAnMaybe (anaTypeItem gk tys) ul
    addDataSen tys
    return rl

-- | add sentences for data type definitions
addDataSen :: [DataPat] -> State Env ()
addDataSen tys = do
    tm <- gets typeMap
    let tis = map ( \ (DataPat _ i _ _ _) -> i) tys
        ds = foldr ( \ i dl -> case Map.lookup i tm of
                     Nothing -> dl
                     Just ti -> case typeDefn ti of
                                DatatypeDefn dd -> dd : dl
                                _ -> dl) [] tis
        sen = (makeNamed ("ga_" ++ showSepList (showString "_") showId tis "")
              $ DatatypeSen ds) { isDef = True }
    unless (null tys) $ appendSentences [sen]

ana1TypeItem :: Annoted TypeItem -> State Env (Maybe TypeItem)
ana1TypeItem t = case item t of
    Datatype d -> do
        md <- ana1Datatype $ replaceAnnoted d t
        return $ fmap Datatype md
    i -> return $ Just i

anaTypeDecl :: [TypePattern] -> Kind -> Range -> State Env (Maybe TypeItem)
anaTypeDecl pats kind ps = do
    cm <- gets classMap
    let Result cs _ = anaKindM kind cm
        Result ds (Just is) = convertTypePatterns pats
    addDiags $ cs ++ ds
    let ak = if null cs then kind else universe
    mis <- mapM (addTypePattern NoTypeDefn ak) is
    let newPats = map toTypePattern $ catMaybes mis
    return $ if null newPats then Nothing else Just $ TypeDecl newPats ak ps

anaIsoDecl :: [TypePattern] -> Range -> State Env (Maybe TypeItem)
anaIsoDecl pats ps = do
    let Result ds (Just is) = convertTypePatterns pats
    addDiags ds
    mis <- mapM (addTypePattern NoTypeDefn universe) is
    case catMaybes mis of
      [] -> return Nothing
      nis -> do
        let (i, _) : ris = reverse nis
        mapM_ (\ (j, _) -> addAliasType False j
              (TypeScheme [] (TypeName i rStar 0) $ posOfId j) universe) ris
        return $ Just $ IsoDecl (map toTypePattern nis) ps

setTypePatternVars :: [(Id, [TypeArg])] -> State Env [(Id, [TypeArg])]
setTypePatternVars ol = do
    l <- mapM ( \ (i, tArgs) -> do
            e <- get
            newAs <- mapM anaddTypeVarDecl tArgs
            put e
            return (i, catMaybes newAs)) ol
    let g = group $ map snd l
    case g of
      [_ : _] -> do
         newAs <- mapM anaddTypeVarDecl $ snd $ head l
         return $ map ( \ (i, _) -> (i, catMaybes newAs)) l
      _ -> do
        addDiags [mkDiag Error
            "variables must be identical for all types within one item" l]
        return []

anaSubtypeDecl :: [TypePattern] -> Type -> Range -> State Env (Maybe TypeItem)
anaSubtypeDecl pats t ps = do
    let Result ds (Just is) = convertTypePatterns pats
    addDiags ds
    tvs <- gets localTypeVars
    nis <- setTypePatternVars is
    let newPats = map toTypePattern nis
    te <- get
    putLocalTypeVars tvs
    let Result es mp = anaTypeM (Nothing, t) te
    case mp of
      Nothing -> do
        mapM_ (addTypePattern NoTypeDefn universe) is
        if null newPats then return Nothing else case t of
            TypeToken tt -> do
                let tid = simpleIdToId tt
                    newT = TypeName tid rStar 0
                addTypeId False NoTypeDefn universe tid
                mapM_ (addSuperType newT universe) nis
                return $ Just $ SubtypeDecl newPats newT ps
            _ -> do
                addDiags es
                return $ Just $ TypeDecl newPats universe ps
      Just ((rk, ks), newT) -> nonUniqueKind ks rk t $ \ kind -> do
          mapM_ (addTypePattern NoTypeDefn kind) is
          mapM_ (addSuperType newT $ rawToKind rk) nis
          return $ if null nis then Nothing else
                       Just $ SubtypeDecl newPats newT ps

anaSubtypeDefn :: Annoted TypeItem -> TypePattern -> Vars -> Type
               -> Annoted Term -> Range -> State Env (Maybe TypeItem)
anaSubtypeDefn aitm pat v t f ps = do
    let Result ds m = convertTypePattern pat
    addDiags ds
    case m of
      Nothing -> return Nothing
      Just (i, tArgs) -> do
        tvs <- gets localTypeVars
        newAs <- mapM anaddTypeVarDecl tArgs
        mt <- anaStarType t
        putLocalTypeVars tvs
        case mt of
          Nothing -> return Nothing
          Just ty -> do
            let nAs = catMaybes newAs
                fullKind = typeArgsListToKind nAs universe
                jTy = TypeName i (typeArgsListToRawKind nAs rStar) 0
                aTy = mkTypeAppl jTy $ map typeArgToType nAs
            e <- get
            let Result es mvds = anaVars e v $ monoType ty
            addDiags es
            if cyclicType i ty then do
                addDiags [mkDiag Error
                          "illegal recursive subtype definition" ty]
                return Nothing
              else case mvds of
                Nothing -> return Nothing
                Just vtt -> do
                  let vds = extractVars vtt
                  checkUniqueVars vds
                  vs <- gets localVars
                  mapM_ (addLocalVar True) vds
                  mf <- anaFormula f
                  putLocalVars vs
                  case mf of
                    Nothing -> return Nothing
                    Just (newF, resF) -> do
                      addTypeId True NoTypeDefn fullKind i
                      addSuperType ty universe (i, nAs)
                      let lab1 = getRLabel resF
                          lab = if null lab1 then getRLabel aitm else lab1
                      appendSentences [makeNamed lab
                        $ Formula $ mkEnvForall e (
                              mkForall (map GenVarDecl vds)
                              $ mkLogTerm eqvId ps
                              (TypedTerm vtt InType aTy ps) $ item resF) ps]
                      return $ Just $ SubtypeDefn (TypePattern i nAs nullRange)
                                    v ty newF ps

anaAliasType :: TypePattern -> Maybe Kind -> TypeScheme
             -> Range -> State Env (Maybe TypeItem)
anaAliasType pat mk sc ps = do
    let Result ds m = convertTypePattern pat
    addDiags ds
    case m of
      Nothing -> return Nothing
      Just (i, tArgs) -> do
        tvs <- gets localTypeVars -- save variables
        newAs <- mapM anaddTypeVarDecl tArgs
        (ik, mt) <- anaPseudoType mk sc
        putLocalTypeVars tvs
        case mt of
          Nothing -> return Nothing
          Just (TypeScheme args ty qs) ->
            if cyclicType i ty then do
                addDiags [mkDiag Error "illegal recursive type synonym" ty]
                return Nothing
              else do
                let nAs = catMaybes newAs
                    allArgs = nAs ++ args
                    fullKind = typeArgsListToKind nAs ik
                    allSc = TypeScheme allArgs ty qs
                b <- addAliasType True i allSc fullKind
                tm <- gets typeMap
                putTypeMap $ Map.map ( \ ti -> case typeDefn ti of
                    AliasTypeDefn y -> ti
                      { typeDefn = AliasTypeDefn $ expandAux tm y }
                    _ -> ti) tm
                return $ if b then Just $ AliasType
                    (TypePattern i [] nullRange) (Just fullKind) allSc ps
                         else Nothing

-- | analyse a 'TypeItem'
anaTypeItem :: GenKind -> [DataPat] -> Annoted TypeItem
            -> State Env (Maybe TypeItem)
anaTypeItem gk tys aitm = case item aitm of
    TypeDecl pats kind ps -> anaTypeDecl pats kind ps
    SubtypeDecl pats t ps -> anaSubtypeDecl pats t ps
    IsoDecl pats ps -> anaIsoDecl pats ps
    SubtypeDefn pat v t f ps -> anaSubtypeDefn aitm pat v t f ps
    AliasType pat mk sc ps -> anaAliasType pat mk sc ps
    Datatype d -> do
        mD <- anaDatatype gk tys $ replaceAnnoted d aitm
        case mD of
          Nothing -> return Nothing
          Just newD -> return $ Just $ Datatype newD

-- | pre-analyse a data type for 'anaDatatype'
ana1Datatype :: Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)
ana1Datatype aitm = do
    let DatatypeDecl pat kind alts derivs ps = item aitm
    cm <- gets classMap
    let Result cs (Just rk) = anaKindM kind cm
        k = if null cs then kind else universe
    addDiags $ checkKinds pat rStar rk ++ cs
    let rms = map ( \ c -> anaKindM (ClassKind c) cm) derivs
        mcs = map maybeResult rms
        jcs = catMaybes mcs
        newDerivs = map fst $ filter (isJust . snd) $ zip derivs mcs
        Result ds m = convertTypePattern pat
    addDiags (ds ++ concatMap diags rms)
    addDiags $ concatMap (checkKinds pat rStar) jcs
    case m of
      Nothing -> return Nothing
      Just (i, tArgs) -> do
          tvs <- gets localTypeVars
          newAs <- mapM anaddTypeVarDecl tArgs
          putLocalTypeVars tvs
          let nAs = catMaybes newAs
              fullKind = typeArgsListToKind nAs k
          addDiags $ checkUniqueTypevars nAs
          b <- addTypeId False PreDatatype fullKind i
          return $ if b then Just $ DatatypeDecl
                     (TypePattern i nAs nullRange) k alts newDerivs ps
                   else Nothing

-- | convert a data type with an analysed type pattern to a data pattern
dataPatToType :: DatatypeDecl -> State Env DataPat
dataPatToType d = case d of
    DatatypeDecl (TypePattern i nAs _) k _ _ _ -> do
      rk <- anaKind k
      return $ DataPat Map.empty i nAs rk $ patToType i nAs rk
    _ -> error "dataPatToType"

addDataSubtype :: DataPat -> Kind -> Type -> State Env ()
addDataSubtype (DataPat _ _ nAs _ rt) k st = case st of
    TypeName i _ _ -> addSuperType rt k (i, nAs)
    _ -> addDiags [mkDiag Warning "data subtype ignored" st]

-- | analyse a pre-analysed data type given all data patterns of the type item
anaDatatype :: GenKind -> [DataPat]
            -> Annoted DatatypeDecl -> State Env (Maybe DatatypeDecl)
anaDatatype genKind tys d = case item d of
    itd@(DatatypeDecl (TypePattern i nAs _) k alts _ _) -> do
       -- recompute data pattern rather than looking it up in tys
       dt@(DataPat _ _ _ rk _) <- dataPatToType itd
       let fullKind = typeArgsListToKind nAs k
       tvs <- gets localTypeVars
       mapM_ (addTypeVarDecl False . nonVarTypeArg) nAs
       mNewAlts <- fromResult $ anaAlts genKind tys dt (map item alts)
       putLocalTypeVars tvs
       case mNewAlts of
         Nothing -> return Nothing
         Just newAlts -> do
           mapM_ (addDataSubtype dt fullKind) $ foldr
             ( \ (Construct mc ts _ _) l -> case mc of
               Nothing -> ts ++ l
               Just _ -> l) [] newAlts
           let gArgs = genTypeArgs nAs
               iMap = Map.fromList $ map (\ (DataPat _ j _ _ _) -> (j, j)) tys
               de = DataEntry iMap i genKind gArgs rk
                    $ Set.fromList newAlts
               dp = toDataPat de
           mapM_ ( \ (Construct mc tc p sels) -> case mc of
               Nothing -> return ()
               Just c -> do
                 let sc = getConstrScheme dp p tc
                 addOpId c sc Set.empty (ConstructData i)
                 mapM_ ( \ (Select ms ts pa) -> case ms of
                   Just s ->
                     addOpId s (getSelScheme dp pa ts) Set.empty $ SelectData
                         (Set.singleton $ ConstrInfo c sc) i
                   Nothing -> return False) $ concat sels) newAlts
           addTypeId True (DatatypeDefn de) fullKind i
           appendSentences $ makeDataSelEqs dp newAlts
           return $ Just itd
    _ -> error "anaDatatype (not preprocessed)"

-- | analyse a pseudo type (represented as a 'TypeScheme')
anaPseudoType :: Maybe Kind -> TypeScheme -> State Env (Kind, Maybe TypeScheme)
anaPseudoType mk (TypeScheme tArgs ty p) = do
    cm <- gets classMap
    let k = case mk of
              Nothing -> Nothing
              Just j -> let Result cs _ = anaKindM j cm
                        in Just $ if null cs then j else universe
    nAs <- mapM anaddTypeVarDecl tArgs
    let ntArgs = catMaybes nAs
    mp <- anaType (Nothing, ty)
    case mp of
      Nothing -> return (universe, Nothing)
      Just ((_, sks), newTy) -> case Set.toList sks of
        [sk] -> do
          let newK = typeArgsListToKind ntArgs sk
          irk <- anaKind newK
          case k of
            Nothing -> return ()
            Just j -> do
              grk <- anaKind j
              addDiags $ checkKinds ty grk irk
          return (newK, Just $ TypeScheme ntArgs newTy p)
        _ -> return (universe, Nothing)

-- | add a type pattern
addTypePattern :: TypeDefn -> Kind -> (Id, [TypeArg])
               -> State Env (Maybe (Id, [TypeArg]))
addTypePattern defn kind (i, tArgs) = do
        tvs <- gets localTypeVars
        newAs <- mapM anaddTypeVarDecl tArgs
        putLocalTypeVars tvs
        let nAs = catMaybes newAs
            fullKind = typeArgsListToKind nAs kind
        addDiags $ checkUniqueTypevars nAs
        b <- addTypeId True defn fullKind i
        return $ if b then Just (i, nAs) else Nothing