-- |
-- Module      :  Cryptol.TypeCheck.PP
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE Safe #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
module Cryptol.TypeCheck.PP
  ( NameMap, WithNames(..)
  , emptyNameMap
  , ppWithNamesPrec, ppWithNames
  , nameList
  , dump
  , module Cryptol.Utils.PP
  ) where

import           Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import           Data.List(transpose)
import           Cryptol.Utils.PP


type NameMap = IntMap String

emptyNameMap :: NameMap
emptyNameMap :: NameMap
emptyNameMap = NameMap
forall a. IntMap a
IntMap.empty

-- | This packages together a type with some names to be used to display
-- the variables.  It is used for pretty printing types.
data WithNames a = WithNames a NameMap

ppWithNamesPrec :: PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec :: NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
names Int
prec a
t = Int -> WithNames a -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
prec (a -> NameMap -> WithNames a
forall a. a -> NameMap -> WithNames a
WithNames a
t NameMap
names)

ppWithNames :: PP (WithNames a) => NameMap -> a -> Doc
ppWithNames :: NameMap -> a -> Doc
ppWithNames NameMap
names a
t = NameMap -> Int -> a -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
names Int
0 a
t

dump :: PP (WithNames a) => a -> String
dump :: a -> String
dump a
x = Doc -> String
forall a. Show a => a -> String
show (NameMap -> a -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
forall a. IntMap a
IntMap.empty a
x)

-- | Compute the n-th variant of a name (e.g., @a5@).
nameVariant :: Int -> String -> String
nameVariant :: Int -> String -> String
nameVariant Int
0 String
x   = String
x
nameVariant Int
n String
x   = String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n

-- | Compute all variants of a name: @a, a1, a2, a3, ...@
nameVariants :: String -> [String]
nameVariants :: String -> [String]
nameVariants String
x = (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> String -> String
`nameVariant` String
x) [ Int
0 .. ]

-- | Expand a list of base names into an infinite list of variations.
nameList :: [String] -> [String]
nameList :: [String] -> [String]
nameList [String]
names = [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ [[String]] -> [[String]]
forall a. [[a]] -> [[a]]
transpose ([[String]] -> [[String]]) -> [[String]] -> [[String]]
forall a b. (a -> b) -> a -> b
$ (String -> [String]) -> [String] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map String -> [String]
nameVariants [String]
baseNames
  where
  baseNames :: [String]
baseNames | [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
names = (Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> String -> String
forall a. a -> [a] -> [a]
:[]) [ Char
'a' .. Char
'z' ]
            | Bool
otherwise  = [String]
names