module PGF.Type ( Type(..), Hypo, CId,
                  readType, showType,
                  mkType, mkHypo, mkDepHypo, mkImplHypo,
                  unType,
                  pType, ppType, ppHypo ) where

import PGF.CId
import {-# SOURCE #-} PGF.Expr
import Data.Char
import Data.List
import qualified Text.PrettyPrint as PP
import qualified Text.ParserCombinators.ReadP as RP
--import Control.Monad


-- | To read a type from a 'String', use 'readType'.

data Type =
   DTyp [Hypo] CId [Expr]
  deriving (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq,Eq Type
Eq Type
-> (Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
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 :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmax :: Type -> Type -> Type
>= :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c< :: Type -> Type -> Bool
compare :: Type -> Type -> Ordering
$ccompare :: Type -> Type -> Ordering
$cp1Ord :: Eq Type
Ord,Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show)

-- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis

type Hypo = (BindType,CId,Type)

-- | Reads a 'Type' from a 'String'.

readType :: String -> Maybe Type
readType :: String -> Maybe Type
readType String
s = case [Type
x | (Type
x,String
cs) <- ReadP Type -> ReadS Type
forall a. ReadP a -> ReadS a
RP.readP_to_S ReadP Type
pType String
s, (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
cs] of
               [Type
x] -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
x
               [Type]
_   -> Maybe Type
forall a. Maybe a
Nothing

-- | renders type as 'String'. The list

-- of identifiers is the list of all free variables

-- in the expression in order reverse to the order

-- of binding.

showType :: [CId] -> Type -> String
showType :: [CId] -> Type -> String
showType [CId]
vars = Doc -> String
PP.render (Doc -> String) -> (Type -> Doc) -> Type -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [CId] -> Type -> Doc
ppType Int
0 [CId]
vars

-- | creates a type from list of hypothesises, category and 

-- list of arguments for the category. The operation 

-- @mkType [h_1,...,h_n] C [e_1,...,e_m]@ will create 

-- @h_1 -> ... -> h_n -> C e_1 ... e_m@

mkType :: [Hypo] -> CId -> [Expr] -> Type
mkType :: [Hypo] -> CId -> [Expr] -> Type
mkType [Hypo]
hyps CId
cat [Expr]
args = [Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hyps CId
cat [Expr]
args

-- | creates hypothesis for non-dependent type i.e. A

mkHypo :: Type -> Hypo
mkHypo :: Type -> Hypo
mkHypo Type
ty = (BindType
Explicit,CId
wildCId,Type
ty)

-- | creates hypothesis for dependent type i.e. (x : A)

mkDepHypo :: CId -> Type -> Hypo
mkDepHypo :: CId -> Type -> Hypo
mkDepHypo CId
x Type
ty = (BindType
Explicit,CId
x,Type
ty)

-- | creates hypothesis for dependent type with implicit argument i.e. ({x} : A)

mkImplHypo :: CId -> Type -> Hypo
mkImplHypo :: CId -> Type -> Hypo
mkImplHypo CId
x Type
ty = (BindType
Implicit,CId
x,Type
ty)

unType :: Type -> ([Hypo], CId, [Expr])
unType :: Type -> ([Hypo], CId, [Expr])
unType (DTyp [Hypo]
hyps CId
cat [Expr]
es) = ([Hypo]
hyps, CId
cat, [Expr]
es)

pType :: RP.ReadP Type
pType :: ReadP Type
pType = do
  ReadP ()
RP.skipSpaces
  [[Hypo]]
hyps <- ReadP [Hypo] -> ReadP () -> ReadP [[Hypo]]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
RP.sepBy (ReadP [Hypo]
pHypo ReadP [Hypo] -> ([Hypo] -> ReadP [Hypo]) -> ReadP [Hypo]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \[Hypo]
h -> ReadP ()
RP.skipSpaces ReadP () -> ReadP String -> ReadP String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> ReadP String
RP.string String
"->" ReadP String -> ReadP [Hypo] -> ReadP [Hypo]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Hypo] -> ReadP [Hypo]
forall (m :: * -> *) a. Monad m => a -> m a
return [Hypo]
h) ReadP ()
RP.skipSpaces
  ReadP ()
RP.skipSpaces
  (CId
cat,[Expr]
args) <- ReadP (CId, [Expr])
pAtom
  Type -> ReadP Type
forall (m :: * -> *) a. Monad m => a -> m a
return ([Hypo] -> CId -> [Expr] -> Type
DTyp ([[Hypo]] -> [Hypo]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Hypo]]
hyps) CId
cat [Expr]
args)
  where
    pHypo :: ReadP [Hypo]
pHypo =
      do (CId
cat,[Expr]
args) <- ReadP (CId, [Expr])
pAtom
         [Hypo] -> ReadP [Hypo]
forall (m :: * -> *) a. Monad m => a -> m a
return [(BindType
Explicit,CId
wildCId,[Hypo] -> CId -> [Expr] -> Type
DTyp [] CId
cat [Expr]
args)]
      ReadP [Hypo] -> ReadP [Hypo] -> ReadP [Hypo]
forall a. ReadP a -> ReadP a -> ReadP a
RP.<++
      do ReadP Char -> ReadP Char -> ReadP [Hypo] -> ReadP [Hypo]
forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
RP.between (Char -> ReadP Char
RP.char Char
'(') (Char -> ReadP Char
RP.char Char
')') ReadP [Hypo]
pHypoBinds

pHypoBinds :: ReadP [Hypo]
pHypoBinds = do
   [(BindType, CId)]
xs <- [(BindType, CId)]
-> ReadP [(BindType, CId)] -> ReadP [(BindType, CId)]
forall a. a -> ReadP a -> ReadP a
RP.option [(BindType
Explicit,CId
wildCId)] (ReadP [(BindType, CId)] -> ReadP [(BindType, CId)])
-> ReadP [(BindType, CId)] -> ReadP [(BindType, CId)]
forall a b. (a -> b) -> a -> b
$ do
               [(BindType, CId)]
xs <- ReadP [(BindType, CId)]
pBinds
               ReadP ()
RP.skipSpaces
               Char -> ReadP Char
RP.char Char
':'
               [(BindType, CId)] -> ReadP [(BindType, CId)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(BindType, CId)]
xs
   Type
ty <- ReadP Type
pType
   [Hypo] -> ReadP [Hypo]
forall (m :: * -> *) a. Monad m => a -> m a
return [(BindType
b,CId
v,Type
ty) | (BindType
b,CId
v) <- [(BindType, CId)]
xs]

pAtom :: ReadP (CId, [Expr])
pAtom = do
   CId
cat <- ReadP CId
pCId
   ReadP ()
RP.skipSpaces
   [Expr]
args <- ReadP Expr -> ReadP () -> ReadP [Expr]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
RP.sepBy ReadP Expr
pArg ReadP ()
RP.skipSpaces
   (CId, [Expr]) -> ReadP (CId, [Expr])
forall (m :: * -> *) a. Monad m => a -> m a
return (CId
cat, [Expr]
args)

ppType :: Int -> [CId] -> Type -> PP.Doc
ppType :: Int -> [CId] -> Type -> Doc
ppType Int
d [CId]
scope (DTyp [Hypo]
hyps CId
cat [Expr]
args)
  | [Hypo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Hypo]
hyps = [CId] -> CId -> [Expr] -> Doc
ppRes [CId]
scope CId
cat [Expr]
args
  | Bool
otherwise = let ([CId]
scope',[Doc]
hdocs) = ([CId] -> Hypo -> ([CId], Doc))
-> [CId] -> [Hypo] -> ([CId], [Doc])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumL (Int -> [CId] -> Hypo -> ([CId], Doc)
ppHypo Int
1) [CId]
scope [Hypo]
hyps
                in Bool -> Doc -> Doc
ppParens (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) ((Doc -> Doc -> Doc) -> Doc -> [Doc] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Doc
hdoc Doc
doc -> Doc
hdoc Doc -> Doc -> Doc
PP.<+> String -> Doc
PP.text String
"->" Doc -> Doc -> Doc
PP.<+> Doc
doc) ([CId] -> CId -> [Expr] -> Doc
ppRes [CId]
scope' CId
cat [Expr]
args) [Doc]
hdocs)
  where
    ppRes :: [CId] -> CId -> [Expr] -> Doc
ppRes [CId]
scope CId
cat [Expr]
es
      | [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
es   = CId -> Doc
ppCId CId
cat
      | Bool
otherwise = Bool -> Doc -> Doc
ppParens (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (CId -> Doc
ppCId CId
cat Doc -> Doc -> Doc
PP.<+> [Doc] -> Doc
PP.hsep ((Expr -> Doc) -> [Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> [CId] -> Expr -> Doc
ppExpr Int
4 [CId]
scope) [Expr]
es))

ppHypo :: Int -> [CId] -> (BindType,CId,Type) -> ([CId],PP.Doc)
ppHypo :: Int -> [CId] -> Hypo -> ([CId], Doc)
ppHypo Int
d [CId]
scope (BindType
Explicit,CId
x,Type
typ) = if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
                                    then ([CId]
scope,Int -> [CId] -> Type -> Doc
ppType Int
d [CId]
scope Type
typ)
                                    else let y :: CId
y = CId -> [CId] -> CId
freshName CId
x [CId]
scope
                                         in (CId
yCId -> [CId] -> [CId]
forall a. a -> [a] -> [a]
:[CId]
scope,Doc -> Doc
PP.parens (CId -> Doc
ppCId CId
y Doc -> Doc -> Doc
PP.<+> Char -> Doc
PP.char Char
':' Doc -> Doc -> Doc
PP.<+> Int -> [CId] -> Type -> Doc
ppType Int
0 [CId]
scope Type
typ))
ppHypo Int
d [CId]
scope (BindType
Implicit,CId
x,Type
typ) = if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
                                    then ([CId]
scope,Doc -> Doc
PP.parens (Doc -> Doc
PP.braces (CId -> Doc
ppCId CId
x) Doc -> Doc -> Doc
PP.<+> Char -> Doc
PP.char Char
':' Doc -> Doc -> Doc
PP.<+> Int -> [CId] -> Type -> Doc
ppType Int
0 [CId]
scope Type
typ))
                                    else let y :: CId
y = CId -> [CId] -> CId
freshName CId
x [CId]
scope
                                         in (CId
yCId -> [CId] -> [CId]
forall a. a -> [a] -> [a]
:[CId]
scope,Doc -> Doc
PP.parens (Doc -> Doc
PP.braces (CId -> Doc
ppCId CId
y) Doc -> Doc -> Doc
PP.<+> Char -> Doc
PP.char Char
':' Doc -> Doc -> Doc
PP.<+> Int -> [CId] -> Type -> Doc
ppType Int
0 [CId]
scope Type
typ))