--- /dev/null
+{-# 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
-- You must have lp_solve installed in order for this to work.
--
-module GArrowTikZ (tikz)
+module GArrowTikZ (tikz,Opaque(..),toTikZ,tikz_header,tikz_footer,skelify',skelify'')
where
import System.Process
import Prelude hiding ( id, (.), lookup )
import GArrowPortShape
import GHC.HetMet.Private
+skelify' :: (forall g . (GArrowCopy g (,) (), GArrowDrop g (,) (), GArrowSwap g (,) (), GArrowLoop g (,) ()) => g x y) ->
+ GArrowSkeleton Opaque x y
+skelify' = \g -> g
+
+skelify'' :: GArrowSkeleton Opaque x y -> GArrowSkeleton Opaque x y
+skelify'' = \g -> g
+
------------------------------------------------------------------------------
-- Tracks
do { (top, x ,bot) <- alloc inp
; (_, y ,_) <- alloc outp
--; constrainEq x y
- ; simpleDiag s top x y bot [] }
+ ; simpleDiag'' s top x y bot [] "black" }
toDiagram q = mkdiag q
-- do (top, x ,bot) <- alloc inp
; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "cancell" ++
drawWires tp x1 y x2 y "black" ++
drawLine x1 (tp!lowermost x) ((x1+x2)/2) (tp!uppermost y) "gray!50" "dashed"
- ; return $ DiagramBox 2 top (TT x y) r y bot }
+ ; return $ DiagramBox 2.4 top (TT x y) r y bot }
mkdiag' GAS_cancelr = do { (top,(TT x y),bot) <- alloc inp
; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "cancelr" ++
drawWires tp x1 x x2 x "black" ++
drawLine x1 (tp!uppermost y) ((x1+x2)/2) (tp!lowermost x) "gray!50" "dashed"
- ; return $ DiagramBox 2 top (TT x y) r x bot }
+ ; return $ DiagramBox 2.4 top (TT x y) r x bot }
mkdiag' GAS_uncancell = do { (top,(TT x y),bot) <- alloc outp
; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "uncancell" ++
drawWires tp x1 y x2 y "black" ++
drawLine ((x1+x2)/2) (tp!uppermost y) x2 (tp!lowermost x) "gray!50" "dashed"
- ; return $ DiagramBox 2 top y r (TT x y) bot }
+ ; return $ DiagramBox 2.8 top y r (TT x y) bot }
mkdiag' GAS_uncancelr = do { (top,(TT x y),bot) <- alloc outp
; let r tp x1 y1 x2 y2 = drawBox x1 y1 x2 y2 "gray!50" "uncancelr" ++
drawWires tp x1 x x2 x "black" ++
drawLine ((x1+x2)/2) (tp!lowermost x) x2 (tp!uppermost y) "gray!50" "dashed"
- ; return $ DiagramBox 2 top x r (TT x y) bot }
+ ; return $ DiagramBox 2.8 top x r (TT x y) bot }
mkdiag' GAS_drop = do { (top, x ,bot) <- alloc inp
; (_, y ,_) <- alloc outp
; constrainEq x y
drawWires tp x1 x ((x1+x2)/2) x "black" ++
drawWires tp ((x1+x2)/2) x x2 y "black" ++
drawWires tp ((x1+x2)/2) x x2 z "black"
- ; return $ DiagramBox 2 top x r (TT y z) bot
+ ; return $ DiagramBox defaultWidth top x r (TT y z) bot
}
mkdiag' GAS_swap = do { (top,(TT x y),bot) <- alloc inp
; (top,(TT x' y'),bot) <- alloc outp
drawWires tp x1 z x2 z "black"
; let pin = (TT (TT x y) z)
; let pout = (TT x (TT y z))
- ; return $ if draw_assoc then DiagramBox 2 top pin r pout bot else DiagramBox 0 top pin noRender pout bot
+ ; return $ if draw_assoc then DiagramBox defaultWidth top pin r pout bot else DiagramBox 0 top pin noRender pout bot
}
mkdiag' GAS_unassoc =
do { (top,(TT x (TT y z)),bot) <- alloc inp
drawWires tp x1 z x2 z "black"
; let pin = (TT x (TT y z))
; let pout = (TT (TT x y) z)
- ; return $ if draw_assoc then DiagramBox 2 top pin r pout bot else DiagramBox 0 top pin noRender pout bot
+ ; return $ if draw_assoc then DiagramBox defaultWidth top pin r pout bot else DiagramBox 0 top pin noRender pout bot
}
mkdiag' (GAS_loopl f) = do { f' <- mkdiag' f
; l <- allocLoop (case (getIn f') of (TT z _) -> z ; _ -> error "GAS_loopl: mismatch")
; return $ DiagramLoopBot f' l }
mkdiag' (GAS_misc f ) = mkdiag f
+defaultWidth = 2
+
diagramBox :: TrackIdentifier -> Tracks -> BoxRenderer -> Tracks -> TrackIdentifier -> ConstraintM Diagram
diagramBox ptop pin r pout pbot = do { constrain ptop LT (uppermost pin) (-1)
; constrain pbot GT (lowermost pin) 1
; constrain ptop LT (uppermost pout) (-1)
; constrain pbot GT (lowermost pout) 1
; constrain ptop LT pbot (-1)
- ; return $ DiagramBox 2 ptop pin r pout pbot
+ ; return $ DiagramBox defaultWidth ptop pin r pout pbot
}
simpleDiag text ptop pin pout pbot conn = simpleDiag' text ptop pin pout pbot conn "black"
simpleDiag' text ptop pin pout pbot conn color = diagramBox ptop pin defren pout pbot
concat (map (\(x,y) -> drawWires tp x1 x x2 y "black") conn)
-- ++ wires (x-1) p1 x "green"
-- ++ wires (x+w) p2 (x+w+1) "red"
+simpleDiag'' text ptop pin pout pbot conn color = diagramBox ptop pin defren pout pbot
+ where
+ defren tp x1 y1 x2 y2 = drawBoxC x1 y1 x2 y2 color text ++
+ concat (map (\(x,y) -> drawWires tp x1 x x2 y "black") conn)
+ -- ++ wires (x-1) p1 x "green"
+ -- ++ wires (x+w) p2 (x+w+1) "red"
draw_assoc = False
draw_first_second = False
do_lp_solve :: [Constraint] -> IO String
do_lp_solve c = do { let stdin = "min: x1;\n" ++ (foldl (++) "" (map show c)) ++ "\n"
- ; putStrLn stdin
+-- ; putStrLn stdin
; stdout <- readProcess "lp_solve" [] stdin
; return stdout
}
toTrackPos [] tr = 0 -- error $ "could not find track "++show tr
toTrackPos ((i,f):rest) tr = if (i==tr) then f else toTrackPos rest tr
+
toTikZ :: (ToDiagram m, Detect m) => GArrowSkeleton m a b -> IO String
toTikZ g =
let cm = do { let g' = detectShape g
; return (t ++ drawWires m 0 (getIn d) 1 (getIn d) "black"
++ drawWires m (width m d+1) (getOut d) (width m d+2) (getOut d) "black")
}
-
-
-tikz :: forall c .
- (forall g .
- (Int -> PGArrow g (GArrowUnit g) Int) ->
- (PGArrow g (GArrowTensor g c c) c) ->
- PGArrow g c c)
- -> IO ()
-tikz x = tikz' $ beautify $ optimize $ unG (x (\c -> PGArrowD { unG = GAS_misc (oconst c) })
- (PGArrowD { unG = GAS_misc omult }))
-
-oconst :: Int -> Opaque () a
-oconst c = MkOpaque ("const "++(show c)) $
- do x <- freshM
- return $ GASPortPassthrough PortUnit (PortFree x) (oconst c)
-
-omult :: Opaque (a,a) a
-omult = MkOpaque "mult" $
- do x <- freshM
- return $ GASPortPassthrough (PortTensor (PortFree x) (PortFree x)) (PortFree x) omult
-
-tikz' example
- = do putStrLn "\\documentclass{article}"
- putStrLn "\\usepackage[paperwidth=\\maxdimen,paperheight=\\maxdimen]{geometry}"
- putStrLn "\\usepackage{tikz}"
- putStrLn "\\usepackage{amsmath}"
- putStrLn "\\usepackage[tightpage,active]{preview}"
- putStrLn "\\begin{document}"
- putStrLn "\\setlength\\PreviewBorder{5pt}"
- putStrLn "\\begin{preview}"
- putStrLn $ "\\begin{tikzpicture}[every on chain/.style={join=by ->},yscale=-1]"
- tikz <- toTikZ example
- putStrLn tikz
- putStrLn "\\end{tikzpicture}"
- putStrLn "\\end{preview}"
- --putStrLn "\\pagebreak"
- --putStrLn "\\begin{align*}"
- --putStr (toTikZ' example)
- --putStrLn "\\end{align*}"
- putStrLn "\\end{document}"
+
+tikz_header =
+ "\\documentclass{article}\n" ++
+ "\\usepackage[paperwidth=\\maxdimen,paperheight=\\maxdimen]{geometry}\n" ++
+ "\\usepackage{tikz}\n" ++
+ "\\usepackage{amsmath}\n" ++
+ "\\usepackage[tightpage,active]{preview}\n" ++
+ "\\begin{document}\n" ++
+ "\\setlength\\PreviewBorder{5pt}\n" ++
+ "\\begin{preview}\n" ++
+ "\\begin{tikzpicture}[every on chain/.style={join=by ->},yscale=-1]\n"
+
+tikz_footer =
+ "\\end{tikzpicture}\n" ++
+ "\\end{preview}\n" ++
+ "\\end{document}\n"
+
+tikz example =
+ do putStrLn tikz_header
+ tikz <- toTikZ example
+ putStrLn tikz
+ putStrLn tikz_footer
-- Random TikZ routines
textc x y text color =
" ("++show (x1*xscale)++","++show (y1*yscale)++") rectangle ("++
show (x2*xscale)++","++show (y2*yscale)++");\n"
+drawBoxC x1 y1 x2 y2 color text =
+ "\\node[anchor=center] at ("++show ((x1+x2)*xscale/2)++"cm,"++show ((y1+y2)*yscale/2)++"cm) "++
+ "{{\\tt{"++text++"}}};\n"
+ ++
+ "\\path[draw,color="++color++"]"++
+ " ("++show (x1*xscale)++","++show (y1*yscale)++") rectangle ("++
+ show (x2*xscale)++","++show (y2*yscale)++");\n"
+
drawLine x1 y1 x2 y2 color style =
"\\path[draw,color="++color++","++style++"] "++
"("++show (x1*xscale)++","++show (y1*yscale)++") -- " ++
projects / coq-hetmet.git / commitdiff