content: module TypeAnalysis (
                       TypeAnalysis(..),
                       analyzeType,
                       analyzeType',
                       showType,
                       getWidth,
  
                       -- to be used with showType
                       kVector, vsVector, kList, vsList
                       ) where
  
  import Data.List(genericDrop, intercalate, (\\), nub, sortBy)
  import Data.Char(isUpper)
  
  import Util(doRight, itos)
  import Error(internalError, EMsg, ErrMsg(..))
  import Flags
  import PFPrint
  import Position(getPosition,noPosition)
  import Id
  import PreIds
  import Pragma
  import CType
  import Type
  import Assump
  import Pred
  import Scheme
  import SymTab
  import MakeSymTab(convCType)
  import TIMonad as TI
  import TCMisc(satisfy, mkVPredFromPred, expandSynN)
  import Subst
  
  
  -- ---------------
  
  data TypeAnalysis =
        Unknown
      -- These we handle by reporting an EMsg:
      -- | OverApplied
      -- | UnderApplied
      | Variable
      | Function
      | Numeric
      | String
      | Primary     Id Kind [Id] Bool (Maybe Integer)
      | Vector      Bool CType CType (Maybe Integer)
      | List        Bool CType
      | Alias       Id Kind [Id] CType
      | Struct      Id Kind [Id] Bool [(Id, Qual Type, Maybe Integer)] (Maybe Integer)
      | Enum        Id [Id] (Maybe Integer)
      | TaggedUnion Id Kind [Id] Bool [(Id, Type, Maybe Integer)] (Maybe Integer)
      | Interface   Id Kind [Id] Bool [(Bool, Id, Qual Type, [IfcPragma])] [IfcPragma]
      | Typeclass   Id Kind [Id] [Type] [[Bool]] (Maybe Bool) [Qual Type] [(Id, Qual Type)]
  
  
  -- ---------------
  
  getWidth :: TypeAnalysis -> Maybe Integer
  getWidth (Primary _ _ _ _ mi)       = mi
  getWidth (Vector _ _ _ mi)          = mi
  getWidth (Struct _ _ _ _ _ mi)      = mi
  getWidth (Enum _ _ mi)              = mi
  getWidth (TaggedUnion _ _ _ _ _ mi) = mi
  getWidth _                          = Nothing
  
  showType :: Bool -> Id -> Kind -> [Id] -> String
  showType showKinds t k user_vs =
      let
          arg_ks = getArgKinds k
          arg_names =
              let user_arg_names = map getIdString user_vs
              in  user_arg_names ++ (inexhaustable_var_names \\ user_arg_names)
          showArg :: Bool -> Kind -> String -> String
          showArg True arg_k name =
              (case arg_k of
                 KNum -> "numeric "
                 KStr -> "string "
                 _ -> "") ++ "type " ++ name
          showArg False arg_k name = name
          showArgs =
              "#" ++ inParens
                       (commaSep
                           (zipWith (showArg showKinds) arg_ks arg_names))
      in
          pvStr t ++
                 (if null arg_ks then [] else showArgs)
  
  
  -- make [a,...,z,aa,ab,...,zy,zz,aaa,...]
  inexhaustable_var_names :: [String]
  inexhaustable_var_names = names
    where
      names = [ x:r | r <- ([]:names),
                      x <- ['a'..'z'] ]
  
  
  -- Given a list of type arguments already supplied
  -- and a list of kinds for the remaining generic types,
  -- produce a list of tyvars to substitute for those remaining types
  -- (which doesn't clash with any names in the supplied types).
  addGenVars :: [Type] -> [Kind] -> [Type]
  addGenVars as ks =
     let
         given_tyvar_names = nub $ map (getIdBaseString . getTyVarId) (tv as)
         additional_names = inexhaustable_var_names \\ given_tyvar_names
         additional_ids = map mk_homeless_id additional_names
         additional_tyvars = zipWith cTVarKind additional_ids ks
     in
         as ++ additional_tyvars
  
  -- ---------------
  
  analyzeType :: Flags -> SymTab -> CType -> Either [EMsg] TypeAnalysis
  analyzeType flags symtab unqual_ty = analyzeType' flags symtab unqual_ty False
  
  analyzeType' :: Flags -> SymTab -> CType -> Bool -> Either [EMsg] TypeAnalysis
  analyzeType' flags symtab unqual_ty primpair_is_interface = doRight analyze (kindCheck unqual_ty)
    where
      w = getBitWidth flags symtab
  
      kindCheck :: CType -> Either [EMsg] CType
      kindCheck t =
          -- "convCType" will error on too-many-args,
          -- but we have to detect too-few-args
          case (convCType symtab t) of
            Left err -> Left [err]
            Right t' ->
                case (kind t') of
                  Kfun _ _ ->
                      let unapTypeName = ppString $ fst (splitTAp t)
                      in  Left [(getPosition t, ETypeTooFewArgs unapTypeName)]
                  k -> Right t'
  
      analyze :: CType -> Either [EMsg] TypeAnalysis
      analyze t =
         case (splitTAp t) of
           (TVar {}, as) -> Right Variable
           (TDefMonad {}, as) ->
               -- need more context
               Right Variable  -- Unknown?
           (TGen {}, as) -> internalError "analyzeType': found TGen"
           (TAp {}, as)  -> internalError "analyzeType': found TAp"
           (TCon (TyNum n pos), as) ->
               if (null as)
               then Right Numeric
               else -- Right OverApplied
                    -- (this can't happen, because kindCheck catches it)
                    Left [(pos, ENumKindArg)]
           (TCon (TyStr s pos), as) ->
               if (null as)
               then Right String
               else -- Right OverApplied
                    -- (this can't happen, because kindCheck catches it)
                    Left [(pos, EStrKindArg)]
           (TCon (TyCon i _ _), as) ->
               -- the other fields are bogus before typechecking
               analyzeTCon t i as
  
      analyzeTCon :: CType -> Id -> [CType] -> Either [EMsg] TypeAnalysis
      analyzeTCon t i as | (i == idArrow noPosition) =
          -- XXX check for full application?
          Right Function
      analyzeTCon t i as =
         -- look up the type
         case (findType symtab i) of
           Nothing -> Right Unknown
           Just (TypeInfo Nothing k vs ti) ->
              internalError "analyzeType': value type without Id"
           Just (TypeInfo (Just qi) k vs tisort) ->
              let isConcrete = null (tv as)
              in  analyzeNonNumTCon t qi k vs as isConcrete tisort
  
      analyzeNonNumTCon :: CType -> Id ->
                           Kind -> [Id] -> [CType] -> Bool -> TISort ->
                           Either [EMsg] TypeAnalysis
      -- interface
      analyzeNonNumTCon t qi k vs as isC (TIstruct (SInterface pragmas) fields) =
          if (qi == idPrimPair && (not primpair_is_interface))
          then Right $ Primary qi k vs isC (w t)
          else
            let fieldInfos = map (getFieldInfo symtab qi) fields
                mkTuple (FieldInfo _ _ _ (fid :>: (Forall ks qt)) fpragmas _ morigtype) =
                    let as' = addGenVars as ks
                        fqtype@(ps :=> ft) =
                            apType (expandSynN flags symtab . rmStructArg) (inst as' qt)
                        is_subifc = isSubInterface ft &&
                                    -- subinterfaces have no provisos
                                    -- XXX this check might be unnecessary
                                    null ps
                    in  (is_subifc, fid, fqtype, fpragmas)
            in  Right $ Interface qi k vs isC (map mkTuple fieldInfos) pragmas
      -- struct
      analyzeNonNumTCon t qi k vs as isC (TIstruct SStruct fields) =
          if (qi == idActionValue)
          then Right $ Primary qi k vs isC Nothing
          else if (qi == idPrimUnit)
          then Right $ Primary qi k vs isC (w t)
          else analyzeStructCon t qi k vs as isC fields
      -- type alias (n is the number of type parameters)
      analyzeNonNumTCon t qi k vs as isC (TItype n t') =
          if (qi == idAction)
          then Right $ Primary qi k vs isC Nothing
          else if (qi == idTuple2) || (qi == idTuple3) ||
                  (qi == idTuple4) || (qi == idTuple5) ||
                  (qi == idTuple6) || (qi == idTuple7) ||
                  (qi == idTuple8)
          then --Right $ Primary qi k vs isC (w t)
               let -- XXX assume "as" is the same size as the tuple
                   sz = length as
                   mkField :: (CType, Int) -> (Id, Qual CType, Maybe Integer)
                   mkField (t,n) = let i = mk_homeless_id ("tpl_" ++ itos n)
                                   in  (i, [] :=> t, w t)
                   fs = map mkField (zip as [1..])
               in  Right $ Struct qi k (vsTuple sz) isC fs (w t)
          else
            -- replace the generic types with the specific ones given
            -- by the user, when reporting the alias type
            -- (since the alias may not use all of the arguments,
            -- we should apply the remaining ones)
            let inst_t' = expandSynN flags symtab (inst as t')
                unused_as = genericDrop n as
            in  Right $ Alias qi k vs (cTApplys inst_t' unused_as)
      -- enum / tagged union
      analyzeNonNumTCon t qi k vs as isC (TIdata constructors is_enum) =
          if (qi == idInt)
          then Right $ Primary qi k vs isC (w t)
          else if (qi == idUInt)
          then Right $ Primary qi k vs isC (w t)
          else if (qi == idFile)
          then Right $ Primary qi k vs isC (w t)
          else if (qi == idList)
          then
            case (as) of
                [el] -> Right $ List isC el
                _ -> internalError ("analyzeType': unexpected List params: " ++
                                    ppReadable as)
          else if (qi == idVector)
          then
            case (as) of
                [len,el] -> Right $ Vector isC len el (w t)
                _ -> internalError ("analyzeType': unexpected Vector params: " ++
                                    ppReadable as)
          else
            let conInfos = map (getConInfo symtab qi) constructors
                getConType (ConInfo { ci_assump = (i :>: (Forall ks (ps :=> t))) }) = t
                getConName (ConInfo { ci_assump = (i :>: _) }) = i
            in
                -- figure out if it's enum or tagged union
                if (is_enum)
                then Right $ Enum qi (map getConName conInfos) (w t)
                else let -- we assume that 'ps' is empty (should we check?)
                         mkTuple ci =
                             let (tagT, unionT) = getUnionTypes (getConType ci)
                                 new_as = reorderUnionTypeArgs unionT as
                                 tf = expandSynN flags symtab $ inst new_as tagT
                             in  (getConName ci, tf, w tf)
                     in  Right $
                           TaggedUnion qi k vs isC (map mkTuple conInfos) (w t)
      -- abstract
      analyzeNonNumTCon t qi k vs as isC (TIabstract) =
          -- XXX if (k == KNum), should we return Numeric?
          -- XXX such as for TAdd etc?  Should TAdd#(1,2) return 3?
          Right $ Primary qi k vs isC (w t)
      -- anonymous struct in Classic tagged union
      analyzeNonNumTCon t qi k vs as isC (TIstruct (SDataCon _ _) fields) =
          analyzeStructCon t qi k vs as isC fields
      -- polymorpic field wrapper
      analyzeNonNumTCon t qi k vs as isC (TIstruct (SPolyWrap _ _ _) fields) =
        analyzeStructCon t qi k vs as isC fields
      -- type class
      analyzeNonNumTCon t qi k vs as isC (TIstruct SClass fields) =
          let
              cls = mustFindClass symtab (CTypeclass qi)
              -- for now, ignore the types provided by the user and just give
              -- the generic info for this typeclass
              orig_as = map TVar (csig cls)
  
              -- filter out the superclass members
              fields' = let isField (c:cs) | isUpper c = False
                            isField _                  = True
                        in  filter (isField . getIdBaseString) fields
              fieldInfos = map (getFieldInfo symtab qi) fields'
              mkPair (FieldInfo _ _ _ (i :>: (Forall ks qt)) _ _ _) =
                  let as' = addGenVars orig_as ks
                      qt' = apType (expandSynN flags symtab . rmStructArg) (inst as' qt)
                  in  (i, qt')
  
              ps = map (predToType . snd) (super cls)
              fdeps = funDeps cls
              insts = let mkInst (Inst _ _ (qs :=> p)) = (qs :=> predToType p)
                      in  map mkInst (getInsts cls)
              allow = allowIncoherent cls
          in  Right $ Typeclass qi k vs ps fdeps allow insts (map mkPair fieldInfos)
  
      analyzeStructCon :: CType -> Id ->
                          Kind -> [Id] -> [CType] -> Bool -> [Id] ->
                          Either [EMsg] TypeAnalysis
      analyzeStructCon t qi k vs as isC fields =
          let fieldInfos = map (getFieldInfo symtab qi) fields
              mkPair (FieldInfo _ _ _ (i :>: (Forall ks qt)) _ _ _) =
                    let as' = addGenVars as ks
                        qt' = apType (expandSynN flags symtab . rmStructArg) (inst as' qt)
                        t = qualToType qt'
                    in (i, qt', w t)
          in  Right $ Struct qi k vs isC (map mkPair fieldInfos) (w t)
  
  
  -- ---------------
  
  -- Symbol table utilities
  
  
  -- this expects not to fail to find the constructor info
  getConInfo :: SymTab -> Id -> Id -> ConInfo
  getConInfo symtab ty con =
      case (findCon symtab con) of
        Nothing -> internalError ("findConInfo: not found: " ++ ppReadable con)
        Just [ci] -> ci
        Just cis ->
            case [ ci | ci@(ConInfo { ci_id = i }) <- cis, qualEq ty i ] of
                [ci] -> ci
                []   -> internalError ("findConInfo: not found: " ++
                                       ppReadable con)
                _    -> internalError ("findConInfo: ambiguous: " ++
                                       ppReadable (con,ty))
  
  
  -- this expects not to fail to find the field info
  getFieldInfo :: SymTab -> Id -> Id -> FieldInfo
  getFieldInfo symtab ty field =
      case (findFieldInfo symtab ty field) of
        Nothing -> internalError ("findFieldInfo: not found: " ++
                                  ppReadable field)
        Just fi -> fi
  
  
  -- The type must have already had "convCType" applied to it, for the
  -- predicate reduction to work
  getBitWidth :: Flags -> SymTab -> CType -> Maybe Integer
  getBitWidth flags symtab t =
      case (findSClass symtab (CTypeclass idBits)) of
          Nothing -> Nothing -- Prelude hasn't been loaded :)
          -- Bits is a coherent typeclass
          Just c -> case (fst $ TI.runTI flags False symtab (getBitWidthM c)) of
                        Right r -> r
                        Left _  -> Nothing
    where
      getBitWidthM :: Class -> TI (Maybe Integer)
      getBitWidthM bitsCls = do
          {- Do this, if you want to return a parameterized width
            -- record any vars in the type,
            -- so that we preserve names as given by the user
            addBoundTVs (tv t)
          -}
          -- construct the proviso Bits#(t,szv) for a new var 'szv'
          szv <- newTVar "getBitWidth" KNum t
          let p = IsIn bitsCls [t, szv]
          vp <- mkVPredFromPred [] p
          -- try to satisfy the proviso
          {- Do this, if you want to return a parameterized width
            -- (use FV version, to allow TAdd/TMul in the result)
            (rs,_) <- satisfyFV [] [] [vp]
          -}
          (rs,_) <- satisfy [] [vp]
          s <- getSubst
          let szv' = apSub s szv
          -- if it was satisfiable, then apply the substitution to 'szv'
          -- and that is the width
          return $
              -- if parameterized width is desired, then allow non TyNum
              -- here as well (it could be a TyVar of TAp of TMul/TAdd/etc)
              if (null rs) && (isTNum szv')
              then Just (getTNum szv')
              else Nothing
  
  
  -- ---------------
  
  -- Type utilities
  
  kVector, kList :: Kind
  kVector = Kfun KNum (Kfun KStar KStar)
  kList   = Kfun KStar KStar
  
  vsVector, vsList :: [Id]
  vsVector = map mk_homeless_id ["vsize", "element_type"]
  vsList   = map mk_homeless_id ["element_type"]
  
  vsTuple :: Int -> [Id]
  vsTuple sz = if sz > 8
               then internalError ("vsTuple: size > 7: " ++ ppReadable sz)
               else map mk_homeless_id (take sz ["a","b","c","d","e","f","g","h"])
  
  -- apply a function to the base of a qualified type
  apType :: (Type -> Type) -> Qual Type -> Qual Type
  apType f (ps :=> t) = ps :=> f t
  
  -- Whether a type is a valid subinterface type
  -- (and should be marked "interface" and not "method").
  isSubInterface :: CType -> Bool
  isSubInterface t =
      case (leftCon t, tyConArgs t) of
        (Just con, []) | (qualEq con idClock) -> True
        (Just con, []) | (qualEq con idReset) -> True
        (Just con, [_]) | (qualEq con idInout) -> True
        (Just con, [TCon (TyNum n _), elem_t])
            | ((qualEq con idListN) || (qualEq con idVector))
          -> isSubInterface elem_t
        _ -> isInterface t
  
  -- For struct and interfaces, the fields take the struct/ifc as the
  -- first argument.  So we remove that argument when displaying the
  -- type as the user knows it.
  -- XXX should we do more to check that the first argument is the struct type?
  rmStructArg :: CType -> CType
  rmStructArg (TAp (TAp (TCon arr) c) t) | (isTConArrow arr) = t
  rmStructArg t = internalError ("rmStructArg: no arrow: " ++ ppReadable t)
  
  {-
  -- For tagged unions, get the type of the field, which is the argument.
  rmUnionRes :: CType -> CType
  rmUnionRes unionT =
      case (getArrows unionT) of
          ([argT], _) -> argT
          _ -> internalError ("rmUnionRes: wrong kind: " ++ ppReadable unionT)
  -}
  
  -- For tagged unions, get the type of the field, which is the argument;
  -- but also return the tagged union type (the result), for adjusting
  -- the type arguments into the proper order
  getUnionTypes :: CType -> (CType, CType)
  getUnionTypes unionT =
      case (getArrows unionT) of
          ([argT], resT) -> (argT, resT)
          _ -> internalError ("getUnionTypes: wrong kind: " ++ ppReadable unionT)
  
  -- reorder the type arguments to a polymorphic tagged union type,
  -- to match the order in which they are generalized in the scheme for
  -- one of the tags
  reorderUnionTypeArgs :: CType -> [CType] -> [CType]
  reorderUnionTypeArgs unionT as =
      let ts = tyConArgs unionT
          getGenIdx (TGen _ n) = n
          getGenIdx t = internalError ("reorderUnionTypeArgs: not Gen: " ++
                                       ppReadable t)
          nas = zip (map getGenIdx ts) as
          cmpFn (n1,_) (n2,_) = compare n1 n2
      in
          map snd (sortBy cmpFn nas)
  
  
  -- ---------------
  
  -- String utilities
  
  pvStr :: (PVPrint a) => a -> String
  pvStr = pvpString
  
  inParens :: String -> String
  inParens s = "(" ++ s ++ ")"
  
  commaSep :: [String] -> String
  commaSep = intercalate ", "
  
  
  -- ---------------
  