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