{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module TypeChecker.PrettyPrinter (pretty) where

import Control.Unification hiding (applyBindings, (=:=))
import Control.Unification.IntVar
import Data.Functor.Fixedpoint
import Data.Text (unpack)
import Text.Printf (printf)
import TypeChecker.HindleyMilner
import Prelude hiding (lookup)

class Pretty p where
  pretty :: p -> String
  pretty = Prec -> p -> String
forall p. Pretty p => Prec -> p -> String
prettyPrec Prec
0

  prettyPrec :: Prec -> p -> String
  prettyPrec Prec
_ = p -> String
forall p. Pretty p => p -> String
pretty

type Prec = Int

instance (Pretty (t (Fix t))) => Pretty (Fix t) where
  prettyPrec :: Prec -> Fix t -> String
prettyPrec Prec
p = Prec -> t (Fix t) -> String
forall p. Pretty p => Prec -> p -> String
prettyPrec Prec
p (t (Fix t) -> String) -> (Fix t -> t (Fix t)) -> Fix t -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fix t -> t (Fix t)
forall (f :: * -> *). Fix f -> f (Fix f)
unFix

instance (Pretty t) => Pretty (TypeF t) where
  prettyPrec :: Prec -> TypeF t -> String
prettyPrec Prec
_ (TVarF Identifier
x) = Identifier -> String
unpack Identifier
x
  prettyPrec Prec
_ TypeF t
TUnitF = String
"unit"
  prettyPrec Prec
_ TypeF t
TBoolF = String
"bool"
  prettyPrec Prec
_ TypeF t
TIntF = String
"int"
  prettyPrec Prec
p (TFunF t
ty1 t
ty2) =
    Bool -> String -> String
mparens (Prec
p Prec -> Prec -> Bool
forall a. Ord a => a -> a -> Bool
> Prec
0) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Prec -> t -> String
forall p. Pretty p => Prec -> p -> String
prettyPrec Prec
1 t
ty1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Prec -> t -> String
forall p. Pretty p => Prec -> p -> String
prettyPrec Prec
0 t
ty2

instance (Pretty (t (UTerm t v)), Pretty v) => Pretty (UTerm t v) where
  pretty :: UTerm t v -> String
pretty (UTerm t (UTerm t v)
t) = t (UTerm t v) -> String
forall p. Pretty p => p -> String
pretty t (UTerm t v)
t
  pretty (UVar v
v) = v -> String
forall p. Pretty p => p -> String
pretty v
v

instance Pretty Polytype where
  pretty :: Polytype -> String
pretty (Forall [] Type
t) = Type -> String
forall p. Pretty p => p -> String
pretty Type
t
  pretty (Forall [Identifier]
xs Type
t) = [String] -> String
unwords (String
"forall" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Identifier -> String
unpack (Identifier -> String) -> [Identifier] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Identifier]
xs)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
". " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall p. Pretty p => p -> String
pretty Type
t

mparens :: Bool -> String -> String
mparens :: Bool -> String -> String
mparens Bool
True = (String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")")
mparens Bool
False = String -> String
forall a. a -> a
id

instance Pretty IntVar where
  pretty :: IntVar -> String
pretty = Identifier -> String
unpack (Identifier -> String)
-> (IntVar -> Identifier) -> IntVar -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IntVar -> Identifier
mkVarName String
"u"

instance Pretty TypeError where
  pretty :: TypeError -> String
pretty TypeError
Unreachable = String -> String
forall r. PrintfType r => String -> r
printf String
"Unreachable state"
  pretty (ImpossibleBinOpApplication UType
c1 UType
c2) = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"It is not possible to apply this operation between '%s' and '%s'" (Prec -> UType -> String
forall p. Pretty p => Prec -> p -> String
prettyPrec Prec
0 UType
c1) (Prec -> UType -> String
forall p. Pretty p => Prec -> p -> String
prettyPrec Prec
0 UType
c2)
  pretty (ImpossibleUnOpApplication UType
c) = String -> String -> String
forall r. PrintfType r => String -> r
printf String
"It is not possible to apply this operation to '%s'" (Prec -> UType -> String
forall p. Pretty p => Prec -> p -> String
prettyPrec Prec
0 UType
c)
  pretty (UnboundVar Identifier
x) = String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Unbound variable '%s'" (Identifier -> String
unpack Identifier
x)
  pretty (Infinite IntVar
x UType
ty) = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Infinite type %s = %s" (IntVar -> String
forall p. Pretty p => p -> String
pretty IntVar
x) (UType -> String
forall p. Pretty p => p -> String
pretty UType
ty)
  pretty (Mismatch TypeF UType
ty1 TypeF UType
ty2) = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"The type '%s' does not match the type '%s'" (TypeF UType -> String
forall p. Pretty p => p -> String
pretty TypeF UType
ty1) (TypeF UType -> String
forall p. Pretty p => p -> String
pretty TypeF UType
ty2)