    -- |
    -- Module      :  Cryptol.Parser.Utils
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable
    --
    -- Utility functions that are also useful for translating programs
    -- from previous Cryptol versions.

    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE Safe #-}

    module Cryptol.Parser.Utils
      ( translateExprToNumT
      , widthIdent
      ) where

    import Cryptol.Parser.AST

    widthIdent :: Ident
    widthIdent :: Ident
    widthIdent  = Text -> Ident
    mkIdent Text
    "width"

    underIdent :: Ident
    underIdent :: Ident
    underIdent = Text -> Ident
    mkIdent Text
    "_"

    translateExprToNumT :: Expr PName -> Maybe (Type PName)
    translateExprToNumT :: Expr PName -> Maybe (Type PName)
    translateExprToNumT Expr PName
    expr =
      case Expr PName
    expr of
        ELocated Expr PName
    e Range
    r -> (Type PName -> Range -> Type PName
    forall n. Type n -> Range -> Type n
    `TLocated` Range
    r) (Type PName -> Type PName)
    -> Maybe (Type PName) -> Maybe (Type PName)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Expr PName -> Maybe (Type PName)
    translateExprToNumT Expr PName
    e
        EVar PName
    n | PName -> Ident
    getIdent PName
    n Ident -> Ident -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ident
    widthIdent -> Type PName -> Maybe (Type PName)
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (PName -> [Type PName] -> Type PName
    forall n. n -> [Type n] -> Type n
    TUser PName
    n [])
               | PName -> Ident
    getIdent PName
    n Ident -> Ident -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ident
    underIdent -> Type PName -> Maybe (Type PName)
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Type PName
    forall n. Type n
    TWild
        EVar PName
    x       -> Type PName -> Maybe (Type PName)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PName -> [Type PName] -> Type PName
    forall n. n -> [Type n] -> Type n
    TUser PName
    x [])
        ELit Literal
    x       -> Literal -> Maybe (Type PName)
    forall {n}. Literal -> Maybe (Type n)
    cvtLit Literal
    x
        EApp Expr PName
    e1 Expr PName
    e2   -> do Type PName
    t1 <- Expr PName -> Maybe (Type PName)
    translateExprToNumT Expr PName
    e1
                           Type PName
    t2 <- Expr PName -> Maybe (Type PName)
    translateExprToNumT Expr PName
    e2
                           Type PName -> Type PName -> Maybe (Type PName)
    forall {n}. Type n -> Type n -> Maybe (Type n)
    tApp Type PName
    t1 Type PName
    t2

        EInfix Expr PName
    a Located PName
    o Fixity
    f Expr PName
    b -> do Type PName
    e1 <- Expr PName -> Maybe (Type PName)
    translateExprToNumT Expr PName
    a
                             Type PName
    e2 <- Expr PName -> Maybe (Type PName)
    translateExprToNumT Expr PName
    b
                             Type PName -> Maybe (Type PName)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type PName -> Located PName -> Fixity -> Type PName -> Type PName
    forall n. Type n -> Located n -> Fixity -> Type n -> Type n
    TInfix Type PName
    e1 Located PName
    o Fixity
    f Type PName
    e2)

        EParens Expr PName
    e    -> do Type PName
    t <- Expr PName -> Maybe (Type PName)
    translateExprToNumT Expr PName
    e
                           Type PName -> Maybe (Type PName)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type PName -> Maybe Kind -> Type PName
    forall n. Type n -> Maybe Kind -> Type n
    TParens Type PName
    t Maybe Kind
    forall a. Maybe a
    Nothing)

        Expr PName
    _            -> Maybe (Type PName)
    forall a. Maybe a
    Nothing

      where
      tApp :: Type n -> Type n -> Maybe (Type n)
    tApp Type n
    ty Type n
    t =
        case Type n
    ty of
          TLocated Type n
    t1 Range
    r -> (Type n -> Range -> Type n
    forall n. Type n -> Range -> Type n
    `TLocated` Range
    r) (Type n -> Type n) -> Maybe (Type n) -> Maybe (Type n)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Type n -> Type n -> Maybe (Type n)
    tApp Type n
    t1 Type n
    t
          TUser n
    f [Type n]
    ts    -> Type n -> Maybe (Type n)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (n -> [Type n] -> Type n
    forall n. n -> [Type n] -> Type n
    TUser n
    f ([Type n]
    ts [Type n] -> [Type n] -> [Type n]
    forall a. [a] -> [a] -> [a]
    ++ [Type n
    t]))
          Type n
    _             -> Maybe (Type n)
    forall a. Maybe a
    Nothing

      cvtLit :: Literal -> Maybe (Type n)
    cvtLit (ECNum Integer
    n NumInfo
    _)        = Type n -> Maybe (Type n)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Type n
    forall n. Integer -> Type n
    TNum Integer
    n)
      cvtLit (ECChar Char
    c)         = Type n -> Maybe (Type n)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Char -> Type n
    forall n. Char -> Type n
    TChar Char
    c)
      cvtLit (ECFrac {})        = Maybe (Type n)
    forall a. Maybe a
    Nothing
      cvtLit (ECString String
    _)       = Maybe (Type n)
    forall a. Maybe a
    Nothing