content: {-# LANGUAGE OverloadedStrings #-}
  --------------------------------------------------------------------
  -- |
  -- Copyright :  (c) Edward Kmett and Dan Doel 2012
  -- License   :  BSD2
  -- Maintainer:  Edward Kmett <ekmett@gmail.com>
  -- Stability :  experimental
  -- Portability: non-portable
  --
  --------------------------------------------------------------------
  module Ermine.Pretty.Kind
    (
    -- * Pretty Printing Kinds
      prettyHardKind
    , prettyKind
    , prettySchema
    ) where
  
  import Bound
  import Control.Applicative
  import Ermine.Pretty
  import Ermine.Syntax.Kind
  
  -- $setup
  -- >>> :set -XOverloadedStrings
  
  prettyHardKind :: HardKind -> Doc
  prettyHardKind Unboxed = "#"
  prettyHardKind Star = "*"
  prettyHardKind Constraint = "Γ"
  prettyHardKind Rho = "ρ"
  prettyHardKind Phi = "φ"
  prettyHardKind Native = "!"
  
  -- | Pretty print a 'Kind'
  prettyKind :: Kind String -> Bool -> Doc
  prettyKind (Var nm)     _ = text nm
  prettyKind (HardKind h) _ = prettyHardKind h
  prettyKind (Type k)     b = prettyKind k b
  prettyKind (l :-> r)    b = parensIf b $ prettyKind l True <+> "->" <+> prettyKind r False
  
  -- | Pretty print a 'Kind', using a fresh kind variable supply
  --
  -- You should have already removed any free variables from the variable set.
  prettySchema :: Schema String -> [String] -> Doc
  prettySchema (Schema hl b) vs = prettyKind (instantiate (pure . (ns!!)) b) False
   where
   (ns, _) = chooseNames (const False) hl vs
  