{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE OverloadedStrings          #-}
module RSTT.Cube where

import           Data.List   (intercalate)
import           Data.String (IsString (..))

-- | A label (constructor symbol).
newtype Label = Label { Label -> String
getLabel :: String }
  deriving newtype (Label -> Label -> Bool
(Label -> Label -> Bool) -> (Label -> Label -> Bool) -> Eq Label
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Label -> Label -> Bool
$c/= :: Label -> Label -> Bool
== :: Label -> Label -> Bool
$c== :: Label -> Label -> Bool
Eq, Eq Label
Eq Label
-> (Label -> Label -> Ordering)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Bool)
-> (Label -> Label -> Label)
-> (Label -> Label -> Label)
-> Ord Label
Label -> Label -> Bool
Label -> Label -> Ordering
Label -> Label -> Label
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Label -> Label -> Label
$cmin :: Label -> Label -> Label
max :: Label -> Label -> Label
$cmax :: Label -> Label -> Label
>= :: Label -> Label -> Bool
$c>= :: Label -> Label -> Bool
> :: Label -> Label -> Bool
$c> :: Label -> Label -> Bool
<= :: Label -> Label -> Bool
$c<= :: Label -> Label -> Bool
< :: Label -> Label -> Bool
$c< :: Label -> Label -> Bool
compare :: Label -> Label -> Ordering
$ccompare :: Label -> Label -> Ordering
Ord, Int -> Label -> String -> String
[Label] -> String -> String
Label -> String
(Int -> Label -> String -> String)
-> (Label -> String) -> ([Label] -> String -> String) -> Show Label
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Label] -> String -> String
$cshowList :: [Label] -> String -> String
show :: Label -> String
$cshow :: Label -> String
showsPrec :: Int -> Label -> String -> String
$cshowsPrec :: Int -> Label -> String -> String
Show, String -> Label
(String -> Label) -> IsString Label
forall a. (String -> a) -> IsString a
fromString :: String -> Label
$cfromString :: String -> Label
IsString)

-- | A variable.
newtype Var = Var { Var -> String
getVar :: String }
  deriving newtype (Var -> Var -> Bool
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Eq Var
-> (Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
Ord, Int -> Var -> String -> String
[Var] -> String -> String
Var -> String
(Int -> Var -> String -> String)
-> (Var -> String) -> ([Var] -> String -> String) -> Show Var
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Var] -> String -> String
$cshowList :: [Var] -> String -> String
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> String -> String
$cshowsPrec :: Int -> Var -> String -> String
Show, String -> Var
(String -> Var) -> IsString Var
forall a. (String -> a) -> IsString a
fromString :: String -> Var
$cfromString :: String -> Var
IsString)

-- | A cube expression.
data Cube
  = CubeUnit                -- ^ Unit cube: \(\mathbb{1}\).
  | CubeProduct Cube Cube   -- ^ Product of cubes: \(I \times J\).
  | CubeCon Label           -- ^ A user-defined cube, e.g. \(\mathbb{2}, \mathbb{I}\).
  | CubeVar Var             -- ^ A cube variable: \(I, J\).
  deriving (Cube -> Cube -> Bool
(Cube -> Cube -> Bool) -> (Cube -> Cube -> Bool) -> Eq Cube
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Cube -> Cube -> Bool
$c/= :: Cube -> Cube -> Bool
== :: Cube -> Cube -> Bool
$c== :: Cube -> Cube -> Bool
Eq, Eq Cube
Eq Cube
-> (Cube -> Cube -> Ordering)
-> (Cube -> Cube -> Bool)
-> (Cube -> Cube -> Bool)
-> (Cube -> Cube -> Bool)
-> (Cube -> Cube -> Bool)
-> (Cube -> Cube -> Cube)
-> (Cube -> Cube -> Cube)
-> Ord Cube
Cube -> Cube -> Bool
Cube -> Cube -> Ordering
Cube -> Cube -> Cube
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Cube -> Cube -> Cube
$cmin :: Cube -> Cube -> Cube
max :: Cube -> Cube -> Cube
$cmax :: Cube -> Cube -> Cube
>= :: Cube -> Cube -> Bool
$c>= :: Cube -> Cube -> Bool
> :: Cube -> Cube -> Bool
$c> :: Cube -> Cube -> Bool
<= :: Cube -> Cube -> Bool
$c<= :: Cube -> Cube -> Bool
< :: Cube -> Cube -> Bool
$c< :: Cube -> Cube -> Bool
compare :: Cube -> Cube -> Ordering
$ccompare :: Cube -> Cube -> Ordering
Ord, Int -> Cube -> String -> String
[Cube] -> String -> String
Cube -> String
(Int -> Cube -> String -> String)
-> (Cube -> String) -> ([Cube] -> String -> String) -> Show Cube
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Cube] -> String -> String
$cshowList :: [Cube] -> String -> String
show :: Cube -> String
$cshow :: Cube -> String
showsPrec :: Int -> Cube -> String -> String
$cshowsPrec :: Int -> Cube -> String -> String
Show)

instance IsString Cube where
  fromString :: String -> Cube
fromString = Var -> Cube
CubeVar (Var -> Cube) -> (String -> Var) -> String -> Cube
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Var
forall a. IsString a => String -> a
fromString

-- | A point in a cube.
data Point
  = PointUnit               -- ^ The only point in the unit cube: \(\star : \mathbb{1}\).
  | PointPair Point Point   -- ^ A pair of points: \(t : I, s : J \vdash \langle t, s \rangle : I \times J\).
  | PointFirst Point        -- ^ First projection: \(\pi_1\;t\).
  | PointSecond Point       -- ^ Second projection: \(\pi_2\;t\).
  | PointCon Label [Point]  -- ^ A user-defined point constructor, e.g. \(0 : \mathbb{2}\) or \(t \land s : \mathbb{I}\).
  | PointVar Var            -- ^ A point variable: \(t, s\).
  deriving (Point -> Point -> Bool
(Point -> Point -> Bool) -> (Point -> Point -> Bool) -> Eq Point
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Point -> Point -> Bool
$c/= :: Point -> Point -> Bool
== :: Point -> Point -> Bool
$c== :: Point -> Point -> Bool
Eq, Eq Point
Eq Point
-> (Point -> Point -> Ordering)
-> (Point -> Point -> Bool)
-> (Point -> Point -> Bool)
-> (Point -> Point -> Bool)
-> (Point -> Point -> Bool)
-> (Point -> Point -> Point)
-> (Point -> Point -> Point)
-> Ord Point
Point -> Point -> Bool
Point -> Point -> Ordering
Point -> Point -> Point
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Point -> Point -> Point
$cmin :: Point -> Point -> Point
max :: Point -> Point -> Point
$cmax :: Point -> Point -> Point
>= :: Point -> Point -> Bool
$c>= :: Point -> Point -> Bool
> :: Point -> Point -> Bool
$c> :: Point -> Point -> Bool
<= :: Point -> Point -> Bool
$c<= :: Point -> Point -> Bool
< :: Point -> Point -> Bool
$c< :: Point -> Point -> Bool
compare :: Point -> Point -> Ordering
$ccompare :: Point -> Point -> Ordering
Ord, Int -> Point -> String -> String
[Point] -> String -> String
Point -> String
(Int -> Point -> String -> String)
-> (Point -> String) -> ([Point] -> String -> String) -> Show Point
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Point] -> String -> String
$cshowList :: [Point] -> String -> String
show :: Point -> String
$cshow :: Point -> String
showsPrec :: Int -> Point -> String -> String
$cshowsPrec :: Int -> Point -> String -> String
Show)

instance IsString Point where
  fromString :: String -> Point
fromString = Var -> Point
PointVar (Var -> Point) -> (String -> Var) -> String -> Point
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Var
forall a. IsString a => String -> a
fromString

-- | A cube context consists of point variables with corresponding cubes.
type CubeContext = [(Var, Cube)]

-- * Pretty-printing

-- | Pretty-print a 'CubeContext'.
ppCubeContext :: CubeContext -> String
ppCubeContext :: CubeContext -> String
ppCubeContext [] = String
"⋅"
ppCubeContext CubeContext
xs = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (((Var, Cube) -> String) -> CubeContext -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var String
x, Cube
c) -> String
x String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" : " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Cube -> String
ppCube Cube
c) CubeContext
xs)

-- | Pretty-print a 'Cube'.
ppCube :: Cube -> String
ppCube :: Cube -> String
ppCube = Int -> Cube -> String
ppCubePrec Int
0

-- | Pretty-print a 'Cube' expression in a given precedence environment.
ppCubePrec :: Int -> Cube -> String
ppCubePrec :: Int -> Cube -> String
ppCubePrec Int
prec = \case
  CubeVar (Var String
x)   -> String
x
  CubeCon (Label String
l) -> String
l
  Cube
CubeUnit          -> String
"𝟙"
  CubeProduct Cube
l Cube
r   -> (Int -> Cube -> String) -> Int -> Cube -> String -> Cube -> String
forall {a} {t}.
(Semigroup a, IsString a) =>
(Int -> t -> a) -> Int -> t -> a -> t -> a
binOp Int -> Cube -> String
ppCubePrec (Int
prec Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Cube
l String
"×" Cube
r
  where
    parens :: a -> a
parens a
s = a
"(" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
s a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
")"
    binOp :: (Int -> t -> a) -> Int -> t -> a -> t -> a
binOp Int -> t -> a
pp Int
opPrec t
l a
op t
r = (if Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
opPrec then a -> a
forall {a}. (Semigroup a, IsString a) => a -> a
parens else a -> a
forall a. a -> a
id) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$
      Int -> t -> a
pp Int
opPrec t
l a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
op a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Int -> t -> a
pp Int
opPrec t
r

-- | Pretty-print a 'Point'.
ppPoint :: Point -> String
ppPoint :: Point -> String
ppPoint = Int -> Point -> String
ppPointPrec Int
0

-- | Pretty-print a 'Point' expression in a given precedence environment.
ppPointPrec :: Int -> Point -> String
ppPointPrec :: Int -> Point -> String
ppPointPrec Int
prec = \case
  PointVar (Var String
x)     -> String
x
  Point
PointUnit     -> String
"⋆"
  PointPair Point
l Point
r -> String
"⟨" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> Point -> String
ppPointPrec Int
prec Point
l String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
", " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> Point -> String
ppPointPrec Int
prec Point
r String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"⟩"
  PointFirst Point
p  -> String
"𝜋₁(" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> Point -> String
ppPointPrec Int
0 Point
p String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")"
  PointSecond Point
p -> String
"𝜋₂(" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> Point -> String
ppPointPrec Int
0 Point
p String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")"
  PointCon (Label String
l) []  -> String
l
  PointCon (Label String
l) [Point]
args  -> String
l String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"(" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Point -> String) -> [Point] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Point -> String
ppPointPrec Int
prec) [Point]
args) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")"