module Language.Lambda.SystemF.Expression
( SystemFExpr(..),
TypedExpr(..),
Ty(..),
_expr,
_ty,
prettyPrint,
substituteTy,
upperLambda
) where
import Data.Monoid
import Prettyprinter
import Prettyprinter.Render.Text (renderStrict)
import RIO
data SystemFExpr name
= Let name (SystemFExpr name)
| Var name
| VarAnn name (Ty name)
| App (SystemFExpr name) (SystemFExpr name)
| Abs name (Ty name) (SystemFExpr name)
| TyAbs name (SystemFExpr name)
| TyApp (SystemFExpr name) (Ty name)
deriving (SystemFExpr name -> SystemFExpr name -> Bool
forall name.
Eq name =>
SystemFExpr name -> SystemFExpr name -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SystemFExpr name -> SystemFExpr name -> Bool
$c/= :: forall name.
Eq name =>
SystemFExpr name -> SystemFExpr name -> Bool
== :: SystemFExpr name -> SystemFExpr name -> Bool
$c== :: forall name.
Eq name =>
SystemFExpr name -> SystemFExpr name -> Bool
Eq, Int -> SystemFExpr name -> ShowS
forall name. Show name => Int -> SystemFExpr name -> ShowS
forall name. Show name => [SystemFExpr name] -> ShowS
forall name. Show name => SystemFExpr name -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SystemFExpr name] -> ShowS
$cshowList :: forall name. Show name => [SystemFExpr name] -> ShowS
show :: SystemFExpr name -> String
$cshow :: forall name. Show name => SystemFExpr name -> String
showsPrec :: Int -> SystemFExpr name -> ShowS
$cshowsPrec :: forall name. Show name => Int -> SystemFExpr name -> ShowS
Show)
data TypedExpr name = TypedExpr
{ forall name. TypedExpr name -> SystemFExpr name
teExpr :: SystemFExpr name,
forall name. TypedExpr name -> Ty name
teTy :: Ty name
} deriving (TypedExpr name -> TypedExpr name -> Bool
forall name. Eq name => TypedExpr name -> TypedExpr name -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TypedExpr name -> TypedExpr name -> Bool
$c/= :: forall name. Eq name => TypedExpr name -> TypedExpr name -> Bool
== :: TypedExpr name -> TypedExpr name -> Bool
$c== :: forall name. Eq name => TypedExpr name -> TypedExpr name -> Bool
Eq, Int -> TypedExpr name -> ShowS
forall name. Show name => Int -> TypedExpr name -> ShowS
forall name. Show name => [TypedExpr name] -> ShowS
forall name. Show name => TypedExpr name -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TypedExpr name] -> ShowS
$cshowList :: forall name. Show name => [TypedExpr name] -> ShowS
show :: TypedExpr name -> String
$cshow :: forall name. Show name => TypedExpr name -> String
showsPrec :: Int -> TypedExpr name -> ShowS
$cshowsPrec :: forall name. Show name => Int -> TypedExpr name -> ShowS
Show)
data Ty name
= TyVar name
| TyArrow (Ty name) (Ty name)
| TyForAll name (Ty name)
deriving (Int -> Ty name -> ShowS
forall name. Show name => Int -> Ty name -> ShowS
forall name. Show name => [Ty name] -> ShowS
forall name. Show name => Ty name -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ty name] -> ShowS
$cshowList :: forall name. Show name => [Ty name] -> ShowS
show :: Ty name -> String
$cshow :: forall name. Show name => Ty name -> String
showsPrec :: Int -> Ty name -> ShowS
$cshowsPrec :: forall name. Show name => Int -> Ty name -> ShowS
Show)
instance (Pretty name) => Pretty (SystemFExpr name) where
pretty :: forall ann. SystemFExpr name -> Doc ann
pretty (Var name
name) = forall a ann. Pretty a => a -> Doc ann
pretty name
name
pretty (VarAnn name
name Ty name
ty) = forall name a. Pretty name => name -> Ty name -> Doc a
prettyVarAnn name
name Ty name
ty
pretty (App SystemFExpr name
e1 SystemFExpr name
e2) = forall name a.
Pretty name =>
SystemFExpr name -> SystemFExpr name -> Doc a
prettyApp SystemFExpr name
e1 SystemFExpr name
e2
pretty (Abs name
name Ty name
ty SystemFExpr name
body) = forall name ann.
Pretty name =>
name -> Ty name -> SystemFExpr name -> Doc ann
prettyAbs name
name Ty name
ty SystemFExpr name
body
pretty (Let name
name SystemFExpr name
expr) = forall name ann. Pretty name => name -> SystemFExpr name -> Doc ann
prettyLet name
name SystemFExpr name
expr
pretty (TyAbs name
ty SystemFExpr name
body) = forall name ann. Pretty name => name -> SystemFExpr name -> Doc ann
prettyTyAbs name
ty SystemFExpr name
body
pretty (TyApp SystemFExpr name
expr Ty name
ty) = forall name ann.
Pretty name =>
SystemFExpr name -> Ty name -> Doc ann
prettyTyApp SystemFExpr name
expr Ty name
ty
instance Pretty name => Pretty (TypedExpr name) where
pretty :: forall ann. TypedExpr name -> Doc ann
pretty TypedExpr name
expr = forall a ann. Pretty a => a -> Doc ann
pretty (TypedExpr name
expr forall s a. s -> Getting a s a -> a
^. forall name. Lens' (TypedExpr name) (SystemFExpr name)
_expr) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
colon forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (TypedExpr name
expr forall s a. s -> Getting a s a -> a
^. forall name. Lens' (TypedExpr name) (Ty name)
_ty)
instance Pretty name => Pretty (Ty name) where
pretty :: forall ann. Ty name -> Doc ann
pretty = forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
False
instance Eq name => Eq (Ty name) where
== :: Ty name -> Ty name -> Bool
(==) = forall name. Eq name => Ty name -> Ty name -> Bool
isTyEquivalent
_expr :: Lens' (TypedExpr name) (SystemFExpr name)
_expr :: forall name. Lens' (TypedExpr name) (SystemFExpr name)
_expr = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall name. TypedExpr name -> SystemFExpr name
teExpr (\TypedExpr name
res SystemFExpr name
expr -> TypedExpr name
res { teExpr :: SystemFExpr name
teExpr = SystemFExpr name
expr })
_ty :: Lens' (TypedExpr name) (Ty name)
_ty :: forall name. Lens' (TypedExpr name) (Ty name)
_ty = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens forall name. TypedExpr name -> Ty name
teTy (\TypedExpr name
res Ty name
ty -> TypedExpr name
res { teTy :: Ty name
teTy = Ty name
ty })
prettyPrint :: Pretty pretty => pretty -> Text
prettyPrint :: forall pretty. Pretty pretty => pretty -> Text
prettyPrint pretty
expr = forall ann. SimpleDocStream ann -> Text
renderStrict SimpleDocStream Any
docStream
where docStream :: SimpleDocStream Any
docStream = forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty LayoutOptions
defaultLayoutOptions (forall a ann. Pretty a => a -> Doc ann
pretty pretty
expr)
substituteTy
:: Eq name
=> Ty name
-> name
-> Ty name
-> Ty name
substituteTy :: forall name. Eq name => Ty name -> name -> Ty name -> Ty name
substituteTy Ty name
ty name
forName Ty name
inTy
= case Ty name
inTy of
TyVar name
n
| name
n forall a. Eq a => a -> a -> Bool
== name
forName -> Ty name
ty
| Bool
otherwise -> Ty name
inTy
TyArrow Ty name
t1 Ty name
t2 -> forall name. Ty name -> Ty name -> Ty name
TyArrow (Ty name -> Ty name
sub Ty name
t1) (Ty name -> Ty name
sub Ty name
t2)
TyForAll name
n Ty name
ty'
| name
n forall a. Eq a => a -> a -> Bool
== name
forName -> Ty name
inTy
| Bool
otherwise -> forall name. name -> Ty name -> Ty name
TyForAll name
n (Ty name -> Ty name
sub Ty name
ty')
where sub :: Ty name -> Ty name
sub = forall name. Eq name => Ty name -> name -> Ty name -> Ty name
substituteTy Ty name
ty name
forName
upperLambda :: Char
upperLambda :: Char
upperLambda = Char
'Λ'
prettyVarAnn :: Pretty name => name -> Ty name -> Doc a
prettyVarAnn :: forall name a. Pretty name => name -> Ty name -> Doc a
prettyVarAnn name
var Ty name
ty = forall a ann. Pretty a => a -> Doc ann
pretty name
var forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon forall a. Semigroup a => a -> a -> a
<> Ty name -> Doc a
prettyTy' Ty name
ty
where prettyTy' :: Ty name -> Doc a
prettyTy' (TyVar name
_) = forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
True Ty name
ty
prettyTy' Ty name
_ = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
True Ty name
ty
prettyApp
:: Pretty name
=> SystemFExpr name
-> SystemFExpr name
-> Doc a
prettyApp :: forall name a.
Pretty name =>
SystemFExpr name -> SystemFExpr name -> Doc a
prettyApp e1 :: SystemFExpr name
e1@Abs{} e2 :: SystemFExpr name
e2@Abs{} = forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e1) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e2)
prettyApp e1 :: SystemFExpr name
e1@Abs{} SystemFExpr name
e2 = forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e1) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e2
prettyApp SystemFExpr name
e1 e2 :: SystemFExpr name
e2@Abs{} = forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e1 forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e2)
prettyApp SystemFExpr name
e1 e2 :: SystemFExpr name
e2@App{} = forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e1 forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
parens (forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e2)
prettyApp SystemFExpr name
e1 SystemFExpr name
e2 = forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e1 forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
e2
prettyAbs
:: Pretty name
=> name
-> Ty name
-> SystemFExpr name
-> Doc ann
prettyAbs :: forall name ann.
Pretty name =>
name -> Ty name -> SystemFExpr name -> Doc ann
prettyAbs name
name Ty name
ty SystemFExpr name
body
= forall ann. Doc ann
lambda
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
hsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall name ty ann.
(Pretty name, Pretty ty) =>
name -> Ty ty -> Doc ann
prettyArg) [(name, Ty name)]
names)
forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
dot
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
body'
where ([(name, Ty name)]
names, SystemFExpr name
body') = forall n.
n -> Ty n -> SystemFExpr n -> ([(n, Ty n)], SystemFExpr n)
uncurryAbs name
name Ty name
ty SystemFExpr name
body
prettyLet :: Pretty name => name -> SystemFExpr name -> Doc ann
prettyLet :: forall name ann. Pretty name => name -> SystemFExpr name -> Doc ann
prettyLet name
name SystemFExpr name
expr = Doc ann
"let" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty name
name forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
equals forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
expr
prettyTyAbs :: (Pretty name) => name -> SystemFExpr name -> Doc ann
prettyTyAbs :: forall name ann. Pretty name => name -> SystemFExpr name -> Doc ann
prettyTyAbs name
name SystemFExpr name
body = forall ann. Doc ann
upperLambda' forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. [Doc ann] -> Doc ann
hsep (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [name]
names) forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
dot
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
body'
where ([name]
names, SystemFExpr name
body') = forall n. n -> SystemFExpr n -> ([n], SystemFExpr n)
uncurryTyAbs name
name SystemFExpr name
body
prettyTyApp :: (Pretty name) => SystemFExpr name -> Ty name -> Doc ann
prettyTyApp :: forall name ann.
Pretty name =>
SystemFExpr name -> Ty name -> Doc ann
prettyTyApp SystemFExpr name
expr Ty name
ty = forall a ann. Pretty a => a -> Doc ann
pretty SystemFExpr name
expr forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
brackets (forall a ann. Pretty a => a -> Doc ann
pretty Ty name
ty)
prettyTy :: Pretty name => Bool -> Ty name -> Doc ann
prettyTy :: forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
_ (TyVar name
name) = forall a ann. Pretty a => a -> Doc ann
pretty name
name
prettyTy Bool
compact (TyArrow Ty name
t1 Ty name
t2) = forall name ann.
Pretty name =>
Bool -> Ty name -> Ty name -> Doc ann
prettyTyArrow Bool
compact Ty name
t1 Ty name
t2
prettyTy Bool
compact (TyForAll name
name Ty name
ty) = forall name ann. Pretty name => Bool -> name -> Ty name -> Doc ann
prettyTyForAll Bool
compact name
name Ty name
ty
isTyEquivalent :: Eq name => Ty name -> Ty name -> Bool
isTyEquivalent :: forall name. Eq name => Ty name -> Ty name -> Bool
isTyEquivalent Ty name
t1 Ty name
t2
| Ty name
t1 forall name. Eq name => Ty name -> Ty name -> Bool
`isTySame` Ty name
t2 = Bool
True
| Bool
otherwise = case (Ty name
t1, Ty name
t2) of
(TyForAll name
n1 Ty name
t1', TyForAll name
n2 Ty name
t2') -> (name
n1, Ty name
t1') forall name. Eq name => (name, Ty name) -> (name, Ty name) -> Bool
`areForAllsEquivalent` (name
n2, Ty name
t2')
(Ty name, Ty name)
_ -> Bool
False
prettyTyArrow :: Pretty name => Bool -> Ty name -> Ty name -> Doc ann
prettyTyArrow :: forall name ann.
Pretty name =>
Bool -> Ty name -> Ty name -> Doc ann
prettyTyArrow Bool
compact (TyArrow Ty name
t1 Ty name
t2) Ty name
t3
= forall ann. Bool -> Doc ann -> Doc ann -> Doc ann
prettyTyArrow' Bool
compact Doc ann
compositeTy forall a b. (a -> b) -> a -> b
$ forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
compact Ty name
t3
where compositeTy :: Doc ann
compositeTy = forall ann. Doc ann -> Doc ann
parens forall a b. (a -> b) -> a -> b
$ forall name ann.
Pretty name =>
Bool -> Ty name -> Ty name -> Doc ann
prettyTyArrow Bool
compact Ty name
t1 Ty name
t2
prettyTyArrow Bool
compact Ty name
t1 Ty name
t2
= forall ann. Bool -> Doc ann -> Doc ann -> Doc ann
prettyTyArrow' Bool
compact (forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
compact Ty name
t1) (forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
compact Ty name
t2)
prettyTyForAll :: Pretty name => Bool -> name -> Ty name -> Doc ann
prettyTyForAll :: forall name ann. Pretty name => Bool -> name -> Ty name -> Doc ann
prettyTyForAll Bool
compact name
name Ty name
ty
= Doc ann
"forall"
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty name
name forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
dot
forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall name ann. Pretty name => Bool -> Ty name -> Doc ann
prettyTy Bool
compact Ty name
ty
lambda :: Doc ann
lambda :: forall ann. Doc ann
lambda = forall a ann. Pretty a => a -> Doc ann
pretty Char
'λ'
prettyArg :: (Pretty name, Pretty ty) => name -> Ty ty -> Doc ann
prettyArg :: forall name ty ann.
(Pretty name, Pretty ty) =>
name -> Ty ty -> Doc ann
prettyArg name
name (TyArrow Ty ty
t1 Ty ty
t2)
= forall a ann. Pretty a => a -> Doc ann
pretty name
name forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
parens (forall name ann.
Pretty name =>
Bool -> Ty name -> Ty name -> Doc ann
prettyTyArrow Bool
True Ty ty
t1 Ty ty
t2)
prettyArg name
name Ty ty
ty = forall a ann. Pretty a => a -> Doc ann
pretty name
name forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Ty ty
ty
upperLambda' :: Doc ann
upperLambda' :: forall ann. Doc ann
upperLambda' = forall a ann. Pretty a => a -> Doc ann
pretty Char
upperLambda
isTySame :: Eq name => Ty name -> Ty name -> Bool
isTySame :: forall name. Eq name => Ty name -> Ty name -> Bool
isTySame (TyVar name
n1) (TyVar name
n2) = name
n1 forall a. Eq a => a -> a -> Bool
== name
n2
isTySame (TyArrow Ty name
t1 Ty name
t2) (TyArrow Ty name
t1' Ty name
t2') = Ty name
t1 forall a. Eq a => a -> a -> Bool
== Ty name
t1' Bool -> Bool -> Bool
&& Ty name
t2 forall a. Eq a => a -> a -> Bool
== Ty name
t2'
isTySame (TyForAll name
n1 Ty name
t1) (TyForAll name
n2 Ty name
t2) = name
n1 forall a. Eq a => a -> a -> Bool
== name
n2 Bool -> Bool -> Bool
&& Ty name
t1 forall a. Eq a => a -> a -> Bool
== Ty name
t2
isTySame Ty name
_ Ty name
_ = Bool
False
areForAllsEquivalent :: Eq name => (name, Ty name) -> (name, Ty name) -> Bool
areForAllsEquivalent :: forall name. Eq name => (name, Ty name) -> (name, Ty name) -> Bool
areForAllsEquivalent (name
n1, Ty name
t1) (name
n2, Ty name
t2) = Ty name
t1 forall a. Eq a => a -> a -> Bool
== forall name. Eq name => Ty name -> name -> Ty name -> Ty name
substituteTy (forall name. name -> Ty name
TyVar name
n1) name
n2 Ty name
t2
prettyTyArrow' :: Bool -> Doc ann -> Doc ann -> Doc ann
prettyTyArrow' :: forall ann. Bool -> Doc ann -> Doc ann -> Doc ann
prettyTyArrow' Bool
compact Doc ann
doc1 Doc ann
doc2 = Doc ann
doc1 Doc ann -> Doc ann -> Doc ann
`add'` Doc ann
"->" Doc ann -> Doc ann -> Doc ann
`add'` Doc ann
doc2
where add' :: Doc ann -> Doc ann -> Doc ann
add'
| Bool
compact = forall a. Semigroup a => a -> a -> a
(<>)
| Bool
otherwise = forall ann. Doc ann -> Doc ann -> Doc ann
(<+>)
uncurryAbs :: n -> Ty n -> SystemFExpr n -> ([(n, Ty n)], SystemFExpr n)
uncurryAbs :: forall n.
n -> Ty n -> SystemFExpr n -> ([(n, Ty n)], SystemFExpr n)
uncurryAbs n
name Ty n
ty = forall {a}.
[(a, Ty a)] -> SystemFExpr a -> ([(a, Ty a)], SystemFExpr a)
uncurry' [(n
name, Ty n
ty)]
where uncurry' :: [(a, Ty a)] -> SystemFExpr a -> ([(a, Ty a)], SystemFExpr a)
uncurry' [(a, Ty a)]
ns (Abs a
n' Ty a
t' SystemFExpr a
body') = [(a, Ty a)] -> SystemFExpr a -> ([(a, Ty a)], SystemFExpr a)
uncurry' ((a
n', Ty a
t')forall a. a -> [a] -> [a]
:[(a, Ty a)]
ns) SystemFExpr a
body'
uncurry' [(a, Ty a)]
ns SystemFExpr a
body' = (forall a. [a] -> [a]
reverse [(a, Ty a)]
ns, SystemFExpr a
body')
uncurryTyAbs :: n -> SystemFExpr n -> ([n], SystemFExpr n)
uncurryTyAbs :: forall n. n -> SystemFExpr n -> ([n], SystemFExpr n)
uncurryTyAbs n
ty = forall {a}. [a] -> SystemFExpr a -> ([a], SystemFExpr a)
uncurry' [n
ty]
where uncurry' :: [a] -> SystemFExpr a -> ([a], SystemFExpr a)
uncurry' [a]
ts (TyAbs a
t' SystemFExpr a
body') = [a] -> SystemFExpr a -> ([a], SystemFExpr a)
uncurry' (a
t'forall a. a -> [a] -> [a]
:[a]
ts) SystemFExpr a
body'
uncurry' [a]
ts SystemFExpr a
body' = (forall a. [a] -> [a]
reverse [a]
ts, SystemFExpr a
body')