{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
{-
Module           : What4.Protocol.VerilogWriter.Export.ABCVerilog
Copyright        : (c) Galois, Inc 2020
Maintainer       : Aaron Tomb <atomb@galois.com>
License          : BSD3

Export Verilog in the particular syntax ABC supports.
-}

module What4.Protocol.VerilogWriter.ABCVerilog where

import Data.BitVector.Sized
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import Data.String
import Prettyprinter
import What4.BaseTypes
import What4.Protocol.VerilogWriter.AST
import Numeric (showHex)
import Prelude hiding ((<$>))

moduleDoc :: Module sym n -> Doc () -> Doc ()
moduleDoc :: Module sym n -> Doc () -> Doc ()
moduleDoc (Module ModuleState sym n
ms) Doc ()
name =
  [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
    [ Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
      [ Doc ()
"module" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
name Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
tupled [Doc ()]
params Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
forall ann. Doc ann
semi
      , [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep (((Some BaseTypeRepr, Identifier) -> Doc ())
-> [(Some BaseTypeRepr, Identifier)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Some BaseTypeRepr, Identifier) -> Doc ()
inputDoc ([(Some BaseTypeRepr, Identifier)]
-> [(Some BaseTypeRepr, Identifier)]
forall a. [a] -> [a]
reverse (ModuleState sym n -> [(Some BaseTypeRepr, Identifier)]
forall sym n.
ModuleState sym n -> [(Some BaseTypeRepr, Identifier)]
vsInputs ModuleState sym n
ms)))
      , [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep (((Some BaseTypeRepr, Bool, Identifier, Some Exp) -> Doc ())
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Doc () -> (Some BaseTypeRepr, Bool, Identifier, Some Exp) -> Doc ()
wireDoc Doc ()
"wire") ([(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
forall a. [a] -> [a]
reverse (ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsWires ModuleState sym n
ms)))
      , [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep (((Some BaseTypeRepr, Bool, Identifier, Some Exp) -> Doc ())
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Doc () -> (Some BaseTypeRepr, Bool, Identifier, Some Exp) -> Doc ()
wireDoc Doc ()
"output") ([(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
forall a. [a] -> [a]
reverse (ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs ModuleState sym n
ms)))
      ]
    , Doc ()
"endmodule"
    ]
  where
    inputNames :: [Doc ()]
inputNames = ((Some BaseTypeRepr, Identifier) -> Doc ())
-> [(Some BaseTypeRepr, Identifier)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Identifier -> Doc ()
identDoc (Identifier -> Doc ())
-> ((Some BaseTypeRepr, Identifier) -> Identifier)
-> (Some BaseTypeRepr, Identifier)
-> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Some BaseTypeRepr, Identifier) -> Identifier
forall a b. (a, b) -> b
snd) (ModuleState sym n -> [(Some BaseTypeRepr, Identifier)]
forall sym n.
ModuleState sym n -> [(Some BaseTypeRepr, Identifier)]
vsInputs ModuleState sym n
ms)
    outputNames :: [Doc ()]
outputNames = ((Some BaseTypeRepr, Bool, Identifier, Some Exp) -> Doc ())
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Identifier -> Doc ()
identDoc (Identifier -> Doc ())
-> ((Some BaseTypeRepr, Bool, Identifier, Some Exp) -> Identifier)
-> (Some BaseTypeRepr, Bool, Identifier, Some Exp)
-> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Some BaseTypeRepr
_, Bool
_, Identifier
n, Some Exp
_) -> Identifier
n)) (ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
forall sym n.
ModuleState sym n
-> [(Some BaseTypeRepr, Bool, Identifier, Some Exp)]
vsOutputs ModuleState sym n
ms)
    params :: [Doc ()]
params = [Doc ()] -> [Doc ()]
forall a. [a] -> [a]
reverse [Doc ()]
inputNames [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. [a] -> [a] -> [a]
++ [Doc ()] -> [Doc ()]
forall a. [a] -> [a]
reverse [Doc ()]
outputNames

typeDoc :: Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
typeDoc :: Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
typeDoc Doc ()
ty Bool
_ BaseTypeRepr tp
BaseBoolRepr = Doc ()
ty
typeDoc Doc ()
ty Bool
isSigned (BaseBVRepr NatRepr w
w) =
  Doc ()
ty Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  (if Bool
isSigned then Doc ()
"signed " else Doc ()
forall a. Monoid a => a
mempty) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<>
  Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
brackets (Integer -> Doc ()
forall a ann. Pretty a => a -> Doc ann
pretty (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
":0")
typeDoc Doc ()
_ Bool
_ BaseTypeRepr tp
_ = Doc ()
"<type error>"

identDoc :: Identifier -> Doc ()
identDoc :: Identifier -> Doc ()
identDoc = Identifier -> Doc ()
forall a ann. Pretty a => a -> Doc ann
pretty

lhsDoc :: LHS -> Doc ()
lhsDoc :: LHS -> Doc ()
lhsDoc (LHS Identifier
name) = Identifier -> Doc ()
identDoc Identifier
name
lhsDoc (LHSBit Identifier
name Integer
idx) =
  Identifier -> Doc ()
identDoc Identifier
name Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
brackets (Integer -> Doc ()
forall a ann. Pretty a => a -> Doc ann
pretty Integer
idx)

inputDoc :: (Some BaseTypeRepr, Identifier) -> Doc ()
inputDoc :: (Some BaseTypeRepr, Identifier) -> Doc ()
inputDoc (Some BaseTypeRepr
tp, Identifier
name) =
  (forall (tp :: BaseType). BaseTypeRepr tp -> Doc ())
-> Some BaseTypeRepr -> Doc ()
forall k (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
forall (tp :: BaseType).
Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
typeDoc Doc ()
"input" Bool
False) Some BaseTypeRepr
tp Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Identifier -> Doc ()
identDoc Identifier
name Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
forall ann. Doc ann
semi

wireDoc :: Doc () -> (Some BaseTypeRepr, Bool, Identifier, Some Exp) -> Doc ()
wireDoc :: Doc () -> (Some BaseTypeRepr, Bool, Identifier, Some Exp) -> Doc ()
wireDoc Doc ()
ty (Some BaseTypeRepr
tp, Bool
isSigned, Identifier
name, Some Exp
e) =
  (forall (tp :: BaseType). BaseTypeRepr tp -> Doc ())
-> Some BaseTypeRepr -> Doc ()
forall k (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
forall (tp :: BaseType).
Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
typeDoc Doc ()
ty Bool
isSigned) Some BaseTypeRepr
tp Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  Identifier -> Doc ()
identDoc Identifier
name Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  Doc ()
forall ann. Doc ann
equals Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  (forall (tp :: BaseType). Exp tp -> Doc ()) -> Some Exp -> Doc ()
forall k (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall (tp :: BaseType). Exp tp -> Doc ()
expDoc Some Exp
e Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<>
  Doc ()
forall ann. Doc ann
semi

unopDoc :: Unop tp -> Doc ()
unopDoc :: Unop tp -> Doc ()
unopDoc Unop tp
Not   = Doc ()
"!"
unopDoc Unop tp
BVNot = Doc ()
"~"

binopDoc :: Binop inTp outTp -> Doc ()
binopDoc :: Binop inTp outTp -> Doc ()
binopDoc Binop inTp outTp
And      = Doc ()
"&&"
binopDoc Binop inTp outTp
Or       = Doc ()
"||"
binopDoc Binop inTp outTp
Xor      = Doc ()
"^^"
binopDoc Binop inTp outTp
BVAnd    = Doc ()
"&"
binopDoc Binop inTp outTp
BVOr     = Doc ()
"|"
binopDoc Binop inTp outTp
BVXor    = Doc ()
"^"
binopDoc Binop inTp outTp
BVAdd    = Doc ()
"+"
binopDoc Binop inTp outTp
BVSub    = Doc ()
"-"
binopDoc Binop inTp outTp
BVMul    = Doc ()
"*"
binopDoc Binop inTp outTp
BVDiv    = Doc ()
"/"
binopDoc Binop inTp outTp
BVRem    = Doc ()
"%"
binopDoc Binop inTp outTp
BVPow    = Doc ()
"**"
binopDoc Binop inTp outTp
BVShiftL = Doc ()
"<<"
binopDoc Binop inTp outTp
BVShiftR = Doc ()
">>"
binopDoc Binop inTp outTp
BVShiftRA = Doc ()
">>>"
binopDoc Binop inTp outTp
Eq       = Doc ()
"=="
binopDoc Binop inTp outTp
Ne       = Doc ()
"!="
binopDoc Binop inTp outTp
Lt       = Doc ()
"<"
binopDoc Binop inTp outTp
Le       = Doc ()
"<="

-- | Show non-negative Integral numbers in base 16.
hexDoc :: BV w -> Doc ()
hexDoc :: BV w -> Doc ()
hexDoc BV w
n = Identifier -> Doc ()
forall a. IsString a => Identifier -> a
fromString (Identifier -> Doc ()) -> Identifier -> Doc ()
forall a b. (a -> b) -> a -> b
$ Integer -> ShowS
forall a. (Integral a, Show a) => a -> ShowS
showHex (BV w -> Integer
forall (w :: Nat). BV w -> Integer
asUnsigned BV w
n) Identifier
""

decDoc :: NatRepr w -> BV w -> Doc ()
decDoc :: NatRepr w -> BV w -> Doc ()
decDoc NatRepr w
w BV w
n = Identifier -> Doc ()
forall a. IsString a => Identifier -> a
fromString (Identifier -> Doc ()) -> Identifier -> Doc ()
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> Identifier
forall (w :: Nat). NatRepr w -> BV w -> Identifier
ppDec NatRepr w
w BV w
n

iexpDoc :: IExp tp -> Doc ()
iexpDoc :: IExp tp -> Doc ()
iexpDoc (Ident BaseTypeRepr tp
_ Identifier
name) = Identifier -> Doc ()
identDoc Identifier
name

-- NB: special pretty-printer because ABC has a hack to detect this specific syntax
rotateDoc :: String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
rotateDoc :: Identifier -> Identifier -> NatRepr w -> IExp tp -> BV w -> Doc ()
rotateDoc Identifier
op1 Identifier
op2 wr :: NatRepr w
wr@(NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue -> Integer
w) IExp tp
e BV w
n =
  Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens (Doc ()
v Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Identifier -> Doc ()
forall a. IsString a => Identifier -> a
fromString Identifier
op1 Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
nd) Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"|" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens (Doc ()
v Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Identifier -> Doc ()
forall a. IsString a => Identifier -> a
fromString Identifier
op2 Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens (Integer -> Doc ()
forall a ann. Pretty a => a -> Doc ann
pretty Integer
w Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"-" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
nd))
    where v :: Doc ()
v = IExp tp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
e
          nd :: Doc ()
nd = NatRepr w -> BV w -> Doc ()
forall (w :: Nat). NatRepr w -> BV w -> Doc ()
decDoc NatRepr w
wr BV w
n

expDoc :: Exp tp -> Doc ()
expDoc :: Exp tp -> Doc ()
expDoc (IExp IExp tp
e) = IExp tp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
e
expDoc (Binop Binop inTp tp
op IExp inTp
l IExp inTp
r) = IExp inTp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp inTp
l Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Binop inTp tp -> Doc ()
forall (inTp :: BaseType) (outTp :: BaseType).
Binop inTp outTp -> Doc ()
binopDoc Binop inTp tp
op Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> IExp inTp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp inTp
r
expDoc (Unop Unop tp
op IExp tp
e) = Unop tp -> Doc ()
forall (tp :: BaseType). Unop tp -> Doc ()
unopDoc Unop tp
op Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> IExp tp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
e
expDoc (BVRotateL NatRepr w
wr IExp tp
e BV w
n) = Identifier -> Identifier -> NatRepr w -> IExp tp -> BV w -> Doc ()
forall (w :: Nat) (tp :: BaseType).
Identifier -> Identifier -> NatRepr w -> IExp tp -> BV w -> Doc ()
rotateDoc Identifier
"<<" Identifier
">>" NatRepr w
wr IExp tp
e BV w
n
expDoc (BVRotateR NatRepr w
wr IExp tp
e BV w
n) = Identifier -> Identifier -> NatRepr w -> IExp tp -> BV w -> Doc ()
forall (w :: Nat) (tp :: BaseType).
Identifier -> Identifier -> NatRepr w -> IExp tp -> BV w -> Doc ()
rotateDoc Identifier
">>" Identifier
"<<" NatRepr w
wr IExp tp
e BV w
n
expDoc (Mux IExp BaseBoolType
c IExp tp
t IExp tp
e) = IExp BaseBoolType -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp BaseBoolType
c Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"?" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> IExp tp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
t Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall ann. Doc ann
colon Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> IExp tp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
e
expDoc (Bit IExp (BaseBVType w)
e Integer
i) =
  IExp (BaseBVType w) -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp (BaseBVType w)
e Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
brackets (Integer -> Doc ()
forall a ann. Pretty a => a -> Doc ann
pretty Integer
i)
expDoc (BitSelect IExp (BaseBVType w)
e (NatRepr start -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue -> Integer
start) (NatRepr len -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue -> Integer
len)) =
  IExp (BaseBVType w) -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp (BaseBVType w)
e Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
brackets (Integer -> Doc ()
forall a ann. Pretty a => a -> Doc ann
pretty (Integer
start Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
len Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
forall ann. Doc ann
colon Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Integer -> Doc ()
forall a ann. Pretty a => a -> Doc ann
pretty Integer
start)
expDoc (Concat NatRepr w
_ [Some IExp]
es) = Doc () -> Doc () -> Doc () -> [Doc ()] -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep Doc ()
forall ann. Doc ann
lbrace Doc ()
forall ann. Doc ann
rbrace Doc ()
forall ann. Doc ann
comma ((Some IExp -> Doc ()) -> [Some IExp] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map ((forall (tp :: BaseType). IExp tp -> Doc ()) -> Some IExp -> Doc ()
forall k (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc) [Some IExp]
es)
expDoc (BVLit NatRepr w
w BV w
n) = Integer -> Doc ()
forall a ann. Pretty a => a -> Doc ann
pretty (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue NatRepr w
w) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"'h" Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> BV w -> Doc ()
forall (w :: Nat). BV w -> Doc ()
hexDoc BV w
n
expDoc (BoolLit Bool
True) = Doc ()
"1'b1"
expDoc (BoolLit Bool
False) = Doc ()
"1'b0"