| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
ReWire.Cryptol.Syntax
Description
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).
Synopsis
- type Name = Text
- type Size = Word
- cryptolName :: Text -> Name
- data Module = Module {}
- helpers :: Doc an
- data Param = Param !Name ![Size] !Size
- ppParams :: [Param] -> Doc an
- data Len
- data Ty
- ppFun :: [Ty] -> Ty -> Doc an
- data Defn = Defn {}
- data Bind = Bind !Name !Ty !Exp
- data Exp
- class Parenless a where
- mparens :: (Pretty a, Parenless a) => a -> Doc an
- ppLit :: BV -> Doc an
- slice :: Size -> Size -> Size -> Exp -> Exp
- resize :: Size -> Exp -> Exp
- cat :: [Exp] -> Exp
- nil :: Exp
- isNil :: Exp -> Bool
Documentation
cryptolName :: Text -> Name Source #
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.
Constructors
| Module | |
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.
An uninterpreted function declared in a parameter block: name, argument
widths, result width.
Sequence lengths in types: the device's quantified variable n, or
1 + n.
Constructors
| Defn | |
A where-binding with an explicit type annotation.
Constructors
| Lit !BV | Sized hex/binary literal (or |
| Var !Name | |
| Call !Name ![Exp] | Prefix application: |
| TCall !Name !Natural ![Exp] | Application with a type argument: |
| BinOp !Name !Exp !Exp | |
| UnOp !Name !Exp | |
| Index !Exp !Natural | e @ k |
| If !Exp !Exp !Exp | |
| Sing !Exp | Bit to |
| Comp !Exp ![(Name, Exp)] | [ e | x <- e1 | y <- e2 ] |
| SeqLit ![Exp] | [e1, e2] |
ppLit :: BV -> Doc an Source #
Hex when the width is a multiple of four (Cryptol hex literals have a width of exactly four bits per digit), binary otherwise.
slice :: Size -> Size -> Size -> Exp -> Exp Source #
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.