{-# 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, (.) )
--- /dev/null
+{-# 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
+
{-# 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, (.) )
{-# 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)
}>
-}
-demo const mult =
- <{ \y ->
- let foo = ~~mult (~~mult foo (~~mult y foo)) y
- in foo }>
-
-
import Control.Category
import GArrowTikZ
import GHC.HetMet.Private
-import GHC.HetMet.GArrow
+import Control.GArrow
import Demo
main = tikz demo
--- /dev/null
+applyCircuit =
+ <[ \higherOrderCircuit -> \arg -> higherOrderCircuit arg ]>
--- /dev/null
+
+
+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
+
--- /dev/null
+{-# 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
-- 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
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
; 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
--- /dev/null
+{-# 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
+
--- /dev/null
+{-# 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
-{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleContexts, FlexibleInstances, TypeFamilies, RankNTypes #-}
-----------------------------------------------------------------------------
-- |
-- Module : GArrowSkeleton
--
-- 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
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
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
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)
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"
------------------------------------------------------------------------------
; 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' }
; 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 ()
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'
(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}"
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
-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
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
--- /dev/null
+{-# 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
--- /dev/null
+{-# 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
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, (.) )
--- /dev/null
+{-# 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 ]>
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 =>
projects / coq-hetmet.git / commitdiff