Plan 9 from Bell Labs’s /usr/web/sources/contrib/fernan/nhc98/src/compiler98/Type/Lib.hs

Copyright © 2021 Plan 9 Foundation.
Distributed under the MIT License.
Download the Plan 9 distribution.


{- ---------------------------------------------------------------------------
Various functions for type checking:
- error messages
...
-}
module Type.Lib (typeUnify,typeUnifyMany,typeUnifyApply,typePatCon,typeExpCon
               ,typeIdentDict,getIdent,getTypeErrors,typeError
               ,typeNewTVar,typeIdentDef,checkExist,funType,extendEnv,getEnv
               ,msgFun,msgPat,msgLit,msgBool,msgGdExps,msgAltExps,msgCase
               ,msgAltPats,msgIf,msgApply,msgList,msgExpType,msgAs,msgNK
               ,newIdent,getState,setState,typeOfMain
               ,msgPatGdExps,msgPatGd) where

import NT
import Type.Env(lookupEnv)
import Util.Extra(assocDef,strPos,snub,mapSnd)
import Id(Id)
import Syntax
import IdKind
import TokenId(t_Arrow,tmain,tIO,t_Tuple)
import Flags
import SyntaxPos
import Type.Subst
import Type.Unify
import Type.Data
import IntState
import Type.Util
import Info
import IO
import Error
import Nice

msgPat :: Pat id -> String -> String
msgPat pat err =
  "Type error " ++ err ++ "\nwhen unifying pattern at " ++ strPos (getPos pat) ++ " with its expression.\n"

msgFun :: Rhs id -> String -> String
msgFun gdexps err =
  "Type error " ++ err ++ "\nwhen binding final type to function at " ++ strPos (getPos gdexps) ++ ".\n"

msgExpType :: Pos -> String -> String
msgExpType pos err =
  "Type error " ++ err ++ "\nwhen unifying explicit type at " ++ strPos pos ++ ".\n"

msgGdExps :: [(Exp id, Exp id)] -> String -> String
msgGdExps gdexps err =
  "Type error " ++ err ++ "\nwhen unifying multiple guarded expressions at " ++ (strPos . getPos . head) gdexps ++ ".\n"

msgPatGdExps gdexps err =
  "Type error " ++ err ++ "\nwhen unifying pattern guarded expressions at " ++ (strPos . getPos . head) gdexps ++ ".\n"

msgBool :: Exp id -> String -> String
msgBool exp err =
  "Type error " ++ err ++ "\nwhen trying to unify expressions at " ++ strPos (getPos exp) ++ " with Bool.\n"

msgPatGd pat exp err =
  "Type error " ++ err ++ "\nwhen trying to unify expression at " ++ strPos (getPos exp) ++ "\nwith pattern at "++ strPos (getPos pat) ++ "\nin pattern guard.\n"

msgAltPats :: [Alt id] -> String -> String
msgAltPats alts err =
  "Type error " ++ err ++ "\nwhen trying to unify pattern part of alternatives at " ++ (strPos . getPos . head) alts ++ ".\n"

msgAltExps :: [Alt id] -> String -> String
msgAltExps alts err =
  "Type error " ++ err ++ "\nwhen trying to unify expression part of alternatives at " ++  (strPos . getPos . head) alts ++ ".\n"

msgCase :: Exp id -> String -> String
msgCase exp err =
  "Type error " ++ err ++ "\nwhen trying to unify expression at " ++ strPos (getPos exp) ++ " with patterns.\n"

msgIf :: Exp id -> Exp id -> String -> String
msgIf exp1 exp2 err =
  "Type error " ++ err ++ "\nwhen trying to unify then-expressions at " ++ strPos (getPos exp1)
                                          ++ " and else-expression at " ++ strPos (getPos exp2) ++ ".\n"

msgLit :: Pos -> String -> String -> a -> String
msgLit pos typ err no =
  "Type error " ++ err ++ "\nwhen processing overloaded " ++ typ ++ " at " ++ strPos pos ++ ".\n"


msgApply :: HasPos a => [a] -> String -> Int -> String

msgApply es err no =
  "Type error " ++ err ++ "\nwhen trying to apply function at " ++  (strPos . getPos . head) es ++ " to its " 
        ++ showEnum no ++ " argument at " ++ (strPos . getPos . (es !!)) no ++ ".\n"

showEnum :: Int -> String
showEnum 1 = "1st"
showEnum 2 = "2nd"
showEnum 3 = "3rd"
showEnum n = show n ++ "th"

msgList :: [Exp id] -> String -> String
msgList es err =
  "Type error " ++ err ++ "\nwhen trying to unify items in a list at " ++  (strPos . getPos . head) es ++ ".\n"

msgAs :: Pos -> String -> String
msgAs pos err =
  "Type error " ++ err ++ "\nwhen trying to unify variable at " ++ strPos pos ++ " with pattern.\n"

msgNK :: Pos -> String -> String
msgNK pos err =
  "Type error " ++ err ++ "\nwhen trying to check (n+k) pattern at " ++ strPos pos ++ ".\n"


typeOfMain :: Flags -> ((TokenId, IdKind) -> Id) -> Decls Id -> IntState -> IO IntState
typeOfMain flags tidFun (DeclsScc depends) state =
  case findMain (concatMap stripDepend depends) of
    Nothing -> hPutStr stderr "Warning: Can not find main in module Main.\n" >>
               return state
    Just imain ->
      if sShowType flags then
        case ntIS state imain of
          (NewType free [] [] [nt],state) -> do
            hPutStr stderr (niceNT Nothing state (mkAL free) nt++"\n")
            exit
          (nt,state) -> do
            hPutStr stderr (niceNewType state nt++"\n")
            exit
      else
        case ntIS state imain of
          (NewType free [] [] [nt],state) ->
            let mainType = mkNTcons (tidFun (tIO,TCon)) 
                                 [mkNTvar (tidFun (t_Tuple 0,TCon))]
            in
            case unify state idSubst (nt, mainType) of
              Right phi -> return state
              Left (phi,str) -> 
                hPutStr stderr ("Function main has the type "++
                                niceNT Nothing state (mkAL free) nt ++
                                " instead of IO ().\n") >>
                exit
          (nt,state) ->
            hPutStr stderr ("Function main has the type "++
                            niceNewType state nt ++ " instead of IO ().\n") >>
            exit
 where
   stripDepend (DeclsNoRec d) = [d]
   stripDepend (DeclsRec ds) = ds

   findMain [] = Nothing
   findMain (DeclFun pos i funs:ds) = if tidIS state i == tmain then Just i else findMain ds
   findMain (d:ds) = findMain ds


typeUnify :: ShowS -> NT -> NT -> TypeDown -> TypeState -> (NT,TypeState)

typeUnify errFun t1 t2  
  down@(TypeDown env tidFun defaults ctxDict envDict) 
  up@(TypeState state phi ctxs ectxsi) =
    {-
    trace ("\n\n1: " ++ 
           niceNT Nothing state (map (\x -> (x, 'a':show x)) [1..]) t1) $
    trace ("\n\n2: " ++ 
           niceNT Nothing state (map (\x -> (x, 'a':show x)) [1..]) t2) $
    -}
    case unify state phi (t1,t2) of
      Right phi' -> let t1' = subst phi t1 in 
                      {-
                      trace ("\n\n3: " ++ 
                             niceNT Nothing state 
                               (map (\x -> (x, 'a':show x)) [1..]) t1') $
                      -}
                      seq t1' (t1',TypeState state phi' ctxs ectxsi)
      Left  (phi',str) ->
        case uniqueIS state of
          (unique,state) -> 
             (NTany unique  -- new type variable as result to continue
                            -- despite error
             ,TypeState (addError state (errFun str)) phi' ctxs ectxsi)


typeUnifyMany :: ShowS -> [NT] -> TypeDown -> TypeState -> (NT,TypeState)

typeUnifyMany errFun []  down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) =
  case uniqueIS state of
    (unique,state) -> (NTany unique,TypeState state phi ctxs ectxsi)
typeUnifyMany errFun ts@(t:_) down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) =
      case unifyr state phi ts of
        Right phi -> let t' = subst phi t in seq t'  (t',TypeState state phi ctxs ectxsi)
        Left  (phi,str) ->
          case uniqueIS state of
            (unique,state) -> (NTany unique,TypeState (addError state (errFun str)) phi ctxs ectxsi)


typeUnifyApply :: (String -> Int -> String) 
               -> [NT] 
               -> TypeDown -> TypeState -> (NT,TypeState)

typeUnifyApply errFun (f:xs)  down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) =
  seq nextTvar (unifyApply state phi f (zip [1 .. ] xs))
 where
  (nextTvar,_) = uniqueIS state

  arrow = tidFun (t_Arrow,TCon)

  unifyApply state phi f [] = 
      let f' = subst phi f
      in seq f' (f',TypeState state phi ctxs ectxsi)
  unifyApply state phi f ((no,x):xs) = 
    case subst phi f of
      NTcons c _ [a,r] | c == arrow ->
        case unify state phi (a,x) of
          Right phi -> unifyApply state phi r xs
          Left (phi,str) ->
            case uniqueIS state of
              (unique,state) -> (NTany unique,TypeState (addError state (errFun str no)) phi ctxs ectxsi)
      phif ->
        case uniqueIS state of
          (a,state) ->
            case uniqueIS state of
              (r,state) ->
                case unify state phi (phif,mkNTcons arrow [NTany a,NTany r]) of
                  Right phi ->
                    case unify state phi (NTany a,x) of
                      Right phi -> unifyApply state phi (NTany r) xs
                      Left (phi,str) ->
                        case uniqueIS state of
                          (unique,state) -> (NTany unique,TypeState (addError state (errFun str no)) phi ctxs ectxsi)
                  Left (phi,str) ->
                    case uniqueIS state of
                      (unique,state) -> (NTany unique,TypeState (addError state (errFun str no)) phi ctxs ectxsi)
          
typeNewTVar :: t
               -> Type.Data.TypeState
               -> (NT.NT, Type.Data.TypeState)
typeNewTVar down up@(TypeState state phi ctxs ectxsi) = 
  case uniqueIS state of
    (unique,state) -> (NTany unique,TypeState state phi ctxs ectxsi)

newIdent :: t
            -> Type.Data.TypeState
            -> (Id.Id, Type.Data.TypeState)
newIdent down up@(TypeState state phi ctxs ectxsi) = 
  case uniqueIS state of
    (unique,state) -> (unique,TypeState state phi ctxs ectxsi)

getState :: t
            -> Type.Data.TypeState
            -> (IntState.IntState, Type.Data.TypeState)
getState down up@(TypeState state phi ctxs ectxsi) = 
    (state,up)

setState :: IntState.IntState
            -> t
            -> Type.Data.TypeState
            -> Type.Data.TypeState
setState state down up@(TypeState _ phi ctxs ectxsi) = 
  TypeState state phi ctxs ectxsi


extendEnv :: [(Id, NT)] -> TypeDown -> b -> (TypeDown, b)
extendEnv ext down@(TypeDown env tidFun defaults ctxDict envDict) up =
  (TypeDown (ext++env) tidFun defaults ctxDict envDict,up)

getEnv :: TypeDown -> b -> ([(Id, NT)], b)
getEnv down@(TypeDown env tidFun defaults ctxDict envDict) up =
  (env,up)

getIdent :: (TokenId, IdKind) -> TypeDown -> b -> (Id, b)
getIdent key down@(TypeDown env tidFun defaults ctxDict envDict) up =
  (tidFun key,up)

-- Drop dictionaries if it is seq, this is used in PrimCode
qDict :: t -> Exp id -> [Exp id] -> Exp id
qDict state exp [] = exp
qDict state exp dict = ExpApplication (getPos exp) (exp:map ExpDict dict)

-- Dictionaries done at call site!

typeIdentDef :: (Id -> a) -> t -> Id -> TypeDown -> TypeState -> ((a, NT), TypeState)
typeIdentDef convar pos ident down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) =
   case lookupEnv ident env of
     Just t ->                             -- Type under construction
          let t' = subst phi t
          in seq t' ((convar ident,t'),up)  -- Only let-bound identifiers in envDict
                                -- Otherwise internal error!

typeExpCon :: Pos -> Id -> TypeDown -> TypeState -> ((Exp Id, NT), TypeState)
typeExpCon pos ident down up@(TypeState state phi ctxs ectxsi) = 
  case typeExpCon' pos ident down up of
    ((exp,expT,ctxs,eTVar),up) -> ((qDict state exp ctxs,expT),up)

typeExpCon' :: Pos -> Id -> TypeDown -> TypeState -> ((Exp Id, NT, [Exp Id], [Id]), TypeState)
typeExpCon' pos ident down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) =
  case ntIS state ident of  -- Be strict!
    (NoType,state) -> -- Not possible for constructors!
          case uniqueIS state of -- Fake answer, there should be an error reported somewhere else
            (u,state) -> ((ExpCon pos ident,mkNTvar u,[],[]),TypeState state phi ctxs ectxsi)
    (nt''@(NewType _ eTVar _ _),state) -> 
     case extractCtxs nt'' of
      (nt',ctxs'') ->
        case dictAndArrows (tidFun (t_Arrow,TCon)) pos state ctxs'' nt' of
            (ictxs,nt,state) -> 
              let ctxsStripped' = map snd ictxs
                  is = map fst $ filter ((`elem` eTVar) . ( \ (TypeDict i nt intpos) -> stripNT nt) . snd) ictxs
                  ctxs' = map ( \ (TypeDict i nt intpos) -> TypeDict i (mkNTvar (stripNT nt)) intpos) ctxsStripped'
                  nt' = subst phi nt
              in seq nt' ((ExpCon pos ident,nt',map (\ i -> assocDef ctxDict 
                                                                  (error "TypeLib:204")
                                                                  i) is,eTVar),TypeState state phi (ctxs'++ctxs) ectxsi)



typePatCon :: Pos -> Id -> TypeDown -> TypeState -> ((Exp Id, NT, [Id]), TypeState)
typePatCon pos ident down up@(TypeState state phi ctxs ectxsi) = 
  case typePatCon' pos ident down up of
    ((exp,expT,ctxs,eTVar),up) -> ((qDict state exp ctxs,existNT eTVar expT,eTVar),up)

typePatCon' :: Pos -> Id -> TypeDown -> TypeState -> ((Exp Id, NT, [Exp Id], [Id]), TypeState)
typePatCon' pos ident down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs inEctxsi) =
  case ntIS state ident of  -- Be strict!
    (NoType,state) -> -- Not possible for constructors!
          case uniqueIS state of -- Fake answer, there should be an error reported somewhere else
            (u,state) -> ((ExpCon pos ident,mkNTvar u,[],[]),TypeState state phi ctxs inEctxsi)
    (nt''@(NewType _ exist _ _),state) -> 
     case extractCtxs nt'' of
      (nt',ectxs') ->
       case uniqueISs state (map (mapSnd ( \ v -> if v `elem` exist then mkNTexist v else mkNTvar v)) ectxs') of
         (ectxsi,state) ->
           let eictxs = cvi2typedict pos exist ectxsi
           in
             case dictAndArrows (tidFun (t_Arrow,TCon)) pos state [] nt' of
               (ictxs,nt,state) -> 
                  let (_,ctxs') = unzip (ictxs ++ eictxs)
                      nt' = subst phi nt
                  in seq nt' ((ExpCon pos ident,nt',map (ExpVar pos . fst) eictxs,exist),TypeState state phi (ctxs'++ctxs) (ectxsi ++ inEctxsi))

existNT :: [Id] -> NT -> NT
existNT tv t@(NTany  a) = t
existNT tv t@(NTvar  a k) = if a `elem` tv then NTexist a k else t
existNT tv t@(NTexist  a _) = t
existNT tv (NTstrict t) = NTstrict (existNT tv t)
existNT tv (NTapp t1 t2) =  NTapp (existNT tv t1) (existNT tv t2)
existNT tv (NTcons a k tas) =  NTcons a k (map (existNT tv) tas)


typeIdentDict :: (Id -> Exp Id) -> Pos -> Id -> TypeDown -> TypeState -> ((Exp Id, NT), TypeState)
typeIdentDict convar pos ident down up@(TypeState state phi ctxs ectxsi) = 
  case typeIdentDict' convar pos ident down up of
    ((exp,expT,ctxs,eTVar),up) -> ((qDict state exp ctxs,expT),up)

typeIdentDict' :: (Id -> Exp Id) -> Pos -> Id -> TypeDown -> TypeState 
                            -> ((Exp Id, NT, [Exp Id], [Id]), TypeState)
typeIdentDict' convar pos ident down@(TypeDown env tidFun defaults ctxDict envDict) up@(TypeState state phi ctxs ectxsi) =
  case ntIS state ident of  -- Be strict!
    (NoType,state) ->
      case lookupEnv ident env of
        Just t -> -- Type still under construction
          let t' = subst phi t
          in seq t' ((convar ident,t',assocDef envDict [] ident,[]),up)  -- Only let-bound identifiers in envDict
        Nothing -> -- This is an identifier bound inside a pattern that need dictionaries, i.e, an error reported elsewhere
          case uniqueIS state of
            (u,state) -> ((convar ident,mkNTvar u,[],[]),TypeState state phi ctxs ectxsi)
    (nt'@(NewType _ eTVar _ _),state) -> 
        case dictAndArrows (tidFun (t_Arrow,TCon)) pos state [] nt' of
            (ictxs,nt,state) -> 
              let (is,ctxs') = unzip ictxs
                  nt' = subst phi nt
              in seq nt' ((convar ident,nt',map (\ i -> assocDef ctxDict 
                                                                  (error "TypeLib:162")
                                                                  i) is,eTVar),TypeState state phi (ctxs'++ctxs) ectxsi)


checkExist :: [(Id, NT)] -> [Id] -> t -> TypeState -> TypeState
checkExist oldEnv eTVars down up@(TypeState state phi ctxs ectxsi) =
 case foldr (cE phi eTVars) state oldEnv of
   state -> TypeState state phi ctxs ectxsi
 where
   cE phi eTVars (v,nt) state =
      let tvars =  (snub . freeNT . subst phi) nt
      in case filter (`elem` eTVars) tvars of
        [] -> state
        _  -> case lookupIS state v of
                 Just info -> addError state ("Existential type escaped with " ++ show (tidI info))
                 Nothing ->   addError state ("Existential type escaped (internal name " ++ show v ++ ")")

      

---- ======

extractCtxs :: NewType -> (NewType, [(Id, Id)])
extractCtxs (NewType free exist ctxs nts) = 
  (NewType free exist ctxs (filter (not . contextNT) nts), map ntContext2Pair (filter contextNT nts))


dictAndArrows :: Id -> Pos -> IntState -> [(Id, Id)] -> NewType -> ([(Id, TypeDict)], NT, IntState)
dictAndArrows arrow pos state ectxs (NewType free exist ctxs nts) = 
  case uniqueISs state (map (mapSnd ( \ v -> if v `elem` exist then mkNTexist v else mkNTvar v)) (ctxs ++ ectxs)) of
    (ctxsi,state) ->
            (cvi2typedict pos exist ctxsi
            ,funType arrow nts
            ,state
            )


funType :: Id -> [NT] -> NT
funType arrow [x] = x
funType arrow (x:xs) = mkNTcons arrow [x , funType arrow xs]


typeError :: [Char] -> t -> TypeState -> a
typeError err down  up@(TypeState state phi ctxs ectxsi) =
   error err
-- (PatWildcard noPos,TypeState (addError state err) phi ctxs ectxsi) 

getTypeErrors :: t -> TypeState -> ([String], TypeState)
getTypeErrors down  up@(TypeState state phi ctxs ectxsi) =
   let (st,errs) = getErrors state in
   (errs, TypeState st phi ctxs ectxsi) 


Bell Labs OSI certified Powered by Plan 9

(Return to Plan 9 Home Page)

Copyright © 2021 Plan 9 Foundation. All Rights Reserved.
Comments to webmaster@9p.io.