{-# LANGUAGE Safe #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
module Cryptol.TypeCheck.AST
( module Cryptol.TypeCheck.AST
, Name()
, TFun(..)
, Selector(..)
, Import, ImportG(..)
, ImportSpec(..)
, ExportType(..)
, ExportSpec(..), isExportedBind, isExportedType, isExported
, Pragma(..)
, Fixity(..)
, PrimMap(..)
, module Cryptol.TypeCheck.Type
) where
import Cryptol.Parser.Position(Located,Range,HasLoc(..))
import Cryptol.ModuleSystem.Name
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Exports(ExportSpec(..)
, isExportedBind, isExportedType, isExported)
import Cryptol.Parser.AST ( Selector(..),Pragma(..)
, Import
, ImportG(..), ImportSpec(..), ExportType(..)
, Fixity(..))
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim)
import Cryptol.Utils.RecordMap
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Type
import GHC.Generics (Generic)
import Control.DeepSeq
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import Data.Text (Text)
data ModuleG mname =
Module { ModuleG mname -> mname
mName :: !mname
, ModuleG mname -> ExportSpec Name
mExports :: ExportSpec Name
, ModuleG mname -> [Import]
mImports :: [Import]
, ModuleG mname -> Map Name (IfaceG Name)
mSubModules :: Map Name (IfaceG Name)
, ModuleG mname -> Map Name ModTParam
mParamTypes :: Map Name ModTParam
, ModuleG mname -> [Located Prop]
mParamConstraints :: [Located Prop]
, ModuleG mname -> Map Name ModVParam
mParamFuns :: Map Name ModVParam
, ModuleG mname -> Map Name TySyn
mTySyns :: Map Name TySyn
, ModuleG mname -> Map Name Newtype
mNewtypes :: Map Name Newtype
, ModuleG mname -> Map Name AbstractType
mPrimTypes :: Map Name AbstractType
, ModuleG mname -> [DeclGroup]
mDecls :: [DeclGroup]
, ModuleG mname -> Map Name (ModuleG Name)
mFunctors :: Map Name (ModuleG Name)
} deriving (Int -> ModuleG mname -> ShowS
[ModuleG mname] -> ShowS
ModuleG mname -> String
(Int -> ModuleG mname -> ShowS)
-> (ModuleG mname -> String)
-> ([ModuleG mname] -> ShowS)
-> Show (ModuleG mname)
forall mname. Show mname => Int -> ModuleG mname -> ShowS
forall mname. Show mname => [ModuleG mname] -> ShowS
forall mname. Show mname => ModuleG mname -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModuleG mname] -> ShowS
$cshowList :: forall mname. Show mname => [ModuleG mname] -> ShowS
show :: ModuleG mname -> String
$cshow :: forall mname. Show mname => ModuleG mname -> String
showsPrec :: Int -> ModuleG mname -> ShowS
$cshowsPrec :: forall mname. Show mname => Int -> ModuleG mname -> ShowS
Show, (forall x. ModuleG mname -> Rep (ModuleG mname) x)
-> (forall x. Rep (ModuleG mname) x -> ModuleG mname)
-> Generic (ModuleG mname)
forall x. Rep (ModuleG mname) x -> ModuleG mname
forall x. ModuleG mname -> Rep (ModuleG mname) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall mname x. Rep (ModuleG mname) x -> ModuleG mname
forall mname x. ModuleG mname -> Rep (ModuleG mname) x
$cto :: forall mname x. Rep (ModuleG mname) x -> ModuleG mname
$cfrom :: forall mname x. ModuleG mname -> Rep (ModuleG mname) x
Generic, ModuleG mname -> ()
(ModuleG mname -> ()) -> NFData (ModuleG mname)
forall mname. NFData mname => ModuleG mname -> ()
forall a. (a -> ()) -> NFData a
rnf :: ModuleG mname -> ()
$crnf :: forall mname. NFData mname => ModuleG mname -> ()
NFData)
emptyModule :: mname -> ModuleG mname
emptyModule :: mname -> ModuleG mname
emptyModule mname
nm =
Module :: forall mname.
mname
-> ExportSpec Name
-> [Import]
-> Map Name (IfaceG Name)
-> Map Name ModTParam
-> [Located Prop]
-> Map Name ModVParam
-> Map Name TySyn
-> Map Name Newtype
-> Map Name AbstractType
-> [DeclGroup]
-> Map Name (ModuleG Name)
-> ModuleG mname
Module
{ mName :: mname
mName = mname
nm
, mExports :: ExportSpec Name
mExports = ExportSpec Name
forall a. Monoid a => a
mempty
, mImports :: [Import]
mImports = []
, mSubModules :: Map Name (IfaceG Name)
mSubModules = Map Name (IfaceG Name)
forall a. Monoid a => a
mempty
, mParamTypes :: Map Name ModTParam
mParamTypes = Map Name ModTParam
forall a. Monoid a => a
mempty
, mParamConstraints :: [Located Prop]
mParamConstraints = [Located Prop]
forall a. Monoid a => a
mempty
, mParamFuns :: Map Name ModVParam
mParamFuns = Map Name ModVParam
forall a. Monoid a => a
mempty
, mTySyns :: Map Name TySyn
mTySyns = Map Name TySyn
forall a. Monoid a => a
mempty
, mNewtypes :: Map Name Newtype
mNewtypes = Map Name Newtype
forall a. Monoid a => a
mempty
, mPrimTypes :: Map Name AbstractType
mPrimTypes = Map Name AbstractType
forall a. Monoid a => a
mempty
, mDecls :: [DeclGroup]
mDecls = [DeclGroup]
forall a. Monoid a => a
mempty
, mFunctors :: Map Name (ModuleG Name)
mFunctors = Map Name (ModuleG Name)
forall a. Monoid a => a
mempty
}
type Module = ModuleG ModName
isParametrizedModule :: ModuleG mname -> Bool
isParametrizedModule :: ModuleG mname -> Bool
isParametrizedModule ModuleG mname
m = Bool -> Bool
not (Map Name ModTParam -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ModuleG mname -> Map Name ModTParam
forall mname. ModuleG mname -> Map Name ModTParam
mParamTypes ModuleG mname
m) Bool -> Bool -> Bool
&&
[Located Prop] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ModuleG mname -> [Located Prop]
forall mname. ModuleG mname -> [Located Prop]
mParamConstraints ModuleG mname
m) Bool -> Bool -> Bool
&&
Map Name ModVParam -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ModuleG mname -> Map Name ModVParam
forall mname. ModuleG mname -> Map Name ModVParam
mParamFuns ModuleG mname
m))
data Expr = EList [Expr] Type
| ETuple [Expr]
| ERec (RecordMap Ident Expr)
| ESel Expr Selector
| ESet Type Expr Selector Expr
| EIf Expr Expr Expr
| EComp Type Type Expr [[Match]]
| EVar Name
| ETAbs TParam Expr
| ETApp Expr Type
| EApp Expr Expr
| EAbs Name Type Expr
| ELocated Range Expr
| EProofAbs Prop Expr
| EProofApp Expr
| EWhere Expr [DeclGroup]
deriving (Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> String
(Int -> Expr -> ShowS)
-> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> String
$cshow :: Expr -> String
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> Expr -> ShowS
Show, (forall x. Expr -> Rep Expr x)
-> (forall x. Rep Expr x -> Expr) -> Generic Expr
forall x. Rep Expr x -> Expr
forall x. Expr -> Rep Expr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Expr x -> Expr
$cfrom :: forall x. Expr -> Rep Expr x
Generic, Expr -> ()
(Expr -> ()) -> NFData Expr
forall a. (a -> ()) -> NFData a
rnf :: Expr -> ()
$crnf :: Expr -> ()
NFData)
data Match = From Name Type Type Expr
| Let Decl
deriving (Int -> Match -> ShowS
[Match] -> ShowS
Match -> String
(Int -> Match -> ShowS)
-> (Match -> String) -> ([Match] -> ShowS) -> Show Match
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Match] -> ShowS
$cshowList :: [Match] -> ShowS
show :: Match -> String
$cshow :: Match -> String
showsPrec :: Int -> Match -> ShowS
$cshowsPrec :: Int -> Match -> ShowS
Show, (forall x. Match -> Rep Match x)
-> (forall x. Rep Match x -> Match) -> Generic Match
forall x. Rep Match x -> Match
forall x. Match -> Rep Match x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Match x -> Match
$cfrom :: forall x. Match -> Rep Match x
Generic, Match -> ()
(Match -> ()) -> NFData Match
forall a. (a -> ()) -> NFData a
rnf :: Match -> ()
$crnf :: Match -> ()
NFData)
data DeclGroup = Recursive [Decl]
| NonRecursive Decl
deriving (Int -> DeclGroup -> ShowS
[DeclGroup] -> ShowS
DeclGroup -> String
(Int -> DeclGroup -> ShowS)
-> (DeclGroup -> String)
-> ([DeclGroup] -> ShowS)
-> Show DeclGroup
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DeclGroup] -> ShowS
$cshowList :: [DeclGroup] -> ShowS
show :: DeclGroup -> String
$cshow :: DeclGroup -> String
showsPrec :: Int -> DeclGroup -> ShowS
$cshowsPrec :: Int -> DeclGroup -> ShowS
Show, (forall x. DeclGroup -> Rep DeclGroup x)
-> (forall x. Rep DeclGroup x -> DeclGroup) -> Generic DeclGroup
forall x. Rep DeclGroup x -> DeclGroup
forall x. DeclGroup -> Rep DeclGroup x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DeclGroup x -> DeclGroup
$cfrom :: forall x. DeclGroup -> Rep DeclGroup x
Generic, DeclGroup -> ()
(DeclGroup -> ()) -> NFData DeclGroup
forall a. (a -> ()) -> NFData a
rnf :: DeclGroup -> ()
$crnf :: DeclGroup -> ()
NFData)
groupDecls :: DeclGroup -> [Decl]
groupDecls :: DeclGroup -> [Decl]
groupDecls DeclGroup
dg = case DeclGroup
dg of
Recursive [Decl]
ds -> [Decl]
ds
NonRecursive Decl
d -> [Decl
d]
data Decl = Decl { Decl -> Name
dName :: !Name
, Decl -> Schema
dSignature :: Schema
, Decl -> DeclDef
dDefinition :: DeclDef
, Decl -> [Pragma]
dPragmas :: [Pragma]
, Decl -> Bool
dInfix :: !Bool
, Decl -> Maybe Fixity
dFixity :: Maybe Fixity
, Decl -> Maybe Text
dDoc :: Maybe Text
} deriving ((forall x. Decl -> Rep Decl x)
-> (forall x. Rep Decl x -> Decl) -> Generic Decl
forall x. Rep Decl x -> Decl
forall x. Decl -> Rep Decl x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Decl x -> Decl
$cfrom :: forall x. Decl -> Rep Decl x
Generic, Decl -> ()
(Decl -> ()) -> NFData Decl
forall a. (a -> ()) -> NFData a
rnf :: Decl -> ()
$crnf :: Decl -> ()
NFData, Int -> Decl -> ShowS
[Decl] -> ShowS
Decl -> String
(Int -> Decl -> ShowS)
-> (Decl -> String) -> ([Decl] -> ShowS) -> Show Decl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Decl] -> ShowS
$cshowList :: [Decl] -> ShowS
show :: Decl -> String
$cshow :: Decl -> String
showsPrec :: Int -> Decl -> ShowS
$cshowsPrec :: Int -> Decl -> ShowS
Show)
data DeclDef = DPrim
| DExpr Expr
deriving (Int -> DeclDef -> ShowS
[DeclDef] -> ShowS
DeclDef -> String
(Int -> DeclDef -> ShowS)
-> (DeclDef -> String) -> ([DeclDef] -> ShowS) -> Show DeclDef
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DeclDef] -> ShowS
$cshowList :: [DeclDef] -> ShowS
show :: DeclDef -> String
$cshow :: DeclDef -> String
showsPrec :: Int -> DeclDef -> ShowS
$cshowsPrec :: Int -> DeclDef -> ShowS
Show, (forall x. DeclDef -> Rep DeclDef x)
-> (forall x. Rep DeclDef x -> DeclDef) -> Generic DeclDef
forall x. Rep DeclDef x -> DeclDef
forall x. DeclDef -> Rep DeclDef x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DeclDef x -> DeclDef
$cfrom :: forall x. DeclDef -> Rep DeclDef x
Generic, DeclDef -> ()
(DeclDef -> ()) -> NFData DeclDef
forall a. (a -> ()) -> NFData a
rnf :: DeclDef -> ()
$crnf :: DeclDef -> ()
NFData)
ePrim :: PrimMap -> PrimIdent -> Expr
ePrim :: PrimMap -> PrimIdent -> Expr
ePrim PrimMap
pm PrimIdent
n = Name -> Expr
EVar (PrimIdent -> PrimMap -> Name
lookupPrimDecl PrimIdent
n PrimMap
pm)
eError :: PrimMap -> Type -> String -> Expr
eError :: PrimMap -> Prop -> String -> Expr
eError PrimMap
prims Prop
t String
str =
Expr -> Expr -> Expr
EApp (Expr -> Prop -> Expr
ETApp (Expr -> Prop -> Expr
ETApp (PrimMap -> PrimIdent -> Expr
ePrim PrimMap
prims (Text -> PrimIdent
prelPrim Text
"error")) Prop
t)
(Int -> Prop
forall a. Integral a => a -> Prop
tNum (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
str))) (PrimMap -> String -> Expr
eString PrimMap
prims String
str)
eString :: PrimMap -> String -> Expr
eString :: PrimMap -> String -> Expr
eString PrimMap
prims String
str = [Expr] -> Prop -> Expr
EList ((Char -> Expr) -> String -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (PrimMap -> Char -> Expr
eChar PrimMap
prims) String
str) Prop
tChar
eChar :: PrimMap -> Char -> Expr
eChar :: PrimMap -> Char -> Expr
eChar PrimMap
prims Char
c = Expr -> Prop -> Expr
ETApp (Expr -> Prop -> Expr
ETApp (PrimMap -> PrimIdent -> Expr
ePrim PrimMap
prims (Text -> PrimIdent
prelPrim Text
"number")) (Int -> Prop
forall a. Integral a => a -> Prop
tNum Int
v)) (Prop -> Prop
tWord (Int -> Prop
forall a. Integral a => a -> Prop
tNum Int
w))
where v :: Int
v = Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c
w :: Int
w = Int
8 :: Int
instance PP (WithNames Expr) where
ppPrec :: Int -> WithNames Expr -> Doc
ppPrec Int
prec (WithNames Expr
expr NameMap
nm) =
case Expr
expr of
ELocated Range
_ Expr
t -> Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP Int
prec Expr
t
EList [] Prop
t -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"[]" Doc -> Doc -> Doc
<+> Doc
colon Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP Int
prec Prop
t
EList [Expr]
es Prop
_ -> [Doc] -> Doc
ppList ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Expr -> Doc) -> [Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW [Expr]
es
ETuple [Expr]
es -> [Doc] -> Doc
ppTuple ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Expr -> Doc) -> [Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW [Expr]
es
ERec RecordMap Ident Expr
fs -> [Doc] -> Doc
ppRecord
[ Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
f Doc -> Doc -> Doc
<+> String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e | (Ident
f,Expr
e) <- RecordMap Ident Expr -> [(Ident, Expr)]
forall a b. (Show a, Ord a) => RecordMap a b -> [(a, b)]
displayFields RecordMap Ident Expr
fs ]
ESel Expr
e Selector
sel -> Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP Int
4 Expr
e Doc -> Doc -> Doc
<.> String -> Doc
text String
"." Doc -> Doc -> Doc
<.> Selector -> Doc
forall a. PP a => a -> Doc
pp Selector
sel
ESet Prop
_ty Expr
e Selector
sel Expr
v -> Doc -> Doc
braces (Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
e Doc -> Doc -> Doc
<+> Doc
"|" Doc -> Doc -> Doc
<+> Selector -> Doc
forall a. PP a => a -> Doc
pp Selector
sel Doc -> Doc -> Doc
<+> Doc
"=" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
v)
EIf Expr
e1 Expr
e2 Expr
e3 -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ String -> Doc
text String
"if" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e1
, String -> Doc
text String
"then" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e2
, String -> Doc
text String
"else" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e3 ]
EComp Prop
_ Prop
_ Expr
e [[Match]]
mss -> let arm :: [a] -> Doc
arm [a]
ms = String -> Doc
text String
"|" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commaSep ((a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW [a]
ms)
in Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e Doc -> Doc -> Doc
<+> (Doc -> Doc
align ([Doc] -> Doc
vcat (([Match] -> Doc) -> [[Match]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map [Match] -> Doc
forall a. PP (WithNames a) => [a] -> Doc
arm [[Match]]
mss)))
EVar Name
x -> Name -> Doc
forall a. PPName a => a -> Doc
ppPrefixName Name
x
EAbs {} -> let ([(Name, Prop)]
xs,Expr
e) = (Expr -> Maybe ((Name, Prop), Expr))
-> Expr -> ([(Name, Prop)], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe ((Name, Prop), Expr)
splitAbs Expr
expr
in NameMap
-> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
ppLam NameMap
nm Int
prec [] [] [(Name, Prop)]
xs Expr
e
EProofAbs {} -> let ([Prop]
ps,Expr
e1) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (Prop, Expr)
splitProofAbs Expr
expr
([(Name, Prop)]
xs,Expr
e2) = (Expr -> Maybe ((Name, Prop), Expr))
-> Expr -> ([(Name, Prop)], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe ((Name, Prop), Expr)
splitAbs Expr
e1
in NameMap
-> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
ppLam NameMap
nm Int
prec [] [Prop]
ps [(Name, Prop)]
xs Expr
e2
ETAbs {} -> let ([TParam]
ts,Expr
e1) = (Expr -> Maybe (TParam, Expr)) -> Expr -> ([TParam], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (TParam, Expr)
splitTAbs Expr
expr
([Prop]
ps,Expr
e2) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (Prop, Expr)
splitProofAbs Expr
e1
([(Name, Prop)]
xs,Expr
e3) = (Expr -> Maybe ((Name, Prop), Expr))
-> Expr -> ([(Name, Prop)], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe ((Name, Prop), Expr)
splitAbs Expr
e2
in NameMap
-> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
ppLam NameMap
nm Int
prec [TParam]
ts [Prop]
ps [(Name, Prop)]
xs Expr
e3
EApp (EApp (EVar Name
o) Expr
a) Expr
b
| Ident -> Bool
isInfixIdent (Name -> Ident
nameIdent Name
o) ->
Int -> Expr -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
3 Expr
a Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PPName a => a -> Doc
ppInfixName Name
o Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
3 Expr
b
| Bool
otherwise ->
Name -> Doc
forall a. PPName a => a -> Doc
ppPrefixName Name
o Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
3 Expr
a Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec Int
3 Expr
b
EApp Expr
e1 Expr
e2 -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP Int
3 Expr
e1 Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP Int
4 Expr
e2
EProofApp Expr
e -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP Int
3 Expr
e Doc -> Doc -> Doc
<+> String -> Doc
text String
"<>"
ETApp Expr
e Prop
t -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP Int
3 Expr
e Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP Int
5 Prop
t
EWhere Expr
e [DeclGroup]
ds -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
align (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
[ Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e
, Doc -> Int -> Doc -> Doc
hang Doc
"where" Int
2 ([Doc] -> Doc
vcat ((DeclGroup -> Doc) -> [DeclGroup] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map DeclGroup -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW [DeclGroup]
ds))
]
where
ppW :: a -> Doc
ppW a
x = NameMap -> a -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm a
x
ppWP :: Int -> a -> Doc
ppWP Int
x = NameMap -> Int -> a -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
x
ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name,Type)] -> Expr -> Doc
ppLam :: NameMap
-> Int -> [TParam] -> [Prop] -> [(Name, Prop)] -> Expr -> Doc
ppLam NameMap
nm Int
prec [] [] [] Expr
e = Int -> Doc -> Doc
nest Int
2 (NameMap -> Int -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
prec Expr
e)
ppLam NameMap
nm Int
prec [TParam]
ts [Prop]
ps [(Name, Prop)]
xs Expr
e =
Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep
[ String -> Doc
text String
"\\" Doc -> Doc -> Doc
<.> [Doc] -> Doc
hsep ([Doc]
tsD [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
psD [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
xsD [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Doc
text String
"->"])
, NameMap -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 Expr
e
]
where
ns1 :: NameMap
ns1 = [TParam] -> NameMap -> NameMap
addTNames [TParam]
ts NameMap
nm
tsD :: [Doc]
tsD = if [TParam] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TParam]
ts then [] else [Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
commaSep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (TParam -> Doc) -> [TParam] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> Doc
ppT [TParam]
ts]
psD :: [Doc]
psD = if [Prop] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Prop]
ps then [] else [Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
commaSep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Prop -> Doc) -> [Prop] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> Doc
ppP [Prop]
ps]
xsD :: [Doc]
xsD = if [(Name, Prop)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, Prop)]
xs then [] else [[Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((Name, Prop) -> Doc) -> [(Name, Prop)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Prop) -> Doc
forall a a. (PP a, PP (WithNames a)) => (a, a) -> Doc
ppArg [(Name, Prop)]
xs]
ppT :: TParam -> Doc
ppT = NameMap -> TParam -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1
ppP :: Prop -> Doc
ppP = NameMap -> Prop -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1
ppArg :: (a, a) -> Doc
ppArg (a
x,a
t) = Doc -> Doc
parens (a -> Doc
forall a. PP a => a -> Doc
pp a
x Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> NameMap -> a -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
ns1 a
t)
splitWhile :: (a -> Maybe (b,a)) -> a -> ([b],a)
splitWhile :: (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile a -> Maybe (b, a)
f a
e = case a -> Maybe (b, a)
f a
e of
Maybe (b, a)
Nothing -> ([], a
e)
Just (b
x,a
e1) -> let ([b]
xs,a
e2) = (a -> Maybe (b, a)) -> a -> ([b], a)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile a -> Maybe (b, a)
f a
e1
in (b
xb -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
xs,a
e2)
splitAbs :: Expr -> Maybe ((Name,Type), Expr)
splitAbs :: Expr -> Maybe ((Name, Prop), Expr)
splitAbs (EAbs Name
x Prop
t Expr
e) = ((Name, Prop), Expr) -> Maybe ((Name, Prop), Expr)
forall a. a -> Maybe a
Just ((Name
x,Prop
t), Expr
e)
splitAbs Expr
_ = Maybe ((Name, Prop), Expr)
forall a. Maybe a
Nothing
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitTAbs (ETAbs TParam
t Expr
e) = (TParam, Expr) -> Maybe (TParam, Expr)
forall a. a -> Maybe a
Just (TParam
t, Expr
e)
splitTAbs Expr
_ = Maybe (TParam, Expr)
forall a. Maybe a
Nothing
splitProofAbs :: Expr -> Maybe (Prop, Expr)
splitProofAbs :: Expr -> Maybe (Prop, Expr)
splitProofAbs (EProofAbs Prop
p Expr
e) = (Prop, Expr) -> Maybe (Prop, Expr)
forall a. a -> Maybe a
Just (Prop
p,Expr
e)
splitProofAbs Expr
_ = Maybe (Prop, Expr)
forall a. Maybe a
Nothing
splitTApp :: Expr -> Maybe (Type,Expr)
splitTApp :: Expr -> Maybe (Prop, Expr)
splitTApp (ETApp Expr
e Prop
t) = (Prop, Expr) -> Maybe (Prop, Expr)
forall a. a -> Maybe a
Just (Prop
t, Expr
e)
splitTApp Expr
_ = Maybe (Prop, Expr)
forall a. Maybe a
Nothing
splitProofApp :: Expr -> Maybe ((), Expr)
splitProofApp :: Expr -> Maybe ((), Expr)
splitProofApp (EProofApp Expr
e) = ((), Expr) -> Maybe ((), Expr)
forall a. a -> Maybe a
Just ((), Expr
e)
splitProofApp Expr
_ = Maybe ((), Expr)
forall a. Maybe a
Nothing
splitExprInst :: Expr -> (Expr, [Type], Int)
splitExprInst :: Expr -> (Expr, [Prop], Int)
splitExprInst Expr
e = (Expr
e2, [Prop] -> [Prop]
forall a. [a] -> [a]
reverse [Prop]
ts, [()] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [()]
ps)
where
([()]
ps,Expr
e1) = (Expr -> Maybe ((), Expr)) -> Expr -> ([()], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe ((), Expr)
splitProofApp Expr
e
([Prop]
ts,Expr
e2) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe (Prop, Expr)
splitTApp Expr
e1
instance HasLoc Expr where
getLoc :: Expr -> Maybe Range
getLoc (ELocated Range
r Expr
_) = Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r
getLoc Expr
_ = Maybe Range
forall a. Maybe a
Nothing
instance PP Expr where
ppPrec :: Int -> Expr -> Doc
ppPrec Int
n Expr
t = NameMap -> Int -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty Int
n Expr
t
instance PP (WithNames Match) where
ppPrec :: Int -> WithNames Match -> Doc
ppPrec Int
_ (WithNames Match
mat NameMap
nm) =
case Match
mat of
From Name
x Prop
_ Prop
_ Expr
e -> Name -> Doc
forall a. PP a => a -> Doc
pp Name
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"<-" Doc -> Doc -> Doc
<+> NameMap -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Expr
e
Let Decl
d -> String -> Doc
text String
"let" Doc -> Doc -> Doc
<+> NameMap -> Decl -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Decl
d
instance PP Match where
ppPrec :: Int -> Match -> Doc
ppPrec = NameMap -> Int -> Match -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty
instance PP (WithNames DeclGroup) where
ppPrec :: Int -> WithNames DeclGroup -> Doc
ppPrec Int
_ (WithNames DeclGroup
dg NameMap
nm) =
case DeclGroup
dg of
Recursive [Decl]
ds -> String -> Doc
text String
"/* Recursive */"
Doc -> Doc -> Doc
$$ [Doc] -> Doc
vcat ((Decl -> Doc) -> [Decl] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> Decl -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm) [Decl]
ds)
Doc -> Doc -> Doc
$$ String -> Doc
text String
""
NonRecursive Decl
d -> String -> Doc
text String
"/* Not recursive */"
Doc -> Doc -> Doc
$$ NameMap -> Decl -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Decl
d
Doc -> Doc -> Doc
$$ String -> Doc
text String
""
instance PP DeclGroup where
ppPrec :: Int -> DeclGroup -> Doc
ppPrec = NameMap -> Int -> DeclGroup -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty
instance PP (WithNames Decl) where
ppPrec :: Int -> WithNames Decl -> Doc
ppPrec Int
_ (WithNames Decl { Bool
[Pragma]
Maybe Text
Maybe Fixity
Name
Schema
DeclDef
dDoc :: Maybe Text
dFixity :: Maybe Fixity
dInfix :: Bool
dPragmas :: [Pragma]
dDefinition :: DeclDef
dSignature :: Schema
dName :: Name
dDoc :: Decl -> Maybe Text
dFixity :: Decl -> Maybe Fixity
dInfix :: Decl -> Bool
dPragmas :: Decl -> [Pragma]
dDefinition :: Decl -> DeclDef
dSignature :: Decl -> Schema
dName :: Decl -> Name
.. } NameMap
nm) =
[Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
[ Name -> Doc
forall a. PP a => a -> Doc
pp Name
dName Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> NameMap -> Schema -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Schema
dSignature ]
[Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ (if [Pragma] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pragma]
dPragmas
then []
else [String -> Doc
text String
"pragmas" Doc -> Doc -> Doc
<+> Name -> Doc
forall a. PP a => a -> Doc
pp Name
dName Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep ((Pragma -> Doc) -> [Pragma] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Pragma -> Doc
forall a. PP a => a -> Doc
pp [Pragma]
dPragmas)])
[Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
sep [Name -> Doc
forall a. PP a => a -> Doc
pp Name
dName Doc -> Doc -> Doc
<+> String -> Doc
text String
"=", NameMap -> DeclDef -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm DeclDef
dDefinition]) ]
instance PP (WithNames DeclDef) where
ppPrec :: Int -> WithNames DeclDef -> Doc
ppPrec Int
_ (WithNames DeclDef
DPrim NameMap
_) = String -> Doc
text String
"<primitive>"
ppPrec Int
_ (WithNames (DExpr Expr
e) NameMap
nm) = NameMap -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Expr
e
instance PP Decl where
ppPrec :: Int -> Decl -> Doc
ppPrec = NameMap -> Int -> Decl -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty
instance PP n => PP (ModuleG n) where
ppPrec :: Int -> ModuleG n -> Doc
ppPrec = NameMap -> Int -> ModuleG n -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty
instance PP n => PP (WithNames (ModuleG n)) where
ppPrec :: Int -> WithNames (ModuleG n) -> Doc
ppPrec Int
_ (WithNames Module { n
[Located Prop]
[Import]
[DeclGroup]
Map Name AbstractType
Map Name Newtype
Map Name TySyn
Map Name ModVParam
Map Name ModTParam
Map Name (IfaceG Name)
Map Name (ModuleG Name)
ExportSpec Name
mFunctors :: Map Name (ModuleG Name)
mDecls :: [DeclGroup]
mPrimTypes :: Map Name AbstractType
mNewtypes :: Map Name Newtype
mTySyns :: Map Name TySyn
mParamFuns :: Map Name ModVParam
mParamConstraints :: [Located Prop]
mParamTypes :: Map Name ModTParam
mSubModules :: Map Name (IfaceG Name)
mImports :: [Import]
mExports :: ExportSpec Name
mName :: n
mFunctors :: forall mname. ModuleG mname -> Map Name (ModuleG Name)
mDecls :: forall mname. ModuleG mname -> [DeclGroup]
mPrimTypes :: forall mname. ModuleG mname -> Map Name AbstractType
mNewtypes :: forall mname. ModuleG mname -> Map Name Newtype
mTySyns :: forall mname. ModuleG mname -> Map Name TySyn
mParamFuns :: forall mname. ModuleG mname -> Map Name ModVParam
mParamConstraints :: forall mname. ModuleG mname -> [Located Prop]
mParamTypes :: forall mname. ModuleG mname -> Map Name ModTParam
mSubModules :: forall mname. ModuleG mname -> Map Name (IfaceG Name)
mImports :: forall mname. ModuleG mname -> [Import]
mExports :: forall mname. ModuleG mname -> ExportSpec Name
mName :: forall mname. ModuleG mname -> mname
.. } NameMap
nm) =
String -> Doc
text String
"module" Doc -> Doc -> Doc
<+> n -> Doc
forall a. PP a => a -> Doc
pp n
mName Doc -> Doc -> Doc
$$
[Doc] -> Doc
vcat ((Import -> Doc) -> [Import] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Import -> Doc
forall a. PP a => a -> Doc
pp [Import]
mImports) Doc -> Doc -> Doc
$$
[Doc] -> Doc
vcat ((DeclGroup -> Doc) -> [DeclGroup] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (NameMap -> DeclGroup -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames ([TParam] -> NameMap -> NameMap
addTNames [TParam]
mps NameMap
nm)) [DeclGroup]
mDecls)
where mps :: [TParam]
mps = (ModTParam -> TParam) -> [ModTParam] -> [TParam]
forall a b. (a -> b) -> [a] -> [b]
map ModTParam -> TParam
mtpParam (Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems Map Name ModTParam
mParamTypes)