{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
module Cryptol.Parser.ExpandPropGuards where
import Control.DeepSeq
import Cryptol.Parser.AST
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
import Data.Text (pack)
import GHC.Generics (Generic)
type ExpandPropGuardsM a = Either Error a
runExpandPropGuardsM :: ExpandPropGuardsM a -> Either Error a
runExpandPropGuardsM :: forall a. ExpandPropGuardsM a -> ExpandPropGuardsM a
runExpandPropGuardsM ExpandPropGuardsM a
m = ExpandPropGuardsM a
m
data Error = NoSignature (Located PName)
deriving (Int -> Error -> ShowS
[Error] -> ShowS
Error -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Error] -> ShowS
$cshowList :: [Error] -> ShowS
show :: Error -> String
$cshow :: Error -> String
showsPrec :: Int -> Error -> ShowS
$cshowsPrec :: Int -> Error -> ShowS
Show, forall x. Rep Error x -> Error
forall x. Error -> Rep Error x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Error x -> Error
$cfrom :: forall x. Error -> Rep Error x
Generic, Error -> ()
forall a. (a -> ()) -> NFData a
rnf :: Error -> ()
$crnf :: Error -> ()
NFData)
instance PP Error where
ppPrec :: Int -> Error -> Doc
ppPrec Int
_ Error
err = case Error
err of
NoSignature Located PName
x ->
String -> Doc
text String
"At" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp (forall a. Located a -> Range
srcRange Located PName
x) Doc -> Doc -> Doc
<.> Doc
colon
Doc -> Doc -> Doc
<+> String -> Doc
text String
"Declarations using constraint guards require an explicit type signature."
expandPropGuards :: ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName)
expandPropGuards :: forall mname.
ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName)
expandPropGuards ModuleG mname PName
m =
do ModuleDefinition PName
def <- ModuleDefinition PName
-> ExpandPropGuardsM (ModuleDefinition PName)
expandModuleDef (forall mname name. ModuleG mname name -> ModuleDefinition name
mDef ModuleG mname PName
m)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleG mname PName
m { mDef :: ModuleDefinition PName
mDef = ModuleDefinition PName
def }
expandModuleDef :: ModuleDefinition PName -> ExpandPropGuardsM (ModuleDefinition PName)
expandModuleDef :: ModuleDefinition PName
-> ExpandPropGuardsM (ModuleDefinition PName)
expandModuleDef ModuleDefinition PName
m =
case ModuleDefinition PName
m of
NormalModule [TopDecl PName]
ds -> forall name. [TopDecl name] -> ModuleDefinition name
NormalModule forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TopDecl PName -> ExpandPropGuardsM [TopDecl PName]
expandTopDecl [TopDecl PName]
ds
FunctorInstance {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleDefinition PName
m
InterfaceModule {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleDefinition PName
m
expandTopDecl :: TopDecl PName -> ExpandPropGuardsM [TopDecl PName]
expandTopDecl :: TopDecl PName -> ExpandPropGuardsM [TopDecl PName]
expandTopDecl TopDecl PName
topDecl =
case TopDecl PName
topDecl of
Decl TopLevel (Decl PName)
topLevelDecl ->
do [Decl PName]
ds <- Decl PName -> ExpandPropGuardsM [Decl PName]
expandDecl (forall a. TopLevel a -> a
tlValue TopLevel (Decl PName)
topLevelDecl)
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ forall name. TopLevel (Decl name) -> TopDecl name
Decl TopLevel (Decl PName)
topLevelDecl { tlValue :: Decl PName
tlValue = Decl PName
d } | Decl PName
d <- [Decl PName]
ds ]
DModule TopLevel (NestedModule PName)
tl | NestedModule ModuleG PName PName
m <- forall a. TopLevel a -> a
tlValue TopLevel (NestedModule PName)
tl ->
do ModuleG PName PName
m1 <- forall mname.
ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName)
expandPropGuards ModuleG PName PName
m
forall (f :: * -> *) a. Applicative f => a -> f a
pure [forall name. TopLevel (NestedModule name) -> TopDecl name
DModule TopLevel (NestedModule PName)
tl { tlValue :: NestedModule PName
tlValue = forall name. ModuleG name name -> NestedModule name
NestedModule ModuleG PName PName
m1 }]
TopDecl PName
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [TopDecl PName
topDecl]
expandDecl :: Decl PName -> ExpandPropGuardsM [Decl PName]
expandDecl :: Decl PName -> ExpandPropGuardsM [Decl PName]
expandDecl Decl PName
decl =
case Decl PName
decl of
DBind Bind PName
bind -> do [Bind PName]
bs <- Bind PName -> ExpandPropGuardsM [Bind PName]
expandBind Bind PName
bind
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a -> b) -> [a] -> [b]
map forall name. Bind name -> Decl name
DBind [Bind PName]
bs)
Decl PName
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [Decl PName
decl]
expandBind :: Bind PName -> ExpandPropGuardsM [Bind PName]
expandBind :: Bind PName -> ExpandPropGuardsM [Bind PName]
expandBind Bind PName
bind =
case forall a. Located a -> a
thing (forall name. Bind name -> Located (BindDef name)
bDef Bind PName
bind) of
DPropGuards [PropGuardCase PName]
guards -> do
Forall [TParam PName]
params [Prop PName]
props Type PName
t Maybe Range
rng <-
case forall name. Bind name -> Maybe (Schema name)
bSignature Bind PName
bind of
Just Schema PName
schema -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Schema PName
schema
Maybe (Schema PName)
Nothing -> forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located PName -> Error
NoSignature forall a b. (a -> b) -> a -> b
$ forall name. Bind name -> Located name
bName Bind PName
bind
let goGuard ::
PropGuardCase PName ->
ExpandPropGuardsM (PropGuardCase PName, Bind PName)
goGuard :: PropGuardCase PName
-> ExpandPropGuardsM (PropGuardCase PName, Bind PName)
goGuard (PropGuardCase [Located (Prop PName)]
props' Expr PName
e) = do
Located PName
bName' <- Located PName -> [Prop PName] -> ExpandPropGuardsM (Located PName)
newName (forall name. Bind name -> Located name
bName Bind PName
bind) (forall a. Located a -> a
thing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located (Prop PName)]
props')
[TParam PName]
tParams <- case forall name. Bind name -> Maybe (Schema name)
bSignature Bind PName
bind of
Just (Forall [TParam PName]
tps [Prop PName]
_ Type PName
_ Maybe Range
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [TParam PName]
tps
Maybe (Schema PName)
Nothing -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Located PName -> Error
NoSignature (forall name. Bind name -> Located name
bName Bind PName
bind)
[TypeInst PName]
typeInsts <-
(\(TParam PName
n Maybe Kind
_ Maybe Range
_) -> forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall name. Type name -> TypeInst name
PosInst forall a b. (a -> b) -> a -> b
$ forall n. n -> [Type n] -> Type n
TUser PName
n [])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [TParam PName]
tParams
let e' :: Expr PName
e' = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall n. Expr n -> Expr n -> Expr n
EApp (forall n. Expr n -> [TypeInst n] -> Expr n
EAppT (forall n. n -> Expr n
EVar forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
thing Located PName
bName') [TypeInst PName]
typeInsts) (Pattern PName -> Expr PName
patternToExpr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall name. Bind name -> [Pattern name]
bParams Bind PName
bind)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( forall name.
[Located (Prop name)] -> Expr name -> PropGuardCase name
PropGuardCase [Located (Prop PName)]
props' Expr PName
e',
Bind PName
bind
{ bName :: Located PName
bName = Located PName
bName',
bSignature :: Maybe (Schema PName)
bSignature = forall a. a -> Maybe a
Just (forall n.
[TParam n] -> [Prop n] -> Type n -> Maybe Range -> Schema n
Forall [TParam PName]
params
([Prop PName]
props forall a. Semigroup a => a -> a -> a
<> forall a b. (a -> b) -> [a] -> [b]
map forall a. Located a -> a
thing [Located (Prop PName)]
props')
Type PName
t Maybe Range
rng),
bDef :: Located (BindDef PName)
bDef = (forall name. Bind name -> Located (BindDef name)
bDef Bind PName
bind) {thing :: BindDef PName
thing = forall name. Expr name -> BindDef name
DExpr Expr PName
e}
}
)
([PropGuardCase PName]
guards', [Bind PName]
binds') <- forall a b. [(a, b)] -> ([a], [b])
unzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PropGuardCase PName
-> ExpandPropGuardsM (PropGuardCase PName, Bind PName)
goGuard [PropGuardCase PName]
guards
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
Bind PName
bind {bDef :: Located (BindDef PName)
bDef = forall name. [PropGuardCase name] -> BindDef name
DPropGuards [PropGuardCase PName]
guards' forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall name. Bind name -> Located (BindDef name)
bDef Bind PName
bind} forall a. a -> [a] -> [a]
:
[Bind PName]
binds'
BindDef PName
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure [Bind PName
bind]
patternToExpr :: Pattern PName -> Expr PName
patternToExpr :: Pattern PName -> Expr PName
patternToExpr (PVar Located PName
locName) = forall n. n -> Expr n
EVar (forall a. Located a -> a
thing Located PName
locName)
patternToExpr Pattern PName
_ =
forall a. HasCallStack => String -> [String] -> a
panic String
"patternToExpr"
[String
"Unimplemented: patternToExpr of anything other than PVar"]
newName :: Located PName -> [Prop PName] -> ExpandPropGuardsM (Located PName)
newName :: Located PName -> [Prop PName] -> ExpandPropGuardsM (Located PName)
newName Located PName
locName [Prop PName]
props =
forall (f :: * -> *) a. Applicative f => a -> f a
pure case forall a. Located a -> a
thing Located PName
locName of
Qual ModName
modName Ident
ident ->
let txt :: Text
txt = Ident -> Text
identText Ident
ident
txt' :: Text
txt' = String -> Text
pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. PP a => a -> Doc
pp [Prop PName]
props
in ModName -> Ident -> PName
Qual ModName
modName (Text -> Ident
mkIdent forall a b. (a -> b) -> a -> b
$ Text
txt forall a. Semigroup a => a -> a -> a
<> Text
txt') forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located PName
locName
UnQual Ident
ident ->
let txt :: Text
txt = Ident -> Text
identText Ident
ident
txt' :: Text
txt' = String -> Text
pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. PP a => a -> Doc
pp [Prop PName]
props
in Ident -> PName
UnQual (Text -> Ident
mkIdent forall a b. (a -> b) -> a -> b
$ Text
txt forall a. Semigroup a => a -> a -> a
<> Text
txt') forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located PName
locName
NewName Pass
_ Int
_ ->
forall a. HasCallStack => String -> [String] -> a
panic String
"mkName"
[ String
"During expanding prop guards"
, String
"tried to make new name from NewName case of PName"
]