From ec996e8cb550676d89d187061db7d018af9ec88d Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Thu, 19 Apr 2012 22:41:07 -0700 Subject: [PATCH] update to use Control.GArrow instead of GHC.HetMet.GArrow --- examples/BiGArrow.hs | 2 +- examples/BitSerialHardware.hs | 47 ++++++++ examples/CircuitExample.hs | 2 +- examples/Demo.hs | 15 +-- examples/DemoMain.hs | 2 +- examples/Fail.hs | 2 + examples/GArrowDemo.hs | 17 +++ examples/GArrowInclusion.hs | 6 + examples/GArrowPortShape.hs | 15 ++- examples/GArrowPretty.hs | 41 +++++++ examples/GArrowShow.hs | 6 + examples/GArrowSkeleton.hs | 31 +++++- examples/GArrowTikZ.hs | 61 ++++++++--- examples/GArrowTutorial.hs | 2 +- examples/Makefile | 27 ++++- examples/Stack.hs | 244 +++++++++++++++++++++++++++++++++++++++++ examples/TuringMachine.hs | 81 ++++++++++++++ examples/Unflattening.hs | 2 +- examples/VerilogDemo.hs | 9 ++ src/ExtractionMain.v | 6 +- 20 files changed, 572 insertions(+), 46 deletions(-) create mode 100644 examples/BitSerialHardware.hs create mode 100644 examples/Fail.hs create mode 100644 examples/GArrowDemo.hs create mode 100644 examples/GArrowInclusion.hs create mode 100644 examples/GArrowPretty.hs create mode 100644 examples/GArrowShow.hs create mode 100644 examples/Stack.hs create mode 100644 examples/TuringMachine.hs create mode 100644 examples/VerilogDemo.hs diff --git a/examples/BiGArrow.hs b/examples/BiGArrow.hs index 40ff343..a6ecde4 100644 --- a/examples/BiGArrow.hs +++ b/examples/BiGArrow.hs @@ -1,7 +1,7 @@ {-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -ddump-types -XNoMonoPatBinds -XFlexibleInstances -XGADTs -XUndecidableInstances -XDatatypeContexts #-} module BiGArrow where -import GHC.HetMet.GArrow +import Control.GArrow import Control.Category import Control.Arrow import Prelude hiding ( id, (.) ) diff --git a/examples/BitSerialHardware.hs b/examples/BitSerialHardware.hs new file mode 100644 index 0000000..2e82b0d --- /dev/null +++ b/examples/BitSerialHardware.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-} +module BitSerialHardware(Wire,BitSerialHardwarePrimitives(..)) where +import Control.GArrow +import Control.Category +import GArrowPretty +import Prelude hiding (id, (.)) +import Text.PrettyPrint.HughesPJ + +------------------------------------------------------------------------------ +-- 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 + diff --git a/examples/CircuitExample.hs b/examples/CircuitExample.hs index b8ca60b..f32d5ff 100644 --- a/examples/CircuitExample.hs +++ b/examples/CircuitExample.hs @@ -1,7 +1,7 @@ {-# OPTIONS_GHC -XModalTypes -ddump-types -XNoMonoPatBinds -XMultiParamTypeClasses -XTypeOperators #-} module CircuitExample where -import GHC.HetMet.GArrow +import Control.GArrow import GHC.HetMet.GuestLanguage hiding ((-)) import Control.Category import Prelude hiding ( id, (.) ) diff --git a/examples/Demo.hs b/examples/Demo.hs index 7a6aee8..579bf4d 100644 --- a/examples/Demo.hs +++ b/examples/Demo.hs @@ -1,11 +1,18 @@ {-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint -XScopedTypeVariables -fsimpleopt-before-flatten #-} module Demo (demo) where + +demo const mult = + <{ \y -> + let foo = ~~mult (~~mult foo (~~mult y foo)) (~~mult y ~~(const 3)) + in foo }> + + {- demo const mult = <{ \y -> ~~mult - (~~mult y y) + (~~(const 1)) (~~mult y y) }> -} @@ -54,12 +61,6 @@ demo const mult = -demo const mult = - <{ \y -> - let foo = ~~mult (~~mult foo (~~mult y foo)) y - in foo }> - - diff --git a/examples/DemoMain.hs b/examples/DemoMain.hs index 08fab3e..c511bfa 100644 --- a/examples/DemoMain.hs +++ b/examples/DemoMain.hs @@ -1,7 +1,7 @@ import Control.Category import GArrowTikZ import GHC.HetMet.Private -import GHC.HetMet.GArrow +import Control.GArrow import Demo main = tikz demo diff --git a/examples/Fail.hs b/examples/Fail.hs new file mode 100644 index 0000000..06466bc --- /dev/null +++ b/examples/Fail.hs @@ -0,0 +1,2 @@ +applyCircuit = + <[ \higherOrderCircuit -> \arg -> higherOrderCircuit arg ]> diff --git a/examples/GArrowDemo.hs b/examples/GArrowDemo.hs new file mode 100644 index 0000000..e341bf2 --- /dev/null +++ b/examples/GArrowDemo.hs @@ -0,0 +1,17 @@ + + +sample1 = + ga_copy >>> + ga_swap >>> + ga_first ga_drop >>> + ga_cancell + +-- from the paper +sample2 = + ga_uncancelr >>> + ga_first ga_copy >>> + ga_swap >>> + ga_second (ga_first ga_drop >>> + ga_cancell) >>> + ga_cancell + diff --git a/examples/GArrowInclusion.hs b/examples/GArrowInclusion.hs new file mode 100644 index 0000000..e8c7fb6 --- /dev/null +++ b/examples/GArrowInclusion.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE FunctionalDependencies, NoMonomorphismRestriction, MultiParamTypeClasses #-} +module GArrowInclusion(GArrowInclusion(ga_inc)) where +import Control.GArrow + +class GArrow g (**) u => GArrowInclusion g (**) u g' where + ga_inc :: g' x y -> g x y diff --git a/examples/GArrowPortShape.hs b/examples/GArrowPortShape.hs index fe0ab58..45cbdb2 100644 --- a/examples/GArrowPortShape.hs +++ b/examples/GArrowPortShape.hs @@ -19,11 +19,11 @@ -- information for certain nodes (the inference mechanism below adds -- it on every node). -- -module GArrowPortShape (GArrowPortShape(..), PortShape(..), detectShape) +module GArrowPortShape (GArrowPortShape(..), PortShape(..), detectShape, Detect(..), DetectM, freshM) where import Prelude hiding ( id, (.), lookup ) import Control.Category -import GHC.HetMet.GArrow +import Control.GArrow import Unify import GArrowSkeleton import Control.Monad.State @@ -128,16 +128,19 @@ resolveG u (GASPortShapeWrapper x y g) = GASPortShapeWrapper (getU' u x) (getU' resolveG' (GAS_loopr f) = GAS_loopr (resolveG' f) resolveG' (GAS_misc g ) = GAS_misc $ resolveG u g -detectShape :: GArrowSkeleton m a b -> GArrowPortShape m () a b +detectShape :: Detect m => GArrowSkeleton m a b -> GArrowPortShape m () a b detectShape g = runM (detect g) -runM :: DetectM (GArrowPortShape m UVar a b) -> GArrowPortShape m () a b +runM :: Detect m => DetectM (GArrowPortShape m UVar a b) -> GArrowPortShape m () a b runM f = let s = (emptyUnifier,uvarSupply) g = evalState f s (u,_) = execState f s in resolveG u g -detect :: GArrowSkeleton m a b -> DetectM (GArrowPortShape m UVar a b) +class Detect m where + detect' :: m x y -> DetectM (GArrowPortShape m UVar x y) + +detect :: Detect m => GArrowSkeleton m a b -> DetectM (GArrowPortShape m UVar a b) detect (GAS_id ) = do { x <- freshM ; return $ GASPortShapeWrapper (PortFree x) (PortFree x) GAS_id } detect (GAS_comp f g) = do { f' <- detect f ; g' <- detect g @@ -211,5 +214,5 @@ detect (GAS_loopr f) = do { x <- freshM ; return $ GASPortShapeWrapper (PortFree x) (PortFree y) (GAS_loopr (GAS_misc f')) } -detect (GAS_misc f) = error "GAS_misc: not implemented" +detect (GAS_misc f) = detect' f diff --git a/examples/GArrowPretty.hs b/examples/GArrowPretty.hs new file mode 100644 index 0000000..0be25dc --- /dev/null +++ b/examples/GArrowPretty.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE FunctionalDependencies, NoMonomorphismRestriction, MultiParamTypeClasses #-} +module GArrowPretty(SourceCode(..),pprGArrow) where +import Prelude hiding (id,(.)) +import Control.GArrow +import Control.Category +import Text.PrettyPrint.HughesPJ + +-- The Bool flag is to minimize the number of parentheses generated: +-- it is true iff the principal connective is of lower precedence than +-- juxtaposition +data SourceCode a b = SC Bool Doc + +instance Category SourceCode where + id = SC False $ text "id" + (SC _ g) . (SC _ f) = SC True $ f <+> (text ">>>") $$ g + +instance GArrow SourceCode (,) () where + ga_first (SC x f) = SC True $ text "ga_first" + <+> if x then parens f else f + ga_second (SC x f) = SC True $ text "ga_second" + <+> if x then parens f else f + ga_cancell = SC False $ text "ga_cancell" + ga_cancelr = SC False $ text "ga_cancelr" + ga_uncancell = SC False $ text "ga_uncancell" + ga_uncancelr = SC False $ text "ga_uncancelr" + ga_assoc = SC False $ text "ga_assoc" + ga_unassoc = SC False $ text "ga_unassoc" + +instance GArrowSwap SourceCode (,) () where + ga_swap = SC False $ text "ga_swap" +instance GArrowDrop SourceCode (,) () where + ga_drop = SC False $ text "ga_drop" +instance GArrowCopy SourceCode (,) () where + ga_copy = SC False $ text "ga_copy" +instance GArrowLoop SourceCode (,) () where + ga_loopl (SC x f) = SC True $ text "ga_loopl" <+> if x then parens f else f + ga_loopr (SC x f) = SC True $ text "ga_loopr" <+> if x then parens f else f + +pprGArrow :: SourceCode x y -> Doc +pprGArrow (SC _ doc) = doc + diff --git a/examples/GArrowShow.hs b/examples/GArrowShow.hs new file mode 100644 index 0000000..39695d6 --- /dev/null +++ b/examples/GArrowShow.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE FunctionalDependencies, NoMonomorphismRestriction, MultiParamTypeClasses #-} +module GArrowShow(GArrowShow) where +import Control.GArrow + +class GArrow g (**) u => GArrowShow g (**) u where + ga_show :: g x y -> String diff --git a/examples/GArrowSkeleton.hs b/examples/GArrowSkeleton.hs index 9f42e8a..963eb45 100644 --- a/examples/GArrowSkeleton.hs +++ b/examples/GArrowSkeleton.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies, RankNTypes #-} ----------------------------------------------------------------------------- -- | -- Module : GArrowSkeleton @@ -23,13 +23,14 @@ -- -- A normal form theorem and normalization algorithm are being prepared. -- -module GArrowSkeleton (GArrowSkeleton(..), optimize, beautify) +module GArrowSkeleton (GArrowSkeleton(..), mkSkeleton, OptimizeFlag(..), optimize, beautify) where import Prelude hiding ( id, (.), lookup, repeat ) import Control.Category -import GHC.HetMet.GArrow +import Control.GArrow import Unify import Control.Monad.State +import GArrowInclusion data GArrowSkeleton m :: * -> * -> * where @@ -83,7 +84,10 @@ type instance GArrowTensor (GArrowSkeleton m) = (,) type instance GArrowUnit (GArrowSkeleton m) = () type instance GArrowExponent (GArrowSkeleton m) = (->) -instance GArrowSTKCL (GArrowSkeleton m) +instance GArrowCopyDropSwapLoop (GArrowSkeleton m) + +instance GArrowInclusion (GArrowSkeleton m) (,) () m where + ga_inc = GAS_misc -- -- | Simple structural equality on skeletons. NOTE: two skeletons @@ -112,8 +116,25 @@ instance Eq ((GArrowSkeleton m) a b) GAS_unassoc === GAS_unassoc = True (GAS_loopl f) === (GAS_loopl f') = f === f' (GAS_loopr f) === (GAS_loopr f') = f === f' + (GAS_misc _) === (GAS_misc _) = True -- FIXME _ === _ = False - -- FIXME: GAS_misc's are never equal!!! + +data OptimizeFlag = DoOptimize | NoOptimize + +mkSkeleton :: OptimizeFlag -> + (forall g . + (GArrow g (,) () + ,GArrowCopy g (,) () + ,GArrowDrop g (,) () + ,GArrowSwap g (,) () + ,GArrowLoop g (,) () + ,GArrowInclusion g (,) () m) => + g x y) + -> GArrowSkeleton m x y +mkSkeleton DoOptimize = \g -> (beautify . optimize) g +mkSkeleton NoOptimize = \g -> g + + -- -- | Performs some very simple-minded optimizations on a diff --git a/examples/GArrowTikZ.hs b/examples/GArrowTikZ.hs index b090c85..66b5295 100644 --- a/examples/GArrowTikZ.hs +++ b/examples/GArrowTikZ.hs @@ -18,7 +18,7 @@ import System.Process import Prelude hiding ( id, (.), lookup ) import Control.Category import Control.Monad.State -import GHC.HetMet.GArrow +import Control.GArrow import Data.List hiding (lookup, insert) import Data.Map hiding (map, (!)) import Data.Maybe (catMaybes) @@ -70,6 +70,28 @@ lowermost (TU x) = x lowermost (TT x y) = lowermost y +class ToDiagram g where + toDiagram :: GArrowPortShape g () x y -> ConstraintM Diagram + +instance (Detect m, ToDiagram m) => ToDiagram (GArrowSkeleton m) where + toDiagram s = mkdiag s + +data Opaque x y where + MkOpaque :: String -> DetectM (GArrowPortShape Opaque UVar x y) -> Opaque x y + +instance Detect Opaque where + detect' (MkOpaque _ dm) = dm + +instance ToDiagram Opaque where + toDiagram (GASPortPassthrough inp outp (MkOpaque s _)) = + do { (top, x ,bot) <- alloc inp + ; (_, y ,_) <- alloc outp + --; constrainEq x y + ; simpleDiag s top x y bot [] } + toDiagram q = mkdiag q + +-- do (top, x ,bot) <- alloc inp +-- simpleDiag' s top x x bot [(x,x)] "gray!50" ------------------------------------------------------------------------------ @@ -171,11 +193,11 @@ alloc1 = do { (t,c) <- get ; return (T t) } -mkdiag :: GArrowPortShape m () a b -> ConstraintM Diagram -mkdiag (GASPortPassthrough inp outp m) = error "not supported" +mkdiag :: ToDiagram m => GArrowPortShape m () a b -> ConstraintM Diagram +mkdiag (GASPortPassthrough inp outp m) = toDiagram (GASPortPassthrough inp outp m) mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x where - mkdiag' :: GArrowSkeleton (GArrowPortShape m ()) a b -> ConstraintM Diagram + mkdiag' :: ToDiagram m => GArrowSkeleton (GArrowPortShape m ()) a b -> ConstraintM Diagram mkdiag' (GAS_comp f g) = do { f' <- mkdiag' f; g' <- mkdiag' g ; constrainEq (getOut f') (getIn g') ; return $ DiagramComp f' g' } @@ -284,26 +306,26 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x ; return $ DiagramLoopBot f' l } mkdiag' (GAS_misc f ) = mkdiag f - diagramBox :: TrackIdentifier -> Tracks -> BoxRenderer -> Tracks -> TrackIdentifier -> ConstraintM Diagram - diagramBox ptop pin r pout pbot = do { constrain ptop LT (uppermost pin) (-1) +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 } - 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 +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 where defren tp x1 y1 x2 y2 = drawBox 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 -draw_assoc = True -draw_first_second = True +draw_assoc = False +draw_first_second = False +--draw_assoc = True +--draw_first_second = True -- constrain that Ports is at least Int units above the topmost portion of Diagram constrainTop :: TrackIdentifier -> Float -> Diagram -> ConstraintM () @@ -487,7 +509,7 @@ lp_solve_to_trackpos s = toTrackPos $ map parse $ catMaybes $ map grab $ lines s 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 :: GArrowSkeleton m a b -> IO String +toTikZ :: (ToDiagram m, Detect m) => GArrowSkeleton m a b -> IO String toTikZ g = let cm = do { let g' = detectShape g ; g'' <- mkdiag g' @@ -509,7 +531,18 @@ tikz :: forall c . (PGArrow g (GArrowTensor g c c) c) -> PGArrow g c c) -> IO () -tikz x = tikz' $ beautify $ optimize $ unG (x (\c -> PGArrowD { unG = GAS_const c }) (PGArrowD { unG = GAS_merge })) +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}" diff --git a/examples/GArrowTutorial.hs b/examples/GArrowTutorial.hs index a993582..be7c930 100644 --- a/examples/GArrowTutorial.hs +++ b/examples/GArrowTutorial.hs @@ -3,7 +3,7 @@ module GArrowTutorial where import Data.Bits import Data.Bool (not) -import GHC.HetMet.GArrow +import Control.GArrow import GHC.HetMet.GuestLanguage hiding ( (-) ) import Control.Category import Control.Arrow diff --git a/examples/Makefile b/examples/Makefile index ff6f713..4e47c6e 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -1,11 +1,15 @@ -ghc_opt := -fwarn-incomplete-patterns -Werror -odir .build -hidir .build +# -fwarn-incomplete-patterns + +ghc = ../../../inplace/bin/ghc-stage2 +#ghc = ghc +ghc_opt := -Werror -odir .build -hidir .build open: make demo open .build/test.pdf #sanity += BiGArrow.hs -sanity += KappaDemo.hs +sanity += IFLDemos.hs sanity += CircuitExample.hs sanity += CommandSyntaxExample.hs sanity += DotProduct.hs @@ -22,13 +26,24 @@ sanity_opts += -fsimpleopt-before-flatten sanity_opts += -odir .build -hidir .build sanity: - for A in $(sanity); do echo; echo; ../../../inplace/bin/ghc-stage2 $(sanity_opts) $$A +RTS -K500M || exit -1; done + for A in $(sanity); do echo; echo; $(ghc) $(sanity_opts) $$A +RTS -K500M || exit -1; done + +demo-pretty: + $(ghc) $(ghc_opt) -main-is GArrowPretty GArrowPretty.hs -o GArrowPretty + +demo-v: + $(ghc) $(ghc_opt) -main-is GArrowVerilog GArrowVerilog.hs -o GArrowVerilog + ./GArrowVerilog +demo-verilog: + $(ghc) $(sanity_opts) -c VerilogDemo.hs + $(ghc) $(ghc_opt) -main-is GArrowVerilog GArrowVerilog.hs -o GArrowVerilog + ./GArrowVerilog demo: mkdir -p .build - ../../../inplace/bin/ghc-stage2 $(ghc_opt) -c Demo.hs -fforce-recomp - ../../../inplace/bin/ghc-stage2 $(ghc_opt) --show-iface .build/Demo.hi - ../../../inplace/bin/ghc-stage2 $(ghc_opt) GArrowTikZ.hs Demo.hs DemoMain.hs Unify.hs -o .build/demo + $(ghc) $(ghc_opt) -c Demo.hs -fforce-recomp + $(ghc) $(ghc_opt) --show-iface .build/Demo.hi + $(ghc) $(ghc_opt) GArrowTikZ.hs Demo.hs DemoMain.hs Unify.hs -o .build/demo ./.build/demo > .build/test.tex cd .build; TEXINPUTS=../tex-bits/:$TEXINPUTS: pdflatex test.tex diff --git a/examples/Stack.hs b/examples/Stack.hs new file mode 100644 index 0000000..19272c2 --- /dev/null +++ b/examples/Stack.hs @@ -0,0 +1,244 @@ +{-# OPTIONS_GHC -XModalTypes -dcore-lint -ddump-types -XNoMonomorphismRestriction #-} +module Stack where +import Prelude hiding (const) + +class ProcessNetwork g where + logic :: ( Bool -> Bool) -> <[ Bool ~~> Bool ]> + logic2 :: (Bool -> Bool -> Bool) -> <[ (Bool,Bool) ~~> Bool ]> + delay :: Bool -> <[ Bool ~~> Bool ]> + select :: <[ (Bool,Bool,Bool) ~~> Bool ]> + switch :: <[ (Bool,Bool) ~~> (Bool,Bool) ]> + +------------------------------------------------------------------------------ +-- +-- Basic logic functions +-- +and' = logic2 (\x y -> x && y) +or' = logic2 (\x y -> x || y) +not' = logic (\x -> case x of {True->False ; False -> True}) + +-- +-- Simulates "conditionally consuming" data from an input port. +-- +-- A value is consumed from "next"; if the value is False, +-- the previous output is repeated. Otherwise, a value is +-- consumed from "input" and emitted as the output. +-- +--peek :: <[ (Bool,Bool) ~~> Bool ]> +peek input next = + <[ \input -> + \next -> + let + prev = ~~(delay True) next + out = select prev input feedback +-- (feedback,_) = switch next out + feedback = switch' next out + in out + ]> + + +------------------------------------------------------------------------------ +-- +-- Numbers are represented in unary (Peano) notation: the number N is +-- N-many False values followed by a single True +-- +type Number = Bool + + +-- +-- Convert a Number to a sequence of False's; the second argument +-- is a stream of Bools, one per Number, indicating whether or not +-- to include the trailing "True" +-- +--numberToBooleans :: <[ (Number,Bool) ~~> Bool ]> +allTrues :: forall g . <[ () ~~> Bool ]>@g +allTrues = undefined +allFalses :: forall g . <[ () ~~> Bool ]>@g +allFalses = undefined + +numberToBooleans = + <[ \numbers -> + \includeTrailingTrue -> + let sel = select numbers includeTrailingTrue ~~allTrues +-- (out,_) = switch sel numbers + out = switch' sel numbers + in out + ]> + + +------------------------------------------------------------------------------ +-- +-- Increment, decrement, and zero-test for Numbers. Each of these +-- follows a similar pattern: keep a copy of the previous input, and +-- "pattern match" on a pair of consecutive bits. +-- +--decrement :: <[ Number ~~> Number ]> +decrement = + <[ \input -> + let isFirstBitOfNumber = ~~(delay True) input + isFirstBitOfNonzeroNumber = ~~and' (~~not' input) isFirstBitOfNumber +-- (_,out) = switch isFirstBitOfNonzeroNumber input + out = switch' isFirstBitOfNonzeroNumber input + in out + ]> + +--increment :: <[ Number ~~> Number ]> +increment = + <[ \input -> + let isFirstBitOfNumber = ~~(delay True) out + out = select isFirstBitOfNumber ~~allFalses input + in out + ]> + +--isZero :: <[ Number ~~> Bool ]> +isZero = + <[ \input -> + let prev = ~~(delay True) input +-- (out,_) = switch input (~~and' prev input) + out = switch' input (~~and' prev input) + in out + ]> + + +------------------------------------------------------------------------------ +-- +-- Versions of the "select" and "select" operators that act on Numbers +-- (the "select" port is still boolean). +-- +-- numberSelect :: <[ (Bool,Number,Number) ~~> Number ]> +{- +numberSelect = + <[ \sel -> + \iftrue -> + \iffalse -> + let sel' = ~~peek sel next_sel + out = select sel' iftrue iffalse + next_sel = out + in out + ]> +-} + +numberSwitch :: <[ (Bool,Number) ~~> (Number,Number) ]> +{- +numberSwitch = + <[ \sel -> + \input -> + let sel' = ~~peek sel next_sel + out = switch sel' input + next_sel = input + in out + ]> +-} + +numberSelect :: <[ (Bool,(Number,(Number,()))) ~~> Number ]>@g +numberSelect = undefined + +------------------------------------------------------------------------------ +-- +-- An example of a functional: given two process networks which each +-- take a Number in and produce a Number output, route each incoming +-- Number to one side or the other based on a control token. +-- +{- +maybeNumber :: ([Number] -> [Number]) -> + ([Number] -> [Number]) -> + [Bool] -> + [Number] -> + [Number] + +maybeNumber ftrue ffalse sel input = + let (inputTrue,inputFalse) = numberSwitch sel input + in numberSelect sel (ftrue inputTrue) (ffalse inputFalse) +-} +maybeNumber :: + <[ Number ~~> Number ]>@g -> + <[ Number ~~> Number ]>@g -> + <[ (Bool,Number) ~~> Number ]>@g +maybeNumber = undefined + + +------------------------------------------------------------------------------ +stack = + <[ \commandIsPop -> + \push -> + let + -- relatively straightforward: the counter, counter update, and emptiness test: + count = ~~(delay True) newCount + newCount = ~~maybeNumber ~~decrement ~~increment commandIsPop count + isEmpty = ~~isZero count + pushOrPopEmpty = ~~or' (~~not' commandIsPop) isEmpty + + -- First stage: popping from an empty stack is implemented by + -- synthesizing a zero value, pushing it, and then popping it. + -- This first stage synthesizes the zero-value if necessary + (popEmptyResult,_) = ~~numberSwitch + pushOrPopEmpty + (~~numberSelect + commandIsPop + ~~allTrues + push) + + -- Second stage: this select copies the existing stack storage + -- from its first input to its output, optionally *preceding* it + -- with a single value drawn from its second input. + pushResult = ~~numberSelect + (~~numberToBooleans count pushOrPopEmpty) + popEmptyResult + stackStorage + + -- Third stage: copy the result of the "push" operation to its + -- second output, optionally diverting the *first* element to the + -- first output. + (popResult,stackStorage) = ~~numberSwitch + (numberToBooleans newCount commandIsPop) + pushResult + + in popResult + ]> + +{- + +------------------------------------------------------------------------------ +-- +-- Boilerplate +-- + + +int2p 0 = [True] +int2p n = False:(int2p (n-1)) + + +p2i (True:xs) = 0:(p2i xs) +p2i (False:xs) = case p2i xs of n:ns -> (n+1):ns +p2i _ = [] + +--x = peek [1,2,3,4,5,6,7,8] [True,True,False,False,True,False] +--x = p2i $ numberSelect [False,True,True,False] even odd +--x = p2i $ fst (numberSwitch [False,True,True,False,True] all) +--x = p2i $ increment even +x = p2i $ stack [True,True,False,False,False,True,True,False,True,True,True,True,True] odd + where + even = concatMap int2p [9,0,2,4,6] + odd = concatMap int2p [9,1,3,5] + all = concatMap int2p [1,2,0,2,3,4,9,9] + +main = do sequence $ map putStrLn $ map show x + +logic1 f in1 = map f in1 +logic2 f in1 in2 = map f (zip in1 in2) + +delay x = \n -> x:n + +select sel iftrue iffalse = + case sel of + (True :sel') -> case iftrue of { (x:iftrue') -> x:(select sel' iftrue' iffalse) ; _ -> [] } + (False:sel') -> case iffalse of { (x:iffalse') -> x:(select sel' iftrue iffalse') ; _ -> [] } + [] -> [] + +switch (True:sel) (x:inp) = let (out1,out2) = switch sel inp in ((x:out1),out2) +switch (False:sel) (x:inp) = let (out1,out2) = switch sel inp in (out1,(x:out2)) +switch _ _ = ([],[]) + +allTrues = delay True allTrues +allFalses = delay False allFalses +-} \ No newline at end of file diff --git a/examples/TuringMachine.hs b/examples/TuringMachine.hs new file mode 100644 index 0000000..df3ac31 --- /dev/null +++ b/examples/TuringMachine.hs @@ -0,0 +1,81 @@ +{-# OPTIONS_GHC -XModalTypes -dcore-lint -ddump-types -XNoMonomorphismRestriction #-} +module TuringMachine (ProcessNetwork) where +import Prelude hiding (const) + +class ProcessNetwork g where + logic :: (Bool -> Bool -> Bool) -> <[ (Bool,(Bool,())) ~~> Bool ]>@g + delay :: Bool -> <[ (Bool,()) ~~> Bool ]>@g + <[ select ]> :: <[ (Bool,(Bool,(Bool,()))) ~~> Bool ]>@g + <[ switch ]> :: <[ (Bool,(Bool,())) ~~> (Bool,Bool) ]>@g + <[ switch' ]> :: <[ (Bool,(Bool,())) ~~> Bool ]>@g + + +or = logic (\x y -> x || y) + +not :: ProcessNetwork g => <[ (Bool,()) ~~> Bool ]>@g +not = undefined + + + + +-- every time it gets an input it spits out the same output value +const :: ProcessNetwork g => Bool -> <[ (Bool,()) ~~> Bool ]>@g +const = undefined + +-- +-- VERY IMPORTANT! +-- +-- Bool is the type of booleans in Haskell. +-- <[Bool]> is the type of a process network arc in which EACH TOKEN is a boolean. +-- +-- This can lead to some slightly-confusing notation: +-- +-- (Bool -> Bool) is a Haskell function that takes a boolean and +-- (if it halts) returns a Boolean. +-- +-- <[Bool ~~> Bool]> is a process network with an input arc whose +-- tokens are booleans and an output arc whose +-- tokens are booleans +-- + +-- +-- Think of Haskell values as being like Ptolemy model parameters! +-- + +condConst initVal = + <[ \condition -> ~~(const initVal) (switch' condition condition) ]> + + +-- +-- The size of the stack is a natural number; these will be +-- represented as a stream of values using *unary notation* in the +-- following form: the number N is represented as "true" followed by +-- N-many "false" values. +-- + +-- +-- A UnaryNumber is just a stream that we give a particular meaning +-- to. We're going to get some help here from Haskell's type system +-- by creating another type UnaryNumber, but not telling our code that +-- it's actually the same thing as a Stream. This prevents us from +-- accidentally using a non-UnaryNumber stream where a UnaryNumber was +-- required! +-- +type UnaryNumber = Bool + + +type IncDec = Bool + +counter :: ProcessNetwork g => <[ IncDec ~~> UnaryNumber ]>@g +counter = undefined + + + + + +-- show myself making a type error + + +-- Investigate later: automatic translation from <[PeanoStream~~>PeanoStream]> to <[Bool~~>Bool]> + +-- show why innocuous Haskell program transforms alter the behavior of PNs \ No newline at end of file diff --git a/examples/Unflattening.hs b/examples/Unflattening.hs index f9ca4ba..6dfbf78 100644 --- a/examples/Unflattening.hs +++ b/examples/Unflattening.hs @@ -2,7 +2,7 @@ module Unflattening where import GHC.HetMet.CodeTypes hiding ((-)) -import GHC.HetMet.GArrow +import Control.GArrow import Control.Category import Control.Arrow import Prelude hiding ( id, (.) ) diff --git a/examples/VerilogDemo.hs b/examples/VerilogDemo.hs new file mode 100644 index 0000000..9c0b4fd --- /dev/null +++ b/examples/VerilogDemo.hs @@ -0,0 +1,9 @@ +{-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint -XScopedTypeVariables -fsimpleopt-before-flatten -XKindSignatures #-} +module VerilogDemo (oscillator) where + +oscillator :: <[ (w,()) ~~> w ]>@a -> <[ (w,(w,())) ~~> w ]>@a -> <[ (w,()) ~~> w ]>@a +oscillator reg xor = + <[ \input -> + let output = ~~xor input delayed + delayed = ~~reg output + in output ]> diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 9f0fc1a..42a29ed 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -547,9 +547,9 @@ Section core2proof. dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa" >>= fun hetmet_kappa => dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa_app" >>= fun hetmet_kappa_app => dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow => - dsLookupTyc "GHC.HetMet.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit => - dsLookupTyc "GHC.HetMet.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor => - dsLookupTyc "GHC.HetMet.GArrow" "GArrowExponent" >>= fun hetmet_PGArrow_exponent => + dsLookupTyc "Control.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit => + dsLookupTyc "Control.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor => + dsLookupTyc "Control.GArrow" "GArrowExponent" >>= fun hetmet_PGArrow_exponent => dsLookupVar "GHC.HetMet.Private" "pga_id" >>= fun hetmet_pga_id => dsLookupVar "GHC.HetMet.Private" "pga_comp" >>= fun hetmet_pga_comp => dsLookupVar "GHC.HetMet.Private" "pga_first" >>= fun hetmet_pga_first => -- 1.7.10.4