{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Safe #-}
-- | Abstract syntax for the fragment of Cryptol emitted by the Cryptol
--   backend (ReWire.Hyle.ToCryptol). The generated file is a
--   self-contained named module (Cryptol allows loading it under any file
--   name): a few helper definitions implementing Hyle primitives, an
--   optional @parameter@ block declaring externs as uninterpreted functions,
--   and one function per Hyle defn. Helper names contain a tick
--   (@rw'resize@) so they can never collide with generated names (see
--   'cryptolName').
module ReWire.Cryptol.Syntax where

import ReWire.BitVector (BV, width, nat)
import qualified ReWire.BitVector as BV
import ReWire.Pretty (empty, text, Pretty (..), parens, (<+>), vsep, hsep, punctuate, comma, nest, Doc, brackets)

import Data.Char (isAlphaNum, intToDigit)
import Data.List (intersperse)
import Data.Text (Text)
import Numeric (showHex, showIntAtBase)
import Numeric.Natural (Natural)

import qualified Data.Text as T

type Name = Text
type Size = Word

-- | Maps a Hyle name to a valid Cryptol identifier body: any character
--   outside @[A-Za-z0-9_]@ becomes an underscore. Callers are expected to
--   prepend a prefix (@rw_@), so the first character doesn't matter and the
--   result can never collide with a Cryptol keyword, a Prelude name, or the
--   tick-containing helper names. The one unprefixed use is the module name
--   ("ReWire.Hyle.ToCryptol" via 'modName'), where a keyword-named @--top@
--   would emit an invalid module header.
cryptolName :: Text -> Name
cryptolName :: Name -> Name
cryptolName = (Char -> Char) -> Name -> Name
T.map Char -> Char
sub
      where sub :: Char -> Char
            sub :: Char -> Char
sub Char
c | Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' = Char
c
                  | Bool
otherwise                = Char
'_'

data Module = Module
      { Module -> Name
modName     :: !Name    -- ^ Cryptol allows loading a file whose name doesn't match.
      , Module -> [Name]
modComments :: ![Text]  -- ^ Header comment lines.
      , Module -> [Param]
modParams   :: ![Param] -- ^ Externs, as uninterpreted functions.
      , Module -> [Defn]
modDefns    :: ![Defn]
      }
      deriving (Module -> Module -> Bool
(Module -> Module -> Bool)
-> (Module -> Module -> Bool) -> Eq Module
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Module -> Module -> Bool
== :: Module -> Module -> Bool
$c/= :: Module -> Module -> Bool
/= :: Module -> Module -> Bool
Eq, Int -> Module -> ShowS
[Module] -> ShowS
Module -> String
(Int -> Module -> ShowS)
-> (Module -> String) -> ([Module] -> ShowS) -> Show Module
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Module -> ShowS
showsPrec :: Int -> Module -> ShowS
$cshow :: Module -> String
show :: Module -> String
$cshowList :: [Module] -> ShowS
showList :: [Module] -> ShowS
Show)

instance Pretty Module where
      pretty :: forall ann. Module -> Doc ann
pretty (Module Name
n [Name]
comments [Param]
params [Defn]
defns) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
intersperse Doc ann
forall ann. Doc ann
empty
            ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$  [[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (Name -> Doc ann) -> [Name] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (\ Name
c -> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"//" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
c) [Name]
comments | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
comments]
            [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> [Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"module" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"where"]
            [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> [Doc ann
forall ann. Doc ann
helpers]
            [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> [[Param] -> Doc ann
forall an. [Param] -> Doc an
ppParams [Param]
params | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Param] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Param]
params]
            [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> (Defn -> Doc ann) -> [Defn] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Defn -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Defn -> Doc ann
pretty [Defn]
defns

-- | Helper definitions emitted with every module, implementing Hyle
--   primitives that don't map directly to a Cryptol operator. @rw'resize@
--   truncates or zero-extends to the new width.
helpers :: Doc an
helpers :: forall ann. Doc ann
helpers = [Doc an] -> Doc an
forall ann. [Doc ann] -> Doc ann
vsep ([Doc an] -> Doc an) -> [Doc an] -> Doc an
forall a b. (a -> b) -> a -> b
$ (Name -> Doc an) -> [Name] -> [Doc an]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc an
forall ann. Name -> Doc ann
text
      [ Name
"// Helpers implementing ReWire Hyle primitive semantics."
      , Name
"rw'resize : {m, n} (fin m, fin n) => [n] -> [m]"
      , Name
"rw'resize x = drop`{n} ((zero : [m]) # x)"
      , Name
""
      , Name
"rw'repl : {n, w} (fin n, fin w) => [w] -> [n * w]"
      , Name
"rw'repl x = join (repeat`{n} x)"
      , Name
""
      , Name
"rw'parity : {n} (fin n) => [n] -> Bit"
      , Name
"rw'parity x = foldr (^) False x"
      , Name
""
      , Name
"rw'sext : {m, n} (fin m, fin n, n >= 1) => [n] -> [m]"
      , Name
"rw'sext x = if x @ 0 then ~ (rw'resize (~ x)) else rw'resize x"
      ]

-- | An uninterpreted function declared in a @parameter@ block: name, argument
--   widths, result width.
data Param = Param !Name ![Size] !Size
      deriving (Param -> Param -> Bool
(Param -> Param -> Bool) -> (Param -> Param -> Bool) -> Eq Param
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Param -> Param -> Bool
== :: Param -> Param -> Bool
$c/= :: Param -> Param -> Bool
/= :: Param -> Param -> Bool
Eq, Int -> Param -> ShowS
[Param] -> ShowS
Param -> String
(Int -> Param -> ShowS)
-> (Param -> String) -> ([Param] -> ShowS) -> Show Param
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Param -> ShowS
showsPrec :: Int -> Param -> ShowS
$cshow :: Param -> String
show :: Param -> String
$cshowList :: [Param] -> ShowS
showList :: [Param] -> ShowS
Show)

ppParams :: [Param] -> Doc an
ppParams :: forall an. [Param] -> Doc an
ppParams [Param]
ps = Int -> Doc an -> Doc an
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc an -> Doc an) -> Doc an -> Doc an
forall a b. (a -> b) -> a -> b
$ [Doc an] -> Doc an
forall ann. [Doc ann] -> Doc ann
vsep ([Doc an] -> Doc an) -> [Doc an] -> Doc an
forall a b. (a -> b) -> a -> b
$ Name -> Doc an
forall ann. Name -> Doc ann
text Name
"parameter" Doc an -> [Doc an] -> [Doc an]
forall a. a -> [a] -> [a]
: (Param -> Doc an) -> [Param] -> [Doc an]
forall a b. (a -> b) -> [a] -> [b]
map Param -> Doc an
forall an. Param -> Doc an
ppParam [Param]
ps
      where ppParam :: Param -> Doc an
            ppParam :: forall an. Param -> Doc an
ppParam (Param Name
n [Size]
args Size
res) = Name -> Doc an
forall ann. Name -> Doc ann
text Name
n Doc an -> Doc an -> Doc an
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc an
forall ann. Name -> Doc ann
text Name
":" Doc an -> Doc an -> Doc an
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Ty] -> Ty -> Doc an
forall an. [Ty] -> Ty -> Doc an
ppFun ((Size -> Ty) -> [Size] -> [Ty]
forall a b. (a -> b) -> [a] -> [b]
map Size -> Ty
TBits [Size]
args) (Size -> Ty
TBits Size
res)

-- | Sequence lengths in types: the device's quantified variable @n@, or
--   @1 + n@.
data Len = LenVar | LenSucc
      deriving (Len -> Len -> Bool
(Len -> Len -> Bool) -> (Len -> Len -> Bool) -> Eq Len
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Len -> Len -> Bool
== :: Len -> Len -> Bool
$c/= :: Len -> Len -> Bool
/= :: Len -> Len -> Bool
Eq, Int -> Len -> ShowS
[Len] -> ShowS
Len -> String
(Int -> Len -> ShowS)
-> (Len -> String) -> ([Len] -> ShowS) -> Show Len
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Len -> ShowS
showsPrec :: Int -> Len -> ShowS
$cshow :: Len -> String
show :: Len -> String
$cshowList :: [Len] -> ShowS
showList :: [Len] -> ShowS
Show)

instance Pretty Len where
      pretty :: forall ann. Len -> Doc ann
pretty = \ case
            Len
LenVar  -> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"n"
            Len
LenSucc -> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"1 + n"

data Ty = TBits !Size    -- ^ > [w]
        | TSeq !Len !Ty  -- ^ > [n]t
      deriving (Ty -> Ty -> Bool
(Ty -> Ty -> Bool) -> (Ty -> Ty -> Bool) -> Eq Ty
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Ty -> Ty -> Bool
== :: Ty -> Ty -> Bool
$c/= :: Ty -> Ty -> Bool
/= :: Ty -> Ty -> Bool
Eq, Int -> Ty -> ShowS
[Ty] -> ShowS
Ty -> String
(Int -> Ty -> ShowS)
-> (Ty -> String) -> ([Ty] -> ShowS) -> Show Ty
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Ty -> ShowS
showsPrec :: Int -> Ty -> ShowS
$cshow :: Ty -> String
show :: Ty -> String
$cshowList :: [Ty] -> ShowS
showList :: [Ty] -> ShowS
Show)

instance Pretty Ty where
      pretty :: forall ann. Ty -> Doc ann
pretty = \ case
            TBits Size
w  -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Integer -> Doc ann) -> Integer -> Doc ann
forall a b. (a -> b) -> a -> b
$ Size -> Integer
forall a. Integral a => a -> Integer
toInteger Size
w
            TSeq Len
l Ty
t -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (Len -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Len -> Doc ann
pretty Len
l) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Ty -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Ty -> Doc ann
pretty Ty
t

ppFun :: [Ty] -> Ty -> Doc an
ppFun :: forall an. [Ty] -> Ty -> Doc an
ppFun [Ty]
args Ty
res = [Doc an] -> Doc an
forall ann. [Doc ann] -> Doc ann
hsep ([Doc an] -> Doc an) -> [Doc an] -> Doc an
forall a b. (a -> b) -> a -> b
$ Doc an -> [Doc an] -> [Doc an]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate (Name -> Doc an
forall ann. Name -> Doc ann
text Name
" ->") ([Doc an] -> [Doc an]) -> [Doc an] -> [Doc an]
forall a b. (a -> b) -> a -> b
$ (Ty -> Doc an) -> [Ty] -> [Doc an]
forall a b. (a -> b) -> [a] -> [b]
map Ty -> Doc an
forall a ann. Pretty a => a -> Doc ann
forall ann. Ty -> Doc ann
pretty ([Ty] -> [Doc an]) -> [Ty] -> [Doc an]
forall a b. (a -> b) -> a -> b
$ [Ty]
args [Ty] -> [Ty] -> [Ty]
forall a. Semigroup a => a -> a -> a
<> [Ty
res]

data Defn = Defn
      { Defn -> [Name]
defnComments :: ![Text]
      , Defn -> Name
defnName     :: !Name
      , Defn -> Bool
defnQuantN   :: !Bool -- ^ Prefix the signature with @{n} (fin n) =>@.
      , Defn -> [(Name, Ty)]
defnArgs     :: ![(Name, Ty)]
      , Defn -> Ty
defnResTy    :: !Ty
      , Defn -> Exp
defnBody     :: !Exp
      , Defn -> [Bind]
defnWhere    :: ![Bind]
      }
      deriving (Defn -> Defn -> Bool
(Defn -> Defn -> Bool) -> (Defn -> Defn -> Bool) -> Eq Defn
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Defn -> Defn -> Bool
== :: Defn -> Defn -> Bool
$c/= :: Defn -> Defn -> Bool
/= :: Defn -> Defn -> Bool
Eq, Int -> Defn -> ShowS
[Defn] -> ShowS
Defn -> String
(Int -> Defn -> ShowS)
-> (Defn -> String) -> ([Defn] -> ShowS) -> Show Defn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Defn -> ShowS
showsPrec :: Int -> Defn -> ShowS
$cshow :: Defn -> String
show :: Defn -> String
$cshowList :: [Defn] -> ShowS
showList :: [Defn] -> ShowS
Show)

instance Pretty Defn where
      pretty :: forall ann. Defn -> Doc ann
pretty (Defn [Name]
comments Name
n Bool
quantN [(Name, Ty)]
args Ty
res Exp
body [Bind]
whr) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
            ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$  (Name -> Doc ann) -> [Name] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (\ Name
c -> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"//" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
c) [Name]
comments
            [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> [ Name -> Doc ann
forall ann. Name -> Doc ann
text Name
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
forall ann. Doc ann
quant Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> [Ty] -> Ty -> Doc ann
forall an. [Ty] -> Ty -> Doc an
ppFun (((Name, Ty) -> Ty) -> [(Name, Ty)] -> [Ty]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Ty) -> Ty
forall a b. (a, b) -> b
snd [(Name, Ty)]
args) Ty
res
               , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
                     ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ [[Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([Name -> Doc ann
forall ann. Name -> Doc ann
text Name
n] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> ((Name, Ty) -> Doc ann) -> [(Name, Ty)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Doc ann
forall ann. Name -> Doc ann
text (Name -> Doc ann) -> ((Name, Ty) -> Name) -> (Name, Ty) -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Ty) -> Name
forall a b. (a, b) -> a
fst) [(Name, Ty)]
args [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> [Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"="]) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Exp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
body]
                    [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. Semigroup a => a -> a -> a
<> [Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"where" Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Bind -> Doc ann) -> [Bind] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Bind -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Bind -> Doc ann
pretty [Bind]
whr | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Bind] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Bind]
whr]
               ]
            where quant :: Doc an
                  quant :: forall ann. Doc ann
quant | Bool
quantN    = Name -> Doc an
forall ann. Name -> Doc ann
text Name
"{n} (fin n) => "
                        | Bool
otherwise = Doc an
forall ann. Doc ann
empty

-- | A @where@-binding with an explicit type annotation.
data Bind = Bind !Name !Ty !Exp
      deriving (Bind -> Bind -> Bool
(Bind -> Bind -> Bool) -> (Bind -> Bind -> Bool) -> Eq Bind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Bind -> Bind -> Bool
== :: Bind -> Bind -> Bool
$c/= :: Bind -> Bind -> Bool
/= :: Bind -> Bind -> Bool
Eq, Int -> Bind -> ShowS
[Bind] -> ShowS
Bind -> String
(Int -> Bind -> ShowS)
-> (Bind -> String) -> ([Bind] -> ShowS) -> Show Bind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Bind -> ShowS
showsPrec :: Int -> Bind -> ShowS
$cshow :: Bind -> String
show :: Bind -> String
$cshowList :: [Bind] -> ShowS
showList :: [Bind] -> ShowS
Show)

instance Pretty Bind where
      pretty :: forall ann. Bind -> Doc ann
pretty (Bind Name
n Ty
t Exp
e) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
            [ Name -> Doc ann
forall ann. Name -> Doc ann
text Name
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Ty -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Ty -> Doc ann
pretty Ty
t
            , Name -> Doc ann
forall ann. Name -> Doc ann
text Name
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Exp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e
            ]

data Exp = Lit !BV               -- ^ Sized hex/binary literal (or @(zero : [0])@).
         | Var !Name
         | Call !Name ![Exp]     -- ^ Prefix application: @f e1 e2@.
         | TCall !Name !Natural ![Exp] -- ^ Application with a type argument: @f`{k} e1 e2@.
         | BinOp !Name !Exp !Exp
         | UnOp !Name !Exp
         | Index !Exp !Natural   -- ^ > e @ k
         | If !Exp !Exp !Exp
         | Sing !Exp             -- ^ Bit to @[1]@: @[e]@.
         | Comp !Exp ![(Name, Exp)] -- ^ > [ e | x <- e1 | y <- e2 ]
         | SeqLit ![Exp]         -- ^ > [e1, e2]
      deriving (Exp -> Exp -> Bool
(Exp -> Exp -> Bool) -> (Exp -> Exp -> Bool) -> Eq Exp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Exp -> Exp -> Bool
== :: Exp -> Exp -> Bool
$c/= :: Exp -> Exp -> Bool
/= :: Exp -> Exp -> Bool
Eq, Int -> Exp -> ShowS
[Exp] -> ShowS
Exp -> String
(Int -> Exp -> ShowS)
-> (Exp -> String) -> ([Exp] -> ShowS) -> Show Exp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Exp -> ShowS
showsPrec :: Int -> Exp -> ShowS
$cshow :: Exp -> String
show :: Exp -> String
$cshowList :: [Exp] -> ShowS
showList :: [Exp] -> ShowS
Show)

class Parenless a where
      parenless :: a -> Bool

instance Parenless Exp where
      parenless :: Exp -> Bool
parenless = \ case
            Lit    {} -> Bool
True -- zero-width literals print their own parens.
            Var    {} -> Bool
True
            Sing   {} -> Bool
True
            Comp   {} -> Bool
True
            SeqLit {} -> Bool
True
            Exp
_         -> Bool
False

mparens :: (Pretty a, Parenless a) => a -> Doc an
mparens :: forall a an. (Pretty a, Parenless a) => a -> Doc an
mparens a
a | a -> Bool
forall a. Parenless a => a -> Bool
parenless a
a = a -> Doc an
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
a
          | Bool
otherwise   = Doc an -> Doc an
forall ann. Doc ann -> Doc ann
parens (Doc an -> Doc an) -> Doc an -> Doc an
forall a b. (a -> b) -> a -> b
$ a -> Doc an
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
a

instance Pretty Exp where
      pretty :: forall ann. Exp -> Doc ann
pretty = \ case
            Lit BV
bv         -> BV -> Doc ann
forall an. BV -> Doc an
ppLit BV
bv
            Var Name
n          -> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
n
            Call Name
f [Exp]
es      -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Name -> Doc ann
forall ann. Name -> Doc ann
text Name
f Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Exp -> Doc ann) -> [Exp] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Doc ann
forall a an. (Pretty a, Parenless a) => a -> Doc an
mparens [Exp]
es
            TCall Name
f Natural
k [Exp]
es   -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (Name -> Doc ann
forall ann. Name -> Doc ann
text Name
f Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"`{" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
k) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"}") Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Exp -> Doc ann) -> [Exp] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Doc ann
forall a an. (Pretty a, Parenless a) => a -> Doc an
mparens [Exp]
es
            BinOp Name
op Exp
e1 Exp
e2 -> Exp -> Doc ann
forall a an. (Pretty a, Parenless a) => a -> Doc an
mparens Exp
e1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
op Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Exp -> Doc ann
forall a an. (Pretty a, Parenless a) => a -> Doc an
mparens Exp
e2
            UnOp Name
op Exp
e      -> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
op Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Exp -> Doc ann
forall a an. (Pretty a, Parenless a) => a -> Doc an
mparens Exp
e
            Index Exp
e Natural
k      -> Exp -> Doc ann
forall a an. (Pretty a, Parenless a) => a -> Doc an
mparens Exp
e Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"@" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
k)
            If Exp
c Exp
e1 Exp
e2     -> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"if" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Exp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
c Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"then" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Exp -> Doc ann
forall a an. (Pretty a, Parenless a) => a -> Doc an
mparens Exp
e1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc ann
forall ann. Name -> Doc ann
text Name
"else" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Exp -> Doc ann
forall a an. (Pretty a, Parenless a) => a -> Doc an
mparens Exp
e2
            Sing Exp
e         -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Exp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e
            Comp Exp
e [(Name, Exp)]
arms    -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Exp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (((Name, Exp) -> Doc ann) -> [(Name, Exp)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Exp) -> Doc ann
forall an. (Name, Exp) -> Doc an
arm [(Name, Exp)]
arms)
                  where arm :: (Name, Exp) -> Doc an
                        arm :: forall an. (Name, Exp) -> Doc an
arm (Name
x, Exp
e') = Name -> Doc an
forall ann. Name -> Doc ann
text Name
"|" Doc an -> Doc an -> Doc an
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc an
forall ann. Name -> Doc ann
text Name
x Doc an -> Doc an -> Doc an
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Name -> Doc an
forall ann. Name -> Doc ann
text Name
"<-" Doc an -> Doc an -> Doc an
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Exp -> Doc an
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty Exp
e'
            SeqLit [Exp]
es      -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ (Exp -> Doc ann) -> [Exp] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Exp -> Doc ann
pretty [Exp]
es

-- | Hex when the width is a multiple of four (Cryptol hex literals have a
--   width of exactly four bits per digit), binary otherwise.
ppLit :: BV -> Doc an
ppLit :: forall an. BV -> Doc an
ppLit BV
bv
      | Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0         = Doc an -> Doc an
forall ann. Doc ann -> Doc ann
parens (Doc an -> Doc an) -> Doc an -> Doc an
forall a b. (a -> b) -> a -> b
$ Name -> Doc an
forall ann. Name -> Doc ann
text Name
"zero : [0]"
      | Int
w Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Name -> Doc an
forall ann. Name -> Doc ann
text (Name -> Doc an) -> Name -> Doc an
forall a b. (a -> b) -> a -> b
$ Name
"0x" Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Int -> Name -> Name
pad (Int
w Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
4) (String -> Name
T.pack (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ Integer -> ShowS
forall a. Integral a => a -> ShowS
showHex (BV -> Integer
nat BV
bv) String
"")
      | Bool
otherwise      = Name -> Doc an
forall ann. Name -> Doc ann
text (Name -> Doc an) -> Name -> Doc an
forall a b. (a -> b) -> a -> b
$ Name
"0b" Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Int -> Name -> Name
pad Int
w (String -> Name
T.pack (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ Integer -> (Int -> Char) -> Integer -> ShowS
forall a. Integral a => a -> (Int -> Char) -> a -> ShowS
showIntAtBase Integer
2 Int -> Char
intToDigit (BV -> Integer
nat BV
bv) String
"")
      where w :: Int
            w :: Int
w = BV -> Int
width BV
bv

            pad :: Int -> Text -> Text
            pad :: Int -> Name -> Name
pad Int
n Name
s = Int -> Name -> Name
T.replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Name -> Int
T.length Name
s) Name
"0" Name -> Name -> Name
forall a. Semigroup a => a -> a -> a
<> Name
s

-- | Slicing, MSB-first (Cryptol's bit order): @k@ bits starting at MSB offset
--   @off@ out of a @w@-bit expression. Skips @take@/@drop@ when they would be
--   the identity.
slice :: Size -> Size -> Size -> Exp -> Exp
slice :: Size -> Size -> Size -> Exp -> Exp
slice Size
w Size
off Size
k Exp
e = Exp -> Exp
takeE (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp
dropE Exp
e
      where takeE :: Exp -> Exp
            takeE :: Exp -> Exp
takeE Exp
e' | Size
off Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
k Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
w = Exp
e'
                     | Bool
otherwise    = Name -> Natural -> [Exp] -> Exp
TCall Name
"take" (Size -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
k) [Exp
e']

            dropE :: Exp -> Exp
            dropE :: Exp -> Exp
dropE Exp
e' | Size
off Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
0  = Exp
e'
                     | Bool
otherwise = Name -> Natural -> [Exp] -> Exp
TCall Name
"drop" (Size -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
off) [Exp
e']

-- | Truncate-or-zero-extend to the given width (the @trunc@ and @zext@
--   coercions), as implemented by the emitted @rw'resize@ helper.
resize :: Size -> Exp -> Exp
resize :: Size -> Exp -> Exp
resize Size
sz = \ case
      TCall Name
"rw'resize" Natural
_ [Exp
e] -> Name -> Natural -> [Exp] -> Exp
TCall Name
"rw'resize" (Size -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
sz) [Exp
e]
      Lit BV
bv | BV -> Int
width BV
bv Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0, Size
sz Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
0 -> BV -> Exp
Lit BV
bv
      Exp
e                       -> Name -> Natural -> [Exp] -> Exp
TCall Name
"rw'resize" (Size -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
sz) [Exp
e]

-- | Concatenation, filtering zero-width parts.
cat :: [Exp] -> Exp
cat :: [Exp] -> Exp
cat [Exp]
es = case (Exp -> Bool) -> [Exp] -> [Exp]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Exp -> Bool) -> Exp -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Bool
isNil) [Exp]
es of
      []  -> Exp
nil
      [Exp]
es' -> (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (Name -> Exp -> Exp -> Exp
BinOp Name
"#") [Exp]
es'

nil :: Exp
nil :: Exp
nil = BV -> Exp
Lit BV
BV.nil

isNil :: Exp -> Bool
isNil :: Exp -> Bool
isNil = \ case
      Lit BV
bv -> BV -> Int
width BV
bv Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0
      Exp
_      -> Bool
False