{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE RecordWildCards            #-}
module RSTT.Tope where

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

import           RSTT.Cube

-- | A tope expression.
data Tope
  = TopeTop               -- ^ Top tope: \(\top\).
  | TopeBottom            -- ^ Bottom tope: \(\bot\).
  | TopeAnd Tope Tope     -- ^ AND tope: \(\phi \land \psi\).
  | TopeOr  Tope Tope     -- ^ OR tope: \(\phi \lor \psi\).
  | TopeEQ  Point Point   -- ^ Point equality tope: \(t \equiv s\).
  | TopeVar Var           -- ^ A tope variable.
  | TopeImplies Tope Tope -- ^ IMPLIES tope: \(\phi \Rightarrow \psi\).
                          -- NOTE: this tope is added to internalise known tope judgements and simplify proof search.
  | TopeCon Label [Point] -- ^ User-defined tope constructor (fully applied to some points).
  deriving (Tope -> Tope -> Bool
(Tope -> Tope -> Bool) -> (Tope -> Tope -> Bool) -> Eq Tope
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Tope -> Tope -> Bool
$c/= :: Tope -> Tope -> Bool
== :: Tope -> Tope -> Bool
$c== :: Tope -> Tope -> Bool
Eq, Eq Tope
Eq Tope
-> (Tope -> Tope -> Ordering)
-> (Tope -> Tope -> Bool)
-> (Tope -> Tope -> Bool)
-> (Tope -> Tope -> Bool)
-> (Tope -> Tope -> Bool)
-> (Tope -> Tope -> Tope)
-> (Tope -> Tope -> Tope)
-> Ord Tope
Tope -> Tope -> Bool
Tope -> Tope -> Ordering
Tope -> Tope -> Tope
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 :: Tope -> Tope -> Tope
$cmin :: Tope -> Tope -> Tope
max :: Tope -> Tope -> Tope
$cmax :: Tope -> Tope -> Tope
>= :: Tope -> Tope -> Bool
$c>= :: Tope -> Tope -> Bool
> :: Tope -> Tope -> Bool
$c> :: Tope -> Tope -> Bool
<= :: Tope -> Tope -> Bool
$c<= :: Tope -> Tope -> Bool
< :: Tope -> Tope -> Bool
$c< :: Tope -> Tope -> Bool
compare :: Tope -> Tope -> Ordering
$ccompare :: Tope -> Tope -> Ordering
Ord, Int -> Tope -> ShowS
[Tope] -> ShowS
Tope -> String
(Int -> Tope -> ShowS)
-> (Tope -> String) -> ([Tope] -> ShowS) -> Show Tope
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Tope] -> ShowS
$cshowList :: [Tope] -> ShowS
show :: Tope -> String
$cshow :: Tope -> String
showsPrec :: Int -> Tope -> ShowS
$cshowsPrec :: Int -> Tope -> ShowS
Show)

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

-- | A shape is a tope in a cube context (with just one cube point variable):
-- \(\{t : I \mid \phi \}\).
data Shape = Shape
  { Shape -> (Var, Cube)
shapePoint :: (Var, Cube)
  , Shape -> Tope
shapeTope  :: Tope
  } deriving (Shape -> Shape -> Bool
(Shape -> Shape -> Bool) -> (Shape -> Shape -> Bool) -> Eq Shape
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Shape -> Shape -> Bool
$c/= :: Shape -> Shape -> Bool
== :: Shape -> Shape -> Bool
$c== :: Shape -> Shape -> Bool
Eq, Int -> Shape -> ShowS
[Shape] -> ShowS
Shape -> String
(Int -> Shape -> ShowS)
-> (Shape -> String) -> ([Shape] -> ShowS) -> Show Shape
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Shape] -> ShowS
$cshowList :: [Shape] -> ShowS
show :: Shape -> String
$cshow :: Shape -> String
showsPrec :: Int -> Shape -> ShowS
$cshowsPrec :: Int -> Shape -> ShowS
Show)

-- | A tope context consists of a set of topes.
type TopeContext = [Tope]

-- * Pretty-printing

-- | Pretty-print a 'TopeContext'.
ppTopeContext :: TopeContext -> String
ppTopeContext :: [Tope] -> String
ppTopeContext [] = String
"⋅"
ppTopeContext [Tope]
xs = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((Tope -> String) -> [Tope] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Tope -> String
ppTope [Tope]
xs)

-- | Pretty-print a 'Shape'.
ppShape :: Shape -> String
ppShape :: Shape -> String
ppShape Shape{(Var, Cube)
Tope
shapeTope :: Tope
shapePoint :: (Var, Cube)
shapeTope :: Shape -> Tope
shapePoint :: Shape -> (Var, Cube)
..} = String
"{" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
t String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" : " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Cube -> String
ppCube Cube
cube String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" | " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Tope -> String
ppTope Tope
shapeTope String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"}"
  where
    (Var String
t, Cube
cube) = (Var, Cube)
shapePoint

-- | Pretty-print a 'Tope'.
ppTope :: Tope -> String
ppTope :: Tope -> String
ppTope = Int -> Tope -> String
ppTopePrec Int
0

-- | Pretty-print a 'Tope' expression in a given precedence environment.
ppTopePrec :: Int -> Tope -> String
ppTopePrec :: Int -> Tope -> String
ppTopePrec Int
prec = \case
  Tope
TopeTop         -> String
"⊤"
  Tope
TopeBottom      -> String
"⊥"
  TopeVar (Var String
x) -> String
x
  TopeImplies Tope
l Tope
r -> (Int -> Tope -> String) -> Int -> Tope -> String -> Tope -> String
forall {a} {t}.
(Semigroup a, IsString a) =>
(Int -> t -> a) -> Int -> t -> a -> t -> a
binOp Int -> Tope -> String
ppTopePrec   Int
1 Tope
l String
"⇒" Tope
r
  TopeOr      Tope
l Tope
r -> (Int -> Tope -> String) -> Int -> Tope -> String -> Tope -> String
forall {a} {t}.
(Semigroup a, IsString a) =>
(Int -> t -> a) -> Int -> t -> a -> t -> a
binOp Int -> Tope -> String
ppTopePrec   Int
2 Tope
l String
"∨" Tope
r
  TopeAnd     Tope
l Tope
r -> (Int -> Tope -> String) -> Int -> Tope -> String -> Tope -> String
forall {a} {t}.
(Semigroup a, IsString a) =>
(Int -> t -> a) -> Int -> t -> a -> t -> a
binOp Int -> Tope -> String
ppTopePrec   Int
3 Tope
l String
"∧" Tope
r
  TopeEQ      Point
l Point
r -> (Int -> Point -> String)
-> Int -> Point -> String -> Point -> String
forall {a} {t}.
(Semigroup a, IsString a) =>
(Int -> t -> a) -> Int -> t -> a -> t -> a
binOp Int -> Point -> String
ppPointPrec  Int
4 Point
l String
"≡" Point
r
  TopeCon (Label String
l) [] -> String
l
  TopeCon (Label String
l) [Point]
args -> String
l String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(" String -> ShowS
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
0) [Point]
args) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  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

-- | Replace a point subterm everywhere in a tope term.
replacePointInTope :: Point -> Point -> Tope -> Tope
replacePointInTope :: Point -> Point -> Tope -> Tope
replacePointInTope Point
old Point
new = Tope -> Tope
go
  where
    go :: Tope -> Tope
go = \case
      Tope
TopeTop          -> Tope
TopeTop
      Tope
TopeBottom       -> Tope
TopeBottom
      TopeAnd Tope
l Tope
r      -> Tope -> Tope -> Tope
TopeAnd (Tope -> Tope
go Tope
l) (Tope -> Tope
go Tope
r)
      TopeOr Tope
l Tope
r       -> Tope -> Tope -> Tope
TopeOr (Tope -> Tope
go Tope
l) (Tope -> Tope
go Tope
r)
      TopeImplies Tope
l Tope
r  -> Tope -> Tope -> Tope
TopeImplies (Tope -> Tope
go Tope
l) (Tope -> Tope
go Tope
r)
      TopeEQ Point
t Point
s       -> Point -> Point -> Tope
TopeEQ (Point -> Point
go' Point
t) (Point -> Point
go' Point
s)
      TopeVar Var
phi      -> Var -> Tope
TopeVar Var
phi
      TopeCon Label
con [Point]
args -> Label -> [Point] -> Tope
TopeCon Label
con (Point -> Point
go' (Point -> Point) -> [Point] -> [Point]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Point]
args)

    go' :: Point -> Point
go' = Point -> Point -> Point -> Point
replacePoint Point
old Point
new

-- | Replace a point subterm everywhere in a point term.
replacePoint :: Point -> Point -> Point -> Point
replacePoint :: Point -> Point -> Point -> Point
replacePoint Point
old Point
new = Point -> Point
go
  where
    go :: Point -> Point
go = \case
      Point
p | Point
p Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
== Point
old      -> Point
new
      Point
PointUnit         -> Point
PointUnit
      PointPair Point
t Point
s     -> Point -> Point -> Point
PointPair (Point -> Point
go Point
t) (Point -> Point
go Point
s)
      PointFirst Point
t      -> Point -> Point
PointFirst (Point -> Point
go Point
t)
      PointSecond Point
t     -> Point -> Point
PointSecond (Point -> Point
go Point
t)
      PointCon Label
con [Point]
args -> Label -> [Point] -> Point
PointCon Label
con (Point -> Point
go (Point -> Point) -> [Point] -> [Point]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Point]
args)
      PointVar Var
var      -> Var -> Point
PointVar Var
var

-- | Check whether a point term is a subterm of another point term.
subPointOf :: Point -> Point -> Bool
subPointOf :: Point -> Point -> Bool
subPointOf Point
p = Point -> Bool
go
  where
    go :: Point -> Bool
go = \case
      Point
p' | Point
p Point -> Point -> Bool
forall a. Eq a => a -> a -> Bool
== Point
p'       -> Bool
True
      PointPair Point
t Point
s      -> (Point -> Bool) -> [Point] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Point -> Bool
go [Point
t, Point
s]
      PointFirst Point
t       -> Point -> Bool
go Point
t
      PointSecond Point
t      -> Point -> Bool
go Point
t
      PointCon Label
_con [Point]
args -> (Point -> Bool) -> [Point] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Point -> Bool
go [Point]
args
      Point
_                  -> Bool
False