{-# LANGUAGE Safe #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-}
module Cryptol.TypeCheck.Parseable
( module Cryptol.TypeCheck.Parseable
, ShowParseable(..)
) where
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Ident (Ident,unpackIdent)
import Cryptol.Parser.AST ( Located(..))
import Cryptol.ModuleSystem.Name
import Text.PrettyPrint hiding ((<>))
import qualified Text.PrettyPrint as PP ((<>))
class ShowParseable t where
showParseable :: t -> Doc
instance ShowParseable Expr where
showParseable :: Expr -> Doc
showParseable (EList es :: [Expr]
es _) = Doc -> Doc
parens (String -> Doc
text "EList" Doc -> Doc -> Doc
<+> [Expr] -> Doc
forall t. ShowParseable t => t -> Doc
showParseable [Expr]
es)
showParseable (ETuple es :: [Expr]
es) = Doc -> Doc
parens (String -> Doc
text "ETuple" Doc -> Doc -> Doc
<+> [Expr] -> Doc
forall t. ShowParseable t => t -> Doc
showParseable [Expr]
es)
showParseable (ERec ides :: [(Ident, Expr)]
ides) = Doc -> Doc
parens (String -> Doc
text "ERec" Doc -> Doc -> Doc
<+> [(Ident, Expr)] -> Doc
forall t. ShowParseable t => t -> Doc
showParseable [(Ident, Expr)]
ides)
showParseable (ESel e :: Expr
e s :: Selector
s) = Doc -> Doc
parens (String -> Doc
text "ESel" Doc -> Doc -> Doc
<+> Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
e Doc -> Doc -> Doc
<+> Selector -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Selector
s)
showParseable (ESet e :: Expr
e s :: Selector
s v :: Expr
v) = Doc -> Doc
parens (String -> Doc
text "ESet" Doc -> Doc -> Doc
<+>
Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
e Doc -> Doc -> Doc
<+> Selector -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Selector
s
Doc -> Doc -> Doc
<+> Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
v)
showParseable (EIf c :: Expr
c t :: Expr
t f :: Expr
f) = Doc -> Doc
parens (String -> Doc
text "EIf" Doc -> Doc -> Doc
<+> Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
c Doc -> Doc -> Doc
$$ Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
t Doc -> Doc -> Doc
$$ Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
f)
showParseable (EComp _ _ e :: Expr
e mss :: [[Match]]
mss) = Doc -> Doc
parens (String -> Doc
text "EComp" Doc -> Doc -> Doc
$$ Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
e Doc -> Doc -> Doc
$$ [[Match]] -> Doc
forall t. ShowParseable t => t -> Doc
showParseable [[Match]]
mss)
showParseable (EVar n :: Name
n) = Doc -> Doc
parens (String -> Doc
text "EVar" Doc -> Doc -> Doc
<+> Name -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Name
n)
showParseable (EApp fe :: Expr
fe ae :: Expr
ae) = Doc -> Doc
parens (String -> Doc
text "EApp" Doc -> Doc -> Doc
$$ Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
fe Doc -> Doc -> Doc
$$ Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
ae)
showParseable (EAbs n :: Name
n _ e :: Expr
e) = Doc -> Doc
parens (String -> Doc
text "EAbs" Doc -> Doc -> Doc
<+> Name -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Name
n Doc -> Doc -> Doc
$$ Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
e)
showParseable (EWhere e :: Expr
e dclg :: [DeclGroup]
dclg) = Doc -> Doc
parens (String -> Doc
text "EWhere" Doc -> Doc -> Doc
$$ Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
e Doc -> Doc -> Doc
$$ [DeclGroup] -> Doc
forall t. ShowParseable t => t -> Doc
showParseable [DeclGroup]
dclg)
showParseable (ETAbs tp :: TParam
tp e :: Expr
e) = Doc -> Doc
parens (String -> Doc
text "ETAbs" Doc -> Doc -> Doc
<+> TParam -> Doc
forall t. ShowParseable t => t -> Doc
showParseable TParam
tp
Doc -> Doc -> Doc
$$ Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
e)
showParseable (ETApp e :: Expr
e t :: Type
t) = Doc -> Doc
parens (String -> Doc
text "ETApp" Doc -> Doc -> Doc
$$ Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
e Doc -> Doc -> Doc
$$ Doc -> Doc
parens (String -> Doc
text "ETyp" Doc -> Doc -> Doc
<+> Type -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Type
t))
showParseable (EProofAbs _ e :: Expr
e) = Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
e
showParseable (EProofApp e :: Expr
e) = Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
e
instance (ShowParseable a, ShowParseable b) => ShowParseable (a,b) where
showParseable :: (a, b) -> Doc
showParseable (x :: a
x,y :: b
y) = Doc -> Doc
parens (a -> Doc
forall t. ShowParseable t => t -> Doc
showParseable a
x Doc -> Doc -> Doc
PP.<> Doc
comma Doc -> Doc -> Doc
PP.<> b -> Doc
forall t. ShowParseable t => t -> Doc
showParseable b
y)
instance ShowParseable Int where
showParseable :: Int -> Doc
showParseable i :: Int
i = Int -> Doc
int Int
i
instance ShowParseable Ident where
showParseable :: Ident -> Doc
showParseable i :: Ident
i = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. Show a => a -> String
show (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Ident -> String
unpackIdent Ident
i
instance ShowParseable Type where
showParseable :: Type -> Doc
showParseable (TUser n :: Name
n lt :: [Type]
lt t :: Type
t) = Doc -> Doc
parens (String -> Doc
text "TUser" Doc -> Doc -> Doc
<+> Name -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Name
n Doc -> Doc -> Doc
<+> [Type] -> Doc
forall t. ShowParseable t => t -> Doc
showParseable [Type]
lt Doc -> Doc -> Doc
<+> Type -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Type
t)
showParseable (TRec lidt :: [(Ident, Type)]
lidt) = Doc -> Doc
parens (String -> Doc
text "TRec" Doc -> Doc -> Doc
<+> [(Ident, Type)] -> Doc
forall t. ShowParseable t => t -> Doc
showParseable [(Ident, Type)]
lidt)
showParseable t :: Type
t = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Type -> String
forall a. Show a => a -> String
show Type
t
instance ShowParseable Selector where
showParseable :: Selector -> Doc
showParseable (TupleSel n :: Int
n _) = Doc -> Doc
parens (String -> Doc
text "TupleSel" Doc -> Doc -> Doc
<+> Int -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Int
n)
showParseable (RecordSel n :: Ident
n _) = Doc -> Doc
parens (String -> Doc
text "RecordSel" Doc -> Doc -> Doc
<+> Ident -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Ident
n)
showParseable (ListSel n :: Int
n _) = Doc -> Doc
parens (String -> Doc
text "ListSel" Doc -> Doc -> Doc
<+> Int -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Int
n)
instance ShowParseable Match where
showParseable :: Match -> Doc
showParseable (From n :: Name
n _ _ e :: Expr
e) = Doc -> Doc
parens (String -> Doc
text "From" Doc -> Doc -> Doc
<+> Name -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Name
n Doc -> Doc -> Doc
<+> Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
e)
showParseable (Let d :: Decl
d) = Doc -> Doc
parens (String -> Doc
text "MLet" Doc -> Doc -> Doc
<+> Decl -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Decl
d)
instance ShowParseable Decl where
showParseable :: Decl -> Doc
showParseable d :: Decl
d = Doc -> Doc
parens (String -> Doc
text "Decl" Doc -> Doc -> Doc
<+> Name -> Doc
forall t. ShowParseable t => t -> Doc
showParseable (Decl -> Name
dName Decl
d)
Doc -> Doc -> Doc
$$ DeclDef -> Doc
forall t. ShowParseable t => t -> Doc
showParseable (Decl -> DeclDef
dDefinition Decl
d))
instance ShowParseable DeclDef where
showParseable :: DeclDef -> Doc
showParseable DPrim = String -> Doc
text (DeclDef -> String
forall a. Show a => a -> String
show DeclDef
DPrim)
showParseable (DExpr e :: Expr
e) = Doc -> Doc
parens (String -> Doc
text "DExpr" Doc -> Doc -> Doc
$$ Expr -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Expr
e)
instance ShowParseable DeclGroup where
showParseable :: DeclGroup -> Doc
showParseable (Recursive ds :: [Decl]
ds) =
Doc -> Doc
parens (String -> Doc
text "Recursive" Doc -> Doc -> Doc
$$ [Decl] -> Doc
forall t. ShowParseable t => t -> Doc
showParseable [Decl]
ds)
showParseable (NonRecursive d :: Decl
d) =
Doc -> Doc
parens (String -> Doc
text "NonRecursive" Doc -> Doc -> Doc
$$ Decl -> Doc
forall t. ShowParseable t => t -> Doc
showParseable Decl
d)
instance (ShowParseable a) => ShowParseable [a] where
showParseable :: [a] -> Doc
showParseable a :: [a]
a = case [a]
a of
[] -> String -> Doc
text "[]"
[x :: a
x] -> Doc -> Doc
brackets (a -> Doc
forall t. ShowParseable t => t -> Doc
showParseable a
x)
x :: a
x : xs :: [a]
xs -> String -> Doc
text "[" Doc -> Doc -> Doc
<+> a -> Doc
forall t. ShowParseable t => t -> Doc
showParseable a
x Doc -> Doc -> Doc
$$
[Doc] -> Doc
vcat [ Doc
comma Doc -> Doc -> Doc
<+> a -> Doc
forall t. ShowParseable t => t -> Doc
showParseable a
y | a
y <- [a]
xs ] Doc -> Doc -> Doc
$$
String -> Doc
text "]"
instance (ShowParseable a) => ShowParseable (Maybe a) where
showParseable :: Maybe a -> Doc
showParseable Nothing = String -> Doc
text "(0,\"\")"
showParseable (Just x :: a
x) = a -> Doc
forall t. ShowParseable t => t -> Doc
showParseable a
x
instance (ShowParseable a) => ShowParseable (Located a) where
showParseable :: Located a -> Doc
showParseable l :: Located a
l = a -> Doc
forall t. ShowParseable t => t -> Doc
showParseable (Located a -> a
forall a. Located a -> a
thing Located a
l)
instance ShowParseable TParam where
showParseable :: TParam -> Doc
showParseable tp :: TParam
tp = Doc -> Doc
parens (String -> Doc
text (Int -> String
forall a. Show a => a -> String
show (TParam -> Int
tpUnique TParam
tp)) Doc -> Doc -> Doc
PP.<> Doc
comma Doc -> Doc -> Doc
PP.<> Maybe Name -> Doc
maybeNameDoc (TParam -> Maybe Name
tpName TParam
tp))
maybeNameDoc :: Maybe Name -> Doc
maybeNameDoc :: Maybe Name -> Doc
maybeNameDoc Nothing = Doc -> Doc
doubleQuotes Doc
empty
maybeNameDoc (Just n :: Name
n) = Ident -> Doc
forall t. ShowParseable t => t -> Doc
showParseable (Name -> Ident
nameIdent Name
n)
instance ShowParseable Name where
showParseable :: Name -> Doc
showParseable n :: Name
n = Doc -> Doc
parens (String -> Doc
text (Int -> String
forall a. Show a => a -> String
show (Name -> Int
nameUnique Name
n)) Doc -> Doc -> Doc
PP.<> Doc
comma Doc -> Doc -> Doc
PP.<> Ident -> Doc
forall t. ShowParseable t => t -> Doc
showParseable (Name -> Ident
nameIdent Name
n))