    {-# 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 :: 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    -> [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 :: Decl PName
    tlValue = Decl PName
    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 PName
    tlValue = ModuleG PName PName -> NestedModule PName
    forall name. ModuleG name name -> NestedModule name
    NestedModule ModuleG PName PName
    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
        DPropGuards [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 :: Located PName
    bName = Located PName
    bName',
                        -- include guarded props in signature
                        bSignature :: Maybe (Schema PName)
    bSignature = Schema PName -> Maybe (Schema PName)
    forall a. a -> Maybe a
    Just ([TParam PName]
    -> [Prop PName] -> Type PName -> Maybe Range -> Schema PName
    forall n.
    [TParam n] -> [Prop n] -> Type n -> Maybe Range -> Schema n
    Forall [TParam PName]
    params
                                             ([Prop PName]
    props [Prop PName] -> [Prop PName] -> [Prop PName]
    forall a. Semigroup a => a -> a -> a
    <> (Located (Prop PName) -> Prop PName)
    -> [Located (Prop PName)] -> [Prop PName]
    forall a b. (a -> b) -> [a] -> [b]
    map Located (Prop PName) -> Prop PName
    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 = (Bind PName -> Located (BindDef PName)
    forall name. Bind name -> Located (BindDef name)
    bDef Bind PName
    bind) {thing :: BindDef PName
    thing = Expr PName -> BindDef PName
    forall name. Expr name -> BindDef name
    DExpr Expr PName
    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 :: Located (BindDef PName)
    bDef = [PropGuardCase PName] -> BindDef PName
    forall name. [PropGuardCase name] -> BindDef name
    DPropGuards [PropGuardCase PName]
    guards' BindDef PName -> Located (BindDef PName) -> Located (BindDef PName)
    forall a b. a -> Located b -> Located a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Bind PName -> Located (BindDef PName)
    forall name. Bind name -> Located (BindDef name)
    bDef Bind PName
    bind} Bind PName -> [Bind PName] -> [Bind PName]
    forall a. a -> [a] -> [a]
    :
            [Bind PName]
    binds'
        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]

    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"
            ]