X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=examples%2FBitSerialHardware.hs-;fp=examples%2FBitSerialHardware.hs-;h=0a35247ad37a8cc9f57f2c2f93d338765e1409c3;hp=0000000000000000000000000000000000000000;hb=c700f5a65d664d4c0a3e76d33aa3769266bf330c;hpb=9238cdac094f9be01ee8978ddb18b6404a6d9ade

diff --git a/examples/BitSerialHardware.hs- b/examples/BitSerialHardware.hs-
new file mode 100644
index 0000000..0a35247
--- /dev/null
+++ b/examples/BitSerialHardware.hs-
@@ -0,0 +1,70 @@
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
+module BitSerialHardware(Wire,BitSerialHardwarePrimitives(..)) where
+import Control.GArrow
+import Control.Category
+import GArrowPretty
+import Prelude hiding (id, (.))
+import Text.PrettyPrint.HughesPJ
+import GArrowPortShape
+import GArrowSkeleton
+import GArrowTikZ
+
+------------------------------------------------------------------------------
+-- Bit-Serial Hardware Primitives
+
+data Wire = Wire
+
+class (GArrowSwap v (,) (), GArrowDrop v (,) (), GArrowCopy v (,) (), GArrowLoop v (,) ()) =>
+      BitSerialHardwarePrimitives v where
+  high    :: v () Wire
+  low     :: v () Wire
+
+  not     :: v Wire        Wire
+  xor     :: v (Wire,Wire) Wire
+  or      :: v (Wire,Wire) Wire
+  and     :: v (Wire,Wire) Wire
+  mux2    :: v (Wire,(Wire,Wire)) Wire
+  maj3    :: v (Wire,(Wire,Wire)) Wire
+  reg     :: v Wire Wire
+
+  loop    :: [Bool] -> v () Wire
+  fifo    ::    Int -> v Wire Wire
+
+  probe   ::    Int -> v Wire Wire
+  oracle  ::    Int -> v ()        Wire
+
+instance BitSerialHardwarePrimitives SourceCode where
+  high        = SC False $ text "high"
+  low         = SC False $ text "low"
+  not         = SC False $ text "not"
+  xor         = SC False $ text "xor"
+  or          = SC False $ text "or"
+  and         = SC False $ text "and"
+  mux2        = SC False $ text "mux2"
+  maj3        = SC False $ text "maj3"
+  reg         = SC False $ text "reg"
+  loop   vals = SC False $ text "loop"   <+> (brackets $ hcat $ punctuate comma $ map (text . show) vals)
+  fifo   len  = SC False $ text "fifo"   <+> (text . show) len
+  probe  id   = SC False $ text "probe"  <+> (text . show) id
+  oracle id   = SC False $ text "oracle" <+> (text . show) id
+
+instance BitSerialHardwarePrimitives (GArrowSkeleton Opaque) where
+  reg         = GAS_misc reg'
+                where reg' = MkOpaque "reg" $
+                             do x <- freshM
+                                return $ GASPortPassthrough (PortFree x) (PortFree x) reg'
+  xor         = GAS_misc xor'
+                where xor' = MkOpaque "xor" $
+                             do x <- freshM
+                                return $ GASPortPassthrough (PortTensor (PortFree x) (PortFree x)) (PortFree x) xor'
+  high        = undefined
+  low         = undefined
+  not         = undefined
+  or          = undefined
+  and         = undefined
+  mux2        = undefined
+  maj3        = undefined
+  loop   vals = undefined
+  fifo   len  = undefined
+  probe  id   = undefined
+  oracle id   = undefined