{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}

-- | Type checking and type inference
module L3.Core.Show where

import Data.Char (isDigit)
import Data.List (intercalate)
import L3.Core.Expr
import L3.Log
import L3.Util

newtype Name = Name String deriving (Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: Name -> Name -> Bool
Eq)

instance Enum Name where
  fromEnum :: Name -> Int
fromEnum (Name (Char
'ζ' : [Char]
digits)) = [Char] -> Int
forall a. Read a => [Char] -> a
read [Char]
digits
  fromEnum (Name [Char]
x) = Int
0
  toEnum :: Int -> Name
toEnum Int
int = [Char] -> Name
Name ([Char] -> Name) -> [Char] -> Name
forall a b. (a -> b) -> a -> b
$ [Char]
"ζ" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
int

instance Show Name where
  show :: Name -> [Char]
show (Name [Char]
s) = [Char]
s

instance (Enum a, Enum b) => Enum (Either a b) where
  fromEnum :: Either a b -> Int
fromEnum (Left a
l) = Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* a -> Int
forall a. Enum a => a -> Int
fromEnum a
l
  fromEnum (Right b
r) = Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* b -> Int
forall a. Enum a => a -> Int
fromEnum b
r Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
  toEnum :: Int -> Either a b
toEnum Int
i | Int -> Bool
forall a. Integral a => a -> Bool
even Int
i = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ Int -> a
forall a. Enum a => Int -> a
toEnum (Int -> a) -> Int -> a
forall a b. (a -> b) -> a -> b
$ Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
  toEnum Int
i = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ Int -> b
forall a. Enum a => Int -> a
toEnum (Int -> b) -> Int -> b
forall a b. (a -> b) -> a -> b
$ (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2

type ShowExpr = Expr Name

-- | Show an expression
showExpr :: (Show a) => Expr a -> String
showExpr :: Expr a -> [Char]
showExpr Expr a
Star = [Char]
"*"
showExpr Expr a
Box = [Char]
"#"
showExpr (Var a
i) = a -> [Char]
forall a. Show a => a -> [Char]
show a
i
showExpr (Lam a
i Expr a
typ Expr a
e) = [Char]
"λ [" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr a -> [Char]
forall a. Show a => Expr a -> [Char]
showExpr Expr a
typ [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"] -> " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr a -> [Char]
forall a. Show a => Expr a -> [Char]
showExpr Expr a
e
showExpr (Pi a
i Expr a
typ Expr a
e) = [Char]
"π [" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr a -> [Char]
forall a. Show a => Expr a -> [Char]
showExpr Expr a
typ [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"] -> " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr a -> [Char]
forall a. Show a => Expr a -> [Char]
showExpr Expr a
e
showExpr (App Expr a
e Expr a
expr) = [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr a -> [Char]
forall a. Show a => Expr a -> [Char]
showExpr Expr a
e [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr a -> [Char]
forall a. Show a => Expr a -> [Char]
showExpr Expr a
expr [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

instance Show a => Show (Expr a) where
  show :: Expr a -> [Char]
show = Expr a -> [Char]
forall a. Show a => Expr a -> [Char]
showExpr

type ShowCtx = Context Name

-- | Show for a context, printing each binding on a separate line.
showCtx :: (Show a) => Context a -> String
showCtx :: Context a -> [Char]
showCtx (Ctx ((a, Expr a)
c : [(a, Expr a)]
cs)) = [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (a, Expr a) -> [Char]
forall a. Show a => a -> [Char]
show (a, Expr a)
c [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Context a -> [Char]
forall a. Show a => Context a -> [Char]
showCtx ([(a, Expr a)] -> Context a
forall a. [(a, Expr a)] -> Context a
Ctx [(a, Expr a)]
cs)
showCtx (Ctx []) = [Char]
""

instance (Show a) => Show (Context a) where
  show :: Context a -> [Char]
show = Context a -> [Char]
forall a. Show a => Context a -> [Char]
showCtx