    -- |
    -- 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 #-}

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

    import Cryptol.Parser.AST

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

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

    translateExprToNumT :: Expr PName -> Maybe (Type PName)
    translateExprToNumT :: Expr PName -> Maybe (Type PName)
    translateExprToNumT expr :: Expr PName
    expr =
      case Expr PName
    expr of
        ELocated e :: Expr PName
    e r :: 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 (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Expr PName -> Maybe (Type PName)
    translateExprToNumT Expr PName
    e
        EVar n :: 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 (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 (f :: * -> *) a. Applicative f => a -> f a
    pure Type PName
    forall n. Type n
    TWild
        EVar x :: PName
    x       -> Type PName -> Maybe (Type PName)
    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 x :: Literal
    x       -> Literal -> Maybe (Type PName)
    forall n. Literal -> Maybe (Type n)
    cvtLit Literal
    x
        EApp e1 :: Expr PName
    e1 e2 :: 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 a :: Expr PName
    a o :: Located PName
    o f :: Fixity
    f b :: 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 (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 e :: Expr PName
    e    -> do Type PName
    t <- Expr PName -> Maybe (Type PName)
    translateExprToNumT Expr PName
    e
                           Type PName -> Maybe (Type PName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type PName -> Type PName
    forall n. Type n -> Type n
    TParens Type PName
    t)

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

      where
      tApp :: Type n -> Type n -> Maybe (Type n)
    tApp ty :: Type n
    ty t :: Type n
    t =
        case Type n
    ty of
          TLocated t1 :: Type n
    t1 r :: 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 (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 f :: n
    f ts :: [Type n]
    ts    -> Type n -> Maybe (Type n)
    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]))
          _             -> Maybe (Type n)
    forall a. Maybe a
    Nothing

      cvtLit :: Literal -> Maybe (Type n)
    cvtLit (ECNum n :: Integer
    n CharLit)  = Type n -> Maybe (Type n)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Char -> Type n
    forall n. Char -> Type n
    TChar (Char -> Type n) -> Char -> Type n
    forall a b. (a -> b) -> a -> b
    $ Int -> Char
    forall a. Enum a => Int -> a
    toEnum (Int -> Char) -> Int -> Char
    forall a b. (a -> b) -> a -> b
    $ Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    n)
      cvtLit (ECNum n :: Integer
    n _)        = Type n -> Maybe (Type n)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Integer -> Type n
    forall n. Integer -> Type n
    TNum Integer
    n)
      cvtLit (ECString _)       = Maybe (Type n)
    forall a. Maybe a
    Nothing