{-# 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
(Int -> Error -> ShowS)
-> (Error -> String) -> ([Error] -> ShowS) -> Show Error
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Error -> ShowS
showsPrec :: Int -> Error -> ShowS
$cshow :: Error -> String
show :: Error -> String
$cshowList :: [Error] -> ShowS
showList :: [Error] -> ShowS
Show, (forall x. Error -> Rep Error x)
-> (forall x. Rep Error x -> Error) -> Generic Error
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
$cfrom :: forall x. Error -> Rep Error x
from :: forall x. Error -> Rep Error x
$cto :: forall x. Rep Error x -> Error
to :: forall x. Rep Error x -> Error
Generic, Error -> ()
(Error -> ()) -> NFData Error
forall a. (a -> ()) -> NFData a
$crnf :: Error -> ()
rnf :: 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
<+> Range -> Doc
forall a. PP a => a -> Doc
pp (Located PName -> Range
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 (ModuleG mname PName -> ModuleDefinition PName
forall mname name. ModuleG mname name -> ModuleDefinition name
mDef ModuleG mname PName
m)
     ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName)
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleG mname PName
m { mDef = 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    -> [TopDecl PName] -> ModuleDefinition PName
forall name. [TopDecl name] -> ModuleDefinition name
NormalModule ([TopDecl PName] -> ModuleDefinition PName)
-> ([[TopDecl PName]] -> [TopDecl PName])
-> [[TopDecl PName]]
-> ModuleDefinition PName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[TopDecl PName]] -> [TopDecl PName]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[TopDecl PName]] -> ModuleDefinition PName)
-> Either Error [[TopDecl PName]]
-> ExpandPropGuardsM (ModuleDefinition PName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TopDecl PName -> Either Error [TopDecl PName])
-> [TopDecl PName] -> Either Error [[TopDecl PName]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TopDecl PName -> Either Error [TopDecl PName]
expandTopDecl [TopDecl PName]
ds
    FunctorInstance {} -> ModuleDefinition PName
-> ExpandPropGuardsM (ModuleDefinition PName)
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleDefinition PName
m
    InterfaceModule {} -> ModuleDefinition PName
-> ExpandPropGuardsM (ModuleDefinition PName)
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ModuleDefinition PName
m

expandTopDecl :: TopDecl PName -> ExpandPropGuardsM [TopDecl PName]
expandTopDecl :: TopDecl PName -> Either Error [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 (TopLevel (Decl PName) -> Decl PName
forall a. TopLevel a -> a
tlValue TopLevel (Decl PName)
topLevelDecl)
         [TopDecl PName] -> Either Error [TopDecl PName]
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ TopLevel (Decl PName) -> TopDecl PName
forall name. TopLevel (Decl name) -> TopDecl name
Decl TopLevel (Decl PName)
topLevelDecl { tlValue = d } | Decl PName
d <- [Decl PName]
ds ]

    DModule TopLevel (NestedModule PName)
tl | NestedModule ModuleG PName PName
m <- TopLevel (NestedModule PName) -> NestedModule PName
forall a. TopLevel a -> a
tlValue TopLevel (NestedModule PName)
tl ->
      do ModuleG PName PName
m1 <- ModuleG PName PName -> ExpandPropGuardsM (ModuleG PName PName)
forall mname.
ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName)
expandPropGuards ModuleG PName PName
m
         [TopDecl PName] -> Either Error [TopDecl PName]
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [TopLevel (NestedModule PName) -> TopDecl PName
forall name. TopLevel (NestedModule name) -> TopDecl name
DModule TopLevel (NestedModule PName)
tl { tlValue = NestedModule m1 }]

    TopDecl PName
_ -> [TopDecl PName] -> Either Error [TopDecl PName]
forall a. a -> Either Error a
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
                     [Decl PName] -> ExpandPropGuardsM [Decl PName]
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Bind PName -> Decl PName) -> [Bind PName] -> [Decl PName]
forall a b. (a -> b) -> [a] -> [b]
map Bind PName -> Decl PName
forall name. Bind name -> Decl name
DBind [Bind PName]
bs)
    Decl PName
_          -> [Decl PName] -> ExpandPropGuardsM [Decl PName]
forall a. a -> Either Error a
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 Located (BindDef PName) -> BindDef PName
forall a. Located a -> a
thing (Bind PName -> Located (BindDef PName)
forall name. Bind name -> Located (BindDef name)
bDef Bind PName
bind) of
    DImpl (DPropGuards [PropGuardCase PName]
guards) -> ([PropGuardCase PName] -> BindDef PName)
-> [PropGuardCase PName] -> ExpandPropGuardsM [Bind PName]
expand (BindImpl PName -> BindDef PName
forall name. BindImpl name -> BindDef name
DImpl (BindImpl PName -> BindDef PName)
-> ([PropGuardCase PName] -> BindImpl PName)
-> [PropGuardCase PName]
-> BindDef PName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [PropGuardCase PName] -> BindImpl PName
forall name. [PropGuardCase name] -> BindImpl name
DPropGuards) [PropGuardCase PName]
guards
    DForeign (Just (DPropGuards [PropGuardCase PName]
guards)) -> ([PropGuardCase PName] -> BindDef PName)
-> [PropGuardCase PName] -> ExpandPropGuardsM [Bind PName]
expand (Maybe (BindImpl PName) -> BindDef PName
forall name. Maybe (BindImpl name) -> BindDef name
DForeign (Maybe (BindImpl PName) -> BindDef PName)
-> ([PropGuardCase PName] -> Maybe (BindImpl PName))
-> [PropGuardCase PName]
-> BindDef PName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindImpl PName -> Maybe (BindImpl PName)
forall a. a -> Maybe a
Just (BindImpl PName -> Maybe (BindImpl PName))
-> ([PropGuardCase PName] -> BindImpl PName)
-> [PropGuardCase PName]
-> Maybe (BindImpl PName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [PropGuardCase PName] -> BindImpl PName
forall name. [PropGuardCase name] -> BindImpl name
DPropGuards) [PropGuardCase PName]
guards
    BindDef PName
_ -> [Bind PName] -> ExpandPropGuardsM [Bind PName]
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Bind PName
bind]

  where
  expand :: ([PropGuardCase PName] -> BindDef PName)
-> [PropGuardCase PName] -> ExpandPropGuardsM [Bind PName]
expand [PropGuardCase PName] -> BindDef PName
def [PropGuardCase PName]
guards = do
    Forall [TParam PName]
params [Prop PName]
props Type PName
t Maybe Range
rng <-
      case Bind PName -> Maybe (Schema PName)
forall name. Bind name -> Maybe (Schema name)
bSignature Bind PName
bind of
        Just Schema PName
schema -> Schema PName -> Either Error (Schema PName)
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Schema PName
schema
        Maybe (Schema PName)
Nothing -> Error -> Either Error (Schema PName)
forall a b. a -> Either a b
Left (Error -> Either Error (Schema PName))
-> (Located PName -> Error)
-> Located PName
-> Either Error (Schema PName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located PName -> Error
NoSignature (Located PName -> Either Error (Schema PName))
-> Located PName -> Either Error (Schema PName)
forall a b. (a -> b) -> a -> b
$ Bind PName -> Located PName
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 (Bind PName -> Located PName
forall name. Bind name -> Located name
bName Bind PName
bind) (Located (Prop PName) -> Prop PName
forall a. Located a -> a
thing (Located (Prop PName) -> Prop PName)
-> [Located (Prop PName)] -> [Prop PName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located (Prop PName)]
props')
          -- call to generated function
          [TParam PName]
tParams <- case Bind PName -> Maybe (Schema PName)
forall name. Bind name -> Maybe (Schema name)
bSignature Bind PName
bind of
            Just (Forall [TParam PName]
tps [Prop PName]
_ Type PName
_ Maybe Range
_) -> [TParam PName] -> Either Error [TParam PName]
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [TParam PName]
tps
            Maybe (Schema PName)
Nothing -> Error -> Either Error [TParam PName]
forall a b. a -> Either a b
Left (Error -> Either Error [TParam PName])
-> Error -> Either Error [TParam PName]
forall a b. (a -> b) -> a -> b
$ Located PName -> Error
NoSignature (Bind PName -> Located PName
forall name. Bind name -> Located name
bName Bind PName
bind)
          [TypeInst PName]
typeInsts <-
            (\(TParam PName
n Maybe Kind
_ Maybe Range
_) -> TypeInst PName -> Either Error (TypeInst PName)
forall a b. b -> Either a b
Right (TypeInst PName -> Either Error (TypeInst PName))
-> (Type PName -> TypeInst PName)
-> Type PName
-> Either Error (TypeInst PName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type PName -> TypeInst PName
forall name. Type name -> TypeInst name
PosInst (Type PName -> Either Error (TypeInst PName))
-> Type PName -> Either Error (TypeInst PName)
forall a b. (a -> b) -> a -> b
$ PName -> [Type PName] -> Type PName
forall n. n -> [Type n] -> Type n
TUser PName
n [])
              (TParam PName -> Either Error (TypeInst PName))
-> [TParam PName] -> Either Error [TypeInst PName]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
`traverse` [TParam PName]
tParams
          let e' :: Expr PName
e' = (Expr PName -> Expr PName -> Expr PName)
-> Expr PName -> [Expr PName] -> Expr PName
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr PName -> Expr PName -> Expr PName
forall n. Expr n -> Expr n -> Expr n
EApp (Expr PName -> [TypeInst PName] -> Expr PName
forall n. Expr n -> [TypeInst n] -> Expr n
EAppT (PName -> Expr PName
forall n. n -> Expr n
EVar (PName -> Expr PName) -> PName -> Expr PName
forall a b. (a -> b) -> a -> b
$ Located PName -> PName
forall a. Located a -> a
thing Located PName
bName') [TypeInst PName]
typeInsts) (Pattern PName -> Expr PName
patternToExpr (Pattern PName -> Expr PName) -> [Pattern PName] -> [Expr PName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bind PName -> [Pattern PName]
forall name. Bind name -> [Pattern name]
bParams Bind PName
bind)
          (PropGuardCase PName, Bind PName)
-> ExpandPropGuardsM (PropGuardCase PName, Bind PName)
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            ( [Located (Prop PName)] -> Expr PName -> PropGuardCase PName
forall name.
[Located (Prop name)] -> Expr name -> PropGuardCase name
PropGuardCase [Located (Prop PName)]
props' Expr PName
e',
              Bind PName
bind
                { bName = bName',
                  -- include guarded props in signature
                  bSignature = Just (Forall params
                                        (props <> map thing props')
                                        t rng),
                  -- keeps same location at original bind
                  -- i.e. "on top of" original bind
                  bDef = (bDef bind) {thing = exprDef e}
                }
            )
    ([PropGuardCase PName]
guards', [Bind PName]
binds') <- [(PropGuardCase PName, Bind PName)]
-> ([PropGuardCase PName], [Bind PName])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(PropGuardCase PName, Bind PName)]
 -> ([PropGuardCase PName], [Bind PName]))
-> Either Error [(PropGuardCase PName, Bind PName)]
-> Either Error ([PropGuardCase PName], [Bind PName])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PropGuardCase PName
 -> ExpandPropGuardsM (PropGuardCase PName, Bind PName))
-> [PropGuardCase PName]
-> Either Error [(PropGuardCase PName, Bind PName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM PropGuardCase PName
-> ExpandPropGuardsM (PropGuardCase PName, Bind PName)
goGuard [PropGuardCase PName]
guards
    [Bind PName] -> ExpandPropGuardsM [Bind PName]
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Bind PName] -> ExpandPropGuardsM [Bind PName])
-> [Bind PName] -> ExpandPropGuardsM [Bind PName]
forall a b. (a -> b) -> a -> b
$
      Bind PName
bind {bDef = def guards' <$ bDef bind} Bind PName -> [Bind PName] -> [Bind PName]
forall a. a -> [a] -> [a]
:
      [Bind PName]
binds'

patternToExpr :: Pattern PName -> Expr PName
patternToExpr :: Pattern PName -> Expr PName
patternToExpr (PVar Located PName
locName) = PName -> Expr PName
forall n. n -> Expr n
EVar (Located PName -> PName
forall a. Located a -> a
thing Located PName
locName)
patternToExpr Pattern PName
_ =
  String -> [String] -> Expr 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 =
  Located PName -> ExpandPropGuardsM (Located PName)
forall a. a -> Either Error a
forall (f :: * -> *) a. Applicative f => a -> f a
pure case Located PName -> PName
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 (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ [Prop PName] -> Doc
forall a. PP a => a -> Doc
pp [Prop PName]
props
       in ModName -> Ident -> PName
Qual ModName
modName (Text -> Ident
mkIdent (Text -> Ident) -> Text -> Ident
forall a b. (a -> b) -> a -> b
$ Text
txt Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
txt') PName -> Located PName -> Located PName
forall a b. a -> Located b -> Located a
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 (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ [Prop PName] -> Doc
forall a. PP a => a -> Doc
pp [Prop PName]
props
       in Ident -> PName
UnQual (Text -> Ident
mkIdent (Text -> Ident) -> Text -> Ident
forall a b. (a -> b) -> a -> b
$ Text
txt Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
txt') PName -> Located PName -> Located PName
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located PName
locName
    NewName Pass
_ Int
_ ->
      String -> [String] -> Located PName
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"
        ]