From caa7ad74b99b34abc5181553e66423da6bdfee26 Mon Sep 17 00:00:00 2001
From: Adam Megacz
Date: Tue, 29 Mar 2011 04:15:27 0700
Subject: [PATCH] reorganized examples directory

examples/BiGArrow.hs  100 ++++
examples/CircuitExample.hs  48 ++
examples/CommandSyntaxExample.hs  40 ++
examples/DotProduct.hs  65 +++
examples/GArrowTutorial.hs  214 +++++++++
examples/GArrowVerilog.hs  65 +++
examples/ImmutableHeap.hs  23 +
examples/IsomorphismForCodeTypes.hs  12 +
examples/LambdaCalculusInterpreter.hs  49 ++
examples/RegexMatcher.hs  163 +++++++
examples/TypeSafeRun.hs  35 ++
examples/Unflattening.hs  47 ++
examples/tutorial.hs  827 
13 files changed, 861 insertions(+), 827 deletions()
create mode 100644 examples/BiGArrow.hs
create mode 100644 examples/CircuitExample.hs
create mode 100644 examples/CommandSyntaxExample.hs
create mode 100644 examples/DotProduct.hs
create mode 100644 examples/GArrowTutorial.hs
create mode 100644 examples/GArrowVerilog.hs
create mode 100644 examples/ImmutableHeap.hs
create mode 100644 examples/IsomorphismForCodeTypes.hs
create mode 100644 examples/LambdaCalculusInterpreter.hs
create mode 100644 examples/RegexMatcher.hs
create mode 100644 examples/TypeSafeRun.hs
create mode 100644 examples/Unflattening.hs
delete mode 100644 examples/tutorial.hs
diff git a/examples/BiGArrow.hs b/examples/BiGArrow.hs
new file mode 100644
index 0000000..466fbc2
 /dev/null
+++ b/examples/BiGArrow.hs
@@ 0,0 +1,100 @@
+{# OPTIONS_GHC XModalTypes XMultiParamTypeClasses ddumptypes XNoMonoPatBinds XFlexibleInstances XGADTs XUndecidableInstances #}
+module BiGArrow
+where
+import GHC.HetMet.GArrow
+import Control.Category
+import Control.Arrow
+import Prelude hiding ( id, (.) )
+
+
+
+
+ BiGArrows
+
+class GArrow g (**) u => BiGArrow g (**) u where
+  Note that we trust the user's pair of functions actually are
+  mutually inverse; confirming this in the type system would
+  require very powerful dependent types (such as Coq's). However,
+  the consequences of failure here are much more mild than failures
+  in BiArrow.inv: if the functions below are not mutually inverse,
+  the LoggingBiGArrow will simply compute the wrong result rather
+  than fail in some manner outside the language's semantics.
+ biga_arr :: (x > y) > (y > x) > g x y
+ biga_inv :: g x y > g y x
+
+
+
+
+
+ GArrowpairs are BiGArrows (but not a GArrowDrop!)
+
+ For any GArrow instance, its mutually inverse pairs form a BiGArrow
+data GArrow g (**) u => GArrowInversePair g (**) u x y =
+ GArrowInversePair { forward :: g x y , backward :: g y x }
+instance GArrow g (**) u => Category (GArrowInversePair g (**) u) where
+ id = GArrowInversePair { forward = id , backward = id }
+ f . g = GArrowInversePair { forward = (forward f) . (forward g) , backward = (backward g) . (backward f) }
+instance GArrow g (**) u => GArrow (GArrowInversePair g (**) u) (**) u where
+ ga_first f = GArrowInversePair { forward = ga_first (forward f), backward = ga_first (backward f) }
+ ga_second f = GArrowInversePair { forward = ga_second (forward f), backward = ga_second (backward f) }
+ ga_cancell = GArrowInversePair { forward = ga_cancell , backward = ga_uncancell }
+ ga_cancelr = GArrowInversePair { forward = ga_cancelr , backward = ga_uncancelr }
+ ga_uncancell = GArrowInversePair { forward = ga_uncancell , backward = ga_cancell }
+ ga_uncancelr = GArrowInversePair { forward = ga_uncancelr , backward = ga_cancelr }
+ ga_assoc = GArrowInversePair { forward = ga_assoc , backward = ga_unassoc }
+ ga_unassoc = GArrowInversePair { forward = ga_unassoc , backward = ga_assoc }
+instance GArrowSwap g (**) u => GArrowSwap (GArrowInversePair g (**) u) (**) u where
+ ga_swap = GArrowInversePair { forward = ga_swap , backward = ga_swap }
+ but notice that we can't (in general) get
+ instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ...
+
+
+
+
+
+ BCPierce's symmetric lenses form a BiGArrow *with* GArrowSwap
+
+
+ NOTE: if you uncomment, this BE SURE YOU ARE NOT USING fcoqpass 
+ the code below will trigger one of the notyetfixed bugs in the
+ code that turns GHC CoreSyn into stronglytyped Coq expressions.
+
+{
+data Lens x y where
+ Lens :: forall x y c1 c2 . ((x,c1)>(y,c2)) > ((y,c2)>(x,c1)) > Lens x y
+
+ can we make lenses out of GArrows other than (>)?
+instance Category Lens where
+ id = Lens (\x > x) (\x > x)
+ (Lens g1 g2) . (Lens f1 f2) = Lens (\(x,(c1,c2)) > let (y,fc) = f1 (x,c1) in let (z,gc) = g1 (y,c2) in (z,(fc,gc)))
+ (\(z,(c1,c2)) > let (y,gc) = g2 (z,c2) in let (x,fc) = f2 (y,c1) in (x,(fc,gc)))
+
+instance GArrow Lens (,) () where
+ ga_first (Lens f1 f2) = Lens (\((x1,x2),c) > let (y,c') = f1 (x1,c) in ((y,x2),c'))
+ (\((x1,x2),c) > let (y,c') = f2 (x1,c) in ((y,x2),c'))
+ ga_second (Lens f1 f2) = Lens (\((x1,x2),c) > let (y,c') = f1 (x2,c) in ((x1,y),c'))
+ (\((x1,x2),c) > let (y,c') = f2 (x2,c) in ((x1,y),c'))
+ ga_cancell = Lens (\(((),x),()) > ( x ,()))
+ (\( x ,()) > (((),x),()))
+ ga_uncancell = Lens (\( x ,()) > (((),x),()))
+ (\(((),x),()) > ( x ,()))
+ ga_cancelr = Lens (\((x,()),()) > ( x ,()))
+ (\( x ,()) > ((x,()),()))
+ ga_uncancelr = Lens (\( x ,()) > ((x,()),()))
+ (\((x,()),()) > ( x ,()))
+ ga_assoc = Lens (\(((x,y),z),()) > ((x,(y,z)),()))
+ (\((x,(y,z)),()) > (((x,y),z),()))
+ ga_unassoc = Lens (\((x,(y,z)),()) > (((x,y),z),()))
+ (\(((x,y),z),()) > ((x,(y,z)),()))
+
+instance GArrowDrop Lens (,) () where
+ ga_drop = Lens (\(x,()) > ((),x)) (\((),x) > (x,()))
+instance GArrowCopy Lens (,) () where
+ ga_copy = Lens (\(x,()) > ((x,x),())) (\((x,_),()) > (x,()))
+instance GArrowSwap Lens (,) () where
+ ga_swap = Lens (\((x,y),()) > ((y,x),())) (\((x,y),()) > ((y,x),()))
+
+instance BiGArrow Lens (,) () where
+ biga_arr f f' = Lens (\(x,()) > ((f x),())) (\(x,()) > ((f' x),()))
+ biga_inv (Lens f1 f2) = Lens f2 f1
+}
diff git a/examples/CircuitExample.hs b/examples/CircuitExample.hs
new file mode 100644
index 0000000..f4f5151
 /dev/null
+++ b/examples/CircuitExample.hs
@@ 0,0 +1,48 @@
+{# OPTIONS_GHC XModalTypes ddumptypes XNoMonoPatBinds XMultiParamTypeClasses XTypeOperators #}
+module CircuitExample
+where
+import GHC.HetMet.CodeTypes hiding (())
+import GHC.HetMet.GArrow
+import Control.Category
+import Prelude hiding ( id, (.) )
+
+
+ From the Appendix of Hughes' __Programming with Arrows__
+
+
+class GArrowLoop g (**) u => GArrowCircuit g (**) u b where
+ delay :: Bool > g b b
+
+ GArrows which can implment LookUp Tables (LUTs)
+class GArrow g (**) u => GArrowLUT g (**) u b where
+ lut1 :: ( Bool > Bool) > g b b
+ lut2 :: ((Bool,Bool) > Bool) > g (b,b) b
+ lut3 :: ((Bool,Bool,Bool) > Bool) > g (b,b,b) b
+
+nor = lut2 (not.uncurry ())
+
+flipflop = ga_loopl $ ga_second ga_swap >>>
+ ga_assoc >>>
+ ga_second ga_unassoc >>>
+ ga_second (ga_first ga_swap) >>>
+ ga_second ga_assoc >>>
+ ga_unassoc >>>
+ ga_first nor >>>
+ ga_second nor >>>
+ ga_first (delay False) >>>
+ ga_second (delay True) >>>
+ ga_copy
+
+edge = ga_copy >>>
+ ga_first (delay False) >>>
+ lut2 (\(x,y) > x && (not y))
+
+ halfAdd :: Arrow arr => arr (Bool,Bool) (Bool,Bool)
+ halfAdd = proc (x,y) > returnA < (x&&y, x/=y)
+
+ fullAdd :: Arrow arr => arr (Bool,Bool,Bool) (Bool,Bool)
+ fullAdd =
+ proc (x,y,c) > do
+ (c1,s1) < halfAdd < (x,y)
+ (c2,s2) < halfAdd < (s1,c)
+ returnA < (c1c2,s2)
diff git a/examples/CommandSyntaxExample.hs b/examples/CommandSyntaxExample.hs
new file mode 100644
index 0000000..e06920c
 /dev/null
+++ b/examples/CommandSyntaxExample.hs
@@ 0,0 +1,40 @@
+{# OPTIONS_GHC XModalTypes XMultiParamTypeClasses ddumptypes XNoMonoPatBinds #}
+module CommandSyntaxExample
+where
+
+
+ Please ignore this; I never got around to implementing it.
+
+
+{
+The example may seem a little contrived, but its purpose is to
+illustrate the be haviour when the argument of mapC refers both to
+its parameter and a free vari able (n).
+
+\begin{verbatim}
+ we can use mapA rather than mapC (from page 100)
+
+mapA f = proc xs > case xs of
+[] > returnA < [] x:xsâ > do y < f < x
+ysâ < mapA f < xsâ returnA < y:ys
+
+example2 =
+ <[ \(n,xs) >
+ ~(mapA <[ \x> (~(delay 0) n, x) ]> )
+ xs
+ ]>
+
+<[ example2 (n,xs) =
+ ~(mapA <[ \x> (~(delay 0) n, x) ]> ) xs ]>
+\end{verbatim}
+
+
+ from Hughes' "programming with Arrows"
+
+mapC :: ArrowChoice arr => arr (env,a) b > arr (env,[a]) [b] mapC c = proc (env,xs) >
+case xs of [] > returnA < [] x:xsâ > do y < c < (env,x)
+ys < mapC c < (env,xsâ) returnA < y:ys
+
+example2 = proc (n,xs) > ( mapC (\x> do delay 0 < n
+&&& do returnA < x) ) xs
+}
diff git a/examples/DotProduct.hs b/examples/DotProduct.hs
new file mode 100644
index 0000000..6de0c01
 /dev/null
+++ b/examples/DotProduct.hs
@@ 0,0 +1,65 @@
+{# OPTIONS_GHC XModalTypes ddumptypes XNoMonoPatBinds XFlexibleContexts #}
+module DotProduct
+where
+import GHC.HetMet.CodeTypes hiding (())
+import Prelude hiding ( id, (.) )
+
+
+ Dot Product
+
+ This shows how to build a twolevel program one step at a time by
+ slowly rearranging it until the brackets can be inserted.
+
+
+ a onelevel function to compute the dot product of two vectors
+dotproduct :: [Int] > [Int] > Int
+dotproduct v1 v2 =
+ case v1 of
+ [] > 0
+ (a:ax) > case v2 of
+ [] > 0
+ (b:bx) >
+ (a*b)+(dotproduct ax bx)
+
+ A slightly modified version of the dot product: note that we
+ check for zeroes and ones to avoid multiplying. In a onelevel
+ program this yields no advantage, however!
+dotproduct' :: [Int] > [Int] > Int
+dotproduct' v1 v2 =
+ case v1 of
+ [] > 0
+ (0:ax) > case v2 of
+ [] > 0
+ (b:bx) > (dotproduct' ax bx)
+ (1:ax) > case v2 of
+ [] > 0
+ (b:bx) > b+(dotproduct' ax bx)
+ (a:ax) > case v2 of
+ [] > 0
+ (b:bx) >
+ (a*b)+(dotproduct' ax bx)
+
+ A twolevel version of the dot product. Note how we ask for the first
+ vector, then produce a program which is optimized for multiplying
+ by that particular vector. If there are zeroes or ones in the
+ original vector, we will emit code which is faster than a onelevel
+ dot product.
+
+dotproduct'' :: forall g.
+ GuestLanguageAdd g Integer =>
+ GuestLanguageMult g Integer =>
+ GuestIntegerLiteral g =>
+ [Integer] > <[ [Integer] > Integer ]>@g
+dotproduct'' v1 =
+ case v1 of
+ [] > <[ \v2 > 0 ]>
+ (0:ax) > <[ \v2 > case v2 of
+ [] > 0
+ (b:bx) > ~~(dotproduct'' ax) bx ]>
+ (1:ax) > <[ \v2 > case v2 of
+ [] > 0
+ (b:bx) > b + ~~(dotproduct'' ax) bx ]>
+
+ (a:ax) > <[ \v2 > case v2 of
+ [] > 0
+ (b:bx) > ~~(guestIntegerLiteral a) * b + ~~(dotproduct'' ax) bx ]>
diff git a/examples/GArrowTutorial.hs b/examples/GArrowTutorial.hs
new file mode 100644
index 0000000..c614d0d
 /dev/null
+++ b/examples/GArrowTutorial.hs
@@ 0,0 +1,214 @@
+{# OPTIONS_GHC XModalTypes XScopedTypeVariables XFlexibleContexts XMultiParamTypeClasses ddumptypes XNoMonoPatBinds #}
+module GArrowTutorial
+where
+import Data.Bits
+import Data.Bool (not)
+import GHC.HetMet.CodeTypes hiding (())
+import GHC.HetMet.GArrow
+import Control.Category
+import Control.Arrow
+import Prelude hiding ( id, (.) )
+
+ The best way to understand heterogeneous metaprogramming and
+ generalized arrows is to play around with this file, poking at the
+ examples until they fail to typecheck  you'll learn a lot that
+ way!
+
+ Once you've built the modified compiler, you can compile this file
+ with:
+
+ $ inplace/bin/ghcstage2 tutorial.hs
+
+
+ XModalTypes adds a new syntactical expression, "code brackets":
+code_fst = <[ \(x,y) > x ]>
+
+ This new expression is the introduction form for modal types:
+code_fst :: forall a b g. <[ (a,b) > a ]>@g
+
+ Think of <[T]>@g as being the type of programs written in language
+ "g" which, when "executed", return a value of type "T". I mention
+ "language g" because the *heterogeneous* aspect of HetMet means
+ that we can limit the sorts of constructs allowed inside the code
+ brackets, permitting only a subset of Haskell (you have to use
+ Haskell syntax, though).
+
+ There is a second new expression form, "~~", called "escape":
+
+code_fst_fst = <[ \z > ~~code_fst (~~code_fst z) ]>
+
+ Note that ~~ binds more tightly than any other operator. There is
+ an alternate version, "~~$", which binds more weakly than any other
+ operator (this is really handy sometimes!). To demonstrate this,
+ the next two expressions differ only in superficial syntax:
+
+example1 foo bar = <[ ~~$ foo bar ]>
+example2 foo bar = <[ ~~( foo bar) ]>
+ example3 foo bar = <[ ~~ foo bar ]>
+
+ ... but the third one is completely different (and in fact, doesn't
+ even parse, but we'll get to that in a moment)
+
+ The escape operation must appear within code brackets. In truth,
+ it is really a "hole" punched in the code brackets  the thing to
+ which the escape operator gets applied is typed as if it were
+ *outside* the code brackets. It must have type <[T]>, and the
+ escape operator allows it to be used *inside* code brackets as if
+ it had type "T".
+
+ So, the escape operator is basically a way of pasting code
+ fragments into each other.
+
+ This is where those type variables after the "@" sign come in: if
+ you paste two pieces of code into a third, all three must be
+ written in the same language. We express this by unifying their
+ tyvars:
+
+compose_code :: forall g a b c. <[a>b]>@g > <[b>c]>@g > <[a>c]>@g
+compose_code x y = <[ \z > ~~y (~~x z) ]>
+
+ Now, try commenting out the type ascription above and uncommenting
+ any of these three:
+
+ compose_code :: forall g h a b c. <[a>b]>@h > <[b>c]>@g > <[a>c]>@g
+ compose_code :: forall g h a b c. <[a>b]>@g > <[b>c]>@h > <[a>c]>@g
+ compose_code :: forall g h a b c. <[a>b]>@g > <[b>c]>@g > <[a>c]>@h
+
+
+ The typechecker won't let you get away with that  you're trying
+ to force a type which is "too polymorphic" onto paste2. If the
+ compiler allowed that, the resulting metaprogram might try to
+ splice together programs written in different languages, resulting
+ in mayhem.
+
+ NEW SCOPING RULES: The syntactical depth (or just "depth") of an
+ expression is the number of surrounding codebrackets minus the
+ number of surrounding escapes (this is strictly a syntax concept
+ and has NOTHING to do with the type system!). It is very important
+ to keep in mind that the scope of a bound variable extends only to
+ expressions at the same depth! To demonstrate, the following
+ expression will fail to parse:
+
+ badness = \x > <[ x ]>
+
+ ...and in the following expression, the occurrence of "x" is bound
+ by the first (outer) lambda, not the second one:
+
+no_shadowing_here = \x > <[ \x > ~~x ]>
+
+ Lastly, you can wrap codebrackets around an identifier in a
+ toplevel, let, or where binding. Notice how GHC doesn't complain
+ here about defining an identifier twice!
+
+foo = \x > x+1
+<[ foo ]> = <[ \(x::Bool) > x ]>
+
+ Now you can use foo (the second one!) inside codebrackets:
+
+bar x = <[ foo ~~x ]>
+
+bar :: forall g. <[Bool]>@g > <[Bool]>@g
+
+ In fact, the identifiers have completely unrelated types. Which
+ brings up another important point: types are ALWAYS assigned
+ "relative to" depth zero. So although we imagine "foo" existing at
+ depthone, its type is quite firmly established as <[ Bool > Bool ]>
+
+ It has to be this way  to see why, consider a term which is more
+ polymorphic than "foo":
+
+<[ foo' ]> = <[ \x > x ]>
+
+ Its type is:
+
+<[ foo' ]> :: forall a g . <[ a > a ]>@g
+
+ ...and there's no way to express the gpolymorphism entirely from
+ within the brackets.
+
+ So why does all of this matter? Mainly so that we can continue to use . We'd like
+ the "+" operator to work "as expected"  in other words, we'd like
+ people to be able to write things like
+
+increment_at_level1 = <[ \x > x + 1 ]>
+
+ However, in unmodified haskell an identifier like (+) may have only
+ one type. In this case that type is:
+
+ (+) :: Num a => a > a > a
+
+ Now, we could simply decree that when (+) appears inside code
+ brackets, an "implicit ~~" is inserted, so the desugared expression
+ is:
+
+ increment_at_level1 = <[ \x > ~~(+) x 1 ]>
+
+ unfortunately this isn't going to work for guest languages that
+ don't have higherorder functions. Haskell uses curried arguments
+ because it has higherorder functions, but in a firstorder guest
+ language a more sensible type for (+) would be:
+
+ (+) :: Num a => (a,a) > a
+
+ ... or even something less polymorphic, like
+
+ (+) :: (Int,Int) > Int
+
+ so to maintain flexibility, we allow an identifier to have
+ different types at different syntactic depths; this way type
+ choices made for Haskell don't get imposed on guest languages that
+ are missing some of its features.
+
+ In hindsight, what we REALLY want is for increment_at_level1 to
+ be desugared like this (much like the Arrow (...) syntax):
+
+ increment_at_level1 = <[ \x > ~~( <[x]> + <[1]> ) ]>
+
+ ... because then we can declare
+
+ instance Num a => Num <[a]> where ...
+
+ or just
+
+ instance Num <[Int]> where ...
+
+ unfortunately there's a major problem: knowing how to do this sort
+ of desugaring requires knowing the *arity* of a function. For
+ symbols we can kludge it by checking Haskell's parsing rules (there
+ are only a handful of unary symbols; all others are binary), but
+ this is crude and won't work at all for nonsymbol identifiers.
+ And we can look at a type like x>y>z and say "oh, that's a
+ twoargument function", but sometimes GHC doesn't know the complete
+ type of an identifier in the midst of unification (i.e. "x has type
+ Int>a for some a, where a could be Int or Int>Int"), so guessing
+ the arity from the type cannot be done during parsing, which is
+ when we need to do this.
+
+ Okay, I think that's more or less a brain dump of why I changed the
+ scoping rules and the problems with the other solutions I tried.
+
+ I am very interested in hearing any suggestions on better ways of
+ dealing with this, so long as you can still use operators like (+)
+ in guest languages without higherorder functions.
+
+
+
+ Ye Olde and Most Venerable "pow" Function
+
+pow :: forall c. GuestIntegerLiteral c => GuestLanguageMult c Integer => Integer > <[ Integer > Integer ]>@c
+pow n =
+ if n==0
+ then <[ \x > 1 ]>
+ else <[ \x > x * ~~(pow (n  1)) x ]>
+
+
+ a more efficient twolevel pow
+pow' :: forall c. GuestIntegerLiteral c => GuestLanguageMult c Integer => Integer > <[ Integer > Integer ]>@c
+pow' 0 = <[ \x > 1 ]>
+pow' 1 = <[ \x > x ]>
+pow' n = if n `mod` 2==0
+ then <[ \x > (\y > y*y) (~~(pow' $ n `shiftR` 2) x) ]>
+ else <[ \x > x * ~~(pow' $ n1) x ]>
+
+
+
diff git a/examples/GArrowVerilog.hs b/examples/GArrowVerilog.hs
new file mode 100644
index 0000000..c867dac
 /dev/null
+++ b/examples/GArrowVerilog.hs
@@ 0,0 +1,65 @@
+{# OPTIONS_GHC XModalTypes XMultiParamTypeClasses ddumptypes XNoMonoPatBinds #}
+module GArrowVerilog
+where
+import Prelude hiding ( id, (.) )
+
+
+ Please ignore this; I didn't manage to finish it
+
+
+
+{
+ A verilog module is an SDoc (chunk of text) giving the module's
+ definition. The UniqueSupply avoids name clashes.
+data VerilogModule =
+ VerilogModule
+ [VerilogModule]  dependencies
+ String >  module name
+ (Tree String >  input port names
+ Tree String >  output port names
+ SDoc)  raw verilog code for the body
+
+
+instance Show VerilogModule where
+ show VerilogModule dep name body =
+ "module "++name++"(FIXME)"++(body FIXME FIXME)
+
+data VerilogWrappedType a =
+ { vwt_rep :: String }
+
+ A "verilog garrow" from A to B is, concretely, the source code for a
+ verilog module having input ports of type A and output ports of type B;
+ the UniqueSupply lets us generate names.
+data GArrowVerilog a b =
+ UniqueSupply >
+ VerilogWrappedType a >
+ VerilogWrappedType b >
+ GArrowVerilog SDoc
+
+instance GArrow GArrowVerilog (,) where
+ ga_id = VerilogModule [] "ga_id" (\ inp outp > zipTree ... "assign "++outp++" = "++inp)
+ ga_comp f g = VerilogModule [] "ga_comp"
+ ga_first :: g x y > g (x ** z) (y ** z)
+ ga_second f = ga_comp (ga_comp ga_swap (ga_first f)) ga_swap
+ ga_cancell f = VerilogModule [] "ga_cancell" (\ [in1,in2] [outp] > "assign "++outp++" = "++in2)
+ ga_cancelr f = VerilogModule [] "ga_cancelr" (\ [in1,in2] [outp] > "assign "++outp++" = "++in1)
+ ga_uncancell f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] > "assign "++out1++"=1'b0;\n assign"++out2++"="++in1)
+ ga_uncancelr f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] > "assign "++out2++"=1'b0;\n assign"++out1++"="++in1)
+ ga_assoc f =
+ ga_unassoc :: g (x**(y**z)) ((x**y)**z)
+
+instance GArrowDrop GArrowVerilog (,) where
+ ga_drop =
+
+instance GArrowCopy GArrowVerilog (,) where
+ ga_copy =
+
+instance GArrowSwap GArrowVerilog (,) where
+ ga_swap =
+
+instance GArrowLoop GArrowVerilog (,) where
+ ga_loop =
+
+instance GArrowLiteral GArrowVerilog (,) where
+ ga_literal =
+}
diff git a/examples/ImmutableHeap.hs b/examples/ImmutableHeap.hs
new file mode 100644
index 0000000..56ff12c
 /dev/null
+++ b/examples/ImmutableHeap.hs
@@ 0,0 +1,23 @@
+{# OPTIONS_GHC XModalTypes XScopedTypeVariables ddumptypes XNoMonoPatBinds #}
+module ImmutableHeap
+where
+import IsomorphismForCodeTypes
+import Prelude hiding ( id, (.) )
+
+
+class GuestLanguageHeap c where
+ alloc :: <[ (Integer,Integer) > Integer ]>@c
+ lookup :: <[ Integer > (Integer,Integer) ]>@c
+
+
+ Here's nice example of Sheard's observation that it's often easier
+ to write twostage programs by applying "back" to some function rather than
+ writing the final result directly
+
+onetwocycle = back onetwocycle'
+ where
+ onetwocycle' xy = <[ let (x,y) = ~~xy
+ in let x' = ~~alloc (1,x)
+ in let y' = ~~alloc (2,y)
+ in (x',y')
+ ]>
diff git a/examples/IsomorphismForCodeTypes.hs b/examples/IsomorphismForCodeTypes.hs
new file mode 100644
index 0000000..6e245d7
 /dev/null
+++ b/examples/IsomorphismForCodeTypes.hs
@@ 0,0 +1,12 @@
+{# OPTIONS_GHC XModalTypes ddumptypes XNoMonoPatBinds #}
+module IsomorphismForCodeTypes
+where
+
+
+ TahaSheard "isomorphism for code types"
+
+back :: forall a b c. (<[b]>@a > <[c]>@a) > <[ b>c ]>@a
+back = \f > <[ \x > ~~(f <[x]>) ]>
+
+forth :: forall a b c. <[b>c]>@a > (<[b]>@a > <[c]>@a)
+forth = \f > \x > <[ ~~f ~~x ]>
diff git a/examples/LambdaCalculusInterpreter.hs b/examples/LambdaCalculusInterpreter.hs
new file mode 100644
index 0000000..67aae51
 /dev/null
+++ b/examples/LambdaCalculusInterpreter.hs
@@ 0,0 +1,49 @@
+{# OPTIONS_GHC XModalTypes ddumptypes XNoMonoPatBinds #}
+module LambdaCalculusInterpreter
+where
+import Prelude hiding ( id, (.) )
+
+
+ A twostage (untyped) Lambda Calculus interpreter, from Hughes'
+ __Generalizing Monads to Arrows__.
+
+
+
+ Note how we have to use environment classifiers to tie Env, Val,
+ and Exp together (I miss Coq's [Section] command!!), yet the result
+ of "eval" is polymorphic in this classifier  so long as the "Env"
+ and "Val" share it.
+
+
+type Id = String
+data Exp = Var Id
+  Add Exp Exp
+  If Exp Exp Exp
+  App Exp Exp
+  Lam Id Exp
+
+type Env c = [(Id,Val c)]
+data Val c = Num Int  Fun <[Val c > Val c]>@c
+
+
+
+ This won't work until I implement proper support for inductive
+ types in the guest language
+
+
+{
+eval :: Exp > forall c. <[ Env c > Val c ]>@c
+
+eval (If e1 e2 e3) = <[ \env > if ~~(eval e1)
+ then ~~(eval e2)
+ else ~~(eval e3) ]>
+
+eval (Add e1 e2) = <[ \env > let (Num v1) = ~~(eval e1) env
+ in let (Num v2) = ~~(eval e2) env
+ in (Num (v1+v2)) ]>
+
+eval (Lam x e) = <[ \env > Fun (\v > ~~(eval e) ((x,v):env)) ]>
+
+eval (App e1 e2) = <[ \env > case ~~(eval e1) env of
+ Fun f > f ~~(eval e2) env ]>
+}
diff git a/examples/RegexMatcher.hs b/examples/RegexMatcher.hs
new file mode 100644
index 0000000..ca02755
 /dev/null
+++ b/examples/RegexMatcher.hs
@@ 0,0 +1,163 @@
+{# OPTIONS_GHC XModalTypes XMultiParamTypeClasses ddumptypes #}
+module RegexMatcher
+where
+import GHC.HetMet.CodeTypes hiding (())
+
+
+
+ A onelevel Regular Expression matcher, adapted from
+ Nanevski+Pfenning's _Staged computation with names and necessity_,
+ Figure 5
+
+
+data Regex
+ = Empty
+  Plus Regex Regex
+  Times Regex Regex
+  Star Regex
+  Const Char
+
+class Stream a where
+ s_empty :: a > Bool
+ s_head :: a > Char
+ s_tail :: a > a
+
+ A continuationpassingstyle matcher. If the "b" argument is false
+ the expression must match at least one character before passing
+ control to the continuation (this avoids the equality test in the
+ Nanevski+Pfenning code)
+
+accept :: Stream s =>
+ Regex >
+ Bool >  may only match the empty string if this is True
+ (s > Bool) >
+ s >
+ Bool
+
+accept Empty False k s =
+ False
+
+accept Empty True k s =
+ k s
+
+accept (Plus e1 e2) emptyOk k s =
+ (accept e1 emptyOk k s)  (accept e2 emptyOk k s)
+
+accept (Times e1 e2) True k s =
+ (accept e1 True (accept e2 True k)) s
+
+accept (Times e1 e2) False k s =
+ (accept e1 False (accept e2 True k)) s 
+ (accept e1 True (accept e2 False k)) s
+
+accept (Star e) emptyOk k s =
+ (emptyOk && (k s)) 
+ (accept e emptyOk (\s' > accept (Star e) False k s') s)
+
+accept (Const c) emptyOk k s =
+ if s_empty s
+ then False
+ else (s_head s) == c && k (s_tail s)
+
+
+
+
+
+ A twolevel Regular Expression matcher, adapted from
+ Nanevski+Pfenning's _Staged computation with names and necessity_,
+ Figure 6
+
+
+class GuestStream g a where
+ <[ gs_empty ]> :: <[ a > Bool ]>@g
+ <[ gs_head ]> :: <[ a > Char ]>@g
+ <[ gs_tail ]> :: <[ a > a ]>@g
+
+class GuestEqChar g where
+ <[ (==) ]> :: <[ Char > Char > Bool ]>@g
+
+staged_accept ::
+ Regex
+ > Bool
+ > forall c s.
+ GuestStream c s =>
+ GuestCharLiteral c =>
+ GuestLanguageBool c =>
+ GuestEqChar c =>
+ <[ s > Bool ]>@c
+ > <[ s > Bool ]>@c
+
+staged_accept Empty False k =
+ <[ \s > false ]>
+
+staged_accept Empty True k =
+ <[ \s > gs_empty s ]>
+
+staged_accept (Plus e1 e2) emptyOk k =
+ <[ \s > let k' = ~~k
+ in (~~(staged_accept e1 emptyOk <[k']>) s) 
+ (~~(staged_accept e2 emptyOk <[k']>) s)
+ ]>
+
+staged_accept (Times e1 e2) True k =
+ <[ \s > ~~(staged_accept e1 True (staged_accept e2 True k)) s ]>
+
+staged_accept (Times e1 e2) emptyOk k =
+ <[ \s > ~~(staged_accept e1 True (staged_accept e2 False k)) s 
+ ~~(staged_accept e1 False (staged_accept e2 True k)) s
+ ]>
+
+staged_accept (Star e) emptyOk' k =
+ loop emptyOk'
+ where
+  loop :: Bool > <[s > Bool]>@g
+ loop emptyOk = if emptyOk
+ then <[ \s > ~~k s  ~~(staged_accept e True (loop False)) s ]>
+ else <[ \s > ~~(staged_accept e False (loop False)) s ]>
+  note that loop is not (forall c s. <[s > Bool]>@c)
+  because "k" is free in loop; it is analogous to the free
+  environment variable in Nanevski's example
+
+staged_accept (Const c) emptyOk k =
+ <[ \s > if gs_empty s
+ then false
+ else (gs_head s) == ~~(guestCharLiteral c) && ~~k (gs_tail s) ]>
+
+
+ Take particular note of the "Plus" case above: note that (following
+ Nanevski+Pfenning) the code for "k" is not duplicated  it is
+ escapified into the constructed term only once, and a tiny scrap of
+ code containing nothing more than the variable name k' is passed
+ to the recursive call. This is in contrast with the naive implementation
+ shown below:
+
+ staged_accept (Plus e1 e2) emptyOk k =
+ <[ \s > (~~(staged_accept e1 emptyOk k) s) 
+ (~~(staged_accept e2 emptyOk k) s)
+ ]>
+
+
+
+ The following commentedout type is "too polymorphic"  try
+ uncommenting it to see what happens. It's a great example of the
+ kind of thing that environment classifiers guard against: the
+ continuation code and the result code get their classifiers
+ unified.
+
+{
+staged_accept ::
+ Regex
+ > Bool
+ > (forall c s.
+ GuestStream c s =>
+ GuestCharLiteral c =>
+ GuestLanguageBool c =>
+ GuestEqChar c =>
+ <[s > Bool]>@c)
+ > (forall c s.
+ GuestStream c s =>
+ GuestCharLiteral c =>
+ GuestLanguageBool c =>
+ GuestEqChar c =>
+ <[s > Bool]>@c)
+}
diff git a/examples/TypeSafeRun.hs b/examples/TypeSafeRun.hs
new file mode 100644
index 0000000..52978da
 /dev/null
+++ b/examples/TypeSafeRun.hs
@@ 0,0 +1,35 @@
+{# OPTIONS_GHC XModalTypes ddumptypes XNoMonoPatBinds #}
+module TypeSafeRun
+where
+import Prelude hiding ( id, (.) )
+
+
+ Examples of "running" code; these examples illustrate the sorts of
+ scoping problems that the TahaNielsen environment classifiers look
+ for in the context of HOMOGENEOUS metaprogramming. You can't
+ actually define these functions for ALL generalized arrows  only
+ those for which you've defined some sort of interpretation in Haskell.
+
+run :: forall a. (forall b. <[a]>@b) > a
+run = undefined
+
+ the typchecker correctly rejects this bogosity if you uncomment it:
+ bogus = <[ \x > ~~( run <[ x ]> ) ]>
+
+ The CalcanoMoggiTaha paper on environment classifier inference
+ had a special type for closed code and two special expressions
+ "close" and "open". These are unnecessary in SystemFC1 where we
+ can use higherrank polymorphism to get the same result (although
+ in truth it's cheating a bit since their type inference is
+ decidable with no annotations, whereas RankN inference is not):
+
+data ClosedCode a = ClosedCode (forall b. <[a]>@b)
+
+open :: forall a b. ClosedCode a > <[a]>@b
+open (ClosedCode x) = x
+
+close :: (forall b. <[a]>@b) > ClosedCode a
+close x = ClosedCode x
+
+run_closed :: ClosedCode a > a
+run_closed = undefined
diff git a/examples/Unflattening.hs b/examples/Unflattening.hs
new file mode 100644
index 0000000..f9ca4ba
 /dev/null
+++ b/examples/Unflattening.hs
@@ 0,0 +1,47 @@
+{# OPTIONS_GHC XModalTypes ddumptypes XNoMonoPatBinds XMultiParamTypeClasses #}
+module Unflattening
+where
+import GHC.HetMet.CodeTypes hiding (())
+import GHC.HetMet.GArrow
+import Control.Category
+import Control.Arrow
+import Prelude hiding ( id, (.) )
+
+
+ Unflattening
+
+ The current implementation has problems with literals at level>0;
+ there are specialpurpose hacks for Int and Char, but none for
+ unit. So I use this instead as a placeholder for <[ () ]>
+
+<[ u ]> = Prelude.error "FIXME"
+
+ This more or less "undoes" the flatten function. People often ask
+ me how you "translate generalized arrows back into multilevel
+ terms".. I'm not sure why you'd want to do that, but this is how:
+
+newtype Code x y = Code { unCode :: forall a. <[ x > y ]>@a }
+
+instance Category Code where
+ id = Code <[ \x > x ]>
+ f . g = Code <[ \x > ~~(unCode f) (~~(unCode g) x) ]>
+
+instance GArrow Code (,) () where
+ ga_first f = Code <[ \(x,y) > ((~~(unCode f) x),y) ]>
+ ga_second f = Code <[ \(x,y) > (x ,(~~(unCode f) y)) ]>
+ ga_cancell = Code <[ \(_,x) > x ]>
+
+ ga_cancelr = Code <[ \(x,_) > x ]>
+ ga_uncancell = Code <[ \x > (u,x) ]>
+ ga_uncancelr = Code <[ \x > (x,u) ]>
+ ga_assoc = Code <[ \((x,y),z) > (x,(y,z)) ]>
+ ga_unassoc = Code <[ \(x,(y,z)) > ((x,y),z) ]>
+
+instance GArrowDrop Code (,) () where
+ ga_drop = Code <[ \_ > u ]>
+
+instance GArrowCopy Code (,) () where
+ ga_copy = Code <[ \x > (x,x) ]>
+
+instance GArrowSwap Code (,) () where
+ ga_swap = Code <[ \(x,y) > (y,x) ]>
diff git a/examples/tutorial.hs b/examples/tutorial.hs
deleted file mode 100644
index 7668eab..0000000
 a/examples/tutorial.hs
+++ /dev/null
@@ 1,827 +0,0 @@
{# OPTIONS_GHC XModalTypes XScopedTypeVariables XFlexibleContexts XMultiParamTypeClasses ddumptypes XNoMonoPatBinds XFlexibleInstances XGADTs XUndecidableInstances #}
module GArrowsTutorial
where
import Data.Bits
import Data.Bool (not)
import GHC.HetMet.CodeTypes hiding (())
import GHC.HetMet.GArrow
import Control.Category
import Control.Arrow
import Prelude hiding ( id, (.) )

 The best way to understand heterogeneous metaprogramming and
 generalized arrows is to play around with this file, poking at the
 examples until they fail to typecheck  you'll learn a lot that
 way!

 Once you've built the modified compiler, you can compile this file
 with:

 $ inplace/bin/ghcstage2 tutorial.hs


 XModalTypes adds a new syntactical expression, "code brackets":
code_fst = <[ \(x,y) > x ]>

 This new expression is the introduction form for modal types:
code_fst :: forall a b g. <[ (a,b) > a ]>@g

 Think of <[T]>@g as being the type of programs written in language
 "g" which, when "executed", return a value of type "T". I mention
 "language g" because the *heterogeneous* aspect of HetMet means
 that we can limit the sorts of constructs allowed inside the code
 brackets, permitting only a subset of Haskell (you have to use
 Haskell syntax, though).

 There is a second new expression form, "~~", called "escape":

code_fst_fst = <[ \z > ~~code_fst (~~code_fst z) ]>

 Note that ~~ binds more tightly than any other operator. There is
 an alternate version, "~~$", which binds more weakly than any other
 operator (this is really handy sometimes!). To demonstrate this,
 the next two expressions differ only in superficial syntax:

example1 foo bar = <[ ~~$ foo bar ]>
example2 foo bar = <[ ~~( foo bar) ]>
 example3 foo bar = <[ ~~ foo bar ]>

 ... but the third one is completely different (and in fact, doesn't
 even parse, but we'll get to that in a moment)

 The escape operation must appear within code brackets. In truth,
 it is really a "hole" punched in the code brackets  the thing to
 which the escape operator gets applied is typed as if it were
 *outside* the code brackets. It must have type <[T]>, and the
 escape operator allows it to be used *inside* code brackets as if
 it had type "T".

 So, the escape operator is basically a way of pasting code
 fragments into each other.

 This is where those type variables after the "@" sign come in: if
 you paste two pieces of code into a third, all three must be
 written in the same language. We express this by unifying their
 tyvars:

compose_code :: forall g a b c. <[a>b]>@g > <[b>c]>@g > <[a>c]>@g
compose_code x y = <[ \z > ~~y (~~x z) ]>

 Now, try commenting out the type ascription above and uncommenting
 any of these three:

 compose_code :: forall g h a b c. <[a>b]>@h > <[b>c]>@g > <[a>c]>@g
 compose_code :: forall g h a b c. <[a>b]>@g > <[b>c]>@h > <[a>c]>@g
 compose_code :: forall g h a b c. <[a>b]>@g > <[b>c]>@g > <[a>c]>@h


 The typechecker won't let you get away with that  you're trying
 to force a type which is "too polymorphic" onto paste2. If the
 compiler allowed that, the resulting metaprogram might try to
 splice together programs written in different languages, resulting
 in mayhem.

 NEW SCOPING RULES: The syntactical depth (or just "depth") of an
 expression is the number of surrounding codebrackets minus the
 number of surrounding escapes (this is strictly a syntax concept
 and has NOTHING to do with the type system!). It is very important
 to keep in mind that the scope of a bound variable extends only to
 expressions at the same depth! To demonstrate, the following
 expression will fail to parse:

 badness = \x > <[ x ]>

 ...and in the following expression, the occurrence of "x" is bound
 by the first (outer) lambda, not the second one:

no_shadowing_here = \x > <[ \x > ~~x ]>

 Lastly, you can wrap codebrackets around an identifier in a
 toplevel, let, or where binding. Notice how GHC doesn't complain
 here about defining an identifier twice!

foo = \x > x+1
<[ foo ]> = <[ \(x::Bool) > x ]>

 Now you can use foo (the second one!) inside codebrackets:

bar x = <[ foo ~~x ]>

bar :: forall g. <[Bool]>@g > <[Bool]>@g

 In fact, the identifiers have completely unrelated types. Which
 brings up another important point: types are ALWAYS assigned
 "relative to" depth zero. So although we imagine "foo" existing at
 depthone, its type is quite firmly established as <[ Bool > Bool ]>

 It has to be this way  to see why, consider a term which is more
 polymorphic than "foo":

<[ foo' ]> = <[ \x > x ]>

 Its type is:

<[ foo' ]> :: forall a g . <[ a > a ]>@g

 ...and there's no way to express the gpolymorphism entirely from
 within the brackets.

 So why does all of this matter? Mainly so that we can continue to use . We'd like
 the "+" operator to work "as expected"  in other words, we'd like
 people to be able to write things like

increment_at_level1 = <[ \x > x + 1 ]>

 However, in unmodified haskell an identifier like (+) may have only
 one type. In this case that type is:

 (+) :: Num a => a > a > a

 Now, we could simply decree that when (+) appears inside code
 brackets, an "implicit ~~" is inserted, so the desugared expression
 is:

 increment_at_level1 = <[ \x > ~~(+) x 1 ]>

 unfortunately this isn't going to work for guest languages that
 don't have higherorder functions. Haskell uses curried arguments
 because it has higherorder functions, but in a firstorder guest
 language a more sensible type for (+) would be:

 (+) :: Num a => (a,a) > a

 ... or even something less polymorphic, like

 (+) :: (Int,Int) > Int

 so to maintain flexibility, we allow an identifier to have
 different types at different syntactic depths; this way type
 choices made for Haskell don't get imposed on guest languages that
 are missing some of its features.

 In hindsight, what we REALLY want is for increment_at_level1 to
 be desugared like this (much like the Arrow (...) syntax):

 increment_at_level1 = <[ \x > ~~( <[x]> + <[1]> ) ]>

 ... because then we can declare

 instance Num a => Num <[a]> where ...

 or just

 instance Num <[Int]> where ...

 unfortunately there's a major problem: knowing how to do this sort
 of desugaring requires knowing the *arity* of a function. For
 symbols we can kludge it by checking Haskell's parsing rules (there
 are only a handful of unary symbols; all others are binary), but
 this is crude and won't work at all for nonsymbol identifiers.
 And we can look at a type like x>y>z and say "oh, that's a
 twoargument function", but sometimes GHC doesn't know the complete
 type of an identifier in the midst of unification (i.e. "x has type
 Int>a for some a, where a could be Int or Int>Int"), so guessing
 the arity from the type cannot be done during parsing, which is
 when we need to do this.

 Okay, I think that's more or less a brain dump of why I changed the
 scoping rules and the problems with the other solutions I tried.

 I am very interested in hearing any suggestions on better ways of
 dealing with this, so long as you can still use operators like (+)
 in guest languages without higherorder functions.







 The rest of this file contains a bunch of example programs:
 exponentiation, dotproduct, a bunch of classic MetaML idioms, and
 a translation of Nanevski+Pfenning's twostage regex matcher.







 Ye Olde and Most Venerable "pow" Function

pow :: forall c. GuestIntegerLiteral c => GuestLanguageMult c Integer => Integer > <[ Integer > Integer ]>@c
pow n =
 if n==0
 then <[ \x > 1 ]>
 else <[ \x > x * ~~(pow (n  1)) x ]>


 a more efficient twolevel pow
pow' :: forall c. GuestIntegerLiteral c => GuestLanguageMult c Integer => Integer > <[ Integer > Integer ]>@c
pow' 0 = <[ \x > 1 ]>
pow' 1 = <[ \x > x ]>
pow' n = if n `mod` 2==0
 then <[ \x > (\y > y*y) (~~(pow' $ n `shiftR` 2) x) ]>
 else <[ \x > x * ~~(pow' $ n1) x ]>











 Dot Product

 This shows how to build a twolevel program one step at a time by
 slowly rearranging it until the brackets can be inserted.


 a onelevel function to compute the dot product of two vectors
dotproduct :: [Int] > [Int] > Int
dotproduct v1 v2 =
 case v1 of
 [] > 0
 (a:ax) > case v2 of
 [] > 0
 (b:bx) >
 (a*b)+(dotproduct ax bx)

 A slightly modified version of the dot product: note that we
 check for zeroes and ones to avoid multiplying. In a onelevel
 program this yields no advantage, however!
dotproduct' :: [Int] > [Int] > Int
dotproduct' v1 v2 =
 case v1 of
 [] > 0
 (0:ax) > case v2 of
 [] > 0
 (b:bx) > (dotproduct' ax bx)
 (1:ax) > case v2 of
 [] > 0
 (b:bx) > b+(dotproduct' ax bx)
 (a:ax) > case v2 of
 [] > 0
 (b:bx) >
 (a*b)+(dotproduct' ax bx)

 A twolevel version of the dot product. Note how we ask for the first
 vector, then produce a program which is optimized for multiplying
 by that particular vector. If there are zeroes or ones in the
 original vector, we will emit code which is faster than a onelevel
 dot product.

dotproduct'' :: forall g.
 GuestLanguageAdd g Integer =>
 GuestLanguageMult g Integer =>
 GuestIntegerLiteral g =>
 [Integer] > <[ [Integer] > Integer ]>@g
dotproduct'' v1 =
 case v1 of
 [] > <[ \v2 > 0 ]>
 (0:ax) > <[ \v2 > case v2 of
 [] > 0
 (b:bx) > ~~(dotproduct'' ax) bx ]>
 (1:ax) > <[ \v2 > case v2 of
 [] > 0
 (b:bx) > b + ~~(dotproduct'' ax) bx ]>

 (a:ax) > <[ \v2 > case v2 of
 [] > 0
 (b:bx) > ~~(guestIntegerLiteral a) * b + ~~(dotproduct'' ax) bx ]>





 TahaSheard "isomorphism for code types"

back :: forall a b c. (<[b]>@a > <[c]>@a) > <[ b>c ]>@a
back = \f > <[ \x > ~~(f <[x]>) ]>

forth :: forall a b c. <[b>c]>@a > (<[b]>@a > <[c]>@a)
forth = \f > \x > <[ ~~f ~~x ]>




 Examples of "running" code; these examples illustrate the sorts of
 scoping problems that the TahaNielsen environment classifiers look
 for in the context of HOMOGENEOUS metaprogramming. You can't
 actually define these functions for ALL generalized arrows  only
 those for which you've defined some sort of interpretation in Haskell.

run :: forall a. (forall b. <[a]>@b) > a
run = undefined

 the typchecker correctly rejects this bogosity if you uncomment it:
 bogus = <[ \x > ~~( run <[ x ]> ) ]>

 The CalcanoMoggiTaha paper on environment classifier inference
 had a special type for closed code and two special expressions
 "close" and "open". These are unnecessary in SystemFC1 where we
 can use higherrank polymorphism to get the same result (although
 in truth it's cheating a bit since their type inference is
 decidable with no annotations, whereas RankN inference is not):

data ClosedCode a = ClosedCode (forall b. <[a]>@b)

open :: forall a b. ClosedCode a > <[a]>@b
open (ClosedCode x) = x

close :: (forall b. <[a]>@b) > ClosedCode a
close x = ClosedCode x

run_closed :: ClosedCode a > a
run_closed = undefined




 A twolevel Regular Expression matcher, adapted from Nanevski+Pfenning, Figure 6
data Regex
 = Empty
  Plus Regex Regex
  Times Regex Regex
  Star Regex
  Const Char

class Stream a where
 s_empty :: a > Bool
 s_head :: a > Char
 s_tail :: a > a

 a continuationpassingstyle matcher

accept :: Stream s => Regex > (s > Bool) > s > Bool

accept Empty k s =
 k s

accept (Plus e1 e2) k s =
 (accept e1 k s)  (accept e2 k s)

accept (Times e1 e2) k s =
 (accept e1 (accept e2 k)) s

accept (Star e) k s =
 (k s)  (accept e (\s' > accept (Star e) k s') s)
  FIXME: this will loop forever if you give it (Star x) where x can
  match the empty string

accept (Const c) k s =
 if s_empty s
 then False
 else (s_head s) == c && k (s_tail s)

class GuestStream g a where
 <[ gs_empty ]> :: <[ a > Bool ]>@g
 <[ gs_head ]> :: <[ a > Char ]>@g
 <[ gs_tail ]> :: <[ a > a ]>@g

class GuestEqChar g where
 <[ (==) ]> :: <[ Char > Char > Bool ]>@g

staged_accept ::
 Regex
 > forall c s.
 GuestStream c s =>
 GuestCharLiteral c =>
 GuestLanguageBool c =>
 GuestEqChar c =>
 <[ s > Bool ]>@c
 > <[ s > Bool ]>@c

staged_accept Empty k =
 <[ \s > gs_empty s ]>

 note that code for "k" gets duplicated here
staged_accept (Plus e1 e2) k =
 <[ \s > (~~(staged_accept e1 k) s)  (~~(staged_accept e2 k) s) ]>

staged_accept (Times e1 e2) k =
 <[ \s > ~~(staged_accept e1 (staged_accept e2 k)) s ]>

staged_accept (Star e) k =
 loop
 where
  loop :: <[s > Bool]>@g
 loop = <[ \s > ~~k s  ~~(staged_accept e loop) s ]>
  note that loop is not (forall c s. <[s > Bool]>@c)
  because "k" is free in loop; it is analogous to the free
  environment variable in Nanevski's example


staged_accept (Const c) k =
 <[ \s > if gs_empty s
 then false
 else (gs_head s) == ~~(guestCharLiteral c) && ~~k (gs_tail s) ]>


 this type won't work unless the case for (Star e) is commented out;
 see loop above
 Regex
 > (forall c s.
 GuestStream c s =>
 GuestLanguageBool c =>
 GuestEqChar c =>
 <[s > Bool]>@c)
 > (forall c s.
 GuestStream c s =>
 GuestLanguageBool c =>
 GuestEqChar c =>
 <[s > Bool]>@c)





 Unflattening

 The current implementation has problems with literals at level>0;
 there are specialpurpose hacks for Int and Char, but none for
 unit. So I use this instead as a placeholder for <[ () ]>

<[ u ]> = Prelude.error "FIXME"

 This more or less "undoes" the flatten function. People often ask
 me how you "translate generalized arrows back into multilevel
 terms".. I'm not sure why you'd want to do that, but this is how:
newtype Code x y = Code { unCode :: forall a. <[ x > y ]>@a }

instance Category Code where
 id = Code <[ \x > x ]>
 f . g = Code <[ \x > ~~(unCode f) (~~(unCode g) x) ]>

instance GArrow Code (,) () where
 ga_first f = Code <[ \(x,y) > ((~~(unCode f) x),y) ]>
 ga_second f = Code <[ \(x,y) > (x ,(~~(unCode f) y)) ]>
 ga_cancell = Code <[ \(_,x) > x ]>

 ga_cancelr = Code <[ \(x,_) > x ]>
 ga_uncancell = Code <[ \x > (u,x) ]>
 ga_uncancelr = Code <[ \x > (x,u) ]>
 ga_assoc = Code <[ \((x,y),z) > (x,(y,z)) ]>
 ga_unassoc = Code <[ \(x,(y,z)) > ((x,y),z) ]>




 BiGArrows

class GArrow g (**) u => BiGArrow g (**) u where
  Note that we trust the user's pair of functions actually are
  mutually inverse; confirming this in the type system would
  require very powerful dependent types (such as Coq's). However,
  the consequences of failure here are much more mild than failures
  in BiArrow.inv: if the functions below are not mutually inverse,
  the LoggingBiGArrow will simply compute the wrong result rather
  than fail in some manner outside the language's semantics.
 biga_arr :: (x > y) > (y > x) > g x y
 biga_inv :: g x y > g y x

 For any GArrow instance, its mutually inverse pairs form a BiGArrow
data GArrow g (**) u => GArrowInversePair g (**) u x y =
 GArrowInversePair { forward :: g x y , backward :: g y x }
instance GArrow g (**) u => Category (GArrowInversePair g (**) u) where
 id = GArrowInversePair { forward = id , backward = id }
 f . g = GArrowInversePair { forward = (forward f) . (forward g) , backward = (backward g) . (backward f) }
instance GArrow g (**) u => GArrow (GArrowInversePair g (**) u) (**) u where
 ga_first f = GArrowInversePair { forward = ga_first (forward f), backward = ga_first (backward f) }
 ga_second f = GArrowInversePair { forward = ga_second (forward f), backward = ga_second (backward f) }
 ga_cancell = GArrowInversePair { forward = ga_cancell , backward = ga_uncancell }
 ga_cancelr = GArrowInversePair { forward = ga_cancelr , backward = ga_uncancelr }
 ga_uncancell = GArrowInversePair { forward = ga_uncancell , backward = ga_cancell }
 ga_uncancelr = GArrowInversePair { forward = ga_uncancelr , backward = ga_cancelr }
 ga_assoc = GArrowInversePair { forward = ga_assoc , backward = ga_unassoc }
 ga_unassoc = GArrowInversePair { forward = ga_unassoc , backward = ga_assoc }
instance GArrowSwap g (**) u => GArrowSwap (GArrowInversePair g (**) u) (**) u where
 ga_swap = GArrowInversePair { forward = ga_swap , backward = ga_swap }
 but notice that we can't (in general) get
 instance GArrowDrop g => GArrowDrop (GArrowInversePair g) where ...


 For that, we need PreLenses, which "log the history" where necessary.
 I call this a "PreLens" because it consists of the data required
 for a Lens (as in BCPierce's Lenses) but does not necessarily
 satisfy the putget/getput laws. Specifically, the "extra stuff" we
 store is the inversion function.
newtype PreLens x y = PreLens { preLens :: x > (y , y>x) }

instance Category PreLens where
 id = PreLens { preLens = \x > (x, (\x > x)) }
 f . g = PreLens { preLens = \x > let (gx,g') = (preLens g) x in let (fgx,f') = (preLens f) gx in (fgx , \q > g' (f' q)) }

instance GArrow PreLens (,) () where
 ga_first f = PreLens { preLens = \(x,z) > let (y,f') = (preLens f) x in ((y,z),(\(q1,q2) > (f' q1,q2))) }
 ga_second f = PreLens { preLens = \(z,x) > let (y,f') = (preLens f) x in ((z,y),(\(q1,q2) > (q1,f' q2))) }
 ga_cancell = PreLens { preLens = \(_,x) > (x, (\x > ((),x))) }
 ga_cancelr = PreLens { preLens = \(x,_) > (x, (\x > (x,()))) }
 ga_uncancell = PreLens { preLens = \x > (((),x), (\(_,x) > x)) }
 ga_uncancelr = PreLens { preLens = \x > ((x,()), (\(x,_) > x)) }
 ga_assoc = PreLens { preLens = \((x,y),z) > ( (x,(y,z)) , (\(x,(y,z)) > ((x,y),z)) ) }
 ga_unassoc = PreLens { preLens = \(x,(y,z)) > ( ((x,y),z) , (\((x,y),z) > (x,(y,z))) ) }

instance GArrowDrop PreLens (,) () where
 ga_drop = PreLens { preLens = \x > (() , (\() > x)) }
instance GArrowCopy PreLens (,) () where
 ga_copy = PreLens { preLens = \x > ((x,x) , fst) }
instance GArrowSwap PreLens (,) () where
 ga_swap = PreLens { preLens = \(x,y) > ((y,x) , (\(z,q) > (q,z))) }



data Lens x y where
 Lens :: forall x y c1 c2 . ((x,c1)>(y,c2)) > ((y,c2)>(x,c1)) > Lens x y
{
 can we make lenses out of GArrows other than (>)?
instance Category Lens where
 id = Lens (\x > x) (\x > x)
 (Lens g1 g2) . (Lens f1 f2) = Lens (\(x,(c1,c2)) > let (y,fc) = f1 (x,c1) in let (z,gc) = g1 (y,c2) in (z,(fc,gc)))
 (\(z,(c1,c2)) > let (y,gc) = g2 (z,c2) in let (x,fc) = f2 (y,c1) in (x,(fc,gc)))

instance GArrow Lens (,) () where
 ga_first (Lens f1 f2) = Lens (\((x1,x2),c) > let (y,c') = f1 (x1,c) in ((y,x2),c'))
 (\((x1,x2),c) > let (y,c') = f2 (x1,c) in ((y,x2),c'))
 ga_second (Lens f1 f2) = Lens (\((x1,x2),c) > let (y,c') = f1 (x2,c) in ((x1,y),c'))
 (\((x1,x2),c) > let (y,c') = f2 (x2,c) in ((x1,y),c'))
 ga_cancell = Lens (\(((),x),()) > ( x ,()))
 (\( x ,()) > (((),x),()))
 ga_uncancell = Lens (\( x ,()) > (((),x),()))
 (\(((),x),()) > ( x ,()))
 ga_cancelr = Lens (\((x,()),()) > ( x ,()))
 (\( x ,()) > ((x,()),()))
 ga_uncancelr = Lens (\( x ,()) > ((x,()),()))
 (\((x,()),()) > ( x ,()))
 ga_assoc = Lens (\(((x,y),z),()) > ((x,(y,z)),()))
 (\((x,(y,z)),()) > (((x,y),z),()))
 ga_unassoc = Lens (\((x,(y,z)),()) > (((x,y),z),()))
 (\(((x,y),z),()) > ((x,(y,z)),()))

instance GArrowDrop Lens (,) () where
 ga_drop = Lens (\(x,()) > ((),x)) (\((),x) > (x,()))
instance GArrowCopy Lens (,) () where
 ga_copy = Lens (\(x,()) > ((x,x),())) (\((x,_),()) > (x,()))
instance GArrowSwap Lens (,) () where
 ga_swap = Lens (\((x,y),()) > ((y,x),())) (\((x,y),()) > ((y,x),()))

instance BiGArrow Lens (,) () where
 biga_arr f f' = Lens (\(x,()) > ((f x),())) (\(x,()) > ((f' x),()))
 biga_inv (Lens f1 f2) = Lens f2 f1
}



 An example generalized arrow

 *** this will be finished and posted by 14Mar2011; the code
 *** below is just a sketch ***

{
 A verilog module is an SDoc (chunk of text) giving the module's
 definition. The UniqueSupply avoids name clashes.
data VerilogModule =
 VerilogModule
 [VerilogModule]  dependencies
 String >  module name
 (Tree String >  input port names
 Tree String >  output port names
 SDoc)  raw verilog code for the body


instance Show VerilogModule where
 show VerilogModule dep name body =
 "module "++name++"(FIXME)"++(body FIXME FIXME)

data VerilogWrappedType a =
 { vwt_rep :: String }

 A "verilog garrow" from A to B is, concretely, the source code for a
 verilog module having input ports of type A and output ports of type B;
 the UniqueSupply lets us generate names.
data GArrowVerilog a b =
 UniqueSupply >
 VerilogWrappedType a >
 VerilogWrappedType b >
 GArrowVerilog SDoc

instance GArrow GArrowVerilog (,) where
 ga_id = VerilogModule [] "ga_id" (\ inp outp > zipTree ... "assign "++outp++" = "++inp)
 ga_comp f g = VerilogModule [] "ga_comp"
 ga_first :: g x y > g (x ** z) (y ** z)
 ga_second f = ga_comp (ga_comp ga_swap (ga_first f)) ga_swap
 ga_cancell f = VerilogModule [] "ga_cancell" (\ [in1,in2] [outp] > "assign "++outp++" = "++in2)
 ga_cancelr f = VerilogModule [] "ga_cancelr" (\ [in1,in2] [outp] > "assign "++outp++" = "++in1)
 ga_uncancell f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] > "assign "++out1++"=1'b0;\n assign"++out2++"="++in1)
 ga_uncancelr f = VerilogModule [] "ga_cancelr" (\ [in1] [out1,out2] > "assign "++out2++"=1'b0;\n assign"++out1++"="++in1)
 ga_assoc f =
 ga_unassoc :: g (x**(y**z)) ((x**y)**z)

instance GArrowDrop GArrowVerilog (,) where
 ga_drop =

instance GArrowCopy GArrowVerilog (,) where
 ga_copy =

instance GArrowSwap GArrowVerilog (,) where
 ga_swap =

instance GArrowLoop GArrowVerilog (,) where
 ga_loop =

instance GArrowLiteral GArrowVerilog (,) where
 ga_literal =
}





{
lambda calculus interpreter

data Val =
 Num Int
 Fun <[Val > Val]>

This requires higherorder functions in the second level...

eval :: Exp > a Env Val
eval (Var s) = <[ lookup s ]>
eval (Add e1 e2) = <[ let (Num v1) = ~(eval e1)
 in let (Num v2) = ~(eval e2)
 in (Num (v1+v2)) ]>
eval (If e1 e2 e3) = <[ let v1 = ~(eval e1) in
 in if v1
 then ~(eval e2)
 else ~(eval e3) ]>
eval (Lam x e) = ???

eval (Var s) = proc env >
 returnA < fromJust (lookup s env)
eval (Add e1 e2) = proc env >
 (eval e1 < env) `bind` \ ~(Num u) >
 (eval e2 < env) `bind` \ ~(Num v) >
 returnA < Num (u + v)
eval (If e1 e2 e3) = proc env >
 (eval e1 < env) `bind` \ ~(Bl b) >
 if b then eval e2 < env
 else eval e3 < env
eval (Lam x e) = proc env >
 returnA < Fun (proc v > eval e < (x,v):env)
eval (App e1 e2) = proc env >
 (eval e1 < env) `bind` \ ~(Fun f) >
 (eval e2 < env) `bind` \ v >
 f < v

eval (Var s) = <[ \env > fromJust (lookup s env) ]>
eval (Add e1 e2) = <[ \env > (~(eval e1) env) + (~(eval e2) env) ]>
eval (If e1 e2 e3) = <[ \env > if ~(eval e1) env
 then ~(eval e2) env
 else ~(eval e2) env
eval (Lam x e) = <[ \env > Fun (\v > ~(eval e) ((x,v):env)) ]>
eval (App e1 e2) = <[ \env > case ~(eval e1) env of
 (Fun f) > f (~(eval e2) env) ]>
eval (Var s) <[env]> = <[ fromJust (lookup s env) ]>
eval (Add e1 e2) <[env]> = <[ (~(eval e1) env) + (~(eval e2) env) ]>
}





{
immutable heap with cycles

 an immutable heap; maps Int>(Int,Int)

alloc :: A (Int,Int) Int
lookup :: A Int (Int,Int)

onetwocycle :: A (Int,Int) (Int,Int)
onetwocycle =
 proc \(x,y)> do
 x' < alloc < (1,y)
 y' < alloc < (2,x)
 return (x',y')
\end{verbatim}

\begin{verbatim}
alloc :: <[ (Int,Int) > Int ]>
lookup :: <[ Int > (Int,Int) ]>

onetwocycle :: <[ (Int,Int) ]> > <[ (Int,Int) ]>
onetwocycle x y = <[
 let x' = ~alloc (1,~y)
 in let y' = ~alloc (2,~x)
 in (x',y')
]>

onetwocycle' :: <[ (Int,Int) > (Int,Int) ]>
onetwocycle' = back2 onetwocycle
\end{verbatim}
}




{
The example may seem a little contrived, but its purpose is to
illustrate the be haviour when the argument of mapC refers both to
its parameter and a free vari able (n).

\begin{verbatim}
 we can use mapA rather than mapC (from page 100)

mapA f = proc xs > case xs of
[] > returnA < [] x:xsâ > do y < f < x
ysâ < mapA f < xsâ returnA < y:ys

example2 =
 <[ \(n,xs) >
 ~(mapA <[ \x> (~(delay 0) n, x) ]> )
 xs
 ]>

<[ example2 (n,xs) =
 ~(mapA <[ \x> (~(delay 0) n, x) ]> ) xs ]>
\end{verbatim}
}






{
delaysA =
 arr listcase >>>
 arr (const []) 
 (arr id *** (delaysA >>> delay []) >>>
 arr (uncurry (:)))

nor :: SF (Bool,Bool) Bool
nor = arr (not.uncurry ())

edge :: SF Bool Bool
edge =
 proc a > do
 b < delay False < a
 returnA < a && not b

flipflop =
 proc (reset,set) > do
 rec c < delay False < nor
 reset d d < delay True < nor set c
 returnA < (c,d)

halfAdd :: Arrow arr => arr (Bool,Bool) (Bool,Bool)
halfAdd =
 proc (x,y) > returnA < (x&&y, x/=y)

fullAdd ::
 Arrow arr => arr (Bool,Bool,Bool) (Bool,Bool)
fullAdd =
 proc (x,y,c) > do
 (c1,s1) < halfAdd < (x,y)
 (c2,s2) < halfAdd < (s1,c)
 returnA < (c1c2,s2)

Here is the appendix of Hughes04:
module Circuits where
import Control.Arrow import List
class ArrowLoop a => ArrowCircuit a where delay :: b > a b b
nor :: Arrow a => a (Bool,Bool) Bool nor = arr (not.uncurry ())
flipflop :: ArrowCircuit a => a (Bool,Bool) (Bool,Bool) flipflop = loop (arr (\((a,b),~(c,d)) > ((a,d),(b,c))) >>>
nor *** nor >>> delay (False,True) >>> arr id &&& arr id)
class Signal a where showSignal :: [a] > String
instance Signal Bool where showSignal bs = concat top++"\n"++concat bot++"\n"
where (top,bot) = unzip (zipWith sh (False:bs) bs) sh True True = ("__"," ") sh True False = (" ","_") sh False True = (" _"," ")
sh False False = (" ","__")
instance (Signal a,Signal b) => Signal showSignal xys = showSignal (map fst showSignal (map snd
instance Signal a => Signal [a] where showSignal = concat . map showSignal
sig = concat . map (uncurry replicate)
(a,b) where xys) ++ xys)
. transpose
flipflopInput = sig [(5,(False,False)),(2,(False,True)),(5,(False,False)),
(2,(True,False)),(5,(False,False)),(2,(True,True)), (6,(False,False))]





 from Hughes' "programming with Arrows"

mapC :: ArrowChoice arr => arr (env,a) b > arr (env,[a]) [b] mapC c = proc (env,xs) >
case xs of [] > returnA < [] x:xsâ > do y < c < (env,x)
ys < mapC c < (env,xsâ) returnA < y:ys

example2 = proc (n,xs) > ( mapC (\x> do delay 0 < n
&&& do returnA < x) ) xs
}




1.7.10.4