{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}

-- |
-- Module      :  Cryptol.Parser.PropGuards
-- Copyright   :  (c) 2022 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
--
-- Expands PropGuards into a top-level definition for each case, and rewrites
-- the body of each case to be an appropriate call to the respectively generated
-- function.
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)

-- | Monad
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

-- | Error
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')
            -- call to generated function
            [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',
                    -- include guarded props in signature
                    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),
                    -- keeps same location at original bind
                    -- i.e. "on top of" original bind
                    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"
        ]