{-# 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 -> (forall n. Type n -> Range -> Type n
`TLocated` Range
r) 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 forall a. Eq a => a -> a -> Bool
== Ident
widthIdent -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall n. n -> [Type n] -> Type n
TUser PName
n [])
| PName -> Ident
getIdent PName
n forall a. Eq a => a -> a -> Bool
== Ident
underIdent -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall n. Type n
TWild
EVar PName
x -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> [Type n] -> Type n
TUser PName
x [])
ELit Literal
x -> 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
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
forall (m :: * -> *) a. Monad m => a -> m a
return (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
forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. Type n -> Maybe Kind -> Type n
TParens Type PName
t forall a. Maybe a
Nothing)
Expr 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 -> (forall n. Type n -> Range -> Type n
`TLocated` Range
r) 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> [Type n] -> Type n
TUser n
f ([Type n]
ts forall a. [a] -> [a] -> [a]
++ [Type n
t]))
Type n
_ -> forall a. Maybe a
Nothing
cvtLit :: Literal -> Maybe (Type n)
cvtLit (ECNum Integer
n NumInfo
_) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. Integer -> Type n
TNum Integer
n)
cvtLit (ECChar Char
c) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. Char -> Type n
TChar Char
c)
cvtLit (ECFrac {}) = forall a. Maybe a
Nothing
cvtLit (ECString String
_) = forall a. Maybe a
Nothing