syntactic 0.6 → 0.7

raw patch · 46 files changed

+5001/−1845 lines, 46 files

Files

• CEFP/Examples/CodeApplication.hs +175/−0
• CEFP/Examples/ExProg.hs +894/−0
• CEFP/Examples/Exercise10.hs +109/−0
• CEFP/Examples/Exercise12.hs +26/−0
• CEFP/Examples/Exercise14.hs +61/−0
• CEFP/Examples/SolutionsSec2.hs +370/−0
• CEFP/Examples/Test.hs +46/−0
• CEFP/Imperative/Compiler.hs +204/−0
• CEFP/Imperative/Imperative.hs +98/−0
• CEFP/MuFeldspar/Core.hs +460/−0
• CEFP/MuFeldspar/Frontend.hs +218/−0
• CEFP/MuFeldspar/Prelude.hs +11/−0
• CEFP/MuFeldspar/Vector.hs +96/−0
• Examples/NanoFeldspar/Core.hs +82/−73
• Examples/NanoFeldspar/Extra.hs +28/−32
• Examples/NanoFeldspar/Test.hs +20/−6
• Examples/NanoFeldspar/Vector.hs +1/−1
• Language/Syntactic.hs +2/−2
• Language/Syntactic/Constructs/Annotate.hs +123/−0
• Language/Syntactic/Constructs/Binding.hs +296/−0
• Language/Syntactic/Constructs/Binding/HigherOrder.hs +96/−0
• Language/Syntactic/Constructs/Binding/Optimize.hs +134/−0
• Language/Syntactic/Constructs/Condition.hs +47/−0
• Language/Syntactic/Constructs/Literal.hs +57/−0
• Language/Syntactic/Constructs/Monad.hs +49/−0
• Language/Syntactic/Constructs/Symbol.hs +93/−0
• Language/Syntactic/Constructs/Tuple.hs +422/−0
• Language/Syntactic/Constructs/TupleSyntacticPoly.hs +138/−0
• Language/Syntactic/Constructs/TupleSyntacticSimple.hs +138/−0
• Language/Syntactic/Features/Annotate.hs +0/−99
• Language/Syntactic/Features/Binding.hs +0/−276
• Language/Syntactic/Features/Binding/HigherOrder.hs +0/−134
• Language/Syntactic/Features/Binding/PartialEval.hs +0/−144
• Language/Syntactic/Features/Condition.hs +0/−57
• Language/Syntactic/Features/Literal.hs +0/−63
• Language/Syntactic/Features/Symbol.hs +0/−179
• Language/Syntactic/Features/Tuple.hs +0/−391
• Language/Syntactic/Features/TupleSyntacticPoly.hs +0/−138
• Language/Syntactic/Features/TupleSyntacticSimple.hs +0/−138
• Language/Syntactic/Frontend/Monad.hs +64/−0
• Language/Syntactic/Sharing/Graph.hs +1/−5
• Language/Syntactic/Sharing/Reify.hs +4/−4
• Language/Syntactic/Sharing/ReifyHO.hs +21/−19
• Language/Syntactic/Sharing/SimpleCodeMotion.hs +190/−0
• Language/Syntactic/Syntax.hs +192/−70
• syntactic.cabal +35/−14

@@ -0,0 +1,175 @@+module Main where
+
+import qualified Prelude
+import MuFeldspar.Prelude
+
+import MuFeldspar.Core
+import MuFeldspar.Frontend
+import MuFeldspar.Vector
+
+import Imperative.Imperative
+import Imperative.Compiler
+
+import Data.Word
+import Data.Bits (Bits)
+
+
+type VecBool = Vector (Data Bool)
+
+type VecInt = Vector (Data Int)
+
+-- Primitive Functions (and tuples)
+
+prog0 :: Data Int -> Data Int
+prog0 = (*2)
+
+prog1 :: (Data Int, Data Int) -> (Data Int, Data Int, Data Int)
+prog1 (a,b) = (min a b, a + b, a ^ b)
+
+prog2 :: Data Int -> Data Int -> (Data Int, Data Int, Data Int)
+prog2 a b = (min a b, a + b, a ^ b)
+
+isEven :: (Type a, Integral a) => Data a -> Data Bool
+isEven i = i `mod` 2 == 0
+
+swap (a,b) = (b,a)
+
+
+-- Conditional
+
+f :: Data Int -> Data Int
+f i = (isEven i) ? (2*i, i)
+
+t1 = eval (f 3)
+
+t2 = eval (f 4)
+
+
+-- Arrays
+
+prog3 :: Data [Int]
+prog3 = parallel 10 (*2)
+
+tst1 = eval prog3
+
+tst1a = drawFeld prog3
+
+tst1b = printFeld prog3
+
+tst1c = compile prog3
+
+prog4 :: Data [Int]
+prog4 = parallel 10 (`mod` 5)
+
+prog5 :: Data [Int]
+prog5 = parallel 10 f
+
+prog6 :: Data [Int]
+prog6 = parallel 10 (<< 3)
+
+prog7 :: Data [Int]
+prog7 = parallel 10 (>> 1)
+
+prog8 :: Data [Int]
+prog8 = parallel 12 (`xor` 3)
+
+
+
+
+perm f arr = parallel (getLength arr) (\i -> getIx arr (f i))
+
+rot arr = perm f arr
+  where
+    f i = (i+1) `mod` (getLength arr)
+
+prog9 :: Data [[Int]]
+prog9 = parallel 8 (\i -> parallel i id)
+
+-- Sequential Arrays
+
+prog10 :: Data [Int]
+prog10 = sequential 10 1 g
+  where
+    g ix st = (j,j) 
+      where j = (ix + 1)  * st
+
+-- for Loop
+
+prog11 :: Data Int -> Data Int
+prog11 k  = forLoop k 1 g
+  where
+    g ix st = (ix + 1) * st
+
+composeN :: (Syntax st) => (st -> st) -> Data Length -> st -> st
+composeN f l i0 = forLoop l i0 g
+  where
+    g _ i = f i
+
+ccn = compile (composeN ((*2) :: Data Int -> Data Int))
+
+
+
+
+
+-- Vectors
+
+prog12 :: Vector (Data Int)
+prog12 = Indexed 10 (*2)
+
+tst2 = eval prog11
+
+prog13 :: Data Int
+prog13 = sum $ Indexed 10 (*2)
+
+
+prog14 :: Vector (Data Int)
+prog14 = map (*5) $ Indexed 10 (*2)
+
+prog15 :: Vector (Data Int)
+prog15 = map (*5) . map (+1) $ Indexed 10 (*2)
+
+scalarProduct :: (Type a, Num a) => Vector (Data a) -> Vector (Data a) -> Data a
+scalarProduct as bs = sum $ zipWith (*) as bs
+
+
+forceEx as bs = (sum . force) $ zipWith (*) as bs
+
+prog16 :: Data Int -> Data Int
+prog16 a = sum $ (isEven a) ? (prog14, prog15)
+
+
+
+
+
+sumEven :: VecInt -> Data Int
+sumEven = sum . map zeroOutOdd
+  where
+    zeroOutOdd x = (testBit x 0) ? (0,x)
+
+{--
+*Main> eval $ sumEven (value [1..10])
+30
+--}
+
+
+
+
+
+testBit :: (Type a, Bits a) => Data a -> Data Index -> Data Bool
+testBit l i = not ((l .&. (1<<i)) == 0)
+
+int2BLN :: Data Length -> Data Int -> VecBool
+int2BLN n v = reverse $ indexed n (testBit v)
+
+int2BL :: (Type a, Bits a)  =>  Data a -> VecBool
+int2BL l = reverse $ indexed (bitSize l) (testBit l)
+
+
+
+dft :: Vector (Data Complex) -> Vector (Data Complex)
+dft v = Indexed l ixf
+  where
+    l = length v
+    ixf i = scalarProduct v (ts i)
+    ts k = indexed l f
+      where f i = cis $ (-2 * (value pi) * (i2n i) * (i2n k)) / (i2n l)

@@ -0,0 +1,894 @@+module Main where
+
+import qualified Prelude
+import MuFeldspar.Prelude
+
+import MuFeldspar.Core
+import MuFeldspar.Frontend
+import MuFeldspar.Vector
+
+import Imperative.Imperative
+import Imperative.Compiler
+
+import Data.Word
+import Data.Bits (Bits)
+
+
+type VecBool = Vector (Data Bool)
+
+type VecInt = Vector (Data Int)
+
+-- Primitive Functions (and tuples)
+
+prog0 :: Data Int -> Data Int
+prog0 = (*2)
+
+prog1 :: (Data Int, Data Int) -> (Data Int, Data Int, Data Int)
+prog1 (a,b) = (min a b, a + b, a ^ b)
+
+prog2 :: Data Int -> Data Int -> (Data Int, Data Int, Data Int)
+prog2 a b = (min a b, a + b, a ^ b)
+
+isEven :: (Type a, Integral a) => Data a -> Data Bool
+isEven i = i `mod` 2 == 0
+
+swap (a,b) = (b,a)
+
+
+-- Conditional
+
+f :: Data Int -> Data Int
+f i = (isEven i) ? (2*i, i)
+
+t1 = eval (f 3)
+
+t2 = eval (f 4)
+
+
+-- Arrays
+
+prog3 :: Data [Int]
+prog3 = parallel 10 (*2)
+
+tst1 = eval prog3
+
+tst1a = drawFeld prog3
+
+tst1b = printFeld prog3
+
+tst1c = compile prog3
+
+prog4 :: Data [Int]
+prog4 = parallel 10 (`mod` 5)
+
+prog5 :: Data [Int]
+prog5 = parallel 10 f
+
+prog6 :: Data [Int]
+prog6 = parallel 10 (<< 3)
+
+prog7 :: Data [Int]
+prog7 = parallel 10 (>> 1)
+
+prog8 :: Data [Int]
+prog8 = parallel 12 (`xor` 3)
+
+
+
+
+perm f arr = parallel (getLength arr) (\i -> getIx arr (f i))
+
+rot arr = perm f arr
+  where
+    f i = (i+1) `mod` (getLength arr)
+
+prog9 :: Data [[Int]]
+prog9 = parallel 8 (\i -> parallel i id)
+
+-- Sequential Arrays
+
+prog10 :: Data [Int]
+prog10 = sequential 10 1 g
+  where
+    g ix st = (j,j) 
+      where j = (ix + 1)  * st
+
+-- for Loop
+
+prog11 :: Data Int -> Data Int
+prog11 k  = forLoop k 1 g
+  where
+    g ix st = (ix + 1) * st
+
+composeN :: (Syntax st) => (st -> st) -> Data Length -> st -> st
+composeN f l i0 = forLoop l i0 g
+  where
+    g _ i = f i
+
+ccn = compile (composeN ((*2) :: Data Int -> Data Int))
+
+
+
+
+
+-- Vectors
+
+prog12 :: Vector (Data Int)
+prog12 = Indexed 10 (*2)
+
+tst2 = eval prog11
+
+prog13 :: Data Int
+prog13 = sum $ Indexed 10 (*2)
+
+
+prog14 :: Vector (Data Int)
+prog14 = map (*5) $ Indexed 10 (*2)
+
+prog15 :: Vector (Data Int)
+prog15 = map (*5) . map (+1) $ Indexed 10 (*2)
+
+scalarProduct :: (Type a, Num a) => Vector (Data a) -> Vector (Data a) -> Data a
+scalarProduct as bs = sum $ zipWith (*) as bs
+
+
+forceEx as bs = (sum . force) $ zipWith (*) as bs
+
+prog16 :: Data Int -> Data Int
+prog16 a = sum $ (isEven a) ? (prog14, prog15)
+
+
+
+
+
+sumEven :: VecInt -> Data Int
+sumEven = sum . map zeroOutOdd
+  where
+    zeroOutOdd x = (testBit x 0) ? (0,x)
+
+{--
+*Main> eval $ sumEven (value [1..10])
+30
+--}
+
+
+
+
+tri :: (Syntax a) => (a -> a)  -> Vector a -> Vector a
+tri f (Indexed len ixf) = (indexed len ixf')
+  where
+    ixf' i = composeN f i (ixf i)
+
+ctri = compile (tri ((*2) :: Data Int -> Data Int))
+
+
+testBit :: (Type a, Bits a) => Data a -> Data Index -> Data Bool
+testBit l i = not ((l .&. (1<<i)) == 0)
+
+
+int2BL :: (Type a, Bits a)  =>  Data a -> VecBool
+int2BL l = reverse $ indexed (bitSize l) (testBit l)
+
+
+int2BLN :: Data Length -> Data Int -> VecBool
+int2BLN n v = reverse $ indexed n (testBit v)
+
+
+pows2 :: Data Length -> Vector (Data Index)
+pows2 k = Indexed k (1<<)
+
+bL2Int :: VecBool -> Data Int
+bL2Int bs = scalarProduct (reverse (map b2i bs)) (pows2 (length bs))
+
+bL2Int' :: VecBool -> Data Int
+bL2Int' = sum . tri (*2) . map b2i
+
+oneBitsN :: Data Index -> Data Index
+oneBitsN  = complement . zeroBitsN
+
+zeroBitsN :: Data Index -> Data Index
+zeroBitsN = shiftL allOnes
+
+allOnes :: Data Index
+allOnes = complement 0
+
+
+
+xorBool :: Data Bool -> Data Bool -> Data Bool
+xorBool a b = not (a == b)
+
+pad :: Data Length -> VecBool -> VecBool
+pad l v = (replicate (l - length v) false) ++ v
+
+crcAdd :: VecBool -> VecBool -> VecBool
+crcAdd as bs = zipWith xorBool (pad m as) (pad m bs)
+  where
+    m = max (length as) (length bs)
+
+
+
+
+simpleCRC :: VecBool -> VecBool -> VecBool
+simpleCRC poly msg =  fst $ composeN step (l+w) (fw, msg ++ fw)
+  where
+    w = length poly
+    fw = replicate w false
+    l = length msg
+    step (reg,ms) = (reg',tlms)
+      where
+        reg' = (index reg 0) ? (zipWith xorBool poly r1, r1)
+        (hms,tlms) = splitAt 1 ms
+        r1 = drop 1 reg ++ hms
+
+simpleCRC1 :: VecBool -> VecBool -> VecBool
+simpleCRC1 poly msg =  fst $ composeN step (length augmsg) (fw,0)
+  where
+    w = length poly
+    fw = replicate w false
+    augmsg = msg ++ fw
+    step (reg,i) = (reg',i+1)
+      where
+        reg' = (index reg 0) ? (zipWith xorBool poly r1, r1)
+        r1 = drop 1 reg ++ replicate 1 (index augmsg i)
+
+simpleCRC2 :: VecBool -> VecBool -> VecBool
+simpleCRC2 poly msg = forLoop (length augmsg) fw step
+  where
+    w = length poly
+    fw = replicate w false
+    augmsg = msg ++ fw
+    step i reg = reg'
+      where
+        reg' = (index reg 0) ? (zipWith xorBool poly r1, r1)
+        r1 = drop 1 reg ++ replicate 1 (index augmsg i)
+
+
+crc16ccitt :: Data Word16
+crc16ccitt = value 0x1021
+
+crc32ieee :: Data Word32
+crc32ieee = value 0x04C11DB7
+
+tst4 = eval $ int2BL crc16ccitt
+
+tstSimpleCRC = eval $ simpleCRC2 (int2BL crc16ccitt) (int2BL (8856 :: Data Word64))
+
+{--
+*Main> tstSimpleCRC
+[False,True,True,False,False,False,True,False,False,False,True,True,False,True,False,True]
+--}
+
+tstSimpleCRCAgain = eval $ simpleCRC2 (int2BL crc16ccitt) (int2BL (8856 :: Data Word64) ++ value [False,True,True,False,False,False,True,False,False,False,True,True,False,True,False,True])
+
+{--
+*Main> tstSimpleCRCAgain
+[False,False,False,False,False,False,False,False,False,False,False,False,False,False,False,False]
+--}
+
+table :: (Bits a, Type a) => Data a -> Data Index -> Data [a]
+table poly size = parallel (2^size) (calc poly size)
+
+
+calc :: (Bits a, Type a) => Data a -> Data Index -> Data Index -> Data a
+calc poly size i = i2n $ bL2Int $ simpleCRC1 (int2BL poly) (int2BLN size i)
+
+
+mTable :: (Type a, Bits a) => Data a -> Data Index -> Data Index -> Data [a]
+mTable poly size i = parallel (2^size) (\j -> calc poly (j `shiftL` (8*i)) size)
+
+calc1 :: Data Index -> Data [Word32]
+calc1 i = parallel 256 (\j -> tableCRCModCh (bytesR (j `shiftL` (8*i))))
+
+table32 :: Data [Word32]
+table32 = table  crc32ieee 8
+
+table16 :: Data [Word16]
+table16 = table crc16ccitt 8
+
+tstTab16 = eval $ table16
+
+{--
+*Main> tstTab16
+[0,4129,8258,12387,16516,20645,24774,28903,33032,37161,41290,45419,49548,53677,5
+7806,61935,4657,528,12915,8786,21173,17044,29431,25302,37689,33560,45947,41818,5
+4205,50076,62463,58334,9314,13379,1056,5121,25830,29895,17572,21637,42346,46411,
+34088,38153,58862,62927,50604,54669,13907,9842,5649,1584,30423,26358,22165,18100
+,46939,42874,38681,34616,63455,59390,55197,51132,18628,22757,26758,30887,2112,62
+41,10242,14371,51660,55789,59790,63919,35144,39273,43274,47403,23285,19156,31415
+,27286,6769,2640,14899,10770,56317,52188,64447,60318,39801,35672,47931,43802,278
+14,31879,19684,23749,11298,15363,3168,7233,60846,64911,52716,56781,44330,48395,3
+6200,40265,32407,28342,24277,20212,15891,11826,7761,3696,65439,61374,57309,53244
+,48923,44858,40793,36728,37256,33193,45514,41451,53516,49453,61774,57711,4224,16
+1,12482,8419,20484,16421,28742,24679,33721,37784,41979,46042,49981,54044,58239,6
+2302,689,4752,8947,13010,16949,21012,25207,29270,46570,42443,38312,34185,62830,5
+8703,54572,50445,13538,9411,5280,1153,29798,25671,21540,17413,42971,47098,34713,
+38840,59231,63358,50973,55100,9939,14066,1681,5808,26199,30326,17941,22068,55628
+,51565,63758,59695,39368,35305,47498,43435,22596,18533,30726,26663,6336,2273,144
+66,10403,52093,56156,60223,64286,35833,39896,43963,48026,19061,23124,27191,31254
+,2801,6864,10931,14994,64814,60687,56684,52557,48554,44427,40424,36297,31782,276
+55,23652,19525,15522,11395,7392,3265,61215,65342,53085,57212,44955,49082,36825,4
+0952,28183,32310,20053,24180,11923,16050,3793,7920]
+--}
+
+tab16 = value [0,4129,8258,12387,16516,20645,24774,28903,33032,37161,41290,45419,49548,53677,57806,61935,4657,528,12915,8786,21173,17044,29431,25302,37689,33560,45947,41818,54205,50076,62463,58334,9314,13379,1056,5121,25830,29895,17572,21637,42346,46411,34088,38153,58862,62927,50604,54669,13907,9842,5649,1584,30423,26358,22165,18100,46939,42874,38681,34616,63455,59390,55197,51132,18628,22757,26758,30887,2112,6241,10242,14371,51660,55789,59790,63919,35144,39273,43274,47403,23285,19156,31415,27286,6769,2640,14899,10770,56317,52188,64447,60318,39801,35672,47931,43802,27814,31879,19684,23749,11298,15363,3168,7233,60846,64911,52716,56781,44330,48395,36200,40265,32407,28342,24277,20212,15891,11826,7761,3696,65439,61374,57309,53244,48923,44858,40793,36728,37256,33193,45514,41451,53516,49453,61774,57711,4224,161,12482,8419,20484,16421,28742,24679,33721,37784,41979,46042,49981,54044,58239,62302,689,4752,8947,13010,16949,21012,25207,29270,46570,42443,38312,34185,62830,58703,54572,50445,13538,9411,5280,1153,29798,25671,21540,17413,42971,47098,34713,38840,59231,63358,50973,55100,9939,14066,1681,5808,26199,30326,17941,22068,55628,51565,63758,59695,39368,35305,47498,43435,22596,18533,30726,26663,6336,2273,14466,10403,52093,56156,60223,64286,35833,39896,43963,48026,19061,23124,27191,31254,2801,6864,10931,14994,64814,60687,56684,52557,48554,44427,40424,36297,31782,27655,23652,19525,15522,11395,7392,3265,61215,65342,53085,57212,44955,49082,36825,40952,28183,32310,20053,24180,11923,16050,3793,7920] :: Data [Word16]
+
+tstTab32 = eval $ table32
+
+{--
+*Main> tstTab32
+[0,79764919,159529838,222504665,319059676,398814059,445009330,507990021,63811935
+2,583659535,797628118,726387553,890018660,835552979,1015980042,944750013,1276238
+704,1221641927,1167319070,1095957929,1595256236,1540665371,1452775106,1381403509
+,1780037320,1859660671,1671105958,1733955601,2031960084,2111593891,1889500026,19
+52343757,2552477408,2632100695,2443283854,2506133561,2334638140,2414271883,21919
+15858,2254759653,3190512472,3135915759,3081330742,3009969537,2905550212,28509594
+11,2762807018,2691435357,3560074640,3505614887,3719321342,3648080713,3342211916,
+3287746299,3467911202,3396681109,4063920168,4143685023,4223187782,4286162673,377
+9000052,3858754371,3904687514,3967668269,881225847,809987520,1023691545,96923409
+4,662832811,591600412,771767749,717299826,311336399,374308984,453813921,53357647
+0,25881363,88864420,134795389,214552010,2023205639,2086057648,1897238633,1976864
+222,1804852699,1867694188,1645340341,1724971778,1587496639,1516133128,1461550545
+,1406951526,1302016099,1230646740,1142491917,1087903418,2896545431,2825181984,27
+70861561,2716262478,3215044683,3143675388,3055782693,3001194130,2326604591,23894
+56536,2200899649,2280525302,2578013683,2640855108,2418763421,2498394922,37699005
+19,3832873040,3912640137,3992402750,4088425275,4151408268,4197601365,4277358050,
+3334271071,3263032808,3476998961,3422541446,3585640067,3514407732,3694837229,364
+0369242,1762451694,1842216281,1619975040,1682949687,2047383090,2127137669,193846
+8188,2001449195,1325665622,1271206113,1183200824,1111960463,1543535498,148906962
+9,1434599652,1363369299,622672798,568075817,748617968,677256519,907627842,853037
+301,1067152940,995781531,51762726,131386257,177728840,240578815,269590778,349224
+269,429104020,491947555,4046411278,4126034873,4172115296,4234965207,3794477266,3
+874110821,3953728444,4016571915,3609705398,3555108353,3735388376,3664026991,3290
+680682,3236090077,3449943556,3378572211,3174993278,3120533705,3032266256,2961025
+959,2923101090,2868635157,2813903052,2742672763,2604032198,2683796849,2461293480
+,2524268063,2284983834,2364738477,2175806836,2238787779,1569362073,1498123566,14
+09854455,1355396672,1317987909,1246755826,1192025387,1137557660,2072149281,21351
+22070,1912620623,1992383480,1753615357,1816598090,1627664531,1707420964,29539018
+5,358241886,404320391,483945776,43990325,106832002,186451547,266083308,932423249
+,861060070,1041341759,986742920,613929101,542559546,756411363,701822548,33161969
+85,3244833742,3425377559,3370778784,3601682597,3530312978,3744426955,3689838204,
+3819031489,3881883254,3928223919,4007849240,4037393693,4100235434,4180117107,425
+9748804,2310601993,2373574846,2151335527,2231098320,2596047829,2659030626,247035
+9227,2550115596,2947551409,2876312838,2788305887,2733848168,3165939309,309470716
+2,3040238851,2985771188]
+--}
+
+tab32 = value [0,79764919,159529838,222504665,319059676,398814059,445009330,507990021,638119352,583659535,797628118,726387553,890018660,835552979,1015980042,944750013,1276238704,1221641927,1167319070,1095957929,1595256236,1540665371,1452775106,1381403509,1780037320,1859660671,1671105958,1733955601,2031960084,2111593891,1889500026,1952343757,2552477408,2632100695,2443283854,2506133561,2334638140,2414271883,2191915858,2254759653,3190512472,3135915759,3081330742,3009969537,2905550212,2850959411,2762807018,2691435357,3560074640,3505614887,3719321342,3648080713,3342211916,3287746299,3467911202,3396681109,4063920168,4143685023,4223187782,4286162673,3779000052,3858754371,3904687514,3967668269,881225847,809987520,1023691545,969234094,662832811,591600412,771767749,717299826,311336399,374308984,453813921,533576470,25881363,88864420,134795389,214552010,2023205639,2086057648,1897238633,1976864222,1804852699,1867694188,1645340341,1724971778,1587496639,1516133128,1461550545,1406951526,1302016099,1230646740,1142491917,1087903418,2896545431,2825181984,2770861561,2716262478,3215044683,3143675388,3055782693,3001194130,2326604591,2389456536,2200899649,2280525302,2578013683,2640855108,2418763421,2498394922,3769900519,3832873040,3912640137,3992402750,4088425275,4151408268,4197601365,4277358050,3334271071,3263032808,3476998961,3422541446,3585640067,3514407732,3694837229,3640369242,1762451694,1842216281,1619975040,1682949687,2047383090,2127137669,1938468188,2001449195,1325665622,1271206113,1183200824,1111960463,1543535498,1489069629,1434599652,1363369299,622672798,568075817,748617968,677256519,907627842,853037301,1067152940,995781531,51762726,131386257,177728840,240578815,269590778,349224269,429104020,491947555,4046411278,4126034873,4172115296,4234965207,3794477266,3874110821,3953728444,4016571915,3609705398,3555108353,3735388376,3664026991,3290680682,3236090077,3449943556,3378572211,3174993278,3120533705,3032266256,2961025959,2923101090,2868635157,2813903052,2742672763,2604032198,2683796849,2461293480,2524268063,2284983834,2364738477,2175806836,2238787779,1569362073,1498123566,1409854455,1355396672,1317987909,1246755826,1192025387,1137557660,2072149281,2135122070,1912620623,1992383480,1753615357,1816598090,1627664531,1707420964,295390185,358241886,404320391,483945776,43990325,106832002,186451547,266083308,932423249,861060070,1041341759,986742920,613929101,542559546,756411363,701822548,3316196985,3244833742,3425377559,3370778784,3601682597,3530312978,3744426955,3689838204,3819031489,3881883254,3928223919,4007849240,4037393693,4100235434,4180117107,4259748804,2310601993,2373574846,2151335527,2231098320,2596047829,2659030626,2470359227,2550115596,2947551409,2876312838,2788305887,2733848168,3165939309,3094707162,3040238851,2985771188] :: Data [Word32]
+
+leftByte ::  (Bits a, Type a, Integral a) => Data a -> Data Index
+leftByte a = i2n $ (a `shiftR` (bitSize a - 8)) .&. 0xFF
+
+byteIn :: (Bits a, Type a, Integral a) => Data Word8 -> Data a -> Data a
+byteIn b w = w `shiftL` 8 .|. i2n b
+
+
+tableCRC :: (Bits a, Type a, Integral a) =>
+            Data a -> Vector (Data Word8) -> Data a
+tableCRC poly msg = forLoop (length augmsg) 0 step
+  where
+    augmsg = msg ++ replicate ((bitSize poly) `div` 8) 0
+    step i reg
+      = byteIn (index augmsg i) reg `xor` getIx (table poly 8) (leftByte reg)
+
+
+tableCRC1 :: (Bits a, Type a, Integral a) =>
+             Data a -> Vector (Data Word8) -> Data a
+tableCRC1 poly msg = share (value (eval (table poly 8))) $ \tab ->
+                     forLoop (length augmsg) 0 (step tab)
+  where
+    augmsg = msg ++ replicate ((bitSize poly) `div` 8) 0
+    step tab i reg
+      = byteIn (index augmsg i) reg `xor` getIx tab (leftByte reg)
+
+tstTabCRC = compile $ tableCRC1 crc16ccitt
+
+{--
+main (v0)
+  v1 := [0,4129,8258,12387,16516,20645,24774,28903,33032,37161,41290,45419,49548
+,53677,57806,61935,4657,528,12915,8786,21173,17044,29431,25302,37689,33560,45947
+,41818,54205,50076,62463,58334,9314,13379,1056,5121,25830,29895,17572,21637,4234
+6,46411,34088,38153,58862,62927,50604,54669,13907,9842,5649,1584,30423,26358,221
+65,18100,46939,42874,38681,34616,63455,59390,55197,51132,18628,22757,26758,30887
+,2112,6241,10242,14371,51660,55789,59790,63919,35144,39273,43274,47403,23285,191
+56,31415,27286,6769,2640,14899,10770,56317,52188,64447,60318,39801,35672,47931,4
+3802,27814,31879,19684,23749,11298,15363,3168,7233,60846,64911,52716,56781,44330
+,48395,36200,40265,32407,28342,24277,20212,15891,11826,7761,3696,65439,61374,573
+09,53244,48923,44858,40793,36728,37256,33193,45514,41451,53516,49453,61774,57711
+,4224,161,12482,8419,20484,16421,28742,24679,33721,37784,41979,46042,49981,54044
+,58239,62302,689,4752,8947,13010,16949,21012,25207,29270,46570,42443,38312,34185
+,62830,58703,54572,50445,13538,9411,5280,1153,29798,25671,21540,17413,42971,4709
+8,34713,38840,59231,63358,50973,55100,9939,14066,1681,5808,26199,30326,17941,220
+68,55628,51565,63758,59695,39368,35305,47498,43435,22596,18533,30726,26663,6336,
+2273,14466,10403,52093,56156,60223,64286,35833,39896,43963,48026,19061,23124,271
+91,31254,2801,6864,10931,14994,64814,60687,56684,52557,48554,44427,40424,36297,3
+1782,27655,23652,19525,15522,11395,7392,3265,61215,65342,53085,57212,44955,49082
+,36825,40952,28183,32310,20053,24180,11923,16050,3793,7920] :: [Word16]
+  x3 := v0
+  x2 := (arrLength x3)
+  x6 := 4129 :: Word16
+  x5 := (bitSize x6)
+  x7 := 8 :: Int
+  x4 := (div x5 x7)
+  x1 := (x2 + x4)
+  x8 := 0 :: Word16
+  x9 := 0 :: Int
+  v3 := (tup2 x8 x9)
+
+  for v2 in 0 .. (x1-1) do
+    x14 := v3
+    x13 := (sel1 x14)
+    x15 := 8 :: Int
+    x12 := (shiftL x13 x15)
+    x20 := v3
+    x19 := (sel2 x20)
+    x22 := v0
+    x21 := (arrLength x22)
+    x18 := (x19 < x21)
+
+    if x18 then
+      x23 := v0
+      x25 := v3
+      x24 := (sel2 x25)
+      x17 := (getIx x23 x24)
+    else
+      x17 := 0 :: Word8
+    x16 := (i2n x17)
+    x11 := (x12 .|. x16)
+    x27 := v1
+    x32 := v3
+    x31 := (sel1 x32)
+    x36 := v3
+    x35 := (sel1 x36)
+    x34 := (bitSize x35)
+    x37 := 8 :: Int
+    x33 := (x34 - x37)
+    x30 := (shiftR x31 x33)
+    x38 := 255 :: Word16
+    x29 := (x30 .&. x38)
+    x28 := (i2n x29)
+    x26 := (getIx x27 x28)
+    x10 := (xor x11 x26)
+    x41 := v3
+    x40 := (sel2 x41)
+    x42 := 1 :: Int
+    x39 := (x40 + x42)
+    v3 := (tup2 x10 x39)
+  x0 := v3
+  out := (sel1 x0)
+--}
+
+
+tableCRC2 :: Vector (Data Word8) -> Data Word16
+tableCRC2 msg = share tab16 $ \tab -> fst (composeN (step tab) (length augmsg) (0,0))
+  where
+    augmsg = msg ++ replicate 2 0
+    step tab (reg, i) = (byteIn (index augmsg i) reg `xor` getIx  tab (leftByte reg), i+1)
+
+
+tstFastTab = compile tableCRC2
+
+tableCRC3 :: Vector (Data Word8) -> Data Word32
+tableCRC3 msg = share tab32 $ \tab -> fst (composeN (step tab) (length augmsg) (0,0))
+  where
+    augmsg = msg ++ replicate 4 0
+    step tab (reg, i) = (byteIn (index augmsg i) reg `xor` getIx  tab (leftByte reg), i+1)
+
+
+tableCRCMod :: (Bits a, Type a, Integral a) =>
+               Data a -> Vector (Data Word8) -> Data a
+tableCRCMod poly msg = share (value (eval (table poly 8))) $ \tab ->
+                       forLoop (length msg) 0 (step tab)
+  where
+    step tab i reg
+      = reg `shiftL` 8  `xor` getIx tab (leftByte reg `xor` i2n (index msg i))
+
+tableCRCModCh :: Vector (Data Word8) -> Data Word32
+tableCRCModCh msg = share tab32 $ \tab -> forLoop (length msg) 0 (step tab)
+  where
+    step tab i reg
+      = reg `shiftL` 8  `xor` getIx tab (leftByte reg `xor` i2n (index msg i))
+
+tstModTab = compile $ tableCRCMod crc16ccitt
+
+{--
+main (v0)
+  v1 := [0,4129,8258,12387,16516,20645,24774,28903,33032,37161,41290,45419,49548
+,53677,57806,61935,4657,528,12915,8786,21173,17044,29431,25302,37689,33560,45947
+,41818,54205,50076,62463,58334,9314,13379,1056,5121,25830,29895,17572,21637,4234
+6,46411,34088,38153,58862,62927,50604,54669,13907,9842,5649,1584,30423,26358,221
+65,18100,46939,42874,38681,34616,63455,59390,55197,51132,18628,22757,26758,30887
+,2112,6241,10242,14371,51660,55789,59790,63919,35144,39273,43274,47403,23285,191
+56,31415,27286,6769,2640,14899,10770,56317,52188,64447,60318,39801,35672,47931,4
+3802,27814,31879,19684,23749,11298,15363,3168,7233,60846,64911,52716,56781,44330
+,48395,36200,40265,32407,28342,24277,20212,15891,11826,7761,3696,65439,61374,573
+09,53244,48923,44858,40793,36728,37256,33193,45514,41451,53516,49453,61774,57711
+,4224,161,12482,8419,20484,16421,28742,24679,33721,37784,41979,46042,49981,54044
+,58239,62302,689,4752,8947,13010,16949,21012,25207,29270,46570,42443,38312,34185
+,62830,58703,54572,50445,13538,9411,5280,1153,29798,25671,21540,17413,42971,4709
+8,34713,38840,59231,63358,50973,55100,9939,14066,1681,5808,26199,30326,17941,220
+68,55628,51565,63758,59695,39368,35305,47498,43435,22596,18533,30726,26663,6336,
+2273,14466,10403,52093,56156,60223,64286,35833,39896,43963,48026,19061,23124,271
+91,31254,2801,6864,10931,14994,64814,60687,56684,52557,48554,44427,40424,36297,3
+1782,27655,23652,19525,15522,11395,7392,3265,61215,65342,53085,57212,44955,49082
+,36825,40952,28183,32310,20053,24180,11923,16050,3793,7920] :: [Word16]
+  x1 := v0
+  x0 := (arrLength x1)
+  v3 := 0 :: Word16
+
+  for v2 in 0 .. (x0-1) do
+    x3 := v3
+    x4 := 8 :: Int
+    x2 := (shiftL x3 x4)
+    x6 := v1
+    x11 := v3
+    x14 := v3
+    x13 := (bitSize x14)
+    x15 := 8 :: Int
+    x12 := (x13 - x15)
+    x10 := (shiftR x11 x12)
+    x16 := 255 :: Word16
+    x9 := (x10 .&. x16)
+    x8 := (i2n x9)
+    x19 := v0
+    x20 := v2
+    x18 := (getIx x19 x20)
+    x17 := (i2n x18)
+    x7 := (xor x8 x17)
+    x5 := (getIx x6 x7)
+    v3 := (xor x2 x5)
+  out := v3
+--}
+
+bytes :: (Bits t, Type t, Integral t) => Data t -> Vector (Data Word8)
+bytes w = map i2n (Indexed l ixf)
+  where
+    ixf k = (w `shiftR` (8*k)) .&. 0xFF
+    l = numBytes w
+
+
+bytesR :: (Bits t, Type t, Integral t) => Data t -> Vector (Data Word8)
+bytesR w = map i2n (Indexed l ixf)
+  where
+    ixf k = (w `shiftR` (8*(l-1-k))) .&. 0xFF
+    l = numBytes w
+
+numBytes :: (Bits t, Type t, Integral t) => Data t -> Data Index
+numBytes a = (bitSize a) `div` 8
+
+
+m1 = eval $ tableCRCMod crc32ieee (value [1..20])
+
+{--
+*Main> m1
+3245827117
+--}
+
+m2 = eval $ tableCRCMod crc32ieee (value [1..20] ++ bytesR (3245827117 :: Data Word32))
+
+{--
+*Main> m2
+0
+--}
+
+sliceCRC :: (Type a, Bits a, Integral a) =>
+             Data a -> Vector (Data a) -> Data a
+sliceCRC poly msg = share (value (eval (parallel n (mTable poly 8)))) $ \tab ->
+                    forLoop (length msg) 0 (step tab)
+  where
+    n = numBytes poly
+    step tab i reg  = fold xor 0 $ g . bytes $ reg `xor` w1
+      where
+        w1 = index msg i
+        g (Indexed len ixf) = Indexed len ixf'
+           where
+             ixf' j = getIx (getIx tab j) (i2n (ixf j))
+
+
+
+
+m3 = eval $ sliceCRC crc16ccitt (value [1..5])
+
+
+sliceCRC' :: Vector (Data Word32) -> Data Word32
+sliceCRC' msg = share (value (eval (parallel 4 calc1))) $ \tab ->
+                forLoop (length msg) 0 (step tab)
+  where
+    step tab i reg = fold xor 0 $ g . bytes $ reg `xor` w1
+      where
+        w1 = index msg i
+        g (Indexed len ixf) = Indexed len ixf'
+           where
+             ixf' j = getIx (getIx tab j) (i2n (ixf j))
+
+
+fold1 :: (Syntax a) => (a -> a -> a) -> Vector a -> a
+fold1 f as = fold f (index as 0) (drop 1 as)
+
+m4 = eval $ sliceCRC' (value [1..100])
+{--
+*Main> m4
+3886779157
+--}
+
+m5 = eval $ sliceCRC' (value [1..5] ++ replicate 1 3886779157)
+
+m6 = eval $ sliceCRC' (value [1..100] ++ replicate 1 4076606085)
+
+{--
+main (v0)
+  v1 := [[0,79764919,159529838,222504665,319059676,398814059,445009330,507990021
+,638119352,583659535,797628118,726387553,890018660,835552979,1015980042,94475001
+3,1276238704,1221641927,1167319070,1095957929,1595256236,1540665371,1452775106,1
+381403509,1780037320,1859660671,1671105958,1733955601,2031960084,2111593891,1889
+500026,1952343757,2552477408,2632100695,2443283854,2506133561,2334638140,2414271
+883,2191915858,2254759653,3190512472,3135915759,3081330742,3009969537,2905550212
+,2850959411,2762807018,2691435357,3560074640,3505614887,3719321342,3648080713,33
+42211916,3287746299,3467911202,3396681109,4063920168,4143685023,4223187782,42861
+62673,3779000052,3858754371,3904687514,3967668269,881225847,809987520,1023691545
+,969234094,662832811,591600412,771767749,717299826,311336399,374308984,453813921
+,533576470,25881363,88864420,134795389,214552010,2023205639,2086057648,189723863
+3,1976864222,1804852699,1867694188,1645340341,1724971778,1587496639,1516133128,1
+461550545,1406951526,1302016099,1230646740,1142491917,1087903418,2896545431,2825
+181984,2770861561,2716262478,3215044683,3143675388,3055782693,3001194130,2326604
+591,2389456536,2200899649,2280525302,2578013683,2640855108,2418763421,2498394922
+,3769900519,3832873040,3912640137,3992402750,4088425275,4151408268,4197601365,42
+77358050,3334271071,3263032808,3476998961,3422541446,3585640067,3514407732,36948
+37229,3640369242,1762451694,1842216281,1619975040,1682949687,2047383090,21271376
+69,1938468188,2001449195,1325665622,1271206113,1183200824,1111960463,1543535498,
+1489069629,1434599652,1363369299,622672798,568075817,748617968,677256519,9076278
+42,853037301,1067152940,995781531,51762726,131386257,177728840,240578815,2695907
+78,349224269,429104020,491947555,4046411278,4126034873,4172115296,4234965207,379
+4477266,3874110821,3953728444,4016571915,3609705398,3555108353,3735388376,366402
+6991,3290680682,3236090077,3449943556,3378572211,3174993278,3120533705,303226625
+6,2961025959,2923101090,2868635157,2813903052,2742672763,2604032198,2683796849,2
+461293480,2524268063,2284983834,2364738477,2175806836,2238787779,1569362073,1498
+123566,1409854455,1355396672,1317987909,1246755826,1192025387,1137557660,2072149
+281,2135122070,1912620623,1992383480,1753615357,1816598090,1627664531,1707420964
+,295390185,358241886,404320391,483945776,43990325,106832002,186451547,266083308,
+932423249,861060070,1041341759,986742920,613929101,542559546,756411363,701822548
+,3316196985,3244833742,3425377559,3370778784,3601682597,3530312978,3744426955,36
+89838204,3819031489,3881883254,3928223919,4007849240,4037393693,4100235434,41801
+17107,4259748804,2310601993,2373574846,2151335527,2231098320,2596047829,26590306
+26,2470359227,2550115596,2947551409,2876312838,2788305887,2733848168,3165939309,
+3094707162,3040238851,2985771188],[0,3524903388,2700254735,1928028115,1159995817
+,2537414773,3856056230,936345210,2319991634,1481736846,716889437,4171439233,3479
+986939,494248743,1872690420,3179756840,273783571,3259521743,2963473692,165640723
+2,1433778874,2272033638,4119274677,664724841,2585385025,1207966109,988497486,390
+8208530,3745380840,220477492,2144298983,2916525627,547567142,4072339450,21528351
+13,1380477429,1703352207,3080640083,3312814464,392972380,2867557748,2029171880,1
+69470843,3623889575,4023342301,1037473025,1329449682,2636385038,821210421,380707
+9657,2415932218,1108996838,1976994972,2815380800,3575911059,121492303,3132812903
+,1755525051,440954984,3360797108,4288597966,763825682,1600934337,2373292061,1095
+134284,2472521104,3786732099,866988959,73551333,3598421049,2760954858,1988694582
+,3406704414,420998850,1811722513,3118821581,2385120951,1546899307,785944760,4240
+527716,1360525151,2198746755,4058343760,603760780,338941686,3324647210,303256600
+9,1725466917,3680482317,155612625,2074946050,2847206366,2658899364,1281512568,10
+49168811,3968911991,1642420842,3019676598,3239560293,319686073,616659907,4141398
+559,2217993676,1445602320,3953989944,968153316,1264551735,2571519723,2928228497,
+2089875789,242984606,3697436482,1907671417,2746024101,3511050102,56598186,881909
+968,3867746572,2489482975,1182514947,4227629611,702890999,1527651364,2300042744,
+3201868674,1824612958,506084749,3425958993,2190268568,1351948612,578700951,40333
+16683,3349739825,363935981,1733977918,3041109730,147102666,3671939606,2822112709
+,2049950745,1306573411,2683927487,3977389164,1057744304,2463974283,1086620247,84
+1997700,3761642584,3623445026,98608126,1997274157,2769436145,412418265,339822208
+5,3093798614,1786666762,1571889520,2410209452,4249075583,794459811,2721050302,18
+82599266,48066737,3502551405,3876310807,890375883,1207521560,2514522308,67788337
+2,4202589232,2291479523,1519186495,1833143365,3210366361,3450933834,531157910,29
+94632109,1617409137,311225250,3231001214,4149892100,625186264,1470679563,2242972
+631,943077119,3929012003,2563025136,1256024364,2098337622,2936788618,3722479961,
+267995269,3284841684,299070728,1664625371,2971790087,2263782781,1425495201,63937
+2146,4094020270,1233319814,2610640474,3916458377,996780117,212260399,3737065459,
+2891204640,2119010812,3550162887,25357851,1936306632,2708500500,2529103470,11517
+82834,911052897,3830731197,1507028117,2345315657,4179751578,725103430,485969212,
+3471740128,3154498355,1847333615,3815342834,829440814,1134238973,2441272609,2790
+105947,1951687303,113196372,3567713416,1763819936,3141009532,3386073007,46626366
+7,738582537,4263256533,2365029894,1592704986,4080540129,555866173,1405781998,217
+8106930,3055302728,1678113172,384738887,3304548251,2037406387,2875825007,3649225
+916,194708832,1012169498,3998071494,2628183317,1321149641],[0,30977159,61954318,
+40498569,123908636,112860827,80997138,84625301,247817272,253610175,225721654,212
+636081,161994276,142572195,169250602,198058925,495634544,475161847,507220350,534
+986233,451443308,456185579,425272162,411144165,323988552,311886031,285144390,287
+726017,338501204,368423635,396117850,373615581,991269088,986528871,950323694,964
+453737,1014440700,1034915451,1069972466,1042208629,902886616,872962143,912371158
+,934871377,850544324,862644803,822288330,819704653,647977104,659026967,623772062
+,620145945,570288780,539313675,575452034,596909829,677002408,696422447,736847270
+,708036897,792235700,786440755,747231162,760314685,1982538176,2012450119,1973057
+742,1950536777,1900647388,1888567131,1928907474,1931503189,2028881400,2033641855
+,2069830902,2055712881,2139944932,2119457635,2084417258,2112160365,1805773232,17
+86332471,1745924286,1774722105,1824742316,1830549291,1869742754,1856679461,17010
+88648,1690050831,1725289606,1728935937,1644576660,1675531027,1639409306,16179389
+73,1295954208,1290149287,1318053934,1331119273,1247544124,1266986939,1240291890,
+1211496117,1140577560,1109621151,1078627350,1100095633,1150904068,1161939843,119
+3819658,1190171277,1354004816,1366087127,1392844894,1390251225,1473694540,144378
+4651,1416073794,1438596805,1584471400,1604956655,1572881510,1545136353,149446232
+4,1489699827,1520629370,1534745341,3965076352,3985567495,4024900238,3997152777,3
+946115484,3941358875,3901073554,3915187221,3801294776,3813378879,3777134262,3774
+534193,3857814948,3827906851,3863006378,3885522989,4057762800,4026804087,4067283
+710,4088757881,4139661804,4150695275,4111425762,4107783269,4279889864,4274078543
+,4238915270,4251982401,4168834516,4188270931,4224320730,4195526749,3611546464,36
+00515047,3572664942,3576309481,3491848572,3522809339,3549444210,3527972085,36494
+84632,3630046175,3661098582,3689890513,3739485508,3745294787,3713358922,37002897
+41,3402177296,3406935959,3380101662,3365990041,3450579212,3430090123,3457871874,
+3485621381,3289153320,3319059375,3351062054,3328543393,3278818612,3266732467,323
+5877946,3238475965,2591908416,2611334855,2580298574,2551486409,2636107868,263031
+9323,2662238546,2675320277,2495088248,2506140415,2533973878,2530341873,248058378
+0,2449610979,2422992234,2444444141,2281155120,2251228855,2219242302,2241748921,2
+157254700,2169353387,2200191266,2197613989,2301808136,2297062031,2323879686,2338
+012033,2387639316,2408108179,2380342554,2352581021,2708009632,2695912999,2732174
+254,2734753577,2785689788,2815618107,2780502450,2757997877,2947389080,2926918175
+,2887569302,2915328785,2832147588,2836891651,2877193610,2863059213,3168942800,31
+74733399,3209913310,3196833625,3145763020,3126338635,3090272706,3119086917,29889
+24648,3019895407,2979399654,2957945697,3041258740,3030204531,3069490682,30731206
+37],[0,3698170551,3155831001,1618457198,2096450565,2694370994,3236914396,4783468
+59,4192901130,629605053,1173401811,2577214052,2233455631,1500663480,956693718,38
+48824417,4145294755,729397012,1259210106,2539888589,2346803622,1468857105,939215
+231,3952530376,251573673,3532861214,3001326960,1854474183,1913387436,2925945627,
+3457274229,310135746,3941156593,914676806,1458794024,2325673119,2518420212,12489
+56483,705045037,4134254746,319020795,3480110156,2937714210,1937009813,1878430462
+,3013281865,3555506727,260120720,503147346,3247501797,2716287883,2106251580,1627
+924311,3177561568,3708948366,25138489,3826774872,947546607,1477303169,2220900662
+,2564996957,1150232042,620271492,4170517811,3507720277,226364130,1829353612,2976
+129595,2917588048,1904953063,301790345,3448860222,687409247,4103377640,249791296
+6,1217313329,1410090074,2288115437,3893783683,880539188,638041590,4201260865,258
+5629999,1181749144,1525871091,2258594628,3874019626,981812125,3756860924,5876922
+7,1677135141,3214579602,2736286201,2138436430,520241440,3278887831,1006294692,38
+85452307,2279669373,1535993034,1192204961,2606891030,4212503160,662186191,325584
+8622,511562777,2114610807,2724723904,3202679467,1653119004,50276978,3734155461,3
+438213895,277045680,1895093214,2895726953,2954606338,1819684277,201433051,349674
+0204,889479949,3916036538,2300464084,1433653603,1240542984,2510075327,4125820881
+,696687974,2800106781,2055972778,452728260,3331428211,3658707224,108981167,17118
+88833,3127165814,1594664215,2204188576,3809906126,1065031545,603580690,428791901
+3,2682503627,1133403004,1374818494,2376043017,3991418983,830841552,755457211,405
+0306572,2434626658,1299246805,2820180148,1953829379,335716461,3362732762,3572352
+177,142630406,1761078376,3030021855,1276083180,2422399323,4027929397,746113410,8
+21704681,3969363294,2363498288,1351452039,3051742182,1770551633,167758655,358313
+6136,3373314019,360527188,1963624250,2842107277,3139130959,1735838968,117538454,
+3681346593,3354270282,461603069,2079601299,2811865124,1123143237,2661045490,4276
+872860,579238955,1040482880,3798538487,2183047833,1584607278,2012589384,28788797
+43,3421472145,394403622,184607053,3614276602,3071986068,1802982179,2384409922,13
+83247861,839196059,3999827756,4075452743,780657648,1324372382,2459814697,2162262
+251,1552685660,1023125554,3767939717,4229221614,544822873,1074717751,2623766144,
+2030770401,2774958678,3306238008,427600527,100553956,3650342483,3118758973,17035
+36266,2635918265,1097953550,554091360,4251670999,3790186428,1032076555,157624304
+5,2174621138,1693873075,3097225476,3639368554,75612637,402866102,3295585537,2753
+107823,2020904408,1778959898,3060096173,3591564995,176125044,385714719,339843908
+0,2867307206,1988769905,2481085968,1334822055,804812489,4086688894,4011266581,86
+3668386,1393375948,2405474427]] :: [[Word32]]
+  x2 := v0
+  x1 := (arrLength x2)
+  x3 := 0 :: Word32
+  x4 := 0 :: Int
+  v3 := (tup2 x3 x4)
+
+  for v2 in 0 .. (x1-1) do
+    x10 := 3 :: Int
+    x11 := 0 :: Int
+    x9 := (x10 - x11)
+    x12 := 1 :: Int
+    x8 := (x9 + x12)
+    x7 := (i2n x8)
+    x17 := v3
+    x16 := (sel1 x17)
+    x19 := v0
+    x21 := v3
+    x20 := (sel2 x21)
+    x18 := (getIx x19 x20)
+    x15 := (xor x16 x18)
+    x14 := (bitSize x15)
+    x22 := 8 :: Int
+    x13 := (div x14 x22)
+    x6 := (min x7 x13)
+    v5 := 0 :: Word32
+
+    for v4 in 0 .. (x6-1) do
+      x23 := v5
+      x26 := v1
+      x29 := v4
+      x28 := (i2n x29)
+      x30 := 0 :: Int
+      x27 := (x28 + x30)
+      x25 := (getIx x26 x27)
+      x37 := v3
+      x36 := (sel1 x37)
+      x39 := v0
+      x41 := v3
+      x40 := (sel2 x41)
+      x38 := (getIx x39 x40)
+      x35 := (xor x36 x38)
+      x43 := 8 :: Int
+      x50 := v3
+      x49 := (sel1 x50)
+      x52 := v0
+      x54 := v3
+      x53 := (sel2 x54)
+      x51 := (getIx x52 x53)
+      x48 := (xor x49 x51)
+      x47 := (bitSize x48)
+      x55 := 8 :: Int
+      x46 := (div x47 x55)
+      x56 := 1 :: Int
+      x45 := (x46 - x56)
+      x63 := v3
+      x62 := (sel1 x63)
+      x65 := v0
+      x67 := v3
+      x66 := (sel2 x67)
+      x64 := (getIx x65 x66)
+      x61 := (xor x62 x64)
+      x60 := (bitSize x61)
+      x68 := 8 :: Int
+      x59 := (div x60 x68)
+      x69 := v4
+      x58 := (x59 - x69)
+      x70 := 1 :: Int
+      x57 := (x58 - x70)
+      x44 := (x45 - x57)
+      x42 := (x43 * x44)
+      x34 := (shiftR x35 x42)
+      x71 := 255 :: Word32
+      x33 := (x34 .&. x71)
+      x32 := (i2n x33)
+      x31 := (i2n x32)
+      x24 := (getIx x25 x31)
+      v5 := (xor x23 x24)
+    x5 := v5
+    x74 := v3
+    x73 := (sel2 x74)
+    x75 := 1 :: Int
+    x72 := (x73 + x75)
+    v3 := (tup2 x5 x72)
+  x0 := v3
+  out := (sel1 x0)
+--}
+
+
+onCond :: Data Bool -> Data Int -> Data Int
+onCond b m = m .&. (- (b2i b))
+
+sumEven1 :: Vector (Data Int) -> Data Int
+sumEven1 = sum . map (\i -> onCond (i .&. 1 == 0) i)
+
+swapOE1 :: (Syntax a) => Vector a -> Vector a
+swapOE1 v = Indexed (length v) ixf
+  where
+    ixf i = (i `mod` 2 == 0) ? (index v (i+1), index v (i-1))
+
+-- same as above
+swapOE2 :: Vector a -> Vector a
+swapOE2 = premap (\i -> (i `mod` 2 == 0) ?  (i+1,i-1))
+
+swapOE3 :: Vector a -> Vector a
+swapOE3 = premap (`xor` 1)
+
+premap :: (Data Index -> Data Index) -> Vector a -> Vector a
+premap f (Indexed l ixf) = Indexed l (ixf . f)
+
+
+bitr :: Data Index -> Data Index -> Data Index
+bitr n a =
+    share (oneBitsN n) $ \mask -> (complement mask .&. a) .|. rev mask
+  where
+    rev mask = rotateL (reverseBits (mask .&. a)) n
+
+bitRev :: Data Index -> Vector a -> Vector a
+bitRev = premap . bitr
+
+countUp :: Data Length -> Vector (Data Index)
+countUp n = Indexed n id
+
+pipe :: Syntax a => (Data Index -> a -> a) -> Vector (Data Index) -> a -> a
+pipe = flip . fold . flip
+
+specbr m n v = bL2Int (l ++ r')
+  where
+    iv = int2BLN m v
+    (l,r) = splitAt (m-n) iv
+    r' = reverse r
+
+
+
+
+{--
+checkCRC :: (VecBool -> VecBool -> VecBool) -> VecBool -> VecBool -> Data Bool
+checkCRC crc poly msg = fold && true (map not (crc poly (msg ++ (crc poly msg))))
+--}

@@ -0,0 +1,109 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}++import Language.Syntactic++++----------------------------------------+-- a)+----------------------------------------++data Circ a+  where+    Const :: Bool -> Circ Bool+    Inv   :: Circ Bool -> Circ Bool+    And   :: Circ Bool -> Circ Bool -> Circ Bool++data ConstSym a where Const' :: Bool -> ConstSym (Full Bool)+data InvSym a   where Inv' :: InvSym (Bool :-> Full Bool)+data AndSym a   where And' :: AndSym (Bool :-> Bool :-> Full Bool)++type CircDom = InvSym :+: AndSym :+: ConstSym++++----------------------------------------+-- b)+----------------------------------------++consT :: (ConstSym :<: dom) => Bool -> ASTF dom Bool+consT a = inject (Const' a)++inv :: (InvSym :<: dom) => ASTF dom Bool -> ASTF dom Bool+inv a = inject Inv' :$: a++anD :: (AndSym :<: dom) =>+    ASTF dom Bool -> ASTF dom Bool -> ASTF dom Bool+anD a b = inject And' :$: a :$: b++++----------------------------------------+-- c)+----------------------------------------++circ1 :: Circ Bool+circ1 = And (Const False) (And (Const True) (Inv (Const False)))++circ2 :: ASTF CircDom Bool+circ2 = anD (consT False) (anD (consT True) (inv (consT False)))++++----------------------------------------+-- d)+----------------------------------------++fromCirc :: Circ a -> ASTF CircDom a+fromCirc (Const a) = inject (Const' a)+fromCirc (Inv a)   = inject Inv' :$: fromCirc a+fromCirc (And a b) = inject And' :$: fromCirc a :$: fromCirc b++toCirc :: ASTF CircDom a -> Circ a+toCirc (project -> Just (Const' a))         = Const a+toCirc ((project -> Just Inv') :$: a)       = Inv (toCirc a)+toCirc ((project -> Just And') :$: a :$: b) = And (toCirc a) (toCirc b)++++----------------------------------------+-- e)+----------------------------------------++instance Render ConstSym where render (Const' a) = show a+instance Render InvSym   where render Inv' = "inv"+instance Render AndSym   where render And' = "and"++instance Eval ConstSym where evaluate (Const' a) = fromEval a+instance Eval InvSym   where evaluate Inv' = fromEval not+instance Eval AndSym   where evaluate And' = fromEval (&&)++++----------------------------------------+-- f)+----------------------------------------++data NandSym a where Nand :: NandSym (Bool :-> Bool :-> Full Bool)++instance Render NandSym where render Nand = "nand"++instance Eval NandSym where evaluate Nand = fromEval $ \a b -> not (a && b)++nandify' :: AST (InvSym :+: AndSym :+: dom) a -> AST (NandSym :+: dom) a+nandify' ((project -> Just Inv') :$: a) = inject Nand :$: a' :$: a'+  where+    a' = nandify a+nandify' ((project -> Just And') :$: a :$: b) = inject Nand :$: ab :$: ab+  where+    ab = inject Nand :$: nandify a :$: nandify b+nandify' (c :$: a) = nandify' c :$: nandify a+nandify' (Symbol (InjectR (InjectR a))) = Symbol (InjectR a)++nandify ::+    ASTF (InvSym :+: AndSym :+: dom) a -> ASTF (NandSym :+: dom) a+nandify = nandify'+

@@ -0,0 +1,26 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}++import Language.Syntactic+import Language.Syntactic.Constructs.Symbol++import MuFeldspar.Core++++data ForLoop' a+  where+    ForLoop' :: Type st =>+        ForLoop' (Length :-> st :-> (Index -> st -> st) :-> Full st)++instance IsSymbol ForLoop'+  where+    toSym ForLoop' = Sym "forLoop" forLoop+      where+        forLoop len init body = foldl (flip body) init (reverse [0 .. len-1])++instance ExprEq ForLoop' where exprEq     = exprEqSym+instance Render ForLoop' where renderPart = renderPartSym+instance Eval   ForLoop' where evaluate   = evaluateSym+instance ToTree ForLoop'+

@@ -0,0 +1,61 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE ViewPatterns #-}++module Option where++++import Language.Syntactic++import MuFeldspar.Core+import MuFeldspar.Frontend++++data Option a = Option { isSome :: Data Bool, fromSome :: a }++instance Syntax a => Syntactic (Option a) FeldDomainAll+  where+    type Internal (Option a) = (Bool, Internal a)+    desugar = desugar . freezeOption . fmap resugar+    sugar   = fmap resugar . unfreezeOption . sugar++instance Functor Option+  where+    fmap f opt = opt {fromSome = f (fromSome opt)}++instance Monad Option+  where+    return = some+    a >>= f = b { isSome = isSome a ? (isSome b, false) }+      where+        b = f (fromSome a)++++freezeOption :: Type a => Option (Data a) -> Data (Bool,a)+freezeOption a = resugar (isSome a, fromSome a)++unfreezeOption :: Type a => Data (Bool,a) -> Option (Data a)+unfreezeOption (resugar -> (valid,a)) = Option valid a++undef :: Syntax a => a+undef = resugar $ getIx (value []) 0++some :: a -> Option a+some = Option true++none :: Syntax a => Option a+none = Option false undef++option :: Syntax b => b -> (a -> b) -> Option a -> b+option noneCase someCase opt = isSome opt ?+    ( someCase (fromSome opt)+    , noneCase+    )++oplus :: Syntax a => Option a -> Option a -> Option a+oplus a b = isSome a ? (a,b)+

@@ -0,0 +1,370 @@+module Main where
+
+import qualified Prelude
+
+import MuFeldspar.Prelude
+
+
+import MuFeldspar.Core
+--import MuFeldspar.Tuple
+import MuFeldspar.Frontend
+import MuFeldspar.Vector
+
+
+import Imperative.Imperative
+import Imperative.Compiler
+
+import Data.Word
+import Data.Bits (Bits)
+
+type VecBool = Vector (Data Bool)
+
+type VecInt = Vector (Data Int)
+
+
+
+-- Exercise 1
+
+composeN :: (Syntax st) => (st -> st) -> Data Length -> st -> st
+composeN f l i0 = forLoop l i0 g
+  where
+    g _ st = f st
+
+tri :: (Syntax a) => (a -> a)  -> Vector a -> Vector a
+tri f (Indexed len ixf) = indexed len ixf'
+  where
+    ixf' i = composeN f i (ixf i)
+
+
+tri1 :: (Syntax a) => (a -> a)  -> Vector a -> Vector a
+tri1 f (Indexed len ixf) = indexed len ixf'
+  where
+    ixf' i = forLoop i (ixf i) (\_ -> f)
+
+
+{--
+*Main> eval $ tri (*2) (1...6)
+[1,4,12,32,80,192]
+*Main> eval $ tri1 (*2) (1...6)
+[1,4,12,32,80,192]
+--}
+
+
+-- Exercise 2
+
+swapOE1 :: (Syntax a) => Vector a -> Vector a
+swapOE1 v = Indexed (length v) ixf
+  where
+    ixf i = (i `mod` 2 == 0) ? (index v (i+1), index v (i-1))
+
+-- same as above
+swapOE2 :: Vector a -> Vector a
+swapOE2 = premap (\i -> (i `mod` 2 == 0) ?  (i+1,i-1))
+
+swapOE3 :: Vector a -> Vector a
+swapOE3 = premap (`xor` 1)
+
+premap :: (Data Index -> Data Index) -> Vector a -> Vector a
+premap f (Indexed l ixf) = Indexed l (ixf . f)
+
+
+
+-- Exercise 3
+
+pows2 :: Data Int -> Vector (Data Int)
+pows2 k = Indexed k (2^)    
+
+
+
+pow2 :: Data Index -> Data Index
+pow2 k = 1 << k                   -- or  2^k    
+
+pows21 :: Data Length -> Vector (Data Index)
+pows21 k = Indexed k pow2   
+
+
+
+
+
+-- Exercise 4
+
+pad :: Data Length -> VecBool -> VecBool
+pad l v = (replicate (l - length v) false) ++ v
+
+xorBool :: Data Bool -> Data Bool -> Data Bool
+xorBool a b = not (a == b)
+
+crcAdd :: VecBool -> VecBool -> VecBool
+crcAdd as bs = zipWith xorBool (pad m as) (pad m bs)
+  where
+    m = max (length as) (length bs)
+
+
+
+
+
+
+-- Exercise 5
+
+-- direct implementation using reverseBits
+bitr :: Data Index -> Data Index -> Data Index
+bitr n a =
+    share (oneBitsN n) $ \mask -> (complement mask .&. a) .|. rev mask
+  where
+    rev mask = rotateL (reverseBits (mask .&. a)) n
+
+bitRev :: Data Index -> Vector a -> Vector a
+bitRev n = premap (bitr n)
+
+oneBitsN :: Data Index -> Data Index
+oneBitsN  = complement . zeroBitsN
+
+zeroBitsN :: Data Index -> Data Index
+zeroBitsN = shiftL allOnes
+
+allOnes :: Data Index
+allOnes = complement 0
+
+
+
+bitrH :: Index -> Data Index -> Data Index
+bitrH n  a =
+    share (oneBitsN vn) $ \mask -> (complement mask .&. a) .|. rev mask
+  where
+    rev mask = rotateL (reverseBits (mask .&. a)) vn
+    vn = value n
+
+
+
+
+
+-- transliteration of solution from bithacks
+bitr1 :: Data Index -> Data Index -> Data Index
+bitr1 n i = snd (pipe stage (countUp n) (i, i >> n))
+  where
+    stage _ (i,r) = (i>>1, (i .&. 1) .|. (r<<1))
+
+bitRev1 :: Data Index -> Vector a -> Vector a
+bitRev1 n = premap (bitr1 n)
+
+countUp :: Data Length -> Vector (Data Index)
+countUp n = Indexed n id
+
+pipe :: Syntax a => (Data Index -> a -> a) -> Vector (Data Index) -> a -> a
+pipe = flip . fold . flip 
+
+
+
+-- A version of composeN that depends on a *Haskell* value
+
+composeNH :: Index -> (a -> a) -> a -> a
+composeNH 0 f = id
+composeNH n f = (composeNH (n-1) f) . f
+
+
+-- Now use this to make bitr. Note the type.
+
+bitr1H :: Index -> Data Index -> Data Index
+bitr1H n i = snd (composeNH n stage (i, i >> vn))
+  where
+    stage (i,r) = (i>>1, (i .&. 1) .|. (r<<1))
+    vn = value n
+
+
+-- Now we must provide the n parameter at compile time
+-- and the recursion gets unwound
+
+{--
+
+main (v0)
+  x3 := v0
+  x4 := 1 :: Int
+  x2 := (shiftR x3 x4)
+  x5 := 1 :: Int
+  x1 := (shiftR x2 x5)
+  x6 := 1 :: Int
+  x0 := (x1 .&. x6)
+  x11 := v0
+  x12 := 1 :: Int
+  x10 := (shiftR x11 x12)
+  x13 := 1 :: Int
+  x9 := (x10 .&. x13)
+  x17 := v0
+  x18 := 1 :: Int
+  x16 := (x17 .&. x18)
+  x21 := v0
+  x22 := 3 :: Int
+  x20 := (shiftR x21 x22)
+  x23 := 1 :: Int
+  x19 := (shiftL x20 x23)
+  x15 := (x16 .|. x19)
+  x24 := 1 :: Int
+  x14 := (shiftL x15 x24)
+  x8 := (x9 .|. x14)
+  x25 := 1 :: Int
+  x7 := (shiftL x8 x25)
+  out := (x0 .|. x7)
+
+
+Compare with  printMain $ bitr1
+which gives the expected for loop
+
+main (v0,v1)
+  x1 := v0
+  x2 := v1
+  x4 := v1
+  x5 := v0
+  x3 := (shiftR x4 x5)
+  v3 := (tup2 x2 x3)
+
+  for v2 in 0 .. (x1-1) do
+    x8 := v3
+    x7 := (sel1 x8)
+    x9 := 1 :: Int
+    x6 := (shiftR x7 x9)
+    x13 := v3
+    x12 := (sel1 x13)
+    x14 := 1 :: Int
+    x11 := (x12 .&. x14)
+    x17 := v3
+    x16 := (sel2 x17)
+    x18 := 1 :: Int
+    x15 := (shiftL x16 x18)
+    x10 := (x11 .|. x15)
+    v3 := (tup2 x6 x10)
+  x0 := v3
+  out := (sel2 x0)
+
+--}
+
+
+
+
+
+
+specbr m n v = bL2Int (l ++ r')
+  where
+    iv = int2BLN m v
+    (l,r) = splitAt (m-n) iv
+    r' = reverse r
+
+testBit :: (Type a, Bits a) => Data a -> Data Index -> Data Bool
+testBit l i = not ((l .&. (1<<i)) == 0)
+
+
+int2BL :: (Type a, Bits a)  =>  Data a -> VecBool
+int2BL l = reverse $ indexed (bitSize l) (testBit l)
+
+
+int2BLN :: Data Length -> Data Int -> VecBool
+int2BLN n v = reverse $ indexed n (testBit v)
+
+
+bL2Int :: VecBool -> Data Int
+bL2Int bs = scalarProduct (reverse (map b2i bs)) (pows2 (length bs))
+
+bL2Int' :: VecBool -> Data Int
+bL2Int' = sum . tri (*2) . map b2i
+
+scalarProduct :: (Type a, Num a) => Vector (Data a) -> Vector (Data a) -> Data a
+scalarProduct as bs = sum (zipWith (*) as bs)
+
+
+
+
+
+-- Exercise 6   (See slides)
+
+-- 2^n input FFT. Applies to sub-parts of input vector
+-- of length 2^(n+i). 
+-- There is currently no check that the input vector is at least of length 2^n
+
+
+countDown n = reverse (indexed n id)
+
+fft :: Data Index ->  Vector (Data Complex) -> Vector (Data Complex)
+fft n = bitRev n . lin stage (countDown n)
+  where
+    stage k = combx f g (bitZero k) (flipBit k) twid 
+      where
+        f a b _ = a + b
+        g a b t = t * (a-b)
+        twid i  = cis ((-(value pi)*(i2n (lsbsN k i)))/  i2n (pow2 k))
+
+
+
+combx f g c p x (Indexed l ixf) =  Indexed l ixf'
+      where
+        ixf' i = (c i) ? (f ai pi xi, g pi ai xi)
+          where
+            ai = ixf i
+            pi = ixf (p i)
+            xi = x i
+
+
+
+
+lin :: Syntax a => (b -> a -> a) -> Vector b -> a -> a
+lin f (Indexed len ixf) a = forLoop len a (\i st -> f (ixf i) st)
+
+lsbsN :: Data Index -> Data Index -> Data Index
+lsbsN k i = i .&. oneBitsN k
+
+bitZero :: Data Index -> Data Index -> Data Bool
+bitZero k i = (i .&. (1<<k)) == 0
+
+flipBit ::  Data Index -> Data Index -> Data Index
+flipBit k = (`xor` (1<<k))
+
+
+
+
+-- Exercise 7 bitonic sort
+
+-- bitonic merge (see slides)
+
+comb :: (Syntax a) =>
+        (t -> t -> a) -> (t -> t -> a)
+         -> (Data Index -> Data Bool) -> (Data Index -> Data Index)
+         -> Vector t 
+         -> Vector a
+comb f g c p (Indexed l ixf) = Indexed l ixf'
+  where
+    ixf' i = (c i) ? (f a b, g a b)
+      where
+        a = ixf i
+        b = ixf (p i)
+
+apart :: (Syntax a) =>
+         (t -> t -> a) -> (t -> t -> a)
+         -> Data Index
+         -> Vector t
+         -> Vector a
+apart f g k = comb f g (bitZero k) (flipBit k)
+
+
+
+
+
+
+bMerge :: Data Index -> Vector (Data Int) -> Vector (Data Int)
+bMerge n = lin (apart min max) (countDown n)
+  
+
+-- now we'd like to be able to reverse half of each 2^n length sub-vector
+
+halfRev :: Data Index -> Vector (Data a) -> Vector (Data a)
+halfRev n = premap (\i -> (bitZero n' i) ? (i ,i `xor` oneBitsN n'))
+  where
+    n' = n-1
+
+
+merge :: Data Index -> Vector (Data Int) -> Vector (Data Int)
+merge n = bMerge n . halfRev n 
+
+bsort :: Data Index -> Vector (Data Int) -> Vector (Data Int)
+bsort n = lin merge (1...n)
+
+
+
+

@@ -0,0 +1,46 @@+import qualified Prelude++import MuFeldspar.Prelude+import MuFeldspar.Core+import MuFeldspar.Frontend+import MuFeldspar.Vector++import Imperative.Imperative+import Imperative.Compiler++++prog1 :: Data Int+prog1 = 23 + min 45 2++test1_1 = eval prog1+test1_2 = printMain $ compile prog1++prog2 = (prog1==3) ? (prog1*3, prog1*4)++test2_1 = eval prog2+test2_2 = printMain $ compile prog2+  -- Note how prog1 is only computed once++prog3 :: Vector (Vector (Data Int)) -> Vector (Vector (Data Int))+prog3 = map reverse . map reverse++test3_1 = eval prog3 [[1,2,3],[4,5],[6]]+test3_2 = printMain $ compile prog3++prog4 :: Vector (Vector (Data Int)) -> Data Int+prog4 = sum . map sum . map reverse . map reverse++test4_1 = eval prog4 [[1,2,3],[4,5],[6]]+test4_2 = printMain $ compile prog4++prog5 = sequential 10 1 $ \i st -> (i+st, (i+1)*st)++test5_1 = eval prog5+test5_2 = printMain $ compile prog5++prog6 as bs = sum (zipWith (*) as bs) :: Data Index++test6_1 = eval prog6 [10..19] [20..29]+test6_2 = printMain $ compile prog6+

@@ -0,0 +1,204 @@+{-# OPTIONS_GHC -fcontext-stack=25 #-}++{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++module Imperative.Compiler where++++import Prelude as P++import Control.Monad.State++import Language.Syntactic+import Language.Syntactic.Constructs.Symbol+import Language.Syntactic.Constructs.Literal+import Language.Syntactic.Constructs.Condition+import Language.Syntactic.Constructs.Tuple+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder+import Language.Syntactic.Sharing.SimpleCodeMotion++import MuFeldspar.Core+import Imperative.Imperative++++--------------------------------------------------------------------------------+-- * Misc.+--------------------------------------------------------------------------------++type Result = Ident++ident :: String -> VarId -> Ident+ident base i = base ++ show i++freshVar :: State VarId String+freshVar = do+    v <- get; put (v+1)+    return (ident "x" v)++viewInfix :: String -> Maybe String+viewInfix name+    | head name P.== '(' && last name P.== ')' = Just (tail $ init name)+    | otherwise = Nothing++projLambda :: (Lambda Poly :<: dom) => AST dom a -> Maybe VarId+projLambda = liftM getVar . project+  where+    getVar :: Lambda Poly a -> VarId+    getVar (Lambda var) = var++++--------------------------------------------------------------------------------+-- * Generic machinery+--------------------------------------------------------------------------------++class Compile sub dom+  where+    compileSym :: sub a -> Result -> HList (AST dom) a -> State VarId Prog++instance (Compile sub1 dom, Compile sub2 dom) => Compile (sub1 :+: sub2) dom+  where+    compileSym (InjectL a) = compileSym a+    compileSym (InjectR a) = compileSym a++compileM :: Compile dom dom => Result -> ASTF dom a -> State VarId Prog+compileM result = queryNodeSimple (flip compileSym result)++compileFresh :: Compile dom dom => ASTF dom a -> State VarId (Result,Prog)+compileFresh arg = do+    var  <- freshVar+    prog <- compileM var arg+    return (var,prog)++compileTop :: (Compile dom dom, Lambda Poly :<: dom) =>+    [Ident] -> ASTF dom a -> Main+compileTop params ((projLambda -> Just inp) :$: body) =+    compileTop (ident "v" inp:params) body+compileTop params a = Main (reverse params) prog+  where+    prog = flip evalState 0 $ compileM "out" a++compile :: Syntactic a FeldDomainAll => a -> Main+compile = compileTop [] . reifySmart poly++++instance Compile dom dom => Compile (Sym ctx) dom+  where+    compileSym (Sym name _) result args = do+        (varArgs,progs) <- liftM unzip $ listHListM compileFresh args+        return $ concat progs ++ [result := expr varArgs]+      where+        expr [a,b]+            | Just op <- viewInfix name = Op op (Var a) (Var b)+        expr args                       = App name (map Var args)++compileSymb :: (IsSymbol expr, Compile dom dom) =>+    expr a -> Result -> HList (AST dom) a -> State VarId Prog+compileSymb = compileSym . toSym++++--------------------------------------------------------------------------------+-- * Compilation of sub-domains+--------------------------------------------------------------------------------++instance Compile (Variable Poly) dom+  where+    compileSym (Variable i) result _ = return [result := Var (ident "v" i)]++instance Compile (Lambda Poly) dom+  where+    compileSym = error "Can only compile top-level Lambda"++instance Compile (Literal Poly) dom+  where+    compileSym (Literal a) result _ = return [result := Lit (show a)]++instance Compile dom dom => Compile NUM dom        where compileSym = compileSymb+instance Compile dom dom => Compile INTEGRAL dom   where compileSym = compileSymb+instance Compile dom dom => Compile FRACTIONAL dom where compileSym = compileSymb+instance Compile dom dom => Compile Conversion dom where compileSym = compileSymb+instance Compile dom dom => Compile COMPLEX dom    where compileSym = compileSymb+instance Compile dom dom => Compile BITS dom       where compileSym = compileSymb+instance Compile dom dom => Compile Logic dom      where compileSym = compileSymb+instance Compile dom dom => Compile ORD dom        where compileSym = compileSymb+instance Compile dom dom => Compile Array dom      where compileSym = compileSymb++instance Compile dom dom => Compile (Condition Poly) dom+  where+    compileSym Condition result (cond :*: tHEN :*: eLSE :*: Nil) = do+        (condVar,condProg) <- compileFresh cond+        thenProg           <- compileM result tHEN+        elseProg           <- compileM result eLSE+        return $ condProg ++ [Cond (Var condVar) thenProg elseProg]++instance Compile dom dom => Compile (Tuple Poly) dom  where compileSym = compileSymb+instance Compile dom dom => Compile (Select Poly) dom where compileSym = compileSymb++instance (Compile dom dom, Lambda Poly :<: dom) => Compile (Let Poly Poly) dom+  where+    compileSym Let result (a :*: ((projLambda -> Just var) :$: body) :*: Nil) =+        liftM2 (++)+          (compileM (ident "v" var) a)+          (compileM result body)++instance (Compile dom dom, Lambda Poly :<: dom) => Compile Parallel dom+  where+    compileSym par@Parallel result (len :*: (lamIx :$: body) :*: Nil)+        | Just ix <- projLambda lamIx+        = do (lenVar,lenProg)   <- compileFresh len+             (elemVar,bodyProg) <- compileFresh body+             let ixVar          =  ident "v" ix+                 emptyProg      =  result := Lit "[]"+                 assignProg     =  result := App "updateArr" [Var result, Var ixVar, Var elemVar]+             let fullBody       =  bodyProg ++ [assignProg]+             return+               $  lenProg+               ++ [emptyProg, For True (Var lenVar) ixVar fullBody]++instance (Compile dom dom, Lambda Poly :<: dom) => Compile Sequential dom+  where+    compileSym seq@Sequential result (len :*: init :*: (lamIx :$: (lamSt :$: body)) :*: Nil)+        | Just ix <- projLambda lamIx+        , Just st <- projLambda lamSt+        = do (lenVar,lenProg)   <- compileFresh len+             let ixVar          =  ident "v" ix+                 stVar          =  ident "v" st+             initProg           <- compileM stVar init+             (bodyVar,bodyProg) <- compileFresh body+             elemVar            <- freshVar+             let fstProg        =  elemVar := App "sel1" [Var bodyVar]+                 sndProg        =  stVar   := App "sel2" [Var bodyVar]+                 emptyProg      =  result  := Lit "[]"+                 assignProg     =  result  := App "setIx" [Var result, Var ixVar, Var elemVar]+             let fullBody       =  bodyProg ++ [fstProg,sndProg,assignProg]+             return+               $  lenProg+               ++ initProg+               ++ [emptyProg, For False (Var lenVar) ixVar fullBody]++instance (Compile dom dom, Lambda Poly :<: dom) => Compile ForLoop dom+  where+    compileSym ForLoop result (len :*: init :*: (lamIx :$: (lamSt :$: body)) :*: Nil)+        | Just ix <- projLambda lamIx+        , Just st <- projLambda lamSt+        = do (lenVar,lenProg) <- compileFresh len+             let ixVar        =  ident "v" ix+                 stVar        =  ident "v" st+             initProg         <- compileM stVar init+             bodyProg         <- compileM stVar body+             return+               $  lenProg+               ++ initProg+               ++ [For False (Var lenVar) ixVar bodyProg, result := Var stVar]+

@@ -0,0 +1,98 @@+module Imperative.Imperative where++++import Data.List++++type Ident = String++data Expr+    = Lit String           -- Literal+    | Var Ident            -- Variable+    | App String [Expr]    -- Function call+    | Op String Expr Expr  -- Binary operator++type IsPar = Bool  --  Parallel or sequential loop?++data Stmt+    = Nop                        -- No-op+    | Ident := Expr              -- Assignment+    | Cond Expr Prog Prog        -- Conditional+    | For IsPar Expr Ident Prog  -- For loop++type Prog = [Stmt]++data Main = Main+    { mainInp  :: [Ident]+    , mainBody :: Prog+    }++instance Show Main+  where+    show = renderMain++++paren :: String -> String+paren = ("(" ++) . (++ ")")++-- | Like 'unlines', but without the final newline+unLines :: [String] -> String+unLines = concat . intersperse "\n"++indent :: Int -> String -> String+indent n = unLines . map move . lines+  where+    move = (replicate n ' ' ++)++renderExpr :: Expr -> String+renderExpr (Lit a)        = a+renderExpr (Var ident)    = ident+renderExpr (App str args) = paren $ unwords (str : map renderExpr args)+renderExpr (Op str a b)   = paren $ unwords [renderExpr a, str, renderExpr b]++mkNop :: Prog -> Prog+mkNop []   = [Nop]+mkNop prog = prog++renderStmt :: Stmt -> String+renderStmt Nop             = "nop"+renderStmt (ident := expr) = ident ++ " := " ++ renderExpr expr+renderStmt (Cond cond tHEN eLSE)+    | isSmall =+        ("if " ++ renderExpr cond ++ " then " ++ tRend ++ " else " ++ eRend)+    | otherwise =+        ("\nif " ++ renderExpr cond ++ " then\n")+          +++        indent 2 tRend+          +++        "\nelse\n"+          +++        indent 2 eRend+  where+    t       = mkNop tHEN+    e       = mkNop eLSE+    tRend   = renderProg t+    eRend   = renderProg e+    isSmall = length (lines tRend) <= 1 && length (lines eRend) <= 1+renderStmt (For isPar len index body) =+    (loop ++ index ++ " in 0 .. (" ++ renderExpr len ++ "-1) do\n")+      +++    indent 2 (renderProg body)+  where+    loop = if isPar then "\npar " else "\nfor "++renderProg :: Prog -> String+renderProg = unLines . map renderStmt++renderMain :: Main -> String+renderMain (Main params prog) =+    ("main (" ++ concat (intersperse "," params) ++ ")\n")+      +++    indent 2 (renderProg prog)++printMain :: Main -> IO ()+printMain = putStrLn . (++"\n") . renderMain+

@@ -0,0 +1,460 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-}++module MuFeldspar.Core where++++import Data.Bits (Bits)+import qualified Data.Bits as Bits+import Data.Complex hiding (Complex)+import qualified Data.Complex as C+import Data.List+import Data.Typeable++import Language.Syntactic+import Language.Syntactic.Constructs.Symbol+import Language.Syntactic.Constructs.Literal+import Language.Syntactic.Constructs.Condition+import Language.Syntactic.Constructs.Tuple+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder++++--------------------------------------------------------------------------------+-- * Types+--------------------------------------------------------------------------------++-- | Set of supported types+class    (Eq a, Show a, Typeable a) => Type a+instance (Eq a, Show a, Typeable a) => Type a++type Length = Int+type Index  = Int++++--------------------------------------------------------------------------------+-- * Numeric functions+--------------------------------------------------------------------------------++data NUM a+  where+    Abs  :: (Type a, Num a) => NUM (a :-> Full a)+    Sign :: (Type a, Num a) => NUM (a :-> Full a)+    Add  :: (Type a, Num a) => NUM (a :-> a :-> Full a)+    Sub  :: (Type a, Num a) => NUM (a :-> a :-> Full a)+    Mul  :: (Type a, Num a) => NUM (a :-> a :-> Full a)++instance IsSymbol NUM+  where+    toSym Abs  = Sym "abs" abs+    toSym Sign = Sym "signum" signum+    toSym Add  = Sym "(+)" (+)+    toSym Sub  = Sym "(-)" (-)+    toSym Mul  = Sym "(*)" (*)++instance ExprEq   NUM where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   NUM where renderPart = renderPartSym+instance Eval     NUM where evaluate   = evaluateSym+instance ToTree   NUM+instance EvalBind NUM where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly NUM where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * Integral functions+--------------------------------------------------------------------------------++data INTEGRAL a+  where+    Div :: (Type a, Integral a) => INTEGRAL (a :-> a :-> Full a)+    Mod :: (Type a, Integral a) => INTEGRAL (a :-> a :-> Full a)+    Exp :: (Type a, Integral a) => INTEGRAL (a :-> a :-> Full a)++instance IsSymbol INTEGRAL+  where+    toSym Div = Sym "div" div+    toSym Mod = Sym "mod" mod+    toSym Exp = Sym "(^)" (^)++instance ExprEq   INTEGRAL where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   INTEGRAL where renderPart = renderPartSym+instance Eval     INTEGRAL where evaluate   = evaluateSym+instance ToTree   INTEGRAL+instance EvalBind INTEGRAL where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly INTEGRAL where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * Fractional functions+--------------------------------------------------------------------------------++data FRACTIONAL a+  where+    FDiv :: (Type a, Fractional a) => FRACTIONAL (a :-> a :-> Full a)++instance IsSymbol FRACTIONAL+  where+    toSym FDiv = Sym "(/)" (/)++instance ExprEq   FRACTIONAL where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   FRACTIONAL where renderPart = renderPartSym+instance Eval     FRACTIONAL where evaluate   = evaluateSym+instance ToTree   FRACTIONAL+instance EvalBind FRACTIONAL where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly FRACTIONAL where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * Conversion functions+--------------------------------------------------------------------------------++data Conversion a+  where+    I2N :: (Type a, Integral a, Type b, Num b) => Conversion (a :-> Full b)+    F2I :: (Type a, Integral a)                => Conversion (Float :-> Full a)+    B2I :: (Type a, Integral a)                => Conversion (Bool :-> Full a)++instance IsSymbol Conversion+  where+    toSym I2N = Sym "i2n" (fromInteger.toInteger)+    toSym F2I = Sym "f2i" truncate+    toSym B2I = Sym "b2i" (\b -> if b then 1 else 0)++instance ExprEq   Conversion where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   Conversion where renderPart = renderPartSym+instance Eval     Conversion where evaluate   = evaluateSym+instance ToTree   Conversion+instance EvalBind Conversion where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly Conversion where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * Complex numbers+--------------------------------------------------------------------------------++type Complex = C.Complex Float++data COMPLEX a+  where+    Complex   :: COMPLEX (Float :-> Float :-> Full Complex)+    RealPart  :: COMPLEX (Complex :-> Full Float)+    ImagPart  :: COMPLEX (Complex :-> Full Float)+    MkPolar   :: COMPLEX (Float :-> Float :-> Full Complex)+    Magnitude :: COMPLEX (Complex :-> Full Float)+    Phase     :: COMPLEX (Complex :-> Full Float)++instance IsSymbol COMPLEX+  where+    toSym Complex   = Sym "complex"   (:+)+    toSym RealPart  = Sym "realPart"  realPart+    toSym ImagPart  = Sym "imagPart"  imagPart+    toSym MkPolar   = Sym "mkPolar"   mkPolar+    toSym Magnitude = Sym "magnitude" magnitude+    toSym Phase     = Sym "phase"     phase++instance ExprEq   COMPLEX where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   COMPLEX where renderPart = renderPartSym+instance Eval     COMPLEX where evaluate   = evaluateSym+instance ToTree   COMPLEX+instance EvalBind COMPLEX where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly COMPLEX where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * Bit manipulation+--------------------------------------------------------------------------------++data BITS a+  where+    Complement  :: (Type a, Bits a) => BITS (a :-> Full a)+    BitAnd      :: (Type a, Bits a) => BITS (a :-> a :-> Full a)+    BitOr       :: (Type a, Bits a) => BITS (a :-> a :-> Full a)+    Xor         :: (Type a, Bits a) => BITS (a :-> a :-> Full a)+    ShiftL      :: (Type a, Bits a) => BITS (a :-> Index :-> Full a)+    ShiftR      :: (Type a, Bits a) => BITS (a :-> Index :-> Full a)+    RotateL     :: (Type a, Bits a) => BITS (a :-> Index :-> Full a)+    RotateR     :: (Type a, Bits a) => BITS (a :-> Index :-> Full a)+    BitSize     :: (Type a, Bits a) => BITS (a :-> Full Index)+    ReverseBits :: (Type a, Bits a) => BITS (a :-> Full a)++instance IsSymbol BITS+  where+    toSym Complement  = Sym "complement" Bits.complement+    toSym BitAnd      = Sym "(.&.)" (Bits..&.)+    toSym BitOr       = Sym "(.|.)" (Bits..|.)+    toSym Xor         = Sym "xor" Bits.xor+    toSym ShiftL      = Sym "shiftL" Bits.shiftL+    toSym ShiftR      = Sym "shiftR" Bits.shiftR+    toSym RotateL     = Sym "rotateL" Bits.rotateL+    toSym RotateR     = Sym "rotateR" Bits.rotateR+    toSym BitSize     = Sym "bitSize" Bits.bitSize+    toSym ReverseBits = Sym "reverseBits" reverseBits+      where+        reverseBits :: Bits.Bits b => b -> b+        reverseBits b = revLoop b 0 (0 `asTypeOf` b)+          where+            bitSize = Bits.bitSize b+            revLoop b i n+              | i Prelude.>= bitSize = n+              | Bits.testBit b i =+                  revLoop b (i+1) (Bits.setBit n (bitSize - i - 1))+              | otherwise = revLoop b (i+1) n++++instance ExprEq   BITS where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   BITS where renderPart = renderPartSym+instance Eval     BITS where evaluate   = evaluateSym+instance ToTree   BITS+instance EvalBind BITS where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly BITS where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * Logic operations+--------------------------------------------------------------------------------++data Logic a+  where+    Eq  :: Type a => Logic (a :-> a :-> Full Bool)+    Not :: Logic (Bool :-> Full Bool)+    And :: Logic (Bool :-> Bool :-> Full Bool)+    Or  :: Logic (Bool :-> Bool :-> Full Bool)++instance IsSymbol Logic+  where+    toSym Eq    = Sym "(==)" (==)+    toSym Not   = Sym "not" not+    toSym And   = Sym "(&&)" (&&)+    toSym Or    = Sym "(||)" (||)++instance ExprEq   Logic where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   Logic where renderPart = renderPartSym+instance Eval     Logic where evaluate   = evaluateSym+instance ToTree   Logic+instance EvalBind Logic where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly Logic where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * Functions on ordered types+--------------------------------------------------------------------------------++data ORD a+  where+    Less    :: (Type a, Ord a) => ORD (a :-> a :-> Full Bool)+    LEQ     :: (Type a, Ord a) => ORD (a :-> a :-> Full Bool)+    Greater :: (Type a, Ord a) => ORD (a :-> a :-> Full Bool)+    GEQ     :: (Type a, Ord a) => ORD (a :-> a :-> Full Bool)+    Min     :: (Type a, Ord a) => ORD (a :-> a :-> Full a)+    Max     :: (Type a, Ord a) => ORD (a :-> a :-> Full a)++instance IsSymbol ORD+  where+    toSym Less    = Sym "(<)" (<)+    toSym LEQ     = Sym "(<=)" (<=)+    toSym Greater = Sym "(>)" (>)+    toSym GEQ     = Sym "(>=)" (>=)+    toSym Min     = Sym "min" min+    toSym Max     = Sym "max" max++instance ExprEq   ORD where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   ORD where renderPart = renderPartSym+instance Eval     ORD where evaluate   = evaluateSym+instance ToTree   ORD+instance EvalBind ORD where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly ORD where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * Array functions+--------------------------------------------------------------------------------++data Array a+  where+    GetLength :: Type a => Array ([a] :-> Full Length)+    SetLength :: Type a => Array (Length :-> [a] :-> Full [a])+    GetIx     :: Type a => Array ([a] :-> Index :-> Full a)++instance IsSymbol Array+  where+    toSym GetLength = Sym "getLength" length+    toSym SetLength = Sym "setLength" take+    toSym GetIx     = Sym "getIx" getIx+      where+        getIx as i+            | (i >= length as) || (i < 0) = error "getIx: index out of bounds"+            | otherwise                   = as !! i++instance ExprEq   Array where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   Array where renderPart = renderPartSym+instance Eval     Array where evaluate   = evaluateSym+instance ToTree   Array+instance EvalBind Array where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly Array where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * Parallel arrays+--------------------------------------------------------------------------------++data Parallel a+  where+    Parallel :: Type a => Parallel (Length :-> (Index -> a) :-> Full [a])++instance IsSymbol Parallel+  where+    toSym Parallel = Sym "parallel" parallelEval+      where+        parallelEval len ixf = map ixf [0 .. len-1]++instance ExprEq   Parallel where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   Parallel where renderPart = renderPartSym+instance Eval     Parallel where evaluate   = evaluateSym+instance ToTree   Parallel+instance EvalBind Parallel where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly Parallel where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * Sequential arrays+--------------------------------------------------------------------------------++data Sequential a+  where+    Sequential :: (Type st, Type a) =>+        Sequential (Length :-> st :-> (Index -> st -> (a,st)) :-> Full [a])++instance IsSymbol Sequential+  where+    toSym Sequential = Sym "sequential" sequentialEval+      where+        sequentialEval l init step = snd $ mapAccumL evalStep init [0 .. l-1]+          where+            evalStep st i = (st',a) where (a,st') = step i st++instance ExprEq   Sequential where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   Sequential where renderPart = renderPartSym+instance Eval     Sequential where evaluate   = evaluateSym+instance ToTree   Sequential+instance EvalBind Sequential where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly Sequential where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * For loops+--------------------------------------------------------------------------------++data ForLoop a+  where+    ForLoop :: Type st =>+        ForLoop (Length :-> st :-> (Index -> st -> st) :-> Full st)++instance IsSymbol ForLoop+  where+    toSym ForLoop = Sym "forLoop" forLoopEval+      where+        forLoopEval len init body = foldl (flip body) init [0 .. len-1]++instance ExprEq   ForLoop where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   ForLoop where renderPart = renderPartSym+instance Eval     ForLoop where evaluate   = evaluateSym+instance ToTree   ForLoop+instance EvalBind ForLoop where evalBindSym = evalBindSymDefault++instance MaybeWitnessSat Poly ForLoop where maybeWitnessSat _ _ = Just SatWit++++--------------------------------------------------------------------------------+-- * Feldspar domain+--------------------------------------------------------------------------------++type FeldDomain+    =   Literal Poly+    :+: Condition Poly+    :+: Tuple Poly+    :+: Select Poly+    :+: Let Poly Poly+    :+: NUM+    :+: INTEGRAL+    :+: FRACTIONAL+    :+: Conversion+    :+: COMPLEX+    :+: BITS+    :+: Logic+    :+: ORD+    :+: Array+    :+: Parallel+    :+: Sequential+    :+: ForLoop++type FeldDomainAll = HODomain Poly FeldDomain++newtype Data a = Data { unData :: ASTF FeldDomainAll a }++instance Type a => Syntactic (Data a) FeldDomainAll+  where+    type Internal (Data a) = a+    desugar = unData+    sugar   = Data++-- | Specialization of the 'Syntactic' class for the Feldspar domain+class    (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a+instance (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a++instance Type a => Eq (Data a)+  where+    Data a == Data b = alphaEq poly (reify poly a) (reify poly b)++instance Type a => Show (Data a)+  where+    show (Data a) = render $ reify poly a++++--------------------------------------------------------------------------------+-- * Back ends+--------------------------------------------------------------------------------++printFeld :: Syntactic a FeldDomainAll => a -> IO ()+printFeld = printExpr . reify poly++drawFeld :: Syntactic a FeldDomainAll => a -> IO ()+drawFeld = drawAST . reify poly++eval :: Syntactic a FeldDomainAll => a -> Internal a+eval = evalBind . reify poly+

@@ -0,0 +1,218 @@+{-# OPTIONS_GHC -fcontext-stack=30 #-}++{-# LANGUAGE GADTs #-}+{-# LANGUAGE ViewPatterns #-}++module MuFeldspar.Frontend where++++import Data.Bits (Bits)++import Language.Syntactic+import Language.Syntactic.Constructs.Symbol+import Language.Syntactic.Constructs.Literal+import Language.Syntactic.Constructs.Condition+import Language.Syntactic.Constructs.TupleSyntacticPoly+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder++import MuFeldspar.Core++++value :: Syntax a => Internal a -> a+value = sugarSymCtx poly . Literal++false :: Data Bool+false = value False++true :: Data Bool+true = value True++-- | For types containing some kind of \"thunk\", this function can be used to+-- force computation+force :: Syntax a => a -> a+force = resugar++desugarD :: Syntax a => a -> Data (Internal a)+desugarD = resugar++sugarD :: Syntax a => Data (Internal a) -> a+sugarD = resugar++share :: (Syntax a, Syntax b) => a -> (a -> b) -> b+share = sugarSym (letBind poly)++instance (Type a, Num a) => Num (Data a)+  where+    fromInteger = value . fromInteger+    abs         = sugarSym Abs+    signum      = sugarSym Sign+    (+)         = sugarSym Add+    (-)         = sugarSym Sub+    (*)         = sugarSym Mul++div :: (Type a, Integral a) => Data a -> Data a -> Data a+div = sugarSym Div++mod :: (Type a, Integral a) => Data a -> Data a -> Data a+mod = sugarSym Mod++(^) :: (Type a, Integral a) => Data a -> Data a -> Data a+(^) = sugarSym Exp++instance (Type a, Fractional a) => Fractional (Data a)+  where+    fromRational = value . fromRational+    (/)          = sugarSym FDiv++i2n :: (Type a, Integral a, Type b, Num b) => Data a -> Data b+i2n = sugarSym I2N++f2i :: (Type a, Integral a) => Data Float -> Data a+f2i = sugarSym F2I++b2i :: (Type a, Integral a) => Data Bool -> Data a+b2i = sugarSym B2I++complex :: Data Float -> Data Float -> Data Complex+complex = sugarSym Complex++realPart :: Data Complex -> Data Float+realPart = sugarSym RealPart++imagPart :: Data Complex -> Data Float+imagPart = sugarSym ImagPart++mkPolar :: Data Float -> Data Float -> Data Complex+mkPolar = sugarSym MkPolar++magnitude :: Data Complex -> Data Float+magnitude = sugarSym Magnitude++phase :: Data Complex -> Data Float+phase = sugarSym Phase++polar :: Data Complex -> (Data Float, Data Float)+polar a = (magnitude a, phase a)++cis :: Data Float -> Data Complex+cis = mkPolar 1++++complement :: (Type a, Bits a) => Data a -> Data a+complement = sugarSym Complement++(.&.) :: (Type a, Bits a) => Data a -> Data a -> Data a+(.&.) = sugarSym BitAnd++(.|.) :: (Type a, Bits a) => Data a -> Data a -> Data a+(.|.) = sugarSym BitOr++xor :: (Type a, Bits a) => Data a -> Data a -> Data a+xor = sugarSym Xor++shiftL :: (Type a, Bits a) => Data a -> Data Index -> Data a+shiftL = sugarSym ShiftL++shiftR :: (Type a, Bits a) => Data a -> Data Index -> Data a+shiftR = sugarSym ShiftR++(<<), (>>) :: (Type a, Bits a) => Data a -> Data Index -> Data a+(<<) = shiftL+(>>) = shiftR++infixl 5 <<, >>++rotateL :: (Type a, Bits a) => Data a -> Data Index -> Data a+rotateL = sugarSym RotateL++rotateR :: (Type a, Bits a) => Data a -> Data Index -> Data a+rotateR = sugarSym RotateR++bitSize :: (Type a, Bits a) => Data a -> Data Index+bitSize = sugarSym BitSize++reverseBits :: (Type a, Bits a) => Data a -> Data a+reverseBits = sugarSym ReverseBits++(==) :: Type a => Data a -> Data a -> Data Bool+(==) = sugarSym Eq++not :: Data Bool -> Data Bool+not = sugarSym Not++(&&) :: Data Bool -> Data Bool -> Data Bool+(&&) = sugarSym And++(||) :: Data Bool -> Data Bool -> Data Bool+(||) = sugarSym Or++(<) :: (Type a, Ord a) => Data a -> Data a -> Data Bool+(<) = sugarSym Less++(<=) :: (Type a, Ord a) => Data a -> Data a -> Data Bool+(<=) = sugarSym LEQ++(>) :: (Type a, Ord a) => Data a -> Data a -> Data Bool+(>) = sugarSym Greater++(>=) :: (Type a, Ord a) => Data a -> Data a -> Data Bool+(>=) = sugarSym GEQ++max :: (Type a, Ord a) => Data a -> Data a -> Data a+max = sugarSym Max++min :: (Type a, Ord a) => Data a -> Data a -> Data a+min = sugarSym Min++(?) :: Syntax a => Data Bool -> (a,a) -> a+cond ? (t,e) = sugarSymCtx poly Condition cond t e++++parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a]++parallel len ixf+    | getIx :$: arr :$: var0 <- body+    , Just GetIx <- project getIx+    , Just (Variable 0) <- prjCtx poly var0+    = setLength len $ Data arr+  where+    body = unData $ ixf $ Data $ inject (Variable 0 `withContext` poly)+  -- This case is an optimization that's included because it has a great effect+  -- on the size of the generated code.++parallel len ixf = sugarSym Parallel len ixf++++sequential :: (Type a, Syntax st) =>+    Data Length -> st -> (Data Index -> st -> (Data a, st)) -> Data [a]+sequential = sugarSym Sequential++forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st+forLoop = sugarSym ForLoop++getLength :: Type a => Data [a] -> Data Length+getLength = sugarSym GetLength++++setLength :: Type a => Data Length -> Data [a] -> Data [a]++setLength (desugar -> ((project -> Just GetLength) :$: arr')) arr+    | alphaEq poly (reify poly arr') (reify poly $ unData arr)+    = arr+  -- This case is an optimization that's needed for the optimization of+  -- 'parallel' to work properly.++setLength arr len = sugarSym SetLength arr len++++getIx :: Type a => Data [a] -> Data Index -> Data a+getIx = sugarSym GetIx+

@@ -0,0 +1,11 @@+module MuFeldspar.Prelude+    ( module Prelude+    ) where++import Prelude hiding+    ( (==), (&&), (||), (<), (<=), (>), (>=), (^), (++), (>>)+    , div, max, min, mod, not+    , concat, drop, length, map, replicate, reverse, splitAt, sum, take, unzip, zip+    , zipWith+    )+

@@ -0,0 +1,96 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}++module MuFeldspar.Vector where++++import qualified Prelude++import Language.Syntactic+import Language.Syntactic.Constructs.Binding.HigherOrder++import MuFeldspar.Prelude+import MuFeldspar.Core+import MuFeldspar.Frontend++++data Vector a+  where+    Indexed :: {length :: Data Length, index :: Data Index -> a } -> Vector a++instance Syntax a => Syntactic (Vector a) FeldDomainAll+  where+    type Internal (Vector a) = [Internal a]+    desugar = desugar . freezeVector . map resugar+    sugar   = map resugar . unfreezeVector . sugar++instance Functor Vector+  where+    fmap = map++++indexed :: Data Length -> (Data Index -> a) -> Vector a+indexed = Indexed++freezeVector :: Type a => Vector (Data a) -> Data [a]+freezeVector vec = parallel (length vec) (index vec)++unfreezeVector :: Type a => Data [a] -> Vector (Data a)+unfreezeVector arr = Indexed (getLength arr) (getIx arr)++take :: Data Length -> Vector a -> Vector a+take n (Indexed l ixf) = indexed (min n l) ixf++drop :: Data Length -> Vector a -> Vector a+drop n (Indexed l ixf) = indexed (max (l-n) 0) (ixf . (+n))++splitAt :: Data Index -> Vector a -> (Vector a, Vector a)+splitAt n vec = (take n vec, drop n vec)++zip :: Vector a -> Vector b -> Vector (a,b)+zip a b = indexed (length a `min` length b) (\i -> (index a i, index b i))++unzip :: Vector (a,b) -> (Vector a, Vector b)+unzip ab = (indexed len (fst . index ab), indexed len (snd . index ab))+  where+    len = length ab++permute :: (Data Length -> Data Index -> Data Index) -> (Vector a -> Vector a)+permute perm vec = indexed len (index vec . perm len)+  where+    len = length vec++reverse :: Vector a -> Vector a+reverse = permute $ \len i -> len-i-1++(...) :: (Type a, Integral a) => Data a -> Data a -> Vector (Data a)+l ... h = indexed (i2n $ h-l+1) ((+l) . i2n)++replicate :: Data Index -> a -> Vector a+replicate len a = indexed len (const a)++(++) :: Syntax a => Vector a -> Vector a -> Vector a+vec1 ++ vec2 = indexed len ixf+  where+    len = length vec1 + length vec2+    ixf i = i < length vec1 ? (index vec1 i, index vec2 (i-length vec1))++map :: (a -> b) -> Vector a -> Vector b+map f (Indexed len ixf) = indexed len (f . ixf)++zipWith :: (a -> b -> c) -> Vector a -> Vector b -> Vector c+zipWith f a b = map (uncurry f) $ zip a b++fold :: Syntax a => (a -> b -> a) -> a -> Vector b -> a+fold f a (Indexed len ixf) = forLoop len a (\i st -> f st (ixf i))++sum :: (Type a, Num a) => Vector (Data a) -> Data a+sum = fold (+) 0+

@@ -12,27 +12,26 @@ -- syntactic. -- -- A more realistic implementation would use custom contexts to restrict the--- types at which constructors operate. Currently, all general features (such as--- 'Literal' and 'Tuple') use a 'SimpleCtx' context, which means that the types--- are quite unrestricted. A real implementation would also probably use custom--- types for primitive functions, since the 'Sym' feature is quite unsafe (uses--- only a 'String' to distinguish between functions).+-- types at which constructors operate. Currently, all general constructs (such+-- as 'Literal' and 'Tuple') use a 'SimpleCtx' context, which means that the+-- types are quite unrestricted. A real implementation would also probably use+-- custom types for primitive functions, since the 'Sym' construct is quite+-- unsafe (uses only a 'String' to distinguish between functions).  module NanoFeldspar.Core where   -import Prelude hiding (max, min)-import qualified Prelude import Data.Typeable  import Language.Syntactic-import Language.Syntactic.Features.Symbol-import Language.Syntactic.Features.Literal-import Language.Syntactic.Features.Condition-import Language.Syntactic.Features.Tuple-import Language.Syntactic.Features.Binding-import Language.Syntactic.Features.Binding.HigherOrder+import Language.Syntactic.Constructs.Symbol+import Language.Syntactic.Constructs.Literal+import Language.Syntactic.Constructs.Condition+import Language.Syntactic.Constructs.Tuple+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder+import Language.Syntactic.Sharing.SimpleCodeMotion   @@ -61,16 +60,26 @@   where     witnessCons Parallel = ConsWit +instance WitnessSat Parallel+  where+    type SatContext Parallel = SimpleCtx+    witnessSat Parallel = SatWit++instance MaybeWitnessSat SimpleCtx Parallel+  where+    maybeWitnessSat = maybeWitnessSatDefault+ instance IsSymbol Parallel   where     toSym Parallel = Sym "parallel" parallel       where         parallel len ixf = map ixf [0 .. len-1] -instance ExprEq Parallel where exprEq = exprEqSym; exprHash = exprHashSym-instance Render Parallel where renderPart = renderPartSym-instance Eval   Parallel where evaluate   = evaluateSym-instance ToTree Parallel+instance ExprEq   Parallel where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   Parallel where renderPart = renderPartSym+instance Eval     Parallel where evaluate   = evaluateSym+instance ToTree   Parallel+instance EvalBind Parallel where evalBindSym = evalBindSymDefault   @@ -87,16 +96,26 @@   where     witnessCons ForLoop = ConsWit +instance WitnessSat ForLoop+  where+    type SatContext ForLoop = SimpleCtx+    witnessSat ForLoop = SatWit++instance MaybeWitnessSat SimpleCtx ForLoop+  where+    maybeWitnessSat = maybeWitnessSatDefault+ instance IsSymbol ForLoop   where     toSym ForLoop = Sym "forLoop" forLoop       where         forLoop len init body = foldl (flip body) init [0 .. len-1] -instance ExprEq ForLoop where exprEq = exprEqSym; exprHash = exprHashSym-instance Render ForLoop where renderPart = renderPartSym-instance Eval   ForLoop where evaluate   = evaluateSym-instance ToTree ForLoop+instance ExprEq   ForLoop where exprEq = exprEqSym; exprHash = exprHashSym+instance Render   ForLoop where renderPart = renderPartSym+instance Eval     ForLoop where evaluate   = evaluateSym+instance ToTree   ForLoop+instance EvalBind ForLoop where evalBindSym = evalBindSymDefault   @@ -106,8 +125,8 @@  -- | The Feldspar domain type FeldDomain-    =   Literal SimpleCtx-    :+: Sym SimpleCtx+    =   Sym SimpleCtx+    :+: Literal SimpleCtx     :+: Condition SimpleCtx     :+: Tuple SimpleCtx     :+: Select SimpleCtx@@ -115,10 +134,9 @@     :+: Parallel     :+: ForLoop -data Data a = Type a => Data { unData :: HOAST SimpleCtx FeldDomain (Full a) }+type FeldDomainAll = HODomain SimpleCtx FeldDomain -type FeldDomainAll =-    HOLambda SimpleCtx FeldDomain :+: Variable SimpleCtx :+: FeldDomain+newtype Data a = Data { unData :: ASTF FeldDomainAll a }  -- | Declaring 'Data' as syntactic sugar instance Type a => Syntactic (Data a) FeldDomainAll@@ -128,19 +146,8 @@     sugar   = Data  -- | Specialization of the 'Syntactic' class for the Feldspar domain-class-    ( Syntactic a FeldDomainAll-    , Type (Internal a)-    , SyntacticN a (ASTF FeldDomainAll (Internal a))-    ) =>-      Syntax a--instance-    ( Syntactic a FeldDomainAll-    , Type (Internal a)-    , SyntacticN a (ASTF FeldDomainAll (Internal a))-    ) =>-      Syntax a+class    (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a+instance (Syntactic a FeldDomainAll, Type (Internal a)) => Syntax a   @@ -149,16 +156,16 @@ --------------------------------------------------------------------------------  -- | Print the expression-printFeld :: Reifiable SimpleCtx a FeldDomain internal => a -> IO ()-printFeld = printExpr . reifyCtx simpleCtx+printFeld :: Syntactic a FeldDomainAll => a -> IO ()+printFeld = printExpr . reifySmart simpleCtx  -- | Draw the syntax tree-drawFeld :: Reifiable SimpleCtx a FeldDomain internal => a -> IO ()-drawFeld = drawAST . reifyCtx simpleCtx+drawFeld :: Syntactic a FeldDomainAll => a -> IO ()+drawFeld = drawAST . reifySmart simpleCtx  -- | Evaluation-eval :: Reifiable SimpleCtx a FeldDomain internal => a -> NAryEval internal-eval = evalLambda . reifyCtx simpleCtx+eval :: Syntactic a FeldDomainAll => a -> Internal a+eval = evalBind . reifySmart simpleCtx   @@ -168,8 +175,14 @@  -- | Literal value :: Syntax a => Internal a -> a-value = sugar . litCtx simpleCtx+value = sugarSymCtx simpleCtx . Literal +false :: Data Bool+false = value False++true :: Data Bool+true = value True+ -- | For types containing some kind of \"thunk\", this function can be used to -- force computation force :: Syntax a => a -> a@@ -177,53 +190,43 @@  -- | Share a value using let binding share :: (Syntax a, Syntax b) => a -> (a -> b) -> b-share a f = sugar $ letBindCtx simpleCtx (desugar a) (desugarN f)+share = sugarSym (letBind simpleCtx)  -- | Alpha equivalence-instance Eq (Data a)+instance Type a => Eq (Data a)   where     Data a == Data b =-        alphaEq simpleCtx (reifyCtx simpleCtx a) (reifyCtx simpleCtx b)+        alphaEq simpleCtx (reify simpleCtx a) (reify simpleCtx b) -instance Show (Data a)+instance Type a => Show (Data a)   where-    show (Data a) = render $ reifyCtx simpleCtx a+    show (Data a) = render $ reify simpleCtx a  instance (Type a, Num a) => Num (Data a)   where     fromInteger = value . fromInteger-    abs         = sugarN $ sym1 simpleCtx "abs" abs-    signum      = sugarN $ sym1 simpleCtx "signum" signum-    (+)         = sugarN $ sym2 simpleCtx "(+)" (+)-    (-)         = sugarN $ sym2 simpleCtx "(-)" (-)-    (*)         = sugarN $ sym2 simpleCtx "(*)" (*)+    abs         = sugarSymCtx simpleCtx $ Sym "abs" abs+    signum      = sugarSymCtx simpleCtx $ Sym "signum" signum+    (+)         = sugarSymCtx simpleCtx $ Sym "(+)" (+)+    (-)         = sugarSymCtx simpleCtx $ Sym "(-)" (-)+    (*)         = sugarSymCtx simpleCtx $ Sym "(*)" (*)  (?) :: Syntax a => Data Bool -> (a,a) -> a-cond ? (t,e) = sugar $-    conditionCtx simpleCtx (desugar cond) (desugar t) (desugar e)+cond ? (t,e) = sugarSymCtx simpleCtx Condition cond t e  -- | Parallel array parallel :: Type a => Data Length -> (Data Index -> Data a) -> Data [a]-parallel len ixf-    =   sugar-    $   inject Parallel-    :$: desugar len-    :$: lambda (desugarN ixf)+parallel = sugarSym Parallel  forLoop :: Syntax st => Data Length -> st -> (Data Index -> st -> st) -> st-forLoop len init body-    =   sugar-    $   inject ForLoop-    :$: desugar len-    :$: desugar init-    :$: lambdaN (desugarN body)+forLoop = sugarSym ForLoop  arrLength :: Type a => Data [a] -> Data Length-arrLength = sugarN $ sym1 simpleCtx "arrLength" Prelude.length+arrLength = sugarSymCtx simpleCtx $ Sym "arrLength" Prelude.length  -- | Array indexing getIx :: Type a => Data [a] -> Data Index -> Data a-getIx = sugarN $ sym2 simpleCtx "getIx" eval+getIx = sugarSymCtx simpleCtx $ Sym "getIx" eval   where     eval as i         | i >= len || i < 0 = error "getIx: index out of bounds"@@ -231,9 +234,15 @@       where         len = Prelude.length as +not :: Data Bool -> Data Bool+not = sugarSymCtx simpleCtx $ Sym "not" Prelude.not++(==) :: Type a => Data a -> Data a -> Data Bool+(==) = sugarSymCtx simpleCtx $ Sym "(==)" (Prelude.==)+ max :: Type a => Data a -> Data a -> Data a-max = sugarN $ sym2 simpleCtx "max" Prelude.max+max = sugarSymCtx simpleCtx $ Sym "max" Prelude.max  min :: Type a => Data a -> Data a -> Data a-min = sugarN $ sym2 simpleCtx "min" Prelude.min+min = sugarSymCtx simpleCtx $ Sym "min" Prelude.min 

@@ -12,11 +12,11 @@   import Language.Syntactic-import Language.Syntactic.Features.Symbol-import Language.Syntactic.Features.Literal-import Language.Syntactic.Features.Binding-import Language.Syntactic.Features.Binding.HigherOrder-import Language.Syntactic.Features.Binding.PartialEval+import Language.Syntactic.Constructs.Symbol+import Language.Syntactic.Constructs.Literal+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder+import Language.Syntactic.Constructs.Binding.Optimize import Language.Syntactic.Sharing.Graph import Language.Syntactic.Sharing.ReifyHO @@ -24,24 +24,21 @@   --- | A predicate deciding which constructs can be shared. Variables and literals--- are not shared.-mkSimpleWit :: (Sym SimpleCtx :<: dom, Parallel :<: dom, ForLoop :<: dom) =>-    ASTF dom a -> Maybe (Witness' SimpleCtx a)-mkSimpleWit ((project -> Just Parallel) :$: _ :$: _)      = Just Witness'-mkSimpleWit ((project -> Just ForLoop) :$: _ :$: _ :$: _) = Just Witness'-mkSimpleWit expr = witnessSatSym simpleCtx expr--- -------------------------------------------------------------------------------- -- * Graph reification -------------------------------------------------------------------------------- +-- | A predicate deciding which constructs can be shared. Literals and variables+-- are not shared.+canShare :: ASTF FeldDomainAll a -> Maybe (SatWit SimpleCtx a)+canShare (prjCtx simpleCtx -> Just (Literal _))  = Nothing+canShare (prjCtx simpleCtx -> Just (Variable _)) = Nothing+canShare a = maybeWitnessSat simpleCtx a+ -- | Draw the syntax graph after common sub-expression elimination-drawFeldCSE :: Reifiable SimpleCtx a FeldDomain internal => a -> IO ()+drawFeldCSE :: Syntactic a FeldDomainAll => a -> IO () drawFeldCSE a = do-    (g,_) <- reifyGraph mkSimpleWit a+    (g,_) <- reifyGraph canShare a     drawASG       $ reindexNodesFrom0       $ inlineSingle@@ -49,39 +46,38 @@       $ g  -- | Draw the syntax graph after observing sharing-drawFeldObs :: Reifiable SimpleCtx a FeldDomain internal => a -> IO ()+drawFeldObs :: Syntactic a FeldDomainAll => a -> IO () drawFeldObs a = do-    (g,_) <- reifyGraph mkSimpleWit a+    (g,_) <- reifyGraph canShare a     drawASG       $ reindexNodesFrom0       $ inlineSingle       $ g ++ -------------------------------------------------------------------------------- -- * Partial evaluation -------------------------------------------------------------------------------- -instance (ForLoop :<: dom, PartialEval dom ctx dom) =>-    PartialEval ForLoop ctx dom+instance (ForLoop :<: dom, Optimize dom ctx dom) =>+    Optimize ForLoop ctx dom   where-    partEvalFeat = partEvalFeatDefault+    optimizeSym = optimizeSymDefault -instance (Parallel :<: dom, PartialEval dom ctx dom) =>-    PartialEval Parallel ctx dom+instance (Parallel :<: dom, Optimize dom ctx dom) =>+    Optimize Parallel ctx dom   where-    partEvalFeat = partEvalFeatDefault--+    optimizeSym = optimizeSymDefault  constFold :: forall a     .  ASTF (Lambda SimpleCtx :+: Variable SimpleCtx :+: FeldDomain) a     -> a     -> ASTF (Lambda SimpleCtx :+: Variable SimpleCtx :+: FeldDomain) a-constFold expr a = case mkSimpleWit expr of-    Just Witness' -> case witness :: Witness SimpleCtx a of-        SimpleWit -> litCtx simpleCtx a+constFold expr a = case fmap fromSatWit (maybeWitnessSat simpleCtx expr) of+    Just SimpleWit -> appSymCtx simpleCtx $ Literal a     _ -> expr -drawFeldPart :: Reifiable SimpleCtx a FeldDomain internal => a -> IO ()-drawFeldPart = drawAST . partialEval simpleCtx constFold . reifyCtx simpleCtx+drawFeldPart :: Syntactic a FeldDomainAll => a -> IO ()+drawFeldPart = drawAST . optimize simpleCtx constFold . reify simpleCtx 

@@ -1,6 +1,6 @@-import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip, zipWith)+import Prelude hiding (length, map, (==), max, min, reverse, sum, unzip, zip, zipWith) -import Language.Syntactic.Features.TupleSyntacticSimple+import Language.Syntactic.Constructs.TupleSyntacticSimple  import NanoFeldspar.Core import NanoFeldspar.Extra@@ -16,7 +16,7 @@ test1_3 = eval prog1 0 10  prog2 :: Data Int -> Data Int-prog2 a = share (min a a) $ \b -> max b b+prog2 a = let b = min a a in max b b  test2_1 = drawFeld prog2 test2_2 = printFeld prog2@@ -63,7 +63,7 @@     as = map (*2) $ force (1...20)  test7_1 = drawFeld prog7-  -- Draws a tree with a lot of duplication+  -- Draws a tree with no duplication  test7_2 = drawFeldCSE prog7   -- Draws a graph with no duplication@@ -74,6 +74,20 @@   -- 'parallel' introduced by 'force' is shared, because 'force' only appears   -- once. --- Note that we're still missing a way to rebuild an expression with let--- bindings from the graph. This is ongoing work.+++--------------------------------------------------------------------------------+-- Demonstration of partial evaluation+--------------------------------------------------------------------------------++prog8 :: Data Int -> Data Int+prog8 a = (a==10) ? (max 5 (6+7), max 5 (6+7))++test8 = drawFeldPart prog8++prog9 a = expensiveCond ? (parallel a (+a), parallel a (+a))+  where+    expensiveCond = getIx (parallel (a*a*a*a) (+a)) 10 == 23++test9 = drawFeldPart prog9 

@@ -19,7 +19,7 @@   -import Prelude hiding (length, map, max, min, reverse, sum, unzip, zip, zipWith)+import Prelude hiding (length, map, (==), max, min, reverse, sum, unzip, zip, zipWith)  import Language.Syntactic 

@@ -8,7 +8,7 @@     , module Language.Syntactic.Interpretation.Equality     , module Language.Syntactic.Interpretation.Render     , module Language.Syntactic.Interpretation.Evaluation-    , module Language.Syntactic.Features.Annotate+    , module Language.Syntactic.Constructs.Annotate     ) where  @@ -17,5 +17,5 @@ import Language.Syntactic.Interpretation.Equality import Language.Syntactic.Interpretation.Render import Language.Syntactic.Interpretation.Evaluation-import Language.Syntactic.Features.Annotate+import Language.Syntactic.Constructs.Annotate 

@@ -0,0 +1,123 @@+-- | Annotations for syntax trees++module Language.Syntactic.Constructs.Annotate where++++import Data.Tree++import Language.Syntactic.Syntax+import Language.Syntactic.Interpretation.Equality+import Language.Syntactic.Interpretation.Render+import Language.Syntactic.Interpretation.Evaluation++++-- | Annotating an expression with arbitrary information.+--+-- This can be used to annotate every node of a syntax tree, which is done by+-- changing+--+-- > AST dom a+--+-- to+--+-- > AST (Ann info dom) a+--+-- Injection/projection of an annotated tree is done using+-- 'injectAnn' / 'projectAnn'.+data Ann info expr a+  where+    Ann+        :: { annInfo :: info (EvalResult a)+           , annExpr :: expr a+           }+        -> Ann info expr a++type AnnSTF info dom a = ASTF (Ann info dom) a++++instance WitnessCons dom => WitnessCons (Ann info dom)+  where+    witnessCons (Ann _ a) = witnessCons a++instance WitnessSat expr => WitnessSat (Ann info expr)+  where+    type SatContext (Ann info expr) = SatContext expr+    witnessSat (Ann _ a) = witnessSat a++instance MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (Ann info dom)+  where+    maybeWitnessSat ctx (Ann _ a) = maybeWitnessSat ctx a++instance ExprEq expr => ExprEq (Ann info expr)+  where+    exprEq a b = annExpr a `exprEq` annExpr b+    exprHash   = exprHash . annExpr++instance Render expr => Render (Ann info expr)+  where+    render = render . annExpr++instance ToTree expr => ToTree (Ann info expr)+  where+    toTreePart args = toTreePart args . annExpr++instance Eval expr => Eval (Ann info expr)+  where+    evaluate = evaluate . annExpr++++injectAnn :: (sub :<: sup, ConsType a) =>+    info (EvalResult a) -> sub a -> AST (Ann info sup) a+injectAnn info = Symbol . Ann info . inject++projectAnn :: (sub :<: sup) =>+    AST (Ann info sup) a -> Maybe (info (EvalResult a), sub a)+projectAnn a = do+    Symbol (Ann info b) <- return a+    c                   <- project b+    return (info, c)++-- | Get the annotation of the top-level node+getInfo :: AST (Ann info dom) a -> info (EvalResult a)+getInfo (Symbol (Ann info _)) = info+getInfo (f :$: _)             = getInfo f++-- | Lift a function that operates on expressions with associated information to+-- operate on an 'Ann' expression. This function is convenient to use together+-- with e.g. 'queryNodeSimple' when the domain has the form @(`Ann` info dom)@.+liftAnn :: (expr a -> info (EvalResult a) -> b) -> (Ann info expr a -> b)+liftAnn f (Ann info a) = f a info++-- | Collect the annotations of all nodes+collectInfo :: (forall a . info a -> b) -> AST (Ann info dom) a -> [b]+collectInfo coll (Symbol (Ann info _)) = [coll info]+collectInfo coll (f :$: a) = collectInfo coll f ++ collectInfo coll a++-- | Rendering of annotated syntax trees+toTreeAnn :: forall info dom a . (Render info, ToTree dom) =>+    ASTF (Ann info dom) a -> Tree String+toTreeAnn a = mkTree [] a+  where+    mkTree :: [Tree String] -> AST (Ann info dom) b -> Tree String+    mkTree args (Symbol (Ann info expr)) = Node infoStr [toTreePart args expr]+      where+        infoStr = "<<" ++ render info ++ ">>"+    mkTree args (f :$: a) = mkTree (mkTree [] a : args) f++-- | Show an annotated syntax tree using ASCII art+showAnn :: (Render info, ToTree dom) => ASTF (Ann info dom) a -> String+showAnn = drawTree . toTreeAnn++-- | Print an annotated syntax tree using ASCII art+drawAnn :: (Render info, ToTree dom) => ASTF (Ann info dom) a -> IO ()+drawAnn = putStrLn . showAnn++-- | Strip annotations from an 'AST'+stripAnn :: AST (Ann info dom) a -> AST dom a+stripAnn (Symbol (Ann _ a)) = Symbol a+stripAnn (f :$: a)          = stripAnn f :$: stripAnn a+

@@ -0,0 +1,296 @@+{-# LANGUAGE OverlappingInstances #-}++-- | General binding constructs++module Language.Syntactic.Constructs.Binding where++++import Control.Monad.Identity+import Control.Monad.Reader+import Data.Dynamic+import Data.Ix+import Data.Tree++import Data.Hash+import Data.Proxy++import Language.Syntactic+import Language.Syntactic.Constructs.Symbol+import Language.Syntactic.Constructs.Literal+import Language.Syntactic.Constructs.Condition+import Language.Syntactic.Constructs.Tuple+import Language.Syntactic.Constructs.Monad++++--------------------------------------------------------------------------------+-- * Variables+--------------------------------------------------------------------------------++-- | Variable identifier+newtype VarId = VarId { varInteger :: Integer }+  deriving (Eq, Ord, Num, Real, Integral, Enum, Ix)++instance Show VarId+  where+    show (VarId i) = show i++showVar :: VarId -> String+showVar v = "var" ++ show v++++-- | Variables+data Variable ctx a+  where+    Variable :: (Typeable a, Sat ctx a) => VarId -> Variable ctx (Full a)+      -- 'Typeable' needed by the dynamic types in 'evalBind'.++instance WitnessCons (Variable ctx)+  where+    witnessCons (Variable _) = ConsWit++instance WitnessSat (Variable ctx)+  where+    type SatContext (Variable ctx) = ctx+    witnessSat (Variable _) = SatWit++instance MaybeWitnessSat ctx (Variable ctx)+  where+    maybeWitnessSat = maybeWitnessSatDefault++instance MaybeWitnessSat ctx1 (Variable ctx2)+  where+    maybeWitnessSat _ _ = Nothing++-- | 'exprEq' does strict identifier comparison; i.e. no alpha equivalence.+--+-- 'exprHash' assigns the same hash to all variables. This is a valid+-- over-approximation that enables the following property:+--+-- @`alphaEq` a b  ==>  `exprHash` a == `exprHash` b@+instance ExprEq (Variable ctx)+  where+    exprEq (Variable v1) (Variable v2) = v1==v2+    exprHash (Variable _)              = hashInt 0++instance Render (Variable ctx)+  where+    render (Variable v) = showVar v++instance ToTree (Variable ctx)+  where+    toTreePart [] (Variable v) = Node ("var:" ++ show v) []++++--------------------------------------------------------------------------------+-- * Lambda binding+--------------------------------------------------------------------------------++-- | Lambda binding+data Lambda ctx a+  where+    Lambda :: (Typeable a, Sat ctx a) =>+        VarId -> Lambda ctx (b :-> Full (a -> b))+      -- 'Typeable' needed by the dynamic types in 'evalBind'.++instance WitnessCons (Lambda ctx)+  where+    witnessCons (Lambda _) = ConsWit++instance MaybeWitnessSat ctx1 (Lambda ctx2)+  where+    maybeWitnessSat _ _ = Nothing++-- | 'exprEq' does strict identifier comparison; i.e. no alpha equivalence.+--+-- 'exprHash' assigns the same hash to all 'Lambda' bindings. This is a valid+-- over-approximation that enables the following property:+--+-- @`alphaEq` a b  ==>  `exprHash` a == `exprHash` b@+instance ExprEq (Lambda ctx)+  where+    exprEq (Lambda v1) (Lambda v2) = v1==v2+    exprHash (Lambda _)            = hashInt 0++instance Render (Lambda ctx)+  where+    renderPart [body] (Lambda v) = "(\\" ++ showVar v ++ " -> "  ++ body ++ ")"++instance ToTree (Lambda ctx)+  where+    toTreePart [body] (Lambda v) = Node ("Lambda " ++ show v) [body]++++--------------------------------------------------------------------------------+-- * Let binding+--------------------------------------------------------------------------------++-- | Let binding+--+-- A 'Let' expression is really just an application of a lambda binding (the+-- argument @(a -> b)@ is preferably constructed by 'Lambda').+data Let ctxa ctxb a+  where+    Let :: (Sat ctxa a, Sat ctxb b) => Let ctxa ctxb (a :-> (a -> b) :-> Full b)++instance WitnessCons (Let ctxa ctxb)+  where+    witnessCons Let = ConsWit++instance WitnessSat (Let ctxa ctxb)+  where+    type SatContext (Let ctxa ctxb) = ctxb+    witnessSat Let = SatWit++instance MaybeWitnessSat ctxb (Let ctxa ctxb)+  where+    maybeWitnessSat = maybeWitnessSatDefault++instance MaybeWitnessSat ctx (Let ctxa ctxb)+  where+    maybeWitnessSat _ _ = Nothing++instance ExprEq (Let ctxa ctxb)+  where+    exprEq Let Let = True++    exprHash Let = hashInt 0++instance Render (Let ctxa ctxb)+  where+    renderPart []    Let = "Let"+    renderPart [f,a] Let = "(" ++ unwords ["letBind",f,a] ++ ")"++instance ToTree (Let ctxa ctxb)+  where+    toTreePart [a,body] Let = case splitAt 7 node of+        ("Lambda ", var) -> Node ("Let " ++ var) [a,body']+        _                -> Node "Let" [a,body]+      where+        Node node [body'] = body+        var               = drop 7 node  -- Drop the "Lambda " prefix++instance Eval (Let ctxa ctxb)+  where+    evaluate Let = fromEval (flip ($))++-- | Let binding with explicit context+letBind :: (Sat ctx a, Sat ctx b) =>+    Proxy ctx -> Let ctx ctx (a :-> (a -> b) :-> Full b)+letBind _ = Let++-- | Partial `Let` projection with explicit context+prjLet :: (Let ctxa ctxb :<: sup) =>+    Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a)+prjLet _ _ = project++++--------------------------------------------------------------------------------+-- * Interpretation+--------------------------------------------------------------------------------++-- | Alpha equivalence in an environment of variable equivalences. The supplied+-- equivalence function gets called when the argument expressions are not both+-- 'Variable's, both 'Lambda's or both ':$:'.+alphaEqM :: (Lambda ctx :<: dom, Variable ctx :<: dom)+    => Proxy ctx+    -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool)+    -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool)++-- TODO This function is not ideal, since the type says nothing about which+--      cases have been handled when calling 'eq'.++alphaEqM ctx eq+    ((prjCtx ctx -> Just (Lambda v1)) :$: a1)+    ((prjCtx ctx -> Just (Lambda v2)) :$: a2) =+        local ((v1,v2):) $ alphaEqM ctx eq a1 a2++alphaEqM ctx eq+    (prjCtx ctx -> Just (Variable v1))+    (prjCtx ctx -> Just (Variable v2)) = do+        env <- ask+        case lookup v1 env of+          Nothing  -> return (v1==v2)   -- Free variables+          Just v2' -> return (v2==v2')++alphaEqM ctx eq (f1 :$: a1) (f2 :$: a2) = do+    e <- alphaEqM ctx eq f1 f2+    if e then alphaEqM ctx eq a1 a2 else return False++alphaEqM _ eq a b = eq a b++++-- | Alpha-equivalence on lambda expressions. Free variables are taken to be+-- equivalent if they have the same identifier.+alphaEq :: (Lambda ctx :<: dom, Variable ctx :<: dom, ExprEq dom) =>+    Proxy ctx -> AST dom a -> AST dom b -> Bool+alphaEq ctx a b = runReader (alphaEqM ctx (\a b -> return $ exprEq a b) a b) []++++class EvalBind sub+  where+    evalBindSym+        :: (EvalBind dom, ConsType a)+        => sub a+        -> HList (AST dom) a+        -> Reader [(VarId,Dynamic)] (EvalResult a)++instance (EvalBind sub1, EvalBind sub2) => EvalBind (sub1 :+: sub2)+  where+    evalBindSym (InjectL a) = evalBindSym a+    evalBindSym (InjectR a) = evalBindSym a++-- | Evaluation of possibly open expressions+evalBindM :: EvalBind dom => ASTF dom a -> Reader [(VarId,Dynamic)] a+evalBindM = liftM result . queryNode (\a -> liftM Full . evalBindSym a)++-- | Evaluation of closed expressions+evalBind :: EvalBind dom => ASTF dom a -> a+evalBind = flip runReader [] . evalBindM++-- | Convenient default implementation of 'evalBindSym'+evalBindSymDefault :: (Eval sub, ConsType a, EvalBind dom)+    => sub a+    -> HList (AST dom) a+    -> Reader [(VarId,Dynamic)] (EvalResult a)+evalBindSymDefault sym args = do+    args' <- mapHListM (liftM (Identity . Full) . evalBindM) args+    return $ appEvalHList (toEval $ evaluate sym) args'++instance EvalBind (Sym ctx)            where evalBindSym = evalBindSymDefault+instance EvalBind (Literal ctx)        where evalBindSym = evalBindSymDefault+instance EvalBind (Condition ctx)      where evalBindSym = evalBindSymDefault+instance EvalBind (Tuple ctx)          where evalBindSym = evalBindSymDefault+instance EvalBind (Select ctx)         where evalBindSym = evalBindSymDefault+instance EvalBind (Let ctxa ctxb)      where evalBindSym = evalBindSymDefault+instance Monad m => EvalBind (MONAD m) where evalBindSym = evalBindSymDefault++instance EvalBind dom => EvalBind (Ann info dom)+  where+    evalBindSym (Ann _ a) args = evalBindSym a args++instance EvalBind (Lambda ctx)+  where+    evalBindSym (Lambda v) (body :*: Nil) = do+        env <- ask+        return+            $ \a -> flip runReader ((v,toDyn a):env)+            $ evalBindM body++instance EvalBind (Variable ctx)+  where+    evalBindSym (Variable v) Nil = do+        env <- ask+        case lookup v env of+            Nothing -> return $ error "evalBind: evaluating free variable"+            Just a  -> case fromDynamic a of+              Just a -> return a+              _      -> return $ error "evalBind: internal type error"+

@@ -0,0 +1,96 @@+{-# LANGUAGE UndecidableInstances #-}++-- | This module provides binding constructs using higher-order syntax and a+-- function for translating to first-order syntax. Expressions constructed using+-- the exported interface are guaranteed to have a well-behaved translation.++module Language.Syntactic.Constructs.Binding.HigherOrder+    ( Variable+    , Let (..)+    , HOLambda (..)+    , HODomain+    , lambda+    , reifyM+    , reifyTop+    , reify+    ) where++++import Control.Monad.State+import Data.Typeable++import Data.Proxy++import Language.Syntactic+import Language.Syntactic.Constructs.Binding++++-- | Higher-order lambda binding+data HOLambda ctx dom a+  where+    HOLambda :: (Typeable a, Typeable b, Sat ctx a)+        => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b)+        -> HOLambda ctx dom (Full (a -> b))++type HODomain ctx dom = HOLambda ctx dom :+: Variable ctx :+: dom++instance WitnessCons (HOLambda ctx dom)+  where+    witnessCons (HOLambda _) = ConsWit++instance MaybeWitnessSat ctx1 (HOLambda ctx2 dom)+  where+    maybeWitnessSat _ _ = Nothing++++-- | Lambda binding+lambda :: (Typeable a, Typeable b, Sat ctx a)+    => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b)+    -> ASTF (HODomain ctx dom) (a -> b)+lambda = inject . HOLambda++instance+    ( Syntactic a (HODomain ctx dom)+    , Syntactic b (HODomain ctx dom)+    , Sat ctx (Internal a)+    ) =>+      Syntactic (a -> b) (HODomain ctx dom)+  where+    type Internal (a -> b) = Internal a -> Internal b+    desugar f = lambda (desugar . f . sugar)+    sugar     = error "sugar not implemented for (a -> b)"+      -- TODO An implementation of sugar would require dom to have some kind of+      --      application. Perhaps use Let for this?++++reifyM :: forall ctx dom a . Typeable a+    => AST (HODomain ctx dom) a+    -> State VarId (AST (Lambda ctx :+: Variable ctx :+: dom) a)+reifyM (f :$: a)            = liftM2 (:$:) (reifyM f) (reifyM a)+reifyM (Symbol (InjectR a)) = return $ Symbol $ InjectR a+reifyM (Symbol (InjectL (HOLambda f))) = do+    v    <- get; put (v+1)+    body <- reifyM $ f $ inject $ (Variable v `withContext` ctx)+    return $ inject (Lambda v `withContext` ctx) :$: body+  where+    ctx = Proxy :: Proxy ctx++-- | Translating expressions with higher-order binding to corresponding+-- expressions using first-order binding+reifyTop :: Typeable a =>+    AST (HODomain ctx dom) a -> AST (Lambda ctx :+: Variable ctx :+: dom) a+reifyTop = flip evalState 0 . reifyM+  -- It is assumed that there are no 'Variable' constructors (i.e. no free+  -- variables) in the argument. This is guaranteed by the exported interface.++-- | Reifying an n-ary syntactic function+reify :: Syntactic a (HODomain ctx dom)+    => Proxy ctx+    -> a+    -> ASTF (Lambda ctx :+: Variable ctx :+: dom) (Internal a)+reify _ = reifyTop . desugar+

@@ -0,0 +1,134 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Basic optimization of expressions+module Language.Syntactic.Constructs.Binding.Optimize where++++import Control.Monad.Writer+import Data.Set as Set++import Data.Proxy++import Language.Syntactic+import Language.Syntactic.Constructs.Symbol+import Language.Syntactic.Constructs.Literal+import Language.Syntactic.Constructs.Condition+import Language.Syntactic.Constructs.Tuple+import Language.Syntactic.Constructs.Binding++++-- | Constant folder+--+-- Given an expression and the statically known value of that expression,+-- returns a (possibly) new expression with the same meaning as the original.+-- Typically, the result will be a 'Literal', if the relevant type constraints+-- are satisfied.+type ConstFolder dom = forall a . ASTF dom a -> a -> ASTF dom a++-- | Basic optimization of a sub-domain+class EvalBind dom => Optimize sub ctx dom+  where+    -- | Bottom-up optimization of a sub-domain. The optimization performed is+    -- up to each instance, but the intention is to provide a sensible set of+    -- \"always-appropriate\" optimizations. The default implementation+    -- 'optimizeSymDefault' does only constant folding. This constant folding+    -- uses the set of free variables to know when it's static evaluation is+    -- possible. Thus it is possible to help constant folding of other+    -- constructs by pruning away parts of the syntax tree that are known not to+    -- be needed. For example, by replacing (using ordinary Haskell as an+    -- example)+    --+    -- > if True then a else b+    --+    -- with @a@, we don't need to report the free variables in @b@. This, in+    -- turn, can lead to more constant folding higher up in the syntax tree.+    optimizeSym+        :: Proxy ctx+        -> ConstFolder dom+        -> sub a+        -> HList (AST dom) a+        -> Writer (Set VarId) (ASTF dom (EvalResult a))++  -- The reason for having @dom@ as a class parameter is that many instances+  -- require the constraint @(sub :<: dom)@. If @dom@ was forall-quantified in+  -- 'optimizeSym', this constraint would not be allowed. On the other hand, it+  -- is not possible to add the constraint @(sub :<: dom)@ to 'optimizeSym',+  -- because the instance for '(:+:)' doesn't satisfy it.++instance (Optimize sub1 ctx dom, Optimize sub2 ctx dom) =>+    Optimize (sub1 :+: sub2) ctx dom+  where+    optimizeSym ctx constFold (InjectL a) = optimizeSym ctx constFold a+    optimizeSym ctx constFold (InjectR a) = optimizeSym ctx constFold a++optimizeM :: Optimize dom ctx dom+    => Proxy ctx+    -> ConstFolder dom+    -> ASTF dom a+    -> Writer (Set VarId) (ASTF dom a)+optimizeM ctx constFold = transformNode (optimizeSym ctx constFold)++-- | Optimize an expression+optimize :: Optimize dom ctx dom =>+    Proxy ctx -> ConstFolder dom -> ASTF dom a -> ASTF dom a+optimize ctx constFold = fst . runWriter . optimizeM ctx constFold++-- | Convenient default implementation of 'optimizeSym' (uses 'evalBind' to+-- partially evaluate)+optimizeSymDefault+    :: ( sub :<: dom+       , WitnessCons sub+       , Optimize dom ctx dom+       )+    => Proxy ctx+    -> ConstFolder dom+    -> sub a+    -> HList (AST dom) a+    -> Writer (Set VarId) (ASTF dom (EvalResult a))+optimizeSymDefault ctx constFold sym@(witnessCons -> ConsWit) args = do+    (args',vars) <- listen $ mapHListM (optimizeM ctx constFold) args+    let result = appHList (Symbol $ inject sym) args'+        value  = evalBind result+    if Set.null vars+      then return $ constFold result value+      else return result++instance (Sym ctx'      :<: dom, Optimize dom ctx dom) => Optimize (Sym ctx')      ctx dom where optimizeSym = optimizeSymDefault+instance (Literal ctx'  :<: dom, Optimize dom ctx dom) => Optimize (Literal ctx')  ctx dom where optimizeSym = optimizeSymDefault+instance (Tuple ctx'    :<: dom, Optimize dom ctx dom) => Optimize (Tuple ctx')    ctx dom where optimizeSym = optimizeSymDefault+instance (Select ctx'   :<: dom, Optimize dom ctx dom) => Optimize (Select ctx')   ctx dom where optimizeSym = optimizeSymDefault+instance (Let ctxa ctxb :<: dom, Optimize dom ctx dom) => Optimize (Let ctxa ctxb) ctx dom where optimizeSym = optimizeSymDefault++instance+    ( Condition ctx' :<: dom+    , Lambda ctx :<: dom+    , Variable ctx :<: dom+    , ExprEq dom+    , Optimize dom ctx dom+    ) =>+      Optimize (Condition ctx') ctx dom+  where+    optimizeSym ctx constFold cond@Condition args@(c :*: t :*: e :*: Nil)+        | Set.null cVars  = optimizeM ctx constFold t_or_e+        | alphaEq ctx t e = optimizeM ctx constFold t+        | otherwise       = optimizeSymDefault ctx constFold cond args+      where+        (c',cVars) = runWriter $ optimizeM ctx constFold c+        t_or_e     = if evalBind c' then t else e++instance (Variable ctx :<: dom, Optimize dom ctx dom) =>+    Optimize (Variable ctx) ctx dom+  where+    optimizeSym _ _ var@(Variable v) Nil = do+        tell (singleton v)+        return (inject var)++instance (Lambda ctx :<: dom, Optimize dom ctx dom) =>+    Optimize (Lambda ctx) ctx dom+  where+    optimizeSym ctx constFold lam@(Lambda v) (body :*: Nil) = do+        body' <- censor (delete v) $ optimizeM ctx constFold body+        return $ inject lam :$: body'+

@@ -0,0 +1,47 @@+{-# LANGUAGE OverlappingInstances #-}++-- | Conditional expressions++module Language.Syntactic.Constructs.Condition where++++import Data.Hash+import Data.Proxy+import Data.Typeable++import Language.Syntactic+import Language.Syntactic.Constructs.Symbol++++data Condition ctx a+  where+    Condition :: Sat ctx a => Condition ctx (Bool :-> a :-> a :-> Full a)++instance WitnessCons (Condition ctx)+  where+    witnessCons Condition = ConsWit++instance WitnessSat (Condition ctx)+  where+    type SatContext (Condition ctx) = ctx+    witnessSat Condition = SatWit++instance MaybeWitnessSat ctx (Condition ctx)+  where+    maybeWitnessSat = maybeWitnessSatDefault++instance MaybeWitnessSat ctx1 (Condition ctx2)+  where+    maybeWitnessSat _ _ = Nothing++instance IsSymbol (Condition ctx)+  where+    toSym Condition = Sym "condition" (\c t e -> if c then t else e)++instance ExprEq (Condition ctx) where exprEq = exprEqSym; exprHash = exprHashSym+instance Render (Condition ctx) where renderPart = renderPartSym+instance Eval   (Condition ctx) where evaluate   = evaluateSym+instance ToTree (Condition ctx)+

@@ -0,0 +1,57 @@+{-# LANGUAGE OverlappingInstances #-}++-- | Literal expressions++module Language.Syntactic.Constructs.Literal where++++import Data.Typeable++import Data.Hash+import Data.Proxy++import Language.Syntactic++++data Literal ctx a+  where+    Literal :: (Eq a, Show a, Typeable a, Sat ctx a) =>+        a -> Literal ctx (Full a)++instance WitnessCons (Literal ctx)+  where+    witnessCons (Literal _) = ConsWit++instance WitnessSat (Literal ctx)+  where+    type SatContext (Literal ctx) = ctx+    witnessSat (Literal _) = SatWit++instance MaybeWitnessSat ctx (Literal ctx)+  where+    maybeWitnessSat = maybeWitnessSatDefault++instance MaybeWitnessSat ctx1 (Literal ctx2)+  where+    maybeWitnessSat _ _ = Nothing++instance ExprEq (Literal ctx)+  where+    Literal a `exprEq` Literal b = case cast a of+        Just a' -> a'==b+        Nothing -> False++    exprHash (Literal a) = hash (show a)++instance Render (Literal ctx)+  where+    render (Literal a) = show a++instance ToTree (Literal ctx)++instance Eval (Literal ctx)+  where+    evaluate (Literal a) = fromEval a+

@@ -0,0 +1,49 @@+-- | Monadic constructs++module Language.Syntactic.Constructs.Monad where++++import Control.Monad++import Language.Syntactic+import Language.Syntactic.Constructs.Symbol++import Data.Proxy++++data MONAD m a+  where+    Return :: MONAD m (a    :-> Full (m a))+    Bind   :: MONAD m (m a  :-> (a -> m b) :-> Full (m b))+    Then   :: MONAD m (m a  :-> m b        :-> Full (m b))+    When   :: MONAD m (Bool :-> m ()       :-> Full (m ()))++instance WitnessCons (MONAD m)+  where+    witnessCons Return = ConsWit+    witnessCons Bind   = ConsWit+    witnessCons Then   = ConsWit+    witnessCons When   = ConsWit++instance MaybeWitnessSat ctx (MONAD m)+  where+    maybeWitnessSat _ _ = Nothing++instance Monad m => IsSymbol (MONAD m)+  where+    toSym Return = Sym "return" return+    toSym Bind   = Sym "bind"   (>>=)+    toSym Then   = Sym "then"   (>>)+    toSym When   = Sym "when"   when++instance Monad m => ExprEq (MONAD m) where exprEq = exprEqSym; exprHash = exprHashSym+instance Monad m => Render (MONAD m) where renderPart = renderPartSym+instance Monad m => Eval   (MONAD m) where evaluate   = evaluateSym+instance Monad m => ToTree (MONAD m)++-- | Projection with explicit monad type+prjMonad :: (MONAD m :<: sup) => Proxy (m ()) -> sup a -> Maybe (MONAD m a)+prjMonad _ = project+

@@ -0,0 +1,93 @@+{-# LANGUAGE OverlappingInstances #-}++-- | Generic symbols+--+-- 'Sym' provides a simple way to make syntactic symbols for prototyping.+-- However, note that 'Sym' is quite unsafe as it only uses 'String' to+-- distinguish between different symbols. Also, 'Sym' has a very free type that+-- allows any number of arguments.++module Language.Syntactic.Constructs.Symbol where++++import Data.Typeable++import Data.Hash+import Data.Proxy++import Language.Syntactic++++data Sym ctx a+  where+    Sym :: (ConsType a, Sat ctx (EvalResult a)) =>+        String -> ConsEval a -> Sym ctx a++instance WitnessCons (Sym ctx)+  where+    witnessCons (Sym _ _) = ConsWit++instance WitnessSat (Sym ctx)+  where+    type SatContext (Sym ctx) = ctx+    witnessSat (Sym _ _) = SatWit++instance MaybeWitnessSat ctx (Sym ctx)+  where+    maybeWitnessSat = maybeWitnessSatDefault++instance MaybeWitnessSat ctx1 (Sym ctx2)+  where+    maybeWitnessSat _ _ = Nothing++instance ExprEq (Sym ctx)+  where+    exprEq (Sym a _) (Sym b _) = a==b+    exprHash (Sym name _)      = hash name++instance Render (Sym ctx)+  where+    renderPart [] (Sym name _) = name+    renderPart args (Sym name _)+        | isInfix   = "(" ++ unwords [a,op,b] ++ ")"+        | otherwise = "(" ++ unwords (name : args) ++ ")"+      where+        [a,b] = args+        op    = init $ tail name+        isInfix+          =  not (null name)+          && head name == '('+          && last name == ')'+          && length args == 2++instance ToTree (Sym ctx)++instance Eval (Sym ctx)+  where+    evaluate (Sym _ a) = fromEval a++++-- | Class of expressions that can be treated as symbols+class IsSymbol expr+  where+    toSym :: expr a -> Sym Poly a++-- | Default implementation of 'exprEq'+exprEqSym :: IsSymbol expr => expr a -> expr b -> Bool+exprEqSym a b = exprEq (toSym a) (toSym b)++-- | Default implementation of 'exprHash'+exprHashSym :: IsSymbol expr => expr a -> Hash+exprHashSym = exprHash . toSym++-- | Default implementation of 'renderPart'+renderPartSym :: IsSymbol expr => [String] -> expr a -> String+renderPartSym args = renderPart args . toSym++-- | Default implementation of 'evaluate'+evaluateSym :: IsSymbol expr => expr a -> a+evaluateSym = evaluate . toSym+

@@ -0,0 +1,422 @@+{-# OPTIONS_GHC -fcontext-stack=30 #-}++{-# LANGUAGE OverlappingInstances #-}++-- | Construction and projection of tuples in the object language+--+-- The function pairs @desugarTupX@/@sugarTupX@ could be used directly in+-- 'Syntactic' instances if it wasn't for the extra @(`Proxy` ctx)@ arguments.+-- For this reason, 'Syntactic' instances have to be written manually for each+-- context. The module "Language.Syntactic.Constructs.TupleSyntacticPoly"+-- provides instances for a 'Poly' context. The exact same code can be used to+-- make instances for other contexts -- just copy/paste and replace 'Poly' and+-- 'poly' with the desired context (and probably add an extra constraint in the+-- class contexts).++module Language.Syntactic.Constructs.Tuple where++++import Data.Hash+import Data.Proxy+import Data.Tuple.Curry+import Data.Tuple.Select++import Language.Syntactic+import Language.Syntactic.Constructs.Symbol++++--------------------------------------------------------------------------------+-- * Construction+--------------------------------------------------------------------------------++-- | Expressions for constructing tuples+data Tuple ctx a+  where+    Tup2 :: Sat ctx (a,b)           => Tuple ctx (a :-> b :-> Full (a,b))+    Tup3 :: Sat ctx (a,b,c)         => Tuple ctx (a :-> b :-> c :-> Full (a,b,c))+    Tup4 :: Sat ctx (a,b,c,d)       => Tuple ctx (a :-> b :-> c :-> d :-> Full (a,b,c,d))+    Tup5 :: Sat ctx (a,b,c,d,e)     => Tuple ctx (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e))+    Tup6 :: Sat ctx (a,b,c,d,e,f)   => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f))+    Tup7 :: Sat ctx (a,b,c,d,e,f,g) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g))++instance WitnessCons (Tuple ctx)+  where+    witnessCons Tup2 = ConsWit+    witnessCons Tup3 = ConsWit+    witnessCons Tup4 = ConsWit+    witnessCons Tup5 = ConsWit+    witnessCons Tup6 = ConsWit+    witnessCons Tup7 = ConsWit++instance WitnessSat (Tuple ctx)+  where+    type SatContext (Tuple ctx) = ctx+    witnessSat Tup2 = SatWit+    witnessSat Tup3 = SatWit+    witnessSat Tup4 = SatWit+    witnessSat Tup5 = SatWit+    witnessSat Tup6 = SatWit+    witnessSat Tup7 = SatWit++instance MaybeWitnessSat ctx (Tuple ctx)+  where+    maybeWitnessSat = maybeWitnessSatDefault++instance MaybeWitnessSat ctx1 (Tuple ctx2)+  where+    maybeWitnessSat _ _ = Nothing++instance IsSymbol (Tuple ctx)+  where+    toSym Tup2 = Sym "tup2" (,)+    toSym Tup3 = Sym "tup3" (,,)+    toSym Tup4 = Sym "tup4" (,,,)+    toSym Tup5 = Sym "tup5" (,,,,)+    toSym Tup6 = Sym "tup6" (,,,,,)+    toSym Tup7 = Sym "tup7" (,,,,,,)++instance ExprEq (Tuple ctx) where exprEq = exprEqSym; exprHash = exprHashSym+instance Render (Tuple ctx) where renderPart = renderPartSym+instance Eval   (Tuple ctx) where evaluate   = evaluateSym+instance ToTree (Tuple ctx)++++desugarTup2+    :: ( Syntactic a dom+       , Syntactic b dom+       , Sat ctx (Internal a, Internal b)+       , Tuple ctx :<: dom+       )+    => Proxy ctx+    -> (a,b)+    -> ASTF dom (Internal a, Internal b)+desugarTup2 ctx = uncurryN $ sugarSymCtx ctx Tup2++desugarTup3+    :: ( Syntactic a dom+       , Syntactic b dom+       , Syntactic c dom+       , Sat ctx (Internal a, Internal b, Internal c)+       , Tuple ctx :<: dom+       )+    => Proxy ctx+    -> (a,b,c)+    -> ASTF dom (Internal a, Internal b, Internal c)+desugarTup3 ctx = uncurryN $ sugarSymCtx ctx Tup3++desugarTup4+    :: ( Syntactic a dom+       , Syntactic b dom+       , Syntactic c dom+       , Syntactic d dom+       , Sat ctx (Internal a, Internal b, Internal c, Internal d)+       , Tuple ctx :<: dom+       )+    => Proxy ctx+    -> (a,b,c,d)+    -> ASTF dom (Internal a, Internal b, Internal c, Internal d)+desugarTup4 ctx = uncurryN $ sugarSymCtx ctx Tup4++desugarTup5+    :: ( Syntactic a dom+       , Syntactic b dom+       , Syntactic c dom+       , Syntactic d dom+       , Syntactic e dom+       , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e)+       , Tuple ctx :<: dom+       )+    => Proxy ctx+    -> (a,b,c,d,e)+    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e)+desugarTup5 ctx = uncurryN $ sugarSymCtx ctx Tup5++desugarTup6+    :: ( Syntactic a dom+       , Syntactic b dom+       , Syntactic c dom+       , Syntactic d dom+       , Syntactic e dom+       , Syntactic f dom+       , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)+       , Tuple ctx :<: dom+       )+    => Proxy ctx+    -> (a,b,c,d,e,f)+    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)+desugarTup6 ctx = uncurryN $ sugarSymCtx ctx Tup6++desugarTup7+    :: ( Syntactic a dom+       , Syntactic b dom+       , Syntactic c dom+       , Syntactic d dom+       , Syntactic e dom+       , Syntactic f dom+       , Syntactic g dom+       , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)+       , Tuple ctx :<: dom+       )+    => Proxy ctx+    -> (a,b,c,d,e,f,g)+    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)+desugarTup7 ctx = uncurryN $ sugarSymCtx ctx Tup7++++--------------------------------------------------------------------------------+-- * Projection+--------------------------------------------------------------------------------++-- | These families ('Sel1'' - 'Sel7'') are needed because of the problem+-- described in:+--+-- <http://emil-fp.blogspot.com/2011/08/fundeps-weaker-than-type-families.html>+type family Sel1' a+type instance Sel1' (a,b)           = a+type instance Sel1' (a,b,c)         = a+type instance Sel1' (a,b,c,d)       = a+type instance Sel1' (a,b,c,d,e)     = a+type instance Sel1' (a,b,c,d,e,f)   = a+type instance Sel1' (a,b,c,d,e,f,g) = a++type family Sel2' a+type instance Sel2' (a,b)           = b+type instance Sel2' (a,b,c)         = b+type instance Sel2' (a,b,c,d)       = b+type instance Sel2' (a,b,c,d,e)     = b+type instance Sel2' (a,b,c,d,e,f)   = b+type instance Sel2' (a,b,c,d,e,f,g) = b++type family Sel3' a+type instance Sel3' (a,b,c)         = c+type instance Sel3' (a,b,c,d)       = c+type instance Sel3' (a,b,c,d,e)     = c+type instance Sel3' (a,b,c,d,e,f)   = c+type instance Sel3' (a,b,c,d,e,f,g) = c++type family Sel4' a+type instance Sel4' (a,b,c,d)       = d+type instance Sel4' (a,b,c,d,e)     = d+type instance Sel4' (a,b,c,d,e,f)   = d+type instance Sel4' (a,b,c,d,e,f,g) = d++type family Sel5' a+type instance Sel5' (a,b,c,d,e)     = e+type instance Sel5' (a,b,c,d,e,f)   = e+type instance Sel5' (a,b,c,d,e,f,g) = e++type family Sel6' a+type instance Sel6' (a,b,c,d,e,f)   = f+type instance Sel6' (a,b,c,d,e,f,g) = f++type family Sel7' a+type instance Sel7' (a,b,c,d,e,f,g) = g++-- | Expressions for selecting elements of a tuple+data Select ctx a+  where+    Sel1 :: (Sel1 a b, Sel1' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)+    Sel2 :: (Sel2 a b, Sel2' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)+    Sel3 :: (Sel3 a b, Sel3' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)+    Sel4 :: (Sel4 a b, Sel4' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)+    Sel5 :: (Sel5 a b, Sel5' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)+    Sel6 :: (Sel6 a b, Sel6' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)+    Sel7 :: (Sel7 a b, Sel7' a ~ b, Sat ctx b) => Select ctx (a :-> Full b)++instance WitnessCons (Select ctx)+  where+    witnessCons Sel1 = ConsWit+    witnessCons Sel2 = ConsWit+    witnessCons Sel3 = ConsWit+    witnessCons Sel4 = ConsWit+    witnessCons Sel5 = ConsWit+    witnessCons Sel6 = ConsWit+    witnessCons Sel7 = ConsWit++instance WitnessSat (Select ctx)+  where+    type SatContext (Select ctx) = ctx+    witnessSat Sel1 = SatWit+    witnessSat Sel2 = SatWit+    witnessSat Sel3 = SatWit+    witnessSat Sel4 = SatWit+    witnessSat Sel5 = SatWit+    witnessSat Sel6 = SatWit+    witnessSat Sel7 = SatWit++instance MaybeWitnessSat ctx (Select ctx)+  where+    maybeWitnessSat = maybeWitnessSatDefault++instance MaybeWitnessSat ctx1 (Select ctx2)+  where+    maybeWitnessSat _ _ = Nothing++instance IsSymbol (Select ctx)+  where+    toSym Sel1 = Sym "sel1" sel1+    toSym Sel2 = Sym "sel2" sel2+    toSym Sel3 = Sym "sel3" sel3+    toSym Sel4 = Sym "sel4" sel4+    toSym Sel5 = Sym "sel5" sel5+    toSym Sel6 = Sym "sel6" sel6+    toSym Sel7 = Sym "sel7" sel7++instance ExprEq (Select ctx) where exprEq = exprEqSym; exprHash = exprHashSym+instance Render (Select ctx) where renderPart = renderPartSym+instance Eval   (Select ctx) where evaluate   = evaluateSym+instance ToTree (Select ctx)++-- | Return the selected position, e.g.+--+-- > selectPos (Sel3 poly :: Select Poly ((Int,Int,Int,Int) :-> Full Int)) = 3+selectPos :: Select ctx a -> Int+selectPos Sel1 = 1+selectPos Sel2 = 2+selectPos Sel3 = 3+selectPos Sel4 = 4+selectPos Sel5 = 5+selectPos Sel6 = 6+selectPos Sel7 = 7++++sugarTup2+    :: ( Syntactic a dom+       , Syntactic b dom+       , Sat ctx (Internal a)+       , Sat ctx (Internal b)+       , Select ctx :<: dom+       )+    => Proxy ctx+    -> ASTF dom (Internal a, Internal b)+    -> (a,b)+sugarTup2 ctx a =+    ( sugarSymCtx ctx Sel1 a+    , sugarSymCtx ctx Sel2 a+    )++sugarTup3+    :: ( Syntactic a dom+       , Syntactic b dom+       , Syntactic c dom+       , Sat ctx (Internal a)+       , Sat ctx (Internal b)+       , Sat ctx (Internal c)+       , Select ctx :<: dom+       )+    => Proxy ctx+    -> ASTF dom (Internal a, Internal b, Internal c)+    -> (a,b,c)+sugarTup3 ctx a =+    ( sugarSymCtx ctx Sel1 a+    , sugarSymCtx ctx Sel2 a+    , sugarSymCtx ctx Sel3 a+    )++sugarTup4+    :: ( Syntactic a dom+       , Syntactic b dom+       , Syntactic c dom+       , Syntactic d dom+       , Sat ctx (Internal a)+       , Sat ctx (Internal b)+       , Sat ctx (Internal c)+       , Sat ctx (Internal d)+       , Select ctx :<: dom+       )+    => Proxy ctx+    -> ASTF dom (Internal a, Internal b, Internal c, Internal d)+    -> (a,b,c,d)+sugarTup4 ctx a =+    ( sugarSymCtx ctx Sel1 a+    , sugarSymCtx ctx Sel2 a+    , sugarSymCtx ctx Sel3 a+    , sugarSymCtx ctx Sel4 a+    )++sugarTup5+    :: ( Syntactic a dom+       , Syntactic b dom+       , Syntactic c dom+       , Syntactic d dom+       , Syntactic e dom+       , Sat ctx (Internal a)+       , Sat ctx (Internal b)+       , Sat ctx (Internal c)+       , Sat ctx (Internal d)+       , Sat ctx (Internal e)+       , Select ctx :<: dom+       )+    => Proxy ctx+    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e)+    -> (a,b,c,d,e)+sugarTup5 ctx a =+    ( sugarSymCtx ctx Sel1 a+    , sugarSymCtx ctx Sel2 a+    , sugarSymCtx ctx Sel3 a+    , sugarSymCtx ctx Sel4 a+    , sugarSymCtx ctx Sel5 a+    )++sugarTup6+    :: ( Syntactic a dom+       , Syntactic b dom+       , Syntactic c dom+       , Syntactic d dom+       , Syntactic e dom+       , Syntactic f dom+       , Sat ctx (Internal a)+       , Sat ctx (Internal b)+       , Sat ctx (Internal c)+       , Sat ctx (Internal d)+       , Sat ctx (Internal e)+       , Sat ctx (Internal f)+       , Select ctx :<: dom+       )+    => Proxy ctx+    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)+    -> (a,b,c,d,e,f)+sugarTup6 ctx a =+    ( sugarSymCtx ctx Sel1 a+    , sugarSymCtx ctx Sel2 a+    , sugarSymCtx ctx Sel3 a+    , sugarSymCtx ctx Sel4 a+    , sugarSymCtx ctx Sel5 a+    , sugarSymCtx ctx Sel6 a+    )++sugarTup7+    :: ( Syntactic a dom+       , Syntactic b dom+       , Syntactic c dom+       , Syntactic d dom+       , Syntactic e dom+       , Syntactic f dom+       , Syntactic g dom+       , Sat ctx (Internal a)+       , Sat ctx (Internal b)+       , Sat ctx (Internal c)+       , Sat ctx (Internal d)+       , Sat ctx (Internal e)+       , Sat ctx (Internal f)+       , Sat ctx (Internal g)+       , Select ctx :<: dom+       )+    => Proxy ctx+    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)+    -> (a,b,c,d,e,f,g)+sugarTup7 ctx a =+    ( sugarSymCtx ctx Sel1 a+    , sugarSymCtx ctx Sel2 a+    , sugarSymCtx ctx Sel3 a+    , sugarSymCtx ctx Sel4 a+    , sugarSymCtx ctx Sel5 a+    , sugarSymCtx ctx Sel6 a+    , sugarSymCtx ctx Sel7 a+    )+

@@ -0,0 +1,138 @@+{-# LANGUAGE UndecidableInstances #-}++-- | 'Syntactic' instances for tuples with 'Poly' context+module Language.Syntactic.Constructs.TupleSyntacticPoly where++++import Language.Syntactic.Syntax+import Language.Syntactic.Constructs.Tuple++++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Tuple  Poly :<: dom+    , Select Poly :<: dom+    ) =>+      Syntactic (a,b) dom+  where+    type Internal (a,b) =+        ( Internal a+        , Internal b+        )++    desugar = desugarTup2 poly+    sugar   = sugarTup2 poly++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Tuple  Poly :<: dom+    , Select Poly :<: dom+    ) =>+      Syntactic (a,b,c) dom+  where+    type Internal (a,b,c) =+        ( Internal a+        , Internal b+        , Internal c+        )++    desugar = desugarTup3 poly+    sugar   = sugarTup3 poly++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , Tuple  Poly :<: dom+    , Select Poly :<: dom+    ) =>+      Syntactic (a,b,c,d) dom+  where+    type Internal (a,b,c,d) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        )++    desugar = desugarTup4 poly+    sugar   = sugarTup4 poly++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , Syntactic e dom+    , Tuple  Poly :<: dom+    , Select Poly :<: dom+    ) =>+      Syntactic (a,b,c,d,e) dom+  where+    type Internal (a,b,c,d,e) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        )++    desugar = desugarTup5 poly+    sugar   = sugarTup5 poly++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , Syntactic e dom+    , Syntactic f dom+    , Tuple  Poly :<: dom+    , Select Poly :<: dom+    ) =>+      Syntactic (a,b,c,d,e,f) dom+  where+    type Internal (a,b,c,d,e,f) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        )++    desugar = desugarTup6 poly+    sugar   = sugarTup6 poly++instance+    ( Syntactic a dom+    , Syntactic b dom+    , Syntactic c dom+    , Syntactic d dom+    , Syntactic e dom+    , Syntactic f dom+    , Syntactic g dom+    , Tuple  Poly :<: dom+    , Select Poly :<: dom+    ) =>+      Syntactic (a,b,c,d,e,f,g) dom+  where+    type Internal (a,b,c,d,e,f,g) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        , Internal g+        )++    desugar = desugarTup7 poly+    sugar   = sugarTup7 poly+

@@ -0,0 +1,138 @@+{-# LANGUAGE UndecidableInstances #-}++-- | 'Syntactic' instances for tuples with 'SimpleCtx' context+module Language.Syntactic.Constructs.TupleSyntacticSimple where++++import Language.Syntactic.Syntax+import Language.Syntactic.Constructs.Tuple++++instance+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)+    , Syntactic b dom, Eq (Internal b), Show (Internal b)+    , Tuple  SimpleCtx :<: dom+    , Select SimpleCtx :<: dom+    ) =>+      Syntactic (a,b) dom+  where+    type Internal (a,b) =+        ( Internal a+        , Internal b+        )++    desugar = desugarTup2 simpleCtx+    sugar   = sugarTup2 simpleCtx++instance+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)+    , Syntactic b dom, Eq (Internal b), Show (Internal b)+    , Syntactic c dom, Eq (Internal c), Show (Internal c)+    , Tuple  SimpleCtx :<: dom+    , Select SimpleCtx :<: dom+    ) =>+      Syntactic (a,b,c) dom+  where+    type Internal (a,b,c) =+        ( Internal a+        , Internal b+        , Internal c+        )++    desugar = desugarTup3 simpleCtx+    sugar   = sugarTup3 simpleCtx++instance+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)+    , Syntactic b dom, Eq (Internal b), Show (Internal b)+    , Syntactic c dom, Eq (Internal c), Show (Internal c)+    , Syntactic d dom, Eq (Internal d), Show (Internal d)+    , Tuple  SimpleCtx :<: dom+    , Select SimpleCtx :<: dom+    ) =>+      Syntactic (a,b,c,d) dom+  where+    type Internal (a,b,c,d) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        )++    desugar = desugarTup4 simpleCtx+    sugar   = sugarTup4 simpleCtx++instance+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)+    , Syntactic b dom, Eq (Internal b), Show (Internal b)+    , Syntactic c dom, Eq (Internal c), Show (Internal c)+    , Syntactic d dom, Eq (Internal d), Show (Internal d)+    , Syntactic e dom, Eq (Internal e), Show (Internal e)+    , Tuple  SimpleCtx :<: dom+    , Select SimpleCtx :<: dom+    ) =>+      Syntactic (a,b,c,d,e) dom+  where+    type Internal (a,b,c,d,e) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        )++    desugar = desugarTup5 simpleCtx+    sugar   = sugarTup5 simpleCtx++instance+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)+    , Syntactic b dom, Eq (Internal b), Show (Internal b)+    , Syntactic c dom, Eq (Internal c), Show (Internal c)+    , Syntactic d dom, Eq (Internal d), Show (Internal d)+    , Syntactic e dom, Eq (Internal e), Show (Internal e)+    , Syntactic f dom, Eq (Internal f), Show (Internal f)+    , Tuple  SimpleCtx :<: dom+    , Select SimpleCtx :<: dom+    ) =>+      Syntactic (a,b,c,d,e,f) dom+  where+    type Internal (a,b,c,d,e,f) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        )++    desugar = desugarTup6 simpleCtx+    sugar   = sugarTup6 simpleCtx++instance+    ( Syntactic a dom, Eq (Internal a), Show (Internal a)+    , Syntactic b dom, Eq (Internal b), Show (Internal b)+    , Syntactic c dom, Eq (Internal c), Show (Internal c)+    , Syntactic d dom, Eq (Internal d), Show (Internal d)+    , Syntactic e dom, Eq (Internal e), Show (Internal e)+    , Syntactic f dom, Eq (Internal f), Show (Internal f)+    , Syntactic g dom, Eq (Internal g), Show (Internal g)+    , Tuple  SimpleCtx :<: dom+    , Select SimpleCtx :<: dom+    ) =>+      Syntactic (a,b,c,d,e,f,g) dom+  where+    type Internal (a,b,c,d,e,f,g) =+        ( Internal a+        , Internal b+        , Internal c+        , Internal d+        , Internal e+        , Internal f+        , Internal g+        )++    desugar = desugarTup7 simpleCtx+    sugar   = sugarTup7 simpleCtx+

@@ -1,99 +0,0 @@--- | Annotations for syntax trees--module Language.Syntactic.Features.Annotate where----import Data.Tree--import Language.Syntactic.Syntax-import Language.Syntactic.Interpretation.Equality-import Language.Syntactic.Interpretation.Render-import Language.Syntactic.Interpretation.Evaluation------ | Annotating an expression with arbitrary information.------ This can be used to annotate every node of a syntax tree, which is done by--- changing------ > AST dom a------ to------ > AST (Ann info dom) a------ Injection/projection of an annotated tree is done using--- 'injectAnn' / 'projectAnn'.-data Ann info expr a-  where-    Ann-        :: { annInfo :: info (EvalResult a)-           , annExpr :: expr a-           }-        -> Ann info expr a--type AnnSTF info dom a = ASTF (Ann info dom) a----instance ExprEq expr => ExprEq (Ann info expr)-  where-    exprEq a b = annExpr a `exprEq` annExpr b-    exprHash   = exprHash . annExpr--instance Render expr => Render (Ann info expr)-  where-    render = render . annExpr--instance ToTree expr => ToTree (Ann info expr)-  where-    toTreePart args = toTreePart args . annExpr--instance Eval expr => Eval (Ann info expr)-  where-    evaluate = evaluate . annExpr----injectAnn :: (sub :<: sup, ConsType a) =>-    info (EvalResult a) -> sub a -> AST (Ann info sup) a-injectAnn info = Symbol . Ann info . inject--projectAnn :: (sub :<: sup) =>-    AST (Ann info sup) a -> Maybe (info (EvalResult a), sub a)-projectAnn a = do-    Symbol (Ann info b) <- return a-    c                   <- project b-    return (info, c)---- | Get the annotation of the top-level node-getInfo :: AST (Ann info dom) a -> info (EvalResult a)-getInfo (Symbol (Ann info _)) = info-getInfo (f :$: _)             = getInfo f---- | Collect the annotations of all nodes-collectInfo :: (forall a . info a -> b) -> AST (Ann info dom) a -> [b]-collectInfo coll (Symbol (Ann info _)) = [coll info]-collectInfo coll (f :$: a) = collectInfo coll f ++ collectInfo coll a---- | Rendering of annotated syntax trees-toTreeAnn :: forall info dom a . (Render info, ToTree dom) =>-    ASTF (Ann info dom) a -> Tree String-toTreeAnn a = mkTree [] a-  where-    mkTree :: [Tree String] -> AST (Ann info dom) b -> Tree String-    mkTree args (Symbol (Ann info expr)) = Node infoStr [toTreePart args expr]-      where-        infoStr = "<<" ++ render info ++ ">>"-    mkTree args (f :$: a) = mkTree (mkTree [] a : args) f---- | Show an annotated syntax tree using ASCII art-showANN :: (Render info, ToTree dom) => ASTF (Ann info dom) a -> String-showANN = drawTree . toTreeAnn---- | Print an annotated syntax tree using ASCII art-drawANN :: (Render info, ToTree dom) => ASTF (Ann info dom) a -> IO ()-drawANN = putStrLn . showANN-

@@ -1,276 +0,0 @@--- | General binding constructs--module Language.Syntactic.Features.Binding where----import Control.Monad.Reader-import Data.Dynamic-import Data.Ix-import Data.Tree--import Data.Hash-import Data.Proxy--import Language.Syntactic--------------------------------------------------------------------------------------- * Variables------------------------------------------------------------------------------------- | Variable identifier-newtype VarId = VarId { varInteger :: Integer }-  deriving (Eq, Ord, Num, Real, Integral, Enum, Ix)--instance Show VarId-  where-    show (VarId i) = show i--showVar :: VarId -> String-showVar v = "var" ++ show v------ | Variables-data Variable ctx a-  where-    Variable :: (Typeable a, Sat ctx a) => VarId -> Variable ctx (Full a)-      -- 'Typeable' needed by the dynamic types in 'evalLambda'.--instance WitnessCons (Variable ctx)-  where-    witnessCons (Variable _) = ConsWit--instance WitnessSat (Variable ctx)-  where-    type Context (Variable ctx) = ctx-    witnessSat (Variable _) = Witness'---- | 'exprEq' does strict identifier comparison; i.e. no alpha equivalence.------ 'exprHash' assigns the same hash to all variables. This is a valid--- over-approximation that enables the following property:------ @`alphaEq` a b  ==>  `exprHash` a == `exprHash` b@-instance ExprEq (Variable ctx)-  where-    exprEq (Variable v1) (Variable v2) = v1==v2-    exprHash (Variable _)              = hashInt 0--instance Render (Variable ctx)-  where-    render (Variable v) = showVar v--instance ToTree (Variable ctx)-  where-    toTreePart [] (Variable v) = Node ("var:" ++ show v) []---- | Partial `Variable` projection with explicit context-prjVariable :: (Variable ctx :<: sup) =>-    Proxy ctx -> sup a -> Maybe (Variable ctx a)-prjVariable _ = project--------------------------------------------------------------------------------------- * Lambda binding------------------------------------------------------------------------------------- | Lambda binding-data Lambda ctx a-  where-    Lambda :: (Typeable a, Sat ctx a) =>-        VarId -> Lambda ctx (b :-> Full (a -> b))-      -- 'Typeable' needed by the dynamic types in 'evalLambda'.--instance WitnessCons (Lambda ctx)-  where-    witnessCons (Lambda _) = ConsWit---- | 'exprEq' does strict identifier comparison; i.e. no alpha equivalence.------ 'exprHash' assigns the same hash to all 'Lambda' bindings. This is a valid--- over-approximation that enables the following property:------ @`alphaEq` a b  ==>  `exprHash` a == `exprHash` b@-instance ExprEq (Lambda ctx)-  where-    exprEq (Lambda v1) (Lambda v2) = v1==v2-    exprHash (Lambda _)            = hashInt 0--instance Render (Lambda ctx)-  where-    renderPart [body] (Lambda v) = "(\\" ++ showVar v ++ " -> "  ++ body ++ ")"--instance ToTree (Lambda ctx)-  where-    toTreePart [body] (Lambda v) = Node ("Lambda " ++ show v) [body]---- | Partial `Lambda` projection with explicit context-prjLambda :: (Lambda ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Lambda ctx a)-prjLambda _ = project------ | The class of n-ary binding functions-class NAry ctx a dom | a -> dom-    -- Note: using a functional dependency rather than an associated type,-    -- because this makes it possible to make a class alias constraining dom.-    -- GHC doesn't yet handle equality super classes.-  where-    type NAryEval a--    -- | N-ary binding by nested use of the supplied binder-    bindN-      :: Proxy ctx-      -> (  forall b c . (Typeable b, Typeable c, Sat ctx b)-         => (ASTF dom b -> ASTF dom c)-         -> ASTF dom (b -> c)-         )-      -> a -> ASTF dom (NAryEval a)--instance Sat ctx a => NAry ctx (ASTF dom a) dom-  where-    type NAryEval (ASTF dom a) = a-    bindN _ _ = id--instance (Typeable a, Sat ctx a, NAry ctx b dom, Typeable (NAryEval b)) =>-    NAry ctx (ASTF dom a -> b) dom-  where-    type NAryEval (ASTF dom a -> b) = a -> NAryEval b-    bindN ctx lambda = lambda . (bindN ctx lambda .)--------------------------------------------------------------------------------------- * Let binding------------------------------------------------------------------------------------- | Let binding------ A 'Let' expression is really just an application of a lambda binding (the--- argument @(a -> b)@ is preferably constructed by 'Lambda').-data Let ctxa ctxb a-  where-    Let :: (Sat ctxa a, Sat ctxb b) => Let ctxa ctxb (a :-> (a -> b) :-> Full b)--instance WitnessCons (Let ctxa ctxb)-  where-    witnessCons Let = ConsWit--instance WitnessSat (Let ctxa ctxb)-  where-    type Context (Let ctxa ctxb) = ctxb-    witnessSat Let = Witness'--instance ExprEq (Let ctxa ctxb)-  where-    exprEq Let Let = True--    exprHash Let = hashInt 0--instance Render (Let ctxa ctxb)-  where-    renderPart []    Let = "Let"-    renderPart [f,a] Let = "(" ++ unwords ["letBind",f,a] ++ ")"--instance ToTree (Let ctxa ctxb)-  where-    toTreePart [a,body] Let = Node ("Let " ++ var) [a,body']-      where-        Node node [body'] = body-        var               = drop 7 node  -- Drop the "Lambda " prefix--instance Eval (Let ctxa ctxb)-  where-    evaluate Let = fromEval (flip ($))---- | Partial `Let` projection with explicit context-prjLet :: (Let ctxa ctxb :<: sup) =>-    Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a)-prjLet _ _ = project--------------------------------------------------------------------------------------- * Interpretation------------------------------------------------------------------------------------- | Alpha equivalence in an environment of variable equivalences. The supplied--- equivalence function gets called when the argument expressions are not both--- 'Variable's, both 'Lambda's or both ':$:'.-alphaEqM :: (Lambda ctx :<: dom, Variable ctx :<: dom)-    => Proxy ctx-    -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool)-    -> (forall a b . AST dom a -> AST dom b -> Reader [(VarId,VarId)] Bool)---- TODO This function is not ideal, since the type says nothing about which---      cases have been handled when calling 'eq'.--alphaEqM ctx eq-    ((prjLambda ctx -> Just (Lambda v1)) :$: a1)-    ((prjLambda ctx -> Just (Lambda v2)) :$: a2) =-        local ((v1,v2):) $ alphaEqM ctx eq a1 a2--alphaEqM ctx eq-    (prjVariable ctx -> Just (Variable v1))-    (prjVariable ctx -> Just (Variable v2)) = do-        env <- ask-        case lookup v1 env of-          Nothing  -> return (v1==v2)   -- Free variables-          Just v2' -> return (v2==v2')--alphaEqM ctx eq (f1 :$: a1) (f2 :$: a2) = do-    e <- alphaEqM ctx eq f1 f2-    if e then alphaEqM ctx eq a1 a2 else return False--alphaEqM _ eq a b = eq a b------ | Alpha-equivalence on lambda expressions. Free variables are taken to be--- equivalent if they have the same identifier.-alphaEq :: (Lambda ctx :<: dom, Variable ctx :<: dom, ExprEq dom) =>-    Proxy ctx -> AST dom a -> AST dom b -> Bool-alphaEq ctx a b = runReader (alphaEqM ctx (\a b -> return $ exprEq a b) a b) []------ | Evaluation of possibly open lambda expressions-evalLambdaM :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>-    ASTF (Lambda ctx :+: Variable ctx :+: dom) a -> m a-evalLambdaM = liftM result . eval-  where-    eval :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>-        AST (Lambda ctx :+: Variable ctx :+: dom) a -> m a-    eval (Symbol (InjectR (InjectL (Variable v)))) = do-        env <- ask-        case lookup v env of-          Nothing -> return $ error "eval: evaluating free variable"-          Just a  -> case fromDynamic a of-            Just a -> return (Full a)-            _      -> return $ error "eval: internal type error"--    eval (Symbol (InjectL (Lambda v)) :$: body) = do-        env <- ask-        return-            $ Full-            $ \a -> flip runReader ((v,toDyn a):env)-            $ liftM result-            $ eval body--    eval (f :$: a) = do-        f' <- eval f-        a' <- eval a-        return (f' $: result a')--    eval (Symbol (InjectR (InjectR a))) = return (evaluate a)------ | Evaluation of closed lambda expressions-evalLambda :: Eval dom => ASTF (Lambda ctx :+: Variable ctx :+: dom) a -> a-evalLambda = flip runReader [] . evalLambdaM-

@@ -1,134 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | This module provides binding constructs using higher-order syntax and a--- function for translating to first-order syntax. Expressions constructed using--- the exported interface are guaranteed to have a well-behaved translation.--module Language.Syntactic.Features.Binding.HigherOrder-    ( Variable-    , evalLambda-    , Let (..)-    , HOLambda (..)-    , HOAST-    , HOASTF-    , lambda-    , lambdaN-    , letBindCtx-    , letBind-    , reifyM-    , reifyTop-    , Reifiable-    , reifyCtx-    , reify-    ) where----import Control.Monad.State-import Data.Typeable--import Data.Proxy--import Language.Syntactic-import Language.Syntactic.Features.Binding------ | Higher-order lambda binding-data HOLambda ctx dom a-  where-    HOLambda :: (Typeable a, Typeable b, Sat ctx a)-        => (HOASTF ctx dom a -> HOASTF ctx dom b)-        -> HOLambda ctx dom (Full (a -> b))--type HOAST  ctx dom   = AST (HOLambda ctx dom :+: Variable ctx :+: dom)-type HOASTF ctx dom a = HOAST ctx dom (Full a)--instance WitnessCons (HOLambda ctx dom)-  where-    witnessCons (HOLambda _) = ConsWit------ | Lambda binding-lambda :: (Typeable a, Typeable b, Sat ctx a) =>-    (HOASTF ctx dom a -> HOASTF ctx dom b) -> HOASTF ctx dom (a -> b)-lambda = inject . HOLambda---- | N-ary lambda binding-lambdaN :: forall ctx dom a-    .  NAry ctx a (HOLambda ctx dom :+: Variable ctx :+: dom)-    => a -> HOASTF ctx dom (NAryEval a)-lambdaN = bindN (Proxy :: Proxy ctx) lambda---- | Let binding with explicit context-letBindCtx :: forall ctxa ctxb dom a b-    .  (Typeable a, Typeable b, Let ctxa ctxb :<: dom, Sat ctxa a, Sat ctxb b)-    => Proxy ctxb-    -> HOASTF ctxa dom a-    -> (HOASTF ctxa dom a -> HOASTF ctxa dom b)-    -> HOASTF ctxa dom b-letBindCtx _ a f = inject let' :$: a :$: lambda f-  where-    let' :: Let ctxa ctxb (a :-> (a -> b) :-> Full b)-    let' = Let---- | Let binding-letBind :: (Typeable a, Typeable b, Let Poly Poly :<: dom)-    => HOASTF Poly dom a-    -> (HOASTF Poly dom a -> HOASTF Poly dom b)-    -> HOASTF Poly dom b-letBind = letBindCtx poly----reifyM :: forall ctx dom a . Typeable a-    => HOAST ctx dom a-    -> State VarId (AST (Lambda ctx :+: Variable ctx :+: dom) a)-reifyM (f :$: a)            = liftM2 (:$:) (reifyM f) (reifyM a)-reifyM (Symbol (InjectR a)) = return $ Symbol $ InjectR a-reifyM (Symbol (InjectL (HOLambda f))) = do-    v    <- get; put (v+1)-    body <- reifyM $ f $ inject $ (Variable v `withContext` ctx)-    return $ inject (Lambda v `withContext` ctx) :$: body-  where-    ctx = Proxy :: Proxy ctx----- | Translating expressions with higher-order binding to corresponding--- expressions using first-order binding-reifyTop :: Typeable a =>-    HOAST ctx dom a -> AST (Lambda ctx :+: Variable ctx :+: dom) a-reifyTop = flip evalState 0 . reifyM-  -- It is assumed that there are no 'Variable' constructors (i.e. no free-  -- variables) in the argument. This is guaranteed by the exported interface.------ | Convenient class alias for n-ary syntactic functions-class-    ( SyntacticN a internal-    , NAry ctx internal (HOLambda ctx dom :+: Variable ctx :+: dom)-    , Typeable (NAryEval internal)-    ) =>-      Reifiable ctx a dom internal | a -> dom internal--instance-    ( SyntacticN a internal-    , NAry ctx internal (HOLambda ctx dom :+: Variable ctx :+: dom)-    , Typeable (NAryEval internal)-    ) =>-      Reifiable ctx a dom internal---- | Reifying an n-ary syntactic function with explicit context-reifyCtx :: Reifiable ctx a dom internal-    => Proxy ctx-    -> a-    -> ASTF (Lambda ctx :+: Variable ctx :+: dom) (NAryEval internal)-reifyCtx _ = reifyTop . lambdaN . desugarN---- | Reifying an n-ary syntactic function-reify :: Reifiable Poly a dom internal =>-    a -> ASTF (Lambda Poly :+: Variable Poly :+: dom) (NAryEval internal)-reify = reifyCtx poly-

@@ -1,144 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | Partial evaluation--module Language.Syntactic.Features.Binding.PartialEval where----import Control.Monad.Writer-import Data.Set as Set--import Data.Proxy--import Language.Syntactic-import Language.Syntactic.Features.Symbol-import Language.Syntactic.Features.Literal-import Language.Syntactic.Features.Condition-import Language.Syntactic.Features.Tuple-import Language.Syntactic.Features.Binding------ | Constant folder------ Given an expression and the statically known value of that expression,--- returns a (possibly) new expression with the same meaning as the original.--- Typically, the result will be a 'Literal', if the relevant type constraints--- are satisfied.-type ConstFolder ctx dom = forall a-    .  ASTF (Lambda ctx :+: Variable ctx :+: dom) a-    -> a-    -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a---- | Partial evaluation-class Eval dom => PartialEval feature ctx dom-  where-    -- | Partial evaluation of a feature. The @(`Set` `VarId`)@ returned is the-    -- set of free variables of the expression. However, free variables are-    -- counted in a \"lazy\" sense: free variables from sub-expressions that are-    -- never evaluated may not be counted. (The instance for 'Conditional' will-    -- throw away the free variables of the pruned branch when the condition is-    -- statically known. This is one reason why partial evaluation and free-    -- variable calculation have to be done simultaneously.)-    partEvalFeat-        :: Proxy ctx-        -> ConstFolder ctx dom-        -> feature a-        -> HList (AST (Lambda ctx :+: Variable ctx :+: dom)) a-        -> Writer-            (Set VarId)-            (ASTF (Lambda ctx :+: Variable ctx :+: dom) (EvalResult a))--instance (PartialEval sub1 ctx dom, PartialEval sub2 ctx dom) =>-    PartialEval (sub1 :+: sub2) ctx dom-  where-    partEvalFeat ctx constFold (InjectL a) = partEvalFeat ctx constFold a-    partEvalFeat ctx constFold (InjectR a) = partEvalFeat ctx constFold a--partialEvalM :: PartialEval dom ctx dom-    => Proxy ctx-    -> ConstFolder ctx dom-    -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a-    -> Writer (Set VarId) (ASTF (Lambda ctx :+: Variable ctx :+: dom) a)-partialEvalM ctx constFold = transformNodeC (partEvalFeat ctx constFold)---- | Partially evaluate an expression-partialEval :: PartialEval dom ctx dom-    => Proxy ctx-    -> ConstFolder ctx dom-    -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a-    -> ASTF (Lambda ctx :+: Variable ctx :+: dom) a-partialEval ctx constFold = fst . runWriter . partialEvalM ctx constFold------ | Convenient default implementation of 'partEvalFeat' (uses 'evalLambda' to--- evaluate)-partEvalFeatDefault-    :: ( feature :<: dom-       , WitnessCons feature-       , PartialEval dom ctx dom-       )-    => Proxy ctx-    -> ConstFolder ctx dom-    -> feature a-    -> HList (AST (Lambda ctx :+: Variable ctx :+: dom)) a-    -> Writer-        (Set VarId)-        (ASTF (Lambda ctx :+: Variable ctx :+: dom) (EvalResult a))-partEvalFeatDefault ctx constFold feat@(witnessCons -> ConsWit) args = do-    (args',vars) <- listen $ mapHListM (partialEvalM ctx constFold) args-    let result = appHList (Symbol $ InjectR $ InjectR $ inject feat) args'-        value  = evalLambda result-    if Set.null vars-      then return $ constFold result value-      else return result--instance (Sym ctx' :<: dom, PartialEval dom ctx dom) =>-    PartialEval (Sym ctx') ctx dom-  where-    partEvalFeat = partEvalFeatDefault--instance (Literal ctx' :<: dom, PartialEval dom ctx dom) =>-    PartialEval (Literal ctx') ctx dom-  where-    partEvalFeat = partEvalFeatDefault--instance (Condition ctx' :<: dom, PartialEval dom ctx dom) =>-    PartialEval (Condition ctx') ctx dom-  where-    partEvalFeat ctx constFold cond@Condition args@(c :*: t :*: e :*: Nil)-        | Set.null cVars = partialEvalM ctx constFold t_or_e-        | otherwise      = partEvalFeatDefault ctx constFold cond args-      where-        (c',cVars) = runWriter $ partialEvalM ctx constFold c-        t_or_e     = if evalLambda c' then t else e--instance (Tuple ctx' :<: dom, PartialEval dom ctx dom) =>-    PartialEval (Tuple ctx') ctx dom-  where-    partEvalFeat = partEvalFeatDefault--instance (Select ctx' :<: dom, PartialEval dom ctx dom) =>-    PartialEval (Select ctx') ctx dom-  where-    partEvalFeat = partEvalFeatDefault--instance PartialEval dom ctx dom => PartialEval (Variable ctx) ctx dom-  where-    partEvalFeat _ _ var@(Variable v) Nil = do-        tell (singleton v)-        return (inject var)--instance PartialEval dom ctx dom => PartialEval (Lambda ctx) ctx dom-  where-    partEvalFeat ctx constFold lam@(Lambda v) (body :*: Nil) = do-        body' <- censor (delete v) $ partialEvalM ctx constFold body-        return $ inject lam :$: body'--instance (Let ctxa ctxb :<: dom, PartialEval dom ctx dom) =>-    PartialEval (Let ctxa ctxb) ctx dom-  where-    partEvalFeat = partEvalFeatDefault-

@@ -1,57 +0,0 @@--- | Conditional expressions--module Language.Syntactic.Features.Condition where----import Data.Hash-import Data.Proxy--import Language.Syntactic-import Language.Syntactic.Features.Symbol----data Condition ctx a-  where-    Condition :: Sat ctx a => Condition ctx (Bool :-> a :-> a :-> Full a)--instance WitnessCons (Condition ctx)-  where-    witnessCons Condition = ConsWit--instance WitnessSat (Condition ctx)-  where-    type Context (Condition ctx) = ctx-    witnessSat Condition = Witness'--instance IsSymbol (Condition ctx)-  where-    toSym Condition = Sym "condition" (\c t e -> if c then t else e)--instance ExprEq (Condition ctx) where exprEq = exprEqSym; exprHash = exprHashSym-instance Render (Condition ctx) where renderPart = renderPartSym-instance Eval   (Condition ctx) where evaluate   = evaluateSym-instance ToTree (Condition ctx)------ | Conditional expression with explicit context-conditionCtx-    :: (Sat ctx (Internal a), Syntactic a dom, Condition ctx :<: dom)-    => Proxy ctx -> ASTF dom Bool -> a -> a -> a-conditionCtx ctx cond tHEN eLSE = sugar $ inject (Condition `withContext` ctx)-    :$: cond-    :$: desugar tHEN-    :$: desugar eLSE---- | Conditional expression-condition :: (Condition Poly :<: dom, Syntactic a dom) =>-    ASTF dom Bool -> a -> a -> a-condition = conditionCtx poly---- | Partial `Condition` projection with explicit context-prjCondition :: (Condition ctx :<: sup) =>-    Proxy ctx -> sup a -> Maybe (Condition ctx a)-prjCondition _ = project-

@@ -1,63 +0,0 @@--- | Literal expressions--module Language.Syntactic.Features.Literal where----import Data.Typeable--import Data.Hash-import Data.Proxy--import Language.Syntactic----data Literal ctx a-  where-    Literal :: (Eq a, Show a, Typeable a, Sat ctx a) =>-        a -> Literal ctx (Full a)--instance WitnessCons (Literal ctx)-  where-    witnessCons (Literal _) = ConsWit--instance WitnessSat (Literal ctx)-  where-    type Context (Literal ctx) = ctx-    witnessSat (Literal _) = Witness'--instance ExprEq (Literal ctx)-  where-    Literal a `exprEq` Literal b = case cast a of-        Just a' -> a'==b-        Nothing -> False--    exprHash (Literal a) = hash (show a)--instance Render (Literal ctx)-  where-    render (Literal a) = show a--instance ToTree (Literal ctx)--instance Eval (Literal ctx)-  where-    evaluate (Literal a) = fromEval a------ | Literal with explicit context-litCtx :: (Eq a, Show a, Typeable a, Sat ctx a, Literal ctx :<: dom) =>-    Proxy ctx -> a -> ASTF dom a-litCtx ctx = inject . (`withContext` ctx) . Literal---- | Literal-lit :: (Eq a, Show a, Typeable a, Literal Poly :<: dom) => a -> ASTF dom a-lit = litCtx poly---- | Partial literal projection with explicit context-prjLiteral :: (Literal ctx :<: sup) =>-    Proxy ctx -> sup a -> Maybe (Literal ctx a)-prjLiteral _ = project-

@@ -1,179 +0,0 @@--- | Simple symbols------ 'Sym' provides a simple way to make syntactic symbols for prototyping.--- However, note that 'Sym' is quite unsafe as it only uses 'String' to--- distinguish between different symbols. Also, 'Sym' has a very free type that--- allows any number of arguments.--module Language.Syntactic.Features.Symbol where----import Data.Typeable--import Data.Hash-import Data.Proxy--import Language.Syntactic----data Sym ctx a-  where-    Sym :: (ConsType a, Sat ctx (EvalResult a)) =>-        String -> ConsEval a -> Sym ctx a--instance WitnessCons (Sym ctx)-  where-    witnessCons (Sym _ _) = ConsWit--instance WitnessSat (Sym ctx)-  where-    type Context (Sym ctx) = ctx-    witnessSat (Sym _ _) = Witness'--witnessSatSym :: forall ctx dom a . (Sym ctx :<: dom)-    => Proxy ctx-    -> ASTF dom a-    -> Maybe (Witness' ctx a)-witnessSatSym ctx = witSym-  where-    witSym :: (EvalResult b ~ a) => AST dom b -> Maybe (Witness' ctx a)-    witSym (prjSym ctx -> Just (Sym _ _)) = Just Witness'-    witSym (f :$: _) = witSym f-    witSym _         = Nothing--instance ExprEq (Sym ctx)-  where-    exprEq (Sym a _) (Sym b _) = a==b-    exprHash (Sym name _)      = hash name--instance Render (Sym ctx)-  where-    renderPart [] (Sym name _) = name-    renderPart args (Sym name _)-        | isInfix   = "(" ++ unwords [a,op,b] ++ ")"-        | otherwise = "(" ++ unwords (name : args) ++ ")"-      where-        [a,b] = args-        op    = init $ tail name-        isInfix-          =  not (null name)-          && head name == '('-          && last name == ')'-          && length args == 2--instance ToTree (Sym ctx)--instance Eval (Sym ctx)-  where-    evaluate (Sym _ a) = fromEval a------ | A zero-argument symbol-sym0-    :: ( Sat ctx a-       , Sym ctx :<: dom-       )-    => Proxy ctx-    -> String-    -> a-    -> ASTF dom a-sym0 ctx name a = inject (Sym name a `withContext` ctx)---- | A one-argument symbol-sym1-    :: ( Typeable a-       , Sat ctx b-       , Sym ctx :<: dom-       )-    => Proxy ctx-    -> String-    -> (a -> b)-    -> ASTF dom a-    -> ASTF dom b-sym1 ctx name f a = inject (Sym name f `withContext` ctx) :$: a---- | A two-argument symbol-sym2-    :: ( Typeable a-       , Typeable b-       , Sat ctx c-       , Sym ctx :<: dom-       )-    => Proxy ctx-    -> String-    -> (a -> b -> c)-    -> ASTF dom a-    -> ASTF dom b-    -> ASTF dom c-sym2 ctx name f a b = inject (Sym name f `withContext` ctx) :$: a :$: b---- | A three-argument symbol-sym3-    :: ( Typeable a-       , Typeable b-       , Typeable c-       , Sat ctx d-       , Sym ctx :<: dom-       )-    => Proxy ctx-    -> String-    -> (a -> b -> c -> d)-    -> ASTF dom a-    -> ASTF dom b-    -> ASTF dom c-    -> ASTF dom d-sym3 ctx name f a b c = inject (Sym name f `withContext` ctx) :$: a :$: b :$: c---- | A four-argument symbol-sym4-    :: ( Typeable a-       , Typeable b-       , Typeable c-       , Typeable d-       , Sat ctx e-       , Sym ctx :<: dom-       )-    => Proxy ctx-    -> String-    -> (a -> b -> c -> d -> e)-    -> ASTF dom a-    -> ASTF dom b-    -> ASTF dom c-    -> ASTF dom d-    -> ASTF dom e-sym4 ctx name f a b c d =-    inject (Sym name f `withContext` ctx) :$: a :$: b :$: c :$: d------ | Partial symbol projection with explicit context-prjSym :: (Sym ctx :<: sup) =>-    Proxy ctx -> sup a -> Maybe (Sym ctx a)-prjSym _ = project------ | Class of expressions that can be treated as symbols-class IsSymbol expr-  where-    toSym :: expr a -> Sym Poly a---- | Default implementation of 'exprEq'-exprEqSym :: IsSymbol expr => expr a -> expr b -> Bool-exprEqSym a b = exprEq (toSym a) (toSym b)---- | Default implementation of 'exprHash'-exprHashSym :: IsSymbol expr => expr a -> Hash-exprHashSym = exprHash . toSym---- | Default implementation of 'renderPart'-renderPartSym :: IsSymbol expr => [String] -> expr a -> String-renderPartSym args = renderPart args . toSym---- | Default implementation of 'evaluate'-evaluateSym :: IsSymbol expr => expr a -> a-evaluateSym = evaluate . toSym-

@@ -1,391 +0,0 @@--- | Construction and projection of tuples in the object language------ The function pairs @desugarTupX@/@sugarTupX@ could be used directly in--- 'Syntactic' instances if it wasn't for the extra @(`Proxy` ctx)@ arguments.--- For this reason, 'Syntactic' instances have to be written manually for each--- context. The module "Language.Syntactic.Features.TupleSyntacticPoly" provides--- instances for a 'Poly' context. The exact same code can be used to make--- instances for other contexts -- just copy/paste and replace 'Poly' and 'poly'--- with the desired context (and probably add an extra constraint in the class--- contexts).--module Language.Syntactic.Features.Tuple where----import Data.Hash-import Data.Proxy-import Data.Tuple.Select--import Language.Syntactic-import Language.Syntactic.Features.Symbol--------------------------------------------------------------------------------------- * Construction------------------------------------------------------------------------------------- | Expressions for constructing tuples-data Tuple ctx a-  where-    Tup2 :: Sat ctx (a,b)           => Tuple ctx (a :-> b :-> Full (a,b))-    Tup3 :: Sat ctx (a,b,c)         => Tuple ctx (a :-> b :-> c :-> Full (a,b,c))-    Tup4 :: Sat ctx (a,b,c,d)       => Tuple ctx (a :-> b :-> c :-> d :-> Full (a,b,c,d))-    Tup5 :: Sat ctx (a,b,c,d,e)     => Tuple ctx (a :-> b :-> c :-> d :-> e :-> Full (a,b,c,d,e))-    Tup6 :: Sat ctx (a,b,c,d,e,f)   => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> Full (a,b,c,d,e,f))-    Tup7 :: Sat ctx (a,b,c,d,e,f,g) => Tuple ctx (a :-> b :-> c :-> d :-> e :-> f :-> g :-> Full (a,b,c,d,e,f,g))--instance WitnessCons (Tuple ctx)-  where-    witnessCons Tup2 = ConsWit-    witnessCons Tup3 = ConsWit-    witnessCons Tup4 = ConsWit-    witnessCons Tup5 = ConsWit-    witnessCons Tup6 = ConsWit-    witnessCons Tup7 = ConsWit--instance WitnessSat (Tuple ctx)-  where-    type Context (Tuple ctx) = ctx-    witnessSat Tup2 = Witness'-    witnessSat Tup3 = Witness'-    witnessSat Tup4 = Witness'-    witnessSat Tup5 = Witness'-    witnessSat Tup6 = Witness'-    witnessSat Tup7 = Witness'--instance IsSymbol (Tuple ctx)-  where-    toSym Tup2 = Sym "tup2" (,)-    toSym Tup3 = Sym "tup3" (,,)-    toSym Tup4 = Sym "tup4" (,,,)-    toSym Tup5 = Sym "tup5" (,,,,)-    toSym Tup6 = Sym "tup6" (,,,,,)-    toSym Tup7 = Sym "tup7" (,,,,,,)--instance ExprEq (Tuple ctx) where exprEq = exprEqSym; exprHash = exprHashSym-instance Render (Tuple ctx) where renderPart = renderPartSym-instance Eval   (Tuple ctx) where evaluate   = evaluateSym-instance ToTree (Tuple ctx)---- | Partial `Tuple` projection with explicit context-prjTuple :: (Tuple ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Tuple ctx a)-prjTuple _ = project----desugarTup2-    :: ( Syntactic a dom-       , Syntactic b dom-       , Sat ctx (Internal a, Internal b)-       , Tuple ctx :<: dom-       )-    => Proxy ctx-    -> (a,b)-    -> ASTF dom (Internal a, Internal b)-desugarTup2 ctx (a,b) = inject (Tup2 `withContext` ctx)-    :$: desugar a-    :$: desugar b--desugarTup3-    :: ( Syntactic a dom-       , Syntactic b dom-       , Syntactic c dom-       , Sat ctx (Internal a, Internal b, Internal c)-       , Tuple ctx :<: dom-       )-    => Proxy ctx-    -> (a,b,c)-    -> ASTF dom (Internal a, Internal b, Internal c)-desugarTup3 ctx (a,b,c) = inject (Tup3 `withContext` ctx)-    :$: desugar a-    :$: desugar b-    :$: desugar c--desugarTup4-    :: ( Syntactic a dom-       , Syntactic b dom-       , Syntactic c dom-       , Syntactic d dom-       , Sat ctx (Internal a, Internal b, Internal c, Internal d)-       , Tuple ctx :<: dom-       )-    => Proxy ctx-    -> (a,b,c,d)-    -> ASTF dom (Internal a, Internal b, Internal c, Internal d)-desugarTup4 ctx (a,b,c,d) = inject (Tup4 `withContext` ctx)-    :$: desugar a-    :$: desugar b-    :$: desugar c-    :$: desugar d--desugarTup5-    :: ( Syntactic a dom-       , Syntactic b dom-       , Syntactic c dom-       , Syntactic d dom-       , Syntactic e dom-       , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e)-       , Tuple ctx :<: dom-       )-    => Proxy ctx-    -> (a,b,c,d,e)-    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e)-desugarTup5 ctx (a,b,c,d,e) = inject (Tup5 `withContext` ctx)-    :$: desugar a-    :$: desugar b-    :$: desugar c-    :$: desugar d-    :$: desugar e--desugarTup6-    :: ( Syntactic a dom-       , Syntactic b dom-       , Syntactic c dom-       , Syntactic d dom-       , Syntactic e dom-       , Syntactic f dom-       , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)-       , Tuple ctx :<: dom-       )-    => Proxy ctx-    -> (a,b,c,d,e,f)-    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)-desugarTup6 ctx (a,b,c,d,e,f) = inject (Tup6 `withContext` ctx)-    :$: desugar a-    :$: desugar b-    :$: desugar c-    :$: desugar d-    :$: desugar e-    :$: desugar f--desugarTup7-    :: ( Syntactic a dom-       , Syntactic b dom-       , Syntactic c dom-       , Syntactic d dom-       , Syntactic e dom-       , Syntactic f dom-       , Syntactic g dom-       , Sat ctx (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)-       , Tuple ctx :<: dom-       )-    => Proxy ctx-    -> (a,b,c,d,e,f,g)-    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)-desugarTup7 ctx (a,b,c,d,e,f,g) = inject (Tup7 `withContext` ctx)-    :$: desugar a-    :$: desugar b-    :$: desugar c-    :$: desugar d-    :$: desugar e-    :$: desugar f-    :$: desugar g--------------------------------------------------------------------------------------- * Projection------------------------------------------------------------------------------------- | Expressions for selecting elements of a tuple-data Select ctx a-  where-    Sel1 :: (Sel1 a b, Sat ctx b) => Select ctx (a :-> Full b)-    Sel2 :: (Sel2 a b, Sat ctx b) => Select ctx (a :-> Full b)-    Sel3 :: (Sel3 a b, Sat ctx b) => Select ctx (a :-> Full b)-    Sel4 :: (Sel4 a b, Sat ctx b) => Select ctx (a :-> Full b)-    Sel5 :: (Sel5 a b, Sat ctx b) => Select ctx (a :-> Full b)-    Sel6 :: (Sel6 a b, Sat ctx b) => Select ctx (a :-> Full b)-    Sel7 :: (Sel7 a b, Sat ctx b) => Select ctx (a :-> Full b)--instance WitnessCons (Select ctx)-  where-    witnessCons Sel1 = ConsWit-    witnessCons Sel2 = ConsWit-    witnessCons Sel3 = ConsWit-    witnessCons Sel4 = ConsWit-    witnessCons Sel5 = ConsWit-    witnessCons Sel6 = ConsWit-    witnessCons Sel7 = ConsWit--instance WitnessSat (Select ctx)-  where-    type Context (Select ctx) = ctx-    witnessSat Sel1 = Witness'-    witnessSat Sel2 = Witness'-    witnessSat Sel3 = Witness'-    witnessSat Sel4 = Witness'-    witnessSat Sel5 = Witness'-    witnessSat Sel6 = Witness'-    witnessSat Sel7 = Witness'--instance IsSymbol (Select ctx)-  where-    toSym Sel1 = Sym "sel1" sel1-    toSym Sel2 = Sym "sel2" sel2-    toSym Sel3 = Sym "sel3" sel3-    toSym Sel4 = Sym "sel4" sel4-    toSym Sel5 = Sym "sel5" sel5-    toSym Sel6 = Sym "sel6" sel6-    toSym Sel7 = Sym "sel7" sel7--instance ExprEq (Select ctx) where exprEq = exprEqSym; exprHash = exprHashSym-instance Render (Select ctx) where renderPart = renderPartSym-instance Eval   (Select ctx) where evaluate   = evaluateSym-instance ToTree (Select ctx)---- | Partial `Select` projection with explicit context-prjSelect :: (Select ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Select ctx a)-prjSelect _ = project---- | Return the selected position, e.g.------ > selectPos (Sel3 poly :: Select Poly ((Int,Int,Int,Int) :-> Full Int)) = 3-selectPos :: Select ctx a -> Int-selectPos Sel1 = 1-selectPos Sel2 = 2-selectPos Sel3 = 3-selectPos Sel4 = 4-selectPos Sel5 = 5-selectPos Sel6 = 6-selectPos Sel7 = 7----sugarTup2-    :: ( Syntactic a dom-       , Syntactic b dom-       , Sat ctx (Internal a)-       , Sat ctx (Internal b)-       , Select ctx :<: dom-       )-    => Proxy ctx-    -> ASTF dom (Internal a, Internal b)-    -> (a,b)-sugarTup2 ctx a =-    ( sugar $ inject (Sel1 `withContext` ctx) :$: a-    , sugar $ inject (Sel2 `withContext` ctx) :$: a-    )--sugarTup3-    :: ( Syntactic a dom-       , Syntactic b dom-       , Syntactic c dom-       , Sat ctx (Internal a)-       , Sat ctx (Internal b)-       , Sat ctx (Internal c)-       , Select ctx :<: dom-       )-    => Proxy ctx-    -> ASTF dom (Internal a, Internal b, Internal c)-    -> (a,b,c)-sugarTup3 ctx a =-    ( sugar $ inject (Sel1 `withContext` ctx) :$: a-    , sugar $ inject (Sel2 `withContext` ctx) :$: a-    , sugar $ inject (Sel3 `withContext` ctx) :$: a-    )--sugarTup4-    :: ( Syntactic a dom-       , Syntactic b dom-       , Syntactic c dom-       , Syntactic d dom-       , Sat ctx (Internal a)-       , Sat ctx (Internal b)-       , Sat ctx (Internal c)-       , Sat ctx (Internal d)-       , Select ctx :<: dom-       )-    => Proxy ctx-    -> ASTF dom (Internal a, Internal b, Internal c, Internal d)-    -> (a,b,c,d)-sugarTup4 ctx a =-    ( sugar $ inject (Sel1 `withContext` ctx) :$: a-    , sugar $ inject (Sel2 `withContext` ctx) :$: a-    , sugar $ inject (Sel3 `withContext` ctx) :$: a-    , sugar $ inject (Sel4 `withContext` ctx) :$: a-    )--sugarTup5-    :: ( Syntactic a dom-       , Syntactic b dom-       , Syntactic c dom-       , Syntactic d dom-       , Syntactic e dom-       , Sat ctx (Internal a)-       , Sat ctx (Internal b)-       , Sat ctx (Internal c)-       , Sat ctx (Internal d)-       , Sat ctx (Internal e)-       , Select ctx :<: dom-       )-    => Proxy ctx-    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e)-    -> (a,b,c,d,e)-sugarTup5 ctx a =-    ( sugar $ inject (Sel1 `withContext` ctx) :$: a-    , sugar $ inject (Sel2 `withContext` ctx) :$: a-    , sugar $ inject (Sel3 `withContext` ctx) :$: a-    , sugar $ inject (Sel4 `withContext` ctx) :$: a-    , sugar $ inject (Sel5 `withContext` ctx) :$: a-    )--sugarTup6-    :: ( Syntactic a dom-       , Syntactic b dom-       , Syntactic c dom-       , Syntactic d dom-       , Syntactic e dom-       , Syntactic f dom-       , Sat ctx (Internal a)-       , Sat ctx (Internal b)-       , Sat ctx (Internal c)-       , Sat ctx (Internal d)-       , Sat ctx (Internal e)-       , Sat ctx (Internal f)-       , Select ctx :<: dom-       )-    => Proxy ctx-    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f)-    -> (a,b,c,d,e,f)-sugarTup6 ctx a =-    ( sugar $ inject (Sel1 `withContext` ctx) :$: a-    , sugar $ inject (Sel2 `withContext` ctx) :$: a-    , sugar $ inject (Sel3 `withContext` ctx) :$: a-    , sugar $ inject (Sel4 `withContext` ctx) :$: a-    , sugar $ inject (Sel5 `withContext` ctx) :$: a-    , sugar $ inject (Sel6 `withContext` ctx) :$: a-    )--sugarTup7-    :: ( Syntactic a dom-       , Syntactic b dom-       , Syntactic c dom-       , Syntactic d dom-       , Syntactic e dom-       , Syntactic f dom-       , Syntactic g dom-       , Sat ctx (Internal a)-       , Sat ctx (Internal b)-       , Sat ctx (Internal c)-       , Sat ctx (Internal d)-       , Sat ctx (Internal e)-       , Sat ctx (Internal f)-       , Sat ctx (Internal g)-       , Select ctx :<: dom-       )-    => Proxy ctx-    -> ASTF dom (Internal a, Internal b, Internal c, Internal d, Internal e, Internal f, Internal g)-    -> (a,b,c,d,e,f,g)-sugarTup7 ctx a =-    ( sugar $ inject (Sel1 `withContext` ctx) :$: a-    , sugar $ inject (Sel2 `withContext` ctx) :$: a-    , sugar $ inject (Sel3 `withContext` ctx) :$: a-    , sugar $ inject (Sel4 `withContext` ctx) :$: a-    , sugar $ inject (Sel5 `withContext` ctx) :$: a-    , sugar $ inject (Sel6 `withContext` ctx) :$: a-    , sugar $ inject (Sel7 `withContext` ctx) :$: a-    )-

@@ -1,138 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | 'Syntactic' instances for tuples with 'Poly' context-module Language.Syntactic.Features.TupleSyntacticPoly where----import Language.Syntactic.Syntax-import Language.Syntactic.Features.Tuple----instance-    ( Syntactic a dom-    , Syntactic b dom-    , Tuple  Poly :<: dom-    , Select Poly :<: dom-    ) =>-      Syntactic (a,b) dom-  where-    type Internal (a,b) =-        ( Internal a-        , Internal b-        )--    desugar = desugarTup2 poly-    sugar   = sugarTup2 poly--instance-    ( Syntactic a dom-    , Syntactic b dom-    , Syntactic c dom-    , Tuple  Poly :<: dom-    , Select Poly :<: dom-    ) =>-      Syntactic (a,b,c) dom-  where-    type Internal (a,b,c) =-        ( Internal a-        , Internal b-        , Internal c-        )--    desugar = desugarTup3 poly-    sugar   = sugarTup3 poly--instance-    ( Syntactic a dom-    , Syntactic b dom-    , Syntactic c dom-    , Syntactic d dom-    , Tuple  Poly :<: dom-    , Select Poly :<: dom-    ) =>-      Syntactic (a,b,c,d) dom-  where-    type Internal (a,b,c,d) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        )--    desugar = desugarTup4 poly-    sugar   = sugarTup4 poly--instance-    ( Syntactic a dom-    , Syntactic b dom-    , Syntactic c dom-    , Syntactic d dom-    , Syntactic e dom-    , Tuple  Poly :<: dom-    , Select Poly :<: dom-    ) =>-      Syntactic (a,b,c,d,e) dom-  where-    type Internal (a,b,c,d,e) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        )--    desugar = desugarTup5 poly-    sugar   = sugarTup5 poly--instance-    ( Syntactic a dom-    , Syntactic b dom-    , Syntactic c dom-    , Syntactic d dom-    , Syntactic e dom-    , Syntactic f dom-    , Tuple  Poly :<: dom-    , Select Poly :<: dom-    ) =>-      Syntactic (a,b,c,d,e,f) dom-  where-    type Internal (a,b,c,d,e,f) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        , Internal f-        )--    desugar = desugarTup6 poly-    sugar   = sugarTup6 poly--instance-    ( Syntactic a dom-    , Syntactic b dom-    , Syntactic c dom-    , Syntactic d dom-    , Syntactic e dom-    , Syntactic f dom-    , Syntactic g dom-    , Tuple  Poly :<: dom-    , Select Poly :<: dom-    ) =>-      Syntactic (a,b,c,d,e,f,g) dom-  where-    type Internal (a,b,c,d,e,f,g) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        , Internal f-        , Internal g-        )--    desugar = desugarTup7 poly-    sugar   = sugarTup7 poly-

@@ -1,138 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}---- | 'Syntactic' instances for tuples with 'SimpleCtx' context-module Language.Syntactic.Features.TupleSyntacticSimple where----import Language.Syntactic.Syntax-import Language.Syntactic.Features.Tuple----instance-    ( Syntactic a dom, Eq (Internal a), Show (Internal a)-    , Syntactic b dom, Eq (Internal b), Show (Internal b)-    , Tuple  SimpleCtx :<: dom-    , Select SimpleCtx :<: dom-    ) =>-      Syntactic (a,b) dom-  where-    type Internal (a,b) =-        ( Internal a-        , Internal b-        )--    desugar = desugarTup2 simpleCtx-    sugar   = sugarTup2 simpleCtx--instance-    ( Syntactic a dom, Eq (Internal a), Show (Internal a)-    , Syntactic b dom, Eq (Internal b), Show (Internal b)-    , Syntactic c dom, Eq (Internal c), Show (Internal c)-    , Tuple  SimpleCtx :<: dom-    , Select SimpleCtx :<: dom-    ) =>-      Syntactic (a,b,c) dom-  where-    type Internal (a,b,c) =-        ( Internal a-        , Internal b-        , Internal c-        )--    desugar = desugarTup3 simpleCtx-    sugar   = sugarTup3 simpleCtx--instance-    ( Syntactic a dom, Eq (Internal a), Show (Internal a)-    , Syntactic b dom, Eq (Internal b), Show (Internal b)-    , Syntactic c dom, Eq (Internal c), Show (Internal c)-    , Syntactic d dom, Eq (Internal d), Show (Internal d)-    , Tuple  SimpleCtx :<: dom-    , Select SimpleCtx :<: dom-    ) =>-      Syntactic (a,b,c,d) dom-  where-    type Internal (a,b,c,d) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        )--    desugar = desugarTup4 simpleCtx-    sugar   = sugarTup4 simpleCtx--instance-    ( Syntactic a dom, Eq (Internal a), Show (Internal a)-    , Syntactic b dom, Eq (Internal b), Show (Internal b)-    , Syntactic c dom, Eq (Internal c), Show (Internal c)-    , Syntactic d dom, Eq (Internal d), Show (Internal d)-    , Syntactic e dom, Eq (Internal e), Show (Internal e)-    , Tuple  SimpleCtx :<: dom-    , Select SimpleCtx :<: dom-    ) =>-      Syntactic (a,b,c,d,e) dom-  where-    type Internal (a,b,c,d,e) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        )--    desugar = desugarTup5 simpleCtx-    sugar   = sugarTup5 simpleCtx--instance-    ( Syntactic a dom, Eq (Internal a), Show (Internal a)-    , Syntactic b dom, Eq (Internal b), Show (Internal b)-    , Syntactic c dom, Eq (Internal c), Show (Internal c)-    , Syntactic d dom, Eq (Internal d), Show (Internal d)-    , Syntactic e dom, Eq (Internal e), Show (Internal e)-    , Syntactic f dom, Eq (Internal f), Show (Internal f)-    , Tuple  SimpleCtx :<: dom-    , Select SimpleCtx :<: dom-    ) =>-      Syntactic (a,b,c,d,e,f) dom-  where-    type Internal (a,b,c,d,e,f) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        , Internal f-        )--    desugar = desugarTup6 simpleCtx-    sugar   = sugarTup6 simpleCtx--instance-    ( Syntactic a dom, Eq (Internal a), Show (Internal a)-    , Syntactic b dom, Eq (Internal b), Show (Internal b)-    , Syntactic c dom, Eq (Internal c), Show (Internal c)-    , Syntactic d dom, Eq (Internal d), Show (Internal d)-    , Syntactic e dom, Eq (Internal e), Show (Internal e)-    , Syntactic f dom, Eq (Internal f), Show (Internal f)-    , Syntactic g dom, Eq (Internal g), Show (Internal g)-    , Tuple  SimpleCtx :<: dom-    , Select SimpleCtx :<: dom-    ) =>-      Syntactic (a,b,c,d,e,f,g) dom-  where-    type Internal (a,b,c,d,e,f,g) =-        ( Internal a-        , Internal b-        , Internal c-        , Internal d-        , Internal e-        , Internal f-        , Internal g-        )--    desugar = desugarTup7 simpleCtx-    sugar   = sugarTup7 simpleCtx-

@@ -0,0 +1,64 @@+module Language.Syntactic.Frontend.Monad where++++import Control.Monad.Cont+import Data.Typeable++import Language.Syntactic+import Language.Syntactic.Constructs.Binding.HigherOrder+import Language.Syntactic.Constructs.Monad++++-- | User interface to embedded monadic programs+newtype Mon ctx dom m a+  where+    Mon+        :: { unMon :: forall r . (Monad m, Typeable r) =>+               Cont (ASTF (HODomain ctx dom) (m r)) a+           }+        -> Mon ctx dom m a++deriving instance Functor (Mon ctx dom m)++instance (Monad m) => Monad (Mon ctx dom m)+  where+    return a = Mon $ return a+    ma >>= f = Mon $ unMon ma >>= unMon . f++-- | One-layer desugaring of monadic actions+desugarMonad+    :: ( MONAD m :<: dom+       , Monad m+       , Typeable1 m+       , Typeable a+       , Sat ctx a+       )+    => Mon ctx dom m (ASTF (HODomain ctx dom) a)+    -> ASTF (HODomain ctx dom) (m a)+desugarMonad = flip runCont (sugarSym Return) . unMon++-- | One-layer sugaring of monadic actions+sugarMonad+    :: ( MONAD m :<: dom+       , Monad m+       , Typeable1 m+       , Typeable a+       , Sat ctx a+       )+    => ASTF (HODomain ctx dom) (m a)+    -> Mon ctx dom m (ASTF (HODomain ctx dom) a)+sugarMonad ma = Mon $ cont $ sugarSym Bind ma++instance ( MONAD m :<: dom+         , Syntactic a (HODomain ctx dom)+         , Monad m, Typeable1 m+         , Sat ctx (Internal a)+         ) =>+         Syntactic (Mon ctx dom m a) (HODomain ctx dom)+  where+    type Internal (Mon ctx dom m a) = m (Internal a)+    desugar = desugarMonad . fmap desugar+    sugar   = fmap sugar   . sugarMonad+

@@ -15,7 +15,7 @@ import Data.Proxy  import Language.Syntactic-import Language.Syntactic.Features.Binding+import Language.Syntactic.Constructs.Binding import Language.Syntactic.Sharing.Utils  @@ -53,10 +53,6 @@     render (Node a) = showNode a  instance ToTree (Node ctx)---- | Partial `Node` projection with explicit context-prjNode :: (Node ctx :<: sup) => Proxy ctx -> sup a -> Maybe (Node ctx a)-prjNode _ = project   

@@ -32,7 +32,7 @@   reifyGraphM :: forall ctx dom a . Typeable a-    => (forall a . ASTF dom a -> Maybe (Witness' ctx a))+    => (forall a . ASTF dom a -> Maybe (SatWit ctx a))     -> IORef NodeId     -> IORef (History (AST dom))     -> ASTF dom a@@ -43,7 +43,7 @@     reifyNode :: Typeable b => ASTF dom b -> GraphMonad ctx dom (Full b)     reifyNode a = case canShare a of         Nothing -> reifyRec a-        Just Witness' | a `seq` True -> do+        Just SatWit | a `seq` True -> do           st   <- liftIO $ makeStableName a           hist <- liftIO $ readIORef history           case lookHistory hist (StName st) of@@ -67,11 +67,11 @@ -- is well-behaved in the sense that the worst thing that could happen is that -- sharing is lost. It is not possible to get false sharing. reifyGraph :: Typeable a-    => (forall a . ASTF dom a -> Maybe (Witness' ctx a))+    => (forall a . ASTF dom a -> Maybe (SatWit ctx a))          -- ^ A function that decides whether a given node can be shared.          -- 'Nothing' means \"don't share\"; 'Just' means \"share\". Nodes whose          -- result type fulfills @(`Sat` ctx a)@ can be shared, which is why the-         -- function returns a 'Witness''.+         -- function returns a 'SatWit'.     -> ASTF dom a     -> IO (ASG ctx dom a) reifyGraph canShare a = do

@@ -1,8 +1,9 @@ -- | This module is similar to "Language.Syntactic.Sharing.Reify", but operates--- on 'HOAST' rather than a general 'AST'. The reason for having this module is--- that when using 'HOAST', it is important to do simultaneous sharing analysis--- and 'HOLambda' reification. Obviously we cannot do sharing analysis first--- (using 'Language.Syntactic.Sharing.Reify.reifyGraph' from+-- on @`AST` (`HODomain` ctx dom)@ rather than a general 'AST'. The reason for+-- having this module is that when using 'HODomain', it is important to do+-- simultaneous sharing analysis and 'HOLambda' reification. Obviously we cannot+-- do sharing analysis first (using+-- 'Language.Syntactic.Sharing.Reify.reifyGraph' from -- "Language.Syntactic.Sharing.Reify"), since it needs to be able to look inside -- 'HOLambda'. On the other hand, if we did 'HOLambda' reification first (using -- 'reify'), we would destroy the sharing.@@ -26,8 +27,8 @@ import Data.Proxy  import Language.Syntactic-import Language.Syntactic.Features.Binding-import Language.Syntactic.Features.Binding.HigherOrder+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder import Language.Syntactic.Sharing.Graph import Language.Syntactic.Sharing.StableName import qualified Language.Syntactic.Sharing.Reify  -- For Haddock@@ -45,19 +46,20 @@   reifyGraphM :: forall ctx dom a . Typeable a-    => (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a))+    => (forall a . ASTF (HODomain ctx dom) a -> Maybe (SatWit ctx a))     -> IORef VarId     -> IORef NodeId-    -> IORef (History (HOAST ctx dom))-    -> HOASTF ctx dom a+    -> IORef (History (AST (HODomain ctx dom)))+    -> ASTF (HODomain ctx dom) a     -> GraphMonad ctx dom (Full a)  reifyGraphM canShare vSupp nSupp history = reifyNode   where-    reifyNode :: Typeable b => HOASTF ctx dom b -> GraphMonad ctx dom (Full b)+    reifyNode :: Typeable b =>+        ASTF (HODomain ctx dom) b -> GraphMonad ctx dom (Full b)     reifyNode a = case canShare a of         Nothing -> reifyRec a-        Just Witness' | a `seq` True -> do+        Just SatWit | a `seq` True -> do           st   <- liftIO $ makeStableName a           hist <- liftIO $ readIORef history           case lookHistory hist (StName st) of@@ -69,7 +71,7 @@               tell [(n, SomeAST a')]               return $ Symbol $ InjectL $ Node n -    reifyRec :: HOAST ctx dom b -> GraphMonad ctx dom b+    reifyRec :: AST (HODomain ctx dom) b -> GraphMonad ctx dom b     reifyRec (f :$: a)            = liftM2 (:$:) (reifyRec f) (reifyNode a)     reifyRec (Symbol (InjectR a)) = return $ Symbol (InjectR (InjectR a))     reifyRec (Symbol (InjectL (HOLambda f))) = do@@ -83,8 +85,8 @@  -- | Convert a syntax tree to a sharing-preserving graph reifyGraphTop :: Typeable a-    => (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a))-    -> HOASTF ctx dom a+    => (forall a . ASTF (HODomain ctx dom) a -> Maybe (SatWit ctx a))+    -> ASTF (HODomain ctx dom) a     -> IO (ASG ctx (Lambda ctx :+: Variable ctx :+: dom) a, VarId) reifyGraphTop canShare a = do     vSupp   <- newIORef 0@@ -100,16 +102,16 @@ -- This function is not referentially transparent (hence the 'IO'). However, it -- is well-behaved in the sense that the worst thing that could happen is that -- sharing is lost. It is not possible to get false sharing.-reifyGraph :: Reifiable ctx a dom internal-    => (forall a . HOASTF ctx dom a -> Maybe (Witness' ctx a))+reifyGraph :: Syntactic a (HODomain ctx dom)+    => (forall a . ASTF (HODomain ctx dom) a -> Maybe (SatWit ctx a))          -- ^ A function that decides whether a given node can be shared.          -- 'Nothing' means \"don't share\"; 'Just' means \"share\". Nodes whose          -- result type fulfills @(`Sat` ctx a)@ can be shared, which is why the-         -- function returns a 'Witness''.+         -- function returns a 'SatWit'.     -> a     -> IO-        ( ASG ctx (Lambda ctx :+: Variable ctx :+: dom) (NAryEval internal)+        ( ASG ctx (Lambda ctx :+: Variable ctx :+: dom) (Internal a)         , VarId         )-reifyGraph canShare = reifyGraphTop canShare . lambdaN . desugarN+reifyGraph canShare = reifyGraphTop canShare . desugar 

@@ -0,0 +1,190 @@+-- | Simple code motion transformation performing common sub-expression+-- elimination and variable hoisting. Note that the implementation is very+-- inefficient.+--+-- The code is based on an implementation by Gergely Dévai.++module Language.Syntactic.Sharing.SimpleCodeMotion+    ( codeMotion+    , reifySmart+    ) where++++import Control.Monad.State+import Data.Set as Set+import Data.Typeable++import Data.Proxy++import Language.Syntactic+import Language.Syntactic.Constructs.Binding+import Language.Syntactic.Constructs.Binding.HigherOrder++++-- | Substituting a sub-expression+substitute :: forall ctx dom a b+    .  ( Typeable a+       , Typeable b+       , Variable ctx :<: dom+       , Lambda ctx :<: dom+       , ExprEq dom+       )+    => Proxy ctx+    -> ASTF dom a  -- ^ Sub-expression to be replaced+    -> ASTF dom a  -- ^ Replacing sub-expression+    -> ASTF dom b  -- ^ Whole expression+    -> ASTF dom b+substitute ctx x y a = subst a+  where+    subst :: Typeable c => AST dom c -> AST dom c+    subst a | Just y' <- gcast y, alphaEq ctx x a = y'+    subst (f :$: a) = subst f :$: subst a+    subst a = a++-- | Count the number of occurrences of a sub-expression+count :: (Variable ctx :<: dom, Lambda ctx :<: dom, ExprEq dom)+    => Proxy ctx+    -> AST dom a  -- ^ Expression to count+    -> AST dom b  -- ^ Expression to count in+    -> VarId+count ctx a b+    | alphaEq ctx a b = 1+count ctx a (f :$: b) = count ctx a f + count ctx a b+count ctx a _         = 0++nonTerminal :: AST dom a -> Bool+nonTerminal (_ :$: _) = True+nonTerminal _         = False++data SomeAST ctx dom+  where+    SomeAST :: (Sat ctx a, Typeable a) => ASTF dom a -> SomeAST ctx dom++-- | Environment for the expression in the 'choose' function+data Env ctx dom = Env+    { context  :: Proxy ctx+    , inLambda :: Bool  -- ^ Whether the current expression is inside a lambda+    , counter  :: SomeAST ctx dom -> VarId+        -- ^ Counting the number of occurrences of an expression in the+        -- environment+    , dependencies :: Set VarId+        -- ^ The set of variables that are not allowed to occur in the chosen+        -- expression+    }++independent :: (Variable ctx :<: dom) => Env ctx dom -> AST dom a -> Bool+independent env (prjCtx (context env) -> Just (Variable v)) =+    not (v `member` dependencies env)+independent env (f :$: a) = independent env f && independent env a+independent _ _           = True++-- | Checks whether a sub-expression in a given environment can be lifted out+liftable :: (Variable ctx :<: dom, Lambda ctx :<: dom, Sat ctx a, Typeable a) =>+    Env ctx dom -> ASTF dom a -> Bool+liftable env a = independent env a && heuristic+    -- Lifting dependent expressions is semantically incorrect+  where+    heuristic = nonTerminal a && (inLambda env || (counter env (SomeAST a) > 1))++-- | Choose a sub-expression to share+choose :: forall ctx dom a+    .  ( Variable ctx :<: dom+       , Lambda ctx :<: dom+       , ExprEq dom+       , MaybeWitnessSat ctx dom+       , Typeable a+       )+    => ASTF dom a -> Maybe (SomeAST ctx dom)+choose a = chooseEnv env a+  where+    ctx = Proxy :: Proxy ctx++    env :: Env ctx dom+    env = Env+        { inLambda     = False+        , counter      = \(SomeAST b) -> count ctx b a+        , dependencies = empty+        , context      = ctx+        }++-- | Choose a sub-expression to share in an 'Env' environment+chooseEnv+    :: ( Variable ctx :<: dom+       , Lambda ctx :<: dom+       , MaybeWitnessSat ctx dom+       , Typeable a+       )+    => Env ctx dom -> ASTF dom a -> Maybe (SomeAST ctx dom)+chooseEnv env a+    | Just SatWit <- maybeWitnessSat (context env) a+    , liftable env a+    = Just (SomeAST a)+    | otherwise = chooseEnvSub env a++-- | Like 'chooseEnv', but does not consider the top expression for sharing+chooseEnvSub+    :: (Variable ctx :<: dom, Lambda ctx :<: dom, MaybeWitnessSat ctx dom)+    => Env ctx dom -> AST dom a -> Maybe (SomeAST ctx dom)+chooseEnvSub env ((prjCtx (context env) -> Just (Lambda v)) :$: a) =+    chooseEnv env' a+  where+    env' = env+        { inLambda     = True+        , dependencies = insert v (dependencies env)+        }+chooseEnvSub env (f :$: a) = chooseEnvSub env f `mplus` chooseEnv env a+chooseEnvSub _ _ = Nothing++-- | Perform common sub-expression elimination and variable hoisting+codeMotion :: forall ctx dom a+    .  ( Variable ctx :<: dom+       , Lambda ctx :<: dom+       , Let ctx ctx :<: dom+       , ExprEq dom+       , MaybeWitnessSat ctx dom+       , Typeable a+       )+    => Proxy ctx -> ASTF dom a -> State VarId (ASTF dom a)+codeMotion ctx a+    | Just SatWit <- maybeWitnessSat ctx a+    , Just b      <- choose a+    = share b+    | otherwise = descend ctx a+  where+    share :: Sat ctx a => SomeAST ctx dom -> State VarId (ASTF dom a)+    share (SomeAST b) = do+        b' <- codeMotion ctx b+        v  <- get; put (v+1)+        let x = inject (Variable v `withContext` ctx)+        body <- codeMotion ctx $ substitute ctx b x a+        return+            $   inject (letBind ctx)+            :$: b'+            :$: (inject (Lambda v `withContext` ctx) :$: body)++descend+    :: ( Variable ctx :<: dom+       , Lambda ctx :<: dom+       , Let ctx ctx :<: dom+       , ExprEq dom+       , MaybeWitnessSat ctx dom+       )+    => Proxy ctx -> AST dom a -> State VarId (AST dom a)+descend ctx (f :$: a) = liftM2 (:$:) (descend ctx f) (codeMotion ctx a)+descend _ a = return a++-- | Like 'reify' but with common sub-expression elimination and variable+-- hoisting+reifySmart+    :: ( Let ctx ctx :<: dom+       , ExprEq dom+       , MaybeWitnessSat ctx dom+       , Syntactic a (HODomain ctx dom)+       )+    => Proxy ctx+    -> a+    -> ASTF (Lambda ctx :+: Variable ctx :+: dom) (Internal a)+reifySmart ctx = flip evalState 0 . (codeMotion ctx <=< reifyM) . desugar+

@@ -60,6 +60,7 @@       Full (..)     , (:->) (..)     , HList (..)+    , WrapFull (..)     , ConsType     , ConsEval     , EvalResult@@ -72,20 +73,27 @@     , mapHList     , mapHListM     , appHList+    , appEvalHList     , ($:)     , AST (..)     , ASTF     , (:+:) (..)+    , ApplySym+    , appSym+    , appSymCtx       -- * Subsumption     , (:<:) (..)+    , injCtx+    , prjCtx       -- * Syntactic sugar     , Syntactic (..)     , resugar     , SyntacticN (..)+    , sugarSym+    , sugarSymCtx       -- * AST processing-    , queryNodeI     , queryNode-    , transformNodeC+    , queryNodeSimple     , transformNode       -- * Restricted syntax trees     , Sat (..)@@ -98,9 +106,12 @@         --         --      I don't know if the fix just removes the warning, or if it means         --      that 'Sat (..)' is enough.-    , Witness' (..)-    , witness'+    , witnessByProxy+    , SatWit (..)+    , fromSatWit     , WitnessSat (..)+    , MaybeWitnessSat (..)+    , maybeWitnessSatDefault     , withContext     , Poly     , poly@@ -139,6 +150,21 @@  infixr :->, :*: +-- | Can be used to turn a type constructor indexed by @a@ to a type constructor+-- indexed by @(`Full` a)@. This is useful together with 'HList', which assumes+-- its constructor to be indexed by @(`Full` a)@. That is, use+--+-- > HList (WrapFull c) ...+--+-- instead of+--+-- > HList c ...+--+-- if @c@ is not indexed by @(`Full` a)@.+data WrapFull c a+  where+    WrapFull :: { unwrapFull :: c a } -> WrapFull c (Full a)+ -- | Fully or partially applied constructor -- -- This class is private to the module to guarantee that all members of the@@ -155,40 +181,42 @@     type ConsEval' a     type EvalResult' a -    fromEval'   :: ConsEval' a -> a-    toEval'     :: a -> ConsEval' a-    listHList'  :: (forall a . c (Full a) -> b) -> HList c a -> [b]-    listHListM' :: Monad m => (forall a . c (Full a) -> m b) -> HList c a -> m [b]-    mapHList'   :: (forall a . c1 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 a-    mapHListM'  :: Monad m => (forall a . c1 (Full a) -> m (c2 (Full a))) -> HList c1 a -> m (HList c2 a)-    appHList'   :: AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a)-+    fromEval'     :: ConsEval' a -> a+    toEval'       :: a -> ConsEval' a+    listHList'    :: (forall a . c (Full a) -> b) -> HList c a -> [b]+    listHListM'   :: Monad m => (forall a . c (Full a) -> m b) -> HList c a -> m [b]+    mapHList'     :: (forall a . c1 (Full a) -> c2 (Full a)) -> HList c1 a -> HList c2 a+    mapHListM'    :: Monad m => (forall a . c1 (Full a) -> m (c2 (Full a))) -> HList c1 a -> m (HList c2 a)+    appHList'     :: AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a)+    appEvalHList' :: ConsEval a -> HList Identity a -> EvalResult a  instance ConsType' (Full a)   where     type ConsEval'   (Full a) = a     type EvalResult' (Full a) = a -    fromEval'         = Full-    toEval'           = result-    listHList'  f Nil = []-    listHListM' f Nil = return []-    mapHList'   f Nil = Nil-    mapHListM'  f Nil = return Nil-    appHList'   a Nil = a+    fromEval'           = Full+    toEval'             = result+    listHList'    f Nil = []+    listHListM'   f Nil = return []+    mapHList'     f Nil = Nil+    mapHListM'    f Nil = return Nil+    appHList'     a Nil = a+    appEvalHList' a Nil = a  instance ConsType' b => ConsType' (a :-> b)   where     type ConsEval'   (a :-> b) = a -> ConsEval' b     type EvalResult' (a :-> b) = EvalResult' b -    fromEval'                = Partial . (fromEval' .)-    toEval' (Partial f)      = toEval' . f-    listHList'  f (a :*: as) = f a : listHList' f as-    listHListM' f (a :*: as) = sequence (f a : listHList' f as)-    mapHList'   f (a :*: as) = f a :*: mapHList' f as-    mapHListM'  f (a :*: as) = liftM2 (:*:) (f a) (mapHListM' f as)-    appHList'   c (a :*: as) = appHList' (c :$: a) as+    fromEval'                  = Partial . (fromEval' .)+    toEval' (Partial f)        = toEval' . f+    listHList'    f (a :*: as) = f a : listHList' f as+    listHListM'   f (a :*: as) = sequence (f a : listHList' f as)+    mapHList'     f (a :*: as) = f a :*: mapHList' f as+    mapHListM'    f (a :*: as) = liftM2 (:*:) (f a) (mapHListM' f as)+    appHList'     c (a :*: as) = appHList' (c :$: a) as+    appEvalHList' f (a :*: as) = appEvalHList' (f $ result $ runIdentity a) as  -- | Fully or partially applied constructor --@@ -249,11 +277,16 @@     (forall a . c1 (Full a) -> m (c2 (Full a))) -> HList c1 a -> m (HList c2 a) mapHListM = mapHListM' --- | Apply the syntax tree to listed arguments+-- | Apply the syntax tree to the listed arguments appHList :: ConsType a =>     AST dom a -> HList (AST dom) a -> ASTF dom (EvalResult a) appHList = appHList' +-- | Apply the evaluation function to the listed arguments+appEvalHList :: ConsType a =>+    ConsEval a -> HList Identity a -> EvalResult a+appEvalHList = appEvalHList'+ -- | Semantic constructor application ($:) :: (a :-> b) -> a -> b Partial f $: a = f a@@ -290,6 +323,37 @@   +-- | Class that performs the type-level recursion needed by 'appSym'+class ApplySym a f dom | a dom -> f, f -> a dom+  where+    appSym' :: AST dom a -> f++instance ApplySym (Full a) (ASTF dom a) dom+  where+    appSym' = id++instance (Typeable a, ApplySym b f' dom) =>+    ApplySym (a :-> b) (ASTF dom a -> f') dom+  where+    appSym' sym a = appSym' (sym :$: a)++-- | Generic symbol application+--+-- 'appSym' has any type of the form:+--+-- > appSym :: (expr :<: AST dom, Typeable a, Typeable b, ..., Typeable x)+-- >     => expr (a :-> b :-> ... :-> Full x)+-- >     -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)+appSym :: (ApplySym a f dom, ConsType a, sym :<: AST dom) => sym a -> f+appSym sym = appSym' (inject sym)++-- | Generic symbol application with explicit context+appSymCtx  :: (ApplySym a f dom, ConsType a, sym ctx :<: dom) =>+    Proxy ctx -> sym ctx a -> f+appSymCtx _ = appSym+++ -------------------------------------------------------------------------------- -- * Subsumption --------------------------------------------------------------------------------@@ -331,6 +395,16 @@   +-- | 'inject' with explicit context+injCtx :: (sub ctx :<: sup, ConsType a) => Proxy ctx -> sub ctx a -> sup a+injCtx _ = inject++-- | 'project' with explicit context+prjCtx :: (sub ctx :<: sup) => Proxy ctx -> sup a -> Maybe (sub ctx a)+prjCtx _ = project+++ -------------------------------------------------------------------------------- -- * Syntactic sugar --------------------------------------------------------------------------------@@ -398,26 +472,63 @@   +-- | \"Sugared\" symbol application+--+-- 'sugarSym' has any type of the form:+--+-- > sugarSym ::+-- >     ( expr :<: AST dom+-- >     , Syntactic a dom+-- >     , Syntactic b dom+-- >     , ...+-- >     , Syntactic x dom+-- >     ) => expr (Internal a :-> Internal b :-> ... :-> Full (Internal x))+-- >       -> (a -> b -> ... -> x)+sugarSym+    :: (ConsType a, expr :<: AST dom, ApplySym a b dom, SyntacticN c b)+    => expr a -> c+sugarSym = sugarN . appSym++-- | \"Sugared\" symbol application with explicit context+sugarSymCtx+    :: (ConsType a, sym ctx :<: dom, ApplySym a b dom, SyntacticN c b)+    => Proxy ctx -> sym ctx a -> c+sugarSymCtx _ = sugarSym+++ -------------------------------------------------------------------------------- -- * AST processing -------------------------------------------------------------------------------- -newtype Wrap a b = Wrap {unWrap :: a}-  -- Only used in the definition of 'queryNode'+newtype Const a b = Const {unConst :: a}+  -- Only used in the definition of 'queryNodeSimple' --- | Like 'queryNode' but with the result indexed by the constructor's result--- type-queryNodeI :: forall dom a b-    .  (forall a . ConsType a => dom a -> HList (AST dom) a -> b (EvalResult a))-    -> ASTF dom a -> b a-queryNodeI f a = query a Nil+newtype WrapAST c dom a = WrapAST { unWrapAST :: c (AST dom a) }+  -- Only used in the definition of 'transformNode'++-- | Query an 'AST' using a function that gets direct access to the top-most+-- constructor and its sub-trees+--+-- Note that, by instantiating the type @c@ with @`AST` dom'@, we get the+-- following type, which shows that 'queryNode' can be directly used to+-- transform syntax trees (see also 'transformNode'):+--+-- > (forall a . ConsType a => dom a -> HList (AST dom) a -> ASTF dom' (EvalResult a))+-- > -> ASTF dom a+-- > -> ASTF dom' a+queryNode :: forall dom a c+    .  (forall a . ConsType a =>+          dom a -> HList (AST dom) a -> c (Full (EvalResult a)))+    -> ASTF dom a+    -> c (Full a)+queryNode f a = query a Nil   where-    query :: AST dom c -> HList (AST dom) c -> b (EvalResult c)+    query :: AST dom b -> HList (AST dom) b -> c (Full (EvalResult b))     query (Symbol a) args = f a args     query (c :$: a)  args = query c (a :*: args) --- | Query an 'AST' using a function that gets direct access to the top-most--- constructor and its sub-trees+-- | A simpler version of 'queryNode' -- -- This function can be used to create 'AST' traversal functions indexed by the -- symbol types, for example:@@ -432,7 +543,7 @@ -- >     count' (InjectR a) args = count' a args -- > -- > count :: Count dom => ASTF dom a -> Int--- > count = queryNode count'+-- > count = queryNodeSimple count' -- -- Here, @count@ represents some static analysis on an 'AST'. Each constructor -- in the tree will be queried by @count'@ indexed by the corresponding symbol@@ -451,36 +562,21 @@ -- > instance Count Add -- >   where -- >     count' Add (a :*: b :*: Nil) = 1 + count a + count b-queryNode :: forall dom a b+queryNodeSimple :: forall dom a b     .  (forall a . ConsType a => dom a -> HList (AST dom) a -> b)-    -> ASTF dom a -> b-queryNode f a = unWrap $ queryNodeI (\c -> Wrap . f c) a--+    -> ASTF dom a+    -> b+queryNodeSimple f a = unConst $ queryNode (\c -> Const . f c) a --- | Like 'transformNode' but with the result wrapped in a type constructor @c@-transformNodeC :: forall dom dom' c a+-- | A version of 'queryNode' where the result is a transformed syntax tree,+-- wrapped in a type constructor @c@+transformNode :: forall dom dom' c a     .  (  forall a . ConsType a        => dom a -> HList (AST dom) a -> c (ASTF dom' (EvalResult a))        )     -> ASTF dom a     -> c (ASTF dom' a)-transformNodeC f a = transform a Nil-  where-    transform :: AST dom b -> HList (AST dom) b -> c (ASTF dom' (EvalResult b))-    transform (Symbol a) args = f a args-    transform (c :$: a)  args = transform c (a :*: args)---- | Transform an 'AST' using a function that gets direct access to the top-most--- constructor and its sub-trees. This function is similar to 'queryNode', but--- returns a transformed 'AST' rather than abstract interpretation.-transformNode :: forall dom dom' a-    .  (  forall a . ConsType a-       => dom a -> HList (AST dom) a -> ASTF dom' (EvalResult a)-       )-    -> ASTF dom a-    -> ASTF dom' a-transformNode f a = runIdentity $ transformNodeC (\c -> Identity . f c) a+transformNode f a = unWrapAST $ queryNode (\a args -> WrapAST (f a args)) a   @@ -511,22 +607,48 @@     data Witness ctx a     witness :: Witness ctx a +witnessByProxy :: Sat ctx a => Proxy ctx -> Proxy a -> Witness ctx a+witnessByProxy _ _ = witness+ -- | Witness of a @(`Sat` ctx a)@ constraint. This is different from -- @(`Witness` ctx a)@, which witnesses the class encoded by @ctx@. 'Witness'' -- has a single constructor for all contexts, while 'Witness' has different -- constructors for different contexts.-data Witness' ctx a+data SatWit ctx a   where-    Witness' :: Sat ctx a => Witness' ctx a+    SatWit :: Sat ctx a => SatWit ctx a -witness' :: Witness' ctx a -> Witness ctx a-witness' Witness' = witness+fromSatWit :: SatWit ctx a -> Witness ctx a+fromSatWit SatWit = witness --- | Symbols that act as witnesses of their result type-class WitnessSat sym+-- | Expressions that act as witnesses of their result type+class WitnessSat expr   where-    type Context sym-    witnessSat :: sym a -> Witness' (Context sym) (EvalResult a)+    type SatContext expr+    witnessSat :: expr a -> SatWit (SatContext expr) (EvalResult a)++-- | Expressions that act as witnesses of their result type+class MaybeWitnessSat ctx expr+  where+    maybeWitnessSat :: Proxy ctx -> expr a -> Maybe (SatWit ctx (EvalResult a))++instance MaybeWitnessSat ctx dom => MaybeWitnessSat ctx (AST dom)+  where+    maybeWitnessSat ctx (Symbol a) = maybeWitnessSat ctx a+    maybeWitnessSat ctx (f :$: _)  = maybeWitnessSat ctx f++instance (MaybeWitnessSat ctx sub1, MaybeWitnessSat ctx sub2) =>+    MaybeWitnessSat ctx (sub1 :+: sub2)+  where+    maybeWitnessSat ctx (InjectL a) = maybeWitnessSat ctx a+    maybeWitnessSat ctx (InjectR a) = maybeWitnessSat ctx a++-- | Convenient default implementation of 'maybeWitnessSat'+maybeWitnessSatDefault :: WitnessSat expr+    => Proxy (SatContext expr)+    -> expr a+    -> Maybe (SatWit (SatContext expr) (EvalResult a))+maybeWitnessSatDefault _ = Just . witnessSat  -- | Type application for constraining the @ctx@ type of a parameterized symbol withContext :: sym ctx a -> Proxy ctx -> sym ctx a

@@ -1,5 +1,5 @@ Name:           syntactic-Version:        0.6+Version:        0.7 Synopsis:       Generic abstract syntax, and utilities for embedded languages Description:    This library provides:                 .@@ -21,6 +21,10 @@                 object languages, such as Feldspar. Currently, it does not                 support cyclic programs.                 .+                The following people have contributed to Syntactic:+                .+                  * Anders Persson+                .                 \[1\] /Data types à la carte/, by Wouter Swierstra, in                 /Journal of Functional Programming/, 2008                 .@@ -41,6 +45,19 @@   Examples/NanoFeldspar/Extra.hs   Examples/NanoFeldspar/Vector.hs   Examples/NanoFeldspar/Test.hs+  CEFP/MuFeldspar/Core.hs+  CEFP/MuFeldspar/Frontend.hs+  CEFP/MuFeldspar/Prelude.hs+  CEFP/MuFeldspar/Vector.hs+  CEFP/Imperative/Compiler.hs+  CEFP/Imperative/Imperative.hs+  CEFP/Examples/CodeApplication.hs+  CEFP/Examples/Exercise10.hs+  CEFP/Examples/Exercise12.hs+  CEFP/Examples/Exercise14.hs+  CEFP/Examples/ExProg.hs+  CEFP/Examples/SolutionsSec2.hs+  CEFP/Examples/Test.hs  source-repository head   type:     darcs@@ -53,16 +70,19 @@     Language.Syntactic.Interpretation.Equality     Language.Syntactic.Interpretation.Render     Language.Syntactic.Interpretation.Evaluation-    Language.Syntactic.Features.Annotate-    Language.Syntactic.Features.Symbol-    Language.Syntactic.Features.Literal-    Language.Syntactic.Features.Condition-    Language.Syntactic.Features.Tuple-    Language.Syntactic.Features.TupleSyntacticPoly-    Language.Syntactic.Features.TupleSyntacticSimple-    Language.Syntactic.Features.Binding-    Language.Syntactic.Features.Binding.HigherOrder-    Language.Syntactic.Features.Binding.PartialEval+    Language.Syntactic.Constructs.Annotate+    Language.Syntactic.Constructs.Symbol+    Language.Syntactic.Constructs.Literal+    Language.Syntactic.Constructs.Condition+    Language.Syntactic.Constructs.Tuple+    Language.Syntactic.Constructs.TupleSyntacticPoly+    Language.Syntactic.Constructs.TupleSyntacticSimple+    Language.Syntactic.Constructs.Binding+    Language.Syntactic.Constructs.Binding.HigherOrder+    Language.Syntactic.Constructs.Binding.Optimize+    Language.Syntactic.Constructs.Monad+    Language.Syntactic.Frontend.Monad+    Language.Syntactic.Sharing.SimpleCodeMotion     Language.Syntactic.Sharing.Utils     Language.Syntactic.Sharing.Graph     Language.Syntactic.Sharing.StableName@@ -83,19 +103,20 @@    Extensions:     DeriveDataTypeable+    DeriveFunctor+    EmptyDataDecls     FlexibleContexts     FlexibleInstances     FunctionalDependencies     GADTs     GeneralizedNewtypeDeriving     MultiParamTypeClasses+    PatternGuards     Rank2Types     ScopedTypeVariables+    StandaloneDeriving     TypeFamilies     TypeOperators     TypeSynonymInstances     ViewPatterns -    -- Required by GHC-6.12:-    EmptyDataDecls-    PatternGuards