{-# 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(..)
, ImportSpec(..)
, ExportType(..)
, ExportSpec(..), isExportedBind, isExportedType
, Pragma(..)
, Fixity(..)
, PrimMap(..)
, TCErrorMessage(..)
, module Cryptol.TypeCheck.Type
) where
import Cryptol.Parser.Position(Located)
import Cryptol.ModuleSystem.Name
import Cryptol.ModuleSystem.Exports(ExportSpec(..)
, isExportedBind, isExportedType)
import Cryptol.Parser.AST ( Selector(..),Pragma(..)
, Import(..), ImportSpec(..), ExportType(..)
, Fixity(..))
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent)
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
data Module = Module { Module -> ModName
mName :: !ModName
, Module -> ExportSpec Name
mExports :: ExportSpec Name
, Module -> [Import]
mImports :: [Import]
, Module -> Map Name TySyn
mTySyns :: Map Name TySyn
, Module -> Map Name Newtype
mNewtypes :: Map Name Newtype
, Module -> Map Name AbstractType
mPrimTypes :: Map Name AbstractType
, Module -> Map Name ModTParam
mParamTypes :: Map Name ModTParam
, Module -> [Located Prop]
mParamConstraints :: [Located Prop]
, Module -> Map Name ModVParam
mParamFuns :: Map Name ModVParam
, Module -> [DeclGroup]
mDecls :: [DeclGroup]
} deriving (Int -> Module -> ShowS
[Module] -> ShowS
Module -> String
(Int -> Module -> ShowS)
-> (Module -> String) -> ([Module] -> ShowS) -> Show Module
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Module] -> ShowS
$cshowList :: [Module] -> ShowS
show :: Module -> String
$cshow :: Module -> String
showsPrec :: Int -> Module -> ShowS
$cshowsPrec :: Int -> Module -> ShowS
Show, (forall x. Module -> Rep Module x)
-> (forall x. Rep Module x -> Module) -> Generic Module
forall x. Rep Module x -> Module
forall x. Module -> Rep Module x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Module x -> Module
$cfrom :: forall x. Module -> Rep Module x
Generic, Module -> ()
(Module -> ()) -> NFData Module
forall a. (a -> ()) -> NFData a
rnf :: Module -> ()
$crnf :: Module -> ()
NFData)
isParametrizedModule :: Module -> Bool
isParametrizedModule :: Module -> Bool
isParametrizedModule m :: Module
m = Bool -> Bool
not (Map Name ModTParam -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Module -> Map Name ModTParam
mParamTypes Module
m) Bool -> Bool -> Bool
&&
[Located Prop] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Module -> [Located Prop]
mParamConstraints Module
m) Bool -> Bool -> Bool
&&
Map Name ModVParam -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Module -> Map Name ModVParam
mParamFuns Module
m))
data ModTParam = ModTParam
{ ModTParam -> Name
mtpName :: Name
, ModTParam -> Kind
mtpKind :: Kind
, ModTParam -> Int
mtpNumber :: !Int
, ModTParam -> Maybe String
mtpDoc :: Maybe String
} deriving (Int -> ModTParam -> ShowS
[ModTParam] -> ShowS
ModTParam -> String
(Int -> ModTParam -> ShowS)
-> (ModTParam -> String)
-> ([ModTParam] -> ShowS)
-> Show ModTParam
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModTParam] -> ShowS
$cshowList :: [ModTParam] -> ShowS
show :: ModTParam -> String
$cshow :: ModTParam -> String
showsPrec :: Int -> ModTParam -> ShowS
$cshowsPrec :: Int -> ModTParam -> ShowS
Show,(forall x. ModTParam -> Rep ModTParam x)
-> (forall x. Rep ModTParam x -> ModTParam) -> Generic ModTParam
forall x. Rep ModTParam x -> ModTParam
forall x. ModTParam -> Rep ModTParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModTParam x -> ModTParam
$cfrom :: forall x. ModTParam -> Rep ModTParam x
Generic,ModTParam -> ()
(ModTParam -> ()) -> NFData ModTParam
forall a. (a -> ()) -> NFData a
rnf :: ModTParam -> ()
$crnf :: ModTParam -> ()
NFData)
mtpParam :: ModTParam -> TParam
mtpParam :: ModTParam -> TParam
mtpParam mtp :: ModTParam
mtp = $WTParam :: Int -> Kind -> TPFlavor -> TVarInfo -> TParam
TParam { tpUnique :: Int
tpUnique = Name -> Int
nameUnique (ModTParam -> Name
mtpName ModTParam
mtp)
, tpKind :: Kind
tpKind = ModTParam -> Kind
mtpKind ModTParam
mtp
, tpFlav :: TPFlavor
tpFlav = Name -> TPFlavor
TPModParam (ModTParam -> Name
mtpName ModTParam
mtp)
, tpInfo :: TVarInfo
tpInfo = TVarInfo
desc
}
where desc :: TVarInfo
desc = TVarInfo :: Range -> TVarSource -> TVarInfo
TVarInfo { tvarDesc :: TVarSource
tvarDesc = Name -> TVarSource
TVFromModParam (ModTParam -> Name
mtpName ModTParam
mtp)
, tvarSource :: Range
tvarSource = Name -> Range
nameLoc (ModTParam -> Name
mtpName ModTParam
mtp)
}
data ModVParam = ModVParam
{ ModVParam -> Name
mvpName :: Name
, ModVParam -> Schema
mvpType :: Schema
, ModVParam -> Maybe String
mvpDoc :: Maybe String
, ModVParam -> Maybe Fixity
mvpFixity :: Maybe Fixity
} deriving (Int -> ModVParam -> ShowS
[ModVParam] -> ShowS
ModVParam -> String
(Int -> ModVParam -> ShowS)
-> (ModVParam -> String)
-> ([ModVParam] -> ShowS)
-> Show ModVParam
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModVParam] -> ShowS
$cshowList :: [ModVParam] -> ShowS
show :: ModVParam -> String
$cshow :: ModVParam -> String
showsPrec :: Int -> ModVParam -> ShowS
$cshowsPrec :: Int -> ModVParam -> ShowS
Show,(forall x. ModVParam -> Rep ModVParam x)
-> (forall x. Rep ModVParam x -> ModVParam) -> Generic ModVParam
forall x. Rep ModVParam x -> ModVParam
forall x. ModVParam -> Rep ModVParam x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModVParam x -> ModVParam
$cfrom :: forall x. ModVParam -> Rep ModVParam x
Generic,ModVParam -> ()
(ModVParam -> ()) -> NFData ModVParam
forall a. (a -> ()) -> NFData a
rnf :: ModVParam -> ()
$crnf :: ModVParam -> ()
NFData)
data Expr = EList [Expr] Type
| ETuple [Expr]
| ERec [(Ident,Expr)]
| ESel Expr Selector
| ESet 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
| 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 dg :: DeclGroup
dg = case DeclGroup
dg of
Recursive ds :: [Decl]
ds -> [Decl]
ds
NonRecursive d :: 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 String
dDoc :: Maybe String
} 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 -> Ident -> Expr
ePrim :: PrimMap -> Ident -> Expr
ePrim pm :: PrimMap
pm n :: Ident
n = Name -> Expr
EVar (Ident -> PrimMap -> Name
lookupPrimDecl Ident
n PrimMap
pm)
eError :: PrimMap -> Type -> String -> Expr
eError :: PrimMap -> Prop -> String -> Expr
eError prims :: PrimMap
prims t :: Prop
t str :: String
str =
Expr -> Expr -> Expr
EApp (Expr -> Prop -> Expr
ETApp (Expr -> Prop -> Expr
ETApp (PrimMap -> Ident -> Expr
ePrim PrimMap
prims (String -> Ident
packIdent "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 prims :: PrimMap
prims str :: 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 prims :: PrimMap
prims c :: Char
c = Expr -> Prop -> Expr
ETApp (Expr -> Prop -> Expr
ETApp (PrimMap -> Ident -> Expr
ePrim PrimMap
prims (String -> Ident
packIdent "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 = 8 :: Int
instance PP (WithNames Expr) where
ppPrec :: Int -> WithNames Expr -> Doc
ppPrec prec :: Int
prec (WithNames expr :: Expr
expr nm :: NameMap
nm) =
case Expr
expr of
EList [] t :: Prop
t -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "[]" 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 es :: [Expr]
es _ -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([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 es :: [Expr]
es -> Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([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 fs :: [(Ident, Expr)]
fs -> Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma
[ Ident -> Doc
forall a. PP a => a -> Doc
pp Ident
f Doc -> Doc -> Doc
<+> String -> Doc
text "=" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e | (f :: Ident
f,e :: Expr
e) <- [(Ident, Expr)]
fs ]
ESel e :: Expr
e sel :: Selector
sel -> Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 4 Expr
e Doc -> Doc -> Doc
<+> String -> Doc
text "." Doc -> Doc -> Doc
<.> Selector -> Doc
forall a. PP a => a -> Doc
pp Selector
sel
ESet e :: Expr
e sel :: Selector
sel v :: Expr
v -> Doc -> Doc
braces (Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
e Doc -> Doc -> Doc
<+> "|" Doc -> Doc -> Doc
<+> Selector -> Doc
forall a. PP a => a -> Doc
pp Selector
sel Doc -> Doc -> Doc
<+> "=" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP a => a -> Doc
pp Expr
v)
EIf e1 :: Expr
e1 e2 :: Expr
e2 e3 :: Expr
e3 -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ String -> Doc
text "if" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e1
, String -> Doc
text "then" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e2
, String -> Doc
text "else" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e3 ]
EComp _ _ e :: Expr
e mss :: [[Match]]
mss -> let arm :: [a] -> Doc
arm ms :: [a]
ms = String -> Doc
text "|" 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
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 x :: Name
x -> Name -> Doc
forall a. PPName a => a -> Doc
ppPrefixName Name
x
EAbs {} -> let (xs :: [(Name, Prop)]
xs,e :: 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 (ps :: [Prop]
ps,e1 :: 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
(xs :: [(Name, Prop)]
xs,e2 :: 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 (ts :: [TParam]
ts,e1 :: 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
(ps :: [Prop]
ps,e2 :: 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
(xs :: [(Name, Prop)]
xs,e3 :: 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 o :: Name
o) a :: Expr
a) b :: Expr
b
| Ident -> Bool
isInfixIdent (Name -> Ident
nameIdent Name
o) ->
Int -> Expr -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec 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 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 3 Expr
a Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. PP a => Int -> a -> Doc
ppPrec 3 Expr
b
EApp e1 :: Expr
e1 e2 :: Expr
e2 -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 3 Expr
e1 Doc -> Doc -> Doc
<+> Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 4 Expr
e2
EProofApp e :: Expr
e -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 3 Expr
e Doc -> Doc -> Doc
<+> String -> Doc
text "<>"
ETApp e :: Expr
e t :: Prop
t -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 3)
(Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Expr -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 3 Expr
e Doc -> Doc -> Doc
<+> Int -> Prop -> Doc
forall a. PP (WithNames a) => Int -> a -> Doc
ppWP 4 Prop
t
EWhere e :: Expr
e ds :: [DeclGroup]
ds -> Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0)
( Expr -> Doc
forall a. PP (WithNames a) => a -> Doc
ppW Expr
e Doc -> Doc -> Doc
$$ String -> Doc
text "where"
Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 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))
Doc -> Doc -> Doc
$$ String -> Doc
text "" )
where
ppW :: a -> Doc
ppW x :: a
x = NameMap -> a -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm a
x
ppWP :: Int -> a -> Doc
ppWP x :: 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 nm :: NameMap
nm prec :: Int
prec [] [] [] e :: Expr
e = NameMap -> Int -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
nm Int
prec Expr
e
ppLam nm :: NameMap
nm prec :: Int
prec ts :: [TParam]
ts ps :: [Prop]
ps xs :: [(Name, Prop)]
xs e :: Expr
e =
Bool -> Doc -> Doc
optParens (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
[Doc] -> Doc
sep [ String -> Doc
text "\\" Doc -> Doc -> Doc
<.> Doc
tsD Doc -> Doc -> Doc
<+> Doc
psD Doc -> Doc -> Doc
<+> Doc
xsD Doc -> Doc -> Doc
<+> String -> Doc
text "->"
, 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 Doc
empty else Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([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 Doc
empty else Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([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 Doc
empty 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 (x :: a
x,t :: a
t) = Doc -> Doc
parens (a -> Doc
forall a. PP a => a -> Doc
pp a
x Doc -> Doc -> Doc
<+> String -> Doc
text ":" 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 f :: a -> Maybe (b, a)
f e :: a
e = case a -> Maybe (b, a)
f a
e of
Nothing -> ([], a
e)
Just (x :: b
x,e1 :: a
e1) -> let (xs :: [b]
xs,e2 :: 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 x :: Name
x t :: Prop
t e :: Expr
e) = ((Name, Prop), Expr) -> Maybe ((Name, Prop), Expr)
forall a. a -> Maybe a
Just ((Name
x,Prop
t), Expr
e)
splitAbs _ = Maybe ((Name, Prop), Expr)
forall a. Maybe a
Nothing
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitTAbs :: Expr -> Maybe (TParam, Expr)
splitTAbs (ETAbs t :: TParam
t e :: Expr
e) = (TParam, Expr) -> Maybe (TParam, Expr)
forall a. a -> Maybe a
Just (TParam
t, Expr
e)
splitTAbs _ = Maybe (TParam, Expr)
forall a. Maybe a
Nothing
splitProofAbs :: Expr -> Maybe (Prop, Expr)
splitProofAbs :: Expr -> Maybe (Prop, Expr)
splitProofAbs (EProofAbs p :: Prop
p e :: Expr
e) = (Prop, Expr) -> Maybe (Prop, Expr)
forall a. a -> Maybe a
Just (Prop
p,Expr
e)
splitProofAbs _ = Maybe (Prop, Expr)
forall a. Maybe a
Nothing
splitTApp :: Expr -> Maybe (Type,Expr)
splitTApp :: Expr -> Maybe (Prop, Expr)
splitTApp (ETApp e :: Expr
e t :: Prop
t) = (Prop, Expr) -> Maybe (Prop, Expr)
forall a. a -> Maybe a
Just (Prop
t, Expr
e)
splitTApp _ = Maybe (Prop, Expr)
forall a. Maybe a
Nothing
splitProofApp :: Expr -> Maybe ((), Expr)
splitProofApp :: Expr -> Maybe ((), Expr)
splitProofApp (EProofApp e :: Expr
e) = ((), Expr) -> Maybe ((), Expr)
forall a. a -> Maybe a
Just ((), Expr
e)
splitProofApp _ = Maybe ((), Expr)
forall a. Maybe a
Nothing
splitExprInst :: Expr -> (Expr, [Type], Int)
splitExprInst :: Expr -> (Expr, [Prop], Int)
splitExprInst e :: 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 :: [()]
ps,e1 :: Expr
e1) = (Expr -> Maybe ((), Expr)) -> Expr -> ([()], Expr)
forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
splitWhile Expr -> Maybe ((), Expr)
splitProofApp Expr
e
(ts :: [Prop]
ts,e2 :: 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 PP Expr where
ppPrec :: Int -> Expr -> Doc
ppPrec n :: Int
n t :: 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 _ (WithNames mat :: Match
mat nm :: NameMap
nm) =
case Match
mat of
From x :: Name
x _ _ e :: Expr
e -> Name -> Doc
forall a. PP a => a -> Doc
pp Name
x Doc -> Doc -> Doc
<+> String -> Doc
text "<-" Doc -> Doc -> Doc
<+> NameMap -> Expr -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Expr
e
Let d :: Decl
d -> String -> Doc
text "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 _ (WithNames dg :: DeclGroup
dg nm :: NameMap
nm) =
case DeclGroup
dg of
Recursive ds :: [Decl]
ds -> String -> Doc
text "/* 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 ""
NonRecursive d :: Decl
d -> String -> Doc
text "/* 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 ""
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 _ (WithNames Decl { .. } nm :: NameMap
nm) =
Name -> Doc
forall a. PP a => a -> Doc
pp Name
dName Doc -> Doc -> Doc
<+> String -> Doc
text ":" Doc -> Doc -> Doc
<+> NameMap -> Schema -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
nm Schema
dSignature Doc -> Doc -> Doc
$$
(if [Pragma] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pragma]
dPragmas
then Doc
empty
else String -> Doc
text "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
$$
Name -> Doc
forall a. PP a => a -> Doc
pp Name
dName Doc -> Doc -> Doc
<+> String -> Doc
text "=" Doc -> Doc -> Doc
<+> 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 _ (WithNames DPrim _) = String -> Doc
text "<primitive>"
ppPrec _ (WithNames (DExpr e :: Expr
e) nm :: 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 Module where
ppPrec :: Int -> Module -> Doc
ppPrec = NameMap -> Int -> Module -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty
instance PP (WithNames Module) where
ppPrec :: Int -> WithNames Module -> Doc
ppPrec _ (WithNames Module { .. } nm :: NameMap
nm) =
String -> Doc
text "module" Doc -> Doc -> Doc
<+> ModName -> Doc
forall a. PP a => a -> Doc
pp ModName
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)