    -- |
    -- Module      :  Cryptol.Parser.Selector
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE Safe #-}

    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE OverloadedStrings #-}
    module Cryptol.Parser.Selector
      ( Selector(..)
      , ppSelector
      , ppNestedSels
      , selName
      ) where

    import GHC.Generics (Generic)
    import Control.DeepSeq
    import Data.List(intersperse)

    import Cryptol.Utils.Ident
    import Cryptol.Utils.PP

    {- | Selectors are used for projecting from various components.
    Each selector has an option spec to specify the shape of the thing
    that is being selected.  Currently, there is no surface syntax for
    list selectors, but they are used during the desugaring of patterns.
    -}

    data Selector = TupleSel Int   (Maybe Int)
                    -- ^ Zero-based tuple selection.
                    -- Optionally specifies the shape of the tuple (one-based).

                  | RecordSel Ident (Maybe [Ident])
                    -- ^ Record selection.
                    -- Optionally specifies the shape of the record.

                  | ListSel Int    (Maybe Int)
                    -- ^ List selection.
                    -- Optionally specifies the length of the list.
                    deriving (Selector -> Selector -> Bool
    (Selector -> Selector -> Bool)
    -> (Selector -> Selector -> Bool) -> Eq Selector
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Selector -> Selector -> Bool
    $c/= :: Selector -> Selector -> Bool
    == :: Selector -> Selector -> Bool
    $c== :: Selector -> Selector -> Bool
    Eq, Int -> Selector -> ShowS
    [Selector] -> ShowS
    Selector -> String
    (Int -> Selector -> ShowS)
    -> (Selector -> String) -> ([Selector] -> ShowS) -> Show Selector
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Selector] -> ShowS
    $cshowList :: [Selector] -> ShowS
    show :: Selector -> String
    $cshow :: Selector -> String
    showsPrec :: Int -> Selector -> ShowS
    $cshowsPrec :: Int -> Selector -> ShowS
    Show, Eq Selector
    Eq Selector =>
    (Selector -> Selector -> Ordering)
    -> (Selector -> Selector -> Bool)
    -> (Selector -> Selector -> Bool)
    -> (Selector -> Selector -> Bool)
    -> (Selector -> Selector -> Bool)
    -> (Selector -> Selector -> Selector)
    -> (Selector -> Selector -> Selector)
    -> Ord Selector
    Selector -> Selector -> Bool
    Selector -> Selector -> Ordering
    Selector -> Selector -> Selector
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Selector -> Selector -> Selector
    $cmin :: Selector -> Selector -> Selector
    max :: Selector -> Selector -> Selector
    $cmax :: Selector -> Selector -> Selector
    >= :: Selector -> Selector -> Bool
    $c>= :: Selector -> Selector -> Bool
    > :: Selector -> Selector -> Bool
    $c> :: Selector -> Selector -> Bool
    <= :: Selector -> Selector -> Bool
    $c<= :: Selector -> Selector -> Bool
    < :: Selector -> Selector -> Bool
    $c< :: Selector -> Selector -> Bool
    compare :: Selector -> Selector -> Ordering
    $ccompare :: Selector -> Selector -> Ordering
    $cp1Ord :: Eq Selector
    Ord, (forall x. Selector -> Rep Selector x)
    -> (forall x. Rep Selector x -> Selector) -> Generic Selector
    forall x. Rep Selector x -> Selector
    forall x. Selector -> Rep Selector x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep Selector x -> Selector
    $cfrom :: forall x. Selector -> Rep Selector x
    Generic, Selector -> ()
    (Selector -> ()) -> NFData Selector
    forall a. (a -> ()) -> NFData a
    rnf :: Selector -> ()
    $crnf :: Selector -> ()
    NFData)

    instance PP Selector where
      ppPrec :: Int -> Selector -> Doc
    ppPrec _ sel :: Selector
    sel =
        case Selector
    sel of
          TupleSel x :: Int
    x sig :: Maybe Int
    sig    -> Int -> Doc
    int Int
    x Doc -> Doc -> Doc
    <+> (Int -> Doc) -> Maybe Int -> Doc
    forall t. (t -> Doc) -> Maybe t -> Doc
    ppSig Int -> Doc
    tupleSig Maybe Int
    sig
          RecordSel x :: Ident
    x sig :: Maybe [Ident]
    sig  -> Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    x  Doc -> Doc -> Doc
    <+> ([Ident] -> Doc) -> Maybe [Ident] -> Doc
    forall t. (t -> Doc) -> Maybe t -> Doc
    ppSig [Ident] -> Doc
    forall a. PP a => [a] -> Doc
    recordSig Maybe [Ident]
    sig
          ListSel x :: Int
    x sig :: Maybe Int
    sig    -> Int -> Doc
    int Int
    x Doc -> Doc -> Doc
    <+> (Int -> Doc) -> Maybe Int -> Doc
    forall t. (t -> Doc) -> Maybe t -> Doc
    ppSig Int -> Doc
    listSig Maybe Int
    sig

        where
        tupleSig :: Int -> Doc
    tupleSig n :: Int
    n   = Int -> Doc
    int Int
    n
        recordSig :: [a] -> Doc
    recordSig xs :: [a]
    xs = Doc -> Doc
    braces (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    fsep ([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
    $ (a -> Doc) -> [a] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Doc
    forall a. PP a => a -> Doc
    pp [a]
    xs
        listSig :: Int -> Doc
    listSig n :: Int
    n    = Int -> Doc
    int Int
    n

        ppSig :: (t -> Doc) -> Maybe t -> Doc
    ppSig f :: t -> Doc
    f = Doc -> (t -> Doc) -> Maybe t -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    empty (\x :: t
    x -> String -> Doc
    text "/* of" Doc -> Doc -> Doc
    <+> t -> Doc
    f t
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text "*/")

    -- | Display the thing selected by the selector, nicely.
    ppSelector :: Selector -> Doc
    ppSelector :: Selector -> Doc
    ppSelector sel :: Selector
    sel =
      case Selector
    sel of
        TupleSel x :: Int
    x _  -> Int -> Doc
    forall a. (Integral a, Show a, Eq a) => a -> Doc
    ordinal (Int
    xInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +1) Doc -> Doc -> Doc
    <+> String -> Doc
    text "field"
        RecordSel x :: Ident
    x _ -> String -> Doc
    text "field" Doc -> Doc -> Doc
    <+> Ident -> Doc
    forall a. PP a => a -> Doc
    pp Ident
    x
        ListSel x :: Int
    x _   -> Int -> Doc
    forall a. (Integral a, Show a, Eq a) => a -> Doc
    ordinal Int
    x Doc -> Doc -> Doc
    <+> String -> Doc
    text "element"

    -- | The name of a selector (e.g., used in update code)
    selName :: Selector -> Ident
    selName :: Selector -> Ident
    selName s :: Selector
    s =
      case Selector
    s of
        RecordSel i :: Ident
    i _ -> Ident
    i
        TupleSel n :: Int
    n _  -> String -> Ident
    packIdent ("_" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n)
        ListSel n :: Int
    n _   -> String -> Ident
    packIdent ("__" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n)

    -- | Show a list of selectors as they appear in a nested selector in an update.
    ppNestedSels :: [Selector] -> Doc
    ppNestedSels :: [Selector] -> Doc
    ppNestedSels = [Doc] -> Doc
    hcat ([Doc] -> Doc) -> ([Selector] -> [Doc]) -> [Selector] -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    intersperse "." ([Doc] -> [Doc]) -> ([Selector] -> [Doc]) -> [Selector] -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Selector -> Doc) -> [Selector] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Selector -> Doc
    ppS
      where ppS :: Selector -> Doc
    ppS s :: Selector
    s = case Selector
    s of
                      RecordSel i :: Ident
    i _ -> String -> Doc
    text (Ident -> String
    unpackIdent Ident
    i)
                      TupleSel n :: Int
    n _ -> Int -> Doc
    int Int
    n
                      ListSel n :: Int
    n _  -> Doc -> Doc
    brackets (Int -> Doc
    int Int
    n) -- not in source